Add language server unit tests

.github/workflows/test.yml

@@ -33,6 +33,10 @@ jobs:
           java-version: 21
           distribution: temurin
 
+      - name: Test server
+        working-directory: server
+        run: mvn -B test
+
       - name: Setup Node.js
         uses: actions/setup-node@v4
         with:

server/src/test/java/dtos/diagnostics/SourcePositionDTOTest.java

@@ -0,0 +1,29 @@
+package dtos.diagnostics;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import org.junit.jupiter.api.Test;
+
+import spoon.reflect.cu.SourcePosition;
+
+class SourcePositionDTOTest {
+    @Test
+    void convertsStringRangeToZeroBasedLinesAndExclusiveEndColumn() {
+        assertEquals(new SourcePositionDTO(null, 1, 4, 3, 18), SourcePositionDTO.from("2:5-4:18"));
+        assertEquals(new SourcePositionDTO(null, 0, 0, 0, 1), SourcePositionDTO.from("1:1-1:1"));
+    }
+
+    @Test
+    void rejectsMalformedRanges() {
+        for (String invalid : new String[] { "", "2:5", "2:5-4", " 2:5-4:18", "2:a-4:18", "prefix 2:5-4:18" }) {
+            assertNull(SourcePositionDTO.from(invalid));
+        }
+    }
+
+    @Test
+    void toleratesMissingAndUnavailablePositions() {
+        assertNull(SourcePositionDTO.from((String) null));
+        assertNull(SourcePositionDTO.from((SourcePosition) null));
+        assertNull(SourcePositionDTO.from(SourcePosition.NOPOSITION));
+    }
+}

server/src/test/java/utils/ContextHistoryConverterTest.java

@@ -0,0 +1,60 @@
+package utils;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.List;
+import java.util.Set;
+
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+import dtos.context.ContextHistoryDTO;
+import dtos.diagnostics.SourcePositionDTO;
+import liquidjava.processor.context.ContextHistory;
+import liquidjava.processor.context.Variable;
+import liquidjava.rj_language.Predicate;
+import spoon.Launcher;
+
+class ContextHistoryConverterTest {
+    private final ContextHistory history = ContextHistory.getInstance();
+
+    @BeforeEach
+    @AfterEach
+    void clearHistory() {
+        history.clearHistory();
+    }
+
+    @Test
+    void convertsEmptyHistoryToEmptyCollections() {
+        ContextHistoryDTO dto = ContextHistoryConverter.convertToDTO(history);
+        assertTrue(dto.localVars().isEmpty());
+        assertTrue(dto.globalVars().isEmpty());
+        assertTrue(dto.ghosts().isEmpty());
+        assertTrue(dto.aliases().isEmpty());
+        assertTrue(dto.methods().isEmpty());
+        assertTrue(dto.fileScopes().isEmpty());
+    }
+
+    @Test
+    void convertsScopesPerFileWithoutDependingOnSetOrder() {
+        history.getFileScopes().put("Example.java", Set.of("2:5-4:18", "1:1-1:1"));
+        history.getFileScopes().put("Other.java", Set.of("8:3-9:12"));
+        ContextHistoryDTO dto = ContextHistoryConverter.convertToDTO(history);
+        assertEquals(Set.of("Example.java", "Other.java"), dto.fileScopes().keySet());
+        assertEquals(Set.of(new SourcePositionDTO(null, 1, 4, 3, 18), new SourcePositionDTO(null, 0, 0, 0, 1)),
+                Set.copyOf(dto.fileScopes().get("Example.java")));
+        assertEquals(List.of(new SourcePositionDTO(null, 7, 2, 8, 12)), dto.fileScopes().get("Other.java"));
+    }
+
+    @Test
+    void omitsVariablesWithoutCodePlacement() {
+        Variable generated = new Variable("generated", new Launcher().getFactory().Type().INTEGER_PRIMITIVE,
+                new Predicate());
+        history.getLocalVars().add(generated);
+        history.getGlobalVars().add(generated);
+        ContextHistoryDTO dto = ContextHistoryConverter.convertToDTO(history);
+        assertTrue(dto.localVars().isEmpty());
+        assertTrue(dto.globalVars().isEmpty());
+    }
+}

server/src/test/java/utils/DiagnosticConverterTest.java

