diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Extract.ml | 131 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 49 | ||||
| -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 |
9 files changed, 210 insertions, 82 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index a93ed6e4..aa097a4f 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,13 +329,15 @@ 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 -> extract_field_projector ctx fmt inside app proj qualif.generics args | TraitConst (trait_ref, const_name) -> - extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref; + extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref; let name = ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id const_name ctx @@ -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,94 @@ 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 = + List.concat [ 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) + 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 @@ -2585,18 +2641,39 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) * Extract the items *) let trait_decl_id = impl.impl_trait.trait_decl_id in + let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in + let trait_decl_provided_consts = + List.map (fun (_, (_, x)) -> x) trait_decl.consts + in (* The constants *) List.iter - (fun (name, (_, id)) -> + (fun (provided_id, (name, (_, id))) -> let item_name = ctx_get_trait_const trait_decl_id name ctx in + (* The parameters are not the same depending on whether the constant + is a provided constant or not *) + let print_params () = + if provided_id = Some id then + extract_generic_args ctx fmt TypeDeclId.Set.empty + impl.impl_trait.decl_generics + else + let all_params = + List.concat [ type_params; cg_params; trait_clauses ] + in + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + all_params + 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); + print_params () in extract_trait_impl_item ctx fmt item_name ty) - impl.consts; + (List.combine trait_decl_provided_consts impl.consts); (* The types *) List.iter diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index dc100fe3..afbf4605 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -1,6 +1,5 @@ open Types open Values -open LlbcAst open Scalars open Expressions open Utils @@ -264,37 +263,23 @@ let eval_operand_no_reorganize (config : config) (op : operand) | CLiteral lit -> cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx | CTraitConst (trait_ref, const_name) -> ( - match trait_ref.trait_id with - | TraitImpl _ -> - (* This shouldn't happen: if we refer to a concrete implementation, we - should directly refer to the top-level constant *) - raise (Failure "Unreachable") - | _ -> ( - (* We refer to a constant defined in a local clause: simply - introduce a fresh symbolic value *) - let ctx0 = ctx in - (* Lookup the trait declaration to retrieve the type of the symbolic value *) - let trait_decl = - ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id - in - let _, (ty, _) = - List.find (fun (name, _) -> name = const_name) trait_decl.consts - in - (* Introduce a fresh symbolic value *) - let v = mk_fresh_symbolic_typed_value ty in - (* Continue the evaluation *) - let e = cf v ctx in - (* We have to wrap the generated expression *) - match e with - | None -> None - | Some e -> - Some - (SymbolicAst.IntroSymbolic - ( ctx0, - None, - value_as_symbolic v.value, - SymbolicAst.VaTraitConstValue (trait_ref, const_name), - e )))) + let ctx0 = ctx in + (* Simply introduce a fresh symbolic value *) + let ty = cv.ty in + let v = mk_fresh_symbolic_typed_value ty in + (* Continue the evaluation *) + let e = cf v ctx in + (* Wrap the generated expression *) + match e with + | None -> None + | Some e -> + Some + (SymbolicAst.IntroSymbolic + ( ctx0, + None, + value_as_symbolic v.value, + SymbolicAst.VaTraitConstValue (trait_ref, const_name), + e ))) | CVar vid -> ( let ctx0 = ctx in (* In concrete mode: lookup the const generic value. 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. |