Method: fullyQualifiedRecType(ARecordTypeIR)

1: package org.overture.codegen.vdm2jml.predgen;
2:
3: import java.util.LinkedList;
4: import java.util.List;
5:
6: import org.apache.commons.lang.BooleanUtils;
7: import org.apache.log4j.Logger;
8: import org.overture.ast.util.ClonableString;
9: import org.overture.codegen.assistant.TypeAssistantIR;
10: import org.overture.codegen.ir.INode;
11: import org.overture.codegen.ir.STypeIR;
12: import org.overture.codegen.ir.declarations.ADefaultClassDeclIR;
13: import org.overture.codegen.ir.declarations.ANamedTypeDeclIR;
14: import org.overture.codegen.ir.expressions.SVarExpIR;
15: import org.overture.codegen.ir.statements.AMetaStmIR;
16: import org.overture.codegen.ir.types.AClassTypeIR;
17: import org.overture.codegen.ir.types.AExternalTypeIR;
18: import org.overture.codegen.ir.types.AMapMapTypeIR;
19: import org.overture.codegen.ir.types.ARecordTypeIR;
20: import org.overture.codegen.ir.types.ASeqSeqTypeIR;
21: import org.overture.codegen.ir.types.ASetSetTypeIR;
22: import org.overture.codegen.ir.types.ATupleTypeIR;
23: import org.overture.codegen.ir.types.AUnionTypeIR;
24: import org.overture.codegen.ir.types.AUnknownTypeIR;
25: import org.overture.codegen.vdm2jml.JmlGenUtil;
26: import org.overture.codegen.vdm2jml.JmlGenerator;
27: import org.overture.codegen.vdm2jml.data.RecClassInfo;
28: import org.overture.codegen.vdm2jml.predgen.info.AbstractTypeInfo;
29: import org.overture.codegen.vdm2jml.predgen.info.LeafTypeInfo;
30: import org.overture.codegen.vdm2jml.predgen.info.MapInfo;
31: import org.overture.codegen.vdm2jml.predgen.info.NamedTypeInfo;
32: import org.overture.codegen.vdm2jml.predgen.info.NamedTypeInvDepCalculator;
33: import org.overture.codegen.vdm2jml.predgen.info.SeqInfo;
34: import org.overture.codegen.vdm2jml.predgen.info.SetInfo;
35: import org.overture.codegen.vdm2jml.predgen.info.TupleInfo;
36: import org.overture.codegen.vdm2jml.predgen.info.UnionInfo;
37: import org.overture.codegen.vdm2jml.predgen.info.UnknownLeaf;
38: import org.overture.codegen.vdm2jml.util.NameGen;
39:
40: public class TypePredUtil
41: {
42:         private TypePredHandler handler;
43:
44:         private Logger log = Logger.getLogger(this.getClass().getName());
45:
46:         public TypePredUtil(TypePredHandler handler)
47:         {
48:                 this.handler = handler;
49:         }
50:
51:         public List<String> consJmlCheck(ADefaultClassDeclIR encClass,
52:                         String jmlVisibility, String annotationType, boolean invChecksGuard,
53:                         AbstractTypeInfo typeInfo, SVarExpIR var)
54:         {
55:                 List<String> predStrs = new LinkedList<>();
56:
57:                 if (handler.getDecorator().buildRecValidChecks())
58:                 {
59:                         appendRecValidChecks(invChecksGuard, typeInfo, var, predStrs, encClass);
60:                 }
61:
62:                 StringBuilder inv = new StringBuilder();
63:                 inv.append("//@ ");
64:
65:                 if (jmlVisibility != null)
66:                 {
67:                         inv.append(jmlVisibility);
68:                         inv.append(' ');
69:                 }
70:
71:                 inv.append(annotationType);
72:                 inv.append(' ');
73:
74:                 if (invChecksGuard)
75:                 {
76:                         inv.append(consInvChecksGuard(encClass));
77:                         inv.append('(');
78:                 }
79:
80:                 String javaPackage = handler.getJmlGen().getJavaSettings().getJavaRootPackage();
81:
82:                 NameGen nameGen = new NameGen(encClass);
83:                 String consCheckExp = typeInfo.consCheckExp(encClass.getName(), javaPackage, var.getName(), nameGen);
84:
85:                 if (consCheckExp != null)
86:                 {
87:                         inv.append(consCheckExp);
88:                 } else
89:                 {
90:                         log.error("Expression could not be checked");
91:                         // TODO: Consider better handling
92:                         inv.append("true");
93:                 }
94:                 if (invChecksGuard)
95:                 {
96:                         inv.append(')');
97:                 }
98:
99:                 inv.append(';');
100:
101:                 predStrs.add(inv.toString());
102:
103:                 return predStrs;
104:         }
105:
106:         private String consInvChecksGuard(ADefaultClassDeclIR encClass)
107:         {
108:                 StringBuilder sb = new StringBuilder();
109:                 sb.append(handler.getJmlGen().getAnnotator().consInvChecksOnNameEncClass(encClass));
110:                 sb.append(JmlGenerator.JML_IMPLIES);
111:
112:                 return sb.toString();
113:         }
114:
115:         private void appendRecValidChecks(boolean invChecksGuard,
116:                         AbstractTypeInfo typeInfo, SVarExpIR var, List<String> predStrs,
117:                         ADefaultClassDeclIR encClass)
118:         {
119:                 List<ARecordTypeIR> recordTypes = getRecTypes(typeInfo);
120:
121:                 if (!recordTypes.isEmpty())
122:                 {
123:                         for (ARecordTypeIR rt : recordTypes)
124:                         {
125:                                 StringBuilder inv = new StringBuilder();
126:                                 String fullyQualifiedRecType = fullyQualifiedRecType(rt);
127:
128:                                 inv.append("//@ ");
129:                                 inv.append(JmlGenerator.JML_ASSERT_ANNOTATION);
130:                                 inv.append(' ');
131:
132:                                 if (invChecksGuard)
133:                                 {
134:                                         inv.append(consInvChecksGuard(encClass));
135:                                 }
136:
137:                                 if (var.getType() instanceof ARecordTypeIR)
138:                                 {
139:                                         if (handler.getJmlGen().getJmlSettings().genInvariantFor())
140:                                         {
141:                                                 inv.append(JmlGenerator.JML_INVARIANT_FOR);
142:                                                 inv.append('(');
143:                                                 inv.append(var.getName());
144:                                                 inv.append(')');
145:                                                 // e.g. invariant_for(r1)
146:                                         } else
147:                                         {
148:                                                 inv.append(var.getName());
149:                                                 inv.append('.');
150:                                                 inv.append(JmlGenerator.REC_VALID_METHOD_CALL);
151:                                                 // e.g. r1.valid()
152:                                         }
153:                                 } else
154:                                 {
155:                                         inv.append(var.getName());
156:                                         inv.append(JmlGenerator.JAVA_INSTANCEOF);
157:                                         inv.append(fullyQualifiedRecType);
158:                                         inv.append(JmlGenerator.JML_IMPLIES);
159:
160:                                         // So far we have:
161:                                         // e.g. r1 instanceof project.Entrytypes.R3
162:
163:                                         if (handler.getJmlGen().getJmlSettings().genInvariantFor())
164:                                         {
165:                                                 inv.append(JmlGenerator.JML_INVARIANT_FOR);
166:                                                 inv.append('(');
167:                                                 inv.append(consRecVarCast(var, fullyQualifiedRecType));
168:                                                 
169:                                                 inv.append(')');
170:
171:                                                 // e.g. r1 instanceof project.Entrytypes.R3 ==> \invariant_for((project.Entrytypes.R3) r1);
172:                                         } else
173:                                         {
174:                                                 inv.append(consRecVarCast(var, fullyQualifiedRecType));
175:                                                 inv.append('.');
176:                                                 inv.append(JmlGenerator.REC_VALID_METHOD_CALL);
177:                                                 // e.g. r1 instanceof project.Entrytypes.R3 ==> ((project.Entrytypes.R3) r1).valid()
178:                                         }
179:                                 }
180:
181:                                 inv.append(';');
182:                                 predStrs.add(inv.toString());
183:                         }
184:                 }
185:         }
186:
187:         private String consRecVarCast(SVarExpIR var, String fullyQualifiedRecType)
188:         {
189:                 return "((" + fullyQualifiedRecType + ") " + var.getName() + ")";
190:         }
191:
192:         public String fullyQualifiedRecType(ARecordTypeIR rt)
193:         {
194:                 String defClass = rt.getName().getDefiningClass();
195:                 String recPackage = JmlGenUtil.consRecPackage(defClass, handler.getJmlGen().getJavaGen().getJavaSettings().getJavaRootPackage());
196:                 String fullyQualifiedRecType = recPackage + "."
197:                                 + rt.getName().getName();
198:                 return fullyQualifiedRecType;
199:         }
200:
201:         private List<ARecordTypeIR> getRecTypes(AbstractTypeInfo typeInfo)
202:         {
203:                 List<ARecordTypeIR> recTypes = new LinkedList<>();
204:
205:                 List<LeafTypeInfo> leaves = typeInfo.getLeafTypesRecursively();
206:
207:                 for (LeafTypeInfo leaf : leaves)
208:                 {
209:                         if (leaf.getType() instanceof ARecordTypeIR)
210:                         {
211:                                 recTypes.add((ARecordTypeIR) leaf.getType());
212:                         }
213:                 }
214:
215:                 return recTypes;
216:         }
217:
218:         public List<AMetaStmIR> consAssertStm(AbstractTypeInfo invTypes,
219:                         ADefaultClassDeclIR encClass, SVarExpIR var, INode node,
220:                         RecClassInfo recInfo)
221:         {
222:                 boolean inAccessor = node != null && recInfo != null
223:                                 && recInfo.inAccessor(node);
224:
225:                 List<AMetaStmIR> asserts = new LinkedList<>();
226:                 List<String> assertStrs = consJmlCheck(encClass, null, JmlGenerator.JML_ASSERT_ANNOTATION, inAccessor, invTypes, var);
227:
228:                 for (String a : assertStrs)
229:                 {
230:                         AMetaStmIR assertStm = new AMetaStmIR();
231:                         List<ClonableString> assertMetaData = handler.getJmlGen().getAnnotator().consMetaData(a);
232:                         handler.getJmlGen().getAnnotator().appendMetaData(assertStm, assertMetaData);
233:                         asserts.add(assertStm);
234:                 }
235:
236:                 return asserts;
237:         }
238:
239:         public AMetaStmIR consVarNotNullAssert(String varName)
240:         {
241:                 AMetaStmIR assertStm = new AMetaStmIR();
242:                 List<ClonableString> assertMetaData = handler.getJmlGen().getAnnotator().consMetaData("//@ assert "
243:                                 + varName + " != null;");
244:                 handler.getJmlGen().getAnnotator().appendMetaData(assertStm, assertMetaData);
245:
246:                 return assertStm;
247:         }
248:
249:         public AbstractTypeInfo findTypeInfo(STypeIR type)
250:         {
251:                 TypeAssistantIR assist = handler.getJmlGen().getJavaGen().getInfo().getTypeAssistant();
252:
253:                 if (type.getNamedInvType() != null)
254:                 {
255:                         ANamedTypeDeclIR namedInv = type.getNamedInvType();
256:
257:                         String defModule = namedInv.getName().getDefiningClass();
258:                         String typeName = namedInv.getName().getName();
259:
260:                         NamedTypeInfo info = NamedTypeInvDepCalculator.findTypeInfo(handler.getJmlGen().getTypeInfoList(), defModule, typeName);
261:
262:                         if (assist.isOptional(type))
263:                         {
264:                                 info = new NamedTypeInfo(info.getTypeName(), info.getDefModule(), info.hasInv(), true, info.getDomainType());
265:                         }
266:
267:                         if (info == null)
268:                         {
269:                                 log.error("Could not find info for named type '" + typeName
270:                                                 + "' defined in module '" + defModule);
271:                         }
272:
273:                         return info;
274:
275:                         // We do not need to collect sub named invariant types
276:                 } else
277:                 {
278:                         if (type instanceof AUnionTypeIR)
279:                         {
280:                                 List<AbstractTypeInfo> types = new LinkedList<>();
281:
282:                                 for (STypeIR t : ((AUnionTypeIR) type).getTypes())
283:                                 {
284:                                         types.add(findTypeInfo(t));
285:                                 }
286:
287:                                 return new UnionInfo(assist.isOptional(type), types);
288:                         } else if (type instanceof ATupleTypeIR)
289:                         {
290:                                 List<AbstractTypeInfo> types = new LinkedList<>();
291:
292:                                 for (STypeIR t : ((ATupleTypeIR) type).getTypes())
293:                                 {
294:                                         types.add(findTypeInfo(t));
295:                                 }
296:
297:                                 return new TupleInfo(assist.isOptional(type), types);
298:                         } else if (type instanceof ASeqSeqTypeIR)
299:                         {
300:                                 ASeqSeqTypeIR seqType = (ASeqSeqTypeIR) type;
301:                                 STypeIR elementType = seqType.getSeqOf();
302:
303:                                 return new SeqInfo(assist.isOptional(seqType), findTypeInfo(elementType), BooleanUtils.isTrue(seqType.getSeq1()));
304:                         } else if (type instanceof ASetSetTypeIR)
305:                         {
306:                                 ASetSetTypeIR setType = (ASetSetTypeIR) type;
307:                                 STypeIR elementType = setType.getSetOf();
308:
309:                                 return new SetInfo(assist.isOptional(setType), findTypeInfo(elementType));
310:                         } else if (type instanceof AMapMapTypeIR)
311:                         {
312:                                 AMapMapTypeIR mapType = (AMapMapTypeIR) type;
313:
314:                                 AbstractTypeInfo domInfo = findTypeInfo(mapType.getFrom());
315:                                 AbstractTypeInfo rngInfo = findTypeInfo(mapType.getTo());
316:
317:                                 boolean injective = BooleanUtils.isTrue(mapType.getInjective());
318:
319:                                 return new MapInfo(assist.isOptional(mapType), domInfo, rngInfo, injective);
320:
321:                         } else if (type instanceof AUnknownTypeIR
322:                                         || type instanceof AClassTypeIR
323:                                         || type instanceof AExternalTypeIR)
324:                         {
325:                                 // Iterators are class types for instance
326:                                 return new UnknownLeaf();
327:                         } else
328:                         {
329:                                 return new LeafTypeInfo(type, assist.isOptional(type));
330:                         }
331:                 }
332:         }
333: }