diff options
Diffstat (limited to 'Source/VCGeneration/Check.cs')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 505 |
1 files changed, 505 insertions, 0 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs new file mode 100644 index 00000000..4bd6edea --- /dev/null +++ b/Source/VCGeneration/Check.cs @@ -0,0 +1,505 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Basetypes;
+
+namespace Microsoft.Boogie
+{
+ /// <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
+ {
+ private readonly VCExpressionGenerator! gen;
+
+ private ProverInterface! thmProver;
+ private CommandLineOptions.BvHandling bitvectors;
+ private int timeout;
+
+ // state for the async interface
+ private volatile ProverInterface.Outcome outcome;
+ private volatile bool busy;
+ private volatile bool hasOutput;
+ private volatile UnexpectedProverOutputException outputExn;
+ private DateTime proverStart;
+ private TimeSpan proverRunTime;
+ private volatile ProverInterface.ErrorHandler handler;
+ private volatile bool closed;
+
+ public readonly AutoResetEvent! ProverDone = new AutoResetEvent(false);
+
+ private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl)
+ {
+ if (impl == null) return CommandLineOptions.Clo.Bitvectors;
+ bool force_int = false;
+ bool force_native = false;
+ ((!)impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int);
+ impl.Proc.CheckBooleanAttribute("forceBvZ3Native", ref force_native);
+ impl.CheckBooleanAttribute("forceBvInt", ref force_int);
+ impl.CheckBooleanAttribute("forceBvZ3Native", ref force_native);
+ if (force_native) return CommandLineOptions.BvHandling.Z3Native;
+ if (force_int) return CommandLineOptions.BvHandling.ToInt;
+ return CommandLineOptions.Clo.Bitvectors;
+ }
+
+ public bool WillingToHandle(Implementation impl, int timeout)
+ {
+ return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl);
+ }
+
+ public VCExpressionGenerator! VCExprGen
+ {
+ get { return this.gen; }
+ }
+ public ProverInterface! TheoremProver
+ {
+ get { return this.thmProver; }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // We share context information for the same program between different Checkers
+
+ private struct ContextCacheKey {
+ public readonly Program! program;
+ public readonly CommandLineOptions.BvHandling bitvectors;
+
+ public ContextCacheKey(Program! prog,
+ CommandLineOptions.BvHandling bitvectors) {
+ this.program = prog;
+ this.bitvectors = bitvectors;
+ }
+
+ [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) &&
+ this.bitvectors.Equals(thatKey.bitvectors);
+ }
+ return false;
+ }
+
+ [Pure]
+ public override int GetHashCode() {
+ return this.program.GetHashCode() + this.bitvectors.GetHashCode();
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+
+ /// <summary>
+ /// Constructor. Initialize a checker with the program and log file.
+ /// </summary>
+ public Checker(VC.ConditionGeneration! vcgen, Program! prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout)
+ {
+ this.bitvectors = BvHandlingForImpl(impl);
+ this.timeout = timeout;
+
+ ProverOptions! options = ((!)CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
+
+ if (logFilePath != null) {
+ options.LogFilename = logFilePath;
+ if (appendLogFile)
+ options.AppendLogFile = appendLogFile;
+ }
+
+ options.Parse(CommandLineOptions.Clo.ProverOptions);
+
+ if (timeout > 0) {
+ options.TimeLimit = timeout * 1000;
+ }
+ options.BitVectors = this.bitvectors;
+
+ ContextCacheKey key = new ContextCacheKey (prog, this.bitvectors);
+ ProverContext ctx;
+ ProverInterface prover;
+
+ if (vcgen.CheckerCommonState == null) {
+ vcgen.CheckerCommonState = new Dictionary<ContextCacheKey, ProverContext!> ();
+ }
+ IDictionary<ContextCacheKey, ProverContext!>! cachedContexts = (IDictionary<ContextCacheKey, ProverContext!>) vcgen.CheckerCommonState;
+
+ if (cachedContexts.TryGetValue(key, out ctx)) {
+ ctx = (ProverContext!)((!)ctx).Clone();
+ prover = (ProverInterface)
+ CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
+ } else {
+ ctx = (ProverContext!)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
+
+ // set up the context
+ foreach (Declaration! decl in prog.TopLevelDeclarations) {
+ TypeCtorDecl t = decl as TypeCtorDecl;
+ if (t != null) {
+ ctx.DeclareType(t, null);
+ }
+ }
+ foreach (Declaration! decl in prog.TopLevelDeclarations) {
+ 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 (Declaration! decl in prog.TopLevelDeclarations) {
+ bool expand = false;
+ Axiom ax = decl as Axiom;
+ decl.CheckBooleanAttribute("inline", ref expand);
+ if (!expand && ax != null) {
+ ctx.AddAxiom(ax, null);
+ }
+ }
+ foreach (Declaration! decl in prog.TopLevelDeclarations) {
+ GlobalVariable v = decl as GlobalVariable;
+ if (v != null) {
+ ctx.DeclareGlobalVariable(v, null);
+ }
+ }
+
+ // 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, (ProverContext!)ctx.Clone());
+ }
+
+ this.thmProver = prover;
+ this.gen = prover.VCExprGen;
+
+ // base();
+ }
+
+
+ /// <summary>
+ /// Clean-up.
+ /// </summary>
+ public void Close()
+ {
+ this.closed = true;
+ thmProver.Close();
+ }
+
+ /// <summary>
+ /// Push a Verification Condition as an Axiom
+ /// (Required for Doomed Program Point detection)
+ /// </summary>
+ public void PushVCExpr(VCExpr! vc)
+ {
+ //thmProver.Context.AddAxiom(vc);
+ thmProver.PushVCExpression(vc);
+ }
+
+ public bool IsBusy
+ {
+ get { return busy; }
+ }
+
+ public bool Closed
+ {
+ get { return closed; }
+ }
+
+ public bool HasOutput
+ {
+ get { return hasOutput; }
+ }
+
+ public TimeSpan ProverRunTime
+ {
+ get { return proverRunTime; }
+ }
+
+ private void WaitForOutput(object dummy)
+ {
+ try {
+ outcome = thmProver.CheckOutcome((!)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;
+ }
+
+ assert busy;
+ hasOutput = true;
+ proverRunTime = DateTime.Now - proverStart;
+
+ ProverDone.Set();
+ }
+
+ public void BeginCheck(string! descriptiveName, VCExpr! vc, ProverInterface.ErrorHandler! handler)
+ requires !IsBusy;
+ {
+ assert !busy;
+ busy = true;
+ hasOutput = false;
+ outputExn = null;
+ this.handler = handler;
+
+ proverStart = DateTime.Now;
+ thmProver.BeginCheck(descriptiveName, vc, handler);
+ // gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
+
+ ThreadPool.QueueUserWorkItem(WaitForOutput);
+ }
+
+ public ProverInterface.Outcome ReadOutcome()
+ throws UnexpectedProverOutputException;
+ requires IsBusy;
+ requires HasOutput;
+ {
+ hasOutput = false;
+ busy = false;
+
+ if (outputExn != null) {
+ throw outputExn;
+ }
+
+ return outcome;
+ }
+ }
+
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+
+ public class ErrorModel {
+ public Dictionary<string!, int>! identifierToPartition;
+ public List<List<string!>>! partitionToIdentifiers;
+ public List<Object>! partitionToValue;
+ public Dictionary<object, int>! valueToPartition;
+ public Dictionary<string!, List<List<int>>!>! definedFunctions;
+
+ public ErrorModel(Dictionary<string!, int>! identifierToPartition, List<List<string!>>! partitionToIdentifiers, List<Object>! partitionToValue, Dictionary<object, int>! valueToPartition, Dictionary<string!, List<List<int>>!>! definedFunctions) {
+ this.identifierToPartition = identifierToPartition;
+ this.partitionToIdentifiers = partitionToIdentifiers;
+ this.partitionToValue = partitionToValue;
+ this.valueToPartition = valueToPartition;
+ this.definedFunctions = definedFunctions;
+ }
+
+ public virtual void Print(TextWriter! writer) { }
+
+ public int LookupPartitionValue(int partition)
+ {
+ BigNum bignum = (BigNum) (!)partitionToValue[partition];
+ return bignum.ToInt;
+ }
+
+ public int LookupControlFlowFunctionAt(int cfc, int id)
+ {
+ List<List<int>>! tuples = this.definedFunctions["ControlFlow"];
+ foreach (List<int> tuple in tuples)
+ {
+ if (tuple == null) continue;
+ if (tuple.Count != 3) continue;
+ if (LookupPartitionValue(tuple[0]) == cfc && LookupPartitionValue(tuple[1]) == id)
+ return LookupPartitionValue(tuple[2]);
+ }
+ assert false;
+ return 0;
+ }
+
+ private string! LookupSkolemConstant(string! name) {
+ foreach (string! functionName in identifierToPartition.Keys)
+ {
+ int index = functionName.LastIndexOf("!");
+ if (index == -1) continue;
+ string! newFunctionName = (!)functionName.Remove(index);
+ if (newFunctionName.Equals(name))
+ return functionName;
+ }
+ return "";
+ }
+ private string! LookupSkolemFunction(string! name) {
+ foreach (string! functionName in definedFunctions.Keys)
+ {
+ int index = functionName.LastIndexOf("!");
+ if (index == -1) continue;
+ string! newFunctionName = (!)functionName.Remove(index);
+ if (newFunctionName.Equals(name))
+ return functionName;
+ }
+ return "";
+ }
+ public int LookupSkolemFunctionAt(string! functionName, List<int>! values)
+ {
+ string! actualFunctionName = LookupSkolemFunction(functionName);
+ if (actualFunctionName.Equals(""))
+ {
+ // The skolem function is actually a skolem constant
+ actualFunctionName = LookupSkolemConstant(functionName);
+ assert !actualFunctionName.Equals("");
+ return identifierToPartition[actualFunctionName];
+ }
+ List<List<int>>! tuples = this.definedFunctions[actualFunctionName];
+ assert tuples.Count > 0;
+ // the last tuple is a dummy tuple
+ for (int n = 0; n < tuples.Count - 1; n++)
+ {
+ List<int>! tuple = (!)tuples[n];
+ assert tuple.Count - 1 <= values.Count;
+ for (int i = 0, j = 0; i < values.Count; i++)
+ {
+ if (values[i] == tuple[j]) {
+ // succeeded in matching tuple[j]
+ j++;
+ if (j == tuple.Count-1) return tuple[tuple.Count - 1];
+ }
+ }
+ }
+ assert false;
+ return 0;
+ }
+
+ public List<object!>! PartitionsToValues(List<int>! args)
+ {
+ List<object!>! vals = new List<object!>();
+ foreach(int i in args)
+ {
+ object! o = (!)partitionToValue[i];
+ if (o is bool) {
+ vals.Add(o);
+ } else if (o is BigNum) {
+ vals.Add(o);
+ } else if (o is List<List<int>!>) {
+ List<List<int>!> array = (List<List<int>!>) o;
+ List<List<object!>!> arrayVal = new List<List<object!>!>();
+ foreach (List<int>! tuple in array) {
+ List<object!> tupleVal = new List<object!>();
+ foreach (int i in tuple) {
+ tupleVal.Add((!)partitionToValue[i]);
+ }
+ arrayVal.Add(tupleVal);
+ }
+ vals.Add(arrayVal);
+ } else {
+ assert false;
+ }
+ }
+ return vals;
+ }
+ }
+
+ public abstract class ProverInterface
+ {
+ public enum Outcome { Valid, Invalid, TimeOut, OutOfMemory, Undetermined }
+
+ public class ErrorHandler
+ {
+ public virtual void OnModel(IList<string!>! labels, ErrorModel errModel)
+ {
+ }
+
+ public virtual void OnResourceExceeded(string! message)
+ {
+ }
+
+ public virtual void OnProverWarning(string! message)
+ modifies Console.Out.*, Console.Error.*;
+ {
+ 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:
+ assume false; // unexpected case
+ }
+ }
+
+
+ public virtual Absy! Label2Absy(string! label)
+ {
+ throw new System.NotImplementedException();
+ }
+ }
+
+ public abstract void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler);
+ [NoDefaultContract]
+ public abstract Outcome CheckOutcome(ErrorHandler! handler);
+ throws UnexpectedProverOutputException;
+
+ public virtual void LogComment(string! comment) {
+ }
+
+ public virtual void Close() {
+ }
+
+ /// <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) {}
+ public virtual string! VCExpressionToString(VCExpr! vc) { return ""; }
+ public virtual void Pop()
+ throws UnexpectedProverOutputException;
+ {}
+ public virtual int NumAxiomsPushed()
+ { return 0; }
+ public virtual int FlushAxiomsToTheoremProver()
+ throws UnexpectedProverOutputException;
+ { return 0; }
+
+
+ public abstract ProverContext! Context { get; }
+ public abstract VCExpressionGenerator! VCExprGen { get; }
+ }
+
+ public class ProverException : Exception
+ {
+ public ProverException(string s) : base(s)
+ {
+ }
+ }
+ public class UnexpectedProverOutputException : ProverException, ICheckedException
+ {
+ 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.")
+ {
+ }
+ }
+}
|