Incremental: (Cheap!) Full Reachability to Prune

src/solvers/postSolver.ml

@@ -17,7 +17,7 @@ end
 (** Functorial postsolver for any system. *)
 module type F =
   functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
-  S with module S = S and module VH = VH
+    S with module S = S and module VH = VH
 
 (** Base implementation for postsolver. *)
 module Unit: F =
@@ -211,7 +211,7 @@ struct
       if M.tracing then M.trace "postsolver" "one_constraint %a %a\n" S.Var.pretty_trace x S.Dom.pretty rhs;
       PS.one_constraint ~vh ~x ~rhs
     in
-    List.iter one_var vs;
+    (Stats.time "potentially_incremental_reach" (List.iter one_var)) vs;
 
     PS.finalize ~vh ~reachable;
     Goblintutil.postsolving := false

src/solvers/td3.ml

@@ -35,6 +35,7 @@ module WP =
       mutable side_infl: VS.t HM.t; (** Influences to side-effected variables. Not normally in [infl], but used for restarting them. *)
       mutable var_messages: Message.t HM.t;
       mutable rho_write: S.Dom.t HM.t HM.t;
+      mutable dep: VS.t HM.t
     }
 
     type marshal = solver_data
@@ -50,12 +51,13 @@ module WP =
       side_infl = HM.create 10;
       var_messages = HM.create 10;
       rho_write = HM.create 10;
+      dep = HM.create 10;
     }
 
     let print_data data str =
       if GobConfig.get_bool "dbg.verbose" then
-        Printf.printf "%s:\n|rho|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n"
-          str (HM.length data.rho) (HM.length data.stable) (HM.length data.infl) (HM.length data.wpoint) (HM.length data.side_dep) (HM.length data.side_infl)
+        Printf.printf "%s:\n|rho|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|dep|=%d\n"
+          str (HM.length data.rho) (HM.length data.stable) (HM.length data.infl) (HM.length data.wpoint) (HM.length data.side_dep) (HM.length data.side_infl) (HM.length data.dep)
 
     let verify_data data =
       if GobConfig.get_bool "solvers.td3.verify" then (
@@ -154,6 +156,9 @@ module WP =
       let abort_verify = GobConfig.get_bool "solvers.td3.abort-verify" in
       let prev_dep_vals = HM.create 10 in
 
+      (* Tracks dependencies between an unknown and the things it depends on AND has side-effects to *)
+      let dep = data.dep in
+
       let () = print_solver_stats := fun () ->
         Printf.printf "|rho|=%d\n|called|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n"
           (HM.length rho) (HM.length called) (HM.length stable) (HM.length infl) (HM.length wpoint) (HM.length side_dep) (HM.length side_infl);
@@ -182,8 +187,12 @@ module WP =
       let add_infl y x =
         if tracing then trace "sol2" "add_infl %a %a\n" S.Var.pretty_trace y S.Var.pretty_trace x;
         HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty));
+        HM.replace dep x (VS.add y (HM.find_default dep x VS.empty));
       in
-      let add_sides y x = HM.replace sides y (VS.add x (try HM.find sides y with Not_found -> VS.empty)) in
+      let add_sides y x =
+        (* dep records also the things an unknown has side-effects on *)
+        HM.replace dep x (VS.add y (HM.find_default dep x VS.empty));
+        HM.replace sides y (VS.add x (try HM.find sides y with Not_found -> VS.empty)) in
 
       let destabilize_ref: (?front:bool -> S.v -> unit) ref = ref (fun ?front _ -> failwith "no destabilize yet") in
       let destabilize x = !destabilize_ref x in (* must be eta-expanded to use changed destabilize_ref *)
@@ -260,10 +269,13 @@ module WP =
           let (tmp, aborted) =
             match reuse_eq with
             | Some d when narrow_reuse && not narrow_reuse_verify ->
+              (* Do not reset deps for reuse of eq *)
               if tracing then trace "sol2" "eq reused %a\n" S.Var.pretty_trace x;
               incr Goblintutil.narrow_reuses;
               (d, false)
             | _ ->
