Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix 5800 soundness rust aliasing #5801

Merged
merged 7 commits into from
Oct 1, 2024
Merged

Fix 5800 soundness rust aliasing #5801

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
e617e23
Fix: Soundness issue when aliasing objects
MikaelMayer Sep 30, 2024
c3fc87b
Updated Dafny runtime to reflect the new constructs
MikaelMayer Sep 30, 2024
1764504
Fix for the issue. No more long-lived mutable borrows
MikaelMayer Sep 30, 2024
88b0656
formatting
MikaelMayer Sep 30, 2024
4cf2984
Fixed
MikaelMayer Sep 30, 2024
f395c70
Fixed one more test
MikaelMayer Sep 30, 2024
55a8ba0
Merge branch 'master' into fix-5800-soundness-rust-aliasing
MikaelMayer Sep 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Source/DafnyCore/Backends/Dafny/AST.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,7 +200,7 @@ module {:extern "DAST"} DAST {

datatype ClassItem = Method(Method)

datatype Field = Field(formal: Formal, defaultValue: Option<Expression>)
datatype Field = Field(formal: Formal, isConstant: bool, defaultValue: Option<Expression>)

datatype Formal = Formal(name: VarName, typ: Type, attributes: seq<Attribute>)

Expand Down Expand Up @@ -239,13 +239,13 @@ module {:extern "DAST"} DAST {
JumpTailCallStart() |
Halt() |
Print(Expression) |
ConstructorNewSeparator(fields: seq<Formal>)
ConstructorNewSeparator(fields: seq<Field>)
{
}

datatype AssignLhs =
Ident(ident: VarName) |
Select(expr: Expression, field: VarName) |
Select(expr: Expression, field: VarName, isConstant: bool) |
Index(expr: Expression, indices: seq<Expression>)

datatype CollKind = Seq | Array | Map
Expand Down
12 changes: 6 additions & 6 deletions Source/DafnyCore/Backends/Dafny/ASTBuilder.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,8 +133,8 @@ public void AddMethod(DAST.Method item) {
body.Add(item);
}

public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
fields.Add((DAST.Field)DAST.Field.create_Field(item, defaultValue));
public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
fields.Add((DAST.Field)DAST.Field.create_Field(item, isConstant, defaultValue));
}

public object Finish() {
Expand Down Expand Up @@ -187,7 +187,7 @@ public void AddMethod(DAST.Method item) {
body.Add(item);
}

public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
}

Expand Down Expand Up @@ -243,7 +243,7 @@ public void AddMethod(DAST.Method item) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
}

public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
}

Expand Down Expand Up @@ -343,7 +343,7 @@ public void AddMethod(DAST.Method item) {
body.Add(item);
}

public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
}

Expand All @@ -363,7 +363,7 @@ public object Finish() {
interface ClassLike {
void AddMethod(DAST.Method item);

void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue);
void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue);

public MethodBuilder Method(bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction,
ISequence<ISequence<Rune>> overridingPath,
Expand Down
36 changes: 22 additions & 14 deletions Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -482,17 +482,21 @@ protected override void TrDividedBlockStmt(Constructor m, DividedBlockStmt divid
if (writer is BuilderSyntaxTree<StatementContainer> builder) {
var membersToInitialize = ((TopLevelDeclWithMembers)m.EnclosingClass).Members.Where((md =>
md is Field and not ConstantField { Rhs: { } }));
var outFormals = membersToInitialize.Select((MemberDecl md) =>
DAST.Formal.create_Formal(
Sequence<Rune>.UnicodeFromString(
(md is ConstantField ? InternalFieldPrefix : "") +
md.GetCompileName(Options)),
GenType(((Field)md).Type.Subst(((TopLevelDeclWithMembers)((Field)md).EnclosingClass).ParentFormalTypeParametersToActuals))
, ParseAttributes(md.Attributes)
)
var outFields = membersToInitialize.Select((MemberDecl md) => {
var formal = DAST.Formal.create_Formal(
Sequence<Rune>.UnicodeFromString(
(md is ConstantField ? InternalFieldPrefix : "") +
md.GetCompileName(Options)),
GenType(((Field)md).Type.Subst(((TopLevelDeclWithMembers)((Field)md).EnclosingClass)
.ParentFormalTypeParametersToActuals))
, ParseAttributes(md.Attributes)
);
return DAST.Field.create_Field(formal, md is ConstantField,
Std.Wrappers.Option<DAST.Expression>.create_None());
}
).ToList();
builder.Builder.AddStatement((DAST.Statement)DAST.Statement.create_ConstructorNewSeparator(
Sequence<_IFormal>.FromArray(outFormals.ToArray())));
Sequence<_IField>.FromArray(outFields.ToArray())));
} else {
throw new InvalidCastException("Divided block statement outside of a statement container");
}
Expand Down Expand Up @@ -669,7 +673,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic,
Sequence<Rune>.UnicodeFromString(name),
compiler.GenType(type),
compiler.ParseAttributes(field.Attributes)
), rhsExpr);
), isConst, rhsExpr);
}

