Replace int -> _Bool in goblint stubs arguments

lib/goblint/runtime/include/goblint.h

@@ -1,6 +1,6 @@
-void __goblint_check(int exp);
-void __goblint_assume(int exp);
-void __goblint_assert(int exp);
+void __goblint_check(_Bool exp);
+void __goblint_assume(_Bool exp);
+void __goblint_assert(_Bool exp);
 
 void __goblint_assume_join(/* pthread_t thread */); // undeclared argument to avoid pthread.h interfering with Linux kernel headers
 void __goblint_globalize(void *ptr);

lib/goblint/runtime/src/goblint.c

@@ -3,15 +3,15 @@
 
 // Empty implementations (instead of asserts) because annotating documentation promises no-op right now.
 
-void __goblint_check(int exp) {
+void __goblint_check(_Bool exp) {
 
 }
 
-void __goblint_assume(int exp) {
+void __goblint_assume(_Bool exp) {
 
 }
 
-void __goblint_assert(int exp) {
+void __goblint_assert(_Bool exp) {
 
 }
 

lib/libc/stub/include/assert.h

@@ -1,6 +1,6 @@
 #ifndef GOBLINT_NO_ASSERT
 
-void __goblint_assert(int expression);
+void __goblint_assert(_Bool expression);
 #undef assert
 #define assert(expression) __goblint_assert(expression)
 

src/analyses/abortUnless.ml

@@ -30,7 +30,7 @@ struct
     if man.local then
       match f.sformals with
       | [arg] when isIntegralType arg.vtype ->
-        (match man.ask (EvalInt (Lval (Var arg, NoOffset))) with
+        (match man.ask (EvalInt (Lval (Var arg, NoOffset))) with (* TODO: Queries.eval_bool? *)
          | v when Queries.ID.is_bot v -> false
          | v ->
            match Queries.ID.to_bool v with

src/analyses/assert.ml

@@ -14,15 +14,6 @@ struct
   (* transfer functions *)
 
   let assert_fn man e check refine =
-
-    let check_assert e st =
-      match man.ask (Queries.EvalInt e) with
-      | v when Queries.ID.is_bot v -> `Bot
-      | v ->
-        match Queries.ID.to_bool v with
-        | Some b -> `Lifted b
-        | None -> `Top
-    in
     let expr = CilType.Exp.show 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). *)
@@ -41,7 +32,7 @@ struct
           warn_fn msg
     in
     (* TODO: use format instead of %s for the following messages *)
-    match check_assert e man.local with
+    match Queries.eval_bool (Analyses.ask_of_man man) e with
     | `Lifted false ->
       warn (M.error ~category:Assert "%s") ~annot:"FAIL" ("Assertion \"" ^ expr ^ "\" will fail.");
       if refine then raise Analyses.Deadcode else man.local

src/analyses/memLeak.ml

@@ -228,7 +228,7 @@ struct
       warn_for_multi_threaded_due_to_abort man;
       state
     | Assert { exp; refine = true; _ } ->
-      begin match man.ask (Queries.EvalInt exp) with
+      begin match man.ask (Queries.EvalInt exp) with (* TODO: Queries.eval_bool? *)
         | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
         | a ->
           begin match Queries.ID.to_bool a with

src/analyses/unassumeAnalysis.ml

@@ -261,7 +261,7 @@ struct
       let e = List.fold_left (fun a {exp = b; _} -> Cil.(BinOp (LAnd, a, b, intType))) x.exp xs in
       M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e;
       if not !AnalysisState.postsolving then (
-        if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (man.ask (EvalInt e)) = Some false) then (
+        if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (man.ask (EvalInt e)) = Some false) then ( (* TODO: Queries.eval_bool? *)
           let tokens = x.token :: List.map (fun {token; _} -> token) xs in
           man.emit (Unassume {exp = e; tokens});
           List.iter WideningTokenLifter.add tokens
@@ -280,7 +280,7 @@ struct
   let body man fd =
     let pres = FH.find_all fun_pres fd in
     let st = List.fold_left (fun acc pre ->
-        let v = man.ask (EvalInt pre) in
+        let v = man.ask (EvalInt pre) in (* TODO: Queries.eval_bool? *)
         (* M.debug ~category:Witness "%a precondition %a evaluated to %a" CilType.Fundec.pretty fd CilType.Exp.pretty pre Queries.ID.pretty v; *)
         if Queries.ID.to_bool v = Some true then
           D.add pre acc

src/domains/queries.ml

@@ -548,6 +548,15 @@ let may_be_equal = eval_int_binop (module MayBool) Eq
 (** Backwards-compatibility for former [MayBeLess] query. *)
 let may_be_less = eval_int_binop (module MayBool) Lt
 
+let eval_bool (ask: ask) e: BoolDomain.FlatBool.t =
+  let e' = CastE (TInt (IBool, []), e) in
+  match ask.f (EvalInt e') with
+  | v when ID.is_bot v -> `Bot
+  | v ->
+    match ID.to_bool v with
+    | Some b -> `Lifted b
+    | None -> `Top
+
 
 module Set = BatSet.Make (Any)
 module Hashtbl = BatHashtbl.Make (Any)

src/transform/expressionEvaluation.ml

@@ -125,7 +125,7 @@ struct
                 value_after
 
       method private try_ask location expression =
-        match ~? (fun () -> (ask location).Queries.f (Queries.EvalInt expression)) with
+        match ~? (fun () -> (ask location).Queries.f (Queries.EvalInt expression)) with (* TODO: Queries.eval_bool? *)
         (* Inapplicable: Unreachable *)
         | Some x when Queries.ID.is_bot_ikind x -> None
         | Some x ->

src/util/library/libraryFunctions.ml

@@ -16,6 +16,11 @@ let intmax_t = lazy (
   !res
 )
 
+let stripOuterBoolCast = function
+  | CastE (TInt (IBool, _), e) -> e
+  | Const (CInt (b, IBool, s)) -> Const (CInt (b, IInt, s))
+  | e -> e
+
 (** C standard library functions.
     These are specified by the C standard. *)
 let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -830,9 +835,9 @@ let linux_kernel_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", 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" });
+    ("__goblint_check", special [__ "exp" []] @@ fun exp -> Assert { exp = stripOuterBoolCast exp; check = true; refine = false });
+    ("__goblint_assume", special [__ "exp" []] @@ fun exp -> Assert { exp = stripOuterBoolCast exp; check = false; refine = true });
+    ("__goblint_assert", special [__ "exp" []] @@ fun exp -> Assert { exp = stripOuterBoolCast exp; check = true; refine = get_bool "sem.assert.refine" });
     ("__goblint_globalize", special [__ "ptr" []] @@ fun ptr -> Globalize ptr);
     ("__goblint_split_begin", unknown [drop "exp" []]);
     ("__goblint_split_end", unknown [drop "exp" []]);

src/witness/yamlWitness.ml

@@ -454,7 +454,7 @@ struct
                   | `Lifted c_inv ->
                     (* Collect all start states that may satisfy the invariant of current_c *)
                     List.iter (fun c ->
-                        let x = R.ask_local (c.node, c.context) ~local:c.state (Queries.EvalInt c_inv) in
+                        let x = R.ask_local (c.node, c.context) ~local:c.state (Queries.EvalInt c_inv) in (* TODO: Queries.eval_bool? *)
                         if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *)
                           failwith "Bottom not expected when querying context state" (* Maybe this is reachable, failwith for now so we see when this happens *)
                         else if Queries.ID.to_bool x = Some false then () (* Nothing to do, the c does definitely not satisfy the predicate of current_c *)
@@ -747,7 +747,7 @@ struct
 
               let result: VR.result = match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with
                 | Ok inv_exp ->
-                  let x = ask_local lvar (Queries.EvalInt inv_exp) in
+                  let x = ask_local lvar (Queries.EvalInt inv_exp) in (* TODO: Queries.eval_bool? *)
                   if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *)
                     Option.get (VR.result_of_enum (VR.bot ()))
                   else (
@@ -859,7 +859,7 @@ struct
 
                 match InvariantParser.parse_cil inv_parser ~fundec ~loc pre_cabs with
                 | Ok pre_exp ->
-                  let x = ask_local pre_lvar (Queries.EvalInt pre_exp) in
+                  let x = ask_local pre_lvar (Queries.EvalInt pre_exp) in (* TODO: Queries.eval_bool? *)
                   if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *)
                     true
                   else (

tests/regression/00-sanity/39-assert-ptr.c

@@ -0,0 +1,15 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main() {
+  int* success = malloc(sizeof(int));
+  int* silence = malloc(sizeof(int));
+  int* fail = NULL;
+  int* unknown;
+  // intentionally using assert, specific order to work with assert refine
+  assert(success);
+  assert(unknown); // UNKNOWN!
+  assert(fail); // FAIL!
+  return 0;
+  assert(silence); // NOWARN!
+}

tests/regression/01-cpa/33-asserts.c

@@ -1,6 +1,6 @@
-extern void __goblint_check(int); // NOWARN
-extern void __goblint_assume(int);
-extern void __goblint_assert(int);      // NOWARN
+extern void __goblint_check(_Bool); // NOWARN
+extern void __goblint_assume(_Bool);
+extern void __goblint_assert(_Bool);      // NOWARN
 extern void __goblint_unknown(void*);
 
 #define check(x)   __goblint_check(x) // NOWARN