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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Cci;
using Microsoft.Cci.MetadataReader;
using Microsoft.Cci.MutableCodeModel;
using Microsoft.Cci.Contracts;
using Microsoft.Cci.ILToCodeModel;
using Bpl = Microsoft.Boogie;
using System.Text.RegularExpressions;
using System.Diagnostics.Contracts;
namespace BytecodeTranslator {
public class MethodParameter {
/// <summary>
/// All parameters of the method get an associated in parameter
/// in the Boogie procedure except for out parameters.
/// </summary>
public Bpl.Formal/*?*/ inParameterCopy;
/// <summary>
/// A local variable when the underlyingParameter is an in parameter
/// and a formal (out) parameter when the underlyingParameter is
/// a ref or out parameter.
/// </summary>
public Bpl.Variable outParameterCopy;
public IParameterDefinition underlyingParameter;
public MethodParameter(IParameterDefinition parameterDefinition, Bpl.Type ptype) {
this.underlyingParameter = parameterDefinition;
var parameterToken = parameterDefinition.Token();
var typeToken = parameterDefinition.Type.Token();
var parameterName = TranslationHelper.TurnStringIntoValidIdentifier(parameterDefinition.Name.Value);
if (String.IsNullOrWhiteSpace(parameterName)) parameterName = "P" + parameterDefinition.Index.ToString();
this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);
if (parameterDefinition.IsByReference) {
this.outParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$out", ptype), false);
} else {
this.outParameterCopy = new Bpl.LocalVariable(parameterToken, new Bpl.TypedIdent(typeToken, parameterName, ptype));
}
}
public override string ToString() {
return this.underlyingParameter.Name.Value;
}
}
/// <summary>
/// Class containing several static helper functions to convert
/// from Cci to Boogie
/// </summary>
static class TranslationHelper {
public static Bpl.StmtList BuildStmtList(Bpl.Cmd cmd, Bpl.TransferCmd tcmd) {
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
builder.Add(cmd);
builder.Add(tcmd);
return builder.Collect(Bpl.Token.NoToken);
}
public static Bpl.StmtList BuildStmtList(Bpl.TransferCmd tcmd) {
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
builder.Add(tcmd);
return builder.Collect(Bpl.Token.NoToken);
}
public static Bpl.StmtList BuildStmtList(params Bpl.Cmd[] cmds) {
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
foreach (Bpl.Cmd cmd in cmds)
builder.Add(cmd);
return builder.Collect(Bpl.Token.NoToken);
}
public static Bpl.AssignCmd BuildAssignCmd(Bpl.IdentifierExpr lhs, Bpl.Expr rhs)
{
List<Bpl.AssignLhs> lhss = new List<Bpl.AssignLhs>();
lhss.Add(new Bpl.SimpleAssignLhs(lhs.tok, lhs));
List<Bpl.Expr> rhss = new List<Bpl.Expr>();
rhss.Add(rhs);
return new Bpl.AssignCmd(lhs.tok, lhss, rhss);
}
public static Bpl.AssignCmd BuildAssignCmd(List<Bpl.IdentifierExpr> lexprs, List<Bpl.Expr> rexprs) {
List<Bpl.AssignLhs> lhss = new List<Bpl.AssignLhs>();
foreach (Bpl.IdentifierExpr lexpr in lexprs) {
lhss.Add(new Bpl.SimpleAssignLhs(lexpr.tok, lexpr));
}
List<Bpl.Expr> rhss = new List<Bpl.Expr>();
return new Bpl.AssignCmd(Bpl.Token.NoToken, lhss, rexprs);
}
public static Bpl.IToken Token(this IObjectWithLocations objectWithLocations) {
//TODO: use objectWithLocations.Locations!
Bpl.IToken tok = Bpl.Token.NoToken;
return tok;
}
internal static int tmpVarCounter = 0;
public static string GenerateTempVarName() {
return "$tmp" + (tmpVarCounter++).ToString();
}
internal static int catchClauseCounter = 0;
public static string GenerateCatchClauseName() {
return "catch" + (catchClauseCounter++).ToString();
}
internal static int finallyClauseCounter = 0;
public static string GenerateFinallyClauseName() {
return "finally" + (finallyClauseCounter++).ToString();
}
public static List<IGenericTypeParameter> ConsolidatedGenericParameters(ITypeReference typeReference) {
Contract.Requires(typeReference != null);
var typeDefinition = typeReference.ResolvedType;
var totalParameters = new List<IGenericTypeParameter>();
ConsolidatedGenericParameters(typeDefinition, totalParameters);
return totalParameters;
//var nestedTypeDefinition = typeDefinition as INestedTypeDefinition;
//while (nestedTypeDefinition != null) {
// var containingType = nestedTypeDefinition.ContainingType.ResolvedType;
// totalParameters.AddRange(containingType.GenericParameters);
// nestedTypeDefinition = containingType as INestedTypeDefinition;
//}
//totalParameters.AddRange(typeDefinition.GenericParameters);
//return totalParameters;
}
private static void ConsolidatedGenericParameters(ITypeDefinition typeDefinition, List<IGenericTypeParameter> consolidatedParameters){
var nestedTypeDefinition = typeDefinition as INestedTypeDefinition;
if (nestedTypeDefinition != null){
ConsolidatedGenericParameters(nestedTypeDefinition.ContainingTypeDefinition, consolidatedParameters);
}
consolidatedParameters.AddRange(typeDefinition.GenericParameters);
}
public static string CreateUniqueMethodName(IMethodReference method) {
var containingTypeName = TypeHelper.GetTypeName(method.ContainingType, NameFormattingOptions.None);
var s = MemberHelper.GetMethodSignature(method, NameFormattingOptions.DocumentationId);
s = s.Substring(2);
s = s.TrimEnd(')');
s = TurnStringIntoValidIdentifier(s);
return s;
}
public static string TurnStringIntoValidIdentifier(string s) {
// Do this specially just to make the resulting string a little bit more readable.
// REVIEW: Just let the main replacement take care of it?
s = s.Replace("[0:,0:]", "2DArray"); // TODO: Do this programmatically to handle arbitrary arity
s = s.Replace("[0:,0:,0:]", "3DArray");
s = s.Replace("[0:,0:,0:,0:]", "4DArray");
s = s.Replace("[0:,0:,0:,0:,0:]", "5DArray");
s = s.Replace("[]", "array");
// The definition of a Boogie identifier is from BoogiePL.atg.
// Just negate that to get which characters should be replaced with a dollar sign.
// letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
// digit = "0123456789".
// special = "'~#$^_.?`".
// nondigit = letter + special.
// ident = [ '\\' ] nondigit {nondigit | digit}.
s = Regex.Replace(s, "[^A-Za-z0-9'~#$^_.?`]", "$");
s = GetRidOfSurrogateCharacters(s);
return s;
}
/// <summary>
/// Unicode surrogates cannot be handled by Boogie.
/// http://msdn.microsoft.com/en-us/library/dd374069(v=VS.85).aspx
/// </summary>
private static string GetRidOfSurrogateCharacters(string s) {
// TODO this is not enough! Actually Boogie cannot support UTF8
var cs = s.ToCharArray();
var okayChars = new char[cs.Length];
for (int i = 0, j = 0; i < cs.Length; i++) {
if (Char.IsSurrogate(cs[i])) continue;
okayChars[j++] = cs[i];
}
var raw = String.Concat(okayChars);
return raw.Trim(new char[] { '\0' });
}
public static bool IsStruct(ITypeReference typ) {
return typ.IsValueType && !typ.IsEnum && typ.TypeCode == PrimitiveTypeCode.NotPrimitive;
}
}
}
|
