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

Use refresh resolver by default #5653

Draft
wants to merge 159 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
159 commits
Select commit Hold shift + click to select a range
51e033a
Change default settings
RustanLeino May 28, 2024
5204eeb
Explicitly declare trait to be a reference type
RustanLeino May 28, 2024
3bdaa87
Make the new type system the default
keyboardDrummer Jun 27, 2024
48a8cf4
Merge branch 'master' into refresh-by-default
RustanLeino Jun 27, 2024
3101604
Explicitly declare trait as reference type
RustanLeino Jun 27, 2024
a134465
Changed from full to datatype
keyboardDrummer Jun 28, 2024
d75f39f
Add “extends object” where it was assumed to be so before
RustanLeino Jun 28, 2024
46484e6
Fix error location for desugared elephant assert
RustanLeino Jun 28, 2024
74a49df
Merge branch 'refresh-by-default' into typeSystemRefreshDefault
RustanLeino Jun 28, 2024
af730de
Merge branch 'master' into refresh-by-default
RustanLeino Jul 17, 2024
5acc14b
Use explicit legacy switches in testDafnyForEach…
RustanLeino Jul 18, 2024
611ac55
Fix missing box adjustment in verifier
RustanLeino Jul 18, 2024
4979a6e
fix: Use just one pre-type proxy for element type in array allocation
RustanLeino Jul 18, 2024
d701a33
Merge branch 'master' into refresh-by-default
RustanLeino Jul 30, 2024
7a5d171
Fix pre-type of StaticReceiverExpr
RustanLeino Aug 18, 2024
a4bf314
Update tests to support new defaults
RustanLeino Aug 20, 2024
18addcf
Involve compatible-type constraints in decision process
RustanLeino Aug 20, 2024
47d4abc
Update test
RustanLeino Aug 20, 2024
43a6a37
Extract method SansPrintablePreType
RustanLeino Aug 20, 2024
a6820e1
Fix type inference of seq/map/multiset update expressions
RustanLeino Aug 20, 2024
99fbb08
Merge branch 'master' into refresh-by-default
RustanLeino Aug 21, 2024
5026519
Fix asserted-expression output for frames
RustanLeino Aug 21, 2024
dab7870
Fix creation of yield-identifier expression
RustanLeino Aug 21, 2024
8028152
Update expect files
RustanLeino Aug 21, 2024
86e2312
Fix pre-type resolution of export-provided members/types
RustanLeino Aug 21, 2024
bb2d519
Improve formatting
RustanLeino Aug 21, 2024
d2624ee
Adjust tests and expected test output
RustanLeino Aug 21, 2024
456afc5
Fix parameter order
RustanLeino Aug 21, 2024
954dd42
Adjust tests and expected test output
RustanLeino Aug 22, 2024
3d617aa
Fix Boogie type of receiver in function-valued members
RustanLeino Aug 22, 2024
fbec421
chore: Improve code
RustanLeino Aug 22, 2024
6ec3676
Add tests
RustanLeino Aug 22, 2024
68ce112
fix: Pass in original (overridden) member
RustanLeino Aug 22, 2024
2d45cf6
Pass CLI parameter values explicitly
RustanLeino Aug 22, 2024
867a207
Prescribe type-refinement flows for SeqUpdateExpr
RustanLeino Aug 22, 2024
289a996
Add some temporary casts, waiting for flows to do more with bounded p…
RustanLeino Aug 22, 2024
785e4cc
Update tests and results
RustanLeino Aug 22, 2024
a442d33
Update tests and expected results
RustanLeino Aug 22, 2024
bddc2ce
Update tests and expected test output
RustanLeino Aug 22, 2024
cec4940
fix: Fix a printing crash
RustanLeino Aug 22, 2024
272bfe4
Update tests and expected output
RustanLeino Aug 23, 2024
35f4877
Update tests
RustanLeino Aug 23, 2024
a6bebff
Use basename for filename in %translate test
RustanLeino Aug 23, 2024
c44b7f8
Update test output
RustanLeino Aug 23, 2024
044d6e6
fix: Report error (and don’t crash) on disjunctive patterns inside ot…
RustanLeino Aug 23, 2024
f35922c
Expect errors for missing parentheses of non-nullary constructors in …
RustanLeino Aug 23, 2024
af98137
Move {:only} warnings from pass 0 to pass 3
RustanLeino Aug 23, 2024
8eadfea
Adjust tests and answers
RustanLeino Aug 23, 2024
2beb41f
Use nested comparable-types constraints as default advice
RustanLeino Aug 23, 2024
f9ca74e
fix: Subrange check and conversions to arrow types
RustanLeino Aug 24, 2024
be77ce8
Handle “as” for datatypes and arrows in compilers and verifier
RustanLeino Aug 24, 2024
8dcd806
Adjust tests
RustanLeino Aug 24, 2024
50c4987
Adjust tests and answers
RustanLeino Aug 24, 2024
d46da94
Adjust tests and outputs
RustanLeino Aug 24, 2024
138b341
Adjust tests and outputs
RustanLeino Aug 24, 2024
a73d698
fix: Support “assigned” in new resolver
RustanLeino Aug 24, 2024
bfb9100
Fill in missing case in type cloning
RustanLeino Aug 27, 2024
5cb67b9
fix: Print DecreasesToExpr with parentheses
RustanLeino Aug 28, 2024
2c3db7b
Don’t update RangeToken when resolving ParensExpression
RustanLeino Aug 28, 2024
b0739ec
Use sub/equal constraints to make type decisions
RustanLeino Aug 28, 2024
32a995a
Update improved (reduced) error messages
RustanLeino Aug 28, 2024
04be175
Update test and answers
RustanLeino Aug 28, 2024
c940168
Merge branch 'master' into refresh-by-default
RustanLeino Aug 28, 2024
e29ded6
Validate resolution CLI options (at a terrible place in the code)
RustanLeino Sep 3, 2024
16a91fe
Merge branch 'master' into refresh-by-default
RustanLeino Sep 3, 2024
5a7f699
Correct previous compensation
RustanLeino Sep 3, 2024
6bc0bab
Merge branch 'master' into refresh-by-default
RustanLeino Sep 4, 2024
8d83506
Fix test script for git-issue-321
RustanLeino Sep 4, 2024
110ff22
fix: Include case for BVNot
RustanLeino Sep 4, 2024
ba1b866
Adjust test outputs
RustanLeino Sep 4, 2024
e691271
Merge branch 'master' into refresh-by-default
RustanLeino Sep 5, 2024
4ba909c
Adjust tests
RustanLeino Sep 26, 2024
3dbd746
Adjust tests
RustanLeino Sep 26, 2024
737c57c
Start adjusting test
RustanLeino Sep 27, 2024
3b54b7e
Merge branch 'master' into refresh-by-default
RustanLeino Sep 27, 2024
27faf49
Merge branch 'master' into refresh-by-default
RustanLeino Oct 4, 2024
feeaa06
Adjust tests and answers
RustanLeino Oct 4, 2024
6652b68
Adjust tests and answers
RustanLeino Oct 5, 2024
006c8af
chore: Improve C#
RustanLeino Oct 5, 2024
ad77757
fix: Incorporate explicit type arguments for function calls and datat…
RustanLeino Oct 5, 2024
1a6ea55
Merge branch 'master' into refresh-by-default
RustanLeino Oct 7, 2024
a79a23e
Adjust tests
RustanLeino Oct 8, 2024
7466e28
Add “extends object” to tests
RustanLeino Oct 8, 2024
68d8dda
Merge branch 'master' into refresh-by-default
RustanLeino Oct 31, 2024
d048c19
Fix parameter resolution
RustanLeino Oct 31, 2024
29353b8
Merge branch 'master' into refresh-by-default
RustanLeino Nov 1, 2024
5e1d3c7
Improve code
RustanLeino Nov 1, 2024
8d69f48
Merge branch 'master' into refresh-by-default
RustanLeino Nov 1, 2024
3b1eb8f
Remove deprecated semi-colons
RustanLeino Nov 1, 2024
b4dc9a4
Update tests
RustanLeino Nov 2, 2024
d90e117
chore: Clean up code
RustanLeino Nov 2, 2024
2c0142d
Fix case where all candidate ctors are ghost
RustanLeino Nov 2, 2024
31af1c2
Fix output
RustanLeino Nov 2, 2024
dcc4ce1
Set .PreType even when DatatypeValue is in error
RustanLeino Nov 2, 2024
717288f
chore: Clean up code and comment
RustanLeino Nov 2, 2024
7b2f342
Forget duplicate destructor names
RustanLeino Nov 2, 2024
d9a5fbe
Merge branch 'master' into refresh-by-default
RustanLeino Nov 11, 2024
a4194d1
fix: Fix issue 2019 for new resolver
RustanLeino Nov 11, 2024
9c56002
Adjust test output
RustanLeino Nov 11, 2024
46721b7
Adjust tests and outputs
RustanLeino Nov 11, 2024
64bb5ac
Fix crash from illegal literal expression in case pattern
RustanLeino Nov 12, 2024
94cff6a
Update test to new type-conversion rules
RustanLeino Nov 12, 2024
c507770
Fix sed issue for the last last time!!
RustanLeino Nov 12, 2024
d56fe91
Improve test and error messages
RustanLeino Nov 12, 2024
2606e87
Adjust tests
RustanLeino Nov 12, 2024
8c6ef14
Clarify tests and don’t insist on having type for _
RustanLeino Nov 12, 2024
bd090f2
Update test answers
RustanLeino Nov 12, 2024
c04d7ee
Fix tests
RustanLeino Nov 12, 2024
ac82f59
Fix type checking of real division
RustanLeino Nov 12, 2024
7c90391
Fix type inference for string literals
RustanLeino Nov 12, 2024
62b36c2
chore: Improve code
RustanLeino Nov 12, 2024
c9b37e7
Make error message more consistent
RustanLeino Nov 12, 2024
d030c34
Fix type constraint checking on string literals
RustanLeino Nov 12, 2024
2f133bd
Improve error messages
RustanLeino Nov 13, 2024
7f74680
Improve error message
RustanLeino Nov 13, 2024
5cf5c0c
Merge branch 'master' into refresh-by-default
RustanLeino Nov 13, 2024
8fc1f58
Fix DatatypeValue type parameter, and fix tests
RustanLeino Nov 13, 2024
59a0849
Merge branch 'master' into refresh-by-default
RustanLeino Nov 13, 2024
18232fe
Remove variance parameter from PreType-to-Type process
RustanLeino Nov 15, 2024
1126c91
Update tests
RustanLeino Nov 15, 2024
f1f54ac
Merge branch 'master' into refresh-by-default
RustanLeino Nov 15, 2024
4aa3559
Merge branch 'master' into refresh-by-default
RustanLeino Dec 10, 2024
4d0aaeb
Adjust tests with improved type inference
RustanLeino Dec 14, 2024
8ab207d
Adjust tests with improved type inference
RustanLeino Dec 14, 2024
1f69ce8
Improve error message
RustanLeino Dec 17, 2024
c39c02e
Use old resolver for tests that need more work
RustanLeino Dec 17, 2024
ca3b1da
Say ‘string’ instead of ‘seq<char>’ for string literals
RustanLeino Dec 17, 2024
6efb5cd
Merge branch 'master' into refresh-by-default
RustanLeino Dec 18, 2024
f17aba5
Revert some tests back to explicitly using old resolver (for now)
RustanLeino Dec 19, 2024
5cc235e
Update AsIs expected output
RustanLeino Dec 23, 2024
8efb254
Add test case for Issue 2040, which has been fixed
RustanLeino Jan 2, 2025
6f59e17
Merge branch 'master' into refresh-by-default
RustanLeino Jan 2, 2025
0137d3d
Fix merge
RustanLeino Jan 2, 2025
14e69f6
Fix and add tests and adjust expected test output
RustanLeino Jan 3, 2025
b06cae7
Merge branch 'master' into refresh-by-default
RustanLeino Jan 4, 2025
9e72c35
Fix up tests and expected output
RustanLeino Jan 4, 2025
b03dbbd
Fix up tests and expected output
RustanLeino Jan 4, 2025
ade18b7
Merge branch 'master' into refresh-by-default
RustanLeino Jan 13, 2025
044fcb0
Update tests
RustanLeino Jan 13, 2025
78885b0
chore: Improve code formatting
RustanLeino Jan 14, 2025
1b7407d
chore: Simplify code (remove premature optimizations)
RustanLeino Jan 14, 2025
e51d4fe
fix: Apply function-call substitution in frame override check
RustanLeino Jan 14, 2025
b047c44
fix: Use correct type of “this” in allowance disjunct
RustanLeino Jan 14, 2025
5ba3a0b
Updated expected output
RustanLeino Jan 14, 2025
bf070b0
Cop-out: Mark failing test as legacy-resolver-only
RustanLeino Jan 14, 2025
e72c868
Merge branch 'master' into refresh-by-default
RustanLeino Jan 14, 2025
f6519a0
Cop-out: Mark failing test as legacy-resolver-only
RustanLeino Jan 14, 2025
71e78d4
Adjust tests
RustanLeino Jan 14, 2025
7acb9bd
Update HowToFAQ ID’s and expected output
RustanLeino Jan 14, 2025
3a2ad0e
Merge branch 'master' into refresh-by-default
RustanLeino Jan 14, 2025
7558275
Update HowToFAQ template
RustanLeino Jan 15, 2025
f0bf4f1
Merge branch 'master' into refresh-by-default
RustanLeino Jan 15, 2025
4e26996
Update some HowToFAQ resolver errors and punted on others
RustanLeino Jan 16, 2025
62c0a59
Fix test expectations
RustanLeino Jan 16, 2025
ec26b80
Add “extends object”
RustanLeino Jan 16, 2025
9d2aa89
Revert Rust tests to using old resolver
RustanLeino Jan 16, 2025
01ddf38
Fix Rust tests via lit on osx
RustanLeino Jan 16, 2025
322da9a
Revert Rust tests to use legacy traits
RustanLeino Jan 16, 2025
66767c6
Revert "Fix Rust tests via lit on osx"
RustanLeino Jan 16, 2025
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
Prev Previous commit
Next Next commit
chore: Simplify code (remove premature optimizations)
RustanLeino committed Jan 14, 2025

