diff options
| author |  kuruis <unknown> | 2013-12-11 12:15:05 -0800 |
|---|---|---|
| committer | kuruis <unknown> | 2013-12-11 12:15:05 -0800 |
| commit | 614648876bd81d6683a9d94207bb514a615202fb (patch) | |
| tree | a6e2c6be603aaff04e1410d486f8c8a5884acc10 /Source/Concurrency/YieldTypeChecker.cs | |
| parent | 9ee988513091d620555874b8a8c82c152b342844 (diff) | |
Updates on YieldTypeCheck
Diffstat (limited to 'Source/Concurrency/YieldTypeChecker.cs')
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 953 |
1 files changed, 330 insertions, 623 deletions
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 0a3ebfb0..b036af82 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -29,103 +29,17 @@ namespace Microsoft.Boogie static YieldTypeChecker()
{
yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
- yieldTypeCheckerAutomaton =
- Automaton<BvSet>.MkProduct(yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex),
- yieldTypeCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$"),
+ 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}
- */
- public static bool IsYieldTypeSafe(Automaton<BvSet> implTypeCheckAutomaton)
+ /*Parameter : Implementation impl : Implementation whose phase intervals, statistical data(number of call stmts) are computed*/
+ private static List<Tuple<int, int>> ComputePhaseIntervals(Implementation impl, int specPhaseNumImpl, MoverTypeChecker moverTypeChecker)
{
+ HashSet<CallCmd> callCmdsInImpl = new HashSet<CallCmd>(); // callCmdsInImpl[Implementation] ==> Set = { call1, call2, call3 ... }
+ List<Tuple<int, int>> phaseIntervals = new List<Tuple<int, int>>(); // [MinValue ph0 ] [ph0 ph1] [ph1 ph2] ..... [phk phk+1] intervals
- List<BvSet> witnessSet;
- var isNonEmpty = Automaton<BvSet>.CheckDifference(
- implTypeCheckAutomaton,
- yieldTypeCheckerAutomaton,
- 0,
- yieldTypeCheckerAutomatonSolver,
- out witnessSet);
- // Ask Margus, Shaz to be sure !
- if (isNonEmpty)
- {
- // var witness = new String(Array.ConvertAll(witnessSet.ToArray(), bvset => (char)yieldTypeCheckerAutomatonSolver.Choose(bvset)));
- //Console.Write("\n Program is not Yield Type Safe \n");
- //Console.Write("Debugging ... \n Difference of impl and yiled type check automaton : \n" + witness);
- return false;
- }
- return true;
- }
- /*
- Parameter : LinearTypeChecker linearTypeChecker : YTS Checker is a component of linearTypeChecker.Adds instance of YTS checker into linearType checker
- */
- public static void PerformYieldTypeChecking(MoverTypeChecker moverTypeChecker)
- {
- 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 = moverTypeChecker.FindPhaseNumber(impl.Proc);
- YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(moverTypeChecker, impl, phaseNumSpecImpl);
- Automaton<BvSet> yieldTypeCheckImpl = yieldTypeCheckerPerImpl.YieldTypeCheckAutomata();
- if (!IsYieldTypeSafe(yieldTypeCheckImpl))
- {
- moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield type safe " + "\n");
- }
- }
- }
- }
-
- /*
- * Executor class for creating L(YTSI).
- */
- class YieldTypeCheckerCore
- {
- Implementation ytypeChecked; // Implementation whose body is being YTS checked
- int specPhaseNumImpl; // impl.proc's spec num
- int yTypeCheckCurrentPhaseNum;// current phase of yield type checking
- int programCounter; // initial state of the impl
- int concreteInitialState; // First seen initial state in an implementation
- HashSet<CallCmd> callCmdsInImpl; // callCmdsInImpl[Implementation] ==> Set = { call1, call2, call3 ... }
- Dictionary<Tuple<int, int>, string> verticesToEdges; // Tuple<int,int> --> "Y" : State(k) --Y--> State(k+1)
- HashSet<Tuple<int, int>> yieldTypeCheckGraph; // (-inf ph0 ] (ph0 ph1] (ph1 ph2] ..... (phk phk+1] where phk+1 == atcSpecPhsNumTypeCheckedProc
- 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(MoverTypeChecker moverTypeChecker, Implementation toTypeCheck, int specPhaseNum)
- {
- this.moverTypeChecker = moverTypeChecker;
- ytypeChecked = toTypeCheck;
-
- specPhaseNumImpl = specPhaseNum;
- yTypeCheckCurrentPhaseNum = 0;
- programCounter = Math.Abs(Guid.NewGuid().GetHashCode());
- initialStates = new List<int>();
- finalStates = new List<int>();
-
- initialStates.Add(programCounter);//
- concreteInitialState = programCounter;
-
- /*Utility Maps*/
- phaseIntervals = new List<Tuple<int, int>>();
- callCmdsInImpl = new HashSet<CallCmd>();
-
- // Graph and Automaton
- yieldTypeCheckGraph = new HashSet<Tuple<int, int>>();
- verticesToEdges = new Dictionary<Tuple<int, int>, string>();
- }
-
- /*Parameter : Implementation impl : Implementation whose phase intervals, statistical data(number of call stmts) are computed
- */
- private void ComputePhaseIntervals(Implementation impl)
- {
// Compute CallCmds inside impl
foreach (Block b in impl.Blocks)
{
@@ -142,7 +56,7 @@ namespace Microsoft.Boogie foreach (CallCmd callCmd in callCmdsInImpl)
{
int tmpPhaseNum = moverTypeChecker.FindPhaseNumber(callCmd.Proc);
- callCmdPhaseNumSet.Add(tmpPhaseNum);
+ callCmdPhaseNumSet.Add(tmpPhaseNum);
}
callCmdPhaseNumSet.Add(specPhaseNumImpl);
@@ -176,262 +90,337 @@ namespace Microsoft.Boogie Console.Write("\n Phase " + i.ToString() + "[" + phaseIntervals[i].Item1.ToString() + "," + phaseIntervals[i].Item2.ToString() + "]" + "\n");
}
#endif
+ return phaseIntervals;
}
- /*Parameter:YieldTypeCheckerCore yieldTypeCheckerPerImpl: takes an executor object to do all computation to build L(YTSI)
+
+ /*
+ 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}
*/
- public Automaton<BvSet> YieldTypeCheckAutomata()
+ public static bool IsYieldTypeSafe(Automaton<BvSet> implTypeCheckAutomaton)
{
- ComputePhaseIntervals(ytypeChecked); // Compute intervals
- for (int i = 0; i < this.phaseIntervals.Count; i++) // take current phase check num from each interval
+
+ List<BvSet> witnessSet;
+ var isNonEmpty = Automaton<BvSet>.CheckDifference(
+ implTypeCheckAutomaton,
+ yieldTypeCheckerAutomaton,
+ 0,
+ yieldTypeCheckerAutomatonSolver,
+ out witnessSet);
+ // Ask Margus, Shaz to be sure !
+ if (isNonEmpty)
{
- yTypeCheckCurrentPhaseNum = this.phaseIntervals[i].Item2; // set current phase num
-#if (DEBUG && !DEBUG_DETAIL)
- Console.Write(" \n TypeChecking for phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");
-#endif
- BuildAutomatonGraph(); // build component of graph for a phase interval
+ // var witness = new String(Array.ConvertAll(witnessSet.ToArray(), bvset => (char)yieldTypeCheckerAutomatonSolver.Choose(bvset)));
+ //Console.Write("\n Program is not Yield Type Safe \n");
+ //Console.Write("Debugging ... \n Difference of impl and yiled type check automaton : \n" + witness);
+ return false;
+ }
+ return true;
+ }
+ /*
+ Parameter : LinearTypeChecker linearTypeChecker : YTS Checker is a component of linearTypeChecker.Adds instance of YTS checker into linearType checker
+ */
+ public static void PerformYieldTypeChecking(MoverTypeChecker moverTypeChecker)
+ {
+ 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 = moverTypeChecker.FindPhaseNumber(impl.Proc);
+
+ YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(moverTypeChecker);
+ List<Tuple<int, int>> phaseIntervals = ComputePhaseIntervals(impl, phaseNumSpecImpl, moverTypeChecker); // Compute intervals
+
+ for (int i = 0; i < phaseIntervals.Count; i++) // take current phase check num from each interval
+ {
+ int yTypeCheckCurrentPhaseNum = phaseIntervals[i].Item2;
+ Automaton<BvSet> yieldTypeCheckAutoPerPhase = yieldTypeCheckerPerImpl.YieldTypeCheckAutomata(impl, phaseNumSpecImpl, yTypeCheckCurrentPhaseNum);
+ if (!IsYieldTypeSafe(yieldTypeCheckAutoPerPhase))
+ {
+ moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield type safe " + "\n");
+ }
+ }
+ }
+ }
+ }
+
+ /*
+ * Executor class for creating L(YTSI).
+ */
+ class YieldTypeCheckerCore
+ {
+
+ int stateCounter;
+ MoverTypeChecker moverTypeChecker;
+ public YieldTypeCheckerCore(MoverTypeChecker moverTypeChecker)
+ {
+ this.moverTypeChecker = moverTypeChecker;
+ }
+
+ /*Parameter:YieldTypeCheckerCore yieldTypeCheckerPerImpl: takes an executor object to do all computation to build L(YTSI)
+ */
+ public Automaton<BvSet> YieldTypeCheckAutomata(Implementation ytypeChecked, int specPhaseNumImpl, int yTypeCheckCurrentPhaseNum)
+ {
+ Dictionary<Tuple<int, int>, string> edgeLabels = new Dictionary<Tuple<int, int>, string>(); // Tuple<int,int> --> "Y" : State(k) --Y--> State(k+1)
+ Dictionary<Absy, int> abysToNode = CreateStateNumbers(ytypeChecked, yTypeCheckCurrentPhaseNum);
+ List<int> finalStates = new List<int>();
+ List<int> initialStates = new List<int>();
+ stateCounter = 0;
+
+ Graph<int> bodyGraphForImplPhaseJ = BuildAutomatonGraph(ytypeChecked, yTypeCheckCurrentPhaseNum, abysToNode, edgeLabels, initialStates, finalStates); // build component of graph for a phase interval
#if (DEBUG && !DEBUG_DETAIL)
Console.Write("\n Raw Graph is : \n");
Console.Write(yieldTypeCheckerPerImpl.PrintGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph()));
#endif
- // Bug found and solved: regenerate program counter , dont get the last state of the graph component from last phase interval
- programCounter = Math.Abs(Guid.NewGuid().GetHashCode());
- }
-
// Update edges w.r.t yield reaching. VocabX{True,False}
- PostProcessGraph(GetTuplesForGraph());
+ PostProcessGraph(bodyGraphForImplPhaseJ, edgeLabels);
#if (DEBUG && !DEBUG_DETAIL)
Console.Write("\n Refined Graph is : \n");
Console.Write(yieldTypeCheckerPerImpl.PrintGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph()));
#endif
//Build Automaton from graph created
- return BuildAutomaton(GetTuplesForGraph());
+ return BuildAutomaton(bodyGraphForImplPhaseJ, edgeLabels, initialStates, finalStates);
}
- /*
- * Implementation visitor call this main-visit-entrance function
- */
- private void BuildAutomatonGraph()
+ public Dictionary<Absy, int> CreateStateNumbers(Implementation ytypeChecked, int yTypeCheckCurrentPhaseNum)
{
-
- foreach (Block block in ytypeChecked.Blocks)
+ Dictionary<Absy, int> abysToNodeNo = new Dictionary<Absy, int>();
+ foreach (Block block in ytypeChecked.Blocks)
{
- // Handles visiting basic commands
- for (int i = 0; i < block.Cmds.Count; i++)
+ foreach (Cmd cmd in block.Cmds)
{
- AddNodeToGraph(block.Cmds[i]);
- }
- //Handles visiting transfer commands
- if (block.TransferCmd is GotoCmd)
- {
- GotoCmd gt = block.TransferCmd as GotoCmd;
- AddNodeToGraphForGotoCmd(gt);
- }
- else if (block.TransferCmd is ReturnCmd)
- {
- ReturnCmd rt = block.TransferCmd as ReturnCmd;
- AddNodeToGraphForReturnCmd(rt);
+ abysToNodeNo[cmd] = stateCounter;
+ stateCounter++;
+
}
+ abysToNodeNo[block.TransferCmd] = stateCounter;
+ stateCounter++;
}
-
-
- }
- /*
- * Creates Graph<int> from HashSet<Tuple<int,int>>
- */
- private Graph<int> GetTuplesForGraph()
- {
- Graph<int> graphFromTuples = new Graph<int>(yieldTypeCheckGraph);
- return graphFromTuples;
+ return abysToNodeNo;
}
+
/*
- * Visitor functions of basic commands
+ * Implementation visitor call this main-visit-entrance function
*/
- private void AddNodeToGraph(Cmd cmd)
+ private Graph<int> BuildAutomatonGraph(Implementation ytypeChecked, int yTypeCheckCurrentPhaseNum, Dictionary<Absy, int> bodyGraphForImplPhaseJ,
+ Dictionary<Tuple<int, int>, string> edgeLabels, List<int> initialStates, List<int> finalStates)
{
- if (cmd is AssignCmd)
- {
- AssignCmd assignCmd = cmd as AssignCmd;
- AddNodeToGraphForAssignCmd(assignCmd);
- }
- else if (cmd is HavocCmd)
- {
- HavocCmd havocCmd = cmd as HavocCmd;
- AddNodeToGraphForHavocCmd(havocCmd);
- }
- else if (cmd is AssumeCmd)
- {
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- AddNodeToGraphForAssumeCmd(assumeCmd);
- }
- else if (cmd is AssertCmd)
- {
- AssertCmd assertCmd = cmd as AssertCmd;
- AddNodeToGraphForAssertCmd(assertCmd);
- }
- else if (cmd is YieldCmd)
- {
- YieldCmd yieldCmd = cmd as YieldCmd;
- AddNodeToGraphForYieldCmd(yieldCmd);
+ HashSet<Tuple<int, int>> edges = new HashSet<Tuple<int, int>>();
- }
- else if (cmd is CallCmd)
+ foreach (Block block in ytypeChecked.Blocks)
{
- CallCmd callCmd = cmd as CallCmd;
- AddNodeToGraphForCallCmd(callCmd, yTypeCheckCurrentPhaseNum);
- }
- }
+ if (block.Cmds.Count >= 2)
+ {
+ for (int i = 0; i < block.Cmds.Count - 1; i++)
+ {
+ if (!IsCallCmdExitPoint(block.Cmds[i], yTypeCheckCurrentPhaseNum) && !IsCallCmdExitPoint(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum))// I think this is handled in else
+ { // proper state transition
+
+ int source = bodyGraphForImplPhaseJ[block.Cmds[i]];
+ int dest = bodyGraphForImplPhaseJ[block.Cmds[i + 1]];
+ Tuple<int, int> edge = new Tuple<int, int>(source, dest);
+ edges.Add(edge);
+ edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));
+
+ }
+ else if (!IsCallCmdExitPoint(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsCallCmdExitPoint(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum))
+ { // create artificial final state
+
+ int source = bodyGraphForImplPhaseJ[block.Cmds[i]];
+ int dest = Math.Abs(Guid.NewGuid().GetHashCode());
+ finalStates.Add(dest);
+ Tuple<int, int> edge = new Tuple<int, int>(source, dest);
+ edges.Add(edge);
+ edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));
+
+ }
+ else if (IsCallCmdExitPoint(block.Cmds[i], yTypeCheckCurrentPhaseNum) && !IsCallCmdExitPoint(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum))
+ { // current cmd exit , next cmd will be put as initial state
+ initialStates.Add(bodyGraphForImplPhaseJ[block.Cmds[i + 1]]);
+
+ }
+ else if (IsCallCmdExitPoint(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsCallCmdExitPoint(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum))
+ {
+ continue;
+ }
+ else
+ {// Do proper transition
+
+ int source = bodyGraphForImplPhaseJ[block.Cmds[i]];
+ int dest = bodyGraphForImplPhaseJ[block.Cmds[i + 1]];
+ Tuple<int, int> edge = new Tuple<int, int>(source, dest);
+ edges.Add(edge);
+ edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));
+
+ }
+ }
- private void AddNodeToGraphForGotoCmd(GotoCmd cmd)
- {
- int source = programCounter;
- int dest = programCounter;//Math.Abs(Guid.NewGuid().GetHashCode());
- programCounter = dest;
-
- // Create a Epsilon transition between them
- Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
- yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "E";
- }
- private void AddNodeToGraphForReturnCmd(ReturnCmd cmd)
- {
- // Do nothing !
- finalStates.Add(programCounter);
- }
-
- private void AddNodeToGraphForYieldCmd(YieldCmd cmd)
- {
- int source = programCounter;
- int dest = Math.Abs(Guid.NewGuid().GetHashCode());
- programCounter = dest;
+ if (IsCallCmdExitPoint(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum))
+ { // put b.TransferCmd into initial states
+ initialStates.Add(bodyGraphForImplPhaseJ[block.TransferCmd]);
+ }
+ else
+ { // proper transition to state before transfer command
- Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
- yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "Y";
+ int source = bodyGraphForImplPhaseJ[block.Cmds[block.Cmds.Count - 1]];
+ int dest = bodyGraphForImplPhaseJ[block.TransferCmd];
+ Tuple<int, int> edge = new Tuple<int, int>(source, dest);
+ edges.Add(edge);
+ edgeLabels.Add(edge, GetEdgeType(block.Cmds[block.Cmds.Count - 1]));
- }
+ }
- private void AddNodeToGraphForAssignCmd(AssignCmd cmd)
- {
- int source = programCounter;
- int dest = Math.Abs(Guid.NewGuid().GetHashCode());
- programCounter = dest;
+ }
+ else if (block.Cmds.Count == 1)
+ {
+ if (IsCallCmdExitPoint(block.Cmds[0], yTypeCheckCurrentPhaseNum))
+ { // put b.TransferCmd into initial states
+ initialStates.Add(bodyGraphForImplPhaseJ[block.Cmds[0]]);
+ }
+ else
+ { // proper transition to state before transfer command
+ int source = bodyGraphForImplPhaseJ[block.Cmds[0]];
+ int dest = bodyGraphForImplPhaseJ[block.TransferCmd];
+ Tuple<int, int> edge = new Tuple<int, int>(source, dest);
+ edges.Add(edge);
+ edgeLabels.Add(edge, GetEdgeType(block.Cmds[0]));
+ }
+ }
+ else if (block.Cmds.Count == 0)
+ {
- Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
- yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "Q";
+ }
+ // Handle
+ HashSet<int> targetBlockEntryStates = GetStateOfTargetBlock(block.TransferCmd, bodyGraphForImplPhaseJ, yTypeCheckCurrentPhaseNum, initialStates, finalStates);
+ foreach (int entryState in targetBlockEntryStates)
+ {
+ int source = bodyGraphForImplPhaseJ[block.TransferCmd];
+ Tuple<int, int> transferEdge = new Tuple<int, int>(source, entryState);
+ edges.Add(transferEdge);
+ edgeLabels.Add(transferEdge, "E");
+ }
+ }
+
+ Graph<int> automatonGraphOfImplPerPhase = new Graph<int>(edges);
+ return automatonGraphOfImplPerPhase;
}
- private void AddNodeToGraphForHavocCmd(HavocCmd cmd)
+ private HashSet<int> GetStateOfTargetBlock(TransferCmd tc, Dictionary<Absy, int> bodyGraphForImplPhaseJ, int yTypeCheckCurrentPhaseNum, List<int> initialStates, List<int> finalStates)
{
- int source = programCounter;
- int dest = Math.Abs(Guid.NewGuid().GetHashCode());
- programCounter = dest;
-
- Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
- yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "Q";
+ HashSet<int> targetBlockEntryStates = new HashSet<int>();
+ if (tc is ReturnCmd)
+ {
+ // Do Nothing
+ }
+ else if (tc is GotoCmd)
+ {
+ GotoCmd transferCmd = tc as GotoCmd;
+ foreach (Block block in transferCmd.labelTargets)
+ {
+ if (block.Cmds.Count == 0)
+ {
+ targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[block.TransferCmd]);
+ }
+ else if (block.Cmds.Count >= 1)
+ {
+ if (IsCallCmdExitPoint(block.Cmds[0], yTypeCheckCurrentPhaseNum))
+ {// Create artificial final state and put this into final states
+ int targetState = Math.Abs(Guid.NewGuid().GetHashCode());
+ finalStates.Add(targetState);
+ targetBlockEntryStates.Add(targetState);
+ }
+ else
+ {
+ targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[block.Cmds[0]]);
+ }
+ }
+ }
+ }
+ return targetBlockEntryStates;
}
- private void AddNodeToGraphForAssumeCmd(AssumeCmd cmd)
+ private bool IsCallCmdExitPoint(Cmd cmd, int yTypeCheckCurrentPhaseNum)
{
- int source = programCounter;
- int dest = Math.Abs(Guid.NewGuid().GetHashCode());
- programCounter = dest;
- Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
- yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "P";
- }
+ if (cmd is CallCmd)
+ {
+ CallCmd callCmd = cmd as CallCmd;
+ int phaseSpecCallCmd = moverTypeChecker.FindPhaseNumber(callCmd.Proc);
+ if (phaseSpecCallCmd > yTypeCheckCurrentPhaseNum)
+ {
+ return true;
+
+ }
+ }
+ return false;
- private void AddNodeToGraphForAssertCmd(AssertCmd cmd)
- {
- int source = programCounter;
- int dest = Math.Abs(Guid.NewGuid().GetHashCode());
- // Create a Epsilon transition between them
- programCounter = dest;
-
- Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
- yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "E";
}
+
/*
- * Parameter : int currentCheckPhsNum: currentCheckPhsNum is phase num that we do YTS check for.
- * If (currentCheckPhsNum <= callePhaseNum) {get atomic specification of CallCmd} else{ exit point in the graph is created}
- *
+ * Visitor functions of basic commands
*/
- private void AddNodeToGraphForCallCmd(CallCmd cmd, int currentCheckPhsNum)
+ private string GetEdgeType(Cmd cmd)
{
- int callePhaseNum = 0;
- foreach (Ensures e in cmd.Proc.Ensures)
+ if (cmd is YieldCmd)
{
- callePhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", 0);
+ return "Y";
}
-
- //Exit point created
- if (callePhaseNum > currentCheckPhsNum)
+ else if (cmd is HavocCmd)
{
- finalStates.Add(programCounter);
- int source = Math.Abs(Guid.NewGuid().GetHashCode());
- programCounter = source;
- initialStates.Add(programCounter);
+ return "Q";
}
- else
+ else if (cmd is AssumeCmd)
{
- // Get atomic specification of CallCmd's procedure and put as a node in graph
- foreach (Ensures e in cmd.Proc.Ensures)
+ return "P";
+ }
+ else if (cmd is AssertCmd)
+ {
+ return "E";
+ }
+
+ else if (cmd is CallCmd)
+ {
+ CallCmd callCmd = cmd as CallCmd;
+ foreach (Ensures e in callCmd.Proc.Ensures)
{
if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
{
- int source = programCounter;
- int dest = Math.Abs(Guid.NewGuid().GetHashCode());
- programCounter = dest;
- Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
- yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "A";
-
+ return "A";
}
else if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
{
- int source = programCounter;
- int dest = Math.Abs(Guid.NewGuid().GetHashCode());
- programCounter = dest;
- Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
- yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "R";
+ return "R";
}
else if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
{
- int source = programCounter;
- int dest = Math.Abs(Guid.NewGuid().GetHashCode());
- programCounter = dest;
- Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
- yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "L";
+ return "L";
}
else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
{
- int source = programCounter;
- int dest = Math.Abs(Guid.NewGuid().GetHashCode());
- programCounter = dest;
- Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
- yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "B";
+ return "B";
}
}
}
+ //rest can only be assigncmd
+ AssignCmd assgnCmd = cmd as AssignCmd;
+ return "Q";
+
}
- public string PrintGraph(Graph<int> graph)
+
+ public string PrintGraph(Graph<int> graph, Implementation yTypeChecked, Dictionary<Tuple<int, int>, string> edgeLabels)
{
var s = new StringBuilder();
- s.AppendLine("\nImplementation " + ytypeChecked.Proc.Name + " digraph G {");
+ s.AppendLine("\nImplementation " + yTypeChecked.Proc.Name + " digraph G {");
foreach (var e in graph.Edges)
- s.AppendLine(" \"" + e.Item1.ToString() + "\" -- " + verticesToEdges[e] + " --> " + " \"" + e.Item2.ToString() + "\";");
+ s.AppendLine(" \"" + e.Item1.ToString() + "\" -- " + edgeLabels[e] + " --> " + " \"" + e.Item2.ToString() + "\";");
s.AppendLine("}");
return s.ToString();
}
@@ -457,7 +446,7 @@ namespace Microsoft.Boogie stack.Push(n); // push n onto stack
#if (DEBUG && !DEBUG_DETAIL)
Console.Write("\n First pushed item on stack is " + n.ToString());
-#endif
+#endif
}
while (stack.Count > 0) // not empty
{
@@ -486,12 +475,12 @@ namespace Microsoft.Boogie /*
* Calls CollectBackEdges for each Y edge existing in graph
*/
- private HashSet<Tuple<int, int>> BackwardEdgesOfYields(Graph<int> graph)
+ private HashSet<Tuple<int, int>> BackwardEdgesOfYields(Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels)
{
HashSet<Tuple<int, int>> yieldTrueEdges = new HashSet<Tuple<int, int>>();
foreach (var e in graph.Edges)
{
- if (verticesToEdges[e] == "Y")
+ if (edgeLabels[e] == "Y")
{
HashSet<Tuple<int, int>> yieldReachingEdges = CollectBackEdges(graph, e);
foreach (Tuple<int, int> yldrch in yieldReachingEdges)
@@ -509,81 +498,80 @@ namespace Microsoft.Boogie /*
* Updates vertices map according to according to yieldReaching edges. If an edge in graph is not yield reaching that its vertices map updated.
*/
- private void PostProcessGraph(Graph<int> graph)
+ private void PostProcessGraph(Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels)
{
- HashSet<Tuple<int, int>> yieldTrueEdges = BackwardEdgesOfYields(graph);
+ HashSet<Tuple<int, int>> yieldTrueEdges = BackwardEdgesOfYields(graph, edgeLabels);
foreach (Tuple<int, int> yldrch in yieldTrueEdges)
{
- if (verticesToEdges[yldrch] == "Q")
+ if (edgeLabels[yldrch] == "Q")
{
- verticesToEdges[yldrch] = "3";
+ edgeLabels[yldrch] = "3";
}
- else if (verticesToEdges[yldrch] == "P")
+ else if (edgeLabels[yldrch] == "P")
{
- verticesToEdges[yldrch] = "1";
+ edgeLabels[yldrch] = "1";
}
- else if (verticesToEdges[yldrch] == "B")
+ else if (edgeLabels[yldrch] == "B")
{
- verticesToEdges[yldrch] = "7";
+ edgeLabels[yldrch] = "7";
}
- else if (verticesToEdges[yldrch] == "R")
+ else if (edgeLabels[yldrch] == "R")
{
- verticesToEdges[yldrch] = "5";
+ edgeLabels[yldrch] = "5";
}
- else if (verticesToEdges[yldrch] == "L")
+ else if (edgeLabels[yldrch] == "L")
{
- verticesToEdges[yldrch] = "9";
+ edgeLabels[yldrch] = "9";
}
- else if (verticesToEdges[yldrch] == "A")
+ else if (edgeLabels[yldrch] == "A")
{
- verticesToEdges[yldrch] = "A";
+ edgeLabels[yldrch] = "A";
}
- else if (verticesToEdges[yldrch] == "Y")
+ else if (edgeLabels[yldrch] == "Y")
{
- verticesToEdges[yldrch] = "D";
+ edgeLabels[yldrch] = "D";
}
}
- foreach (Tuple<int, int> nyldrch in yieldTypeCheckGraph)
+ foreach (Tuple<int, int> nyldrch in graph.Edges)
{
if (!yieldTrueEdges.Contains(nyldrch))
{
- if (verticesToEdges[nyldrch] == "Q")
+ if (edgeLabels[nyldrch] == "Q")
{
- verticesToEdges[nyldrch] = "4";
+ edgeLabels[nyldrch] = "4";
}
- else if (verticesToEdges[nyldrch] == "P")
+ else if (edgeLabels[nyldrch] == "P")
{
- verticesToEdges[nyldrch] = "2";
+ edgeLabels[nyldrch] = "2";
}
- else if (verticesToEdges[nyldrch] == "B")
+ else if (edgeLabels[nyldrch] == "B")
{
- verticesToEdges[nyldrch] = "8";
+ edgeLabels[nyldrch] = "8";
}
- else if (verticesToEdges[nyldrch] == "R")
+ else if (edgeLabels[nyldrch] == "R")
{
- verticesToEdges[nyldrch] = "6";
+ edgeLabels[nyldrch] = "6";
}
- else if (verticesToEdges[nyldrch] == "L")
+ else if (edgeLabels[nyldrch] == "L")
{
- verticesToEdges[nyldrch] = "C";
+ edgeLabels[nyldrch] = "C";
}
- else if (verticesToEdges[nyldrch] == "A")
+ else if (edgeLabels[nyldrch] == "A")
{
- verticesToEdges[nyldrch] = "B";
+ edgeLabels[nyldrch] = "B";
}
- else if (verticesToEdges[nyldrch] == "Y")
+ else if (edgeLabels[nyldrch] == "Y")
{
- // Bug found : Yielding(Y) == NonYielding(Y)
- verticesToEdges[nyldrch] = "D";
+ edgeLabels[nyldrch] = "D";
}
}
}
}
- private int[] ComputeFinalStates()
+ private int[] ComputeFinalStates(List<int> finalStates)
{
int[] finalS = new int[finalStates.Count];
for (int i = 0; i < finalStates.Count; i++)
@@ -600,9 +588,9 @@ namespace Microsoft.Boogie return finalS;
}
- private List<int> ComputeInitalStates()
- {
-
+ private List<int> ComputeInitalStates(List<int> initialStates)
+ {
+
#if (DEBUG && !DEBUG_DETAIL)
for (int i = 0; i<initialStates.Count;i++ )
{
@@ -613,13 +601,13 @@ namespace Microsoft.Boogie return initialStates;
}
- private Automaton<BvSet> BuildAutomaton(Graph<int> graph)
+ private Automaton<BvSet> BuildAutomaton(Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels, List<int> initialStates, List<int> finalStates)
{
//List<Move<YieldTypeSet>> transitions = new List<Move<YieldTypeSet>>();
List<int[]> transitions = new List<int[]>();
foreach (Tuple<int, int> e in graph.Edges)
{
- if (verticesToEdges[e] == "3")
+ if (edgeLabels[e] == "3")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -628,16 +616,9 @@ namespace Microsoft.Boogie transition[3] = e.Item2;
transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(51);
- transition.Add(e.Item2);
- transitions.Add(transition);*/
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.Q)));
}
- else if (verticesToEdges[e] == "1")
+ else if (edgeLabels[e] == "1")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -645,17 +626,9 @@ namespace Microsoft.Boogie transition[2] = 49;
transition[3] = e.Item2;
transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(49);
- transition.Add(e.Item2);
- transitions.Add(transition);
- */
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.P)));
}
- else if (verticesToEdges[e] == "7")
+ else if (edgeLabels[e] == "7")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -663,15 +636,9 @@ namespace Microsoft.Boogie transition[2] = 55;
transition[3] = e.Item2;
transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(55);
- transition.Add(e.Item2);
- transitions.Add(transition);*/
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.B)));
+
}
- else if (verticesToEdges[e] == "5")
+ else if (edgeLabels[e] == "5")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -680,15 +647,8 @@ namespace Microsoft.Boogie transition[3] = e.Item2;
transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(53);
- transition.Add(e.Item2);
- transitions.Add(transition);*/
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.R)));
}
- else if (verticesToEdges[e] == "9")
+ else if (edgeLabels[e] == "9")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -697,15 +657,8 @@ namespace Microsoft.Boogie transition[3] = e.Item2;
transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(57);
- transition.Add(e.Item2);
- transitions.Add(transition);*/
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.L)));
}
- else if (verticesToEdges[e] == "A")
+ else if (edgeLabels[e] == "A")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -713,15 +666,8 @@ namespace Microsoft.Boogie transition[2] = 65;
transition[3] = e.Item2;
transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(65);
- transition.Add(e.Item2);
- transitions.Add(transition);*/
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.A)));
}
- else if (verticesToEdges[e] == "D")
+ else if (edgeLabels[e] == "D")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -729,16 +675,8 @@ namespace Microsoft.Boogie transition[2] = 68;
transition[3] = e.Item2;
transitions.Add(transition);
-
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(68);
- transition.Add(e.Item2);
- transitions.Add(transition);*/
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.Y)));
}
- else if (verticesToEdges[e] == "4")
+ else if (edgeLabels[e] == "4")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -746,16 +684,8 @@ namespace Microsoft.Boogie transition[2] = 52;
transition[3] = e.Item2;
transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(52);
- transition.Add(e.Item2);
- transitions.Add(transition);*/
-
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.QF)));
}
- else if (verticesToEdges[e] == "2")
+ else if (edgeLabels[e] == "2")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -763,15 +693,8 @@ namespace Microsoft.Boogie transition[2] = 50;
transition[3] = e.Item2;
transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(50);
- transition.Add(e.Item2);
- transitions.Add(transition);*/
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.PF)));
}
- else if (verticesToEdges[e] == "8")
+ else if (edgeLabels[e] == "8")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -779,15 +702,8 @@ namespace Microsoft.Boogie transition[2] = 56;
transition[3] = e.Item2;
transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(56);
- transition.Add(e.Item2);
- transitions.Add(transition);*/
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.BF)));
}
- else if (verticesToEdges[e] == "6")
+ else if (edgeLabels[e] == "6")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -795,33 +711,17 @@ namespace Microsoft.Boogie transition[2] = 54;
transition[3] = e.Item2;
transitions.Add(transition);
-
- /*List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(54);
- transition.Add(e.Item2);
- transitions.Add(transition);*/
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.RF)));
}
- else if (verticesToEdges[e] == "C")
+ else if (edgeLabels[e] == "C")
{
int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 67; // ASCII C
transition[2] = 67;
transition[3] = e.Item2;
-
- transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(67);
- transition.Add(e.Item2);
transitions.Add(transition);
- */
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.LF)));
}
- else if (verticesToEdges[e] == "B")
+ else if (edgeLabels[e] == "B")
{
int[] transition = new int[4];
transition[0] = e.Item1;
@@ -829,33 +729,15 @@ namespace Microsoft.Boogie transition[2] = 66;
transition[3] = e.Item2;
transitions.Add(transition);
- /*List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(66);
- transition.Add(e.Item2);
- transitions.Add(transition);
- */
- //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.AF)));
-
}
- else if (verticesToEdges[e] == "E")
+ else if (edgeLabels[e] == "E")
{
-
int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = -1;
transition[2] = -1;
transition[3] = e.Item2;
transitions.Add(transition);
-
- /*List<int> transition = new List<int>();
- transition.Add(e.Item1);
- transition.Add(69);
- transition.Add(e.Item2);
- transitions.Add(transition);
- */
- //transitions.Add(Move<YieldTypeSet>.Epsilon(e.Item1,e.Item2));
-
}
}
@@ -871,36 +753,24 @@ namespace Microsoft.Boogie var solver = new CharSetSolver();
// get initial states
- List<int> initialStates = ComputeInitalStates();
+ List<int> initialSts = ComputeInitalStates(initialStates);
// get final states
- int[] finalStates = ComputeFinalStates();
+ int[] finalSts = ComputeFinalStates(finalStates);
- // put Epslion from first initial state seen to other initial states created
+ // Take one initial state from initial states
+ int source = initialStates[0];
foreach (int s in initialStates)
{
- // Put every one epsilon to itself no problem
- /*if (!s.Equals(concreteInitialState)) { }*/
-
- if (!s.Equals(concreteInitialState))
- {
+ if (!s.Equals(source))
+ {
int[] transition = new int[4];
- transition[0] = concreteInitialState;
- transition[1] = 69;
- transition[2] = 69;
+ transition[0] = source;
+ transition[1] = -1;
+ transition[2] = -1;
transition[3] = s;
transitions.Add(transition);
- /*
- List<int> transition = new List<int>();
- transition.Add(concreteInitialState);
- transition.Add(69);
- transition.Add(69);
-
- transition.Add(s);
- transitions.Add(transition);
- */
}
- //transitions.Add(Move<YieldTypeSet>.Epsilon(concreteInitialState,s));
}
#if (DEBUG && !DEBUG_DETAIL)
@@ -912,12 +782,11 @@ namespace Microsoft.Boogie }
#endif
-
// create Automaton
- Automaton<BvSet> yieldTypeCheckAutomaton = solver.ReadFromRanges(concreteInitialState, finalStates, transitions);
+ Automaton<BvSet> yieldTypeCheckAutomaton = solver.ReadFromRanges(source, finalSts, transitions);
#if (DEBUG && DEBUG_DETAIL)
- Console.Write("\n" + ytypeChecked.Proc.Name + " Automaton \n");
+ // Console.Write("\n" + ytypeChecked.Proc.Name + " Automaton \n");
Console.Write("\n" + "Number of moves " + yieldTypeCheckAutomaton.MoveCount.ToString() + "\n");
Console.Write("\n" + "Number of states " + yieldTypeCheckAutomaton.StateCount.ToString() + "\n");
foreach (var move in yieldTypeCheckAutomaton.GetMoves())
@@ -934,168 +803,6 @@ namespace Microsoft.Boogie }
}
- static class Transitions
- {
- public static uint P = 0x1;
- public static uint Q = 0x4;
- public static uint Y = 0x1000;
- public static uint R = 0x10;
- public static uint B = 0x40;
- public static uint A = 0x200;
- public static uint L = 0x100;
- public static uint PF = 0x2;
- public static uint QF = 0x8;
- public static uint BF = 0x80;
- public static uint RF = 0x20;
- public static uint LF = 0x800;
- public static uint AF = 0x400;
- }
-
- // Ask Margus,Shaz:
- // 1. We dont have BvSet constructor to pass uint as parameter
- // 1.1 Assume that I want to add a transition to my list of moves List<Move<BvSet>> transitions ;
- // transitions.Add( Move<BvSet>.M( source, final, !! Here I can not pass an uint as condition and there is no casting possible to BvSet))
- // but I would like to pass a specific bit set in an uint. How can I provide this?
- // 2. Assme that I have a regex like
- //string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";
- //2.1 I would like to create an automaton from this regex.
- // Do I need to perform range constraint in BitWidth.BV7 to have only the strings that can be generated by those letters ? Like the following :
-
- // yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
- // yieldTypeCheckerVocabulary = new char[][] {
- // new char[]{'1','2'},
- // new char[]{'3','4'},
- // new char[]{'5','6'},
- // new char[]{'7','8'},
- // new char[]{'9','A'},
- // new char[]{'B','C'},
- // new char[]{'D','E'}
- // };
- // yielTypeCheckerBvSet = yieldTypeCheckerAutomatonSolver.MkRangesConstraint(false, yieldTypeCheckerVocabulary);
- // yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); //accepts strings that match the regex r
-
- //2.2 If we have such automaton created in 2.1 and we would like to check whether another automaton is subset of this. The automaton that we do check for is built as the following
- // state1 -- transitionCond --> state2 : In order to proper subset type checking what transitionCond should be ? BvSet, uint, int, ASCII[CHAR]-> int ? ex : a -> 65
-
-
- public class YieldTypeSet
- {
- uint elems;
-
- static internal YieldTypeSet Empty = new YieldTypeSet(0);
- static internal YieldTypeSet Full = new YieldTypeSet(uint.MaxValue);
-
- public YieldTypeSet(uint elems)
- {
- this.elems = elems;
- }
-
- public override bool Equals(object obj)
- {
- YieldTypeSet s = obj as YieldTypeSet;
- if (s == null)
- return false;
- return elems == s.elems;
- }
-
- public override int GetHashCode()
- {
- return (int)elems;
- }
-
- public YieldTypeSet Union(YieldTypeSet s)
- {
- return new YieldTypeSet(elems | s.elems);
- }
-
- public YieldTypeSet Intersect(YieldTypeSet s)
- {
- return new YieldTypeSet(elems & s.elems);
- }
-
- public YieldTypeSet Complement()
- {
- return new YieldTypeSet(~elems);
- }
-
- public override string ToString()
- {
- return string.Format("YieldTypeSet(0x{0})", elems.ToString("X"));
- }
- }
-
-
- public class YieldTypeSetSolver : IBoolAlgMinterm<YieldTypeSet>
- {
-
- MintermGenerator<YieldTypeSet> mtg; //use the default built-in minterm generator
- YieldTypeSetSolver()
- {
- //create the minterm generator for this solver
- mtg = new MintermGenerator<YieldTypeSet>(this);
- }
-
- public bool AreEquivalent(YieldTypeSet predicate1, YieldTypeSet predicate2)
- {
- return predicate1.Equals(predicate2);
- }
-
- public YieldTypeSet False
- {
- get { return YieldTypeSet.Empty; }
- }
-
- public YieldTypeSet MkAnd(IEnumerable<YieldTypeSet> predicates)
- {
- YieldTypeSet res = YieldTypeSet.Full;
- foreach (var s in predicates)
- res = res.Intersect(s);
- return res;
- }
-
- public YieldTypeSet MkNot(YieldTypeSet predicate)
- {
- return predicate.Complement();
- }
-
- public YieldTypeSet MkOr(IEnumerable<YieldTypeSet> predicates)
- {
- YieldTypeSet res = YieldTypeSet.Empty;
- foreach (var s in predicates)
- res = res.Union(s);
- return res;
- }
-
- public YieldTypeSet True
- {
- get { return YieldTypeSet.Full; }
- }
-
- public bool IsSatisfiable(YieldTypeSet predicate)
- {
- return !predicate.Equals(YieldTypeSet.Empty);
- }
-
- public YieldTypeSet MkAnd(YieldTypeSet predicate1, YieldTypeSet predicate2)
- {
- return predicate1.Intersect(predicate2);
- }
-
- public YieldTypeSet MkOr(YieldTypeSet predicate1, YieldTypeSet predicate2)
- {
- return predicate1.Union(predicate2);
- }
-
- public IEnumerable<Pair<bool[], YieldTypeSet>> GenerateMinterms(params YieldTypeSet[] constraints)
- {
- return mtg.GenerateMinterms(constraints);
- }
- public YieldTypeSet Simplify(YieldTypeSet s)
- {
- return s;
-
- }
- }
}
|