summaryrefslogtreecommitdiff
path: root/Source/Houdini/Checker.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Houdini/Checker.cs')
-rw-r--r--Source/Houdini/Checker.cs108
1 files changed, 46 insertions, 62 deletions
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 661393ff..294f5d1b 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -9,35 +9,33 @@ using System.Collections.Generic;
using Microsoft.Boogie;
using Microsoft.Boogie.VCExprAST;
using Microsoft.Boogie.Simplify;
-using VC;
using Microsoft.Boogie.Z3;
using System.Collections;
using System.IO;
using System.Threading;
+using VC;
namespace Microsoft.Boogie.Houdini {
- public class HoudiniChecker {
+ class HoudiniChecker {
private Stack<VCExpr> axioms = new Stack<VCExpr>();
private Checker checker;
private string descriptiveName;
private VCExpr conjecture;
private ProverInterface.ErrorHandler handler;
-
- internal HoudiniChecker(Checker checker)
+
+ 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;
- }
-
- public void PrepareCheck(string _descriptiveName, VCExpr _vc, ProverInterface.ErrorHandler _handler)
- {
this.descriptiveName = _descriptiveName;
this.conjecture = _vc;
this.handler = _handler;
}
-
- public void PushAxiom(VCExpr vc) {
+
+ public void PushAxiom(Axiom axiom) {
+ DeclFreeProverContext proverContext = (DeclFreeProverContext) checker.TheoremProver.Context;
+ VCExpr vc = proverContext.BoogieExprTranslator.Translate(axiom.Expr);
axioms.Push(vc);
}
@@ -53,7 +51,7 @@ namespace Microsoft.Boogie.Houdini {
if (vc_axioms == null)
vc_axioms = axiom;
else
- vc_axioms = checker.VCExprGen.And(vc_axioms,axiom);
+ vc_axioms = checker.VCExprGen.And(vc_axioms, axiom);
}
return vc_axioms;
}
@@ -78,7 +76,6 @@ namespace Microsoft.Boogie.Houdini {
}
private ProverInterface.Outcome outcome;
- private UnexpectedProverOutputException outputExn;
public ProverInterface.Outcome ReadOutcome()
{
@@ -93,73 +90,61 @@ namespace Microsoft.Boogie.Houdini {
public class HoudiniVCGen : VCGen {
private HoudiniChecker hdnChecker;
- private VCExpressionGenerator gen;
- CounterexampleCollector collector = new CounterexampleCollector();
-
- public HoudiniVCGen(Program program, string logFilePath, bool appendLogFile)
- : base(program, logFilePath, appendLogFile)
- {
- }
-
- public void VerifyImplementation(Implementation impl, Program program) {
+ CounterexampleCollector collector;
+
+ public HoudiniVCGen(Program program, Implementation impl, string logFilePath, bool appendLogFile)
+ : base(program, logFilePath, appendLogFile) {
+ collector = new CounterexampleCollector();
collector.OnProgress("HdnVCGen", 0, 0, 0.0);
if (CommandLineOptions.Clo.SoundnessSmokeTest) {
throw new Exception("HoudiniVCGen does not support Soundness smoke test.");
}
-
+
ConvertCFG2DAG(impl, program);
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);
+ 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);
-
+
ErrorReporter reporter;
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
- reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, null, program);
- } else {
- reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, null, program);
+ reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, checker.TheoremProver.Context, program);
+ }
+ else {
+ reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, checker.TheoremProver.Context, program);
}
- this.gen = checker.VCExprGen;
if (checker.TheoremProver is Z3ProcessTheoremProver)
- this.hdnChecker = new HoudiniChecker(checker);
+ this.hdnChecker = new HoudiniChecker(checker, impl.Name, vc, reporter);
else
throw new Exception("HdnChecker only works with z3");
- this.hdnChecker.PrepareCheck(impl.Name, vc, reporter);
- this.hdnChecker.Check();
}
-
- public void PushAxiom(Axiom axiom)
- {
- Contract.Assume(hdnChecker != null);
- Contract.Assume(gen != null);
- //VCExpr vc = axiom.Expr.VCView(gen);
- //this.hdnChecker.PushAxiom(vc);
+
+ public void PushAxiom(Axiom axiom) {
+ this.hdnChecker.PushAxiom(axiom);
}
public void Pop() {
- Contract.Assume(hdnChecker!=null);
hdnChecker.Pop();
}
-
- public Outcome Verify(out List<Counterexample> errors)
- {
- Contract.Assume (hdnChecker != null);
+
+ public Outcome Verify(out List<Counterexample> errors) {
collector.examples.Clear();
hdnChecker.Check();
ProverInterface.Outcome proverOutcome;
proverOutcome = hdnChecker.ReadOutcome();
Outcome verifyOutcome = ReadOutcome(proverOutcome);
if (verifyOutcome == Outcome.Errors) {
- Contract.Assume (collector.examples != null);
+ Contract.Assume(collector.examples != null);
if (collector.examples.Count == 0) {
- string memStr = System.Convert.ToString(System.GC.GetTotalMemory(false));
- if (memStr != null)
- memStr = "?";
- throw new UnexpectedProverOutputException("Outcome.Errors w/ 0 counter examples. " + memStr + " memory used");
+ string memStr = System.Convert.ToString(System.GC.GetTotalMemory(false));
+ if (memStr != null)
+ memStr = "?";
+ throw new UnexpectedProverOutputException("Outcome.Errors w/ 0 counter examples. " + memStr + " memory used");
}
errors = collector.examples;
- } else {
+ }
+ else {
errors = null;
}
return verifyOutcome;
@@ -167,20 +152,19 @@ namespace Microsoft.Boogie.Houdini {
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.");
- }
+ 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.");
+ }
}
}
-
} \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 06:08:14 +0000