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
|
//-----------------------------------------------------------------------------
//
// 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;
namespace BytecodeTranslator {
public class Sink {
public TraverserFactory Factory {
get { return this.factory; }
}
readonly TraverserFactory factory;
public Sink(TraverserFactory factory, Heap heap) {
this.factory = factory;
this.heap = heap;
}
public Heap Heap {
get { return this.heap; }
}
readonly Heap heap;
public Bpl.Variable HeapVariable {
get { return this.Heap.HeapVariable; }
}
public Bpl.Variable ArrayContentsVariable
{
get { return this.arrayContentsVariable; }
}
readonly Bpl.Variable arrayContentsVariable = TranslationHelper.TempArrayContentsVar();
public Bpl.Variable ArrayLengthVariable
{
get { return this.arrayLengthVariable; }
}
readonly Bpl.Variable arrayLengthVariable = TranslationHelper.TempArrayLengthVar();
public Bpl.Variable ThisVariable = TranslationHelper.TempThisVar();
public Bpl.Variable RetVariable;
public readonly string AllocationMethodName = "Alloc";
public readonly string StaticFieldFunction = "ClassRepr";
public readonly string ReferenceTypeName = "Ref";
public readonly Bpl.Program TranslatedProgram = new Bpl.Program();
/// <summary>
/// Creates a fresh local var of the given Type and adds it to the
/// Bpl Implementation
/// </summary>
/// <param name="typeReference"> The type of the new variable </param>
/// <returns> A fresh Variable with automatic generated name and location </returns>
public Bpl.Variable CreateFreshLocal(ITypeReference typeReference) {
Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location
Bpl.Type t = TranslationHelper.CciTypeToBoogie(typeReference);
Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));
ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie
localVarMap.Add(dummy, v);
return v;
}
private Dictionary<ILocalDefinition, Bpl.LocalVariable> localVarMap = null;
public Dictionary<ILocalDefinition, Bpl.LocalVariable> LocalVarMap {
get { return this.localVarMap; }
}
/// <summary>
///
/// </summary>
/// <param name="local"></param>
/// <returns></returns>
public Bpl.Variable FindOrCreateLocalVariable(ILocalDefinition local) {
Bpl.LocalVariable v;
Bpl.IToken tok = local.Token();
Bpl.Type t = TranslationHelper.CciTypeToBoogie(local.Type.ResolvedType);
if (!localVarMap.TryGetValue(local, out v)) {
v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, local.Name.Value, t));
localVarMap.Add(local, v);
}
return v;
}
/// <summary>
///
/// </summary>
/// <param name="param"></param>
/// <remarks>STUB</remarks>
/// <returns></returns>
public Bpl.Variable FindParameterVariable(IParameterDefinition param) {
MethodParameter mp;
this.FormalMap.TryGetValue(param, out mp);
return mp.outParameterCopy;
}
public Dictionary<IParameterDefinition, MethodParameter> FormalMap = null;
public Bpl.Variable FindOrCreateFieldVariable(IFieldReference field) {
// The Heap has to decide how to represent the field (i.e., its type),
// all the Sink cares about is adding a declaration for it.
Bpl.Variable v;
var key = Tuple.Create(field.ContainingType.InternedKey, field.Name);
if (!this.declaredFields.TryGetValue(key, out v)) {
v = this.Heap.CreateFieldVariable(field);
this.declaredFields.Add(key, v);
this.TranslatedProgram.TopLevelDeclarations.Add(v);
}
return v;
}
/// <summary>
/// The keys to the table are tuples of the containing type (its interned key) and the name of the field. That
/// should uniquely identify each field.
/// </summary>
private Dictionary<Tuple<uint, IName>, Bpl.Variable> declaredFields = new Dictionary<Tuple<uint, IName>, Bpl.Variable>();
public void BeginMethod() {
this.localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();
}
}
}
|
