Merge pull request #219 from goblint/no_verify_allow_warnings

Introduce option `warn` with options `post | early | never`

conf/incremental.json

@@ -33,5 +33,5 @@
   "printstats": true,
   "result": "none",
   "solver": "td3",
-  "noverify": true
+  "verify": true
 }

conf/minimal_incremental.json

@@ -35,5 +35,5 @@
   "printstats": true,
   "result": "none",
   "solver": "td3",
-  "noverify": true
+  "verify": true
 }

src/framework/constraints.ml

@@ -1234,8 +1234,9 @@ struct
   open S
 
   let verify (sigma:D.t LH.t) (theta:G.t GH.t) =
+    let should_verify = get_bool "verify" in
     Goblintutil.in_verifying_stage := true;
-    Goblintutil.verified := Some true;
+    (if should_verify then Goblintutil.verified := Some true);
     let complain_l (v:LVar.t) lhs rhs =
       Goblintutil.verified := Some false;
       ignore (Pretty.printf "Fixpoint not reached at %a (%s:%d)\n @[Solver computed:\n%a\nRight-Hand-Side:\n%a\nDifference: %a\n@]"
@@ -1265,12 +1266,12 @@ struct
          * invariant. *)
         let check_local l lv =
           let lv' = sigma' l in
-          if not (D.leq lv lv') then
+          if should_verify && not (D.leq lv lv') then
             complain_sidel v l lv' lv
         in
         let check_glob g gv =
           let gv' = theta' g in
-          if not (G.leq gv gv') then
+          if should_verify && not (G.leq gv gv') then
             complain_sideg v g gv' gv
         in
         let d = rhs sigma' check_local theta' check_glob in

src/framework/control.ml

@@ -411,7 +411,7 @@ struct
         ) else (
           if get_bool "dbg.verbose" then
             print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s.");
-          if get_bool "dbg.earlywarn" then Goblintutil.should_warn := true;
+          if get_string "warn" = "early" then Goblintutil.should_warn := true;
           let lh, gh = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' in
           if save_run <> "" then (
             let analyses = append_opt "save_run" "analyses.marshalled" in
@@ -445,9 +445,9 @@ struct
         compare_with (Slvr.choose_solver (get_string "comparesolver"))
       );
 
-      if get_bool "verify" && compare_runs = [] then (
-        if (get_bool "dbg.verbose") then print_endline "Verifying the result.";
-        Goblintutil.should_warn := true;
+      if (get_bool "verify" || get_string "warn" <> "never") && compare_runs = [] then (
+        if (get_bool "verify" && get_bool "dbg.verbose") then print_endline "Verifying the result.";
+        Goblintutil.should_warn := get_string "warn" <> "never";
         Stats.time "verify" (Vrfyr.verify lh) gh;
       );
 

src/util/defaults.ml

@@ -91,13 +91,13 @@ let _ = ()
       ; reg Std "save_run"        "''"           "Save the result of the solver, the current configuration and meta-data about the run to this directory (if set). The data can then be loaded (without solving again) to do post-processing like generating output in a different format or comparing results."
       ; reg Std "load_run"        "''"           "Load a saved run. See save_run."
       ; reg Std "compare_runs"    "[]"           "Load these saved runs and compare the results. Note that currently only two runs can be compared!"
+      ; reg Std "warn"            "'post'"       "Output warnings: 'post'. Output warnings after solving. Best results. 'never': Do not produce warnings, 'early'. For debugging. Outputs warnings already while solving (may lead to spurious warnings/asserts that would disappear after narrowing)."
 
 (* {4 category [Analyses]} *)
 let _ = ()
       ; reg Analyses "ana.activated"  "['expRelation','base','threadid','threadflag','escape','mutex', 'mallocWrapper']"  "Lists of activated analyses in this phase."
       ; reg Analyses "ana.path_sens"  "['OSEK','OSEK2','mutex','malloc_null','uninit']"  "List of path-sensitive analyses"
       ; reg Analyses "ana.ctx_insens" "['OSEK2','stack_loc','stack_trace_set']"                      "List of context-insensitive analyses"
-      ; reg Analyses "ana.warnings"        "false" "Print soundness warnings."
       ; reg Analyses "ana.cont.localclass" "false" "Analyzes classes defined in main Class."
       ; reg Analyses "ana.cont.class"      "''"    "Analyzes all the member functions of the class (CXX.json file required)."
       ; reg Analyses "ana.osek.oil"        "''"    "Oil file for the analyzed program"
@@ -225,7 +225,6 @@ let _ = ()
       ; reg Debugging "dbg.slice.on"        "false" "Turn slicer on or off."
       ; reg Debugging "dbg.slice.n"         "10"    "How deep function stack do we analyze."
       ; reg Debugging "dbg.limit.widen"     "0"     "Limit for number of widenings per node (0 = no limit)."
-      ; reg Debugging "dbg.earlywarn"       "false" "Output warnings already while solving (may lead to spurious warnings/asserts that would disappear after narrowing)."
       ; reg Debugging "dbg.warn_with_context" "false" "Keep warnings for different contexts apart (currently only done for asserts)."
       ; reg Debugging "dbg.regression"      "false" "Only output warnings for assertions that have an unexpected result (no comment, comment FAIL, comment UNKNOWN)"
       ; reg Debugging "dbg.test.domain"     "false" "Test domain properties"
@@ -296,6 +295,7 @@ let default_schema = "\
   , 'save_run'        : {}
   , 'load_run'        : {}
   , 'compare_runs'    : {}
+  , 'warn'            : {}
   }
 }"
 

src/util/goblintutil.ml

@@ -18,7 +18,7 @@ let jsonFiles : string list ref = ref []
 let has_otherfuns = ref false
 
 (** If this is true we output messages and collect accesses.
-    This is set to true in control.ml before we verify the result (or already before solving if dbg.earlywarn) *)
+    This is set to true in control.ml before we verify the result (or already before solving if warn = 'early') *)
 let should_warn = ref false
 
 let did_overflow = ref false