summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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.csproj8
-rw-r--r--Source/Concurrency/MoverCheck.cs26
-rw-r--r--Source/Concurrency/Program.cs12
-rw-r--r--Source/Concurrency/YieldTypeChecker.cs36
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs22
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;
}