Skip to content

Commit

Permalink
use a single shared AST instead of a functorized one, use object types
Browse files Browse the repository at this point in the history
and GADTs to forbid some constructors in a given AST
  • Loading branch information
zapashcanon committed Nov 21, 2023
1 parent 818e269 commit 9c35387
Show file tree
Hide file tree
Showing 65 changed files with 1,567 additions and 1,491 deletions.
31 changes: 16 additions & 15 deletions src/assigned.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,19 +2,19 @@
(* Copyright © 2021 Léo Andrès *)
(* Copyright © 2021 Pierre Chambart *)

open Syntax
open Types
open Simplified
open Syntax

module StrType = struct
type t = str_type
type t = simplified str_type

let compare = compare
end

module TypeMap = Map.Make (StrType)

let equal_func_types (a : func_type) (b : func_type) : bool =
let equal_func_types (a : simplified func_type) (b : simplified func_type) :
bool =
let remove_param (pt, rt) =
let pt = List.map (fun (_id, vt) -> (None, vt)) pt in
(pt, rt)
Expand All @@ -23,20 +23,20 @@ let equal_func_types (a : func_type) (b : func_type) : bool =

type t =
{ id : string option
; typ : str_type Named.t
; global : (Text.global, global_type) Runtime.t Named.t
; table : (table, table_type) Runtime.t Named.t
; typ : simplified str_type Named.t
; global : (Text.global, simplified global_type) Runtime.t Named.t
; table : (simplified table, simplified table_type) Runtime.t Named.t
; mem : (mem, limits) Runtime.t Named.t
; func : (Text.func, Text.block_type) Runtime.t Named.t
; func : (text func, (text, text) block_type) Runtime.t Named.t
; elem : Text.elem Named.t
; data : Text.data Named.t
; exports : Grouped.opt_exports
; start : Text.indice option
; start : text indice option
}

