Skip to content

Add final messages about unsound results #1191

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

Merged
merged 10 commits into from
Sep 29, 2023
Merged

Add final messages about unsound results #1191

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
0caab0f
Add final messages (issue #1190)
sim642 Sep 26, 2023
857b6c1
Add fixpoint not reached final message
sim642 Sep 26, 2023
f2d2c1c
Add function definition missing final message
sim642 Sep 26, 2023
2430e6e
Add both branches dead final message
sim642 Sep 26, 2023
5060978
Add ASM final message
sim642 Sep 26, 2023
a28a8ff
Add no suitable function final message
sim642 Sep 26, 2023
684a74c
Update cram tests with final messages
sim642 Sep 26, 2023
e780a83
Print final messages deterministically
sim642 Sep 28, 2023
3c7555b
Remove context from noloc and final messages
sim642 Sep 28, 2023
b5ebff6
Merge branch 'master' into final-errors
sim642 Sep 29, 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
6 changes: 4 additions & 2 deletions src/analyses/libraryFunctions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1230,8 +1230,10 @@ let unknown_desc f =
[]
in
(* TODO: remove hack when all classify are migrated *)
if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then
M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname;
if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then (
M.msg_final Error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing";
M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname
);
LibraryDesc.of_old ~attrs old_accesses

let find f =
Expand Down
3 changes: 2 additions & 1 deletion src/framework/analyses.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -643,7 +643,8 @@ struct
let vdecl ctx _ = ctx.local

let asm x =
ignore (M.info ~category:Unsound "ASM statement ignored.");
M.msg_final Info ~category:Unsound "ASM ignored";
M.info ~category:Unsound "ASM statement ignored.";
x.local (* Just ignore. *)

let skip x = x.local (* Just ignore. *)
Expand Down
2 changes: 2 additions & 0 deletions src/framework/constraints.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -785,6 +785,7 @@ struct
in
let funs = List.filter_map one_function functions in
if [] = funs then begin
M.msg_final Warning ~category:Unsound ~tags:[Category Call] "No suitable function to call";
M.warn ~category:Unsound ~tags:[Category Call] "No suitable function to be called at call site. Continuing with state before call.";
d (* because LevelSliceLifter *)
end else
Expand Down Expand Up @@ -1390,6 +1391,7 @@ struct
let cilinserted = if loc.synthetic then "(possibly inserted by CIL) " else "" in
M.warn ~loc:(Node g) ~tags:[CWE (if tv then 571 else 570)] ~category:Deadcode "condition '%a' %sis always %B" d_exp exp cilinserted tv
| `Bot when not (CilType.Exp.equal exp one) -> (* all branches dead *)
M.msg_final Error ~category:Analyzer ~tags:[Category Unsound] "Both branches dead";
M.error ~loc:(Node g) ~category:Analyzer ~tags:[Category Unsound] "both branches over condition '%a' are dead" d_exp exp
| `Bot (* all branches dead, fine at our inserted Neg(1)-s because no Pos(1) *)
| `Top -> (* may be both true and false *)
Expand Down
3 changes: 3 additions & 0 deletions src/solvers/postSolver.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,10 +82,13 @@ module Verify: F =

let complain_constraint x ~lhs ~rhs =
AnalysisState.verified := Some false;
M.msg_final Error ~category:Unsound "Fixpoint not reached";
ignore (Pretty.printf "Fixpoint not reached at %a\n @[Solver computed:\n%a\nRight-Hand-Side:\n%a\nDifference: %a\n@]" S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs))

let complain_side x y ~lhs ~rhs =
AnalysisState.verified := Some false;

M.msg_final Error ~category:Unsound "Fixpoint not reached";
ignore (Pretty.printf "Fixpoint not reached at %a\nOrigin: %a\n @[Solver computed:\n%a\nSide-effect:\n%a\nDifference: %a\n@]" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs))

let one_side ~vh ~x ~y ~d =
Expand Down
27 changes: 25 additions & 2 deletions src/util/messages.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -248,12 +248,24 @@ let add m =
Table.add m
)

let final_table: unit Table.MH.t = Table.MH.create 13

let add_final m =
Table.MH.replace final_table m ()

let finalize () =
if get_bool "warn.deterministic" then (
!Table.messages_list
|> List.sort Message.compare
|> List.iter print
)
);
Table.MH.to_seq_keys final_table
|> List.of_seq
|> List.sort Message.compare
|> List.iter (fun m ->
print m;
Table.add m
)

let current_context: ControlSpecC.t option ref = ref None

Expand Down Expand Up @@ -282,7 +294,7 @@ let msg_noloc severity ?(tags=[]) ?(category=Category.Unknown) fmt =
if !AnalysisState.should_warn && Severity.should_warn severity && (Category.should_warn category || Tags.should_warn tags) then (
let finish doc =
let text = GobPretty.show doc in
add {tags = Category category :: tags; severity; multipiece = Single {loc = None; text; context = msg_context ()}}
add {tags = Category category :: tags; severity; multipiece = Single {loc = None; text; context = None}}
in
Pretty.gprintf finish fmt
)
Expand Down Expand Up @@ -316,4 +328,15 @@ let debug_noloc ?tags = msg_noloc Debug ?tags
let success ?loc = msg Success ?loc
let success_noloc ?tags = msg_noloc Success ?tags

let msg_final severity ?(tags=[]) ?(category=Category.Unknown) fmt =
if !AnalysisState.should_warn then (
let finish doc =
let text = GobPretty.show doc in
add_final {tags = Category category :: tags; severity; multipiece = Single {loc = None; text; context = None}}
in
Pretty.gprintf finish fmt
)
else
GobPretty.igprintf () fmt

include Tracing
1 change: 1 addition & 0 deletions src/util/server.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -264,6 +264,7 @@ let node_locator: Locator.t ResettableLazy.t =

let analyze ?(reset=false) (s: t) =
Messages.Table.(MH.clear messages_table);
Messages.(Table.MH.clear final_table);
Messages.Table.messages_list := [];
let file, reparsed = reparse s in
if reset then (
Expand Down
2 changes: 2 additions & 0 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 @@ -21,6 +21,7 @@
[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)
[Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21)
[Error][Imprecise][Unsound] Function definition missing

$ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21)
Expand All @@ -45,3 +46,4 @@
[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)
[Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21)
[Error][Imprecise][Unsound] Function definition missing
1 change: 1 addition & 0 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 @@ -27,3 +27,4 @@
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (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
1 change: 1 addition & 0 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 @@ -27,3 +27,4 @@
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (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
1 change: 1 addition & 0 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 @@ -27,3 +27,4 @@
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (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
1 change: 1 addition & 0 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 @@ -29,3 +29,4 @@
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (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
1 change: 1 addition & 0 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 @@ -29,3 +29,4 @@
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (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
1 change: 1 addition & 0 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 @@ -29,3 +29,4 @@
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (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
1 change: 1 addition & 0 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 @@ -23,3 +23,4 @@
[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)
[Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:13:3-13:29)
[Error][Imprecise][Unsound] Function definition missing
2 changes: 2 additions & 0 deletions tests/regression/06-symbeq/16-type_rc.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ Disable info messages because race summary contains (safe) memory location count
write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:35:3-35:37#top]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9)
[Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24)
[Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14)
[Error][Imprecise][Unsound] Function definition missing

$ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 16-type_rc.c
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:21:3-21:15)
Expand All @@ -20,3 +21,4 @@ Disable info messages because race summary contains (safe) memory location count
write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#top]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15)
[Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24)
[Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14)
[Error][Imprecise][Unsound] Function definition missing
2 changes: 2 additions & 0 deletions tests/regression/06-symbeq/21-mult_accs_rc.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ Disable info messages because race summary contains (safe) memory location count
[Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:13:3-13:14)
[Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:15:3-15:14)
[Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:27:3-27:14)
[Error][Imprecise][Unsound] Function definition missing

$ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 21-mult_accs_rc.c
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:14:3-14:32)
Expand All @@ -30,3 +31,4 @@ Disable info messages because race summary contains (safe) memory location count
[Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:13:3-13:14)
[Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:15:3-15:14)
[Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:27:3-27:14)
[Error][Imprecise][Unsound] Function definition missing