Skip to content

Commit

Permalink
parsing, printing, and resolution
Browse files Browse the repository at this point in the history
  • Loading branch information
@fabiomadge
fabiomadge committed Aug 1, 2024
1 parent d8938a9 commit 3397cdc
Show file tree
Hide file tree
Showing 6 changed files with 105 additions and 20 deletions.
20 changes: 17 additions & 3 deletions Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -363,7 +363,7 @@ public void PrintStatement(Statement stmt, int indent) {
wr.Write(" ");
}
PrintUpdateRHS(s, indent);
wr.Write(";");
PrintBy(s);

} else if (stmt is CallStmt) {
// Most calls are printed from their concrete syntax given in the input. However, recursive calls to
Expand Down Expand Up @@ -395,8 +395,7 @@ public void PrintStatement(Statement stmt, int indent) {
wr.Write(" ");
PrintUpdateRHS(s.Update, indent);
}
wr.Write(";");

PrintBy(s.Update);
} else if (stmt is VarDeclPattern) {
var s = (VarDeclPattern)stmt;
if (s.tok is AutoGeneratedToken) {
Expand Down Expand Up @@ -455,6 +454,21 @@ public void PrintStatement(Statement stmt, int indent) {
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}

void PrintBy(ConcreteUpdateStatement s)
{
BlockStmt proof = s switch {
UpdateStmt updateStmt => updateStmt.Proof,
AssignOrReturnStmt returnStmt => returnStmt.Proof,
_ => null
};
if (proof != null) {
wr.Write(" by ");
PrintStatement(proof, indent);
} else {
wr.Write(";");
}
}
}

private void PrintRevealStmt(RevealStmt revealStmt) {
Expand Down
18 changes: 16 additions & 2 deletions Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ public class AssignOrReturnStmt : ConcreteUpdateStatement, ICloneable<AssignOrRe
public readonly ExprRhs Rhs; // this is the unresolved RHS, and thus can also be a method call
public readonly List<AssignmentRhs> Rhss;
public readonly AttributedToken KeywordToken;
public readonly BlockStmt Proof;
[FilledInDuringResolution] public readonly List<Statement> ResolvedStatements = new List<Statement>();
public override IEnumerable<Statement> SubStatements => ResolvedStatements;
public override IToken Tok {
Expand Down Expand Up @@ -43,13 +44,14 @@ public AssignOrReturnStmt(Cloner cloner, AssignOrReturnStmt original) : base(clo
Rhs = (ExprRhs)cloner.CloneRHS(original.Rhs);
Rhss = original.Rhss.ConvertAll(cloner.CloneRHS);
KeywordToken = cloner.AttributedTok(original.KeywordToken);
Proof = cloner.CloneBlockStmt(original.Proof);

if (cloner.CloneResolvedFields) {
ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList();
}
}

public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs rhs, AttributedToken keywordToken, List<AssignmentRhs> rhss)
public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs rhs, AttributedToken keywordToken, List<AssignmentRhs> rhss, BlockStmt proof = null)
: base(rangeToken, lhss) {
Contract.Requires(rangeToken != null);
Contract.Requires(lhss != null);
Expand All @@ -59,6 +61,7 @@ public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs
Rhs = rhs;
Rhss = rhss;
KeywordToken = keywordToken;
Proof = proof;
}

public override IEnumerable<Expression> PreResolveSubExpressions {
Expand Down Expand Up @@ -190,6 +193,17 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
return;
}

if (Proof != null) {
// clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body
var prevLblStmts = resolver.EnclosingStatementLabels;
var prevLoopStack = resolver.LoopStack;
resolver.EnclosingStatementLabels = new Scope<Statement>(resolver.Options);
resolver.LoopStack = new List<Statement>();
resolver.ResolveStatement(Proof, resolutionContext);
resolver.EnclosingStatementLabels = prevLblStmts;
resolver.LoopStack = prevLoopStack;
}

Expression lhsExtract = null;
if (expectExtract) {
if (resolutionContext.CodeContext is Method caller && caller.Outs.Count == 0 && KeywordToken == null) {
Expand Down Expand Up @@ -285,7 +299,7 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract,
}
}
// " temp, ... := MethodOrExpression, ...;"
UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2);
UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2, Proof);
if (expectExtract) {
up.OriginalInitialLhs = Lhss.Count == 0 ? null : Lhss[0];
}
Expand Down
22 changes: 19 additions & 3 deletions Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ public class UpdateStmt : ConcreteUpdateStatement, ICloneable<UpdateStmt>, ICanR
public readonly List<AssignmentRhs> Rhss;
public readonly bool CanMutateKnownState;
public Expression OriginalInitialLhs = null;
public readonly BlockStmt Proof;

