From 4b7df8bc30f0e5c8e65a3708c3642a9eebee8e45 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 09:51:58 +0100
Subject: [PATCH 01/22] Add option for restarting unknowns belonging to global
 variables selected by the user.

Adds the option incremental.restart_globs.globs, where a user can provide a list of global variables which should be restarted.
---
 src/framework/analyses.ml     |  9 +++++++--
 src/incremental/compareCIL.ml |  3 ++-
 src/maingoblint.ml            | 23 ++++++++++++++-------
 src/solvers/td3.ml            | 38 +++++++++++++++++++++++++++++++++++
 src/util/cilfacade.ml         | 35 ++++++++++++++++++++++++++++++++
 src/util/options.schema.json  | 20 +++++++++++++++++-
 src/util/server.ml            |  3 ++-
 7 files changed, 119 insertions(+), 12 deletions(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index eefb414596..10f4582e9a 100644
--- a/src/framework/analyses.ml
+++ b/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: Cil.global 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. *)
diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index 2ce81948b7..470a941ff0 100644
--- a/src/incremental/compareCIL.ml
+++ b/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
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index f2e8d685c3..7795703ff6 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -433,8 +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_globs.globs" <> [] then (warn "Passing a non-empty list to incremental.restart_globs.globs (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated. Aborting."; exit 5 )
 let handle_extraspecials () =
   let funs = get_string_list "exp.extraspecials" in
   LibraryFunctions.add_lib_funs funs
@@ -447,15 +447,20 @@ let diff_and_rename current_file =
       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)
+        print_endline "trying to get the string list";
+        let restarting = GobConfig.get_string_list "incremental.restart_globs.globs" in
+        print_endline "retrieved list of options!";
+        (* TODO: Check whether passing current_file is correct, or whether we need the version map. *)
+        let restarting = BatList.filter_map (Cilfacade.global_from_name current_file) restarting in
+        (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 +475,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 +508,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 ();
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 77636ab07c..e637ecd9c1 100644
--- a/src/solvers/td3.ml
+++ b/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) =
+            match HM.find_option side_dep x with
+            | Some w ->
+              HM.remove side_dep x;
+              VS.iter (fun y ->
+                  HM.remove stable y;
+                  destabilize y;
+                ) w;
+            | None ->
+              ignore @@ Pretty.printf
+                "Could not find globals in side_dep, so side_dep %a is not restarted.\n"
+                S.Var.pretty_trace x
+          in
+          destab_side_dep x;
+          destabilize x;
+          restart_leaf 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 ->
+            (* All gs arriving here should yield Some varinfo. *)
+            let g = Option.get @@ Cilfacade.varinfo_from_global g in
+            ignore @@ Pretty.printf "Restarting global %s.\n" g.vname;
+            S.iter_vars
+              get
+              (Global g)
+              (fun v ->
+                if HM.mem stable v then begin
+                  destabilize_leaf v;
+                end
+            )
+          )
+          globals_to_restart;
+
         let restart_and_destabilize x = (* destabilize_with_side doesn't restart x itself *)
           restart_leaf x;
           destabilize x
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 1742ac86ff..f138fb5f25 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -21,6 +21,41 @@ let rec get_labelsLoc = function
     else
       loc
 
+module String = struct
+  include String
+  let hash = Hashtbl.hash
+end
+
+module SM = Hashtbl.Make(String)
+let varinfo_map: Cil.global SM.t option ref = ref None
+
+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
+  | _ ->
+    Messages.warn
+      ~category:MessageCategory.Analyzer
+      "Not considering global cil object %a for restarting."
+      Cil.d_global g;
+    None
+
+let init_hash_map (file: Cil.file): Cil.global SM.t =
+  let vm = SM.create 113 in
+  varinfo_map := Some vm;
+  Cil.iterGlobals file
+    (fun v ->
+      match varinfo_from_global v with
+      | Some vi -> SM.add vm vi.vname v
+      | None -> ());
+  vm
+
+let global_from_name (file: Cil.file) (name: string) =
+  let vm = (match !varinfo_map with
+    | None -> init_hash_map file
+    | Some vm -> vm) in
+  SM.find_opt vm name
+
 let get_stmtkindLoc = Cil.get_stmtLoc (* CIL has a confusing name for this function *)
 
 let get_stmtLoc stmt =
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 070daf4cce..2d57ead24c 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -902,7 +902,25 @@
               "description":
                 "List of functions that are to be re-analayzed from scratch",
               "type": "array",
-              "items": { "type": "string" },
+              "items": {
+                "type": "string"
+              },
+              "default": []
+            }
+          },
+          "additionalProperties": false
+        },
+        "restart_globs": {
+          "title": "incremental.restart_globs",
+          "type": "object",
+          "properties": {
+            "globs": {
+              "title": "incremental.restart_globs.globs",
+              "description": "List of globals for which the analysis is to be restarted.",
+              "type": "array",
+              "items": {
+                "type": "string"
+              },
               "default": []
             }
           },
diff --git a/src/util/server.ml b/src/util/server.ml
index a47e6a1a02..6ea9af6979 100644
--- a/src/util/server.ml
+++ b/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);

From b7d195e7f87bb46b25ee486cf18e88014f2b8b3c Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 10:12:57 +0100
Subject: [PATCH 02/22] Add test for manual restarting

---
 .../01-restart_manual_simple.c                |  9 ++++++
 .../01-restart_manual_simple.json             | 15 +++++++++
 .../01-restart_manual_simple.patch            | 31 +++++++++++++++++++
 3 files changed, 55 insertions(+)
 create mode 100644 tests/incremental/04-manual-restart/01-restart_manual_simple.c
 create mode 100644 tests/incremental/04-manual-restart/01-restart_manual_simple.json
 create mode 100644 tests/incremental/04-manual-restart/01-restart_manual_simple.patch

