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.overturetool.vdmj;
25
26 import java.io.File;
27 import java.nio.charset.Charset;
28 import java.util.Arrays;
29 import java.util.Iterator;
30 import java.util.List;
31 import java.util.Map;
32 import java.util.Vector;
33
34 import org.overturetool.vdmj.messages.Console;
35 import org.overturetool.vdmj.runtime.Interpreter;
36
37
38 /***
39 * The main class of the VDMJ parser/checker/interpreter.
40 */
41
42 abstract public class VDMJ
43 {
44 protected static boolean warnings = true;
45 protected static boolean interpret = false;
46 protected static boolean pog = false;
47 protected static boolean quiet = false;
48 protected static String script = null;
49 protected static String outfile = null;
50
51 public static String filecharset = Charset.defaultCharset().name();
52
53 /***
54 * The main method. This validates the arguments, then parses and type
55 * checks the files provided (if any), and finally enters the interpreter
56 * if required.
57 *
58 * @param args Arguments passed to the program.
59 */
60
61 public static void main(String[] args)
62 {
63 List<File> filenames = new Vector<File>();
64 List<String> largs = Arrays.asList(args);
65 VDMJ controller = null;
66
67 for (Iterator<String> i = largs.iterator(); i.hasNext();)
68 {
69 String arg = i.next();
70
71 if (arg.equals("-vdmsl"))
72 {
73 controller = new VDMSL();
74 }
75 else if (arg.equals("-vdmpp"))
76 {
77 controller = new VDMPP();
78 }
79 else if (arg.equals("-vdmrt"))
80 {
81 controller = new VDMRT();
82 }
83 else if (arg.equals("-overture"))
84 {
85 controller = new VDMOV();
86 }
87 else if (arg.equals("-w"))
88 {
89 warnings = false;
90 }
91 else if (arg.equals("-i"))
92 {
93 interpret = true;
94 }
95 else if (arg.equals("-p"))
96 {
97 pog = true;
98 }
99 else if (arg.equals("-q"))
100 {
101 quiet = true;
102 }
103 else if (arg.equals("-e"))
104 {
105 interpret = true;
106 pog = false;
107
108 if (i.hasNext())
109 {
110 script = i.next();
111 }
112 else
113 {
114 usage("-e option requires an expression");
115 }
116 }
117 else if (arg.equals("-o"))
118 {
119 if (i.hasNext())
120 {
121 if (outfile != null)
122 {
123 usage("Only one -o option allowed");
124 }
125
126 outfile = i.next();
127 }
128 else
129 {
130 usage("-o option requires a filename");
131 }
132 }
133 else if (arg.equals("-c"))
134 {
135 if (i.hasNext())
136 {
137 filecharset = validateCharset(i.next());
138 }
139 else
140 {
141 usage("-c option requires a charset name");
142 }
143 }
144 else if (arg.equals("-t"))
145 {
146 if (i.hasNext())
147 {
148 Console.setCharset(validateCharset(i.next()));
149 }
150 else
151 {
152 usage("-t option requires a charset name");
153 }
154 }
155 else if (arg.equals("-pre"))
156 {
157 Settings.prechecks = false;
158 }
159 else if (arg.equals("-post"))
160 {
161 Settings.postchecks = false;
162 }
163 else if (arg.equals("-inv"))
164 {
165 Settings.invchecks = false;
166 }
167 else if (arg.equals("-dtc"))
168 {
169
170 Settings.invchecks = false;
171 Settings.dynamictypechecks = false;
172 }
173 else if (arg.startsWith("-"))
174 {
175 usage("Unknown option " + arg);
176 }
177 else
178 {
179 filenames.add(new File(arg));
180 }
181 }
182
183 if (controller == null)
184 {
185 usage("You must specify either -vdmsl, -vdmpp, -vdmrt or -overture");
186 }
187
188 ExitStatus status = null;
189
190 if (filenames.isEmpty() && !interpret)
191 {
192 usage("You didn't specify any files");
193 status = ExitStatus.EXIT_ERRORS;
194 }
195 else
196 {
197 do
198 {
199 if (filenames.isEmpty())
200 {
201 status = controller.interpret(filenames);
202 }
203 else
204 {
205 status = controller.parse(filenames);
206
207 if (status == ExitStatus.EXIT_OK)
208 {
209 status = controller.typeCheck();
210
211 if (status == ExitStatus.EXIT_OK && interpret)
212 {
213 status = controller.interpret(filenames);
214 }
215 }
216 }
217 }
218 while (status == ExitStatus.RELOAD);
219 }
220
221 if (interpret)
222 {
223 infoln("Bye");
224 }
225
226 System.exit(status == ExitStatus.EXIT_OK ? 0 : 1);
227 }
228
229 private static void usage(String msg)
230 {
231 System.err.println("VDMJ: " + msg + "\n");
232 System.err.println("Usage: VDMJ <-vdmsl | -vdmpp | -vdmrt | -overture> [<options>] [<files>]");
233 System.err.println("-vdmsl: parse files as VDM-SL");
234 System.err.println("-vdmpp: parse files as VDM++");
235 System.err.println("-vdmrt: parse files as VICE");
236 System.err.println("-overture: parse files as VICE with Overture");
237 System.err.println("-w: suppress warning messages");
238 System.err.println("-q: suppress information messages");
239 System.err.println("-i: run the interpreter if successfully type checked");
240 System.err.println("-p: generate proof obligations and stop");
241 System.err.println("-e <exp>: evaluate <exp> and stop");
242 System.err.println("-c <charset>: select a file charset");
243 System.err.println("-t <charset>: select a console charset");
244 System.err.println("-t <charset>: select a console charset");
245 System.err.println("-o <filename>: saved type checked specification");
246 System.err.println("-pre: disable precondition checks");
247 System.err.println("-post: disable postcondition checks");
248 System.err.println("-inv: disable type/state invariant checks");
249 System.err.println("-dtc: disable all dynamic type checking");
250
251 System.exit(1);
252 }
253
254 /***
255 * Parse the list of files passed. The value returned is the number of
256 * syntax errors encountered.
257 *
258 * @param files The files to parse.
259 * @return The number of syntax errors.
260 */
261
262 public abstract ExitStatus parse(List<File> files);
263
264 /***
265 * Type check the files previously parsed by {@link #parse(List)}. The
266 * value returned is the number of type checking errors.
267 *
268 * @return The number of type check errors.
269 */
270
271 public abstract ExitStatus typeCheck();
272
273 /***
274 * Generate an interpreter from the classes parsed.
275 * @return An initialized interpreter.
276 * @throws Exception
277 */
278
279 public abstract Interpreter getInterpreter() throws Exception;
280
281 /***
282 * Interpret the type checked specification. The number returned is the
283 * number of runtime errors not caught by the interpreter (usually zero
284 * or one).
285 *
286 * @param filenames The filenames currently loaded.
287 * @return The exit status of the interpreter.
288 */
289
290 abstract protected ExitStatus interpret(List<File> filenames);
291
292 public void setWarnings(boolean w)
293 {
294 warnings = w;
295 }
296
297 protected static void info(String m)
298 {
299 if (!quiet)
300 {
301 print(m);
302 }
303 }
304
305 protected static void infoln(String m)
306 {
307 if (!quiet)
308 {
309 println(m);
310 }
311 }
312
313 protected static void print(String m)
314 {
315 Console.out.print(m);
316 Console.out.flush();
317 }
318
319 protected static void println(String m)
320 {
321 Console.out.println(m);
322 }
323
324 protected String plural(int n, String s, String pl)
325 {
326 return n + " " + (n != 1 ? s + pl : s);
327 }
328
329 private static String validateCharset(String cs)
330 {
331 if (!Charset.isSupported(cs))
332 {
333 println("Charset " + cs + " is not supported\n");
334 println("Available charsets:");
335 println("Default = " + Charset.defaultCharset());
336 Map<String,Charset> available = Charset.availableCharsets();
337
338 for (String name: available.keySet())
339 {
340 println(name + " " + available.get(name).aliases());
341 }
342
343 println("");
344 usage("Charset " + cs + " is not supported");
345 }
346
347 return cs;
348 }
349 }