Incremental analysis: Eagerly analyze functions in force-reanalyze, even when reluctant is on

src/incremental/compareCIL.ml

@@ -16,49 +16,61 @@ type changed_global = {
   diff: nodes_diff option
 }
 
+module VarinfoSet = Set.Make(CilType.Varinfo)
+
 type change_info = {
   mutable changed: changed_global list;
   mutable unchanged: global list;
   mutable removed: global list;
-  mutable added: global list
+  mutable added: global list;
+  mutable force_reanalyze: VarinfoSet.t;
+  (** Set of functions that are to be force-reanalyzed.
+      These functions are additionally included in the [changed] field, among the other changed globals. *)
 }
 
 let empty_change_info () : change_info =
-  {added = []; removed = []; changed = []; unchanged = []}
+  {added = []; removed = []; changed = []; unchanged = []; force_reanalyze = VarinfoSet.empty}
+
+type change_status = Unchanged | Changed | ForceReanalyze of Cil.fundec
+
+(** Given a boolean that indicates whether the code object is identical to the previous version, returns the corresponding [change_status]*)
+let unchanged_to_change_status = function
+  | true -> Unchanged
+  | false -> Changed
 
 (* If some CFGs of the two functions to be compared are provided, a fine-grained CFG comparison is done that also determines which
  * nodes of the function changed. If on the other hand no CFGs are provided, the "old" AST comparison on the CIL.file is
  * used for functions. Then no information is collected regarding which parts/nodes of the function changed. *)
-let eqF (a: Cil.fundec) (b: Cil.fundec) (cfgs : (cfg * cfg) option) =
+let eqF (old: Cil.fundec) (current: Cil.fundec) (cfgs : (cfg * cfg) option) =
   let unchangedHeader =
     try
-      eq_varinfo a.svar b.svar &&
-      List.for_all2 eq_varinfo a.sformals b.sformals
+      eq_varinfo old.svar current.svar &&
+      List.for_all2 eq_varinfo old.sformals current.sformals
     with Invalid_argument _ -> false in
-  let identical, diffOpt =
-    if List.mem a.svar.vname (GobConfig.get_string_list "incremental.force-reanalyze.funs") then
-      false, None
+  let change_status, diffOpt =
+    if List.mem current.svar.vname (GobConfig.get_string_list "incremental.force-reanalyze.funs") then
+      ForceReanalyze current, None
     else
       try
-        let sameDef = unchangedHeader && List.for_all2 eq_varinfo a.slocals b.slocals in
+        let sameDef = unchangedHeader && List.for_all2 eq_varinfo old.slocals current.slocals in
         match cfgs with
-        | None -> sameDef && eq_block (a.sbody, a) (b.sbody, b), None
+        | None -> unchanged_to_change_status (sameDef && eq_block (old.sbody, old) (current.sbody, current)), None
         | Some (cfgOld, cfgNew) ->
           let module CfgOld : MyCFG.CfgForward = struct let next = cfgOld end in
           let module CfgNew : MyCFG.CfgForward = struct let next = cfgNew end in
-          let matches, diffNodes1, diffNodes2 = compareFun (module CfgOld) (module CfgNew) a b in
-          if not sameDef then (false, None)
-          else if diffNodes1 = [] && diffNodes2 = [] then (true, None)
-          else (false, Some {unchangedNodes = matches; primObsoleteNodes = diffNodes1; primNewNodes = diffNodes2})
+          let matches, diffNodes1, diffNodes2 = compareFun (module CfgOld) (module CfgNew) old current in
+          if not sameDef then (Changed, None)
+          else if diffNodes1 = [] && diffNodes2 = [] then (Changed, None)
+          else (Changed, Some {unchangedNodes = matches; primObsoleteNodes = diffNodes1; primNewNodes = diffNodes2})
       with Invalid_argument _ -> (* The combine failed because the lists have differend length *)
-        false, None in
-  identical, unchangedHeader, diffOpt
+        Changed, None in
+  change_status, unchangedHeader, diffOpt
 