@@ -0,0 +1,180 @@
+package utils;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.List;
+
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.io.TempDir;
+
+import dtos.diagnostics.LJDiagnosticDTO;
+import dtos.diagnostics.SourcePositionDTO;
+import dtos.errors.*;
+import dtos.warnings.*;
+import liquidjava.diagnostics.TranslationTable;
+import liquidjava.diagnostics.errors.*;
+import liquidjava.diagnostics.warnings.*;
+import liquidjava.processor.VCImplication;
+import liquidjava.processor.context.PlacementInCode;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.opt.VCSimplificationResult;
+import spoon.Launcher;
+import spoon.reflect.cu.SourcePosition;
+import spoon.reflect.declaration.CtField;
+
+class DiagnosticConverterTest {
+    @TempDir
+    Path workspace;
+
+    private CtField<?> field;
+    private SourcePosition position;
+
+    @BeforeEach
+    void createSourcePosition() throws Exception {
+        Path file = workspace.resolve("Example.java");
+        Files.writeString(file, "class Example {\n    int value = 0;\n}\n");
+        Launcher launcher = new Launcher();
+        launcher.getEnvironment().setNoClasspath(true);
+        launcher.addInputResource(file.toString());
+        launcher.buildModel();
+        field = launcher.getFactory().Class().get("Example").getField("value");
+        position = field.getPosition();
+    }
+
+    @Test
+    void preservesCommonDiagnosticFields() throws Exception {
+        CustomError error = new CustomError("verification failed", position);
+        error.setHint("check the refinement");
+        LJDiagnosticDTO dto = (LJDiagnosticDTO) DiagnosticConverter.convertToDTO(error);
+        assertEquals("error", dto.category);
+        assertEquals("custom-error", dto.type);
+        assertEquals("Error", dto.title);
+        assertEquals("verification failed", dto.message);
+        assertEquals("check the refinement", dto.hint);
+        assertEquals(workspace.resolve("Example.java").toRealPath().toString(), dto.file);
+        assertEquals(new SourcePositionDTO(dto.file, 1, 8, 1, 18), dto.position);
+    }
+
+    @Test
+    void convertsIllegalConstructorTransitionToAnError() {
+        LJDiagnosticDTO dto = (LJDiagnosticDTO) DiagnosticConverter.convertToDTO(
+                new IllegalConstructorTransitionError(position));
+        assertEquals("error", dto.category);
+        assertEquals("illegal-constructor-transition-error", dto.type);
+    }
+
+    @Test
+    void convertsCustomWarningWithoutTreatingItAsAnError() {
+        LJDiagnosticDTO dto = (LJDiagnosticDTO) DiagnosticConverter.convertToDTO(new CustomWarning("custom warning"));
+        assertEquals("warning", dto.category);
+        assertEquals("custom-warning", dto.type);
+        assertEquals("custom warning", dto.message);
+    }
+
+    @Test
+    void preservesErrorSpecificDetails() {
+        SyntaxErrorDTO syntax = (SyntaxErrorDTO) DiagnosticConverter.convertToDTO(new SyntaxError("invalid syntax", "_ >"));
+        assertEquals("error", syntax.category);
+        assertEquals("syntax-error", syntax.type);
+        assertEquals("_ >", syntax.refinement);
+        assertNull(syntax.file);
+        assertNull(syntax.position);
+        assertTrue(syntax.translationTable.isEmpty());
+
+        InvalidRefinementErrorDTO invalid = (InvalidRefinementErrorDTO) DiagnosticConverter.convertToDTO(
+                new InvalidRefinementError(position, "not boolean", "42"));
+        assertEquals("error", invalid.category);
+        assertEquals("invalid-refinement-error", invalid.type);
+        assertEquals("42", invalid.refinement);
+
+        NotFoundErrorDTO missing = (NotFoundErrorDTO) DiagnosticConverter.convertToDTO(
+                new NotFoundError(position, "missing", NotFoundError.Kind.GHOST, List.of()));
+        assertEquals("error", missing.category);
+        assertEquals("not-found-error", missing.type);
+        assertEquals("missing", missing.name);
+        assertEquals("Ghost", missing.kind);
+
+        StateConflictErrorDTO conflict = (StateConflictErrorDTO) DiagnosticConverter.convertToDTO(
+                new StateConflictError(position, new LiteralBoolean(false), null));
+        assertEquals("error", conflict.category);
+        assertEquals("state-conflict-error", conflict.type);
+        assertEquals("false", conflict.state);
+    }
+
+    @Test
+    void preservesWarningSpecificDetailsAndOverloadHint() {
+        ExternalClassNotFoundWarningDTO missingClass = (ExternalClassNotFoundWarningDTO) DiagnosticConverter.convertToDTO(
+                new ExternalClassNotFoundWarning(position, "missing class", "example.External"));
+        assertEquals("warning", missingClass.category);
+        assertEquals("external-class-not-found-warning", missingClass.type);
+        assertEquals("example.External", missingClass.className);
+
+        ExternalMethodNotFoundWarningDTO missingMethod = (ExternalMethodNotFoundWarningDTO) DiagnosticConverter.convertToDTO(
+                new ExternalMethodNotFoundWarning(position, "missing method", "run()", "example.External",
+                        new String[] { "run(int)", "run(String)" }));
+        assertEquals("warning", missingMethod.category);
+        assertEquals("external-method-not-found-warning", missingMethod.type);
+        assertEquals("run()", missingMethod.signature);
+        assertEquals("example.External", missingMethod.className);
+        assertArrayEquals(new String[] { "run(int)", "run(String)" }, missingMethod.overloads);
+        assertEquals("Available overloads:\n  run(int)\n  run(String)", missingMethod.hint);
+
+        UnsatisfiableRefinementWarningDTO unsatisfiable = (UnsatisfiableRefinementWarningDTO) DiagnosticConverter.convertToDTO(
+                new UnsatisfiableRefinementWarning(position, "_ > 0 && _ < 0"));
+        assertEquals("warning", unsatisfiable.category);
+        assertEquals("unsatisfiable-refinement-warning", unsatisfiable.type);
+        assertEquals("_ > 0 && _ < 0", unsatisfiable.refinement);
+    }
+
+    @Test
+    void preservesRefinementDetailsAndSimplificationHistory() {
+        VCSimplificationResult origin = new VCSimplificationResult(new VCImplication(new Predicate()));
+        VCSimplificationResult found = new VCSimplificationResult(
+                new VCImplication(new Predicate(new LiteralBoolean(false))), origin, "constant folding");
+        RefinementErrorDTO dto = (RefinementErrorDTO) DiagnosticConverter.convertToDTO(
+                new RefinementError(position, position, new Predicate(), found, null, null, "expected true"));
+        assertEquals("error", dto.category);
+        assertEquals("refinement-error", dto.type);
+        assertEquals("true", dto.expected);
+        assertEquals("expected true", dto.customMessage);
+        assertEquals(dto.position, dto.declarationPosition);
+        assertEquals("false", dto.found.implication().predicate());
+        assertEquals("constant folding", dto.found.simplification());
+        assertEquals("true", dto.found.origin().implication().predicate());
+        assertNull(dto.found.origin().origin());
+        assertNull(dto.found.origin().simplification());
+        assertTrue(dto.counterexample.assignments().isEmpty());
+    }
+
+    @Test
+    void preservesStateRefinementDetailsWithoutDeclarationFile() {
+        StateRefinementErrorDTO dto = (StateRefinementErrorDTO) DiagnosticConverter.convertToDTO(
+                new StateRefinementError(position, null, new Predicate(new LiteralBoolean(false)),
+                        new VCSimplificationResult(new VCImplication(new Predicate())), null, "expected closed"));
+        assertEquals("error", dto.category);
+        assertEquals("state-refinement-error", dto.type);
+        assertEquals("false", dto.expected);
+        assertEquals("true", dto.found.implication().predicate());
+        assertEquals("expected closed", dto.customMessage);
+        assertNull(dto.declarationPosition);
+        assertNull(dto.stateMachine);
+    }
+
+    @Test
+    void convertsTranslationTablePlacementsAndDisplayNames() {
+        TranslationTable table = new TranslationTable();
+        table.put("#value_12", PlacementInCode.createPlacement(field));
+        ArgumentMismatchErrorDTO dto = (ArgumentMismatchErrorDTO) DiagnosticConverter.convertToDTO(
+                new ArgumentMismatchError("wrong arguments", position, table));
+        assertEquals("error", dto.category);
+        assertEquals("argument-mismatch-error", dto.type);
+        assertEquals(1, dto.translationTable.size());
+        assertFalse(dto.translationTable.containsKey("#value_12"));
+        assertEquals("int value = 0;", dto.translationTable.get("value¹²").text());
+        assertEquals(dto.position, dto.translationTable.get("value¹²").position());
+    }
+}

