Merge pull request #1560 from goblint/issue-1541

Add backtrace markers around `LibraryFunctions` special calls

src/autoTune.ml

@@ -68,6 +68,7 @@ let functionArgs fd = (ResettableLazy.force functionCallMaps).argLists |> Functi
 
 let findMallocWrappers () =
   let isMalloc f =
+    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
@@ -153,13 +154,15 @@ let disableIntervalContextsInRecursiveFunctions () =
 
 let hasFunction pred =
   let relevant_static var =
+    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.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 *)

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.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () ->
       let desc = LibraryFunctions.find f in
       begin match desc.special args with
         | Assert { exp; _ } ->

src/common/dune

@@ -11,6 +11,7 @@
    goblint_logs
    goblint_config
    goblint_tracing
+   goblint_backtrace
    goblint-cil
    fpath
    yojson

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 *)

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.wrap_val ~mark:(Cilfacade.FunVarinfo v) @@ fun () ->
           let desc = LibraryFunctions.find v in
           (match desc.special args with
            | Lock _ -> true

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 []
 

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.
 

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]]);

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.wrap_val ~mark:(Cilfacade.FunVarinfo info) @@ fun () ->
         let desc = LibraryFunctions.find info in
         match desc.special args with
         | Malloc _

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.wrap_val ~mark:(Cilfacade.FunVarinfo fv) @@ fun () ->
               let desc = LibraryFunctions.find fv in
               begin match desc.special args with
                 | Lock _ -> true