-let eq_glob (a: global) (b: global) (cfgs : (cfg * cfg) option) = match a, b with
+let eq_glob (old: global) (current: global) (cfgs : (cfg * cfg) option) = match old, current with
   | GFun (f,_), GFun (g,_) -> eqF f g cfgs
-  | GVar (x, init_x, _), GVar (y, init_y, _) -> eq_varinfo x y, false, None (* ignore the init_info - a changed init of a global will lead to a different start state *)
-  | GVarDecl (x, _), GVarDecl (y, _) -> eq_varinfo x y, false, None
-  | _ -> ignore @@ Pretty.printf "Not comparable: %a and %a\n" Cil.d_global a Cil.d_global b; false, false, None
+  | GVar (x, init_x, _), GVar (y, init_y, _) -> unchanged_to_change_status (eq_varinfo x y), false, None (* ignore the init_info - a changed init of a global will lead to a different start state *)
+  | GVarDecl (x, _), GVarDecl (y, _) -> unchanged_to_change_status (eq_varinfo x y), false, None
+  | _ -> ignore @@ Pretty.printf "Not comparable: %a and %a\n" Cil.d_global old Cil.d_global current; Changed, false, None
 
 let compareCilFiles (oldAST: file) (newAST: file) =
   let cfgs = if GobConfig.get_string "incremental.compare" = "cfg"
@@ -79,10 +91,17 @@ let compareCilFiles (oldAST: file) (newAST: file) =
       (try
          let old_global = GlobalMap.find ident map in
          (* Do a (recursive) equal comparison ignoring location information *)
-         let identical, unchangedHeader, diff = eq_glob old_global global cfgs in
-         if identical
-         then changes.unchanged <- global :: changes.unchanged
-         else changes.changed <- {current = global; old = old_global; unchangedHeader; diff} :: changes.changed
+         let change_status, unchangedHeader, diff = eq_glob old_global global cfgs in
+         let append_to_changed () =
+           changes.changed <- {current = global; old = old_global; unchangedHeader; diff} :: changes.changed
+         in
+         match change_status with
+         | Changed -> append_to_changed ()
+         | Unchanged -> changes.unchanged <- global :: changes.unchanged
+         | ForceReanalyze f ->
+           changes.force_reanalyze <- VarinfoSet.add f.svar changes.force_reanalyze;
+           append_to_changed ();
+
        with Not_found -> ())
     with NoGlobalIdentifier _ -> () (* Global was no variable or function, it does not belong into the map *)  in
   let checkExists map global =

src/solvers/td3.ml

@@ -627,22 +627,39 @@ module WP =
             )
         in
 
+        let reluctant = GobConfig.get_bool "incremental.reluctant.on" in
+        let reanalyze_entry f =
+          (* destabilize the entry points of a changed function when reluctant is off,
+             or the function is to be force-reanalyzed  *)
+          (not reluctant) || CompareCIL.VarinfoSet.mem f.svar S.increment.changes.force_reanalyze
+        in
         let obsolete_ret = HM.create 103 in
         let obsolete_entry = HM.create 103 in
         let obsolete_prim = HM.create 103 in
+
+        (* When reluctant is on:
+           Only add function entry nodes to obsolete_entry if they are in force-reanalyze *)
         List.iter (fun f ->
-            mark_node obsolete_entry f (FunctionEntry f);
-            mark_node obsolete_ret f (Function f);
+            if reanalyze_entry f then
+              (* collect function entry for eager destabilization *)
+              mark_node obsolete_entry f (FunctionEntry f)
+            else
+              (* collect function return for reluctant analysis *)
+              mark_node obsolete_ret f (Function f)
           ) changed_funs;
-        List.iter (fun (f, pn, _) ->
-            List.iter (fun n ->
-                mark_node obsolete_prim f n
-              ) pn;
-            mark_node obsolete_ret f (Function f);
-          ) part_changed_funs;
+        (* Unknowns from partially changed functions need only to be collected for eager destabilization when reluctant is off *)
+        (* We utilize that force-reanalyzed functions are always considered as completely changed (and not partially changed) *)
+        if not reluctant then (
+          List.iter (fun (f, pn, _) ->
+              List.iter (fun n ->
+                  mark_node obsolete_prim f n
+                ) pn;
+              mark_node obsolete_ret f (Function f);
+            ) part_changed_funs;
+        );
 
         let old_ret = HM.create 103 in
