Store pc freshness in thread

Author: krtab

src/intf/thread_intf.ml

@@ -21,6 +21,7 @@ module type S = sig
        int
     -> Smtml.Symbol.t list
     -> Symbolic_value.bool list
+    -> bool
     -> Memory.collection
     -> Symbolic_table.collection
     -> Symbolic_global.collection
@@ -29,6 +30,10 @@ module type S = sig
 
   val pc : t -> Symbolic_value.bool list
 
+  val pc_is_fresh : t -> bool
+
+  val mark_pc_fresh : t -> t
+
   val memories : t -> Memory.collection
 
   val tables : t -> Symbolic_table.collection

src/symbolic/symbolic_choice.ml

@@ -381,38 +381,41 @@ module Make (Thread : Thread.S) = struct
             ~other_machine:n_chck.other_machine )
       | None -> default
     in
-    let* () = yield in
     let* thread in
-    let* solver in
-    let interrupter = fun () -> Solver.interrupt solver in
-    let other_unsat =
-      on_n_chck false (fun ~self_machine ~other_machine ->
-        match !other_machine with
-        | Done `Unsat -> true
-        | Done `SatOrUnknown -> false
-        | Init | Running _ ->
-          self_machine := Running interrupter;
-          false )
-    in
-    let pc = Thread.pc thread in
-    let our_result = if other_unsat then `Sat else Solver.check solver pc in
-    match our_result with
-    | `Sat ->
-      on_n_chck () (fun ~self_machine ~other_machine:_ ->
-        self_machine := Done `SatOrUnknown );
-      return ()
-    | `Unsat ->
-      on_n_chck () (fun ~self_machine ~other_machine ->
-        self_machine := Done `Unsat;
-        match !other_machine with Running inter -> inter () | _ -> () );
-      stop
-    | `Unknown ->
-      (* Unknown is what is returned when interrupted *)
-      on_n_chck stop (fun ~self_machine ~other_machine ->
-        self_machine := Done `SatOrUnknown;
-        match !other_machine with
-        | Init | Done `SatOrUnknown | Running _ -> stop
-        | Done `Unsat -> return () )
+    let pc_fresh = Thread.pc_is_fresh thread in
+    if pc_fresh then return ()
+    else
+      let* () = yield in
+      let* solver in
+      let interrupter = fun () -> Solver.interrupt solver in
+      let other_unsat =
+        on_n_chck false (fun ~self_machine ~other_machine ->
+          match !other_machine with
+          | Done `Unsat -> true
+          | Done `SatOrUnknown -> false
+          | Init | Running _ ->
+            self_machine := Running interrupter;
+            false )
+      in
+      let pc = Thread.pc thread in
+      let our_result = if other_unsat then `Sat else Solver.check solver pc in
+      match our_result with
+      | `Sat ->
+        on_n_chck () (fun ~self_machine ~other_machine:_ ->
+          self_machine := Done `SatOrUnknown );
+        modify_thread Thread.mark_pc_fresh
+      | `Unsat ->
+        on_n_chck () (fun ~self_machine ~other_machine ->
+          self_machine := Done `Unsat;
+          match !other_machine with Running inter -> inter () | _ -> () );
+        stop
+      | `Unknown ->
+        (* Unknown is what is returned when interrupted *)
+        on_n_chck stop (fun ~self_machine ~other_machine ->
+          self_machine := Done `SatOrUnknown;
+          match !other_machine with
+          | Init | Done `SatOrUnknown | Running _ -> stop
+          | Done `Unsat -> modify_thread Thread.mark_pc_fresh )
 
   let get_model_or_stop symbol =
     let* () = yield in
@@ -438,7 +441,7 @@ module Make (Thread : Thread.S) = struct
     | Val False -> return false
     | Val (Num (I32 _)) -> Fmt.failwith "unreachable (type error)"
     | _ ->
-      let* () = check_reachability None in 
+      let* () = check_reachability None in
       let machine_a = ref Init in
       let machine_b = ref Init in
       let mutex = Mutex.create () in

src/symbolic/thread.ml