public override IToken Tok {
get {
Expand Down Expand Up @@ -45,26 +46,29 @@ public UpdateStmt Clone(Cloner cloner) {
public UpdateStmt(Cloner cloner, UpdateStmt original) : base(cloner, original) {
Rhss = original.Rhss.Select(cloner.CloneRHS).ToList();
CanMutateKnownState = original.CanMutateKnownState;
Proof = cloner.CloneBlockStmt(original.Proof);
if (cloner.CloneResolvedFields) {
ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList();
}
}

public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss)
public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, BlockStmt proof = null)
: base(rangeToken, lhss) {
Contract.Requires(cce.NonNullElements(lhss));
Contract.Requires(cce.NonNullElements(rhss));
Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
Rhss = rhss;
CanMutateKnownState = false;
Proof = proof;
}
public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate)
public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate, BlockStmt proof = null)
: base(rangeToken, lhss) {
Contract.Requires(cce.NonNullElements(lhss));
Contract.Requires(cce.NonNullElements(rhss));
Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
Rhss = rhss;
CanMutateKnownState = mutate;
Proof = proof;
}

public override IEnumerable<Expression> PreResolveSubExpressions {
Expand Down Expand Up @@ -123,6 +127,18 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
resolver.ResolveAttributes(rhs, resolutionContext);
}

// resolve proof
if (Proof != null) {
// clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body
var prevLblStmts = resolver.EnclosingStatementLabels;
var prevLoopStack = resolver.LoopStack;
resolver.EnclosingStatementLabels = new Scope<Statement>(resolver.Options);
resolver.LoopStack = new List<Statement>();
resolver.ResolveStatement(Proof, resolutionContext);
resolver.EnclosingStatementLabels = prevLblStmts;
resolver.LoopStack = prevLoopStack;
}

// figure out what kind of UpdateStmt this is
if (firstEffectfulRhs == null) {
if (Lhss.Count == 0) {
Expand Down Expand Up @@ -178,7 +194,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
foreach (var ll in Lhss) {
resolvedLhss.Add(ll.Resolved);
}
CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok);
CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok, Proof);
a.OriginalInitialLhs = OriginalInitialLhs;
ResolvedStatements.Add(a);
}
Expand Down
9 changes: 6 additions & 3 deletions Source/DafnyCore/AST/Statements/Methods/CallStmt.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,12 @@ void ObjectInvariant() {
public readonly ActualBindings Bindings;
public List<Expression> Args => Bindings.Arguments;
public Expression OriginalInitialLhs = null;
public readonly BlockStmt Proof;

public Expression Receiver { get { return MethodSelect.Obj; } }
public Method Method { get { return (Method)MethodSelect.Member; } }

public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<ActualBinding> args, IToken overrideToken = null)
public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<ActualBinding> args, IToken overrideToken = null, BlockStmt proof = null)
: base(rangeToken) {
Contract.Requires(rangeToken != null);
Contract.Requires(cce.NonNullElements(lhs));
Expand All @@ -41,6 +42,7 @@ public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr me
this.MethodSelect = memSel;
this.overrideToken = overrideToken;
this.Bindings = new ActualBindings(args);
Proof = proof;
}

public CallStmt Clone(Cloner cloner) {
Expand All @@ -52,14 +54,15 @@ public CallStmt(Cloner cloner, CallStmt original) : base(cloner, original) {
Lhs = original.Lhs.Select(cloner.CloneExpr).ToList();
Bindings = new ActualBindings(cloner, original.Bindings);
overrideToken = original.overrideToken;
Proof = cloner.CloneBlockStmt(original.Proof);
}

/// <summary>
/// This constructor is intended to be used when constructing a resolved CallStmt. The "args" are expected
/// to be already resolved, and are all given positionally.
/// </summary>
public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args)
: this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e))) {
public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args, BlockStmt proof = null)
: this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e)), proof: proof) {
Bindings.AcceptArgumentExpressionsAsExactParameterList();
}

