diff options
Diffstat (limited to 'compiler/InterpreterExpansion.ml')
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 158 |
1 files changed, 79 insertions, 79 deletions
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index 39c9bd4a..388d7382 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -49,14 +49,14 @@ type proj_kind = LoanProj | BorrowProj it would make things clearer. *) let apply_symbolic_expansion_to_target_avalues (config : config) - (meta : Meta.meta) (allow_reborrows : bool) (proj_kind : proj_kind) + (span : Meta.span) (allow_reborrows : bool) (proj_kind : proj_kind) (original_sv : symbolic_value) (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx = (* Symbolic values contained in the expansion might contain already ended regions *) let check_symbolic_no_ended = false in (* Prepare reborrows registration *) let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config meta allow_reborrows + prepare_reborrows config span allow_reborrows in (* Visitor to apply the expansion *) let obj = @@ -66,7 +66,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (** When visiting an abstraction, we remember the regions it owns to be able to properly reduce projectors when expanding symbolic values *) method! visit_abs current_abs abs = - sanity_check __FILE__ __LINE__ (Option.is_none current_abs) meta; + sanity_check __FILE__ __LINE__ (Option.is_none current_abs) span; let current_abs = Some abs in super#visit_abs current_abs abs @@ -80,7 +80,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) | AProjLoans (sv, _) | AProjBorrows (sv, _) -> sanity_check __FILE__ __LINE__ (not (same_symbolic_id sv original_sv)) - meta + span | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj current_abs aproj @@ -100,10 +100,10 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (* Check if this is the symbolic value we are looking for *) if same_symbolic_id sv original_sv then ( (* There mustn't be any given back values *) - sanity_check __FILE__ __LINE__ (given_back = []) meta; + sanity_check __FILE__ __LINE__ (given_back = []) span; (* Apply the projector *) let projected_value = - apply_proj_loans_on_symbolic_expansion meta proj_regions + apply_proj_loans_on_symbolic_expansion span proj_regions ancestors_regions expansion original_sv.sv_ty in (* Replace *) @@ -120,12 +120,12 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (* WARNING: we mustn't get there if the expansion is for a shared * reference. *) let expansion = - symbolic_expansion_non_shared_borrow_to_value meta original_sv + symbolic_expansion_non_shared_borrow_to_value span original_sv expansion in (* Apply the projector *) let projected_value = - apply_proj_borrows meta check_symbolic_no_ended ctx + apply_proj_borrows span check_symbolic_no_ended ctx fresh_reborrow proj_regions ancestors_regions expansion proj_ty in @@ -149,11 +149,11 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (** Auxiliary function. Apply a symbolic expansion to avalues in a context. *) -let apply_symbolic_expansion_to_avalues (config : config) (meta : Meta.meta) +let apply_symbolic_expansion_to_avalues (config : config) (span : Meta.span) (allow_reborrows : bool) (original_sv : symbolic_value) (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx = let apply_expansion proj_kind ctx = - apply_symbolic_expansion_to_target_avalues config meta allow_reborrows + apply_symbolic_expansion_to_target_avalues config span allow_reborrows proj_kind original_sv expansion ctx in (* First target the loan projectors, then the borrow projectors *) @@ -166,12 +166,12 @@ let apply_symbolic_expansion_to_avalues (config : config) (meta : Meta.meta) Simply replace the symbolic values (*not avalues*) in the context with a given value. Will break invariants if not used properly. *) -let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) +let replace_symbolic_values (span : Meta.span) (at_most_once : bool) (original_sv : symbolic_value) (nv : value) (ctx : eval_ctx) : eval_ctx = (* Count *) let replaced = ref false in let replace () = - if at_most_once then sanity_check __FILE__ __LINE__ (not !replaced) meta; + if at_most_once then sanity_check __FILE__ __LINE__ (not !replaced) span; replaced := true; nv in @@ -190,18 +190,18 @@ let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (* Return *) ctx -let apply_symbolic_expansion_non_borrow (config : config) (meta : Meta.meta) +let apply_symbolic_expansion_non_borrow (config : config) (span : Meta.span) (original_sv : symbolic_value) (ctx : eval_ctx) (expansion : symbolic_expansion) : eval_ctx = (* Apply the expansion to non-abstraction values *) - let nv = symbolic_expansion_non_borrow_to_value meta original_sv expansion in + let nv = symbolic_expansion_non_borrow_to_value span original_sv expansion in let at_most_once = false in let ctx = - replace_symbolic_values meta at_most_once original_sv nv.value ctx + replace_symbolic_values span at_most_once original_sv nv.value ctx in (* Apply the expansion to abstraction values *) let allow_reborrows = false in - apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv + apply_symbolic_expansion_to_avalues config span allow_reborrows original_sv expansion ctx (** Compute the expansion of a non-assumed (i.e.: not [Box], etc.) @@ -214,7 +214,7 @@ let apply_symbolic_expansion_non_borrow (config : config) (meta : Meta.meta) [expand_enumerations] controls the expansion of enumerations: if false, it doesn't allow the expansion of enumerations *containing several variants*. *) -let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) +let compute_expanded_symbolic_non_assumed_adt_value (span : Meta.span) (expand_enumerations : bool) (def_id : TypeDeclId.id) (generics : generic_args) (ctx : eval_ctx) : symbolic_expansion list = (* Lookup the definition and check if it is an enumeration with several @@ -222,21 +222,21 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) let def = ctx_lookup_type_decl ctx def_id in sanity_check __FILE__ __LINE__ (List.length generics.regions = List.length def.generics.regions) - meta; + span; (* Retrieve, for every variant, the list of its instantiated field types *) let variants_fields_types = - AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes meta ctx def + AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes span ctx def generics in (* Check if there is strictly more than one variant *) if List.length variants_fields_types > 1 && not expand_enumerations then - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span "Not allowed to expand enumerations with several variants"; (* Initialize the expanded value for a given variant *) let initialize ((variant_id, field_types) : VariantId.id option * rty list) : symbolic_expansion = let field_values = - List.map (fun (ty : rty) -> mk_fresh_symbolic_value meta ty) field_types + List.map (fun (ty : rty) -> mk_fresh_symbolic_value span ty) field_types in let see = SeAdt (variant_id, field_values) in see @@ -244,20 +244,20 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (* Initialize all the expanded values of all the variants *) List.map initialize variants_fields_types -let compute_expanded_symbolic_tuple_value (meta : Meta.meta) +let compute_expanded_symbolic_tuple_value (span : Meta.span) (field_types : rty list) : symbolic_expansion = (* Generate the field values *) let field_values = - List.map (fun sv_ty -> mk_fresh_symbolic_value meta sv_ty) field_types + List.map (fun sv_ty -> mk_fresh_symbolic_value span sv_ty) field_types in let variant_id = None in let see = SeAdt (variant_id, field_values) in see -let compute_expanded_symbolic_box_value (meta : Meta.meta) (boxed_ty : rty) : +let compute_expanded_symbolic_box_value (span : Meta.span) (boxed_ty : rty) : symbolic_expansion = (* Introduce a fresh symbolic value *) - let boxed_value = mk_fresh_symbolic_value meta boxed_ty in + let boxed_value = mk_fresh_symbolic_value span boxed_ty in let see = SeAdt (None, [ boxed_value ]) in see @@ -270,22 +270,22 @@ let compute_expanded_symbolic_box_value (meta : Meta.meta) (boxed_ty : rty) : [expand_enumerations] controls the expansion of enumerations: if [false], it doesn't allow the expansion of enumerations *containing several variants*. *) -let compute_expanded_symbolic_adt_value (meta : Meta.meta) +let compute_expanded_symbolic_adt_value (span : Meta.span) (expand_enumerations : bool) (adt_id : type_id) (generics : generic_args) (ctx : eval_ctx) : symbolic_expansion list = match (adt_id, generics.regions, generics.types) with | TAdtId def_id, _, _ -> - compute_expanded_symbolic_non_assumed_adt_value meta expand_enumerations + compute_expanded_symbolic_non_assumed_adt_value span expand_enumerations def_id generics ctx | TTuple, [], _ -> - [ compute_expanded_symbolic_tuple_value meta generics.types ] + [ compute_expanded_symbolic_tuple_value span generics.types ] | TAssumed TBox, [], [ boxed_ty ] -> - [ compute_expanded_symbolic_box_value meta boxed_ty ] + [ compute_expanded_symbolic_box_value span boxed_ty ] | _ -> - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span "compute_expanded_symbolic_adt_value: unexpected combination" -let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) +let expand_symbolic_value_shared_borrow (config : config) (span : Meta.span) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) (ref_ty : rty) : cm_fun = fun ctx -> @@ -318,11 +318,11 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) Some [ AsbBorrow bid; shared_asb ] else (* Not in the set: ignore *) Some [ shared_asb ] - | _ -> craise __FILE__ __LINE__ meta "Unexpected" + | _ -> craise __FILE__ __LINE__ span "Unexpected" else None in (* The fresh symbolic value for the shared value *) - let shared_sv = mk_fresh_symbolic_value meta ref_ty in + let shared_sv = mk_fresh_symbolic_value span ref_ty in (* Visitor to replace the projectors on borrows *) let obj = object (self) @@ -335,7 +335,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) else super#visit_VSymbolic env sv method! visit_EAbs proj_regions abs = - sanity_check __FILE__ __LINE__ (Option.is_none proj_regions) meta; + sanity_check __FILE__ __LINE__ (Option.is_none proj_regions) span; let proj_regions = Some abs.regions in super#visit_EAbs proj_regions abs @@ -362,7 +362,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) | AProjLoans (sv, _) | AProjBorrows (sv, _) -> sanity_check __FILE__ __LINE__ (not (same_symbolic_id sv original_sv)) - meta + span | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj proj_regions aproj @@ -388,62 +388,62 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) let ctx = obj#visit_eval_ctx None ctx in (* Finally, replace the projectors on loans *) let bids = !borrows in - sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) meta; + sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) span; let see = SeSharedRef (bids, shared_sv) in let allow_reborrows = true in let ctx = - apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv + apply_symbolic_expansion_to_avalues config span allow_reborrows original_sv see ctx in ( ctx, (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv + S.synthesize_symbolic_expansion_no_branching span original_sv original_sv_place see ) (** TODO: simplify and merge with the other expansion function *) -let expand_symbolic_value_borrow (config : config) (meta : Meta.meta) +let expand_symbolic_value_borrow (config : config) (span : Meta.span) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun = fun ctx -> - sanity_check __FILE__ __LINE__ (region <> RErased) meta; + sanity_check __FILE__ __LINE__ (region <> RErased) span; (* Check that we are allowed to expand the reference *) sanity_check __FILE__ __LINE__ (not (region_in_set region ctx.ended_regions)) - meta; + span; (* Match on the reference kind *) match rkind with | RMut -> (* Simple case: simply create a fresh symbolic value and a fresh * borrow id *) - let sv = mk_fresh_symbolic_value meta ref_ty in + let sv = mk_fresh_symbolic_value span ref_ty in let bid = fresh_borrow_id () in let see = SeMutRef (bid, sv) in (* Expand the symbolic values - we simply perform a substitution (and * check that we perform exactly one substitution) *) let nv = - symbolic_expansion_non_shared_borrow_to_value meta original_sv see + symbolic_expansion_non_shared_borrow_to_value span original_sv see in let at_most_once = true in let ctx = - replace_symbolic_values meta at_most_once original_sv nv.value ctx + replace_symbolic_values span at_most_once original_sv nv.value ctx in (* Expand the symbolic avalues *) let allow_reborrows = true in let ctx = - apply_symbolic_expansion_to_avalues config meta allow_reborrows + apply_symbolic_expansion_to_avalues config span allow_reborrows original_sv see ctx in (* Apply the continuation *) ( ctx, fun e -> (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv + S.synthesize_symbolic_expansion_no_branching span original_sv original_sv_place see e ) | RShared -> - expand_symbolic_value_shared_borrow config meta original_sv + expand_symbolic_value_shared_borrow config span original_sv original_sv_place ref_ty ctx -let expand_symbolic_bool (config : config) (meta : Meta.meta) +let expand_symbolic_bool (config : config) (span : Meta.span) (sv : symbolic_value) (sv_place : SA.mplace option) : eval_ctx -> (eval_ctx * eval_ctx) @@ -453,26 +453,26 @@ let expand_symbolic_bool (config : config) (meta : Meta.meta) (* Compute the expanded value *) let original_sv = sv in let rty = original_sv.sv_ty in - sanity_check __FILE__ __LINE__ (rty = TLiteral TBool) meta; + sanity_check __FILE__ __LINE__ (rty = TLiteral TBool) span; (* Expand the symbolic value to true or false and continue execution *) let see_true = SeLiteral (VBool true) in let see_false = SeLiteral (VBool false) in let seel = [ Some see_true; Some see_false ] in (* Apply the symbolic expansion *) let apply_expansion = - apply_symbolic_expansion_non_borrow config meta sv ctx + apply_symbolic_expansion_non_borrow config span sv ctx in let ctx_true = apply_expansion see_true in let ctx_false = apply_expansion see_false in (* Compute the continuation to build the expression *) let cf e = let el = match e with Some (a, b) -> Some [ a; b ] | None -> None in - S.synthesize_symbolic_expansion meta sv sv_place seel el + S.synthesize_symbolic_expansion span sv sv_place seel el in (* Return *) ((ctx_true, ctx_false), cf) -let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) +let expand_symbolic_value_no_branching (config : config) (span : Meta.span) (sv : symbolic_value) (sv_place : SA.mplace option) : cm_fun = fun ctx -> (* Debug *) @@ -493,26 +493,26 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (* Compute the expanded value *) let allow_branching = false in let seel = - compute_expanded_symbolic_adt_value meta allow_branching adt_id + compute_expanded_symbolic_adt_value span allow_branching adt_id generics ctx in (* There should be exacly one branch *) let see = Collections.List.to_cons_nil seel in (* Apply in the context *) let ctx = - apply_symbolic_expansion_non_borrow config meta original_sv ctx see + apply_symbolic_expansion_non_borrow config span original_sv ctx see in (* Return*) ( ctx, (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv + S.synthesize_symbolic_expansion_no_branching span original_sv original_sv_place see ) (* Borrows *) | TRef (region, ref_ty, rkind) -> - expand_symbolic_value_borrow config meta original_sv original_sv_place + expand_symbolic_value_borrow config span original_sv original_sv_place region ref_ty rkind ctx | _ -> - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("expand_symbolic_value_no_branching: unexpected type: " ^ show_rty rty) in @@ -522,18 +522,18 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) ("expand_symbolic_value_no_branching: " ^ symbolic_value_to_string ctx0 sv ^ "\n\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ eval_ctx_to_string ~span:(Some span) ctx0 ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n")); (* Sanity check: the symbolic value has disappeared *) sanity_check __FILE__ __LINE__ (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) - meta; + span; (* Return *) (ctx, cc) -let expand_symbolic_adt (config : config) (meta : Meta.meta) +let expand_symbolic_adt (config : config) (span : Meta.span) (sv : symbolic_value) (sv_place : SA.mplace option) : eval_ctx -> eval_ctx list * (SymbolicAst.expression list option -> eval_result) = @@ -552,21 +552,21 @@ let expand_symbolic_adt (config : config) (meta : Meta.meta) let allow_branching = true in (* Compute the expanded value *) let seel = - compute_expanded_symbolic_adt_value meta allow_branching adt_id generics + compute_expanded_symbolic_adt_value span allow_branching adt_id generics ctx in (* Apply *) let ctx_branches = - List.map (apply_symbolic_expansion_non_borrow config meta sv ctx) seel + List.map (apply_symbolic_expansion_non_borrow config span sv ctx) seel in ( ctx_branches, - S.synthesize_symbolic_expansion meta sv original_sv_place + S.synthesize_symbolic_expansion span sv original_sv_place (List.map (fun el -> Some el) seel) ) | _ -> - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("expand_symbolic_adt: unexpected type: " ^ show_rty rty) -let expand_symbolic_int (config : config) (meta : Meta.meta) +let expand_symbolic_int (config : config) (span : Meta.span) (sv : symbolic_value) (sv_place : SA.mplace option) (int_type : integer_type) (tgts : scalar_value list) : eval_ctx -> @@ -575,7 +575,7 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) eval_result) = fun ctx -> (* Sanity check *) - sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral (TInteger int_type)) meta; + sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral (TInteger int_type)) span; (* For all the branches of the switch, we expand the symbolic value * to the value given by the branch and execute the branch statement. * For the otherwise branch, we leave the symbolic value as it is @@ -585,7 +585,7 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) (* Substitute the symbolic values to generate the contexts in the branches *) let seel = List.map (fun v -> SeLiteral (VScalar v)) tgts in let ctx_branches = - List.map (apply_symbolic_expansion_non_borrow config meta sv ctx) seel + List.map (apply_symbolic_expansion_non_borrow config span sv ctx) seel in let ctx_otherwise = ctx in (* Update the symbolic ast *) @@ -594,7 +594,7 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) | None -> None | Some (el, e) -> let seel = List.map (fun x -> Some x) seel in - S.synthesize_symbolic_expansion meta sv sv_place (seel @ [ None ]) + S.synthesize_symbolic_expansion span sv sv_place (seel @ [ None ]) (Some (el @ [ e ])) in ((ctx_branches, ctx_otherwise), cf) @@ -607,7 +607,7 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) an enumeration with strictly more than one variant, a slice, etc.) or if we need to expand a recursive type (because this leads to looping). *) -let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : +let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) : cm_fun = fun ctx -> (* The visitor object, to look for symbolic values in the concrete environment *) @@ -649,30 +649,30 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : (match def.kind with | Struct _ | Enum ([] | [ _ ]) -> () | Enum (_ :: _) -> - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("Attempted to greedily expand a symbolic enumeration with > \ 1 variants (option [greedy_expand_symbolics_with_borrows] \ of [config]): " ^ name_to_string ctx def.name) | Opaque -> - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span "Attempted to greedily expand an opaque type"); (* Also, we need to check if the definition is recursive *) if ctx_type_decl_is_rec ctx def_id then - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("Attempted to greedily expand a recursive definition (option \ [greedy_expand_symbolics_with_borrows] of [config]): " ^ name_to_string ctx def.name) - else expand_symbolic_value_no_branching config meta sv None ctx + else expand_symbolic_value_no_branching config span sv None ctx | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) -> (* Ok *) - expand_symbolic_value_no_branching config meta sv None ctx + expand_symbolic_value_no_branching config span sv None ctx | TAdt (TAssumed (TArray | TSlice | TStr), _) -> (* We can't expand those *) - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span "Attempted to greedily expand an ADT which can't be expanded " | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ -> - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" in (* Compose and continue *) comp cc (expand ctx) @@ -680,10 +680,10 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : (* Apply *) expand ctx -let greedy_expand_symbolic_values (config : config) (meta : Meta.meta) : cm_fun +let greedy_expand_symbolic_values (config : config) (span : Meta.span) : cm_fun = fun ctx -> if Config.greedy_expand_symbolics_with_borrows then ( log#ldebug (lazy "greedy_expand_symbolic_values"); - greedy_expand_symbolics_with_borrows config meta ctx) + greedy_expand_symbolics_with_borrows config span ctx) else (ctx, fun e -> e) |