Skip to content

Commit b0299eb

Browse files
sim642sim642
authored
Merge pull request #1292 from goblint/plain-cil-printer
Make some exception printers lazy, do not use plain CIL printers in messages
2 parents ad43006 + 86ab239 commit b0299eb

11 files changed

+35
-33
lines changed

‎src/analyses/base.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1878,7 +1878,7 @@ struct
18781878

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

‎src/analyses/baseInvariant.ml‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -243,12 +243,12 @@ struct
243243
refine_lv_fallback ctx a gs st lval value tv
244244
| None ->
245245
if M.tracing then M.traceu "invariant" "Doing nothing.\n";
246-
M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_plainexp exp;
246+
M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_exp exp;
247247
st
248248

249249
let invariant ctx a gs st exp tv: D.t =
250250
let fallback reason st =
251-
if M.tracing then M.tracel "inv" "Can't handle %a.\n%s\n" d_plainexp exp reason;
251+
if M.tracing then M.tracel "inv" "Can't handle %a.\n%t\n" d_plainexp exp reason;
252252
invariant_fallback ctx a gs st exp tv
253253
in
254254
(* inverse values for binary operation a `op` b == c *)
@@ -689,7 +689,7 @@ struct
689689
(* Mixed Float and Int cases should never happen, as there are no binary operators with one float and one int parameter ?!*)
690690
| Int _, Float _ | Float _, Int _ -> failwith "ill-typed program";
691691
(* | Address a, Address b -> ... *)
692-
| a1, a2 -> fallback (GobPretty.sprintf "binop: got abstract values that are not Int: %a and %a" VD.pretty a1 VD.pretty a2) st)
692+
| a1, a2 -> fallback (fun () -> Pretty.dprintf "binop: got abstract values that are not Int: %a and %a" VD.pretty a1 VD.pretty a2) st)
693693
(* use closures to avoid unused casts *)
694694
in (match c_typed with
695695
| 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
778778
| TFloat (fk, _), FLongDouble
779779
| TFloat (FDouble as fk, _), FDouble
780780
| TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
781-
| _ -> fallback ("CastE: incompatible types") st)
781+
| _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
782782
| CastE ((TInt (ik, _)) as t, e), Int c
783783
| 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. *)
784784
(match eval e st with
@@ -791,11 +791,11 @@ struct
791791
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? *)
792792
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';
793793
inv_exp (Int c') e st
794-
| x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st
794+
| x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st
795795
else
796-
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
797-
| v -> fallback (GobPretty.sprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
798-
| e, _ -> fallback (GobPretty.sprintf "%a not implemented" d_plainexp e) st
796+
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
797+
| v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
798+
| e, _ -> fallback (fun () -> Pretty.dprintf "%a not implemented" d_plainexp e) st
799799
in
800800
if eval_bool exp st = Some (not tv) then contra st (* we already know that the branch is dead *)
801801
else

‎src/cdomains/offset.ml‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -142,15 +142,11 @@ struct
142142
| TPtr (t,_), `Index (i,o) -> type_of ~base:t o
143143
| TComp (ci,_), `Field (f,o) ->
144144
let fi = try getCompField ci f.fname
145-
with Not_found ->
146-
let s = GobPretty.sprintf "Addr.type_offset: field %s not found in type %a" f.fname d_plaintype t in
147-
raise (Type_of_error (t, s))
145+
with Not_found -> raise (Type_of_error (t, show o))
148146
in type_of ~base:fi.ftype o
149147
(* TODO: Why? Imprecise on zstd-thread-pool regression tests. *)
150148
(* | TComp _, `Index (_,o) -> type_of ~base:t o (* this happens (hmmer, perlbench). safe? *) *)
151-
| t,o ->
152-
let s = GobPretty.sprintf "Addr.type_offset: could not follow offset in type. type: %a, offset: %a" d_plaintype t pretty o in
153-
raise (Type_of_error (t, s))
149+
| t, o -> raise (Type_of_error (t, show o))
154150

155151
let rec prefix (x: t) (y: t): t option = match x,y with
156152
| `Index (x, xs), `Index (y, ys) when Idx.equal x y -> prefix xs ys
@@ -261,3 +257,9 @@ struct
261257
| `Index (i,o) -> Index (i, to_cil o)
262258
| `Field (f,o) -> Field (f, to_cil o)
263259
end
260+
261+
262+
let () = Printexc.register_printer (function
263+
| Type_of_error (t, o) -> Some (GobPretty.sprintf "Offset.Type_of_error(%a, %s)" d_plaintype t o)
264+
| _ -> None (* for other exceptions *)
265+
)

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,8 @@
1616
total lines: 7
1717
[Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21)
1818
[Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21)
19-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21)
20-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21)
19+
[Info][Imprecise] Invalidating expressions: & s (49-type-invariants.c:21:3-21:21)
20+
[Info][Imprecise] Invalidating expressions: & tmp (49-type-invariants.c:21:3-21:21)
2121
[Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21)
2222
[Error][Imprecise][Unsound] Function definition missing
2323

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

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,9 @@
1818
[Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:31:3-31:20)
1919
[Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:38:3-38:22)
2020
[Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:31:3-31:20)
21-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:31:3-31:20)
21+
[Info][Imprecise] Invalidating expressions: & tmp (77-type-nested-fields.c:31:3-31:20)
2222
[Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:38:3-38:22)
23-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:38:3-38:22)
23+
[Info][Imprecise] Invalidating expressions: & tmp (77-type-nested-fields.c:38:3-38:22)
2424
[Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:31:3-31:20)
2525
[Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:38:3-38:22)
2626
[Error][Imprecise][Unsound] Function definition missing

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,9 @@
1818
[Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:36:3-36:20)
1919
[Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:43:3-43:24)
2020
[Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:36:3-36:20)
21-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:36:3-36:20)
21+
[Info][Imprecise] Invalidating expressions: & tmp (79-type-nested-fields-deep1.c:36:3-36:20)
2222
[Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:43:3-43:24)
23-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:43:3-43:24)
23+
[Info][Imprecise] Invalidating expressions: & tmp (79-type-nested-fields-deep1.c:43:3-43:24)
2424
[Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:36:3-36:20)
2525
[Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:43:3-43:24)
2626
[Error][Imprecise][Unsound] Function definition missing

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,9 @@
1818
[Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:36:3-36:22)
1919
[Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:43:3-43:24)
2020
[Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:36:3-36:22)
21-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:36:3-36:22)
21+
[Info][Imprecise] Invalidating expressions: & tmp (80-type-nested-fields-deep2.c:36:3-36:22)
2222
[Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:43:3-43:24)
23-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:43:3-43:24)
23+
[Info][Imprecise] Invalidating expressions: & tmp (80-type-nested-fields-deep2.c:43:3-43:24)
2424
[Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:36:3-36:22)
2525
[Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:43:3-43:24)
2626
[Error][Imprecise][Unsound] Function definition missing

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,9 +20,9 @@
2020
[Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:31:3-31:20)
2121
[Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:39:3-39:17)
2222
[Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:31:3-31:20)
23-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:31:3-31:20)
23+
[Info][Imprecise] Invalidating expressions: & tmp (90-distribute-fields-type-1.c:31:3-31:20)
2424
[Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:39:3-39:17)
25-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:39:3-39:17)
25+
[Info][Imprecise] Invalidating expressions: & tmp (90-distribute-fields-type-1.c:39:3-39:17)
2626
[Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:31:3-31:20)
2727
[Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:39:3-39:17)
2828
[Error][Imprecise][Unsound] Function definition missing

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,9 +20,9 @@
2020
[Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:32:3-32:17)
2121
[Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:40:3-40:17)
2222
[Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:32:3-32:17)
23-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:32:3-32:17)
23+
[Info][Imprecise] Invalidating expressions: & tmp (91-distribute-fields-type-2.c:32:3-32:17)
2424
[Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:40:3-40:17)
25-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:40:3-40:17)
25+
[Info][Imprecise] Invalidating expressions: & tmp (91-distribute-fields-type-2.c:40:3-40:17)
2626
[Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:32:3-32:17)
2727
[Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:40:3-40:17)
2828
[Error][Imprecise][Unsound] Function definition missing

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,9 +20,9 @@
2020
[Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:36:3-36:20)
2121
[Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:44:3-44:17)
2222
[Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:36:3-36:20)
23-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:36:3-36:20)
23+
[Info][Imprecise] Invalidating expressions: & tmp (92-distribute-fields-type-deep.c:36:3-36:20)
2424
[Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:44:3-44:17)
25-
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:44:3-44:17)
25+
[Info][Imprecise] Invalidating expressions: & tmp (92-distribute-fields-type-deep.c:44:3-44:17)
2626
[Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:36:3-36:20)
2727
[Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:44:3-44:17)
2828
[Error][Imprecise][Unsound] Function definition missing

0 commit comments

Comments
 (0)