Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 15 additions & 12 deletions cli/bin/main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down
20 changes: 11 additions & 9 deletions cli/lib/isla/assembler.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
29 changes: 19 additions & 10 deletions cli/lib/isla/converter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -32,15 +36,18 @@ 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 () =
let 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 =
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -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
Expand Down
14 changes: 7 additions & 7 deletions cli/lib/isla/ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -28,22 +28,22 @@ 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)
| Otoml.TomlString s -> (
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
Expand All @@ -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 =
Expand All @@ -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"];
Expand Down
4 changes: 2 additions & 2 deletions cli/lib/isla/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
2 changes: 1 addition & 1 deletion cli/lib/isla/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -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) }
Expand Down
6 changes: 4 additions & 2 deletions cli/lib/isla/symbols.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
Expand Down
4 changes: 2 additions & 2 deletions cli/lib/litmus/arch_id.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand All @@ -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)
16 changes: 13 additions & 3 deletions cli/lib/litmus/config.ml
Original file line number Diff line number Diff line change
Expand Up @@ -22,19 +22,29 @@ 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} *)

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

Expand Down
74 changes: 74 additions & 0 deletions cli/lib/litmus/error.ml
Original file line number Diff line number Diff line change
@@ -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
Loading
Loading