Closed
Description
(module
(import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
(import "symbolic" "assume" (func $assume (param i32)))
(import "symbolic" "assert" (func $assert (param i32)))
(func $start (local $x i32) (local $y i32)
(local.set $x (call $i32_symbol))
(local.set $y (call $i32_symbol))
(call $positive_i32 (local.get $x)) ;; x >= 0
(call $assume (i32.gt_s (local.get $y) (i32.const 0))) ;; y > 0
;; if x + y <= 0
(if (i32.le_s (i32.add (local.get $x) (local.get $y)) (i32.const 0))
;; possible if they overflow
(then unreachable))
;; otherwise (x + y > 0)
(call $assert (i32.gt_s (i32.add (local.get $x) (local.get $y)) (i32.const 0)))
)
(start $start))$ owi sym /tmp/bug.wat
owi: internal error, uncaught exception:
File "src/text_to_binary/rewrite.ml", line 25, characters 14-20: Assertion failed
Raised at Owi__Rewrite.find in file "src/text_to_binary/rewrite.ml", line 25, characters 14-26
Called from Owi__Rewrite.rewrite_expr.find_func in file "src/text_to_binary/rewrite.ml" (inlined), line 110, characters 21-39
Called from Owi__Rewrite.rewrite_expr.body in file "src/text_to_binary/rewrite.ml", line 129, characters 15-27
Called from Owi__Syntax.list_map.(fun) in file "src/utils/syntax.ml", line 33, characters 17-20
Called from Stdlib__List.map in file "list.ml", line 87, characters 15-19
Called from Stdlib__List.map in file "list.ml", line 88, characters 14-21
Called from Owi__Syntax.list_map in file "src/utils/syntax.ml", lines 31-38, characters 7-10
Called from Owi__Rewrite.rewrite_func in file "src/text_to_binary/rewrite.ml", line 330, characters 14-63
Called from Owi__Rewrite.rewrite_runtime in file "src/text_to_binary/rewrite.ml", line 341, characters 13-16
Called from Owi__Rewrite.rewrite_named.(fun) in file "src/text_to_binary/rewrite.ml", line 353, characters 21-28
Called from Owi__Syntax.list_map.(fun) in file "src/utils/syntax.ml", line 33, characters 17-20
Called from Stdlib__List.map in file "list.ml", line 86, characters 15-19
Called from Owi__Syntax.list_map in file "src/utils/syntax.ml", lines 31-38, characters 7-10
Called from Owi__Rewrite.rewrite_named in file "src/text_to_binary/rewrite.ml", lines 349-355, characters 4-24
Called from Owi__Rewrite.modul in file "src/text_to_binary/rewrite.ml", line 524, characters 4-36
Called from Owi__Compile.Text.until_binary in file "src/ast/compile.ml", line 21, characters 13-28
Called from Owi__Compile.Text.until_binary_validate in file "src/ast/compile.ml", line 27, characters 13-46
Called from Owi__Cmd_sym.run_file in file "src/cmd/cmd_sym.ml", line 33, characters 12-74
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Owi__Cmd_sym.cmd in file "src/cmd/cmd_sym.ml", line 59, characters 4-67
Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
For some reason, positive_i32 does not exists but the validation doesn't spot it