diff options
| author |  kuruis <unknown> | 2013-12-08 22:45:54 -0800 |
|---|---|---|
| committer | kuruis <unknown> | 2013-12-08 22:45:54 -0800 |
| commit | 38c16e74324b992e8f35779373e9d4702669e5e3 (patch) | |
| tree | dac5f4db86dc22b074a185e60d202c061c702b50 /Source/Concurrency/YieldTypeChecker.cs | |
| parent | 5f5dca6e2ca543fab3d70ccb9da6b306aacec236 (diff) | |
debug hastags are inserted to yieldtypechecker
Diffstat (limited to 'Source/Concurrency/YieldTypeChecker.cs')
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 560 |
1 files changed, 310 insertions, 250 deletions
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 25bf7b9e..366d9a8b 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -1,14 +1,15 @@ #if QED
+#define DEBUG
+#define DEBUG_DETAIL
+
using System;
using System.Collections;
using System.Collections.Generic;
-
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using Microsoft.Automata;
-
using System.Diagnostics.Contracts;
using Microsoft.Boogie.AbstractInterpretation;
using Microsoft.Boogie.GraphUtil;
@@ -21,17 +22,16 @@ namespace Microsoft.Boogie */
class YieldTypeChecker
{
+ /*static subfields of yieldtypesafe(YTS) property language*/
+ 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 Char[][] yieldTypeCheckerVocabulary;
+ static BvSet yielTypeCheckerBvSet;
+ static Automaton<BvSet> yieldTypeCheckerAutomaton;
- static CharSetSolver yieldTypeCheckerAutomatonSolver;
- static string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";
- static Char[][] yieldTypeCheckerVocabulary;
- static BvSet yielTypeCheckerBvSet;
- static Automaton<BvSet> yieldTypeCheckerAutomaton;
-
-
private YieldTypeChecker()
{
-
+
yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
yieldTypeCheckerVocabulary = new char[][] {
new char[]{'1','2'},
@@ -43,54 +43,61 @@ namespace Microsoft.Boogie new char[]{'D','E'}
};
yielTypeCheckerBvSet = yieldTypeCheckerAutomatonSolver.MkRangesConstraint(false, yieldTypeCheckerVocabulary);
- yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); //accepts strings that match the regex r
-
-
+ yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); // YTS property , L(YTSP)
+
+
}
- public static bool IsYieldTypeSafe(Automaton<BvSet> implTypeCheckAutomaton){
-
- List<BvSet> witnessSet;
- var isNonEmpty = Automaton<BvSet>.CheckDifference(
- implTypeCheckAutomaton,
- yieldTypeCheckerAutomaton,
- 0,
- yieldTypeCheckerAutomatonSolver,
- out witnessSet);
+ /*
+ 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)
+ {
+
+ 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)));
+ // 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;
}
-
- //Console.Write("\n Program is Yield Type Safe \n");
return true;
}
-
+ /*
+ Parameter : LinearTypeChecker linearTypeChecker : YTS Checker is a component of linearTypeChecker.Adds instance of YTS checker into linearType checker
+ */
public static void AddChecker(LinearTypeChecker linearTypeChecker)
{
Program yielTypeCheckedProgram = linearTypeChecker.program;
YieldTypeChecker regExprToAuto = new YieldTypeChecker();
foreach (var decl in yielTypeCheckedProgram.TopLevelDeclarations)
{
- Implementation impl = decl as Implementation;
+ Implementation impl = decl as Implementation;
if (impl != null)
{
- if (impl.Blocks.Count > 0)
+ if (impl.Blocks.Count > 0)// Do yield type checking for every implementation who has body.
{
int phaseNumSpecImpl = 0;
foreach (Ensures e in impl.Proc.Ensures)
{
- phaseNumSpecImpl = QKeyValue.FindIntAttribute(e.Attributes, "phase", int.MaxValue);
+ phaseNumSpecImpl = QKeyValue.FindIntAttribute(e.Attributes, "phase", 0); // Get phase number of implementation's procedure
}
Automaton<BvSet> yieldTypeCheckImpl = YieldTypeCheckerCore.TypeCheck(impl, phaseNumSpecImpl);
- if (!IsYieldTypeSafe(yieldTypeCheckImpl)) {
+ if (!IsYieldTypeSafe(yieldTypeCheckImpl))
+ {
Console.Write("\n Body of " + impl.Proc.Name + " is not yield type safe " + "\n");
return;
-
+
}
}
@@ -99,31 +106,26 @@ namespace Microsoft.Boogie }
}
-
+ /*
+ * Executor class for creating L(YTSI).
+ */
class YieldTypeCheckerCore
{
-
CheckingContext checkingContext;
int errorCount;
-
-
- Implementation ytypeChecked;
- // int numCallInEncImpl; // number of callcmds in impl
+ 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 ... }
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
+ List<int> finalStates; //final
+ List<int> initialStates; // initial states collection. There are epsilon transitions (ASCII 'E') from concreteInitial state to these initial states
-
private YieldTypeCheckerCore(Implementation toTypeCheck, int specPhaseNum)
{
ytypeChecked = toTypeCheck;
@@ -133,6 +135,10 @@ namespace Microsoft.Boogie 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*/
@@ -142,15 +148,16 @@ namespace Microsoft.Boogie // Graph and Automaton
yieldTypeCheckGraph = new HashSet<Tuple<int, int>>();
- verticesToEdges = new Dictionary<Tuple<int, int>, string>();
+ verticesToEdges = new Dictionary<Tuple<int, int>, string>();
}
-
- // return phase intervals
- private void CalculateCallCmds(Implementation impl)
+ /*Parameter : Implementation impl : Implementation whose phase intervals, statistical data(number of call stmts) are computed
+ */
+ private void ComputePhaseIntervals(Implementation impl)
{
List<CallCmd> callCmdInBodyEncImplList = new List<CallCmd>();
-
+
+ // Compute CallCmds inside impl
foreach (Block b in impl.Blocks)
{
List<Cmd> cmds = new List<Cmd>();
@@ -161,61 +168,103 @@ namespace Microsoft.Boogie {
CallCmd callCmd = b.Cmds[i] as CallCmd;
numCallCmdInEnclosingProc = numCallCmdInEnclosingProc + 1;
-
-
-
+
if (!(callCmdsInImpl.Contains(callCmd)))
{
callCmdsInImpl.Add(callCmd);
callCmdInBodyEncImplList.Add(callCmd);//
}
-
}
}
-
}
- //Sort all PhaseNum of callCmds inside Implementation
+
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n CallCmds inside program \n");
+ for (int i = 0; i < callCmdInBodyEncImplList.Count; i++) {
+ Console.Write("\nCallCmd " + callCmdInBodyEncImplList[i].Proc.Name+" ");
+
+ }
+#endif
+ //Collect phase numbers of CallCmds inside impl
List<int> callCmdPhaseNumIndexList = new List<int>();
for (int i = 0; i < callCmdInBodyEncImplList.Count; i++)
{
- int tmpPhaseNum = QKeyValue.FindIntAttribute(callCmdInBodyEncImplList[i].Proc.Attributes, "phase", 0);
- callCmdPhaseNumIndexList.Add(tmpPhaseNum);
+ foreach (Ensures e in callCmdInBodyEncImplList[i].Proc.Ensures)
+ {
+ //callePhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", int.MaxValue);
+ int tmpPhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", 0);
+ callCmdPhaseNumIndexList.Add(tmpPhaseNum);
+ }
}
+ // Get phase number of procedure of implementation : No Need !
+ // foreach (Ensures e in ytypeChecked.Proc.Ensures)
+ // {
+ // int tmpPhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", 0);
+ callCmdPhaseNumIndexList.Add(specPhaseNumImpl);
+ //}
+ //Sort all PhaseNum of callCmds inside Implementation
callCmdPhaseNumIndexList.Sort();
-
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n CallCmds's phase numbers \n");
+ for (int i = 0; i < callCmdInBodyEncImplList.Count; i++)
+ {
+ Console.Write("\nCallCmd Phase Num " + callCmdPhaseNumIndexList[i].ToString() + " ");
+ }
+#endif
//Create Phase Intervals
for (int i = 0; i < callCmdPhaseNumIndexList.Count; i++)
{
- //set the initial
+ //create the initial phase (-inf leastPhaseNum]
if (i == 0)
{
Tuple<int, int> initTuple = new Tuple<int, int>(int.MinValue, callCmdPhaseNumIndexList[i]);
phaseIntervals.Add(initTuple);
}
- else
+ else // create other phase intervals
{
Tuple<int, int> intervalToInsert = new Tuple<int, int>(callCmdPhaseNumIndexList[i - 1] + 1, callCmdPhaseNumIndexList[i]);
phaseIntervals.Add(intervalToInsert);
}
}
-
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n Number of phases is " + phaseIntervals.Count.ToString());
+ for (int i = 0;i<phaseIntervals.Count ; i++) {
+ Console.Write("\n Phase " + i.ToString() + "[" + phaseIntervals[i].Item1.ToString() + "," + phaseIntervals[i].Item2.ToString() + "]" + "\n");
+ }
+#endif
}
-
+ /*Parameter:YieldTypeCheckerCore yieldTypeCheckerPerImpl: takes an executor object to do all computation to build L(YTSI)
+ */
public Automaton<BvSet> YieldTypeCheckAutomata(YieldTypeCheckerCore yieldTypeCheckerPerImpl)
- {
-
- for (int i = 0; i<this.phaseIntervals.Count ; i++) {
- yTypeCheckCurrentPhaseNum = this.phaseIntervals[i].Item2 - 1;
+ {
+ ComputePhaseIntervals(yieldTypeCheckerPerImpl.ytypeChecked); // Compute intervals
+ for (int i = 0; i < this.phaseIntervals.Count; i++) // take current phase check num from each interval
+ {
+ yTypeCheckCurrentPhaseNum = this.phaseIntervals[i].Item2 - 1; // set current phase num
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write(" \n TypeChecking for phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");
+#endif
+ yieldTypeCheckerPerImpl.BuildAutomatonGraph(); // 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());
}
- yieldTypeCheckerPerImpl.BuildAutomatonGraph();
- //Console.Write(yieldTypeCheckerPerImpl.PrintGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph()));
+ // Update edges w.r.t yield reaching. VocabX{True,False}
yieldTypeCheckerPerImpl.PostProcessGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph());
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n Refined Graph is : \n");
+ Console.Write(yieldTypeCheckerPerImpl.PrintGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph()));
+#endif
+ //Build Automaton from graph created
return yieldTypeCheckerPerImpl.BuildAutomaton(yieldTypeCheckerPerImpl.GetTuplesForGraph());
-
+
}
public static Automaton<BvSet> TypeCheck(Implementation impl, int specPhsNum)
@@ -223,20 +272,21 @@ namespace Microsoft.Boogie YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(impl, specPhsNum);
return yieldTypeCheckerPerImpl.YieldTypeCheckAutomata(yieldTypeCheckerPerImpl);
}
-
-
-
-
+ /*
+ * Implementation visitor call this main-visit-entrance function
+ */
private void BuildAutomatonGraph()
{
- foreach (Block block in ytypeChecked.Blocks)
+
+ foreach (Block block in ytypeChecked.Blocks)
{
-
+ // Handles visiting basic commands
for (int i = 0; i < block.Cmds.Count; i++)
{
AddNodeToGraph(block.Cmds[i]);
}
+ //Handles visiting transfer commands
if (block.TransferCmd is GotoCmd)
{
GotoCmd gt = block.TransferCmd as GotoCmd;
@@ -251,14 +301,17 @@ namespace Microsoft.Boogie }
-
+ /*
+ * Creates Graph<int> from HashSet<Tuple<int,int>>
+ */
private Graph<int> GetTuplesForGraph()
{
Graph<int> graphFromTuples = new Graph<int>(yieldTypeCheckGraph);
return graphFromTuples;
-
}
-
+ /*
+ * Visitor functions of basic commands
+ */
private void AddNodeToGraph(Cmd cmd)
{
if (cmd is AssignCmd)
@@ -289,10 +342,8 @@ namespace Microsoft.Boogie }
else if (cmd is CallCmd)
{
-
CallCmd callCmd = cmd as CallCmd;
AddNodeToGraphForCallCmd(callCmd, yTypeCheckCurrentPhaseNum);
-
}
}
@@ -305,19 +356,17 @@ namespace Microsoft.Boogie // Create a Epsilon transition between them
Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "N";
+ 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;
@@ -330,7 +379,6 @@ namespace Microsoft.Boogie private void AddNodeToGraphForAssignCmd(AssignCmd cmd)
{
-
int source = programCounter;
int dest = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = dest;
@@ -342,7 +390,6 @@ namespace Microsoft.Boogie private void AddNodeToGraphForHavocCmd(HavocCmd cmd)
{
-
int source = programCounter;
int dest = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = dest;
@@ -350,12 +397,10 @@ namespace Microsoft.Boogie Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
yieldTypeCheckGraph.Add(srcdst);
verticesToEdges[srcdst] = "Q";
-
}
private void AddNodeToGraphForAssumeCmd(AssumeCmd cmd)
{
-
int source = programCounter;
int dest = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = dest;
@@ -363,7 +408,6 @@ namespace Microsoft.Boogie Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
yieldTypeCheckGraph.Add(srcdst);
verticesToEdges[srcdst] = "P";
-
}
private void AddNodeToGraphForAssertCmd(AssertCmd cmd)
@@ -376,28 +420,32 @@ namespace Microsoft.Boogie 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}
+ *
+ */
private void AddNodeToGraphForCallCmd(CallCmd cmd, int currentCheckPhsNum)
{
int callePhaseNum = 0;
-
foreach (Ensures e in cmd.Proc.Ensures)
{
- callePhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", int.MaxValue);
+ callePhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", 0);
}
+ //Exit point created
if (callePhaseNum > currentCheckPhsNum)
{
+ finalStates.Add(programCounter);
int source = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = source;
+ initialStates.Add(programCounter);
}
else
{
-
-
+ // Get atomic specification of CallCmd's procedure and put as a node in graph
foreach (Ensures e in cmd.Proc.Ensures)
{
if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
@@ -430,7 +478,6 @@ namespace Microsoft.Boogie }
else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
{
-
int source = programCounter;
int dest = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = dest;
@@ -438,24 +485,10 @@ namespace Microsoft.Boogie yieldTypeCheckGraph.Add(srcdst);
verticesToEdges[srcdst] = "B";
}
-
}
-
}
-
}
-
- private Graph<int> CreateGrapFromHashSet(HashSet<Tuple<int, int>> grph)
- {
-
- Graph<int> graphForAutomaton = new Graph<int>(grph);
-
- // Do Some transformation on graph here //
-
- return graphForAutomaton;
-
- }
public string PrintGraph(Graph<int> graph)
{
var s = new StringBuilder();
@@ -463,38 +496,49 @@ namespace Microsoft.Boogie foreach (var e in graph.Edges)
s.AppendLine(" \"" + e.Item1.ToString() + "\" -- " + verticesToEdges[e] + " --> " + " \"" + e.Item2.ToString() + "\";");
s.AppendLine("}");
-
return s.ToString();
-
}
-
- private HashSet<Tuple<int,int>> CollectBackEdges(Graph<int> g, Tuple<int,int> backEdge)
- {
+
+ // Dragon Book Pagepg 662
+ /*
+ * Parameter : backEdge : is an Yield transition in the graph. Compute all backward edges based on predecessors of this node.
+ * This is called for every edge X, CollectBackEdges(graph,X) that has cond "Y".
+ * Return: HashSet<Tuple<int, int>> yieldingEdges : set of edges that can be reached by backEdge which has Y(yield) condition
+ */
+ private HashSet<Tuple<int, int>> CollectBackEdges(Graph<int> g, Tuple<int, int> backEdge)
+ {
int n = backEdge.Item1;
int d = backEdge.Item2;
HashSet<int> loop = new HashSet<int>();
Stack<int> stack = new Stack<int>();
- HashSet<Tuple<int,int>> yieldReachingEdges = new HashSet<Tuple<int,int>>();
+ HashSet<Tuple<int, int>> yieldReachingEdges = new HashSet<Tuple<int, int>>();
loop.Add(d);
if (!n.Equals(d)) // then n is not in loop
{
loop.Add(n);
stack.Push(n); // push n onto stack
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n First pushed item on stack is " + n.ToString());
+#endif
}
while (stack.Count > 0) // not empty
{
int m = stack.Peek();
- // Console.Write("\n Back is : " + m.ToString()+ "\n");
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n Back is : " + m.ToString() + "\n");
+#endif
stack.Pop(); // pop stack
foreach (int p in g.Predecessors(m))
{
- // Contract.Assert(p!= null);
+ // Contract.Assert(p!= null);
if (!(loop.Contains(p)))
{
- Tuple<int , int > yieldReaching = new Tuple<int,int>(p,m);
+ Tuple<int, int> yieldReaching = new Tuple<int, int>(p, m);
yieldReachingEdges.Add(yieldReaching);
- //Console.Write("\n "+ p.ToString()+ " --> " + m.ToString() + "\n");
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n " + p.ToString() + " --> " + m.ToString() + "\n");
+#endif
loop.Add(p);
stack.Push(p); // push p onto stack
}
@@ -502,18 +546,22 @@ namespace Microsoft.Boogie }
return yieldReachingEdges;
}
-
- private HashSet<Tuple<int,int>> BackwardEdgesOfYields(Graph<int> graph)
+ /*
+ * Calls CollectBackEdges for each Y edge existing in graph
+ */
+ private HashSet<Tuple<int, int>> BackwardEdgesOfYields(Graph<int> graph)
{
HashSet<Tuple<int, int>> yieldTrueEdges = new HashSet<Tuple<int, int>>();
-
- foreach(var e in graph.Edges){
-
-
- if(verticesToEdges[e] == "Y"){
- HashSet<Tuple<int,int>> yieldReachingEdges= CollectBackEdges(graph, e);
- foreach(Tuple<int,int> yldrch in yieldReachingEdges){
- // Console.Write("\n" + " From :"+yldrch.Item1.ToString() + " To :"+yldrch.Item2.ToString()+"\n");
+ foreach (var e in graph.Edges)
+ {
+ if (verticesToEdges[e] == "Y")
+ {
+ HashSet<Tuple<int, int>> yieldReachingEdges = CollectBackEdges(graph, e);
+ foreach (Tuple<int, int> yldrch in yieldReachingEdges)
+ {
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n" + " From :" + yldrch.Item1.ToString() + " To :" + yldrch.Item2.ToString() + "\n");
+#endif
yieldTrueEdges.Add(yldrch);
}
}
@@ -521,6 +569,9 @@ namespace Microsoft.Boogie return yieldTrueEdges;
}
+ /*
+ * 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)
{
HashSet<Tuple<int, int>> yieldTrueEdges = BackwardEdgesOfYields(graph);
@@ -557,16 +608,11 @@ namespace Microsoft.Boogie {
verticesToEdges[yldrch] = "D";
}
-
-
-
}
foreach (Tuple<int, int> nyldrch in yieldTypeCheckGraph)
{
-
if (!yieldTrueEdges.Contains(nyldrch))
{
-
if (verticesToEdges[nyldrch] == "Q")
{
verticesToEdges[nyldrch] = "4";
@@ -590,69 +636,60 @@ namespace Microsoft.Boogie else if (verticesToEdges[nyldrch] == "A")
{
verticesToEdges[nyldrch] = "B";
- }
-
+ }
+ else if (verticesToEdges[nyldrch] == "Y")
+ {
+ // Bug found : Yielding(Y) == NonYielding(Y)
+ verticesToEdges[nyldrch] = "D";
+ }
}
-
}
}
- private int[] ComputeFinalStates(Graph<int> graph)
+ private int[] ComputeFinalStates()
{
-
- List<int> finalStatesList = new List<int>();
-
- foreach (int fe in graph.Nodes)
+ int[] finalS = new int[finalStates.Count];
+ for (int i = 0; i < finalStates.Count; i++)
{
- foreach (Tuple<int, int> e in graph.Edges)
- {
- if (!fe.Equals(e.Item1))
- {
- finalStatesList.Add(fe);
- }
- }
+ finalS[i] = finalStates[i];
}
- int[] finalStates = new int[finalStatesList.Count];
-
- for (int i = 0; i < finalStatesList.Count; i++) {
- finalStates[i] = finalStatesList[i];
+#if (DEBUG && !DEBUG_DETAIL)
+ for (int i = 0; i < finalStates.Count; i++)
+ {
+ Console.Write("\nAn final state : \n");
+ Console.Write(finalStates[i].ToString() + " ");
}
-
- return finalStates;
+#endif
+ return finalS;
}
- private List<int> ComputeInitalStates(Graph<int> graph) {
+ private List<int> ComputeInitalStates()
+ {
- List<int> initialStates = new List<int>();
- foreach (int fe in graph.Nodes)
+#if (DEBUG && !DEBUG_DETAIL)
+ for (int i = 0; i<initialStates.Count;i++ )
{
- foreach (Tuple<int, int> e in graph.Edges)
- {
- if (!fe.Equals(e.Item2))
- {
- initialStates.Add(fe);
- }
- }
- }
+ Console.Write("\nAn initial state : \n");
+ Console.Write(initialStates[i].ToString() + " ");
+ }
+#endif
return initialStates;
-
}
-
- private Automaton<BvSet> BuildAutomaton(Graph<int> graph) {
-
+
+ private Automaton<BvSet> BuildAutomaton(Graph<int> graph)
+ {
//List<Move<YieldTypeSet>> transitions = new List<Move<YieldTypeSet>>();
List<int[]> transitions = new List<int[]>();
-
- foreach (Tuple<int, int> e in graph.Edges) {
+ foreach (Tuple<int, int> e in graph.Edges)
+ {
if (verticesToEdges[e] == "3")
{
-
int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 51; // ASCII 3
- transition[2]=51;
- transition[3] = e.Item2;
- transitions.Add(transition);
+ transition[2] = 51;
+ transition[3] = e.Item2;
+ transitions.Add(transition);
/*
List<int> transition = new List<int>();
@@ -661,14 +698,14 @@ namespace Microsoft.Boogie 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")
{
int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 49; // ASCII 1
- transition[2]=49;
+ transition[2] = 49;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -679,14 +716,14 @@ namespace Microsoft.Boogie transitions.Add(transition);
*/
//transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.P)));
-
+
}
else if (verticesToEdges[e] == "7")
{
int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 55; // ASCII 7
- transition[2]=55;
+ transition[2] = 55;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -702,10 +739,10 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 53; // ASCII 5
- transition[2]=53;
+ transition[2] = 53;
transition[3] = e.Item2;
transitions.Add(transition);
-
+
/*
List<int> transition = new List<int>();
transition.Add(e.Item1);
@@ -719,10 +756,10 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 57; // ASCII 9
- transition[2]=57;
+ transition[2] = 57;
transition[3] = e.Item2;
transitions.Add(transition);
-
+
/*
List<int> transition = new List<int>();
transition.Add(e.Item1);
@@ -736,7 +773,7 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 65; // ASCII A
- transition[2]=65;
+ transition[2] = 65;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -752,10 +789,10 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 68; // ASCII D
- transition[2]=68;
+ transition[2] = 68;
transition[3] = e.Item2;
transitions.Add(transition);
-
+
/*
List<int> transition = new List<int>();
transition.Add(e.Item1);
@@ -769,7 +806,7 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 52; // ASCII 4
- transition[2]=52;
+ transition[2] = 52;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -786,7 +823,7 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 50; // ASCII 2
- transition[2]=50;
+ transition[2] = 50;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -802,7 +839,7 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 56; // ASCII 8
- transition[2]=56;
+ transition[2] = 56;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -836,7 +873,7 @@ namespace Microsoft.Boogie transition[1] = 67; // ASCII C
transition[2] = 67;
transition[3] = e.Item2;
-
+
transitions.Add(transition);
/*
List<int> transition = new List<int>();
@@ -860,18 +897,20 @@ namespace Microsoft.Boogie transition.Add(66);
transition.Add(e.Item2);
transitions.Add(transition);
- *///transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.AF)));
-
+ */
+ //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.AF)));
+
}
- else if (verticesToEdges[e] == "E") {
-
+ else if (verticesToEdges[e] == "E")
+ {
+
int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 69; // ASCII E
transition[2] = 69;
- transition[3] =e.Item2;
+ transition[3] = e.Item2;
transitions.Add(transition);
-
+
/*List<int> transition = new List<int>();
transition.Add(e.Item1);
transition.Add(69);
@@ -879,32 +918,41 @@ namespace Microsoft.Boogie transitions.Add(transition);
*/
//transitions.Add(Move<YieldTypeSet>.Epsilon(e.Item1,e.Item2));
-
+
}
-
- }
+ }
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write(" \n Transitions before EPSILONS are added\n ");
+ for (int i = 0; i < transitions.Count; i++)
+ {
+ int[] trans = transitions[i];
+ Console.Write("\n From : " + trans[0].ToString() + "--- " + trans[1] + " --- " + " to : " + trans[3].ToString());
+ }
+#endif
var solver = new CharSetSolver();
-
+
// get initial states
- List<int> initialStates = ComputeInitalStates(graph);
+ List<int> initialStates = ComputeInitalStates();
+
// get final states
- int[] finalStates = ComputeFinalStates(graph);
- // put Epslion from first initial state seen to other initial states created
+ int[] finalStates = ComputeFinalStates();
- foreach (int s in initialStates) {
+ // put Epslion from first initial state seen to other initial states created
+ foreach (int s in initialStates)
+ {
// Put every one epsilon to itself no problem
/*if (!s.Equals(concreteInitialState)) { }*/
-
+
if (!s.Equals(concreteInitialState))
- {
+ {
int[] transition = new int[4];
transition[0] = concreteInitialState;
transition[1] = 69;
transition[2] = 69;
- transition[3] = s;
-
+ transition[3] = s;
+ transitions.Add(transition);
/*
List<int> transition = new List<int>();
transition.Add(concreteInitialState);
@@ -913,41 +961,54 @@ namespace Microsoft.Boogie transition.Add(s);
transitions.Add(transition);
- */
+ */
}
//transitions.Add(Move<YieldTypeSet>.Epsilon(concreteInitialState,s));
}
-
-
-
-
- // int[][] transitionArray = new int[5][];
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write(" \n Transitions are\n ");
+ for (int i = 0; i < transitions.Count; i++)
+ {
+ int[] trans = transitions[i];
+ Console.Write("\n From : " + trans[0].ToString() + "--- " + trans[1] + " --- " + " to : " + trans[3].ToString());
+ }
+#endif
+
+
// create Automaton
- Automaton<BvSet> yieldTypeCheckAutomaton = solver.ReadFromRanges(concreteInitialState,finalStates,transitions);
+ Automaton<BvSet> yieldTypeCheckAutomaton = solver.ReadFromRanges(concreteInitialState, finalStates, transitions);
+#if (DEBUG && !DEBUG_DETAIL)
+ 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())
+ {
+ // Ask Margus,Shaz : BvSet concerns !
+ Console.WriteLine(move.SourceState.ToString() + " " + move.Condition.ToString() + " " + move.TargetState.ToString());
+ //solver.ShowDAG(yieldTypeCheckAutomaton,ytypeChecked.Proc.Name+" Automaton");
+ // solver.ShowGraph(yieldTypeCheckAutomaton,ytypeChecked.Proc.Name+" Automaton");
+ }
+#endif
//create Automaton
//Automaton<YieldTypeSet> yieldTypeCheckAutomaton = Automaton<YieldTypeSet>.Create(concreteInitialState, finalStates, transitions); ;
-
- return yieldTypeCheckAutomaton;
+ return yieldTypeCheckAutomaton;
}
-
+
private void Error(Absy node, string message)
{
checkingContext.Error(node, message);
errorCount++;
}
-
-
}
static class Transitions
{
-
public static uint P = 0x1;
public static uint Q = 0x4;
public static uint Y = 0x1000;
@@ -961,38 +1022,36 @@ namespace Microsoft.Boogie public static uint RF = 0x20;
public static uint LF = 0x800;
public static uint AF = 0x400;
-
-
}
- // Ask Margus :
+ // 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?
+ // 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
+ //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;
@@ -1112,4 +1171,5 @@ namespace Microsoft.Boogie }
}
+
#endif
\ No newline at end of file |