From dd0703ff179dec9534f58a2261a41eba6e2bcce3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Mon, 2 Dec 2024 17:01:27 +0100 Subject: [PATCH] Fix ownership object issues (#5933) Fixes #5932 ### Description Previously, there was some conversion code that, in the case of an upcast conversion, was removing a borrow annotation to ensure the object stayed owned. This was done in the context of newtypes that had copy semantics. However, that same piece of code is invoked in cases of variables with non-copy semantics. This PR fixes that by doing a proper check. ### How has this been tested? The test traits.dfy has been extended, was not passing, and now passes. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../Backends/Rust/Dafny-compiler-rust.dfy | 71 ++++++------ Source/DafnyCore/DafnyGeneratedFromDafny.sh | 1 - .../DafnyCore/DafnyGeneratedFromDafnyPost.py | 4 + Source/DafnyCore/GeneratedFromDafny/DCOMP.cs | 102 +++++++++--------- .../LitTests/LitTest/comp/rust/traits.dfy | 13 +++ .../LitTest/comp/rust/traits.dfy.expect | 2 +- 6 files changed, 113 insertions(+), 80 deletions(-) diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index d39dcf2d654..29621b7ba2a 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy @@ -2207,48 +2207,48 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } } - method ToPrimitive(r: R.Expr, typ: Type, primitiveType: Type) returns (out: R.Expr) + method ToPrimitive(r: R.Expr, typ: Type, primitiveType: Type, env: Environment) returns (out: R.Expr) modifies this { out := r; if typ != primitiveType { var dummy; - out, dummy := GenExprConvertTo(r, OwnershipOwned, typ, primitiveType, OwnershipOwned); + out, dummy := GenExprConvertTo(r, OwnershipOwned, typ, primitiveType, env, OwnershipOwned); } } - method ToBool(r: R.Expr, typ: Type) returns (out: R.Expr) + method ToBool(r: R.Expr, typ: Type, env: Environment) returns (out: R.Expr) modifies this { - out := ToPrimitive(r, typ, Primitive(Primitive.Bool)); + out := ToPrimitive(r, typ, Primitive(Primitive.Bool), env); } - method ToInt(r: R.Expr, typ: Type) returns (out: R.Expr) + method ToInt(r: R.Expr, typ: Type, env: Environment) returns (out: R.Expr) modifies this { - out := ToPrimitive(r, typ, Primitive(Primitive.Int)); + out := ToPrimitive(r, typ, Primitive(Primitive.Int), env); } - method FromPrimitive(r: R.Expr, primitiveType: Type, typ: Type) returns (out: R.Expr) + method FromPrimitive(r: R.Expr, primitiveType: Type, typ: Type, env: Environment) returns (out: R.Expr) modifies this { out := r; if typ != primitiveType { var dummy; - out, dummy := GenExprConvertTo(r, OwnershipOwned, primitiveType, typ, OwnershipOwned); + out, dummy := GenExprConvertTo(r, OwnershipOwned, primitiveType, typ, env, OwnershipOwned); } } - method FromBool(r: R.Expr, typ: Type) returns (out: R.Expr) + method FromBool(r: R.Expr, typ: Type, env: Environment) returns (out: R.Expr) modifies this { - out := FromPrimitive(r, Primitive(Primitive.Bool), typ); + out := FromPrimitive(r, Primitive(Primitive.Bool), typ, env); } - method FromInt(r: R.Expr, typ: Type) returns (out: R.Expr) + method FromInt(r: R.Expr, typ: Type, env: Environment) returns (out: R.Expr) modifies this { - out := FromPrimitive(r, Primitive(Primitive.Int), typ); + out := FromPrimitive(r, Primitive(Primitive.Int), typ, env); } method GenExprBinary( @@ -2332,8 +2332,8 @@ module {:extern "DCOMP"} DafnyToRustCompiler { case _ => { if op in OpTable { if IsBooleanOperator(op) { - left := ToBool(left, lType); - right := ToBool(right, rType); + left := ToBool(left, lType, env); + right := ToBool(right, rType, env); } r := R.Expr.BinaryOp( OpTable[op], @@ -2341,12 +2341,12 @@ module {:extern "DCOMP"} DafnyToRustCompiler { right, format); if IsBooleanOperator(op) { - r := FromBool(r, resType); + r := FromBool(r, resType, env); } } else { if IsComplexArithmetic(op) { - left := ToInt(left, lType); - right := ToInt(right, rType); + left := ToInt(left, lType, env); + right := ToInt(right, rType, env); } match op { case Eq(referential) => { @@ -2365,7 +2365,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } else { r := R.BinaryOp("==", left, right, DAST.Format.BinaryOpFormat.NoFormat()); if resType != Primitive(Primitive.Bool) { - r, resultingOwnership := GenExprConvertTo(r, OwnershipOwned, Primitive(Primitive.Bool), resType, OwnershipOwned); + r, resultingOwnership := GenExprConvertTo(r, OwnershipOwned, Primitive(Primitive.Bool), resType, env, OwnershipOwned); } } } @@ -2389,7 +2389,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } } if IsComplexArithmetic(op) { - r := FromInt(r, resType); + r := FromInt(r, resType, env); } } } @@ -2445,6 +2445,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { exprOwnership: Ownership, fromTpe: Type, toTpe: Type, + env: Environment, expectedOwnership: Ownership ) returns (r: R.Expr, resultingOwnership: Ownership) requires exprOwnership != OwnershipAutoBorrowed @@ -2458,24 +2459,24 @@ module {:extern "DCOMP"} DafnyToRustCompiler { return; } if fromTpe.UserDefined? && fromTpe.resolved.kind.SynonymType? { - r, resultingOwnership := GenExprConvertTo(expr, exprOwnership, fromTpe.resolved.kind.baseType, toTpe, expectedOwnership); + r, resultingOwnership := GenExprConvertTo(expr, exprOwnership, fromTpe.resolved.kind.baseType, toTpe, env, expectedOwnership); return; } if toTpe.UserDefined? && toTpe.resolved.kind.SynonymType? { - r, resultingOwnership := GenExprConvertTo(expr, exprOwnership, fromTpe, toTpe.resolved.kind.baseType, expectedOwnership); + r, resultingOwnership := GenExprConvertTo(expr, exprOwnership, fromTpe, toTpe.resolved.kind.baseType, env, expectedOwnership); return; } if NeedsUnwrappingConversion(fromTpe) { // From type is a newtype but it's not a primitive one. r := UnwrapNewtype(r, exprOwnership, fromTpe); r, resultingOwnership := - GenExprConvertTo(r, exprOwnership, fromTpe.resolved.kind.baseType, toTpe, expectedOwnership); + GenExprConvertTo(r, exprOwnership, fromTpe.resolved.kind.baseType, toTpe, env, expectedOwnership); return; } if NeedsUnwrappingConversion(toTpe) { var toKind := toTpe.resolved.kind; r, resultingOwnership := - GenExprConvertTo(r, exprOwnership, fromTpe, toKind.baseType, expectedOwnership); + GenExprConvertTo(r, exprOwnership, fromTpe, toKind.baseType, env, expectedOwnership); r := WrapWithNewtype(r, resultingOwnership, toTpe); r, resultingOwnership := FromOwnership(r, resultingOwnership, expectedOwnership); return; @@ -2580,7 +2581,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { r, resultingOwnership := FromOwned(r, expectedOwnership); } case _ => { - r, resultingOwnership := GenExprConvertOther(expr, exprOwnership, fromTpe, toTpe, expectedOwnership); + r, resultingOwnership := GenExprConvertOther(expr, exprOwnership, fromTpe, toTpe, env, expectedOwnership); } } } @@ -2707,11 +2708,24 @@ module {:extern "DCOMP"} DafnyToRustCompiler { false } + // Assumes expr to be borrowed. Will return and expression that is owned instead + function BorrowedToOwned(expr: R.Expr, env: Environment): (out: R.Expr) { + match expr + case UnaryOp("&", underlying, _) => + // We need to clone underlying unless it has borrow semantics. + if underlying.Identifier? && env.CanReadWithoutClone(underlying.name) then + underlying + else + underlying.Clone() // Auto-borrow allows for implicit code + case _ => expr.Clone() + } + method GenExprConvertOther( expr: R.Expr, exprOwnership: Ownership, fromTpe: Type, toTpe: Type, + env: Environment, expectedOwnership: Ownership ) returns (r: R.Expr, resultingOwnership: Ownership) modifies this @@ -2724,11 +2738,8 @@ module {:extern "DCOMP"} DafnyToRustCompiler { if upcastConverter.Success? { var conversionLambda := upcastConverter.value; if exprOwnership == OwnershipBorrowed { - match r { - case UnaryOp("&", underlying, _) => - r := underlying; - case _ => r := r.Clone(); - } + // we need the value to be owned for conversion + r := BorrowedToOwned(r, env); } r := conversionLambda.Apply1(r); r, resultingOwnership := FromOwnership(r, OwnershipOwned, expectedOwnership); @@ -2765,7 +2776,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { var recursiveGen, recOwned, recIdents := GenExpr(expr, selfIdent, env, argumentOwnership); r := recursiveGen; readIdents := recIdents; - r, resultingOwnership := GenExprConvertTo(r, recOwned, fromTpe, toTpe, expectedOwnership); + r, resultingOwnership := GenExprConvertTo(r, recOwned, fromTpe, toTpe, env, expectedOwnership); assert OwnershipGuarantee(expectedOwnership, resultingOwnership); return; } diff --git a/Source/DafnyCore/DafnyGeneratedFromDafny.sh b/Source/DafnyCore/DafnyGeneratedFromDafny.sh index ddc4ccab8fa..2ae61370ed8 100755 --- a/Source/DafnyCore/DafnyGeneratedFromDafny.sh +++ b/Source/DafnyCore/DafnyGeneratedFromDafny.sh @@ -33,5 +33,4 @@ if [ $? -ne 0 ]; then exit 1 fi -rm $output-cs.dtr python3 DafnyGeneratedFromDafnyPost.py $output \ No newline at end of file diff --git a/Source/DafnyCore/DafnyGeneratedFromDafnyPost.py b/Source/DafnyCore/DafnyGeneratedFromDafnyPost.py index 8ed810683f8..9486726fc45 100644 --- a/Source/DafnyCore/DafnyGeneratedFromDafnyPost.py +++ b/Source/DafnyCore/DafnyGeneratedFromDafnyPost.py @@ -20,6 +20,10 @@ print(f"File {output}.cs was not generated. Fix issues and re-run ./DafnyGeneratedFromDafny.sh") exit() +if os.path.exists(output + '-cs.dtr'): + os.remove(output + '-cs.dtr') + print("File deleted: " + output + '-cs.dtr') + with open(output + '.cs', 'r' ) as f: content = f.read() content_trimmed = re.sub('\[assembly[\s\S]*?(?=namespace Formatting)|namespace\s+\w+\s*\{\s*\}\s*//.*', '', content, flags = re.M) diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index 8bb7cb0d186..324fad1d0f7 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -3093,7 +3093,7 @@ public void GenExprLiteral(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs. } after_match0: ; } - public RAST._IExpr ToPrimitive(RAST._IExpr r, DAST._IType typ, DAST._IType primitiveType) + public RAST._IExpr ToPrimitive(RAST._IExpr r, DAST._IType typ, DAST._IType primitiveType, Defs._IEnvironment env) { RAST._IExpr @out = RAST.Expr.Default(); @out = r; @@ -3101,29 +3101,29 @@ public RAST._IExpr ToPrimitive(RAST._IExpr r, DAST._IType typ, DAST._IType primi Defs._IOwnership _0_dummy = Defs.Ownership.Default(); RAST._IExpr _out0; Defs._IOwnership _out1; - (this).GenExprConvertTo(r, Defs.Ownership.create_OwnershipOwned(), typ, primitiveType, Defs.Ownership.create_OwnershipOwned(), out _out0, out _out1); + (this).GenExprConvertTo(r, Defs.Ownership.create_OwnershipOwned(), typ, primitiveType, env, Defs.Ownership.create_OwnershipOwned(), out _out0, out _out1); @out = _out0; _0_dummy = _out1; } return @out; } - public RAST._IExpr ToBool(RAST._IExpr r, DAST._IType typ) + public RAST._IExpr ToBool(RAST._IExpr r, DAST._IType typ, Defs._IEnvironment env) { RAST._IExpr @out = RAST.Expr.Default(); RAST._IExpr _out0; - _out0 = (this).ToPrimitive(r, typ, DAST.Type.create_Primitive(DAST.Primitive.create_Bool())); + _out0 = (this).ToPrimitive(r, typ, DAST.Type.create_Primitive(DAST.Primitive.create_Bool()), env); @out = _out0; return @out; } - public RAST._IExpr ToInt(RAST._IExpr r, DAST._IType typ) + public RAST._IExpr ToInt(RAST._IExpr r, DAST._IType typ, Defs._IEnvironment env) { RAST._IExpr @out = RAST.Expr.Default(); RAST._IExpr _out0; - _out0 = (this).ToPrimitive(r, typ, DAST.Type.create_Primitive(DAST.Primitive.create_Int())); + _out0 = (this).ToPrimitive(r, typ, DAST.Type.create_Primitive(DAST.Primitive.create_Int()), env); @out = _out0; return @out; } - public RAST._IExpr FromPrimitive(RAST._IExpr r, DAST._IType primitiveType, DAST._IType typ) + public RAST._IExpr FromPrimitive(RAST._IExpr r, DAST._IType primitiveType, DAST._IType typ, Defs._IEnvironment env) { RAST._IExpr @out = RAST.Expr.Default(); @out = r; @@ -3131,25 +3131,25 @@ public RAST._IExpr FromPrimitive(RAST._IExpr r, DAST._IType primitiveType, DAST. Defs._IOwnership _0_dummy = Defs.Ownership.Default(); RAST._IExpr _out0; Defs._IOwnership _out1; - (this).GenExprConvertTo(r, Defs.Ownership.create_OwnershipOwned(), primitiveType, typ, Defs.Ownership.create_OwnershipOwned(), out _out0, out _out1); + (this).GenExprConvertTo(r, Defs.Ownership.create_OwnershipOwned(), primitiveType, typ, env, Defs.Ownership.create_OwnershipOwned(), out _out0, out _out1); @out = _out0; _0_dummy = _out1; } return @out; } - public RAST._IExpr FromBool(RAST._IExpr r, DAST._IType typ) + public RAST._IExpr FromBool(RAST._IExpr r, DAST._IType typ, Defs._IEnvironment env) { RAST._IExpr @out = RAST.Expr.Default(); RAST._IExpr _out0; - _out0 = (this).FromPrimitive(r, DAST.Type.create_Primitive(DAST.Primitive.create_Bool()), typ); + _out0 = (this).FromPrimitive(r, DAST.Type.create_Primitive(DAST.Primitive.create_Bool()), typ, env); @out = _out0; return @out; } - public RAST._IExpr FromInt(RAST._IExpr r, DAST._IType typ) + public RAST._IExpr FromInt(RAST._IExpr r, DAST._IType typ, Defs._IEnvironment env) { RAST._IExpr @out = RAST.Expr.Default(); RAST._IExpr _out0; - _out0 = (this).FromPrimitive(r, DAST.Type.create_Primitive(DAST.Primitive.create_Int()), typ); + _out0 = (this).FromPrimitive(r, DAST.Type.create_Primitive(DAST.Primitive.create_Int()), typ, env); @out = _out0; return @out; } @@ -3353,25 +3353,25 @@ public void GenExprBinary(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._ if ((Defs.__default.OpTable).Contains(_0_op)) { if (Defs.__default.IsBooleanOperator(_0_op)) { RAST._IExpr _out6; - _out6 = (this).ToBool(_11_left, _1_lType); + _out6 = (this).ToBool(_11_left, _1_lType, env); _11_left = _out6; RAST._IExpr _out7; - _out7 = (this).ToBool(_14_right, _2_rType); + _out7 = (this).ToBool(_14_right, _2_rType, env); _14_right = _out7; } r = RAST.Expr.create_BinaryOp(Dafny.Map>.Select(Defs.__default.OpTable,_0_op), _11_left, _14_right, _6_format); if (Defs.__default.IsBooleanOperator(_0_op)) { RAST._IExpr _out8; - _out8 = (this).FromBool(r, _3_resType); + _out8 = (this).FromBool(r, _3_resType, env); r = _out8; } } else { if (Defs.__default.IsComplexArithmetic(_0_op)) { RAST._IExpr _out9; - _out9 = (this).ToInt(_11_left, _1_lType); + _out9 = (this).ToInt(_11_left, _1_lType, env); _11_left = _out9; RAST._IExpr _out10; - _out10 = (this).ToInt(_14_right, _2_rType); + _out10 = (this).ToInt(_14_right, _2_rType, env); _14_right = _out10; } DAST._IBinOp _source1 = _0_op; @@ -3397,7 +3397,7 @@ public void GenExprBinary(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._ if (!object.Equals(_3_resType, DAST.Type.create_Primitive(DAST.Primitive.create_Bool()))) { RAST._IExpr _out12; Defs._IOwnership _out13; - (this).GenExprConvertTo(r, Defs.Ownership.create_OwnershipOwned(), DAST.Type.create_Primitive(DAST.Primitive.create_Bool()), _3_resType, Defs.Ownership.create_OwnershipOwned(), out _out12, out _out13); + (this).GenExprConvertTo(r, Defs.Ownership.create_OwnershipOwned(), DAST.Type.create_Primitive(DAST.Primitive.create_Bool()), _3_resType, env, Defs.Ownership.create_OwnershipOwned(), out _out12, out _out13); r = _out12; resultingOwnership = _out13; } @@ -3468,7 +3468,7 @@ public void GenExprBinary(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._ after_match1: ; if (Defs.__default.IsComplexArithmetic(_0_op)) { RAST._IExpr _out14; - _out14 = (this).FromInt(r, _3_resType); + _out14 = (this).FromInt(r, _3_resType, env); r = _out14; } } @@ -3514,7 +3514,7 @@ public RAST._IExpr WrapWithNewtype(RAST._IExpr expr, Defs._IOwnership exprOwners } return r; } - public void GenExprConvertTo(RAST._IExpr expr, Defs._IOwnership exprOwnership, DAST._IType fromTpe, DAST._IType toTpe, Defs._IOwnership expectedOwnership, out RAST._IExpr r, out Defs._IOwnership resultingOwnership) + public void GenExprConvertTo(RAST._IExpr expr, Defs._IOwnership exprOwnership, DAST._IType fromTpe, DAST._IType toTpe, Defs._IEnvironment env, Defs._IOwnership expectedOwnership, out RAST._IExpr r, out Defs._IOwnership resultingOwnership) { r = RAST.Expr.Default(); resultingOwnership = Defs.Ownership.Default(); @@ -3530,7 +3530,7 @@ public void GenExprConvertTo(RAST._IExpr expr, Defs._IOwnership exprOwnership, D if (((fromTpe).is_UserDefined) && ((((fromTpe).dtor_resolved).dtor_kind).is_SynonymType)) { RAST._IExpr _out2; Defs._IOwnership _out3; - (this).GenExprConvertTo(expr, exprOwnership, (((fromTpe).dtor_resolved).dtor_kind).dtor_baseType, toTpe, expectedOwnership, out _out2, out _out3); + (this).GenExprConvertTo(expr, exprOwnership, (((fromTpe).dtor_resolved).dtor_kind).dtor_baseType, toTpe, env, expectedOwnership, out _out2, out _out3); r = _out2; resultingOwnership = _out3; return ; @@ -3538,7 +3538,7 @@ public void GenExprConvertTo(RAST._IExpr expr, Defs._IOwnership exprOwnership, D if (((toTpe).is_UserDefined) && ((((toTpe).dtor_resolved).dtor_kind).is_SynonymType)) { RAST._IExpr _out4; Defs._IOwnership _out5; - (this).GenExprConvertTo(expr, exprOwnership, fromTpe, (((toTpe).dtor_resolved).dtor_kind).dtor_baseType, expectedOwnership, out _out4, out _out5); + (this).GenExprConvertTo(expr, exprOwnership, fromTpe, (((toTpe).dtor_resolved).dtor_kind).dtor_baseType, env, expectedOwnership, out _out4, out _out5); r = _out4; resultingOwnership = _out5; return ; @@ -3549,7 +3549,7 @@ public void GenExprConvertTo(RAST._IExpr expr, Defs._IOwnership exprOwnership, D r = _out6; RAST._IExpr _out7; Defs._IOwnership _out8; - (this).GenExprConvertTo(r, exprOwnership, (((fromTpe).dtor_resolved).dtor_kind).dtor_baseType, toTpe, expectedOwnership, out _out7, out _out8); + (this).GenExprConvertTo(r, exprOwnership, (((fromTpe).dtor_resolved).dtor_kind).dtor_baseType, toTpe, env, expectedOwnership, out _out7, out _out8); r = _out7; resultingOwnership = _out8; return ; @@ -3559,7 +3559,7 @@ public void GenExprConvertTo(RAST._IExpr expr, Defs._IOwnership exprOwnership, D _0_toKind = ((toTpe).dtor_resolved).dtor_kind; RAST._IExpr _out9; Defs._IOwnership _out10; - (this).GenExprConvertTo(r, exprOwnership, fromTpe, (_0_toKind).dtor_baseType, expectedOwnership, out _out9, out _out10); + (this).GenExprConvertTo(r, exprOwnership, fromTpe, (_0_toKind).dtor_baseType, env, expectedOwnership, out _out9, out _out10); r = _out9; resultingOwnership = _out10; RAST._IExpr _out11; @@ -3817,7 +3817,7 @@ public void GenExprConvertTo(RAST._IExpr expr, Defs._IOwnership exprOwnership, D { RAST._IExpr _out48; Defs._IOwnership _out49; - (this).GenExprConvertOther(expr, exprOwnership, fromTpe, toTpe, expectedOwnership, out _out48, out _out49); + (this).GenExprConvertOther(expr, exprOwnership, fromTpe, toTpe, env, expectedOwnership, out _out48, out _out49); r = _out48; resultingOwnership = _out49; } @@ -3965,7 +3965,27 @@ public bool IsDowncastConversion(RAST._IType fromTpe, RAST._IType toTpe) return false; } } - public void GenExprConvertOther(RAST._IExpr expr, Defs._IOwnership exprOwnership, DAST._IType fromTpe, DAST._IType toTpe, Defs._IOwnership expectedOwnership, out RAST._IExpr r, out Defs._IOwnership resultingOwnership) + public RAST._IExpr BorrowedToOwned(RAST._IExpr expr, Defs._IEnvironment env) + { + RAST._IExpr _source0 = expr; + { + if (_source0.is_UnaryOp) { + Dafny.ISequence op10 = _source0.dtor_op1; + if (object.Equals(op10, Dafny.Sequence.UnicodeFromString("&"))) { + RAST._IExpr _0_underlying = _source0.dtor_underlying; + if (((_0_underlying).is_Identifier) && ((env).CanReadWithoutClone((_0_underlying).dtor_name))) { + return _0_underlying; + } else { + return (_0_underlying).Clone(); + } + } + } + } + { + return (expr).Clone(); + } + } + public void GenExprConvertOther(RAST._IExpr expr, Defs._IOwnership exprOwnership, DAST._IType fromTpe, DAST._IType toTpe, Defs._IEnvironment env, Defs._IOwnership expectedOwnership, out RAST._IExpr r, out Defs._IOwnership resultingOwnership) { r = RAST.Expr.Default(); resultingOwnership = Defs.Ownership.Default(); @@ -3984,21 +4004,7 @@ public void GenExprConvertOther(RAST._IExpr expr, Defs._IOwnership exprOwnership RAST._IExpr _3_conversionLambda; _3_conversionLambda = (_2_upcastConverter).dtor_value; if (object.Equals(exprOwnership, Defs.Ownership.create_OwnershipBorrowed())) { - RAST._IExpr _source0 = r; - { - if (_source0.is_UnaryOp) { - Dafny.ISequence op10 = _source0.dtor_op1; - if (object.Equals(op10, Dafny.Sequence.UnicodeFromString("&"))) { - RAST._IExpr _4_underlying = _source0.dtor_underlying; - r = _4_underlying; - goto after_match0; - } - } - } - { - r = (r).Clone(); - } - after_match0: ; + r = (this).BorrowedToOwned(r, env); } r = (_3_conversionLambda).Apply1(r); RAST._IExpr _out2; @@ -4017,13 +4023,13 @@ public void GenExprConvertOther(RAST._IExpr expr, Defs._IOwnership exprOwnership } else { Std.Wrappers._IResult,RAST._IExpr>>> _let_tmp_rhs0 = _2_upcastConverter; _System._ITuple5,RAST._IExpr>> _let_tmp_rhs1 = _let_tmp_rhs0.dtor_error; - DAST._IType _5_fromType = _let_tmp_rhs1.dtor__0; - RAST._IType _6_fromTpeGen = _let_tmp_rhs1.dtor__1; - DAST._IType _7_toType = _let_tmp_rhs1.dtor__2; - RAST._IType _8_toTpeGen = _let_tmp_rhs1.dtor__3; - Dafny.IMap<_System._ITuple2,RAST._IExpr> _9_m = _let_tmp_rhs1.dtor__4; + DAST._IType _4_fromType = _let_tmp_rhs1.dtor__0; + RAST._IType _5_fromTpeGen = _let_tmp_rhs1.dtor__1; + DAST._IType _6_toType = _let_tmp_rhs1.dtor__2; + RAST._IType _7_toTpeGen = _let_tmp_rhs1.dtor__3; + Dafny.IMap<_System._ITuple2,RAST._IExpr> _8_m = _let_tmp_rhs1.dtor__4; RAST._IExpr _out6; - _out6 = (this).Error(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("Coercion from "), (_6_fromTpeGen)._ToString(Defs.__default.IND)), Dafny.Sequence.UnicodeFromString(" to ")), (_8_toTpeGen)._ToString(Defs.__default.IND)), Dafny.Sequence.UnicodeFromString(" not yet implemented")), r); + _out6 = (this).Error(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("Coercion from "), (_5_fromTpeGen)._ToString(Defs.__default.IND)), Dafny.Sequence.UnicodeFromString(" to ")), (_7_toTpeGen)._ToString(Defs.__default.IND)), Dafny.Sequence.UnicodeFromString(" not yet implemented")), r); r = _out6; RAST._IExpr _out7; Defs._IOwnership _out8; @@ -4060,7 +4066,7 @@ public void GenExprConvert(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs. readIdents = _6_recIdents; RAST._IExpr _out3; Defs._IOwnership _out4; - (this).GenExprConvertTo(r, _5_recOwned, _1_fromTpe, _2_toTpe, expectedOwnership, out _out3, out _out4); + (this).GenExprConvertTo(r, _5_recOwned, _1_fromTpe, _2_toTpe, env, expectedOwnership, out _out3, out _out4); r = _out3; resultingOwnership = _out4; return ; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/traits.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/traits.dfy index 952050e36b2..b9ba137de84 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/traits.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/traits.dfy @@ -127,6 +127,19 @@ module All { r := Some(true); } + datatype ObjectContainer = ObjectContainer(y: Y) + + method ParameterBorrows(y: Y, o: ObjectContainer) { // y is borrowed + var z: SubTrait := y as SubTrait; + var p: SuperTrait := y; + var y2 := o.y; // y2 is owned + ConsumeBorrows(y2 as SubTrait); + ConsumeBorrows(y2 as SubTrait); + } + method ConsumeBorrows(y: SubTrait) { + + } + method Main() { var rts := Test(Some(2)); expect rts == Some(true); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/traits.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/traits.dfy.expect index 2123d1f24c3..506e5ca1d4c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/traits.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/traits.dfy.expect @@ -1,3 +1,3 @@ -Dafny program verifier finished with 20 verified, 0 errors +Dafny program verifier finished with 21 verified, 0 errors Main passed all the tests