server/src/test/java/utils/PathUtilsTest.java

@@ -0,0 +1,95 @@
+package utils;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.io.File;
+import java.nio.file.Path;
+
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.io.TempDir;
+
+class PathUtilsTest {
+    @TempDir
+    Path workspace;
+
+    @Test
+    void extractsSourceFolderAtDifferentDepths() {
+        for (String parent : new String[] { "", "project", "projects/example/module" }) {
+            Path sourceRoot = workspace.resolve(parent).resolve("src/main");
+            assertEquals(sourceRoot.toString(),
+                    PathUtils.extractBasePath(sourceRoot.resolve("java/Example.java").toUri().toString()));
+        }
+    }
+
+    @Test
+    void usesFirstSourceFolderAndOneFollowingSegment() {
+        Path sourceRoot = workspace.resolve("src/generated");
+        assertEquals(sourceRoot.toString(),
+                PathUtils.extractBasePath(sourceRoot.resolve("src/main/Example.java").toUri().toString()));
+    }
+
+    @Test
+    void retainsFullPathWithoutSourceFolder() {
+        Path file = workspace.resolve("sources/Example.java");
+        assertEquals(file.toString(), PathUtils.extractBasePath(file.toUri().toString()));
+    }
+
+    @Test
+    void retainsPathEndingAtSourceFolder() {
+        Path source = workspace.resolve("src");
+        assertEquals(source.toString(), PathUtils.extractBasePath(source.toUri().toString()));
+    }
+
+    @Test
+    void decodesEscapedSourcePath() {
+        Path source = workspace.resolve("project with spaces/src/main");
+        assertEquals(source.toString(),
+                PathUtils.extractBasePath(source.resolve("Example.java").toUri().toString()));
+    }
+
+    @Test
+    void handlesWindowsDriveUrisUsingHostPathSemantics() {
+        // a windows file uri has a drive root on windows, and /C:/ on unix.
+        String source = File.separatorChar == '\\' ? "C:\\Users\\user\\project\\src\\main"
+                : "/C:/Users/user/project/src/main";
+        assertEquals(source, PathUtils.extractBasePath("file:///C:/Users/user/project/src/main/java/Example.java"));
+        assertTrue(PathUtils.isFileInDirectory("file:///C:/Users/user/project/src/main/java/Example.java",
+                "file:///C:/Users/user/project"));
+        assertFalse(PathUtils.isFileInDirectory("file:///D:/Users/user/project/Example.java",
+                "file:///C:/Users/user/project"));
+    }
+
+    @Test
+    void matchesDirectorySegmentsRatherThanStringPrefixes() {
+        Path directory = workspace.resolve("project");
+        assertTrue(PathUtils.isFileInDirectory(directory.resolve("src/main/Example.java").toUri().toString(),
+                directory.toUri().toString()));
+        assertFalse(PathUtils.isFileInDirectory(workspace.resolve("project-other/Example.java").toUri().toString(),
+                directory.toUri().toString()));
+        assertFalse(PathUtils.isFileInDirectory(workspace.resolve("Elsewhere.java").toUri().toString(),
+                directory.toUri().toString()));
+    }
+
+    @Test
+    void rejectsInvalidAndNonFileUrisForDirectoryMembership() {
+        String directory = workspace.toUri().toString();
+        for (String invalid : new String[] { null, "not a uri", "https://example.com/Example.java", "file://host/path" }) {
+            assertFalse(PathUtils.isFileInDirectory(invalid, directory));
+            assertFalse(PathUtils.isFileInDirectory(directory, invalid));
+        }
+    }
+
+    @Test
+    void convertsFilePathsToEscapedUris() {
+        Path file = workspace.resolve("project with spaces/Example.java");
+        String uri = PathUtils.toFileUri(file.toString());
+        assertTrue(uri.startsWith("file:"));
+        assertTrue(uri.contains("project%20with%20spaces"));
+        assertEquals(file, Path.of(java.net.URI.create(uri)));
+    }
+
+    @Test
+    void convertsNullPathToEmptyUri() {
+        assertEquals("", PathUtils.toFileUri(null));
+    }
+}