Package: JmlGenerator

JmlGenerator

nameinstructionbranchcomplexitylinemethod
JmlGenerator()
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
JmlGenerator(JavaCodeGen)
M: 0 C: 34
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
addAssertions(List, TypePredDecorator)
M: 7 C: 33
83%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 3 C: 7
70%
M: 0 C: 1
100%
addJmlTransformations()
M: 5 C: 120
96%
M: 2 C: 10
83%
M: 2 C: 5
71%
M: 2 C: 22
92%
M: 0 C: 1
100%
addVdmToJmlRuntimeImport(ADefaultClassDeclIR)
M: 0 C: 22
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
adjustNamedTypeInvFuncs(IRStatus)
M: 2 C: 172
99%
M: 2 C: 10
83%
M: 2 C: 5
71%
M: 2 C: 38
95%
M: 0 C: 1
100%
annotateRecsWithInvs(List)
M: 0 C: 42
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
changeRecInvMethod(ARecordDeclIR)
M: 7 C: 11
61%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 3 C: 3
50%
M: 0 C: 1
100%
computeNamedTypeInvInfo(List)
M: 0 C: 33
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 7
100%
M: 0 C: 1
100%
consMethodCond(SDeclIR, List, String)
M: 15 C: 56
79%
M: 3 C: 5
63%
M: 2 C: 3
60%
M: 3 C: 8
73%
M: 0 C: 1
100%
finalIRConstructed(List, IRInfo)
M: 0 C: 189
100%
M: 0 C: 20
100%
M: 0 C: 11
100%
M: 0 C: 39
100%
M: 0 C: 1
100%
generateJml(List)
M: 0 C: 26
100%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 6
100%
M: 0 C: 1
100%
getAnnotator()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getInvChecksFlagOwner()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getIrSettings()
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getJavaGen()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getJavaSettings()
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getJmlSettings()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getStateDesInfo()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getTypeInfoList()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getUtil()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
initSettings()
M: 0 C: 36
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
initialIRConstructed(List, IRInfo)
M: 20 C: 56
74%
M: 3 C: 9
75%
M: 3 C: 4
57%
M: 6 C: 12
67%
M: 0 C: 1
100%
makeRecStateAccessorBased(List)
M: 19 C: 26
58%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 4 C: 6
60%
M: 0 C: 1
100%
normaliseTargets(List)
M: 41 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 10 C: 0
0%
M: 1 C: 0
0%
quoteClassesProduced(List)
M: 0 C: 19
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
setInvChecksOnOwner(List)
M: 0 C: 27
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
setIrSettings(IRSettings)
M: 5 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
setJavaSettings(JavaSettings)
M: 5 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
setJmlSettings(JmlSettings)
M: 4 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
sortAnnotations(List)
M: 15 C: 34
69%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 4 C: 7
64%
M: 0 C: 1
100%
tcTraceTest(TypePredDecorator)
M: 0 C: 68
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 11
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: import java.util.Set;
7:
8: import org.apache.log4j.Logger;
9: import org.overture.ast.analysis.AnalysisException;
10: import org.overture.ast.definitions.SFunctionDefinition;
11: import org.overture.ast.modules.AModuleModules;
12: import org.overture.ast.util.ClonableString;
13: import org.overture.codegen.ir.CodeGenBase;
14: import org.overture.codegen.ir.INode;
15: import org.overture.codegen.ir.IRConstants;
16: import org.overture.codegen.ir.IREventObserver;
17: import org.overture.codegen.ir.IRInfo;
18: import org.overture.codegen.ir.IRSettings;
19: import org.overture.codegen.ir.IRStatus;
20: import org.overture.codegen.ir.IrNodeInfo;
21: import org.overture.codegen.ir.PIR;
22: import org.overture.codegen.ir.SDeclIR;
23: import org.overture.codegen.ir.SStmIR;
24: import org.overture.codegen.ir.analysis.DepthFirstAnalysisAdaptor;
25: import org.overture.codegen.ir.declarations.ADefaultClassDeclIR;
26: import org.overture.codegen.ir.declarations.AFieldDeclIR;
27: import org.overture.codegen.ir.declarations.AFormalParamLocalParamIR;
28: import org.overture.codegen.ir.declarations.AMethodDeclIR;
29: import org.overture.codegen.ir.declarations.AModuleDeclIR;
30: import org.overture.codegen.ir.declarations.ANamedTypeDeclIR;
31: import org.overture.codegen.ir.declarations.ARecordDeclIR;
32: import org.overture.codegen.ir.declarations.ATypeDeclIR;
33: import org.overture.codegen.ir.declarations.AVarDeclIR;
34: import org.overture.codegen.ir.declarations.SClassDeclIR;
35: import org.overture.codegen.ir.expressions.ACastUnaryExpIR;
36: import org.overture.codegen.ir.expressions.AIdentifierVarExpIR;
37: import org.overture.codegen.ir.statements.ABlockStmIR;
38: import org.overture.codegen.ir.types.AUnknownTypeIR;
39: import org.overture.codegen.traces.TracesTrans;
40: import org.overture.codegen.trans.AssignStmTrans;
41: import org.overture.codegen.trans.assistants.TransAssistantIR;
42: import org.overture.codegen.trans.uniontypes.UnionTypeTrans;
43: import org.overture.codegen.trans.uniontypes.UnionTypeVarPrefixes;
44: import org.overture.codegen.utils.GeneratedData;
45: import org.overture.codegen.vdm2java.IJavaQuoteEventObserver;
46: import org.overture.codegen.vdm2java.JavaCodeGen;
47: import org.overture.codegen.vdm2java.JavaCodeGenUtil;
48: import org.overture.codegen.vdm2java.JavaSettings;
49: import org.overture.codegen.vdm2jml.data.RecClassInfo;
50: import org.overture.codegen.vdm2jml.data.StateDesInfo;
51: import org.overture.codegen.vdm2jml.predgen.TypePredDecorator;
52: import org.overture.codegen.vdm2jml.predgen.info.AbstractTypeInfo;
53: import org.overture.codegen.vdm2jml.predgen.info.NamedTypeInfo;
54: import org.overture.codegen.vdm2jml.predgen.info.NamedTypeInvDepCalculator;
55: import org.overture.codegen.vdm2jml.trans.JmlTraceTrans;
56: import org.overture.codegen.vdm2jml.trans.JmlUnionTypeTrans;
57: import org.overture.codegen.vdm2jml.trans.RecAccessorTrans;
58: import org.overture.codegen.vdm2jml.trans.RecInvTransformation;
59: import org.overture.codegen.vdm2jml.trans.TargetNormaliserTrans;
60: import org.overture.codegen.vdm2jml.trans.TcExpInfo;
61: import org.overture.codegen.vdm2jml.util.AnnotationSorter;
62: import org.overture.codegen.vdm2jml.util.IsValChecker;
63: import org.overture.codegen.vdm2jml.util.NameGen;
64:
65: public class JmlGenerator implements IREventObserver, IJavaQuoteEventObserver
66: {
67:         private static final String VDM_JML_RUNTIME_IMPORT = "org.overture.codegen.vdm2jml.runtime.*";
68:         public static final String DEFAULT_JAVA_ROOT_PACKAGE = "project";
69:         public static final String GEN_INV_METHOD_PARAM_NAME = "elem";
70:         public static final String INV_PREFIX = "inv_";
71:         public static final String INV_METHOD_REPLACEMENT_NAME_PREFIX = "check_";
72:
73:         public static final String JML_PUBLIC = "public";
74:         public static final String JML_STATIC_INV_ANNOTATION = "static invariant";
75:         public static final String JML_OR = " || ";
76:         public static final String JML_AND = " && ";
77:         public static final String JML_IMPLIES = " ==> ";
78:         public static final String JML_INSTANCE_INV_ANNOTATION = "instance invariant";
79:         public static final String JML_REQ_ANNOTATION = "requires";
80:         public static final String JML_ENS_ANNOTATION = "ensures";
81:         public static final String JML_ASSERT_ANNOTATION = "assert";
82:         public static final String JML_OLD_PREFIX = "\\old";
83:         public static final String JML_SPEC_PUBLIC = "/*@ spec_public @*/";
84:         public static final String JML_PURE = "/*@ pure @*/";
85:         public static final String JML_HELPER = "/*@ helper @*/";
86:         public static final String JML_RESULT = "\\result";
87:         public static final String JML_NULLABLE_BY_DEFAULT = "//@ nullable_by_default";
88:
89:         public static final String INV_CHECKS_ON_GHOST_VAR_NAME = "invChecksOn";
90:         public static final String JML_INV_CHECKS_ON_DECL = "/*@ public ghost static boolean %s = true; @*/";
91:         public static final String JML_SET_INV_CHECKS = "//@ set %s = %s;";
92:
93:         public static final String JML_INVARIANT_FOR = "\\invariant_for";
94:         public static final String REC_VALID_METHOD_NAMEVALID = "valid";
95:         public static final String REC_VALID_METHOD_CALL = REC_VALID_METHOD_NAMEVALID
96:                         + "()";
97:
98:         public static final String JAVA_INSTANCEOF = " instanceof ";
99:
100:         private JavaCodeGen javaGen;
101:
102:         private JmlSettings jmlSettings;
103:
104:         private List<NamedTypeInfo> typeInfoList;
105:         private JmlGenUtil util;
106:         private JmlAnnotationHelper annotator;
107:
108:         private StateDesInfo stateDesInfo;
109:
110:         // The class owning the invChecksOn flag
111:         private ADefaultClassDeclIR invChecksFlagOwner = null;
112:
113:         private List<TcExpInfo> tcExpInfo;
114:
115:         private Logger log = Logger.getLogger(this.getClass().getName());
116:
117:         public JmlGenerator()
118:         {
119:                 this(new JavaCodeGen());
120:         }
121:
122:         public JmlGenerator(JavaCodeGen javaGen)
123:         {
124:                 this.javaGen = javaGen;
125:
126:                 // Named invariant type info will be derived (later) from the VDM-SL AST
127:                 this.typeInfoList = null;
128:                 this.util = new JmlGenUtil(this);
129:                 this.annotator = new JmlAnnotationHelper(this);
130:
131:                 initSettings();
132:
133:                 addJmlTransformations();
134:         }
135:
136:         private void addJmlTransformations()
137:         {
138:                 TargetNormaliserTrans targetNormaliserTrans = new TargetNormaliserTrans(this);
139:
140:                 // Info structures are populated with data when the transformations are applied
141:                 this.stateDesInfo = targetNormaliserTrans.getStateDesInfo();
142:
143:                 List<DepthFirstAnalysisAdaptor> series = this.javaGen.getTransSeries().getSeries();
144:
145:                 List<INode> cloneFreeNodes = javaGen.getJavaFormat().getValueSemantics().getCloneFreeNodes();
146:
147:                 // Replace the union type transformation
148:•                for (int i = 0; i < series.size(); i++)
149:                 {
150:                         DepthFirstAnalysisAdaptor currentTr = series.get(i);
151:
152:•                        if (currentTr instanceof UnionTypeTrans)
153:                         {
154:                                 TransAssistantIR assist = javaGen.getTransAssistant();
155:                                 UnionTypeVarPrefixes varPrefixes = javaGen.getVarPrefixManager().getUnionTypePrefixes();
156:
157:                                 JmlUnionTypeTrans newUnionTypeTr = new JmlUnionTypeTrans(assist, varPrefixes, cloneFreeNodes, stateDesInfo);
158:
159:                                 series.set(i, newUnionTypeTr);
160:•                        } else if (currentTr instanceof TracesTrans)
161:                         {
162:                                 TracesTrans orig = (TracesTrans) currentTr;
163:                                 JmlTraceTrans newTraceTrans = new JmlTraceTrans(orig.getTransAssist(), orig.getIteVarPrefixes(), orig.getTracePrefixes(), orig.getLangIterator(), orig.getToStringBuilder(), cloneFreeNodes);
164:                                 series.set(i, newTraceTrans);
165:                                 this.tcExpInfo = newTraceTrans.getTcExpInfo();
166:                         }
167:                 }
168:
169:                 // Now add the assignment transformation
170:•                for (int i = 0; i < series.size(); i++)
171:                 {
172:                         // We'll add the transformations after the assignment transformation
173:•                        if (series.get(i).getClass().equals(AssignStmTrans.class))
174:                         {
175:                                 int targetTransIdx = i + 1;
176:
177:•                                if (targetTransIdx <= series.size())
178:                                 {
179:                                         series.add(targetTransIdx, targetNormaliserTrans);
180:                                 } else
181:                                 {
182:                                         log.error("Could not add transformations to the transformation series");
183:                                 }
184:
185:                                 break;
186:                         }
187:                 }
188:         }
189:
190:         private void initSettings()
191:         {
192:                 IRSettings irSettings = getIrSettings();
193:                 irSettings.setGeneratePreConds(true);
194:                 irSettings.setGeneratePreCondChecks(false);
195:                 irSettings.setGeneratePostConds(true);
196:                 irSettings.setGeneratePostCondChecks(false);
197:                 irSettings.setGenerateInvariants(true);
198:                 irSettings.setGenerateTraces(true);
199:                 irSettings.setAddStateInvToModule(false);
200:
201:                 JavaSettings javaSettings = getJavaSettings();
202:                 javaSettings.setGenRecsAsInnerClasses(false);
203:
204:                 this.jmlSettings = new JmlSettings();
205:         }
206:
207:         public GeneratedData generateJml(List<AModuleModules> ast)
208:                         throws AnalysisException
209:         {
210:•                if (!JavaCodeGenUtil.isValidJavaPackage(getJavaSettings().getJavaRootPackage()))
211:                 {
212:                         getJavaSettings().setJavaRootPackage(DEFAULT_JAVA_ROOT_PACKAGE);
213:                 }
214:
215:                 computeNamedTypeInvInfo(ast);
216:
217:                 javaGen.registerIrObs(this);
218:                 javaGen.registerJavaQuoteObs(this);
219:
220:                 return javaGen.generate(CodeGenBase.getNodes(ast));
221:         }
222:
223:         @Override
224:         public List<IRStatus<PIR>> initialIRConstructed(List<IRStatus<PIR>> ast,
225:                         IRInfo info)
226:         {
227:                 List<IRStatus<AModuleDeclIR>> modules = IRStatus.extract(ast, AModuleDeclIR.class);
228:
229:•                for (IRStatus<AModuleDeclIR> m : modules)
230:                 {
231:•                        for (SDeclIR d : m.getIrNode().getDecls())
232:                         {
233:•                                if (d instanceof AFieldDeclIR)
234:                                 {
235:                                         AFieldDeclIR f = (AFieldDeclIR) d;
236:
237:•                                        if (f.getInitial() != null && f.getFinal())
238:                                         {
239:                                                 IsValChecker isVal = new IsValChecker();
240:                                                 try
241:                                                 {
242:•                                                        if (!f.getInitial().apply(isVal))
243:                                                         {
244:                                                                 Set<IrNodeInfo> wrap = new HashSet<>();
245:                                                                 IrNodeInfo warning = new IrNodeInfo(f, "The JML generator only allows literal-based expressions "
246:                                                                                 + "to be used to initialise value definitions");
247:                                                                 // By requiring that there is no need to assert that it is not null
248:                                                                 wrap.add(warning);
249:                                                                 m.addTransformationWarnings(wrap);
250:                                                         }
251:
252:                                                 } catch (org.overture.codegen.ir.analysis.AnalysisException e)
253:                                                 {
254:                                                         e.printStackTrace();
255:                                                 }
256:
257:                                         }
258:                                 }
259:                         }
260:                 }
261:
262:                 return ast;
263:         }
264:
265:         @Override
266:         public List<IRStatus<PIR>> finalIRConstructed(List<IRStatus<PIR>> ast,
267:                         IRInfo info)
268:         {
269:                 // In the final version of the IR, received by the Java code generator, all
270:                 // top level containers are classes
271:                 setInvChecksOnOwner(ast);
272:                 annotateRecsWithInvs(ast);
273:
274:                 // All the record methods are JML pure
275:                 annotator.makeRecMethodsPure(ast);
276:
277:                 /**
278:                  * Make records accessor-based (i.e. using setters and getters), which will force the record into a visible
279:                  * state when modified/read.
280:                  */
281:                 RecClassInfo recInfo = makeRecStateAccessorBased(ast);
282:
283:                 List<IRStatus<PIR>> newAst = new LinkedList<IRStatus<PIR>>(ast);
284:
285:                 // To circumvent a problem with OpenJML. See documentation of makeRecsOuterClasses
286:                 newAst.addAll(util.makeRecsOuterClasses(ast, recInfo));
287:
288:                 // Also extract classes that are records
289:•                for (IRStatus<ADefaultClassDeclIR> status : IRStatus.extract(newAst, ADefaultClassDeclIR.class))
290:                 {
291:                         ADefaultClassDeclIR clazz = status.getIrNode();
292:
293:                         // VDM uses the type system to control whether 'nil' is allowed as a value so we'll
294:                         // just annotate all classes as @nullable_by_default
295:                         annotator.makeNullableByDefault(clazz);
296:
297:                         // Make sure that the classes can access the VDM to JML runtime
298:                         addVdmToJmlRuntimeImport(clazz);
299:                 }
300:
301:                 // Only extract from 'ast' to not get the record classes
302:•                for (IRStatus<ADefaultClassDeclIR> status : IRStatus.extract(ast, ADefaultClassDeclIR.class))
303:                 {
304:                         ADefaultClassDeclIR clazz = status.getIrNode();
305:
306:•                        if (info.getDeclAssistant().isLibraryName(clazz.getName()))
307:                         {
308:                                 continue;
309:                         }
310:
311:•                        for (AFieldDeclIR f : clazz.getFields())
312:                         {
313:                                 // Make fields JML @spec_public so they can be passed to post conditions.
314:                                 // However, we'll avoid doing it for public fields as this does not make sense
315:•                                if (!f.getAccess().equals(IRConstants.PUBLIC))
316:                                 {
317:                                         annotator.makeSpecPublic(f);
318:                                 }
319:                         }
320:
321:                         // Named type invariant functions will potentially also have to be
322:                         // accessed by other modules
323:                         annotator.makeNamedTypeInvFuncsPublic(clazz);
324:
325:                         // In order for a value to be compatible with a named invariant type
326:                         // two conditions must be met:
327:                         //
328:                         // 1) The type of the value must match the domain type of the named
329:                         // type invariant. T = <domainType>
330:                         //
331:                         // 2) the value must meet the invariant predicate
332:                         adjustNamedTypeInvFuncs(status);
333:
334:                         // Note that the methods contained in clazz.getMethod() include
335:                         // pre post and invariant methods
336:•                        for (AMethodDeclIR m : clazz.getMethods())
337:                         {
338:•                                if (m.getPreCond() != null)
339:                                 {
340:                                         // We need to make pre and post conditions functions public in order to
341:                                         // be able to call them in the @requires and @ensures clauses, respectively.
342:                                         annotator.makeCondPublic(m.getPreCond());
343:                                         annotator.appendMetaData(m, consMethodCond(m.getPreCond(), m.getFormalParams(), JML_REQ_ANNOTATION));
344:                                 }
345:
346:•                                if (m.getPostCond() != null)
347:                                 {
348:                                         annotator.makeCondPublic(m.getPostCond());
349:                                         annotator.appendMetaData(m, consMethodCond(m.getPostCond(), m.getFormalParams(), JML_ENS_ANNOTATION));
350:                                 }
351:
352:                                 // Some methods such as those in record classes
353:                                 // will not have a source node. Thus this check.
354:•                                if (m.getSourceNode() != null)
355:                                 {
356:•                                        if (m.getSourceNode().getVdmNode() instanceof SFunctionDefinition)
357:                                         {
358:                                                 annotator.makePure(m);
359:                                         }
360:                                 }
361:                         }
362:                 }
363:
364:                 TypePredDecorator assertTr = new TypePredDecorator(this, stateDesInfo, recInfo);
365:
366:                 // Add assertions to check for violation of record and named type invariants
367:                 addAssertions(newAst, assertTr);
368:
369:                 // Make sure that the JML annotations are ordered correctly
370:                 sortAnnotations(newAst);
371:
372:                 // Make all nodes have a copy of each named type invariant method
373:                 util.distributeNamedTypeInvs(newAst);
374:
375:                 // Type check trace tests
376:                 tcTraceTest(assertTr);
377:
378:                 // Return back the modified AST to the Java code generator
379:                 return newAst;
380:         }
381:
382:         private void tcTraceTest(TypePredDecorator assertTr)
383:         {
384:•                for (TcExpInfo currentInfo : tcExpInfo)
385:                 {
386:                         AbstractTypeInfo typeInfo = assertTr.getTypePredUtil().findTypeInfo(currentInfo.getFormalParamType());
387:
388:                         String enclosingClass = currentInfo.getTraceEnclosingClass();
389:                         String javaRootPackage = getJavaSettings().getJavaRootPackage();
390:
391:                         SClassDeclIR clazz = getJavaGen().getInfo().getDeclAssistant().findClass(getJavaGen().getInfo().getClasses(), enclosingClass);
392:                         NameGen nameGen = new NameGen(clazz);
393:                         String expRef = currentInfo.getExpRef();
394:                         String checkStr = typeInfo.consCheckExp(enclosingClass, javaRootPackage, expRef, nameGen);
395:
396:                         currentInfo.getTypeCheck().setMetaData(annotator.consMetaData("//@ "
397:                                         + JML_ASSERT_ANNOTATION + " " + checkStr + ";"));
398:                 }
399:         }
400:
401:         private void addVdmToJmlRuntimeImport(ADefaultClassDeclIR clazz)
402:         {
403:                 String vdmJmlRuntimeImport = VDM_JML_RUNTIME_IMPORT;
404:                 List<ClonableString> allImports = new LinkedList<>();
405:                 allImports.addAll(clazz.getDependencies());
406:                 allImports.add(new ClonableString(vdmJmlRuntimeImport));
407:                 clazz.setDependencies(allImports);
408:         }
409:
410:         private RecClassInfo makeRecStateAccessorBased(List<IRStatus<PIR>> ast)
411:         {
412:
413:                 RecAccessorTrans recAccTr = new RecAccessorTrans(this);
414:
415:•                for (IRStatus<PIR> status : ast)
416:                 {
417:                         try
418:                         {
419:                                 javaGen.getIRGenerator().applyPartialTransformation(status, recAccTr);
420:                         } catch (org.overture.codegen.ir.analysis.AnalysisException e)
421:                         {
422:
423:                                 log.error("Could not apply '" + RecAccessorTrans.class
424:                                                 + "' to status " + status.getIrNodeName());
425:                                 e.printStackTrace();
426:                         }
427:                 }
428:
429:                 return recAccTr.getRecInfo();
430:         }
431:
432:         private void sortAnnotations(List<IRStatus<PIR>> newAst)
433:         {
434:                 AnnotationSorter sorter = new AnnotationSorter();
435:
436:•                for (IRStatus<ADefaultClassDeclIR> status : IRStatus.extract(newAst, ADefaultClassDeclIR.class))
437:                 {
438:•                        if (!javaGen.getInfo().getDeclAssistant().isLibraryName(status.getIrNode().getName()))
439:                         {
440:                                 try
441:                                 {
442:                                         status.getIrNode().apply(sorter);
443:                                 } catch (org.overture.codegen.ir.analysis.AnalysisException e)
444:                                 {
445:                                         log.error("Could not sort JML annotations for node "
446:                                                         + status.getIrNode());
447:                                         e.printStackTrace();
448:                                 }
449:                         }
450:                 }
451:         }
452:
453:         private void computeNamedTypeInvInfo(List<AModuleModules> ast)
454:                         throws AnalysisException
455:         {
456:                 NamedTypeInvDepCalculator depCalc = new NamedTypeInvDepCalculator(this.getJavaGen().getInfo());
457:
458:•                for (AModuleModules m : ast)
459:                 {
460:•                        if (!javaGen.getInfo().getDeclAssistant().isLibrary(m))
461:                         {
462:                                 m.apply(depCalc);
463:                         }
464:                 }
465:
466:                 this.typeInfoList = depCalc.getTypeDataList();
467:         }
468:
469:         private void addAssertions(List<IRStatus<PIR>> newAst,
470:                         TypePredDecorator assertTr)
471:         {
472:•                for (IRStatus<ADefaultClassDeclIR> status : IRStatus.extract(newAst, ADefaultClassDeclIR.class))
473:                 {
474:                         ADefaultClassDeclIR clazz = status.getIrNode();
475:
476:•                        if (!this.javaGen.getInfo().getDeclAssistant().isLibraryName(clazz.getName()))
477:                         {
478:                                 try
479:                                 {
480:                                         this.javaGen.getIRGenerator().applyPartialTransformation(status, assertTr);
481:                                 } catch (org.overture.codegen.ir.analysis.AnalysisException e)
482:                                 {
483:                                         log.error("Unexpected problem occured when applying transformation");
484:                                         e.printStackTrace();
485:                                 }
486:                         }
487:                 }
488:         }
489:
490:         private void annotateRecsWithInvs(List<IRStatus<PIR>> ast)
491:         {
492:                 List<ARecordDeclIR> recs = util.getRecords(ast);
493:
494:•                for (ARecordDeclIR r : recs)
495:                 {
496:•                        if (r.getInvariant() != null)
497:                         {
498:                                 // The record invariant is an instance invariant and the invariant method
499:                                 // is updated such that it passes the record fields (rather than the record instance)
500:                                 // to the invariant method. See the changeRecInvMethod for more information about
501:                                 // this. Also note that there is no need for the record invariant method to guard against
502:                                 // the record being null (because the invariant is specified as an instance invariant).
503:                                 changeRecInvMethod(r);
504:
505:                                 // Must be public otherwise we can't access it from the invariant
506:                                 annotator.makeCondPublic(r.getInvariant());
507:                                 // Must be a helper since we use this function from the invariant
508:                                 annotator.makeHelper(r.getInvariant());
509:
510:                                 annotator.makePure(r.getInvariant());
511:
512:                                 // Add the instance invariant to the record
513:                                 // Make it public so we can access the record fields from the invariant clause
514:                                 annotator.addRecInv(r);
515:                         }
516:                 }
517:         }
518:
519:         private void setInvChecksOnOwner(List<IRStatus<PIR>> ast)
520:         {
521:
522:•                for (IRStatus<ADefaultClassDeclIR> status : IRStatus.extract(ast, ADefaultClassDeclIR.class))
523:                 {
524:•                        if (invChecksFlagOwner == null)
525:                         {
526:                                 invChecksFlagOwner = status.getIrNode();
527:                                 annotator.addInvCheckGhostVarDecl(invChecksFlagOwner);
528:                         }
529:                 }
530:         }
531:
532:         /**
533:          * The record invariant method is generated such that it takes the record instance as an argument, e.g.
534:          * inv_Rec(recToCheck). When I try to invoke it from the instance invariant clause as //@ invariant inv_Rec(this);
535:          * it crashes on a stackoverflow where it keeps calling the invariant check. Adjusting the invariant method such
536:          * that it instead takes the fields as arguments does, however, work. This is exactly what this method does. After
537:          * calling this method a call to the invariant method from the invariant will take the following form: //@ public
538:          * instance invariant inv_Rec(field1,field2);
539:          *
540:          * @param rec
541:          * The record for which we will change the invariant method
542:          */
543:         private void changeRecInvMethod(ARecordDeclIR rec)
544:         {
545:                 try
546:                 {
547:                         rec.getInvariant().apply(new RecInvTransformation(javaGen, rec));
548:                 } catch (org.overture.codegen.ir.analysis.AnalysisException e)
549:                 {
550:                         log.error("Could not transform the invariant method of a record");
551:                         e.printStackTrace();
552:                 }
553:         }
554:
555:         private List<ClonableString> consMethodCond(SDeclIR decl,
556:                         List<AFormalParamLocalParamIR> parentMethodParams, String jmlAnno)
557:         {
558:•                if (decl instanceof AMethodDeclIR)
559:                 {
560:                         AMethodDeclIR cond = (AMethodDeclIR) decl;
561:
562:                         List<String> fieldNames = new LinkedList<String>();
563:
564:                         // The arguments of a function or an operation are passed to the pre/post condition
565:                         int i;
566:•                        for (i = 0; i < parentMethodParams.size(); i++)
567:                         {
568:                                 fieldNames.add(util.getMethodCondArgName(parentMethodParams.get(i).getPattern()));
569:                         }
570:
571:                         // Now compute the remaining argument names which (possibly)
572:                         // include the RESULT and the old state passed
573:•                        for (; i < cond.getFormalParams().size(); i++)
574:                         {
575:                                 fieldNames.add(util.getMethodCondArgName(cond.getFormalParams().get(i).getPattern()));
576:                         }
577:
578:                         return annotator.consAnno(jmlAnno, cond.getName(), fieldNames);
579:
580:•                } else if (decl != null)
581:                 {
582:                         log.error("Expected pre/post condition to be a method declaration at this point. Got: "
583:                                         + decl);
584:                 }
585:
586:                 return null;
587:         }
588:
589:         public void adjustNamedTypeInvFuncs(IRStatus<ADefaultClassDeclIR> status)
590:         {
591:                 ADefaultClassDeclIR clazz = status.getIrNode();
592:
593:•                for (ATypeDeclIR typeDecl : clazz.getTypeDecls())
594:                 {
595:•                        if (typeDecl.getDecl() instanceof ANamedTypeDeclIR)
596:                         {
597:                                 ANamedTypeDeclIR namedTypeDecl = (ANamedTypeDeclIR) typeDecl.getDecl();
598:
599:                                 AMethodDeclIR method = util.getInvMethod(typeDecl);
600:
601:                                 boolean invMethodIsGen = false;
602:
603:•                                if (method == null)
604:                                 {
605:                                         method = util.genInvMethod(clazz, namedTypeDecl);
606:                                         typeDecl.setInv(method);
607:                                         invMethodIsGen = true;
608:                                 }
609:
610:                                 String defModule = namedTypeDecl.getName().getDefiningClass();
611:                                 String name = namedTypeDecl.getName().getName();
612:                                 method.setName(JmlGenerator.INV_PREFIX + defModule + "_"
613:                                                 + name);
614:
615:                                 AFormalParamLocalParamIR invParam = util.getInvFormalParam(method);
616:                                 AFormalParamLocalParamIR invParamCopy = invParam.clone();
617:
618:                                 invParam.setType(new AUnknownTypeIR());
619:
620:                                 String paramName = util.getName(invParam.getPattern());
621:
622:•                                if (paramName == null)
623:                                 {
624:                                         continue;
625:                                 }
626:
627:                                 invParam.setPattern(util.consInvParamReplacementId(clazz, paramName));
628:
629:                                 // Invariant methods are really functions so we'll annotate them as pure
630:                                 annotator.makePure(method);
631:
632:                                 // We'll also make it a helper so it can be called from invariants, which is needed for fields
633:                                 // Otherwise we would get errors on the form:
634:                                 // "Calling a pure non-helper method in an invariant may lead to unbounded recursive
635:                                 // invariant checks and stack-overflow: inv_C(java.lang.Object)"
636:                                 annotator.makeHelper(method);
637:
638:                                 ABlockStmIR declStmBlock = new ABlockStmIR();
639:
640:•                                if (!invMethodIsGen)
641:                                 {
642:                                         AIdentifierVarExpIR paramVar = util.getInvParamVar(method);
643:
644:•                                        if (paramVar == null)
645:                                         {
646:                                                 continue;
647:                                         }
648:
649:                                         ACastUnaryExpIR cast = new ACastUnaryExpIR();
650:                                         cast.setType(invParamCopy.getType().clone());
651:                                         cast.setExp(paramVar.clone());
652:
653:                                         AVarDeclIR decl = javaGen.getInfo().getDeclAssistant().consLocalVarDecl(invParamCopy.getType(), invParamCopy.getPattern(), cast);
654:                                         declStmBlock.setScoped(false);
655:                                         declStmBlock.getLocalDefs().add(decl);
656:                                 }
657:
658:                                 SStmIR body = method.getBody();
659:
660:                                 ABlockStmIR repBlock = new ABlockStmIR();
661:                                 javaGen.getTransAssistant().replaceNodeWith(body, repBlock);
662:
663:                                 repBlock.getStatements().add(declStmBlock);
664:                                 repBlock.getStatements().add(body);
665:                         }
666:                 }
667:         }
668:
669:         public StateDesInfo normaliseTargets(List<IRStatus<PIR>> newAst)
670:         {
671:                 TargetNormaliserTrans normaliser = new TargetNormaliserTrans(this);
672:•                for (IRStatus<PIR> n : newAst)
673:                 {
674:                         try
675:                         {
676:                                 javaGen.getIRGenerator().applyPartialTransformation(n, normaliser);
677:                         } catch (org.overture.codegen.ir.analysis.AnalysisException e)
678:                         {
679:                                 log.error("Problem normalising state designators: "
680:                                                 + e.getMessage());
681:                                 e.printStackTrace();
682:                         }
683:                 }
684:
685:                 return normaliser.getStateDesInfo();
686:         }
687:
688:         @Override
689:         public void quoteClassesProduced(List<ADefaultClassDeclIR> quoteClasses)
690:         {
691:•                for (ADefaultClassDeclIR qc : quoteClasses)
692:                 {
693:                         // Code generated quotes are represented as singletons and by default the instance
694:                         // field is null. So we'll mark quote classes as nullable_by_default.
695:                         // Example from class represented <A>: private static AQuote instance = null;
696:                         annotator.makeNullableByDefault(qc);
697:                         addVdmToJmlRuntimeImport(qc);
698:                 }
699:         }
700:
701:         public JmlSettings getJmlSettings()
702:         {
703:                 return jmlSettings;
704:         }
705:
706:         public void setJmlSettings(JmlSettings jmlSettings)
707:         {
708:                 this.jmlSettings = jmlSettings;
709:         }
710:
711:         public IRSettings getIrSettings()
712:         {
713:                 return javaGen.getSettings();
714:         }
715:
716:         public void setIrSettings(IRSettings irSettings)
717:         {
718:                 javaGen.setSettings(irSettings);
719:         }
720:
721:         public JavaSettings getJavaSettings()
722:         {
723:                 return javaGen.getJavaSettings();
724:         }
725:
726:         public void setJavaSettings(JavaSettings javaSettings)
727:         {
728:                 javaGen.setJavaSettings(javaSettings);
729:         }
730:
731:         public JmlAnnotationHelper getAnnotator()
732:         {
733:                 return annotator;
734:         }
735:
736:         public JavaCodeGen getJavaGen()
737:         {
738:                 return javaGen;
739:         }
740:
741:         public JmlGenUtil getUtil()
742:         {
743:                 return util;
744:         }
745:
746:         public List<NamedTypeInfo> getTypeInfoList()
747:         {
748:                 return typeInfoList;
749:         }
750:
751:         public ADefaultClassDeclIR getInvChecksFlagOwner()
752:         {
753:                 return invChecksFlagOwner;
754:         }
755:
756:         public StateDesInfo getStateDesInfo()
757:         {
758:                 return stateDesInfo;
759:         }
760: }