Added new option /captureState (/c) for generating a capture state assumption

after each statement.

4 files changed, 28 insertions, 10 deletions

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 18d735af..2a863aa8 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -31,6 +31,9 @@ namespace BytecodeTranslator {
     [OptionDescription("Break into debugger", ShortForm = "break")]

     public bool breakIntoDebugger = false;

 

+    [OptionDescription("Emit a 'capture state' directive after each statement, (default: false)", ShortForm = "c")]

+    public bool captureState = false;

+

     [OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]

     public List<string> libpaths = new List<string>();

 

@@ -165,16 +168,16 @@ namespace BytecodeTranslator {
       return result;

     }

 

-    public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options/*?*/ options, List<Regex> exemptionList, bool whiteList) {

+    public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {

       Contract.Requires(assemblyNames != null);

       Contract.Requires(heapFactory != null);

 

-      var libPaths = options == null ? null : options.libpaths;

-      var wholeProgram = options == null ? false : options.wholeProgram;

-      var/*?*/ stubAssemblies = options == null ? null : options.stub;

-      var phoneControlsConfigFile = options == null ? null : options.phoneControls;

-      var doPhoneNav = options == null ? false : options.phoneNavigationCode;

-      var doPhoneFeedback = options == null ? false : options.phoneFeedbackCode;

+      var libPaths = options.libpaths;

+      var wholeProgram = options.wholeProgram;

+      var/*?*/ stubAssemblies = options.stub;

+      var phoneControlsConfigFile = options.phoneControls;

+      var doPhoneNav = options.phoneNavigationCode;

+      var doPhoneFeedback = options.phoneFeedbackCode;

 

       var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);

       Host = host;

@@ -247,7 +250,7 @@ namespace BytecodeTranslator {
       else

         traverserFactory = new CLRSemantics();

 

-      Sink sink= new Sink(host, traverserFactory, heapFactory, exemptionList, whiteList);

+      Sink sink= new Sink(host, traverserFactory, heapFactory, options, exemptionList, whiteList);

       TranslationHelper.tmpVarCounter = 0;

       MetadataTraverser translator;

       translator= traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index b2c1177e..1427b836 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -27,10 +27,11 @@ namespace BytecodeTranslator {
       get { return this.factory; }

     }

     readonly TraverserFactory factory;

+    private readonly Options options;

     readonly bool whiteList;

     readonly List<Regex> exemptionList;

 

-    public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, List<Regex> exemptionList, bool whiteList) {

+    public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {

       Contract.Requires(host != null);

       Contract.Requires(factory != null);

       Contract.Requires(heapFactory != null);

@@ -38,6 +39,7 @@ namespace BytecodeTranslator {
       this.host = host;

       this.factory = factory;

       var b = heapFactory.MakeHeap(this, out this.heap, out this.TranslatedProgram); // TODO: what if it returns false?

+      this.options = options;

       this.exemptionList = exemptionList;

       this.whiteList = whiteList;

       if (this.TranslatedProgram == null) {

@@ -52,6 +54,8 @@ namespace BytecodeTranslator {
       }

     }

 

+    public Options Options { get { return this.options; } }

+

     public Heap Heap {

       get { return this.heap; }

     }

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 4c927b3e..015e57ce 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -54,6 +54,8 @@ namespace BytecodeTranslator
     public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();

     private bool contractContext;

     internal readonly Stack<IExpression> operandStack = new Stack<IExpression>();

+    private bool captureState;

+    private static int captureStateCounter = 0;

 

     #region Constructors

     public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {

@@ -61,6 +63,7 @@ namespace BytecodeTranslator
       this.factory = sink.Factory;

       PdbReader = pdbReader;

       this.contractContext = contractContext;

+      this.captureState = sink.Options.captureState;

     }

     #endregion

 

@@ -108,6 +111,14 @@ namespace BytecodeTranslator
 

     public override void Visit(IStatement statement) {

       EmitSourceContext(statement);

+      if (this.sink.Options.captureState) {

+        var tok = statement.Token();

+        var state = String.Format("s{0}", StatementTraverser.captureStateCounter++);

+        var attrib = new Bpl.QKeyValue(tok, "captureState ", new List<object> { state }, null);

+        StmtBuilder.Add(

+          new Bpl.AssumeCmd(tok, Bpl.Expr.True, attrib)

+          );

+      }

       base.Visit(statement);

     }

 

diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index e3da57b5..a8b5fdb2 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -61,7 +61,7 @@ namespace TranslationTest {
     #endregion

 

     private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {

-      BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, null, null, false);

+      BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, new Options(), null, false);

       var fileName = Path.ChangeExtension(assemblyName, "bpl");

       var s = File.ReadAllText(fileName);

       return s;