From 2ddc25af4d4992a1fd8af3629d4ac3d7dff17d5b Mon Sep 17 00:00:00 2001 From: Arthur Carcano Date: Wed, 21 Feb 2024 12:14:28 +0100 Subject: [PATCH] Adapt check that divisor is not zero for the symbolic case --- src/interpret.ml | 28 ++++++++++---- test/sym/div.t | 45 +++++++++++++++++++--- test/sym/div_zero.wat | 89 +++++++++++++++++++++++++++++++++++++++++++ test/sym/dune | 1 + 4 files changed, 149 insertions(+), 14 deletions(-) create mode 100644 test/sym/div_zero.wat diff --git a/src/interpret.ml b/src/interpret.ml index ec83a698d..a3b943fe1 100644 --- a/src/interpret.ml +++ b/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 diff --git a/test/sym/div.t b/test/sym/div.t index 1362a0421..c02e692f3 100644 --- a/test/sym/div.t +++ b/test/sym/div.t @@ -1,21 +1,31 @@ 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 @@ -23,7 +33,7 @@ div binop: (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 @@ -31,3 +41,26 @@ div binop: (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] diff --git a/test/sym/div_zero.wat b/test/sym/div_zero.wat new file mode 100644 index 000000000..c198bd551 --- /dev/null +++ b/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) +) diff --git a/test/sym/dune b/test/sym/dune index be53fb2a8..d5698c850 100644 --- a/test/sym/dune +++ b/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