1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
//-----------------------------------------------------------------------------
//
// Copyright (c) Microsoft. All rights reserved.
// This code is licensed under the Microsoft Public License.
// THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF
// ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY
// IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR
// PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.IO;
using System.Runtime.Serialization; // needed for defining exception .ctors
using Microsoft.Cci;
using Microsoft.Cci.MutableCodeModel;
using Bpl = Microsoft.Boogie;
using System.Diagnostics;
namespace AssertionInjector {
class Program {
const int errorValue = -1;
static int Main(string[] args) {
if (args == null || args.Length < 4) {
Console.WriteLine("Usage: AssertionInjector <assembly> <filename+extension> <line number> <column number> [<outputPath>]");
return errorValue;
}
int lineNumber;
if (!Int32.TryParse(args[2], out lineNumber)) {
Console.WriteLine("Error: couldn't parse '{0}' as an integer to use as a line number", args[2]);
return errorValue;
}
int columnNumber;
if (!Int32.TryParse(args[3], out columnNumber)) {
Console.WriteLine("Error: couldn't parse '{0}' as an integer to use as a column number", args[3]);
return errorValue;
}
return InjectAssertionInBpl(args[0], args[1], lineNumber, columnNumber);
}
static int InjectAssertionInBpl(string bplFileName, string fileName, int lineNumber, int columnNumber) {
Bpl.CommandLineOptions.Install(new Bpl.CommandLineOptions());
Bpl.CommandLineOptions.Clo.DoModSetAnalysis = true;
var returnValue = errorValue;
Bpl.Program program;
Bpl.Parser.Parse(bplFileName, new List<string>(), out program);
int errorCount = program.Resolve();
if (errorCount != 0) {
Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, bplFileName);
return returnValue;
}
errorCount = program.Typecheck();
if (errorCount != 0) {
Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName);
return returnValue;
}
GetMeHereBplInjector bplInjector = new GetMeHereBplInjector(fileName, lineNumber, columnNumber);
bplInjector.Visit(program);
using (Bpl.TokenTextWriter writer = new Bpl.TokenTextWriter(bplFileName)) {
Bpl.CommandLineOptions.Clo.PrintInstrumented = true;
program.Emit(writer);
}
return returnValue;
}
}
public class GetMeHereBplInjector : Bpl.StandardVisitor {
string fileName;
int lineNumber;
int columnNumber;
public GetMeHereBplInjector(string fileName, int lineNumber, int columnNumber) {
this.fileName = fileName;
this.lineNumber = lineNumber;
this.columnNumber = columnNumber;
}
public override Bpl.CmdSeq VisitCmdSeq(Bpl.CmdSeq cmdSeq) {
Bpl.CmdSeq newCmdSeq = new Bpl.CmdSeq();
for (int i = 0; i < cmdSeq.Length; i++) {
Bpl.Cmd cmd = cmdSeq[i];
if (IsRelevant(cmd))
newCmdSeq.Add(new Bpl.AssertCmd(cmd.tok, Bpl.Expr.False));
newCmdSeq.Add(cmd);
}
return newCmdSeq;
}
private bool IsRelevant(Bpl.Cmd cmd) {
Bpl.AssertCmd assertCmd = cmd as Bpl.AssertCmd;
if (assertCmd == null)
return false;
string sourceFile = Bpl.QKeyValue.FindStringAttribute(assertCmd.Attributes, "sourceFile");
if (sourceFile == null)
return false;
string[] ds = sourceFile.Split('\\');
if (sourceFile != fileName && ds[ds.Length - 1] != fileName)
return false;
int sourceLine = Bpl.QKeyValue.FindIntAttribute(assertCmd.Attributes, "sourceLine", -1);
Debug.Assert(sourceLine != -1);
if (sourceLine != lineNumber)
return false;
return true;
}
}
}
|
