Skip to content

Commit

Permalink
Re-enable test store.wat
Browse files Browse the repository at this point in the history
Test was to slow because once the out of bounds cases have been ruled
out, all "in bounds" cases still have to concretize a value for the symbol
and perform the store, leading to approx. <page_size> calls to Z3.

By reducing the possible values of idx, we ensure that the test runs fast.
  • Loading branch information
krtab authored and zapashcanon committed Feb 20, 2024
1 parent 5923419 commit c535389
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 12 deletions.
16 changes: 7 additions & 9 deletions test/sym/memory.t
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,12 @@ memory stuff:
(symbol_0 (i32 1)))
Reached problem!
[13]
# Deactivated because it is currently an enumeration of all i32s with the forced concretization
# $ dune exec owi -- sym store.wat
# Trap: out of bounds memory access
# Model:
# (model
# (symbol_0 (i32 -11))
# (symbol_1 (i32 0)))
# Reached problem!
# [1]
$ dune exec owi -- sym store.wat
Trap: out of bounds memory access
Model:
(model
(symbol_0 (i32 2146549760)))
Reached problem!
[13]
$ dune exec owi -- sym memory2.wat
All OK
13 changes: 10 additions & 3 deletions test/sym/store.wat
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
(module
(import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
(import "symbolic" "assume" (func $owi_assume (param i32)))

(memory $m 1)

Expand All @@ -8,9 +9,15 @@

(local $idx i32)

(local.tee $idx (call $i32_symbol))
call $i32_symbol
i32.store
(local.set $idx (call $i32_symbol))

;; Hackish way to reduce the size of the search space. Otherwise, all possible
;; values of idx between 0 and <page_size> get checked.
(call $owi_assume
(i32.eqz (i32.rem_s (local.get $idx) (i32.const 4096)))
)

(i32.store (local.get $idx) (i32.const 42))
)

(start $start)
Expand Down

0 comments on commit c535389

Please sign in to comment.