migration of lsp, further fixes

jml2java/build.gradle.kts

@@ -6,4 +6,5 @@ plugins {
 dependencies {
     api(project(":utils"))
     testImplementation(libs.snakeyaml)
+    testImplementation(kotlin("serialization"))
 }

jml2java/src/test/kotlin/jml2java/Jml2JavaTests.kt → jml2java/src/test/kotlin/io/github/jmltoolkit/jml2java/Jml2JavaTests.kt

@@ -1,11 +1,10 @@
-package jml2java
+package io.github.jmltoolkit.jml2java
 
 import com.github.javaparser.ParseResult
 import com.github.javaparser.Problem
 import com.github.javaparser.ast.expr.Expression
 import com.github.javaparser.printer.DefaultPrettyPrinter
 import com.google.common.truth.Truth
-import io.github.jmltoolkit.jml2java.Jml2JavaFacade
 import io.github.jmltoolkit.utils.TestWithJavaParser
 import org.junit.jupiter.api.Assertions
 import org.junit.jupiter.api.DynamicTest
@@ -23,7 +22,7 @@ class Jml2JavaTests : TestWithJavaParser() {
     @TestFactory
     @Throws(IOException::class)
     fun j2jTranslation(): Stream<DynamicTest> {
-        javaClass.getResourceAsStream("expr.yaml").use { inputStream ->
+        javaClass.getResourceAsStream("/expr.yaml").use { inputStream ->
             val yaml = Yaml()
             val obj: List<Map<String, Any>> = yaml.load(inputStream)
             return obj.stream().map { m: Map<String, Any> ->
@@ -36,7 +35,7 @@ class Jml2JavaTests : TestWithJavaParser() {
         }
     }
 
-    fun jml2JavaTranslation(input: String?, expected: String) {
+    private fun jml2JavaTranslation(input: String?, expected: String) {
         val e: ParseResult<Expression> = parser.parseJmlExpression(input)
         if (!e.isSuccessful) {
             e.problems.forEach(Consumer { x: Problem? -> System.err.println(x) })

jml2java/src/test/kotlin/jml2java/Jml2JavaTranslatorTest.kt → jml2java/src/test/kotlin/io/github/jmltoolkit/jml2java/Jml2JavaTranslatorTest.kt

@@ -1,8 +1,7 @@
-package jml2java
+package io.github.jmltoolkit.jml2java
 
 import com.github.javaparser.ast.jml.expr.JmlQuantifiedExpr
 import com.google.common.truth.Truth
-import io.github.jmltoolkit.jml2java.Jml2JavaTranslator
 import org.junit.jupiter.api.Test
 
 /**

jml2java/src/test/kotlin/jml2java/PatternTest.kt → jml2java/src/test/kotlin/io/github/jmltoolkit/jml2java/PatternTest.kt

@@ -1,4 +1,4 @@
-package jml2java
+package io.github.jmltoolkit.jml2java
 
 import io.github.jmltoolkit.utils.Pattern
 import org.junit.jupiter.api.Test

lint/build.gradle.kts

@@ -8,4 +8,6 @@ dependencies {
     api(libs.gson)
     implementation(libs.logback)
     implementation("se.bjurr.violations:violations-lib:1.156.7")
+
+    testImplementation(project(":utils"))
 }

lint/src/main/kotlin/io/github/jmltoolkit/lint/JmlLintingFacade.kt

@@ -12,14 +12,8 @@ import kotlin.Exception
  * @author Alexander Weigl
  * @version 1 (12/29/21)
  */
-class JmlLintingFacade(config: JmlLintingConfig) {
-    private val linters: List<LintRule>
-    private val config: JmlLintingConfig
-
-    init {
-        linters = getLinter(config)
-        this.config = config
-    }
+class JmlLintingFacade(private val config: JmlLintingConfig) {
+    val linters: List<LintRule> = getLinter(config)
 
     private val sarifTool: Tool
         get() = Tool().withDriver(
@@ -64,7 +58,7 @@ class JmlLintingFacade(config: JmlLintingConfig) {
 
     companion object {
         private val LOGGER: Logger = LoggerFactory.getLogger(JmlLintingFacade::class.java)
-        private val VERSION: String = JmlLintingFacade::class.java.getPackage().implementationVersion
+        private val VERSION: String = JmlLintingFacade::class.java.getPackage().implementationVersion ?: "n/a"
         private const val NAME = "JML-lint"
 
         private fun getLinter(config: JmlLintingConfig): List<LintRule> {

lint/src/test/kotlin/LinterTest.kt

@@ -1,23 +1,22 @@
-import com.github.jmlparser.TestWithJavaParser;
-import org.junit.jupiter.api.Assumptions;
-import org.junit.jupiter.api.Test;
-
-import java.util.Collections;
+import io.github.jmltoolkit.lint.JmlLintingConfig
+import io.github.jmltoolkit.lint.JmlLintingFacade
+import io.github.jmltoolkit.utils.TestWithJavaParser
+import org.junit.jupiter.api.Assumptions
+import org.junit.jupiter.api.Test
 
 /**
  * @author Alexander Weigl
  * @version 1 (14.10.22)
  */
-class LinterTest extends TestWithJavaParser {
+internal class LinterTest : TestWithJavaParser() {
     @Test
-    void everythingWrong() {
-        var result = parser.parse(getClass().getResourceAsStream("EverythingWrong.java"));
-        Assumptions.assumeTrue(result.isSuccessful());
-        var actual =
-                new JmlLintingFacade(new JmlLintingConfig()).lint(Collections.singletonList(result.getResult().get()));
+    fun everythingWrong() {
+        val result = parser.parse(javaClass.getResourceAsStream("EverythingWrong.java"))
+        Assumptions.assumeTrue(result.isSuccessful)
+        val actual = JmlLintingFacade(JmlLintingConfig()).lint(listOf(result.result.get()))
 
-        for (LintProblem lintProblem : actual) {
-            System.out.println(lintProblem);
+        for (lintProblem in actual) {
+            println(lintProblem)
         }
     }
 }

lsp/build.gradle.kts

@@ -0,0 +1,36 @@
+plugins {
+    id("standard-kotlin")
+    id("com.github.johnrengelman.shadow") version "7.1.2"
+    id("application")
+}
+
+version = "1.0-SNAPSHOT"
+
+dependencies {
+    api(libs.jmlcore)
+    api(libs.jmlsymbol)
+
+    testImplementation(kotlin("test"))
+
+    implementation(project(":utils"))
+    implementation(project(":smt"))
+    implementation(project(":wd"))
+    implementation(project(":stat"))
+    implementation(project(":redux"))
+    implementation(project(":lint"))
+    implementation(project(":jml2java"))
+
+    implementation("org.tinylog:tinylog-api-kotlin:2.5.0")
+    implementation("org.tinylog:tinylog-api:2.5.0-M2.1")
+    implementation("org.tinylog:tinylog-impl:2.5.0")
+
+    implementation("org.eclipse.lsp4j:org.eclipse.lsp4j:0.21.2")
+
+    implementation("com.github.ajalt.clikt:clikt:4.2.2")
+
+    //implementation("org.apache.groovy:groovy:4.0.6")
+}
+
+application {
+    mainClass = "jml.lsp.Main"
+}

lsp/settings.gradle.kts

@@ -0,0 +1,3 @@
+
+rootProject.name = "jml-lsp"
+

lsp/src/main/kotlin/jml/lsp/CatchSymbols.kt

@@ -0,0 +1,227 @@
+package jml.lsp
+
+import com.github.javaparser.ast.CompilationUnit
+import com.github.javaparser.ast.Node
+import com.github.javaparser.ast.NodeList
+import com.github.javaparser.ast.body.*
+import com.github.javaparser.ast.expr.VariableDeclarationExpr
+import com.github.javaparser.ast.jml.body.*
+import com.github.javaparser.ast.jml.clauses.*
+import com.github.javaparser.ast.modules.ModuleDeclaration
+import com.github.javaparser.ast.visitor.GenericVisitorAdapter
+import org.eclipse.lsp4j.DocumentSymbol
+import org.eclipse.lsp4j.SymbolKind
+import java.util.*
+
+/**
+ * Runs through an AST and gathers symbols within JML annotations.
+ *
+ * @author Alexander Weigl
+ */
+class CatchSymbols : GenericVisitorAdapter<MutableList<DocumentSymbol>?, Unit?>() {
+    override fun visit(n: CompilationUnit, arg: Unit?): MutableList<DocumentSymbol> {
+        val children = acceptAll(n.types)
+        return arrayListOf(
+            DocumentSymbol(
+                n.storage.get().fileName,
+                SymbolKind.File,
+                n.asRange, n.primaryType.map { it.name.asRange }.orElse(n.asRange), "", children
+            )
+        )
+    }
+
+    override fun visit(n: AnnotationDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        val children = acceptAll(n.members)
+        return arrayListOf(
+            DocumentSymbol(
+                n.nameAsString,
+                SymbolKind.Interface,
+                n.asRange, n.name.asRange, "", children
+            )
+        )
+    }
+
+    override fun visit(n: AnnotationMemberDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        return arrayListOf(
+            DocumentSymbol(
+                n.nameAsString,
+                SymbolKind.Field,
+                n.asRange, n.name.asRange, ""
+            )
+        )
+    }
+
+    override fun visit(n: ClassOrInterfaceDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        val children = acceptAll(n.members)
+        return arrayListOf(
+            DocumentSymbol(
+                n.nameAsString,
+                if (n.isInterface) SymbolKind.Interface else SymbolKind.Class,
+                n.asRange, n.name.asRange, "", children
+            )
+        )
+    }
+
+    private fun acceptAll(members: NodeList<*>?): MutableList<DocumentSymbol> {
+        if (members == null) return arrayListOf()
+        return members.flatMap { it.accept(this, null) ?: arrayListOf() }.toMutableList()
+    }
+
+    private fun <T : Node> acceptAllo(members: Optional<NodeList<T>>?): MutableList<DocumentSymbol> =
+        acceptAll(members?.orElse(null))
+
+    override fun visit(n: ConstructorDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        val children = acceptAllo(n.contracts)
+        return arrayListOf(
+            DocumentSymbol(
+                n.nameAsString,
+                SymbolKind.Constructor,
+                n.asRange, n.name.asRange, "", children
+            )
+        )
+    }
+
+
+    override fun visit(n: EnumConstantDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        return arrayListOf(
+            DocumentSymbol(
+                n.nameAsString,
+                SymbolKind.EnumMember,
+                n.asRange, n.name.asRange,
+            )
+        )
+    }
+
+    override fun visit(n: EnumDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        val children = acceptAll(n.members)
+        return arrayListOf(
+            DocumentSymbol(
+                n.nameAsString,
+                SymbolKind.Enum,
+                n.asRange, n.name.asRange, "", children
+            )
+        )
+    }
+
+    override fun visit(n: FieldDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        return n.variables.map {
+            DocumentSymbol(
+                it.nameAsString,
+                SymbolKind.Field,
+                it.asRange, it.name.asRange, it.typeAsString, arrayListOf()
+            )
+        }.toMutableList()
+    }
+
+    override fun visit(n: MethodDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        val children = acceptAllo(n.contracts)
+        return arrayListOf(
+            DocumentSymbol(
+                n.nameAsString,
+                SymbolKind.Method,
+                n.asRange, n.name.asRange, "", children
+            )
+        )
+    }
+
+    override fun visit(n: JmlMethodDeclaration, arg: Unit?): MutableList<DocumentSymbol>? {
+        return n.methodDeclaration.accept(this, arg)
+    }
+
+    override fun visit(n: VariableDeclarationExpr?, arg: Unit?): MutableList<DocumentSymbol>? {
+        return super.visit(n, arg)
+    }
+
+    override fun visit(n: ModuleDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        return arrayListOf(
+            DocumentSymbol(
+                n.nameAsString,
+                SymbolKind.Module,
+                n.asRange, n.name.asRange, "", arrayListOf()
+            )
+        )
+    }
+
+    override fun visit(n: JmlContract, arg: Unit?): MutableList<DocumentSymbol> {
+        val children = acceptAll(n.subContracts) + acceptAll(n.clauses)
+        return arrayListOf(
+            DocumentSymbol(
+                n.name.map { it.asString() }.orElse(n.behavior.asString()),
+                SymbolKind.Key,
+                n.asRange, n.asRange, "${n.jmlTags}", children
+            )
+        )
+    }
+
+    override fun visit(n: JmlRepresentsDeclaration?, arg: Unit?): MutableList<DocumentSymbol> {
+        return arrayListOf()//return super.visit(n, arg)
+    }
+
+    override fun visit(n: JmlFieldDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        val decl = n.decl
+        return decl.variables.map { v ->
+            DocumentSymbol(
+                v.nameAsString,
+                SymbolKind.Property,
+                n.asRange, n.asRange, "Jml model method: activated with ${n.jmlTags}", listOf()
+            )
+        }.toMutableList()
+
+    }
+
+    override fun visit(n: JmlClassAccessibleDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        return arrayListOf() //super.visit(n, arg)
+    }
+
+    override fun visit(n: JmlClassExprDeclaration, arg: Unit?): MutableList<DocumentSymbol> {
+        return arrayListOf(
+            DocumentSymbol(
+                n.name.map { it.asString() }.orElse("anon invariant"),
+                SymbolKind.Property,
+                n.asRange, n.asRange, "Jml class invariant", listOf()
+            )
+        )
+    }
+
+    override fun visit(n: JmlSimpleExprClause, arg: Unit?): MutableList<DocumentSymbol> {
+        return arrayListOf(
+            DocumentSymbol(
+                n.name.map { "$it : ${n.kind}" }.orElse("Clause ${n.kind}"),
+                SymbolKind.EnumMember,
+                n.asRange, n.asRange, "Jml clause", listOf()
+            )
+        )
+    }
+
+    override fun visit(n: JmlSignalsClause?, arg: Unit?): MutableList<DocumentSymbol>? {
+        return super.visit(n, arg)
+    }
+
+    override fun visit(n: JmlSignalsOnlyClause?, arg: Unit?): MutableList<DocumentSymbol>? {
+        return super.visit(n, arg)
+    }
+
+    override fun visit(n: JmlCallableClause?, arg: Unit?): MutableList<DocumentSymbol>? {
+        return super.visit(n, arg)
+    }
+
+    override fun visit(n: JmlCapturesClause?, arg: Unit?): MutableList<DocumentSymbol>? {
+        return super.visit(n, arg)
+    }
+
+    override fun visit(n: JmlForallClause?, arg: Unit?): MutableList<DocumentSymbol>? {
+        return super.visit(n, arg)
+    }
+
+    override fun visit(n: JmlClauseIf?, arg: Unit?): MutableList<DocumentSymbol>? {
+        return super.visit(n, arg)
+    }
+
+    override fun visit(n: JmlOldClause?, arg: Unit?): MutableList<DocumentSymbol>? {
+        return super.visit(n, arg)
+    }
+
+    override fun visit(n: JmlMultiExprClause?, arg: Unit?): MutableList<DocumentSymbol>? {
+        return super.visit(n, arg)
+    }
+}