Package: ModuleInterpreter

ModuleInterpreter

nameinstructionbranchcomplexitylinemethod
ModuleInterpreter(IInterpreterAssistantFactory, ModuleList)
M: 0 C: 25
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
ModuleInterpreter(ModuleList)
M: 0 C: 7
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
evaluate(String, Context)
M: 33 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 9 C: 0
0%
M: 1 C: 0
0%
execute(String, DBGPReader)
M: 0 C: 64
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 13
100%
M: 0 C: 1
100%
findExpression(File, int)
M: 9 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
findModule(String)
M: 0 C: 12
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
findStatement(File, int)
M: 9 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
findTraceDefinition(LexNameToken)
M: 5 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
findType(String)
M: 37 C: 0
0%
M: 8 C: 0
0%
M: 5 C: 0
0%
M: 8 C: 0
0%
M: 1 C: 0
0%
getDefaultFile()
M: 6 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getDefaultName()
M: 0 C: 5
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getGlobalEnvironment()
M: 0 C: 8
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getGlobalEnvironment(String)
M: 9 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getInitialTraceContext(ANamedTraceDefinition, boolean)
M: 0 C: 31
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
getModules()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getProofObligations()
M: 7 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getSourceFiles()
M: 4 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getStateContext()
M: 7 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
init(DBGPReader)
M: 0 C: 43
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
parseExpression(String, String)
M: 17 C: 28
62%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 1 C: 7
88%
M: 0 C: 1
100%
runOneTrace(ANamedTraceDefinition, CallSequence, boolean)
M: 8 C: 30
79%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 3 C: 9
75%
M: 0 C: 1
100%
setDefaultName(String)
M: 15 C: 28
65%
M: 2 C: 4
67%
M: 2 C: 2
50%
M: 2 C: 7
78%
M: 0 C: 1
100%
traceInit(DBGPReader)
M: 21 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 4 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.runtime;
25:
26: import java.io.File;
27: import java.util.List;
28: import java.util.Set;
29: import java.util.Vector;
30:
31: import org.overture.ast.analysis.AnalysisException;
32: import org.overture.ast.annotations.Annotation;
33: import org.overture.ast.definitions.ANamedTraceDefinition;
34: import org.overture.ast.definitions.ATypeDefinition;
35: import org.overture.ast.definitions.PDefinition;
36: import org.overture.ast.expressions.PExp;
37: import org.overture.ast.factory.AstFactory;
38: import org.overture.ast.lex.Dialect;
39: import org.overture.ast.lex.LexIdentifierToken;
40: import org.overture.ast.lex.LexLocation;
41: import org.overture.ast.lex.LexNameToken;
42: import org.overture.ast.lex.LexToken;
43: import org.overture.ast.lex.VDMToken;
44: import org.overture.ast.modules.AModuleModules;
45: import org.overture.ast.statements.PStm;
46: import org.overture.ast.types.PType;
47: import org.overture.ast.util.modules.ModuleList;
48: import org.overture.interpreter.annotations.INAnnotation;
49: import org.overture.interpreter.assistant.IInterpreterAssistantFactory;
50: import org.overture.interpreter.assistant.InterpreterAssistantFactory;
51: import org.overture.interpreter.debug.DBGPReader;
52: import org.overture.interpreter.messages.Console;
53: import org.overture.interpreter.scheduler.BasicSchedulableThread;
54: import org.overture.interpreter.scheduler.CTMainThread;
55: import org.overture.interpreter.scheduler.InitThread;
56: import org.overture.interpreter.scheduler.MainThread;
57: import org.overture.interpreter.traces.CallSequence;
58: import org.overture.interpreter.util.ModuleListInterpreter;
59: import org.overture.interpreter.values.CPUValue;
60: import org.overture.interpreter.values.Value;
61: import org.overture.parser.lex.LexTokenReader;
62: import org.overture.parser.messages.VDMErrorsException;
63: import org.overture.parser.syntax.ExpressionReader;
64: import org.overture.parser.syntax.ParserException;
65: import org.overture.pog.pub.IProofObligationList;
66: import org.overture.typechecker.Environment;
67: import org.overture.typechecker.ModuleEnvironment;
68:
69: /**
70: * The VDM-SL module interpreter.
71: */
72:
73: public class ModuleInterpreter extends Interpreter
74: {
75:         /** A list of module definitions in the specification. */
76:         public final ModuleListInterpreter modules;
77:         /** The module starting execution. */
78:         public AModuleModules defaultModule;
79:
80:         /**
81:          * Create an Interpreter from the list of modules passed.
82:          *
83:          * @param modules
84:          * @throws Exception
85:          */
86:         public ModuleInterpreter(ModuleList modules) throws Exception
87:         {
88:                 this(new InterpreterAssistantFactory(), modules);
89:         }
90:
91:         /**
92:          * Create an Interpreter from the list of modules passed.
93:          *
94:          * @param assistantFactory
95:          * @param modules
96:          * @throws Exception
97:          */
98:         public ModuleInterpreter(IInterpreterAssistantFactory assistantFactory,
99:                         ModuleList modules) throws Exception
100:         {
101:                 super(assistantFactory);
102:                 this.modules = new ModuleListInterpreter(modules);
103:
104:•                if (modules.isEmpty())
105:                 {
106:                         setDefaultName(null);
107:                 } else
108:                 {
109:                         setDefaultName(modules.get(0).getName().getName());
110:                 }
111:         }
112:
113:         @Override
114:         public PStm findStatement(File file, int lineno)
115:         {
116:                 return assistantFactory.createAModuleModulesAssistant().findStatement(modules, file, lineno);
117:         }
118:
119:         @Override
120:         public PExp findExpression(File file, int lineno)
121:         {
122:                 return assistantFactory.createAModuleModulesAssistant().findExpression(modules, file, lineno);
123:         }
124:
125:         /**
126:          * Set the default module to the name given.
127:          *
128:          * @param mname
129:          * The name of the new default module.
130:          * @throws Exception
131:          * The module name is not known.
132:          */
133:
134:         @Override
135:         public void setDefaultName(String mname) throws Exception
136:         {
137:•                if (mname == null)
138:                 {
139:                         defaultModule = AstFactory.newAModuleModules();
140:                 } else
141:                 {
142:•                        for (AModuleModules m : modules)
143:                         {
144:•                                if (m.getName().getName().equals(mname))
145:                                 {
146:                                         defaultModule = m;
147:                                         return;
148:                                 }
149:                         }
150:
151:                         throw new Exception("Module " + mname + " not loaded");
152:                 }
153:         }
154:
155:         /**
156:          * @return The current default module name.
157:          */
158:
159:         @Override
160:         public String getDefaultName()
161:         {
162:                 return defaultModule.getName().getName();
163:         }
164:
165:         /**
166:          * @return The current default module's file name.
167:          */
168:
169:         @Override
170:         public File getDefaultFile()
171:         {
172:                 return defaultModule.getName().getLocation().getFile();
173:         }
174:
175:         @Override
176:         public Set<File> getSourceFiles()
177:         {
178:                 return modules.getSourceFiles();
179:         }
180:
181:         /**
182:          * @return The state context for the current default module.
183:          */
184:
185:         public Context getStateContext()
186:         {
187:                 return assistantFactory.createAModuleModulesAssistant().getStateContext(defaultModule);
188:         }
189:
190:         @Override
191:         public Environment getGlobalEnvironment()
192:         {
193:                 return new ModuleEnvironment(assistantFactory, defaultModule);
194:         }
195:         
196:         @Override
197:         public Environment getGlobalEnvironment(String module)
198:         {
199:                 return new ModuleEnvironment(assistantFactory, findModule(module));
200:         }
201:
202:         /**
203:          * @return The list of loaded modules.
204:          */
205:
206:         public ModuleList getModules()
207:         {
208:                 return modules;
209:         }
210:
211:         @Override
212:         public void init(DBGPReader dbgp)
213:         {
214:                 VdmRuntime.initialize();
215:                 InitThread iniThread = new InitThread(Thread.currentThread());
216:                 BasicSchedulableThread.setInitialThread(iniThread);
217:                 scheduler.init();
218:                 CPUValue.init(scheduler, assistantFactory);
219:                 initialContext = assistantFactory.createModuleListAssistant().createInitialContext(modules);
220:                 assistantFactory.createModuleListAssistant().initialize(initialContext, modules, dbgp);
221:                 Annotation.init(INAnnotation.class, initialContext);
222:         }
223:
224:         @Override
225:         public void traceInit(DBGPReader dbgp)
226:         {
227:                 scheduler.reset();
228:                 initialContext = assistantFactory.createModuleListAssistant().createInitialContext(modules);
229:                 assistantFactory.createModuleListAssistant().initialize(initialContext, modules, dbgp);
230:         }
231:
232:         @Override
233:         protected PExp parseExpression(String line, String module) throws Exception
234:         {
235:                 LexTokenReader ltr = new LexTokenReader(line, Dialect.VDM_SL, Console.charset);
236:                 ExpressionReader reader = new ExpressionReader(ltr);
237:                 reader.setCurrentModule(getDefaultName());
238:                 PExp ast = reader.readExpression();
239:                 LexToken end = ltr.getLast();
240:                 
241:•                if (!end.is(VDMToken.EOF))
242:                 {
243:                         throw new ParserException(2330, "Tokens found after expression at " + end, new LexLocation(), 0);
244:                 }
245:                 
246:                 return ast;
247:         }
248:
249:         /**
250:          * Parse the line passed, type check it and evaluate it as an expression in the initial module context (with default
251:          * module's state).
252:          *
253:          * @param line
254:          * A VDM expression.
255:          * @return The value of the expression.
256:          * @throws Exception
257:          * Parser, type checking or runtime errors.
258:          */
259:
260:         @Override
261:         public Value execute(String line, DBGPReader dbgp) throws Exception
262:         {
263:                 PExp expr = parseExpression(line, getDefaultName());
264:                 Environment env = getGlobalEnvironment();
265:                 typeCheck(expr, env);
266:
267:                 Context mainContext = new StateContext(assistantFactory, defaultModule.getName().getLocation(), "module scope", null, assistantFactory.createAModuleModulesAssistant().getStateContext(defaultModule));
268:
269:                 mainContext.putAll(initialContext);
270:                 mainContext.setThreadState(dbgp, null);
271:                 clearBreakpointHits();
272:
273:                 // scheduler.reset();
274:
275:                 InitThread iniThread = new InitThread(Thread.currentThread());
276:                 BasicSchedulableThread.setInitialThread(iniThread);
277:
278:                 MainThread main = new MainThread(expr, mainContext);
279:                 main.start();
280:                 scheduler.start(main);
281:
282:                 return main.getResult(); // Can throw ContextException
283:         }
284:
285:         /**
286:          * Parse the line passed, and evaluate it as an expression in the context passed.
287:          *
288:          * @param line
289:          * A VDM expression.
290:          * @param ctxt
291:          * The context in which to evaluate the expression.
292:          * @return The value of the expression.
293:          * @throws Exception
294:          * Parser or runtime errors.
295:          */
296:
297:         @Override
298:         public Value evaluate(String line, Context ctxt) throws Exception
299:         {
300:                 PExp expr = parseExpression(line, getDefaultName());
301:                 Environment env = new ModuleEnvironment(assistantFactory, defaultModule);
302:
303:                 try
304:                 {
305:                         typeCheck(expr, env);
306:                 } catch (VDMErrorsException e)
307:                 {
308:                         // We don't care... we just needed to type check it.
309:                 }
310:
311:                 ctxt.threadState.init();
312:
313:                 try
314:                 {
315:                         return expr.apply(VdmRuntime.getExpressionEvaluator(), ctxt);
316:                 } catch (Exception e)
317:                 {
318:                         throw e;
319:                 }
320:         }
321:
322:         @Override
323:         public AModuleModules findModule(String module)
324:         {
325:                 LexIdentifierToken name = new LexIdentifierToken(module, false, null);
326:                 return modules.findModule(name);
327:         }
328:
329:         @Override
330:         protected ANamedTraceDefinition findTraceDefinition(LexNameToken name)
331:         {
332:                 return modules.findTraceDefinition(name);
333:         }
334:
335:         // /**
336:         // * Find a Statement in the given file that starts on the given line.
337:         // * If there are none, return null.
338:         // *
339:         // * @param file The file name to search.
340:         // * @param lineno The line number in the file.
341:         // * @return A Statement starting on the line, or null.
342:         // */
343:         //
344:         // @Override
345:         // public PStm findStatement(File file, int lineno)
346:         // {
347:         // return modules.findStatement(file, lineno);
348:         // }
349:
350:         // /**
351:         // * Find an Expression in the given file that starts on the given line.
352:         // * If there are none, return null.
353:         // *
354:         // * @param file The file name to search.
355:         // * @param lineno The line number in the file.
356:         // * @return An Expression starting on the line, or null.
357:         // */
358:         //
359:         // @Override
360:         // public PExp findExpression(File file, int lineno)
361:         // {
362:         // return modules.findExpression(file, lineno);
363:         // }
364:
365:         @Override
366:         public IProofObligationList getProofObligations() throws AnalysisException
367:         {
368:                 return assistantFactory.createModuleListAssistant().getProofObligations(modules);
369:         }
370:
371:         @Override
372:         public Context getInitialTraceContext(ANamedTraceDefinition tracedef,
373:                         boolean debug) throws ValueException
374:         {
375:                 Context mainContext = new StateContext(assistantFactory, defaultModule.getName().getLocation(), "module scope", initialContext, assistantFactory.createAModuleModulesAssistant().getStateContext(defaultModule));
376:
377:                 mainContext.putAll(initialContext);
378:                 mainContext.setThreadState(mainContext.threadState.dbgp, CPUValue.vCPU);
379:
380:                 return mainContext;
381:         }
382:
383:         @Override
384:         public List<Object> runOneTrace(ANamedTraceDefinition tracedef,
385:                         CallSequence test, boolean debug)
386:         {
387:                 List<Object> list = new Vector<Object>();
388:                 Context ctxt = null;
389:
390:                 try
391:                 {
392:                         ctxt = getInitialTraceContext(tracedef, debug);
393:
394:                 } catch (ValueException e)
395:                 {
396:                         list.add(e.getMessage());
397:                         return list;
398:                 }
399:
400:                 clearBreakpointHits();
401:
402:                 // scheduler.reset();
403:                 CTMainThread main = new CTMainThread(test, ctxt, debug);
404:                 main.start();
405:                 scheduler.start(main);
406:
407:                 return main.getList();
408:         }
409:
410:         @Override
411:         public PType findType(String typename)
412:         {
413:•                for (AModuleModules module : modules)
414:                 {
415:•                        for (PDefinition def : module.getDefs())
416:                         {
417:•                                if (def instanceof ATypeDefinition)
418:                                 {
419:•                                        if (def.getName().equals(typename))
420:                                         {
421:                                                 return def.getType();
422:                                         }
423:                                 }
424:                         }
425:                 }
426:                 return null;
427:         }
428: }