Add Goblint_backtrace.wrap_val

goblint · Aug 12, 2024 · 4eb58d6 · 4eb58d6
1 parent 476f20b
commit 4eb58d6
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 7 deletions.
diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -68,7 +68,7 @@ let functionArgs fd = (ResettableLazy.force functionCallMaps).argLists |> Functi
 
 let findMallocWrappers () =
   let isMalloc f =
-    Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo f) ~finally:Fun.id @@ fun () ->
+    Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () ->
     if LibraryFunctions.is_special f then (
       let desc = LibraryFunctions.find f in
       match functionArgs f with
@@ -154,15 +154,15 @@ let disableIntervalContextsInRecursiveFunctions () =
 
 let hasFunction pred =
   let relevant_static var =
-    Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo var) ~finally:Fun.id @@ fun () ->
+    Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () ->
     if LibraryFunctions.is_special var then
       let desc = LibraryFunctions.find var in
       GobOption.exists (fun args -> pred (desc.special args)) (functionArgs var)
     else
       false
   in
   let relevant_dynamic var =
-    Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo var) ~finally:Fun.id @@ fun () ->
+    Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () ->
     if LibraryFunctions.is_special var then
       let desc = LibraryFunctions.find var in
       (* We don't really have arguments at hand, so we cheat and just feed it a list of MyCFG.unknown_exp of appropriate length *)

diff --git a/src/cdomain/value/util/wideningThresholds.ml b/src/cdomain/value/util/wideningThresholds.ml
@@ -121,7 +121,7 @@ class extractInvariantsVisitor (exps) = object
   method! vinst (i: instr) =
     match i with
     | Call (_, Lval (Var f, NoOffset), args, _, _) when LibraryFunctions.is_special f ->
-      Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo f) ~finally:Fun.id @@ fun () ->
+      Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () ->
       let desc = LibraryFunctions.find f in
       begin match desc.special args with
         | Assert { exp; _ } ->

diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
@@ -44,7 +44,7 @@ struct
       let is_lock exp args =
         match exp with
         | Lval(Var v,_) when LibraryFunctions.is_special v ->
-          Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo v) ~finally:Fun.id @@ fun () ->
+          Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo v) @@ fun () ->
           let desc = LibraryFunctions.find v in
           (match desc.special args with
            | Lock _ -> true

diff --git a/src/util/backtrace/goblint_backtrace.ml b/src/util/backtrace/goblint_backtrace.ml
@@ -36,6 +36,15 @@ let protect ~(mark: unit -> mark) ~(finally: unit -> unit) work =
     add_mark work_exn (mark ());
     Printexc.raise_with_backtrace work_exn work_bt
 
+(* Copied & modified from protect. *)
+let wrap_val ~(mark:mark) work =
+  try
+    work ()
+  with work_exn ->
+    let work_bt = Printexc.get_raw_backtrace () in
+    add_mark work_exn mark;
+    Printexc.raise_with_backtrace work_exn work_bt
+
 
 let mark_printers: (mark -> string option) list ref = ref []
 

diff --git a/src/util/backtrace/goblint_backtrace.mli b/src/util/backtrace/goblint_backtrace.mli
@@ -24,6 +24,9 @@ val add_mark: exn -> mark -> unit
 val protect: mark:(unit -> mark) -> finally:(unit -> unit) -> (unit -> 'a) -> 'a
 (** {!Fun.protect} with additional [~mark] addition to all exceptions. *)
 
+val wrap_val: mark:mark -> (unit -> 'a) -> 'a
+(** {!protect} with [~mark] value and without [~finally]. *)
+
 val print_marktrace: out_channel -> exn -> unit
 (** Print trace of marks of an exception.
 

diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
@@ -311,7 +311,7 @@ class loopUnrollingCallVisitor = object
 
   method! vinst = function
     | Call (_,Lval ((Var info), NoOffset),args,_,_) when LibraryFunctions.is_special info -> (
-        Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo info) ~finally:Fun.id @@ fun () ->
+        Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo info) @@ fun () ->
         let desc = LibraryFunctions.find info in
         match desc.special args with
         | Malloc _

diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml
@@ -63,7 +63,7 @@ struct
         List.exists (fun (_, edge) ->
             match edge with
             | Proc (_, Lval (Var fv, NoOffset), args) when LibraryFunctions.is_special fv ->
-              Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo fv) ~finally:Fun.id @@ fun () ->
+              Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo fv) @@ fun () ->
               let desc = LibraryFunctions.find fv in
               begin match desc.special args with
                 | Lock _ -> true