Adapt check that divisor is not zero for the symbolic case

src/interpret.ml

@@ -45,6 +45,10 @@ module Make (P : Interpret_intf.P) :
 
     let ( <> ) = ne
 
+    let ( = ) = eq
+
+    let eqz v = v = zero
+
     let min_int = const_i32 Int32.min_int
   end
 
@@ -71,6 +75,10 @@ module Make (P : Interpret_intf.P) :
 
     let ( <> ) = ne
 
+    let ( = ) = eq
+
+    let eqz v = v = zero
+
     let min_int = const_i64 Int64.min_int
   end
 
@@ -150,21 +158,23 @@ module Make (P : Interpret_intf.P) :
         | Sub -> Choice.return @@ sub n1 n2
         | Mul -> Choice.return @@ mul n1 n2
         | Div s -> begin
-          try
+          let> cond = eqz n2 in
+          if cond then Choice.trap Integer_divide_by_zero
+          else
             match s with
             | S ->
               let> overflow = Bool.and_ (eq n1 min_int) @@ eq n2 ~-(const 1l) in
               if overflow then Choice.trap Integer_overflow
               else Choice.return @@ div n1 n2
             | U -> Choice.return @@ unsigned_div n1 n2
-          with Division_by_zero -> Choice.trap Integer_divide_by_zero
         end
         | Rem s -> begin
-          try
+          let> cond = eqz n2 in
+          if cond then Choice.trap Integer_divide_by_zero
+          else
             match s with
             | S -> Choice.return @@ rem n1 n2
             | U -> Choice.return @@ unsigned_rem n1 n2
-          with Division_by_zero -> Choice.trap Integer_divide_by_zero
         end
         | And -> Choice.return @@ logand n1 n2
         | Or -> Choice.return @@ logor n1 n2
@@ -185,7 +195,9 @@ module Make (P : Interpret_intf.P) :
         | Sub -> Choice.return @@ sub n1 n2
         | Mul -> Choice.return @@ mul n1 n2
         | Div s -> begin
-          try
+          let> cond = eqz n2 in
+          if cond then Choice.trap Integer_divide_by_zero
+          else
             match s with
             | S ->
               let> overflow =
@@ -195,14 +207,14 @@ module Make (P : Interpret_intf.P) :
               if overflow then Choice.trap Integer_overflow
               else Choice.return @@ div n1 n2
             | U -> Choice.return @@ unsigned_div n1 n2
-          with Division_by_zero -> Choice.trap Integer_divide_by_zero
         end
         | Rem s -> begin
-          try
+          let> cond = eqz n2 in
+          if cond then Choice.trap Integer_divide_by_zero
+          else
             match s with
             | S -> Choice.return @@ rem n1 n2
             | U -> Choice.return @@ unsigned_rem n1 n2
-          with Division_by_zero -> Choice.trap Integer_divide_by_zero
         end
         | And -> Choice.return @@ logand n1 n2
         | Or -> Choice.return @@ logor n1 n2

test/sym/div.t

@@ -1,33 +1,66 @@
 div binop:
-  $ dune exec owi -- sym div_i32.wat --no-value
+  $ dune exec owi -- sym div_i32.wat --no-value --no-stop-at-failure -w1
   Trap: integer overflow
   Model:
     (model
       (symbol_0 i32)
       (symbol_1 i32))
-  Reached problem!
+  Trap: integer divide by zero
+  Model:
+    (model
+      (symbol_0 i32)
+      (symbol_1 i32))
+  Reached 2 problems!
   [13]
-  $ dune exec owi -- sym div_i64.wat --no-value
+  $ dune exec owi -- sym div_i64.wat --no-value --no-stop-at-failure -w1
   Trap: integer overflow
   Model:
     (model
       (symbol_0 i64)
       (symbol_1 i64))
-  Reached problem!
+  Trap: integer divide by zero
+  Model:
+    (model
+      (symbol_0 i64)
+      (symbol_1 i64))
+  Reached 2 problems!
   [13]
