001 package escjava.vcGeneration.xml;
002
003 import escjava.vcGeneration.*;
004
005 import java.io.*;
006
007 import org.w3c.dom.*;
008
009 /**
010 * Visitor implementation that generates an XML string conforming to the
011 * DTD <i>escjava/vcGeneration/xml/xmlprover.dtd</i>.
012 *
013 * @author Carl Pulley
014 */
015 class TXmlVisitor extends TVisitor {
016
017 private Document dom;
018 private Element node;
019
020 /**
021 * In this visitor class, the <i>out</i> stream is <b>not</b> used.
022 *
023 * <p>Instead, the <i>node</i> and <i>dom</i> object references are used to pass
024 * back the generated term to calling code.
025 *
026 * @param out this parameter is <b>ignored</b> by this class implementation
027 * @throws IOException
028 */
029 public TXmlVisitor(Writer out) throws IOException {
030 super(out);
031 }
032
033 public void setDocumentNode(Document dom, Element node) {
034 this.dom = dom;
035 this.node = node;
036 }
037
038 private void prop(String tagName, TFunction n) throws IOException {
039 Element propNode = dom.createElement("PROP");
040 Attr nameAttr = dom.createAttribute("name");
041 nameAttr.setValue(tagName);
042 propNode.setAttributeNode(nameAttr);
043 node.appendChild(propNode);
044 Element savedNode = node;
045 node = propNode;
046 for (int index = 0; index < n.sons.size(); index++) {
047 n.getChildAt(index).accept(this);
048 }
049 node = savedNode;
050 }
051 private void quant(String tagName, TFunction n) throws IOException {
052 Element quantNode = dom.createElement("QUANT");
053 Attr nameAttr = dom.createAttribute("name");
054 nameAttr.setValue(tagName);
055 quantNode.setAttributeNode(nameAttr);
056 node.appendChild(quantNode);
057 Element savedNode = node;
058 Element patternNode = dom.createElement("PAT");
059 quantNode.appendChild(patternNode);
060 Element bodyNode = dom.createElement("BODY");
061 quantNode.appendChild(bodyNode);
062 node = quantNode;
063 n.getChildAt(0).accept(this);
064 node = patternNode;
065 n.getChildAt(1).accept(this);
066 node = bodyNode;
067 n.getChildAt(2).accept(this);
068 node = savedNode;
069 }
070
071 private void pred(String tagType, String tagName, TFunction n) throws IOException {
072 Element tagNmNode = dom.createElement("PRED");
073 Attr nameAttr = dom.createAttribute("name");
074 nameAttr.setValue(tagName);
075 tagNmNode.setAttributeNode(nameAttr);
076 if (tagType != null) {
077 Attr typeAttr = dom.createAttribute("type");
078 typeAttr.setValue(tagType);
079 tagNmNode.setAttributeNode(typeAttr);
080 }
081 node.appendChild(tagNmNode);
082 Element savedNode = node;
083 node = tagNmNode;
084 for(int index = 0; index < n.sons.size(); index++) {
085 n.getChildAt(index).accept(this);
086 }
087 node = savedNode;
088 }
089
090 private void term(String tagType, String tagName, TFunction n) throws IOException {
091 Element tagNmNode = dom.createElement("TERM");
092 Attr nameAttr = dom.createAttribute("name");
093 nameAttr.setValue(tagName);
094 tagNmNode.setAttributeNode(nameAttr);
095 if (tagType != null) {
096 Attr typeAttr = dom.createAttribute("type");
097 typeAttr.setValue(tagType);
098 tagNmNode.setAttributeNode(typeAttr);
099 }
100 node.appendChild(tagNmNode);
101 Element savedNode = node;
102 node = tagNmNode;
103 for(int index = 0; index < n.sons.size(); index++) {
104 n.getChildAt(index).accept(this);
105 }
106 node = savedNode;
107 }
108
109 private void xmlValue(String tagType, Object value) throws IOException {
110 Element valueNode = dom.createElement("CONST");
111 Attr typeAttr = dom.createAttribute("type");
112 typeAttr.setValue(tagType);
113 valueNode.setAttributeNode(typeAttr);
114 Attr valueAttr = dom.createAttribute("value");
115 if (value != null) {
116 valueAttr.setValue(value.toString());
117 } else {
118 valueAttr.setValue("null");
119 }
120 valueNode.setAttributeNode(valueAttr);
121 node.appendChild(valueNode);
122 }
123
124 public void visitTName(/*@ non_null @*/TName n) throws IOException {
125 VariableInfo vi = TNode.getVariableInfo(n.name);
126 Element nameNode = dom.createElement("VAR");
127 Attr valueAttr = dom.createAttribute("name");
128 valueAttr.setValue(vi.getVariableInfo());
129 nameNode.setAttributeNode(valueAttr);
130 node.appendChild(nameNode);
131 }
132
133 public void visitTRoot(/*@ non_null @*/TRoot n) throws IOException {
134 for(int index = 0; index < n.sons.size(); index++) {
135 n.getChildAt(index).accept(this);
136 }
137 }
138
139 public void visitTBoolImplies(/*@ non_null @*/TBoolImplies n) throws IOException {
140 prop("IMPLIES", n);
141 }
142
143 public void visitTBoolAnd(/*@ non_null @*/TBoolAnd n) throws IOException {
144 prop("AND", n);
145 }
146
147 public void visitTBoolOr(/*@ non_null @*/TBoolOr n) throws IOException {
148 prop("OR", n);
149 }
150
151 public void visitTBoolNot(/*@ non_null @*/TBoolNot n) throws IOException {
152 prop("NOT", n);
153 }
154
155 public void visitTBoolEQ(/*@ non_null @*/TBoolEQ n) throws IOException {
156 prop("EQ", n);
157 }
158
159 public void visitTBoolNE(/*@ non_null @*/TBoolNE n) throws IOException {
160 prop("NEQ", n);
161 }
162
163 public void visitTAllocLT(/*@ non_null @*/TAllocLT n) throws IOException {
164 pred("alloc", "LT", n);
165 }
166
167 public void visitTAllocLE(/*@ non_null @*/TAllocLE n) throws IOException {
168 pred("alloc", "LE", n);
169 }
170
171 public void visitTAnyEQ(/*@ non_null @*/TAnyEQ n) throws IOException {
172 pred("any", "EQ", n);
173 }
174
175 public void visitTAnyNE(/*@ non_null @*/TAnyNE n) throws IOException {
176 pred("any", "NEQ", n);
177 }
178
179 public void visitTIntegralEQ(/*@ non_null @*/TIntegralEQ n) throws IOException {
180 pred("int", "EQ", n);
181 }
182
183 public void visitTIntegralGE(/*@ non_null @*/TIntegralGE n) throws IOException {
184 pred("int", "GE", n);
185 }
186
187 public void visitTIntegralGT(/*@ non_null @*/TIntegralGT n) throws IOException {
188 pred("int", "GT", n);
189 }
190
191 public void visitTIntegralLE(/*@ non_null @*/TIntegralLE n) throws IOException {
192 pred("int", "LE", n);
193 }
194
195 public void visitTIntegralLT(/*@ non_null @*/TIntegralLT n) throws IOException {
196 pred("int", "LT", n);
197 }
198
199 public void visitTIntegralNE(/*@ non_null @*/TIntegralNE n) throws IOException {
200 pred("int", "NEQ", n);
201 }
202
203 public void visitTIntegralAdd(/*@ non_null @*/TIntegralAdd n) throws IOException {
204 term("int", "ADD", n);
205 }
206
207 public void visitTIntegralDiv(/*@ non_null @*/TIntegralDiv n) throws IOException {
208 term("int", "DIV", n);
209 }
210
211 public void visitTIntegralMod(/*@ non_null @*/TIntegralMod n) throws IOException {
212 term("int", "MOD", n);
213 }
214
215 public void visitTIntegralMul(/*@ non_null @*/TIntegralMul n) throws IOException {
216 term("int", "TIMES", n);
217 }
218
219 public void visitTFloatEQ(/*@ non_null @*/TFloatEQ n) throws IOException {
220 pred("float", "EQ", n);
221 }
222
223 public void visitTFloatGE(/*@ non_null @*/TFloatGE n) throws IOException {
224 pred("float", "GE", n);
225 }
226
227 public void visitTFloatGT(/*@ non_null @*/TFloatGT n) throws IOException {
228 pred("float", "GT", n);
229 }
230
231 public void visitTFloatLE(/*@ non_null @*/TFloatLE n) throws IOException {
232 pred("float", "LE", n);
233 }
234
235 public void visitTFloatLT(/*@ non_null @*/TFloatLT n) throws IOException {
236 pred("float", "GE", n);
237 }
238
239 public void visitTFloatNE(/*@ non_null @*/TFloatNE n) throws IOException {
240 pred("float", "NEQ", n);
241 }
242
243 public void visitTFloatAdd(/*@ non_null @*/TFloatAdd n) throws IOException {
244 term("float", "ADD", n);
245 }
246
247 public void visitTFloatDiv(/*@ non_null @*/TFloatDiv n) throws IOException {
248 term("float", "DIV", n);
249 }
250
251 public void visitTFloatMod(/*@ non_null @*/TFloatMod n) throws IOException {
252 term("float", "MOD", n);
253 }
254
255 public void visitTFloatMul(/*@ non_null @*/TFloatMul n) throws IOException {
256 term("float", "TIMES", n);
257 }
258
259 public void visitTLockLE(/*@ non_null @*/TLockLE n) throws IOException {
260 pred("lock", "LE", n);
261 }
262
263 public void visitTLockLT(/*@ non_null @*/TLockLT n) throws IOException {
264 pred("lock", "LT", n);
265 }
266
267 public void visitTRefEQ(/*@ non_null @*/TRefEQ n) throws IOException {
268 pred("ref", "EQ", n);
269 }
270
271 public void visitTRefNE(/*@ non_null @*/TRefNE n) throws IOException {
272 pred("ref", "NEQ", n);
273 }
274
275 public void visitTTypeEQ(/*@ non_null @*/TTypeEQ n) throws IOException {
276 pred("type", "EQ", n);
277 }
278
279 public void visitTTypeNE(/*@ non_null @*/TTypeNE n) throws IOException {
280 pred("type", "NEQ", n);
281 }
282
283 public void visitTTypeLE(/*@ non_null @*/TTypeLE n) throws IOException {
284 pred("type", "LE", n);
285 }
286
287 public void visitTCast(/*@ non_null @*/TCast n) throws IOException {
288 term(null, "cast", n);
289 }
290
291 public void visitTIs(/*@ non_null @*/TIs n) throws IOException {
292 pred(null, "is", n);
293 }
294
295 public void visitTSelect(/*@ non_null @*/TSelect n) throws IOException {
296 term(null, "select", n);
297 }
298
299 public void visitTStore(/*@ non_null @*/TStore n) throws IOException {
300 term(null, "store", n);
301 }
302
303 public void visitTTypeOf(/*@ non_null @*/TTypeOf n) throws IOException {
304 term(null, "typeof", n);
305 }
306
307 public void visitTForAll(/*@ non_null @*/TForAll n) throws IOException {
308 quant("FORALL", n);
309 }
310
311 public void visitTExist(/*@ non_null @*/TExist n) throws IOException {
312 quant("EXISTS", n);
313 }
314
315 public void visitTIsAllocated(/*@ non_null @*/TIsAllocated n) throws IOException {
316 pred(null, "isAllocated", n);
317 }
318
319 public void visitTEClosedTime(/*@ non_null @*/TEClosedTime n) throws IOException {
320 term(null, "eClosedTime", n);
321 }
322
323 public void visitTFClosedTime(/*@ non_null @*/TFClosedTime n) throws IOException {
324 term(null, "fClosedTime", n);
325 }
326
327 public void visitTAsElems(/*@ non_null @*/TAsElems n) throws IOException {
328 term(null, "asElems", n);
329 }
330
331 public void visitTAsField(/*@ non_null @*/TAsField n) throws IOException {
332 term(null, "asField", n);
333 }
334
335 public void visitTAsLockSet(/*@ non_null @*/TAsLockSet n) throws IOException {
336 term(null, "asLockSet", n);
337 }
338
339 public void visitTArrayLength(/*@ non_null @*/TArrayLength n) throws IOException {
340 term("array", "Length", n);
341 }
342
343 public void visitTArrayFresh(/*@ non_null @*/TArrayFresh n) throws IOException {
344 term("array", "Fresh", n);
345 }
346
347 public void visitTArrayShapeOne(/*@ non_null @*/TArrayShapeOne n) throws IOException {
348 term("array", "ShapeOne", n);
349 }
350
351 public void visitTArrayShapeMore(/*@ non_null @*/TArrayShapeMore n) throws IOException {
352 term("array", "ShapeMore", n);
353 }
354
355 public void visitTIsNewArray(/*@ non_null @*/TIsNewArray n) throws IOException {
356 term(null, "IsNewArray", n);
357 }
358
359 public void visitTString(/*@ non_null @*/TString n) throws IOException {
360 xmlValue("String", n.value);
361 }
362
363 public void visitTBoolean(/*@ non_null @*/TBoolean n) throws IOException {
364 xmlValue("Boolean", new Boolean(n.value));
365 }
366
367 public void visitTChar(/*@ non_null @*/TChar n) throws IOException {
368 xmlValue("Character", new Character(n.value));
369 }
370
371 public void visitTInt(/*@ non_null @*/TInt n) throws IOException {
372 xmlValue("Integer", new Integer(n.value));
373 }
374
375 public void visitTFloat(/*@ non_null @*/TFloat n) throws IOException {
376 xmlValue("Float", new Float(n.value));
377 }
378
379 public void visitTDouble(/*@ non_null @*/TDouble n) throws IOException {
380 xmlValue("Double", new Double(n.value));
381 }
382
383 public void visitTNull(/*@ non_null @*/TNull n) throws IOException {
384 xmlValue("Object", null);
385 }
386
387 public void visitTUnset(/*@non_null*/TUnset n) throws IOException {
388 term(null, "unset", n);
389 }
390
391 public void visitTMethodCall(/*@non_null*/TMethodCall call) throws IOException {
392 term("Method", TNode.prover.getVariableInfo(call.getName()), call);
393 }
394
395 public void visitTIntegralSub(/*@non_null*/TIntegralSub sub) throws IOException {
396 term("int", "SUB", sub);
397 }
398
399 public void visitTSum(TSum s) {
400 // TODO Auto-generated method stub
401
402 }
403
404 }