Package: JmlGenUtil

JmlGenUtil

nameinstructionbranchcomplexitylinemethod
JmlGenUtil(JmlGenerator)
M: 0 C: 12
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
consInvParamReplacementId(ADefaultClassDeclIR, String)
M: 0 C: 27
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
consRecPackage(String, String)
M: 0 C: 29
100%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 5
100%
M: 0 C: 1
100%
distributeNamedTypeInvs(List)
M: 0 C: 108
100%
M: 0 C: 16
100%
M: 0 C: 9
100%
M: 0 C: 22
100%
M: 0 C: 1
100%
genInvMethod(ADefaultClassDeclIR, ANamedTypeDeclIR)
M: 0 C: 106
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 22
100%
M: 0 C: 1
100%
getEnclosingClass(INode)
M: 13 C: 9
41%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 2 C: 3
60%
M: 0 C: 1
100%
getEnclosingMethod(INode)
M: 13 C: 9
41%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 2 C: 3
60%
M: 0 C: 1
100%
getInvFormalParam(AMethodDeclIR)
M: 30 C: 11
27%
M: 3 C: 1
25%
M: 2 C: 1
33%
M: 6 C: 2
25%
M: 0 C: 1
100%
getInvMethod(ATypeDeclIR)
M: 12 C: 13
52%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 2 C: 4
67%
M: 0 C: 1
100%
getInvParamVar(AMethodDeclIR)
M: 4 C: 26
87%
M: 2 C: 2
50%
M: 2 C: 1
33%
M: 2 C: 6
75%
M: 0 C: 1
100%
getMethodCondArgName(SPatternIR)
M: 13 C: 32
71%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 2 C: 7
78%
M: 0 C: 1
100%
getName(SPatternIR)
M: 13 C: 7
35%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 2 C: 2
50%
M: 0 C: 1
100%
getNamedTypeInvMethods(ADefaultClassDeclIR)
M: 0 C: 32
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
getRecFieldNames(ARecordDeclIR)
M: 0 C: 23
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
getRecords(List)
M: 0 C: 43
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
makeRecsOuterClasses(List, RecClassInfo)
M: 11 C: 259
96%
M: 1 C: 15
94%
M: 1 C: 8
89%
M: 1 C: 57
98%
M: 0 C: 1
100%
toJmlOldExp(String)
M: 0 C: 30
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%

Coverage