diff --git a/tests/incremental/04-manual-restart/01-restart_manual_simple.c b/tests/incremental/04-manual-restart/01-restart_manual_simple.c
new file mode 100644
index 0000000000..cbfb0ba70c
--- /dev/null
+++ b/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;
+}
diff --git a/tests/incremental/04-manual-restart/01-restart_manual_simple.json b/tests/incremental/04-manual-restart/01-restart_manual_simple.json
new file mode 100644
index 0000000000..582ede8df1
--- /dev/null
+++ b/tests/incremental/04-manual-restart/01-restart_manual_simple.json
@@ -0,0 +1,15 @@
+{
+    "exp": {
+        "earlyglobs": true
+    },
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        },
+        "restart_globs": {
+            "globs": []
+        }
+    }
+}
diff --git a/tests/incremental/04-manual-restart/01-restart_manual_simple.patch b/tests/incremental/04-manual-restart/01-restart_manual_simple.patch
new file mode 100644
index 0000000000..483ebe1bc1
--- /dev/null
+++ b/tests/incremental/04-manual-restart/01-restart_manual_simple.patch
@@ -0,0 +1,31 @@
+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 582ede8df..51d6d31b2 100644
+--- tests/incremental/04-manual-restart/01-restart_manual_simple.json
++++ tests/incremental/04-manual-restart/01-restart_manual_simple.json
+@@ -9,7 +9,9 @@
+             }
+         },
+         "restart_globs": {
+-            "globs": []
++            "globs": [
++                "g"
++            ]
+         }
+     }
+ }

From 37aefd6505224b8d6347369f222b70f7dec09934 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 10:40:34 +0100
Subject: [PATCH 03/22] Add test for manual restarting of globals when reads
 and writes occur in different functions

---
 .../04-manual-restart/02-read_write_global.c  | 16 ++++++++++
 .../02-read_write_global.json                 | 21 ++++++++++++
 .../02-read_write_global.patch                | 32 +++++++++++++++++++
 3 files changed, 69 insertions(+)
 create mode 100644 tests/incremental/04-manual-restart/02-read_write_global.c
 create mode 100644 tests/incremental/04-manual-restart/02-read_write_global.json
 create mode 100644 tests/incremental/04-manual-restart/02-read_write_global.patch

diff --git a/tests/incremental/04-manual-restart/02-read_write_global.c b/tests/incremental/04-manual-restart/02-read_write_global.c
new file mode 100644
index 0000000000..257aa969ac
--- /dev/null
+++ b/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
+}
+
+int main(){
+    foo();
+    bar();
+    return 0;
+}
diff --git a/tests/incremental/04-manual-restart/02-read_write_global.json b/tests/incremental/04-manual-restart/02-read_write_global.json
new file mode 100644
index 0000000000..8685ac3b70
--- /dev/null
+++ b/tests/incremental/04-manual-restart/02-read_write_global.json
@@ -0,0 +1,21 @@
+{
+    "exp": {
+        "earlyglobs": true
+    },
+    "ana": {
+        "int": {
+            "interval": true,
+            "congruence": true
+        }
+    },
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        },
+        "restart_globs": {
+            "globs": []
+        }
+    }
+}
diff --git a/tests/incremental/04-manual-restart/02-read_write_global.patch b/tests/incremental/04-manual-restart/02-read_write_global.patch
new file mode 100644
index 0000000000..92893d37c5
--- /dev/null
+++ b/tests/incremental/04-manual-restart/02-read_write_global.patch
@@ -0,0 +1,32 @@
+diff --git tests/incremental/04-manual-restart/02-read_write_global.c tests/incremental/04-manual-restart/02-read_write_global.c
+index 257aa969a..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
++    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 8685ac3b7..acf0568c8 100644
+--- tests/incremental/04-manual-restart/02-read_write_global.json
++++ tests/incremental/04-manual-restart/02-read_write_global.json
+@@ -15,7 +15,7 @@
+             }
+         },
+         "restart_globs": {
+-            "globs": []
++            "globs": ["g"]
+         }
+     }
+ }

From 1e20f209bbac26d0bb4b425c066642021f97990b Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 11:11:52 +0100
Subject: [PATCH 04/22] Change global_from_name to globals_from_names working
 on a list, remove usage of a mutable hashtable

