From ea8f475d9f26ac46339bbaca436035b1b75c671d Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 9 Jan 2012 17:08:16 -0800 Subject: Boogie: output number of proof obligations (asserts) along with timing information when using the /trace option --- Source/VCGeneration/DoomCheck.cs | 78 +++++++++++++++++++++------------------- 1 file changed, 41 insertions(+), 37 deletions(-) (limited to 'Source/VCGeneration/DoomCheck.cs') 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 uncheckable) { + public DoomCheck (Implementation passive_impl, Block unifiedExit, Checker check, List 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() != null); - TypecheckingContext tc = new TypecheckingContext(null); - impl.Typecheck(tc); - label2absy = new Hashtable/**/(); - 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/**/(); + 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/**/ label2absy, - ProverContext proverCtxt) - {Contract.Requires(startBlock != null); + Hashtable/**/ label2absy, + ProverContext proverCtxt, + out int assertionCount) + { + Contract.Requires(startBlock != null); Contract.Requires(label2absy != null); Contract.Requires(proverCtxt != null); Contract.Ensures(Contract.Result() != null); Hashtable/**/ blockVariables = new Hashtable/**/(); List bindings = new List(); - 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/**/ label2absy, - Hashtable/**/ blockVariables, - List bindings, - ProverContext proverCtxt) + Hashtable/**/ label2absy, + Hashtable/**/ blockVariables, + List 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() != null); + assertionCount = 0; VCExpressionGenerator gen = proverCtxt.ExprGen; Contract.Assert(gen != null); VCExprVar v = (VCExprVar)blockVariables[block]; @@ -371,17 +373,19 @@ void ObjectInvariant() List SuccCorrectVars = new List(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)); -- cgit v1.2.3