Track values that have been added to the pc since last fresh check

Author: krtab

src/intf/thread_intf.ml

@@ -21,7 +21,7 @@ module type S = sig
        int
     -> Symbol_scope.t
     -> Symbolic_path_condition.t
-    -> bool
+    -> Symbolic_value.bool list
     -> Memory.collection
     -> Symbolic_table.collection
     -> Symbolic_global.collection
@@ -31,9 +31,9 @@ module type S = sig
 
   val pc : t -> Symbolic_path_condition.t
 
-  val pc_is_fresh : t -> bool
+  val pending_pc : t -> Symbolic_value.bool list
 
-  val mark_pc_fresh : t -> t
+  val mark_pending_pc_done : t -> t
 
   val memories : t -> Memory.collection
 

src/symbolic/symbolic_choice.ml

@@ -382,7 +382,7 @@ module Make (Thread : Thread_intf.S) = struct
     let* () = yield in
     let* solver in
     match Solver.check solver pc with
-    | `Sat -> modify_thread Thread.mark_pc_fresh
+    | `Sat -> modify_thread Thread.mark_pending_pc_done
     | `Unsat -> stop
     | `Unknown -> assert false
 
@@ -392,17 +392,15 @@ module Make (Thread : Thread_intf.S) = struct
   *)
   let check_reachability =
     let* thread in
-    if Thread.pc_is_fresh thread then return ()
-    else
-      let pc = Thread.pc thread in
-      stop_if_unreachable (Symbolic_path_condition.to_set pc)
-
-  let add_to_pc_and_check_reachability v =
-    let* () = check_reachability in
-    let* () = add_pc v in
-    let* thread in
-    let pc = Symbolic_path_condition.slice (Thread.pc thread) v in
-    stop_if_unreachable pc
+    match Thread.pending_pc thread with
+    | [] -> return ()
+    | hd :: tl -> begin
+      let pc_to_check = List.fold_left Symbolic_value.Bool.and_ hd tl in
+      let pc_to_check =
+        Symbolic_path_condition.slice (Thread.pc thread) pc_to_check
+      in
+      stop_if_unreachable pc_to_check
+    end
 
   let get_model_or_stop symbol =
     let* () = yield in
@@ -413,7 +411,7 @@ module Make (Thread : Thread_intf.S) = struct
     | `Unsat -> stop
     | `Sat -> begin
       let symbol_scopes = Symbol_scope.of_symbol symbol in
-      let* () = modify_thread Thread.mark_pc_fresh in
+      let* () = modify_thread Thread.mark_pending_pc_done in
       (* TODO: we are doing the check two times here, because Solver.model is also doing it, we should remove it! *)
       let model = Solver.model solver ~symbol_scopes ~pc in
       match Smtml.Model.evaluate model symbol with
@@ -433,15 +431,18 @@ module Make (Thread : Thread_intf.S) = struct
     | _ ->
       let true_branch =
         let* () = add_breadcrumb 1 in
-        let+ () = add_to_pc_and_check_reachability v in
+        let* () = add_pc v in
+        let+ () = check_reachability in
         true
       in
       let false_branch =
         let neg_v = Symbolic_value.Bool.not v in
         let* () = add_breadcrumb 0 in
-        let+ () = add_to_pc_and_check_reachability neg_v in
+        let* () = add_pc neg_v in
+        let+ () = check_reachability in
         false
       in
+      let* () = check_reachability in
       if explore_first then choose true_branch false_branch
       else choose false_branch true_branch
   [@@inline]
@@ -494,15 +495,18 @@ module Make (Thread : Thread_intf.S) = struct
         in
         let this_val_branch =
           let* () = add_breadcrumb (Int32.to_int i) in
-          let+ () = add_pc this_value_cond in
+          let* () = add_pc this_value_cond in
+          let+ () = modify_thread Thread.mark_pending_pc_done in
           i
         in
         let not_this_val_branch =
           let* () = add_pc not_this_value_cond in
+          let* () = modify_thread Thread.mark_pending_pc_done in
           generator ()
         in
         choose this_val_branch not_this_val_branch
       in
+      let* () = check_reachability in
       generator ()
 
   let assertion c =

src/symbolic/thread.ml

