Package: TypeChecker$1

TypeChecker$1

nameinstructionbranchcomplexitylinemethod
equals(Object)
M: 0 C: 31
100%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 0 C: 7
100%
M: 0 C: 1
100%
hashCode()
M: 0 C: 8
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
{...}
M: 0 C: 11
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%

Coverage

1: /*******************************************************************************
2: *
3: *        Copyright (c) 2008 Fujitsu Services Ltd.
4: *
5: *        Author: Nick Battle
6: *
7: *        This file is part of VDMJ.
8: *
9: *        VDMJ is free software: you can redistribute it and/or modify
10: *        it under the terms of the GNU General Public License as published by
11: *        the Free Software Foundation, either version 3 of the License, or
12: *        (at your option) any later version.
13: *
14: *        VDMJ is distributed in the hope that it will be useful,
15: *        but WITHOUT ANY WARRANTY; without even the implied warranty of
16: *        MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17: *        GNU General Public License for more details.
18: *
19: *        You should have received a copy of the GNU General Public License
20: *        along with VDMJ. If not, see <http://www.gnu.org/licenses/>.
21: *
22: ******************************************************************************/
23:
24: package org.overture.typechecker;
25:
26: import java.io.PrintWriter;
27: import java.util.HashMap;
28: import java.util.List;
29: import java.util.Map;
30: import java.util.Stack;
31: import java.util.Vector;
32:
33: import org.overture.ast.definitions.PDefinition;
34: import org.overture.ast.intf.lex.ILexLocation;
35: import org.overture.ast.intf.lex.ILexNameToken;
36: import org.overture.ast.lex.LexNameSet;
37: import org.overture.ast.lex.LexNameToken;
38: import org.overture.ast.messages.InternalException;
39: import org.overture.ast.types.SInvariantType;
40: import org.overture.parser.messages.VDMError;
41: import org.overture.parser.messages.VDMMessage;
42: import org.overture.parser.messages.VDMWarning;
43: import org.overture.typechecker.assistant.ITypeCheckerAssistantFactory;
44: import org.overture.typechecker.assistant.TypeCheckerAssistantFactory;
45: import org.overture.typechecker.assistant.definition.PDefinitionAssistantTC;
46: import org.overture.typechecker.utilities.FreeVarInfo;
47:
48: /**
49: * The abstract root of all type checker classes.
50: */
51:
52: abstract public class TypeChecker
53: {
54:         private static boolean suppress=false;
55:
56:         public interface IStatusListener
57:         {
58:                 void report(VDMError error);
59:
60:                 void warning(VDMWarning warning);
61:         }
62:
63:         private static List<VDMError> errors = new Vector<VDMError>();
64:         private static List<VDMWarning> warnings = new Vector<VDMWarning>();
65:         private static VDMMessage lastMessage = null;
66:         private static final int MAX = 200;
67:
68:         final protected ITypeCheckerAssistantFactory assistantFactory;
69:
70:         static List<IStatusListener> listners = new Vector<IStatusListener>();
71:
72:         /**
73:          * VDM-only constructor. <b>NOT</b> for use by extensions.
74:          */
75:         public TypeChecker()
76:         {
77:                 clearErrors();
78:                 this.assistantFactory = new TypeCheckerAssistantFactory();
79:         }
80:
81:         public TypeChecker(ITypeCheckerAssistantFactory factory)
82:         {
83:                 clearErrors();
84:                 this.assistantFactory = factory;
85:         }
86:
87:         abstract public void typeCheck();
88:
89:         /**
90:          * Check for cyclic dependencies between the free variables that definitions depend
91:          * on and the definition of those variables.
92:          */
93:         protected void cyclicDependencyCheck(List<PDefinition> defs)
94:         {
95:                 if (System.getProperty("skip.cyclic.check") != null)
96:                 {
97:                         return;                // For now, to allow us to skip if there are issues.
98:                 }
99:                 
100:                 if (getErrorCount() > 0)
101:                 {
102:                         return;                // Can't really check everything until it's clean
103:                 }
104:                 
105:                 Map<ILexNameToken, LexNameSet> dependencies = new HashMap<ILexNameToken, LexNameSet>();
106:                 LexNameSet skip = new LexNameSet();
107:                 PDefinitionAssistantTC assistant = assistantFactory.createPDefinitionAssistant();
108:                 Environment globals = new FlatEnvironment(assistantFactory, defs, null);
109:
110:         for (PDefinition def: defs)
111:         {
112:                 Environment env = new FlatEnvironment(assistantFactory, new Vector<PDefinition>());
113:                 FreeVarInfo empty = new FreeVarInfo(globals, env, false);
114:                         LexNameSet freevars = assistant.getFreeVariables(def, empty);
115:                         
116:                         if (!freevars.isEmpty())
117:                         {
118:                         for (ILexNameToken name: assistant.getVariableNames(def))
119:                         {
120:                                 dependencies.put(nameFix(name.getExplicit(true)), nameFix(freevars));
121:                         }
122:                         }
123:                         
124:                         // Skipped definition names occur in the cycle path, but are not checked
125:                         // for cycles themselves, because they are not "initializable".
126:                         
127:                         if (assistant.isTypeDefinition(def) || assistant.isOperation(def))
128:                         {
129:                                 if (def.getName() != null)
130:                                 {
131:                                         skip.add(nameFix(def.getName().getExplicit(true)));
132:                                 }
133:                         }
134:         }
135:         
136:                 for (ILexNameToken sought: dependencies.keySet())
137:                 {
138:                         if (!skip.contains(sought))
139:                         {
140:                         Stack<ILexNameToken> stack = new Stack<ILexNameToken>();
141:                         stack.push(sought);
142:                         
143:                         if (reachable(sought, dependencies.get(sought), dependencies, stack))
144:                         {
145:                          report(3355, "Cyclic dependency detected for " + sought, sought.getLocation());
146:                          detail("Cycle", stack.toString());
147:                         }
148:                         
149:                         stack.pop();
150:                         }
151:                 }
152:         }
153:         
154:         /**
155:          * We have to "fix" names to include equals and hashcode methods that take the type qualifier
156:          * into account. This is so that we can distinguish (say) f(nat) and f(char). It also allows
157:          * us to realise that f(nat1) and f(nat) are "the same".
158:          */
159:
160:         private LexNameSet nameFix(LexNameSet names)
161:         {
162:                 LexNameSet result = new LexNameSet();
163:                 
164:                 for (ILexNameToken name: names)
165:                 {
166:                         result.add(nameFix(name));
167:                 }
168:                 
169:                 return result;
170:         }
171:
172:         private ILexNameToken nameFix(ILexNameToken name)
173:         {
174:                 LexNameToken rv = new LexNameToken(name.getModule(), name.getName(), name.getLocation(), name.isOld(), name.getExplicit())
175:                 {
176:                         private static final long serialVersionUID = 1L;
177:
178:                         @Override
179:                         public boolean equals(Object other)
180:                         {
181:•                                if (super.equals(other))
182:                                 {
183:                                         LexNameToken lother = (LexNameToken)other;
184:                                         
185:•                                        if (typeQualifier != null && lother.typeQualifier != null)
186:                                         {
187:                                                 TypeComparator comp = new TypeComparator(assistantFactory);
188:                                                 return comp.compatible(typeQualifier, lother.typeQualifier);
189:                                         }
190:                                         else
191:                                         {
192:                                                 return true;
193:                                         }
194:                                 }
195:                                 else
196:                                 {
197:                                         return false;
198:                                 }
199:                         }
200:                         
201:                         @Override
202:                         public int hashCode()
203:                         {
204:                                 return name.hashCode() + module.hashCode();
205:                         }
206:                 };
207:                 
208:                 rv.setTypeQualifier(name.getTypeQualifier());
209:                 return rv;
210:         }
211:
212:         /**
213:          * Return true if the name sought is reachable via the next set of names passed using
214:          * the dependency map. The stack passed records the path taken to find a cycle.
215:          */
216:         private boolean reachable(ILexNameToken sought, LexNameSet nextset,
217:                 Map<ILexNameToken, LexNameSet> dependencies, Stack<ILexNameToken> stack)
218:         {
219:                 if (nextset == null)
220:                 {
221:                         return false;
222:                 }
223:                 
224:                 if (nextset.contains(sought))
225:                 {
226:                         stack.push(sought);
227:                         return true;
228:                 }
229:                 
230:                 for (ILexNameToken nextname: nextset)
231:                 {
232:                         if (stack.contains(nextname))        // Been here before!
233:                         {
234:                                 return false;
235:                         }
236:                         
237:                         stack.push(nextname);
238:                         
239:                         if (reachable(sought, dependencies.get(nextname), dependencies, stack))
240:                         {
241:                                 return true;
242:                         }
243:                         
244:                         stack.pop();
245:                 }
246:                 
247:                 return false;
248: }
249:
250:         public static void suppressErrors(boolean sup)
251:         {
252:                 suppress =sup;
253:         }
254:
255:         public static void report(int number, String problem, ILexLocation location)
256:         {
257:                 if (suppress) return;
258:                 VDMError error = new VDMError(number, problem, location);
259:                 // System.out.println(error.toString());
260:                 errors.add(error);
261:                 lastMessage = error;
262:
263:                 for (IStatusListener listner : listners)
264:                 {
265:                         listner.report(error);
266:                 }
267:
268:                 if (errors.size() >= MAX - 1)
269:                 {
270:                         errors.add(new VDMError(10, "Too many type checking errors", location));
271:                         throw new InternalException(10, "Too many type checking errors");
272:                 }
273:         }
274:
275:         public static void warning(int number, String problem, ILexLocation location)
276:         {
277:                 if (suppress) return;
278:                 VDMWarning warning = new VDMWarning(number, problem, location);
279:                 warnings.add(warning);
280:                 lastMessage = warning;
281:
282:                 for (IStatusListener listner : listners)
283:                 {
284:                         listner.warning(warning);
285:                 }
286:         }
287:
288:         public static void detail(String tag, Object obj)
289:         {
290:                 if (suppress) return;
291:                 if (lastMessage != null)
292:                 {
293:                         lastMessage.add(tag + ": " + obj);
294:                 }
295:         }
296:
297:         public static void detail2(String tag1, Object obj1, String tag2,
298:                         Object obj2)
299:         {
300:                 detail(tag1, obj1);
301:                 detail(tag2, obj2);
302:         }
303:
304:         public static void clearErrors()
305:         {
306:                 errors.clear();
307:                 warnings.clear();
308:         }
309:
310:         public static int getErrorCount()
311:         {
312:                 return errors.size();
313:         }
314:
315:         public static int getWarningCount()
316:         {
317:                 return warnings.size();
318:         }
319:
320:         public static List<VDMError> getErrors()
321:         {
322:                 return errors;
323:         }
324:
325:         public static List<VDMWarning> getWarnings()
326:         {
327:                 return warnings;
328:         }
329:
330:         public static void printErrors(PrintWriter out)
331:         {
332:                 for (VDMError e : errors)
333:                 {
334:                         out.println(e.toString());
335:                 }
336:         }
337:
338:         public static void printWarnings(PrintWriter out)
339:         {
340:                 for (VDMWarning w : warnings)
341:                 {
342:                         out.println(w.toString());
343:                 }
344:         }
345:
346:         public static void addStatusListner(IStatusListener listner)
347:         {
348:                 listners.add(listner);
349:         }
350:
351:         public static void removeStatusListner(IStatusListener listner)
352:         {
353:                 listners.remove(listner);
354:         }
355:         
356:         /**
357:          * An invariant type is opaque to the caller if it is opaque (not struct exported) and
358:          * the module being used from is not the type's defining module.
359:          */
360:         public static boolean isOpaque(SInvariantType type, String fromModule)
361:         {
362:                 return type.getOpaque() && fromModule != null && !type.getLocation().getModule().equals(fromModule);
363:         }
364: }