public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) {
Expand Down Expand Up @@ -1929,7 +1933,8 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
member.EnclosingClass is DatatypeDecl, GenType(expectedType)
), (DAST.AssignLhs)DAST.AssignLhs.create_Select(
objExpr,
Sequence<Rune>.UnicodeFromString(member.GetCompileName(Options))
Sequence<Rune>.UnicodeFromString(member.GetCompileName(Options)),
member is ConstantField
), this);
}
} else if (member is SpecialField { SpecialId: SpecialField.ID.ArrayLength } arraySpecial) {
Expand Down Expand Up @@ -1973,7 +1978,8 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
member.EnclosingClass is DatatypeDecl, GenType(expectedType)
), (DAST.AssignLhs)DAST.AssignLhs.create_Select(
objExpr,
Sequence<Rune>.UnicodeFromString(compiledName)
Sequence<Rune>.UnicodeFromString(compiledName),
member is ConstantField
), this);
} else if (member is SpecialField sf2 && sf2.SpecialId == SpecialField.ID.UseIdParam && sf2.IdParam is string fieldName && fieldName.StartsWith("is_")) {
obj(new BuilderSyntaxTree<ExprContainer>(objReceiver, this));
Expand Down Expand Up @@ -2005,7 +2011,8 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
member.EnclosingClass is DatatypeDecl, GenType(expectedType)
), (DAST.AssignLhs)DAST.AssignLhs.create_Select(
objExpr,
Sequence<Rune>.UnicodeFromString(InternalFieldPrefix + member.GetCompileName(Options))
Sequence<Rune>.UnicodeFromString(InternalFieldPrefix + member.GetCompileName(Options)),
member is ConstantField
), this);
} else {
return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select(
Expand All @@ -2015,7 +2022,8 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
member.EnclosingClass is DatatypeDecl, GenType(expectedType)
), (DAST.AssignLhs)DAST.AssignLhs.create_Select(
objExpr,
Sequence<Rune>.UnicodeFromString(member.GetCompileName(Options))
Sequence<Rune>.UnicodeFromString(member.GetCompileName(Options)),
member is ConstantField
), this);
}
}
Expand Down
54 changes: 34 additions & 20 deletions Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,18 +30,25 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
const allocate_fn := "_" + allocate
const update_field_uninit_macro :=
if pointerType.Raw? then "update_field_uninit!" else "update_field_uninit_object!"
const update_field_mut_uninit_macro :=
if pointerType.Raw? then "update_field_mut_uninit!" else "update_field_mut_uninit_object!"
const thisInConstructor :=
if pointerType.Raw? then R.Identifier("this") else R.Identifier("this").Clone()
const array_construct :=
if pointerType.Raw? then "construct" else "construct_object"
const modify_macro := R.dafny_runtime.MSel(if pointerType.Raw? then "modify!" else "md!").AsExpr()
const read_macro := R.dafny_runtime.MSel(if pointerType.Raw? then "read!" else "rd!").AsExpr()
const modify_field_macro := R.dafny_runtime.MSel("modify_field!").AsExpr()
const read_field_macro := R.dafny_runtime.MSel("read_field!").AsExpr()