@@ -13,7 +13,7 @@ struct
     { num_symbols : int
     ; symbol_scopes : Symbol_scope.t
     ; pc : Symbolic_path_condition.t
-    ; pc_fresh : bool
+    ; pending_pc : Symbolic_value.bool list
     ; memories : Memory.collection
     ; tables : Symbolic_table.collection
     ; globals : Symbolic_global.collection
@@ -23,12 +23,12 @@ struct
     ; labels : (int * string) list
     }
 
-  let create num_symbols symbol_scopes pc pc_fresh memories tables globals
+  let create num_symbols symbol_scopes pc pending_pc memories tables globals
     breadcrumbs labels =
     { num_symbols
     ; symbol_scopes
     ; pc
-    ; pc_fresh
+    ; pending_pc
     ; memories
     ; tables
     ; globals
@@ -40,13 +40,13 @@ struct
     let num_symbols = 0 in
     let symbol_scopes = Symbol_scope.empty in
     let pc = Symbolic_path_condition.empty in
-    let pc_fresh = true in
+    let pending_pc = [] in
     let memories = Memory.init () in
     let tables = Symbolic_table.init () in
     let globals = Symbolic_global.init () in
     let breadcrumbs = [] in
     let labels = [] in
-    create num_symbols symbol_scopes pc pc_fresh memories tables globals
+    create num_symbols symbol_scopes pc pending_pc memories tables globals
       breadcrumbs labels
 
   let num_symbols t = t.num_symbols
@@ -55,9 +55,9 @@ struct
 
   let pc t = t.pc
 
-  let pc_is_fresh t = t.pc_fresh
+  let pending_pc t = t.pending_pc
 
-  let mark_pc_fresh t = { t with pc_fresh = true }
+  let mark_pending_pc_done t = { t with pending_pc = [] }
 
   let memories t = t.memories
 
@@ -75,7 +75,7 @@ struct
 
   let add_pc t c =
     let pc = Symbolic_path_condition.add t.pc c in
-    { t with pc; pc_fresh = false }
+    { t with pc; pending_pc = c :: t.pending_pc }
 
   let add_breadcrumb t crumb =
     let breadcrumbs = crumb :: t.breadcrumbs in
@@ -99,20 +99,22 @@ struct
     { num_symbols
     ; symbol_scopes
     ; pc
-    ; pc_fresh
+    ; pending_pc
     ; memories
     ; tables
     ; globals
     ; breadcrumbs
     ; labels
     } =
+    if not @@ List.is_empty pending_pc then
+      Fmt.epr "Warning: cloning thread with a non empty pending pc";
     let memories = Memory.clone memories in
     let tables = Symbolic_table.clone tables in
     let globals = Symbolic_global.clone globals in
     { num_symbols
     ; symbol_scopes
     ; pc
-    ; pc_fresh
+    ; pending_pc
     ; memories
     ; tables
     ; globals

src/symbolic/thread_with_memory.ml

@@ -9,14 +9,14 @@ let project (th : t) : Thread_without_memory.t * _ =
     let num_symbols = num_symbols th in
     let symbol_scopes = symbol_scopes th in
     let pc = pc th in
-    let pc_fresh = pc_is_fresh th in
+    let pending_pc = pending_pc 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
     let labels = labels th in
-    Thread_without_memory.create num_symbols symbol_scopes pc pc_fresh memories
-      tables globals breadcrumbs labels
+    Thread_without_memory.create num_symbols symbol_scopes pc pending_pc
+      memories tables globals breadcrumbs labels
   in
   let backup = memories th in
   (projected, backup)
@@ -25,7 +25,7 @@ let restore backup th =
   let num_symbols = Thread_without_memory.num_symbols th in
   let symbol_scopes = Thread_without_memory.symbol_scopes th in
   let pc = Thread_without_memory.pc th in
-  let pc_fresh = Thread_without_memory.pc_is_fresh th in
+  let pending_pc = Thread_without_memory.pending_pc th in
   let memories =
     if Thread_without_memory.memories th then
       Symbolic_memory_concretizing.clone backup
@@ -35,5 +35,5 @@ let restore backup th =
   let globals = Thread_without_memory.globals th in
   let breadcrumbs = Thread_without_memory.breadcrumbs th in
   let labels = Thread_without_memory.labels th in
-  create num_symbols symbol_scopes pc pc_fresh memories tables globals
+  create num_symbols symbol_scopes pc pending_pc memories tables globals
     breadcrumbs labels