diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 7 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 2 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 6 | ||||
| -rw-r--r-- | Source/Provers/TPTP/ProverInterface.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/Z3/ProverInterface.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomCheck.cs | 78 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 17 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 113 | ||||
| -rw-r--r-- | Source/VCGeneration/VCDoomed.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 33 |
11 files changed, 153 insertions, 113 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index cffe3b5a..4ec10162 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -516,7 +516,7 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
} else if(CommandLineOptions.Clo.StratifiedInlining > 0) {
- vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
} else {
vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
}
@@ -529,6 +529,7 @@ namespace Microsoft.Boogie { var decls = program.TopLevelDeclarations.ToArray();
foreach (Declaration decl in decls) {
Contract.Assert(decl != null);
+ int prevAssertionCount = vcgen.CumulativeAssertionCount;
Implementation impl = decl as Implementation;
if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {
List<Counterexample/*!*/>/*?*/ errors;
@@ -550,7 +551,7 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.inferLeastForUnsat != null)
{
var svcgen = vcgen as VC.StratifiedVCGen;
- Debug.Assert(svcgen != null);
+ Contract.Assert(svcgen != null);
var ss = new HashSet<string>();
foreach (var tdecl in program.TopLevelDeclarations)
{
@@ -587,7 +588,7 @@ namespace Microsoft.Boogie { TimeSpan elapsed = end - start;
if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {
if (CommandLineOptions.Clo.Trace) {
- timeIndication = string.Format(" [{0} s] ", elapsed.TotalSeconds);
+ timeIndication = string.Format(" [{0} s, {1} proof obligations] ", elapsed.TotalSeconds, vcgen.CumulativeAssertionCount - prevAssertionCount);
}
}
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 7ff0af6c..76eaf661 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -736,6 +736,7 @@ namespace Microsoft.Boogie { return g;
}
throw new IrreducibleLoopException();
+#if USED_CODE
System.Diagnostics.Debug.Assert(g.SplitCandidates.Count > 0);
Block splitCandidate = null;
foreach (Block b in g.SplitCandidates) {
@@ -770,6 +771,7 @@ namespace Microsoft.Boogie { impl.Blocks.Add(copy);
gotoCmd.AddTarget(copy);
}
+#endif
}
}
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index ef24f07a..3fa678a8 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -590,7 +590,8 @@ namespace Microsoft.Dafny var decls = program.TopLevelDeclarations.ToArray();
foreach (var decl in decls )
- {Contract.Assert(decl != null);
+ {
+ Contract.Assert(decl != null);
Implementation impl = decl as Implementation;
if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification)
{
@@ -612,6 +613,7 @@ namespace Microsoft.Dafny }
ConditionGeneration.Outcome outcome;
+ int prevAssertionCount = vcgen.CumulativeAssertionCount;
try
{
outcome = vcgen.VerifyImplementation(impl, program, out errors);
@@ -636,7 +638,7 @@ namespace Microsoft.Dafny {
if (CommandLineOptions.Clo.Trace)
{
- timeIndication = string.Format(" [{0} s] ", elapsed.TotalSeconds);
+ timeIndication = string.Format(" [{0} s, {1} proof obligations] ", elapsed.TotalSeconds, vcgen.CumulativeAssertionCount - prevAssertionCount);
}
}
diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs index 424e36ac..662d45d3 100644 --- a/Source/Provers/TPTP/ProverInterface.cs +++ b/Source/Provers/TPTP/ProverInterface.cs @@ -240,7 +240,7 @@ USE_PREDICATES=<bool> Try to use SMT predicates for functions returning bool if (CommandLineOptions.Clo.Trace) {
DateTime end = DateTime.Now;
TimeSpan elapsed = end - start;
- Console.WriteLine("finished [{0} s] ", elapsed.TotalSeconds);
+ Console.WriteLine("finished [{0} s]", elapsed.TotalSeconds);
}
return res;
}
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs index 388cf91b..45f2d098 100644 --- a/Source/Provers/Z3/ProverInterface.cs +++ b/Source/Provers/Z3/ProverInterface.cs @@ -350,7 +350,7 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P. if (CommandLineOptions.Clo.Trace) {
TimeSpan elapsed = DateTime.Now - start;
- Console.WriteLine("finished [{0} s] ", elapsed.TotalSeconds);
+ Console.WriteLine("finished [{0} s]", elapsed.TotalSeconds);
}
return res;
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index ed698d5f..bdbdd0f2 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -479,6 +479,8 @@ namespace VC { Contract.Invariant(program != null);
}
+ public int CumulativeAssertionCount; // for statistics
+
protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();
protected VariableSeq CurrentLocalVariables = null;
diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs index 9e1b2b1c..8571caee 100644 --- a/Source/VCGeneration/DoomCheck.cs +++ b/Source/VCGeneration/DoomCheck.cs @@ -170,7 +170,7 @@ void ObjectInvariant() }
[NotDelayed]
- public DoomCheck (Implementation passive_impl, Block unifiedExit, Checker check, List<Block> uncheckable) {
+ public DoomCheck (Implementation passive_impl, Block unifiedExit, Checker check, List<Block> uncheckable, out int assertionCount) {
Contract.Requires(passive_impl != null);
Contract.Requires(check != null);
Contract.Requires(uncheckable != null);
@@ -217,7 +217,7 @@ void ObjectInvariant() Label2Absy = new Hashtable(); // This is only a dummy
m_Evc = new Evc(check);
Hashtable l2a = null;
- VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check);
+ VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);
Contract.Assert(vce != null);
Contract.Assert( l2a!=null);
Label2Absy = l2a;
@@ -233,7 +233,8 @@ void ObjectInvariant() Label2Absy = new Hashtable(); // This is only a dummy
m_Evc = new Evc(check);
Hashtable l2a = null;
- VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check);
+ int assertionCount; // compute and then ignore
+ VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);
Contract.Assert(vce != null);
Contract.Assert(l2a != null);
Label2Absy = l2a;
@@ -293,42 +294,41 @@ void ObjectInvariant() CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed;
#endregion
- */
-
- VCExpr GenerateEVC(Implementation impl, out Hashtable label2absy, Checker ch)
- {
+ */
+
+ VCExpr GenerateEVC(Implementation impl, out Hashtable label2absy, Checker ch, out int assertionCount) {
Contract.Requires(impl != null);
Contract.Requires(ch != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- TypecheckingContext tc = new TypecheckingContext(null);
- impl.Typecheck(tc);
- label2absy = new Hashtable/*<int, Absy!>*/();
- VCExpr vc;
- switch (CommandLineOptions.Clo.vcVariety) {
- case CommandLineOptions.VCVariety.Doomed:
-
- vc = LetVC(cce.NonNull(impl.Blocks[0]), label2absy, ch.TheoremProver.Context);
-
- break;
-
- default:
- Contract.Assert(false);throw new cce.UnreachableException(); // unexpected enumeration value
- }
- return vc;
+ TypecheckingContext tc = new TypecheckingContext(null);
+ impl.Typecheck(tc);
+ label2absy = new Hashtable/*<int, Absy!>*/();
+ VCExpr vc;
+ switch (CommandLineOptions.Clo.vcVariety) {
+ case CommandLineOptions.VCVariety.Doomed:
+ vc = LetVC(cce.NonNull(impl.Blocks[0]), label2absy, ch.TheoremProver.Context, out assertionCount);
+ break;
+
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected enumeration value
+ }
+ return vc;
}
public VCExpr LetVC(Block startBlock,
- Hashtable/*<int, Absy!>*/ label2absy,
- ProverContext proverCtxt)
- {Contract.Requires(startBlock != null);
+ Hashtable/*<int, Absy!>*/ label2absy,
+ ProverContext proverCtxt,
+ out int assertionCount)
+ {
+ Contract.Requires(startBlock != null);
Contract.Requires(label2absy != null);
Contract.Requires(proverCtxt != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();
- VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt);
+ VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt, out assertionCount);
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
return proverCtxt.ExprGen.Let(bindings, proverCtxt.ExprGen.Not(startCorrect) );
} else {
@@ -337,17 +337,19 @@ void ObjectInvariant() }
VCExpr LetVC(Block block,
- Hashtable/*<int, Absy!>*/ label2absy,
- Hashtable/*<Block, VCExprVar!>*/ blockVariables,
- List<VCExprLetBinding> bindings,
- ProverContext proverCtxt)
+ Hashtable/*<int, Absy!>*/ label2absy,
+ Hashtable/*<Block, VCExprVar!>*/ blockVariables,
+ List<VCExprLetBinding> bindings,
+ ProverContext proverCtxt,
+ out int assertionCount)
{
- Contract.Requires(label2absy != null);
- Contract.Requires(blockVariables != null);
- Contract.Requires(proverCtxt != null);
- Contract.Requires(cce.NonNullElements(bindings));
+ Contract.Requires(label2absy != null);
+ Contract.Requires(blockVariables != null);
+ Contract.Requires(proverCtxt != null);
+ Contract.Requires(cce.NonNullElements(bindings));
Contract.Ensures(Contract.Result<VCExpr>() != null);
+ assertionCount = 0;
VCExpressionGenerator gen = proverCtxt.ExprGen;
Contract.Assert(gen != null);
VCExprVar v = (VCExprVar)blockVariables[block];
@@ -371,17 +373,19 @@ void ObjectInvariant() List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);
foreach (Block successor in gotocmd.labelTargets) {
Contract.Assert(successor != null);
- VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt);
+ int ac;
+ VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt, out ac);
+ assertionCount += ac;
SuccCorrectVars.Add(s);
}
SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);
}
VCContext context = new VCContext(label2absy, proverCtxt);
- // m_Context = context;
+ // m_Context = context;
VCExpr vc = Wlp.Block(block, SuccCorrect, context);
-
+ assertionCount += context.AssertionCount;
v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);
bindings.Add(gen.LetBinding(v, vc));
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index e1c5ce13..27237a51 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1692,7 +1692,9 @@ namespace VC }
}
if (toExpand.Count == 0) expand = false;
- else DoExpansion(incrementalSearch, toExpand, vState);
+ else {
+ DoExpansion(incrementalSearch, toExpand, vState);
+ }
}
}
#endregion
@@ -2402,14 +2404,13 @@ namespace VC static int newVarCnt = 0;
// Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
- private void DoExpansion(bool incremental, List<int>/*!*/ candidates, VerificationState vState)
- {
- vState.expansionCount += candidates.Count;
+ private void DoExpansion(bool incremental, List<int>/*!*/ candidates, VerificationState vState) {
+ vState.expansionCount += candidates.Count;
- if (incremental)
- DoExpansionAndPush(candidates, vState);
- else
- DoExpansionAndInline(candidates, vState);
+ if (incremental)
+ DoExpansionAndPush(candidates, vState);
+ else
+ DoExpansionAndInline(candidates, vState);
}
// Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 36b9edc2..351591df 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -271,7 +271,9 @@ namespace VC { TypecheckingContext tc = new TypecheckingContext(null);
impl.Typecheck(tc);
- VCExpr vcexpr = gen.Not(LetVC(impl.Blocks[0], info.controlFlowVariable, null, checker.TheoremProver.Context));
+ int assertionCount;
+ VCExpr vcexpr = gen.Not(LetVC(impl.Blocks[0], info.controlFlowVariable, null, checker.TheoremProver.Context, out assertionCount));
+ CumulativeAssertionCount += assertionCount;
Contract.Assert(vcexpr != null);
ResetPredecessors(impl.Blocks);
VCExpr reachvcexpr = GenerateReachVC(impl, info, checker);
@@ -1484,7 +1486,7 @@ namespace VC { }
}
- public void BeginCheck(VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout) {
+ public void BeginCheck(VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout, out int assertionCount) {
Contract.Requires(callback != null);
splitNo = no;
@@ -1508,13 +1510,8 @@ namespace VC { ResetPredecessors(codeExpr.Blocks);
vcgen.AddBlocksBetween(codeExpr.Blocks);
Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));
- VCExpr startCorrect = VCGen.LetVC(
- codeExpr.Blocks[0],
- null,
- label2absy,
- blockVariables,
- bindings,
- ctx);
+ int ac; // computed, but then ignored for this CodeExpr
+ VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);
VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
if (vcgen.CurrentLocalVariables.Length != 0) {
@@ -1536,8 +1533,10 @@ namespace VC { }
));
+ int prev = parent.CumulativeAssertionCount;
VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker);
Contract.Assert(vc != null);
+ assertionCount = parent.CumulativeAssertionCount - prev;
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);
@@ -1630,42 +1629,44 @@ namespace VC { impl.Typecheck(tc);
VCExpr vc;
+ int assertionCount;
switch (CommandLineOptions.Clo.vcVariety) {
case CommandLineOptions.VCVariety.Structured:
- vc = VCViaStructuredProgram(impl, label2absy, ch.TheoremProver.Context);
+ vc = VCViaStructuredProgram(impl, label2absy, ch.TheoremProver.Context, out assertionCount);
break;
case CommandLineOptions.VCVariety.Block:
- vc = FlatBlockVC(impl, label2absy, false, false, false, ch.TheoremProver.Context);
+ vc = FlatBlockVC(impl, label2absy, false, false, false, ch.TheoremProver.Context, out assertionCount);
break;
case CommandLineOptions.VCVariety.BlockReach:
- vc = FlatBlockVC(impl, label2absy, false, true, false, ch.TheoremProver.Context);
+ vc = FlatBlockVC(impl, label2absy, false, true, false, ch.TheoremProver.Context, out assertionCount);
break;
case CommandLineOptions.VCVariety.Local:
- vc = FlatBlockVC(impl, label2absy, true, false, false, ch.TheoremProver.Context);
+ vc = FlatBlockVC(impl, label2absy, true, false, false, ch.TheoremProver.Context, out assertionCount);
break;
case CommandLineOptions.VCVariety.BlockNested:
- vc = NestedBlockVC(impl, label2absy, false, ch.TheoremProver.Context);
+ vc = NestedBlockVC(impl, label2absy, false, ch.TheoremProver.Context, out assertionCount);
break;
case CommandLineOptions.VCVariety.BlockNestedReach:
- vc = NestedBlockVC(impl, label2absy, true, ch.TheoremProver.Context);
+ vc = NestedBlockVC(impl, label2absy, true, ch.TheoremProver.Context, out assertionCount);
break;
case CommandLineOptions.VCVariety.Dag:
if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) {
- vc = DagVC(cce.NonNull(impl.Blocks[0]), label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context);
+ vc = DagVC(cce.NonNull(impl.Blocks[0]), label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);
} else {
- vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, ch.TheoremProver.Context);
+ vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, ch.TheoremProver.Context, out assertionCount);
}
break;
case CommandLineOptions.VCVariety.DagIterative:
- vc = LetVCIterative(impl.Blocks, controlFlowVariable, label2absy, ch.TheoremProver.Context);
+ vc = LetVCIterative(impl.Blocks, controlFlowVariable, label2absy, ch.TheoremProver.Context, out assertionCount);
break;
case CommandLineOptions.VCVariety.Doomed:
- vc = FlatBlockVC(impl, label2absy, false, false, true, ch.TheoremProver.Context);
+ vc = FlatBlockVC(impl, label2absy, false, false, true, ch.TheoremProver.Context, out assertionCount);
break;
default:
Contract.Assert(false);
throw new cce.UnreachableException(); // unexpected enumeration value
}
+ CumulativeAssertionCount += assertionCount;
return vc;
}
@@ -1677,11 +1678,12 @@ namespace VC { }
}
- public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback){
+ public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {
//Contract.Requires(impl != null);
//Contract.Requires(program != null);
//Contract.Requires(callback != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+
if (impl.SkipVerification) {
return Outcome.Inconclusive; // not sure about this one
}
@@ -1756,10 +1758,13 @@ namespace VC { }
callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
+ int assertionCount;
s.BeginCheck(callback, mvInfo, no,
(keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
- CommandLineOptions.Clo.ProverKillTime);
+ CommandLineOptions.Clo.ProverKillTime,
+ out assertionCount);
+ CumulativeAssertionCount += assertionCount;
no++;
@@ -3421,7 +3426,8 @@ namespace VC { static VCExpr LetVC(Block startBlock,
Variable controlFlowVariable,
Hashtable/*<int, Absy!>*/ label2absy,
- ProverContext proverCtxt) {
+ ProverContext proverCtxt,
+ out int assertionCount) {
Contract.Requires(startBlock != null);
Contract.Requires(proverCtxt != null);
@@ -3429,18 +3435,21 @@ namespace VC { Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();
- VCExpr startCorrect = LetVC(startBlock, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt);
+ VCExpr startCorrect = LetVC(startBlock, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt, out assertionCount);
return proverCtxt.ExprGen.Let(bindings, startCorrect);
}
static VCExpr LetVCIterative(List<Block> blocks,
Variable controlFlowVariable,
Hashtable label2absy,
- ProverContext proverCtxt) {
+ ProverContext proverCtxt,
+ out int assertionCount) {
Contract.Requires(blocks != null);
Contract.Requires(proverCtxt != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
+ assertionCount = 0;
+
Graph<Block> dag = new Graph<Block>();
dag.AddSource(blocks[0]);
foreach (Block b in blocks) {
@@ -3491,6 +3500,7 @@ namespace VC { VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);
VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+ assertionCount += context.AssertionCount;
VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);
bindings.Add(gen.LetBinding(v, vc));
@@ -3505,7 +3515,8 @@ namespace VC { Hashtable/*<int, Absy!>*/ label2absy,
Hashtable/*<Block, VCExprVar!>*/ blockVariables,
List<VCExprLetBinding/*!*/>/*!*/ bindings,
- ProverContext proverCtxt)
+ ProverContext proverCtxt,
+ out int assertionCount)
{
Contract.Requires(block != null);
Contract.Requires(blockVariables!= null);
@@ -3514,6 +3525,8 @@ namespace VC { Contract.Ensures(Contract.Result<VCExpr>() != null);
+ assertionCount = 0;
+
VCExpressionGenerator gen = proverCtxt.ExprGen;
Contract.Assert(gen != null);
VCExprVar v = (VCExprVar)blockVariables[block];
@@ -3536,8 +3549,11 @@ namespace VC { } else {
Contract.Assert( gotocmd.labelTargets != null);
List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);
- foreach (Block successor in gotocmd.labelTargets) {Contract.Assert(successor != null);
- VCExpr s = LetVC(successor, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt);
+ foreach (Block successor in gotocmd.labelTargets) {
+ Contract.Assert(successor != null);
+ int ac;
+ VCExpr s = LetVC(successor, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt, out ac);
+ assertionCount += ac;
if (controlFlowVariable != null)
{
VCExprVar controlFlowVariableExpr = proverCtxt.BoogieExprTranslator.LookupVariable(controlFlowVariable);
@@ -3553,6 +3569,7 @@ namespace VC { VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);
VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+ assertionCount += context.AssertionCount;
v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);
bindings.Add(gen.LetBinding(v, vc));
@@ -3564,7 +3581,8 @@ namespace VC { static VCExpr DagVC(Block block,
Hashtable/*<int, Absy!>*/ label2absy,
Hashtable/*<Block, VCExpr!>*/ blockEquations,
- ProverContext proverCtxt)
+ ProverContext proverCtxt,
+ out int assertionCount)
{
Contract.Requires(block != null);
Contract.Requires(label2absy != null);
@@ -3572,6 +3590,7 @@ namespace VC { Contract.Requires(proverCtxt != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
+ assertionCount = 0;
VCExpressionGenerator gen = proverCtxt.ExprGen;
Contract.Assert(gen != null);
VCExpr vc = (VCExpr)blockEquations[block];
@@ -3589,7 +3608,9 @@ namespace VC { {
foreach (Block successor in cce.NonNull(gotocmd.labelTargets)) {
Contract.Assert(successor != null);
- VCExpr c = DagVC(successor, label2absy, blockEquations, proverCtxt);
+ int ac;
+ VCExpr c = DagVC(successor, label2absy, blockEquations, proverCtxt, out ac);
+ assertionCount += ac;
SuccCorrect = SuccCorrect == null ? c : gen.And(SuccCorrect, c);
}
}
@@ -3599,6 +3620,7 @@ namespace VC { VCContext context = new VCContext(label2absy, proverCtxt);
vc = Wlp.Block(block, SuccCorrect, context);
+ assertionCount += context.AssertionCount;
// gen.MarkAsSharedFormula(vc); PR: don't know yet what to do with this guy
@@ -3609,7 +3631,8 @@ namespace VC { static VCExpr FlatBlockVC(Implementation impl,
Hashtable/*<int, Absy!>*/ label2absy,
bool local, bool reach, bool doomed,
- ProverContext proverCtxt)
+ ProverContext proverCtxt,
+ out int assertionCount)
{
Contract.Requires(impl != null);
Contract.Requires(label2absy != null);
@@ -3680,6 +3703,7 @@ namespace VC { programSemantics.Add(binding);
}
+ assertionCount = context.AssertionCount;
return gen.Let(programSemantics, proofObligation);
}
@@ -3743,7 +3767,8 @@ namespace VC { static VCExpr NestedBlockVC(Implementation impl,
Hashtable/*<int, Absy!>*/ label2absy,
bool reach,
- ProverContext proverCtxt){
+ ProverContext proverCtxt,
+ out int assertionCount){
Contract.Requires(impl != null);
Contract.Requires(label2absy != null);
Contract.Requires(proverCtxt != null);
@@ -3766,10 +3791,10 @@ namespace VC { {
List<Block> blocks = impl.Blocks;
- // block sorting is now done on the VCExpr
- // if (((!)CommandLineOptions.Clo.TheProverFactory).NeedsBlockSorting) {
- // blocks = SortBlocks(blocks);
- // }
+ // block sorting is now done on the VCExpr
+ // if (((!)CommandLineOptions.Clo.TheProverFactory).NeedsBlockSorting) {
+ // blocks = SortBlocks(blocks);
+ // }
int i = 0;
foreach (Block b in blocks) {
Contract.Assert(b != null);
@@ -3781,7 +3806,8 @@ namespace VC { VCExprLetBinding programSemantics = NestedBlockEquation(cce.NonNull(impl.Blocks[0]), BlkCorrect, BlkReached, totalOrder, context, g, gen);
List<VCExprLetBinding> ps = new List<VCExprLetBinding>(1);
ps.Add(programSemantics);
-
+
+ assertionCount = context.AssertionCount;
return gen.Let(ps, proofObligation);
}
@@ -3863,12 +3889,13 @@ namespace VC { static VCExpr VCViaStructuredProgram
(Implementation impl, Hashtable/*<int, Absy!>*/ label2absy,
- ProverContext proverCtxt)
+ ProverContext proverCtxt,
+ out int assertionCount)
{
- Contract.Requires(impl != null);
- Contract.Requires(label2absy != null);
- Contract.Requires(proverCtxt != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires(impl != null);
+ Contract.Requires(label2absy != null);
+ Contract.Requires(proverCtxt != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
#region Convert block structure back to a "regular expression"
RE r = DAG2RE.Transform(cce.NonNull(impl.Blocks[0]));
@@ -3878,7 +3905,9 @@ namespace VC { VCContext ctxt = new VCContext(label2absy, proverCtxt);
Contract.Assert(ctxt != null);
#region Send wlp(program,true) to Simplify
- return Wlp.RegExpr(r, VCExpressionGenerator.True, ctxt);
+ var vcexp = Wlp.RegExpr(r, VCExpressionGenerator.True, ctxt);
+ assertionCount = ctxt.AssertionCount;
+ return vcexp;
#endregion
}
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index 734d81d6..4d2e0775 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -121,7 +121,9 @@ namespace VC { Checker checker = FindCheckerFor(impl, 1000);
Contract.Assert(checker != null);
- DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks);
+ int assertionCount;
+ DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount);
+ CumulativeAssertionCount += assertionCount;
//EmitImpl(impl, false);
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index c3134c09..b84df433 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -23,6 +23,7 @@ namespace VC { [Rep] public readonly Hashtable/*<int, Absy!>*/ Label2absy;
[Rep] public readonly ProverContext Ctxt;
public readonly Variable ControlFlowVariable;
+ public int AssertionCount; // counts the number of assertions for which Wlp has been computed
public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt)
{
@@ -85,9 +86,8 @@ namespace VC { /// <summary>
/// Computes the wlp for an assert or assume command "cmd".
/// </summary>
- public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt)
- {
- Contract.Requires(cmd!= null);
+ public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
+ Contract.Requires(cmd != null);
Contract.Requires(N != null);
Contract.Requires(ctxt != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -99,8 +99,7 @@ namespace VC { VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
return gen.Implies(C, N);
- }
- else {
+ } else {
int id = ac.UniqueId;
if (ctxt.Label2absy != null) {
ctxt.Label2absy[id] = ac;
@@ -126,11 +125,11 @@ namespace VC { if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
return gen.Implies(C, N);
+ ctxt.AssertionCount++;
if (ctxt.ControlFlowVariable == null) {
Contract.Assert(ctxt.Label2absy != null);
return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N);
- }
- else {
+ } else {
VCExpr controlFlowVariableExpr = ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable);
Contract.Assert(controlFlowVariableExpr != null);
VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(b.UniqueId)));
@@ -138,8 +137,7 @@ namespace VC { VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(ac.UniqueId)));
if (ctxt.Label2absy == null) {
return gen.AndSimp(gen.Implies(assertFailure, C), gen.Implies(C, N));
- }
- else {
+ } else {
return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), gen.Implies(C, N));
}
}
@@ -148,12 +146,11 @@ namespace VC { } else if (cmd is AssumeCmd) {
AssumeCmd ac = (AssumeCmd)cmd;
- if(CommandLineOptions.Clo.StratifiedInlining > 0) {
- var pname = QKeyValue.FindStringAttribute(ac.Attributes, "candidate");
- if(pname != null)
- {
- return gen.ImpliesSimp(gen.LabelPos("candidate_" + pname.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
- }
+ if (CommandLineOptions.Clo.StratifiedInlining > 0) {
+ var pname = QKeyValue.FindStringAttribute(ac.Attributes, "candidate");
+ if (pname != null) {
+ return gen.ImpliesSimp(gen.LabelPos("candidate_" + pname.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
+ }
// Label the assume if it is a procedure call
NAryExpr naryExpr = ac.Expr as NAryExpr;
@@ -165,12 +162,12 @@ namespace VC { }
}
}
-
+
return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
} else {
- Console.WriteLine(cmd.ToString());
- Contract.Assert(false);throw new cce.UnreachableException(); // unexpected command
+ Console.WriteLine(cmd.ToString());
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command
}
}
|