Add breadcrumbs to Thread.t

As identified in #208, the
deterministic order option is not deterministic across architectures.

A likely culprit is the use of the polymorphic compare function which
may not give the same result in different environments or on different
targets.

This commit resolves this by keeping track of each choice made ('select')
through "breadcrumbs" and sorting results on these breadcrumbs.

Closes: #208

src/cmd_sym.ml

@@ -250,7 +250,13 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
   in
   let results =
     if deterministic_result_order then
-      List.to_seq @@ List.sort compare @@ List.of_seq results
+      results
+      |> Seq.map (function (_, th) as x ->
+           (x, List.rev @@ Thread.breadcrumbs th) )
+      |> List.of_seq
+      |> List.sort (fun (_, bc1) (_, bc2) ->
+             List.compare Stdlib.Int32.compare bc1 bc2 )
+      |> List.to_seq |> Seq.map fst
     else results
   in
   let* count = print_and_count_failures 0 results in

src/symbolic_choice.ml

@@ -465,6 +465,9 @@ module Multicore = struct
       set_thread new_thread
   [@@inline]
 
+  let add_breadcrumb crumb =
+    modify_thread (fun t -> { t with breadcrumbs = crumb :: t.breadcrumbs })
+
   (*
     Yielding is currently done each time the solver is about to be called,
     in check_reachability and get_model.
@@ -511,11 +514,13 @@ module Multicore = struct
     | _ ->
       let true_branch =
         let* () = add_pc v in
+        let* () = add_breadcrumb 1l in
         let+ () = check_reachability in
         true
       in
       let false_branch =
         let* () = add_pc (Symbolic_value.Bool.not v) in
+        let* () = add_breadcrumb 0l in
         let+ () = check_reachability in
         false
       in
@@ -556,6 +561,7 @@ module Multicore = struct
           Expr.Bitv.I32.(Expr.mk_symbol symbol != v i)
         in
         let this_val_branch =
+          let* () = add_breadcrumb i in
           let+ () = add_pc this_value_cond in
           i
         in

src/thread.ml

@@ -9,6 +9,9 @@ type t =
   ; memories : Symbolic_memory.collection
   ; tables : Symbolic_table.collection
   ; globals : Symbolic_global.collection
+      (** Breadcrumbs represent the list of choices that were made so far. They
+          identify one given symbolic execution trace. *)
+  ; breadcrumbs : int32 list
   }
 
 let pc t = t.pc
@@ -19,17 +22,20 @@ let tables t = t.tables
 
 let globals t = t.globals
 
+let breadcrumbs t = t.breadcrumbs
+
 let create () =
   { choices = 0
   ; symbol_set = []
   ; pc = []
   ; memories = Symbolic_memory.init ()
   ; tables = Symbolic_table.init ()
   ; globals = Symbolic_global.init ()
+  ; breadcrumbs = []
   }
 
-let clone { choices; symbol_set; pc; memories; tables; globals } =
+let clone { choices; symbol_set; pc; memories; tables; globals; breadcrumbs } =
   let memories = Symbolic_memory.clone memories in
   let tables = Symbolic_table.clone tables in
   let globals = Symbolic_global.clone globals in
-  { choices; symbol_set; pc; memories; tables; globals }
+  { choices; symbol_set; pc; memories; tables; globals; breadcrumbs }

test/sym/table.t

@@ -1,14 +1,14 @@
 table stuff:
   $ owi sym table.wat --deterministic-result-order
-  Trap: undefined element
+  Trap: unreachable
   Model:
     (model
       (symbol_0 (i32 0))
-      (symbol_1 (i32 -2147483648)))
-  Trap: unreachable
+      (symbol_1 (i32 0)))
+  Trap: undefined element
   Model:
     (model
       (symbol_0 (i32 0))
-      (symbol_1 (i32 0)))
+      (symbol_1 (i32 -2147483648)))
   Reached 2 problems!
   [13]