diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index 2de1b1864..b02f7730b 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -39,6 +39,7 @@ import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.ast.lex.LexBooleanToken; import com.fujitsu.vdmj.in.INNode; +import com.fujitsu.vdmj.in.annotations.INAnnotation; import com.fujitsu.vdmj.in.definitions.INClassDefinition; import com.fujitsu.vdmj.in.expressions.INBooleanLiteralExpression; import com.fujitsu.vdmj.in.expressions.INExpression; @@ -456,6 +457,11 @@ else if (results.provedBy != null) do { ictxt.next(); + + // Suspend annotation execution by the interpreter, because the + // expressions and statements in the PO can invoke them. + INAnnotation.suspend(true); + execResult = poexp.eval(ictxt); } while (ictxt.hasNext() && execResult.boolValue(ctxt)); @@ -472,6 +478,10 @@ else if (results.provedBy != null) exception = e; } } + finally + { + INAnnotation.suspend(false); + } long after = System.currentTimeMillis() + results.duration; diff --git a/lsp/src/main/java/workspace/LSPXWorkspaceManager.java b/lsp/src/main/java/workspace/LSPXWorkspaceManager.java index bb99c96fb..c3f092108 100644 --- a/lsp/src/main/java/workspace/LSPXWorkspaceManager.java +++ b/lsp/src/main/java/workspace/LSPXWorkspaceManager.java @@ -121,7 +121,6 @@ public void enablePlugins() throws Exception Method factory = clazz.getMethod("factory", Dialect.class); AnalysisPlugin instance = (AnalysisPlugin)factory.invoke(null, Settings.dialect); registry.registerPlugin(instance); - messagehub.addPlugin(instance); Diag.info("Registered LSPX plugin %s", plugin); } catch (NoSuchMethodException e) // Try default constructor @@ -137,7 +136,6 @@ public void enablePlugins() throws Exception Constructor ctor = clazz.getConstructor(); AnalysisPlugin instance = (AnalysisPlugin) ctor.newInstance(); registry.registerPlugin(instance); - messagehub.addPlugin(instance); Diag.info("Registered LSPX plugin %s", plugin); } catch (Throwable th) diff --git a/lsp/src/main/java/workspace/MessageHub.java b/lsp/src/main/java/workspace/MessageHub.java index 8028168f4..df27b955d 100644 --- a/lsp/src/main/java/workspace/MessageHub.java +++ b/lsp/src/main/java/workspace/MessageHub.java @@ -78,20 +78,6 @@ public static void reset() } } - /** - * This is used by the LSPX workspace manager to add new lspx.plugins. - */ - public synchronized void addPlugin(AnalysisPlugin plugin) - { - for (File file: messageMap.keySet()) - { - Map> pmap = messageMap.get(file); - pmap.put(plugin.getName(), new HashSet()); - } - - Diag.info("Added plugin %s to MessageHub", plugin.getName()); - } - /** * This is used by the workspace manager to populate a blank plugin map for a * new file. diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index f7871e85f..b5ed49862 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -25,14 +25,23 @@ package workspace.plugins; import java.io.File; +import java.io.IOException; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import java.util.Vector; import com.fujitsu.vdmj.lex.Dialect; import com.fujitsu.vdmj.mapper.Mappable; +import com.fujitsu.vdmj.messages.VDMMessage; +import com.fujitsu.vdmj.messages.VDMWarning; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.tc.lex.TCNameToken; import json.JSONArray; import json.JSONObject; +import lsp.LSPServer; import lsp.Utils; import rpc.RPCMessageList; import rpc.RPCRequest; @@ -151,9 +160,12 @@ protected JSONArray splitPO(String value) public JSONArray getObligations(File file) { ProofObligationList poGeneratedList = getProofObligations(); - poGeneratedList.renumber(); JSONArray results = new JSONArray(); + messagehub.clearPluginMessages(this); + List messages = new Vector(); + Set errFiles = new HashSet(); + for (ProofObligation po: poGeneratedList) { if (file != null) @@ -183,16 +195,69 @@ else if (file.isDirectory()) name.add(part); } - results.add( - new JSONObject( + JSONObject json = new JSONObject( "id", Long.valueOf(po.number), "kind", po.kind.toString(), "name", name, "location", Utils.lexLocationToLocation(po.location), "source", splitPO(po.value), - "status", po.status.toString())); + "status", po.status.toString()); + + if (!po.counterexample.isEmpty()) + { + JSONObject values = new JSONObject(); + + for (TCNameToken vname: po.counterexample.keySet()) + { + values.put(vname.getName(), po.counterexample.get(vname).toString()); + } + + json.put("counterexample", values); + + StringBuilder sb = new StringBuilder(); + sb.append("PO #"); + sb.append(po.number); + sb.append(" counterexample: "); + String sep = ""; + + for (TCNameToken vname: po.counterexample.keySet()) + { + sb.append(sep); + sb.append(vname.getName()); + sb.append(" = "); + sb.append(po.counterexample.get(vname)); + sep = ", "; + } + + messages.add(new VDMWarning(9000, sb.toString(), po.location)); + errFiles.add(po.location.file); + } + + if (po.countermessage != null) + { + json.put("message", "PO #" + po.number + ": " + po.countermessage); + messages.add(new VDMWarning(9001, po.countermessage, po.location)); + errFiles.add(po.location.file); + } + + results.add(json); + } + + messagehub.addPluginMessages(this, messages); + RPCMessageList errs = messagehub.getDiagnosticResponses(errFiles); + + for (JSONObject err: errs) + { + try + { + LSPServer.getInstance().writeMessage(err); + } + catch (IOException e) + { + Diag.error(e); + } } - return results; + return results; // Just POG display results } } diff --git a/lsp/src/main/scripts/lsp.sh b/lsp/src/main/scripts/lsp.sh index 8723272f0..a6386804b 100755 --- a/lsp/src/main/scripts/lsp.sh +++ b/lsp/src/main/scripts/lsp.sh @@ -54,8 +54,9 @@ VDMJ_JAR=$MAVENREPO/vdmj/${VERSION}/vdmj-${VERSION}.jar ANNOTATIONS_JAR=$MAVENREPO/annotations/${VERSION}/annotations-${VERSION}.jar LSP_JAR=$MAVENREPO/lsp/${VERSION}/lsp-${VERSION}.jar STDLIB_JAR=$MAVENREPO/stdlib/${VERSION}/stdlib-${VERSION}.jar +QUICKCHECK_JAR=$MAVENREPO/quickcheck/${VERSION}/quickcheck-${VERSION}.jar exec java ${JAVA64_VMOPTS} \ - -cp $VDMJ_JAR:$ANNOTATIONS_JAR:$LSP_JAR:$STDLIB_JAR \ + -cp $VDMJ_JAR:$ANNOTATIONS_JAR:$LSP_JAR:$STDLIB_JAR:$QUICKCHECK_JAR \ lsp.LSPServerDebug $DIALECT -lsp 8000 -dap 8001 diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java index b33242fe9..c46c02b5b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java @@ -54,9 +54,9 @@ public String toString() public Value eval(Context ctxt) { breakpoint.check(location, ctxt); - annotation.inBefore(this, ctxt); + if (!INAnnotation.suspended) annotation.inBefore(this, ctxt); Value rv = expression.eval(ctxt); - annotation.inAfter(this, rv, ctxt); + if (!INAnnotation.suspended) annotation.inAfter(this, rv, ctxt); return rv; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java index 1d29492b4..afdf748f9 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java @@ -54,9 +54,9 @@ public String toString() public Value eval(Context ctxt) { breakpoint.check(location, ctxt); - annotation.inBefore(this, ctxt); + if (!INAnnotation.suspended) annotation.inBefore(this, ctxt); Value rv = statement.eval(ctxt); - annotation.inAfter(this, rv, ctxt); + if (!INAnnotation.suspended) annotation.inAfter(this, rv, ctxt); return rv; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotation.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotation.java index f35f0c0a3..4e9fb3a1c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotation.java @@ -49,7 +49,9 @@ public abstract class INAnnotation extends INNode implements MappingOptional public final INExpressionList args; private static final Set> declared = new HashSet>(); - private static final List instances = new Vector(); + private static final List instances = new Vector(); + + public static boolean suspended = false; public INAnnotation(TCIdentifierToken name, INExpressionList args) { @@ -65,6 +67,11 @@ public static void reset() declared.clear(); instances.clear(); } + + public static void suspend(boolean flag) + { + suspended = flag; // Used in INAnnotatedExpression and Statement + } public static void init(Context ctxt) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java index 904fa2c6c..74d25e034 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java @@ -35,7 +35,7 @@ public class PogCommand extends AnalysisCommand { - private final static String USAGE = "Usage: pog [ | | ]"; + private final static String USAGE = "Usage: pog [ | | ]"; public PogCommand(String line) { @@ -58,9 +58,9 @@ public String run(String line) { list = all; } - else + else if (argv.length == 2) { - String match = line.substring(line.indexOf(' ') + 1); + String match = argv[1]; list = new ProofObligationList(); for (ProofObligation obligation: all) @@ -73,6 +73,10 @@ public String run(String line) } } } + else + { + return USAGE; + } if (list.isEmpty()) { @@ -104,6 +108,6 @@ public String run(String line) public static void help() { - println("pog [] - generate proof obligations"); + println("pog [ | | ] - generate proof obligations"); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java index c5d1a3fcf..72da7110c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java @@ -43,12 +43,13 @@ public POAnnotatedExpression(LexLocation location, POAnnotation annotation, POEx super(location); this.annotation = (annotation != null) ? annotation : new PONoAnnotation(); this.expression = expression; + setExptype(expression.getExptype()); } @Override public String toString() { - return "/* " + annotation + " */ " + expression; + return expression.toString(); // Don't include annotation in PO sources } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java index add72d1d3..07f9f019a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java @@ -43,12 +43,13 @@ public POAnnotatedStatement(LexLocation location, POAnnotation annotation, POSta super(location); this.annotation = (annotation != null) ? annotation : new PONoAnnotation(); this.statement = statement; + setStmttype(statement.getStmttype()); } @Override public String toString() { - return "/* " + annotation + " */ " + statement; + return statement.toString(); // Don't include annotation in PO source } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java index 93d637ad5..3057a6193 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -174,10 +174,12 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env LexTokenReader ltr = new LexTokenReader(obligation.getValue(), Settings.dialect); ExpressionReader reader = new ExpressionReader(ltr); reader.setCurrentModule(mname); - boolean old = Properties.parser_maximal_types; - Properties.parser_maximal_types = true; // For parse of PO on inv_T2 + + boolean oldmax = Properties.parser_maximal_types; + Properties.parser_maximal_types = true; // For parse of PO on inv_T(T!) ASTExpression ast = reader.readExpression(); - Properties.parser_maximal_types = old; + Properties.parser_maximal_types = oldmax; + LexToken end = ltr.getLast(); if (!end.is(Token.EOF)) @@ -213,7 +215,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env iter.remove(); obligation.status = POStatus.FAILED; obligation.isCheckable = false; - obligation.countermessage = "Error: Missing measure function"; + obligation.countermessage = "PO #" + obligation.number + ": Missing measure function"; } break;