From 95da7aa688840a8d08060d87f21758c00de3fd7c Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Sun, 24 Nov 2024 04:23:54 +0100 Subject: [PATCH] work on replay command --- example/README.md | 4 + src/bin/owi.ml | 37 +++++++++- src/cmd/cmd_c.ml | 8 +- src/cmd/cmd_replay.ml | 75 +++++++++++++++---- src/data_structures/sexp.ml | 111 ++++++++++++++++++++++++++++ src/data_structures/sexp.mli | 2 + 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 | 0 test/replay/no_bug.t | 22 ++++++ test/replay/no_bug.wat | 7 ++ test/replay/simple.model | 1 + test/replay/simple.t | 32 ++++++++ test/replay/simple.wat | 9 +++ 16 files changed, 305 insertions(+), 22 deletions(-) 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/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/src/bin/owi.ml b/src/bin/owi.ml index 80e91dff1..ef867e962 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 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 index 02f75f0f8..d7b94ebf5 100644 --- a/src/cmd/cmd_replay.ml +++ b/src/cmd/cmd_replay.ml @@ -4,9 +4,11 @@ open Syntax -module M (Model : sig +module type Model = sig val model : Concrete_value.t Array.t -end) : +end + +module M (Model : Model) : Wasm_ffi_intf.S0 with type 'a t = 'a and type memory = Concrete_memory.t @@ -52,29 +54,74 @@ end) : let exit _ = assert false end -let run_file ~unsafe ~optimize filename (module Model) = +let run_file ~unsafe ~optimize filename (module Model : Model) = let module M = M (Model) in - let* m = Compile.File.until_binary_validate ~unsafe filename in - let* m = Cmd_utils.add_main_as_start m in - let link_state = Link.empty_state in + let replay_extern_module = + let functions = + [ ( "i8_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), M.symbol_i8) + ) + ; ( "char_symbol" + , Concrete_value.Func.Extern_func + (Func (UArg Res, R1 I32), M.symbol_char) ) + ; ( "i32_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), M.symbol_i32) + ) + ; ( "i64_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I64), M.symbol_i64) + ) + ; ( "f32_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 F32), M.symbol_f32) + ) + ; ( "f64_symbol" + , Concrete_value.Func.Extern_func (Func (UArg Res, R1 F64), M.symbol_f64) + ) + ; ( "assume" + , Concrete_value.Func.Extern_func + (Func (Arg (I32, Res), R0), M.assume_i32) ) + ; ( "assume_positive_i32" + , Concrete_value.Func.Extern_func + (Func (Arg (I32, Res), R0), M.assume_positive_i32) ) + ; ( "assert" + , Concrete_value.Func.Extern_func + (Func (Arg (I32, Res), R0), M.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 parse_replay_file _replay_file : 'a Array.t = assert false +let parse_replay_file file : 'a Array.t Result.t = + let+ str = Bos.OS.File.read file in + let sexp = Sexp.of_string str in + match sexp with + | List [] -> [||] + | List [ Atom _symbol_name; List [ Atom "i32"; Atom n ] ] -> begin + match int_of_string n with + | None -> assert false + | Some n -> [| Concrete_value.I32 (Int32.of_int n) |] + end + | _ -> assert false let cmd profiling debug unsafe optimize (replay_file : Fpath.t) file = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; - let model = parse_replay_file replay_file in - let module Model : sig - val model : Concrete_value.t Array.t - end = struct + let* model = parse_replay_file replay_file in + let module Model : Model = struct let model = model end in - let _result = run_file ~unsafe ~optimize file (module Model) in - Fmt.pr "All OK@."; - Ok () + let+ () = run_file ~unsafe ~optimize file (module Model) in + Fmt.pr "All OK@." 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/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..e69de29bb 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..c4ef63522 --- /dev/null +++ b/test/replay/simple.model @@ -0,0 +1 @@ +(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))