Skip to content

When splitting assertions, delete implicit assertions that would otherwise be converted to assumes #5721

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.

Sign up for GitHub

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

Open
keyboardDrummer wants to merge 3 commits into
base: master
Choose a base branch
from
Open

When splitting assertions, delete implicit assertions that would otherwise be converted to assumes #5721

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7b17d81
Use custom Boogie
keyboardDrummer Aug 26, 2024
d7501de
Make remember false the default for generated assertions
keyboardDrummer Aug 26, 2024
64ed59b
Added Boogie as a submodule
keyboardDrummer Aug 26, 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
3 changes: 3 additions & 0 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
[submodule "Test/libraries"]
path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries
url = https://github.com/dafny-lang/libraries.git
[submodule "boogie"]
path = boogie
url = https://github.com/keyboardDrummer/boogie
38 changes: 38 additions & 0 deletions Source/Dafny.sln
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
EndProject
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}"
EndProject
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Expand Down Expand Up @@ -138,5 +164,17 @@ Global
SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187}
EndGlobalSection
GlobalSection(NestedProjects) = preSolution
{68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90}
{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90}
{09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90}
{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90}
{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90}
{0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90}
{05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90}
{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90}
{D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90}
{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90}
{E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90}
{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90}
EndGlobalSection
EndGlobal
12 changes: 11 additions & 1 deletion Source/DafnyCore/DafnyCore.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,17 @@
<PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
<PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
<PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
<PackageReference Include="Boogie.ExecutionEngine" Version="3.2.4" />
<ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
<ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
<ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />
<ProjectReference Include="..\..\boogie\Source\Graph\Graph.csproj" />
<ProjectReference Include="..\..\boogie\Source\Model\Model.csproj" />
<ProjectReference Include="..\..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj" />
<ProjectReference Include="..\..\boogie\Source\VCExpr\VCExpr.csproj" />
<ProjectReference Include="..\..\boogie\Source\VCGeneration\VCGeneration.csproj" />
<ProjectReference Include="..\..\boogie\Source\Provers\SMTLib\SMTLib.csproj" />
<ProjectReference Include="..\..\boogie\Source\Houdini\Houdini.csproj" />
<ProjectReference Include="..\..\boogie\Source\Concurrency\Concurrency.csproj" />
<PackageReference Include="Tomlyn" Version="0.16.2" />
</ItemGroup>

Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Verifier/BoogieGenerator.TrPredicateStatement.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,14 +166,14 @@ private bool TrAssertCondition(PredicateStmt stmt, BoogieStmtListBuilder builder
var tok = enclosingToken == null ? GetToken(stmt.Expr) : new NestedToken(enclosingToken, GetToken(stmt.Expr));
var desc = new PODesc.AssertStatementDescription(stmt, errorMessage, successMessage);
proofBuilder.Add(Assert(tok, etran.TrExpr(stmt.Expr), desc, stmt.Tok,
etran.TrAttributes(stmt.Attributes, null)));
etran.TrAttributes(stmt.Attributes, null), remember: true));
} else {
foreach (var split in splits) {
if (split.IsChecked) {
var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.Tok);
var desc = new PODesc.AssertStatementDescription(stmt, errorMessage, successMessage);
proofBuilder.Add(AssertNS(ToDafnyToken(flags.ReportRanges, tok), split.E, desc, stmt.Tok,
etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split
etran.TrAttributes(stmt.Attributes, null), remember: true)); // attributes go on every split
}
}
}
Expand Down
27 changes: 17 additions & 10 deletions Source/DafnyCore/Verifier/BoogieGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3388,12 +3388,14 @@ public override IToken WithVal(string newVal) {
}
}

Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription description, Bpl.QKeyValue kv = null) {
var cmd = Assert(tok, condition, description, tok, kv);
Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription description,
Bpl.QKeyValue kv = null, bool remember = false) {
var cmd = Assert(tok, condition, description, tok, kv, remember);
return cmd;
}

Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription description, IToken refinesToken, Bpl.QKeyValue kv = null) {
PredicateCmd Assert(IToken tok, Expr condition, PODesc.ProofObligationDescription description, IToken refinesToken,
QKeyValue kv = null, bool remember = false) {
Contract.Requires(tok != null);
Contract.Requires(condition != null);
Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
Expand All @@ -3406,7 +3408,9 @@ Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDe
cmd = TrAssumeCmd(tok, condition, kv);
proofDependencies?.AddProofDependencyId(cmd, tok, new AssumedProofObligationDependency(tok, description));
} else {
cmd = TrAssertCmdDesc(ForceCheckToken.Unwrap(tok), condition, description, kv);
var assertCmd = TrAssertCmdDesc(ForceCheckToken.Unwrap(tok), condition, description, kv);
assertCmd.Remember = remember;
cmd = assertCmd;
proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description));
}
return cmd;
Expand All @@ -3416,7 +3420,8 @@ Bpl.PredicateCmd AssertNS(IToken tok, Bpl.Expr condition, PODesc.ProofObligation
return AssertNS(tok, condition, desc, tok, null);
}

