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

Erase ghost code in a separate phase #5831

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
Draft

Erase ghost code in a separate phase #5831

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
d72162f
Do part of the work of erasing ghost code before running target speci…
keyboardDrummer Oct 14, 2024
a9f82f9
Some success
keyboardDrummer Oct 14, 2024
79cd409
Erase ghost code
keyboardDrummer Oct 14, 2024
4bb79aa
Datatype contructor formals fixes
keyboardDrummer Oct 14, 2024
916e855
Fixes
keyboardDrummer Oct 14, 2024
b1c8883
Fixes
keyboardDrummer Oct 14, 2024
b22c4f3
Something with destructors
keyboardDrummer Oct 14, 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
22 changes: 22 additions & 0 deletions Source/DafnyCore/AST/AstVisitor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -230,6 +230,9 @@ protected virtual void VisitExpression(Expression expr, VisitorContext context)
}
}

foreach (var pattern in letExpr.LHSs) {
VisitCasePattern(pattern);
}
} else if (expr is QuantifierExpr quantifierExpr) {
foreach (BoundVar v in quantifierExpr.BoundVars) {
VisitUserProvidedType(v.Type, context);
Expand Down Expand Up @@ -260,6 +263,10 @@ protected virtual void VisitExpression(Expression expr, VisitorContext context)
foreach (var mc in nestedMatchExpr.Cases) {
VisitExtendedPattern(mc.Pat, context);
}

if (nestedMatchExpr.Flattened != null) {
VisitExpression(nestedMatchExpr.Flattened, context);
}
}

// Visit substatements
Expand Down Expand Up @@ -336,6 +343,8 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) {
VisitUserProvidedType(local.SyntacticType, context);
}

VisitCasePattern(varDeclPattern.LHS);

} else if (stmt is SingleAssignStmt assignStmt) {
if (assignStmt.Rhs is TypeRhs typeRhs) {
if (typeRhs.EType != null) {
Expand All @@ -358,6 +367,9 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) {
VisitExtendedPattern(mc.Pat, context);
}

if (nestedMatchStmt.Flattened != null) {
VisitStatement(nestedMatchStmt.Flattened, context);
}
} else if (stmt is MatchStmt matchStmt) {
foreach (MatchCaseStmt mc in matchStmt.Cases) {
if (mc.Arguments != null) {
Expand All @@ -378,6 +390,16 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) {
}
}

protected virtual void VisitCasePattern<T>(CasePattern<T> pattern) where T : class, IVariable {
if (pattern.Arguments == null) {
return;
}

foreach (var argument in pattern.Arguments) {
VisitCasePattern(argument);
}
}

/// <summary>
/// Visits the given statement.
/// Returns "true" to request that the caller
Expand Down
10 changes: 9 additions & 1 deletion Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,15 @@ public override IEnumerable<Expression> SubExpressions {
}
}

public override IEnumerable<INode> Children => new[] { Source }.Concat<Node>(Cases);
public override IEnumerable<INode> Children {
get {
var result = new[] { Source }.Concat<Node>(Cases);
if (Flattened != null) {
result = result.Concat(new[] { Flattened });
}
return result;
}
}

public void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext) {

Expand Down
10 changes: 9 additions & 1 deletion Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,15 @@ public NestedMatchStmt(Cloner cloner, NestedMatchStmt original) : base(cloner, o
}
}

public override IEnumerable<INode> Children => new[] { Source }.Concat<Node>(Cases);
public override IEnumerable<INode> Children {
get {
var result = new[] { Source }.Concat<Node>(Cases);
if (Flattened != null) {
result = result.Concat(new[] { Flattened });
}
return result;
}
}

