diff options
| author |  kuruis <unknown> | 2013-12-04 14:59:19 -0800 |
|---|---|---|
| committer | kuruis <unknown> | 2013-12-04 14:59:19 -0800 |
| commit | 617d18eaaf52bf1c58a3985f43542b75e2ff731f (patch) | |
| tree | 9a7db4509484c727f503b909e89a7c7caf138282 /Source/Concurrency/YieldTypeChecker.cs | |
| parent | 3c260ee33f3c9c680581f9684a2334fbb2a0fa9b (diff) | |
Building raw graphs of YieldTypeChecker for building Automata is added
Diffstat (limited to 'Source/Concurrency/YieldTypeChecker.cs')
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 598 |
1 files changed, 376 insertions, 222 deletions
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 407cb0d3..064230dd 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -1,4 +1,5 @@ #if QED
+
using System;
using System.Collections;
using System.Collections.Generic;
@@ -6,8 +7,11 @@ using System.Collections.Generic; using System.Linq;
using System.Text;
using Microsoft.Boogie;
-using Microsoft.Automata;
+//using Microsoft.Automata;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie.GraphUtil;
namespace Microsoft.Boogie
{
/*
@@ -16,18 +20,16 @@ namespace Microsoft.Boogie */
class YieldTypeChecker
{
- Program typeCheckedProg;
- private YieldTypeCheckerCore yTypeChecker;
- CharSetSolver yieldTypeCheckerAutomatonSolver;
- string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";
- Char[][] yieldTypeCheckerVocabulary;
- BvSet yielTypeCheckerBvSet;
- Automaton<BvSet> yieldTypeCheckerAutomaton;
-
-
- public YieldTypeChecker(Program program)
+ /* CharSetSolver yieldTypeCheckerAutomatonSolver;
+ string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";
+ Char[][] yieldTypeCheckerVocabulary;
+ BvSet yielTypeCheckerBvSet;
+ Automaton<BvSet> yieldTypeCheckerAutomaton;
+ */
+
+ private YieldTypeChecker()
{
- typeCheckedProg = program;
+ /*
yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
yieldTypeCheckerVocabulary = new char[][] {
new char[]{'1','2'},
@@ -36,126 +38,95 @@ namespace Microsoft.Boogie new char[]{'7','8'},
new char[]{'9','A'},
new char[]{'B','C'},
- new char[]{'D','F'}
+ new char[]{'D','E'}
};
yielTypeCheckerBvSet = yieldTypeCheckerAutomatonSolver.MkRangesConstraint(false, yieldTypeCheckerVocabulary);
yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); //accepts strings that match the regex r
- this.Run(typeCheckedProg);
- }
-
- // Complete after discussing with Shaz!
- // Important function, may be one more function needed ?
- //This Function will process the implementation body's <Interval, list<string>>
- //1. Map each character in the path string into a character in our Autamaton vocab.
- private Dictionary<Tuple<int, int>, string[]> ProcRawPath(Dictionary<Tuple<int, int>, string[]> rawPaths)
- {
-
- Dictionary<Tuple<int, int>, string[]> processedPaths = new Dictionary<Tuple<int, int>, string[]>();
- return processedPaths;
+ */
}
-
- public bool Run(Program program)
+ public static void AddChecker(LinearTypeChecker linearTypeChecker)
{
-
- foreach (Implementation impl in program.TopLevelDeclarations)
+ Program yielTypeCheckedProgram = linearTypeChecker.program;
+ YieldTypeChecker regExprToAuto = new YieldTypeChecker();
+ foreach (var decl in yielTypeCheckedProgram.TopLevelDeclarations)
{
- // Create YieldTypeChecker
- // Compute Utility Maps for an Implementation
- if (impl.Blocks.Count > 0)
+ Implementation impl = decl as Implementation;
+ if (impl != null)
{
- int phaseNumSpecImpl = QKeyValue.FindIntAttribute(impl.Proc.Attributes, "phase", 0);
- yTypeChecker = new YieldTypeCheckerCore(impl, phaseNumSpecImpl);
- Dictionary<Tuple<int, int>, string[]> inputToAutomata = ProcRawPath(yTypeChecker.PostProcessPaths());
- foreach (KeyValuePair<Tuple<int, int>, string[]> pair in inputToAutomata)
+
+ // Create YieldTypeChecker
+ // Compute Utility Maps for an Implementation
+ if (impl.Blocks.Count > 0)
{
- foreach (string inputPath in pair.Value)
- {
- if (!(yieldTypeCheckerAutomatonSolver.Accepts(yieldTypeCheckerAutomaton, inputPath)))
- {
- return false;
- }
- }
- }
+ int phaseNumSpecImpl = QKeyValue.FindIntAttribute(impl.Proc.Attributes, "phase", 0);
+ //
+ YieldTypeCheckerCore.TypeCheck(impl, phaseNumSpecImpl);
+
+ }
}
}
- return true;
}
}
- /* Dictionary<Implementation, Dictionary<Procedure, int>> phaseNumToCall; */
- // I think I dont need this
- // phaseNumToCall[Impl] ==> Dictionary dict={
- //foreach(CallCmd in callCmdsInImpl[Impl]
- // ->foreach KeyValPair p in dict
- // -> get p.Second gives phase num in
- class YieldTypeCheckerCore
+ class YieldTypeCheckerCore : StandardVisitor
{
CheckingContext checkingContext;
int errorCount;
- Implementation ytypeChecked; // YieldTypeChecked body
- int numCallInEncImpl;
- int specPhaseNumImpl;
- int yTypeCheckCurrentPhaseNum;
+ Implementation ytypeChecked;
+ // int numCallInEncImpl; // number of callcmds in impl
+ int specPhaseNumImpl; // impl.proc's spec num
+ //! int yTypeCheckCurrentPhaseNum;// current phase of yield type checking
+ int programCounter; // initial state of the impl
+
+
+ HashSet<CallCmd> callCmdsInImpl; // callCmdsInImpl[Implementation] ==> Set = { call1, call2, call3 ... }
+ int numCallCmdInEnclosingProc; // Number of CallCmds in
+
+ 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
+ // Dictionary<Implementation, Automaton<YieldTypeSet>> yieldTypeCheckAutomaton; // To be generated with input yieldTypeCheckGraph
+
+ List<Tuple<int, int>> phaseIntervals; // (-inf ph0 ] (ph0 ph1] (ph1 ph2] ..... (phk phk+1] intervals
- Dictionary<Implementation, HashSet<CallCmd>> callCmdsInImpl; // callCmdsInImpl[Implementation] ==> Set = { call1, call2, call3 ... }
- Dictionary<Implementation, int> numCallCmdInEnclosingProc; // Number of CallCmds in
- Dictionary<Implementation, Dictionary<Tuple<int, int>, string>> yieldTypeCheckPattern; // (-inf ph0 ] (ph0 ph1] (ph1 ph2] ..... (phk phk+1] where phk+1 == atcSpecPhsNumTypeCheckedProc
- Dictionary<Implementation, List<Tuple<int, int>>> phaseIntervals; // (-inf ph0 ] (ph0 ph1] (ph1 ph2] ..... (phk phk+1] intervals
- public YieldTypeCheckerCore(Implementation toTypeCheck, int specPhaseNum)
+ private YieldTypeCheckerCore(Implementation toTypeCheck, int specPhaseNum)
{
ytypeChecked = toTypeCheck;
this.errorCount = 0;
this.checkingContext = new CheckingContext(null);
- numCallInEncImpl = 0;
+ // numCallInEncImpl = 0;
specPhaseNumImpl = specPhaseNum;
- yTypeCheckCurrentPhaseNum = 0;
+ //! yTypeCheckCurrentPhaseNum = 0;
+ programCounter = Guid.NewGuid().GetHashCode();
- /*Utility Maps*/
- phaseIntervals = new Dictionary<Implementation, List<Tuple<int, int>>>();
- yieldTypeCheckPattern = new Dictionary<Implementation, Dictionary<Tuple<int, int>, string>>();
- callCmdsInImpl = new Dictionary<Implementation, HashSet<CallCmd>>();
- numCallCmdInEnclosingProc = new Dictionary<Implementation, int>();
+ /*Utility Maps*/
+ phaseIntervals = new List<Tuple<int, int>>();
+ callCmdsInImpl = new HashSet<CallCmd>();
+ numCallCmdInEnclosingProc = 0;
+
+ // Graph and Automaton
+ yieldTypeCheckGraph = new HashSet<Tuple<int, int>>();
+ // yieldTypeCheckAutomaton = new Dictionary<Implementation, Automaton<YieldTypeSet>>();
+ verticesToEdges = new Dictionary<Tuple<int, int>, string>();
}
- public Dictionary<Tuple<int, int>, string[]> CreateRawInputToTypeCheck()
- {
- List<Tuple<int, int>> iterOverPhaseList = phaseIntervals[ytypeChecked];
- this.CalculateCallCmds(ytypeChecked);
- this.VisitImplementation(ytypeChecked);
-
- for (int i = 0;
- yTypeCheckCurrentPhaseNum <= specPhaseNumImpl
- && i < iterOverPhaseList.Count;
-
- i++)
- {
- VisitImplementation(ytypeChecked);
- yTypeCheckCurrentPhaseNum = yTypeCheckCurrentPhaseNum + iterOverPhaseList[i].Item2 + 1;
- }
-
- return PostProcessPaths();
-
-
-
-
- }
private void CalculateCallCmds(Implementation impl)
{
- HashSet<CallCmd> callCmdInBodyEncImpl = new HashSet<CallCmd>();
+ // HashSet<CallCmd> callCmdInBodyEncImpl = new HashSet<CallCmd>();
List<CallCmd> callCmdInBodyEncImplList = new List<CallCmd>();
+
foreach (Block b in impl.Blocks)
{
List<Cmd> cmds = new List<Cmd>();
@@ -165,13 +136,13 @@ namespace Microsoft.Boogie if (cmd is CallCmd)
{
CallCmd callCmd = b.Cmds[i] as CallCmd;
- numCallInEncImpl = numCallInEncImpl + 1;
- numCallCmdInEnclosingProc.Add(impl, numCallInEncImpl);
+ numCallCmdInEnclosingProc = numCallCmdInEnclosingProc + 1;
+
- if (!(callCmdInBodyEncImpl.Contains(callCmd)))
+ if (!(callCmdsInImpl.Contains(callCmd)))
{
- callCmdInBodyEncImpl.Add(callCmd);
+ callCmdsInImpl.Add(callCmd);
callCmdInBodyEncImplList.Add(callCmd);//
}
@@ -191,7 +162,6 @@ namespace Microsoft.Boogie callCmdPhaseNumIndexList.Sort();
- List<Tuple<int, int>> phsIntrvs = new List<Tuple<int, int>>();
//Create Phase Intervals
for (int i = 0; i < callCmdPhaseNumIndexList.Count; i++)
{
@@ -199,197 +169,381 @@ namespace Microsoft.Boogie if (i == 0)
{
Tuple<int, int> initTuple = new Tuple<int, int>(int.MinValue, callCmdPhaseNumIndexList[i]);
- phsIntrvs.Add(initTuple);
+ phaseIntervals.Add(initTuple);
}
else
{
Tuple<int, int> intervalToInsert = new Tuple<int, int>(callCmdPhaseNumIndexList[i - 1] + 1, callCmdPhaseNumIndexList[i]);
- phsIntrvs.Add(intervalToInsert);
+ phaseIntervals.Add(intervalToInsert);
}
}
- //Set Implementation -> List<Tuple> map
- phaseIntervals.Add(ytypeChecked, phsIntrvs);
- //Set Implelentation -> CallCmds
- callCmdsInImpl.Add(ytypeChecked, callCmdInBodyEncImpl);
- //Set Implementation -> numberofCalls
- numCallCmdInEnclosingProc.Add(ytypeChecked, numCallInEncImpl);
-
}
- public void ComputePaths(Block b)
+
+ public static bool TypeCheck(Implementation impl, int checkPhsNum)
{
- foreach (Cmd cmd in b.Cmds)
+ YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(impl, checkPhsNum);
+ yieldTypeCheckerPerImpl.CalculateCallCmds(impl);
+ yieldTypeCheckerPerImpl.BuildAutomatonGraph();
+ yieldTypeCheckerPerImpl.GetTuplesForGraph();
+
+ return true;
+ }
+
+
+ public void BuildAutomatonGraph()
+ {
+ foreach (Block block in ytypeChecked.Blocks)
{
- if (cmd is AssignCmd)
- {
- AssignCmd assnCmd = cmd as AssignCmd;
- AddCheckAssignCmd(assnCmd);
- }
- else if (cmd is CallCmd)
- {
- CallCmd callCmd = cmd as CallCmd;
- AddCheckCallCmd(callCmd, yTypeCheckCurrentPhaseNum);
- }
- else if (cmd is AssumeCmd)
- {
- AssumeCmd assmCmd = cmd as AssumeCmd;
- AddCheckAssumeCmd(assmCmd);
- }
- else if (cmd is HavocCmd)
+
+ for (int i = 0; i < block.Cmds.Count; i++)
{
- HavocCmd havocCmd = cmd as HavocCmd;
- AddCheckHavocCmd(havocCmd);
+ AddNodeToGraph(block.Cmds[i]);
+
}
- else if (cmd is YieldCmd)
+
+ if (block.TransferCmd is GotoCmd)
{
- YieldCmd yldCmd = cmd as YieldCmd;
- AddCheckYieldCmd(yldCmd);
+ GotoCmd gt = block.TransferCmd as GotoCmd;
+ AddNodeToGraphForGotoCmd(gt);
}
- else if (cmd is AssertCmd)
+ else if (block.TransferCmd is ReturnCmd)
{
- AssertCmd assertCmd = cmd as AssertCmd;
- AddCheckAssertCmd(assertCmd);
+ ReturnCmd rt = block.TransferCmd as ReturnCmd;
+ AddNodeToGraphForReturnCmd(rt);
}
}
+
+
}
- /*
- (-inf 4] -> "PQBAL" "..."
- [3 7] -> "PQB" , "PQYA " ...
- ..
- ..
- (k specReachPoint] -> ....
- */
- public Dictionary<Tuple<int, int>, string[]> PostProcessPaths()
+ public Graph<int> GetTuplesForGraph()
{
- Dictionary<Tuple<int, int>, string[]> pathsPerPhase = new Dictionary<Tuple<int, int>, string[]>();
- Dictionary<Tuple<int, int>, string> pathPerPhase = yieldTypeCheckPattern[ytypeChecked];
- List<Tuple<int, int>> iterOverPhaseList = phaseIntervals[ytypeChecked];
+ Graph<int> graphFromTuples = new Graph<int>(yieldTypeCheckGraph);
+ // Just for debugging purposes
+ Console.Write("ToDot version is being printed " + graphFromTuples.ToDot());
+ return graphFromTuples;
- for (int i = 0; i < iterOverPhaseList.Count; i++)
+ }
+
+ public void AddNodeToGraph(Cmd cmd)
+ {
+ 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)
{
- string[] pathsPerPhs = pathPerPhase[iterOverPhaseList[i]].Split('S');
- pathsPerPhase.Add(iterOverPhaseList[i], pathsPerPhs);
+ AssertCmd assertCmd = cmd as AssertCmd;
+ AddNodeToGraphForAssertCmd(assertCmd);
}
- //Discuss with Shaz in detail !
- return pathsPerPhase;
+ else if (cmd is YieldCmd)
+ {
+ YieldCmd yieldCmd = cmd as YieldCmd;
+ AddNodeToGraphForYieldCmd(yieldCmd);
+
+ }
+ else if (cmd is CallCmd)
+ {
+
+ CallCmd callCmd = cmd as CallCmd;
+ AddNodeToGraphForCallCmd(callCmd, 5/*yTypeCheckCurrentPhaseNum*/);
+
+ }
+ }
+
+ public void AddNodeToGraphForGotoCmd(GotoCmd cmd)
+ {
+ if (ytypeChecked == null) { Console.WriteLine("Fuck Yeah !"); }
+
+ int source = programCounter;
+ int dest = Guid.NewGuid().GetHashCode();
+ // Create a Epsilon transition between them
+ Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
+ yieldTypeCheckGraph.Add(srcdst);
+ verticesToEdges[srcdst] = "N";
+ }
+
+ public void AddNodeToGraphForReturnCmd(ReturnCmd cmd)
+ {
+
+ // Do nothing !
+
}
- public void AddCheckCallCmd(CallCmd cmd, int currentCheckPhsNum)
+ public void AddNodeToGraphForYieldCmd(YieldCmd cmd)
{
- List<Tuple<int, int>> iterOverPhaseList = phaseIntervals[ytypeChecked];
- for (int i = 0; i < iterOverPhaseList.Count; i++)
+
+ int source = programCounter;
+ int dest = Guid.NewGuid().GetHashCode();
+ Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
+ yieldTypeCheckGraph.Add(srcdst);
+ verticesToEdges[srcdst] = "Y";
+
+ }
+
+ public void AddNodeToGraphForAssignCmd(AssignCmd cmd)
+ {
+
+ int source = programCounter;
+ int dest = Guid.NewGuid().GetHashCode();
+ Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
+ yieldTypeCheckGraph.Add(srcdst);
+ verticesToEdges[srcdst] = "Q";
+ }
+
+ public void AddNodeToGraphForHavocCmd(HavocCmd cmd)
+ {
+
+ int source = programCounter;
+ int dest = Guid.NewGuid().GetHashCode();
+ Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
+ yieldTypeCheckGraph.Add(srcdst);
+ verticesToEdges[srcdst] = "Q";
+
+ }
+
+ public void AddNodeToGraphForAssumeCmd(AssumeCmd cmd)
+ {
+
+ int source = Guid.NewGuid().GetHashCode();
+ int dest = Guid.NewGuid().GetHashCode();
+ Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
+ yieldTypeCheckGraph.Add(srcdst);
+ verticesToEdges[srcdst] = "P";
+
+ }
+
+ public void AddNodeToGraphForAssertCmd(AssertCmd cmd)
+ {
+ int source = programCounter;
+ int dest = Guid.NewGuid().GetHashCode();
+ // Create a Epsilon transition between them
+ Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
+ yieldTypeCheckGraph.Add(srcdst);
+ verticesToEdges[srcdst] = "N";
+
+ }
+
+
+ public void AddNodeToGraphForCallCmd(CallCmd cmd, int currentCheckPhsNum)
+ {
+
+ int callePhaseNum = QKeyValue.FindIntAttribute(cmd.Proc.Attributes, "phase", 0);
+
+ if (callePhaseNum > currentCheckPhsNum)
{
+ int source = Guid.NewGuid().GetHashCode();
+ programCounter = source;
- if (currentCheckPhsNum <= iterOverPhaseList[i].Item2)
- {
- yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "S";
- }
- else
+ }
+ else
+ {
+ foreach (Ensures e in cmd.Proc.Ensures)
{
- foreach (Ensures e in ytypeChecked.Proc.Ensures)
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
{
- if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
- {
- yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "A";
+ int source = programCounter;
+ int dest = Guid.NewGuid().GetHashCode();
+ Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
+ yieldTypeCheckGraph.Add(srcdst);
+ verticesToEdges[srcdst] = "A";
- }
- else if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
- {
- yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "R";
- }
- else if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
- {
- yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "L";
- }
- else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
- {
- yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "B";
- }
+ }
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
+ {
+ int source = programCounter;
+ int dest = Guid.NewGuid().GetHashCode();
+ Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
+ yieldTypeCheckGraph.Add(srcdst);
+ verticesToEdges[srcdst] = "R";
+ }
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
+ {
+ int source = programCounter;
+ int dest = Guid.NewGuid().GetHashCode();
+ Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
+ yieldTypeCheckGraph.Add(srcdst);
+ verticesToEdges[srcdst] = "L";
+ }
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
+ {
+ int source = programCounter;
+ int dest = Guid.NewGuid().GetHashCode();
+ Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
+ yieldTypeCheckGraph.Add(srcdst);
+ verticesToEdges[srcdst] = "B";
}
}
+
}
+
}
- public void AddCheckYieldCmd(YieldCmd cmd)
+
+ public Graph<int> CreateGrapFromHashSet(HashSet<Tuple<int, int>> grph)
+ {
+
+ Graph<int> graphForAutomaton = new Graph<int>(grph);
+
+ // Do Some transformation on graph here //
+
+ return graphForAutomaton;
+
+ }
+ public void PrintGraph(Graph<int> graph)
+ {
+
+ graph.ToDot();
+
+ }
+
+ private void Error(Absy node, string message)
{
- List<Tuple<int, int>> iterOverPhaseList = phaseIntervals[ytypeChecked];
- for (int i = 0; i < iterOverPhaseList.Count; i++)
+ checkingContext.Error(node, message);
+ errorCount++;
+ }
+
+
+ /*
+
+ internal class YieldTypeSet
+ {
+ uint elems;
+
+ static internal YieldTypeSet Empty = new YieldTypeSet(0);
+ static internal YieldTypeSet Full = new YieldTypeSet(uint.MaxValue);
+
+ internal 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()
{
- yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] =
- yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "Y";
+ return new YieldTypeSet(~elems);
+ }
+
+ public override string ToString()
+ {
+ return string.Format("YieldTypeSet(0x{0})", elems.ToString("X"));
}
}
- //Assuming that "AssumeCmd can not include Global variable" check done in previous typechecks
- public void AddCheckAssumeCmd(AssumeCmd cmd)
+
+
+ internal class YieldTypeSetSolver : IBoolAlgMinterm<YieldTypeSet>
{
- List<Tuple<int, int>> iterOverPhaseList = phaseIntervals[ytypeChecked];
- for (int i = 0; i < iterOverPhaseList.Count; i++)
+ MintermGenerator<YieldTypeSet> mtg; //use the default built-in minterm generator
+ internal YieldTypeSetSolver()
{
- yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] =
- yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "Y";
+ //create the minterm generator for this solver
+ mtg = new MintermGenerator<YieldTypeSet>(this);
}
- }
- // Go through with Shaz
- //public void AddCheckNaryExpr() { }
+ public bool AreEquivalent(YieldTypeSet predicate1, YieldTypeSet predicate2)
+ {
+ return predicate1.Equals(predicate2);
+ }
+
+ public YieldTypeSet False
+ {
+ get { return YieldTypeSet.Empty; }
+ }
- // Go through with Shaz
- public void AddCheckAssignCmd(AssignCmd cmd) { }
+ public YieldTypeSet MkAnd(IEnumerable<YieldTypeSet> predicates)
+ {
+ YieldTypeSet res = YieldTypeSet.Full;
+ foreach (var s in predicates)
+ res = res.Intersect(s);
+ return res;
+ }
- //Go through with Shaz
- public void AddCheckHavocCmd(HavocCmd cmd) { }
+ public YieldTypeSet MkNot(YieldTypeSet predicate)
+ {
+ return predicate.Complement();
+ }
- // Go through with Shaz
- public void AddCheckAssertCmd(AssertCmd cmd) { }
+ 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 void VisitImplementation(Implementation node)
- {
- if (node != ytypeChecked)
+ public bool IsSatisfiable(YieldTypeSet predicate)
{
+ return !predicate.Equals(YieldTypeSet.Empty);
+ }
- Error(node, "The visited implementation must be" + ytypeChecked.Name);
+ public YieldTypeSet MkAnd(YieldTypeSet predicate1, YieldTypeSet predicate2)
+ {
+ return predicate1.Intersect(predicate2);
}
- specPhaseNumImpl = QKeyValue.FindIntAttribute(node.Proc.Attributes, "phase", 0);
+ public YieldTypeSet MkOr(YieldTypeSet predicate1, YieldTypeSet predicate2)
+ {
+ return predicate1.Union(predicate2);
+ }
- //
- Stack<Block> dfsStack = new Stack<Block>();
- HashSet<Block> dfsStackAsSet = new HashSet<Block>();
- dfsStack.Push(node.Blocks[0]);
- dfsStackAsSet.Add(node.Blocks[0]);
- while (dfsStack.Count > 0)
+ public IEnumerable<Pair<bool[], YieldTypeSet>> GenerateMinterms(params YieldTypeSet[] constraints)
{
- Block b = dfsStack.Pop();
- dfsStackAsSet.Remove(b);
- ComputePaths(b);
+ return mtg.GenerateMinterms(constraints);
+ }
+ public YieldTypeSet Simplify(YieldTypeSet s)
+ {
+ return s;
- if (b.TransferCmd is ReturnCmd)
- {
- continue;
- }
- GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
- foreach (Block target in gotoCmd.labelTargets)
- {
- dfsStack.Push(target);
- dfsStackAsSet.Add(target);
- }
}
- }
+ }*/
- private void Error(Absy node, string message)
- {
- checkingContext.Error(node, message);
- errorCount++;
- }
}
}
+
#endif
\ No newline at end of file |