Bpl.PredicateCmd AssertNS(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription desc, IToken refinesTok, Bpl.QKeyValue kv) {
Bpl.PredicateCmd AssertNS(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription desc, IToken refinesTok,
Bpl.QKeyValue kv, bool remember = false) {
Contract.Requires(tok != null);
Contract.Requires(desc != null);
Contract.Requires(condition != null);
Expand All @@ -3429,9 +3434,8 @@ Bpl.PredicateCmd AssertNS(IToken tok, Bpl.Expr condition, PODesc.ProofObligation
cmd = TrAssumeCmd(tok, Bpl.Expr.True, kv);
} else {
tok = ForceCheckToken.Unwrap(tok);
var args = new List<object>();
args.Add(Bpl.Expr.Literal(0));
cmd = TrAssertCmdDesc(tok, condition, desc, new Bpl.QKeyValue(tok, "subsumption", args, kv));
var args = new List<object> { Bpl.Expr.Literal(0) };
cmd = TrAssertCmdDesc(tok, condition, desc, new Bpl.QKeyValue(tok, "subsumption", args, kv), remember);
proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, desc));
}

Expand Down Expand Up @@ -3552,9 +3556,12 @@ Bpl.AssertCmd TrAssertCmd(IToken tok, Bpl.Expr expr, Bpl.QKeyValue attributes =
return attributes == null ? new Bpl.AssertCmd(tok, expr) : new Bpl.AssertCmd(tok, expr, attributes);
}

Bpl.AssertCmd TrAssertCmdDesc(IToken tok, Bpl.Expr expr, PODesc.ProofObligationDescription description, Bpl.QKeyValue attributes = null) {
Bpl.AssertCmd TrAssertCmdDesc(IToken tok, Bpl.Expr expr, PODesc.ProofObligationDescription description,
Bpl.QKeyValue attributes = null, bool remember = false) {
ReportAssertion(tok, description);
return new Bpl.AssertCmd(tok, expr, description, attributes);
return new Bpl.AssertCmd(tok, expr, description, attributes) {
Remember = remember
};
}

private ISet<(Uri, int)> reportedAssertions = new HashSet<(Uri, int)>();
Expand Down
6 changes: 3 additions & 3 deletions Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ module Std.Unicode.Utf16EncodingForm refines UnicodeEncodingForm {
}

function
{:resource_limit 1200000}
{:isolate_assertions}
DecodeMinimalWellFormedCodeUnitSubsequenceDoubleWord(m: MinimalWellFormedCodeUnitSeq): (v: ScalarValue)
requires |m| == 2
ensures 0x10000 <= v <= 0x10FFFF
Expand All @@ -128,8 +128,8 @@ module Std.Unicode.Utf16EncodingForm refines UnicodeEncodingForm {
var w := ((firstWord & 0x3C0) >> 6) as bv24;
var u := (w + 1) as bv24;
var v := (u << 16) | (x1 << 10) | x2 as ScalarValue;
assert {:split_here} true;
assert EncodeScalarValueDoubleWord(v) == m;
assert EncodeScalarValueDoubleWord(v)[0] == m[0];
assert EncodeScalarValueDoubleWord(v)[1] == m[1];
v
}
}
1 change: 1 addition & 0 deletions boogie
Open in desktop
Submodule boogie added at 49f48c