specific tests on add sub mul div operators

test/sym/add.t

@@ -0,0 +1,15 @@
+add binop:
+  $ dune exec owi -- sym add_i32.wat
+  Assert failure: (i32.le (i32 0) (i32.add symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (i32 1073741825))
+      (symbol_1 (i32 1073741824)))
+  Reached problem!
+  $ dune exec owi -- sym add_i64.wat
+  Assert failure: (i64.le (i64 0) (i64.add symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (i64 4611686018427387905))
+      (symbol_1 (i64 4611686018427387904)))
+  Reached problem!

test/sym/add_i32.wat

@@ -0,0 +1,20 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "assume_positive_i32" (func $assume_positive_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i32)
+    (local $y i32)
+
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i32_symbol))
+
+    (call $assume_positive_i32 (local.get $x))  ;; x >= 0
+    (call $assume_positive_i32 (local.get $y))  ;; y >= 0
+    (call $assert_i32                           ;; x + y >= 0 (== 0 =< x + y)
+      (i32.le_s (i32.const 0) (i32.add (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)

test/sym/add_i64.wat

@@ -0,0 +1,22 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+  (import "symbolic" "assume" (func $assume_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i64)
+    (local $y i64)
+
+    (local.set $x (call $i64_symbol))
+    (local.set $y (call $i64_symbol))
+
+    (call $assume_i32
+      (i64.ge_s (local.get $x) (i64.const 0)))    ;; x >= 0
+    (call $assume_i32
+      (i64.ge_s (local.get $y) (i64.const 0)))    ;; y >= 0
+    (call $assert_i32                             ;; x + y >= 0 (== 0 =< x + y)
+      (i64.le_s (i64.const 0) (i64.add (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)

test/sym/div.t

@@ -0,0 +1,15 @@
+div binop:
+  $ dune exec owi -- sym div_i32.wat
+  Trap: integer overflow
+  Model:
+    (model
+      (symbol_0 (i32 -2147483648))
+      (symbol_1 (i32 -1)))
+  Reached problem!
+  $ dune exec owi -- sym div_i64.wat
+  Trap: integer overflow
+  Model:
+    (model
+      (symbol_0 (i64 -9223372036854775808))
+      (symbol_1 (i64 -1)))
+  Reached problem!

test/sym/div_i32.wat

@@ -0,0 +1,19 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+
+  (func $start
+
+    (local $x i32)
+    (local $y i32)
+
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i32_symbol))
+
+    local.get $x
+    local.get $y
+    i32.div_s     ;; MIN_INT/(-1) != MAX_INT -- MAX_INT = (-MIN_INT)-1
+    drop
+  )
+
+  (start $start)
+)

test/sym/div_i64.wat

@@ -0,0 +1,19 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+
+  (func $start
+
+    (local $x i64)
+    (local $y i64)
+
+    (local.set $x (call $i64_symbol))
+    (local.set $y (call $i64_symbol))
+
+    local.get $x
+    local.get $y
+    i64.div_s     ;; MIN_INT/(-1) != MAX_INT -- MAX_INT = (-MIN_INT)-1
+    drop
+  )
+
+  (start $start)
+)

test/sym/dune

@@ -1,19 +1,28 @@
 (cram
  (deps
   %{bin:owi}
-  mini_test.wat
+  add_i32.wat
+  add_i64.wat
   assume.wat
-  binop_i32.wat
-  binop_i32-2.wat
-  binop_i64.wat
-  binop_i64-2.wat
-  binop_f32.wat
-  binop_f64.wat
-  global.wat
-  grow.wat
-  memory.wat
+  ; binop_i32.wat
+  ; binop_i32-2.wat
+  ; binop_i64.wat
+  ; binop_i64-2.wat
+  ; binop_f32.wat
+  ; binop_f64.wat
+  div_i32.wat
+  div_i64.wat
+  ; global.wat
+  ; grow.wat
+  ; memory.wat
+  mini_test.wat
+  mul_i32.wat
+  mul_i64.wat
+  sub_i32.wat
+  sub_i64.wat
   table.wat
-  unop_i32.wat
-  unop_i64.wat
-  unop_f32.wat
-  unop_f64.wat))
+  ; unop_i32.wat
+  ; unop_i64.wat
+  ; unop_f32.wat
+  ; unop_f64.wat
+ ))

test/sym/mul.t

@@ -0,0 +1,15 @@
+mul binop:
+  $ dune exec owi -- sym mul_i32.wat
+  Assert failure: (i32.ge (i32.mul symbol_0 symbol_1) (i32 0))
+  Model:
+    (model
+      (symbol_0 (i32 792711941))
+      (symbol_1 (i32 229807418)))
+  Reached problem!
+  $ dune exec owi -- sym mul_i64.wat
+  Assert failure: (i64.ge (i64.mul symbol_0 symbol_1) (i64 0))
+  Model:
+    (model
+      (symbol_0 (i64 3276315702285119495))
+      (symbol_1 (i64 4152879772057883690)))
+  Reached problem!

test/sym/mul_i32.wat

@@ -0,0 +1,20 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "assume_positive_i32" (func $assume_positive_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i32)
+    (local $y i32)
+
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i32_symbol))
+
+    (call $assume_positive_i32 (local.get $x))  ;; x >= 0
+    (call $assume_positive_i32 (local.get $y))  ;; y >= 0
+    (call $assert_i32                           ;; x * y >= 0
+      (i32.ge_s (i32.mul (local.get $x) (local.get $y)) (i32.const 0)))
+  )
+
+  (start $start)
+)

test/sym/mul_i64.wat

@@ -0,0 +1,22 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+  (import "symbolic" "assume" (func $assume_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i64)
+    (local $y i64)
+
+    (local.set $x (call $i64_symbol))
+    (local.set $y (call $i64_symbol))
+
+    (call $assume_i32
+      (i64.ge_s (local.get $x) (i64.const 0)))  ;; y >= 0
+    (call $assume_i32
+      (i64.ge_s (local.get $y) (i64.const 0)))  ;; y >= 0
+    (call $assert_i32                           ;; x * y >= 0
+      (i64.ge_s (i64.mul (local.get $x) (local.get $y)) (i64.const 0)))
+  )
+
+  (start $start)
+)

test/sym/sub.t

@@ -0,0 +1,15 @@
+sub binop:
+  $ dune exec owi -- sym sub_i32.wat
+  Assert failure: (i32.ge symbol_0 (i32.sub symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (i32 -2147483648))
+      (symbol_1 (i32 2147483645)))
+  Reached problem!
+  $ dune exec owi -- sym sub_i64.wat
+  Assert failure: (i64.ge symbol_0 (i64.sub symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (i64 -9223372036854775808))
+      (symbol_1 (i64 9223372036854775805)))
+  Reached problem!

test/sym/sub_i32.wat

@@ -0,0 +1,19 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "assume_positive_i32" (func $assume_positive_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i32)
+    (local $y i32)
+
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i32_symbol))
+
+    (call $assume_positive_i32 (local.get $y))  ;; y >= 0
+    (call $assert_i32                           ;; x >= x - y
+      (i32.ge_s (local.get $x) (i32.sub (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)

test/sym/sub_i64.wat

@@ -0,0 +1,20 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+  (import "symbolic" "assume" (func $assume_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i64)
+    (local $y i64)
+
+    (local.set $x (call $i64_symbol))
+    (local.set $y (call $i64_symbol))
+
+    (call $assume_i32
+      (i64.ge_s (local.get $y) (i64.const 0)))  ;; y >= 0
+    (call $assert_i32                           ;; x >= x - y
+      (i64.ge_s (local.get $x) (i64.sub (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)