diff options
| -rw-r--r-- | Source/Concurrency/LinearSets.cs | 2 | ||||
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 331 | ||||
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 9 | ||||
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 62 | ||||
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 37 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 10 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 23 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.csproj | 6 | ||||
| -rw-r--r-- | Test/og/DeviceCache.bpl | 20 | ||||
| -rw-r--r-- | Test/og/DeviceCacheWithBuffer.bpl | 20 | ||||
| -rw-r--r-- | Test/og/lock.bpl | 6 |
11 files changed, 270 insertions, 256 deletions
diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs index 51f7f328..576d6163 100644 --- a/Source/Concurrency/LinearSets.cs +++ b/Source/Concurrency/LinearSets.cs @@ -47,7 +47,7 @@ namespace Microsoft.Boogie this.varToDomainName = new Dictionary<Variable, string>();
this.linearDomains = new Dictionary<string, LinearDomain>();
}
- public void Typecheck()
+ public void TypeCheck()
{
this.VisitProgram(program);
foreach (string domainName in domainNameToType.Keys)
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 0a918ad1..53d61ba5 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -7,31 +7,173 @@ using System.Diagnostics; namespace Microsoft.Boogie
{
- /*
- * Typechecking rules:
- * At most one atomic specification per procedure
- * The gate of an atomic specification refers only to global and input variables
- */
+ public enum MoverType
+ {
+ Top,
+ Atomic,
+ Right,
+ Left,
+ Both
+ }
+
+ public class ActionInfo
+ {
+ public Procedure proc;
+ public MoverType moverType;
+ public int phaseNum;
+ public List<AssertCmd> thisGate;
+ public CodeExpr thisAction;
+ public List<Variable> thisInParams;
+ public List<Variable> thisOutParams;
+ public List<AssertCmd> thatGate;
+ public CodeExpr thatAction;
+ public List<Variable> thatInParams;
+ public List<Variable> thatOutParams;
+
+ public bool IsRightMover
+ {
+ get { return moverType == MoverType.Right || moverType == MoverType.Both; }
+ }
+
+ public bool IsLeftMover
+ {
+ get { return moverType == MoverType.Left || moverType == MoverType.Both; }
+ }
+
+ public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType, int phaseNum)
+ {
+ this.proc = proc;
+ this.moverType = moverType;
+ this.phaseNum = phaseNum;
+ this.thisGate = new List<AssertCmd>();
+ this.thisAction = codeExpr;
+ this.thisInParams = new List<Variable>();
+ this.thisOutParams = new List<Variable>();
+ this.thatGate = new List<AssertCmd>();
+ this.thatInParams = new List<Variable>();
+ this.thatOutParams = new List<Variable>();
+
+ var cmds = thisAction.Blocks[0].Cmds;
+ for (int i = 0; i < cmds.Count; i++)
+ {
+ AssertCmd assertCmd = cmds[i] as AssertCmd;
+ if (assertCmd == null) break;
+ thisGate.Add(assertCmd);
+ cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);
+ }
+
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ foreach (Variable x in proc.InParams)
+ {
+ this.thisInParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true);
+ this.thatInParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ foreach (Variable x in proc.OutParams)
+ {
+ this.thisOutParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ this.thatOutParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ List<Variable> otherLocVars = new List<Variable>();
+ foreach (Variable x in thisAction.LocVars)
+ {
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ otherLocVars.Add(y);
+ }
+ Contract.Assume(proc.TypeParameters.Count == 0);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ foreach (AssertCmd assertCmd in thisGate)
+ {
+ thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
+ }
+ Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+ List<Block> otherBlocks = new List<Block>();
+ foreach (Block block in thisAction.Blocks)
+ {
+ List<Cmd> otherCmds = new List<Cmd>();
+ foreach (Cmd cmd in block.Cmds)
+ {
+ otherCmds.Add(Substituter.Apply(subst, cmd));
+ }
+ Block otherBlock = new Block();
+ otherBlock.Cmds = otherCmds;
+ otherBlock.Label = "that_" + block.Label;
+ block.Label = "this_" + block.Label;
+ otherBlocks.Add(otherBlock);
+ blockMap[block] = otherBlock;
+ if (block.TransferCmd is GotoCmd)
+ {
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ for (int i = 0; i < gotoCmd.labelNames.Count; i++)
+ {
+ gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
+ }
+ }
+ }
+ foreach (Block block in thisAction.Blocks)
+ {
+ if (block.TransferCmd is ReturnExprCmd)
+ {
+ blockMap[block].TransferCmd = new ReturnExprCmd(block.TransferCmd.tok, Expr.True);
+ continue;
+ }
+ List<Block> otherGotoCmdLabelTargets = new List<Block>();
+ List<string> otherGotoCmdLabelNames = new List<string>();
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ otherGotoCmdLabelTargets.Add(blockMap[target]);
+ otherGotoCmdLabelNames.Add(blockMap[target].Label);
+ }
+ blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
+ }
+ this.thatAction = new CodeExpr(otherLocVars, otherBlocks);
+ }
+ }
+
public class MoverCheck
{
+ public static MoverType GetMoverType(Ensures e, out int phaseNum)
+ {
+ phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "atomic", int.MaxValue);
+ if (phaseNum != int.MaxValue)
+ return MoverType.Atomic;
+ phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "right", int.MaxValue);
+ if (phaseNum != int.MaxValue)
+ return MoverType.Right;
+ phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "left", int.MaxValue);
+ if (phaseNum != int.MaxValue)
+ return MoverType.Left;
+ phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "both", int.MaxValue);
+ if (phaseNum != int.MaxValue)
+ return MoverType.Both;
+ return MoverType.Top;
+ }
+
HashSet<Tuple<ActionInfo, ActionInfo>> commutativityCheckerCache;
HashSet<Tuple<ActionInfo, ActionInfo>> gatePreservationCheckerCache;
HashSet<Tuple<ActionInfo, ActionInfo>> failurePreservationCheckerCache;
LinearTypeChecker linearTypeChecker;
+ MoverTypeChecker moverTypeChecker;
Program moverCheckerProgram;
- private MoverCheck(LinearTypeChecker linearTypeChecker)
+ private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)
{
this.commutativityCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
this.gatePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
this.failurePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
this.linearTypeChecker = linearTypeChecker;
+ this.moverTypeChecker = moverTypeChecker;
this.moverCheckerProgram = new Program();
- foreach (Declaration decl in linearTypeChecker.program.TopLevelDeclarations)
+ foreach (Declaration decl in moverTypeChecker.program.TopLevelDeclarations)
{
if (decl is TypeCtorDecl || decl is TypeSynonymDecl || decl is Constant || decl is Function || decl is Axiom)
this.moverCheckerProgram.TopLevelDeclarations.Add(decl);
}
- foreach (Variable v in linearTypeChecker.program.GlobalVariables())
+ foreach (Variable v in moverTypeChecker.program.GlobalVariables())
{
this.moverCheckerProgram.TopLevelDeclarations.Add(v);
}
@@ -84,163 +226,18 @@ namespace Microsoft.Boogie }
}
- enum MoverType
- {
- Top,
- Atomic,
- Right,
- Left,
- Both
- }
-
- class ActionInfo
- {
- public Procedure proc;
- public MoverType moverType;
- public List<AssertCmd> thisGate;
- public CodeExpr thisAction;
- public List<Variable> thisInParams;
- public List<Variable> thisOutParams;
- public List<AssertCmd> thatGate;
- public CodeExpr thatAction;
- public List<Variable> thatInParams;
- public List<Variable> thatOutParams;
-
- public bool IsRightMover
- {
- get { return moverType == MoverType.Right || moverType == MoverType.Both; }
- }
-
- public bool IsLeftMover
- {
- get { return moverType == MoverType.Left || moverType == MoverType.Both; }
- }
-
- public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType)
- {
- this.proc = proc;
- this.moverType = moverType;
- this.thisGate = new List<AssertCmd>();
- this.thisAction = codeExpr;
- this.thisInParams = new List<Variable>();
- this.thisOutParams = new List<Variable>();
- this.thatGate = new List<AssertCmd>();
- this.thatInParams = new List<Variable>();
- this.thatOutParams = new List<Variable>();
-
- var cmds = thisAction.Blocks[0].Cmds;
- for (int i = 0; i < cmds.Count; i++)
- {
- AssertCmd assertCmd = cmds[i] as AssertCmd;
- if (assertCmd == null) break;
- thisGate.Add(assertCmd);
- cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);
- }
-
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- foreach (Variable x in proc.InParams)
- {
- this.thisInParams.Add(x);
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true);
- this.thatInParams.Add(y);
- map[x] = new IdentifierExpr(Token.NoToken, y);
- }
- foreach (Variable x in proc.OutParams)
- {
- this.thisOutParams.Add(x);
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
- this.thatOutParams.Add(y);
- map[x] = new IdentifierExpr(Token.NoToken, y);
- }
- List<Variable> otherLocVars = new List<Variable>();
- foreach (Variable x in thisAction.LocVars)
- {
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
- map[x] = new IdentifierExpr(Token.NoToken, y);
- otherLocVars.Add(y);
- }
- Contract.Assume(proc.TypeParameters.Count == 0);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- foreach (AssertCmd assertCmd in thisGate)
- {
- thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
- }
- Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
- List<Block> otherBlocks = new List<Block>();
- foreach (Block block in thisAction.Blocks)
- {
- List<Cmd> otherCmds = new List<Cmd>();
- foreach (Cmd cmd in block.Cmds)
- {
- otherCmds.Add(Substituter.Apply(subst, cmd));
- }
- Block otherBlock = new Block();
- otherBlock.Cmds = otherCmds;
- otherBlock.Label = "that_" + block.Label;
- block.Label = "this_" + block.Label;
- otherBlocks.Add(otherBlock);
- blockMap[block] = otherBlock;
- if (block.TransferCmd is GotoCmd)
- {
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- for (int i = 0; i < gotoCmd.labelNames.Count; i++)
- {
- gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
- }
- }
- }
- foreach (Block block in thisAction.Blocks)
- {
- if (block.TransferCmd is ReturnExprCmd)
- {
- blockMap[block].TransferCmd = new ReturnExprCmd(block.TransferCmd.tok, Expr.True);
- continue;
- }
- List<Block> otherGotoCmdLabelTargets = new List<Block>();
- List<string> otherGotoCmdLabelNames = new List<string>();
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- foreach (Block target in gotoCmd.labelTargets)
- {
- otherGotoCmdLabelTargets.Add(blockMap[target]);
- otherGotoCmdLabelNames.Add(blockMap[target].Label);
- }
- blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
- }
- this.thatAction = new CodeExpr(otherLocVars, otherBlocks);
- }
- }
-
- public static void AddCheckers(LinearTypeChecker linearTypeChecker)
+ public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)
{
- Program program = linearTypeChecker.program;
- List<ActionInfo> gatedActions = new List<ActionInfo>();
- foreach (Declaration decl in program.TopLevelDeclarations)
- {
- Procedure proc = decl as Procedure;
- if (proc == null) continue;
- foreach (Ensures e in proc.Ensures)
- {
- MoverType moverType = GetMoverType(e);
- if (moverType == MoverType.Top) continue;
- CodeExpr codeExpr = e.Condition as CodeExpr;
- if (codeExpr == null)
- {
- Console.WriteLine("Warning: an atomic action must be a CodeExpr");
- continue;
- }
- ActionInfo info = new ActionInfo(proc, codeExpr, moverType);
- gatedActions.Add(info);
- }
- }
- if (gatedActions.Count == 0)
+ if (moverTypeChecker.procToActionInfo.Count == 0)
return;
- MoverCheck moverChecking = new MoverCheck(linearTypeChecker);
- foreach (ActionInfo first in gatedActions)
+ Program program = moverTypeChecker.program;
+ MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker);
+ foreach (ActionInfo first in moverTypeChecker.procToActionInfo.Values)
{
Debug.Assert(first.moverType != MoverType.Top);
if (first.moverType == MoverType.Atomic)
continue;
- foreach (ActionInfo second in gatedActions)
+ foreach (ActionInfo second in moverTypeChecker.procToActionInfo.Values)
{
if (first.IsRightMover)
{
@@ -274,20 +271,6 @@ namespace Microsoft.Boogie }
}
- private static MoverType GetMoverType(Ensures e)
- {
- if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
- return MoverType.Atomic;
- else if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
- return MoverType.Right;
- else if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
- return MoverType.Left;
- else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
- return MoverType.Both;
- else
- return MoverType.Top;
- }
-
class TransitionRelationComputation
{
private Program program;
@@ -638,4 +621,4 @@ namespace Microsoft.Boogie this.moverCheckerProgram.TopLevelDeclarations.Add(proc);
}
}
-}
+}
\ No newline at end of file diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 27528826..7125bfcd 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -14,14 +14,16 @@ namespace Microsoft.Boogie {
List<IdentifierExpr> globalMods;
LinearTypeChecker linearTypeChecker;
+ MoverTypeChecker moverTypeChecker;
Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
List<Procedure> yieldCheckerProcs;
List<Implementation> yieldCheckerImpls;
Procedure yieldProc;
- public OwickiGriesTransform(LinearTypeChecker linearTypeChecker)
+ public OwickiGriesTransform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)
{
this.linearTypeChecker = linearTypeChecker;
+ this.moverTypeChecker = moverTypeChecker;
Program program = linearTypeChecker.program;
globalMods = new List<IdentifierExpr>();
foreach (Variable g in program.GlobalVariables())
@@ -689,11 +691,6 @@ namespace Microsoft.Boogie public void Transform()
{
- MoverCheck.AddCheckers(linearTypeChecker);
-#if QED
- YieldTypeChecker.PerformYieldTypeChecking(linearTypeChecker);
- RefinementCheck.AddCheckers(linearTypeChecker);
-#endif
Program program = linearTypeChecker.program;
foreach (var decl in program.TopLevelDeclarations)
{
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index b463bcfd..8f8638d6 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -6,28 +6,62 @@ using Microsoft.Boogie; namespace Microsoft.Boogie
{
- class TypeCheck : StandardVisitor
+ public class MoverTypeChecker : StandardVisitor
{
- public static int FindPhaseNumber(Procedure proc)
+ public int FindPhaseNumber(Procedure proc)
{
- foreach (Ensures ensures in proc.Ensures)
- {
-
- }
- return int.MaxValue;
+ if (procToActionInfo.ContainsKey(proc))
+ return procToActionInfo[proc].phaseNum;
+ else
+ return int.MaxValue;
}
CheckingContext checkingContext;
- int errorCount;
+ public int errorCount;
HashSet<Variable> globalVariables;
bool insideYield;
int phaseNumEnclosingProc;
-
- public TypeCheck(Program program)
+ public Dictionary<Procedure, ActionInfo> procToActionInfo;
+ public Program program;
+
+ public void TypeCheck()
+ {
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ foreach (Ensures e in proc.Ensures)
+ {
+ int phaseNum;
+ MoverType moverType = MoverCheck.GetMoverType(e, out phaseNum);
+ if (moverType == MoverType.Top) continue;
+ CodeExpr codeExpr = e.Condition as CodeExpr;
+ if (codeExpr == null)
+ {
+ Error(e, "An atomic action must be a CodeExpr");
+ continue;
+ }
+ if (procToActionInfo.ContainsKey(proc))
+ {
+ Error(proc, "A procedure can have at most one atomic action");
+ continue;
+ }
+ procToActionInfo[proc] = new ActionInfo(proc, codeExpr, moverType, phaseNum);
+ }
+ }
+ this.VisitProgram(program);
+#if QED
+ YieldTypeChecker.PerformYieldTypeChecking(this);
+#endif
+ }
+
+ public MoverTypeChecker(Program program)
{
globalVariables = new HashSet<Variable>(program.GlobalVariables());
+ procToActionInfo = new Dictionary<Procedure, ActionInfo>();
this.errorCount = 0;
this.checkingContext = new CheckingContext(null);
+ this.program = program;
}
public override Block VisitBlock(Block node)
{
@@ -118,14 +152,10 @@ namespace Microsoft.Boogie return base.VisitAssumeCmd(node);
}
- //
-
- private void Error(Absy node, string message)
+ public void Error(Absy node, string message)
{
checkingContext.Error(node, message);
errorCount++;
}
-
-
}
-}
+}
\ No newline at end of file diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 2be2ef55..0a3ebfb0 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -26,26 +26,15 @@ namespace Microsoft.Boogie static CharSetSolver yieldTypeCheckerAutomatonSolver;
static string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";// regex of property to build automaton of YTS language
static Automaton<BvSet> yieldTypeCheckerAutomaton;
- static int errorCount;
- static CheckingContext checkingContext;
- static Automaton<BvSet> foo;
static YieldTypeChecker()
{
yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
- foo = yieldTypeCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$");
- yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); // YTS property , L(YTSP)
- yieldTypeCheckerAutomaton = Automaton<BvSet>.MkProduct(yieldTypeCheckerAutomaton, foo, yieldTypeCheckerAutomatonSolver);
-
- errorCount = 0;
- checkingContext = new CheckingContext(null);
- }
-
- private static void Error(Absy node, string message)
- {
- checkingContext.Error(node, message);
- errorCount++;
+ yieldTypeCheckerAutomaton =
+ Automaton<BvSet>.MkProduct(yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex),
+ yieldTypeCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$"),
+ yieldTypeCheckerAutomatonSolver);
}
-
+
/*
Parameter: Automaton<BvSet> implTypeCheckAutomaton : Automaton of implementation body build with respect to YTSI.
Return : if L(YTSI) is subset of L(YTSP) {TRUE} else {FALSE}
@@ -73,20 +62,20 @@ namespace Microsoft.Boogie /*
Parameter : LinearTypeChecker linearTypeChecker : YTS Checker is a component of linearTypeChecker.Adds instance of YTS checker into linearType checker
*/
- public static void PerformYieldTypeChecking(LinearTypeChecker linearTypeChecker)
+ public static void PerformYieldTypeChecking(MoverTypeChecker moverTypeChecker)
{
- Program yieldTypeCheckedProgram = linearTypeChecker.program;
+ Program yieldTypeCheckedProgram = moverTypeChecker.program;
YieldTypeChecker regExprToAuto = new YieldTypeChecker();
foreach (var decl in yieldTypeCheckedProgram.TopLevelDeclarations)
{
Implementation impl = decl as Implementation;
if (impl == null) continue;
- int phaseNumSpecImpl = TypeCheck.FindPhaseNumber(impl.Proc);
- YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(impl, phaseNumSpecImpl);
+ int phaseNumSpecImpl = moverTypeChecker.FindPhaseNumber(impl.Proc);
+ YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(moverTypeChecker, impl, phaseNumSpecImpl);
Automaton<BvSet> yieldTypeCheckImpl = yieldTypeCheckerPerImpl.YieldTypeCheckAutomata();
if (!IsYieldTypeSafe(yieldTypeCheckImpl))
{
- Error(impl, "\n Body of " + impl.Proc.Name + " is not yield type safe " + "\n");
+ moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield type safe " + "\n");
}
}
}
@@ -108,9 +97,11 @@ namespace Microsoft.Boogie List<Tuple<int, int>> phaseIntervals; // [MinValue ph0 ] [ph0 ph1] [ph1 ph2] ..... [phk phk+1] intervals
List<int> finalStates; //final
List<int> initialStates; // initial states collection. There are epsilon transitions (ASCII 'E') from concreteInitial state to these initial states
+ MoverTypeChecker moverTypeChecker;
- public YieldTypeCheckerCore(Implementation toTypeCheck, int specPhaseNum)
+ public YieldTypeCheckerCore(MoverTypeChecker moverTypeChecker, Implementation toTypeCheck, int specPhaseNum)
{
+ this.moverTypeChecker = moverTypeChecker;
ytypeChecked = toTypeCheck;
specPhaseNumImpl = specPhaseNum;
@@ -150,7 +141,7 @@ namespace Microsoft.Boogie HashSet<int> callCmdPhaseNumSet = new HashSet<int>();
foreach (CallCmd callCmd in callCmdsInImpl)
{
- int tmpPhaseNum = TypeCheck.FindPhaseNumber(callCmd.Proc);
+ int tmpPhaseNum = moverTypeChecker.FindPhaseNumber(callCmd.Proc);
callCmdPhaseNumSet.Add(tmpPhaseNum);
}
callCmdPhaseNumSet.Add(specPhaseNumImpl);
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 33c4e91a..1776f64e 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2350,14 +2350,14 @@ namespace Microsoft.Boogie { //Contract.Requires(rc != null);
this.Condition.Resolve(rc);
}
-
+
public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
bool isAtomicSpecification =
- QKeyValue.FindBoolAttribute(this.Attributes, "atomic") ||
- QKeyValue.FindBoolAttribute(this.Attributes, "right") ||
- QKeyValue.FindBoolAttribute(this.Attributes, "left") ||
- QKeyValue.FindBoolAttribute(this.Attributes, "both");
+ QKeyValue.FindIntAttribute(this.Attributes, "atomic", int.MaxValue) != int.MaxValue ||
+ QKeyValue.FindIntAttribute(this.Attributes, "right", int.MaxValue) != int.MaxValue ||
+ QKeyValue.FindIntAttribute(this.Attributes, "left", int.MaxValue) != int.MaxValue ||
+ QKeyValue.FindIntAttribute(this.Attributes, "both", int.MaxValue) != int.MaxValue;
bool oldYields = tc.Yields;
tc.Yields = isAtomicSpecification;
this.Condition.Typecheck(tc);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index a53fa06f..80e91e22 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -461,7 +461,8 @@ namespace Microsoft.Boogie }
LinearTypeChecker linearTypeChecker;
- PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker);
+ MoverTypeChecker moverTypeChecker;
+ PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out moverTypeChecker);
if (oc != PipelineOutcome.ResolvedAndTypeChecked)
return;
@@ -484,7 +485,7 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.StratifiedInlining == 0)
{
- OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypeChecker);
+ OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypeChecker, moverTypeChecker);
ogTransform.Transform();
var eraser = new LinearEraser();
eraser.VisitProgram(program);
@@ -641,12 +642,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)
+ public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out MoverTypeChecker moverTypeChecker)
{
Contract.Requires(program != null);
Contract.Requires(bplFileName != null);
linearTypeChecker = null;
+ moverTypeChecker = null;
// ---------- Resolve ------------------------------------------------------------
@@ -682,7 +684,7 @@ namespace Microsoft.Boogie }
linearTypeChecker = new LinearTypeChecker(program);
- linearTypeChecker.Typecheck();
+ linearTypeChecker.TypeCheck();
if (linearTypeChecker.errorCount == 0)
{
linearTypeChecker.Transform();
@@ -693,6 +695,16 @@ namespace Microsoft.Boogie return PipelineOutcome.TypeCheckingError;
}
+#if QED
+ moverTypeChecker = new MoverTypeChecker(program);
+ moverTypeChecker.TypeCheck();
+ if (moverTypeChecker.errorCount != 0)
+ {
+ Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, bplFileName);
+ return PipelineOutcome.TypeCheckingError;
+ }
+#endif
+
if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)
{
// if PrintDesugaring option is engaged, print the file here, after resolution and type checking
@@ -1197,7 +1209,8 @@ namespace Microsoft.Boogie Program p = ParseBoogieProgram(new List<string> { filename }, false);
System.Diagnostics.Debug.Assert(p != null);
LinearTypeChecker linearTypeChecker;
- PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker);
+ MoverTypeChecker moverTypeChecker;
+ PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out moverTypeChecker);
System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked);
return p;
}
diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj index b7f63cc5..a1be2f35 100644 --- a/Source/ExecutionEngine/ExecutionEngine.csproj +++ b/Source/ExecutionEngine/ExecutionEngine.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>
@@ -72,7 +72,7 @@ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
<OutputPath>bin\QED\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DefineConstants>TRACE;DEBUG;QED</DefineConstants>
<DebugType>full</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
<ErrorReport>prompt</ErrorReport>
@@ -146,4 +146,4 @@ <Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project>
\ No newline at end of file diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index f6510bee..7bf74e9c 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -99,7 +99,7 @@ COPY_TO_BUFFER: }
procedure {:yields} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X)
-ensures {:right} {:phase 0} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; return true; }|;
+ensures {:right 0} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; return true; }|;
{
var j: int;
tid := tid';
@@ -129,28 +129,28 @@ requires 0 <= start && 0 <= bytesRead && (bytesRead == 0 || start + bytesRead <= }
procedure {:yields} ReadCurrsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);
-ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;
+ensures {:right -1} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;
procedure {:yields} ReadNewsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);
-ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;
+ensures {:right -1} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;
procedure {:yields} WriteNewsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);
-ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;
+ensures {:atomic -1} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;
procedure {:yields} WriteCurrsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);
-ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;
+ensures {:atomic -1} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;
procedure {:yields} ReadCacheEntry(index: int);
-ensures {:atomic} |{ A: assert 0 <= index && index < currsize; return true; }|;
+ensures {:atomic -1} |{ A: assert 0 <= index && index < currsize; return true; }|;
procedure {:yields} WriteCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);
-ensures {:right} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; return true; }|;
+ensures {:right -1} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; return true; }|;
procedure {:yields} acquire({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
-ensures {:right} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lock := tid; return true; }|;
+ensures {:right -1} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lock := tid; return true; }|;
procedure {:yields} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
-ensures {:left} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;
+ensures {:left -1} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;
procedure {:yields} Skip();
-ensures {:both} |{ A: return true; }|;
\ No newline at end of file +ensures {:both -1} |{ A: return true; }|;
\ No newline at end of file diff --git a/Test/og/DeviceCacheWithBuffer.bpl b/Test/og/DeviceCacheWithBuffer.bpl index 549acacf..71e09ae2 100644 --- a/Test/og/DeviceCacheWithBuffer.bpl +++ b/Test/og/DeviceCacheWithBuffer.bpl @@ -105,7 +105,7 @@ COPY_TO_BUFFER: }
procedure {:yields} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X)
-ensures {:right} {:phase 0} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; cache := (lambda i: int :: if (currsize <= i && i < index) then device[i] else cache[i]); return true; }|;
+ensures {:right 0} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; cache := (lambda i: int :: if (currsize <= i && i < index) then device[i] else cache[i]); return true; }|;
{
var j: int;
tid := tid';
@@ -142,28 +142,28 @@ ensures (forall i: int :: 0 <= i && i < bytesRead ==> buffer[i] == device[start+ }
procedure {:yields} ReadCurrsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);
-ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;
+ensures {:right -1} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;
procedure {:yields} ReadNewsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);
-ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;
+ensures {:right -1} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;
procedure {:yields} WriteNewsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);
-ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;
+ensures {:atomic -1} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;
procedure {:yields} WriteCurrsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);
-ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;
+ensures {:atomic -1} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;
procedure {:yields} ReadCacheEntry(index: int) returns (val: int);
-ensures {:atomic} |{ A: assert 0 <= index && index < currsize; val := cache[index]; return true; }|;
+ensures {:atomic -1} |{ A: assert 0 <= index && index < currsize; val := cache[index]; return true; }|;
procedure {:yields} WriteCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);
-ensures {:right} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; cache[index] := device[index]; return true; }|;
+ensures {:right -1} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; cache[index] := device[index]; return true; }|;
procedure {:yields} acquire({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
-ensures {:right} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lock := tid; return true; }|;
+ensures {:right -1} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lock := tid; return true; }|;
procedure {:yields} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
-ensures {:left} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;
+ensures {:left -1} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;
procedure {:yields} Skip();
-ensures {:both} |{ A: return true; }|;
\ No newline at end of file +ensures {:both -1} |{ A: return true; }|;
\ No newline at end of file diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl index 4c019846..0b250b6d 100644 --- a/Test/og/lock.bpl +++ b/Test/og/lock.bpl @@ -23,7 +23,7 @@ procedure {:yields} {:stable} Customer() }
procedure {:yields} Enter()
-ensures {:atomic} {:phase 0} |{ A: assume !b; b := true; return true; }|;
+ensures {:atomic 0} |{ A: assume !b; b := true; return true; }|;
{
var status: bool;
L:
@@ -42,11 +42,11 @@ ensures {:atomic} {:phase 0} |{ A: assume !b; b := true; return true; }|; }
procedure CAS(prev: bool, next: bool) returns (status: bool);
-ensures {:atomic} |{
+ensures {:atomic -1} |{
A: goto B, C;
B: assume b == prev; b := next; status := true; return true;
C: status := false; return true;
}|;
procedure {:yields} Leave();
-ensures {:atomic} |{ A: b := false; return true; }|;
+ensures {:atomic -1} |{ A: b := false; return true; }|;
|