From b9f50d07fabfbbf4ae2684781178598d146e11ef Mon Sep 17 00:00:00 2001 From: Mike Barnett 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(-) 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 { 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 { 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++; + } + + /// /// /// -- cgit v1.2.3