Package: VDMPP

VDMPP

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