From 4eb58d6be1462f75b113cf87fe63beddb4cce770 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 12 Aug 2024 14:30:38 +0300 Subject: [PATCH] Add Goblint_backtrace.wrap_val --- src/autoTune.ml | 6 +++--- src/cdomain/value/util/wideningThresholds.ml | 2 +- src/transform/evalAssert.ml | 2 +- src/util/backtrace/goblint_backtrace.ml | 9 +++++++++ src/util/backtrace/goblint_backtrace.mli | 3 +++ src/util/loopUnrolling.ml | 2 +- src/witness/witnessUtil.ml | 2 +- 7 files changed, 19 insertions(+), 7 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 43067b8bbc..a0b57c34e4 100644 --- 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,7 +154,7 @@ 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) @@ -162,7 +162,7 @@ let hasFunction pred = 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 index 42dff238ef..939ed9482f 100644 --- 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 index 90da794a93..8f858d09df 100644 --- 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 index 29198c27ea..513753bddb 100644 --- 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 index e2b6ed2913..e53bfd826a 100644 --- 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 index 42518708e9..07c20cb574 100644 --- 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 index c585b21abc..1526b6f95c 100644 --- 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