Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions doc/src/manpages/owi.md
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,10 @@ COMMANDS
fuzz [OPTION]… FILE
Run the fuzzer

haskell [OPTION]… FILE…
Compile a Haskell file to Wasm and run the symbolic interpreter on
it

instrument COMMAND …
Instrument a program in various ways

Expand Down
17 changes: 17 additions & 0 deletions src/bin/owi.ml
Original file line number Diff line number Diff line change
Expand Up @@ -425,6 +425,22 @@ let fuzz_cmd =
and+ source_file in
Cmd_fuzz.cmd ~rounds ~seed ~source_file ~timeout ~timeout_instr ~unsafe

(* owi haskell *)

let haskell_info =
let doc =
"Compile a Haskell file to Wasm and run the symbolic interpreter on it"
in
let man = [] @ shared_man in
Cmd.info "haskell" ~version ~doc ~sdocs ~man

let haskell_cmd =
let+ files
and+ out_file
and+ () = setup_log
and+ symbolic_parameters = symbolic_parameters (Some "_start") in
Cmd_haskell.cmd ~symbolic_parameters ~files ~out_file

(* owi instrument *)

let instrument_info =
Expand Down Expand Up @@ -683,6 +699,7 @@ let cli =
; Cmd.v fuzz_info fuzz_cmd
; Cmd.group instrument_info
[ Cmd.v instrument_label_info instrument_label_cmd ]
; Cmd.v haskell_info haskell_cmd
; Cmd.v iso_info iso_cmd
; Cmd.v replay_info replay_cmd
; Cmd.v run_info run_cmd
Expand Down
63 changes: 63 additions & 0 deletions src/cmd/cmd_haskell.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)

open Bos
open Syntax

let compile ~workspace ~out_file (files : Fpath.t list) : Fpath.t Result.t =
let* haskell_bin =
let name = "wasm32-wasi-ghc" in
match OS.Cmd.resolve @@ Cmd.v name with
| Error _ ->
Fmt.error_msg
"The `%s` binary was not found, please make sure it is in your path."
name
| Ok _ as ok -> ok
in

let out = Option.value ~default:Fpath.(workspace / "out.wasm") out_file in
let haskell : Cmd.t =
Cmd.(
haskell_bin
(* output and input *)
% "-o"
% p out
%% Cmd.of_list (List.map p files)
(* % p libhaskell *) )
in

let err =
match Logs.Src.level Log.main_src with
| Some (Logs.Debug | Logs.Info) -> OS.Cmd.err_run_out
| None | Some _ -> OS.Cmd.err_null
in

