diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 185 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.mli | 12 |
2 files changed, 99 insertions, 98 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 51be904f..f82c7130 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -11,6 +11,7 @@ open Cps open InterpreterUtils open InterpreterExpansion open InterpreterPaths +open Errors (** The local logger *) let log = Logging.expressions_log @@ -29,14 +30,14 @@ let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config) (* Small helper *) let rec expand : cm_fun = fun cf ctx -> - let v = read_place access p ctx in + let v = read_place meta access p ctx in match find_first_primitively_copyable_sv_with_borrows ctx.type_ctx.type_infos v with | None -> cf ctx | Some sv -> let cc = - expand_symbolic_value_no_branching config sv (Some (mk_mplace meta p ctx)) + expand_symbolic_value_no_branching meta config sv (Some (mk_mplace meta p ctx)) in comp cc expand cf ctx in @@ -48,14 +49,14 @@ let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config) We also check that the value *doesn't contain bottoms or reserved borrows*. *) -let read_place (access : access_kind) (p : place) (cf : typed_value -> m_fun) : +let read_place (meta : Meta.meta) (access : access_kind) (p : place) (cf : typed_value -> m_fun) : m_fun = fun ctx -> - let v = read_place access p ctx in + let v = read_place meta access p ctx in (* Check that there are no bottoms in the value *) - assert (not (bottom_in_value ctx.ended_regions v)); + cassert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value"; (* Check that there are no reserved borrows in the value *) - assert (not (reserved_in_value v)); + cassert (not (reserved_in_value v)) meta "There should be no reserved borrows in the value"; (* Call the continuation *) cf v ctx @@ -64,9 +65,9 @@ let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config) (cf : typed_value -> m_fun) : m_fun = fun ctx -> (* Make sure we can evaluate the path *) - let cc = update_ctx_along_read_place config access p in + let cc = update_ctx_along_read_place meta config access p in (* End the proper loans at the place itself *) - let cc = comp cc (end_loans_at_place config access p) in + let cc = comp cc (end_loans_at_place meta config access p) in (* Expand the copyable values which contain borrows (which are necessarily shared * borrows) *) let cc = @@ -75,7 +76,7 @@ let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config) else cc in (* Read the place - note that this checks that the value doesn't contain bottoms *) - let read_place = read_place access p in + let read_place = read_place meta access p in (* Compose *) comp cc read_place cf ctx @@ -87,7 +88,7 @@ let access_rplace_reorganize (meta : Meta.meta) (config : config) (expand_prim_c ctx (** Convert an operand constant operand value to a typed value *) -let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value = +let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal) : typed_value = (* Check the type while converting - we actually need some information * contained in the type *) log#ldebug @@ -100,11 +101,11 @@ let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value = | TChar, VChar v -> { value = VLiteral (VChar v); ty = TLiteral ty } | TInteger int_ty, VScalar v -> (* Check the type and the ranges *) - assert (int_ty = v.int_ty); - assert (check_scalar_value_in_range v); + cassert (int_ty = v.int_ty) meta "Wrong type TODO: error message"; + cassert (check_scalar_value_in_range v) meta "Wrong range TODO: error message"; { value = VLiteral (VScalar v); ty = TLiteral ty } (* Remaining cases (invalid) *) - | _, _ -> raise (Failure "Improperly typed constant value") + | _, _ -> craise meta "Improperly typed constant value" (** Copy a value, and return the resulting value. @@ -117,13 +118,13 @@ let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value = parameter to control this copy ([allow_adt_copy]). Note that here by ADT we mean the user-defined ADTs (not tuples or assumed types). *) -let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx) +let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) (ctx : eval_ctx) (v : typed_value) : eval_ctx * typed_value = log#ldebug (lazy ("copy_value: " - ^ typed_value_to_string ctx v - ^ "\n- context:\n" ^ eval_ctx_to_string ctx)); + ^ typed_value_to_string meta ctx v + ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx)); (* Remark: at some point we rewrote this function to use iterators, but then * we reverted the changes: the result was less clear actually. In particular, * the fact that we have exhaustive matches below makes very obvious the cases @@ -134,9 +135,9 @@ let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx) (* Sanity check *) (match v.ty with | TAdt (TAssumed TBox, _) -> - raise (Failure "Can't copy an assumed value other than Option") + craise meta "Can't copy an assumed value other than Option" | TAdt (TAdtId _, _) as ty -> - assert (allow_adt_copy || ty_is_primitively_copyable ty) + cassert (allow_adt_copy || ty_is_primitively_copyable ty) meta "TODO: error message" | TAdt (TTuple, _) -> () (* Ok *) | TAdt ( TAssumed (TSlice | TArray), @@ -146,15 +147,15 @@ let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx) const_generics = []; trait_refs = []; } ) -> - assert (ty_is_primitively_copyable ty) - | _ -> raise (Failure "Unreachable")); + cassert (ty_is_primitively_copyable ty) meta "TODO: error message" + | _ -> craise meta "Unreachable"); let ctx, fields = List.fold_left_map - (copy_value allow_adt_copy config) + (copy_value meta allow_adt_copy config) ctx av.field_values in (ctx, { v with value = VAdt { av with field_values = fields } }) - | VBottom -> raise (Failure "Can't copy ⊥") + | VBottom -> craise meta "Can't copy ⊥" | VBorrow bc -> ( (* We can only copy shared borrows *) match bc with @@ -162,24 +163,24 @@ let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx) (* We need to create a new borrow id for the copied borrow, and * update the context accordingly *) let bid' = fresh_borrow_id () in - let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in + let ctx = InterpreterBorrows.reborrow_shared meta bid bid' ctx in (ctx, { v with value = VBorrow (VSharedBorrow bid') }) - | VMutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow") + | VMutBorrow (_, _) -> craise meta "Can't copy a mutable borrow" | VReservedMutBorrow _ -> - raise (Failure "Can't copy a reserved mut borrow")) + craise meta "Can't copy a reserved mut borrow") | VLoan lc -> ( (* We can only copy shared loans *) match lc with - | VMutLoan _ -> raise (Failure "Can't copy a mutable loan") + | VMutLoan _ -> craise meta "Can't copy a mutable loan" | VSharedLoan (_, sv) -> (* We don't copy the shared loan: only the shared value inside *) - copy_value allow_adt_copy config ctx sv) + copy_value meta allow_adt_copy config ctx sv) | VSymbolic sp -> (* We can copy only if the type is "primitively" copyable. * Note that in the general case, copy is a trait: copying values * thus requires calling the proper function. Here, we copy values * for very simple types such as integers, shared borrows, etc. *) - assert (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty)); + cassert (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty)) meta "Not primitively copyable"; (* If the type is copyable, we simply return the current value. Side * remark: what is important to look at when copying symbolic values * is symbolic expansion. The important subcase is the expansion of shared @@ -248,25 +249,25 @@ let prepare_eval_operand_reorganize (meta : Meta.meta) (config : config) (op : o prepare cf ctx (** Evaluate an operand, without reorganizing the context before *) -let eval_operand_no_reorganize (config : config) (op : operand) +let eval_operand_no_reorganize (meta : Meta.meta) (config : config) (op : operand) (cf : typed_value -> m_fun) : m_fun = fun ctx -> (* Debug *) log#ldebug (lazy ("eval_operand_no_reorganize: op: " ^ operand_to_string ctx op - ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n")); + ^ "\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n")); (* Evaluate *) match op with | Constant cv -> ( match cv.value with | CLiteral lit -> - cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx + cf (literal_to_typed_value meta (ty_as_literal cv.ty) lit) ctx | CTraitConst (trait_ref, const_name) -> ( let ctx0 = ctx in (* Simply introduce a fresh symbolic value *) let ty = cv.ty in - let v = mk_fresh_symbolic_typed_value ty in + let v = mk_fresh_symbolic_typed_value meta ty in (* Continue the evaluation *) let e = cf v ctx in (* Wrap the generated expression *) @@ -277,7 +278,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) (SymbolicAst.IntroSymbolic ( ctx0, None, - value_as_symbolic v.value, + value_as_symbolic meta v.value, SymbolicAst.VaTraitConstValue (trait_ref, const_name), e ))) | CVar vid -> ( @@ -294,49 +295,49 @@ let eval_operand_no_reorganize (config : config) (op : operand) | ConcreteMode -> (* Copy the value - this is more of a sanity check *) let allow_adt_copy = false in - copy_value allow_adt_copy config ctx cv + copy_value meta allow_adt_copy config ctx cv | SymbolicMode -> (* We use the looked up value only for its type *) - let v = mk_fresh_symbolic_typed_value cv.ty in + let v = mk_fresh_symbolic_typed_value meta cv.ty in (ctx, v) in (* Continue *) let e = cf cv ctx in (* If we are synthesizing a symbolic AST, it means that we are in symbolic mode: the value of the const generic is necessarily symbolic. *) - assert (e = None || is_symbolic cv.value); + cassert (e = None || is_symbolic cv.value) meta "The value of the const generic should be symbolic"; (* We have to wrap the generated expression *) match e with | None -> None | Some e -> (* If we are synthesizing a symbolic AST, it means that we are in symbolic mode: the value of the const generic is necessarily symbolic. *) - assert (is_symbolic cv.value); + cassert (is_symbolic cv.value) meta "The value of the const generic should be symbolic"; (* *) Some (SymbolicAst.IntroSymbolic ( ctx0, None, - value_as_symbolic cv.value, + value_as_symbolic meta cv.value, SymbolicAst.VaCgValue vid, e ))) - | CFnPtr _ -> raise (Failure "TODO")) + | CFnPtr _ -> craise meta "TODO") | Copy p -> (* Access the value *) let access = Read in - let cc = read_place access p in + let cc = read_place meta access p in (* Copy the value *) let copy cf v : m_fun = fun ctx -> (* Sanity checks *) - assert (not (bottom_in_value ctx.ended_regions v)); - assert ( + cassert (not (bottom_in_value ctx.ended_regions v)) meta "TODO: error message"; + cassert ( Option.is_none (find_first_primitively_copyable_sv_with_borrows - ctx.type_ctx.type_infos v)); + ctx.type_ctx.type_infos v)) meta "TODO: error message"; (* Actually perform the copy *) let allow_adt_copy = false in - let ctx, v = copy_value allow_adt_copy config ctx v in + let ctx, v = copy_value meta allow_adt_copy config ctx v in (* Continue *) cf v ctx in @@ -345,14 +346,14 @@ let eval_operand_no_reorganize (config : config) (op : operand) | Move p -> (* Access the value *) let access = Move in - let cc = read_place access p in + let cc = read_place meta access p in (* Move the value *) let move cf v : m_fun = fun ctx -> (* Check that there are no bottoms in the value we are about to move *) - assert (not (bottom_in_value ctx.ended_regions v)); + cassert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value we are about to move"; let bottom : typed_value = { value = VBottom; ty = v.ty } in - let ctx = write_place access p bottom ctx in + let ctx = write_place meta access p bottom ctx in cf v ctx in (* Compose and apply *) @@ -365,11 +366,11 @@ let eval_operand (meta : Meta.meta) (config : config) (op : operand) (cf : type log#ldebug (lazy ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n" - ^ eval_ctx_to_string ctx ^ "\n")); + ^ eval_ctx_to_string meta ctx ^ "\n")); (* We reorganize the context, then evaluate the operand *) comp (prepare_eval_operand_reorganize meta config op) - (eval_operand_no_reorganize config op) + (eval_operand_no_reorganize meta config op) cf ctx (** Small utility. @@ -388,7 +389,7 @@ let eval_operands (meta : Meta.meta) (config : config) (ops : operand list) let prepare = prepare_eval_operands_reorganize meta config ops in (* Evaluate the operands *) let eval = - fold_left_list_apply_continuation (eval_operand_no_reorganize config) ops + fold_left_list_apply_continuation (eval_operand_no_reorganize meta config) ops in (* Compose and apply *) comp prepare eval cf ctx @@ -399,7 +400,7 @@ let eval_two_operands (meta : Meta.meta) (config : config) (op1 : operand) (op2 let use_res cf res = match res with | [ v1; v2 ] -> cf (v1, v2) - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in comp eval_op use_res cf @@ -420,7 +421,7 @@ let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (o | ( Cast (CastScalar (TInteger src_ty, TInteger tgt_ty)), VLiteral (VScalar sv) ) -> ( (* Cast between integers *) - assert (src_ty = sv.int_ty); + cassert (src_ty = sv.int_ty) meta "TODO: error message"; let i = sv.value in match mk_scalar tgt_ty i with | Error _ -> cf (Error EPanic) @@ -442,12 +443,12 @@ let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (o let b = if Z.of_int 0 = sv.value then false else if Z.of_int 1 = sv.value then true - else raise (Failure "Conversion from int to bool: out of range") + else craise meta "Conversion from int to bool: out of range" in let value = VLiteral (VBool b) in let ty = TLiteral TBool in cf (Ok { ty; value }) - | _ -> raise (Failure "Invalid input for unop") + | _ -> craise meta "Invalid input for unop" in comp eval_op apply cf @@ -465,7 +466,7 @@ let eval_unary_op_symbolic (meta : Meta.meta) (config : config) (unop : unop) (o | Not, (TLiteral TBool as lty) -> lty | Neg, (TLiteral (TInteger _) as lty) -> lty | Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty - | _ -> raise (Failure "Invalid input for unop") + | _ -> craise meta "Invalid input for unop" in let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in (* Call the continuation *) @@ -487,15 +488,15 @@ let eval_unary_op (meta : Meta.meta) (config : config) (unop : unop) (op : opera (** Small helper for [eval_binary_op_concrete]: computes the result of applying the binop *after* the operands have been successfully evaluated *) -let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value) +let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typed_value) (v2 : typed_value) : (typed_value, eval_error) result = (* Equality check binops (Eq, Ne) accept values from a wide variety of types. * The remaining binops only operate on scalars. *) if binop = Eq || binop = Ne then ( (* Equality operations *) - assert (v1.ty = v2.ty); + cassert (v1.ty = v2.ty) meta "TODO: error message"; (* Equality/inequality check is primitive only for a subset of types *) - assert (ty_is_primitively_copyable v1.ty); + cassert (ty_is_primitively_copyable v1.ty) meta "Not primitively copyable TODO: error message"; let b = v1 = v2 in Ok { value = VLiteral (VBool b); ty = TLiteral TBool }) else @@ -510,7 +511,7 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value) match binop with | Lt | Le | Ge | Gt -> (* The two operands must have the same type and the result is a boolean *) - assert (sv1.int_ty = sv2.int_ty); + cassert (sv1.int_ty = sv2.int_ty) meta "The two operands must have the same type and the result is a boolean"; let b = match binop with | Lt -> Z.lt sv1.value sv2.value @@ -519,14 +520,14 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value) | Gt -> Z.gt sv1.value sv2.value | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl | Shr | Ne | Eq -> - raise (Failure "Unreachable") + craise meta "Unreachable" in Ok ({ value = VLiteral (VBool b); ty = TLiteral TBool } : typed_value) | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> ( (* The two operands must have the same type and the result is an integer *) - assert (sv1.int_ty = sv2.int_ty); + cassert (sv1.int_ty = sv2.int_ty) meta "The two operands must have the same type and the result is an integer"; let res = match binop with | Div -> @@ -543,7 +544,7 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value) | BitAnd -> raise Unimplemented | BitOr -> raise Unimplemented | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq -> - raise (Failure "Unreachable") + craise meta "Unreachable" in match res with | Error _ -> Error EPanic @@ -554,8 +555,8 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value) ty = TLiteral (TInteger sv1.int_ty); }) | Shl | Shr -> raise Unimplemented - | Ne | Eq -> raise (Failure "Unreachable")) - | _ -> raise (Failure "Invalid inputs for binop") + | Ne | Eq -> craise meta "Unreachable") + | _ -> craise meta "Invalid inputs for binop" let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand) (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun = @@ -564,7 +565,7 @@ let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop) (* Compute the result of the binop *) let compute cf (res : typed_value * typed_value) = let v1, v2 = res in - cf (eval_binary_op_concrete_compute binop v1 v2) + cf (eval_binary_op_concrete_compute meta binop v1 v2) in (* Compose and apply *) comp eval_ops compute cf @@ -582,9 +583,9 @@ let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop) let res_sv_ty = if binop = Eq || binop = Ne then ( (* Equality operations *) - assert (v1.ty = v2.ty); + cassert (v1.ty = v2.ty) meta "TODO: error message"; (* Equality/inequality check is primitive only for a subset of types *) - assert (ty_is_primitively_copyable v1.ty); + cassert (ty_is_primitively_copyable v1.ty) meta "Not primitively copyable TODO: error message"; TLiteral TBool) else (* Other operations: input types are integers *) @@ -592,17 +593,17 @@ let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop) | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> ( match binop with | Lt | Le | Ge | Gt -> - assert (int_ty1 = int_ty2); + cassert (int_ty1 = int_ty2) meta "TODO: error message"; TLiteral TBool | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> - assert (int_ty1 = int_ty2); + cassert (int_ty1 = int_ty2) meta "TODO: error message"; TLiteral (TInteger int_ty1) | Shl | Shr -> (* The number of bits can be of a different integer type than the operand *) TLiteral (TInteger int_ty1) - | Ne | Eq -> raise (Failure "Unreachable")) - | _ -> raise (Failure "Invalid inputs for binop") + | Ne | Eq -> craise meta "Unreachable") + | _ -> craise meta "Invalid inputs for binop" in let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in (* Call the continuattion *) @@ -631,14 +632,14 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo In practice this restricted the behaviour too much, so for now we forbid them. *) - assert (bkind <> BShallow); + cassert (bkind <> BShallow) meta "Shallow borrow are currently forbidden"; (* Access the value *) let access = match bkind with | BShared | BShallow -> Read | BTwoPhaseMut -> Write - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in let expand_prim_copy = false in @@ -663,14 +664,14 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo { v with value = v' } in (* Update the borrowed value in the context *) - let ctx = write_place access p nv ctx in + let ctx = write_place meta access p nv ctx in (* Compute the rvalue - simply a shared borrow with a the fresh id. * Note that the reference is *mutable* if we do a two-phase borrow *) let ref_kind = match bkind with | BShared | BShallow -> RShared | BTwoPhaseMut -> RMut - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in let rv_ty = TRef (RErased, v.ty, ref_kind) in let bc = @@ -680,7 +681,7 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo handle shallow borrows like shared borrows *) VSharedBorrow bid | BTwoPhaseMut -> VReservedMutBorrow bid - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in let rv : typed_value = { value = VBorrow bc; ty = rv_ty } in (* Continue *) @@ -707,7 +708,7 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo (* Compute the value with which to replace the value at place p *) let nv = { v with value = VLoan (VMutLoan bid) } in (* Update the value in the context *) - let ctx = write_place access p nv ctx in + let ctx = write_place meta access p nv ctx in (* Continue *) cf rv ctx in @@ -736,16 +737,16 @@ let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind : | TAdtId def_id -> (* Sanity checks *) let type_decl = ctx_lookup_type_decl ctx def_id in - assert ( + cassert ( List.length type_decl.generics.regions - = List.length generics.regions); + = List.length generics.regions) meta "TODO: error message"; let expected_field_types = AssociatedTypes.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id generics in - assert ( + cassert ( expected_field_types - = List.map (fun (v : typed_value) -> v.ty) values); + = List.map (fun (v : typed_value) -> v.ty) values) meta "TODO: error message"; (* Construct the value *) let av : adt_value = { variant_id = opt_variant_id; field_values = values } @@ -754,13 +755,13 @@ let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind : let aggregated : typed_value = { value = VAdt av; ty = aty } in (* Call the continuation *) cf aggregated ctx - | TAssumed _ -> raise (Failure "Unreachable")) + | TAssumed _ -> craise meta "Unreachable") | AggregatedArray (ety, cg) -> ( (* Sanity check: all the values have the proper type *) - assert (List.for_all (fun (v : typed_value) -> v.ty = ety) values); + cassert (List.for_all (fun (v : typed_value) -> v.ty = ety) values) meta "All the values do not have the proper type"; (* Sanity check: the number of values is consistent with the length *) let len = (literal_as_scalar (const_generic_as_literal cg)).value in - assert (len = Z.of_int (List.length values)); + cassert (len = Z.of_int (List.length values)) meta "The number of values is not consistent with the length"; let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in let ty = TAdt (TAssumed TArray, generics) in (* In order to generate a better AST, we introduce a symbolic @@ -768,15 +769,15 @@ let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind : array we introduce here might be duplicated in the generated code: by introducing a symbolic value we introduce a let-binding in the generated code. *) - let saggregated = mk_fresh_symbolic_typed_value ty in + let saggregated = mk_fresh_symbolic_typed_value meta ty in (* Call the continuation *) match cf saggregated ctx with | None -> None | Some e -> (* Introduce the symbolic value in the AST *) - let sv = ValuesUtils.value_as_symbolic saggregated.value in + let sv = ValuesUtils.value_as_symbolic meta saggregated.value in Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e))) - | AggregatedClosure _ -> raise (Failure "Closures are not supported yet") + | AggregatedClosure _ -> craise meta "Closures are not supported yet" in (* Compose and apply *) comp eval_ops compute cf @@ -800,11 +801,11 @@ let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue | Aggregate (aggregate_kind, ops) -> comp_wrap (eval_rvalue_aggregate meta config aggregate_kind ops) ctx | Discriminant _ -> - raise - (Failure + craise + meta "Unreachable: discriminant reads should have been eliminated from \ - the AST") - | Global _ -> raise (Failure "Unreachable") + the AST" + | Global _ -> craise meta "Unreachable" let eval_fake_read (meta : Meta.meta) (config : config) (p : place) : cm_fun = fun cf ctx -> @@ -814,7 +815,7 @@ let eval_fake_read (meta : Meta.meta) (config : config) (p : place) : cm_fun = in let cf_continue cf v : m_fun = fun ctx -> - assert (not (bottom_in_value ctx.ended_regions v)); + cassert (not (bottom_in_value ctx.ended_regions v)) meta "TODO: error message"; cf ctx in comp cf_prepare cf_continue cf ctx diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli index b975371c..69455682 100644 --- a/compiler/InterpreterExpressions.mli +++ b/compiler/InterpreterExpressions.mli @@ -12,7 +12,7 @@ open InterpreterPaths This function doesn't reorganize the context to make sure we can read the place. If needs be, you should call {!InterpreterPaths.update_ctx_along_read_place} first. *) -val read_place : access_kind -> place -> (typed_value -> m_fun) -> m_fun +val read_place : Meta.meta -> access_kind -> place -> (typed_value -> m_fun) -> m_fun (** Auxiliary function. @@ -31,7 +31,7 @@ val read_place : access_kind -> place -> (typed_value -> m_fun) -> m_fun primitively copyable and contain borrows. *) val access_rplace_reorganize_and_read : - config -> bool -> access_kind -> place -> (typed_value -> m_fun) -> m_fun + Meta.meta -> config -> bool -> access_kind -> place -> (typed_value -> m_fun) -> m_fun (** Evaluate an operand. @@ -42,11 +42,11 @@ val access_rplace_reorganize_and_read : of the environment, before evaluating all the operands at once. Use {!eval_operands} instead. *) -val eval_operand : config -> operand -> (typed_value -> m_fun) -> m_fun +val eval_operand : Meta.meta -> config -> operand -> (typed_value -> m_fun) -> m_fun (** Evaluate several operands at once. *) val eval_operands : - config -> operand list -> (typed_value list -> m_fun) -> m_fun + Meta.meta -> config -> operand list -> (typed_value list -> m_fun) -> m_fun (** Evaluate an rvalue which is not a global (globals are handled elsewhere). @@ -56,7 +56,7 @@ val eval_operands : reads should have been eliminated from the AST. *) val eval_rvalue_not_global : - config -> rvalue -> ((typed_value, eval_error) result -> m_fun) -> m_fun + Meta.meta -> config -> rvalue -> ((typed_value, eval_error) result -> m_fun) -> m_fun (** Evaluate a fake read (update the context so that we can read a place) *) -val eval_fake_read : config -> place -> cm_fun +val eval_fake_read : Meta.meta -> config -> place -> cm_fun |