type type_acc =
{ declared_types : str_type Indexed.t list
; func_types : str_type Indexed.t list
{ declared_types : simplified str_type Indexed.t list
; func_types : simplified str_type Indexed.t list
; named_types : int String_map.t
; last_assigned_int : int
; all_types : int TypeMap.t
Expand Down Expand Up @@ -83,7 +83,7 @@ let assign_heap_type (acc : type_acc) typ : type_acc Result.t =
in
{ acc with func_types; last_assigned_int; all_types }

let assign_types (modul : Grouped.t) : str_type Named.t Result.t =
let assign_types (modul : Grouped.t) : simplified str_type Named.t Result.t =
let empty_acc : type_acc =
{ declared_types = []
; func_types = []
Expand Down Expand Up @@ -118,7 +118,8 @@ let name kind ~get_name values =
let+ named = list_fold_left assign_one String_map.empty values in
{ Named.values; named }

let check_type_id (types : str_type Named.t) (check : Grouped.type_check) =
let check_type_id (types : simplified str_type Named.t)
(check : Grouped.type_check) =
let id, func_type = check in
let* id =
match id with
Expand Down Expand Up @@ -148,7 +149,7 @@ let of_grouped (modul : Grouped.t) : t Result.t =
in
let* table =
name "table"
~get_name:(get_runtime_name (fun ((id, _) : table) -> id))
~get_name:(get_runtime_name (fun ((id, _) : simplified table) -> id))
modul.table
in
let* mem =
Expand All @@ -158,7 +159,7 @@ let of_grouped (modul : Grouped.t) : t Result.t =
in
let* func =
name "func"
~get_name:(get_runtime_name (fun ({ id; _ } : Text.func) -> id))
~get_name:(get_runtime_name (fun ({ id; _ } : text func) -> id))
modul.func
in
let* elem =
Expand Down
12 changes: 7 additions & 5 deletions src/assigned.mli
Original file line number Diff line number Diff line change
@@ -1,14 +1,16 @@
open Types

type t =
{ id : string option
; typ : Simplified.str_type Named.t
; global : (Text.global, Simplified.global_type) Runtime.t Named.t
; table : (Simplified.table, Simplified.table_type) Runtime.t Named.t
; typ : simplified str_type Named.t
; global : (Text.global, simplified global_type) Runtime.t Named.t
; table : (simplified table, simplified table_type) Runtime.t Named.t
; mem : (Types.mem, Types.limits) Runtime.t Named.t
; func : (Text.func, Text.block_type) Runtime.t Named.t
; func : (text func, (text, text) block_type) Runtime.t Named.t
; elem : Text.elem Named.t
; data : Text.data Named.t
; exports : Grouped.opt_exports
; start : Text.indice option
; start : text indice option
}

val of_grouped : Grouped.t -> t Result.t
4 changes: 1 addition & 3 deletions src/bin/owi.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,7 @@ let files =
let parse s = Ok s in
Cmdliner.Arg.(
value
& pos 0
(list ~sep:' ' (conv (parse, Format.pp_print_string)))
[] (info [] ~doc) )
& pos 0 (list ~sep:' ' (conv (parse, Format.pp_string))) [] (info [] ~doc) )

let no_exhaustion =
let doc = "no exhaustion tests" in
Expand Down
3 changes: 1 addition & 2 deletions src/choice_monad.ml
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,7 @@ let check (sym_bool : vbool) (state : Thread.t) : bool =
| _ ->
let check = no :: pc in
Format.printf "CHECK:@.%a"
(Format.pp_print_list ~pp_sep:Format.pp_print_newline
Encoding.Expression.pp )
(Format.pp_list ~pp_sep:Format.pp_print_newline Encoding.Expression.pp)
check;
let module Solver = (val solver_module) in
let r = Solver.check solver check in
Expand Down
1 change: 1 addition & 0 deletions src/cmd_script.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
val cmd : bool -> bool -> bool -> string list -> bool -> unit
6 changes: 3 additions & 3 deletions src/concrete.ml
Original file line number Diff line number Diff line change
Expand Up @@ -17,9 +17,9 @@ module P = struct

type table = Table.t

type elem = Link.Env.elem
type elem = Link_env.elem

type data = Link.Env.data
type data = Link_env.data

type global = Concrete_global.t

Expand All @@ -35,7 +35,7 @@ module P = struct

type extern_func = Concrete_value.Func.extern_func

type env = extern_func Link.Env.t
type env = extern_func Link_env.t

module Choice = struct
type 'a t = 'a
Expand Down
6 changes: 4 additions & 2 deletions src/concrete_global.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,13 @@
(* Copyright © 2021 Léo Andrès *)
(* Copyright © 2021 Pierre Chambart *)

open Types

type t =
{ mutable value : Concrete_value.t
; label : string option
; mut : Types.mut
; typ : Simplified.val_type
; mut : mut
; typ : simplified val_type
}

let value g = g.value
Expand Down
11 changes: 7 additions & 4 deletions src/concrete_global.mli
Original file line number Diff line number Diff line change
@@ -1,15 +1,18 @@
(** runtime global *)

open Types

type t =
{ mutable value : Concrete_value.t
; label : string option
; mut : Types.mut
; typ : Simplified.val_type
; mut : mut
; typ : simplified val_type
}

val value : t -> Concrete_value.t

val set_value : t -> Concrete_value.t -> unit

val typ : t -> Simplified.val_type
val typ : t -> simplified val_type

val mut : t -> Types.mut
val mut : t -> mut
16 changes: 4 additions & 12 deletions src/concrete_memory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -7,21 +7,13 @@ open Types
let page_size = 65_536

type t =
{ id : int
; label : string option
; mutable limits : limits
{ mutable limits : limits
; mutable data : bytes
}

let fresh =
let r = ref (-1) in
fun () ->
incr r;
!r

let init ?label (typ : limits) : t =
let data = Bytes.make (page_size * typ.min) '\x00' in
{ id = fresh (); label; limits = typ; data }
let init limits : t =
let data = Bytes.make (page_size * limits.min) '\x00' in
{ limits; data }

let update_memory mem data =
let limits =
Expand Down
2 changes: 1 addition & 1 deletion src/concrete_memory.mli
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ val get_limit_max : t -> int64 option

val get_limits : t -> Types.limits

val init : ?label:string -> Types.limits -> t
val init : Types.limits -> t

val update_memory : t -> bytes -> unit

Expand Down
5 changes: 2 additions & 3 deletions src/concrete_table.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
(* Copyright © 2021 Pierre Chambart *)

open Types
open Simplified

(* TODO: Concrete_value.ref_value array, gadt to constraint to the right ref_type ? *)
type table = Concrete_value.ref_value array
Expand All @@ -12,7 +11,7 @@ type t =
{ id : int
; label : string option
; limits : limits
; typ : ref_type
; typ : simplified ref_type
; mutable data : table
}

Expand All @@ -22,7 +21,7 @@ let fresh =
incr r;
!r

let init ?label (typ : table_type) : t =
let init ?label (typ : simplified table_type) : t =
let limits, ((_null, heap_type) as ref_type) = typ in
let null = Concrete_value.ref_null' heap_type in
let table = Array.make limits.min null in
Expand Down
11 changes: 7 additions & 4 deletions src/concrete_table.mli
Original file line number Diff line number Diff line change
@@ -1,11 +1,14 @@
(** runtime table *)

open Types

type table = Concrete_value.ref_value array

type t =
{ id : int
; label : string option
; limits : Types.limits
; typ : Simplified.ref_type
; limits : limits
; typ : simplified ref_type
; mutable data : table
}

Expand All @@ -15,11 +18,11 @@ val set : t -> int -> Concrete_value.ref_value -> unit

val size : t -> int

val typ : t -> Simplified.ref_type
val typ : t -> simplified ref_type

val update : t -> table -> unit

val init : ?label:string -> Simplified.table_type -> t
val init : ?label:string -> simplified table_type -> t

val max_size : t -> int option

Expand Down
27 changes: 15 additions & 12 deletions src/concrete_value.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@
(* Copyright © 2021 Léo Andrès *)
(* Copyright © 2021 Pierre Chambart *)

open Types

module Make_extern_func (V : Func_intf.Value_types) (M : Func_intf.Monad_type) =
struct
type 'a m = 'a M.t
Expand Down Expand Up @@ -30,23 +32,23 @@ struct

type extern_func = Extern_func : 'a func_type * 'a -> extern_func

let elt_type (type t) (e : t telt) : Simplified.val_type =
let elt_type (type t) (e : t telt) : simplified val_type =
match e with
| I32 -> Num_type I32
| I64 -> Num_type I64
| F32 -> Num_type F32
| F64 -> Num_type F64
| Externref _ -> Ref_type (Null, Extern_ht)

let res_type (type t) (r : t rtype) : Simplified.result_type =
let res_type (type t) (r : t rtype) : simplified result_type =
match r with
| R0 -> []
| R1 a -> [ elt_type a ]
| R2 (a, b) -> [ elt_type a; elt_type b ]
| R3 (a, b, c) -> [ elt_type a; elt_type b; elt_type c ]
| R4 (a, b, c, d) -> [ elt_type a; elt_type b; elt_type c; elt_type d ]

let rec arg_type : type t r. (t, r) atype -> Simplified.param_type = function
let rec arg_type : type t r. (t, r) atype -> simplified param_type = function
| UArg tl -> arg_type tl
| Arg (hd, tl) -> (None, elt_type hd) :: arg_type tl
| NArg (name, hd, tl) -> (Some name, elt_type hd) :: arg_type tl
Expand All @@ -55,7 +57,8 @@ struct
(* let extern_type (Func (arg, res)) : Simplified.func_type = *)
(* (arg_type arg, res_type res) *)

let extern_type (Extern_func (Func (arg, res), _)) : Simplified.func_type =
let extern_type (Extern_func (Func (arg, res), _)) :
simplified Types.func_type =
(arg_type arg, res_type res)

type t = Func_intf.t
Expand Down Expand Up @@ -110,7 +113,7 @@ type t =
| F64 of Float64.t
| Ref of ref_value

let of_instr (i : Simplified.instr) : t =
let of_instr (i : simplified instr) : t =
match i with
| I32_const c -> I32 c
| I64_const c -> I64 c
Expand All @@ -119,10 +122,10 @@ let of_instr (i : Simplified.instr) : t =
| _ -> assert false

let to_instr = function
| I32 c -> Simplified.I32_const c
| I64 c -> Simplified.I64_const c
| F32 c -> Simplified.F32_const c
| F64 c -> Simplified.F64_const c
| I32 c -> I32_const c
| I64 c -> I64_const c
| F32 c -> F32_const c
| F64 c -> F64_const c
| _ -> assert false

let pp_ref fmt = function
Expand All @@ -133,12 +136,12 @@ let pp_ref fmt = function
let pp fmt = function
| I32 i -> Format.fprintf fmt "i32.const %ld" i
| I64 i -> Format.fprintf fmt "i64.const %Ld" i
| F32 f -> Format.fprintf fmt "f32.const %a" Simplified.Pp.f32 f
| F64 f -> Format.fprintf fmt "f64.const %a" Simplified.Pp.f64 f
| F32 f -> Format.fprintf fmt "f32.const %a" Float32.pp f
| F64 f -> Format.fprintf fmt "f64.const %a" Float64.pp f
| Ref r -> pp_ref fmt r

let ref_null' = function
| Simplified.Func_ht -> Funcref None
| Func_ht -> Funcref None
| Extern_ht -> Externref None
| _ -> failwith "TODO ref_null' Value.ml"

Expand Down
10 changes: 6 additions & 4 deletions src/concrete_value.mli
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
(** Module to define externref values in OCaml. You should look in the `example`
directory to understand how to use this before reading the code... *)

open Types

type externref = E : 'a Type.Id.t * 'a -> externref

module Make_extern_func (V : Func_intf.Value_types) (M : Func_intf.Monad_type) :
Expand Down Expand Up @@ -33,13 +35,13 @@ type t =

val cast_ref : externref -> 'a Type.Id.t -> 'a option

val of_instr : Simplified.instr -> t
val of_instr : simplified instr -> t

val to_instr : t -> Simplified.instr
val to_instr : t -> simplified instr

val ref_null' : Simplified.heap_type -> ref_value
val ref_null' : simplified heap_type -> ref_value

val ref_null : Simplified.heap_type -> t
val ref_null : simplified heap_type -> t

val ref_func : Func.t -> t

Expand Down
Loading

0 comments on commit 9c35387

Please sign in to comment.