Simplify file #310

Laplace-Demon · 2024-06-14T11:33:17Z

No description provided.

zapashcanon · 2024-06-14T12:09:01Z

src/libc/src/test-comp.c

@@ -2,7 +2,7 @@

 _Bool __VERIFIER_nondet_bool(void) {
  _Bool var = owi_i32();
-  owi_assume(or_(var == 0, var == 1));
+  owi_assume(var == 0 || var == 1);


@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 ?

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.

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

src/concolic/concolic_wasm_ffi.ml

src/symbolic/symbolic_wasm_ffi.ml

src/concolic/concolic_wasm_ffi.ml

src/libc/src/owi.c

zapashcanon · 2024-06-24T11:17:19Z

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

Laplace-Demon · 2024-06-25T08:56:16Z

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

dw, it's fixed

zapashcanon · 2024-07-16T12:24:03Z

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

zapashcanon · 2024-07-16T15:35:51Z

src/symbolic/symbolic_wasm_ffi.ml

+  let symbol_bool () =
+    let open Choice in
+    let+ sym = symbol Ty_bool () in
+    Expr.make (Cvtop (Ty_bool, Smtml.Ty.OfBool, sym))


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 · 2024-07-16T15:38:03Z

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 · 2024-07-16T19:58:19Z

@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 ? 😅

…bol for the time being

filipeom · 2024-07-16T20:35:59Z

@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 · 2024-07-16T20:39:55Z

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 · 2024-07-16T20:40:58Z

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

filipeom · 2024-07-16T20:41:57Z

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 · 2024-07-18T12:39:02Z

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 · 2024-07-19T09:07:30Z

@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 · 2024-07-22T09:22:28Z

src/libc/src/owi.c

+                       "i32.ne;"
+                       "i32.and;"
+                       "return;");
+}


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 · 2024-07-23T08:32:57Z

Thanks!

zapashcanon reviewed Jun 14, 2024

View reviewed changes

Laplace-Demon force-pushed the simplify-file branch from 1b36ab7 to e99e9f1 Compare June 17, 2024 10:23

zapashcanon reviewed Jun 17, 2024

View reviewed changes

src/concolic/concolic_wasm_ffi.ml Outdated Show resolved Hide resolved

zapashcanon reviewed Jun 17, 2024

View reviewed changes

src/symbolic/symbolic_wasm_ffi.ml Outdated Show resolved Hide resolved

filipeom reviewed Jun 17, 2024

View reviewed changes

src/concolic/concolic_wasm_ffi.ml Outdated Show resolved Hide resolved

zapashcanon reviewed Jun 18, 2024

View reviewed changes

src/libc/src/owi.c Outdated Show resolved Hide resolved

zapashcanon added the no changelog label Jul 3, 2024

zapashcanon reviewed Jul 16, 2024

View reviewed changes

Laplace-Demon added 8 commits July 16, 2024 22:18

delete wrapper functions in owi.c

3b98437

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

d7776f7

…bol for the time being

delete __VERIFIER_nondet_bool comment

21865ce

change for the definition of symbol_bool

1cc199b

format

aaf9e96

modify concolic symbol_bool

dc79a35

remove attributes in header file and add final newline

aba61ef

fix owi header

011692f

Laplace-Demon force-pushed the simplify-file branch from 0a8a28a to 011692f Compare July 16, 2024 20:18

revert bool related changes

09c91a1

zapashcanon reviewed Jul 22, 2024

View reviewed changes

inline _or in test-comp.c

c620abd

zapashcanon mentioned this pull request Jul 23, 2024

add a owi_bool function #374

Open

zapashcanon merged commit da85f7b into OCamlPro:main Jul 23, 2024
3 checks passed

Laplace-Demon deleted the simplify-file branch July 23, 2024 10:48

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Simplify file #310

Simplify file #310

Laplace-Demon commented Jun 14, 2024

zapashcanon Jun 14, 2024

filipeom Jun 14, 2024 •

edited

Loading

zapashcanon Jun 16, 2024

zapashcanon commented Jun 24, 2024

Laplace-Demon commented Jun 25, 2024

zapashcanon commented Jul 16, 2024

zapashcanon Jul 16, 2024 •

edited

Loading

zapashcanon commented Jul 16, 2024 •

edited

Loading

zapashcanon commented Jul 16, 2024

filipeom commented Jul 16, 2024

zapashcanon commented Jul 16, 2024

zapashcanon commented Jul 16, 2024

filipeom commented Jul 16, 2024

filipeom commented Jul 18, 2024 •

edited

Loading

Laplace-Demon commented Jul 19, 2024

zapashcanon Jul 22, 2024 •

edited

Loading

zapashcanon commented Jul 23, 2024

Simplify file #310

Simplify file #310

Conversation

Laplace-Demon commented Jun 14, 2024

zapashcanon Jun 14, 2024

Choose a reason for hiding this comment

filipeom Jun 14, 2024 • edited Loading

Choose a reason for hiding this comment

zapashcanon Jun 16, 2024

Choose a reason for hiding this comment

zapashcanon commented Jun 24, 2024

Laplace-Demon commented Jun 25, 2024

zapashcanon commented Jul 16, 2024

zapashcanon Jul 16, 2024 • edited Loading

Choose a reason for hiding this comment

zapashcanon commented Jul 16, 2024 • edited Loading

zapashcanon commented Jul 16, 2024

filipeom commented Jul 16, 2024

zapashcanon commented Jul 16, 2024

zapashcanon commented Jul 16, 2024

filipeom commented Jul 16, 2024

filipeom commented Jul 18, 2024 • edited Loading

Laplace-Demon commented Jul 19, 2024

zapashcanon Jul 22, 2024 • edited Loading

Choose a reason for hiding this comment

zapashcanon commented Jul 23, 2024

filipeom Jun 14, 2024 •

edited

Loading

zapashcanon Jul 16, 2024 •

edited

Loading

zapashcanon commented Jul 16, 2024 •

edited

Loading

filipeom commented Jul 18, 2024 •

edited

Loading

zapashcanon Jul 22, 2024 •

edited

Loading