@@ -12,6 +12,7 @@ module Make (Symbolic_memory : M) :
     { symbols : int
     ; symbol_set : Smtml.Symbol.t list
     ; pc : Symbolic_value.bool list
+    ; pc_fresh : bool
     ; memories : Memory.collection
     ; tables : Symbolic_table.collection
     ; globals : Symbolic_global.collection
@@ -20,25 +21,39 @@ module Make (Symbolic_memory : M) :
     ; breadcrumbs : int32 list
     }
 
-  let create symbols symbol_set pc memories tables globals breadcrumbs =
-    { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs }
+  let create symbols symbol_set pc pc_fresh memories tables globals breadcrumbs
+      =
+    { symbols
+    ; symbol_set
+    ; pc
+    ; pc_fresh
+    ; memories
+    ; tables
+    ; globals
+    ; breadcrumbs
+    }
 
   let init () =
     let symbols = 0 in
     let symbol_set = [] in
     let pc = [] in
+    let pc_fresh = true in
     let memories = Memory.init () in
     let tables = Symbolic_table.init () in
     let globals = Symbolic_global.init () in
     let breadcrumbs = [] in
-    create symbols symbol_set pc memories tables globals breadcrumbs
+    create symbols symbol_set pc pc_fresh memories tables globals breadcrumbs
 
   let symbols t = t.symbols
 
   let symbols_set t = t.symbol_set
 
   let pc t = t.pc
 
+  let pc_is_fresh t = t.pc_fresh
+
+  let mark_pc_fresh t = { t with pc_fresh = true }
+
   let memories t = t.memories
 
   let tables t = t.tables
@@ -49,16 +64,32 @@ module Make (Symbolic_memory : M) :
 
   let add_symbol t s = { t with symbol_set = s :: t.symbol_set }
 
-  let add_pc t c = { t with pc = c :: t.pc }
+  let add_pc t c = { t with pc = c :: t.pc; pc_fresh = false }
 
   let add_breadcrumb t crumb = { t with breadcrumbs = crumb :: t.breadcrumbs }
 
   let incr_symbols t = { t with symbols = succ t.symbols }
 
-  let clone { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs }
-      =
+  let clone
+    { symbols
+    ; symbol_set
+    ; pc
+    ; pc_fresh
+    ; memories
+    ; tables
+    ; globals
+    ; breadcrumbs
+    } =
     let memories = Memory.clone memories in
     let tables = Symbolic_table.clone tables in
     let globals = Symbolic_global.clone globals in
-    { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs }
+    { symbols
+    ; symbol_set
+    ; pc
+    ; pc_fresh
+    ; memories
+    ; tables
+    ; globals
+    ; breadcrumbs
+    }
 end

src/symbolic/thread_with_memory.ml

@@ -9,12 +9,13 @@ let project (th : t) : Thread_without_memory.t * _ =
     let symbols = symbols th in
     let symbols_set = symbols_set th in
     let pc = pc th in
+    let pc_fresh = pc_is_fresh th in
     let memories = Thread_without_memory.Memory.init () in
     let tables = tables th in
     let globals = globals th in
     let breadcrumbs = breadcrumbs th in
-    Thread_without_memory.create symbols symbols_set pc memories tables globals
-      breadcrumbs
+    Thread_without_memory.create symbols symbols_set pc pc_fresh memories tables
+      globals breadcrumbs
   in
   let backup = memories th in
   (projected, backup)
@@ -23,6 +24,7 @@ let restore backup th =
   let symbols = Thread_without_memory.symbols th in
   let symbols_set = Thread_without_memory.symbols_set th in
   let pc = Thread_without_memory.pc th in
+  let pc_fresh = Thread_without_memory.pc_is_fresh th in
   let memories =
     if Thread_without_memory.memories th then
       Symbolic_memory_concretizing.clone backup
@@ -31,4 +33,4 @@ let restore backup th =
   let tables = Thread_without_memory.tables th in
   let globals = Thread_without_memory.globals th in
   let breadcrumbs = Thread_without_memory.breadcrumbs th in
-  create symbols symbols_set pc memories tables globals breadcrumbs
+  create symbols symbols_set pc pc_fresh memories tables globals breadcrumbs