diff options
Diffstat (limited to 'Source/VCGeneration/Check.cs')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 333 |
1 files changed, 174 insertions, 159 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index d5505dd4..d30c93e9 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -14,26 +14,23 @@ using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie.VCExprAST;
using Microsoft.Basetypes;
-namespace Microsoft.Boogie
-{
+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
- {
+ public sealed class Checker {
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(gen!=null);
+ void ObjectInvariant() {
+ Contract.Invariant(gen != null);
Contract.Invariant(thmProver != null);
Contract.Invariant(ProverDone != null);
-}
+ }
private readonly VCExpressionGenerator gen;
-
+
private ProverInterface thmProver;
private CommandLineOptions.BvHandling bitvectors;
private int timeout;
@@ -50,34 +47,37 @@ void ObjectInvariant() public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);
- private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl)
- {
- if (impl == null) return CommandLineOptions.Clo.Bitvectors;
+ private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) {
+ if (impl == null)
+ return CommandLineOptions.Clo.Bitvectors;
bool force_int = false;
bool force_native = false;
cce.NonNull(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;
+ 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)
- {
+ public bool WillingToHandle(Implementation impl, int timeout) {
return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl);
}
- public VCExpressionGenerator VCExprGen
- {
- get {Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);
- return this.gen; }
+ 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; }
+ public ProverInterface TheoremProver {
+ get {
+ Contract.Ensures(Contract.Result<ProverInterface>() != null);
+ return this.thmProver;
+ }
}
/////////////////////////////////////////////////////////////////////////////////
@@ -85,10 +85,9 @@ void ObjectInvariant() private struct ContextCacheKey {
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(program!=null);
-}
+ void ObjectInvariant() {
+ Contract.Invariant(program != null);
+ }
public readonly Program program;
public readonly CommandLineOptions.BvHandling bitvectors;
@@ -100,7 +99,8 @@ void ObjectInvariant() this.bitvectors = bitvectors;
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (that is ContextCacheKey) {
ContextCacheKey thatKey = (ContextCacheKey)that;
@@ -121,8 +121,7 @@ void ObjectInvariant() /// <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)
- {
+ public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) {
Contract.Requires(vcgen != null);
Contract.Requires(prog != null);
this.bitvectors = BvHandlingForImpl(impl);
@@ -143,14 +142,14 @@ void ObjectInvariant() }
options.BitVectors = this.bitvectors;
- ContextCacheKey key = new ContextCacheKey (prog, this.bitvectors);
+ ContextCacheKey key = new ContextCacheKey(prog, this.bitvectors);
ProverContext ctx;
ProverInterface prover;
if (vcgen.CheckerCommonState == null) {
- vcgen.CheckerCommonState = new Dictionary<ContextCacheKey, ProverContext> ();
+ vcgen.CheckerCommonState = new Dictionary<ContextCacheKey, ProverContext>();
}
- IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>) vcgen.CheckerCommonState;
+ IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>)vcgen.CheckerCommonState;
if (cachedContexts.TryGetValue(key, out ctx)) {
ctx = (ProverContext)cce.NonNull(ctx).Clone();
@@ -203,7 +202,7 @@ void ObjectInvariant() CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
cachedContexts.Add(key, cce.NonNull((ProverContext)ctx.Clone()));
}
-
+
this.thmProver = prover;
this.gen = prover.VCExprGen;
@@ -214,8 +213,7 @@ void ObjectInvariant() /// <summary>
/// Clean-up.
/// </summary>
- public void Close()
- {
+ public void Close() {
this.closed = true;
thmProver.Close();
}
@@ -224,35 +222,37 @@ void ObjectInvariant() /// Push a Verification Condition as an Axiom
/// (Required for Doomed Program Point detection)
/// </summary>
- public void PushVCExpr(VCExpr vc)
- {
+ public void PushVCExpr(VCExpr vc) {
Contract.Requires(vc != null);
//thmProver.Context.AddAxiom(vc);
thmProver.PushVCExpression(vc);
}
- public bool IsBusy
- {
- get { return busy; }
+ public bool IsBusy {
+ get {
+ return busy;
+ }
}
- public bool Closed
- {
- get { return closed; }
+ public bool Closed {
+ get {
+ return closed;
+ }
}
- public bool HasOutput
- {
- get { return hasOutput; }
+ public bool HasOutput {
+ get {
+ return hasOutput;
+ }
}
- public TimeSpan ProverRunTime
- {
- get { return proverRunTime; }
+ public TimeSpan ProverRunTime {
+ get {
+ return proverRunTime;
+ }
}
- private void WaitForOutput(object dummy)
- {
+ private void WaitForOutput(object dummy) {
try {
outcome = thmProver.CheckOutcome(cce.NonNull(handler));
} catch (UnexpectedProverOutputException e) {
@@ -277,20 +277,20 @@ void ObjectInvariant() break;
}
- Contract.Assert( busy);
+ Contract.Assert(busy);
hasOutput = true;
proverRunTime = DateTime.Now - proverStart;
ProverDone.Set();
}
-
- public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler){
+
+ public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
Contract.Requires(descriptiveName != null);
Contract.Requires(vc != null);
Contract.Requires(handler != null);
-
- Contract.Requires( !IsBusy);
- Contract.Assert( !busy);
+
+ Contract.Requires(!IsBusy);
+ Contract.Assert(!busy);
busy = true;
hasOutput = false;
outputExn = null;
@@ -303,11 +303,11 @@ void ObjectInvariant() ThreadPool.QueueUserWorkItem(WaitForOutput);
}
- public ProverInterface.Outcome ReadOutcome(){
-
- Contract.Requires( IsBusy);
- Contract.Requires( HasOutput);
- Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);
+ public ProverInterface.Outcome ReadOutcome() {
+
+ Contract.Requires(IsBusy);
+ Contract.Requires(HasOutput);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
hasOutput = false;
busy = false;
@@ -318,7 +318,7 @@ void ObjectInvariant() return outcome;
}
}
-
+
// -----------------------------------------------------------------------------------------------
// -----------------------------------------------------------------------------------------------
// -----------------------------------------------------------------------------------------------
@@ -331,21 +331,20 @@ void ObjectInvariant() public Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(cce.NonNullElements(identifierToPartition));
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(identifierToPartition));
Contract.Invariant(partitionToIdentifiers != null);
- Contract.Invariant(Contract.ForAll(partitionToIdentifiers,i=>cce.NonNullElements(i)));
+ Contract.Invariant(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i)));
Contract.Invariant(partitionToValue != null);
Contract.Invariant(valueToPartition != null);
Contract.Invariant(cce.NonNullElements(definedFunctions));
-}
+ }
public ErrorModel(Dictionary<string, int> identifierToPartition, List<List<string>> partitionToIdentifiers, List<Object> partitionToValue, Dictionary<object, int> valueToPartition, Dictionary<string, List<List<int>>> definedFunctions) {
Contract.Requires(cce.NonNullElements(identifierToPartition));
Contract.Requires(partitionToIdentifiers != null);
- Contract.Requires(Contract.ForAll(partitionToIdentifiers,i=>cce.NonNullElements(i)));
+ Contract.Requires(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i)));
Contract.Requires(partitionToValue != null);
Contract.Requires(valueToPartition != null);
Contract.Requires(cce.NonNullElements(definedFunctions));
@@ -356,39 +355,41 @@ void ObjectInvariant() this.definedFunctions = definedFunctions;
}
- public virtual void Print(TextWriter writer) {Contract.Requires(writer != null); }
-
- public int LookupPartitionValue(int partition)
- {
- BigNum bignum = (BigNum) cce.NonNull(partitionToValue)[partition];
+ public virtual void Print(TextWriter writer) {
+ Contract.Requires(writer != null);
+ }
+
+ public int LookupPartitionValue(int partition) {
+ BigNum bignum = (BigNum)cce.NonNull(partitionToValue)[partition];
return bignum.ToInt;
}
-
- public int LookupControlFlowFunctionAt(int cfc, int id)
- {
+
+ public int LookupControlFlowFunctionAt(int cfc, int id) {
List<List<int>> tuples = this.definedFunctions["ControlFlow"];
Contract.Assert(tuples != null);
- foreach (List<int> tuple in tuples)
- {
- if (tuple == null) continue;
- if (tuple.Count != 3) continue;
+ 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]);
}
- Contract.Assert(false);throw new cce.UnreachableException();
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
return 0;
}
-
+
private string LookupSkolemConstant(string name) {
Contract.Requires(name != null);
Contract.Ensures(Contract.Result<string>() != null);
- foreach (string functionName in identifierToPartition.Keys)
- {
+ foreach (string functionName in identifierToPartition.Keys) {
Contract.Assert(functionName != null);
int index = functionName.LastIndexOf("!");
- if (index == -1) continue;
+ if (index == -1)
+ continue;
string newFunctionName = cce.NonNull(functionName.Remove(index));
if (newFunctionName.Equals(name))
return functionName;
@@ -399,67 +400,62 @@ void ObjectInvariant() Contract.Requires(name != null);
Contract.Ensures(Contract.Result<string>() != null);
- foreach (string functionName in definedFunctions.Keys)
- {
+ foreach (string functionName in definedFunctions.Keys) {
Contract.Assert(functionName != null);
int index = functionName.LastIndexOf("!");
- if (index == -1) continue;
+ if (index == -1)
+ continue;
string newFunctionName = cce.NonNull(functionName.Remove(index));
if (newFunctionName.Equals(name))
return functionName;
}
return "";
}
- public int LookupSkolemFunctionAt(string functionName, List<int> values)
-
- {
- Contract.Requires(functionName!= null);
+ public int LookupSkolemFunctionAt(string functionName, List<int> values) {
+ Contract.Requires(functionName != null);
Contract.Requires(values != null);
string actualFunctionName = LookupSkolemFunction(functionName);
Contract.Assert(actualFunctionName != null);
- if (actualFunctionName.Equals(""))
- {
+ if (actualFunctionName.Equals("")) {
// The skolem function is actually a skolem constant
actualFunctionName = LookupSkolemConstant(functionName);
- Contract.Assert( !actualFunctionName.Equals(""));
+ Contract.Assert(!actualFunctionName.Equals(""));
return identifierToPartition[actualFunctionName];
}
List<List<int>> tuples = this.definedFunctions[actualFunctionName];
- Contract.Assert( tuples.Count > 0);
+ Contract.Assert(tuples.Count > 0);
// the last tuple is a dummy tuple
- for (int n = 0; n < tuples.Count - 1; n++)
- {
+ for (int n = 0; n < tuples.Count - 1; n++) {
List<int> tuple = cce.NonNull(tuples[n]);
- Contract.Assert( tuple.Count - 1 <= values.Count);
- for (int i = 0, j = 0; i < values.Count; i++)
- {
+ Contract.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];
+ if (j == tuple.Count - 1)
+ return tuple[tuple.Count - 1];
}
}
}
- Contract.Assert(false);throw new cce.UnreachableException();
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
return 0;
}
-
- public List<object>/*!>!*/ PartitionsToValues(List<int> args)
- {
+
+ public List<object>/*!>!*/ PartitionsToValues(List<int> args) {
Contract.Requires(args != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<object>>()));
List<object> vals = new List<object>();
- foreach(int i in args)
- {
+ foreach (int i in args) {
object o = cce.NonNull(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<int>> array = (List<List<int>>)o;
List<List<object>> arrayVal = new List<List<object>>();
foreach (List<int> tuple in array) {
Contract.Assert(tuple != null);
@@ -472,30 +468,33 @@ void ObjectInvariant() }
vals.Add(arrayVal);
} else {
- Contract.Assert(false);throw new cce.UnreachableException();
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
}
}
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 abstract class ProverInterface {
+ public enum Outcome {
+ Valid,
+ Invalid,
+ TimeOut,
+ OutOfMemory,
+ Undetermined
+ }
+ public class ErrorHandler {
+ public virtual void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel) {
Contract.Requires(cce.NonNullElements(labels));
}
- public virtual void OnResourceExceeded(string message)
- {
- Contract.Requires(message!=null);
+ public virtual void OnResourceExceeded(string message) {
+ Contract.Requires(message != null);
}
public virtual void OnProverWarning(string message)
- //modifies Console.Out.*, Console.Error.*;
+ //modifies Console.Out.*, Console.Error.*;
{
Contract.Requires(message != null);
switch (CommandLineOptions.Clo.PrintProverWarnings) {
@@ -508,13 +507,13 @@ void ObjectInvariant() Console.Error.WriteLine("Prover warning: " + message);
break;
default:
- Contract.Assume( false);throw new cce.UnreachableException(); // unexpected case
+ Contract.Assume(false);
+ throw new cce.UnreachableException(); // unexpected case
}
}
- public virtual Absy Label2Absy(string label)
- {
+ public virtual Absy Label2Absy(string label) {
Contract.Requires(label != null);
Contract.Ensures(Contract.Result<Absy>() != null);
@@ -529,26 +528,40 @@ void ObjectInvariant() }
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) {Contract.Requires(vc != null);}
- public virtual string VCExpressionToString(VCExpr vc) {Contract.Requires(vc != null);Contract.Ensures(Contract.Result<string>() != null); return ""; }
- public virtual void Pop()
- {Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);}
- public virtual int NumAxiomsPushed()
- { return 0; }
- public virtual int FlushAxiomsToTheoremProver()
- { Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);return 0; }
-
-
- public abstract ProverContext Context { get; }
-public abstract VCExpressionGenerator VCExprGen { get; }
+ public virtual void PushVCExpression(VCExpr vc) {
+ Contract.Requires(vc != null);
+ }
+ public virtual string VCExpressionToString(VCExpr vc) {
+ Contract.Requires(vc != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ return "";
+ }
+ public virtual void Pop() {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ }
+ public virtual int NumAxiomsPushed() {
+ return 0;
+ }
+ public virtual int FlushAxiomsToTheoremProver() {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ return 0;
+ }
+
+
+ public abstract ProverContext Context {
+ get;
+ }
+ public abstract VCExpressionGenerator VCExprGen {
+ get;
+ }
}
- public class ProverInterfaceContracts:ProverInterface{
+ public class ProverInterfaceContracts : ProverInterface {
public override ProverContext Context {
get {
Contract.Ensures(Contract.Result<ProverContext>() != null);
@@ -563,32 +576,34 @@ public abstract VCExpressionGenerator VCExprGen { get; } 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();}
+ 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){
- //Contract.Requires(handler != null);
- Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);
- throw new NotImplementedException();}
+ public override Outcome CheckOutcome(ErrorHandler handler) {
+ //Contract.Requires(handler != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ throw new NotImplementedException();
+ }
}
-
- public class ProverException : Exception
- {
- public ProverException(string s) : base(s)
- {
+
+ public class ProverException : Exception {
+ public ProverException(string s)
+ : base(s) {
}
}
- public class UnexpectedProverOutputException : ProverException, Microsoft.Contracts.ICheckedException
- {
- public UnexpectedProverOutputException(string s) : base(s)
- {
+ public class UnexpectedProverOutputException : ProverException, Microsoft.Contracts.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.")
- {
+ public class ProverDiedException : UnexpectedProverOutputException {
+ public ProverDiedException()
+ : base("Prover died with no further output, perhaps it ran out of memory or was killed.") {
}
}
}
|