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 ++++++++++++++++++++++++++++++++++ 1 file changed, 1240 insertions(+) create mode 100644 Source/Concurrency/CivlRefinement.cs (limited to 'Source/Concurrency/CivlRefinement.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()); + } + } + } +} -- cgit v1.2.3 From c1b06a908ab1ed746672dd42eaf9417916a297cc Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 1 Oct 2015 09:40:42 -0700 Subject: another fix requested by Chris verification is performed now for all created layers --- Source/Concurrency/CivlRefinement.cs | 2 +- Source/Concurrency/CivlTypeChecker.cs | 20 -------------------- Source/Concurrency/YieldTypeChecker.cs | 2 +- Test/civl/DeviceCache.bpl.expect | 2 +- Test/civl/FlanaganQadeer.bpl.expect | 2 +- Test/civl/Program1.bpl.expect | 2 +- Test/civl/Program2.bpl.expect | 2 +- Test/civl/Program3.bpl.expect | 2 +- Test/civl/Program4.bpl.expect | 2 +- Test/civl/Program5.bpl.expect | 2 +- Test/civl/StoreBuffer.bpl.expect | 2 +- Test/civl/akash.bpl.expect | 2 +- Test/civl/alloc.bpl.expect | 2 +- Test/civl/bar.bpl.expect | 2 +- Test/civl/chris2.bpl.expect | 2 +- Test/civl/chris6.bpl | 14 ++++++++++++++ Test/civl/chris6.bpl.expect | 5 +++++ Test/civl/civl-paper.bpl.expect | 2 +- Test/civl/foo.bpl.expect | 2 +- Test/civl/ghost.bpl.expect | 2 +- Test/civl/linear-set.bpl.expect | 2 +- Test/civl/linear-set2.bpl.expect | 2 +- Test/civl/lock-introduced.bpl.expect | 2 +- Test/civl/lock.bpl.expect | 2 +- Test/civl/lock2.bpl.expect | 2 +- Test/civl/multiset.bpl.expect | 2 +- Test/civl/new1.bpl.expect | 2 +- Test/civl/one.bpl.expect | 2 +- Test/civl/par-incr.bpl.expect | 2 +- Test/civl/parallel1.bpl.expect | 2 +- Test/civl/parallel2.bpl.expect | 2 +- Test/civl/parallel4.bpl.expect | 2 +- Test/civl/parallel5.bpl.expect | 2 +- Test/civl/perm.bpl.expect | 2 +- Test/civl/t1.bpl.expect | 2 +- Test/civl/termination2.bpl.expect | 2 +- Test/civl/ticket.bpl.expect | 2 +- Test/civl/treiber-stack.bpl.expect | 2 +- Test/civl/wsq.bpl.expect | 2 +- 39 files changed, 55 insertions(+), 56 deletions(-) create mode 100644 Test/civl/chris6.bpl create mode 100644 Test/civl/chris6.bpl.expect (limited to 'Source/Concurrency/CivlRefinement.cs') diff --git a/Source/Concurrency/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs index 43d0f60c..8fc27be9 100644 --- a/Source/Concurrency/CivlRefinement.cs +++ b/Source/Concurrency/CivlRefinement.cs @@ -1212,7 +1212,7 @@ namespace Microsoft.Boogie public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List decls) { Program program = linearTypeChecker.program; - foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums) + foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums) { if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index dba7ab4b..5215bc52 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -486,26 +486,6 @@ namespace Microsoft.Boogie } } - 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 { diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index a69f066d..027e7e83 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -141,7 +141,7 @@ namespace Microsoft.Boogie Graph implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; - foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums) + foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums) { if (layerNum > specLayerNum) continue; YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers); diff --git a/Test/civl/DeviceCache.bpl.expect b/Test/civl/DeviceCache.bpl.expect index c4cf5ccf..129e60e2 100644 --- a/Test/civl/DeviceCache.bpl.expect +++ b/Test/civl/DeviceCache.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 30 verified, 0 errors +Boogie program verifier finished with 39 verified, 0 errors diff --git a/Test/civl/FlanaganQadeer.bpl.expect b/Test/civl/FlanaganQadeer.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/FlanaganQadeer.bpl.expect +++ b/Test/civl/FlanaganQadeer.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/Program1.bpl.expect b/Test/civl/Program1.bpl.expect index 41374b00..00ddb38b 100644 --- a/Test/civl/Program1.bpl.expect +++ b/Test/civl/Program1.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/Program2.bpl.expect b/Test/civl/Program2.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/Program2.bpl.expect +++ b/Test/civl/Program2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/Program3.bpl.expect b/Test/civl/Program3.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/Program3.bpl.expect +++ b/Test/civl/Program3.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/Program4.bpl.expect +++ b/Test/civl/Program4.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/Program5.bpl.expect b/Test/civl/Program5.bpl.expect index fde7e712..4bcb1071 100644 --- a/Test/civl/Program5.bpl.expect +++ b/Test/civl/Program5.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 18 verified, 0 errors +Boogie program verifier finished with 21 verified, 0 errors diff --git a/Test/civl/StoreBuffer.bpl.expect b/Test/civl/StoreBuffer.bpl.expect index 8c74fe2e..1931ffd2 100644 --- a/Test/civl/StoreBuffer.bpl.expect +++ b/Test/civl/StoreBuffer.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 17 verified, 0 errors +Boogie program verifier finished with 27 verified, 0 errors diff --git a/Test/civl/akash.bpl.expect b/Test/civl/akash.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/akash.bpl.expect +++ b/Test/civl/akash.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/alloc.bpl.expect b/Test/civl/alloc.bpl.expect index f08c6e00..4bcb1071 100644 --- a/Test/civl/alloc.bpl.expect +++ b/Test/civl/alloc.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 12 verified, 0 errors +Boogie program verifier finished with 21 verified, 0 errors diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect index 810c93bf..be6722fe 100644 --- a/Test/civl/bar.bpl.expect +++ b/Test/civl/bar.bpl.expect @@ -10,4 +10,4 @@ Execution trace: (0,0): anon00 (0,0): inline$Impl_YieldChecker_PC_1$0$L0 -Boogie program verifier finished with 3 verified, 2 errors +Boogie program verifier finished with 8 verified, 2 errors diff --git a/Test/civl/chris2.bpl.expect b/Test/civl/chris2.bpl.expect index ddb8537e..f3b66f4a 100644 --- a/Test/civl/chris2.bpl.expect +++ b/Test/civl/chris2.bpl.expect @@ -15,4 +15,4 @@ Execution trace: Execution trace: (0,0): this_A -Boogie program verifier finished with 1 verified, 4 errors +Boogie program verifier finished with 2 verified, 4 errors diff --git a/Test/civl/chris6.bpl b/Test/civl/chris6.bpl new file mode 100644 index 00000000..a0aecf1e --- /dev/null +++ b/Test/civl/chris6.bpl @@ -0,0 +1,14 @@ +// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure{:extern}{:yields}{:layer 1,2} P1(); + requires{:layer 1} false; + ensures{:atomic} |{ A: return true; }|; + +procedure{:yields}{:layer 2,3} P2() + ensures{:atomic} |{ A: return true; }|; +{ + assert{:layer 1} false; + yield; + call P1(); + yield; +} diff --git a/Test/civl/chris6.bpl.expect b/Test/civl/chris6.bpl.expect new file mode 100644 index 00000000..229e4e10 --- /dev/null +++ b/Test/civl/chris6.bpl.expect @@ -0,0 +1,5 @@ +chris6.bpl(10,3): Error BP5001: This assertion might not hold. +Execution trace: + chris6.bpl(10,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/civl/civl-paper.bpl.expect b/Test/civl/civl-paper.bpl.expect index 11d204a8..bd1df2f9 100644 --- a/Test/civl/civl-paper.bpl.expect +++ b/Test/civl/civl-paper.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 35 verified, 0 errors +Boogie program verifier finished with 45 verified, 0 errors diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect index 41e30691..44a93860 100644 --- a/Test/civl/foo.bpl.expect +++ b/Test/civl/foo.bpl.expect @@ -5,4 +5,4 @@ Execution trace: foo.bpl(14,3): inline$Incr_1$0$A (0,0): inline$Impl_YieldChecker_PC_1$0$L0 -Boogie program verifier finished with 4 verified, 1 error +Boogie program verifier finished with 9 verified, 1 error diff --git a/Test/civl/ghost.bpl.expect b/Test/civl/ghost.bpl.expect index 9823d44a..76a9a2bf 100644 --- a/Test/civl/ghost.bpl.expect +++ b/Test/civl/ghost.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 6 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/linear-set.bpl.expect b/Test/civl/linear-set.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/linear-set.bpl.expect +++ b/Test/civl/linear-set.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/linear-set2.bpl.expect b/Test/civl/linear-set2.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/linear-set2.bpl.expect +++ b/Test/civl/linear-set2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/lock-introduced.bpl.expect b/Test/civl/lock-introduced.bpl.expect index f08c6e00..8c74fe2e 100644 --- a/Test/civl/lock-introduced.bpl.expect +++ b/Test/civl/lock-introduced.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 12 verified, 0 errors +Boogie program verifier finished with 17 verified, 0 errors diff --git a/Test/civl/lock.bpl.expect b/Test/civl/lock.bpl.expect index 3e6d423a..76a9a2bf 100644 --- a/Test/civl/lock.bpl.expect +++ b/Test/civl/lock.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/lock2.bpl.expect b/Test/civl/lock2.bpl.expect index 3e6d423a..76a9a2bf 100644 --- a/Test/civl/lock2.bpl.expect +++ b/Test/civl/lock2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/multiset.bpl.expect b/Test/civl/multiset.bpl.expect index 0a77c517..63682bb4 100644 --- a/Test/civl/multiset.bpl.expect +++ b/Test/civl/multiset.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 78 verified, 0 errors +Boogie program verifier finished with 85 verified, 0 errors diff --git a/Test/civl/new1.bpl.expect b/Test/civl/new1.bpl.expect index 41374b00..00ddb38b 100644 --- a/Test/civl/new1.bpl.expect +++ b/Test/civl/new1.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/one.bpl.expect b/Test/civl/one.bpl.expect index 37fad75c..41374b00 100644 --- a/Test/civl/one.bpl.expect +++ b/Test/civl/one.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 1 verified, 0 errors +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/par-incr.bpl.expect b/Test/civl/par-incr.bpl.expect index 00ddb38b..3e3dc54b 100644 --- a/Test/civl/par-incr.bpl.expect +++ b/Test/civl/par-incr.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 7 verified, 0 errors diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect index 889ee4f2..fa974099 100644 --- a/Test/civl/parallel1.bpl.expect +++ b/Test/civl/parallel1.bpl.expect @@ -5,4 +5,4 @@ Execution trace: parallel1.bpl(14,3): inline$Incr_1$0$A (0,0): inline$Impl_YieldChecker_PC_1$0$L0 -Boogie program verifier finished with 3 verified, 1 error +Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/parallel2.bpl.expect b/Test/civl/parallel2.bpl.expect index 3e6d423a..12041afe 100644 --- a/Test/civl/parallel2.bpl.expect +++ b/Test/civl/parallel2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 10 verified, 0 errors diff --git a/Test/civl/parallel4.bpl.expect b/Test/civl/parallel4.bpl.expect index 2d4c8148..baf228c8 100644 --- a/Test/civl/parallel4.bpl.expect +++ b/Test/civl/parallel4.bpl.expect @@ -3,4 +3,4 @@ Execution trace: parallel4.bpl(29,5): anon0 (0,0): anon01 -Boogie program verifier finished with 3 verified, 1 error +Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/parallel5.bpl.expect b/Test/civl/parallel5.bpl.expect index 3e6d423a..12041afe 100644 --- a/Test/civl/parallel5.bpl.expect +++ b/Test/civl/parallel5.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 10 verified, 0 errors diff --git a/Test/civl/perm.bpl.expect b/Test/civl/perm.bpl.expect index 41374b00..00ddb38b 100644 --- a/Test/civl/perm.bpl.expect +++ b/Test/civl/perm.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect index fcef7e58..27a208d4 100644 --- a/Test/civl/t1.bpl.expect +++ b/Test/civl/t1.bpl.expect @@ -6,4 +6,4 @@ Execution trace: t1.bpl(25,21): inline$SetG_1$0$A (0,0): inline$Impl_YieldChecker_A_1$0$L1 -Boogie program verifier finished with 4 verified, 1 error +Boogie program verifier finished with 9 verified, 1 error diff --git a/Test/civl/termination2.bpl.expect b/Test/civl/termination2.bpl.expect index 37fad75c..41374b00 100644 --- a/Test/civl/termination2.bpl.expect +++ b/Test/civl/termination2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 1 verified, 0 errors +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect index b072912b..dc45a0ee 100644 --- a/Test/civl/ticket.bpl.expect +++ b/Test/civl/ticket.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 16 verified, 0 errors +Boogie program verifier finished with 24 verified, 0 errors diff --git a/Test/civl/treiber-stack.bpl.expect b/Test/civl/treiber-stack.bpl.expect index 9823d44a..76a9a2bf 100644 --- a/Test/civl/treiber-stack.bpl.expect +++ b/Test/civl/treiber-stack.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 6 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/wsq.bpl.expect b/Test/civl/wsq.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/wsq.bpl.expect +++ b/Test/civl/wsq.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors -- cgit v1.2.3 From 0569be4268fe9c6174ff14cd0e9ab1a8170cfd21 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 1 Oct 2015 17:34:53 -0700 Subject: added a fix to check all layers: created layer of actions or layers in requires, ensures, or asserts --- Source/Concurrency/CivlRefinement.cs | 2 +- Source/Concurrency/CivlTypeChecker.cs | 31 +++++++++++++------------------ Source/Concurrency/YieldTypeChecker.cs | 2 +- 3 files changed, 15 insertions(+), 20 deletions(-) (limited to 'Source/Concurrency/CivlRefinement.cs') diff --git a/Source/Concurrency/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs index 8fc27be9..dfe50ef9 100644 --- a/Source/Concurrency/CivlRefinement.cs +++ b/Source/Concurrency/CivlRefinement.cs @@ -1212,7 +1212,7 @@ namespace Microsoft.Boogie public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List decls) { Program program = linearTypeChecker.program; - foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums) + foreach (int layerNum in civlTypeChecker.AllLayerNums) { if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index 5215bc52..430c0d2c 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -486,20 +486,27 @@ namespace Microsoft.Boogie } } - private HashSet allCreatedLayerNums; - public IEnumerable AllCreatedLayerNums + private HashSet allLayerNums; + public IEnumerable AllLayerNums { get { - if (allCreatedLayerNums == null) + if (allLayerNums == null) { - allCreatedLayerNums = new HashSet(); + allLayerNums = new HashSet(); foreach (ActionInfo actionInfo in procToActionInfo.Values) { - allCreatedLayerNums.Add(actionInfo.createdAtLayerNum); + allLayerNums.Add(actionInfo.createdAtLayerNum); + } + foreach (var layerNums in absyToLayerNums.Values) + { + foreach (var layer in layerNums) + { + allLayerNums.Add(layer); + } } } - return allCreatedLayerNums; + return allLayerNums; } } @@ -705,18 +712,6 @@ namespace Microsoft.Boogie 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; diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 027e7e83..ed59d3ad 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -141,7 +141,7 @@ namespace Microsoft.Boogie Graph implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; - foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums) + foreach (int layerNum in civlTypeChecker.AllLayerNums) { if (layerNum > specLayerNum) continue; YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers); -- cgit v1.2.3 From a6b78b0ea28c22744fa846d7729b5c50247f9987 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Fri, 16 Oct 2015 14:08:21 -0700 Subject: bug fix in the type checking of calls to atomic procedures --- Source/Concurrency/CivlRefinement.cs | 14 +-- Source/Concurrency/CivlTypeChecker.cs | 219 ++++++++++++++++++---------------- Test/civl/chris8.bpl | 15 +++ Test/civl/chris8.bpl.expect | 2 + Test/civl/wsq.bpl | 14 +-- 5 files changed, 139 insertions(+), 125 deletions(-) create mode 100644 Test/civl/chris8.bpl create mode 100644 Test/civl/chris8.bpl.expect (limited to 'Source/Concurrency/CivlRefinement.cs') diff --git a/Source/Concurrency/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs index dfe50ef9..75ff2358 100644 --- a/Source/Concurrency/CivlRefinement.cs +++ b/Source/Concurrency/CivlRefinement.cs @@ -315,19 +315,9 @@ namespace Microsoft.Boogie foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys) { LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v]; - if (info.isGhost) + if (layerNum < info.layer) { - if (info.layer != layerNum) - { - availableVars.Remove(v); - } - } - else - { - if (layerNum < info.layer) - { - availableVars.Remove(v); - } + availableVars.Remove(v); } } return availableVars; diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index 71feb927..b426d9ed 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -333,26 +333,24 @@ namespace Microsoft.Boogie public class AtomicProcedureInfo { public bool isPure; - public HashSet layers; + public LayerRange layerRange; public AtomicProcedureInfo() { this.isPure = true; - this.layers = null; + this.layerRange = null; } - public AtomicProcedureInfo(HashSet layers) + public AtomicProcedureInfo(LayerRange layerRange) { this.isPure = false; - this.layers = layers; + this.layerRange = layerRange; } } public class LocalVariableInfo { - public bool isGhost; public int layer; - public LocalVariableInfo(bool isGhost, int layer) + public LocalVariableInfo(int layer) { - this.isGhost = isGhost; this.layer = layer; } } @@ -364,7 +362,6 @@ namespace Microsoft.Boogie Implementation enclosingImpl; HashSet sharedVarsAccessed; int introducedLocalVarsUpperBound; - int ghostVarIntroLayerAllowed; public Program program; public int errorCount; @@ -373,28 +370,15 @@ namespace Microsoft.Boogie public Dictionary procToAtomicProcedureInfo; public Dictionary> absyToLayerNums; public Dictionary localVarToLocalVariableInfo; + Dictionary pureCallLayer; 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; + return pureCallLayer[callCmd] <= layerNum; } else { @@ -456,13 +440,13 @@ namespace Microsoft.Boogie 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(); + this.procToAtomicProcedureInfo = new Dictionary(); + this.pureCallLayer = new Dictionary(); foreach (var g in program.GlobalVariables) { @@ -553,27 +537,39 @@ namespace Microsoft.Boogie foreach (var proc in program.Procedures) { if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue; - var procLayerNums = RemoveDuplicatesAndSort(FindLayers(proc.Attributes)); + var procLayerNums = 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"); + continue; } - 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) + int lower, upper; + if (procLayerNums.Count == 1) + { + lower = procLayerNums[0]; + upper = procLayerNums[0]; + } + else if (procLayerNums.Count == 2) { - procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(new HashSet(procLayerNums)); + lower = procLayerNums[0]; + upper = procLayerNums[1]; + if (lower >= upper) + { + Error(proc, "Lower layer must be less than upper layer"); + continue; + } } else { - Error(proc, "An atomic procedure with more than one layer must not modify a global variable"); + Error(proc, "Atomic procedure must specify a layer range"); + continue; } + LayerRange layerRange = new LayerRange(lower, upper); + procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(layerRange); } if (errorCount > 0) return; @@ -592,7 +588,7 @@ namespace Microsoft.Boogie this.sharedVarsAccessed = new HashSet(); (new PurityChecker(this)).VisitImplementation(impl); LayerRange upperBound = FindLayerRange(); - LayerRange lowerBound = new LayerRange(atomicProcedureInfo.layers); + LayerRange lowerBound = atomicProcedureInfo.layerRange; if (!lowerBound.Subset(upperBound)) { Error(impl, "Atomic procedure cannot access global variable"); @@ -695,14 +691,14 @@ namespace Microsoft.Boogie Variable v = proc.InParams[i]; var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum); if (layer == int.MinValue) continue; - localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer); + localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer); } for (int i = 0; i < proc.OutParams.Count; i++) { Variable v = proc.OutParams[i]; var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum); if (layer == int.MinValue) continue; - localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer); + localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer); } } foreach (Implementation node in program.Implementations) @@ -712,21 +708,21 @@ namespace Microsoft.Boogie { var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum); if (layer == int.MinValue) continue; - localVarToLocalVariableInfo[v] = new LocalVariableInfo(QKeyValue.FindBoolAttribute(node.Attributes, "ghost"), layer); + localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer); } for (int i = 0; i < node.Proc.InParams.Count; i++) { Variable v = node.Proc.InParams[i]; if (!localVarToLocalVariableInfo.ContainsKey(v)) continue; var layer = localVarToLocalVariableInfo[v].layer; - localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(false, layer); + localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(layer); } for (int i = 0; i < node.Proc.OutParams.Count; i++) { Variable v = node.Proc.OutParams[i]; if (!localVarToLocalVariableInfo.ContainsKey(v)) continue; var layer = localVarToLocalVariableInfo[v].layer; - localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(false, layer); + localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(layer); } } if (errorCount > 0) return; @@ -818,13 +814,17 @@ namespace Microsoft.Boogie } for (int i = 0; i < node.Ins.Count; i++) { - var formal = node.Proc.InParams[i]; - if (localVarToLocalVariableInfo.ContainsKey(formal)) + Visit(node.Ins[i]); + if (introducedLocalVarsUpperBound != int.MinValue) { - introducedLocalVarsUpperBound = localVarToLocalVariableInfo[formal].layer; + var formal = node.Proc.InParams[i]; + if (!localVarToLocalVariableInfo.ContainsKey(formal) || + introducedLocalVarsUpperBound > localVarToLocalVariableInfo[formal].layer) + { + Error(node, "An introduced local variable is accessed but not available"); + } + introducedLocalVarsUpperBound = int.MinValue; } - Visit(node.Ins[i]); - introducedLocalVarsUpperBound = int.MinValue; } for (int i = 0; i < node.Outs.Count; i++) { @@ -840,69 +840,83 @@ namespace Microsoft.Boogie } 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) + var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc]; + if (atomicProcedureInfo.isPure) { - if (localVarToLocalVariableInfo.ContainsKey(ie.Decl)) + if (node.Outs.Count > 0) { - var localVariableInfo = localVarToLocalVariableInfo[ie.Decl]; - if (introducedLocalVarsUpperBound == int.MinValue) + int inferredLayer = int.MinValue; + foreach (var ie in node.Outs) { - introducedLocalVarsUpperBound = localVariableInfo.layer; - isGhost = localVariableInfo.isGhost; - var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc]; - if (!atomicProcedureInfo.isPure) + if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) continue; + if (inferredLayer < localVarToLocalVariableInfo[ie.Decl].layer) { - if (!atomicProcedureInfo.layers.Contains(introducedLocalVarsUpperBound)) + inferredLayer = localVarToLocalVariableInfo[ie.Decl].layer; + } + } + pureCallLayer[node] = inferredLayer; + if (inferredLayer != int.MinValue) + { + foreach (var ie in node.Outs) + { + if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) { - Error(node, "Layer of output variable must be a layer of the callee"); + Error(node, "Output variable must be introduced"); } - if (!isGhost && !atomicProcedureInfo.layers.Contains(enclosingProcLayerNum)) + else if (inferredLayer != localVarToLocalVariableInfo[ie.Decl].layer) { - Error(node, "The creation layer of caller must be a layer of the callee"); + Error(node, "All output variables must be introduced at the same layer"); } } } - else + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + foreach (var e in node.Ins) { - if (localVariableInfo.layer != introducedLocalVarsUpperBound) + Visit(e); + if (inferredLayer < introducedLocalVarsUpperBound) { - Error(node, "All outputs must have the same layer"); - } - if (localVariableInfo.isGhost != isGhost) - { - Error(node, "Outputs are either all ghost or all introduced"); + Error(node, "An introduced local variable is not accessible"); } + introducedLocalVarsUpperBound = int.MinValue; } } else { - Error(node, "Output variable must be a ghost or introduced local variable"); + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + int inferredLayer = int.MinValue; + foreach (var e in node.Ins) + { + Visit(e); + if (inferredLayer < introducedLocalVarsUpperBound) + { + inferredLayer = introducedLocalVarsUpperBound; + } + introducedLocalVarsUpperBound = int.MinValue; + } + pureCallLayer[node] = inferredLayer; } } - - if (node.Proc.Modifies.Count > 0) + else { - var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc]; - if (!atomicProcedureInfo.layers.Contains(enclosingProcLayerNum)) + if (enclosingProcLayerNum != atomicProcedureInfo.layerRange.upperLayerNum) { - Error(node, "The layer of called atomic procedure must be identical to the creation layer of callee"); + Error(node, "Creation layer of caller must be the upper bound of the layer range of callee"); + } + foreach (var ie in node.Proc.Modifies) + { + if (enclosingProcLayerNum != globalVarToSharedVarInfo[ie.Decl].introLayerNum) + { + Error(node, "Creation layer of caller must be identical to the introduction layer of modified variable"); + } + } + foreach (var ie in node.Outs) + { + if (localVarToLocalVariableInfo.ContainsKey(ie.Decl) && + enclosingProcLayerNum == localVarToLocalVariableInfo[ie.Decl].layer) + continue; + Error(node, "Output variable must be introduced at the creation layer of caller"); } - introducedLocalVarsUpperBound = enclosingProcLayerNum; - } - foreach (var e in node.Ins) - { - Visit(e); } - introducedLocalVarsUpperBound = int.MinValue; return node; } else @@ -973,19 +987,9 @@ namespace Microsoft.Boogie else if ((node.Decl is Formal || node.Decl is Variable) && localVarToLocalVariableInfo.ContainsKey(node.Decl)) { var localVariableInfo = localVarToLocalVariableInfo[node.Decl]; - if (localVariableInfo.isGhost) + if (introducedLocalVarsUpperBound < localVariableInfo.layer) { - if (ghostVarIntroLayerAllowed != localVariableInfo.layer) - { - Error(node, "Ghost variable inaccessible"); - } - } - else - { - if (introducedLocalVarsUpperBound < localVariableInfo.layer) - { - Error(node, "Introduced variable inaccessible"); - } + introducedLocalVarsUpperBound = localVariableInfo.layer; } } return base.VisitIdentifierExpr(node); @@ -1003,9 +1007,12 @@ namespace Microsoft.Boogie { sharedVarsAccessed = new HashSet(); Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); - introducedLocalVarsUpperBound = Least(FindLayers(ensures.Attributes)); base.VisitEnsures(ensures); CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum); + if (introducedLocalVarsUpperBound > Least(FindLayers(ensures.Attributes))) + { + Error(ensures, "An introduced local variable is accessed but not available"); + } introducedLocalVarsUpperBound = int.MinValue; sharedVarsAccessed = null; } @@ -1016,9 +1023,12 @@ namespace Microsoft.Boogie { sharedVarsAccessed = new HashSet(); Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); - introducedLocalVarsUpperBound = Least(FindLayers(requires.Attributes)); base.VisitRequires(requires); CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum); + if (introducedLocalVarsUpperBound > Least(FindLayers(requires.Attributes))) + { + Error(requires, "An introduced local variable is accessed but not available"); + } introducedLocalVarsUpperBound = int.MinValue; sharedVarsAccessed = null; return requires; @@ -1033,16 +1043,13 @@ namespace Microsoft.Boogie } 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); + if (introducedLocalVarsUpperBound > Least(FindLayers(node.Attributes))) + { + Error(node, "An introduced local variable is accessed but not available"); + } introducedLocalVarsUpperBound = int.MinValue; - ghostVarIntroLayerAllowed = int.MinValue; sharedVarsAccessed = null; return node; } @@ -1115,7 +1122,7 @@ namespace Microsoft.Boogie { civlTypeChecker.Error(node, "Pure procedure can only call pure procedures"); } - else if (!callerInfo.layers.IsSubsetOf(calleeInfo.layers)) + else if (!callerInfo.layerRange.Subset(calleeInfo.layerRange)) { civlTypeChecker.Error(node, "Caller layers must be subset of callee layers"); } diff --git a/Test/civl/chris8.bpl b/Test/civl/chris8.bpl new file mode 100644 index 00000000..070cfec4 --- /dev/null +++ b/Test/civl/chris8.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var{:layer 1,1} x:int; + +procedure{:layer 1}{:extern} P1(i:int); +procedure{:pure}{:extern} P2(j:int); + +procedure{:yields}{:layer 1,2} A1({:layer 1}i:int) + ensures {:atomic} |{ A: return true; }|; +{ + yield; + call P1(i); + call P2(i); + yield; +} diff --git a/Test/civl/chris8.bpl.expect b/Test/civl/chris8.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/civl/chris8.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl index 39dad919..0a2227b6 100644 --- a/Test/civl/wsq.bpl +++ b/Test/civl/wsq.bpl @@ -89,9 +89,9 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|; { var t: int; - var {:ghost} {:layer 3} oldH:int; - var {:ghost} {:layer 3} oldT:int; - var {:ghost} {:layer 3} oldStatusT:bool; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; + var {:layer 3} oldStatusT:bool; call oldH, oldT := GhostRead(); yield; @@ -142,8 +142,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu { var h, t: int; var chk: bool; - var {:ghost} {:layer 3} oldH:int; - var {:ghost} {:layer 3} oldT:int; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; call oldH, oldT := GhostRead(); yield; @@ -304,8 +304,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu { var h, t: int; var chk: bool; - var {:ghost} {:layer 3} oldH:int; - var {:ghost} {:layer 3} oldT:int; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; call oldH, oldT := GhostRead(); yield; -- cgit v1.2.3