Method: setWarnings(boolean)

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.equals("-strict"))
270:                         {
271:                                 Settings.strict = true;
272:                         } else if (arg.startsWith("-"))
273:                         {
274:                                 usage("Unknown option " + arg);
275:                         } else
276:                         {
277:                                 // It's a file or a directory
278:                                 File file = new File(arg);
279:
280:                                 if (file.isDirectory())
281:                                 {
282:                                         for (File subFile : file.listFiles(dialect.getFilter()))
283:                                         {
284:                                                 if (subFile.isFile())
285:                                                 {
286:                                                         filenames.add(subFile);
287:                                                 }
288:                                         }
289:                                 } else
290:                                 {
291:                                         if (file.exists())
292:                                         {
293:                                                 filenames.add(file);
294:                                         } else
295:                                         {
296:                                                 boolean OK = false;
297:
298:                                                 for (File path : pathnames)
299:                                                 {
300:                                                         File pfile = new File(path, arg);
301:
302:                                                         if (pfile.exists())
303:                                                         {
304:                                                                 filenames.add(pfile);
305:                                                                 OK = true;
306:                                                                 break;
307:                                                         }
308:                                                 }
309:
310:                                                 if (!OK)
311:                                                 {
312:                                                         usage("Cannot find file " + file);
313:                                                 }
314:
315:                                         }
316:                                 }
317:                         }
318:                 }
319:
320:                 if (controller == null)
321:                 {
322:                         usage("You must specify either -vdmsl, -vdmpp or -vdmrt");
323:                 }
324:
325:                 if (logfile != null && !(controller instanceof VDMRT))
326:                 {
327:                         usage("The -log option can only be used with -vdmrt");
328:                 }
329:
330:                 if (remoteName != null)
331:                 {
332:                         try
333:                         {
334:                                 Class<?> cls = ClassLoader.getSystemClassLoader().loadClass(remoteName);
335:                                 remoteClass = (Class<RemoteControl>) cls;
336:                         } catch (ClassNotFoundException e)
337:                         {
338:                                 usage("Cannot locate " + remoteName + " on the CLASSPATH");
339:                         }
340:                 }
341:
342:                 ExitStatus status = null;
343:
344:                 if (filenames.isEmpty() && (!interpret || remoteClass != null))
345:                 {
346:                         usage("You didn't specify any files");
347:                         status = ExitStatus.EXIT_ERRORS;
348:                 } else
349:                 {
350:                         do
351:                         {
352:                                 if (filenames.isEmpty())
353:                                 {
354:                                         status = controller.interpret(filenames, null);
355:                                 } else
356:                                 {
357:                                         status = controller.parse(filenames);
358:
359:                                         if (status == ExitStatus.EXIT_OK)
360:                                         {
361:                                                 status = controller.typeCheck();
362:
363:                                                 if (status == ExitStatus.EXIT_OK && interpret)
364:                                                 {
365:                                                         if (remoteClass == null)
366:                                                         {
367:                                                                 status = controller.interpret(filenames, defaultName);
368:                                                         } else
369:                                                         {
370:                                                                 try
371:                                                                 {
372:                                                                         final RemoteControl remote = remoteClass.newInstance();
373:                                                                         Interpreter i = controller.getInterpreter();
374:
375:                                                                         if (defaultName != null)
376:                                                                         {
377:                                                                                 i.setDefaultName(defaultName);
378:                                                                         }
379:
380:                                                                         i.init(null);
381:
382:                                                                         try
383:                                                                         {
384:                                                                                 // remote.run(new RemoteInterpreter(i, null));
385:                                                                                 final RemoteInterpreter remoteInterpreter = new RemoteInterpreter(i, null);
386:                                                                                 Thread remoteThread = new Thread(new Runnable()
387:                                                                                 {
388:
389:                                                                                         public void run()
390:                                                                                         {
391:                                                                                                 try
392:                                                                                                 {
393:                                                                                                         remote.run(remoteInterpreter);
394:                                                                                                 } catch (Exception e)
395:                                                                                                 {
396:                                                                                                         println(e.getMessage());
397:                                                                                                         // status = ExitStatus.EXIT_ERRORS;
398:                                                                                                 }
399:                                                                                         }
400:                                                                                 });
401:                                                                                 remoteThread.setName("RemoteControl runner");
402:                                                                                 remoteThread.setDaemon(true);
403:                                                                                 remoteThread.start();
404:                                                                                 remoteInterpreter.processRemoteCalls();
405:                                                                                 status = ExitStatus.EXIT_OK;
406:                                                                         } catch (Exception e)
407:                                                                         {
408:                                                                                 println(e.getMessage());
409:                                                                                 status = ExitStatus.EXIT_ERRORS;
410:                                                                         }
411:                                                                 } catch (InstantiationException e)
412:                                                                 {
413:                                                                         usage("Cannot instantiate " + remoteName);
414:                                                                 } catch (Exception e)
415:                                                                 {
416:                                                                         usage(e.getMessage());
417:                                                                 }
418:                                                         }
419:                                                 }
420:                                         }
421:                                 }
422:                         } while (status == ExitStatus.RELOAD);
423:                 }
424:
425:                 if (interpret)
426:                 {
427:                         infoln("Bye");
428:                 }
429:
430:                 System.exit(status == ExitStatus.EXIT_OK ? 0 : 1);
431:         }
432:         
433:         public static String getOvertureVersion() {
434:                 String path = "/version.prop";
435:                 InputStream stream = VDMJ.class.getResourceAsStream(path);
436:                 if (stream == null) return "UNKNOWN";
437:                 java.util.Properties props = new java.util.Properties();
438:                 try {
439:                         props.load(stream);
440:                         stream.close();
441:                         return (String)props.get("version");
442:                 } catch (IOException e) {
443:                         return "UNKNOWN";
444:                 }
445:         }
446:
447:         private static void usage(String msg)
448:         {
449:                 System.err.println("Overture: " + msg + "\n");
450:                 System.err.println("Usage: Overture <-vdmsl | -vdmpp | -vdmrt> [<options>] [<files or dirs>]");
451:                 System.err.println("-vdmsl: parse files as VDM-SL");
452:                 System.err.println("-vdmpp: parse files as VDM++");
453:                 System.err.println("-vdmrt: parse files as VDM-RT");
454:                 System.err.println("-path: search path for files");
455:                 System.err.println("-r <release>: VDM language release");
456:                 System.err.println("-w: suppress warning messages");
457:                 System.err.println("-q: suppress information messages");
458:                 System.err.println("-i: run the interpreter if successfully type checked");
459:                 System.err.println("-p: generate proof obligations and stop");
460:                 System.err.println("-e <exp>: evaluate <exp> and stop");
461:                 System.err.println("-c <charset>: select a file charset");
462:                 System.err.println("-t <charset>: select a console charset");
463:                 System.err.println("-o <filename>: saved type checked specification");
464:                 System.err.println("-default <name>: set the default module/class");
465:                 System.err.println("-pre: disable precondition checks");
466:                 System.err.println("-post: disable postcondition checks");
467:                 System.err.println("-inv: disable type/state invariant checks");
468:                 System.err.println("-dtc: disable all dynamic type checking");
469:                 System.err.println("-measures: disable recursive measure checking");
470:                 System.err.println("-log: enable real-time event logging");
471:                 System.err.println("-remote <class>: enable remote control");
472:                 System.err.println("-version: print Overture version number");
473:
474:                 System.exit(1);
475:         }
476:
477:         /**
478:          * Parse the list of files passed. The value returned is the number of syntax errors encountered.
479:          *
480:          * @param files
481:          * The files to parse.
482:          * @return The number of syntax errors.
483:          */
484:
485:         public abstract ExitStatus parse(List<File> files);
486:
487:         /**
488:          * Type check the files previously parsed by {@link #parse(List)}. The value returned is the number of type checking
489:          * errors.
490:          *
491:          * @return The number of type check errors.
492:          */
493:
494:         public abstract ExitStatus typeCheck();
495:
496:         /**
497:          * Generate an interpreter from the classes parsed.
498:          *
499:          * @return An initialized interpreter.
500:          * @throws Exception
501:          */
502:
503:         public abstract Interpreter getInterpreter() throws Exception;
504:
505:         /**
506:          * Interpret the type checked specification. The number returned is the number of runtime errors not caught by the
507:          * interpreter (usually zero or one).
508:          *
509:          * @param filenames
510:          * The filenames currently loaded.
511:          * @param defaultName
512:          * The default module or class (or null).
513:          * @return The exit status of the interpreter.
514:          */
515:
516:         abstract protected ExitStatus interpret(List<File> filenames,
517:                         String defaultName);
518:
519:         /**
520:          * Dump log files
521:          */
522:         protected void dumpLogs()
523:         {
524:                 if (logfile != null)
525:                 {
526:                         RTLogger.dump(true);
527:                         infoln("RT events dumped to " + logfile);
528:                 }
529:         }
530:
531:         public void setWarnings(boolean w)
532:         {
533:                 warnings = w;
534:         }
535:
536:         public void setQuiet(boolean q)
537:         {
538:                 quiet = q;
539:         }
540:
541:         public void setCharset(String charset)
542:         {
543:                 filecharset = charset;
544:                 Console.setCharset(charset);
545:         }
546:
547:         protected static void info(String m)
548:         {
549:                 if (!quiet)
550:                 {
551:                         print(m);
552:                 }
553:         }
554:
555:         protected static void infoln(String m)
556:         {
557:                 if (!quiet)
558:                 {
559:                         println(m);
560:                 }
561:         }
562:
563:         protected static void print(String m)
564:         {
565:                 Console.out.print(m);
566:                 Console.out.flush();
567:         }
568:
569:         protected static void println(String m)
570:         {
571:                 Console.out.println(m);
572:         }
573:
574:         protected String plural(int n, String s, String pl)
575:         {
576:                 return n + " " + (n != 1 ? s + pl : s);
577:         }
578:
579:         private static String validateCharset(String cs)
580:         {
581:                 if (!Charset.isSupported(cs))
582:                 {
583:                         println("Charset " + cs + " is not supported\n");
584:                         println("Available charsets:");
585:                         println("Default = " + Charset.defaultCharset());
586:                         Map<String, Charset> available = Charset.availableCharsets();
587:
588:                         for (Entry<String, Charset> entry : available.entrySet())
589:                         {
590:                                 println(entry.getKey() + " "
591:                                                 + available.get(entry.getValue()).aliases());
592:                         }
593:
594:                         println("");
595:                         usage("Charset " + cs + " is not supported");
596:                 }
597:
598:                 return cs;
599:         }
600: }