-        if GobConfig.get_bool "incremental.reluctant.on" then (
+        if reluctant then (
           (* save entries of changed functions in rho for the comparison whether the result has changed after a function specific solve *)
           HM.iter (fun k v ->
               if HM.mem rho k then (
@@ -651,44 +668,43 @@ module WP =
                 HM.replace old_ret k (old_rho, old_infl)
               )
             ) obsolete_ret;
-        ) else (
-          (* If reluctant destabilization is turned off we need to destabilize all nodes in completely changed functions
-             and the primary obsolete nodes of partly changed functions *)
-          print_endline "Destabilizing changed functions and primary old nodes ...";
-          HM.iter (fun k _ ->
-              if HM.mem stable k then
-                destabilize k
-            ) obsolete_entry;
-          HM.iter (fun k _ ->
-              if HM.mem stable k then
-                destabilize k
-            ) obsolete_prim;
         );
 
+        if not (HM.is_empty obsolete_entry) || not (HM.is_empty obsolete_prim) then
+          print_endline "Destabilizing changed functions and primary old nodes ...";
+        HM.iter (fun k _ ->
+            if HM.mem stable k then
+              destabilize k
+          ) obsolete_entry;
+        HM.iter (fun k _ ->
+            if HM.mem stable k then
+              destabilize k
+          ) obsolete_prim;
+
         (* We remove all unknowns for program points in changed or removed functions from rho, stable, infl and wpoint *)
         let marked_for_deletion = HM.create 103 in
 
         let dummy_pseudo_return_node f =
           (* not the same as in CFG, but compares equal because of sid *)
           Node.Statement ({Cil.dummyStmt with sid = CfgTools.get_pseudo_return_id f})
         in
-        let add_nodes_of_fun (functions: fundec list) withEntry =
+        let add_nodes_of_fun (functions: fundec list) (withEntry: fundec -> bool) =
           let add_stmts (f: fundec) =
             List.iter (fun s ->
                 mark_node marked_for_deletion f (Statement s)
               ) f.sallstmts
           in
           List.iter (fun f ->
-              if withEntry then
+              if withEntry f then
                 mark_node marked_for_deletion f (FunctionEntry f);
               mark_node marked_for_deletion f (Function f);
               add_stmts f;
               mark_node marked_for_deletion f (dummy_pseudo_return_node f)
             ) functions;
         in
 
-        add_nodes_of_fun changed_funs (not (GobConfig.get_bool "incremental.reluctant.on"));
-        add_nodes_of_fun removed_funs true;
+        add_nodes_of_fun changed_funs reanalyze_entry;
+        add_nodes_of_fun removed_funs (fun _ -> true);
         (* it is necessary to remove all unknowns for changed pseudo-returns because they have static ids *)
         let add_pseudo_return f un =
           let pseudo = dummy_pseudo_return_node f in
@@ -798,7 +814,7 @@ module WP =
 
         (* TODO: reluctant doesn't call destabilize on removed functions or old copies of modified functions (e.g. after removing write), so those globals don't get restarted *)
 
-        if GobConfig.get_bool "incremental.reluctant.on" then (
+        if reluctant then (
           (* solve on the return node of changed functions. Only destabilize the function's return node if the analysis result changed *)
           print_endline "Separately solving changed functions...";
           let op = if GobConfig.get_string "incremental.reluctant.compare" = "leq" then S.Dom.leq else S.Dom.equal in

tests/incremental/01-force-reanalyze/01-int-reluctant.c

@@ -0,0 +1,17 @@
+#include<assert.h>
+
+int f(int in){
+  while(in < 17) {
+    in++;
+  }
+  assert(in == 17); //UNKNOWN
+  return in;
+}
+
+int main() {
+  int a = 0;
+  assert(a); // FAIL!
+  a = f(a);
+  assert(a == 17); //UNKNOWN
+  return 0;
+}

tests/incremental/01-force-reanalyze/01-int-reluctant.json

@@ -0,0 +1,21 @@
+{
+    "annotation" : {
+        "int" : {
+            "enabled" : true
+        }
+    },
+    "ana" : {
+        "int" : {
+            "refinement" : "fixpoint"
+        }
+    },
+    "incremental" : {
+        "force-reanalyze" : {
+            "funs": ["f"]
+        },
+        "reluctant" : {
+            "on": true
+        },
+        "verify": false
+    }
+}

tests/incremental/01-force-reanalyze/01-int-reluctant.patch

@@ -0,0 +1,37 @@
+diff --git tests/incremental/01-force-reanalyze/01-int-reluctant.c tests/incremental/01-force-reanalyze/01-int-reluctant.c
+index 38187f1c0..6126fe8cf 100644
+--- tests/incremental/01-force-reanalyze/01-int-reluctant.c
++++ tests/incremental/01-force-reanalyze/01-int-reluctant.c
+@@ -4,7 +4,7 @@ int f(int in){
+   while(in < 17) {
+     in++;
+   }
+-  assert(in == 17); //UNKNOWN
++  assert(in == 17);
+   return in;
+ }
+
+@@ -12,6 +12,6 @@ int main() {
+   int a = 0;
+   assert(a); // FAIL!
+   a = f(a);
+-  assert(a == 17); //UNKNOWN
++  assert(a == 17);
+   return 0;
+ }
+diff --git tests/incremental/01-force-reanalyze/01-int-reluctant.json tests/incremental/01-force-reanalyze/01-int-reluctant.json
+index d58c2254b..8834d182d 100644
+--- tests/incremental/01-force-reanalyze/01-int-reluctant.json
++++ tests/incremental/01-force-reanalyze/01-int-reluctant.json
+@@ -2,6 +2,11 @@
+     "annotation" : {
+         "int" : {
+             "enabled" : true
++        },
++        "goblint_precision": {
++            "interval": [
++                "f"
++            ]
+         }
+     },
+     "ana" : {

tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c

@@ -0,0 +1,17 @@
+#include<assert.h>
+
+int f(int in){
+  while(in < 17) {
+    in++;
+  }
+  assert(in == 17); //UNKNOWN
+  return in;
+}
+
+int main() {
+  int a = 0;
+  assert(a); // FAIL!
+  a = f(a);
+  assert(a == 17); //UNKNOWN
+  return 0;
+}

tests/incremental/03-precision-annotation/02-reluctant-int-annotation.json

@@ -0,0 +1,18 @@
+{
+    "annotation": {
+        "int": {
+            "enabled": true
+        }
+    },
+    "ana": {
+        "int": {
+            "refinement": "fixpoint"
+        }
+    },
+    "incremental": {
+        "reluctant": {
+            "on": true
+        },
+        "verify": false
+    }
+}

tests/incremental/03-precision-annotation/02-reluctant-int-annotation.patch

@@ -0,0 +1,25 @@
+diff --git tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c
+index 38187f1c0..698e45b62 100644
+--- tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c
++++ tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c
+@@ -1,10 +1,11 @@
+ #include<assert.h>
+
++int f(int in) __attribute__ ((goblint_precision("def_exc", "interval")));
+ int f(int in){
+   while(in < 17) {
+     in++;
+   }
+-  assert(in == 17); //UNKNOWN
++  assert(in == 17);
+   return in;
+ }
+
+@@ -12,6 +13,6 @@ int main() {
+   int a = 0;
+   assert(a); // FAIL!
+   a = f(a);
+-  assert(a == 17); //UNKNOWN
++  assert(a == 17);
+   return 0;
+ }

tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.c

@@ -0,0 +1,24 @@
+#include<assert.h>
+
+typedef int int_to_int_fun (int);
+
+int f(int in){
+  while(in < 17) {
+    in++;
+  }
+  assert(in == 17); //UNKNOWN
+  return in;
+}
+
+int_to_int_fun *get_fun(){
+  return &f;
+}
+
+int main() {
+  int_to_int_fun *fun = get_fun();
+  int a = 0;
+  assert(a); // FAIL!
+  a = fun(a);
+  assert(a == 17); //UNKNOWN
+  return 0;
+}