Package: TypePredDecorator

TypePredDecorator

nameinstructionbranchcomplexitylinemethod
TypePredDecorator(JmlGenerator, StateDesInfo, RecClassInfo)
M: 0 C: 31
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
add(ABlockStmIR, AMetaStmIR)
M: 0 C: 8
100%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 3
100%
M: 0 C: 1
100%
add(List, AMetaStmIR)
M: 0 C: 7
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
addAsserts(List, AIdentifierVarExpIR)
M: 0 C: 29
100%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 0 C: 8
100%
M: 0 C: 1
100%
addStateDesAsserts(SVarExpIR, List, ABlockStmIR)
M: 0 C: 19
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
addStateDesAssertsAtomic(SVarExpIR, List)
M: 0 C: 18
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
addSubjectAssertAtomic(AMetaStmIR, List)
M: 0 C: 18
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
addSubjectAsserts(AMetaStmIR, List, ABlockStmIR)
M: 0 C: 20
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
buildRecValidChecks()
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%
caseAAssignToExpStmIR(AAssignToExpStmIR)
M: 0 C: 8
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseABlockStmIR(ABlockStmIR)
M: 0 C: 5
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseACallObjectExpStmIR(ACallObjectExpStmIR)
M: 24 C: 36
60%
M: 2 C: 4
67%
M: 2 C: 2
50%
M: 4 C: 11
73%
M: 0 C: 1
100%
caseADefaultClassDeclIR(ADefaultClassDeclIR)
M: 0 C: 5
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAFieldDeclIR(AFieldDeclIR)
M: 0 C: 5
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAMapSeqUpdateStmIR(AMapSeqUpdateStmIR)
M: 12 C: 23
66%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 2 C: 5
71%
M: 0 C: 1
100%
caseAMethodDeclIR(AMethodDeclIR)
M: 0 C: 10
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
caseAReturnStmIR(AReturnStmIR)
M: 0 C: 5
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAVarDeclIR(AVarDeclIR)
M: 16 C: 47
75%
M: 5 C: 11
69%
M: 4 C: 5
56%
M: 4 C: 13
76%
M: 0 C: 1
100%
consObjVarAsserts(SVarExpIR, List)
M: 4 C: 44
92%
M: 2 C: 6
75%
M: 2 C: 3
60%
M: 1 C: 9
90%
M: 0 C: 1
100%
consSubjectAsserts(AMetaStmIR, List)
M: 0 C: 27
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 7
100%
M: 0 C: 1
100%
getRecInfo()
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%
getTypePredUtil()
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%
handleStateUpdate(ACallObjectExpStmIR, SVarExpIR)
M: 0 C: 17
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
handleStateUpdate(SStmIR, SVarExpIR, List, AMetaStmIR, List)
M: 0 C: 46
100%
M: 0 C: 8
100%
M: 0 C: 5
100%
M: 0 C: 12
100%
M: 0 C: 1
100%

Coverage

