TD3: optimize destabilization by aborting transfer function when unchanged

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 exp.solver.td3.abort --enable exp.solver.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

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

@@ -454,7 +454,7 @@ module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment)
                            and module GVar = Basetype.Variables
                            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) -> (Cil.varinfo -> G.t) -> (Cil.varinfo -> 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) -> (Cil.varinfo -> G.t) -> (Cil.varinfo -> G.t -> unit) -> D.t
   end
 =
 struct
@@ -679,53 +679,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

src/maingoblint.ml

@@ -320,7 +320,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    aborts = %d\n" !Goblintutil.vars !Goblintutil.evals !Goblintutil.aborts);
     print_newline ();
     Stats.print (Messages.get_out "timing" Legacy.stderr) "Timings:\n";
     flush_all ()

src/solvers/generic.ml

@@ -242,6 +242,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