Merge pull request #1684 from goblint/assert-ptr

Replace `int` -> `_Bool` in goblint stubs arguments

Author: sim642

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,9 +30,10 @@ struct
     if man.local then
       match f.sformals with
       | [arg] when isIntegralType arg.vtype ->
-        (match man.ask (EvalInt (Lval (Var arg, NoOffset))) with
-         | v when Queries.ID.is_bot v -> false
-         | v -> BatOption.default false (Queries.ID.to_bool v))
+        (match Queries.eval_bool (Analyses.ask_of_man man) (Lval (Var arg, NoOffset)) with
+         | `Bot -> false
+         | `Lifted b -> b
+         | `Top -> false)
       | _ ->
         (* should not happen, man.local should always be false in this case *)
         false

src/analyses/assert.ml

@@ -14,12 +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 -> Option.map_default (fun b -> `Lifted b) `Top (Queries.ID.to_bool v)
-    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). *)
@@ -38,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,19 +228,16 @@ struct
       warn_for_multi_threaded_due_to_abort man;
       state
     | Assert { exp; refine = true; _ } ->
-      begin match man.ask (Queries.EvalInt exp) with
-        | 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
-            | Some true -> ()
-            | Some false ->
-              (* If we know for sure that the expression in "assert" is false => need to check for memory leaks *)
-              warn_for_multi_threaded_due_to_abort man;
-              check_for_mem_leak man
-            | None ->
-              warn_for_multi_threaded_due_to_abort man;
-              check_for_mem_leak man ~assert_exp_imprecise:true ~exp:(Some exp)
-          end
+      begin match Queries.eval_bool (Analyses.ask_of_man man) exp with
+        | `Bot -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
+        | `Lifted true -> ()
+        | `Lifted false ->
+          (* If we know for sure that the expression in "assert" is false => need to check for memory leaks *)
+          warn_for_multi_threaded_due_to_abort man;
+          check_for_mem_leak man
+        | `Top ->
+          warn_for_multi_threaded_due_to_abort man;
+          check_for_mem_leak man ~assert_exp_imprecise:true ~exp:(Some exp)
       end;
       state
     | ThreadExit _ ->

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.eval_bool (Analyses.ask_of_man man) e = `Lifted false) then (
           let tokens = x.token :: List.map (fun {token; _} -> token) xs in
           man.emit (Unassume {exp = e; tokens});
           List.iter WideningTokenLifter.add tokens
@@ -280,9 +280,8 @@ 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
         (* 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
+        if Queries.eval_bool (Analyses.ask_of_man man) pre = `Lifted true then
           D.add pre acc
         else
           acc

src/domains/queries.ml

@@ -561,6 +561,12 @@ 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 || ID.is_bot_ikind v -> `Bot
+  | v -> BatOption.map_default (fun b -> `Lifted b) `Top (ID.to_bool v)
+
 
 module Set = BatSet.Make (Any)
 module Hashtbl = BatHashtbl.Make (Any)

src/transform/expressionEvaluation.ml

@@ -125,16 +125,10 @@ struct
                 value_after
 
       method private try_ask location expression =
-        match ~? (fun () -> (ask location).Queries.f (Queries.EvalInt expression)) with
-        (* Inapplicable: Unreachable *)
-        | Some x when Queries.ID.is_bot_ikind x -> None
-        | Some x ->
-          begin match Queries.ID.to_int x with
-            (* Evaluable: Definite *)
-            | Some i -> Some (Some (not (Z.equal i Z.zero)))
-            (* Evaluable: Inconclusive *)
-            | None -> Some None
-          end
+        match ~? (fun () -> Queries.eval_bool (ask location) expression) with
+        | Some `Bot -> None (* Inapplicable: Unreachable *)
+        | Some (`Lifted b) -> Some (Some b) (* Evaluable: Definite *)
+        | Some `Top -> Some None (* Evaluable: Inconclusive *)
         (* Inapplicable: Unlisted *)
         | None
         | exception Not_found -> None

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.[
@@ -833,9 +838,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" []]);