|
1
|
/**
|
|
2
|
*
|
|
3
|
* OOAS Compiler (Deprecated)
|
|
4
|
*
|
|
5
|
* Copyright 2015, Institute for Software Technology, Graz University of
|
|
6
|
* Technology. Portions are copyright 2015 by the AIT Austrian Institute
|
|
7
|
* of Technology. All rights reserved.
|
|
8
|
*
|
|
9
|
* SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.
|
|
10
|
*
|
|
11
|
* Please notice that this version of the OOAS compiler is considered de-
|
|
12
|
* precated. Only the Java version is maintained.
|
|
13
|
*
|
|
14
|
* Contributors:
|
|
15
|
* Willibald Krenn (TU Graz/AIT)
|
|
16
|
* Stefan Tiran (TU Graz/AIT)
|
|
17
|
*/
|
|
18
|
|
|
19
|
using System;
|
|
20
|
using System.Collections.Generic;
|
|
21
|
using System.Text;
|
|
22
|
|
|
23
|
namespace TUG.Mogentes
|
|
24
|
{
|
|
25
|
|
|
26
|
/// <summary>
|
|
27
|
/// internal; used to count occurrences of attribute access in an expression
|
|
28
|
/// </summary>
|
|
29
|
internal sealed class OoaInitializerCheck : OoaExpressionVisitor
|
|
30
|
{
|
|
31
|
internal List<Identifier> attributeAccess = new List<Identifier>();
|
|
32
|
|
|
33
|
public override void visit(IdentifierExpression identifierExpression)
|
|
34
|
{
|
|
35
|
Identifier id = identifierExpression.identifier;
|
|
36
|
if (id.kind == IdentifierKind.AttributeIdentifier)
|
|
37
|
attributeAccess.Add(id);
|
|
38
|
base.visit(identifierExpression);
|
|
39
|
}
|
|
40
|
|
|
41
|
internal OoaInitializerCheck()
|
|
42
|
: base()
|
|
43
|
{ }
|
|
44
|
}
|
|
45
|
|
|
46
|
|
|
47
|
/// <summary>
|
|
48
|
/// Requires: ResolveExpressionVisitor and MethodPureClassifierVisitor
|
|
49
|
///
|
|
50
|
/// Does the typechecking of statements and initializers.
|
|
51
|
/// Needs resolved expressions, hence a run of ResolveVisitor first.
|
|
52
|
/// </summary>
|
|
53
|
public sealed class OoaTypeCheckVisitor : OoaCompleteAstTraversalVisitor
|
|
54
|
{
|
|
55
|
private void Error(Statement statement, string p)
|
|
56
|
{
|
|
57
|
ParserError error = new ParserError(m_ParserState.filename,
|
|
58
|
statement.line, statement.pos, p);
|
|
59
|
m_ParserState.AddErrorMessage(error);
|
|
60
|
}
|
|
61
|
private void Error(Identifier id, string p)
|
|
62
|
{
|
|
63
|
ParserError error = new ParserError(m_ParserState.filename,
|
|
64
|
id.line, id.column, p);
|
|
65
|
m_ParserState.AddErrorMessage(error);
|
|
66
|
}
|
|
67
|
|
|
68
|
|
|
69
|
|
|
70
|
private void Warning(Statement aStatement, string p)
|
|
71
|
{
|
|
72
|
ParserWarning warn = new ParserWarning(m_ParserState.filename,
|
|
73
|
aStatement.line, aStatement.pos, p);
|
|
74
|
m_ParserState.AddWarningMessage(warn);
|
|
75
|
}
|
|
76
|
private void Warning(Identifier aStatement, string p)
|
|
77
|
{
|
|
78
|
ParserWarning warn = new ParserWarning(m_ParserState.filename,
|
|
79
|
aStatement.line, aStatement.column, p);
|
|
80
|
m_ParserState.AddWarningMessage(warn);
|
|
81
|
}
|
|
82
|
|
|
83
|
|
|
84
|
|
|
85
|
private void RemoveWarning(Identifier expression, string p)
|
|
86
|
{
|
|
87
|
List<ParserWarning> toRemove = new List<ParserWarning>();
|
|
88
|
foreach (var x in m_ParserState.listOfParserWarnings)
|
|
89
|
{
|
|
90
|
if (p.Equals(x.message) && x.line == expression.line && x.column == expression.column)
|
|
91
|
toRemove.Add(x);
|
|
92
|
}
|
|
93
|
foreach (var x in toRemove)
|
|
94
|
m_ParserState.listOfParserWarnings.Remove(x);
|
|
95
|
}
|
|
96
|
|
|
97
|
private void TypeCheckGuardedCommand(GuardedCommand gc)
|
|
98
|
{
|
|
99
|
if (gc.guard.type == null ||
|
|
100
|
gc.guard.type.kind != TypeKind.BoolType)
|
|
101
|
Error(gc, "Guard needs to be boolean expression");
|
|
102
|
|
|
103
|
List<ExpressionVariableIdentifier> uninitfree = gc.guard.GetUninitializedFreeVariables();
|
|
104
|
if (uninitfree.Count > 0)
|
|
105
|
Error(gc, String.Format("Undefined variable: '{0}'", uninitfree[0].tokenText));
|
|
106
|
|
|
107
|
CheckMethodCallsArePure(gc.guard);
|
|
108
|
|
|
109
|
gc.body.Accept(this);
|
|
110
|
}
|
|
111
|
|
|
112
|
private void CheckMethodCallsArePure(Expression expression)
|
|
113
|
{
|
|
114
|
foreach (var method in expression.callTargets)
|
|
115
|
{
|
|
116
|
if (!((FunctionType)method.type).isPureFunction)
|
|
117
|
Error(method, String.Format("Method '{0}' needs to be pure: No change of state allowed.", method.tokenText));
|
|
118
|
}
|
|
119
|
}
|
|
120
|
|
|
121
|
|
|
122
|
private void TypeCheckAssignment(Assignment assignment)
|
|
123
|
{
|
|
124
|
SymbolTable freevars = new SymbolTable();
|
|
125
|
if (assignment.nondetExpression != null)
|
|
126
|
{
|
|
127
|
CheckMethodCallsArePure(assignment.nondetExpression);
|
|
128
|
|
|
129
|
if (assignment.nondetExpression.freeVariables != null
|
|
130
|
&& assignment.nondetExpression.freeVariables.symbolList.Count > 0)
|
|
131
|
{
|
|
132
|
// expression has free variables we need to match with right-hand-side of assignment.
|
|
133
|
freevars = assignment.nondetExpression.freeVariables;
|
|
134
|
|
|
135
|
foreach (var aRhsExpr in assignment.values)
|
|
136
|
{
|
|
137
|
if (aRhsExpr.freeVariables != null)
|
|
138
|
foreach (var freeRhsVar in aRhsExpr.freeVariables.symbolList)
|
|
139
|
{
|
|
140
|
if (freevars.Defined(freeRhsVar.tokenText))
|
|
141
|
{
|
|
142
|
Identifier exprvar = freevars.Get(freeRhsVar.tokenText);
|
|
143
|
if (freeRhsVar.type.kind == TypeKind.Any)
|
|
144
|
{
|
|
145
|
freeRhsVar.SetType(exprvar.type);
|
|
146
|
assignment.AddIdentifier(exprvar, null);
|
|
147
|
// remove free variable warnings
|
|
148
|
RemoveWarning(exprvar, String.Format("Free variable in expression: '{0}'.", exprvar.tokenText));
|
|
149
|
RemoveWarning(freeRhsVar, String.Format("Free variable in expression: '{0}'.", exprvar.tokenText));
|
|
150
|
}
|
|
151
|
else if (UlyssesType.TypeEqual(freeRhsVar.type, exprvar.type))
|
|
152
|
{
|
|
153
|
assignment.AddIdentifier(exprvar, null);
|
|
154
|
// remove free variable warnings
|
|
155
|
RemoveWarning(exprvar, String.Format("Free variable in expression: '{0}'.", exprvar.tokenText));
|
|
156
|
RemoveWarning(freeRhsVar, String.Format("Free variable in expression: '{0}'.", exprvar.tokenText));
|
|
157
|
}
|
|
158
|
else
|
|
159
|
Error(assignment, String.Format("Type mismatch on variable {0}: {1} <> {2}", freeRhsVar.tokenText, freeRhsVar.type.ToString(), exprvar.type.ToString()));
|
|
160
|
}
|
|
161
|
else
|
|
162
|
Error(assignment, String.Format("Undefined variable '{0}'", freeRhsVar.tokenText));
|
|
163
|
}
|
|
164
|
}
|
|
165
|
}
|
|
166
|
}
|
|
167
|
|
|
168
|
foreach (var avar in freevars.symbolList)
|
|
169
|
if (!assignment.symbols.Defined(avar.tokenText))
|
|
170
|
Error(assignment, String.Format("Undefined variable '{0}'", avar.tokenText));
|
|
171
|
|
|
172
|
if (assignment.places.Count != assignment.values.Count)
|
|
173
|
{
|
|
174
|
Error(assignment, "Number of places does not match number of values in assignment.");
|
|
175
|
//return;
|
|
176
|
}
|
|
177
|
|
|
178
|
LinkedListNode<Expression> aplace = assignment.places.First;
|
|
179
|
LinkedListNode<Expression> avalue = assignment.values.First;
|
|
180
|
|
|
181
|
while (aplace != null && avalue != null)
|
|
182
|
{
|
|
183
|
CheckPlace(aplace.Value, assignment);
|
|
184
|
|
|
185
|
// we allow non-pure methods only for assignments of the form 'variable := function(x,y)'
|
|
186
|
if (avalue.Value.kind != ExpressionKind.Call)
|
|
187
|
CheckMethodCallsArePure(avalue.Value);
|
|
188
|
|
|
189
|
UlyssesType acover = UlyssesType.CoverType(aplace.Value.type, avalue.Value.type);
|
|
190
|
if (acover == null)
|
|
191
|
Error(assignment, String.Format("Type mismatch in assignment: {0} ( {1} := {2} )", aplace.Value.ToString(), aplace.Value.type.ToString(), avalue.Value.type.ToString()));
|
|
192
|
else if (!UlyssesType.TypeEqualByKind(aplace.Value.type, acover)) /*ignore range things.. (see warning below)*/
|
|
193
|
Error(assignment, String.Format("Type mismatch in assignment: {0} ( {1} := {2} )", aplace.Value.ToString(), aplace.Value.type.ToString(), acover.ToString()));
|
|
194
|
else
|
|
195
|
{
|
|
196
|
List<ExpressionVariableIdentifier> uninitvars = avalue.Value.GetUninitializedFreeVariables();
|
|
197
|
Expression constantvalue = avalue.Value.kind == ExpressionKind.Value ? avalue.Value : null;
|
|
198
|
|
|
199
|
if (uninitvars.Count > 0)
|
|
200
|
Error(assignment, String.Format("Undefined variable '{0}'", uninitvars[0].tokenText));
|
|
201
|
|
|
202
|
if (!UlyssesType.TypeEqual(avalue.Value.type, acover))
|
|
203
|
{
|
|
204
|
UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, avalue.Value, avalue.Value.line, avalue.Value.pos);
|
|
205
|
cast.SetType(acover);
|
|
206
|
avalue.Value = cast;
|
|
207
|
}
|
|
208
|
|
|
209
|
if (UlyssesType.FirstTypeLessRange(aplace.Value.type, acover))
|
|
210
|
{
|
|
211
|
if (constantvalue == null)
|
|
212
|
{
|
|
213
|
Warning(assignment, String.Format("Assignment may over/underflow: {0} := {1}", aplace.Value.type.ToString(), acover.ToString()));
|
|
214
|
UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, avalue.Value, avalue.Value.line, avalue.Value.pos);
|
|
215
|
cast.SetType(aplace.Value.type);
|
|
216
|
avalue.Value = cast;
|
|
217
|
}
|
|
218
|
else
|
|
219
|
{
|
|
220
|
Error(assignment, String.Format("Assignment out of range ({0} := {1})", aplace.Value.ToString(), constantvalue.ToString()));
|
|
221
|
}
|
|
222
|
}
|
|
223
|
}
|
|
224
|
|
|
225
|
|
|
226
|
aplace = aplace.Next;
|
|
227
|
avalue = avalue.Next;
|
|
228
|
}
|
|
229
|
|
|
230
|
}
|
|
231
|
|
|
232
|
/// <summary>
|
|
233
|
/// Checks whether the LHS-expression of an assignment is a valid place.
|
|
234
|
/// IMPORTANT: If more complicated LHS expressions are allowed, then
|
|
235
|
/// ooaPrologExpression.cs needs to be adapted too!
|
|
236
|
/// </summary>
|
|
237
|
private void CheckPlace(Expression expression, Assignment assignment)
|
|
238
|
{
|
|
239
|
// check that we have some LHS of following forms
|
|
240
|
// self.<var/attr>
|
|
241
|
// attr[..]
|
|
242
|
bool result = true;
|
|
243
|
|
|
244
|
// one array/map access allowed
|
|
245
|
if (expression.kind == ExpressionKind.TupleMapAccess)
|
|
246
|
{
|
|
247
|
TupleMapAccessExpression tAccessExpression = (TupleMapAccessExpression)expression;
|
|
248
|
expression = tAccessExpression.child;
|
|
249
|
}
|
|
250
|
|
|
251
|
// attributes feature a self ref
|
|
252
|
if (expression.kind == ExpressionKind.Access)
|
|
253
|
{
|
|
254
|
AccessExpression accessExpression = (AccessExpression)expression;
|
|
255
|
if (accessExpression.left.kind == ExpressionKind.Identifier && ((IdentifierExpression)accessExpression.left).isSelf)
|
|
256
|
expression = accessExpression.right;
|
|
257
|
else
|
|
258
|
result = false;
|
|
259
|
}
|
|
260
|
|
|
261
|
// now we need to have an identifier
|
|
262
|
if (expression.kind != ExpressionKind.Identifier)
|
|
263
|
result = false;
|
|
264
|
|
|
265
|
if (!result)
|
|
266
|
Error(assignment, String.Format("LHS of assignment must be variable or attribute."));
|
|
267
|
}
|
|
268
|
|
|
269
|
|
|
270
|
private void TypeCheckQualConstraint(QualitativeConstraintStatement qualConstr)
|
|
271
|
{
|
|
272
|
if (qualConstr.variable0.type.kind != TypeKind.QrType && qualConstr.variable0.type.kind != TypeKind.Any)
|
|
273
|
Error(qualConstr, String.Format("Qualitative type expected: '{0}'", qualConstr.variable0.tokenText));
|
|
274
|
if (qualConstr.variable1.type.kind != TypeKind.QrType && qualConstr.variable1.type.kind != TypeKind.Any)
|
|
275
|
Error(qualConstr, String.Format("Qualitative type expected: '{0}'", qualConstr.variable0.tokenText));
|
|
276
|
if (qualConstr.variable2 != null && qualConstr.variable2.type.kind != TypeKind.QrType
|
|
277
|
&& qualConstr.variable2.type.kind != TypeKind.Any)
|
|
278
|
Error(qualConstr, String.Format("Qualitative type expected: '{0}'", qualConstr.variable0.tokenText));
|
|
279
|
}
|
|
280
|
private void TypeCheck(Statement statement)
|
|
281
|
{
|
|
282
|
switch (statement.kind)
|
|
283
|
{
|
|
284
|
case StatementKind.Abort:
|
|
285
|
case StatementKind.Skip:
|
|
286
|
break;
|
|
287
|
|
|
288
|
case StatementKind.NondetBlock:
|
|
289
|
case StatementKind.PrioBlock:
|
|
290
|
case StatementKind.SeqBlock:
|
|
291
|
statement.Accept(this);
|
|
292
|
break;
|
|
293
|
|
|
294
|
case StatementKind.Assignment:
|
|
295
|
Assignment assignment = (Assignment)statement;
|
|
296
|
TypeCheckAssignment(assignment);
|
|
297
|
break;
|
|
298
|
case StatementKind.GuardedCommand:
|
|
299
|
GuardedCommand gc = (GuardedCommand)statement;
|
|
300
|
TypeCheckGuardedCommand(gc);
|
|
301
|
break;
|
|
302
|
case StatementKind.Kill:
|
|
303
|
KillStatement kill = (KillStatement)statement;
|
|
304
|
if (kill.someOne.type.kind != TypeKind.OoActionSystemType)
|
|
305
|
Error(kill, String.Format(" {0} not an object", kill.someOne.tokenText));
|
|
306
|
break;
|
|
307
|
case StatementKind.MethodCall:
|
|
308
|
Call callstatement = (Call)statement;
|
|
309
|
if (callstatement.callExpression.GetUninitializedFreeVariables().Count > 0)
|
|
310
|
Error(callstatement, "Uninitialized free variables in call expression.");
|
|
311
|
if (callstatement.callExpression.kind != ExpressionKind.Call
|
|
312
|
&& callstatement.callExpression.kind != ExpressionKind.foldRL
|
|
313
|
&& callstatement.callExpression.kind != ExpressionKind.foldLR)
|
|
314
|
Error(callstatement, "Not a valid method call");
|
|
315
|
break;
|
|
316
|
case StatementKind.QualConstraint:
|
|
317
|
QualitativeConstraintStatement qualConstr = (QualitativeConstraintStatement)statement;
|
|
318
|
TypeCheckQualConstraint(qualConstr);
|
|
319
|
break;
|
|
320
|
default:
|
|
321
|
throw new NotImplementedException();
|
|
322
|
}
|
|
323
|
}
|
|
324
|
|
|
325
|
//private void TypeCheck()
|
|
326
|
|
|
327
|
private void TypeCheck(AttributeIdentifier attributeIdentifier)
|
|
328
|
{
|
|
329
|
if (attributeIdentifier.initializer == null)
|
|
330
|
throw new ArgumentException();
|
|
331
|
|
|
332
|
UlyssesType atype = attributeIdentifier.initializer.type;
|
|
333
|
if (atype == null)
|
|
334
|
Error(attributeIdentifier, "Initializer lacks type.");
|
|
335
|
else
|
|
336
|
{
|
|
337
|
/* we use the typecheck to validate a few more properties of the initializer that
|
|
338
|
* need a completely resolved expression
|
|
339
|
*/
|
|
340
|
OoaInitializerCheck initCheck = new OoaInitializerCheck();
|
|
341
|
attributeIdentifier.initializer.Accept(initCheck);
|
|
342
|
if (initCheck.attributeAccess.Count > 0)
|
|
343
|
// disallow use of other attributes in initializer
|
|
344
|
Error(attributeIdentifier, "Access of other attributes not allowed in attribute initializer.");
|
|
345
|
else if (attributeIdentifier.initializer.callTargets.Count > 0)
|
|
346
|
// disallow method calls in initializer
|
|
347
|
Error(attributeIdentifier, "Method calls not allowed in attribute initializer.");
|
|
348
|
else if (attributeIdentifier.initializer.freeVariables.symbolList.Count > 0)
|
|
349
|
// disallow use of free variables in initializer
|
|
350
|
Error(attributeIdentifier,
|
|
351
|
String.Format("Unknown identifier in initializer: '{0}'",
|
|
352
|
attributeIdentifier.initializer.freeVariables.symbolList[0].tokenText));
|
|
353
|
else
|
|
354
|
{
|
|
355
|
UlyssesType idtype = attributeIdentifier.type;
|
|
356
|
UlyssesType acover = UlyssesType.CoverType(idtype, atype);
|
|
357
|
|
|
358
|
if (acover == null)
|
|
359
|
Error(attributeIdentifier, String.Format("Type mismatch in attribute initializer: {0} ( {1} := {2} )", attributeIdentifier.ToString(), idtype.ToString(), atype.ToString()));
|
|
360
|
else if (!UlyssesType.TypeEqualByKind(idtype, acover)) /*ignore range things.. (see warning below)*/
|
|
361
|
Error(attributeIdentifier, String.Format("Type mismatch in attribute initializer: {0} ( {1} := {2} )", attributeIdentifier.ToString(), idtype.ToString(), acover.ToString()));
|
|
362
|
else
|
|
363
|
{
|
|
364
|
Expression constantvalue = attributeIdentifier.initializer.kind == ExpressionKind.Value ? attributeIdentifier.initializer : null;
|
|
365
|
|
|
366
|
if (!UlyssesType.TypeEqual(atype, acover))
|
|
367
|
{
|
|
368
|
UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, attributeIdentifier.initializer,
|
|
369
|
attributeIdentifier.initializer.line, attributeIdentifier.initializer.pos);
|
|
370
|
cast.SetType(acover);
|
|
371
|
attributeIdentifier.SetInitializer(cast);
|
|
372
|
}
|
|
373
|
|
|
374
|
if (UlyssesType.FirstTypeLessRange(idtype, acover))
|
|
375
|
{
|
|
376
|
if (constantvalue == null)
|
|
377
|
{
|
|
378
|
Warning(attributeIdentifier, String.Format("Assignment may over/underflow: {0} := {1}", idtype.ToString(), acover.ToString()));
|
|
379
|
UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, attributeIdentifier.initializer,
|
|
380
|
attributeIdentifier.initializer.line, attributeIdentifier.initializer.pos);
|
|
381
|
cast.SetType(idtype);
|
|
382
|
attributeIdentifier.SetInitializer(cast);
|
|
383
|
}
|
|
384
|
else
|
|
385
|
{
|
|
386
|
Error(attributeIdentifier, String.Format("Initialization out of range ({0} := {1})", attributeIdentifier.ToString(), constantvalue.ToString()));
|
|
387
|
}
|
|
388
|
}
|
|
389
|
}
|
|
390
|
|
|
391
|
/*
|
|
392
|
|
|
393
|
|
|
394
|
if (cover == null || !UlyssesType.TypeEqual(cover, idtype))
|
|
395
|
Error(attributeIdentifier,
|
|
396
|
String.Format("Type mismatch in attribute initializer: expected '{0}', found '{1}'",
|
|
397
|
idtype.ToString(), atype.ToString()));
|
|
398
|
else
|
|
399
|
attributeIdentifier.SetInitializer(UnaryOperator.CoerceUp(attributeIdentifier.initializer, idtype));
|
|
400
|
* */
|
|
401
|
}
|
|
402
|
}
|
|
403
|
}
|
|
404
|
|
|
405
|
|
|
406
|
protected override void VisitAstElement(IAst element, IAst parent)
|
|
407
|
{
|
|
408
|
if (element.nodeType == AstNodeTypeEnum.statement)
|
|
409
|
{
|
|
410
|
TypeCheck((Statement)element);
|
|
411
|
}
|
|
412
|
else if (element.nodeType == AstNodeTypeEnum.identifier
|
|
413
|
&& ((Identifier)element).kind == IdentifierKind.AttributeIdentifier)
|
|
414
|
{
|
|
415
|
TypeCheck((AttributeIdentifier)element);
|
|
416
|
}
|
|
417
|
else base.VisitAstElement(element, parent);
|
|
418
|
}
|
|
419
|
|
|
420
|
|
|
421
|
|
|
422
|
public OoaTypeCheckVisitor(ParserState aState)
|
|
423
|
: base(aState)
|
|
424
|
{
|
|
425
|
if (aState == null)
|
|
426
|
throw new ArgumentException();
|
|
427
|
}
|
|
428
|
}
|
|
429
|
|
|
430
|
|
|
431
|
|
|
432
|
}
|