Print final register and memory states

.gitignore

@@ -10,3 +10,4 @@
 _build
 _opam
 .envrc
+.vscode

cli/bin/main.ml

@@ -184,19 +184,32 @@ 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 =
   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_term 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 =
@@ -208,11 +221,15 @@ let cmd_seq =
 (** The user-mode promising command *)
 let cmd_ump =
   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_term 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 =
@@ -250,11 +267,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_term 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 =
@@ -274,12 +294,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_term 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 =

cli/lib/litmus/mcompare.ml

@@ -0,0 +1,159 @@
+(******************************************************************************)
+(*                                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 <test name> <string freq> <true count> <false count>.
+  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)
+  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 <Optional extra detail>
+    Observation <test_name> Always/Sometimes/Never <#observed> <#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
+
+  (* 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)
+        (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 observable true final_states test_name
+      else if unobservable <> [] then
+        observation_statistics_string unobservable false final_states test_name
+      else "ERROR: no conditions to observe"
+    in
+
+    states_count_part ^ state_list_part ^ observation_part
+end

cli/lib/litmus/minState.ml

@@ -0,0 +1,135 @@
+(******************************************************************************)
+(*                                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;
+    value : int
+  }
+
+type mem_state =
+  { sym : string;
+    addr : int;
+    size : int;
+    value : int
+  }
+
+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
+    =
+    List.concat_map
+      (fun (thread, reg_pair) ->
+         List.map (fun (name, _) -> (thread, name)) reg_pair
+       )
+      reg_cond
+
+  (* 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
+    =
+    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
+    =
+    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
+
+  (* 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
+    =
+    let mem = ArchState.mem state in
+    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}
+       )
+      mem_conds
+
+  (* For a list of final states, for each final state, 
+    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)
+        (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
+
+  (* 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