summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml12
-rw-r--r--compiler/FunsAnalysis.ml6
-rw-r--r--compiler/InterpreterBorrows.ml29
-rw-r--r--compiler/InterpreterBorrowsCore.ml2
-rw-r--r--compiler/InterpreterLoopsCore.ml7
-rw-r--r--compiler/InterpreterLoopsJoinCtxs.ml10
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml41
-rw-r--r--compiler/InterpreterPaths.ml2
-rw-r--r--compiler/InterpreterProjectors.ml32
-rw-r--r--compiler/PrePasses.ml2
-rw-r--r--compiler/PureMicroPasses.ml1
-rw-r--r--compiler/SymbolicToPure.ml221
-rw-r--r--compiler/Translate.ml1
13 files changed, 172 insertions, 194 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index d6a5f0fc..1f9c9117 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -509,8 +509,6 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx)
| Error (types, err) ->
extract_generic_args meta ctx fmt TypeDeclId.Set.empty
{ generics with types };
- (* if !Config.fail_hard then craise __FILE__ __LINE__ meta err
- else *)
save_error __FILE__ __LINE__ (Some meta) err;
F.pp_print_string fmt
"(\"ERROR: ill-formed builtin: invalid number of filtering \
@@ -1876,8 +1874,8 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx)
let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
(global : global_decl) (body : fun_decl) (interface : bool) : unit =
let meta = body.meta in
- sanity_check __FILE__ __LINE__ body.is_global_decl_body body.meta;
- sanity_check __FILE__ __LINE__ (body.signature.inputs = []) body.meta;
+ sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
+ sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta;
(* Add a break then the name of the corresponding LLBC declaration *)
F.pp_print_break fmt 0 0;
@@ -2232,7 +2230,8 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
cassert __FILE__ __LINE__
(trait_impl.provided_methods = [])
trait_impl.meta
- ("Overriding provided methods is not supported yet (overriden methods: "
+ ("Overriding trait provided methods in trait implementations is not \
+ supported yet (overriden methods: "
^ String.concat ", " (List.map fst trait_impl.provided_methods)
^ ")");
(* Everything is taken care of by {!extract_trait_decl_register_names} *but*
@@ -2622,8 +2621,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
in
extract_trait_impl_item ctx fmt fun_name ty
-(** Extract a trait implementation
-*)
+(** Extract a trait implementation *)
let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(impl : trait_impl) : unit =
log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name));
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index cad469f9..f194d4e5 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -119,7 +119,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
method! visit_Call env call =
(match call.func with
| FnOpMove _ ->
- (* Ignoring this: we lookup t he called function upon creating
+ (* Ignoring this: we lookup the called function upon creating
the closure *)
()
| FnOpRegular func -> (
@@ -145,9 +145,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
end
in
(* Sanity check: global bodies don't contain stateful calls *)
- sanity_check __FILE__ __LINE__
+ cassert __FILE__ __LINE__
((not f.is_global_decl_body) || not !stateful)
- f.meta;
+ f.meta "Global definition containing a stateful call in its body";
let builtin_info = get_builtin_info f in
let has_builtin_info = builtin_info <> None in
group_has_builtin_info := !group_has_builtin_info || has_builtin_info;
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index b32261e6..e593ae75 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -443,8 +443,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
(* Explore the environment *)
let ctx = obj#visit_eval_ctx None ctx in
(* Check we gave back to exactly one loan *)
- cassert __FILE__ __LINE__ !replaced meta
- "Only one loan should have been given back";
+ cassert __FILE__ __LINE__ !replaced meta "No loan updated";
(* Apply the reborrows *)
apply_registered_reborrows ctx
@@ -503,7 +502,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
let replaced : bool ref = ref false in
let set_replaced () =
cassert __FILE__ __LINE__ (not !replaced) meta
- "Only one loan should have been updated";
+ "Exacly one loan should be updated";
replaced := true
in
let obj =
@@ -589,7 +588,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
(* Explore the environment *)
let ctx = obj#visit_eval_ctx None ctx in
(* Check we gave back to exactly one loan *)
- cassert __FILE__ __LINE__ !replaced meta "Only one loan should be given back";
+ cassert __FILE__ __LINE__ !replaced meta "No loan updated";
(* Return *)
ctx
@@ -608,7 +607,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
let replaced : bool ref = ref false in
let set_replaced () =
cassert __FILE__ __LINE__ (not !replaced) meta
- "Only one loan should be updated";
+ "Exactly one loan should be updated";
replaced := true
in
let obj =
@@ -673,8 +672,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
(* Explore the environment *)
let ctx = obj#visit_eval_ctx None ctx in
(* Check we gave back to exactly one loan *)
- cassert __FILE__ __LINE__ !replaced meta
- "Exactly one loan should be given back";
+ cassert __FILE__ __LINE__ !replaced meta "No loan updated";
(* Return *)
ctx
@@ -1553,8 +1551,8 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
(* I don't think it is possible to have two-phase borrows involving borrows
* returned by abstractions. I'm not sure how we could handle that anyway. *)
craise __FILE__ __LINE__ meta
- "Can't promote a shared loan to a mutable loan if the loan is inside \
- an abstraction"
+ "Can't promote a shared loan to a mutable loan if the loan is inside a \
+ region abstraction"
(** Helper function: see {!activate_reserved_mut_borrow}.
@@ -1581,7 +1579,7 @@ let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id)
(* This can't happen for sure *)
craise __FILE__ __LINE__ meta
"Can't promote a shared borrow to a mutable borrow if the borrow is \
- inside an abstraction"
+ inside a region abstraction"
in
(* Continue *)
cf ctx
@@ -1647,7 +1645,7 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta)
* returned by abstractions. I'm not sure how we could handle that anyway. *)
craise __FILE__ __LINE__ meta
"Can't activate a reserved mutable borrow referencing a loan inside\n\
- \ an abstraction"
+ \ a region abstraction"
let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
(destructure_shared_values : bool) (ctx : eval_ctx) (abs0 : abs) : abs =
@@ -2272,12 +2270,11 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
(* Sanity check: there is no loan/borrows which appears in both abstractions,
unless we allow to merge duplicates *)
- if merge_funs = None then
- (sanity_check __FILE__ __LINE__
- (BorrowId.Set.disjoint borrows0 borrows1)
- meta;
- sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1))
+ if merge_funs = None then (
+ sanity_check __FILE__ __LINE__
+ (BorrowId.Set.disjoint borrows0 borrows1)
meta;
+ sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) meta);
(* Merge.
There are several cases:
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 92d8670a..6e65b11d 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -864,7 +864,7 @@ let update_intersecting_aproj_borrows (meta : Meta.meta)
let ctx = obj#visit_eval_ctx None ctx in
(* Check that we updated the context at least once *)
cassert __FILE__ __LINE__ (Option.is_some !shared) meta
- "Context was not updated at least once";
+ "Context was not updated";
(* Return *)
ctx
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 2283e842..a5b3a021 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -256,12 +256,12 @@ module type PrimMatcher = sig
end
module type Matcher = sig
+ val meta : Meta.meta
+
(** Match two values.
Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}.
*)
- val meta : Meta.meta
-
val match_typed_values :
eval_ctx -> eval_ctx -> typed_value -> typed_value -> typed_value
@@ -279,6 +279,8 @@ end
Very annoying: functors only take modules as inputs...
*)
module type MatchCheckEquivState = sig
+ val meta : Meta.meta
+
(** [true] if we check equivalence between contexts, [false] if we match
a source context with a target context. *)
val check_equiv : bool
@@ -299,7 +301,6 @@ module type MatchCheckEquivState = sig
val aid_map : AbstractionId.InjSubst.t ref
val lookup_shared_value_in_ctx0 : BorrowId.id -> typed_value
val lookup_shared_value_in_ctx1 : BorrowId.id -> typed_value
- val meta : Meta.meta
end
module type CheckEquivMatcher = sig
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index d97b05d0..de00cb93 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -491,8 +491,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
are not in the prefix anymore *)
if DummyVarId.Set.mem b0 fixed_ids.dids then (
(* Still in the prefix: match the values *)
- cassert __FILE__ __LINE__ (b0 = b1) meta
- "Bindings are not the same. We are not in the prefix anymore";
+ sanity_check __FILE__ __LINE__ (b0 = b1) meta;
let b = b0 in
let v = M.match_typed_values ctx0 ctx1 v0 v1 in
let var = EBinding (BDummy b, v) in
@@ -514,9 +513,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
(* Variable bindings *must* be in the prefix and consequently their
ids must be the same *)
- cassert __FILE__ __LINE__ (b0 = b1) meta
- "Variable bindings *must* be in the prefix and consequently their\n\
- \ ids must be the same";
+ sanity_check __FILE__ __LINE__ (b0 = b1) meta;
(* Match the values *)
let b = b0 in
let v = M.match_typed_values ctx0 ctx1 v0 v1 in
@@ -537,8 +534,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
(* Same as for the dummy values: there are two cases *)
if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
(* Still in the prefix: the abstractions must be the same *)
- cassert __FILE__ __LINE__ (abs0 = abs1) meta
- "The abstractions are not the same";
+ sanity_check __FILE__ __LINE__ (abs0 = abs1) meta;
(* Continue *)
abs :: join_prefixes env0' env1')
else (* Not in the prefix anymore *)
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index bd271ff4..e710ed2b 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -827,13 +827,13 @@ end
(* Very annoying: functors only take modules as inputs... *)
module type MatchMoveState = sig
+ val meta : Meta.meta
+
(** The current loop *)
val loop_id : LoopId.id
(** The moved values *)
val nvalues : typed_value list ref
-
- val meta : Meta.meta
end
(* We use this matcher to move values in environment.
@@ -853,9 +853,9 @@ end
indeed matches the resulting target environment: it will be re-checked later.
*)
module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
- (** Small utility *)
let meta = S.meta
+ (** Small utility *)
let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues
let match_etys _ _ ty0 ty1 =
@@ -959,6 +959,8 @@ end
module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher =
struct
+ let meta = S.meta
+
module MkGetSetM (Id : Identifiers.Id) = struct
module Inj = Id.InjSubst
@@ -1001,8 +1003,6 @@ struct
(match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1))
end
- let meta = S.meta
-
module GetSetRid = MkGetSetM (RegionId)
let match_rid = GetSetRid.match_e "match_rid: " S.rid_map
@@ -1383,15 +1383,15 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
| EBinding (BDummy b0, v0) :: env0', EBinding (BDummy b1, v1) :: env1' ->
(* Sanity check: if the dummy value is an old value, the bindings must
be the same and their values equal (and the borrows/loans/symbolic *)
- if DummyVarId.Set.mem b0 fixed_ids.dids then
- ((* Fixed values: the values must be equal *)
- sanity_check __FILE__ __LINE__ (b0 = b1) meta;
- sanity_check __FILE__ __LINE__ (v0 = v1) meta;
- (* The ids present in the left value must be fixed *)
- let ids, _ = compute_typed_value_ids v0 in
- sanity_check __FILE__ __LINE__
- ((not S.check_equiv) || ids_are_fixed ids))
- meta;
+ if DummyVarId.Set.mem b0 fixed_ids.dids then (
+ (* Fixed values: the values must be equal *)
+ sanity_check __FILE__ __LINE__ (b0 = b1) meta;
+ sanity_check __FILE__ __LINE__ (v0 = v1) meta;
+ (* The ids present in the left value must be fixed *)
+ let ids, _ = compute_typed_value_ids v0 in
+ sanity_check __FILE__ __LINE__
+ ((not S.check_equiv) || ids_are_fixed ids)
+ meta);
(* We still match the values - allows to compute mappings (which
are the identity actually) *)
let _ = M.match_typed_values ctx0 ctx1 v0 v1 in
@@ -1457,9 +1457,16 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
}
in
Some maps
- with Distinct msg ->
- log#ldebug (lazy ("match_ctxs: distinct: " ^ msg));
- None
+ with
+ | Distinct msg ->
+ log#ldebug (lazy ("match_ctxs: distinct: " ^ msg ^ "\n"));
+ None
+ | ValueMatchFailure k ->
+ log#ldebug
+ (lazy
+ ("match_ctxs: distinct: ValueMatchFailure" ^ show_updt_env_kind k
+ ^ "\n"));
+ None
let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets)
(ctx0 : eval_ctx) (ctx1 : eval_ctx) : bool =
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 93e56106..f2c0bcb1 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -483,7 +483,7 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta)
(Some (Synth.mk_mplace meta prefix ctx))
| FailBottom (_, _, _) ->
(* We can't expand {!Bottom} values while reading them *)
- craise __FILE__ __LINE__ meta "Found [Bottom] while reading a place"
+ craise __FILE__ __LINE__ meta "Found bottom while reading a place"
| FailBorrow _ ->
craise __FILE__ __LINE__ meta "Could not read a borrow"
in
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 8b6eeb6c..6e86e6a4 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -199,22 +199,22 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
| VSymbolic s, _ ->
(* Check that the projection doesn't contain already ended regions,
* if necessary *)
- if check_symbolic_no_ended then
- (let ty1 = s.sv_ty in
- let rset1 = ctx.ended_regions in
- let ty2 = ty in
- let rset2 = regions in
- log#ldebug
- (lazy
- ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1
- ^ "\n- rset1: "
- ^ RegionId.Set.to_string None rset1
- ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
- ^ RegionId.Set.to_string None rset2
- ^ "\n"));
- sanity_check __FILE__ __LINE__
- (not (projections_intersect meta ty1 rset1 ty2 rset2)))
- meta;
+ if check_symbolic_no_ended then (
+ let ty1 = s.sv_ty in
+ let rset1 = ctx.ended_regions in
+ let ty2 = ty in
+ let rset2 = regions in
+ log#ldebug
+ (lazy
+ ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1
+ ^ "\n- rset1: "
+ ^ RegionId.Set.to_string None rset1
+ ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
+ ^ RegionId.Set.to_string None rset2
+ ^ "\n"));
+ sanity_check __FILE__ __LINE__
+ (not (projections_intersect meta ty1 rset1 ty2 rset2))
+ meta);
ASymbolic (AProjBorrows (s, ty))
| _ ->
log#lerror
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 11cd89fc..0b39f64a 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -402,8 +402,8 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl =
let check_visitor =
object
inherit [_] iter_statement as super
- (* Remember the span of the statement we enter *)
+ (* Remember the span of the statement we enter *)
method! visit_statement _ st = super#visit_statement st.meta st
method! visit_var_id meta id =
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 12b3387a..9fa07029 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1989,6 +1989,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
(List.concat (List.map (fun { f; loops } -> [ f :: loops ]) transl))
in
let subgroups = ReorderDecls.group_reorder_fun_decls all_decls in
+
log#ldebug
(lazy
("filter_loop_inputs: all_decls:\n\n"
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4830f65a..0c30f44c 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -144,6 +144,7 @@ type loop_info = {
(** Body synthesis context *)
type bs_ctx = {
(* TODO: there are a lot of duplications with the various decls ctx *)
+ meta : Meta.meta; (** The meta information about the current declaration *)
decls_ctx : C.decls_ctx;
type_ctx : type_ctx;
fun_ctx : fun_ctx;
@@ -325,7 +326,7 @@ let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string =
let env = bs_ctx_to_fmt_env ctx in
- Print.Values.typed_value_to_string ~meta:(Some ctx.fun_decl.meta) env v
+ Print.Values.typed_value_to_string ~meta:(Some ctx.meta) env v
let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string =
let env = bs_ctx_to_pure_fmt_env ctx in
@@ -349,8 +350,7 @@ let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
let texpression_to_string (ctx : bs_ctx) (e : texpression) : string =
let env = bs_ctx_to_pure_fmt_env ctx in
- PrintPure.texpression_to_string ~metadata:(Some ctx.fun_decl.meta) env false
- "" " " e
+ PrintPure.texpression_to_string ~metadata:(Some ctx.meta) env false "" " " e
let fun_id_to_string (ctx : bs_ctx) (id : A.fun_id) : string =
let env = bs_ctx_to_fmt_env ctx in
@@ -364,10 +364,9 @@ let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
let env = bs_ctx_to_pure_fmt_env ctx in
PrintPure.fun_decl_to_string env def
-let typed_pattern_to_string ?(meta : Meta.meta option = None) (ctx : bs_ctx)
- (p : Pure.typed_pattern) : string =
+let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string =
let env = bs_ctx_to_pure_fmt_env ctx in
- PrintPure.typed_pattern_to_string ~meta env p
+ PrintPure.typed_pattern_to_string ~meta:(Some ctx.meta) env p
let ctx_get_effect_info_for_bid (ctx : bs_ctx) (bid : RegionGroupId.id option) :
fun_effect_info =
@@ -386,7 +385,7 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
let verbose = false in
let indent = "" in
let indent_incr = " " in
- Print.Values.abs_to_string ~meta:(Some ctx.fun_decl.meta) env verbose indent
+ Print.Values.abs_to_string ~meta:(Some ctx.meta) env verbose indent
indent_incr abs
let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
@@ -676,13 +675,13 @@ and translate_fwd_trait_instance_id (meta : Meta.meta) (type_infos : type_infos)
(** Simply calls [translate_fwd_ty] *)
let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty =
let type_infos = ctx.type_ctx.type_infos in
- translate_fwd_ty ctx.fun_decl.meta type_infos ty
+ translate_fwd_ty ctx.meta type_infos ty
(** Simply calls [translate_fwd_generic_args] *)
let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
generic_args =
let type_infos = ctx.type_ctx.type_infos in
- translate_fwd_generic_args ctx.fun_decl.meta type_infos generics
+ translate_fwd_generic_args ctx.meta type_infos generics
(** Translate a type, when some regions may have ended.
@@ -775,7 +774,7 @@ let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos)
let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
(inside_mut : bool) (ty : T.ty) : ty option =
let type_infos = ctx.type_ctx.type_infos in
- translate_back_ty ctx.fun_decl.meta type_infos keep_region inside_mut ty
+ translate_back_ty ctx.meta type_infos keep_region inside_mut ty
let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
let const_generics =
@@ -794,14 +793,14 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
}
let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
- let meta = ctx.fun_decl.meta in
+ let meta = ctx.meta in
let ctx = mk_type_check_ctx ctx in
let _ = PureTypeCheck.check_typed_pattern meta ctx v in
()
let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
if !Config.type_check_pure_code then
- let meta = ctx.fun_decl.meta in
+ let meta = ctx.meta in
let ctx = mk_type_check_ctx ctx in
PureTypeCheck.check_texpression meta ctx e
@@ -811,9 +810,7 @@ let translate_fun_id_or_trait_method_ref (ctx : bs_ctx)
| FunId fun_id -> FunId fun_id
| TraitMethod (trait_ref, method_name, fun_decl_id) ->
let type_infos = ctx.type_ctx.type_infos in
- let trait_ref =
- translate_fwd_trait_ref ctx.fun_decl.meta type_infos trait_ref
- in
+ let trait_ref = translate_fwd_trait_ref ctx.meta type_infos trait_ref in
TraitMethod (trait_ref, method_name, fun_decl_id)
let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
@@ -823,7 +820,7 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
let calls = ctx.calls in
sanity_check __FILE__ __LINE__
(not (V.FunCallId.Map.mem call_id calls))
- ctx.fun_decl.meta;
+ ctx.meta;
let info = { forward; forward_inputs = args; back_funs } in
let calls = V.FunCallId.Map.add call_id info calls in
{ ctx with calls }
@@ -847,7 +844,7 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
let abstractions = ctx.abstractions in
sanity_check __FILE__ __LINE__
(not (V.AbstractionId.Map.mem abs.abs_id abstractions))
- ctx.fun_decl.meta;
+ ctx.meta;
let abstractions =
V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions
in
@@ -953,22 +950,20 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref)
in
{ info with is_rec = info.is_rec || Option.is_some lid }
| FunId (FAssumed _) ->
- compute_raw_fun_effect_info ctx.fun_decl.meta ctx.fun_ctx.fun_infos
- fun_id lid gid)
+ compute_raw_fun_effect_info ctx.meta ctx.fun_ctx.fun_infos fun_id lid
+ gid)
| Some lid -> (
(* This is necessarily for the current function *)
match fun_id with
| FunId (FRegular fid) -> (
- sanity_check __FILE__ __LINE__
- (fid = ctx.fun_decl.def_id)
- ctx.fun_decl.meta;
+ sanity_check __FILE__ __LINE__ (fid = ctx.fun_decl.def_id) ctx.meta;
(* Lookup the loop *)
let lid = V.LoopId.Map.find lid ctx.loop_ids_map in
let loop_info = LoopId.Map.find lid ctx.loops in
match gid with
| None -> loop_info.fwd_effect_info
| Some gid -> RegionGroupId.Map.find gid loop_info.back_effect_infos)
- | _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable")
+ | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable")
(** Translate a function signature to a decomposed function signature.
@@ -1514,7 +1509,7 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
match V.SymbolicValueId.Map.find_opt sv.sv_id ctx.sv_to_var with
| Some v -> v
| None ->
- craise __FILE__ __LINE__ ctx.fun_decl.meta
+ craise __FILE__ __LINE__ ctx.meta
("Could not find var for symbolic value: "
^ V.SymbolicValueId.to_string sv.sv_id)
@@ -1564,7 +1559,7 @@ let symbolic_value_to_texpression (ctx : bs_ctx) (sv : V.symbolic_value) :
let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
(v : V.typed_value) : texpression =
(* We need to ignore boxes *)
- let v = unbox_typed_value ctx.fun_decl.meta v in
+ let v = unbox_typed_value ctx.meta v in
let translate = typed_value_to_texpression ctx ectx in
(* Translate the type *)
let ty = ctx_translate_fwd_ty ctx v.ty in
@@ -1578,12 +1573,12 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
(* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
match v.ty with
| TAdt (TTuple, _) ->
- sanity_check __FILE__ __LINE__ (variant_id = None) ctx.fun_decl.meta;
- mk_simpl_tuple_texpression ctx.fun_decl.meta field_values
+ sanity_check __FILE__ __LINE__ (variant_id = None) ctx.meta;
+ mk_simpl_tuple_texpression ctx.meta field_values
| _ ->
(* Retrieve the type and the translated generics from the translated
type (simpler this way) *)
- let adt_id, generics = ty_as_adt ctx.fun_decl.meta ty in
+ let adt_id, generics = ty_as_adt ctx.meta ty in
(* Create the constructor *)
let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in
let qualif = { id = qualif_id; generics } in
@@ -1594,20 +1589,18 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
let cons_ty = mk_arrows field_tys ty in
let cons = { e = cons_e; ty = cons_ty } in
(* Apply the constructor *)
- mk_apps ctx.fun_decl.meta cons field_values)
- | VBottom -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ mk_apps ctx.meta cons field_values)
+ | VBottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
| VLoan lc -> (
match lc with
| VSharedLoan (_, v) -> translate v
- | VMutLoan _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
- )
+ | VMutLoan _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable")
| VBorrow bc -> (
match bc with
| VSharedBorrow bid ->
(* Lookup the shared value in the context, and continue *)
let sv =
- InterpreterBorrowsCore.lookup_shared_value ctx.fun_decl.meta ectx
- bid
+ InterpreterBorrowsCore.lookup_shared_value ctx.meta ectx bid
in
translate sv
| VReservedMutBorrow bid ->
@@ -1615,8 +1608,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
* only in *meta-data*: a value *actually used* in the translation can't come
* from an unpromoted reserved borrow *)
let sv =
- InterpreterBorrowsCore.lookup_shared_value ctx.fun_decl.meta ectx
- bid
+ InterpreterBorrowsCore.lookup_shared_value ctx.meta ectx bid
in
translate sv
| VMutBorrow (_, v) ->
@@ -1663,7 +1655,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
| TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
- cassert __FILE__ __LINE__ (field_values = []) ctx.fun_decl.meta
+ cassert __FILE__ __LINE__ (field_values = []) ctx.meta
"ADTs containing borrows are not supported yet";
None
| TTuple ->
@@ -1672,11 +1664,9 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
else
(* Note that if there is exactly one field value,
* [mk_simpl_tuple_rvalue] is the identity *)
- let rv =
- mk_simpl_tuple_texpression ctx.fun_decl.meta field_values
- in
+ let rv = mk_simpl_tuple_texpression ctx.meta field_values in
Some rv)
- | ABottom -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ | ABottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
| ALoan lc -> aloan_content_to_consumed ctx ectx lc
| ABorrow bc -> aborrow_content_to_consumed ctx bc
| ASymbolic aproj -> aproj_to_consumed ctx aproj
@@ -1694,7 +1684,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
(lc : V.aloan_content) : texpression option =
match lc with
| AMutLoan (_, _) | ASharedLoan (_, _, _) ->
- craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ craise __FILE__ __LINE__ ctx.meta "Unreachable"
| AEndedMutLoan { child = _; given_back = _; given_back_meta } ->
(* Return the meta-value *)
Some (typed_value_to_texpression ctx ectx given_back_meta)
@@ -1706,7 +1696,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
None
| AIgnoredMutLoan (_, _) ->
(* There can be *inner* not ended mutable loans, but not outer ones *)
- craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ craise __FILE__ __LINE__ ctx.meta "Unreachable"
| AEndedIgnoredMutLoan _ ->
(* This happens with nested borrows: we need to dive in *)
raise Unimplemented
@@ -1718,7 +1708,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) :
texpression option =
match bc with
| V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
- craise __FILE__ __LINE__ _ctx.fun_decl.meta "Unreachable"
+ craise __FILE__ __LINE__ _ctx.meta "Unreachable"
| AEndedMutBorrow (_, _) ->
(* We collect consumed values: ignore *)
None
@@ -1737,7 +1727,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option =
| V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) ->
sanity_check __FILE__ __LINE__
(child_aproj = AIgnoredProjBorrows)
- ctx.fun_decl.meta;
+ ctx.meta;
(* The symbolic value was updated *)
Some (symbolic_value_to_texpression ctx mnv)
| V.AEndedProjLoans (_, _) ->
@@ -1746,7 +1736,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option =
raise Unimplemented
| AEndedProjBorrows _ -> (* We consider consumed values *) None
| AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
- craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ craise __FILE__ __LINE__ ctx.meta "Unreachable"
(** Convert the abstraction values in an abstraction to consumed values.
@@ -1812,20 +1802,20 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
| TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
- cassert __FILE__ __LINE__ (field_values = []) ctx.fun_decl.meta
+ cassert __FILE__ __LINE__ (field_values = []) ctx.meta
"ADTs with borrows are not supported yet";
(ctx, None)
| TTuple ->
(* Return *)
let variant_id = adt_v.variant_id in
- sanity_check __FILE__ __LINE__ (variant_id = None) ctx.fun_decl.meta;
+ sanity_check __FILE__ __LINE__ (variant_id = None) ctx.meta;
if field_values = [] then (ctx, None)
else
(* Note that if there is exactly one field value, [mk_simpl_tuple_pattern]
* is the identity *)
let lv = mk_simpl_tuple_pattern field_values in
(ctx, Some lv))
- | ABottom -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ | ABottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
| ALoan lc -> aloan_content_to_given_back mp lc ctx
| ABorrow bc -> aborrow_content_to_given_back mp bc ctx
| ASymbolic aproj -> aproj_to_given_back mp aproj ctx
@@ -1841,14 +1831,14 @@ and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content)
(ctx : bs_ctx) : bs_ctx * typed_pattern option =
match lc with
| AMutLoan (_, _) | ASharedLoan (_, _, _) ->
- craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ craise __FILE__ __LINE__ ctx.meta "Unreachable"
| AEndedMutLoan { child = _; given_back = _; given_back_meta = _ }
| AEndedSharedLoan (_, _) ->
(* We consider given back values, and thus ignore those *)
(ctx, None)
| AIgnoredMutLoan (_, _) ->
(* There can be *inner* not ended mutable loans, but not outer ones *)
- craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ craise __FILE__ __LINE__ ctx.meta "Unreachable"
| AEndedIgnoredMutLoan _ ->
(* This happens with nested borrows: we need to dive in *)
raise Unimplemented
@@ -1860,7 +1850,7 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content)
(ctx : bs_ctx) : bs_ctx * typed_pattern option =
match bc with
| V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
- craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ craise __FILE__ __LINE__ ctx.meta "Unreachable"
| AEndedMutBorrow (msv, _) ->
(* Return the meta-symbolic-value *)
let ctx, var = fresh_var_for_symbolic_value msv ctx in
@@ -1882,14 +1872,14 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
(List.for_all
(fun (_, aproj) -> aproj = V.AIgnoredProjBorrows)
child_projs)
- ctx.fun_decl.meta "Nested borrows are not supported yet";
+ ctx.meta "Nested borrows are not supported yet";
(ctx, None)
| AEndedProjBorrows mv ->
(* Return the meta-value *)
let ctx, var = fresh_var_for_symbolic_value mv ctx in
(ctx, Some (mk_typed_pattern_from_var var mp))
| AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
- craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ craise __FILE__ __LINE__ ctx.meta "Unreachable"
(** Convert the abstraction values in an abstraction to given back values.
@@ -2004,7 +1994,7 @@ and translate_panic (ctx : bs_ctx) : texpression =
(* Here we use the function return type - note that it is ok because
* we don't match on panics which happen inside the function body -
* but it won't be true anymore once we translate individual blocks *)
- (* If we use a state modune partie nad, we need to add a lambda for the state variable *)
+ (* If we use a state monad, we need to add a lambda for the state variable *)
(* Note that only forward functions return a state *)
let effect_info = ctx_get_effect_info ctx in
(* TODO: we should use a [Fail] function *)
@@ -2013,13 +2003,13 @@ and translate_panic (ctx : bs_ctx) : texpression =
(* Create the [Fail] value *)
let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
let ret_v =
- mk_result_fail_texpression_with_error_id ctx.fun_decl.meta
- error_failure_id ret_ty
+ mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
+ ret_ty
in
ret_v
else
- mk_result_fail_texpression_with_error_id ctx.fun_decl.meta
- error_failure_id output_ty
+ mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
+ output_ty
in
if ctx.inside_loop && Option.is_some ctx.bid then
(* We are synthesizing the backward function of a loop body *)
@@ -2075,12 +2065,12 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
| Some _ ->
(* Backward function *)
(* Sanity check *)
- sanity_check __FILE__ __LINE__ (opt_v = None) ctx.fun_decl.meta;
+ sanity_check __FILE__ __LINE__ (opt_v = None) ctx.meta;
(* Group the variables in which we stored the values we need to give back.
See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
let backward_outputs = Option.get ctx.backward_outputs in
let field_values = List.map mk_texpression_from_var backward_outputs in
- mk_simpl_tuple_texpression ctx.fun_decl.meta field_values
+ mk_simpl_tuple_texpression ctx.meta field_values
in
(* We may need to return a state
* - error-monad: Return x
@@ -2090,21 +2080,17 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
let output =
if effect_info.stateful then
let state_rvalue = mk_state_texpression ctx.state_var in
- mk_simpl_tuple_texpression ctx.fun_decl.meta [ state_rvalue; output ]
+ mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
else output
in
(* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
- mk_result_return_texpression ctx.fun_decl.meta output
+ mk_result_return_texpression ctx.meta output
and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
(ctx : bs_ctx) : texpression =
- sanity_check __FILE__ __LINE__
- (is_continue = ctx.inside_loop)
- ctx.fun_decl.meta;
+ sanity_check __FILE__ __LINE__ (is_continue = ctx.inside_loop) ctx.meta;
let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in
- sanity_check __FILE__ __LINE__
- (loop_id = Option.get ctx.loop_id)
- ctx.fun_decl.meta;
+ sanity_check __FILE__ __LINE__ (loop_id = Option.get ctx.loop_id) ctx.meta;
(* Lookup the loop information *)
let loop_id = Option.get ctx.loop_id in
@@ -2128,7 +2114,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
match ctx.backward_outputs with Some outputs -> outputs | None -> []
in
let field_values = List.map mk_texpression_from_var backward_outputs in
- mk_simpl_tuple_texpression ctx.fun_decl.meta field_values
+ mk_simpl_tuple_texpression ctx.meta field_values
in
(* We may need to return a state
@@ -2142,12 +2128,12 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
let output =
if effect_info.stateful then
let state_rvalue = mk_state_texpression ctx.state_var in
- mk_simpl_tuple_texpression ctx.fun_decl.meta [ state_rvalue; output ]
+ mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
else output
in
(* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
mk_emeta (Tag "return_with_loop")
- (mk_result_return_texpression ctx.fun_decl.meta output)
+ (mk_result_return_texpression ctx.meta output)
and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
texpression =
@@ -2198,8 +2184,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
let sg = Option.get call.sg in
let decls_ctx = ctx.decls_ctx in
let dsg =
- translate_fun_sig_with_regions_hierarchy_to_decomposed
- ctx.fun_decl.meta decls_ctx fid call.regions_hierarchy sg
+ translate_fun_sig_with_regions_hierarchy_to_decomposed ctx.meta
+ decls_ctx fid call.regions_hierarchy sg
(List.map (fun _ -> None) sg.inputs)
in
log#ldebug
@@ -2212,7 +2198,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
ctx_translate_fwd_generic_args ctx all_generics
in
let tr_self =
- translate_fwd_trait_instance_id ctx.fun_decl.meta
+ translate_fwd_trait_instance_id ctx.meta
ctx.type_ctx.type_infos tr_self
in
(tr_self, all_generics)
@@ -2333,7 +2319,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
| S.Unop E.Neg -> (
match args with
| [ arg ] ->
- let int_ty = ty_as_integer ctx.fun_decl.meta arg.ty in
+ let int_ty = ty_as_integer ctx.meta arg.ty in
(* Note that negation can lead to an overflow and thus fail (it
* is thus monadic) *)
let effect_info =
@@ -2348,7 +2334,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
let dest = mk_typed_pattern_from_var dest dest_mplace in
(ctx, Unop (Neg int_ty), effect_info, args, dest)
- | _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable")
+ | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable")
| S.Unop (E.Cast cast_kind) -> (
match cast_kind with
| CastScalar (src_ty, tgt_ty) ->
@@ -2366,18 +2352,16 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
let dest = mk_typed_pattern_from_var dest dest_mplace in
(ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, dest)
| CastFnPtr _ ->
- craise __FILE__ __LINE__ ctx.fun_decl.meta "TODO: function casts")
+ craise __FILE__ __LINE__ ctx.meta "TODO: function casts")
| S.Binop binop -> (
match args with
| [ arg0; arg1 ] ->
- let int_ty0 = ty_as_integer ctx.fun_decl.meta arg0.ty in
- let int_ty1 = ty_as_integer ctx.fun_decl.meta arg1.ty in
+ let int_ty0 = ty_as_integer ctx.meta arg0.ty in
+ let int_ty1 = ty_as_integer ctx.meta arg1.ty in
(match binop with
(* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *)
| E.Shl | E.Shr -> ()
- | _ ->
- sanity_check __FILE__ __LINE__ (int_ty0 = int_ty1)
- ctx.fun_decl.meta);
+ | _ -> sanity_check __FILE__ __LINE__ (int_ty0 = int_ty1) ctx.meta);
let effect_info =
{
can_fail = ExpressionsUtils.binop_can_fail binop;
@@ -2390,7 +2374,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
let dest = mk_typed_pattern_from_var dest dest_mplace in
(ctx, Binop (binop, int_ty0), effect_info, args, dest)
- | _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable")
+ | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable")
in
let func = { id = FunOrOp fun_id; generics } in
let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
@@ -2399,7 +2383,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
in
let func_ty = mk_arrows input_tys ret_ty in
let func = { e = Qualif func; ty = func_ty } in
- let call = mk_apps ctx.fun_decl.meta func args in
+ let call = mk_apps ctx.meta func args in
(* Translate the next expression *)
let next_e = translate_expression e ctx in
(* Put together *)
@@ -2433,7 +2417,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
^ "\n- loop_id: "
^ Print.option_to_string Pure.LoopId.to_string ctx.loop_id
^ "\n- eval_ctx:\n"
- ^ eval_ctx_to_string ~meta:(Some ctx.fun_decl.meta) ectx
+ ^ eval_ctx_to_string ~meta:(Some ctx.meta) ectx
^ "\n- abs:\n" ^ abs_to_string ctx abs ^ "\n"));
(* When we end an input abstraction, this input abstraction gets back
@@ -2447,7 +2431,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
for a parent backward function.
*)
let bid = Option.get ctx.bid in
- sanity_check __FILE__ __LINE__ (rg_id = bid) ctx.fun_decl.meta;
+ sanity_check __FILE__ __LINE__ (rg_id = bid) ctx.meta;
(* First, introduce the given back variables.
@@ -2497,7 +2481,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
(fun (var, v) ->
sanity_check __FILE__ __LINE__
((var : var).ty = (v : texpression).ty)
- ctx.fun_decl.meta)
+ ctx.meta)
variables_values;
(* Translate the next expression *)
let next_e = translate_expression e ctx in
@@ -2518,7 +2502,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
| S.Fun (fun_id, _) -> fun_id
| Unop _ | Binop _ ->
(* Those don't have backward functions *)
- craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ craise __FILE__ __LINE__ ctx.meta "Unreachable"
in
let effect_info = get_fun_effect_info ctx fun_id None (Some rg_id) in
(* Retrieve the values consumed upon ending the loans inside this
@@ -2580,7 +2564,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
^ "\nfunc type: "
^ pure_ty_to_string ctx func.ty
^ "\n\nargs:\n" ^ String.concat "\n" args));
- let call = mk_apps ctx.fun_decl.meta func args in
+ let call = mk_apps ctx.meta func args in
mk_let effect_info.can_fail output call next_e
and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs)
@@ -2591,8 +2575,8 @@ and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs)
(* We can do this simply by checking that it consumes and gives back nothing *)
let inputs = abs_to_consumed ctx ectx abs in
let ctx, outputs = abs_to_given_back None abs ctx in
- sanity_check __FILE__ __LINE__ (inputs = []) ctx.fun_decl.meta;
- sanity_check __FILE__ __LINE__ (outputs = []) ctx.fun_decl.meta;
+ sanity_check __FILE__ __LINE__ (inputs = []) ctx.meta;
+ sanity_check __FILE__ __LINE__ (outputs = []) ctx.meta;
(* Translate the next expression *)
translate_expression e ctx
@@ -2634,7 +2618,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
(* Retrieve the values consumed upon ending the loans inside this
* abstraction: as there are no nested borrows, there should be none. *)
let consumed = abs_to_consumed ctx ectx abs in
- cassert __FILE__ __LINE__ (consumed = []) ctx.fun_decl.meta
+ cassert __FILE__ __LINE__ (consumed = []) ctx.meta
"Nested borrows are not supported yet";
(* Retrieve the values given back upon ending this abstraction - note that
* we don't provide meta-place information, because those assignments will
@@ -2653,8 +2637,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
^ pure_ty_to_string ctx given_back.ty
^ "\n- sig input ty: "
^ pure_ty_to_string ctx input.ty));
- sanity_check __FILE__ __LINE__ (given_back.ty = input.ty)
- ctx.fun_decl.meta)
+ sanity_check __FILE__ __LINE__ (given_back.ty = input.ty) ctx.meta)
given_back_inputs;
(* Translate the next expression *)
let next_e = translate_expression e ctx in
@@ -2671,9 +2654,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
texpression =
let vloop_id = loop_id in
let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in
- sanity_check __FILE__ __LINE__
- (loop_id = Option.get ctx.loop_id)
- ctx.fun_decl.meta;
+ sanity_check __FILE__ __LINE__ (loop_id = Option.get ctx.loop_id) ctx.meta;
let rg_id = Option.get rg_id in
(* There are two cases depending on the [abs_kind] (whether this is a
synth input or a regular loop call) *)
@@ -2743,7 +2724,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
match func with
| None -> next_e
| Some func ->
- let call = mk_apps ctx.fun_decl.meta func args in
+ let call = mk_apps ctx.meta func args in
(* Add meta-information - this is slightly hacky: we look at the
values consumed by the abstraction (note that those come from
*before* we applied the fixed-point context) and use them to
@@ -2800,7 +2781,7 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value)
in
let func_ty = mk_arrow (TLiteral TBool) mk_unit_ty in
let func = { e = Qualif func; ty = func_ty } in
- let assertion = mk_apps ctx.fun_decl.meta func args in
+ let assertion = mk_apps ctx.meta func args in
mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e
and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
@@ -2815,7 +2796,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
| V.SeLiteral _ ->
(* We do not *register* symbolic expansions to literal
values in the symbolic ADT *)
- craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ craise __FILE__ __LINE__ ctx.meta "Unreachable"
| SeMutRef (_, nsv) | SeSharedRef (_, nsv) ->
(* The (mut/shared) borrow type is extracted to identity: we thus simply
introduce an reassignment *)
@@ -2828,11 +2809,11 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
next_e
| SeAdt _ ->
(* Should be in the [ExpandAdt] case *)
- craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable")
+ craise __FILE__ __LINE__ ctx.meta "Unreachable")
| ExpandAdt branches -> (
(* We don't do the same thing if there is a branching or not *)
match branches with
- | [] -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ | [] -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
| [ (variant_id, svl, branch) ]
when not
(TypesUtils.ty_is_custom_adt sv.V.sv_ty
@@ -2873,7 +2854,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
(* Sanity check *)
sanity_check __FILE__ __LINE__
(List.for_all (fun br -> br.branch.ty = ty) branches)
- ctx.fun_decl.meta;
+ ctx.meta;
(* Return *)
{ e; ty })
| ExpandBool (true_e, false_e) ->
@@ -2893,7 +2874,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
^ pure_ty_to_string ctx true_e.ty
^ "\n\nfalse_e.ty: "
^ pure_ty_to_string ctx false_e.ty));
- sanity_check __FILE__ __LINE__ (ty = false_e.ty) ctx.fun_decl.meta;
+ sanity_check __FILE__ __LINE__ (ty = false_e.ty) ctx.meta;
{ e; ty }
| ExpandInt (int_ty, branches, otherwise) ->
let translate_branch ((v, branch_e) : V.scalar_value * S.expression) :
@@ -2920,7 +2901,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
let ty = otherwise.branch.ty in
sanity_check __FILE__ __LINE__
(List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches)
- ctx.fun_decl.meta;
+ ctx.meta;
{ e; ty }
(* Translate and [ExpandAdt] when there is no branching (i.e., one branch).
@@ -2995,14 +2976,14 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
* field.
* We use the [dest] variable in order not to have to recompute
* the type of the result of the projection... *)
- let adt_id, generics = ty_as_adt ctx.fun_decl.meta scrutinee.ty in
+ let adt_id, generics = ty_as_adt ctx.meta scrutinee.ty in
let gen_field_proj (field_id : FieldId.id) (dest : var) : texpression =
let proj_kind = { adt_id; field_id } in
let qualif = { id = Proj proj_kind; generics } in
let proj_e = Qualif qualif in
let proj_ty = mk_arrow scrutinee.ty dest.ty in
let proj = { e = proj_e; ty = proj_ty } in
- mk_app ctx.fun_decl.meta proj scrutinee
+ mk_app ctx.meta proj scrutinee
in
let id_var_pairs = FieldId.mapi (fun fid v -> (fid, v)) vars in
let monadic = false in
@@ -3023,7 +3004,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
let var =
match vars with
| [ v ] -> v
- | _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
in
(* We simply introduce an assignment - the box type is the
* identity when extracted ([box a = a]) *)
@@ -3037,7 +3018,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
* through the functions provided by the API (note that we don't
* know how to expand values like vectors or arrays, because they have a variable number
* of fields!) *)
- craise __FILE__ __LINE__ ctx.fun_decl.meta
+ craise __FILE__ __LINE__ ctx.meta
"Attempt to expand a non-expandable value"
and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
@@ -3075,9 +3056,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
| VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
| VaTraitConstValue (trait_ref, const_name) ->
let type_infos = ctx.type_ctx.type_infos in
- let trait_ref =
- translate_fwd_trait_ref ctx.fun_decl.meta type_infos trait_ref
- in
+ let trait_ref = translate_fwd_trait_ref ctx.meta type_infos trait_ref in
let qualif_id = TraitConst (trait_ref, const_name) in
let qualif = { id = qualif_id; generics = empty_generic_args } in
{ e = Qualif qualif; ty = var.ty }
@@ -3218,7 +3197,7 @@ and translate_forward_end (ectx : C.eval_ctx)
else pure_fwd_var :: back_vars
in
let vars = List.map mk_texpression_from_var vars in
- let ret = mk_simpl_tuple_texpression ctx.fun_decl.meta vars in
+ let ret = mk_simpl_tuple_texpression ctx.meta vars in
(* Introduce a fresh input state variable for the forward expression *)
let _ctx, state_var, state_pat =
@@ -3229,10 +3208,8 @@ and translate_forward_end (ectx : C.eval_ctx)
in
let state_var = List.map mk_texpression_from_var state_var in
- let ret =
- mk_simpl_tuple_texpression ctx.fun_decl.meta (state_var @ [ ret ])
- in
- let ret = mk_result_return_texpression ctx.fun_decl.meta ret in
+ let ret = mk_simpl_tuple_texpression ctx.meta (state_var @ [ ret ]) in
+ let ret = mk_result_return_texpression ctx.meta ret in
(* Introduce all the let-bindings *)
@@ -3405,7 +3382,7 @@ and translate_forward_end (ectx : C.eval_ctx)
in
let func_ty = mk_arrows input_tys ret_ty in
let func = { e = Qualif func; ty = func_ty } in
- let call = mk_apps ctx.fun_decl.meta func args in
+ let call = mk_apps ctx.meta func args in
call
in
@@ -3464,7 +3441,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
(fun (sv : V.symbolic_value) ->
V.SymbolicValueId.Map.mem sv.sv_id ctx.sv_to_var)
loop.input_svalues)
- ctx.fun_decl.meta;
+ ctx.meta;
(* Translate the loop inputs *)
let inputs =
@@ -3486,7 +3463,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
(fun ty ->
cassert __FILE__ __LINE__
(not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty))
- !ctx.fun_decl.meta "The types shouldn't contain borrows";
+ !ctx.meta "The types shouldn't contain borrows";
ctx_translate_fwd_ty !ctx ty)
tys)
loop.rg_to_given_back_tys
@@ -3567,7 +3544,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
let ctx =
sanity_check __FILE__ __LINE__
(not (LoopId.Map.mem loop_id ctx.loops))
- ctx.fun_decl.meta;
+ ctx.meta;
(* Note that we will retrieve the input values later in the [ForwardEnd]
(and will introduce the outputs at that moment, together with the actual
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 4c0f2e0d..348183c5 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -127,6 +127,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
let ctx =
{
+ meta = fdef.meta;
decls_ctx = trans_ctx;
SymbolicToPure.bid = None;
sg;