diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs index 49ee3003c..43f0a7922 100644 --- a/Source/Concurrency/CivlUtil.cs +++ b/Source/Concurrency/CivlUtil.cs @@ -133,7 +133,6 @@ public static int ResolveAndTypecheck(CoreOptions options, Absy absy, Resolution } var tc = new TypecheckingContext(null, options); - tc.CheckModifies = false; // to prevent access to tc.Proc which is null absy.Typecheck(tc); return tc.ErrorCount; } diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index c5a2c181b..266d93287 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -530,10 +530,7 @@ private void ResolveAndTypecheck(CoreOptions options, IEnumerable absys) return; } var tc = new TypecheckingContext(null, options); - var oldCheckModifies = tc.CheckModifies; - tc.CheckModifies = false; absys.ForEach(absy => absy.Typecheck(tc)); - tc.CheckModifies = oldCheckModifies; } private List CreateAccessAsserts(Expr expr, IToken tok, string msg) diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 6a3d53f23..cdda0d7cf 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -2951,12 +2951,6 @@ public override void Resolve(ResolutionContext rc) public override void Typecheck(TypecheckingContext tc) { - if (IsAnonymous) - { - var modSetCollector = new ModSetCollector(tc.Options); - modSetCollector.DoModSetAnalysis(this.Impl); - } - var oldProc = tc.Proc; tc.Proc = this; base.Typecheck(tc); diff --git a/Source/Core/Analysis/ModSetCollector.cs b/Source/Core/Analysis/ModSetCollector.cs index c1939d9c1..f14df22b6 100644 --- a/Source/Core/Analysis/ModSetCollector.cs +++ b/Source/Core/Analysis/ModSetCollector.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; namespace Microsoft.Boogie; @@ -25,36 +26,10 @@ public ModSetCollector(CoreOptions options) private bool moreProcessingRequired; - public void DoModSetAnalysis(Implementation impl) - { - this.VisitImplementation(impl); - var proc = impl.Proc; - proc.Modifies = new List(); - foreach (Variable v in modSets[proc]) - { - proc.Modifies.Add(new IdentifierExpr(v.tok, v)); - } - } - public void DoModSetAnalysis(Program program) { Contract.Requires(program != null); - - if (options.Trace) - { -// Console.WriteLine(); -// Console.WriteLine("Running modset analysis ..."); -// int procCount = 0; -// foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) -// { -// Contract.Assert(decl != null); -// if (decl is Procedure) -// procCount++; -// } -// Console.WriteLine("Number of procedures = {0}", procCount);*/ - } - - HashSet implementedProcs = new HashSet(); + var implementedProcs = new HashSet(); foreach (var impl in program.Implementations) { if (impl.Proc != null) @@ -63,7 +38,7 @@ public void DoModSetAnalysis(Program program) } } - foreach (var proc in program.Procedures) + foreach (var proc in program.Procedures.Where(x => x is not YieldProcedureDecl)) { if (!implementedProcs.Contains(proc)) { @@ -100,30 +75,33 @@ public void DoModSetAnalysis(Program program) #if DEBUG_PRINT options.OutputWriter.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count); - foreach (Procedure/*!*/ x in modSets.Keys) { + foreach (Procedure x in modSets.Keys) + { Contract.Assert(x != null); options.OutputWriter.Write("{0} : ", x.Name); bool first = true; - foreach (Variable/*!*/ y in modSets[x]) { - Contract.Assert(y != null); + foreach (var y in modSets[x]) + { if (first) + { first = false; + } else + { options.OutputWriter.Write(", "); + } options.OutputWriter.Write("{0}", y.Name); } options.OutputWriter.WriteLine(""); - options.OutputWriter + } #endif } public override Implementation VisitImplementation(Implementation node) { - //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); enclosingProc = node.Proc; - Implementation /*!*/ - ret = base.VisitImplementation(node); + Implementation ret = base.VisitImplementation(node); Contract.Assert(ret != null); enclosingProc = null; @@ -169,9 +147,14 @@ public override Cmd VisitHavocCmd(HavocCmd havocCmd) public override Cmd VisitCallCmd(CallCmd callCmd) { - //Contract.Requires(callCmd != null); Contract.Ensures(Contract.Result() != null); Cmd ret = base.VisitCallCmd(callCmd); + + if (callCmd.IsAsync) + { + return ret; + } + foreach (IdentifierExpr ie in callCmd.Outs) { if (ie != null) @@ -215,7 +198,7 @@ private void ProcessVariable(Variable var) return; } - if (!(var is GlobalVariable)) + if (var is not GlobalVariable) { return; } diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 7cabd38ce..681e0d7b7 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -759,20 +759,19 @@ SpecRefinedActionForAtomicAction SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List ins, List outs.> = - (. IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List locals; StmtList stmtList; .) + (. IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.Atomic; List locals; StmtList stmtList; .) "refines" { Attribute } ( - MoverQualifier + [ MoverQualifier ] "action" (. tok = t; .) { Attribute } Ident ImplBody (. - if (m.val != "_") { - this.SemErr("expected _ for name of anoonymous action"); - } else if (refinedAction == null) { - var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), + if (refinedAction == null) { + var actionName = m.val == "_" ? null : m.val; + var actionDecl = new ActionDecl(tok, actionName, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), false, new List(), null, null, new List(), new List(), new List(), new List(), null, akv); Pgm.AddTopLevelDeclaration(actionDecl); @@ -1134,15 +1133,19 @@ WhileCmd "invariant" { Attribute } ( - Expression (. if (isFree) { - invariants.Add(new AssumeCmd(z, e, kv)); - } else { - invariants.Add(new AssertCmd(z, e, kv)); - } - kv = null; + Expression (. + if (isFree) { + invariants.Add(new AssumeCmd(z, e, kv)); + } else { + invariants.Add(new AssertCmd(z, e, kv)); + } + kv = null; .) | - CallCmd (. yields.Add((CallCmd)cmd); .) + CallCmd (. + yields.Add((CallCmd)cmd); + kv = null; + .) ) ";" } diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index b7ab2e965..d62bac5a3 100644 --- a/Source/Core/CoreOptions.cs +++ b/Source/Core/CoreOptions.cs @@ -55,7 +55,7 @@ public enum VerbosityLevel bool OverlookBoogieTypeErrors { get; } uint TimeLimit { get; } uint ResourceLimit { get; } - bool DoModSetAnalysis { get; } + bool DoModSetAnalysis { get; set; } bool DebugStagedHoudini { get; } int LoopUnrollCount { get; } bool DeterministicExtractLoops { get; } diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index e048776fe..b06d6cc77 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1219,13 +1219,15 @@ void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) { } void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken name, List ins, List outs) { - IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List locals; StmtList stmtList; + IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.Atomic; List locals; StmtList stmtList; Expect(41); while (la.kind == 26) { Attribute(ref kv); } - if (StartOf(5)) { - MoverQualifier(ref moverType); + if (StartOf(16)) { + if (StartOf(5)) { + MoverQualifier(ref moverType); + } Expect(39); tok = t; while (la.kind == 26) { @@ -1233,10 +1235,9 @@ void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken } Ident(out m); ImplBody(out locals, out stmtList); - if (m.val != "_") { - this.SemErr("expected _ for name of anoonymous action"); - } else if (refinedAction == null) { - var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), + if (refinedAction == null) { + var actionName = m.val == "_" ? null : m.val; + var actionDecl = new ActionDecl(tok, actionName, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), false, new List(), null, null, new List(), new List(), new List(), new List(), null, akv); Pgm.AddTopLevelDeclaration(actionDecl); @@ -1274,7 +1275,7 @@ void SpecYieldRequires(List pre, List yieldRequires ) { Expr e; Cmd cmd; Token tok; QKeyValue kv = null; Expect(49); tok = t; - if (StartOf(16)) { + if (StartOf(17)) { while (la.kind == 26) { Attribute(ref kv); } @@ -1338,7 +1339,7 @@ void SpecYieldEnsures(List post, List yieldEnsures ) { Expr e; Cmd cmd; Token tok; QKeyValue kv = null; Expect(50); tok = t; - if (StartOf(16)) { + if (StartOf(17)) { while (la.kind == 26) { Attribute(ref kv); } @@ -1423,8 +1424,8 @@ void StmtList(out StmtList/*!*/ stmtList) { StructuredCmd ec = null; StructuredCmd/*!*/ ecn; TransferCmd tc = null; TransferCmd/*!*/ tcn; - while (StartOf(17)) { - if (StartOf(18)) { + while (StartOf(18)) { + if (StartOf(19)) { LabelOrCmd(out c, out label); Contract.Assert(c == null || label == null); if (c != null) { @@ -1655,7 +1656,7 @@ void WhileCmd(out WhileCmd wcmd) { while (la.kind == 26) { Attribute(ref kv); } - if (StartOf(19)) { + if (StartOf(20)) { Expression(out e); if (isFree) { invariants.Add(new AssumeCmd(z, e, kv)); @@ -1666,7 +1667,9 @@ void WhileCmd(out WhileCmd wcmd) { } else if (la.kind == 38 || la.kind == 53 || la.kind == 71) { CallCmd(out cmd); - yields.Add((CallCmd)cmd); + yields.Add((CallCmd)cmd); + kv = null; + } else SynErr(151); Expect(10); } @@ -1695,7 +1698,7 @@ void Guard(out Expr e) { if (la.kind == 60) { Get(); e = null; - } else if (StartOf(19)) { + } else if (StartOf(20)) { Expression(out ee); e = ee; } else SynErr(152); @@ -1733,7 +1736,7 @@ void LabelOrAssign(out Cmd c, out IToken label) { Expect(10); c = new UnpackCmd(x, lhsExpr, e0, kv); - } else if (StartOf(20)) { + } else if (StartOf(21)) { lhss = new List(); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); while (la.kind == 19 || la.kind == 70) { @@ -1804,7 +1807,7 @@ void MapAssignIndex(out IToken/*!*/ x, out List/*!*/ indexes) { Expect(19); x = t; - if (StartOf(19)) { + if (StartOf(20)) { Expression(out e); indexes.Add(e); while (la.kind == 14) { @@ -1839,7 +1842,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { Ident(out first); if (la.kind == 11) { Get(); - if (StartOf(19)) { + if (StartOf(20)) { Expression(out en); es.Add(en); while (la.kind == 14) { @@ -1865,7 +1868,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { Expect(69); Ident(out first); Expect(11); - if (StartOf(19)) { + if (StartOf(20)) { Expression(out en); es.Add(en); while (la.kind == 14) { @@ -1893,7 +1896,7 @@ void Expressions(out List/*!*/ es) { void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; LogicalExpression(out e0); - if (StartOf(21)) { + if (StartOf(22)) { if (la.kind == 76 || la.kind == 77) { ImpliesOp(); x = t; @@ -1927,7 +1930,7 @@ void EquivOp() { void LogicalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; RelationalExpression(out e0); - if (StartOf(22)) { + if (StartOf(23)) { if (la.kind == 80 || la.kind == 81) { AndOp(); x = t; @@ -1973,7 +1976,7 @@ void ExpliesOp() { void RelationalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; BvTerm(out e0); - if (StartOf(23)) { + if (StartOf(24)) { RelOp(out x, out op); BvTerm(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -2072,7 +2075,7 @@ void Term(out Expr/*!*/ e0) { void Factor(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; Power(out e0); - while (StartOf(24)) { + while (StartOf(25)) { MulOp(out x, out op); Power(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -2145,7 +2148,7 @@ void UnaryExpression(out Expr/*!*/ e) { x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); - } else if (StartOf(25)) { + } else if (StartOf(26)) { CoercionExpression(out e); } else SynErr(163); } @@ -2197,8 +2200,8 @@ void ArrayExpression(out Expr/*!*/ e) { x = t; allArgs = new List (); allArgs.Add(e); store = false; bvExtract = false; - if (StartOf(26)) { - if (StartOf(19)) { + if (StartOf(27)) { + if (StartOf(20)) { Expression(out index0); if (index0 is BvBounds) bvExtract = true; @@ -2363,7 +2366,7 @@ void AtomExpression(out Expr/*!*/ e) { id = new IdentifierExpr(x, x.val); e = id; if (la.kind == 11) { Get(); - if (StartOf(19)) { + if (StartOf(20)) { Expressions(out es); e = new NAryExpr(x, new FunctionCall(id), es); } else if (la.kind == 12) { @@ -2402,7 +2405,7 @@ void AtomExpression(out Expr/*!*/ e) { } case 11: { Get(); - if (StartOf(19)) { + if (StartOf(20)) { Expression(out e); if (e is BvBounds) this.SemErr("parentheses around bitvector bounds are not allowed"); @@ -2617,7 +2620,7 @@ void SpecBlock(out Block/*!*/ b) { Ident(out x); Expect(13); - while (StartOf(18)) { + while (StartOf(19)) { LabelOrCmd(out c, out label); Contract.Assert(c == null || label == null); if (c != null) { @@ -2666,7 +2669,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { Get(); Ident(out id); parameters = new List(); - if (StartOf(19)) { + if (StartOf(20)) { AttributeParameter(out param); parameters.Add(param); while (la.kind == 14) { @@ -2694,7 +2697,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { } } - } else if (StartOf(19)) { + } else if (StartOf(20)) { Expression(out e); es = new List { e }; while (la.kind == 14) { @@ -2720,7 +2723,7 @@ void AttributeParameter(out object/*!*/ o) { if (la.kind == 4) { Get(); o = t.val.Substring(1, t.val.Length-2); - } else if (StartOf(19)) { + } else if (StartOf(20)) { Expression(out e); o = e; } else SynErr(177); @@ -2776,6 +2779,7 @@ public void Parse() { {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_T,_x,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index ee240bde7..29987d672 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -751,13 +751,12 @@ public class TypecheckingContext : CheckingContext public LayerRange ExpectedLayerRange; public bool GlobalAccessOnlyInOld; public int InsideOld; - public bool CheckModifies; + public bool CheckModifies => Proc != null && (!Options?.DoModSetAnalysis ?? true); public TypecheckingContext(IErrorSink errorSink, CoreOptions options) : base(errorSink) { this.Options = options; - this.CheckModifies = !options?.DoModSetAnalysis ?? true; } public bool InFrame(Variable v) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 72002036b..ff8085b26 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -339,6 +339,7 @@ public Program ParseBoogieProgram(IList fileNames, bool suppressTraceOut if (program.TopLevelDeclarations.Any(d => d.HasCivlAttribute())) { Options.Libraries.Add("base"); + Options.DoModSetAnalysis = true; } foreach (var libraryName in Options.Libraries) diff --git a/Test/civl/inductive-sequentialization/Gauss.bpl b/Test/civl/inductive-sequentialization/Gauss.bpl index 5fa9ee390..d440627db 100644 --- a/Test/civl/inductive-sequentialization/Gauss.bpl +++ b/Test/civl/inductive-sequentialization/Gauss.bpl @@ -8,7 +8,6 @@ var {:layer 0,2} x:int; atomic action {:layer 1} SUM (n: int) refines MAIN' using INV; creates ADD; -modifies x; { assert n >= 0; diff --git a/Test/civl/inductive-sequentialization/Gauss.bpl.expect b/Test/civl/inductive-sequentialization/Gauss.bpl.expect index 9823d44a8..3e6d423af 100644 --- a/Test/civl/inductive-sequentialization/Gauss.bpl.expect +++ b/Test/civl/inductive-sequentialization/Gauss.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 6 verified, 0 errors +Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/civl/large-samples/cache-coherence.bpl b/Test/civl/large-samples/cache-coherence.bpl new file mode 100644 index 000000000..5d622eb4e --- /dev/null +++ b/Test/civl/large-samples/cache-coherence.bpl @@ -0,0 +1,752 @@ +// RUN: %parallel-boogie -vcsSplitOnEveryAssert "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type MemAddr; + +type Value; + +datatype State { + Modified(), + Exclusive(), + Shared(), + Invalid() +} + +type CacheAddr; + +datatype Result { + Ok(), + Fail() +} + +datatype CacheLine { + CacheLine(ma: MemAddr, value: Value, state: State) +} + +type Cache = [CacheAddr]CacheLine; + +type CacheId; +const i0: CacheId; + +function Hash(MemAddr): CacheAddr; + +datatype DirState { + Owner(i: CacheId), + Sharers(iset: Set CacheId) +} + +datatype DirRequest { + EvictAtDir(i: CacheId), + ReadShdAtDir(i: CacheId), + ReadExcAtDir(i: CacheId), + NoDirRequest() +} + +datatype DirInfo { + DirInfo(state: DirState, currRequest: DirRequest) +} + +datatype CachePermission { + CachePermission(i: CacheId, ca: CacheAddr) +} + +datatype DirPermission { + DirPermission(i: CacheId, ma: MemAddr) +} + +function {:inline} WholeDirPermission(ma: MemAddr): Set DirPermission { + Set((lambda {:pool "DirPermission"} x: DirPermission :: x->ma == ma)) +} + +var {:layer 0,2} mem: [MemAddr]Value; +var {:layer 0,2} dir: [MemAddr]DirInfo; +var {:layer 0,2} cache: [CacheId]Cache; +var {:layer 0,1} cacheBusy: [CacheId][CacheAddr]bool; +var {:linear} {:layer 1,2} cachePermissions: Set CachePermission; +var {:linear} {:layer 1,2} dirPermissions: Set DirPermission; +var {:layer 1,3} absMem: [MemAddr]Value; + +/// Yield invariants +yield invariant {:layer 1} YieldInv#1(); +invariant (forall i: CacheId, ca: CacheAddr:: Set_Contains(cachePermissions, CachePermission(i, ca)) || cacheBusy[i][ca]); + +function {:inline} Owns(cache: [CacheId]Cache, i: CacheId, ca: CacheAddr): bool { + cache[i][ca]->state == Exclusive() || cache[i][ca]->state == Modified() +} + +yield invariant {:layer 2} YieldInv#2(); +invariant (forall i: CacheId, ca: CacheAddr:: Hash(cache[i][ca]->ma) == ca); +invariant (forall i: CacheId, ca: CacheAddr:: + (var line := cache[i][ca]; (var state := dir[line->ma]->state; + line->state == Invalid() || (line->value == absMem[line->ma] && if line->state == Shared() then state is Sharers else state is Owner)))); +invariant (forall ma: MemAddr:: {dir[ma]} (var state := dir[ma]->state; state is Owner ==> Owns(cache, state->i, Hash(ma)) && cache[state->i][Hash(ma)]->ma == ma)); +invariant (forall ma: MemAddr:: {dir[ma]} (var state := dir[ma]->state; state is Owner ==> + (forall i: CacheId:: cache[i][Hash(ma)]->ma == ma ==> state->i == i || cache[i][Hash(ma)]->state == Invalid()))); +invariant (forall ma: MemAddr:: {dir[ma]} (var state := dir[ma]->state; state is Sharers ==> + (forall i: CacheId:: Set_Contains(state->iset, i) ==> cache[i][Hash(ma)]->state == Shared() && cache[i][Hash(ma)]->ma == ma))); +invariant (forall ma: MemAddr:: {dir[ma]} (var state := dir[ma]->state; state is Sharers ==> + (forall i: CacheId:: cache[i][Hash(ma)]->ma == ma ==> Set_Contains(state->iset, i) || cache[i][Hash(ma)]->state == Invalid()))); +invariant (forall ma: MemAddr:: {dir[ma]} dir[ma]->state is Sharers ==> mem[ma] == absMem[ma]); +invariant (forall ma: MemAddr:: {dir[ma]} dir[ma]->currRequest == NoDirRequest() ==> Set_IsSubset(WholeDirPermission(ma), dirPermissions)); + +yield invariant {:layer 2} YieldEvict(i: CacheId, ma: MemAddr, value: Value, {:linear} drp: Set CachePermission); +invariant Set_Contains(drp, CachePermission(i, Hash(ma))); +invariant value == cache[i][Hash(ma)]->value; + +yield invariant {:layer 2} YieldRead(i: CacheId, ma: MemAddr, {:linear} drp: Set CachePermission); +invariant Set_Contains(drp, CachePermission(i, Hash(ma))); +invariant (var line := cache[i][Hash(ma)]; (line->state == Invalid() || line->state == Shared()) && line->ma == ma); + +/// Cache +yield procedure {:layer 2} cache_read(i: CacheId, ma: MemAddr) returns (result: Option Value) +preserves call YieldInv#2(); +refines atomic action {:layer 3} _ { + if (*) { + result := None(); + } else { + result := Some(absMem[ma]); + } +} +{ + call result := cache_read#1(i, ma); +} + +yield procedure {:layer 2} cache_write(i: CacheId, ma: MemAddr, v: Value) returns (result: Result) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +refines atomic action {:layer 3} _ { + if (*) { + result := Fail(); + } else { + result := Ok(); + absMem[ma] := v; + } +} +{ + call result := cache_write#1(i, ma, v); +} + +yield procedure {:layer 2} cache_evict_req(i: CacheId, ca: CacheAddr) returns (result: Result) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +{ + var ma: MemAddr; + var value: Value; + var {:linear} {:layer 1,2} drp: Set CachePermission; + + call result, ma, value, drp := cache_evict_req#1(i, ca); + if (result == Ok()) { + async call dir_evict_req(i, ma, value, drp); + } +} + +yield procedure {:layer 2} cache_read_shd_req(i: CacheId, ma: MemAddr) returns (result: Result) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +{ + var line: CacheLine; + var {:linear} {:layer 1,2} drp: Set CachePermission; + + call result, drp := cache_read_shd_req#1(i, ma); + if (result == Ok()) { + async call dir_read_shd_req(i, ma, drp); + } +} + +yield procedure {:layer 2} cache_read_exc_req(i: CacheId, ma: MemAddr) returns (result: Result) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +{ + var {:linear} {:layer 1,2} drp: Set CachePermission; + + call result, drp := cache_read_exc_req#1(i, ma); + if (result == Ok()) { + async call dir_read_exc_req(i, ma, drp); + } +} + +yield procedure {:layer 1} cache_read#1(i: CacheId, ma: MemAddr) returns (result: Option Value) +refines atomic action {:layer 2} _ { + if (*) { + result := None(); + } else if (*) { + result := Some(absMem[ma]); + } else { + call result := primitive_cache_read(i, ma); + } +} +{ + call result := cache_read#0(i, ma); +} + +yield procedure {:layer 1} cache_write#1(i: CacheId, ma: MemAddr, v: Value) returns (result: Result) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + var ca: CacheAddr; + var line: CacheLine; + + if (*) { + result := Fail(); + } else { + result := Ok(); + ca := Hash(ma); + line := cache[i][ca]; + assume line->state != Invalid() && line->state != Shared() && line->ma == ma && Set_Contains(cachePermissions, CachePermission(i, ca)); + cache[i][ca]->value := v; + cache[i][ca]->state := Modified(); + absMem[ma] := v; + } +} +{ + call result := cache_write#0(i, ma, v); + if (result == Ok()) { + call {:layer 1} absMem := Copy(absMem[ma := v]); + } +} + +yield procedure {:layer 1} cache_evict_req#1(i: CacheId, ca: CacheAddr) returns (result: Result, ma: MemAddr, value: Value, {:linear} {:layer 1} drp: Set CachePermission) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + var line: CacheLine; + + result := Fail(); + call drp := Set_MakeEmpty(); + if (*) { + assume Set_Contains(cachePermissions, CachePermission(i, ca)); + call drp := Set_Get(cachePermissions, MapOne(CachePermission(i, ca))); + line := cache[i][ca]; + ma := line->ma; + value := line->value; + result := Ok(); + } +} +{ + call result, ma, value := cache_evict_req#0(i, ca); + call {:layer 1} drp := Set_MakeEmpty(); + if (result == Ok()) { + call {:layer 1} drp := Set_Get(cachePermissions, MapOne(CachePermission(i, ca))); + } +} + +yield procedure {:layer 1} cache_read_shd_req#1(i: CacheId, ma: MemAddr) returns (result: Result, {:linear} {:layer 1} drp: Set CachePermission) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + var ca: CacheAddr; + var line: CacheLine; + + result := Fail(); + ca := Hash(ma); + line := cache[i][ca]; + call drp := Set_MakeEmpty(); + if (*) { + assume line->state == Invalid(); + assume Set_Contains(cachePermissions, CachePermission(i, ca)); + call drp := Set_Get(cachePermissions, MapOne(CachePermission(i, ca))); + cache[i][ca]->ma := ma; + result := Ok(); + } +} +{ + call result := cache_read_shd_req#0(i, ma); + call {:layer 1} drp := Set_MakeEmpty(); + if (result == Ok()) { + call {:layer 1} drp := Set_Get(cachePermissions, MapOne(CachePermission(i, Hash(ma)))); + } +} + +yield procedure {:layer 1} cache_read_exc_req#1(i: CacheId, ma: MemAddr) returns (result: Result, {:linear} {:layer 1} drp: Set CachePermission) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + var ca: CacheAddr; + var line: CacheLine; + + result := Fail(); + ca := Hash(ma); + line := cache[i][ca]; + call drp := Set_MakeEmpty(); + if (*) { + assume line->state == Invalid() || (line->ma == ma && line->state == Shared()); + assume Set_Contains(cachePermissions, CachePermission(i, ca)); + call drp := Set_Get(cachePermissions, MapOne(CachePermission(i, ca))); + cache[i][ca]->ma := ma; + result := Ok(); + } +} +{ + call result := cache_read_exc_req#0(i, ma); + call {:layer 1} drp := Set_MakeEmpty(); + if (result == Ok()) { + call {:layer 1} drp := Set_Get(cachePermissions, MapOne(CachePermission(i, Hash(ma)))); + } +} + +yield procedure {:layer 1} cache_nop_resp#1(i: CacheId, ma: MemAddr, {:linear_in} {:layer 1} drp: Set CachePermission, {:linear} {:layer 1} dp: Set DirPermission) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + assert Set_Contains(drp, CachePermission(i, Hash(ma))); + assert dp == WholeDirPermission(ma); + call Set_Put(cachePermissions, drp); +} +{ + call {:layer 1} Set_Put(cachePermissions, drp); +} + +yield procedure {:layer 1} cache_evict_resp#1(i: CacheId, ma: MemAddr, {:linear_in} {:layer 1} drp: Set CachePermission, {:linear} {:layer 1} dp: Set DirPermission) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + assert Set_Contains(drp, CachePermission(i, ca)); + assert dp == WholeDirPermission(ma); + assert line->ma == ma; + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + cache[i][ca]->state := Invalid(); + call Set_Put(cachePermissions, drp); +} +{ + call cache_evict_resp#0(i, ma); + call {:layer 1} Set_Put(cachePermissions, drp); +} + +yield procedure {:layer 1} cache_read_resp#1(i: CacheId, ma: MemAddr, v: Value, s: State, {:linear_in} {:layer 1} drp: Set CachePermission, {:linear} {:layer 1} dp: Set DirPermission) +preserves call YieldInv#1(); +refines left action {:layer 2} _ { + var ca: CacheAddr; + var line: CacheLine; + + assert dp == WholeDirPermission(ma); + assert s == Shared() || s == Exclusive(); + ca := Hash(ma); + assert Set_Contains(drp, CachePermission(i, ca)); + line := cache[i][ca]; + assert line->state == Invalid() || line->state == Shared(); + assert line->ma == ma; + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + if (line->state == Invalid()) { + cache[i][ca] := CacheLine(ma, v, s); + } else { + cache[i][ca]->state := s; + } + call Set_Put(cachePermissions, drp); +} +{ + call cache_read_resp#0(i, ma, v, s); + call {:layer 1} Set_Put(cachePermissions, drp); +} + +yield procedure {:layer 1} cache_snoop_req_shd#1(i: CacheId, ma: MemAddr, s: State, {:linear} {:layer 1} dp: Set DirPermission) +refines left action {:layer 2} _ { + var ca: CacheAddr; + + assert Set_Contains(dp, DirPermission(i, ma)); + assume {:add_to_pool "DirPermission", DirPermission(i, ma)} true; + ca := Hash(ma); + assert (forall j: CacheId :: (var line := cache[j][ca]; line->ma == ma ==> line->state == Invalid() || line->state == Shared())); + assert cache[i][ca]->value == absMem[ma]; + call primitive_cache_snoop_req_shd(i, ma, s); +} +{ + call cache_snoop_req_shd#0(i, ma, s); +} + +yield procedure {:layer 1} cache_snoop_req_exc#1(i: CacheId, ma: MemAddr, s: State, {:linear} {:layer 1} dp: Set DirPermission) returns (value: Value) +refines atomic action {:layer 2} _ { + assert dp == WholeDirPermission(ma); + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + call value := primitive_cache_snoop_req_exc(i, ma, s); +} +{ + call value := cache_snoop_req_exc#0(i, ma, s); +} + +// Cache primitives +yield procedure {:layer 0} cache_read#0(i: CacheId, ma: MemAddr) returns (result: Option Value); +refines atomic action {:layer 1} _ { + call result := primitive_cache_read(i, ma); +} + +action {:layer 1, 2} primitive_cache_read(i: CacheId, ma: MemAddr) returns (result: Option Value) +{ + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + result := None(); + if (line->state != Invalid() && line->ma == ma) { + result := Some(line->value); + } +} + +yield procedure {:layer 0} cache_write#0(i: CacheId, ma: MemAddr, v: Value) returns (result: Result); +refines atomic action {:layer 1} _ { + call result := primitive_cache_write(i, ma, v); +} + +action {:layer 1} primitive_cache_write(i: CacheId, ma: MemAddr, v: Value) returns (result: Result) +modifies cache; +{ + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + result := Fail(); + if (line->state != Invalid() && line->state != Shared() && line->ma == ma && !cacheBusy[i][ca]) { + cache[i][ca]->value := v; + cache[i][ca]->state := Modified(); + result := Ok(); + } +} + +yield procedure {:layer 0} cache_evict_req#0(i: CacheId, ca: CacheAddr) returns (result: Result, ma: MemAddr, value: Value); +refines atomic action {:layer 1} _ { + call result, ma, value := primitive_cache_evict_req(i, ca); +} + +action {:layer 1} primitive_cache_evict_req(i: CacheId, ca: CacheAddr) returns (result: Result, ma: MemAddr, value: Value) +modifies cache; +{ + var line: CacheLine; + + line := cache[i][ca]; + ma := line->ma; + value := line->value; + if (line->state != Invalid()) { + call result := acquire_cache_lock(i, ca); + } else { + result := Fail(); + } +} + +yield procedure {:layer 0} cache_read_shd_req#0(i: CacheId, ma: MemAddr) returns (result: Result); +refines atomic action {:layer 1} _ { + call result := primitive_cache_read_shd_req(i, ma); +} + +action {:layer 1} primitive_cache_read_shd_req(i: CacheId, ma: MemAddr) returns (result: Result) +modifies cache; +{ + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + if (line->state == Invalid()) { + call result := acquire_cache_lock(i, ca); + if (result == Ok()) { + cache[i][ca]->ma := ma; + } + } else { + result := Fail(); + } +} + +yield procedure {:layer 0} cache_read_exc_req#0(i: CacheId, ma: MemAddr) returns (result: Result); +refines atomic action {:layer 1} _ { + call result := primitive_cache_read_exc_req(i, ma); +} + +action {:layer 1} primitive_cache_read_exc_req(i: CacheId, ma: MemAddr) returns (result: Result) +{ + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + if (line->state == Invalid() || (line->ma == ma && line->state == Shared())) { + call result := acquire_cache_lock(i, ca); + if (result == Ok()) { + cache[i][ca]->ma := ma; + } + } else { + result := Fail(); + } +} + +action {:layer 1} acquire_cache_lock(i: CacheId, ca: CacheAddr) returns (result: Result) +modifies cache; +{ + if (!cacheBusy[i][ca]) { + cacheBusy[i][ca] := true; + result := Ok(); + } else { + result := Fail(); + } +} + +yield procedure {:layer 0} cache_evict_resp#0(i: CacheId, ma: MemAddr); +refines atomic action {:layer 1} _ { + call primitive_cache_evict_resp(i, ma); +} + +action {:layer 1} primitive_cache_evict_resp(i: CacheId, ma: MemAddr) +{ + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + assert line->ma == ma; + cache[i][ca]->state := Invalid(); + cacheBusy[i][ca] := false; +} + +yield procedure {:layer 0} cache_read_resp#0(i: CacheId, ma: MemAddr, v: Value, s: State); +refines atomic action {:layer 1} _ { + call primitive_cache_read_resp(i, ma, v, s); +} + +action {:layer 1} primitive_cache_read_resp(i: CacheId, ma: MemAddr, v: Value, s: State) +{ + var ca: CacheAddr; + var line: CacheLine; + + assert s == Shared() || s == Exclusive(); + ca := Hash(ma); + line := cache[i][ca]; + assert line->state == Invalid() || (line->state == Shared() && line->ma == ma); + cache[i][ca] := CacheLine(ma, if line->state == Invalid() then v else line->value, s); + cacheBusy[i][ca] := false; +} + +yield procedure {:layer 0} cache_snoop_req_shd#0(i: CacheId, ma: MemAddr, s: State); +refines atomic action {:layer 1} _ { + call primitive_cache_snoop_req_shd(i, ma, s); +} + +action {:layer 1,2} primitive_cache_snoop_req_shd(i: CacheId, ma: MemAddr, s: State) +{ + var ca: CacheAddr; + var line: CacheLine; + + assert s == Invalid(); + ca := Hash(ma); + line := cache[i][ca]; + assert line->state == Shared(); + assert line->ma == ma; + cache[i][ca]->state := s; +} + +yield procedure {:layer 0} cache_snoop_req_exc#0(i: CacheId, ma: MemAddr, s: State) returns (value: Value); +refines atomic action {:layer 1} _ { + call value := primitive_cache_snoop_req_exc(i, ma, s); +} + +action {:layer 1,2} primitive_cache_snoop_req_exc(i: CacheId, ma: MemAddr, s: State) returns (value: Value) +{ + var ca: CacheAddr; + var line: CacheLine; + + assert s == Invalid() || s == Shared(); + ca := Hash(ma); + line := cache[i][ca]; + assert line->state == Exclusive() || line->state == Modified(); + assert line->ma == ma; + value := line->value; + cache[i][ca]->state := s; +} + +/// Directory +yield procedure {:layer 2} dir_evict_req(i: CacheId, ma: MemAddr, value: Value, {:layer 1,2} {:linear_in} drp: Set CachePermission) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +requires call YieldEvict(i, ma, value, drp); +{ + var dirInfo: DirInfo; + var dirState: DirState; + var {:linear} {:layer 1,2} dp: Set DirPermission; + + par dirInfo, dp := dir_req_begin(ma, EvictAtDir(i)) | YieldInv#1(); + dirState := dirInfo->state; + // do not change dirState in case this is a stale evict request due to a race condition with a snoop + if (dirState == Owner(i)) { + par write_mem(ma, value, dp) | YieldInv#1(); + dirState := Sharers(Set_Empty()); + call cache_evict_resp#1(i, ma, drp, dp); + } else if (dirState is Sharers && Set_Contains(dirState->iset, i)) { + dirState := Sharers(Set_Remove(dirState->iset, i)); + call cache_evict_resp#1(i, ma, drp, dp); + } else { + call cache_nop_resp#1(i, ma, drp, dp); + } + par dir_req_end(ma, dirState, dp) | YieldInv#1(); +} + +yield procedure {:layer 2} dir_read_shd_req(i: CacheId, ma: MemAddr, {:layer 1,2} {:linear_in} drp: Set CachePermission) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +requires call YieldRead(i, ma, drp); +{ + var dirInfo: DirInfo; + var dirState: DirState; + var {:linear} {:layer 1,2} dp: Set DirPermission; + var value: Value; + + par dirInfo, dp := dir_req_begin(ma, ReadShdAtDir(i)) | YieldInv#1(); + dirState := dirInfo->state; + if (dirState is Owner) { + par value := cache_snoop_req_exc#1(dirState->i, ma, Shared(), dp) | YieldInv#1(); + par write_mem(ma, value, dp) | YieldInv#1(); + call cache_read_resp#1(i, ma, value, Shared(), drp, dp); + par dir_req_end(ma, Sharers(Set_Add(Set_Add(Set_Empty(), dirState->i), i)), dp) | YieldInv#1(); + } else { + par value := read_mem(ma, dp) | YieldInv#1(); + call cache_read_resp#1(i, ma, value, if dirState->iset == Set_Empty() then Exclusive() else Shared(), drp, dp); + par dir_req_end(ma, if dirState->iset == Set_Empty() then Owner(i) else Sharers(Set_Add(dirState->iset, i)), dp) | YieldInv#1(); + } +} + +yield procedure {:layer 2} dir_read_exc_req(i: CacheId, ma: MemAddr, {:layer 1,2} {:linear_in} drp: Set CachePermission) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +requires call YieldRead(i, ma, drp); +{ + var dirInfo: DirInfo; + var dirState: DirState; + var value: Value; + var {:linear} {:layer 1,2} dp: Set DirPermission; + var {:linear} {:layer 1,2} dpOne: Set DirPermission; + var victims: Set CacheId; + var victim: CacheId; + var {:layer 2} cache_s: [CacheId]Cache; + + par dirInfo, dp := dir_req_begin(ma, ReadExcAtDir(i)) | YieldInv#1(); + dirState := dirInfo->state; + if (dirState is Owner) { + par value := cache_snoop_req_exc#1(dirState->i, ma, Invalid(), dp) | YieldInv#1(); + par write_mem(ma, value, dp) | YieldInv#1(); + } else { + call {:layer 2} cache_s := Copy(cache); + victims := dirState->iset; + while (victims != Set_Empty()) + invariant {:yields} {:layer 1} true; + invariant {:layer 1} call YieldInv#1(); + invariant {:layer 2} dp == WholeDirPermission(ma); + invariant {:layer 2} Set_IsSubset(victims, dirState->iset); + invariant {:layer 2} (forall i: CacheId:: Set_Contains(dirState->iset, i) || cache[i] == cache_s[i]); + invariant {:layer 2} (forall i: CacheId:: Set_Contains(dirState->iset, i) ==> + if Set_Contains(victims, i) + then cache[i] == cache_s[i] + else cache[i] == cache_s[i][Hash(ma) := CacheLine(ma, cache_s[i][Hash(ma)]->value, Invalid())]); + { + victim := Choice(victims->val); + victims := Set_Remove(victims, victim); + par dpOne, dp := get_victim(victim, ma, dp) | YieldInv#1(); + par cache_snoop_req_shd#1(victim, ma, Invalid(), dpOne) | YieldInv#1(); + par dp := put_victim(dpOne, dp) | YieldInv#1(); + } + par value := read_mem(ma, dp) | YieldInv#1(); + } + call cache_read_resp#1(i, ma, value, Exclusive(), drp, dp); + par dir_req_end(ma, Owner(i), dp) | YieldInv#1(); +} + +yield procedure {:layer 1} get_victim(victim: CacheId, ma: MemAddr, {:layer 1} {:linear_in} dp: Set DirPermission) +returns ({:linear} {:layer 1} dpOne: Set DirPermission, {:linear} {:layer 1} dp': Set DirPermission) +refines both action {:layer 2} _ { + dp' := dp; + call dpOne := Set_Get(dp', MapOne(DirPermission(victim, ma))); +} +{ + dp' := dp; + call {:layer 1} dpOne := Set_Get(dp', MapOne(DirPermission(victim, ma))); +} + +yield procedure {:layer 1} put_victim({:linear_in} {:layer 1} dpOne: Set DirPermission, {:layer 1} {:linear_in} dp: Set DirPermission) +returns ({:linear} {:layer 1} dp': Set DirPermission) +refines both action {:layer 2} _ { + dp' := dp; + call Set_Put(dp', dpOne); +} +{ + dp' := dp; + call {:layer 1} Set_Put(dp', dpOne); +} + +yield procedure {:layer 1} dir_req_begin(ma: MemAddr, dirRequest: DirRequest) returns (dirInfo: DirInfo, {:linear} {:layer 1} dp: Set DirPermission) +refines right action {:layer 2} _ { + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + call dirInfo := primitive_dir_req_begin(ma, dirRequest); + call dp := Set_Get(dirPermissions, WholeDirPermission(ma)->val); +} +{ + call dirInfo := dir_req_begin#0(ma, dirRequest); + call {:layer 1} dp := Set_Get(dirPermissions, WholeDirPermission(ma)->val); +} + +yield procedure {:layer 1} dir_req_end(ma: MemAddr, dirState: DirState, {:layer 1} {:linear_in} dp: Set DirPermission) +refines left action {:layer 2} _ { + assert dp == WholeDirPermission(ma); + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + call primitive_dir_req_end(ma, dirState); + call Set_Put(dirPermissions, dp); +} +{ + call dir_req_end#0(ma, dirState); + call {:layer 1} Set_Put(dirPermissions, dp); +} + +// Directory primitives +yield procedure {:layer 0} dir_req_begin#0(ma: MemAddr, dirRequest: DirRequest) returns (dirInfo: DirInfo); +refines atomic action {:layer 1} _ { + call dirInfo := primitive_dir_req_begin(ma, dirRequest); +} + +action {:layer 1,2} primitive_dir_req_begin(ma: MemAddr, dirRequest: DirRequest) returns (dirInfo: DirInfo) +modifies dir; +{ + assert !(dirRequest is NoDirRequest); + assume dir[ma]->currRequest == NoDirRequest(); + dir[ma]->currRequest := dirRequest; + dirInfo := dir[ma]; +} + +yield procedure {:layer 0} dir_req_end#0(ma: MemAddr, dirState: DirState); +refines atomic action {:layer 1} _ { + call primitive_dir_req_end(ma, dirState); +} + +action {:layer 1,2} primitive_dir_req_end(ma: MemAddr, dirState: DirState) +modifies dir; +{ + assert !(dir[ma]->currRequest is NoDirRequest); + dir[ma]->state := dirState; + dir[ma]->currRequest := NoDirRequest(); +} + +/// Memory +yield procedure {:layer 1} read_mem(ma: MemAddr, {:linear} {:layer 1} dp: Set DirPermission) returns (value: Value) +refines both action {:layer 2} _ { + assert dp == WholeDirPermission(ma); + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + value := mem[ma]; +} +{ + call value := read_mem#0(ma); +} + +yield procedure {:layer 1} write_mem(ma: MemAddr, value: Value, {:linear} {:layer 1} dp: Set DirPermission) +refines both action {:layer 2} _ { + assert dp == WholeDirPermission(ma); + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + mem[ma] := value; +} +{ + call write_mem#0(ma, value); +} + +// Memory primitives +yield procedure {:layer 0} read_mem#0(ma: MemAddr) returns (value: Value); +refines atomic action {:layer 1} _ { + value := mem[ma]; +} + +yield procedure {:layer 0} write_mem#0(ma: MemAddr, value: Value); +refines atomic action {:layer 1} _ { + mem[ma] := value; +} + diff --git a/Test/civl/large-samples/cache-coherence.bpl.expect b/Test/civl/large-samples/cache-coherence.bpl.expect new file mode 100644 index 000000000..795fb8ddc --- /dev/null +++ b/Test/civl/large-samples/cache-coherence.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 94 verified, 0 errors diff --git a/Test/civl/regression-tests/Pure1.bpl b/Test/civl/regression-tests/Pure1.bpl index dd667ff21..b40ed0594 100644 --- a/Test/civl/regression-tests/Pure1.bpl +++ b/Test/civl/regression-tests/Pure1.bpl @@ -17,4 +17,14 @@ async atomic action A() pure action F() creates A; { -} \ No newline at end of file +} + +pure action G(d: int) +{ + x := d; +} + +pure action H() returns (d: int) +{ + d := x; +} diff --git a/Test/civl/regression-tests/Pure1.bpl.expect b/Test/civl/regression-tests/Pure1.bpl.expect index 0bceadf41..5bee4e351 100644 --- a/Test/civl/regression-tests/Pure1.bpl.expect +++ b/Test/civl/regression-tests/Pure1.bpl.expect @@ -1,4 +1,6 @@ Pure1.bpl(6,12): Error: unnecessary modifies clause for pure action Pure1.bpl(10,9): Error: cannot refer to a global variable in this context: x Pure1.bpl(17,12): Error: unnecessary creates clause for pure action -3 name resolution errors detected in Pure1.bpl \ No newline at end of file +Pure1.bpl(24,4): Error: cannot refer to a global variable in this context: x +Pure1.bpl(29,9): Error: cannot refer to a global variable in this context: x +5 name resolution errors detected in Pure1.bpl \ No newline at end of file diff --git a/Test/civl/regression-tests/Pure2.bpl b/Test/civl/regression-tests/Pure2.bpl deleted file mode 100644 index 709989049..000000000 --- a/Test/civl/regression-tests/Pure2.bpl +++ /dev/null @@ -1,10 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:layer 0,1} g:int; - -action {:layer 1} F(d: int) -{ - var c: int; - g := c; -} diff --git a/Test/civl/regression-tests/Pure2.bpl.expect b/Test/civl/regression-tests/Pure2.bpl.expect deleted file mode 100644 index 7abd8bcb6..000000000 --- a/Test/civl/regression-tests/Pure2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -Pure2.bpl(9,6): Error: command assigns to a global variable that is not in the enclosing action's modifies clause: g -1 type checking errors detected in Pure2.bpl diff --git a/Test/civl/regression-tests/anonymous-action-fail.bpl b/Test/civl/regression-tests/anonymous-action-fail.bpl deleted file mode 100644 index 3ce5c15b1..000000000 --- a/Test/civl/regression-tests/anonymous-action-fail.bpl +++ /dev/null @@ -1,9 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:layer 0,2} x: int; - -yield procedure {:layer 0} A(i: int) returns (j: int); -refines both action {:layer 1} B { - x := x + 1; -} \ No newline at end of file diff --git a/Test/civl/regression-tests/anonymous-action-fail.bpl.expect b/Test/civl/regression-tests/anonymous-action-fail.bpl.expect deleted file mode 100644 index ad2fa5050..000000000 --- a/Test/civl/regression-tests/anonymous-action-fail.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -anonymous-action-fail.bpl(9,1): error: expected _ for name of anoonymous action -1 parse errors detected in anonymous-action-fail.bpl diff --git a/Test/civl/regression-tests/anonymous-action.bpl b/Test/civl/regression-tests/anonymous-action.bpl index 8e9aa05bd..df33a221f 100644 --- a/Test/civl/regression-tests/anonymous-action.bpl +++ b/Test/civl/regression-tests/anonymous-action.bpl @@ -14,4 +14,15 @@ refines both action {:layer 2} _ { } { call j := A(i); +} + +yield procedure {:layer 0} C(i: int) returns (j: int); +refines both action {:layer 1} AC { + call Incr(); +} + +action {:layer 1} Incr() +modifies x; +{ + x := x + 1; } \ No newline at end of file diff --git a/Test/civl/regression-tests/anonymous-action.bpl.expect b/Test/civl/regression-tests/anonymous-action.bpl.expect index a9949f2e7..9823d44a8 100644 --- a/Test/civl/regression-tests/anonymous-action.bpl.expect +++ b/Test/civl/regression-tests/anonymous-action.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/samples/snapshot-parallel.bpl b/Test/civl/samples/snapshot-parallel.bpl new file mode 100644 index 000000000..05e338b3c --- /dev/null +++ b/Test/civl/samples/snapshot-parallel.bpl @@ -0,0 +1,141 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type Value; + +type Tid; + +datatype StampedValue { + StampedValue(ts: int, value: Value) +} + +var {:layer 0,3} mem: [int]StampedValue; + +const n: int; +axiom n >= 1; + +yield procedure {:layer 3} main() +{ + var snapshot: [int]StampedValue; + var i: int; + var v: Value; + + while (*) + invariant {:yields} {:layer 3} true; + { + if (*) + { + havoc i, v; + call write(i, v); + } + else + { + call snapshot := scan(); + } + } +} + +yield procedure {:layer 2} scan() returns (snapshot: [int]StampedValue) +refines atomic action {:layer 3} _ { + assume (forall j:int :: 1 <= j && j <= n ==> snapshot[j] == mem[j]); +} +{ + var i: int; + var b: bool; + var r1: [int]StampedValue; + var r2: [int]StampedValue; + var out: StampedValue; + + while (true) + invariant {:yields} true; + { + call r1 := scan_f(n); + call r2 := scan_s(n); + assert {:layer 2} (forall j:int :: 1 <= j && j <= n ==> (r1[j] == r2[j] ==> r1[j] == mem[j])); + if (r1 == r2) { + assert {:layer 2} (forall j:int :: 1 <= j && j <= n ==> r1[j] == mem[j]); + snapshot := r1; + break; + } + } +} + +yield right procedure {:layer 2} scan_f(i: int) returns (snapshot: [int]StampedValue) +requires {:layer 2} 0 <= i && i <= n; +ensures {:layer 2} (forall j:int :: 1 <= j && j <= i ==> + snapshot[j]->ts <= mem[j]->ts && + (snapshot[j]->ts == mem[j]->ts ==> snapshot[j]->value == mem[j]->value)); +{ + var out: StampedValue; + + if (i == 0) { + return; + } + par snapshot := scan_f(i-1) | out := read_f(i); + snapshot[i] := out; +} + +yield left procedure {:layer 2} scan_s(i: int) returns (snapshot: [int]StampedValue) +requires {:layer 2} 0 <= i && i <= n; +ensures {:layer 2} (forall j:int :: 1 <= j && j <= i ==> + mem[j]->ts <= snapshot[j]->ts && + (snapshot[j]->ts == mem[j]->ts ==> snapshot[j]->value == mem[j]->value)); +{ + var out: StampedValue; + + if (i == 0) { + return; + } + par snapshot := scan_s(i-1) | out := read_s(i); + snapshot[i] := out; +} + +right action {:layer 2} action_read_f (i: int) returns (out: StampedValue) +{ + var {:pool "K"} k: int; + var {:pool "V"} v: Value; + + if (*) { + assume {:add_to_pool "K", mem[i]->ts, k} {:add_to_pool "V", mem[i]->value, v} true; + assume k < mem[i]->ts; + out := StampedValue(k, v); + } else { + out := mem[i]; + } +} + +yield procedure {:layer 1} read_f (i: int) returns (out: StampedValue) +refines action_read_f; +{ + call out := read(i); +} + +left action {:layer 2} action_read_s(i: int) returns (out: StampedValue) +{ + var {:pool "K"} k: int; + var {:pool "V"} v: Value; + + if (*) { + assume {:add_to_pool "K", mem[i]->ts, k} {:add_to_pool "V", mem[i]->value, v} true; + assume k > mem[i]->ts; + out := StampedValue(k, v); + } else { + out := mem[i]; + } +} + +yield procedure {:layer 1} read_s (i: int) returns (out: StampedValue) +refines action_read_s; +{ + call out := read(i); +} + +yield procedure {:layer 0} write(i: int, v: Value); +refines atomic action {:layer 1,3} _ { + mem[i] := StampedValue(mem[i]->ts + 1, v); +} + +yield procedure {:layer 0} read (i: int) returns (v: StampedValue); +refines atomic action {:layer 1,3} _ { + v := mem[i]; +} \ No newline at end of file diff --git a/Test/civl/samples/snapshot-parallel.bpl.expect b/Test/civl/samples/snapshot-parallel.bpl.expect new file mode 100644 index 000000000..efe084e87 --- /dev/null +++ b/Test/civl/samples/snapshot-parallel.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 14 verified, 0 errors diff --git a/Test/civl/samples/snapshot.bpl b/Test/civl/samples/snapshot.bpl index 11f5f8d21..c0fcd1812 100644 --- a/Test/civl/samples/snapshot.bpl +++ b/Test/civl/samples/snapshot.bpl @@ -14,13 +14,31 @@ var {:layer 0,3} mem: [int]StampedValue; const n: int; axiom n >= 1; -atomic action {:layer 3} scan'() returns (snapshot: [int]StampedValue) +yield procedure {:layer 3} main() { - assume (forall j:int :: 1 <= j && j <= n ==> snapshot[j] == mem[j]); + var snapshot: [int]StampedValue; + var i: int; + var v: Value; + + while (*) + invariant {:yields} {:layer 3} true; + { + if (*) + { + havoc i, v; + call write(i, v); + } + else + { + call snapshot := scan(); + } + } } yield procedure {:layer 2} scan() returns (snapshot: [int]StampedValue) -refines scan'; +refines atomic action {:layer 3} _ { + assume (forall j:int :: 1 <= j && j <= n ==> snapshot[j] == mem[j]); +} { var i: int; var b: bool; @@ -65,8 +83,9 @@ refines scan'; right action {:layer 2} action_read_f (i: int) returns (out: StampedValue) { - var {:pool "K"} k:int; - var {:pool "V"} v:Value; + var {:pool "K"} k: int; + var {:pool "V"} v: Value; + if (*) { assume {:add_to_pool "K", mem[i]->ts, k} {:add_to_pool "V", mem[i]->value, v} true; assume k < mem[i]->ts; @@ -84,8 +103,8 @@ refines action_read_f; left action {:layer 2} action_read_s(i: int) returns (out: StampedValue) { - var {:pool "K"} k:int; - var {:pool "V"} v:Value; + var {:pool "K"} k: int; + var {:pool "V"} v: Value; if (*) { assume {:add_to_pool "K", mem[i]->ts, k} {:add_to_pool "V", mem[i]->value, v} true; @@ -102,18 +121,12 @@ refines action_read_s; call out := read(i); } -atomic action {:layer 1,3} action_write (v:Value, i: int) -modifies mem; -{ - var x: StampedValue; - x := mem[i]; - mem[i] := StampedValue(x->ts + 1, v); -} - -action {:layer 1,3} action_read (i: int) returns (v: StampedValue) -{ - v := mem[i]; +yield procedure {:layer 0} write(i: int, v: Value); +refines atomic action {:layer 1,3} _ { + mem[i] := StampedValue(mem[i]->ts + 1, v); } yield procedure {:layer 0} read (i: int) returns (v: StampedValue); -refines action_read; \ No newline at end of file +refines atomic action {:layer 1,3} _ { + v := mem[i]; +} \ No newline at end of file diff --git a/Test/civl/samples/snapshot.bpl.expect b/Test/civl/samples/snapshot.bpl.expect index 3e3dc54b2..12041afe1 100644 --- a/Test/civl/samples/snapshot.bpl.expect +++ b/Test/civl/samples/snapshot.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 7 verified, 0 errors +Boogie program verifier finished with 10 verified, 0 errors