diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 107 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 32 | ||||
| -rw-r--r-- | compiler/Pure.ml | 20 | ||||
| -rw-r--r-- | compiler/PureTypeCheck.ml | 4 | ||||
| -rw-r--r-- | compiler/SymbolicAst.ml | 2 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 47 | ||||
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 6 | ||||
| -rw-r--r-- | compiler/Translate.ml | 1 |
8 files changed, 172 insertions, 47 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index a93ed6e4..3c5ea15b 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -185,9 +185,17 @@ let extract_adt_g_value | _ -> raise (Failure "Inconsistent typed value") (* Extract globals in the same way as variables *) -let extract_global (ctx : extraction_ctx) (fmt : F.formatter) - (id : A.GlobalDeclId.id) : unit = - F.pp_print_string fmt (ctx_get_global id ctx) +let extract_global (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) + (id : A.GlobalDeclId.id) (generics : generic_args) : unit = + let use_brackets = inside && generics <> empty_generic_args in + F.pp_open_hvbox fmt ctx.indent_incr; + if use_brackets then F.pp_print_string fmt "("; + (* Extract the global name *) + F.pp_print_string fmt (ctx_get_global id ctx); + (* Extract the generics *) + extract_generic_args ctx fmt TypeDeclId.Set.empty generics; + if use_brackets then F.pp_print_string fmt ")"; + F.pp_close_box fmt () (* Filter the generics of a function if it is builtin *) let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list) @@ -321,7 +329,9 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) match qualif.id with | FunOrOp fun_id -> extract_function_call ctx fmt inside fun_id qualif.generics args - | Global global_id -> extract_global ctx fmt global_id + | Global global_id -> + assert (args = []); + extract_global ctx fmt inside global_id qualif.generics | AdtCons adt_cons_id -> extract_adt_cons ctx fmt inside adt_cons_id qualif.generics args | Proj proj -> @@ -1691,7 +1701,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) of those declarations. See {!extract_global_decl} for more explanations. *) let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) - (kind : decl_kind) (name : string) (ty : ty) + (kind : decl_kind) (name : string) (generics : generic_params) + (type_params : string list) (cg_params : string list) + (trait_clauses : string list) (ty : ty) (extract_body : (F.formatter -> unit) Option.t) : unit = let is_opaque = Option.is_none extract_body in @@ -1708,9 +1720,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hvbox fmt 0; F.pp_open_hvbox fmt ctx.indent_incr; - (* Open "QUALIF NAME : TYPE =" box (depth=1) *) + (* Open "QUALIF NAME PARAMS : TYPE =" box (depth=1) *) F.pp_open_hovbox fmt ctx.indent_incr; - (* Print "QUALIF NAME " *) + (* Print "QUALIF NAME PARAMS " *) (match fun_decl_kind_to_qualif kind with | Some qualif -> F.pp_print_string fmt qualif; @@ -1719,6 +1731,12 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt name; F.pp_print_space fmt (); + (* Extract the generic parameters *) + let space = ref true in + extract_generic_params ctx fmt TypeDeclId.Set.empty ~space:(Some space) + generics type_params cg_params trait_clauses; + if not !space then F.pp_print_space fmt (); + (* Open ": TYPE =" box (depth=2) *) F.pp_open_hvbox fmt 0; (* Print ": " *) @@ -1775,7 +1793,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) but I could not find a better way. *) let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) - (name : string) (ty : ty) : unit = + (name : string) (generics : generic_params) (ty : ty) : unit = + (* TODO: non-empty generics *) + assert (generics = empty_generic_params); (* Open the definition boxe (depth=0) *) F.pp_open_hvbox fmt ctx.indent_incr; (* [val ..._def = new_constant ("...",] *) @@ -1815,58 +1835,92 @@ let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) and {!extract_fun_decl}. *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) - (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = + (global : global_decl) (body : fun_decl) (interface : bool) : unit = assert body.is_global_decl_body; assert (body.signature.inputs = []); - assert (body.signature.generics = empty_generic_params); (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; let name = if !Config.extract_external_name_patterns && not global.is_local then - Some global.name + Some global.llbc_name else None in extract_comment_with_span ctx fmt - [ "[" ^ name_to_string ctx global.name ^ "]" ] + [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ] name global.meta.span; F.pp_print_space fmt (); let decl_name = ctx_get_global global.def_id ctx in let body_name = - ctx_get_function (FromLlbc (Pure.FunId (FRegular global.body), None)) ctx + ctx_get_function (FromLlbc (Pure.FunId (FRegular global.body_id), None)) ctx in - let decl_ty, body_ty = let ty = body.signature.output in if body.signature.fwd_info.effect_info.can_fail then (unwrap_result_ty ty, ty) else (ty, mk_result_ty ty) in + (* Add the type parameters *) + let ctx, type_params, cg_params, trait_clauses = + ctx_add_generic_params global.llbc_name global.llbc_generics global.generics + ctx + in match body.body with | None -> (* No body: only generate a [val x_c : u32] declaration *) let kind = if interface then Declared else Assumed in if !backend = HOL4 then - extract_global_decl_hol4_opaque ctx fmt decl_name decl_ty - else extract_global_decl_body_gen ctx fmt kind decl_name decl_ty None + extract_global_decl_hol4_opaque ctx fmt decl_name global.generics + decl_ty + else + extract_global_decl_body_gen ctx fmt kind decl_name global.generics + type_params cg_params trait_clauses decl_ty None | Some body -> (* There is a body *) (* Generate: [let x_body : result u32 = Return 3] *) - extract_global_decl_body_gen ctx fmt SingleNonRec body_name body_ty + extract_global_decl_body_gen ctx fmt SingleNonRec body_name + global.generics type_params cg_params trait_clauses body_ty (Some (fun fmt -> extract_texpression ctx fmt false body.body)); F.pp_print_break fmt 0 0; (* Generate: [let x_c : u32 = eval_global x_body] *) - extract_global_decl_body_gen ctx fmt SingleNonRec decl_name decl_ty + extract_global_decl_body_gen ctx fmt SingleNonRec decl_name + global.generics type_params cg_params trait_clauses decl_ty (Some (fun fmt -> - let body = + let all_params = [ type_params; cg_params; trait_clauses ] in + let extract_params () = + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + (List.concat all_params) + in + let use_brackets = all_params <> [] in + (* Extract the name *) + let before, after = match !backend with - | FStar | Lean -> "eval_global " ^ body_name - | Coq -> body_name ^ "%global" - | HOL4 -> "get_return_value " ^ body_name + | FStar | Lean -> + ( (fun () -> + F.pp_print_string fmt "eval_global"; + F.pp_print_space fmt ()), + fun () -> () ) + | Coq -> + ((fun () -> ()), fun () -> F.pp_print_string fmt "%global") + | HOL4 -> + ( (fun () -> + F.pp_print_string fmt "get_return_value"; + F.pp_print_space fmt ()), + fun () -> () ) in - F.pp_print_string fmt body)); + before (); + if use_brackets then F.pp_print_string fmt "("; + F.pp_print_string fmt body_name; + (* Extract the generic params *) + extract_params (); + if use_brackets then F.pp_print_string fmt ")"; + (* *) + after ())); (* Add a break to insert lines between declarations *) F.pp_print_break fmt 0 0 @@ -2592,7 +2646,12 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) let item_name = ctx_get_trait_const trait_decl_id name ctx in let ty () = F.pp_print_space fmt (); - F.pp_print_string fmt (ctx_get_global id ctx) + F.pp_print_string fmt (ctx_get_global id ctx); + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + (List.concat [ type_params; cg_params; trait_clauses ]) in extract_trait_impl_item ctx fmt item_name ty) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index eef9e2c9..95a2956b 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -949,9 +949,9 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = | Assign (p, rvalue) -> ( (* We handle global assignments separately *) match rvalue with - | Global gid -> + | Global (gid, generics) -> (* Evaluate the global *) - eval_global config p gid cf ctx + eval_global config p gid generics cf ctx | _ -> (* Evaluate the rvalue *) let cf_eval_rvalue = eval_rvalue_not_global config rvalue in @@ -1021,31 +1021,37 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = (* Compose and apply *) comp cc cf_eval_st cf ctx -and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) : - st_cm_fun = +and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) + (generics : generic_args) : st_cm_fun = fun cf ctx -> let global = ctx_lookup_global_decl ctx gid in match config.mode with | ConcreteMode -> - (* Treat the evaluation of the global as a call to the global body (without arguments) *) - let func = - { - func = FunId (FRegular global.body); - generics = TypesUtils.empty_generic_args; - } - in + (* Treat the evaluation of the global as a call to the global body *) + let func = { func = FunId (FRegular global.body); generics } in let call = { func = FnOpRegular func; args = []; dest } in (eval_transparent_function_call_concrete config global.body call) cf ctx | SymbolicMode -> (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *) assert (ty_no_regions global.ty); - let sval = mk_fresh_symbolic_value global.ty in + (* Instantiate the type *) + (* There shouldn't be any reference to Self *) + let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in + let generics = Subst.generic_args_erase_regions generics in + let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = + Subst.make_subst_from_generics global.generics generics tr_self + in + let ty = + Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self + global.ty + in + let sval = mk_fresh_symbolic_value ty in let cc = assign_to_place config (mk_typed_value_from_symbolic_value sval) dest in let e = cc (cf Unit) ctx in - S.synthesize_global_eval gid sval e + S.synthesize_global_eval gid generics sval e (** Evaluate a switch *) and eval_switch (config : config) (switch : switch) : st_cm_fun = diff --git a/compiler/Pure.ml b/compiler/Pure.ml index a735667e..cf6710aa 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -1087,6 +1087,26 @@ type fun_decl = { } [@@deriving show] +type global_decl = { + meta : meta; + def_id : GlobalDeclId.id; + is_local : bool; + llbc_name : llbc_name; (** The original LLBC name. *) + name : string; + (** We use the name only for printing purposes (for debugging): + the name used at extraction time will be derived from the + llbc_name. + *) + llbc_generics : Types.generic_params; + (** See the comment for [llbc_generics] in fun_decl. *) + generics : generic_params; + preds : predicates; + ty : ty; + kind : item_kind; + body_id : FunDeclId.id; +} +[@@deriving show] + type trait_decl = { def_id : trait_decl_id; is_local : bool; diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index a989fd3b..fc94fa4c 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -208,7 +208,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = get_adt_field_types ctx.type_decls adt_id variant_id adt_generics in List.iter - (fun (fid, fe) -> + (fun ((fid, fe) : _ * texpression) -> let expected_field_ty = FieldId.nth expected_field_tys fid in assert (expected_field_ty = fe.ty); check_texpression ctx fe) @@ -218,7 +218,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = Collections.List.to_cons_nil adt_generics.types in List.iter - (fun (_, fe) -> + (fun ((_, fe) : _ * texpression) -> assert (expected_field_ty = fe.ty); check_texpression ctx fe) supd.updates diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 79c03e58..cc74a16b 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -141,7 +141,7 @@ type expression = The context is the evaluation context from after evaluating the asserted value. It has the same purpose as for the {!Return} case. *) - | EvalGlobal of global_decl_id * symbolic_value * expression + | EvalGlobal of global_decl_id * generic_args * symbolic_value * expression (** Evaluate a global to a fresh symbolic value *) | Assertion of Contexts.eval_ctx * typed_value * expression (** An assertion. diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 27279327..58fb6d04 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1890,7 +1890,8 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = | Panic -> translate_panic ctx | FunCall (call, e) -> translate_function_call call e ctx | EndAbstraction (ectx, abs, e) -> translate_end_abstraction ectx abs e ctx - | EvalGlobal (gid, sv, e) -> translate_global_eval gid sv e ctx + | EvalGlobal (gid, generics, sv, e) -> + translate_global_eval gid generics sv e ctx | Assertion (ectx, v, e) -> translate_assertion ectx v e ctx | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx | IntroSymbolic (ectx, p, sv, v, e) -> @@ -2662,11 +2663,12 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) (* Create the let-binding *) mk_let effect_info.can_fail output call next_e) -and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value) - (e : S.expression) (ctx : bs_ctx) : texpression = +and translate_global_eval (gid : A.GlobalDeclId.id) (generics : T.generic_args) + (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression = let ctx, var = fresh_var_for_symbolic_value sval ctx in let decl = A.GlobalDeclId.Map.find gid ctx.global_ctx.llbc_global_decls in - let global_expr = { id = Global gid; generics = empty_generic_args } in + let generics = ctx_translate_fwd_generic_args ctx generics in + let global_expr = { id = Global gid; generics } in (* We use translate_fwd_ty to translate the global type *) let ty = ctx_translate_fwd_ty ctx decl.ty in let gval = { e = Qualif global_expr; ty } in @@ -3838,3 +3840,40 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) required_methods; provided_methods; } + +let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) : + global_decl = + let { + A.meta; + def_id; + is_local; + name = llbc_name; + generics = llbc_generics; + preds; + ty; + kind; + body = body_id; + } = + decl + in + let name = + Print.Types.name_to_string + (Print.Contexts.decls_ctx_to_fmt_env ctx) + llbc_name + in + let generics = translate_generic_params llbc_generics in + let preds = translate_predicates preds in + let ty = translate_fwd_ty ctx.type_ctx.type_infos ty in + { + meta; + def_id; + is_local; + llbc_name; + name; + llbc_generics; + generics; + preds; + ty; + kind; + body_id; + } diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 20bc107e..a42c43ac 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -119,9 +119,9 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx) FunCall (call, e)) e -let synthesize_global_eval (gid : GlobalDeclId.id) (dest : symbolic_value) - (e : expression option) : expression option = - Option.map (fun e -> EvalGlobal (gid, dest, e)) e +let synthesize_global_eval (gid : GlobalDeclId.id) (generics : generic_args) + (dest : symbolic_value) (e : expression option) : expression option = + Option.map (fun e -> EvalGlobal (gid, generics, dest, e)) e let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref) (call_id : FunCallId.id) (ctx : Contexts.eval_ctx) (sg : fun_sig) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index fba1dfb0..9af3c71b 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -469,6 +469,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) groups are always singletons, so the [extract_global_decl] function takes care of generating the delimiters. *) + let global = SymbolicToPure.translate_global ctx.trans_ctx global in Extract.extract_global_decl ctx fmt global body config.interface (** Utility. |