Add option for manual restarting of globals

src/framework/analyses.ml

@@ -452,13 +452,18 @@ type analyzed_data = {
 type increment_data = {
   old_data: analyzed_data option;
   new_file: Cil.file;
-  changes: CompareCIL.change_info
+  changes: CompareCIL.change_info;
+
+  (* Globals for whiche the constraint
+     system unknowns should be restarted *)
+  restarting: VarQuery.t list;
 }
 
 let empty_increment_data file = {
   old_data = None;
   new_file = file;
-  changes = CompareCIL.empty_change_info ()
+  changes = CompareCIL.empty_change_info ();
+  restarting = []
 }
 
 (** A side-effecting system. *)

src/framework/varQuery.ml

@@ -4,3 +4,35 @@ type t =
 [@@deriving ord]
 
 type 'v f = 'v -> unit
+
+let varinfo_from_global (g : Cil.global) : Cil.varinfo option = match g with
+  | GFun (f, _) -> Some f.svar
+  | GVar (v, _, _) -> Some v
+  | GVarDecl (v, _) -> Some v
+  | _ -> None
+
+let varquery_from_global (g : Cil.global) : t option = match g with
+  | GFun (f, _) -> Some (Node {node = FunctionEntry f; fundec = Some f})
+  | GVar (v, _, _) -> Some (Global v)
+  | GVarDecl (v, _) -> Some (Global v)
+  | _ -> None
+
+let varqueries_from_names (file: Cil.file) (names: string list): t list * string list =
+  let module SM = Set.Make(Printable.Strings) in
+  let set = SM.of_list names in
+
+  (* Find list of [Cil.global]s that have one of the queried names, and a set of the found names *)
+  let globals, matched =
+    Cil.foldGlobals file (fun ((globs, matched) as acc) g ->
+        match varinfo_from_global g, varquery_from_global g with
+        | Some v, Some vq ->
+          begin match SM.mem v.vname set  with
+            | true -> (vq::globs, SM.add v.vname matched)
+            | _ -> acc
+          end
+        | None, None -> acc
+        | _, _ -> assert false
+      ) ([], SM.empty) in
+  (* List of queried but not found names *)
+  let unmatched = List.filter (fun s -> not @@ SM.mem s matched) names in
+  globals, unmatched

src/framework/varQuery.mli

@@ -0,0 +1,10 @@
+type t =
+    Global of Cil.varinfo
+  | Node of { node : Node.t; fundec : Cil.fundec option; }
+val compare : t -> t -> int
+type 'v f = 'v -> unit
+
+(** Takes a [Cil.file] and a list of names of globals.contents
+    Returns a list of [VarQuery.t]s of globals whose [vname] is contained in the argument list,
+    and the list of names for which no global with the name could be found. *)
+val varqueries_from_names : Cil.file -> string list -> t list * string list

src/incremental/compareCIL.ml

@@ -23,7 +23,8 @@ type change_info = {
   mutable added: global list
 }
 
-let empty_change_info () : change_info = {added = []; removed = []; changed = []; unchanged = []}
+let empty_change_info () : change_info =
+  {added = []; removed = []; changed = []; unchanged = []}
 
 (* 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

src/maingoblint.ml

@@ -433,7 +433,8 @@ let check_arguments () =
   if get_bool "ana.base.context.int" && not (get_bool "ana.base.context.non-ptr") then (set_bool "ana.base.context.int" false; warn "ana.base.context.int implicitly disabled by ana.base.context.non-ptr");
   (* order matters: non-ptr=false, int=true -> int=false cascades to interval=false with warning *)
   if get_bool "ana.base.context.interval" && not (get_bool "ana.base.context.int") then (set_bool "ana.base.context.interval" false; warn "ana.base.context.interval implicitly disabled by ana.base.context.int");
-  if get_bool "incremental.only-rename" then (set_bool "incremental.load" true; warn "incremental.only-rename implicitly activates incremental.load. Previous AST is loaded for diff and rename, but analyis results are not reused.")
+  if get_bool "incremental.only-rename" then (set_bool "incremental.load" true; warn "incremental.only-rename implicitly activates incremental.load. Previous AST is loaded for diff and rename, but analyis results are not reused.");
+  if get_bool "incremental.restart.sided.enabled" && get_string_list "incremental.restart.list" <> [] then warn "Passing a non-empty list to incremental.restart.list (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated."
 
 let handle_extraspecials () =
   let funs = get_string_list "exp.extraspecials" in
@@ -443,19 +444,30 @@ let handle_extraspecials () =
 let diff_and_rename current_file =
   (* Create change info, either from old results, or from scratch if there are no previous results. *)
   let change_info: Analyses.increment_data =
+    let warn m = eprint_color ("{yellow}Warning: "^m) in
     if GobConfig.get_bool "incremental.load" && not (Serialize.results_exist ()) then begin
-      let warn m = eprint_color ("{yellow}Warning: "^m) in
       warn "incremental.load is activated but no data exists that can be loaded."
     end;
-    let (changes, old_file, version_map, max_ids) =
+    let (changes, restarting, old_file, version_map, max_ids) =
       if Serialize.results_exist () && GobConfig.get_bool "incremental.load" then begin
         let old_file = Serialize.load_data Serialize.CilFile in
         let (version_map, changes, max_ids) = VersionLookup.load_and_update_map old_file current_file in
         let max_ids = UpdateCil.update_ids old_file max_ids current_file version_map changes in
-        (changes, Some old_file, version_map, max_ids)
+        let restarting = GobConfig.get_string_list "incremental.restart.list" in
+
+        let restarting, not_found = VarQuery.varqueries_from_names current_file restarting in
+
+        if not (List.is_empty not_found) then begin
+          List.iter
+            (fun s ->
+              warn @@ "Should restart " ^ s ^ " but no such global could not be found in the CIL-file.")
+            not_found;
+          flush stderr
+        end;
+        (changes, restarting, Some old_file, version_map, max_ids)
       end else begin
         let (version_map, max_ids) = VersionLookup.create_map current_file in
-        (CompareCIL.empty_change_info (), None, version_map, max_ids)
+        (CompareCIL.empty_change_info (), [], None, version_map, max_ids)
       end
     in
     let solver_data = if Serialize.results_exist () && GobConfig.get_bool "incremental.load" && not (GobConfig.get_bool "incremental.only-rename")
@@ -470,7 +482,7 @@ let diff_and_rename current_file =
       | Some cil_file, Some solver_data -> Some ({cil_file; solver_data}: Analyses.analyzed_data)
       | _, _ -> None
     in
-    {Analyses.changes = changes; old_data; new_file = current_file}
+    {Analyses.changes = changes; restarting; old_data; new_file = current_file}
   in change_info
 
 let () = (* signal for printing backtrace; other signals in Generic.SolverStats and Timeout *)
@@ -503,7 +515,11 @@ let main () =
       )
     in
     if get_bool "server.enabled" then Server.start file do_analyze else (
-      let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else Analyses.empty_increment_data file in
+      let changeInfo =
+        if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then
+          diff_and_rename file
+        else
+          Analyses.empty_increment_data file in
       file|> do_analyze changeInfo;
       do_stats ();
       do_html_output ();

src/solvers/td3.ml

@@ -719,6 +719,44 @@ module WP =
             ) marked_for_deletion
         );
 
