add owi_char

CHANGES.md

@@ -1,5 +1,6 @@
 ## unreleased
 
+- adds a `owi_char` function to create char symbolic value
 - 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,6 +41,19 @@ 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_i64 () : Value.int64 Choice.t =
     Choice.with_new_symbol (Ty_bitv 64) (fun sym forced_value ->
         let n =

src/intf/wasm_ffi_intf.ml

@@ -19,6 +19,8 @@ module type S0 = sig
 
   val symbol_i8 : unit -> Value.int32 t
 
+  val symbol_char : unit -> Value.int32 t
+
   val symbol_i32 : unit -> Value.int32 t
 
   val symbol_i64 : unit -> Value.int64 t

src/libc/include/owi.h

@@ -8,6 +8,8 @@ owi_free(void *);
 
 __attribute__((import_module("symbolic"), import_name("i8_symbol"))) char
 owi_i8(void);
+__attribute__((import_module("symbolic"), import_name("char_symbol"))) char
+owi_char(void);
 __attribute__((import_module("symbolic"), import_name("i32_symbol"))) int
 owi_i32(void);
 __attribute__((import_module("symbolic"), import_name("i64_symbol"))) long long

src/symbolic/symbolic_wasm_ffi.ml

@@ -31,6 +31,10 @@ module M :
     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_i32 () = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol
 
   let symbol_i64 () = Choice.with_new_symbol (Ty_bitv 64) Expr.symbol
@@ -80,6 +84,9 @@ let symbolic_extern_module =
     [ ( "i8_symbol"
       , Symbolic.P.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_i8)
       )
+    ; ( "char_symbol"
+      , Symbolic.P.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_char)
+      )
     ; ( "i32_symbol"
       , Symbolic.P.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_i32)
       )

test/c/char.c

@@ -0,0 +1,8 @@
+#include <owi.h>
+
+int main(void) {
+    char c = owi_char();
+    owi_assume(c == 'B');
+    owi_assert('b' - c == 32);
+    return 0;
+}

test/c/char.t

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

test/c/dune

@@ -4,4 +4,5 @@
   (package owi)
   malloc_aligned.c
   main.c
-  exit.c))
+  exit.c
+  char.c))