From e630b744c71f370a746ef1b9955f11efa654523a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 12 Aug 2024 14:20:48 +0300 Subject: [PATCH 1/3] Add backtrace markers around LibraryFunctions special calls (issue #1541) --- src/autoTune.ml | 3 +++ src/cdomain/value/util/wideningThresholds.ml | 1 + src/common/dune | 1 + src/common/util/cilfacade.ml | 8 ++++++++ src/transform/evalAssert.ml | 1 + src/util/loopUnrolling.ml | 1 + src/witness/witnessUtil.ml | 1 + 7 files changed, 16 insertions(+) diff --git a/src/autoTune.ml b/src/autoTune.ml index 8ec77739e7..43067b8bbc 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -68,6 +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 () -> if LibraryFunctions.is_special f then ( let desc = LibraryFunctions.find f in match functionArgs f with @@ -153,6 +154,7 @@ let disableIntervalContextsInRecursiveFunctions () = let hasFunction pred = let relevant_static var = + Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo var) ~finally:Fun.id @@ fun () -> if LibraryFunctions.is_special var then let desc = LibraryFunctions.find var in GobOption.exists (fun args -> pred (desc.special args)) (functionArgs var) @@ -160,6 +162,7 @@ let hasFunction pred = false in let relevant_dynamic var = + Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo var) ~finally:Fun.id @@ 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 0d93be76ff..42dff238ef 100644 --- a/src/cdomain/value/util/wideningThresholds.ml +++ b/src/cdomain/value/util/wideningThresholds.ml @@ -121,6 +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 () -> let desc = LibraryFunctions.find f in begin match desc.special args with | Assert { exp; _ } -> diff --git a/src/common/dune b/src/common/dune index 2d6816a00f..e5aeddde7f 100644 --- a/src/common/dune +++ b/src/common/dune @@ -11,6 +11,7 @@ goblint_logs goblint_config goblint_tracing + goblint_backtrace goblint-cil fpath yojson diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 99430ee8b6..8cd8c2c53f 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -6,6 +6,14 @@ module E = Errormsg include Cilfacade0 +type Goblint_backtrace.mark += FunVarinfo of varinfo + +let () = Goblint_backtrace.register_mark_printer (function + | FunVarinfo var -> + Some ("function " ^ CilType.Varinfo.show var) + | _ -> None (* for other marks *) + ) + (** Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method *) let create_var (var: varinfo) = (* Hack: using negative integers should preempt conflicts with ids generated by CIL *) diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml index 0fee26355b..90da794a93 100644 --- a/src/transform/evalAssert.ml +++ b/src/transform/evalAssert.ml @@ -44,6 +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 () -> let desc = LibraryFunctions.find v in (match desc.special args with | Lock _ -> true diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index e433c34b4a..42518708e9 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -311,6 +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 () -> 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 5d22fd1e83..c585b21abc 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -63,6 +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 () -> let desc = LibraryFunctions.find fv in begin match desc.special args with | Lock _ -> true From 476f20be1ad83c0857cd975741683d8e66e2608c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 12 Aug 2024 14:23:59 +0300 Subject: [PATCH 2/3] Fix __printf_chk library function specification (closes #1541) --- src/util/library/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index e7ff2a4d04..25a90da2d3 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -712,7 +712,7 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__errno", unknown []); ("__errno_location", unknown []); ("__h_errno_location", unknown []); - ("__printf_chk", unknown [drop "flag" []; drop "format" [r]]); + ("__printf_chk", unknown (drop "flag" [] :: drop "format" [r] :: VarArgs (drop' [r]))); ("__fprintf_chk", unknown (drop "stream" [r_deep; w_deep] :: drop "flag" [] :: drop "format" [r] :: VarArgs (drop' [r]))); ("__vfprintf_chk", unknown [drop "stream" [r_deep; w_deep]; drop "flag" []; drop "format" [r]; drop "ap" [r_deep]]); ("sysinfo", unknown [drop "info" [w_deep]]); From 4eb58d6be1462f75b113cf87fe63beddb4cce770 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 12 Aug 2024 14:30:38 +0300 Subject: [PATCH 3/3] 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