+        (* [destabilize_leaf] is meant for restarting of globals selected by the user. *)
+        (* Must be called on a leaf! *)
+        let destabilize_leaf (x : S.v) =
+          let destab_side_dep (x : S.v) =
+            let w = HM.find_default side_dep x VS.empty in
+            if not (VS.is_empty w) then (
+              HM.remove side_dep x;
+              (* add side_dep to front to prevent them from being aborted *)
+              destabilize_front ~front:true x w;
+              (* destabilize side dep to redo side effects *)
+              VS.iter (fun y ->
+                  if tracing then trace "sol2" "destabilize_leaf %a side_dep %a\n" S.Var.pretty_trace x S.Var.pretty_trace y;
+                  if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
+                  HM.remove stable y;
+                  HM.remove superstable y;
+                  destabilize_normal y
+                ) w
+            )
+          in
+          restart_leaf x;
+          destab_side_dep x;
+          destabilize_normal x
+
+        in
+        let globals_to_restart = S.increment.restarting in
+        let get x = try HM.find rho x with Not_found -> S.Dom.bot () in
+
+        List.iter
+          (fun g ->
+             S.iter_vars get g
+               (fun v ->
+                  if S.system v <> None then
+                    ignore @@ Pretty.printf "Trying to restart non-leaf unknown %a. This has no effect.\n" S.Var.pretty_trace v
+                  else if HM.mem stable v then
+                    destabilize_leaf v)
+          )
+          globals_to_restart;
+
         let restart_and_destabilize x = (* destabilize_with_side doesn't restart x itself *)
           restart_leaf x;
           destabilize x

src/util/options.schema.json

@@ -902,7 +902,9 @@
               "description":
                 "List of functions that are to be re-analayzed from scratch",
               "type": "array",
-              "items": { "type": "string" },
+              "items": {
+                "type": "string"
+              },
               "default": []
             }
           },
@@ -930,6 +932,15 @@
                 }
               },
               "additionalProperties": false
+            },
+            "list": {
+              "title": "incremental.restart.list",
+              "description": "List of globals variables and function definitions for which the analysis is to be restarted.",
+              "type": "array",
+              "items": {
+                "type": "string"
+              },
+              "default": []
             }
           },
           "additionalProperties": false

