From 5e75ccaa9ec43fab8b71c837477e6a0a7a6a89a3 Mon Sep 17 00:00:00 2001 From: Zhicheng HUI Date: Mon, 19 Aug 2024 01:30:04 +0200 Subject: [PATCH] framework for rac code generation --- src/annot/contract.ml | 8 + src/annot/contract.mli | 4 + src/annot/spec.ml | 45 +-- src/annot/spec.mli | 8 +- src/ast/binary_encoder.ml | 4 +- src/ast/binary_encoder.mli | 1 + src/ast/code_generator.ml | 585 ++++++++++++++++++++++++++++++++ src/ast/code_generator.mli | 5 + src/ast/compile.ml | 80 ++--- src/ast/compile.mli | 39 ++- src/ast/types.ml | 17 +- src/bin/owi.ml | 48 +-- src/cmd/cmd_conc.ml | 17 +- src/cmd/cmd_opt.ml | 8 +- src/cmd/cmd_opt.mli | 2 +- src/cmd/cmd_run.ml | 8 +- src/cmd/cmd_run.mli | 2 +- src/cmd/cmd_script.ml | 4 +- src/cmd/cmd_script.mli | 2 +- src/cmd/cmd_sym.ml | 12 +- src/cmd/cmd_validate.ml | 8 +- src/cmd/cmd_validate.mli | 2 +- src/cmd/cmd_wat2wasm.ml | 8 +- src/cmd/cmd_wat2wasm.mli | 2 +- src/data_structures/indexed.ml | 4 + src/data_structures/indexed.mli | 2 + src/dune | 1 + src/script/script.ml | 24 +- src/script/script.mli | 7 +- src/text_to_binary/rewrite.ml | 18 +- src/utils/result.ml | 60 ++-- src/utils/result.mli | 27 +- src/utils/syntax.ml | 14 + src/utils/syntax.mli | 5 + 34 files changed, 893 insertions(+), 188 deletions(-) create mode 100644 src/ast/code_generator.ml create mode 100644 src/ast/code_generator.mli diff --git a/src/annot/contract.ml b/src/annot/contract.ml index 2cc0da56a..4c69d2ddd 100644 --- a/src/annot/contract.ml +++ b/src/annot/contract.ml @@ -13,6 +13,14 @@ type 'a t = ; postconditions : 'a prop list } +let compare_funcid c1 c2 = compare_indice c1.funcid c2.funcid + +let join_contract { preconditions = pre1; postconditions = post1; funcid } + { preconditions = pre2; postconditions = post2; _ } = + let preconditions = pre1 @ pre2 in + let postconditions = post1 @ post2 in + { funcid; preconditions; postconditions } + let pp_contract fmt { funcid; preconditions; postconditions } = pf fmt "@[Contract of function %a@,\ diff --git a/src/annot/contract.mli b/src/annot/contract.mli index cd55c5acb..2cce4e16a 100644 --- a/src/annot/contract.mli +++ b/src/annot/contract.mli @@ -12,6 +12,10 @@ type 'a t = ; postconditions : 'a prop list } +val compare_funcid : 'a t -> 'a t -> int + +val join_contract : 'a t -> 'a t -> 'a t + val pp_contract : formatter -> 'a t -> unit val parse_contract : Sexp.t -> text t Result.t diff --git a/src/annot/spec.ml b/src/annot/spec.ml index 947a653f0..ee299956a 100644 --- a/src/annot/spec.ml +++ b/src/annot/spec.ml @@ -18,17 +18,18 @@ binop ::= '+' ==> Plus term ::= '(' pterm ')' ==> pterm | i32 ==> match Int32.of_string i32 with Some i32 -> Int32 i32 | ind ==> match parse_text_id ind with Some ind -> Var (Text ind) - | result ==> Result + | 'result' ==> Result None -pterm ::= 'i32' i32 ==> match Int32.of_string i32 with Some i32 -> Int32 i32 | None -> `Invalid_int32 i32 - | 'i64' i64 ==> match Int64.of_string i64 with Some i64 -> Int64 i64 | None -> `Invalid_int64 i64 - | 'f32' f32 ==> match Float32.of_string f32 with Some f32 -> Float32 f32 | None -> `Invalid_float32 f32 - | 'f64' f64 ==> match Float64.of_string f64 with Some f64 -> Float64 f64 | None -> `Invalid_float64 f64 +pterm ::= 'i32' i32 ==> match Int32.of_string i32 with Some i32 -> Int32 i32 | None -> `Spec_invalid_int32 i32 + | 'i64' i64 ==> match Int64.of_string i64 with Some i64 -> Int64 i64 | None -> `Spec_invalid_int64 i64 + | 'f32' f32 ==> match Float32.of_string f32 with Some f32 -> Float32 f32 | None -> `Spec_invalid_float32 f32 + | 'f64' f64 ==> match Float64.of_string f64 with Some f64 -> Float64 f64 | None -> `Spec_invalid_float64 f64 | 'param' ind ==> let* ind = parse_indice ind in ParamVar ind | 'global' ind ==> let* ind = parse_indice ind in GlobalVar ind | 'binder' ind ==> let* ind = parse_indice ind in BinderVar ind | unop term_1 ==> Unop (unop, term_1) | binop term_1 term_2 ==> BinOp (binop, term_1, term_2) + | 'result' i ==> Result (Some i) binpred ::= '>=' ==> Ge | '>' ==> Gt @@ -109,7 +110,7 @@ type 'a term = | BinderVar : 'a indice -> 'a term | UnOp : unop * 'a term -> 'a term | BinOp : binop * 'a term * 'a term -> 'a term - | Result : 'a term + | Result : int option -> 'a term type 'a prop = | Const : bool -> 'a prop @@ -162,7 +163,8 @@ let rec pp_term : type a. formatter -> a term -> unit = | UnOp (u, tm1) -> pf fmt "@[(%a@ %a)@]" pp_unop u pp_term tm1 | BinOp (b, tm1, tm2) -> pf fmt "@[(%a@ %a@ %a)@]" pp_binop b pp_term tm1 pp_term tm2 - | Result -> pf fmt "result" + | Result (Some i) -> pf fmt "(result %i)" i + | Result None -> pf fmt "result" let rec pp_prop : type a. formatter -> a prop -> unit = fun fmt -> function @@ -205,8 +207,8 @@ let parse_text_id_result id = let hd = String.get id 0 in let tl = String.sub id 1 (len - 1) in if Char.equal hd '$' && String.for_all valid_text_indice_char id then Ok tl - else Error (`Invalid_text_indice id) - else Error (`Invalid_text_indice id) + else Error (`Spec_invalid_text_indice id) + else Error (`Spec_invalid_text_indice id) let parse_raw_id id = int_of_string id @@ -214,7 +216,7 @@ let parse_indice id = match (parse_text_id id, parse_raw_id id) with | Some id, _ -> Ok (Text id) | _, Some id -> Ok (Raw id) - | _, _ -> Error (`Invalid_indice id) + | _, _ -> Error (`Spec_invalid_indice id) let parse_binder_type = let open Sexp in @@ -223,7 +225,7 @@ let parse_binder_type = | Atom "i64" -> Ok I64 | Atom "f32" -> Ok F32 | Atom "f64" -> Ok F64 - | bt -> Error (`Unknown_binder_type bt) + | bt -> Error (`Spec_unknown_binder_type bt) let rec parse_term = let open Sexp in @@ -238,29 +240,34 @@ let rec parse_term = | Some ind -> Ok (Var (Text ind)) | None -> (* Result *) - if String.equal "result" a then Ok Result (* Invalid *) - else Error (`Unknown_term tm) ) + if String.equal "result" a then Ok (Result None) (* Invalid *) + else Error (`Spec_unknown_term tm) ) end + (* Result *) + | List [ Atom "result"; Atom i ] -> ( + match int_of_string i with + | Some i -> Ok (Result (Some i)) + | None -> Error (`Spec_invalid_int32 i) ) (* Int32 *) | List [ Atom "i32"; Atom i32 ] -> ( match Int32.of_string i32 with | Some i32 -> ok @@ Int32 i32 - | None -> Error (`Invalid_int32 i32) ) + | None -> Error (`Spec_invalid_int32 i32) ) (* Int64 *) | List [ Atom "i64"; Atom i64 ] -> ( match Int64.of_string i64 with | Some i64 -> ok @@ Int64 i64 - | None -> Error (`Invalid_int64 i64) ) + | None -> Error (`Spec_invalid_int64 i64) ) (* Float32 *) | List [ Atom "f32"; Atom f32 ] -> ( match Float32.of_string f32 with | Some f32 -> ok @@ Float32 f32 - | None -> Error (`Invalid_float32 f32) ) + | None -> Error (`Spec_invalid_float32 f32) ) (* Float64 *) | List [ Atom "f64"; Atom f64 ] -> ( match Float64.of_string f64 with | Some f64 -> ok @@ Float64 f64 - | None -> Error (`Invalid_float64 f64) ) + | None -> Error (`Spec_invalid_float64 f64) ) (* ParamVar *) | List [ Atom "param"; Atom ind ] -> let+ ind = parse_indice ind in @@ -302,7 +309,7 @@ let rec parse_term = let+ tm2 = parse_term tm2 in BinOp (CustomBinOp c, tm1, tm2) (* Invalid *) - | tm -> Error (`Unknown_term tm) + | tm -> Error (`Spec_unknown_term tm) let rec parse_prop = let open Sexp in @@ -376,4 +383,4 @@ let rec parse_prop = let+ pr1 = parse_prop pr1 in Binder (Exists, bt, Some ind, pr1) (* invalid *) - | _ as pr -> Error (`Unknown_prop pr) + | _ as pr -> Error (`Spec_unknown_prop pr) diff --git a/src/annot/spec.mli b/src/annot/spec.mli index a0fc1a0e0..0cac60a82 100644 --- a/src/annot/spec.mli +++ b/src/annot/spec.mli @@ -49,7 +49,7 @@ type 'a term = | BinderVar : 'a indice -> 'a term | UnOp : unop * 'a term -> 'a term | BinOp : binop * 'a term * 'a term -> 'a term - | Result : 'a term + | Result : int option -> 'a term type 'a prop = | Const : bool -> 'a prop @@ -68,10 +68,14 @@ val pp_binder : formatter -> binder -> unit val pp_binder_type : formatter -> binder_type -> unit -val pp_prop : formatter -> 'a prop -> unit +val pp_unop : formatter -> unop -> unit + +val pp_binop : formatter -> binop -> unit val pp_term : formatter -> 'a term -> unit +val pp_prop : formatter -> 'a prop -> unit + val parse_indice : string -> text indice Result.t val parse_prop : Sexp.t -> text prop Result.t diff --git a/src/ast/binary_encoder.ml b/src/ast/binary_encoder.ml index 394d6e577..d67deba65 100644 --- a/src/ast/binary_encoder.ml +++ b/src/ast/binary_encoder.ml @@ -778,8 +778,8 @@ let write_file filename content = Out_channel.output_string oc content; Out_channel.close oc -let convert (filename : Fpath.t) ~unsafe ~optimize m = +let convert (filename : Fpath.t) ~unsafe ~rac ~optimize m = Log.debug0 "bin encoding ...@\n"; - let+ m = Compile.Text.until_optimize ~unsafe ~optimize m in + let+ m = Compile.Text.until_optimize ~unsafe ~rac ~optimize m in let content = encode m in write_file filename content diff --git a/src/ast/binary_encoder.mli b/src/ast/binary_encoder.mli index d1481b2c5..43af12e3e 100644 --- a/src/ast/binary_encoder.mli +++ b/src/ast/binary_encoder.mli @@ -5,6 +5,7 @@ val convert : Fpath.t -> unsafe:bool + -> rac:bool -> optimize:bool -> Text.modul -> (unit, Result.err) result diff --git a/src/ast/code_generator.ml b/src/ast/code_generator.ml new file mode 100644 index 000000000..5dc5e34c5 --- /dev/null +++ b/src/ast/code_generator.ml @@ -0,0 +1,585 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +open Types +open Binary +open Spec +open Syntax + +let type_env (m : modul) (func_ty : binary param_type * binary result_type) + (owi_funcs : (string * int) list) = + object + val param_types : binary val_type list = List.map snd (fst func_ty) + + val global_types : binary val_type list = + let sorted_global_types = + List.sort + (fun x y -> compare (Indexed.get_index x) (Indexed.get_index y)) + m.global.values + in + List.map + (fun (x : (global, binary global_type) Runtime.t Indexed.t) -> + match Indexed.get x with + | Runtime.Local { typ = _, gt; _ } -> gt + | Runtime.Imported { desc = _, gt; _ } -> gt ) + sorted_global_types + + val result_types : binary val_type list = snd func_ty + + val param_number : int = List.length (fst func_ty) + + val result_number : int = List.length (snd func_ty) + + val owi_i32 : int = List.assoc "i32_symbol" owi_funcs + + val owi_i64 : int = List.assoc "i64_symbol" owi_funcs + + val owi_f32 : int = List.assoc "f32_symbol" owi_funcs + + val owi_f64 : int = List.assoc "f64_symbol" owi_funcs + + val owi_assume : int = List.assoc "assume" owi_funcs + + val owi_assert : int = List.assoc "assert" owi_funcs + + method get_param_type (Raw i : binary indice) : binary val_type option = + List.nth_opt param_types i + + method get_global_type (Raw i : binary indice) : binary val_type option = + List.nth_opt global_types i + + method get_result_type (i : int) : binary val_type option = + List.nth_opt result_types i + + method get_param_number : int = param_number + + method get_result_number : int = result_number + + method get_result_types : binary val_type list = result_types + + method get_owi_i32 : int = owi_i32 + + method get_owi_i64 : int = owi_i64 + + method get_owi_f32 : int = owi_f32 + + method get_owi_f64 : int = owi_f64 + + method get_owi_assume : int = owi_assume + + method get_owi_assert : int = owi_assert + end + +let prop_true = I32_const (Int32.of_int 1) + +let prop_false = I32_const (Int32.of_int 0) + +let unop_generate (u : unop) (expr1 : binary expr) (ty1 : binary val_type) : + (binary expr * binary val_type) Result.t = + match u with + | Neg -> ( + match ty1 with + | Num_type I32 -> + let expr = + (I32_const (Int32.of_int 0) :: expr1) @ [ I_binop (S32, Sub) ] + in + Ok (expr, Num_type I32) + | Num_type I64 -> + let expr = + (I64_const (Int64.of_int 0) :: expr1) @ [ I_binop (S64, Sub) ] + in + Ok (expr, Num_type I64) + | Num_type F32 -> + let expr = + (F32_const (Float32.of_float 0.) :: expr1) @ [ F_binop (S32, Sub) ] + in + Ok (expr, Num_type F32) + | Num_type F64 -> + let expr = + (F64_const (Float64.of_float 0.) :: expr1) @ [ F_binop (S64, Sub) ] + in + Ok (expr, Num_type F64) + | Ref_type _ -> Error (`Spec_type_error Fmt.(str "%a" pp_unop u)) ) + | CustomUnOp _ -> Error (`Spec_type_error Fmt.(str "%a" pp_unop u)) + +let binop_generate (b : binop) (expr1 : binary expr) (ty1 : binary val_type) + (expr2 : binary expr) (ty2 : binary val_type) : + (binary expr * binary val_type) Result.t = + match b with + | Plus -> ( + match (ty1, ty2) with + | Num_type I32, Num_type I32 -> + let expr = expr1 @ expr2 @ [ I_binop (S32, Add) ] in + Ok (expr, Num_type I32) + | Num_type I64, Num_type I64 -> + let expr = expr1 @ expr2 @ [ I_binop (S64, Add) ] in + Ok (expr, Num_type I64) + | Num_type F32, Num_type F32 -> + let expr = expr1 @ expr2 @ [ F_binop (S32, Add) ] in + Ok (expr, Num_type F32) + | Num_type F64, Num_type F64 -> + let expr = expr1 @ expr2 @ [ F_binop (S64, Add) ] in + Ok (expr, Num_type F64) + | _, _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binop b)) ) + | Minus -> ( + match (ty1, ty2) with + | Num_type I32, Num_type I32 -> + let expr = expr1 @ expr2 @ [ I_binop (S32, Sub) ] in + Ok (expr, Num_type I32) + | Num_type I64, Num_type I64 -> + let expr = expr1 @ expr2 @ [ I_binop (S64, Sub) ] in + Ok (expr, Num_type I64) + | Num_type F32, Num_type F32 -> + let expr = expr1 @ expr2 @ [ F_binop (S32, Sub) ] in + Ok (expr, Num_type F32) + | Num_type F64, Num_type F64 -> + let expr = expr1 @ expr2 @ [ F_binop (S64, Sub) ] in + Ok (expr, Num_type F64) + | _, _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binop b)) ) + | Mult -> ( + match (ty1, ty2) with + | Num_type I32, Num_type I32 -> + let expr = expr1 @ expr2 @ [ I_binop (S32, Mul) ] in + Ok (expr, Num_type I32) + | Num_type I64, Num_type I64 -> + let expr = expr1 @ expr2 @ [ I_binop (S64, Mul) ] in + Ok (expr, Num_type I64) + | Num_type F32, Num_type F32 -> + let expr = expr1 @ expr2 @ [ F_binop (S32, Mul) ] in + Ok (expr, Num_type F32) + | Num_type F64, Num_type F64 -> + let expr = expr1 @ expr2 @ [ F_binop (S64, Mul) ] in + Ok (expr, Num_type F64) + | _, _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binop b)) ) + | Div -> ( + match (ty1, ty2) with + | Num_type I32, Num_type I32 -> + let expr = expr1 @ expr2 @ [ I_binop (S32, Div S) ] in + Ok (expr, Num_type I32) + | Num_type I64, Num_type I64 -> + let expr = expr1 @ expr2 @ [ I_binop (S64, Div S) ] in + Ok (expr, Num_type I64) + | Num_type F32, Num_type F32 -> + let expr = expr1 @ expr2 @ [ F_binop (S32, Div) ] in + Ok (expr, Num_type F32) + | Num_type F64, Num_type F64 -> + let expr = expr1 @ expr2 @ [ F_binop (S64, Div) ] in + Ok (expr, Num_type F64) + | _, _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binop b)) ) + | CustomBinOp _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binop b)) + +let rec term_generate tenv term : (binary expr * binary val_type) Result.t = + match term with + | Int32 i32 -> Ok ([ I32_const i32 ], Num_type I32) + | Int64 i64 -> Ok ([ I64_const i64 ], Num_type I64) + | Float32 f32 -> Ok ([ F32_const f32 ], Num_type F32) + | Float64 f64 -> Ok ([ F64_const f64 ], Num_type F64) + | ParamVar id -> ( + match tenv#get_param_type id with + | Some t -> Ok ([ Local_get id ], t) + | None -> Error (`Spec_type_error Fmt.(str "%a" pp_term term)) ) + | GlobalVar id -> ( + match tenv#get_global_type id with + | Some t -> Ok ([ Global_get id ], t) + | None -> Error (`Spec_type_error Fmt.(str "%a" pp_term term)) ) + | BinderVar _id -> Ok ([], Num_type I32) (* TODO : binder index calculation *) + | UnOp (u, tm1) -> + let* expr1, ty1 = term_generate tenv tm1 in + unop_generate u expr1 ty1 + | BinOp (b, tm1, tm2) -> + let* expr1, ty1 = term_generate tenv tm1 in + let* expr2, ty2 = term_generate tenv tm2 in + binop_generate b expr1 ty1 expr2 ty2 + | Result (Some i) -> ( + match tenv#get_result_type i with + | Some t -> Ok ([ Local_get (Raw (tenv#get_param_number + i)) ], t) + | None -> Error (`Spec_type_error Fmt.(str "%a" pp_term term)) ) + | Result None -> ( + match tenv#get_result_type 0 with + | Some t -> Ok ([ Local_get (Raw tenv#get_param_number) ], t) + | None -> Error (`Spec_type_error Fmt.(str "%a" pp_term term)) ) + +let binpred_generate (b : binpred) (expr1 : binary expr) (ty1 : binary val_type) + (expr2 : binary expr) (ty2 : binary val_type) : binary expr Result.t = + match b with + | Ge -> ( + match (ty1, ty2) with + | Num_type I32, Num_type I32 -> Ok (expr1 @ expr2 @ [ I_relop (S32, Ge S) ]) + | Num_type I64, Num_type I64 -> Ok (expr1 @ expr2 @ [ I_relop (S64, Ge S) ]) + | Num_type F32, Num_type F32 -> Ok (expr1 @ expr2 @ [ F_relop (S32, Ge) ]) + | Num_type F64, Num_type F64 -> Ok (expr1 @ expr2 @ [ F_relop (S64, Ge) ]) + | _, _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binpred b)) ) + | Gt -> ( + match (ty1, ty2) with + | Num_type I32, Num_type I32 -> Ok (expr1 @ expr2 @ [ I_relop (S32, Gt S) ]) + | Num_type I64, Num_type I64 -> Ok (expr1 @ expr2 @ [ I_relop (S64, Gt S) ]) + | Num_type F32, Num_type F32 -> Ok (expr1 @ expr2 @ [ F_relop (S32, Gt) ]) + | Num_type F64, Num_type F64 -> Ok (expr1 @ expr2 @ [ F_relop (S64, Gt) ]) + | _, _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binpred b)) ) + | Le -> ( + match (ty1, ty2) with + | Num_type I32, Num_type I32 -> Ok (expr1 @ expr2 @ [ I_relop (S32, Le S) ]) + | Num_type I64, Num_type I64 -> Ok (expr1 @ expr2 @ [ I_relop (S64, Le S) ]) + | Num_type F32, Num_type F32 -> Ok (expr1 @ expr2 @ [ F_relop (S32, Le) ]) + | Num_type F64, Num_type F64 -> Ok (expr1 @ expr2 @ [ F_relop (S64, Le) ]) + | _, _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binpred b)) ) + | Lt -> ( + match (ty1, ty2) with + | Num_type I32, Num_type I32 -> Ok (expr1 @ expr2 @ [ I_relop (S32, Lt S) ]) + | Num_type I64, Num_type I64 -> Ok (expr1 @ expr2 @ [ I_relop (S64, Lt S) ]) + | Num_type F32, Num_type F32 -> Ok (expr1 @ expr2 @ [ F_relop (S32, Lt) ]) + | Num_type F64, Num_type F64 -> Ok (expr1 @ expr2 @ [ F_relop (S64, Lt) ]) + | _, _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binpred b)) ) + | Eq -> ( + match (ty1, ty2) with + | Num_type I32, Num_type I32 -> Ok (expr1 @ expr2 @ [ I_relop (S32, Eq) ]) + | Num_type I64, Num_type I64 -> Ok (expr1 @ expr2 @ [ I_relop (S64, Eq) ]) + | Num_type F32, Num_type F32 -> Ok (expr1 @ expr2 @ [ F_relop (S32, Eq) ]) + | Num_type F64, Num_type F64 -> Ok (expr1 @ expr2 @ [ F_relop (S64, Eq) ]) + | _, _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binpred b)) ) + | Neq -> ( + match (ty1, ty2) with + | Num_type I32, Num_type I32 -> Ok (expr1 @ expr2 @ [ I_relop (S32, Ne) ]) + | Num_type I64, Num_type I64 -> Ok (expr1 @ expr2 @ [ I_relop (S64, Ne) ]) + | Num_type F32, Num_type F32 -> Ok (expr1 @ expr2 @ [ F_relop (S32, Ne) ]) + | Num_type F64, Num_type F64 -> Ok (expr1 @ expr2 @ [ F_relop (S64, Ne) ]) + | _, _ -> Error (`Spec_type_error Fmt.(str "%a" pp_binpred b)) ) + +let unconnect_generate (u : unconnect) (expr1 : binary expr) : + binary expr Result.t = + match u with Not -> Ok ((prop_true :: expr1) @ [ I_binop (S32, Xor) ]) + +let binconnect_generate (b : binconnect) (expr1 : binary expr) + (expr2 : binary expr) : binary expr Result.t = + let bt = Bt_raw (None, ([ (None, Num_type I32) ], [ Num_type I32 ])) in + match b with + | And -> Ok (expr1 @ [ If_else (None, Some bt, expr2, [ prop_false ]) ]) + | Or -> Ok (expr1 @ [ If_else (None, Some bt, [ prop_true ], expr2) ]) + | Imply -> Ok (expr1 @ [ If_else (None, Some bt, expr2, [ prop_true ]) ]) + | Equiv -> + Ok + ( expr1 + @ [ If_else + (None, Some bt, expr2, (prop_true :: expr2) @ [ I_binop (S32, Xor) ]) + ] ) + +let prop_generate tenv : binary prop -> binary expr Result.t = + let rec prop_generate_aux = function + | Const true -> Ok [ prop_true ] + | Const false -> Ok [ prop_false ] + | BinPred (b, tm1, tm2) -> + let* expr1, ty1 = term_generate tenv tm1 in + let* expr2, ty2 = term_generate tenv tm2 in + binpred_generate b expr1 ty1 expr2 ty2 + | UnConnect (u, pr1) -> + let* expr1 = prop_generate_aux pr1 in + unconnect_generate u expr1 + | BinConnect (b, pr1, pr2) -> + let* expr1 = prop_generate_aux pr1 in + let* expr2 = prop_generate_aux pr2 in + binconnect_generate b expr1 expr2 + | Binder (_b, _bt, _, _pr1) -> + (* TODO : quantification checking *) + Ok [] + in + fun pr -> + let+ expr = prop_generate_aux pr in + expr @ [ Call (Raw tenv#get_owi_assert) ] + +let subst_index ?(subst_custom = false) (old_index : int) (index : int) + (m : modul) : modul = + let subst i = if i = old_index then index else i in + let rec subst_instr (instr : binary instr) : binary instr = + match instr with + | Ref_func (Raw i) -> Ref_func (Raw (subst i)) + | Block (str_opt, bt_opt, expr1) -> Block (str_opt, bt_opt, subst_expr expr1) + | Loop (str_opt, bt_opt, expr1) -> Loop (str_opt, bt_opt, subst_expr expr1) + | If_else (str_opt, bt_opt, expr1, expr2) -> + If_else (str_opt, bt_opt, subst_expr expr1, subst_expr expr2) + | Return_call (Raw i) -> Return_call (Raw (subst i)) + | Call (Raw i) -> Call (Raw (subst i)) + | instr -> instr + and subst_expr (expr : binary expr) = List.map subst_instr expr in + + let subst_global (global : (global, binary global_type) Runtime.t) = + match global with + | Runtime.Local { typ; init; id } -> + Runtime.Local { typ; init = subst_expr init; id } + | Imported _ -> global + in + let global = + { m.global with + values = + List.map + (fun v -> Indexed.(return (get_index v) (subst_global (get v)))) + m.global.values + } + in + + let subst_func (func : (binary func, binary block_type) Runtime.t) = + match func with + | Runtime.Local { type_f; locals; body; id } -> + Runtime.Local { type_f; locals; body = subst_expr body; id } + | Imported _ -> func + in + let func = + { m.func with + values = + List.map + (fun v -> Indexed.(return (get_index v) (subst_func (get v)))) + m.func.values + } + in + + let subst_elem_mode = function + | Elem_passive -> Elem_passive + | Elem_active (int_opt, expr1) -> Elem_active (int_opt, subst_expr expr1) + | Elem_declarative -> Elem_declarative + in + let subst_elem ({ id; typ; init; mode } : elem) = + { id; typ; init = List.map subst_expr init; mode = subst_elem_mode mode } + in + let elem = + { m.elem with + values = + List.map + (fun v -> Indexed.(return (get_index v) (subst_elem (get v)))) + m.elem.values + } + in + + let subst_data_mode = function + | Data_passive -> Data_passive + | Data_active (int, expr1) -> Data_active (int, subst_expr expr1) + in + let subst_data ({ id; init; mode } : data) = + { id; init; mode = subst_data_mode mode } + in + let data = + { m.data with + values = + List.map + (fun v -> Indexed.(return (get_index v) (subst_data (get v)))) + m.data.values + } + in + + let subst_export ({ name; id } : export) = { name; id = subst id } in + let exports = + { m.exports with func = List.map subst_export m.exports.func } + in + + let start = match m.start with Some i -> Some (subst i) | None -> None in + + let subst_contract + ({ Contract.funcid = Raw i; preconditions; postconditions } : + binary Contract.t ) = + { Contract.funcid = Raw (subst i); preconditions; postconditions } + in + let custom = + if subst_custom then + List.map + (function + | From_annot (Annot.Contract c) -> + From_annot (Contract (subst_contract c)) + | _ as c -> c ) + m.custom + else m.custom + in + + { id = m.id + ; types = m.types + ; global + ; table = m.table + ; mem = m.mem + ; func + ; elem + ; data + ; exports + ; start + ; custom + } + +let contract_generate (owi_funcs : (string * int) list) (m : modul) + ({ funcid = Raw old_index; preconditions; postconditions } : binary Contract.t) + : modul Result.t = + let* old_id, Bt_raw (ty_index, old_type) = + match Indexed.get_at old_index m.func.values with + | Some (Runtime.Local { id; type_f; _ }) -> ( + match id with + | Some id -> Ok (id, type_f) + | None -> Ok (Fmt.str "func_%i" old_index, type_f) ) + | Some (Imported { modul; name; assigned_name; desc }) -> ( + match assigned_name with + | Some assigned_name -> Ok (assigned_name, desc) + | None -> Ok (Fmt.str "func_%s_%s_%i" modul name old_index, desc) ) + | None -> Error (`Contract_unknown_func (Raw old_index)) + in + let index = List.length m.func.values in + let id = Fmt.str "__rac_%s" old_id in + + let tenv = type_env m old_type owi_funcs in + + let locals = + List.mapi + (fun i rt -> (Some Fmt.(str "__rac_res_%i" i), rt)) + tenv#get_result_types + in + let call = + List.init tenv#get_param_number (fun i -> Local_get (Raw i)) + @ [ Call (Raw old_index) ] + @ List.init tenv#get_result_number (fun i -> + Local_set (Raw (tenv#get_param_number + i)) ) + in + let return = + List.init tenv#get_result_number (fun i -> + Local_get (Raw (tenv#get_param_number + i)) ) + in + let* precond_checker = list_concat_map (prop_generate tenv) preconditions in + let+ postcond_checker = list_concat_map (prop_generate tenv) postconditions in + let body = precond_checker @ call @ postcond_checker @ return in + + let m = subst_index old_index index m in + + let value = + Runtime.Local + { type_f = Bt_raw (ty_index, old_type); locals; body; id = Some id } + in + let func = + { Named.values = Indexed.return index value :: m.func.values + ; named = String_map.add id index m.func.named + } + in + { m with func } + +let contracts_generate (owi_funcs : (string * int) list) (m : modul) + (contracts : binary Contract.t list) : modul Result.t = + let rec join = function + | ([] | [ _ ]) as l -> l + | c1 :: c2 :: l -> + if Contract.compare_funcid c1 c2 <> 0 then c1 :: join (c2 :: l) + else join (Contract.join_contract c1 c2 :: l) + in + (* sort by numerical index and join contracts of a same function *) + let contracts = join (List.sort Contract.compare_funcid contracts) in + list_fold_left (contract_generate owi_funcs) m contracts + +let add_owi_funcs (m : modul) : modul * (string * int) list = + let owi_funcs : (string * binary func_type) list = + [ ("i32_symbol", ([], [ Num_type I32 ])) + ; ("i64_symbol", ([], [ Num_type I64 ])) + ; ("f32_symbol", ([], [ Num_type F32 ])) + ; ("f64_symbol", ([], [ Num_type F64 ])) + ; ("assume", ([ (None, Num_type I32) ], [])) + ; ("assert", ([ (None, Num_type I32) ], [])) + ] + in + + (* update module field `types` *) + let update_types () : modul * (string * (binary func_type * int)) list = + let func_type2rec_type : binary func_type -> binary rec_type = + fun ty -> [ (None, (Final, [], Def_func_t ty)) ] + in + let owi_funcs : (string * (binary func_type * binary rec_type)) list = + List.map (fun (name, ty) -> (name, (ty, func_type2rec_type ty))) owi_funcs + in + let values = m.types.values in + let values, owi_funcs = + List.fold_left_map + (fun values (name, (ft, rt)) -> + match + List.find_map + (fun (index, rt') -> + if rec_type_eq rt rt' then Some index else None ) + (Indexed.to_assoc_list values) + with + | Some index -> (values, (name, (ft, index))) + | None -> + let index = List.length values in + (Indexed.return index rt :: values, (name, (ft, index))) ) + (List.rev values) owi_funcs + in + let values = List.rev values in + ({ m with types = { values; named = m.types.named } }, owi_funcs) + in + let m, owi_funcs = update_types () in + + (* update module field `func` *) + let update_func () : modul * (string * int) list = + let imported, locals = + List.partition_map + (fun i -> + let v = Indexed.get i in + match v with + | Runtime.Imported _ -> Either.Left (Indexed.get_index i, v) + | Local _ -> Either.Right (Indexed.get_index i, v) ) + m.func.values + in + let imported_num = List.length imported in + let owi_funcs = + List.mapi + (fun i (name, (ty, index)) -> + ( name + , ( { Imported.modul = "symbolic" + ; name + ; assigned_name = Some name + ; desc = Bt_raw (Some (Raw index), ty) + } + , imported_num + i ) ) ) + owi_funcs + in + + let imported = + List.map + (fun (_, (f, index)) -> (index, Runtime.Imported f)) + (List.rev owi_funcs) + @ imported + in + + let subst_task, locals = + List.fold_left_map + (fun subst_task (old_index, f) -> + let index = old_index + List.length owi_funcs in + ((old_index, index) :: subst_task, (index, f)) ) + [] locals + in + + let values = + List.map (fun (index, f) -> Indexed.return index f) (imported @ locals) + in + let named = + List.map + (fun (name, index) -> + if index < imported_num then (name, index) + else (name, index + List.length owi_funcs) ) + (String_map.to_list m.func.named) + in + let named = + String_map.of_list + (List.map (fun (name, (_, index)) -> (name, index)) owi_funcs @ named) + in + + let m = { m with func = { values; named } } in + + let m = + List.fold_left + (fun m (old_index, index) -> + subst_index ~subst_custom:true old_index index m ) + m subst_task + in + let owi_funcs = + List.map (fun (name, (_, index)) -> (name, index)) owi_funcs + in + (m, owi_funcs) + in + update_func () + +let generate (enabled : bool) (m : modul) : modul Result.t = + if not enabled then Ok m + else + let m, owi_funcs = add_owi_funcs m in + contracts_generate owi_funcs m + (List.filter_map + (function From_annot (Annot.Contract c) -> Some c | _ -> None) + m.custom ) diff --git a/src/ast/code_generator.mli b/src/ast/code_generator.mli new file mode 100644 index 000000000..2f4eca1c1 --- /dev/null +++ b/src/ast/code_generator.mli @@ -0,0 +1,5 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +val generate : bool -> Binary.modul -> Binary.modul Result.t diff --git a/src/ast/compile.ml b/src/ast/compile.ml index 3411d41ae..3c8aea589 100644 --- a/src/ast/compile.ml +++ b/src/ast/compile.ml @@ -19,96 +19,100 @@ module Text = struct let* m = until_assign ~unsafe m in Rewrite.modul m - let until_typecheck ~unsafe m = + let until_typecheck ~unsafe ~rac m = let* m = until_binary ~unsafe m in + let* m = Code_generator.generate rac m in if unsafe then Ok m else let+ () = Typecheck.modul m in m - let until_optimize ~unsafe ~optimize m = - let+ m = until_typecheck ~unsafe m in + let until_optimize ~unsafe ~rac ~optimize m = + let+ m = until_typecheck ~unsafe ~rac m in if optimize then Optimize.modul m else m - let until_link ~unsafe ~optimize ~name link_state m = - let* m = until_optimize ~unsafe ~optimize m in + let until_link ~unsafe ~rac ~optimize ~name link_state m = + let* m = until_optimize ~unsafe ~rac ~optimize m in Link.modul link_state ~name m - let until_interpret ~unsafe ~optimize ~name link_state m = - let* m, link_state = until_link ~unsafe ~optimize ~name link_state m in + let until_interpret ~unsafe ~rac ~optimize ~name link_state m = + let* m, link_state = until_link ~unsafe ~rac ~optimize ~name link_state m in let+ () = Interpret.Concrete.modul link_state.envs m in link_state end module Binary = struct - let until_typecheck ~unsafe m = + let until_typecheck ~unsafe ~rac m = + let* m = Code_generator.generate rac m in if unsafe then Ok m else let+ () = Typecheck.modul m in m - let until_optimize ~unsafe ~optimize m = - let+ m = until_typecheck ~unsafe m in + let until_optimize ~unsafe ~rac ~optimize m = + let+ m = until_typecheck ~unsafe ~rac m in if optimize then Optimize.modul m else m - let until_link ~unsafe ~optimize ~name link_state m = - let* m = until_optimize ~unsafe ~optimize m in + let until_link ~unsafe ~rac ~optimize ~name link_state m = + let* m = until_optimize ~unsafe ~rac ~optimize m in Link.modul link_state ~name m - let until_interpret ~unsafe ~optimize ~name link_state m = - let* m, link_state = until_link ~unsafe ~optimize ~name link_state m in + let until_interpret ~unsafe ~rac ~optimize ~name link_state m = + let* m, link_state = until_link ~unsafe ~rac ~optimize ~name link_state m in let+ () = Interpret.Concrete.modul link_state.envs m in link_state end module Any = struct - let until_typecheck ~unsafe = function - | Kind.Wat m -> Text.until_typecheck ~unsafe m - | Wasm m -> Binary.until_typecheck ~unsafe m + let until_typecheck ~unsafe ~rac = function + | Kind.Wat m -> Text.until_typecheck ~unsafe ~rac m + | Wasm m -> Binary.until_typecheck ~unsafe ~rac m | Wast _ | Ocaml _ -> assert false - let until_optimize ~unsafe ~optimize = function - | Kind.Wat m -> Text.until_optimize ~unsafe ~optimize m - | Wasm m -> Binary.until_optimize ~unsafe ~optimize m + let until_optimize ~unsafe ~rac ~optimize = function + | Kind.Wat m -> Text.until_optimize ~unsafe ~rac ~optimize m + | Wasm m -> Binary.until_optimize ~unsafe ~rac ~optimize m | Wast _ | Ocaml _ -> assert false - let until_link ~unsafe ~optimize ~name link_state = function - | Kind.Wat m -> Text.until_link ~unsafe ~optimize ~name link_state m - | Wasm m -> Binary.until_link ~unsafe ~optimize ~name link_state m + let until_link ~unsafe ~rac ~optimize ~name link_state = function + | Kind.Wat m -> Text.until_link ~unsafe ~rac ~optimize ~name link_state m + | Wasm m -> Binary.until_link ~unsafe ~rac ~optimize ~name link_state m | Wast _ | Ocaml _ -> assert false - let until_interpret ~unsafe ~optimize ~name link_state = function - | Kind.Wat m -> Text.until_interpret ~unsafe ~optimize ~name link_state m - | Wasm m -> Binary.until_interpret ~unsafe ~optimize ~name link_state m + let until_interpret ~unsafe ~rac ~optimize ~name link_state = function + | Kind.Wat m -> + Text.until_interpret ~unsafe ~rac ~optimize ~name link_state m + | Wasm m -> Binary.until_interpret ~unsafe ~rac ~optimize ~name link_state m | Wast _ | Ocaml _ -> assert false end module File = struct - let until_typecheck ~unsafe filename = + let until_typecheck ~unsafe ~rac filename = let* m = Parse.guess_from_file filename in match m with - | Kind.Wat m -> Text.until_typecheck ~unsafe m - | Wasm m -> Binary.until_typecheck ~unsafe m + | Kind.Wat m -> Text.until_typecheck ~unsafe ~rac m + | Wasm m -> Binary.until_typecheck ~unsafe ~rac m | Wast _ | Ocaml _ -> assert false - let until_optimize ~unsafe ~optimize filename = + let until_optimize ~unsafe ~rac ~optimize filename = let* m = Parse.guess_from_file filename in match m with - | Kind.Wat m -> Text.until_optimize ~unsafe ~optimize m - | Wasm m -> Binary.until_optimize ~unsafe ~optimize m + | Kind.Wat m -> Text.until_optimize ~unsafe ~rac ~optimize m + | Wasm m -> Binary.until_optimize ~unsafe ~rac ~optimize m | Wast _ | Ocaml _ -> assert false - let until_link ~unsafe ~optimize ~name link_state filename = + let until_link ~unsafe ~rac ~optimize ~name link_state filename = let* m = Parse.guess_from_file filename in match m with - | Kind.Wat m -> Text.until_link ~unsafe ~optimize ~name link_state m - | Wasm m -> Binary.until_link ~unsafe ~optimize ~name link_state m + | Kind.Wat m -> Text.until_link ~unsafe ~rac ~optimize ~name link_state m + | Wasm m -> Binary.until_link ~unsafe ~rac ~optimize ~name link_state m | Wast _ | Ocaml _ -> assert false - let until_interpret ~unsafe ~optimize ~name link_state filename = + let until_interpret ~unsafe ~rac ~optimize ~name link_state filename = let* m = Parse.guess_from_file filename in match m with - | Kind.Wat m -> Text.until_interpret ~unsafe ~optimize ~name link_state m - | Wasm m -> Binary.until_interpret ~unsafe ~optimize ~name link_state m + | Kind.Wat m -> + Text.until_interpret ~unsafe ~rac ~optimize ~name link_state m + | Wasm m -> Binary.until_interpret ~unsafe ~rac ~optimize ~name link_state m | Wast _ | Ocaml _ -> assert false end diff --git a/src/ast/compile.mli b/src/ast/compile.mli index cde34ea63..e5bb649fb 100644 --- a/src/ast/compile.mli +++ b/src/ast/compile.mli @@ -6,15 +6,20 @@ module Any : sig val until_typecheck : - unsafe:bool -> 'extern_func Kind.t -> Binary.modul Result.t + unsafe:bool -> rac:bool -> 'extern_func Kind.t -> Binary.modul Result.t val until_optimize : - unsafe:bool -> optimize:bool -> 'extern_func Kind.t -> Binary.modul Result.t + unsafe:bool + -> rac:bool + -> optimize:bool + -> 'extern_func Kind.t + -> Binary.modul Result.t (** compile a module with a given link state and produce a new link state and a runnable module *) val until_link : unsafe:bool + -> rac:bool -> optimize:bool -> name:string option -> 'extern_func Link.state @@ -25,6 +30,7 @@ module Any : sig link state *) val until_interpret : unsafe:bool + -> rac:bool -> optimize:bool -> name:string option -> Concrete_value.Func.extern_func Link.state @@ -33,15 +39,17 @@ module Any : sig end module File : sig - val until_typecheck : unsafe:bool -> Fpath.t -> Binary.modul Result.t + val until_typecheck : + unsafe:bool -> rac:bool -> Fpath.t -> Binary.modul Result.t val until_optimize : - unsafe:bool -> optimize:bool -> Fpath.t -> Binary.modul Result.t + unsafe:bool -> rac:bool -> optimize:bool -> Fpath.t -> Binary.modul Result.t (** compile a file with a given link state and produce a new link state and a runnable module *) val until_link : unsafe:bool + -> rac:bool -> optimize:bool -> name:string option -> 'extern_func Link.state @@ -52,6 +60,7 @@ module File : sig link state *) val until_interpret : unsafe:bool + -> rac:bool -> optimize:bool -> name:string option -> Concrete_value.Func.extern_func Link.state @@ -64,15 +73,21 @@ module Text : sig val until_binary : unsafe:bool -> Text.modul -> Binary.modul Result.t - val until_typecheck : unsafe:bool -> Text.modul -> Binary.modul Result.t + val until_typecheck : + unsafe:bool -> rac:bool -> Text.modul -> Binary.modul Result.t val until_optimize : - unsafe:bool -> optimize:bool -> Text.modul -> Binary.modul Result.t + unsafe:bool + -> rac:bool + -> optimize:bool + -> Text.modul + -> Binary.modul Result.t (** compile a module with a given link state and produce a new link state and a runnable module *) val until_link : unsafe:bool + -> rac:bool -> optimize:bool -> name:string option -> 'f Link.state @@ -83,6 +98,7 @@ module Text : sig link state *) val until_interpret : unsafe:bool + -> rac:bool -> optimize:bool -> name:string option -> Concrete_value.Func.extern_func Link.state @@ -91,15 +107,21 @@ module Text : sig end module Binary : sig - val until_typecheck : unsafe:bool -> Binary.modul -> Binary.modul Result.t + val until_typecheck : + unsafe:bool -> rac:bool -> Binary.modul -> Binary.modul Result.t val until_optimize : - unsafe:bool -> optimize:bool -> Binary.modul -> Binary.modul Result.t + unsafe:bool + -> rac:bool + -> optimize:bool + -> Binary.modul + -> Binary.modul Result.t (** compile a module with a given link state and produce a new link state and a runnable module *) val until_link : unsafe:bool + -> rac:bool -> optimize:bool -> name:string option -> 'f Link.state @@ -110,6 +132,7 @@ module Binary : sig link state *) val until_interpret : unsafe:bool + -> rac:bool -> optimize:bool -> name:string option -> Concrete_value.Func.extern_func Link.state diff --git a/src/ast/types.ml b/src/ast/types.ml index 9794ac50c..af2ab109d 100644 --- a/src/ast/types.ml +++ b/src/ast/types.ml @@ -42,13 +42,15 @@ let pp_indice (type kind) fmt : kind indice -> unit = function | Raw u -> int fmt u | Text i -> pp_id fmt i -let compare_indice id1 id2 = +let compare_indice (type a) (id1 : a indice) (id2 : a indice) = match (id1, id2) with | Raw i1, Raw i2 -> compare i1 i2 | Text s1, Text s2 -> String.compare s1 s2 | Raw _, Text _ -> -1 | Text _, Raw _ -> 1 +let indice_eq id1 id2 = compare_indice id1 id2 = 0 + let pp_indice_opt fmt = function None -> () | Some i -> pp_indice fmt i let pp_indices fmt ids = list ~sep:sp pp_indice fmt ids @@ -257,6 +259,11 @@ let pp_final fmt = function | Final -> pf fmt "final" | No_final -> pf fmt "no_final" +let final_eq f1 f2 = + match (f1, f2) with + | Final, Final | No_final, No_final -> true + | _, _ -> false + (** Structure *) (** Types *) @@ -927,6 +934,9 @@ type 'a sub_type = final * 'a indice list * 'a str_type let pp_sub_type fmt (f, ids, t) = pf fmt "(sub %a %a %a)" pp_final f pp_indices ids str_type t +let sub_type_eq (f1, ids1, t1) (f2, ids2, t2) = + final_eq f1 f2 && List.equal indice_eq ids1 ids2 && str_type_eq t1 t2 + type 'a type_def = string option * 'a sub_type let pp_type_def_no_indent fmt (id, t) = @@ -934,6 +944,9 @@ let pp_type_def_no_indent fmt (id, t) = let pp_type_def fmt t = pf fmt "@\n @[%a@]" pp_type_def_no_indent t +let type_def_eq (id1, t1) (id2, t2) = + Option.equal String.equal id1 id2 && sub_type_eq t1 t2 + type 'a rec_type = 'a type_def list let pp_rec_type fmt l = @@ -942,6 +955,8 @@ let pp_rec_type fmt l = | [ t ] -> pf fmt "@\n%a" pp_type_def_no_indent t | l -> pf fmt "(rec %a)" (list ~sep:sp pp_type_def) l +let rec_type_eq l1 l2 = List.equal type_def_eq l1 l2 + let pp_start fmt start = pf fmt "(start %a)" pp_indice start type 'a const = diff --git a/src/bin/owi.ml b/src/bin/owi.ml index 156faa89e..ed16601f9 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -103,9 +103,9 @@ let workspace = Cmdliner.Arg.( value & opt dir_file (Fpath.v "owi-out") & info [ "workspace" ] ~doc ) -let spec = +let rac = let doc = "WEbAssembly Specification Language" in - Cmdliner.Arg.(value & flag & info [ "spec" ] ~doc) + Cmdliner.Arg.(value & flag & info [ "runtime-assertion-checking"; "r" ] ~doc) let copts_t = Cmdliner.Term.(const []) @@ -181,7 +181,7 @@ let opt_cmd = let man = [] @ shared_man in Cmd.info "opt" ~version ~doc ~sdocs ~man in - Cmd.v info Term.(const Cmd_opt.cmd $ debug $ unsafe $ files) + Cmd.v info Term.(const Cmd_opt.cmd $ debug $ unsafe $ rac $ files) let run_cmd = let open Cmdliner in @@ -191,7 +191,8 @@ let run_cmd = Cmd.info "run" ~version ~doc ~sdocs ~man in Cmd.v info - Term.(const Cmd_run.cmd $ profiling $ debug $ unsafe $ optimize $ files) + Term.( + const Cmd_run.cmd $ profiling $ debug $ unsafe $ rac $ optimize $ files ) let validate_cmd = let open Cmdliner in @@ -200,7 +201,7 @@ let validate_cmd = let man = [] @ shared_man in Cmd.info "validate" ~version ~doc ~sdocs ~man in - Cmd.v info Term.(const Cmd_validate.cmd $ debug $ files) + Cmd.v info Term.(const Cmd_validate.cmd $ debug $ rac $ files) let script_cmd = let open Cmdliner in @@ -211,7 +212,7 @@ let script_cmd = in Cmd.v info Term.( - const Cmd_script.cmd $ profiling $ debug $ optimize $ files + const Cmd_script.cmd $ profiling $ debug $ rac $ optimize $ files $ no_exhaustion ) let sym_cmd = @@ -224,7 +225,7 @@ let sym_cmd = Cmd.v info Term.( const Cmd_sym.cmd $ profiling $ debug $ unsafe $ optimize $ workers - $ no_stop_at_failure $ no_values $ deterministic_result_order $ spec + $ no_stop_at_failure $ no_values $ deterministic_result_order $ rac $ fail_mode $ workspace $ solver $ files ) let conc_cmd = @@ -237,7 +238,7 @@ let conc_cmd = Cmd.v info Term.( const Cmd_conc.cmd $ profiling $ debug $ unsafe $ optimize $ workers - $ no_stop_at_failure $ no_values $ deterministic_result_order $ spec + $ no_stop_at_failure $ no_values $ deterministic_result_order $ rac $ fail_mode $ workspace $ solver $ files ) let wasm2wat_cmd = @@ -261,7 +262,9 @@ let wat2wasm_cmd = Cmd.info "wat2wasm" ~version ~doc ~sdocs ~man in Cmd.v info - Term.(const Cmd_wat2wasm.cmd $ profiling $ debug $ unsafe $ optimize $ files) + Term.( + const Cmd_wat2wasm.cmd $ profiling $ debug $ unsafe $ rac $ optimize + $ files ) let cli = let open Cmdliner in @@ -351,21 +354,22 @@ let exit_code = | `Unknown_type _id -> 52 | `Unsupported_file_extension _ext -> 53 | `Failed_with_but_expected (_got, _expected) -> 54 - | `Annotation_id_incorrect _annotid -> 55 - | `Invalid_int32 _i32 -> 56 - | `Invalid_int64 _i64 -> 57 - | `Invalid_float32 _f32 -> 58 - | `Invalid_float64 _f64 -> 59 - | `Invalid_indice _id -> 60 - | `Invalid_text_indice _id -> 61 + | `Spec_invalid_int32 _i32 -> 56 + | `Spec_invalid_int64 _i64 -> 57 + | `Spec_invalid_float32 _f32 -> 58 + | `Spec_invalid_float64 _f64 -> 59 + | `Spec_invalid_indice _id -> 60 + | `Spec_invalid_text_indice _id -> 61 | `Unknown_annotation_clause _s -> 62 | `Unknown_annotation_object _s -> 63 - | `Unknown_binder _id -> 64 - | `Unknown_param _id -> 65 - | `Unknown_variable _id -> 66 - | `Unknown_binder_type _s -> 67 - | `Unknown_prop _pr -> 68 - | `Unknown_term _tm -> 69 + | `Spec_unknown_binder _id -> 64 + | `Spec_unknown_param _id -> 65 + | `Spec_unknown_variable _id -> 66 + | `Spec_unknown_binder_type _s -> 67 + | `Spec_unknown_prop _pr -> 68 + | `Spec_unknown_term _tm -> 69 + | `Spec_type_error _str -> 70 + | `Contract_unknown_func _id -> 71 end end | Error e -> ( diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index d628a324e..58a0d5f07 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -15,21 +15,22 @@ let ( let** ) (t : 'a Result.t Choice.t) (f : 'a -> 'b Result.t Choice.t) : Choice.bind t (fun t -> match t with Error e -> Choice.return (Error e) | Ok x -> f x ) -let simplify_then_link ~unsafe ~optimize link_state m = +let simplify_then_link ~unsafe ~optimize ~rac link_state m = let* m = match m with - | Kind.Wat _ | Wasm _ -> Compile.Any.until_typecheck ~unsafe m + | Kind.Wat _ | Wasm _ -> Compile.Any.until_typecheck ~unsafe ~rac m | Wast _ -> Error (`Msg "can't run concolic interpreter on a script") | Ocaml _ -> assert false in let* m = Cmd_utils.add_main_as_start m in let+ m, link_state = - Compile.Binary.until_link ~unsafe link_state ~optimize ~name:None m + Compile.Binary.until_link ~unsafe ~rac:false ~optimize ~name:None link_state + m in let module_to_run = Concolic.convert_module_to_run m in (link_state, module_to_run) -let simplify_then_link_files ~unsafe ~optimize filenames = +let simplify_then_link_files ~unsafe ~optimize ~rac filenames = let link_state = Link.empty_state in let link_state = Link.extern_module' link_state ~name:"symbolic" @@ -47,7 +48,7 @@ let simplify_then_link_files ~unsafe ~optimize filenames = let* link_state, modules_to_run = acc in let* m0dule = Parse.guess_from_file filename in let+ link_state, module_to_run = - simplify_then_link ~unsafe ~optimize link_state m0dule + simplify_then_link ~unsafe ~optimize ~rac link_state m0dule in (link_state, module_to_run :: modules_to_run) ) (Ok (link_state, [])) @@ -401,8 +402,8 @@ let launch solver tree link_state modules_to_run = which are handled here. Most of the computations are done in the Result monad, hence the let*. *) let cmd profiling debug unsafe optimize _workers _no_stop_at_failure no_values - _deterministic_result_order _spec _fail_mode (workspace : Fpath.t) solver - files = + _deterministic_result_order rac _fail_mode (workspace : Fpath.t) solver files + = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; @@ -411,7 +412,7 @@ let cmd profiling debug unsafe optimize _workers _no_stop_at_failure no_values let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in let solver = Solver.fresh solver () in let* link_state, modules_to_run = - simplify_then_link_files ~unsafe ~optimize files + simplify_then_link_files ~unsafe ~optimize ~rac files in let tree = fresh_tree [] in let* result = launch solver tree link_state modules_to_run in diff --git a/src/cmd/cmd_opt.ml b/src/cmd/cmd_opt.ml index 1104f0362..a333f87d2 100644 --- a/src/cmd/cmd_opt.ml +++ b/src/cmd/cmd_opt.ml @@ -4,14 +4,14 @@ open Syntax -let optimize_file ~unsafe filename = - Compile.File.until_optimize ~unsafe ~optimize:true filename +let optimize_file ~unsafe ~rac filename = + Compile.File.until_optimize ~unsafe ~rac ~optimize:true filename -let cmd debug unsafe files = +let cmd debug unsafe rac files = if debug then Log.debug_on := true; list_iter (fun file -> - let+ m = optimize_file ~unsafe file in + let+ m = optimize_file ~unsafe ~rac file in let m = Binary_to_text.modul m in Fmt.pr "%a@\n" Text.pp_modul m ) files diff --git a/src/cmd/cmd_opt.mli b/src/cmd/cmd_opt.mli index b26bccd2a..96aaaceb4 100644 --- a/src/cmd/cmd_opt.mli +++ b/src/cmd/cmd_opt.mli @@ -2,4 +2,4 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> bool -> Fpath.t list -> unit Result.t +val cmd : bool -> bool -> bool -> Fpath.t list -> unit Result.t diff --git a/src/cmd/cmd_run.ml b/src/cmd/cmd_run.ml index 689dc2e65..abf51ce5b 100644 --- a/src/cmd/cmd_run.ml +++ b/src/cmd/cmd_run.ml @@ -4,15 +4,15 @@ open Syntax -let run_file ~unsafe ~optimize filename = +let run_file ~unsafe ~rac ~optimize filename = let name = None in let+ (_ : _ Link.state) = - Compile.File.until_interpret ~unsafe ~optimize ~name Link.empty_state + Compile.File.until_interpret ~unsafe ~rac ~optimize ~name Link.empty_state filename in () -let cmd profiling debug unsafe optimize files = +let cmd profiling debug unsafe rac optimize files = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; - list_iter (run_file ~unsafe ~optimize) files + list_iter (run_file ~unsafe ~rac ~optimize) files diff --git a/src/cmd/cmd_run.mli b/src/cmd/cmd_run.mli index 5cef2e0c3..63aec0acf 100644 --- a/src/cmd/cmd_run.mli +++ b/src/cmd/cmd_run.mli @@ -2,4 +2,4 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> bool -> bool -> bool -> Fpath.t list -> unit Result.t +val cmd : bool -> bool -> bool -> bool -> bool -> Fpath.t list -> unit Result.t diff --git a/src/cmd/cmd_script.ml b/src/cmd/cmd_script.ml index 30048a92c..4bf1be2da 100644 --- a/src/cmd/cmd_script.ml +++ b/src/cmd/cmd_script.ml @@ -8,8 +8,8 @@ let run_file exec filename = let* script = Parse.Text.Script.from_file filename in exec script -let cmd profiling debug optimize files no_exhaustion = - let exec = Script.exec ~no_exhaustion ~optimize in +let cmd profiling debug rac optimize files no_exhaustion = + let exec = Script.exec ~rac ~no_exhaustion ~optimize in if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; list_iter (run_file exec) files diff --git a/src/cmd/cmd_script.mli b/src/cmd/cmd_script.mli index fe2dd1058..60666d712 100644 --- a/src/cmd/cmd_script.mli +++ b/src/cmd/cmd_script.mli @@ -2,4 +2,4 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> bool -> bool -> Fpath.t list -> bool -> unit Result.t +val cmd : bool -> bool -> bool -> bool -> Fpath.t list -> bool -> unit Result.t diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 136eb65e4..7bb2a732d 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -26,14 +26,15 @@ let link_state = Link.extern_module' link_state ~name:"summaries" ~func_typ Symbolic_wasm_ffi.summaries_extern_module ) -let run_file ~unsafe ~optimize pc filename = - let*/ m = Compile.File.until_typecheck ~unsafe filename in +let run_file ~unsafe ~optimize ~rac pc filename = + let*/ m = Compile.File.until_typecheck ~unsafe ~rac filename in let*/ m = Cmd_utils.add_main_as_start m in let link_state = Lazy.force link_state in let*/ m, link_state = - Compile.Binary.until_link ~unsafe link_state ~optimize ~name:None m + Compile.Binary.until_link ~unsafe ~rac:false ~optimize ~name:None link_state + m in let m = Symbolic.convert_module_to_run m in let c = Interpret.SymbolicP.modul link_state.envs m in @@ -45,15 +46,14 @@ let run_file ~unsafe ~optimize pc filename = which are handled here. Most of the computations are done in the Result monad, hence the let*. *) let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values - deterministic_result_order _spec fail_mode (workspace : Fpath.t) solver files - = + deterministic_result_order rac fail_mode (workspace : Fpath.t) solver files = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; (* deterministic_result_order implies no_stop_at_failure *) let no_stop_at_failure = deterministic_result_order || no_stop_at_failure in let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in let pc = Choice.return (Ok ()) in - let result = List.fold_left (run_file ~unsafe ~optimize) pc files in + let result = List.fold_left (run_file ~unsafe ~optimize ~rac) pc files in let thread = Thread_with_memory.init () in let res_queue = Wq.make () in let callback v = diff --git a/src/cmd/cmd_validate.ml b/src/cmd/cmd_validate.ml index d9bffa72d..d56c1ad1a 100644 --- a/src/cmd/cmd_validate.ml +++ b/src/cmd/cmd_validate.ml @@ -4,12 +4,12 @@ open Syntax -let validate filename = +let validate rac filename = let+ (_modul : Binary.modul) = - Compile.File.until_typecheck ~unsafe:false filename + Compile.File.until_typecheck ~unsafe:false ~rac filename in () -let cmd debug files = +let cmd debug rac files = if debug then Log.debug_on := true; - list_iter validate files + list_iter (validate rac) files diff --git a/src/cmd/cmd_validate.mli b/src/cmd/cmd_validate.mli index 433a95470..b26bccd2a 100644 --- a/src/cmd/cmd_validate.mli +++ b/src/cmd/cmd_validate.mli @@ -2,4 +2,4 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> Fpath.t list -> unit Result.t +val cmd : bool -> bool -> Fpath.t list -> unit Result.t diff --git a/src/cmd/cmd_wat2wasm.ml b/src/cmd/cmd_wat2wasm.ml index 4192eaeb4..f25863e64 100644 --- a/src/cmd/cmd_wat2wasm.ml +++ b/src/cmd/cmd_wat2wasm.ml @@ -4,15 +4,15 @@ open Syntax -let cmd_one ~unsafe ~optimize file = +let cmd_one ~unsafe ~rac ~optimize file = let ext = Fpath.get_ext file in match ext with | ".wat" -> let* modul = Parse.Text.Module.from_file file in - Binary_encoder.convert file ~unsafe ~optimize modul + Binary_encoder.convert file ~unsafe ~rac ~optimize modul | ext -> Error (`Unsupported_file_extension ext) -let cmd profiling debug unsafe optimize files = +let cmd profiling debug unsafe rac optimize files = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; - list_iter (cmd_one ~unsafe ~optimize) files + list_iter (cmd_one ~unsafe ~rac ~optimize) files diff --git a/src/cmd/cmd_wat2wasm.mli b/src/cmd/cmd_wat2wasm.mli index 5cef2e0c3..63aec0acf 100644 --- a/src/cmd/cmd_wat2wasm.mli +++ b/src/cmd/cmd_wat2wasm.mli @@ -2,4 +2,4 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> bool -> bool -> bool -> Fpath.t list -> unit Result.t +val cmd : bool -> bool -> bool -> bool -> bool -> Fpath.t list -> unit Result.t diff --git a/src/data_structures/indexed.ml b/src/data_structures/indexed.ml index 02b89f1b2..a16deb1df 100644 --- a/src/data_structures/indexed.ml +++ b/src/data_structures/indexed.ml @@ -21,3 +21,7 @@ let get_at i values = match List.find_opt (has_index i) values with | None -> None | Some { value; _ } -> Some value + +let rec to_assoc_list = function + | [] -> [] + | { index; value } :: l -> (index, value) :: to_assoc_list l diff --git a/src/data_structures/indexed.mli b/src/data_structures/indexed.mli index 14602cf80..146a98bd0 100644 --- a/src/data_structures/indexed.mli +++ b/src/data_structures/indexed.mli @@ -15,3 +15,5 @@ val return : int -> 'a -> 'a t val get_at : int -> 'a t list -> 'a option val has_index : int -> 'a t -> bool + +val to_assoc_list : 'a t list -> (int * 'a) list diff --git a/src/dune b/src/dune index adcde45a9..51ce53df1 100644 --- a/src/dune +++ b/src/dune @@ -24,6 +24,7 @@ cmd_validate cmd_wasm2wat cmd_wat2wasm + code_generator compile concolic concolic_choice diff --git a/src/script/script.ml b/src/script/script.ml index 3a4ec98f7..6ed2cb5d2 100644 --- a/src/script/script.ml +++ b/src/script/script.ml @@ -141,7 +141,7 @@ let action (link_state : Concrete_value.Func.extern_func Link.state) = function let unsafe = false -let run ~no_exhaustion ~optimize script = +let run ~no_exhaustion ~rac ~optimize script = let state = Link.extern_module Link.empty_state ~name:"spectest_extern" Spectest.extern_m @@ -157,7 +157,8 @@ let run ~no_exhaustion ~optimize script = Log.debug0 "*** module@\n"; incr curr_module; let+ link_state = - Compile.Text.until_interpret link_state ~unsafe ~optimize ~name:None m + Compile.Text.until_interpret link_state ~unsafe ~rac ~optimize + ~name:None m in Log.debug_on := debug_on; link_state @@ -166,7 +167,8 @@ let run ~no_exhaustion ~optimize script = incr curr_module; let* m = Parse.Text.Inline_module.from_string m in let+ link_state = - Compile.Text.until_interpret link_state ~unsafe ~optimize ~name:None m + Compile.Text.until_interpret link_state ~unsafe ~rac ~optimize + ~name:None m in link_state | Text.Binary_module (id, m) -> @@ -175,15 +177,15 @@ let run ~no_exhaustion ~optimize script = let* m = Parse.Binary.Module.from_string m in let m = { m with id } in let+ link_state = - Compile.Binary.until_interpret link_state ~unsafe ~optimize ~name:None - m + Compile.Binary.until_interpret link_state ~unsafe ~rac ~optimize + ~name:None m in link_state | Assert (Assert_trap_module (m, expected)) -> Log.debug0 "*** assert_trap@\n"; incr curr_module; let* m, link_state = - Compile.Text.until_link link_state ~unsafe ~optimize ~name:None m + Compile.Text.until_link link_state ~unsafe ~rac ~optimize ~name:None m in let got = Interpret.Concrete.modul link_state.envs m in let+ () = check_error_result expected got in @@ -224,7 +226,7 @@ let run ~no_exhaustion ~optimize script = | Assert (Assert_invalid (m, expected)) -> Log.debug0 "*** assert_invalid@\n"; let got = - Compile.Text.until_link link_state ~unsafe ~optimize ~name:None m + Compile.Text.until_link link_state ~unsafe ~rac ~optimize ~name:None m in let+ () = check_error_result expected got in link_state @@ -236,14 +238,14 @@ let run ~no_exhaustion ~optimize script = | Assert (Assert_unlinkable (m, expected)) -> Log.debug0 "*** assert_unlinkable@\n"; let got = - Compile.Text.until_link link_state ~unsafe ~optimize ~name:None m + Compile.Text.until_link link_state ~unsafe ~rac ~optimize ~name:None m in let+ () = check_error_result expected got in link_state | Assert (Assert_malformed (m, expected)) -> Log.debug0 "*** assert_malformed@\n"; let got = - Compile.Text.until_link ~unsafe ~optimize ~name:None link_state m + Compile.Text.until_link ~unsafe ~rac ~optimize ~name:None link_state m in let+ () = check_error_result expected got in assert false @@ -286,6 +288,6 @@ let run ~no_exhaustion ~optimize script = link_state ) state script -let exec ~no_exhaustion ~optimize script = - let+ _link_state = run ~no_exhaustion ~optimize script in +let exec ~no_exhaustion ~rac ~optimize script = + let+ _link_state = run ~no_exhaustion ~rac ~optimize script in () diff --git a/src/script/script.mli b/src/script/script.mli index d3a86af8a..08788491e 100644 --- a/src/script/script.mli +++ b/src/script/script.mli @@ -5,4 +5,9 @@ (** Module to execute a full Wasm script. *) (** execute a Wasm script *) -val exec : no_exhaustion:bool -> optimize:bool -> Text.script -> unit Result.t +val exec : + no_exhaustion:bool + -> rac:bool + -> optimize:bool + -> Text.script + -> unit Result.t diff --git a/src/text_to_binary/rewrite.ml b/src/text_to_binary/rewrite.ml index 6020b6f44..243a7cba5 100644 --- a/src/text_to_binary/rewrite.ml +++ b/src/text_to_binary/rewrite.ml @@ -405,14 +405,14 @@ let rec rewrite_term ~(binder_list : string option list) ~(modul : Binary.modul) binary indice Result.t = match ind with | Raw id -> Ok (Raw id) - | Text id -> find_raw_indice (`Unknown_binder ind) 0 id binder_list + | Text id -> find_raw_indice (`Spec_unknown_binder ind) 0 id binder_list in let find_param (func_param_list : string option list) (ind : text indice) : binary indice Result.t = match ind with | Raw id -> Ok (Raw id) - | Text id -> find_raw_indice (`Unknown_param ind) 0 id func_param_list + | Text id -> find_raw_indice (`Spec_unknown_param ind) 0 id func_param_list in let find_global (modul : Binary.modul) (ind : text indice) : @@ -440,7 +440,7 @@ let rec rewrite_term ~(binder_list : string option list) ~(modul : Binary.modul) | Ok ind, _, _ -> Ok (BinderVar ind) | _, Ok ind, _ -> Ok (ParamVar ind) | _, _, Ok ind -> Ok (GlobalVar ind) - | _, _, _ -> Error (`Unknown_variable ind) ) + | _, _, _ -> Error (`Spec_unknown_variable ind) ) | ParamVar ind -> let+ ind = find_param func_param_list ind in ParamVar ind @@ -457,7 +457,7 @@ let rec rewrite_term ~(binder_list : string option list) ~(modul : Binary.modul) let* tm1 = rewrite_term ~binder_list ~modul ~func_param_list tm1 in let+ tm2 = rewrite_term ~binder_list ~modul ~func_param_list tm2 in BinOp (b, tm1, tm2) - | Result -> Ok Result + | Result i -> Ok (Result i) let rec rewrite_prop ~(binder_list : string option list) ~(modul : Binary.modul) ~(func_param_list : string option list) : @@ -484,11 +484,15 @@ let rec rewrite_prop ~(binder_list : string option list) ~(modul : Binary.modul) let rewrite_contract (modul : Binary.modul) : text Contract.t -> binary Contract.t Result.t = fun { Contract.funcid; preconditions; postconditions } -> - let* func = get (`Unknown_func funcid) modul.func funcid in - let funcid = Raw (Indexed.get_index func) in + let (Raw i as funcid) = find modul.func funcid in + let* func = + match Indexed.get_at i modul.func.values with + | None -> Error (`Unknown_func funcid) + | Some v -> Ok v + in let func_param_list = let (Bt_raw (_, (params, _))) = - match Indexed.get func with + match func with | Local { type_f; _ } -> type_f | Imported { desc; _ } -> desc in diff --git a/src/utils/result.ml b/src/utils/result.ml index f4361e0ab..8eaf59aac 100644 --- a/src/utils/result.ml +++ b/src/utils/result.ml @@ -59,21 +59,22 @@ type err = | `Unknown_table of Types.text Types.indice | `Unknown_type of Types.text Types.indice | `Unsupported_file_extension of string - | `Annotation_id_incorrect of string - | `Invalid_int32 of string - | `Invalid_int64 of string - | `Invalid_float32 of string - | `Invalid_float64 of string - | `Invalid_indice of string - | `Invalid_text_indice of string + | `Spec_invalid_int32 of string + | `Spec_invalid_int64 of string + | `Spec_invalid_float32 of string + | `Spec_invalid_float64 of string + | `Spec_invalid_indice of string + | `Spec_invalid_text_indice of string | `Unknown_annotation_clause of Sexp.t | `Unknown_annotation_object of Sexp.t - | `Unknown_binder of Types.text Types.indice - | `Unknown_param of Types.text Types.indice - | `Unknown_variable of Types.text Types.indice - | `Unknown_binder_type of Sexp.t - | `Unknown_prop of Sexp.t - | `Unknown_term of Sexp.t + | `Spec_unknown_binder of Types.text Types.indice + | `Spec_unknown_param of Types.text Types.indice + | `Spec_unknown_variable of Types.text Types.indice + | `Spec_unknown_binder_type of Sexp.t + | `Spec_unknown_prop of Sexp.t + | `Spec_unknown_term of Sexp.t + | `Spec_type_error of string + | `Contract_unknown_func of Types.text Types.indice ] type 'a t = ('a, err) Prelude.Result.t @@ -139,21 +140,26 @@ let rec err_to_string = function | `Unknown_type id -> Fmt.str "unknown type %a" Types.pp_indice id | `Unsupported_file_extension ext -> Fmt.str "unsupported file_extension %S" ext - | `Annotation_id_incorrect annotid -> - Fmt.str "annotation id %S incorrect" annotid - | `Invalid_int32 i32 -> Fmt.str "invalid int32 %S" i32 - | `Invalid_int64 i64 -> Fmt.str "invalid int64 %S" i64 - | `Invalid_float32 f32 -> Fmt.str "invalid float32 %S" f32 - | `Invalid_float64 f64 -> Fmt.str "invalid float64 %S" f64 - | `Invalid_indice id -> Fmt.str "invalid indice %S" id - | `Invalid_text_indice id -> Fmt.str "invalid text indice %S" id + | `Spec_invalid_int32 i32 -> Fmt.str "spec: invalid int32 %S" i32 + | `Spec_invalid_int64 i64 -> Fmt.str "spec: invalid int64 %S" i64 + | `Spec_invalid_float32 f32 -> Fmt.str "spec: invalid float32 %S" f32 + | `Spec_invalid_float64 f64 -> Fmt.str "spec: invalid float64 %S" f64 + | `Spec_invalid_indice id -> Fmt.str "spec: invalid indice %S" id + | `Spec_invalid_text_indice id -> Fmt.str "spec: invalid text indice %S" id | `Unknown_annotation_clause s -> Fmt.str "unknown annotation clause %a" Sexp.pp_sexp s | `Unknown_annotation_object s -> Fmt.str "unknown annotation object %a" Sexp.pp_sexp s - | `Unknown_binder id -> Fmt.str "unknown binder %a" Types.pp_indice id - | `Unknown_param id -> Fmt.str "unknown param %a" Types.pp_indice id - | `Unknown_variable id -> Fmt.str "unknown variable %a" Types.pp_indice id - | `Unknown_binder_type s -> Fmt.str "unknown binder type %a" Sexp.pp_sexp s - | `Unknown_prop pr -> Fmt.str "unknown prop %a" Sexp.pp_sexp pr - | `Unknown_term tm -> Fmt.str "unknown term %a" Sexp.pp_sexp tm + | `Spec_unknown_binder id -> + Fmt.str "spec: unknown binder %a" Types.pp_indice id + | `Spec_unknown_param id -> + Fmt.str "spec: unknown param %a" Types.pp_indice id + | `Spec_unknown_variable id -> + Fmt.str "spec: unknown variable %a" Types.pp_indice id + | `Spec_unknown_binder_type s -> + Fmt.str "spec: unknown binder type %a" Sexp.pp_sexp s + | `Spec_unknown_prop pr -> Fmt.str "spec: unknown prop %a" Sexp.pp_sexp pr + | `Spec_unknown_term tm -> Fmt.str "spec: unknown term %a" Sexp.pp_sexp tm + | `Spec_type_error str -> Fmt.str "spec: %S type error" str + | `Contract_unknown_func id -> + Fmt.str "contract: unknown function %a" Types.pp_indice id diff --git a/src/utils/result.mli b/src/utils/result.mli index bbc69331b..41856833e 100644 --- a/src/utils/result.mli +++ b/src/utils/result.mli @@ -59,21 +59,22 @@ type err = | `Unknown_table of Types.text Types.indice | `Unknown_type of Types.text Types.indice | `Unsupported_file_extension of string - | `Annotation_id_incorrect of string - | `Invalid_int32 of string - | `Invalid_int64 of string - | `Invalid_float32 of string - | `Invalid_float64 of string - | `Invalid_indice of string - | `Invalid_text_indice of string + | `Spec_invalid_int32 of string + | `Spec_invalid_int64 of string + | `Spec_invalid_float32 of string + | `Spec_invalid_float64 of string + | `Spec_invalid_indice of string + | `Spec_invalid_text_indice of string | `Unknown_annotation_clause of Sexp.t | `Unknown_annotation_object of Sexp.t - | `Unknown_binder of Types.text Types.indice - | `Unknown_param of Types.text Types.indice - | `Unknown_variable of Types.text Types.indice - | `Unknown_binder_type of Sexp.t - | `Unknown_prop of Sexp.t - | `Unknown_term of Sexp.t + | `Spec_unknown_binder of Types.text Types.indice + | `Spec_unknown_param of Types.text Types.indice + | `Spec_unknown_variable of Types.text Types.indice + | `Spec_unknown_binder_type of Sexp.t + | `Spec_unknown_prop of Sexp.t + | `Spec_unknown_term of Sexp.t + | `Spec_type_error of string + | `Contract_unknown_func of Types.text Types.indice ] type 'a t = ('a, err) Prelude.Result.t diff --git a/src/utils/syntax.ml b/src/utils/syntax.ml index dcab8db4b..c790b24bc 100644 --- a/src/utils/syntax.ml +++ b/src/utils/syntax.ml @@ -38,6 +38,20 @@ let list_map f l = l with Exit -> Option.get !err +let list_concat_map f l = + let err = ref None in + try + ok + @@ List.concat_map + (fun v -> + match f v with + | Error _e as e -> + err := Some e; + raise Exit + | Ok v -> v ) + l + with Exit -> Option.get !err + let list_fold_left f acc l = List.fold_left (fun acc v -> diff --git a/src/utils/syntax.mli b/src/utils/syntax.mli index bec07d026..bad4a7951 100644 --- a/src/utils/syntax.mli +++ b/src/utils/syntax.mli @@ -22,6 +22,11 @@ val list_map : -> 'a list -> ('b list, 'err) Prelude.Result.t +val list_concat_map : + ('a -> ('b list, 'err) Prelude.Result.t) + -> 'a list + -> ('b list, 'err) Prelude.Result.t + val list_fold_left : ('a -> 'b -> ('a, 'err) Prelude.Result.t) -> 'a