-  $ dune exec owi -- sym div_f32.wat --no-value
+  $ dune exec owi -- sym div_f32.wat --no-value --no-stop-at-failure -w1
   Assert failure: (f32.eq (f32.div symbol_0 symbol_1) (f32.div symbol_0 symbol_1))
   Model:
     (model
       (symbol_0 f32)
       (symbol_1 f32))
   Reached problem!
   [13]
-  $ dune exec owi -- sym div_f64.wat --no-value
+  $ dune exec owi -- sym div_f64.wat --no-value --no-stop-at-failure -w1
   Assert failure: (f64.eq (f64.div symbol_0 symbol_1) (f64.div symbol_0 symbol_1))
   Model:
     (model
       (symbol_0 f64)
       (symbol_1 f64))
   Reached problem!
   [13]
+  $ dune exec owi -- sym div_zero.wat --no-stop-at-failure -w1
+  Trap: integer divide by zero
+  Model:
+    (model
+      (symbol_0 (i32 3))
+      (symbol_6 (i64 0)))
+  Trap: integer divide by zero
+  Model:
+    (model
+      (symbol_0 (i32 2))
+      (symbol_3 (i64 0)))
+  Trap: integer divide by zero
+  Model:
+    (model
+      (symbol_0 (i32 1))
+      (symbol_2 (i32 0)))
+  Trap: integer divide by zero
+  Model:
+    (model
+      (symbol_0 (i32 0))
+      (symbol_1 (i32 0)))
+  Reached 4 problems!
+  [13]

test/sym/div_zero.wat

@@ -0,0 +1,89 @@
+;; Checks that all integer divisions by zero trap
+;; but not floating point ones
+;; Regression-test for https://github.com/OCamlPro/owi/issues/128
+(module
+  (type $void_t (func))
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+  (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
+  (import "symbolic" "f64_symbol" (func $f64_symbol (result f64)))
+  (import "symbolic" "assume" (func $assume (param i32)))
+
+  (table $func_table 6 6 funcref)
+
+  (elem (i32.const 0) $i32_block)
+  (elem (i32.const 1) $i32_block_u)
+  (elem (i32.const 2) $i64_block)
+  (elem (i32.const 3) $i64_block_u)
+  (elem (i32.const 4) $f32_block)
+  (elem (i32.const 5) $f64_block)
+
+  (func $start
+
+    (local $n i32)
+
+    (local.set $n (call $i32_symbol))
+
+    (call $assume 
+      (i32.and
+        (i32.ge_u (local.get $n) (i32.const 0))
+        (i32.lt_u (local.get $n) (i32.const 6))
+        )
+    )
+
+    (local.get $n)
+
+    call_indirect  (type $void_t) 
+  )
+
+  (func $i32_block (type $void_t)
+    i32.const 1
+    (call $i32_symbol)
+    i32.div_s
+    drop
+    return
+  )
+
+   (func $i32_block_u (type $void_t)
+    i32.const 1
+    (call $i32_symbol)
+    i32.div_u
+    drop
+    return
+  )
+
+  (func $i64_block (type $void_t)
+    i64.const 1
+    (call $i64_symbol)
+    i64.div_s
+    drop
+    return
+  )
+
+    (func $i64_block_u (type $void_t)
+    i64.const 1
+    (call $i64_symbol)
+    i64.div_u
+    drop
+    return
+  )
+
+
+  (func $f32_block (type $void_t)
+    f32.const 1
+    (call $f32_symbol)
+    f32.div
+    drop
+    return
+  )
+
+  (func $f64_block (type $void_t)
+    f64.const 1
+    (call $f64_symbol)
+    f64.div
+    drop
+    return
+  )
+
+  (start $start)
+)

test/sym/dune

@@ -16,6 +16,7 @@
   div_i64.wat
   div_f32.wat
   div_f64.wat
+  div_zero.wat
   global.wat
   grow.wat
   memory.wat