Skip to content

Commit

Permalink
more tests for owi replay
Browse files Browse the repository at this point in the history
  • Loading branch information
zapashcanon committed Dec 3, 2024
1 parent a8d5033 commit e82c3b3
Show file tree
Hide file tree
Showing 5 changed files with 153 additions and 6 deletions.
41 changes: 35 additions & 6 deletions src/cmd/cmd_replay.ml
Original file line number Diff line number Diff line change
Expand Up @@ -19,23 +19,52 @@ let run_file ~unsafe ~optimize filename model =
let assert_i32 n = assert (not @@ Prelude.Int32.equal n 0l) in

let symbol_i32 () =
match model.(next ()) with Concrete_value.I32 n -> n | _ -> assert false
match model.(next ()) with
| Concrete_value.I32 n -> n
| v ->
Fmt.epr "Got value %a but expected a i32 value." Concrete_value.pp v;
assert false
in

let symbol_char = symbol_i32 in
let symbol_char () =
match model.(next ()) with
| Concrete_value.I32 n -> n
| v ->
Fmt.epr "Got value %a but expected a char (i32) value." Concrete_value.pp
v;
assert false
in

let symbol_i8 = symbol_i32 in
let symbol_i8 () =
match model.(next ()) with
| Concrete_value.I32 n -> n
| v ->
Fmt.epr "Got value %a but expected a i8 (i32) value." Concrete_value.pp v;
assert false
in

let symbol_i64 () =
match model.(next ()) with Concrete_value.I64 n -> n | _ -> assert false
match model.(next ()) with
| Concrete_value.I64 n -> n
| v ->
Fmt.epr "Got value %a but expected a i64 value." Concrete_value.pp v;
assert false
in

let symbol_f32 () =
match model.(next ()) with Concrete_value.F32 n -> n | _ -> assert false
match model.(next ()) with
| Concrete_value.F32 n -> n
| v ->
Fmt.epr "Got value %a but expected a f32 value." Concrete_value.pp v;
assert false
in

let symbol_f64 () =
match model.(next ()) with Concrete_value.F64 n -> n | _ -> assert false
match model.(next ()) with
| Concrete_value.F64 n -> n
| v ->
Fmt.epr "Got value %a but expected a f64 value." Concrete_value.pp v;
assert false
in

let replay_extern_module =
Expand Down
94 changes: 94 additions & 0 deletions test/replay/all_types.t
Original file line number Diff line number Diff line change
@@ -0,0 +1,94 @@
$ owi sym -w1 all_types.wat > all_types.model
Reached problem!
[13]
$ owi replay --replay-file all_types.model all_types.wat --debug
parsing ...
checking ...
grouping ...
assigning ...
rewriting ...
typechecking ...
typechecking ...
linking ...
interpreting ...
stack : [ ]
running instr: call 4
calling func : func start
stack : [ ]
running instr: i32.const 42
stack : [ i32.const 42 ]
running instr: call 0
stack : [ i32.const 42 ; i32.const 42 ]
running instr: i32.eq
stack : [ i32.const 1 ]
running instr: (if
(then
i64.const 84
call 2
i64.eq
(if
(then
f32.const 13.119_999_885_559_082
call 1
f32.eq
(if
(then
call 3
f64.const 12.130_000_000_000_001
f64.eq
(if
(then
unreachable
)
)
)
)
)
)
)
)
stack : [ ]
running instr: i64.const 84
stack : [ i64.const 84 ]
running instr: call 2
stack : [ i64.const 84 ; i64.const 84 ]
running instr: i64.eq
stack : [ i32.const 1 ]
running instr: (if
(then
f32.const 13.119_999_885_559_082
call 1
f32.eq
(if
(then
call 3
f64.const 12.130_000_000_000_001
f64.eq
(if
(then
unreachable
)
)
)
)
)
)
stack : [ ]
running instr: f32.const 13.119_999_885_559_082
stack : [ f32.const 13.119_999_885_559_082 ]
running instr: call 1
Got value i32.const 1095887749 but expected a f32 value.owi: internal error, uncaught exception:
File "src/cmd/cmd_replay.ml", line 59, characters 6-12: Assertion failed
Raised at Owi__Cmd_replay.run_file.symbol_f32 in file "src/cmd/cmd_replay.ml", line 59, characters 6-18
Called from Owi__Interpret.Make.exec_extern_func.apply in file "src/interpret/interpret.ml", line 529, characters 38-44
Called from Owi__Interpret.Make.exec_extern_func in file "src/interpret/interpret.ml", line 537, characters 13-45
Called from Owi__Interpret.Make.exec_vfunc in file "src/interpret/interpret.ml", line 765, characters 19-59
Called from Owi__Interpret.Make.loop in file "src/interpret/interpret.ml", line 1461, characters 19-53
Called from Owi__Interpret.Make.exec_expr in file "src/interpret/interpret.ml", line 1489, characters 17-27
Called from Owi__Interpret.Make.modul.(fun) in file "src/interpret/interpret.ml", lines 1503-1504, characters 16-22
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Owi__Interpret.Make.modul in file "src/interpret/interpret.ml", lines 1498-1511, characters 10-40
Called from Owi__Cmd_replay.cmd in file "src/cmd/cmd_replay.ml", line 144, characters 12-49
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
[125]
18 changes: 18 additions & 0 deletions test/replay/all_types.wat
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
(module

(import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
(import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
(import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
(import "symbolic" "f64_symbol" (func $f64_symbol (result f64)))

(func $start
(i32.eq (i32.const 42) (call $i32_symbol))
(if (then
(i64.eq (i64.const 84) (call $i64_symbol))
(if (then
(f32.eq (f32.const 13.12) (call $f32_symbol))
(if (then
(f64.eq (f64.const 12.13 (call $f64_symbol)))
(if (then unreachable)))))))))

(start $start))
1 change: 1 addition & 0 deletions test/replay/dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
(deps
%{bin:owi}
(package owi)
all_types.wat
missing_replay_file.wat
no_bug.model
no_bug.wat
Expand Down
5 changes: 5 additions & 0 deletions test/replay/missing_replay_file.t
Original file line number Diff line number Diff line change
Expand Up @@ -3,3 +3,8 @@
Usage: owi replay [OPTION]… ARG
Try 'owi replay --help' or 'owi --help' for more information.
[124]
$ owi replay missing_replay_file.wat --replay-file
owi: option '--replay-file' needs an argument
Usage: owi replay [OPTION]… ARG
Try 'owi replay --help' or 'owi --help' for more information.
[124]

0 comments on commit e82c3b3

Please sign in to comment.