summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/AssociatedTypes.ml4
-rw-r--r--compiler/Contexts.ml13
-rw-r--r--compiler/Interpreter.ml64
-rw-r--r--compiler/InterpreterStatements.ml7
-rw-r--r--compiler/InterpreterUtils.ml2
-rw-r--r--compiler/Logging.ml3
-rw-r--r--compiler/Print.ml4
7 files changed, 81 insertions, 16 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index bce0fb11..92cd464e 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -136,7 +136,7 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty =
("ctx_normalize_ty: trait type: " ^ ctx.ty_to_string ty
^ "\n- trait_ref: "
^ ctx.trait_ref_to_string trait_ref
- ^ "\n- raw trait ref: "
+ ^ "\n- raw trait ref:\n"
^ T.show_trait_ref ctx.pp_r trait_ref));
(* Normalize and attempt to project the type from the trait ref *)
let trait_ref = ctx_normalize_trait_ref ctx trait_ref in
@@ -197,7 +197,7 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty =
("ctx_normalize_ty: trait type: not a trait ref: "
^ ctx.ty_to_string ty ^ "\n- trait_ref: "
^ ctx.trait_ref_to_string trait_ref
- ^ "\n- raw trait ref: "
+ ^ "\n- raw trait ref:\n"
^ T.show_trait_ref ctx.pp_r trait_ref));
(* We can't project *)
assert (trait_instance_id_is_local_clause trait_ref.trait_id);
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index df77959e..65760d94 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -5,6 +5,7 @@ open LlbcAst
module V = Values
open ValuesUtils
open Identifiers
+module L = Logging
(** The [Id] module for dummy variables.
@@ -17,6 +18,9 @@ IdGen ()
type dummy_var_id = DummyVarId.id [@@deriving show, ord]
+(** The local logger *)
+let log = L.contexts_log
+
(** Some global counters.
Note that those counters were initially stored in {!eval_ctx} values,
@@ -449,6 +453,15 @@ let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
*)
let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
=
+ log#ldebug
+ (lazy
+ ("push_vars:\n"
+ ^ String.concat "\n"
+ (List.map
+ (fun (var, value) ->
+ (* We can unfortunately not use Print because it depends on Contexts... *)
+ show_var var ^ " -> " ^ V.show_typed_value value)
+ vars)));
assert (
List.for_all
(fun (var, (value : typed_value)) -> var.var_ty = value.ty)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index b5e9fcb9..4ce6dae8 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -64,15 +64,39 @@ let initialize_eval_context (ctx : C.decls_ctx)
C.ended_regions = T.RegionId.Set.empty;
}
-(** Instantiate a function signature for a symbolic execution *)
-let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (fdef : A.fun_decl) :
+(** Small helper.
+
+ Normalize an instantiated function signature provided we used this signature
+ to compute a normalization map (for the associated types) and that we added
+ it in the context.
+ *)
+let normalize_inst_fun_sig (ctx : C.eval_ctx) (sg : A.inst_fun_sig) :
A.inst_fun_sig =
+ let { A.regions_hierarchy = _; trait_type_constraints = _; inputs; output } =
+ sg
+ in
+ let norm = AssociatedTypes.ctx_normalize_rty ctx in
+ let inputs = List.map norm inputs in
+ let output = norm output in
+ { sg with A.inputs; output }
+
+(** Instantiate a function signature for a symbolic execution.
+
+ We return a new context because we compute and add the type normalization
+ map in the same step.
+
+ **WARNING**: this doesn't normalize the types. This step has to be done
+ separately. Remark: we need to normalize essentially because of the where
+ clauses (we are not considering a function call, so we don't need to
+ normalize because a trait clause was instantiated with a specific trait ref).
+ *)
+let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (fdef : A.fun_decl) :
+ C.eval_ctx * A.inst_fun_sig =
let sg = fdef.signature in
let tr_self =
match fdef.kind with
| RegularKind | TraitMethodImpl _ -> T.UnknownTrait __FUNCTION__
- | TraitMethodDecl _ | TraitMethodProvided _ ->
- raise (Failure "Unimplemented")
+ | TraitMethodDecl _ | TraitMethodProvided _ -> T.Self
in
let generics =
let { T.regions; types; const_generics; trait_clauses } = sg.generics in
@@ -98,12 +122,27 @@ let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (fdef : A.fun_decl) :
let { T.trait_id = trait_decl_id; generics; _ } = c in
let generics = Subst.generic_args_substitute subst generics in
let trait_decl_ref = { T.trait_decl_id; decl_generics = generics } in
- { T.trait_id = T.Clause c.clause_id; generics; trait_decl_ref })
+ (* Note that because we directly refer to the clause, we give it
+ empty generics *)
+ {
+ T.trait_id = T.Clause c.clause_id;
+ generics = TypesUtils.mk_empty_generic_args;
+ trait_decl_ref;
+ })
trait_clauses
in
{ T.regions; types; const_generics; trait_refs }
in
- instantiate_fun_sig ctx generics tr_self sg
+ let inst_sg = instantiate_fun_sig ctx generics tr_self sg in
+ (* Compute the normalization maps *)
+ let ctx =
+ AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx
+ inst_sg.trait_type_constraints
+ in
+ (* Normalize the signature *)
+ let inst_sg = normalize_inst_fun_sig ctx inst_sg in
+ (* Return *)
+ (ctx, inst_sg)
(** Initialize an evaluation context to execute a function.
@@ -140,13 +179,10 @@ let initialize_symbolic_context_for_fun (ctx : C.decls_ctx) (fdef : A.fun_decl)
initialize_eval_context ctx region_groups sg.generics.types
sg.generics.const_generics
in
- (* Instantiate the signature *)
- let inst_sg = symbolic_instantiate_fun_sig ctx fdef in
- (* Compute the normalization maps *)
- let ctx =
- AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx
- inst_sg.trait_type_constraints
- in
+ (* Instantiate the signature. This updates the context because we compute
+ at the same time the normalization map for the associated types.
+ *)
+ let ctx, inst_sg = symbolic_instantiate_fun_sig ctx fdef in
(* Create fresh symbolic values for the inputs *)
let input_svs =
List.map (fun ty -> mk_fresh_symbolic_value V.SynthInput ty) inst_sg.inputs
@@ -221,7 +257,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
* an instantiation of the signature, so that we use fresh
* region ids for the return abstractions. *)
let sg = fdef.signature in
- let ret_inst_sg = symbolic_instantiate_fun_sig ctx fdef in
+ let _, ret_inst_sg = symbolic_instantiate_fun_sig ctx fdef in
let ret_rty = ret_inst_sg.output in
(* Move the return value out of the return variable *)
let pop_return_value = is_regular_return in
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 97fb80f4..88e20a92 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -664,6 +664,13 @@ let eval_assumed_function_call_concrete (config : C.config)
let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.egeneric_args)
(tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
+ log#ldebug
+ (lazy
+ ("instantiate_fun_sig:" ^ "\n- generics: "
+ ^ egeneric_args_to_string ctx generics
+ ^ "\n- tr_self: "
+ ^ rtrait_instance_id_to_string ctx tr_self
+ ^ "\n- sg: " ^ fun_sig_to_string ctx sg));
(* Generate fresh abstraction ids and create a substitution from region
* group ids to abstraction ids *)
let rg_abs_ids_bindings =
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 8525be29..6fde8d68 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -39,6 +39,8 @@ let typed_avalue_to_string = PA.typed_avalue_to_string
let place_to_string = PA.place_to_string
let operand_to_string = PA.operand_to_string
let egeneric_args_to_string = PA.egeneric_args_to_string
+let rtrait_instance_id_to_string = PA.rtrait_instance_id_to_string
+let fun_sig_to_string = PA.fun_sig_to_string
let fun_decl_to_string = PA.fun_decl_to_string
let call_to_string = PA.call_to_string
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index d0f5b0c5..59abbfc7 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -9,6 +9,9 @@ let pre_passes_log = L.get_logger "MainLogger.PrePasses"
(** Logger for Translate *)
let translate_log = L.get_logger "MainLogger.Translate"
+(** Logger for Contexts *)
+let contexts_log = L.get_logger "MainLogger.Contexts"
+
(** Logger for PureUtils *)
let pure_utils_log = L.get_logger "MainLogger.PureUtils"
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 93a1f970..522d9fdd 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -732,6 +732,10 @@ module EvalCtxLlbcAst = struct
let fmt = PC.eval_ctx_to_ast_formatter ctx in
PA.fun_decl_to_string fmt "" " " f
+ let fun_sig_to_string (ctx : C.eval_ctx) (x : A.fun_sig) : string =
+ let fmt = PC.eval_ctx_to_ast_formatter ctx in
+ PA.fun_sig_to_string fmt "" " " x
+
let statement_to_string (ctx : C.eval_ctx) (indent : string)
(indent_incr : string) (e : A.statement) : string =
let fmt = PC.eval_ctx_to_ast_formatter ctx in
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 19:42:46 +0000