Generate "assume {:filename "foo.cs"}{:line 3} true" statements for each statement that has a source location.

4 files changed, 46 insertions, 10 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