Use nodes for messages instead of locations

.semgrep/cil.yml

@@ -8,6 +8,7 @@ rules:
       - pattern: Cil.get_stmtLoc
     paths:
       exclude:
+        - cilfacade0.ml
         - cilfacade.ml
     message: use Cilfacade instead
     languages: [ocaml]

src/analyses/deadlock.ml

@@ -26,8 +26,8 @@ struct
     if !Goblintutil.postsolving then begin
       D.iter (fun e -> List.iter (fun (a,b) ->
           if ((MyLock.equal a e) && (MyLock.equal b newLock)) then (
-            Messages.warn "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty e.addr ValueDomain.Addr.pretty newLock.addr CilType.Location.pretty e.loc CilType.Location.pretty newLock.loc CilType.Location.pretty b.loc CilType.Location.pretty a.loc;
-            Messages.warn ~loc:a.loc "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty newLock.addr ValueDomain.Addr.pretty e.addr CilType.Location.pretty b.loc CilType.Location.pretty a.loc CilType.Location.pretty e.loc CilType.Location.pretty newLock.loc;
+            Messages.warn "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty e.addr ValueDomain.Addr.pretty newLock.addr pretty_node_loc e.node pretty_node_loc newLock.node pretty_node_loc b.node pretty_node_loc a.node;
+            Messages.warn ~loc:(Node a.node) "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty newLock.addr ValueDomain.Addr.pretty e.addr pretty_node_loc b.node pretty_node_loc a.node pretty_node_loc e.node pretty_node_loc newLock.node;
           )
           else () ) !forbiddenList ) lockList;
 
@@ -96,8 +96,8 @@ struct
       match LibraryFunctions.classify f.vname arglist with
       | `Lock (_, _, _) ->
         List.fold_left (fun d lockAddr ->
-          addLockingInfo {addr = lockAddr; loc = !Tracing.current_loc } ctx.local;
-          D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local
+          addLockingInfo {addr = lockAddr; node = Option.get !Node.current_node } ctx.local;
+          D.add {addr = lockAddr; node = Option.get !Node.current_node } ctx.local
         ) ctx.local (eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist))
       | `Unlock ->
         let lockAddrs = eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist) in

src/analyses/fileUse.ml

@@ -155,7 +155,7 @@ struct
     (* M.debug @@ "entering function "^f.vname^string_of_callstack ctx.local; *)
     let m = if f.svar.vname <> "main" then
         (* push current location onto stack *)
-        D.edit_callstack (BatList.cons !Tracing.current_loc) ctx.local
+        D.edit_callstack (BatList.cons (Option.get !Node.current_node)) ctx.local
       else ctx.local in
     (* we need to remove all variables that are neither globals nor special variables from the domain for f *)
     (* problem: we need to be able to check aliases of globals in check_overwrite_open -> keep those in too :/ *)
@@ -206,7 +206,7 @@ struct
     (* is f a pointer to a function we look out for? *)
     let f = eval_fv (Analyses.ask_of_ctx ctx) (Lval (Var f, NoOffset)) |? f in
     let m = ctx.local in
-    let loc = !Tracing.current_loc::(D.callstack m) in
+    let loc = (Option.get !Node.current_node)::(D.callstack m) in
     let arglist = List.map (Cil.stripCasts) arglist in (* remove casts, TODO safe? *)
     let split_err_branch lval dom =
       (* type? NULL = 0 = 0-ptr? Cil.intType, Cil.intPtrType, Cil.voidPtrType -> no difference *)

src/analyses/spec.ml

@@ -44,7 +44,7 @@ struct
   struct
     (* custom goto (D.goto is just for modifying) that checks if the target state is a warning and acts accordingly *)
     let goto ?may:(may=false) ?change_state:(change_state=true) key state m ws =
-      let loc = !Tracing.current_loc::(D.callstack m) in
+      let loc = (Option.get !Node.current_node)::(D.callstack m) in
       let warn key m msg =
         Str.global_replace (Str.regexp_string "$") (D.string_of_key key) msg
         |> D.warn ~may:(D.is_may key m || D.is_unknown key m)
