Merge pull request #1191 from goblint/final-errors

Add final messages about unsound results

Author: sim642

src/analyses/libraryFunctions.ml

@@ -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 =

src/framework/analyses.ml

@@ -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. *)

src/framework/constraints.ml

@@ -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
@@ -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 *)

src/solvers/postSolver.ml

@@ -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 =

src/util/messages.ml

@@ -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
 
@@ -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
   )
@@ -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

src/util/server.ml

@@ -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 (

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

@@ -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)
@@ -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

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

@@ -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

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

@@ -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

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

@@ -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

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

@@ -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

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

@@ -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

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

@@ -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

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

@@ -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

tests/regression/06-symbeq/16-type_rc.t

@@ -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)
@@ -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

tests/regression/06-symbeq/21-mult_accs_rc.t

@@ -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)
@@ -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