---
 src/maingoblint.ml    |  2 +-
 src/util/cilfacade.ml | 41 ++++++++++++++++-------------------------
 2 files changed, 17 insertions(+), 26 deletions(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 7795703ff6..1a5e4159c4 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -456,7 +456,7 @@ let diff_and_rename current_file =
         let restarting = GobConfig.get_string_list "incremental.restart_globs.globs" in
         print_endline "retrieved list of options!";
         (* TODO: Check whether passing current_file is correct, or whether we need the version map. *)
-        let restarting = BatList.filter_map (Cilfacade.global_from_name current_file) restarting in
+        let restarting = Cilfacade.globals_from_names current_file restarting in
         (changes, restarting, Some old_file, version_map, max_ids)
       end else begin
         let (version_map, max_ids) = VersionLookup.create_map current_file in
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index f138fb5f25..af2ea23ab8 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -26,35 +26,26 @@ module String = struct
   let hash = Hashtbl.hash
 end
 
-module SM = Hashtbl.Make(String)
-let varinfo_map: Cil.global SM.t option ref = ref None
-
 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
-  | _ ->
-    Messages.warn
-      ~category:MessageCategory.Analyzer
-      "Not considering global cil object %a for restarting."
-      Cil.d_global g;
-    None
-
-let init_hash_map (file: Cil.file): Cil.global SM.t =
-  let vm = SM.create 113 in
-  varinfo_map := Some vm;
-  Cil.iterGlobals file
-    (fun v ->
-      match varinfo_from_global v with
-      | Some vi -> SM.add vm vi.vname v
-      | None -> ());
-  vm
-
-let global_from_name (file: Cil.file) (name: string) =
-  let vm = (match !varinfo_map with
-    | None -> init_hash_map file
-    | Some vm -> vm) in
-  SM.find_opt vm name
+  | _ -> None
+
+let globals_from_names (file: Cil.file) (names: string list): global list =
+  let module SM = Set.Make(String) in
+  let set = SM.of_list names in
+  let globals =
+    Cil.foldGlobals file (fun acc g ->
+      match varinfo_from_global g with
+        | Some v ->
+          if SM.mem v.vname set then
+            g::acc
+          else
+            acc
+        | None -> acc
+      ) [] in
+  globals
 
 let get_stmtkindLoc = Cil.get_stmtLoc (* CIL has a confusing name for this function *)
 

From c5015757ed781c5b0300b6535979178fb4372cc9 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 11:35:31 +0100
Subject: [PATCH 05/22] Issue warning if both automatic and manual restarting
 are active instead of aborting

---
 src/maingoblint.ml | 3 ++-
 src/solvers/td3.ml | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 1a5e4159c4..28606da239 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -434,7 +434,8 @@ let check_arguments () =
   (* 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.restart.sided.enabled" && get_string_list "incremental.restart_globs.globs" <> [] then (warn "Passing a non-empty list to incremental.restart_globs.globs (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated. Aborting."; exit 5 )
+  if get_bool "incremental.restart.sided.enabled" && get_string_list "incremental.restart_globs.globs" <> [] then warn "Passing a non-empty list to incremental.restart_globs.globs (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated."
+
 let handle_extraspecials () =
   let funs = get_string_list "exp.extraspecials" in
   LibraryFunctions.add_lib_funs funs
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index e637ecd9c1..73ceb2cd45 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -736,7 +736,7 @@ module WP =
                 S.Var.pretty_trace x
           in
           destab_side_dep x;
-          destabilize x;
+          destabilize_normal x;
           restart_leaf x
         in
         let globals_to_restart = S.increment.restarting in

From f9d01242de7d6888e732b7b0e4900b79ad79ca57 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@yahoo.de>
Date: Thu, 27 Jan 2022 11:38:53 +0100
Subject: [PATCH 06/22] Remove unnecessary debug printout

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 src/maingoblint.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 28606da239..7cd01b74cf 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -453,9 +453,7 @@ let diff_and_rename current_file =
         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
-        print_endline "trying to get the string list";
         let restarting = GobConfig.get_string_list "incremental.restart_globs.globs" in
-        print_endline "retrieved list of options!";
         (* TODO: Check whether passing current_file is correct, or whether we need the version map. *)
         let restarting = Cilfacade.globals_from_names current_file restarting in
         (changes, restarting, Some old_file, version_map, max_ids)

From 253a44c90254e65e65c565cbde27ab1e459e86eb Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 13:34:52 +0100
Subject: [PATCH 07/22] Add logic for destabilize_front, handling superstable
 to destabilize_leaf.

Copied and adapted code from destabilize_with_side
---
 src/solvers/td3.ml | 29 ++++++++++++++++++-----------
 1 file changed, 18 insertions(+), 11 deletions(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 73ceb2cd45..c7788a8332 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -723,21 +723,28 @@ module WP =
         (* Must be called on a leaf! *)
         let destabilize_leaf (x : S.v) =
           let destab_side_dep (x : S.v) =
-            match HM.find_option side_dep x with
-            | Some w ->
+            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;
-                  destabilize y;
-                ) w;
-            | None ->
-              ignore @@ Pretty.printf
-                "Could not find globals in side_dep, so side_dep %a is not restarted.\n"
-                S.Var.pretty_trace x
+                  HM.remove superstable y;
+                  destabilize y
+                ) w
+            )
           in
-          destab_side_dep x;
-          destabilize_normal x;
-          restart_leaf x
+          if Node.equal (S.Var.node x) (Function Cil.dummyFunDec) then (
+            restart_leaf x;
+            destab_side_dep x;
+            destabilize_normal x
+          ) else (
+            ignore @@ Pretty.printf "Trying to restart %a which does not describe a global variable." S.Var.pretty_trace 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

From 7fcc4b26211630d2b1af724e64ec05a2b999daf9 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 13:36:13 +0100
Subject: [PATCH 08/22] Reformat code for user-triggered global restarting

---
 src/solvers/td3.ml | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index c7788a8332..e555732012 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -750,17 +750,16 @@ module WP =
         let get x = try HM.find rho x with Not_found -> S.Dom.bot () in
         List.iter
           (fun g ->
-            (* All gs arriving here should yield Some varinfo. *)
-            let g = Option.get @@ Cilfacade.varinfo_from_global g in
-            ignore @@ Pretty.printf "Restarting global %s.\n" g.vname;
-            S.iter_vars
-              get
-              (Global g)
-              (fun v ->
-                if HM.mem stable v then begin
-                  destabilize_leaf v;
-                end
-            )
+             (* All gs arriving here should yield Some varinfo. *)
+             let g = Option.get @@ Cilfacade.varinfo_from_global g in
+             S.iter_vars
+               get
+               (Global g)
+               (fun v ->
+                  if HM.mem stable v then begin
+                    destabilize_leaf v;
+                  end
+               )
           )
           globals_to_restart;
 

From 83dab6469277f77bddbfb4d5b3072f9b53b7b67c Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 14:24:27 +0100
Subject: [PATCH 09/22] Collect varinfos instead of Cil.globals for manually
 restarted globals

---
 src/framework/analyses.ml | 2 +-
 src/maingoblint.ml        | 3 +--
 src/solvers/td3.ml        | 6 +-----
 src/util/cilfacade.ml     | 8 +++++---
 4 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 10f4582e9a..d1eb1e1f46 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -456,7 +456,7 @@ type increment_data = {
 
   (* Globals for whiche the constraint
      system unknowns should be restarted *)
-  restarting: Cil.global list;
+  restarting: Cil.varinfo list;
 }
 
 let empty_increment_data file = {
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 7cd01b74cf..9ece899a60 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -454,8 +454,7 @@ let diff_and_rename current_file =
         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
         let restarting = GobConfig.get_string_list "incremental.restart_globs.globs" in
-        (* TODO: Check whether passing current_file is correct, or whether we need the version map. *)
-        let restarting = Cilfacade.globals_from_names current_file restarting in
+        let restarting = Cilfacade.global_varinfos_from_names current_file restarting in
         (changes, restarting, Some old_file, version_map, max_ids)
       end else begin
         let (version_map, max_ids) = VersionLookup.create_map current_file in
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index e555732012..d73f5f7e8e 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -750,11 +750,7 @@ module WP =
         let get x = try HM.find rho x with Not_found -> S.Dom.bot () in
         List.iter
           (fun g ->
-             (* All gs arriving here should yield Some varinfo. *)
-             let g = Option.get @@ Cilfacade.varinfo_from_global g in
-             S.iter_vars
-               get
-               (Global g)
+             S.iter_vars get (Global g)
                (fun v ->
                   if HM.mem stable v then begin
                     destabilize_leaf v;
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index af2ea23ab8..b115905398 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -32,15 +32,17 @@ let varinfo_from_global (g : Cil.global) : Cil.varinfo option = match g with
   | GVarDecl (v, _) -> Some v
   | _ -> None
 
-let globals_from_names (file: Cil.file) (names: string list): global list =
+(** Takes a [Cil.file] and a list of names of globals, and returns a
+    list of [varinfo]s of globals whose [vname] is contained in the argument list. *)
+let global_varinfos_from_names (file: Cil.file) (names: string list): varinfo list =
   let module SM = Set.Make(String) in
   let set = SM.of_list names in
   let globals =
     Cil.foldGlobals file (fun acc g ->
-      match varinfo_from_global g with
+        match varinfo_from_global g with
         | Some v ->
           if SM.mem v.vname set then
-            g::acc
+            v::acc
           else
             acc
         | None -> acc

From 2e6f19400a3182fbfa6cf4afddd79da02c81661f Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 14:57:10 +0100
Subject: [PATCH 10/22] Reuse Printable.String instead of creating a new module
 for it

---
 src/util/cilfacade.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index b115905398..24bb996a9c 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -21,11 +21,6 @@ let rec get_labelsLoc = function
     else
       loc
 
-module String = struct
-  include String
-  let hash = Hashtbl.hash
-end
-
 let varinfo_from_global (g : Cil.global) : Cil.varinfo option = match g with
   | GFun (f, _) -> Some f.svar
   | GVar (v, _, _) -> Some v
@@ -35,7 +30,7 @@ let varinfo_from_global (g : Cil.global) : Cil.varinfo option = match g with
 (** Takes a [Cil.file] and a list of names of globals, and returns a
     list of [varinfo]s of globals whose [vname] is contained in the argument list. *)
 let global_varinfos_from_names (file: Cil.file) (names: string list): varinfo list =
-  let module SM = Set.Make(String) in
+  let module SM = Set.Make(Printable.Strings) in
   let set = SM.of_list names in
   let globals =
     Cil.foldGlobals file (fun acc g ->

From dd8cf517550f578bb8f17a6c4b80b4bddf383be7 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 15:16:39 +0100
Subject: [PATCH 11/22] Annotate that earlyglobs is reason for imprecision

---
 .../04-manual-restart/02-read_write_global.c         |  2 +-
 .../04-manual-restart/02-read_write_global.patch     | 12 +++++++-----
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/tests/incremental/04-manual-restart/02-read_write_global.c b/tests/incremental/04-manual-restart/02-read_write_global.c
index 257aa969ac..8a93caabe3 100644
--- a/tests/incremental/04-manual-restart/02-read_write_global.c
+++ b/tests/incremental/04-manual-restart/02-read_write_global.c
@@ -6,7 +6,7 @@ void foo(){
 
 void bar(){
     int x = g;
-    assert(x % 2 == 0); // UNKNOWN
+    assert(x % 2 == 0); // UNKNOWN (imprecision caused by earlyglobs)
 }
 
 int main(){
diff --git a/tests/incremental/04-manual-restart/02-read_write_global.patch b/tests/incremental/04-manual-restart/02-read_write_global.patch
index 92893d37c5..1563f54146 100644
--- a/tests/incremental/04-manual-restart/02-read_write_global.patch
+++ b/tests/incremental/04-manual-restart/02-read_write_global.patch
@@ -1,5 +1,5 @@
 diff --git tests/incremental/04-manual-restart/02-read_write_global.c tests/incremental/04-manual-restart/02-read_write_global.c
-index 257aa969a..521322dd0 100644
+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 @@
@@ -12,21 +12,23 @@ index 257aa969a..521322dd0 100644
  
  void bar(){
      int x = g;
--    assert(x % 2 == 0); // UNKNOWN
+-    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 8685ac3b7..acf0568c8 100644
+index 8685ac3b7..b0bb607d9 100644
 --- tests/incremental/04-manual-restart/02-read_write_global.json
 +++ tests/incremental/04-manual-restart/02-read_write_global.json
-@@ -15,7 +15,7 @@
+@@ -15,7 +15,9 @@
              }
          },
          "restart_globs": {
 -            "globs": []
-+            "globs": ["g"]
++            "globs": [
++                "g"
++            ]
          }
      }
  }

From e7d591e4c1a0440d12645e691abf66918c95b8e1 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 27 Jan 2022 15:17:50 +0100
Subject: [PATCH 12/22] Comment that check is a hack to determine whether
 unknown relates to a global variable

---
 src/solvers/td3.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index d73f5f7e8e..15fa931621 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -738,6 +738,7 @@ module WP =
                 ) w
             )
           in
+          (* Hack: Only restart unknowns describing global variables *)
           if Node.equal (S.Var.node x) (Function Cil.dummyFunDec) then (
             restart_leaf x;
             destab_side_dep x;

From f5ee0948bd2da46474a6c2b3ca1794ffbf06530b Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Fri, 28 Jan 2022 10:00:18 +0100
Subject: [PATCH 13/22] Allow manual restarting of functions

---
 src/framework/analyses.ml |  2 +-
 src/maingoblint.ml        |  2 +-
 src/solvers/td3.ml        | 21 +++++++------------
 src/util/cilUtil.ml       | 43 +++++++++++++++++++++++++++++++++++++++
 src/util/cilfacade.ml     | 23 ---------------------
 5 files changed, 52 insertions(+), 39 deletions(-)
 create mode 100644 src/util/cilUtil.ml

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index d1eb1e1f46..6a1dc4c60b 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -456,7 +456,7 @@ type increment_data = {
 
   (* Globals for whiche the constraint
      system unknowns should be restarted *)
-  restarting: Cil.varinfo list;
+  restarting: VarQuery.t list;
 }
 
 let empty_increment_data file = {
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 9ece899a60..3f07656683 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -454,7 +454,7 @@ let diff_and_rename current_file =
         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
         let restarting = GobConfig.get_string_list "incremental.restart_globs.globs" in
-        let restarting = Cilfacade.global_varinfos_from_names current_file restarting in
+        let restarting = CilUtil.varquery_from_names current_file restarting in
         (changes, restarting, Some old_file, version_map, max_ids)
       end else begin
         let (version_map, max_ids) = VersionLookup.create_map current_file in
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 15fa931621..aed49ba145 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -738,25 +738,18 @@ module WP =
                 ) w
             )
           in
-          (* Hack: Only restart unknowns describing global variables *)
-          if Node.equal (S.Var.node x) (Function Cil.dummyFunDec) then (
-            restart_leaf x;
-            destab_side_dep x;
-            destabilize_normal x
-          ) else (
-            ignore @@ Pretty.printf "Trying to restart %a which does not describe a global variable." S.Var.pretty_trace x
-          )
+          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 (Global g)
-               (fun v ->
-                  if HM.mem stable v then begin
-                    destabilize_leaf v;
-                  end
-               )
+            S.iter_vars get g
+               (fun v -> if HM.mem stable v then destabilize_leaf v)
           )
           globals_to_restart;
 
diff --git a/src/util/cilUtil.ml b/src/util/cilUtil.ml
new file mode 100644
index 0000000000..9041bf12ec
--- /dev/null
+++ b/src/util/cilUtil.ml
@@ -0,0 +1,43 @@
+(** Functionality to create [VarQuery.t] lists from a list of names of global variable and function definitions *)
+(* Separate file from cilfacade.ml, for functions that depend both on [Node] and [VarQuery]. Avoids dependency cycle *)
+
+module type S =
+sig
+  val varquery_from_names : Cil.file -> string list -> VarQuery.t list
+end
+
+module M : S =
+struct
+  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) : VarQuery.t option = match g with
+    | GFun (f, _) -> Some (VarQuery.Node {node = FunctionEntry f; fundec = Some f})
+    | GVar (v, _, _) -> Some (VarQuery.Global v)
+    | GVarDecl (v, _) -> Some (VarQuery.Global v)
+    | _ -> None
+
+  (** Takes a [Cil.file] and a list of names of globals, and returns a
+      list of [VarQuery.t]s of globals whose [vname] is contained in the argument list.
+      For  *)
+  let varquery_from_names (file: Cil.file) (names: string list): VarQuery.t list =
+    let module SM = Set.Make(Printable.Strings) in
+    let set = SM.of_list names in
+    let globals =
+      Cil.foldGlobals file (fun 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::acc
+              | _ -> acc
+            end
+          | None, None -> acc
+          | _, _ -> assert false
+        ) [] in
+    globals
+end
+
+include M
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 24bb996a9c..1742ac86ff 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -21,29 +21,6 @@ let rec get_labelsLoc = function
     else
       loc
 
-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
-
-(** Takes a [Cil.file] and a list of names of globals, and returns a
-    list of [varinfo]s of globals whose [vname] is contained in the argument list. *)
-let global_varinfos_from_names (file: Cil.file) (names: string list): varinfo list =
-  let module SM = Set.Make(Printable.Strings) in
-  let set = SM.of_list names in
-  let globals =
-    Cil.foldGlobals file (fun acc g ->
-        match varinfo_from_global g with
-        | Some v ->
-          if SM.mem v.vname set then
-            v::acc
-          else
-            acc
-        | None -> acc
-      ) [] in
-  globals
-
 let get_stmtkindLoc = Cil.get_stmtLoc (* CIL has a confusing name for this function *)
 
 let get_stmtLoc stmt =

From 35896633ebfb8edf28c8d5dcada34d7fda6e4ddd Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Fri, 28 Jan 2022 11:27:48 +0100
Subject: [PATCH 14/22] Add test case for manual restarting of function with
 partial contexts

---
 .../04-manual-restart/03-partial_contexts.c   | 11 ++++++++
 .../03-partial_contexts.json                  | 19 ++++++++++++++
 .../03-partial_contexts.patch                 | 26 +++++++++++++++++++
 3 files changed, 56 insertions(+)
 create mode 100644 tests/incremental/04-manual-restart/03-partial_contexts.c
 create mode 100644 tests/incremental/04-manual-restart/03-partial_contexts.json
 create mode 100644 tests/incremental/04-manual-restart/03-partial_contexts.patch

diff --git a/tests/incremental/04-manual-restart/03-partial_contexts.c b/tests/incremental/04-manual-restart/03-partial_contexts.c
new file mode 100644
index 0000000000..a2a7016734
--- /dev/null
+++ b/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;
+}
diff --git a/tests/incremental/04-manual-restart/03-partial_contexts.json b/tests/incremental/04-manual-restart/03-partial_contexts.json
new file mode 100644
index 0000000000..99334fccb8
--- /dev/null
+++ b/tests/incremental/04-manual-restart/03-partial_contexts.json
@@ -0,0 +1,19 @@
+{
+    "ana": {
+        "base": {
+            "context": {
+                "int": false
+            }
+        }
+    },
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        },
+        "restart_globs": {
+            "globs": []
+        }
+    }
+}
diff --git a/tests/incremental/04-manual-restart/03-partial_contexts.patch b/tests/incremental/04-manual-restart/03-partial_contexts.patch
new file mode 100644
index 0000000000..5245a4ac37
--- /dev/null
+++ b/tests/incremental/04-manual-restart/03-partial_contexts.patch
@@ -0,0 +1,26 @@
+diff --git tests/incremental/04-manual-restart/03-partial_contexts.c tests/incremental/04-manual-restart/03-partial_contexts.c
+index a2a701673..d0b4d3efc 100644
+--- tests/incremental/04-manual-restart/03-partial_contexts.c
++++ tests/incremental/04-manual-restart/03-partial_contexts.c
+@@ -4,7 +4,7 @@ int foo(int x){
+ }
+ 
+ int main(){
+-    int x = 12;
++    int x = 13;
+     int y = foo(x);
+     assert(x == y);
+     return 0;
+diff --git tests/incremental/04-manual-restart/03-partial_contexts.json tests/incremental/04-manual-restart/03-partial_contexts.json
+index 99334fccb..3da6121a1 100644
+--- tests/incremental/04-manual-restart/03-partial_contexts.json
++++ tests/incremental/04-manual-restart/03-partial_contexts.json
+@@ -13,7 +13,7 @@
+             }
+         },
+         "restart_globs": {
+-            "globs": []
++            "globs": ["g"]
+         }
+     }
+ }

