Simplify file

[Laplace-Demon]

No description provided.

[zapashcanon]

@filipeom, I thought we were not using or_ and and_ anymore but actually we are using it there, do you think this is going to have a negative impact in some way to change it like this ? Maybe, we could also expose a owi_bool() function instead, what do you think ?

[filipeom]

It will depend on how the compiler decides to compile this. But most likely it will try to lazy evaluate the condition, possibly causing unnecessary branches. Creating a owi_bool is cleaner. But, using a bitwise-or or chaining two owi_assume would most-likely also work to reduce branching.

[zapashcanon]

@Laplace-Demon, do you want to try to add a owi_bool function ?

[zapashcanon]

@Laplace-Demon oops, I meant, removed from the .c file but kept in the header, sorry !

[Laplace-Demon]

@Laplace-Demon oops, I meant, removed from the .c file but kept in the header, sorry !

dw, it's fixed

[zapashcanon]

@Laplace-Demon, could you rebase this one so I can re-run the CI now that is has been fixed ?

[zapashcanon]

You'll need the following patch after rebasing to get the code to compile:

diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml
index 3f4ed0b2..4ad1ba33 100644
--- a/src/symbolic/symbolic_wasm_ffi.ml
+++ b/src/symbolic/symbolic_wasm_ffi.ml
@@ -40,9 +40,7 @@ module M :
   let symbol_f64 () = Choice.with_new_symbol (Ty_fp 64) Expr.symbol
 
   let symbol_bool () =
-    let open Choice in
-    let+ sym = symbol Ty_bool () in
-    Expr.make (Cvtop (Ty_bool, Smtml.Ty.OfBool, sym))
+    Choice.with_new_symbol Ty_bool Expr.symbol
 
   open Expr

[zapashcanon]

I started a benchmark to check if the boolean stuff makes any difference, it's in results-testcomp-owi_w24_O3_sZ3-2024-07-16_15h37m05s/

Results:

Run 1216/1216: testcomp/sv-benchmarks/c/xcsp/aim-200-6-0-sat-4.c
  Timeout in 30.0612 260.387 260.013
  Nothing:     75    Reached:    560    Timeout:    469    Other:    112    Killed:      0

I'll investigate the Others.

[zapashcanon]

@filipeom, I'm getting a lot of:

owi: internal error, uncaught exception:
     Z3.Error("Sorts Bool and (_ BitVec 32) are incompatible")

Is my suggested patch incorrect ? 😅

[filipeom]

@filipeom, I'm getting a lot of:

owi: internal error, uncaught exception:
     Z3.Error("Sorts Bool and (_ BitVec 32) are incompatible")

Is my suggested patch incorrect ? 😅

It's most likely because of to_bool:

owi/src/symbolic/symbolic_value.ml

Lines 192 to 196 in 10b939f

	let to_bool (e : vbool) =
	match view e with
	| Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l
	| Cvtop (_, OfBool, cond) -> cond
	| _ -> make (Cvtop (ty, ToBool, e))

ToBool is assuming its being passed something of type I32. I can suggest a workaround:

diff --git a/src/symbolic/symbolic_value.ml b/src/symbolic/symbolic_value.ml
index d32f69fd..ed50be17 100644
--- a/src/symbolic/symbolic_value.ml
+++ b/src/symbolic/symbolic_value.ml
@@ -192,6 +192,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))

But, I'm not sure this is enough. I need to play around with this and most likely fix it directly in `smtml.

[zapashcanon]

OK, I'll wait then. If you want to find a reproduction case, you can look on the server with the results mentioned earlier. Then look at which tests are causing Other and open the output of one of them to check it has the same error message.

[zapashcanon]

@Laplace-Demon, actually, maybe we could do a first PR without the bool related changes and make a second one later, WDYT?

[filipeom]

OK, I'll wait then. If you want to find a reproduction case, you can look on the server with the results mentioned earlier. Then look at which tests are causing Other and open the output of one of them to check it has the same error message.

Yes, I'm checking it out 😄

[filipeom]

Ok so instead of this #310 (comment)

We should use the following patch instead:

diff --git a/src/cmd/cmd_utils.ml b/src/cmd/cmd_utils.ml
index be7ac19d..e9fb3d1d 100644
--- a/src/cmd/cmd_utils.ml
+++ b/src/cmd/cmd_utils.ml
@@ -8,7 +8,7 @@ let out_testcase ~dst testcase =
   let o = Xmlm.make_output ~nl:true ~indent:(Some 2) dst in
   let tag atts name = (("", name), atts) in
   let atts = [ (("", "coversError"), "true") ] in
-  let to_string v = Format.asprintf "%a" Smtml.Value.pp_num v in
+  let to_string v = Format.asprintf "%a" Smtml.Value.pp v in
   let input v = `El (tag [] "input", [ `Data (to_string v) ]) in
   let testcase = `El (tag atts "testcase", List.map input testcase) in
   let dtd =
diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml
index 3f4ed0b2..8eaee478 100644
--- a/src/symbolic/symbolic_wasm_ffi.ml
+++ b/src/symbolic/symbolic_wasm_ffi.ml
@@ -40,9 +40,8 @@ module M :
   let symbol_f64 () = Choice.with_new_symbol (Ty_fp 64) Expr.symbol
 
   let symbol_bool () =
-    let open Choice in
-    let+ sym = symbol Ty_bool () in
-    Expr.make (Cvtop (Ty_bool, Smtml.Ty.OfBool, sym))
+    Choice.with_new_symbol (Ty_bitv 1) (fun sym ->
+        Expr.cvtop (Ty_bitv 32) (Smtml.Ty.Zero_extend 31) (Expr.symbol sym) )
 
   open Expr

And the latest version of formalsec/smtml#179.

But we should probably do this in another PR instead

[Laplace-Demon]

@Laplace-Demon, actually, maybe we could do a first PR without the bool related changes and make a second one later, WDYT?

Yes you have raison :)

[zapashcanon]

I think you can still remove and_ and only keep or_. :)

EDIT: you could actually remove both and inline the definition of or_ inside the definition of _Bool __VERIFIER_nondet_bool(void)

[zapashcanon]

Thanks!