001 package escjava.vcGeneration.pvs;
002
003 import java.io.*;
004
005 import escjava.vcGeneration.*;
006
007 public class TPvsVisitor extends TVisitor {
008
009 TPvsVisitor(Writer out) {
010 super(out);
011 }
012
013 /**
014 * General Function
015 * You give the operator at the first argument and then it outputs
016 * op (son1, son2 ...)
017 * )
018 */
019 public void genericFun(/*@ non_null @*/String s, TFunction n) throws IOException{
020
021 lib.appendI(s + " (");
022
023 for (int i = 0; i < n.sons.size(); i++) {
024 n.getChildAt(i).accept(this);
025
026 /*
027 * If not last, output a comma
028 */
029 if (i != n.sons.size() - 1)
030 lib.appendN(", ");
031 }
032
033 lib.appendN(")");
034
035 int lastChild = n.sons.size() - 1;
036 if ((n.getChildAt(lastChild)) instanceof TName
037 || (n.getChildAt(lastChild)) instanceof TLiteral)
038 lib.reduceIwNl();
039 else
040 lib.reduceI();
041
042 }
043
044 /**
045 * Function/Operator with arity 1 :
046 * (op X)
047 */
048 public void unaryGeneric(/*@ non_null @*/String s, TFunction n) throws IOException {
049
050 if (n.sons.size() != 1)
051 TDisplay.err(this, "unaryGeneric(String s, TFunction n)",
052 "An unary operator named " + s
053 + " has a number of sons equals to "
054 + n.sons.size() + " which is different from 1");
055
056 lib.appendI(s);
057
058 n.getChildAt(0).accept(this);
059
060 if ((n.getChildAt(0)) instanceof TName
061 || (n.getChildAt(0)) instanceof TLiteral)
062 lib.reduceIwNl();
063 else
064 lib.reduceI();
065
066 }
067
068 /**
069 * You give the operator at the first argument and then it outputs
070 * (son1
071 op
072 son2 ...
073 op
074 sonN)
075 */
076 public void genericOp(/*@ non_null @*/String s, TFunction n) throws IOException {
077
078 lib.appendI("");
079
080 int i = 0;
081 for (; i < n.sons.size(); i++) {
082 n.getChildAt(i).accept(this);
083
084 /*
085 * not the last
086 */
087 if (i != n.sons.size() - 1) {
088 lib.appendN("\n");
089 lib.append(s);
090 }
091
092 lib.appendN(" ");
093 }
094
095 lib.reduceI();
096 }
097
098 /**
099 * Function for binary operator
100 * You give the operator at the first argument and then it outputs
101 * (son1
102 * op
103 * son2)
104 *
105 * If son1 is a variable, op isn't on the next line
106 * If son2 is a variable, it doesn't go to next line.
107 */
108 public void binOp(/*@ non_null @*/String s, TFunction n) throws IOException {
109
110 if (n.sons.size() != 2)
111 TDisplay.err(this, "binOp(String s, TFunction n)",
112 "Binary operator named " + s
113 + " has a number of sons equals to "
114 + n.sons.size() + " which is different from 2");
115
116 lib.appendI("");
117
118 n.getChildAt(0).accept(this);
119
120 if (!((n.getChildAt(0)) instanceof TName || (n.getChildAt(0)) instanceof TLiteral)) {
121 lib.appendN("\n");
122 lib.append("");
123 }
124
125 lib.appendN(" " + s + " ");
126 n.getChildAt(1).accept(this);
127
128 if ((n.getChildAt(1)) instanceof TName
129 || (n.getChildAt(1)) instanceof TLiteral)
130 lib.reduceIwNl();
131 else
132 lib.reduceI();
133
134 }
135
136 public void visitTName(/*@ non_null @*/TName n) throws IOException {
137 /*
138 * This call handles everything, ie if n is a variable or a type name
139 */
140 VariableInfo vi = TNode.getVariableInfo(n.name);
141 lib.appendN(vi.getVariableInfo());
142 }
143
144 public void visitTRoot(/*@ non_null @*/TRoot n) throws IOException {
145 for (int i = 0; i <= n.sons.size() - 1; i++)
146 n.getChildAt(i).accept(this);
147 }
148
149 /*
150 * class created using the perl script
151 */
152 public void visitTBoolImplies(/*@ non_null @*/TBoolImplies n) throws IOException {
153 binOp("IMPLIES", n);
154 }
155
156 public void visitTBoolAnd(/*@ non_null @*/TBoolAnd n) throws IOException {
157 genericOp("AND", n);
158 }
159
160 public void visitTBoolOr(/*@ non_null @*/TBoolOr n) throws IOException {
161 genericOp("OR", n);
162 }
163
164 public void visitTBoolNot(/*@ non_null @*/TBoolNot n) throws IOException {
165 unaryGeneric("NOT", n);
166 }
167
168 public void visitTBoolEQ(/*@ non_null @*/TBoolEQ n) throws IOException {
169 genericOp("=", n);
170 }
171
172 public void visitTBoolNE(/*@ non_null @*/TBoolNE n) throws IOException {
173 binOp("/=", n);
174 }
175
176 public void visitTAllocLT(/*@ non_null @*/TAllocLT n) throws IOException {
177 binOp("<", n);
178 }
179
180 public void visitTAllocLE(/*@ non_null @*/TAllocLE n) throws IOException {
181 binOp("<=", n);
182 }
183
184 public void visitTAnyEQ(/*@ non_null @*/TAnyEQ n) throws IOException {
185 genericOp("=", n);
186 }
187
188 public void visitTAnyNE(/*@ non_null @*/TAnyNE n) throws IOException {
189 binOp("/=", n);
190 }
191
192 public void visitTIntegralEQ(/*@ non_null @*/TIntegralEQ n) throws IOException {
193 binOp("=", n);
194 }
195
196 public void visitTIntegralGE(/*@ non_null @*/TIntegralGE n) throws IOException {
197 binOp(">=", n);
198 }
199
200 public void visitTIntegralGT(/*@ non_null @*/TIntegralGT n) throws IOException {
201 binOp(">", n);
202 }
203
204 public void visitTIntegralLE(/*@ non_null @*/TIntegralLE n) throws IOException {
205 binOp("<=", n);
206 }
207
208 public void visitTIntegralLT(/*@ non_null @*/TIntegralLT n) throws IOException {
209 binOp("<", n);
210 }
211
212 public void visitTIntegralNE(/*@ non_null @*/TIntegralNE n) throws IOException {
213 binOp("/=", n);
214 }
215
216 public void visitTIntegralAdd(/*@ non_null @*/TIntegralAdd n) throws IOException {
217 binOp("+", n);
218 }
219
220 public void visitTIntegralDiv(/*@ non_null @*/TIntegralDiv n) throws IOException {
221 binOp("/", n);
222 }
223
224 public void visitTIntegralMod(/*@ non_null @*/TIntegralMod n) throws IOException {
225 binOp("mod", n);
226 }
227
228 public void visitTIntegralMul(/*@ non_null @*/TIntegralMul n) throws IOException {
229 binOp("*", n);
230 }
231
232 public void visitTFloatEQ(/*@ non_null @*/TFloatEQ n) throws IOException {
233 binOp("=", n);
234 }
235
236 public void visitTFloatGE(/*@ non_null @*/TFloatGE n) throws IOException {
237 binOp(">=", n);
238 }
239
240 public void visitTFloatGT(/*@ non_null @*/TFloatGT n) throws IOException {
241 binOp(">", n);
242 }
243
244 public void visitTFloatLE(/*@ non_null @*/TFloatLE n) throws IOException {
245 binOp("<=", n);
246 }
247
248 public void visitTFloatLT(/*@ non_null @*/TFloatLT n) throws IOException {
249 binOp("<", n);
250 }
251
252 public void visitTFloatNE(/*@ non_null @*/TFloatNE n) throws IOException {
253 binOp("/=", n);
254 }
255
256 public void visitTFloatAdd(/*@ non_null @*/TFloatAdd n) throws IOException {
257 binOp("+", n);
258 }
259
260 public void visitTFloatDiv(/*@ non_null @*/TFloatDiv n) throws IOException {
261 binOp("/", n);
262 }
263
264 public void visitTFloatMod(/*@ non_null @*/TFloatMod n) throws IOException {
265 binOp("mod", n);
266 }
267
268 public void visitTFloatMul(/*@ non_null @*/TFloatMul n) throws IOException {
269 binOp("*", n);
270 }
271
272 // FIXME LockLE and LockLT have the same symbol
273 public void visitTLockLE(/*@ non_null @*/TLockLE n) throws IOException {
274 binOp("lockLess", n);
275 }
276
277 public void visitTLockLT(/*@ non_null @*/TLockLT n) throws IOException {
278 binOp("lockLess", n);
279 }
280
281 public void visitTRefEQ(/*@ non_null @*/TRefEQ n) throws IOException {
282 binOp("=", n);
283 }
284
285 public void visitTRefNE(/*@ non_null @*/TRefNE n) throws IOException {
286 binOp("/=", n);
287 }
288
289 public void visitTTypeEQ(/*@ non_null @*/TTypeEQ n) throws IOException {
290 binOp("=", n);
291 }
292
293 public void visitTTypeNE(/*@ non_null @*/TTypeNE n) throws IOException {
294 binOp("/=", n);
295 }
296
297 public void visitTTypeLE(/*@ non_null @*/TTypeLE n) throws IOException {
298 genericFun("subtype?", n); //FIXME, maybe it's extends ? // have to check logics semantics..
299 }
300
301 public void visitTCast(/*@ non_null @*/TCast n) throws IOException {
302 genericFun("cast", n);
303 }
304
305 public void visitTIs(/*@ non_null @*/TIs n) throws IOException {
306
307 /*
308 * As this node should be simplified in TProofSimplifier, we should not be here.
309 */
310 TDisplay.err(this, "visitTIs",
311 "This node should have been simplified in TProofSimplifier");
312
313 /*
314 * As the proof is typed, no need for this operator anymore.
315 * FIXME, handle it in a nicer way.
316 */
317 lib.appendN("TAMERE");
318
319 }
320
321 public void visitTSelect(/*@ non_null @*/TSelect n) throws IOException {
322 genericFun("get", n);
323 }
324
325 public void visitTStore(/*@ non_null @*/TStore n) throws IOException {
326 genericFun("set", n);
327 }
328
329 public void visitTTypeOf(/*@ non_null @*/TTypeOf n) throws IOException {
330 genericFun("typeOf", n);
331 }
332
333 // FIXME not handled atm
334 public void visitTForAll(/*@ non_null @*/TForAll n) throws IOException {
335 lib.appendN("TRUE");
336 }
337
338 public void visitTExist(/*@ non_null @*/TExist n) throws IOException {
339 lib.appendN("TRUE");
340 }
341
342 //
343
344 public void visitTIsAllocated(/*@ non_null @*/TIsAllocated n) throws IOException {
345 genericFun("isAllocated", n);
346 }
347
348 public void visitTEClosedTime(/*@ non_null @*/TEClosedTime n) throws IOException {
349 genericFun("eClosedTime", n);
350 }
351
352 public void visitTFClosedTime(/*@ non_null @*/TFClosedTime n) throws IOException {
353 genericFun("fClosedTime", n);
354 }
355
356 public void visitTAsElems(/*@ non_null @*/TAsElems n) throws IOException {
357 genericFun("asElems", n);
358 }
359
360 public void visitTAsField(/*@ non_null @*/TAsField n) throws IOException {
361 genericFun("asField", n);
362 }
363
364 public void visitTAsLockSet(/*@ non_null @*/TAsLockSet n) throws IOException {
365 genericFun("asLockSet", n);
366 }
367
368 public void visitTArrayLength(/*@ non_null @*/TArrayLength n) throws IOException {
369 }
370
371 public void visitTArrayFresh(/*@ non_null @*/TArrayFresh n) throws IOException {
372 }
373
374 public void visitTArrayShapeOne(/*@ non_null @*/TArrayShapeOne n) throws IOException {
375 }
376
377 public void visitTArrayShapeMore(/*@ non_null @*/TArrayShapeMore n) throws IOException {
378 }
379
380 public void visitTIsNewArray(/*@ non_null @*/TIsNewArray n) throws IOException {
381 }
382
383 public void visitTString(/*@ non_null @*/TString n) throws IOException {
384 }
385
386 public void visitTBoolean(/*@ non_null @*/TBoolean n) throws IOException {
387 if (n.value)
388 lib.appendN("TRUE");
389 else
390 lib.appendN("FALSE");
391 }
392
393 public void visitTChar(/*@ non_null @*/TChar n) throws IOException {
394 lib.appendN(" |C_" + n.value + "|");
395 }
396
397 // "" is added to be able to make this call
398 // without redefining append for each type
399 // It works because of the way the java compiler
400 // handles the + operator
401 public void visitTInt(/*@ non_null @*/TInt n) throws IOException {
402 lib.appendN("" + n.value); //FIXME not sure // seems to be ok
403 }
404
405 public void visitTFloat(/*@ non_null @*/TFloat n) throws IOException {
406 lib.appendN(" |F_" + n.value + "|");
407 }
408
409 public void visitTDouble(/*@ non_null @*/TDouble n) throws IOException {
410 lib.appendN(" |F_" + n.value + "|"); // FIXME
411 }
412
413 public void visitTNull(/*@ non_null @*/TNull n) throws IOException {
414 lib.appendN(" null");
415 }
416
417 public void visitTUnset(/*@non_null*/TUnset n) throws IOException {
418 // TODO Auto-generated method stub
419
420 }
421
422 public void visitTMethodCall(/*@non_null*/TMethodCall call) throws IOException {
423 // TODO Auto-generated method stub
424
425 }
426
427 public void visitTIntegralSub(/*@non_null*/TIntegralSub sub) throws IOException {
428 // TODO Auto-generated method stub
429
430 }
431
432 public void visitTSum(TSum s) {
433 // TODO Auto-generated method stub
434
435 }
436
437 }