From 3bdf2f0e5ae28a38bda913df4b73085415f2a0e4 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 29 Feb 2012 21:36:03 -0800 Subject: Dafny: fixed well-formedness checking of LET expressions to allow the RHS to be used --- Source/Dafny/Translator.cs | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index c0a56d05..40d7c266 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2406,10 +2406,21 @@ namespace Microsoft.Dafny { } else if (expr is LetExpr) { var e = (LetExpr)expr; - foreach (var rhs in e.RHSs) { - CheckWellformed(rhs, options, locals, builder, etran); + + var substMap = new Dictionary(); + Contract.Assert(e.Vars.Count == e.RHSs.Count); // checked by resolution + for (int i = 0; i < e.Vars.Count; i++) { + var vr = e.Vars[i]; + var tp = TrType(vr.Type); + var v = new Bpl.LocalVariable(vr.tok, new Bpl.TypedIdent(vr.tok, vr.UniqueName, tp)); + locals.Add(v); + var lhs = new Bpl.IdentifierExpr(vr.tok, vr.UniqueName, tp); + + CheckWellformedWithResult(e.RHSs[i], options, lhs, vr.Type, locals, builder, etran); + substMap.Add(vr, new BoogieWrapper(lhs, vr.Type)); } - CheckWellformedWithResult(etran.GetSubstitutedBody(e), options, result, resultType, locals, builder, etran); + CheckWellformedWithResult(Substitute(e.Body, null, substMap), options, result, resultType, locals, builder, etran); + result = null; } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; -- cgit v1.2.3 From 5ec8bc0ea0f8a0e5a4b993c86c18d7b01e413f4e Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 1 Mar 2012 19:53:31 +0000 Subject: Support for access annotations. --- Source/GPUVerify/AccessInvariantProcessor.cs | 94 ++++++++++ Source/GPUVerify/AsymmetricExpressionFinder.cs | 29 ++++ Source/GPUVerify/CrossThreadInvariantProcessor.cs | 4 +- Source/GPUVerify/GPUVerifier.cs | 202 ++++++++++++++++++++-- Source/GPUVerify/GPUVerify.csproj | 2 + Source/GPUVerify/Predicator.cs | 2 +- 6 files changed, 314 insertions(+), 19 deletions(-) create mode 100644 Source/GPUVerify/AccessInvariantProcessor.cs create mode 100644 Source/GPUVerify/AsymmetricExpressionFinder.cs (limited to 'Source') diff --git a/Source/GPUVerify/AccessInvariantProcessor.cs b/Source/GPUVerify/AccessInvariantProcessor.cs new file mode 100644 index 00000000..fbbfda79 --- /dev/null +++ b/Source/GPUVerify/AccessInvariantProcessor.cs @@ -0,0 +1,94 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using Microsoft.Boogie; + +namespace GPUVerify +{ + class AccessInvariantProcessor : StandardVisitor + { + + private const string NO_READ = "__no_read_"; + private const string NO_WRITE = "__no_write_"; + private const string READ_OFFSET = "__read_offset_"; + private const string WRITE_OFFSET = "__write_offset_"; + private const string READ_IMPLIES = "__read_implies_"; + private const string WRITE_IMPLIES = "__write_implies_"; + + public override Expr VisitNAryExpr(NAryExpr node) + { + + if (node.Fun is FunctionCall) + { + FunctionCall call = node.Fun as FunctionCall; + + if (MatchesIntrinsic(call.Func, NO_READ)) + { + return Expr.Not( + MakeReadHasOccurred(node, call) + ); + } + + if (MatchesIntrinsic(call.Func, NO_WRITE)) + { + return Expr.Not( + MakeWriteHasOccurred(node, call) + ); + } + + if (MatchesIntrinsic(call.Func, READ_OFFSET)) + { + return new IdentifierExpr(node.tok, new GlobalVariable( + node.tok, new TypedIdent(node.tok, "_READ_OFFSET_X_" + + call.Func.Name.Substring(READ_OFFSET.Length), Microsoft.Boogie.Type.GetBvType(32))) + ); + } + + if (MatchesIntrinsic(call.Func, WRITE_OFFSET)) + { + return new IdentifierExpr(node.tok, new GlobalVariable( + node.tok, new TypedIdent(node.tok, "_WRITE_OFFSET_X_" + + call.Func.Name.Substring(WRITE_OFFSET.Length), Microsoft.Boogie.Type.GetBvType(32))) + ); + } + + if (MatchesIntrinsic(call.Func, READ_IMPLIES)) + { + return Expr.Imp(MakeReadHasOccurred(node, call), node.Args[0]); + } + + if (MatchesIntrinsic(call.Func, WRITE_IMPLIES)) + { + return Expr.Imp(MakeWriteHasOccurred(node, call), node.Args[0]); + } + + } + + return base.VisitNAryExpr(node); + } + + private static IdentifierExpr MakeReadHasOccurred(NAryExpr node, FunctionCall call) + { + return new IdentifierExpr(node.tok, new GlobalVariable( + node.tok, new TypedIdent(node.tok, "_READ_HAS_OCCURRED_" + + call.Func.Name.Substring(NO_READ.Length), Microsoft.Boogie.Type.Bool))); + } + + private static IdentifierExpr MakeWriteHasOccurred(NAryExpr node, FunctionCall call) + { + return new IdentifierExpr(node.tok, new GlobalVariable( + node.tok, new TypedIdent(node.tok, "_WRITE_HAS_OCCURRED_" + + call.Func.Name.Substring(NO_WRITE.Length), Microsoft.Boogie.Type.Bool))); + } + + + private bool MatchesIntrinsic(Function function, string intrinsicPrefix) + { + return function.Name.Length > intrinsicPrefix.Length && + function.Name.Substring(0, intrinsicPrefix.Length).Equals(intrinsicPrefix); + } + + + } +} diff --git a/Source/GPUVerify/AsymmetricExpressionFinder.cs b/Source/GPUVerify/AsymmetricExpressionFinder.cs new file mode 100644 index 00000000..40c7eb32 --- /dev/null +++ b/Source/GPUVerify/AsymmetricExpressionFinder.cs @@ -0,0 +1,29 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using Microsoft.Boogie; + +namespace GPUVerify +{ + class AsymmetricExpressionFinder : StandardVisitor + { + private bool found = false; + + internal bool foundAsymmetricExpr() + { + return found; + } + + public override Variable VisitVariable(Variable node) + { + if (node.TypedIdent.Name.Contains("_READ_HAS_OCCURRED") || + node.TypedIdent.Name.Contains("_READ_OFFSET")) + { + found = true; + } + return node; + } + + } +} diff --git a/Source/GPUVerify/CrossThreadInvariantProcessor.cs b/Source/GPUVerify/CrossThreadInvariantProcessor.cs index b5772c0c..16416e11 100644 --- a/Source/GPUVerify/CrossThreadInvariantProcessor.cs +++ b/Source/GPUVerify/CrossThreadInvariantProcessor.cs @@ -19,10 +19,8 @@ namespace GPUVerify if (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool")) { - return Expr.True; -/* Debug.Assert(false); return Expr.Eq(new VariableDualiser(1).VisitExpr(node.Args[0].Clone() as Expr), - new VariableDualiser(2).VisitExpr(node.Args[0].Clone() as Expr));*/ + new VariableDualiser(2).VisitExpr(node.Args[0].Clone() as Expr)); } if (call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool")) diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 7432c823..632777c9 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -310,6 +310,8 @@ namespace GPUVerify return; } + ProcessAccessInvariants(); + if (CommandLineOptions.ShowStages) { emitProgram(outputFilename + "_instrumented"); @@ -406,35 +408,146 @@ namespace GPUVerify } - private void ProcessCrossThreadInvariants() + private void ProcessAccessInvariants() { foreach (Declaration d in Program.TopLevelDeclarations) { if (d is Procedure) { - // TODO: requires and ensures + Procedure p = d as Procedure; + p.Requires = ProcessAccessInvariants(p.Requires); + p.Ensures = ProcessAccessInvariants(p.Ensures); } + if (d is Implementation) { Implementation i = d as Implementation; - List newBlocks = new List(); - foreach (Block b in i.Blocks) - { - Console.WriteLine("Before"); - Console.WriteLine(b.Cmds); - Block newBlock = new CrossThreadInvariantProcessor().VisitBlock(b); - Console.WriteLine("After"); - Console.WriteLine(newBlock.Cmds); + ProcessAccessInvariants(i.StructuredStmts); + } + } + } + private void ProcessAccessInvariants(StmtList stmtList) + { + + foreach (BigBlock bb in stmtList.BigBlocks) + { + ProcessAccessInvariants(bb); + } + } - newBlocks.Add(newBlock); - } - i.Blocks = newBlocks; + private void ProcessAccessInvariants(BigBlock bb) + { + if (bb.ec is WhileCmd) + { + WhileCmd whileCmd = bb.ec as WhileCmd; + whileCmd.Invariants = ProcessAccessInvariants(whileCmd.Invariants); + ProcessAccessInvariants(whileCmd.Body); + } + else if (bb.ec is IfCmd) + { + ProcessAccessInvariants((bb.ec as IfCmd).thn); + if ((bb.ec as IfCmd).elseBlock != null) + { + ProcessAccessInvariants((bb.ec as IfCmd).elseBlock); + } + } + } + + private List ProcessAccessInvariants(List invariants) + { + List result = new List(); + + foreach (PredicateCmd p in invariants) + { + result.Add(new AssertCmd(p.tok, new AccessInvariantProcessor().VisitExpr(p.Expr.Clone() as Expr))); + } + + return result; + } + + private EnsuresSeq ProcessAccessInvariants(EnsuresSeq ensuresSeq) + { + EnsuresSeq result = new EnsuresSeq(); + foreach (Ensures e in ensuresSeq) + { + result.Add(new Ensures(e.Free, new AccessInvariantProcessor().VisitExpr(e.Condition.Clone() as Expr))); + } + return result; + } + + private RequiresSeq ProcessAccessInvariants(RequiresSeq requiresSeq) + { + RequiresSeq result = new RequiresSeq(); + foreach (Requires r in requiresSeq) + { + result.Add(new Requires(r.Free, new AccessInvariantProcessor().VisitExpr(r.Condition.Clone() as Expr))); + } + return result; + } + + private void ProcessCrossThreadInvariants() + { + foreach (Declaration d in Program.TopLevelDeclarations) + { + if (d is Procedure) + { + Procedure p = d as Procedure; + p.Requires = ProcessCrossThreadInvariants(p.Requires); + p.Ensures = ProcessCrossThreadInvariants(p.Ensures); + } + if (d is Implementation) + { + Implementation i = d as Implementation; + ProcessCrossThreadInvariants(i.StructuredStmts); } } } + private EnsuresSeq ProcessCrossThreadInvariants(EnsuresSeq ensuresSeq) + { + EnsuresSeq result = new EnsuresSeq(); + foreach (Ensures e in ensuresSeq) + { + result.Add(new Ensures(e.Free, new CrossThreadInvariantProcessor().VisitExpr(e.Condition.Clone() as Expr))); + } + return result; + } + + private RequiresSeq ProcessCrossThreadInvariants(RequiresSeq requiresSeq) + { + RequiresSeq result = new RequiresSeq(); + foreach (Requires r in requiresSeq) + { + result.Add(new Requires(r.Free, new CrossThreadInvariantProcessor().VisitExpr(r.Condition.Clone() as Expr))); + } + return result; + } + + private void ProcessCrossThreadInvariants(StmtList stmtList) + { + foreach (BigBlock bb in stmtList.BigBlocks) + { + ProcessCrossThreadInvariants(bb); + } + } + + private void ProcessCrossThreadInvariants(BigBlock bb) + { + if (bb.ec is WhileCmd) + { + WhileCmd whileCmd = bb.ec as WhileCmd; + List newInvariants = new List(); + foreach(PredicateCmd p in whileCmd.Invariants) + { + newInvariants.Add(new AssertCmd(p.tok, new CrossThreadInvariantProcessor().VisitExpr(p.Expr))); + } + whileCmd.Invariants = newInvariants; + ProcessCrossThreadInvariants(whileCmd.Body); + } + } + private void emitProgram(string filename) { using (TokenTextWriter writer = new TokenTextWriter(filename + ".bpl")) @@ -1924,6 +2037,9 @@ namespace GPUVerify bool HalfDualise = HalfDualisedProcedureNames.Contains(proc.Name); + proc.Requires = DualiseRequires(proc.Requires); + proc.Ensures = DualiseEnsures(proc.Ensures); + proc.InParams = DualiseVariableSequence(proc.InParams, HalfDualise); proc.OutParams = DualiseVariableSequence(proc.OutParams, HalfDualise); IdentifierExprSeq NewModifies = new IdentifierExprSeq(); @@ -1988,6 +2104,42 @@ namespace GPUVerify } + private EnsuresSeq DualiseEnsures(EnsuresSeq ensuresSeq) + { + EnsuresSeq newEnsures = new EnsuresSeq(); + foreach (Ensures e in ensuresSeq) + { + newEnsures.Add(new Ensures(e.Free, new VariableDualiser(1).VisitExpr(e.Condition.Clone() as Expr))); + if (!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(e.Condition)) + { + newEnsures.Add(new Ensures(e.Free, new VariableDualiser(2).VisitExpr(e.Condition.Clone() as Expr))); + } + } + return newEnsures; + } + + private RequiresSeq DualiseRequires(RequiresSeq requiresSeq) + { + RequiresSeq newRequires = new RequiresSeq(); + foreach (Requires r in requiresSeq) + { + newRequires.Add(new Requires(r.Free, new VariableDualiser(1).VisitExpr(r.Condition.Clone() as Expr))); + + if (!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(r.Condition)) + { + newRequires.Add(new Requires(r.Free, new VariableDualiser(2).VisitExpr(r.Condition.Clone() as Expr))); + } + } + return newRequires; + } + + private bool ContainsAsymmetricExpression(Expr expr) + { + AsymmetricExpressionFinder finder = new AsymmetricExpressionFinder(); + finder.VisitExpr(expr); + return finder.foundAsymmetricExpr(); + } + private static VariableSeq DualiseVariableSequence(VariableSeq seq, bool HalfDualise) { VariableSeq result = new VariableSeq(); @@ -2017,12 +2169,29 @@ namespace GPUVerify // Add predicate to start of parameter list Procedure proc = d as Procedure; VariableSeq NewIns = new VariableSeq(); - NewIns.Add(new LocalVariable(proc.tok, new TypedIdent(proc.tok, "_P", Microsoft.Boogie.Type.Bool))); + TypedIdent enabled = new TypedIdent(proc.tok, "_P", Microsoft.Boogie.Type.Bool); + NewIns.Add(new LocalVariable(proc.tok, enabled)); foreach (Variable v in proc.InParams) { NewIns.Add(v); } proc.InParams = NewIns; + + RequiresSeq newRequires = new RequiresSeq(); + foreach (Requires r in proc.Requires) + { + newRequires.Add(new Requires(r.Free, Predicator.ProcessEnabledIntrinsics(r.Condition, enabled))); + } + proc.Requires = newRequires; + + EnsuresSeq newEnsures = new EnsuresSeq(); + foreach (Ensures e in proc.Ensures) + { + newEnsures.Add(new Ensures(e.Free, Predicator.ProcessEnabledIntrinsics(e.Condition, enabled))); + } + proc.Ensures = newEnsures; + + } } @@ -2195,7 +2364,10 @@ namespace GPUVerify foreach(PredicateCmd p in originalInvariants) { result.Add(new AssertCmd(p.tok, new VariableDualiser(1).VisitExpr(p.Expr.Clone() as Expr))); - result.Add(new AssertCmd(p.tok, new VariableDualiser(2).VisitExpr(p.Expr.Clone() as Expr))); + if (!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(p.Expr)) + { + result.Add(new AssertCmd(p.tok, new VariableDualiser(2).VisitExpr(p.Expr.Clone() as Expr))); + } } return result; diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 204ffabe..99cbf0cd 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -104,7 +104,9 @@ + + diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs index 1ade15c9..7b4f7982 100644 --- a/Source/GPUVerify/Predicator.cs +++ b/Source/GPUVerify/Predicator.cs @@ -258,7 +258,7 @@ namespace GPUVerify return result; } - private Expr ProcessEnabledIntrinsics(Expr expr, TypedIdent currentPredicate) + internal static Expr ProcessEnabledIntrinsics(Expr expr, TypedIdent currentPredicate) { return new EnabledToPredicateVisitor(currentPredicate).VisitExpr(expr); } -- cgit v1.2.3 From 7d1a42f0c26e2c7ba37a7de4b1ba3175777596c9 Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 2 Mar 2012 11:28:04 -0800 Subject: various refactorings related to houdini --- Source/BoogieDriver/BoogieDriver.cs | 361 +++++++++++++++++++----------------- Source/Core/CommandLineOptions.cs | 9 +- Source/Houdini/Checker.cs | 9 +- Source/Houdini/Houdini.cs | 263 +++----------------------- Test/houdini/Answer | 14 ++ Test/houdini/runtest.bat | 4 +- 6 files changed, 246 insertions(+), 414 deletions(-) (limited to 'Source') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 9a30401d..1a2af93b 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -429,6 +429,134 @@ namespace Microsoft.Boogie { } } + static void ProcessOutcome(VC.VCGen.Outcome outcome, List errors, string timeIndication, + ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories) { + switch (outcome) { + default: + Contract.Assert(false); // unexpected outcome + throw new cce.UnreachableException(); + case VCGen.Outcome.ReachedBound: + Inform(String.Format("{0}verified", timeIndication)); + Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound)); + verified++; + break; + case VCGen.Outcome.Correct: + if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { + Inform(String.Format("{0}credible", timeIndication)); + verified++; + } + else { + Inform(String.Format("{0}verified", timeIndication)); + verified++; + } + break; + case VCGen.Outcome.TimedOut: + timeOuts++; + Inform(String.Format("{0}timed out", timeIndication)); + break; + case VCGen.Outcome.OutOfMemory: + outOfMemories++; + Inform(String.Format("{0}out of memory", timeIndication)); + break; + case VCGen.Outcome.Inconclusive: + inconclusives++; + Inform(String.Format("{0}inconclusive", timeIndication)); + break; + case VCGen.Outcome.Errors: + if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { + Inform(String.Format("{0}doomed", timeIndication)); + errorCount++; + } //else { + Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation + + { + // BP1xxx: Parsing errors + // BP2xxx: Name resolution errors + // BP3xxx: Typechecking errors + // BP4xxx: Abstract interpretation errors (Is there such a thing?) + // BP5xxx: Verification errors + + errors.Sort(new CounterexampleComparer()); + foreach (Counterexample error in errors) { + if (error is CallCounterexample) { + CallCounterexample err = (CallCounterexample)error; + if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null) { + ReportBplError(err.FailingRequires, err.FailingRequires.ErrorMessage, true, false); + } + else { + ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true, true); + ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true); + } + if (CommandLineOptions.Clo.XmlSink != null) { + CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace); + } + } + else if (error is ReturnCounterexample) { + ReturnCounterexample err = (ReturnCounterexample)error; + if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null) { + ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false); + } + else { + ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true, true); + ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true); + } + if (CommandLineOptions.Clo.XmlSink != null) { + CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace); + } + } + else // error is AssertCounterexample + { + AssertCounterexample err = (AssertCounterexample)error; + if (err.FailingAssert is LoopInitAssertCmd) { + ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true, true); + if (CommandLineOptions.Clo.XmlSink != null) { + CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace); + } + } + else if (err.FailingAssert is LoopInvMaintainedAssertCmd) { + // this assertion is a loop invariant which is not maintained + ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true, true); + if (CommandLineOptions.Clo.XmlSink != null) { + CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace); + } + } + else { + if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null) { + ReportBplError(err.FailingAssert, err.FailingAssert.ErrorMessage, true, false); + } + else if (err.FailingAssert.ErrorData is string) { + ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true); + } + else { + ReportBplError(err.FailingAssert, "Error BP5001: This assertion might not hold.", true, true); + } + if (CommandLineOptions.Clo.XmlSink != null) { + CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace); + } + } + } + if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) { + foreach (string info in error.relatedInformation) { + Contract.Assert(info != null); + Console.WriteLine(" " + info); + } + } + if (CommandLineOptions.Clo.ErrorTrace > 0) { + Console.WriteLine("Execution trace:"); + error.Print(4); + } + if (CommandLineOptions.Clo.ModelViewFile != null) { + error.PrintModel(); + } + errorCount++; + } + //} + Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s")); + } + break; + } + } + /// /// Given a resolved and type checked Boogie program, infers invariants for the program /// and then attempts to verify it. Returns: @@ -453,30 +581,6 @@ namespace Microsoft.Boogie { Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program); } - if (CommandLineOptions.Clo.ContractInfer) { - Houdini.Houdini houdini = new Houdini.Houdini(program, true); - Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference(); - int numTrueAssigns = 0; - Console.WriteLine("Assignment computed by Houdini:"); - foreach (var x in outcome.assignment) { - Console.WriteLine(x.Key + " = " + x.Value); - if (x.Value) - numTrueAssigns++; - } - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Number of true assignments = " + numTrueAssigns); - Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns)); - Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime); - Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries); - } - errorCount = outcome.ErrorCount; - verified = outcome.Verified; - inconclusives = outcome.Inconclusives; - timeOuts = outcome.TimeOuts; - outOfMemories = 0; - return PipelineOutcome.Done; - } - if (CommandLineOptions.Clo.LoopUnrollCount != -1) { program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount); } @@ -502,6 +606,40 @@ namespace Microsoft.Boogie { return PipelineOutcome.Done; } + #region Run Houdini and verify + if (CommandLineOptions.Clo.ContractInfer) { + Houdini.Houdini houdini = new Houdini.Houdini(program, true); + Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference(); + if (CommandLineOptions.Clo.PrintAssignment) { + Console.WriteLine("Assignment computed by Houdini:"); + foreach (var x in outcome.assignment) { + Console.WriteLine(x.Key + " = " + x.Value); + } + } + if (CommandLineOptions.Clo.Trace) { + int numTrueAssigns = 0; + foreach (var x in outcome.assignment) { + if (x.Value) + numTrueAssigns++; + } + Console.WriteLine("Number of true assignments = " + numTrueAssigns); + Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns)); + Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime); + Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries); + } + + foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) { + ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories); + } + //errorCount = outcome.ErrorCount; + //verified = outcome.Verified; + //inconclusives = outcome.Inconclusives; + //timeOuts = outcome.TimeOuts; + //outOfMemories = 0; + return PipelineOutcome.Done; + } + #endregion + #region Verify each implementation ConditionGeneration vcgen = null; @@ -541,42 +679,39 @@ namespace Microsoft.Boogie { VCGen.Outcome outcome; try { - if (CommandLineOptions.Clo.inferLeastForUnsat != null) - { - var svcgen = vcgen as VC.StratifiedVCGen; - Contract.Assert(svcgen != null); - var ss = new HashSet(); - foreach (var tdecl in program.TopLevelDeclarations) - { - var c = tdecl as Constant; - if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue; - ss.Add(c.Name); - } - outcome = svcgen.FindLeastToVerify(impl, program, ref ss); - errors = new List(); - Console.Write("Result: "); - foreach (var s in ss) - { - Console.Write("{0} ", s); - } - Console.WriteLine(); + if (CommandLineOptions.Clo.inferLeastForUnsat != null) { + var svcgen = vcgen as VC.StratifiedVCGen; + Contract.Assert(svcgen != null); + var ss = new HashSet(); + foreach (var tdecl in program.TopLevelDeclarations) { + var c = tdecl as Constant; + if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue; + ss.Add(c.Name); } - else - { - outcome = vcgen.VerifyImplementation(impl, program, out errors); + outcome = svcgen.FindLeastToVerify(impl, program, ref ss); + errors = new List(); + Console.Write("Result: "); + foreach (var s in ss) { + Console.Write("{0} ", s); } - } catch (VCGenException e) { + Console.WriteLine(); + } + else { + outcome = vcgen.VerifyImplementation(impl, program, out errors); + } + } + catch (VCGenException e) { ReportBplError(impl, String.Format("Error BP5010: {0} Encountered in implementation {1}.", e.Message, impl.Name), true, true); errors = null; outcome = VCGen.Outcome.Inconclusive; - } catch (UnexpectedProverOutputException upo) { + } + catch (UnexpectedProverOutputException upo) { AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message); errors = null; outcome = VCGen.Outcome.Inconclusive; } string timeIndication = ""; - DateTime end = DateTime.UtcNow; TimeSpan elapsed = end - start; if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) { @@ -586,130 +721,14 @@ namespace Microsoft.Boogie { } } - - switch (outcome) { - default: - Contract.Assert(false); // unexpected outcome - throw new cce.UnreachableException(); - case VCGen.Outcome.ReachedBound: - Inform(String.Format("{0}verified", timeIndication)); - Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound)); - verified++; - break; - case VCGen.Outcome.Correct: - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { - Inform(String.Format("{0}credible", timeIndication)); - verified++; - } else { - Inform(String.Format("{0}verified", timeIndication)); - verified++; + if (CommandLineOptions.Clo.ExtractLoops && (vcgen is VCGen)) { + for (int i = 0; i < errors.Count; i++) { + errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo); } - break; - case VCGen.Outcome.TimedOut: - timeOuts++; - Inform(String.Format("{0}timed out", timeIndication)); - break; - case VCGen.Outcome.OutOfMemory: - outOfMemories++; - Inform(String.Format("{0}out of memory", timeIndication)); - break; - case VCGen.Outcome.Inconclusive: - inconclusives++; - Inform(String.Format("{0}inconclusive", timeIndication)); - break; - case VCGen.Outcome.Errors: - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { - Inform(String.Format("{0}doomed", timeIndication)); - errorCount++; - } //else { - Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation + } - { - // BP1xxx: Parsing errors - // BP2xxx: Name resolution errors - // BP3xxx: Typechecking errors - // BP4xxx: Abstract interpretation errors (Is there such a thing?) - // BP5xxx: Verification errors - - if (CommandLineOptions.Clo.ExtractLoops && (vcgen is VCGen)) - { - for (int i = 0; i < errors.Count; i++) - { - errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo); - } - } + ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories); - errors.Sort(new CounterexampleComparer()); - foreach (Counterexample error in errors) { - if (error is CallCounterexample) { - CallCounterexample err = (CallCounterexample)error; - if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null) { - ReportBplError(err.FailingRequires, err.FailingRequires.ErrorMessage, true, false); - } else { - ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true, true); - ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true); - } - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace); - } - } else if (error is ReturnCounterexample) { - ReturnCounterexample err = (ReturnCounterexample)error; - if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null) { - ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false); - } else { - ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true, true); - ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true); - } - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace); - } - } else // error is AssertCounterexample - { - AssertCounterexample err = (AssertCounterexample)error; - if (err.FailingAssert is LoopInitAssertCmd) { - ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true, true); - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace); - } - } else if (err.FailingAssert is LoopInvMaintainedAssertCmd) { - // this assertion is a loop invariant which is not maintained - ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true, true); - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace); - } - } else { - if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null) { - ReportBplError(err.FailingAssert, err.FailingAssert.ErrorMessage, true, false); - } else if (err.FailingAssert.ErrorData is string) { - ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true); - } else { - ReportBplError(err.FailingAssert, "Error BP5001: This assertion might not hold.", true, true); - } - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace); - } - } - } - if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) { - foreach (string info in error.relatedInformation) { - Contract.Assert(info != null); - Console.WriteLine(" " + info); - } - } - if (CommandLineOptions.Clo.ErrorTrace > 0) { - Console.WriteLine("Execution trace:"); - error.Print(4); - } - if (CommandLineOptions.Clo.ModelViewFile != null) { - error.PrintModel(); - } - errorCount++; - } - //} - Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s")); - } - break; - } if (CommandLineOptions.Clo.XmlSink != null) { CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed); } @@ -718,6 +737,7 @@ namespace Microsoft.Boogie { } } } + vcgen.Close(); cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close(); @@ -726,6 +746,5 @@ namespace Microsoft.Boogie { return PipelineOutcome.VerificationCompleted; } - } } diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 42155f45..1a2d7fda 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -389,6 +389,7 @@ namespace Microsoft.Boogie { public int /*(0:3)*/ ErrorTrace = 1; public bool IntraproceduralInfer = true; public bool ContractInfer = false; + public bool PrintAssignment = false; public int InlineDepth = -1; public bool UseUncheckedContracts = false; public bool SimplifyLogFileAppend = false; @@ -830,10 +831,6 @@ namespace Microsoft.Boogie { ps.GetNumericArgument(ref EnhancedErrorMessages, 2); return true; - case "contractInfer": - ContractInfer = true; - return true; - case "inlineDepth": ps.GetNumericArgument(ref InlineDepth); return true; @@ -1229,7 +1226,9 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("monomorphize", ref Monomorphize) || ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) || ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) || - ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) + ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) || + ps.CheckBooleanFlag("contractInfer", ref ContractInfer) || + ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ) { // one of the boolean flags matched return true; diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index a2bf0304..29357997 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -56,12 +56,19 @@ namespace Microsoft.Boogie.Houdini { collector.examples.Clear(); VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture); + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Verifying " + descriptiveName); + } DateTime now = DateTime.UtcNow; checker.BeginCheck(descriptiveName, vc, handler); WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone }); ProverInterface.Outcome proverOutcome = checker.ReadOutcome(); - proverTime += (DateTime.UtcNow - now).TotalSeconds; + double queryTime = (DateTime.UtcNow - now).TotalSeconds; + proverTime += queryTime; numProverQueries++; + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Time taken = " + queryTime); + } if (proverOutcome == ProverInterface.Outcome.Invalid) { Contract.Assume(collector.examples != null); diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 68a8efb6..5ac78731 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -537,25 +537,6 @@ namespace Microsoft.Boogie.Houdini { return outcome; } - private ProverInterface.Outcome VerifyCurrent( - HoudiniSession session, - HoudiniState current, - Program program, - out List errors, - out bool exc) { - if (current.Implementation != null) { - Implementation implementation = current.Implementation; - if (vcgen == null) - throw new Exception("HdnVCGen not found for implementation: " + implementation.Name); - - ProverInterface.Outcome outcome = TrySpinSameFunc(session, current, program, out errors, out exc); - return outcome; - } - else { - throw new Exception("VerifyCurrent has null implementation"); - } - } - private bool IsOutcomeNotHoudini(ProverInterface.Outcome outcome, List errors) { switch (outcome) { case ProverInterface.Outcome.Valid: @@ -651,51 +632,6 @@ namespace Microsoft.Boogie.Houdini { } } - private void UpdateWorkList(HoudiniState current, - ProverInterface.Outcome outcome, - List errors) { - Contract.Assume(current.Implementation != null); - - switch (outcome) { - case ProverInterface.Outcome.Valid: - current.WorkQueue.Dequeue(); - this.NotifyDequeue(); - break; - case ProverInterface.Outcome.Invalid: - Contract.Assume(errors != null); - bool dequeue = false; - foreach (Counterexample error in errors) { - RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error); - if (refutedAnnotation != null) { - foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) { AddToWorkList(current, implementation); } - UpdateAssignment(current, refutedAnnotation); - } - else { - dequeue = true; //once one non-houdini error is hit dequeue?! - } - } - if (dequeue) { - current.WorkQueue.Dequeue(); - this.NotifyDequeue(); - } - break; - case ProverInterface.Outcome.TimeOut: - // TODO: reset session instead of blocking timed out funcs? - current.addToBlackList(current.Implementation.Name); - current.WorkQueue.Dequeue(); - this.NotifyDequeue(); - break; - case ProverInterface.Outcome.OutOfMemory: - case ProverInterface.Outcome.Undetermined: - current.WorkQueue.Dequeue(); - this.NotifyDequeue(); - break; - default: - throw new Exception("Unknown vcgen outcome"); - } - } - - private void AddRelatedToWorkList(HoudiniState current, RefutedAnnotation refutedAnnotation) { Contract.Assume(current.Implementation != null); foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) { @@ -810,102 +746,6 @@ namespace Microsoft.Boogie.Houdini { } } - private void PrintBadList(string kind, List list) { - if (list.Count != 0) { - Console.WriteLine("----------------------------------------"); - Console.WriteLine("Functions: {0}", kind); - foreach (string fname in list) { - Console.WriteLine("\t{0}", fname); - } - Console.WriteLine("----------------------------------------"); - } - } - - private void PrintBadOutcomes(List timeouts, List inconc, List errors) { - PrintBadList("TimedOut", timeouts); - PrintBadList("Inconclusive", inconc); - PrintBadList("Errors", errors); - } - - public HoudiniOutcome VerifyProgram() { - HoudiniOutcome outcome = VerifyProgramSameFuncFirst(); - PrintBadOutcomes(outcome.ListOfTimeouts, outcome.ListOfInconclusives, outcome.ListOfErrors); - return outcome; - } - - // Old main loop - public HoudiniOutcome VerifyProgramUnorderedWork() { - HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys)); - this.NotifyStart(program, houdiniConstants.Keys.Count); - - while (current.WorkQueue.Count > 0) { - //System.GC.Collect(); - this.NotifyIteration(); - - VCExpr axiom = BuildAxiom(current.Assignment); - this.NotifyAssignment(current.Assignment); - - current.Implementation = current.WorkQueue.Peek(); - this.NotifyImplementation(current.Implementation); - - List errors; - HoudiniSession session; - houdiniSessions.TryGetValue(current.Implementation, out session); - ProverInterface.Outcome outcome = VerifyUsingAxiom(session, current.Implementation, axiom, out errors); - this.NotifyOutcome(outcome); - - UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors); - if (IsOutcomeNotHoudini(outcome, errors) && !continueAtError) { - current.WorkQueue.Dequeue(); - this.NotifyDequeue(); - FlushWorkList(current); - } - else - UpdateWorkList(current, outcome, errors); - } - this.NotifyEnd(true); - current.Outcome.assignment = current.Assignment; - return current.Outcome; - } - - // New main loop - public HoudiniOutcome VerifyProgramSameFuncFirst() { - HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys)); - this.NotifyStart(program, houdiniConstants.Keys.Count); - - while (current.WorkQueue.Count > 0) { - bool exceptional = false; - //System.GC.Collect(); - this.NotifyIteration(); - - current.Implementation = current.WorkQueue.Peek(); - this.NotifyImplementation(current.Implementation); - - HoudiniSession session; - houdiniSessions.TryGetValue(current.Implementation, out session); - List errors; - ProverInterface.Outcome outcome = VerifyCurrent(session, current, program, out errors, out exceptional); - - // updates to worklist already done in VerifyCurrent, unless there was an exception - if (exceptional) { - this.NotifyOutcome(outcome); - UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors); - if (IsOutcomeNotHoudini(outcome, errors) && !continueAtError) { - current.WorkQueue.Dequeue(); - this.NotifyDequeue(); - FlushWorkList(current); - } - else { - UpdateAssignmentWorkList(current, outcome, errors); - } - exceptional = false; - } - } - this.NotifyEnd(true); - current.Outcome.assignment = current.Assignment; - return current.Outcome; - } - //Clean houdini (Based on "Houdini Spec in Boogie" email 10/22/08 //Aborts when there is a violation of non-candidate assertion //This can be used in eager mode (continueAfterError) by simply making @@ -1098,67 +938,7 @@ namespace Microsoft.Boogie.Houdini { return outcome; } - //version of TryCatchVerify that spins on the same function - //as long as the current assignment is changing - private ProverInterface.Outcome TrySpinSameFunc( - HoudiniSession session, - HoudiniState current, - Program program, - out List errors, - out bool exceptional) { - Contract.Assert(current.Implementation != null); - ProverInterface.Outcome outcome; - errors = null; - outcome = ProverInterface.Outcome.Undetermined; - try { - bool trySameFunc = true; - bool pastFirstIter = false; //see if this new loop is even helping - - do { - if (pastFirstIter) { - //System.GC.Collect(); - this.NotifyIteration(); - } - - VCExpr currentAx = BuildAxiom(current.Assignment); - this.NotifyAssignment(current.Assignment); - - outcome = session.Verify(checker, currentAx, out errors); - this.NotifyOutcome(outcome); - - DebugRefutedCandidates(current.Implementation, errors); - UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors); - if (!continueAtError && IsOutcomeNotHoudini(outcome, errors)) { - current.WorkQueue.Dequeue(); - this.NotifyDequeue(); - trySameFunc = false; - FlushWorkList(current); - } - else { - trySameFunc = UpdateAssignmentWorkList(current, outcome, errors); - //reset for the next round - errors = null; - outcome = ProverInterface.Outcome.Undetermined; - } - pastFirstIter = true; - } while (trySameFunc && current.WorkQueue.Count > 0); - - } - catch (VCGenException e) { - Contract.Assume(e != null); - NotifyException("VCGen"); - exceptional = true; - return outcome; - } - catch (UnexpectedProverOutputException upo) { - Contract.Assume(upo != null); - NotifyException("UnexpectedProverOutput"); - exceptional = true; - return outcome; - } - exceptional = false; - return outcome; - } + //Similar to TrySpinSameFunc except no Candidate logic private ProverInterface.Outcome HoudiniVerifyCurrentAux( @@ -1191,9 +971,6 @@ namespace Microsoft.Boogie.Houdini { this.NotifyAssignment(current.Assignment); //check the VC with the current assignment - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Verifying " + session.descriptiveName); - } outcome = session.Verify(checker, currentAx, out errors); this.NotifyOutcome(outcome); @@ -1232,10 +1009,26 @@ namespace Microsoft.Boogie.Houdini { public enum HoudiniOutcomeKind { Done, FatalError, VerificationCompleted } public class VCGenOutcome { - public ProverInterface.Outcome outcome; + public VCGen.Outcome outcome; public List errors; public VCGenOutcome(ProverInterface.Outcome outcome, List errors) { - this.outcome = outcome; + switch (outcome) { + case ProverInterface.Outcome.Invalid: + this.outcome = ConditionGeneration.Outcome.Errors; + break; + case ProverInterface.Outcome.OutOfMemory: + this.outcome = ConditionGeneration.Outcome.OutOfMemory; + break; + case ProverInterface.Outcome.TimeOut: + this.outcome = ConditionGeneration.Outcome.TimedOut; + break; + case ProverInterface.Outcome.Undetermined: + this.outcome = ConditionGeneration.Outcome.Inconclusive; + break; + case ProverInterface.Outcome.Valid: + this.outcome = ConditionGeneration.Outcome.Correct; + break; + } this.errors = errors; } } @@ -1250,7 +1043,7 @@ namespace Microsoft.Boogie.Houdini { // statistics - private int CountResults(ProverInterface.Outcome outcome) { + private int CountResults(VCGen.Outcome outcome) { int outcomeCount = 0; foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values) { if (verifyOutcome.outcome == outcome) @@ -1259,7 +1052,7 @@ namespace Microsoft.Boogie.Houdini { return outcomeCount; } - private List ListOutcomeMatches(ProverInterface.Outcome outcome) { + private List ListOutcomeMatches(VCGen.Outcome outcome) { List result = new List(); foreach (KeyValuePair kvpair in implementationOutcomes) { if (kvpair.Value.outcome == outcome) @@ -1270,37 +1063,37 @@ namespace Microsoft.Boogie.Houdini { public int ErrorCount { get { - return CountResults(ProverInterface.Outcome.Invalid); + return CountResults(VCGen.Outcome.Errors); } } public int Verified { get { - return CountResults(ProverInterface.Outcome.Valid); + return CountResults(VCGen.Outcome.Correct); } } public int Inconclusives { get { - return CountResults(ProverInterface.Outcome.Undetermined); + return CountResults(VCGen.Outcome.Inconclusive); } } public int TimeOuts { get { - return CountResults(ProverInterface.Outcome.TimeOut); + return CountResults(VCGen.Outcome.TimedOut); } } public List ListOfTimeouts { get { - return ListOutcomeMatches(ProverInterface.Outcome.TimeOut); + return ListOutcomeMatches(VCGen.Outcome.TimedOut); } } public List ListOfInconclusives { get { - return ListOutcomeMatches(ProverInterface.Outcome.Undetermined); + return ListOutcomeMatches(VCGen.Outcome.Inconclusive); } } public List ListOfErrors { get { - return ListOutcomeMatches(ProverInterface.Outcome.Invalid); + return ListOutcomeMatches(VCGen.Outcome.Errors); } } } diff --git a/Test/houdini/Answer b/Test/houdini/Answer index 6053b442..d7edbce6 100644 --- a/Test/houdini/Answer +++ b/Test/houdini/Answer @@ -9,6 +9,10 @@ Boogie program verifier finished with 1 verified, 0 errors Assignment computed by Houdini: b1 = False b2 = True +houd2.bpl(12,1): Error BP5003: A postcondition might not hold on this return path. +houd2.bpl(9,1): Related location: This is the postcondition that might not hold. +Execution trace: + houd2.bpl(11,3): anon0 Boogie program verifier finished with 1 verified, 1 error @@ -72,6 +76,9 @@ Assignment computed by Houdini: b1 = True b2 = True b3 = True +houd9.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + houd9.bpl(18,9): anon0 Boogie program verifier finished with 0 verified, 1 error @@ -80,11 +87,18 @@ Assignment computed by Houdini: b1 = True b2 = True b3 = True +houd10.bpl(15,3): Error BP5002: A precondition for this call might not hold. +houd10.bpl(20,1): Related location: This is the precondition that might not hold. +Execution trace: + houd10.bpl(14,9): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- houd11.bpl -------------------- Assignment computed by Houdini: +houd11.bpl(8,3): Error BP5001: This assertion might not hold. +Execution trace: + houd11.bpl(7,9): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat index f0065b0d..b9816bb9 100644 --- a/Test/houdini/runtest.bat +++ b/Test/houdini/runtest.bat @@ -6,11 +6,11 @@ set BGEXE=..\..\Binaries\Boogie.exe for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd9.bpl houd10.bpl houd11.bpl houd12.bpl) do ( echo. echo -------------------- %%f -------------------- - %BGEXE% %* /nologo /noinfer /contractInfer %%f + %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment %%f ) for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do ( echo . echo -------------------- %%f -------------------- - %BGEXE% %* /nologo /noinfer /contractInfer /inlineDepth:1 %%f + %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 %%f ) -- cgit v1.2.3 From b07e5b62739645a6a3a4018b41c0e8690f0e10ff Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 2 Mar 2012 12:06:22 -0800 Subject: small fix for a bug I introduced during the refactoring of InferAndVerify --- Source/BoogieDriver/BoogieDriver.cs | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'Source') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 1a2af93b..b765a1c3 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -698,6 +698,11 @@ namespace Microsoft.Boogie { } else { outcome = vcgen.VerifyImplementation(impl, program, 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); + } + } } } catch (VCGenException e) { @@ -721,12 +726,6 @@ namespace Microsoft.Boogie { } } - if (CommandLineOptions.Clo.ExtractLoops && (vcgen is VCGen)) { - for (int i = 0; i < errors.Count; i++) { - errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo); - } - } - ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories); if (CommandLineOptions.Clo.XmlSink != null) { -- cgit v1.2.3