Revert "Merge pull request #364 from goblint/td3-solve-tf-abort"

This reverts commit 8cb50d4, reversing
changes made to b72dfe4.

Author: sim642

scripts/creduce-abort-verify.sh

@@ -458,7 +458,7 @@ module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment)
                            and module GVar = GVarF (S.V)
                            and module D = S.D
                            and module G = GVarG (S.G) (S.C)
-    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
+    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
   end
 =
 struct
@@ -695,64 +695,53 @@ 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
-    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 _       = 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
     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) pval getl sidel getg sideg =
+  let tf (v,c) (e,u) getl sidel getg sideg =
     let old_node = !current_node in
     let old_context = !M.current_context in
-    current_node := Some u;
+    let _       = current_node := Some u in
     M.current_context := Some (Obj.repr c);
-    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 d       = tf (v,c) (e,u) getl sidel getg sideg in
+    let _       = current_node := old_node in
+    M.current_context := old_context;
+    d
 
   let system (v,c) =
     match v with
     | FunctionEntry _ ->
       None
     | _ ->
       let tf getl sidel getg sideg =
-        let get_pval (_, u) = getl (u, c) in
-        let tf' eu pval = tf (v,c) eu pval getl sidel getg sideg in
+        let tf' eu = tf (v,c) eu 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_default scc.prev v [] 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
+          let xs_stricts = List.map tf' 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 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
+            let xs_non_stricts = List.map tf' non_stricts in
             List.fold_left S.D.join xs_strict xs_non_stricts
         | _ ->
-          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
+          let xs = List.map tf' (Cfg.prev v) in
           List.fold_left S.D.join (S.D.bot ()) xs
       in
       Some tf

src/framework/constraints.ml

@@ -388,7 +388,7 @@ let preprocess_and_merge () = preprocess_files () |> merge_preprocessed
 let do_stats () =
   if get_bool "printstats" then (
     print_newline ();
-    ignore (Pretty.printf "vars = %d    evals = %d    narrow_reuses = %d    aborts = %d\n" !Goblintutil.vars !Goblintutil.evals !Goblintutil.narrow_reuses !Goblintutil.aborts);
+    ignore (Pretty.printf "vars = %d    evals = %d    narrow_reuses = %d\n" !Goblintutil.vars !Goblintutil.evals !Goblintutil.narrow_reuses);
     print_newline ();
     Stats.print (Messages.get_out "timing" Legacy.stderr) "Timings:\n";
     flush_all ()
@@ -398,7 +398,6 @@ let reset_stats () =
   Goblintutil.vars := 0;
   Goblintutil.evals := 0;
   Goblintutil.narrow_reuses := 0;
-  Goblintutil.aborts := 0;
   Stats.reset SoftwareTimer
 
 (** Perform the analysis over the merged AST.  *)

src/maingoblint.ml

@@ -78,9 +78,6 @@ struct
     incr Goblintutil.evals;
     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