From 2e688a2ec1255f381fcfa93aba1a4725d8fffcf2 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Fri, 28 Jan 2022 16:31:07 +0100
Subject: [PATCH 15/22] Fix json in diff so to restart function foo

---
 .../04-manual-restart/03-partial_contexts.patch           | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/tests/incremental/04-manual-restart/03-partial_contexts.patch b/tests/incremental/04-manual-restart/03-partial_contexts.patch
index 5245a4ac37..295e2a5fa9 100644
--- a/tests/incremental/04-manual-restart/03-partial_contexts.patch
+++ b/tests/incremental/04-manual-restart/03-partial_contexts.patch
@@ -12,15 +12,17 @@ index a2a701673..d0b4d3efc 100644
      assert(x == y);
      return 0;
 diff --git tests/incremental/04-manual-restart/03-partial_contexts.json tests/incremental/04-manual-restart/03-partial_contexts.json
-index 99334fccb..3da6121a1 100644
+index 99334fccb..42a1da505 100644
 --- tests/incremental/04-manual-restart/03-partial_contexts.json
 +++ tests/incremental/04-manual-restart/03-partial_contexts.json
-@@ -13,7 +13,7 @@
+@@ -13,7 +13,9 @@
              }
          },
          "restart_globs": {
 -            "globs": []
-+            "globs": ["g"]
++            "globs": [
++                "foo"
++            ]
          }
      }
  }

