From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:28:56 +0100 Subject: Remove the 'r type variable from the ty type definition --- compiler/InterpreterExpressions.ml | 90 +++++++++++++++++++------------------- 1 file changed, 44 insertions(+), 46 deletions(-) (limited to 'compiler/InterpreterExpressions.ml') diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 245f3b77..f4430c77 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -105,13 +105,13 @@ let literal_to_typed_value (ty : PV.literal_type) (cv : V.literal) : ^ Print.PrimitiveValues.literal_to_string cv)); match (ty, cv) with (* Scalar, boolean... *) - | PV.Bool, Bool v -> { V.value = V.Literal (Bool v); ty = T.Literal ty } - | Char, Char v -> { V.value = V.Literal (Char v); ty = T.Literal ty } - | Integer int_ty, PV.Scalar v -> + | PV.TBool, VBool v -> { V.value = V.VLiteral (VBool v); ty = T.TLiteral ty } + | TChar, VChar v -> { V.value = V.VLiteral (VChar v); ty = T.TLiteral ty } + | TInteger int_ty, PV.VScalar v -> (* Check the type and the ranges *) assert (int_ty = v.int_ty); assert (check_scalar_value_in_range v); - { V.value = V.Literal (PV.Scalar v); ty = T.Literal ty } + { V.value = V.VLiteral (PV.VScalar v); ty = T.TLiteral ty } (* Remaining cases (invalid) *) | _, _ -> raise (Failure "Improperly typed constant value") @@ -138,17 +138,17 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) * the fact that we have exhaustive matches below makes very obvious the cases * in which we need to fail *) match v.V.value with - | V.Literal _ -> (ctx, v) - | V.Adt av -> + | V.VLiteral _ -> (ctx, v) + | V.VAdt av -> (* Sanity check *) (match v.V.ty with - | T.Adt (T.Assumed T.Box, _) -> + | T.TAdt (T.TAssumed T.TBox, _) -> raise (Failure "Can't copy an assumed value other than Option") - | T.Adt (T.AdtId _, _) as ty -> + | T.TAdt (T.AdtId _, _) as ty -> assert (allow_adt_copy || ty_is_primitively_copyable ty) - | T.Adt (T.Tuple, _) -> () (* Ok *) - | T.Adt - ( T.Assumed (Slice | T.Array), + | T.TAdt (T.Tuple, _) -> () (* Ok *) + | T.TAdt + ( T.TAssumed (TSlice | T.TArray), { regions = []; types = [ ty ]; @@ -162,7 +162,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) (copy_value allow_adt_copy config) ctx av.field_values in - (ctx, { v with V.value = V.Adt { av with field_values = fields } }) + (ctx, { v with V.value = V.VAdt { av with field_values = fields } }) | V.Bottom -> raise (Failure "Can't copy ⊥") | V.Borrow bc -> ( (* We can only copy shared borrows *) @@ -292,7 +292,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) List.find (fun (name, _) -> name = const_name) trait_decl.consts in (* Introduce a fresh symbolic value *) - let v = mk_fresh_symbolic_typed_value_from_ety V.TraitConst ty in + let v = mk_fresh_symbolic_typed_value V.TraitConst ty in (* Continue the evaluation *) let e = cf v ctx in (* We have to wrap the generated expression *) @@ -304,7 +304,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) ( ctx0, None, value_as_symbolic v.value, - SymbolicAst.TraitConstValue + SymbolicAst.VaTraitConstValue (trait_ref, generics, const_name), e )))) | E.CVar vid -> ( @@ -329,7 +329,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) ( ctx0, None, value_as_symbolic v.value, - SymbolicAst.ConstGenericValue vid, + SymbolicAst.VaConstGenericValue vid, e ))) | E.CFnPtr _ -> raise (Failure "TODO")) | E.Copy p -> @@ -421,21 +421,21 @@ let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand) (* Apply the unop *) let apply cf (v : V.typed_value) : m_fun = match (unop, v.V.value) with - | E.Not, V.Literal (Bool b) -> - cf (Ok { v with V.value = V.Literal (Bool (not b)) }) - | E.Neg, V.Literal (PV.Scalar sv) -> ( + | E.Not, V.VLiteral (VBool b) -> + cf (Ok { v with V.value = V.VLiteral (VBool (not b)) }) + | E.Neg, V.VLiteral (PV.VScalar sv) -> ( let i = Z.neg sv.PV.value in match mk_scalar sv.int_ty i with | Error _ -> cf (Error EPanic) - | Ok sv -> cf (Ok { v with V.value = V.Literal (PV.Scalar sv) })) - | E.Cast (E.CastInteger (src_ty, tgt_ty)), V.Literal (PV.Scalar sv) -> ( + | Ok sv -> cf (Ok { v with V.value = V.VLiteral (PV.VScalar sv) })) + | E.Cast (E.CastInteger (src_ty, tgt_ty)), V.VLiteral (PV.VScalar sv) -> ( assert (src_ty = sv.int_ty); let i = sv.PV.value in match mk_scalar tgt_ty i with | Error _ -> cf (Error EPanic) | Ok sv -> - let ty = T.Literal (Integer tgt_ty) in - let value = V.Literal (PV.Scalar sv) in + let ty = T.TLiteral (TInteger tgt_ty) in + let value = V.VLiteral (PV.VScalar sv) in cf (Ok { V.ty; value })) | _ -> raise (Failure "Invalid input for unop") in @@ -452,9 +452,9 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand) let res_sv_id = C.fresh_symbolic_value_id () in let res_sv_ty = match (unop, v.V.ty) with - | E.Not, (T.Literal Bool as lty) -> lty - | E.Neg, (T.Literal (Integer _) as lty) -> lty - | E.Cast (E.CastInteger (_, tgt_ty)), _ -> T.Literal (Integer tgt_ty) + | E.Not, (T.TLiteral TBool as lty) -> lty + | E.Neg, (T.TLiteral (TInteger _) as lty) -> lty + | E.Cast (E.CastInteger (_, tgt_ty)), _ -> T.TLiteral (TInteger tgt_ty) | _ -> raise (Failure "Invalid input for unop") in let res_sv = @@ -489,11 +489,11 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value) (* Equality/inequality check is primitive only for a subset of types *) assert (ty_is_primitively_copyable v1.ty); let b = v1 = v2 in - Ok { V.value = V.Literal (Bool b); ty = T.Literal Bool }) + Ok { V.value = V.VLiteral (VBool b); ty = T.TLiteral TBool }) else (* For the non-equality operations, the input values are necessarily scalars *) match (v1.V.value, v2.V.value) with - | V.Literal (PV.Scalar sv1), V.Literal (PV.Scalar sv2) -> ( + | V.VLiteral (PV.VScalar sv1), V.VLiteral (PV.VScalar sv2) -> ( (* There are binops which require the two operands to have the same type, and binops for which it is not the case. There are also binops which return booleans, and binops which @@ -514,7 +514,7 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value) raise (Failure "Unreachable") in Ok - ({ V.value = V.Literal (Bool b); ty = T.Literal Bool } + ({ V.value = V.VLiteral (VBool b); ty = T.TLiteral TBool } : V.typed_value) | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr -> ( @@ -543,8 +543,8 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value) | Ok sv -> Ok { - V.value = V.Literal (PV.Scalar sv); - ty = T.Literal (Integer sv1.int_ty); + V.value = V.VLiteral (PV.VScalar sv); + ty = T.TLiteral (TInteger sv1.int_ty); }) | E.Shl | E.Shr -> raise Unimplemented | E.Ne | E.Eq -> raise (Failure "Unreachable")) @@ -580,19 +580,19 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop) assert (v1.ty = v2.ty); (* Equality/inequality check is primitive only for a subset of types *) assert (ty_is_primitively_copyable v1.ty); - T.Literal Bool) + T.TLiteral TBool) else (* Other operations: input types are integers *) match (v1.V.ty, v2.V.ty) with - | T.Literal (Integer int_ty1), T.Literal (Integer int_ty2) -> ( + | T.TLiteral (TInteger int_ty1), T.TLiteral (TInteger int_ty2) -> ( match binop with | E.Lt | E.Le | E.Ge | E.Gt -> assert (int_ty1 = int_ty2); - T.Literal Bool + T.TLiteral TBool | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr -> assert (int_ty1 = int_ty2); - T.Literal (Integer int_ty1) + T.TLiteral (TInteger int_ty1) | E.Shl | E.Shr -> raise Unimplemented | E.Ne | E.Eq -> raise (Failure "Unreachable")) | _ -> raise (Failure "Invalid inputs for binop") @@ -670,7 +670,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) | E.TwoPhaseMut -> T.Mut | _ -> raise (Failure "Unreachable") in - let rv_ty = T.Ref (T.Erased, v.ty, ref_kind) in + let rv_ty = T.Ref (T.RErased, v.ty, ref_kind) in let bc = match bkind with | E.Shared | E.Shallow -> @@ -698,7 +698,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) fun ctx -> (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) let bid = C.fresh_borrow_id () in - let rv_ty = T.Ref (T.Erased, v.ty, Mut) in + let rv_ty = T.Ref (T.RErased, v.ty, Mut) in let rv : V.typed_value = { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } in @@ -727,9 +727,9 @@ let eval_rvalue_aggregate (config : C.config) match type_id with | Tuple -> let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in - let v = V.Adt { variant_id = None; field_values = values } in + let v = V.VAdt { variant_id = None; field_values = values } in let generics = TypesUtils.mk_generic_args [] tys [] [] in - let ty = T.Adt (T.Tuple, generics) in + let ty = T.TAdt (T.Tuple, generics) in let aggregated : V.typed_value = { V.value = v; ty } in (* Call the continuation *) cf aggregated ctx @@ -750,11 +750,11 @@ let eval_rvalue_aggregate (config : C.config) let av : V.adt_value = { V.variant_id = opt_variant_id; V.field_values = values } in - let aty = T.Adt (T.AdtId def_id, generics) in - let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in + let aty = T.TAdt (T.AdtId def_id, generics) in + let aggregated : V.typed_value = { V.value = VAdt av; ty = aty } in (* Call the continuation *) cf aggregated ctx - | Assumed _ -> raise (Failure "Unreachable")) + | TAssumed _ -> raise (Failure "Unreachable")) | E.AggregatedArray (ety, cg) -> ( (* Sanity check: all the values have the proper type *) assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values); @@ -762,22 +762,20 @@ let eval_rvalue_aggregate (config : C.config) let len = (literal_as_scalar (const_generic_as_literal cg)).value in assert (len = Z.of_int (List.length values)); let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in - let ty = T.Adt (T.Assumed T.Array, generics) in + let ty = T.TAdt (T.TAssumed T.TArray, generics) in (* In order to generate a better AST, we introduce a symbolic value equal to the array. The reason is that otherwise, the 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_from_ety V.Aggregate ty - in + let saggregated = mk_fresh_symbolic_typed_value V.Aggregate 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 - Some (SymbolicAst.IntroSymbolic (ctx, None, sv, Array values, e))) + Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e))) in (* Compose and apply *) comp eval_ops compute cf -- cgit v1.2.3 From 0a5859fbb7bcd99bfa221eaf1af029ff660bf963 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:35:24 +0100 Subject: Rename some variants --- compiler/InterpreterExpressions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/InterpreterExpressions.ml') diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index f4430c77..c7fcc1af 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -329,7 +329,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) ( ctx0, None, value_as_symbolic v.value, - SymbolicAst.VaConstGenericValue vid, + SymbolicAst.VaCGValue vid, e ))) | E.CFnPtr _ -> raise (Failure "TODO")) | E.Copy p -> -- cgit v1.2.3 From 6ef68fa9ffd4caec09677ee2800a778080d6da34 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 20:04:11 +0100 Subject: Prefix variants related to types with "T" --- compiler/InterpreterExpressions.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'compiler/InterpreterExpressions.ml') diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index c7fcc1af..7865d7be 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -144,9 +144,9 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) (match v.V.ty with | T.TAdt (T.TAssumed T.TBox, _) -> raise (Failure "Can't copy an assumed value other than Option") - | T.TAdt (T.AdtId _, _) as ty -> + | T.TAdt (T.TAdtId _, _) as ty -> assert (allow_adt_copy || ty_is_primitively_copyable ty) - | T.TAdt (T.Tuple, _) -> () (* Ok *) + | T.TAdt (T.TTuple, _) -> () (* Ok *) | T.TAdt ( T.TAssumed (TSlice | T.TArray), { @@ -670,7 +670,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) | E.TwoPhaseMut -> T.Mut | _ -> raise (Failure "Unreachable") in - let rv_ty = T.Ref (T.RErased, v.ty, ref_kind) in + let rv_ty = T.TRef (T.RErased, v.ty, ref_kind) in let bc = match bkind with | E.Shared | E.Shallow -> @@ -698,7 +698,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) fun ctx -> (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) let bid = C.fresh_borrow_id () in - let rv_ty = T.Ref (T.RErased, v.ty, Mut) in + let rv_ty = T.TRef (T.RErased, v.ty, Mut) in let rv : V.typed_value = { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } in @@ -725,15 +725,15 @@ let eval_rvalue_aggregate (config : C.config) match aggregate_kind with | E.AggregatedAdt (type_id, opt_variant_id, generics) -> ( match type_id with - | Tuple -> + | TTuple -> let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in let v = V.VAdt { variant_id = None; field_values = values } in let generics = TypesUtils.mk_generic_args [] tys [] [] in - let ty = T.TAdt (T.Tuple, generics) in + let ty = T.TAdt (T.TTuple, generics) in let aggregated : V.typed_value = { V.value = v; ty } in (* Call the continuation *) cf aggregated ctx - | AdtId def_id -> + | TAdtId def_id -> (* Sanity checks *) let type_decl = C.ctx_lookup_type_decl ctx def_id in assert ( @@ -750,7 +750,7 @@ let eval_rvalue_aggregate (config : C.config) let av : V.adt_value = { V.variant_id = opt_variant_id; V.field_values = values } in - let aty = T.TAdt (T.AdtId def_id, generics) in + let aty = T.TAdt (T.TAdtId def_id, generics) in let aggregated : V.typed_value = { V.value = VAdt av; ty = aty } in (* Call the continuation *) cf aggregated ctx -- cgit v1.2.3 From 746239e8f29de85f848d14e44eac8690e2065a1d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 20:41:58 +0100 Subject: Add the "V" prefix to most variants related to values --- compiler/InterpreterExpressions.ml | 106 ++++++++++++++++++------------------- 1 file changed, 53 insertions(+), 53 deletions(-) (limited to 'compiler/InterpreterExpressions.ml') diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 7865d7be..58426cad 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -137,18 +137,18 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) * 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 * in which we need to fail *) - match v.V.value with - | V.VLiteral _ -> (ctx, v) - | V.VAdt av -> + match v.value with + | VLiteral _ -> (ctx, v) + | VAdt av -> (* Sanity check *) - (match v.V.ty with - | T.TAdt (T.TAssumed T.TBox, _) -> + (match v.ty with + | TAdt (TAssumed TBox, _) -> raise (Failure "Can't copy an assumed value other than Option") - | T.TAdt (T.TAdtId _, _) as ty -> + | TAdt (TAdtId _, _) as ty -> assert (allow_adt_copy || ty_is_primitively_copyable ty) - | T.TAdt (T.TTuple, _) -> () (* Ok *) - | T.TAdt - ( T.TAssumed (TSlice | T.TArray), + | TAdt (TTuple, _) -> () (* Ok *) + | TAdt + ( TAssumed (TSlice | TArray), { regions = []; types = [ ty ]; @@ -162,33 +162,33 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) (copy_value allow_adt_copy config) ctx av.field_values in - (ctx, { v with V.value = V.VAdt { av with field_values = fields } }) - | V.Bottom -> raise (Failure "Can't copy ⊥") - | V.Borrow bc -> ( + (ctx, { v with value = VAdt { av with field_values = fields } }) + | VBottom -> raise (Failure "Can't copy ⊥") + | VBorrow bc -> ( (* We can only copy shared borrows *) match bc with - | SharedBorrow bid -> + | VSharedBorrow bid -> (* We need to create a new borrow id for the copied borrow, and * update the context accordingly *) let bid' = C.fresh_borrow_id () in let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in - (ctx, { v with V.value = V.Borrow (SharedBorrow bid') }) - | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow") - | V.ReservedMutBorrow _ -> + (ctx, { v with value = VBorrow (VSharedBorrow bid') }) + | VMutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow") + | VReservedMutBorrow _ -> raise (Failure "Can't copy a reserved mut borrow")) - | V.Loan lc -> ( + | VLoan lc -> ( (* We can only copy shared loans *) match lc with - | V.MutLoan _ -> raise (Failure "Can't copy a mutable loan") - | V.SharedLoan (_, sv) -> + | VMutLoan _ -> raise (Failure "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) - | V.Symbolic sp -> + | 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 (Subst.erase_regions sp.V.sv_ty)); + assert (ty_is_primitively_copyable (Subst.erase_regions sp.sv_ty)); (* 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 @@ -239,16 +239,16 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) : let prepare : cm_fun = fun cf ctx -> match op with - | E.Constant _ -> + | Constant _ -> (* No need to reorganize the context *) cf ctx - | E.Copy p -> + | Copy p -> (* Access the value *) let access = Read in (* Expand the symbolic values, if necessary *) let expand_prim_copy = true in access_rplace_reorganize config expand_prim_copy access p cf ctx - | E.Move p -> + | Move p -> (* Access the value *) let access = Move in let expand_prim_copy = false in @@ -268,11 +268,11 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Evaluate *) match op with - | E.Constant cv -> ( + | Constant cv -> ( match cv.value with - | E.CLiteral lit -> + | CLiteral lit -> cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx - | E.CTraitConst (trait_ref, generics, const_name) -> ( + | CTraitConst (trait_ref, generics, const_name) -> ( assert (generics = TypesUtils.mk_empty_generic_args); match trait_ref.trait_id with | T.TraitImpl _ -> @@ -307,7 +307,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) SymbolicAst.VaTraitConstValue (trait_ref, generics, const_name), e )))) - | E.CVar vid -> ( + | CVar vid -> ( let ctx0 = ctx in (* Lookup the const generic value *) let cv = C.ctx_lookup_const_generic_value ctx vid in @@ -331,8 +331,8 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) value_as_symbolic v.value, SymbolicAst.VaCGValue vid, e ))) - | E.CFnPtr _ -> raise (Failure "TODO")) - | E.Copy p -> + | CFnPtr _ -> raise (Failure "TODO")) + | Copy p -> (* Access the value *) let access = Read in let cc = read_place access p in @@ -353,7 +353,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) in (* Compose and apply *) comp cc copy cf ctx - | E.Move p -> + | Move p -> (* Access the value *) let access = Move in let cc = read_place access p in @@ -362,7 +362,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) 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)); - let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in + let bottom : V.typed_value = { V.value = VBottom; ty = v.ty } in let ctx = write_place access p bottom ctx in cf v ctx in @@ -622,18 +622,18 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> match bkind with - | E.Shared | E.TwoPhaseMut | E.Shallow -> + | Shared | TwoPhaseMut | Shallow -> (* **REMARK**: we initially treated shallow borrows like shared borrows. In practice this restricted the behaviour too much, so for now we forbid them. *) - assert (bkind <> E.Shallow); + assert (bkind <> Shallow); (* Access the value *) let access = match bkind with - | E.Shared | E.Shallow -> Read - | E.TwoPhaseMut -> Write + | Shared | Shallow -> Read + | TwoPhaseMut -> Write | _ -> raise (Failure "Unreachable") in @@ -648,17 +648,17 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) let bid = C.fresh_borrow_id () in (* Compute the loan value, with which to replace the value at place p *) let nv = - match v.V.value with - | V.Loan (V.SharedLoan (bids, sv)) -> + match v.value with + | VLoan (VSharedLoan (bids, sv)) -> (* Shared loan: insert the new borrow id *) let bids1 = V.BorrowId.Set.add bid bids in - { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) } + { v with value = VLoan (VSharedLoan (bids1, sv)) } | _ -> (* Not a shared loan: add a wrapper *) let v' = - V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v)) + V.VLoan (VSharedLoan (V.BorrowId.Set.singleton bid, v)) in - { v with V.value = v' } + { v with value = v' } in (* Update the borrowed value in the context *) let ctx = write_place access p nv ctx in @@ -666,27 +666,27 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) * Note that the reference is *mutable* if we do a two-phase borrow *) let ref_kind = match bkind with - | E.Shared | E.Shallow -> T.Shared - | E.TwoPhaseMut -> T.Mut + | Shared | Shallow -> T.Shared + | TwoPhaseMut -> T.Mut | _ -> raise (Failure "Unreachable") in let rv_ty = T.TRef (T.RErased, v.ty, ref_kind) in let bc = match bkind with - | E.Shared | E.Shallow -> + | Shared | Shallow -> (* See the remark at the beginning of the match branch: we handle shallow borrows like shared borrows *) - V.SharedBorrow bid - | E.TwoPhaseMut -> V.ReservedMutBorrow bid + V.VSharedBorrow bid + | TwoPhaseMut -> VReservedMutBorrow bid | _ -> raise (Failure "Unreachable") in - let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in + let rv : V.typed_value = { value = VBorrow bc; ty = rv_ty } in (* Continue *) cf rv ctx in (* Compose and apply *) comp prepare eval cf ctx - | E.Mut -> + | Mut -> (* Access the value *) let access = Write in let expand_prim_copy = false in @@ -698,12 +698,12 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) fun ctx -> (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) let bid = C.fresh_borrow_id () in - let rv_ty = T.TRef (T.RErased, v.ty, Mut) in + let rv_ty = T.TRef (RErased, v.ty, Mut) in let rv : V.typed_value = - { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } + { V.value = VBorrow (VMutBorrow (bid, v)); ty = rv_ty } in (* Compute the value with which to replace the value at place p *) - let nv = { v with V.value = V.Loan (V.MutLoan bid) } in + let nv = { v with value = VLoan (VMutLoan bid) } in (* Update the value in the context *) let ctx = write_place access p nv ctx in (* Continue *) @@ -723,7 +723,7 @@ let eval_rvalue_aggregate (config : C.config) fun ctx -> (* Match on the aggregate kind *) match aggregate_kind with - | E.AggregatedAdt (type_id, opt_variant_id, generics) -> ( + | AggregatedAdt (type_id, opt_variant_id, generics) -> ( match type_id with | TTuple -> let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in @@ -755,7 +755,7 @@ let eval_rvalue_aggregate (config : C.config) (* Call the continuation *) cf aggregated ctx | TAssumed _ -> raise (Failure "Unreachable")) - | E.AggregatedArray (ety, cg) -> ( + | AggregatedArray (ety, cg) -> ( (* Sanity check: all the values have the proper type *) assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values); (* Sanity check: the number of values is consistent with the length *) -- cgit v1.2.3 From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 15 Nov 2023 22:03:21 +0100 Subject: Start updating the name type, cleanup the names and the module abbrevs --- compiler/InterpreterExpressions.ml | 387 ++++++++++++++++++------------------- 1 file changed, 185 insertions(+), 202 deletions(-) (limited to 'compiler/InterpreterExpressions.ml') diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 58426cad..1e28fd4b 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -1,25 +1,21 @@ -module T = Types -module PV = PrimitiveValues -module V = Values -module LA = LlbcAst +open PrimitiveValues +open Types +open Values +open LlbcAst open Scalars -module E = Expressions +open Expressions open Utils -module C = Contexts -module Subst = Substitute -module Assoc = AssociatedTypes -module L = Logging +open Contexts open TypesUtils open ValuesUtils -module Inv = Invariants -module S = SynthesizeSymbolic +open SynthesizeSymbolic open Cps open InterpreterUtils open InterpreterExpansion open InterpreterPaths (** The local logger *) -let log = L.expressions_log +let log = Logging.expressions_log (** As long as there are symbolic values at a given place (potentially in subvalues) which contain borrows and are primitively copyable, expand them. @@ -29,8 +25,8 @@ let log = L.expressions_log Note that the place should have been prepared so that there are no remaining loans. *) -let expand_primitively_copyable_at_place (config : C.config) - (access : access_kind) (p : E.place) : cm_fun = +let expand_primitively_copyable_at_place (config : config) + (access : access_kind) (p : place) : cm_fun = fun cf ctx -> (* Small helper *) let rec expand : cm_fun = @@ -43,8 +39,7 @@ let expand_primitively_copyable_at_place (config : C.config) | None -> cf ctx | Some sv -> let cc = - expand_symbolic_value_no_branching config sv - (Some (S.mk_mplace p ctx)) + expand_symbolic_value_no_branching config sv (Some (mk_mplace p ctx)) in comp cc expand cf ctx in @@ -56,8 +51,8 @@ let expand_primitively_copyable_at_place (config : C.config) We also check that the value *doesn't contain bottoms or reserved borrows*. *) -let read_place (access : access_kind) (p : E.place) - (cf : V.typed_value -> m_fun) : m_fun = +let read_place (access : access_kind) (p : place) (cf : typed_value -> m_fun) : + m_fun = fun ctx -> let v = read_place access p ctx in (* Check that there are no bottoms in the value *) @@ -67,9 +62,9 @@ let read_place (access : access_kind) (p : E.place) (* Call the continuation *) cf v ctx -let access_rplace_reorganize_and_read (config : C.config) - (expand_prim_copy : bool) (access : access_kind) (p : E.place) - (cf : V.typed_value -> m_fun) : m_fun = +let access_rplace_reorganize_and_read (config : config) + (expand_prim_copy : bool) (access : access_kind) (p : place) + (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 @@ -87,16 +82,15 @@ let access_rplace_reorganize_and_read (config : C.config) (* Compose *) comp cc read_place cf ctx -let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool) - (access : access_kind) (p : E.place) : cm_fun = +let access_rplace_reorganize (config : config) (expand_prim_copy : bool) + (access : access_kind) (p : place) : cm_fun = fun cf ctx -> access_rplace_reorganize_and_read config expand_prim_copy access p (fun _v -> cf) ctx (** Convert an operand constant operand value to a typed value *) -let literal_to_typed_value (ty : PV.literal_type) (cv : V.literal) : - V.typed_value = +let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value = (* Check the type while converting - we actually need some information * contained in the type *) log#ldebug @@ -105,13 +99,13 @@ let literal_to_typed_value (ty : PV.literal_type) (cv : V.literal) : ^ Print.PrimitiveValues.literal_to_string cv)); match (ty, cv) with (* Scalar, boolean... *) - | PV.TBool, VBool v -> { V.value = V.VLiteral (VBool v); ty = T.TLiteral ty } - | TChar, VChar v -> { V.value = V.VLiteral (VChar v); ty = T.TLiteral ty } - | TInteger int_ty, PV.VScalar v -> + | TBool, VBool v -> { value = VLiteral (VBool v); ty = TLiteral ty } + | 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); - { V.value = V.VLiteral (PV.VScalar v); ty = T.TLiteral ty } + { value = VLiteral (VScalar v); ty = TLiteral ty } (* Remaining cases (invalid) *) | _, _ -> raise (Failure "Improperly typed constant value") @@ -126,8 +120,8 @@ let literal_to_typed_value (ty : PV.literal_type) (cv : V.literal) : 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 : C.config) - (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value = +let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx) + (v : typed_value) : eval_ctx * typed_value = log#ldebug (lazy ("copy_value: " @@ -170,7 +164,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) | VSharedBorrow bid -> (* We need to create a new borrow id for the copied borrow, and * update the context accordingly *) - let bid' = C.fresh_borrow_id () in + let bid' = fresh_borrow_id () in let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in (ctx, { v with value = VBorrow (VSharedBorrow bid') }) | VMutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow") @@ -188,7 +182,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) * 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 (Subst.erase_regions sp.sv_ty)); + assert (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty)); (* 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 @@ -233,8 +227,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) what we do in the formalization (because we don't enforce the same constraints as MIR in the formalization). *) -let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) : - cm_fun = +let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun = fun cf ctx -> let prepare : cm_fun = fun cf ctx -> @@ -258,8 +251,8 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) : prepare cf ctx (** Evaluate an operand, without reorganizing the context before *) -let eval_operand_no_reorganize (config : C.config) (op : E.operand) - (cf : V.typed_value -> m_fun) : m_fun = +let eval_operand_no_reorganize (config : config) (op : operand) + (cf : typed_value -> m_fun) : m_fun = fun ctx -> (* Debug *) log#ldebug @@ -271,11 +264,11 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) | Constant cv -> ( match cv.value with | CLiteral lit -> - cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx + cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx | CTraitConst (trait_ref, generics, const_name) -> ( - assert (generics = TypesUtils.mk_empty_generic_args); + assert (generics = empty_generic_args); match trait_ref.trait_id with - | T.TraitImpl _ -> + | TraitImpl _ -> (* This shouldn't happen: if we refer to a concrete implementation, we should directly refer to the top-level constant *) raise (Failure "Unreachable") @@ -285,14 +278,13 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) let ctx0 = ctx in (* Lookup the trait declaration to retrieve the type of the symbolic value *) let trait_decl = - C.ctx_lookup_trait_decl ctx - trait_ref.trait_decl_ref.trait_decl_id + ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id in let _, (ty, _) = List.find (fun (name, _) -> name = const_name) trait_decl.consts in (* Introduce a fresh symbolic value *) - let v = mk_fresh_symbolic_typed_value V.TraitConst ty in + let v = mk_fresh_symbolic_typed_value TraitConst ty in (* Continue the evaluation *) let e = cf v ctx in (* We have to wrap the generated expression *) @@ -310,7 +302,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) | CVar vid -> ( let ctx0 = ctx in (* Lookup the const generic value *) - let cv = C.ctx_lookup_const_generic_value ctx vid in + let cv = ctx_lookup_const_generic_value ctx vid in (* Copy the value *) let allow_adt_copy = false in let ctx, v = copy_value allow_adt_copy config ctx cv in @@ -322,7 +314,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) | 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.V.value); + assert (is_symbolic cv.value); (* *) Some (SymbolicAst.IntroSymbolic @@ -362,15 +354,15 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) 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)); - let bottom : V.typed_value = { V.value = VBottom; ty = v.ty } in + let bottom : typed_value = { value = VBottom; ty = v.ty } in let ctx = write_place access p bottom ctx in cf v ctx in (* Compose and apply *) comp cc move cf ctx -let eval_operand (config : C.config) (op : E.operand) - (cf : V.typed_value -> m_fun) : m_fun = +let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) : + m_fun = fun ctx -> (* Debug *) log#ldebug @@ -387,13 +379,13 @@ let eval_operand (config : C.config) (op : E.operand) See [prepare_eval_operand_reorganize]. *) -let prepare_eval_operands_reorganize (config : C.config) (ops : E.operand list) - : cm_fun = +let prepare_eval_operands_reorganize (config : config) (ops : operand list) : + cm_fun = fold_left_apply_continuation (prepare_eval_operand_reorganize config) ops (** Evaluate several operands. *) -let eval_operands (config : C.config) (ops : E.operand list) - (cf : V.typed_value list -> m_fun) : m_fun = +let eval_operands (config : config) (ops : operand list) + (cf : typed_value list -> m_fun) : m_fun = fun ctx -> (* Prepare the operands *) let prepare = prepare_eval_operands_reorganize config ops in @@ -404,8 +396,8 @@ let eval_operands (config : C.config) (ops : E.operand list) (* Compose and apply *) comp prepare eval cf ctx -let eval_two_operands (config : C.config) (op1 : E.operand) (op2 : E.operand) - (cf : V.typed_value * V.typed_value -> m_fun) : m_fun = +let eval_two_operands (config : config) (op1 : operand) (op2 : operand) + (cf : typed_value * typed_value -> m_fun) : m_fun = let eval_op = eval_operands config [ op1; op2 ] in let use_res cf res = match res with @@ -414,73 +406,73 @@ let eval_two_operands (config : C.config) (op1 : E.operand) (op2 : E.operand) in comp eval_op use_res cf -let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand) - (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = +let eval_unary_op_concrete (config : config) (unop : unop) (op : operand) + (cf : (typed_value, eval_error) result -> m_fun) : m_fun = (* Evaluate the operand *) let eval_op = eval_operand config op in (* Apply the unop *) - let apply cf (v : V.typed_value) : m_fun = - match (unop, v.V.value) with - | E.Not, V.VLiteral (VBool b) -> - cf (Ok { v with V.value = V.VLiteral (VBool (not b)) }) - | E.Neg, V.VLiteral (PV.VScalar sv) -> ( - let i = Z.neg sv.PV.value in + let apply cf (v : typed_value) : m_fun = + match (unop, v.value) with + | Not, VLiteral (VBool b) -> + cf (Ok { v with value = VLiteral (VBool (not b)) }) + | Neg, VLiteral (VScalar sv) -> ( + let i = Z.neg sv.value in match mk_scalar sv.int_ty i with | Error _ -> cf (Error EPanic) - | Ok sv -> cf (Ok { v with V.value = V.VLiteral (PV.VScalar sv) })) - | E.Cast (E.CastInteger (src_ty, tgt_ty)), V.VLiteral (PV.VScalar sv) -> ( + | Ok sv -> cf (Ok { v with value = VLiteral (VScalar sv) })) + | Cast (CastInteger (src_ty, tgt_ty)), VLiteral (VScalar sv) -> ( assert (src_ty = sv.int_ty); - let i = sv.PV.value in + let i = sv.value in match mk_scalar tgt_ty i with | Error _ -> cf (Error EPanic) | Ok sv -> - let ty = T.TLiteral (TInteger tgt_ty) in - let value = V.VLiteral (PV.VScalar sv) in - cf (Ok { V.ty; value })) + let ty = TLiteral (TInteger tgt_ty) in + let value = VLiteral (VScalar sv) in + cf (Ok { ty; value })) | _ -> raise (Failure "Invalid input for unop") in comp eval_op apply cf -let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand) - (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = +let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand) + (cf : (typed_value, eval_error) result -> m_fun) : m_fun = fun ctx -> (* Evaluate the operand *) let eval_op = eval_operand config op in (* Generate a fresh symbolic value to store the result *) - let apply cf (v : V.typed_value) : m_fun = + let apply cf (v : typed_value) : m_fun = fun ctx -> - let res_sv_id = C.fresh_symbolic_value_id () in + let res_sv_id = fresh_symbolic_value_id () in let res_sv_ty = - match (unop, v.V.ty) with - | E.Not, (T.TLiteral TBool as lty) -> lty - | E.Neg, (T.TLiteral (TInteger _) as lty) -> lty - | E.Cast (E.CastInteger (_, tgt_ty)), _ -> T.TLiteral (TInteger tgt_ty) + match (unop, v.ty) with + | Not, (TLiteral TBool as lty) -> lty + | Neg, (TLiteral (TInteger _) as lty) -> lty + | Cast (CastInteger (_, tgt_ty)), _ -> TLiteral (TInteger tgt_ty) | _ -> raise (Failure "Invalid input for unop") in let res_sv = - { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty } + { sv_kind = FunCallRet; sv_id = res_sv_id; sv_ty = res_sv_ty } in (* Call the continuation *) let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in (* Synthesize the symbolic AST *) - S.synthesize_unary_op ctx unop v - (S.mk_opt_place_from_op op ctx) + synthesize_unary_op ctx unop v + (mk_opt_place_from_op op ctx) res_sv None expr in (* Compose and apply *) comp eval_op apply cf ctx -let eval_unary_op (config : C.config) (unop : E.unop) (op : E.operand) - (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = +let eval_unary_op (config : config) (unop : unop) (op : operand) + (cf : (typed_value, eval_error) result -> m_fun) : m_fun = match config.mode with - | C.ConcreteMode -> eval_unary_op_concrete config unop op cf - | C.SymbolicMode -> eval_unary_op_symbolic config unop op cf + | ConcreteMode -> eval_unary_op_concrete config unop op cf + | SymbolicMode -> eval_unary_op_symbolic config unop op cf (** 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 : E.binop) (v1 : V.typed_value) - (v2 : V.typed_value) : (V.typed_value, eval_error) result = +let eval_binary_op_concrete_compute (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 ( @@ -489,53 +481,52 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value) (* Equality/inequality check is primitive only for a subset of types *) assert (ty_is_primitively_copyable v1.ty); let b = v1 = v2 in - Ok { V.value = V.VLiteral (VBool b); ty = T.TLiteral TBool }) + Ok { value = VLiteral (VBool b); ty = TLiteral TBool }) else (* For the non-equality operations, the input values are necessarily scalars *) - match (v1.V.value, v2.V.value) with - | V.VLiteral (PV.VScalar sv1), V.VLiteral (PV.VScalar sv2) -> ( + match (v1.value, v2.value) with + | VLiteral (VScalar sv1), VLiteral (VScalar sv2) -> ( (* There are binops which require the two operands to have the same type, and binops for which it is not the case. There are also binops which return booleans, and binops which return integers. *) match binop with - | E.Lt | E.Le | E.Ge | E.Gt -> + | 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); let b = match binop with - | E.Lt -> Z.lt sv1.PV.value sv2.PV.value - | E.Le -> Z.leq sv1.PV.value sv2.PV.value - | E.Ge -> Z.geq sv1.PV.value sv2.PV.value - | E.Gt -> Z.gt sv1.PV.value sv2.PV.value - | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd - | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq -> + | Lt -> Z.lt sv1.value sv2.value + | Le -> Z.leq sv1.value sv2.value + | Ge -> Z.geq sv1.value sv2.value + | Gt -> Z.gt sv1.value sv2.value + | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl + | Shr | Ne | Eq -> raise (Failure "Unreachable") in Ok - ({ V.value = V.VLiteral (VBool b); ty = T.TLiteral TBool } - : V.typed_value) - | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr - -> ( + ({ 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); let res = match binop with - | E.Div -> - if sv2.PV.value = Z.zero then Error () - else mk_scalar sv1.int_ty (Z.div sv1.PV.value sv2.PV.value) - | E.Rem -> + | Div -> + if sv2.value = Z.zero then Error () + else mk_scalar sv1.int_ty (Z.div sv1.value sv2.value) + | Rem -> (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *) - if sv2.PV.value = Z.zero then Error () - else mk_scalar sv1.int_ty (Z.rem sv1.PV.value sv2.PV.value) - | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.PV.value sv2.PV.value) - | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.PV.value sv2.PV.value) - | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.PV.value sv2.PV.value) - | E.BitXor -> raise Unimplemented - | E.BitAnd -> raise Unimplemented - | E.BitOr -> raise Unimplemented - | E.Lt | E.Le | E.Ge | E.Gt | E.Shl | E.Shr | E.Ne | E.Eq -> + if sv2.value = Z.zero then Error () + else mk_scalar sv1.int_ty (Z.rem sv1.value sv2.value) + | Add -> mk_scalar sv1.int_ty (Z.add sv1.value sv2.value) + | Sub -> mk_scalar sv1.int_ty (Z.sub sv1.value sv2.value) + | Mul -> mk_scalar sv1.int_ty (Z.mul sv1.value sv2.value) + | BitXor -> raise Unimplemented + | BitAnd -> raise Unimplemented + | BitOr -> raise Unimplemented + | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq -> raise (Failure "Unreachable") in match res with @@ -543,97 +534,93 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value) | Ok sv -> Ok { - V.value = V.VLiteral (PV.VScalar sv); - ty = T.TLiteral (TInteger sv1.int_ty); + value = VLiteral (VScalar sv); + ty = TLiteral (TInteger sv1.int_ty); }) - | E.Shl | E.Shr -> raise Unimplemented - | E.Ne | E.Eq -> raise (Failure "Unreachable")) + | Shl | Shr -> raise Unimplemented + | Ne | Eq -> raise (Failure "Unreachable")) | _ -> raise (Failure "Invalid inputs for binop") -let eval_binary_op_concrete (config : C.config) (binop : E.binop) - (op1 : E.operand) (op2 : E.operand) - (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = +let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand) + (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun = (* Evaluate the operands *) let eval_ops = eval_two_operands config op1 op2 in (* Compute the result of the binop *) - let compute cf (res : V.typed_value * V.typed_value) = + let compute cf (res : typed_value * typed_value) = let v1, v2 = res in cf (eval_binary_op_concrete_compute binop v1 v2) in (* Compose and apply *) comp eval_ops compute cf -let eval_binary_op_symbolic (config : C.config) (binop : E.binop) - (op1 : E.operand) (op2 : E.operand) - (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = +let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand) + (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun = fun ctx -> (* Evaluate the operands *) let eval_ops = eval_two_operands config op1 op2 in (* Compute the result of applying the binop *) - let compute cf ((v1, v2) : V.typed_value * V.typed_value) : m_fun = + let compute cf ((v1, v2) : typed_value * typed_value) : m_fun = fun ctx -> (* Generate a fresh symbolic value to store the result *) - let res_sv_id = C.fresh_symbolic_value_id () in + let res_sv_id = fresh_symbolic_value_id () in let res_sv_ty = if binop = Eq || binop = Ne then ( (* Equality operations *) assert (v1.ty = v2.ty); (* Equality/inequality check is primitive only for a subset of types *) assert (ty_is_primitively_copyable v1.ty); - T.TLiteral TBool) + TLiteral TBool) else (* Other operations: input types are integers *) - match (v1.V.ty, v2.V.ty) with - | T.TLiteral (TInteger int_ty1), T.TLiteral (TInteger int_ty2) -> ( + match (v1.ty, v2.ty) with + | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> ( match binop with - | E.Lt | E.Le | E.Ge | E.Gt -> + | Lt | Le | Ge | Gt -> assert (int_ty1 = int_ty2); - T.TLiteral TBool - | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd - | E.BitOr -> + TLiteral TBool + | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> assert (int_ty1 = int_ty2); - T.TLiteral (TInteger int_ty1) - | E.Shl | E.Shr -> raise Unimplemented - | E.Ne | E.Eq -> raise (Failure "Unreachable")) + TLiteral (TInteger int_ty1) + | Shl | Shr -> raise Unimplemented + | Ne | Eq -> raise (Failure "Unreachable")) | _ -> raise (Failure "Invalid inputs for binop") in let res_sv = - { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty } + { sv_kind = FunCallRet; sv_id = res_sv_id; sv_ty = res_sv_ty } in (* Call the continuattion *) let v = mk_typed_value_from_symbolic_value res_sv in let expr = cf (Ok v) ctx in (* Synthesize the symbolic AST *) - let p1 = S.mk_opt_place_from_op op1 ctx in - let p2 = S.mk_opt_place_from_op op2 ctx in - S.synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr + let p1 = mk_opt_place_from_op op1 ctx in + let p2 = mk_opt_place_from_op op2 ctx in + synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr in (* Compose and apply *) comp eval_ops compute cf ctx -let eval_binary_op (config : C.config) (binop : E.binop) (op1 : E.operand) - (op2 : E.operand) (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun - = +let eval_binary_op (config : config) (binop : binop) (op1 : operand) + (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun = match config.mode with - | C.ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf - | C.SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf + | ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf + | SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf -let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) - (cf : V.typed_value -> m_fun) : m_fun = +let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind) + (cf : typed_value -> m_fun) : m_fun = fun ctx -> match bkind with - | Shared | TwoPhaseMut | Shallow -> + | BShared | BTwoPhaseMut | BShallow -> (* **REMARK**: we initially treated shallow borrows like shared borrows. In practice this restricted the behaviour too much, so for now we forbid them. *) - assert (bkind <> Shallow); + assert (bkind <> BShallow); (* Access the value *) let access = match bkind with - | Shared | Shallow -> Read - | TwoPhaseMut -> Write + | BShared | BShallow -> Read + | BTwoPhaseMut -> Write | _ -> raise (Failure "Unreachable") in @@ -642,22 +629,20 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) access_rplace_reorganize_and_read config expand_prim_copy access p in (* Evaluate the borrowing operation *) - let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = + let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun = fun ctx -> (* Generate the fresh borrow id *) - let bid = C.fresh_borrow_id () in + let bid = fresh_borrow_id () in (* Compute the loan value, with which to replace the value at place p *) let nv = match v.value with | VLoan (VSharedLoan (bids, sv)) -> (* Shared loan: insert the new borrow id *) - let bids1 = V.BorrowId.Set.add bid bids in + let bids1 = BorrowId.Set.add bid bids in { v with value = VLoan (VSharedLoan (bids1, sv)) } | _ -> (* Not a shared loan: add a wrapper *) - let v' = - V.VLoan (VSharedLoan (V.BorrowId.Set.singleton bid, v)) - in + let v' = VLoan (VSharedLoan (BorrowId.Set.singleton bid, v)) in { v with value = v' } in (* Update the borrowed value in the context *) @@ -666,27 +651,27 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) * Note that the reference is *mutable* if we do a two-phase borrow *) let ref_kind = match bkind with - | Shared | Shallow -> T.Shared - | TwoPhaseMut -> T.Mut + | BShared | BShallow -> RShared + | BTwoPhaseMut -> RMut | _ -> raise (Failure "Unreachable") in - let rv_ty = T.TRef (T.RErased, v.ty, ref_kind) in + let rv_ty = TRef (RErased, v.ty, ref_kind) in let bc = match bkind with - | Shared | Shallow -> + | BShared | BShallow -> (* See the remark at the beginning of the match branch: we handle shallow borrows like shared borrows *) - V.VSharedBorrow bid - | TwoPhaseMut -> VReservedMutBorrow bid + VSharedBorrow bid + | BTwoPhaseMut -> VReservedMutBorrow bid | _ -> raise (Failure "Unreachable") in - let rv : V.typed_value = { value = VBorrow bc; ty = rv_ty } in + let rv : typed_value = { value = VBorrow bc; ty = rv_ty } in (* Continue *) cf rv ctx in (* Compose and apply *) comp prepare eval cf ctx - | Mut -> + | BMut -> (* Access the value *) let access = Write in let expand_prim_copy = false in @@ -694,13 +679,13 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) access_rplace_reorganize_and_read config expand_prim_copy access p in (* Evaluate the borrowing operation *) - let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = + let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun = fun ctx -> (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) - let bid = C.fresh_borrow_id () in - let rv_ty = T.TRef (RErased, v.ty, Mut) in - let rv : V.typed_value = - { V.value = VBorrow (VMutBorrow (bid, v)); ty = rv_ty } + let bid = fresh_borrow_id () in + let rv_ty = TRef (RErased, v.ty, RMut) in + let rv : typed_value = + { value = VBorrow (VMutBorrow (bid, v)); ty = rv_ty } in (* Compute the value with which to replace the value at place p *) let nv = { v with value = VLoan (VMutLoan bid) } in @@ -712,63 +697,61 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (* Compose and apply *) comp prepare eval cf ctx -let eval_rvalue_aggregate (config : C.config) - (aggregate_kind : E.aggregate_kind) (ops : E.operand list) - (cf : V.typed_value -> m_fun) : m_fun = +let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind) + (ops : operand list) (cf : typed_value -> m_fun) : m_fun = (* Evaluate the operands *) let eval_ops = eval_operands config ops in (* Compute the value *) - let compute (cf : V.typed_value -> m_fun) (values : V.typed_value list) : - m_fun = + let compute (cf : typed_value -> m_fun) (values : typed_value list) : m_fun = fun ctx -> (* Match on the aggregate kind *) match aggregate_kind with | AggregatedAdt (type_id, opt_variant_id, generics) -> ( match type_id with | TTuple -> - let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in - let v = V.VAdt { variant_id = None; field_values = values } in - let generics = TypesUtils.mk_generic_args [] tys [] [] in - let ty = T.TAdt (T.TTuple, generics) in - let aggregated : V.typed_value = { V.value = v; ty } in + let tys = List.map (fun (v : typed_value) -> v.ty) values in + let v = VAdt { variant_id = None; field_values = values } in + let generics = mk_generic_args [] tys [] [] in + let ty = TAdt (TTuple, generics) in + let aggregated : typed_value = { value = v; ty } in (* Call the continuation *) cf aggregated ctx | TAdtId def_id -> (* Sanity checks *) - let type_decl = C.ctx_lookup_type_decl ctx def_id in + let type_decl = ctx_lookup_type_decl ctx def_id in assert ( List.length type_decl.generics.regions = List.length generics.regions); let expected_field_types = - Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id - generics + AssociatedTypes.ctx_adt_get_inst_norm_field_etypes ctx def_id + opt_variant_id generics in assert ( expected_field_types - = List.map (fun (v : V.typed_value) -> v.V.ty) values); + = List.map (fun (v : typed_value) -> v.ty) values); (* Construct the value *) - let av : V.adt_value = - { V.variant_id = opt_variant_id; V.field_values = values } + let av : adt_value = + { variant_id = opt_variant_id; field_values = values } in - let aty = T.TAdt (T.TAdtId def_id, generics) in - let aggregated : V.typed_value = { V.value = VAdt av; ty = aty } in + let aty = TAdt (TAdtId def_id, generics) in + let aggregated : typed_value = { value = VAdt av; ty = aty } in (* Call the continuation *) cf aggregated ctx | TAssumed _ -> raise (Failure "Unreachable")) | AggregatedArray (ety, cg) -> ( (* Sanity check: all the values have the proper type *) - assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values); + assert (List.for_all (fun (v : typed_value) -> v.ty = ety) values); (* 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)); let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in - let ty = T.TAdt (T.TAssumed T.TArray, generics) in + let ty = TAdt (TAssumed TArray, generics) in (* In order to generate a better AST, we introduce a symbolic value equal to the array. The reason is that otherwise, the 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 V.Aggregate ty in + let saggregated = mk_fresh_symbolic_typed_value Aggregate ty in (* Call the continuation *) match cf saggregated ctx with | None -> None @@ -780,32 +763,32 @@ let eval_rvalue_aggregate (config : C.config) (* Compose and apply *) comp eval_ops compute cf -let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue) - (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = +let eval_rvalue_not_global (config : config) (rvalue : rvalue) + (cf : (typed_value, eval_error) result -> m_fun) : m_fun = fun ctx -> log#ldebug (lazy "eval_rvalue"); (* Small helpers *) - let wrap_in_result (cf : (V.typed_value, eval_error) result -> m_fun) - (v : V.typed_value) : m_fun = + let wrap_in_result (cf : (typed_value, eval_error) result -> m_fun) + (v : typed_value) : m_fun = cf (Ok v) in let comp_wrap f = comp f wrap_in_result cf in (* Delegate to the proper auxiliary function *) match rvalue with - | E.Use op -> comp_wrap (eval_operand config op) ctx - | E.RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx - | E.UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx - | E.BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx - | E.Aggregate (aggregate_kind, ops) -> + | Use op -> comp_wrap (eval_operand config op) ctx + | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx + | UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx + | BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx + | Aggregate (aggregate_kind, ops) -> comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx - | E.Discriminant _ -> + | Discriminant _ -> raise (Failure "Unreachable: discriminant reads should have been eliminated from \ the AST") - | E.Global _ -> raise (Failure "Unreachable") + | Global _ -> raise (Failure "Unreachable") -let eval_fake_read (config : C.config) (p : E.place) : cm_fun = +let eval_fake_read (config : config) (p : place) : cm_fun = fun cf ctx -> let expand_prim_copy = false in let cf_prepare cf = -- cgit v1.2.3 From 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Nov 2023 21:58:25 +0100 Subject: Use the name matcher implemented in Charon --- compiler/InterpreterExpressions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/InterpreterExpressions.ml') diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 1e28fd4b..38620be0 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -321,7 +321,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) ( ctx0, None, value_as_symbolic v.value, - SymbolicAst.VaCGValue vid, + SymbolicAst.VaCgValue vid, e ))) | CFnPtr _ -> raise (Failure "TODO")) | Copy p -> -- cgit v1.2.3 From f852e1a1334b7506c0baf366b9e75cd01b9c843e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 12:15:37 +0100 Subject: Rename PrimitiveValues to Values --- compiler/InterpreterExpressions.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'compiler/InterpreterExpressions.ml') diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 38620be0..cc0580be 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -1,4 +1,3 @@ -open PrimitiveValues open Types open Values open LlbcAst @@ -96,7 +95,7 @@ let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value = log#ldebug (lazy ("literal_to_typed_value:" ^ "\n- cv: " - ^ Print.PrimitiveValues.literal_to_string cv)); + ^ Print.Values.literal_to_string cv)); match (ty, cv) with (* Scalar, boolean... *) | TBool, VBool v -> { value = VLiteral (VBool v); ty = TLiteral ty } -- cgit v1.2.3