src/util/server.ml

@@ -113,7 +113,8 @@ let analyze ?(reset=false) ({ file; do_analyze; _ }: t)=
     | Some solver_data ->
       let changes = CompareCIL.compareCilFiles file file in
       let old_data = Some { Analyses.cil_file = file; solver_data } in
-      { Analyses.changes; old_data; new_file = file }, false
+      (* TODO: get globals for restarting from config *)
+      { Analyses.changes; old_data; new_file = file; restarting = [] }, false
     | _ -> Analyses.empty_increment_data file, true
   in
   GobConfig.set_bool "incremental.load" (not fresh);

tests/incremental/04-manual-restart/01-restart_manual_simple.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int g = 4;
+
+int main() {
+    int x = g;
+    assert(x == 4);
+    return 0;
+}

tests/incremental/04-manual-restart/01-restart_manual_simple.json

@@ -0,0 +1,13 @@
+{
+    "exp": {
+        "earlyglobs": true
+    },
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            },
+            "list": []
+        }
+    }
+}

tests/incremental/04-manual-restart/01-restart_manual_simple.patch

@@ -0,0 +1,29 @@
+diff --git tests/incremental/04-manual-restart/01-restart_manual_simple.c tests/incremental/04-manual-restart/01-restart_manual_simple.c
+index cbfb0ba70..aa83393ac 100644
+--- tests/incremental/04-manual-restart/01-restart_manual_simple.c
++++ tests/incremental/04-manual-restart/01-restart_manual_simple.c
+@@ -1,9 +1,9 @@
+ #include <assert.h>
+
+-int g = 4;
++int g = 5;
+
+ int main() {
+     int x = g;
+-    assert(x == 4);
++    assert(x == 4); //FAIL
+     return 0;
+ }
+diff --git tests/incremental/04-manual-restart/01-restart_manual_simple.json tests/incremental/04-manual-restart/01-restart_manual_simple.json
+index dbdb1d651..d66a6cf36 100644
+--- tests/incremental/04-manual-restart/01-restart_manual_simple.json
++++ tests/incremental/04-manual-restart/01-restart_manual_simple.json
+@@ -7,7 +7,7 @@
+             "sided": {
+                 "enabled": false
+             },
+-            "list": []
++            "list": ["g"]
+         }
+     }
+ }

tests/incremental/04-manual-restart/02-read_write_global.c

@@ -0,0 +1,16 @@
+int g = 0;
+
+void foo(){
+    g = 1;
+}
+
+void bar(){
+    int x = g;
+    assert(x % 2 == 0); // UNKNOWN (imprecision caused by earlyglobs)
+}
+
+int main(){
+    foo();
+    bar();
+    return 0;
+}

tests/incremental/04-manual-restart/02-read_write_global.json

@@ -0,0 +1,19 @@
+{
+    "exp": {
+        "earlyglobs": true
+    },
+    "ana": {
+        "int": {
+            "interval": true,
+            "congruence": true
+        }
+    },
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            },
+            "list": []
+        }
+    }
+}

tests/incremental/04-manual-restart/02-read_write_global.patch

@@ -0,0 +1,34 @@
+diff --git tests/incremental/04-manual-restart/02-read_write_global.c tests/incremental/04-manual-restart/02-read_write_global.c
+index 8a93caabe..521322dd0 100644
+--- tests/incremental/04-manual-restart/02-read_write_global.c
++++ tests/incremental/04-manual-restart/02-read_write_global.c
+@@ -1,12 +1,12 @@
+ int g = 0;
+
+ void foo(){
+-    g = 1;
++    g = 2;
+ }
+
+ void bar(){
+     int x = g;
+-    assert(x % 2 == 0); // UNKNOWN (imprecision caused by earlyglobs)
++    assert(x % 2 == 0);
+ }
+
+ int main(){
+diff --git tests/incremental/04-manual-restart/02-read_write_global.json tests/incremental/04-manual-restart/02-read_write_global.json
+index 33dd19da4..0820029df 100644
+--- tests/incremental/04-manual-restart/02-read_write_global.json
++++ tests/incremental/04-manual-restart/02-read_write_global.json
+@@ -13,7 +13,9 @@
+             "sided": {
+                 "enabled": false
+             },
+-            "list": []
++            "list": [
++                "g"
++            ]
+         }
+     }
+ }

tests/incremental/04-manual-restart/03-partial_contexts.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+int foo(int x){
+    return x;
+}
+
+int main(){
+    int x = 12;
+    int y = foo(x);
+    assert(x == y);
+    return 0;
+}

tests/incremental/04-manual-restart/03-partial_contexts.json

@@ -0,0 +1,17 @@
+{
+    "ana": {
+        "base": {
+            "context": {
+                "int": false
+            }
+        }
+    },
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            },
+            "list": []
+        }
+    }
+}