diff options
Diffstat (limited to 'BCT')
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 19 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 6 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 11 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/UnitTest0.cs | 2 |
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;
|