function Object(underlying: R.Type): R.Type {
if pointerType.Raw? then R.PtrType(underlying) else R.ObjectType(underlying)
}
const placebos_usize := if pointerType.Raw? then "placebos_usize" else "placebos_usize_object"
const update_field_if_uninit_macro :=
if pointerType.Raw? then "update_field_if_uninit!" else "update_field_if_uninit_object!"
const update_field_mut_if_uninit_macro :=
if pointerType.Raw? then "update_field_mut_if_uninit!" else "update_field_mut_if_uninit_object!"
const Upcast :=
if pointerType.Raw? then "Upcast" else "UpcastObject"
const UpcastFnMacro :=
Expand Down Expand Up @@ -207,6 +214,9 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
for fieldI := 0 to |c.fields| {
var field := c.fields[fieldI];
var fieldType := GenType(field.formal.typ, GenTypeContext.default());
if !field.isConstant {
fieldType := R.dafny_runtime.MSel("Field").AsType().Apply([fieldType]);
}
usedTypeParams := GatherTypeParamNames(usedTypeParams, fieldType);
var fieldRustName := escapeVar(field.formal.name);
fields := fields + [R.Field(R.PUB, R.Formal(fieldRustName, fieldType))];
Expand Down Expand Up @@ -1392,7 +1402,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
case _ => enclosingType
};
if (forTrait) {
var selfFormal := if m.wasFunction then R.Formal.selfBorrowed else R.Formal.selfBorrowedMut;
var selfFormal := R.Formal.selfBorrowed;
params := [selfFormal] + params;
} else {
var tpe := GenType(instanceType, GenTypeContext.default());
Expand All @@ -1403,11 +1413,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
// For raw pointers, no borrowing is necessary, because it implements the Copy type
} else if selfId == "self" {
if tpe.IsObjectOrPointer() { // For classes and traits
if m.wasFunction {
tpe := R.SelfBorrowed;
} else {
tpe := R.SelfBorrowedMut;
}
tpe := R.SelfBorrowed;
} else { // For Rc-defined datatypes
if enclosingType.UserDefined? && enclosingType.resolved.kind.Datatype?
&& IsRcWrapped(enclosingType.resolved.attributes) {
Expand Down Expand Up @@ -1584,7 +1590,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
needsIIFE := false;
}

case Select(on, field) => {
case Select(on, field, isConstant) => {
var fieldName := escapeVar(field);
var onExpr, onOwned, recIdents := GenExpr(on, selfIdent, env, OwnershipAutoBorrowed);

Expand All @@ -1594,22 +1600,26 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
| UnaryOp("&", Identifier("this"), _) =>
var isAssignedVar := AddAssignedPrefix(fieldName);
if isAssignedVar in newEnv.names {
generated := R.dafny_runtime.MSel(update_field_uninit_macro).AsExpr().Apply(
var update_field_uninit :=
if isConstant then
update_field_uninit_macro
else
update_field_mut_uninit_macro;
generated := R.dafny_runtime.MSel(update_field_uninit).AsExpr().Apply(
[ thisInConstructor,
R.Identifier(fieldName),
R.Identifier(isAssignedVar),
rhs]);
newEnv := newEnv.RemoveAssigned(isAssignedVar);
} else {
// Already assigned, safe to override
generated := R.Assign(Some(R.SelectMember(modify_macro.Apply1(thisInConstructor), fieldName)), rhs);
generated := modify_field_macro.Apply([read_macro.Apply1(thisInConstructor).Sel(fieldName), rhs]);
}
case _ =>
if onExpr != R.Identifier("self") {
onExpr := modify_macro.Apply1(onExpr);
onExpr := read_macro.Apply1(onExpr);
}
generated :=
R.AssignMember(onExpr, fieldName, rhs);
generated := modify_field_macro.Apply([onExpr.Sel(fieldName), rhs]);
}
readIdents := recIdents;
needsIIFE := false;
Expand Down Expand Up @@ -1658,15 +1668,17 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
newEnv := env;
for i := 0 to |fields| {
var field := fields[i];
var fieldName := escapeVar(field.name);
var fieldTyp := GenType(field.typ, GenTypeContext.default());
var fieldName := escapeVar(field.formal.name);
var fieldTyp := GenType(field.formal.typ, GenTypeContext.default());
var isAssignedVar := AddAssignedPrefix(fieldName);
if isAssignedVar in newEnv.names {
assume {:axiom} InitializationValue(field.typ) < stmt; // Needed for termination
var rhs, _, _ := GenExpr(InitializationValue(field.typ), selfIdent, env, OwnershipOwned);
assume {:axiom} InitializationValue(field.formal.typ) < stmt; // Needed for termination
var rhs, _, _ := GenExpr(InitializationValue(field.formal.typ), selfIdent, env, OwnershipOwned);
readIdents := readIdents + {isAssignedVar};
generated := generated.Then(R.dafny_runtime.MSel(update_field_if_uninit_macro).AsExpr().Apply([
R.Identifier("this"), R.Identifier(fieldName), R.Identifier(isAssignedVar), rhs]));
var update_if_uninit :=
if field.isConstant then update_field_if_uninit_macro else update_field_mut_if_uninit_macro;
generated := generated.Then(R.dafny_runtime.MSel(update_if_uninit).AsExpr().Apply(
[ R.Identifier("this"), R.Identifier(fieldName), R.Identifier(isAssignedVar), rhs]));
newEnv := newEnv.RemoveAssigned(isAssignedVar);
}
}
Expand Down Expand Up @@ -1855,7 +1867,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
case CallName(_, Some(tpe), _, _, _) =>
var typ := GenType(tpe, GenTypeContext.default());
if typ.IsObjectOrPointer() && onExpr != R.Identifier("self") {
onExpr := modify_macro.Apply1(onExpr);
onExpr := read_macro.Apply1(onExpr);
}
case _ =>
}
Expand Down Expand Up @@ -3288,8 +3300,10 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
r := r.Sel(escapeVar(field));
if isConstant {
r := r.Apply0();
r := r.Clone(); // self could be &mut, so to avoid any borrow checker problem, we clone the value.
} else {
r := read_field_macro.Apply1(r); // Already contains a clone.
}
r := r.Clone(); // self could be &mut, so to avoid any borrow checker problem, we clone the value.
r, resultingOwnership := FromOwned(r, expectedOwnership);
readIdents := recIdents;
}
Expand Down
Loading