Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 4 commits into from
Dec 15, 2023
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
8a2a977
Do not use plain CIL printers in user messages
sim642 Dec 14, 2023
4b77174
Make BaseInvariant fallback reason printing lazy
sim642 Dec 14, 2023
0dd4396
Make Offset.Type_of_error string construction lazy
sim642 Dec 14, 2023
86ab239
Promote cram tests after invalidating expressions output change
sim642 Dec 14, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/analyses/base.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
16 changes: 8 additions & 8 deletions src/analyses/baseInvariant.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
14 changes: 8 additions & 6 deletions src/cdomains/offset.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
)
8 changes: 4 additions & 4 deletions tests/regression/04-mutex/49-type-invariants.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
4 changes: 2 additions & 2 deletions tests/regression/04-mutex/77-type-nested-fields.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions tests/regression/04-mutex/79-type-nested-fields-deep1.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions tests/regression/04-mutex/80-type-nested-fields-deep2.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions tests/regression/04-mutex/90-distribute-fields-type-1.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions tests/regression/04-mutex/91-distribute-fields-type-2.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions tests/regression/04-mutex/92-distribute-fields-type-deep.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions tests/regression/04-mutex/93-distribute-fields-type-global.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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