Merge pull request #1292 from goblint/plain-cil-printer

Make some exception printers lazy, do not use plain CIL printers in messages

src/analyses/base.ml

@@ -1878,7 +1878,7 @@ struct
 
   let invalidate ?(deep=true) ~ctx ask (gs:glob_fun) (st:store) (exps: exp list): store =
     if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]\n" (d_list ", " d_plainexp) exps;
-    if exps <> [] then M.info ~category:Imprecise "Invalidating expressions: %a" (d_list ", " d_plainexp) exps;
+    if exps <> [] then M.info ~category:Imprecise "Invalidating expressions: %a" (d_list ", " d_exp) exps;
     (* To invalidate a single address, we create a pair with its corresponding
      * top value. *)
     let invalidate_address st a =

src/analyses/baseInvariant.ml

@@ -243,12 +243,12 @@ struct
       refine_lv_fallback ctx a gs st lval value tv
     | None ->
       if M.tracing then M.traceu "invariant" "Doing nothing.\n";
-      M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_plainexp exp;
+      M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_exp exp;
       st
 
   let invariant ctx a gs st exp tv: D.t =
     let fallback reason st =
-      if M.tracing then M.tracel "inv" "Can't handle %a.\n%s\n" d_plainexp exp reason;
+      if M.tracing then M.tracel "inv" "Can't handle %a.\n%t\n" d_plainexp exp reason;
       invariant_fallback ctx a gs st exp tv
     in
     (* inverse values for binary operation a `op` b == c *)
@@ -689,7 +689,7 @@ struct
              (* Mixed Float and Int cases should never happen, as there are no binary operators with one float and one int parameter ?!*)
              | Int _, Float _ | Float _, Int _ -> failwith "ill-typed program";
                (* | Address a, Address b -> ... *)
