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

src/solvers/td3.ml

@@ -16,6 +16,8 @@ open Messages
 open CompareCIL
 open Cil
 
+module StringSet = Set.Make(Printable.Strings)
+
 module WP =
   functor (Arg: IncrSolverArg) ->
   functor (S:EqConstrSys) ->
@@ -627,12 +629,27 @@ module WP =
             )
         in
 
+        let force_reanalyze = StringSet.of_list @@ GobConfig.get_string_list "incremental.force-reanalyze.funs" in
+        let eager = (not (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  *)
+          eager || StringSet.mem f.svar.vname 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 ->
@@ -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

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;
+ }