Skip to content

Commit

Permalink
Support class fields in the Rust backend (dafny-lang#4429)
Browse files Browse the repository at this point in the history 
Support class fields in the Rust backend



Right now, we still use reference counted pointers, which means that
cycles will result in memory leaks. I plan to address this with cycle
collection in a later PR.

<small>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).</small>

---
Stack created with [Sapling](https://sapling-scm.com). Best reviewed
with [ReviewStack](https://reviewstack.dev/dafny-lang/dafny/pull/4429).
* dafny-lang#4438
* __->__ dafny-lang#4429
  • Loading branch information
@shadaj @keyboardDrummer
shadaj authored and keyboardDrummer committed Sep 15, 2023
1 parent 38a8f67 commit 824675f
Show file tree
Hide file tree
Showing 6 changed files with 2,671 additions and 2,243 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/msbuild.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@ jobs:
reportgenerator \
-reports:"./**/coverage.cobertura.xml" \
-reporttypes:Cobertura -targetdir:coverage-cobertura \
-classfilters:"-Microsoft.Dafny.*PreType*;-Microsoft.Dafny.ResolverPass;-Microsoft.Dafny.*Underspecification*;-Microsoft.Dafny.DetectUnderspecificationVisitor;-Microsoft.Dafny.Microsoft.Dafny.UnderspecificationDetector;-DAST.*;-DCOMP.*"
-classfilters:"-Microsoft.Dafny.*PreType*;-Microsoft.Dafny.ResolverPass;-Microsoft.Dafny.*Underspecification*;-Microsoft.Dafny.DetectUnderspecificationVisitor;-Microsoft.Dafny.Microsoft.Dafny.UnderspecificationDetector;-Microsoft.Dafny.Compilers.DafnyCompiler;-DAST.*;-DCOMP.*"
# Generate HTML from combined report, leaving out XUnitExtensions
reportgenerator \
-reports:"coverage-cobertura/Cobertura.xml" \
Expand Down
16 changes: 10 additions & 6 deletions Source/DafnyCore/Compilers/Dafny/AST.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,6 @@ module {:extern "DAST"} DAST {

datatype ModuleItem = Module(Module) | Class(Class) | Trait(Trait) | Newtype(Newtype) | Datatype(Datatype)

datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Optional<Expression>)

datatype Type =
Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) |
Tuple(seq<Type>) |
Expand All @@ -23,15 +21,19 @@ module {:extern "DAST"} DAST {

datatype Ident = Ident(id: string)

datatype Class = Class(name: string, superClasses: seq<Type>, body: seq<ClassItem>)
datatype Class = Class(name: string, typeParams: seq<Type>, superClasses: seq<Type>, fields: seq<Field>, body: seq<ClassItem>)

datatype Trait = Trait(name: string, typeParams: seq<Type>, body: seq<ClassItem>)

datatype Datatype = Datatype(name: string, enclosingModule: Ident, typeParams: seq<Type>, ctors: seq<DatatypeCtor>, body: seq<ClassItem>, isCo: bool)

datatype DatatypeCtor = DatatypeCtor(name: string, args: seq<Formal>, hasAnyArgs: bool /* includes ghost */)

datatype ClassItem = Method(Method) | Field(Formal)
datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Optional<Expression>)

datatype ClassItem = Method(Method)

datatype Field = Field(formal: Formal, defaultValue: Optional<Expression>)

datatype Formal = Formal(name: string, typ: Type)

Expand All @@ -41,7 +43,7 @@ module {:extern "DAST"} DAST {

datatype Statement =
DeclareVar(name: string, typ: Type, maybeValue: Optional<Expression>) |
Assign(name: string, value: Expression) |
Assign(lhs: AssignLhs, value: Expression) |
If(cond: Expression, thn: seq<Statement>, els: seq<Statement>) |
While(cond: Expression, body: seq<Statement>) |
Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Optional<seq<Ident>>) |
Expand All @@ -50,6 +52,8 @@ module {:extern "DAST"} DAST {
Halt() |
Print(Expression)

datatype AssignLhs = Ident(Ident) | Select(expr: Expression, field: string)

datatype Expression =
Literal(Literal) |
Ident(string) |
Expand All @@ -66,7 +70,7 @@ module {:extern "DAST"} DAST {
Ite(cond: Expression, thn: Expression, els: Expression) |
UnOp(unOp: UnaryOp, expr: Expression) |
BinOp(op: string, left: Expression, right: Expression) |
Select(expr: Expression, field: string, onDatatype: bool) |
Select(expr: Expression, field: string, isConstant: bool, onDatatype: bool) |
SelectFn(expr: Expression, field: string, onDatatype: bool, isStatic: bool, arity: nat) |
TupleSelect(expr: Expression, index: nat) |
Call(on: Expression, name: Ident, typeArgs: seq<Type>, args: seq<Expression>) |
Expand Down
121 changes: 74 additions & 47 deletions Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,36 +65,41 @@ public object Finish() {
interface ClassContainer {
void AddClass(Class item);

public ClassBuilder Class(string name, List<DAST.Type> superClasses) {
return new ClassBuilder(this, name, superClasses);
public ClassBuilder Class(string name, List<DAST.Type> typeParams, List<DAST.Type> superClasses) {
return new ClassBuilder(this, name, typeParams, superClasses);
}
}

class ClassBuilder : ClassLike {
readonly ClassContainer parent;
readonly string name;
readonly List<DAST.Type> typeParams;
readonly List<DAST.Type> superClasses;
readonly List<ClassItem> body = new();
readonly List<DAST.Field> fields = new();
readonly List<DAST.Method> body = new();

public ClassBuilder(ClassContainer parent, string name, List<DAST.Type> superClasses) {
public ClassBuilder(ClassContainer parent, string name, List<DAST.Type> typeParams, List<DAST.Type> superClasses) {
this.parent = parent;
this.name = name;
this.typeParams = typeParams;
this.superClasses = superClasses;
}

public void AddMethod(DAST.Method item) {
body.Add((ClassItem)ClassItem.create_Method(item));
body.Add(item);
}

public void AddField(DAST.Formal item) {
body.Add((ClassItem)ClassItem.create_Field(item));
public void AddField(DAST.Formal item, DAST.Expression defaultValue) {
fields.Add((DAST.Field)DAST.Field.create_Field(item, defaultValue != null ? Optional<DAST._IExpression>.create_Some(defaultValue) : Optional<DAST._IExpression>.create_None()));
}

public object Finish() {
parent.AddClass((Class)Class.create(
Sequence<Rune>.UnicodeFromString(this.name),
Sequence<DAST.Type>.FromArray(this.typeParams.ToArray()),
Sequence<DAST.Type>.FromArray(this.superClasses.ToArray()),
Sequence<ClassItem>.FromArray(body.ToArray())
Sequence<DAST.Field>.FromArray(this.fields.ToArray()),
Sequence<DAST.Method>.FromArray(body.ToArray())
));
return parent;
}
Expand All @@ -112,7 +117,7 @@ class TraitBuilder : ClassLike {
readonly TraitContainer parent;
readonly string name;
readonly List<DAST.Type> typeParams;
readonly List<ClassItem> body = new();
readonly List<DAST.Method> body = new();

public TraitBuilder(TraitContainer parent, string name, List<DAST.Type> typeParams) {
this.parent = parent;
Expand All @@ -123,24 +128,24 @@ public TraitBuilder(TraitContainer parent, string name, List<DAST.Type> typePara
public void AddMethod(DAST.Method item) {
// remove existing method with the same name, because we're going to define an implementation
for (int i = 0; i < body.Count; i++) {
if (body[i].is_Method && body[i].dtor_Method_a0.dtor_name.Equals(item.dtor_name)) {
if (body[i].is_Method && body[i].dtor_name.Equals(item.dtor_name)) {
body.RemoveAt(i);
break;
}
}

body.Add((ClassItem)ClassItem.create_Method(item));
body.Add(item);
}

public void AddField(DAST.Formal item) {
public void AddField(DAST.Formal item, DAST.Expression defaultValue) {
throw new NotImplementedException();
}

public object Finish() {
parent.AddTrait((Trait)Trait.create(
Sequence<Rune>.UnicodeFromString(this.name),
Sequence<DAST.Type>.FromArray(typeParams.ToArray()),
Sequence<ClassItem>.FromArray(body.ToArray()))
Sequence<DAST.Method>.FromArray(body.ToArray()))
);
return parent;
}
Expand Down Expand Up @@ -175,7 +180,7 @@ public void AddMethod(DAST.Method item) {
throw new NotImplementedException();
}

public void AddField(DAST.Formal item) {
public void AddField(DAST.Formal item, DAST.Expression defaultValue) {
throw new NotImplementedException();
}

Expand Down Expand Up @@ -206,7 +211,7 @@ class DatatypeBuilder : ClassLike {
readonly List<DAST.Type> typeParams;
readonly List<DAST.DatatypeCtor> ctors;
readonly bool isCo;
readonly List<ClassItem> body = new();
readonly List<DAST.Method> body = new();

public DatatypeBuilder(DatatypeContainer parent, string name, ISequence<Rune> enclosingModule, List<DAST.Type> typeParams, List<DAST.DatatypeCtor> ctors, bool isCo) {
this.parent = parent;
Expand All @@ -218,10 +223,10 @@ public DatatypeBuilder(DatatypeContainer parent, string name, ISequence<Rune> en
}

public void AddMethod(DAST.Method item) {
body.Add((ClassItem)ClassItem.create_Method(item));
body.Add(item);
}

public void AddField(DAST.Formal item) {
public void AddField(DAST.Formal item, DAST.Expression defaultValue) {
throw new NotImplementedException();
}

Expand All @@ -231,7 +236,7 @@ public object Finish() {
this.enclosingModule,
Sequence<DAST.Type>.FromArray(typeParams.ToArray()),
Sequence<DAST.DatatypeCtor>.FromArray(ctors.ToArray()),
Sequence<ClassItem>.FromArray(body.ToArray()),
Sequence<DAST.Method>.FromArray(body.ToArray()),
this.isCo
));
return parent;
Expand All @@ -241,7 +246,7 @@ public object Finish() {
interface ClassLike {
void AddMethod(DAST.Method item);

void AddField(DAST.Formal item);
void AddField(DAST.Formal item, DAST.Expression defaultValue);

public MethodBuilder Method(
bool isStatic, bool hasBody,
Expand Down Expand Up @@ -351,13 +356,13 @@ public void Print(DAST.Expression expr) {
}

public AssignBuilder Assign() {
var ret = new AssignBuilder(false, null);
var ret = new AssignBuilder();
AddBuildable(ret);
return ret;
}

public AssignBuilder DeclareAndAssign(DAST.Type type) {
var ret = new AssignBuilder(true, type);
public DeclareBuilder DeclareAndAssign(DAST.Type type, string name) {
var ret = new DeclareBuilder(type, name);
AddBuildable(ret);
return ret;
}
Expand Down Expand Up @@ -407,26 +412,58 @@ public void AddBuildable(BuildableStatement item) {
}

public List<object> ForkList() {
return new List<object>();
var ret = new List<object>();
list.Add(ret);
return ret;
}
}

class AssignBuilder : ExprContainer, BuildableStatement {
readonly bool isDeclare;
class DeclareBuilder : ExprContainer, BuildableStatement {
readonly DAST.Type type;
string name = null;
readonly string name;
public object value;

public AssignBuilder(bool isDeclare, DAST.Type type) {
this.isDeclare = isDeclare;
public DeclareBuilder(DAST.Type type, string name) {
this.type = type;
this.name = name;
}

public void SetName(string name) {
if (this.name != null && this.name != name) {
throw new InvalidOperationException("Cannot change name of variable in assignment: " + this.name + " -> " + name);
public void AddExpr(DAST.Expression value) {
if (this.value != null) {
throw new InvalidOperationException();
} else {
this.name = name;
this.value = value;
}
}

public void AddBuildable(BuildableExpr value) {
if (this.value != null) {
throw new InvalidOperationException();
} else {
this.value = value;
}
}

public DAST.Statement Build() {
if (this.value == null) {
return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, DAST.Optional<DAST._IExpression>.create_None());
} else {
var builtValue = new List<DAST.Expression>();
ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, DAST.Optional<DAST._IExpression>.create_Some(builtValue[0]));
}
}
}

class AssignBuilder : ExprContainer, BuildableStatement {
DAST.AssignLhs lhs = null;
public object value;

public void SetLhs(DAST.AssignLhs lhs) {
if (this.lhs != null && this.lhs != lhs) {
throw new InvalidOperationException("Cannot change name of variable in assignment: " + this.lhs + " -> " + lhs);
} else {
this.lhs = lhs;
}
}

Expand All @@ -447,22 +484,12 @@ public void AddBuildable(BuildableExpr value) {
}

public DAST.Statement Build() {
if (isDeclare) {
if (this.value == null) {
return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, DAST.Optional<DAST._IExpression>.create_None());
} else {
var builtValue = new List<DAST.Expression>();
ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, DAST.Optional<DAST._IExpression>.create_Some(builtValue[0]));
}
if (this.value == null) {
throw new InvalidOperationException("Cannot assign null value to variable: " + lhs);
} else {
if (this.value == null) {
throw new InvalidOperationException("Cannot assign null value to variable: " + name);
} else {
var builtValue = new List<DAST.Expression>();
ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
return (DAST.Statement)DAST.Statement.create_Assign(Sequence<Rune>.UnicodeFromString(name), builtValue[0]);
}
var builtValue = new List<DAST.Expression>();
ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
return (DAST.Statement)DAST.Statement.create_Assign(lhs, builtValue[0]);
}
}
}
Expand Down
Loading

0 comments on commit 824675f

Please sign in to comment.