|
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
|
/// <summary>
|
|
26
|
/// This visitor scans all methods and named actions in order to check
|
|
27
|
/// whether they are safe, in the sense that they are only using
|
|
28
|
/// basic commands that obey the excluded miracle rule automatically.
|
|
29
|
///
|
|
30
|
/// The idea is that the weakest precondition of "safe named actions"
|
|
31
|
/// automatically is the guard of the obligatorty guarded command.
|
|
32
|
///
|
|
33
|
/// Allowed commands for "safe" code:
|
|
34
|
/// -> Assignment (deterministic!)
|
|
35
|
/// -> Sequential Composition
|
|
36
|
/// Currently not supported within the analysis:
|
|
37
|
/// -> Conditional Statement (emulated by requires A: end [] requires not A: end)
|
|
38
|
/// -> Iteration (not available)
|
|
39
|
/// </summary>
|
|
40
|
public sealed class OoaActionClassifierVisitor : OoaCompleteAstTraversalVisitor
|
|
41
|
{
|
|
42
|
|
|
43
|
|
|
44
|
private void CalcBodySafe(FunctionIdentifier methodIdentifier, FunctionType mType, ref bool m_hasUnsafeElement, ref Block ablock)
|
|
45
|
{
|
|
46
|
string methodAction;
|
|
47
|
if (mType.functionType == FunctionTypeEnum.Method)
|
|
48
|
methodAction = "Method";
|
|
49
|
else
|
|
50
|
methodAction = "Action";
|
|
51
|
|
|
52
|
|
|
53
|
while ((ablock != null) && (ablock.kind != StatementKind.SeqBlock) && (ablock.statements.Count > 0))
|
|
54
|
{
|
|
55
|
if (ablock.statements.Count > 1)
|
|
56
|
{
|
|
57
|
m_ParserState.AddMessage(
|
|
58
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
59
|
ablock.pos, String.Format("{0} {1} extended: More than one element in Nondet/Prio Block.",
|
|
60
|
methodAction, methodIdentifier.tokenText)));
|
|
61
|
mType.SetMiracleSafe(false);
|
|
62
|
}
|
|
63
|
ablock = (Block)ablock.statements.First.Value;
|
|
64
|
}
|
|
65
|
|
|
66
|
foreach (var s in ablock.statements)
|
|
67
|
{
|
|
68
|
switch (s.kind)
|
|
69
|
{
|
|
70
|
case StatementKind.Abort:
|
|
71
|
// abort maps any postcondition to false, iow. wp(abort,X) = false
|
|
72
|
m_hasUnsafeElement = true; // excluded miracle holds, but I'm not sure about continuity.. *g*
|
|
73
|
m_ParserState.AddMessage(
|
|
74
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
75
|
ablock.pos, String.Format("{0} {1} extended: Abort detected.",
|
|
76
|
methodAction, methodIdentifier.tokenText)));
|
|
77
|
break;
|
|
78
|
case StatementKind.Assignment:
|
|
79
|
Assignment ass = (Assignment)s;
|
|
80
|
m_hasUnsafeElement |= ass.nondetExpression != null;
|
|
81
|
if (m_hasUnsafeElement)
|
|
82
|
m_ParserState.AddMessage(
|
|
83
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
84
|
ablock.pos, String.Format("{0} {1} extended: possibly nondeterministic assignment.",
|
|
85
|
methodAction, methodIdentifier.tokenText)));
|
|
86
|
// check value expressions
|
|
87
|
foreach (var x in ass.values)
|
|
88
|
{
|
|
89
|
if (x.GetUninitializedFreeVariables().Count > 0)
|
|
90
|
{
|
|
91
|
m_hasUnsafeElement = true;
|
|
92
|
m_ParserState.AddMessage(
|
|
93
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
94
|
ablock.pos, String.Format("{0} {1} extended: uninitialized free variables in expression.",
|
|
95
|
methodAction, methodIdentifier.tokenText)));
|
|
96
|
continue;
|
|
97
|
}
|
|
98
|
foreach (var ct in x.callTargets)
|
|
99
|
{
|
|
100
|
if ( ((FunctionType)ct.type).isMiracleSafe == null)
|
|
101
|
ct.Accept(this);
|
|
102
|
m_hasUnsafeElement |= ((FunctionType)ct.type).isMiracleSafe ?? true;
|
|
103
|
if (m_hasUnsafeElement)
|
|
104
|
m_ParserState.AddMessage(
|
|
105
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
106
|
ablock.pos, String.Format("{0} {1} extended: call of extended method in value expression.",
|
|
107
|
methodAction, methodIdentifier.tokenText)));
|
|
108
|
}
|
|
109
|
}
|
|
110
|
break;
|
|
111
|
case StatementKind.GuardedCommand:
|
|
112
|
m_hasUnsafeElement = true; // we do not allow guarded commands in methods as they would be included in actions!
|
|
113
|
// we do not allow a second guarded command in named actions.
|
|
114
|
m_ParserState.AddMessage(
|
|
115
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
116
|
ablock.pos, String.Format("{0} {1} extended: guarded command detected.",
|
|
117
|
methodAction, methodIdentifier.tokenText)));
|
|
118
|
break;
|
|
119
|
case StatementKind.Kill:
|
|
120
|
m_hasUnsafeElement = true;
|
|
121
|
m_ParserState.AddMessage(
|
|
122
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
123
|
ablock.pos, String.Format("{0} {1} extended: Kill detected.",
|
|
124
|
methodAction, methodIdentifier.tokenText)));
|
|
125
|
break;
|
|
126
|
case StatementKind.MethodCall:
|
|
127
|
Call acall = (Call)s;
|
|
128
|
|
|
129
|
foreach (FunctionIdentifier anid in acall.callExpression.callTargets)
|
|
130
|
{
|
|
131
|
FunctionType atype = (FunctionType)anid.type;
|
|
132
|
if (atype.isMiracleSafe == null)
|
|
133
|
atype.identifier.Accept(this);
|
|
134
|
m_hasUnsafeElement |= atype.isMiracleSafe ?? true;
|
|
135
|
if (m_hasUnsafeElement)
|
|
136
|
m_ParserState.AddMessage(
|
|
137
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
138
|
ablock.pos, String.Format("{0} {1} extended: calls extended method '{2}'.",
|
|
139
|
methodAction, methodIdentifier.tokenText,anid.tokenText)));
|
|
140
|
}
|
|
141
|
break;
|
|
142
|
case StatementKind.NondetBlock:
|
|
143
|
m_hasUnsafeElement = true;
|
|
144
|
m_ParserState.AddMessage(
|
|
145
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
146
|
ablock.pos, String.Format("{0} {1} extended: more than one nondet-block.",
|
|
147
|
methodAction, methodIdentifier.tokenText)));
|
|
148
|
break;
|
|
149
|
case StatementKind.PrioBlock:
|
|
150
|
m_hasUnsafeElement = true;
|
|
151
|
m_ParserState.AddMessage(
|
|
152
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
153
|
ablock.pos, String.Format("{0} {1} extended: more than one prio block.",
|
|
154
|
methodAction, methodIdentifier.tokenText)));
|
|
155
|
break;
|
|
156
|
case StatementKind.Skip:
|
|
157
|
break;
|
|
158
|
case StatementKind.QualConstraint:
|
|
159
|
m_hasUnsafeElement = true;
|
|
160
|
break;
|
|
161
|
case StatementKind.SeqBlock:
|
|
162
|
// seq block in seq block should not occur..
|
|
163
|
default:
|
|
164
|
throw new NotImplementedException();
|
|
165
|
}
|
|
166
|
if (m_hasUnsafeElement)
|
|
167
|
break;
|
|
168
|
}
|
|
169
|
}
|
|
170
|
|
|
171
|
|
|
172
|
public override void visit(MethodIdentifier methodIdentifier)
|
|
173
|
{
|
|
174
|
FunctionType mType = (FunctionType)methodIdentifier.type;
|
|
175
|
if (mType.isMiracleSafe != null)
|
|
176
|
return;
|
|
177
|
|
|
178
|
// AST of method may have one prioritized block before the nondet block
|
|
179
|
// both blocks must not have more than one element. (we do not implement conditional)
|
|
180
|
bool m_hasUnsafeElement = false;
|
|
181
|
Block ablock = methodIdentifier.body;
|
|
182
|
|
|
183
|
CalcBodySafe(methodIdentifier, mType, ref m_hasUnsafeElement, ref ablock);
|
|
184
|
|
|
185
|
/*
|
|
186
|
if (!m_hasUnsafeElement)
|
|
187
|
m_ParserState.AddMessage(
|
|
188
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
189
|
ablock.pos, String.Format("Found basic method: '{0}'",
|
|
190
|
methodIdentifier.tokenText)));
|
|
191
|
*/
|
|
192
|
|
|
193
|
mType.SetMiracleSafe(!m_hasUnsafeElement);
|
|
194
|
}
|
|
195
|
|
|
196
|
|
|
197
|
public override void visit(NamedActionIdentifier namedActionIdentifier)
|
|
198
|
{
|
|
199
|
FunctionType mType = (FunctionType)namedActionIdentifier.type;
|
|
200
|
if (mType.isMiracleSafe != null)
|
|
201
|
return;
|
|
202
|
|
|
203
|
// AST of namedaction starts with a seq block with only one guarded command..
|
|
204
|
Block seqb = namedActionIdentifier.body;
|
|
205
|
System.Diagnostics.Debug.Assert(seqb.statements.Count == 1);
|
|
206
|
System.Diagnostics.Debug.Assert(seqb.statements.First.Value.kind == StatementKind.GuardedCommand);
|
|
207
|
|
|
208
|
GuardedCommand gc = (GuardedCommand)seqb.statements.First.Value;
|
|
209
|
Block ablock = gc.body;
|
|
210
|
bool hasUnsafeElement = false;
|
|
211
|
|
|
212
|
CalcBodySafe(namedActionIdentifier, mType, ref hasUnsafeElement, ref ablock);
|
|
213
|
/*
|
|
214
|
if (!hasUnsafeElement)
|
|
215
|
m_ParserState.AddMessage(
|
|
216
|
new ParserMessage(m_ParserState.filename, ablock.line,
|
|
217
|
ablock.pos, String.Format("Found basic action: '{0}'",
|
|
218
|
namedActionIdentifier.tokenText)));
|
|
219
|
*/
|
|
220
|
mType.SetMiracleSafe(!hasUnsafeElement);
|
|
221
|
}
|
|
222
|
|
|
223
|
public override void visit(OoActionSystemType ooActionSystemType)
|
|
224
|
{
|
|
225
|
base.visit(ooActionSystemType);
|
|
226
|
bool allsafe = true;
|
|
227
|
foreach (var x in ooActionSystemType.symbols.symbolList)
|
|
228
|
{
|
|
229
|
if (x.kind == IdentifierKind.MethodIdentifier
|
|
230
|
|| x.kind == IdentifierKind.NamedActionIdentifier)
|
|
231
|
{
|
|
232
|
allsafe &= ((FunctionType)x.type).isMiracleSafe ?? false;
|
|
233
|
}
|
|
234
|
}
|
|
235
|
if (allsafe)
|
|
236
|
m_ParserState.AddMessage(
|
|
237
|
new ParserMessage(m_ParserState.filename, ooActionSystemType.identifier.line,
|
|
238
|
ooActionSystemType.identifier.column, String.Format("Found action system with basic actions/methods only: '{0}'",
|
|
239
|
ooActionSystemType.identifier.tokenText)));
|
|
240
|
|
|
241
|
}
|
|
242
|
|
|
243
|
|
|
244
|
public OoaActionClassifierVisitor(ParserState aState)
|
|
245
|
: base(aState)
|
|
246
|
{ }
|
|
247
|
}
|
|
248
|
}
|
|
249
|
|