@@ -419,7 +419,7 @@ struct
     (* M.debug @@ "entering function "^f.vname^D.string_of_callstack ctx.local; *)
     if f.svar.vname = "main" then load_specfile ();
     let m = if f.svar.vname <> "main" then
-        D.edit_callstack (BatList.cons !Tracing.current_loc) ctx.local
+        D.edit_callstack (BatList.cons (Option.get !Node.current_node)) ctx.local
       else ctx.local in [m, m]
 
   let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =

src/cdomains/deadlockDomain.ml

@@ -1,7 +1,8 @@
-open Cil
 open Pretty
 
-type myowntypeEntry = {addr : ValueDomain.Addr.t ; loc : location}
+type myowntypeEntry = {addr : ValueDomain.Addr.t ; node : Node.t}
+
+let pretty_node_loc () node = CilType.Location.pretty () (Node.location node)
 
 
 module MyLock : Printable.S with type t = myowntypeEntry =
@@ -15,8 +16,8 @@ struct
   let hash x = Ad.hash x.addr
   let compare x y = Ad.compare x.addr y.addr (* ignores loc field *)
   (* TODO: deadlock analysis output doesn't even use these, but manually outputs locations *)
-  let show x = (Ad.show x.addr) ^ "@" ^ (CilType.Location.show x.loc)
-  let pretty () x = Ad.pretty () x.addr ++ text "@" ++ CilType.Location.pretty () x.loc
+  let show x = (Ad.show x.addr) ^ "@" ^ (CilType.Location.show (Node.location x.node))
+  let pretty () x = Ad.pretty () x.addr ++ text "@" ++ pretty_node_loc () x.node
   let printXml c x = Ad.printXml c x.addr
   let to_yojson x = `String (show x)
 end

src/cdomains/lvalMapDomain.ml

@@ -21,7 +21,7 @@ sig
   val string_of_record: r -> string
 
   (* constructing *)
-  val make: k -> location list -> s -> t
+  val make: k -> Node.t list -> s -> t
 
   (* manipulation *)
   val map: (r -> r) -> t -> t
@@ -42,8 +42,8 @@ sig
   val may: (r -> bool) -> t -> bool
   (* properties of records *)
   val key: r -> k
-  val loc: r -> location list
-  val edit_loc: (location list -> location list) -> r -> r
+  val loc: r -> Node.t list
+  val edit_loc: (Node.t list -> Node.t list) -> r -> r
   val state: r -> s
   val in_state: s -> r -> bool
 
@@ -71,14 +71,14 @@ struct
   type s = Impl.s
   module R = struct
     include Printable.Blank
-    type t = { key: k; loc: location list; state: s }
+    type t = { key: k; loc: Node.t list; state: s }
     let hash = Hashtbl.hash
-    let equal a b = Lval.CilLval.equal a.key b.key && a.loc = b.loc (* FIXME: polymorphic list equal! *) && a.state = b.state
+    let equal a b = Lval.CilLval.equal a.key b.key && BatList.eq Node.equal a.loc b.loc && a.state = b.state
 
     let compare a b =
       let r = Lval.CilLval.compare a.key b.key in
       if r <> 0 then r else
-        let r = compare a.loc b.loc in (* FIXME: polymorphic list compare! *)
+        let r = List.compare Node.compare a.loc b.loc in
         if r <> 0 then r else
           Impl.compare a.state b.state
 
@@ -104,7 +104,7 @@ struct
 
   (* Printing *)
   let string_of_key k = Lval.CilLval.show k
-  let string_of_loc xs = String.concat ", " (List.map CilType.Location.show xs)
+  let string_of_loc xs = String.concat ", " (List.map (CilType.Location.show % Node.location) xs)
   let string_of_record r = Impl.string_of_state r.state^" ("^string_of_loc r.loc^")"
   let string_of (x,y) =
     if is_alias (x,y) then
@@ -222,7 +222,7 @@ struct
   (* callstack for locations *)
   let callstack_var = Goblintutil.create_var @@ Cil.makeVarinfo false "@callstack" Cil.voidType, `NoOffset
   let callstack m = get_record callstack_var m |> Option.map_default V.loc []
-  let string_of_callstack m = " [call stack: "^String.concat ", " (List.map CilType.Location.show (callstack m))^"]"
+  let string_of_callstack m = " [call stack: "^String.concat ", " (List.map (CilType.Location.show % Node.location) (callstack m))^"]"
   let edit_callstack f m = edit_record callstack_var (V.edit_loc f) m
 
 
@@ -250,12 +250,12 @@ struct
   let string_of_entry k m = string_of_key k ^ ": " ^ string_of_state k m
   let string_of_map m = List.map (fun (k,v) -> string_of_entry k m) (bindings m)
 
-  let warn ?may:(may=false) ?loc:(loc=[!Tracing.current_loc]) msg =
+  let warn ?may:(may=false) ?loc:(loc=[Option.get !Node.current_node]) msg =
     match msg |> Str.split (Str.regexp "[ \n\r\x0c\t]+") with
-    | [] -> (if may then Messages.warn else Messages.error) ~loc:(List.last loc) "%s" msg
+    | [] -> (if may then Messages.warn else Messages.error) ~loc:(Node (List.last loc)) "%s" msg
     | h :: t ->
       let warn_type = Messages.Category.from_string_list (h |> Str.split (Str.regexp "[.]"))
-      in (if may then Messages.warn else Messages.error) ~loc:(List.last loc) ~category:warn_type "%a" (Pretty.docList ~sep:(Pretty.text " ") Pretty.text) t
+      in (if may then Messages.warn else Messages.error) ~loc:(Node (List.last loc)) ~category:warn_type "%a" (Pretty.docList ~sep:(Pretty.text " ") Pretty.text) t
 
   (* getting keys from Cil Lvals *)
   let sprint f x = Pretty.sprint 80 (f () x)

src/domains/access.ml

@@ -211,7 +211,7 @@ let get_val_type e (vo: var_o) (oo: off_o) : acc_typ =
 
 let add_one side (e:exp) (w:bool) (conf:int) (ty:acc_typ) (lv:(varinfo*offs) option) ((pp,lp):part): unit =
   if is_ignorable lv then () else begin
-    let loc = !Tracing.current_loc in
+    let loc = Option.get !Node.current_node in
     let add_part ls =
       side ty lv (Some ls) (conf, w, loc, e, lp)
     in
@@ -374,12 +374,12 @@ let add side e w conf vo oo p =
 module A =
 struct
   include Printable.Std
-  type t = int * bool * CilType.Location.t * CilType.Exp.t * LSSet.t [@@deriving eq, ord]
+  type t = int * bool * Node.t * CilType.Exp.t * LSSet.t [@@deriving eq, ord]
 
   let hash (conf, w, loc, e, lp) = 0 (* TODO: never hashed? *)
 
-  let pretty () (conf, w, loc, e, lp) =
-    Pretty.dprintf "%d, %B, %a, %a, %a" conf w CilType.Location.pretty loc CilType.Exp.pretty e LSSet.pretty lp
+  let pretty () (conf, w, node, e, lp) =
+    Pretty.dprintf "%d, %B, %a, %a, %a" conf w CilType.Location.pretty (Node.location node) CilType.Exp.pretty e LSSet.pretty lp
 
   let show x = Pretty.sprint ~width:max_int (pretty () x)
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
@@ -466,7 +466,7 @@ let print_accesses (lv, ty) pm =
   let allglobs = get_bool "allglobs" in
   let debug = get_bool "dbg.debug" in
   let g (ls, acs) =
-    let h (conf,w,loc,e,lp) =
+    let h (conf,w,node,e,lp) =
       let d_ls () = match ls with
         | None -> Pretty.text " is ok" (* None is used by add_one when access partitions set is empty (not singleton), so access is considered unracing (single-threaded or bullet region)*)
         | Some ls when LSSet.is_empty ls -> nil
@@ -480,7 +480,7 @@ let print_accesses (lv, ty) pm =
         else
           d_msg ()
       in
-      (doc, Some loc)
+      (doc, Some (Messages.Location.Node node))
     in
     AS.elements acs
     |> List.enum

src/framework/analyses.ml

@@ -168,7 +168,8 @@ struct
   let printXmlWarning f () =
     let one_text f Messages.Piece.{loc; text = m; _} =
       match loc with
-      | Some l ->
+      | Some loc ->
+        let l = Messages.Location.to_cil loc in
         BatPrintf.fprintf f "\n<text file=\"%s\" line=\"%d\" column=\"%d\">%s</text>" l.file l.line l.column (GU.escape m)
       | None ->
         () (* TODO: not outputting warning without location *)

src/framework/constraints.ml

@@ -1110,7 +1110,7 @@ struct
         EM.iter (fun exp tv ->
             match tv with
             | `Lifted tv ->
-              M.warn ~loc:(Node.location g) ~tags:[CWE (if tv then 571 else 570)] ~category:Deadcode "condition '%a' is always %B" d_exp exp tv
+              M.warn ~loc:(Node g) ~tags:[CWE (if tv then 571 else 570)] ~category:Deadcode "condition '%a' is always %B" d_exp exp tv
             | `Bot (* all branches dead? can happen at our inserted Neg(1)-s because no Pos(1) *)
             | `Top -> (* may be both true and false *)
               ()

src/framework/control.ml

@@ -126,7 +126,7 @@ struct
           endByte = 0; (* wrong, but not shown *)
         }
         in
-        (doc, Some loc)
+        (doc, Some (Messages.Location.CilLocation loc)) (* CilLocation is fine because always printed from scratch *)
       in
       let msgs =
         BatISet.fold_range (fun b e acc ->
@@ -514,7 +514,7 @@ struct
             let cnt = Cilfacade.countLoc fn in
             uncalled_dead := !uncalled_dead + cnt;
             if get_bool "dbg.uncalled" then
-              M.warn ~loc ~category:Deadcode "Function \"%a\" will never be called: %dLoC" CilType.Fundec.pretty fn cnt
+              M.warn ~loc:(CilLocation loc) ~category:Deadcode "Function \"%a\" will never be called: %dLoC" CilType.Fundec.pretty fn cnt  (* CilLocation is fine because always printed from scratch *)
         | _ -> ()
       in
       List.iter print_and_calculate_uncalled file.globals;
@@ -574,7 +574,7 @@ struct
 
     (* Use "normal" constraint solving *)
     let timeout_reached () =
-      M.error ~loc:!Tracing.current_loc "Timeout reached!";
+      M.error "Timeout reached!";
       (* let module S = Generic.SolverStats (EQSys) (LHT) in *)
       (* Can't call Generic.SolverStats...print_stats :(
          print_stats is triggered by dbg.solver-signal, so we send that signal to ourself in maingoblint before re-raising Timeout.

src/framework/myCFG.ml

@@ -45,7 +45,7 @@ end
 module NodeH = BatHashtbl.Make (Node)
 
 
-let current_node : node option ref = ref None
+let current_node = Node.current_node
 
 let unknown_exp : exp = mkString "__unknown_value__"
 let dummy_func = emptyFunction "__goblint_dummy_init" (* TODO get rid of this? *)

src/framework/node.ml

@@ -3,18 +3,7 @@ open Pretty
 
 include Printable.Std
 
-(** A node in the Control Flow Graph is either a statement or function. Think of
- * the function node as last node that all the returning nodes point to.  So
- * the result of the function call is contained in the function node. *)
-type t =
-  | Statement of CilType.Stmt.t
-  (** The statements as identified by CIL *)
-  (* The stmt in a Statement node is misleading because nodes are program points between transfer functions (edges), which actually correspond to statement execution. *)
-  | FunctionEntry of CilType.Fundec.t
-  (** *)
-  | Function of CilType.Fundec.t
-  (** The variable information associated with the function declaration. *)
-[@@deriving eq, ord, to_yojson]
+include Node0
 
 let name () = "node"
 
@@ -57,17 +46,6 @@ let show_cfg = function
   | FunctionEntry fd -> fd.svar.vname ^ "()"
 
 
-let hash = function
-  | Statement   stmt -> Hashtbl.hash (CilType.Stmt.hash stmt, 0)
-  | Function      fd -> Hashtbl.hash (CilType.Fundec.hash fd, 1)
-  | FunctionEntry fd -> Hashtbl.hash (CilType.Fundec.hash fd, 2)
-
-let location (node: t) =
-  match node with
-  | Statement stmt -> Cilfacade.get_stmtLoc stmt
-  | Function fd -> fd.svar.vdecl
-  | FunctionEntry fd -> fd.svar.vdecl
-
 (** Find [fundec] which the node is in. In an incremental run this might yield old fundecs for pseudo-return nodes from the old file. *)
 let find_fundec (node: t) =
   match node with

src/framework/node0.ml

@@ -0,0 +1,27 @@
+(** Node functions to avoid dependency cycles. *)
+
+(** A node in the Control Flow Graph is either a statement or function. Think of
+ * the function node as last node that all the returning nodes point to.  So
+ * the result of the function call is contained in the function node. *)
+type t =
+  | Statement of CilType.Stmt.t
+  (** The statements as identified by CIL *)
+  (* The stmt in a Statement node is misleading because nodes are program points between transfer functions (edges), which actually correspond to statement execution. *)
+  | FunctionEntry of CilType.Fundec.t
+  (** *)
+  | Function of CilType.Fundec.t
+  (** The variable information associated with the function declaration. *)
+[@@deriving eq, ord, to_yojson]
+
+let hash = function
+  | Statement   stmt -> Hashtbl.hash (CilType.Stmt.hash stmt, 0)
+  | Function      fd -> Hashtbl.hash (CilType.Fundec.hash fd, 1)
+  | FunctionEntry fd -> Hashtbl.hash (CilType.Fundec.hash fd, 2)
+
+let location (node: t) =
+  match node with
+  | Statement stmt -> Cilfacade0.get_stmtLoc stmt
+  | Function fd -> fd.svar.vdecl
+  | FunctionEntry fd -> fd.svar.vdecl
+
+let current_node: t option ref = ref None

src/incremental/updateCil.ml

@@ -3,19 +3,7 @@ open CompareCIL
 open VersionLookup
 open MyCFG
 
-module NodeMap = Hashtbl.Make(Node)
-
-let location_map = ref (NodeMap.create 103: location NodeMap.t)
-
-let getLoc (node: Node.t) =
-  (* In case this belongs to a changed function, we will find the true location in the map*)
-  try
-    NodeMap.find !location_map node
-  with Not_found ->
-    Node.location node
-
-let store_node_location (n: Node.t) (l: location): unit =
-  NodeMap.add !location_map n l
+include UpdateCil0
 
 let update_ids (old_file: file) (ids: max_ids) (new_file: file) (map: (global_identifier, Cil.global) Hashtbl.t) (changes: change_info) =
   let vid_max = ref ids.max_vid in

src/incremental/updateCil0.ml

@@ -0,0 +1,15 @@
+(** UpdateCil functions to avoid dependency cycles.*)
+
+module NodeMap = Hashtbl.Make(Node0)
+
+let location_map = ref (NodeMap.create 103: Cil.location NodeMap.t)
+
+let getLoc (node: Node0.t) =
+  (* In case this belongs to a changed function, we will find the true location in the map*)
+  try
+    NodeMap.find !location_map node
+  with Not_found ->
+    Node0.location node
+
+let store_node_location (n: Node0.t) (l: Cil.location): unit =
+  NodeMap.add !location_map n l

src/maingoblint.ml

@@ -352,8 +352,7 @@ let do_analyze change_info merged_AST =
         try Control.analyze change_info ast funs
         with e ->
           let backtrace = Printexc.get_raw_backtrace () in (* capture backtrace immediately, otherwise the following loses it (internal exception usage without raise_notrace?) *)
-          let loc = !Tracing.current_loc in
-          Messages.error ~loc "About to crash!"; (* TODO: move severity coloring to Messages *)
+          Messages.error "About to crash!"; (* TODO: move severity coloring to Messages *)
           (* trigger Generic.SolverStats...print_stats *)
           Goblintutil.(self_signal (signal_of_string (get_string "dbg.solver-signal")));
           do_stats ();