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.

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

Optimize compilation of functional-looking assignment RHSs #5589

Merged
Merged
Show file tree
Hide file tree
Changes from 33 commits
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
bab7cf5
Parameterize TrOptExpr in its continuation
RustanLeino Jun 29, 2024
cf34d7e
Use TrExprOpt for simple assignment statements
RustanLeino Jun 29, 2024
93f5ccf
Add release notes
RustanLeino Jun 29, 2024
013f6d2
Add tests
RustanLeino Jul 3, 2024
0e27fa6
fix: Thread inLetExprBody through EmitNestedMatchGeneric
RustanLeino Jul 3, 2024
8c85e32
Use last case unconditionally
RustanLeino Jul 3, 2024
ac36a0c
Remove “unmatched” mechanism
RustanLeino Jul 3, 2024
97ac904
Always emit exception-throw for zero-case match
RustanLeino Jul 3, 2024
0f4d7d9
chore: Improve code
RustanLeino Jul 3, 2024
15afb89
Emit no tests for last case
RustanLeino Jul 3, 2024
df493ff
Introduce OptimizedExpressionContinuation record type
RustanLeino Jul 3, 2024
434e3fb
Prevent case fall-through by using break/goto
RustanLeino Jul 3, 2024
5502bff
fix: Use Downcast for let RHS and for function body
RustanLeino Jul 4, 2024
d89fb6b
Add tests
RustanLeino Jul 4, 2024
e02d322
Handle only non-degenerate matches differently for Java
RustanLeino Jul 4, 2024
ab826e3
fix: Add a missing case in C# type conversions
RustanLeino Jul 4, 2024
fa1bb32
Updated code generated from Dafny
RustanLeino Jul 4, 2024
8e392d9
chore: Code improvements
RustanLeino Jul 8, 2024
69bf890
fix: Revert the added downcast for exprs being returned
RustanLeino Jul 8, 2024
64c7840
Improve and unify code
RustanLeino Jul 8, 2024
64ba677
chore: Improve code
RustanLeino Jul 8, 2024
498ed9c
fix: Always wrap a block around each case
RustanLeino Jul 8, 2024
065b415
fix: Rename override-member type parameters
RustanLeino Jul 9, 2024
7da8a60
refactor: Extract method TrTailCall
RustanLeino Jul 9, 2024
a6a08e0
fix: Pass “inLetExprBody” through
RustanLeino Jul 9, 2024
7742cd8
Add comment to test file
RustanLeino Jul 9, 2024
9b2ca24
Merge branch 'master' into optimize-functional-assignment-rhs
RustanLeino Jul 9, 2024
89d062a
Merge branch 'master' into optimize-functional-assignment-rhs
RustanLeino Jul 9, 2024
f7763ab
Regenerate Dafny code
RustanLeino Jul 9, 2024
12361cc
Merge branch 'master' into optimize-functional-assignment-rhs
RustanLeino Jul 10, 2024
df1adf5
Update ignore file
RustanLeino Jul 10, 2024
6e15f06
Regenerate Dafny
RustanLeino Jul 10, 2024
5b28ba8
Merge branch 'master' into optimize-functional-assignment-rhs
RustanLeino Jul 10, 2024
9b46ec4
chore: Remove dead code leftover from merge
RustanLeino Jul 10, 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
4 changes: 4 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -84,3 +84,7 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/**/*.html
Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.dtr
/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary-lib
/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary.doo
Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.deps.json
Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.csproj
/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule2
/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/PythonModule1
13 changes: 13 additions & 0 deletions Source/DafnyCore/AST/Members/Function.cs
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,19 @@ public TailStatus
public readonly Formal Result;
public PreType ResultPreType;
public readonly Type ResultType;
public Type OriginalResultTypeWithRenamings() {
if (OverriddenFunction == null) {
return ResultType;
}

Contract.Assert(TypeArgs.Count == OverriddenFunction.TypeArgs.Count);
var renamings = new Dictionary<TypeParameter, Type>();
for (var i = 0; i < TypeArgs.Count; i++) {
renamings.Add(OverriddenFunction.TypeArgs[i], new UserDefinedType(tok, TypeArgs[i]));
}
return OverriddenFunction.ResultType.Subst(renamings);

}
public Expression Body; // an extended expression; Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution
public IToken /*?*/ ByMethodTok; // null iff ByMethodBody is null
public BlockStmt /*?*/ ByMethodBody;
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2975,8 +2975,8 @@ protected override void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExp
}

protected override void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts,
bool inLetExprBody, IVariable accumulatorVar) {
TrExprOpt(match.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar);
bool inLetExprBody, IVariable accumulatorVar, OptimizedExpressionContinuation continuation) {
TrExprOpt(match.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar, continuation);
}

