From e129afe1528a5213c56171dd12afaadb1e219d4c Mon Sep 17 00:00:00 2001 From: qadeer Date: Thu, 4 Aug 2011 21:55:13 -0700 Subject: further changes for making houdini work --- Source/BoogieDriver/BoogieDriver.cs | 12 ++- Source/Houdini/Checker.cs | 134 +++++------------------- Source/Houdini/Houdini.cs | 199 +++++++++++++++++------------------- Source/VCGeneration/VC.cs | 4 +- Test/houdini/houd6.bpl | 2 +- 5 files changed, 132 insertions(+), 219 deletions(-) diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 35c0832a..82c864d5 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -431,7 +431,17 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.ContractInfer) { Houdini.Houdini houdini = new Houdini.Houdini(program, true); - houdini.PerformHoudiniInference(); + Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference(); + Console.WriteLine("Assignment computed by Houdini:"); + foreach (var x in outcome.assignment) { + Console.WriteLine(x.Key + " = " + x.Value); + } + errorCount = outcome.ErrorCount; + verified = outcome.Verified; + inconclusives = outcome.Inconclusives; + timeOuts = outcome.TimeOuts; + outOfMemories = 0; + return PipelineOutcome.Done; } if (CommandLineOptions.Clo.LoopUnrollCount != -1) { diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 294f5d1b..437dbc98 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -16,84 +16,29 @@ using System.Threading; using VC; namespace Microsoft.Boogie.Houdini { - class HoudiniChecker { - private Stack axioms = new Stack(); + public class HoudiniVCGen : VCGen { private Checker checker; private string descriptiveName; private VCExpr conjecture; private ProverInterface.ErrorHandler handler; + CounterexampleCollector collector; - internal HoudiniChecker(Checker checker, string _descriptiveName, VCExpr _vc, ProverInterface.ErrorHandler _handler) - { - Contract.Requires(checker.TheoremProver != null); - Contract.Requires(checker.TheoremProver is Z3ProcessTheoremProver); - this.checker = checker; - this.descriptiveName = _descriptiveName; - this.conjecture = _vc; - this.handler = _handler; - } - - public void PushAxiom(Axiom axiom) { - DeclFreeProverContext proverContext = (DeclFreeProverContext) checker.TheoremProver.Context; - VCExpr vc = proverContext.BoogieExprTranslator.Translate(axiom.Expr); - axioms.Push(vc); - } - - public void Pop() { - axioms.Pop(); - } - - private VCExpr BuildVCAxioms(Stack axioms) - { - Contract.Requires(axioms.Count > 0); - VCExpr vc_axioms = null; - foreach (VCExpr axiom in axioms) { - if (vc_axioms == null) - vc_axioms = axiom; - else - vc_axioms = checker.VCExprGen.And(vc_axioms, axiom); - } - return vc_axioms; - } - - public void Check() - { - Contract.Assert (descriptiveName != null); - Contract.Assert (conjecture != null); - Contract.Assert (handler != null); - outcome = ProverInterface.Outcome.Undetermined; - - VCExpr vc; - if (axioms.Count > 0) { - VCExpr vc_axioms = BuildVCAxioms(axioms); - vc = checker.VCExprGen.Implies(vc_axioms, conjecture); - } - else { - vc = conjecture; + public VCExpressionGenerator VCExprGenerator { + get { + return checker.VCExprGen; } - checker.BeginCheck(descriptiveName, vc, handler); - WaitHandle.WaitAny(new WaitHandle[] {checker.ProverDone}); } - - private ProverInterface.Outcome outcome; - public ProverInterface.Outcome ReadOutcome() - { - try { - outcome = checker.ReadOutcome(); - } catch (UnexpectedProverOutputException e) { - throw e; + public Boogie2VCExprTranslator BooogieExprTranslator { + get { + DeclFreeProverContext proverContext = (DeclFreeProverContext)checker.TheoremProver.Context; + return proverContext.BoogieExprTranslator; } - return outcome; } - } - public class HoudiniVCGen : VCGen { - private HoudiniChecker hdnChecker; - CounterexampleCollector collector; - - public HoudiniVCGen(Program program, Implementation impl, string logFilePath, bool appendLogFile) - : base(program, logFilePath, appendLogFile) { + public HoudiniVCGen(Program program, Implementation impl, string logFilePath, bool appendLogFile) + : base(program, logFilePath, appendLogFile) { + descriptiveName = impl.Name; collector = new CounterexampleCollector(); collector.OnProgress("HdnVCGen", 0, 0, 0.0); if (CommandLineOptions.Clo.SoundnessSmokeTest) { @@ -104,37 +49,28 @@ namespace Microsoft.Boogie.Houdini { ModelViewInfo mvInfo; Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo); Hashtable/**/ label2absy; - Checker checker = new Checker(this, program, this.logFilePath, this.appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime); - VCExpr vc = GenerateVC(impl, null, out label2absy, checker); + checker = new Checker(this, program, logFilePath, appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime); + if (!(checker.TheoremProver is Z3ProcessTheoremProver)) { + throw new Exception("HdnChecker only works with z3"); + } + conjecture = GenerateVC(impl, null, out label2absy, checker); - ErrorReporter reporter; if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) { - reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, checker.TheoremProver.Context, program); + handler = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, implName2LazyInliningInfo, checker.TheoremProver.Context, program); } else { - reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, checker.TheoremProver.Context, program); + handler = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, implName2LazyInliningInfo, checker.TheoremProver.Context, program); } - if (checker.TheoremProver is Z3ProcessTheoremProver) - this.hdnChecker = new HoudiniChecker(checker, impl.Name, vc, reporter); - else - throw new Exception("HdnChecker only works with z3"); } - public void PushAxiom(Axiom axiom) { - this.hdnChecker.PushAxiom(axiom); - } - - public void Pop() { - hdnChecker.Pop(); - } - - public Outcome Verify(out List errors) { + public ProverInterface.Outcome Verify(VCExpr axiom, out List errors) { collector.examples.Clear(); - hdnChecker.Check(); - ProverInterface.Outcome proverOutcome; - proverOutcome = hdnChecker.ReadOutcome(); - Outcome verifyOutcome = ReadOutcome(proverOutcome); - if (verifyOutcome == Outcome.Errors) { + VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture); + checker.BeginCheck(descriptiveName, vc, handler); + WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone }); + + ProverInterface.Outcome proverOutcome = checker.ReadOutcome(); + if (proverOutcome == ProverInterface.Outcome.Invalid) { Contract.Assume(collector.examples != null); if (collector.examples.Count == 0) { string memStr = System.Convert.ToString(System.GC.GetTotalMemory(false)); @@ -147,24 +83,8 @@ namespace Microsoft.Boogie.Houdini { else { errors = null; } - return verifyOutcome; - } - - private Outcome ReadOutcome(ProverInterface.Outcome proverOutcome) { - switch (proverOutcome) { - case ProverInterface.Outcome.Valid: - return Outcome.Correct; - case ProverInterface.Outcome.Invalid: - return Outcome.Errors; - case ProverInterface.Outcome.TimeOut: - return Outcome.TimedOut; - case ProverInterface.Outcome.Undetermined: - return Outcome.Inconclusive; - default: - throw new Exception("Unknown Prover Interface outcome while reading outcome."); - } + return proverOutcome; } } - } \ No newline at end of file diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 1efc0e91..714ecd3b 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -42,7 +42,7 @@ namespace Microsoft.Boogie.Houdini { public virtual void UpdateIteration() { } public virtual void UpdateImplementation(Implementation implementation) { } public virtual void UpdateAssignment(Dictionary assignment) { } - public virtual void UpdateOutcome(VCGen.Outcome outcome) { } + public virtual void UpdateOutcome(ProverInterface.Outcome outcome) { } public virtual void UpdateEnqueue(Implementation implementation) { } public virtual void UpdateDequeue() { } public virtual void UpdateConstant(string constantName) { } @@ -108,7 +108,7 @@ namespace Microsoft.Boogie.Houdini { public override void UpdateImplementation(Implementation implementation) { curImp = implementation; } - public override void UpdateOutcome(VCGen.Outcome o) { + public override void UpdateOutcome(ProverInterface.Outcome o) { Contract.Assert(curImp != null); DateTime endT = DateTime.Now; times.AddTime(curImp.Name, (endT - startT).TotalMilliseconds); // assuming names are unique @@ -155,7 +155,7 @@ namespace Microsoft.Boogie.Houdini { wr.WriteLine(");"); wr.Flush(); } - public override void UpdateOutcome(VCGen.Outcome outcome) { + public override void UpdateOutcome(ProverInterface.Outcome outcome) { wr.WriteLine("analysis outcome :" + outcome); wr.Flush(); } @@ -221,7 +221,7 @@ namespace Microsoft.Boogie.Houdini { protected void NotifyAssignment(Dictionary assignment) { Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateAssignment(assignment); }); } - protected void NotifyOutcome(VCGen.Outcome outcome) { + protected void NotifyOutcome(ProverInterface.Outcome outcome) { Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateOutcome(outcome); }); } protected void NotifyEnqueue(Implementation implementation) { @@ -300,15 +300,19 @@ namespace Microsoft.Boogie.Houdini { } private Graph BuildCallGraph() { + Graph callGraph = new Graph(); Dictionary> procToImpls = new Dictionary>(); + foreach (Declaration decl in program.TopLevelDeclarations) { + Procedure proc = decl as Procedure; + if (proc == null) continue; + procToImpls[proc] = new HashSet(); + } foreach (Declaration decl in program.TopLevelDeclarations) { Implementation impl = decl as Implementation; if (impl == null) continue; - if (!procToImpls.ContainsKey(impl.Proc)) - procToImpls[impl.Proc] = new HashSet(); + callGraph.AddSource(impl); procToImpls[impl.Proc].Add(impl); } - Graph callGraph = new Graph(); foreach (Declaration decl in program.TopLevelDeclarations) { Implementation impl = decl as Implementation; if (impl == null) continue; @@ -350,21 +354,24 @@ namespace Microsoft.Boogie.Houdini { return false; } - private Axiom BuildAxiom(Dictionary currentAssignment, Boogie2VCExprTranslator exprTranslator) { - Expr expr = new LiteralExpr(Token.NoToken, true); - expr.Type = Type.Bool; + private VCExpr BuildAxiom(HoudiniVCGen vcgen, Dictionary currentAssignment) { + Boogie2VCExprTranslator exprTranslator = vcgen.BooogieExprTranslator; + VCExpressionGenerator exprGen = vcgen.VCExprGenerator; + + VCExpr expr = VCExpressionGenerator.True; foreach (KeyValuePair kv in currentAssignment) { IdentifierExpr constantExpr; houdiniConstants.TryGetValue(kv.Key, out constantExpr); Contract.Assume(constantExpr != null); - Expr valueExpr = new LiteralExpr(Token.NoToken, kv.Value); - valueExpr.Type = Type.Bool; - Expr constantAssignment = Expr.Binary(Token.NoToken, BinaryOperator.Opcode.Eq, constantExpr, valueExpr); - constantAssignment.Type = Type.Bool; - expr = Expr.Binary(Token.NoToken, BinaryOperator.Opcode.And, expr, constantAssignment); - expr.Type = Type.Bool; + VCExprVar exprVar = exprTranslator.LookupVariable(constantExpr.Decl); + if (kv.Value) { + expr = exprGen.And(expr, exprVar); + } + else { + expr = exprGen.And(expr, exprGen.Not(exprVar)); + } } - return new Axiom(Token.NoToken, expr); + return expr; } private Dictionary BuildAssignment(Dictionary.KeyCollection constants) { @@ -374,20 +381,18 @@ namespace Microsoft.Boogie.Houdini { return initial; } - private VCGen.Outcome VerifyUsingAxiom(Implementation implementation, Axiom axiom, out List errors) { + private ProverInterface.Outcome VerifyUsingAxiom(Implementation implementation, VCExpr axiom, out List errors) { HoudiniVCGen vcgen; vcgenSessions.TryGetValue(implementation, out vcgen); if (vcgen == null) throw new Exception("HdnVCGen not found for implementation: " + implementation.Name); - vcgen.PushAxiom(axiom); - VCGen.Outcome outcome = TryCatchVerify(vcgen, out errors); - vcgen.Pop(); + ProverInterface.Outcome outcome = TryCatchVerify(vcgen, axiom, out errors); return outcome; } // the main procedure that checks a procedure and updates the // assignment and the worklist - private VCGen.Outcome HoudiniVerifyCurrent(HoudiniState current, + private ProverInterface.Outcome HoudiniVerifyCurrent(HoudiniState current, Program program, out List errors, out bool exc) { @@ -400,11 +405,11 @@ namespace Microsoft.Boogie.Houdini { if (vcgen == null) throw new Exception("HdnVCGen not found for implementation: " + implementation.Name); - VCGen.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc); + ProverInterface.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc); return outcome; } - private VCGen.Outcome VerifyCurrent(HoudiniState current, + private ProverInterface.Outcome VerifyCurrent(HoudiniState current, Program program, out List errors, out bool exc) { @@ -415,7 +420,7 @@ namespace Microsoft.Boogie.Houdini { if (vcgen == null) throw new Exception("HdnVCGen not found for implementation: " + implementation.Name); - VCGen.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc); + ProverInterface.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc); return outcome; } else { @@ -423,37 +428,32 @@ namespace Microsoft.Boogie.Houdini { } } - private bool IsOutcomeNotHoudini(VCGen.Outcome outcome, List errors) { + private bool IsOutcomeNotHoudini(ProverInterface.Outcome outcome, List errors) { switch (outcome) { - case VCGen.Outcome.Correct: + case ProverInterface.Outcome.Valid: return false; - case VCGen.Outcome.Errors: + case ProverInterface.Outcome.Invalid: Contract.Assume(errors != null); foreach (Counterexample error in errors) { if (ExtractRefutedAnnotation(error) == null) return true; } return false; - case VCGen.Outcome.TimedOut: - case VCGen.Outcome.Inconclusive: default: return true; } } // returns true if at least one of the violations is non-candidate - private bool AnyNonCandidateViolation(VCGen.Outcome outcome, List errors) { + private bool AnyNonCandidateViolation(ProverInterface.Outcome outcome, List errors) { switch (outcome) { - case VCGen.Outcome.Errors: + case ProverInterface.Outcome.Invalid: Contract.Assert(errors != null); foreach (Counterexample error in errors) { if (ExtractRefutedAnnotation(error) == null) return true; } return false; - case VCGen.Outcome.Correct: - case VCGen.Outcome.TimedOut: - case VCGen.Outcome.Inconclusive: default: return false; } @@ -464,23 +464,20 @@ namespace Microsoft.Boogie.Houdini { // Record most current Non-Candidate errors found by Boogie, etc. private void UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome, Implementation implementation, - VCGen.Outcome verificationOutcome, + ProverInterface.Outcome verificationOutcome, List errors) { string implName = implementation.ToString(); houdiniOutcome.implementationOutcomes.Remove(implName); List nonCandidateErrors = new List(); switch (verificationOutcome) { - case VCGen.Outcome.Errors: + case ProverInterface.Outcome.Invalid: Contract.Assume(errors != null); foreach (Counterexample error in errors) { if (ExtractRefutedAnnotation(error) == null) nonCandidateErrors.Add(error); } break; - case VCGen.Outcome.TimedOut: - case VCGen.Outcome.Correct: - case VCGen.Outcome.Inconclusive: default: break; } @@ -489,7 +486,9 @@ namespace Microsoft.Boogie.Houdini { private void FlushWorkList(HoudiniState current) { this.NotifyFlushStart(); - Axiom axiom = BuildAxiom(current.Assignment); + HoudiniVCGen vcgen; + vcgenSessions.TryGetValue(current.Implementation, out vcgen); + VCExpr axiom = BuildAxiom(vcgen, current.Assignment); while (current.WorkList.Count > 0) { this.NotifyIteration(); @@ -497,7 +496,7 @@ namespace Microsoft.Boogie.Houdini { this.NotifyImplementation(current.Implementation); List errors; - VCGen.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors); + ProverInterface.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors); UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors); this.NotifyOutcome(outcome); @@ -522,16 +521,16 @@ namespace Microsoft.Boogie.Houdini { } private void UpdateWorkList(HoudiniState current, - VCGen.Outcome outcome, + ProverInterface.Outcome outcome, List errors) { Contract.Assume(current.Implementation != null); switch (outcome) { - case VCGen.Outcome.Correct: + case ProverInterface.Outcome.Valid: current.WorkList.Dequeue(); this.NotifyDequeue(); break; - case VCGen.Outcome.Errors: + case ProverInterface.Outcome.Invalid: Contract.Assume(errors != null); bool dequeue = false; foreach (Counterexample error in errors) { @@ -549,14 +548,14 @@ namespace Microsoft.Boogie.Houdini { this.NotifyDequeue(); } break; - case VCGen.Outcome.TimedOut: + case ProverInterface.Outcome.TimeOut: // TODO: reset session instead of blocking timed out funcs? current.addToBlackList(current.Implementation.Name); current.WorkList.Dequeue(); this.NotifyDequeue(); break; - case VCGen.Outcome.OutOfMemory: - case VCGen.Outcome.Inconclusive: + case ProverInterface.Outcome.OutOfMemory: + case ProverInterface.Outcome.Undetermined: current.WorkList.Dequeue(); this.NotifyDequeue(); break; @@ -577,16 +576,16 @@ namespace Microsoft.Boogie.Houdini { // Updates the worklist and current assignment // @return true if the current function is kept on the queue private bool UpdateAssignmentWorkList(HoudiniState current, - VCGen.Outcome outcome, + ProverInterface.Outcome outcome, List errors) { Contract.Assume(current.Implementation != null); bool dequeue = true; switch (outcome) { - case VCGen.Outcome.Correct: + case ProverInterface.Outcome.Valid: //yeah, dequeue break; - case VCGen.Outcome.Errors: + case ProverInterface.Outcome.Invalid: Contract.Assume(errors != null); foreach (Counterexample error in errors) { RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error); @@ -598,12 +597,12 @@ namespace Microsoft.Boogie.Houdini { } break; - case VCGen.Outcome.TimedOut: + case ProverInterface.Outcome.TimeOut: // TODO: reset session instead of blocking timed out funcs? current.addToBlackList(current.Implementation.Name); break; - case VCGen.Outcome.Inconclusive: - case VCGen.Outcome.OutOfMemory: + case ProverInterface.Outcome.Undetermined: + case ProverInterface.Outcome.OutOfMemory: break; default: throw new Exception("Unknown vcgen outcome"); @@ -679,18 +678,22 @@ namespace Microsoft.Boogie.Houdini { HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys)); this.NotifyStart(program, houdiniConstants.Keys.Count); + + while (current.WorkList.Count > 0) { System.GC.Collect(); this.NotifyIteration(); - Axiom axiom = BuildAxiom(current.Assignment); + HoudiniVCGen vcgen; + vcgenSessions.TryGetValue(current.Implementation, out vcgen); + VCExpr axiom = BuildAxiom(vcgen, current.Assignment); this.NotifyAssignment(current.Assignment); current.Implementation = current.WorkList.Peek(); this.NotifyImplementation(current.Implementation); List errors; - VCGen.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors); + ProverInterface.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors); this.NotifyOutcome(outcome); UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors); @@ -721,7 +724,7 @@ namespace Microsoft.Boogie.Houdini { this.NotifyImplementation(current.Implementation); List errors; - VCGen.Outcome outcome = VerifyCurrent(current, program, out errors, out exceptional); + ProverInterface.Outcome outcome = VerifyCurrent(current, program, out errors, out exceptional); // updates to worklist already done in VerifyCurrent, unless there was an exception if (exceptional) { @@ -762,7 +765,7 @@ namespace Microsoft.Boogie.Houdini { this.NotifyImplementation(current.Implementation); List errors; - VCGen.Outcome outcome = HoudiniVerifyCurrent(current, program, out errors, out exceptional); + ProverInterface.Outcome outcome = HoudiniVerifyCurrent(current, program, out errors, out exceptional); // updates to worklist already done in VerifyCurrent, unless there was an exception if (exceptional) { @@ -914,36 +917,35 @@ namespace Microsoft.Boogie.Houdini { return null; } - private VCGen.Outcome TryCatchVerify(HoudiniVCGen vcgen, out List errors) { - VCGen.Outcome outcome; + private ProverInterface.Outcome TryCatchVerify(HoudiniVCGen vcgen, VCExpr axiom, out List errors) { + ProverInterface.Outcome outcome; try { - outcome = vcgen.Verify(out errors); + outcome = vcgen.Verify(axiom, out errors); } catch (VCGenException e) { Contract.Assume(e != null); errors = null; - outcome = VCGen.Outcome.Inconclusive; + outcome = ProverInterface.Outcome.Undetermined; } catch (UnexpectedProverOutputException upo) { Contract.Assume(upo != null); errors = null; - outcome = VCGen.Outcome.Inconclusive; + outcome = ProverInterface.Outcome.Undetermined; } return outcome; } //version of TryCatchVerify that spins on the same function //as long as the current assignment is changing - private VCGen.Outcome TrySpinSameFunc(HoudiniState current, + private ProverInterface.Outcome TrySpinSameFunc(HoudiniState current, Program program, HoudiniVCGen vcgen, out List errors, out bool exceptional) { Contract.Assert(current.Implementation != null); - VCGen.Outcome outcome; - bool pushed = false; + ProverInterface.Outcome outcome; errors = null; - outcome = VCGen.Outcome.Inconclusive; + outcome = ProverInterface.Outcome.Undetermined; try { bool trySameFunc = true; bool pastFirstIter = false; //see if this new loop is even helping @@ -953,14 +955,12 @@ namespace Microsoft.Boogie.Houdini { System.GC.Collect(); this.NotifyIteration(); } - Axiom currentAx = BuildAxiom(current.Assignment); + + this.vcgenSessions.TryGetValue(current.Implementation, out vcgen); + VCExpr currentAx = BuildAxiom(vcgen, current.Assignment); this.NotifyAssignment(current.Assignment); - vcgen.PushAxiom(currentAx); - pushed = true; - outcome = vcgen.Verify(out errors); - vcgen.Pop(); - pushed = false; + outcome = vcgen.Verify(currentAx, out errors); this.NotifyOutcome(outcome); DebugRefutedCandidates(current.Implementation, errors); @@ -975,7 +975,7 @@ namespace Microsoft.Boogie.Houdini { trySameFunc = UpdateAssignmentWorkList(current, outcome, errors); //reset for the next round errors = null; - outcome = VCGen.Outcome.Inconclusive; + outcome = ProverInterface.Outcome.Undetermined; } pastFirstIter = true; } while (trySameFunc && current.WorkList.Count > 0); @@ -983,18 +983,12 @@ namespace Microsoft.Boogie.Houdini { } catch (VCGenException e) { Contract.Assume(e != null); - if (pushed) { - vcgen.Pop(); // what if session is dead? - } NotifyException("VCGen"); exceptional = true; return outcome; } catch (UnexpectedProverOutputException upo) { Contract.Assume(upo != null); - if (pushed) { - vcgen.Pop(); - } NotifyException("UnexpectedProverOutput"); exceptional = true; return outcome; @@ -1004,16 +998,15 @@ namespace Microsoft.Boogie.Houdini { } //Similar to TrySpinSameFunc except no Candidate logic - private VCGen.Outcome HoudiniVerifyCurrentAux(HoudiniState current, + private ProverInterface.Outcome HoudiniVerifyCurrentAux(HoudiniState current, Program program, HoudiniVCGen vcgen, out List errors, out bool exceptional) { Contract.Assert(current.Implementation != null); - VCGen.Outcome outcome; - bool pushed = false; + ProverInterface.Outcome outcome; errors = null; - outcome = VCGen.Outcome.Inconclusive; + outcome = ProverInterface.Outcome.Undetermined; try { bool trySameFunc = true; bool pastFirstIter = false; //see if this new loop is even helping @@ -1024,15 +1017,11 @@ namespace Microsoft.Boogie.Houdini { this.NotifyIteration(); } - Axiom currentAx = BuildAxiom(current.Assignment); + VCExpr currentAx = BuildAxiom(vcgen, current.Assignment); this.NotifyAssignment(current.Assignment); //check the VC with the current assignment - vcgen.PushAxiom(currentAx); - pushed = true; - outcome = vcgen.Verify(out errors); - vcgen.Pop(); - pushed = false; + outcome = vcgen.Verify(currentAx, out errors); this.NotifyOutcome(outcome); DebugRefutedCandidates(current.Implementation, errors); @@ -1048,7 +1037,7 @@ namespace Microsoft.Boogie.Houdini { trySameFunc = UpdateAssignmentWorkList(current, outcome, errors); //reset for the next round errors = null; - outcome = VCGen.Outcome.Inconclusive; + outcome = ProverInterface.Outcome.Undetermined; } pastFirstIter = true; } while (trySameFunc && current.WorkList.Count > 0); @@ -1056,18 +1045,12 @@ namespace Microsoft.Boogie.Houdini { } catch (VCGenException e) { Contract.Assume(e != null); - if (pushed) { - vcgen.Pop(); // what if session is dead? - } NotifyException("VCGen"); exceptional = true; return outcome; } catch (UnexpectedProverOutputException upo) { Contract.Assume(upo != null); - if (pushed) { - vcgen.Pop(); - } NotifyException("UnexpectedProverOutput"); exceptional = true; return outcome; @@ -1080,9 +1063,9 @@ namespace Microsoft.Boogie.Houdini { public enum HoudiniOutcomeKind { Done, FatalError, VerificationCompleted } public class VCGenOutcome { - public VCGen.Outcome outcome; + public ProverInterface.Outcome outcome; public List errors; - public VCGenOutcome(VCGen.Outcome outcome, List errors) { + public VCGenOutcome(ProverInterface.Outcome outcome, List errors) { this.outcome = outcome; this.errors = errors; } @@ -1098,7 +1081,7 @@ namespace Microsoft.Boogie.Houdini { // statistics - private int CountResults(VCGen.Outcome outcome) { + private int CountResults(ProverInterface.Outcome outcome) { int outcomeCount = 0; foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values) { if (verifyOutcome.outcome == outcome) @@ -1107,7 +1090,7 @@ namespace Microsoft.Boogie.Houdini { return outcomeCount; } - private List ListOutcomeMatches(VCGen.Outcome outcome) { + private List ListOutcomeMatches(ProverInterface.Outcome outcome) { List result = new List(); foreach (KeyValuePair kvpair in implementationOutcomes) { if (kvpair.Value.outcome == outcome) @@ -1118,37 +1101,37 @@ namespace Microsoft.Boogie.Houdini { public int ErrorCount { get { - return CountResults(VCGen.Outcome.Errors); + return CountResults(ProverInterface.Outcome.Invalid); } } public int Verified { get { - return CountResults(VCGen.Outcome.Correct); + return CountResults(ProverInterface.Outcome.Valid); } } public int Inconclusives { get { - return CountResults(VCGen.Outcome.Inconclusive); + return CountResults(ProverInterface.Outcome.Undetermined); } } public int TimeOuts { get { - return CountResults(VCGen.Outcome.TimedOut); + return CountResults(ProverInterface.Outcome.TimeOut); } } public List ListOfTimeouts { get { - return ListOutcomeMatches(VCGen.Outcome.TimedOut); + return ListOutcomeMatches(ProverInterface.Outcome.TimeOut); } } public List ListOfInconclusives { get { - return ListOutcomeMatches(VCGen.Outcome.Inconclusive); + return ListOutcomeMatches(ProverInterface.Outcome.Undetermined); } } public List ListOfErrors { get { - return ListOutcomeMatches(VCGen.Outcome.Errors); + return ListOutcomeMatches(ProverInterface.Outcome.Invalid); } } } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index ff106380..87ab590d 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -164,8 +164,8 @@ namespace VC { Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullDictionaryAndValues(implName2LazyInliningInfo)); } - private Dictionary implName2LazyInliningInfo; - private GlobalVariable errorVariable; + protected Dictionary implName2LazyInliningInfo; + protected GlobalVariable errorVariable; public void GenerateVCsForLazyInlining(Program program) { Contract.Requires(program != null); diff --git a/Test/houdini/houd6.bpl b/Test/houdini/houd6.bpl index 09f2dd0e..820d2d73 100644 --- a/Test/houdini/houd6.bpl +++ b/Test/houdini/houd6.bpl @@ -41,4 +41,4 @@ modifies array; } // expected outcome: Correct -// expected assigment: bi->True forall i \ No newline at end of file +// expected assigment: bi->False forall i \ No newline at end of file -- cgit v1.2.3