Verified

This commit was signed with the committer’s verified signature. The key has expired.
jasonb5 Jason Boutte
commit 1b7407d377f17e50e51bb55245cfde48b6b5e862
51 changes: 21 additions & 30 deletions Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
Original file line number Diff line number Diff line change
@@ -1139,20 +1139,18 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder
}

// conjunction of class post-conditions
var allOverrideEns = f.Ens.Count == 0 ? null : f.Ens
var allOverrideEns = f.Ens
.Select(e => e.E)
.Aggregate((e0, e1) => new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, e0, e1));
.Aggregate((Expression)Expression.CreateBoolLiteral(f.Origin, true), (e0, e1) => Expression.CreateAnd(e0, e1));
//generating trait post-conditions with class variables
cco = new CanCallOptions(true, f, true);
FunctionCallSubstituter sub = null;
FunctionCallSubstituter sub = new FunctionCallSubstituter(substMap, typeMap,
(TraitDecl)f.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)f.EnclosingClass);
foreach (var en in ConjunctsOf(f.OverriddenFunction.Ens)) {
sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)f.EnclosingClass);
var subEn = sub.Substitute(en.E);
foreach (var s in TrSplitExpr(new BodyTranslationContext(false), subEn, etran, false, out _).Where(s => s.IsChecked)) {
builder.Add(TrAssumeCmd(f.Origin, etran.CanCallAssumption(subEn, cco)));
var constraint = allOverrideEns == null
? null
: new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp, allOverrideEns, subEn);
var constraint = Expression.CreateImplies(allOverrideEns, subEn);
builder.Add(Assert(f.Origin, s.E, new FunctionContractOverride(true, constraint), builder.Context));
}
}
@@ -1188,9 +1186,9 @@ private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder b
Dictionary<IVariable, Expression> substMap, Dictionary<TypeParameter, Type> typeMap) {
//getting framePrime
List<FrameExpression> traitFrameExps = new List<FrameExpression>();
FunctionCallSubstituter sub = null;
FunctionCallSubstituter sub = new FunctionCallSubstituter(substMap, typeMap,
(TraitDecl)func.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)func.EnclosingClass);
foreach (var e in func.OverriddenFunction.Reads.Expressions) {
sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)func.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)func.EnclosingClass);
var newE = sub.Substitute(e.E);
FrameExpression fe = new FrameExpression(e.Origin, newE, e.FieldName);
traitFrameExps.Add(fe);
@@ -1234,25 +1232,23 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde
Contract.Requires(substMap != null);
//generating trait pre-conditions with class variables
var cco = new CanCallOptions(true, f, true);
FunctionCallSubstituter sub = null;
FunctionCallSubstituter sub = new FunctionCallSubstituter(substMap, typeMap,
(TraitDecl)f.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)f.EnclosingClass);
var subReqs = new List<Expression>();
foreach (var req in ConjunctsOf(f.OverriddenFunction.Req)) {
sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)f.EnclosingClass);
var subReq = sub.Substitute(req.E);
builder.Add(TrAssumeCmd(f.Origin, etran.CanCallAssumption(subReq, cco)));
builder.Add(TrAssumeCmdWithDependencies(etran, f.Origin, subReq, "overridden function requires clause"));
subReqs.Add(subReq);
}
var allTraitReqs = subReqs.Count == 0 ? null : subReqs
.Aggregate((e0, e1) => new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, e0, e1));

