diff --git a/.gitmodules b/.gitmodules index aa94f844181..52e984eddac 100644 --- a/.gitmodules +++ b/.gitmodules @@ -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 diff --git a/Source/Dafny.sln b/Source/Dafny.sln index 23297b185ed..fc8e8b1fa49 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln @@ -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 @@ -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 diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 5899a78c19a..c15a3145ea3 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,17 @@ - + + + + + + + + + + + diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrPredicateStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrPredicateStatement.cs index 06e112b3c09..28789380284 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrPredicateStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrPredicateStatement.cs @@ -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 } } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 6a4da1fa878..0b7c0e1902f 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -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() != null); @@ -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; @@ -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); @@ -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(); - args.Add(Bpl.Expr.Literal(0)); - cmd = TrAssertCmdDesc(tok, condition, desc, new Bpl.QKeyValue(tok, "subsumption", args, kv)); + var args = new List { 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)); } @@ -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)>(); diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy index e8679c68069..41701e9df6c 100644 --- a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy @@ -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 @@ -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 } } diff --git a/boogie b/boogie new file mode 160000 index 00000000000..49f48cf2e22 --- /dev/null +++ b/boogie @@ -0,0 +1 @@ +Subproject commit 49f48cf2e22a570f194e1cfa99a71180d88d98f4