Fix Unreached Fixpoint in Reluctant Incremental Analysis

conf/zstd-race.json

@@ -41,9 +41,6 @@
     }
   },
   "incremental": {
-    "reluctant": {
-      "compare": "leq"
-    },
     "restart": {
       "sided": {
         "enabled": false

src/solvers/td3.ml

@@ -721,15 +721,13 @@ module Base =
         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
+          HM.iter (fun x (old_rho, old_infl) -> HM.replace rho x old_rho; HM.replace infl x old_infl) old_ret;
           HM.iter (fun x (old_rho, old_infl) ->
               ignore @@ Pretty.printf "test for %a\n" Node.pretty_trace (S.Var.node x);
               solve x Widen;
-              if not (op (HM.find rho x) old_rho) then (
-                print_endline "Destabilization required...";
-                HM.replace infl x old_infl;
-                destabilize x;
-                HM.replace stable x ()
+              VS.iter (fun k -> ignore @@ Pretty.printf "in infl after solving: %a\n" Node.pretty_trace (S.Var.node k)) (HM.find_default infl x VS.empty);
+              if not (S.Dom.equal (HM.find rho x) old_rho) then (
+                print_endline "Further destabilization happened ...";
               )
               else (
                 print_endline "Destabilization not required...";

src/util/options.schema.json

@@ -1053,14 +1053,6 @@
                 "Destabilize nodes in changed functions reluctantly",
               "type": "boolean",
               "default": false
-            },
-            "compare": {
-              "title": "incremental.reluctant.compare",
-              "description":
-                "In order to reuse the function's old abstract value the new abstract value must be leq (focus on efficiency) or equal (focus on precision) compared to the old.",
-              "type": "string",
-              "enum": ["leq", "equal"],
-              "default": "equal"
             }
           },
           "additionalProperties": false

tests/incremental/00-basic/15-reluctant-test.c

@@ -0,0 +1,34 @@
+#include <goblint.h>
+// This test used to resulted in an unreached fixpoint in the incremental implementation.
+
+int g = 3;
+
+int bar(){
+	int x = foo();
+	return x;
+}
+
+int foo(){
+	int top;
+	int r = 0;
+	if(top){
+		r = g;
+	} else {
+		// bar();
+		// r = 5;
+	}
+	return r;
+}
+
+int main(){
+	int x;
+
+	x = foo();
+	if(x == 5){
+		g = 4;
+		int i = bar();
+
+
+	}
+	return x;
+}

tests/incremental/00-basic/15-reluctant-test.json

@@ -0,0 +1,15 @@
+{
+	"ana": {
+		"int": {
+			"enums": true
+		}
+	},
+	"incremental": {
+		"reluctant": {
+			"enabled": true
+		}
+	},
+	"exp": {
+		"earlyglobs": true
+	}
+}

tests/incremental/00-basic/15-reluctant-test.patch

@@ -0,0 +1,22 @@
+--- tests/incremental/00-basic/15-reluctant-test.c
++++ tests/incremental/00-basic/15-reluctant-test.c
+@@ -14,8 +14,8 @@ int foo(){
+ 	if(top){
+ 		r = g;
+ 	} else {
+-		// bar();
+-		// r = 5;
++		bar();
++		r = 5;
+ 	}
+ 	return r;
+ }
+@@ -28,7 +28,7 @@ int main(){
+ 		g = 4;
+ 		int i = bar();
+
+-
++    __goblint_check(i == 4); //UNKNOWN!
+ 	}
+ 	return x;
+ }