add options --rac and --srac

example/README.md

@@ -38,7 +38,7 @@ COMMANDS
        fmt [--inplace] [OPTION]… [ARG]…
            Format a .wat or .wast file
 
-       instrument [--debug] [--unsafe] [OPTION]… [ARG]…
+       instrument [--debug] [--symbolic] [--unsafe] [OPTION]… [ARG]…
            Generate an instrumented file with runtime assertion checking
            coming from Weasel specifications
 

example/conc/README.md

@@ -71,9 +71,15 @@ OPTIONS
        -p, --profiling
            profiling mode
 
+       --rac
+           runtime assertion checking mode
+
        -s VAL, --solver=VAL (absent=Z3)
            SMT solver to use
 
+       --srac
+           symbolic runtime assertion checking mode
+
        -u, --unsafe
            skip typechecking pass
 

example/define_host_function/README.md

@@ -85,8 +85,8 @@ let pure_wasm_module =
 (* our pure wasm module, linked with `sausage` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module
   with
   | Error _ -> assert false
   | Ok v -> v
@@ -203,8 +203,8 @@ let pure_wasm_module =
 (* our pure wasm module, linked with `chorizo` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module
   with
   | Error _ -> assert false
   | Ok v -> v

example/define_host_function/extern.ml

@@ -39,8 +39,8 @@ let pure_wasm_module =
 (* our pure wasm module, linked with `sausage` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module
   with
   | Error _ -> assert false
   | Ok v -> v

example/define_host_function/extern_mem.ml

@@ -38,8 +38,8 @@ let pure_wasm_module =
 (* our pure wasm module, linked with `chorizo` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module
   with
   | Error _ -> assert false
   | Ok v -> v

example/define_host_function/life_game/life_console.ml

@@ -64,8 +64,8 @@ let pure_wasm_module_1 =
 (* our first pure wasm module, linked with `life_ext` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true
-      ~name:(Some "life") pure_wasm_module_1
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:(Some "life") pure_wasm_module_1
   with
   | Error _ -> assert false
   | Ok (m, state) -> (m, state)
@@ -85,8 +85,8 @@ let pure_wasm_module_2 =
 (* our second pure wasm module, linked with `life_ext` and `life` interpreted before *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module_2
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module_2
   with
   | Error _ -> assert false
   | Ok (m, state) -> (m, state)

example/define_host_function/life_game/life_graphics.ml

@@ -76,8 +76,8 @@ let pure_wasm_module_1 =
 (* our first pure wasm module, linked with `life_ext` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true
-      ~name:(Some "life") pure_wasm_module_1
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:(Some "life") pure_wasm_module_1
   with
   | Error _ -> assert false
   | Ok (m, state) -> (m, state)
@@ -97,8 +97,8 @@ let pure_wasm_module_2 =
 (* our second pure wasm module, linked with `life_ext` and `life` interpreted before *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module_2
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module_2
   with
   | Error _ -> assert false
   | Ok (m, state) -> (m, state)

example/lib/README.md

@@ -16,7 +16,7 @@ val filename : Fpath.t = <abstr>
 val m : Text.modul =
 ...
 # let module_to_run, link_state =
-    match Compile.Text.until_link Link.empty_state ~unsafe:false ~optimize:false ~name:None m with
+    match Compile.Text.until_link Link.empty_state ~unsafe:false ~rac:false ~srac:false ~optimize:false ~name:None m with
     | Ok v -> v
     | Error _ -> assert false;;
 val module_to_run : '_weak1 Link.module_to_run =

example/run/README.md

@@ -70,6 +70,9 @@ OPTIONS
        -p, --profiling
            profiling mode
 
+       --rac
+           runtime assertion checking mode
+
        -u, --unsafe
            skip typechecking pass
 

example/sym/README.md

@@ -75,9 +75,15 @@ OPTIONS
        -p, --profiling
            profiling mode
 
+       --rac
+           runtime assertion checking mode
+
        -s VAL, --solver=VAL (absent=Z3)
            SMT solver to use
 
+       --srac
+           symbolic runtime assertion checking mode
+
        -u, --unsafe
            skip typechecking pass
 

src/ast/binary_encoder.ml

@@ -767,6 +767,8 @@ let write_file filename content =
 
 let convert (filename : Fpath.t) ~unsafe ~optimize m =
   Log.debug0 "bin encoding ...@\n";
-  let* m = Compile.Text.until_optimize ~unsafe ~optimize m in
+  let* m =
+    Compile.Text.until_optimize ~unsafe ~rac:false ~srac:false ~optimize m
+  in
   let content = encode m in
   write_file filename content

src/ast/code_generator.ml

@@ -210,10 +210,10 @@ let rec term_generate tenv (term : binary term) :
   | Result (Some i) ->
     if i < 0 || i >= Array.length tenv.result_types then
       Error (`Spec_invalid_indice (Int.to_string i))
-    else Ok ([ Local_get (Raw i) ], tenv.result_types.(i))
+    else Ok ([ Local_get (tenv.result i) ], tenv.result_types.(i))
   | Result None ->
     if Array.length tenv.result_types = 0 then Error (`Spec_invalid_indice "0")
-    else Ok ([ Local_get (Raw 0) ], tenv.result_types.(0))
+    else Ok ([ Local_get (tenv.result 0) ], tenv.result_types.(0))
 
 let binpred_generate (b : binpred) (expr1 : binary expr) (ty1 : binary val_type)
   (expr2 : binary expr) (ty2 : binary val_type) : binary expr Result.t =

src/ast/compile.ml

@@ -16,27 +16,32 @@ module Text = struct
     let* m = until_group ~unsafe m in
     Assigned.of_grouped m
 
-  let until_binary ~unsafe m =
+  let until_binary ~unsafe ~rac ~srac m =
     let* m = until_assign ~unsafe m in
-    Rewrite.modul m
+    let* m = Rewrite.modul m in
+    if srac then Code_generator.generate true m
+    else if rac then Code_generator.generate false m
+    else Ok m
 
-  let until_binary_validate ~unsafe m =
-    let* m = until_binary ~unsafe m in
+  let until_binary_validate ~unsafe ~rac ~srac m =
+    let* m = until_binary ~unsafe ~rac ~srac m in
     if unsafe then Ok m
     else
       let+ () = Binary_validate.modul m in
       m
 
-  let until_optimize ~unsafe ~optimize m =
-    let+ m = until_binary_validate ~unsafe m in
+  let until_optimize ~unsafe ~rac ~srac ~optimize m =
+    let+ m = until_binary_validate ~unsafe ~rac ~srac m in
     if optimize then Optimize.modul m else m
 
-  let until_link ~unsafe ~optimize ~name link_state m =
-    let* m = until_optimize ~unsafe ~optimize m in
+  let until_link ~unsafe ~rac ~srac ~optimize ~name link_state m =
+    let* m = until_optimize ~unsafe ~rac ~srac ~optimize m in
     Link.modul link_state ~name m
 
-  let until_interpret ~unsafe ~optimize ~name link_state m =
-    let* m, link_state = until_link ~unsafe ~optimize ~name link_state m in
+  let until_interpret ~unsafe ~rac ~srac ~optimize ~name link_state m =
+    let* m, link_state =
+      until_link ~unsafe ~rac ~srac ~optimize ~name link_state m
+    in
     let+ () = Interpret.Concrete.modul link_state.envs m in
     link_state
 end
@@ -63,53 +68,57 @@ module Binary = struct
 end
 
 module Any = struct
-  let until_binary_validate ~unsafe = function
-    | Kind.Wat m -> Text.until_binary_validate ~unsafe m
+  let until_binary_validate ~unsafe ~rac ~srac = function
+    | Kind.Wat m -> Text.until_binary_validate ~unsafe ~rac ~srac m
     | Wasm m -> Binary.until_binary_validate ~unsafe m
     | Wast _ | Ocaml _ -> assert false
 
-  let until_optimize ~unsafe ~optimize = function
-    | Kind.Wat m -> Text.until_optimize ~unsafe ~optimize m
+  let until_optimize ~unsafe ~rac ~srac ~optimize = function
+    | Kind.Wat m -> Text.until_optimize ~unsafe ~rac ~srac ~optimize m
     | Wasm m -> Binary.until_optimize ~unsafe ~optimize m
     | Wast _ | Ocaml _ -> assert false
 
-  let until_link ~unsafe ~optimize ~name link_state = function
-    | Kind.Wat m -> Text.until_link ~unsafe ~optimize ~name link_state m
+  let until_link ~unsafe ~rac ~srac ~optimize ~name link_state = function
+    | Kind.Wat m ->
+      Text.until_link ~unsafe ~rac ~srac ~optimize ~name link_state m
     | Wasm m -> Binary.until_link ~unsafe ~optimize ~name link_state m
     | Wast _ | Ocaml _ -> assert false
 
-  let until_interpret ~unsafe ~optimize ~name link_state = function
-    | Kind.Wat m -> Text.until_interpret ~unsafe ~optimize ~name link_state m
+  let until_interpret ~unsafe ~rac ~srac ~optimize ~name link_state = function
+    | Kind.Wat m ->
+      Text.until_interpret ~unsafe ~rac ~srac ~optimize ~name link_state m
     | Wasm m -> Binary.until_interpret ~unsafe ~optimize ~name link_state m
     | Wast _ | Ocaml _ -> assert false
 end
 
 module File = struct
-  let until_binary_validate ~unsafe filename =
+  let until_binary_validate ~unsafe ~rac ~srac filename =
     let* m = Parse.guess_from_file filename in
     match m with
-    | Kind.Wat m -> Text.until_binary_validate ~unsafe m
+    | Kind.Wat m -> Text.until_binary_validate ~unsafe ~rac ~srac m
     | Wasm m -> Binary.until_binary_validate ~unsafe m
     | Wast _ | Ocaml _ -> assert false
 
-  let until_optimize ~unsafe ~optimize filename =
+  let until_optimize ~unsafe ~rac ~srac ~optimize filename =
     let* m = Parse.guess_from_file filename in
     match m with
-    | Kind.Wat m -> Text.until_optimize ~unsafe ~optimize m
+    | Kind.Wat m -> Text.until_optimize ~unsafe ~rac ~srac ~optimize m
     | Wasm m -> Binary.until_optimize ~unsafe ~optimize m
     | Wast _ | Ocaml _ -> assert false
 
-  let until_link ~unsafe ~optimize ~name link_state filename =
+  let until_link ~unsafe ~rac ~srac ~optimize ~name link_state filename =
     let* m = Parse.guess_from_file filename in
     match m with
-    | Kind.Wat m -> Text.until_link ~unsafe ~optimize ~name link_state m
+    | Kind.Wat m ->
+      Text.until_link ~unsafe ~rac ~srac ~optimize ~name link_state m
     | Wasm m -> Binary.until_link ~unsafe ~optimize ~name link_state m
     | Wast _ | Ocaml _ -> assert false
 
-  let until_interpret ~unsafe ~optimize ~name link_state filename =
+  let until_interpret ~unsafe ~rac ~srac ~optimize ~name link_state filename =
     let* m = Parse.guess_from_file filename in
     match m with
-    | Kind.Wat m -> Text.until_interpret ~unsafe ~optimize ~name link_state m
+    | Kind.Wat m ->
+      Text.until_interpret ~unsafe ~rac ~srac ~optimize ~name link_state m
     | Wasm m -> Binary.until_interpret ~unsafe ~optimize ~name link_state m
     | Wast _ | Ocaml _ -> assert false
 end

src/ast/compile.mli

@@ -6,15 +6,26 @@
 
 module Any : sig
   val until_binary_validate :
-    unsafe:bool -> 'extern_func Kind.t -> Binary.modul Result.t
+       unsafe:bool
+    -> rac:bool
+    -> srac:bool
+    -> 'extern_func Kind.t
+    -> Binary.modul Result.t
 
   val until_optimize :
-    unsafe:bool -> optimize:bool -> 'extern_func Kind.t -> Binary.modul Result.t
+       unsafe:bool
+    -> rac:bool
+    -> srac:bool
+    -> optimize:bool
+    -> 'extern_func Kind.t
+    -> Binary.modul Result.t
 
   (** compile a module with a given link state and produce a new link state and
       a runnable module *)
   val until_link :
        unsafe:bool
+    -> rac:bool
+    -> srac:bool
     -> optimize:bool
     -> name:string option
     -> 'extern_func Link.state
@@ -25,6 +36,8 @@ module Any : sig
       link state *)
   val until_interpret :
        unsafe:bool
+    -> rac:bool
+    -> srac:bool
     -> optimize:bool
     -> name:string option
     -> Concrete_value.Func.extern_func Link.state
@@ -33,15 +46,23 @@ module Any : sig
 end
 
 module File : sig
-  val until_binary_validate : unsafe:bool -> Fpath.t -> Binary.modul Result.t
+  val until_binary_validate :
+    unsafe:bool -> rac:bool -> srac:bool -> Fpath.t -> Binary.modul Result.t
 
   val until_optimize :
-    unsafe:bool -> optimize:bool -> Fpath.t -> Binary.modul Result.t
+       unsafe:bool
+    -> rac:bool
+    -> srac:bool
+    -> optimize:bool
+    -> Fpath.t
+    -> Binary.modul Result.t
 
   (** compile a file with a given link state and produce a new link state and a
       runnable module *)
   val until_link :
        unsafe:bool
+    -> rac:bool
+    -> srac:bool
     -> optimize:bool
     -> name:string option
     -> 'extern_func Link.state
@@ -52,6 +73,8 @@ module File : sig
       link state *)
   val until_interpret :
        unsafe:bool
+    -> rac:bool
+    -> srac:bool
     -> optimize:bool
     -> name:string option
     -> Concrete_value.Func.extern_func Link.state
@@ -62,17 +85,26 @@ end
 module Text : sig
   val until_text_validate : unsafe:bool -> Text.modul -> Text.modul Result.t
 
-  val until_binary : unsafe:bool -> Text.modul -> Binary.modul Result.t
+  val until_binary :
+    unsafe:bool -> rac:bool -> srac:bool -> Text.modul -> Binary.modul Result.t
 
-  val until_binary_validate : unsafe:bool -> Text.modul -> Binary.modul Result.t
+  val until_binary_validate :
+    unsafe:bool -> rac:bool -> srac:bool -> Text.modul -> Binary.modul Result.t
 
   val until_optimize :
-    unsafe:bool -> optimize:bool -> Text.modul -> Binary.modul Result.t
+       unsafe:bool
+    -> rac:bool
+    -> srac:bool
+    -> optimize:bool
+    -> Text.modul
+    -> Binary.modul Result.t
 
   (** compile a module with a given link state and produce a new link state and
       a runnable module *)
   val until_link :
        unsafe:bool
+    -> rac:bool
+    -> srac:bool
     -> optimize:bool
     -> name:string option
     -> 'f Link.state
@@ -83,6 +115,8 @@ module Text : sig
       link state *)
   val until_interpret :
        unsafe:bool
+    -> rac:bool
+    -> srac:bool
     -> optimize:bool
     -> name:string option
     -> Concrete_value.Func.extern_func Link.state