add bool symbol in owi.c, whose implementation is the same as i32 sym…

…bol for the time being
OCamlPro · Jun 17, 2024 · e99e9f1 · e99e9f1
1 parent 5a78349
commit e99e9f1
Show file tree

Hide file tree

Showing 6 changed files with 33 additions and 5 deletions.
diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml
@@ -69,6 +69,19 @@ 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_bitv 32) (fun sym forced_value ->
+        let n =
+          match forced_value with
+          | None -> Int32.logand 1l (Random.bits32 ())
+          | Some (Num (I32 n)) -> n
+          | _ -> assert false
+        in
+        let sym_expr =
+          Expr.make (Cvtop (Ty_bitv 32, Zero_extend 31, Expr.mk_symbol sym))
+        in
+        (I32 n, Value.pair n sym_expr) )
+
   let assume_i32 (i : Value.int32) : unit Choice.t =
     let c = Value.I32.to_bool i in
     Concolic_choice.assume c
@@ -160,6 +173,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) )

diff --git a/src/intf/wasm_ffi_intf.ml b/src/intf/wasm_ffi_intf.ml
@@ -25,6 +25,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

diff --git a/src/libc/include/owi.h b/src/libc/include/owi.h
@@ -15,6 +15,7 @@ float owi_f32(void) __attribute__((import_module("symbolic"))) __attribute__((im
 
 double owi_f64(void) __attribute__((import_module("symbolic"))) __attribute__((import_name("f64_symbol")));
 
+_Bool owi_bool(void) __attribute__((import_module("symbolic"))) __attribute__((import_name("bool_symbol")));
 
 void owi_assume(int c) __attribute__((import_module("symbolic"))) __attribute__((import_name("assume")));
 void owi_assert(int c) __attribute__((import_module("symbolic"))) __attribute__((import_name("assert")));

diff --git a/src/libc/src/owi.c b/src/libc/src/owi.c
@@ -15,6 +15,8 @@ __attribute__((import_module("symbolic"), import_name("f32_symbol"))) float
 owi_f32(void);
 __attribute__((import_module("symbolic"), import_name("f64_symbol"))) double
 owi_f64(void);
+__attribute__((import_module("symbolic"), import_name("bool_symbol"))) _Bool
+owi_bool(void);
 
 __attribute__((import_module("symbolic"), import_name("assume"))) void
 owi_assume(int);

diff --git a/src/libc/src/test-comp.c b/src/libc/src/test-comp.c
@@ -1,10 +1,12 @@
 #include <owi.h>
 
-_Bool __VERIFIER_nondet_bool(void) {
-  _Bool var = owi_i32();
-  owi_assume(or_(var == 0, var == 1));
-  return var;
-}
+// _Bool __VERIFIER_nondet_bool(void) {
+//   _Bool var = owi_i32();
+//   owi_assume(var == 0 || var == 1);
+//   return var;
+// }
+
+_Bool __VERIFIER_nondet_bool(void) { return owi_bool(); }
 
 char __VERIFIER_nondet_char(void) { return (char)owi_i32(); }
 

diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml
@@ -48,6 +48,8 @@ module M :
 
   let symbol_f64 = symbol (Ty_fp 64)
 
+  let symbol_bool = symbol (Ty_bitv 32)
+
   open Expr
 
   let abort () : unit Choice.t = Choice.add_pc @@ Value.Bool.const false
@@ -116,6 +118,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) )