From ebb9b602832e26fa248f7d6487024ee12a9b203b Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Fri, 28 Jan 2022 16:38:54 +0100
Subject: [PATCH 16/22] Change call to destabilize to destabilize_normal.

Manual restarting should not cause transitively restarting other
unknowns, even in case that restart.sided.enabled is true.
The destabilize function relies on a reference to chose the function
whose implementation is actually used and may use the
destabilize_with_side internally. This is avoided by calling
destabilze_normal.
---
 src/solvers/td3.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index aed49ba145..ee5e7c29e3 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -734,7 +734,7 @@ module WP =
                   if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
                   HM.remove stable y;
                   HM.remove superstable y;
-                  destabilize y
+                  destabilize_normal y
                 ) w
             )
           in

From 2f98aa00ac1e60c251b7be20569d6c5747c92518 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Mon, 31 Jan 2022 14:49:24 +0100
Subject: [PATCH 17/22] Manual restarting: check whether unkown is a leaf, and
 warn if it is not.

---
 src/solvers/td3.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index ee5e7c29e3..06f5ccd5e4 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -748,8 +748,12 @@ module WP =
 
         List.iter
           (fun g ->
-            S.iter_vars get g
-               (fun v -> if HM.mem stable v then destabilize_leaf v)
+             S.iter_vars get g
+               (fun v ->
+                  if S.system v <> None then
+                    ignore @@ Pretty.printf "Trying to restart a non-leaf unknown. This has no effect."
+                  else if HM.mem stable v then
+                    destabilize_leaf v)
           )
           globals_to_restart;
 

