add a owi_bool function

CHANGES.md

@@ -1,7 +1,7 @@
 ## unreleased
 
 - parameterize the `Thread` module on the symbolic memory and the `Choice_monad` module on a Thread
-- adds a `owi_char` function to create char symbolic value
+- add `owi_char` and `owi_bool` function to create char and bool symbolic values
 - adds a `Mem` argument to external function to allow direct manipulation of the memory.
 - support other solvers through the `--solver` option (Z3, Colibri2, Bitwuzla and CVC5)
 - support the extended constant expressions proposal

src/concolic/concolic_wasm_ffi.ml

@@ -41,18 +41,7 @@ module M :
         in
         (I32 n, Value.pair n sym_expr) )
 
-  let symbol_char () : Value.int32 Choice.t =
-    Choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value ->
-        let n =
-          match forced_value with
-          | None -> Int32.logand 0xFFl (Random.bits32 ())
-          | Some (Num (I32 n)) -> n
-          | _ -> assert false
-        in
-        let sym_expr =
-          Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.mk_symbol sym))
-        in
-        (I32 n, Value.pair n sym_expr) )
+  let symbol_char = symbol_i8
 
   let symbol_i64 () : Value.int64 Choice.t =
     Choice.with_new_symbol (Ty_bitv 64) (fun sym forced_value ->
@@ -86,6 +75,18 @@ module M :
         let n = Float64.of_bits n in
         (F64 n, Value.pair n (Expr.mk_symbol sym)) )
 
+  let symbol_bool () : Value.int32 Choice.t =
+    Choice.with_new_symbol Ty_bool (fun sym forced_value ->
+        let b =
+          match forced_value with
+          | None -> Random.bool ()
+          | Some True -> true
+          | Some False -> false
+          | _ -> assert false
+        in
+        let n = V.Bool.int32 b in
+        (I32 n, Value.(Bool.int32 (pair b (Expr.mk_symbol sym)))) )
+
   let assume_i32 (i : Value.int32) : unit Choice.t =
     let c = Value.I32.to_bool i in
     Concolic_choice.assume c
@@ -157,6 +158,9 @@ let symbolic_extern_module =
     ; ( "f64_symbol"
       , Concolic.P.Extern_func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
       )
+    ; ( "bool_symbol"
+      , Concolic.P.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_bool)
+      )
     ; ( "assume"
       , Concolic.P.Extern_func.Extern_func
           (Func (Arg (I32, Res), R0), assume_i32) )

src/intf/wasm_ffi_intf.ml

@@ -29,6 +29,8 @@ module type S0 = sig
 
   val symbol_f64 : unit -> Value.float64 t
 
+  val symbol_bool : unit -> Value.int32 t
+
   val assume_i32 : Value.int32 -> unit t
 
   val assume_positive_i32 : Value.int32 -> unit t

src/libc/src/test-comp.c

@@ -1,17 +1,7 @@
 #include <owi.h>
 
-static __attribute__((naked,noinline,optnone)) _Bool or_(_Bool a, _Bool b) {
-  __asm__ __volatile__("local.get 0;"
-                       "local.get 1;"
-                       "i32.or;"
-                       "return;");
-}
-
 _Bool __VERIFIER_nondet_bool(void) {
-  const _Bool var = owi_i32();
-  const _Bool pc = or_(var == 0, var == 1);
-  owi_assume(pc);
-  return var;
+  return owi_bool();
 }
 
 char __VERIFIER_nondet_char(void) { return (char)owi_i32(); }

src/symbolic/symbolic_value.ml

@@ -200,6 +200,7 @@ module I32 = struct
   let to_bool (e : vbool) =
     match view e with
     | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l
+    | Symbol { ty = Ty_bool; _ } -> e
     | Cvtop (_, OfBool, cond) -> cond
     | _ -> make (Cvtop (ty, ToBool, e))
 

src/symbolic/symbolic_wasm_ffi.ml

@@ -27,13 +27,15 @@ module M :
   let assert_i32 (i : Value.int32) : unit Choice.t =
     Choice.assertion @@ Value.I32.to_bool i
 
+  let symbol_bool () =
+    Choice.with_new_symbol (Ty_bitv 1) (fun sym ->
+        Expr.cvtop (Ty_bitv 32) (Smtml.Ty.Zero_extend 31) (Expr.symbol sym) )
+
   let symbol_i8 () =
     Choice.with_new_symbol (Ty_bitv 8) (fun sym ->
         Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) )
 
-  let symbol_char () =
-    Choice.with_new_symbol (Ty_bitv 8) (fun sym ->
-        Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) )
+  let symbol_char = symbol_i8
 
   let symbol_i32 () = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol
 
@@ -78,6 +80,9 @@ let symbolic_extern_module =
     ; ( "f64_symbol"
       , Symbolic.P.Extern_func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
       )
+    ; ( "bool_symbol"
+      , Symbolic.P.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_bool)
+      )
     ; ( "assume"
       , Symbolic.P.Extern_func.Extern_func
           (Func (Arg (I32, Res), R0), assume_i32) )

test/c/bool.c

@@ -0,0 +1,9 @@
+#include <owi.h>
+
+int main() {
+    _Bool b1 = owi_bool(), b2 = owi_bool();
+    owi_assume(b1 || b2);
+    owi_assume(b1 || !b2);
+    owi_assert(b1);
+    return 0;
+}

test/c/bool.t

@@ -0,0 +1,2 @@
+  $ owi c ./bool.c
+  All OK

test/c/dune

@@ -2,7 +2,8 @@
  (deps
   %{bin:owi}
   (package owi)
-  malloc_aligned.c
-  main.c
+  bool.c
+  char.c
   exit.c
-  char.c))
+  main.c
+  malloc_aligned.c))