diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Graph/Graph.cs | 5 | ||||
| -rw-r--r-- | Source/Houdini/AssemblyInfo.ssc | 4 | ||||
| -rw-r--r-- | Source/Houdini/Checker.cs | 108 | ||||
| -rw-r--r-- | Source/Houdini/Checker.ssc | 460 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 2026 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.ssc | 1188 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.sscproj | 118 |
7 files changed, 1058 insertions, 2851 deletions
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 99df97cd..21336545 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -344,7 +344,6 @@ namespace Graphing { Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Item2 != null && p.Item1 != null));
}
-
private class PreHeader {
Node/*!*/ myHeader;
[ContractInvariantMethod]
@@ -464,7 +463,7 @@ namespace Graphing { }
}
- internal IEnumerable<Node> Predecessors(Node n) {
+ public IEnumerable<Node> Predecessors(Node n) {
// original A#
//Set<Node> result = Set{ x : x in Nodes, Edge(x,n) };
@@ -472,7 +471,7 @@ namespace Graphing { return predCache[n];
}
- internal IEnumerable<Node> Successors(Node n) {
+ public IEnumerable<Node> Successors(Node n) {
ComputePredSuccCaches();
return succCache[n];
}
diff --git a/Source/Houdini/AssemblyInfo.ssc b/Source/Houdini/AssemblyInfo.ssc deleted file mode 100644 index 6ed99a25..00000000 --- a/Source/Houdini/AssemblyInfo.ssc +++ /dev/null @@ -1,4 +0,0 @@ -using System.Reflection;
-using System.Runtime.CompilerServices;
-
-[assembly: AssemblyKeyFile("..\\InterimKey.snk")]
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 diff --git a/Source/Houdini/Checker.ssc b/Source/Houdini/Checker.ssc deleted file mode 100644 index 03c2beda..00000000 --- a/Source/Houdini/Checker.ssc +++ /dev/null @@ -1,460 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using Microsoft.Contracts;
-using System.Collections.Generic;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify.AST;
-using VC;
-using Microsoft.Boogie.Z3;
-using Microsoft.AbstractInterpretationFramework;
-using Microsoft.Boogie.AbstractInterpretation;
-using System.Collections;
-using System.Compiler;
-using System.IO;
-using System.Threading;
-
-namespace Microsoft.Boogie.Houdini {
-
- public abstract class HdnCheckerFactory {
- public static HdnChecker! BuildHdnChecker(Checker! checker) {
- if (checker.TheoremProver is Z3ThreadTheoremProver)
- return new HoudiniZ3ApiChecker(checker);
- else if (checker.TheoremProver is Z3ProcessTheoremProver) {
- if (CommandLineOptions.Clo.houdiniFlags.incremental) {
- return new HoudiniZ3CheckerIncr(checker);
- } else {
- return new HoudiniZ3Checker(checker);
- }
- } else
- throw new Exception("HdnChecker only works with z3");
- }
- }
-
- public abstract class HdnChecker {
- public abstract void PrepareCheck(string! _descriptiveName,
- VCExpr! _vc, ProverInterface.ErrorHandler! _handler);
- public abstract void PushAxiom(VCExpr! vc);
- public abstract void Pop();
- public abstract void Check();
- public abstract ProverInterface.Outcome ReadOutcome()
- throws UnexpectedProverOutputException;
- }
-
- public class HoudiniZ3ApiChecker:HdnChecker {
-
- private Z3ThreadTheoremProver! z3prover;
-
- private ProverInterface.ErrorHandler handler;
- private ProverInterface.Outcome outcome;
- private UnexpectedProverOutputException outputExn;
-
- internal HoudiniZ3ApiChecker(Checker! checker)
- requires checker.TheoremProver!=null;
- requires checker.TheoremProver is Z3ThreadTheoremProver;
- {
- this.z3prover = (Z3ThreadTheoremProver)checker.TheoremProver;
- }
-
- public override void PrepareCheck(string! _descriptiveName, VCExpr! _vc, ProverInterface.ErrorHandler! _handler) {
- handler = _handler;
- z3prover.LogComment(_descriptiveName);
- z3prover.PrepareCheck(_descriptiveName,_vc);
- }
-
- public override void PushAxiom(VCExpr! vc) {
- z3prover.PushAxiom(vc);
- }
-
- public override void Pop() {
- z3prover.Pop();
- }
-
- public override void Check() {
- z3prover.BeginPreparedCheck();
- try {
- outcome = z3prover.CheckOutcome((!)handler);
- } catch (UnexpectedProverOutputException e) {
- outputExn = e;
- }
- }
-
- public override ProverInterface.Outcome ReadOutcome()
- throws UnexpectedProverOutputException;
- {
- if (outputExn != null) {
- throw outputExn;
- }
- return outcome;
- }
- }
-
- // version of Z3PTP exposing more of the prover process functionality
- public class Z3ProcessTPExposed : Z3ProcessTheoremProver {
-
- [NotDelayed]
- public Z3ProcessTPExposed (TextWriter/*?*/ logFileWriter, VCExpressionGenerator! gen, DeclFreeProverContext! ctx, int timeout, bool typed)
- throws UnexpectedProverOutputException;
- {
- base(logFileWriter, gen, ctx, timeout, typed, "z3.exe");
- }
-
-
- //MOVED Directly Z3 ProverInterface for now...
- //To introduce this cleanly, need to add a new subproject under Provers
- //and must use the commandline option for that, instead of saying /prover:z3
- //That way, the class is constructed in class Checker the same way
- //all the other provers are constructed
-
- }
-
- public class Z3ExposedFactory : Z3.Factory {
-
- }
-
-
- //Old version
- public class HoudiniZ3Checker:HdnChecker {
- private Stack<VCExpr!>! axioms = new Stack<VCExpr!>();
- private Checker! checker;
- private string descriptiveName;
- private VCExpr conjecture;
- private ProverInterface.ErrorHandler handler;
-
- internal HoudiniZ3Checker(Checker! checker)
- requires checker.TheoremProver!=null;
- requires checker.TheoremProver is Z3ProcessTheoremProver;
- {
- this.checker = checker;
- }
-
- public override void PrepareCheck(string! _descriptiveName, VCExpr! _vc, ProverInterface.ErrorHandler! _handler)
- {
- this.descriptiveName = _descriptiveName;
- this.conjecture = _vc;
- this.handler = _handler;
- }
- public override void PushAxiom(VCExpr! vc) {
- axioms.Push(vc);
- }
- public override void Pop() {
- axioms.Pop();
- }
- private VCExpr! BuildVCAxioms(Stack<VCExpr!>! axioms)
- 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 override void Check()
- {
- assert (descriptiveName!=null);
- assert (conjecture!=null);
- 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;
-
- checker.BeginCheck(descriptiveName,vc,handler);
- WaitHandle.WaitAny(new WaitHandle[] {checker.ProverDone});
- }
-
- private ProverInterface.Outcome outcome;
- private UnexpectedProverOutputException outputExn;
-
- public override ProverInterface.Outcome ReadOutcome()
- throws UnexpectedProverOutputException;
- {
- try {
- outcome = checker.ReadOutcome();
- } catch (UnexpectedProverOutputException e) {
- throw e;
- }
- return outcome;
- }
- }
-
- //new version
- public class HoudiniZ3CheckerIncr:HdnChecker {
- private Checker! checker;
- private string descriptiveName;
- private VCExpr conjecture;
- private ProverInterface.ErrorHandler handler;
-
- // Hack to delay the exception throwing (from Push/Pop...) for now
- private UnexpectedProverOutputException delayedExc;
- private Z3ProcessTheoremProver! thmProver;
-
- internal HoudiniZ3CheckerIncr(Checker! checker)
- requires checker.TheoremProver!=null;
- requires checker.TheoremProver is Z3ProcessTheoremProver;
- {
- this.checker = checker;
- this.thmProver = (Z3ProcessTheoremProver!)checker.TheoremProver;
- }
-
- private void delayException(UnexpectedProverOutputException exc) {
- if (delayedExc == null) { delayedExc = exc; }
- }
-
- public override void PrepareCheck(string! _descriptiveName, VCExpr! _vc,
- ProverInterface.ErrorHandler! _handler)
- {
- this.descriptiveName = _descriptiveName;
- this.conjecture = _vc;
- this.handler = _handler;
- this.thmProver.LogComment(_descriptiveName);
- try {
- this.thmProver.PrepareCheck(_descriptiveName,_vc);
- } catch (UnexpectedProverOutputException exc) {
- delayException(exc);
- }
- }
- public override void PushAxiom(VCExpr! vc) {
- string! vcStr = vc.ToString();
- try {
- thmProver.PushAxioms(vcStr);
- } catch (UnexpectedProverOutputException exc) {
- delayException(exc);
- }
- }
- public override void Pop() {
- try {
- thmProver.PopAxioms();
- } catch (UnexpectedProverOutputException exc) {
- delayException(exc);
- }
- }
-
- public override void Check()
- {
- assert (descriptiveName!=null);
- assert (conjecture!=null);
- assert (handler!=null);
- outcome = ProverInterface.Outcome.Undetermined;
-
- VCExpr! vc = checker.VCExprGen.False;
- checker.BeginCheck(descriptiveName,vc,handler);
- WaitHandle.WaitAny(new WaitHandle[] {checker.ProverDone});
- }
-
- private ProverInterface.Outcome outcome;
- private UnexpectedProverOutputException outputExn;
-
- public override ProverInterface.Outcome ReadOutcome()
- throws UnexpectedProverOutputException;
- {
- // HACK
- if (delayedExc != null) {
- UnexpectedProverOutputException temp = delayedExc;
- delayedExc = null;
- throw temp;
- }
- // Normal stuff
- try {
- outcome = checker.ReadOutcome();
- } catch (UnexpectedProverOutputException e) {
- throw e;
- }
- return outcome;
- }
- }
-
- public abstract class HdnVCGenFactory {
- public abstract HdnVCGen! BuildVCGen(Program! program, string logFilePath, bool appendLogFile);
- }
- public class Z3APIHdnVCGenFactory:HdnVCGenFactory {
- public override HdnVCGen! BuildVCGen(Program! program, string logFilePath, bool appendLogFile) {
- return new Z3ApiHdnVCGen(program, logFilePath, appendLogFile);
- }
- }
- public class Z3HdnVCGenFactory:HdnVCGenFactory {
- public override HdnVCGen! BuildVCGen(Program! program, string logFilePath, bool appendLogFile) {
- return new Z3HdnVCGen(program, logFilePath, appendLogFile);
- }
- }
-
- public abstract class HdnVCGen {
- public abstract void PrepareVerification(Implementation! impl, Program! program);
- public abstract void PushAxiom(Axiom! axiom);
- public abstract void Pop();
- public abstract VC.VCGen.Outcome Verify(out List<Counterexample!>? errors)
- throws UnexpectedProverOutputException;
-
- }
-
- public class Z3HdnVCGen: HdnVCGen {
- private Program! program;
- private string logFilePath;
- private bool appendLogFile;
- private Implementation implementation;
- private Axiom axiom;
-
- private ExtVCGen vcgen;
-
- public Z3HdnVCGen(Program! program, string logFilePath, bool appendLogFile) {
- this.program = program;
- this.logFilePath = logFilePath;
- this.appendLogFile= appendLogFile;
- }
-
- public override void PrepareVerification(Implementation! impl, Program! program) {
- this.implementation = impl;
- this.program = program;
- this.vcgen = new ExtVCGen(program,logFilePath,appendLogFile);
- this.vcgen.PrepareVerification(this.implementation,this.program);
- //watch out for > 1 call -- don't want CFG conversion to happen too many times!!!
- }
-
- public override void PushAxiom(Axiom! axiom) {
- assert this.vcgen != null;
- this.axiom=axiom;
- this.vcgen.PushAxiom(this.axiom);
- }
-
- public override void Pop() {
- assert this.vcgen != null;
- this.vcgen.Pop();
- this.axiom = null;
- }
-
- public override VC.VCGen.Outcome Verify(out List<Counterexample!>? errors)
- throws UnexpectedProverOutputException; {
- assert(this.vcgen!=null);
-
- return vcgen.Verify(out errors);
- }
-
- }
-
- public class Z3ApiHdnVCGen: HdnVCGen {
- private ExtVCGen! vcgen;
-
- public Z3ApiHdnVCGen(Program! program, string logFilePath, bool appendLogFile) {
- this.vcgen = new ExtVCGen(program,logFilePath,appendLogFile);
- }
-
- public override void PrepareVerification(Implementation! impl, Program! program) {
- vcgen.PrepareVerification(impl,program);
- }
-
- public override void PushAxiom(Axiom! axiom) {
- vcgen.PushAxiom(axiom);
- }
-
- public override void Pop() {
- vcgen.Pop();
- }
-
- public override VC.VCGen.Outcome Verify(out List<Counterexample!>? errors)
- throws UnexpectedProverOutputException; {
- return vcgen.Verify(out errors);
- }
-
- }
-
-
-
- public class ExtVCGen : VCGen {
-
- private HdnChecker hdnChecker;
- private VCExpressionGenerator gen;
- CounterexampleCollector! collector = new CounterexampleCollector();
-
- public ExtVCGen(Program! program, string logFilePath, bool appendLogFile) {
- base(program,logFilePath,appendLogFile);
- }
-
- public void PrepareVerification(Implementation! impl, Program! program) {
- collector.OnProgress("HdnVCGen", 0, 0, 0.0);
- if (CommandLineOptions.Clo.SoundnessSmokeTest) {
- throw new Exception("HoudiniVCGen does not support Soundness smoke test.");
- }
-
- ConvertCFG2DAG(impl, program);
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program);
- Hashtable/*<int, Absy!>*/! label2absy;
- Checker! checker = new Checker(program, this.logFilePath, this.appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime);
- VCExpr! vc = GenerateVC(impl, out label2absy, checker);
-
- ErrorReporter reporter;
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
- reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector);
- } else {
- reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector);
- }
- this.gen = checker.VCExprGen;
- this.hdnChecker = HdnCheckerFactory.BuildHdnChecker(checker);
- this.hdnChecker.PrepareCheck((!) impl.Name, vc, reporter);
- }
-
-
- public void PushAxiom(Axiom! axiom)
- {
- assume (hdnChecker!=null);
- assume (gen!=null);
- VCExpr vc = axiom.Expr.VCView(gen);
- this.hdnChecker.PushAxiom(vc);
- }
- public void Pop() {
- assume (hdnChecker!=null);
- hdnChecker.Pop();
- }
-
- public Outcome Verify(out List<Counterexample!>? errors)
- throws UnexpectedProverOutputException; {
- assume (hdnChecker!=null);
- collector.examples.Clear();
- hdnChecker.Check();
- ProverInterface.Outcome proverOutcome;
- proverOutcome = hdnChecker.ReadOutcome();
- Outcome verifyOutcome = ReadOutcome(proverOutcome);
- if (verifyOutcome == Outcome.Errors) {
- 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");
- }
- errors = collector.examples;
- } 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.");
- }
- }
-
- }
-
-
-}
\ No newline at end of file diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 6dc58dde..c3b302e7 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -15,1064 +15,1058 @@ using System.IO; using Microsoft.AbstractInterpretationFramework;
using Graphing;
-namespace Microsoft.Boogie.Houdini
-{
+namespace Microsoft.Boogie.Houdini {
- class ReadOnlyDictionary<K,V> {
- private Dictionary<K,V> dictionary;
- public ReadOnlyDictionary(Dictionary<K,V> dictionary) {
- this.dictionary = dictionary;
- }
-
- public Dictionary<K,V>.KeyCollection Keys {
- get { return this.dictionary.Keys; }
- }
-
- public bool TryGetValue(K k, out V v) {
- return this.dictionary.TryGetValue(k, out v);
- }
+ class ReadOnlyDictionary<K, V> {
+ private Dictionary<K, V> dictionary;
+ public ReadOnlyDictionary(Dictionary<K, V> dictionary) {
+ this.dictionary = dictionary;
+ }
+
+ public Dictionary<K, V>.KeyCollection Keys {
+ get { return this.dictionary.Keys; }
+ }
+
+ public bool TryGetValue(K k, out V v) {
+ return this.dictionary.TryGetValue(k, out v);
+ }
- public bool ContainsKey(K k) {
- return this.dictionary.ContainsKey(k);
- }
- }
-
- public class CallGraph {
- Graph<Implementation> callGraph;
- public CallGraph() {
- //this.callGraph = null;
- }
-
- public IEnumerable PreviousNodes(Implementation n) {
- //return this.callGraph.PreviousNodes(n);
- return null;
- }
- public IEnumerable NextNodes(Implementation n) {
- //return this.callGraph.NextNodes(n);
- return null;
- }
-
- }
-
- public abstract class HoudiniObserver {
- public virtual void UpdateStart(Program program, int numConstants) {}
- 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 UpdateEnqueue(Implementation implementation) {}
- public virtual void UpdateDequeue() {}
- public virtual void UpdateConstant(string constantName) {}
- public virtual void UpdateEnd(bool isNormalEnd) {}
- public virtual void UpdateFlushStart() {}
- public virtual void UpdateFlushFinish() {}
- public virtual void SeeException(string msg){}
- }
-
- public class IterationTimer <K> {
- private Dictionary<K, List<double>> times;
-
- public IterationTimer () {
- times = new Dictionary<K, List<double>>();
- }
-
- public void AddTime(K key, double timeMS) {
- List<double> oldList;
- times.TryGetValue(key, out oldList);
- if (oldList == null) {
- oldList = new List<double>();
- } else {
- times.Remove(key);
+ public bool ContainsKey(K k) {
+ return this.dictionary.ContainsKey(k);
+ }
+ }
+
+ public abstract class HoudiniObserver {
+ public virtual void UpdateStart(Program program, int numConstants) { }
+ 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 UpdateEnqueue(Implementation implementation) { }
+ public virtual void UpdateDequeue() { }
+ public virtual void UpdateConstant(string constantName) { }
+ public virtual void UpdateEnd(bool isNormalEnd) { }
+ public virtual void UpdateFlushStart() { }
+ public virtual void UpdateFlushFinish() { }
+ public virtual void SeeException(string msg) { }
+ }
+
+ public class IterationTimer<K> {
+ private Dictionary<K, List<double>> times;
+
+ public IterationTimer() {
+ times = new Dictionary<K, List<double>>();
+ }
+
+ public void AddTime(K key, double timeMS) {
+ List<double> oldList;
+ times.TryGetValue(key, out oldList);
+ if (oldList == null) {
+ oldList = new List<double>();
+ }
+ else {
+ times.Remove(key);
+ }
+ oldList.Add(timeMS);
+ times.Add(key, oldList);
+ }
+
+ public void PrintTimes(TextWriter wr) {
+ wr.WriteLine("Total procedures: {0}", times.Count);
+ double total = 0;
+ int totalIters = 0;
+ foreach (KeyValuePair<K, List<double>> kv in times) {
+ int curIter = 0;
+ wr.WriteLine("Times for {0}:", kv.Key);
+ foreach (double v in kv.Value) {
+ wr.WriteLine(" ({0})\t{1}ms", curIter, v);
+ total += v;
+ curIter++;
}
- oldList.Add(timeMS);
- times.Add(key, oldList);
- }
-
- public void PrintTimes(TextWriter wr) {
- wr.WriteLine ("Total procedures: {0}", times.Count);
- double total = 0;
- int totalIters = 0;
- foreach(KeyValuePair<K, List<double>> kv in times) {
- int curIter = 0;
- wr.WriteLine("Times for {0}:", kv.Key);
- foreach(double v in kv.Value) {
- wr.WriteLine(" ({0})\t{1}ms", curIter, v);
- total += v;
- curIter++;
+ totalIters += curIter;
+ }
+ total = total / 1000.0;
+ wr.WriteLine("Total time: {0} (s)", total);
+ wr.WriteLine("Avg: {0} (s/iter)", total / totalIters);
+ }
+ }
+
+ public class HoudiniTimer : HoudiniObserver {
+ private DateTime startT;
+ private Implementation curImp;
+ private IterationTimer<string> times;
+ private TextWriter wr;
+
+ public HoudiniTimer(TextWriter wr) {
+ this.wr = wr;
+ times = new IterationTimer<string>();
+ }
+ public override void UpdateIteration() {
+ startT = DateTime.Now;
+ }
+ public override void UpdateImplementation(Implementation implementation) {
+ curImp = implementation;
+ }
+ public override void UpdateOutcome(VCGen.Outcome o) {
+ Contract.Assert(curImp != null);
+ DateTime endT = DateTime.Now;
+ times.AddTime(curImp.Name, (endT - startT).TotalMilliseconds); // assuming names are unique
+ }
+ public void PrintTimes() {
+ wr.WriteLine("-----------------------------------------");
+ wr.WriteLine("Times for each iteration for each procedure");
+ wr.WriteLine("-----------------------------------------");
+ times.PrintTimes(wr);
+ }
+ }
+
+ public class HoudiniTextReporter : HoudiniObserver {
+ private TextWriter wr;
+ private int currentIteration = -1;
+
+ public HoudiniTextReporter(TextWriter wr) {
+ this.wr = wr;
+ }
+ public override void UpdateStart(Program program, int numConstants) {
+ wr.WriteLine("Houdini started:" + program.ToString() + " #constants: " + numConstants.ToString());
+ currentIteration = -1;
+ wr.Flush();
+ }
+ public override void UpdateIteration() {
+ currentIteration++;
+ wr.WriteLine("---------------------------------------");
+ wr.WriteLine("Houdini iteration #" + currentIteration);
+ wr.Flush();
+ }
+ public override void UpdateImplementation(Implementation implementation) {
+ wr.WriteLine("implementation under analysis :" + implementation.Name);
+ wr.Flush();
+ }
+ public override void UpdateAssignment(Dictionary<string, bool> assignment) {
+ bool firstTime = true;
+ wr.Write("assignment under analysis : axiom (");
+ foreach (KeyValuePair<string, bool> kv in assignment) {
+ if (!firstTime) wr.Write(" && "); else firstTime = false;
+ string valString; // ugliness to get it lower cased
+ if (kv.Value) valString = "true"; else valString = "false";
+ wr.Write(kv.Key + " == " + valString);
+ }
+ wr.WriteLine(");");
+ wr.Flush();
+ }
+ public override void UpdateOutcome(VCGen.Outcome outcome) {
+ wr.WriteLine("analysis outcome :" + outcome);
+ wr.Flush();
+ }
+ public override void UpdateEnqueue(Implementation implementation) {
+ wr.WriteLine("worklist enqueue :" + implementation.Name);
+ wr.Flush();
+ }
+ public override void UpdateDequeue() {
+ wr.WriteLine("worklist dequeue");
+ wr.Flush();
+ }
+ public override void UpdateConstant(string constantName) {
+ wr.WriteLine("constant disabled : " + constantName);
+ wr.Flush();
+ }
+ public override void UpdateEnd(bool isNormalEnd) {
+ wr.WriteLine("Houdini ended: " + (isNormalEnd ? "Normal" : "Abnormal"));
+ wr.WriteLine("Number of iterations: " + (this.currentIteration + 1));
+ wr.Flush();
+ }
+ public override void UpdateFlushStart() {
+ wr.WriteLine("***************************************");
+ wr.WriteLine("Flushing remaining implementations");
+ wr.Flush();
+ }
+ public override void UpdateFlushFinish() {
+ wr.WriteLine("***************************************");
+ wr.WriteLine("Flushing finished");
+ wr.Flush();
+ }
+ public override void SeeException(string msg) {
+ wr.WriteLine("Caught exception: " + msg);
+ wr.Flush();
+ }
+
+ }
+
+
+ public abstract class ObservableHoudini {
+ private List<HoudiniObserver> observers = new List<HoudiniObserver>();
+
+ public void AddObserver(HoudiniObserver observer) {
+ if (!observers.Contains(observer))
+ observers.Add(observer);
+ }
+ private delegate void NotifyDelegate(HoudiniObserver observer);
+
+ private void Notify(NotifyDelegate notifyDelegate) {
+ foreach (HoudiniObserver observer in observers) {
+ notifyDelegate(observer);
+ }
+ }
+ protected void NotifyStart(Program program, int numConstants) {
+ NotifyDelegate notifyDelegate = (NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateStart(program, numConstants); };
+ Notify(notifyDelegate);
+ }
+ protected void NotifyIteration() {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateIteration(); });
+ }
+ protected void NotifyImplementation(Implementation implementation) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateImplementation(implementation); });
+ }
+ protected void NotifyAssignment(Dictionary<string, bool> assignment) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateAssignment(assignment); });
+ }
+ protected void NotifyOutcome(VCGen.Outcome outcome) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateOutcome(outcome); });
+ }
+ protected void NotifyEnqueue(Implementation implementation) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateEnqueue(implementation); });
+ }
+ protected void NotifyDequeue() {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateDequeue(); });
+ }
+ protected void NotifyConstant(string constantName) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateConstant(constantName); });
+ }
+ protected void NotifyEnd(bool isNormalEnd) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateEnd(isNormalEnd); });
+ }
+ protected void NotifyFlushStart() {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateFlushStart(); });
+ }
+ protected void NotifyFlushFinish() {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateFlushFinish(); });
+ }
+
+ protected void NotifyException(string msg) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.SeeException(msg); });
+ }
+ }
+
+ public class Houdini : ObservableHoudini {
+ private Program program;
+ private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;
+ private ReadOnlyDictionary<Implementation, HoudiniVCGen> vcgenSessions;
+ private Graph<Implementation> callGraph;
+ private bool continueAtError;
+
+ public Houdini(Program program, bool continueAtError) {
+ this.program = program;
+ this.callGraph = BuildCallGraph(program);
+ this.continueAtError = continueAtError;
+ this.houdiniConstants = CollectExistentialConstants(program);
+ this.vcgenSessions = PrepareVCGenSessions(program);
+ }
+
+ private ReadOnlyDictionary<Implementation, HoudiniVCGen> PrepareVCGenSessions(Program program) {
+ Dictionary<Implementation, HoudiniVCGen> vcgenSessions = new Dictionary<Implementation, HoudiniVCGen>();
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Implementation impl = decl as Implementation;
+ if (impl != null) {
+ // make a different simplify log file for each function
+ String simplifyLog = null;
+ if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
+ simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
}
- totalIters += curIter;
+ HoudiniVCGen vcgen = new HoudiniVCGen(program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ vcgenSessions.Add(impl, vcgen);
}
- total = total / 1000.0;
- wr.WriteLine ("Total time: {0} (s)", total);
- wr.WriteLine ("Avg: {0} (s/iter)", total/totalIters);
- }
- }
-
- public class HoudiniTimer : HoudiniObserver {
- private DateTime startT;
- private Implementation curImp;
- private IterationTimer<string> times;
- private TextWriter wr;
-
- public HoudiniTimer(TextWriter wr) {
- this.wr = wr;
- times = new IterationTimer<string>();
- }
- public override void UpdateIteration() {
- startT = DateTime.Now;
- }
- public override void UpdateImplementation(Implementation implementation){
- curImp = implementation;
- }
- public override void UpdateOutcome (VCGen.Outcome o) {
- Contract.Assert(curImp != null);
- DateTime endT = DateTime.Now;
- times.AddTime(curImp.Name, (endT - startT).TotalMilliseconds); // assuming names are unique
- }
- public void PrintTimes() {
- wr.WriteLine("-----------------------------------------");
- wr.WriteLine("Times for each iteration for each procedure");
- wr.WriteLine("-----------------------------------------");
- times.PrintTimes(wr);
- }
- }
-
- public class HoudiniTextReporter: HoudiniObserver {
- private TextWriter wr;
- private int currentIteration = -1;
-
- public HoudiniTextReporter(TextWriter wr) {
- this.wr = wr;
- }
- public override void UpdateStart(Program program, int numConstants) {
- wr.WriteLine("Houdini started:" + program.ToString() + " #constants: " + numConstants.ToString());
- currentIteration = -1;
- wr.Flush();
- }
- public override void UpdateIteration() {
- currentIteration++;
- wr.WriteLine("---------------------------------------");
- wr.WriteLine("Houdini iteration #" + currentIteration);
- wr.Flush();
- }
- public override void UpdateImplementation(Implementation implementation){
- wr.WriteLine("implementation under analysis :" + implementation.Name);
- wr.Flush();
- }
- public override void UpdateAssignment(Dictionary<string,bool> assignment) {
- bool firstTime = true;
- wr.Write("assignment under analysis : axiom (");
- foreach (KeyValuePair<string,bool> kv in assignment) {
- if (!firstTime) wr.Write(" && "); else firstTime = false;
- string valString; // ugliness to get it lower cased
- if (kv.Value) valString = "true"; else valString = "false";
- wr.Write(kv.Key + " == " + valString);
- }
- wr.WriteLine(");");
- wr.Flush();
- }
- public override void UpdateOutcome(VCGen.Outcome outcome) {
- wr.WriteLine("analysis outcome :" + outcome);
- wr.Flush();
- }
- public override void UpdateEnqueue(Implementation implementation) {
- wr.WriteLine("worklist enqueue :" + implementation.Name);
- wr.Flush();
- }
- public override void UpdateDequeue() {
- wr.WriteLine("worklist dequeue");
- wr.Flush();
- }
- public override void UpdateConstant(string constantName) {
- wr.WriteLine("constant disabled : " + constantName);
- wr.Flush();
- }
- public override void UpdateEnd(bool isNormalEnd) {
- wr.WriteLine("Houdini ended: " + (isNormalEnd ? "Normal" : "Abnormal"));
- wr.WriteLine("Number of iterations: " + (this.currentIteration+1));
- wr.Flush();
- }
- public override void UpdateFlushStart() {
- wr.WriteLine("***************************************");
- wr.WriteLine("Flushing remaining implementations");
- wr.Flush();
- }
- public override void UpdateFlushFinish() {
- wr.WriteLine("***************************************");
- wr.WriteLine("Flushing finished");
- wr.Flush();
- }
- public override void SeeException(string msg) {
- wr.WriteLine("Caught exception: " + msg);
- wr.Flush();
- }
-
- }
-
-
- public abstract class ObservableHoudini {
- private List<HoudiniObserver> observers = new List<HoudiniObserver>();
-
- public void AddObserver(HoudiniObserver observer) {
- if (!observers.Contains(observer))
- observers.Add(observer);
- }
- private delegate void NotifyDelegate(HoudiniObserver observer);
-
- private void Notify(NotifyDelegate notifyDelegate) {
- foreach (HoudiniObserver observer in observers) {
- notifyDelegate(observer);
+ }
+ return new ReadOnlyDictionary<Implementation, HoudiniVCGen>(vcgenSessions);
+ }
+
+ private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants(Program program) {
+ Dictionary<string, IdentifierExpr> existentialConstants = new Dictionary<string, IdentifierExpr>();
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Constant constant = decl as Constant;
+ if (constant != null) {
+ bool result = false;
+ if (constant.CheckBooleanAttribute("existential", ref result)) {
+ if (result == true)
+ existentialConstants.Add(constant.Name, new IdentifierExpr(Token.NoToken, constant));
+ }
}
}
- protected void NotifyStart(Program program, int numConstants) {
- NotifyDelegate notifyDelegate = (NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateStart(program, numConstants); };
- Notify(notifyDelegate);
+ return new ReadOnlyDictionary<string, IdentifierExpr>(existentialConstants);
+ }
+
+ private Graph<Implementation> BuildCallGraph(Program program) {
+ Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, 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>();
+ procToImpls[impl.Proc].Add(impl);
}
- protected void NotifyIteration() {
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateIteration(); });
+ Graph<Implementation> callGraph = new Graph<Implementation>();
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ foreach (Block b in impl.Blocks) {
+ foreach (Cmd c in b.Cmds) {
+ CallCmd cc = c as CallCmd;
+ if (cc == null) continue;
+ foreach (Implementation callee in procToImpls[cc.Proc]) {
+ callGraph.AddEdge(impl, callee);
+ }
+ }
+ }
}
- protected void NotifyImplementation(Implementation implementation) {
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateImplementation(implementation); });
+ return callGraph;
+ }
+
+ private Queue<Implementation> BuildWorkList(Program program) {
+ Queue<Implementation> queue = new Queue<Implementation>();
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Implementation impl = decl as Implementation;
+ if (impl != null) {
+ queue.Enqueue(impl);
+ }
}
- protected void NotifyAssignment(Dictionary<string,bool> assignment) {
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateAssignment(assignment); });
+ return queue;
+ }
+
+ private bool MatchCandidate(Expr boogieExpr, out string candidateConstant) {
+ candidateConstant = null;
+ IExpr antecedent;
+ IExpr expr = boogieExpr as IExpr;
+ if (expr != null && ExprUtil.Match(expr, Prop.Implies, out antecedent)) {
+ IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;
+ if (constantFunApp != null && houdiniConstants.ContainsKey(constantFunApp.IdentifierExpr.Name)) {
+ candidateConstant = constantFunApp.IdentifierExpr.Name;
+ return true;
+ }
}
- protected void NotifyOutcome(VCGen.Outcome outcome) {
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateOutcome(outcome); });
+ return false;
+ }
+
+ private Axiom BuildAxiom(Dictionary<string, bool> currentAssignment) {
+ Expr axiom = new LiteralExpr(Token.NoToken, 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);
+ Expr constantAssignment = Expr.Binary(Token.NoToken, BinaryOperator.Opcode.Eq, constantExpr, valueExpr);
+ axiom = Expr.Binary(Token.NoToken, BinaryOperator.Opcode.And, axiom, constantAssignment);
}
- protected void NotifyEnqueue(Implementation implementation){
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateEnqueue(implementation); });
+ return new Axiom(Token.NoToken, axiom);
+ }
+
+ private Dictionary<string, bool> BuildAssignment(Dictionary<string, IdentifierExpr>.KeyCollection constants) {
+ Dictionary<string, bool> initial = new Dictionary<string, bool>();
+ foreach (string constant in constants)
+ initial.Add(constant, true);
+ return initial;
+ }
+
+ private VCGen.Outcome VerifyUsingAxiom(Implementation implementation, Axiom 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();
+ return outcome;
+ }
+
+ // the main procedure that checks a procedure and updates the
+ // assignment and the worklist
+ private VCGen.Outcome HoudiniVerifyCurrent(HoudiniState current,
+ Program program,
+ out List<Counterexample> errors,
+ out bool exc) {
+ HoudiniVCGen vcgen;
+ if (current.Implementation == null)
+ throw new Exception("HoudiniVerifyCurrent has null implementation");
+
+ Implementation implementation = current.Implementation;
+ vcgenSessions.TryGetValue(implementation, out vcgen);
+ if (vcgen == null)
+ throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
+
+ VCGen.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc);
+ return outcome;
+ }
+
+ private VCGen.Outcome VerifyCurrent(HoudiniState current,
+ Program program,
+ out List<Counterexample> errors,
+ out bool exc) {
+ HoudiniVCGen vcgen;
+ if (current.Implementation != null) {
+ Implementation implementation = current.Implementation;
+ vcgenSessions.TryGetValue(implementation, out vcgen);
+ if (vcgen == null)
+ throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
+
+ VCGen.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc);
+ return outcome;
}
- protected void NotifyDequeue(){
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateDequeue(); });
+ else {
+ throw new Exception("VerifyCurrent has null implementation");
}
- protected void NotifyConstant(string constantName){
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateConstant(constantName); });
+ }
+
+ private bool IsOutcomeNotHoudini(VCGen.Outcome outcome, List<Counterexample> errors) {
+ switch (outcome) {
+ case VCGen.Outcome.Correct:
+ return false;
+ case VCGen.Outcome.Errors:
+ 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;
}
- protected void NotifyEnd(bool isNormalEnd) {
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateEnd(isNormalEnd); });
+ }
+
+ // returns true if at least one of the violations is non-candidate
+ private bool AnyNonCandidateViolation(VCGen.Outcome outcome, List<Counterexample> errors) {
+ switch (outcome) {
+ case VCGen.Outcome.Errors:
+ 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;
}
- protected void NotifyFlushStart() {
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateFlushStart(); });
+ }
+
+ private List<Counterexample> emptyList = new List<Counterexample>();
+
+ // Record most current Non-Candidate errors found by Boogie, etc.
+ private void UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,
+ Implementation implementation,
+ VCGen.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:
+ 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;
}
- protected void NotifyFlushFinish() {
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.UpdateFlushFinish(); });
+ houdiniOutcome.implementationOutcomes.Add(implName, new VCGenOutcome(verificationOutcome, nonCandidateErrors));
+ }
+
+ private void FlushWorkList(HoudiniState current) {
+ this.NotifyFlushStart();
+ Axiom axiom = BuildAxiom(current.Assignment);
+ while (current.WorkList.Count > 0) {
+ this.NotifyIteration();
+
+ current.Implementation = current.WorkList.Peek();
+ this.NotifyImplementation(current.Implementation);
+
+ List<Counterexample> errors;
+ VCGen.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors);
+ UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
+ this.NotifyOutcome(outcome);
+
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+
}
-
- protected void NotifyException(string msg) {
- Notify((NotifyDelegate) delegate (HoudiniObserver r) { r.SeeException(msg); });
+ this.NotifyFlushFinish();
+ }
+
+ private void UpdateAssignment(HoudiniState current, RefutedAnnotation refAnnot) {
+ current.Assignment.Remove(refAnnot.Constant);
+ current.Assignment.Add(refAnnot.Constant, false);
+ this.NotifyConstant(refAnnot.Constant);
+ }
+
+ private void AddToWorkList(HoudiniState current, Implementation imp) {
+ if (!current.WorkList.Contains(imp) && !current.isBlackListed(imp.Name)) {
+ current.WorkList.Enqueue(imp);
+ this.NotifyEnqueue(imp);
}
}
-
- public class Houdini : ObservableHoudini {
- private Program program;
- private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;
- private ReadOnlyDictionary<Implementation, HoudiniVCGen> vcgenSessions;
- private CallGraph callGraph;
- private bool continueAtError;
- public Houdini(Program program, bool continueAtError) {
- this.program = program;
- this.callGraph = BuildCallGraph(program);
- this.continueAtError = continueAtError;
- this.houdiniConstants = CollectExistentialConstants(program);
- this.vcgenSessions = PrepareVCGenSessions(program);
- }
+ private void UpdateWorkList(HoudiniState current,
+ VCGen.Outcome outcome,
+ List<Counterexample> errors) {
+ Contract.Assume(current.Implementation != null);
- private ReadOnlyDictionary<Implementation, HoudiniVCGen> PrepareVCGenSessions(Program program) {
- Dictionary<Implementation, HoudiniVCGen> vcgenSessions = new Dictionary<Implementation, HoudiniVCGen>();
-
- foreach (Declaration decl in program.TopLevelDeclarations) {
- Implementation impl = decl as Implementation;
- if (impl != null) {
- // make a different simplify log file for each function
- String simplifyLog = null;
- if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
- simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
- }
- HoudiniVCGen vcgen = new HoudiniVCGen(program, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
- //vcgen.PrepareVerification(impl, program);
- vcgenSessions.Add(impl, vcgen);
+ switch (outcome) {
+ case VCGen.Outcome.Correct:
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ break;
+ case VCGen.Outcome.Errors:
+ 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);
}
- }
- return new ReadOnlyDictionary<Implementation, HoudiniVCGen>(vcgenSessions);
- }
-
- private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants(Program program) {
- Dictionary<string, IdentifierExpr> existentialConstants = new Dictionary<string, IdentifierExpr>();
- foreach (Declaration decl in program.TopLevelDeclarations) {
- Constant constant = decl as Constant;
- if (constant != null) {
- bool result = false;
- if (constant.CheckBooleanAttribute("existential", ref result)) {
- if (result == true)
- existentialConstants.Add(constant.Name, new IdentifierExpr(Token.NoToken, constant));
- }
+ else {
+ dequeue = true; //once one non-houdini error is hit dequeue?!
}
}
- return new ReadOnlyDictionary<string, IdentifierExpr>(existentialConstants);
- }
-
- private CallGraph BuildCallGraph(Program program) {
- return null;
- }
- private Queue<Implementation> BuildWorkList(Program program) {
- Queue<Implementation> queue = new Queue<Implementation>();
- foreach ( Declaration decl in program.TopLevelDeclarations ) {
- Implementation impl = decl as Implementation;
- if (impl!=null) {
- queue.Enqueue(impl);
- }
+ if (dequeue) {
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
}
- return queue;
- }
+ break;
+ case VCGen.Outcome.TimedOut:
+ // 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:
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ break;
+ default:
+ throw new Exception("Unknown vcgen outcome");
+ }
+ }
- private bool MatchCandidate(Expr boogieExpr, out string candidateConstant) {
- candidateConstant = null;
- IExpr antecedent;
- IExpr expr = boogieExpr as IExpr;
- if (expr != null && ExprUtil.Match(expr, Prop.Implies, out antecedent)) {
- IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;
- if (constantFunApp != null && houdiniConstants.ContainsKey(constantFunApp.IdentifierExpr.Name)) {
- candidateConstant = constantFunApp.IdentifierExpr.Name;
- return true;
+
+ private void AddRelatedToWorkList(HoudiniState current, RefutedAnnotation refutedAnnotation) {
+ Contract.Assume(current.Implementation != null);
+ foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) {
+ AddToWorkList(current, implementation);
+ }
+ }
+
+
+ // 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,
+ List<Counterexample> errors) {
+ Contract.Assume(current.Implementation != null);
+ bool dequeue = true;
+
+ switch (outcome) {
+ case VCGen.Outcome.Correct:
+ //yeah, dequeue
+ break;
+ case VCGen.Outcome.Errors:
+ Contract.Assume(errors != null);
+ foreach (Counterexample error in errors) {
+ RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
+ if (refutedAnnotation != null) { // some candidate annotation removed
+ AddRelatedToWorkList(current, refutedAnnotation);
+ UpdateAssignment(current, refutedAnnotation);
+ dequeue = false;
}
}
- return false;
- }
-
-
- private Axiom BuildAxiom(Dictionary<string,bool> currentAssignment) {
- Expr axiom = null;
- 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);
- Expr constantAssignment = Expr.Binary(Token.NoToken,BinaryOperator.Opcode.Eq,constantExpr,valueExpr);
- if (axiom==null)
- axiom = constantAssignment;
- else
- axiom = Expr.Binary(Token.NoToken,BinaryOperator.Opcode.And,axiom,constantAssignment);
- }
- if (axiom==null)
- axiom = new LiteralExpr(Token.NoToken, true);
- return new Axiom(Token.NoToken,axiom);
- }
+ break;
- private Dictionary<string,bool> BuildAssignment(Dictionary<string,IdentifierExpr>.KeyCollection constants) {
- Dictionary<string,bool> initial = new Dictionary<string,bool>();
- foreach (string constant in constants)
- initial.Add(constant,true);
- return initial;
- }
+ case VCGen.Outcome.TimedOut:
+ // TODO: reset session instead of blocking timed out funcs?
+ current.addToBlackList(current.Implementation.Name);
+ break;
+ case VCGen.Outcome.Inconclusive:
+ case VCGen.Outcome.OutOfMemory:
+ break;
+ default:
+ throw new Exception("Unknown vcgen outcome");
+ }
+ if (dequeue) {
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ }
+ return !dequeue;
+ }
- private VCGen.Outcome VerifyUsingAxiom(Implementation implementation, Axiom 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();
- return outcome;
- }
-
- // the main procedure that checks a procedure and updates the
- // assignment and the worklist
- private VCGen.Outcome HoudiniVerifyCurrent(HoudiniState current,
- Program program,
- out List<Counterexample> errors,
- out bool exc) {
- HoudiniVCGen vcgen;
- if (current.Implementation == null)
- throw new Exception("HoudiniVerifyCurrent has null implementation");
-
- Implementation implementation = current.Implementation;
- vcgenSessions.TryGetValue(implementation,out vcgen);
- if(vcgen==null)
- throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
-
- VCGen.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc);
- return outcome;
- }
-
- private VCGen.Outcome VerifyCurrent(HoudiniState current,
- Program program,
- out List<Counterexample> errors,
- out bool exc) {
- HoudiniVCGen vcgen;
- if (current.Implementation != null) {
- Implementation implementation = current.Implementation;
- vcgenSessions.TryGetValue(implementation, out vcgen);
- if(vcgen == null)
- throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
-
- VCGen.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc);
- return outcome;
- } else {
- throw new Exception("VerifyCurrent has null implementation");
- }
- }
-
- private bool IsOutcomeNotHoudini(VCGen.Outcome outcome, List<Counterexample> errors) {
- switch (outcome) {
- case VCGen.Outcome.Correct:
- return false;
- break;
- case VCGen.Outcome.Errors:
- Contract.Assume (errors!=null);
- foreach (Counterexample error in errors) {
- if (ExtractRefutedAnnotation(error)==null)
- return true;
- }
- return false;
- break;
- case VCGen.Outcome.TimedOut:
- case VCGen.Outcome.Inconclusive:
- default:
- return true;
- break;
- }
- }
-
-
- // returns true if at least one of the violations is non-candidate
- private bool AnyNonCandidateViolation(VCGen.Outcome outcome, List<Counterexample> errors) {
- switch (outcome) {
- case VCGen.Outcome.Errors:
- Contract.Assert (errors!=null);
- foreach (Counterexample error in errors) {
- if (ExtractRefutedAnnotation(error)==null)
- return true;
- }
- return false;
- break;
- case VCGen.Outcome.Correct:
- case VCGen.Outcome.TimedOut:
- case VCGen.Outcome.Inconclusive:
- default:
- return false;
- break;
- }
- }
-
-
- private List<Counterexample> emptyList = new List<Counterexample>();
-
- // Record most current Non-Candidate errors found by Boogie, etc.
- private void UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,
- Implementation implementation,
- VCGen.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:
- 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;
- }
- houdiniOutcome.implementationOutcomes.Add(implName,
- new VCGenOutcome(verificationOutcome, nonCandidateErrors));
-
- }
-
- private void FlushWorkList(HoudiniState current) {
- this.NotifyFlushStart();
- Axiom axiom = BuildAxiom(current.Assignment);
- while (current.WorkList.Count>0) {
- this.NotifyIteration();
-
- current.Implementation= current.WorkList.Peek();
- this.NotifyImplementation(current.Implementation);
-
- List<Counterexample> errors;
- VCGen.Outcome outcome = VerifyUsingAxiom(current.Implementation,axiom,out errors);
- UpdateHoudiniOutcome(current.Outcome,current.Implementation,outcome,errors);
- this.NotifyOutcome(outcome);
-
- current.WorkList.Dequeue();
- this.NotifyDequeue();
-
- }
- this.NotifyFlushFinish();
- }
-
- private void UpdateAssignment(HoudiniState current, RefutedAnnotation refAnnot){
- current.Assignment.Remove(refAnnot.Constant);
- current.Assignment.Add(refAnnot.Constant,false);
- this.NotifyConstant(refAnnot.Constant);
- }
-
- private void AddToWorkList(HoudiniState current, Implementation imp) {
- if (!current.WorkList.Contains(imp) && !current.isBlackListed(imp.Name)) {
- current.WorkList.Enqueue(imp);
- this.NotifyEnqueue(imp);
- }
- }
-
- private void UpdateWorkList(HoudiniState current,
- VCGen.Outcome outcome,
- List<Counterexample> errors) {
- Contract.Assume (current.Implementation!=null);
-
- switch (outcome) {
- case VCGen.Outcome.Correct:
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- break;
- case VCGen.Outcome.Errors:
- 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.WorkList.Dequeue();
- this.NotifyDequeue();
- }
- break;
- case VCGen.Outcome.TimedOut:
- // 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:
- current.WorkList.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)) {
- AddToWorkList(current, implementation);
- }
- }
-
-
- // 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,
- List<Counterexample> errors) {
- Contract.Assume (current.Implementation!=null);
- bool dequeue = true;
-
- switch (outcome) {
- case VCGen.Outcome.Correct:
- //yeah, dequeue
- break;
- case VCGen.Outcome.Errors:
- Contract.Assume (errors!=null);
- foreach (Counterexample error in errors) {
- RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
- if (refutedAnnotation!=null) { // some candidate annotation removed
- AddRelatedToWorkList(current, refutedAnnotation);
- UpdateAssignment(current, refutedAnnotation);
- dequeue = false;
- }
- }
- break;
-
- case VCGen.Outcome.TimedOut:
- // TODO: reset session instead of blocking timed out funcs?
- current.addToBlackList(current.Implementation.Name);
- break;
- case VCGen.Outcome.Inconclusive:
- case VCGen.Outcome.OutOfMemory:
- break;
- default:
- throw new Exception("Unknown vcgen outcome");
- }
- if (dequeue) {
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- }
- return !dequeue;
- }
-
-
-
- private class HoudiniState {
- private Queue<Implementation> _workList;
- private HashSet<string> blackList;
- private Dictionary<string,bool> _assignment;
- private Implementation _implementation;
- private HoudiniOutcome _outcome;
-
- public HoudiniState(Queue<Implementation> workList, Dictionary<string,bool> currentAssignment) {
- this._workList = workList;
- this._assignment = currentAssignment;
- this._implementation = null;
- this._outcome = new HoudiniOutcome();
- this.blackList = new HashSet<string>();
- }
-
- public Queue<Implementation> WorkList {
- get { return this._workList; }
- }
- public Dictionary<string,bool> Assignment {
- get { return this._assignment; }
- }
- public Implementation Implementation {
- get { return this._implementation; }
- set { this._implementation = value; }
- }
- public HoudiniOutcome Outcome {
- get { return this._outcome; }
- }
- public bool isBlackListed(string funcName) {
- return blackList.Contains(funcName);
- }
- public void addToBlackList(string funcName) {
- blackList.Add(funcName);
- }
- }
+ private class HoudiniState {
+ private Queue<Implementation> _workList;
+ private HashSet<string> blackList;
+ private Dictionary<string, bool> _assignment;
+ private Implementation _implementation;
+ private HoudiniOutcome _outcome;
- private void PrintBadList(string kind, List<string> list) {
- if(list.Count != 0) {
- Console.WriteLine("----------------------------------------");
- Console.WriteLine("Functions: {0}", kind);
- foreach(string fname in list) {
- Console.WriteLine("\t{0}", fname);
- }
- Console.WriteLine("----------------------------------------");
- }
- }
+ public HoudiniState(Queue<Implementation> workList, Dictionary<string, bool> currentAssignment) {
+ this._workList = workList;
+ this._assignment = currentAssignment;
+ this._implementation = null;
+ this._outcome = new HoudiniOutcome();
+ this.blackList = new HashSet<string>();
+ }
- private void PrintBadOutcomes(List<string> timeouts, List<string> inconc, List<string> errors) {
- PrintBadList("TimedOut", timeouts);
- PrintBadList("Inconclusive", inconc);
- PrintBadList("Errors", errors);
- }
+ public Queue<Implementation> WorkList {
+ get { return this._workList; }
+ }
+ public Dictionary<string, bool> Assignment {
+ get { return this._assignment; }
+ }
+ public Implementation Implementation {
+ get { return this._implementation; }
+ set { this._implementation = value; }
+ }
+ public HoudiniOutcome Outcome {
+ get { return this._outcome; }
+ }
+ public bool isBlackListed(string funcName) {
+ return blackList.Contains(funcName);
+ }
+ public void addToBlackList(string funcName) {
+ blackList.Add(funcName);
+ }
+ }
- public HoudiniOutcome VerifyProgram (Program program) {
- HoudiniOutcome outcome = VerifyProgramSameFuncFirst(program);
- PrintBadOutcomes(outcome.ListOfTimeouts, outcome.ListOfInconclusives, outcome.ListOfErrors);
- return outcome;
+ private void PrintBadList(string kind, List<string> list) {
+ if (list.Count != 0) {
+ Console.WriteLine("----------------------------------------");
+ Console.WriteLine("Functions: {0}", kind);
+ foreach (string fname in list) {
+ Console.WriteLine("\t{0}", fname);
}
+ Console.WriteLine("----------------------------------------");
+ }
+ }
- // Old main loop
- public HoudiniOutcome VerifyProgramUnorderedWork (Program program) {
- 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);
- 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);
- this.NotifyOutcome(outcome);
-
- UpdateHoudiniOutcome(current.Outcome,current.Implementation,outcome,errors);
- if (IsOutcomeNotHoudini(outcome,errors) && !continueAtError) {
- current.WorkList.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 (Program program) {
- HoudiniState current = new HoudiniState(BuildWorkList(program),BuildAssignment(houdiniConstants.Keys));
- this.NotifyStart(program, houdiniConstants.Keys.Count);
-
- while (current.WorkList.Count>0) {
- bool exceptional = false;
- System.GC.Collect();
- this.NotifyIteration();
-
- current.Implementation = current.WorkList.Peek();
- this.NotifyImplementation(current.Implementation);
-
- List<Counterexample> errors;
- VCGen.Outcome outcome = VerifyCurrent(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.WorkList.Dequeue();
- this.NotifyDequeue();
- FlushWorkList(current);
- } else {
- UpdateAssignmentWorkList(current, outcome, errors);
- }
- exceptional = false;
- }
- }
- this.NotifyEnd(true);
- current.Outcome.assignment = current.Assignment;
- return current.Outcome;
- }
+ private void PrintBadOutcomes(List<string> timeouts, List<string> inconc, List<string> errors) {
+ PrintBadList("TimedOut", timeouts);
+ PrintBadList("Inconclusive", inconc);
+ PrintBadList("Errors", errors);
+ }
- //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
- //all non-candidate annotations as unchecked (free requires/ensures, assumes)
- public HoudiniOutcome PerformHoudiniInference(Program program) {
- HoudiniState current = new HoudiniState(BuildWorkList(program),BuildAssignment(houdiniConstants.Keys));
- this.NotifyStart(program, houdiniConstants.Keys.Count);
-
- Console.WriteLine("Using the new houdini algorithm\n");
-
- while (current.WorkList.Count > 0) {
- bool exceptional = false;
- System.GC.Collect();
- this.NotifyIteration();
-
- current.Implementation = current.WorkList.Peek();
- this.NotifyImplementation(current.Implementation);
-
- List<Counterexample> errors;
- VCGen.Outcome outcome = HoudiniVerifyCurrent(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 (AnyNonCandidateViolation(outcome, errors)) { //abort
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- FlushWorkList(current);
- } else { //continue
- UpdateAssignmentWorkList(current, outcome, errors);
- }
- }
- }
- this.NotifyEnd(true);
- current.Outcome.assignment = current.Assignment;
- return current.Outcome;
- }
+ public HoudiniOutcome VerifyProgram(Program program) {
+ HoudiniOutcome outcome = VerifyProgramSameFuncFirst(program);
+ PrintBadOutcomes(outcome.ListOfTimeouts, outcome.ListOfInconclusives, outcome.ListOfErrors);
+ return outcome;
+ }
-
- private List<Implementation> FindImplementationsToEnqueue(RefutedAnnotation refutedAnnotation, Implementation currentImplementation) {
- List<Implementation> implementations = new List<Implementation>();
- switch (refutedAnnotation.Kind) {
- case RefutedAnnotationKind.REQUIRES:
- foreach (Implementation callee in callGraph.NextNodes(currentImplementation)) {
- Contract.Assume (callee.Proc!=null);
- if (callee.Proc.Equals(refutedAnnotation.CalleeProc))
- implementations.Add(callee);
- }
- break;
- case RefutedAnnotationKind.ENSURES:
- foreach (Implementation caller in callGraph.PreviousNodes(currentImplementation))
- implementations.Add(caller);
- break;
- case RefutedAnnotationKind.ASSERT: //the implementation is already in queue
- break;
- default:
- throw new Exception("Unknown Refuted annotation kind:" + refutedAnnotation.Kind);
- break;
- }
- return implementations;
+ // Old main loop
+ public HoudiniOutcome VerifyProgramUnorderedWork(Program program) {
+ 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);
+ 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);
+ this.NotifyOutcome(outcome);
+
+ UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
+ if (IsOutcomeNotHoudini(outcome, errors) && !continueAtError) {
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ FlushWorkList(current);
}
-
- private enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT};
-
- private class RefutedAnnotation {
- private string _constant;
- private RefutedAnnotationKind _kind;
- private Procedure _callee;
-
- private RefutedAnnotation(string constant, RefutedAnnotationKind kind, Procedure callee) {
- this._constant = constant;
- this._kind = kind;
- this._callee = callee;
- }
- public RefutedAnnotationKind Kind {
- get { return this._kind; }
- }
- public string Constant {
- get { return this._constant; }
+ else
+ UpdateWorkList(current, outcome, errors);
+ }
+ this.NotifyEnd(true);
+ current.Outcome.assignment = current.Assignment;
+ return current.Outcome;
+ }
+
+ // New main loop
+ public HoudiniOutcome VerifyProgramSameFuncFirst(Program program) {
+ HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
+ this.NotifyStart(program, houdiniConstants.Keys.Count);
+
+ while (current.WorkList.Count > 0) {
+ bool exceptional = false;
+ System.GC.Collect();
+ this.NotifyIteration();
+
+ current.Implementation = current.WorkList.Peek();
+ this.NotifyImplementation(current.Implementation);
+
+ List<Counterexample> errors;
+ VCGen.Outcome outcome = VerifyCurrent(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.WorkList.Dequeue();
+ this.NotifyDequeue();
+ FlushWorkList(current);
}
- public Procedure CalleeProc {
- get { return this._callee; }
+ else {
+ UpdateAssignmentWorkList(current, outcome, errors);
}
- public static RefutedAnnotation BuildRefutedRequires(string constant, Procedure callee) {
- return new RefutedAnnotation(constant,RefutedAnnotationKind.REQUIRES,callee);
+ 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
+ //all non-candidate annotations as unchecked (free requires/ensures, assumes)
+ public HoudiniOutcome PerformHoudiniInference(Program program) {
+ HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
+ this.NotifyStart(program, houdiniConstants.Keys.Count);
+
+ Console.WriteLine("Using the new houdini algorithm\n");
+
+ while (current.WorkList.Count > 0) {
+ bool exceptional = false;
+ System.GC.Collect();
+ this.NotifyIteration();
+
+ current.Implementation = current.WorkList.Peek();
+ this.NotifyImplementation(current.Implementation);
+
+ List<Counterexample> errors;
+ VCGen.Outcome outcome = HoudiniVerifyCurrent(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 (AnyNonCandidateViolation(outcome, errors)) { //abort
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ FlushWorkList(current);
}
- public static RefutedAnnotation BuildRefutedEnsures(string constant) {
- return new RefutedAnnotation(constant,RefutedAnnotationKind.ENSURES, null);
+ else { //continue
+ UpdateAssignmentWorkList(current, outcome, errors);
}
- public static RefutedAnnotation BuildRefutedAssert(string constant) {
- return new RefutedAnnotation(constant,RefutedAnnotationKind.ASSERT, null);
+ }
+ }
+ this.NotifyEnd(true);
+ current.Outcome.assignment = current.Assignment;
+ return current.Outcome;
+ }
+
+ private List<Implementation> FindImplementationsToEnqueue(RefutedAnnotation refutedAnnotation, Implementation currentImplementation) {
+ List<Implementation> implementations = new List<Implementation>();
+ switch (refutedAnnotation.Kind) {
+ case RefutedAnnotationKind.REQUIRES:
+ foreach (Implementation callee in callGraph.Successors(currentImplementation)) {
+ Contract.Assume(callee.Proc != null);
+ if (callee.Proc.Equals(refutedAnnotation.CalleeProc))
+ implementations.Add(callee);
}
+ break;
+ case RefutedAnnotationKind.ENSURES:
+ foreach (Implementation caller in callGraph.Predecessors(currentImplementation))
+ implementations.Add(caller);
+ break;
+ case RefutedAnnotationKind.ASSERT: //the implementation is already in queue
+ break;
+ default:
+ throw new Exception("Unknown Refuted annotation kind:" + refutedAnnotation.Kind);
+ }
+ return implementations;
+ }
+
+ private enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT };
+
+ private class RefutedAnnotation {
+ private string _constant;
+ private RefutedAnnotationKind _kind;
+ private Procedure _callee;
+
+ private RefutedAnnotation(string constant, RefutedAnnotationKind kind, Procedure callee) {
+ this._constant = constant;
+ this._kind = kind;
+ this._callee = callee;
+ }
+ public RefutedAnnotationKind Kind {
+ get { return this._kind; }
+ }
+ public string Constant {
+ get { return this._constant; }
+ }
+ public Procedure CalleeProc {
+ get { return this._callee; }
+ }
+ public static RefutedAnnotation BuildRefutedRequires(string constant, Procedure callee) {
+ return new RefutedAnnotation(constant, RefutedAnnotationKind.REQUIRES, callee);
+ }
+ public static RefutedAnnotation BuildRefutedEnsures(string constant) {
+ return new RefutedAnnotation(constant, RefutedAnnotationKind.ENSURES, null);
+ }
+ public static RefutedAnnotation BuildRefutedAssert(string constant) {
+ return new RefutedAnnotation(constant, RefutedAnnotationKind.ASSERT, null);
+ }
+ }
+
+ private void PrintRefutedCall(CallCounterexample err, XmlSink xmlOut) {
+ Expr cond = err.FailingRequires.Condition;
+ string houdiniConst;
+ if (MatchCandidate(cond, out houdiniConst)) {
+ xmlOut.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, err.Trace);
+ }
+ }
+
+ private void PrintRefutedReturn(ReturnCounterexample err, XmlSink xmlOut) {
+ Expr cond = err.FailingEnsures.Condition;
+ string houdiniConst;
+ if (MatchCandidate(cond, out houdiniConst)) {
+ xmlOut.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, err.Trace);
+ }
+ }
+
+ private void PrintRefutedAssert(AssertCounterexample err, XmlSink xmlOut) {
+ Expr cond = err.FailingAssert.OrigExpr;
+ string houdiniConst;
+ if (MatchCandidate(cond, out houdiniConst)) {
+ xmlOut.WriteError("postcondition violation", err.FailingAssert.tok, err.FailingAssert.tok, err.Trace);
+ }
+ }
+
+
+ private void DebugRefutedCandidates(Implementation curFunc, List<Counterexample> errors) {
+ XmlSink xmlRefuted = CommandLineOptions.Clo.XmlRefuted;
+ if (xmlRefuted != null && errors != null) {
+ DateTime start = DateTime.Now;
+ xmlRefuted.WriteStartMethod(curFunc.ToString(), start);
+
+ foreach (Counterexample error in errors) {
+ CallCounterexample ce = error as CallCounterexample;
+ if (ce != null) PrintRefutedCall(ce, xmlRefuted);
+ ReturnCounterexample re = error as ReturnCounterexample;
+ if (re != null) PrintRefutedReturn(re, xmlRefuted);
+ AssertCounterexample ae = error as AssertCounterexample;
+ if (ae != null) PrintRefutedAssert(ae, xmlRefuted);
}
-
- private void PrintRefutedCall(CallCounterexample err, XmlSink xmlOut) {
- Expr cond = err.FailingRequires.Condition;
- string houdiniConst;
- if (MatchCandidate(cond, out houdiniConst)) {
- xmlOut.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, err.Trace);
- }
+
+ DateTime end = DateTime.Now;
+ xmlRefuted.WriteEndMethod("errors", end, end.Subtract(start));
+ }
+ }
+
+ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {
+ string houdiniConstant;
+ CallCounterexample callCounterexample = error as CallCounterexample;
+ if (callCounterexample != null) {
+ Procedure failingProcedure = callCounterexample.FailingCall.Proc;
+ Requires failingRequires = callCounterexample.FailingRequires;
+ if (MatchCandidate(failingRequires.Condition, out houdiniConstant)) {
+ Contract.Assert(houdiniConstant != null);
+ return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure);
}
-
- private void PrintRefutedReturn(ReturnCounterexample err, XmlSink xmlOut) {
- Expr cond = err.FailingEnsures.Condition;
- string houdiniConst;
- if (MatchCandidate(cond, out houdiniConst)) {
- xmlOut.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, err.Trace);
- }
+ }
+ ReturnCounterexample returnCounterexample = error as ReturnCounterexample;
+ if (returnCounterexample != null) {
+ Ensures failingEnsures = returnCounterexample.FailingEnsures;
+ if (MatchCandidate(failingEnsures.Condition, out houdiniConstant)) {
+ Contract.Assert(houdiniConstant != null);
+ return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant);
}
-
- private void PrintRefutedAssert(AssertCounterexample err, XmlSink xmlOut) {
- Expr cond = err.FailingAssert.OrigExpr;
- string houdiniConst;
- if (MatchCandidate(cond, out houdiniConst)) {
- xmlOut.WriteError("postcondition violation", err.FailingAssert.tok, err.FailingAssert.tok, err.Trace);
- }
+ }
+ AssertCounterexample assertCounterexample = error as AssertCounterexample;
+ if (assertCounterexample != null) {
+ AssertCmd failingAssert = assertCounterexample.FailingAssert;
+ if (MatchCandidate(failingAssert.OrigExpr, out houdiniConstant)) {
+ Contract.Assert(houdiniConstant != null);
+ return RefutedAnnotation.BuildRefutedAssert(houdiniConstant);
}
+ }
+ return null;
+ }
- private void DebugRefutedCandidates(Implementation curFunc, List<Counterexample> errors) {
- XmlSink xmlRefuted = CommandLineOptions.Clo.XmlRefuted;
- if (xmlRefuted != null && errors != null) {
- DateTime start = DateTime.Now;
- xmlRefuted.WriteStartMethod(curFunc.ToString(), start);
-
- foreach (Counterexample error in errors) {
- CallCounterexample ce = error as CallCounterexample;
- if (ce != null) PrintRefutedCall(ce, xmlRefuted);
- ReturnCounterexample re = error as ReturnCounterexample;
- if (re != null) PrintRefutedReturn(re, xmlRefuted);
- AssertCounterexample ae = error as AssertCounterexample;
- if (ae != null) PrintRefutedAssert(ae, xmlRefuted);
- }
-
- DateTime end = DateTime.Now;
- xmlRefuted.WriteEndMethod("errors", end, end.Subtract(start));
- }
- }
-
- private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {
- string houdiniConstant;
- CallCounterexample callCounterexample = error as CallCounterexample;
- if (callCounterexample!=null) {
- Procedure failingProcedure = callCounterexample.FailingCall.Proc;
- Requires failingRequires = callCounterexample.FailingRequires;
- if (MatchCandidate(failingRequires.Condition,out houdiniConstant)) {
- Contract.Assert (houdiniConstant!=null);
- return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure);
- }
- }
- ReturnCounterexample returnCounterexample = error as ReturnCounterexample;
- if (returnCounterexample!=null) {
- Ensures failingEnsures =returnCounterexample.FailingEnsures;
- if (MatchCandidate(failingEnsures.Condition,out houdiniConstant)) {
- Contract.Assert (houdiniConstant!=null);
- return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant);
- }
+ private VCGen.Outcome TryCatchVerify(HoudiniVCGen vcgen, out List<Counterexample> errors) {
+ VCGen.Outcome outcome;
+ try {
+ outcome = vcgen.Verify(out errors);
+ }
+ catch (VCGenException e) {
+ Contract.Assume(e != null);
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ }
+ catch (UnexpectedProverOutputException upo) {
+ Contract.Assume(upo != null);
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ }
+ 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,
+ Program program,
+ HoudiniVCGen vcgen,
+ out List<Counterexample> errors,
+ out bool exceptional) {
+ Contract.Assert(current.Implementation != null);
+ VCGen.Outcome outcome;
+ bool pushed = false;
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ try {
+ bool trySameFunc = true;
+ bool pastFirstIter = false; //see if this new loop is even helping
+
+ do {
+ if (pastFirstIter) {
+ System.GC.Collect();
+ this.NotifyIteration();
}
- AssertCounterexample assertCounterexample = error as AssertCounterexample;
- if (assertCounterexample!=null) {
- AssertCmd failingAssert = assertCounterexample.FailingAssert;
- if (MatchCandidate(failingAssert.OrigExpr,out houdiniConstant)) {
- Contract.Assert (houdiniConstant!=null);
- return RefutedAnnotation.BuildRefutedAssert(houdiniConstant);
- }
+ Axiom currentAx = BuildAxiom(current.Assignment);
+ this.NotifyAssignment(current.Assignment);
+
+ vcgen.PushAxiom(currentAx);
+ pushed = true;
+ outcome = vcgen.Verify(out errors);
+ vcgen.Pop();
+ pushed = false;
+ this.NotifyOutcome(outcome);
+
+ DebugRefutedCandidates(current.Implementation, errors);
+ UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
+ if (!continueAtError && IsOutcomeNotHoudini(outcome, errors)) {
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ trySameFunc = false;
+ FlushWorkList(current);
}
-
- return null;
- }
-
- private VCGen.Outcome TryCatchVerify(HoudiniVCGen vcgen, out List<Counterexample> errors) {
- VCGen.Outcome outcome;
- try {
- outcome = vcgen.Verify(out errors);
- } catch (VCGenException e) {
- Contract.Assume(e!=null);
+ else {
+ trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
+ //reset for the next round
errors = null;
outcome = VCGen.Outcome.Inconclusive;
- } catch (UnexpectedProverOutputException upo) {
- Contract.Assume(upo!=null);
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- return outcome;
+ }
+ pastFirstIter = true;
+ } while (trySameFunc && current.WorkList.Count > 0);
+
+ }
+ catch (VCGenException e) {
+ Contract.Assume(e != null);
+ if (pushed) {
+ vcgen.Pop(); // what if session is dead?
}
-
- //version of TryCatchVerify that spins on the same function
- //as long as the current assignment is changing
- private VCGen.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;
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- try {
- bool trySameFunc = true;
- bool pastFirstIter = false; //see if this new loop is even helping
-
- do {
- if (pastFirstIter) {
- System.GC.Collect();
- this.NotifyIteration();
- }
- Axiom currentAx = BuildAxiom(current.Assignment);
- this.NotifyAssignment(current.Assignment);
-
- vcgen.PushAxiom(currentAx);
- pushed = true;
- outcome = vcgen.Verify(out errors);
- vcgen.Pop();
- pushed = false;
- this.NotifyOutcome(outcome);
-
- DebugRefutedCandidates(current.Implementation, errors);
- UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
- if (!continueAtError && IsOutcomeNotHoudini(outcome,errors)) {
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- trySameFunc = false;
- FlushWorkList(current);
- } else {
- trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
- //reset for the next round
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- pastFirstIter = true;
- } while (trySameFunc && current.WorkList.Count > 0);
-
- } 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;
- }
- exceptional = false;
- return outcome;
+ NotifyException("VCGen");
+ exceptional = true;
+ return outcome;
+ }
+ catch (UnexpectedProverOutputException upo) {
+ Contract.Assume(upo != null);
+ if (pushed) {
+ vcgen.Pop();
}
-
-
-
- //Similar to TrySpinSameFunc except no Candidate logic
- private VCGen.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;
+ NotifyException("UnexpectedProverOutput");
+ exceptional = true;
+ return outcome;
+ }
+ exceptional = false;
+ return outcome;
+ }
+
+ //Similar to TrySpinSameFunc except no Candidate logic
+ private VCGen.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;
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ try {
+ bool trySameFunc = true;
+ bool pastFirstIter = false; //see if this new loop is even helping
+
+ do {
+ if (pastFirstIter) {
+ System.GC.Collect();
+ this.NotifyIteration();
+ }
+
+ Axiom currentAx = BuildAxiom(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;
+ this.NotifyOutcome(outcome);
+
+ DebugRefutedCandidates(current.Implementation, errors);
+ UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
+
+ if (AnyNonCandidateViolation(outcome, errors)) { //abort
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ trySameFunc = false;
+ FlushWorkList(current);
+ }
+ else { //continue
+ trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
+ //reset for the next round
errors = null;
outcome = VCGen.Outcome.Inconclusive;
- try {
- bool trySameFunc = true;
- bool pastFirstIter = false; //see if this new loop is even helping
-
- do {
- if (pastFirstIter) {
- System.GC.Collect();
- this.NotifyIteration();
- }
-
- Axiom currentAx = BuildAxiom(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;
- this.NotifyOutcome(outcome);
-
- DebugRefutedCandidates(current.Implementation, errors);
- UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
-
- if (AnyNonCandidateViolation(outcome, errors)) { //abort
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- trySameFunc = false;
- FlushWorkList(current);
- } else { //continue
- trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
- //reset for the next round
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- pastFirstIter = true;
- } while (trySameFunc && current.WorkList.Count > 0);
-
- } 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;
- }
- exceptional = false;
- return outcome;
+ }
+ pastFirstIter = true;
+ } while (trySameFunc && current.WorkList.Count > 0);
+
+ }
+ 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;
+ }
+ exceptional = false;
+ return outcome;
}
+ }
public enum HoudiniOutcomeKind { Done, FatalError, VerificationCompleted }
@@ -1087,32 +1081,32 @@ namespace Microsoft.Boogie.Houdini public class HoudiniOutcome {
// final assignment
- public Dictionary<string,bool> assignment = new Dictionary<string,bool>();
+ public Dictionary<string, bool> assignment = new Dictionary<string, bool>();
// boogie errors
- public Dictionary<string,VCGenOutcome> implementationOutcomes = new Dictionary<string,VCGenOutcome>();
+ public Dictionary<string, VCGenOutcome> implementationOutcomes = new Dictionary<string, VCGenOutcome>();
// outcome kind
public HoudiniOutcomeKind kind;
-
+
// statistics
-
+
private int CountResults(VCGen.Outcome outcome) {
- int outcomeCount=0;
- foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values) {
- if (verifyOutcome.outcome==outcome)
- outcomeCount++;
- }
- return outcomeCount;
+ int outcomeCount = 0;
+ foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values) {
+ if (verifyOutcome.outcome == outcome)
+ outcomeCount++;
+ }
+ return outcomeCount;
}
-
+
private List<string> ListOutcomeMatches(VCGen.Outcome outcome) {
- List<string> result = new List<string>();
- foreach (KeyValuePair<string, VCGenOutcome> kvpair in implementationOutcomes) {
- if (kvpair.Value.outcome==outcome)
- result.Add(kvpair.Key);
- }
- return result;
+ List<string> result = new List<string>();
+ foreach (KeyValuePair<string, VCGenOutcome> kvpair in implementationOutcomes) {
+ if (kvpair.Value.outcome == outcome)
+ result.Add(kvpair.Key);
+ }
+ return result;
}
-
+
public int ErrorCount {
get {
return CountResults(VCGen.Outcome.Errors);
@@ -1127,7 +1121,7 @@ namespace Microsoft.Boogie.Houdini get {
return CountResults(VCGen.Outcome.Inconclusive);
}
- }
+ }
public int TimeOuts {
get {
return CountResults(VCGen.Outcome.TimedOut);
diff --git a/Source/Houdini/Houdini.ssc b/Source/Houdini/Houdini.ssc deleted file mode 100644 index bd8348be..00000000 --- a/Source/Houdini/Houdini.ssc +++ /dev/null @@ -1,1188 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using Microsoft.Contracts;
-using System.Collections.Generic;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify.AST;
-using VC;
-using Microsoft.Boogie.Z3;
-using Microsoft.AbstractInterpretationFramework;
-using Microsoft.Boogie.AbstractInterpretation;
-using System.Collections;
-using System.Compiler;
-using System.IO;
-
-namespace Microsoft.Boogie.Houdini
-{
-
- class ReadOnlyDictionary<K,V> {
- private Dictionary<K,V>! dictionary;
- public ReadOnlyDictionary(Dictionary<K,V>! dictionary) {
- this.dictionary = dictionary;
- }
-
- public Dictionary<K,V>.KeyCollection Keys {
- get { return this.dictionary.Keys; }
- }
-
- public bool TryGetValue(K k, out V? v) {
- return this.dictionary.TryGetValue(k, out v);
- }
-
- public bool ContainsKey(K k) {
- return this.dictionary.ContainsKey(k);
- }
- }
-
- public class CallGraph {
-
- private IGraphNavigator! aiCallGraph;
-
- public CallGraph(IGraphNavigator! aiCallGraph) {
- this.aiCallGraph = aiCallGraph;
- }
-
- public IEnumerable! PreviousNodes(Implementation! n) {
- return (!)this.aiCallGraph.PreviousNodes(n);
- }
- public IEnumerable! NextNodes(Implementation! n) {
- return (!)this.aiCallGraph.NextNodes(n);
- }
-
- }
-
- public abstract class HoudiniObserver {
- public virtual void UpdateStart(Program! program, int numConstants) {}
- 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 UpdateEnqueue(Implementation! implementation) {}
- public virtual void UpdateDequeue() {}
- public virtual void UpdateConstant(string! constantName) {}
- public virtual void UpdateEnd(bool isNormalEnd) {}
- public virtual void UpdateFlushStart() {}
- public virtual void UpdateFlushFinish() {}
- public virtual void SeeException(string! msg){}
- }
-
- public class IterationTimer <K> {
- private Dictionary<K, List<double>!>! times;
-
- public IterationTimer () {
- times = new Dictionary<K, List<double>!>();
- }
-
- public void AddTime(K key, double timeMS) {
- List<double> oldList;
- times.TryGetValue(key, out oldList);
- if (oldList == null) {
- oldList = new List<double>();
- } else {
- times.Remove(key);
- }
- oldList.Add(timeMS);
- times.Add(key, oldList);
- }
-
- public void PrintTimes(TextWriter! wr) {
- wr.WriteLine ("Total procedures: {0}", times.Count);
- double total = 0;
- int totalIters = 0;
- foreach(KeyValuePair<K, List<double>!> kv in times) {
- int curIter = 0;
- wr.WriteLine("Times for {0}:", kv.Key);
- foreach(double v in kv.Value) {
- wr.WriteLine(" ({0})\t{1}ms", curIter, v);
- total += v;
- curIter++;
- }
- totalIters += curIter;
- }
- total = total / 1000.0;
- wr.WriteLine ("Total time: {0} (s)", total);
- wr.WriteLine ("Avg: {0} (s/iter)", total/totalIters);
- }
- }
-
- public class HoudiniTimer : HoudiniObserver {
- private DateTime startT;
- private Implementation curImp;
- private IterationTimer<string!>! times;
- private TextWriter! wr;
-
- public HoudiniTimer(TextWriter! wr) {
- this.wr = wr;
- times = new IterationTimer<string!>();
- }
- public override void UpdateIteration() {
- startT = DateTime.Now;
- }
- public override void UpdateImplementation(Implementation! implementation){
- curImp = implementation;
- }
- public override void UpdateOutcome (VCGen.Outcome o) {
- assert curImp != null;
- DateTime endT = DateTime.Now;
- times.AddTime(curImp.Name, (endT - startT).TotalMilliseconds); // assuming names are unique
- }
- public void PrintTimes() {
- wr.WriteLine("-----------------------------------------");
- wr.WriteLine("Times for each iteration for each procedure");
- wr.WriteLine("-----------------------------------------");
- times.PrintTimes(wr);
- }
- }
-
- public class HoudiniTextReporter: HoudiniObserver {
- private TextWriter! wr;
- private int currentIteration = -1;
-
- public HoudiniTextReporter(TextWriter! wr) {
- this.wr = wr;
- }
- public override void UpdateStart(Program! program, int numConstants) {
- wr.WriteLine("Houdini started:" + program.ToString() + " #constants: " + numConstants.ToString());
- currentIteration = -1;
- wr.Flush();
- }
- public override void UpdateIteration() {
- currentIteration++;
- wr.WriteLine("---------------------------------------");
- wr.WriteLine("Houdini iteration #" + currentIteration);
- wr.Flush();
- }
- public override void UpdateImplementation(Implementation! implementation){
- wr.WriteLine("implementation under analysis :" + implementation.Name);
- wr.Flush();
- }
- public override void UpdateAssignment(Dictionary<string!,bool>! assignment) {
- bool firstTime = true;
- wr.Write("assignment under analysis : axiom (");
- foreach (KeyValuePair<string!,bool> kv in assignment) {
- if (!firstTime) wr.Write(" && "); else firstTime = false;
- string! valString; // ugliness to get it lower cased
- if (kv.Value) valString = "true"; else valString = "false";
- wr.Write(kv.Key + " == " + valString);
- }
- wr.WriteLine(");");
- wr.Flush();
- }
- public override void UpdateOutcome(VCGen.Outcome outcome) {
- wr.WriteLine("analysis outcome :" + outcome);
- wr.Flush();
- }
- public override void UpdateEnqueue(Implementation! implementation) {
- wr.WriteLine("worklist enqueue :" + implementation.Name);
- wr.Flush();
- }
- public override void UpdateDequeue() {
- wr.WriteLine("worklist dequeue");
- wr.Flush();
- }
- public override void UpdateConstant(string! constantName) {
- wr.WriteLine("constant disabled : " + constantName);
- wr.Flush();
- }
- public override void UpdateEnd(bool isNormalEnd) {
- wr.WriteLine("Houdini ended: " + (isNormalEnd ? "Normal" : "Abnormal"));
- wr.WriteLine("Number of iterations: " + (this.currentIteration+1));
- wr.Flush();
- }
- public override void UpdateFlushStart() {
- wr.WriteLine("***************************************");
- wr.WriteLine("Flushing remaining implementations");
- wr.Flush();
- }
- public override void UpdateFlushFinish() {
- wr.WriteLine("***************************************");
- wr.WriteLine("Flushing finished");
- wr.Flush();
- }
- public override void SeeException(string! msg) {
- wr.WriteLine("Caught exception: " + msg);
- wr.Flush();
- }
-
- }
-
-
- public abstract class ObservableHoudini {
- private List<HoudiniObserver!>! observers= new List<HoudiniObserver!>();
-
- public void AddObserver(HoudiniObserver! observer) {
- if (!observers.Contains(observer))
- observers.Add(observer);
- }
- private delegate void NotifyDelegate(HoudiniObserver! observer);
-
- private void Notify(NotifyDelegate! notifyDelegate) {
- foreach (HoudiniObserver! observer in observers) {
- notifyDelegate(observer);
- }
- }
- protected void NotifyStart(Program! program, int numConstants) {
- NotifyDelegate notifyDelegate = (NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateStart(program, numConstants); };
- Notify(notifyDelegate);
- }
- protected void NotifyIteration() {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateIteration(); });
- }
- protected void NotifyImplementation(Implementation! implementation) {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateImplementation(implementation); });
- }
- protected void NotifyAssignment(Dictionary<string!,bool>! assignment) {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateAssignment(assignment); });
- }
- protected void NotifyOutcome(VCGen.Outcome outcome) {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateOutcome(outcome); });
- }
- protected void NotifyEnqueue(Implementation! implementation){
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateEnqueue(implementation); });
- }
- protected void NotifyDequeue(){
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateDequeue(); });
- }
- protected void NotifyConstant(string! constantName){
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateConstant(constantName); });
- }
- protected void NotifyEnd(bool isNormalEnd) {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateEnd(isNormalEnd); });
- }
- protected void NotifyFlushStart() {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateFlushStart(); });
- }
- protected void NotifyFlushFinish() {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateFlushFinish(); });
- }
-
- protected void NotifyException(string! msg) {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.SeeException(msg); });
- }
- }
-
- public enum HoudiniProver { Z3, Z3API }
-
- public class Houdini : ObservableHoudini {
-
- private Program! program;
-
- private ReadOnlyDictionary<string!,IdentifierExpr!>! houdiniConstants;
- private ReadOnlyDictionary<Implementation!,HdnVCGen!>! vcgenSessions;
- private CallGraph! callGraph;
- private bool continueAtError;
- private HoudiniProver houdiniProver;
- private HdnVCGenFactory! vcgenFactory;
-
- public Houdini(Program! program, CallGraph! callgraph, bool continueAtError, HoudiniProver houdiniProver) {
- this.program=program;
- this.callGraph = callgraph;
- this.continueAtError = continueAtError;
- this.houdiniProver = houdiniProver;
- HdnVCGenFactory factory;
- switch (this.houdiniProver) {
- case HoudiniProver.Z3:
- factory = new Z3HdnVCGenFactory();
- break;
- case HoudiniProver.Z3API:
- default:
- factory = new Z3APIHdnVCGenFactory();
- break;
- }
- this.vcgenFactory = factory;
- HoudiniHelper helper = new HoudiniHelper(factory);
- this.houdiniConstants = helper.CollectExistentialConstants(program);
- this.vcgenSessions = helper.PrepareVCGenSessions(program);
- }
-
- private Queue<Implementation!>! BuildWorkList(Program! program) {
- Queue<Implementation!>! queue = new Queue<Implementation!>();
- foreach ( Declaration! decl in program.TopLevelDeclarations ) {
- Implementation impl = decl as Implementation;
- if (impl!=null) {
- queue.Enqueue(impl);
- }
- }
- return queue;
- }
-
- private class HoudiniHelper {
- private HdnVCGenFactory! vcgenFactory;
- public HoudiniHelper(HdnVCGenFactory! vcgenFactory) {
- this.vcgenFactory = vcgenFactory;
- }
-
- public ReadOnlyDictionary<Implementation!,HdnVCGen!>! PrepareVCGenSessions(Program! program) {
- Dictionary<Implementation!,HdnVCGen!>! vcgenSessions = new Dictionary<Implementation!,HdnVCGen!>();
-
- foreach ( Declaration! decl in program.TopLevelDeclarations ) {
- Implementation impl = decl as Implementation;
- if (impl!=null) {
- // make a different simplify log file for each function
- String simplifyLog = null;
- if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
- simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
- }
- HdnVCGen! vcgen = vcgenFactory.BuildVCGen(program, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
- vcgen.PrepareVerification(impl,program);
- vcgenSessions.Add(impl,vcgen);
- }
- }
- return new ReadOnlyDictionary<Implementation!,HdnVCGen!>(vcgenSessions);
- }
-
- public ReadOnlyDictionary<string!,IdentifierExpr!>! CollectExistentialConstants(Program! program) {
- Dictionary<string!,IdentifierExpr!>! existentialConstants = new Dictionary<string!,IdentifierExpr!>();
- foreach ( Declaration! decl in program.TopLevelDeclarations ) {
- Constant constant = decl as Constant;
- if (constant!=null) {
- bool result=false;
- if (constant.CheckBooleanAttribute("existential",ref result)) {
- if (result==true)
- existentialConstants.Add(constant.Name, new IdentifierExpr(Token.NoToken,constant));
- }
- }
- }
- return new ReadOnlyDictionary<string!,IdentifierExpr!>(existentialConstants);
- }
- }
-
- private bool MatchCandidate(Expr boogieExpr, out string candidateConstant) {
- candidateConstant = null;
- IExpr antecedent;
- IExpr expr = boogieExpr as IExpr;
- if (expr!=null && ExprUtil.Match(expr, Prop.Implies, out antecedent)) {
- IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;
- if ((constantFunApp !=null) && (houdiniConstants.ContainsKey(constantFunApp.IdentifierExpr.Name))) {
- candidateConstant = constantFunApp.IdentifierExpr.Name;
- return true;
- }
- }
- return false;
- }
-
-
- private Axiom! BuildAxiom(Dictionary<string!,bool>! currentAssignment) {
- Expr axiom = null;
- foreach (KeyValuePair<string!,bool> kv in currentAssignment) {
- IdentifierExpr constantExpr;
- houdiniConstants.TryGetValue(kv.Key,out constantExpr);
- assume (constantExpr!=null);
- Expr valueExpr = new LiteralExpr(Token.NoToken, kv.Value);
- Expr constantAssignment = Expr.Binary(Token.NoToken,BinaryOperator.Opcode.Eq,constantExpr,valueExpr);
- if (axiom==null)
- axiom = constantAssignment;
- else
- axiom = Expr.Binary(Token.NoToken,BinaryOperator.Opcode.And,axiom,constantAssignment);
- }
- if (axiom==null)
- axiom = new LiteralExpr(Token.NoToken, true);
- return new Axiom(Token.NoToken,axiom);
- }
-
- private Dictionary<string!,bool>! BuildAssignment(Dictionary<string!,IdentifierExpr!>.KeyCollection! constants) {
- Dictionary<string!,bool>! initial = new Dictionary<string!,bool>();
- foreach (string! constant in constants)
- initial.Add(constant,true);
- return initial;
- }
-
- private VCGen.Outcome VerifyUsingAxiom(Implementation! implementation, Axiom! axiom, out List<Counterexample!>? errors) {
- HdnVCGen 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();
- return outcome;
- }
-
- // the main procedure that checks a procedure and updates the
- // assignment and the worklist
- private VCGen.Outcome HoudiniVerifyCurrent(HoudiniState! current,
- Program! program,
- out List<Counterexample!>? errors,
- out bool exc) {
- HdnVCGen vcgen;
- if (current.Implementation == null)
- throw new Exception("HoudiniVerifyCurrent has null implementation");
-
- Implementation! implementation = current.Implementation;
- vcgenSessions.TryGetValue(implementation,out vcgen);
- if(vcgen==null)
- throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
-
- VCGen.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc);
- return outcome;
- }
-
- private VCGen.Outcome VerifyCurrent(HoudiniState! current,
- Program! program,
- out List<Counterexample!>? errors,
- out bool exc) {
- HdnVCGen vcgen;
- if (current.Implementation != null) {
- Implementation! implementation = current.Implementation;
- vcgenSessions.TryGetValue(implementation,out vcgen);
- if(vcgen==null)
- throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
-
- VCGen.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc);
- return outcome;
- } else {
- throw new Exception("VerifyCurrent has null implementation");
- }
- }
-
- private bool IsOutcomeNotHoudini(VCGen.Outcome outcome, List<Counterexample!>? errors) {
- switch (outcome) {
- case VCGen.Outcome.Correct:
- return false;
- break;
- case VCGen.Outcome.Errors:
- assume (errors!=null);
- foreach (Counterexample error in errors) {
- if (ExtractRefutedAnnotation(error)==null)
- return true;
- }
- return false;
- break;
- case VCGen.Outcome.TimedOut:
- case VCGen.Outcome.Inconclusive:
- default:
- return true;
- break;
- }
- }
-
-
- // returns true if at least one of the violations is non-candidate
- private bool AnyNonCandidateViolation(VCGen.Outcome outcome, List<Counterexample!>? errors) {
- switch (outcome) {
- case VCGen.Outcome.Errors:
- assert (errors!=null);
- foreach (Counterexample error in errors) {
- if (ExtractRefutedAnnotation(error)==null)
- return true;
- }
- return false;
- break;
- case VCGen.Outcome.Correct:
- case VCGen.Outcome.TimedOut:
- case VCGen.Outcome.Inconclusive:
- default:
- return false;
- break;
- }
- }
-
-
- private List<Counterexample!> emptyList = new List<Counterexample!>();
-
- // Record most current Non-Candidate errors found by Boogie, etc.
- private void UpdateHoudiniOutcome(HoudiniOutcome! houdiniOutcome,
- Implementation! implementation,
- VCGen.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:
- 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;
- }
- houdiniOutcome.implementationOutcomes.Add(implName,
- new VCGenOutcome(verificationOutcome, nonCandidateErrors));
-
- }
-
- private void FlushWorkList(HoudiniState! current) {
- this.NotifyFlushStart();
- Axiom axiom = BuildAxiom(current.Assignment);
- while (current.WorkList.Count>0) {
- this.NotifyIteration();
-
- current.Implementation= current.WorkList.Peek();
- this.NotifyImplementation(current.Implementation);
-
- List<Counterexample!>? errors;
- VCGen.Outcome outcome = VerifyUsingAxiom(current.Implementation,axiom,out errors);
- UpdateHoudiniOutcome(current.Outcome,current.Implementation,outcome,errors);
- this.NotifyOutcome(outcome);
-
- current.WorkList.Dequeue();
- this.NotifyDequeue();
-
- }
- this.NotifyFlushFinish();
- }
-
- private void UpdateAssignment(HoudiniState! current, RefutedAnnotation! refAnnot){
- current.Assignment.Remove(refAnnot.Constant);
- current.Assignment.Add(refAnnot.Constant,false);
- this.NotifyConstant(refAnnot.Constant);
- }
-
- private void AddToWorkList(HoudiniState! current, Implementation! imp) {
- if (!current.WorkList.Contains(imp) && !current.isBlackListed(imp.Name)) {
- current.WorkList.Enqueue(imp);
- this.NotifyEnqueue(imp);
- }
- }
-
- private void UpdateWorkList(HoudiniState! current,
- VCGen.Outcome outcome,
- List<Counterexample!>? errors) {
- assume (current.Implementation!=null);
-
- switch (outcome) {
- case VCGen.Outcome.Correct:
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- break;
- case VCGen.Outcome.Errors:
- 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.WorkList.Dequeue();
- this.NotifyDequeue();
- }
- break;
- case VCGen.Outcome.TimedOut:
- // 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:
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- break;
- default:
- throw new Exception("Unknown vcgen outcome");
- }
- }
-
-
- private void AddRelatedToWorkList(HoudiniState! current, RefutedAnnotation! refutedAnnotation) {
- assume (current.Implementation != null);
- foreach (Implementation! implementation in FindImplementationsToEnqueue(refutedAnnotation,current.Implementation)) {
- AddToWorkList(current, implementation);
- }
- }
-
-
- // 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,
- List<Counterexample!>? errors) {
- assume (current.Implementation!=null);
- bool dequeue = true;
-
- switch (outcome) {
- case VCGen.Outcome.Correct:
- //yeah, dequeue
- break;
- case VCGen.Outcome.Errors:
- assume (errors!=null);
- foreach (Counterexample! error in errors) {
- RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
- if (refutedAnnotation!=null) { // some candidate annotation removed
- AddRelatedToWorkList(current, refutedAnnotation);
- UpdateAssignment(current, refutedAnnotation);
- dequeue = false;
- }
- }
- break;
-
- case VCGen.Outcome.TimedOut:
- // TODO: reset session instead of blocking timed out funcs?
- current.addToBlackList(current.Implementation.Name);
- break;
- case VCGen.Outcome.Inconclusive:
- case VCGen.Outcome.OutOfMemory:
- break;
- default:
- throw new Exception("Unknown vcgen outcome");
- }
- if (dequeue) {
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- }
- return !dequeue;
- }
-
-
-
- private class HoudiniState {
- private Queue<Implementation!>! _workList;
- private Set<string!>! blackList;
- private Dictionary<string!,bool>! _assignment;
- private Implementation _implementation;
- private HoudiniOutcome! _outcome;
-
- public HoudiniState(Queue<Implementation!>! workList, Dictionary<string!,bool>! currentAssignment) {
- this._workList = workList;
- this._assignment = currentAssignment;
- this._implementation = null;
- this._outcome = new HoudiniOutcome();
- this.blackList = new Set<string!>();
- }
-
- public Queue<Implementation!>! WorkList {
- get { return this._workList; }
- }
- public Dictionary<string!,bool>! Assignment {
- get { return this._assignment; }
- }
- public Implementation Implementation {
- get { return this._implementation; }
- set { this._implementation = value; }
- }
- public HoudiniOutcome! Outcome {
- get { return this._outcome; }
- }
- public bool isBlackListed(string! funcName) {
- return blackList.Contains(funcName);
- }
- public void addToBlackList(string! funcName) {
- blackList.Add(funcName);
- }
- }
-
- private void PrintBadList(string kind, List<string!>! 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<string!>! timeouts, List<string!>! inconc, List<string!>! errors) {
- PrintBadList("TimedOut", timeouts);
- PrintBadList("Inconclusive", inconc);
- PrintBadList("Errors", errors);
- }
-
- public HoudiniOutcome! VerifyProgram (Program! program) {
- HoudiniOutcome outcome;
- switch (this.houdiniProver) {
- case HoudiniProver.Z3:
- outcome = VerifyProgramSameFuncFirst(program);
- //outcome = PerformHoudiniInference(program);
- break;
- case HoudiniProver.Z3API: // not that stable
- outcome = VerifyProgramUnorderedWork(program);
- break;
- default:
- throw new Exception("Unknown HoudiniProver: " + this.houdiniProver.ToString());
- }
- PrintBadOutcomes(outcome.ListOfTimeouts, outcome.ListOfInconclusives, outcome.ListOfErrors);
- return outcome;
- }
-
- // Old main loop
- public HoudiniOutcome! VerifyProgramUnorderedWork (Program! program) {
- 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);
- 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);
- this.NotifyOutcome(outcome);
-
- UpdateHoudiniOutcome(current.Outcome,current.Implementation,outcome,errors);
- if (IsOutcomeNotHoudini(outcome,errors) && !continueAtError) {
- current.WorkList.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 (Program! program) {
- HoudiniState current = new HoudiniState(BuildWorkList(program),BuildAssignment((!)houdiniConstants.Keys));
- this.NotifyStart(program, houdiniConstants.Keys.Count);
-
- while (current.WorkList.Count>0) {
- bool exceptional = false;
- System.GC.Collect();
- this.NotifyIteration();
-
- current.Implementation = current.WorkList.Peek();
- this.NotifyImplementation(current.Implementation);
-
- List<Counterexample!>? errors;
- VCGen.Outcome outcome = VerifyCurrent(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.WorkList.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
- //all non-candidate annotations as unchecked (free requires/ensures, assumes)
- public HoudiniOutcome! PerformHoudiniInference(Program! program) {
- HoudiniState current = new HoudiniState(BuildWorkList(program),BuildAssignment((!)houdiniConstants.Keys));
- this.NotifyStart(program, houdiniConstants.Keys.Count);
-
- Console.WriteLine("Using the new houdini algorithm\n");
-
- while (current.WorkList.Count > 0) {
- bool exceptional = false;
- System.GC.Collect();
- this.NotifyIteration();
-
- current.Implementation = current.WorkList.Peek();
- this.NotifyImplementation(current.Implementation);
-
- List<Counterexample!>? errors;
- VCGen.Outcome outcome = HoudiniVerifyCurrent(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 (AnyNonCandidateViolation(outcome, errors)) { //abort
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- FlushWorkList(current);
- } else { //continue
- UpdateAssignmentWorkList(current, outcome, errors);
- }
- }
- }
- this.NotifyEnd(true);
- current.Outcome.assignment = current.Assignment;
- return current.Outcome;
- }
-
-
- private List<Implementation!>! FindImplementationsToEnqueue(RefutedAnnotation! refutedAnnotation, Implementation! currentImplementation) {
- List<Implementation!>! implementations = new List<Implementation!>();
- switch (refutedAnnotation.Kind) {
- case RefutedAnnotationKind.REQUIRES:
- foreach (Implementation! callee in callGraph.NextNodes(currentImplementation)) {
- assume (callee.Proc!=null);
- if (callee.Proc.Equals(refutedAnnotation.CalleeProc))
- implementations.Add(callee);
- }
- break;
- case RefutedAnnotationKind.ENSURES:
- foreach (Implementation! caller in callGraph.PreviousNodes(currentImplementation))
- implementations.Add(caller);
- break;
- case RefutedAnnotationKind.ASSERT: //the implementation is already in queue
- break;
- default:
- throw new Exception("Unknown Refuted annotation kind:" + refutedAnnotation.Kind);
- break;
- }
- return implementations;
- }
-
- private enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT};
-
- private class RefutedAnnotation {
- private string! _constant;
- private RefutedAnnotationKind _kind;
- private Procedure _callee;
-
- private RefutedAnnotation(string! constant, RefutedAnnotationKind kind, Procedure callee) {
- this._constant = constant;
- this._kind = kind;
- this._callee = callee;
- }
- public RefutedAnnotationKind Kind {
- get { return this._kind; }
- }
- public string! Constant {
- get { return this._constant; }
- }
- public Procedure CalleeProc {
- get { return this._callee; }
- }
- public static RefutedAnnotation BuildRefutedRequires(string! constant, Procedure! callee) {
- return new RefutedAnnotation(constant,RefutedAnnotationKind.REQUIRES,callee);
- }
- public static RefutedAnnotation BuildRefutedEnsures(string! constant) {
- return new RefutedAnnotation(constant,RefutedAnnotationKind.ENSURES, null);
- }
- public static RefutedAnnotation BuildRefutedAssert(string! constant) {
- return new RefutedAnnotation(constant,RefutedAnnotationKind.ASSERT, null);
- }
-
- }
-
- private void PrintRefutedCall(CallCounterexample! err, XmlSink! xmlOut) {
- Expr! cond = err.FailingRequires.Condition;
- string houdiniConst;
- if (MatchCandidate(cond, out houdiniConst)) {
- xmlOut.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, err.Trace);
- }
- }
-
- private void PrintRefutedReturn(ReturnCounterexample! err, XmlSink! xmlOut) {
- Expr! cond = err.FailingEnsures.Condition;
- string houdiniConst;
- if (MatchCandidate(cond, out houdiniConst)) {
- xmlOut.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, err.Trace);
- }
- }
-
- private void PrintRefutedAssert(AssertCounterexample! err, XmlSink! xmlOut) {
- Expr cond = err.FailingAssert.OrigExpr;
- string houdiniConst;
- if (MatchCandidate(cond, out houdiniConst)) {
- xmlOut.WriteError("postcondition violation", err.FailingAssert.tok, err.FailingAssert.tok, err.Trace);
- }
- }
-
-
- private void DebugRefutedCandidates(Implementation! curFunc, List<Counterexample!> errors) {
- XmlSink xmlRefuted = CommandLineOptions.Clo.XmlRefuted;
- if (xmlRefuted != null && errors != null) {
- DateTime start = DateTime.Now;
- xmlRefuted.WriteStartMethod(curFunc.ToString(), start);
-
- foreach (Counterexample! error in errors) {
- CallCounterexample ce = error as CallCounterexample;
- if (ce != null) PrintRefutedCall(ce, xmlRefuted);
- ReturnCounterexample re = error as ReturnCounterexample;
- if (re != null) PrintRefutedReturn(re, xmlRefuted);
- AssertCounterexample ae = error as AssertCounterexample;
- if (ae != null) PrintRefutedAssert(ae, xmlRefuted);
- }
-
- DateTime end = DateTime.Now;
- xmlRefuted.WriteEndMethod("errors", end, end.Subtract(start));
- }
- }
-
- private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {
- string houdiniConstant;
- CallCounterexample callCounterexample = error as CallCounterexample;
- if (callCounterexample!=null) {
- Procedure! failingProcedure = (!)callCounterexample.FailingCall.Proc;
- Requires! failingRequires = (!)callCounterexample.FailingRequires;
- if (MatchCandidate(failingRequires.Condition,out houdiniConstant)) {
- assert (houdiniConstant!=null);
- return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure);
- }
- }
- ReturnCounterexample returnCounterexample = error as ReturnCounterexample;
- if (returnCounterexample!=null) {
- Ensures failingEnsures =returnCounterexample.FailingEnsures;
- if (MatchCandidate(failingEnsures.Condition,out houdiniConstant)) {
- assert (houdiniConstant!=null);
- return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant);
- }
- }
- AssertCounterexample assertCounterexample = error as AssertCounterexample;
- if (assertCounterexample!=null) {
- AssertCmd failingAssert = assertCounterexample.FailingAssert;
- if (MatchCandidate(failingAssert.OrigExpr,out houdiniConstant)) {
- assert (houdiniConstant!=null);
- return RefutedAnnotation.BuildRefutedAssert(houdiniConstant);
- }
- }
-
- return null;
- }
-
- private VCGen.Outcome TryCatchVerify(HdnVCGen! vcgen, out List<Counterexample!>? errors) {
- VCGen.Outcome outcome;
- try {
- outcome = vcgen.Verify(out errors);
- } catch (VCGenException e) {
- assume(e!=null);
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- } catch (UnexpectedProverOutputException upo) {
- assume(upo!=null);
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- 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,
- Program! program,
- HdnVCGen! vcgen,
- out List<Counterexample!>? errors,
- out bool exceptional) {
- assert (current.Implementation != null);
- VCGen.Outcome outcome;
- bool pushed = false;
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- try {
- bool trySameFunc = true;
- bool pastFirstIter = false; //see if this new loop is even helping
-
- do {
- if (pastFirstIter) {
- System.GC.Collect();
- this.NotifyIteration();
- }
- Axiom! currentAx = BuildAxiom(current.Assignment);
- this.NotifyAssignment(current.Assignment);
-
- vcgen.PushAxiom(currentAx);
- pushed = true;
- outcome = vcgen.Verify(out errors);
- vcgen.Pop();
- pushed = false;
- this.NotifyOutcome(outcome);
-
- DebugRefutedCandidates(current.Implementation, errors);
- UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
- if (!continueAtError && IsOutcomeNotHoudini(outcome,errors)) {
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- trySameFunc = false;
- FlushWorkList(current);
- } else {
- trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
- //reset for the next round
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- pastFirstIter = true;
- } while (trySameFunc && current.WorkList.Count > 0);
-
- } catch (VCGenException e) {
- assume(e!=null);
- if (pushed){
- vcgen.Pop(); // what if session is dead?
- }
- NotifyException("VCGen");
- exceptional = true;
- return outcome;
- } catch (UnexpectedProverOutputException upo) {
- assume(upo!=null);
- if (pushed){
- vcgen.Pop();
- }
- NotifyException("UnexpectedProverOutput");
- exceptional = true;
- return outcome;
- }
- exceptional = false;
- return outcome;
- }
-
-
-
- //Similar to TrySpinSameFunc except no Candidate logic
- private VCGen.Outcome HoudiniVerifyCurrentAux(HoudiniState! current,
- Program! program,
- HdnVCGen! vcgen,
- out List<Counterexample!>? errors,
- out bool exceptional) {
- assert (current.Implementation != null);
- VCGen.Outcome outcome;
- bool pushed = false;
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- try {
- bool trySameFunc = true;
- bool pastFirstIter = false; //see if this new loop is even helping
-
- do {
- if (pastFirstIter) {
- System.GC.Collect();
- this.NotifyIteration();
- }
-
- Axiom! currentAx = BuildAxiom(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;
- this.NotifyOutcome(outcome);
-
- DebugRefutedCandidates(current.Implementation, errors);
- UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
-
- if (AnyNonCandidateViolation(outcome, errors)) { //abort
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- trySameFunc = false;
- FlushWorkList(current);
- } else { //continue
- trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
- //reset for the next round
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- pastFirstIter = true;
- } while (trySameFunc && current.WorkList.Count > 0);
-
- } catch (VCGenException e) {
- assume(e!=null);
- if (pushed){
- vcgen.Pop(); // what if session is dead?
- }
- NotifyException("VCGen");
- exceptional = true;
- return outcome;
- } catch (UnexpectedProverOutputException upo) {
- assume(upo!=null);
- if (pushed){
- vcgen.Pop();
- }
- NotifyException("UnexpectedProverOutput");
- exceptional = true;
- return outcome;
- }
- exceptional = false;
- return outcome;
- }
- }
-
- public enum HoudiniOutcomeKind { Done, FatalError, VerificationCompleted }
-
- public class VCGenOutcome {
- public VCGen.Outcome outcome;
- public List<Counterexample!> errors;
- public VCGenOutcome(VCGen.Outcome outcome, List<Counterexample!> errors) {
- this.outcome = outcome;
- this.errors = errors;
- }
- }
-
- public class HoudiniOutcome {
- // final assignment
- public Dictionary<string!,bool>! assignment = new Dictionary<string!,bool>();
- // boogie errors
- public Dictionary<string!,VCGenOutcome!>! implementationOutcomes = new Dictionary<string!,VCGenOutcome!>();
- // outcome kind
- public HoudiniOutcomeKind kind;
-
- // statistics
-
- private int CountResults(VCGen.Outcome outcome) {
- int outcomeCount=0;
- foreach (VCGenOutcome! verifyOutcome in implementationOutcomes.Values) {
- if (verifyOutcome.outcome==outcome)
- outcomeCount++;
- }
- return outcomeCount;
- }
-
- private List<string!>! ListOutcomeMatches(VCGen.Outcome outcome) {
- List<string!>! result = new List<string!>();
- foreach (KeyValuePair<string!, VCGenOutcome!> kvpair in implementationOutcomes) {
- if (kvpair.Value.outcome==outcome)
- result.Add(kvpair.Key);
- }
- return result;
- }
-
- public int ErrorCount {
- get {
- return CountResults(VCGen.Outcome.Errors);
- }
- }
- public int Verified {
- get {
- return CountResults(VCGen.Outcome.Correct);
- }
- }
- public int Inconclusives {
- get {
- return CountResults(VCGen.Outcome.Inconclusive);
- }
- }
- public int TimeOuts {
- get {
- return CountResults(VCGen.Outcome.TimedOut);
- }
- }
- public List<string!>! ListOfTimeouts {
- get {
- return ListOutcomeMatches(VCGen.Outcome.TimedOut);
- }
- }
- public List<string!>! ListOfInconclusives {
- get {
- return ListOutcomeMatches(VCGen.Outcome.Inconclusive);
- }
- }
- public List<string!>! ListOfErrors {
- get {
- return ListOutcomeMatches(VCGen.Outcome.Errors);
- }
- }
- }
-
-}
diff --git a/Source/Houdini/Houdini.sscproj b/Source/Houdini/Houdini.sscproj deleted file mode 100644 index 3f68bb91..00000000 --- a/Source/Houdini/Houdini.sscproj +++ /dev/null @@ -1,118 +0,0 @@ -<?xml version="1.0" encoding="utf-8"?>
-<VisualStudioProject>
- <XEN ProjectType="Local"
- SchemaVersion="1.0"
- Name="Houdini"
- ProjectGuid="40454b39-4f61-48b2-bde3-e9271b24f469"
- >
- <Build>
- <Settings ApplicationIcon=""
- AssemblyName="Houdini"
- OutputType="Library"
- RootNamespace="Houdini"
- StartupObject=""
- StandardLibraryLocation=""
- TargetPlatform="v2"
- TargetPlatformLocation=""
- >
- <Config Name="Debug"
- AllowUnsafeBlocks="False"
- BaseAddress="285212672"
- CheckForOverflowUnderflow="False"
- ConfigurationOverrideFile=""
- DefineConstants="DEBUG;TRACE"
- DocumentationFile=""
- DebugSymbols="True"
- FileAlignment="4096"
- IncrementalBuild="True"
- Optimize="False"
- OutputPath="bin\debug"
- RegisterForComInterop="False"
- RemoveIntegerChecks="false"
- TreatWarningsAsErrors="False"
- WarningLevel="4"
- CheckContractAdmissibility="True"
- CheckPurity="False"
- />
- <Config Name="Release"
- AllowUnsafeBlocks="false"
- BaseAddress="285212672"
- CheckForOverflowUnderflow="false"
- ConfigurationOverrideFile=""
- DefineConstants="TRACE"
- DocumentationFile=""
- DebugSymbols="false"
- FileAlignment="4096"
- IncrementalBuild="false"
- Optimize="true"
- OutputPath="bin\release"
- RegisterForComInterop="false"
- RemoveIntegerChecks="false"
- TreatWarningsAsErrors="false"
- WarningLevel="4"
- CheckContractAdmissibility="True"
- CheckPurity="False"
- />
- </Settings>
- <References>
- <Reference Name="System"
- AssemblyName="System"
- Private="false"
- />
- <Reference Name="System.Data"
- AssemblyName="System.Data"
- Private="false"
- />
- <Reference Name="System.Xml"
- AssemblyName="System.Xml"
- Private="false"
- />
- <Reference Name="Core"
- Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
- Private="true"
- />
- <Reference Name="VCGeneration"
- Project="{F65666DE-FB56-457C-8782-09BE243450FC}"
- Private="true"
- />
- <Reference Name="Simplify"
- Project="{F75666DE-FB56-457C-8782-09BE243450FC}"
- Private="true"
- />
- <Reference Name="AIFramework"
- Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
- Private="true"
- />
- <Reference Name="AbsInt"
- Project="{11D06232-2039-4BCA-853B-C596E2A4EDB0}"
- Private="true"
- />
- <Reference Name="System.Compiler.Framework"
- AssemblyName="System.Compiler.Framework"
- Private="false"
- HintPath="../../Binaries/System.Compiler.Framework.dll"
- />
- <Reference Name="Z3"
- Project="{F75666DE-CD56-457C-8782-09BE243450FC}"
- Private="true"
- />
- </References>
- </Build>
- <Files>
- <Include>
- <File RelPath="Houdini.ssc"
- SubType="Code"
- BuildAction="Compile"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="Checker.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="..\version.ssc"
- />
- </Include>
- </Files>
- </XEN>
-</VisualStudioProject>
\ No newline at end of file |