|
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
|
package org.momut.ooas.codegen.cadp;
|
|
29
|
|
|
30
|
import java.util.ArrayList;
|
|
31
|
import java.util.HashSet;
|
|
32
|
import java.util.Iterator;
|
|
33
|
import java.util.List;
|
|
34
|
|
|
35
|
import org.momut.ooas.ast.expressions.AccessExpression;
|
|
36
|
import org.momut.ooas.ast.expressions.BinaryOperator;
|
|
37
|
import org.momut.ooas.ast.expressions.CallExpression;
|
|
38
|
import org.momut.ooas.ast.expressions.ExistsQuantifier;
|
|
39
|
import org.momut.ooas.ast.expressions.Expression;
|
|
40
|
import org.momut.ooas.ast.expressions.ExpressionKind;
|
|
41
|
import org.momut.ooas.ast.expressions.ForallQuantifier;
|
|
42
|
import org.momut.ooas.ast.expressions.IdentifierExpression;
|
|
43
|
import org.momut.ooas.ast.expressions.ListConstructor;
|
|
44
|
import org.momut.ooas.ast.expressions.MapConstructor;
|
|
45
|
import org.momut.ooas.ast.expressions.ObjectConstructor;
|
|
46
|
import org.momut.ooas.ast.expressions.SetConstructor;
|
|
47
|
import org.momut.ooas.ast.expressions.TernaryOperator;
|
|
48
|
import org.momut.ooas.ast.expressions.TupleConstructor;
|
|
49
|
import org.momut.ooas.ast.expressions.TupleMapAccessExpression;
|
|
50
|
import org.momut.ooas.ast.expressions.TypeExpression;
|
|
51
|
import org.momut.ooas.ast.expressions.UnaryOperator;
|
|
52
|
import org.momut.ooas.ast.expressions.UnresolvedIdentifierExpression;
|
|
53
|
import org.momut.ooas.ast.expressions.ValueExpression;
|
|
54
|
import org.momut.ooas.ast.expressions.LeafExpression.LeafTypeEnum;
|
|
55
|
import org.momut.ooas.ast.identifiers.ExpressionVariableIdentifier;
|
|
56
|
import org.momut.ooas.ast.identifiers.FunctionIdentifier;
|
|
57
|
import org.momut.ooas.ast.identifiers.Identifier;
|
|
58
|
import org.momut.ooas.ast.identifiers.IdentifierKind;
|
|
59
|
import org.momut.ooas.ast.types.FunctionType;
|
|
60
|
import org.momut.ooas.ast.types.ListType;
|
|
61
|
import org.momut.ooas.ast.types.MapType;
|
|
62
|
import org.momut.ooas.ast.types.OoActionSystemInstance;
|
|
63
|
import org.momut.ooas.ast.types.OoActionSystemType;
|
|
64
|
import org.momut.ooas.ast.types.QrType;
|
|
65
|
import org.momut.ooas.ast.types.TupleType;
|
|
66
|
import org.momut.ooas.ast.types.TypeKind;
|
|
67
|
import org.momut.ooas.ast.types.UlyssesType;
|
|
68
|
import org.momut.ooas.codegen.OoasCodeEmitter;
|
|
69
|
import org.momut.ooas.parser.SymbolTable;
|
|
70
|
import org.momut.ooas.visitors.OoaExpressionVisitor;
|
|
71
|
|
|
72
|
|
|
73
|
|
|
74
|
|
|
75
|
|
|
76
|
public final class CadpExpression extends OoaExpressionVisitor
|
|
77
|
{
|
|
78
|
private OoasCodeEmitter m_emitter = new OoasCodeEmitter();
|
|
79
|
private final CadpActionInfo m_procInfo;
|
|
80
|
private final ArrayList<Identifier> m_usedIdentifier = new ArrayList<Identifier>();
|
|
81
|
private static OoasCodeEmitter m_helperCode = new OoasCodeEmitter();
|
|
82
|
private static OoasCodeEmitter m_resetCode = new OoasCodeEmitter();
|
|
83
|
|
|
84
|
public static HashSet<String> emittedOperations = new HashSet<String>();
|
|
85
|
public List<Identifier> usedIdentifiers() { return m_usedIdentifier; }
|
|
86
|
|
|
87
|
private String OperatorString(Expression expression)
|
|
88
|
{
|
|
89
|
switch (expression.kind())
|
|
90
|
{
|
|
91
|
case abs:
|
|
92
|
case card:
|
|
93
|
case dom:
|
|
94
|
case range:
|
|
95
|
case merge:
|
|
96
|
case elems:
|
|
97
|
case inds:
|
|
98
|
case dinter:
|
|
99
|
case dunion:
|
|
100
|
case domresby:
|
|
101
|
case domresto:
|
|
102
|
case rngresby:
|
|
103
|
case rngresto:
|
|
104
|
case inter:
|
|
105
|
case union:
|
|
106
|
case munion:
|
|
107
|
case seqmod_mapoverride:
|
|
108
|
case subset:
|
|
109
|
case biimplies:
|
|
110
|
case Primed:
|
|
111
|
throw new UnsupportedOperationException();
|
|
112
|
|
|
113
|
case notelemin:
|
|
114
|
case elemin:
|
|
115
|
case implies:
|
|
116
|
case conc:
|
|
117
|
case head:
|
|
118
|
case tail:
|
|
119
|
case len:
|
|
120
|
throw new IllegalArgumentException();
|
|
121
|
|
|
122
|
|
|
123
|
case div:
|
|
124
|
return "/";
|
|
125
|
case idiv:
|
|
126
|
return "/";
|
|
127
|
case mod:
|
|
128
|
return "%";
|
|
129
|
case prod:
|
|
130
|
return "*";
|
|
131
|
case sum:
|
|
132
|
return "+";
|
|
133
|
case minus:
|
|
134
|
return "-";
|
|
135
|
case less:
|
|
136
|
return "<";
|
|
137
|
case lessequal:
|
|
138
|
return "<=";
|
|
139
|
case greater:
|
|
140
|
return ">";
|
|
141
|
case greaterequal:
|
|
142
|
return ">=";
|
|
143
|
case equal:
|
|
144
|
return "==";
|
|
145
|
case notequal:
|
|
146
|
return "!=";
|
|
147
|
case and:
|
|
148
|
return "&&";
|
|
149
|
case or:
|
|
150
|
return "||";
|
|
151
|
case not:
|
|
152
|
return "!";
|
|
153
|
|
|
154
|
case Cast:
|
|
155
|
throw new IllegalArgumentException();
|
|
156
|
|
|
157
|
|
|
158
|
|
|
159
|
|
|
160
|
|
|
161
|
default:
|
|
162
|
return expression.kind().toString();
|
|
163
|
}
|
|
164
|
}
|
|
165
|
@Override
|
|
166
|
public <T>void visit(ValueExpression<T> valueExpression)
|
|
167
|
{
|
|
168
|
if (valueExpression.value() == null)
|
|
169
|
{
|
|
170
|
m_emitter.Append("NULL");
|
|
171
|
}
|
|
172
|
else if (valueExpression.valueType() == LeafTypeEnum.bool)
|
|
173
|
{
|
|
174
|
|
|
175
|
final boolean aboolval = (Boolean)valueExpression.value();
|
|
176
|
m_emitter.AppendLine(aboolval ? "1" : "0");
|
|
177
|
}
|
|
178
|
else if (valueExpression.valueType() == LeafTypeEnum.chr)
|
|
179
|
m_emitter.Append(String.format("'%1$s'", valueExpression.toString()));
|
|
180
|
else
|
|
181
|
m_emitter.Append(valueExpression.value().toString());
|
|
182
|
}
|
|
183
|
@Override
|
|
184
|
public void visit(UnresolvedIdentifierExpression unresolvedIdentifierExpression)
|
|
185
|
{
|
|
186
|
throw new IllegalArgumentException();
|
|
187
|
}
|
|
188
|
|
|
189
|
@Override
|
|
190
|
public void visit(IdentifierExpression identifierExpression)
|
|
191
|
{
|
|
192
|
final CadpIdentifier idvis = new CadpIdentifier(m_procInfo.stateVariableString);
|
|
193
|
identifierExpression.Accept(idvis);
|
|
194
|
m_emitter.Append(idvis.toString());
|
|
195
|
|
|
196
|
if (identifierExpression.identifier().kind() == IdentifierKind.ExpressionVariableIdentifier)
|
|
197
|
{
|
|
198
|
|
|
199
|
|
|
200
|
final ExpressionVariableIdentifier id = (ExpressionVariableIdentifier)identifierExpression.identifier();
|
|
201
|
if (!emittedVariabes.contains(id))
|
|
202
|
{
|
|
203
|
emittedVariabes.add(id);
|
|
204
|
final CadpType atype = new CadpType();
|
|
205
|
id.type().Accept(atype);
|
|
206
|
varDecl.Append(String.format("%1$s %2$s; ", atype.ToString(), idvis.toString()));
|
|
207
|
}
|
|
208
|
}
|
|
209
|
|
|
210
|
if (!m_usedIdentifier.contains(identifierExpression.identifier()))
|
|
211
|
m_usedIdentifier.add(identifierExpression.identifier());
|
|
212
|
}
|
|
213
|
|
|
214
|
@Override
|
|
215
|
public void visit(TypeExpression typeExpression)
|
|
216
|
{
|
|
217
|
m_emitter.Append(typeExpression.type().identifier().tokenText());
|
|
218
|
}
|
|
219
|
|
|
220
|
@Override
|
|
221
|
public void visit(ListConstructor listConstructor)
|
|
222
|
{
|
|
223
|
final ListType aListType = (ListType)listConstructor.type();
|
|
224
|
if (!listConstructor.hasComprehension())
|
|
225
|
{
|
|
226
|
CadpType.EmitType(aListType);
|
|
227
|
|
|
228
|
m_emitter.Append(String.format("%1$s%2$s(%3$s", CadpType.constructorString, CadpIdentifier.GetIdentifierString(aListType.identifier()), listConstructor.elements().size()));
|
|
229
|
int i;
|
|
230
|
for (i = 0; i < aListType.maxNumberOfElements(); i++)
|
|
231
|
{
|
|
232
|
m_emitter.Append(", ");
|
|
233
|
if (i < listConstructor.elements().size())
|
|
234
|
listConstructor.elements().get(i).Accept(this);
|
|
235
|
else
|
|
236
|
m_emitter.Append(String.format("%1$s%2$s(%3$s%2$s())", CadpType.enumString, CadpIdentifier.GetIdentifierString(aListType.innerType().identifier()), CadpType.lowString));
|
|
237
|
}
|
|
238
|
m_emitter.Append(")");
|
|
239
|
}
|
|
240
|
else
|
|
241
|
{
|
|
242
|
final CadpExpression compExpr = new CadpExpression(new CadpActionInfo(null, -1, 0, m_procInfo.toDoListString, m_procInfo.doneListString, "aState"), emittedVariabes);
|
|
243
|
if (listConstructor.comprehension() != null)
|
|
244
|
listConstructor.comprehension().Accept(compExpr);
|
|
245
|
else
|
|
246
|
new ValueExpression<Integer>(1, 0, 0, Integer.class).Accept(compExpr);
|
|
247
|
|
|
248
|
final CadpExpression listElementExpr = new CadpExpression(m_procInfo, emittedVariabes);
|
|
249
|
listConstructor.elements().get(0).Accept(listElementExpr);
|
|
250
|
|
|
251
|
|
|
252
|
compExpr.usedIdentifiers().addAll(listElementExpr.usedIdentifiers());
|
|
253
|
final List<Identifier> importVars = getListOfAccessedIdentifiers(compExpr, listConstructor.comprehensionVariables());
|
|
254
|
|
|
255
|
|
|
256
|
|
|
257
|
|
|
258
|
|
|
259
|
|
|
260
|
final List<Identifier> varsToRemove = new ArrayList<Identifier>();
|
|
261
|
|
|
262
|
for (final Identifier id : importVars)
|
|
263
|
{
|
|
264
|
final CadpType atype = new CadpType();
|
|
265
|
id.type().Accept(atype);
|
|
266
|
final String typeAndName = (String.format("%1$s %2$s; ", atype.ToString(), id.tokenText()));
|
|
267
|
|
|
268
|
if (compExpr.VariableDeclarations().contains(typeAndName))
|
|
269
|
varsToRemove.add(id);
|
|
270
|
}
|
|
271
|
int tmpcntr = importVars.size() -1;
|
|
272
|
for (tmpcntr = importVars.size() -1; tmpcntr>=0; tmpcntr--)
|
|
273
|
if (varsToRemove.contains(importVars.get(tmpcntr)))
|
|
274
|
importVars.remove(tmpcntr);
|
|
275
|
|
|
276
|
|
|
277
|
final String functionName = String.format("create_dyn_list_%1$s", OoaCADPVisitor.getUIntHashCode(listConstructor));
|
|
278
|
m_emitter.Append(functionName);
|
|
279
|
m_emitter.Append(String.format("( %1$s", this.m_procInfo.stateVariableString));
|
|
280
|
for (final Identifier x : importVars)
|
|
281
|
{
|
|
282
|
m_emitter.Append(",");
|
|
283
|
m_emitter.Append(String.format("%1$s", CadpIdentifier.GetIdentifierString(x)));
|
|
284
|
}
|
|
285
|
m_emitter.Append(")");
|
|
286
|
|
|
287
|
|
|
288
|
final ListType listType = (ListType)listConstructor.type();
|
|
289
|
CadpType.EmitType(listType.innerType());
|
|
290
|
final OoasCodeEmitter helper = new OoasCodeEmitter();
|
|
291
|
final String listtypename = String.format("struct_list_%1$s", CadpType.DumpType(listType.innerType()).replaceAll(" ", "_"));
|
|
292
|
|
|
293
|
|
|
294
|
final StringBuilder typedefbuilder = new StringBuilder();
|
|
295
|
typedefbuilder.append("#ifdef WINDOWSPACK" + System.lineSeparator());
|
|
296
|
typedefbuilder.append("#pragma pack(1)" + System.lineSeparator());
|
|
297
|
typedefbuilder.append("#endif" + System.lineSeparator());
|
|
298
|
typedefbuilder.append(String.format("struct %2$s { struct %2$s *next; %1$s element;} UNIXPACK;", CadpType.DumpType(listType.innerType()), listtypename));
|
|
299
|
typedefbuilder.append(System.lineSeparator());
|
|
300
|
final String listStruct = typedefbuilder.toString();
|
|
301
|
CadpType.AddTypeDefinition(listStruct);
|
|
302
|
|
|
303
|
helper.AppendLine(String.format("struct %1$s* %2$s(CAESAR_TYPE_STATE aState", listtypename, functionName));
|
|
304
|
for (final Identifier x : importVars)
|
|
305
|
{
|
|
306
|
helper.Append(", ");
|
|
307
|
helper.Append(String.format("%1$s %2$s", CadpType.DumpType(x.type()), CadpIdentifier.GetIdentifierString(x)));
|
|
308
|
}
|
|
309
|
helper.AppendLine("){");
|
|
310
|
|
|
311
|
helper.AppendLine(String.format("struct %1$s* result = NULL;", listtypename));
|
|
312
|
helper.AppendLine(String.format("struct %1$s* __currhead = NULL;", listtypename));
|
|
313
|
helper.AppendLine(compExpr.VariableDeclarations());
|
|
314
|
|
|
315
|
int loops = 0;
|
|
316
|
for (final Identifier enumvar : listConstructor.comprehensionVariables().symbolList())
|
|
317
|
{
|
|
318
|
helper.AppendLine(String.format("long long iterator_%1$s;", CadpIdentifier.GetIdentifierString(enumvar)));
|
|
319
|
helper.AppendLine(String.format("for (iterator_%1$s = %2$s; iterator_%1$s <= %3$s; iterator_%1$s++) {",
|
|
320
|
CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetMinVal(enumvar.type()), CadpType.GetMaxVal(enumvar.type())));
|
|
321
|
|
|
322
|
if (compExpr.VariableDeclarations().contains(String.format(" %1$s;", CadpIdentifier.GetIdentifierString(enumvar))))
|
|
323
|
helper.AppendLine(String.format("/*%1$s*/ %2$s = %3$s(iterator_%2$s);",
|
|
324
|
CadpType.DumpType(enumvar.type()), CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetEnumVal(enumvar.type())));
|
|
325
|
else
|
|
326
|
helper.AppendLine(String.format("%1$s %2$s = %3$s(iterator_%2$s);",
|
|
327
|
CadpType.DumpType(enumvar.type()), CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetEnumVal(enumvar.type())));
|
|
328
|
loops++;
|
|
329
|
}
|
|
330
|
|
|
331
|
helper.AppendLine(String.format("%1$s __newElem;", CadpType.DumpType(listType.innerType())));
|
|
332
|
|
|
333
|
|
|
334
|
helper.AppendLine(String.format("if ((%1$s) && (CALC_INVALID == 0)) { __newElem = %2$s; ", compExpr.toString(), listElementExpr.toString()));
|
|
335
|
|
|
336
|
helper.AppendLine(String.format("struct %1$s* __listelem = (struct %1$s*) malloc(sizeof(struct %1$s));", listtypename));
|
|
337
|
helper.AppendLine(String.format("if (__listelem == NULL) { fprintf(stderr,\"malloc failure\"); exit(1);}"));
|
|
338
|
helper.AppendLine(String.format("memset((char*)__listelem,0,sizeof(struct %1$s));", listtypename));
|
|
339
|
|
|
340
|
helper.AppendLine(String.format(String.format("memcpy(&(__listelem->element),&__newElem, sizeof(%1$s));", CadpType.DumpType(listType.innerType()))));
|
|
341
|
helper.AppendLine(String.format("if (result == NULL) result = __listelem; else __currhead->next = __listelem; __currhead = __listelem;"));
|
|
342
|
|
|
343
|
helper.AppendLine("} /*if*/");
|
|
344
|
helper.AppendLine("if (CALC_INVALID == 1) CALC_INVALID = 0;");
|
|
345
|
while (loops > 0)
|
|
346
|
{
|
|
347
|
helper.AppendLine("}");
|
|
348
|
loops--;
|
|
349
|
}
|
|
350
|
helper.AppendLine("return result; }");
|
|
351
|
|
|
352
|
m_helperCode.Append(helper.toString());
|
|
353
|
}
|
|
354
|
}
|
|
355
|
|
|
356
|
@Override
|
|
357
|
public void visit(SetConstructor setConstructor)
|
|
358
|
{
|
|
359
|
final ListType aSetType = (ListType)setConstructor.type();
|
|
360
|
m_emitter.Append(String.format(" /*set constr*/ %1$s%2$s(", CadpType.constructorString, CadpIdentifier.GetIdentifierString(aSetType.identifier())));
|
|
361
|
m_emitter.Append(setConstructor.items().size());
|
|
362
|
for (final Expression x : setConstructor.items())
|
|
363
|
{
|
|
364
|
m_emitter.Append(", ");
|
|
365
|
x.Accept(this);
|
|
366
|
}
|
|
367
|
m_emitter.Append(")");
|
|
368
|
}
|
|
369
|
|
|
370
|
@Override
|
|
371
|
public void visit(MapConstructor mapConstructor)
|
|
372
|
{
|
|
373
|
throw new UnsupportedOperationException();
|
|
374
|
}
|
|
375
|
|
|
376
|
@Override
|
|
377
|
public void visit(TupleConstructor tupleConstructor)
|
|
378
|
{
|
|
379
|
final TupleType aTupleType = (TupleType)tupleConstructor.type();
|
|
380
|
|
|
381
|
if (tupleConstructor.isMatcher())
|
|
382
|
{
|
|
383
|
|
|
384
|
throw new IllegalArgumentException();
|
|
385
|
}
|
|
386
|
else
|
|
387
|
{
|
|
388
|
m_emitter.Append(String.format("%1$s%2$s(", CadpType.constructorString, CadpIdentifier.GetIdentifierString(aTupleType.identifier())));
|
|
389
|
int i = 0;
|
|
390
|
for (final Expression x : tupleConstructor.values())
|
|
391
|
{
|
|
392
|
if (i != 0)
|
|
393
|
m_emitter.Append(", ");
|
|
394
|
else
|
|
395
|
i++;
|
|
396
|
x.Accept(this);
|
|
397
|
}
|
|
398
|
m_emitter.Append(")");
|
|
399
|
}
|
|
400
|
}
|
|
401
|
|
|
402
|
@Override
|
|
403
|
public void visit(ObjectConstructor objectConstructor)
|
|
404
|
{
|
|
405
|
final OoActionSystemInstance instance = objectConstructor.GetNextInstance();
|
|
406
|
CadpType.EmitType(instance.Type);
|
|
407
|
if (objectConstructor.instances().size() == 1)
|
|
408
|
{
|
|
409
|
m_emitter.Append(String.format("%1$s", instance.Name));
|
|
410
|
}
|
|
411
|
else
|
|
412
|
{
|
|
413
|
final String helpername = String.format("obj_constr_%1$s", OoaCADPVisitor.getUIntHashCode(objectConstructor));
|
|
414
|
m_emitter.Append(String.format("%1$s()", helpername));
|
|
415
|
|
|
416
|
|
|
417
|
|
|
418
|
final OoasCodeEmitter helper = new OoasCodeEmitter();
|
|
419
|
helper.AppendLine(String.format("int %1$s_counter = 0;", helpername));
|
|
420
|
m_resetCode.AppendLine(String.format("%1$s_counter = 0;", helpername));
|
|
421
|
helper.AppendLine(String.format("%1$s %2$s(){", CadpType.DumpType(objectConstructor.type()), helpername));
|
|
422
|
int i = 0;
|
|
423
|
for (final OoActionSystemInstance x : objectConstructor.instances())
|
|
424
|
{
|
|
425
|
CadpType.EmitType(x.Type);
|
|
426
|
helper.AppendLine(String.format("if (%1$s_counter == %2$s) {%1$s_counter++; return %3$s;}",
|
|
427
|
helpername, i, x.Name));
|
|
428
|
i++;
|
|
429
|
}
|
|
430
|
helper.AppendLine(String.format("fprintf(stderr,\"constructor called too often: %1$s\"); exit(1);", helpername));
|
|
431
|
helper.Append("}");
|
|
432
|
m_helperCode.AppendLine(helper.toString());
|
|
433
|
}
|
|
434
|
}
|
|
435
|
|
|
436
|
|
|
437
|
@Override
|
|
438
|
public void visit(AccessExpression accessExpression)
|
|
439
|
{
|
|
440
|
|
|
441
|
if (accessExpression.left().kind() == ExpressionKind.Type &&
|
|
442
|
((TypeExpression)accessExpression.left()).type().kind() == TypeKind.EnumeratedType )
|
|
443
|
{
|
|
444
|
accessExpression.right().Accept(this);
|
|
445
|
return;
|
|
446
|
}
|
|
447
|
|
|
448
|
|
|
449
|
|
|
450
|
if (accessExpression.left().kind() == ExpressionKind.Identifier &&
|
|
451
|
((IdentifierExpression)accessExpression.left()).isSelf())
|
|
452
|
{
|
|
453
|
if (accessExpression.right().kind() != ExpressionKind.Identifier ||
|
|
454
|
((IdentifierExpression)accessExpression.right()).identifier().kind() != IdentifierKind.MethodIdentifier)
|
|
455
|
{
|
|
456
|
accessExpression.right().Accept(this);
|
|
457
|
return;
|
|
458
|
}
|
|
459
|
}
|
|
460
|
|
|
461
|
accessExpression.left().Accept(this);
|
|
462
|
m_emitter.Append(".");
|
|
463
|
|
|
464
|
if (((IdentifierExpression)accessExpression.right()).identifier().kind() == IdentifierKind.MethodIdentifier ||
|
|
465
|
((IdentifierExpression)accessExpression.right()).identifier().kind() == IdentifierKind.NamedActionIdentifier)
|
|
466
|
m_emitter.Append("methods->");
|
|
467
|
accessExpression.right().Accept(this);
|
|
468
|
}
|
|
469
|
|
|
470
|
|
|
471
|
OoasCodeEmitter varDecl = new OoasCodeEmitter();
|
|
472
|
HashSet<Identifier> emittedVariabes = new HashSet<Identifier>();
|
|
473
|
|
|
474
|
public void addEmittedVariables(HashSet<Identifier> elementsToAdd)
|
|
475
|
{
|
|
476
|
emittedVariabes.addAll(elementsToAdd);
|
|
477
|
}
|
|
478
|
|
|
479
|
private void EmitMatcher(TupleConstructor tupleConstructor, Expression expression)
|
|
480
|
{
|
|
481
|
final OoasCodeEmitter tmp = m_emitter;
|
|
482
|
|
|
483
|
m_emitter = new OoasCodeEmitter();
|
|
484
|
expression.Accept(this);
|
|
485
|
final OoasCodeEmitter expr = m_emitter;
|
|
486
|
m_emitter = tmp;
|
|
487
|
|
|
488
|
|
|
489
|
final Iterator<UlyssesType> elem = ((TupleType)tupleConstructor.type()).innerTypes().iterator();
|
|
490
|
int i = 0;
|
|
491
|
m_emitter.Append("(");
|
|
492
|
while (elem.hasNext())
|
|
493
|
{
|
|
494
|
final Expression var = tupleConstructor.values().get(i);
|
|
495
|
|
|
496
|
if (i != 0)
|
|
497
|
m_emitter.Append(" , ");
|
|
498
|
|
|
499
|
var.Accept(this);
|
|
500
|
m_emitter.Append(String.format(" = (%1$s).elem_%2$s ", expr.toString(), i));
|
|
501
|
|
|
502
|
i++;
|
|
503
|
}
|
|
504
|
m_emitter.Append(", 1==1)");
|
|
505
|
}
|
|
506
|
|
|
507
|
private void EmitDefaultBinaryOperator(BinaryOperator binaryOperator)
|
|
508
|
{
|
|
509
|
m_emitter.Append("(");
|
|
510
|
VisitSub(binaryOperator.left(), binaryOperator);
|
|
511
|
m_emitter.Append(") ");
|
|
512
|
m_emitter.Append(OperatorString(binaryOperator));
|
|
513
|
m_emitter.Append(" (");
|
|
514
|
VisitSub(binaryOperator.right(), binaryOperator);
|
|
515
|
m_emitter.Append(")");
|
|
516
|
}
|
|
517
|
|
|
518
|
@Override
|
|
519
|
public void visit(BinaryOperator binaryOperator)
|
|
520
|
{
|
|
521
|
switch (binaryOperator.kind())
|
|
522
|
{
|
|
523
|
case equal:
|
|
524
|
|
|
525
|
if (binaryOperator.left().kind() == ExpressionKind.TupleConstr &&
|
|
526
|
((TupleConstructor)binaryOperator.left()).isMatcher())
|
|
527
|
{
|
|
528
|
EmitMatcher((TupleConstructor)binaryOperator.left(), binaryOperator.right());
|
|
529
|
}
|
|
530
|
else if (binaryOperator.right().kind() == ExpressionKind.TupleConstr &&
|
|
531
|
((TupleConstructor)binaryOperator.right()).isMatcher())
|
|
532
|
{
|
|
533
|
EmitMatcher((TupleConstructor)binaryOperator.right(), binaryOperator.left());
|
|
534
|
}
|
|
535
|
else if (!CadpType.IsNumeric(binaryOperator.left().type()))
|
|
536
|
{
|
|
537
|
m_emitter.Append("0 == ");
|
|
538
|
EmitComplexEqual(binaryOperator);
|
|
539
|
}
|
|
540
|
else
|
|
541
|
EmitDefaultBinaryOperator(binaryOperator);
|
|
542
|
break;
|
|
543
|
case notequal:
|
|
544
|
if (!CadpType.IsNumeric(binaryOperator.left().type()))
|
|
545
|
{
|
|
546
|
m_emitter.Append("0 != ");
|
|
547
|
EmitComplexEqual(binaryOperator);
|
|
548
|
}
|
|
549
|
else
|
|
550
|
EmitDefaultBinaryOperator(binaryOperator);
|
|
551
|
break;
|
|
552
|
case conc:
|
|
553
|
final String conc = EmitConcOperation(binaryOperator);
|
|
554
|
m_emitter.Append(String.format("%1$s(", conc));
|
|
555
|
VisitSub(binaryOperator.left(), binaryOperator);
|
|
556
|
m_emitter.Append(",");
|
|
557
|
VisitSub(binaryOperator.right(), binaryOperator);
|
|
558
|
m_emitter.Append(")");
|
|
559
|
break;
|
|
560
|
case implies:
|
|
561
|
m_emitter.Append("!(");
|
|
562
|
VisitSub(binaryOperator.left(), binaryOperator);
|
|
563
|
m_emitter.Append(") || (");
|
|
564
|
VisitSub(binaryOperator.right(), binaryOperator);
|
|
565
|
m_emitter.Append(")");
|
|
566
|
break;
|
|
567
|
case elemin:
|
|
568
|
EmitInOperator(binaryOperator);
|
|
569
|
break;
|
|
570
|
case notelemin:
|
|
571
|
EmitNotInOperator(binaryOperator);
|
|
572
|
break;
|
|
573
|
case diff:
|
|
574
|
final String diff = EmitSetDifference(binaryOperator);
|
|
575
|
m_emitter.Append(String.format("%1$s(", diff));
|
|
576
|
VisitSub(binaryOperator.left(), binaryOperator);
|
|
577
|
m_emitter.Append(",");
|
|
578
|
VisitSub(binaryOperator.right(), binaryOperator);
|
|
579
|
m_emitter.Append(")");
|
|
580
|
break;
|
|
581
|
default:
|
|
582
|
EmitDefaultBinaryOperator(binaryOperator);
|
|
583
|
break;
|
|
584
|
}
|
|
585
|
}
|
|
586
|
|
|
587
|
private String EmitSetDifference(BinaryOperator binaryOperator)
|
|
588
|
{
|
|
589
|
final String childBTypeName = CadpIdentifier.GetIdentifierString(binaryOperator.right().type().identifier());
|
|
590
|
final String childATypeName = CadpIdentifier.GetIdentifierString(binaryOperator.left().type().identifier());
|
|
591
|
final String result = String.format("op_listdiff_%1$s_%2$s", childATypeName, childBTypeName);
|
|
592
|
if (emittedOperations.contains(result))
|
|
593
|
return result;
|
|
594
|
|
|
595
|
CadpType.EmitType(binaryOperator.type());
|
|
596
|
final ListType alist = (ListType)binaryOperator.type();
|
|
597
|
final UlyssesType innerType = alist.innerType();
|
|
598
|
final String resultTypeName = CadpIdentifier.GetIdentifierString(binaryOperator.type().identifier());
|
|
599
|
|
|
600
|
m_helperCode.AppendLine(String.format("%4$s %3$s(%1$s listA, %2$s listB){", childATypeName, childBTypeName, result, resultTypeName));
|
|
601
|
m_helperCode.AppendLine(String.format("%1$s result;", resultTypeName));
|
|
602
|
m_helperCode.AppendLine(String.format("int len = 0; int i; int j;"));
|
|
603
|
|
|
604
|
m_helperCode.AppendLine(String.format("for (i = 0; i < listA.length; i++) {"));
|
|
605
|
m_helperCode.AppendLine(String.format("for (j = 0; j < listB.length; j++) {"));
|
|
606
|
m_helperCode.AppendLine(String.format("if (memcmp(&listA.elements[i],&listB.elements[j],sizeof(%1$s))==0)", CadpType.DumpType(innerType)));
|
|
607
|
m_helperCode.AppendLine("goto NotCopy;");
|
|
608
|
m_helperCode.AppendLine("}");
|
|
609
|
m_helperCode.AppendLine(String.format("memcpy(&result.elements[len],&listA.elements[i],sizeof(%1$s));", CadpType.DumpType(innerType)));
|
|
610
|
m_helperCode.AppendLine("len++;");
|
|
611
|
m_helperCode.AppendLine("NotCopy:");
|
|
612
|
m_helperCode.AppendLine("len = len;");
|
|
613
|
m_helperCode.AppendLine("}");
|
|
614
|
m_helperCode.AppendLine("result.length = len;");
|
|
615
|
|
|
616
|
|
|
617
|
m_helperCode.AppendLine(String.format("int counter;"));
|
|
618
|
m_helperCode.AppendLine(String.format("for (counter = %1$s; counter >= result.length; counter--) {", ((ListType)binaryOperator.type()).maxNumberOfElements() - 1));
|
|
619
|
m_helperCode.AppendLine(String.format("result.elements[counter] = %1$s%2$s(%3$s%2$s());}",
|
|
620
|
CadpType.enumString, CadpIdentifier.GetIdentifierString(alist.innerType().identifier()), CadpType.lowString));
|
|
621
|
|
|
622
|
m_helperCode.AppendLine("return result; }");
|
|
623
|
|
|
624
|
emittedOperations.add(result);
|
|
625
|
return result;
|
|
626
|
}
|
|
627
|
|
|
628
|
private void EmitInOperator(BinaryOperator binop)
|
|
629
|
{
|
|
630
|
m_emitter.Append(String.format("0 != setin_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
|
|
631
|
VisitSub(binop.left(), binop);
|
|
632
|
m_emitter.Append(",");
|
|
633
|
VisitSub(binop.right(), binop);
|
|
634
|
m_emitter.Append(")");
|
|
635
|
|
|
636
|
CadpType.EmitType(binop.left().type());
|
|
637
|
CadpType.EmitType(binop.right().type());
|
|
638
|
final OoasCodeEmitter helper = new OoasCodeEmitter();
|
|
639
|
helper.Append(String.format("int setin_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
|
|
640
|
helper.AppendLine(String.format("%1$s arg1, %2$s arg2){", CadpType.DumpType(binop.left().type()), CadpType.DumpType(binop.right().type())));
|
|
641
|
helper.AppendLine("int __counter;");
|
|
642
|
helper.AppendLine(String.format("for (__counter = 0; __counter < arg2.length; __counter++)"));
|
|
643
|
helper.AppendLine(String.format("if (memcmp(&arg1,&(arg2.elements[__counter]),sizeof(%1$s))==0) return 1;", CadpType.DumpType(binop.left().type())));
|
|
644
|
helper.AppendLine("return 0;}");
|
|
645
|
m_helperCode.Append(helper.toString());
|
|
646
|
}
|
|
647
|
|
|
648
|
|
|
649
|
private void EmitNotInOperator(BinaryOperator binop)
|
|
650
|
{
|
|
651
|
m_emitter.Append(String.format("0 == setin_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
|
|
652
|
VisitSub(binop.left(), binop);
|
|
653
|
m_emitter.Append(",");
|
|
654
|
VisitSub(binop.right(), binop);
|
|
655
|
m_emitter.Append(")");
|
|
656
|
|
|
657
|
CadpType.EmitType(binop.left().type());
|
|
658
|
CadpType.EmitType(binop.right().type());
|
|
659
|
final OoasCodeEmitter helper = new OoasCodeEmitter();
|
|
660
|
helper.Append(String.format("int setin_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
|
|
661
|
helper.AppendLine(String.format("%1$s arg1, %2$s arg2){", CadpType.DumpType(binop.left().type()), CadpType.DumpType(binop.right().type())));
|
|
662
|
helper.AppendLine("int __counter;");
|
|
663
|
helper.AppendLine(String.format("for (__counter = 0; __counter < arg2.length; __counter++)"));
|
|
664
|
helper.AppendLine(String.format("if (memcmp(&arg1,&(arg2.elements[__counter]),sizeof(%1$s))==0) return 1;", CadpType.DumpType(binop.left().type())));
|
|
665
|
helper.AppendLine("return 0;}");
|
|
666
|
m_helperCode.Append(helper.toString());
|
|
667
|
}
|
|
668
|
|
|
669
|
|
|
670
|
|
|
671
|
private void EmitComplexEqual(BinaryOperator binop)
|
|
672
|
{
|
|
673
|
m_emitter.Append(String.format("complex_equal_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
|
|
674
|
VisitSub(binop.left(), binop);
|
|
675
|
m_emitter.Append(",");
|
|
676
|
VisitSub(binop.right(), binop);
|
|
677
|
m_emitter.Append(")");
|
|
678
|
|
|
679
|
CadpType.EmitType(binop.left().type());
|
|
680
|
CadpType.EmitType(binop.right().type());
|
|
681
|
final OoasCodeEmitter helper = new OoasCodeEmitter();
|
|
682
|
helper.Append(String.format("int complex_equal_%1$s(", OoaCADPVisitor.getUIntHashCode(binop)));
|
|
683
|
helper.AppendLine(String.format("%1$s arg1, %2$s arg2){", CadpType.DumpType(binop.left().type()), CadpType.DumpType(binop.right().type())));
|
|
684
|
helper.AppendLine(String.format("return memcmp(&arg1, &arg2, sizeof(%1$s));}", CadpIdentifier.GetIdentifierString(binop.left().type().identifier())));
|
|
685
|
m_helperCode.Append(helper.toString());
|
|
686
|
}
|
|
687
|
|
|
688
|
private String EmitConcOperation(BinaryOperator binaryOperator)
|
|
689
|
{
|
|
690
|
final String childBTypeName = CadpIdentifier.GetIdentifierString(binaryOperator.right().type().identifier());
|
|
691
|
final String childATypeName = CadpIdentifier.GetIdentifierString(binaryOperator.left().type().identifier());
|
|
692
|
final String result = String.format("op_conc_%1$s_%2$s", childATypeName, childBTypeName);
|
|
693
|
if (emittedOperations.contains(result))
|
|
694
|
return result;
|
|
695
|
|
|
696
|
CadpType.EmitType(binaryOperator.type());
|
|
697
|
final ListType alist = (ListType)binaryOperator.type();
|
|
698
|
final UlyssesType innerType = alist.innerType();
|
|
699
|
final String resultTypeName = CadpIdentifier.GetIdentifierString(binaryOperator.type().identifier());
|
|
700
|
|
|
701
|
m_helperCode.AppendLine(String.format("%4$s %3$s(%1$s listA, %2$s listB){", childATypeName, childBTypeName, result, resultTypeName));
|
|
702
|
m_helperCode.AppendLine(String.format("%1$s result;", resultTypeName));
|
|
703
|
m_helperCode.AppendLine(String.format("result.length = listA.length + listB.length;"));
|
|
704
|
|
|
705
|
m_helperCode.AppendLine(String.format("if (result.length > %1$s) { printf(\"Concatenation result too long! %2$s\\n\"); abort();}", alist.maxNumberOfElements(), result));
|
|
706
|
m_helperCode.AppendLine(String.format("memcpy(&result.elements[0],&listA.elements[0],listA.length * sizeof(%1$s));", CadpType.DumpType(innerType)));
|
|
707
|
m_helperCode.AppendLine(String.format("memcpy(&result.elements[listA.length],&listB.elements[0],listB.length * sizeof(%1$s));", CadpType.DumpType(innerType)));
|
|
708
|
m_helperCode.AppendLine(String.format("int counter;"));
|
|
709
|
m_helperCode.AppendLine(String.format("for (counter = %1$s; counter >= (listA.length + listB.length); counter--) {", alist.maxNumberOfElements() - 1));
|
|
710
|
m_helperCode.AppendLine(String.format("result.elements[counter] = %1$s%2$s(%3$s%2$s());}",
|
|
711
|
CadpType.enumString, CadpIdentifier.GetIdentifierString(alist.innerType().identifier()), CadpType.lowString));
|
|
712
|
m_helperCode.AppendLine("return result; }");
|
|
713
|
|
|
714
|
emittedOperations.add(result);
|
|
715
|
return result;
|
|
716
|
}
|
|
717
|
|
|
718
|
@Override
|
|
719
|
public void visit(TernaryOperator ternaryOperator)
|
|
720
|
{
|
|
721
|
if (ternaryOperator.kind() == ExpressionKind.conditional)
|
|
722
|
{
|
|
723
|
m_emitter.Append("(");
|
|
724
|
VisitSub(ternaryOperator.left(), ternaryOperator);
|
|
725
|
m_emitter.Append(" ? ");
|
|
726
|
|
|
727
|
VisitSub(ternaryOperator.mid(), ternaryOperator);
|
|
728
|
m_emitter.Append(" : ");
|
|
729
|
|
|
730
|
VisitSub(ternaryOperator.right(), ternaryOperator);
|
|
731
|
m_emitter.Append(")");
|
|
732
|
}
|
|
733
|
else if (ternaryOperator.kind() == ExpressionKind.foldLR ||
|
|
734
|
ternaryOperator.kind() == ExpressionKind.foldRL)
|
|
735
|
{
|
|
736
|
final CallExpression leftcall = (CallExpression)ternaryOperator.left();
|
|
737
|
final Expression initializer = ternaryOperator.mid();
|
|
738
|
final Expression listgetter = ternaryOperator.right();
|
|
739
|
|
|
740
|
m_emitter.Append(String.format("fold_%1$s(%2$s", OoaCADPVisitor.getUIntHashCode(ternaryOperator), m_procInfo.stateVariableString));
|
|
741
|
|
|
742
|
|
|
743
|
final CadpExpression cadpexpr = new CadpExpression(m_procInfo, emittedVariabes);
|
|
744
|
leftcall.child().Accept(cadpexpr);
|
|
745
|
final List<String> paramtypes = new ArrayList<String>();
|
|
746
|
final List<String> parameters = new ArrayList<String>();
|
|
747
|
for (int i = 0; i < leftcall.arguments().size() - 2; i++)
|
|
748
|
{
|
|
749
|
final Expression arg = leftcall.arguments().get(i);
|
|
750
|
final CadpExpression paramexpr = new CadpExpression(m_procInfo, emittedVariabes);
|
|
751
|
arg.Accept(paramexpr);
|
|
752
|
m_emitter.Append(",");
|
|
753
|
m_emitter.Append(paramexpr.toString());
|
|
754
|
}
|
|
755
|
|
|
756
|
final FunctionType fun = (FunctionType)leftcall.child().type();
|
|
757
|
final FunctionIdentifier funid = (FunctionIdentifier) fun.identifier();
|
|
758
|
final Iterator<UlyssesType> node = fun.parameter().iterator();
|
|
759
|
for (int i = 0; i < fun.parameter().size() - 2; i++)
|
|
760
|
{
|
|
761
|
final UlyssesType nodeValue = node.next();
|
|
762
|
paramtypes.add(CadpType.DumpType(nodeValue));
|
|
763
|
final CadpIdentifier paramid = new CadpIdentifier(m_procInfo.stateVariableString);
|
|
764
|
funid.parameter().get(i).Accept(paramid);
|
|
765
|
parameters.add(paramid.toString());
|
|
766
|
}
|
|
767
|
|
|
768
|
m_emitter.Append(")");
|
|
769
|
|
|
770
|
|
|
771
|
CadpType.EmitType(initializer.type());
|
|
772
|
CadpType.EmitType(listgetter.type());
|
|
773
|
final ListType thelist = (ListType)listgetter.type();
|
|
774
|
CadpType.EmitType(thelist.innerType());
|
|
775
|
final OoasCodeEmitter helper = new OoasCodeEmitter();
|
|
776
|
helper.Append(String.format("%2$s fold_%1$s(CAESAR_TYPE_STATE oldState", OoaCADPVisitor.getUIntHashCode(ternaryOperator), CadpType.DumpType(leftcall.type())));
|
|
777
|
if (paramtypes.size() > 0)
|
|
778
|
{
|
|
779
|
for (int i = 0; i < paramtypes.size(); i++)
|
|
780
|
{
|
|
781
|
helper.Append(",");
|
|
782
|
helper.Append(paramtypes.get(i));
|
|
783
|
helper.Append(" ");
|
|
784
|
helper.Append(parameters.get(i));
|
|
785
|
}
|
|
786
|
}
|
|
787
|
helper.AppendLine("){");
|
|
788
|
|
|
789
|
helper.AppendLine(String.format("int __iterator;"));
|
|
790
|
helper.AppendLine(String.format("%1$s param__result;", CadpType.DumpType(leftcall.type())));
|
|
791
|
helper.AppendLine(String.format("%1$s __thelist;", CadpType.DumpType(listgetter.type())));
|
|
792
|
helper.AppendLine(String.format("%1$s param__elem;", CadpType.DumpType(thelist.innerType())));
|
|
793
|
|
|
794
|
final CadpActionInfo actionInfo = new CadpActionInfo(m_procInfo.action, -1, 0, m_procInfo.toDoListString, m_procInfo.doneListString, "oldState");
|
|
795
|
|
|
796
|
final CadpExpression initvizcode = new CadpExpression(actionInfo, emittedVariabes);
|
|
797
|
initializer.Accept(initvizcode);
|
|
798
|
helper.AppendLine(initvizcode.VariableDeclarations());
|
|
799
|
helper.AppendLine(String.format("param__result = %1$s;", initvizcode.toString()));
|
|
800
|
|
|
801
|
final CadpExpression listgettercode = new CadpExpression(actionInfo, emittedVariabes);
|
|
802
|
listgetter.Accept(listgettercode);
|
|
803
|
helper.AppendLine(listgettercode.VariableDeclarations());
|
|
804
|
helper.AppendLine(String.format("__thelist = %1$s;", listgettercode.toString()));
|
|
805
|
|
|
806
|
final CadpExpression filtercall = new CadpExpression(actionInfo, emittedVariabes);
|
|
807
|
leftcall.Accept(filtercall);
|
|
808
|
helper.AppendLine(filtercall.VariableDeclarations());
|
|
809
|
|
|
810
|
if (ternaryOperator.kind() == ExpressionKind.foldLR)
|
|
811
|
helper.AppendLine(String.format("for (__iterator = 0; __iterator < __thelist.length; __iterator++) {"));
|
|
812
|
else
|
|
813
|
helper.AppendLine(String.format("for (__iterator = __thelist.length - 1; __iterator >= 0; __iterator--) {"));
|
|
814
|
|
|
815
|
helper.AppendLine(String.format("param__elem = __thelist.elements[__iterator];"));
|
|
816
|
helper.AppendLine(String.format("param__result = %1$s;", filtercall.toString()));
|
|
817
|
|
|
818
|
|
|
819
|
helper.AppendLine("}");
|
|
820
|
helper.AppendLine("return param__result;}");
|
|
821
|
m_helperCode.Append(helper.toString());
|
|
822
|
}
|
|
823
|
else
|
|
824
|
throw new UnsupportedOperationException();
|
|
825
|
}
|
|
826
|
|
|
827
|
@Override
|
|
828
|
public void visit(TupleMapAccessExpression tupleMapAccessExpression)
|
|
829
|
{
|
|
830
|
VisitSub(tupleMapAccessExpression.child(), tupleMapAccessExpression);
|
|
831
|
if (tupleMapAccessExpression.child().type().kind() == TypeKind.TupleType)
|
|
832
|
{
|
|
833
|
|
|
834
|
@SuppressWarnings("unchecked")
|
|
835
|
final ValueExpression<Integer> accessValue = (ValueExpression<Integer>)tupleMapAccessExpression.argument();
|
|
836
|
m_emitter.Append(String.format(".elem_%1$s", accessValue.value()));
|
|
837
|
}
|
|
838
|
else if (tupleMapAccessExpression.child().type().kind() == TypeKind.ListType)
|
|
839
|
{
|
|
840
|
m_emitter.Append(".elements[");
|
|
841
|
VisitSub(tupleMapAccessExpression.argument(), tupleMapAccessExpression);
|
|
842
|
m_emitter.Append("]");
|
|
843
|
}
|
|
844
|
else
|
|
845
|
throw new UnsupportedOperationException();
|
|
846
|
}
|
|
847
|
@Override
|
|
848
|
public void visit(CallExpression callExpression)
|
|
849
|
{
|
|
850
|
|
|
851
|
|
|
852
|
|
|
853
|
|
|
854
|
|
|
855
|
final FunctionType funtype = (FunctionType)callExpression.child().type();
|
|
856
|
if (funtype.returnType() == null)
|
|
857
|
throw new IllegalArgumentException("Internal error: Function call in expression with return-type void!");
|
|
858
|
|
|
859
|
|
|
860
|
final String tmpresult = String.format("detcallresult_%1$s", OoaCADPVisitor.getUIntHashCode(callExpression));
|
|
861
|
final String tmpaftercallstates = String.format("callresult_%1$s", OoaCADPVisitor.getUIntHashCode(callExpression));
|
|
862
|
|
|
863
|
varDecl.AppendLine(String.format("%1$s %2$s;", CadpType.DumpType(funtype.returnType()), tmpresult));
|
|
864
|
varDecl.AppendLine(String.format("struct STATE_LIST * %1$s;", tmpaftercallstates));
|
|
865
|
|
|
866
|
final CadpExpression cadpexpr = new CadpExpression(m_procInfo, emittedVariabes);
|
|
867
|
callExpression.child().Accept(cadpexpr);
|
|
868
|
final String callstatement = cadpexpr.toString();
|
|
869
|
varDecl.Append(cadpexpr.VariableDeclarations());
|
|
870
|
m_usedIdentifier.addAll(cadpexpr.usedIdentifiers());
|
|
871
|
final StringBuilder parameter = new StringBuilder(m_procInfo.stateVariableString);
|
|
872
|
for (final Expression arg : callExpression.arguments())
|
|
873
|
{
|
|
874
|
parameter.append(", ");
|
|
875
|
final CadpExpression paramexpr = new CadpExpression(m_procInfo, emittedVariabes);
|
|
876
|
arg.Accept(paramexpr);
|
|
877
|
parameter.append(paramexpr.toString());
|
|
878
|
}
|
|
879
|
parameter.append(String.format(", &(%1$s)", tmpresult));
|
|
880
|
|
|
881
|
m_emitter.Append("(");
|
|
882
|
m_emitter.Append(String.format("%3$s = %1$s(%2$s)", callstatement, parameter, tmpaftercallstates));
|
|
883
|
m_emitter.Append(",");
|
|
884
|
m_emitter.Append(String.format(" CALC_INVALID = %1$s == NULL ? (fprintf(stderr,\"call to %2$s returns NULL!\\n\"), 1) : (%1$s->next == NULL ? CALC_INVALID : (fprintf(stderr,\"call to %2$s non-deterministic!\\n\"), 1))", tmpaftercallstates, callstatement.replaceAll("\"", "'")));
|
|
885
|
if (!funtype.isPureFunction())
|
|
886
|
{
|
|
887
|
m_emitter.Append(",");
|
|
888
|
m_emitter.Append(String.format(" elem = %1$s == NULL ? elem : (list_insert_list(%2$s, %1$s),%1$s)", tmpaftercallstates, m_procInfo.doneListString));
|
|
889
|
}
|
|
890
|
m_emitter.Append(",");
|
|
891
|
m_emitter.Append(String.format("%1$s", tmpresult));
|
|
892
|
m_emitter.Append(")");
|
|
893
|
}
|
|
894
|
|
|
895
|
|
|
896
|
private interface IFilter<T> {
|
|
897
|
boolean apply (T input);
|
|
898
|
}
|
|
899
|
|
|
900
|
private static <T> void removeAll(List<T> list, IFilter<T> filter) {
|
|
901
|
int max;
|
|
902
|
for (max = list.size() - 1; max >= 0; max --) {
|
|
903
|
if (filter.apply(list.get(max)))
|
|
904
|
list.remove(max);
|
|
905
|
}
|
|
906
|
}
|
|
907
|
|
|
908
|
private List<Identifier> getListOfAccessedIdentifiers(CadpExpression child, final SymbolTable currentScopeSymbols)
|
|
909
|
{
|
|
910
|
final List<Identifier> importVars = new ArrayList<Identifier>(child.usedIdentifiers());
|
|
911
|
if (currentScopeSymbols != null)
|
|
912
|
removeAll(importVars, new IFilter<Identifier>(){
|
|
913
|
@Override
|
|
914
|
public boolean apply(Identifier input) {
|
|
915
|
return currentScopeSymbols.symbolList().contains(input);
|
|
916
|
}});
|
|
917
|
|
|
918
|
removeAll(importVars, new IFilter<Identifier>(){
|
|
919
|
@Override
|
|
920
|
public boolean apply(Identifier input) {
|
|
921
|
return input.kind() == IdentifierKind.AttributeIdentifier ||
|
|
922
|
input.kind() == IdentifierKind.EnumIdentifier ||
|
|
923
|
input.kind() == IdentifierKind.MethodIdentifier ||
|
|
924
|
input.kind() == IdentifierKind.NamedActionIdentifier;
|
|
925
|
}
|
|
926
|
});
|
|
927
|
return importVars;
|
|
928
|
}
|
|
929
|
|
|
930
|
|
|
931
|
@Override
|
|
932
|
public void visit(ForallQuantifier quantifier)
|
|
933
|
{
|
|
934
|
final CadpActionInfo info = new CadpActionInfo(null, -1, -1, m_procInfo.toDoListString, m_procInfo.doneListString, "oldstate");
|
|
935
|
final CadpExpression compExpr = new CadpExpression(info, emittedVariabes);
|
|
936
|
quantifier.child().Accept(compExpr);
|
|
937
|
|
|
938
|
|
|
939
|
final List<Identifier> importVars = getListOfAccessedIdentifiers(compExpr, quantifier.symbols());
|
|
940
|
|
|
941
|
final String functionName = String.format("forall_%1$s", OoaCADPVisitor.getUIntHashCode(quantifier));
|
|
942
|
m_emitter.Append(String.format("1 == %1$s", functionName));
|
|
943
|
m_emitter.Append(String.format("( %1$s", this.m_procInfo.stateVariableString));
|
|
944
|
for (final Identifier x : importVars)
|
|
945
|
{
|
|
946
|
m_emitter.Append(",");
|
|
947
|
m_emitter.Append(String.format("%1$s", CadpIdentifier.GetIdentifierString(x)));
|
|
948
|
}
|
|
949
|
m_emitter.Append(")");
|
|
950
|
|
|
951
|
|
|
952
|
final OoasCodeEmitter helper = new OoasCodeEmitter();
|
|
953
|
helper.AppendLine(String.format("int %1$s(CAESAR_TYPE_STATE %2$s", functionName, "oldstate"));
|
|
954
|
for (final Identifier x : importVars)
|
|
955
|
{
|
|
956
|
helper.Append(", ");
|
|
957
|
helper.Append(String.format("%1$s %2$s", CadpType.DumpType(x.type()), CadpIdentifier.GetIdentifierString(x)));
|
|
958
|
}
|
|
959
|
helper.AppendLine("){");
|
|
960
|
|
|
961
|
helper.AppendLine(compExpr.VariableDeclarations());
|
|
962
|
|
|
963
|
int loops = 0;
|
|
964
|
for (final Identifier enumvar : quantifier.symbols().symbolList())
|
|
965
|
{
|
|
966
|
CadpType.EmitType(enumvar.type());
|
|
967
|
helper.AppendLine(String.format("long long iterator_%1$s;", CadpIdentifier.GetIdentifierString(enumvar)));
|
|
968
|
helper.AppendLine(String.format("for (iterator_%1$s = %2$s; iterator_%1$s <= %3$s; iterator_%1$s++) {",
|
|
969
|
CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetMinVal(enumvar.type()), CadpType.GetMaxVal(enumvar.type())));
|
|
970
|
helper.AppendLine(String.format("/*%1$s*/ %2$s = %3$s(iterator_%2$s);",
|
|
971
|
CadpType.DumpType(enumvar.type()), CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetEnumVal(enumvar.type())));
|
|
972
|
if (enumvar.type().kind() == TypeKind.OoActionSystemType)
|
|
973
|
{
|
|
974
|
|
|
975
|
helper.AppendLine(String.format("if (memcmp(&%1$s, &%2$s, sizeof(%3$s)) == 0) continue;",
|
|
976
|
CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetNullConstant((OoActionSystemType)enumvar.type()), CadpType.DumpType(enumvar.type())));
|
|
977
|
}
|
|
978
|
loops++;
|
|
979
|
}
|
|
980
|
|
|
981
|
helper.AppendLine(String.format("if (!("));
|
|
982
|
helper.AppendLine(compExpr.toString());
|
|
983
|
helper.AppendLine(String.format(") ) return 0;"));
|
|
984
|
|
|
985
|
|
|
986
|
while (loops > 0)
|
|
987
|
{
|
|
988
|
helper.AppendLine("}");
|
|
989
|
loops--;
|
|
990
|
}
|
|
991
|
helper.AppendLine("return 1; }");
|
|
992
|
|
|
993
|
m_helperCode.Append(helper.toString());
|
|
994
|
}
|
|
995
|
|
|
996
|
@Override
|
|
997
|
public void visit(ExistsQuantifier quantifier)
|
|
998
|
{
|
|
999
|
final CadpActionInfo info = new CadpActionInfo(null, -1, -1, m_procInfo.toDoListString, m_procInfo.doneListString, "oldstate");
|
|
1000
|
final CadpExpression compExpr = new CadpExpression(info, emittedVariabes);
|
|
1001
|
quantifier.child().Accept(compExpr);
|
|
1002
|
|
|
1003
|
|
|
1004
|
final List<Identifier> importVars = getListOfAccessedIdentifiers(compExpr, quantifier.symbols());
|
|
1005
|
|
|
1006
|
final String functionName = String.format("exists_%1$s", OoaCADPVisitor.getUIntHashCode(quantifier));
|
|
1007
|
m_emitter.Append(String.format("1 == %1$s", functionName));
|
|
1008
|
m_emitter.Append(String.format("( %1$s", this.m_procInfo.stateVariableString));
|
|
1009
|
for (final Identifier x : importVars)
|
|
1010
|
{
|
|
1011
|
m_emitter.Append(",");
|
|
1012
|
m_emitter.Append(String.format("%1$s", CadpIdentifier.GetIdentifierString(x)));
|
|
1013
|
}
|
|
1014
|
m_emitter.Append(")");
|
|
1015
|
|
|
1016
|
|
|
1017
|
final OoasCodeEmitter helper = new OoasCodeEmitter();
|
|
1018
|
helper.Append(String.format("int %1$s(CAESAR_TYPE_STATE %2$s", functionName, "oldstate"));
|
|
1019
|
for (final Identifier x : importVars)
|
|
1020
|
{
|
|
1021
|
helper.Append(", ");
|
|
1022
|
helper.Append(String.format("%1$s %2$s", CadpType.DumpType(x.type()), CadpIdentifier.GetIdentifierString(x)));
|
|
1023
|
}
|
|
1024
|
helper.AppendLine("){");
|
|
1025
|
|
|
1026
|
helper.AppendLine(compExpr.VariableDeclarations());
|
|
1027
|
|
|
1028
|
int loops = 0;
|
|
1029
|
for (final Identifier enumvar : quantifier.symbols().symbolList())
|
|
1030
|
{
|
|
1031
|
CadpType.EmitType(enumvar.type());
|
|
1032
|
helper.AppendLine(String.format("long long iterator_%1$s;", CadpIdentifier.GetIdentifierString(enumvar)));
|
|
1033
|
helper.AppendLine(String.format("for (iterator_%1$s = %2$s; iterator_%1$s <= %3$s; iterator_%1$s++) {",
|
|
1034
|
CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetMinVal(enumvar.type()), CadpType.GetMaxVal(enumvar.type())));
|
|
1035
|
helper.AppendLine(String.format("/*%1$s*/ %2$s = %3$s(iterator_%2$s);",
|
|
1036
|
CadpType.DumpType(enumvar.type()), CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetEnumVal(enumvar.type())));
|
|
1037
|
if (enumvar.type().kind() == TypeKind.OoActionSystemType)
|
|
1038
|
{
|
|
1039
|
|
|
1040
|
helper.AppendLine(String.format("if (memcmp(&%1$s, &%2$s, sizeof(%3$s)) == 0) continue;",
|
|
1041
|
CadpIdentifier.GetIdentifierString(enumvar), CadpType.GetNullConstant((OoActionSystemType)enumvar.type()), CadpType.DumpType(enumvar.type())));
|
|
1042
|
}
|
|
1043
|
loops++;
|
|
1044
|
}
|
|
1045
|
|
|
1046
|
helper.AppendLine(String.format("if (("));
|
|
1047
|
helper.AppendLine(compExpr.toString());
|
|
1048
|
helper.AppendLine(String.format(") ) return 1;"));
|
|
1049
|
|
|
1050
|
|
|
1051
|
while (loops > 0)
|
|
1052
|
{
|
|
1053
|
helper.AppendLine("}");
|
|
1054
|
loops--;
|
|
1055
|
}
|
|
1056
|
helper.AppendLine("return 0; }");
|
|
1057
|
|
|
1058
|
m_helperCode.Append(helper.toString());
|
|
1059
|
}
|
|
1060
|
|
|
1061
|
private static final class RefBool {
|
|
1062
|
boolean value = false;
|
|
1063
|
}
|
|
1064
|
|
|
1065
|
@Override
|
|
1066
|
public void visit(UnaryOperator unaryOperator)
|
|
1067
|
{
|
|
1068
|
switch (unaryOperator.kind())
|
|
1069
|
{
|
|
1070
|
case tail:
|
|
1071
|
final String tail = EmitTailOperation(unaryOperator);
|
|
1072
|
m_emitter.Append(String.format("%1$s(", tail));
|
|
1073
|
VisitSub(unaryOperator.child(), unaryOperator);
|
|
1074
|
m_emitter.Append(")");
|
|
1075
|
break;
|
|
1076
|
case head:
|
|
1077
|
m_emitter.Append("(");
|
|
1078
|
VisitSub(unaryOperator.child(), unaryOperator);
|
|
1079
|
m_emitter.Append(String.format(").elements[0]"));
|
|
1080
|
break;
|
|
1081
|
case len:
|
|
1082
|
m_emitter.Append("(");
|
|
1083
|
VisitSub(unaryOperator.child(), unaryOperator);
|
|
1084
|
m_emitter.Append(String.format(").length"));
|
|
1085
|
break;
|
|
1086
|
case Cast:
|
|
1087
|
m_emitter.Append("/*cast*/");
|
|
1088
|
final RefBool doSub = new RefBool();
|
|
1089
|
final String cast = EmitCastOperation(unaryOperator, doSub);
|
|
1090
|
if (doSub.value)
|
|
1091
|
{
|
|
1092
|
m_emitter.Append(String.format("(%1$s(", cast));
|
|
1093
|
VisitSub(unaryOperator.child(), unaryOperator);
|
|
1094
|
m_emitter.Append("))");
|
|
1095
|
}
|
|
1096
|
break;
|
|
1097
|
default:
|
|
1098
|
m_emitter.Append(" ");
|
|
1099
|
m_emitter.Append(OperatorString(unaryOperator));
|
|
1100
|
m_emitter.Append("(");
|
|
1101
|
VisitSub(unaryOperator.child(), unaryOperator);
|
|
1102
|
m_emitter.Append(")");
|
|
1103
|
break;
|
|
1104
|
}
|
|
1105
|
}
|
|
1106
|
|
|
1107
|
|
|
1108
|
|
|
1109
|
|
|
1110
|
private boolean CADPCastEquivalent(UlyssesType type1, UlyssesType type2)
|
|
1111
|
{
|
|
1112
|
if ((type1 == null) || (type2 == null))
|
|
1113
|
return false;
|
|
1114
|
|
|
1115
|
final TypeKind tk1 = type1.kind();
|
|
1116
|
final TypeKind tk2 = type2.kind();
|
|
1117
|
|
|
1118
|
|
|
1119
|
if (tk1 != tk2)
|
|
1120
|
return false;
|
|
1121
|
|
|
1122
|
|
|
1123
|
switch (tk1)
|
|
1124
|
{
|
|
1125
|
case IntType:
|
|
1126
|
return true;
|
|
1127
|
case BoolType:
|
|
1128
|
return true;
|
|
1129
|
case FloatType:
|
|
1130
|
throw new UnsupportedOperationException();
|
|
1131
|
case EnumeratedType:
|
|
1132
|
return type1 == type2;
|
|
1133
|
case ListType:
|
|
1134
|
final ListType listt1 = (ListType)type1;
|
|
1135
|
final ListType listt2 = (ListType)type2;
|
|
1136
|
return CADPCastEquivalent(listt1.innerType(), listt2.innerType()) &&
|
|
1137
|
listt1.maxNumberOfElements() == listt2.maxNumberOfElements();
|
|
1138
|
case MapType:
|
|
1139
|
final MapType mapt1 = (MapType)type1;
|
|
1140
|
final MapType mapt2 = (MapType)type2;
|
|
1141
|
return CADPCastEquivalent(mapt1.fromType(), mapt2.fromType()) &&
|
|
1142
|
CADPCastEquivalent(mapt1.toType(), mapt2.toType()) &&
|
|
1143
|
mapt1.maxNumberOfElements() == mapt2.maxNumberOfElements();
|
|
1144
|
case QrType:
|
|
1145
|
final QrType qr1 = (QrType)type1;
|
|
1146
|
final QrType qr2 = (QrType)type2;
|
|
1147
|
return qr1 == qr2;
|
|
1148
|
case TupleType:
|
|
1149
|
final TupleType tuplet1 = (TupleType)type1;
|
|
1150
|
final TupleType tuplet2 = (TupleType)type2;
|
|
1151
|
if (tuplet1.innerTypes().size() != tuplet2.innerTypes().size())
|
|
1152
|
return false;
|
|
1153
|
final Iterator<UlyssesType> innert1 = tuplet1.innerTypes().iterator();
|
|
1154
|
final Iterator<UlyssesType> innert2 = tuplet2.innerTypes().iterator();
|
|
1155
|
while (innert1.hasNext())
|
|
1156
|
{
|
|
1157
|
final UlyssesType innert1Value = innert1.next();
|
|
1158
|
final UlyssesType innert2Value = innert2.next();
|
|
1159
|
|
|
1160
|
if (!CADPCastEquivalent(innert1Value, innert2Value))
|
|
1161
|
return false;
|
|
1162
|
}
|
|
1163
|
return true;
|
|
1164
|
case OoActionSystemType:
|
|
1165
|
return type1 == type2 ||
|
|
1166
|
UlyssesType.Covariance((OoActionSystemType)type2, (OoActionSystemType)type1);
|
|
1167
|
case OpaqueType:
|
|
1168
|
throw new IllegalArgumentException();
|
|
1169
|
case Null:
|
|
1170
|
case Any:
|
|
1171
|
return true;
|
|
1172
|
default:
|
|
1173
|
throw new UnsupportedOperationException();
|
|
1174
|
}
|
|
1175
|
}
|
|
1176
|
|
|
1177
|
|
|
1178
|
private String EmitCastOperation(UnaryOperator unaryOperator, RefBool doSub)
|
|
1179
|
{
|
|
1180
|
doSub.value = true;
|
|
1181
|
if (unaryOperator.child().kind() == ExpressionKind.ListConstr &&
|
|
1182
|
((ListConstructor)unaryOperator.child()).hasComprehension())
|
|
1183
|
{
|
|
1184
|
|
|
1185
|
final String childTypeName = CadpIdentifier.GetIdentifierString(unaryOperator.child().type().identifier());
|
|
1186
|
final String resultTypeName = CadpIdentifier.GetIdentifierString(unaryOperator.type().identifier());
|
|
1187
|
final String result = String.format("op_cast_malloc_%1$s_%2$s", childTypeName, resultTypeName);
|
|
1188
|
|
|
1189
|
if (emittedOperations.contains(result))
|
|
1190
|
return result;
|
|
1191
|
|
|
1192
|
|
|
1193
|
CadpType.EmitType(unaryOperator.type());
|
|
1194
|
|
|
1195
|
switch (unaryOperator.type().kind())
|
|
1196
|
{
|
|
1197
|
case ListType:
|
|
1198
|
final ListType toType = (ListType)unaryOperator.type();
|
|
1199
|
final ListType fromType = (ListType)unaryOperator.child().type();
|
|
1200
|
final String listStruct = String.format("struct struct_list_%1$s", CadpType.DumpType(fromType.innerType()).replaceAll(" ", "_"));
|
|
1201
|
|
|
1202
|
if (!(fromType.innerType().kind() == TypeKind.Null || CADPCastEquivalent(fromType.innerType(), toType.innerType())))
|
|
1203
|
throw new UnsupportedOperationException(String.format("CADP Target does not support this type of cast: '%1$s' to '%2$s'", fromType.innerType().toString(), toType.innerType().toString()));
|
|
1204
|
m_helperCode.AppendLine(String.format("%3$s %2$s(%1$s *toCast){", listStruct, result, resultTypeName));
|
|
1205
|
m_helperCode.AppendLine(String.format("%1$s result;", resultTypeName));
|
|
1206
|
m_helperCode.AppendLine(String.format("%1$s *tmp = toCast;", listStruct));
|
|
1207
|
m_helperCode.AppendLine(String.format("int len = 0;"));
|
|
1208
|
m_helperCode.AppendLine(String.format("result.length = 0;"));
|
|
1209
|
|
|
1210
|
m_helperCode.AppendLine("while (toCast != NULL)");
|
|
1211
|
m_helperCode.AppendLine("{");
|
|
1212
|
m_helperCode.AppendLine(String.format(" if (len < %1$s)", toType.maxNumberOfElements()));
|
|
1213
|
m_helperCode.AppendLine(" {");
|
|
1214
|
m_helperCode.AppendLine(String.format("memcpy(&result.elements[len],&(toCast->element),sizeof(%1$s));", CadpType.DumpType(toType.innerType())));
|
|
1215
|
m_helperCode.AppendLine(String.format("result.length = len+1;"));
|
|
1216
|
m_helperCode.AppendLine(" }");
|
|
1217
|
m_helperCode.AppendLine(" else ");
|
|
1218
|
m_helperCode.AppendLine(" CALC_INVALID = 1;");
|
|
1219
|
m_helperCode.AppendLine(" len++;");
|
|
1220
|
m_helperCode.AppendLine(" tmp = toCast->next;");
|
|
1221
|
m_helperCode.AppendLine(" free(toCast);");
|
|
1222
|
m_helperCode.AppendLine(" toCast = tmp;");
|
|
1223
|
m_helperCode.AppendLine("}");
|
|
1224
|
m_helperCode.AppendLine(" if (CALC_INVALID == 1)");
|
|
1225
|
m_helperCode.AppendLine(String.format(" printf(\"\\n\\nCalculation invalid: Cast to smaller list in %1$s\\n\\n\");", result));
|
|
1226
|
|
|
1227
|
|
|
1228
|
m_helperCode.AppendLine(String.format("int counter;"));
|
|
1229
|
m_helperCode.AppendLine(String.format("for (counter = %1$s; counter >= result.length; counter--) {", toType.maxNumberOfElements() - 1));
|
|
1230
|
m_helperCode.AppendLine(String.format("result.elements[counter] = %1$s%2$s(%3$s%2$s());}",
|
|
1231
|
CadpType.enumString, CadpIdentifier.GetIdentifierString(toType.innerType().identifier()), CadpType.lowString));
|
|
1232
|
m_helperCode.AppendLine("return result; }");
|
|
1233
|
|
|
1234
|
|
|
1235
|
break;
|
|
1236
|
default:
|
|
1237
|
|
|
1238
|
return "";
|
|
1239
|
}
|
|
1240
|
emittedOperations.add(result);
|
|
1241
|
return result;
|
|
1242
|
|
|
1243
|
|
|
1244
|
}
|
|
1245
|
else
|
|
1246
|
{
|
|
1247
|
final String childTypeName = CadpIdentifier.GetIdentifierString(unaryOperator.child().type().identifier());
|
|
1248
|
final String resultTypeName = CadpIdentifier.GetIdentifierString(unaryOperator.type().identifier());
|
|
1249
|
final String result = String.format("op_cast_%1$s_%2$s", childTypeName, resultTypeName);
|
|
1250
|
|
|
1251
|
if (emittedOperations.contains(result))
|
|
1252
|
return result;
|
|
1253
|
|
|
1254
|
|
|
1255
|
CadpType.EmitType(unaryOperator.type());
|
|
1256
|
|
|
1257
|
switch (unaryOperator.type().kind())
|
|
1258
|
{
|
|
1259
|
case ListType:
|
|
1260
|
final ListType toType = (ListType)unaryOperator.type();
|
|
1261
|
final ListType fromType = (ListType)unaryOperator.child().type();
|
|
1262
|
if (!(fromType.innerType().kind() == TypeKind.Null || CADPCastEquivalent(fromType.innerType(), toType.innerType())))
|
|
1263
|
throw new UnsupportedOperationException(String.format("CADP Target does not support this type of cast: '%1$s' to '%2$s'", fromType.innerType().toString(), toType.innerType().toString()));
|
|
1264
|
m_helperCode.AppendLine(String.format("%3$s %2$s(%1$s toCast){", childTypeName, result, resultTypeName));
|
|
1265
|
m_helperCode.AppendLine(String.format("%1$s result;", resultTypeName));
|
|
1266
|
m_helperCode.AppendLine(String.format("if (toCast.length > %1$s) { printf(\"Cast to smaller list! %2$s\\n\"); ", toType.maxNumberOfElements(), result));
|
|
1267
|
m_helperCode.AppendLine(String.format("%1$s%2$s(stdout, toCast); fflush(stdout); CALC_INVALID=1; result.length = %3$s;} else", CadpType.printString, childTypeName, toType.maxNumberOfElements()));
|
|
1268
|
m_helperCode.AppendLine(String.format("result.length = toCast.length;"));
|
|
1269
|
m_helperCode.AppendLine(String.format("if (result.length > 0)"));
|
|
1270
|
m_helperCode.AppendLine(String.format("memcpy(result.elements,toCast.elements,result.length * sizeof(%1$s));", CadpType.DumpType(toType.innerType())));
|
|
1271
|
m_helperCode.AppendLine(String.format("int counter;"));
|
|
1272
|
m_helperCode.AppendLine(String.format("for (counter = %1$s; counter >= result.length; counter--) {", toType.maxNumberOfElements() - 1));
|
|
1273
|
m_helperCode.AppendLine(String.format("result.elements[counter] = %1$s%2$s(%3$s%2$s());}",
|
|
1274
|
CadpType.enumString, CadpIdentifier.GetIdentifierString(toType.innerType().identifier()), CadpType.lowString));
|
|
1275
|
m_helperCode.AppendLine("return result; }");
|
|
1276
|
|
|
1277
|
|
|
1278
|
break;
|
|
1279
|
case OoActionSystemType:
|
|
1280
|
if (unaryOperator.child().kind() == ExpressionKind.Value &&
|
|
1281
|
(unaryOperator.child() instanceof ValueExpression<?>) &&
|
|
1282
|
((ValueExpression<?>)unaryOperator.child()).value() == null)
|
|
1283
|
{
|
|
1284
|
m_emitter.Append(String.format("NULL_%1$s", CadpIdentifier.GetIdentifierString(unaryOperator.type().identifier())));
|
|
1285
|
doSub.value = false;
|
|
1286
|
}
|
|
1287
|
else
|
|
1288
|
{
|
|
1289
|
doSub.value = true;
|
|
1290
|
final CadpType targetType = new CadpType();
|
|
1291
|
unaryOperator.type().Accept(targetType);
|
|
1292
|
final CadpType sourceType = new CadpType();
|
|
1293
|
unaryOperator.child().type().Accept(sourceType);
|
|
1294
|
if (!(UlyssesType.Covariance((OoActionSystemType)unaryOperator.child().type(), (OoActionSystemType)unaryOperator.type())))
|
|
1295
|
{
|
|
1296
|
|
|
1297
|
return String.format("/* up-cast: %1$s as %2$s */ *(%2$s*)&", sourceType.ToString(), targetType.ToString());
|
|
1298
|
}
|
|
1299
|
else
|
|
1300
|
{
|
|
1301
|
return String.format(" /* down-cast: %1$s as %2$s */ *(%2$s*)&", sourceType.ToString(), targetType.ToString());
|
|
1302
|
}
|
|
1303
|
|
|
1304
|
}
|
|
1305
|
return "";
|
|
1306
|
default:
|
|
1307
|
|
|
1308
|
return "";
|
|
1309
|
}
|
|
1310
|
emittedOperations.add(result);
|
|
1311
|
return result;
|
|
1312
|
}
|
|
1313
|
}
|
|
1314
|
|
|
1315
|
private String EmitTailOperation(UnaryOperator unaryOperator)
|
|
1316
|
{
|
|
1317
|
final String childTypeName = CadpIdentifier.GetIdentifierString(unaryOperator.child().type().identifier());
|
|
1318
|
final String result = String.format("op_tail_%1$s", childTypeName);
|
|
1319
|
if (emittedOperations.contains(result))
|
|
1320
|
return result;
|
|
1321
|
|
|
1322
|
final ListType alist = (ListType)unaryOperator.child().type();
|
|
1323
|
CadpType.EmitType(unaryOperator.type());
|
|
1324
|
final String resultType = CadpIdentifier.GetIdentifierString(unaryOperator.type().identifier());
|
|
1325
|
final ListType resultList = (ListType)unaryOperator.type();
|
|
1326
|
|
|
1327
|
|
|
1328
|
m_helperCode.AppendLine(String.format("%3$s %2$s(%1$s toCopy){", childTypeName, result, resultType));
|
|
1329
|
m_helperCode.AppendLine(String.format("%1$s result;", resultType));
|
|
1330
|
m_helperCode.AppendLine(String.format("if (toCopy.length == 0) { printf(\"Tail from empty list! %1$s\\n\"); abort();}", childTypeName));
|
|
1331
|
m_helperCode.AppendLine(String.format("result.length = toCopy.length - 1;"));
|
|
1332
|
m_helperCode.AppendLine(String.format("if (result.length == 0)"));
|
|
1333
|
m_helperCode.AppendLine(String.format("memset(&result,0,sizeof(%1$s));", resultType));
|
|
1334
|
m_helperCode.AppendLine(String.format("else"));
|
|
1335
|
m_helperCode.AppendLine(String.format("memcpy(&result.elements[0],&toCopy.elements[1],result.length * sizeof(%1$s));", CadpType.DumpType(alist.innerType()), alist.maxNumberOfElements() - 1));
|
|
1336
|
|
|
1337
|
|
|
1338
|
m_helperCode.AppendLine(String.format("int counter;"));
|
|
1339
|
m_helperCode.AppendLine(String.format("for (counter = %1$s; counter >= result.length; counter--) {", resultList.maxNumberOfElements() - 1));
|
|
1340
|
m_helperCode.AppendLine(String.format("result.elements[counter] = %1$s%2$s(%3$s%2$s());}",
|
|
1341
|
CadpType.enumString, CadpIdentifier.GetIdentifierString(alist.innerType().identifier()), CadpType.lowString));
|
|
1342
|
|
|
1343
|
|
|
1344
|
m_helperCode.AppendLine("return result; }");
|
|
1345
|
|
|
1346
|
|
|
1347
|
emittedOperations.add(result);
|
|
1348
|
return result;
|
|
1349
|
}
|
|
1350
|
|
|
1351
|
public String VariableDeclarations()
|
|
1352
|
{
|
|
1353
|
return varDecl.toString();
|
|
1354
|
}
|
|
1355
|
|
|
1356
|
@Override
|
|
1357
|
public String toString()
|
|
1358
|
{
|
|
1359
|
return m_emitter.toString();
|
|
1360
|
}
|
|
1361
|
|
|
1362
|
public static String GetHelperCode()
|
|
1363
|
{
|
|
1364
|
final StringBuilder result = new StringBuilder(m_helperCode.toString());
|
|
1365
|
result.append("void Model_Reset() {");
|
|
1366
|
result.append(System.lineSeparator());
|
|
1367
|
result.append(m_resetCode.toString());
|
|
1368
|
result.append("}");
|
|
1369
|
result.append(System.lineSeparator());
|
|
1370
|
return result.toString();
|
|
1371
|
}
|
|
1372
|
|
|
1373
|
public CadpExpression(CadpActionInfo aProcInfo)
|
|
1374
|
{
|
|
1375
|
if (aProcInfo == null)
|
|
1376
|
throw new IllegalArgumentException();
|
|
1377
|
m_procInfo = aProcInfo;
|
|
1378
|
}
|
|
1379
|
|
|
1380
|
|
|
1381
|
public CadpExpression(CadpActionInfo aProcInfo, HashSet<Identifier> varDecls)
|
|
1382
|
{
|
|
1383
|
if (aProcInfo == null)
|
|
1384
|
throw new IllegalArgumentException();
|
|
1385
|
m_procInfo = aProcInfo;
|
|
1386
|
emittedVariabes.addAll(varDecls);
|
|
1387
|
}
|
|
1388
|
}
|