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

…bol for the time being
OCamlPro · Jun 17, 2024 · 1b36ab7 · 1b36ab7
1 parent 895006b
commit 1b36ab7
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 5 deletions.
diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml
@@ -49,6 +49,9 @@ let symbolic_extern_module :
     ; ( "f64_symbol"
       , Symbolic.P.Extern_func.Extern_func
           (Func (UArg Res, R1 F64), symbol (Ty_fp 64)) )
+    ; ( "bool_symbol"
+      , Symbolic.P.Extern_func.Extern_func
+          (Func (UArg Res, R1 I32), symbol (Ty_bitv 32)) )
     ; ( "assume"
       , Symbolic.P.Extern_func.Extern_func
           (Func (Arg (I32, Res), R0), assume_i32) )

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(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(); }