From 8db96458ddd1c5ee667556ae4413f91edfff9c80 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Wed, 4 Sep 2024 20:57:31 +0200 Subject: [PATCH] add `owi replay` --- CHANGES.md | 1 + README.md | 2 + example/README.md | 4 + example/replay/README.md | 91 ++++++++++++++++++++++ example/replay/dune | 4 + example/replay/mini.wat | 11 +++ src/bin/owi.ml | 38 ++++++++- src/cmd/cmd_c.ml | 8 +- src/cmd/cmd_replay.ml | 116 ++++++++++++++++++++++++++++ src/cmd/cmd_replay.mli | 5 ++ src/data_structures/sexp.ml | 111 ++++++++++++++++++++++++++ src/data_structures/sexp.mli | 2 + src/dune | 1 + src/utils/result.ml | 2 + src/utils/result.mli | 1 + test/help/help.t | 4 + test/replay/dune | 9 +++ test/replay/missing_replay_file.t | 5 ++ test/replay/missing_replay_file.wat | 1 + test/replay/no_bug.model | 1 + test/replay/no_bug.t | 22 ++++++ test/replay/no_bug.wat | 7 ++ test/replay/simple.model | 3 + test/replay/simple.t | 32 ++++++++ test/replay/simple.wat | 9 +++ 25 files changed, 482 insertions(+), 8 deletions(-) create mode 100644 example/replay/README.md create mode 100644 example/replay/dune create mode 100644 example/replay/mini.wat create mode 100644 src/cmd/cmd_replay.ml create mode 100644 src/cmd/cmd_replay.mli create mode 100644 test/replay/dune create mode 100644 test/replay/missing_replay_file.t create mode 100644 test/replay/missing_replay_file.wat create mode 100644 test/replay/no_bug.model create mode 100644 test/replay/no_bug.t create mode 100644 test/replay/no_bug.wat create mode 100644 test/replay/simple.model create mode 100644 test/replay/simple.t create mode 100644 test/replay/simple.wat diff --git a/CHANGES.md b/CHANGES.md index 1bb94a343..d8b9d9806 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,6 @@ ## unreleased +- add `owi replay` command to check a model produced by symbolic execution on a concrete execution - add `owi instrument` to instrument Webassembly module annotated by Weasel specification language - add `--srac` option to `sym` and `conc` cmd - add `--rac` option to `run`, `sym` and `conc` cmd diff --git a/README.md b/README.md index d56625837..55448773c 100644 --- a/README.md +++ b/README.md @@ -6,6 +6,7 @@ - [`owi conc`]: a concolic Wasm interpreter; - [`owi fmt`]: a formatter for Wasm; - [`owi opt`]: an optimizer for Wasm; +- [`owi replay`]: run a module containing symbols with concrete values from a model produced by a previous symbolic execution - [`owi run`]: a concrete Wasm interpreter; - [`owi script`]: an interpreter for [Wasm scripts]; - [`owi sym`]: a symbolic Wasm interpreter; @@ -214,6 +215,7 @@ This project was partly funded through the [NGI0 Core] Fund, a fund established [`owi conc`]: example/conc [`owi fmt`]: example/fmt [`owi opt`]: example/opt +[`owi replay`]: example/replay [`owi run`]: example/run [`owi script`]: example/script [`owi sym`]: example/sym diff --git a/example/README.md b/example/README.md index 5c6dc10bc..03322c8fb 100644 --- a/example/README.md +++ b/example/README.md @@ -45,6 +45,10 @@ COMMANDS opt [--debug] [--output=FILE] [--unsafe] [OPTION]… ARG Optimize a module + replay [OPTION]… ARG + Replay a module containing symbols with concrete values in a + replay file containing a model + run [OPTION]… [ARG]… Run the concrete interpreter diff --git a/example/replay/README.md b/example/replay/README.md new file mode 100644 index 000000000..c454bc742 --- /dev/null +++ b/example/replay/README.md @@ -0,0 +1,91 @@ +# Symbolic interpreter + +## Basic example + +First, you need to perform a symbolic run and to store the output model in a file. Given the following `mini.wat` file containing symbols: + + +```wat +(module + (import "symbolic" "i32_symbol" (func $gen_i32 (result i32))) + + (func $start (local $x i32) + (local.set $x (call $gen_i32)) + (if (i32.lt_s (i32.const 5) (local.get $x)) (then + unreachable + ))) + + (start $start) +) +``` + +You can get a model like this: + +```sh +$ owi sym ./mini.wat > mini.model +Reached problem! +[13] +``` + +Then you can replay the module execution with the values in the model like this: + +```sh +$ owi replay --replay-file mini.model mini.wat +invalid model: can not find the directive `model` while parsing the scfg config +[78] +``` + +## Man page + +```sh +$ owi replay --help=plain +NAME + owi-replay - Replay a module containing symbols with concrete values + in a replay file containing a model + +SYNOPSIS + owi replay [OPTION]… ARG + +OPTIONS + -d, --debug + debug mode + + --optimize + optimize mode + + -p, --profiling + profiling mode + + --replay-file=VAL (required) + Which replay file to use + + -u, --unsafe + skip typechecking pass + +COMMON OPTIONS + --help[=FMT] (default=auto) + Show this help in format FMT. The value FMT must be one of auto, + pager, groff or plain. With auto, the format is pager or plain + whenever the TERM env var is dumb or undefined. + + --version + Show version information. + +EXIT STATUS + owi replay exits with: + + 0 on success. + + 123 on indiscriminate errors reported on standard error. + + 124 on command line parsing errors. + + 125 on unexpected internal errors (bugs). + +BUGS + Email them to . + +SEE ALSO + owi(1) + +``` diff --git a/example/replay/dune b/example/replay/dune new file mode 100644 index 000000000..d3c998951 --- /dev/null +++ b/example/replay/dune @@ -0,0 +1,4 @@ +(mdx + (libraries owi) + (deps %{bin:owi} mini.wat) + (files README.md)) diff --git a/example/replay/mini.wat b/example/replay/mini.wat new file mode 100644 index 000000000..9db4a3083 --- /dev/null +++ b/example/replay/mini.wat @@ -0,0 +1,11 @@ +(module + (import "symbolic" "i32_symbol" (func $gen_i32 (result i32))) + + (func $start (local $x i32) + (local.set $x (call $gen_i32)) + (if (i32.lt_s (i32.const 5) (local.get $x)) (then + unreachable + ))) + + (start $start) +) diff --git a/src/bin/owi.ml b/src/bin/owi.ml index 80e91dff1..c456e4f91 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -41,8 +41,21 @@ let files = let sourcefile = let doc = "source file" in - let f = existing_non_dir_file in - Cmdliner.Arg.(required & pos 0 (some f) None (info [] ~doc)) + Cmdliner.Arg.( + required & pos 0 (some existing_non_dir_file) None (info [] ~doc) ) + +let replay_file = + let parse s = + let path = Fpath.v s in + match Bos.OS.File.exists path with + | Ok true -> Ok path + | Ok false -> Error (`Msg (Fmt.str "no file '%a'" Fpath.pp path)) + | Error _e as e -> e + in + let replay_file = Cmdliner.Arg.conv (parse, Fpath.pp) in + let doc = "Which replay file to use" in + Cmdliner.Arg.( + required & opt (some replay_file) None & info [ "replay-file" ] ~doc ) let outfile = let doc = "Write output to a file." in @@ -273,6 +286,21 @@ let sym_cmd = $ no_assert_failure_expression_printing $ deterministic_result_order $ fail_mode $ workspace $ solver $ files ) +let replay_cmd = + let open Cmdliner in + let info = + let doc = + "Replay a module containing symbols with concrete values in a replay \ + file containing a model" + in + let man = [] @ shared_man in + Cmd.info "replay" ~version ~doc ~sdocs ~man + in + Cmd.v info + Term.( + const Cmd_replay.cmd $ profiling $ debug $ unsafe $ optimize $ replay_file + $ sourcefile ) + let conc_cmd = let open Cmdliner in let info = @@ -325,13 +353,14 @@ let cli = in Cmd.group info ~default [ c_cmd + ; conc_cmd ; fmt_cmd - ; opt_cmd ; instrument_cmd + ; opt_cmd + ; replay_cmd ; run_cmd ; script_cmd ; sym_cmd - ; conc_cmd ; validate_cmd ; wasm2wat_cmd ; wat2wasm_cmd @@ -424,6 +453,7 @@ let exit_code = | `Unclosed_comment -> 75 | `Unclosed_string -> 76 | `Unbounded_quantification -> 77 + | `Invalid_model _msg -> 78 end end | Error e -> ( diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index b63549c65..b32f8b1b9 100644 --- a/src/cmd/cmd_c.ml +++ b/src/cmd/cmd_c.ml @@ -20,7 +20,7 @@ let find location file : Fpath.t Result.t = list_map (fun dir -> let filename = Fpath.append dir file in - match Bos.OS.File.exists filename with + match OS.File.exists filename with | Ok true -> Ok (Some filename) | Ok false -> Ok None | Error (`Msg msg) -> Error (`Msg msg) ) @@ -68,7 +68,7 @@ let eacsl_instrument eacsl debug ~includes (files : Fpath.t list) : files in - let framac : Fpath.t -> Fpath.t -> Bos.Cmd.t = + let framac : Fpath.t -> Fpath.t -> Cmd.t = fun file out -> Cmd.(framac_bin %% flags1 % p file %% flags2 % p out) in @@ -120,7 +120,7 @@ let compile ~includes ~opt_lvl debug (files : Fpath.t list) : Fpath.t Result.t = let* libc = find binc_location (Fpath.v "libc.wasm") in let files = Cmd.of_list (List.map Fpath.to_string (libc :: files)) in - let clang : Bos.Cmd.t = Cmd.(clang_bin %% flags % "-o" % p out %% files) in + let clang : Cmd.t = Cmd.(clang_bin %% flags % "-o" % p out %% files) in let+ () = match OS.Cmd.run clang with @@ -152,7 +152,7 @@ let metadata ~workspace arch property files : unit Result.t = let* hash = list_fold_left (fun context file -> - let+ str = Bos.OS.File.read file in + let+ str = OS.File.read file in Digestif.SHA256.feed_string context str ) Digestif.SHA256.empty files in diff --git a/src/cmd/cmd_replay.ml b/src/cmd/cmd_replay.ml new file mode 100644 index 000000000..2a100990d --- /dev/null +++ b/src/cmd/cmd_replay.ml @@ -0,0 +1,116 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +open Syntax + +let run_file ~unsafe ~optimize filename model = + let next = + let next = ref ~-1 in + fun () -> + incr next; + !next + in + + let assume_i32 _ = () in + + let assume_positive_i32 _ = () in + + 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 + in + + let symbol_char = symbol_i32 in + + let symbol_i8 = symbol_i32 in + + let symbol_i64 () = + match model.(next ()) with Concrete_value.I64 n -> n | _ -> assert false + in + + let symbol_f32 () = + match model.(next ()) with Concrete_value.F32 n -> n | _ -> assert false + in + + let symbol_f64 () = + match model.(next ()) with Concrete_value.F64 n -> n | _ -> assert false + in + + let replay_extern_module = + let functions = + [ ( "i8_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), symbol_i8) + ) + ; ( "char_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), symbol_char) + ) + ; ( "i32_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), symbol_i32) + ) + ; ( "i64_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I64), symbol_i64) + ) + ; ( "f32_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 F32), symbol_f32) + ) + ; ( "f64_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 F64), symbol_f64) + ) + ; ( "assume" + , Concrete_value.Func.Extern_func (Func (Arg (I32, Res), R0), assume_i32) + ) + ; ( "assume_positive_i32" + , Concrete_value.Func.Extern_func + (Func (Arg (I32, Res), R0), assume_positive_i32) ) + ; ( "assert" + , Concrete_value.Func.Extern_func (Func (Arg (I32, Res), R0), assert_i32) + ) + ] + in + { Link.functions } + in + + let link_state = + Link.extern_module Link.empty_state ~name:"symbolic" replay_extern_module + in + + let* m = + Compile.File.until_binary_validate ~rac:false ~srac:false ~unsafe filename + in + let* m = Cmd_utils.add_main_as_start m in + let* m, link_state = + Compile.Binary.until_link ~unsafe link_state ~optimize ~name:None m + in + let c = Interpret.Concrete.modul link_state.envs m in + c + +let cmd profiling debug unsafe optimize replay_file file = + if profiling then Log.profiling_on := true; + if debug then Log.debug_on := true; + let* model = + match Smtml.Model.Parse.Scfg.from_file replay_file with + | Error msg -> Error (`Invalid_model msg) + | Ok model -> + let+ model = + list_map + (fun (_sym, v) -> + match v with + | Smtml.Value.False -> Ok (Concrete_value.I32 0l) + | True -> Ok (Concrete_value.I32 1l) + | Num (I8 n) -> Ok (Concrete_value.I32 (Int32.of_int n)) + | Num (I32 n) -> Ok (Concrete_value.I32 n) + | Num (I64 n) -> Ok (Concrete_value.I64 n) + | Num (F32 n) -> Ok (Concrete_value.F32 (Float32.of_bits n)) + | Num (F64 n) -> Ok (Concrete_value.F64 (Float64.of_bits n)) + | Unit | Int _ | Real _ | Str _ | List _ | App _ | Nothing -> + Error + (`Invalid_model + (Fmt.str "unexpected value type: %a" Smtml.Value.pp v) ) ) + (Smtml.Model.get_bindings model) + in + Array.of_list model + in + let+ () = run_file ~unsafe ~optimize file model in + Fmt.pr "All OK@." diff --git a/src/cmd/cmd_replay.mli b/src/cmd/cmd_replay.mli new file mode 100644 index 000000000..8301e9176 --- /dev/null +++ b/src/cmd/cmd_replay.mli @@ -0,0 +1,5 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +val cmd : bool -> bool -> bool -> bool -> Fpath.t -> Fpath.t -> unit Result.t diff --git a/src/data_structures/sexp.ml b/src/data_structures/sexp.ml index 457f24a39..80aa8ce1e 100644 --- a/src/data_structures/sexp.ml +++ b/src/data_structures/sexp.ml @@ -9,3 +9,114 @@ let rec pp_sexp fmt = function | List [] -> pf fmt "()" | List (_ as l) -> pf fmt "@[(%a)@]" (list ~sep:(fun fmt () -> pf fmt "@ ") pp_sexp) l + +(* Parser taken from: https://www.martinjosefsson.com/parser/compiler/interpreter/programming/language/2019/04/03/Simple-S_expression_parser_in_OCaml.html + + The MIT License (MIT) + + Copyright © 2019 Martin Josefsson + + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the “Software”), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. + + The software is provided “as is”, without warranty of any kind, express or implied, including but not limited to the warranties of merchantability, fitness for a particular purpose and noninfringement. In no event shall the authors or copyright holders be liable for any claim, damages or other liability, whether in an action of contract, tort or otherwise, arising from, out of or in connection with the software or the use or other dealings in the software. +*) + +let str = String.concat "" + +type token = + | SymbolToken of string + | ListOpening + | ListClosing + | EndOfTransmission + +let rest : string -> string = fun s -> String.sub s 1 (String.length s - 1) + +let slurp_until_end_quote_and_give_me_the_string rest_of_quoted_symbol = + let rec inner : string -> string -> string = + fun src_str symbol_buffer -> + match src_str.[0] with + | '\'' -> symbol_buffer + | _ -> + inner (rest src_str) (str [ symbol_buffer; String.make 1 src_str.[0] ]) + in + inner rest_of_quoted_symbol "" + +let slurp_until_symbol_end : string -> string = + fun src -> + let rec iter src acc = + if String.equal src "" then acc + else + match src.[0] with + | ' ' | '\n' | '\t' | '(' | ')' -> acc + | _ -> iter (rest src) (String.concat "" [ acc; String.make 1 src.[0] ]) + in + iter src "" + +let tokenize : string -> token list = + fun src -> + let rec tokenize_iter4 : string -> token list -> token list = + fun src acc -> + if String.equal src "" then EndOfTransmission :: acc + else + match src.[0] with + | ' ' | '\n' -> tokenize_iter4 (rest src) acc (* just skip one *) + | '\'' -> + let symbol = slurp_until_end_quote_and_give_me_the_string (rest src) in + let symbol_length = String.length symbol + 2 in + let src_with_symbol_cut_off = + String.sub src symbol_length + (String.length src - symbol_length (* - 2 *)) + in + SymbolToken symbol :: tokenize_iter4 src_with_symbol_cut_off acc + | '(' -> ListOpening :: tokenize_iter4 (rest src) acc + | ')' -> ListClosing :: tokenize_iter4 (rest src) acc + | _ -> + let symbol = slurp_until_symbol_end src in + let symbol_length = String.length symbol in + let src_with_symbol_cut_off = + String.sub src symbol_length (String.length src - symbol_length) + in + SymbolToken symbol :: tokenize_iter4 src_with_symbol_cut_off acc + in + tokenize_iter4 src [] + +type ('i, 'e) parse_result = + | ParseNext of 'i * 'e + | ParseOut of 'i + | ParseEnd + +let parse_list iterator parse_s_expressions = + match parse_s_expressions iterator [] with + | next_iterator, expressions -> ParseNext (next_iterator, List expressions) + +let parse_expression (iterator : int * token list) parse_s_expressions = + let index, tokens = iterator in + let current_token = List.nth tokens index in + match current_token with + | EndOfTransmission -> ParseEnd + | ListOpening -> parse_list (index + 1, tokens) parse_s_expressions + | ListClosing -> ParseOut (index + 1, tokens) + | SymbolToken s -> ParseNext ((index + 1, tokens), Atom s) + +let s_expression_of_token_list : token list -> t = + fun tokens -> + let rec parse_s_expressions (iterator : int * token list) + (expressions : t list) = + match parse_expression iterator parse_s_expressions with + | ParseEnd -> (iterator, List.rev expressions) + | ParseOut iterator -> (iterator, List.rev expressions) + | ParseNext (iterator, result) -> + parse_s_expressions iterator (result :: expressions) + in + match parse_s_expressions (0, tokens) [] with + | _, [ first ] -> first + | _, _first :: _throw_away -> assert false + | _, [] -> List [] + +(* end of code taken somewhere else *) + +let of_string s = + let tokens = tokenize s in + s_expression_of_token_list tokens diff --git a/src/data_structures/sexp.mli b/src/data_structures/sexp.mli index a50a04f9e..0bdc4277c 100644 --- a/src/data_structures/sexp.mli +++ b/src/data_structures/sexp.mli @@ -5,3 +5,5 @@ type t = | List of t list val pp_sexp : formatter -> t -> unit + +val of_string : string -> t diff --git a/src/dune b/src/dune index 9490b7f47..c25944b6b 100644 --- a/src/dune +++ b/src/dune @@ -18,6 +18,7 @@ cmd_fmt cmd_instrument cmd_opt + cmd_replay cmd_run cmd_script cmd_sym diff --git a/src/utils/result.ml b/src/utils/result.ml index 7d53086f4..7064a0bb9 100644 --- a/src/utils/result.ml +++ b/src/utils/result.ml @@ -82,6 +82,7 @@ type err = | `Unclosed_comment | `Unclosed_string | `Unbounded_quantification + | `Invalid_model of string ] type 'a t = ('a, err) Prelude.Result.t @@ -177,3 +178,4 @@ let rec err_to_string = function | `Unclosed_comment -> Fmt.str "unclosed comment" | `Unclosed_string -> Fmt.str "unclosed string" | `Unbounded_quantification -> Fmt.str "unbounded quantification" + | `Invalid_model msg -> Fmt.str "invalid model: %s" msg diff --git a/src/utils/result.mli b/src/utils/result.mli index acf6dde9c..1536ab8dc 100644 --- a/src/utils/result.mli +++ b/src/utils/result.mli @@ -82,6 +82,7 @@ type err = | `Unclosed_comment | `Unclosed_string | `Unbounded_quantification + | `Invalid_model of string ] type 'a t = ('a, err) Prelude.Result.t diff --git a/test/help/help.t b/test/help/help.t index 3ea92ba12..0377bfa03 100644 --- a/test/help/help.t +++ b/test/help/help.t @@ -23,6 +23,10 @@ no subcommand should print help opt [--debug] [--output=FILE] [--unsafe] [OPTION]… ARG Optimize a module + replay [OPTION]… ARG + Replay a module containing symbols with concrete values in a + replay file containing a model + run [OPTION]… [ARG]… Run the concrete interpreter diff --git a/test/replay/dune b/test/replay/dune new file mode 100644 index 000000000..229eb20dc --- /dev/null +++ b/test/replay/dune @@ -0,0 +1,9 @@ +(cram + (deps + %{bin:owi} + (package owi) + missing_replay_file.wat + no_bug.model + no_bug.wat + simple.model + simple.wat)) diff --git a/test/replay/missing_replay_file.t b/test/replay/missing_replay_file.t new file mode 100644 index 000000000..8015bb58c --- /dev/null +++ b/test/replay/missing_replay_file.t @@ -0,0 +1,5 @@ + $ owi replay missing_replay_file.wat + owi: required option --replay-file is missing + Usage: owi replay [OPTION]… ARG + Try 'owi replay --help' or 'owi --help' for more information. + [124] diff --git a/test/replay/missing_replay_file.wat b/test/replay/missing_replay_file.wat new file mode 100644 index 000000000..3af8f2545 --- /dev/null +++ b/test/replay/missing_replay_file.wat @@ -0,0 +1 @@ +(module) diff --git a/test/replay/no_bug.model b/test/replay/no_bug.model new file mode 100644 index 000000000..12fae23f5 --- /dev/null +++ b/test/replay/no_bug.model @@ -0,0 +1 @@ +model diff --git a/test/replay/no_bug.t b/test/replay/no_bug.t new file mode 100644 index 000000000..d15186a0e --- /dev/null +++ b/test/replay/no_bug.t @@ -0,0 +1,22 @@ + $ owi replay --replay-file no_bug.model no_bug.wat + All OK + $ owi replay --replay-file no_bug.model no_bug.wat --debug + parsing ... + checking ... + grouping ... + assigning ... + rewriting ... + typechecking ... + typechecking ... + linking ... + interpreting ... + stack : [ ] + running instr: call 0 + calling func : func f + stack : [ ] + running instr: i32.const 42 + stack : [ i32.const 42 ] + running instr: drop + stack : [ ] + stack : [ ] + All OK diff --git a/test/replay/no_bug.wat b/test/replay/no_bug.wat new file mode 100644 index 000000000..eb44b738f --- /dev/null +++ b/test/replay/no_bug.wat @@ -0,0 +1,7 @@ +(module + (func $f + i32.const 42 + drop + ) + (start $f) +) diff --git a/test/replay/simple.model b/test/replay/simple.model new file mode 100644 index 000000000..6e10a6ad9 --- /dev/null +++ b/test/replay/simple.model @@ -0,0 +1,3 @@ +model { + symbol symbol_0 i32 42 +} diff --git a/test/replay/simple.t b/test/replay/simple.t new file mode 100644 index 000000000..8cfbc6fec --- /dev/null +++ b/test/replay/simple.t @@ -0,0 +1,32 @@ + $ owi replay --replay-file simple.model simple.wat + unreachable + [26] + $ owi replay --replay-file simple.model simple.wat --debug + parsing ... + checking ... + grouping ... + assigning ... + rewriting ... + typechecking ... + typechecking ... + linking ... + interpreting ... + stack : [ ] + running instr: call 1 + 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 + unreachable + ) + ) + stack : [ ] + running instr: unreachable + unreachable + [26] diff --git a/test/replay/simple.wat b/test/replay/simple.wat new file mode 100644 index 000000000..0ca325688 --- /dev/null +++ b/test/replay/simple.wat @@ -0,0 +1,9 @@ +(module + + (import "symbolic" "i32_symbol" (func $i32_symbol (result i32))) + + (func $start + (i32.eq (i32.const 42) (call $i32_symbol)) + (if (then unreachable))) + + (start $start))