Feature/agnosis pull request

.vscode/settings.json

@@ -1,5 +1,7 @@
 {
  "silver.jvmArgs": "-Xmx10G -Xss40M",
  "java.jdt.ls.vmargs": "-XX:+UseParallelGC -XX:GCTimeRatio=4 -XX:AdaptiveSizePolicyWeight=90 -Dsun.zip.disableMemoryMapping=true -Xmx2G -Xms100m -Xlog:disable",
- "silver.compilerJar": "jars/silver.compiler.composed.Default.jar"
+ "silver.compilerJar": "jars/silver.compiler.composed.Default.jar",
+ "java.compile.nullAnalysis.mode": "automatic",
+ "liveServer.settings.port": 5501
 }

grammars/silver/core/Debug.sv

@@ -0,0 +1,12 @@
+grammar silver:core;
+
+@{-
+ - Launch an interactive debug session to explore a tree.
+ -}
+function debug
+Decorated a with i ::= tree::Decorated a with i
+{
+ return error("foreign function");
+} foreign {
+ "java" : return "common.Debug.runDebug(%tree%)";
+}

grammars/silver/testing/bin/TestSpecLang.sv

@@ -91,7 +91,7 @@ ts::Run ::= 'test' 'suite' jar::Jar_t
  local testSuiteResults :: IOVal<Integer> 
  = systemT ("cd " ++ ts.testFileDir ++ ";" ++
  "rm -f " ++ ts.testFileName ++ ".output ; " ++ 
- " java -Xss6M -jar " ++ jar.lexeme ++
+ " java -Xss30M -jar " ++ jar.lexeme ++
  " >& " ++ ts.testFileName ++ ".output" ,
  msgBefore ) ;
 

language-server/launcher/.settings/org.eclipse.jdt.core.prefs

@@ -33,7 +33,7 @@ org.eclipse.jdt.core.compiler.annotation.inheritNullAnnotations=disabled
 org.eclipse.jdt.core.compiler.annotation.missingNonNullByDefaultAnnotation=ignore
 org.eclipse.jdt.core.compiler.annotation.nonnull=javax.annotation.Nonnull
 org.eclipse.jdt.core.compiler.annotation.nonnull.secondary=
-org.eclipse.jdt.core.compiler.annotation.nonnullbydefault=org.eclipse.jdt.annotation.NonNullByDefault
+org.eclipse.jdt.core.compiler.annotation.nonnullbydefault=javax.annotation.ParametersAreNonnullByDefault
 org.eclipse.jdt.core.compiler.annotation.nonnullbydefault.secondary=
 org.eclipse.jdt.core.compiler.annotation.nullable=javax.annotation.Nullable
 org.eclipse.jdt.core.compiler.annotation.nullable.secondary=
@@ -110,7 +110,7 @@ org.eclipse.jdt.core.compiler.problem.nonnullTypeVariableFromLegacyInvocation=wa
 org.eclipse.jdt.core.compiler.problem.nullAnnotationInferenceConflict=warning
 org.eclipse.jdt.core.compiler.problem.nullReference=warning
 org.eclipse.jdt.core.compiler.problem.nullSpecViolation=warning
-org.eclipse.jdt.core.compiler.problem.nullUncheckedConversion=warning
+org.eclipse.jdt.core.compiler.problem.nullUncheckedConversion=ignore
 org.eclipse.jdt.core.compiler.problem.overridingMethodWithoutSuperInvocation=ignore
 org.eclipse.jdt.core.compiler.problem.overridingPackageDefaultMethod=warning
 org.eclipse.jdt.core.compiler.problem.parameterAssignment=ignore

runtime/java/src/common/CMDContextVisualization.java

@@ -0,0 +1,27 @@
+package common;
+
+import java.util.Iterator;
+
+public class CMDContextVisualization extends ContextVisualization {
+ private final String printFormat = "%s\n%s\n%s\n";
+ protected String border;
+
+ public CMDContextVisualization(String border) {
+ super();
+
+ this.border = border;
+ }
+
+ @Override
+ public void show() {
+ // for(NodeContextMessage nodeContextMessage : this.contextStack.iterator()) {
+ // System.out.printf(this.printFormat, this.border, nodeContextMessage.toString(), this.border);
+ // }
+
+ Iterator<NodeContextMessage> iterator = this.contextStack.iterator();
+ while (iterator.hasNext()) {
+ NodeContextMessage nodeContextMessage = iterator.next();
+ System.out.printf(this.printFormat, this.border, nodeContextMessage.toString(), this.border);
+ }
+ }
+}

runtime/java/src/common/ContextStack.java

@@ -0,0 +1,63 @@
+package common;
+
+// Key intermediate structure of debugging contextualization.
+// We push/pop nodes while navigating in Debug.java into this stack.
+// A ContextStack is then a member of a SimplifiedContextStack, which
+// produces the actual contextualization.
+
+// ContextStack is fundementally a stack of NodeContextMessage objects.
+// Each of these objects represents a record of contextualization
+// information we store about a single visited node (only maintain
+// those on the path from root to the current node, like a DFS traversal).
+
+// Wrapped around built-in Java Stack class
+// No error handling in current version
+
+import java.util.Iterator;
+import java.util.Stack;
+
+import javax.swing.plaf.basic.BasicInternalFrameTitlePane.SystemMenuBar;
+
+public class ContextStack {
+
+ public void push(DecoratedNode n) {
+
+ this.height++;
+ NodeContextMessage ncm = new NodeContextMessage(n, this.nextIndex++);
+ this.stack.push(ncm);
+ }
+
+ public NodeContextMessage pop() {
+
+ this.height--;
+ this.nextIndex--;
+ return this.stack.pop();
+ } 
+
+ public NodeContextMessage peak() {
+ return this.stack.peek();
+ }
+
+ public int getHeight() {
+ return this.height;
+ }
+
+ public Iterator<NodeContextMessage> iterator() {
+ return this.stack.iterator();
+ }
+
+ public NodeContextMessage get(int stackIndex) {
+
+ // Index 0 is the bottom of the stack
+ if (stackIndex >= 0 && stackIndex < this.stack.size()) {
+ return this.stack.get(stackIndex);
+ } else {
+ throw new IndexOutOfBoundsException("Index " + stackIndex + " is out of bounds.");
+ }
+ }
+
+ private Stack<NodeContextMessage> stack = new Stack<NodeContextMessage>();
+ private int height = 0;
+ // Used for indices
+ private int nextIndex = 1;
+}

runtime/java/src/common/ContextVisualization.java

@@ -0,0 +1,23 @@
+package common;
+
+public abstract class ContextVisualization {
+ protected ContextStack contextStack;
+
+ public ContextVisualization() {
+ this.contextStack = new ContextStack();
+ }
+
+ public void push(DecoratedNode decoratedNode) {
+ this.contextStack.push(decoratedNode);
+ } 
+
+ public NodeContextMessage pop() {
+ return this.contextStack.pop();
+ }
+
+ public abstract void show();
+
+ public ContextStack getContextStack() {
+ return this.contextStack;
+ }
+}