Method: caseARepeatTraceDeclIR(ARepeatTraceDeclIR)

1: package org.overture.codegen.traces;
2:
3: import java.util.LinkedList;
4: import java.util.List;
5: import java.util.Set;
6:
7: import org.apache.log4j.Logger;
8: import org.overture.ast.definitions.SFunctionDefinition;
9: import org.overture.ast.definitions.SOperationDefinition;
10: import org.overture.ast.lex.Dialect;
11: import org.overture.ast.statements.ACallStm;
12: import org.overture.codegen.assistant.DeclAssistantIR;
13: import org.overture.codegen.assistant.ExpAssistantIR;
14: import org.overture.codegen.ir.INode;
15: import org.overture.codegen.ir.IRConstants;
16: import org.overture.codegen.ir.IRInfo;
17: import org.overture.codegen.ir.SExpIR;
18: import org.overture.codegen.ir.SStmIR;
19: import org.overture.codegen.ir.STraceDeclIR;
20: import org.overture.codegen.ir.STypeIR;
21: import org.overture.codegen.ir.SourceNode;
22: import org.overture.codegen.ir.analysis.AnalysisException;
23: import org.overture.codegen.ir.analysis.AnswerAdaptor;
24: import org.overture.codegen.ir.analysis.DepthFirstAnalysisAdaptor;
25: import org.overture.codegen.ir.declarations.AFieldDeclIR;
26: import org.overture.codegen.ir.declarations.AMethodDeclIR;
27: import org.overture.codegen.ir.declarations.AVarDeclIR;
28: import org.overture.codegen.ir.declarations.SClassDeclIR;
29: import org.overture.codegen.ir.expressions.AAnonymousClassExpIR;
30: import org.overture.codegen.ir.expressions.AApplyExpIR;
31: import org.overture.codegen.ir.expressions.ACastUnaryExpIR;
32: import org.overture.codegen.ir.expressions.AExplicitVarExpIR;
33: import org.overture.codegen.ir.expressions.AFieldExpIR;
34: import org.overture.codegen.ir.expressions.AIdentifierVarExpIR;
35: import org.overture.codegen.ir.expressions.AIntLiteralExpIR;
36: import org.overture.codegen.ir.expressions.ANewExpIR;
37: import org.overture.codegen.ir.expressions.ATypeArgExpIR;
38: import org.overture.codegen.ir.name.ATypeNameIR;
39: import org.overture.codegen.ir.patterns.AIdentifierPatternIR;
40: import org.overture.codegen.ir.patterns.ASetMultipleBindIR;
41: import org.overture.codegen.ir.statements.ABlockStmIR;
42: import org.overture.codegen.ir.statements.ACallObjectExpStmIR;
43: import org.overture.codegen.ir.statements.APlainCallStmIR;
44: import org.overture.codegen.ir.statements.AReturnStmIR;
45: import org.overture.codegen.ir.statements.ASkipStmIR;
46: import org.overture.codegen.ir.statements.SCallStmIR;
47: import org.overture.codegen.ir.traces.AApplyExpTraceCoreDeclIR;
48: import org.overture.codegen.ir.traces.ABracketedExpTraceCoreDeclIR;
49: import org.overture.codegen.ir.traces.AConcurrentExpTraceCoreDeclIR;
50: import org.overture.codegen.ir.traces.ALetBeStBindingTraceDeclIR;
51: import org.overture.codegen.ir.traces.ALetDefBindingTraceDeclIR;
52: import org.overture.codegen.ir.traces.ARepeatTraceDeclIR;
53: import org.overture.codegen.ir.traces.ATraceDeclTermIR;
54: import org.overture.codegen.ir.types.ABoolBasicTypeIR;
55: import org.overture.codegen.ir.types.AClassTypeIR;
56: import org.overture.codegen.ir.types.AExternalTypeIR;
57: import org.overture.codegen.ir.types.AMethodTypeIR;
58: import org.overture.codegen.ir.types.AObjectTypeIR;
59: import org.overture.codegen.ir.types.AVoidTypeIR;
60: import org.overture.codegen.ir.types.SSetTypeIR;
61: import org.overture.codegen.trans.assistants.TransAssistantIR;
62: import org.overture.config.Settings;
63:
64: public class TraceStmBuilder extends AnswerAdaptor<TraceNodeData>
65: {
66:         protected String traceEnclosingClass;
67:         protected StoreAssistant storeAssistant;
68:         protected TracesTrans traceTrans;
69:
70:         protected Logger log = Logger.getLogger(this.getClass().getName());
71:
72:         public TraceStmBuilder(TracesTrans traceTrans, String traceEnclosingClass,
73:                         StoreAssistant storeAssist)
74:         {
75:                 this.traceTrans = traceTrans;
76:                 this.traceEnclosingClass = traceEnclosingClass;
77:                 this.storeAssistant = storeAssist;
78:         }
79:
80:         public IRInfo getInfo()
81:         {
82:                 return getTransAssist().getInfo();
83:         }
84:
85:         @Override
86:         public TraceNodeData caseATraceDeclTermIR(ATraceDeclTermIR node)
87:                         throws AnalysisException
88:         {
89:                 String name = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().altTraceNodeNamePrefix());
90:                 AClassTypeIR classType = getTransAssist().consClassType(traceTrans.getTracePrefixes().altTraceNodeNodeClassName());
91:
92:                 if (node.getTraceDecls().size() == 1)
93:                 {
94:                         return node.getTraceDecls().getFirst().apply(this);
95:                 }
96:                 {
97:                         AVarDeclIR altTests = getTransAssist().consDecl(name, classType, getTransAssist().consDefaultConsCall(classType));
98:
99:                         ABlockStmIR stms = new ABlockStmIR();
100:                         stms.getLocalDefs().add(altTests);
101:
102:                         List<SStmIR> addStms = new LinkedList<SStmIR>();
103:
104:                         for (STraceDeclIR traceDecl : node.getTraceDecls())
105:                         {
106:                                 TraceNodeData nodeData = traceDecl.apply(this);
107:
108:                                 stms.getStatements().add(nodeData.getStms());
109:                                 addStms.add(getTransAssist().consInstanceCallStm(classType, name, traceTrans.getTracePrefixes().addMethodName(), nodeData.getNodeVar()));
110:                         }
111:
112:                         stms.getStatements().addAll(addStms);
113:
114:                         return new TraceNodeData(getInfo().getExpAssistant().consIdVar(name, classType.clone()), stms, stms);
115:                 }
116:         }
117:
118:         @Override
119:         public TraceNodeData caseAApplyExpTraceCoreDeclIR(
120:                         AApplyExpTraceCoreDeclIR node) throws AnalysisException
121:         {
122:                 List<AVarDeclIR> argDecls = replaceArgsWithVars(node.getCallStm());
123:
124:                 String classTypeName;
125:
126:                 if (Settings.dialect != Dialect.VDM_SL)
127:                 {
128:                         classTypeName = traceTrans.getTracePrefixes().callStmClassTypeName();
129:                 } else
130:                 {
131:                         classTypeName = traceTrans.getTracePrefixes().callStmBaseClassTypeName();
132:                 }
133:
134:                 AClassTypeIR callStmType = getTransAssist().consClassType(classTypeName);
135:                 String callStmName = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().callStmNamePrefix());
136:                 AAnonymousClassExpIR callStmCreation = new AAnonymousClassExpIR();
137:                 callStmCreation.setType(callStmType);
138:
139:                 AMethodDeclIR typeCheckMethod = consTypeCheckMethod(node.getCallStm().clone());
140:
141:                 if (typeCheckMethod != null)
142:                 {
143:                         callStmCreation.getMethods().add(typeCheckMethod);
144:                 }
145:
146:                 AMethodDeclIR preCondMethod = condMeetsPreCondMethod(node.getCallStm().clone());
147:
148:                 if (preCondMethod != null)
149:                 {
150:                         callStmCreation.getMethods().add(preCondMethod);
151:                 }
152:
153:                 callStmCreation.getMethods().add(consExecuteMethod(node.getCallStm().clone()));
154:                 callStmCreation.getMethods().add(traceTrans.getToStringBuilder().consToString(getInfo(), node.getCallStm(), storeAssistant.getIdConstNameMap(), storeAssistant, getTransAssist()));
155:                 AVarDeclIR callStmDecl = getTransAssist().consDecl(callStmName, callStmType.clone(), callStmCreation);
156:
157:                 AClassTypeIR stmTraceNodeType = getTransAssist().consClassType(traceTrans.getTracePrefixes().stmTraceNodeClassName());
158:                 ANewExpIR newStmTraceNodeExp = getTransAssist().consDefaultConsCall(stmTraceNodeType);
159:                 newStmTraceNodeExp.getArgs().add(getInfo().getExpAssistant().consIdVar(callStmName, callStmType.clone()));
160:
161:                 String stmNodeName = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().stmTraceNodeNamePrefix());
162:                 AVarDeclIR stmNodeDecl = getTransAssist().consDecl(stmNodeName, stmTraceNodeType.clone(), newStmTraceNodeExp);
163:
164:                 ABlockStmIR decls = new ABlockStmIR();
165:
166:                 if (!argDecls.isEmpty())
167:                 {
168:                         decls.getLocalDefs().addAll(argDecls);
169:                 }
170:
171:                 decls.getLocalDefs().add(callStmDecl);
172:                 decls.getLocalDefs().add(stmNodeDecl);
173:
174:                 return new TraceNodeData(getInfo().getExpAssistant().consIdVar(stmNodeName, stmTraceNodeType.clone()), decls, decls);
175:         }
176:
177:         @Override
178:         public TraceNodeData caseABracketedExpTraceCoreDeclIR(
179:                         ABracketedExpTraceCoreDeclIR node) throws AnalysisException
180:         {
181:                 return buildFromDeclTerms(node.getTerms());
182:         }
183:
184:         @Override
185:         public TraceNodeData caseAConcurrentExpTraceCoreDeclIR(
186:                         AConcurrentExpTraceCoreDeclIR node) throws AnalysisException
187:         {
188:                 String name = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().concTraceNodeNamePrefix());
189:
190:                 AClassTypeIR classType = getTransAssist().consClassType(traceTrans.getTracePrefixes().concTraceNodeNodeClassName());
191:
192:                 AVarDeclIR concNodeDecl = getTransAssist().consDecl(name, classType, getTransAssist().consDefaultConsCall(classType));
193:
194:                 ABlockStmIR stms = new ABlockStmIR();
195:                 stms.getLocalDefs().add(concNodeDecl);
196:
197:                 List<SStmIR> addStms = new LinkedList<SStmIR>();
198:
199:                 // The number of declarations is > 1
200:                 for (STraceDeclIR term : node.getDecls())
201:                 {
202:                         TraceNodeData nodeData = term.apply(this);
203:                         AIdentifierVarExpIR var = nodeData.getNodeVar();
204:                         nodeData.getNodeVarScope().getStatements().add(getTransAssist().consInstanceCallStm(classType, name, traceTrans.getTracePrefixes().addMethodName(), var));
205:
206:                         stms.getStatements().add(nodeData.getStms());
207:                 }
208:
209:                 stms.getStatements().addAll(addStms);
210:
211:                 return new TraceNodeData(getInfo().getExpAssistant().consIdVar(name, classType.clone()), stms, stms);
212:         }
213:
214:         @Override
215:         public TraceNodeData caseALetBeStBindingTraceDeclIR(
216:                         ALetBeStBindingTraceDeclIR node) throws AnalysisException
217:         {
218:                 ASetMultipleBindIR bind = node.getBind();
219:
220:                 IdentifierPatternCollector idCollector = new IdentifierPatternCollector();
221:                 idCollector.setTopNode(bind);
222:
223:                 if (Settings.dialect != Dialect.VDM_SL)
224:                 {
225:                         List<AIdentifierPatternIR> patterns = idCollector.findOccurences();
226:
227:                         for (AIdentifierPatternIR p : patterns)
228:                         {
229:                                 String idConstName = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().idConstNamePrefix());
230:                                 storeAssistant.getIdConstNameMap().put(((AIdentifierPatternIR) p).getName(), idConstName);
231:                         }
232:                 }
233:
234:                 String name = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().altTraceNodeNamePrefix());
235:
236:                 AClassTypeIR classType = getTransAssist().consClassType(traceTrans.getTracePrefixes().altTraceNodeNodeClassName());
237:
238:                 AIdentifierPatternIR id = getInfo().getPatternAssistant().consIdPattern(name);
239:
240:                 AVarDeclIR altTests = getTransAssist().consDecl(name, classType, getTransAssist().consDefaultConsCall(classType));
241:
242:                 STraceDeclIR body = node.getBody();
243:                 SExpIR exp = node.getStExp();
244:
245:                 TraceNodeData bodyTraceData = body.apply(this);
246:
247:                 SSetTypeIR setType = getTransAssist().getSetTypeCloned(bind.getSet());
248:                 TraceLetBeStStrategy strategy = new TraceLetBeStStrategy(getTransAssist(), exp, setType, traceTrans.getLangIterator(), getInfo().getTempVarNameGen(), traceTrans.getIteVarPrefixes(), storeAssistant, storeAssistant.getIdConstNameMap(), traceTrans.getTracePrefixes(), id, altTests, bodyTraceData, this);
249:
250:                 if (getTransAssist().hasEmptySet(bind))
251:                 {
252:                         getTransAssist().cleanUpBinding(bind);
253:
254:                         ABlockStmIR skip = getTransAssist().wrap(new ASkipStmIR());
255:                         return new TraceNodeData(null, skip, skip);
256:                 }
257:
258:                 ABlockStmIR outerBlock = getTransAssist().consIterationBlock(node.getBind().getPatterns(), bind.getSet(), getInfo().getTempVarNameGen(), strategy, traceTrans.getIteVarPrefixes());
259:
260:                 return new TraceNodeData(getInfo().getExpAssistant().consIdVar(name, classType.clone()), outerBlock, outerBlock);
261:         }
262:
263:         @Override
264:         public TraceNodeData caseALetDefBindingTraceDeclIR(
265:                         ALetDefBindingTraceDeclIR node) throws AnalysisException
266:         {
267:                 ABlockStmIR outer = new ABlockStmIR();
268:                 outer.setScoped(true);
269:
270:                 IdentifierPatternCollector idCollector = new IdentifierPatternCollector();
271:
272:                 ABlockStmIR declBlock = new ABlockStmIR();
273:
274:                 List<AIdentifierVarExpIR> traceVars = new LinkedList<>();
275:
276:                 for (AVarDeclIR dec : node.getLocalDefs())
277:                 {
278:                         // Find types for all sub patterns
279:                         PatternTypeFinder typeFinder = new PatternTypeFinder(getInfo());
280:                         dec.getPattern().apply(typeFinder, dec.getType());
281:
282:                         idCollector.setTopNode(dec);
283:                         List<AIdentifierPatternIR> idOccurences = idCollector.findOccurences();
284:
285:                         AVarDeclIR decCopy = dec.clone();
286:                         decCopy.setFinal(true);
287:                         declBlock.getLocalDefs().add(decCopy);
288:
289:                         for (AIdentifierPatternIR occ : idOccurences)
290:                         {
291:                                 if (Settings.dialect != Dialect.VDM_SL)
292:                                 {
293:                                         String idConstName = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().idConstNamePrefix());
294:                                         storeAssistant.getIdConstNameMap().put(occ.getName(), idConstName);
295:                                         outer.getLocalDefs().add(storeAssistant.consIdConstDecl(idConstName));
296:                                         storeAssistant.appendStoreRegStms(declBlock, occ.getName(), idConstName, false);
297:                                 }
298:
299:                                 traceVars.add(getInfo().getExpAssistant().consIdVar(occ.getName(), PatternTypeFinder.getType(typeFinder, occ)));
300:                         }
301:                 }
302:
303:                 TraceNodeData bodyNodeData = node.getBody().apply(this);
304:
305:                 for (int i = traceVars.size() - 1; i >= 0; i--)
306:                 {
307:                         AIdentifierVarExpIR a = traceVars.get(i);
308:
309:                         ACallObjectExpStmIR addVar = consAddTraceVarCall(bodyNodeData.getNodeVar(), a);
310:                         ensureStoreLookups(addVar);
311:                         bodyNodeData.getNodeVarScope().getStatements().add(addVar);
312:                 }
313:
314:                 outer.getStatements().add(declBlock);
315:                 outer.getStatements().add(bodyNodeData.getStms());
316:
317:                 return new TraceNodeData(bodyNodeData.getNodeVar(), outer, bodyNodeData.getNodeVarScope());
318:         }
319:
320:         @Override
321:         public TraceNodeData caseARepeatTraceDeclIR(ARepeatTraceDeclIR node)
322:                         throws AnalysisException
323:         {
324:                 Long from = node.getFrom();
325:                 Long to = node.getTo();
326:
327:•                if (from == 1 && to == 1)
328:                 {
329:                         return node.getCore().apply(this);
330:                 } else
331:                 {
332:                         String name = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().repeatTraceNodeNamePrefix());
333:
334:                         TraceNodeData traceData = node.getCore().apply(this);
335:
336:                         AIdentifierVarExpIR varArg = traceData.getNodeVar();
337:                         AIntLiteralExpIR fromArg = getInfo().getExpAssistant().consIntLiteral(from);
338:                         AIntLiteralExpIR toArg = getInfo().getExpAssistant().consIntLiteral(to);
339:
340:                         AClassTypeIR repeat = getTransAssist().consClassType(traceTrans.getTracePrefixes().repeatTraceNodeNamePrefix());
341:
342:                         ABlockStmIR block = new ABlockStmIR();
343:                         block.getStatements().add(traceData.getStms());
344:                         block.getStatements().add(consDecl(traceTrans.getTracePrefixes().repeatTraceNodeNodeClassName(), name, varArg, fromArg, toArg));
345:
346:                         return new TraceNodeData(getInfo().getExpAssistant().consIdVar(name, repeat), block, block);
347:                 }
348:         }
349:
350:         /**
351:          * Assumes dialect is VDM-SL. This method does not work with store lookups for local variables and since code
352:          * generated VDM-SL traces do not rely on this then it is safe to use this method for this dialect.
353:          *
354:          * @param callStm
355:          * the call statement for which we want to replace the arguments with variables
356:          * @return the variable declarations corresponding to the variables that replace the arguments
357:          */
358:         protected List<AVarDeclIR> replaceArgsWithVars(SStmIR callStm)
359:         {
360:                 List<AVarDeclIR> decls = new LinkedList<AVarDeclIR>();
361:
362:                 if (Settings.dialect != Dialect.VDM_SL)
363:                 {
364:                         return decls;
365:                 }
366:
367:                 List<SExpIR> args = null;
368:
369:                 if (callStm instanceof SCallStmIR)
370:                 {
371:                         args = ((SCallStmIR) callStm).getArgs();
372:                 } else if (callStm instanceof ACallObjectExpStmIR)
373:                 {
374:                         args = ((ACallObjectExpStmIR) callStm).getArgs();
375:                 } else
376:                 {
377:                         log.error("Expected a call statement or call object statement. Got: "
378:                                         + callStm);
379:                         return decls;
380:                 }
381:
382:                 for (SExpIR arg : args)
383:                 {
384:                         String argName = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().callStmArgNamePrefix());
385:                         STypeIR type = arg.getType();
386:
387:                         AVarDeclIR argDecl = getTransAssist().consDecl(argName, type.clone(), arg.clone());
388:                         argDecl.setFinal(true);
389:                         decls.add(argDecl);
390:
391:                         getTransAssist().replaceNodeWith(arg, getInfo().getExpAssistant().consIdVar(argName, type.clone()));
392:                 }
393:
394:                 return decls;
395:         }
396:
397:         protected AMethodDeclIR consExecuteMethod(SStmIR stm)
398:         {
399:                 AMethodTypeIR methodType = new AMethodTypeIR();
400:                 methodType.setResult(new AObjectTypeIR());
401:
402:                 AMethodDeclIR execMethod = new AMethodDeclIR();
403:                 execMethod.setImplicit(false);
404:                 execMethod.setAbstract(false);
405:                 execMethod.setAccess(IRConstants.PUBLIC);
406:                 execMethod.setAsync(false);
407:                 execMethod.setIsConstructor(false);
408:                 execMethod.setMethodType(methodType);
409:                 execMethod.setName(traceTrans.getTracePrefixes().callStmExecMethodNamePrefix());
410:                 execMethod.setStatic(false);
411:
412:                 ABlockStmIR body = new ABlockStmIR();
413:                 body.getStatements().add(makeInstanceCall(stm));
414:
415:                 ensureStoreLookups(body);
416:
417:                 execMethod.setBody(body);
418:
419:                 return execMethod;
420:         }
421:
422:         protected void ensureStoreLookups(SStmIR body)
423:         {
424:                 if (Settings.dialect == Dialect.VDM_SL)
425:                 {
426:                         return;
427:                 }
428:
429:                 try
430:                 {
431:                         final Set<String> localVarNames = storeAssistant.getIdConstNameMap().keySet();
432:
433:                         body.apply(new DepthFirstAnalysisAdaptor()
434:                         {
435:                                 // No need to consider explicit variables because they cannot be local
436:
437:                                 @Override
438:                                 public void caseAIdentifierVarExpIR(AIdentifierVarExpIR node)
439:                                                 throws AnalysisException
440:                                 {
441:                                         if (localVarNames.contains(node.getName()))
442:                                         {
443:                                                 getTransAssist().replaceNodeWith(node, storeAssistant.consStoreLookup(node));
444:                                         }
445:                                 }
446:                         });
447:
448:                 } catch (AnalysisException e)
449:                 {
450:                         log.error("Problem replacing variable expressions with storage lookups");
451:                 }
452:         }
453:
454:         public TraceNodeData buildFromDeclTerms(List<ATraceDeclTermIR> terms)
455:                         throws AnalysisException
456:         {
457:                 String name = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().seqTraceNodeNamePrefix());
458:
459:                 AClassTypeIR classType = getTransAssist().consClassType(traceTrans.getTracePrefixes().seqClassTypeName());
460:
461:                 AVarDeclIR seqNodeDecl = getTransAssist().consDecl(name, classType, getTransAssist().consDefaultConsCall(classType));
462:
463:                 ABlockStmIR stms = new ABlockStmIR();
464:                 stms.getLocalDefs().add(seqNodeDecl);
465:
466:                 for (ATraceDeclTermIR term : terms)
467:                 {
468:                         TraceNodeData nodeData = term.apply(this);
469:                         stms.getStatements().add(nodeData.getStms());
470:
471:                         AIdentifierVarExpIR var = nodeData.getNodeVar();
472:                         nodeData.getNodeVarScope().getStatements().add(getTransAssist().consInstanceCallStm(classType, name, traceTrans.getTracePrefixes().addMethodName(), var));
473:                 }
474:
475:                 return new TraceNodeData(getInfo().getExpAssistant().consIdVar(name, classType.clone()), stms, stms);
476:         }
477:
478:         public AMethodDeclIR consTypeCheckMethod(SStmIR stm)
479:         {
480:                 return null;
481:         }
482:
483:         public AMethodDeclIR condMeetsPreCondMethod(SStmIR stm)
484:         {
485:                 if (!canBeGenerated())
486:                 {
487:                         return null;
488:                 }
489:
490:                 AMethodDeclIR meetsPredMethod = initPredDecl(traceTrans.getTracePrefixes().callStmMeetsPreCondNamePrefix());
491:
492:                 boolean isOp = false;
493:                 String pre = "pre_";
494:                 List<SExpIR> args = null;
495:
496:                 if (stm instanceof APlainCallStmIR)
497:                 {
498:                         APlainCallStmIR plainCall = (APlainCallStmIR) stm;
499:                         args = plainCall.getArgs();
500:                         SourceNode source = plainCall.getSourceNode();
501:                         if (source != null)
502:                         {
503:                                 org.overture.ast.node.INode vdmNode = source.getVdmNode();
504:
505:                                 if (vdmNode instanceof ACallStm)
506:                                 {
507:                                         ACallStm callStm = (ACallStm) vdmNode;
508:                                         if (callStm.getRootdef() instanceof SOperationDefinition)
509:                                         {
510:                                                 SOperationDefinition op = (SOperationDefinition) callStm.getRootdef();
511:
512:                                                 if (op.getPredef() == null)
513:                                                 {
514:                                                         // The pre condition is "true"
515:                                                         return null;
516:                                                 }
517:
518:                                                 isOp = true;
519:                                         } else if (callStm.getRootdef() instanceof SFunctionDefinition)
520:                                         {
521:                                                 SFunctionDefinition func = (SFunctionDefinition) callStm.getRootdef();
522:
523:                                                 if (func.getPredef() == null)
524:                                                 {
525:                                                         // The pre condition is true
526:                                                         return null;
527:                                                 }
528:                                         }
529:                                 } else
530:                                 {
531:                                         log.error("Expected VDM source node to be a call statement at this point. Got: "
532:                                                         + vdmNode);
533:                                 }
534:                         } else
535:                         {
536:                                 log.error("Could not find VDM source node for the plain statement call: "
537:                                                 + plainCall);
538:                         }
539:
540:                         plainCall.setName(pre + plainCall.getName());
541:                         plainCall.setType(new ABoolBasicTypeIR());
542:
543:                         meetsPredMethod.setBody(plainCall);
544:                 } else
545:                 {
546:                         log.error("Got unexpected statement: " + stm);
547:                         return null;
548:                 }
549:
550:                 if (args != null)
551:                 {
552:                         if (isOp)
553:                         {
554:                                 DeclAssistantIR dAssist = this.getInfo().getDeclAssistant();
555:                                 String invokedModule = getInvokedModule(stm);
556:                                 SClassDeclIR clazz = dAssist.findClass(getInfo().getClasses(), invokedModule);
557:
558:                                 for (AFieldDeclIR f : clazz.getFields())
559:                                 {
560:                                         if (!f.getFinal())
561:                                         {
562:                                                 // It's the state component
563:                                                 if (traceEnclosingClass.equals(invokedModule))
564:                                                 {
565:                                                         ExpAssistantIR eAssist = getInfo().getExpAssistant();
566:                                                         AIdentifierVarExpIR stateArg = eAssist.consIdVar(f.getName(), f.getType().clone());
567:                                                         traceTrans.getCloneFreeNodes().add(stateArg);
568:                                                         args.add(stateArg);
569:                                                 } else
570:                                                 {
571:                                                         AExternalTypeIR traceNodeClassType = new AExternalTypeIR();
572:                                                         traceNodeClassType.setName(traceTrans.getTracePrefixes().traceUtilClassName());
573:
574:                                                         AExplicitVarExpIR readStateMethod = new AExplicitVarExpIR();
575:                                                         readStateMethod.setClassType(traceNodeClassType);
576:                                                         readStateMethod.setIsLambda(false);
577:                                                         readStateMethod.setIsLocal(false);
578:                                                         readStateMethod.setName(traceTrans.getTracePrefixes().readStateMethodName());
579:
580:                                                         AMethodTypeIR readStateMethodType = new AMethodTypeIR();
581:                                                         readStateMethodType.setResult(f.getType().clone());
582:                                                         readStateMethodType.getParams().add(getTransAssist().consClassType(invokedModule));
583:                                                         readStateMethodType.getParams().add(f.getType().clone());
584:
585:                                                         readStateMethod.setType(readStateMethodType);
586:
587:                                                         AApplyExpIR readStateCall = new AApplyExpIR();
588:                                                         readStateCall.setRoot(readStateMethod);
589:                                                         readStateCall.setType(f.getType().clone());
590:
591:                                                         ATypeArgExpIR moduleArg = new ATypeArgExpIR();
592:                                                         moduleArg.setType(getTransAssist().consClassType(invokedModule));
593:
594:                                                         ATypeArgExpIR stateArg = new ATypeArgExpIR();
595:                                                         stateArg.setType(f.getType().clone());
596:
597:                                                         readStateCall.getArgs().add(moduleArg);
598:                                                         readStateCall.getArgs().add(stateArg);
599:
600:                                                         args.add(readStateCall);
601:                                                 }
602:
603:                                                 break;
604:                                         }
605:                                 }
606:                         }
607:                 } else
608:                 {
609:                         log.error("Could not find args for: " + stm);
610:                 }
611:
612:                 ensureStoreLookups(meetsPredMethod.getBody());
613:
614:                 return meetsPredMethod;
615:         }
616:
617:         protected AMethodDeclIR initPredDecl(String name)
618:         {
619:                 AMethodTypeIR methodType = new AMethodTypeIR();
620:                 methodType.setResult(new ABoolBasicTypeIR());
621:
622:                 AMethodDeclIR meetsPredMethod = new AMethodDeclIR();
623:                 meetsPredMethod.setImplicit(false);
624:                 meetsPredMethod.setAbstract(false);
625:                 meetsPredMethod.setAccess(IRConstants.PUBLIC);
626:                 meetsPredMethod.setAsync(false);
627:                 meetsPredMethod.setIsConstructor(false);
628:                 meetsPredMethod.setMethodType(methodType);
629:                 meetsPredMethod.setStatic(false);
630:                 meetsPredMethod.setName(name);
631:
632:                 return meetsPredMethod;
633:         }
634:
635:         protected boolean canBeGenerated()
636:         {
637:                 // This only works for VDM-SL
638:                 return Settings.dialect == Dialect.VDM_SL
639:                                 && getInfo().getSettings().generatePreConds();
640:         }
641:
642:         protected String getInvokedModule(SStmIR stm)
643:         {
644:                 if (stm instanceof APlainCallStmIR)
645:                 {
646:                         APlainCallStmIR call = (APlainCallStmIR) stm;
647:
648:                         STypeIR type = call.getClassType();
649:
650:                         if (type instanceof AClassTypeIR)
651:                         {
652:                                 return ((AClassTypeIR) type).getName();
653:                         }
654:                 }
655:
656:                 return traceEnclosingClass;
657:         }
658:
659:         protected SStmIR makeInstanceCall(SStmIR stm)
660:         {
661:                 if (stm instanceof ACallObjectExpStmIR)
662:                 {
663:                         // Assume the class enclosing the trace to be S
664:                         // self.op(42) becomes ((S)instance).op(42L)
665:                         // a.op(42) remains a.op(42L) if a is local
666:                         // a.op(42) becomes ((S)instance).a.op(42L) if a is an instance variable
667:
668:                         ACallObjectExpStmIR call = (ACallObjectExpStmIR) stm;
669:
670:                         try
671:                         {
672:                                 call.getObj().apply(new CallObjTraceLocalizer(getTransAssist(), traceTrans.getTracePrefixes(), traceEnclosingClass));
673:                         } catch (AnalysisException e)
674:                         {
675:                                 log.error("Got unexpected problem when trying to create instance call"
676:                                                 + e.getMessage());
677:                                 e.printStackTrace();
678:                         }
679:
680:                         /**
681:                          * We don't narrow the types of the arguments, which we should and which we do for the 'APlainCallStmIR'
682:                          * case using <code>castArgs(call);</code>. Code generation of traces does not really work for PP..
683:                          */
684:
685:                         if (call.getType() instanceof AVoidTypeIR)
686:                         {
687:                                 return handleVoidValueReturn(call);
688:                         }
689:
690:                         return stm;
691:                 } else if (stm instanceof APlainCallStmIR)
692:                 {
693:                         // Assume the class enclosing the trace to be S
694:                         // Example: op(42) becomes ((S)instance).op(42L)
695:                         try
696:                         {
697:                                 return handlePlainCallStm((APlainCallStmIR) stm);
698:                         } catch (AnalysisException e)
699:                         {
700:                                 log.error("Got unexpected problem when handling plain call statement: "
701:                                                 + e.getMessage());
702:                                 e.printStackTrace();
703:                         }
704:                 }
705:                 // Super call statements are not supported and this case should not be reached!
706:
707:                 log.error("Got unexpected statement: " + stm);
708:
709:                 return stm;
710:         }
711:
712:         protected SStmIR handleVoidValueReturn(SStmIR stm)
713:         {
714:                 AExternalTypeIR traceNodeClassType = new AExternalTypeIR();
715:                 traceNodeClassType.setName(traceTrans.getTracePrefixes().voidValueEnclosingClassName());
716:
717:                 AExplicitVarExpIR voidValue = new AExplicitVarExpIR();
718:                 voidValue.setType(new AObjectTypeIR());
719:                 voidValue.setClassType(traceNodeClassType);
720:                 voidValue.setIsLambda(false);
721:                 voidValue.setIsLocal(true);
722:                 voidValue.setName(traceTrans.getTracePrefixes().voidValueFieldName());
723:
724:                 AReturnStmIR returnVoidVal = new AReturnStmIR();
725:                 returnVoidVal.setExp(voidValue);
726:
727:                 ABlockStmIR block = new ABlockStmIR();
728:
729:                 block.getStatements().add(stm);
730:                 block.getStatements().add(returnVoidVal);
731:
732:                 return block;
733:         }
734:
735:         protected SStmIR handlePlainCallStm(APlainCallStmIR callStmIR)
736:                         throws AnalysisException
737:         {
738:                 STypeIR type = callStmIR.getType();
739:
740:                 if (callStmIR.getIsStatic())
741:                 {
742:                         if (type instanceof AVoidTypeIR)
743:                         {
744:                                 return handleVoidValueReturn(callStmIR);
745:                         } else
746:                         {
747:                                 return callStmIR;
748:                         }
749:                 }
750:
751:                 List<SExpIR> args = callStmIR.getArgs();
752:                 STypeIR classType = callStmIR.getClassType();
753:                 String name = callStmIR.getName();
754:
755:                 SourceNode sourceNode = callStmIR.getSourceNode();
756:
757:                 AClassTypeIR consClassType = getTransAssist().consClassType(traceEnclosingClass);
758:
759:                 ACastUnaryExpIR cast = new ACastUnaryExpIR();
760:                 cast.setType(consClassType);
761:                 cast.setExp(getInfo().getExpAssistant().consIdVar(traceTrans.getTracePrefixes().callStmMethodParamName(), consClassType.clone()));
762:
763:                 if (type instanceof AVoidTypeIR)
764:                 {
765:                         ACallObjectExpStmIR paramExp = new ACallObjectExpStmIR();
766:                         paramExp.setObj(cast);
767:
768:                         paramExp.setFieldName(name);
769:                         paramExp.setType(type.clone());
770:
771:                         for (SExpIR arg : args)
772:                         {
773:                                 paramExp.getArgs().add(arg.clone());
774:                         }
775:
776:                         paramExp.setSourceNode(sourceNode);
777:
778:                         return handleVoidValueReturn(paramExp);
779:                 } else
780:                 {
781:                         AFieldExpIR field = new AFieldExpIR();
782:                         String fieldModule = classType instanceof AClassTypeIR
783:                                         ? ((AClassTypeIR) classType).getName()
784:                                         : traceEnclosingClass;
785:                         field.setType(getInfo().getTypeAssistant().getMethodType(getInfo(), fieldModule, name, args));
786:                         field.setMemberName(name);
787:                         field.setObject(cast);
788:
789:                         AApplyExpIR apply = new AApplyExpIR();
790:                         apply.setType(type.clone());
791:                         apply.setRoot(field);
792:                         apply.setSourceNode(callStmIR.getSourceNode());
793:
794:                         for (SExpIR arg : args)
795:                         {
796:                                 apply.getArgs().add(arg.clone());
797:                         }
798:
799:                         String resultName = getInfo().getTempVarNameGen().nextVarName(traceTrans.getTracePrefixes().callStmResultNamePrefix());
800:                         AVarDeclIR resultDecl = getTransAssist().consDecl(resultName, type.clone(), apply);
801:
802:                         AReturnStmIR returnStm = new AReturnStmIR();
803:                         returnStm.setExp(getInfo().getExpAssistant().consIdVar(resultName, type.clone()));
804:
805:                         ABlockStmIR stms = new ABlockStmIR();
806:                         stms.getLocalDefs().add(resultDecl);
807:                         stms.getStatements().add(returnStm);
808:
809:                         return stms;
810:
811:                 }
812:         }
813:
814:         protected ABlockStmIR consDecl(String classTypeName, String varName,
815:                         SExpIR... args)
816:         {
817:                 ATypeNameIR typeName = getTransAssist().consTypeNameForClass(classTypeName);
818:
819:                 AClassTypeIR classType = getTransAssist().consClassType(classTypeName);
820:
821:                 ANewExpIR newExp = new ANewExpIR();
822:                 newExp.setName(typeName);
823:                 newExp.setType(classType);
824:
825:                 for (SExpIR arg : args)
826:                 {
827:                         newExp.getArgs().add(arg);
828:                 }
829:
830:                 return getTransAssist().wrap(getTransAssist().consDecl(varName, classType.clone(), newExp));
831:         }
832:
833:         public ACallObjectExpStmIR consAddTraceVarCall(AIdentifierVarExpIR subject,
834:                         AIdentifierVarExpIR t)
835:         {
836:                 ANewExpIR newVar = new ANewExpIR();
837:                 newVar.setName(getTransAssist().consTypeNameForClass(traceTrans.getTracePrefixes().traceVarClassName()));
838:                 newVar.setType(getTransAssist().consClassType(traceTrans.getTracePrefixes().traceVarClassName()));
839:
840:                 newVar.getArgs().add(getInfo().getExpAssistant().consStringLiteral(t.getName(), false));
841:                 newVar.getArgs().add(getInfo().getExpAssistant().consStringLiteral(""
842:                                 + getTransAssist().getInfo().getTypeAssistant().getVdmType(t.getType()), false));
843:                 newVar.getArgs().add(traceTrans.getToStringBuilder().toStringOf(t.clone()));
844:
845:                 return getTransAssist().consInstanceCallStm(subject.getType(), subject.getName(), traceTrans.getTracePrefixes().addVarFirstMethodName(), newVar);
846:         }
847:
848:         private TransAssistantIR getTransAssist()
849:         {
850:                 return traceTrans.getTransAssist();
851:         }
852:
853:         @Override
854:         public TraceNodeData createNewReturnValue(INode node)
855:                         throws AnalysisException
856:         {
857:                 assert false : "This should never happen";
858:                 return null;
859:         }
860:
861:         @Override
862:         public TraceNodeData createNewReturnValue(Object node)
863:                         throws AnalysisException
864:         {
865:                 assert false : "This should never happen";
866:                 return null;
867:         }
868: }