protected override void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {
Expand Down
8 changes: 0 additions & 8 deletions Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1985,14 +1985,6 @@ protected override void EmitReturn(List<Formal> outParams, ConcreteSyntaxTree wr
EmitReturnWithCoercions(outParams, null, null, wr);
}

protected override void EmitReturnExpr(Expression expr, Type resultType, bool inLetExprBody, ConcreteSyntaxTree wr) {
var wStmts = wr.Fork();
var w = EmitReturnExpr(wr);
var fromType = thisContext == null ? expr.Type : expr.Type.Subst(thisContext.ParentFormalTypeParametersToActuals);
w = EmitCoercionIfNecessary(fromType, resultType, expr.tok, w);
w.Append(Expr(expr, inLetExprBody, wStmts));
}

protected void EmitReturnWithCoercions(List<Formal> outParams, List<Formal>/*?*/ overriddenOutParams, Dictionary<TypeParameter, Type>/*?*/ typeMap, ConcreteSyntaxTree wr) {
wr.Write("return");
var sep = " ";
Expand Down
24 changes: 20 additions & 4 deletions Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -3606,6 +3606,10 @@ protected override void EmitAbsurd(string message, ConcreteSyntaxTree wr) {
message = "unexpected control point";
}

// Wrapping an "if (true) { ... }" around the "break" statement is a way to tell the Java compiler not to give
// errors for any (unreachable) code that may follow.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

:-P

wr = EmitIf(out var guardWriter, false, wr);
guardWriter.Write("true");
wr.WriteLine($"throw new IllegalArgumentException(\"{message}\");");
}

Expand Down Expand Up @@ -4369,16 +4373,28 @@ protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageV

protected override void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExprBody, ConcreteSyntaxTree output,
ConcreteSyntaxTree wStmts) {
EmitExpr(match.Flattened, inLetExprBody, output, wStmts);
if (match.Cases.Count == 0) {
base.EmitNestedMatchExpr(match, inLetExprBody, output, wStmts);
} else {
EmitExpr(match.Flattened, inLetExprBody, output, wStmts);
}
}

protected override void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts,
bool inLetExprBody, IVariable accumulatorVar) {
TrExprOpt(match.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar);
bool inLetExprBody, IVariable accumulatorVar, OptimizedExpressionContinuation continuation) {
if (match.Cases.Count == 0) {
base.TrOptNestedMatchExpr(match, resultType, wr, wStmts, inLetExprBody, accumulatorVar, continuation);
} else {
TrExprOpt(match.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar, continuation);
}
}

protected override void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {
TrStmt(match.Flattened, writer);
if (match.Cases.Count == 0) {
base.EmitNestedMatchStmt(match, writer);
} else {
TrStmt(match.Flattened, writer);
}
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -704,7 +704,8 @@ private void EmitMatchExpr(MatchExpr e, bool inLetExprBody, ConcreteSyntaxTree w
var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand();
foreach (MatchCaseExpr mc in e.Cases) {
var wCase = MatchCasePrelude(source, sourceType, mc.Ctor, mc.Arguments, i, e.Cases.Count, w);
TrExprOpt(mc.Body, mc.Body.Type, wCase, wStmts, inLetExprBody: true, accumulatorVar: null);
var continuation = new OptimizedExpressionContinuation(EmitReturnExpr, false);
TrExprOpt(mc.Body, mc.Body.Type, wCase, wStmts, inLetExprBody: true, accumulatorVar: null, continuation);
i++;
}
}
Expand All @@ -715,18 +716,19 @@ private void EmitMatchExpr(MatchExpr e, bool inLetExprBody, ConcreteSyntaxTree w

protected virtual void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExprBody, ConcreteSyntaxTree output, ConcreteSyntaxTree wStmts) {
var lambdaBody = EmitAppliedLambda(output, wStmts, match.Tok, match.Type);
TrOptNestedMatchExpr(match, match.Type, lambdaBody, wStmts, inLetExprBody, null);
var continuation = new OptimizedExpressionContinuation(EmitReturnExpr, false);
TrOptNestedMatchExpr(match, match.Type, lambdaBody, wStmts, inLetExprBody, null, continuation);
}

protected virtual void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultType, ConcreteSyntaxTree wr,
ConcreteSyntaxTree wStmts, bool inLetExprBody, IVariable accumulatorVar) {
ConcreteSyntaxTree wStmts, bool inLetExprBody, IVariable accumulatorVar, OptimizedExpressionContinuation continuation) {

wStmts = wr.Fork();

EmitNestedMatchGeneric(match, (caseIndex, caseBody) => {
EmitNestedMatchGeneric(match, continuation.PreventCaseFallThrough, (caseIndex, caseBody) => {
var myCase = match.Cases[caseIndex];
TrExprOpt(myCase.Body, myCase.Body.Type, caseBody, wStmts, inLetExprBody: true, accumulatorVar: null);
}, wr, true);
TrExprOpt(myCase.Body, myCase.Body.Type, caseBody, wStmts, inLetExprBody, accumulatorVar: null, continuation);
}, inLetExprBody, wr);
}

