Boogie\VCGeneration: Renaming sources in preparation for my addition of the ported C# version

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.")

+    {

+    }

+  }

+}