From b9f50d07fabfbbf4ae2684781178598d146e11ef Mon Sep 17 00:00:00 2001
From: Mike Barnett <mbarnett@microsoft.com>
Date: Wed, 28 Dec 2011 18:19:57 -0800
Subject: Add instrumentation for branches.

---
 BCT/BytecodeTranslator/Program.cs            |  5 ++++-
 BCT/BytecodeTranslator/StatementTraverser.cs | 17 +++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)

(limited to 'BCT')

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 9a48f1f0..eaef7e40 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -66,6 +66,9 @@ namespace BytecodeTranslator {
     [OptionDescription("File containing white/black list (optionally end file name with + for white list, - for black list, default is white list", ShortForm = "exempt")]
     public string exemptionFile = "";
 
+    [OptionDescription("Instrument branches with unique counter values", ShortForm = "ib")]
+    public bool instrumentBranches = false;
+
   }
 
   public class BCT {
@@ -248,7 +251,7 @@ namespace BytecodeTranslator {
         }
         var m2 = Decompiler.GetCodeModelFromMetadataModel(host, m, pdbReader) as IModule;
         // The decompiler does not turn calls to Assert/Assume into Code Model nodes
-        m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(m2);
+        m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(m2);
         decompiledModules.Add(m2);
         host.RegisterAsLatest(m2);
         contractExtractors.Add(m2, host.GetContractExtractor(m2.UnitIdentity));
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 424064ff..43441642 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -198,6 +198,17 @@ namespace BytecodeTranslator
       StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
       StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
       ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
+
+      if (this.sink.Options.instrumentBranches) {
+        var tok = conditionalStatement.Token();
+        thenTraverser.StmtBuilder.Add(
+          new Bpl.AssumeCmd(tok, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.NextUniqueNumber()) }, null))
+          );
+        elseTraverser.StmtBuilder.Add(
+          new Bpl.AssumeCmd(tok, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.NextUniqueNumber()) }, null))
+          );
+      }
+
       condTraverser.Traverse(conditionalStatement.Condition);
       thenTraverser.Traverse(conditionalStatement.TrueBranch);
       elseTraverser.Traverse(conditionalStatement.FalseBranch);
@@ -225,6 +236,12 @@ namespace BytecodeTranslator
 
     }
 
+    private static int counter = 0;
+    internal int NextUniqueNumber() {
+      return counter++;
+    }
+
+
     /// <summary>
     /// 
     /// </summary>
-- 
cgit v1.2.3