From e8612db1d4e6b383cf442e44db0439ab68c5f907 Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 3 Apr 2026 20:55:14 +0100 Subject: [PATCH 01/13] Print final states --- .gitignore | 1 + cli/bin/main.ml | 42 +++++-- cli/lib/litmus/runner.ml | 142 ++++++++++++++++++++-- cli/lib/litmus/testrepr.ml | 7 ++ cli/tests/unit/isla/converter_test.ml | 28 ++++- cli/tests/unit/litmus/testrepr_test.ml | 9 +- cli/tests/x86/um/R_PO_MFENCE.archsem.toml | 2 +- cli/tests/x86/um/R_PO_MFENCE.litmus.toml | 2 +- 8 files changed, 205 insertions(+), 28 deletions(-) diff --git a/.gitignore b/.gitignore index ebb934b0..3915e5d0 100644 --- a/.gitignore +++ b/.gitignore @@ -10,3 +10,4 @@ _build _opam .envrc +.vscode diff --git a/cli/bin/main.ml b/cli/bin/main.ml index 5c360453..b37c6296 100644 --- a/cli/bin/main.ml +++ b/cli/bin/main.ml @@ -185,18 +185,24 @@ let format_term = Arg.(value & opt (some format_enum) None & info ["format"; "f"] ~doc ~docv:"FMT") (** The sequential model command *) -let cmd_seq = +let cmd_seq print_final_states = let run = - let+ files = path_and_conf_term and+ fmt = format_term in + let+ files = path_and_conf_term + and+ fmt = format_term + and+ print_final_states = print_final_states in let parse = parse_testfile fmt in match Config.get_arch () with | Arm -> run_tests "arm-seq" - (ArmRunner.run_litmus_test ~parse Arm.(seq_model tiny_isa)) + (ArmRunner.run_litmus_test ~parse print_final_states + Arm.(seq_model tiny_isa) + ) files | X86 -> run_tests "x86-seq" - (X86Runner.run_litmus_test ~parse X86.(seq_model tiny_isa)) + (X86Runner.run_litmus_test ~parse print_final_states + X86.(seq_model tiny_isa) + ) files in let info = @@ -206,13 +212,17 @@ let cmd_seq = Cmd.v info run (** The user-mode promising command *) -let cmd_ump = +let cmd_ump print_final_states = let run = - let+ files = path_and_conf_term and+ fmt = format_term in + let+ files = path_and_conf_term + and+ fmt = format_term + and+ print_final_states = print_final_states in let parse = parse_testfile fmt in assert (Config.get_arch () = Arch_id.Arm); run_tests "ump" - (ArmRunner.run_litmus_test ~parse Arm.(umProm_model tiny_isa)) + (ArmRunner.run_litmus_test ~parse print_final_states + Arm.(umProm_model tiny_isa) + ) files in let info = @@ -235,7 +245,7 @@ let bbm_of_config () = --bbm" (** The virtual-memory promising command *) -let cmd_vmp = +let cmd_vmp print_final_states = let open Arm in let bbm_mode = let doc = "Break-before-make mode: off, lax, or strict" in @@ -250,11 +260,14 @@ let cmd_vmp = let run = let+ files = path_and_conf_term and+ bbm_param = bbm_mode - and+ fmt = format_term in + and+ fmt = format_term + and+ print_final_states = print_final_states in let parse = parse_testfile fmt in assert (Config.get_arch () = Arch_id.Arm); run_tests "vmp" - (ArmRunner.run_litmus_test ~parse (vmProm_model ~bbm_param tiny_isa)) + (ArmRunner.run_litmus_test ~parse print_final_states + (vmProm_model ~bbm_param tiny_isa) + ) files in let info = @@ -266,7 +279,7 @@ let cmd_vmp = in Cmd.v info run -let cmd_tso = +let cmd_tso print_final_states = let no_eager = let doc = "Disable eager transitions (eager is enabled by default)" in Arg.(value & flag & info ["no-eager"] ~doc) @@ -274,12 +287,15 @@ let cmd_tso = let run = let+ files = path_and_conf_term and+ fmt = format_term - and+ no_eager = no_eager in + and+ no_eager = no_eager + and+ print_final_states = print_final_states in let allow_eager = not no_eager in let parse = parse_testfile fmt in assert (Config.get_arch () = Arch_id.X86); run_tests "tso" - (X86Runner.run_litmus_test ~parse X86.(op_model ~allow_eager tiny_isa)) + (X86Runner.run_litmus_test ~parse print_final_states + X86.(op_model ~allow_eager tiny_isa) + ) files in let info = diff --git a/cli/lib/litmus/runner.ml b/cli/lib/litmus/runner.ml index 53c4e97c..ac06da0e 100644 --- a/cli/lib/litmus/runner.ml +++ b/cli/lib/litmus/runner.ml @@ -98,10 +98,31 @@ let result_to_string = function | NoBehaviour -> Terminal.red ^ "NO BEHAVIOUR" ^ Terminal.reset | ParseError -> Terminal.red ^ "PARSE ERROR" ^ Terminal.reset +let outcome_freq_to_string yes_freq no_freq = + if yes_freq = 0 then "Never" else if no_freq = 0 then "Always" else "Sometimes" + +(* Return string of format: Observation *) +let test_observation_stats_to_string bool_list test_name = + let (obs_count, not_obs_count) = + List.fold_left + (fun (t, f) b -> if b then (t + 1, f) else (t, f + 1)) + (0, 0) bool_list + in + Printf.sprintf "Observation %s %s %d %d" test_name + (outcome_freq_to_string obs_count not_obs_count) + obs_count not_obs_count + module Make (Arch : Archsem.Arch) = struct open Arch module AS = ToArchState.Make (Arch) + (* Allow conversion of an iterable structure of ArchStates into a set*) + module ArchStateSet = Set.Make (struct + type t = Arch.ArchState.t + + let compare = Stdlib.compare + end) + let check_outcome (fs : ArchState.t) (cond : Testrepr.thread_cond list) : bool = List.for_all (fun (tid, reqs) -> @@ -141,7 +162,82 @@ module Make (Arch : Archsem.Arch) = struct ) mem_conds - let run_executions model init fuel term finals = + let final_regs_to_string + (fs : ArchState.t) + (cond : Testrepr.thread_cond list) + (arch : string) : string + = + String.concat " " + (List.concat_map + (fun (tid, reqs) -> + let regs = ArchState.reg tid fs in + List.map + (fun (req_name, _) -> + let reg = Reg.of_string req_name in + let value = RegMap.geti reg regs in + (* Note that we are making the register name lowercase *) + let reg_name = + if + String.starts_with ~prefix:"x86" (String.lowercase_ascii arch) + then String.lowercase_ascii req_name + else req_name + in + Printf.sprintf "%d:%s=%d;" tid reg_name value + ) + reqs + ) + cond + ) + + let final_mem_to_string + (fs : ArchState.t) + (mem_conds : Testrepr.mem_cond list) + (mem_blocks : Testrepr.memory_block list) : string + = + let mem = ArchState.mem fs in + String.concat " " + (List.map + (fun (mc : Testrepr.mem_cond) -> + let mem_symbol = Testrepr.mem_addr_to_symbol mc.addr mem_blocks in + let value = MemMap.lookupi mc.addr mc.size mem in + Printf.sprintf "[%s]=%d;" mem_symbol value + ) + mem_conds + ) + + (* Print observation statistics. The format is: + Ok/No + Observation Always/Sometimes/Never <#times_test_cond_observed> <#times_test_cond_not_observed> *) + let observation_statistics_string + (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) + (checking_for_positive : bool) + (state_list : ArchState.t list) + (test_name : string) : string + = + let (matched_msg, not_matched_msg) = + if checking_for_positive then ("Ok", "No (\"allowed\" not found)") + else ("No (\"not allowed\" found)", "Ok") + in + + String.concat "\n" + (List.map + (fun (cond, mem_cond) -> + let each_obs_ok = + List.map + (fun fs -> check_outcome fs cond && check_mem_outcome fs mem_cond) + state_list + in + let matched = List.exists Fun.id each_obs_ok in + let stats_opening = + if matched then matched_msg else not_matched_msg + in + stats_opening ^ "\n" + ^ test_observation_stats_to_string each_obs_ok test_name + ) + conds + ) + + let run_executions print_final_states model init fuel term test = let msgs = ref [] in let msg s = msgs := s :: !msgs in let results = model fuel term init in @@ -149,12 +245,12 @@ module Make (Arch : Archsem.Arch) = struct let observable = List.filter_map (function Testrepr.Observable (c, mc) -> Some (c, mc) | _ -> None) - finals + test.Testrepr.finals in let unobservable = List.filter_map (function Testrepr.Unobservable (c, mc) -> Some (c, mc) | _ -> None) - finals + test.Testrepr.finals in let errors = @@ -173,6 +269,31 @@ module Make (Arch : Archsem.Arch) = struct results in + (* If the print-final-states flag is set, print all observable states and statistics *) + if print_final_states then ( + let final_states_set = ArchStateSet.of_list final_states in + (* Print number of distinct observed states *) + msg (Printf.sprintf "States %d" (ArchStateSet.cardinal final_states_set)); + (* Print each distinct observable state *) + let conds = observable @ unobservable in + if conds <> [] then ( + let (reg_cond, mem_cond) = List.hd (observable @ unobservable) in + ArchStateSet.iter + (fun fs -> + msg + (Printf.sprintf "%s %s" + (final_regs_to_string fs reg_cond test.arch) + (final_mem_to_string fs mem_cond test.memory) + ) + ) + final_states_set; + (* Print statistics about the condition(s) that we did and didn't want to observe *) + msg (observation_statistics_string observable true final_states test.name); + msg + (observation_statistics_string unobservable false final_states test.name) + ) + ); + List.iter (fun e -> msg (Printf.sprintf "%s[Error]%s %s" Terminal.red Terminal.reset e) @@ -232,12 +353,12 @@ module Make (Arch : Archsem.Arch) = struct in (result, List.rev !msgs) - let run_testrepr model (test : Testrepr.t) = + let run_testrepr print_final_states model (test : Testrepr.t) = let fuel = Config.get_fuel () in let (init, term) = AS.testrepr_to_archstate test in - run_executions model init fuel term test.finals + run_executions print_final_states model init fuel term test - let run_litmus_test ~parse model filename = + let run_litmus_test ~parse print_final_states 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 @@ -247,18 +368,19 @@ module Make (Arch : Archsem.Arch) = struct else try let test = parse filename in - let (result, msgs) = run_testrepr model test in + let (result, msgs) = run_testrepr print_final_states 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; + Printf.printf "\n%s%s%s %s\n" color icon Terminal.reset name; + Printf.printf "Test %s Allowed\n" test.name; + List.iter (fun m -> Printf.printf "%s\n" m) msgs; result with Otoml.Parse_error (pos, msg) -> - Printf.printf " %s✗%s %s %sparse error at %s: %s%s\n" Terminal.red + 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) diff --git a/cli/lib/litmus/testrepr.ml b/cli/lib/litmus/testrepr.ml index 3f7bad64..359778ae 100644 --- a/cli/lib/litmus/testrepr.ml +++ b/cli/lib/litmus/testrepr.ml @@ -108,3 +108,10 @@ 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) + +(* Convert memory address to corresponding symbol. Returns "?" if symbol is None. *) +let mem_addr_to_symbol (addr : int) (mem_blocks : memory_block list) : string = + let mem_block = + List.find (fun (mb : memory_block) -> mb.addr = addr) mem_blocks + in + match mem_block.sym with Some symbol -> symbol | None -> "?" diff --git a/cli/tests/unit/isla/converter_test.ml b/cli/tests/unit/isla/converter_test.ml index 32712860..8e627725 100644 --- a/cli/tests/unit/isla/converter_test.ml +++ b/cli/tests/unit/isla/converter_test.ml @@ -233,7 +233,29 @@ let tests = >:: fun _ -> Test_utils.setup_arm (); let (result, _msgs) = - ArmRunner.run_testrepr Arm.(seq_model tiny_isa) (convert simple_toml) + ArmRunner.run_testrepr true + Arm.(seq_model tiny_isa) + (convert simple_toml) + in + assert_equal Runner.Expected result + ); + ("e2e: SimpleStore seq" + >:: fun _ -> + Test_utils.setup_arm (); + let (result, _msgs) = + ArmRunner.run_testrepr false + Arm.(seq_model tiny_isa) + (convert simple_toml) + in + assert_equal Runner.Expected result + ); + ("e2e: MP ump" + >:: fun _ -> + Test_utils.setup_arm (); + let (result, _msgs) = + ArmRunner.run_testrepr true + Arm.(umProm_model tiny_isa) + (convert mp_toml) in assert_equal Runner.Expected result ); @@ -241,7 +263,9 @@ let tests = >:: fun _ -> Test_utils.setup_arm (); let (result, _msgs) = - ArmRunner.run_testrepr Arm.(umProm_model tiny_isa) (convert mp_toml) + ArmRunner.run_testrepr false + Arm.(umProm_model tiny_isa) + (convert mp_toml) in assert_equal Runner.Expected result ) diff --git a/cli/tests/unit/litmus/testrepr_test.ml b/cli/tests/unit/litmus/testrepr_test.ml index 2f804e43..ec44146d 100644 --- a/cli/tests/unit/litmus/testrepr_test.ml +++ b/cli/tests/unit/litmus/testrepr_test.ml @@ -246,7 +246,14 @@ let archstate_runner_tests = >::: [ ("EOR Expected with seq model" >:: fun _ -> let (result, _msgs) = - ArmRunner.run_testrepr Arm.(seq_model tiny_isa) eor + ArmRunner.run_testrepr true Arm.(seq_model tiny_isa) eor + in + assert_equal Runner.Expected result + ); + ("EOR Expected with seq model" + >:: fun _ -> + let (result, _msgs) = + ArmRunner.run_testrepr false Arm.(seq_model tiny_isa) eor in assert_equal Runner.Expected result ) diff --git a/cli/tests/x86/um/R_PO_MFENCE.archsem.toml b/cli/tests/x86/um/R_PO_MFENCE.archsem.toml index 1629a9a5..b7e4e0c3 100644 --- a/cli/tests/x86/um/R_PO_MFENCE.archsem.toml +++ b/cli/tests/x86/um/R_PO_MFENCE.archsem.toml @@ -1,5 +1,5 @@ arch = "x86" -name = "R_PO_MFENCE" +name = "R+po+mfence" # Read + Program Order + MFENCE litmus test # Thread 0: MOV [ECX], 0x1; MOV [EDX], 0x1 diff --git a/cli/tests/x86/um/R_PO_MFENCE.litmus.toml b/cli/tests/x86/um/R_PO_MFENCE.litmus.toml index 392ceec2..d926b590 100644 --- a/cli/tests/x86/um/R_PO_MFENCE.litmus.toml +++ b/cli/tests/x86/um/R_PO_MFENCE.litmus.toml @@ -1,5 +1,5 @@ arch = "x86" -name = "R_PO_MFENCE" +name = "R+po+mfence" symbolic = ["x", "y"] # MFENCE prevents store-buffer reordering. From 5a1b183fb5ce9ec0f090d37199a24af2333e254e Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 3 Apr 2026 21:18:58 +0100 Subject: [PATCH 02/13] Refactoring --- cli/bin/main.ml | 22 ++++++++++++++-------- cli/lib/litmus/runner.ml | 18 ++++-------------- cli/lib/litmus/testrepr.ml | 7 ------- 3 files changed, 18 insertions(+), 29 deletions(-) diff --git a/cli/bin/main.ml b/cli/bin/main.ml index b37c6296..44081ee7 100644 --- a/cli/bin/main.ml +++ b/cli/bin/main.ml @@ -184,12 +184,18 @@ let format_term = let format_enum = Arg.enum [("archsem", Archsem); ("isla", Isla)] in Arg.(value & opt (some format_enum) None & info ["format"; "f"] ~doc ~docv:"FMT") +let print_final_states_term = + let doc = + "Print all possible final states of relevant registers / memory locations. Output for x86 is compatible with mcompare" + in + Arg.(value & flag & info ["print-final-states"] ~doc) + (** The sequential model command *) -let cmd_seq print_final_states = +let cmd_seq = let run = let+ files = path_and_conf_term and+ fmt = format_term - and+ print_final_states = print_final_states in + and+ print_final_states = print_final_states_term in let parse = parse_testfile fmt in match Config.get_arch () with | Arm -> @@ -212,11 +218,11 @@ let cmd_seq print_final_states = Cmd.v info run (** The user-mode promising command *) -let cmd_ump print_final_states = +let cmd_ump = let run = let+ files = path_and_conf_term and+ fmt = format_term - and+ print_final_states = print_final_states in + and+ print_final_states = print_final_states_term in let parse = parse_testfile fmt in assert (Config.get_arch () = Arch_id.Arm); run_tests "ump" @@ -245,7 +251,7 @@ let bbm_of_config () = --bbm" (** The virtual-memory promising command *) -let cmd_vmp print_final_states = +let cmd_vmp = let open Arm in let bbm_mode = let doc = "Break-before-make mode: off, lax, or strict" in @@ -261,7 +267,7 @@ let cmd_vmp print_final_states = let+ files = path_and_conf_term and+ bbm_param = bbm_mode and+ fmt = format_term - and+ print_final_states = print_final_states in + and+ print_final_states = print_final_states_term in let parse = parse_testfile fmt in assert (Config.get_arch () = Arch_id.Arm); run_tests "vmp" @@ -279,7 +285,7 @@ let cmd_vmp print_final_states = in Cmd.v info run -let cmd_tso print_final_states = +let cmd_tso = let no_eager = let doc = "Disable eager transitions (eager is enabled by default)" in Arg.(value & flag & info ["no-eager"] ~doc) @@ -288,7 +294,7 @@ let cmd_tso print_final_states = let+ files = path_and_conf_term and+ fmt = format_term and+ no_eager = no_eager - and+ print_final_states = print_final_states in + and+ print_final_states = print_final_states_term in let allow_eager = not no_eager in let parse = parse_testfile fmt in assert (Config.get_arch () = Arch_id.X86); diff --git a/cli/lib/litmus/runner.ml b/cli/lib/litmus/runner.ml index ac06da0e..71349ff3 100644 --- a/cli/lib/litmus/runner.ml +++ b/cli/lib/litmus/runner.ml @@ -165,7 +165,6 @@ module Make (Arch : Archsem.Arch) = struct let final_regs_to_string (fs : ArchState.t) (cond : Testrepr.thread_cond list) - (arch : string) : string = String.concat " " (List.concat_map @@ -175,14 +174,7 @@ module Make (Arch : Archsem.Arch) = struct (fun (req_name, _) -> let reg = Reg.of_string req_name in let value = RegMap.geti reg regs in - (* Note that we are making the register name lowercase *) - let reg_name = - if - String.starts_with ~prefix:"x86" (String.lowercase_ascii arch) - then String.lowercase_ascii req_name - else req_name - in - Printf.sprintf "%d:%s=%d;" tid reg_name value + Printf.sprintf "%d:%s=%d;" tid req_name value ) reqs ) @@ -192,15 +184,13 @@ module Make (Arch : Archsem.Arch) = struct let final_mem_to_string (fs : ArchState.t) (mem_conds : Testrepr.mem_cond list) - (mem_blocks : Testrepr.memory_block list) : string = let mem = ArchState.mem fs in String.concat " " (List.map (fun (mc : Testrepr.mem_cond) -> - let mem_symbol = Testrepr.mem_addr_to_symbol mc.addr mem_blocks in let value = MemMap.lookupi mc.addr mc.size mem in - Printf.sprintf "[%s]=%d;" mem_symbol value + Printf.sprintf "[%s]=%d;" mc.sym value ) mem_conds ) @@ -282,8 +272,8 @@ module Make (Arch : Archsem.Arch) = struct (fun fs -> msg (Printf.sprintf "%s %s" - (final_regs_to_string fs reg_cond test.arch) - (final_mem_to_string fs mem_cond test.memory) + (final_regs_to_string fs reg_cond) + (final_mem_to_string fs mem_cond) ) ) final_states_set; diff --git a/cli/lib/litmus/testrepr.ml b/cli/lib/litmus/testrepr.ml index 359778ae..3f7bad64 100644 --- a/cli/lib/litmus/testrepr.ml +++ b/cli/lib/litmus/testrepr.ml @@ -108,10 +108,3 @@ 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) - -(* Convert memory address to corresponding symbol. Returns "?" if symbol is None. *) -let mem_addr_to_symbol (addr : int) (mem_blocks : memory_block list) : string = - let mem_block = - List.find (fun (mb : memory_block) -> mb.addr = addr) mem_blocks - in - match mem_block.sym with Some symbol -> symbol | None -> "?" From 3b21f1c419be00ea794ed2bf3f34449912530396 Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 3 Apr 2026 23:24:08 +0100 Subject: [PATCH 03/13] Display all relevant reg and mem locs, and combine observation count --- cli/lib/litmus/runner.ml | 91 +++++++++++++++++++++++----------------- 1 file changed, 52 insertions(+), 39 deletions(-) diff --git a/cli/lib/litmus/runner.ml b/cli/lib/litmus/runner.ml index 71349ff3..1281620f 100644 --- a/cli/lib/litmus/runner.ml +++ b/cli/lib/litmus/runner.ml @@ -102,12 +102,7 @@ let outcome_freq_to_string yes_freq no_freq = if yes_freq = 0 then "Never" else if no_freq = 0 then "Always" else "Sometimes" (* Return string of format: Observation *) -let test_observation_stats_to_string bool_list test_name = - let (obs_count, not_obs_count) = - List.fold_left - (fun (t, f) b -> if b then (t + 1, f) else (t, f + 1)) - (0, 0) bool_list - in +let test_observation_stats_to_string obs_count not_obs_count test_name = Printf.sprintf "Observation %s %s %d %d" test_name (outcome_freq_to_string obs_count not_obs_count) obs_count not_obs_count @@ -162,23 +157,41 @@ module Make (Arch : Archsem.Arch) = struct ) mem_conds + let get_thread_regname_pairs (reg_cond : Testrepr.thread_cond list) : (int * string) list = + List.concat_map (fun (thread, reg_pair) -> + List.map (fun (name, _) -> (thread, name)) reg_pair + ) reg_cond + + let compare_mem_id (mem_cond_1 : Testrepr.mem_cond) (mem_cond_2 : Testrepr.mem_cond) = + if mem_cond_1.sym = mem_cond_2.sym then 0 + else if mem_cond_1.sym > mem_cond_2.sym then 1 + else -1 + + let get_unique_conds_ignoring_value (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) + : (int * string) list * Testrepr.mem_cond list = + (* Assuming that each (Testrepr.thread_cond list * Testrepr.mem_cond list) already contains unique values *) + List.fold_left + (fun (acc_reg_cond, acc_mem_cond) (reg_cond, mem_cond) -> + let new_reg_cond = get_thread_regname_pairs reg_cond in + (List.sort_uniq compare (acc_reg_cond @ new_reg_cond), + List.sort_uniq compare_mem_id (acc_mem_cond @ mem_cond)) + ) + ([],[]) + conds + let final_regs_to_string (fs : ArchState.t) - (cond : Testrepr.thread_cond list) + (regs : (int * string) list) (* list of (thread, reg_name) pairs *) = String.concat " " - (List.concat_map - (fun (tid, reqs) -> + (List.map + (fun (tid, reg_name) -> let regs = ArchState.reg tid fs in - List.map - (fun (req_name, _) -> - let reg = Reg.of_string req_name in - let value = RegMap.geti reg regs in - Printf.sprintf "%d:%s=%d;" tid req_name value - ) - reqs + let reg = Reg.of_string reg_name in + let value = RegMap.geti reg regs in + Printf.sprintf "%d:%s=%d;" tid reg_name value ) - cond + regs ) let final_mem_to_string @@ -195,6 +208,19 @@ module Make (Arch : Archsem.Arch) = struct mem_conds ) + let get_obs_count + (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) + (state_list : ArchState.t list) = + (List.length state_list) - List.length ( + List.fold_left + (fun unmatched_state_list (cond, mem_cond) -> ( + List.filter + (fun fs -> not (check_outcome fs cond && check_mem_outcome fs mem_cond)) + unmatched_state_list ) + ) + state_list + conds) + (* Print observation statistics. The format is: Ok/No Observation Always/Sometimes/Never <#times_test_cond_observed> <#times_test_cond_not_observed> *) @@ -208,24 +234,9 @@ module Make (Arch : Archsem.Arch) = struct if checking_for_positive then ("Ok", "No (\"allowed\" not found)") else ("No (\"not allowed\" found)", "Ok") in - - String.concat "\n" - (List.map - (fun (cond, mem_cond) -> - let each_obs_ok = - List.map - (fun fs -> check_outcome fs cond && check_mem_outcome fs mem_cond) - state_list - in - let matched = List.exists Fun.id each_obs_ok in - let stats_opening = - if matched then matched_msg else not_matched_msg - in - stats_opening ^ "\n" - ^ test_observation_stats_to_string each_obs_ok test_name - ) - conds - ) + let obs_count = get_obs_count conds state_list in + let msg = if obs_count > 0 then matched_msg else not_matched_msg in + msg ^ "\n" ^ test_observation_stats_to_string obs_count (List.length state_list - obs_count) test_name let run_executions print_final_states model init fuel term test = let msgs = ref [] in @@ -267,7 +278,7 @@ module Make (Arch : Archsem.Arch) = struct (* Print each distinct observable state *) let conds = observable @ unobservable in if conds <> [] then ( - let (reg_cond, mem_cond) = List.hd (observable @ unobservable) in + let (reg_cond, mem_cond) = get_unique_conds_ignoring_value conds in ArchStateSet.iter (fun fs -> msg @@ -278,9 +289,11 @@ module Make (Arch : Archsem.Arch) = struct ) final_states_set; (* Print statistics about the condition(s) that we did and didn't want to observe *) - msg (observation_statistics_string observable true final_states test.name); - msg - (observation_statistics_string unobservable false final_states test.name) + if observable <> [] then + msg (observation_statistics_string observable true final_states test.name) + else if unobservable <> [] then + msg (observation_statistics_string unobservable false final_states test.name) + else msg "ERROR: no conditions to observe" ) ); From 1e12b4056fbda910c6be324c85b5c0b4908052d8 Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 3 Apr 2026 23:24:43 +0100 Subject: [PATCH 04/13] Fix formatting --- cli/bin/main.ml | 3 +- cli/lib/litmus/runner.ml | 79 ++++++++++++++++++++++++---------------- 2 files changed, 50 insertions(+), 32 deletions(-) diff --git a/cli/bin/main.ml b/cli/bin/main.ml index 44081ee7..18869fe5 100644 --- a/cli/bin/main.ml +++ b/cli/bin/main.ml @@ -186,7 +186,8 @@ let format_term = let print_final_states_term = let doc = - "Print all possible final states of relevant registers / memory locations. Output for x86 is compatible with mcompare" + "Print all possible final states of relevant registers / memory locations. \ + Output for x86 is compatible with mcompare" in Arg.(value & flag & info ["print-final-states"] ~doc) diff --git a/cli/lib/litmus/runner.ml b/cli/lib/litmus/runner.ml index 1281620f..63997ed0 100644 --- a/cli/lib/litmus/runner.ml +++ b/cli/lib/litmus/runner.ml @@ -157,27 +157,36 @@ module Make (Arch : Archsem.Arch) = struct ) mem_conds - let get_thread_regname_pairs (reg_cond : Testrepr.thread_cond list) : (int * string) list = - List.concat_map (fun (thread, reg_pair) -> - List.map (fun (name, _) -> (thread, name)) reg_pair - ) reg_cond + let get_thread_regname_pairs (reg_cond : Testrepr.thread_cond list) : + (int * string) list + = + List.concat_map + (fun (thread, reg_pair) -> + List.map (fun (name, _) -> (thread, name)) reg_pair + ) + reg_cond - let compare_mem_id (mem_cond_1 : Testrepr.mem_cond) (mem_cond_2 : Testrepr.mem_cond) = + let compare_mem_id + (mem_cond_1 : Testrepr.mem_cond) + (mem_cond_2 : Testrepr.mem_cond) + = if mem_cond_1.sym = mem_cond_2.sym then 0 else if mem_cond_1.sym > mem_cond_2.sym then 1 else -1 - let get_unique_conds_ignoring_value (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) - : (int * string) list * Testrepr.mem_cond list = + let get_unique_conds_ignoring_value + (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) : + (int * string) list * Testrepr.mem_cond list + = (* Assuming that each (Testrepr.thread_cond list * Testrepr.mem_cond list) already contains unique values *) List.fold_left - (fun (acc_reg_cond, acc_mem_cond) (reg_cond, mem_cond) -> - let new_reg_cond = get_thread_regname_pairs reg_cond in - (List.sort_uniq compare (acc_reg_cond @ new_reg_cond), - List.sort_uniq compare_mem_id (acc_mem_cond @ mem_cond)) - ) - ([],[]) - conds + (fun (acc_reg_cond, acc_mem_cond) (reg_cond, mem_cond) -> + let new_reg_cond = get_thread_regname_pairs reg_cond in + ( List.sort_uniq compare (acc_reg_cond @ new_reg_cond), + List.sort_uniq compare_mem_id (acc_mem_cond @ mem_cond) + ) + ) + ([], []) conds let final_regs_to_string (fs : ArchState.t) @@ -194,10 +203,7 @@ module Make (Arch : Archsem.Arch) = struct regs ) - let final_mem_to_string - (fs : ArchState.t) - (mem_conds : Testrepr.mem_cond list) - = + let final_mem_to_string (fs : ArchState.t) (mem_conds : Testrepr.mem_cond list) = let mem = ArchState.mem fs in String.concat " " (List.map @@ -210,16 +216,20 @@ module Make (Arch : Archsem.Arch) = struct let get_obs_count (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) - (state_list : ArchState.t list) = - (List.length state_list) - List.length ( - List.fold_left - (fun unmatched_state_list (cond, mem_cond) -> ( - List.filter - (fun fs -> not (check_outcome fs cond && check_mem_outcome fs mem_cond)) - unmatched_state_list ) - ) - state_list - conds) + (state_list : ArchState.t list) + = + List.length state_list + - List.length + (List.fold_left + (fun unmatched_state_list (cond, mem_cond) -> + List.filter + (fun fs -> + not (check_outcome fs cond && check_mem_outcome fs mem_cond) + ) + unmatched_state_list + ) + state_list conds + ) (* Print observation statistics. The format is: Ok/No @@ -236,7 +246,10 @@ module Make (Arch : Archsem.Arch) = struct in let obs_count = get_obs_count conds state_list in let msg = if obs_count > 0 then matched_msg else not_matched_msg in - msg ^ "\n" ^ test_observation_stats_to_string obs_count (List.length state_list - obs_count) test_name + msg ^ "\n" + ^ test_observation_stats_to_string obs_count + (List.length state_list - obs_count) + test_name let run_executions print_final_states model init fuel term test = let msgs = ref [] in @@ -290,9 +303,13 @@ module Make (Arch : Archsem.Arch) = struct final_states_set; (* Print statistics about the condition(s) that we did and didn't want to observe *) if observable <> [] then - msg (observation_statistics_string observable true final_states test.name) + msg + (observation_statistics_string observable true final_states test.name) else if unobservable <> [] then - msg (observation_statistics_string unobservable false final_states test.name) + msg + (observation_statistics_string unobservable false final_states + test.name + ) else msg "ERROR: no conditions to observe" ) ); From bc675295ed528b2ed0e4c8379023c364d90b3e71 Mon Sep 17 00:00:00 2001 From: s-prism Date: Wed, 8 Apr 2026 17:03:39 +0100 Subject: [PATCH 05/13] Deduplicate final states manually --- cli/lib/litmus/minState.ml | 108 +++++++++++++++++++++++++++++++++++++ cli/lib/litmus/runner.ml | 87 +++++------------------------- 2 files changed, 122 insertions(+), 73 deletions(-) create mode 100644 cli/lib/litmus/minState.ml diff --git a/cli/lib/litmus/minState.ml b/cli/lib/litmus/minState.ml new file mode 100644 index 00000000..01d5a692 --- /dev/null +++ b/cli/lib/litmus/minState.ml @@ -0,0 +1,108 @@ +type reg_state = + { tid : int; + regname : string; + value : int + } + +type mem_state = + { sym : string; + addr : int; + size : int; + value : int + } + +module Make (Arch : Archsem.Arch) = struct + open Arch + + let get_thread_regname_pairs (reg_cond : Testrepr.thread_cond list) : + (int * string) list + = + List.concat_map + (fun (thread, reg_pair) -> + List.map (fun (name, _) -> (thread, name)) reg_pair + ) + reg_cond + + let compare_mem_id + (mem_cond_1 : Testrepr.mem_cond) + (mem_cond_2 : Testrepr.mem_cond) + = + String.compare mem_cond_1.sym mem_cond_2.sym + + let get_unique_conds_ignoring_value + (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) : + (int * string) list * Testrepr.mem_cond list + = + (* Assuming that each (Testrepr.thread_cond list * Testrepr.mem_cond list) already contains unique values *) + List.fold_left + (fun (acc_reg_cond, acc_mem_cond) (reg_cond, mem_cond) -> + let new_reg_cond = get_thread_regname_pairs reg_cond in + ( List.sort_uniq compare (acc_reg_cond @ new_reg_cond), + List.sort_uniq compare_mem_id (acc_mem_cond @ mem_cond) + ) + ) + ([], []) conds + + let minimise_reg_state (reg_conds : (int * string) list) (state : ArchState.t) : + reg_state list + = + List.map + (fun (tid, regname) -> + let regs = ArchState.reg tid state in + let value = RegMap.geti (Reg.of_string regname) regs in + {tid; regname; value} + ) + reg_conds + + let minimise_mem_state (mem_conds : Testrepr.mem_cond list) (state : ArchState.t) + : mem_state list + = + let mem = ArchState.mem state in + List.map + (fun (mc : Testrepr.mem_cond) -> + match MemMap.lookupi_opt mc.addr mc.size mem with + | None -> + failwith + (Printf.sprintf "[[outcome]] memory not found at 0x%x" mc.addr) + | Some mv -> {sym = mc.sym; addr = mc.addr; size = mc.size; value = mv} + ) + mem_conds + + let minimise_states + ((reg_conds, mem_conds) : (int * string) list * Testrepr.mem_cond list) + (states : ArchState.t list) : (reg_state list * mem_state list) list + = + List.map + (fun state -> + (minimise_reg_state reg_conds state, minimise_mem_state mem_conds state) + ) + states + + let compare_minimised_states + ((regs1, mems1) : reg_state list * mem_state list) + ((regs2, mems2) : reg_state list * mem_state list) : int + = + let c = + List.compare + (fun (r1 : reg_state) (r2 : reg_state) -> Int.compare r1.value r2.value) + regs1 regs2 + in + if c <> 0 then c + else List.compare (fun m1 m2 -> Int.compare m1.value m2.value) mems1 mems2 + + let final_regs_to_string (rs : reg_state list) = + String.concat " " + (List.map + (fun (r : reg_state) -> + Printf.sprintf "%d:%s=%d;" r.tid r.regname r.value + ) + rs + ) + + let final_mem_to_string (ms : mem_state list) = + String.concat " " + (List.map + (fun (m : mem_state) -> Printf.sprintf "[%s]=%d;" m.sym m.value) + ms + ) +end diff --git a/cli/lib/litmus/runner.ml b/cli/lib/litmus/runner.ml index 63997ed0..2d19dc5f 100644 --- a/cli/lib/litmus/runner.ml +++ b/cli/lib/litmus/runner.ml @@ -110,13 +110,7 @@ let test_observation_stats_to_string obs_count not_obs_count test_name = module Make (Arch : Archsem.Arch) = struct open Arch module AS = ToArchState.Make (Arch) - - (* Allow conversion of an iterable structure of ArchStates into a set*) - module ArchStateSet = Set.Make (struct - type t = Arch.ArchState.t - - let compare = Stdlib.compare - end) + module MinimiseState = MinState.Make (Arch) let check_outcome (fs : ArchState.t) (cond : Testrepr.thread_cond list) : bool = List.for_all @@ -157,63 +151,6 @@ module Make (Arch : Archsem.Arch) = struct ) mem_conds - let get_thread_regname_pairs (reg_cond : Testrepr.thread_cond list) : - (int * string) list - = - List.concat_map - (fun (thread, reg_pair) -> - List.map (fun (name, _) -> (thread, name)) reg_pair - ) - reg_cond - - let compare_mem_id - (mem_cond_1 : Testrepr.mem_cond) - (mem_cond_2 : Testrepr.mem_cond) - = - if mem_cond_1.sym = mem_cond_2.sym then 0 - else if mem_cond_1.sym > mem_cond_2.sym then 1 - else -1 - - let get_unique_conds_ignoring_value - (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) : - (int * string) list * Testrepr.mem_cond list - = - (* Assuming that each (Testrepr.thread_cond list * Testrepr.mem_cond list) already contains unique values *) - List.fold_left - (fun (acc_reg_cond, acc_mem_cond) (reg_cond, mem_cond) -> - let new_reg_cond = get_thread_regname_pairs reg_cond in - ( List.sort_uniq compare (acc_reg_cond @ new_reg_cond), - List.sort_uniq compare_mem_id (acc_mem_cond @ mem_cond) - ) - ) - ([], []) conds - - let final_regs_to_string - (fs : ArchState.t) - (regs : (int * string) list) (* list of (thread, reg_name) pairs *) - = - String.concat " " - (List.map - (fun (tid, reg_name) -> - let regs = ArchState.reg tid fs in - let reg = Reg.of_string reg_name in - let value = RegMap.geti reg regs in - Printf.sprintf "%d:%s=%d;" tid reg_name value - ) - regs - ) - - let final_mem_to_string (fs : ArchState.t) (mem_conds : Testrepr.mem_cond list) = - let mem = ArchState.mem fs in - String.concat " " - (List.map - (fun (mc : Testrepr.mem_cond) -> - let value = MemMap.lookupi mc.addr mc.size mem in - Printf.sprintf "[%s]=%d;" mc.sym value - ) - mem_conds - ) - let get_obs_count (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) (state_list : ArchState.t list) @@ -285,22 +222,26 @@ module Make (Arch : Archsem.Arch) = struct (* If the print-final-states flag is set, print all observable states and statistics *) if print_final_states then ( - let final_states_set = ArchStateSet.of_list final_states in + let conds = observable @ unobservable in + let unique_cond = MinimiseState.get_unique_conds_ignoring_value conds in + let minimised_fs = MinimiseState.minimise_states unique_cond final_states in + let unique_minimised_fs = + List.sort_uniq MinimiseState.compare_minimised_states minimised_fs + in + (* Print number of distinct observed states *) - msg (Printf.sprintf "States %d" (ArchStateSet.cardinal final_states_set)); + msg (Printf.sprintf "States %d" (List.length unique_minimised_fs)); (* Print each distinct observable state *) - let conds = observable @ unobservable in if conds <> [] then ( - let (reg_cond, mem_cond) = get_unique_conds_ignoring_value conds in - ArchStateSet.iter - (fun fs -> + List.iter + (fun (regs_state, mems_state) -> msg (Printf.sprintf "%s %s" - (final_regs_to_string fs reg_cond) - (final_mem_to_string fs mem_cond) + (MinimiseState.final_regs_to_string regs_state) + (MinimiseState.final_mem_to_string mems_state) ) ) - final_states_set; + unique_minimised_fs; (* Print statistics about the condition(s) that we did and didn't want to observe *) if observable <> [] then msg From 1a442e4e59159d7d53d921cad9a5898fcba67234 Mon Sep 17 00:00:00 2001 From: s-prism Date: Wed, 8 Apr 2026 17:15:38 +0100 Subject: [PATCH 06/13] Change R+po+mfence test name back --- cli/tests/x86/um/R_PO_MFENCE.archsem.toml | 2 +- cli/tests/x86/um/R_PO_MFENCE.litmus.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/cli/tests/x86/um/R_PO_MFENCE.archsem.toml b/cli/tests/x86/um/R_PO_MFENCE.archsem.toml index b7e4e0c3..1629a9a5 100644 --- a/cli/tests/x86/um/R_PO_MFENCE.archsem.toml +++ b/cli/tests/x86/um/R_PO_MFENCE.archsem.toml @@ -1,5 +1,5 @@ arch = "x86" -name = "R+po+mfence" +name = "R_PO_MFENCE" # Read + Program Order + MFENCE litmus test # Thread 0: MOV [ECX], 0x1; MOV [EDX], 0x1 diff --git a/cli/tests/x86/um/R_PO_MFENCE.litmus.toml b/cli/tests/x86/um/R_PO_MFENCE.litmus.toml index d926b590..392ceec2 100644 --- a/cli/tests/x86/um/R_PO_MFENCE.litmus.toml +++ b/cli/tests/x86/um/R_PO_MFENCE.litmus.toml @@ -1,5 +1,5 @@ arch = "x86" -name = "R+po+mfence" +name = "R_PO_MFENCE" symbolic = ["x", "y"] # MFENCE prevents store-buffer reordering. From fb5426316efc79fe7db24d9395345c036c13a3db Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 10 Apr 2026 01:10:49 +0100 Subject: [PATCH 07/13] Refactoring --- cli/bin/main.ml | 10 +- cli/lib/litmus/mcompare.ml | 138 ++++++++++++++++++ cli/lib/litmus/minState.ml | 96 +++++++----- cli/lib/litmus/runner.ml | 193 +++++++++++-------------- cli/tests/converter/gen/gen.ml | 39 +++++ cli/tests/unit/isla/converter_test.ml | 8 +- cli/tests/unit/litmus/testrepr_test.ml | 22 +-- 7 files changed, 329 insertions(+), 177 deletions(-) create mode 100644 cli/lib/litmus/mcompare.ml diff --git a/cli/bin/main.ml b/cli/bin/main.ml index 18869fe5..75472ec1 100644 --- a/cli/bin/main.ml +++ b/cli/bin/main.ml @@ -201,13 +201,13 @@ let cmd_seq = match Config.get_arch () with | Arm -> run_tests "arm-seq" - (ArmRunner.run_litmus_test ~parse print_final_states + (ArmRunner.run_litmus_test ~parse ~print_final_states Arm.(seq_model tiny_isa) ) files | X86 -> run_tests "x86-seq" - (X86Runner.run_litmus_test ~parse print_final_states + (X86Runner.run_litmus_test ~parse ~print_final_states X86.(seq_model tiny_isa) ) files @@ -227,7 +227,7 @@ let cmd_ump = let parse = parse_testfile fmt in assert (Config.get_arch () = Arch_id.Arm); run_tests "ump" - (ArmRunner.run_litmus_test ~parse print_final_states + (ArmRunner.run_litmus_test ~parse ~print_final_states Arm.(umProm_model tiny_isa) ) files @@ -272,7 +272,7 @@ let cmd_vmp = let parse = parse_testfile fmt in assert (Config.get_arch () = Arch_id.Arm); run_tests "vmp" - (ArmRunner.run_litmus_test ~parse print_final_states + (ArmRunner.run_litmus_test ~parse ~print_final_states (vmProm_model ~bbm_param tiny_isa) ) files @@ -300,7 +300,7 @@ let cmd_tso = let parse = parse_testfile fmt in assert (Config.get_arch () = Arch_id.X86); run_tests "tso" - (X86Runner.run_litmus_test ~parse print_final_states + (X86Runner.run_litmus_test ~parse ~print_final_states X86.(op_model ~allow_eager tiny_isa) ) files diff --git a/cli/lib/litmus/mcompare.ml b/cli/lib/litmus/mcompare.ml new file mode 100644 index 00000000..710a1850 --- /dev/null +++ b/cli/lib/litmus/mcompare.ml @@ -0,0 +1,138 @@ +(******************************************************************************) +(* ArchSem *) +(* *) +(* Copyright (c) 2021 *) +(* Thibaut Pérami, University of Cambridge *) +(* Yeji Han, Seoul National University *) +(* Zongyuan Liu, Aarhus University *) +(* Nils Lauermann, University of Cambridge *) +(* Jean Pichon-Pharabod, University of Cambridge, Aarhus University *) +(* Brian Campbell, University of Edinburgh *) +(* Alasdair Armstrong, University of Cambridge *) +(* Ben Simner, University of Cambridge *) +(* Peter Sewell, University of Cambridge *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *) +(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *) +(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *) +(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *) +(* COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *) +(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *) +(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS *) +(* OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR *) +(* TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE *) +(* USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* *) +(******************************************************************************) + +(** Functions for displaying mcompare-compatible output *) + +(* Convert a list of register state to string format, + suitable for printing final register states for mcompare *) +let final_regs_to_string (rs : MinState.reg_state list) = + String.concat " " + (List.map + (fun (r : MinState.reg_state) -> + Printf.sprintf "%d:%s=%d;" r.tid r.regname r.value + ) + rs + ) + +(* Convert a list of memory state to string format, + suitable for printing final memory states for mcompare *) +let final_mem_to_string (ms : MinState.mem_state list) = + String.concat " " + (List.map + (fun (m : MinState.mem_state) -> Printf.sprintf "[%s]=%d;" m.sym m.value) + ms + ) + +(* Print how often an outcome occurs, part of the required Mcompare output *) +let outcome_freq_to_string yes_freq no_freq = + if yes_freq = 0 then "Never" else if no_freq = 0 then "Always" else "Sometimes" + +(* Return string of format: Observation . + which is required for Mcompare output*) +let test_observation_stats_to_string obs_count not_obs_count test_name = + Printf.sprintf "Observation %s %s %d %d" test_name + (outcome_freq_to_string obs_count not_obs_count) + obs_count not_obs_count + +module Make (Arch : Archsem.Arch) = struct + open Arch + module MinimiseState = MinState.Make (Arch) + + (* Print observation statistics for Mcompare. The format is: + Ok/No + Observation Always/Sometimes/Never <#observed> <#not_observed> *) + let observation_statistics_string + (obs_count : int) + (checking_for_positive : bool) + (state_list : ArchState.t list) + (test_name : string) : string + = + let (matched_msg, not_matched_msg) = + if checking_for_positive then ("Ok", "No (\"allowed\" not found)") + else ("No (\"not allowed\" found)", "Ok") + in + let msg = if obs_count > 0 then matched_msg else not_matched_msg in + msg ^ "\n" + ^ test_observation_stats_to_string obs_count + (List.length state_list - obs_count) + test_name + + (* Top-level function to call for mcompare-compatible output *) + let print_final_states + (observable : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) + (unobservable : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) + (obs_count : int) + (unobs_count : int) + (final_states : ArchState.t list) + (test_name : string) : string + = + let conds = observable @ unobservable in + let unique_cond = MinimiseState.get_unique_conds_ignoring_value conds in + let minimised_fs = MinimiseState.minimise_states unique_cond final_states in + let unique_minimised_fs = List.sort_uniq compare minimised_fs in + + (* Print number of distinct observed states *) + let states_count_part = + Printf.sprintf "States %d\n" (List.length unique_minimised_fs) + in + (* Print each distinct observable state *) + let state_list_part = + if conds <> [] then + List.map + (fun (regs_state, mems_state) -> + Printf.sprintf "%s %s\n" + (final_regs_to_string regs_state) + (final_mem_to_string mems_state) + ) + unique_minimised_fs + |> String.concat "" + else "" + in + let observation_part = + if + (* Print statistics about the condition(s) that we did and didn't want to observe *) + observable <> [] + then observation_statistics_string obs_count true final_states test_name + else if unobservable <> [] then + observation_statistics_string unobs_count false final_states test_name + else "ERROR: no conditions to observe" + in + + states_count_part ^ state_list_part ^ observation_part +end diff --git a/cli/lib/litmus/minState.ml b/cli/lib/litmus/minState.ml index 01d5a692..aebfb26f 100644 --- a/cli/lib/litmus/minState.ml +++ b/cli/lib/litmus/minState.ml @@ -1,3 +1,45 @@ +(******************************************************************************) +(* ArchSem *) +(* *) +(* Copyright (c) 2021 *) +(* Thibaut Pérami, University of Cambridge *) +(* Yeji Han, Seoul National University *) +(* Zongyuan Liu, Aarhus University *) +(* Nils Lauermann, University of Cambridge *) +(* Jean Pichon-Pharabod, University of Cambridge, Aarhus University *) +(* Brian Campbell, University of Edinburgh *) +(* Alasdair Armstrong, University of Cambridge *) +(* Ben Simner, University of Cambridge *) +(* Peter Sewell, University of Cambridge *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *) +(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *) +(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *) +(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *) +(* COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *) +(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *) +(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS *) +(* OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR *) +(* TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE *) +(* USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* *) +(******************************************************************************) + +(** Convert an ArchState.t into a (reg_state list * mem_state list), and related functions +*) + type reg_state = { tid : int; regname : string; @@ -14,6 +56,8 @@ type mem_state = module Make (Arch : Archsem.Arch) = struct open Arch + (* Convert a collection of register conditions (each having a thread id and a register name) + into a list of thread-regname pairs *) let get_thread_regname_pairs (reg_cond : Testrepr.thread_cond list) : (int * string) list = @@ -23,26 +67,26 @@ module Make (Arch : Archsem.Arch) = struct ) reg_cond - let compare_mem_id + (* Compare the memory symbol of 2 memory conditions *) + let compare_mem_sym (mem_cond_1 : Testrepr.mem_cond) (mem_cond_2 : Testrepr.mem_cond) = String.compare mem_cond_1.sym mem_cond_2.sym + (* From the test conditions, get a list of all unique thread-register pairs, + and a list of all unique memory symbols *) let get_unique_conds_ignoring_value (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) : (int * string) list * Testrepr.mem_cond list = - (* Assuming that each (Testrepr.thread_cond list * Testrepr.mem_cond list) already contains unique values *) - List.fold_left - (fun (acc_reg_cond, acc_mem_cond) (reg_cond, mem_cond) -> - let new_reg_cond = get_thread_regname_pairs reg_cond in - ( List.sort_uniq compare (acc_reg_cond @ new_reg_cond), - List.sort_uniq compare_mem_id (acc_mem_cond @ mem_cond) - ) - ) - ([], []) conds + let (reg_conds, mem_conds) = List.split conds in + let all_reg_conds = get_thread_regname_pairs (List.flatten reg_conds) in + ( List.sort_uniq compare all_reg_conds, + List.sort_uniq compare_mem_sym (List.flatten mem_conds) + ) + (* From a final state, extract the registers (and values) that the register conditions check *) let minimise_reg_state (reg_conds : (int * string) list) (state : ArchState.t) : reg_state list = @@ -54,6 +98,7 @@ module Make (Arch : Archsem.Arch) = struct ) reg_conds + (* From a final state, extract the memory locations (and values) that the memory conditions check *) let minimise_mem_state (mem_conds : Testrepr.mem_cond list) (state : ArchState.t) : mem_state list = @@ -68,6 +113,9 @@ module Make (Arch : Archsem.Arch) = struct ) mem_conds + (* For a list of final states, for each final state, + extract the registers and memory location that the conditions check + (with the final values of these locations) *) let minimise_states ((reg_conds, mem_conds) : (int * string) list * Testrepr.mem_cond list) (states : ArchState.t list) : (reg_state list * mem_state list) list @@ -77,32 +125,4 @@ module Make (Arch : Archsem.Arch) = struct (minimise_reg_state reg_conds state, minimise_mem_state mem_conds state) ) states - - let compare_minimised_states - ((regs1, mems1) : reg_state list * mem_state list) - ((regs2, mems2) : reg_state list * mem_state list) : int - = - let c = - List.compare - (fun (r1 : reg_state) (r2 : reg_state) -> Int.compare r1.value r2.value) - regs1 regs2 - in - if c <> 0 then c - else List.compare (fun m1 m2 -> Int.compare m1.value m2.value) mems1 mems2 - - let final_regs_to_string (rs : reg_state list) = - String.concat " " - (List.map - (fun (r : reg_state) -> - Printf.sprintf "%d:%s=%d;" r.tid r.regname r.value - ) - rs - ) - - let final_mem_to_string (ms : mem_state list) = - String.concat " " - (List.map - (fun (m : mem_state) -> Printf.sprintf "[%s]=%d;" m.sym m.value) - ms - ) end diff --git a/cli/lib/litmus/runner.ml b/cli/lib/litmus/runner.ml index 2d19dc5f..6ef60550 100644 --- a/cli/lib/litmus/runner.ml +++ b/cli/lib/litmus/runner.ml @@ -98,19 +98,18 @@ let result_to_string = function | NoBehaviour -> Terminal.red ^ "NO BEHAVIOUR" ^ Terminal.reset | ParseError -> Terminal.red ^ "PARSE ERROR" ^ Terminal.reset -let outcome_freq_to_string yes_freq no_freq = - if yes_freq = 0 then "Never" else if no_freq = 0 then "Always" else "Sometimes" - -(* Return string of format: Observation *) -let test_observation_stats_to_string obs_count not_obs_count test_name = - Printf.sprintf "Observation %s %s %d %d" test_name - (outcome_freq_to_string obs_count not_obs_count) - obs_count not_obs_count +let find_index p lst = + let rec aux i = function + | [] -> None + | x :: tl -> if p x then Some i else aux (i + 1) tl + in + aux 0 lst module Make (Arch : Archsem.Arch) = struct open Arch module AS = ToArchState.Make (Arch) module MinimiseState = MinState.Make (Arch) + module McompareInst = Mcompare.Make (Arch) let check_outcome (fs : ArchState.t) (cond : Testrepr.thread_cond list) : bool = List.for_all @@ -151,44 +150,7 @@ module Make (Arch : Archsem.Arch) = struct ) mem_conds - let get_obs_count - (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) - (state_list : ArchState.t list) - = - List.length state_list - - List.length - (List.fold_left - (fun unmatched_state_list (cond, mem_cond) -> - List.filter - (fun fs -> - not (check_outcome fs cond && check_mem_outcome fs mem_cond) - ) - unmatched_state_list - ) - state_list conds - ) - - (* Print observation statistics. The format is: - Ok/No - Observation Always/Sometimes/Never <#times_test_cond_observed> <#times_test_cond_not_observed> *) - let observation_statistics_string - (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) - (checking_for_positive : bool) - (state_list : ArchState.t list) - (test_name : string) : string - = - let (matched_msg, not_matched_msg) = - if checking_for_positive then ("Ok", "No (\"allowed\" not found)") - else ("No (\"not allowed\" found)", "Ok") - in - let obs_count = get_obs_count conds state_list in - let msg = if obs_count > 0 then matched_msg else not_matched_msg in - msg ^ "\n" - ^ test_observation_stats_to_string obs_count - (List.length state_list - obs_count) - test_name - - let run_executions print_final_states model init fuel term test = + let run_executions ~print_final_states model init fuel term test = let msgs = ref [] in let msg s = msgs := s :: !msgs in let results = model fuel term init in @@ -220,40 +182,56 @@ module Make (Arch : Archsem.Arch) = struct results in - (* If the print-final-states flag is set, print all observable states and statistics *) - if print_final_states then ( - let conds = observable @ unobservable in - let unique_cond = MinimiseState.get_unique_conds_ignoring_value conds in - let minimised_fs = MinimiseState.minimise_states unique_cond final_states in - let unique_minimised_fs = - List.sort_uniq MinimiseState.compare_minimised_states minimised_fs + (* For each condition in observed, get a list of bool representing which final states satisfy the condition *) + let observable_matrix = + List.map + (fun (cond, mem_cond) -> + List.map + (fun fs -> check_outcome fs cond && check_mem_outcome fs mem_cond) + final_states + ) + observable + in + (* For each condition in unobserved, get a list of bool representing which final states satisfy the condition *) + let unobservable_matrix = + List.map + (fun (cond, mem_cond) -> + List.map + (fun fs -> check_outcome fs cond && check_mem_outcome fs mem_cond) + final_states + ) + unobservable + in + + (* Get the number of states which satisfy at least one condition in observable *) + let observable_count = + let state_satisfied_list = + match observable_matrix with + | [] -> [] + | h :: t -> List.fold_left (List.map2 ( || )) h t + in + List.fold_left + (fun acc x -> if x then acc + 1 else acc) + 0 state_satisfied_list + in + (* Get the number of states which satisfy at least one condition in unobservable *) + let unobservable_count = + let state_satisfied_list = + match unobservable_matrix with + | [] -> [] + | h :: t -> List.fold_left (List.map2 ( || )) h t in + List.fold_left + (fun acc x -> if x then acc + 1 else acc) + 0 state_satisfied_list + in - (* Print number of distinct observed states *) - msg (Printf.sprintf "States %d" (List.length unique_minimised_fs)); - (* Print each distinct observable state *) - if conds <> [] then ( - List.iter - (fun (regs_state, mems_state) -> - msg - (Printf.sprintf "%s %s" - (MinimiseState.final_regs_to_string regs_state) - (MinimiseState.final_mem_to_string mems_state) - ) - ) - unique_minimised_fs; - (* Print statistics about the condition(s) that we did and didn't want to observe *) - if observable <> [] then - msg - (observation_statistics_string observable true final_states test.name) - else if unobservable <> [] then - msg - (observation_statistics_string unobservable false final_states - test.name - ) - else msg "ERROR: no conditions to observe" - ) - ); + (* If the print-final-states flag is set, print all observable states and statistics *) + if print_final_states then + msg + (McompareInst.print_final_states observable unobservable observable_count + unobservable_count final_states test.name + ); List.iter (fun e -> @@ -263,46 +241,43 @@ module Make (Arch : Archsem.Arch) = struct if flags <> [] then msg "Flagged"; let observable_ok = - List.for_all - (fun (cond, mem_cond) -> - let matched = - List.exists - (fun fs -> check_outcome fs cond && check_mem_outcome fs mem_cond) - final_states - in - if (not matched) && final_states <> [] then - msg - (Printf.sprintf "%sObservable not found%s: %s %s" Terminal.red - Terminal.reset (cond_to_string cond) - (mem_cond_to_string mem_cond) - ); - matched - ) - observable + List.for_all Fun.id + (List.mapi + (fun i matched_list -> + let matched = List.exists Fun.id matched_list in + ( if (not matched) && final_states <> [] then + let (cond, mem_cond) = List.nth observable i in + msg + (Printf.sprintf "%sObservable not found%s: %s %s" Terminal.red + Terminal.reset (cond_to_string cond) + (mem_cond_to_string mem_cond) + ) + ); + matched + ) + observable_matrix + ) in let unobservable_ok = List.for_all Fun.id (List.mapi - (fun i fs -> - match - List.find_opt - (fun (cond, mem_cond) -> - check_outcome fs cond && check_mem_outcome fs mem_cond - ) - unobservable - with - | Some (cond, mem_cond) -> + (fun i matched_list -> + let opt_index = find_index Fun.id matched_list in + match opt_index with + | Some index -> + let (cond, mem_cond) = List.nth unobservable i in msg (Printf.sprintf "%sUnobservable found%s in execution %d: %s %s" - Terminal.red Terminal.reset (i + 1) (cond_to_string cond) + Terminal.red Terminal.reset (index + 1) + (cond_to_string cond) (mem_cond_to_string mem_cond) ); false | None -> true ) - final_states + unobservable_matrix ) in @@ -314,12 +289,12 @@ module Make (Arch : Archsem.Arch) = struct in (result, List.rev !msgs) - let run_testrepr print_final_states model (test : Testrepr.t) = + let run_testrepr ~print_final_states model (test : Testrepr.t) = let fuel = Config.get_fuel () in let (init, term) = AS.testrepr_to_archstate test in - run_executions print_final_states model init fuel term test + run_executions ~print_final_states model init fuel term test - let run_litmus_test ~parse print_final_states model filename = + let run_litmus_test ~parse ~print_final_states 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 @@ -329,7 +304,7 @@ module Make (Arch : Archsem.Arch) = struct else try let test = parse filename in - let (result, msgs) = run_testrepr print_final_states model test in + let (result, msgs) = run_testrepr ~print_final_states model test in let (icon, color) = match result with | Expected -> (Terminal.check, Terminal.green) diff --git a/cli/tests/converter/gen/gen.ml b/cli/tests/converter/gen/gen.ml index 93707c8e..ac2e5db3 100644 --- a/cli/tests/converter/gen/gen.ml +++ b/cli/tests/converter/gen/gen.ml @@ -1,3 +1,42 @@ +(******************************************************************************) +(* ArchSem *) +(* *) +(* Copyright (c) 2021 *) +(* Thibaut Pérami, University of Cambridge *) +(* Yeji Han, Seoul National University *) +(* Zongyuan Liu, Aarhus University *) +(* Nils Lauermann, University of Cambridge *) +(* Jean Pichon-Pharabod, University of Cambridge, Aarhus University *) +(* Brian Campbell, University of Edinburgh *) +(* Alasdair Armstrong, University of Cambridge *) +(* Ben Simner, University of Cambridge *) +(* Peter Sewell, University of Cambridge *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *) +(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *) +(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *) +(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *) +(* COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *) +(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *) +(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS *) +(* OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR *) +(* TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE *) +(* USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* *) +(******************************************************************************) + (** This file actually runs in the converter directory (parent) but the generated rules run in the expect directory*) diff --git a/cli/tests/unit/isla/converter_test.ml b/cli/tests/unit/isla/converter_test.ml index 8e627725..77e0fdb6 100644 --- a/cli/tests/unit/isla/converter_test.ml +++ b/cli/tests/unit/isla/converter_test.ml @@ -233,7 +233,7 @@ let tests = >:: fun _ -> Test_utils.setup_arm (); let (result, _msgs) = - ArmRunner.run_testrepr true + ArmRunner.run_testrepr ~print_final_states:true Arm.(seq_model tiny_isa) (convert simple_toml) in @@ -243,7 +243,7 @@ let tests = >:: fun _ -> Test_utils.setup_arm (); let (result, _msgs) = - ArmRunner.run_testrepr false + ArmRunner.run_testrepr ~print_final_states:false Arm.(seq_model tiny_isa) (convert simple_toml) in @@ -253,7 +253,7 @@ let tests = >:: fun _ -> Test_utils.setup_arm (); let (result, _msgs) = - ArmRunner.run_testrepr true + ArmRunner.run_testrepr ~print_final_states:true Arm.(umProm_model tiny_isa) (convert mp_toml) in @@ -263,7 +263,7 @@ let tests = >:: fun _ -> Test_utils.setup_arm (); let (result, _msgs) = - ArmRunner.run_testrepr false + ArmRunner.run_testrepr ~print_final_states:false Arm.(umProm_model tiny_isa) (convert mp_toml) in diff --git a/cli/tests/unit/litmus/testrepr_test.ml b/cli/tests/unit/litmus/testrepr_test.ml index ec44146d..243e3389 100644 --- a/cli/tests/unit/litmus/testrepr_test.ml +++ b/cli/tests/unit/litmus/testrepr_test.ml @@ -241,26 +241,6 @@ let parse_bad_file_test = (** {1 ArchState Conversion And Execution} *) -let archstate_runner_tests = - "testrepr_to_archstate / run_testrepr" - >::: [ ("EOR Expected with seq model" - >:: fun _ -> - let (result, _msgs) = - ArmRunner.run_testrepr true Arm.(seq_model tiny_isa) eor - in - assert_equal Runner.Expected result - ); - ("EOR Expected with seq model" - >:: fun _ -> - let (result, _msgs) = - ArmRunner.run_testrepr false Arm.(seq_model tiny_isa) eor - in - assert_equal Runner.Expected result - ) - ] - let () = run_test_tt_main - ("litmus_testrepr" - >::: [parse_correct_file_test; parse_bad_file_test; archstate_runner_tests] - ) + ("litmus_testrepr" >::: [parse_correct_file_test; parse_bad_file_test]) From 44ec97dd9cd8031649c89d69a3d0fcc4869d0a0c Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 10 Apr 2026 10:56:49 +0100 Subject: [PATCH 08/13] Change lookupi_opt to lookupi --- cli/lib/litmus/minState.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/cli/lib/litmus/minState.ml b/cli/lib/litmus/minState.ml index aebfb26f..c6d4a15e 100644 --- a/cli/lib/litmus/minState.ml +++ b/cli/lib/litmus/minState.ml @@ -105,11 +105,8 @@ module Make (Arch : Archsem.Arch) = struct let mem = ArchState.mem state in List.map (fun (mc : Testrepr.mem_cond) -> - match MemMap.lookupi_opt mc.addr mc.size mem with - | None -> - failwith - (Printf.sprintf "[[outcome]] memory not found at 0x%x" mc.addr) - | Some mv -> {sym = mc.sym; addr = mc.addr; size = mc.size; value = mv} + let value = MemMap.lookupi mc.addr mc.size mem in + {sym = mc.sym; addr = mc.addr; size = mc.size; value = value} ) mem_conds From a813bee7ae477c0d094c8c17d9293c0ee8a515df Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 10 Apr 2026 11:03:34 +0100 Subject: [PATCH 09/13] Minor refactoring --- cli/lib/litmus/mcompare.ml | 6 +++--- cli/lib/litmus/minState.ml | 14 ++++++++++++-- 2 files changed, 15 insertions(+), 5 deletions(-) diff --git a/cli/lib/litmus/mcompare.ml b/cli/lib/litmus/mcompare.ml index 710a1850..755f019e 100644 --- a/cli/lib/litmus/mcompare.ml +++ b/cli/lib/litmus/mcompare.ml @@ -103,9 +103,9 @@ module Make (Arch : Archsem.Arch) = struct (test_name : string) : string = let conds = observable @ unobservable in - let unique_cond = MinimiseState.get_unique_conds_ignoring_value conds in - let minimised_fs = MinimiseState.minimise_states unique_cond final_states in - let unique_minimised_fs = List.sort_uniq compare minimised_fs in + let unique_minimised_fs = + MinimiseState.get_unique_minimised_states conds final_states + in (* Print number of distinct observed states *) let states_count_part = diff --git a/cli/lib/litmus/minState.ml b/cli/lib/litmus/minState.ml index c6d4a15e..20f484c1 100644 --- a/cli/lib/litmus/minState.ml +++ b/cli/lib/litmus/minState.ml @@ -106,12 +106,12 @@ module Make (Arch : Archsem.Arch) = struct List.map (fun (mc : Testrepr.mem_cond) -> let value = MemMap.lookupi mc.addr mc.size mem in - {sym = mc.sym; addr = mc.addr; size = mc.size; value = value} + {sym = mc.sym; addr = mc.addr; size = mc.size; value} ) mem_conds (* For a list of final states, for each final state, - extract the registers and memory location that the conditions check + extract the registers and memory locations that the conditions check (with the final values of these locations) *) let minimise_states ((reg_conds, mem_conds) : (int * string) list * Testrepr.mem_cond list) @@ -122,4 +122,14 @@ module Make (Arch : Archsem.Arch) = struct (minimise_reg_state reg_conds state, minimise_mem_state mem_conds state) ) states + + (* Find all the registers and memory locations that the conditions check, + extract only those locations from each final state, and deduplicate them *) + let get_unique_minimised_states + (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) + (final_states : ArchState.t list) : (reg_state list * mem_state list) list + = + let unique_cond = get_unique_conds_ignoring_value conds in + let minimised_fs = minimise_states unique_cond final_states in + List.sort_uniq compare minimised_fs end From 87cd22c60c26575fd7c80805ef530497035999d1 Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 10 Apr 2026 17:18:02 +0100 Subject: [PATCH 10/13] Separate logically different instances of checking if conds are satisfied --- cli/lib/litmus/mcompare.ml | 37 +++++++-- cli/lib/litmus/runner.ml | 143 ++++++++------------------------- cli/lib/litmus/runner_utils.ml | 85 ++++++++++++++++++++ 3 files changed, 148 insertions(+), 117 deletions(-) create mode 100644 cli/lib/litmus/runner_utils.ml diff --git a/cli/lib/litmus/mcompare.ml b/cli/lib/litmus/mcompare.ml index 755f019e..15db7c73 100644 --- a/cli/lib/litmus/mcompare.ml +++ b/cli/lib/litmus/mcompare.ml @@ -73,12 +73,34 @@ let test_observation_stats_to_string obs_count not_obs_count test_name = module Make (Arch : Archsem.Arch) = struct open Arch module MinimiseState = MinState.Make (Arch) + module RunnerUtils = Runner_utils.Make (Arch) + + (* Get the number of states which satisfy at least one condition in conds *) + let get_obs_count + (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) + (state_list : ArchState.t list) + = + List.length state_list + - List.length + (List.fold_left + (fun unmatched_state_list (cond, mem_cond) -> + List.filter + (fun fs -> + not + (RunnerUtils.check_outcome fs cond + && RunnerUtils.check_mem_outcome fs mem_cond + ) + ) + unmatched_state_list + ) + state_list conds + ) (* Print observation statistics for Mcompare. The format is: Ok/No Observation Always/Sometimes/Never <#observed> <#not_observed> *) let observation_statistics_string - (obs_count : int) + (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) (checking_for_positive : bool) (state_list : ArchState.t list) (test_name : string) : string @@ -87,6 +109,7 @@ module Make (Arch : Archsem.Arch) = struct if checking_for_positive then ("Ok", "No (\"allowed\" not found)") else ("No (\"not allowed\" found)", "Ok") in + let obs_count = get_obs_count conds state_list in let msg = if obs_count > 0 then matched_msg else not_matched_msg in msg ^ "\n" ^ test_observation_stats_to_string obs_count @@ -97,15 +120,13 @@ module Make (Arch : Archsem.Arch) = struct let print_final_states (observable : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) (unobservable : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) - (obs_count : int) - (unobs_count : int) (final_states : ArchState.t list) (test_name : string) : string = let conds = observable @ unobservable in - let unique_minimised_fs = - MinimiseState.get_unique_minimised_states conds final_states - in + let unique_cond = MinimiseState.get_unique_conds_ignoring_value conds in + let minimised_fs = MinimiseState.minimise_states unique_cond final_states in + let unique_minimised_fs = List.sort_uniq compare minimised_fs in (* Print number of distinct observed states *) let states_count_part = @@ -128,9 +149,9 @@ module Make (Arch : Archsem.Arch) = struct if (* Print statistics about the condition(s) that we did and didn't want to observe *) observable <> [] - then observation_statistics_string obs_count true final_states test_name + then observation_statistics_string observable true final_states test_name else if unobservable <> [] then - observation_statistics_string unobs_count false final_states test_name + observation_statistics_string unobservable false final_states test_name else "ERROR: no conditions to observe" in diff --git a/cli/lib/litmus/runner.ml b/cli/lib/litmus/runner.ml index 6ef60550..d6a12718 100644 --- a/cli/lib/litmus/runner.ml +++ b/cli/lib/litmus/runner.ml @@ -108,48 +108,10 @@ let find_index p lst = module Make (Arch : Archsem.Arch) = struct open Arch module AS = ToArchState.Make (Arch) + module RunnerUtils = Runner_utils.Make (Arch) module MinimiseState = MinState.Make (Arch) module McompareInst = Mcompare.Make (Arch) - let check_outcome (fs : ArchState.t) (cond : Testrepr.thread_cond list) : bool = - List.for_all - (fun (tid, reqs) -> - let regs = ArchState.reg tid fs in - List.for_all - (fun (name, req) -> - let reg = Reg.of_string name in - match RegMap.get_opt reg regs with - | None -> - failwith - ("[[outcome]] register not found in final state: " ^ name) - | Some rv -> ( - match req with - | Testrepr.ReqEq exp -> rv = RegVal.of_gen reg exp - | Testrepr.ReqNe exp -> rv = RegVal.of_gen reg exp - ) - ) - reqs - ) - cond - - let check_mem_outcome (fs : ArchState.t) (mem_conds : Testrepr.mem_cond list) : - bool - = - let mem = ArchState.mem fs in - List.for_all - (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) - | Some actual -> ( - match mc.req with - | Testrepr.MemEq expected -> Z.equal actual expected - | Testrepr.MemNe expected -> not (Z.equal actual expected) - ) - ) - mem_conds - let run_executions ~print_final_states model init fuel term test = let msgs = ref [] in let msg s = msgs := s :: !msgs in @@ -182,55 +144,11 @@ module Make (Arch : Archsem.Arch) = struct results in - (* For each condition in observed, get a list of bool representing which final states satisfy the condition *) - let observable_matrix = - List.map - (fun (cond, mem_cond) -> - List.map - (fun fs -> check_outcome fs cond && check_mem_outcome fs mem_cond) - final_states - ) - observable - in - (* For each condition in unobserved, get a list of bool representing which final states satisfy the condition *) - let unobservable_matrix = - List.map - (fun (cond, mem_cond) -> - List.map - (fun fs -> check_outcome fs cond && check_mem_outcome fs mem_cond) - final_states - ) - unobservable - in - - (* Get the number of states which satisfy at least one condition in observable *) - let observable_count = - let state_satisfied_list = - match observable_matrix with - | [] -> [] - | h :: t -> List.fold_left (List.map2 ( || )) h t - in - List.fold_left - (fun acc x -> if x then acc + 1 else acc) - 0 state_satisfied_list - in - (* Get the number of states which satisfy at least one condition in unobservable *) - let unobservable_count = - let state_satisfied_list = - match unobservable_matrix with - | [] -> [] - | h :: t -> List.fold_left (List.map2 ( || )) h t - in - List.fold_left - (fun acc x -> if x then acc + 1 else acc) - 0 state_satisfied_list - in - (* If the print-final-states flag is set, print all observable states and statistics *) if print_final_states then msg - (McompareInst.print_final_states observable unobservable observable_count - unobservable_count final_states test.name + (McompareInst.print_final_states observable unobservable final_states + test.name ); List.iter @@ -241,43 +159,50 @@ module Make (Arch : Archsem.Arch) = struct if flags <> [] then msg "Flagged"; let observable_ok = - List.for_all Fun.id - (List.mapi - (fun i matched_list -> - let matched = List.exists Fun.id matched_list in - ( if (not matched) && final_states <> [] then - let (cond, mem_cond) = List.nth observable i in - msg - (Printf.sprintf "%sObservable not found%s: %s %s" Terminal.red - Terminal.reset (cond_to_string cond) - (mem_cond_to_string mem_cond) - ) - ); - matched - ) - observable_matrix - ) + List.for_all + (fun (cond, mem_cond) -> + let matched = + List.exists + (fun fs -> + RunnerUtils.check_outcome fs cond + && RunnerUtils.check_mem_outcome fs mem_cond + ) + final_states + in + if (not matched) && final_states <> [] then + msg + (Printf.sprintf "%sObservable not found%s: %s %s" Terminal.red + Terminal.reset (cond_to_string cond) + (mem_cond_to_string mem_cond) + ); + matched + ) + observable in let unobservable_ok = List.for_all Fun.id (List.mapi - (fun i matched_list -> - let opt_index = find_index Fun.id matched_list in - match opt_index with - | Some index -> - let (cond, mem_cond) = List.nth unobservable i in + (fun i fs -> + match + List.find_opt + (fun (cond, mem_cond) -> + RunnerUtils.check_outcome fs cond + && RunnerUtils.check_mem_outcome fs mem_cond + ) + unobservable + with + | Some (cond, mem_cond) -> msg (Printf.sprintf "%sUnobservable found%s in execution %d: %s %s" - Terminal.red Terminal.reset (index + 1) - (cond_to_string cond) + Terminal.red Terminal.reset (i + 1) (cond_to_string cond) (mem_cond_to_string mem_cond) ); false | None -> true ) - unobservable_matrix + final_states ) in diff --git a/cli/lib/litmus/runner_utils.ml b/cli/lib/litmus/runner_utils.ml new file mode 100644 index 00000000..4e1d56b2 --- /dev/null +++ b/cli/lib/litmus/runner_utils.ml @@ -0,0 +1,85 @@ +(******************************************************************************) +(* ArchSem *) +(* *) +(* Copyright (c) 2021 *) +(* Thibaut Pérami, University of Cambridge *) +(* Yeji Han, Seoul National University *) +(* Zongyuan Liu, Aarhus University *) +(* Nils Lauermann, University of Cambridge *) +(* Jean Pichon-Pharabod, University of Cambridge, Aarhus University *) +(* Brian Campbell, University of Edinburgh *) +(* Alasdair Armstrong, University of Cambridge *) +(* Ben Simner, University of Cambridge *) +(* Peter Sewell, University of Cambridge *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *) +(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *) +(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *) +(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *) +(* COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *) +(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *) +(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS *) +(* OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR *) +(* TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE *) +(* USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* *) +(******************************************************************************) + +(** Helper functions for checking final states *) + +module Make (Arch : Archsem.Arch) = struct + open Arch + + (* Check if a final state satisfies cond (register conditions) *) + let check_outcome (fs : ArchState.t) (cond : Testrepr.thread_cond list) : bool = + List.for_all + (fun (tid, reqs) -> + let regs = ArchState.reg tid fs in + List.for_all + (fun (name, req) -> + let reg = Reg.of_string name in + match RegMap.get_opt reg regs with + | None -> + failwith + ("[[outcome]] register not found in final state: " ^ name) + | Some rv -> ( + match req with + | Testrepr.ReqEq exp -> rv = RegVal.of_gen reg exp + | Testrepr.ReqNe exp -> rv = RegVal.of_gen reg exp + ) + ) + reqs + ) + cond + + (* Check if a final state satisfies mem_conds *) + let check_mem_outcome (fs : ArchState.t) (mem_conds : Testrepr.mem_cond list) : + bool + = + let mem = ArchState.mem fs in + List.for_all + (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) + | Some actual -> ( + match mc.req with + | Testrepr.MemEq expected -> Z.equal actual expected + | Testrepr.MemNe expected -> not (Z.equal actual expected) + ) + ) + mem_conds +end From 62596a3277c017273737a1c3984890ad044b9be9 Mon Sep 17 00:00:00 2001 From: s-prism Date: Wed, 15 Apr 2026 14:56:14 +0100 Subject: [PATCH 11/13] Map 32-bit regs --- config/X86.toml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/config/X86.toml b/config/X86.toml index c07d44a0..174767ab 100644 --- a/config/X86.toml +++ b/config/X86.toml @@ -33,3 +33,13 @@ r13 = 0 r14 = 0 r15 = 0 rflags = 0 + +[isla.register_renames] +eax = "rax" +ecx = "rcx" +edx = "rdx" +ebx = "rbx" +esp = "rsp" +ebp = "rbp" +esi = "rsi" +edi = "rdi" \ No newline at end of file From acd769f2ffba95097638ab80efdbf62b36231092 Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 17 Apr 2026 17:31:16 +0100 Subject: [PATCH 12/13] Map 16-bit regs --- config/X86.toml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/config/X86.toml b/config/X86.toml index 174767ab..a7552648 100644 --- a/config/X86.toml +++ b/config/X86.toml @@ -42,4 +42,12 @@ ebx = "rbx" esp = "rsp" ebp = "rbp" esi = "rsi" -edi = "rdi" \ No newline at end of file +edi = "rdi" +ax = "rax" +cx = "rcx" +dx = "rdx" +bx = "rbx" +sp = "rsp" +bp = "rbp" +si = "rsi" +di = "rdi" \ No newline at end of file From 534317ebd4412e659f2640ebda4c7d6d9f8dccda Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 17 Apr 2026 17:35:15 +0100 Subject: [PATCH 13/13] Update sail-tiny-x86 --- coq-archsem-x86.opam.locked | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq-archsem-x86.opam.locked b/coq-archsem-x86.opam.locked index 523e8dd8..8b131573 100644 --- a/coq-archsem-x86.opam.locked +++ b/coq-archsem-x86.opam.locked @@ -138,7 +138,7 @@ pin-depends: [ ] [ "coq-sail-tiny-x86.dev" - "git+https://github.com/rems-project/sail-tiny-x86.git#840cbb7" + "git+https://github.com/rems-project/sail-tiny-x86.git#2e6f12e" ] [ "coq-stdpp.1.12.0"