summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml131
-rw-r--r--compiler/InterpreterExpressions.ml49
-rw-r--r--compiler/InterpreterStatements.ml32
-rw-r--r--compiler/Pure.ml20
-rw-r--r--compiler/PureTypeCheck.ml4
-rw-r--r--compiler/SymbolicAst.ml2
-rw-r--r--compiler/SymbolicToPure.ml47
-rw-r--r--compiler/SynthesizeSymbolic.ml6
-rw-r--r--compiler/Translate.ml1
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.