diff --git a/cli/bin/main.ml b/cli/bin/main.ml index 6cb41169..00450bc9 100644 --- a/cli/bin/main.ml +++ b/cli/bin/main.ml @@ -32,8 +32,8 @@ let parse_testfile fmt filename = | ".litmus" -> Isla | ".archsem" -> Archsem | _ -> - failwith - "Could not guess test format from filename. Only .archsem.toml and \ + Error.raise_error Config + "could not guess test format from filename. Only .archsem.toml and \ .litmus.toml are supported" ) in @@ -81,17 +81,17 @@ let run_tests model_name run_test files = let num_unexpected = count (fun r -> r = Unexpected) in let num_model_error = count (fun r -> r = ModelError) in let num_no_behaviour = count (fun r -> r = NoBehaviour) in - let num_parse_error = count (fun r -> r = ParseError) in + let num_setup_error = count (fun r -> r = SetupError) in let total = List.length results in let failures = List.filter (fun (_, r) -> r <> Expected) results - |> List.map (fun (f, r) -> (Filename.basename f, result_to_string r)) + |> List.map (fun (f, r) -> (Filename.basename f, styled_result r)) in Terminal.print_summary ~model_name ~total ~expected:num_expected ~unexpected:num_unexpected ~model_error:num_model_error - ~parse_error:num_parse_error ~no_behaviour:num_no_behaviour ~failures; + ~setup_error:num_setup_error ~no_behaviour:num_no_behaviour ~failures; if num_expected <> total then exit 1 @@ -122,12 +122,16 @@ let path_and_conf_term = match conf with | Some conf -> conf | None -> ( - let file = List.hd files in + let file = + match files with + | f :: _ -> f + | [] -> Error.raise_error Config "no test files found" + in let arch = Arch_id.guess_from_test file in match Config.default_path_for_arch arch with | Some conf -> conf | None -> - Printf.ksprintf failwith "Unable to find %s.toml automatically" + Error.raise_error Config "unable to find %s.toml automatically" (Arch_id.to_string arch) ) in @@ -179,12 +183,11 @@ let bbm_of_config () = | Some "strict" -> Arm.BBM.Strict | Some "off" -> Arm.BBM.Off | Some s -> - Printf.ksprintf failwith - "Config key vmp.bbm contains %s which is not off, lax or strict" s + Error.raise_error Config + "vmp.bbm contains %s which is not off, lax or strict" s | _ -> - failwith - "Config key vmp.bbm is unspecified in config, please specify on CLI with \ - --bbm" + Error.raise_error Config + "vmp.bbm is unspecified in config, please specify on CLI with --bbm" (** The virtual-memory promising command *) let cmd_vmp = diff --git a/cli/lib/isla/assembler.ml b/cli/lib/isla/assembler.ml index ead34fe5..65e86a3e 100644 --- a/cli/lib/isla/assembler.ml +++ b/cli/lib/isla/assembler.ml @@ -10,24 +10,26 @@ let get_assemble_cmd () = let get_extract_cmd () = Otoml.find (Config.get ()) Otoml.get_string ["assembler"; "extract"] -(** Run a cmd specified by a format string. Raise [Failure] if the command - fails *) +(** Run a cmd specified by a format string. Raise {!Litmus.Error.Cli_error} + if the command fails. *) let run_cmd fmt = let run cmd = let rc = Sys.command cmd in if rc != 0 then - Printf.ksprintf failwith "assember: %s failed with code %d" cmd rc + Litmus.Error.raise_error Assembler "%s failed with code %d" cmd rc in Printf.ksprintf run fmt (** Read a file into a [Byte.t] *) let read_file_bytes path : Bytes.t = - let ic = open_in_bin path in - let length = in_channel_length ic in - let buf = Bytes.create length in - really_input ic buf 0 length; - close_in ic; - buf + try + let ic = open_in_bin path in + let length = in_channel_length ic in + let buf = Bytes.create length in + really_input ic buf 0 length; + close_in ic; + buf + with Sys_error msg -> Litmus.Error.raise_error Assembler "%s" msg (** Assemble code into a [Bytes.t] *) let assemble (asm : string) : Bytes.t = diff --git a/cli/lib/isla/converter.ml b/cli/lib/isla/converter.ml index 4ced8a34..2e2ae8b3 100644 --- a/cli/lib/isla/converter.ml +++ b/cli/lib/isla/converter.ml @@ -11,11 +11,15 @@ let regval_of_toml = function (fun (k, v) -> match v with | Otoml.TomlInteger i -> (k, RegValGen.Number (Z.of_int i)) - | _ -> failwith ("config: register field " ^ k ^ " must be integer") + | _ -> + Litmus.Error.raise_error_ctx Config + ~ctx:("registers.defaults." ^ k) "must be integer" ) fields ) - | _ -> failwith "config: register default must be integer or inline table" + | _ -> + Litmus.Error.raise_error_ctx Config ~ctx:"registers.defaults" + "must be integer or inline table" let pc_reg arch = match arch with @@ -32,7 +36,8 @@ let instruction_step () = Otoml.find (Config.get ()) Otoml.get_integer ["assembler"; "instruction_step"] in if width <= 0 then - failwith "config: [assembler] instruction_step must be positive"; + Litmus.Error.raise_error_ctx Config ~ctx:"assembler.instruction_step" + "must be positive"; width let default_memory_size () = @@ -40,7 +45,9 @@ let default_memory_size () = Otoml.find_or ~default:8 (Config.get ()) Otoml.get_integer ["isla"; "default_memory_size"] in - if size <= 0 then failwith "config: [isla] default_memory_size must be positive"; + if size <= 0 then + Litmus.Error.raise_error_ctx Config ~ctx:"isla.default_memory_size" + "must be positive"; size let reg_requirement op value = @@ -71,11 +78,11 @@ let atoms_to_conds ~resolve_sym ~memory_size atoms = in (reg_atoms, mem_cond :: mem_atoms) | Assertion.CmpLoc (Assertion.Reg _, _, _) -> - failwith - "assertion: register-to-location comparisons are not supported" + Litmus.Error.raise_error_ctx Converter ~ctx:"final.assertion" + "register-to-location comparisons are not supported" | Assertion.CmpLoc (Assertion.Mem _, _, _) -> - failwith - "assertion: memory-to-location comparisons are not supported" + Litmus.Error.raise_error_ctx Converter ~ctx:"final.assertion" + "memory-to-location comparisons are not supported" ) ([], []) atoms in @@ -141,7 +148,8 @@ let build_data_memory syms sym addr init_value = let mem_size = default_memory_size () in let value = z_of_value syms init_value in if Z.numbits value > mem_size * 8 then - failwith ("Number doesn't fit in symbol " ^ sym); + Litmus.Error.raise_error_ctx Converter ~ctx:("locations." ^ sym) + "number doesn't fit in %d bytes" mem_size; let data = Bytes.make mem_size '\x00' in let bits = Z.to_bits value in Bytes.blit_string bits 0 data 0 (min mem_size (String.length bits)); @@ -193,7 +201,8 @@ let to_testrepr (ir : Ir.t) : Testrepr.t = let memory_size sym = match List.assoc_opt sym mem_sizes with | Some size -> size - | None -> failwith ("isla: unknown memory size for symbol: " ^ sym) + | None -> + Litmus.Error.raise_error_ctx Converter ~ctx:sym "unknown memory size" in let term_cond = let pc = pc_reg ir.arch in diff --git a/cli/lib/isla/ir.ml b/cli/lib/isla/ir.ml index 5d8589e2..c4bda25d 100644 --- a/cli/lib/isla/ir.ml +++ b/cli/lib/isla/ir.ml @@ -28,7 +28,7 @@ type t = (** {1 Isla test parsing } *) -let type_error fmt = Printf.ksprintf (fun s -> raise (Otoml.Type_error s)) fmt +let parse_error fmt = Litmus.Error.raise_error Parser fmt let parse_value = function | Otoml.TomlInteger i -> Int (Z.of_int i) @@ -36,14 +36,14 @@ let parse_value = function try Int (Z.of_string s) with Invalid_argument _ -> Sym s ) | value -> - type_error "Value is invalid, should be int or string, but is: %s" + parse_error "value is invalid, should be int or string, but is: %s" (Otoml.Printer.to_string value) let parse_thread (tid, table) = let tid = match int_of_string_opt tid with | Some tid -> tid - | None -> type_error "Thread table contained a non-number field: %s" tid + | None -> parse_error "thread table contained a non-number field: %s" tid in let _ = Otoml.get_table table in let code = Otoml.find table Otoml.get_string ["code"] |> String.trim in @@ -60,13 +60,14 @@ let parse_expect toml = match Otoml.get_string toml with | "sat" -> Sat | "unsat" -> Unsat - | expect -> raise (Otoml.Type_error ("invalid expectation value: " ^ expect)) + | expect -> + Litmus.Error.raise_error Parser "invalid expectation value: %s" expect let parse_assertion_expr s = let lexbuf = Lexing.from_string s in try Parser.assertion Lexer.token lexbuf with Parser.Error -> - type_error "assertion parse error at position %d in: %s" + parse_error "assertion parse error at position %d in: %s" lexbuf.lex_curr_p.pos_cnum s let parse_assertion toml = @@ -76,8 +77,7 @@ let parse_assertion toml = let parse_arch toml = let arch_string = Otoml.get_string toml in - try Litmus.Arch_id.of_string arch_string - with Failure msg -> raise (Otoml.Type_error msg) + Litmus.Arch_id.of_string arch_string let of_toml toml = { arch = Otoml.find toml parse_arch ["arch"]; diff --git a/cli/lib/isla/lexer.mll b/cli/lib/isla/lexer.mll index ff3a67db..031a90bf 100644 --- a/cli/lib/isla/lexer.mll +++ b/cli/lib/isla/lexer.mll @@ -25,7 +25,7 @@ rule token = parse | alpha alnum* as s { IDENT s } | eof { EOF } | _ as c { - failwith (Printf.sprintf + Litmus.Error.raise_error Parser "assertion lexer: unexpected character '%c' at position %d" - c (Lexing.lexeme_start lexbuf)) + c (Lexing.lexeme_start lexbuf) } diff --git a/cli/lib/isla/parser.mly b/cli/lib/isla/parser.mly index 5af57f06..15707186 100644 --- a/cli/lib/isla/parser.mly +++ b/cli/lib/isla/parser.mly @@ -39,7 +39,7 @@ atom: | l = loc; "="; v = NUM { match l with | Reg _ -> CmpCst (l, Eq, v) - | Mem _ -> failwith "assertion: use *sym = value for memory comparisons" + | Mem _ -> Litmus.Error.raise_error Parser "assertion: use *sym = value for memory comparisons" } | l1 = loc; "="; l2 = loc { CmpLoc (l1, Eq, l2) } | "*"; s = IDENT; "="; v = NUM { CmpCst (Mem s, Eq, v) } diff --git a/cli/lib/isla/symbols.ml b/cli/lib/isla/symbols.ml index d04fac0e..8762cd85 100644 --- a/cli/lib/isla/symbols.ml +++ b/cli/lib/isla/symbols.ml @@ -10,13 +10,15 @@ let resolve_opt t name = List.assoc_opt name t.table let resolve t name = match List.assoc_opt name t.table with | Some sym -> sym - | None -> failwith ("Unknown symbol: " ^ name) + | None -> Litmus.Error.raise_error_ctx Symbols ~ctx:name "unknown symbol" let page_bits () = let bits = Otoml.find (Litmus.Config.get ()) Otoml.get_integer ["isla"; "page_bits"] in - if bits < 0 then failwith "config: [isla] page_bits must be non-negative"; + if bits < 0 then + Litmus.Error.raise_error_ctx Config ~ctx:"isla.page_bits" + "must be non-negative"; bits let page_size () = 1 lsl page_bits () diff --git a/cli/lib/litmus/arch_id.ml b/cli/lib/litmus/arch_id.ml index 9e2b9d48..9a80041b 100644 --- a/cli/lib/litmus/arch_id.ml +++ b/cli/lib/litmus/arch_id.ml @@ -9,7 +9,7 @@ let of_string_opt = function let of_string arch = match of_string_opt arch with | Some arch -> arch - | None -> failwith ("unknown architecture: " ^ arch) + | None -> Error.raise_error Parser "unknown architecture: %s" arch let to_string = function Arm -> "Arm" @@ -22,5 +22,5 @@ let guess_from_test filename = let toml = Otoml.Parser.from_file filename in Otoml.find toml of_toml ["arch"] with exn -> - Printf.ksprintf failwith "Failed to guess architecture in %s with error : %s" + Error.raise_error Parser "failed to guess architecture in %s with error: %s" filename (Printexc.to_string exn) diff --git a/cli/lib/litmus/config.ml b/cli/lib/litmus/config.ml index 9d0f995e..a202546c 100644 --- a/cli/lib/litmus/config.ml +++ b/cli/lib/litmus/config.ml @@ -22,11 +22,21 @@ let default_path_for_arch arch = let exec_dir = Filename.dirname Sys.argv.(0) in first_some [find_from (Sys.getcwd ()) relpath; find_from exec_dir relpath] +let parse_toml_file path = + try Otoml.Parser.from_file path with + | Otoml.Parse_error (pos, msg) -> + let pos_str = + Option.fold ~none:"?" ~some:(fun (l, c) -> Printf.sprintf "%d:%d" l c) pos + in + Error.raise_error_ctx Config ~ctx:path "parse error at %s: %s" pos_str msg + | Sys_error msg -> Error.raise_error_ctx Config ~ctx:path "%s" msg + let of_arch arch = match default_path_for_arch arch with - | Some path -> Otoml.Parser.from_file path + | Some path -> parse_toml_file path | None -> - failwith ("config: no default config for arch " ^ Arch_id.to_string arch) + Error.raise_error_ctx Config ~ctx:(Arch_id.to_string arch) + "no default config found" (** {1 Global config} *) @@ -34,7 +44,7 @@ let global : t ref = ref empty let set config = global := config -let load file = global := Otoml.Parser.from_file file +let load file = global := parse_toml_file file let get () = !global diff --git a/cli/lib/litmus/error.ml b/cli/lib/litmus/error.ml new file mode 100644 index 00000000..5b16b47c --- /dev/null +++ b/cli/lib/litmus/error.ml @@ -0,0 +1,74 @@ +(** Structured error handling for the CLI. + + All CLI-originated errors raise {!Cli_error} with an {!origin} tag, + enabling the runner to distinguish parse-time errors from model crashes. + + {2 Error output format} + + The runner displays errors as: + {v ✗ test.toml [origin] ctx: message v} + + where [origin] comes from {!origin}, and [ctx] is an optional location + hint provided via {!raise_error_ctx}. + +*) + +(** Error origin — which logical subsystem raised the error. *) +type origin = + | Config (** Configuration file or CLI flag validation *) + | Parser (** TOML/term/assertion parsing *) + | Converter (** Isla IR to Testrepr conversion *) + | Assembler (** External assembler invocation *) + | Symbols (** Symbol table resolution *) + | Printer (** TOML output and file writing *) + | Runner (** Test execution and outcome checking *) + +(** The single exception type for all CLI errors. + + Caught by {!Runner.run_litmus_test} which uses nested [try-with]: + - Outer: parse phase errors ({!Cli_error} or [Otoml] exceptions) → [SetupError] + - Inner: run phase — {!Cli_error} from outcome checking → [ModelError]; + unrecognised exceptions (Coq model crash) → [ModelError] *) +exception Cli_error of origin * string + +(** Human-readable origin label for error output. *) +let string_of_origin = function + | Config -> "config" + | Parser -> "parser" + | Converter -> "converter" + | Assembler -> "assembler" + | Symbols -> "symbols" + | Printer -> "printer" + | Runner -> "runner" + +(** Raise a {!Cli_error} with a formatted message. + + {[ + Error.raise_error Config "must be positive" + (* raises Cli_error (Config, "must be positive") *) + + Error.raise_error Parser "unknown architecture: %s" arch + (* raises Cli_error (Parser, "unknown architecture: MIPS") *) + ]} *) +let raise_error origin fmt = + Printf.ksprintf (fun msg -> raise (Cli_error (origin, msg))) fmt + +(** Raise a {!Cli_error} with a context hint prepended to the message. + + Use [~ctx] to indicate {e where} in the input the error occurred — + a TOML key path, symbol name, register, or any relevant locator. + + {[ + Error.raise_error_ctx Config ~ctx:"assembler.instruction_step" + "must be positive" + (* raises Cli_error (Config, "assembler.instruction_step: must be positive") *) + + Error.raise_error_ctx Symbols ~ctx:"x" "unknown symbol" + (* raises Cli_error (Symbols, "x: unknown symbol") *) + + Error.raise_error_ctx Runner ~ctx:"outcome.0:X0" + "register not found in final state" + (* raises Cli_error (Runner, "outcome.0:X0: register not found ...") *) + ]} *) +let raise_error_ctx origin ~ctx fmt = + Printf.ksprintf (fun msg -> raise (Cli_error (origin, ctx ^ ": " ^ msg))) fmt diff --git a/cli/lib/litmus/parser.ml b/cli/lib/litmus/parser.ml index 6143a97d..78fa14b0 100644 --- a/cli/lib/litmus/parser.ml +++ b/cli/lib/litmus/parser.ml @@ -32,7 +32,9 @@ let rec toml_to_gen : Otoml.t -> RegValGen.t = function | TomlArray l -> Array (List.map toml_to_gen l) | TomlTable t | TomlInlineTable t -> Struct (List.map (fun (k, v) -> (k, toml_to_gen v)) t) - | v -> failwith ("Unsupported register value type: " ^ toml_type_name v) + | v -> + Error.raise_error Parser "unsupported register value type: %s" + (toml_type_name v) (** Parse [[registers]] into register lists with string keys *) let parse_test_registers toml = @@ -50,7 +52,8 @@ let parse_test_memory toml : Testrepr.memory_block list = in let n = List.length values in let step = Otoml.find table Otoml.get_integer ["step"] in - if step <= 0 then failwith "Memory block step must be positive"; + if step <= 0 then + Error.raise_error Parser "memory block step must be positive"; let data = Bytes.create (n * step) in List.iteri (fun i v -> @@ -65,7 +68,7 @@ let parse_test_memory toml : Testrepr.memory_block list = |> Option.fold ~none:Testrepr.Data ~some:Testrepr.memory_kind_of_string in if kind = Code && sym <> None then - failwith "[[memory]] code blocks must not have sym"; + Error.raise_error_ctx Parser ~ctx:"memory" "code blocks must not have sym"; {addr; step; data; sym; kind} in Otoml.find toml (Otoml.get_array parse_memory_block) ["memory"] @@ -86,7 +89,8 @@ let parse_reg_requirement (toml : Otoml.t) : Testrepr.reg_requirement = | (Some (TomlString "eq"), Some v) -> Testrepr.ReqEq (toml_to_gen v) | (Some (TomlString "ne"), Some v) -> Testrepr.ReqNe (toml_to_gen v) | (Some (TomlString op), _) -> - failwith ("[[outcome]] unknown requirement op: " ^ op) + Error.raise_error_ctx Parser ~ctx:"outcome" "unknown requirement op: %s" + op | _ -> Testrepr.ReqEq (toml_to_gen toml) ) | _ -> Testrepr.ReqEq (toml_to_gen toml) @@ -117,10 +121,9 @@ let parse_mem_requirement (toml : Otoml.t) : Testrepr.mem_requirement = | (Some (TomlString "eq"), Some v) -> MemEq (Z.of_int @@ Otoml.get_integer v) | (Some (TomlString "ne"), Some v) -> MemNe (Z.of_int @@ Otoml.get_integer v) | (_, _) -> - failwith - ("[[outcome]] unknown memory requirement: " - ^ Otoml.Printer.to_string toml - ) + Error.raise_error_ctx Parser ~ctx:"outcome.mem" + "unknown memory requirement: %s" + (Otoml.Printer.to_string toml) ) | _ -> MemEq (Z.of_int @@ Otoml.get_integer toml) @@ -128,7 +131,8 @@ let parse_mem_entry mem sym toml : Testrepr.mem_cond = let block = try Testrepr.mem_by_sym sym mem with Not_found -> - failwith ("[[outcome]].mem." ^ sym ^ " not found in memory") + Error.raise_error_ctx Parser ~ctx:("outcome.mem." ^ sym) + "not found in memory blocks" in let req = parse_mem_requirement toml in {sym; addr = block.addr; size = Testrepr.block_size block; req} @@ -154,9 +158,11 @@ let parse_test_finals mem toml : Testrepr.final_cond list = | (Some (regs, mem), None) -> Testrepr.Observable (regs, mem) | (None, Some (regs, mem)) -> Testrepr.Unobservable (regs, mem) | (Some _, Some _) -> - failwith "[[outcome]] cannot have both observable and unobservable" + Error.raise_error_ctx Parser ~ctx:"outcome" + "cannot have both observable and unobservable" | (None, None) -> - failwith "[[outcome]] must have observable or unobservable key" + Error.raise_error_ctx Parser ~ctx:"outcome" + "must have observable or unobservable key" in Otoml.find toml (Otoml.get_array parse_test_final) ["outcome"] @@ -173,7 +179,9 @@ let resolve_mem_conds memory (mcs : Testrepr.mem_cond list) = let (addr, size) = match List.assoc_opt mc.sym sym_table with | Some (addr, step) -> (addr, if mc.size = 0 then step else mc.size) - | None -> failwith ("[[outcome]] unknown memory symbol: " ^ mc.sym) + | None -> + Error.raise_error_ctx Parser ~ctx:("outcome.mem." ^ mc.sym) + "unknown memory symbol" in {mc with addr; size} ) diff --git a/cli/lib/litmus/printer.ml b/cli/lib/litmus/printer.ml index 72a580c4..acce8e67 100644 --- a/cli/lib/litmus/printer.ml +++ b/cli/lib/litmus/printer.ml @@ -24,7 +24,7 @@ let registers_to_toml regs : Otoml.t = let memory_block_to_toml (block : Testrepr.memory_block) : Otoml.t = let step = block.step in - if step <= 0 then failwith "memory block step must be positive"; + if step <= 0 then Error.raise_error Printer "memory block step must be positive"; let len = Bytes.length block.data in let n = len / step in assert (len = n * step); @@ -137,6 +137,8 @@ let to_string test = Otoml.Printer.to_string ~force_table_arrays:true (to_toml test) let to_file path test = - let oc = open_out path in - output_string oc (to_string test); - close_out oc + try + let oc = open_out path in + output_string oc (to_string test); + close_out oc + with Sys_error msg -> Error.raise_error_ctx Printer ~ctx:path "%s" msg diff --git a/cli/lib/litmus/runner.ml b/cli/lib/litmus/runner.ml index cba771b9..ff39e5e6 100644 --- a/cli/lib/litmus/runner.ml +++ b/cli/lib/litmus/runner.ml @@ -7,7 +7,7 @@ type test_result = | Unexpected (** Outcome did not match test expectations *) | ModelError (** Model produced errors during execution *) | NoBehaviour (** Model produces no behaviours (model bug) *) - | ParseError (** Parser or configuration error *) + | SetupError (** Pre-execution error: parsing, config, conversion, assembly *) (** {1 Display Helpers} *) let rec string_of_regval_gen : Archsem.RegValGen.t -> string = function @@ -52,12 +52,21 @@ let mem_cond_to_string mem_reqs = mem_reqs |> String.concat " " -let result_to_string = function - | Expected -> Terminal.green ^ "EXPECTED" ^ Terminal.reset - | Unexpected -> Terminal.yellow ^ "UNEXPECTED" ^ Terminal.reset - | ModelError -> Terminal.red ^ "MODEL ERROR" ^ Terminal.reset - | NoBehaviour -> Terminal.red ^ "NO BEHAVIOUR" ^ Terminal.reset - | ParseError -> Terminal.red ^ "PARSE ERROR" ^ Terminal.reset +let string_of_result = function + | Expected -> "EXPECTED" + | Unexpected -> "UNEXPECTED" + | ModelError -> "MODEL ERROR" + | NoBehaviour -> "NO BEHAVIOUR" + | SetupError -> "SETUP ERROR" + +let styled_result r = + let color = + match r with + | Expected -> Terminal.green + | Unexpected -> Terminal.yellow + | _ -> Terminal.red + in + color ^ string_of_result r ^ Terminal.reset module Make (Arch : Archsem.Arch) = struct open Arch @@ -72,8 +81,8 @@ module Make (Arch : Archsem.Arch) = struct let reg = Reg.of_string name in match RegMap.get_opt reg regs with | None -> - failwith - ("[[outcome]] register not found in final state: " ^ name) + Error.raise_error_ctx Runner ~ctx:("outcome." ^ name) + "register not found in final state" | Some rv -> ( match req with | Testrepr.ReqEq exp -> rv = RegVal.of_gen reg exp @@ -92,8 +101,9 @@ module Make (Arch : Archsem.Arch) = struct (fun (mc : Testrepr.mem_cond) -> match MemMap.lookup_opt mc.addr mc.size mem with | None -> - failwith - (Printf.sprintf "[[outcome]] memory not found at 0x%x" mc.addr) + Error.raise_error_ctx Runner + ~ctx:(Printf.sprintf "outcome.*0x%x" mc.addr) + "memory not found at address" | Some actual -> ( match mc.req with | Testrepr.MemEq expected -> Z.equal actual expected @@ -198,42 +208,55 @@ module Make (Arch : Archsem.Arch) = struct let (init, term) = AS.testrepr_to_archstate test in run_executions model init fuel term test.finals + let print_error name origin msg = + Printf.printf " %s%s%s %s %s[%s] %s%s\n" Terminal.red Terminal.cross + Terminal.reset name Terminal.red origin msg Terminal.reset + let run_litmus_test ~parse model filename = let name = Filename.basename filename in if not (Sys.file_exists filename) then ( - Printf.printf " %s✗%s %s %sfile not found%s\n" Terminal.red Terminal.reset - name Terminal.red Terminal.reset; - ParseError + print_error name "config" "file not found"; + SetupError ) else try let test = parse filename in - let (result, msgs) = run_testrepr model test in - let (icon, color) = - match result with - | Expected -> (Terminal.check, Terminal.green) - | Unexpected -> (Terminal.cross, Terminal.yellow) - | _ -> (Terminal.cross, Terminal.red) - in - Printf.printf " %s%s%s %s\n" color icon Terminal.reset name; - List.iter (fun m -> Printf.printf " %s\n" m) msgs; - result + (* Inner try: exceptions here are model crashes, not parse errors *) + try + let (result, msgs) = run_testrepr model test in + let (icon, color) = + match result with + | Expected -> (Terminal.check, Terminal.green) + | Unexpected -> (Terminal.cross, Terminal.yellow) + | _ -> (Terminal.cross, Terminal.red) + in + Printf.printf " %s%s%s %s\n" color icon Terminal.reset name; + List.iter (fun m -> Printf.printf " %s\n" m) msgs; + result + with + | Error.Cli_error (origin, msg) -> + print_error name (Error.string_of_origin origin) msg; + ModelError + | exn -> + print_error name "model" (Printexc.to_string exn); + ModelError with + | Error.Cli_error (origin, msg) -> + print_error name (Error.string_of_origin origin) msg; + SetupError | Otoml.Parse_error (pos, msg) -> - Printf.printf " %s✗%s %s %sparse error at %s: %s%s\n" Terminal.red - Terminal.reset name Terminal.red - (Option.fold ~none:"?" - ~some:(fun (l, c) -> Printf.sprintf "%d:%d" l c) - pos - ) - msg Terminal.reset; - ParseError + let pos_str = + Option.fold ~none:"?" + ~some:(fun (l, c) -> Printf.sprintf "%d:%d" l c) + pos + in + print_error name "parser" + (Printf.sprintf "parse error at %s: %s" pos_str msg); + SetupError | Failure msg -> - Printf.printf " %s✗%s %s %s%s%s\n" Terminal.red Terminal.reset name - Terminal.red msg Terminal.reset; - ParseError + print_error name "setup" msg; + SetupError | exn -> - Printf.printf " %s✗%s %s %s%s%s\n" Terminal.red Terminal.reset name - Terminal.red (Printexc.to_string exn) Terminal.reset; - ParseError + print_error name "setup" (Printexc.to_string exn); + SetupError end diff --git a/cli/lib/litmus/terminal.ml b/cli/lib/litmus/terminal.ml index 87542edc..59cf6975 100644 --- a/cli/lib/litmus/terminal.ml +++ b/cli/lib/litmus/terminal.ml @@ -35,7 +35,7 @@ let print_summary ~expected ~unexpected ~model_error - ~parse_error + ~setup_error ~no_behaviour ~failures = @@ -66,8 +66,8 @@ let print_summary if model_error > 0 then Printf.printf " %s%s%s Model Error %s%d%s\n" red cross reset red model_error reset; - if parse_error > 0 then - Printf.printf " %s%s%s Parse Error %s%d%s\n" red cross reset red parse_error + if setup_error > 0 then + Printf.printf " %s%s%s Setup Error %s%d%s\n" red cross reset red setup_error reset; if no_behaviour > 0 then Printf.printf " %s%s%s No Behaviour %s%d%s\n" red cross reset red diff --git a/cli/lib/litmus/testrepr.ml b/cli/lib/litmus/testrepr.ml index cb32dc5c..e5e7a826 100644 --- a/cli/lib/litmus/testrepr.ml +++ b/cli/lib/litmus/testrepr.ml @@ -67,5 +67,7 @@ type t = let block_size (mb : memory_block) : int = Bytes.length mb.data -let mem_by_sym (sym : string) = - List.find (fun (mb : memory_block) -> mb.sym = Some sym) +let mem_by_sym (sym : string) mem = + match List.find_opt (fun (mb : memory_block) -> mb.sym = Some sym) mem with + | Some mb -> mb + | None -> raise Not_found diff --git a/cli/lib/litmus/toArchState.ml b/cli/lib/litmus/toArchState.ml index b7a4bf83..40d45e82 100644 --- a/cli/lib/litmus/toArchState.ml +++ b/cli/lib/litmus/toArchState.ml @@ -29,10 +29,9 @@ module Make (Arch : Archsem.Arch) = struct match RegMap.get_opt reg rm with | Some actual -> rv = actual | None -> - failwith - ("[[termCond]] register not found in thread state: " - ^ Reg.to_string reg - ) + Error.raise_error_ctx Runner + ~ctx:("termCond." ^ Reg.to_string reg) + "register not found in thread state" ) parsed @@ -41,11 +40,9 @@ module Make (Arch : Archsem.Arch) = struct let validate_thread_count regs term = let num_threads = List.length regs in if List.length term <> num_threads then - failwith - (Printf.sprintf - "[[termCond]] count (%d) must match [[registers]] thread count (%d)" - (List.length term) num_threads - ) + Error.raise_error_ctx Runner ~ctx:"termCond" + "count (%d) must match registers thread count (%d)" (List.length term) + num_threads (** Convert Testrepr.t into ArchState.t and termination conditions. *) let testrepr_to_archstate (test : Testrepr.t) = diff --git a/cli/tests/unit/litmus/config_test.ml b/cli/tests/unit/litmus/config_test.ml index 96f6f99f..ed587166 100644 --- a/cli/tests/unit/litmus/config_test.ml +++ b/cli/tests/unit/litmus/config_test.ml @@ -18,9 +18,9 @@ let default_config_tests = ); ("RISCV alias is rejected" >:: fun _ -> - assert_raises (Failure "unknown architecture: RISCV") (fun () -> - ignore (Arch_id.of_string "RISCV") - ) + assert_raises + (Error.Cli_error (Parser, "unknown architecture: RISCV")) + (fun () -> ignore (Arch_id.of_string "RISCV")) ); ("loads built-in Arm config" >:: fun _ -> diff --git a/cli/tests/unit/litmus/dune b/cli/tests/unit/litmus/dune index ab016d6a..64c5ae5d 100644 --- a/cli/tests/unit/litmus/dune +++ b/cli/tests/unit/litmus/dune @@ -4,8 +4,8 @@ (libraries litmus otoml)) (tests - (names testrepr_test printer_test config_test) - (modules testrepr_test printer_test config_test) + (names testrepr_test printer_test config_test error_test) + (modules testrepr_test printer_test config_test error_test) (libraries archsem litmus test_utils otoml ounit2) (deps (glob_files ../../seq/*.toml) diff --git a/cli/tests/unit/litmus/error_test.ml b/cli/tests/unit/litmus/error_test.ml new file mode 100644 index 00000000..2f71e6a7 --- /dev/null +++ b/cli/tests/unit/litmus/error_test.ml @@ -0,0 +1,56 @@ +(** Unit tests for the runner's error classification. + + Verifies that the nested try-with in {!Runner.run_litmus_test} + correctly separates parse-phase errors ([SetupError]) from + model-phase crashes ([ModelError]). *) + +open OUnit2 +open Litmus +module Arm = Archsem.Arm +module ArmRunner = Runner.Make (Arm) + +(** A path that exists so [Sys.file_exists] passes. + The parse function is injected, so the content is never read. *) +let dummy_path = "/dev/null" + +let tests = + "runner error classification" + >::: [ ("parse phase error returns SetupError" + >:: fun _ -> + Test_utils.setup (); + let parse _filename = + Error.raise_error Config "simulated config error" + in + let model = Arm.(seq_model tiny_isa) in + let result = ArmRunner.run_litmus_test ~parse model dummy_path in + assert_equal ~printer:Runner.string_of_result Runner.SetupError result + ); + ("file not found returns SetupError" + >:: fun _ -> + Test_utils.setup (); + let parse _f = failwith "should not be called" in + let model = Arm.(seq_model tiny_isa) in + let result = + ArmRunner.run_litmus_test ~parse model "/nonexistent/file.toml" + in + assert_equal ~printer:Runner.string_of_result Runner.SetupError result + ); + ("model crash returns ModelError" + >:: fun _ -> + Test_utils.setup (); + let parse _filename : Testrepr.t = + { arch = "Arm"; + name = "crash-test"; + registers = [[]]; + memory = []; + term_cond = [[]]; + finals = [] + } + in + let model _fuel _term _init = failwith "simulated model crash" in + let result = ArmRunner.run_litmus_test ~parse model dummy_path in + assert_equal ~printer:Runner.string_of_result Runner.ModelError result + ) + ] + +let () = run_test_tt_main tests diff --git a/cli/tests/unit/litmus/testrepr_test.ml b/cli/tests/unit/litmus/testrepr_test.ml index c6470203..f5fcfa3d 100644 --- a/cli/tests/unit/litmus/testrepr_test.ml +++ b/cli/tests/unit/litmus/testrepr_test.ml @@ -187,7 +187,8 @@ let parse_bad_file_test = in "parse_bad_file" >::: [ parse_fails "non-positive memory step fails" - (Failure "Memory block step must be positive") bad_step_toml; + (Error.Cli_error (Parser, "memory block step must be positive")) + bad_step_toml; parse_fails "size-only memory blocks fail" (Otoml.Key_error "Failed to retrieve a value at step: field step not found"