work on replay command

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
 

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

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

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@."

src/data_structures/sexp.ml

@@ -9,3 +9,114 @@ let rec pp_sexp fmt = function
   | List [] -> pf fmt "()"
   | List (_ as l) ->
     pf fmt "@[<b>(%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

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

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
 

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))

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]

test/replay/missing_replay_file.wat

@@ -0,0 +1 @@
+(module)

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

test/replay/no_bug.wat

@@ -0,0 +1,7 @@
+(module
+  (func $f
+    i32.const 42
+    drop
+  )
+  (start $f)
+)

test/replay/simple.model

@@ -0,0 +1 @@
+(symbol_0 (i32 42))