private ConcreteSyntaxTree EmitAppliedLambda(ConcreteSyntaxTree output, ConcreteSyntaxTree wStmts,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -116,13 +116,25 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
if (Options.ForbidNondeterminism) {
Error(ErrorId.c_nondeterminism_forbidden, s.Rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr);
}
} else if (s.Rhs is ExprRhs eRhs && eRhs.Expr.Resolved is FunctionCallExpr fce && IsTailRecursiveByMethodCall(fce)) {
TrTailCallStmt(s.Tok, fce.Function.ByMethodDecl, fce.Receiver, fce.Args, null, wr);
} else {
} else if (s.Rhs is TypeRhs typeRhs) {
var lvalue = CreateLvalue(s.Lhs, wr, wStmts);
wStmts = wr.Fork();
var wRhs = EmitAssignment(lvalue, TypeOfLhs(s.Lhs), TypeOfRhs(s.Rhs), wr, assignStmt.Tok);
TrRhs(s.Rhs, wRhs, wStmts);
var wRhs = EmitAssignment(lvalue, TypeOfLhs(s.Lhs), TypeOfRhs(typeRhs), wr, assignStmt.Tok);
TrRhs(typeRhs, wRhs, wStmts);
} else {
var eRhs = (ExprRhs)s.Rhs;
if (eRhs.Expr.Resolved is FunctionCallExpr fce && IsTailRecursiveByMethodCall(fce)) {
TrTailCallStmt(s.Tok, fce.Function.ByMethodDecl, fce.Receiver, fce.Args, wr);
} else {
var lvalue = CreateLvalue(s.Lhs, wr, wStmts);
var doAssignment = (Expression e, Type resultType, bool inLetExprBody, ConcreteSyntaxTree wrAssignment) => {
var wStmtsBeforeAssignment = wrAssignment.Fork();
var wRhs = EmitAssignment(lvalue, resultType, e.Type, wrAssignment, assignStmt.Tok);
EmitExpr(e, false, wRhs, wStmtsBeforeAssignment);
};
var continuation = new OptimizedExpressionContinuation(doAssignment, true);
TrExprOpt(eRhs.Expr, TypeOfLhs(s.Lhs), wr, wStmts, false, null, continuation);
}
}

break;
Expand Down Expand Up @@ -511,78 +523,91 @@ private void EmitMatchStmt(ConcreteSyntaxTree wr, MatchStmt s) {
}

protected virtual void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {
EmitNestedMatchGeneric(match, (caseIndex, caseBody) => {
EmitNestedMatchGeneric(match, true, (caseIndex, caseBody) => {
TrStmtList(match.Cases[caseIndex].Body, caseBody);
}, writer, false);
}, false, writer);
}

