diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 2 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 2 | ||||
| -rw-r--r-- | Source/GPUVerify/ArrayControlFlowAnalyser.cs | 33 | ||||
| -rw-r--r-- | Source/GPUVerify/BlockPredicator.cs | 25 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 106 | ||||
| -rw-r--r-- | Source/GPUVerify/KernelDualiser.cs | 23 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs | 20 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBeGidAnalyser.cs | 20 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBeGlobalSizeAnalyser.cs | 20 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs | 40 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBePowerOfTwoAnalyser.cs | 16 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs | 20 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenterBase.cs | 101 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 14 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 254 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/VCDoomed.cs | 9 |
17 files changed, 404 insertions, 306 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 0911cbd3..44adce15 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -701,7 +701,7 @@ namespace Microsoft.Boogie { Console.WriteLine();
}
else {
- outcome = vcgen.VerifyImplementation(impl, program, out errors);
+ outcome = vcgen.VerifyImplementation(impl, out errors);
if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null) {
for (int i = 0; i < errors.Count; i++) {
errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 4cf64788..3534dcbf 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -616,7 +616,7 @@ namespace Microsoft.Dafny int prevAssertionCount = vcgen.CumulativeAssertionCount;
try
{
- outcome = vcgen.VerifyImplementation(impl, program, out errors);
+ outcome = vcgen.VerifyImplementation(impl, out errors);
}
catch (VCGenException e)
{
diff --git a/Source/GPUVerify/ArrayControlFlowAnalyser.cs b/Source/GPUVerify/ArrayControlFlowAnalyser.cs index b202dbb3..20036abe 100644 --- a/Source/GPUVerify/ArrayControlFlowAnalyser.cs +++ b/Source/GPUVerify/ArrayControlFlowAnalyser.cs @@ -117,27 +117,28 @@ namespace GPUVerify if (c is AssignCmd)
{
AssignCmd assignCmd = c as AssignCmd;
- Debug.Assert(assignCmd.Lhss.Count == 1);
- Debug.Assert(assignCmd.Rhss.Count == 1);
- if (assignCmd.Lhss[0] is SimpleAssignLhs)
+ for (int i = 0; i != assignCmd.Lhss.Count; i++)
{
- SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[0];
+ if (assignCmd.Lhss[i] is SimpleAssignLhs)
+ {
+ SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
+ Expr rhs = assignCmd.Rhss[i];
- VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();
- visitor.VisitExpr(rhs);
+ VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();
+ visitor.VisitExpr(rhs);
- foreach (Variable v in visitor.GetVariables())
- {
- if (!mayBeDerivedFrom[impl.Name].ContainsKey(v.Name))
- {
- continue;
- }
- foreach (String s in mayBeDerivedFrom[impl.Name][v.Name])
+ foreach (Variable v in visitor.GetVariables())
{
- if (!mayBeDerivedFrom[impl.Name][lhs.AssignedVariable.Name].Contains(s))
+ if (!mayBeDerivedFrom[impl.Name].ContainsKey(v.Name))
{
- SetMayBeDerivedFrom(impl.Name, lhs.AssignedVariable.Name, s);
+ continue;
+ }
+ foreach (String s in mayBeDerivedFrom[impl.Name][v.Name])
+ {
+ if (!mayBeDerivedFrom[impl.Name][lhs.AssignedVariable.Name].Contains(s))
+ {
+ SetMayBeDerivedFrom(impl.Name, lhs.AssignedVariable.Name, s);
+ }
}
}
}
diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs index 15ad2432..80d97ebc 100644 --- a/Source/GPUVerify/BlockPredicator.cs +++ b/Source/GPUVerify/BlockPredicator.cs @@ -1,3 +1,4 @@ +using Graphing; using Microsoft.Boogie; using System; using System.Collections.Generic; @@ -10,6 +11,7 @@ class BlockPredicator { Program prog; Implementation impl; + Graph<Block> blockGraph; Expr returnBlockId; @@ -19,6 +21,7 @@ class BlockPredicator { Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars = new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>(); Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>(); + HashSet<Block> doneBlocks = new HashSet<Block>(); BlockPredicator(Program p, Implementation i) { prog = p; @@ -95,6 +98,23 @@ class BlockPredicator { PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken, targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or))); } + + foreach (Block b in gCmd.labelTargets) { + if (blockGraph.Predecessors(b).Count() == 1) { + if (!doneBlocks.Contains(b)) { + var assumes = b.Cmds.Cast<Cmd>().TakeWhile(c => c is AssumeCmd); + if (assumes.Count() > 0) { + foreach (AssumeCmd aCmd in assumes) { + cmdSeq.Add(new AssumeCmd(Token.NoToken, + Expr.Imp(Expr.Eq(cur, blockIds[b]), + aCmd.Expr))); + } + b.Cmds = + new CmdSeq(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray()); + } + } + } + } } else if (cmd is ReturnCmd) { PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId)); } else { @@ -103,8 +123,8 @@ class BlockPredicator { } void PredicateImplementation() { - var g = prog.ProcessLoops(impl); - var sortedBlocks = g.LoopyTopSort(); + blockGraph = prog.ProcessLoops(impl); + var sortedBlocks = blockGraph.LoopyTopSort(); int blockId = 0; foreach (var block in impl.Blocks) @@ -163,6 +183,7 @@ class BlockPredicator { prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(runBlock)); prevBlock = runBlock; + doneBlocks.Add(runBlock); } } diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 6659566b..27ec052e 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -1374,7 +1374,8 @@ namespace GPUVerify IdentifierExpr P1 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[0].TypedIdent));
IdentifierExpr P2 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[1].TypedIdent));
- checkNonDivergence.simpleCmds.Add(new AssertCmd(tok, Expr.Eq(P1, P2)));
+ if (!CommandLineOptions.Unstructured)
+ checkNonDivergence.simpleCmds.Add(new AssertCmd(tok, Expr.Eq(P1, P2)));
if (!CommandLineOptions.OnlyDivergence)
{
@@ -1520,8 +1521,10 @@ namespace GPUVerify impl.LocVars = NewLocVars;
- impl.StructuredStmts = PerformFullSharedStateAbstraction(impl.StructuredStmts);
-
+ if (CommandLineOptions.Unstructured)
+ impl.Blocks = impl.Blocks.Select(PerformFullSharedStateAbstraction).ToList();
+ else
+ impl.StructuredStmts = PerformFullSharedStateAbstraction(impl.StructuredStmts);
}
@@ -1538,50 +1541,78 @@ namespace GPUVerify return result;
}
- private BigBlock PerformFullSharedStateAbstraction(BigBlock bb)
+ private CmdSeq PerformFullSharedStateAbstraction(CmdSeq cs)
{
- BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
+ var result = new CmdSeq();
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in cs)
{
if (c is AssignCmd)
{
AssignCmd assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1);
- Debug.Assert(assign.Rhss.Count == 1);
- AssignLhs lhs = assign.Lhss[0];
- Expr rhs = assign.Rhss[0];
- ReadCollector rc = new ReadCollector(NonLocalState);
- rc.Visit(rhs);
-
- bool foundAdversarial = false;
- foreach (AccessRecord ar in rc.accesses)
+
+ var lhss = new List<AssignLhs>();
+ var rhss = new List<Expr>();
+
+ for (int i = 0; i != assign.Lhss.Count; i++)
{
- if (ArrayModelledAdversarially(ar.v))
+ AssignLhs lhs = assign.Lhss[i];
+ Expr rhs = assign.Rhss[i];
+ ReadCollector rc = new ReadCollector(NonLocalState);
+ rc.Visit(rhs);
+
+ bool foundAdversarial = false;
+ foreach (AccessRecord ar in rc.accesses)
{
- foundAdversarial = true;
- break;
+ if (ArrayModelledAdversarially(ar.v))
+ {
+ foundAdversarial = true;
+ break;
+ }
}
- }
- if (foundAdversarial)
- {
- Debug.Assert(lhs is SimpleAssignLhs);
- result.simpleCmds.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));
- continue;
+ if (foundAdversarial)
+ {
+ Debug.Assert(lhs is SimpleAssignLhs);
+ result.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));
+ continue;
+ }
+
+ WriteCollector wc = new WriteCollector(NonLocalState);
+ wc.Visit(lhs);
+ if (wc.GetAccess() != null && ArrayModelledAdversarially(wc.GetAccess().v))
+ {
+ continue; // Just remove the write
+ }
+
+ lhss.Add(lhs);
+ rhss.Add(rhs);
}
- WriteCollector wc = new WriteCollector(NonLocalState);
- wc.Visit(lhs);
- if (wc.GetAccess() != null && ArrayModelledAdversarially(wc.GetAccess().v))
+ if (lhss.Count != 0)
{
- continue; // Just remove the write
+ result.Add(new AssignCmd(assign.tok, lhss, rhss));
}
-
+ continue;
}
- result.simpleCmds.Add(c);
+ result.Add(c);
}
+ return result;
+ }
+
+ private Block PerformFullSharedStateAbstraction(Block b)
+ {
+ b.Cmds = PerformFullSharedStateAbstraction(b.Cmds);
+ return b;
+ }
+
+ private BigBlock PerformFullSharedStateAbstraction(BigBlock bb)
+ {
+ BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
+
+ result.simpleCmds = PerformFullSharedStateAbstraction(bb.simpleCmds);
+
if (bb.ec is WhileCmd)
{
WhileCmd WhileCommand = bb.ec as WhileCmd;
@@ -1874,19 +1905,18 @@ namespace GPUVerify {
AssignCmd assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
-
- AssignLhs lhs = assign.Lhss.ElementAt(0);
- Expr rhs = assign.Rhss.ElementAt(0);
-
- if (!NonLocalAccessCollector.ContainsNonLocalAccess(rhs, NonLocalState) ||
- (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, NonLocalState) &&
- NonLocalAccessCollector.IsNonLocalAccess(rhs, NonLocalState)))
+ if (assign.Lhss.Zip(assign.Rhss, (lhs, rhs) =>
+ !NonLocalAccessCollector.ContainsNonLocalAccess(rhs, NonLocalState) ||
+ (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, NonLocalState) &&
+ NonLocalAccessCollector.IsNonLocalAccess(rhs, NonLocalState))).All(b => b))
{
result.simpleCmds.Add(c);
}
else
{
+ Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
+ AssignLhs lhs = assign.Lhss.ElementAt(0);
+ Expr rhs = assign.Rhss.ElementAt(0);
rhs = PullOutNonLocalAccessesIntoTemps(result, rhs, impl);
List<AssignLhs> newLhss = new List<AssignLhs>();
newLhss.Add(lhs);
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index 8d51e74e..49b04251 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -147,23 +147,22 @@ namespace GPUVerify {
AssignCmd assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
-
- if (assign.Lhss[0] is SimpleAssignLhs &&
- verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))
+ if (assign.Lhss.All(lhs =>
+ lhs is SimpleAssignLhs &&
+ verifier.uniformityAnalyser.IsUniform(procName, (lhs as SimpleAssignLhs).AssignedVariable.Name)))
{
cs.Add(assign);
}
else
{
- List<AssignLhs> newLhss = new List<AssignLhs>();
- List<Expr> newRhss = new List<Expr>();
-
- newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
- newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
-
- newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
- newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+ List<AssignLhs> newLhss = assign.Lhss.SelectMany(lhs => new AssignLhs[] {
+ new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(lhs.Clone() as AssignLhs) as AssignLhs,
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(lhs.Clone() as AssignLhs) as AssignLhs
+ }).ToList();
+ List<Expr> newRhss = assign.Rhss.SelectMany(rhs => new Expr[] {
+ new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(rhs.Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(rhs.Clone() as Expr)
+ }).ToList();
AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);
diff --git a/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs b/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs index 88ac000f..3d65ec61 100644 --- a/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs +++ b/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs @@ -186,19 +186,19 @@ namespace GPUVerify private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)
{
- Debug.Assert(assignCmd.Lhss.Count == 1);
- Debug.Assert(assignCmd.Rhss.Count == 1);
- if (assignCmd.Lhss[0] is SimpleAssignLhs)
+ for (int i = 0; i != assignCmd.Lhss.Count; ++i)
{
- SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[0];
-
- if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
- && !MayBe(component, impl.Name, rhs))
+ if (assignCmd.Lhss[i] is SimpleAssignLhs)
{
- SetNot(component, impl.Name, lhs.AssignedVariable.Name);
- }
+ SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
+ Expr rhs = assignCmd.Rhss[i];
+ if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
+ && !MayBe(component, impl.Name, rhs))
+ {
+ SetNot(component, impl.Name, lhs.AssignedVariable.Name);
+ }
+ }
}
}
diff --git a/Source/GPUVerify/MayBeGidAnalyser.cs b/Source/GPUVerify/MayBeGidAnalyser.cs index bb0f8d22..969e8935 100644 --- a/Source/GPUVerify/MayBeGidAnalyser.cs +++ b/Source/GPUVerify/MayBeGidAnalyser.cs @@ -186,19 +186,19 @@ namespace GPUVerify private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)
{
- Debug.Assert(assignCmd.Lhss.Count == 1);
- Debug.Assert(assignCmd.Rhss.Count == 1);
- if (assignCmd.Lhss[0] is SimpleAssignLhs)
+ for (int i = 0; i != assignCmd.Lhss.Count; ++i)
{
- SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[0];
-
- if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
- && !MayBe(component, impl.Name, rhs))
+ if (assignCmd.Lhss[i] is SimpleAssignLhs)
{
- SetNot(component, impl.Name, lhs.AssignedVariable.Name);
- }
+ SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
+ Expr rhs = assignCmd.Rhss[i];
+ if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
+ && !MayBe(component, impl.Name, rhs))
+ {
+ SetNot(component, impl.Name, lhs.AssignedVariable.Name);
+ }
+ }
}
}
diff --git a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs b/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs index cd3c27d6..579f6805 100644 --- a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs +++ b/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs @@ -186,19 +186,19 @@ namespace GPUVerify private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)
{
- Debug.Assert(assignCmd.Lhss.Count == 1);
- Debug.Assert(assignCmd.Rhss.Count == 1);
- if (assignCmd.Lhss[0] is SimpleAssignLhs)
+ for (int i = 0; i != assignCmd.Lhss.Count; ++i)
{
- SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[0];
-
- if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
- && !MayBe(component, impl.Name, rhs))
+ if (assignCmd.Lhss[i] is SimpleAssignLhs)
{
- SetNot(component, impl.Name, lhs.AssignedVariable.Name);
- }
+ SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
+ Expr rhs = assignCmd.Rhss[i];
+ if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
+ && !MayBe(component, impl.Name, rhs))
+ {
+ SetNot(component, impl.Name, lhs.AssignedVariable.Name);
+ }
+ }
}
}
diff --git a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs index 676213e6..a8563dfa 100644 --- a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs +++ b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs @@ -98,38 +98,38 @@ namespace GPUVerify if (c is AssignCmd)
{
AssignCmd assign = c as AssignCmd;
- assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1);
- Debug.Assert(assign.Rhss.Count == 1);
- if (assign.Lhss[0] is SimpleAssignLhs)
+ for (int i = 0; i != assign.Lhss.Count; i++)
{
- Variable lhsV = (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Decl;
-
- if (mayBeAssignedId[impl.Name].ContainsKey(lhsV.Name))
+ if (assign.Lhss[i] is SimpleAssignLhs)
{
+ Variable lhsV = (assign.Lhss[i] as SimpleAssignLhs).AssignedVariable.Decl;
- if (assign.Rhss[0] is IdentifierExpr)
+ if (mayBeAssignedId[impl.Name].ContainsKey(lhsV.Name))
{
- Variable rhsV = (assign.Rhss[0] as IdentifierExpr).Decl;
-
- if (mayBeAnalyser.MayBe(ComponentString(), impl.Name, rhsV.Name))
+ if (assign.Rhss[i] is IdentifierExpr)
{
- mayBeAssignedId[impl.Name][lhsV.Name] = true;
- }
- }
- else
- {
+ Variable rhsV = (assign.Rhss[i] as IdentifierExpr).Decl;
- Expr constantIncrement = GetConstantIncrement(lhsV, assign.Rhss[0]);
+ if (mayBeAnalyser.MayBe(ComponentString(), impl.Name, rhsV.Name))
+ {
+ mayBeAssignedId[impl.Name][lhsV.Name] = true;
+ }
- if (constantIncrement != null)
- {
- incrementedBy[impl.Name][lhsV.Name].Add(constantIncrement);
}
+ else
+ {
+
+ Expr constantIncrement = GetConstantIncrement(lhsV, assign.Rhss[i]);
+ if (constantIncrement != null)
+ {
+ incrementedBy[impl.Name][lhsV.Name].Add(constantIncrement);
+ }
+
+ }
}
}
}
diff --git a/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs b/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs index a00462c8..506add7c 100644 --- a/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs +++ b/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs @@ -85,18 +85,18 @@ namespace GPUVerify if (c is AssignCmd)
{
AssignCmd assign = c as AssignCmd;
- assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1);
- Debug.Assert(assign.Rhss.Count == 1);
- if (assign.Lhss[0] is SimpleAssignLhs)
+ for (int i = 0; i != assign.Lhss.Count; i++)
{
- Variable v = (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Decl;
- if (mayBePowerOfTwoInfo[impl.Name].ContainsKey(v.Name))
+ if (assign.Lhss[i] is SimpleAssignLhs)
{
- if (isPowerOfTwoOperation(v, assign.Rhss[0]))
+ Variable v = (assign.Lhss[i] as SimpleAssignLhs).AssignedVariable.Decl;
+ if (mayBePowerOfTwoInfo[impl.Name].ContainsKey(v.Name))
{
- mayBePowerOfTwoInfo[impl.Name][v.Name] = true;
+ if (isPowerOfTwoOperation(v, assign.Rhss[i]))
+ {
+ mayBePowerOfTwoInfo[impl.Name][v.Name] = true;
+ }
}
}
}
diff --git a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs index bca71171..53efbea8 100644 --- a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs +++ b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs @@ -221,19 +221,19 @@ namespace GPUVerify private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)
{
- Debug.Assert(assignCmd.Lhss.Count == 1);
- Debug.Assert(assignCmd.Rhss.Count == 1);
- if (assignCmd.Lhss[0] is SimpleAssignLhs)
+ for (int i = 0; i != assignCmd.Lhss.Count; ++i)
{
- SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[0];
-
- if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
- && !MayBe(component, impl.Name, rhs))
+ if (assignCmd.Lhss[i] is SimpleAssignLhs)
{
- SetNot(component, impl.Name, lhs.AssignedVariable.Name);
- }
+ SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
+ Expr rhs = assignCmd.Rhss[i];
+ if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
+ && !MayBe(component, impl.Name, rhs))
+ {
+ SetNot(component, impl.Name, lhs.AssignedVariable.Name);
+ }
+ }
}
}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 11feb017..a0c4b5f7 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -800,7 +800,8 @@ namespace GPUVerify private Block AddRaceCheckCalls(Block b)
{
- return new Block(Token.NoToken, b.Label, AddRaceCheckCalls(b.Cmds), b.TransferCmd);
+ b.Cmds = AddRaceCheckCalls(b.Cmds);
+ return b;
}
private void AddRaceCheckCalls(Implementation impl)
@@ -845,79 +846,79 @@ namespace GPUVerify if (c is AssignCmd)
{
AssignCmd assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1);
- Debug.Assert(assign.Rhss.Count == 1);
- AssignLhs lhs = assign.Lhss[0];
- Expr rhs = assign.Rhss[0];
ReadCollector rc = new ReadCollector(NonLocalStateToCheck);
- rc.Visit(rhs);
+ foreach (var rhs in assign.Rhss)
+ rc.Visit(rhs);
if (rc.accesses.Count > 0)
{
- Debug.Assert(rc.accesses.Count == 1);
- AccessRecord ar = rc.accesses[0];
-
- if (shouldAddLogCallAndIncr())
+ foreach (AccessRecord ar in rc.accesses)
{
-
- ExprSeq inParams = new ExprSeq();
- if (ar.IndexZ != null)
+ if (shouldAddLogCallAndIncr())
{
- inParams.Add(ar.IndexZ);
- }
- if (ar.IndexY != null)
- {
- inParams.Add(ar.IndexY);
- }
- if (ar.IndexX != null)
- {
- inParams.Add(ar.IndexX);
- }
- Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_READ_" + ar.v.Name);
+ ExprSeq inParams = new ExprSeq();
+ if (ar.IndexZ != null)
+ {
+ inParams.Add(ar.IndexZ);
+ }
+ if (ar.IndexY != null)
+ {
+ inParams.Add(ar.IndexY);
+ }
+ if (ar.IndexX != null)
+ {
+ inParams.Add(ar.IndexX);
+ }
- CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
+ Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_READ_" + ar.v.Name);
- logAccessCallCmd.Proc = logProcedure;
+ CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
- cs.Add(logAccessCallCmd);
+ logAccessCallCmd.Proc = logProcedure;
+ cs.Add(logAccessCallCmd);
+
+ }
}
}
- WriteCollector wc = new WriteCollector(NonLocalStateToCheck);
- wc.Visit(lhs);
- if (wc.GetAccess() != null)
+ foreach (var lhs in assign.Lhss)
{
- AccessRecord ar = wc.GetAccess();
-
- if (shouldAddLogCallAndIncr())
+ WriteCollector wc = new WriteCollector(NonLocalStateToCheck);
+ wc.Visit(lhs);
+ if (wc.GetAccess() != null)
{
+ AccessRecord ar = wc.GetAccess();
- ExprSeq inParams = new ExprSeq();
- if (ar.IndexZ != null)
- {
- inParams.Add(ar.IndexZ);
- }
- if (ar.IndexY != null)
- {
- inParams.Add(ar.IndexY);
- }
- if (ar.IndexX != null)
+ if (shouldAddLogCallAndIncr())
{
- inParams.Add(ar.IndexX);
- }
- Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);
+ ExprSeq inParams = new ExprSeq();
+ if (ar.IndexZ != null)
+ {
+ inParams.Add(ar.IndexZ);
+ }
+ if (ar.IndexY != null)
+ {
+ inParams.Add(ar.IndexY);
+ }
+ if (ar.IndexX != null)
+ {
+ inParams.Add(ar.IndexX);
+ }
- CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
+ Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);
- logAccessCallCmd.Proc = logProcedure;
+ CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
- cs.Add(logAccessCallCmd);
+ logAccessCallCmd.Proc = logProcedure;
- addedLogWrite = true;
+ cs.Add(logAccessCallCmd);
+ addedLogWrite = true;
+
+ }
}
}
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index dd898c36..ba58a5de 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -447,9 +447,8 @@ namespace VC { }
[ContractClassFor(typeof(ConditionGeneration))]
public abstract class ConditionGenerationContracts : ConditionGeneration {
- public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {
+ public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) {
Contract.Requires(impl != null);
- Contract.Requires(program != null);
Contract.Requires(callback != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
throw new NotImplementedException();
@@ -522,9 +521,8 @@ namespace VC { /// each counterexample consisting of an array of labels.
/// </summary>
/// <param name="impl"></param>
- public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample>/*?*/ errors) {
+ public Outcome VerifyImplementation(Implementation impl, out List<Counterexample>/*?*/ errors) {
Contract.Requires(impl != null);
- Contract.Requires(program != null);
Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));
Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);
@@ -532,7 +530,7 @@ namespace VC { Helpers.ExtraTraceInformation("Starting implementation verification");
CounterexampleCollector collector = new CounterexampleCollector();
- Outcome outcome = VerifyImplementation(impl, program, collector);
+ Outcome outcome = VerifyImplementation(impl, collector);
if (outcome == Outcome.Errors) {
errors = collector.examples;
} else {
@@ -550,7 +548,7 @@ namespace VC { /// each counterexample consisting of an array of labels.
/// </summary>
/// <param name="impl"></param>
- public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample> errors, out List<Model> errorsModel)
+ public Outcome VerifyImplementation(Implementation impl, out List<Counterexample> errors, out List<Model> errorsModel)
{
Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || Contract.ValueAtReturn(out errors) != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
@@ -558,14 +556,14 @@ namespace VC { Outcome outcome;
errorModelList = new List<Model>();
- outcome = VerifyImplementation(impl, program, out errorsOut);
+ outcome = VerifyImplementation(impl, out errorsOut);
errors = errorsOut;
errorsModel = errorModelList;
return outcome;
}
- public abstract Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback);
+ public abstract Outcome VerifyImplementation(Implementation impl, VerifierCallback callback);
/////////////////////////////////// Common Methods and Classes //////////////////////////////////////////
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 65aa8486..563cbf40 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -21,15 +21,13 @@ namespace VC { public int id;
public List<VCExprVar> interfaceExprVars;
public Dictionary<Block, List<StratifiedCallSite>> callSites;
+ public Dictionary<Block, List<StratifiedCallSite>> recordProcCallSites;
public VCExpr vcexpr;
public Dictionary<Block, VCExprVar> reachVars;
public StratifiedVC(StratifiedInliningInfo siInfo) {
info = siInfo;
- if (!info.initialized) {
- info.GenerateVC();
- }
-
+ info.GenerateVC();
vcexpr = info.vcexpr;
var vcgen = info.vcgen;
var prover = vcgen.prover;
@@ -84,6 +82,14 @@ namespace VC { callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));
}
}
+
+ recordProcCallSites = new Dictionary<Block, List<StratifiedCallSite>>();
+ foreach (Block b in info.recordProcCallSites.Keys) {
+ recordProcCallSites[b] = new List<StratifiedCallSite>();
+ foreach (CallSite cs in info.recordProcCallSites[b]) {
+ recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));
+ }
+ }
}
public List<StratifiedCallSite> CallSites {
@@ -150,6 +156,7 @@ namespace VC { public Hashtable/*<int, Absy!>*/ label2absy;
public ModelViewInfo mvInfo;
public Dictionary<Block, List<CallSite>> callSites;
+ public Dictionary<Block, List<CallSite>> recordProcCallSites;
public bool initialized { get; private set; }
public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen) {
@@ -232,9 +239,8 @@ namespace VC { var exprGen = proverInterface.Context.ExprGen;
var translator = proverInterface.Context.BoogieExprTranslator;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : translator.LookupVariable(controlFlowVariable);
-
vcexpr = gen.Not(vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context));
- if (!CommandLineOptions.Clo.UseLabels) {
+ if (controlFlowVariableExpr != null) {
VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));
VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
vcexpr = exprGen.And(eqExpr, vcexpr);
@@ -260,6 +266,7 @@ namespace VC { }
callSites = vcgen.CollectCallSites(impl);
+ recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl);
initialized = true;
}
}
@@ -303,7 +310,8 @@ namespace VC { }
}
- public class StratifiedVCGenBase : VCGen {
+ public abstract class StratifiedVCGenBase : VCGen {
+ public readonly static string recordProcName = "boogie_si_record";
public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
public ProverInterface prover;
@@ -316,6 +324,37 @@ namespace VC { if (impl == null) continue;
implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);
}
+ GenerateRecordFunctions();
+ }
+
+ private void GenerateRecordFunctions() {
+ foreach (var decl in program.TopLevelDeclarations) {
+ var proc = decl as Procedure;
+ if (proc == null) continue;
+ if (!proc.Name.StartsWith(recordProcName)) continue;
+ Contract.Assert(proc.InParams.Length == 1);
+
+ // Make a new function
+ TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);
+ Contract.Assert(ti != null);
+ Formal returnVar = new Formal(Token.NoToken, ti, false);
+ Contract.Assert(returnVar != null);
+
+ // Get record type
+ var argtype = proc.InParams[0].TypedIdent.Type;
+
+ var ins = new VariableSeq();
+ ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));
+
+ var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);
+ prover.Context.DeclareFunction(recordFunc, "");
+
+ var exprs = new ExprSeq();
+ exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));
+
+ Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);
+ proc.Ensures.Add(new Ensures(true, freePostExpr));
+ }
}
public override void Close() {
@@ -345,6 +384,28 @@ namespace VC { return callSites;
}
+ public Dictionary<Block, List<CallSite>> CollectRecordProcedureCallSites(Implementation implementation) {
+ var callSites = new Dictionary<Block, List<CallSite>>();
+ foreach (Block block in implementation.Blocks) {
+ for (int i = 0; i < block.Cmds.Length; i++) {
+ AssumeCmd assumeCmd = block.Cmds[i] as AssumeCmd;
+ if (assumeCmd == null) continue;
+ NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
+ if (naryExpr == null) continue;
+ if (!naryExpr.Fun.FunctionName.StartsWith(recordProcName)) continue;
+ List<VCExpr> interfaceExprs = new List<VCExpr>();
+ foreach (Expr e in naryExpr.Args) {
+ interfaceExprs.Add(prover.Context.BoogieExprTranslator.Translate(e));
+ }
+ CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, block, i);
+ if (!callSites.ContainsKey(block))
+ callSites[block] = new List<CallSite>();
+ callSites[block].Add(cs);
+ }
+ }
+ return callSites;
+ }
+
private int newVarCountForStratifiedInlining = 0;
public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {
string newName = "StratifiedInlining@" + newVarCountForStratifiedInlining.ToString();
@@ -357,29 +418,94 @@ namespace VC { public int CreateNewId() {
return idCountForStratifiedInlining++;
}
+
+ // Used inside PassifyImpl
+ protected override void addExitAssert(string implName, Block exitBlock) {
+ if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName)) {
+ Expr assertExpr = implName2StratifiedInliningInfo[implName].assertExpr;
+ Contract.Assert(assertExpr != null);
+ exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));
+ }
+ }
+
+ public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo) {
+ // Construct the set of inlined procs in the original program
+ var inlinedProcs = new HashSet<string>();
+ foreach (var decl in program.TopLevelDeclarations) {
+ // Implementations
+ if (decl is Implementation) {
+ var impl = decl as Implementation;
+ if (!(impl.Proc is LoopProcedure)) {
+ inlinedProcs.Add(impl.Name);
+ }
+ }
+
+ // And recording procedures
+ if (decl is Procedure) {
+ var proc = decl as Procedure;
+ if (proc.Name.StartsWith(recordProcName)) {
+ Debug.Assert(!(decl is LoopProcedure));
+ inlinedProcs.Add(proc.Name);
+ }
+ }
+ }
+
+ return extractLoopTraceRec(
+ new CalleeCounterexampleInfo(cex, new List<Model.Element>()),
+ mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
+ }
+
+ protected override bool elIsLoop(string procname) {
+ StratifiedInliningInfo info = null;
+ if (implName2StratifiedInliningInfo.ContainsKey(procname)) {
+ info = implName2StratifiedInliningInfo[procname];
+ }
+
+ if (info == null) return false;
+
+ var lp = info.impl.Proc as LoopProcedure;
+
+ if (lp == null) return false;
+ return true;
+ }
+
+ public abstract Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars);
}
public class StratifiedVCGen : StratifiedVCGenBase {
public bool PersistCallTree;
public static Dictionary<string, int> callTree = null;
public int numInlined = 0;
- public readonly static string recordProcName = "boogie_si_record";
private bool useSummary;
private SummaryComputation summaryComputation;
private HashSet<string> procsThatReachedRecBound;
- public int boundUsedInLastQuery { get; private set; }
public HashSet<string> procsToSkip;
public Dictionary<string, int> extraRecBound;
+ public StratifiedVCGen(bool usePrevCallTree, Dictionary<string, int> prevCallTree,
+ HashSet<string> procsToSkip, Dictionary<string, int> extraRecBound,
+ Program program, string/*?*/ logFilePath, bool appendLogFile)
+ : this(program, logFilePath, appendLogFile)
+ {
+ this.procsToSkip = new HashSet<string>(procsToSkip);
+ this.extraRecBound = new Dictionary<string, int>(extraRecBound);
+
+ if (usePrevCallTree) {
+ callTree = prevCallTree;
+ PersistCallTree = true;
+ }
+ else {
+ PersistCallTree = false;
+ }
+ }
+
public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
: base(program, logFilePath, appendLogFile) {
- this.GenerateRecordFunctions();
PersistCallTree = false;
useSummary = false;
procsThatReachedRecBound = new HashSet<string>();
procsToSkip = new HashSet<string>();
extraRecBound = new Dictionary<string, int>();
- boundUsedInLastQuery = -1;
}
// Is this procedure to be "skipped"
@@ -397,36 +523,6 @@ namespace VC { else return extraRecBound[procName];
}
- public void GenerateRecordFunctions() {
- foreach (var decl in program.TopLevelDeclarations) {
- var proc = decl as Procedure;
- if (proc == null) continue;
- if (!proc.Name.StartsWith(recordProcName)) continue;
- Contract.Assert(proc.InParams.Length == 1);
-
- // Make a new function
- TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);
- Contract.Assert(ti != null);
- Formal returnVar = new Formal(Token.NoToken, ti, false);
- Contract.Assert(returnVar != null);
-
- // Get record type
- var argtype = proc.InParams[0].TypedIdent.Type;
-
- var ins = new VariableSeq();
- ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));
-
- var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);
- prover.Context.DeclareFunction(recordFunc, "");
-
- var exprs = new ExprSeq();
- exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));
-
- Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);
- proc.Ensures.Add(new Ensures(true, freePostExpr));
- }
- }
-
public class SummaryComputation {
// The verification state
VerificationState vState;
@@ -1008,7 +1104,7 @@ namespace VC { }
}
- public Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars) {
+ public override Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars) {
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
// Record current time
@@ -1189,7 +1285,7 @@ namespace VC { }
}
- public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {
+ public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {
Debug.Assert(QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"));
Debug.Assert(this.program == program);
@@ -1318,8 +1414,6 @@ namespace VC { // case 2: (bug) We find a bug
// case 3: (internal error) The theorem prover TimesOut of runs OutOfMemory
while (true) {
- boundUsedInLastQuery = bound;
-
// Check timeout
if (CommandLineOptions.Clo.ProverKillTime != -1) {
if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime) {
@@ -1630,9 +1724,7 @@ namespace VC { if (!implName2StratifiedInliningInfo.ContainsKey(procName)) continue;
StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];
- if (!info.initialized) {
- info.GenerateVC();
- }
+ info.GenerateVC();
//Console.WriteLine("Inlining {0}", procName);
VCExpr expansion = cce.NonNull(info.vcexpr);
@@ -1857,9 +1949,21 @@ namespace VC { if (getProc(id) == str && !forcedCandidates.Contains(id)) ret++;
}
- if (extraRecursion.ContainsKey(str)) ret -= extraRecursion[str];
+ // Usual
+ if (!extraRecursion.ContainsKey(str))
+ return ret;
- return ret;
+ // Usual
+ if (ret <= CommandLineOptions.Clo.RecursionBound - 1)
+ return ret;
+
+ // Special
+ if (ret >= CommandLineOptions.Clo.RecursionBound &&
+ ret <= CommandLineOptions.Clo.RecursionBound + extraRecursion[str] - 1)
+ return CommandLineOptions.Clo.RecursionBound - 1;
+
+ // Special
+ return ret - extraRecursion[str];
}
// Set user-define increment/decrement to recursionBound
@@ -2581,56 +2685,6 @@ namespace VC { }
}
- // Used inside PassifyImpl
- protected override void addExitAssert(string implName, Block exitBlock) {
- if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName)) {
- Expr assertExpr = implName2StratifiedInliningInfo[implName].assertExpr;
- Contract.Assert(assertExpr != null);
- exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));
- }
- }
-
- public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo) {
- // Construct the set of inlined procs in the original program
- var inlinedProcs = new HashSet<string>();
- foreach (var decl in program.TopLevelDeclarations) {
- // Implementations
- if (decl is Implementation) {
- var impl = decl as Implementation;
- if (!(impl.Proc is LoopProcedure)) {
- inlinedProcs.Add(impl.Name);
- }
- }
-
- // And recording procedures
- if (decl is Procedure) {
- var proc = decl as Procedure;
- if (proc.Name.StartsWith(recordProcName)) {
- Debug.Assert(!(decl is LoopProcedure));
- inlinedProcs.Add(proc.Name);
- }
- }
- }
-
- return extractLoopTraceRec(
- new CalleeCounterexampleInfo(cex, new List<Model.Element>()),
- mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
- }
-
- protected override bool elIsLoop(string procname) {
- StratifiedInliningInfo info = null;
- if (implName2StratifiedInliningInfo.ContainsKey(procname)) {
- info = implName2StratifiedInliningInfo[procname];
- }
-
- if (info == null) return false;
-
- var lp = info.impl.Proc as LoopProcedure;
-
- if (lp == null) return false;
- return true;
- }
-
} // class StratifiedVCGen
} // namespace VC
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 7e3e3f17..373b685a 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1384,10 +1384,7 @@ namespace VC { }
}
- public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {
- //Contract.Requires(impl != null);
- //Contract.Requires(program != null);
- //Contract.Requires(callback != null);
+ public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
if (impl.SkipVerification) {
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index 4d2e0775..15c6e2aa 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -101,10 +101,7 @@ namespace VC { /// - check if |= (reach=false) => wlp.S.false holds for each reach
///
/// </summary>
- public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {
- //Contract.Requires(impl != null);
- //Contract.Requires(program != null);
- //Contract.Requires(callback != null);
+ public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) {
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
Console.WriteLine();
@@ -115,7 +112,7 @@ namespace VC { //Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name));
- Transform4DoomedCheck(impl, program);
+ Transform4DoomedCheck(impl);
//Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));
@@ -694,7 +691,7 @@ namespace VC { // this might be redundant, but I didn't find a better place to get this information.
private Dictionary<Variable, Expr> m_LastReachVarIncarnation = new Dictionary<Variable, Expr>();
- private void Transform4DoomedCheck(Implementation impl, Program program)
+ private void Transform4DoomedCheck(Implementation impl)
{
variable2SequenceNumber = new Hashtable/*Variable -> int*/();
incarnationOriginMap = new Dictionary<Incarnation, Absy>();
|