let+ () =
Log.bench_fn "compiling time" @@ fun () ->
match OS.Cmd.run ~err haskell with
| Ok _ as v -> v
| Error (`Msg e) ->
Log.debug (fun m -> m "haskell failed: %s" e);
Fmt.error_msg
"haskell failed: run with -vv to get the full error message if it was \
not displayed above"
in

out

let cmd ~(symbolic_parameters : Symbolic_parameters.t) ~files ~out_file :
unit Result.t =
let* workspace =
match symbolic_parameters.workspace with
| Some path -> Ok path
| None -> OS.Dir.tmp "cmd_haskell_%s"
in
let* _did_create : bool = OS.Dir.create workspace in

let* source_file = compile ~workspace ~out_file files in
let workspace = Some workspace in

let parameters = { symbolic_parameters with workspace } in

Cmd_sym.cmd ~parameters ~source_file
9 changes: 9 additions & 0 deletions src/cmd/cmd_haskell.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)

val cmd :
symbolic_parameters:Symbolic_parameters.t
-> files:Fpath.t list
-> out_file:Fpath.t option
-> unit Result.t
14 changes: 13 additions & 1 deletion src/compile/binary_to_text.ml
Original file line number Diff line number Diff line change
Expand Up @@ -232,6 +232,18 @@ let convert_f64_instr : Binary.f64_instr -> Text.f64_instr = function
let memarg = convert_memarg memarg in
Store (indice, memarg)

let convert_v128_instr : Binary.v128_instr -> Text.v128_instr = function
| Const n -> Const n
| And -> And
| Load (indice, memarg) ->
let indice = convert_indice indice in
let memarg = convert_memarg memarg in
Load (indice, memarg)
| Store (indice, memarg) ->
let indice = convert_indice indice in
let memarg = convert_memarg memarg in
Store (indice, memarg)

let convert_ref_instr : Binary.ref_instr -> Text.ref_instr = function
| Null heap_type -> Null (convert_heap_type heap_type)
| Is_null -> Is_null
Expand Down Expand Up @@ -345,7 +357,7 @@ let rec convert_instr : Binary.instr -> Text.instr = function
| I64 i -> Text.I64 (convert_i64_instr i)
| F32 i -> Text.F32 (convert_f32_instr i)
| F64 i -> Text.F64 (convert_f64_instr i)
| V128 i -> Text.V128 i
| V128 i -> Text.V128 (convert_v128_instr i)
| I8x16 i -> Text.I8x16 i
| I16x8 i -> Text.I16x8 i
| I32x4 i -> Text.I32x4 i
Expand Down
17 changes: 16 additions & 1 deletion src/compile/rewrite.ml
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,19 @@ let rewrite_f64_instr assigned : Text.f64_instr -> Binary.f64_instr Result.t =
let+ indice = Assigned.find_memory assigned indice in
(Store (indice, memarg) : Binary.f64_instr)

let rewrite_v128_instr assigned : Text.v128_instr -> Binary.v128_instr Result.t
= function
| Const f -> Ok (Const f : Binary.v128_instr)
| And -> Ok And
| Load (indice, memarg) ->
let* memarg = rewrite_memarg memarg in
let+ indice = Assigned.find_memory assigned indice in
(Load (indice, memarg) : Binary.v128_instr)
| Store (indice, memarg) ->
let* memarg = rewrite_memarg memarg in
let+ indice = Assigned.find_memory assigned indice in
(Store (indice, memarg) : Binary.v128_instr)

let rewrite_ref_instr assigned : Text.ref_instr -> Binary.ref_instr Result.t =
function
| Null heap_type ->
Expand Down Expand Up @@ -458,7 +471,9 @@ let rewrite_expr (assigned : Assigned.t) (locals : Text.param list)
| F64 i ->
let+ i = rewrite_f64_instr assigned i in
Binary.F64 i
| V128 i -> Ok (Binary.V128 i)
| V128 i ->
let+ i = rewrite_v128_instr assigned i in
Binary.V128 i
| I8x16 i -> Ok (Binary.I8x16 i)
| I16x8 i -> Ok (Binary.I16x8 i)
| I32x4 i -> Ok (Binary.I32x4 i)
Expand Down
1 change: 1 addition & 0 deletions src/dune
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@
cmd_cpp
cmd_fmt
cmd_fuzz
cmd_haskell
cmd_instrument_label
cmd_iso
cmd_replay
Expand Down
15 changes: 11 additions & 4 deletions src/interpret/interpret.ml
Original file line number Diff line number Diff line change
Expand Up @@ -736,14 +736,19 @@ struct
let+ () = Memory.store_64 mem ~addr (F64.to_bits n) in
stack

let exec_v128_instr stack : Text.v128_instr -> _ = function
let exec_v128_instr stack : Binary.v128_instr -> _ = function
| Const n -> Stack.push_concrete_v128 stack n
| And | Load _ | Store _ -> raise @@ Failure "todo"

let exec_i8x16_instr _stack : Text.i8x16_instr -> _ = function
| _ -> (* TODO *) assert false
| _ ->
(* TODO *)
raise @@ Failure "todo"

let exec_i16x8_instr _stack : Text.i16x8_instr -> _ = function
| _ -> (* TODO *) assert false
| _ ->
(* TODO *)
raise @@ Failure "todo"

let exec_i32x4_instr stack : Text.i32x4_instr -> _ = function
| Add ->
Expand All @@ -764,6 +769,7 @@ struct
let c = I32.sub c1 c2 in
let d = I32.sub d1 d2 in
Stack.push_v128 stack (V128.of_i32x4 a b c d)
| Mul -> raise @@ Failure "todo"

let exec_i64x2_instr stack : Text.i64x2_instr -> _ = function
| Add ->
Expand All @@ -780,6 +786,7 @@ struct
let a = I64.sub a1 a2 in
let b = I64.sub b1 b2 in
Stack.push_v128 stack (V128.of_i64x2 a b)
| Mul -> raise @@ Failure "todo"

let exec_ref_instr env stack : Binary.ref_instr -> _ = function
| Null t -> Stack.push_ref stack (Ref.null t) |> Choice.return
Expand Down Expand Up @@ -1268,7 +1275,7 @@ struct

let call_ref ~return:_ (_state : State.exec_state) _typ_i =
(* TODO *)
assert false
raise @@ Failure "TODO"
(* let fun_ref, stack = Stack.pop_as_ref state.stack in *)
(* let state = { state with stack } in *)
(* let func = *)
Expand Down
19 changes: 17 additions & 2 deletions src/ir/binary.ml
Original file line number Diff line number Diff line change
Expand Up @@ -536,6 +536,21 @@ let pp_f64_instr ppf = function
| Store (indice, memarg) ->
pf ppf "f64.store%a%a" pp_indice_not0 indice pp_memarg memarg

(** V128 instructions *)
type v128_instr =
| Const of Concrete_v128.t
| And
| Load of (indice * memarg)
| Store of (indice * memarg)

let pp_v128_instr ppf = function
| Const n -> pf ppf "v128.const %a" Concrete_v128.pp n
| And -> pf ppf "v128.and"
| Load (indice, memarg) ->
pf ppf "v128.load%a%a" pp_indice_not0 indice pp_memarg memarg
| Store (indice, memarg) ->
pf ppf "v128.store%a%a" pp_indice_not0 indice pp_memarg memarg

(** Reference instructions *)
type ref_instr =
| Null of heap_type
Expand Down Expand Up @@ -686,7 +701,7 @@ type instr =
| I64 of i64_instr
| F32 of f32_instr
| F64 of f64_instr
| V128 of Text.v128_instr
| V128 of v128_instr
| I8x16 of Text.i8x16_instr
| I16x8 of Text.i16x8_instr
| I32x4 of Text.i32x4_instr
Expand Down Expand Up @@ -735,7 +750,7 @@ let rec pp_instr ~short ppf = function
| I64 i -> pp_i64_instr ppf i
| F32 i -> pp_f32_instr ppf i
| F64 i -> pp_f64_instr ppf i
| V128 i -> Text.pp_v128_instr ppf i
| V128 i -> pp_v128_instr ppf i
| I8x16 i -> Text.pp_i8x16_instr ppf i
| I16x8 i -> Text.pp_i16x8_instr ppf i
| I32x4 i -> Text.pp_i32x4_instr ppf i
Expand Down
11 changes: 10 additions & 1 deletion src/ir/binary.mli
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,15 @@ type f64_instr =
| Load of indice * memarg
| Store of indice * memarg

(** V128 instructions *)
type v128_instr =
| Const of Concrete_v128.t
| And
| Load of (indice * memarg)
| Store of (indice * memarg)

val pp_v128_instr : v128_instr Fmt.t

(** Reference instructions *)
type ref_instr =
| Null of heap_type
Expand Down Expand Up @@ -308,7 +317,7 @@ type instr =
| I64 of i64_instr
| F32 of f32_instr
| F64 of f64_instr
| V128 of Text.v128_instr
| V128 of v128_instr
| I8x16 of Text.i8x16_instr
| I16x8 of Text.i16x8_instr
| I32x4 of Text.i32x4_instr
Expand Down
6 changes: 5 additions & 1 deletion src/ir/binary_encoder.ml
Original file line number Diff line number Diff line change
Expand Up @@ -472,12 +472,13 @@ let write_f64_instr buf : Binary.f64_instr -> _ =
| Reinterpret_i S32 -> (* TODO *) assert false
| Reinterpret_i S64 -> add_char '\xBF'

let write_v128_instr buf : Text.v128_instr -> _ = function
let write_v128_instr buf : Binary.v128_instr -> _ = function
| Const v ->
write_fd buf 12;
let a, b = Concrete_v128.to_i64x2 v in
write_bytes_8 buf a;
write_bytes_8 buf b
| And | Load _ | Store _ -> raise @@ Failure "TODO"

let write_i8x16_instr buf : Text.i8x16_instr -> _ = function
| Add -> write_fd buf 110
Expand All @@ -486,14 +487,17 @@ let write_i8x16_instr buf : Text.i8x16_instr -> _ = function
let write_i16x8_instr buf : Text.i16x8_instr -> _ = function
| Add -> write_fd buf 142
| Sub -> write_fd buf 145
| Mul -> raise @@ Failure "TODO"

let write_i32x4_instr buf : Text.i32x4_instr -> _ = function
| Add -> write_fd buf 174
| Sub -> write_fd buf 177
| Mul -> raise @@ Failure "TODO"

let write_i64x2_instr buf : Text.i64x2_instr -> _ = function
| Add -> write_fd buf 206
| Sub -> write_fd buf 209
| Mul -> raise @@ Failure "TODO"

let write_ref_instr buf : Binary.ref_instr -> _ =
let add_char c = Buffer.add_char buf c in
Expand Down
17 changes: 16 additions & 1 deletion src/ir/text.ml
Original file line number Diff line number Diff line change
Expand Up @@ -690,10 +690,19 @@ let pp_f64_instr ppf = function
pf ppf "f64.store%a%a" pp_indice_not0 indice pp_memarg memarg

(** V128 instructions *)
type v128_instr = Const of Concrete_v128.t
type v128_instr =
| Const of Concrete_v128.t
| And
| Load of (indice * memarg)
| Store of (indice * memarg)

let pp_v128_instr ppf = function
| Const n -> pf ppf "v128.const %a" Concrete_v128.pp n
| And -> pf ppf "v128.and"
| Load (indice, memarg) ->
pf ppf "v128.load%a%a" pp_indice_not0 indice pp_memarg memarg
| Store (indice, memarg) ->
pf ppf "v128.store%a%a" pp_indice_not0 indice pp_memarg memarg

(** I8x16 instructions *)
type i8x16_instr =
Expand All @@ -708,28 +717,34 @@ let pp_i8x16_instr ppf = function
type i16x8_instr =
| Add
| Sub
| Mul

let pp_i16x8_instr ppf = function
| Add -> pf ppf "i16x8.add"
| Sub -> pf ppf "i16x8.sub"
| Mul -> pf ppf "i16x8.mul"

(* I32x4 instructions *)
type i32x4_instr =
| Add
| Sub
| Mul

let pp_i32x4_instr ppf = function
| Add -> pf ppf "i32x4.add"
| Sub -> pf ppf "i32x4.sub"
| Mul -> pf ppf "i32x4.mul"

(** I64x2 instructions *)
type i64x2_instr =
| Add
| Sub
| Mul

let pp_i64x2_instr ppf = function
| Add -> pf ppf "i64x2.add"
| Sub -> pf ppf "i64x2.sub"
| Mul -> pf ppf "i64x2.mul"

(** Reference instructions *)
type ref_instr =
Expand Down
Loading
Loading