Skip to content

Commit

Permalink
Refactor codebase in preparation for hide PR (#5594)
Browse files Browse the repository at this point in the history 
Factors out the refactoring parts of
#5562

### Description
- Extracted methods into separate files
- Extracted code into separate methods

### How has this been tested?
- Pure refactoring, no additional tests needed

<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>
  • Loading branch information
@keyboardDrummer
keyboardDrummer authored Jul 4, 2024
1 parent 141053d commit 040b54c
Show file tree
Hide file tree
Showing 13 changed files with 622 additions and 587 deletions.
34 changes: 18 additions & 16 deletions Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,22 +70,8 @@ public void PrintStatement(Statement stmt, int indent) {
PrintAttributeArgs(s.Args, true);
wr.Write(";");

} else if (stmt is RevealStmt) {
var s = (RevealStmt)stmt;
wr.Write("reveal ");
var sep = "";
foreach (var e in s.Exprs) {
wr.Write(sep);
sep = ", ";
if (RevealStmt.SingleName(e) != null) {
// this will do the printing correctly for labels (or label-lookalikes) like 00_023 (which by PrintExpression below would be printed as 23)
wr.Write(RevealStmt.SingleName(e));
} else {
PrintExpression(e, true);
}
}
wr.Write(";");

} else if (stmt is RevealStmt revealStmt) {
PrintRevealStmt(revealStmt);
} else if (stmt is BreakStmt) {
var s = (BreakStmt)stmt;
if (s.TargetLabel != null) {
Expand Down Expand Up @@ -471,6 +457,22 @@ public void PrintStatement(Statement stmt, int indent) {
}
}

private void PrintRevealStmt(RevealStmt revealStmt) {
wr.Write("reveal ");
var sep = "";
foreach (var e in revealStmt.Exprs) {
wr.Write(sep);
sep = ", ";
if (RevealStmt.SingleName(e) != null) {
// this will do the printing correctly for labels (or label-lookalikes) like 00_023 (which by PrintExpression below would be printed as 23)
wr.Write(RevealStmt.SingleName(e));
} else {
PrintExpression(e, true);
}
}
wr.Write(";");
}

private void PrintModifyStmt(int indent, ModifyStmt s, bool omitFrame) {
Contract.Requires(0 <= indent);
Contract.Requires(s != null);
Expand Down
47 changes: 47 additions & 0 deletions Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,4 +53,51 @@ public static string SingleName(Expression e) {
public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
return formatter.SetIndentPrintRevealStmt(indentBefore, OwnedTokens);
}

public void ResolveRevealStmt(PreTypeResolver preTypeResolver, ResolutionContext resolutionContext) {
foreach (var expr in Exprs) {
var name = RevealStmt.SingleName(expr);
var labeledAssert = name == null ? null : preTypeResolver.DominatingStatementLabels.Find(name) as AssertLabel;
if (labeledAssert != null) {
LabeledAsserts.Add(labeledAssert);
} else {
var revealResolutionContext = resolutionContext with { InReveal = true };
if (expr is ApplySuffix applySuffix) {
var methodCallInfo = preTypeResolver.ResolveApplySuffix(applySuffix, revealResolutionContext, true);
if (methodCallInfo == null) {
// error has already been reported
} else if (methodCallInfo.Callee.Member is TwoStateLemma && !revealResolutionContext.IsTwoState) {
preTypeResolver.ReportError(methodCallInfo.Tok, "a two-state function can only be revealed in a two-state context");
} else if (methodCallInfo.Callee.AtLabel != null) {
Contract.Assert(methodCallInfo.Callee.Member is TwoStateLemma);
preTypeResolver.ReportError(methodCallInfo.Tok, "to reveal a two-state function, do not list any parameters or @-labels");
} else {
var call = new CallStmt(RangeToken, new List<Expression>(), methodCallInfo.Callee, methodCallInfo.ActualParameters);
ResolvedStatements.Add(call);
}
} else if (expr is NameSegment or ExprDotName) {
if (expr is NameSegment) {
preTypeResolver.ResolveNameSegment((NameSegment)expr, true, null, revealResolutionContext, true);
} else {
preTypeResolver.ResolveDotSuffix((ExprDotName)expr, true, null, revealResolutionContext, true);
}
var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression;
if (callee == null) {
} else if (callee.Member is Lemma or TwoStateLemma && Attributes.Contains(callee.Member.Attributes, "axiom")) {
//The revealed member is a function
preTypeResolver.ReportError(callee.tok, "to reveal a function ({0}), append parentheses", callee.Member.ToString().Substring(7));
} else {
var call = new CallStmt(RangeToken, new List<Expression>(), callee, new List<ActualBinding>(), expr.tok);
ResolvedStatements.Add(call);
}
} else {
preTypeResolver.ResolveExpression(expr, revealResolutionContext);
}
}
}

foreach (var a in ResolvedStatements) {
preTypeResolver.ResolveStatement(a, resolutionContext);
}
}
}
6 changes: 3 additions & 3 deletions Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1184,7 +1184,7 @@ private void ReportMemberNotFoundError(IToken tok, string memberName, [CanBeNull
/// <param name="specialOpaqueHackAllowance">If "true", treats an expression "f" where "f" is an instance function, as "this.f", even though
/// there is no "this" in scope. This seems like a terrible hack, because it breaks scope invariants about the AST. But, for now, it's here
/// to mimic what the legacy resolver does.</param>
Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<ActualBinding> args,
public Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<ActualBinding> args,
ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true, bool specialOpaqueHackAllowance = false) {
Contract.Requires(expr != null);
Contract.Requires(!expr.WasResolved());
Expand Down Expand Up @@ -1439,7 +1439,7 @@ private bool ResolveDatatypeConstructor(NameSegment expr, List<ActualBinding>/*?
/// <param name="resolutionContext"></param>
/// <param name="allowMethodCall">If false, generates an error if the name denotes a method. If true and the name denotes a method, returns
/// a Resolver_MethodCall.</param>
Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<ActualBinding> args, ResolutionContext resolutionContext, bool allowMethodCall) {
public Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<ActualBinding> args, ResolutionContext resolutionContext, bool allowMethodCall) {
Contract.Requires(expr != null);
Contract.Requires(!expr.WasResolved());
Contract.Requires(resolutionContext != null);
Expand Down Expand Up @@ -1710,7 +1710,7 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext
}
Label atLabel = null;
if (e.AtTok != null) {
atLabel = dominatingStatementLabels.Find(e.AtTok.val);
atLabel = DominatingStatementLabels.Find(e.AtTok.val);
if (atLabel == null) {
ReportError(e.AtTok, "no label '{0}' in scope at this time", e.AtTok.val);
}
Expand Down
83 changes: 17 additions & 66 deletions Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,14 +13,9 @@

namespace Microsoft.Dafny {
public partial class PreTypeResolver : INewOrOldResolver {
private Scope<Statement> enclosingStatementLabels;
private readonly Scope<Label> dominatingStatementLabels;
public Scope<Label> DominatingStatementLabels => dominatingStatementLabels;
public Scope<Label> DominatingStatementLabels { get; }

public Scope<Statement> EnclosingStatementLabels {
get => enclosingStatementLabels;
set => enclosingStatementLabels = value;
}
public Scope<Statement> EnclosingStatementLabels { get; set; }

public List<Statement> LoopStack {
get => loopStack;
Expand Down Expand Up @@ -70,10 +65,10 @@ void ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionCont
} else {
var r = EnclosingStatementLabels.Push(lnode.Name, stmt);
Contract.Assert(r == Scope<Statement>.PushResult.Success); // since we just checked for duplicates, we expect the Push to succeed
if (dominatingStatementLabels.Find(lnode.Name) != null) {
if (DominatingStatementLabels.Find(lnode.Name) != null) {
ReportError(lnode.Tok, "label shadows a dominating label");
} else {
var rr = dominatingStatementLabels.Push(lnode.Name, lnode);
var rr = DominatingStatementLabels.Push(lnode.Name, lnode);
Contract.Assert(rr == Scope<Label>.PushResult.Success); // since we just checked for duplicates, we expect the Push to succeed
}
}
Expand All @@ -91,7 +86,7 @@ void ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionCont
if (!resolutionContext.IsTwoState) {
ReportError(tok, $"{expressionDescription} expressions are not allowed in this context");
} else if (labelName != null) {
label = dominatingStatementLabels.Find(labelName);
label = DominatingStatementLabels.Find(labelName);
if (label == null) {
ReportError(tok, $"no label '{labelName}' in scope at this time");
}
Expand All @@ -117,52 +112,8 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
ResolveExpression(e, resolutionContext);
}

} else if (stmt is RevealStmt) {
var s = (RevealStmt)stmt;
foreach (var expr in s.Exprs) {
var name = RevealStmt.SingleName(expr);
var labeledAssert = name == null ? null : dominatingStatementLabels.Find(name) as AssertLabel;
if (labeledAssert != null) {
s.LabeledAsserts.Add(labeledAssert);
} else {
var revealResolutionContext = resolutionContext with { InReveal = true };
if (expr is ApplySuffix applySuffix) {
var methodCallInfo = ResolveApplySuffix(applySuffix, revealResolutionContext, true);
if (methodCallInfo == null) {
// error has already been reported
} else if (methodCallInfo.Callee.Member is TwoStateLemma && !revealResolutionContext.IsTwoState) {
ReportError(methodCallInfo.Tok, "a two-state function can only be revealed in a two-state context");
} else if (methodCallInfo.Callee.AtLabel != null) {
Contract.Assert(methodCallInfo.Callee.Member is TwoStateLemma);
ReportError(methodCallInfo.Tok, "to reveal a two-state function, do not list any parameters or @-labels");
} else {
var call = new CallStmt(s.RangeToken, new List<Expression>(), methodCallInfo.Callee, methodCallInfo.ActualParameters);
s.ResolvedStatements.Add(call);
}
} else if (expr is NameSegment or ExprDotName) {
if (expr is NameSegment) {
ResolveNameSegment((NameSegment)expr, true, null, revealResolutionContext, true);
} else {
ResolveDotSuffix((ExprDotName)expr, true, null, revealResolutionContext, true);
}
var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression;
if (callee == null) {
} else if (callee.Member is Lemma or TwoStateLemma && Attributes.Contains(callee.Member.Attributes, "axiom")) {
//The revealed member is a function
ReportError(callee.tok, "to reveal a function ({0}), append parentheses", callee.Member.ToString().Substring(7));
} else {
var call = new CallStmt(s.RangeToken, new List<Expression>(), callee, new List<ActualBinding>(), expr.tok);
s.ResolvedStatements.Add(call);
}
} else {
ResolveExpression(expr, revealResolutionContext);
}
}
}
foreach (var a in s.ResolvedStatements) {
ResolveStatement(a, resolutionContext);
}

} else if (stmt is RevealStmt revealStmt) {
revealStmt.ResolveRevealStmt(this, resolutionContext);
} else if (stmt is BreakStmt) {
var s = (BreakStmt)stmt;
if (s.TargetLabel != null) {
Expand Down Expand Up @@ -329,15 +280,15 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
ScopePushAndReport(v, "bound-variable", false);
}
}
dominatingStatementLabels.PushMarker();
DominatingStatementLabels.PushMarker();
ResolveBlockStatement(s.Thn, resolutionContext);
dominatingStatementLabels.PopMarker();
DominatingStatementLabels.PopMarker();
scope.PopMarker();

if (s.Els != null) {
dominatingStatementLabels.PushMarker();
DominatingStatementLabels.PushMarker();
ResolveStatement(s.Els, resolutionContext);
dominatingStatementLabels.PopMarker();
DominatingStatementLabels.PopMarker();
}

} else if (stmt is AlternativeStmt) {
Expand Down Expand Up @@ -511,9 +462,9 @@ private void ResolveOneBodyLoopStmt(OneBodyLoopStmt s, ResolutionContext resolut

if (s.Body != null) {
loopStack.Add(s); // push
dominatingStatementLabels.PushMarker();
DominatingStatementLabels.PushMarker();
ResolveStatement(s.Body, resolutionContext);
dominatingStatementLabels.PopMarker();
DominatingStatementLabels.PopMarker();
loopStack.RemoveAt(loopStack.Count - 1); // pop
}

Expand Down Expand Up @@ -560,9 +511,9 @@ private void ResolveCalc(CalcStmt s, ResolutionContext resolutionContext) {
loopStack = new List<Statement>();
foreach (var h in s.Hints) {
foreach (var oneHint in h.Body) {
dominatingStatementLabels.PushMarker();
DominatingStatementLabels.PushMarker();
ResolveStatement(oneHint, resolutionContext);
dominatingStatementLabels.PopMarker();
DominatingStatementLabels.PopMarker();
}
}
EnclosingStatementLabels = prevLblStmts;
Expand Down Expand Up @@ -1334,7 +1285,7 @@ void ResolveAlternatives(List<GuardedAlternative> alternatives, AlternativeLoopS
}
foreach (var alternative in alternatives) {
scope.PushMarker();
dominatingStatementLabels.PushMarker();
DominatingStatementLabels.PushMarker();
if (alternative.IsBindingGuard) {
var exists = (ExistsExpr)alternative.Guard;
foreach (var v in exists.BoundVars) {
Expand All @@ -1345,7 +1296,7 @@ void ResolveAlternatives(List<GuardedAlternative> alternatives, AlternativeLoopS
foreach (Statement ss in alternative.Body) {
ResolveStatementWithLabels(ss, resolutionContext);
}
dominatingStatementLabels.PopMarker();
DominatingStatementLabels.PopMarker();
scope.PopMarker();
}
if (loopToCatchBreaks != null) {
Expand Down
18 changes: 9 additions & 9 deletions Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -427,7 +427,7 @@ private PreTypeResolver(ModuleResolver resolver, PreTypeInferenceModuleState pre

scope = new Scope<IVariable>(resolver.Options);
EnclosingStatementLabels = new Scope<Statement>(resolver.Options);
dominatingStatementLabels = new Scope<Label>(resolver.Options);
DominatingStatementLabels = new Scope<Label>(resolver.Options);
Constraints = new PreTypeConstraints(this);
}

Expand Down Expand Up @@ -1216,19 +1216,19 @@ void ResolveIterator(IteratorDecl iter) {

// Resolve body
if (iter.Body != null) {
dominatingStatementLabels.PushMarker();
DominatingStatementLabels.PushMarker();
foreach (var req in iter.Requires) {
if (req.Label != null) {
if (dominatingStatementLabels.Find(req.Label.Name) != null) {
if (DominatingStatementLabels.Find(req.Label.Name) != null) {
ReportError(req.Label.Tok, "assert label shadows a dominating label");
} else {
var rr = dominatingStatementLabels.Push(req.Label.Name, req.Label);
var rr = DominatingStatementLabels.Push(req.Label.Name, req.Label);
Contract.Assert(rr == Scope<Label>.PushResult.Success); // since we just checked for duplicates, we expect the Push to succeed
}
}
}
ResolveBlockStatement(iter.Body, ResolutionContext.FromCodeContext(iter));
dominatingStatementLabels.PopMarker();
DominatingStatementLabels.PopMarker();
Constraints.SolveAllTypeConstraints($"body of iterator '{iter.Name}'");
}

Expand Down Expand Up @@ -1413,19 +1413,19 @@ void ResolveMethod(Method m) {
ScopePushExpectSuccess(k, "_k parameter", false);
}

dominatingStatementLabels.PushMarker();
DominatingStatementLabels.PushMarker();
foreach (var req in m.Req) {
if (req.Label != null) {
if (dominatingStatementLabels.Find(req.Label.Name) != null) {
if (DominatingStatementLabels.Find(req.Label.Name) != null) {
ReportError(req.Label.Tok, "assert label shadows a dominating label");
} else {
var rr = dominatingStatementLabels.Push(req.Label.Name, req.Label);
var rr = DominatingStatementLabels.Push(req.Label.Name, req.Label);
Contract.Assert(rr == Scope<Label>.PushResult.Success); // since we just checked for duplicates, we expect the Push to succeed
}
}
}
ResolveBlockStatement(m.Body, ResolutionContext.FromCodeContext(m));
dominatingStatementLabels.PopMarker();
DominatingStatementLabels.PopMarker();
Constraints.SolveAllTypeConstraints($"body of {m.WhatKind} '{m.Name}'");
}

Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Resolver/PreType/PreTypeResolver.Match.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,9 @@ void ResolveNestedMatchStmt(NestedMatchStmt stmt, ResolutionContext resolutionCo
scope.PushMarker();
ResolveExtendedPattern(stmt.Source.tok, mc.Pat, stmt.Source.PreType, false, resolutionContext);

dominatingStatementLabels.PushMarker();
DominatingStatementLabels.PushMarker();
mc.Body.ForEach(ss => ResolveStatementWithLabels(ss, resolutionContext));
dominatingStatementLabels.PopMarker();
DominatingStatementLabels.PopMarker();

scope.PopMarker();
}
Expand Down
Loading

0 comments on commit 040b54c

Please sign in to comment.