/// <summary>
///
/// match a
/// Given
///
/// match a
/// case X(Y(b),Z(W(c)) => body1
/// case r => body2
///
/// If there are no cases, then emit:
///
/// throw ABSURD;
///
/// var unmatched = true;
/// if (unmatched && a is X) {
/// var x1 = ((X)a).1;
/// if (x1 is Y) {
/// var b = ((Y)x1).1;
/// Else, emit:
///
/// var x2 = ((X)a).2;
/// if (x2 is Z) {
/// var x4 = ((Z)x2).1;
/// if (x4 is W) {
/// var c = ((W)x4).1;
/// body1;
/// BLOCK {
/// { // this defines the scope for any new local variables in the case
/// if (a is X) {
/// var x0 = ((X)a).0;
/// if (x0 is Y) {
/// var b = ((Y)x0).0;
///
/// var x1 = ((X)a).1;
/// if (x1 is Z) {
/// var xz0 = ((Z)x1).0;
/// if (xz0 is W) {
/// var c = ((W)xz0).0;
///
/// body1;
/// break BLOCK;
/// }
/// }
/// }
/// }
/// }
///
/// {
/// var r = a;
/// body2;
/// }
/// }
/// }
/// if (unmatched) {
/// var r = a;
/// body2;
/// }
///
/// </summary>
private void EmitNestedMatchGeneric(INestedMatch match, Action<int, ConcreteSyntaxTree> emitBody,
ConcreteSyntaxTree output, bool bodyExpected) {
private void EmitNestedMatchGeneric(INestedMatch match, bool preventCaseFallThrough, Action<int, ConcreteSyntaxTree> emitBody,
bool inLetExprBody, ConcreteSyntaxTree output) {
if (match.Cases.Count == 0) {
if (bodyExpected) {
// the verifier would have proved we never get here; still, we need some code that will compile
EmitAbsurd(null, output);
}
// the verifier would have proved we never get here; still, we need some code that will compile
EmitAbsurd(null, output);
} else {
string sourceName = ProtectedFreshId("_source");
DeclareLocalVar(sourceName, match.Source.Type, match.Source.tok, match.Source, false, output);
DeclareLocalVar(sourceName, match.Source.Type, match.Source.tok, match.Source, inLetExprBody, output);

string unmatched = ProtectedFreshId("unmatched");
DeclareLocalVar(unmatched, Type.Bool, match.Source.Tok, Expression.CreateBoolLiteral(match.Source.Tok, true), false, output);
var label = preventCaseFallThrough ? ProtectedFreshId("match") : null;
if (label != null) {
output = CreateLabeledCode(label, false, output);
}

var sourceType = match.Source.Type.NormalizeExpand();
for (var index = 0; index < match.Cases.Count; index++) {
var myCase = match.Cases[index];
var lastCase = index == match.Cases.Count - 1;
var result = EmitIf(out var guardWriter, false, output);
guardWriter.Write(unmatched);
var innerWriter = EmitNestedMatchCaseConditions(sourceName, sourceType, myCase.Pat, result, lastCase);

var caseBlock = EmitBlock(output);
var innerWriter = EmitNestedMatchCaseConditions(sourceName, sourceType, myCase.Pat, caseBlock, lastCase);
Coverage.Instrument(myCase.Tok, "case body", innerWriter);
EmitAssignment(unmatched, Type.Bool, False, Type.Bool, innerWriter);

emitBody(index, innerWriter);
}

if (bodyExpected) {
EmitAbsurd(null, output);
if (label != null && !lastCase) {
EmitBreak(label, innerWriter);
}
}
}
}

private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName,
Type sourceType,
private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName, Type sourceType,
ExtendedPattern pattern, ConcreteSyntaxTree writer, bool lastCase) {

var litExpression = MatchFlattener.GetLiteralExpressionFromPattern(pattern);
if (litExpression != null) {
if (lastCase) {
return writer;
}

var thenWriter = EmitIf(out var guardWriter, false, writer);
CompileBinOp(BinaryExpr.ResolvedOpcode.EqCommon, sourceType, litExpression.Type, pattern.Tok, Type.Bool,
out var opString, out var preOpString, out var postOpString, out var callString, out var staticCallString,
Expand All @@ -591,22 +616,25 @@ private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName,
var right = new ConcreteSyntaxTree();
EmitExpr(litExpression, false, right, writer);
EmitBinaryExprUsingConcreteSyntax(guardWriter, Type.Bool, preOpString, opString, new LineSegment(sourceName), right, callString, staticCallString, postOpString);
writer = thenWriter;
return thenWriter;

} else if (pattern is IdPattern idPattern) {
if (idPattern.BoundVar != null) {
var boundVar = idPattern.BoundVar;
if (boundVar.Tok.val.StartsWith(IdPattern.WildcardString)) {
return writer;
}
if (idPattern.BoundVar == null) {
return EmitNestedMatchStmtCaseConstructor(sourceName, sourceType, idPattern, writer, lastCase);
}

var boundVar = idPattern.BoundVar;
if (!boundVar.Tok.val.StartsWith(IdPattern.WildcardString)) {
var valueWriter = DeclareLocalVar(IdName(boundVar), boundVar.Type, idPattern.Tok, writer);
valueWriter.Write(sourceName);
return writer;
} else {
writer = EmitNestedMatchStmtCaseConstructor(sourceName, sourceType, idPattern, writer, lastCase);
}
return writer;

} else if (pattern is DisjunctivePattern disjunctivePattern) {
if (lastCase) {
return writer;
}

string disjunctiveMatch = ProtectedFreshId("disjunctiveMatch");
DeclareLocalVar(disjunctiveMatch, Type.Bool, disjunctivePattern.Tok, Expression.CreateBoolLiteral(disjunctivePattern.Tok, false), false, writer);
foreach (var alternative in disjunctivePattern.Alternatives) {
Expand All @@ -615,11 +643,11 @@ private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName,
}
writer = EmitIf(out var guardWriter, false, writer);
guardWriter.Write(disjunctiveMatch);
return writer;

} else {
throw new Exception();
}

return writer;
}

private ConcreteSyntaxTree EmitNestedMatchStmtCaseConstructor(string sourceName, Type sourceType,
Expand Down
Loading