diff options
| -rw-r--r-- | Source/Concurrency/CivlRefinement.cs (renamed from Source/Concurrency/OwickiGries.cs) | 80 | ||||
| -rw-r--r-- | Source/Concurrency/CivlTypeChecker.cs (renamed from Source/Concurrency/TypeCheck.cs) | 41 | ||||
| -rw-r--r-- | Source/Concurrency/Concurrency.csproj | 8 | ||||
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 26 | ||||
| -rw-r--r-- | Source/Concurrency/Program.cs | 12 | ||||
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 36 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 22 |
7 files changed, 112 insertions, 113 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/CivlRefinement.cs index d861e2f3..43d0f60c 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/CivlRefinement.cs @@ -13,7 +13,7 @@ namespace Microsoft.Boogie { public class MyDuplicator : Duplicator { - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; public int layerNum; Procedure enclosingProc; Implementation enclosingImpl; @@ -23,9 +23,9 @@ namespace Microsoft.Boogie public HashSet<Procedure> yieldingProcs; public List<Implementation> impls; - public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum) + public MyDuplicator(CivlTypeChecker civlTypeChecker, int layerNum) { - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.layerNum = layerNum; this.enclosingProc = null; this.enclosingImpl = null; @@ -38,19 +38,19 @@ namespace Microsoft.Boogie private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds) { - int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; + int enclosingProcLayerNum = civlTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; Procedure originalProc = originalCallCmd.Proc; - if (moverTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc)) + if (civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc)) { - if (moverTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum)) + if (civlTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum)) { newCmds.Add(callCmd); } } - else if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc)) + else if (civlTypeChecker.procToActionInfo.ContainsKey(originalProc)) { - AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo; + AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo; if (atomicActionInfo != null && atomicActionInfo.gate.Count > 0 && layerNum == enclosingProcLayerNum) { newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) }))); @@ -78,7 +78,7 @@ namespace Microsoft.Boogie int maxCalleeLayerNum = 0; foreach (CallCmd iter in originalParCallCmd.CallCmds) { - int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum; + int calleeLayerNum = civlTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum; if (calleeLayerNum > maxCalleeLayerNum) maxCalleeLayerNum = calleeLayerNum; } @@ -156,7 +156,7 @@ namespace Microsoft.Boogie public override Procedure VisitProcedure(Procedure node) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(node)) + if (!civlTypeChecker.procToActionInfo.ContainsKey(node)) return node; if (!procMap.ContainsKey(node)) { @@ -167,7 +167,7 @@ namespace Microsoft.Boogie proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies); proc.OutParams = this.VisitVariableSeq(node.OutParams); - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[node]; if (actionInfo.createdAtLayerNum < layerNum) { proc.Requires = new List<Requires>(); @@ -210,7 +210,7 @@ namespace Microsoft.Boogie } procMap[node] = proc; proc.Modifies = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x))); } return procMap[node]; } @@ -232,7 +232,7 @@ namespace Microsoft.Boogie Requires requires = base.VisitRequires(node); if (node.Free) return requires; - if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) requires.Condition = Expr.True; return requires; } @@ -242,12 +242,12 @@ namespace Microsoft.Boogie Ensures ensures = base.VisitEnsures(node); if (node.Free) return ensures; - AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo; + AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo; bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node; - if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + if (isAtomicSpecification || !civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) { ensures.Condition = Expr.True; - ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes); + ensures.Attributes = CivlRefinement.RemoveMoverAttribute(ensures.Attributes); } return ensures; } @@ -255,16 +255,16 @@ namespace Microsoft.Boogie public override Cmd VisitAssertCmd(AssertCmd node) { AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node); - if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) assertCmd.Expr = Expr.True; return assertCmd; } } - public class OwickiGries + public class CivlRefinement { LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; Dictionary<Absy, Absy> absyMap; Dictionary<Implementation, Implementation> implMap; HashSet<Procedure> yieldingProcs; @@ -281,17 +281,17 @@ namespace Microsoft.Boogie Expr beta; HashSet<Variable> frame; - public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator) + public CivlRefinement(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, MyDuplicator duplicator) { this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; + 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<IdentifierExpr>(); - foreach (Variable g in moverTypeChecker.SharedVariables) + foreach (Variable g in civlTypeChecker.SharedVariables) { globalMods.Add(Expr.Ident(g)); } @@ -304,17 +304,17 @@ namespace Microsoft.Boogie private IEnumerable<Variable> AvailableLinearVars(Absy absy) { HashSet<Variable> availableVars = new HashSet<Variable>(linearTypeChecker.AvailableLinearVars(absyMap[absy])); - foreach (var g in moverTypeChecker.globalVarToSharedVarInfo.Keys) + foreach (var g in civlTypeChecker.globalVarToSharedVarInfo.Keys) { - SharedVariableInfo info = moverTypeChecker.globalVarToSharedVarInfo[g]; + SharedVariableInfo info = civlTypeChecker.globalVarToSharedVarInfo[g]; if (!(info.introLayerNum <= layerNum && layerNum <= info.hideLayerNum)) { availableVars.Remove(g); } } - foreach (var v in moverTypeChecker.localVarToLocalVariableInfo.Keys) + foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys) { - LocalVariableInfo info = moverTypeChecker.localVarToLocalVariableInfo[v]; + LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v]; if (info.isGhost) { if (info.layer != layerNum) @@ -754,7 +754,7 @@ namespace Microsoft.Boogie } Procedure originalProc = implMap[impl].Proc; - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[originalProc]; if (actionInfo.createdAtLayerNum == this.layerNum) { pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool)); @@ -777,11 +777,11 @@ namespace Microsoft.Boogie foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]); } Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); - frame = new HashSet<Variable>(moverTypeChecker.SharedVariables); - foreach (Variable v in moverTypeChecker.SharedVariables) + frame = new HashSet<Variable>(civlTypeChecker.SharedVariables); + foreach (Variable v in civlTypeChecker.SharedVariables) { - if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || - moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum) + if (civlTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || + civlTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum) { frame.Remove(v); } @@ -798,7 +798,7 @@ namespace Microsoft.Boogie } else { - Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, new HashSet<Variable>())).TransitionRelationCompute(true); + Expr betaExpr = (new MoverCheck.TransitionRelationComputation(civlTypeChecker.program, atomicActionInfo, frame, new HashSet<Variable>())).TransitionRelationCompute(true); beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr); Expr alphaExpr = Expr.True; foreach (AssertCmd assertCmd in atomicActionInfo.gate) @@ -1209,31 +1209,31 @@ namespace Microsoft.Boogie return decls; } - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls) { Program program = linearTypeChecker.program; - foreach (int layerNum in moverTypeChecker.AllImplementedLayerNums) + foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums) { if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; - MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum); + MyDuplicator duplicator = new MyDuplicator(civlTypeChecker, layerNum); foreach (var proc in program.Procedures) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue; + if (!civlTypeChecker.procToActionInfo.ContainsKey(proc)) continue; Procedure duplicateProc = duplicator.VisitProcedure(proc); decls.Add(duplicateProc); } decls.AddRange(duplicator.impls); - OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator); + CivlRefinement civlTransform = new CivlRefinement(linearTypeChecker, civlTypeChecker, duplicator); foreach (var impl in program.Implementations) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum) + if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum) continue; Implementation duplicateImpl = duplicator.VisitImplementation(impl); - ogTransform.TransformImpl(duplicateImpl); + civlTransform.TransformImpl(duplicateImpl); decls.Add(duplicateImpl); } - decls.AddRange(ogTransform.Collect()); + decls.AddRange(civlTransform.Collect()); } } } diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/CivlTypeChecker.cs index 0e257f30..dba7ab4b 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -357,7 +357,7 @@ namespace Microsoft.Boogie } } - public class MoverTypeChecker : ReadOnlyVisitor + public class CivlTypeChecker : ReadOnlyVisitor { CheckingContext checkingContext; Procedure enclosingProc; @@ -376,8 +376,7 @@ namespace Microsoft.Boogie public bool CallExists(CallCmd callCmd, int enclosingProcLayerNum, int layerNum) { - if (!procToAtomicProcedureInfo.ContainsKey(callCmd.Proc)) - return true; + Debug.Assert(procToAtomicProcedureInfo.ContainsKey(callCmd.Proc)); var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc]; if (callCmd.Proc.Modifies.Count > 0) { @@ -448,7 +447,7 @@ namespace Microsoft.Boogie return MoverType.Top; } - public MoverTypeChecker(Program program) + public CivlTypeChecker(Program program) { this.errorCount = 0; this.checkingContext = new CheckingContext(null); @@ -1105,60 +1104,60 @@ namespace Microsoft.Boogie private class PurityChecker : StandardVisitor { - private MoverTypeChecker moverTypeChecker; + private CivlTypeChecker civlTypeChecker; - public PurityChecker(MoverTypeChecker moverTypeChecker) + public PurityChecker(CivlTypeChecker civlTypeChecker) { - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; } public override Cmd VisitCallCmd(CallCmd node) { - Procedure enclosingProc = moverTypeChecker.enclosingImpl.Proc; - if (!moverTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc)) + Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc; + if (!civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc)) { - moverTypeChecker.Error(node, "Atomic procedure can only call an atomic procedure"); + civlTypeChecker.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]; + var callerInfo = civlTypeChecker.procToAtomicProcedureInfo[enclosingProc]; + var calleeInfo = civlTypeChecker.procToAtomicProcedureInfo[node.Proc]; if (calleeInfo.isPure) { // do nothing } else if (callerInfo.isPure) { - moverTypeChecker.Error(node, "Pure procedure can only call pure procedures"); + civlTypeChecker.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"); + civlTypeChecker.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"); + civlTypeChecker.Error(node, "Atomic procedures cannot make parallel calls"); return node; } public override Expr VisitIdentifierExpr(IdentifierExpr node) { - Procedure enclosingProc = moverTypeChecker.enclosingImpl.Proc; + Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc; if (node.Decl is GlobalVariable) { - if (moverTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure) + if (civlTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure) { - moverTypeChecker.Error(node, "Pure procedure cannot access global variables"); + civlTypeChecker.Error(node, "Pure procedure cannot access global variables"); } - else if (!moverTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl)) + else if (!civlTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl)) { - moverTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers"); + civlTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers"); } else { - moverTypeChecker.sharedVarsAccessed.Add(node.Decl); + 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 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" /> <PropertyGroup> @@ -73,11 +73,11 @@ <ItemGroup> <Compile Include="LinearSets.cs" /> <Compile Include="MoverCheck.cs" /> - <Compile Include="OwickiGries.cs" /> + <Compile Include="CivlRefinement.cs" /> <Compile Include="Program.cs" /> <Compile Include="Properties\AssemblyInfo.cs" /> <Compile Include="SimulationRelation.cs" /> - <Compile Include="TypeCheck.cs" /> + <Compile Include="CivlTypeChecker.cs" /> <Compile Include="YieldTypeChecker.cs" /> </ItemGroup> <ItemGroup> @@ -112,4 +112,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project>
\ No newline at end of file +</Project> 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<Declaration> decls; HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache; HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache; HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache; - private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + private MoverCheck(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls) { this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.decls = decls; this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); } - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls) { - if (moverTypeChecker.procToActionInfo.Count == 0) + if (civlTypeChecker.procToActionInfo.Count == 0) return; - List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(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<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(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<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>(); @@ -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<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - 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<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), 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<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - 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<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), 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<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - 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<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks); impl.Proc = proc; @@ -662,7 +662,7 @@ namespace Microsoft.Boogie blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken))); string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name); List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - 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<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks); impl.Proc = proc; 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<Declaration> originalDecls = new List<Declaration>(); 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<Declaration> decls = new List<Declaration>(); 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/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<int, HashSet<int>> 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<int, HashSet<int>> 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<int, HashSet<int>> 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<Block> 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<Absy, int> absyToNode; @@ -160,9 +160,9 @@ namespace Microsoft.Boogie Dictionary<Tuple<int, int>, int> edgeLabels; IEnumerable<Block> loopHeaders; - private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders) + private YieldTypeChecker(CivlTypeChecker civlTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> 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 /// </summary> - 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<string> { 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; } |