root / trunk / compiler / ooasCompiler / src / org / momut / ooas / visitors / OoaActionClassifierVisitor.java @ 9
1 |
/**
|
---|---|
2 |
*
|
3 |
* OOAS Compiler
|
4 |
*
|
5 |
* Copyright 2015, AIT Austrian Institute of Technology.
|
6 |
* This code is based on the C# Version of the OOAS Compiler, which is
|
7 |
* copyright 2015 by the Institute of Software Technology, Graz University
|
8 |
* of Technology with portions copyright by the AIT Austrian Institute of
|
9 |
* Technology. All rights reserved.
|
10 |
*
|
11 |
* SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.
|
12 |
*
|
13 |
* If you modify the file please update the list of contributors below to in-
|
14 |
* clude your name. Please also stick to the coding convention of using TABs
|
15 |
* to do the basic (block-level) indentation and spaces for anything after
|
16 |
* that. (Enable the display of special chars and it should be pretty obvious
|
17 |
* what this means.) Also, remove all trailing whitespace.
|
18 |
*
|
19 |
* Contributors:
|
20 |
* Willibald Krenn (AIT)
|
21 |
* Stephan Zimmerer (AIT)
|
22 |
* Markus Demetz (AIT)
|
23 |
* Christoph Czurda (AIT)
|
24 |
*
|
25 |
*/
|
26 |
|
27 |
|
28 |
package org.momut.ooas.visitors; |
29 |
|
30 |
import java.util.LinkedList; |
31 |
|
32 |
import org.momut.ooas.ast.expressions.Expression; |
33 |
import org.momut.ooas.ast.identifiers.FunctionIdentifier; |
34 |
import org.momut.ooas.ast.identifiers.Identifier; |
35 |
import org.momut.ooas.ast.identifiers.IdentifierKind; |
36 |
import org.momut.ooas.ast.identifiers.MethodIdentifier; |
37 |
import org.momut.ooas.ast.identifiers.NamedActionIdentifier; |
38 |
import org.momut.ooas.ast.statements.Assignment; |
39 |
import org.momut.ooas.ast.statements.Block; |
40 |
import org.momut.ooas.ast.statements.Call; |
41 |
import org.momut.ooas.ast.statements.Statement; |
42 |
import org.momut.ooas.ast.statements.StatementKind; |
43 |
import org.momut.ooas.ast.types.FunctionType; |
44 |
import org.momut.ooas.ast.types.OoActionSystemType; |
45 |
import org.momut.ooas.ast.types.FunctionType.FunctionTypeEnum; |
46 |
import org.momut.ooas.parser.ParserMessage; |
47 |
import org.momut.ooas.parser.ParserState; |
48 |
import org.momut.ooas.utils.exceptions.NotImplementedException; |
49 |
|
50 |
/// <summary>
|
51 |
/// This visitor scans all methods and named actions in order to check
|
52 |
/// whether they are safe, in the sense that they are only using
|
53 |
/// basic commands that obey the excluded miracle rule automatically.
|
54 |
///
|
55 |
/// The idea is that the weakest precondition of "safe named actions"
|
56 |
/// automatically is the guard of the obligatorty guarded command.
|
57 |
///
|
58 |
/// Allowed commands for "safe" code:
|
59 |
/// -> Assignment (deterministic!)
|
60 |
/// -> Sequential Composition
|
61 |
/// Currently not supported within the analysis:
|
62 |
/// -> Conditional Statement (emulated by requires A: end [] requires not A: end)
|
63 |
/// -> Iteration (not available)
|
64 |
/// </summary>
|
65 |
public final class OoaActionClassifierVisitor extends OoaCompleteAstTraversalVisitor |
66 |
{ |
67 |
private static final class RefWorkAround { |
68 |
boolean m_hasUnsafeElement;
|
69 |
Statement ablock;
|
70 |
public RefWorkAround(boolean ue, Statement b) { |
71 |
m_hasUnsafeElement = ue; |
72 |
ablock = b; |
73 |
} |
74 |
} |
75 |
|
76 |
private boolean getValue(Boolean input, boolean defaultValue) { |
77 |
return input == null ? defaultValue: input; |
78 |
} |
79 |
|
80 |
|
81 |
@SuppressWarnings("serial") |
82 |
private void CalcBodySafe(FunctionIdentifier methodIdentifier, FunctionType mType, final RefWorkAround w) |
83 |
{ |
84 |
String methodAction;
|
85 |
if (mType.functionType() == FunctionTypeEnum.Method)
|
86 |
methodAction = "Method";
|
87 |
else
|
88 |
methodAction = "Action";
|
89 |
|
90 |
|
91 |
while ((w.ablock != null) && (w.ablock.kind() == StatementKind.PrioBlock || w.ablock.kind() == StatementKind.NondetBlock)) |
92 |
{ |
93 |
final Block block = (Block) w.ablock;
|
94 |
if (block.statements().size() == 0) |
95 |
break;
|
96 |
|
97 |
if (block.statements().size() > 1) |
98 |
{ |
99 |
m_ParserState.AddMessage( |
100 |
new ParserMessage(m_ParserState.filename, w.ablock.line(),
|
101 |
w.ablock.pos(), String.format("%s %s extended: More than one element in Nondet/Prio Block.", |
102 |
methodAction, methodIdentifier.tokenText()))); |
103 |
mType.SetMiracleSafe(false);
|
104 |
} |
105 |
w.ablock = block.statements().peekFirst(); |
106 |
} |
107 |
|
108 |
final LinkedList<Statement> stmts = w.ablock.kind() == StatementKind.SeqBlock ? ((Block) w.ablock).statements() : new LinkedList<Statement>(){{add(w.ablock);}}; |
109 |
for (final Statement s: stmts) |
110 |
{ |
111 |
switch (s.kind())
|
112 |
{ |
113 |
case Abort:
|
114 |
// abort maps any postcondition to false, iow. wp(abort,X) = false
|
115 |
w.m_hasUnsafeElement = true; // excluded miracle holds, but I'm not sure about continuity.. *g* |
116 |
m_ParserState.AddMessage( |
117 |
new ParserMessage(m_ParserState.filename, w.ablock.line(),
|
118 |
w.ablock.pos(), String.format("%s %s extended: Abort detected.", |
119 |
methodAction, methodIdentifier.tokenText()))); |
120 |
break;
|
121 |
case Assignment:
|
122 |
final Assignment ass = (Assignment)s;
|
123 |
w.m_hasUnsafeElement |= ass.nondetExpression() != null;
|
124 |
if (w.m_hasUnsafeElement)
|
125 |
m_ParserState.AddMessage( |
126 |
new ParserMessage(m_ParserState.filename, w.ablock.line(),
|
127 |
w.ablock.pos(), String.format("%s %s extended: possibly nondeterministic assignment.", |
128 |
methodAction, methodIdentifier.tokenText()))); |
129 |
// check value expressions
|
130 |
for (final Expression x: ass.values()) |
131 |
{ |
132 |
if (x.GetUninitializedFreeVariables().size() > 0) |
133 |
{ |
134 |
w.m_hasUnsafeElement = true;
|
135 |
m_ParserState.AddMessage( |
136 |
new ParserMessage(m_ParserState.filename, w.ablock.line(),
|
137 |
w.ablock.pos(), String.format("%s %s extended: uninitialized free variables in expression.", |
138 |
methodAction, methodIdentifier.tokenText()))); |
139 |
continue;
|
140 |
} |
141 |
for (final FunctionIdentifier ct: x.callTargets()) |
142 |
{ |
143 |
if ( ((FunctionType)ct.type()).isMiracleSafe() == null) |
144 |
ct.Accept(this);
|
145 |
w.m_hasUnsafeElement |= getValue(((FunctionType)ct.type()).isMiracleSafe(), true);
|
146 |
if (w.m_hasUnsafeElement)
|
147 |
m_ParserState.AddMessage( |
148 |
new ParserMessage(m_ParserState.filename, w.ablock.line(),
|
149 |
w.ablock.pos(), String.format("%s %s extended: call of extended method in value expression.", |
150 |
methodAction, methodIdentifier.tokenText()))); |
151 |
} |
152 |
} |
153 |
break;
|
154 |
case GuardedCommand:
|
155 |
w.m_hasUnsafeElement = true; // we do not allow guarded commands in methods as they would be included in actions! |
156 |
// we do not allow a second guarded command in named actions.
|
157 |
m_ParserState.AddMessage( |
158 |
new ParserMessage(m_ParserState.filename, w.ablock.line(),
|
159 |
w.ablock.pos(), String.format("%s %s extended: guarded command detected.", |
160 |
methodAction, methodIdentifier.tokenText()))); |
161 |
break;
|
162 |
case Kill:
|
163 |
w.m_hasUnsafeElement = true;
|
164 |
m_ParserState.AddMessage( |
165 |
new ParserMessage(m_ParserState.filename, w.ablock.line(),
|
166 |
w.ablock.pos(), String.format("%s %s extended: Kill detected.", |
167 |
methodAction, methodIdentifier.tokenText()))); |
168 |
break;
|
169 |
case MethodCall:
|
170 |
final Call acall = (Call)s;
|
171 |
|
172 |
for (final FunctionIdentifier anid: acall.callExpression().callTargets()) |
173 |
{ |
174 |
final FunctionType atype = (FunctionType)anid.type();
|
175 |
if (atype.isMiracleSafe() == null) |
176 |
atype.identifier().Accept(this);
|
177 |
w.m_hasUnsafeElement |= getValue(atype.isMiracleSafe(), true);
|
178 |
if (w.m_hasUnsafeElement)
|
179 |
m_ParserState.AddMessage( |
180 |
new ParserMessage(m_ParserState.filename, w.ablock.line(),
|
181 |
w.ablock.pos(), String.format("%s %s extended: calls extended method '%s'.", |
182 |
methodAction, methodIdentifier.tokenText(),anid.tokenText()))); |
183 |
} |
184 |
break;
|
185 |
case NondetBlock:
|
186 |
w.m_hasUnsafeElement = true;
|
187 |
m_ParserState.AddMessage( |
188 |
new ParserMessage(m_ParserState.filename, w.ablock.line(),
|
189 |
w.ablock.pos(), String.format("%s %s extended: more than one nondet-block.", |
190 |
methodAction, methodIdentifier.tokenText()))); |
191 |
break;
|
192 |
case PrioBlock:
|
193 |
w.m_hasUnsafeElement = true;
|
194 |
m_ParserState.AddMessage( |
195 |
new ParserMessage(m_ParserState.filename, w.ablock.line(),
|
196 |
w.ablock.pos(), String.format("%s %s extended: more than one prio block.", |
197 |
methodAction, methodIdentifier.tokenText()))); |
198 |
break;
|
199 |
case Skip:
|
200 |
case Break:
|
201 |
break;
|
202 |
case SeqBlock:
|
203 |
// seq block in seq block should not occur..
|
204 |
default:
|
205 |
throw new NotImplementedException(); |
206 |
} |
207 |
if (w.m_hasUnsafeElement)
|
208 |
break;
|
209 |
} |
210 |
} |
211 |
|
212 |
|
213 |
@Override
|
214 |
public void visit(MethodIdentifier methodIdentifier) |
215 |
{ |
216 |
final FunctionType mType = (FunctionType)methodIdentifier.type();
|
217 |
if (mType.isMiracleSafe() != null) |
218 |
return;
|
219 |
|
220 |
// AST of method may have one prioritized block before the nondet block
|
221 |
// both blocks must not have more than one element. (we do not implement conditional)
|
222 |
final RefWorkAround w = new RefWorkAround(false, methodIdentifier.body()); |
223 |
CalcBodySafe(methodIdentifier, mType, w); |
224 |
|
225 |
/*
|
226 |
if (!m_hasUnsafeElement)
|
227 |
m_ParserState.AddMessage(
|
228 |
new ParserMessage(m_ParserState.filename, ablock.line,
|
229 |
ablock.pos, String.Format("Found basic method: '%s'",
|
230 |
methodIdentifier.tokenText)));
|
231 |
*/
|
232 |
|
233 |
mType.SetMiracleSafe(!w.m_hasUnsafeElement); |
234 |
} |
235 |
|
236 |
|
237 |
@Override
|
238 |
public void visit(NamedActionIdentifier namedActionIdentifier) |
239 |
{ |
240 |
final FunctionType mType = (FunctionType)namedActionIdentifier.type();
|
241 |
if (mType.isMiracleSafe() != null) |
242 |
return;
|
243 |
|
244 |
final RefWorkAround w = new RefWorkAround(false, namedActionIdentifier.body()); |
245 |
|
246 |
CalcBodySafe(namedActionIdentifier, mType, w); |
247 |
/*
|
248 |
if (!hasUnsafeElement)
|
249 |
m_ParserState.AddMessage(
|
250 |
new ParserMessage(m_ParserState.filename, ablock.line,
|
251 |
ablock.pos, String.Format("Found basic action: '%s'",
|
252 |
namedActionIdentifier.tokenText)));
|
253 |
*/
|
254 |
mType.SetMiracleSafe(!w.m_hasUnsafeElement); |
255 |
} |
256 |
|
257 |
@Override
|
258 |
public void visit(OoActionSystemType ooActionSystemType) |
259 |
{ |
260 |
super.visit(ooActionSystemType);
|
261 |
boolean allsafe = true; |
262 |
for (final Identifier x: ooActionSystemType.symbols().symbolList()) |
263 |
{ |
264 |
if (x.kind() == IdentifierKind.MethodIdentifier
|
265 |
|| x.kind() == IdentifierKind.NamedActionIdentifier) |
266 |
{ |
267 |
allsafe &= getValue(((FunctionType)x.type()).isMiracleSafe(), false);
|
268 |
} |
269 |
} |
270 |
if (allsafe)
|
271 |
m_ParserState.AddMessage( |
272 |
new ParserMessage(m_ParserState.filename, ooActionSystemType.identifier().line(),
|
273 |
ooActionSystemType.identifier().column(), String.format("Found action system with basic actions/methods only: '%s'", |
274 |
ooActionSystemType.identifier().tokenText()))); |
275 |
} |
276 |
|
277 |
|
278 |
public OoaActionClassifierVisitor(ParserState aState)
|
279 |
{ |
280 |
super (aState);
|
281 |
} |
282 |
} |