From 293ba9e03963f8eb2bc4e8ec7fe86586823b41c9 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Mon, 31 Jan 2022 14:52:32 +0100
Subject: [PATCH 18/22] Add pretty printing of unknown in printout.

---
 src/solvers/td3.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 06f5ccd5e4..c2beee72da 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -751,7 +751,7 @@ module WP =
              S.iter_vars get g
                (fun v ->
                   if S.system v <> None then
-                    ignore @@ Pretty.printf "Trying to restart a non-leaf unknown. This has no effect."
+                    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)
           )

From 6afc7838e0cb6fc764be1a6285569406cbde52d2 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Mon, 31 Jan 2022 15:36:23 +0100
Subject: [PATCH 19/22] Manual global restarting: Warn about globals that
 should be restarted according to option, but cannot be found in the CIL-file.

---
 src/maingoblint.ml  | 13 +++++++++++--
 src/util/cilUtil.ml | 24 ++++++++++++++----------
 2 files changed, 25 insertions(+), 12 deletions(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 3f07656683..3177581278 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -444,8 +444,8 @@ 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, restarting, old_file, version_map, max_ids) =
@@ -454,7 +454,16 @@ let diff_and_rename current_file =
         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
         let restarting = GobConfig.get_string_list "incremental.restart_globs.globs" in
-        let restarting = CilUtil.varquery_from_names current_file restarting in
+
+        let restarting, not_found = CilUtil.varquery_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
diff --git a/src/util/cilUtil.ml b/src/util/cilUtil.ml
index 9041bf12ec..095c76ad57 100644
--- a/src/util/cilUtil.ml
+++ b/src/util/cilUtil.ml
@@ -3,7 +3,7 @@
 
 module type S =
 sig
