Package: VDMJ

VDMJ

nameinstructionbranchcomplexitylinemethod
VDMJ()
M: 0 C: 8
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
dumpLogs()
M: 14 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 4 C: 0
0%
M: 1 C: 0
0%
getOvertureVersion()
M: 27 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 9 C: 0
0%
M: 1 C: 0
0%
info(String)
M: 0 C: 5
100%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 3
100%
M: 0 C: 1
100%
infoln(String)
M: 0 C: 5
100%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 3
100%
M: 0 C: 1
100%
main(String[])
M: 609 C: 0
0%
M: 122 C: 0
0%
M: 62 C: 0
0%
M: 166 C: 0
0%
M: 1 C: 0
0%
plural(int, String, String)
M: 0 C: 23
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
print(String)
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
println(String)
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
setCharset(String)
M: 5 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 3 C: 0
0%
M: 1 C: 0
0%
setQuiet(boolean)
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
setWarnings(boolean)
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
static {...}
M: 0 C: 18
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
usage(String)
M: 84 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 26 C: 0
0%
M: 1 C: 0
0%
validateCharset(String)
M: 72 C: 0
0%
M: 4 C: 0
0%
M: 3 C: 0
0%
M: 12 C: 0
0%
M: 1 C: 0
0%

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.IOException;
28: import java.io.InputStream;
29: import java.nio.charset.Charset;
30: import java.util.Arrays;
31: import java.util.Iterator;
32: import java.util.List;
33: import java.util.Map;
34: import java.util.Map.Entry;
35: import java.util.Vector;
36:
37: import org.overture.ast.lex.Dialect;
38: import org.overture.config.Release;
39: import org.overture.config.Settings;
40: import org.overture.interpreter.assistant.IInterpreterAssistantFactory;
41: import org.overture.interpreter.assistant.InterpreterAssistantFactory;
42: import org.overture.interpreter.debug.RemoteControl;
43: import org.overture.interpreter.debug.RemoteInterpreter;
44: import org.overture.interpreter.messages.Console;
45: import org.overture.interpreter.messages.rtlog.RTLogger;
46: import org.overture.interpreter.runtime.Interpreter;
47: import org.overture.interpreter.util.ExitStatus;
48: import org.overture.parser.config.Properties;
49:
50: /**
51: * The main class of the VDMJ parser/checker/interpreter.
52: */
53:
54: abstract public class VDMJ
55: {
56:         protected static boolean warnings = true;
57:         protected static boolean interpret = false;
58:         protected static boolean pog = false;
59:         protected static boolean quiet = false;
60:         protected static String script = null;
61:         protected static String outfile = null;
62:         protected static String logfile = null;
63:
64:         public static String filecharset = Charset.defaultCharset().name();
65:
66:         final protected IInterpreterAssistantFactory assistantFactory;// = new TypeCheckerAssistantFactory();
67:
68:         /**
69:          * VDM-only constructor. <b>NOT</b> for use by extensions.
70:          */
71:         public VDMJ()
72:         {
73:                 this.assistantFactory = new InterpreterAssistantFactory();
74:         }
75:
76:         /**
77:          * The main method. This validates the arguments, then parses and type checks the files provided (if any), and
78:          * finally enters the interpreter if required.
79:          *
80:          * @param args
81:          * Arguments passed to the program.
82:          */
83:
84:         @SuppressWarnings("unchecked")
85:         public static void main(String[] args)
86:         {
87:                 List<File> filenames = new Vector<File>();
88:                 List<File> pathnames = new Vector<File>();
89:                 List<String> largs = Arrays.asList(args);
90:                 VDMJ controller = null;
91:                 Dialect dialect = Dialect.VDM_SL;
92:                 String remoteName = null;
93:                 Class<RemoteControl> remoteClass = null;
94:                 String defaultName = null;
95:
96:                 Properties.init(); // Read properties file, if any
97:                 Settings.usingCmdLine = true;
98:                 
99:•                if(largs.contains("-version"))
100:                 {
101:                         println(getOvertureVersion());
102:                         System.exit(0);
103:                 }
104:                 
105:•                for (Iterator<String> i = largs.iterator(); i.hasNext();)
106:                 {
107:                         String arg = i.next();
108:
109:•                        if (arg.equals("-vdmsl"))
110:                         {
111:                                 controller = new VDMSL();
112:                                 dialect = Dialect.VDM_SL;
113:•                        } else if (arg.equals("-vdmpp"))
114:                         {
115:                                 controller = new VDMPP();
116:                                 dialect = Dialect.VDM_PP;
117:•                        } else if (arg.equals("-vdmrt"))
118:                         {
119:                                 controller = new VDMRT();
120:                                 dialect = Dialect.VDM_RT;
121:•                        } else if (arg.equals("-w"))
122:                         {
123:                                 warnings = false;
124:•                        } else if (arg.equals("-i"))
125:                         {
126:                                 interpret = true;
127:•                        } else if (arg.equals("-p"))
128:                         {
129:                                 pog = true;
130:•                        } else if (arg.equals("-q"))
131:                         {
132:                                 quiet = true;
133:•                        } else if (arg.equals("-e"))
134:                         {
135:                                 Settings.usingCmdLine = false;
136:                                 interpret = true;
137:                                 pog = false;
138:
139:•                                if (i.hasNext())
140:                                 {
141:                                         script = i.next();
142:                                 } else
143:                                 {
144:                                         usage("-e option requires an expression");
145:                                 }
146:•                        } else if (arg.equals("-o"))
147:                         {
148:•                                if (i.hasNext())
149:                                 {
150:•                                        if (outfile != null)
151:                                         {
152:                                                 usage("Only one -o option allowed");
153:                                         }
154:
155:                                         outfile = i.next();
156:                                 } else
157:                                 {
158:                                         usage("-o option requires a filename");
159:                                 }
160:•                        } else if (arg.equals("-c"))
161:                         {
162:•                                if (i.hasNext())
163:                                 {
164:                                         filecharset = validateCharset(i.next());
165:                                 } else
166:                                 {
167:                                         usage("-c option requires a charset name");
168:                                 }
169:•                        } else if (arg.equals("-t"))
170:                         {
171:•                                if (i.hasNext())
172:                                 {
173:                                         Console.setCharset(validateCharset(i.next()));
174:                                 } else
175:                                 {
176:                                         usage("-t option requires a charset name");
177:                                 }
178:•                        } else if (arg.equals("-r"))
179:                         {
180:•                                if (i.hasNext())
181:                                 {
182:                                         Settings.release = Release.lookup(i.next());
183:
184:•                                        if (Settings.release == null)
185:                                         {
186:                                                 usage("-r option must be " + Release.list());
187:                                         }
188:                                 } else
189:                                 {
190:                                         usage("-r option requires a VDM release");
191:                                 }
192:•                        } else if (arg.equals("-pre"))
193:                         {
194:                                 Settings.prechecks = false;
195:•                        } else if (arg.equals("-post"))
196:                         {
197:                                 Settings.postchecks = false;
198:•                        } else if (arg.equals("-inv"))
199:                         {
200:                                 Settings.invchecks = false;
201:•                        } else if (arg.equals("-dtc"))
202:                         {
203:                                 // NB. Turn off both when no DTC
204:                                 Settings.invchecks = false;
205:                                 Settings.dynamictypechecks = false;
206:•                        } else if (arg.equals("-measures"))
207:                         {
208:                                 Settings.measureChecks = false;
209:•                        } else if (arg.equals("-log"))
210:                         {
211:•                                if (i.hasNext())
212:                                 {
213:                                         logfile = i.next();
214:                                 } else
215:                                 {
216:                                         usage("-log option requires a filename");
217:                                 }
218:•                        } else if (arg.equals("-remote"))
219:                         {
220:•                                if (i.hasNext())
221:                                 {
222:                                         interpret = true;
223:                                         remoteName = i.next();
224:                                 } else
225:                                 {
226:                                         usage("-remote option requires a Java classname");
227:                                 }
228:•                        } else if (arg.equals("-default"))
229:                         {
230:•                                if (i.hasNext())
231:                                 {
232:                                         defaultName = i.next();
233:                                 } else
234:                                 {
235:                                         usage("-default option requires a name");
236:                                 }
237:•                        } else if (arg.equals("-path"))
238:                         {
239:•                                if (i.hasNext())
240:                                 {
241:                                         File path = new File(i.next());
242:
243:•                                        if (path.isDirectory())
244:                                         {
245:                                                 pathnames.add(path);
246:                                         } else
247:                                         {
248:                                                 usage(path + " is not a directory");
249:                                         }
250:                                 } else
251:                                 {
252:                                         usage("-path option requires a directory");
253:                                 }
254:•                        }else if (arg.equals("-baseDir"))
255:                         {
256:•                                if (i.hasNext())
257:                                 {
258:                                         try
259:                                         {
260:                                                 Settings.baseDir = new File(i.next());
261:                                         } catch (IllegalArgumentException e)
262:                                         {
263:                                                 usage(e.getMessage() + ": " + arg);
264:                                         }
265:                                 } else
266:                                 {
267:                                         usage("-baseDir option requires a folder name");
268:                                 }
269:•                        } else if (arg.startsWith("-"))
270:                         {
271:                                 usage("Unknown option " + arg);
272:                         } else
273:                         {
274:                                 // It's a file or a directory
275:                                 File file = new File(arg);
276:
277:•                                if (file.isDirectory())
278:                                 {
279:•                                        for (File subFile : file.listFiles(dialect.getFilter()))
280:                                         {
281:•                                                if (subFile.isFile())
282:                                                 {
283:                                                         filenames.add(subFile);
284:                                                 }
285:                                         }
286:                                 } else
287:                                 {
288:•                                        if (file.exists())
289:                                         {
290:                                                 filenames.add(file);
291:                                         } else
292:                                         {
293:                                                 boolean OK = false;
294:
295:•                                                for (File path : pathnames)
296:                                                 {
297:                                                         File pfile = new File(path, arg);
298:
299:•                                                        if (pfile.exists())
300:                                                         {
301:                                                                 filenames.add(pfile);
302:                                                                 OK = true;
303:                                                                 break;
304:                                                         }
305:                                                 }
306:
307:•                                                if (!OK)
308:                                                 {
309:                                                         usage("Cannot find file " + file);
310:                                                 }
311:
312:                                         }
313:                                 }
314:                         }
315:                 }
316:
317:•                if (controller == null)
318:                 {
319:                         usage("You must specify either -vdmsl, -vdmpp or -vdmrt");
320:                 }
321:
322:•                if (logfile != null && !(controller instanceof VDMRT))
323:                 {
324:                         usage("The -log option can only be used with -vdmrt");
325:                 }
326:
327:•                if (remoteName != null)
328:                 {
329:                         try
330:                         {
331:                                 Class<?> cls = ClassLoader.getSystemClassLoader().loadClass(remoteName);
332:                                 remoteClass = (Class<RemoteControl>) cls;
333:                         } catch (ClassNotFoundException e)
334:                         {
335:                                 usage("Cannot locate " + remoteName + " on the CLASSPATH");
336:                         }
337:                 }
338:
339:                 ExitStatus status = null;
340:
341:•                if (filenames.isEmpty() && (!interpret || remoteClass != null))
342:                 {
343:                         usage("You didn't specify any files");
344:                         status = ExitStatus.EXIT_ERRORS;
345:                 } else
346:                 {
347:                         do
348:                         {
349:•                                if (filenames.isEmpty())
350:                                 {
351:                                         status = controller.interpret(filenames, null);
352:                                 } else
353:                                 {
354:                                         status = controller.parse(filenames);
355:
356:•                                        if (status == ExitStatus.EXIT_OK)
357:                                         {
358:                                                 status = controller.typeCheck();
359:
360:•                                                if (status == ExitStatus.EXIT_OK && interpret)
361:                                                 {
362:•                                                        if (remoteClass == null)
363:                                                         {
364:                                                                 status = controller.interpret(filenames, defaultName);
365:                                                         } else
366:                                                         {
367:                                                                 try
368:                                                                 {
369:                                                                         final RemoteControl remote = remoteClass.newInstance();
370:                                                                         Interpreter i = controller.getInterpreter();
371:
372:•                                                                        if (defaultName != null)
373:                                                                         {
374:                                                                                 i.setDefaultName(defaultName);
375:                                                                         }
376:
377:                                                                         i.init(null);
378:
379:                                                                         try
380:                                                                         {
381:                                                                                 // remote.run(new RemoteInterpreter(i, null));
382:                                                                                 final RemoteInterpreter remoteInterpreter = new RemoteInterpreter(i, null);
383:                                                                                 Thread remoteThread = new Thread(new Runnable()
384:                                                                                 {
385:
386:                                                                                         public void run()
387:                                                                                         {
388:                                                                                                 try
389:                                                                                                 {
390:                                                                                                         remote.run(remoteInterpreter);
391:                                                                                                 } catch (Exception e)
392:                                                                                                 {
393:                                                                                                         println(e.getMessage());
394:                                                                                                         // status = ExitStatus.EXIT_ERRORS;
395:                                                                                                 }
396:                                                                                         }
397:                                                                                 });
398:                                                                                 remoteThread.setName("RemoteControl runner");
399:                                                                                 remoteThread.setDaemon(true);
400:                                                                                 remoteThread.start();
401:                                                                                 remoteInterpreter.processRemoteCalls();
402:                                                                                 status = ExitStatus.EXIT_OK;
403:                                                                         } catch (Exception e)
404:                                                                         {
405:                                                                                 println(e.getMessage());
406:                                                                                 status = ExitStatus.EXIT_ERRORS;
407:                                                                         }
408:                                                                 } catch (InstantiationException e)
409:                                                                 {
410:                                                                         usage("Cannot instantiate " + remoteName);
411:                                                                 } catch (Exception e)
412:                                                                 {
413:                                                                         usage(e.getMessage());
414:                                                                 }
415:                                                         }
416:                                                 }
417:                                         }
418:                                 }
419:•                        } while (status == ExitStatus.RELOAD);
420:                 }
421:
422:•                if (interpret)
423:                 {
424:                         infoln("Bye");
425:                 }
426:
427:•                System.exit(status == ExitStatus.EXIT_OK ? 0 : 1);
428:         }
429:         
430:         public static String getOvertureVersion() {
431:                 String path = "/version.prop";
432:                 InputStream stream = VDMJ.class.getResourceAsStream(path);
433:•                if (stream == null) return "UNKNOWN";
434:                 java.util.Properties props = new java.util.Properties();
435:                 try {
436:                         props.load(stream);
437:                         stream.close();
438:                         return (String)props.get("version");
439:                 } catch (IOException e) {
440:                         return "UNKNOWN";
441:                 }
442:         }
443:
444:         private static void usage(String msg)
445:         {
446:                 System.err.println("Overture: " + msg + "\n");
447:                 System.err.println("Usage: Overture <-vdmsl | -vdmpp | -vdmrt> [<options>] [<files or dirs>]");
448:                 System.err.println("-vdmsl: parse files as VDM-SL");
449:                 System.err.println("-vdmpp: parse files as VDM++");
450:                 System.err.println("-vdmrt: parse files as VDM-RT");
451:                 System.err.println("-path: search path for files");
452:                 System.err.println("-r <release>: VDM language release");
453:                 System.err.println("-w: suppress warning messages");
454:                 System.err.println("-q: suppress information messages");
455:                 System.err.println("-i: run the interpreter if successfully type checked");
456:                 System.err.println("-p: generate proof obligations and stop");
457:                 System.err.println("-e <exp>: evaluate <exp> and stop");
458:                 System.err.println("-c <charset>: select a file charset");
459:                 System.err.println("-t <charset>: select a console charset");
460:                 System.err.println("-o <filename>: saved type checked specification");
461:                 System.err.println("-default <name>: set the default module/class");
462:                 System.err.println("-pre: disable precondition checks");
463:                 System.err.println("-post: disable postcondition checks");
464:                 System.err.println("-inv: disable type/state invariant checks");
465:                 System.err.println("-dtc: disable all dynamic type checking");
466:                 System.err.println("-measures: disable recursive measure checking");
467:                 System.err.println("-log: enable real-time event logging");
468:                 System.err.println("-remote <class>: enable remote control");
469:                 System.err.println("-version: print Overture version number");
470:
471:                 System.exit(1);
472:         }
473:
474:         /**
475:          * Parse the list of files passed. The value returned is the number of syntax errors encountered.
476:          *
477:          * @param files
478:          * The files to parse.
479:          * @return The number of syntax errors.
480:          */
481:
482:         public abstract ExitStatus parse(List<File> files);
483:
484:         /**
485:          * Type check the files previously parsed by {@link #parse(List)}. The value returned is the number of type checking
486:          * errors.
487:          *
488:          * @return The number of type check errors.
489:          */
490:
491:         public abstract ExitStatus typeCheck();
492:
493:         /**
494:          * Generate an interpreter from the classes parsed.
495:          *
496:          * @return An initialized interpreter.
497:          * @throws Exception
498:          */
499:
500:         public abstract Interpreter getInterpreter() throws Exception;
501:
502:         /**
503:          * Interpret the type checked specification. The number returned is the number of runtime errors not caught by the
504:          * interpreter (usually zero or one).
505:          *
506:          * @param filenames
507:          * The filenames currently loaded.
508:          * @param defaultName
509:          * The default module or class (or null).
510:          * @return The exit status of the interpreter.
511:          */
512:
513:         abstract protected ExitStatus interpret(List<File> filenames,
514:                         String defaultName);
515:
516:         /**
517:          * Dump log files
518:          */
519:         protected void dumpLogs()
520:         {
521:•                if (logfile != null)
522:                 {
523:                         RTLogger.dump(true);
524:                         infoln("RT events dumped to " + logfile);
525:                 }
526:         }
527:
528:         public void setWarnings(boolean w)
529:         {
530:                 warnings = w;
531:         }
532:
533:         public void setQuiet(boolean q)
534:         {
535:                 quiet = q;
536:         }
537:
538:         public void setCharset(String charset)
539:         {
540:                 filecharset = charset;
541:                 Console.setCharset(charset);
542:         }
543:
544:         protected static void info(String m)
545:         {
546:•                if (!quiet)
547:                 {
548:                         print(m);
549:                 }
550:         }
551:
552:         protected static void infoln(String m)
553:         {
554:•                if (!quiet)
555:                 {
556:                         println(m);
557:                 }
558:         }
559:
560:         protected static void print(String m)
561:         {
562:                 Console.out.print(m);
563:                 Console.out.flush();
564:         }
565:
566:         protected static void println(String m)
567:         {
568:                 Console.out.println(m);
569:         }
570:
571:         protected String plural(int n, String s, String pl)
572:         {
573:•                return n + " " + (n != 1 ? s + pl : s);
574:         }
575:
576:         private static String validateCharset(String cs)
577:         {
578:•                if (!Charset.isSupported(cs))
579:                 {
580:                         println("Charset " + cs + " is not supported\n");
581:                         println("Available charsets:");
582:                         println("Default = " + Charset.defaultCharset());
583:                         Map<String, Charset> available = Charset.availableCharsets();
584:
585:•                        for (Entry<String, Charset> entry : available.entrySet())
586:                         {
587:                                 println(entry.getKey() + " "
588:                                                 + available.get(entry.getValue()).aliases());
589:                         }
590:
591:                         println("");
592:                         usage("Charset " + cs + " is not supported");
593:                 }
594:
595:                 return cs;
596:         }
597: }