Skip to content
Draft
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
20 changes: 17 additions & 3 deletions shell.nix
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,10 @@
}:

let
bootstrapGhcWasm = pkgs.fetchurl {
url = "https://gitlab.haskell.org/haskell-wasm/ghc-wasm-meta/-/raw/master/bootstrap.sh";
sha256 = "sha256-ma3MaYD8TWhTGb/Sohivp08GJMYR/2Nqt5ymuX7cvJc=";
};
ocamlPackages = pkgs.ocamlPackages.overrideScope (self: super: {
ocaml = (super.ocaml.overrideAttrs {
doCheck = false;
Expand All @@ -29,7 +33,7 @@ let
smtml = super.smtml.overrideAttrs (old: {
src = fetchGit {
url = "https://github.com/formalsec/smtml";
rev = "d1f09d5aeb4c6cbde5f2604c3e25915fbb28817d";
rev = "65c7da28d2aa7c2a94cc1ffdc727382cdf38c136";
};
});
});
Expand Down Expand Up @@ -61,10 +65,13 @@ pkgs.mkShell {
ocb
odoc
sedlex
# unwrapped because wrapped tries to enforce a target and the build script wants to do its own thing
pkgs.llvmPackages.clang-unwrapped
pkgs.curl
pkgs.git
pkgs.jq
# lld + llc isn't included in unwrapped, so we pull it in here
pkgs.llvmPackages.bintools-unwrapped
# unwrapped because wrapped tries to enforce a target and the build script wants to do its own thing
pkgs.llvmPackages.clang-unwrapped
tinygo
pkgs.rustc
pkgs.zig
Expand Down Expand Up @@ -104,5 +111,12 @@ pkgs.mkShell {
pkgs.rustc
pkgs.zig
]}

if [ ! -f "$HOME/.ghc-wasm/env" ]; then
echo "Running ghc-wasm bootstrap..."
bash "${bootstrapGhcWasm}"
fi

source "$HOME/.ghc-wasm/env"
'';
}
19 changes: 19 additions & 0 deletions src/compile/binary_to_text.ml
Original file line number Diff line number Diff line change
Expand Up @@ -234,7 +234,26 @@ let convert_f64_instr : Binary.f64_instr -> Text.f64_instr = function

let convert_v128_instr : Binary.v128_instr -> Text.v128_instr = function
| Const n -> Const n
| Not -> Not
| And -> And
| Or -> Or
| Any_true -> Any_true
| Load16x4_s (indice, memarg) ->
let indice = convert_indice indice in
let memarg = convert_memarg memarg in
Load16x4_s (indice, memarg)
| Load16x4_u (indice, memarg) ->
let indice = convert_indice indice in
let memarg = convert_memarg memarg in
Load16x4_u (indice, memarg)
| Load32_lane (indice, memarg, n) ->
let indice = convert_indice indice in
let memarg = convert_memarg memarg in
Load32_lane (indice, memarg, n)
| Load64_zero (indice, memarg) ->
let indice = convert_indice indice in
let memarg = convert_memarg memarg in
Load64_zero (indice, memarg)
| Load (indice, memarg) ->
let indice = convert_indice indice in
let memarg = convert_memarg memarg in
Expand Down
19 changes: 19 additions & 0 deletions src/compile/rewrite.ml
Original file line number Diff line number Diff line change
Expand Up @@ -276,7 +276,26 @@ let rewrite_f64_instr assigned : Text.f64_instr -> Binary.f64_instr Result.t =
let rewrite_v128_instr assigned : Text.v128_instr -> Binary.v128_instr Result.t
= function
| Const f -> Ok (Const f : Binary.v128_instr)
| Not -> Ok Not
| And -> Ok And
| Or -> Ok Or
| Any_true -> Ok Any_true
| Load16x4_s (indice, memarg) ->
let* memarg = rewrite_memarg memarg in
let+ indice = Assigned.find_memory assigned indice in
(Load16x4_s (indice, memarg) : Binary.v128_instr)
| Load16x4_u (indice, memarg) ->
let* memarg = rewrite_memarg memarg in
let+ indice = Assigned.find_memory assigned indice in
(Load16x4_u (indice, memarg) : Binary.v128_instr)
| Load32_lane (indice, memarg, n) ->
let* memarg = rewrite_memarg memarg in
let+ indice = Assigned.find_memory assigned indice in
(Load32_lane (indice, memarg, n) : Binary.v128_instr)
| Load64_zero (indice, memarg) ->
let* memarg = rewrite_memarg memarg in
let+ indice = Assigned.find_memory assigned indice in
(Load64_zero (indice, memarg) : Binary.v128_instr)
| Load (indice, memarg) ->
let* memarg = rewrite_memarg memarg in
let+ indice = Assigned.find_memory assigned indice in
Expand Down
8 changes: 8 additions & 0 deletions src/concrete/concrete_i32.ml
Original file line number Diff line number Diff line change
Expand Up @@ -96,3 +96,11 @@ let pp = Fmt.int32
let of_int32 (v : int32) : t = v

let to_int32 (v : t) : int32 = v

let min_int = Int32.min_int

let eqz (v : t) = eq v zero

let ( = ) = eq

let ( + ) = add
12 changes: 12 additions & 0 deletions src/concrete/concrete_i64.ml
Original file line number Diff line number Diff line change
Expand Up @@ -97,3 +97,15 @@ let pp = Fmt.int64
let of_int64 (v : int64) : t = v

let to_int64 (v : t) : int64 = v

let min_int = Int64.min_int

let eqz (v : t) = eq v zero

let ( = ) = eq

let ( + ) = add

let ( * ) = mul

let ( / ) = div
14 changes: 14 additions & 0 deletions src/concrete/concrete_memory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,13 @@ let store_64 mem ~addr n =
let addr = Int32.to_int addr in
Ok (Bytes.set_int64_le mem.data addr n)

let store_128 mem ~addr n =
let addr = Int32.to_int addr in
let left, right = Concrete_v128.to_i64x2 n in
Bytes.set_int64_le mem.data addr left;
Bytes.set_int64_le mem.data (addr + 8) right;
Ok ()

let load_8_s mem addr =
let addr = Int32.to_int addr in
Ok (Int32.of_int @@ Bytes.get_int8 mem.data addr)
Expand All @@ -108,6 +115,13 @@ let load_64 mem addr =
let addr = Int32.to_int addr in
Ok (Bytes.get_int64_le mem.data addr)

let load_128 mem addr =
let addr = Int32.to_int addr in
let left = Bytes.get_int64_le mem.data addr in
let right = Bytes.get_int64_le mem.data (addr + 8) in
let v = Concrete_v128.of_i64x2 left right in
Ok v

let size_in_pages mem = Int32.of_int @@ (Bytes.length mem.data / page_size)

let size mem = Int32.of_int @@ Bytes.length mem.data
1 change: 1 addition & 0 deletions src/concrete/concrete_memory.mli
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ include
with type t := t
and type i32 := Concrete_i32.t
and type i64 := Concrete_i64.t
and type v128 := Concrete_v128.t
and type 'a choice := 'a Concrete_choice.t

val get_limits : t -> Binary.Mem.Type.limits
Expand Down
4 changes: 4 additions & 0 deletions src/concrete/concrete_v128.ml
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,10 @@ let to_i32x4 = function
| I32x4 (a, b, c, d) -> (a, b, c, d)
| v -> i64x2_to_i32x4 (to_i64x2 v)

let to_i8x16 _ = raise @@ Failure "TODO"

let to_i16x8 _ = raise @@ Failure "TODO"

let zero = of_i64x2 0L 0L

let eq a b =
Expand Down
6 changes: 5 additions & 1 deletion src/concrete/concrete_value.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,10 @@

type boolean = Concrete_boolean.t

type i8 = int

type i16 = int

type i32 = Concrete_i32.t

type i64 = Concrete_i64.t
Expand All @@ -17,12 +21,12 @@ type v128 = Concrete_v128.t
type reference = Concrete_ref.t

module Boolean = Concrete_boolean
module Ref = Concrete_ref
module I32 = Concrete_i32
module I64 = Concrete_i64
module F32 = Concrete_f32
module F64 = Concrete_f64
module V128 = Concrete_v128
module Ref = Concrete_ref

type t =
| I32 of i32
Expand Down
Loading
Loading