Expand Down
29 changes: 22 additions & 7 deletions Source/DafnyCore/Dafny.atg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2288,6 +2288,7 @@ UpdateStmt<out Statement/*!*/ s>
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
Expression e;
AssignmentRhs r;
BlockStmt proof = null;
IToken x = Token.NoToken;
IToken endTok = Token.NoToken;
IToken startToken = Token.NoToken;
Expand Down Expand Up @@ -2325,10 +2326,16 @@ UpdateStmt<out Statement/*!*/ s>
{ "," Rhs<out r> (. rhss.Add(r); .)
}
)
";" (. endTok = t; .)
(
"by" BlockStmt<out proof, out _, out _>
| ";"
)
| ":" (. SemErr(ErrorId.p_invalid_colon, new RangeToken(startToken, t), "invalid statement beginning here (is a 'label' keyword missing? or a 'const' or 'var' keyword?)"); .)
| { Attribute<ref attrs> } (. endToken = t; .)
";" (. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) }); .)
(
"by" BlockStmt<out proof, out _, out _>
| ";"
) (. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) }); .)
| { Attribute<ref attrs> } (. endToken = t; .)
(. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) });
SemErr(ErrorId.p_missing_semicolon, new RangeToken(startToken, t), "missing semicolon at end of statement");
Expand All @@ -2343,18 +2350,22 @@ UpdateStmt<out Statement/*!*/ s>
{ Attribute<ref attrs> } (. exceptionRhs = new ExprRhs(exceptionExpr, attrs); .)
{ "," Rhs<out r> (. rhss.Add(r); .)
}
(
"by" BlockStmt<out proof, out _, out _>
| ";"
)
";" (. endTok = t; .)
)
(. var rangeToken = new RangeToken(startToken, t);
if (suchThat != null) {
s = new AssignSuchThatStmt(rangeToken, lhss, suchThat, suchThatAssume, null);
} else if (exceptionRhs != null) {
s = new AssignOrReturnStmt(rangeToken, lhss, exceptionRhs, keywordToken, rhss);
s = new AssignOrReturnStmt(rangeToken, lhss, exceptionRhs, keywordToken, rhss, proof);
} else {
if (lhss.Count == 0 && rhss.Count == 0) {
s = new BlockStmt(rangeToken, new List<Statement>()); // error, give empty statement
} else {
s = new UpdateStmt(rangeToken, lhss, rhss);
s = new UpdateStmt(rangeToken, lhss, rhss, proof);
}
}
.)
Expand Down Expand Up @@ -2454,6 +2465,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
ExprRhs exceptionRhs = null;
Attributes attrs = null;
Attributes tokenAttrs = null;
BlockStmt proof = null;
IToken endTok;
IToken startToken = null;
s = dummyStmt;
Expand Down Expand Up @@ -2490,7 +2502,10 @@ VarDeclStatement<.out Statement/*!*/ s.>
{ "," Rhs<out r> (. rhss.Add(r); .)
}
]
SYNC ";" (. endTok = t; .)
( "by"
BlockStmt<out proof, out _, out _>
| SYNC ";" (. endTok = t; .)
)
(. ConcreteUpdateStatement update;
var lhsExprs = new List<Expression>();
if (isGhost || (rhss.Count == 0 && exceptionRhs == null && suchThat == null)) { // explicitly ghost or no init
Expand All @@ -2507,11 +2522,11 @@ VarDeclStatement<.out Statement/*!*/ s.>
if (suchThat != null) {
update = new AssignSuchThatStmt(updateRangeToken, lhsExprs, suchThat, suchThatAssume, attrs);
} else if (exceptionRhs != null) {
update = new AssignOrReturnStmt(updateRangeToken, lhsExprs, exceptionRhs, keywordToken, rhss);
update = new AssignOrReturnStmt(updateRangeToken, lhsExprs, exceptionRhs, keywordToken, rhss, proof);
} else if (rhss.Count == 0) {
update = null;
} else {
update = new UpdateStmt(updateRangeToken, lhsExprs, rhss);
update = new UpdateStmt(updateRangeToken, lhsExprs, rhss, proof);
}
s = new VarDeclStmt(rangeToken, lhss, update);
.)
Expand Down
27 changes: 25 additions & 2 deletions Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -650,6 +650,18 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo
ResolveAttributes(rhs, resolutionContext, false);
}

// resolve proof
if (update.Proof != null) {
// clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body
var prevLblStmts = resolver.EnclosingStatementLabels;
var prevLoopStack = resolver.LoopStack;
resolver.EnclosingStatementLabels = new Scope<Statement>(resolver.Options);
resolver.LoopStack = new List<Statement>();
resolver.ResolveStatement(update.Proof, resolutionContext);
resolver.EnclosingStatementLabels = prevLblStmts;
resolver.LoopStack = prevLoopStack;
}

// figure out what kind of UpdateStmt this is
if (firstEffectfulRhs == null) {
if (update.Lhss.Count == 0) {
Expand Down Expand Up @@ -703,7 +715,7 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo
} else if (ErrorCount == errorCountBeforeCheckingStmt) {
// a call statement
var resolvedLhss = update.Lhss.ConvertAll(ll => ll.Resolved);
var a = new CallStmt(update.RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok);
var a = new CallStmt(update.RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok, update.Proof);
a.OriginalInitialLhs = update.OriginalInitialLhs;
update.ResolvedStatements.Add(a);
}
Expand Down Expand Up @@ -929,6 +941,17 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r
return;
}

if (s.Proof != null) {
// clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body
var prevLblStmts = resolver.EnclosingStatementLabels;
var prevLoopStack = resolver.LoopStack;
resolver.EnclosingStatementLabels = new Scope<Statement>(resolver.Options);
resolver.LoopStack = new List<Statement>();
resolver.ResolveStatement(s.Proof, resolutionContext);
resolver.EnclosingStatementLabels = prevLblStmts;
resolver.LoopStack = prevLoopStack;
}

Expression lhsExtract = null;
if (expectExtract) {
if (enclosingMethod.Outs.Count == 0 && s.KeywordToken == null) {
Expand Down Expand Up @@ -991,7 +1014,7 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r
}
}
// " temp, ... := MethodOrExpression, ...;"
UpdateStmt up = new UpdateStmt(s.RangeToken, lhss2, rhss2);
UpdateStmt up = new UpdateStmt(s.RangeToken, lhss2, rhss2, s.Proof);
if (expectExtract) {
up.OriginalInitialLhs = s.Lhss.Count == 0 ? null : s.Lhss[0];
}
Expand Down

0 comments on commit 3397cdc

Please sign in to comment.