Interactive analysis

docs/user-guide/configuring.md

@@ -11,7 +11,8 @@ In `.vscode/settings.json` add the following:
     "json.schemas": [
         {
             "fileMatch": [
-                "/conf/*.json"
+                "/conf/*.json",
+                "/tests/incremental/*/*.json"
             ],
             "url": "/src/util/options.schema.json"
         }

scripts/creduce-abort-verify.sh

@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+set -e
+
+gcc -c -Werror=implicit-function-declaration ./abort-verify.c
+
+GOBLINTDIR="/mnt/goblint-svcomp/sv-comp/goblint"
+OPTS="--conf $GOBLINTDIR/conf/svcomp.json --enable solvers.td3.abort --enable solvers.td3.abort-verify --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit ./abort-verify.c"
+INTERESTING="TD3 abort verify: should not abort"
+OUTDIR="creduce-abort-verify"
+
+
+mkdir -p $OUTDIR
+
+LOG="$OUTDIR/out.log"
+$GOBLINTDIR/goblint $OPTS -v --enable dbg.debug &> $LOG || true
+grep -F "Function definition missing" $LOG && exit 1
+
+grep -F "$INTERESTING" $LOG

scripts/fix_patch_headers.sh

@@ -0,0 +1,9 @@
+#!/bin/bash
+#Run from root, e.g.,: ./scripts/fix_patch_headers.sh tests/incremental/11-restart/*.patch
+for file in "$@"
+do
+  echo $file
+  cfile="${file%.patch}.c"
+  efile="${cfile//\//\\/}"
+  perl -0777 -i -pe "s/.*?@/--- $efile\n+++ $efile\n@/is" $file
+done

scripts/update_suite.rb

@@ -406,8 +406,13 @@ def create_test_set(lines)
     super(lines)
     @testset.p = self
     `patch -p0 -b <#{patch_path}`
+    status = $?.exitstatus
     lines_incr = IO.readlines(path)
     `patch -p0 -b -R <#{patch_path}`
+    if status != 0
+      puts "Failed to apply patch: #{patch_path}"
+      exit 1
+    end
     @testset_incr = parse_tests(lines_incr)
     @testset_incr.p = self
     @testset_incr.warnfile = File.join($testresults, group, name + ".incr.warn.txt")

src/framework/analyses.ml

@@ -55,6 +55,7 @@ struct
 
   let pretty_trace () ((n,c) as x) =
     if get_bool "dbg.trace.context" then dprintf "(%a, %a) on %a \n" Node.pretty_trace n LD.pretty c CilType.Location.pretty (getLocation x)
+    (* if get_bool "dbg.trace.context" then dprintf "(%a, %d) on %a" Node.pretty_trace n (LD.tag c) CilType.Location.pretty (getLocation x) *)
     else dprintf "%a on %a" Node.pretty_trace n CilType.Location.pretty (getLocation x)
 
   let printXml f (n,c) =

src/framework/constraints.ml

@@ -459,7 +459,7 @@ module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment)
                            and module GVar = GVarF (S.V)
                            and module D = S.D
                            and module G = S.G
