Package: DBGPReader$1

DBGPReader$1

nameinstructionbranchcomplexitylinemethod
run()
M: 23 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 7 C: 0
0%
M: 1 C: 0
0%
{...}
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%

Coverage

1: /*******************************************************************************
2: *
3: *        Copyright (c) 2009 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.debug;
25:
26: import java.io.ByteArrayOutputStream;
27: import java.io.File;
28: import java.io.FileNotFoundException;
29: import java.io.IOException;
30: import java.io.InputStream;
31: import java.io.OutputStream;
32: import java.io.PrintWriter;
33: import java.io.UnsupportedEncodingException;
34: import java.net.InetAddress;
35: import java.net.Socket;
36: import java.net.SocketException;
37: import java.net.URI;
38: import java.net.URISyntaxException;
39: import java.nio.charset.Charset;
40: import java.util.Arrays;
41: import java.util.Iterator;
42: import java.util.List;
43: import java.util.Map;
44: import java.util.Map.Entry;
45: import java.util.Random;
46: import java.util.Set;
47: import java.util.Vector;
48:
49: import org.overture.ast.analysis.AnalysisException;
50: import org.overture.ast.definitions.AMutexSyncDefinition;
51: import org.overture.ast.definitions.APerSyncDefinition;
52: import org.overture.ast.definitions.PDefinition;
53: import org.overture.ast.definitions.SClassDefinition;
54: import org.overture.ast.expressions.AHistoryExp;
55: import org.overture.ast.expressions.PExp;
56: import org.overture.ast.factory.AstFactory;
57: import org.overture.ast.intf.lex.ILexLocation;
58: import org.overture.ast.intf.lex.ILexNameToken;
59: import org.overture.ast.lex.CoverageUtil;
60: import org.overture.ast.lex.Dialect;
61: import org.overture.ast.lex.LexLocation;
62: import org.overture.ast.lex.LexLocationUtils;
63: import org.overture.ast.lex.LexNameList;
64: import org.overture.ast.lex.LexNameToken;
65: import org.overture.ast.lex.LexToken;
66: import org.overture.ast.lex.VDMToken;
67: import org.overture.ast.messages.InternalException;
68: import org.overture.ast.modules.AModuleModules;
69: import org.overture.ast.statements.PStm;
70: import org.overture.ast.util.definitions.ClassList;
71: import org.overture.config.Release;
72: import org.overture.config.Settings;
73: import org.overture.interpreter.VDMJ;
74: import org.overture.interpreter.VDMPP;
75: import org.overture.interpreter.VDMRT;
76: import org.overture.interpreter.VDMSL;
77: import org.overture.interpreter.messages.Console;
78: import org.overture.interpreter.messages.rtlog.RTLogger;
79: import org.overture.interpreter.messages.rtlog.RTTextLogger;
80: import org.overture.interpreter.messages.rtlog.nextgen.NextGenRTLogger;
81: import org.overture.interpreter.runtime.Breakpoint;
82: import org.overture.interpreter.runtime.ClassContext;
83: import org.overture.interpreter.runtime.ClassInterpreter;
84: import org.overture.interpreter.runtime.Context;
85: import org.overture.interpreter.runtime.ContextException;
86: import org.overture.interpreter.runtime.Interpreter;
87: import org.overture.interpreter.runtime.LatexSourceFile;
88: import org.overture.interpreter.runtime.ModuleInterpreter;
89: import org.overture.interpreter.runtime.ObjectContext;
90: import org.overture.interpreter.runtime.SourceFile;
91: import org.overture.interpreter.runtime.StateContext;
92: import org.overture.interpreter.runtime.VdmRuntime;
93: import org.overture.interpreter.scheduler.BasicSchedulableThread;
94: import org.overture.interpreter.util.ExitStatus;
95: import org.overture.interpreter.values.CPUValue;
96: import org.overture.interpreter.values.NameValuePairMap;
97: import org.overture.interpreter.values.Value;
98: import org.overture.parser.config.Properties;
99: import org.overture.parser.lex.LexException;
100: import org.overture.parser.lex.LexTokenReader;
101: import org.overture.parser.syntax.ParserException;
102: import org.overture.pog.obligation.ProofObligationList;
103: import org.overture.pog.pub.IProofObligation;
104: import org.overture.pog.pub.IProofObligationList;
105: import org.overture.util.Base64;
106:
107: public class DBGPReader
108: {
109:         protected final String host;
110:         protected final int port;
111:         protected final String ideKey;
112:         protected final String expression;
113:         protected Socket socket;
114:         protected InputStream input;
115:         protected OutputStream output;
116:         protected final Interpreter interpreter;
117:         protected final CPUValue cpu;
118:
119:         protected int sessionId = 0;
120:         protected DBGPStatus status = null;
121:         protected DBGPReason statusReason = null;
122:         protected DBGPCommandType command = null;
123:         protected String transaction = "";
124:         protected DBGPFeatures features;
125:         protected byte separator = '\0';
126:
127:         protected Context breakContext = null;
128:         protected Breakpoint breakpoint = null;
129:         protected Value theAnswer = null;
130:         protected boolean breaksSuspended = false;
131:         protected boolean connected = false;
132:         protected RemoteControl remoteControl = null;
133:         protected boolean stopped = false;
134:
135:         protected boolean errorState = false;
136:
137:         protected static final int SOURCE_LINES = 5;
138:
139:         protected static List<DBGPReader> connectecReaders = new Vector<DBGPReader>();
140:
141:         @SuppressWarnings("unchecked")
142:         public static void main(String[] args)
143:         {
144:                 Settings.usingDBGP = true;
145:
146:                 String host = null;
147:                 int port = -1;
148:                 String ideKey = null;
149:                 Settings.dialect = null;
150:                 String expression = null;
151:                 List<File> files = new Vector<File>();
152:                 List<String> largs = Arrays.asList(args);
153:                 VDMJ controller = null;
154:                 boolean warnings = true;
155:                 boolean quiet = false;
156:                 String logfile = null;
157:                 boolean expBase64 = false;
158:                 File coverage = null;
159:                 String defaultName = null;
160:                 String remoteName = null;
161:                 Class<RemoteControl> remoteClass = null;
162:
163:                 Properties.init(); // Read properties file, if any
164:
165:                 for (Iterator<String> i = largs.iterator(); i.hasNext();)
166:                 {
167:                         String arg = i.next();
168:
169:                         if (arg.equals("-vdmsl"))
170:                         {
171:                                 controller = new VDMSL();
172:                         } else if (arg.equals("-vdmpp"))
173:                         {
174:                                 controller = new VDMPP();
175:                         } else if (arg.equals("-vdmrt"))
176:                         {
177:                                 controller = new VDMRT();
178:                         } else if (arg.equals("-h"))
179:                         {
180:                                 if (i.hasNext())
181:                                 {
182:                                         host = i.next();
183:                                 } else
184:                                 {
185:                                         usage("-h option requires a hostname");
186:                                 }
187:                         } else if (arg.equals("-p"))
188:                         {
189:                                 try
190:                                 {
191:                                         port = Integer.parseInt(i.next());
192:                                 } catch (Exception e)
193:                                 {
194:                                         usage("-p option requires a port");
195:                                 }
196:                         } else if (arg.equals("-k"))
197:                         {
198:                                 if (i.hasNext())
199:                                 {
200:                                         ideKey = i.next();
201:                                 } else
202:                                 {
203:                                         usage("-k option requires a key");
204:                                 }
205:                         } else if (arg.equals("-e"))
206:                         {
207:                                 if (i.hasNext())
208:                                 {
209:                                         expression = i.next();
210:                                 } else
211:                                 {
212:                                         usage("-e option requires an expression");
213:                                 }
214:                         } else if (arg.equals("-e64"))
215:                         {
216:                                 if (i.hasNext())
217:                                 {
218:                                         expression = i.next();
219:                                         expBase64 = true;
220:                                 } else
221:                                 {
222:                                         usage("-e64 option requires an expression");
223:                                 }
224:                         } else if (arg.equals("-c"))
225:                         {
226:                                 if (i.hasNext())
227:                                 {
228:                                         if (controller == null)
229:                                         {
230:                                                 usage("-c must come after <-vdmpp|-vdmsl|-vdmrt>");
231:                                         }
232:
233:                                         controller.setCharset(validateCharset(i.next()));
234:                                 } else
235:                                 {
236:                                         usage("-c option requires a charset name");
237:                                 }
238:                         } else if (arg.equals("-r"))
239:                         {
240:                                 if (i.hasNext())
241:                                 {
242:                                         Settings.release = Release.lookup(i.next());
243:
244:                                         if (Settings.release == null)
245:                                         {
246:                                                 usage("-r option must be " + Release.list());
247:                                         }
248:                                 } else
249:                                 {
250:                                         usage("-r option requires a VDM release");
251:                                 }
252:                         } else if (arg.equals("-pre"))
253:                         {
254:                                 Settings.prechecks = false;
255:                         } else if (arg.equals("-post"))
256:                         {
257:                                 Settings.postchecks = false;
258:                         } else if (arg.equals("-inv"))
259:                         {
260:                                 Settings.invchecks = false;
261:                         } else if (arg.equals("-dtc"))
262:                         {
263:                                 // NB. Turn off both when no DTC
264:                                 Settings.invchecks = false;
265:                                 Settings.dynamictypechecks = false;
266:                         } else if (arg.equals("-measures"))
267:                         {
268:                                 Settings.measureChecks = false;
269:                         } else if (arg.equals("-log"))
270:                         {
271:                                 if (i.hasNext())
272:                                 {
273:                                         try
274:                                         {
275:                                                 logfile = new URI(i.next()).getPath();
276:                                         } catch (URISyntaxException e)
277:                                         {
278:                                                 usage(e.getMessage() + ": " + arg);
279:                                         } catch (IllegalArgumentException e)
280:                                         {
281:                                                 usage(e.getMessage() + ": " + arg);
282:                                         }
283:                                 } else
284:                                 {
285:                                         usage("-log option requires a filename");
286:                                 }
287:                         } else if (arg.equals("-w"))
288:                         {
289:                                 warnings = false;
290:                         } else if (arg.equals("-q"))
291:                         {
292:                                 quiet = true;
293:                         } else if (arg.equals("-coverage"))
294:                         {
295:                                 if (i.hasNext())
296:                                 {
297:                                         try
298:                                         {
299:                                                 coverage = new File(new URI(i.next()));
300:
301:                                                 if (!coverage.isDirectory())
302:                                                 {
303:                                                         usage("Coverage location is not a directory");
304:                                                 }
305:                                         } catch (URISyntaxException e)
306:                                         {
307:                                                 usage(e.getMessage() + ": " + arg);
308:                                         } catch (IllegalArgumentException e)
309:                                         {
310:                                                 usage(e.getMessage() + ": " + arg);
311:                                         }
312:                                 } else
313:                                 {
314:                                         usage("-coverage option requires a directory name");
315:                                 }
316:                         } else if (arg.equals("-default64"))
317:                         {
318:                                 if (i.hasNext())
319:                                 {
320:                                         defaultName = i.next();
321:                                 } else
322:                                 {
323:                                         usage("-default64 option requires a name");
324:                                 }
325:                         } else if (arg.equals("-remote"))
326:                         {
327:                                 if (i.hasNext())
328:                                 {
329:                                         remoteName = i.next();
330:                                 } else
331:                                 {
332:                                         usage("-remote option requires a Java classname");
333:                                 }
334:                         } else if (arg.equals("-consoleName"))
335:                         {
336:                                 if (i.hasNext())
337:                                 {
338:                                         LexTokenReader.consoleFileName = i.next();
339:                                 } else
340:                                 {
341:                                         usage("-consoleName option requires a console name");
342:                                 }
343:                         } else if (arg.equals("-strict"))
344:                         {
345:                                 Settings.strict = true;
346:                         } else if (arg.startsWith("-"))
347:                         {
348:                                 usage("Unknown option " + arg);
349:                         } else
350:                         {
351:                                 try
352:                                 {
353:                                         File dir = new File(new URI(arg));
354:
355:                                         if (dir.isDirectory())
356:                                         {
357:                                                 for (File file : dir.listFiles(Settings.dialect.getFilter()))
358:                                                 {
359:                                                         if (file.isFile())
360:                                                         {
361:                                                                 files.add(file);
362:                                                         }
363:                                                 }
364:                                         } else
365:                                         {
366:                                                 files.add(dir);
367:                                         }
368:                                 } catch (URISyntaxException e)
369:                                 {
370:                                         usage(e.getMessage() + ": " + arg);
371:                                 } catch (IllegalArgumentException e)
372:                                 {
373:                                         usage(e.getMessage() + ": " + arg);
374:                                 }
375:                         }
376:                 }
377:
378:                 if (host == null || port == -1 || controller == null || ideKey == null
379:                                 || expression == null || Settings.dialect == null
380:                                 || files.isEmpty())
381:                 {
382:                         usage("Missing mandatory arguments");
383:                 }
384:
385:                 if (Settings.dialect != Dialect.VDM_RT && logfile != null)
386:                 {
387:                         usage("-log can only be used with -vdmrt");
388:                 }
389:
390:                 if (expBase64)
391:                 {
392:                         try
393:                         {
394:                                 byte[] bytes = Base64.decode(expression);
395:                                 expression = new String(bytes, VDMJ.filecharset);
396:                         } catch (Exception e)
397:                         {
398:                                 usage("Malformed -e64 base64 expression");
399:                         }
400:                 }
401:
402:                 if (defaultName != null)
403:                 {
404:                         try
405:                         {
406:                                 byte[] bytes = Base64.decode(defaultName);
407:                                 defaultName = new String(bytes, VDMJ.filecharset);
408:                         } catch (Exception e)
409:                         {
410:                                 usage("Malformed -default64 base64 name");
411:                         }
412:                 }
413:
414:                 if (remoteName != null)
415:                 {
416:                         try
417:                         {
418:                                 Class<?> cls = ClassLoader.getSystemClassLoader().loadClass(remoteName);
419:                                 remoteClass = (Class<RemoteControl>) cls;
420:                         } catch (ClassNotFoundException e)
421:                         {
422:                                 usage("Cannot locate " + remoteName + " on the CLASSPATH");
423:                         }
424:                 }
425:
426:                 controller.setWarnings(warnings);
427:                 controller.setQuiet(quiet);
428:
429:                 if (controller.parse(files) == ExitStatus.EXIT_OK)
430:                 {
431:                         if (controller.typeCheck() == ExitStatus.EXIT_OK)
432:                         {
433:                                 try
434:                                 {
435:                                         if (logfile != null)
436:                                         {
437:                                                 RTLogger.setLogfile(RTTextLogger.class, new File(logfile));
438:                                                 RTLogger.setLogfile(NextGenRTLogger.class, new File(logfile));
439:                                         }
440:
441:                                         Interpreter i = controller.getInterpreter();
442:
443:                                         if (defaultName != null)
444:                                         {
445:                                                 i.setDefaultName(defaultName);
446:                                         }
447:
448:                                         RemoteControl remote = remoteClass == null ? null
449:                                                         : remoteClass.newInstance();
450:
451:                                         new DBGPReader(host, port, ideKey, i, expression, null).startup(remote);
452:
453:                                         if (coverage != null)
454:                                         {
455:                                                 writeCoverage(i, coverage);
456:                                         }
457:
458:                                         RTLogger.dump(true);
459:                                         System.exit(0);
460:                                 } catch (ContextException e)
461:                                 {
462:                                         System.out.println("Initialization: " + e);
463:                                         
464:                                         if (e.isStackOverflow())
465:                                         {
466:                                                 e.ctxt.printStackFrames(Console.out);
467:                                         }
468:                                         else
469:                                         {
470:                                                 e.ctxt.printStackTrace(Console.out, true);
471:                                         }
472:                                         
473:                                         RTLogger.dump(true);
474:                                         System.exit(3);
475:                                 } catch (Exception e)
476:                                 {
477:                                         System.out.println("Initialization: " + e);
478:                                         RTLogger.dump(true);
479:                                         System.exit(3);
480:                                 }
481:                         } else
482:                         {
483:                                 System.exit(2);
484:                         }
485:                 } else
486:                 {
487:                         System.exit(1);
488:                 }
489:         }
490:
491:         protected static void usage(String string)
492:         {
493:                 System.err.println(string);
494:                 System.err.println("Usage: -h <host> -p <port> -k <ide key> <-vdmpp|-vdmsl|-vdmrt>"
495:                                 + " -e <expression> | -e64 <base64 expression>"
496:                                 + " [-w] [-q] [-log <logfile URL>] [-c <charset>] [-r <release>]"
497:                                 + " [-pre] [-post] [-inv] [-dtc] [-measures]"
498:                                 + " [-coverage <dir URL>] [-default64 <base64 name>]"
499:                                 + " [-remote <class>] [-consoleName <console>] [-baseDir <File>] {<filename URLs>}");
500:
501:                 System.exit(1);
502:         }
503:
504:         protected static String validateCharset(String cs)
505:         {
506:                 if (!Charset.isSupported(cs))
507:                 {
508:                         System.err.println("Charset " + cs + " is not supported\n");
509:                         System.err.println("Available charsets:");
510:                         System.err.println("Default = " + Charset.defaultCharset());
511:                         Map<String, Charset> available = Charset.availableCharsets();
512:
513:                         for (Entry<String, Charset> name : available.entrySet())
514:                         {
515:                                 System.err.println(name.getKey() + " "
516:                                                 + name.getValue().aliases());
517:                         }
518:
519:                         System.err.println("");
520:                         usage("Charset " + cs + " is not supported");
521:                 }
522:
523:                 return cs;
524:         }
525:
526:         public DBGPReader(String host, int port, String ideKey,
527:                         Interpreter interpreter, String expression, CPUValue cpu)
528:         {
529:                 this.host = host;
530:                 this.port = port;
531:                 this.ideKey = ideKey;
532:                 this.expression = expression;
533:                 this.interpreter = interpreter;
534:                 this.cpu = cpu;
535:         }
536:
537:         public DBGPReader newThread(CPUValue _cpu)
538:         {
539:                 DBGPReader r = new DBGPReader(host, port, ideKey, interpreter, null, _cpu);
540:                 r.command = DBGPCommandType.UNKNOWN;
541:                 r.transaction = "?";
542:                 return r;
543:         }
544:
545:         protected void connect() throws IOException
546:         {
547:                 if (!connected)
548:                 {
549:                         if (port > 0)
550:                         {
551:                                 InetAddress server = InetAddress.getByName(host);
552:                                 socket = new Socket(server, port);
553:                                 input = socket.getInputStream();
554:                                 output = socket.getOutputStream();
555:                         } else
556:                         {
557:                                 socket = null;
558:                                 input = System.in;
559:                                 output = System.out;
560:                                 separator = ' ';
561:                         }
562:
563:                         connected = true;
564:                         addThisReader();
565:                         init();
566:                         interpreter.init(this);
567:
568:                         run(); // New threads wait for a "run -i"
569:                 }
570:         }
571:
572:         protected void startup(RemoteControl remote) throws IOException
573:         {
574:                 remoteControl = remote; // Main thread only
575:                 connect();
576:         }
577:
578:         protected void init() throws IOException
579:         {
580:                 sessionId = Math.abs(new Random().nextInt(1000000));
581:                 status = DBGPStatus.STARTING;
582:                 statusReason = DBGPReason.OK;
583:                 features = new DBGPFeatures();
584:
585:                 StringBuilder sb = new StringBuilder();
586:
587:                 sb.append("<init ");
588:                 sb.append("appid=\"");
589:                 sb.append(features.getProperty(DBGPFeatures.LANGUAGE_NAME));
590:                 sb.append("\" ");
591:                 sb.append("idekey=\"" + ideKey + "\" ");
592:                 sb.append("session=\"" + sessionId + "\" ");
593:                 sb.append("thread=\"");
594:
595:                 String threadName = BasicSchedulableThread.getThreadName(Thread.currentThread());
596:
597:                 if (threadName != null)
598:                 {
599:                         sb.append(threadName);
600:                 } else
601:                 {
602:                         sb.append(Thread.currentThread().getName());
603:                 }
604:                 if (cpu != null)
605:                 {
606:                         sb.append(" on ");
607:                         sb.append(cpu.getName());
608:                 }
609:
610:                 sb.append("\" ");
611:                 sb.append("parent=\"");
612:                 sb.append(features.getProperty(DBGPFeatures.LANGUAGE_NAME));
613:                 sb.append("\" ");
614:                 sb.append("language=\"");
615:                 sb.append(features.getProperty(DBGPFeatures.LANGUAGE_NAME));
616:                 sb.append("\" ");
617:                 sb.append("protocol_version=\"");
618:                 sb.append(features.getProperty(DBGPFeatures.PROTOCOL_VERSION));
619:                 sb.append("\"");
620:
621:                 Set<File> files = interpreter.getSourceFiles();
622:                 sb.append(" fileuri=\"");
623:                 sb.append(files.iterator().next().toURI()); // Any old one...
624:                 sb.append("\"");
625:
626:                 sb.append("/>\n");
627:
628:                 write(sb);
629:         }
630:
631:         protected String readLine() throws IOException
632:         {
633:                 try
634:                 {
635:                         StringBuilder line = new StringBuilder();
636:                         int c = input.read();
637:                         while (c != '\n' && c > 0)
638:                         {
639:                                 if (c != '\r')
640:                                 {
641:                                         line.append((char) c); // Ignore CRs
642:                                 }
643:                                 c = input.read();
644:                         }
645:
646:                         return line.length() == 0 && c == -1 ? null : line.toString();
647:                 } catch (SocketException e)
648:                 {
649:                         // If DBGP is stopped there is no guarantee that the IDE will be available
650:                         if (stopped)
651:                         {
652:                                 return null;
653:                         } else
654:                         {
655:                                 throw e;
656:                         }
657:                 }
658:         }
659:
660:         protected void write(StringBuilder data) throws IOException
661:         {
662:                 if (output == null)
663:                 {
664:                         // TODO: Handle the error in VDMJ, terminate?
665:                         System.err.println("Socket to IDE not valid.");
666:                         return;
667:                 }
668:                 byte[] header = "<?xml version=\"1.0\" encoding=\"UTF-8\"?>".getBytes("UTF-8");
669:                 byte[] body = data.toString().getBytes("UTF-8");
670:                 byte[] size = Integer.toString(header.length + body.length).getBytes("UTF-8");
671:
672:                 output.write(size);
673:                 output.write(separator);
674:                 output.write(header);
675:                 output.write(body);
676:                 output.write(separator);
677:
678:                 output.flush();
679:         }
680:
681:         protected void response(StringBuilder hdr, StringBuilder body)
682:                         throws IOException
683:         {
684:                 StringBuilder sb = new StringBuilder();
685:
686:                 sb.append("<response command=\"");
687:                 sb.append(command);
688:                 sb.append("\"");
689:
690:                 if (hdr != null)
691:                 {
692:                         sb.append(" ");
693:                         sb.append(hdr);
694:                 }
695:
696:                 sb.append(" transaction_id=\"");
697:                 sb.append(transaction);
698:                 sb.append("\"");
699:
700:                 if (body != null)
701:                 {
702:                         sb.append(">");
703:                         sb.append(body);
704:                         sb.append("</response>\n");
705:                 } else
706:                 {
707:                         sb.append("/>\n");
708:                 }
709:
710:                 write(sb);
711:         }
712:
713:         protected void errorResponse(DBGPErrorCode errorCode, String reason)
714:         {
715:                 try
716:                 {
717:                         StringBuilder sb = new StringBuilder();
718:
719:                         sb.append("<error code=\"");
720:                         sb.append(errorCode.value);
721:                         sb.append("\" apperr=\"\"><message>");
722:                         sb.append(quote(reason));
723:                         sb.append("</message></error>");
724:
725:                         response(null, sb);
726:                 } catch (SocketException e)
727:                 {
728:                         // Do not report these since the socket connection is down.
729:                 } catch (IOException e)
730:                 {
731:                         throw new InternalException(29, "DBGP: " + reason);
732:                 }
733:         }
734:
735:         protected void statusResponse() throws IOException
736:         {
737:                 statusResponse(status, statusReason);
738:         }
739:
740:         protected void statusResponse(DBGPStatus s, DBGPReason reason)
741:                         throws IOException
742:         {
743:                 StringBuilder sb = new StringBuilder();
744:
745:                 if (s == DBGPStatus.STOPPED)
746:                 {
747:                         stopped = true;
748:                 }
749:
750:                 status = s;
751:                 statusReason = reason;
752:
753:                 sb.append("status=\"");
754:                 sb.append(status);
755:                 sb.append("\"");
756:                 sb.append(" reason=\"");
757:                 sb.append(statusReason);
758:                 sb.append("\"");
759:
760:                 response(sb, null);
761:         }
762:
763:         protected StringBuilder breakpointResponse(Breakpoint bp)
764:         {
765:                 StringBuilder sb = new StringBuilder();
766:
767:                 sb.append("<breakpoint id=\"" + bp.number + "\"");
768:                 sb.append(" type=\"line\"");
769:                 sb.append(" state=\"" + (bp.isEnabled() ? "enabled" : "disabled")
770:                                 + "\"");
771:                 sb.append(" filename=\"" + bp.location.getFile().toURI() + "\"");
772:                 sb.append(" lineno=\"" + bp.location.getStartLine() + "\"");
773:                 sb.append(">");
774:
775:                 if (bp.trace != null)
776:                 {
777:                         sb.append("<expression>" + quote(bp.trace) + "</expression>");
778:                 }
779:
780:                 sb.append("</breakpoint>");
781:
782:                 return sb;
783:         }
784:
785:         protected StringBuilder stackResponse(ILexLocation location, int level)
786:         {
787:                 StringBuilder sb = new StringBuilder();
788:
789:                 sb.append("<stack level=\"" + level + "\"");
790:                 sb.append(" type=\"file\"");
791:                 sb.append(" filename=\"" + location.getFile().toURI() + "\"");
792:                 sb.append(" lineno=\"" + location.getStartLine() + "\"");
793:                 sb.append(" cmdbegin=\"" + location.getStartLine() + ":"
794:                                 + location.getStartPos() + "\"");
795:                 sb.append("/>");
796:
797:                 return sb;
798:         }
799:
800:         protected StringBuilder propertyResponse(NameValuePairMap vars,
801:                         DBGPContextType context) throws UnsupportedEncodingException
802:         {
803:                 StringBuilder sb = new StringBuilder();
804:
805:                 for (Entry<ILexNameToken, Value> e : vars.entrySet())
806:                 {
807:                         sb.append(propertyResponse(e.getKey(), e.getValue(), context));
808:                 }
809:
810:                 return sb;
811:         }
812:
813:         protected StringBuilder propertyResponse(ILexNameToken name, Value value,
814:                         DBGPContextType context) throws UnsupportedEncodingException
815:         {
816:                 return propertyResponse(name.getName(), name.getExplicit(true).toString(), name.getModule(), value.toString());
817:         }
818:
819:         protected StringBuilder propertyResponse(String name, String fullname,
820:                         String clazz, String value) throws UnsupportedEncodingException
821:         {
822:                 StringBuilder sb = new StringBuilder();
823:
824:                 sb.append("<property");
825:                 sb.append(" name=\"" + quote(name) + "\"");
826:                 sb.append(" fullname=\"" + quote(fullname) + "\"");
827:                 sb.append(" type=\"string\"");
828:                 sb.append(" classname=\"" + clazz + "\"");
829:                 sb.append(" constant=\"0\"");
830:                 sb.append(" children=\"0\"");
831:                 sb.append(" size=\"" + value.length() + "\"");
832:                 sb.append(" encoding=\"base64\"");
833:                 sb.append("><![CDATA[");
834:                 sb.append(Base64.encode(value.getBytes("UTF-8")));
835:                 sb.append("]]></property>");
836:
837:                 return sb;
838:         }
839:
840:         protected void cdataResponse(String msg) throws IOException
841:         {
842:                 // Send back a CDATA response with a plain message
843:                 response(null, new StringBuilder("<![CDATA[" + quote(msg) + "]]>"));
844:         }
845:
846:         protected static String quote(String in)
847:         {
848:                 return in.replace("&", "&").replace("<", "<").replace(">", ">").replace("\"", """);
849:         }
850:
851:         protected void run() throws IOException
852:         {
853:                 String line = null;
854:
855:                 do
856:                 {
857:                         line = readLine();
858:                 } while (line != null && process(line));
859:         }
860:
861:         public void stopped(Context ctxt, ILexLocation location)
862:         {
863:                 stopped(ctxt, new Breakpoint(location));
864:         }
865:
866:         public void stopped(Context ctxt, Breakpoint bp)
867:         {
868:                 if (breaksSuspended)
869:                 {
870:                         return; // We're inside an eval command, so don't stop
871:                 }
872:
873:                 try
874:                 {
875:                         connect();
876:
877:                         breakContext = ctxt;
878:                         breakpoint = bp;
879:                         if (errorState)
880:                         {
881:                                 statusResponse(DBGPStatus.BREAK, DBGPReason.ERROR);
882:                         } else
883:                         {
884:                                 statusResponse(DBGPStatus.BREAK, DBGPReason.OK);
885:                         }
886:                         run();
887:
888:                         breakContext = null;
889:                         breakpoint = null;
890:
891:                 } catch (Exception e)
892:                 {
893:                         errorResponse(DBGPErrorCode.INTERNAL_ERROR, e.getMessage());
894:                 }
895:         }
896:
897:         public void setErrorState()
898:         {
899:                 errorState = true;
900:         }
901:
902:         public void invocationError(Throwable e)
903:         {
904:                 String message = e.getMessage();
905:
906:                 if (e instanceof StackOverflowError)
907:                 {
908:                         message = "StackOverflowError:\n Try to increase Java Stack size by adding -Xss4M to the Virtual Machine running the debugger";// +getStackTrace(e));
909:                 }
910:
911:                 errorResponse(DBGPErrorCode.INTERNAL_ERROR, message);
912:         }
913:
914:         public void tracing(String display)
915:         {
916:                 try
917:                 {
918:                         connect();
919:                         cdataResponse(display);
920:                 } catch (Exception e)
921:                 {
922:                         errorResponse(DBGPErrorCode.INTERNAL_ERROR, e.getMessage());
923:                 }
924:         }
925:
926:         public void complete(DBGPReason reason, ContextException ctxt)
927:         {
928:                 try
929:                 {
930:                         if (reason == DBGPReason.OK && !connected)
931:                         {
932:                                 // We never connected and there's no problem so just complete...
933:                         } else
934:                         {
935:                                 connect();
936:
937:                                 if (reason == DBGPReason.EXCEPTION && ctxt != null)
938:                                 {
939:                                         dyingThread(ctxt);
940:                                 } else
941:                                 {
942:                                         statusResponse(DBGPStatus.STOPPED, reason);
943:                                 }
944:                         }
945:                 } catch (IOException e)
946:                 {
947:                         try
948:                         {
949:                                 errorResponse(DBGPErrorCode.INTERNAL_ERROR, e.getMessage());
950:                         } catch (Throwable th)
951:                         {
952:                                 // Probably a shutdown race...
953:                         }
954:                 } finally
955:                 {
956:                         try
957:                         {
958:                                 if (socket != null)
959:                                 {
960:                                         socket.close();
961:                                 }
962:                         } catch (IOException e)
963:                         {
964:                                 // ?
965:                         }
966:                 }
967:         }
968:
969:         protected boolean process(String line)
970:         {
971:                 boolean carryOn = true;
972:
973:                 try
974:                 {
975:                         command = DBGPCommandType.UNKNOWN;
976:                         transaction = "?";
977:
978:                         String[] parts = line.split("\\s+");
979:                         DBGPCommand c = parse(parts);
980:
981:                         switch (c.type)
982:                         {
983:                                 case STATUS:
984:                                         processStatus(c);
985:                                         break;
986:
987:                                 case FEATURE_GET:
988:                                         processFeatureGet(c);
989:                                         break;
990:
991:                                 case FEATURE_SET:
992:                                         processFeatureSet(c);
993:                                         break;
994:
995:                                 case RUN:
996:                                         carryOn = processRun(c);
997:                                         break;
998:
999:                                 case EVAL:
1000:                                         carryOn = processEval(c);
1001:                                         break;
1002:
1003:                                 case EXPR:
1004:                                         carryOn = processExpr(c);
1005:                                         break;
1006:
1007:                                 case STEP_INTO:
1008:                                         processStepInto(c);
1009:                                         carryOn = false;
1010:                                         break;
1011:
1012:                                 case STEP_OVER:
1013:                                         processStepOver(c);
1014:                                         carryOn = false;
1015:                                         break;
1016:
1017:                                 case STEP_OUT:
1018:                                         processStepOut(c);
1019:                                         carryOn = false;
1020:                                         break;
1021:
1022:                                 case STOP:
1023:                                         processStop(c);
1024:                                         carryOn = false;
1025:                                         break;
1026:
1027:                                 case BREAKPOINT_GET:
1028:                                         breakpointGet(c);
1029:                                         break;
1030:
1031:                                 case BREAKPOINT_SET:
1032:                                         breakpointSet(c);
1033:                                         break;
1034:
1035:                                 case BREAKPOINT_UPDATE:
1036:                                         breakpointUpdate(c);
1037:                                         break;
1038:
1039:                                 case BREAKPOINT_REMOVE:
1040:                                         breakpointRemove(c);
1041:                                         break;
1042:
1043:                                 case BREAKPOINT_LIST:
1044:                                         breakpointList(c);
1045:                                         break;
1046:
1047:                                 case STACK_DEPTH:
1048:                                         stackDepth(c);
1049:                                         break;
1050:
1051:                                 case STACK_GET:
1052:                                         stackGet(c);
1053:                                         break;
1054:
1055:                                 case CONTEXT_NAMES:
1056:                                         contextNames(c);
1057:                                         break;
1058:
1059:                                 case CONTEXT_GET:
1060:                                         contextGet(c);
1061:                                         break;
1062:
1063:                                 case PROPERTY_GET:
1064:                                         propertyGet(c);
1065:                                         break;
1066:
1067:                                 case SOURCE:
1068:                                         processSource(c);
1069:                                         break;
1070:
1071:                                 case STDOUT:
1072:                                         processStdout(c);
1073:                                         break;
1074:
1075:                                 case STDERR:
1076:                                         processStderr(c);
1077:                                         break;
1078:
1079:                                 case DETACH:
1080:                                         carryOn = false;
1081:                                         break;
1082:
1083:                                 case XCMD_OVERTURE_CMD:
1084:                                         processOvertureCmd(c);
1085:                                         break;
1086:
1087:                                 case PROPERTY_SET:
1088:                                 default:
1089:                                         errorResponse(DBGPErrorCode.NOT_AVAILABLE, c.type.value);
1090:                         }
1091:                 } catch (DBGPException e)
1092:                 {
1093:                         errorResponse(e.code, e.reason);
1094:                 } catch (Throwable e)
1095:                 {
1096:                         errorResponse(DBGPErrorCode.INTERNAL_ERROR, e.getMessage());
1097:                 }
1098:
1099:                 return carryOn;
1100:         }
1101:
1102:         protected DBGPCommand parse(String[] parts) throws Exception
1103:         {
1104:                 // "<type> [<options>] [-- <base64 args>]"
1105:
1106:                 List<DBGPOption> options = new Vector<DBGPOption>();
1107:                 String args = null;
1108:                 boolean doneOpts = false;
1109:                 boolean gotXID = false;
1110:
1111:                 try
1112:                 {
1113:                         command = DBGPCommandType.lookup(parts[0]);
1114:
1115:                         for (int i = 1; i < parts.length; i++)
1116:                         {
1117:                                 if (doneOpts)
1118:                                 {
1119:                                         if (args != null)
1120:                                         {
1121:                                                 throw new Exception("Expecting one base64 arg after '--'");
1122:                                         } else
1123:                                         {
1124:                                                 args = parts[i];
1125:                                         }
1126:                                 } else
1127:                                 {
1128:                                         if (parts[i].equals("--"))
1129:                                         {
1130:                                                 doneOpts = true;
1131:                                         } else
1132:                                         {
1133:                                                 DBGPOptionType opt = DBGPOptionType.lookup(parts[i++]);
1134:
1135:                                                 if (opt == DBGPOptionType.TRANSACTION_ID)
1136:                                                 {
1137:                                                         gotXID = true;
1138:                                                         transaction = parts[i];
1139:                                                 }
1140:
1141:                                                 options.add(new DBGPOption(opt, parts[i]));
1142:                                         }
1143:                                 }
1144:                         }
1145:
1146:                         if (!gotXID)
1147:                         {
1148:                                 throw new Exception("No transaction_id");
1149:                         }
1150:                 } catch (DBGPException e)
1151:                 {
1152:                         throw e;
1153:                 } catch (ArrayIndexOutOfBoundsException e)
1154:                 {
1155:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, "Option arg missing");
1156:                 } catch (Exception e)
1157:                 {
1158:                         if (doneOpts)
1159:                         {
1160:                                 throw new DBGPException(DBGPErrorCode.PARSE, e.getMessage());
1161:                         } else
1162:                         {
1163:                                 throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, e.getMessage());
1164:                         }
1165:                 }
1166:
1167:                 return new DBGPCommand(command, options, args);
1168:         }
1169:
1170:         protected void checkArgs(DBGPCommand c, int n, boolean data)
1171:                         throws DBGPException
1172:         {
1173:                 if (data && c.data == null)
1174:                 {
1175:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1176:                 }
1177:
1178:                 if (c.options.size() != n)
1179:                 {
1180:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1181:                 }
1182:         }
1183:
1184:         protected void processStatus(DBGPCommand c) throws DBGPException,
1185:                         IOException
1186:         {
1187:                 checkArgs(c, 1, false);
1188:                 statusResponse();
1189:         }
1190:
1191:         protected void processFeatureGet(DBGPCommand c) throws DBGPException,
1192:                         IOException
1193:         {
1194:                 checkArgs(c, 2, false);
1195:                 DBGPOption option = c.getOption(DBGPOptionType.N);
1196:
1197:                 if (option == null)
1198:                 {
1199:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1200:                 }
1201:
1202:                 String feature = features.getProperty(option.value);
1203:                 StringBuilder hdr = new StringBuilder();
1204:                 StringBuilder body = new StringBuilder();
1205:
1206:                 if (feature == null)
1207:                 {
1208:                         // Unknown feature - unsupported in header; nothing in body
1209:                         hdr.append("feature_name=\"");
1210:                         hdr.append(option.value);
1211:                         hdr.append("\" supported=\"0\"");
1212:                 } else
1213:                 {
1214:                         // Known feature - supported in header; body reflects actual support
1215:                         hdr.append("feature_name=\"");
1216:                         hdr.append(option.value);
1217:                         hdr.append("\" supported=\"1\"");
1218:                         body.append(feature);
1219:                 }
1220:
1221:                 response(hdr, body);
1222:         }
1223:
1224:         protected void processFeatureSet(DBGPCommand c) throws DBGPException,
1225:                         IOException
1226:         {
1227:                 checkArgs(c, 3, false);
1228:                 DBGPOption option = c.getOption(DBGPOptionType.N);
1229:
1230:                 if (option == null)
1231:                 {
1232:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1233:                 }
1234:
1235:                 String feature = features.getProperty(option.value);
1236:
1237:                 if (feature == null)
1238:                 {
1239:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1240:                 }
1241:
1242:                 DBGPOption newval = c.getOption(DBGPOptionType.V);
1243:
1244:                 if (newval == null)
1245:                 {
1246:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1247:                 }
1248:
1249:                 features.setProperty(option.value, newval.value);
1250:
1251:                 StringBuilder hdr = new StringBuilder();
1252:
1253:                 hdr.append("feature_name=\"");
1254:                 hdr.append(option.value);
1255:                 hdr.append("\" success=\"1\"");
1256:
1257:                 response(hdr, null);
1258:         }
1259:
1260:         protected void dyingThread(ContextException ex)
1261:         {
1262:                 try
1263:                 {
1264:                         breakContext = ex.ctxt;
1265:                         breakpoint = new Breakpoint(ex.ctxt.location);
1266:                         status = DBGPStatus.STOPPING;
1267:                         statusReason = DBGPReason.EXCEPTION;
1268:                         errorResponse(DBGPErrorCode.EVALUATION_ERROR, ex.getMessage());
1269:
1270:                         run();
1271:
1272:                         breakContext = null;
1273:                         breakpoint = null;
1274:                         statusResponse(DBGPStatus.STOPPED, DBGPReason.EXCEPTION);
1275:                 } catch (Exception e)
1276:                 {
1277:                         errorResponse(DBGPErrorCode.INTERNAL_ERROR, e.getMessage());
1278:                 }
1279:         }
1280:
1281:         protected boolean processRun(DBGPCommand c) throws DBGPException
1282:         {
1283:                 checkArgs(c, 1, false);
1284:
1285:                 if (status == DBGPStatus.BREAK || status == DBGPStatus.STOPPING)
1286:                 {
1287:                         if (breakContext != null)
1288:                         {
1289:                                 breakContext.threadState.setBreaks(null, null, null);
1290:                                 status = DBGPStatus.RUNNING;
1291:                                 statusReason = DBGPReason.OK;
1292:                                 return false; // run means continue
1293:                         } else
1294:                         {
1295:                                 throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
1296:                         }
1297:                 }
1298:
1299:                 if (status == DBGPStatus.STARTING && expression == null)
1300:                 {
1301:                         status = DBGPStatus.RUNNING;
1302:                         statusReason = DBGPReason.OK;
1303:                         return false; // a run for a new thread, means continue
1304:                 }
1305:
1306:                 if (status != DBGPStatus.STARTING)
1307:                 {
1308:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
1309:                 }
1310:
1311:                 if (c.data != null) // data is in "expression"
1312:                 {
1313:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1314:                 }
1315:
1316:                 if (remoteControl != null)
1317:                 {
1318:                         try
1319:                         {
1320:                                 status = DBGPStatus.RUNNING;
1321:                                 statusReason = DBGPReason.OK;
1322:
1323:                                 final RemoteInterpreter remoteInterpreter = new RemoteInterpreter(interpreter, this);
1324:                                 Thread remoteThread = new Thread(new Runnable()
1325:                                 {
1326:
1327:                                         public void run()
1328:                                         {
1329:                                                 try
1330:                                                 {
1331:                                                         remoteControl.run(remoteInterpreter);
1332:                                                 } catch (Exception e)
1333:                                                 {
1334:                                                         status = DBGPStatus.STOPPED;
1335:                                                         statusReason = DBGPReason.ERROR;
1336:                                                         errorResponse(DBGPErrorCode.INTERNAL_ERROR, e.getMessage());
1337:                                                 }
1338:                                         }
1339:                                 });
1340:                                 remoteThread.setName("RemoteControl runner");
1341:                                 remoteThread.setDaemon(true);
1342:                                 remoteThread.start();
1343:                                 remoteInterpreter.processRemoteCalls();
1344:                                 // remoteControl.run(new RemoteInterpreter(interpreter, this));
1345:                                 stdout("Remote control completed");
1346:                                 statusResponse(DBGPStatus.STOPPED, DBGPReason.OK);
1347:                         } catch (Exception e)
1348:                         {
1349:                                 status = DBGPStatus.STOPPED;
1350:                                 statusReason = DBGPReason.ERROR;
1351:                                 errorResponse(DBGPErrorCode.INTERNAL_ERROR, e.getMessage());
1352:                         }
1353:
1354:                         return false; // Do not continue after remote session
1355:                 } else
1356:                 {
1357:                         try
1358:                         {
1359:                                 status = DBGPStatus.RUNNING;
1360:                                 statusReason = DBGPReason.OK;
1361:                                 theAnswer = interpreter.execute(expression, this);
1362:                                 stdout(expression + " = " + theAnswer.toString());
1363:                                 statusResponse(DBGPStatus.STOPPED, DBGPReason.OK);
1364:
1365:                         } catch (ContextException e)
1366:                         {
1367:                                 dyingThread(e);
1368:                         } catch (Exception e)
1369:                         {
1370:                                 status = DBGPStatus.STOPPED;
1371:                                 statusReason = DBGPReason.ERROR;
1372:                                 errorResponse(DBGPErrorCode.EVALUATION_ERROR, e.getMessage());
1373:                         }
1374:
1375:                         return true;
1376:                 }
1377:         }
1378:
1379:         protected boolean processEval(DBGPCommand c) throws DBGPException
1380:         {
1381:                 checkArgs(c, 1, true);
1382:
1383:                 if (status != DBGPStatus.BREAK && status != DBGPStatus.STOPPING
1384:                                 || breakpoint == null)
1385:                 {
1386:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
1387:                 }
1388:
1389:                 breaksSuspended = true;
1390:
1391:                 try
1392:                 {
1393:                         String exp = c.data; // Already base64 decoded by the parser
1394:                         interpreter.setDefaultName(breakpoint.location.getModule());
1395:                         theAnswer = interpreter.evaluate(exp, breakContext);
1396:                         StringBuilder property = propertyResponse(exp, exp, interpreter.getDefaultName(), theAnswer.toString());
1397:                         StringBuilder hdr = new StringBuilder("success=\"1\"");
1398:                         response(hdr, property);
1399:                 } catch (Exception e)
1400:                 {
1401:                         errorResponse(DBGPErrorCode.EVALUATION_ERROR, e.getMessage());
1402:                 } finally
1403:                 {
1404:                         breaksSuspended = false;
1405:                 }
1406:
1407:                 return true;
1408:         }
1409:
1410:         protected boolean processExpr(DBGPCommand c) throws DBGPException
1411:         {
1412:                 checkArgs(c, 1, true);
1413:
1414:                 if (status == DBGPStatus.BREAK || status == DBGPStatus.STOPPING)
1415:                 {
1416:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
1417:                 }
1418:
1419:                 try
1420:                 {
1421:                         status = DBGPStatus.RUNNING;
1422:                         statusReason = DBGPReason.OK;
1423:                         String exp = c.data; // Already base64 decoded by the parser
1424:                         theAnswer = interpreter.execute(exp, this);
1425:                         StringBuilder property = propertyResponse(exp, exp, interpreter.getDefaultName(), theAnswer.toString());
1426:                         StringBuilder hdr = new StringBuilder("success=\"1\"");
1427:                         status = DBGPStatus.STOPPED;
1428:                         statusReason = DBGPReason.OK;
1429:                         response(hdr, property);
1430:                 } catch (ContextException e)
1431:                 {
1432:                         dyingThread(e);
1433:                 } catch (Exception e)
1434:                 {
1435:                         status = DBGPStatus.STOPPED;
1436:                         statusReason = DBGPReason.ERROR;
1437:                         errorResponse(DBGPErrorCode.EVALUATION_ERROR, e.getMessage());
1438:                 }
1439:
1440:                 return true;
1441:         }
1442:
1443:         protected void processStepInto(DBGPCommand c) throws DBGPException
1444:         {
1445:                 checkArgs(c, 1, false);
1446:
1447:                 if (breakpoint != null)
1448:                 {
1449:                         breakContext.threadState.setBreaks(breakpoint.location, null, null);
1450:                 }
1451:
1452:                 status = DBGPStatus.RUNNING;
1453:                 statusReason = DBGPReason.OK;
1454:         }
1455:
1456:         protected void processStepOver(DBGPCommand c) throws DBGPException
1457:         {
1458:                 checkArgs(c, 1, false);
1459:
1460:                 if (breakpoint != null)
1461:                 {
1462:                         breakContext.threadState.setBreaks(breakpoint.location, breakContext.getRoot(), null);
1463:                 }
1464:
1465:                 status = DBGPStatus.RUNNING;
1466:                 statusReason = DBGPReason.OK;
1467:         }
1468:
1469:         protected void processStepOut(DBGPCommand c) throws DBGPException
1470:         {
1471:                 checkArgs(c, 1, false);
1472:
1473:                 if (breakpoint != null)
1474:                 {
1475:                         breakContext.threadState.setBreaks(breakpoint.location, null, breakContext.getRoot().outer);
1476:                 }
1477:
1478:                 status = DBGPStatus.RUNNING;
1479:                 statusReason = DBGPReason.OK;
1480:         }
1481:
1482:         protected void processStop(DBGPCommand c) throws DBGPException, IOException
1483:         {
1484:                 checkArgs(c, 1, false);
1485:                 statusResponse(DBGPStatus.STOPPED, DBGPReason.OK);
1486:
1487:                 if (isLastConnectedReader())
1488:                 {
1489:                         handleExit();
1490:                 } else
1491:                 {
1492:                         removeThisReader();
1493:                 }
1494:         }
1495:
1496:         protected void handleExit()
1497:         {
1498:                 try
1499:                 {
1500:
1501:                         if (socket != null)
1502:                         {
1503:                                 socket.close();
1504:                         }
1505:                 } catch (Exception e)
1506:                 {
1507:
1508:                 }
1509:
1510:                 System.exit(0);
1511:         }
1512:
1513:         private boolean isLastConnectedReader()
1514:         {
1515:                 synchronized (connectecReaders)
1516:                 {
1517:                         return connectecReaders.size() == 1;
1518:                 }
1519:         }
1520:
1521:         private void addThisReader()
1522:         {
1523:                 synchronized (connectecReaders)
1524:                 {
1525:                         connectecReaders.add(this);
1526:                 }
1527:         }
1528:
1529:         private void removeThisReader()
1530:         {
1531:                 synchronized (connectecReaders)
1532:                 {
1533:                         connectecReaders.remove(this);
1534:                 }
1535:         }
1536:
1537:         protected void breakpointGet(DBGPCommand c) throws DBGPException,
1538:                         IOException
1539:         {
1540:                 checkArgs(c, 2, false);
1541:
1542:                 DBGPOption option = c.getOption(DBGPOptionType.D);
1543:
1544:                 if (option == null)
1545:                 {
1546:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1547:                 }
1548:
1549:                 Breakpoint bp = interpreter.breakpoints.get(Integer.parseInt(option.value));
1550:
1551:                 if (bp == null)
1552:                 {
1553:                         throw new DBGPException(DBGPErrorCode.INVALID_BREAKPOINT, c.toString());
1554:                 }
1555:
1556:                 response(null, breakpointResponse(bp));
1557:         }
1558:
1559:         protected void breakpointSet(DBGPCommand c) throws DBGPException,
1560:                         IOException, URISyntaxException
1561:         {
1562:                 DBGPOption option = c.getOption(DBGPOptionType.T);
1563:
1564:                 if (option == null)
1565:                 {
1566:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1567:                 }
1568:
1569:                 DBGPBreakpointType type = DBGPBreakpointType.lookup(option.value);
1570:
1571:                 if (type == null)
1572:                 {
1573:                         throw new DBGPException(DBGPErrorCode.BREAKPOINT_TYPE_UNSUPPORTED, option.value);
1574:                 }
1575:
1576:                 option = c.getOption(DBGPOptionType.F);
1577:                 File filename = null;
1578:
1579:                 if (option != null)
1580:                 {
1581:                         filename = new File(new URI(option.value));
1582:                 } else
1583:                 {
1584:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1585:                 }
1586:
1587:                 option = c.getOption(DBGPOptionType.N);
1588:                 int lineno = 0;
1589:
1590:                 if (option != null)
1591:                 {
1592:                         lineno = Integer.parseInt(option.value);
1593:                 }
1594:
1595:                 String condition = null;
1596:
1597:                 if (c.data != null)
1598:                 {
1599:                         condition = c.data;
1600:                 } else
1601:                 {
1602:                         DBGPOption cond = c.getOption(DBGPOptionType.O);
1603:                         DBGPOption hits = c.getOption(DBGPOptionType.H);
1604:
1605:                         if (cond != null || hits != null)
1606:                         {
1607:                                 String cs = cond == null ? ">=" : cond.value;
1608:                                 String hs = hits == null ? "0" : hits.value;
1609:
1610:                                 if (hs.equals("0"))
1611:                                 {
1612:                                         condition = "= 0"; // impossible (disabled)
1613:                                 } else if (cs.equals("=="))
1614:                                 {
1615:                                         condition = "= " + hs;
1616:                                 } else if (cs.equals(">="))
1617:                                 {
1618:                                         condition = ">= " + hs;
1619:                                 } else if (cs.equals("%"))
1620:                                 {
1621:                                         condition = "mod " + hs;
1622:                                 } else
1623:                                 {
1624:                                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1625:                                 }
1626:                         }
1627:                 }
1628:
1629:                 Breakpoint bp = null;
1630:                 PStm stmt = interpreter.findStatement(filename, lineno);
1631:
1632:                 if (stmt == null)
1633:                 {
1634:                         PExp exp = interpreter.findExpression(filename, lineno);
1635:
1636:                         if (exp == null)
1637:                         {
1638:                                 throw new DBGPException(DBGPErrorCode.CANT_SET_BREAKPOINT, filename
1639:                                                 + ":" + lineno);
1640:                         } else
1641:                         {
1642:                                 try
1643:                                 {
1644:                                         if (BreakpointManager.getBreakpoint(exp).number != 0)
1645:                                         {
1646:                                                 // Multiple threads set BPs multiple times, so...
1647:                                                 bp = BreakpointManager.getBreakpoint(exp); // Re-use the existing one
1648:                                         } else
1649:                                         {
1650:                                                 bp = interpreter.setBreakpoint(exp, condition);
1651:                                         }
1652:                                 } catch (ParserException e)
1653:                                 {
1654:                                         throw new DBGPException(DBGPErrorCode.CANT_SET_BREAKPOINT, filename
1655:                                                         + ":" + lineno + ", " + e.getMessage());
1656:                                 } catch (LexException e)
1657:                                 {
1658:                                         throw new DBGPException(DBGPErrorCode.CANT_SET_BREAKPOINT, filename
1659:                                                         + ":" + lineno + ", " + e.getMessage());
1660:                                 }
1661:                         }
1662:                 } else
1663:                 {
1664:                         try
1665:                         {
1666:                                 if (BreakpointManager.getBreakpoint(stmt).number != 0)
1667:                                 {
1668:                                         // Multiple threads set BPs multiple times, so...
1669:                                         bp = BreakpointManager.getBreakpoint(stmt); // Re-use the existing one
1670:                                 } else
1671:                                 {
1672:                                         bp = interpreter.setBreakpoint(stmt, condition);
1673:                                 }
1674:                         } catch (ParserException e)
1675:                         {
1676:                                 throw new DBGPException(DBGPErrorCode.CANT_SET_BREAKPOINT, filename
1677:                                                 + ":" + lineno + ", " + e.getMessage());
1678:                         } catch (LexException e)
1679:                         {
1680:                                 throw new DBGPException(DBGPErrorCode.CANT_SET_BREAKPOINT, filename
1681:                                                 + ":" + lineno + ", " + e.getMessage());
1682:                         }
1683:                 }
1684:
1685:                 option = c.getOption(DBGPOptionType.S);
1686:
1687:                 if (option != null)
1688:                 {
1689:                         if (!option.value.equalsIgnoreCase("enabled"))
1690:                         {
1691:                                 bp.setEnabled(false);
1692:                         }
1693:                 }
1694:
1695:                 StringBuilder hdr = new StringBuilder("state=\""
1696:                                 + (bp.isEnabled() ? "enabled" : "disabled") + "\" id=\""
1697:                                 + bp.number + "\"");
1698:                 response(hdr, null);
1699:         }
1700:
1701:         protected void breakpointUpdate(DBGPCommand c) throws DBGPException,
1702:                         IOException
1703:         {
1704:                 checkArgs(c, 4, false);
1705:
1706:                 DBGPOption option = c.getOption(DBGPOptionType.D);
1707:
1708:                 if (option == null)
1709:                 {
1710:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1711:                 }
1712:
1713:                 Breakpoint bp = interpreter.breakpoints.get(Integer.parseInt(option.value));
1714:
1715:                 if (bp == null)
1716:                 {
1717:                         throw new DBGPException(DBGPErrorCode.INVALID_BREAKPOINT, c.toString());
1718:                 }
1719:
1720:                 option = c.getOption(DBGPOptionType.S);
1721:
1722:                 if (option == null)
1723:                 {
1724:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1725:                 }
1726:
1727:                 if (option.value.equalsIgnoreCase("disabled"))
1728:                 {
1729:                         bp.setEnabled(false);
1730:                         response(null, null);
1731:                         return;
1732:                 }
1733:
1734:                 if (option.value.equalsIgnoreCase("enabled"))
1735:                 {
1736:                         bp.setEnabled(true);
1737:                         response(null, null);
1738:                         return;
1739:                 }
1740:
1741:                 throw new DBGPException(DBGPErrorCode.UNIMPLEMENTED, c.toString());
1742:         }
1743:
1744:         protected void breakpointRemove(DBGPCommand c) throws DBGPException,
1745:                         IOException
1746:         {
1747:                 checkArgs(c, 2, false);
1748:
1749:                 DBGPOption option = c.getOption(DBGPOptionType.D);
1750:
1751:                 if (option == null)
1752:                 {
1753:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1754:                 }
1755:
1756:                 if (interpreter.clearBreakpoint(Integer.parseInt(option.value)) == null)
1757:                 {
1758:                         // Multiple threads remove BPs multiple times
1759:                         // throw new DBGPException(DBGPErrorCode.INVALID_BREAKPOINT, c.toString());
1760:                 }
1761:
1762:                 response(null, null);
1763:         }
1764:
1765:         protected void breakpointList(DBGPCommand c) throws IOException,
1766:                         DBGPException
1767:         {
1768:                 checkArgs(c, 1, false);
1769:                 StringBuilder bps = new StringBuilder();
1770:
1771:                 for (Integer key : interpreter.breakpoints.keySet())
1772:                 {
1773:                         Breakpoint bp = interpreter.breakpoints.get(key);
1774:                         bps.append(breakpointResponse(bp));
1775:                 }
1776:
1777:                 response(null, bps);
1778:         }
1779:
1780:         protected void stackDepth(DBGPCommand c) throws DBGPException, IOException
1781:         {
1782:                 checkArgs(c, 1, false);
1783:
1784:                 if (status != DBGPStatus.BREAK && status != DBGPStatus.STOPPING)
1785:                 {
1786:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
1787:                 }
1788:
1789:                 StringBuilder sb = new StringBuilder();
1790:                 sb.append(breakContext.getDepth());
1791:
1792:                 response(null, sb);
1793:         }
1794:
1795:         protected void stackGet(DBGPCommand c) throws DBGPException, IOException
1796:         {
1797:                 checkArgs(c, 1, false);
1798:
1799:                 if (status != DBGPStatus.BREAK && status != DBGPStatus.STOPPING
1800:                                 || breakpoint == null)
1801:                 {
1802:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
1803:                 }
1804:
1805:                 DBGPOption option = c.getOption(DBGPOptionType.D);
1806:                 int depth = -1;
1807:
1808:                 if (option != null)
1809:                 {
1810:                         depth = Integer.parseInt(option.value); // 0 to n-1
1811:                 }
1812:
1813:                 // We omit the last frame, as this is unhelpful (globals),
1814:
1815:                 int actualDepth = breakContext.getDepth() - 1;
1816:
1817:                 if (depth >= actualDepth)
1818:                 {
1819:                         throw new DBGPException(DBGPErrorCode.INVALID_STACK_DEPTH, c.toString());
1820:                 }
1821:
1822:                 if (depth == 0)
1823:                 {
1824:                         response(null, stackResponse(breakpoint.location, 0));
1825:                 } else if (depth > 0)
1826:                 {
1827:                         Context ctxt = breakContext.getFrame(depth);
1828:                         response(null, stackResponse(ctxt.location, depth));
1829:                 } else
1830:                 {
1831:                         // The location of a context is where it was called from, so
1832:                         // to build the stack locations, we take the location of the
1833:                         // level above, and the first level is the BP's location,
1834:                         // assuming we have one which is different to the ctxt location.
1835:
1836:                         StringBuilder sb = new StringBuilder();
1837:                         int d = 0;
1838:
1839:                         if (!breakpoint.location.equals(breakContext.location)) // BP is different
1840:                         {
1841:                                 sb.append(stackResponse(breakpoint.location, d++));
1842:                                 actualDepth--;
1843:                         }
1844:
1845:                         for (int f = 0; f < actualDepth; f++)
1846:                         {
1847:                                 Context ctxt = breakContext.getFrame(f);
1848:                                 sb.append(stackResponse(ctxt.location, d++));
1849:                         }
1850:
1851:                         response(null, sb);
1852:                 }
1853:         }
1854:
1855:         protected void contextNames(DBGPCommand c) throws DBGPException,
1856:                         IOException
1857:         {
1858:                 if (c.data != null)
1859:                 {
1860:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1861:                 }
1862:
1863:                 DBGPOption option = c.getOption(DBGPOptionType.D);
1864:
1865:                 if (c.options.size() > (option == null ? 1 : 2))
1866:                 {
1867:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
1868:                 }
1869:
1870:                 StringBuilder names = new StringBuilder();
1871:                 // String dialect = Settings.dialect == Dialect.VDM_SL ? "Module" : "Class";
1872:
1873:                 // names.append("<context name=\"Local\" id=\"0\"/>");
1874:                 // names.append("<context name=\"" + dialect + "\" id=\"1\"/>");
1875:                 // names.append("<context name=\"Global\" id=\"2\"/>");
1876:
1877:                 for (DBGPContextType type : DBGPContextType.values())
1878:                 {
1879:                         String name = type == DBGPContextType.CLASS
1880:                                         && Settings.dialect == Dialect.VDM_SL ? "Module"
1881:                                         : type.name();
1882:                         names.append("<context name=\"" + name + "\" id=\"" + type.code
1883:                                         + "\"/>");
1884:                 }
1885:
1886:                 response(null, names);
1887:         }
1888:
1889:         protected NameValuePairMap getContextValues(DBGPContextType context,
1890:                         int depth)
1891:         {
1892:                 NameValuePairMap vars = new NameValuePairMap();
1893:
1894:                 switch (context)
1895:                 {
1896:                         case LOCAL:
1897:                                 if (depth == 0)
1898:                                 {
1899:                                         vars.putAll(breakContext.getVisibleVariables());
1900:                                 } else
1901:                                 {
1902:                                         Context frame = breakContext.getFrame(depth - 1).outer;
1903:
1904:                                         if (frame != null)
1905:                                         {
1906:                                                 vars.putAll(frame.getVisibleVariables());
1907:                                         }
1908:                                 }
1909:
1910:                                 if (breakContext instanceof ObjectContext)
1911:                                 {
1912:                                         ObjectContext octxt = (ObjectContext) breakContext;
1913:                                         int line = breakpoint.location.getStartLine();
1914:                                         String opname = breakContext.guardOp == null ? ""
1915:                                                         : breakContext.guardOp.name.getName();
1916:
1917:                                         for (PDefinition d : octxt.self.type.getClassdef().getDefinitions())
1918:                                         {
1919:                                                 if (d instanceof APerSyncDefinition)
1920:                                                 {
1921:                                                         APerSyncDefinition pdef = (APerSyncDefinition) d;
1922:
1923:                                                         if (pdef.getOpname().getName().equals(opname)
1924:                                                                         || pdef.getLocation().getStartLine() == line
1925:                                                                         || octxt.assistantFactory.createPExpAssistant().findExpression(pdef.getGuard(), line) != null)
1926:                                                         {
1927:                                                                 for (PExp sub : octxt.assistantFactory.createPExpAssistant().getSubExpressions(pdef.getGuard()))
1928:                                                                 {
1929:                                                                         if (sub instanceof AHistoryExp)
1930:                                                                         {
1931:                                                                                 AHistoryExp hexp = (AHistoryExp) sub;
1932:
1933:                                                                                 try
1934:                                                                                 {
1935:                                                                                         Value v = hexp.apply(VdmRuntime.getExpressionEvaluator(), octxt);
1936:                                                                                         LexNameToken name = new LexNameToken(octxt.self.type.getName().getModule(), hexp.toString(), hexp.getLocation());
1937:                                                                                         vars.put(name, v);
1938:                                                                                 } catch (Throwable e)
1939:                                                                                 {
1940:                                                                                         // Ignore
1941:                                                                                 }
1942:
1943:                                                                         }
1944:                                                                 }
1945:                                                         }
1946:                                                 } else if (d instanceof AMutexSyncDefinition)
1947:                                                 {
1948:                                                         AMutexSyncDefinition mdef = (AMutexSyncDefinition) d;
1949:
1950:                                                         for (ILexNameToken mop : mdef.getOperations())
1951:                                                         {
1952:                                                                 if (mop.getName().equals(opname))
1953:                                                                 {
1954:                                                                         for (ILexNameToken op : mdef.getOperations())
1955:                                                                         {
1956:                                                                                 LexNameList ops = new LexNameList(op);// TODO: this needs to be checked when
1957:                                                                                                                                                                 // testing
1958:                                                                                 PExp hexp = AstFactory.newAHistoryExp(mdef.getLocation(), new LexToken(new LexLocation(), VDMToken.ACTIVE), ops);
1959:
1960:                                                                                 try
1961:                                                                                 {
1962:                                                                                         Value v = hexp.apply(VdmRuntime.getExpressionEvaluator(), octxt);
1963:                                                                                         LexNameToken name = new LexNameToken(octxt.self.type.getName().getModule(), hexp.toString(), mdef.getLocation());
1964:                                                                                         vars.put(name, v);
1965:                                                                                 } catch (Throwable e)
1966:                                                                                 {
1967:                                                                                         // Ignore
1968:                                                                                 }
1969:
1970:                                                                         }
1971:
1972:                                                                         break;
1973:                                                                 }
1974:                                                         }
1975:                                                 }
1976:                                         }
1977:                                 }
1978:                                 break;
1979:
1980:                         case CLASS: // Includes modules
1981:                                 Context root = breakContext.getFrame(depth);
1982:
1983:                                 if (root instanceof ObjectContext)
1984:                                 {
1985:                                         ObjectContext octxt = (ObjectContext) root;
1986:                                         vars.putAll(octxt.self.members);
1987:                                 } else if (root instanceof ClassContext)
1988:                                 {
1989:                                         ClassContext cctxt = (ClassContext) root;
1990:                                         vars.putAll(cctxt.assistantFactory.createSClassDefinitionAssistant().getStatics(cctxt.classdef));
1991:                                 } else if (root instanceof StateContext)
1992:                                 {
1993:                                         StateContext sctxt = (StateContext) root;
1994:
1995:                                         if (sctxt.stateCtxt != null)
1996:                                         {
1997:                                                 vars.putAll(sctxt.stateCtxt);
1998:                                         }
1999:                                 }
2000:                                 break;
2001:
2002:                         case GLOBAL:
2003:                                 vars.putAll(interpreter.initialContext);
2004:                                 break;
2005:                 }
2006:
2007:                 return vars;
2008:         }
2009:
2010:         protected void contextGet(DBGPCommand c) throws DBGPException, IOException
2011:         {
2012:                 if (c.data != null || c.options.size() > 3)
2013:                 {
2014:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
2015:                 }
2016:
2017:                 if (status != DBGPStatus.BREAK && status != DBGPStatus.STOPPING)
2018:                 {
2019:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
2020:                 }
2021:
2022:                 DBGPOption option = c.getOption(DBGPOptionType.C);
2023:                 int type = 0;
2024:
2025:                 if (option != null)
2026:                 {
2027:                         type = Integer.parseInt(option.value);
2028:                 }
2029:
2030:                 DBGPContextType context = DBGPContextType.lookup(type);
2031:
2032:                 option = c.getOption(DBGPOptionType.D);
2033:                 int depth = 0;
2034:
2035:                 if (option != null)
2036:                 {
2037:                         depth = Integer.parseInt(option.value);
2038:                 }
2039:
2040:                 int actualDepth = breakContext.getDepth() - 1;
2041:
2042:                 if (depth >= actualDepth)
2043:                 {
2044:                         throw new DBGPException(DBGPErrorCode.INVALID_STACK_DEPTH, c.toString());
2045:                 }
2046:
2047:                 NameValuePairMap vars = getContextValues(context, depth);
2048:
2049:                 response(null, propertyResponse(vars, context));
2050:         }
2051:
2052:         protected void propertyGet(DBGPCommand c) throws DBGPException, IOException
2053:         {
2054:                 if (c.data != null || c.options.size() > 4)
2055:                 {
2056:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
2057:                 }
2058:
2059:                 if (status != DBGPStatus.BREAK && status != DBGPStatus.STOPPING)
2060:                 {
2061:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
2062:                 }
2063:
2064:                 DBGPOption option = c.getOption(DBGPOptionType.C);
2065:                 int type = 0;
2066:
2067:                 if (option != null)
2068:                 {
2069:                         type = Integer.parseInt(option.value);
2070:                 }
2071:
2072:                 DBGPContextType context = DBGPContextType.lookup(type);
2073:
2074:                 option = c.getOption(DBGPOptionType.D);
2075:                 int depth = -1;
2076:
2077:                 if (option != null)
2078:                 {
2079:                         depth = Integer.parseInt(option.value);
2080:                 }
2081:
2082:                 option = c.getOption(DBGPOptionType.N);
2083:
2084:                 if (option == null)
2085:                 {
2086:                         throw new DBGPException(DBGPErrorCode.CANT_GET_PROPERTY, c.toString());
2087:                 }
2088:
2089:                 LexTokenReader ltr = new LexTokenReader(option.value, Dialect.VDM_PP);
2090:                 LexToken token = null;
2091:
2092:                 try
2093:                 {
2094:                         token = ltr.nextToken();
2095:                 } catch (LexException e)
2096:                 {
2097:                         throw new DBGPException(DBGPErrorCode.CANT_GET_PROPERTY, option.value);
2098:                 } finally
2099:                 {
2100:                         ltr.close();
2101:                 }
2102:
2103:                 if (token.isNot(VDMToken.NAME))
2104:                 {
2105:                         throw new DBGPException(DBGPErrorCode.CANT_GET_PROPERTY, token.toString());
2106:                 }
2107:
2108:                 NameValuePairMap vars = getContextValues(context, depth);
2109:                 LexNameToken longname = (LexNameToken) token;
2110:                 Value value = vars.get(longname);
2111:
2112:                 if (value == null)
2113:                 {
2114:                         throw new DBGPException(DBGPErrorCode.CANT_GET_PROPERTY, longname.toString());
2115:                 }
2116:
2117:                 response(null, propertyResponse(longname, value, context));
2118:         }
2119:
2120:         protected void processSource(DBGPCommand c) throws DBGPException,
2121:                         IOException
2122:         {
2123:                 if (c.data != null || c.options.size() > 4)
2124:                 {
2125:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
2126:                 }
2127:
2128:                 DBGPOption option = c.getOption(DBGPOptionType.B);
2129:                 int begin = 1;
2130:
2131:                 if (option != null)
2132:                 {
2133:                         begin = Integer.parseInt(option.value);
2134:                 }
2135:
2136:                 option = c.getOption(DBGPOptionType.E);
2137:                 int end = 0;
2138:
2139:                 if (option != null)
2140:                 {
2141:                         end = Integer.parseInt(option.value);
2142:                 }
2143:
2144:                 option = c.getOption(DBGPOptionType.F);
2145:
2146:                 if (option == null)
2147:                 {
2148:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
2149:                 }
2150:
2151:                 File file = null;
2152:
2153:                 try
2154:                 {
2155:                         file = new File(new URI(option.value));
2156:                 } catch (URISyntaxException e)
2157:                 {
2158:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
2159:                 }
2160:
2161:                 SourceFile s = interpreter.getSourceFile(file);
2162:                 StringBuilder sb = new StringBuilder();
2163:
2164:                 if (end == 0)
2165:                 {
2166:                         end = s.getCount();
2167:                 }
2168:
2169:                 sb.append("<![CDATA[");
2170:
2171:                 for (int n = begin; n <= end; n++)
2172:                 {
2173:                         sb.append(quote(s.getLine(n)));
2174:                         sb.append("\n");
2175:                 }
2176:
2177:                 sb.append("]]>");
2178:                 response(null, sb);
2179:         }
2180:
2181:         protected void processStdout(DBGPCommand c) throws DBGPException,
2182:                         IOException
2183:         {
2184:                 checkArgs(c, 2, false);
2185:                 DBGPOption option = c.getOption(DBGPOptionType.C);
2186:
2187:                 if (option == null)
2188:                 {
2189:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
2190:                 }
2191:
2192:                 DBGPRedirect redirect = DBGPRedirect.lookup(option.value);
2193:                 Console.directStdout(this, redirect);
2194:
2195:                 response(new StringBuilder("success=\"1\""), null);
2196:         }
2197:
2198:         protected void processStderr(DBGPCommand c) throws DBGPException,
2199:                         IOException
2200:         {
2201:                 checkArgs(c, 2, false);
2202:                 DBGPOption option = c.getOption(DBGPOptionType.C);
2203:
2204:                 if (option == null)
2205:                 {
2206:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
2207:                 }
2208:
2209:                 DBGPRedirect redirect = DBGPRedirect.lookup(option.value);
2210:                 Console.directStderr(this, redirect);
2211:
2212:                 response(new StringBuilder("success=\"1\""), null);
2213:         }
2214:
2215:         public synchronized void stdout(String line) throws IOException
2216:         {
2217:                 StringBuilder sb = new StringBuilder("<stream type=\"stdout\"><![CDATA[");
2218:                 sb.append(Base64.encode(line.getBytes("UTF-8")));
2219:                 sb.append("]]></stream>\n");
2220:                 write(sb);
2221:         }
2222:
2223:         public synchronized void stderr(String line) throws IOException
2224:         {
2225:                 StringBuilder sb = new StringBuilder("<stream type=\"stderr\"><![CDATA[");
2226:                 sb.append(Base64.encode(line.getBytes("UTF-8")));
2227:                 sb.append("]]></stream>\n");
2228:                 write(sb);
2229:         }
2230:
2231:         protected void processOvertureCmd(DBGPCommand c) throws DBGPException,
2232:                         IOException, URISyntaxException, AnalysisException
2233:         {
2234:                 checkArgs(c, 2, false);
2235:                 DBGPOption option = c.getOption(DBGPOptionType.C);
2236:
2237:                 if (option == null)
2238:                 {
2239:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
2240:                 }
2241:
2242:                 if (option.value.equals("init"))
2243:                 {
2244:                         processInit(c);
2245:                 } else if (option.value.equals("create"))
2246:                 {
2247:                         processCreate(c);
2248:                 } else if (option.value.equals("currentline"))
2249:                 {
2250:                         processCurrentLine(c);
2251:                 } else if (option.value.equals("source"))
2252:                 {
2253:                         processCurrentSource(c);
2254:                 } else if (option.value.equals("coverage"))
2255:                 {
2256:                         processCoverage(c);
2257:                 } else if (option.value.equals("runtrace"))
2258:                 {
2259:                         processRuntrace(c);
2260:                 } else if (option.value.startsWith("latex"))
2261:                 {
2262:                         processLatex(c);
2263:                 } else if (option.value.equals("word"))
2264:                 {
2265:                         processWord(c);
2266:                 } else if (option.value.equals("pog"))
2267:                 {
2268:                         processPOG(c);
2269:                 } else if (option.value.equals("stack"))
2270:                 {
2271:                         processStack(c);
2272:                 } else if (option.value.equals("trace"))
2273:                 {
2274:                         processTrace(c);
2275:                 } else if (option.value.equals("list"))
2276:                 {
2277:                         processList();
2278:                 } else if (option.value.equals("files"))
2279:                 {
2280:                         processFiles();
2281:                 } else if (option.value.equals("classes"))
2282:                 {
2283:                         processClasses();
2284:                 } else if (option.value.equals("modules"))
2285:                 {
2286:                         processModules();
2287:                 } else if (option.value.equals("default"))
2288:                 {
2289:                         processDefault(c);
2290:                 } else if (option.value.equals("log"))
2291:                 {
2292:                         processLog(c);
2293:                 } else
2294:                 {
2295:                         throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
2296:                 }
2297:         }
2298:
2299:         protected void processInit(DBGPCommand c) throws IOException, DBGPException
2300:         {
2301:                 if (status == DBGPStatus.BREAK || status == DBGPStatus.STOPPING)
2302:                 {
2303:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
2304:                 }
2305:
2306:                 LexLocationUtils.clearLocations();
2307:                 interpreter.init(this);
2308:                 statusResponse(DBGPStatus.STOPPED, DBGPReason.OK);
2309:                 cdataResponse("Global context and test coverage initialized");
2310:         }
2311:
2312:         protected void processLog(DBGPCommand c) throws IOException
2313:         {
2314:                 StringBuilder out = new StringBuilder();
2315:
2316:                 try
2317:                 {
2318:                         if (c.data == null)
2319:                         {
2320:                                 if (RTLogger.getLogSize() > 0)
2321:                                 {
2322:                                         out.append("Flushing " + RTLogger.getLogSize()
2323:                                                         + " RT events\n");
2324:                                 }
2325:
2326:                                 RTLogger.setLogfile(RTTextLogger.class, null);
2327:                                 RTLogger.setLogfile(NextGenRTLogger.class, (File) null);
2328:                                 out.append("RT events now logged to the console");
2329:                         } else if (c.data.equals("off"))
2330:                         {
2331:                                 RTLogger.enable(false);
2332:                                 out.append("RT event logging disabled");
2333:                         } else
2334:                         {
2335:                                 RTLogger.setLogfile(RTTextLogger.class, new File(c.data));
2336:                                 out.append("RT events now logged to " + c.data);
2337:                         }
2338:                 } catch (FileNotFoundException e)
2339:                 {
2340:                         out.append("Cannot create RT event log: " + e.getMessage());
2341:                 }
2342:
2343:                 cdataResponse(out.toString());
2344:         }
2345:
2346:         protected void processCreate(DBGPCommand c) throws DBGPException
2347:         {
2348:                 if (!(interpreter instanceof ClassInterpreter))
2349:                 {
2350:                         throw new DBGPException(DBGPErrorCode.INTERNAL_ERROR, "Not available for VDM-SL");
2351:                 }
2352:
2353:                 try
2354:                 {
2355:                         int i = c.data.indexOf(' ');
2356:                         String var = c.data.substring(0, i);
2357:                         String exp = c.data.substring(i + 1);
2358:
2359:                         ((ClassInterpreter) interpreter).create(var, exp);
2360:                 } catch (Exception e)
2361:                 {
2362:                         throw new DBGPException(DBGPErrorCode.INTERNAL_ERROR, e.getMessage());
2363:                 }
2364:         }
2365:
2366:         protected void processStack(DBGPCommand c) throws IOException,
2367:                         DBGPException
2368:         {
2369:                 if (status != DBGPStatus.BREAK && status != DBGPStatus.STOPPING
2370:                                 || breakpoint == null)
2371:                 {
2372:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
2373:                 }
2374:
2375:                 OutputStream out = new ByteArrayOutputStream();
2376:                 PrintWriter pw = new PrintWriter(out);
2377:                 pw.println(breakpoint.stoppedAtString());
2378:                 breakContext.printStackTrace(pw, true);
2379:                 pw.close();
2380:                 cdataResponse(out.toString());
2381:         }
2382:
2383:         protected void processTrace(DBGPCommand c) throws DBGPException
2384:         {
2385:                 File file = null;
2386:                 int line = 0;
2387:                 String trace = null;
2388:
2389:                 try
2390:                 {
2391:                         int i = c.data.indexOf(' ');
2392:                         int j = c.data.indexOf(' ', i + 1);
2393:                         file = new File(new URI(c.data.substring(0, i)));
2394:                         line = Integer.parseInt(c.data.substring(i + 1, j));
2395:                         trace = c.data.substring(j + 1);
2396:
2397:                         if (trace.length() == 0)
2398:                         {
2399:                                 trace = null;
2400:                         }
2401:
2402:                         OutputStream out = new ByteArrayOutputStream();
2403:                         PrintWriter pw = new PrintWriter(out);
2404:
2405:                         PStm stmt = interpreter.findStatement(file, line);
2406:
2407:                         if (stmt == null)
2408:                         {
2409:                                 PExp exp = interpreter.findExpression(file, line);
2410:
2411:                                 if (exp == null)
2412:                                 {
2413:                                         throw new DBGPException(DBGPErrorCode.CANT_SET_BREAKPOINT, "No breakable expressions or statements at "
2414:                                                         + file + ":" + line);
2415:                                 } else
2416:                                 {
2417:                                         interpreter.clearBreakpoint(BreakpointManager.getBreakpoint(exp).number);
2418:                                         Breakpoint bp = interpreter.setTracepoint(exp, trace);
2419:                                         pw.println("Created " + bp);
2420:                                         pw.println(interpreter.getSourceLine(bp.location));
2421:                                 }
2422:                         } else
2423:                         {
2424:                                 interpreter.clearBreakpoint(BreakpointManager.getBreakpoint(stmt).number);
2425:                                 Breakpoint bp = interpreter.setTracepoint(stmt, trace);
2426:                                 pw.println("Created " + bp);
2427:                                 pw.println(interpreter.getSourceLine(bp.location));
2428:                         }
2429:
2430:                         pw.close();
2431:                         cdataResponse(out.toString());
2432:                 } catch (Exception e)
2433:                 {
2434:                         throw new DBGPException(DBGPErrorCode.CANT_SET_BREAKPOINT, e.getMessage());
2435:                 }
2436:         }
2437:
2438:         protected void processList() throws IOException
2439:         {
2440:                 Map<Integer, Breakpoint> map = interpreter.getBreakpoints();
2441:                 OutputStream out = new ByteArrayOutputStream();
2442:                 PrintWriter pw = new PrintWriter(out);
2443:
2444:                 for (Entry<Integer, Breakpoint> entry : map.entrySet())
2445:                 {
2446:                         Breakpoint bp = entry.getValue();
2447:                         pw.println(bp.toString());
2448:                         pw.println(interpreter.getSourceLine(bp.location));
2449:                 }
2450:
2451:                 pw.close();
2452:                 cdataResponse(out.toString());
2453:         }
2454:
2455:         protected void processFiles() throws IOException
2456:         {
2457:                 Set<File> filenames = interpreter.getSourceFiles();
2458:                 OutputStream out = new ByteArrayOutputStream();
2459:                 PrintWriter pw = new PrintWriter(out);
2460:
2461:                 for (File file : filenames)
2462:                 {
2463:                         pw.println(file.getPath());
2464:                 }
2465:
2466:                 pw.close();
2467:                 cdataResponse(out.toString());
2468:         }
2469:
2470:         protected void processClasses() throws IOException, DBGPException
2471:         {
2472:                 if (!(interpreter instanceof ClassInterpreter))
2473:                 {
2474:                         throw new DBGPException(DBGPErrorCode.INTERNAL_ERROR, "Not available for VDM-SL");
2475:                 }
2476:
2477:                 ClassInterpreter cinterpreter = (ClassInterpreter) interpreter;
2478:                 String def = cinterpreter.getDefaultName();
2479:                 ClassList classes = cinterpreter.getClasses();
2480:                 OutputStream out = new ByteArrayOutputStream();
2481:                 PrintWriter pw = new PrintWriter(out);
2482:
2483:                 for (SClassDefinition cls : classes)
2484:                 {
2485:                         if (cls.getName().getName().equals(def))
2486:                         {
2487:                                 pw.println(cls.getName().getName() + " (default)");
2488:                         } else
2489:                         {
2490:                                 pw.println(cls.getName().getName());
2491:                         }
2492:                 }
2493:
2494:                 pw.close();
2495:                 cdataResponse(out.toString());
2496:         }
2497:
2498:         protected void processModules() throws DBGPException, IOException
2499:         {
2500:                 if (!(interpreter instanceof ModuleInterpreter))
2501:                 {
2502:                         throw new DBGPException(DBGPErrorCode.INTERNAL_ERROR, "Only available for VDM-SL");
2503:                 }
2504:
2505:                 ModuleInterpreter minterpreter = (ModuleInterpreter) interpreter;
2506:                 String def = minterpreter.getDefaultName();
2507:                 List<AModuleModules> modules = minterpreter.getModules();
2508:                 OutputStream out = new ByteArrayOutputStream();
2509:                 PrintWriter pw = new PrintWriter(out);
2510:
2511:                 for (AModuleModules m : modules)
2512:                 {
2513:                         if (m.getName().getName().equals(def))
2514:                         {
2515:                                 pw.println(m.getName().getName() + " (default)");
2516:                         } else
2517:                         {
2518:                                 pw.println(m.getName().getName());
2519:                         }
2520:                 }
2521:
2522:                 pw.close();
2523:                 cdataResponse(out.toString());
2524:         }
2525:
2526:         protected void processDefault(DBGPCommand c) throws DBGPException
2527:         {
2528:                 try
2529:                 {
2530:                         interpreter.setDefaultName(c.data);
2531:                         cdataResponse("Default set to " + interpreter.getDefaultName());
2532:                 } catch (Exception e)
2533:                 {
2534:                         throw new DBGPException(DBGPErrorCode.INTERNAL_ERROR, e.getMessage());
2535:                 }
2536:         }
2537:
2538:         protected void processCoverage(DBGPCommand c) throws DBGPException,
2539:                         IOException, URISyntaxException
2540:         {
2541:                 if (status == DBGPStatus.BREAK)
2542:                 {
2543:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
2544:                 }
2545:
2546:                 File file = new File(new URI(c.data));
2547:                 SourceFile source = interpreter.getSourceFile(file);
2548:
2549:                 if (source == null)
2550:                 {
2551:                         cdataResponse(file + ": file not found");
2552:                 } else
2553:                 {
2554:                         OutputStream out = new ByteArrayOutputStream();
2555:                         PrintWriter pw = new PrintWriter(out);
2556:                         source.printCoverage(pw);
2557:                         pw.close();
2558:                         cdataResponse(out.toString());
2559:                 }
2560:         }
2561:
2562:         protected void processRuntrace(DBGPCommand c) throws DBGPException
2563:         {
2564:                 if (status == DBGPStatus.BREAK)
2565:                 {
2566:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
2567:                 }
2568:
2569:                 try
2570:                 {
2571:                         String[] parts = c.data.split("\\s+");
2572:                         int testNo = Integer.parseInt(parts[1]);
2573:                         boolean debug = Boolean.parseBoolean(parts[2]);
2574:
2575:                         ByteArrayOutputStream out = new ByteArrayOutputStream();
2576:                         PrintWriter pw = new PrintWriter(out);
2577:                         Interpreter.setTraceOutput(pw);
2578:                         interpreter.runtrace(parts[0], testNo, debug);
2579:                         pw.close();
2580:
2581:                         cdataResponse(out.toString());
2582:                 } catch (Exception e)
2583:                 {
2584:                         throw new DBGPException(DBGPErrorCode.INTERNAL_ERROR, e.getMessage());
2585:                 }
2586:         }
2587:
2588:         protected void processLatex(DBGPCommand c) throws DBGPException,
2589:                         IOException, URISyntaxException
2590:         {
2591:                 if (status == DBGPStatus.BREAK)
2592:                 {
2593:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
2594:                 }
2595:
2596:                 int i = c.data.indexOf(' ');
2597:                 File dir = new File(new URI(c.data.substring(0, i)));
2598:                 File file = new File(new URI(c.data.substring(i + 1)));
2599:
2600:                 SourceFile source = interpreter.getSourceFile(file);
2601:                 boolean headers = c.getOption(DBGPOptionType.C).value.equals("latexdoc");
2602:
2603:                 if (source == null)
2604:                 {
2605:                         cdataResponse(file + ": file not found");
2606:                 } else
2607:                 {
2608:                         File tex = new File(dir.getPath() + File.separator + file.getName()
2609:                                         + ".tex");
2610:                         PrintWriter pw = new PrintWriter(tex);
2611:                         CoverageUtil coverageUtil = new CoverageUtil(LexLocation.getAllLocations(),LexLocation.getNameSpans());
2612:                         new LatexSourceFile(source).printCoverage(pw, headers, coverageUtil);
2613:                         pw.close();
2614:                         cdataResponse("Latex coverage written to " + tex);
2615:                 }
2616:         }
2617:
2618:         private void processWord(DBGPCommand c) throws DBGPException, IOException,
2619:                         URISyntaxException
2620:         {
2621:                 if (status == DBGPStatus.BREAK)
2622:                 {
2623:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
2624:                 }
2625:
2626:                 int i = c.data.indexOf(' ');
2627:                 File dir = new File(new URI(c.data.substring(0, i)));
2628:                 File file = new File(new URI(c.data.substring(i + 1)));
2629:
2630:                 SourceFile source = interpreter.getSourceFile(file);
2631:
2632:                 if (source == null)
2633:                 {
2634:                         cdataResponse(file + ": file not found");
2635:                 } else
2636:                 {
2637:                         File html = new File(dir.getPath() + File.separator
2638:                                         + file.getName() + ".doc");
2639:                         PrintWriter pw = new PrintWriter(html);
2640:                         source.printWordCoverage(pw);
2641:                         pw.close();
2642:                         cdataResponse("Word HTML coverage written to " + html);
2643:                 }
2644:         }
2645:
2646:         protected void processCurrentLine(DBGPCommand c) throws DBGPException,
2647:                         IOException
2648:         {
2649:                 if (status != DBGPStatus.BREAK && status != DBGPStatus.STOPPING
2650:                                 || breakpoint == null)
2651:                 {
2652:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
2653:                 }
2654:
2655:                 OutputStream out = new ByteArrayOutputStream();
2656:                 PrintWriter pw = new PrintWriter(out);
2657:                 pw.println(breakpoint.stoppedAtString());
2658:                 pw.println(interpreter.getSourceLine(breakpoint.location.getFile(), breakpoint.location.getStartLine(), ": "));
2659:                 pw.close();
2660:                 cdataResponse(out.toString());
2661:         }
2662:
2663:         protected void processCurrentSource(DBGPCommand c) throws DBGPException,
2664:                         IOException
2665:         {
2666:                 if (status != DBGPStatus.BREAK && status != DBGPStatus.STOPPING
2667:                                 || breakpoint == null)
2668:                 {
2669:                         throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
2670:                 }
2671:
2672:                 File file = breakpoint.location.getFile();
2673:                 int current = breakpoint.location.getStartLine();
2674:
2675:                 int start = current - SOURCE_LINES;
2676:                 if (start < 1)
2677:                 {
2678:                         start = 1;
2679:                 }
2680:                 int end = start + SOURCE_LINES * 2 + 1;
2681:
2682:                 StringBuilder sb = new StringBuilder();
2683:
2684:                 for (int src = start; src < end; src++)
2685:                 {
2686:                         sb.append(interpreter.getSourceLine(file, src, src == current ? ":>>"
2687:                                         : ": "));
2688:                         sb.append("\n");
2689:                 }
2690:
2691:                 cdataResponse(sb.toString());
2692:         }
2693:
2694:         protected void processPOG(DBGPCommand c) throws IOException,
2695:                         AnalysisException
2696:         {
2697:                 IProofObligationList all = interpreter.getProofObligations();
2698:                 IProofObligationList list = null;
2699:
2700:                 if (c.data.equals("*"))
2701:                 {
2702:                         list = all;
2703:                 } else
2704:                 {
2705:                         list = new ProofObligationList();
2706:                         String name = c.data + "(";
2707:
2708:                         for (IProofObligation po : all)
2709:                         {
2710:                                 if (po.getName().indexOf(name) >= 0)
2711:                                 {
2712:                                         list.add(po);
2713:                                 }
2714:                         }
2715:                 }
2716:
2717:                 if (list.isEmpty())
2718:                 {
2719:                         cdataResponse("No proof obligations generated");
2720:                 } else
2721:                 {
2722:                         StringBuilder sb = new StringBuilder();
2723:                         sb.append("Generated ");
2724:                         sb.append(plural(list.size(), "proof obligation", "s"));
2725:                         sb.append(":\n");
2726:                         sb.append(list);
2727:                         cdataResponse(sb.toString());
2728:                 }
2729:         }
2730:
2731:         protected String plural(int n, String s, String pl)
2732:         {
2733:                 return n + " " + (n != 1 ? s + pl : s);
2734:         }
2735:
2736:         protected static void writeCoverage(Interpreter interpreter, File coverage)
2737:                         throws IOException
2738:         {
2739:                 for (File f : interpreter.getSourceFiles())
2740:                 {
2741:                         SourceFile source = interpreter.getSourceFile(f);
2742:
2743:                         File data = new File(coverage.getPath() + File.separator
2744:                                         + f.getName() + ".cov");
2745:                         PrintWriter pw = new PrintWriter(data);
2746:                         source.writeCoverage(pw);
2747:                         pw.close();
2748:                 }
2749:         }
2750: }