diff options
| author |  Ally Donaldson <unknown> | 2014-01-17 10:36:33 +0000 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2014-01-17 10:36:33 +0000 |
| commit | b6e440731cf30f00b7b8840be8a1e048c8f21d60 (patch) | |
| tree | 7000e81ad029df274530352db584a1629a1fdd4f /Source | |
| parent | 16bc038b94f93c37ce5ecd1ba0cbeff1a3aa5ec7 (diff) | |
| parent | 4b265b8ef4428e6d583359650c07c652884112bb (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 212 | ||||
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 67 | ||||
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 5 | ||||
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 1559 |
4 files changed, 366 insertions, 1477 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 75e1f7e3..78943c1b 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -41,53 +41,6 @@ namespace Microsoft.Boogie this.gatePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
this.failurePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
}
- private sealed class MySubstituter : Duplicator
- {
- private readonly Substitution outsideOld;
- private readonly Substitution insideOld;
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(insideOld != null);
- }
-
- public MySubstituter(Substitution outsideOld, Substitution insideOld)
- : base()
- {
- Contract.Requires(outsideOld != null && insideOld != null);
- this.outsideOld = outsideOld;
- this.insideOld = insideOld;
- }
-
- private bool insideOldExpr = false;
-
- public override Expr VisitIdentifierExpr(IdentifierExpr node)
- {
- Contract.Ensures(Contract.Result<Expr>() != null);
- Expr e = null;
-
- if (insideOldExpr)
- {
- e = insideOld(node.Decl);
- }
- else
- {
- e = outsideOld(node.Decl);
- }
- return e == null ? base.VisitIdentifierExpr(node) : e;
- }
-
- public override Expr VisitOldExpr(OldExpr node)
- {
- Contract.Ensures(Contract.Result<Expr>() != null);
- bool previouslyInOld = insideOldExpr;
- insideOldExpr = true;
- Expr tmp = (Expr)this.Visit(node.Expr);
- OldExpr e = new OldExpr(node.tok, tmp);
- insideOldExpr = previouslyInOld;
- return e;
- }
- }
public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
{
@@ -141,6 +94,20 @@ namespace Microsoft.Boogie }
}
+ public sealed class MyDuplicator : Duplicator
+ {
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ IdentifierExpr ret = (IdentifierExpr) base.VisitIdentifierExpr(node);
+ if (ret.Decl is GlobalVariable)
+ {
+ return new OldExpr(Token.NoToken, ret);
+ }
+ else
+ return ret;
+ }
+ }
+
public class TransitionRelationComputation
{
private Program program;
@@ -193,6 +160,21 @@ namespace Microsoft.Boogie }
}
+ struct PathInfo
+ {
+ public HashSet<Variable> existsVars;
+ public Dictionary<Variable, Expr> varToExpr;
+ public Expr pathExpr;
+
+ public PathInfo(HashSet<Variable> existsVars, Dictionary<Variable, Expr> varToExpr, Expr pathExpr)
+ {
+ this.existsVars = existsVars;
+ this.varToExpr = varToExpr;
+ this.pathExpr = pathExpr;
+ }
+ }
+
+ private List<PathInfo> paths = new List<PathInfo>();
private Expr CalculatePathCondition()
{
HashSet<Variable> existsVars = new HashSet<Variable>();
@@ -212,14 +194,14 @@ namespace Microsoft.Boogie {
varToExpr[v] = Expr.Ident(v);
}
- Expr returnExpr = Expr.True;
+ Expr pathExpr = Expr.True;
int boundVariableCount = 0;
foreach (Cmd cmd in path)
{
if (cmd is AssumeCmd)
{
AssumeCmd assumeCmd = cmd as AssumeCmd;
- returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr);
+ pathExpr = Expr.And(assumeCmd.Expr, pathExpr);
}
else if (cmd is AssignCmd)
{
@@ -229,7 +211,7 @@ namespace Microsoft.Boogie {
map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];
}
- Substitute(map, ref returnExpr, ref varToExpr);
+ Substitute(map, ref pathExpr, ref varToExpr);
}
else if (cmd is HavocCmd)
{
@@ -241,13 +223,15 @@ namespace Microsoft.Boogie map[ie.Decl] = new IdentifierExpr(Token.NoToken, bv);
existsVars.Add(bv);
}
- Substitute(map, ref returnExpr, ref varToExpr);
+ Substitute(map, ref pathExpr, ref varToExpr);
}
else
{
Debug.Assert(false);
}
}
+ paths.Add(new PathInfo(existsVars, varToExpr, pathExpr));
+
Dictionary<Variable, Expr> existsMap = new Dictionary<Variable, Expr>();
foreach (Variable v in varToExpr.Keys)
{
@@ -258,21 +242,39 @@ namespace Microsoft.Boogie existsVars.Remove(ie.Decl);
}
}
- Substitute(existsMap, ref returnExpr, ref varToExpr);
- returnExpr = new OldExpr(Token.NoToken, returnExpr);
+ pathExpr = (new MyDuplicator()).VisitExpr(pathExpr);
foreach (Variable v in varToExpr.Keys)
{
- returnExpr = Expr.And(returnExpr, Expr.Eq(Expr.Ident(v), varToExpr[v]));
+ pathExpr = Expr.And(pathExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v])));
}
+ pathExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(existsMap), pathExpr);
if (existsVars.Count > 0)
{
- returnExpr = new ExistsExpr(Token.NoToken, new List<Variable>(existsVars), returnExpr);
+ pathExpr = new ExistsExpr(Token.NoToken, new List<Variable>(existsVars), pathExpr);
+ }
+ return pathExpr;
+ }
+
+ public Expr LeftMoverCompute(Expr failureExpr)
+ {
+ Expr returnExpr = Expr.False;
+ foreach (PathInfo path in paths)
+ {
+ Expr expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(path.varToExpr), failureExpr);
+ expr = Expr.And(path.pathExpr, expr);
+ expr = new OldExpr(Token.NoToken, expr);
+ if (path.existsVars.Count > 0)
+ {
+ expr = new ExistsExpr(Token.NoToken, new List<Variable>(path.existsVars), expr);
+ }
+ returnExpr = Expr.Or(returnExpr, expr);
}
return returnExpr;
}
private void Search(Block b, bool inFirst)
{
+ int pathSizeAtEntry = path.Count;
foreach (Cmd cmd in b.Cmds)
{
path.Push(cmd);
@@ -304,7 +306,8 @@ namespace Microsoft.Boogie Search(target, inFirst);
}
}
- foreach (Cmd cmd in b.Cmds)
+ Debug.Assert(path.Count >= pathSizeAtEntry);
+ while (path.Count > pathSizeAtEntry)
{
path.Pop();
}
@@ -379,7 +382,7 @@ namespace Microsoft.Boogie private void CreateCommutativityChecker(Program program, ActionInfo first, ActionInfo second)
{
- if (first == second)
+ if (first == second && first.thatInParams.Count == 0 && first.thatOutParams.Count == 0)
return;
if (first.CommutesWith(second))
return;
@@ -416,7 +419,9 @@ namespace Microsoft.Boogie List<Requires> requires = DisjointnessRequires(program, first, second);
List<Ensures> ensures = new List<Ensures>();
Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).Compute();
- ensures.Add(new Ensures(false, transitionRelation));
+ Ensures ensureCheck = new Ensures(false, transitionRelation);
+ ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name);
+ ensures.Add(ensureCheck);
string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);
List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));
@@ -450,7 +455,9 @@ namespace Microsoft.Boogie foreach (AssertCmd assertCmd in first.thatGate)
{
requires.Add(new Requires(false, assertCmd.Expr));
- ensures.Add(new Ensures(false, assertCmd.Expr));
+ Ensures ensureCheck = new Ensures(assertCmd.tok, false, assertCmd.Expr, null);
+ ensureCheck.ErrorData = string.Format("Gate not preserved by {0}", second.proc.Name);
+ ensures.Add(ensureCheck);
}
string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
@@ -464,49 +471,6 @@ namespace Microsoft.Boogie private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
{
- Debug.Assert(second.isNonBlocking);
- if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
- return;
- Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
- if (failurePreservationCheckerCache.Contains(actionPair))
- return;
- failurePreservationCheckerCache.Add(actionPair);
-
- List<Variable> inputs = new List<Variable>();
- inputs.AddRange(first.thatInParams);
- inputs.AddRange(second.thisInParams);
-
- Expr failureExpr = Expr.True;
- foreach (AssertCmd assertCmd in first.thatGate)
- {
- failureExpr = Expr.And(assertCmd.Expr, failureExpr);
- }
- failureExpr = Expr.Not(failureExpr);
-
- List<Requires> requires = DisjointnessRequires(program, first, second);
- requires.Add(new Requires(false, failureExpr));
-
- List<Ensures> ensures = new List<Ensures>();
- ensures.Add(new Ensures(false, failureExpr));
-
- List<Variable> outputs = new List<Variable>();
- outputs.AddRange(first.thatOutParams);
- outputs.AddRange(second.thisOutParams);
- List<Variable> locals = new List<Variable>();
- locals.AddRange(second.thisAction.LocVars);
- List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);
- string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
- List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
- program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));
- Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
- Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
- impl.Proc = proc;
- this.decls.Add(impl);
- this.decls.Add(proc);
- }
-
- private void CreateFailurePreservationCheckerExists(Program program, ActionInfo first, ActionInfo second)
- {
if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0 && second.isNonBlocking)
return;
@@ -524,48 +488,22 @@ namespace Microsoft.Boogie {
requiresExpr = Expr.And(assertCmd.Expr, requiresExpr);
}
- requiresExpr = Expr.Not(requiresExpr);
+ Expr failureExpr = Expr.Not(requiresExpr);
List<Requires> requires = DisjointnessRequires(program, first, second);
- requires.Add(new Requires(false, requiresExpr));
+ requires.Add(new Requires(false, failureExpr));
foreach (AssertCmd assertCmd in second.thisGate)
{
requires.Add(new Requires(false, assertCmd.Expr));
}
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- Dictionary<Variable, Expr> oldMap = new Dictionary<Variable, Expr>();
- List<Variable> boundVars = new List<Variable>();
- foreach (Variable v in program.GlobalVariables())
- {
- if (second.modifiedGlobalVars.Contains(v))
- {
- BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));
- boundVars.Add(bv);
- map[v] = new IdentifierExpr(Token.NoToken, bv);
- }
- else
- {
- map[v] = new OldExpr(Token.NoToken, Expr.Ident(v));
- }
- oldMap[v] = Expr.Ident(v);
- }
- foreach (Variable v in second.thisOutParams)
- {
- BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));
- boundVars.Add(bv);
- map[v] = new IdentifierExpr(Token.NoToken, bv);
- }
-
- Expr ensuresExpr = Expr.And((new TransitionRelationComputation(program, second)).Compute(), requiresExpr);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap);
- ensuresExpr = Substituter.Apply(subst, oldSubst, ensuresExpr);
- if (boundVars.Count > 0)
- {
- ensuresExpr = new ExistsExpr(Token.NoToken, boundVars, ensuresExpr);
- }
+ TransitionRelationComputation transitionRelationComputation = new TransitionRelationComputation(program, second);
+ transitionRelationComputation.Compute();
+ Expr ensuresExpr = transitionRelationComputation.LeftMoverCompute(failureExpr);
List<Ensures> ensures = new List<Ensures>();
- ensures.Add(new Ensures(false, ensuresExpr));
+ Ensures ensureCheck = new Ensures(false, ensuresExpr);
+ ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);
+ ensures.Add(ensureCheck);
+
List<Block> blocks = new List<Block>();
blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 0fdb01e6..85fce9ff 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -266,7 +266,7 @@ namespace Microsoft.Boogie return linearTypeChecker.availableLinearVars[absyMap[absy]];
}
- private void AddCallToYieldProc(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
+ private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
{
List<Expr> exprSeq = new List<Expr>();
foreach (string domainName in linearTypeChecker.linearDomains.Keys)
@@ -302,12 +302,15 @@ namespace Microsoft.Boogie {
Expr bb = OldEqualityExpr(ogOldGlobalMap);
- // assert pc ==> o_old == o && g_old == g;
- newCmds.Add(new AssertCmd(Token.NoToken, Expr.Imp(Expr.Ident(pc), bb)));
-
// assert (o_old == o && g_old == g) || beta(i, g_old, o, g);
- AssertCmd betaAssertCmd = new AssertCmd(Token.NoToken, Expr.Or(bb, beta));
- newCmds.Add(betaAssertCmd);
+ AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, Expr.Or(bb, beta));
+ skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated";
+ newCmds.Add(skipOrBetaAssertCmd);
+
+ // assert pc ==> o_old == o && g_old == g;
+ AssertCmd skipAssertCmd = new AssertCmd(tok, Expr.Imp(Expr.Ident(pc), bb));
+ skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ;
+ newCmds.Add(skipAssertCmd);
// pc, ok := ite(o_old == o && g_old == g, pc, true), ok || beta(i, g_old, o, g);
List<Expr> iteArgs = new List<Expr>(new Expr[] { bb, Expr.Ident(pc), Expr.True });
@@ -385,7 +388,7 @@ namespace Microsoft.Boogie private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)
{
- AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
+ AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
if (globalMods.Count > 0)
{
@@ -544,9 +547,15 @@ namespace Microsoft.Boogie {
var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldGlobalSubst, ensures.Condition);
if (ensures.Free)
+ {
newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
+ }
else
- newCmds.Add(new AssertCmd(Token.NoToken, newExpr));
+ {
+ AssertCmd assertCmd = new AssertCmd(ensures.tok, newExpr);
+ assertCmd.ErrorData = "Backwards non-interference check failed";
+ newCmds.Add(assertCmd);
+ }
}
newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
yieldCheckerBlock = new Block(Token.NoToken, "L", newCmds, new ReturnCmd(Token.NoToken));
@@ -641,9 +650,15 @@ namespace Microsoft.Boogie PredicateCmd predCmd = (PredicateCmd)cmd;
var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
if (predCmd is AssertCmd)
- newCmds.Add(new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes));
+ {
+ AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes);
+ assertCmd.ErrorData = "Non-interference check failed";
+ newCmds.Add(assertCmd);
+ }
else
+ {
newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
+ }
}
newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));
@@ -832,7 +847,7 @@ namespace Microsoft.Boogie CallCmd callCmd = cmd as CallCmd;
if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
{
- AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
+ AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
}
if (callCmd.IsAsync)
{
@@ -864,8 +879,13 @@ namespace Microsoft.Boogie else if (cmd is ParCallCmd)
{
ParCallCmd parCallCmd = cmd as ParCallCmd;
- AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
+ AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
DesugarParallelCallCmd(newCmds, parCallCmd);
+ if (globalMods.Count > 0 && pc != null)
+ {
+ // assume pc || alpha(i, g);
+ newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Or(Expr.Ident(pc), alpha)));
+ }
HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));
foreach (CallCmd callCmd in parCallCmd.CallCmds)
{
@@ -894,10 +914,12 @@ namespace Microsoft.Boogie }
if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))
{
- AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
+ AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
if (pc != null)
{
- newCmds.Add(new AssertCmd(Token.NoToken, Expr.Ident(ok)));
+ AssertCmd assertCmd = new AssertCmd(b.TransferCmd.tok, Expr.Ident(ok));
+ assertCmd.ErrorData = "Failed to execute atomic action before procedure return";
+ newCmds.Add(assertCmd);
}
}
b.Cmds = newCmds;
@@ -917,7 +939,7 @@ namespace Microsoft.Boogie Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar);
foreach (Block pred in header.Predecessors)
{
- AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
+ AddCallToYieldProc(header.tok, pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
if (pc != null && !graph.BackEdgeNodes(header).Contains(pred))
{
pred.Cmds.Add(new AssignCmd(Token.NoToken, new List<AssignLhs>(
@@ -929,8 +951,13 @@ namespace Microsoft.Boogie List<Cmd> newCmds = new List<Cmd>();
if (pc != null)
{
- newCmds.Add(new AssertCmd(Token.NoToken, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc))));
- newCmds.Add(new AssertCmd(Token.NoToken, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok))));
+ AssertCmd assertCmd;
+ assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc)));
+ assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";
+ newCmds.Add(assertCmd);
+ assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok)));
+ assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";
+ newCmds.Add(assertCmd);
}
foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
@@ -1041,7 +1068,9 @@ namespace Microsoft.Boogie }
else
{
- cmds.Add(new AssertCmd(r.tok, r.Condition, r.Attributes));
+ AssertCmd assertCmd = new AssertCmd(r.tok, r.Condition, r.Attributes);
+ assertCmd.ErrorData = "Non-interference check failed";
+ cmds.Add(assertCmd);
}
}
yields.Add(cmds);
@@ -1080,7 +1109,9 @@ namespace Microsoft.Boogie }
else
{
- cmds.Add(new AssertCmd(e.tok, e.Condition, e.Attributes));
+ AssertCmd assertCmd = new AssertCmd(e.tok, e.Condition, e.Attributes);
+ assertCmd.ErrorData = "Non-interference check failed";
+ cmds.Add(assertCmd);
}
}
yields.Add(cmds);
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 542f0e4b..2e7881f6 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -171,7 +171,7 @@ namespace Microsoft.Boogie {
VariableCollector collector = new VariableCollector();
- this.thisGate.ForEach (assertCmd => collector.Visit(assertCmd));
+ this.thisGate.ForEach(assertCmd => collector.Visit(assertCmd));
this.gateUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
}
}
@@ -223,11 +223,14 @@ namespace Microsoft.Boogie continue;
}
ActionInfo actionInfo = new ActionInfo(proc, codeExpr, moverType, phaseNum);
+ /*
+ * Removing this restriction based on the new failure preservation check
if (actionInfo.IsLeftMover && !actionInfo.isNonBlocking)
{
Error(e, "A left mover must be non blocking");
continue;
}
+ */
procToActionInfo[proc] = actionInfo;
}
}
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index d7c6b5c2..a848ebeb 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -1,9 +1,5 @@ #if QED
-#define DEBUG
-#define OPTIMIZED
-#define NONOPTIMIZED
-
using System;
using System.Collections;
using System.Collections.Generic;
@@ -14,947 +10,328 @@ using Microsoft.Automata; using System.Diagnostics.Contracts;
using Microsoft.Boogie.AbstractInterpretation;
using Microsoft.Boogie.GraphUtil;
+using System.Diagnostics;
namespace Microsoft.Boogie
{
- using Set = GSet<object>;
-
class YieldTypeChecker
{
- /*static subfields of yieldtypesafe(YTS) property language*/
- static CharSetSolver yieldCheckerAutomatonSolver;
-#if OPTIMIZED
- static string yieldReachabilityOptCheckerRegex = @"^1*([D]+([571])*A?([97])*)*$";
- static Automaton<BvSet> yieldReachabilityOptCheckerAutomaton;
- static Automaton<BvSet> minimizedReachabilityOptCheckerAutomaton;
-#endif
-#if !NONOPTIMIZED
- static string yieldReachabilityCheckerRegex = @"^([1234])*([D]+([56781234])*A?([973])*)*$";// regex of property to build automaton of YTS language
- static Automaton<BvSet> yieldReachabilityCheckerAutomaton;
- static Automaton<BvSet> minimizedReachabilityCheckerAutomaton;
-#endif
- static Automaton<BvSet> yieldTypeSafeCheckerAutomaton;
- static Automaton<BvSet> minimizedYieldTypeSafeCheckerAutomaton;
-
+ static CharSetSolver yieldTypeCheckerAutomatonSolver;
+ static Automaton<BvSet> yieldTypeCheckerAutomaton;
static YieldTypeChecker()
{
- yieldCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
-#if !NONOPTIMIZED
- yieldReachabilityCheckerAutomaton =
- Automaton<BvSet>.MkProduct(yieldCheckerAutomatonSolver.Convert(yieldReachabilityCheckerRegex),
- yieldCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$"), // result of product with this Automaton provides us an automaton that has (*) existence alphanum chars in our property automaton
- yieldCheckerAutomatonSolver);
- minimizedReachabilityCheckerAutomaton = yieldReachabilityCheckerAutomaton.Determinize(yieldCheckerAutomatonSolver).Minimize(yieldCheckerAutomatonSolver);
-#endif
-
-#if OPTIMIZED
- yieldReachabilityOptCheckerAutomaton =
- Automaton<BvSet>.MkProduct(yieldCheckerAutomatonSolver.Convert(yieldReachabilityOptCheckerRegex),
- yieldCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$"), // result of product with this Automaton provides us an automaton that has (*) existence alphanum chars in our property automaton
- yieldCheckerAutomatonSolver);
- minimizedReachabilityOptCheckerAutomaton = yieldReachabilityOptCheckerAutomaton.Determinize(yieldCheckerAutomatonSolver).Minimize(yieldCheckerAutomatonSolver);
-
-#endif
- yieldTypeSafeCheckerAutomaton = yieldCheckerAutomatonSolver.ReadFromRanges(
- 0,
- new int[] { 0, 2 },
- new int[][] {
- // self loop on state 0 transitions
- new int[] {0,51,51,0}, // Q
- new int[] {0,68,68,0},// Y
- new int[] {0,49,49,0},
- //0 to 1 transitions
- new int[] {0,65,65,1},//A
- new int[] {0,55,55,1}, //B
- new int[] {0,57,57,1},//L
- new int[] {0,53,53,1}, //R
- //self loop on state 1 transitions
- new int[] {1,65,65,1},//A
- new int[] {1,55,55,1},//B
- new int[] {1,57,57,1},//L
- new int[] {1,53,53,1},//R
- new int[] {1,49,49,1},//P
- new int[] {1,51,51,1},//Q
- //1 to 2 transition
- new int[] {1,68,68,2}, //Y
- //self loop on state 2 transitions
- new int[] {2,65,65,2},//A
- new int[] {2,55,55,2},//B
- new int[] {2,57,57,2},//L
- new int[] {2,53,53,2},//R
- new int[] {2,49,49,2},//P
- new int[] {2,68,68,2},//Y
- new int[] {2,51,51,2},//Q
- });
- minimizedYieldTypeSafeCheckerAutomaton = yieldTypeSafeCheckerAutomaton.Determinize(yieldCheckerAutomatonSolver).Minimize(yieldCheckerAutomatonSolver);
-
-#if !DEBUG
- yieldCheckerAutomatonSolver.ShowGraph(minimizedReachabilityOptCheckerAutomaton, "minimizedReachabilityPropertyAutomaton.dgml");
- yieldCheckerAutomatonSolver.ShowGraph(minimizedYieldTypeSafeCheckerAutomaton, "minimizedTypeSafePropertyAutomaton.dgml");
-#endif
- }
-
- private static Tuple<Automaton<BvSet>, bool> IsYieldReachabilitySafe(Automaton<BvSet> implReachabilityCheckAutomaton, Implementation impl, MoverTypeChecker moverTypeChecker, int phaseNum)
- {
- List<BvSet> witnessSet;
-#if !NONOPTIMIZED
- var isNonEmpty = Automaton<BvSet>.CheckDifference(
- implReachabilityCheckAutomaton,
- yieldReachabilityCheckerAutomaton,
- 0,
- yieldCheckerAutomatonSolver,
- out witnessSet);
- var diffAutomaton = implReachabilityCheckAutomaton.Minus(yieldReachabilityCheckerAutomaton, yieldCheckerAutomatonSolver);
-#endif
-
-#if OPTIMIZED
- var isNonEmpty = Automaton<BvSet>.CheckDifference(
- implReachabilityCheckAutomaton,
- yieldReachabilityOptCheckerAutomaton,
- 0,
- yieldCheckerAutomatonSolver,
- out witnessSet);
-
- var diffAutomaton = implReachabilityCheckAutomaton.Minus(yieldReachabilityOptCheckerAutomaton, yieldCheckerAutomatonSolver);
-#endif
-
- if (isNonEmpty)
- {
- var witness = new String(Array.ConvertAll(witnessSet.ToArray(), bvset => (char)yieldCheckerAutomatonSolver.Choose(bvset)));
- Tuple<Automaton<BvSet>, bool> errTraceExists = new Tuple<Automaton<BvSet>, bool>(diffAutomaton, false);
- return errTraceExists;
- }
- Tuple<Automaton<BvSet>, bool> errTraceNotExist = new Tuple<Automaton<BvSet>, bool>(diffAutomaton, true);
- return errTraceNotExist;
- }
-
- private static Tuple<Automaton<BvSet>, bool> IsYieldTypeSafe(Automaton<BvSet> implTypeSafeCheckAutomaton, Implementation impl, MoverTypeChecker moverTypeChecker, int phaseNum)
+ yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
+ yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.ReadFromRanges(0, new int[] { 0 },
+ new int[][] {
+ new int[] {0, 'P', 'P', 0 },
+ new int[] {0, 'Y', 'Y', 0 },
+ new int[] {0, 'Y', 'Y', 1 },
+ 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[] {2, 'L', 'L', 2 },
+ new int[] {2, 'B', 'B', 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");
+ }
+
+ public void IsYieldTypeSafe(Automaton<BvSet> implAutomaton)
{
List<BvSet> witnessSet;
var isNonEmpty = Automaton<BvSet>.CheckDifference(
- implTypeSafeCheckAutomaton,
- yieldTypeSafeCheckerAutomaton,
+ implAutomaton,
+ yieldTypeCheckerAutomaton,
0,
- yieldCheckerAutomatonSolver,
+ yieldTypeCheckerAutomatonSolver,
out witnessSet);
- var diffAutomaton = implTypeSafeCheckAutomaton.Minus(yieldTypeSafeCheckerAutomaton, yieldCheckerAutomatonSolver);
-
+ var diffAutomaton = implAutomaton.Minus(yieldTypeCheckerAutomaton, yieldTypeCheckerAutomatonSolver);
if (isNonEmpty)
{
- var witness = new String(Array.ConvertAll(witnessSet.ToArray(), bvset => (char)yieldCheckerAutomatonSolver.Choose(bvset)));
- Tuple<Automaton<BvSet>, bool> errTraceExists = new Tuple<Automaton<BvSet>, bool>(diffAutomaton, false);
- return errTraceExists;
+ moverTypeChecker.Error(impl, PrintErrorTrace(diffAutomaton));
}
- Tuple<Automaton<BvSet>, bool> errTraceNotExist = new Tuple<Automaton<BvSet>, bool>(diffAutomaton, true);
- return errTraceNotExist;
}
- private static void/*string*/ PrintErrorTrace(Dictionary<int, Absy> cmds, Automaton<BvSet> errorAutomaton, Implementation yTypeChecked)
+ public string PrintErrorTrace(Automaton<BvSet> errorAutomaton)
{
- // var s = new StringBuilder();
- String s = "";
-
- s += "\nError Trace " + yTypeChecked.Proc.Name + "{" + "\n";
+ String s = "\nBody of " + impl.Proc.Name + " is not yield_type_safe at phase " + currPhaseNum.ToString() + "\n";
foreach (var move in errorAutomaton.GetMoves())
{
- s += " [Line :" + cmds[move.SourceState].Line.ToString() + "] , [Cmd :" + cmds[move.SourceState].ToString() + " ]" + " \n";
+ IToken tok = nodeToAbsy[move.SourceState].tok;
+ s += string.Format("{0}({1}, {2})\n", tok.filename, tok.line, tok.col);
}
- s += "}";
-
- Console.WriteLine(s);
- // return s;
+ return s;
}
+
public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker)
{
- Program yieldTypeCheckedProgram = moverTypeChecker.program;
- YieldTypeChecker regExprToAuto = new YieldTypeChecker();
-
- HashSet<int> phases = moverTypeChecker.allPhaseNums;
- foreach (int yTypeCheckCurrentPhaseNum in phases) // take current phase check num from each interval
+ foreach (int yTypeCheckCurrentPhaseNum in moverTypeChecker.allPhaseNums)
{
- foreach (var decl in yieldTypeCheckedProgram.TopLevelDeclarations)
+ foreach (var decl in moverTypeChecker.program.TopLevelDeclarations)
{
Implementation impl = decl as Implementation;
if (impl == null) continue;
int phaseNumSpecImpl = moverTypeChecker.FindPhaseNumber(impl.Proc);
if (yTypeCheckCurrentPhaseNum > phaseNumSpecImpl) continue;
- Tuple<Tuple<Dictionary<int, Absy>, Automaton<BvSet>>, Tuple<Dictionary<int, Absy>, Automaton<BvSet>>> yieldCheckAutomatons =
- YieldTypeCheckExecutor.YieldTypeCheckAutomaton(impl, phaseNumSpecImpl, yTypeCheckCurrentPhaseNum, moverTypeChecker);
-
- Tuple<Automaton<BvSet>, bool> isYieldReachable = IsYieldReachabilitySafe(yieldCheckAutomatons.Item2.Item2, impl, moverTypeChecker, yTypeCheckCurrentPhaseNum);
- Tuple<Automaton<BvSet>, bool> isYieldTypeSafe = IsYieldTypeSafe(yieldCheckAutomatons.Item1.Item2, impl, moverTypeChecker, yTypeCheckCurrentPhaseNum);
- Automaton<BvSet> isYieldTypeSafeErrorAut = isYieldTypeSafe.Item1;
- Automaton<BvSet> isYieldReachableErrorAut = isYieldReachable.Item1;
-
- Dictionary<int, Absy> isYieldTypeSafeCmds = yieldCheckAutomatons.Item1.Item1;
- Dictionary<int, Absy> isYieldReachableSafeCmds = yieldCheckAutomatons.Item2.Item1;
-
- if (!isYieldReachable.Item2 && !isYieldTypeSafe.Item2)
- {
- moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield_type_safe at phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");
- PrintErrorTrace(isYieldTypeSafeCmds, isYieldTypeSafeErrorAut, impl);
- moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield_reachable_safe at phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");
- PrintErrorTrace(isYieldReachableSafeCmds, isYieldReachableErrorAut, impl);
- }
- else if (isYieldReachable.Item2 && !isYieldTypeSafe.Item2)
- {
- moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield_type_safe at phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");
- PrintErrorTrace(isYieldTypeSafeCmds, isYieldTypeSafeErrorAut, impl);
- }
- else if (!isYieldReachable.Item2 && isYieldTypeSafe.Item2)
- {
- moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield_reachable_safe at phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");
- PrintErrorTrace(isYieldReachableSafeCmds, isYieldReachableErrorAut, impl);
- }
- else if (isYieldReachable.Item2 && isYieldTypeSafe.Item2)
- {
-
- }
+ YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, yTypeCheckCurrentPhaseNum);
}
}
}
- }
- class YieldTypeCheckExecutor
- {
- private static YieldTypeCheckExecutor yieldTypeCheckExecutorInstance;
- static int stateCounter;
-
- protected YieldTypeCheckExecutor()
+ public MoverType FindMoverType(Procedure proc)
{
+ if (!moverTypeChecker.procToActionInfo.ContainsKey(proc))
+ return MoverType.Top;
+ ActionInfo actionInfo = moverTypeChecker.procToActionInfo[proc];
+ if (actionInfo.phaseNum >= currPhaseNum)
+ return MoverType.Top;
+ return actionInfo.moverType;
}
- public static Tuple<Tuple<Dictionary<int, Absy>, Automaton<BvSet>>, Tuple<Dictionary<int, Absy>, Automaton<BvSet>>>
- YieldTypeCheckAutomaton(Implementation yTypeChecked, int specPhaseNumImpl, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)
- {
+ int stateCounter;
+ MoverTypeChecker moverTypeChecker;
+ Implementation impl;
+ int currPhaseNum;
+ Dictionary<Absy, int> absyToNode;
+ Dictionary<int, Absy> nodeToAbsy;
+ HashSet<int> initialStates;
+ HashSet<int> finalStates;
+ Dictionary<Tuple<int, int>, int> edgeLabels;
- if (yieldTypeCheckExecutorInstance == null)
+ public YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum)
+ {
+ this.moverTypeChecker = moverTypeChecker;
+ this.impl = impl;
+ this.currPhaseNum = currPhaseNum;
+ this.stateCounter = 0;
+ this.absyToNode = new Dictionary<Absy, int>();
+ this.initialStates = new HashSet<int>();
+ initialStates.Add(0);
+ this.finalStates = new HashSet<int>();
+ this.edgeLabels = new Dictionary<Tuple<int, int>, int>();
+
+ foreach (Block block in impl.Blocks)
{
- yieldTypeCheckExecutorInstance = new YieldTypeCheckExecutor();
+ foreach (Cmd cmd in block.Cmds)
+ {
+ absyToNode[cmd] = stateCounter;
+ stateCounter++;
+ }
+ absyToNode[block.TransferCmd] = stateCounter;
+ stateCounter++;
+ if (block.TransferCmd is ReturnCmd)
+ {
+ finalStates.Add(absyToNode[block.TransferCmd]);
+ }
}
-
- CharSetSolver solver = new CharSetSolver(BitWidth.BV7);
- Dictionary<Tuple<int, int>, string> edgeLabels = new Dictionary<Tuple<int, int>, string>(); // Tuple<int,int> --> "Y" : State(k) --Y--> State(k+1)
- HashSet<int> finalStates = new HashSet<int>();
- HashSet<int> initialStates = new HashSet<int>();
- stateCounter = 0;
- initialStates.Add(stateCounter); // First state is added to initial states
- Dictionary<Absy, int> abysToNode = yieldTypeCheckExecutorInstance.CreateStateNumbers(yTypeChecked);
- Graph<int> graph = yieldTypeCheckExecutorInstance.BuildAutomatonGraph(yTypeChecked, yTypeCheckCurrentPhaseNum, abysToNode, edgeLabels, finalStates, initialStates, moverTypeChecker); // build component of graph for a phase interval
-
- //Buradayim
- Automaton<BvSet> implYieldTypeSafeCheckAut = yieldTypeCheckExecutorInstance.BuildAutomatonYieldSafe(graph, initialStates, finalStates, edgeLabels, solver);
- Dictionary<int, Absy> nodeToAbysYieldTypeSafe = new Dictionary<int, Absy>();
- foreach (KeyValuePair<Absy, int> state in abysToNode)
+ foreach (Block block in impl.Blocks)
{
- nodeToAbysYieldTypeSafe[state.Value] = state.Key;
+ 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';
+ }
}
- Tuple<Dictionary<int, Absy>, Automaton<BvSet>> implYieldTypeSafeCheckAutomaton = new Tuple<Dictionary<int, Absy>, Automaton<BvSet>>(nodeToAbysYieldTypeSafe, implYieldTypeSafeCheckAut);
-#if !NONOPTIMIZED
- // Update edges w.r.t yield reaching. VocabX{True,False}
- PostProcessGraph(bodyGraphForImplPhaseJ, edgeLabels);
- Automaton<BvSet> implYieldReachCheckAut = BuildAutomatonYieldReachSafe(bodyGraphForImplPhaseJ, edgeLabels, initialStates, finalStates, ytypeChecked, yTypeCheckCurrentPhaseNum); // Last to arguments are just only for showGraph of automaton lib
-#endif
-#if OPTIMIZED
- Automaton<BvSet> implYieldReachCheckAut = yieldTypeCheckExecutorInstance.BuildOptAutomatonYieldReachSafe(yTypeChecked, graph, edgeLabels, initialStates, finalStates, moverTypeChecker, solver);
-#endif
- Dictionary<int, Absy> nodeToAbysYieldReachSafe = new Dictionary<int, Absy>();
- foreach (KeyValuePair<Absy, int> state in abysToNode)
+
+ this.nodeToAbsy = new Dictionary<int, Absy>();
+ foreach (KeyValuePair<Absy, int> state in absyToNode)
{
- nodeToAbysYieldReachSafe[state.Value] = state.Key;
+ this.nodeToAbsy[state.Value] = state.Key;
}
- Tuple<Dictionary<int, Absy>, Automaton<BvSet>> implYieldReachCheckAutomaton = new Tuple<Dictionary<int, Absy>, Automaton<BvSet>>(nodeToAbysYieldReachSafe, implYieldReachCheckAut);
- Tuple<Tuple<Dictionary<int, Absy>, Automaton<BvSet>>, Tuple<Dictionary<int, Absy>, Automaton<BvSet>>> yieldCheckImplAutomaton =
- new Tuple<Tuple<Dictionary<int, Absy>, Automaton<BvSet>>, Tuple<Dictionary<int, Absy>, Automaton<BvSet>>>(implYieldTypeSafeCheckAutomaton, implYieldReachCheckAutomaton);
- return yieldCheckImplAutomaton;
- }
- public Dictionary<Absy, int> CreateStateNumbers(Implementation yTypeChecked)
- {
- Dictionary<Absy, int> abysToNodeNo = new Dictionary<Absy, int>();
- foreach (Block block in yTypeChecked.Blocks)
+ 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)
{
- foreach (Cmd cmd in block.Cmds)
+ 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 (IsAsyncCallCmd(cmd)) continue;
- if (cmd is ParCallCmd)
+ if (!backwardReachableEdges.Contains(edge))
{
- ParCallCmd calle = cmd as ParCallCmd;
- for (int i = 0; i < calle.CallCmds.Count; i++)
- {
- abysToNodeNo[calle.CallCmds[i]] = stateCounter;
- stateCounter++;
- }
+ 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
{
- abysToNodeNo[cmd] = stateCounter;
- stateCounter++;
+ edgeLabels[edge] = -1;
}
}
- abysToNodeNo[block.TransferCmd] = stateCounter;
- stateCounter++;
}
- return abysToNodeNo;
+ Automaton<BvSet> implYieldTypeSafeCheckAut = BuildAutomatonYieldSafe();
+ IsYieldTypeSafe(implYieldTypeSafeCheckAut);
}
- private Graph<int> BuildAutomatonGraph(Implementation yTypeChecked, int yTypeCheckCurrentPhaseNum, Dictionary<Absy, int> abysToNode, Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<int> finalStates, HashSet<int> initialStates, MoverTypeChecker moverTypeChecker)
+ private Graph<int> ComputeGraph()
{
- HashSet<Tuple<int, int>> edges = new HashSet<Tuple<int, int>>();
- foreach (Block block in yTypeChecked.Blocks)
+ foreach (Block block in impl.Blocks)
{
- if (block.Cmds.Count >= 2)
+ for (int i = 0; i < block.Cmds.Count; i++)
{
- for (int i = 0; i < block.Cmds.Count - 1; i++)
+ Cmd cmd = block.Cmds[i];
+ int curr = absyToNode[cmd];
+ int next = (i + 1 == block.Cmds.Count) ? absyToNode[block.TransferCmd] : absyToNode[block.Cmds[i + 1]];
+ Tuple<int, int> edge = new Tuple<int, int>(curr, next);
+ if (cmd is CallCmd)
{
- //IsProper
- if (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))// this is handled in else but keep this branch now
- { // proper state transition
- int source = abysToNode[block.Cmds[i]];
- int dest = abysToNode[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 (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- int source = abysToNode[block.Cmds[i]];
- // create artificial final state
- int dest = Math.Abs(Guid.NewGuid().GetHashCode()); // Generate unique dummy node ref: http://msdn.microsoft.com/en-us/library/system.guid(v=vs.110).aspx
- 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 (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
+ CallCmd callCmd = cmd as CallCmd;
+ if (callCmd.IsAsync)
{
- int source = abysToNode[block.Cmds[i]];
- ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;
- int dest = abysToNode[nextCmd.CallCmds[0]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));
- }
- else if (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- int source = abysToNode[block.Cmds[i]];
- ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;
- int dest = abysToNode[nextCmd.CallCmds[0]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));
- }
- // IsCallCmdsExit
- else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- { // current cmd exit , next cmd will be put as initial state
- initialStates.Add(abysToNode[block.Cmds[i + 1]]);
+ edgeLabels[edge] = 'Q';
}
- else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
+ else
{
- continue;
- }
- else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- // Add state number CallCmd of ParallelCmd
- ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;
- initialStates.Add(abysToNode[nextCmd.CallCmds[0]]);
- }
- else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- // Add state number CallCmd of ParallelCmd
- ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;
- initialStates.Add(abysToNode[nextCmd.CallCmds[0]]);
-
- }
- // ParallelCallCmdYield
- else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;
- ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;
-
- int source = abysToNode[currentCmd.CallCmds[0]];
- int dest = abysToNode[nextCmd.CallCmds[0]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));
-
- }
- else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;
- ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;
-
- int source = abysToNode[currentCmd.CallCmds[0]];
- int dest = abysToNode[nextCmd.CallCmds[0]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));
-
+ switch (FindMoverType(callCmd.Proc))
+ {
+ case MoverType.Atomic:
+ edgeLabels[edge] = 'A';
+ break;
+ case MoverType.Both:
+ edgeLabels[edge] = 'B';
+ break;
+ case MoverType.Left:
+ edgeLabels[edge] = 'L';
+ break;
+ case MoverType.Right:
+ edgeLabels[edge] = 'R';
+ break;
+ case MoverType.Top:
+ finalStates.Add(curr);
+ initialStates.Add(next);
+ break;
+ }
}
- else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
+ }
+ else if (cmd is ParCallCmd)
+ {
+ ParCallCmd parCallCmd = cmd as ParCallCmd;
+ bool isYield = false;
+ bool isRightMover = true;
+ bool isLeftMover = true;
+ foreach (CallCmd callCmd in parCallCmd.CallCmds)
{
- //create dummy state as next state
- ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;
- int source = abysToNode[currentCmd.CallCmds[0]];
- int dest = Math.Abs(Guid.NewGuid().GetHashCode()); // Generate unique dummy node
- finalStates.Add(dest);
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));
-
+ int phaseSpecCallee = moverTypeChecker.FindPhaseNumber(callCmd.Proc);
+ if (phaseSpecCallee >= currPhaseNum)
+ {
+ isYield = true;
+ }
}
- else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
+ if (isYield)
{
- ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;
- int source = abysToNode[currentCmd.CallCmds[0]];
- int dest = abysToNode[block.Cmds[i + 1]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));
+ edgeLabels[edge] = 'Y';
}
- //SeqComposable Parallel Cmd
- else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
+ else
{
- ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;
- ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;
-
- for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)
+ foreach (CallCmd callCmd in parCallCmd.CallCmds)
{
- int source = abysToNode[currentCmd.CallCmds[j]];
- int dest = abysToNode[currentCmd.CallCmds[j + 1]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(block.Cmds[j]));
+ ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+ isRightMover = isRightMover && actionInfo.IsRightMover;
+ isLeftMover = isLeftMover && actionInfo.IsLeftMover;
}
- // Peelout last iteration
- int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];
- int destBtwCalls = abysToNode[nextCmd.CallCmds[0]];
- Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);
- edges.Add(edgeBtw);
- edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));
- }
- else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;
- ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;
-
- for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)
+ if (isLeftMover && isRightMover)
{
- int source = abysToNode[currentCmd.CallCmds[j]];
- int dest = abysToNode[currentCmd.CallCmds[j + 1]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j]));
+ edgeLabels[edge] = 'B';
}
- // Peelout last iteration
- int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];
- int destBtwCalls = abysToNode[nextCmd.CallCmds[0]];
- Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);
- edges.Add(edgeBtw);
- edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));
- }
- else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;
- for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)
+ else if (isLeftMover)
{
- int source = abysToNode[currentCmd.CallCmds[j]];
- int dest = abysToNode[currentCmd.CallCmds[j + 1]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j]));
+ edgeLabels[edge] = 'L';
}
- // Peelout last iteration
- int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];
- int destBtwCalls = Math.Abs(Guid.NewGuid().GetHashCode()); // Generate unique dummy node
- finalStates.Add(destBtwCalls);
- Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);
- edges.Add(edgeBtw);
- edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));
-
- }
- else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;
-
- for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)
+ else if (isRightMover)
{
- int source = abysToNode[currentCmd.CallCmds[j]];
- int dest = abysToNode[currentCmd.CallCmds[j + 1]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j]));
+ edgeLabels[edge] = 'R';
+ }
+ else
+ {
+ Debug.Assert(false);
}
- // Peelout last iteration
- int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];
- int destBtwCalls = abysToNode[block.Cmds[i + 1]]; // Generate unique dummy node
- Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);
- edges.Add(edgeBtw);
- edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));
}
}
- if (IsExitStatement(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- { // put b.TransferCmd into initial states
- initialStates.Add(abysToNode[block.TransferCmd]);
- }
- else if (IsParallelCallCmdYield(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
+ else if (cmd is YieldCmd)
{
- ParCallCmd currentCmd = block.Cmds[block.Cmds.Count - 1] as ParCallCmd;
- int source = abysToNode[currentCmd.CallCmds[0]];
- int dest = abysToNode[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]));
+ edgeLabels[edge] = 'Y';
}
- else if (IsSeqComposableParCallCmd(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
+ else if (cmd is AssumeCmd)
{
- ParCallCmd currentCmd = block.Cmds[block.Cmds.Count - 1] as ParCallCmd;
- for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)
+ if (AccessesGlobals(cmd))
{
- int source = abysToNode[currentCmd.CallCmds[j]];
- int dest = abysToNode[currentCmd.CallCmds[j + 1]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j]));
+ finalStates.Add(curr);
+ initialStates.Add(next);
}
-
- int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];
- int destBtwCalls = abysToNode[block.TransferCmd]; // Generate unique dummy node
- Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);
- edges.Add(edgeBtw);
- edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));
-
- }
- else if (IsProperActionCmd(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- // proper transition to state before transfer command
- int source = abysToNode[block.Cmds[block.Cmds.Count - 1]];
- int dest = abysToNode[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]));
- }
- }
- else if (block.Cmds.Count == 1)
- {
- if (IsExitStatement(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- { // put b.TransferCmd into initial states
- initialStates.Add(abysToNode[block.TransferCmd]);
- }
- else if (IsProperActionCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- { // proper transition to state before transfer command
- int source = abysToNode[block.Cmds[0]];
- int dest = abysToNode[block.TransferCmd];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(block.Cmds[0]));
- }
- else if (IsParallelCallCmdYield(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- ParCallCmd currentCmd = block.Cmds[0] as ParCallCmd;
- int source = abysToNode[currentCmd.CallCmds[0]];
- int dest = abysToNode[block.TransferCmd];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(block.Cmds[0]));
- }
- else if (IsSeqComposableParCallCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- ParCallCmd currentCmd = block.Cmds[0] as ParCallCmd;
- for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)
+ else
{
- int source = abysToNode[currentCmd.CallCmds[j]];
- int dest = abysToNode[currentCmd.CallCmds[j + 1]];
- Tuple<int, int> edge = new Tuple<int, int>(source, dest);
- edges.Add(edge);
- edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j]));
+ edgeLabels[edge] = 'P';
}
-
- int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];
- int destBtwCalls = abysToNode[block.TransferCmd]; // Generate unique dummy node
- Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);
- edges.Add(edgeBtw);
- edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));
-
}
- }
- else if (block.Cmds.Count == 0)
- {// Target block Entry state will be fetched
- }
- // Handle
- HashSet<int> targetBlockEntryStates = GetStateOfTargetBlock(block.TransferCmd, yTypeCheckCurrentPhaseNum, abysToNode, finalStates, moverTypeChecker);
- foreach (int entryState in targetBlockEntryStates)
- {
- int source = abysToNode[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 HashSet<int> GetStateOfTargetBlock(TransferCmd tc, int yTypeCheckCurrentPhaseNum, Dictionary<Absy, int> abysToNode, HashSet<int> finalStates, MoverTypeChecker moverTypeChecker)
- {
- HashSet<int> targetBlockEntryStates = new HashSet<int>();
- if (tc is ReturnCmd)
- {
- ReturnCmd returnCmd = tc as ReturnCmd;
- int source = abysToNode[tc];
- finalStates.Add(source);
- }
- else if (tc is GotoCmd)
- {
- GotoCmd transferCmd = tc as GotoCmd;
- foreach (Block block in transferCmd.labelTargets)
- {
- if (block.Cmds.Count == 0)
+ else if (cmd is AssertCmd)
{
- targetBlockEntryStates.Add(abysToNode[block.TransferCmd]); //Target block is empty. Add state of target block's transfer command (Goto or Return)
+ edgeLabels[edge] = 'Q';
}
- else if (block.Cmds.Count >= 1)
+ else if (cmd is AssignCmd || cmd is HavocCmd)
{
- if (IsExitStatement(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- int targetState = Math.Abs(Guid.NewGuid().GetHashCode());
- finalStates.Add(targetState);
- targetBlockEntryStates.Add(targetState);
- }
- else if (IsProperActionCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- targetBlockEntryStates.Add(abysToNode[block.Cmds[0]]);
- }
- else if (IsParallelCallCmdYield(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))
+ if (AccessesGlobals(cmd))
{
- ParCallCmd targetCmd = block.Cmds[0] as ParCallCmd;
- targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]);
+ finalStates.Add(curr);
+ initialStates.Add(next);
}
- else if (IsSeqComposableParCallCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))
+ else
{
- ParCallCmd targetCmd = block.Cmds[0] as ParCallCmd;
- targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]);
- }
- else if (IsAsyncCallCmd(block.Cmds[0]))
- {
- if (block.Cmds.Count == 1)
- {
- targetBlockEntryStates.Add(abysToNode[block.TransferCmd]);
- }
- else if (block.Cmds.Count > 1)
- {
- int existsNonAsync;
- for (existsNonAsync = 0; existsNonAsync < block.Cmds.Count; existsNonAsync++)
- {
- if (IsAsyncCallCmd(block.Cmds[existsNonAsync])) continue;
- else if (IsParallelCallCmdYield(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- ParCallCmd targetCmd = block.Cmds[existsNonAsync] as ParCallCmd;
- targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]);
- break;
- }
- else if (IsSeqComposableParCallCmd(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- ParCallCmd targetCmd = block.Cmds[existsNonAsync] as ParCallCmd;
- targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]);
- break;
-
- }
- else if (IsExitStatement(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- int targetState = Math.Abs(Guid.NewGuid().GetHashCode());
- finalStates.Add(targetState);
- targetBlockEntryStates.Add(targetState);
- break;
- }
- else if (IsExitStatement(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum, moverTypeChecker))
- {
- targetBlockEntryStates.Add(abysToNode[block.Cmds[existsNonAsync]]);
- break;
- }
- }
- if (existsNonAsync == block.Cmds.Count)
- {
- // put target
- targetBlockEntryStates.Add(abysToNode[block.TransferCmd]); //Target block is empty. Add state of target block's transfer command (Goto or Return)
- }
- }
+ edgeLabels[edge] = 'Q';
}
}
- }
- }
- return targetBlockEntryStates;
- }
-
- private bool IsAccessToNonQedVar(Cmd cmd, MoverTypeChecker moverTypeChecker)
- {
- HashSet<Variable> qedGlobalVariables = moverTypeChecker.QedGlobalVariables();
- Set globalAccesOfCmd = ComputeGlobalAccesses(cmd);
-
- HashSet<Variable> glbAccessOfCmd = new HashSet<Variable>();
- foreach (object var in globalAccesOfCmd)
- {
- Variable v = (Variable)var;
- glbAccessOfCmd.Add(v);
- }
- if (glbAccessOfCmd.IsSubsetOf(qedGlobalVariables))
- {
- return false;
- }
- return true;
- }
-
- //
- private Set FilterGlobalVariables(Set vars)
- {
- Set globals = new Set();
- foreach (object var in vars)
- {
- if (var is GlobalVariable)
- {
- globals.Add((GlobalVariable)var);
- }
- }
- return globals;
- }
-
- private Set ComputeGlobalAccesses(Cmd cmd)
- {
- Set s = ComputeGlobalReads(cmd);
- s.AddRange(ComputeGlobalWrites(cmd));
- return s;
- }
-
- private Set ComputeGlobalReads(Cmd cmd)
- {
- return FilterGlobalVariables(ComputeReads(cmd));
- }
-
- private Set ComputeGlobalWrites(Cmd cmd)
- {
- return FilterGlobalVariables(ComputeWrites(cmd));
- }
-
- private Set ComputeReads(Cmd cmd)
- {
- Set vars = new Set();
-
- if (cmd is AssertCmd)
- { // noop
- // AssertCmd assertCmd = cmd as AssertCmd;
- //assertCmd.Expr.ComputeFreeVariables(vars); // We can ignore assert cmds
- }
- else if (cmd is AssumeCmd)
- {
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- assumeCmd.Expr.ComputeFreeVariables(vars);
- }
- else if (cmd is AssignCmd)
- {
- AssignCmd assignCmd = cmd as AssignCmd;
- foreach (AssignLhs assignLhs in assignCmd.Lhss)
- {
- if (assignLhs is MapAssignLhs)
+ else
{
- MapAssignLhs mapLhs = assignLhs as MapAssignLhs;
- foreach (Expr index in mapLhs.Indexes)
- {
- index.ComputeFreeVariables(vars);
- }
+ edgeLabels[edge] = 'Q';
}
}
- foreach (Expr rhs in assignCmd.Rhss)
- {
- rhs.ComputeFreeVariables(vars);
- }
- }
-
- else if (cmd is HavocCmd)
- {
- // noop
- }
- // Delegated to Shaz's type checker
- /*else if (cmd is CallCmd)
- {
- CallCmd callCmd = cmd as CallCmd;
- foreach (Expr var in callCmd.Ins) {var.ComputeFreeVariables(vars); }
-
- }
- else if(cmd is ParCallCmd){
- ParCallCmd parCallCmd = cmd as ParCallCmd;
-
- foreach (CallCmd parCalle in parCallCmd.CallCmds) {
- foreach (Expr var in parCalle.Ins) {
- // Console.WriteLine("ParCall rd var " + var.ToString());
- var.ComputeFreeVariables(vars);
- }
-
- }
- }*/
- return vars;
- }
- // Discuss and remove
- private Set ComputeWrites(Cmd cmd)
- {
- Set vars = new Set();
- /*
- List<Variable> varseq = new List<Variable>();
- cmd.AddAssignedVariables(varseq);
- foreach (Variable var in varseq)
- {
- vars.Add(var);
- }
- return vars;
- */
- if (cmd is AssertCmd)
- {
- // noop
- }
- else if (cmd is AssumeCmd)
- {
- // noop
- }
- else if (cmd is AssignCmd)
- {
- AssignCmd assignCmd = cmd as AssignCmd;
- foreach (AssignLhs assignLhs in assignCmd.Lhss)
- {
- vars.Add(assignLhs.DeepAssignedVariable);
- }
- }
- else if (cmd is HavocCmd)
- {
- HavocCmd havocCmd = cmd as HavocCmd;
- foreach (Expr var in havocCmd.Vars) { var.ComputeFreeVariables(vars); }
- }
- // Delegated to Shaz's type checker
- /*
- else if (cmd is CallCmd)
- {
- CallCmd callCmd = cmd as CallCmd;
- foreach (Expr var in callCmd.Proc.Modifies) { var.ComputeFreeVariables(vars); }
- foreach (Expr var in callCmd.Outs) { var.ComputeFreeVariables(vars); }
- }
- else if (cmd is ParCallCmd) {
- ParCallCmd parCallCmd = cmd as ParCallCmd;
- foreach (CallCmd parCalle in parCallCmd.CallCmds) {
- foreach (Expr var in parCalle.Proc.Modifies) { var.ComputeFreeVariables(vars); }
- foreach (Expr var in parCalle.Outs) { var.ComputeFreeVariables(vars); }
- }
- }*/
- return vars;
- }
-
- //
- private bool IsProperActionCmd(Cmd cmd, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)
- {
- if (!IsExitStatement(cmd, yTypeCheckCurrentPhaseNum, moverTypeChecker) &&
- !IsParallelCallCmdYield(cmd, yTypeCheckCurrentPhaseNum, moverTypeChecker) &&
- !IsSeqComposableParCallCmd(cmd, yTypeCheckCurrentPhaseNum, moverTypeChecker) &&
- !IsAsyncCallCmd(cmd))
- {
- return true;
- }
- return false;
-
- }
- private bool IsExitStatement(Cmd cmd, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)
- {
- if (IsCallCmdExitPoint(cmd, yTypeCheckCurrentPhaseNum, moverTypeChecker) || IsAccessToNonQedVar(cmd, moverTypeChecker)) { return true; }
- return false;
- }
-
- private bool IsCallCmdExitPoint(Cmd cmd, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)
- {
- if (cmd is CallCmd && !IsAsyncCallCmd(cmd))
- {
- CallCmd callee = cmd as CallCmd;
- int phaseSpecCallee = moverTypeChecker.FindPhaseNumber(callee.Proc);
- if (phaseSpecCallee >= yTypeCheckCurrentPhaseNum)
- {
- return true;
- }
}
- return false;
- }
-
- private bool IsParallelCallCmdYield(Cmd cmd, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)
- {
- if (cmd is ParCallCmd)
+ Graph<int> graph = new Graph<int>(new HashSet<Tuple<int, int>>(edgeLabels.Keys));
+ for (int i = 0; i < stateCounter; i++)
{
- ParCallCmd callee = cmd as ParCallCmd;
- foreach (CallCmd parCallee in callee.CallCmds)
- {
- int phaseSpecCallee = moverTypeChecker.FindPhaseNumber(parCallee.Proc);
- if (phaseSpecCallee >= yTypeCheckCurrentPhaseNum)
- {
- return true;
- }
- }
+ graph.AddSource(i);
}
- return false;
+ return graph;
}
- private bool IsSeqComposableParCallCmd(Cmd cmd, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)
+ private static bool AccessesGlobals(Cmd cmd)
{
- if (cmd is ParCallCmd && !IsParallelCallCmdYield(cmd, yTypeCheckCurrentPhaseNum, moverTypeChecker)) { return true; }
- return false;
+ VariableCollector collector = new VariableCollector();
+ collector.Visit(cmd);
+ return collector.usedVars.Any(x => x is GlobalVariable);
}
- private bool IsAsyncCallCmd(Cmd cmd)
- {
- if (cmd is CallCmd)
- {
- CallCmd calle = cmd as CallCmd;
- if (calle.IsAsync) { return true; }
- }
- return false;
- }
- private string GetEdgeType(Cmd cmd)
- {
- if (cmd is YieldCmd)
- {
- return "Y";
- }
- else if (cmd is HavocCmd)
- {
- return "Q";
- }
- else if (cmd is AssumeCmd)
- {
- 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)
- {
- int pnum;
- MoverType actionType = MoverCheck.GetMoverType(e, out pnum);
- if (actionType == MoverType.Atomic) return "A";
- else if (actionType == MoverType.Both) return "B";
- else if (actionType == MoverType.Left) return "L";
- else if (actionType == MoverType.Right) return "R";
- else if (actionType == MoverType.Top) continue; // Ask this to Shaz
- }
- }
- else if (cmd is ParCallCmd) // A small trick here : While getting type of SeqCompositional_parCall_commands we pass CallCmd typed parameter
- {
- return "Y";
- }
- //else if (cmd is AssignCmd)
- //{ //rest can only be assigncmd
- return "Q";
- //}
- }
- private string PrintGraph(Implementation yTypeChecked, Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels)
+
+ private static string PrintGraph(Implementation yTypeChecked, Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels)
{
var s = new StringBuilder();
s.AppendLine("\nImplementation " + yTypeChecked.Proc.Name + " digraph G {");
@@ -964,494 +341,48 @@ namespace Microsoft.Boogie return s.ToString();
}
-#if !NONOPTIMIZED
- private HashSet<Tuple<int, int>> CollectBackwardEdgesOfYieldEdge(int source)
- {
- HashSet<Tuple<int, int>> yieldReachingEdges = new HashSet<Tuple<int, int>>(); // Collect edges that are backward reachable from source vertex of yield a edge,source ---Y---> sink, in backward direction
- HashSet<int> gray = new HashSet<int>();
- HashSet<int> black = new HashSet<int>();
- HashSet<int> white = new HashSet<int>();
- // Add all vertices except s into
- foreach (int v in graph.Nodes)
- {
- if (!v.Equals(source))
- white.Add(v);
- }
-
- Queue<int> frontier = new Queue<int>(); //
- // n is given as start vertex
- gray.Add(source);
- frontier.Enqueue(source);
-
- while (frontier.Count > 0)
- {
- int u = frontier.Dequeue();
- foreach (int v in graph.Predecessors(u))
- {
-
- if (white.Contains(v) && !gray.Contains(v) && !black.Contains(v))
- {
-
- gray.Add(v);
- frontier.Enqueue(v);
- // Add to yielding edges
- yieldReachingEdges.Add(new Tuple<int, int>(v, u));
- }
-
- }
- black.Add(u);
- }
-
- return yieldReachingEdges;
- }
-
-
- /*
- * Calls CollectBackEdges for each Y edge existing in graph
- */
- private HashSet<Tuple<int, int>> CollectYieldReachingEdgesOfGraph()
- {
- HashSet<Tuple<int, int>> yieldTrueEdges = new HashSet<Tuple<int, int>>(); // Set {forall edges e : e is reaching a Y labeled edge}
- foreach (var e in graph.Edges) // Visits all edges to and do backward yield reachability analysis starting from source vertex of an "Y" labeled edge
- {
- if (edgeLabels[e] == "Y")
- {
- HashSet<Tuple<int, int>> yieldReachingEdges = CollectBackwardEdgesOfYieldEdge(e.Item1);
- foreach (Tuple<int, int> yldrch in yieldReachingEdges)
- {
-
- yieldTrueEdges.Add(yldrch);
- }
- }
- }
- return yieldTrueEdges;
- }
-#endif
- private HashSet<Tuple<int, int>> CollectEdgesReachableFromAction(Graph<int> graph, int source)
+ private static HashSet<Tuple<int, int>> CollectBackwardReachableEdges(Graph<int> graph, HashSet<int> targets)
{
- HashSet<Tuple<int, int>> edgesReachable = new HashSet<Tuple<int, int>>(); // Collect edges that are backward reachable from source vertex of yield a edge,source ---Y---> sink, in backward direction
+ HashSet<Tuple<int, int>> edgesReachable = new HashSet<Tuple<int, int>>();
HashSet<int> gray = new HashSet<int>();
- HashSet<int> black = new HashSet<int>();
- HashSet<int> white = new HashSet<int>();
- // Add all vertices except s into
- foreach (int v in graph.Nodes)
+ Queue<int> frontier = new Queue<int>();
+ foreach (int v in targets)
{
- if (!v.Equals(source))
- white.Add(v);
+ gray.Add(v);
+ frontier.Enqueue(v);
}
- Queue<int> frontier = new Queue<int>(); //
- // n is given as start vertex
- gray.Add(source);
- frontier.Enqueue(source);
-
while (frontier.Count > 0)
{
- int u = frontier.Dequeue();
- foreach (int v in graph.Successors(u))
+ int v = frontier.Dequeue();
+ foreach (int u in graph.Predecessors(v))
{
- if (white.Contains(v) && !gray.Contains(v) && !black.Contains(v))
+ edgesReachable.Add(new Tuple<int, int>(u, v));
+ if (!gray.Contains(u))
{
- gray.Add(v);
- frontier.Enqueue(v);
- // Add to yielding edges
- edgesReachable.Add(new Tuple<int, int>(u, v));
+ gray.Add(u);
+ frontier.Enqueue(u);
}
}
- black.Add(u);
}
return edgesReachable;
}
- private void IsExitOrRetReachableFromAtomicOrLeft(Implementation yTypeChecked, Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<int> finalStates, MoverTypeChecker moverTypeChecker)
- {
- foreach (var e in graph.Edges)
- {
- if (edgeLabels[e] == "A" || edgeLabels[e] == "L")
- {
- HashSet<Tuple<int, int>> edgesReachable = CollectEdgesReachableFromAction(graph, e.Item1);
-
- if (!(ReachesFinalState(finalStates, edgesReachable) || ReachesYieldState(edgeLabels, edgesReachable)))
- {
- moverTypeChecker.Error(yTypeChecked, "Implementation Yield Reachable " + yTypeChecked.Proc.Name);
- }
- }
- }
- }
- private void IsExitOrReachableFromBoth(Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<int> finalStates)
- {
- foreach (var e in graph.Edges)
- {
- if (edgeLabels[e] == "B")
- {
- HashSet<Tuple<int, int>> edgesReachable = CollectEdgesReachableFromAction(graph, e.Item1);
- if (!(ReachesFinalState(finalStates, edgesReachable) || ReachesYieldState(edgeLabels, edgesReachable)))
- {
- edgeLabels[e] = "R";
- }
- }
- }
-
- }
- private void IsExitOrReachableFromLocal(Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<int> finalStates)
- {
- foreach (var e in graph.Edges)
- {
- if (edgeLabels[e] == "Q")
- {
- HashSet<Tuple<int, int>> edgesReachable = CollectEdgesReachableFromAction(graph, e.Item1);
- if (!(ReachesFinalState(finalStates, edgesReachable) || ReachesYieldState(edgeLabels, edgesReachable)))
- {
- edgeLabels[e] = "P";
- }
- edgeLabels[e] = "E";
- }
- }
- }
- private bool ReachesFinalState(HashSet<int> finalStates, HashSet<Tuple<int, int>> edges)
- {
-
- foreach (Tuple<int, int> e in edges)
- {
- if (finalStates.Contains(e.Item1) || finalStates.Contains(e.Item2)) return true;
- }
- return false;
- }
- private bool ReachesYieldState(Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<Tuple<int, int>> edges)
- {
- foreach (var e in edges)
- {
-
- if (edgeLabels[e] == "Y") return true;
- }
- return false;
- }
-
- private Automaton<BvSet> BuildOptAutomatonYieldReachSafe(Implementation yTypeChecked, Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<int> initialStates, HashSet<int> finalStates, MoverTypeChecker moverTypeChecker, CharSetSolver solver)
- {
- IsExitOrRetReachableFromAtomicOrLeft(yTypeChecked, graph, edgeLabels, finalStates, moverTypeChecker); ;
- IsExitOrReachableFromBoth(graph, edgeLabels, finalStates);
- IsExitOrReachableFromLocal(graph, edgeLabels, finalStates);
- return BuildAutomatonYieldSafe(graph, initialStates, finalStates, edgeLabels, solver);
- }
-#if !NONOPTIMIZED
- /*
- * 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()
- {
- HashSet<Tuple<int, int>> yieldTrueEdges = CollectYieldReachingEdgesOfGraph();
-
- foreach (Tuple<int, int> yldrch in yieldTrueEdges)
- {
- if (edgeLabels[yldrch] == "Q")
- {
- edgeLabels[yldrch] = "3";
- }
- else if (edgeLabels[yldrch] == "P")
- {
- edgeLabels[yldrch] = "1";
- }
- else if (edgeLabels[yldrch] == "B")
- {
- edgeLabels[yldrch] = "7";
- }
- else if (edgeLabels[yldrch] == "R")
- {
- edgeLabels[yldrch] = "5";
- }
- else if (edgeLabels[yldrch] == "L")
- {
- edgeLabels[yldrch] = "9";
- }
- else if (edgeLabels[yldrch] == "A")
- {
- edgeLabels[yldrch] = "A";
- }
- else if (edgeLabels[yldrch] == "Y")
- {
- edgeLabels[yldrch] = "D";
- }
- }
- foreach (Tuple<int, int> nyldrch in graph.Edges)
- {
- if (!yieldTrueEdges.Contains(nyldrch))
- {
- if (edgeLabels[nyldrch] == "Q")
- {
- edgeLabels[nyldrch] = "4";
- }
- else if (edgeLabels[nyldrch] == "P")
- {
- edgeLabels[nyldrch] = "2";
- }
- else if (edgeLabels[nyldrch] == "B")
- {
- edgeLabels[nyldrch] = "8";
- }
- else if (edgeLabels[nyldrch] == "R")
- {
- edgeLabels[nyldrch] = "6";
- }
- else if (edgeLabels[nyldrch] == "L")
- {
- edgeLabels[nyldrch] = "C";
- }
- else if (edgeLabels[nyldrch] == "A")
- {
- edgeLabels[nyldrch] = "B";
- }
- else if (edgeLabels[nyldrch] == "Y")
- {
- edgeLabels[nyldrch] = "D";
- }
- }
- }
- }
-#endif
- private int[] ComputeFinalStates(HashSet<int> finalStates)
- {
- return finalStates.ToArray();
- }
- private int[] ComputeInitialStates(HashSet<int> initialStates)
- {
- return initialStates.ToArray();
- }
-
- private Automaton<BvSet> BuildAutomatonYieldSafe(Graph<int> graph, HashSet<int> initialStates, HashSet<int> finalStates, Dictionary<Tuple<int, int>, string> edgeLabels, CharSetSolver solver)
+ private Automaton<BvSet> BuildAutomatonYieldSafe()
{
List<int[]> transitions = new List<int[]>();
- foreach (Tuple<int, int> e in graph.Edges)
- {
- if (edgeLabels[e] == "Q")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 51; // ASCII 3
- transition[2] = 51;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "P")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 49; // ASCII 1
- transition[2] = 49;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "B")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 55; // ASCII 7
- transition[2] = 55;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "R")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 53; // ASCII 5
- transition[2] = 53;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "L")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 57; // ASCII 9
- transition[2] = 57;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "A")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 65; // ASCII A
- transition[2] = 65;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "Y")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 68; // ASCII D
- transition[2] = 68;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- 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);
- }
-
- }
-
- // get final states
- int[] finalSts = ComputeFinalStates(finalStates);
- int dummyInitial = Math.Abs(Guid.NewGuid().GetHashCode());
- foreach (int s in initialStates)
+ foreach (Tuple<int, int> e in edgeLabels.Keys)
{
+ int label = edgeLabels[e];
+ Debug.Assert(label != 'Q');
int[] transition = new int[4];
- transition[0] = dummyInitial;
- transition[1] = -1;
- transition[2] = -1;
- transition[3] = s;
+ transition[0] = e.Item1;
+ transition[1] = label;
+ transition[2] = label;
+ transition[3] = e.Item2;
transitions.Add(transition);
}
- // create Automaton
- Automaton<BvSet> yieldTypeCheckAutomaton = solver.ReadFromRanges(dummyInitial, finalSts, transitions);
- return yieldTypeCheckAutomaton;
- }
-#if !NONOPTIMIZED
- private Automaton<BvSet> BuildAutomatonYieldReachSafe()
- {
- List<int[]> transitions = new List<int[]>();
- foreach (Tuple<int, int> e in graph.Edges)
- {
- if (edgeLabels[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);
- }
- else if (edgeLabels[e] == "1")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 49; // ASCII 1
- transition[2] = 49;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "7")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 55; // ASCII 7
- transition[2] = 55;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "5")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 53; // ASCII 5
- transition[2] = 53;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "9")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 57; // ASCII 9
- transition[2] = 57;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "A")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 65; // ASCII A
- transition[2] = 65;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "D")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 68; // ASCII D
- transition[2] = 68;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "4")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 52; // ASCII 4
- transition[2] = 52;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "2")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 50; // ASCII 2
- transition[2] = 50;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "8")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 56; // ASCII 8
- transition[2] = 56;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- else if (edgeLabels[e] == "6")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 54; // ASCII 6
- transition[2] = 54;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- 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);
- }
- else if (edgeLabels[e] == "B")
- {
- int[] transition = new int[4];
- transition[0] = e.Item1;
- transition[1] = 66; // ASCII B
- transition[2] = 66;
- transition[3] = e.Item2;
- transitions.Add(transition);
- }
- 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);
- }
-
- }
-
- // get final states
- int[] finalSts = ComputeFinalStates();
- int dummyInitial = Math.Abs(Guid.NewGuid().GetHashCode());
+ int dummyInitial = stateCounter;
foreach (int s in initialStates)
{
int[] transition = new int[4];
@@ -1462,24 +393,10 @@ namespace Microsoft.Boogie transitions.Add(transition);
}
- // create Automaton
- Automaton<BvSet> yieldTypeCheckAutomaton = solver.ReadFromRanges(dummyInitial, finalSts, transitions);
+ Automaton<BvSet> yieldTypeCheckAutomaton = yieldTypeCheckerAutomatonSolver.ReadFromRanges(dummyInitial, finalStates.ToArray(), transitions);
return yieldTypeCheckAutomaton;
-
- }
-#endif
- private string PrintEpsilon(BvSet cond, CharSetSolver slvr)
- {
- if (cond == null)
- {
- return "E";
- }
- else return slvr.PrettyPrint(cond);
-
}
}
-
-
}
#endif
\ No newline at end of file |