-  val varquery_from_names : Cil.file -> string list -> VarQuery.t list
+  val varquery_from_names : Cil.file -> string list -> VarQuery.t list * string list
 end
 
 module M : S =
@@ -20,24 +20,28 @@ struct
     | GVarDecl (v, _) -> Some (VarQuery.Global v)
     | _ -> None
 
-  (** Takes a [Cil.file] and a list of names of globals, and returns a
-      list of [VarQuery.t]s of globals whose [vname] is contained in the argument list.
-      For  *)
-  let varquery_from_names (file: Cil.file) (names: string list): VarQuery.t list =
+  (** 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. *)
+  let varquery_from_names (file: Cil.file) (names: string list): VarQuery.t list * string list =
     let module SM = Set.Make(Printable.Strings) in
     let set = SM.of_list names in
-    let globals =
-      Cil.foldGlobals file (fun acc g ->
+
+    (* 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::acc
+              | true -> (vq::globs, SM.add v.vname matched)
               | _ -> acc
             end
           | None, None -> acc
           | _, _ -> assert false
-        ) [] in
-    globals
+        ) ([], 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
 end
 
 include M

From 2a1665b842f9048b899f15aa242c72b491b078d5 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Mon, 31 Jan 2022 15:51:08 +0100
Subject: [PATCH 20/22] Move contents from cilUtil to varQuery

---
 src/framework/varQuery.ml  | 35 ++++++++++++++++++++++++++++
 src/framework/varQuery.mli |  6 +++++
 src/maingoblint.ml         |  2 +-
 src/util/cilUtil.ml        | 47 --------------------------------------
 4 files changed, 42 insertions(+), 48 deletions(-)
 create mode 100644 src/framework/varQuery.mli
 delete mode 100644 src/util/cilUtil.ml

diff --git a/src/framework/varQuery.ml b/src/framework/varQuery.ml
index d3c3a88a4f..39072d5322 100644
--- a/src/framework/varQuery.ml
+++ b/src/framework/varQuery.ml
@@ -4,3 +4,38 @@ 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
+
+(** 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. *)
+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
diff --git a/src/framework/varQuery.mli b/src/framework/varQuery.mli
new file mode 100644
index 0000000000..40a9ba31f0
--- /dev/null
+++ b/src/framework/varQuery.mli
@@ -0,0 +1,6 @@
+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
+val varqueries_from_names : Cil.file -> string list -> t list * string list
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 3177581278..8945014087 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -455,7 +455,7 @@ let diff_and_rename current_file =
         let max_ids = UpdateCil.update_ids old_file max_ids current_file version_map changes in
         let restarting = GobConfig.get_string_list "incremental.restart_globs.globs" in
 
-        let restarting, not_found = CilUtil.varquery_from_names current_file restarting in
+        let restarting, not_found = VarQuery.varqueries_from_names current_file restarting in
 
         if not (List.is_empty not_found) then begin
           List.iter
diff --git a/src/util/cilUtil.ml b/src/util/cilUtil.ml
deleted file mode 100644
index 095c76ad57..0000000000
--- a/src/util/cilUtil.ml
+++ /dev/null
@@ -1,47 +0,0 @@
-(** Functionality to create [VarQuery.t] lists from a list of names of global variable and function definitions *)
-(* Separate file from cilfacade.ml, for functions that depend both on [Node] and [VarQuery]. Avoids dependency cycle *)
-
-module type S =
-sig
-  val varquery_from_names : Cil.file -> string list -> VarQuery.t list * string list
-end
-
-module M : S =
-struct
-  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) : VarQuery.t option = match g with
-    | GFun (f, _) -> Some (VarQuery.Node {node = FunctionEntry f; fundec = Some f})
-    | GVar (v, _, _) -> Some (VarQuery.Global v)
-    | GVarDecl (v, _) -> Some (VarQuery.Global v)
-    | _ -> None
-
-  (** 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. *)
-  let varquery_from_names (file: Cil.file) (names: string list): VarQuery.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
-end
-
-include M

From 8268dc0e447f9cbe4800f673ed5fed97cdd9a6cf Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Tue, 1 Feb 2022 18:09:47 +0100
Subject: [PATCH 21/22] Move documentation comment to .mli file

---
 src/framework/varQuery.ml  | 3 ---
 src/framework/varQuery.mli | 4 ++++
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/framework/varQuery.ml b/src/framework/varQuery.ml
index 39072d5322..40e856c900 100644
--- a/src/framework/varQuery.ml
+++ b/src/framework/varQuery.ml
@@ -17,9 +17,6 @@ let varquery_from_global (g : Cil.global) : t option = match g with
   | GVarDecl (v, _) -> Some (Global v)
   | _ -> None
 
-(** 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. *)
 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
diff --git a/src/framework/varQuery.mli b/src/framework/varQuery.mli
index 40a9ba31f0..01c7eda99f 100644
--- a/src/framework/varQuery.mli
+++ b/src/framework/varQuery.mli
@@ -3,4 +3,8 @@ type t =
   | 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

From ac4cb98ff18df5b92fa9614160e448c7c5a9b23f Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Fri, 11 Feb 2022 11:16:40 +0100
Subject: [PATCH 22/22] Rename option incremental.restart_globs.globs to
 incremental.restart.list

