diff options
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 9 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 2 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 32 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TraverserFactory.cs | 13 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/RegressionTestInput.txt | 30 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/UnitTest0.cs | 2 |
6 files changed, 77 insertions, 11 deletions
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index e84bd836..50ab2e30 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -31,14 +31,17 @@ namespace BytecodeTranslator { public readonly IContractProvider ContractProvider;
+ public readonly ISourceLocationProvider/*?*/ SourceLocationProvider;
+
public Bpl.Variable HeapVariable;
-
- public MetadataTraverser(Sink sink, IContractProvider cp)
+
+ public MetadataTraverser(Sink sink, IContractProvider cp, ISourceLocationProvider/*?*/ sourceLocationProvider)
: base() {
this.sink = sink;
this.factory = sink.Factory;
ContractProvider = cp;
+ this.SourceLocationProvider = sourceLocationProvider;
}
public Bpl.Program TranslatedProgram {
@@ -223,7 +226,7 @@ namespace BytecodeTranslator { throw new NotImplementedException("abstract methods are not yet implemented");
}
- StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink);
+ StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.SourceLocationProvider);
#region Add assignements from In-Params to local-Params
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index c1875b97..d272e879 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -102,7 +102,7 @@ namespace BytecodeTranslator { #region Pass 3: Translate the code model to BPL
//tmp_BPLGenerator translator = new tmp_BPLGenerator(host, acp);
var factory = new CLRSemantics();
- MetadataTraverser translator = factory.MakeMetadataTraverser(host.GetContractExtractor(module.ModuleIdentity));
+ MetadataTraverser translator = factory.MakeMetadataTraverser(host.GetContractExtractor(module.ModuleIdentity), pdbReader);
assembly = module as IAssembly;
if (assembly != null)
translator.Visit(assembly);
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 99431469..0bd2be12 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -26,15 +26,18 @@ namespace BytecodeTranslator readonly Sink sink;
+ public readonly ISourceLocationProvider/*?*/ SourceLocationProvider;
+
private readonly Bpl.Variable HeapVariable;
public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();
#region Constructors
- public StatementTraverser(Sink sink) {
+ public StatementTraverser(Sink sink, ISourceLocationProvider/*?*/ sourceLocationProvider) {
this.sink = sink;
this.factory = sink.Factory;
HeapVariable = sink.HeapVariable;
+ this.SourceLocationProvider = sourceLocationProvider;
}
#endregion
@@ -57,6 +60,29 @@ namespace BytecodeTranslator }
}
+ public override void Visit(IStatement statement) {
+ var tok = statement.Token();
+ string fileName = null;
+ int lineNumber = 0;
+ if (this.SourceLocationProvider != null) {
+ var slocs = this.SourceLocationProvider.GetPrimarySourceLocationsFor(statement.Locations);
+ foreach (var sloc in slocs) {
+ fileName = sloc.Document.Name.Value;
+ lineNumber = sloc.StartLine;
+ break;
+ }
+ if (fileName != null) {
+ var attrib = new Bpl.QKeyValue(tok, "line", new List<object> { Bpl.Expr.Literal((int)lineNumber) }, null);
+ attrib = new Bpl.QKeyValue(tok, "filename", new List<object> { fileName }, attrib);
+ StmtBuilder.Add(
+ new Bpl.AssumeCmd(tok, Bpl.Expr.True, attrib)
+ );
+ }
+ }
+
+ base.Visit(statement);
+ }
+
#region Basic Statements
public override void Visit(IAssertStatement assertStatement) {
@@ -77,8 +103,8 @@ namespace BytecodeTranslator /// <remarks>(mschaef) Works, but still a stub</remarks>
/// <param name="conditionalStatement"></param>
public override void Visit(IConditionalStatement conditionalStatement) {
- StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink);
- StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink);
+ StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.SourceLocationProvider);
+ StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.SourceLocationProvider);
ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, null);
condTraverser.Visit(conditionalStatement.Condition);
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs index 4a48cf5f..953e5030 100644 --- a/BCT/BytecodeTranslator/TraverserFactory.cs +++ b/BCT/BytecodeTranslator/TraverserFactory.cs @@ -18,8 +18,15 @@ using Bpl = Microsoft.Boogie; namespace BytecodeTranslator {
public abstract class TraverserFactory {
- public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider) { return new MetadataTraverser(new Sink(this), contractProvider); }
- public virtual StatementTraverser MakeStatementTraverser(Sink sink) { return new StatementTraverser(sink); }
- public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser) { return new ExpressionTraverser(sink, statementTraverser); }
+ public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider, ISourceLocationProvider/*?*/ sourceLocationProvider)
+ {
+ return new MetadataTraverser(new Sink(this), contractProvider, sourceLocationProvider);
+ }
+ public virtual StatementTraverser MakeStatementTraverser(Sink sink, ISourceLocationProvider/*?*/ sourceLocationProvider) {
+ return new StatementTraverser(sink, sourceLocationProvider);
+ }
+ public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser) {
+ return new ExpressionTraverser(sink, statementTraverser);
+ }
}
}
\ No newline at end of file diff --git a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt index 1771644a..a0a2714c 100644 --- a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt +++ b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt @@ -41,7 +41,9 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int x := x$in;
y := y$in;
+ assume {:filename "Class1.cs"} {:line 64} true;
local_0 := x < y;
+ assume {:filename "Class1.cs"} {:line 65} true;
$result := local_0;
return;
}
@@ -57,9 +59,13 @@ implementation RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: in var z: bool;
z := z$in;
+ assume {:filename "Class1.cs"} {:line 67} true;
+ assume {:filename "Class1.cs"} {:line 68} true;
$Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := z;
+ assume {:filename "Class1.cs"} {:line 16707566} true;
if (z)
{
+ assume {:filename "Class1.cs"} {:line 69} true;
RegressionTestInput.ClassWithBoolTypes.staticB := z;
}
else
@@ -79,7 +85,9 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main$System.Void() {
var $tmp0: bool;
+ assume {:filename "Class1.cs"} {:line 73} true;
call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(3, 4);
+ assume {:filename "Class1.cs"} {:line 74} true;
return;
}
@@ -97,7 +105,9 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r var local_0: int;
x := x$in;
+ assume {:filename "Class1.cs"} {:line 17} true;
local_0 := x + 1;
+ assume {:filename "Class1.cs"} {:line 18} true;
$result := local_0;
return;
}
@@ -122,12 +132,15 @@ implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int) assert $tmp1 != 0;
__temp_1 := 5 / $tmp1;
__temp_2 := 3;
+ assume {:filename "Class1.cs"} {:line 21} true;
__temp_3 := __temp_2;
x := __temp_3;
local_0 := __temp_1 + __temp_2;
assert x == 3 && local_0 <= 8;
+ assume {:filename "Class1.cs"} {:line 23} true;
RegressionTestInput.Class0.StaticInt := local_0;
assert local_0 == RegressionTestInput.Class0.StaticInt;
+ assume {:filename "Class1.cs"} {:line 25} true;
return;
}
@@ -142,8 +155,10 @@ implementation RegressionTestInput.Class0.NonVoid$System.Int32(this: int) return var local_0: int;
var $tmp2: int;
+ assume {:filename "Class1.cs"} {:line 28} true;
call $tmp2 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
local_0 := 3 + RegressionTestInput.Class0.StaticInt + $tmp2;
+ assume {:filename "Class1.cs"} {:line 29} true;
$result := local_0;
return;
}
@@ -158,8 +173,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32(this: int) retur {
var local_0: int;
+ assume {:filename "Class1.cs"} {:line 32} true;
x$out := 3 + RegressionTestInput.Class0.StaticInt;
+ assume {:filename "Class1.cs"} {:line 33} true;
local_0 := x$out;
+ assume {:filename "Class1.cs"} {:line 34} true;
$result := local_0;
return;
}
@@ -175,9 +193,13 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: var local_0: int;
x$out := x$in;
+ assume {:filename "Class1.cs"} {:line 37} true;
x$out := x$out + 1;
+ assume {:filename "Class1.cs"} {:line 38} true;
RegressionTestInput.Class0.StaticInt := x$out;
+ assume {:filename "Class1.cs"} {:line 39} true;
local_0 := x$out;
+ assume {:filename "Class1.cs"} {:line 40} true;
$result := local_0;
return;
}
@@ -194,9 +216,13 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int var local_0: int;
x := x$in;
+ assume {:filename "Class1.cs"} {:line 43} true;
x := x + 1;
+ assume {:filename "Class1.cs"} {:line 44} true;
RegressionTestInput.Class0.StaticInt := x;
+ assume {:filename "Class1.cs"} {:line 45} true;
local_0 := x;
+ assume {:filename "Class1.cs"} {:line 46} true;
$result := local_0;
return;
}
@@ -213,7 +239,9 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho var local_0: int;
x := x$in;
+ assume {:filename "Class1.cs"} {:line 50} true;
local_0 := x;
+ assume {:filename "Class1.cs"} {:line 51} true;
$result := local_0;
return;
}
@@ -231,8 +259,10 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int var $tmp3: int;
y := y$in;
+ assume {:filename "Class1.cs"} {:line 54} true;
call {:async} $tmp3 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
local_0 := $tmp3;
+ assume {:filename "Class1.cs"} {:line 55} true;
$result := local_0;
return;
}
diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs index 5079cc64..c45829a5 100644 --- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs +++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs @@ -84,7 +84,7 @@ namespace TranslationTest { #region Pass 3: Translate the code model to BPL
var factory = new CLRSemantics();
- MetadataTraverser translator = factory.MakeMetadataTraverser(host.GetContractExtractor(module.ModuleIdentity));
+ MetadataTraverser translator = factory.MakeMetadataTraverser(host.GetContractExtractor(module.ModuleIdentity), pdbReader);
assembly = module as IAssembly;
if (assembly != null)
translator.Visit(assembly);
|