From 4a6feb7b93835f92b31ede2684c1d3fcca9f50b8 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Mon, 24 Feb 2025 17:27:13 +0100 Subject: [PATCH] proper error on unknown identifiers when rewriting text2binary --- src/bin/owi.ml | 1 + src/text_to_binary/assigned.ml | 21 +++ src/text_to_binary/assigned.mli | 14 ++ src/text_to_binary/rewrite.ml | 266 +++++++++++++++----------------- src/utils/result.ml | 2 + src/utils/result.mli | 1 + test/validate/dune | 2 +- test/validate/unknown.t | 6 + test/validate/unknown_func.wat | 4 + test/validate/unknown_label.t | 3 - 10 files changed, 172 insertions(+), 148 deletions(-) create mode 100644 test/validate/unknown.t create mode 100644 test/validate/unknown_func.wat delete mode 100644 test/validate/unknown_label.t diff --git a/src/bin/owi.ml b/src/bin/owi.ml index 16ea9ce6e..0dcfb6b11 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -613,6 +613,7 @@ let exit_code = | `Unclosed_string -> 76 | `Unbounded_quantification -> 77 | `Invalid_model _msg -> 78 + | `Unknown_export _id -> 79 end end | Error e -> ( diff --git a/src/text_to_binary/assigned.ml b/src/text_to_binary/assigned.ml index 5a8885e26..64d8a5fe2 100644 --- a/src/text_to_binary/assigned.ml +++ b/src/text_to_binary/assigned.ml @@ -174,3 +174,24 @@ let of_grouped (modul : Grouped.t) : t Result.t = ; start = modul.start ; annots = modul.annots } + +let find (named : 'a Named.t) err : _ -> binary indice Result.t = function + | Raw _i as indice -> Ok indice + | Text name -> ( + match String_map.find_opt name named.named with + | None -> Error err + | Some i -> Ok (Raw i) ) + +let find_func modul id = find modul.func (`Unknown_func id) id + +let find_global modul id = find modul.global (`Unknown_global id) id + +let find_memory modul id = find modul.mem (`Unknown_memory id) id + +let find_table modul id = find modul.table (`Unknown_table id) id + +let find_data modul id = find modul.data (`Unknown_data id) id + +let find_elem modul id = find modul.elem (`Unknown_elem id) id + +let find_type modul id = find modul.typ (`Unknown_type id) id diff --git a/src/text_to_binary/assigned.mli b/src/text_to_binary/assigned.mli index f1e5769ba..7fa89a0ab 100644 --- a/src/text_to_binary/assigned.mli +++ b/src/text_to_binary/assigned.mli @@ -19,3 +19,17 @@ type t = } val of_grouped : Grouped.t -> t Result.t + +val find_func : t -> text indice -> binary indice Result.t + +val find_global : t -> text indice -> binary indice Result.t + +val find_memory : t -> text indice -> binary indice Result.t + +val find_data : t -> text indice -> binary indice Result.t + +val find_table : t -> text indice -> binary indice Result.t + +val find_elem : t -> text indice -> binary indice Result.t + +val find_type : t -> text indice -> binary indice Result.t diff --git a/src/text_to_binary/rewrite.ml b/src/text_to_binary/rewrite.ml index 373156a28..082087ff3 100644 --- a/src/text_to_binary/rewrite.ml +++ b/src/text_to_binary/rewrite.ml @@ -18,35 +18,21 @@ let typemap (types : binary str_type Named.t) = (fun idx typ acc -> TypeMap.add typ (Raw idx) acc) types TypeMap.empty -let find (named : 'a Named.t) : _ -> binary indice = function - | Raw _i as indice -> indice - | Text name -> ( - match String_map.find_opt name named.named with - | None -> assert false - | Some i -> Raw i ) - -let get error (named : 'a Named.t) indice : 'a Indexed.t Result.t = - let (Raw i) = find named indice in - (* TODO change Named.t structure to make that sensible *) - match List.nth_opt named.values i with - | None -> Error error - | Some v -> Ok v - -let find_global (modul : Assigned.t) id : binary indice = find modul.global id - -let find_memory (modul : Assigned.t) id : binary indice = find modul.mem id - let rewrite_block_type (typemap : binary indice TypeMap.t) (modul : Assigned.t) (block_type : text block_type) : binary block_type Result.t = match block_type with | Bt_ind id -> begin - let+ v = get (`Unknown_type id) modul.typ id in - match Indexed.get v with - | Def_func_t t' -> - let idx = Indexed.get_index v in - Bt_raw (Some (Raw idx), t') - | _ -> assert false - end + let* (Raw v) = Assigned.find_type modul id in + match List.nth_opt modul.typ.values v with + | None -> Error (`Unknown_type id) + | Some v -> begin + match Indexed.get v with + | Def_func_t t' -> + let idx = Indexed.get_index v in + Ok (Bt_raw (Some (Raw idx), t')) + | _ -> assert false + end + end | Bt_raw (_, func_type) -> let+ t = Binary_types.convert_func_type None func_type in let idx = @@ -63,14 +49,14 @@ let rewrite_expr (typemap : binary indice TypeMap.t) (modul : Assigned.t) let* id = match id with | Text id -> begin - match - List.find_index - (function Some id' -> String.equal id id' | None -> false) - block_ids - with - | None -> Error (`Unknown_label (Text id)) - | Some id -> Ok id - end + match + List.find_index + (function Some id' -> String.equal id id' | None -> false) + block_ids + with + | None -> Error (`Unknown_label (Text id)) + | Some id -> Ok id + end | Raw id -> Ok id in (* this is > and not >= because you can `br 0` without any block to target the function *) @@ -90,28 +76,22 @@ let rewrite_expr (typemap : binary indice TypeMap.t) (modul : Assigned.t) let* locals, _after_last_assigned_local = list_fold_left (fun (locals, next_free_int) ((name, _type) : binary param) -> - match name with - | None -> Ok (locals, next_free_int + 1) - | Some name -> - if String_map.mem name locals then Error (`Duplicate_local name) - else Ok (String_map.add name next_free_int locals, next_free_int + 1) ) + match name with + | None -> Ok (locals, next_free_int + 1) + | Some name -> + if String_map.mem name locals then Error (`Duplicate_local name) + else Ok (String_map.add name next_free_int locals, next_free_int + 1) ) (String_map.empty, 0) locals in let find_local = function | Raw _i as id -> id | Text name -> ( - match String_map.find_opt name locals with - | None -> assert false - | Some id -> Raw id ) + match String_map.find_opt name locals with + | None -> assert false + | Some id -> Raw id ) in - let find_table id = find modul.table id in - let find_func id = find modul.func id in - let find_data id = find modul.data id in - let find_elem id = find modul.elem id in - let find_type id = find modul.typ id in - let rec body (loop_count, block_ids) : text instr -> binary instr Result.t = function | Br_table (ids, id) -> @@ -126,11 +106,11 @@ let rewrite_expr (typemap : binary indice TypeMap.t) (modul : Assigned.t) let+ id = block_id_to_raw (loop_count, block_ids) id in Br id | Call id -> - let id = find_func id in - Ok (Call id) + let+ id = Assigned.find_func modul id in + Call id | Return_call id -> - let id = find_func id in - Ok (Return_call id) + let+ id = Assigned.find_func modul id in + Return_call id | Local_set id -> let id = find_local id in Ok (Local_set id) @@ -155,92 +135,92 @@ let rewrite_expr (typemap : binary indice TypeMap.t) (modul : Assigned.t) let+ e = expr e (loop_count, id :: block_ids) in Block (id, bt, e) | Call_indirect (tbl_i, bt) -> - let tbl_i = find_table tbl_i in + let* tbl_i = Assigned.find_table modul tbl_i in let+ bt = rewrite_block_type typemap modul bt in Call_indirect (tbl_i, bt) | Return_call_indirect (tbl_i, bt) -> - let tbl_i = find_table tbl_i in + let* tbl_i = Assigned.find_table modul tbl_i in let+ bt = rewrite_block_type typemap modul bt in Return_call_indirect (tbl_i, bt) | Call_ref t -> - let t = find_type t in - Ok (Call_ref t) + let+ t = Assigned.find_type modul t in + Call_ref t | Return_call_ref bt -> let+ bt = rewrite_block_type typemap modul bt in Return_call_ref bt | Global_set id -> - let idx = find_global modul id in - Ok (Global_set idx) + let+ idx = Assigned.find_global modul id in + Global_set idx | Global_get id -> - let idx = find_global modul id in - Ok (Global_get idx) + let+ idx = Assigned.find_global modul id in + Global_get idx | Ref_func id -> - let id = find_func id in - Ok (Ref_func id) + let+ id = Assigned.find_func modul id in + Ref_func id | Table_size id -> - let id = find_table id in - Ok (Table_size id) + let+ id = Assigned.find_table modul id in + Table_size id | Table_get id -> - let id = find_table id in - Ok (Table_get id) + let+ id = Assigned.find_table modul id in + Table_get id | Table_set id -> - let id = find_table id in - Ok (Table_set id) + let+ id = Assigned.find_table modul id in + Table_set id | Table_grow id -> - let id = find_table id in - Ok (Table_grow id) + let+ id = Assigned.find_table modul id in + Table_grow id | Table_init (i, i') -> - let table = find_table i in - let elem = find_elem i' in - Ok (Table_init (table, elem)) + let* table = Assigned.find_table modul i in + let+ elem = Assigned.find_elem modul i' in + Table_init (table, elem) | Table_fill id -> - let id = find_table id in - Ok (Table_fill id) + let+ id = Assigned.find_table modul id in + Table_fill id | Table_copy (i, i') -> - let table = find_table i in - let table' = find_table i' in - Ok (Table_copy (table, table')) + let* table = Assigned.find_table modul i in + let+ table' = Assigned.find_table modul i' in + Table_copy (table, table') | Memory_init id -> - let id = find_data id in - Ok (Memory_init id) + let+ id = Assigned.find_data modul id in + Memory_init id | Data_drop id -> - let id = find_data id in - Ok (Data_drop id) + let+ id = Assigned.find_data modul id in + Data_drop id | Elem_drop id -> - let id = find_elem id in - Ok (Elem_drop id) + let+ id = Assigned.find_elem modul id in + Elem_drop id | Select typ -> begin - match typ with - | None -> Ok (Select None) - | Some [ t ] -> - let+ t = Binary_types.convert_val_type None t in - Select (Some [ t ]) - | Some [] | Some (_ :: _ :: _) -> Error `Invalid_result_arity - end + match typ with + | None -> Ok (Select None) + | Some [ t ] -> + let+ t = Binary_types.convert_val_type None t in + Select (Some [ t ]) + | Some [] | Some (_ :: _ :: _) -> Error `Invalid_result_arity + end | Array_new_default id -> - let id = find_type id in - Ok (Array_new_default id) + let+ id = Assigned.find_type modul id in + Array_new_default id | Array_set id -> - let id = find_type id in - Ok (Array_set id) + let+ id = Assigned.find_type modul id in + Array_set id | Array_get id -> - let id = find_type id in - Ok (Array_set id) + let+ id = Assigned.find_type modul id in + Array_set id | Ref_null heap_type -> let+ t = Binary_types.convert_heap_type None heap_type in Ref_null t | Br_on_cast (i, t1, t2) -> - let i = find_type i in + let* i = Assigned.find_type modul i in let* t1 = Binary_types.convert_ref_type None t1 in let+ t2 = Binary_types.convert_ref_type None t2 in Br_on_cast (i, t1, t2) | Br_on_cast_fail (i, null, ht) -> - let i = find_type i in + let* i = Assigned.find_type modul i in let+ ht = Binary_types.convert_heap_type None ht in Br_on_cast_fail (i, null, ht) | Struct_new_default i -> - let i = find_type i in - Ok (Struct_new_default i) + let+ i = Assigned.find_type modul i in + Struct_new_default i | Ref_cast (null, ht) -> let+ ht = Binary_types.convert_heap_type None ht in Ref_cast (null, ht) @@ -284,7 +264,7 @@ let rewrite_elem (typemap : binary indice TypeMap.t) (modul : Assigned.t) | Elem_passive -> Ok Elem_passive | Elem_active (None, _expr) -> assert false | Elem_active (Some id, expr) -> - let (Raw indice) = find modul.table id in + let* (Raw indice) = Assigned.find_table modul id in let+ expr = rewrite_expr typemap modul [] expr in Binary.Elem_active (Some indice, expr) in @@ -299,26 +279,34 @@ let rewrite_data (typemap : binary indice TypeMap.t) (modul : Assigned.t) | Data_passive -> Ok Binary.Data_passive | Data_active (None, _expr) -> assert false | Data_active (Some indice, expr) -> - let (Raw indice) = find_memory modul indice in + let* (Raw indice) = Assigned.find_memory modul indice in let+ expr = rewrite_expr typemap modul [] expr in Binary.Data_active (indice, expr) in { Binary.mode; id = data.id; init = data.init } let rewrite_export named (exports : Grouped.opt_export list) : - Binary.export list = - List.map + Binary.export list Result.t = + list_map (fun { Grouped.name; id } -> - let (Raw id) = find named id in - { Binary.name; id } ) + let+ (Raw id) : binary indice = + match id with + | Raw _i as indice -> Ok indice + | Text name -> ( + match String_map.find_opt name named.Named.named with + | None -> Error (`Unknown_export id) + | Some i -> Ok (Raw i) ) + in + + { Binary.name; id } ) exports let rewrite_exports (modul : Assigned.t) (exports : Grouped.opt_exports) : - Binary.exports = - let global = rewrite_export modul.global exports.global in - let mem = rewrite_export modul.mem exports.mem in - let table = rewrite_export modul.table exports.table in - let func = rewrite_export modul.func exports.func in + Binary.exports Result.t = + let* global = rewrite_export modul.global exports.global in + let* mem = rewrite_export modul.mem exports.mem in + let* table = rewrite_export modul.table exports.table in + let+ func = rewrite_export modul.func exports.func in { Binary.global; mem; table; func } let rewrite_func (typemap : binary indice TypeMap.t) (modul : Assigned.t) @@ -348,10 +336,10 @@ let rewrite_named f named = let+ values = list_map (fun ind -> - let index = Indexed.get_index ind in - let value = Indexed.get ind in - let+ value = f value in - Indexed.return index value ) + let index = Indexed.get_index ind in + let value = Indexed.get ind in + let+ value = f value in + Indexed.return index value ) named.Named.values in { named with Named.values } @@ -387,16 +375,6 @@ let rec rewrite_term ~(binder_list : string option list) ~(modul : Assigned.t) | Text id -> find_raw_indice (`Spec_unknown_param ind) 0 id func_param_list in - let find_global (modul : Assigned.t) (ind : text indice) : - binary indice Result.t = - match ind with - | Raw id -> Ok (Raw id) - | Text id -> ( - match String_map.find_opt id modul.global.named with - | None -> Error (`Unknown_global ind) - | Some i -> Ok (Raw i) ) - in - let open Spec in function | Int32 i32 -> Ok (Int32 i32) @@ -404,20 +382,20 @@ let rec rewrite_term ~(binder_list : string option list) ~(modul : Assigned.t) | Float32 f32 -> Ok (Float32 f32) | Float64 f64 -> Ok (Float64 f64) | Var ind -> ( - match - ( find_binder binder_list ind - , find_param func_param_list ind - , find_global modul ind ) - with - | Ok ind, _, _ -> Ok (BinderVar ind) - | _, Ok ind, _ -> Ok (ParamVar ind) - | _, _, Ok ind -> Ok (GlobalVar ind) - | _, _, _ -> Error (`Spec_unknown_variable ind) ) + match + ( find_binder binder_list ind + , find_param func_param_list ind + , Assigned.find_global modul ind ) + with + | Ok ind, _, _ -> Ok (BinderVar ind) + | _, Ok ind, _ -> Ok (ParamVar ind) + | _, _, Ok ind -> Ok (GlobalVar ind) + | _, _, _ -> Error (`Spec_unknown_variable ind) ) | ParamVar ind -> let+ ind = find_param func_param_list ind in ParamVar ind | GlobalVar ind -> - let+ ind = find_global modul ind in + let+ ind = Assigned.find_global modul ind in GlobalVar ind | BinderVar ind -> let+ ind = find_binder binder_list ind in @@ -458,8 +436,8 @@ let rec rewrite_prop ~(binder_list : string option list) ~(modul : Assigned.t) let rewrite_contract (modul : Assigned.t) : text Contract.t -> binary Contract.t Result.t = - fun { Contract.funcid; preconditions; postconditions } -> - let funcid = find modul.func funcid in + fun { Contract.funcid; preconditions; postconditions } -> + let* funcid = Assigned.find_func modul funcid in let* func = let (Raw i) = funcid in match Indexed.get_at i modul.func.values with @@ -474,10 +452,10 @@ let rewrite_contract (modul : Assigned.t) : let* func_param_list = match func_bt with | Bt_ind ind -> ( - let (Raw i) = find modul.typ ind in - match Indexed.get_at i modul.typ.values with - | Some (Def_func_t (func_pt, _)) -> Ok (List.map fst func_pt) - | _ -> Error (`Spec_invalid_indice (Int.to_string i)) ) + let* (Raw i) = Assigned.find_type modul ind in + match Indexed.get_at i modul.typ.values with + | Some (Def_func_t (func_pt, _)) -> Ok (List.map fst func_pt) + | _ -> Error (`Spec_invalid_indice (Int.to_string i)) ) | Bt_raw (_, (func_pt, _)) -> Ok (List.map fst func_pt) in let* preconditions = @@ -517,7 +495,7 @@ let modul (modul : Assigned.t) : Binary.modul Result.t = in let* elem = rewrite_named (rewrite_elem typemap modul) modul.elem in let* data = rewrite_named (rewrite_data typemap modul) modul.data in - let exports = rewrite_exports modul modul.exports in + let* exports = rewrite_exports modul modul.exports in let* func = let import = rewrite_import (rewrite_block_type typemap modul) in let runtime = rewrite_runtime (rewrite_func typemap modul) import in @@ -528,8 +506,8 @@ let modul (modul : Assigned.t) : Binary.modul Result.t = match modul.start with | None -> Ok None | Some id -> - let (Raw id) = find func id in - Ok (Some id) + let+ (Raw id) = Assigned.find_func modul id in + Some id in let+ custom = rewrite_annots modul modul.annots in diff --git a/src/utils/result.ml b/src/utils/result.ml index 7064a0bb9..8967aa450 100644 --- a/src/utils/result.ml +++ b/src/utils/result.ml @@ -55,6 +55,7 @@ type err = | `Unknown_label of Types.text Types.indice | `Unknown_local of Types.text Types.indice | `Unknown_memory of Types.text Types.indice + | `Unknown_export of Types.text Types.indice | `Unknown_module of string | `Unknown_operator | `Unknown_table of Types.text Types.indice @@ -143,6 +144,7 @@ let rec err_to_string = function | `Unknown_label id -> Fmt.str "unknown label %a" Types.pp_indice id | `Unknown_local id -> Fmt.str "unknown local %a" Types.pp_indice id | `Unknown_memory id -> Fmt.str "unknown memory %a" Types.pp_indice id + | `Unknown_export id -> Fmt.str "unknown export %a" Types.pp_indice id | `Unknown_module name -> Fmt.str "unknown module %s" name | `Unknown_operator -> Fmt.str "unknown operator" | `Unknown_table id -> Fmt.str "unknown table %a" Types.pp_indice id diff --git a/src/utils/result.mli b/src/utils/result.mli index 1536ab8dc..458c44bf0 100644 --- a/src/utils/result.mli +++ b/src/utils/result.mli @@ -55,6 +55,7 @@ type err = | `Unknown_label of Types.text Types.indice | `Unknown_local of Types.text Types.indice | `Unknown_memory of Types.text Types.indice + | `Unknown_export of Types.text Types.indice | `Unknown_module of string | `Unknown_operator | `Unknown_table of Types.text Types.indice diff --git a/test/validate/dune b/test/validate/dune index b356a90fb..4f77645e6 100644 --- a/test/validate/dune +++ b/test/validate/dune @@ -1,2 +1,2 @@ (cram - (deps %{bin:owi} unknown_label.wat)) + (deps %{bin:owi} ./unknown_label.wat ./unknown_func.wat)) diff --git a/test/validate/unknown.t b/test/validate/unknown.t new file mode 100644 index 000000000..9f4893ae5 --- /dev/null +++ b/test/validate/unknown.t @@ -0,0 +1,6 @@ + $ owi validate ./unknown_label.wat + unknown label 2 + [46] + $ owi validate ./unknown_func.wat + unknown function $g + [43] diff --git a/test/validate/unknown_func.wat b/test/validate/unknown_func.wat new file mode 100644 index 000000000..c19ab8f15 --- /dev/null +++ b/test/validate/unknown_func.wat @@ -0,0 +1,4 @@ +(module + (func $f + call $g + )) diff --git a/test/validate/unknown_label.t b/test/validate/unknown_label.t deleted file mode 100644 index d6e54899c..000000000 --- a/test/validate/unknown_label.t +++ /dev/null @@ -1,3 +0,0 @@ - $ owi validate ./unknown_label.wat - unknown label 2 - [46]