Package: VDMPP

VDMPP

nameinstructionbranchcomplexitylinemethod
VDMPP()
M: 0 C: 10
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
getInterpreter()
M: 0 C: 8
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
interpret(List, String)
M: 183 C: 0
0%
M: 8 C: 0
0%
M: 5 C: 0
0%
M: 44 C: 0
0%
M: 1 C: 0
0%
parse(List)
M: 139 C: 110
44%
M: 11 C: 11
50%
M: 10 C: 2
17%
M: 28 C: 24
46%
M: 0 C: 1
100%
typeCheck()
M: 143 C: 97
40%
M: 16 C: 12
43%
M: 12 C: 3
20%
M: 30 C: 20
40%
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.interpreter;
25:
26: import java.io.File;
27: import java.io.FileInputStream;
28: import java.io.FileNotFoundException;
29: import java.io.FileOutputStream;
30: import java.io.IOException;
31: import java.io.ObjectInputStream;
32: import java.io.ObjectOutputStream;
33: import java.util.List;
34: import java.util.zip.GZIPInputStream;
35: import java.util.zip.GZIPOutputStream;
36:
37: import org.overture.ast.analysis.AnalysisException;
38: import org.overture.ast.lex.Dialect;
39: import org.overture.ast.lex.LexLocation;
40: import org.overture.ast.messages.InternalException;
41: import org.overture.ast.util.definitions.ClassList;
42: import org.overture.config.Settings;
43: import org.overture.interpreter.commands.ClassCommandReader;
44: import org.overture.interpreter.commands.CommandReader;
45: import org.overture.interpreter.messages.Console;
46: import org.overture.interpreter.messages.rtlog.RTLogger;
47: import org.overture.interpreter.messages.rtlog.RTTextLogger;
48: import org.overture.interpreter.messages.rtlog.nextgen.NextGenRTLogger;
49: import org.overture.interpreter.runtime.ClassInterpreter;
50: import org.overture.interpreter.runtime.ContextException;
51: import org.overture.interpreter.util.ClassListInterpreter;
52: import org.overture.interpreter.util.ExitStatus;
53: import org.overture.parser.lex.LexTokenReader;
54: import org.overture.parser.syntax.ClassReader;
55: import org.overture.pog.obligation.ProofObligationList;
56: import org.overture.typechecker.ClassTypeChecker;
57: import org.overture.typechecker.TypeChecker;
58:
59: /**
60: * The main class of the VDM++ and VICE parser/checker/interpreter.
61: */
62:
63: public class VDMPP extends VDMJ
64: {
65:         protected ClassListInterpreter classes = new ClassListInterpreter();
66:
67:         public VDMPP()
68:         {
69:                 super();
70:                 Settings.dialect = Dialect.VDM_PP;
71:         }
72:
73:         /**
74:          * @see VDMJ#parse(java.util.List)
75:          */
76:
77:         @Override
78:         public ExitStatus parse(List<File> files)
79:         {
80:                 classes.clear();
81:                 LexLocation.resetLocations();
82:                 int perrs = 0;
83:                 int pwarn = 0;
84:                 long duration = 0;
85:
86:•                for (File file : files)
87:                 {
88:                         ClassReader reader = null;
89:
90:                         try
91:                         {
92:•                                if (file.getName().endsWith(".lib"))
93:                                 {
94:                                         FileInputStream fis = new FileInputStream(file);
95:                                         GZIPInputStream gis = new GZIPInputStream(fis);
96:                                         ObjectInputStream ois = new ObjectInputStream(gis);
97:
98:                                         ClassListInterpreter loaded = null;
99:                                         long begin = System.currentTimeMillis();
100:
101:                                         try
102:                                         {
103:                                                 loaded = new ClassListInterpreter((ClassList) ois.readObject());
104:                                         } catch (Exception e)
105:                                         {
106:                                                 println(file + " is not a valid VDM++ library");
107:                                                 perrs++;
108:                                                 continue;
109:                                         } finally
110:                                         {
111:                                                 ois.close();
112:                                         }
113:
114:                                         long end = System.currentTimeMillis();
115:                                         loaded.setLoaded();
116:                                         classes.addAll(loaded);
117:                                         classes.remap();
118:
119:                                         infoln("Loaded " + plural(loaded.size(), "class", "es")
120:                                                         + " from " + file + " in " + (double) (end - begin)
121:                                                         / 1000 + " secs");
122:                                 } else
123:                                 {
124:                                         long before = System.currentTimeMillis();
125:                                         LexTokenReader ltr = new LexTokenReader(file, Settings.dialect, filecharset);
126:                                         reader = new ClassReader(ltr);
127:                                         classes.addAll(reader.readClasses());
128:                                         long after = System.currentTimeMillis();
129:                                         duration += after - before;
130:                                 }
131:                         } catch (InternalException e)
132:                         {
133:                                 println(e.toString());
134:                                 perrs++;
135:                         } catch (Throwable e)
136:                         {
137:                                 println(e.toString());
138:                                 perrs++;
139:                         }
140:
141:•                        if (reader != null && reader.getErrorCount() > 0)
142:                         {
143:                                 perrs += reader.getErrorCount();
144:                                 reader.printErrors(Console.out);
145:                         }
146:
147:•                        if (reader != null && reader.getWarningCount() > 0)
148:                         {
149:                                 pwarn += reader.getWarningCount();
150:                                 reader.printWarnings(Console.out);
151:                         }
152:                 }
153:
154:                 int n = classes.notLoaded();
155:
156:•                if (n > 0)
157:                 {
158:                         info("Parsed " + plural(n, "class", "es") + " in "
159:                                         + (double) duration / 1000 + " secs. ");
160:•                        info(perrs == 0 ? "No syntax errors" : "Found "
161:                                         + plural(perrs, "syntax error", "s"));
162:•                        infoln(pwarn == 0 ? "" : " and " + (warnings ? "" : "suppressed ")
163:                                         + plural(pwarn, "warning", "s"));
164:                 }
165:
166:•                return perrs == 0 ? ExitStatus.EXIT_OK : ExitStatus.EXIT_ERRORS;
167:         }
168:
169:         /**
170:          * @see VDMJ#typeCheck()
171:          */
172:
173:         @Override
174:         public ExitStatus typeCheck()
175:         {
176:                 int terrs = 0;
177:                 long before = System.currentTimeMillis();
178:
179:                 try
180:                 {
181:                         TypeChecker typeChecker = new ClassTypeChecker(classes, assistantFactory);
182:                         typeChecker.typeCheck();
183:                 } catch (InternalException e)
184:                 {
185:                         println(e.toString());
186:                 } catch (Throwable e)
187:                 {
188:                         println(e.toString());
189:
190:•                        if (e instanceof StackOverflowError)
191:                         {
192:                                 e.printStackTrace();
193:                         }
194:
195:                         terrs++;
196:                 }
197:
198:                 long after = System.currentTimeMillis();
199:                 terrs += TypeChecker.getErrorCount();
200:
201:•                if (terrs > 0)
202:                 {
203:                         TypeChecker.printErrors(Console.out);
204:                 }
205:
206:                 int twarn = TypeChecker.getWarningCount();
207:
208:•                if (twarn > 0 && warnings)
209:                 {
210:                         TypeChecker.printWarnings(Console.out);
211:                 }
212:
213:                 int n = classes.notLoaded();
214:
215:•                if (n > 0)
216:                 {
217:                         info("Type checked " + plural(n, "class", "es") + " in "
218:                                         + (double) (after - before) / 1000 + " secs. ");
219:•                        info(terrs == 0 ? "No type errors" : "Found "
220:                                         + plural(terrs, "type error", "s"));
221:•                        infoln(twarn == 0 ? "" : " and " + (warnings ? "" : "suppressed ")
222:                                         + plural(twarn, "warning", "s"));
223:                 }
224:
225:•                if (outfile != null && terrs == 0)
226:                 {
227:                         try
228:                         {
229:                                 before = System.currentTimeMillis();
230:                                 FileOutputStream fos = new FileOutputStream(outfile);
231:                                 GZIPOutputStream gos = new GZIPOutputStream(fos);
232:                                 ObjectOutputStream oos = new ObjectOutputStream(gos);
233:
234:                                 oos.writeObject(classes);
235:                                 oos.close();
236:                                 after = System.currentTimeMillis();
237:
238:                                 infoln("Saved " + plural(classes.size(), "class", "es")
239:                                                 + " to " + outfile + " in " + (double) (after - before)
240:                                                 / 1000 + " secs. ");
241:                         } catch (IOException e)
242:                         {
243:                                 infoln("Cannot write " + outfile + ": " + e.getMessage());
244:                                 terrs++;
245:                         }
246:                 }
247:
248:•                if (pog && terrs == 0)
249:                 {
250:                         ProofObligationList list;
251:                         try
252:                         {
253:                                 list = classes.getProofObligations(assistantFactory);
254:
255:•                                if (list.isEmpty())
256:                                 {
257:                                         println("No proof obligations generated");
258:                                 } else
259:                                 {
260:                                         println("Generated "
261:                                                         + plural(list.size(), "proof obligation", "s")
262:                                                         + ":\n");
263:                                         print(list.toString());
264:                                 }
265:                         } catch (AnalysisException e)
266:                         {
267:                                 println(e.toString());
268:                         }
269:
270:                 }
271:
272:•                return terrs == 0 ? ExitStatus.EXIT_OK : ExitStatus.EXIT_ERRORS;
273:         }
274:
275:         /**
276:          * @see org.overture.interpreter.VDMJ#interpret(List, String)
277:          */
278:
279:         @Override
280:         protected ExitStatus interpret(List<File> filenames, String defaultName)
281:         {
282:                 ClassInterpreter interpreter = null;
283:
284:•                if (logfile != null)
285:                 {
286:                         try
287:                         {
288:                                 RTLogger.setLogfile(RTTextLogger.class, new File(logfile));
289:                                 RTLogger.setLogfile(NextGenRTLogger.class, new File(logfile));
290:                                 println("RT events now logged to " + logfile);
291:                         } catch (FileNotFoundException e)
292:                         {
293:                                 println("Cannot create RT event log: " + e.getMessage());
294:                                 return ExitStatus.EXIT_ERRORS;
295:                         }
296:                 }
297:
298:                 try
299:                 {
300:                         long before = System.currentTimeMillis();
301:                         interpreter = getInterpreter();
302:                         interpreter.init(null);
303:
304:•                        if (defaultName != null)
305:                         {
306:                                 interpreter.setDefaultName(defaultName);
307:                         }
308:
309:                         long after = System.currentTimeMillis();
310:
311:                         infoln("Initialized " + plural(classes.size(), "class", "es")
312:                                         + " in " + (double) (after - before) / 1000 + " secs. ");
313:                 } catch (ContextException e)
314:                 {
315:                         println("Initialization: " + e);
316:                         e.ctxt.printStackTrace(Console.out, true);
317:                         dumpLogs();
318:                         return ExitStatus.EXIT_ERRORS;
319:                 } catch (Exception e)
320:                 {
321:                         println("Initialization: " + e.getMessage());
322:                         dumpLogs();
323:                         return ExitStatus.EXIT_ERRORS;
324:                 }
325:
326:                 try
327:                 {
328:                         ExitStatus status;
329:
330:•                        if (script != null)
331:                         {
332:                                 println(interpreter.execute(script, null).toString());
333:                                 status = ExitStatus.EXIT_OK;
334:                         } else
335:                         {
336:                                 infoln("Interpreter started");
337:                                 CommandReader reader = new ClassCommandReader(interpreter, "> ");
338:                                 status = reader.run(filenames);
339:                         }
340:
341:•                        if (logfile != null)
342:                         {
343:                                 RTLogger.dump(true);
344:                                 infoln("RT events dumped to " + logfile);
345:                         }
346:
347:                         return status;
348:                 } catch (ContextException e)
349:                 {
350:                         println("Execution: " + e);
351:                         e.ctxt.printStackTrace(Console.out, true);
352:                 } catch (Exception e)
353:                 {
354:                         println("Execution: " + e);
355:                 }
356:
357:                 dumpLogs();
358:
359:                 return ExitStatus.EXIT_ERRORS;
360:         }
361:
362:         @Override
363:         public ClassInterpreter getInterpreter() throws Exception
364:         {
365:                 ClassInterpreter interpreter = new ClassInterpreter(classes);
366:                 return interpreter;
367:         }
368: }