Merge pull request #278 from goblint/assert-analysis

Move assert result output from base to separate assert analysis

includes/goblint.h

@@ -0,0 +1,3 @@
+void __goblint_check(int);
+void __goblint_assume(int);
+void __goblint_assert(int);

scripts/update_suite.rb

@@ -295,7 +295,7 @@ def parse_tests (lines)
         tests[i] = "fail"
       elsif obj =~ /UNKNOWN/ then
         tests[i] = "unknown"
-      elsif obj =~ /assert.*\(/ then
+      elsif obj =~ /(assert|__goblint_check).*\(/ then
         if obj =~ /FAIL/ then
           tests[i] = "fail"
         elsif obj =~ /UNKNOWN/ then

src/analyses/apron/apronAnalysis.apron.ml

@@ -3,6 +3,7 @@
 open Prelude.Ana
 open Analyses
 open ApronDomain
+open GobConfig
 
 module M = Messages
 
@@ -400,15 +401,26 @@ struct
         invalidate_one ask ctx st lval
       ) st rs
 
+  let assert_fn ctx e refine =
+    if not refine then
+      ctx.local
+    else
+      (* copied from branch *)
+      let st = ctx.local in
+      let res = assign_from_globals_wrapper (Analyses.ask_of_ctx ctx) ctx.global st e (fun apr' e' ->
+          (* not an assign, but must remove g#in-s still *)
+          AD.assert_inv apr' e' false
+        )
+      in
+      if AD.is_bot_env res then raise Deadcode;
+      {st with apr = res}
+
   let special ctx r f args =
     let ask = Analyses.ask_of_ctx ctx in
     let st = ctx.local in
     let desc = LibraryFunctions.find f in
     match desc.special args, f.vname with
-    (* TODO: assert handling from https://github.com/goblint/analyzer/pull/278 *)
-    | Assert expression, _ -> st
-    | Unknown, "__goblint_check" -> st
-    | Unknown, "__goblint_commit" -> st
+    | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine
     | ThreadJoin { thread = id; ret_var = retvar }, _ ->
       (
         (* Forget value that thread return is assigned to *)

src/analyses/assert.ml

@@ -0,0 +1,91 @@
+open Prelude.Ana
+open Analyses
+open GobConfig
+
+module Spec : Analyses.MCPSpec =
+struct
+  include Analyses.DefaultSpec
+
+  let name () = "assert"
+  module D = Lattice.Unit
+  module G = Lattice.Unit
+  module C = Lattice.Unit
+
+  (* transfer functions *)
+  let assign ctx (lval:lval) (rval:exp) : D.t =
+    ctx.local
+
+  let branch ctx (exp:exp) (tv:bool) : D.t =
+    ctx.local
+
+  let body ctx (f:fundec) : D.t =
+    ctx.local
+
+  let return ctx (exp:exp option) (f:fundec) : D.t =
+    ctx.local
+
+  let enter ctx (lval: lval option) (fd:fundec) (args:exp list) : (D.t * D.t) list =
+    [ctx.local, ctx.local]
+
+  let combine ctx (lval:lval option) fexp (fd:fundec) (args:exp list) fc (au:D.t) : D.t =
+    au
+
+  let assert_fn ctx e check refine =
+
+    let check_assert e st =
+      match ctx.ask (Queries.EvalInt e) with
+      | v when Queries.ID.is_bool v ->
+        begin match Queries.ID.to_bool v with
+          | Some false ->  `Lifted false
+          | Some true  ->  `Lifted true
+          | _ -> `Top
+        end
+      | v when Queries.ID.is_bot v -> `Bot
+      | _ -> `Top
+    in
+    let expr = sprint d_exp e in
+    let warn warn_fn ?annot msg = if check then
+        if get_bool "dbg.regression" then ( (* This only prints unexpected results (with the difference) as indicated by the comment behind the assert (same as used by the regression test script). *)
+          let loc = !M.current_loc in
+          let line = List.at (List.of_enum @@ File.lines_of loc.file) (loc.line-1) in
+          let open Str in
+          let expected = if string_match (regexp ".+//.*\\(FAIL\\|UNKNOWN\\).*") line 0 then Some (matched_group 1 line) else None in
+          if expected <> annot then (
+            let result = if annot = None && (expected = Some ("NOWARN") || (expected = Some ("UNKNOWN") && not (String.exists line "UNKNOWN!"))) then "improved" else "failed" in
+            (* Expressions with logical connectives like a && b are calculated in temporary variables by CIL. Instead of the original expression, we then see something like tmp___0. So we replace expr in msg by the original source if this is the case. *)
+            let assert_expr = if string_match (regexp ".*assert(\\(.+\\));.*") line 0 then matched_group 1 line else expr in
+            let msg = if expr <> assert_expr then String.nreplace ~str:msg ~sub:expr ~by:assert_expr else msg in
+            warn_fn (msg ^ " Expected: " ^ (expected |? "SUCCESS") ^ " -> " ^ result)
+          )
+        ) else
+          warn_fn msg
+    in
+    (* TODO: use format instead of %s for the following messages *)
+    match check_assert e ctx.local with
+    | `Lifted false ->
+      warn (M.error ~category:Assert "%s") ~annot:"FAIL" ("Assertion \"" ^ expr ^ "\" will fail.");
+      if refine then raise Analyses.Deadcode else ctx.local
+    | `Lifted true ->
+      warn (M.success ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" will succeed");
+      ctx.local
+    | `Bot ->
+      M.error ~category:Assert "%s" ("Assertion \"" ^ expr ^ "\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)");
+      ctx.local
+    | `Top ->
+      warn (M.warn ~category:Assert "%s") ~annot:"UNKNOWN" ("Assertion \"" ^ expr ^ "\" is unknown.");
+      ctx.local
+
+  let special ctx (lval: lval option) (f:varinfo) (args:exp list) : D.t =
+    let desc = LibraryFunctions.find f in
+    match desc.special args, f.vname with
+    | Assert { exp; check; refine }, _ -> assert_fn ctx exp check refine
+    | _, _ -> ctx.local
+
+  let startstate v = D.bot ()
+  let threadenter ctx lval f args = [D.top ()]
+  let threadspawn ctx lval f args fctx = ctx.local
+  let exitstate  v = D.top ()
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)

src/analyses/base.ml

@@ -1030,6 +1030,7 @@ struct
     let r = match eval_rv_no_ask_evalint ask gs st e with
       | `Int i -> `Lifted i (* cast should be unnecessary, eval_rv should guarantee right ikind already *)
       | `Bot   -> Queries.ID.top () (* out-of-scope variables cause bot, but query result should then be unknown *)
+      | `Top   -> Queries.ID.top () (* some float computations cause top (57-float/01-base), but query result should then be unknown *)
       | v      -> M.debug ~category:Analyzer "Base EvalInt %a query answering bot instead of %a" d_exp e VD.pretty v; Queries.ID.bot ()
     in
     if M.tracing then M.traceu "evalint" "base query_evalint %a -> %a\n" d_exp e Queries.ID.pretty r;
@@ -2425,56 +2426,14 @@ struct
       if addrs <> [] then M.debug ~category:Analyzer "Spawning functions from unknown function: %a" (d_list ", " d_varinfo) addrs;
       List.filter_map (create_thread None None) addrs
 
-  let assert_fn ctx e should_warn change =
-
-    let check_assert e st =
-      match eval_rv (Analyses.ask_of_ctx ctx) ctx.global st e with
-      | `Int v when ID.is_bool v ->
-        begin match ID.to_bool v with
-          | Some false ->  `Lifted false
-          | Some true  ->  `Lifted true
-          | _ -> `Top
-        end
-      | `Bot -> `Bot
-      | _ -> `Top
-    in
-    let expr = sprint d_exp e in
-    let warn warn_fn ?annot msg = if should_warn then
-        if get_bool "dbg.regression" then ( (* This only prints unexpected results (with the difference) as indicated by the comment behind the assert (same as used by the regression test script). *)
-          let loc = !M.current_loc in
-          let line = List.at (List.of_enum @@ File.lines_of loc.file) (loc.line-1) in
-          let open Str in
-          let expected = if string_match (regexp ".+//.*\\(FAIL\\|UNKNOWN\\).*") line 0 then Some (matched_group 1 line) else None in
-          if expected <> annot then (
-            let result = if annot = None && (expected = Some ("NOWARN") || (expected = Some ("UNKNOWN") && not (String.exists line "UNKNOWN!"))) then "improved" else "failed" in
-            (* Expressions with logical connectives like a && b are calculated in temporary variables by CIL. Instead of the original expression, we then see something like tmp___0. So we replace expr in msg by the original source if this is the case. *)
-            let assert_expr = if string_match (regexp ".*assert(\\(.+\\));.*") line 0 then matched_group 1 line else expr in
-            let msg = if expr <> assert_expr then String.nreplace ~str:msg ~sub:expr ~by:assert_expr else msg in
-            warn_fn (msg ^ " Expected: " ^ (expected |? "SUCCESS") ^ " -> " ^ result)
-          )
-        ) else
-          warn_fn msg
-    in
-    (* TODO: use format instead of %s for the following messages *)
-    match check_assert e ctx.local with
-    | `Lifted false ->
-      warn (M.error ~category:Assert "%s") ~annot:"FAIL" ("Assertion \"" ^ expr ^ "\" will fail.");
-      if change then raise Analyses.Deadcode else ctx.local
-    | `Lifted true ->
-      warn (M.success ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" will succeed");
-      ctx.local
-    | `Bot ->
-      M.error ~category:Assert "%s" ("Assertion \"" ^ expr ^ "\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)");
-      ctx.local
-    | `Top ->
-      warn (M.warn ~category:Assert "%s") ~annot:"UNKNOWN" ("Assertion \"" ^ expr ^ "\" is unknown.");
-      (* make the state meet the assertion in the rest of the code *)
-      if not change then ctx.local else begin
-        let newst = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local e true in
-        (* if check_assert e newst <> `Lifted true then
-            M.warn ~category:Assert ~msg:("Invariant \"" ^ expr ^ "\" does not stick.") (); *)
-        newst
-      end
+  let assert_fn ctx e refine =
+    (* make the state meet the assertion in the rest of the code *)
+    if not refine then ctx.local else begin
+      let newst = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local e true in
+      (* if check_assert e newst <> `Lifted true then
+          M.warn ~category:Assert ~msg:("Invariant \"" ^ expr ^ "\" does not stick.") (); *)
+      newst
+    end
 
   let special_unknown_invalidate ctx ask gs st f args =
     (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise "Unknown function ptr called");
@@ -2721,10 +2680,7 @@ struct
       end
     (* Handling the assertions *)
     | Unknown, "__assert_rtn" -> raise Deadcode (* gcc's built-in assert *)
-    (* TODO: assert handling from https://github.com/goblint/analyzer/pull/278 *)
-    | Unknown, "__goblint_check" -> assert_fn ctx (List.hd args) true false
-    | Unknown, "__goblint_commit" -> assert_fn ctx (List.hd args) false true
-    | Assert e, _ -> assert_fn ctx e (get_bool "dbg.debug") (not (get_bool "dbg.debug")) (* __goblint_assert previously had [true true] and Assert should too, but cannot until #278 *)
+    | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine
     | _, _ -> begin
         let st =
           special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) gs st f args

src/analyses/libraryDesc.ml

@@ -34,7 +34,7 @@ type special =
   | Malloc of Cil.exp
   | Calloc of { count: Cil.exp; size: Cil.exp; }
   | Realloc of { ptr: Cil.exp; size: Cil.exp; }
-  | Assert of Cil.exp
+  | Assert of { exp: Cil.exp; check: bool; refine: bool; }
   | Lock of { lock: Cil.exp; try_: bool; write: bool; return_on_success: bool; }
   | Unlock of Cil.exp
   | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; }
@@ -102,7 +102,6 @@ let special_of_old classify_name = fun args ->
   | `Malloc e -> Malloc e
   | `Calloc (count, size) -> Calloc { count; size; }
   | `Realloc (ptr, size) -> Realloc { ptr; size; }
-  | `Assert e -> Assert e
   | `Lock (try_, write, return_on_success) -> Lock { lock = List.hd args; try_; write; return_on_success; }
   | `Unlock -> Unlock (List.hd args)
   | `ThreadCreate (thread, start_routine, arg) -> ThreadCreate { thread; start_routine; arg; }

src/analyses/libraryFunctions.ml

@@ -46,9 +46,9 @@ let linux_descs_list: (string * LibraryDesc.t) list = (* LibraryDsl. *) [
 (** Goblint functions. *)
 let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__goblint_unknown", unknown [drop' [w]]);
-    ("__goblint_check", unknown [drop' []]);
-    ("__goblint_commit", unknown [drop' []]);
-    ("__goblint_assert", special [__ "cond" []] @@ fun cond -> Assert cond);
+    ("__goblint_check", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = false });
+    ("__goblint_assume", special [__ "exp" []] @@ fun exp -> Assert { exp; check = false; refine = true });
+    ("__goblint_assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" });
   ]
 
 (** zstd functions.
@@ -125,7 +125,6 @@ type categories = [
   | `Malloc       of exp
   | `Calloc       of exp * exp
   | `Realloc      of exp * exp
-  | `Assert       of exp
   | `Lock         of bool * bool * bool  (* try? * write? * return  on success *)
   | `Unlock
   | `ThreadCreate of exp * exp * exp (* id * f  * x       *)

src/analyses/termination.ml

@@ -91,7 +91,7 @@ let makeVar fd loc name =
   with Not_found ->
     let typ = intType in (* TODO the type should be the same as the one of the original loop counter *)
     Goblintutil.create_var (makeLocalVar fd id ~init:(SingleInit zero) typ)
-let f_commit = Lval (var (emptyFunction "__goblint_commit").svar)
+let f_assume = Lval (var (emptyFunction "__goblint_assume").svar)
 let f_check  = Lval (var (emptyFunction "__goblint_check").svar)
 class loopInstrVisitor (fd : fundec) = object(self)
   inherit nopCilVisitor
@@ -128,8 +128,8 @@ class loopInstrVisitor (fd : fundec) = object(self)
         let typ = intType in
         let e1 = BinOp (Eq, Lval t, BinOp (MinusA, Lval x, Lval d1, typ), typ) in
         let e2 = BinOp (Eq, Lval t, BinOp (MinusA, Lval d2, Lval x, typ), typ) in
-        let inv1 = mkStmtOneInstr @@ Call (None, f_commit, [e1], loc, eloc) in
-        let inv2 = mkStmtOneInstr @@ Call (None, f_commit, [e2], loc, eloc) in
+        let inv1 = mkStmtOneInstr @@ Call (None, f_assume, [e1], loc, eloc) in
+        let inv2 = mkStmtOneInstr @@ Call (None, f_assume, [e2], loc, eloc) in
         (match b.bstmts with
          | cont :: cond :: ss ->
            (* changing succs/preds directly doesn't work -> need to replace whole stmts  *)

src/maingoblint.ml

@@ -220,6 +220,7 @@ let preprocess_files () =
   get_string_list "pre.includes" |> List.map Fpath.v |> List.iter (one_include_f identity);
 
   include_dirs := custom_include_dirs @ !include_dirs;
+  include_files := find_custom_include (Fpath.v "goblint.h") :: !include_files;
 
   (* If we analyze a kernel module, some special includes are needed. *)
   if get_bool "kernel" then (

src/util/options.schema.json

@@ -326,7 +326,8 @@
           "items": { "type": "string" },
           "default": [
             "expRelation", "base", "threadid", "threadflag", "threadreturn",
-            "escape", "mutexEvents", "mutex", "access", "mallocWrapper", "mhp"
+            "escape", "mutexEvents", "mutex", "access", "mallocWrapper", "mhp",
+            "assert"
           ]
         },
         "path_sens": {
@@ -1125,6 +1126,19 @@
             }
           },
           "additionalProperties": false
+        },
+        "assert": {
+          "title": "sem.assert",
+          "type": "object",
+          "properties": {
+            "refine": {
+              "title": "sem.assert.refine",
+              "description": "Standard assert refines state",
+              "type": "boolean",
+              "default": true
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false

src/util/wideningThresholds.ml

@@ -41,8 +41,8 @@ class extractInvariantsVisitor (exps) = object
     | Call (_, Lval (Var f, NoOffset), args, _, _) ->
       let desc = LibraryFunctions.find f in
       begin match desc.special args with
-        | Assert e ->
-          EH.replace exps e ();
+        | Assert { exp; _ } ->
+          EH.replace exps exp ();
           DoChildren
         | _ ->
           DoChildren

tests/incremental/00-basic/00-local.c

@@ -2,6 +2,6 @@
 
 int main() {
     int x = 1;
-    assert(x == 1); // success before, success after
+    __goblint_check(x == 1); // success before, success after
     return 0;
 }

tests/incremental/00-basic/00-local.patch

@@ -5,9 +5,9 @@
 
  int main() {
 -    int x = 1;
--    assert(x == 1); // success before, success after
+-    __goblint_check(x == 1); // success before, success after
 +    int x = 2;
-+    assert(x == 2); // success before, success after
++    __goblint_check(x == 2); // success before, success after
      return 0;
  }
 \ No newline at end of file

tests/incremental/00-basic/02-changed_start_state1.c

@@ -7,7 +7,7 @@ int main() {
     // If the change of the start state of main would not be propagated by the call to side on all start variables, the
     // asserts in the incremental run would wrongly fail. Side however only joins with the previous value instead of
     // overwriting, therefore the current imprecision.
-    assert(g == 1);
-    assert(g != 2);
+    __goblint_check(g == 1);
+    __goblint_check(g != 2);
     return 0;
 }

tests/incremental/00-basic/02-changed_start_state1.patch

@@ -11,9 +11,9 @@
      // If the change of the start state of main would not be propagated by the call to side on all start variables, the
      // asserts in the incremental run would wrongly fail. Side however only joins with the previous value instead of
      // overwriting, therefore the current imprecision.
--    assert(g == 1);
--    assert(g != 2);
-+    assert(g != 1); // TODO (restarting)
-+    assert(g == 2); // TODO
+-    __goblint_check(g == 1);
+-    __goblint_check(g != 2);
++    __goblint_check(g != 1); // TODO (restarting)
++    __goblint_check(g == 2); // TODO
      return 0;
  }

tests/incremental/00-basic/03-changed_start_state2.c

@@ -7,7 +7,7 @@ int main() {
     // If the change of the start state of main would not be propagated by the call to side on all start variables, the
     // asserts in the incremental run would wrongly fail. Side however only joins with the previous value instead of
     // overwriting, therefore the current imprecision.
-    assert(g == 1);
-    assert(g != 2);
+    __goblint_check(g == 1);
+    __goblint_check(g != 2);
     return 0;
 }