-    val tf : MyCFG.node * S.C.t -> (Cil.location * MyCFG.edge) list * MyCFG.node -> ((MyCFG.node * S.C.t) -> S.D.t) -> (MyCFG.node * S.C.t -> S.D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t
+    val tf : MyCFG.node * S.C.t -> (Cil.location * MyCFG.edge) list * MyCFG.node -> D.t -> ((MyCFG.node * S.C.t) -> S.D.t) -> (MyCFG.node * S.C.t -> S.D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t
   end
 =
 struct
@@ -684,53 +684,64 @@ struct
   let tf var getl sidel getg sideg prev_node (_,edge) d (f,t) =
     let old_loc  = !Tracing.current_loc in
     let old_loc2 = !Tracing.next_loc in
-    let _       = Tracing.current_loc := f in
-    let _       = Tracing.next_loc := t in
-    let d       = tf var getl sidel getg sideg prev_node edge d in
-    let _       = Tracing.current_loc := old_loc in
-    let _       = Tracing.next_loc := old_loc2 in
-    d
-
-  let tf (v,c) (edges, u) getl sidel getg sideg =
-    let pval = getl (u,c) in
+    Tracing.current_loc := f;
+    Tracing.next_loc := t;
+    Fun.protect ~finally:(fun () ->
+        Tracing.current_loc := old_loc;
+        Tracing.next_loc := old_loc2
+      ) (fun () ->
+        let d       = tf var getl sidel getg sideg prev_node edge d in
+        d
+      )
+
+  let tf (v,c) (edges, u) pval getl sidel getg sideg =
+    (* let pval = getl (u,c) in *)
     let _, locs = List.fold_right (fun (f,e) (t,xs) -> f, (f,t)::xs) edges (Node.location v,[]) in
     List.fold_left2 (|>) pval (List.map (tf (v,Obj.repr (fun () -> c)) getl sidel getg sideg u) edges) locs
 
-  let tf (v,c) (e,u) getl sidel getg sideg =
+  let tf (v,c) (e,u) pval getl sidel getg sideg =
     let old_node = !current_node in
     let old_context = !M.current_context in
-    let _       = current_node := Some u in
+    current_node := Some u;
     M.current_context := Some (Obj.repr c);
-    let d       = tf (v,c) (e,u) getl sidel getg sideg in
-    let _       = current_node := old_node in
-    M.current_context := old_context;
-    d
+    Fun.protect ~finally:(fun () ->
+        current_node := old_node;
+        M.current_context := old_context
+      ) (fun () ->
+        let d       = tf (v,c) (e,u) pval getl sidel getg sideg in
+        d
+      )
 
   let system (v,c) =
     match v with
     | FunctionEntry _ ->
       None
     | _ ->
       let tf getl sidel getg sideg =
-        let tf' eu = tf (v,c) eu getl sidel getg sideg in
+        let get_pval (_, u) = getl (u, c) in
+        let tf' eu pval = tf (v,c) eu pval getl sidel getg sideg in
 
         match NodeH.find_option CfgTools.node_scc_global v with
         | Some scc when NodeH.mem scc.prev v && NodeH.length scc.prev = 1 ->
           (* Limited to loops with only one entry node. Otherwise unsound as is. *)
           (* TODO: Is it possible to do soundly for multi-entry loops? *)
           let stricts = NodeH.find_all scc.prev v in
-          let xs_stricts = List.map tf' stricts in
+          let pvals_stricts = List.map get_pval stricts in (* get pvals before executing any tf to maximize abort *)
+          let xs_stricts = List.map2 tf' stricts pvals_stricts in
           if List.for_all S.D.is_bot xs_stricts then
             S.D.bot ()
           else
             let xs_strict = List.fold_left S.D.join (S.D.bot ()) xs_stricts in
             let equal = [%eq: (CilType.Location.t * Edge.t) list * Node.t] in
             let is_strict eu = List.exists (equal eu) stricts in
             let non_stricts = List.filter (neg is_strict) (Cfg.prev v) in
-            let xs_non_stricts = List.map tf' non_stricts in
+            let pvals_non_stricts = List.map get_pval non_stricts in (* get pvals before executing any tf to maximize abort *)
+            let xs_non_stricts = List.map2 tf' non_stricts pvals_non_stricts in
             List.fold_left S.D.join xs_strict xs_non_stricts
         | _ ->
-          let xs = List.map tf' (Cfg.prev v) in
+          let prevs = Cfg.prev v in
+          let pvals = List.map get_pval prevs in (* get pvals before executing any tf to maximize abort *)
+          let xs = List.map2 tf' prevs pvals in
           List.fold_left S.D.join (S.D.bot ()) xs
       in
       Some tf
@@ -1096,14 +1107,19 @@ struct
         f_eq ()
       else if b1 then begin
         if get_bool "solverdiffs" then
-          ignore (Pretty.printf "Global %a is more precise using left:\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2));
+          ignore (Pretty.printf "Global %a is more precise using left:\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1));
         f_le ()
       end else if b2 then begin
         if get_bool "solverdiffs" then
           ignore (Pretty.printf "Global %a is more precise using right:\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2));
         f_gr ()
-      end else
+      end else begin
+        if get_bool "solverdiffs" then (
+          ignore (Pretty.printf "Global %a is incomparable (diff):\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2));
+          ignore (Pretty.printf "Global %a is incomparable (reverse diff):\n%a\n" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1));
+        );
         f_uk ()
+      end
     in
     GH.iter f g1;
     Printf.printf "globals:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\n" !eq !le !gr !uk
@@ -1119,14 +1135,19 @@ struct
           incr eq
         else if b1 then begin
           if get_bool "solverdiffs" then
-            ignore (Pretty.printf "%a @@ %a is more precise using left:\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2));
+            ignore (Pretty.printf "%a @@ %a is more precise using left:\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1));
           incr le
         end else if b2 then begin
           if get_bool "solverdiffs" then
             ignore (Pretty.printf "%a @@ %a is more precise using right:\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2));
           incr gr
-        end else
+        end else begin
+          if get_bool "solverdiffs" then (
+            ignore (Pretty.printf "%a @@ %a is incomparable (diff):\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2));
+            ignore (Pretty.printf "%a @@ %a is incomparable (reverse diff):\n%a\n" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1));
+          );
           incr uk
+        end
     in
     PP.iter f h1;
     (* let k1 = Set.of_enum @@ PP.keys h1 in
@@ -1137,7 +1158,7 @@ struct
     Printf.printf "locals: \tequal = %d\tleft = %d\tright = %d\tincomparable = %d\n" !eq !le !gr !uk
 
   let compare_locals_ctx h1 h2 =
-    let eq, le, gr, uk, no2 = ref 0, ref 0, ref 0, ref 0, ref 0 in
+    let eq, le, gr, uk, no2, no1 = ref 0, ref 0, ref 0, ref 0, ref 0, ref 0 in
     let f_eq () = incr eq in
     let f_le () = incr le in
     let f_gr () = incr gr in
@@ -1150,22 +1171,31 @@ struct
         if b1 && b2 then
           f_eq ()
         else if b1 then begin
-          (* if get_bool "solverdiffs" then *)
-          (*   ignore (Pretty.printf "%a @@ %a is more precise using left:\n%a\n" pretty_node k CilType.Location.pretty (getLoc k) D.pretty_diff (v1,v2)); *)
+          if get_bool "solverdiffs" then
+            ignore (Pretty.printf "%a is more precise using left:\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1));
           f_le ()
         end else if b2 then begin
-          (* if get_bool "solverdiffs" then *)
-          (*   ignore (Pretty.printf "%a @@ %a is more precise using right:\n%a\n" pretty_node k CilType.Location.pretty (getLoc k) D.pretty_diff (v1,v2)); *)
+          if get_bool "solverdiffs" then
+            ignore (Pretty.printf "%a is more precise using right:\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2));
           f_gr ()
-        end else
+        end else begin
+          if get_bool "solverdiffs" then (
+            ignore (Pretty.printf "%a is incomparable (diff):\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2));
+            ignore (Pretty.printf "%a is incomparable (reverse diff):\n%a\n" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1));
+          );
           f_uk ()
+        end
     in
     LH.iter f h1;
+    let f k v2 =
+      if not (LH.mem h1 k) then incr no1
+    in
+    LH.iter f h2;
     (* let k1 = Set.of_enum @@ PP.keys h1 in *)
     (* let k2 = Set.of_enum @@ PP.keys h2 in *)
     (* let o1 = Set.cardinal @@ Set.diff k1 k2 in *)
     (* let o2 = Set.cardinal @@ Set.diff k2 k1 in *)
-    Printf.printf "locals_ctx:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\tno_ctx_in_right = %d\n" !eq !le !gr !uk !no2
+    Printf.printf "locals_ctx:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\tno_ctx_in_right = %d\tno_ctx_in_left = %d\n" !eq !le !gr !uk !no2 !no1
 
   let compare (name1,name2) (l1,g1) (l2,g2) =
     let one_ctx (n,_) v h =
@@ -1200,7 +1230,8 @@ struct
 
   let compare (name1, name2) vh1 vh2 =
     Printf.printf "\nComparing precision of %s (left) with %s (right) as EqConstrSys:\n" name1 name2;
-    let (_, msg) = Compare.compare ~name1 vh1 ~name2 vh2 in
+    let verbose = get_bool "solverdiffs" in
+    let (_, msg) = Compare.compare ~verbose ~name1 vh1 ~name2 vh2 in
     ignore (Pretty.printf "Comparison summary: %t\n" (fun () -> msg));
     print_newline ();
 end

src/framework/control.ml

@@ -298,11 +298,15 @@ struct
 
     GU.global_initialization := true;
     GU.earlyglobs := get_bool "exp.earlyglobs";
-    if get_string "load_run" <> "" then (
-      Spec.init (Some (Serialize.unmarshal (Filename.concat (get_string "load_run") "spec_marshal")))
-    )
-    else
-      Spec.init None;
+    let marshal =
+      if get_string "load_run" <> "" then
+        Some (Serialize.unmarshal (Filename.concat (get_string "load_run") "spec_marshal"))
+      else if Serialize.results_exist () && get_bool "incremental.load" then
+        Some (Serialize.load_data Serialize.AnalysisData)
+      else
+        None
+    in
+    Spec.init marshal;
     Access.init file;
 
     let test_domain (module D: Lattice.S): unit =
@@ -508,10 +512,6 @@ struct
       (* Most warnings happen before durin postsolver, but some happen later (e.g. in finalize), so enable this for the rest (if required by option). *)
       Goblintutil.should_warn := PostSolverArg.should_warn;
 
-      if GobConfig.get_bool "incremental.save" then (
-        Serialize.move_tmp_results_to_results () (* Move new incremental results to place where they will be reused *)
-      );
-
       let insrt k _ s = match k with
         | (MyCFG.Function fn,_) -> if not (get_bool "exp.forward") then Set.Int.add fn.svar.vid s else s
         | (MyCFG.FunctionEntry fn,_) -> if (get_bool "exp.forward") then Set.Int.add fn.svar.vid s else s
@@ -643,7 +643,10 @@ struct
     if get_string "save_run" <> "" then (
       Serialize.marshal marshal (Filename.concat (get_string "save_run") "spec_marshal")
     );
-
+    if get_bool "incremental.save" then (
+      Serialize.store_data marshal Serialize.AnalysisData;
+      Serialize.move_tmp_results_to_results ()
+    );
     if get_bool "dbg.verbose" && get_string "result" <> "none" then print_endline ("Generating output: " ^ get_string "result");
     Result.output (lazy local_xml) gh make_global_fast_xml file
 end

src/incremental/serialize.ml

@@ -5,6 +5,7 @@ let goblint_dirname = "incremental_data"
 let version_map_filename = "version.data"
 let cil_file_name = "ast.data"
 let solver_data_file_name = "solver.data"
+let analysis_data_file_name = "analysis.data"
 let results_dir = "results"
 let results_tmp_dir = "results_tmp"
 let gob_directory () = let src_dir = !base_directory in
@@ -31,12 +32,13 @@ let results_exist () =
   Sys.file_exists r && Sys.is_directory r
 
 (* Convenience enumeration of the different data types we store for incremental analysis, so file-name logic is concentrated in one place *)
-type incremental_data_kind = SolverData | CilFile | VersionData
+type incremental_data_kind = SolverData | CilFile | VersionData | AnalysisData
 
 let type_to_file_name = function
   | SolverData -> solver_data_file_name
   | CilFile -> cil_file_name
   | VersionData -> version_map_filename
+  | AnalysisData -> analysis_data_file_name
 
 (** Loads data for incremental runs from the appropriate file *)
 let load_data (data_type: incremental_data_kind) =

src/maingoblint.ml

@@ -319,7 +319,7 @@ let merge_preprocessed cpp_file_names =
 let do_stats () =
   if get_bool "printstats" then (
     print_newline ();
-    ignore (Pretty.printf "vars = %d    evals = %d  \n" !Goblintutil.vars !Goblintutil.evals);
+    ignore (Pretty.printf "vars = %d    evals = %d    narrow_reuses = %d    aborts = %d\n" !Goblintutil.vars !Goblintutil.evals !Goblintutil.narrow_reuses !Goblintutil.aborts);
     print_newline ();
     Stats.print (Messages.get_out "timing" Legacy.stderr) "Timings:\n";
     flush_all ()
@@ -431,7 +431,7 @@ 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.rename-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.")
 
 let handle_extraspecials () =
   let funs = get_string_list "exp.extraspecials" in

src/solvers/generic.ml

@@ -77,6 +77,9 @@ struct
     Goblintutil.evals := !Goblintutil.evals + 1;
     if (get_bool "dbg.solver-progress") then (incr stack_d; print_int !stack_d; flush stdout)
 
+  let abort_rhs_event x =
+    incr Goblintutil.aborts
+
   let update_var_event x o n =
     if tracing then increase x;
     if full_trace || ((not (Dom.is_bot o)) && Option.is_some !max_var && Var.equal (Option.get !max_var) x) then begin