---
 src/maingoblint.ml                            |  4 +--
 src/util/options.schema.json                  | 25 +++++++------------
 .../01-restart_manual_simple.json             |  6 ++---
 .../01-restart_manual_simple.patch            | 16 ++++++------
 .../02-read_write_global.json                 |  6 ++---
 .../02-read_write_global.patch                | 14 +++++------
 .../03-partial_contexts.json                  |  6 ++---
 .../03-partial_contexts.patch                 | 14 +++++------
 8 files changed, 38 insertions(+), 53 deletions(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 8945014087..1eea6ff0ef 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -434,7 +434,7 @@ let check_arguments () =
   (* 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.restart.sided.enabled" && get_string_list "incremental.restart_globs.globs" <> [] then warn "Passing a non-empty list to incremental.restart_globs.globs (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated."
+  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
@@ -453,7 +453,7 @@ let diff_and_rename current_file =
         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
-        let restarting = GobConfig.get_string_list "incremental.restart_globs.globs" in
+        let restarting = GobConfig.get_string_list "incremental.restart.list" in
 
         let restarting, not_found = VarQuery.varqueries_from_names current_file restarting in
 
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 2d57ead24c..97fca8f05d 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -910,22 +910,6 @@
           },
           "additionalProperties": false
         },
-        "restart_globs": {
-          "title": "incremental.restart_globs",
-          "type": "object",
-          "properties": {
-            "globs": {
-              "title": "incremental.restart_globs.globs",
-              "description": "List of globals for which the analysis is to be restarted.",
-              "type": "array",
-              "items": {
-                "type": "string"
-              },
-              "default": []
-            }
-          },
-          "additionalProperties": false
-        },
         "restart": {
           "title": "incremental.restart",
           "type": "object",
@@ -948,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
diff --git a/tests/incremental/04-manual-restart/01-restart_manual_simple.json b/tests/incremental/04-manual-restart/01-restart_manual_simple.json
index 582ede8df1..dbdb1d651e 100644
--- a/tests/incremental/04-manual-restart/01-restart_manual_simple.json
+++ b/tests/incremental/04-manual-restart/01-restart_manual_simple.json
@@ -6,10 +6,8 @@
         "restart": {
             "sided": {
                 "enabled": false
-            }
-        },
-        "restart_globs": {
-            "globs": []
+            },
+            "list": []
         }
     }
 }
diff --git a/tests/incremental/04-manual-restart/01-restart_manual_simple.patch b/tests/incremental/04-manual-restart/01-restart_manual_simple.patch
index 483ebe1bc1..c27da3c70f 100644
--- a/tests/incremental/04-manual-restart/01-restart_manual_simple.patch
+++ b/tests/incremental/04-manual-restart/01-restart_manual_simple.patch
@@ -15,17 +15,15 @@ index cbfb0ba70..aa83393ac 100644
      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 582ede8df..51d6d31b2 100644
+index dbdb1d651..d66a6cf36 100644
 --- tests/incremental/04-manual-restart/01-restart_manual_simple.json
 +++ tests/incremental/04-manual-restart/01-restart_manual_simple.json
-@@ -9,7 +9,9 @@
-             }
-         },
-         "restart_globs": {
--            "globs": []
-+            "globs": [
-+                "g"
-+            ]
+@@ -7,7 +7,7 @@
+             "sided": {
+                 "enabled": false
+             },
+-            "list": []
++            "list": ["g"]
          }
      }
  }
diff --git a/tests/incremental/04-manual-restart/02-read_write_global.json b/tests/incremental/04-manual-restart/02-read_write_global.json
index 8685ac3b70..33dd19da40 100644
--- a/tests/incremental/04-manual-restart/02-read_write_global.json
+++ b/tests/incremental/04-manual-restart/02-read_write_global.json
@@ -12,10 +12,8 @@
         "restart": {
             "sided": {
                 "enabled": false
-            }
-        },
-        "restart_globs": {
-            "globs": []
+            },
+            "list": []
         }
     }
 }
diff --git a/tests/incremental/04-manual-restart/02-read_write_global.patch b/tests/incremental/04-manual-restart/02-read_write_global.patch
index 1563f54146..2d93b2c191 100644
--- a/tests/incremental/04-manual-restart/02-read_write_global.patch
+++ b/tests/incremental/04-manual-restart/02-read_write_global.patch
@@ -18,15 +18,15 @@ index 8a93caabe..521322dd0 100644
  
  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 8685ac3b7..b0bb607d9 100644
+index 33dd19da4..0820029df 100644
 --- tests/incremental/04-manual-restart/02-read_write_global.json
 +++ tests/incremental/04-manual-restart/02-read_write_global.json
-@@ -15,7 +15,9 @@
-             }
-         },
-         "restart_globs": {
--            "globs": []
-+            "globs": [
+@@ -13,7 +13,9 @@
+             "sided": {
+                 "enabled": false
+             },
+-            "list": []
++            "list": [
 +                "g"
 +            ]
          }
diff --git a/tests/incremental/04-manual-restart/03-partial_contexts.json b/tests/incremental/04-manual-restart/03-partial_contexts.json
index 99334fccb8..96011c8711 100644
--- a/tests/incremental/04-manual-restart/03-partial_contexts.json
+++ b/tests/incremental/04-manual-restart/03-partial_contexts.json
@@ -10,10 +10,8 @@
         "restart": {
             "sided": {
                 "enabled": false
-            }
-        },
-        "restart_globs": {
-            "globs": []
+            },
+            "list": []
         }
     }
 }
diff --git a/tests/incremental/04-manual-restart/03-partial_contexts.patch b/tests/incremental/04-manual-restart/03-partial_contexts.patch
index 295e2a5fa9..743330368c 100644
--- a/tests/incremental/04-manual-restart/03-partial_contexts.patch
+++ b/tests/incremental/04-manual-restart/03-partial_contexts.patch
@@ -12,15 +12,15 @@ index a2a701673..d0b4d3efc 100644
      assert(x == y);
      return 0;
 diff --git tests/incremental/04-manual-restart/03-partial_contexts.json tests/incremental/04-manual-restart/03-partial_contexts.json
-index 99334fccb..42a1da505 100644
+index 96011c871..0a42408a0 100644
 --- tests/incremental/04-manual-restart/03-partial_contexts.json
 +++ tests/incremental/04-manual-restart/03-partial_contexts.json
-@@ -13,7 +13,9 @@
-             }
-         },
-         "restart_globs": {
--            "globs": []
-+            "globs": [
+@@ -11,7 +11,9 @@
+             "sided": {
+                 "enabled": false
+             },
+-            "list": []
++            "list": [
 +                "foo"
 +            ]
          }