diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 5a47abf..4815a71 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -49,7 +49,7 @@ jobs: - name: Type-check run: npx tsc --noEmit - - name: Build server + - name: Build and test server working-directory: server run: | mvn -B package diff --git a/server/src/test/java/dtos/diagnostics/SourcePositionDTOTest.java b/server/src/test/java/dtos/diagnostics/SourcePositionDTOTest.java new file mode 100644 index 0000000..c8f7364 --- /dev/null +++ b/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)); + } +} diff --git a/server/src/test/java/utils/ContextHistoryConverterTest.java b/server/src/test/java/utils/ContextHistoryConverterTest.java new file mode 100644 index 0000000..6485142 --- /dev/null +++ b/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()); + } +} diff --git a/server/src/test/java/utils/DiagnosticConverterTest.java b/server/src/test/java/utils/DiagnosticConverterTest.java new file mode 100644 index 0000000..b276efb --- /dev/null +++ b/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()); + } +} diff --git a/server/src/test/java/utils/PathUtilsTest.java b/server/src/test/java/utils/PathUtilsTest.java new file mode 100644 index 0000000..6c2e9f8 --- /dev/null +++ b/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)); + } +}