Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

bug in validation #500

Open
zapashcanon opened this issue Feb 12, 2025 · 0 comments
Open

bug in validation #500

zapashcanon opened this issue Feb 12, 2025 · 0 comments
Labels
bug Something isn't working good first issue Good for newcomers

Comments

@zapashcanon
Copy link
Member

(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

@zapashcanon zapashcanon added bug Something isn't working good first issue Good for newcomers labels Feb 12, 2025
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
bug Something isn't working good first issue Good for newcomers
Projects
None yet
Development

No branches or pull requests

1 participant