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
|
#include "DeepCloneVisitor.hpp"
|
33
|
#include <list>
|
34
|
#include <ast/identifiers/NamedActionIdentifier.hpp>
|
35
|
#include <ast/statements/SeqBlock.hpp>
|
36
|
#include <ast/expressions/BinaryOperator.hpp>
|
37
|
#include <ast/statements/Assignment.hpp>
|
38
|
#include <ast/identifiers/AttributeIdentifier.hpp>
|
39
|
#include <ast/statements/Call.hpp>
|
40
|
#include <ast/expressions/CallExpression.hpp>
|
41
|
#include <ast/statements/GuardedCommand.hpp>
|
42
|
#include <ast/expressions/IdentifierExpression.hpp>
|
43
|
#include <ast/expressions/ListConstructor.hpp>
|
44
|
#include <ast/expressions/SetConstructor.hpp>
|
45
|
#include <ast/expressions/TernaryOperator.hpp>
|
46
|
#include <ast/expressions/TupleConstructor.hpp>
|
47
|
#include <ast/expressions/TupleMapAccessExpression.hpp>
|
48
|
|
49
|
namespace Ast {
|
50
|
|
51
|
|
52
|
|
53
|
void DeepCloneVisitor::updateScope(IScope* aScope) {
|
54
|
IScope* parentScope = aScope->getParentScope();
|
55
|
if (parentScope != nullptr) {
|
56
|
if(m_mapping.count(parentScope) == 0) {
|
57
|
if (!m_allowLinksToNonClonedParents) {
|
58
|
m_context->logError("Internal Error. Scope update failed.");
|
59
|
abort();
|
60
|
}
|
61
|
return;
|
62
|
}
|
63
|
aScope->setParentScope((IScope*)m_mapping[parentScope]);
|
64
|
}
|
65
|
}
|
66
|
|
67
|
void DeepCloneVisitor::checkScope(IScope* aScope) {
|
68
|
if (aScope->getParentScope() == nullptr)
|
69
|
return;
|
70
|
if (m_mapping.count(aScope->getParentScope()) > 0) {
|
71
|
m_context->logError("Internal Error. Scope check failed.");
|
72
|
abort();
|
73
|
}
|
74
|
}
|
75
|
|
76
|
Expression* DeepCloneVisitor::eClone(Expression* anExpr) {
|
77
|
Expression* result = nullptr;
|
78
|
if (anExpr != nullptr)
|
79
|
{
|
80
|
result = m_cloneAst->createExpression(*anExpr);
|
81
|
if (anExpr->asScope() != nullptr)
|
82
|
{
|
83
|
m_mapping[anExpr] = result;
|
84
|
updateScope(result->asScope());
|
85
|
}
|
86
|
result->accept(*this);
|
87
|
}
|
88
|
return result;
|
89
|
}
|
90
|
|
91
|
Statement* DeepCloneVisitor::sClone(Statement* aStatement) {
|
92
|
Statement* result = nullptr;
|
93
|
if (aStatement != nullptr)
|
94
|
{
|
95
|
result = m_cloneAst->createStatement(*aStatement);
|
96
|
if (aStatement->asScope() != nullptr)
|
97
|
{
|
98
|
m_mapping[aStatement] = result;
|
99
|
updateScope(result->asScope());
|
100
|
}
|
101
|
result->accept(*this);
|
102
|
}
|
103
|
return result;
|
104
|
}
|
105
|
|
106
|
void DeepCloneVisitor::symTabClone(SymbolTable* aTable) {
|
107
|
if (aTable != nullptr && aTable->size() > 0)
|
108
|
{
|
109
|
std::list<Identifier*> newList;
|
110
|
for (auto& x: *aTable)
|
111
|
{
|
112
|
if (m_mapping.count(x.second) == 0) {
|
113
|
Identifier* newid = m_cloneAst->createIdentifier(*x.second);
|
114
|
newList.push_back(newid);
|
115
|
m_mapping[x.second] = newid;
|
116
|
} else {
|
117
|
newList.push_back((Identifier*) m_mapping[x.second]);
|
118
|
}
|
119
|
}
|
120
|
aTable->setSymbolList(newList);
|
121
|
}
|
122
|
}
|
123
|
|
124
|
void DeepCloneVisitor::cloneBlock(Block* aBlock) {
|
125
|
symTabClone(aBlock->symbols());
|
126
|
StatementList& statements = aBlock->statements();
|
127
|
for (std::size_t cntr = 0; cntr < statements.size(); cntr++) {
|
128
|
statements[cntr] = sClone(statements[cntr]);
|
129
|
}
|
130
|
}
|
131
|
|
132
|
void DeepCloneVisitor::cloneQuantifier(Quantifier* qf) {
|
133
|
symTabClone(qf->symbols());
|
134
|
bool oldQunatifierState = m_quantifierState;
|
135
|
m_quantifierState = true;
|
136
|
visit(qf);
|
137
|
m_quantifierState = oldQunatifierState;
|
138
|
}
|
139
|
|
140
|
void DeepCloneVisitor::cloneExpressionList(ExpressionList& aList) {
|
141
|
for (std::size_t cntr =0; cntr < aList.size(); cntr ++)
|
142
|
aList[cntr] = eClone(aList[cntr]);
|
143
|
}
|
144
|
|
145
|
|
146
|
|
147
|
void DeepCloneVisitor::visit(NamedActionIdentifier* namedActionIdentifier)
|
148
|
{
|
149
|
namedActionIdentifier->setBody(sClone(namedActionIdentifier->body()));
|
150
|
|
151
|
}
|
152
|
|
153
|
|
154
|
void DeepCloneVisitor::visit(ObjectConstructor* )
|
155
|
{
|
156
|
|
157
|
}
|
158
|
|
159
|
|
160
|
void DeepCloneVisitor::visit(NondetBlock* nondetBlock)
|
161
|
{
|
162
|
cloneBlock((Block*)nondetBlock);
|
163
|
}
|
164
|
|
165
|
void DeepCloneVisitor::visit(SeqBlock* seqBlock)
|
166
|
{
|
167
|
seqBlock->setFilter(eClone(seqBlock->filter()));
|
168
|
cloneBlock((Block*)seqBlock);
|
169
|
}
|
170
|
|
171
|
void DeepCloneVisitor::visit(PrioBlock* prioBlock)
|
172
|
{
|
173
|
cloneBlock((Block*)prioBlock);
|
174
|
}
|
175
|
|
176
|
|
177
|
void DeepCloneVisitor::visit(AccessExpression* accessExpression)
|
178
|
{
|
179
|
visit((BinaryOperator*)accessExpression);
|
180
|
}
|
181
|
|
182
|
void DeepCloneVisitor::visit(BinaryOperator* binaryOperator)
|
183
|
{
|
184
|
Expression* left = eClone(binaryOperator->left());
|
185
|
Expression* right = eClone(binaryOperator->right());
|
186
|
binaryOperator->setLeftChild(left);
|
187
|
binaryOperator->setRightChild(right);
|
188
|
}
|
189
|
|
190
|
void DeepCloneVisitor::visit(Assignment* assignment)
|
191
|
{
|
192
|
symTabClone(assignment->symbols());
|
193
|
cloneExpressionList(assignment->places());
|
194
|
cloneExpressionList(assignment->values());
|
195
|
assignment->setNondetExpression(eClone(assignment->nondetExpression()));
|
196
|
checkScope(assignment);
|
197
|
}
|
198
|
|
199
|
|
200
|
void DeepCloneVisitor::visit(AttributeIdentifier* attributeIdentifier)
|
201
|
{
|
202
|
attributeIdentifier->setInitializer(eClone(attributeIdentifier->initializer()));
|
203
|
}
|
204
|
|
205
|
void DeepCloneVisitor::visit(Call* call)
|
206
|
{
|
207
|
call->setCallExpression(eClone(call->callExpression()));
|
208
|
}
|
209
|
|
210
|
void DeepCloneVisitor::visit(CallExpression* callExpression)
|
211
|
{
|
212
|
cloneExpressionList(callExpression->arguments());
|
213
|
visit((UnaryOperator*)callExpression);
|
214
|
}
|
215
|
|
216
|
void DeepCloneVisitor::visit(ExistsQuantifier* quantifier)
|
217
|
{
|
218
|
cloneQuantifier((Quantifier*)quantifier);
|
219
|
}
|
220
|
|
221
|
void DeepCloneVisitor::visit(ForallQuantifier* quantifier)
|
222
|
{
|
223
|
cloneQuantifier((Quantifier*)quantifier);
|
224
|
}
|
225
|
|
226
|
void DeepCloneVisitor::visit(GuardedCommand* guardedCommand)
|
227
|
{
|
228
|
Statement* newblock = sClone(guardedCommand->body());
|
229
|
Expression* newguard = eClone(guardedCommand->guard());
|
230
|
guardedCommand->setBody(newblock);
|
231
|
guardedCommand->setGuard(newguard);
|
232
|
}
|
233
|
|
234
|
|
235
|
void DeepCloneVisitor::visit(IdentifierExpression* identifierExpression)
|
236
|
{
|
237
|
if (identifierExpression->isSelf() && m_selfreplacement != nullptr)
|
238
|
identifierExpression->setIdentifier(m_selfreplacement);
|
239
|
else if (m_mapping.count(identifierExpression->identifier()) > 0
|
240
|
&& identifierExpression->identifier()->kind() != IdentifierKind::MethodIdentifier)
|
241
|
{
|
242
|
|
243
|
|
244
|
|
245
|
|
246
|
identifierExpression->setIdentifier((Identifier*)m_mapping[identifierExpression->identifier()]);
|
247
|
}
|
248
|
}
|
249
|
|
250
|
|
251
|
void DeepCloneVisitor::visit(ListConstructor* listConstructor)
|
252
|
{
|
253
|
symTabClone(listConstructor->comprehensionVariables());
|
254
|
cloneExpressionList(listConstructor->elements());
|
255
|
listConstructor->setComprehension(eClone(listConstructor->comprehension()));
|
256
|
}
|
257
|
|
258
|
|
259
|
void DeepCloneVisitor::visit(SetConstructor* setConstructor)
|
260
|
{
|
261
|
symTabClone(setConstructor->comprehensionVariables());
|
262
|
cloneExpressionList(setConstructor->items());
|
263
|
setConstructor->setComprehension(eClone(setConstructor->comprehension()));
|
264
|
}
|
265
|
|
266
|
|
267
|
void DeepCloneVisitor::visit(TernaryOperator* ternaryOperator)
|
268
|
{
|
269
|
ternaryOperator->setLeftChild(eClone(ternaryOperator->left()));
|
270
|
ternaryOperator->setMidChild(eClone(ternaryOperator->mid()));
|
271
|
ternaryOperator->setRightChild(eClone(ternaryOperator->right()));
|
272
|
}
|
273
|
|
274
|
|
275
|
void DeepCloneVisitor::visit(TupleConstructor* tupleConstructor)
|
276
|
{
|
277
|
cloneExpressionList(tupleConstructor->values());
|
278
|
}
|
279
|
|
280
|
|
281
|
void DeepCloneVisitor::visit(TupleMapAccessExpression* tupleMapAccessExpression)
|
282
|
{
|
283
|
tupleMapAccessExpression->setArgument(eClone(tupleMapAccessExpression->argument()));
|
284
|
visit((UnaryOperator*)tupleMapAccessExpression);
|
285
|
}
|
286
|
|
287
|
|
288
|
void DeepCloneVisitor::visit(UnaryOperator* unaryOperator)
|
289
|
{
|
290
|
unaryOperator->setChild(eClone(unaryOperator->child()));
|
291
|
}
|
292
|
|
293
|
}
|