001 package escjava.vcGeneration;
002
003 import java.io.*;
004 import java.util.Iterator;
005 import java.util.HashMap;
006 import java.util.Set;
007
008 abstract public class TNode {
009
010 /*@
011 @ protected invariant (\forall TNode i,j ; i != j; i.id != j.id);
012 @ protected invariant lastType >= 0 &&
013 @ (typeProofSet ==> (lastType <= 1 && lastType <= 3)) &&
014 @ (isroot ==> (this instanceof TRoot)) && // you probably want this to be <==> [Chalin]
015 @ (parent != null || this instanceof TRoot); // ditto
016 @*/
017
018 // FIXME explain it in the doc
019 static/*@ spec_public @*/protected PrintStream dotPs;
020
021 protected int id;
022
023 static protected int counter = 0;
024
025 protected boolean isroot = false;
026
027 public TypeInfo type = null;
028
029 // internal representation of last type asked
030 static/*@ spec_public @*/protected int lastType = 0;
031
032 static/*@ spec_public @*/protected boolean typeProofSet = false;
033
034 public TFunction parent = null;
035
036 String label = null;
037
038 /** map containing the variables names
039 * When the tree is created, old name are entered as keys with
040 * a new {@link VariableInfo}(oldName, type) associated as value.
041 * When the vc are generated, each time a variable is looked at, we look
042 * at this map. We look into the {@link VariableInfo} object associated.
043 * If the renaming hasn't been done into this object, we do it.
044 * If present, we use the already existing name.
045 * Thus we will only rename one time and use previous value for next acccess.
046 *
047 * It handles multiple renaming because each {@link VariableInfo} object contains
048 * multiples fields for renaming (take a look at it).
049 */
050 static/*@ spec_public non_null @*/protected HashMap variablesName = null;
051
052 /**
053 * map containing all the types used in the proof.
054 *
055 * After calling {@link typeTree}, each node has his {@link TypeInfo} field
056 * not null. It points on a TypeInfo object which is a value of this HashMap.
057 * Each TypeInfo object contains the old type, the pvs corresponding type,
058 * and the sammy corresponding type.
059 * The old type can be {reference, integer, boolean, type}.
060 * The tree is typechecked after call to {@link SetOutputType} and
061 * this map is filled with only the type asked.
062 * Ie if you call setOutputType("unsortedPvs"), the tree will be typed
063 * with the old type and the types for the unsorted logic of pvs.
064 * If you make another call to setOutputType, it will add type the tree
065 * for the new tree etc...
066 */
067 static public/* spec_public */ /*@ non_null @*//* protected */HashMap typesName = null;
068
069 /**
070 * We add some types that we know will be used to avoid looking
071 * at the map typesName when we want to add it.
072 */
073 static public TypeInfo _Reference = null;
074
075 static public TypeInfo _Type = null;
076
077 static public TypeInfo _DOUBLETYPE = null;
078
079 static public TypeInfo _boolean = null;
080
081 static public TypeInfo _char = null;
082
083 static public TypeInfo _double = null;
084
085 static public TypeInfo _Field = null;
086
087 static public TypeInfo _INTTYPE = null;
088
089 static public TypeInfo _integer = null;
090
091 static public TypeInfo _float = null;
092
093 static public TypeInfo _String = null;
094
095 static public TypeInfo _Time = null;
096
097 static public TypeInfo _Path = null;
098
099 public TNode() {
100
101 // FIXME :)
102 //@ assert false;
103
104 counter += 1;
105 id = counter;
106 }
107
108 static public ProverType prover = null;
109
110 // init every both variable and type map.
111
112 static public void init(ProverType prover) {
113 TNode.prover = prover;
114
115 typesName = new HashMap();
116 variablesName = new HashMap();
117
118 prover.init();
119 }
120
121 protected void generateDeclarations(/*@ non_null @*/Writer s, ProverType p) throws IOException {
122 p.generateDeclarations(s, variablesName);
123 }
124
125 /**
126 * This function add variable to the global map name.
127 * @param oldName the old name.
128 * @param type the type of the variable which has been infered from the old tree.
129 *
130 * @return the VariableInfo object representing this variables name
131 */
132 /*@
133 @ ensures variablesName.containsKey(oldName);
134 @*/
135 static public/*@ non_null @*/VariableInfo addName(/*@ non_null @*/String oldName, /*@ non_null @*/String type, String def) {
136
137 if (!variablesName.containsKey(oldName)) {
138 // we will do the renaming when necessary (look at {@link VariableInfo})
139
140 TypeInfo ti = null;
141
142 /*
143 * We retrieve the type if necessary.
144 */
145 if (type != null)
146 ti = TNode.addType(type);
147 else
148 TDisplay.warn("TNode", "addName", "Adding variable named "
149 + oldName + " with no types");
150
151 //@ assert typesName.containsKey(type);
152 variablesName.put(oldName, new VariableInfo(oldName, ti, def, prover));
153 }
154 //++
155 else {
156
157 // debugging stuff that checks the new type is the same as the previous on
158 if (type != null) {
159
160 VariableInfo vi = (VariableInfo) variablesName.get(oldName);
161 if (vi.type != typesName.get(type)) {
162
163 TDisplay
164 .warn(
165 "TNode",
166 "addName",
167 "You're trying to add a variable named "
168 + oldName
169 + " whith type "
170 + type.toString()
171 + " which has been already stored with the type "
172 + vi.type.toString()
173 + " to the proof tree");
174 }
175 }
176
177 }
178
179 //@ assert variablesName.containsKey(oldName);
180
181 /* we return the node which represents this variable.
182 * Note that if this oldName wasn't present in the hashMap
183 * the node returned is the one added created with TName node = new TName(oldName);
184 */
185 return (VariableInfo) variablesName.get(oldName);
186
187 //++
188 }
189
190 static public/*@ non_null @*/VariableInfo addName(/*@ non_null @*/String oldName, /*@ non_null @*/String type) {
191 return addName(oldName, type, null);
192 }
193
194 /**
195 * return the {@link VariableInfo} object associated with this name
196 */
197 // xxx requires variablesName.contains(s); //prj 15may2006 s not defined in this context
198 static public/*@ non_null @*/VariableInfo getVariableInfo(/*@ non_null @*/String name) {
199 return (VariableInfo) variablesName.get(name);
200 }
201
202 /**
203 * return the {@link VariableInfo} object associated of the caller which
204 * must be an instance of TName.
205 */
206 // xxx requires variablesName.contains(s); //prj 15may2006 s not defined in this context
207 /*@ non_null @*/VariableInfo getVariableInfo() {
208
209 //@ assert this instanceof TName;
210
211 if (!(this instanceof TName)) {
212 TDisplay.err(this, "getVariableInfo()",
213 "Warning calling getVariableInfo on a non TName Node");
214 return null;
215 } else {
216 TName n = (TName) this;
217 return getVariableInfo(n.name);
218 }
219
220 }
221
222 /**
223 * This function add type to the global map .
224 * @param oldName the old name.
225 *
226 * @return the node pointing on that variable (can already exist if this add is
227 * useless, in this case we return the previous TypeInfo representing this type).
228 */
229 /*@
230 @ ensures typesName.containsKey(oldType);
231 @*/
232 static public/*@ non_null @*/TypeInfo addType(/*@ non_null @*/String oldType, String def) {
233
234 if (!typesName.containsKey(oldType)) {
235 // we will do the renaming when necessary (look at {@link TypeInfo})
236
237 TypeInfo ti = new TypeInfo(oldType, def, prover);
238 typesName.put(oldType, ti);
239
240 //@ assert typesName.containsKey(oldType);
241
242 return ti;
243 } else {
244 //@ assert typesName.containsKey(oldType);
245
246 return (TypeInfo) typesName.get(oldType);
247 }
248
249 }
250
251 static public/*@ non_null @*/TypeInfo addType(/*@ non_null @*/String oldType) {
252 return TNode.addType(oldType, null);
253 }
254
255 /** dot id which is unique because of adding
256 'id' to the name of the node */
257 protected/*@ non_null @*/String dotId() {
258
259 /* escjava.vcGeneration.Tabc => r = abc */
260 String r = getClass().getName().substring(22);
261 r = r + id;
262
263 return r;
264 }
265
266 // to avoid printing eachtime 'escjava.dsaParser.' and remove first 'T'
267 protected/*@ pure non_null @*/String getShortName() {
268 return getClass().getName().substring(22);
269 }
270
271 /*@
272 @ requires typeProofSet;
273 @ ensures type != null;
274 @*/
275 abstract protected void typeTree();
276
277 /**
278 * Add the type if not present to the global map of type
279 * and fill the correct field with it.
280 */
281 protected void setType(String s, boolean sure) {
282 type = TNode.addType(s);
283 }
284
285
286 protected void setType(TypeInfo type, boolean sure) {
287
288 if (this instanceof TName) {
289 TName m = (TName) this;
290
291 //@ assert m.type == null;
292
293 // retrieve current type;
294 if (!variablesName.containsKey(m.name)) {
295 TDisplay
296 .err(
297 this,
298 "setType(TypeInfo, boolean)",
299 "You're manipulating a TName ("
300 + m.name
301 + ") node, yet the name isn't in the global map 'variablesName'");
302 }
303 // take care no else here
304
305 VariableInfo vi = (VariableInfo) variablesName.get(m.name);
306
307 if (vi.type == null) {// we set it
308 vi.type = type;
309 } else {
310 if (vi.type != type) {// inconsistency
311 if (vi.typeSure) // we don't change it
312 TDisplay.err(this, "setType(TypeInfo, boolean)",
313 "Variable named " + m.name + ", has type "
314 + vi.type.old
315 + " yet you try to change it to "
316 + type.old);
317 else {
318 TDisplay.warn(this, "setType(TypeInfo, boolean)",
319 "Changing type of " + m.name + " (which was "
320 + vi.type.old + ") to " + type.old);
321 vi.type = type;
322 }
323 }
324
325 }
326 } else {
327 if (this.type != null) {
328 // we compare the existing type
329 if (this.type != type) { // The two types are not equals
330 // inconsistancy
331 TDisplay.warn(this, "setType(TypeInfo, boolean)",
332 "Typechecking inconsistancy, " + this.toString()
333 + "has type " + this.type.old
334 + "but you're trying to set his type to "
335 + type.old);
336 }
337 } else
338 // type is null que pasa ?
339 TDisplay.err(this, "setType(TypeInfo, boolean)", "Node "
340 + this.toString() + " has no type");
341
342 }
343 }
344
345 /**
346 * return the type of the node according to the type of proof asked
347 * or "?" if type isn't known.
348 */
349 /*@
350 @ requires typeProofSet;
351 @*/
352 public/*@ non_null @*/String getType() {
353
354 if (this instanceof TName) {
355 // retrieve the type in the global variablesNames map
356 TName m = (TName) this;
357
358 //@ assert m.type == null;
359
360 // retrieve current type;
361 if (!variablesName.containsKey(m.name)) {
362 TDisplay
363 .err(
364 this,
365 "getType",
366 "You're manipulating a TName ("
367 + m.name
368 + ") node, yet the name isn't in the global map 'variablesName'");
369 }
370 // take care no else here
371
372 VariableInfo vi = (VariableInfo) variablesName.get(m.name);
373
374 if (vi.type == null)
375 return "?";
376 else {
377 TypeInfo ti = vi.type;
378
379 String result = "";
380 /*
381 * Handle double type here
382 */
383 if (ti == _Field) { // variables may have a second type;
384 if (vi.getSecondType() != null) {
385
386 /*
387 * FIXME : explanations needed here, tricky stuff.
388 */
389
390 TypeInfo ti2 = vi.getSecondType();
391 VariableInfo vi2 = getVariableInfo(ti2.old);
392
393 result = vi2.getVariableInfo() + "\\n";
394
395 }
396
397 }
398
399 result = result + ti.getTypeInfo();
400
401 return result;
402 }
403
404 } else {
405 if (this.type == null)
406 return "?";
407
408 return this.type.getTypeInfo();
409 }
410
411 }
412
413 /**
414 * Return the typeInfo associated with this node. It can just be
415 * the 'type' field for non instance of TName. Or in the case
416 * of TName node, we retrieve it in the global map.
417 */
418 public TypeInfo getTypeInfo() {
419
420 if (!(this instanceof TName))
421 return this.type;
422 else { //retrieve the type in the map
423
424 TName m = (TName) this;
425
426 //@ assert m.type == null;
427
428 // retrieve current type;
429 if (!variablesName.containsKey(m.name)) {
430 TDisplay
431 .err(
432 this,
433 "getType",
434 "You're manipulating a TName ("
435 + m.name
436 + ") node, yet the name isn't in the global map 'variablesName'");
437 }
438 // take care no else here
439
440 VariableInfo vi = (VariableInfo) variablesName.get(m.name);
441
442 //++
443 // if(vi.type != null)
444 // System.out.println("returning "+vi.type.old+" for "+this.toString());
445 //++
446
447 // can be null
448 return vi.type;
449 }
450
451 }
452
453 public /*@non_null*/ String toString() {
454 if (type != null)
455 return getShortName() + id + ", " + type.old;
456 else
457 return getShortName() + id;
458 }
459
460 abstract public void accept(/*@ non_null @*/TVisitor v) throws IOException;
461
462 static public void printInfo() {
463
464 // print all variables and their renaming in a 'nice' way
465 Set keySet = variablesName.keySet();
466
467 Iterator iter = keySet.iterator();
468 String keyTemp = null;
469 VariableInfo viTemp = null;
470
471 System.out.println("\n=== List of variables ===");
472 System.out
473 .println("[oldName, newName : oldType]\n");
474
475 while (iter.hasNext()) {
476
477 try {
478 keyTemp = (String) iter.next();
479 } catch (Exception e) {
480 System.err.println(e.getMessage());
481 }
482 viTemp = (VariableInfo) variablesName.get(keyTemp);
483
484 /* output informations in this format : oldName, pvsUnsortedName,
485 * pvsName, sammyName, type.
486 */
487 if (viTemp.type != null) // FIXME
488 System.out.println("[" + viTemp.old + ", " + viTemp.getVariableInfo() + " : "
489 + viTemp.type.old + "]");
490 else
491 System.out.println("[" + viTemp.old + ", " + viTemp.getVariableInfo()
492 + " : ?type? ]");
493 }
494
495 keySet = typesName.keySet();
496 iter = keySet.iterator();
497 TypeInfo tiTemp = null;
498
499 System.out.println("\n=== List of type ===");
500 System.out.println("[old, new]\n");
501
502 while (iter.hasNext()) {
503
504 try {
505 keyTemp = (String) iter.next();
506 } catch (Exception e) {
507 System.err.println(e.getMessage());
508 }
509 tiTemp = (TypeInfo) typesName.get(keyTemp);
510
511 /* output informations in this format : old, pvsUnsorted,
512 * pvs, sammy.
513 */
514
515 System.out.println("[" + tiTemp.old + ", " + tiTemp.getTypeInfo() + "]");
516 }
517
518 System.out.print("\n");
519 }
520 }