reviews (assume_extern_module and binop sym tests)

src/cmd_sym.ml

@@ -9,20 +9,6 @@ let print_solver_time = false
 
 let print_path_condition = false
 
-let assume_extern_module : Symbolic.P.extern_func Link.extern_module =
-  let assume_positive_i32 (i : Value.int32) : unit Choice.t =
-    let c = Value.I32.ge i Value.I32.zero in
-    Choice.add_pc c
-  in
-  (* we need to describe their types *)
-  let functions =
-    [ ( "assume_positive_i32"
-      , Symbolic.P.Extern_func.Extern_func
-          (Func (Arg (I32, Res), R0), assume_positive_i32) )
-    ]
-  in
-  { functions }
-
 let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
   let sym_cnt = Atomic.make 0 in
   let mk_symbol = Encoding.Symbol.mk_symbol in
@@ -37,6 +23,10 @@ let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
     let c = Value.I32.to_bool i in
     Choice.add_pc c
   in
+  let assume_positive_i32 (i : Value.int32) : unit Choice.t =
+    let c = Value.I32.ge i Value.I32.zero in
+    Choice.add_pc c
+  in
   let assert_i32 (i : Value.int32) : unit Choice.t =
     let c = Value.I32.to_bool i in
     Choice.assertion c
@@ -61,6 +51,9 @@ let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
     ; ( "assume"
       , Symbolic.P.Extern_func.Extern_func
           (Func (Arg (I32, Res), R0), assume_i32) )
+    ; ( "assume_positive"
+      , Symbolic.P.Extern_func.Extern_func
+          (Func (Arg (I32, Res), R0), assume_positive_i32) )
     ; ( "assert"
       , Symbolic.P.Extern_func.Extern_func
           (Func (Arg (I32, Res), R0), assert_i32) )
