Skip to content

Commit

Permalink
Penetrating by blocks (#5779)
Browse files Browse the repository at this point in the history 
### Description
- Make all by block proofs penetrate the entire LHS

### How has this been tested?
- Updated tests for call statements and the three types of assignment
statements (`:=,` `:-`, `:|`)

<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 Oct 7, 2024
1 parent b5f57e0 commit c538717
Show file tree
Hide file tree
Showing 97 changed files with 1,281 additions and 1,217 deletions.
33 changes: 19 additions & 14 deletions Source/DafnyCore/AST/Expressions/StmtExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,20 +53,25 @@ public override IEnumerable<Expression> TerminalExpressions {
/// S is executed.
/// This method should be called only after successful resolution of the expression.
/// </summary>
public Expression GetSConclusion() {
// this is one place where we actually investigate what kind of statement .S is
if (S is PredicateStmt) {
var s = (PredicateStmt)S;
return s.Expr;
} else if (S is CalcStmt) {
var s = (CalcStmt)S;
return s.Result;
} else if (S is HideRevealStmt) {
return CreateBoolLiteral(tok, true); // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :)
} else if (S is AssignStatement) {
return CreateBoolLiteral(tok, true); // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :)
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
public Expression GetStatementConclusion() {
return GetStatementConclusion(S);
}

private Expression GetStatementConclusion(Statement statement) {
switch (statement) {
// this is one place where we actually investigate what kind of statement .S is
case PredicateStmt stmt:
return stmt.Expr;
case CalcStmt stmt:
return stmt.Result;
case HideRevealStmt:
return CreateBoolLiteral(tok, true); // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :)
case AssignStatement:
return CreateBoolLiteral(tok, true); // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :)
case BlockByProofStmt stmt:
return GetStatementConclusion(stmt.Body);
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
}

Expand Down
121 changes: 29 additions & 92 deletions Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,14 +19,18 @@

namespace Microsoft.Dafny {

interface ICanPrint {
void Render(TextWriter wr, Printer printer, int indent);
}

public partial class Printer {

/// <summary>
/// Prints from the current position of the current line.
/// If the statement requires several lines, subsequent lines are indented at "indent".
/// No newline is printed after the statement.
/// </summary>
public void PrintStatement(Statement stmt, int indent) {
public void PrintStatement(Statement stmt, int indent, bool includeSemicolon = true) {
Contract.Requires(stmt != null);

if (stmt.IsGhost && printMode == PrintModes.NoGhostOrIncludes) {
Expand All @@ -40,38 +44,13 @@ public void PrintStatement(Statement stmt, int indent) {
}
}

if (stmt is PredicateStmt) {
if (printMode == PrintModes.NoGhostOrIncludes) {
return;
}

Expression expr = ((PredicateStmt)stmt).Expr;
var assertStmt = stmt as AssertStmt;
var expectStmt = stmt as ExpectStmt;
wr.Write(assertStmt != null ? "assert" :
expectStmt != null ? "expect" :
"assume");
if (stmt.Attributes != null) {
PrintAttributes(stmt.Attributes);
}

wr.Write(" ");
if (assertStmt != null && assertStmt.Label != null) {
wr.Write("{0}: ", assertStmt.Label.Name);
}

PrintExpression(expr, true);
if (assertStmt != null && assertStmt.Proof != null) {
wr.Write(" by ");
PrintStatement(assertStmt.Proof, indent);
} else if (expectStmt != null && expectStmt.Message != null) {
wr.Write(", ");
PrintExpression(expectStmt.Message, true);
wr.Write(";");
} else {
wr.Write(";");
}
if (stmt is ICanPrint canPrint) {
canPrint.Render(wr, this, indent);
return;
}

if (stmt is PredicateStmt) {
PrintPredicateStmt(stmt, includeSemicolon);
} else if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
wr.Write("print");
Expand All @@ -88,7 +67,6 @@ public void PrintStatement(Statement stmt, int indent) {
for (int i = 0; i < s.BreakAndContinueCount - 1; i++) {
wr.Write("break ");
}

wr.Write($"{s.Kind};");
}

Expand All @@ -103,7 +81,6 @@ public void PrintStatement(Statement stmt, int indent) {
sep = ", ";
}
}

wr.Write(";");

} else if (stmt is SingleAssignStmt) {
Expand All @@ -122,7 +99,6 @@ public void PrintStatement(Statement stmt, int indent) {
PrintStatement(s, ind);
wr.WriteLine();
}

if (sbs.BodyProper.Count != 0 || sbs.SeparatorTok != null) {
Indent(indent + IndentAmount);
wr.WriteLine("new;");
Expand All @@ -132,7 +108,6 @@ public void PrintStatement(Statement stmt, int indent) {
wr.WriteLine();
}
}

Indent(indent);
wr.Write("}");

Expand All @@ -149,7 +124,6 @@ public void PrintStatement(Statement stmt, int indent) {
if (s.UsesOptionalBraces) {
wr.Write(" {");
}

PrintAlternatives(indent + (s.UsesOptionalBraces ? IndentAmount : 0), s.Alternatives);
if (s.UsesOptionalBraces) {
wr.WriteLine();
Expand All @@ -176,10 +150,8 @@ public void PrintStatement(Statement stmt, int indent) {
} else {
wr.Write(" ");
}

wr.Write("{");
}

Contract.Assert(s.Alternatives.Count != 0);
PrintAlternatives(indent + (s.UsesOptionalBraces ? IndentAmount : 0), s.Alternatives);
if (s.UsesOptionalBraces) {
Expand All @@ -198,7 +170,6 @@ public void PrintStatement(Statement stmt, int indent) {
foreach (var expr in s.EffectiveEnsuresClauses) {
PrintExpression(expr, false, new string(' ', indent + IndentAmount) + "ensures ");
}

if (s.Body != null) {
wr.WriteLine();
Indent(indent);
Expand All @@ -209,7 +180,6 @@ public void PrintStatement(Statement stmt, int indent) {
wr.Write(" ");
PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range);
}

PrintSpec("ensures", s.Ens, indent + IndentAmount);
if (s.Body != null) {
if (s.Ens.Count == 0) {
Expand All @@ -220,7 +190,6 @@ public void PrintStatement(Statement stmt, int indent) {
}
}
}

if (s.Body != null) {
PrintStatement(s.Body, indent);
}
Expand All @@ -231,10 +200,7 @@ public void PrintStatement(Statement stmt, int indent) {

} else if (stmt is CalcStmt) {
CalcStmt s = (CalcStmt)stmt;
if (printMode == PrintModes.NoGhostOrIncludes) {
return;
} // Calcs don't get a "ghost" attribute, but they are.

if (printMode == PrintModes.NoGhostOrIncludes) { return; } // Calcs don't get a "ghost" attribute, but they are.
wr.Write("calc");
PrintAttributes(stmt.Attributes);
wr.Write(" ");
Expand All @@ -245,11 +211,9 @@ public void PrintStatement(Statement stmt, int indent) {
PrintCalcOp(s.Op);
wr.Write(" ");
}

wr.WriteLine("{");
int lineInd = indent + IndentAmount;
int lineCount =
s.Lines.Count == 0 ? 0 : s.Lines.Count - 1; // if nonempty, .Lines always contains a duplicated last line
int lineCount = s.Lines.Count == 0 ? 0 : s.Lines.Count - 1; // if nonempty, .Lines always contains a duplicated last line
// The number of op/hints is commonly one less than the number of lines, but
// it can also equal the number of lines for empty calc's and for calc's with
// a dangling hint.
Expand All @@ -265,22 +229,19 @@ public void PrintStatement(Statement stmt, int indent) {
if (i == hintCount) {
break;
}

// print the operator, if any
if (op != null || (options.DafnyPrintResolvedFile != null && s.Op != null)) {
Indent(indent); // this lines up with the "calc"
PrintCalcOp(op ?? s.Op);
wr.WriteLine();
}

// print the hints
foreach (var st in h.Body) {
Indent(lineInd);
PrintStatement(st, lineInd);
wr.WriteLine();
}
}

Indent(indent);
wr.Write("}");
} else if (stmt is NestedMatchStmt) {
Expand All @@ -290,22 +251,18 @@ public void PrintStatement(Statement stmt, int indent) {
if (s.Flattened != null && options.DafnyPrintResolvedFile != null) {
wr.WriteLine();
if (!printingDesugared) {
Indent(indent);
wr.WriteLine("/*---------- flattened ----------");
Indent(indent); wr.WriteLine("/*---------- flattened ----------");
}

var savedDesugarMode = printingDesugared;
printingDesugared = true;
Indent(indent);
PrintStatement(s.Flattened, indent);
Indent(indent); PrintStatement(s.Flattened, indent);
wr.WriteLine();
printingDesugared = savedDesugarMode;

if (!printingDesugared) {
Indent(indent);
wr.WriteLine("---------- end flattened ----------*/");
Indent(indent); wr.WriteLine("---------- end flattened ----------*/");
}

Indent(indent);
}

Expand All @@ -317,7 +274,6 @@ public void PrintStatement(Statement stmt, int indent) {
if (s.UsesOptionalBraces) {
wr.Write(" {");
}

int caseInd = indent + (s.UsesOptionalBraces ? IndentAmount : 0);
foreach (NestedMatchCaseStmt mc in s.Cases) {
wr.WriteLine();
Expand All @@ -333,7 +289,6 @@ public void PrintStatement(Statement stmt, int indent) {
PrintStatement(bs, caseInd + IndentAmount);
}
}

if (s.UsesOptionalBraces) {
wr.WriteLine();
Indent(indent);
Expand Down Expand Up @@ -375,8 +330,9 @@ public void PrintStatement(Statement stmt, int indent) {
Indent(indent);
wr.Write("}");
}

} else if (stmt is ConcreteAssignStatement concreteAssignStatement) {
PrintConcreteUpdateStatement(concreteAssignStatement, indent);
PrintConcreteUpdateStatement(concreteAssignStatement, indent, includeSemicolon);
} else if (stmt is CallStmt) {
// Most calls are printed from their concrete syntax given in the input. However, recursive calls to
// prefix lemmas end up as CallStmt's by the end of resolution and they may need to be printed here.
Expand All @@ -386,45 +342,39 @@ public void PrintStatement(Statement stmt, int indent) {

} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
if (s.Locals.Exists(v => v.IsGhost) && printMode == PrintModes.NoGhostOrIncludes) {
return;
}

if (s.Locals.Exists(v => v.IsGhost) && printMode == PrintModes.NoGhostOrIncludes) { return; }
if (s.Locals.TrueForAll((v => v.IsGhost))) {
// Emit the "ghost" modifier if all of the variables are ghost. If some are ghost, but not others,
// then some of these ghosts are auto-converted to ghost, so we should not emit the "ghost" keyword.
wr.Write("ghost ");
}

wr.Write("var");
string sep = "";
foreach (var local in s.Locals) {
wr.Write(sep);
if (local.Attributes != null) {
PrintAttributes(local.Attributes);
}

wr.Write(" {0}", local.DisplayName);
PrintType(": ", local.SyntacticType);
sep = ",";
}

if (s.Assign != null) {
wr.Write(" ");
PrintUpdateRHS(s.Assign, indent);
}

PrintBy(s.Assign, indent);
if (includeSemicolon) {
wr.Write(";");
}
} else if (stmt is VarDeclPattern) {
var s = (VarDeclPattern)stmt;
if (s.tok is AutoGeneratedToken) {
wr.Write("/* ");
}

if (s.HasGhostModifier) {
wr.Write("ghost ");
}

wr.Write("var ");
PrintCasePattern(s.LHS);
wr.Write(" := ");
Expand Down Expand Up @@ -473,26 +423,11 @@ public void PrintStatement(Statement stmt, int indent) {
PrintStatement(haltRecoveryStatement.RecoverBody, ind);
wr.Write("[[ } ]]");
} else {
Contract.Assert(false);
throw new cce.UnreachableException(); // unexpected statement
}
}

void PrintBy(ConcreteAssignStatement statement, int indent) {
var proof = statement switch {
AssignStatement updateStmt => updateStmt.Proof,
AssignOrReturnStmt returnStmt => returnStmt.Proof,
_ => null
};
if (proof != null) {
wr.Write(" by ");
PrintStatement(proof, indent);
} else {
wr.Write(";");
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
}

public void PrintConcreteUpdateStatement(ConcreteAssignStatement stmt, int indent) {
public void PrintConcreteUpdateStatement(ConcreteAssignStatement stmt, int indent, bool includeSemicolon = true) {
string sep = "";
foreach (var lhs in stmt.Lhss) {
wr.Write(sep);
Expand All @@ -503,7 +438,9 @@ public void PrintConcreteUpdateStatement(ConcreteAssignStatement stmt, int inden
wr.Write(" ");
}
PrintUpdateRHS(stmt, indent);
PrintBy(stmt, indent);
if (includeSemicolon) {
wr.Write(";");
}
}

public void PrintBlockStmt(BlockStmt stmt, int indent) {
Expand Down Expand Up @@ -773,8 +710,8 @@ void PrintRhs(AssignmentRhs rhs) {
PrintType(t.EType);
}
if (options.DafnyPrintResolvedFile == null &&
t.InitDisplay != null && t.ArrayDimensions.Count == 1 &&
AutoGeneratedToken.Is(t.ArrayDimensions[0].tok)) {
t.InitDisplay != null && t.ArrayDimensions.Count == 1 &&
AutoGeneratedToken.Is(t.ArrayDimensions[0].tok)) {
// elide the size
wr.Write("[]");
} else {
Expand Down
4 changes: 3 additions & 1 deletion Source/DafnyCore/AST/Grammar/Printer/Printer.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1112,7 +1112,9 @@ void PrintFormal(Formal f, bool showNewKeyword) {

internal void PrintDecreasesSpec(Specification<Expression> decs, int indent) {
Contract.Requires(decs != null);
if (printMode == PrintModes.NoGhostOrIncludes) { return; }
if (printMode == PrintModes.NoGhostOrIncludes) {
return;
}
if (decs.Expressions != null && decs.Expressions.Count != 0) {
wr.WriteLine();
Indent(indent);
Expand Down
Loading

0 comments on commit c538717

Please sign in to comment.