From 21f1cfff139759d9b9f91ed800da2158daca8ed4 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 27 Aug 2015 20:10:41 -0700 Subject: Added /verifySnapshots:3, which prints recycled errors messages with the source locations of the new code. --- Source/ExecutionEngine/ExecutionEngine.cs | 45 +++++++++++++------------------ 1 file changed, 19 insertions(+), 26 deletions(-) (limited to 'Source/ExecutionEngine/ExecutionEngine.cs') diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 67ce49a5..a408642a 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -151,25 +151,18 @@ namespace Microsoft.Boogie { Contract.Requires(message != null); - if (category != null) - { + if (category != null) { message = string.Format("{0}: {1}", category, message); } string s; - if (tok != null) - { + if (tok != null) { s = string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(tok.filename), tok.line, tok.col, message); - } - else - { + } else { s = message; } - if (error) - { + if (error) { ErrorWriteLine(tw, s); - } - else - { + } else { tw.WriteLine(s); } } @@ -1114,23 +1107,23 @@ namespace Microsoft.Boogie printer.Inform(string.Format("Verifying {0} ...", impl.Name), output); int priority = 0; - if (0 < CommandLineOptions.Clo.VerifySnapshots) - { - verificationResult = Cache.Lookup(impl, out priority); - } - var wasCached = false; - if (verificationResult != null && priority == Priority.SKIP) - { - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start); - } + if (0 < CommandLineOptions.Clo.VerifySnapshots) { + var cachedResults = Cache.Lookup(impl, out priority); + if (cachedResults != null && priority == Priority.SKIP) { + if (CommandLineOptions.Clo.XmlSink != null) { + CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, cachedResults.Start); + } - printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output); - wasCached = true; + printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output); + if (CommandLineOptions.Clo.VerifySnapshots < 3 || cachedResults.Outcome == ConditionGeneration.Outcome.Correct) { + verificationResult = cachedResults; + wasCached = true; + } + } } - else + + if (!wasCached) { #region Verify the implementation -- cgit v1.2.3 From 80e6c54ccfeac0a2ae07c18f3c8f21970e483185 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 28 Sep 2015 09:42:55 -0700 Subject: cleaned up some names --- Source/Concurrency/CivlRefinement.cs | 1240 +++++++++++++++++++++++++++++ Source/Concurrency/CivlTypeChecker.cs | 1167 +++++++++++++++++++++++++++ Source/Concurrency/Concurrency.csproj | 8 +- Source/Concurrency/MoverCheck.cs | 26 +- Source/Concurrency/OwickiGries.cs | 1240 ----------------------------- Source/Concurrency/Program.cs | 12 +- Source/Concurrency/TypeCheck.cs | 1168 --------------------------- Source/Concurrency/YieldTypeChecker.cs | 36 +- Source/ExecutionEngine/ExecutionEngine.cs | 22 +- 9 files changed, 2459 insertions(+), 2460 deletions(-) create mode 100644 Source/Concurrency/CivlRefinement.cs create mode 100644 Source/Concurrency/CivlTypeChecker.cs delete mode 100644 Source/Concurrency/OwickiGries.cs delete mode 100644 Source/Concurrency/TypeCheck.cs (limited to 'Source/ExecutionEngine/ExecutionEngine.cs') diff --git a/Source/Concurrency/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs new file mode 100644 index 00000000..43d0f60c --- /dev/null +++ b/Source/Concurrency/CivlRefinement.cs @@ -0,0 +1,1240 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Threading.Tasks; +using Microsoft.Boogie; +using System.Diagnostics; +using System.Diagnostics.Contracts; +using Microsoft.Boogie.GraphUtil; + +namespace Microsoft.Boogie +{ + public class MyDuplicator : Duplicator + { + CivlTypeChecker civlTypeChecker; + public int layerNum; + Procedure enclosingProc; + Implementation enclosingImpl; + public Dictionary procMap; /* Original -> Duplicate */ + public Dictionary absyMap; /* Duplicate -> Original */ + public Dictionary implMap; /* Duplicate -> Original */ + public HashSet yieldingProcs; + public List impls; + + public MyDuplicator(CivlTypeChecker civlTypeChecker, int layerNum) + { + this.civlTypeChecker = civlTypeChecker; + this.layerNum = layerNum; + this.enclosingProc = null; + this.enclosingImpl = null; + this.procMap = new Dictionary(); + this.absyMap = new Dictionary(); + this.implMap = new Dictionary(); + this.yieldingProcs = new HashSet(); + this.impls = new List(); + } + + private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List newCmds) + { + int enclosingProcLayerNum = civlTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; + Procedure originalProc = originalCallCmd.Proc; + + if (civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc)) + { + if (civlTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum)) + { + newCmds.Add(callCmd); + } + } + else if (civlTypeChecker.procToActionInfo.ContainsKey(originalProc)) + { + AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo; + if (atomicActionInfo != null && atomicActionInfo.gate.Count > 0 && layerNum == enclosingProcLayerNum) + { + newCmds.Add(new HavocCmd(Token.NoToken, new List(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) }))); + Dictionary map = new Dictionary(); + for (int i = 0; i < originalProc.InParams.Count; i++) + { + map[originalProc.InParams[i]] = callCmd.Ins[i]; + } + Substitution subst = Substituter.SubstitutionFromHashtable(map); + foreach (AssertCmd assertCmd in atomicActionInfo.gate) + { + newCmds.Add(Substituter.Apply(subst, assertCmd)); + } + } + newCmds.Add(callCmd); + } + else + { + Debug.Assert(false); + } + } + + private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List newCmds) + { + int maxCalleeLayerNum = 0; + foreach (CallCmd iter in originalParCallCmd.CallCmds) + { + int calleeLayerNum = civlTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum; + if (calleeLayerNum > maxCalleeLayerNum) + maxCalleeLayerNum = calleeLayerNum; + } + if (layerNum > maxCalleeLayerNum) + { + for (int i = 0; i < parCallCmd.CallCmds.Count; i++) + { + ProcessCallCmd(originalParCallCmd.CallCmds[i], parCallCmd.CallCmds[i], newCmds); + absyMap[parCallCmd.CallCmds[i]] = originalParCallCmd; + } + } + else + { + newCmds.Add(parCallCmd); + } + } + + public override List VisitCmdSeq(List cmdSeq) + { + List cmds = base.VisitCmdSeq(cmdSeq); + List newCmds = new List(); + for (int i = 0; i < cmds.Count; i++) + { + Cmd originalCmd = cmdSeq[i]; + Cmd cmd = cmds[i]; + + CallCmd originalCallCmd = originalCmd as CallCmd; + if (originalCallCmd != null) + { + ProcessCallCmd(originalCallCmd, cmd as CallCmd, newCmds); + continue; + } + + ParCallCmd originalParCallCmd = originalCmd as ParCallCmd; + if (originalParCallCmd != null) + { + ProcessParCallCmd(originalParCallCmd, cmd as ParCallCmd, newCmds); + continue; + } + + newCmds.Add(cmd); + } + return newCmds; + } + + public override YieldCmd VisitYieldCmd(YieldCmd node) + { + YieldCmd yieldCmd = base.VisitYieldCmd(node); + absyMap[yieldCmd] = node; + return yieldCmd; + } + + public override Block VisitBlock(Block node) + { + Block block = base.VisitBlock(node); + absyMap[block] = node; + return block; + } + + public override Cmd VisitCallCmd(CallCmd node) + { + CallCmd callCmd = (CallCmd) base.VisitCallCmd(node); + callCmd.Proc = VisitProcedure(callCmd.Proc); + callCmd.callee = callCmd.Proc.Name; + absyMap[callCmd] = node; + return callCmd; + } + + public override Cmd VisitParCallCmd(ParCallCmd node) + { + ParCallCmd parCallCmd = (ParCallCmd) base.VisitParCallCmd(node); + absyMap[parCallCmd] = node; + return parCallCmd; + } + + public override Procedure VisitProcedure(Procedure node) + { + if (!civlTypeChecker.procToActionInfo.ContainsKey(node)) + return node; + if (!procMap.ContainsKey(node)) + { + enclosingProc = node; + Procedure proc = (Procedure)node.Clone(); + proc.Name = string.Format("{0}_{1}", node.Name, layerNum); + proc.InParams = this.VisitVariableSeq(node.InParams); + proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies); + proc.OutParams = this.VisitVariableSeq(node.OutParams); + + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[node]; + if (actionInfo.createdAtLayerNum < layerNum) + { + proc.Requires = new List(); + proc.Ensures = new List(); + Implementation impl; + AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; + if (atomicActionInfo != null) + { + CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.action); + List cmds = new List(); + foreach (AssertCmd assertCmd in atomicActionInfo.gate) + { + cmds.Add(new AssumeCmd(Token.NoToken, (Expr)Visit(assertCmd.Expr))); + } + Block newInitBlock = new Block(Token.NoToken, "_init", cmds, + new GotoCmd(Token.NoToken, new List(new string[] { action.Blocks[0].Label }), + new List(new Block[] { action.Blocks[0] }))); + List newBlocks = new List(); + newBlocks.Add(newInitBlock); + newBlocks.AddRange(action.Blocks); + impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks); + } + else + { + Block newInitBlock = new Block(Token.NoToken, "_init", new List(), new ReturnCmd(Token.NoToken)); + List newBlocks = new List(); + newBlocks.Add(newInitBlock); + impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List(), newBlocks); + } + impl.Proc = proc; + impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + impls.Add(impl); + } + else + { + yieldingProcs.Add(proc); + proc.Requires = this.VisitRequiresSeq(node.Requires); + proc.Ensures = this.VisitEnsuresSeq(node.Ensures); + } + procMap[node] = proc; + proc.Modifies = new List(); + civlTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x))); + } + return procMap[node]; + } + + private Variable dummyLocalVar; + public override Implementation VisitImplementation(Implementation node) + { + enclosingImpl = node; + dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool)); + Implementation impl = base.VisitImplementation(node); + implMap[impl] = node; + impl.LocVars.Add(dummyLocalVar); + impl.Name = impl.Proc.Name; + return impl; + } + + public override Requires VisitRequires(Requires node) + { + Requires requires = base.VisitRequires(node); + if (node.Free) + return requires; + if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) + requires.Condition = Expr.True; + return requires; + } + + public override Ensures VisitEnsures(Ensures node) + { + Ensures ensures = base.VisitEnsures(node); + if (node.Free) + return ensures; + AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo; + bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node; + if (isAtomicSpecification || !civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) + { + ensures.Condition = Expr.True; + ensures.Attributes = CivlRefinement.RemoveMoverAttribute(ensures.Attributes); + } + return ensures; + } + + public override Cmd VisitAssertCmd(AssertCmd node) + { + AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node); + if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) + assertCmd.Expr = Expr.True; + return assertCmd; + } + } + + public class CivlRefinement + { + LinearTypeChecker linearTypeChecker; + CivlTypeChecker civlTypeChecker; + Dictionary absyMap; + Dictionary implMap; + HashSet yieldingProcs; + int layerNum; + List globalMods; + Dictionary asyncAndParallelCallDesugarings; + List yieldCheckerProcs; + List yieldCheckerImpls; + Procedure yieldProc; + + Variable pc; + Variable ok; + Expr alpha; + Expr beta; + HashSet frame; + + public CivlRefinement(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, MyDuplicator duplicator) + { + this.linearTypeChecker = linearTypeChecker; + this.civlTypeChecker = civlTypeChecker; + this.absyMap = duplicator.absyMap; + this.layerNum = duplicator.layerNum; + this.implMap = duplicator.implMap; + this.yieldingProcs = duplicator.yieldingProcs; + Program program = linearTypeChecker.program; + globalMods = new List(); + foreach (Variable g in civlTypeChecker.SharedVariables) + { + globalMods.Add(Expr.Ident(g)); + } + asyncAndParallelCallDesugarings = new Dictionary(); + yieldCheckerProcs = new List(); + yieldCheckerImpls = new List(); + yieldProc = null; + } + + private IEnumerable AvailableLinearVars(Absy absy) + { + HashSet availableVars = new HashSet(linearTypeChecker.AvailableLinearVars(absyMap[absy])); + foreach (var g in civlTypeChecker.globalVarToSharedVarInfo.Keys) + { + SharedVariableInfo info = civlTypeChecker.globalVarToSharedVarInfo[g]; + if (!(info.introLayerNum <= layerNum && layerNum <= info.hideLayerNum)) + { + availableVars.Remove(g); + } + } + foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys) + { + LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v]; + if (info.isGhost) + { + if (info.layer != layerNum) + { + availableVars.Remove(v); + } + } + else + { + if (layerNum < info.layer) + { + availableVars.Remove(v); + } + } + } + return availableVars; + } + + private CallCmd CallToYieldProc(IToken tok, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) + { + List exprSeq = new List(); + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName])); + } + foreach (IdentifierExpr ie in globalMods) + { + exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl])); + } + if (yieldProc == null) + { + List inputs = new List(); + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + var domain = linearTypeChecker.linearDomains[domainName]; + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true); + inputs.Add(f); + } + foreach (IdentifierExpr ie in globalMods) + { + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); + inputs.Add(f); + } + yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", layerNum), new List(), inputs, new List(), new List(), new List(), new List()); + yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + } + CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List()); + yieldCallCmd.Proc = yieldProc; + return yieldCallCmd; + } + + private void AddCallToYieldProc(IToken tok, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) + { + if (!CommandLineOptions.Clo.TrustNonInterference) + { + CallCmd yieldCallCmd = CallToYieldProc(tok, ogOldGlobalMap, domainNameToLocalVar); + newCmds.Add(yieldCallCmd); + } + + if (pc != null) + { + Expr aa = OldEqualityExprForGlobals(ogOldGlobalMap); + Expr bb = OldEqualityExpr(ogOldGlobalMap); + + // assert pc || g_old == g || beta(i, g_old, o, g); + Expr assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta)); + assertExpr.Typecheck(new TypecheckingContext(null)); + AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, assertExpr); + skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated"; + newCmds.Add(skipOrBetaAssertCmd); + + // assert pc ==> o_old == o && g_old == g; + assertExpr = Expr.Imp(Expr.Ident(pc), bb); + assertExpr.Typecheck(new TypecheckingContext(null)); + AssertCmd skipAssertCmd = new AssertCmd(tok, assertExpr); + skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ; + newCmds.Add(skipAssertCmd); + + // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g); + List pcUpdateLHS = new List( + new AssignLhs[] { + new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)), + new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)) + }); + List pcUpdateRHS = new List( + new Expr[] { + Expr.Imp(aa, Expr.Ident(pc)), + Expr.Or(Expr.Ident(ok), beta) + }); + foreach (Expr e in pcUpdateRHS) + { + e.Typecheck(new TypecheckingContext(null)); + } + newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS)); + } + } + + private Dictionary ComputeAvailableExprs(IEnumerable availableLinearVars, Dictionary domainNameToInputVar) + { + Dictionary domainNameToExpr = new Dictionary(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + var expr = Expr.Ident(domainNameToInputVar[domainName]); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + domainNameToExpr[domainName] = expr; + } + foreach (Variable v in availableLinearVars) + { + var domainName = linearTypeChecker.FindDomainName(v); + if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; + var domain = linearTypeChecker.linearDomains[domainName]; + if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue; + Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List { Expr.Ident(v) }); + var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { ie, domainNameToExpr[domainName] }); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + domainNameToExpr[domainName] = expr; + } + return domainNameToExpr; + } + + private void AddUpdatesToOldGlobalVars(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar, Dictionary domainNameToExpr) + { + List lhss = new List(); + List rhss = new List(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName]))); + rhss.Add(domainNameToExpr[domainName]); + } + foreach (Variable g in ogOldGlobalMap.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); + rhss.Add(Expr.Ident(g)); + } + if (lhss.Count > 0) + { + newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); + } + } + + private Expr OldEqualityExpr(Dictionary ogOldGlobalMap) + { + Expr bb = Expr.True; + foreach (Variable o in ogOldGlobalMap.Keys) + { + if (o is GlobalVariable && !frame.Contains(o)) continue; + bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); + bb.Type = Type.Bool; + } + return bb; + } + + private Expr OldEqualityExprForGlobals(Dictionary ogOldGlobalMap) + { + Expr bb = Expr.True; + foreach (Variable o in ogOldGlobalMap.Keys) + { + if (o is GlobalVariable && frame.Contains(o)) + { + bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); + bb.Type = Type.Bool; + } + } + return bb; + } + + private void DesugarYield(YieldCmd yieldCmd, List cmds, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar) + { + AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); + + if (globalMods.Count > 0) + { + newCmds.Add(new HavocCmd(Token.NoToken, globalMods)); + if (pc != null) + { + // assume pc || alpha(i, g); + Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha); + assumeExpr.Type = Type.Bool; + newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr)); + } + } + + Dictionary domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(yieldCmd), domainNameToInputVar); + AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + + for (int j = 0; j < cmds.Count; j++) + { + PredicateCmd predCmd = (PredicateCmd)cmds[j]; + newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr)); + } + } + + public void DesugarParallelCallCmd(List newCmds, ParCallCmd parCallCmd) + { + List parallelCalleeNames = new List(); + List ins = new List(); + List outs = new List(); + string procName = "og"; + foreach (CallCmd callCmd in parCallCmd.CallCmds) + { + procName = procName + "_" + callCmd.Proc.Name; + ins.AddRange(callCmd.Ins); + outs.AddRange(callCmd.Outs); + } + Procedure proc; + if (asyncAndParallelCallDesugarings.ContainsKey(procName)) + { + proc = asyncAndParallelCallDesugarings[procName]; + } + else + { + List inParams = new List(); + List outParams = new List(); + List requiresSeq = new List(); + List ensuresSeq = new List(); + int count = 0; + foreach (CallCmd callCmd in parCallCmd.CallCmds) + { + Dictionary map = new Dictionary(); + foreach (Variable x in callCmd.Proc.InParams) + { + Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), true); + inParams.Add(y); + map[x] = Expr.Ident(y); + } + foreach (Variable x in callCmd.Proc.OutParams) + { + Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), false); + outParams.Add(y); + map[x] = Expr.Ident(y); + } + Contract.Assume(callCmd.Proc.TypeParameters.Count == 0); + Substitution subst = Substituter.SubstitutionFromHashtable(map); + foreach (Requires req in callCmd.Proc.Requires) + { + requiresSeq.Add(new Requires(req.tok, req.Free, Substituter.Apply(subst, req.Condition), null, req.Attributes)); + } + foreach (Ensures ens in callCmd.Proc.Ensures) + { + ensuresSeq.Add(new Ensures(ens.tok, ens.Free, Substituter.Apply(subst, ens.Condition), null, ens.Attributes)); + } + count++; + } + proc = new Procedure(Token.NoToken, procName, new List(), inParams, outParams, requiresSeq, globalMods, ensuresSeq); + asyncAndParallelCallDesugarings[procName] = proc; + } + CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes); + dummyCallCmd.Proc = proc; + newCmds.Add(dummyCallCmd); + } + + private void CreateYieldCheckerImpl(Implementation impl, List> yields) + { + if (yields.Count == 0) return; + + Dictionary map = new Dictionary(); + foreach (Variable local in impl.LocVars) + { + var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type)); + map[local] = Expr.Ident(copy); + } + + Program program = linearTypeChecker.program; + List locals = new List(); + List inputs = new List(); + foreach (IdentifierExpr ie in map.Values) + { + locals.Add(ie.Decl); + } + for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) + { + Variable inParam = impl.InParams[i]; + Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type)); + locals.Add(copy); + map[impl.InParams[i]] = Expr.Ident(copy); + } + { + int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count; + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + Variable inParam = impl.InParams[i]; + Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true); + inputs.Add(copy); + map[impl.InParams[i]] = Expr.Ident(copy); + i++; + } + } + for (int i = 0; i < impl.OutParams.Count; i++) + { + Variable outParam = impl.OutParams[i]; + var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type)); + locals.Add(copy); + map[impl.OutParams[i]] = Expr.Ident(copy); + } + Dictionary ogOldLocalMap = new Dictionary(); + Dictionary assumeMap = new Dictionary(map); + foreach (IdentifierExpr ie in globalMods) + { + Variable g = ie.Decl; + var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type)); + locals.Add(copy); + ogOldLocalMap[g] = Expr.Ident(copy); + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true); + inputs.Add(f); + assumeMap[g] = Expr.Ident(f); + } + + Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap); + Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap); + Substitution subst = Substituter.SubstitutionFromHashtable(map); + List yieldCheckerBlocks = new List(); + List labels = new List(); + List labelTargets = new List(); + Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); + labels.Add(yieldCheckerBlock.Label); + labelTargets.Add(yieldCheckerBlock); + yieldCheckerBlocks.Add(yieldCheckerBlock); + int yieldCount = 0; + foreach (List cs in yields) + { + List newCmds = new List(); + foreach (Cmd cmd in cs) + { + PredicateCmd predCmd = (PredicateCmd)cmd; + newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr))); + } + foreach (Cmd cmd in cs) + { + PredicateCmd predCmd = (PredicateCmd)cmd; + var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr); + if (predCmd is AssertCmd) + { + AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes); + assertCmd.ErrorData = "Non-interference check failed"; + newCmds.Add(assertCmd); + } + else + { + newCmds.Add(new AssumeCmd(Token.NoToken, newExpr)); + } + } + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); + yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken)); + labels.Add(yieldCheckerBlock.Label); + labelTargets.Add(yieldCheckerBlock); + yieldCheckerBlocks.Add(yieldCheckerBlock); + } + yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List(), new GotoCmd(Token.NoToken, labels, labelTargets))); + + // Create the yield checker procedure + var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", "Impl", impl.Name); + var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List(), new List(), new List(), new List()); + yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + yieldCheckerProcs.Add(yieldCheckerProc); + + // Create the yield checker implementation + var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List(), locals, yieldCheckerBlocks); + yieldCheckerImpl.Proc = yieldCheckerProc; + yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + yieldCheckerImpls.Add(yieldCheckerImpl); + } + + private bool IsYieldingHeader(Graph graph, Block header) + { + foreach (Block backEdgeNode in graph.BackEdgeNodes(header)) + { + foreach (Block x in graph.NaturalLoops(header, backEdgeNode)) + { + foreach (Cmd cmd in x.Cmds) + { + if (cmd is YieldCmd) + return true; + if (cmd is ParCallCmd) + return true; + CallCmd callCmd = cmd as CallCmd; + if (callCmd == null) continue; + if (yieldingProcs.Contains(callCmd.Proc)) + return true; + } + } + } + return false; + } + + private Graph ComputeYieldingLoopHeaders(Implementation impl, out HashSet yieldingHeaders) + { + Graph graph; + impl.PruneUnreachableBlocks(); + impl.ComputePredecessorsForBlocks(); + graph = Program.GraphFromImpl(impl); + graph.ComputeLoops(); + if (!graph.Reducible) + { + throw new Exception("Irreducible flow graphs are unsupported."); + } + yieldingHeaders = new HashSet(); + IEnumerable sortedHeaders = graph.SortHeadersByDominance(); + foreach (Block header in sortedHeaders) + { + if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header))) + { + yieldingHeaders.Add(header); + } + else if (IsYieldingHeader(graph, header)) + { + yieldingHeaders.Add(header); + } + else + { + continue; + } + } + return graph; + } + + private void SetupRefinementCheck(Implementation impl, + out List newLocalVars, + out Dictionary domainNameToInputVar, out Dictionary domainNameToLocalVar, out Dictionary ogOldGlobalMap) + { + pc = null; + ok = null; + alpha = null; + beta = null; + frame = null; + + newLocalVars = new List(); + Program program = linearTypeChecker.program; + ogOldGlobalMap = new Dictionary(); + foreach (IdentifierExpr ie in globalMods) + { + Variable g = ie.Decl; + LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type)); + ogOldGlobalMap[g] = l; + newLocalVars.Add(l); + } + + Procedure originalProc = implMap[impl].Proc; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[originalProc]; + if (actionInfo.createdAtLayerNum == this.layerNum) + { + pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool)); + newLocalVars.Add(pc); + ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool)); + newLocalVars.Add(ok); + Dictionary alwaysMap = new Dictionary(); + for (int i = 0; i < originalProc.InParams.Count; i++) + { + alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]); + } + for (int i = 0; i < originalProc.OutParams.Count; i++) + { + alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]); + } + Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap); + Dictionary foroldMap = new Dictionary(); + foreach (IdentifierExpr ie in globalMods) + { + foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]); + } + Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); + frame = new HashSet(civlTypeChecker.SharedVariables); + foreach (Variable v in civlTypeChecker.SharedVariables) + { + if (civlTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || + civlTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum) + { + frame.Remove(v); + } + } + AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; + if (atomicActionInfo == null) + { + beta = Expr.True; + foreach (var v in frame) + { + beta = Expr.And(beta, Expr.Eq(Expr.Ident(v), foroldMap[v])); + } + alpha = Expr.True; + } + else + { + Expr betaExpr = (new MoverCheck.TransitionRelationComputation(civlTypeChecker.program, atomicActionInfo, frame, new HashSet())).TransitionRelationCompute(true); + beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr); + Expr alphaExpr = Expr.True; + foreach (AssertCmd assertCmd in atomicActionInfo.gate) + { + alphaExpr = Expr.And(alphaExpr, assertCmd.Expr); + alphaExpr.Type = Type.Bool; + } + alpha = Substituter.Apply(always, alphaExpr); + } + foreach (Variable f in impl.OutParams) + { + LocalVariable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_old_{0}", f.Name), f.TypedIdent.Type)); + newLocalVars.Add(copy); + ogOldGlobalMap[f] = copy; + } + } + + domainNameToInputVar = new Dictionary(); + domainNameToLocalVar = new Dictionary(); + { + int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count; + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + Variable inParam = impl.InParams[i]; + domainNameToInputVar[domainName] = inParam; + Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type)); + domainNameToLocalVar[domainName] = l; + newLocalVars.Add(l); + i++; + } + } + } + + private void TransformImpl(Implementation impl) + { + HashSet yieldingHeaders; + Graph graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders); + + List newLocalVars; + Dictionary domainNameToInputVar, domainNameToLocalVar; + Dictionary ogOldGlobalMap; + SetupRefinementCheck(impl, out newLocalVars, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap); + + List> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap); + + List oldPcs, oldOks; + ProcessLoopHeaders(impl, graph, yieldingHeaders, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap, out oldPcs, out oldOks); + + AddInitialBlock(impl, oldPcs, oldOks, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap); + + CreateYieldCheckerImpl(impl, yields); + + impl.LocVars.AddRange(newLocalVars); + impl.LocVars.AddRange(oldPcs); + impl.LocVars.AddRange(oldOks); + + UnifyCallsToYieldProc(impl, ogOldGlobalMap, domainNameToLocalVar); + } + + private void UnifyCallsToYieldProc(Implementation impl, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) + { + CallCmd yieldCallCmd = CallToYieldProc(Token.NoToken, ogOldGlobalMap, domainNameToLocalVar); + Block yieldCheckBlock = new Block(Token.NoToken, "CallToYieldProc", new List(new Cmd[] { yieldCallCmd, new AssumeCmd(Token.NoToken, Expr.False) }), new ReturnCmd(Token.NoToken)); + List newBlocks = new List(); + foreach (Block b in impl.Blocks) + { + TransferCmd transferCmd = b.TransferCmd; + List newCmds = new List(); + for (int i = b.Cmds.Count-1; i >= 0; i--) + { + CallCmd callCmd = b.Cmds[i] as CallCmd; + if (callCmd == null || callCmd.Proc != yieldProc) + { + newCmds.Insert(0, b.Cmds[i]); + } + else + { + Block newBlock = new Block(Token.NoToken, b.Label + i, newCmds, transferCmd); + newCmds = new List(); + transferCmd = new GotoCmd(Token.NoToken, new List(new string[] { newBlock.Label, yieldCheckBlock.Label }), + new List(new Block[] { newBlock, yieldCheckBlock })); + newBlocks.Add(newBlock); + } + } + b.Cmds = newCmds; + b.TransferCmd = transferCmd; + } + impl.Blocks.AddRange(newBlocks); + impl.Blocks.Add(yieldCheckBlock); + } + + private List> CollectAndDesugarYields(Implementation impl, + Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap) + { + // Collect the yield predicates and desugar yields + List> yields = new List>(); + List cmds = new List(); + foreach (Block b in impl.Blocks) + { + YieldCmd yieldCmd = null; + List newCmds = new List(); + for (int i = 0; i < b.Cmds.Count; i++) + { + Cmd cmd = b.Cmds[i]; + if (cmd is YieldCmd) + { + yieldCmd = (YieldCmd)cmd; + continue; + } + if (yieldCmd != null) + { + PredicateCmd pcmd = cmd as PredicateCmd; + if (pcmd == null) + { + DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar); + if (cmds.Count > 0) + { + yields.Add(cmds); + cmds = new List(); + } + yieldCmd = null; + } + else + { + cmds.Add(pcmd); + } + } + + if (cmd is CallCmd) + { + CallCmd callCmd = cmd as CallCmd; + if (yieldingProcs.Contains(callCmd.Proc)) + { + AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); + } + if (callCmd.IsAsync) + { + if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name)) + { + asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List(), new List()); + } + var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name]; + CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs, callCmd.Attributes); + dummyCallCmd.Proc = dummyAsyncTargetProc; + newCmds.Add(dummyCallCmd); + } + else + { + newCmds.Add(callCmd); + } + if (yieldingProcs.Contains(callCmd.Proc)) + { + HashSet availableLinearVars = new HashSet(AvailableLinearVars(callCmd)); + linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars); + + if (!callCmd.IsAsync && globalMods.Count > 0 && pc != null) + { + // assume pc || alpha(i, g); + Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha); + assumeExpr.Type = Type.Bool; + newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr)); + } + + Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); + AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + } + } + else if (cmd is ParCallCmd) + { + ParCallCmd parCallCmd = cmd as ParCallCmd; + AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); + DesugarParallelCallCmd(newCmds, parCallCmd); + HashSet availableLinearVars = new HashSet(AvailableLinearVars(parCallCmd)); + linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars); + + if (globalMods.Count > 0 && pc != null) + { + // assume pc || alpha(i, g); + Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha); + assumeExpr.Type = Type.Bool; + newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr)); + } + + Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); + AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + } + else + { + newCmds.Add(cmd); + } + } + if (yieldCmd != null) + { + DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar); + if (cmds.Count > 0) + { + yields.Add(cmds); + cmds = new List(); + } + } + if (b.TransferCmd is ReturnCmd) + { + AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); + if (pc != null) + { + AssertCmd assertCmd = new AssertCmd(b.TransferCmd.tok, Expr.Ident(ok)); + assertCmd.ErrorData = "Failed to execute atomic action before procedure return"; + newCmds.Add(assertCmd); + } + } + b.Cmds = newCmds; + } + return yields; + } + + private void ProcessLoopHeaders(Implementation impl, Graph graph, HashSet yieldingHeaders, + Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap, + out List oldPcs, out List oldOks) + { + oldPcs = new List(); + oldOks = new List(); + foreach (Block header in yieldingHeaders) + { + LocalVariable oldPc = null; + LocalVariable oldOk = null; + if (pc != null) + { + oldPc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", pc.Name, header.Label), Type.Bool)); + oldPcs.Add(oldPc); + oldOk = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", ok.Name, header.Label), Type.Bool)); + oldOks.Add(oldOk); + } + Dictionary domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar); + foreach (Block pred in header.Predecessors) + { + AddCallToYieldProc(header.tok, pred.Cmds, ogOldGlobalMap, domainNameToLocalVar); + if (pc != null && !graph.BackEdgeNodes(header).Contains(pred)) + { + pred.Cmds.Add(new AssignCmd(Token.NoToken, new List( + new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }), + new List(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) }))); + } + AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + } + List newCmds = new List(); + if (pc != null) + { + AssertCmd assertCmd; + assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc))); + assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers"; + newCmds.Add(assertCmd); + assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok))); + assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers"; + newCmds.Add(assertCmd); + } + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName]))); + } + foreach (Variable v in ogOldGlobalMap.Keys) + { + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v])))); + } + newCmds.AddRange(header.Cmds); + header.Cmds = newCmds; + } + } + + private void AddInitialBlock(Implementation impl, List oldPcs, List oldOks, + Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap) + { + // Add initial block + List lhss = new List(); + List rhss = new List(); + if (pc != null) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc))); + rhss.Add(Expr.False); + foreach (Variable oldPc in oldPcs) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc))); + rhss.Add(Expr.False); + } + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))); + rhss.Add(Expr.False); + foreach (Variable oldOk in oldOks) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk))); + rhss.Add(Expr.False); + } + } + Dictionary domainNameToExpr = new Dictionary(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]); + } + for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) + { + Variable v = impl.InParams[i]; + var domainName = linearTypeChecker.FindDomainName(v); + if (domainName == null) continue; + if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; + var domain = linearTypeChecker.linearDomains[domainName]; + if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue; + Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List { Expr.Ident(v) }); + domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { ie, domainNameToExpr[domainName] }); + } + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName]))); + rhss.Add(domainNameToExpr[domainName]); + } + foreach (Variable g in ogOldGlobalMap.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); + rhss.Add(Expr.Ident(g)); + } + if (lhss.Count > 0) + { + Block initBlock = new Block(Token.NoToken, "og_init", new List { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] })); + impl.Blocks.Insert(0, initBlock); + } + } + + private void AddYieldProcAndImpl(List decls) + { + if (yieldProc == null) return; + + Program program = linearTypeChecker.program; + List inputs = new List(); + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + var domain = linearTypeChecker.linearDomains[domainName]; + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true); + inputs.Add(f); + } + foreach (IdentifierExpr ie in globalMods) + { + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); + inputs.Add(f); + } + List blocks = new List(); + TransferCmd transferCmd = new ReturnCmd(Token.NoToken); + if (yieldCheckerProcs.Count > 0) + { + List blockTargets = new List(); + List labelTargets = new List(); + int labelCount = 0; + foreach (Procedure proc in yieldCheckerProcs) + { + List exprSeq = new List(); + foreach (Variable v in inputs) + { + exprSeq.Add(Expr.Ident(v)); + } + CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List()); + callCmd.Proc = proc; + string label = string.Format("L_{0}", labelCount++); + Block block = new Block(Token.NoToken, label, new List { callCmd }, new ReturnCmd(Token.NoToken)); + labelTargets.Add(label); + blockTargets.Add(block); + blocks.Add(block); + } + transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets); + } + blocks.Insert(0, new Block(Token.NoToken, "enter", new List(), transferCmd)); + + var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List(), inputs, new List(), new List(), blocks); + yieldImpl.Proc = yieldProc; + yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + decls.Add(yieldProc); + decls.Add(yieldImpl); + } + + public static QKeyValue RemoveYieldsAttribute(QKeyValue iter) + { + if (iter == null) return null; + iter.Next = RemoveYieldsAttribute(iter.Next); + return (iter.Key == "yields") ? iter.Next : iter; + } + + public static QKeyValue RemoveMoverAttribute(QKeyValue iter) + { + if (iter == null) return null; + iter.Next = RemoveMoverAttribute(iter.Next); + if (iter.Key == "atomic" || iter.Key == "right" || iter.Key == "left" || iter.Key == "both") + return iter.Next; + else + return iter; + } + + private List Collect() + { + List decls = new List(); + foreach (Procedure proc in yieldCheckerProcs) + { + decls.Add(proc); + } + foreach (Implementation impl in yieldCheckerImpls) + { + decls.Add(impl); + } + foreach (Procedure proc in asyncAndParallelCallDesugarings.Values) + { + decls.Add(proc); + } + AddYieldProcAndImpl(decls); + return decls; + } + + public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List decls) + { + Program program = linearTypeChecker.program; + foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums) + { + if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; + + MyDuplicator duplicator = new MyDuplicator(civlTypeChecker, layerNum); + foreach (var proc in program.Procedures) + { + if (!civlTypeChecker.procToActionInfo.ContainsKey(proc)) continue; + Procedure duplicateProc = duplicator.VisitProcedure(proc); + decls.Add(duplicateProc); + } + decls.AddRange(duplicator.impls); + CivlRefinement civlTransform = new CivlRefinement(linearTypeChecker, civlTypeChecker, duplicator); + foreach (var impl in program.Implementations) + { + if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum) + continue; + Implementation duplicateImpl = duplicator.VisitImplementation(impl); + civlTransform.TransformImpl(duplicateImpl); + decls.Add(duplicateImpl); + } + decls.AddRange(civlTransform.Collect()); + } + } + } +} diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs new file mode 100644 index 00000000..dba7ab4b --- /dev/null +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -0,0 +1,1167 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using Microsoft.Boogie; +using System.Diagnostics.Contracts; +using System.Diagnostics; + +namespace Microsoft.Boogie +{ + public enum MoverType + { + Top, + Atomic, + Right, + Left, + Both + } + + public class ActionInfo + { + public Procedure proc; + public int createdAtLayerNum; + public int availableUptoLayerNum; + public bool hasImplementation; + public bool isExtern; + + public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum) + { + this.proc = proc; + this.createdAtLayerNum = createdAtLayerNum; + this.availableUptoLayerNum = availableUptoLayerNum; + this.hasImplementation = false; + this.isExtern = QKeyValue.FindBoolAttribute(proc.Attributes, "extern"); + } + + public virtual bool IsRightMover + { + get { return true; } + } + + public virtual bool IsLeftMover + { + get { return true; } + } + } + + public class AtomicActionInfo : ActionInfo + { + public Ensures ensures; + public MoverType moverType; + public List gate; + public CodeExpr action; + public List thisGate; + public CodeExpr thisAction; + public List thisInParams; + public List thisOutParams; + public List thatGate; + public CodeExpr thatAction; + public List thatInParams; + public List thatOutParams; + public HashSet actionUsedGlobalVars; + public HashSet modifiedGlobalVars; + public HashSet gateUsedGlobalVars; + public bool hasAssumeCmd; + public Dictionary thisMap; + public Dictionary thatMap; + + public bool CommutesWith(AtomicActionInfo actionInfo) + { + if (this.modifiedGlobalVars.Intersect(actionInfo.actionUsedGlobalVars).Count() > 0) + return false; + if (this.actionUsedGlobalVars.Intersect(actionInfo.modifiedGlobalVars).Count() > 0) + return false; + return true; + } + + public override bool IsRightMover + { + get { return moverType == MoverType.Right || moverType == MoverType.Both; } + } + + public override bool IsLeftMover + { + get { return moverType == MoverType.Left || moverType == MoverType.Both; } + } + + public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int layerNum, int availableUptoLayerNum) + : base(proc, layerNum, availableUptoLayerNum) + { + this.ensures = ensures; + this.moverType = moverType; + this.gate = new List(); + this.action = ensures.Condition as CodeExpr; + this.thisGate = new List(); + this.thisInParams = new List(); + this.thisOutParams = new List(); + this.thatGate = new List(); + this.thatInParams = new List(); + this.thatOutParams = new List(); + this.hasAssumeCmd = false; + this.thisMap = new Dictionary(); + this.thatMap = new Dictionary(); + + foreach (Block block in this.action.Blocks) + { + block.Cmds.ForEach(x => this.hasAssumeCmd = this.hasAssumeCmd || x is AssumeCmd); + } + + foreach (Block block in this.action.Blocks) + { + if (block.TransferCmd is ReturnExprCmd) + { + block.TransferCmd = new ReturnCmd(block.TransferCmd.tok); + } + } + + var cmds = this.action.Blocks[0].Cmds; + for (int i = 0; i < cmds.Count; i++) + { + AssertCmd assertCmd = cmds[i] as AssertCmd; + if (assertCmd == null) break; + this.gate.Add(assertCmd); + cmds[i] = new AssumeCmd(assertCmd.tok, Expr.True); + } + + foreach (Variable x in proc.InParams) + { + Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), true, x.Attributes); + this.thisInParams.Add(thisx); + this.thisMap[x] = Expr.Ident(thisx); + Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true, x.Attributes); + this.thatInParams.Add(thatx); + this.thatMap[x] = Expr.Ident(thatx); + } + foreach (Variable x in proc.OutParams) + { + Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), false, x.Attributes); + this.thisOutParams.Add(thisx); + this.thisMap[x] = Expr.Ident(thisx); + Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false, x.Attributes); + this.thatOutParams.Add(thatx); + this.thatMap[x] = Expr.Ident(thatx); + } + List thisLocVars = new List(); + List thatLocVars = new List(); + foreach (Variable x in this.action.LocVars) + { + Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), false); + thisMap[x] = Expr.Ident(thisx); + thisLocVars.Add(thisx); + Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false); + thatMap[x] = Expr.Ident(thatx); + thatLocVars.Add(thatx); + } + Contract.Assume(proc.TypeParameters.Count == 0); + Substitution thisSubst = Substituter.SubstitutionFromHashtable(this.thisMap); + Substitution thatSubst = Substituter.SubstitutionFromHashtable(this.thatMap); + foreach (AssertCmd assertCmd in this.gate) + { + this.thisGate.Add((AssertCmd)Substituter.Apply(thisSubst, assertCmd)); + this.thatGate.Add((AssertCmd)Substituter.Apply(thatSubst, assertCmd)); + } + this.thisAction = new CodeExpr(thisLocVars, SubstituteBlocks(this.action.Blocks, thisSubst, "this_")); + this.thatAction = new CodeExpr(thatLocVars, SubstituteBlocks(this.action.Blocks, thatSubst, "that_")); + + { + VariableCollector collector = new VariableCollector(); + collector.Visit(this.action); + this.actionUsedGlobalVars = new HashSet(collector.usedVars.Where(x => x is GlobalVariable)); + } + + List modifiedVars = new List(); + foreach (Block block in this.action.Blocks) + { + block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars)); + } + this.modifiedGlobalVars = new HashSet(modifiedVars.Where(x => x is GlobalVariable)); + + { + VariableCollector collector = new VariableCollector(); + this.gate.ForEach(assertCmd => collector.Visit(assertCmd)); + this.gateUsedGlobalVars = new HashSet(collector.usedVars.Where(x => x is GlobalVariable)); + } + } + + private List SubstituteBlocks(List blocks, Substitution subst, string blockLabelPrefix) + { + Dictionary blockMap = new Dictionary(); + List otherBlocks = new List(); + foreach (Block block in blocks) + { + List otherCmds = new List(); + foreach (Cmd cmd in block.Cmds) + { + otherCmds.Add(Substituter.Apply(subst, cmd)); + } + Block otherBlock = new Block(); + otherBlock.Cmds = otherCmds; + otherBlock.Label = blockLabelPrefix + block.Label; + otherBlocks.Add(otherBlock); + blockMap[block] = otherBlock; + } + foreach (Block block in blocks) + { + if (block.TransferCmd is ReturnCmd) + { + blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok); + continue; + } + List otherGotoCmdLabelTargets = new List(); + List otherGotoCmdLabelNames = new List(); + GotoCmd gotoCmd = block.TransferCmd as GotoCmd; + foreach (Block target in gotoCmd.labelTargets) + { + otherGotoCmdLabelTargets.Add(blockMap[target]); + otherGotoCmdLabelNames.Add(blockMap[target].Label); + } + blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets); + } + return otherBlocks; + } + } + + public class SharedVariableInfo + { + public int introLayerNum; + public int hideLayerNum; + + public SharedVariableInfo(int introLayerNum, int hideLayerNum) + { + this.introLayerNum = introLayerNum; + this.hideLayerNum = hideLayerNum; + } + } + + public class LayerEraser : ReadOnlyVisitor + { + private QKeyValue RemoveLayerAttribute(QKeyValue iter) + { + if (iter == null) return null; + iter.Next = RemoveLayerAttribute(iter.Next); + return (iter.Key == "layer") ? iter.Next : iter; + } + + public override Variable VisitVariable(Variable node) + { + node.Attributes = RemoveLayerAttribute(node.Attributes); + return base.VisitVariable(node); + } + + public override Procedure VisitProcedure(Procedure node) + { + node.Attributes = RemoveLayerAttribute(node.Attributes); + return base.VisitProcedure(node); + } + + public override Implementation VisitImplementation(Implementation node) + { + node.Attributes = RemoveLayerAttribute(node.Attributes); + return base.VisitImplementation(node); + } + + public override Requires VisitRequires(Requires node) + { + node.Attributes = RemoveLayerAttribute(node.Attributes); + return base.VisitRequires(node); + } + + public override Ensures VisitEnsures(Ensures node) + { + node.Attributes = RemoveLayerAttribute(node.Attributes); + return base.VisitEnsures(node); + } + + public override Cmd VisitAssertCmd(AssertCmd node) + { + node.Attributes = RemoveLayerAttribute(node.Attributes); + return base.VisitAssertCmd(node); + } + } + + public class LayerRange + { + public int lowerLayerNum; + public int upperLayerNum; + public LayerRange(int layer) + { + this.lowerLayerNum = layer; + this.upperLayerNum = layer; + } + public LayerRange(int lower, int upper) + { + this.lowerLayerNum = lower; + this.upperLayerNum = upper; + } + public LayerRange(IEnumerable layerNums) + { + int min = int.MaxValue; + int max = int.MinValue; + foreach (var layerNum in layerNums) + { + if (layerNum < min) + { + min = layerNum; + } + if (max < layerNum) + { + max = layerNum; + } + } + this.lowerLayerNum = min; + this.upperLayerNum = max; + } + public bool Contains(int layerNum) + { + return lowerLayerNum <= layerNum && layerNum <= upperLayerNum; + } + public bool Subset(int lower, int upper) + { + return lower <= lowerLayerNum && upperLayerNum <= upper; + } + public bool Equal(int lower, int upper) + { + return lower == lowerLayerNum && upperLayerNum == upper; + } + public bool Subset(LayerRange info) + { + return info.lowerLayerNum <= lowerLayerNum && upperLayerNum <= info.upperLayerNum; + } + } + + public class AtomicProcedureInfo + { + public bool isPure; + public HashSet layers; + public AtomicProcedureInfo() + { + this.isPure = true; + this.layers = null; + } + public AtomicProcedureInfo(HashSet layers) + { + this.isPure = false; + this.layers = layers; + } + } + + public class LocalVariableInfo + { + public bool isGhost; + public int layer; + public LocalVariableInfo(bool isGhost, int layer) + { + this.isGhost = isGhost; + this.layer = layer; + } + } + + public class CivlTypeChecker : ReadOnlyVisitor + { + CheckingContext checkingContext; + Procedure enclosingProc; + Implementation enclosingImpl; + HashSet sharedVarsAccessed; + int introducedLocalVarsUpperBound; + int ghostVarIntroLayerAllowed; + + public Program program; + public int errorCount; + public Dictionary globalVarToSharedVarInfo; + public Dictionary procToActionInfo; + public Dictionary procToAtomicProcedureInfo; + public Dictionary> absyToLayerNums; + public Dictionary localVarToLocalVariableInfo; + + public bool CallExists(CallCmd callCmd, int enclosingProcLayerNum, int layerNum) + { + Debug.Assert(procToAtomicProcedureInfo.ContainsKey(callCmd.Proc)); + var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc]; + if (callCmd.Proc.Modifies.Count > 0) + { + return enclosingProcLayerNum == layerNum; + } + if (callCmd.Outs.Count == 0) + { + return true; + } + var outputVar = callCmd.Outs[0].Decl; + var localVariableInfo = localVarToLocalVariableInfo[outputVar]; + if (localVariableInfo.isGhost) + { + return localVariableInfo.layer == layerNum; + } + if (atomicProcedureInfo.isPure) + { + return localVariableInfo.layer <= layerNum; + } + else + { + return enclosingProcLayerNum == layerNum; + } + } + + private static List FindLayers(QKeyValue kv) + { + List layers = new List(); + for (; kv != null; kv = kv.Next) + { + if (kv.Key != "layer") continue; + foreach (var o in kv.Params) + { + Expr e = o as Expr; + if (e == null) return null; + LiteralExpr l = e as LiteralExpr; + if (l == null) return null; + if (!l.isBigNum) return null; + layers.Add(l.asBigNum.ToIntSafe); + } + } + return layers; + } + + private static int Least(IEnumerable layerNums) + { + int least = int.MaxValue; + foreach (var layer in layerNums) + { + if (layer < least) + { + least = layer; + } + } + return least; + } + + private static MoverType GetMoverType(Ensures e) + { + if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic")) + return MoverType.Atomic; + if (QKeyValue.FindBoolAttribute(e.Attributes, "right")) + return MoverType.Right; + if (QKeyValue.FindBoolAttribute(e.Attributes, "left")) + return MoverType.Left; + if (QKeyValue.FindBoolAttribute(e.Attributes, "both")) + return MoverType.Both; + return MoverType.Top; + } + + public CivlTypeChecker(Program program) + { + this.errorCount = 0; + this.checkingContext = new CheckingContext(null); + this.program = program; + this.enclosingProc = null; + this.enclosingImpl = null; + this.sharedVarsAccessed = null; + this.introducedLocalVarsUpperBound = int.MinValue; + this.ghostVarIntroLayerAllowed = int.MinValue; + + this.localVarToLocalVariableInfo = new Dictionary(); + this.absyToLayerNums = new Dictionary>(); + this.globalVarToSharedVarInfo = new Dictionary(); + this.procToActionInfo = new Dictionary(); + this.procToAtomicProcedureInfo = new Dictionary(); + + foreach (var g in program.GlobalVariables) + { + List layerNums = FindLayers(g.Attributes); + if (layerNums.Count == 0) + { + // Inaccessible from yielding and atomic procedures + } + else if (layerNums.Count == 1) + { + this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue); + } + else if (layerNums.Count == 2) + { + this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]); + } + else + { + Error(g, "Too many layer numbers"); + } + } + } + + private HashSet allImplementedLayerNums; + public IEnumerable AllImplementedLayerNums + { + get + { + if (allImplementedLayerNums == null) + { + allImplementedLayerNums = new HashSet(); + foreach (ActionInfo actionInfo in procToActionInfo.Values) + { + if (actionInfo.hasImplementation) + { + allImplementedLayerNums.Add(actionInfo.createdAtLayerNum); + } + } + } + return allImplementedLayerNums; + } + } + + private HashSet allCreatedLayerNums; + public IEnumerable AllCreatedLayerNums + { + get + { + if (allCreatedLayerNums == null) + { + allCreatedLayerNums = new HashSet(); + foreach (ActionInfo actionInfo in procToActionInfo.Values) + { + allCreatedLayerNums.Add(actionInfo.createdAtLayerNum); + } + } + return allCreatedLayerNums; + } + } + + private LayerRange FindLayerRange() + { + int maxIntroLayerNum = int.MinValue; + int minHideLayerNum = int.MaxValue; + foreach (var g in sharedVarsAccessed) + { + if (globalVarToSharedVarInfo[g].introLayerNum > maxIntroLayerNum) + { + maxIntroLayerNum = globalVarToSharedVarInfo[g].introLayerNum; + } + if (globalVarToSharedVarInfo[g].hideLayerNum < minHideLayerNum) + { + minHideLayerNum = globalVarToSharedVarInfo[g].hideLayerNum; + } + } + return new LayerRange(maxIntroLayerNum, minHideLayerNum); + } + + public void TypeCheck() + { + foreach (var proc in program.Procedures) + { + if (!QKeyValue.FindBoolAttribute(proc.Attributes, "pure")) continue; + if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) + { + Error(proc, "Pure procedure must not yield"); + continue; + } + if (QKeyValue.FindBoolAttribute(proc.Attributes, "layer")) + { + Error(proc, "Pure procedure must not have layers"); + continue; + } + if (proc.Modifies.Count > 0) + { + Error(proc, "Pure procedure must not modify a global variable"); + continue; + } + procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(); + } + foreach (var proc in program.Procedures) + { + if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue; + var procLayerNums = RemoveDuplicatesAndSort(FindLayers(proc.Attributes)); + if (procLayerNums.Count == 0) continue; + foreach (IdentifierExpr ie in proc.Modifies) + { + if (!globalVarToSharedVarInfo.ContainsKey(ie.Decl)) + { + Error(proc, "Atomic procedure cannot modify a global variable without layer numbers"); + } + else if (globalVarToSharedVarInfo[ie.Decl].introLayerNum != procLayerNums[0]) + { + Error(proc, "The introduction layer of a modified global variable must be identical to the layer of the atomic procedure"); + } + } + if (proc.Modifies.Count == 0 || procLayerNums.Count == 1) + { + procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(new HashSet(procLayerNums)); + } + else + { + Error(proc, "An atomic procedure with more than one layer must not modify a global variable"); + } + } + if (errorCount > 0) return; + + foreach (Implementation impl in program.Implementations) + { + if (!procToAtomicProcedureInfo.ContainsKey(impl.Proc)) continue; + var atomicProcedureInfo = procToAtomicProcedureInfo[impl.Proc]; + if (atomicProcedureInfo.isPure) + { + this.enclosingImpl = impl; + (new PurityChecker(this)).VisitImplementation(impl); + } + else + { + this.enclosingImpl = impl; + this.sharedVarsAccessed = new HashSet(); + (new PurityChecker(this)).VisitImplementation(impl); + LayerRange upperBound = FindLayerRange(); + LayerRange lowerBound = new LayerRange(atomicProcedureInfo.layers); + if (!lowerBound.Subset(upperBound)) + { + Error(impl, "Atomic procedure cannot access global variable"); + } + this.sharedVarsAccessed = null; + } + } + if (errorCount > 0) return; + + foreach (var proc in program.Procedures) + { + if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue; + + int createdAtLayerNum; // must be initialized by the following code, otherwise it is an error + int availableUptoLayerNum = int.MaxValue; + List attrs = FindLayers(proc.Attributes); + if (attrs.Count == 1) + { + createdAtLayerNum = attrs[0]; + } + else if (attrs.Count == 2) + { + createdAtLayerNum = attrs[0]; + availableUptoLayerNum = attrs[1]; + } + else + { + Error(proc, "Incorrect number of layers"); + continue; + } + foreach (Ensures e in proc.Ensures) + { + MoverType moverType = GetMoverType(e); + if (moverType == MoverType.Top) continue; + CodeExpr codeExpr = e.Condition as CodeExpr; + if (codeExpr == null) + { + Error(e, "An atomic action must be a CodeExpr"); + continue; + } + if (procToActionInfo.ContainsKey(proc)) + { + Error(proc, "A procedure can have at most one atomic action"); + continue; + } + if (availableUptoLayerNum <= createdAtLayerNum) + { + Error(proc, "Creation layer number must be less than the available upto layer number"); + continue; + } + + sharedVarsAccessed = new HashSet(); + enclosingProc = proc; + enclosingImpl = null; + base.VisitEnsures(e); + LayerRange upperBound = FindLayerRange(); + LayerRange lowerBound = new LayerRange(createdAtLayerNum, availableUptoLayerNum); + if (lowerBound.Subset(upperBound)) + { + procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum); + } + else + { + Error(e, "A variable being accessed in this action is unavailable"); + } + sharedVarsAccessed = null; + } + if (errorCount > 0) continue; + if (!procToActionInfo.ContainsKey(proc)) + { + if (availableUptoLayerNum < createdAtLayerNum) + { + Error(proc, "Creation layer number must be no more than the available upto layer number"); + continue; + } + else + { + procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum); + } + } + } + if (errorCount > 0) return; + foreach (Implementation node in program.Implementations) + { + if (!procToActionInfo.ContainsKey(node.Proc)) continue; + foreach (Variable v in node.LocVars) + { + var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum); + if (layer == int.MinValue) continue; + localVarToLocalVariableInfo[v] = new LocalVariableInfo(QKeyValue.FindBoolAttribute(node.Attributes, "ghost"), layer); + } + for (int i = 0; i < node.Proc.InParams.Count; i++) + { + Variable v = node.Proc.InParams[i]; + var layer = FindLocalVariableLayer(node.Proc, v, procToActionInfo[node.Proc].createdAtLayerNum); + if (layer == int.MinValue) continue; + localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer); + localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(false, layer); + } + for (int i = 0; i < node.Proc.OutParams.Count; i++) + { + Variable v = node.Proc.OutParams[i]; + var layer = FindLocalVariableLayer(node.Proc, v, procToActionInfo[node.Proc].createdAtLayerNum); + if (layer == int.MinValue) continue; + localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer); + localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(false, layer); + } + } + if (errorCount > 0) return; + foreach (var impl in program.Implementations) + { + if (!procToActionInfo.ContainsKey(impl.Proc)) continue; + ActionInfo actionInfo = procToActionInfo[impl.Proc]; + procToActionInfo[impl.Proc].hasImplementation = true; + if (actionInfo.isExtern) + { + Error(impl.Proc, "Extern procedure cannot have an implementation"); + } + } + foreach (var g in this.globalVarToSharedVarInfo.Keys) + { + var info = globalVarToSharedVarInfo[g]; + if (!this.AllCreatedLayerNums.Contains(info.introLayerNum)) + { + Error(g, "Variable must be introduced with creation of some atomic action"); + } + if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum)) + { + Error(g, "Variable must be hidden with creation of some atomic action"); + } + } + if (errorCount > 0) return; + this.VisitProgram(program); + if (errorCount > 0) return; + YieldTypeChecker.PerformYieldSafeCheck(this); + new LayerEraser().VisitProgram(program); + } + + public IEnumerable SharedVariables + { + get { return this.globalVarToSharedVarInfo.Keys; } + } + + private int FindLocalVariableLayer(Declaration decl, Variable v, int enclosingProcLayerNum) + { + var layers = FindLayers(v.Attributes); + if (layers.Count == 0) return int.MinValue; + if (layers.Count > 1) + { + Error(decl, "Incorrect number of layers"); + return int.MinValue; + } + if (layers[0] > enclosingProcLayerNum) + { + Error(decl, "Layer of local variable cannot be greater than the creation layer of enclosing procedure"); + return int.MinValue; + } + return layers[0]; + } + + public override Implementation VisitImplementation(Implementation node) + { + if (!procToActionInfo.ContainsKey(node.Proc)) + { + return node; + } + this.enclosingImpl = node; + this.enclosingProc = null; + return base.VisitImplementation(node); + } + + public override Procedure VisitProcedure(Procedure node) + { + if (!procToActionInfo.ContainsKey(node)) + { + return node; + } + this.enclosingProc = node; + this.enclosingImpl = null; + return base.VisitProcedure(node); + } + + public override Cmd VisitCallCmd(CallCmd node) + { + int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; + if (procToActionInfo.ContainsKey(node.Proc)) + { + ActionInfo actionInfo = procToActionInfo[node.Proc]; + if (node.IsAsync && actionInfo is AtomicActionInfo) + { + Error(node, "Target of async call cannot be an atomic action"); + } + int calleeLayerNum = procToActionInfo[node.Proc].createdAtLayerNum; + if (enclosingProcLayerNum < calleeLayerNum || + (enclosingProcLayerNum == calleeLayerNum && actionInfo is AtomicActionInfo)) + { + Error(node, "The layer of the caller must be greater than the layer of the callee"); + } + else if (enclosingProcLayerNum == calleeLayerNum && enclosingImpl.OutParams.Count > 0) + { + HashSet outParams = new HashSet(enclosingImpl.OutParams); + foreach (var x in node.Outs) + { + if (x.Decl is GlobalVariable) + { + Error(node, "A global variable cannot be used as output argument for this call"); + } + else if (outParams.Contains(x.Decl)) + { + Error(node, "An output variable of the enclosing implementation cannot be used as output argument for this call"); + } + } + } + if (actionInfo.availableUptoLayerNum < enclosingProcLayerNum) + { + Error(node, "The callee is not available in the caller procedure"); + } + for (int i = 0; i < node.Ins.Count; i++) + { + var formal = node.Proc.InParams[i]; + if (localVarToLocalVariableInfo.ContainsKey(formal)) + { + introducedLocalVarsUpperBound = localVarToLocalVariableInfo[formal].layer; + } + Visit(node.Ins[i]); + introducedLocalVarsUpperBound = int.MinValue; + } + for (int i = 0; i < node.Outs.Count; i++) + { + var formal = node.Proc.OutParams[i]; + if (!localVarToLocalVariableInfo.ContainsKey(formal)) continue; + var actual = node.Outs[i].Decl; + if (localVarToLocalVariableInfo.ContainsKey(actual) && + localVarToLocalVariableInfo[formal].layer <= localVarToLocalVariableInfo[actual].layer) + continue; + Error(node, "Formal parameter of call must be introduced no later than the actual parameter"); + } + return node; + } + else if (procToAtomicProcedureInfo.ContainsKey(node.Proc)) + { + // 1. Outputs are either all ghost or all introduced. + // 2. All outputs have the same layer; call it output layer. + // 3. If callee is impure and has outputs, output layer is a member of layer set of callee. + // 4. If callee is impure and has introduced outputs, then creation number of caller belongs to layer set of callee. + // 5. If callee is impure and modifies globals, then creation number of caller belongs to layer set of callee. + + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + bool isGhost = false; // This assignment stops the compiler from complaining. + // In the absence of errors, isGhost is initialized by loop below. + foreach (var ie in node.Outs) + { + if (localVarToLocalVariableInfo.ContainsKey(ie.Decl)) + { + var localVariableInfo = localVarToLocalVariableInfo[ie.Decl]; + if (introducedLocalVarsUpperBound == int.MinValue) + { + introducedLocalVarsUpperBound = localVariableInfo.layer; + isGhost = localVariableInfo.isGhost; + var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc]; + if (!atomicProcedureInfo.isPure) + { + if (!atomicProcedureInfo.layers.Contains(introducedLocalVarsUpperBound)) + { + Error(node, "Layer of output variable must be a layer of the callee"); + } + if (!isGhost && !atomicProcedureInfo.layers.Contains(enclosingProcLayerNum)) + { + Error(node, "The creation layer of caller must be a layer of the callee"); + } + } + } + else + { + if (localVariableInfo.layer != introducedLocalVarsUpperBound) + { + Error(node, "All outputs must have the same layer"); + } + if (localVariableInfo.isGhost != isGhost) + { + Error(node, "Outputs are either all ghost or all introduced"); + } + } + } + else + { + Error(node, "Output variable must be a ghost or introduced local variable"); + } + } + + if (node.Proc.Modifies.Count > 0) + { + var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc]; + if (procToActionInfo[enclosingImpl.Proc] is AtomicActionInfo) + { + if (!atomicProcedureInfo.layers.Contains(enclosingProcLayerNum)) + { + Error(node, "The layer of called atomic procedure must be identical to the creation layer of callee"); + } + } + else + { + Error(node, "Enclosing implementation must refine an atomic action"); + } + introducedLocalVarsUpperBound = enclosingProcLayerNum; + } + foreach (var e in node.Ins) + { + Visit(e); + } + introducedLocalVarsUpperBound = int.MinValue; + return node; + } + else + { + Error(node, "A yielding procedure can call only atomic or yielding procedures"); + return node; + } + } + + public override Cmd VisitParCallCmd(ParCallCmd node) + { + int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; + bool isLeftMover = true; + bool isRightMover = true; + int maxCalleeLayerNum = 0; + int atomicActionCalleeLayerNum = 0; + int numAtomicActions = 0; + foreach (CallCmd iter in node.CallCmds) + { + ActionInfo actionInfo = procToActionInfo[iter.Proc]; + isLeftMover = isLeftMover && actionInfo.IsLeftMover; + isRightMover = isRightMover && actionInfo.IsRightMover; + if (actionInfo.createdAtLayerNum > maxCalleeLayerNum) + { + maxCalleeLayerNum = actionInfo.createdAtLayerNum; + } + if (actionInfo is AtomicActionInfo) + { + numAtomicActions++; + if (atomicActionCalleeLayerNum == 0) + { + atomicActionCalleeLayerNum = actionInfo.createdAtLayerNum; + } + else if (atomicActionCalleeLayerNum != actionInfo.createdAtLayerNum) + { + Error(node, "All atomic actions must be introduced at the same layer"); + } + } + } + if (numAtomicActions > 1 && !isLeftMover && !isRightMover) + { + Error(node, "The atomic actions in the parallel call must be all right movers or all left movers"); + } + if (0 < atomicActionCalleeLayerNum && atomicActionCalleeLayerNum < maxCalleeLayerNum) + { + Error(node, "Atomic actions must be introduced at the highest layer"); + } + return base.VisitParCallCmd(node); + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + if (node.Decl is GlobalVariable) + { + if (sharedVarsAccessed == null) + { + Error(node, "Shared variable can be accessed only in atomic actions or specifications"); + } + else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl)) + { + sharedVarsAccessed.Add(node.Decl); + } + else + { + Error(node, "Accessed shared variable must have layer annotation"); + } + } + else if ((node.Decl is Formal || node.Decl is Variable) && localVarToLocalVariableInfo.ContainsKey(node.Decl)) + { + var localVariableInfo = localVarToLocalVariableInfo[node.Decl]; + if (localVariableInfo.isGhost) + { + if (ghostVarIntroLayerAllowed != localVariableInfo.layer) + { + Error(node, "Ghost variable inaccessible"); + } + } + else + { + if (introducedLocalVarsUpperBound < localVariableInfo.layer) + { + Error(node, "Introduced variable inaccessible"); + } + } + } + return base.VisitIdentifierExpr(node); + } + + public override Ensures VisitEnsures(Ensures ensures) + { + ActionInfo actionInfo = procToActionInfo[enclosingProc]; + AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; + if (atomicActionInfo != null && atomicActionInfo.ensures == ensures) + { + // This case has already been checked + } + else + { + sharedVarsAccessed = new HashSet(); + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + introducedLocalVarsUpperBound = Least(FindLayers(ensures.Attributes)); + base.VisitEnsures(ensures); + CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum); + introducedLocalVarsUpperBound = int.MinValue; + sharedVarsAccessed = null; + } + return ensures; + } + + public override Requires VisitRequires(Requires requires) + { + sharedVarsAccessed = new HashSet(); + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + introducedLocalVarsUpperBound = Least(FindLayers(requires.Attributes)); + base.VisitRequires(requires); + CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum); + introducedLocalVarsUpperBound = int.MinValue; + sharedVarsAccessed = null; + return requires; + } + + public override Cmd VisitAssertCmd(AssertCmd node) + { + if (enclosingImpl == null) + { + // in this case, we are visiting an assert inside a CodeExpr + return base.VisitAssertCmd(node); + } + sharedVarsAccessed = new HashSet(); + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + var layerNums = FindLayers(node.Attributes); + introducedLocalVarsUpperBound = Least(layerNums); + if (layerNums.Count == 1) + { + ghostVarIntroLayerAllowed = layerNums[0]; + } + base.VisitAssertCmd(node); + CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum); + introducedLocalVarsUpperBound = int.MinValue; + ghostVarIntroLayerAllowed = int.MinValue; + sharedVarsAccessed = null; + return node; + } + + private List RemoveDuplicatesAndSort(List attrs) + { + HashSet layerSet = new HashSet(attrs); + List layers = new List(layerSet); + layers.Sort(); + return layers; + } + + private void CheckAndAddLayers(Absy node, QKeyValue attributes, int enclosingProcLayerNum) + { + List attrs = RemoveDuplicatesAndSort(FindLayers(attributes)); + if (attrs.Count == 0) + { + Error(node, "layer not present"); + return; + } + LayerRange upperBound = FindLayerRange(); + absyToLayerNums[node] = new HashSet(); + foreach (int layerNum in attrs) + { + if (layerNum > enclosingProcLayerNum) + { + Error(node, "The layer cannot be greater than the layer of enclosing procedure"); + } + else if (upperBound.Contains(layerNum)) + { + absyToLayerNums[node].Add(layerNum); + } + else + { + Error(node, string.Format("A variable being accessed in this specification is unavailable at layer {0}", layerNum)); + } + } + } + + public void Error(Absy node, string message) + { + checkingContext.Error(node, message); + errorCount++; + } + + private class PurityChecker : StandardVisitor + { + private CivlTypeChecker civlTypeChecker; + + public PurityChecker(CivlTypeChecker civlTypeChecker) + { + this.civlTypeChecker = civlTypeChecker; + } + + public override Cmd VisitCallCmd(CallCmd node) + { + Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc; + if (!civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc)) + { + civlTypeChecker.Error(node, "Atomic procedure can only call an atomic procedure"); + return base.VisitCallCmd(node); + } + var callerInfo = civlTypeChecker.procToAtomicProcedureInfo[enclosingProc]; + var calleeInfo = civlTypeChecker.procToAtomicProcedureInfo[node.Proc]; + if (calleeInfo.isPure) + { + // do nothing + } + else if (callerInfo.isPure) + { + civlTypeChecker.Error(node, "Pure procedure can only call pure procedures"); + } + else if (!callerInfo.layers.IsSubsetOf(calleeInfo.layers)) + { + civlTypeChecker.Error(node, "Caller layers must be subset of callee layers"); + } + return base.VisitCallCmd(node); + } + + public override Cmd VisitParCallCmd(ParCallCmd node) + { + civlTypeChecker.Error(node, "Atomic procedures cannot make parallel calls"); + return node; + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc; + if (node.Decl is GlobalVariable) + { + if (civlTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure) + { + civlTypeChecker.Error(node, "Pure procedure cannot access global variables"); + } + else if (!civlTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl)) + { + civlTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers"); + } + else + { + civlTypeChecker.sharedVarsAccessed.Add(node.Decl); + } + } + return node; + } + } + } +} diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj index f15ebca3..113019fd 100644 --- a/Source/Concurrency/Concurrency.csproj +++ b/Source/Concurrency/Concurrency.csproj @@ -1,4 +1,4 @@ - + @@ -73,11 +73,11 @@ - + - + @@ -112,4 +112,4 @@ --> - \ No newline at end of file + diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 7c6d4ac4..732bcaa4 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -10,29 +10,29 @@ namespace Microsoft.Boogie public class MoverCheck { LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; List decls; HashSet> commutativityCheckerCache; HashSet> gatePreservationCheckerCache; HashSet> failurePreservationCheckerCache; - private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) + private MoverCheck(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List decls) { this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.decls = decls; this.commutativityCheckerCache = new HashSet>(); this.gatePreservationCheckerCache = new HashSet>(); this.failurePreservationCheckerCache = new HashSet>(); } - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) + public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List decls) { - if (moverTypeChecker.procToActionInfo.Count == 0) + if (civlTypeChecker.procToActionInfo.Count == 0) return; - List sortedByCreatedLayerNum = new List(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + List sortedByCreatedLayerNum = new List(civlTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; }); - List sortedByAvailableUptoLayerNum = new List(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + List sortedByAvailableUptoLayerNum = new List(civlTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; }); Dictionary> pools = new Dictionary>(); @@ -60,8 +60,8 @@ namespace Microsoft.Boogie currPool = pools[currLayerNum]; } - Program program = moverTypeChecker.program; - MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls); + Program program = civlTypeChecker.program; + MoverCheck moverChecking = new MoverCheck(linearTypeChecker, civlTypeChecker, decls); foreach (int layerNum in pools.Keys) { foreach (AtomicActionInfo first in pools[layerNum]) @@ -537,7 +537,7 @@ namespace Microsoft.Boogie ensures.Add(ensureCheck); string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name); List globalVars = new List(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, outputs, locals, blocks); impl.Proc = proc; @@ -580,7 +580,7 @@ namespace Microsoft.Boogie requires.Add(new Requires(false, assertCmd.Expr)); string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); List globalVars = new List(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, outputs, locals, secondBlocks); impl.Proc = proc; @@ -628,7 +628,7 @@ namespace Microsoft.Boogie requires.Add(new Requires(false, assertCmd.Expr)); string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); List globalVars = new List(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, outputs, locals, secondBlocks); impl.Proc = proc; @@ -662,7 +662,7 @@ namespace Microsoft.Boogie blocks.Add(new Block(Token.NoToken, "L", new List(), new ReturnCmd(Token.NoToken))); string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name); List globalVars = new List(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, new List(), requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, new List(), new List(), blocks); impl.Proc = proc; diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs deleted file mode 100644 index d861e2f3..00000000 --- a/Source/Concurrency/OwickiGries.cs +++ /dev/null @@ -1,1240 +0,0 @@ -using System; -using System.Collections; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Threading.Tasks; -using Microsoft.Boogie; -using System.Diagnostics; -using System.Diagnostics.Contracts; -using Microsoft.Boogie.GraphUtil; - -namespace Microsoft.Boogie -{ - public class MyDuplicator : Duplicator - { - MoverTypeChecker moverTypeChecker; - public int layerNum; - Procedure enclosingProc; - Implementation enclosingImpl; - public Dictionary procMap; /* Original -> Duplicate */ - public Dictionary absyMap; /* Duplicate -> Original */ - public Dictionary implMap; /* Duplicate -> Original */ - public HashSet yieldingProcs; - public List impls; - - public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum) - { - this.moverTypeChecker = moverTypeChecker; - this.layerNum = layerNum; - this.enclosingProc = null; - this.enclosingImpl = null; - this.procMap = new Dictionary(); - this.absyMap = new Dictionary(); - this.implMap = new Dictionary(); - this.yieldingProcs = new HashSet(); - this.impls = new List(); - } - - private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List newCmds) - { - int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; - Procedure originalProc = originalCallCmd.Proc; - - if (moverTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc)) - { - if (moverTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum)) - { - newCmds.Add(callCmd); - } - } - else if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc)) - { - AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo; - if (atomicActionInfo != null && atomicActionInfo.gate.Count > 0 && layerNum == enclosingProcLayerNum) - { - newCmds.Add(new HavocCmd(Token.NoToken, new List(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) }))); - Dictionary map = new Dictionary(); - for (int i = 0; i < originalProc.InParams.Count; i++) - { - map[originalProc.InParams[i]] = callCmd.Ins[i]; - } - Substitution subst = Substituter.SubstitutionFromHashtable(map); - foreach (AssertCmd assertCmd in atomicActionInfo.gate) - { - newCmds.Add(Substituter.Apply(subst, assertCmd)); - } - } - newCmds.Add(callCmd); - } - else - { - Debug.Assert(false); - } - } - - private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List newCmds) - { - int maxCalleeLayerNum = 0; - foreach (CallCmd iter in originalParCallCmd.CallCmds) - { - int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum; - if (calleeLayerNum > maxCalleeLayerNum) - maxCalleeLayerNum = calleeLayerNum; - } - if (layerNum > maxCalleeLayerNum) - { - for (int i = 0; i < parCallCmd.CallCmds.Count; i++) - { - ProcessCallCmd(originalParCallCmd.CallCmds[i], parCallCmd.CallCmds[i], newCmds); - absyMap[parCallCmd.CallCmds[i]] = originalParCallCmd; - } - } - else - { - newCmds.Add(parCallCmd); - } - } - - public override List VisitCmdSeq(List cmdSeq) - { - List cmds = base.VisitCmdSeq(cmdSeq); - List newCmds = new List(); - for (int i = 0; i < cmds.Count; i++) - { - Cmd originalCmd = cmdSeq[i]; - Cmd cmd = cmds[i]; - - CallCmd originalCallCmd = originalCmd as CallCmd; - if (originalCallCmd != null) - { - ProcessCallCmd(originalCallCmd, cmd as CallCmd, newCmds); - continue; - } - - ParCallCmd originalParCallCmd = originalCmd as ParCallCmd; - if (originalParCallCmd != null) - { - ProcessParCallCmd(originalParCallCmd, cmd as ParCallCmd, newCmds); - continue; - } - - newCmds.Add(cmd); - } - return newCmds; - } - - public override YieldCmd VisitYieldCmd(YieldCmd node) - { - YieldCmd yieldCmd = base.VisitYieldCmd(node); - absyMap[yieldCmd] = node; - return yieldCmd; - } - - public override Block VisitBlock(Block node) - { - Block block = base.VisitBlock(node); - absyMap[block] = node; - return block; - } - - public override Cmd VisitCallCmd(CallCmd node) - { - CallCmd callCmd = (CallCmd) base.VisitCallCmd(node); - callCmd.Proc = VisitProcedure(callCmd.Proc); - callCmd.callee = callCmd.Proc.Name; - absyMap[callCmd] = node; - return callCmd; - } - - public override Cmd VisitParCallCmd(ParCallCmd node) - { - ParCallCmd parCallCmd = (ParCallCmd) base.VisitParCallCmd(node); - absyMap[parCallCmd] = node; - return parCallCmd; - } - - public override Procedure VisitProcedure(Procedure node) - { - if (!moverTypeChecker.procToActionInfo.ContainsKey(node)) - return node; - if (!procMap.ContainsKey(node)) - { - enclosingProc = node; - Procedure proc = (Procedure)node.Clone(); - proc.Name = string.Format("{0}_{1}", node.Name, layerNum); - proc.InParams = this.VisitVariableSeq(node.InParams); - proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies); - proc.OutParams = this.VisitVariableSeq(node.OutParams); - - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node]; - if (actionInfo.createdAtLayerNum < layerNum) - { - proc.Requires = new List(); - proc.Ensures = new List(); - Implementation impl; - AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; - if (atomicActionInfo != null) - { - CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.action); - List cmds = new List(); - foreach (AssertCmd assertCmd in atomicActionInfo.gate) - { - cmds.Add(new AssumeCmd(Token.NoToken, (Expr)Visit(assertCmd.Expr))); - } - Block newInitBlock = new Block(Token.NoToken, "_init", cmds, - new GotoCmd(Token.NoToken, new List(new string[] { action.Blocks[0].Label }), - new List(new Block[] { action.Blocks[0] }))); - List newBlocks = new List(); - newBlocks.Add(newInitBlock); - newBlocks.AddRange(action.Blocks); - impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks); - } - else - { - Block newInitBlock = new Block(Token.NoToken, "_init", new List(), new ReturnCmd(Token.NoToken)); - List newBlocks = new List(); - newBlocks.Add(newInitBlock); - impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List(), newBlocks); - } - impl.Proc = proc; - impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - impls.Add(impl); - } - else - { - yieldingProcs.Add(proc); - proc.Requires = this.VisitRequiresSeq(node.Requires); - proc.Ensures = this.VisitEnsuresSeq(node.Ensures); - } - procMap[node] = proc; - proc.Modifies = new List(); - moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x))); - } - return procMap[node]; - } - - private Variable dummyLocalVar; - public override Implementation VisitImplementation(Implementation node) - { - enclosingImpl = node; - dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool)); - Implementation impl = base.VisitImplementation(node); - implMap[impl] = node; - impl.LocVars.Add(dummyLocalVar); - impl.Name = impl.Proc.Name; - return impl; - } - - public override Requires VisitRequires(Requires node) - { - Requires requires = base.VisitRequires(node); - if (node.Free) - return requires; - if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) - requires.Condition = Expr.True; - return requires; - } - - public override Ensures VisitEnsures(Ensures node) - { - Ensures ensures = base.VisitEnsures(node); - if (node.Free) - return ensures; - AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo; - bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node; - if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) - { - ensures.Condition = Expr.True; - ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes); - } - return ensures; - } - - public override Cmd VisitAssertCmd(AssertCmd node) - { - AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node); - if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) - assertCmd.Expr = Expr.True; - return assertCmd; - } - } - - public class OwickiGries - { - LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; - Dictionary absyMap; - Dictionary implMap; - HashSet yieldingProcs; - int layerNum; - List globalMods; - Dictionary asyncAndParallelCallDesugarings; - List yieldCheckerProcs; - List yieldCheckerImpls; - Procedure yieldProc; - - Variable pc; - Variable ok; - Expr alpha; - Expr beta; - HashSet frame; - - public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator) - { - this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; - this.absyMap = duplicator.absyMap; - this.layerNum = duplicator.layerNum; - this.implMap = duplicator.implMap; - this.yieldingProcs = duplicator.yieldingProcs; - Program program = linearTypeChecker.program; - globalMods = new List(); - foreach (Variable g in moverTypeChecker.SharedVariables) - { - globalMods.Add(Expr.Ident(g)); - } - asyncAndParallelCallDesugarings = new Dictionary(); - yieldCheckerProcs = new List(); - yieldCheckerImpls = new List(); - yieldProc = null; - } - - private IEnumerable AvailableLinearVars(Absy absy) - { - HashSet availableVars = new HashSet(linearTypeChecker.AvailableLinearVars(absyMap[absy])); - foreach (var g in moverTypeChecker.globalVarToSharedVarInfo.Keys) - { - SharedVariableInfo info = moverTypeChecker.globalVarToSharedVarInfo[g]; - if (!(info.introLayerNum <= layerNum && layerNum <= info.hideLayerNum)) - { - availableVars.Remove(g); - } - } - foreach (var v in moverTypeChecker.localVarToLocalVariableInfo.Keys) - { - LocalVariableInfo info = moverTypeChecker.localVarToLocalVariableInfo[v]; - if (info.isGhost) - { - if (info.layer != layerNum) - { - availableVars.Remove(v); - } - } - else - { - if (layerNum < info.layer) - { - availableVars.Remove(v); - } - } - } - return availableVars; - } - - private CallCmd CallToYieldProc(IToken tok, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) - { - List exprSeq = new List(); - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName])); - } - foreach (IdentifierExpr ie in globalMods) - { - exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl])); - } - if (yieldProc == null) - { - List inputs = new List(); - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - var domain = linearTypeChecker.linearDomains[domainName]; - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true); - inputs.Add(f); - } - foreach (IdentifierExpr ie in globalMods) - { - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); - inputs.Add(f); - } - yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", layerNum), new List(), inputs, new List(), new List(), new List(), new List()); - yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - } - CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List()); - yieldCallCmd.Proc = yieldProc; - return yieldCallCmd; - } - - private void AddCallToYieldProc(IToken tok, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) - { - if (!CommandLineOptions.Clo.TrustNonInterference) - { - CallCmd yieldCallCmd = CallToYieldProc(tok, ogOldGlobalMap, domainNameToLocalVar); - newCmds.Add(yieldCallCmd); - } - - if (pc != null) - { - Expr aa = OldEqualityExprForGlobals(ogOldGlobalMap); - Expr bb = OldEqualityExpr(ogOldGlobalMap); - - // assert pc || g_old == g || beta(i, g_old, o, g); - Expr assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta)); - assertExpr.Typecheck(new TypecheckingContext(null)); - AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, assertExpr); - skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated"; - newCmds.Add(skipOrBetaAssertCmd); - - // assert pc ==> o_old == o && g_old == g; - assertExpr = Expr.Imp(Expr.Ident(pc), bb); - assertExpr.Typecheck(new TypecheckingContext(null)); - AssertCmd skipAssertCmd = new AssertCmd(tok, assertExpr); - skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ; - newCmds.Add(skipAssertCmd); - - // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g); - List pcUpdateLHS = new List( - new AssignLhs[] { - new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)), - new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)) - }); - List pcUpdateRHS = new List( - new Expr[] { - Expr.Imp(aa, Expr.Ident(pc)), - Expr.Or(Expr.Ident(ok), beta) - }); - foreach (Expr e in pcUpdateRHS) - { - e.Typecheck(new TypecheckingContext(null)); - } - newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS)); - } - } - - private Dictionary ComputeAvailableExprs(IEnumerable availableLinearVars, Dictionary domainNameToInputVar) - { - Dictionary domainNameToExpr = new Dictionary(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - var expr = Expr.Ident(domainNameToInputVar[domainName]); - expr.Resolve(new ResolutionContext(null)); - expr.Typecheck(new TypecheckingContext(null)); - domainNameToExpr[domainName] = expr; - } - foreach (Variable v in availableLinearVars) - { - var domainName = linearTypeChecker.FindDomainName(v); - if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; - var domain = linearTypeChecker.linearDomains[domainName]; - if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue; - Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List { Expr.Ident(v) }); - var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { ie, domainNameToExpr[domainName] }); - expr.Resolve(new ResolutionContext(null)); - expr.Typecheck(new TypecheckingContext(null)); - domainNameToExpr[domainName] = expr; - } - return domainNameToExpr; - } - - private void AddUpdatesToOldGlobalVars(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar, Dictionary domainNameToExpr) - { - List lhss = new List(); - List rhss = new List(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName]))); - rhss.Add(domainNameToExpr[domainName]); - } - foreach (Variable g in ogOldGlobalMap.Keys) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); - rhss.Add(Expr.Ident(g)); - } - if (lhss.Count > 0) - { - newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); - } - } - - private Expr OldEqualityExpr(Dictionary ogOldGlobalMap) - { - Expr bb = Expr.True; - foreach (Variable o in ogOldGlobalMap.Keys) - { - if (o is GlobalVariable && !frame.Contains(o)) continue; - bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); - bb.Type = Type.Bool; - } - return bb; - } - - private Expr OldEqualityExprForGlobals(Dictionary ogOldGlobalMap) - { - Expr bb = Expr.True; - foreach (Variable o in ogOldGlobalMap.Keys) - { - if (o is GlobalVariable && frame.Contains(o)) - { - bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); - bb.Type = Type.Bool; - } - } - return bb; - } - - private void DesugarYield(YieldCmd yieldCmd, List cmds, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar) - { - AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); - - if (globalMods.Count > 0) - { - newCmds.Add(new HavocCmd(Token.NoToken, globalMods)); - if (pc != null) - { - // assume pc || alpha(i, g); - Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha); - assumeExpr.Type = Type.Bool; - newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr)); - } - } - - Dictionary domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(yieldCmd), domainNameToInputVar); - AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); - - for (int j = 0; j < cmds.Count; j++) - { - PredicateCmd predCmd = (PredicateCmd)cmds[j]; - newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr)); - } - } - - public void DesugarParallelCallCmd(List newCmds, ParCallCmd parCallCmd) - { - List parallelCalleeNames = new List(); - List ins = new List(); - List outs = new List(); - string procName = "og"; - foreach (CallCmd callCmd in parCallCmd.CallCmds) - { - procName = procName + "_" + callCmd.Proc.Name; - ins.AddRange(callCmd.Ins); - outs.AddRange(callCmd.Outs); - } - Procedure proc; - if (asyncAndParallelCallDesugarings.ContainsKey(procName)) - { - proc = asyncAndParallelCallDesugarings[procName]; - } - else - { - List inParams = new List(); - List outParams = new List(); - List requiresSeq = new List(); - List ensuresSeq = new List(); - int count = 0; - foreach (CallCmd callCmd in parCallCmd.CallCmds) - { - Dictionary map = new Dictionary(); - foreach (Variable x in callCmd.Proc.InParams) - { - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), true); - inParams.Add(y); - map[x] = Expr.Ident(y); - } - foreach (Variable x in callCmd.Proc.OutParams) - { - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), false); - outParams.Add(y); - map[x] = Expr.Ident(y); - } - Contract.Assume(callCmd.Proc.TypeParameters.Count == 0); - Substitution subst = Substituter.SubstitutionFromHashtable(map); - foreach (Requires req in callCmd.Proc.Requires) - { - requiresSeq.Add(new Requires(req.tok, req.Free, Substituter.Apply(subst, req.Condition), null, req.Attributes)); - } - foreach (Ensures ens in callCmd.Proc.Ensures) - { - ensuresSeq.Add(new Ensures(ens.tok, ens.Free, Substituter.Apply(subst, ens.Condition), null, ens.Attributes)); - } - count++; - } - proc = new Procedure(Token.NoToken, procName, new List(), inParams, outParams, requiresSeq, globalMods, ensuresSeq); - asyncAndParallelCallDesugarings[procName] = proc; - } - CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes); - dummyCallCmd.Proc = proc; - newCmds.Add(dummyCallCmd); - } - - private void CreateYieldCheckerImpl(Implementation impl, List> yields) - { - if (yields.Count == 0) return; - - Dictionary map = new Dictionary(); - foreach (Variable local in impl.LocVars) - { - var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type)); - map[local] = Expr.Ident(copy); - } - - Program program = linearTypeChecker.program; - List locals = new List(); - List inputs = new List(); - foreach (IdentifierExpr ie in map.Values) - { - locals.Add(ie.Decl); - } - for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) - { - Variable inParam = impl.InParams[i]; - Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type)); - locals.Add(copy); - map[impl.InParams[i]] = Expr.Ident(copy); - } - { - int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count; - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - Variable inParam = impl.InParams[i]; - Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true); - inputs.Add(copy); - map[impl.InParams[i]] = Expr.Ident(copy); - i++; - } - } - for (int i = 0; i < impl.OutParams.Count; i++) - { - Variable outParam = impl.OutParams[i]; - var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type)); - locals.Add(copy); - map[impl.OutParams[i]] = Expr.Ident(copy); - } - Dictionary ogOldLocalMap = new Dictionary(); - Dictionary assumeMap = new Dictionary(map); - foreach (IdentifierExpr ie in globalMods) - { - Variable g = ie.Decl; - var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type)); - locals.Add(copy); - ogOldLocalMap[g] = Expr.Ident(copy); - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true); - inputs.Add(f); - assumeMap[g] = Expr.Ident(f); - } - - Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap); - Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap); - Substitution subst = Substituter.SubstitutionFromHashtable(map); - List yieldCheckerBlocks = new List(); - List labels = new List(); - List labelTargets = new List(); - Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); - labels.Add(yieldCheckerBlock.Label); - labelTargets.Add(yieldCheckerBlock); - yieldCheckerBlocks.Add(yieldCheckerBlock); - int yieldCount = 0; - foreach (List cs in yields) - { - List newCmds = new List(); - foreach (Cmd cmd in cs) - { - PredicateCmd predCmd = (PredicateCmd)cmd; - newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr))); - } - foreach (Cmd cmd in cs) - { - PredicateCmd predCmd = (PredicateCmd)cmd; - var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr); - if (predCmd is AssertCmd) - { - AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes); - assertCmd.ErrorData = "Non-interference check failed"; - newCmds.Add(assertCmd); - } - else - { - newCmds.Add(new AssumeCmd(Token.NoToken, newExpr)); - } - } - newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); - yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken)); - labels.Add(yieldCheckerBlock.Label); - labelTargets.Add(yieldCheckerBlock); - yieldCheckerBlocks.Add(yieldCheckerBlock); - } - yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List(), new GotoCmd(Token.NoToken, labels, labelTargets))); - - // Create the yield checker procedure - var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", "Impl", impl.Name); - var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List(), new List(), new List(), new List()); - yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - yieldCheckerProcs.Add(yieldCheckerProc); - - // Create the yield checker implementation - var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List(), locals, yieldCheckerBlocks); - yieldCheckerImpl.Proc = yieldCheckerProc; - yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - yieldCheckerImpls.Add(yieldCheckerImpl); - } - - private bool IsYieldingHeader(Graph graph, Block header) - { - foreach (Block backEdgeNode in graph.BackEdgeNodes(header)) - { - foreach (Block x in graph.NaturalLoops(header, backEdgeNode)) - { - foreach (Cmd cmd in x.Cmds) - { - if (cmd is YieldCmd) - return true; - if (cmd is ParCallCmd) - return true; - CallCmd callCmd = cmd as CallCmd; - if (callCmd == null) continue; - if (yieldingProcs.Contains(callCmd.Proc)) - return true; - } - } - } - return false; - } - - private Graph ComputeYieldingLoopHeaders(Implementation impl, out HashSet yieldingHeaders) - { - Graph graph; - impl.PruneUnreachableBlocks(); - impl.ComputePredecessorsForBlocks(); - graph = Program.GraphFromImpl(impl); - graph.ComputeLoops(); - if (!graph.Reducible) - { - throw new Exception("Irreducible flow graphs are unsupported."); - } - yieldingHeaders = new HashSet(); - IEnumerable sortedHeaders = graph.SortHeadersByDominance(); - foreach (Block header in sortedHeaders) - { - if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header))) - { - yieldingHeaders.Add(header); - } - else if (IsYieldingHeader(graph, header)) - { - yieldingHeaders.Add(header); - } - else - { - continue; - } - } - return graph; - } - - private void SetupRefinementCheck(Implementation impl, - out List newLocalVars, - out Dictionary domainNameToInputVar, out Dictionary domainNameToLocalVar, out Dictionary ogOldGlobalMap) - { - pc = null; - ok = null; - alpha = null; - beta = null; - frame = null; - - newLocalVars = new List(); - Program program = linearTypeChecker.program; - ogOldGlobalMap = new Dictionary(); - foreach (IdentifierExpr ie in globalMods) - { - Variable g = ie.Decl; - LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type)); - ogOldGlobalMap[g] = l; - newLocalVars.Add(l); - } - - Procedure originalProc = implMap[impl].Proc; - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc]; - if (actionInfo.createdAtLayerNum == this.layerNum) - { - pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool)); - newLocalVars.Add(pc); - ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool)); - newLocalVars.Add(ok); - Dictionary alwaysMap = new Dictionary(); - for (int i = 0; i < originalProc.InParams.Count; i++) - { - alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]); - } - for (int i = 0; i < originalProc.OutParams.Count; i++) - { - alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]); - } - Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap); - Dictionary foroldMap = new Dictionary(); - foreach (IdentifierExpr ie in globalMods) - { - foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]); - } - Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); - frame = new HashSet(moverTypeChecker.SharedVariables); - foreach (Variable v in moverTypeChecker.SharedVariables) - { - if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || - moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum) - { - frame.Remove(v); - } - } - AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; - if (atomicActionInfo == null) - { - beta = Expr.True; - foreach (var v in frame) - { - beta = Expr.And(beta, Expr.Eq(Expr.Ident(v), foroldMap[v])); - } - alpha = Expr.True; - } - else - { - Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, new HashSet())).TransitionRelationCompute(true); - beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr); - Expr alphaExpr = Expr.True; - foreach (AssertCmd assertCmd in atomicActionInfo.gate) - { - alphaExpr = Expr.And(alphaExpr, assertCmd.Expr); - alphaExpr.Type = Type.Bool; - } - alpha = Substituter.Apply(always, alphaExpr); - } - foreach (Variable f in impl.OutParams) - { - LocalVariable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_old_{0}", f.Name), f.TypedIdent.Type)); - newLocalVars.Add(copy); - ogOldGlobalMap[f] = copy; - } - } - - domainNameToInputVar = new Dictionary(); - domainNameToLocalVar = new Dictionary(); - { - int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count; - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - Variable inParam = impl.InParams[i]; - domainNameToInputVar[domainName] = inParam; - Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type)); - domainNameToLocalVar[domainName] = l; - newLocalVars.Add(l); - i++; - } - } - } - - private void TransformImpl(Implementation impl) - { - HashSet yieldingHeaders; - Graph graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders); - - List newLocalVars; - Dictionary domainNameToInputVar, domainNameToLocalVar; - Dictionary ogOldGlobalMap; - SetupRefinementCheck(impl, out newLocalVars, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap); - - List> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap); - - List oldPcs, oldOks; - ProcessLoopHeaders(impl, graph, yieldingHeaders, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap, out oldPcs, out oldOks); - - AddInitialBlock(impl, oldPcs, oldOks, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap); - - CreateYieldCheckerImpl(impl, yields); - - impl.LocVars.AddRange(newLocalVars); - impl.LocVars.AddRange(oldPcs); - impl.LocVars.AddRange(oldOks); - - UnifyCallsToYieldProc(impl, ogOldGlobalMap, domainNameToLocalVar); - } - - private void UnifyCallsToYieldProc(Implementation impl, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) - { - CallCmd yieldCallCmd = CallToYieldProc(Token.NoToken, ogOldGlobalMap, domainNameToLocalVar); - Block yieldCheckBlock = new Block(Token.NoToken, "CallToYieldProc", new List(new Cmd[] { yieldCallCmd, new AssumeCmd(Token.NoToken, Expr.False) }), new ReturnCmd(Token.NoToken)); - List newBlocks = new List(); - foreach (Block b in impl.Blocks) - { - TransferCmd transferCmd = b.TransferCmd; - List newCmds = new List(); - for (int i = b.Cmds.Count-1; i >= 0; i--) - { - CallCmd callCmd = b.Cmds[i] as CallCmd; - if (callCmd == null || callCmd.Proc != yieldProc) - { - newCmds.Insert(0, b.Cmds[i]); - } - else - { - Block newBlock = new Block(Token.NoToken, b.Label + i, newCmds, transferCmd); - newCmds = new List(); - transferCmd = new GotoCmd(Token.NoToken, new List(new string[] { newBlock.Label, yieldCheckBlock.Label }), - new List(new Block[] { newBlock, yieldCheckBlock })); - newBlocks.Add(newBlock); - } - } - b.Cmds = newCmds; - b.TransferCmd = transferCmd; - } - impl.Blocks.AddRange(newBlocks); - impl.Blocks.Add(yieldCheckBlock); - } - - private List> CollectAndDesugarYields(Implementation impl, - Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap) - { - // Collect the yield predicates and desugar yields - List> yields = new List>(); - List cmds = new List(); - foreach (Block b in impl.Blocks) - { - YieldCmd yieldCmd = null; - List newCmds = new List(); - for (int i = 0; i < b.Cmds.Count; i++) - { - Cmd cmd = b.Cmds[i]; - if (cmd is YieldCmd) - { - yieldCmd = (YieldCmd)cmd; - continue; - } - if (yieldCmd != null) - { - PredicateCmd pcmd = cmd as PredicateCmd; - if (pcmd == null) - { - DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar); - if (cmds.Count > 0) - { - yields.Add(cmds); - cmds = new List(); - } - yieldCmd = null; - } - else - { - cmds.Add(pcmd); - } - } - - if (cmd is CallCmd) - { - CallCmd callCmd = cmd as CallCmd; - if (yieldingProcs.Contains(callCmd.Proc)) - { - AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); - } - if (callCmd.IsAsync) - { - if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name)) - { - asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List(), new List()); - } - var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name]; - CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs, callCmd.Attributes); - dummyCallCmd.Proc = dummyAsyncTargetProc; - newCmds.Add(dummyCallCmd); - } - else - { - newCmds.Add(callCmd); - } - if (yieldingProcs.Contains(callCmd.Proc)) - { - HashSet availableLinearVars = new HashSet(AvailableLinearVars(callCmd)); - linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars); - - if (!callCmd.IsAsync && globalMods.Count > 0 && pc != null) - { - // assume pc || alpha(i, g); - Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha); - assumeExpr.Type = Type.Bool; - newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr)); - } - - Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); - AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); - } - } - else if (cmd is ParCallCmd) - { - ParCallCmd parCallCmd = cmd as ParCallCmd; - AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); - DesugarParallelCallCmd(newCmds, parCallCmd); - HashSet availableLinearVars = new HashSet(AvailableLinearVars(parCallCmd)); - linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars); - - if (globalMods.Count > 0 && pc != null) - { - // assume pc || alpha(i, g); - Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha); - assumeExpr.Type = Type.Bool; - newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr)); - } - - Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); - AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); - } - else - { - newCmds.Add(cmd); - } - } - if (yieldCmd != null) - { - DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar); - if (cmds.Count > 0) - { - yields.Add(cmds); - cmds = new List(); - } - } - if (b.TransferCmd is ReturnCmd) - { - AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); - if (pc != null) - { - AssertCmd assertCmd = new AssertCmd(b.TransferCmd.tok, Expr.Ident(ok)); - assertCmd.ErrorData = "Failed to execute atomic action before procedure return"; - newCmds.Add(assertCmd); - } - } - b.Cmds = newCmds; - } - return yields; - } - - private void ProcessLoopHeaders(Implementation impl, Graph graph, HashSet yieldingHeaders, - Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap, - out List oldPcs, out List oldOks) - { - oldPcs = new List(); - oldOks = new List(); - foreach (Block header in yieldingHeaders) - { - LocalVariable oldPc = null; - LocalVariable oldOk = null; - if (pc != null) - { - oldPc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", pc.Name, header.Label), Type.Bool)); - oldPcs.Add(oldPc); - oldOk = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", ok.Name, header.Label), Type.Bool)); - oldOks.Add(oldOk); - } - Dictionary domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar); - foreach (Block pred in header.Predecessors) - { - AddCallToYieldProc(header.tok, pred.Cmds, ogOldGlobalMap, domainNameToLocalVar); - if (pc != null && !graph.BackEdgeNodes(header).Contains(pred)) - { - pred.Cmds.Add(new AssignCmd(Token.NoToken, new List( - new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }), - new List(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) }))); - } - AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); - } - List newCmds = new List(); - if (pc != null) - { - AssertCmd assertCmd; - assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc))); - assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers"; - newCmds.Add(assertCmd); - assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok))); - assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers"; - newCmds.Add(assertCmd); - } - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName]))); - } - foreach (Variable v in ogOldGlobalMap.Keys) - { - newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v])))); - } - newCmds.AddRange(header.Cmds); - header.Cmds = newCmds; - } - } - - private void AddInitialBlock(Implementation impl, List oldPcs, List oldOks, - Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap) - { - // Add initial block - List lhss = new List(); - List rhss = new List(); - if (pc != null) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc))); - rhss.Add(Expr.False); - foreach (Variable oldPc in oldPcs) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc))); - rhss.Add(Expr.False); - } - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))); - rhss.Add(Expr.False); - foreach (Variable oldOk in oldOks) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk))); - rhss.Add(Expr.False); - } - } - Dictionary domainNameToExpr = new Dictionary(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]); - } - for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) - { - Variable v = impl.InParams[i]; - var domainName = linearTypeChecker.FindDomainName(v); - if (domainName == null) continue; - if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; - var domain = linearTypeChecker.linearDomains[domainName]; - if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue; - Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List { Expr.Ident(v) }); - domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { ie, domainNameToExpr[domainName] }); - } - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName]))); - rhss.Add(domainNameToExpr[domainName]); - } - foreach (Variable g in ogOldGlobalMap.Keys) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); - rhss.Add(Expr.Ident(g)); - } - if (lhss.Count > 0) - { - Block initBlock = new Block(Token.NoToken, "og_init", new List { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] })); - impl.Blocks.Insert(0, initBlock); - } - } - - private void AddYieldProcAndImpl(List decls) - { - if (yieldProc == null) return; - - Program program = linearTypeChecker.program; - List inputs = new List(); - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - var domain = linearTypeChecker.linearDomains[domainName]; - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true); - inputs.Add(f); - } - foreach (IdentifierExpr ie in globalMods) - { - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); - inputs.Add(f); - } - List blocks = new List(); - TransferCmd transferCmd = new ReturnCmd(Token.NoToken); - if (yieldCheckerProcs.Count > 0) - { - List blockTargets = new List(); - List labelTargets = new List(); - int labelCount = 0; - foreach (Procedure proc in yieldCheckerProcs) - { - List exprSeq = new List(); - foreach (Variable v in inputs) - { - exprSeq.Add(Expr.Ident(v)); - } - CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List()); - callCmd.Proc = proc; - string label = string.Format("L_{0}", labelCount++); - Block block = new Block(Token.NoToken, label, new List { callCmd }, new ReturnCmd(Token.NoToken)); - labelTargets.Add(label); - blockTargets.Add(block); - blocks.Add(block); - } - transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets); - } - blocks.Insert(0, new Block(Token.NoToken, "enter", new List(), transferCmd)); - - var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List(), inputs, new List(), new List(), blocks); - yieldImpl.Proc = yieldProc; - yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - decls.Add(yieldProc); - decls.Add(yieldImpl); - } - - public static QKeyValue RemoveYieldsAttribute(QKeyValue iter) - { - if (iter == null) return null; - iter.Next = RemoveYieldsAttribute(iter.Next); - return (iter.Key == "yields") ? iter.Next : iter; - } - - public static QKeyValue RemoveMoverAttribute(QKeyValue iter) - { - if (iter == null) return null; - iter.Next = RemoveMoverAttribute(iter.Next); - if (iter.Key == "atomic" || iter.Key == "right" || iter.Key == "left" || iter.Key == "both") - return iter.Next; - else - return iter; - } - - private List Collect() - { - List decls = new List(); - foreach (Procedure proc in yieldCheckerProcs) - { - decls.Add(proc); - } - foreach (Implementation impl in yieldCheckerImpls) - { - decls.Add(impl); - } - foreach (Procedure proc in asyncAndParallelCallDesugarings.Values) - { - decls.Add(proc); - } - AddYieldProcAndImpl(decls); - return decls; - } - - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) - { - Program program = linearTypeChecker.program; - foreach (int layerNum in moverTypeChecker.AllImplementedLayerNums) - { - if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; - - MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum); - foreach (var proc in program.Procedures) - { - if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue; - Procedure duplicateProc = duplicator.VisitProcedure(proc); - decls.Add(duplicateProc); - } - decls.AddRange(duplicator.impls); - OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator); - foreach (var impl in program.Implementations) - { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum) - continue; - Implementation duplicateImpl = duplicator.VisitImplementation(impl); - ogTransform.TransformImpl(duplicateImpl); - decls.Add(duplicateImpl); - } - decls.AddRange(ogTransform.Collect()); - } - } - } -} diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs index b56e1cf3..1be7cc07 100644 --- a/Source/Concurrency/Program.cs +++ b/Source/Concurrency/Program.cs @@ -7,20 +7,20 @@ namespace Microsoft.Boogie { public class Concurrency { - public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker) + public static void Transform(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker) { List originalDecls = new List(); Program program = linearTypeChecker.program; foreach (var decl in program.TopLevelDeclarations) { Procedure proc = decl as Procedure; - if (proc != null && moverTypeChecker.procToActionInfo.ContainsKey(proc)) + if (proc != null && civlTypeChecker.procToActionInfo.ContainsKey(proc)) { originalDecls.Add(proc); continue; } Implementation impl = decl as Implementation; - if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) + if (impl != null && civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) { originalDecls.Add(impl); } @@ -29,12 +29,12 @@ namespace Microsoft.Boogie List decls = new List(); if (!CommandLineOptions.Clo.TrustAtomicityTypes) { - MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls); + MoverCheck.AddCheckers(linearTypeChecker, civlTypeChecker, decls); } - OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls); + CivlRefinement.AddCheckers(linearTypeChecker, civlTypeChecker, decls); foreach (Declaration decl in decls) { - decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes); + decl.Attributes = CivlRefinement.RemoveYieldsAttribute(decl.Attributes); } program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x)); program.AddTopLevelDeclarations(decls); diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs deleted file mode 100644 index 0e257f30..00000000 --- a/Source/Concurrency/TypeCheck.cs +++ /dev/null @@ -1,1168 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Boogie; -using System.Diagnostics.Contracts; -using System.Diagnostics; - -namespace Microsoft.Boogie -{ - public enum MoverType - { - Top, - Atomic, - Right, - Left, - Both - } - - public class ActionInfo - { - public Procedure proc; - public int createdAtLayerNum; - public int availableUptoLayerNum; - public bool hasImplementation; - public bool isExtern; - - public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum) - { - this.proc = proc; - this.createdAtLayerNum = createdAtLayerNum; - this.availableUptoLayerNum = availableUptoLayerNum; - this.hasImplementation = false; - this.isExtern = QKeyValue.FindBoolAttribute(proc.Attributes, "extern"); - } - - public virtual bool IsRightMover - { - get { return true; } - } - - public virtual bool IsLeftMover - { - get { return true; } - } - } - - public class AtomicActionInfo : ActionInfo - { - public Ensures ensures; - public MoverType moverType; - public List gate; - public CodeExpr action; - public List thisGate; - public CodeExpr thisAction; - public List thisInParams; - public List thisOutParams; - public List thatGate; - public CodeExpr thatAction; - public List thatInParams; - public List thatOutParams; - public HashSet actionUsedGlobalVars; - public HashSet modifiedGlobalVars; - public HashSet gateUsedGlobalVars; - public bool hasAssumeCmd; - public Dictionary thisMap; - public Dictionary thatMap; - - public bool CommutesWith(AtomicActionInfo actionInfo) - { - if (this.modifiedGlobalVars.Intersect(actionInfo.actionUsedGlobalVars).Count() > 0) - return false; - if (this.actionUsedGlobalVars.Intersect(actionInfo.modifiedGlobalVars).Count() > 0) - return false; - return true; - } - - public override bool IsRightMover - { - get { return moverType == MoverType.Right || moverType == MoverType.Both; } - } - - public override bool IsLeftMover - { - get { return moverType == MoverType.Left || moverType == MoverType.Both; } - } - - public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int layerNum, int availableUptoLayerNum) - : base(proc, layerNum, availableUptoLayerNum) - { - this.ensures = ensures; - this.moverType = moverType; - this.gate = new List(); - this.action = ensures.Condition as CodeExpr; - this.thisGate = new List(); - this.thisInParams = new List(); - this.thisOutParams = new List(); - this.thatGate = new List(); - this.thatInParams = new List(); - this.thatOutParams = new List(); - this.hasAssumeCmd = false; - this.thisMap = new Dictionary(); - this.thatMap = new Dictionary(); - - foreach (Block block in this.action.Blocks) - { - block.Cmds.ForEach(x => this.hasAssumeCmd = this.hasAssumeCmd || x is AssumeCmd); - } - - foreach (Block block in this.action.Blocks) - { - if (block.TransferCmd is ReturnExprCmd) - { - block.TransferCmd = new ReturnCmd(block.TransferCmd.tok); - } - } - - var cmds = this.action.Blocks[0].Cmds; - for (int i = 0; i < cmds.Count; i++) - { - AssertCmd assertCmd = cmds[i] as AssertCmd; - if (assertCmd == null) break; - this.gate.Add(assertCmd); - cmds[i] = new AssumeCmd(assertCmd.tok, Expr.True); - } - - foreach (Variable x in proc.InParams) - { - Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), true, x.Attributes); - this.thisInParams.Add(thisx); - this.thisMap[x] = Expr.Ident(thisx); - Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true, x.Attributes); - this.thatInParams.Add(thatx); - this.thatMap[x] = Expr.Ident(thatx); - } - foreach (Variable x in proc.OutParams) - { - Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), false, x.Attributes); - this.thisOutParams.Add(thisx); - this.thisMap[x] = Expr.Ident(thisx); - Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false, x.Attributes); - this.thatOutParams.Add(thatx); - this.thatMap[x] = Expr.Ident(thatx); - } - List thisLocVars = new List(); - List thatLocVars = new List(); - foreach (Variable x in this.action.LocVars) - { - Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), false); - thisMap[x] = Expr.Ident(thisx); - thisLocVars.Add(thisx); - Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false); - thatMap[x] = Expr.Ident(thatx); - thatLocVars.Add(thatx); - } - Contract.Assume(proc.TypeParameters.Count == 0); - Substitution thisSubst = Substituter.SubstitutionFromHashtable(this.thisMap); - Substitution thatSubst = Substituter.SubstitutionFromHashtable(this.thatMap); - foreach (AssertCmd assertCmd in this.gate) - { - this.thisGate.Add((AssertCmd)Substituter.Apply(thisSubst, assertCmd)); - this.thatGate.Add((AssertCmd)Substituter.Apply(thatSubst, assertCmd)); - } - this.thisAction = new CodeExpr(thisLocVars, SubstituteBlocks(this.action.Blocks, thisSubst, "this_")); - this.thatAction = new CodeExpr(thatLocVars, SubstituteBlocks(this.action.Blocks, thatSubst, "that_")); - - { - VariableCollector collector = new VariableCollector(); - collector.Visit(this.action); - this.actionUsedGlobalVars = new HashSet(collector.usedVars.Where(x => x is GlobalVariable)); - } - - List modifiedVars = new List(); - foreach (Block block in this.action.Blocks) - { - block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars)); - } - this.modifiedGlobalVars = new HashSet(modifiedVars.Where(x => x is GlobalVariable)); - - { - VariableCollector collector = new VariableCollector(); - this.gate.ForEach(assertCmd => collector.Visit(assertCmd)); - this.gateUsedGlobalVars = new HashSet(collector.usedVars.Where(x => x is GlobalVariable)); - } - } - - private List SubstituteBlocks(List blocks, Substitution subst, string blockLabelPrefix) - { - Dictionary blockMap = new Dictionary(); - List otherBlocks = new List(); - foreach (Block block in blocks) - { - List otherCmds = new List(); - foreach (Cmd cmd in block.Cmds) - { - otherCmds.Add(Substituter.Apply(subst, cmd)); - } - Block otherBlock = new Block(); - otherBlock.Cmds = otherCmds; - otherBlock.Label = blockLabelPrefix + block.Label; - otherBlocks.Add(otherBlock); - blockMap[block] = otherBlock; - } - foreach (Block block in blocks) - { - if (block.TransferCmd is ReturnCmd) - { - blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok); - continue; - } - List otherGotoCmdLabelTargets = new List(); - List otherGotoCmdLabelNames = new List(); - GotoCmd gotoCmd = block.TransferCmd as GotoCmd; - foreach (Block target in gotoCmd.labelTargets) - { - otherGotoCmdLabelTargets.Add(blockMap[target]); - otherGotoCmdLabelNames.Add(blockMap[target].Label); - } - blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets); - } - return otherBlocks; - } - } - - public class SharedVariableInfo - { - public int introLayerNum; - public int hideLayerNum; - - public SharedVariableInfo(int introLayerNum, int hideLayerNum) - { - this.introLayerNum = introLayerNum; - this.hideLayerNum = hideLayerNum; - } - } - - public class LayerEraser : ReadOnlyVisitor - { - private QKeyValue RemoveLayerAttribute(QKeyValue iter) - { - if (iter == null) return null; - iter.Next = RemoveLayerAttribute(iter.Next); - return (iter.Key == "layer") ? iter.Next : iter; - } - - public override Variable VisitVariable(Variable node) - { - node.Attributes = RemoveLayerAttribute(node.Attributes); - return base.VisitVariable(node); - } - - public override Procedure VisitProcedure(Procedure node) - { - node.Attributes = RemoveLayerAttribute(node.Attributes); - return base.VisitProcedure(node); - } - - public override Implementation VisitImplementation(Implementation node) - { - node.Attributes = RemoveLayerAttribute(node.Attributes); - return base.VisitImplementation(node); - } - - public override Requires VisitRequires(Requires node) - { - node.Attributes = RemoveLayerAttribute(node.Attributes); - return base.VisitRequires(node); - } - - public override Ensures VisitEnsures(Ensures node) - { - node.Attributes = RemoveLayerAttribute(node.Attributes); - return base.VisitEnsures(node); - } - - public override Cmd VisitAssertCmd(AssertCmd node) - { - node.Attributes = RemoveLayerAttribute(node.Attributes); - return base.VisitAssertCmd(node); - } - } - - public class LayerRange - { - public int lowerLayerNum; - public int upperLayerNum; - public LayerRange(int layer) - { - this.lowerLayerNum = layer; - this.upperLayerNum = layer; - } - public LayerRange(int lower, int upper) - { - this.lowerLayerNum = lower; - this.upperLayerNum = upper; - } - public LayerRange(IEnumerable layerNums) - { - int min = int.MaxValue; - int max = int.MinValue; - foreach (var layerNum in layerNums) - { - if (layerNum < min) - { - min = layerNum; - } - if (max < layerNum) - { - max = layerNum; - } - } - this.lowerLayerNum = min; - this.upperLayerNum = max; - } - public bool Contains(int layerNum) - { - return lowerLayerNum <= layerNum && layerNum <= upperLayerNum; - } - public bool Subset(int lower, int upper) - { - return lower <= lowerLayerNum && upperLayerNum <= upper; - } - public bool Equal(int lower, int upper) - { - return lower == lowerLayerNum && upperLayerNum == upper; - } - public bool Subset(LayerRange info) - { - return info.lowerLayerNum <= lowerLayerNum && upperLayerNum <= info.upperLayerNum; - } - } - - public class AtomicProcedureInfo - { - public bool isPure; - public HashSet layers; - public AtomicProcedureInfo() - { - this.isPure = true; - this.layers = null; - } - public AtomicProcedureInfo(HashSet layers) - { - this.isPure = false; - this.layers = layers; - } - } - - public class LocalVariableInfo - { - public bool isGhost; - public int layer; - public LocalVariableInfo(bool isGhost, int layer) - { - this.isGhost = isGhost; - this.layer = layer; - } - } - - public class MoverTypeChecker : ReadOnlyVisitor - { - CheckingContext checkingContext; - Procedure enclosingProc; - Implementation enclosingImpl; - HashSet sharedVarsAccessed; - int introducedLocalVarsUpperBound; - int ghostVarIntroLayerAllowed; - - public Program program; - public int errorCount; - public Dictionary globalVarToSharedVarInfo; - public Dictionary procToActionInfo; - public Dictionary procToAtomicProcedureInfo; - public Dictionary> absyToLayerNums; - public Dictionary localVarToLocalVariableInfo; - - public bool CallExists(CallCmd callCmd, int enclosingProcLayerNum, int layerNum) - { - if (!procToAtomicProcedureInfo.ContainsKey(callCmd.Proc)) - return true; - var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc]; - if (callCmd.Proc.Modifies.Count > 0) - { - return enclosingProcLayerNum == layerNum; - } - if (callCmd.Outs.Count == 0) - { - return true; - } - var outputVar = callCmd.Outs[0].Decl; - var localVariableInfo = localVarToLocalVariableInfo[outputVar]; - if (localVariableInfo.isGhost) - { - return localVariableInfo.layer == layerNum; - } - if (atomicProcedureInfo.isPure) - { - return localVariableInfo.layer <= layerNum; - } - else - { - return enclosingProcLayerNum == layerNum; - } - } - - private static List FindLayers(QKeyValue kv) - { - List layers = new List(); - for (; kv != null; kv = kv.Next) - { - if (kv.Key != "layer") continue; - foreach (var o in kv.Params) - { - Expr e = o as Expr; - if (e == null) return null; - LiteralExpr l = e as LiteralExpr; - if (l == null) return null; - if (!l.isBigNum) return null; - layers.Add(l.asBigNum.ToIntSafe); - } - } - return layers; - } - - private static int Least(IEnumerable layerNums) - { - int least = int.MaxValue; - foreach (var layer in layerNums) - { - if (layer < least) - { - least = layer; - } - } - return least; - } - - private static MoverType GetMoverType(Ensures e) - { - if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic")) - return MoverType.Atomic; - if (QKeyValue.FindBoolAttribute(e.Attributes, "right")) - return MoverType.Right; - if (QKeyValue.FindBoolAttribute(e.Attributes, "left")) - return MoverType.Left; - if (QKeyValue.FindBoolAttribute(e.Attributes, "both")) - return MoverType.Both; - return MoverType.Top; - } - - public MoverTypeChecker(Program program) - { - this.errorCount = 0; - this.checkingContext = new CheckingContext(null); - this.program = program; - this.enclosingProc = null; - this.enclosingImpl = null; - this.sharedVarsAccessed = null; - this.introducedLocalVarsUpperBound = int.MinValue; - this.ghostVarIntroLayerAllowed = int.MinValue; - - this.localVarToLocalVariableInfo = new Dictionary(); - this.absyToLayerNums = new Dictionary>(); - this.globalVarToSharedVarInfo = new Dictionary(); - this.procToActionInfo = new Dictionary(); - this.procToAtomicProcedureInfo = new Dictionary(); - - foreach (var g in program.GlobalVariables) - { - List layerNums = FindLayers(g.Attributes); - if (layerNums.Count == 0) - { - // Inaccessible from yielding and atomic procedures - } - else if (layerNums.Count == 1) - { - this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue); - } - else if (layerNums.Count == 2) - { - this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]); - } - else - { - Error(g, "Too many layer numbers"); - } - } - } - - private HashSet allImplementedLayerNums; - public IEnumerable AllImplementedLayerNums - { - get - { - if (allImplementedLayerNums == null) - { - allImplementedLayerNums = new HashSet(); - foreach (ActionInfo actionInfo in procToActionInfo.Values) - { - if (actionInfo.hasImplementation) - { - allImplementedLayerNums.Add(actionInfo.createdAtLayerNum); - } - } - } - return allImplementedLayerNums; - } - } - - private HashSet allCreatedLayerNums; - public IEnumerable AllCreatedLayerNums - { - get - { - if (allCreatedLayerNums == null) - { - allCreatedLayerNums = new HashSet(); - foreach (ActionInfo actionInfo in procToActionInfo.Values) - { - allCreatedLayerNums.Add(actionInfo.createdAtLayerNum); - } - } - return allCreatedLayerNums; - } - } - - private LayerRange FindLayerRange() - { - int maxIntroLayerNum = int.MinValue; - int minHideLayerNum = int.MaxValue; - foreach (var g in sharedVarsAccessed) - { - if (globalVarToSharedVarInfo[g].introLayerNum > maxIntroLayerNum) - { - maxIntroLayerNum = globalVarToSharedVarInfo[g].introLayerNum; - } - if (globalVarToSharedVarInfo[g].hideLayerNum < minHideLayerNum) - { - minHideLayerNum = globalVarToSharedVarInfo[g].hideLayerNum; - } - } - return new LayerRange(maxIntroLayerNum, minHideLayerNum); - } - - public void TypeCheck() - { - foreach (var proc in program.Procedures) - { - if (!QKeyValue.FindBoolAttribute(proc.Attributes, "pure")) continue; - if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) - { - Error(proc, "Pure procedure must not yield"); - continue; - } - if (QKeyValue.FindBoolAttribute(proc.Attributes, "layer")) - { - Error(proc, "Pure procedure must not have layers"); - continue; - } - if (proc.Modifies.Count > 0) - { - Error(proc, "Pure procedure must not modify a global variable"); - continue; - } - procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(); - } - foreach (var proc in program.Procedures) - { - if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue; - var procLayerNums = RemoveDuplicatesAndSort(FindLayers(proc.Attributes)); - if (procLayerNums.Count == 0) continue; - foreach (IdentifierExpr ie in proc.Modifies) - { - if (!globalVarToSharedVarInfo.ContainsKey(ie.Decl)) - { - Error(proc, "Atomic procedure cannot modify a global variable without layer numbers"); - } - else if (globalVarToSharedVarInfo[ie.Decl].introLayerNum != procLayerNums[0]) - { - Error(proc, "The introduction layer of a modified global variable must be identical to the layer of the atomic procedure"); - } - } - if (proc.Modifies.Count == 0 || procLayerNums.Count == 1) - { - procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(new HashSet(procLayerNums)); - } - else - { - Error(proc, "An atomic procedure with more than one layer must not modify a global variable"); - } - } - if (errorCount > 0) return; - - foreach (Implementation impl in program.Implementations) - { - if (!procToAtomicProcedureInfo.ContainsKey(impl.Proc)) continue; - var atomicProcedureInfo = procToAtomicProcedureInfo[impl.Proc]; - if (atomicProcedureInfo.isPure) - { - this.enclosingImpl = impl; - (new PurityChecker(this)).VisitImplementation(impl); - } - else - { - this.enclosingImpl = impl; - this.sharedVarsAccessed = new HashSet(); - (new PurityChecker(this)).VisitImplementation(impl); - LayerRange upperBound = FindLayerRange(); - LayerRange lowerBound = new LayerRange(atomicProcedureInfo.layers); - if (!lowerBound.Subset(upperBound)) - { - Error(impl, "Atomic procedure cannot access global variable"); - } - this.sharedVarsAccessed = null; - } - } - if (errorCount > 0) return; - - foreach (var proc in program.Procedures) - { - if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue; - - int createdAtLayerNum; // must be initialized by the following code, otherwise it is an error - int availableUptoLayerNum = int.MaxValue; - List attrs = FindLayers(proc.Attributes); - if (attrs.Count == 1) - { - createdAtLayerNum = attrs[0]; - } - else if (attrs.Count == 2) - { - createdAtLayerNum = attrs[0]; - availableUptoLayerNum = attrs[1]; - } - else - { - Error(proc, "Incorrect number of layers"); - continue; - } - foreach (Ensures e in proc.Ensures) - { - MoverType moverType = GetMoverType(e); - if (moverType == MoverType.Top) continue; - CodeExpr codeExpr = e.Condition as CodeExpr; - if (codeExpr == null) - { - Error(e, "An atomic action must be a CodeExpr"); - continue; - } - if (procToActionInfo.ContainsKey(proc)) - { - Error(proc, "A procedure can have at most one atomic action"); - continue; - } - if (availableUptoLayerNum <= createdAtLayerNum) - { - Error(proc, "Creation layer number must be less than the available upto layer number"); - continue; - } - - sharedVarsAccessed = new HashSet(); - enclosingProc = proc; - enclosingImpl = null; - base.VisitEnsures(e); - LayerRange upperBound = FindLayerRange(); - LayerRange lowerBound = new LayerRange(createdAtLayerNum, availableUptoLayerNum); - if (lowerBound.Subset(upperBound)) - { - procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum); - } - else - { - Error(e, "A variable being accessed in this action is unavailable"); - } - sharedVarsAccessed = null; - } - if (errorCount > 0) continue; - if (!procToActionInfo.ContainsKey(proc)) - { - if (availableUptoLayerNum < createdAtLayerNum) - { - Error(proc, "Creation layer number must be no more than the available upto layer number"); - continue; - } - else - { - procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum); - } - } - } - if (errorCount > 0) return; - foreach (Implementation node in program.Implementations) - { - if (!procToActionInfo.ContainsKey(node.Proc)) continue; - foreach (Variable v in node.LocVars) - { - var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum); - if (layer == int.MinValue) continue; - localVarToLocalVariableInfo[v] = new LocalVariableInfo(QKeyValue.FindBoolAttribute(node.Attributes, "ghost"), layer); - } - for (int i = 0; i < node.Proc.InParams.Count; i++) - { - Variable v = node.Proc.InParams[i]; - var layer = FindLocalVariableLayer(node.Proc, v, procToActionInfo[node.Proc].createdAtLayerNum); - if (layer == int.MinValue) continue; - localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer); - localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(false, layer); - } - for (int i = 0; i < node.Proc.OutParams.Count; i++) - { - Variable v = node.Proc.OutParams[i]; - var layer = FindLocalVariableLayer(node.Proc, v, procToActionInfo[node.Proc].createdAtLayerNum); - if (layer == int.MinValue) continue; - localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer); - localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(false, layer); - } - } - if (errorCount > 0) return; - foreach (var impl in program.Implementations) - { - if (!procToActionInfo.ContainsKey(impl.Proc)) continue; - ActionInfo actionInfo = procToActionInfo[impl.Proc]; - procToActionInfo[impl.Proc].hasImplementation = true; - if (actionInfo.isExtern) - { - Error(impl.Proc, "Extern procedure cannot have an implementation"); - } - } - foreach (var g in this.globalVarToSharedVarInfo.Keys) - { - var info = globalVarToSharedVarInfo[g]; - if (!this.AllCreatedLayerNums.Contains(info.introLayerNum)) - { - Error(g, "Variable must be introduced with creation of some atomic action"); - } - if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum)) - { - Error(g, "Variable must be hidden with creation of some atomic action"); - } - } - if (errorCount > 0) return; - this.VisitProgram(program); - if (errorCount > 0) return; - YieldTypeChecker.PerformYieldSafeCheck(this); - new LayerEraser().VisitProgram(program); - } - - public IEnumerable SharedVariables - { - get { return this.globalVarToSharedVarInfo.Keys; } - } - - private int FindLocalVariableLayer(Declaration decl, Variable v, int enclosingProcLayerNum) - { - var layers = FindLayers(v.Attributes); - if (layers.Count == 0) return int.MinValue; - if (layers.Count > 1) - { - Error(decl, "Incorrect number of layers"); - return int.MinValue; - } - if (layers[0] > enclosingProcLayerNum) - { - Error(decl, "Layer of local variable cannot be greater than the creation layer of enclosing procedure"); - return int.MinValue; - } - return layers[0]; - } - - public override Implementation VisitImplementation(Implementation node) - { - if (!procToActionInfo.ContainsKey(node.Proc)) - { - return node; - } - this.enclosingImpl = node; - this.enclosingProc = null; - return base.VisitImplementation(node); - } - - public override Procedure VisitProcedure(Procedure node) - { - if (!procToActionInfo.ContainsKey(node)) - { - return node; - } - this.enclosingProc = node; - this.enclosingImpl = null; - return base.VisitProcedure(node); - } - - public override Cmd VisitCallCmd(CallCmd node) - { - int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; - if (procToActionInfo.ContainsKey(node.Proc)) - { - ActionInfo actionInfo = procToActionInfo[node.Proc]; - if (node.IsAsync && actionInfo is AtomicActionInfo) - { - Error(node, "Target of async call cannot be an atomic action"); - } - int calleeLayerNum = procToActionInfo[node.Proc].createdAtLayerNum; - if (enclosingProcLayerNum < calleeLayerNum || - (enclosingProcLayerNum == calleeLayerNum && actionInfo is AtomicActionInfo)) - { - Error(node, "The layer of the caller must be greater than the layer of the callee"); - } - else if (enclosingProcLayerNum == calleeLayerNum && enclosingImpl.OutParams.Count > 0) - { - HashSet outParams = new HashSet(enclosingImpl.OutParams); - foreach (var x in node.Outs) - { - if (x.Decl is GlobalVariable) - { - Error(node, "A global variable cannot be used as output argument for this call"); - } - else if (outParams.Contains(x.Decl)) - { - Error(node, "An output variable of the enclosing implementation cannot be used as output argument for this call"); - } - } - } - if (actionInfo.availableUptoLayerNum < enclosingProcLayerNum) - { - Error(node, "The callee is not available in the caller procedure"); - } - for (int i = 0; i < node.Ins.Count; i++) - { - var formal = node.Proc.InParams[i]; - if (localVarToLocalVariableInfo.ContainsKey(formal)) - { - introducedLocalVarsUpperBound = localVarToLocalVariableInfo[formal].layer; - } - Visit(node.Ins[i]); - introducedLocalVarsUpperBound = int.MinValue; - } - for (int i = 0; i < node.Outs.Count; i++) - { - var formal = node.Proc.OutParams[i]; - if (!localVarToLocalVariableInfo.ContainsKey(formal)) continue; - var actual = node.Outs[i].Decl; - if (localVarToLocalVariableInfo.ContainsKey(actual) && - localVarToLocalVariableInfo[formal].layer <= localVarToLocalVariableInfo[actual].layer) - continue; - Error(node, "Formal parameter of call must be introduced no later than the actual parameter"); - } - return node; - } - else if (procToAtomicProcedureInfo.ContainsKey(node.Proc)) - { - // 1. Outputs are either all ghost or all introduced. - // 2. All outputs have the same layer; call it output layer. - // 3. If callee is impure and has outputs, output layer is a member of layer set of callee. - // 4. If callee is impure and has introduced outputs, then creation number of caller belongs to layer set of callee. - // 5. If callee is impure and modifies globals, then creation number of caller belongs to layer set of callee. - - Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); - bool isGhost = false; // This assignment stops the compiler from complaining. - // In the absence of errors, isGhost is initialized by loop below. - foreach (var ie in node.Outs) - { - if (localVarToLocalVariableInfo.ContainsKey(ie.Decl)) - { - var localVariableInfo = localVarToLocalVariableInfo[ie.Decl]; - if (introducedLocalVarsUpperBound == int.MinValue) - { - introducedLocalVarsUpperBound = localVariableInfo.layer; - isGhost = localVariableInfo.isGhost; - var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc]; - if (!atomicProcedureInfo.isPure) - { - if (!atomicProcedureInfo.layers.Contains(introducedLocalVarsUpperBound)) - { - Error(node, "Layer of output variable must be a layer of the callee"); - } - if (!isGhost && !atomicProcedureInfo.layers.Contains(enclosingProcLayerNum)) - { - Error(node, "The creation layer of caller must be a layer of the callee"); - } - } - } - else - { - if (localVariableInfo.layer != introducedLocalVarsUpperBound) - { - Error(node, "All outputs must have the same layer"); - } - if (localVariableInfo.isGhost != isGhost) - { - Error(node, "Outputs are either all ghost or all introduced"); - } - } - } - else - { - Error(node, "Output variable must be a ghost or introduced local variable"); - } - } - - if (node.Proc.Modifies.Count > 0) - { - var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc]; - if (procToActionInfo[enclosingImpl.Proc] is AtomicActionInfo) - { - if (!atomicProcedureInfo.layers.Contains(enclosingProcLayerNum)) - { - Error(node, "The layer of called atomic procedure must be identical to the creation layer of callee"); - } - } - else - { - Error(node, "Enclosing implementation must refine an atomic action"); - } - introducedLocalVarsUpperBound = enclosingProcLayerNum; - } - foreach (var e in node.Ins) - { - Visit(e); - } - introducedLocalVarsUpperBound = int.MinValue; - return node; - } - else - { - Error(node, "A yielding procedure can call only atomic or yielding procedures"); - return node; - } - } - - public override Cmd VisitParCallCmd(ParCallCmd node) - { - int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; - bool isLeftMover = true; - bool isRightMover = true; - int maxCalleeLayerNum = 0; - int atomicActionCalleeLayerNum = 0; - int numAtomicActions = 0; - foreach (CallCmd iter in node.CallCmds) - { - ActionInfo actionInfo = procToActionInfo[iter.Proc]; - isLeftMover = isLeftMover && actionInfo.IsLeftMover; - isRightMover = isRightMover && actionInfo.IsRightMover; - if (actionInfo.createdAtLayerNum > maxCalleeLayerNum) - { - maxCalleeLayerNum = actionInfo.createdAtLayerNum; - } - if (actionInfo is AtomicActionInfo) - { - numAtomicActions++; - if (atomicActionCalleeLayerNum == 0) - { - atomicActionCalleeLayerNum = actionInfo.createdAtLayerNum; - } - else if (atomicActionCalleeLayerNum != actionInfo.createdAtLayerNum) - { - Error(node, "All atomic actions must be introduced at the same layer"); - } - } - } - if (numAtomicActions > 1 && !isLeftMover && !isRightMover) - { - Error(node, "The atomic actions in the parallel call must be all right movers or all left movers"); - } - if (0 < atomicActionCalleeLayerNum && atomicActionCalleeLayerNum < maxCalleeLayerNum) - { - Error(node, "Atomic actions must be introduced at the highest layer"); - } - return base.VisitParCallCmd(node); - } - - public override Expr VisitIdentifierExpr(IdentifierExpr node) - { - if (node.Decl is GlobalVariable) - { - if (sharedVarsAccessed == null) - { - Error(node, "Shared variable can be accessed only in atomic actions or specifications"); - } - else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl)) - { - sharedVarsAccessed.Add(node.Decl); - } - else - { - Error(node, "Accessed shared variable must have layer annotation"); - } - } - else if ((node.Decl is Formal || node.Decl is Variable) && localVarToLocalVariableInfo.ContainsKey(node.Decl)) - { - var localVariableInfo = localVarToLocalVariableInfo[node.Decl]; - if (localVariableInfo.isGhost) - { - if (ghostVarIntroLayerAllowed != localVariableInfo.layer) - { - Error(node, "Ghost variable inaccessible"); - } - } - else - { - if (introducedLocalVarsUpperBound < localVariableInfo.layer) - { - Error(node, "Introduced variable inaccessible"); - } - } - } - return base.VisitIdentifierExpr(node); - } - - public override Ensures VisitEnsures(Ensures ensures) - { - ActionInfo actionInfo = procToActionInfo[enclosingProc]; - AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; - if (atomicActionInfo != null && atomicActionInfo.ensures == ensures) - { - // This case has already been checked - } - else - { - sharedVarsAccessed = new HashSet(); - Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); - introducedLocalVarsUpperBound = Least(FindLayers(ensures.Attributes)); - base.VisitEnsures(ensures); - CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum); - introducedLocalVarsUpperBound = int.MinValue; - sharedVarsAccessed = null; - } - return ensures; - } - - public override Requires VisitRequires(Requires requires) - { - sharedVarsAccessed = new HashSet(); - Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); - introducedLocalVarsUpperBound = Least(FindLayers(requires.Attributes)); - base.VisitRequires(requires); - CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum); - introducedLocalVarsUpperBound = int.MinValue; - sharedVarsAccessed = null; - return requires; - } - - public override Cmd VisitAssertCmd(AssertCmd node) - { - if (enclosingImpl == null) - { - // in this case, we are visiting an assert inside a CodeExpr - return base.VisitAssertCmd(node); - } - sharedVarsAccessed = new HashSet(); - Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); - var layerNums = FindLayers(node.Attributes); - introducedLocalVarsUpperBound = Least(layerNums); - if (layerNums.Count == 1) - { - ghostVarIntroLayerAllowed = layerNums[0]; - } - base.VisitAssertCmd(node); - CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum); - introducedLocalVarsUpperBound = int.MinValue; - ghostVarIntroLayerAllowed = int.MinValue; - sharedVarsAccessed = null; - return node; - } - - private List RemoveDuplicatesAndSort(List attrs) - { - HashSet layerSet = new HashSet(attrs); - List layers = new List(layerSet); - layers.Sort(); - return layers; - } - - private void CheckAndAddLayers(Absy node, QKeyValue attributes, int enclosingProcLayerNum) - { - List attrs = RemoveDuplicatesAndSort(FindLayers(attributes)); - if (attrs.Count == 0) - { - Error(node, "layer not present"); - return; - } - LayerRange upperBound = FindLayerRange(); - absyToLayerNums[node] = new HashSet(); - foreach (int layerNum in attrs) - { - if (layerNum > enclosingProcLayerNum) - { - Error(node, "The layer cannot be greater than the layer of enclosing procedure"); - } - else if (upperBound.Contains(layerNum)) - { - absyToLayerNums[node].Add(layerNum); - } - else - { - Error(node, string.Format("A variable being accessed in this specification is unavailable at layer {0}", layerNum)); - } - } - } - - public void Error(Absy node, string message) - { - checkingContext.Error(node, message); - errorCount++; - } - - private class PurityChecker : StandardVisitor - { - private MoverTypeChecker moverTypeChecker; - - public PurityChecker(MoverTypeChecker moverTypeChecker) - { - this.moverTypeChecker = moverTypeChecker; - } - - public override Cmd VisitCallCmd(CallCmd node) - { - Procedure enclosingProc = moverTypeChecker.enclosingImpl.Proc; - if (!moverTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc)) - { - moverTypeChecker.Error(node, "Atomic procedure can only call an atomic procedure"); - return base.VisitCallCmd(node); - } - var callerInfo = moverTypeChecker.procToAtomicProcedureInfo[enclosingProc]; - var calleeInfo = moverTypeChecker.procToAtomicProcedureInfo[node.Proc]; - if (calleeInfo.isPure) - { - // do nothing - } - else if (callerInfo.isPure) - { - moverTypeChecker.Error(node, "Pure procedure can only call pure procedures"); - } - else if (!callerInfo.layers.IsSubsetOf(calleeInfo.layers)) - { - moverTypeChecker.Error(node, "Caller layers must be subset of callee layers"); - } - return base.VisitCallCmd(node); - } - - public override Cmd VisitParCallCmd(ParCallCmd node) - { - moverTypeChecker.Error(node, "Atomic procedures cannot make parallel calls"); - return node; - } - - public override Expr VisitIdentifierExpr(IdentifierExpr node) - { - Procedure enclosingProc = moverTypeChecker.enclosingImpl.Proc; - if (node.Decl is GlobalVariable) - { - if (moverTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure) - { - moverTypeChecker.Error(node, "Pure procedure cannot access global variables"); - } - else if (!moverTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl)) - { - moverTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers"); - } - else - { - moverTypeChecker.sharedVarsAccessed.Add(node.Decl); - } - } - return node; - } - } - } -} diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 5b479ed5..a69f066d 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -81,7 +81,7 @@ namespace Microsoft.Boogie Dictionary> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum)); + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum)); } } @@ -97,7 +97,7 @@ namespace Microsoft.Boogie Dictionary> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum)); + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum)); } } @@ -115,7 +115,7 @@ namespace Microsoft.Boogie Dictionary> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum)); + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum)); } } @@ -124,7 +124,7 @@ namespace Microsoft.Boogie foreach (Cmd cmd in block.Cmds) { AssertCmd assertCmd = cmd as AssertCmd; - if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum)) + if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && civlTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum)) { return true; } @@ -132,25 +132,25 @@ namespace Microsoft.Boogie return false; } - public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker) + public static void PerformYieldSafeCheck(CivlTypeChecker civlTypeChecker) { - foreach (var impl in moverTypeChecker.program.Implementations) + foreach (var impl in civlTypeChecker.program.Implementations) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue; + if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue; impl.PruneUnreachableBlocks(); Graph implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); - int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; - foreach (int layerNum in moverTypeChecker.AllImplementedLayerNums) + int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; + foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums) { if (layerNum > specLayerNum) continue; - YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers); + YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers); } } } int stateCounter; - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; Implementation impl; int currLayerNum; Dictionary absyToNode; @@ -160,9 +160,9 @@ namespace Microsoft.Boogie Dictionary, int> edgeLabels; IEnumerable loopHeaders; - private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable loopHeaders) + private YieldTypeChecker(CivlTypeChecker civlTypeChecker, Implementation impl, int currLayerNum, IEnumerable loopHeaders) { - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.impl = impl; this.currLayerNum = currLayerNum; this.loopHeaders = loopHeaders; @@ -226,20 +226,20 @@ namespace Microsoft.Boogie CallCmd callCmd = cmd as CallCmd; if (callCmd.IsAsync) { - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; if (currLayerNum <= actionInfo.createdAtLayerNum) edgeLabels[edge] = 'L'; else edgeLabels[edge] = 'B'; } - else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc)) + else if (!civlTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc)) { edgeLabels[edge] = 'P'; } else { MoverType moverType; - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; if (actionInfo.createdAtLayerNum >= currLayerNum) { moverType = MoverType.Top; @@ -280,7 +280,7 @@ namespace Microsoft.Boogie bool isLeftMover = true; foreach (CallCmd callCmd in parCallCmd.CallCmds) { - if (moverTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum) + if (civlTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum) { isYield = true; } @@ -294,7 +294,7 @@ namespace Microsoft.Boogie int numAtomicActions = 0; foreach (CallCmd callCmd in parCallCmd.CallCmds) { - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; isRightMover = isRightMover && actionInfo.IsRightMover; isLeftMover = isLeftMover && actionInfo.IsLeftMover; if (actionInfo is AtomicActionInfo) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 353ac94f..cf44a77f 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -482,8 +482,8 @@ namespace Microsoft.Boogie } LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; - PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out moverTypeChecker); + CivlTypeChecker civlTypeChecker; + PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out civlTypeChecker); if (oc != PipelineOutcome.ResolvedAndTypeChecked) return; @@ -500,7 +500,7 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.StratifiedInlining == 0) { - Concurrency.Transform(linearTypeChecker, moverTypeChecker); + Concurrency.Transform(linearTypeChecker, civlTypeChecker); (new LinearEraser()).VisitProgram(program); if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null) { @@ -692,13 +692,13 @@ namespace Microsoft.Boogie /// - TypeCheckingError if a type checking error occurred /// - ResolvedAndTypeChecked if both resolution and type checking succeeded /// - public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out MoverTypeChecker moverTypeChecker) + public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out CivlTypeChecker civlTypeChecker) { Contract.Requires(program != null); Contract.Requires(bplFileName != null); linearTypeChecker = null; - moverTypeChecker = null; + civlTypeChecker = null; // ---------- Resolve ------------------------------------------------------------ @@ -735,11 +735,11 @@ namespace Microsoft.Boogie CollectModSets(program); - moverTypeChecker = new MoverTypeChecker(program); - moverTypeChecker.TypeCheck(); - if (moverTypeChecker.errorCount != 0) + civlTypeChecker = new CivlTypeChecker(program); + civlTypeChecker.TypeCheck(); + if (civlTypeChecker.errorCount != 0) { - Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, GetFileNameForConsole(bplFileName)); + Console.WriteLine("{0} type checking errors detected in {1}", civlTypeChecker.errorCount, GetFileNameForConsole(bplFileName)); return PipelineOutcome.TypeCheckingError; } @@ -1358,8 +1358,8 @@ namespace Microsoft.Boogie Program p = ParseBoogieProgram(new List { filename }, false); System.Diagnostics.Debug.Assert(p != null); LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; - PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out moverTypeChecker); + CivlTypeChecker civlTypeChecker; + PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out civlTypeChecker); System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked); return p; } -- cgit v1.2.3 From 7a2aec84f1d924086b6f8e0f3dcbde036e12345c Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 28 Sep 2015 09:47:27 -0700 Subject: update --- Source/Core/CommandLineOptions.cs | 6 +++--- Source/ExecutionEngine/ExecutionEngine.cs | 4 ++-- Source/VCGeneration/VC.cs | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) (limited to 'Source/ExecutionEngine/ExecutionEngine.cs') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 2dda1dd9..f4cba1dc 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -588,7 +588,7 @@ namespace Microsoft.Boogie { } } - public string OwickiGriesDesugaredOutputFile = null; + public string CivlDesugaredFile = null; public bool TrustAtomicityTypes = false; public bool TrustNonInterference = false; public int TrustLayersUpto = -1; @@ -915,9 +915,9 @@ namespace Microsoft.Boogie { } return true; - case "OwickiGries": + case "CivlDesugaredFile": if (ps.ConfirmArgumentCount(1)) { - OwickiGriesDesugaredOutputFile = args[ps.i]; + CivlDesugaredFile = args[ps.i]; } return true; diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index cf44a77f..15fdc081 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -502,11 +502,11 @@ namespace Microsoft.Boogie { Concurrency.Transform(linearTypeChecker, civlTypeChecker); (new LinearEraser()).VisitProgram(program); - if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null) + if (CommandLineOptions.Clo.CivlDesugaredFile != null) { int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; CommandLineOptions.Clo.PrintUnstructured = 1; - PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false, CommandLineOptions.Clo.PrettyPrint); + PrintBplFile(CommandLineOptions.Clo.CivlDesugaredFile, program, false, false, CommandLineOptions.Clo.PrettyPrint); CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; } } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index b457b383..94584027 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1632,7 +1632,7 @@ namespace VC { //use Duplicator and Substituter rather than new //nested IToken? //document expand attribute (search for {:ignore}, for example) - //fix up new CallCmd, new Requires, new Ensures in OwickiGries.cs + //fix up new CallCmd, new Requires, new Ensures in CivlRefinement.cs Func withType = (Expr from, Expr to) => { NAryExpr nFrom = from as NAryExpr; -- cgit v1.2.3 From 597a558b2fde558b7f5c581481fd51258aa37c46 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 30 Sep 2015 21:53:31 +0200 Subject: Improve output for diagnosing timeouts. --- Source/ExecutionEngine/ExecutionEngine.cs | 37 ++++++++++++++++++++++++++++-- Source/VCGeneration/ConditionGeneration.cs | 13 ++++++++++- Source/VCGeneration/VC.cs | 1 + 3 files changed, 48 insertions(+), 3 deletions(-) (limited to 'Source/ExecutionEngine/ExecutionEngine.cs') diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 15fdc081..4ab0a9c5 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1459,11 +1459,11 @@ namespace Microsoft.Boogie printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw); - ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit); + ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit, errors); } - private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit) + private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit, List errors) { ErrorInformation errorInfo = null; @@ -1476,6 +1476,35 @@ namespace Microsoft.Boogie if (implName != null && implTok != null) { errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId); + + // Report timed out assertions as auxiliary info. + if (errors != null) + { + var cmpr = new CounterexampleComparer(); + var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(cmpr).ToList(); + timedOutAssertions.Sort(cmpr); + int idx = 1; + foreach (Counterexample error in timedOutAssertions) + { + var callError = error as CallCounterexample; + var returnError = error as ReturnCounterexample; + var assertError = error as AssertCounterexample; + IToken tok = null; + if (callError != null) + { + tok = callError.FailingCall.tok; + } + else if (returnError != null) + { + tok = returnError.FailingReturn.tok; + } + else + { + tok = assertError.FailingAssert.tok; + } + errorInfo.AddAuxInfo(tok, string.Format("unverified assertion due to timeout ({0} of {1})", idx++, timedOutAssertions.Count)); + } + } } break; case VCGen.Outcome.OutOfMemory: @@ -1592,6 +1621,10 @@ namespace Microsoft.Boogie errors.Sort(new CounterexampleComparer()); foreach (Counterexample error in errors) { + if (error.IsAuxiliaryCexForDiagnosingTimeouts) + { + continue; + } var errorInfo = CreateErrorInformation(error, outcome); errorInfo.ImplementationName = implName; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 1f010757..ae0a1147 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -85,6 +85,7 @@ namespace Microsoft.Boogie { public string RequestId; public abstract byte[] Checksum { get; } public byte[] SugaredCmdChecksum; + public bool IsAuxiliaryCexForDiagnosingTimeouts; public Dictionary calleeCounterexamples; @@ -313,7 +314,7 @@ namespace Microsoft.Boogie { public abstract int GetLocation(); } - public class CounterexampleComparer : IComparer { + public class CounterexampleComparer : IComparer, IEqualityComparer { private int Compare(List bs1, List bs2) { @@ -375,6 +376,16 @@ namespace Microsoft.Boogie { } return -1; } + + public bool Equals(Counterexample x, Counterexample y) + { + return Compare(x, y) == 0; + } + + public int GetHashCode(Counterexample obj) + { + return 0; + } } public class AssertCounterexample : Counterexample { diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 94584027..33e2f928 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2113,6 +2113,7 @@ namespace VC { foreach (var cmd in assertCmds) { Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List(), null, null, context); + cex.IsAuxiliaryCexForDiagnosingTimeouts = true; callback.OnCounterexample(cex, msg); } } -- cgit v1.2.3 From f1d7e9e90e69854f8f33c474f544855abb8508c2 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 1 Oct 2015 22:57:55 +0200 Subject: Improve output for diagnosing timeouts. --- Source/ExecutionEngine/ExecutionEngine.cs | 49 ++++++++++++++++++++++++++----- 1 file changed, 42 insertions(+), 7 deletions(-) (limited to 'Source/ExecutionEngine/ExecutionEngine.cs') diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 4ab0a9c5..9623139a 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -135,7 +135,7 @@ namespace Microsoft.Boogie foreach (var e in errorInfo.Aux) { - if (!(skipExecutionTrace && e.Category.Contains("Execution trace"))) + if (!(skipExecutionTrace && e.Category != null && e.Category.Contains("Execution trace"))) { ReportBplError(e.Tok, e.FullMsg, false, tw); } @@ -1472,37 +1472,67 @@ namespace Microsoft.Boogie case VCGen.Outcome.ReachedBound: tw.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound)); break; + case VCGen.Outcome.Errors: case VCGen.Outcome.TimedOut: if (implName != null && implTok != null) { - errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId); - + if (outcome == ConditionGeneration.Outcome.TimedOut || (errors != null && errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts))) + { + errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification of '{1}' timed out after {0} seconds", timeLimit, implName), requestId); + } + // Report timed out assertions as auxiliary info. if (errors != null) { var cmpr = new CounterexampleComparer(); var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(cmpr).ToList(); timedOutAssertions.Sort(cmpr); - int idx = 1; + if (0 < timedOutAssertions.Count) + { + errorInfo.Msg += string.Format(" with {0} check(s) that timed out individually", timedOutAssertions.Count); + } foreach (Counterexample error in timedOutAssertions) { var callError = error as CallCounterexample; var returnError = error as ReturnCounterexample; var assertError = error as AssertCounterexample; IToken tok = null; + string msg = null; if (callError != null) { tok = callError.FailingCall.tok; + msg = callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold."; } else if (returnError != null) { tok = returnError.FailingReturn.tok; + msg = "A postcondition might not hold on this return path."; } else { tok = assertError.FailingAssert.tok; + if (assertError.FailingAssert is LoopInitAssertCmd) + { + msg = "This loop invariant might not hold on entry."; + } + else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd) + { + msg = "This loop invariant might not be maintained by the loop."; + } + else + { + msg = assertError.FailingAssert.ErrorData as string; + if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null) + { + msg = assertError.FailingAssert.ErrorMessage; + } + if (msg == null) + { + msg = "This assertion might not hold."; + } + } } - errorInfo.AddAuxInfo(tok, string.Format("unverified assertion due to timeout ({0} of {1})", idx++, timedOutAssertions.Count)); + errorInfo.AddAuxInfo(tok, msg, "Unverified check due to timeout"); } } } @@ -1531,6 +1561,10 @@ namespace Microsoft.Boogie er(errorInfo); } } + else + { + printer.WriteErrorInformation(errorInfo, tw); + } } } @@ -1604,8 +1638,9 @@ namespace Microsoft.Boogie } else { - Interlocked.Add(ref stats.ErrorCount, errors.Count); - if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, errors.Count); } + int cnt = errors.Where(e => !e.IsAuxiliaryCexForDiagnosingTimeouts).Count(); + Interlocked.Add(ref stats.ErrorCount, cnt); + if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, cnt); } } break; } -- cgit v1.2.3 From f049d2ec646244bc40964b36d961966fe2a3e4dc Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 16 Nov 2015 12:04:37 -0600 Subject: Add support for identifying unnecessary assumes. --- Source/Core/Absy.cs | 2 ++ Source/Core/AbsyCmd.cs | 12 +++++++++ Source/Core/CommandLineOptions.cs | 3 +++ Source/Core/ResolutionContext.cs | 12 +++++++++ Source/ExecutionEngine/ExecutionEngine.cs | 5 ++++ Source/Provers/SMTLib/ProverInterface.cs | 30 ++++++++++++++++++++-- Source/VCGeneration/Check.cs | 16 ++++++++++-- Source/VCGeneration/VC.cs | 28 ++++++++++++++------ Source/VCGeneration/Wlp.cs | 17 +++++++++--- Test/unnecessaryassumes/unnecessaryassumes0.bpl | 13 ++++++++++ .../unnecessaryassumes0.bpl.expect | 3 +++ Test/unnecessaryassumes/unnecessaryassumes1.bpl | 23 +++++++++++++++++ .../unnecessaryassumes1.bpl.expect | 3 +++ 13 files changed, 151 insertions(+), 16 deletions(-) create mode 100644 Test/unnecessaryassumes/unnecessaryassumes0.bpl create mode 100644 Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect create mode 100644 Test/unnecessaryassumes/unnecessaryassumes1.bpl create mode 100644 Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect (limited to 'Source/ExecutionEngine/ExecutionEngine.cs') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index d2243085..8be4f24e 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -696,6 +696,8 @@ namespace Microsoft.Boogie { } } + public readonly ISet NecessaryAssumes = new HashSet(); + public IEnumerable Blocks() { return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item); diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 404945a9..c33f0743 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2463,6 +2463,12 @@ namespace Microsoft.Boogie { } finally { rc.TypeBinderState = previousTypeBinderState; } + + var id = QKeyValue.FindStringAttribute(Attributes, "id"); + if (id != null) + { + rc.AddStatementId(tok, id); + } } public override void AddAssignedVariables(List vars) { @@ -2890,6 +2896,12 @@ namespace Microsoft.Boogie { public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); Expr.Resolve(rc); + + var id = QKeyValue.FindStringAttribute(Attributes, "id"); + if (id != null) + { + rc.AddStatementId(tok, id); + } } public override void AddAssignedVariables(List vars) { //Contract.Requires(vars != null); diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 3892bbc0..e9aa3ceb 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -479,6 +479,8 @@ namespace Microsoft.Boogie { public string AbstractHoudini = null; public bool UseUnsatCoreForContractInfer = false; public bool PrintAssignment = false; + // TODO(wuestholz): Add documentation for this flag. + public bool PrintNecessaryAssumes = false; public int InlineDepth = -1; public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values public bool UseUncheckedContracts = false; @@ -1619,6 +1621,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) || ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) || ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) || + ps.CheckBooleanFlag("printNecessaryAssumes", ref PrintNecessaryAssumes) || ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) || ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) || ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) || diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 474a91dd..279e00bf 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -339,6 +339,18 @@ namespace Microsoft.Boogie { varContext = varContext.ParentContext; } + public readonly ISet StatementIds = new HashSet(); + + public void AddStatementId(IToken tok, string name) + { + if (StatementIds.Contains(name)) + { + Error(tok, "more than one statement with same id: " + name); + return; + } + StatementIds.Add(name); + } + public void AddVariable(Variable var, bool global) { Contract.Requires(var != null); var previous = FindVariable(cce.NonNull(var.Name), !global); diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 9623139a..9bc855be 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1008,6 +1008,11 @@ namespace Microsoft.Boogie CleanupCheckers(requestId); } + if (CommandLineOptions.Clo.PrintNecessaryAssumes && program.NecessaryAssumes.Any()) + { + Console.WriteLine("Necessary assume command(s): {0}", string.Join(", ", program.NecessaryAssumes)); + } + cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close(); outputCollector.WriteMoreOutput(); diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index e93ecee9..cb8442e5 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -246,9 +246,9 @@ namespace Microsoft.Boogie.SMTLib // Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value // gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 ) - if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini)) + if (CommandLineOptions.Clo.PrintNecessaryAssumes || (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))) { - SendThisVC("(set-option :produce-unsat-cores true)"); + SendCommon("(set-option :produce-unsat-cores true)"); this.usingUnsatCore = true; } @@ -408,6 +408,15 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(push 1)"); SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); + + if (NamedAssumeVars != null) + { + foreach (var v in NamedAssumeVars) + { + SendThisVC(string.Format("(assert (! {0} :named {1}))", v, "aux$$" + v.Name)); + } + } + SendThisVC(vcString); FlushLogFile(); @@ -446,6 +455,7 @@ namespace Microsoft.Boogie.SMTLib if (options.Solver == SolverKind.Z3) { this.gen = gen; + SendThisVC("(reset)"); Namer.Reset(); common.Clear(); SetupAxiomBuilder(gen); @@ -1264,6 +1274,22 @@ namespace Microsoft.Boogie.SMTLib result = GetResponse(); + var reporter = handler as VC.VCGen.ErrorReporter; + // TODO(wuestholz): Is the reporter ever null? + if (NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null) + { + SendThisVC("(get-unsat-core)"); + var resp = Process.GetProverResponse(); + if (resp.Name != "") + { + reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length)); + } + foreach (var arg in resp.Arguments) + { + reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length)); + } + } + if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut) { #region Run timeout diagnostics diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 3c3b5cae..da445a00 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -346,7 +346,7 @@ namespace Microsoft.Boogie { } } - public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) { + public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, IList namedAssumeVars = null) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); Contract.Requires(handler != null); @@ -357,9 +357,18 @@ namespace Microsoft.Boogie { outputExn = null; this.handler = handler; - thmProver.Reset(gen); + if (namedAssumeVars != null && namedAssumeVars.Any()) + { + // TODO(wuestholz): Avoid doing a full reset. This is currently necessary for old versions of Z3 due to a bug. + thmProver.FullReset(gen); + } + else + { + thmProver.Reset(gen); + } SetTimeout(); proverStart = DateTime.UtcNow; + thmProver.NamedAssumeVars = namedAssumeVars; thmProver.BeginCheck(descriptiveName, vc, handler); // gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy @@ -386,6 +395,9 @@ namespace Microsoft.Boogie { // ----------------------------------------------------------------------------------------------- public abstract class ProverInterface { + + public IList NamedAssumeVars; + public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) { Contract.Requires(prog != null); diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 79f56934..2762fc72 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1386,7 +1386,8 @@ namespace VC { var exprGen = ctx.ExprGen; VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); - VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context); + var namedAssumeVars = new List(); + VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context, namedAssumeVars: namedAssumeVars); Contract.Assert(vc != null); if (!CommandLineOptions.Clo.UseLabels) @@ -1414,7 +1415,7 @@ namespace VC { string desc = cce.NonNull(impl.Name); if (no >= 0) desc += "_split" + no; - checker.BeginCheck(desc, vc, reporter); + checker.BeginCheck(desc, vc, reporter, namedAssumeVars); } private void SoundnessCheck(HashSet/*!*/>/*!*/ cache, Block/*!*/ orig, List/*!*/ copies) { @@ -1519,7 +1520,7 @@ namespace VC { } } - public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary/*!*/ label2absy, ProverContext proverContext) + public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary/*!*/ label2absy, ProverContext proverContext, IList namedAssumeVars = null) { Contract.Requires(impl != null); Contract.Requires(proverContext != null); @@ -1527,10 +1528,10 @@ namespace VC { Contract.Ensures(Contract.Result() != null); label2absy = new Dictionary(); - return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext); + return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext, namedAssumeVars: namedAssumeVars); } - public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary/*!*/ label2absy, ProverContext proverContext) { + public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary/*!*/ label2absy, ProverContext proverContext, IList namedAssumeVars = null) { Contract.Requires(impl != null); Contract.Requires(proverContext != null); Contract.Ensures(Contract.Result() != null); @@ -1567,7 +1568,8 @@ namespace VC { } break; case CommandLineOptions.VCVariety.DagIterative: - vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount); + // TODO(wuestholz): Support named assume statements not just for this encoding. + vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount, namedAssumeVars: namedAssumeVars); break; case CommandLineOptions.VCVariety.Doomed: vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount); @@ -2021,6 +2023,16 @@ namespace VC { protected ProverContext/*!*/ context; Program/*!*/ program; + public IEnumerable NecessaryAssumes + { + get { return program.NecessaryAssumes; } + } + + public void AddNecessaryAssume(string id) + { + program.NecessaryAssumes.Add(id); + } + public ErrorReporter(Dictionary/*!*/ gotoCmdOrigins, Dictionary/*!*/ label2absy, List/*!*/ blocks, @@ -3192,7 +3204,7 @@ namespace VC { Dictionary label2absy, ProverContext proverCtxt, out int assertionCount, - bool isPositiveContext = true) + bool isPositiveContext = true, IList namedAssumeVars = null) { Contract.Requires(blocks != null); Contract.Requires(proverCtxt != null); @@ -3252,7 +3264,7 @@ namespace VC { } VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext); - VCExpr vc = Wlp.Block(block, SuccCorrect, context); + VCExpr vc = Wlp.Block(block, SuccCorrect, context, namedAssumeVars); assertionCount += context.AssertionCount; VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool); diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index b4ee4c09..74b77188 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -48,7 +48,7 @@ namespace VC { public class Wlp { - public static VCExpr Block(Block b, VCExpr N, VCContext ctxt) + public static VCExpr Block(Block b, VCExpr N, VCContext ctxt, IList namedAssumeVars = null) //modifies ctxt.*; { Contract.Requires(b != null); @@ -63,7 +63,7 @@ namespace VC { for (int i = b.Cmds.Count; --i >= 0; ) { - res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt); + res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt, namedAssumeVars); } int id = b.UniqueId; @@ -87,7 +87,7 @@ namespace VC { /// /// Computes the wlp for an assert or assume command "cmd". /// - public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) { + internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt, IList namedAssumeVars = null) { Contract.Requires(cmd != null); Contract.Requires(N != null); Contract.Requires(ctxt != null); @@ -190,7 +190,16 @@ namespace VC { } } } - return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N); + var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); + + var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); + if (aid != null && namedAssumeVars != null) + { + var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool); + namedAssumeVars.Add(v); + expr = gen.ImpliesSimp(v, expr); + } + return gen.ImpliesSimp(expr, N); } else { Console.WriteLine(cmd.ToString()); Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl b/Test/unnecessaryassumes/unnecessaryassumes0.bpl new file mode 100644 index 00000000..a955495a --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie /printNecessaryAssumes "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:id "s0"} 0 < n; + assume {:id "s0"} 0 < n; +} + +procedure test1(n: int) +{ + assume {:id "s0"} 0 < n; +} diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect new file mode 100644 index 00000000..9e420fa7 --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect @@ -0,0 +1,3 @@ +unnecessaryassumes0.bpl(7,4): Error: more than one statement with same id: s0 +unnecessaryassumes0.bpl(12,4): Error: more than one statement with same id: s0 +2 name resolution errors detected in unnecessaryassumes0.bpl diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl new file mode 100644 index 00000000..04226dfd --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl @@ -0,0 +1,23 @@ +// RUN: %boogie /printNecessaryAssumes "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:id "s0"} 0 < n; + assert 0 <= n; // verified under s0 +} + +procedure test1(n: int) +{ + assume 0 < n; + assume {:id "s1"} n == 3; + assert 0 <= n; // verified under true +} + +procedure test2(n: int) +{ + assume 0 < n; + assume {:id "s2"} n <= 42; + assume {:id "s3"} 42 <= n; + assert n == 42; // verified under s2 and s3 +} diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect new file mode 100644 index 00000000..dd04bb46 --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect @@ -0,0 +1,3 @@ +Necessary assume command(s): s0, s3, s2 + +Boogie program verifier finished with 3 verified, 0 errors -- cgit v1.2.3