1: package org.overture.codegen.vdm2jml;
2:
3: import java.util.HashSet;
4: import java.util.LinkedList;
5: import java.util.List;
6:
7: import org.apache.log4j.Logger;
8: import org.overture.ast.util.ClonableString;
9: import org.overture.codegen.ir.INode;
10: import org.overture.codegen.ir.IRConstants;
11: import org.overture.codegen.ir.IRStatus;
12: import org.overture.codegen.ir.PIR;
13: import org.overture.codegen.ir.SPatternIR;
14: import org.overture.codegen.ir.STypeIR;
15: import org.overture.codegen.ir.VdmNodeInfo;
16: import org.overture.codegen.ir.declarations.ADefaultClassDeclIR;
17: import org.overture.codegen.ir.declarations.AFieldDeclIR;
18: import org.overture.codegen.ir.declarations.AFormalParamLocalParamIR;
19: import org.overture.codegen.ir.declarations.AInterfaceDeclIR;
20: import org.overture.codegen.ir.declarations.AMethodDeclIR;
21: import org.overture.codegen.ir.declarations.ANamedTypeDeclIR;
22: import org.overture.codegen.ir.declarations.ARecordDeclIR;
23: import org.overture.codegen.ir.declarations.ATypeDeclIR;
24: import org.overture.codegen.ir.expressions.AIdentifierVarExpIR;
25: import org.overture.codegen.ir.patterns.AIdentifierPatternIR;
26: import org.overture.codegen.ir.statements.AReturnStmIR;
27: import org.overture.codegen.ir.types.ABoolBasicTypeIR;
28: import org.overture.codegen.ir.types.AExternalTypeIR;
29: import org.overture.codegen.ir.types.AMethodTypeIR;
30: import org.overture.codegen.vdm2java.JavaCodeGen;
31: import org.overture.codegen.vdm2java.JavaCodeGenUtil;
32: import org.overture.codegen.vdm2java.JavaFormat;
33: import org.overture.codegen.vdm2jml.data.RecClassInfo;
34: import org.overture.codegen.vdm2jml.util.NameGen;
35:
36: public class JmlGenUtil
37: {
38:         private JmlGenerator jmlGen;
39:
40:         private Logger log = Logger.getLogger(this.getClass().getName());
41:
42:         public JmlGenUtil(JmlGenerator jmlGen)
43:         {
44:                 this.jmlGen = jmlGen;
45:         }
46:
47:         public AIdentifierVarExpIR getInvParamVar(AMethodDeclIR invMethod)
48:         {
49:                 AFormalParamLocalParamIR formalParam = getInvFormalParam(invMethod);
50:
51:•                if (formalParam == null)
52:                 {
53:                         return null;
54:                 }
55:
56:                 String paramName = getName(formalParam.getPattern());
57:
58:•                if (paramName == null)
59:                 {
60:                         return null;
61:                 }
62:
63:                 STypeIR paramType = formalParam.getType().clone();
64:
65:                 return jmlGen.getJavaGen().getInfo().getExpAssistant().consIdVar(paramName, paramType);
66:         }
67:
68:         public String getName(SPatternIR id)
69:         {
70:•                if (!(id instanceof AIdentifierPatternIR))
71:                 {
72:                         log.error("Expected identifier pattern "
73:                                         + "to be an identifier pattern at this point. Got: " + id);
74:                         return null;
75:                 }
76:
77:                 return ((AIdentifierPatternIR) id).getName();
78:         }
79:
80:         public AFormalParamLocalParamIR getInvFormalParam(AMethodDeclIR invMethod)
81:         {
82:•                if (invMethod.getFormalParams().size() == 1)
83:                 {
84:                         return invMethod.getFormalParams().get(0);
85:                 } else
86:                 {
87:                         log.error("Expected only a single formal parameter "
88:                                         + "for named invariant type method " + invMethod.getName()
89:                                         + " but got " + invMethod.getFormalParams().size());
90:
91:•                        if (!invMethod.getFormalParams().isEmpty())
92:                         {
93:                                 return invMethod.getFormalParams().get(0);
94:                         } else
95:                         {
96:                                 return null;
97:                         }
98:                 }
99:         }
100:
101:         public AMethodDeclIR getInvMethod(ATypeDeclIR typeDecl)
102:         {
103:•                if (typeDecl.getInv() instanceof AMethodDeclIR)
104:                 {
105:                         return (AMethodDeclIR) typeDecl.getInv();
106:•                } else if (typeDecl.getInv() != null)
107:                 {
108:                         log.error("Expected named type invariant function "
109:                                         + "to be a method declaration at this point. Got: "
110:                                         + typeDecl.getDecl());
111:                 }
112:
113:                 return null;
114:         }
115:
116:         public List<AMethodDeclIR> getNamedTypeInvMethods(ADefaultClassDeclIR clazz)
117:         {
118:                 List<AMethodDeclIR> invDecls = new LinkedList<AMethodDeclIR>();
119:
120:•                for (ATypeDeclIR typeDecl : clazz.getTypeDecls())
121:                 {
122:•                        if (typeDecl.getDecl() instanceof ANamedTypeDeclIR)
123:                         {
124:                                 AMethodDeclIR m = getInvMethod(typeDecl);
125:
126:•                                if (m != null)
127:                                 {
128:                                         invDecls.add(m);
129:                                 }
130:                         }
131:                 }
132:
133:                 return invDecls;
134:         }
135:
136:         public List<String> getRecFieldNames(ARecordDeclIR r)
137:         {
138:                 List<String> args = new LinkedList<String>();
139:
140:•                for (AFieldDeclIR f : r.getFields())
141:                 {
142:                         args.add(f.getName());
143:                 }
144:                 return args;
145:         }
146:
147:         public List<ARecordDeclIR> getRecords(List<IRStatus<PIR>> ast)
148:         {
149:                 List<ARecordDeclIR> records = new LinkedList<ARecordDeclIR>();
150:
151:•                for (IRStatus<ADefaultClassDeclIR> classStatus : IRStatus.extract(ast, ADefaultClassDeclIR.class))
152:                 {
153:•                        for (ATypeDeclIR typeDecl : classStatus.getIrNode().getTypeDecls())
154:                         {
155:•                                if (typeDecl.getDecl() instanceof ARecordDeclIR)
156:                                 {
157:                                         records.add((ARecordDeclIR) typeDecl.getDecl());
158:                                 }
159:                         }
160:                 }
161:
162:                 return records;
163:         }
164:
165:         public String getMethodCondArgName(SPatternIR pattern)
166:         {
167:                 // By now all patterns should be identifier patterns
168:•                if (pattern instanceof AIdentifierPatternIR)
169:                 {
170:                         String paramName = ((AIdentifierPatternIR) pattern).getName();
171:
172:•                        if (jmlGen.getJavaGen().getInfo().getExpAssistant().isOld(paramName))
173:                         {
174:                                 paramName = toJmlOldExp(paramName);
175:•                        } else if (jmlGen.getJavaGen().getInfo().getExpAssistant().isResult(paramName))
176:                         {
177:                                 // The type checker prohibits use of 'RESULT' as name of a user specified identifier
178:                                 paramName = JmlGenerator.JML_RESULT;
179:                         }
180:
181:                         return paramName;
182:
183:                 } else
184:                 {
185:                         log.error("Expected formal parameter pattern to be an indentifier pattern. Got: "
186:                                         + pattern);
187:
188:                         return "UNKNOWN";
189:                 }
190:         }
191:
192:         public String toJmlOldExp(String paramName)
193:         {
194:                 // Convert old name to current name (e.g. _St to St)
195:                 String currentArg = jmlGen.getJavaGen().getInfo().getExpAssistant().oldNameToCurrentName(paramName);
196:
197:                 // Note that invoking the copy method on the state should be okay
198:                 // because the state should never be a null pointer
199:                 currentArg += ".copy()";
200:
201:                 // Convert current name to JML old expression (e.g. \old(St)
202:                 return String.format("%s(%s)", JmlGenerator.JML_OLD_PREFIX, currentArg);
203:         }
204:
205:         /**
206:          * This change to the IR is really only to circumvent a bug in OpenJML with loading of inner classes. The only thing
207:          * that the Java code generator uses inner classes for is records. If this problem gets fixed the workaround
208:          * introduced by this method should be removed.
209:          *
210:          * @param ast
211:          * The IR passed by the Java code generator after the transformation process
212:          * @param recInfo
213:          * Since the new record classes are deep copies we need to update the record info too
214:          */
215:         public List<IRStatus<PIR>> makeRecsOuterClasses(List<IRStatus<PIR>> ast,
216:                         RecClassInfo recInfo)
217:         {
218:                 List<IRStatus<PIR>> extraClasses = new LinkedList<IRStatus<PIR>>();
219:
220:•                for (IRStatus<ADefaultClassDeclIR> status : IRStatus.extract(ast, ADefaultClassDeclIR.class))
221:                 {
222:                         ADefaultClassDeclIR clazz = status.getIrNode();
223:
224:                         List<ARecordDeclIR> recDecls = new LinkedList<ARecordDeclIR>();
225:
226:•                        for (ATypeDeclIR d : clazz.getTypeDecls())
227:                         {
228:•                                if (d.getDecl() instanceof ARecordDeclIR)
229:                                 {
230:                                         recDecls.add((ARecordDeclIR) d.getDecl());
231:                                 }
232:                         }
233:
234:                         // Note that we do not remove the type declarations (or records) from the class.
235:
236:                         // For each of the records we will make a top-level class
237:•                        for (ARecordDeclIR recDecl : recDecls)
238:                         {
239:                                 ADefaultClassDeclIR recClass = new ADefaultClassDeclIR();
240:
241:                                 recInfo.registerRecClass(recClass);
242:
243:                                 recClass.setMetaData(recDecl.getMetaData());
244:                                 recClass.setAbstract(false);
245:                                 recClass.setAccess(IRConstants.PUBLIC);
246:                                 recClass.setSourceNode(recDecl.getSourceNode());
247:                                 recClass.setStatic(false);
248:                                 recClass.setName(recDecl.getName());
249:
250:•                                if (recDecl.getInvariant() != null)
251:                                 {
252:                                         recClass.setInvariant(recDecl.getInvariant().clone());
253:                                 }
254:
255:                                 AInterfaceDeclIR recInterface = new AInterfaceDeclIR();
256:                                 recInterface.setPackage("org.overture.codegen.runtime");
257:
258:                                 final String RECORD_NAME = "Record";
259:                                 recInterface.setName(RECORD_NAME);
260:                                 AExternalTypeIR recInterfaceType = new AExternalTypeIR();
261:                                 recInterfaceType.setName(RECORD_NAME);
262:                                 AMethodTypeIR copyMethodType = new AMethodTypeIR();
263:                                 copyMethodType.setResult(recInterfaceType);
264:
265:                                 AMethodDeclIR copyMethod = jmlGen.getJavaGen().getJavaFormat().getRecCreator().consCopySignature(copyMethodType);
266:                                 copyMethod.setAbstract(true);
267:
268:                                 recInterface.getMethodSignatures().add(copyMethod);
269:
270:                                 recClass.getInterfaces().add(recInterface);
271:
272:                                 // Copy the record methods to the class
273:                                 List<AMethodDeclIR> methods = new LinkedList<AMethodDeclIR>();
274:•                                for (AMethodDeclIR m : recDecl.getMethods())
275:                                 {
276:                                         AMethodDeclIR newMethod = m.clone();
277:                                         methods.add(newMethod);
278:                                         recInfo.updateAccessor(m, newMethod);
279:                                 }
280:                                 recClass.setMethods(methods);
281:
282:                                 // Copy the record fields to the class
283:                                 List<AFieldDeclIR> fields = new LinkedList<AFieldDeclIR>();
284:•                                for (AFieldDeclIR f : recDecl.getFields())
285:                                 {
286:                                         AFieldDeclIR newField = f.clone();
287:                                         fields.add(newField);
288:                                         recInfo.register(newField);
289:                                 }
290:                                 recClass.setFields(fields);
291:
292:                                 // Put the record classes of module M in package <userpackage>.<modulename>types
293:                                 // Examples: my.pack.Mtypes
294:•                                if (JavaCodeGenUtil.isValidJavaPackage(jmlGen.getJavaSettings().getJavaRootPackage()))
295:                                 {
296:                                         String recPackage = consRecPackage(clazz.getName(), jmlGen.getJavaSettings().getJavaRootPackage());
297:                                         recClass.setPackage(recPackage);
298:                                 } else
299:                                 {
300:                                         recClass.setPackage(clazz.getName()
301:                                                         + JavaFormat.TYPE_DECL_PACKAGE_SUFFIX);
302:                                 }
303:
304:                                 List<ClonableString> imports = new LinkedList<>();
305:                                 imports.add(new ClonableString(JavaCodeGen.JAVA_UTIL));
306:                                 imports.add(new ClonableString(JavaCodeGen.RUNTIME_IMPORT));
307:                                 recClass.setDependencies(imports);
308:
309:                                 extraClasses.add(new IRStatus<PIR>(recClass.getSourceNode().getVdmNode(), recClass.getName(), recClass, new HashSet<VdmNodeInfo>()));
310:                         }
311:                 }
312:
313:                 return extraClasses;
314:         }
315:
316:         public static String consRecPackage(String defClass, String javaRootPackage)
317:         {
318:                 String recPackage = "";
319:
320:•                if (JavaCodeGenUtil.isValidJavaPackage(javaRootPackage))
321:                 {
322:                         recPackage += javaRootPackage + ".";
323:                 }
324:
325:                 recPackage += defClass + JavaFormat.TYPE_DECL_PACKAGE_SUFFIX;
326:
327:                 return recPackage;
328:         }
329:
330:         public AMethodDeclIR genInvMethod(ADefaultClassDeclIR clazz,
331:                         ANamedTypeDeclIR namedTypeDecl)
332:         {
333:                 AReturnStmIR body = new AReturnStmIR();
334:                 body.setExp(jmlGen.getJavaGen().getInfo().getExpAssistant().consBoolLiteral(true));
335:
336:                 STypeIR paramType = namedTypeDecl.getType();
337:
338:                 AMethodTypeIR invMethodType = new AMethodTypeIR();
339:                 invMethodType.setResult(new ABoolBasicTypeIR());
340:                 invMethodType.getParams().add(paramType.clone());
341:
342:                 String formalParamName = new NameGen(clazz).getName(JmlGenerator.GEN_INV_METHOD_PARAM_NAME);
343:
344:                 AFormalParamLocalParamIR formalParam = new AFormalParamLocalParamIR();
345:                 formalParam.setType(paramType.clone());
346:                 formalParam.setPattern(jmlGen.getJavaGen().getInfo().getPatternAssistant().consIdPattern(formalParamName));
347:
348:                 AMethodDeclIR method = new AMethodDeclIR();
349:                 method.setImplicit(false);
350:                 method.setAbstract(false);
351:                 method.setAccess(IRConstants.PUBLIC);
352:                 method.setAsync(false);
353:                 method.setBody(body);
354:                 method.getFormalParams().add(formalParam);
355:                 method.setIsConstructor(false);
356:                 method.setMethodType(invMethodType);
357:                 method.setName("inv_" + namedTypeDecl.getName());
358:                 method.setStatic(true);
359:
360:                 return method;
361:         }
362:
363:         public AIdentifierPatternIR consInvParamReplacementId(
364:                         ADefaultClassDeclIR encClass, String originalParamName)
365:         {
366:                 NameGen nameGen = new NameGen(encClass);
367:                 nameGen.addName(originalParamName);
368:
369:                 String newParamName = nameGen.getName(JmlGenerator.INV_METHOD_REPLACEMENT_NAME_PREFIX
370:                                 + originalParamName);
371:
372:                 return jmlGen.getJavaGen().getInfo().getPatternAssistant().consIdPattern(newParamName);
373:         }
374:
375:         public ADefaultClassDeclIR getEnclosingClass(INode node)
376:         {
377:                 ADefaultClassDeclIR enclosingClass = node.getAncestor(ADefaultClassDeclIR.class);
378:
379:•                if (enclosingClass != null)
380:                 {
381:                         return enclosingClass;
382:                 } else
383:                 {
384:                         log.error("Could not find enclosing class of node: " + node);
385:                         return null;
386:                 }
387:         }
388:
389:         public AMethodDeclIR getEnclosingMethod(INode node)
390:         {
391:                 AMethodDeclIR enclosingMethod = node.getAncestor(AMethodDeclIR.class);
392:
393:•                if (enclosingMethod != null)
394:                 {
395:                         return enclosingMethod;
396:                 } else
397:                 {
398:                         log.error("Could not find enclosing method of node: " + node);
399:                         return null;
400:                 }
401:         }
402:
403:         /**
404:          * There are problems with OpenJML when you invoke named type invariant methods across classes. Until these bugs are
405:          * fixed the workaround is simply to make sure that all generated classes have a local copy of a named invariant
406:          * method. TODO: Currently invariant method are named on the form "module_typename" although this does not truly
407:          * garuantee uniqueness. For example if module A defines type B_C the invariant method name is A_B_C. However if
408:          * module A_B defines type C then the invariant method will also be named A_B_C. So something needs to be done about
409:          * this.
410:          *
411:          * @param newAst
412:          */
413:         public void distributeNamedTypeInvs(List<IRStatus<PIR>> newAst)
414:         {
415:                 // Collect all named type invariants
416:                 List<ATypeDeclIR> allNamedTypeInvTypeDecls = new LinkedList<ATypeDeclIR>();
417:•                for (IRStatus<ADefaultClassDeclIR> status : IRStatus.extract(newAst, ADefaultClassDeclIR.class))
418:                 {
419:                         ADefaultClassDeclIR clazz = status.getIrNode();
420:
421:•                        if (jmlGen.getJavaGen().getInfo().getDeclAssistant().isLibraryName(clazz.getName()))
422:                         {
423:                                 continue;
424:                         }
425:
426:•                        for (ATypeDeclIR typeDecl : clazz.getTypeDecls())
427:                         {
428:•                                if (typeDecl.getDecl() instanceof ANamedTypeDeclIR)
429:                                 {
430:                                         allNamedTypeInvTypeDecls.add(typeDecl);
431:                                 }
432:                         }
433:                 }
434:
435:•                for (IRStatus<ADefaultClassDeclIR> status : IRStatus.extract(newAst, ADefaultClassDeclIR.class))
436:                 {
437:                         ADefaultClassDeclIR clazz = status.getIrNode();
438:
439:•                        if (jmlGen.getJavaGen().getInfo().getDeclAssistant().isLibraryName(clazz.getName()))
440:                         {
441:                                 continue;
442:                         }
443:
444:                         List<ATypeDeclIR> classTypeDecls = new LinkedList<ATypeDeclIR>(clazz.getTypeDecls());
445:
446:•                        for (ATypeDeclIR namedTypeInv : allNamedTypeInvTypeDecls)
447:                         {
448:•                                if (!classTypeDecls.contains(namedTypeInv))
449:                                 {
450:                                         classTypeDecls.add(namedTypeInv.clone());
451:                                 }
452:                         }
453:
454:                         clazz.setTypeDecls(classTypeDecls);
455:                 }
456:         }
457: }