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.visitors;
|
29
|
|
30
|
import java.util.ArrayList;
|
31
|
import java.util.ListIterator;
|
32
|
|
33
|
import org.momut.ooas.ast.AstNodeTypeEnum;
|
34
|
import org.momut.ooas.ast.IAst;
|
35
|
import org.momut.ooas.ast.expressions.AccessExpression;
|
36
|
import org.momut.ooas.ast.expressions.Expression;
|
37
|
import org.momut.ooas.ast.expressions.ExpressionKind;
|
38
|
import org.momut.ooas.ast.expressions.IdentifierExpression;
|
39
|
import org.momut.ooas.ast.expressions.TupleMapAccessExpression;
|
40
|
import org.momut.ooas.ast.expressions.UnaryOperator;
|
41
|
import org.momut.ooas.ast.identifiers.AttributeIdentifier;
|
42
|
import org.momut.ooas.ast.identifiers.ExpressionVariableIdentifier;
|
43
|
import org.momut.ooas.ast.identifiers.FunctionIdentifier;
|
44
|
import org.momut.ooas.ast.identifiers.Identifier;
|
45
|
import org.momut.ooas.ast.identifiers.IdentifierKind;
|
46
|
import org.momut.ooas.ast.statements.Assignment;
|
47
|
import org.momut.ooas.ast.statements.Call;
|
48
|
import org.momut.ooas.ast.statements.GuardedCommand;
|
49
|
import org.momut.ooas.ast.statements.KillStatement;
|
50
|
import org.momut.ooas.ast.statements.Statement;
|
51
|
import org.momut.ooas.ast.types.FunctionType;
|
52
|
import org.momut.ooas.ast.types.ListType;
|
53
|
import org.momut.ooas.ast.types.TypeKind;
|
54
|
import org.momut.ooas.ast.types.Type;
|
55
|
import org.momut.ooas.parser.ParserError;
|
56
|
import org.momut.ooas.parser.ParserState;
|
57
|
import org.momut.ooas.parser.ParserWarning;
|
58
|
import org.momut.ooas.parser.SymbolTable;
|
59
|
import org.momut.ooas.utils.exceptions.ArgumentException;
|
60
|
import org.momut.ooas.utils.exceptions.NotImplementedException;
|
61
|
import org.momut.ooas.utils.exceptions.OoasCompilerRuntimeException;
|
62
|
|
63
|
|
64
|
|
65
|
|
66
|
|
67
|
|
68
|
|
69
|
public final class OoaTypeCheckVisitor extends OoaCompleteAstTraversalVisitor
|
70
|
{
|
71
|
|
72
|
|
73
|
|
74
|
|
75
|
private static final class OoaInitializerCheck extends OoaExpressionVisitor
|
76
|
{
|
77
|
ArrayList<Identifier> attributeAccess = new ArrayList<Identifier>();
|
78
|
|
79
|
@Override
|
80
|
public void visit(IdentifierExpression identifierExpression)
|
81
|
{
|
82
|
final Identifier id = identifierExpression.identifier();
|
83
|
if (id.kind() == IdentifierKind.AttributeIdentifier)
|
84
|
attributeAccess.add(id);
|
85
|
super.visit(identifierExpression);
|
86
|
}
|
87
|
|
88
|
}
|
89
|
|
90
|
|
91
|
|
92
|
|
93
|
private void Error(Statement statement, String p)
|
94
|
{
|
95
|
final ParserError error = new ParserError(m_ParserState.filename,
|
96
|
statement.line(), statement.pos(), p);
|
97
|
m_ParserState.AddErrorMessage(error);
|
98
|
}
|
99
|
private void Error(Identifier id, String p)
|
100
|
{
|
101
|
final ParserError error = new ParserError(m_ParserState.filename,
|
102
|
id.line(), id.column(), p);
|
103
|
m_ParserState.AddErrorMessage(error);
|
104
|
}
|
105
|
|
106
|
|
107
|
|
108
|
private void Warning(Statement aStatement, String p)
|
109
|
{
|
110
|
final ParserWarning warn = new ParserWarning(m_ParserState.filename,
|
111
|
aStatement.line(), aStatement.pos(), p);
|
112
|
m_ParserState.AddWarningMessage(warn);
|
113
|
}
|
114
|
private void Warning(Identifier aStatement, String p)
|
115
|
{
|
116
|
final ParserWarning warn = new ParserWarning(m_ParserState.filename,
|
117
|
aStatement.line(), aStatement.column(), p);
|
118
|
m_ParserState.AddWarningMessage(warn);
|
119
|
}
|
120
|
|
121
|
|
122
|
|
123
|
private void RemoveWarning(Identifier expression, String p)
|
124
|
{
|
125
|
final ArrayList<ParserWarning> toRemove = new ArrayList<ParserWarning>();
|
126
|
for (final ParserWarning x: m_ParserState.listOfParserWarnings)
|
127
|
{
|
128
|
if (p.equals(x.message()) && x.line() == expression.line() && x.column() == expression.column())
|
129
|
toRemove.add(x);
|
130
|
}
|
131
|
for (final ParserWarning x: toRemove)
|
132
|
m_ParserState.listOfParserWarnings.remove(x);
|
133
|
}
|
134
|
|
135
|
private void TypeCheckGuardedCommand(GuardedCommand gc)
|
136
|
{
|
137
|
if (gc.guard().type() == null ||
|
138
|
gc.guard().type().kind() != TypeKind.BoolType)
|
139
|
Error(gc, "Guard needs to be boolean expression");
|
140
|
|
141
|
final ArrayList<ExpressionVariableIdentifier> uninitfree = gc.guard().GetUninitializedFreeVariables();
|
142
|
if (uninitfree.size() > 0)
|
143
|
Error(gc, String.format("Undefined variable: '%s'", uninitfree.get(0).tokenText()));
|
144
|
|
145
|
CheckMethodCallsArePure(gc.guard());
|
146
|
|
147
|
gc.body().Accept(this);
|
148
|
}
|
149
|
|
150
|
private void CheckMethodCallsArePure(Expression expression)
|
151
|
{
|
152
|
for (final FunctionIdentifier method: expression.callTargets())
|
153
|
{
|
154
|
if (!((FunctionType)method.type()).isPureFunction())
|
155
|
Error(method, String.format("Method '%s' needs to be pure: No change of state allowed.", method.tokenText()));
|
156
|
}
|
157
|
}
|
158
|
|
159
|
|
160
|
private void TypeCheckAssignment(Assignment assignment)
|
161
|
{
|
162
|
SymbolTable freevars = new SymbolTable();
|
163
|
if (assignment.nondetExpression() != null)
|
164
|
{
|
165
|
CheckMethodCallsArePure(assignment.nondetExpression());
|
166
|
|
167
|
if (assignment.nondetExpression().freeVariables() != null
|
168
|
&& assignment.nondetExpression().freeVariables().symbolList().size() > 0)
|
169
|
{
|
170
|
|
171
|
freevars = assignment.nondetExpression().freeVariables();
|
172
|
|
173
|
for (final Expression aRhsExpr: assignment.values())
|
174
|
{
|
175
|
if (aRhsExpr.freeVariables() != null)
|
176
|
for (final Identifier freeRhsVar: aRhsExpr.freeVariables().symbolList())
|
177
|
{
|
178
|
if (freevars.Defined(freeRhsVar.tokenText()))
|
179
|
{
|
180
|
final Identifier exprvar = freevars.Get(freeRhsVar.tokenText());
|
181
|
if (freeRhsVar.type().kind() == TypeKind.Any)
|
182
|
{
|
183
|
freeRhsVar.SetType(exprvar.type());
|
184
|
assignment.AddIdentifier(exprvar, null);
|
185
|
|
186
|
RemoveWarning(exprvar, String.format("Free variable in expression: '%s'.", exprvar.tokenText()));
|
187
|
RemoveWarning(freeRhsVar, String.format("Free variable in expression: '%s'.", exprvar.tokenText()));
|
188
|
}
|
189
|
else if (Type.TypeEqual(freeRhsVar.type(), exprvar.type()))
|
190
|
{
|
191
|
assignment.AddIdentifier(exprvar, null);
|
192
|
|
193
|
RemoveWarning(exprvar, String.format("Free variable in expression: '%s'.", exprvar.tokenText()));
|
194
|
RemoveWarning(freeRhsVar, String.format("Free variable in expression: '%s'.", exprvar.tokenText()));
|
195
|
}
|
196
|
else
|
197
|
Error(assignment, String.format("Type mismatch on variable %s: %s <> %s", freeRhsVar.tokenText(), freeRhsVar.type().toString(), exprvar.type().toString()));
|
198
|
}
|
199
|
else
|
200
|
Error(assignment, String.format("Undefined variable '%s'", freeRhsVar.tokenText()));
|
201
|
}
|
202
|
}
|
203
|
}
|
204
|
}
|
205
|
|
206
|
for (final Identifier avar: freevars.symbolList())
|
207
|
if (!assignment.symbols().Defined(avar.tokenText()))
|
208
|
Error(assignment, String.format("Undefined variable '%s'", avar.tokenText()));
|
209
|
|
210
|
if (assignment.places().size() != assignment.values().size())
|
211
|
{
|
212
|
Error(assignment, "Number of places does not match number of values in assignment.");
|
213
|
|
214
|
}
|
215
|
|
216
|
final ListIterator<Expression> aplaceIt = assignment.places().listIterator();
|
217
|
final ListIterator<Expression> avalueIt = assignment.values().listIterator();
|
218
|
while (aplaceIt.hasNext() && avalueIt.hasNext())
|
219
|
{
|
220
|
final Expression aplace = aplaceIt.next();
|
221
|
Expression avalue = avalueIt.next();
|
222
|
|
223
|
CheckPlace(aplace, assignment);
|
224
|
|
225
|
|
226
|
if (avalue.kind() != ExpressionKind.Call)
|
227
|
CheckMethodCallsArePure(avalue);
|
228
|
|
229
|
final Type acover = Type.CoverType(aplace.type(), avalue.type());
|
230
|
if (acover == null)
|
231
|
Error(assignment, String.format("Type mismatch in assignment: %s ( %s := %s )", aplace.toString(), aplace.type().toString(), avalue.type().toString()));
|
232
|
else if (!Type.TypeEqualByKind(aplace.type(), acover))
|
233
|
Error(assignment, String.format("Type mismatch in assignment: %s ( %s := %s )", aplace.toString(), aplace.type().toString(), acover.toString()));
|
234
|
else
|
235
|
{
|
236
|
final ArrayList<ExpressionVariableIdentifier> uninitvars = avalue.GetUninitializedFreeVariables();
|
237
|
final Expression constantvalue = avalue.kind() == ExpressionKind.Value ? avalue : null;
|
238
|
|
239
|
if (uninitvars.size() > 0)
|
240
|
Error(assignment, String.format("Undefined variable '%s'", uninitvars.get(0).tokenText()));
|
241
|
|
242
|
if (!Type.TypeEqual(avalue.type(), acover))
|
243
|
{
|
244
|
final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, avalue, avalue.line(), avalue.pos());
|
245
|
cast.SetType(acover);
|
246
|
avalueIt.remove();
|
247
|
avalueIt.add(cast);
|
248
|
avalue = avalueIt.previous();
|
249
|
if (avalue != cast)
|
250
|
throw new OoasCompilerRuntimeException();
|
251
|
}
|
252
|
|
253
|
if (Type.FirstTypeLessRange(aplace.type(), acover))
|
254
|
{
|
255
|
if (constantvalue == null)
|
256
|
{
|
257
|
Warning(assignment, String.format("Assignment may over/underflow: %s := %s", aplace.type().toString(), acover.toString()));
|
258
|
final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, avalue, avalue.line(), avalue.pos());
|
259
|
cast.SetType(aplace.type());
|
260
|
avalueIt.remove();
|
261
|
avalueIt.add(cast);
|
262
|
avalue = avalueIt.previous();
|
263
|
if (avalue != cast)
|
264
|
throw new OoasCompilerRuntimeException();
|
265
|
}
|
266
|
else
|
267
|
{
|
268
|
Error(assignment, String.format("Assignment out of range (%s := %s)", aplace.toString(), constantvalue.toString()));
|
269
|
}
|
270
|
}
|
271
|
}
|
272
|
}
|
273
|
}
|
274
|
|
275
|
|
276
|
|
277
|
|
278
|
|
279
|
|
280
|
private void CheckPlace(Expression expression, Assignment assignment)
|
281
|
{
|
282
|
|
283
|
|
284
|
|
285
|
boolean result = true;
|
286
|
|
287
|
|
288
|
if (expression.kind() == ExpressionKind.TupleMapAccess)
|
289
|
{
|
290
|
final TupleMapAccessExpression tAccessExpression = (TupleMapAccessExpression)expression;
|
291
|
expression = tAccessExpression.child();
|
292
|
}
|
293
|
|
294
|
|
295
|
if (expression.kind() == ExpressionKind.Access)
|
296
|
{
|
297
|
final AccessExpression accessExpression = (AccessExpression)expression;
|
298
|
if (accessExpression.left().kind() == ExpressionKind.Identifier && ((IdentifierExpression)accessExpression.left()).isSelf())
|
299
|
expression = accessExpression.right();
|
300
|
else
|
301
|
result = false;
|
302
|
}
|
303
|
|
304
|
|
305
|
if (expression.kind() != ExpressionKind.Identifier)
|
306
|
result = false;
|
307
|
|
308
|
if (!result)
|
309
|
Error(assignment, String.format("LHS of assignment must be variable or attribute."));
|
310
|
}
|
311
|
|
312
|
|
313
|
private void TypeCheck(Statement statement)
|
314
|
{
|
315
|
switch (statement.kind())
|
316
|
{
|
317
|
case Abort:
|
318
|
case Skip:
|
319
|
case Break:
|
320
|
break;
|
321
|
|
322
|
case NondetBlock:
|
323
|
case PrioBlock:
|
324
|
case SeqBlock:
|
325
|
statement.Accept(this);
|
326
|
break;
|
327
|
|
328
|
case Assignment:
|
329
|
final Assignment assignment = (Assignment)statement;
|
330
|
TypeCheckAssignment(assignment);
|
331
|
break;
|
332
|
case GuardedCommand:
|
333
|
final GuardedCommand gc = (GuardedCommand)statement;
|
334
|
TypeCheckGuardedCommand(gc);
|
335
|
break;
|
336
|
case Kill:
|
337
|
final KillStatement kill = (KillStatement)statement;
|
338
|
if (kill.someOne.type().kind() != TypeKind.OoActionSystemType)
|
339
|
Error(kill, String.format(" %s not an object", kill.someOne.tokenText()));
|
340
|
break;
|
341
|
case MethodCall:
|
342
|
final Call callstatement = (Call)statement;
|
343
|
if (callstatement.callExpression().GetUninitializedFreeVariables().size() > 0)
|
344
|
Error(callstatement, "Uninitialized free variables in call expression.");
|
345
|
if (callstatement.callExpression().kind() != ExpressionKind.Call
|
346
|
&& callstatement.callExpression().kind() != ExpressionKind.foldRL
|
347
|
&& callstatement.callExpression().kind() != ExpressionKind.foldLR)
|
348
|
Error(callstatement, "Not a valid method call");
|
349
|
break;
|
350
|
default:
|
351
|
throw new NotImplementedException();
|
352
|
}
|
353
|
}
|
354
|
|
355
|
|
356
|
|
357
|
private void TypeCheck(AttributeIdentifier attributeIdentifier)
|
358
|
{
|
359
|
if (attributeIdentifier.initializer() == null)
|
360
|
throw new ArgumentException();
|
361
|
|
362
|
final Type atype = attributeIdentifier.initializer().type();
|
363
|
if (atype == null)
|
364
|
Error(attributeIdentifier, "Initializer lacks type.");
|
365
|
else
|
366
|
{
|
367
|
|
368
|
|
369
|
|
370
|
final OoaInitializerCheck initCheck = new OoaInitializerCheck();
|
371
|
attributeIdentifier.initializer().Accept(initCheck);
|
372
|
if (initCheck.attributeAccess.size() > 0)
|
373
|
|
374
|
Error(attributeIdentifier, "Access of other attributes not allowed in attribute initializer.");
|
375
|
else if (attributeIdentifier.initializer().callTargets().size() > 0)
|
376
|
|
377
|
Error(attributeIdentifier, "Method calls not allowed in attribute initializer.");
|
378
|
else if (attributeIdentifier.initializer().freeVariables().symbolList().size() > 0)
|
379
|
|
380
|
Error(attributeIdentifier,
|
381
|
String.format("Unknown identifier in initializer: '%s'",
|
382
|
attributeIdentifier.initializer().freeVariables().symbolList().get(0).tokenText()));
|
383
|
else
|
384
|
{
|
385
|
final Type idtype = attributeIdentifier.type();
|
386
|
final Type acover = Type.CoverType(idtype, atype);
|
387
|
|
388
|
if (acover == null)
|
389
|
Error(attributeIdentifier, String.format("Type mismatch in attribute initializer: %s ( %s := %s )", attributeIdentifier.toString(), idtype.toString(), atype.toString()));
|
390
|
else if (!Type.TypeEqualByKind(idtype, acover))
|
391
|
Error(attributeIdentifier, String.format("Type mismatch in attribute initializer: %s ( %s := %s )", attributeIdentifier.toString(), idtype.toString(), acover.toString()));
|
392
|
else
|
393
|
{
|
394
|
if (!Type.TypeEqual(atype, acover))
|
395
|
{
|
396
|
if(acover.kind() == TypeKind.ListType)
|
397
|
{
|
398
|
attributeIdentifier.initializer().Accept(new OoaStaticListCastVisitor((ListType) acover));
|
399
|
|
400
|
|
401
|
((ListType) atype).SetInnerType(((ListType) idtype).innerType());
|
402
|
final Type lengthCover = Type.CoverType(idtype, attributeIdentifier.initializer().type());
|
403
|
if (!Type.TypeEqual(atype, lengthCover)) {
|
404
|
final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, attributeIdentifier.initializer(),
|
405
|
attributeIdentifier.initializer().line(), attributeIdentifier.initializer().pos());
|
406
|
cast.SetType(lengthCover);
|
407
|
attributeIdentifier.SetInitializer(cast);
|
408
|
}
|
409
|
}
|
410
|
else
|
411
|
{
|
412
|
final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, attributeIdentifier.initializer(),
|
413
|
attributeIdentifier.initializer().line(), attributeIdentifier.initializer().pos());
|
414
|
cast.SetType(acover);
|
415
|
attributeIdentifier.SetInitializer(cast);
|
416
|
}
|
417
|
}
|
418
|
|
419
|
if (Type.FirstTypeLessRange(idtype, acover))
|
420
|
{
|
421
|
final Expression constantvalue = attributeIdentifier.initializer().kind() == ExpressionKind.Value ? attributeIdentifier.initializer() : null;
|
422
|
if (constantvalue == null)
|
423
|
{
|
424
|
Warning(attributeIdentifier, String.format("Assignment may over/underflow: %s := %s", idtype.toString(), acover.toString()));
|
425
|
final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, attributeIdentifier.initializer(),
|
426
|
attributeIdentifier.initializer().line(), attributeIdentifier.initializer().pos());
|
427
|
cast.SetType(idtype);
|
428
|
attributeIdentifier.SetInitializer(cast);
|
429
|
}
|
430
|
else
|
431
|
{
|
432
|
Error(attributeIdentifier, String.format("Initialization out of range (%s := %s)", attributeIdentifier.toString(), constantvalue.toString()));
|
433
|
}
|
434
|
}
|
435
|
}
|
436
|
}
|
437
|
}
|
438
|
}
|
439
|
|
440
|
|
441
|
@Override
|
442
|
protected void VisitAstElement(IAst element, IAst parent)
|
443
|
{
|
444
|
if (element.nodeType() == AstNodeTypeEnum.statement)
|
445
|
{
|
446
|
TypeCheck((Statement)element);
|
447
|
}
|
448
|
else if (element.nodeType() == AstNodeTypeEnum.identifier
|
449
|
&& ((Identifier)element).kind() == IdentifierKind.AttributeIdentifier)
|
450
|
{
|
451
|
TypeCheck((AttributeIdentifier)element);
|
452
|
}
|
453
|
else super.VisitAstElement(element, parent);
|
454
|
}
|
455
|
|
456
|
|
457
|
|
458
|
public OoaTypeCheckVisitor(ParserState aState)
|
459
|
{
|
460
|
super (aState);
|
461
|
if (aState == null)
|
462
|
throw new ArgumentException();
|
463
|
}
|
464
|
}
|