@@ -127,10 +120,6 @@ let ( let*/ ) (t : 'a Result.t) (f : 'a -> 'b Result.t Choice.t) :
 let simplify_then_link_then_run ~unsafe ~optimize (pc : unit Result.t Choice.t)
   file =
   let link_state = Link.empty_state in
-  let link_state =
-    Link.extern_module' link_state ~name:"assume"
-      ~func_typ:Symbolic.P.Extern_func.extern_type assume_extern_module
-  in
   let link_state =
     Link.extern_module' link_state ~name:"symbolic"
       ~func_typ:Symbolic.P.Extern_func.extern_type symbolic_extern_module

test/sym/assume.t

@@ -1,3 +1,8 @@
-assume extern module:
+symbolic extern module (assume and assert test):
   $ dune exec owi -- sym assume.wast
+  CHECK:
+  (i32.not (i32.to_bool symbol_0))
+  (i32.ge symbol_0 (i32 0))
+  (i32.to_bool symbol_0)
+  /CHECK OK
   All OK

test/sym/assume.wast

@@ -1,11 +1,15 @@
 (module
   (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
-  (import "assume" "assume_positive_i32" (func $positive_i32 (param i32)))
+  (import "symbolic" "assume" (func $assume_i32 (param i32)))
+  (import "symbolic" "assume_positive" (func $positive_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
 
   (func $start
     (local $x i32)
     (local.set $x (call $i32_symbol))
+    (call $assume_i32 (local.get $x))
     (call $positive_i32 (local.get $x))
+    (call $assert_i32 (local.get $x))
     (if (i32.gt_s (i32.const 0) (local.get $x))
       (then unreachable)))
 

test/sym/binop_f32.wast

@@ -3,25 +3,20 @@
 
   (func $start
     (local $x f32)
-    (local $res f32)
 
     (local.set $x (call $f32_symbol))
 
-    (local.set $res (f32.add (local.get $x) (f32.const 42)))
-    (if (f32.eq (local.get $res) (f32.const 0))
-      (then unreachable))
+    (f32.eq (f32.add (local.get $x) (f32.const 42)) (f32.const 0))
+    (if (then unreachable))
 
-    (local.set $res (f32.sub (local.get $x) (f32.const 42)))
-    (if (f32.eq (local.get $res) (f32.const 0))
-      (then unreachable))
+    (f32.eq (f32.sub (local.get $x) (f32.const 42)) (f32.const 0))
+    (if (then unreachable))
 
-    (local.set $res (f32.mul (local.get $x) (f32.const 42)))
-    (if (f32.eq (local.get $res) (f32.const 0))
-      (then unreachable))
+    (f32.eq (f32.mul (local.get $x) (f32.const 42)) (f32.const 0))
+    (if (then unreachable))
 
-    (local.set $res (f32.div (local.get $x) (f32.const 42)))
-    (if (f32.eq (local.get $res) (f32.const 0))
-      (then unreachable)))
+    (f32.eq (f32.div (local.get $x) (f32.const 42)) (f32.const 0))
+    (if (then unreachable)))
 
   (start $start)
 )

test/sym/binop_f64.wast

@@ -3,25 +3,20 @@
 
   (func $start
     (local $x f64)
-    (local $res f64)
 
     (local.set $x (call $f64_symbol))
 
-    (local.set $res (f64.add (local.get $x) (f64.const 42)))
-    (if (f64.eq (local.get $res) (f64.const 0))
-      (then unreachable))
+    (f64.eq (f64.add (local.get $x) (f64.const 42)) (f64.const 0))
+    (if (then unreachable))
 
-    (local.set $res (f64.sub (local.get $x) (f64.const 42)))
-    (if (f64.eq (local.get $res) (f64.const 0))
-      (then unreachable))
+    (f64.eq (f64.sub (local.get $x) (f64.const 42)) (f64.const 0))
+    (if (then unreachable))
 
-    (local.set $res (f64.mul (local.get $x) (f64.const 42)))
-    (if (f64.eq (local.get $res) (f64.const 0))
-      (then unreachable))
+    (f64.eq (f64.mul (local.get $x) (f64.const 42)) (f64.const 0))
+    (if (then unreachable))
 
-    (local.set $res (f64.div (local.get $x) (f64.const 42)))
-    (if (f64.eq (local.get $res) (f64.const 0))
-      (then unreachable)))
+    (f64.eq (f64.div (local.get $x) (f64.const 42)) (f64.const 0))
+    (if (then unreachable)))
 
   (start $start)
 )

test/sym/binop_i32.wast

@@ -3,29 +3,28 @@
 
   (func $start
     (local $x i32)
-    (local $res i32)
-
+
     (local.set $x (call $i32_symbol))
 
-    (local.set $res (i32.add (local.get $x) (i32.const 42)))
-    (if (i32.eqz (local.get $res))
-      (then unreachable))
+    (i32.add (local.get $x) (i32.const 42))
+    i32.eqz
+    (if (then unreachable))
 
-    (local.set $res (i32.sub (local.get $x) (i32.const 42)))
-    (if (i32.eqz (local.get $res))
-      (then unreachable))
+    (i32.sub (local.get $x) (i32.const 42))
+    i32.eqz
+    (if (then unreachable))
 
-    (local.set $res (i32.mul (local.get $x) (i32.const 42)))
-    (if (i32.eqz (local.get $res))
-      (then unreachable))
+    (i32.mul (local.get $x) (i32.const 42))
+    i32.eqz
+    (if (then unreachable))
 
-    (local.set $res (i32.div_u (local.get $x) (i32.const 42)))
-    (if (i32.eqz (local.get $res))
-      (then unreachable))
+    (i32.div_u (local.get $x) (i32.const 42))
+    i32.eqz
+    (if (then unreachable))
 
-    (local.set $res (i32.div_s (local.get $x) (i32.const 42)))
-    (if (i32.eqz (local.get $res))
-      (then unreachable)))
+    (i32.div_s (local.get $x) (i32.const 42))
+    i32.eqz
+    (if (then unreachable)))
 
   (start $start)
 )

test/sym/binop_i64.wast

@@ -3,29 +3,28 @@
 
   (func $start
     (local $x i64)
-    (local $res i64)
 
     (local.set $x (call $i64_symbol))
 
-    (local.set $res (i64.add (local.get $x) (i64.const 42)))
-    (if (i64.eqz (local.get $res))
-      (then unreachable))
+    (i64.add (local.get $x) (i64.const 42))
+    i64.eqz
+    (if (then unreachable))
 
-    (local.set $res (i64.sub (local.get $x) (i64.const 42)))
-    (if (i64.eqz (local.get $res))
-      (then unreachable))
+    (i64.sub (local.get $x) (i64.const 42))
+    i64.eqz
+    (if (then unreachable))
 
-    (local.set $res (i64.mul (local.get $x) (i64.const 42)))
-    (if (i64.eqz (local.get $res))
-      (then unreachable))
+    (i64.mul (local.get $x) (i64.const 42))
+    i64.eqz
+    (if (then unreachable))
 
-    (local.set $res (i64.div_u (local.get $x) (i64.const 42)))
-    (if (i64.eqz (local.get $res))
-      (then unreachable))
+    (i64.div_u (local.get $x) (i64.const 42))
+    i64.eqz
+    (if (then unreachable))
 
-    (local.set $res (i64.div_s (local.get $x) (i64.const 42)))
-    (if (i64.eqz (local.get $res))
-      (then unreachable)))
+    (i64.div_s (local.get $x) (i64.const 42))
+    i64.eqz
+    (if (then unreachable)))
 
   (start $start)
 )