+              (* The RHS is re-evaluated, all deps are re-trigerred *)
+              HM.replace dep x VS.empty;
               try
                 if abort && abort_verify then (
                   (* collect dep vals for x *)
@@ -739,6 +751,7 @@ module WP =
         delete_marked rho;
         delete_marked infl;
         delete_marked wpoint;
+        delete_marked dep;
 
         (* destabilize_with_side doesn't have all infl to follow anymore, so should somewhat work with reluctant *)
         if restart_sided then (
@@ -964,6 +977,7 @@ module WP =
           filter_vs_hm infl;
           filter_vs_hm side_infl;
           filter_vs_hm side_dep;
+          filter_vs_hm dep;
 
           VH.filteri_inplace (fun x w ->
               if VH.mem reachable x then (
@@ -980,17 +994,41 @@ module WP =
       end
       in
 
-      (* postsolver also populates side_dep and side_infl *)
+      (* postsolver also populates side_dep, side_infl, and dep *)
       let module SideInfl: PostSolver.S with module S = S and module VH = HM =
       struct
         include PostSolver.Unit (S) (HM)
 
         let one_side ~vh ~x ~y ~d =
+          (* Also record side-effects caused by post-solver *)
+          HM.replace dep x (VS.add y (HM.find_default dep x VS.empty));
           HM.replace side_dep y (VS.add x (try HM.find side_dep y with Not_found -> VS.empty));
           HM.replace side_infl x (VS.add y (try HM.find side_infl x with Not_found -> VS.empty));
       end
       in
 
+      let reachable_and_superstable =
+        if incr_verify then
+          (* Perform reachability on whole constraint system, but cheaply by using logged dependencies *)
+          (* This only works if the other reachability has been performed before, so dependencies created only during postsolve are recorded *)
+          let reachable' = HM.create (HM.length rho) in
+          let rechable_and_superstable = HM.create (HM.length rho) in
+          let rec one_var' x =
+            if (not (HM.mem reachable' x)) then (
+              if HM.mem superstable x then HM.replace rechable_and_superstable x ();
+              HM.replace reachable' x ();
+              match HM.find_option dep x with
+              | Some vs -> VS.iter one_var' vs
+              | None -> ()
+            )
+          in
+          (Stats.time "cheap_full_reach" (List.iter one_var')) vs;
+
+          rechable_and_superstable (* consider superstable reached if it is still reachable: stop recursion (evaluation) and keep from being pruned *)
+        else
+          HM.create 0 (* doesn't matter, not used *)
+      in
+
       (* restart write-only *)
       HM.iter (fun x w ->
           HM.iter (fun y d ->
@@ -999,20 +1037,15 @@ module WP =
         ) rho_write;
 
       if incr_verify then (
-        HM.filteri_inplace (fun x _ -> HM.mem superstable x) var_messages;
-        HM.filteri_inplace (fun x _ -> HM.mem superstable x) rho_write
+        HM.filteri_inplace (fun x _ -> HM.mem reachable_and_superstable x) var_messages;
+        HM.filteri_inplace (fun x _ -> HM.mem reachable_and_superstable x) rho_write
       )
       else (
         HM.clear var_messages;
         HM.clear rho_write
       );
 
-      let init_reachable =
-        if incr_verify then
-          HM.copy superstable (* consider superstable reached: stop recursion (evaluation) and keep from being pruned *)
-        else
-          HM.create 0 (* doesn't matter, not used *)
-      in
+      let init_reachable = reachable_and_superstable in
 
       let module IncrWarn: PostSolver.S with module S = S and module VH = HM =
       struct
@@ -1021,13 +1054,6 @@ module WP =
         let init () =
           init (); (* enable warning like standard Warn *)
 
-          (* replay superstable messages *)
-          if incr_verify then (
-            HM.iter (fun _ m ->
-                Messages.add m
-              ) var_messages;
-          );
-
           (* hook to collect new messages *)
           Messages.Table.add_hook := (fun m ->
             match !current_var with
@@ -1036,6 +1062,13 @@ module WP =
           )
 
         let finalize ~vh ~reachable =
+          (* replay superstable messages from unknowns that are still reachable *)
+          if incr_verify then (
+            HM.iter (fun (l:S.v) m ->
+                Messages.add m
+              ) var_messages;
+          );
+
           finalize ~vh ~reachable; (* disable warning like standard Warn *)
 
           (* unhook to avoid accidental var_messages modifications *)
@@ -1049,19 +1082,7 @@ module WP =
       struct
         include PostSolver.Unit (S) (HM)
 
-        let init () =
-          (* retrigger superstable side writes *)
-          if incr_verify then (
-            HM.iter (fun x w ->
-                HM.iter (fun y d ->
-                    let old_d = try HM.find rho y with Not_found -> S.Dom.bot () in
-                    (* ignore (Pretty.printf "rho_write retrigger %a %a %a %a\n" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty old_d S.Dom.pretty d); *)
-                    HM.replace rho y (S.Dom.join old_d d);
-                    HM.replace init_reachable y ();
-                    HM.replace stable y (); (* make stable just in case, so following incremental load would have in superstable *)
-                  ) w
-              ) rho_write
-          )
+        let init () = ()
 
         let one_side ~vh ~x ~y ~d =
           if S.Var.is_write_only y then (
@@ -1077,6 +1098,21 @@ module WP =
             in
             VH.add w y d (* intentional add *)
           )
+
+        let finalize ~vh ~reachable =
+          (* retrigger superstable side writes from unknowns that are still reachable *)
+          if incr_verify then (
+            HM.iter (fun x w ->
+                HM.iter (fun y d ->
+                    let old_d = try HM.find rho y with Not_found -> S.Dom.bot () in
+                    (* ignore (Pretty.printf "rho_write retrigger %a %a %a %a\n" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty old_d S.Dom.pretty d); *)
+                    HM.replace rho y (S.Dom.join old_d d);
+                    HM.replace init_reachable y ();
+                    HM.replace stable y (); (* make stable just in case, so following incremental load would have in superstable *)
+                  ) w
+              ) rho_write
+          )
+
       end
       in
 
@@ -1106,7 +1142,7 @@ module WP =
       print_data data "Data after postsolve";
 
       verify_data data;
-      {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write}
+      {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}
 
     let solve box st vs =
       let reuse_stable = GobConfig.get_bool "incremental.stable" in
@@ -1180,6 +1216,11 @@ module WP =
               HM.replace rho_write' (S.Var.relift x) w';
             ) data.rho_write;
           data.rho_write <- rho_write';
+          let dep' = HM.create (HM.length data.dep) in
+          HM.iter (fun k v ->
+              HM.replace dep' (S.Var.relift k) (VS.map S.Var.relift v)
+            ) data.dep;
+          data.dep <- dep';
         );
         if not reuse_stable then (
           print_endline "Destabilizing everything!";

tests/incremental/00-basic/09-unreach.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+void foo() {
+  int x = 2;
+  assert(x == 3); //FAIL
+}
+
+int main() {
+  int a = 1;
+
+  foo();
+
+  return 0;
+}

tests/incremental/00-basic/09-unreach.json

@@ -0,0 +1,8 @@
+{
+    "dbg": {
+        "debug": true
+    },
+    "incremental" : {
+        "verify": true
+    }
+}

tests/incremental/00-basic/09-unreach.patch

@@ -0,0 +1,17 @@
+--- tests/incremental/00-basic/09-unreach.c
++++ tests/incremental/00-basic/09-unreach.c
+@@ -2,13 +2,12 @@
+
+ void foo() {
+   int x = 2;
+-  assert(x == 3); //FAIL
++  assert(x == 3); //NOWARN
+ }
+
+ int main() {
+   int a = 1;
+
+-  foo();
+
+   return 0;
+ }

tests/incremental/00-basic/10-reach.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include<pthread.h>
+
+void foo() {
+  int x = 2;
+  assert(x == 2);
+}
+
+int main() {
+    pthread_t id;
+    pthread_create(&id, NULL, foo, NULL); // just go multithreaded
+
+  return 0;
+}

tests/incremental/00-basic/10-reach.json

@@ -0,0 +1,8 @@
+{
+    "dbg": {
+        "debug": true
+    },
+    "incremental" : {
+        "verify": true
+    }
+}