Package: RecInvTransformation

RecInvTransformation

nameinstructionbranchcomplexitylinemethod
RecInvTransformation(JavaCodeGen, ARecordDeclIR)
M: 0 C: 17
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
caseAExplicitVarExpIR(AExplicitVarExpIR)
M: 43 C: 0
0%
M: 4 C: 0
0%
M: 3 C: 0
0%
M: 9 C: 0
0%
M: 1 C: 0
0%
caseAIdentifierVarExpIR(AIdentifierVarExpIR)
M: 85 C: 59
41%
M: 6 C: 10
63%
M: 4 C: 5
56%
M: 18 C: 15
45%
M: 0 C: 1
100%
changeRecInvSignature()
M: 48 C: 94
66%
M: 5 C: 5
50%
M: 4 C: 2
33%
M: 10 C: 19
66%
M: 0 C: 1
100%
consUniqueName(String)
M: 0 C: 9
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
terminate()
M: 5 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%

Coverage

1: package org.overture.codegen.vdm2jml.trans;
2:
3: import org.apache.log4j.Logger;
4: import org.overture.ast.definitions.SFunctionDefinition;
5: import org.overture.ast.definitions.SOperationDefinition;
6: import org.overture.ast.expressions.AVariableExp;
7: import org.overture.ast.node.INode;
8: import org.overture.codegen.ir.STypeIR;
9: import org.overture.codegen.ir.SourceNode;
10: import org.overture.codegen.ir.analysis.AnalysisException;
11: import org.overture.codegen.ir.analysis.DepthFirstAnalysisAdaptor;
12: import org.overture.codegen.ir.declarations.ADefaultClassDeclIR;
13: import org.overture.codegen.ir.declarations.AFieldDeclIR;
14: import org.overture.codegen.ir.declarations.AFormalParamLocalParamIR;
15: import org.overture.codegen.ir.declarations.AMethodDeclIR;
16: import org.overture.codegen.ir.declarations.ARecordDeclIR;
17: import org.overture.codegen.ir.expressions.AExplicitVarExpIR;
18: import org.overture.codegen.ir.expressions.AFieldExpIR;
19: import org.overture.codegen.ir.expressions.AIdentifierVarExpIR;
20: import org.overture.codegen.ir.patterns.AIdentifierPatternIR;
21: import org.overture.codegen.ir.types.ABoolBasicTypeIR;
22: import org.overture.codegen.ir.types.AClassTypeIR;
23: import org.overture.codegen.ir.types.AMethodTypeIR;
24: import org.overture.codegen.trans.assistants.TransAssistantIR;
25: import org.overture.codegen.vdm2java.JavaCodeGen;
26: import org.overture.codegen.vdm2java.JavaCodeGenUtil;
27:
28: public class RecInvTransformation extends DepthFirstAnalysisAdaptor
29: {
30:         private JavaCodeGen javaGen;
31:         private String paramName;
32:         private ARecordDeclIR rec;
33:
34:         private Logger log = Logger.getLogger(this.getClass().getName());
35:
36:         public RecInvTransformation(JavaCodeGen javaGen, ARecordDeclIR rec)
37:                         throws AnalysisException
38:         {
39:                 this.javaGen = javaGen;
40:                 this.rec = rec;
41:                 changeRecInvSignature();
42:         }
43:
44:         private void changeRecInvSignature() throws AnalysisException
45:         {
46:•                if (!(rec.getInvariant() instanceof AMethodDeclIR))
47:                 {
48:                         log.error("Expected invariant to be a method declaration. Got: "
49:                                         + rec.getInvariant());
50:                         terminate();
51:                 }
52:
53:                 AMethodDeclIR invMethod = (AMethodDeclIR) rec.getInvariant();
54:
55:•                if (invMethod.getFormalParams().size() != 1)
56:                 {
57:                         log.error("Expected invariant to take a single argument. Instead it takes "
58:                                         + invMethod.getFormalParams().size());
59:
60:•                        if (invMethod.getFormalParams().isEmpty())
61:                         {
62:                                 terminate();
63:                         }
64:                 }
65:
66:                 AFormalParamLocalParamIR param = invMethod.getFormalParams().getFirst();
67:
68:•                if (!(param.getPattern() instanceof AIdentifierPatternIR))
69:                 {
70:                         log.error("Expected pattern of formal parameter to be an identifier pattern at this point. Got "
71:                                         + param.getPattern());
72:
73:                         terminate();
74:                 }
75:
76:                 // First update the signature of the invariant method to take the fields
77:
78:                 invMethod.setMethodType(null);
79:                 invMethod.getFormalParams().clear();
80:
81:                 AMethodTypeIR newMethodType = new AMethodTypeIR();
82:                 newMethodType.setResult(new ABoolBasicTypeIR());
83:                 invMethod.setMethodType(newMethodType);
84:
85:•                for (AFieldDeclIR f : rec.getFields())
86:                 {
87:                         newMethodType.getParams().add(f.getType().clone());
88:
89:                         AFormalParamLocalParamIR nextParam = new AFormalParamLocalParamIR();
90:                         nextParam.setPattern(javaGen.getInfo().getPatternAssistant().consIdPattern(consUniqueName(f.getName())));
91:                         nextParam.setType(f.getType().clone());
92:
93:                         invMethod.getFormalParams().add(nextParam);
94:                 }
95:
96:                 this.paramName = ((AIdentifierPatternIR) param.getPattern()).getName();
97:         }
98:
99:         private void terminate() throws AnalysisException
100:         {
101:                 throw new AnalysisException("Invalid record invariant - transformation cannot be applied. See error log.");
102:         }
103:
104:         @Override
105:         public void caseAExplicitVarExpIR(AExplicitVarExpIR node)
106:                         throws AnalysisException
107:         {
108:                 String pack = javaGen.getJavaSettings().getJavaRootPackage();
109:
110:•                if (JavaCodeGenUtil.isValidJavaPackage(pack))
111:                 {
112:                         STypeIR type = node.getClassType();
113:
114:•                        if (type instanceof AClassTypeIR)
115:                         {
116:                                 AClassTypeIR classType = (AClassTypeIR) type;
117:                                 classType.setName(pack + "." + classType.getName());
118:                         } else
119:                         {
120:                                 log.error("Expected type of explicit variable to be a class type at this point. Got: "
121:                                                 + type);
122:                         }
123:                 }
124:         }
125:
126:         @Override
127:         public void caseAIdentifierVarExpIR(AIdentifierVarExpIR node)
128:                         throws AnalysisException
129:         {
130:•                if (node.parent() instanceof AFieldExpIR
131:•                                && node.getName().equals(paramName))
132:                 {
133:                         AFieldExpIR field = (AFieldExpIR) node.parent();
134:
135:                         TransAssistantIR assistant = javaGen.getTransAssistant();
136:                         AIdentifierVarExpIR replField = javaGen.getInfo().getExpAssistant().consIdVar(consUniqueName(field.getMemberName()), field.getType().clone());
137:                         assistant.replaceNodeWith(field, replField);
138:                 } else
139:                 {
140:                         SourceNode sourceNode = node.getSourceNode();
141:•                        if (sourceNode != null)
142:                         {
143:                                 INode vdmNode = sourceNode.getVdmNode();
144:
145:•                                if (vdmNode instanceof AVariableExp)
146:                                 {
147:                                         AVariableExp varExp = (AVariableExp) vdmNode;
148:
149:•                                        if (varExp.getVardef() instanceof SFunctionDefinition
150:•                                                        || varExp.getVardef() instanceof SOperationDefinition)
151:                                         {
152:                                                 ADefaultClassDeclIR encClass = rec.getAncestor(ADefaultClassDeclIR.class);
153:
154:•                                                if (encClass != null)
155:                                                 {
156:                                                         String defClass = "";
157:
158:•                                                        if (JavaCodeGenUtil.isValidJavaPackage(encClass.getPackage()))
159:                                                         {
160:                                                                 defClass += encClass.getPackage() + ".";
161:                                                         }
162:
163:                                                         defClass += encClass.getName();
164:
165:                                                         AExplicitVarExpIR func = new AExplicitVarExpIR();
166:
167:                                                         AClassTypeIR classType = new AClassTypeIR();
168:                                                         classType.setName(defClass);
169:
170:                                                         func.setClassType(classType);
171:                                                         func.setIsLambda(false);
172:                                                         func.setIsLocal(false);
173:                                                         func.setSourceNode(sourceNode);
174:                                                         func.setName(node.getName());
175:
176:                                                         javaGen.getTransAssistant().replaceNodeWith(node, func);
177:                                                 } else
178:                                                 {
179:                                                         log.error("Could not find enclosing class of record "
180:                                                                         + rec.getName());
181:                                                 }
182:                                         }
183:                                 }
184:                         }
185:                 }
186:         }
187:
188:         /**
189:          * TODO: Constructing names like this will work since names on the form _<name> cannot appear in a VDM model. What
190:          * is not so nice about this approach is that it uses the naming conventions of an old name in the IR. Please note
191:          * that since this method is used to construct names that appear inside an invariant no old name will ever appear. A
192:          * better solution than the current one would be to pick a name that is not already used in the scope the name is
193:          * constructed for.
194:          */
195:         private String consUniqueName(String name)
196:         {
197:                 return "_" + name;
198:         }
199: }