diff options
| author |  qadeer <unknown> | 2014-04-20 21:08:11 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-04-20 21:08:11 -0700 |
| commit | b23a93d04bd66014854af44258264f9867c73f55 (patch) | |
| tree | cdc58392e8428189951ed390745a9f772218d4d0 /Source | |
| parent | 2e190e24541eb9608e1d4ba18874c2403156e792 (diff) | |
added simulation relation computation to yield type checking
updated the type check to incorporate {:terminates} annotation
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Concurrency/Concurrency.csproj | 3 | ||||
| -rw-r--r-- | Source/Concurrency/SimulationRelation.cs | 197 | ||||
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 271 |
3 files changed, 331 insertions, 140 deletions
diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj index 2d2b7d12..c245d05a 100644 --- a/Source/Concurrency/Concurrency.csproj +++ b/Source/Concurrency/Concurrency.csproj @@ -11,7 +11,7 @@ <AssemblyName>Concurrency</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<PlatformTarget>AnyCPU</PlatformTarget>
@@ -76,6 +76,7 @@ <Compile Include="OwickiGries.cs" />
<Compile Include="Program.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="SimulationRelation.cs" />
<Compile Include="TypeCheck.cs" />
<Compile Include="YieldTypeChecker.cs" />
</ItemGroup>
diff --git a/Source/Concurrency/SimulationRelation.cs b/Source/Concurrency/SimulationRelation.cs new file mode 100644 index 00000000..7f130f76 --- /dev/null +++ b/Source/Concurrency/SimulationRelation.cs @@ -0,0 +1,197 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie.GraphUtil;
+
+namespace Microsoft.Boogie
+{
+ public class SimulationRelation<A, B, L>
+ {
+ class Graph<T>
+ {
+ HashSet<T> nodes;
+ Dictionary<T, Dictionary<L, List<T>>> successors;
+ Dictionary<T, Dictionary<L, List<T>>> predecessors;
+
+ public Graph(List<Tuple<T, L, T>> edges)
+ {
+ nodes = new HashSet<T>();
+ successors = new Dictionary<T, Dictionary<L, List<T>>>();
+ predecessors = new Dictionary<T, Dictionary<L, List<T>>>();
+ foreach (Tuple<T, L, T> edge in edges)
+ {
+ T source = edge.Item1;
+ L label = edge.Item2;
+ T dest = edge.Item3;
+ nodes.Add(source);
+ nodes.Add(dest);
+ if (!successors.ContainsKey(source))
+ {
+ successors[source] = new Dictionary<L, List<T>>();
+ }
+ if (!successors[source].ContainsKey(label))
+ {
+ successors[source][label] = new List<T>();
+ }
+ if (!predecessors.ContainsKey(dest))
+ {
+ predecessors[dest] = new Dictionary<L, List<T>>();
+ }
+ if (!predecessors[dest].ContainsKey(label))
+ {
+ predecessors[dest][label] = new List<T>();
+ }
+ successors[source][label].Add(dest);
+ predecessors[dest][label].Add(source);
+ }
+ }
+
+ public IEnumerable<T> Nodes { get { return nodes; } }
+
+ public IEnumerable<T> Post(T t, L l)
+ {
+ if (successors.ContainsKey(t) && successors[t].ContainsKey(l))
+ {
+ return successors[t][l];
+ }
+ else
+ {
+ return Enumerable.Empty<T>();
+ }
+ }
+
+ public IEnumerable<T> Post(IEnumerable<T> set, L l)
+ {
+ return set.Select(x => Post(x, l)).Aggregate(Enumerable.Empty<T>(), (p, q) => p.Concat(q));
+ }
+
+ public IEnumerable<T> Pre(T t, L l)
+ {
+ if (predecessors.ContainsKey(t) && predecessors[t].ContainsKey(l))
+ {
+ return predecessors[t][l];
+ }
+ else
+ {
+ return Enumerable.Empty<T>();
+ }
+ }
+
+ public IEnumerable<T> Pre(IEnumerable<T> set, L l)
+ {
+ return set.Select(x => Pre(x, l)).Aggregate(Enumerable.Empty<T>(), (p, q) => p.Concat(q));
+ }
+
+ public IEnumerable<L> PostLabels(T t)
+ {
+ if (successors.ContainsKey(t))
+ {
+ return successors[t].Keys;
+ }
+ else
+ {
+ return Enumerable.Empty<L>();
+ }
+ }
+
+ public IEnumerable<L> PreLabels(T t)
+ {
+ if (predecessors.ContainsKey(t))
+ {
+ return predecessors[t].Keys;
+ }
+ else
+ {
+ return Enumerable.Empty<L>();
+ }
+ }
+ }
+
+ Graph<A> aGraph;
+ Graph<B> bGraph;
+ Dictionary<A, HashSet<B>> initialConstraints;
+
+ public SimulationRelation(List<Tuple<A, L, A>> aEdges, List<Tuple<B, L, B>> bEdges, Dictionary<A, HashSet<B>> initialConstraints)
+ {
+ this.aGraph = new Graph<A>(aEdges);
+ this.bGraph = new Graph<B>(bEdges);
+ this.initialConstraints = initialConstraints;
+ }
+
+ public Dictionary<A, HashSet<B>> ComputeSimulationRelation()
+ {
+ Dictionary<A, HashSet<B>> prevsim;
+ Dictionary<A, HashSet<B>> sim;
+ Dictionary<Tuple<A, L>, HashSet<B>> remove;
+ Queue<Tuple<A,L>> workQueue;
+
+ prevsim = new Dictionary<A, HashSet<B>>();
+ sim = new Dictionary<A, HashSet<B>>();
+ remove = new Dictionary<Tuple<A, L>, HashSet<B>>();
+ workQueue = new Queue<Tuple<A,L>>();
+ foreach (var a in aGraph.Nodes)
+ {
+ prevsim[a] = new HashSet<B>(bGraph.Nodes);
+ sim[a] = new HashSet<B>();
+ HashSet<L> aOutgoingLabels = new HashSet<L>(aGraph.PostLabels(a));
+ foreach (var b in bGraph.Nodes)
+ {
+ IEnumerable<L> bOutgoingLabels = bGraph.PostLabels(b);
+ if (aOutgoingLabels.IsSubsetOf(bOutgoingLabels))
+ {
+ sim[a].Add(b);
+ }
+ }
+ if (initialConstraints.ContainsKey(a))
+ {
+ sim[a].IntersectWith(initialConstraints[a]);
+ }
+
+ foreach (var l in aGraph.PreLabels(a))
+ {
+ Tuple<A, L> x = new Tuple<A, L>(a, l);
+ remove[x] = new HashSet<B>(bGraph.Pre(prevsim[a], l).Except(bGraph.Pre(sim[a], l)));
+ if (remove[x].Count > 0)
+ {
+ workQueue.Enqueue(x);
+ }
+ }
+ }
+
+ while (workQueue.Count > 0)
+ {
+ Tuple<A,L> x = workQueue.Dequeue();
+ A v = x.Item1;
+ foreach (A u in aGraph.Pre(v, x.Item2))
+ {
+ foreach (B w in remove[x])
+ {
+ if (sim[u].Contains(w))
+ {
+ sim[u].Remove(w);
+ foreach (L l in bGraph.PreLabels(w))
+ {
+ foreach (B b in bGraph.Pre(w, l))
+ {
+ if (bGraph.Post(b, l).Intersect(sim[u]).Count() == 0)
+ {
+ Tuple<A, L> z = new Tuple<A, L>(u, l);
+ if (!remove.ContainsKey(z))
+ remove[z] = new HashSet<B>();
+ remove[z].Add(b);
+ workQueue.Enqueue(z);
+ }
+ }
+ }
+ }
+ }
+ }
+ prevsim[v] = new HashSet<B>(sim[v]);
+ remove[x] = new HashSet<B>();
+ }
+
+ return sim;
+ }
+ }
+}
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index fd632994..4ba23c2e 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -18,6 +18,7 @@ namespace Microsoft.Boogie {
static CharSetSolver yieldTypeCheckerAutomatonSolver;
static Automaton<BvSet> yieldTypeCheckerAutomaton;
+ static List<Tuple<int, int, int>> yieldTypeCheckerAutomatonEdges;
static YieldTypeChecker()
{
yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
@@ -26,24 +27,103 @@ namespace Microsoft.Boogie new int[] {0, 'P', 'P', 0 },
new int[] {0, 'Y', 'Y', 0 },
new int[] {0, 'Y', 'Y', 1 },
+ new int[] {0, 'Y', 'Y', 2 },
new int[] {1, 'P', 'P', 1 },
new int[] {1, 'R', 'R', 1 },
new int[] {1, 'B', 'B', 1 },
new int[] {1, 'Y', 'Y', 1 },
new int[] {1, 'Y', 'Y', 0 },
new int[] {1, 'A', 'A', 2 },
- new int[] {1, -1, -1, 2 },
+ new int[] {1, 'P', 'P', 2 },
+ new int[] {1, 'R', 'R', 2 },
+ new int[] {1, 'B', 'B', 2 },
+ new int[] {1, 'Y', 'Y', 2 },
new int[] {2, 'L', 'L', 2 },
new int[] {2, 'B', 'B', 2 },
+ new int[] {2, 'P', 'P', 2 },
+ new int[] {2, 'Y', 'Y', 2 },
new int[] {2, 'Y', 'Y', 1 },
new int[] {2, 'Y', 'Y', 0 },
});
// uncomment the following line to visualize the spec automaton
// yieldTypeCheckerAutomatonSolver.ShowGraph(yieldTypeCheckerAutomaton, "yieldTypeCheckerAutomaton.dgml");
+
+ yieldTypeCheckerAutomatonEdges = new List<Tuple<int, int, int>>();
+ AddEdge(0, 'P', 0);
+ AddEdge(0, 'Y', 0);
+ AddEdge(0, 'Y', 1);
+ AddEdge(0, 'Y', 2);
+ AddEdge(1, 'P', 1);
+ AddEdge(1, 'R', 1);
+ AddEdge(1, 'B', 1);
+ AddEdge(1, 'Y', 1);
+ AddEdge(1, 'Y', 0);
+ AddEdge(1, 'A', 2);
+ AddEdge(1, 'P', 2);
+ AddEdge(1, 'R', 2);
+ AddEdge(1, 'B', 2);
+ AddEdge(1, 'Y', 2);
+ AddEdge(2, 'L', 2);
+ AddEdge(2, 'B', 2);
+ AddEdge(2, 'P', 2);
+ AddEdge(2, 'Y', 2);
+ AddEdge(2, 'Y', 1);
+ AddEdge(2, 'Y', 0);
+ }
+ private static void AddEdge(int source, int label, int dest)
+ {
+ yieldTypeCheckerAutomatonEdges.Add(new Tuple<int, int, int>(source, label, dest));
}
- public void IsYieldTypeSafe(Automaton<BvSet> implAutomaton)
+ public void IsYieldTypeSafe()
{
+ List<int[]> transitions = new List<int[]>();
+ foreach (Tuple<int, int> e in edgeLabels.Keys)
+ {
+ int label = edgeLabels[e];
+ int[] transition = new int[4];
+ transition[0] = e.Item1;
+ transition[1] = label;
+ transition[2] = label;
+ transition[3] = e.Item2;
+ transitions.Add(transition);
+ }
+
+ int dummyInitial = stateCounter;
+ foreach (Tuple<int, int> e in edgeLabels.Keys)
+ {
+ if (initialStates.Contains(e.Item1))
+ {
+ int[] transition = new int[4];
+ transition[0] = dummyInitial;
+ transition[1] = edgeLabels[e];
+ transition[2] = edgeLabels[e];
+ transition[3] = e.Item2;
+ transitions.Add(transition);
+ }
+ }
+
+ List<Tuple<int, int, int>> implEdges = new List<Tuple<int, int, int>>();
+ foreach (int[] transition in transitions)
+ {
+ implEdges.Add(new Tuple<int, int, int>(transition[0], transition[1], transition[3]));
+ }
+ Dictionary<int, HashSet<int>> initialConstraints = new Dictionary<int, HashSet<int>>();
+ initialConstraints[dummyInitial] = new HashSet<int>(new int[] {0});
+ foreach (var finalState in finalStates)
+ {
+ initialConstraints[finalState] = new HashSet<int>(new int[] { 0 });
+ }
+ foreach (Block block in loopHeaders)
+ {
+ if (!IsTerminatingLoopHeader(block))
+ {
+ initialConstraints[absyToNode[block]] = new HashSet<int>(new int[] { 0, 1 });
+ }
+ }
+
+ Automaton<BvSet> implAutomaton = yieldTypeCheckerAutomatonSolver.ReadFromRanges(dummyInitial, finalStates.ToArray(), transitions);
+ // yieldTypeCheckerAutomatonSolver.SaveAsDgml(implAutomaton, string.Format("{0}.dgml", impl.Name));
List<BvSet> witnessSet;
var isNonEmpty = Automaton<BvSet>.CheckDifference(
implAutomaton,
@@ -56,8 +136,33 @@ namespace Microsoft.Boogie {
moverTypeChecker.Error(impl, PrintErrorTrace(diffAutomaton));
}
+
+ SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, yieldTypeCheckerAutomatonEdges, initialConstraints);
+ Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
+ foreach (Block block in loopHeaders)
+ {
+ if (simulationRelation[absyToNode[block]].Count == 0)
+ {
+ IToken tok = block.tok;
+ moverTypeChecker.Error(impl, string.Format("Loop at {0}({1}, {2}) not simulated appropriately at phase {3}\n", tok.filename, tok.line, tok.col, currPhaseNum));
+ yieldTypeCheckerAutomatonSolver.SaveAsDgml(implAutomaton, string.Format("{0}_{1}.dgml", impl.Name, currPhaseNum));
+ }
+ }
}
+ static bool IsTerminatingLoopHeader(Block block)
+ {
+ foreach (Cmd cmd in block.Cmds)
+ {
+ AssertCmd assertCmd = cmd as AssertCmd;
+ if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates"))
+ {
+ return true;
+ }
+ }
+ return false;
+ }
+
public string PrintErrorTrace(Automaton<BvSet> errorAutomaton)
{
String s = "\nBody of " + impl.Proc.Name + " is not yield_type_safe at phase " + currPhaseNum.ToString() + "\n";
@@ -74,16 +179,18 @@ namespace Microsoft.Boogie public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker)
{
- foreach (int yTypeCheckCurrentPhaseNum in moverTypeChecker.allPhaseNums)
+ foreach (var decl in moverTypeChecker.program.TopLevelDeclarations)
{
- foreach (var decl in moverTypeChecker.program.TopLevelDeclarations)
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ impl.PruneUnreachableBlocks();
+ Graph<Block> implGraph = Program.GraphFromImpl(impl);
+ implGraph.ComputeLoops();
+ int phaseNumSpecImpl = moverTypeChecker.FindPhaseNumber(impl.Proc);
+ foreach (int phaseNum in moverTypeChecker.allPhaseNums)
{
- Implementation impl = decl as Implementation;
- if (impl == null) continue;
- int phaseNumSpecImpl = moverTypeChecker.FindPhaseNumber(impl.Proc);
- if (yTypeCheckCurrentPhaseNum > phaseNumSpecImpl) continue;
-
- YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, yTypeCheckCurrentPhaseNum);
+ if (phaseNum > phaseNumSpecImpl) continue;
+ YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, phaseNum, implGraph.Headers);
}
}
}
@@ -107,12 +214,14 @@ namespace Microsoft.Boogie HashSet<int> initialStates;
HashSet<int> finalStates;
Dictionary<Tuple<int, int>, int> edgeLabels;
+ IEnumerable<Block> loopHeaders;
- public YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum)
+ public YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum, IEnumerable<Block> loopHeaders)
{
this.moverTypeChecker = moverTypeChecker;
this.impl = impl;
this.currPhaseNum = currPhaseNum;
+ this.loopHeaders = loopHeaders;
this.stateCounter = 0;
this.absyToNode = new Dictionary<Absy, int>();
this.initialStates = new HashSet<int>();
@@ -122,6 +231,8 @@ namespace Microsoft.Boogie foreach (Block block in impl.Blocks)
{
+ absyToNode[block] = stateCounter;
+ stateCounter++;
foreach (Cmd cmd in block.Cmds)
{
absyToNode[cmd] = stateCounter;
@@ -136,12 +247,14 @@ namespace Microsoft.Boogie }
foreach (Block block in impl.Blocks)
{
+ Absy blockEntry = block.Cmds.Count == 0 ? (Absy)block.TransferCmd : (Absy)block.Cmds[0];
+ edgeLabels[new Tuple<int, int>(absyToNode[block], absyToNode[blockEntry])] = 'P';
+
GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
if (gotoCmd == null) continue;
foreach (Block successor in gotoCmd.labelTargets)
{
- Absy successorEntry = successor.Cmds.Count == 0 ? (Absy)successor.TransferCmd : (Absy)successor.Cmds[0];
- edgeLabels[new Tuple<int, int>(absyToNode[block.TransferCmd], absyToNode[successorEntry])] = 'Q';
+ edgeLabels[new Tuple<int, int>(absyToNode[gotoCmd], absyToNode[successor])] = 'P';
}
}
@@ -151,53 +264,11 @@ namespace Microsoft.Boogie this.nodeToAbsy[state.Value] = state.Key;
}
- Graph<int> graph = ComputeGraph();
-
- // Compute all edges that can reach yield or exit
- HashSet<int> targetStates = new HashSet<int>(finalStates);
- foreach (Tuple<int, int> edge in edgeLabels.Keys)
- {
- if (edgeLabels[edge] == 'Y')
- {
- targetStates.Add(edge.Item1);
- }
- }
- HashSet<Tuple<int, int>> backwardReachableEdges = CollectBackwardReachableEdges(graph, targetStates);
- HashSet<Tuple<int, int>> edges = new HashSet<Tuple<int, int>>(edgeLabels.Keys);
- foreach (Tuple<int, int> edge in edges)
- {
- int label = edgeLabels[edge];
- if (label == 'A' || label == 'L')
- {
- if (!backwardReachableEdges.Contains(edge))
- {
- moverTypeChecker.Error(impl, "Error message TBD");
- }
- }
- else if (label == 'B')
- {
- if (!backwardReachableEdges.Contains(edge))
- {
- edgeLabels[edge] = 'R';
- }
- }
- else if (label == 'Q')
- {
- if (!backwardReachableEdges.Contains(edge))
- {
- edgeLabels[edge] = 'P';
- }
- else
- {
- edgeLabels[edge] = -1;
- }
- }
- }
- Automaton<BvSet> implYieldTypeSafeCheckAut = BuildAutomatonYieldSafe();
- IsYieldTypeSafe(implYieldTypeSafeCheckAut);
+ ComputeGraph();
+ IsYieldTypeSafe();
}
- private Graph<int> ComputeGraph()
+ private void ComputeGraph()
{
foreach (Block block in impl.Blocks)
{
@@ -212,7 +283,7 @@ namespace Microsoft.Boogie CallCmd callCmd = cmd as CallCmd;
if (callCmd.IsAsync)
{
- edgeLabels[edge] = 'Q';
+ edgeLabels[edge] = 'P';
}
else
{
@@ -286,7 +357,7 @@ namespace Microsoft.Boogie {
edgeLabels[edge] = 'Y';
}
- else if (cmd is AssumeCmd)
+ else if (cmd is AssumeCmd || cmd is AssignCmd || cmd is HavocCmd)
{
if (AccessesGlobals(cmd))
{
@@ -298,34 +369,12 @@ namespace Microsoft.Boogie edgeLabels[edge] = 'P';
}
}
- else if (cmd is AssertCmd)
- {
- edgeLabels[edge] = 'Q';
- }
- else if (cmd is AssignCmd || cmd is HavocCmd)
- {
- if (AccessesGlobals(cmd))
- {
- finalStates.Add(curr);
- initialStates.Add(next);
- }
- else
- {
- edgeLabels[edge] = 'Q';
- }
- }
else
{
- edgeLabels[edge] = 'Q';
+ edgeLabels[edge] = 'P';
}
}
}
- Graph<int> graph = new Graph<int>(new HashSet<Tuple<int, int>>(edgeLabels.Keys));
- for (int i = 0; i < stateCounter; i++)
- {
- graph.AddSource(i);
- }
- return graph;
}
private static bool AccessesGlobals(Cmd cmd)
@@ -344,62 +393,6 @@ namespace Microsoft.Boogie s.AppendLine("}");
return s.ToString();
}
-
- private static HashSet<Tuple<int, int>> CollectBackwardReachableEdges(Graph<int> graph, HashSet<int> targets)
- {
- HashSet<Tuple<int, int>> edgesReachable = new HashSet<Tuple<int, int>>();
- HashSet<int> gray = new HashSet<int>();
- Queue<int> frontier = new Queue<int>();
- foreach (int v in targets)
- {
- gray.Add(v);
- frontier.Enqueue(v);
- }
- while (frontier.Count > 0)
- {
- int v = frontier.Dequeue();
- foreach (int u in graph.Predecessors(v))
- {
- edgesReachable.Add(new Tuple<int, int>(u, v));
- if (!gray.Contains(u))
- {
- gray.Add(u);
- frontier.Enqueue(u);
- }
- }
- }
- return edgesReachable;
- }
-
- private Automaton<BvSet> BuildAutomatonYieldSafe()
- {
- List<int[]> transitions = new List<int[]>();
- foreach (Tuple<int, int> e in edgeLabels.Keys)
- {
- int label = edgeLabels[e];
- Debug.Assert(label != 'Q');
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = label;
- transition[2] = label;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
-
- int dummyInitial = stateCounter;
- foreach (int s in initialStates)
- {
- int[] transition = new int[4];
- transition[0] = dummyInitial;
- transition[1] = -1;
- transition[2] = -1;
- transition[3] = s;
- transitions.Add(transition);
- }
-
- Automaton<BvSet> yieldTypeCheckAutomaton = yieldTypeCheckerAutomatonSolver.ReadFromRanges(dummyInitial, finalStates.ToArray(), transitions);
- return yieldTypeCheckAutomaton;
- }
}
}
|