Skip to content

Commit

Permalink
Construct REF.FUNC_ADDR
Browse files Browse the repository at this point in the history
  • Loading branch information
@f52985
f52985 committed Jul 25, 2024
1 parent 7ccd75a commit dc06cca
Show file tree
Hide file tree
Showing 3 changed files with 85 additions and 70 deletions.
145 changes: 80 additions & 65 deletions spectec/src/backend-interpreter/construct.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -213,71 +213,6 @@ let al_to_memory_type: value -> memory_type = function
| v -> error_value "memory type" v


(* Destruct value *)

let rec al_to_field: value -> Aggr.field = function
| CaseV ("PACK", [pack_size; c]) ->
(* TODO: fix bug in packsize *)
let pack_size' =
match pack_size with
| CaseV ("I8", []) -> Pack.Pack8
| CaseV ("I16", []) -> Pack.Pack16
| CaseV ("I32", []) -> Pack.Pack32
| CaseV ("I64", []) -> Pack.Pack64
| v -> error_value "packsize" v
in
Aggr.PackField (pack_size', ref (al_to_int c))
| v -> Aggr.ValField (ref (al_to_value v))

and al_to_array: value -> Aggr.array = function
| StrV r when Record.mem "TYPE" r && Record.mem "FIELDS" r ->
Aggr.Array (
al_to_def_type (Record.find "TYPE" r),
al_to_list al_to_field (Record.find "FIELDS" r)
)
| v -> error_value "array" v

and al_to_struct: value -> Aggr.struct_ = function
| StrV r when Record.mem "TYPE" r && Record.mem "FIELDS" r ->
Aggr.Struct (
al_to_def_type (Record.find "TYPE" r),
al_to_list al_to_field (Record.find "FIELDS" r)
)
| v -> error_value "struct" v

and al_to_num: value -> num = function
| CaseV ("CONST", [ CaseV ("I32", []); i32 ]) -> I32 (al_to_int32 i32)
| CaseV ("CONST", [ CaseV ("I64", []); i64 ]) -> I64 (al_to_int64 i64)
| CaseV ("CONST", [ CaseV ("F32", []); f32 ]) -> F32 (al_to_float32 f32)
| CaseV ("CONST", [ CaseV ("F64", []); f64 ]) -> F64 (al_to_float64 f64)
| v -> error_value "num" v

and al_to_vec: value -> vec = function
| CaseV ("VCONST", [ CaseV ("V128", []); v128 ]) -> V128 (al_to_vec128 v128)
| v -> error_value "vec" v

and al_to_ref: value -> ref_ = function
| CaseV ("REF.NULL", [ ht ]) -> NullRef (al_to_heap_type ht)
| CaseV ("REF.HOST_ADDR", [ i32 ]) -> Script.HostRef (al_to_int32 i32)
| CaseV ("REF.I31_NUM", [ i ]) -> I31.I31Ref (al_to_int i)
| CaseV ("REF.STRUCT_ADDR", [ addr ]) ->
let struct_insts = Ds.Store.access "STRUCTS" in
let struct_ = addr |> al_to_int |> listv_nth struct_insts |> al_to_struct in
Aggr.StructRef struct_
| CaseV ("REF.ARRAY_ADDR", [ addr ]) ->
let arr_insts = Ds.Store.access "ARRAYS" in
let arr = addr |> al_to_int |> listv_nth arr_insts |> al_to_array in
Aggr.ArrayRef arr
| CaseV ("REF.EXTERN", [ r ]) -> Extern.ExternRef (al_to_ref r)
| v -> error_value "ref" v

and al_to_value: value -> Value.value = function
| CaseV ("CONST", _) as v -> Num (al_to_num v)
| CaseV (ref_, _) as v when String.sub ref_ 0 4 = "REF." -> Ref (al_to_ref v)
| CaseV ("VCONST", _) as v -> Vec (al_to_vec v)
| v -> error_value "value" v


(* Destruct operator *)

let al_to_op f1 f2 = function
Expand Down Expand Up @@ -747,6 +682,19 @@ let al_to_vlaneop: value list -> idx * vec_laneop * int = function
| vs -> error_value "vlaneop" (TupV vs)


(* Destruct expressions *)

let al_to_num: value -> num = function
| CaseV ("CONST", [ CaseV ("I32", []); i32 ]) -> I32 (al_to_int32 i32)
| CaseV ("CONST", [ CaseV ("I64", []); i64 ]) -> I64 (al_to_int64 i64)
| CaseV ("CONST", [ CaseV ("F32", []); f32 ]) -> F32 (al_to_float32 f32)
| CaseV ("CONST", [ CaseV ("F64", []); f64 ]) -> F64 (al_to_float64 f64)
| v -> error_value "num" v

let al_to_vec: value -> vec = function
| CaseV ("VCONST", [ CaseV ("V128", []); v128 ]) -> V128 (al_to_vec128 v128)
| v -> error_value "vec" v

let rec al_to_instr (v: value): Ast.instr = al_to_phrase al_to_instr' v
and al_to_instr': value -> Ast.instr' = function
(* wasm values *)
Expand Down Expand Up @@ -990,6 +938,73 @@ let al_to_module': value -> module_' = function
let al_to_module: value -> module_ = al_to_phrase al_to_module'


(* Destruct value *)

let rec al_to_field: value -> Aggr.field = function
| CaseV ("PACK", [pack_size; c]) ->
(* TODO: fix bug in packsize *)
let pack_size' =
match pack_size with
| CaseV ("I8", []) -> Pack.Pack8
| CaseV ("I16", []) -> Pack.Pack16
| CaseV ("I32", []) -> Pack.Pack32
| CaseV ("I64", []) -> Pack.Pack64
| v -> error_value "packsize" v
in
Aggr.PackField (pack_size', ref (al_to_int c))
| v -> Aggr.ValField (ref (al_to_value v))

and al_to_array: value -> Aggr.array = function
| StrV r when Record.mem "TYPE" r && Record.mem "FIELDS" r ->
Aggr.Array (
al_to_def_type (Record.find "TYPE" r),
al_to_list al_to_field (Record.find "FIELDS" r)
)
| v -> error_value "array" v

and al_to_struct: value -> Aggr.struct_ = function
| StrV r when Record.mem "TYPE" r && Record.mem "FIELDS" r ->
Aggr.Struct (
al_to_def_type (Record.find "TYPE" r),
al_to_list al_to_field (Record.find "FIELDS" r)
)
| v -> error_value "struct" v

and al_to_funcinst: value -> Instance.func_inst = function
| StrV r when Record.mem "TYPE" r && Record.mem "MODULE" r && Record.mem "CODE" r ->
Func.AstFunc (
al_to_def_type (Record.find "TYPE" r),
Reference_interpreter.Lib.Promise.make (), (* TODO: Fulfill the promise with module instance *)
al_to_func (Record.find "CODE" r)
)
| v -> error_value "funcinst" v

and al_to_ref: value -> ref_ = function
| CaseV ("REF.NULL", [ ht ]) -> NullRef (al_to_heap_type ht)
| CaseV ("REF.I31_NUM", [ i ]) -> I31.I31Ref (al_to_int i)
| CaseV ("REF.STRUCT_ADDR", [ addr ]) ->
let struct_insts = Ds.Store.access "STRUCTS" in
let struct_ = addr |> al_to_int |> listv_nth struct_insts |> al_to_struct in
Aggr.StructRef struct_
| CaseV ("REF.ARRAY_ADDR", [ addr ]) ->
let arr_insts = Ds.Store.access "ARRAYS" in
let arr = addr |> al_to_int |> listv_nth arr_insts |> al_to_array in
Aggr.ArrayRef arr
| CaseV ("REF.FUNC_ADDR", [ addr ]) ->
let func_insts = Ds.Store.access "FUNCS" in
let func = addr |> al_to_int |> listv_nth func_insts |> al_to_funcinst in
Instance.FuncRef func
| CaseV ("REF.HOST_ADDR", [ i32 ]) -> Script.HostRef (al_to_int32 i32)
| CaseV ("REF.EXTERN", [ r ]) -> Extern.ExternRef (al_to_ref r)
| v -> error_value "ref" v

and al_to_value: value -> Value.value = function
| CaseV ("CONST", _) as v -> Num (al_to_num v)
| CaseV (ref_, _) as v when String.sub ref_ 0 4 = "REF." -> Ref (al_to_ref v)
| CaseV ("VCONST", _) as v -> Vec (al_to_vec v)
| v -> error_value "value" v


(* Construct *)

(* Construct data structure *)
Expand Down
8 changes: 4 additions & 4 deletions spectec/src/backend-interpreter/interpreter.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,13 @@ let empty = ""
let error at msg step = raise (Exception.Error (at, msg, step))

let fail_expr expr msg =
failwith ("on expr `" ^ structured_string_of_expr expr ^ "` " ^ msg)
failwith ("on expr `" ^ string_of_expr expr ^ "` " ^ msg)

let fail_path path msg =
failwith ("on path `" ^ structured_string_of_path path ^ "` " ^ msg)
failwith ("on path `" ^ string_of_path path ^ "` " ^ msg)

let try_with_error fname at stringifier f step =
let prefix = if fname <> empty then fname ^ ": " else fname in
let prefix = if fname <> empty then "$" ^ fname ^ ": " else fname in
try f step with
| Construct.InvalidConversion msg
| Exception.InvalidArg msg
Expand Down Expand Up @@ -608,7 +608,7 @@ and step_instr (fname: string) (ctx: AlContext.t) (env: value Env.t) (instr: ins
| _ -> failwith "cannot step instr"

and try_step_instr fname ctx env instr =
try_with_error fname instr.at structured_string_of_instr (step_instr fname ctx env) instr
try_with_error fname instr.at string_of_instr (step_instr fname ctx env) instr

and step_wasm (ctx: AlContext.t) : value -> AlContext.t = function
(* TODO: Change ref.null semantics *)
Expand Down
2 changes: 1 addition & 1 deletion spectec/src/il2al/translate.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -933,7 +933,7 @@ let translate_helper_body name clause =
if is_config exp then
get_config_return_instrs name exp clause.at
else
[ returnI (Some (translate_exp exp)) ]
[ returnI (Some (translate_exp exp)) ~at:exp.at ]
in
translate_prems prems return_instrs

Expand Down

0 comments on commit dc06cca

Please sign in to comment.