diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterStatements.ml | 484 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.mli | 3 |
2 files changed, 271 insertions, 216 deletions
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 6b9f47ce..1cf1c5ef 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -11,6 +11,7 @@ open InterpreterProjectors open InterpreterExpansion open InterpreterPaths open InterpreterExpressions +open Errors module Subst = Substitute module S = SynthesizeSymbolic @@ -18,33 +19,33 @@ module S = SynthesizeSymbolic let log = L.statements_log (** Drop a value at a given place - TODO: factorize this with [assign_to_place] *) -let drop_value (config : config) (p : place) : cm_fun = +let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun = fun cf ctx -> log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n" - ^ eval_ctx_to_string ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Note that we use [Write], not [Move]: we allow to drop values *below* borrows *) let access = Write in (* First make sure we can access the place, by ending loans or expanding * symbolic values along the path, for instance *) - let cc = update_ctx_along_read_place config access p in + let cc = update_ctx_along_read_place config meta access p in (* Prepare the place (by ending the outer loans *at* the place). *) - let cc = comp cc (prepare_lplace config p) in + let cc = comp cc (prepare_lplace config meta p) in (* Replace the value with {!Bottom} *) let replace cf (v : typed_value) ctx = (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows it may contain *) - let mv = InterpreterPaths.read_place access p ctx in + let mv = InterpreterPaths.read_place meta access p ctx in let dummy_id = fresh_dummy_var_id () in let ctx = ctx_push_dummy_var ctx dummy_id mv in (* Update the destination to ⊥ *) let nv = { v with value = VBottom } in - let ctx = write_place access p nv ctx in + let ctx = write_place meta access p nv ctx in log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" - ^ eval_ctx_to_string ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); cf ctx in (* Compose and apply *) @@ -57,33 +58,34 @@ let push_dummy_var (vid : DummyVarId.id) (v : typed_value) : cm_fun = cf ctx (** Remove a dummy variable from the environment *) -let remove_dummy_var (vid : DummyVarId.id) (cf : typed_value -> m_fun) : m_fun = +let remove_dummy_var (meta : Meta.meta) (vid : DummyVarId.id) + (cf : typed_value -> m_fun) : m_fun = fun ctx -> - let ctx, v = ctx_remove_dummy_var ctx vid in + let ctx, v = ctx_remove_dummy_var meta ctx vid in cf v ctx (** Push an uninitialized variable to the environment *) -let push_uninitialized_var (var : var) : cm_fun = +let push_uninitialized_var (meta : Meta.meta) (var : var) : cm_fun = fun cf ctx -> - let ctx = ctx_push_uninitialized_var ctx var in + let ctx = ctx_push_uninitialized_var meta ctx var in cf ctx (** Push a list of uninitialized variables to the environment *) -let push_uninitialized_vars (vars : var list) : cm_fun = +let push_uninitialized_vars (meta : Meta.meta) (vars : var list) : cm_fun = fun cf ctx -> - let ctx = ctx_push_uninitialized_vars ctx vars in + let ctx = ctx_push_uninitialized_vars meta ctx vars in cf ctx (** Push a variable to the environment *) -let push_var (var : var) (v : typed_value) : cm_fun = +let push_var (meta : Meta.meta) (var : var) (v : typed_value) : cm_fun = fun cf ctx -> - let ctx = ctx_push_var ctx var v in + let ctx = ctx_push_var meta ctx var v in cf ctx (** Push a list of variables to the environment *) -let push_vars (vars : (var * typed_value) list) : cm_fun = +let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun = fun cf ctx -> - let ctx = ctx_push_vars ctx vars in + let ctx = ctx_push_vars meta ctx vars in cf ctx (** Assign a value to a given place. @@ -93,41 +95,44 @@ let push_vars (vars : (var * typed_value) list) : cm_fun = dummy variable and putting in its destination (after having checked that preparing the destination didn't introduce ⊥). *) -let assign_to_place (config : config) (rv : typed_value) (p : place) : cm_fun = +let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) + (p : place) : cm_fun = fun cf ctx -> log#ldebug (lazy ("assign_to_place:" ^ "\n- rv: " - ^ typed_value_to_string ctx rv + ^ typed_value_to_string ~meta:(Some meta) ctx rv ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n" - ^ eval_ctx_to_string ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Push the rvalue to a dummy variable, for bookkeeping *) let rvalue_vid = fresh_dummy_var_id () in let cc = push_dummy_var rvalue_vid rv in (* Prepare the destination *) - let cc = comp cc (prepare_lplace config p) in + let cc = comp cc (prepare_lplace config meta p) in (* Retrieve the rvalue from the dummy variable *) - let cc = comp cc (fun cf _lv -> remove_dummy_var rvalue_vid cf) in + let cc = comp cc (fun cf _lv -> remove_dummy_var meta rvalue_vid cf) in (* Update the destination *) let move_dest cf (rv : typed_value) : m_fun = fun ctx -> (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows *) - let mv = InterpreterPaths.read_place Write p ctx in + let mv = InterpreterPaths.read_place meta Write p ctx in let dest_vid = fresh_dummy_var_id () in let ctx = ctx_push_dummy_var ctx dest_vid mv in (* Write to the destination *) (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) - assert (not (bottom_in_value ctx.ended_regions rv)); + exec_assert __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions rv)) + meta "The value to move contains bottom"; (* Update the destination *) - let ctx = write_place Write p rv ctx in + let ctx = write_place meta Write p rv ctx in (* Debug *) log#ldebug (lazy ("assign_to_place:" ^ "\n- rv: " - ^ typed_value_to_string ctx rv + ^ typed_value_to_string ~meta:(Some meta) ctx rv ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" - ^ eval_ctx_to_string ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Continue *) cf ctx in @@ -135,11 +140,11 @@ let assign_to_place (config : config) (rv : typed_value) (p : place) : cm_fun = comp cc move_dest cf ctx (** Evaluate an assertion, when the scrutinee is not symbolic *) -let eval_assertion_concrete (config : config) (assertion : assertion) : - st_cm_fun = +let eval_assertion_concrete (config : config) (meta : Meta.meta) + (assertion : assertion) : st_cm_fun = fun cf ctx -> (* There won't be any symbolic expansions: fully evaluate the operand *) - let eval_op = eval_operand config assertion.cond in + let eval_op = eval_operand config meta assertion.cond in let eval_assert cf (v : typed_value) : m_fun = fun ctx -> match v.value with @@ -147,8 +152,9 @@ let eval_assertion_concrete (config : config) (assertion : assertion) : (* Branch *) if b = assertion.expected then cf Unit ctx else cf Panic ctx | _ -> - raise - (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v)) + craise __FILE__ __LINE__ meta + ("Expected a boolean, got: " + ^ typed_value_to_string ~meta:(Some meta) ctx v) in (* Compose and apply *) comp eval_op eval_assert cf ctx @@ -159,14 +165,15 @@ let eval_assertion_concrete (config : config) (assertion : assertion) : a call to [assert ...] then continue in the success branch (and thus expand the boolean to [true]). *) -let eval_assertion (config : config) (assertion : assertion) : st_cm_fun = +let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) + : st_cm_fun = fun cf ctx -> (* Evaluate the operand *) - let eval_op = eval_operand config assertion.cond in + let eval_op = eval_operand config meta assertion.cond in (* Evaluate the assertion *) let eval_assert cf (v : typed_value) : m_fun = fun ctx -> - assert (v.ty = TLiteral TBool); + sanity_check __FILE__ __LINE__ (v.ty = TLiteral TBool) meta; (* We make a choice here: we could completely decouple the concrete and * symbolic executions here but choose not to. In the case where we * know the concrete value of the boolean we test, we use this value @@ -175,25 +182,26 @@ let eval_assertion (config : config) (assertion : assertion) : st_cm_fun = match v.value with | VLiteral (VBool _) -> (* Delegate to the concrete evaluation function *) - eval_assertion_concrete config assertion cf ctx + eval_assertion_concrete config meta assertion cf ctx | VSymbolic sv -> - assert (config.mode = SymbolicMode); - assert (sv.sv_ty = TLiteral TBool); + sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; + sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral TBool) meta; (* We continue the execution as if the test had succeeded, and thus * perform the symbolic expansion: sv ~~> true. * We will of course synthesize an assertion in the generated code * (see below). *) let ctx = - apply_symbolic_expansion_non_borrow config sv (SeLiteral (VBool true)) - ctx + apply_symbolic_expansion_non_borrow config meta sv + (SeLiteral (VBool true)) ctx in (* Continue *) let expr = cf Unit ctx in (* Add the synthesized assertion *) S.synthesize_assertion ctx v expr | _ -> - raise - (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v)) + craise __FILE__ __LINE__ meta + ("Expected a boolean, got: " + ^ typed_value_to_string ~meta:(Some meta) ctx v) in (* Compose and apply *) comp eval_op eval_assert cf ctx @@ -209,19 +217,20 @@ let eval_assertion (config : config) (assertion : assertion) : st_cm_fun = a variant with all its fields set to {!Bottom}. For instance, something like: [Cons Bottom Bottom]. *) -let set_discriminant (config : config) (p : place) (variant_id : VariantId.id) : - st_cm_fun = +let set_discriminant (config : config) (meta : Meta.meta) (p : place) + (variant_id : VariantId.id) : st_cm_fun = fun cf ctx -> log#ldebug (lazy ("set_discriminant:" ^ "\n- p: " ^ place_to_string ctx p ^ "\n- variant id: " ^ VariantId.to_string variant_id - ^ "\n- initial context:\n" ^ eval_ctx_to_string ctx)); + ^ "\n- initial context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Access the value *) let access = Write in - let cc = update_ctx_along_read_place config access p in - let cc = comp cc (prepare_lplace config p) in + let cc = update_ctx_along_read_place config meta access p in + let cc = comp cc (prepare_lplace config meta p) in (* Update the value *) let update_value cf (v : typed_value) : m_fun = fun ctx -> @@ -234,7 +243,9 @@ let set_discriminant (config : config) (p : place) (variant_id : VariantId.id) : a variant with all its fields set to {!Bottom} *) match av.variant_id with - | None -> raise (Failure "Found a struct value while expected an enum") + | None -> + craise __FILE__ __LINE__ meta + "Found a struct value while expected an enum" | Some variant_id' -> if variant_id' = variant_id then (* Nothing to do *) cf Unit ctx @@ -243,22 +254,22 @@ let set_discriminant (config : config) (p : place) (variant_id : VariantId.id) : let bottom_v = match type_id with | TAdtId def_id -> - compute_expanded_bottom_adt_value ctx def_id + compute_expanded_bottom_adt_value meta ctx def_id (Some variant_id) generics - | _ -> raise (Failure "Unreachable") + | _ -> craise __FILE__ __LINE__ meta "Unreachable" in - assign_to_place config bottom_v p (cf Unit) ctx) + assign_to_place config meta bottom_v p (cf Unit) ctx) | TAdt ((TAdtId _ as type_id), generics), VBottom -> let bottom_v = match type_id with | TAdtId def_id -> - compute_expanded_bottom_adt_value ctx def_id (Some variant_id) - generics - | _ -> raise (Failure "Unreachable") + compute_expanded_bottom_adt_value meta ctx def_id + (Some variant_id) generics + | _ -> craise __FILE__ __LINE__ meta "Unreachable" in - assign_to_place config bottom_v p (cf Unit) ctx + assign_to_place config meta bottom_v p (cf Unit) ctx | _, VSymbolic _ -> - assert (config.mode = SymbolicMode); + sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; (* This is a bit annoying: in theory we should expand the symbolic value * then set the discriminant, because in the case the discriminant is * exactly the one we set, the fields are left untouched, and in the @@ -266,10 +277,11 @@ let set_discriminant (config : config) (p : place) (variant_id : VariantId.id) : * For now, we forbid setting the discriminant of a symbolic value: * setting a discriminant should only be used to initialize a value, * or reset an already initialized value, really. *) - raise (Failure "Unexpected value") - | _, (VAdt _ | VBottom) -> raise (Failure "Inconsistent state") + craise __FILE__ __LINE__ meta "Unexpected value" + | _, (VAdt _ | VBottom) -> + craise __FILE__ __LINE__ meta "Inconsistent state" | _, (VLiteral _ | VBorrow _ | VLoan _) -> - raise (Failure "Unexpected value") + craise __FILE__ __LINE__ meta "Unexpected value" in (* Compose and apply *) comp cc update_value cf ctx @@ -284,15 +296,15 @@ let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx) (** Small helper: compute the type of the return value for a specific instantiation of an assumed function. *) -let get_assumed_function_return_type (ctx : eval_ctx) (fid : assumed_fun_id) - (generics : generic_args) : ety = - assert (generics.trait_refs = []); +let get_assumed_function_return_type (meta : Meta.meta) (ctx : eval_ctx) + (fid : assumed_fun_id) (generics : generic_args) : ety = + sanity_check __FILE__ __LINE__ (generics.trait_refs = []) meta; (* [Box::free] has a special treatment *) match fid with | BoxFree -> - assert (generics.regions = []); - assert (List.length generics.types = 1); - assert (generics.const_generics = []); + sanity_check __FILE__ __LINE__ (generics.regions = []) meta; + sanity_check __FILE__ __LINE__ (List.length generics.types = 1) meta; + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; mk_unit_ty | _ -> (* Retrieve the function's signature *) @@ -308,28 +320,28 @@ let get_assumed_function_return_type (ctx : eval_ctx) (fid : assumed_fun_id) Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self sg.output in - AssociatedTypes.ctx_normalize_erase_ty ctx ty + AssociatedTypes.ctx_normalize_erase_ty meta ctx ty -let move_return_value (config : config) (pop_return_value : bool) - (cf : typed_value option -> m_fun) : m_fun = +let move_return_value (config : config) (meta : Meta.meta) + (pop_return_value : bool) (cf : typed_value option -> m_fun) : m_fun = fun ctx -> if pop_return_value then let ret_vid = VarId.zero in - let cc = eval_operand config (Move (mk_place_from_var_id ret_vid)) in + let cc = eval_operand config meta (Move (mk_place_from_var_id ret_vid)) in cc (fun v ctx -> cf (Some v) ctx) ctx else cf None ctx -let pop_frame (config : config) (pop_return_value : bool) +let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) (cf : typed_value option -> m_fun) : m_fun = fun ctx -> (* Debug *) - log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ctx)); + log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* List the local variables, but the return variable *) let ret_vid = VarId.zero in let rec list_locals env = match env with - | [] -> raise (Failure "Inconsistent environment") + | [] -> craise __FILE__ __LINE__ meta "Inconsistent environment" | EAbs _ :: env -> list_locals env | EBinding (BDummy _, _) :: env -> list_locals env | EBinding (BVar var, _) :: env -> @@ -346,14 +358,16 @@ let pop_frame (config : config) (pop_return_value : bool) ^ "]")); (* Move the return value out of the return variable *) - let cc = move_return_value config pop_return_value in + let cc = move_return_value config meta pop_return_value in (* Sanity check *) let cc = comp_check_value cc (fun ret_value ctx -> match ret_value with | None -> () | Some ret_value -> - assert (not (bottom_in_value ctx.ended_regions ret_value))) + sanity_check __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions ret_value)) + meta) in (* Drop the outer *loans* we find in the local variables *) @@ -363,7 +377,7 @@ let pop_frame (config : config) (pop_return_value : bool) let cf_drop = List.fold_left (fun cf lid -> - drop_outer_loans_at_lplace config (mk_place_from_var_id lid) cf) + drop_outer_loans_at_lplace config meta (mk_place_from_var_id lid) cf) (cf ret_value) locals in (* Apply *) @@ -376,7 +390,7 @@ let pop_frame (config : config) (pop_return_value : bool) log#ldebug (lazy ("pop_frame: after dropping outer loans in local variables:\n" - ^ eval_ctx_to_string ctx))) + ^ eval_ctx_to_string ~meta:(Some meta) ctx))) in (* Pop the frame - we remove the [Frame] delimiter, and reintroduce all @@ -384,7 +398,7 @@ let pop_frame (config : config) (pop_return_value : bool) * no outer loans) as dummy variables in the caller frame *) let rec pop env = match env with - | [] -> raise (Failure "Inconsistent environment") + | [] -> craise __FILE__ __LINE__ meta "Inconsistent environment" | EAbs abs :: env -> EAbs abs :: pop env | EBinding (_, v) :: env -> let vid = fresh_dummy_var_id () in @@ -401,15 +415,17 @@ let pop_frame (config : config) (pop_return_value : bool) comp cc cf_pop cf ctx (** Pop the current frame and assign the returned value to its destination. *) -let pop_frame_assign (config : config) (dest : place) : cm_fun = - let cf_pop = pop_frame config true in +let pop_frame_assign (config : config) (meta : Meta.meta) (dest : place) : + cm_fun = + let cf_pop = pop_frame config meta true in let cf_assign cf ret_value : m_fun = - assign_to_place config (Option.get ret_value) dest cf + assign_to_place config meta (Option.get ret_value) dest cf in comp cf_pop cf_assign (** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun = +let eval_box_new_concrete (config : config) (meta : Meta.meta) + (generics : generic_args) : cm_fun = fun cf ctx -> (* Check and retrieve the arguments *) match @@ -422,11 +438,13 @@ let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun = :: EBinding (_ret_var, _) :: EFrame :: _ ) -> (* Required type checking *) - assert (input_value.ty = boxed_ty); + cassert __FILE__ __LINE__ + (input_value.ty = boxed_ty) + meta "The input given to Box::new doesn't have the proper type"; (* Move the input value *) let cf_move = - eval_operand config (Move (mk_place_from_var_id input_var.index)) + eval_operand config meta (Move (mk_place_from_var_id input_var.index)) in (* Create the new box *) @@ -437,11 +455,11 @@ let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun = let box_v = VAdt { variant_id = None; field_values = [ moved_input_value ] } in - let box_v = mk_typed_value box_ty box_v in + let box_v = mk_typed_value meta box_ty box_v in (* Move this value to the return variable *) let dest = mk_place_from_var_id VarId.zero in - let cf_assign = assign_to_place config box_v dest in + let cf_assign = assign_to_place config meta box_v dest in (* Continue *) cf_assign cf @@ -449,7 +467,7 @@ let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun = (* Compose and apply *) comp cf_move cf_create cf ctx - | _ -> raise (Failure "Inconsistent state") + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" (** Auxiliary function - see {!eval_assumed_function_call}. @@ -470,40 +488,43 @@ let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun = It thus updates the box value (by calling {!drop_value}) and updates the destination (by setting it to [()]). *) -let eval_box_free (config : config) (generics : generic_args) +let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args) (args : operand list) (dest : place) : cm_fun = fun cf ctx -> match (generics.regions, generics.types, generics.const_generics, args) with | [], [ boxed_ty ], [], [ Move input_box_place ] -> (* Required type checking *) - let input_box = InterpreterPaths.read_place Write input_box_place ctx in + let input_box = + InterpreterPaths.read_place meta Write input_box_place ctx + in (let input_ty = ty_get_box input_box.ty in - assert (input_ty = boxed_ty)); + sanity_check __FILE__ __LINE__ (input_ty = boxed_ty)) + meta; (* Drop the value *) - let cc = drop_value config input_box_place in + let cc = drop_value config meta input_box_place in (* Update the destination by setting it to [()] *) - let cc = comp cc (assign_to_place config mk_unit_value dest) in + let cc = comp cc (assign_to_place config meta mk_unit_value dest) in (* Continue *) cc cf ctx - | _ -> raise (Failure "Inconsistent state") + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" (** Evaluate a non-local function call in concrete mode *) -let eval_assumed_function_call_concrete (config : config) (fid : assumed_fun_id) - (call : call) : cm_fun = +let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) + (fid : assumed_fun_id) (call : call) : cm_fun = let args = call.args in let dest = call.dest in match call.func with | FnOpMove _ -> (* Closure case: TODO *) - raise (Failure "Closures are not supported yet") + craise __FILE__ __LINE__ meta "Closures are not supported yet" | FnOpRegular func -> ( let generics = func.generics in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) - assert (generics.const_generics = []); + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; (* There are two cases (and this is extremely annoying): - the function is not box_free - the function is box_free @@ -512,12 +533,12 @@ let eval_assumed_function_call_concrete (config : config) (fid : assumed_fun_id) match fid with | BoxFree -> (* Degenerate case: box_free *) - eval_box_free config generics args dest + eval_box_free config meta generics args dest | _ -> (* "Normal" case: not box_free *) (* Evaluate the operands *) (* let ctx, args_vl = eval_operands config ctx args in *) - let cf_eval_ops = eval_operands config args in + let cf_eval_ops = eval_operands config meta args in (* Evaluate the call * @@ -534,9 +555,11 @@ let eval_assumed_function_call_concrete (config : config) (fid : assumed_fun_id) (* Create and push the return variable *) let ret_vid = VarId.zero in - let ret_ty = get_assumed_function_return_type ctx fid generics in + let ret_ty = + get_assumed_function_return_type meta ctx fid generics + in let ret_var = mk_var ret_vid (Some "@return") ret_ty in - let cc = comp cc (push_uninitialized_var ret_var) in + let cc = comp cc (push_uninitialized_var meta ret_var) in (* Create and push the input variables *) let input_vars = @@ -544,27 +567,27 @@ let eval_assumed_function_call_concrete (config : config) (fid : assumed_fun_id) (fun id (v : typed_value) -> (mk_var id None v.ty, v)) args_vl in - let cc = comp cc (push_vars input_vars) in + let cc = comp cc (push_vars meta input_vars) in (* "Execute" the function body. As the functions are assumed, here we call * custom functions to perform the proper manipulations: we don't have * access to a body. *) let cf_eval_body : cm_fun = match fid with - | BoxNew -> eval_box_new_concrete config generics + | BoxNew -> eval_box_new_concrete config meta generics | BoxFree -> (* Should have been treated above *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut -> - raise (Failure "Unimplemented") + craise __FILE__ __LINE__ meta "Unimplemented" in let cc = comp cc cf_eval_body in (* Pop the frame *) - let cc = comp cc (pop_frame_assign config dest) in + let cc = comp cc (pop_frame_assign config meta dest) in (* Continue *) cc cf ctx @@ -727,8 +750,8 @@ let create_push_abstractions_from_abs_region_groups which means that whenever we call a provided trait method, we do not refer to a trait clause but directly to the method provided in the trait declaration. *) -let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) - : +let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) + (call : call) (ctx : eval_ctx) : fun_id_or_trait_method_ref * generic_args * (generic_args * trait_instance_id) option @@ -738,7 +761,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) match call.func with | FnOpMove _ -> (* Closure case: TODO *) - raise (Failure "Closures are not supported yet") + craise __FILE__ __LINE__ meta "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular fid) -> @@ -756,13 +779,13 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) ctx.fun_ctx.regions_hierarchies in let inst_sg = - instantiate_fun_sig ctx func.generics tr_self def.signature + instantiate_fun_sig meta ctx func.generics tr_self def.signature regions_hierarchy in (func.func, func.generics, None, def, regions_hierarchy, inst_sg) | FunId (FAssumed _) -> (* Unreachable: must be a transparent function *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" | TraitMethod (trait_ref, method_name, _) -> ( log#ldebug (lazy @@ -803,7 +826,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) ctx.fun_ctx.regions_hierarchies in let inst_sg = - instantiate_fun_sig ctx generics tr_self + instantiate_fun_sig meta ctx generics tr_self method_def.signature regions_hierarchy in (* Also update the function identifier: we want to forget @@ -822,7 +845,9 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) | None -> (* If not found, lookup the methods provided by the trait *declaration* (remember: for now, we forbid overriding provided methods) *) - assert (trait_impl.provided_methods = []); + cassert __FILE__ __LINE__ + (trait_impl.provided_methods = []) + meta "Overriding provided methods is currently forbidden"; let trait_decl = ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id @@ -869,7 +894,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) in let tr_self = TraitRef trait_ref in let inst_sg = - instantiate_fun_sig ctx all_generics tr_self + instantiate_fun_sig meta ctx all_generics tr_self method_def.signature regions_hierarchy in ( func.func, @@ -911,8 +936,8 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) in let tr_self = TraitRef trait_ref in let inst_sg = - instantiate_fun_sig ctx generics tr_self method_def.signature - regions_hierarchy + instantiate_fun_sig meta ctx generics tr_self + method_def.signature regions_hierarchy in ( func.func, func.generics, @@ -929,15 +954,17 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = (lazy ("\n**About to evaluate statement**: [\n" ^ statement_to_string_with_tab ctx st - ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string ctx ^ "\n\n")); + ^ "\n]\n\n**Context**:\n" + ^ eval_ctx_to_string ~meta:(Some st.meta) ctx + ^ "\n\n")); (* Take a snapshot of the current context for the purpose of generating pretty names *) let cc = S.cf_save_snapshot in (* Expand the symbolic values if necessary - we need to do that before * checking the invariants *) - let cc = comp cc (greedy_expand_symbolic_values config) in + let cc = comp cc (greedy_expand_symbolic_values config st.meta) in (* Sanity check *) - let cc = comp cc Invariants.cf_check_invariants in + let cc = comp cc (Invariants.cf_check_invariants st.meta) in (* Evaluate *) let cf_eval_st cf : m_fun = @@ -956,44 +983,48 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = eval_global config p gid generics cf ctx | _ -> (* Evaluate the rvalue *) - let cf_eval_rvalue = eval_rvalue_not_global config rvalue in + let cf_eval_rvalue = eval_rvalue_not_global config st.meta rvalue in (* Assign *) let cf_assign cf (res : (typed_value, eval_error) result) ctx = log#ldebug (lazy ("about to assign to place: " ^ place_to_string ctx p - ^ "\n- Context:\n" ^ eval_ctx_to_string ctx)); + ^ "\n- Context:\n" + ^ eval_ctx_to_string ~meta:(Some st.meta) ctx)); match res with | Error EPanic -> cf Panic ctx | Ok rv -> ( - let expr = assign_to_place config rv p (cf Unit) ctx in + let expr = + assign_to_place config st.meta rv p (cf Unit) ctx + in (* Update the synthesized AST - here we store meta-information. * We do it only in specific cases (it is not always useful, and * also it can lead to issues - for instance, if we borrow a * reserved borrow, we later can't translate it to pure values...) *) match rvalue with - | Global _ -> raise (Failure "Unreachable") + | Global _ -> craise __FILE__ __LINE__ st.meta "Unreachable" | Use _ | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> let rp = rvalue_get_place rvalue in let rp = match rp with - | Some rp -> Some (S.mk_mplace rp ctx) + | Some rp -> Some (S.mk_mplace st.meta rp ctx) | None -> None in - S.synthesize_assignment ctx (S.mk_mplace p ctx) rv rp expr - ) + S.synthesize_assignment ctx + (S.mk_mplace st.meta p ctx) + rv rp expr) in (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx) - | FakeRead p -> eval_fake_read config p (cf Unit) ctx + | FakeRead p -> eval_fake_read config st.meta p (cf Unit) ctx | SetDiscriminant (p, variant_id) -> - set_discriminant config p variant_id cf ctx - | Drop p -> drop_value config p (cf Unit) ctx - | Assert assertion -> eval_assertion config assertion cf ctx - | Call call -> eval_function_call config call cf ctx + set_discriminant config st.meta p variant_id cf ctx + | Drop p -> drop_value config st.meta p (cf Unit) ctx + | Assert assertion -> eval_assertion config st.meta assertion cf ctx + | Call call -> eval_function_call config st.meta call cf ctx | Panic -> cf Panic ctx | Return -> cf Return ctx | Break i -> cf (Break i) ctx @@ -1018,7 +1049,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = InterpreterLoops.eval_loop config st.meta (eval_statement config loop_body) cf ctx - | Switch switch -> eval_switch config switch cf ctx + | Switch switch -> eval_switch config st.meta switch cf ctx in (* Compose and apply *) comp cc cf_eval_st cf ctx @@ -1032,11 +1063,14 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) (* 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 + (eval_transparent_function_call_concrete config global.meta 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); + cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.meta + "Const globals should not contain regions"; (* Instantiate the type *) (* There shouldn't be any reference to Self *) let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in @@ -1048,15 +1082,18 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) 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 sval = mk_fresh_symbolic_value global.meta ty in let cc = - assign_to_place config (mk_typed_value_from_symbolic_value sval) dest + assign_to_place config global.meta + (mk_typed_value_from_symbolic_value sval) + dest in let e = cc (cf Unit) ctx in S.synthesize_global_eval gid generics sval e (** Evaluate a switch *) -and eval_switch (config : config) (switch : switch) : st_cm_fun = +and eval_switch (config : config) (meta : Meta.meta) (switch : switch) : + st_cm_fun = fun cf ctx -> (* We evaluate the operand in two steps: * first we prepare it, then we check if its value is concrete or @@ -1072,7 +1109,7 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = match switch with | If (op, st1, st2) -> (* Evaluate the operand *) - let cf_eval_op = eval_operand config op in + let cf_eval_op = eval_operand config meta op in (* Switch on the value *) let cf_if (cf : st_m_fun) (op_v : typed_value) : m_fun = fun ctx -> @@ -1091,16 +1128,16 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = * the branches *) let cf_true : st_cm_fun = eval_statement config st1 in let cf_false : st_cm_fun = eval_statement config st2 in - expand_symbolic_bool config sv - (S.mk_opt_place_from_op op ctx) + expand_symbolic_bool config meta sv + (S.mk_opt_place_from_op meta op ctx) cf_true cf_false cf ctx - | _ -> raise (Failure "Inconsistent state") + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" in (* Compose *) comp cf_eval_op cf_if cf ctx | SwitchInt (op, int_ty, stgts, otherwise) -> (* Evaluate the operand *) - let cf_eval_op = eval_operand config op in + let cf_eval_op = eval_operand config meta op in (* Switch on the value *) let cf_switch (cf : st_m_fun) (op_v : typed_value) : m_fun = fun ctx -> @@ -1109,7 +1146,7 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = (* Evaluate the branch *) let cf_eval_branch cf = (* Sanity check *) - assert (sv.int_ty = int_ty); + sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta; (* Find the branch *) match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with | None -> eval_statement config otherwise cf @@ -1138,10 +1175,10 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = (* Translate the otherwise branch *) let otherwise = eval_statement config otherwise in (* Expand and continue *) - expand_symbolic_int config sv - (S.mk_opt_place_from_op op ctx) + expand_symbolic_int config meta sv + (S.mk_opt_place_from_op meta op ctx) int_ty stgts otherwise cf ctx - | _ -> raise (Failure "Inconsistent state") + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" in (* Compose *) comp cf_eval_op cf_switch cf ctx @@ -1150,7 +1187,8 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = let access = Read in let expand_prim_copy = false in let cf_read_p cf : m_fun = - access_rplace_reorganize_and_read config expand_prim_copy access p cf + access_rplace_reorganize_and_read config meta expand_prim_copy access + p cf in (* Match on the value *) let cf_match (cf : st_m_fun) (p_v : typed_value) : m_fun = @@ -1167,18 +1205,19 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with | None -> ( match otherwise with - | None -> raise (Failure "No otherwise branch") + | None -> craise __FILE__ __LINE__ meta "No otherwise branch" | Some otherwise -> eval_statement config otherwise cf ctx) | Some (_, tgt) -> eval_statement config tgt cf ctx) | VSymbolic sv -> (* Expand the symbolic value - may lead to branching *) let cf_expand = - expand_symbolic_adt config sv (Some (S.mk_mplace p ctx)) + expand_symbolic_adt config meta sv + (Some (S.mk_mplace meta p ctx)) in (* Re-evaluate the switch - the value is not symbolic anymore, which means we will go to the other branch *) - cf_expand (eval_switch config switch) cf ctx - | _ -> raise (Failure "Inconsistent state") + cf_expand (eval_switch config meta switch) cf ctx + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" in (* Compose *) comp cf_read_p cf_match cf ctx @@ -1187,54 +1226,57 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = cf_match cf ctx (** Evaluate a function call (auxiliary helper for [eval_statement]) *) -and eval_function_call (config : config) (call : call) : st_cm_fun = +and eval_function_call (config : config) (meta : Meta.meta) (call : call) : + st_cm_fun = (* There are several cases: - this is a local function, in which case we execute its body - this is an assumed function, in which case there is a special treatment - this is a trait method *) match config.mode with - | ConcreteMode -> eval_function_call_concrete config call - | SymbolicMode -> eval_function_call_symbolic config call + | ConcreteMode -> eval_function_call_concrete config meta call + | SymbolicMode -> eval_function_call_symbolic config meta call -and eval_function_call_concrete (config : config) (call : call) : st_cm_fun = +and eval_function_call_concrete (config : config) (meta : Meta.meta) + (call : call) : st_cm_fun = fun cf ctx -> match call.func with - | FnOpMove _ -> raise (Failure "Closures are not supported yet") + | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular fid) -> - eval_transparent_function_call_concrete config fid call cf ctx + eval_transparent_function_call_concrete config meta fid call cf ctx | FunId (FAssumed fid) -> (* Continue - note that we do as if the function call has been successful, * by giving {!Unit} to the continuation, because we place us in the case * where we haven't panicked. Of course, the translation needs to take the * panic case into account... *) - eval_assumed_function_call_concrete config fid call (cf Unit) ctx - | TraitMethod _ -> raise (Failure "Unimplemented")) + eval_assumed_function_call_concrete config meta fid call (cf Unit) ctx + | TraitMethod _ -> craise __FILE__ __LINE__ meta "Unimplemented") -and eval_function_call_symbolic (config : config) (call : call) : st_cm_fun = +and eval_function_call_symbolic (config : config) (meta : Meta.meta) + (call : call) : st_cm_fun = match call.func with - | FnOpMove _ -> raise (Failure "Closures are not supported yet") + | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular _) | TraitMethod _ -> - eval_transparent_function_call_symbolic config call + eval_transparent_function_call_symbolic config meta call | FunId (FAssumed fid) -> - eval_assumed_function_call_symbolic config fid call func) + eval_assumed_function_call_symbolic config meta fid call func) (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) -and eval_transparent_function_call_concrete (config : config) +and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta) (fid : FunDeclId.id) (call : call) : st_cm_fun = let args = call.args in let dest = call.dest in match call.func with - | FnOpMove _ -> raise (Failure "Closures are not supported yet") + | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" | FnOpRegular func -> let generics = func.generics in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) - assert (generics.const_generics = []); + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; fun cf ctx -> (* Retrieve the (correctly instantiated) body *) let def = ctx_lookup_fun_decl ctx fid in @@ -1242,14 +1284,14 @@ and eval_transparent_function_call_concrete (config : config) let body = match def.body with | None -> - raise - (Failure - ("Can't evaluate a call to an opaque function: " - ^ name_to_string ctx def.name)) + craise __FILE__ __LINE__ meta + ("Can't evaluate a call to an opaque function: " + ^ name_to_string ctx def.name) | Some body -> body in (* TODO: we need to normalize the types if we want to correctly support traits *) - assert (generics.trait_refs = []); + cassert __FILE__ __LINE__ (generics.trait_refs = []) body.meta + "Traits are not supported yet in concrete mode"; (* There shouldn't be any reference to Self *) let tr_self = UnknownTrait __FUNCTION__ in let subst = @@ -1258,8 +1300,10 @@ and eval_transparent_function_call_concrete (config : config) let locals, body_st = Subst.fun_body_substitute_in_body subst body in (* Evaluate the input operands *) - assert (List.length args = body.arg_count); - let cc = eval_operands config args in + sanity_check __FILE__ __LINE__ + (List.length args = body.arg_count) + body.meta; + let cc = eval_operands config body.meta args in (* Push a frame delimiter - we use {!comp_transmit} to transmit the result * of the operands evaluation from above to the functions afterwards, while @@ -1271,14 +1315,15 @@ and eval_transparent_function_call_concrete (config : config) let ret_var, locals = match locals with | ret_ty :: locals -> (ret_ty, locals) - | _ -> raise (Failure "Unreachable") + | _ -> craise __FILE__ __LINE__ meta "Unreachable" in let input_locals, locals = Collections.List.split_at locals body.arg_count in let cc = - comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) + comp_transmit cc + (push_var meta ret_var (mk_bottom meta ret_var.var_ty)) in (* 2. Push the input values *) @@ -1286,12 +1331,12 @@ and eval_transparent_function_call_concrete (config : config) let inputs = List.combine input_locals args in (* Note that this function checks that the variables and their values * have the same type (this is important) *) - push_vars inputs cf + push_vars meta inputs cf in let cc = comp cc cf_push_inputs in (* 3. Push the remaining local variables (initialized as {!Bottom}) *) - let cc = comp cc (push_uninitialized_vars locals) in + let cc = comp cc (push_uninitialized_vars meta locals) in (* Execute the function body *) let cc = comp cc (eval_function_body config body_st) in @@ -1303,10 +1348,10 @@ and eval_transparent_function_call_concrete (config : config) | Return -> (* Pop the stack frame, retrieve the return value, move it to * its destination and continue *) - pop_frame_assign config dest (cf Unit) + pop_frame_assign config meta dest (cf Unit) | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" in let cc = comp cc cf_finish in @@ -1314,16 +1359,18 @@ and eval_transparent_function_call_concrete (config : config) cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) -and eval_transparent_function_call_symbolic (config : config) (call : call) : - st_cm_fun = +and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) + (call : call) : st_cm_fun = fun cf ctx -> let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg = - eval_transparent_function_call_symbolic_inst call ctx + eval_transparent_function_call_symbolic_inst meta call ctx in (* Sanity check *) - assert (List.length call.args = List.length def.signature.inputs); + sanity_check __FILE__ __LINE__ + (List.length call.args = List.length def.signature.inputs) + def.meta; (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config func def.signature + eval_function_call_symbolic_from_inst_sig config def.meta func def.signature regions_hierarchy inst_sg generics trait_method_generics call.args call.dest cf ctx @@ -1339,7 +1386,7 @@ and eval_transparent_function_call_symbolic (config : config) (call : call) : trait ref as input. *) and eval_function_call_symbolic_from_inst_sig (config : config) - (fid : fun_id_or_trait_method_ref) (sg : fun_sig) + (meta : Meta.meta) (fid : fun_id_or_trait_method_ref) (sg : fun_sig) (regions_hierarchy : region_var_groups) (inst_sg : inst_fun_sig) (generics : generic_args) (trait_method_generics : (generic_args * trait_instance_id) option) @@ -1359,16 +1406,18 @@ and eval_function_call_symbolic_from_inst_sig (config : config) (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.output in - let ret_spc = mk_fresh_symbolic_value ret_sv_ty in + let ret_spc = mk_fresh_symbolic_value meta ret_sv_ty in let ret_value = mk_typed_value_from_symbolic_value ret_spc in let ret_av regions = mk_aproj_loans_value_from_symbolic_value regions ret_spc in - let args_places = List.map (fun p -> S.mk_opt_place_from_op p ctx) args in - let dest_place = Some (S.mk_mplace dest ctx) in + let args_places = + List.map (fun p -> S.mk_opt_place_from_op meta p ctx) args + in + let dest_place = Some (S.mk_mplace meta dest ctx) in (* Evaluate the input operands *) - let cc = eval_operands config args in + let cc = eval_operands config meta args in (* Generate the abstractions and insert them in the context *) let abs_ids = List.map (fun rg -> rg.id) inst_sg.regions_hierarchy in @@ -1377,20 +1426,22 @@ and eval_function_call_symbolic_from_inst_sig (config : config) let args_with_rtypes = List.combine args inst_sg.inputs in (* Check the type of the input arguments *) - assert ( - List.for_all - (fun ((arg, rty) : typed_value * rty) -> - arg.ty = Subst.erase_regions rty) - args_with_rtypes); + cassert __FILE__ __LINE__ + (List.for_all + (fun ((arg, rty) : typed_value * rty) -> + arg.ty = Subst.erase_regions rty) + args_with_rtypes) + meta "The input arguments don't have the proper type"; (* Check that the input arguments don't contain symbolic values that can't * be fed to functions (i.e., symbolic values output from function return * values and which contain borrows of borrows can't be used as function * inputs *) - assert ( - List.for_all - (fun arg -> - not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) - args); + sanity_check __FILE__ __LINE__ + (List.for_all + (fun arg -> + not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) + args) + meta; (* Initialize the abstractions and push them in the context. * First, we define the function which, given an initialized, empty @@ -1402,7 +1453,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) let ctx, args_projs = List.fold_left_map (fun ctx (arg, arg_rty) -> - apply_proj_borrows_on_input_value config ctx abs.regions + apply_proj_borrows_on_input_value config meta ctx abs.regions abs.ancestors_regions arg arg_rty) ctx args_with_rtypes in @@ -1429,7 +1480,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) let cc = comp cc cf_call in (* Move the return value to its destination *) - let cc = comp cc (assign_to_place config ret_value dest) in + let cc = comp cc (assign_to_place config meta ret_value dest) in (* End the abstractions which don't contain loans and don't have parent * abstractions. @@ -1450,7 +1501,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) (* Check if it contains non-ignored loans *) && Option.is_none (InterpreterBorrowsCore - .get_first_non_ignored_aloan_in_abstraction abs)) + .get_first_non_ignored_aloan_in_abstraction meta abs)) !abs_ids in (* Check if there are abstractions to end *) @@ -1459,7 +1510,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) abs_ids := with_loans_abs; (* End the abstractions which can be ended *) let no_loans_abs = AbstractionId.Set.of_list no_loans_abs in - let cc = InterpreterBorrows.end_abstractions config no_loans_abs in + let cc = InterpreterBorrows.end_abstractions config meta no_loans_abs in (* Recursive call *) let cc = comp cc end_abs_with_no_loans in (* Continue *) @@ -1485,18 +1536,19 @@ and eval_function_call_symbolic_from_inst_sig (config : config) cc (cf Unit) ctx (** Evaluate a non-local function call in symbolic mode *) -and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) - (call : call) (func : fn_ptr) : st_cm_fun = +and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) + (fid : assumed_fun_id) (call : call) (func : fn_ptr) : st_cm_fun = fun cf ctx -> let generics = func.generics in let args = call.args in let dest = call.dest in (* Sanity check: make sure the type parameters don't contain regions - * this is a current limitation of our synthesis *) - assert ( - List.for_all - (fun ty -> not (ty_has_borrows ctx.type_ctx.type_infos ty)) - generics.types); + sanity_check __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_borrows ctx.type_ctx.type_infos ty)) + generics.types) + meta; (* There are two cases (and this is extremely annoying): - the function is not box_free @@ -1507,7 +1559,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) | BoxFree -> (* Degenerate case: box_free - note that this is not really a function * call: no need to call a "synthesize_..." function *) - eval_box_free config generics args dest (cf Unit) ctx + eval_box_free config meta generics args dest (cf Unit) ctx | _ -> (* "Normal" case: not box_free *) (* In symbolic mode, the behaviour of a function call is completely defined @@ -1517,7 +1569,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) match fid with | BoxFree -> (* Should have been treated above *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" | _ -> let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FAssumed fid) @@ -1527,14 +1579,15 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) let tr_self = UnknownTrait __FUNCTION__ in let sg = Assumed.get_assumed_fun_sig fid in let inst_sg = - instantiate_fun_sig ctx generics tr_self sg regions_hierarchy + instantiate_fun_sig meta ctx generics tr_self sg regions_hierarchy in (sg, regions_hierarchy, inst_sg) in (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config (FunId (FAssumed fid)) sg - regions_hierarchy inst_sig generics None args dest cf ctx + eval_function_call_symbolic_from_inst_sig config meta + (FunId (FAssumed fid)) sg regions_hierarchy inst_sig generics None args + dest cf ctx (** Evaluate a statement seen as a function body *) and eval_function_body (config : config) (body : statement) : st_cm_fun = @@ -1547,9 +1600,10 @@ and eval_function_body (config : config) (body : statement) : st_cm_fun = * delegate the check to the caller. *) (* Expand the symbolic values if necessary - we need to do that before * checking the invariants *) - let cc = greedy_expand_symbolic_values config in + let cc = greedy_expand_symbolic_values config body.meta in (* Sanity check *) - let cc = comp_check_ctx cc Invariants.check_invariants in + let cc = comp_check_ctx cc (Invariants.check_invariants body.meta) in + (* Check if right meta *) (* Continue *) cc (cf res) in diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli index 3832d02f..7a2783bb 100644 --- a/compiler/InterpreterStatements.mli +++ b/compiler/InterpreterStatements.mli @@ -16,7 +16,8 @@ open Cps If the boolean is false, we don't move the return value, and call the continuation with [None]. *) -val pop_frame : config -> bool -> (typed_value option -> m_fun) -> m_fun +val pop_frame : + config -> Meta.meta -> bool -> (typed_value option -> m_fun) -> m_fun (** Helper. |