diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 12 | ||||
| -rw-r--r-- | Source/Houdini/Checker.cs | 134 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 199 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 4 | ||||
| -rw-r--r-- | 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<VCExpr> axioms = new Stack<VCExpr>();
+ 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<VCExpr> 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/*<int, Absy!>*/ 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<Counterexample> errors) {
+ public ProverInterface.Outcome Verify(VCExpr axiom, out List<Counterexample> 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<string, bool> 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<string, bool> 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<Implementation> BuildCallGraph() {
+ Graph<Implementation> callGraph = new Graph<Implementation>();
Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
foreach (Declaration decl in program.TopLevelDeclarations) {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ procToImpls[proc] = new HashSet<Implementation>();
+ }
+ 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<Implementation>();
+ callGraph.AddSource(impl);
procToImpls[impl.Proc].Add(impl);
}
- Graph<Implementation> callGraph = new Graph<Implementation>();
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<string, bool> currentAssignment, Boogie2VCExprTranslator exprTranslator) {
- Expr expr = new LiteralExpr(Token.NoToken, true);
- expr.Type = Type.Bool;
+ private VCExpr BuildAxiom(HoudiniVCGen vcgen, Dictionary<string, bool> currentAssignment) {
+ Boogie2VCExprTranslator exprTranslator = vcgen.BooogieExprTranslator;
+ VCExpressionGenerator exprGen = vcgen.VCExprGenerator;
+
+ VCExpr expr = VCExpressionGenerator.True;
foreach (KeyValuePair<string, bool> 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<string, bool> BuildAssignment(Dictionary<string, IdentifierExpr>.KeyCollection constants) {
@@ -374,20 +381,18 @@ namespace Microsoft.Boogie.Houdini { return initial;
}
- private VCGen.Outcome VerifyUsingAxiom(Implementation implementation, Axiom axiom, out List<Counterexample> errors) {
+ private ProverInterface.Outcome VerifyUsingAxiom(Implementation implementation, VCExpr axiom, out List<Counterexample> 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<Counterexample> 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<Counterexample> 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<Counterexample> errors) {
+ private bool IsOutcomeNotHoudini(ProverInterface.Outcome outcome, List<Counterexample> 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<Counterexample> errors) {
+ private bool AnyNonCandidateViolation(ProverInterface.Outcome outcome, List<Counterexample> 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<Counterexample> errors) {
string implName = implementation.ToString();
houdiniOutcome.implementationOutcomes.Remove(implName);
List<Counterexample> nonCandidateErrors = new List<Counterexample>();
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<Counterexample> 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<Counterexample> 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<Counterexample> 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<Counterexample> 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<Counterexample> 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<Counterexample> 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<Counterexample> errors) {
- VCGen.Outcome outcome;
+ private ProverInterface.Outcome TryCatchVerify(HoudiniVCGen vcgen, VCExpr axiom, out List<Counterexample> 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<Counterexample> 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<Counterexample> 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<Counterexample> errors;
- public VCGenOutcome(VCGen.Outcome outcome, List<Counterexample> errors) {
+ public VCGenOutcome(ProverInterface.Outcome outcome, List<Counterexample> 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<string> ListOutcomeMatches(VCGen.Outcome outcome) {
+ private List<string> ListOutcomeMatches(ProverInterface.Outcome outcome) {
List<string> result = new List<string>();
foreach (KeyValuePair<string, VCGenOutcome> 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<string> ListOfTimeouts {
get {
- return ListOutcomeMatches(VCGen.Outcome.TimedOut);
+ return ListOutcomeMatches(ProverInterface.Outcome.TimeOut);
}
}
public List<string> ListOfInconclusives {
get {
- return ListOutcomeMatches(VCGen.Outcome.Inconclusive);
+ return ListOutcomeMatches(ProverInterface.Outcome.Undetermined);
}
}
public List<string> 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<string, LazyInliningInfo> implName2LazyInliningInfo;
- private GlobalVariable errorVariable;
+ protected Dictionary<string, LazyInliningInfo> 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 |