1: package org.overture.codegen.vdm2jml.predgen;
2:
3: import java.util.Collections;
4: import java.util.LinkedList;
5: import java.util.List;
6:
7: import org.apache.log4j.Logger;
8: import org.overture.codegen.ir.SStmIR;
9: import org.overture.codegen.ir.analysis.AnalysisException;
10: import org.overture.codegen.ir.declarations.ADefaultClassDeclIR;
11: import org.overture.codegen.ir.declarations.AFieldDeclIR;
12: import org.overture.codegen.ir.declarations.AMethodDeclIR;
13: import org.overture.codegen.ir.declarations.AVarDeclIR;
14: import org.overture.codegen.ir.expressions.ACastUnaryExpIR;
15: import org.overture.codegen.ir.expressions.AIdentifierVarExpIR;
16: import org.overture.codegen.ir.expressions.SVarExpIR;
17: import org.overture.codegen.ir.statements.AAssignToExpStmIR;
18: import org.overture.codegen.ir.statements.ABlockStmIR;
19: import org.overture.codegen.ir.statements.ACallObjectExpStmIR;
20: import org.overture.codegen.ir.statements.AMapSeqUpdateStmIR;
21: import org.overture.codegen.ir.statements.AMetaStmIR;
22: import org.overture.codegen.ir.statements.AReturnStmIR;
23: import org.overture.codegen.traces.TraceMethodTag;
24: import org.overture.codegen.vdm2jml.JmlGenerator;
25: import org.overture.codegen.vdm2jml.data.RecClassInfo;
26: import org.overture.codegen.vdm2jml.data.StateDesInfo;
27: import org.overture.codegen.vdm2jml.trans.RecAccessorTrans;
28: import org.overture.codegen.vdm2jml.trans.TargetNormaliserTrans;
29:
30: /**
31: * This class is responsible for adding additional checks, like assertions, to the IR to preserve the semantics of the
32: * contract-based notations of VDM-SL when they are translated to JML annotated Java.
33: *
34: * @see RecAccessorTrans
35: * @see TargetNormaliserTrans
36: */
37: public class TypePredDecorator extends AtomicAssertTrans
38: {
39:         private RecModHandler recHandler;
40:         private TypePredHandler namedTypeHandler;
41:         private StateDesInfo stateDesInfo;
42:         private RecClassInfo recInfo;
43:
44:         private boolean buildRecChecks = false;
45:
46:         private Logger log = Logger.getLogger(this.getClass().getName());
47:
48:         public TypePredDecorator(JmlGenerator jmlGen, StateDesInfo stateDesInfo,
49:                         RecClassInfo recInfo)
50:         {
51:                 super(jmlGen);
52:                 this.recHandler = new RecModHandler(this);
53:                 this.namedTypeHandler = new TypePredHandler(this);
54:                 this.stateDesInfo = stateDesInfo;
55:                 this.recInfo = recInfo;
56:         }
57:
58:         @Override
59:         public void caseACallObjectExpStmIR(ACallObjectExpStmIR node)
60:                         throws AnalysisException
61:         {
62:•                if (node.getObj() instanceof SVarExpIR)
63:                 {
64:                         SVarExpIR obj = (SVarExpIR) node.getObj();
65:                         handleStateUpdate(node, obj);
66:•                } else if (node.getObj() instanceof ACastUnaryExpIR)
67:                 {
68:                         ACastUnaryExpIR cast = (ACastUnaryExpIR) node.getObj();
69:
70:•                        if (cast.getExp() instanceof SVarExpIR)
71:                         {
72:                                 SVarExpIR obj = (SVarExpIR) cast.getExp();
73:                                 handleStateUpdate(node, obj);
74:                         } else
75:                         {
76:                                 log.error("Expected subject of cast expression to be a variable expression at this point. Got: "
77:                                                 + cast.getExp());
78:                         }
79:                 } else
80:                 {
81:                         log.error("Expected object of call object statement "
82:                                         + " to be a variable or cast expression by now. Got: "
83:                                         + node.getObj());
84:                 }
85:         }
86:
87:         private void handleStateUpdate(ACallObjectExpStmIR node, SVarExpIR obj)
88:         {
89:                 handleStateUpdate(node, obj, stateDesInfo.getStateDesVars(node), recHandler.handleCallObj(node), namedTypeHandler.handleCallObj(node));
90:         }
91:
92:         @Override
93:         public void caseAFieldDeclIR(AFieldDeclIR node) throws AnalysisException
94:         {
95:                 namedTypeHandler.handleField(node);
96:         }
97:
98:         @Override
99:         public void caseABlockStmIR(ABlockStmIR node) throws AnalysisException
100:         {
101:                 namedTypeHandler.handleBlock(node);
102:         }
103:
104:         @Override
105:         public void caseAVarDeclIR(AVarDeclIR node) throws AnalysisException
106:         {
107:                 /**
108:                  * Variable declarations occurring inside an atomic statement do not need handling. The reason for this is that
109:                  * the call statement and the map/seq update cases currently take care of generating the assertions for variable
110:                  * expressions used to represent state designators. TODO: Make this case handle state designators
111:                  */
112:•                if (inAtomic())
113:                 {
114:                         return;
115:                 }
116:
117:•                if (stateDesInfo.isStateDesDecl(node))
118:                 {
119:                         return;
120:                 }
121:
122:                 /**
123:                  * Since the target of map/seq updates (e.g. Utils.mapsSeqUpdate(stateDes_3, 4, 'a')) and call object statements
124:                  * (e.g. stateDes_3.set_x("a")) (i.e. assignments in the VDM-SL model) are split into variables named stateDes_
125:                  * <n> we can also expect local variable declarations in atomic statement blocks
126:                  */
127:                 List<AMetaStmIR> as = namedTypeHandler.handleVarDecl(node);
128:
129:•                if (as == null || as.isEmpty())
130:                 {
131:                         return;
132:                 }
133:
134:                 ABlockStmIR encBlock = namedTypeHandler.getEncBlockStm(node);
135:
136:•                if (encBlock == null)
137:                 {
138:                         return;
139:                 }
140:
141:                 /**
142:                  * The variable declaration is a local declaration of the statement block. Therefore, making the assertion the
143:                  * first statement in the statement block makes the assertion appear immediately right after the variable
144:                  * declaration.
145:                  */
146:•                if (inAtomic())
147:                 {
148:•                        for (AMetaStmIR a : as)
149:                         {
150:                                 addPostAtomicCheck(a);
151:                         }
152:                 } else
153:                 {
154:•                        for (int i = as.size() - 1; i >= 0; i--)
155:                         {
156:                                 encBlock.getStatements().addFirst(as.get(i));
157:                         }
158:                 }
159:         }
160:
161:         @Override
162:         public void caseAAssignToExpStmIR(AAssignToExpStmIR node)
163:                         throws AnalysisException
164:         {
165:                 /**
166:                  * Record modifications are now all on the form E.g. St = <recvalue>, i.e. node.getTarget() instanceof SVarExpIR
167:                  * && node.getTarget().getType() instanceof ARecordTypeIR. Invariant violations will therefore be detected when
168:                  * the record value is constructed or it appears in the temporary variable section if the assignment occurs in
169:                  * the context of an atomic statement block. Therefore, no record invariant needs to be asserted. Note that more
170:                  * complicated record modifications (e.g. rec1.rec2.f := 5) appear as nodes of type caseACallObjectExpStmIR
171:                  */
172:
173:•                if (!inAtomic())
174:                 {
175:                         namedTypeHandler.handleAssign(node);
176:                 }
177:         }
178:
179:         @Override
180:         public void caseAMapSeqUpdateStmIR(AMapSeqUpdateStmIR node)
181:                         throws AnalysisException
182:         {
183:•                if (node.getCol() instanceof SVarExpIR)
184:                 {
185:                         SVarExpIR col = (SVarExpIR) node.getCol();
186:                         handleStateUpdate(node, col, stateDesInfo.getStateDesVars(node), null, namedTypeHandler.handleMapSeq(node));
187:                 } else
188:                 {
189:                         log.error("Expected collection of map/sequence"
190:                                         + " update to be a variable expression by now. Got: "
191:                                         + node.getCol());
192:                 }
193:         }
194:
195:         @Override
196:         public void caseAMethodDeclIR(AMethodDeclIR node) throws AnalysisException
197:         {
198:•                if (node.getTag() instanceof TraceMethodTag)
199:                 {
200:                         return;
201:                 }
202:
203:                 namedTypeHandler.handleMethod(node);
204:         }
205:
206:         @Override
207:         public void caseAReturnStmIR(AReturnStmIR node) throws AnalysisException
208:         {
209:                 namedTypeHandler.handleReturn(node);
210:         }
211:
212:         @Override
213:         public void caseADefaultClassDeclIR(ADefaultClassDeclIR node)
214:                         throws AnalysisException
215:         {
216:                 namedTypeHandler.handleClass(node);
217:         }
218:
219:         private void handleStateUpdate(SStmIR node, SVarExpIR target,
220:                         List<AIdentifierVarExpIR> objVars, AMetaStmIR recAssert,
221:                         List<AMetaStmIR> namedTypeInvAssert)
222:         {
223:•                if (recAssert == null && namedTypeInvAssert == null && objVars == null)
224:                 {
225:                         return;
226:                 }
227:
228:•                if (!inAtomic())
229:                 {
230:                         // NOT inside atomic statement block
231:                         ABlockStmIR replBlock = new ABlockStmIR();
232:                         jmlGen.getJavaGen().getTransAssistant().replaceNodeWith(node, replBlock);
233:                         replBlock.getStatements().add(node);
234:
235:                         addSubjectAsserts(recAssert, namedTypeInvAssert, replBlock);
236:                         addStateDesAsserts(target, objVars, replBlock);
237:                 } else
238:                 {
239:                         // We'll store the checks and let the atomic statement case handle the assert insertion
240:                         addSubjectAssertAtomic(recAssert, namedTypeInvAssert);
241:                         addStateDesAssertsAtomic(target, objVars);
242:                 }
243:         }
244:
245:         private void addSubjectAssertAtomic(AMetaStmIR recAssert,
246:                         List<AMetaStmIR> namedTypeInvAssert)
247:         {
248:•                for (AMetaStmIR a : consSubjectAsserts(recAssert, namedTypeInvAssert))
249:                 {
250:                         addPostAtomicCheck(a);
251:                 }
252:         }
253:
254:         private void addSubjectAsserts(AMetaStmIR recAssert,
255:                         List<AMetaStmIR> namedTypeInvAssert, ABlockStmIR replBlock)
256:         {
257:•                for (AMetaStmIR a : consSubjectAsserts(recAssert, namedTypeInvAssert))
258:                 {
259:                         replBlock.getStatements().add(a);
260:                 }
261:         }
262:
263:         private List<AMetaStmIR> consSubjectAsserts(AMetaStmIR recAssert,
264:                         List<AMetaStmIR> namedTypeInvAsserts)
265:         {
266:                 List<AMetaStmIR> allAsserts = new LinkedList<AMetaStmIR>();
267:
268:                 add(allAsserts, recAssert);
269:
270:•                if (namedTypeInvAsserts != null)
271:                 {
272:•                        for (AMetaStmIR a : namedTypeInvAsserts)
273:                         {
274:                                 add(allAsserts, a);
275:                         }
276:                 }
277:
278:                 return allAsserts;
279:         }
280:
281:         private void addStateDesAssertsAtomic(SVarExpIR target,
282:                         List<AIdentifierVarExpIR> objVars)
283:         {
284:•                for (AMetaStmIR a : consObjVarAsserts(target, objVars))
285:                 {
286:                         addPostAtomicCheck(a);
287:                 }
288:         }
289:
290:         private void addStateDesAsserts(SVarExpIR target,
291:                         List<AIdentifierVarExpIR> objVars, ABlockStmIR replBlock)
292:         {
293:•                for (AMetaStmIR a : consObjVarAsserts(target, objVars))
294:                 {
295:                         add(replBlock, a);
296:                 }
297:         }
298:
299:         private List<AMetaStmIR> consObjVarAsserts(SVarExpIR target,
300:                         List<AIdentifierVarExpIR> objVars)
301:         {
302:                 List<AMetaStmIR> objVarAsserts = new LinkedList<AMetaStmIR>();
303:
304:•                if (objVars != null)
305:                 {
306:                         // All of them except the last
307:•                        for (int i = 0; i < objVars.size() - 1; i++)
308:                         {
309:                                 addAsserts(objVarAsserts, objVars.get(i));
310:                         }
311:
312:•                        if (!objVarAsserts.isEmpty())
313:                         {
314:                                 AIdentifierVarExpIR last = objVars.get(objVars.size() - 1);
315:
316:•                                if (!target.getName().equals(last.getName()))
317:                                 {
318:                                         addAsserts(objVarAsserts, last);
319:                                 }
320:                         }
321:                 }
322:
323:                 Collections.reverse(objVarAsserts);
324:                 return objVarAsserts;
325:         }
326:
327:         private void addAsserts(List<AMetaStmIR> objVarAsserts,
328:                         AIdentifierVarExpIR var)
329:         {
330:                 buildRecChecks = true;
331:                 List<AMetaStmIR> asserts = namedTypeHandler.consAsserts(var);
332:                 buildRecChecks = false;
333:
334:•                if (asserts != null)
335:                 {
336:•                        for (AMetaStmIR a : asserts)
337:                         {
338:                                 add(objVarAsserts, a);
339:                         }
340:                 }
341:         }
342:
343:         private void add(List<AMetaStmIR> asserts, AMetaStmIR as)
344:         {
345:•                if (as != null)
346:                 {
347:                         asserts.add(as);
348:                 }
349:         }
350:
351:         private void add(ABlockStmIR block, AMetaStmIR as)
352:         {
353:•                if (as != null)
354:                 {
355:                         block.getStatements().add(as);
356:                 }
357:         }
358:
359:         public RecClassInfo getRecInfo()
360:         {
361:                 return recInfo;
362:         }
363:
364:         public StateDesInfo getStateDesInfo()
365:         {
366:                 return stateDesInfo;
367:         }
368:
369:         public boolean buildRecValidChecks()
370:         {
371:                 return buildRecChecks;
372:         }
373:
374:         public TypePredUtil getTypePredUtil()
375:         {
376:                 return this.namedTypeHandler.getTypePredUtil();
377:         }
378: }