summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/Check.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration/Check.cs')
-rw-r--r--Source/VCGeneration/Check.cs1381
1 files changed, 694 insertions, 687 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index da8624e9..7bda0022 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -1,687 +1,694 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Linq;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-using System.IO;
-using System.Text.RegularExpressions;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie.VCExprAST;
-using Microsoft.Basetypes;
-using System.Threading.Tasks;
-
-namespace Microsoft.Boogie {
-
- enum CheckerStatus
- {
- Idle,
- Ready,
- Busy,
- Closed
- }
-
- /// <summary>
- /// Interface to the theorem prover specialized to Boogie.
- ///
- /// This class creates the appropriate background axioms. There
- /// should be one instance per BoogiePL program.
- /// </summary>
- public sealed class Checker {
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(gen != null);
- Contract.Invariant(thmProver != null);
- }
-
- private readonly VCExpressionGenerator gen;
-
- private ProverInterface thmProver;
- private int timeout;
-
- // state for the async interface
- private volatile ProverInterface.Outcome outcome;
- private volatile bool hasOutput;
- private volatile UnexpectedProverOutputException outputExn;
- private DateTime proverStart;
- private TimeSpan proverRunTime;
- private volatile ProverInterface.ErrorHandler handler;
- private volatile CheckerStatus status;
- public volatile Program Program;
-
- public void GetReady()
- {
- Contract.Requires(IsIdle);
-
- status = CheckerStatus.Ready;
- }
-
- public void GoBackToIdle()
- {
- Contract.Requires(IsBusy);
-
- status = CheckerStatus.Idle;
- }
-
- public Task ProverTask { get; set; }
-
- public bool WillingToHandle(int timeout, Program prog) {
- return status == CheckerStatus.Idle && timeout == this.timeout && (prog == null || Program == prog);
- }
-
- public VCExpressionGenerator VCExprGen {
- get {
- Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);
- return this.gen;
- }
- }
- public ProverInterface TheoremProver {
- get {
- Contract.Ensures(Contract.Result<ProverInterface>() != null);
- return this.thmProver;
- }
- }
-
- /////////////////////////////////////////////////////////////////////////////////
- // We share context information for the same program between different Checkers
-
- private struct ContextCacheKey {
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(program != null);
- }
-
- public readonly Program program;
-
- public ContextCacheKey(Program prog) {
- Contract.Requires(prog != null);
- this.program = prog;
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object that) {
- if (that is ContextCacheKey) {
- ContextCacheKey thatKey = (ContextCacheKey)that;
- return this.program.Equals(thatKey.program);
- }
- return false;
- }
-
- [Pure]
- public override int GetHashCode() {
- return this.program.GetHashCode();
- }
- }
-
- /////////////////////////////////////////////////////////////////////////////////
-
- /// <summary>
- /// Constructor. Initialize a checker with the program and log file.
- /// Optionally, use prover context provided by parameter "ctx".
- /// </summary>
- public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, ProverContext ctx = null) {
- Contract.Requires(vcgen != null);
- Contract.Requires(prog != null);
- this.timeout = timeout;
- this.Program = prog;
-
- ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
-
- if (logFilePath != null) {
- options.LogFilename = logFilePath;
- if (appendLogFile)
- options.AppendLogFile = appendLogFile;
- }
-
- if (timeout > 0) {
- options.TimeLimit = timeout * 1000;
- }
-
- options.Parse(CommandLineOptions.Clo.ProverOptions);
-
- ContextCacheKey key = new ContextCacheKey(prog);
- ProverInterface prover;
-
- if (vcgen.CheckerCommonState == null) {
- vcgen.CheckerCommonState = new Dictionary<ContextCacheKey, ProverContext>();
- }
- IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>)vcgen.CheckerCommonState;
-
- if (ctx == null && cachedContexts.TryGetValue(key, out ctx))
- {
- ctx = (ProverContext)cce.NonNull(ctx).Clone();
- prover = (ProverInterface)
- CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
- } else {
- if (ctx == null) ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
-
- Setup(prog, ctx);
-
- // we first generate the prover and then store a clone of the
- // context in the cache, so that the prover can setup stuff in
- // the context to be cached
- prover = (ProverInterface)
- CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
- cachedContexts.Add(key, cce.NonNull((ProverContext)ctx.Clone()));
- }
-
- this.thmProver = prover;
- this.gen = prover.VCExprGen;
- }
-
- public void Retarget(Program prog, ProverContext ctx, int timeout = 0)
- {
- lock (this)
- {
- hasOutput = default(bool);
- outcome = default(ProverInterface.Outcome);
- outputExn = default(UnexpectedProverOutputException);
- handler = default(ProverInterface.ErrorHandler);
- TheoremProver.FullReset(gen);
- ctx.Reset();
- Setup(prog, ctx);
- this.timeout = timeout;
- SetTimeout();
- }
- }
-
- public void RetargetWithoutReset(Program prog, ProverContext ctx)
- {
- ctx.Clear();
- Setup(prog, ctx);
- }
-
-
- public void SetTimeout()
- {
- if (0 < timeout)
- {
- TheoremProver.SetTimeOut(timeout * 1000);
- }
- else
- {
- TheoremProver.SetTimeOut(0);
- }
- }
-
- /// <summary>
- /// Set up the context.
- /// </summary>
- private void Setup(Program prog, ProverContext ctx)
- {
- Program = prog;
- lock (Program.TopLevelDeclarations)
- {
- foreach (Declaration decl in Program.TopLevelDeclarations)
- {
- Contract.Assert(decl != null);
- var typeDecl = decl as TypeCtorDecl;
- var constDecl = decl as Constant;
- var funDecl = decl as Function;
- var axiomDecl = decl as Axiom;
- var glVarDecl = decl as GlobalVariable;
- if (typeDecl != null)
- {
- ctx.DeclareType(typeDecl, null);
- }
- else if (constDecl != null)
- {
- ctx.DeclareConstant(constDecl, constDecl.Unique, null);
- }
- else if (funDecl != null)
- {
- ctx.DeclareFunction(funDecl, null);
- }
- else if (axiomDecl != null)
- {
- ctx.AddAxiom(axiomDecl, null);
- }
- else if (glVarDecl != null)
- {
- ctx.DeclareGlobalVariable(glVarDecl, null);
- }
- }
- }
- }
-
- /// <summary>
- /// Clean-up.
- /// </summary>
- public void Close() {
- thmProver.Close();
- status = CheckerStatus.Closed;
- }
-
- /// <summary>
- /// Push a Verification Condition as an Axiom
- /// (Required for Doomed Program Point detection)
- /// </summary>
- public void PushVCExpr(VCExpr vc) {
- Contract.Requires(vc != null);
- //thmProver.Context.AddAxiom(vc);
- thmProver.PushVCExpression(vc);
- }
-
- public bool IsBusy {
- get {
- return status == CheckerStatus.Busy;
- }
- }
-
- public bool IsReady
- {
- get
- {
- return status == CheckerStatus.Ready;
- }
- }
-
- public bool IsClosed {
- get {
- return status == CheckerStatus.Closed;
- }
- }
-
- public bool IsIdle
- {
- get
- {
- return status == CheckerStatus.Idle;
- }
- }
-
- public bool HasOutput {
- get {
- return hasOutput;
- }
- }
-
- public TimeSpan ProverRunTime {
- get {
- return proverRunTime;
- }
- }
-
- private void WaitForOutput(object dummy) {
- lock (this)
- {
- try
- {
- outcome = thmProver.CheckOutcome(cce.NonNull(handler));
- }
- catch (UnexpectedProverOutputException e)
- {
- outputExn = e;
- }
-
- switch (outcome)
- {
- case ProverInterface.Outcome.Valid:
- thmProver.LogComment("Valid");
- break;
- case ProverInterface.Outcome.Invalid:
- thmProver.LogComment("Invalid");
- break;
- case ProverInterface.Outcome.TimeOut:
- thmProver.LogComment("Timed out");
- break;
- case ProverInterface.Outcome.OutOfMemory:
- thmProver.LogComment("Out of memory");
- break;
- case ProverInterface.Outcome.Undetermined:
- thmProver.LogComment("Undetermined");
- break;
- }
-
- hasOutput = true;
- proverRunTime = DateTime.UtcNow - proverStart;
- }
- }
-
- public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
- Contract.Requires(descriptiveName != null);
- Contract.Requires(vc != null);
- Contract.Requires(handler != null);
- Contract.Requires(IsReady);
-
- status = CheckerStatus.Busy;
- hasOutput = false;
- outputExn = null;
- this.handler = handler;
-
- thmProver.Reset(gen);
- SetTimeout();
- proverStart = DateTime.UtcNow;
- thmProver.BeginCheck(descriptiveName, vc, handler);
- // gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
-
- ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); } , TaskCreationOptions.LongRunning);
- }
-
- public ProverInterface.Outcome ReadOutcome() {
- Contract.Requires(IsBusy);
- Contract.Requires(HasOutput);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- hasOutput = false;
-
- if (outputExn != null) {
- throw outputExn;
- }
-
- return outcome;
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public abstract class ProverInterface {
- public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
- Contract.Requires(prog != null);
-
- ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
-
- if (logFilePath != null) {
- options.LogFilename = logFilePath;
- if (appendLogFile)
- options.AppendLogFile = appendLogFile;
- }
-
- if (timeout > 0) {
- options.TimeLimit = timeout * 1000;
- }
-
- if (taskID >= 0) {
- options.Parse(CommandLineOptions.Clo.Cho[taskID].ProverOptions);
- } else {
- options.Parse(CommandLineOptions.Clo.ProverOptions);
- }
-
- ProverContext ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
-
- // set up the context
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- TypeCtorDecl t = decl as TypeCtorDecl;
- if (t != null) {
- ctx.DeclareType(t, null);
- }
- }
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- Constant c = decl as Constant;
- if (c != null) {
- ctx.DeclareConstant(c, c.Unique, null);
- }
- else {
- Function f = decl as Function;
- if (f != null) {
- ctx.DeclareFunction(f, null);
- }
- }
- }
- foreach (var ax in prog.Axioms) {
- ctx.AddAxiom(ax, null);
- }
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- GlobalVariable v = decl as GlobalVariable;
- if (v != null) {
- ctx.DeclareGlobalVariable(v, null);
- }
- }
-
- return (ProverInterface)CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
- }
-
- public enum Outcome {
- Valid,
- Invalid,
- TimeOut,
- OutOfMemory,
- Undetermined
- }
- public class ErrorHandler {
- // Used in CheckOutcomeCore
- public virtual int StartingProcId()
- {
- return 0;
- }
-
- public virtual void OnModel(IList<string> labels, Model model, Outcome proverOutcome) {
- Contract.Requires(cce.NonNullElements(labels));
- }
-
- public virtual void OnResourceExceeded(string message) {
- Contract.Requires(message != null);
- }
-
- public virtual void OnProverWarning(string message)
- {
- Contract.Requires(message != null);
- switch (CommandLineOptions.Clo.PrintProverWarnings) {
- case CommandLineOptions.ProverWarnings.None:
- break;
- case CommandLineOptions.ProverWarnings.Stdout:
- Console.WriteLine("Prover warning: " + message);
- break;
- case CommandLineOptions.ProverWarnings.Stderr:
- Console.Error.WriteLine("Prover warning: " + message);
- break;
- default:
- Contract.Assume(false);
- throw new cce.UnreachableException(); // unexpected case
- }
- }
-
- public virtual Absy Label2Absy(string label) {
- Contract.Requires(label != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
-
- throw new System.NotImplementedException();
- }
- }
- public abstract void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler);
-
- public virtual Outcome CheckRPFP(string descriptiveName, RPFP vc, ErrorHandler handler,
- out RPFP.Node cex,
- Dictionary<int, Dictionary<string, string>> varSubst, Dictionary<string,int> extra_bound = null)
- {
- throw new System.NotImplementedException();
- }
- [NoDefaultContract]
- public abstract Outcome CheckOutcome(ErrorHandler handler, int taskID = -1);
- public virtual string[] CalculatePath(int controlFlowConstant) {
- throw new System.NotImplementedException();
- }
- public virtual void LogComment(string comment) {
- Contract.Requires(comment != null);
- }
- public virtual void Close() {
- }
-
- public abstract void Reset(VCExpressionGenerator gen);
-
- public abstract void FullReset(VCExpressionGenerator gen);
-
- /// <summary>
- /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
- /// for now it is only implemented by ProcessTheoremProver and still requires some
- /// testing
- /// </summary>
- public virtual void PushVCExpression(VCExpr vc) {
- Contract.Requires(vc != null);
- throw new NotImplementedException();
- }
- public virtual string VCExpressionToString(VCExpr vc) {
- Contract.Requires(vc != null);
- Contract.Ensures(Contract.Result<string>() != null);
- throw new NotImplementedException();
- }
- public virtual void Pop() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- throw new NotImplementedException();
- }
- public virtual int NumAxiomsPushed() {
- throw new NotImplementedException();
- }
- public virtual int FlushAxiomsToTheoremProver() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- throw new NotImplementedException();
- }
-
- // (assert vc)
- public virtual void Assert(VCExpr vc, bool polarity)
- {
- throw new NotImplementedException();
- }
-
- // (assert implicit-axioms)
- public virtual void AssertAxioms()
- {
- throw new NotImplementedException();
- }
-
- // (check-sat)
- public virtual void Check()
- {
- throw new NotImplementedException();
- }
-
- // (check-sat + get-unsat-core + checkOutcome)
- public virtual Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)
- {
- throw new NotImplementedException();
- }
-
- public virtual Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions, out List<int> unsatisfiedSoftAssumptions, ErrorHandler handler) {
- throw new NotImplementedException();
- }
-
- public virtual Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1)
- {
- throw new NotImplementedException();
- }
-
- // (push 1)
- public virtual void Push()
- {
- throw new NotImplementedException();
- }
-
- // Set theorem prover timeout for the next "check-sat"
- public virtual void SetTimeOut(int ms)
- { }
-
- public abstract ProverContext Context {
- get;
- }
-
- public abstract VCExpressionGenerator VCExprGen {
- get;
- }
-
- public virtual void DefineMacro(Macro fun, VCExpr vc) {
- throw new NotImplementedException();
- }
-
- public class VCExprEvaluationException : Exception
- {
-
- }
-
- public virtual object Evaluate(VCExpr expr)
- {
- throw new NotImplementedException();
- }
-
- //////////////////////
- // For interpolation queries
- //////////////////////
-
- // Assert vc tagged with a name
- public virtual void AssertNamed(VCExpr vc, bool polarity, string name)
- {
- throw new NotImplementedException();
- }
-
- // Returns Interpolant(A,B)
- public virtual VCExpr ComputeInterpolant(VCExpr A, VCExpr B)
- {
- throw new NotImplementedException();
- }
-
- // Returns for each l, Interpolant(root + (leaves - l), l)
- // Preconditions:
- // leaves cannot have subformulas with same variable names
- // Both root and leaves should have been previously named via AssertNamed
- public virtual List<VCExpr> GetTreeInterpolant(List<string> root, List<string> leaves)
- {
- throw new NotImplementedException();
- }
-
- }
-
- public class ProverInterfaceContracts : ProverInterface {
- public override ProverContext Context {
- get {
- Contract.Ensures(Contract.Result<ProverContext>() != null);
-
- throw new NotImplementedException();
- }
- }
- public override VCExpressionGenerator VCExprGen {
- get {
- Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);
-
- throw new NotImplementedException();
- }
- }
- public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {/*Contract.Requires(descriptiveName != null);*/
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- throw new NotImplementedException();
- }
- [NoDefaultContract]
- public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1) {
- //Contract.Requires(handler != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- throw new NotImplementedException();
- }
-
- public override void Reset(VCExpressionGenerator gen)
- {
- throw new NotImplementedException();
- }
-
- public override void FullReset(VCExpressionGenerator gen)
- {
- throw new NotImplementedException();
- }
- }
-
- public class ProverException : Exception {
- public ProverException(string s)
- : base(s) {
- }
- }
- public class UnexpectedProverOutputException : ProverException {
- public UnexpectedProverOutputException(string s)
- : base(s) {
- }
- }
- public class ProverDiedException : UnexpectedProverOutputException {
- public ProverDiedException()
- : base("Prover died with no further output, perhaps it ran out of memory or was killed.") {
- }
- }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Linq;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Text.RegularExpressions;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Basetypes;
+using System.Threading.Tasks;
+
+namespace Microsoft.Boogie {
+
+ enum CheckerStatus
+ {
+ Idle,
+ Ready,
+ Busy,
+ Closed
+ }
+
+ /// <summary>
+ /// Interface to the theorem prover specialized to Boogie.
+ ///
+ /// This class creates the appropriate background axioms. There
+ /// should be one instance per BoogiePL program.
+ /// </summary>
+ public sealed class Checker {
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(gen != null);
+ Contract.Invariant(thmProver != null);
+ }
+
+ private readonly VCExpressionGenerator gen;
+
+ private ProverInterface thmProver;
+ private int timeout;
+
+ // state for the async interface
+ private volatile ProverInterface.Outcome outcome;
+ private volatile bool hasOutput;
+ private volatile UnexpectedProverOutputException outputExn;
+ private DateTime proverStart;
+ private TimeSpan proverRunTime;
+ private volatile ProverInterface.ErrorHandler handler;
+ private volatile CheckerStatus status;
+ public volatile Program Program;
+
+ public void GetReady()
+ {
+ Contract.Requires(IsIdle);
+
+ status = CheckerStatus.Ready;
+ }
+
+ public void GoBackToIdle()
+ {
+ Contract.Requires(IsBusy);
+
+ status = CheckerStatus.Idle;
+ }
+
+ public Task ProverTask { get; set; }
+
+ public bool WillingToHandle(int timeout, Program prog) {
+ return status == CheckerStatus.Idle && timeout == this.timeout && (prog == null || Program == prog);
+ }
+
+ public VCExpressionGenerator VCExprGen {
+ get {
+ Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);
+ return this.gen;
+ }
+ }
+ public ProverInterface TheoremProver {
+ get {
+ Contract.Ensures(Contract.Result<ProverInterface>() != null);
+ return this.thmProver;
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // We share context information for the same program between different Checkers
+
+ private struct ContextCacheKey {
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(program != null);
+ }
+
+ public readonly Program program;
+
+ public ContextCacheKey(Program prog) {
+ Contract.Requires(prog != null);
+ this.program = prog;
+ }
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (that is ContextCacheKey) {
+ ContextCacheKey thatKey = (ContextCacheKey)that;
+ return this.program.Equals(thatKey.program);
+ }
+ return false;
+ }
+
+ [Pure]
+ public override int GetHashCode() {
+ return this.program.GetHashCode();
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+
+ /// <summary>
+ /// Constructor. Initialize a checker with the program and log file.
+ /// Optionally, use prover context provided by parameter "ctx".
+ /// </summary>
+ public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, ProverContext ctx = null) {
+ Contract.Requires(vcgen != null);
+ Contract.Requires(prog != null);
+ this.timeout = timeout;
+ this.Program = prog;
+
+ ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
+
+ if (logFilePath != null) {
+ options.LogFilename = logFilePath;
+ if (appendLogFile)
+ options.AppendLogFile = appendLogFile;
+ }
+
+ if (timeout > 0) {
+ options.TimeLimit = timeout * 1000;
+ }
+
+ options.Parse(CommandLineOptions.Clo.ProverOptions);
+
+ ContextCacheKey key = new ContextCacheKey(prog);
+ ProverInterface prover;
+
+ if (vcgen.CheckerCommonState == null) {
+ vcgen.CheckerCommonState = new Dictionary<ContextCacheKey, ProverContext>();
+ }
+ IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>)vcgen.CheckerCommonState;
+
+ if (ctx == null && cachedContexts.TryGetValue(key, out ctx))
+ {
+ ctx = (ProverContext)cce.NonNull(ctx).Clone();
+ prover = (ProverInterface)
+ CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
+ } else {
+ if (ctx == null) ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
+
+ Setup(prog, ctx);
+
+ // we first generate the prover and then store a clone of the
+ // context in the cache, so that the prover can setup stuff in
+ // the context to be cached
+ prover = (ProverInterface)
+ CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
+ cachedContexts.Add(key, cce.NonNull((ProverContext)ctx.Clone()));
+ }
+
+ this.thmProver = prover;
+ this.gen = prover.VCExprGen;
+ }
+
+ public void Retarget(Program prog, ProverContext ctx, int timeout = 0)
+ {
+ lock (this)
+ {
+ hasOutput = default(bool);
+ outcome = default(ProverInterface.Outcome);
+ outputExn = default(UnexpectedProverOutputException);
+ handler = default(ProverInterface.ErrorHandler);
+ TheoremProver.FullReset(gen);
+ ctx.Reset();
+ Setup(prog, ctx);
+ this.timeout = timeout;
+ SetTimeout();
+ }
+ }
+
+ public void RetargetWithoutReset(Program prog, ProverContext ctx)
+ {
+ ctx.Clear();
+ Setup(prog, ctx);
+ }
+
+
+ public void SetTimeout()
+ {
+ if (0 < timeout)
+ {
+ TheoremProver.SetTimeOut(timeout * 1000);
+ }
+ else
+ {
+ TheoremProver.SetTimeOut(0);
+ }
+ }
+
+ /// <summary>
+ /// Set up the context.
+ /// </summary>
+ private void Setup(Program prog, ProverContext ctx)
+ {
+ Program = prog;
+ // TODO(wuestholz): Is this lock necessary?
+ lock (Program.TopLevelDeclarations)
+ {
+ foreach (Declaration decl in Program.TopLevelDeclarations)
+ {
+ Contract.Assert(decl != null);
+ var typeDecl = decl as TypeCtorDecl;
+ var constDecl = decl as Constant;
+ var funDecl = decl as Function;
+ var axiomDecl = decl as Axiom;
+ var glVarDecl = decl as GlobalVariable;
+ if (typeDecl != null)
+ {
+ ctx.DeclareType(typeDecl, null);
+ }
+ else if (constDecl != null)
+ {
+ ctx.DeclareConstant(constDecl, constDecl.Unique, null);
+ }
+ else if (funDecl != null)
+ {
+ ctx.DeclareFunction(funDecl, null);
+ }
+ else if (axiomDecl != null)
+ {
+ ctx.AddAxiom(axiomDecl, null);
+ }
+ else if (glVarDecl != null)
+ {
+ ctx.DeclareGlobalVariable(glVarDecl, null);
+ }
+ }
+ }
+ }
+
+ /// <summary>
+ /// Clean-up.
+ /// </summary>
+ public void Close() {
+ thmProver.Close();
+ status = CheckerStatus.Closed;
+ }
+
+ /// <summary>
+ /// Push a Verification Condition as an Axiom
+ /// (Required for Doomed Program Point detection)
+ /// </summary>
+ public void PushVCExpr(VCExpr vc) {
+ Contract.Requires(vc != null);
+ //thmProver.Context.AddAxiom(vc);
+ thmProver.PushVCExpression(vc);
+ }
+
+ public bool IsBusy {
+ get {
+ return status == CheckerStatus.Busy;
+ }
+ }
+
+ public bool IsReady
+ {
+ get
+ {
+ return status == CheckerStatus.Ready;
+ }
+ }
+
+ public bool IsClosed {
+ get {
+ return status == CheckerStatus.Closed;
+ }
+ }
+
+ public bool IsIdle
+ {
+ get
+ {
+ return status == CheckerStatus.Idle;
+ }
+ }
+
+ public bool HasOutput {
+ get {
+ return hasOutput;
+ }
+ }
+
+ public TimeSpan ProverRunTime {
+ get {
+ return proverRunTime;
+ }
+ }
+
+ private void WaitForOutput(object dummy) {
+ lock (this)
+ {
+ try
+ {
+ outcome = thmProver.CheckOutcome(cce.NonNull(handler));
+ }
+ catch (UnexpectedProverOutputException e)
+ {
+ outputExn = e;
+ }
+
+ switch (outcome)
+ {
+ case ProverInterface.Outcome.Valid:
+ thmProver.LogComment("Valid");
+ break;
+ case ProverInterface.Outcome.Invalid:
+ thmProver.LogComment("Invalid");
+ break;
+ case ProverInterface.Outcome.TimeOut:
+ thmProver.LogComment("Timed out");
+ break;
+ case ProverInterface.Outcome.OutOfMemory:
+ thmProver.LogComment("Out of memory");
+ break;
+ case ProverInterface.Outcome.Undetermined:
+ thmProver.LogComment("Undetermined");
+ break;
+ }
+
+ hasOutput = true;
+ proverRunTime = DateTime.UtcNow - proverStart;
+ }
+ }
+
+ public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
+ Contract.Requires(descriptiveName != null);
+ Contract.Requires(vc != null);
+ Contract.Requires(handler != null);
+ Contract.Requires(IsReady);
+
+ status = CheckerStatus.Busy;
+ hasOutput = false;
+ outputExn = null;
+ this.handler = handler;
+
+ thmProver.Reset(gen);
+ SetTimeout();
+ proverStart = DateTime.UtcNow;
+ thmProver.BeginCheck(descriptiveName, vc, handler);
+ // gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
+
+ ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); }, TaskCreationOptions.LongRunning);
+ }
+
+ public ProverInterface.Outcome ReadOutcome() {
+ Contract.Requires(IsBusy);
+ Contract.Requires(HasOutput);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+
+ hasOutput = false;
+
+ if (outputExn != null) {
+ throw outputExn;
+ }
+
+ return outcome;
+ }
+ }
+
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+
+ public abstract class ProverInterface {
+
+ public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
+ Contract.Requires(prog != null);
+
+ ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
+
+ if (logFilePath != null) {
+ options.LogFilename = logFilePath;
+ if (appendLogFile)
+ options.AppendLogFile = appendLogFile;
+ }
+
+ if (timeout > 0) {
+ options.TimeLimit = timeout * 1000;
+ }
+
+ if (taskID >= 0) {
+ options.Parse(CommandLineOptions.Clo.Cho[taskID].ProverOptions);
+ } else {
+ options.Parse(CommandLineOptions.Clo.ProverOptions);
+ }
+
+ ProverContext ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
+
+ // set up the context
+ foreach (Declaration decl in prog.TopLevelDeclarations) {
+ Contract.Assert(decl != null);
+ TypeCtorDecl t = decl as TypeCtorDecl;
+ if (t != null) {
+ ctx.DeclareType(t, null);
+ }
+ }
+ foreach (Declaration decl in prog.TopLevelDeclarations) {
+ Contract.Assert(decl != null);
+ Constant c = decl as Constant;
+ if (c != null) {
+ ctx.DeclareConstant(c, c.Unique, null);
+ }
+ else {
+ Function f = decl as Function;
+ if (f != null) {
+ ctx.DeclareFunction(f, null);
+ }
+ }
+ }
+ foreach (var ax in prog.Axioms) {
+ ctx.AddAxiom(ax, null);
+ }
+ foreach (Declaration decl in prog.TopLevelDeclarations) {
+ Contract.Assert(decl != null);
+ GlobalVariable v = decl as GlobalVariable;
+ if (v != null) {
+ ctx.DeclareGlobalVariable(v, null);
+ }
+ }
+
+ return (ProverInterface)CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
+ }
+
+ public enum Outcome {
+ Valid,
+ Invalid,
+ TimeOut,
+ OutOfMemory,
+ Undetermined,
+ Bounded
+ }
+
+ public readonly ISet<VCExprVar> NamedAssumes = new HashSet<VCExprVar>();
+ public ISet<string> UsedNamedAssumes { get; protected set; }
+
+ public class ErrorHandler {
+ // Used in CheckOutcomeCore
+ public virtual int StartingProcId()
+ {
+ return 0;
+ }
+
+ public virtual void OnModel(IList<string> labels, Model model, Outcome proverOutcome) {
+ Contract.Requires(cce.NonNullElements(labels));
+ }
+
+ public virtual void OnResourceExceeded(string message, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null) {
+ Contract.Requires(message != null);
+ }
+
+ public virtual void OnProverWarning(string message)
+ {
+ Contract.Requires(message != null);
+ switch (CommandLineOptions.Clo.PrintProverWarnings) {
+ case CommandLineOptions.ProverWarnings.None:
+ break;
+ case CommandLineOptions.ProverWarnings.Stdout:
+ Console.WriteLine("Prover warning: " + message);
+ break;
+ case CommandLineOptions.ProverWarnings.Stderr:
+ Console.Error.WriteLine("Prover warning: " + message);
+ break;
+ default:
+ Contract.Assume(false);
+ throw new cce.UnreachableException(); // unexpected case
+ }
+ }
+
+ public virtual Absy Label2Absy(string label) {
+ Contract.Requires(label != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+
+ throw new System.NotImplementedException();
+ }
+ }
+ public abstract void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler);
+
+ public virtual Outcome CheckRPFP(string descriptiveName, RPFP vc, ErrorHandler handler,
+ out RPFP.Node cex,
+ Dictionary<int, Dictionary<string, string>> varSubst, Dictionary<string,int> extra_bound = null)
+ {
+ throw new System.NotImplementedException();
+ }
+ [NoDefaultContract]
+ public abstract Outcome CheckOutcome(ErrorHandler handler, int taskID = -1);
+ public virtual string[] CalculatePath(int controlFlowConstant) {
+ throw new System.NotImplementedException();
+ }
+ public virtual void LogComment(string comment) {
+ Contract.Requires(comment != null);
+ }
+ public virtual void Close() {
+ }
+
+ public abstract void Reset(VCExpressionGenerator gen);
+
+ public abstract void FullReset(VCExpressionGenerator gen);
+
+ /// <summary>
+ /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
+ /// for now it is only implemented by ProcessTheoremProver and still requires some
+ /// testing
+ /// </summary>
+ public virtual void PushVCExpression(VCExpr vc) {
+ Contract.Requires(vc != null);
+ throw new NotImplementedException();
+ }
+ public virtual string VCExpressionToString(VCExpr vc) {
+ Contract.Requires(vc != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ throw new NotImplementedException();
+ }
+ public virtual void Pop() {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ throw new NotImplementedException();
+ }
+ public virtual int NumAxiomsPushed() {
+ throw new NotImplementedException();
+ }
+ public virtual int FlushAxiomsToTheoremProver() {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ throw new NotImplementedException();
+ }
+
+ // (assert vc)
+ public virtual void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1)
+ {
+ throw new NotImplementedException();
+ }
+
+ // (assert implicit-axioms)
+ public virtual void AssertAxioms()
+ {
+ throw new NotImplementedException();
+ }
+
+ // (check-sat)
+ public virtual void Check()
+ {
+ throw new NotImplementedException();
+ }
+
+ // (check-sat + get-unsat-core + checkOutcome)
+ public virtual Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)
+ {
+ throw new NotImplementedException();
+ }
+
+ public virtual Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions, out List<int> unsatisfiedSoftAssumptions, ErrorHandler handler) {
+ throw new NotImplementedException();
+ }
+
+ public virtual Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1)
+ {
+ throw new NotImplementedException();
+ }
+
+ // (push 1)
+ public virtual void Push()
+ {
+ throw new NotImplementedException();
+ }
+
+ // Set theorem prover timeout for the next "check-sat"
+ public virtual void SetTimeOut(int ms)
+ { }
+
+ public abstract ProverContext Context {
+ get;
+ }
+
+ public abstract VCExpressionGenerator VCExprGen {
+ get;
+ }
+
+ public virtual void DefineMacro(Macro fun, VCExpr vc) {
+ throw new NotImplementedException();
+ }
+
+ public class VCExprEvaluationException : Exception
+ {
+
+ }
+
+ public virtual object Evaluate(VCExpr expr)
+ {
+ throw new NotImplementedException();
+ }
+
+ //////////////////////
+ // For interpolation queries
+ //////////////////////
+
+ // Assert vc tagged with a name
+ public virtual void AssertNamed(VCExpr vc, bool polarity, string name)
+ {
+ throw new NotImplementedException();
+ }
+
+ // Returns Interpolant(A,B)
+ public virtual VCExpr ComputeInterpolant(VCExpr A, VCExpr B)
+ {
+ throw new NotImplementedException();
+ }
+
+ // Returns for each l, Interpolant(root + (leaves - l), l)
+ // Preconditions:
+ // leaves cannot have subformulas with same variable names
+ // Both root and leaves should have been previously named via AssertNamed
+ public virtual List<VCExpr> GetTreeInterpolant(List<string> root, List<string> leaves)
+ {
+ throw new NotImplementedException();
+ }
+
+ }
+
+ public class ProverInterfaceContracts : ProverInterface {
+ public override ProverContext Context {
+ get {
+ Contract.Ensures(Contract.Result<ProverContext>() != null);
+
+ throw new NotImplementedException();
+ }
+ }
+ public override VCExpressionGenerator VCExprGen {
+ get {
+ Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);
+
+ throw new NotImplementedException();
+ }
+ }
+ public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {/*Contract.Requires(descriptiveName != null);*/
+ //Contract.Requires(vc != null);
+ //Contract.Requires(handler != null);
+ throw new NotImplementedException();
+ }
+ [NoDefaultContract]
+ public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1) {
+ //Contract.Requires(handler != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ throw new NotImplementedException();
+ }
+
+ public override void Reset(VCExpressionGenerator gen)
+ {
+ throw new NotImplementedException();
+ }
+
+ public override void FullReset(VCExpressionGenerator gen)
+ {
+ throw new NotImplementedException();
+ }
+ }
+
+ public class ProverException : Exception {
+ public ProverException(string s)
+ : base(s) {
+ }
+ }
+ public class UnexpectedProverOutputException : ProverException {
+ public UnexpectedProverOutputException(string s)
+ : base(s) {
+ }
+ }
+ public class ProverDiedException : UnexpectedProverOutputException {
+ public ProverDiedException()
+ : base("Prover died with no further output, perhaps it ran out of memory or was killed.") {
+ }
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 11:54:11 +0000