public override IEnumerable<Statement> SubStatements {
get {
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
namespace Microsoft.Dafny;

public class LetExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBearingExpression, ICloneable<LetExpr>, ICanFormat {
public readonly List<CasePattern<BoundVar>> LHSs;
public List<CasePattern<BoundVar>> LHSs;
public readonly List<Expression> RHSs;
public readonly Expression Body;
public readonly bool Exact; // Exact==true means a regular let expression; Exact==false means an assign-such-that expression
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Members/MethodOrFunction.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ static MethodOrFunction() {
public readonly List<AttributedExpression> Req;
public readonly List<AttributedExpression> Ens;
public readonly Specification<Expression> Decreases;
public readonly List<Formal> Ins;
public List<Formal> Ins;

protected MethodOrFunction(RangeToken rangeToken, Name name, bool hasStaticKeyword, bool isGhost,
Attributes attributes, bool isRefining, List<TypeParameter> typeArgs, List<Formal> ins,
Expand Down
2 changes: 2 additions & 0 deletions Source/DafnyCore/AST/SystemModuleManager.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ public class SystemModuleManager {
public readonly Dictionary<int, SubsetTypeDecl> TotalArrowTypeDecls = new(); // same keys as arrowTypeDecl
readonly Dictionary<List<bool>, TupleTypeDecl> tupleTypeDecls = new(new Dafny.IEnumerableComparer<bool>());

public IEnumerable<TupleTypeDecl> TupleTypeDecls => tupleTypeDecls.Values;

internal readonly ValuetypeDecl[] valuetypeDecls;

/// <summary>
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ namespace Microsoft.Dafny;

public class DatatypeCtor : Declaration, TypeParameter.ParentType, IHasDocstring, ICanVerify {
public readonly bool IsGhost;
public readonly List<Formal> Formals;
public List<Formal> Formals;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Formals));
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
namespace Microsoft.Dafny;

public abstract class TopLevelDeclWithMembers : TopLevelDecl, IHasSymbolChildren {
public readonly List<MemberDecl> Members;
public List<MemberDecl> Members;

// TODO remove this and instead clone the AST after parsing.
public ImmutableList<MemberDecl> MembersBeforeResolution;
Expand Down
95 changes: 43 additions & 52 deletions Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -458,15 +458,15 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
Constructor ct = constructors[0];

foreach (var member in iter.Members) {
if (member is Field f && !f.IsGhost) {
if (member is Field f) {
cw.DeclareField(IdName(f), iter, false, false, f.Type, f.tok, PlaceboValue(f.Type, w, f.tok, true), f);
}
}

w.WriteLine("System.Collections.Generic.IEnumerator<object> _iter;");

// here we rely on the parameters and the corresponding fields having the same names
var nonGhostFormals = ct.Ins.Where(p => !p.IsGhost).ToList();
var nonGhostFormals = ct.Ins.ToList();
var parameters = nonGhostFormals.Comma(p => $"{TypeName(p.Type, w, p.tok)} {IdName(p)}");

// here's the initializer method
Expand Down Expand Up @@ -623,11 +623,10 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {

var wDefaultArguments = wDefault.Write(DtCreateName(groundingCtor)).ForkInParens();
wDefaultArguments.Append(wDefaultTypeArguments);
var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList();
if (defaultMethodTypeDescriptorCount != 0 && nonGhostFormals.Count != 0) {
if (defaultMethodTypeDescriptorCount != 0 && groundingCtor.Formals.Count != 0) {
wDefaultArguments.Write(", ");
}
wDefaultArguments.Write(nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok)));
wDefaultArguments.Write(groundingCtor.Formals.Comma(f => DefaultValue(f.Type, wDefault, f.tok)));
}

EmitTypeDescriptorMethod(dt, wr);
Expand All @@ -645,7 +644,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
var formalCount = WriteFormals(typeDescriptorCount > 0 ? ", " : "", ctor.Formals, wr);
var sep = typeDescriptorCount > 0 && formalCount > 0 ? ", " : "";
wr.NewBlock(")")
.WriteLine($"return new {DtCtorDeclarationName(ctor)}{DtT_TypeArgs}({wCallArguments}{sep}{ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
.WriteLine($"return new {DtCtorDeclarationName(ctor)}{DtT_TypeArgs}({wCallArguments}{sep}{ctor.Formals.Comma(FormalName)});");
}

if (dt.IsRecordType) {
Expand All @@ -659,7 +658,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
var formalCount = WriteFormals(typeDescriptorCount > 0 ? ", " : "", ctor.Formals, wr);
var sep = typeDescriptorCount > 0 && formalCount > 0 ? ", " : "";
wr.NewBlock(")")
.WriteLine($"return create({wCallArguments}{sep}{ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
.WriteLine($"return create({wCallArguments}{sep}{ctor.Formals.Comma(FormalName)});");
}

// query properties
Expand Down Expand Up @@ -721,7 +720,7 @@ bool InvalidType(Type ty, bool refTy) =>
(ty.AsTypeParameter != null && refTy && datatype.TypeArgs.Contains(ty.AsTypeParameter))
|| ty.TypeArgs.Exists(arg => InvalidType(arg, refTy || ty.IsRefType));

if (datatype.Ctors.Any(ctor => ctor.Formals.Any(f => !f.IsGhost && InvalidType(f.SyntacticType, false)))) {
if (datatype.Ctors.Any(ctor => ctor.Formals.Any(f => InvalidType(f.SyntacticType, false)))) {
return;
}

Expand Down Expand Up @@ -845,7 +844,7 @@ string PrintInvocation(Formal f, int i) {
var typeDescriptorArgumentsStrings = wCallArguments.ToString();
string constructorArgs;
if (!lazy) {
constructorArgs = ctor.Formals.Where(f => !f.IsGhost).Comma(PrintInvocation);
constructorArgs = ctor.Formals.Comma(PrintInvocation);
} else if (customReceiver) {
var sep0 = typeDescriptorCount != 0 ? ", " : "";
var sep1 = converters.Length != 0 ? ", " : "";
Expand All @@ -855,7 +854,7 @@ string PrintInvocation(Formal f, int i) {
var sep0 = typeDescriptorCount != 0 && converters.Length != 0 ? ", " : "";
constructorArgs = $"() => _Get().DowncastClone{uTypeArgs}({typeDescriptorArgumentsStrings}{sep0}{converters})";
}
var sep = typeDescriptorCount != 0 && (lazy || ctor.Formals.Any(f => !f.IsGhost)) ? ", " : "";
var sep = typeDescriptorCount != 0 && (lazy || ctor.Formals.Any()) ? ", " : "";
var className = lazy ? lazyClass : DtCtorDeclarationName(ctor);
wBody.WriteLine($"return new {className}{uTypeArgs}({typeDescriptorArgumentsStrings}{sep}{constructorArgs});");
}
Expand All @@ -875,7 +874,8 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre
if (!arg.IsGhost) {
var DtorM = arg.HasName ? InternalFieldPrefix + arg.CompileName : FieldName(arg, index);
// TN dtor_QDtorM { get; }
interfaceTree.WriteLine($"{TypeName(arg.Type, wr, arg.tok)} {DestructorGetterName(arg, ctor, index)} {{ get; }}");
interfaceTree.WriteLine(
$"{TypeName(arg.Type, wr, arg.tok)} {DestructorGetterName(arg, ctor, index)} {{ get; }}");

// public TN dtor_QDtorM { get {
// var d = this; // for inductive datatypes
Expand Down Expand Up @@ -909,6 +909,7 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre
if (ctor_i.IsGhost) {
continue;
}

var type = $"{dt.GetCompileName(Options)}_{ctor_i.GetCompileName(Options)}{DtT_TypeArgs}";
// TODO use pattern matching to replace cast.
var returnTheValue = $"return (({type})d).{IdProtect(DtorM)};";
Expand All @@ -917,9 +918,11 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre
} else {
wGet.WriteLine(returnTheValue);
}

compiledConstructorsProcessed++;
}
}

index++;
}
}
Expand All @@ -929,7 +932,7 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre

private void CompileDatatypeInterfaceMembers(DatatypeDecl dt, ConcreteSyntaxTree interfaceTree) {
foreach (var member in dt.Members) {
if (member.IsGhost || member.IsStatic) { continue; }
if (member.IsStatic) { continue; }
if (member is Function fn && !NeedsCustomReceiver(member)) {
CreateFunction(IdName(fn), CombineAllTypeArguments(fn), fn.Ins, fn.ResultType, fn.tok, fn.IsStatic,
false, fn, interfaceTree, false, false);
Expand Down Expand Up @@ -957,7 +960,7 @@ public override bool NeedsCustomReceiverInDatatype(MemberDecl member) {
foreach (var tp in d.TypeArgs) {
bool InvalidType(Type ty) => (ty.AsTypeParameter != null && ty.AsTypeParameter.Equals(tp))
|| ty.TypeArgs.Exists(InvalidType);
bool InvalidFormal(Formal f) => !f.IsGhost && InvalidType(f.SyntacticType);
bool InvalidFormal(Formal f) => InvalidType(f.SyntacticType);
switch (tp.Variance) {
//Can only be in output
case TypeParameter.TPVariance.Co:
Expand Down Expand Up @@ -1060,10 +1063,8 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr

var i = 0;
foreach (Formal arg in ctor.Formals) {
if (!arg.IsGhost) {
wr.WriteLine($"public readonly {TypeName(arg.Type, wr, arg.tok)} {FieldName(arg, i)};");
i++;
}
wr.WriteLine($"public readonly {TypeName(arg.Type, wr, arg.tok)} {FieldName(arg, i)};");
i++;
}

var typeDescriptorCount = EmitTypeDescriptorsForClass(dt.TypeArgs, dt, out var wTypeFields, out var wCtorParams, out var wBaseCallArguments, out var wCtorBody);
Expand All @@ -1080,10 +1081,8 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr
var w = wCtorBody;
i = 0;
foreach (Formal arg in ctor.Formals) {
if (!arg.IsGhost) {
w.WriteLine($"this.{FieldName(arg, i)} = {FormalName(arg, i)};");
i++;
}
w.WriteLine($"this.{FieldName(arg, i)} = {FormalName(arg, i)};");
i++;
}
}

Expand All @@ -1102,14 +1101,12 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr
w.Write("return oth != null");
i = 0;
foreach (var arg in ctor.Formals) {
if (!arg.IsGhost) {
var nm = FieldName(arg, i);
w.Write(IsDirectlyComparable(DatatypeWrapperEraser.SimplifyType(Options, arg.Type))
? $" && this.{nm} == oth.{nm}"
: $" && object.Equals(this.{nm}, oth.{nm})");
var nm = FieldName(arg, i);
w.Write(IsDirectlyComparable(DatatypeWrapperEraser.SimplifyType(Options, arg.Type))
? $" && this.{nm} == oth.{nm}"
: $" && object.Equals(this.{nm}, oth.{nm})");

i++;
}
i++;
}

w.WriteLine(";");
Expand All @@ -1122,11 +1119,9 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr
w.WriteLine($"hash = ((hash << 5) + hash) + {constructorIndex};");
i = 0;
foreach (Formal arg in ctor.Formals) {
if (!arg.IsGhost) {
string nm = FieldName(arg, i);
w.WriteLine($"hash = ((hash << 5) + hash) + ((ulong){DafnyHelpersClass}.GetHashCode(this.{nm}));");
i++;
}
string nm = FieldName(arg, i);
w.WriteLine($"hash = ((hash << 5) + hash) + ((ulong){DafnyHelpersClass}.GetHashCode(this.{nm}));");
i++;
}

w.WriteLine("return (int) hash;");
Expand Down Expand Up @@ -1156,19 +1151,17 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr
w.WriteLine($"{tempVar} += \"(\";");
i = 0;
foreach (var arg in ctor.Formals) {
if (!arg.IsGhost) {
if (i != 0) {
w.WriteLine($"{tempVar} += \", \";");
}

if (arg.Type.IsStringType && UnicodeCharEnabled) {
w.WriteLine($"{tempVar} += this.{FieldName(arg, i)}.ToVerbatimString(true);");
} else {
w.WriteLine($"{tempVar} += {DafnyHelpersClass}.ToString(this.{FieldName(arg, i)});");
}
if (i != 0) {
w.WriteLine($"{tempVar} += \", \";");
}

i++;
if (arg.Type.IsStringType && UnicodeCharEnabled) {
w.WriteLine($"{tempVar} += this.{FieldName(arg, i)}.ToVerbatimString(true);");
} else {
w.WriteLine($"{tempVar} += {DafnyHelpersClass}.ToString(this.{FieldName(arg, i)});");
}

i++;
}

w.WriteLine($"{tempVar} += \")\";");
Expand Down Expand Up @@ -2658,14 +2651,12 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
lambdaHeader.Write(" => ");

foreach (var arg in fn.Ins) {
if (!arg.IsGhost) {
var name = idGenerator.FreshId("_eta");
var ty = arg.Type.Subst(typeMap);
arguments.Write($"{prefixSep}{TypeName(ty, arguments, arg.tok)} {name}");
callArguments.Write($"{sep}{name}");
sep = ", ";
prefixSep = ", ";
}
var name = idGenerator.FreshId("_eta");
var ty = arg.Type.Subst(typeMap);
arguments.Write($"{prefixSep}{TypeName(ty, arguments, arg.tok)} {name}");
callArguments.Write($"{sep}{name}");
sep = ", ";
prefixSep = ", ";
}
return EnclosedLvalue(lambdaHeader.ToString(), obj, $".{wr}");
}
Expand Down
Loading
Loading