var allTraitReqs = subReqs.Aggregate((Expression)Expression.CreateBoolLiteral(f.Origin, true), (e0, e1) => Expression.CreateAnd(e0, e1));
//generating class pre-conditions
cco = new CanCallOptions(true, f);
foreach (var req in ConjunctsOf(f.Req)) {
foreach (var s in TrSplitExpr(new BodyTranslationContext(false), req.E, etran, false, out _).Where(s => s.IsChecked)) {
builder.Add(TrAssumeCmd(f.Origin, etran.CanCallAssumption(req.E, cco)));
var constraint = allTraitReqs == null
? null
: new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp, allTraitReqs, req.E);
var constraint = Expression.CreateImplies(allTraitReqs, req.E);
builder.Add(Assert(f.Origin, s.E, new FunctionContractOverride(false, constraint), builder.Context));
}
}
@@ -1504,19 +1500,17 @@ private void AddMethodOverrideEnsChk(Method m, BoogieStmtListBuilder builder, Ex
builder.Add(TrAssumeCmdWithDependencies(etran, m.Origin, en.E, "overridden ensures clause"));
}
// conjunction of class post-conditions
var allOverrideEns = m.Ens.Count == 0 ? null : m.Ens
var allOverrideEns = m.Ens
.Select(e => e.E)
.Aggregate((e0, e1) => new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, e0, e1));
.Aggregate((Expression)Expression.CreateBoolLiteral(m.Origin, true), (e0, e1) => Expression.CreateAnd(e0, e1));
//generating trait post-conditions with class variables
FunctionCallSubstituter sub = null;
FunctionCallSubstituter sub = new FunctionCallSubstituter(substMap, typeMap,
(TraitDecl)m.OverriddenMethod.EnclosingClass, (TopLevelDeclWithMembers)m.EnclosingClass);
foreach (var en in ConjunctsOf(m.OverriddenMethod.Ens)) {
sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (TopLevelDeclWithMembers)m.EnclosingClass);
var subEn = sub.Substitute(en.E);
foreach (var s in TrSplitExpr(new BodyTranslationContext(false), subEn, etran, false, out _).Where(s => s.IsChecked)) {
builder.Add(TrAssumeCmd(m.OverriddenMethod.Origin, etran.CanCallAssumption(subEn)));
var constraint = allOverrideEns == null
? null
: new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp, allOverrideEns, subEn);
var constraint = Expression.CreateImplies(allOverrideEns, subEn);
builder.Add(Assert(m.Origin, s.E, new EnsuresStronger(constraint), builder.Context));
}
}
@@ -1530,25 +1524,22 @@ private void AddMethodOverrideReqsChk(Method m, BoogieStmtListBuilder builder, E
Contract.Requires(etran != null);
Contract.Requires(substMap != null);
//generating trait pre-conditions with class variables
FunctionCallSubstituter sub = null;
FunctionCallSubstituter sub = new FunctionCallSubstituter(substMap, typeMap,
(TraitDecl)m.OverriddenMethod.EnclosingClass, (TopLevelDeclWithMembers)m.EnclosingClass);
var subReqs = new List<Expression>();
foreach (var req in ConjunctsOf(m.OverriddenMethod.Req)) {
sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (TopLevelDeclWithMembers)m.EnclosingClass);
var subReq = sub.Substitute(req.E);
builder.Add(TrAssumeCmd(m.OverriddenMethod.Origin, etran.CanCallAssumption(subReq)));
builder.Add(TrAssumeCmdWithDependencies(etran, m.Origin, subReq, "overridden requires clause"));
subReqs.Add(subReq);
}
var allTraitReqs = subReqs.Count == 0 ? null : subReqs
.Aggregate((e0, e1) => new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, e0, e1));
var allTraitReqs = subReqs.Aggregate((Expression)Expression.CreateBoolLiteral(m.Origin, true), (e0, e1) => Expression.CreateAnd(e0, e1));

// generating class pre-conditions
foreach (var req in ConjunctsOf(m.Req)) {
foreach (var s in TrSplitExpr(new BodyTranslationContext(false), req.E, etran, false, out _).Where(s => s.IsChecked)) {
builder.Add(TrAssumeCmd(m.Origin, etran.CanCallAssumption(req.E)));
var constraint = allTraitReqs == null
? null
: new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp, allTraitReqs, req.E);
var constraint = Expression.CreateImplies(allTraitReqs, req.E);
builder.Add(Assert(m.Origin, s.E, new RequiresWeaker(constraint), builder.Context));
}
}