-             | a1, a2 -> fallback (GobPretty.sprintf "binop: got abstract values that are not Int: %a and %a" VD.pretty a1 VD.pretty a2) st)
+             | a1, a2 -> fallback (fun () -> Pretty.dprintf "binop: got abstract values that are not Int: %a and %a" VD.pretty a1 VD.pretty a2) st)
             (* use closures to avoid unused casts *)
           in (match c_typed with
               | Int c -> invert_binary_op c ID.pretty (fun ik -> ID.cast_to ik c) (fun fk -> FD.of_int fk c)
@@ -778,7 +778,7 @@ struct
            | TFloat (fk, _), FLongDouble
            | TFloat (FDouble as fk, _), FDouble
            | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
-           | _ -> fallback ("CastE: incompatible types") st)
+           | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
         | CastE ((TInt (ik, _)) as t, e), Int c
         | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
           (match eval e st with
@@ -791,11 +791,11 @@ struct
                  let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) in (* TODO: cast without overflow, is this right for normal invariant? *)
                  if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a\n" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
                  inv_exp (Int c') e st
-               | x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st
+               | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st
              else
-               fallback (GobPretty.sprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
-           | v -> fallback (GobPretty.sprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
-        | e, _ -> fallback (GobPretty.sprintf "%a not implemented" d_plainexp e) st
+               fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
+           | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
+        | e, _ -> fallback (fun () -> Pretty.dprintf "%a not implemented" d_plainexp e) st
     in
     if eval_bool exp st = Some (not tv) then contra st (* we already know that the branch is dead *)
     else

src/cdomains/offset.ml

@@ -142,15 +142,11 @@ struct
     | TPtr (t,_), `Index (i,o) -> type_of ~base:t o
     | TComp (ci,_), `Field (f,o) ->
       let fi = try getCompField ci f.fname
-        with Not_found ->
-          let s = GobPretty.sprintf "Addr.type_offset: field %s not found in type %a" f.fname d_plaintype t in
-          raise (Type_of_error (t, s))
+        with Not_found -> raise (Type_of_error (t, show o))
       in type_of ~base:fi.ftype o
     (* TODO: Why? Imprecise on zstd-thread-pool regression tests. *)
     (* | TComp _, `Index (_,o) -> type_of ~base:t o (* this happens (hmmer, perlbench). safe? *) *)
-    | t,o ->
-      let s = GobPretty.sprintf "Addr.type_offset: could not follow offset in type. type: %a, offset: %a" d_plaintype t pretty o in
-      raise (Type_of_error (t, s))
+    | t, o -> raise (Type_of_error (t, show o))
 
   let rec prefix (x: t) (y: t): t option = match x,y with
     | `Index (x, xs), `Index (y, ys) when Idx.equal x y -> prefix xs ys
@@ -261,3 +257,9 @@ struct
     | `Index (i,o) -> Index (i, to_cil o)
     | `Field (f,o) -> Field (f, to_cil o)
 end
+
+
+let () = Printexc.register_printer (function
+    | Type_of_error (t, o) -> Some (GobPretty.sprintf "Offset.Type_of_error(%a, %s)" d_plaintype t o)
+    | _ -> None (* for other exceptions *)
+  )

tests/regression/04-mutex/49-type-invariants.t

@@ -16,8 +16,8 @@
     total lines: 7
   [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21)
+  [Info][Imprecise] Invalidating expressions: & s (49-type-invariants.c:21:3-21:21)
+  [Info][Imprecise] Invalidating expressions: & tmp (49-type-invariants.c:21:3-21:21)
   [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21)
   [Error][Imprecise][Unsound] Function definition missing
 
@@ -39,7 +39,7 @@
     total lines: 7
   [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21)
+  [Info][Imprecise] Invalidating expressions: & s (49-type-invariants.c:21:3-21:21)
+  [Info][Imprecise] Invalidating expressions: & tmp (49-type-invariants.c:21:3-21:21)
   [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21)
   [Error][Imprecise][Unsound] Function definition missing

tests/regression/04-mutex/77-type-nested-fields.t

@@ -18,9 +18,9 @@
   [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:31:3-31:20)
   [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:38:3-38:22)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:31:3-31:20)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:31:3-31:20)
+  [Info][Imprecise] Invalidating expressions: & tmp (77-type-nested-fields.c:31:3-31:20)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:38:3-38:22)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:38:3-38:22)
+  [Info][Imprecise] Invalidating expressions: & tmp (77-type-nested-fields.c:38:3-38:22)
   [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:31:3-31:20)
   [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:38:3-38:22)
   [Error][Imprecise][Unsound] Function definition missing

tests/regression/04-mutex/79-type-nested-fields-deep1.t

@@ -18,9 +18,9 @@
   [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:36:3-36:20)
   [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:43:3-43:24)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:36:3-36:20)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:36:3-36:20)
+  [Info][Imprecise] Invalidating expressions: & tmp (79-type-nested-fields-deep1.c:36:3-36:20)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:43:3-43:24)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:43:3-43:24)
+  [Info][Imprecise] Invalidating expressions: & tmp (79-type-nested-fields-deep1.c:43:3-43:24)
   [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:36:3-36:20)
   [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:43:3-43:24)
   [Error][Imprecise][Unsound] Function definition missing

tests/regression/04-mutex/80-type-nested-fields-deep2.t

@@ -18,9 +18,9 @@
   [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:36:3-36:22)
   [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:43:3-43:24)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:36:3-36:22)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:36:3-36:22)
+  [Info][Imprecise] Invalidating expressions: & tmp (80-type-nested-fields-deep2.c:36:3-36:22)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:43:3-43:24)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:43:3-43:24)
+  [Info][Imprecise] Invalidating expressions: & tmp (80-type-nested-fields-deep2.c:43:3-43:24)
   [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:36:3-36:22)
   [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:43:3-43:24)
   [Error][Imprecise][Unsound] Function definition missing

tests/regression/04-mutex/90-distribute-fields-type-1.t

@@ -20,9 +20,9 @@
   [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:31:3-31:20)
   [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:39:3-39:17)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:31:3-31:20)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:31:3-31:20)
+  [Info][Imprecise] Invalidating expressions: & tmp (90-distribute-fields-type-1.c:31:3-31:20)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:39:3-39:17)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:39:3-39:17)
+  [Info][Imprecise] Invalidating expressions: & tmp (90-distribute-fields-type-1.c:39:3-39:17)
   [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:31:3-31:20)
   [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:39:3-39:17)
   [Error][Imprecise][Unsound] Function definition missing

tests/regression/04-mutex/91-distribute-fields-type-2.t

@@ -20,9 +20,9 @@
   [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:32:3-32:17)
   [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:40:3-40:17)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:32:3-32:17)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:32:3-32:17)
+  [Info][Imprecise] Invalidating expressions: & tmp (91-distribute-fields-type-2.c:32:3-32:17)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:40:3-40:17)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:40:3-40:17)
+  [Info][Imprecise] Invalidating expressions: & tmp (91-distribute-fields-type-2.c:40:3-40:17)
   [Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:32:3-32:17)
   [Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:40:3-40:17)
   [Error][Imprecise][Unsound] Function definition missing

tests/regression/04-mutex/92-distribute-fields-type-deep.t

@@ -20,9 +20,9 @@
   [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:36:3-36:20)
   [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:44:3-44:17)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:36:3-36:20)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:36:3-36:20)
+  [Info][Imprecise] Invalidating expressions: & tmp (92-distribute-fields-type-deep.c:36:3-36:20)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:44:3-44:17)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:44:3-44:17)
+  [Info][Imprecise] Invalidating expressions: & tmp (92-distribute-fields-type-deep.c:44:3-44:17)
   [Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:36:3-36:20)
   [Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:44:3-44:17)
   [Error][Imprecise][Unsound] Function definition missing

tests/regression/04-mutex/93-distribute-fields-type-global.t

@@ -18,7 +18,7 @@
     total lines: 7
   [Info][Unsound] Write to unknown address: privatization is unsound. (93-distribute-fields-type-global.c:13:3-13:29)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (93-distribute-fields-type-global.c:13:3-13:29)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29)
+  [Info][Imprecise] Invalidating expressions: & s (93-distribute-fields-type-global.c:13:3-13:29)
+  [Info][Imprecise] Invalidating expressions: & tmp (93-distribute-fields-type-global.c:13:3-13:29)
   [Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:13:3-13:29)
   [Error][Imprecise][Unsound] Function definition missing