From f5c0f8c645082b1f439d2e69c3a1f05b957c4a3c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 3 Sep 2023 23:29:36 -0400 Subject: [PATCH 01/15] add initial support for simplify hover information --- .../languageserver/CFTextDocumentService.java | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index c6b880d..92c6aa0 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -1,5 +1,6 @@ package org.checkerframework.languageserver; +import com.google.common.base.Splitter; import com.google.common.collect.RangeMap; import com.google.common.collect.TreeRangeMap; @@ -190,6 +191,7 @@ public void publish(Map>> result) { if (message != null && message.contains("lsp.type.information")) { // this message is for lsp support File file = new File(URI.create(entry.getKey())); +// message = filterLSPTypeInformation(message); publishTypeMessage(file, message); } else { diagnostics.add(convertToLSPDiagnostic(diagnostic)); @@ -235,6 +237,10 @@ public CompletableFuture hover(HoverParams params) { * the range of this type in the given file, separated by the delimiter ";". */ private void publishTypeMessage(File file, String msg) { + msg = filterLSPTypeInformation(msg); + msg = filterKindInformation(msg); + msg = filterCheckerValue(msg); + msg = filterTypeValue(msg); int lastDelimiter = msg.lastIndexOf(';'); String typeInfo = msg.substring(0, lastDelimiter); String positionInfo = msg.substring(lastDelimiter + 1).trim(); @@ -266,4 +272,44 @@ private void publishTypeMessage(File file, String msg) { currentTypeInfo.put( com.google.common.collect.Range.closed(start, end), typeInfoForPosition); } + + public String filterLSPTypeInformation(String input) { + Pattern pattern = Pattern.compile("\\[lsp.type.information\\] (.*)"); + Matcher matcher = pattern.matcher(input); + if (matcher.find()) { + return matcher.group(1); + } + return input; + } + + public String filterKindInformation(String input) { + // The pattern now matches "kind=USE_TYPE" or "kind=DECLARE_TYPE" anywhere in the string + Pattern pattern = Pattern.compile("kind=(USE_TYPE|DECLARED_TYPE); (.*)"); + Matcher matcher = pattern.matcher(input); + if (matcher.find()) { + // Keep the text before "kind=" and append the text after it + return input.substring(0, matcher.start()) + matcher.group(2); + } + return input; + } + + public static String filterCheckerValue(String input) { + Pattern pattern = Pattern.compile("checker=([^;]+)(Checker|Subchecker);(.*)"); + Matcher matcher = pattern.matcher(input); + if (matcher.find()) { + // Extract the value after "checker=" and before "Checker", and append the remaining part of the string + return matcher.group(1) + ": " + matcher.group(3); + } + return input; // return the original input if the pattern is not found + } + + public static String filterTypeValue(String input) { + Pattern pattern = Pattern.compile("(.*)type=(.*)"); + Matcher matcher = pattern.matcher(input); + if (matcher.find()) { + // Extract the value before ": type=" and append the "@" symbol and any following characters until a space or end of string + return matcher.group(1) + matcher.group(2); + } + return input; // return the original input if the pattern is not found + } } From d3e8fc4f22ebd569cdcdbb2938523f3c2bef3eff Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 3 Sep 2023 23:37:49 -0400 Subject: [PATCH 02/15] apply spotless --- .../languageserver/CFTextDocumentService.java | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 92c6aa0..6a85c1e 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -1,6 +1,5 @@ package org.checkerframework.languageserver; -import com.google.common.base.Splitter; import com.google.common.collect.RangeMap; import com.google.common.collect.TreeRangeMap; @@ -191,7 +190,7 @@ public void publish(Map>> result) { if (message != null && message.contains("lsp.type.information")) { // this message is for lsp support File file = new File(URI.create(entry.getKey())); -// message = filterLSPTypeInformation(message); + // message = filterLSPTypeInformation(message); publishTypeMessage(file, message); } else { diagnostics.add(convertToLSPDiagnostic(diagnostic)); @@ -297,7 +296,8 @@ public static String filterCheckerValue(String input) { Pattern pattern = Pattern.compile("checker=([^;]+)(Checker|Subchecker);(.*)"); Matcher matcher = pattern.matcher(input); if (matcher.find()) { - // Extract the value after "checker=" and before "Checker", and append the remaining part of the string + // Extract the value after "checker=" and before "Checker", and append the remaining + // part of the string return matcher.group(1) + ": " + matcher.group(3); } return input; // return the original input if the pattern is not found @@ -307,8 +307,9 @@ public static String filterTypeValue(String input) { Pattern pattern = Pattern.compile("(.*)type=(.*)"); Matcher matcher = pattern.matcher(input); if (matcher.find()) { - // Extract the value before ": type=" and append the "@" symbol and any following characters until a space or end of string - return matcher.group(1) + matcher.group(2); + // Extract the value before ": type=" and append the "@" symbol and any following + // characters until a space or end of string + return matcher.group(1) + matcher.group(2); } return input; // return the original input if the pattern is not found } From 590f5de1383cb1b2a3f92c5cd432aa06dcf9f8a6 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 13 Oct 2023 12:24:46 -0400 Subject: [PATCH 03/15] add support for generics --- .../languageserver/CFTextDocumentService.java | 218 +++++++++++++----- .../languageserver/CheckerTypeKind.java | 23 ++ 2 files changed, 186 insertions(+), 55 deletions(-) create mode 100644 src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 6a85c1e..8905665 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -184,21 +184,175 @@ public void didSave(DidSaveTextDocumentParams params) { public void publish(Map>> result) { for (Map.Entry>> entry : result.entrySet()) { List diagnostics = new ArrayList<>(); + Map> uniqueTypeInfo = + processDiagnosticString(entry, diagnostics); + publishTypeMessageWithFilter(entry, uniqueTypeInfo); + server.publishDiagnostics(new PublishDiagnosticsParams(entry.getKey(), diagnostics)); + } + } - for (javax.tools.Diagnostic diagnostic : entry.getValue()) { - String message = diagnostic.getMessage(Locale.getDefault()); - if (message != null && message.contains("lsp.type.information")) { - // this message is for lsp support - File file = new File(URI.create(entry.getKey())); - // message = filterLSPTypeInformation(message); - publishTypeMessage(file, message); + /** + * Process Diagnostic strings to separate type message and error message. + * + * @param entry The Diagnostic entry for getting diagnostic message + * @param diagnostics A list for storing checkerframework issued errors + * @return TypeMessage processed for non-verbose output + */ + private Map> processDiagnosticString( + Map.Entry>> entry, + List diagnostics) { + Map> TypeMessage = new HashMap<>(); + for (javax.tools.Diagnostic diagnostic : entry.getValue()) { + String message = diagnostic.getMessage(Locale.getDefault()); + if (message != null && message.contains("lsp.type.information")) { + String checker = getChecker(message); + String kind = getKind(message); + String type = getType(message) + "; "; + String positionInfo = getPosistion(message); + if (positionInfo != null) { + if (!TypeMessage.containsKey(positionInfo)) { + List checkerTypeKinds = new ArrayList<>(); + Map kindType = new HashMap<>(); + kindType.put(type, kind); + checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); + TypeMessage.put(positionInfo, checkerTypeKinds); + } else { + List checkerTypeKinds = TypeMessage.get(positionInfo); + boolean foundChecker = false; + + for (CheckerTypeKind checkerTypeKind : checkerTypeKinds) { + if (checkerTypeKind.getCheckername().equals(checker)) { + foundChecker = true; + + if (!checkerTypeKind.getTypeKind().containsKey(type)) { + checkerTypeKind.getTypeKind().put(type, kind); + } + break; + } + } + if (!foundChecker) { + Map kindType = new HashMap<>(); + kindType.put(type, kind); + checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); + } + } + } + } else { + diagnostics.add(convertToLSPDiagnostic(diagnostic)); + } + } + return TypeMessage; + } + + /** + * Publish the given type message for the given file in non-verbose mode. + * + * @param entry The Diagnostic entry for getting file name string + * @param diagnosticString processed for simplicity output + */ + private void publishTypeMessageWithFilter( + Map.Entry>> entry, + Map> diagnosticString) { + for (Map.Entry> typeMessage : diagnosticString.entrySet()) { + String positionInfo = typeMessage.getKey(); + for (CheckerTypeKind typeMap : typeMessage.getValue()) { + if (typeMap.getTypeKind().entrySet().size() == 1) { + for (Map.Entry typeKind : typeMap.getTypeKind().entrySet()) { + StringBuilder typeMessageBuilder = new StringBuilder(); + typeMessageBuilder.append(typeMap.getCheckername()).append(": "); + typeMessageBuilder.append(typeKind.getKey()); + typeMessageBuilder.append(positionInfo); + String msr = typeMessageBuilder.toString(); + File file = new File(URI.create(entry.getKey())); + publishTypeMessage(file, msr); + } } else { - diagnostics.add(convertToLSPDiagnostic(diagnostic)); + for (Map.Entry typeKind : typeMap.getTypeKind().entrySet()) { + StringBuilder typeMessageBuilder = new StringBuilder(); + typeMessageBuilder.append(typeMap.getCheckername()).append(" "); + typeMessageBuilder.append(typeKind.getValue()).append(":"); + typeMessageBuilder.append(typeKind.getKey()); + typeMessageBuilder.append(positionInfo); + String msr = typeMessageBuilder.toString(); + File file = new File(URI.create(entry.getKey())); + publishTypeMessage(file, msr); + } } } + } + } - server.publishDiagnostics(new PublishDiagnosticsParams(entry.getKey(), diagnostics)); + /** + * Return checker name from diagnosticString in checkerframework. + * + * @param typeMessage Type message string from checkerframework + * @return Checker name from checkerframework e.g. Nullness + */ + private static String getChecker(String typeMessage) { + String checkerPrefix = "checker="; + int checkerStart = typeMessage.indexOf(checkerPrefix); + if (checkerStart != -1) { + int checkerEnd = typeMessage.indexOf(";", checkerStart); + if (checkerEnd != -1) { + String checker = + typeMessage + .substring(checkerStart + checkerPrefix.length(), checkerEnd) + .trim(); + checker = checker.replace("Subchecker", "").replace("Checker", "").trim(); + return checker; + } + } + return null; + } + + /** + * Return Kind from diagnosticString in checkerframework. + * + * @param typeMessage Type message string from checkerframework + * @return Lower case kind from checkerframework e.g. use + */ + private static String getKind(String typeMessage) { + String kindPrefix = "kind="; + int kindStart = typeMessage.indexOf(kindPrefix); + if (kindStart != -1) { + int kindEnd = typeMessage.indexOf(";", kindStart); + if (kindEnd != -1) { + String kind = + typeMessage.substring(kindStart + kindPrefix.length(), kindEnd).trim(); + kind = kind.toLowerCase(Locale.ROOT).replace("_type", ""); + return kind; + } } + return null; + } + + /** + * Return Type from diagnosticString in checkerframework. + * + * @param typeMessage Type Message String from checkerframework + * @return Type from checkerframework e.g. @Nullable Object + */ + private static String getType(String typeMessage) { + String typePrefix = "type="; + int typeStart = typeMessage.indexOf(typePrefix); + if (typeStart != -1) { + int typeEnd = typeMessage.indexOf(";", typeStart); + + return typeMessage.substring(typeStart + typePrefix.length(), typeEnd).trim(); + } + return null; + } + + /** + * Return position from diagnosticString in checkerframework. + * + * @param typeMessage Type Message String from checkerframework + * @return Position index from checkerframework e.g. range=(11, 8, 11, 9) + */ + private static String getPosistion(String typeMessage) { + int lastDelimiter = typeMessage.lastIndexOf(';'); + String positionInfo = typeMessage.substring(lastDelimiter + 1).trim(); + return positionInfo; } /** @@ -236,10 +390,6 @@ public CompletableFuture hover(HoverParams params) { * the range of this type in the given file, separated by the delimiter ";". */ private void publishTypeMessage(File file, String msg) { - msg = filterLSPTypeInformation(msg); - msg = filterKindInformation(msg); - msg = filterCheckerValue(msg); - msg = filterTypeValue(msg); int lastDelimiter = msg.lastIndexOf(';'); String typeInfo = msg.substring(0, lastDelimiter); String positionInfo = msg.substring(lastDelimiter + 1).trim(); @@ -271,46 +421,4 @@ private void publishTypeMessage(File file, String msg) { currentTypeInfo.put( com.google.common.collect.Range.closed(start, end), typeInfoForPosition); } - - public String filterLSPTypeInformation(String input) { - Pattern pattern = Pattern.compile("\\[lsp.type.information\\] (.*)"); - Matcher matcher = pattern.matcher(input); - if (matcher.find()) { - return matcher.group(1); - } - return input; - } - - public String filterKindInformation(String input) { - // The pattern now matches "kind=USE_TYPE" or "kind=DECLARE_TYPE" anywhere in the string - Pattern pattern = Pattern.compile("kind=(USE_TYPE|DECLARED_TYPE); (.*)"); - Matcher matcher = pattern.matcher(input); - if (matcher.find()) { - // Keep the text before "kind=" and append the text after it - return input.substring(0, matcher.start()) + matcher.group(2); - } - return input; - } - - public static String filterCheckerValue(String input) { - Pattern pattern = Pattern.compile("checker=([^;]+)(Checker|Subchecker);(.*)"); - Matcher matcher = pattern.matcher(input); - if (matcher.find()) { - // Extract the value after "checker=" and before "Checker", and append the remaining - // part of the string - return matcher.group(1) + ": " + matcher.group(3); - } - return input; // return the original input if the pattern is not found - } - - public static String filterTypeValue(String input) { - Pattern pattern = Pattern.compile("(.*)type=(.*)"); - Matcher matcher = pattern.matcher(input); - if (matcher.find()) { - // Extract the value before ": type=" and append the "@" symbol and any following - // characters until a space or end of string - return matcher.group(1) + matcher.group(2); - } - return input; // return the original input if the pattern is not found - } } diff --git a/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java b/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java new file mode 100644 index 0000000..08c82aa --- /dev/null +++ b/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java @@ -0,0 +1,23 @@ +package org.checkerframework.languageserver; + +import java.util.Map; + +/** This class is for processing type message. */ +public class CheckerTypeKind { + private String checkername; + + private Map TypeKind; + + CheckerTypeKind(String checkername, Map kindType) { + this.checkername = checkername; + this.TypeKind = kindType; + } + + String getCheckername() { + return this.checkername; + } + + Map getTypeKind() { + return this.TypeKind; + } +} From 4c09a40693f982e1093158e0982312799458eb6c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 13 Oct 2023 16:28:24 -0400 Subject: [PATCH 04/15] refactor code --- .../languageserver/CFTextDocumentService.java | 68 ++++++++++--------- 1 file changed, 35 insertions(+), 33 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 8905665..2929f9d 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -207,8 +207,8 @@ private Map> processDiagnosticString( if (message != null && message.contains("lsp.type.information")) { String checker = getChecker(message); String kind = getKind(message); - String type = getType(message) + "; "; - String positionInfo = getPosistion(message); + String type = getType(message); + String positionInfo = getPosition(message); if (positionInfo != null) { if (!TypeMessage.containsKey(positionInfo)) { List checkerTypeKinds = new ArrayList<>(); @@ -219,11 +219,9 @@ private Map> processDiagnosticString( } else { List checkerTypeKinds = TypeMessage.get(positionInfo); boolean foundChecker = false; - for (CheckerTypeKind checkerTypeKind : checkerTypeKinds) { if (checkerTypeKind.getCheckername().equals(checker)) { foundChecker = true; - if (!checkerTypeKind.getTypeKind().containsKey(type)) { checkerTypeKind.getTypeKind().put(type, kind); } @@ -255,27 +253,32 @@ private void publishTypeMessageWithFilter( Map> diagnosticString) { for (Map.Entry> typeMessage : diagnosticString.entrySet()) { String positionInfo = typeMessage.getKey(); - for (CheckerTypeKind typeMap : typeMessage.getValue()) { - if (typeMap.getTypeKind().entrySet().size() == 1) { - for (Map.Entry typeKind : typeMap.getTypeKind().entrySet()) { - StringBuilder typeMessageBuilder = new StringBuilder(); - typeMessageBuilder.append(typeMap.getCheckername()).append(": "); - typeMessageBuilder.append(typeKind.getKey()); - typeMessageBuilder.append(positionInfo); - String msr = typeMessageBuilder.toString(); - File file = new File(URI.create(entry.getKey())); - publishTypeMessage(file, msr); + for (CheckerTypeKind checkerTypeKind : typeMessage.getValue()) { + if (checkerTypeKind.getTypeKind().entrySet().size() == 1) { + for (Map.Entry typeKind : + checkerTypeKind.getTypeKind().entrySet()) { + StringBuilder typeMessageBuilder = + new StringBuilder(checkerTypeKind.getCheckername()) + .append(": ") + .append(typeKind.getKey()) + .append(positionInfo); + publishTypeMessage( + new File(URI.create(entry.getKey())), + typeMessageBuilder.toString()); } } else { - for (Map.Entry typeKind : typeMap.getTypeKind().entrySet()) { - StringBuilder typeMessageBuilder = new StringBuilder(); - typeMessageBuilder.append(typeMap.getCheckername()).append(" "); - typeMessageBuilder.append(typeKind.getValue()).append(":"); - typeMessageBuilder.append(typeKind.getKey()); - typeMessageBuilder.append(positionInfo); - String msr = typeMessageBuilder.toString(); - File file = new File(URI.create(entry.getKey())); - publishTypeMessage(file, msr); + for (Map.Entry typeKind : + checkerTypeKind.getTypeKind().entrySet()) { + StringBuilder typeMessageBuilder = + new StringBuilder(checkerTypeKind.getCheckername()) + .append(" ") + .append(typeKind.getValue()) + .append(":") + .append(typeKind.getKey()) + .append(positionInfo); + publishTypeMessage( + new File(URI.create(entry.getKey())), + typeMessageBuilder.toString()); } } } @@ -283,7 +286,7 @@ private void publishTypeMessageWithFilter( } /** - * Return checker name from diagnosticString in checkerframework. + * Get checker name from type message in checkerframework. * * @param typeMessage Type message string from checkerframework * @return Checker name from checkerframework e.g. Nullness @@ -306,10 +309,10 @@ private static String getChecker(String typeMessage) { } /** - * Return Kind from diagnosticString in checkerframework. + * Get message kind from type message in checkerframework. * * @param typeMessage Type message string from checkerframework - * @return Lower case kind from checkerframework e.g. use + * @return Lower case message kind from checkerframework e.g. use/declared */ private static String getKind(String typeMessage) { String kindPrefix = "kind="; @@ -327,29 +330,28 @@ private static String getKind(String typeMessage) { } /** - * Return Type from diagnosticString in checkerframework. + * Get type information from type message in checkerframework. * * @param typeMessage Type Message String from checkerframework - * @return Type from checkerframework e.g. @Nullable Object + * @return Type information from checkerframework e.g. @Nullable Object */ private static String getType(String typeMessage) { String typePrefix = "type="; int typeStart = typeMessage.indexOf(typePrefix); if (typeStart != -1) { int typeEnd = typeMessage.indexOf(";", typeStart); - - return typeMessage.substring(typeStart + typePrefix.length(), typeEnd).trim(); + return typeMessage.substring(typeStart + typePrefix.length(), typeEnd).trim() + "; "; } return null; } /** - * Return position from diagnosticString in checkerframework. + * Get position range from type message in checkerframework. * * @param typeMessage Type Message String from checkerframework - * @return Position index from checkerframework e.g. range=(11, 8, 11, 9) + * @return Position range from checkerframework e.g. range=(11, 8, 11, 9) */ - private static String getPosistion(String typeMessage) { + private static String getPosition(String typeMessage) { int lastDelimiter = typeMessage.lastIndexOf(';'); String positionInfo = typeMessage.substring(lastDelimiter + 1).trim(); return positionInfo; From 80e227efa857acab874bc5949ac0e5046b177941 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 22 Nov 2023 14:05:40 -0500 Subject: [PATCH 05/15] temp for migrate to new laptop --- build.gradle | 4 +- .../languageserver/CFLanguageServer.java | 1 + .../languageserver/CFTextDocumentService.java | 106 ++++++++++++++++++ 3 files changed, 109 insertions(+), 2 deletions(-) diff --git a/build.gradle b/build.gradle index 36547dd..9ba410d 100644 --- a/build.gradle +++ b/build.gradle @@ -38,13 +38,13 @@ shadowJar { } tasks.compileJava { - options.compilerArgs += ['-Xlint', '-Werror'] +// options.compilerArgs += ['-Xlint', '-Werror'] } spotless { java { googleJavaFormat().aosp() - importOrder('com', 'jdk', 'lib', 'lombok', 'org', 'java', 'javax') + importOrder('com', 'jdk', 'lib', 'lomlspbok', 'org', 'java', 'javax') formatAnnotations() } groovyGradle { diff --git a/src/main/java/org/checkerframework/languageserver/CFLanguageServer.java b/src/main/java/org/checkerframework/languageserver/CFLanguageServer.java index ea3fde8..2acb28d 100644 --- a/src/main/java/org/checkerframework/languageserver/CFLanguageServer.java +++ b/src/main/java/org/checkerframework/languageserver/CFLanguageServer.java @@ -78,6 +78,7 @@ public CompletableFuture initialize(InitializeParams params) { ServerCapabilities capabilities = new ServerCapabilities(); capabilities.setTextDocumentSync(TextDocumentSyncKind.Full); capabilities.setHoverProvider(Boolean.TRUE); + capabilities.setCodeActionProvider(Boolean.TRUE); return CompletableFuture.completedFuture(new InitializeResult(capabilities)); } diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 2929f9d..faf1c82 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -1,9 +1,14 @@ package org.checkerframework.languageserver; +import com.google.common.base.Splitter; import com.google.common.collect.RangeMap; import com.google.common.collect.TreeRangeMap; import org.checkerframework.javacutil.BugInCF; +import org.eclipse.lsp4j.CodeAction; +import org.eclipse.lsp4j.CodeActionKind; +import org.eclipse.lsp4j.CodeActionParams; +import org.eclipse.lsp4j.Command; import org.eclipse.lsp4j.Diagnostic; import org.eclipse.lsp4j.DiagnosticSeverity; import org.eclipse.lsp4j.DidChangeTextDocumentParams; @@ -17,10 +22,18 @@ import org.eclipse.lsp4j.Position; import org.eclipse.lsp4j.PublishDiagnosticsParams; import org.eclipse.lsp4j.Range; +import org.eclipse.lsp4j.TextEdit; +import org.eclipse.lsp4j.WorkspaceEdit; +import org.eclipse.lsp4j.jsonrpc.messages.Either; import org.eclipse.lsp4j.services.TextDocumentService; import java.io.File; +import java.io.IOException; import java.net.URI; +import java.net.URISyntaxException; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Paths; import java.util.ArrayList; import java.util.Collections; import java.util.HashMap; @@ -423,4 +436,97 @@ private void publishTypeMessage(File file, String msg) { currentTypeInfo.put( com.google.common.collect.Range.closed(start, end), typeInfoForPosition); } + + @Override + public CompletableFuture>> codeAction( + CodeActionParams params) { + List> actions = new ArrayList<>(); + for (Diagnostic diagnostic : params.getContext().getDiagnostics()) { + if (!diagnostic.getMessage().contains("lsp.type.information")) { + if (diagnostic.getMessage().contains("dereference.of.nullable")) { + CodeAction codeAction = new CodeAction("Add nullcheck"); + codeAction.setKind(CodeActionKind.QuickFix); + String uri = params.getTextDocument().getUri(); + Range range = params.getRange(); + String str = getContentInRange(uri, range); + List editList = new ArrayList<>(); + TextEdit edit1 = + new TextEdit( + new Range( + new Position( + params.getRange().getStart().getLine(), + params.getRange().getStart().getCharacter()), + new Position( + params.getRange().getEnd().getLine(), + params.getRange().getEnd().getCharacter())), + " if (" + + str + + " != null) {\n" + + " " + + str + + ".toString();\n"); + TextEdit edit2 = + new TextEdit( + new Range( + new Position( + params.getRange().getStart().getLine() + 1, + params.getRange().getStart().getCharacter()), + new Position( + params.getRange().getEnd().getLine(), + params.getRange().getEnd().getCharacter())), + " } else {\n" + + " //TODO: Implement if the variable is null\n" + + " }\n" + + " }"); + editList.add(edit1); + editList.add(edit2); + codeAction.setEdit(new WorkspaceEdit(Collections.singletonMap(uri, editList))); + codeAction.setDiagnostics(Collections.singletonList(diagnostic)); + actions.add(Either.forRight(codeAction)); + } + } else { + break; + } + } + return CompletableFuture.completedFuture(actions); + } + + private static String getContentInRange(String uri, Range range) { + try { + URI uriObject = new URI(uri); + String filePath = Paths.get(uriObject).toFile().getAbsolutePath(); + String fileContent = new String(Files.readAllBytes(Paths.get(filePath)), StandardCharsets.UTF_8); + int startLine = range.getStart().getLine(); + int startCharacter = range.getStart().getCharacter(); + int endLine = range.getEnd().getLine(); + int endCharacter = range.getEnd().getCharacter(); + + List lines = Splitter.onPattern(System.lineSeparator()).splitToList(fileContent); + + StringBuilder textInRange = new StringBuilder(); + for (int i = startLine; i <= endLine; i++) { + String line = lines.get(i); + if (i == startLine) { + if (i == endLine) { + textInRange.append(line.substring(startCharacter, endCharacter)); + } else { + textInRange.append(line.substring(startCharacter)); + textInRange.append(System.lineSeparator()); + } + } else if (i == endLine) { + textInRange.append(line.substring(0, endCharacter)); + } else { + textInRange.append(line); + textInRange.append(System.lineSeparator()); + } + } + + return textInRange.toString(); + } catch (IOException e) { + e.printStackTrace(); + return ""; + } catch (URISyntaxException e) { + throw new RuntimeException(e); + } + } } From 3c756c122e49af26af7924a97577506bb124d520 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Mon, 27 Nov 2023 18:17:10 -0500 Subject: [PATCH 06/15] Fix formatting error --- build.gradle | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle b/build.gradle index 21631ad..9cb30df 100644 --- a/build.gradle +++ b/build.gradle @@ -38,7 +38,7 @@ shadowJar { } tasks.compileJava { -// options.compilerArgs += ['-Xlint', '-Werror'] + options.compilerArgs += ['-Xlint', '-Werror'] } spotless { From 81ba914641c981e8691e7b44566cc3f88f541e6a Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 5 Dec 2023 18:51:05 -0500 Subject: [PATCH 07/15] apply spotless --- .../languageserver/CFTextDocumentService.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 17cc36d..4040808 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -513,13 +513,15 @@ private static String getContentInRange(String uri, Range range) { try { URI uriObject = new URI(uri); String filePath = Paths.get(uriObject).toFile().getAbsolutePath(); - String fileContent = new String(Files.readAllBytes(Paths.get(filePath)), StandardCharsets.UTF_8); + String fileContent = + new String(Files.readAllBytes(Paths.get(filePath)), StandardCharsets.UTF_8); int startLine = range.getStart().getLine(); int startCharacter = range.getStart().getCharacter(); int endLine = range.getEnd().getLine(); int endCharacter = range.getEnd().getCharacter(); - List lines = Splitter.onPattern(System.lineSeparator()).splitToList(fileContent); + List lines = + Splitter.onPattern(System.lineSeparator()).splitToList(fileContent); StringBuilder textInRange = new StringBuilder(); for (int i = startLine; i <= endLine; i++) { From b1845755114f28f99d41e100a55bc26eaaf3dd04 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 28 Feb 2024 13:13:38 -0500 Subject: [PATCH 08/15] Undo unintentional change to build gradle --- build.gradle | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle b/build.gradle index 3af4414..5a9887c 100644 --- a/build.gradle +++ b/build.gradle @@ -56,7 +56,7 @@ tasks.compileJava { spotless { java { googleJavaFormat().aosp() - importOrder('com', 'jdk', 'lib', 'lomlspbok', 'org', 'java', 'javax') + importOrder('com', 'jdk', 'lib', 'lombok', 'org', 'java', 'javax') formatAnnotations() } groovyGradle { From 451231e978ee989d58d8ae972a00e82ef5921ed6 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 28 Feb 2024 13:16:28 -0500 Subject: [PATCH 09/15] Undo code action and leave to new PR --- .../languageserver/CFLanguageServer.java | 1 - .../languageserver/CFTextDocumentService.java | 108 ------------------ 2 files changed, 109 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/CFLanguageServer.java b/src/main/java/org/checkerframework/languageserver/CFLanguageServer.java index 7451b0b..bfcc65f 100644 --- a/src/main/java/org/checkerframework/languageserver/CFLanguageServer.java +++ b/src/main/java/org/checkerframework/languageserver/CFLanguageServer.java @@ -88,7 +88,6 @@ public CompletableFuture initialize(InitializeParams params) { ServerCapabilities capabilities = new ServerCapabilities(); capabilities.setTextDocumentSync(TextDocumentSyncKind.Full); capabilities.setHoverProvider(Boolean.TRUE); - capabilities.setCodeActionProvider(Boolean.TRUE); return CompletableFuture.completedFuture(new InitializeResult(capabilities)); } diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 4040808..1f0bc8f 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -1,14 +1,9 @@ package org.checkerframework.languageserver; -import com.google.common.base.Splitter; import com.google.common.collect.RangeMap; import com.google.common.collect.TreeRangeMap; import org.checkerframework.javacutil.BugInCF; -import org.eclipse.lsp4j.CodeAction; -import org.eclipse.lsp4j.CodeActionKind; -import org.eclipse.lsp4j.CodeActionParams; -import org.eclipse.lsp4j.Command; import org.eclipse.lsp4j.Diagnostic; import org.eclipse.lsp4j.DiagnosticSeverity; import org.eclipse.lsp4j.DidChangeTextDocumentParams; @@ -22,18 +17,10 @@ import org.eclipse.lsp4j.Position; import org.eclipse.lsp4j.PublishDiagnosticsParams; import org.eclipse.lsp4j.Range; -import org.eclipse.lsp4j.TextEdit; -import org.eclipse.lsp4j.WorkspaceEdit; -import org.eclipse.lsp4j.jsonrpc.messages.Either; import org.eclipse.lsp4j.services.TextDocumentService; import java.io.File; -import java.io.IOException; import java.net.URI; -import java.net.URISyntaxException; -import java.nio.charset.StandardCharsets; -import java.nio.file.Files; -import java.nio.file.Paths; import java.util.ArrayList; import java.util.Collections; import java.util.HashMap; @@ -454,99 +441,4 @@ private void publishTypeMessage(File file, String msg) { currentTypeInfo.put( com.google.common.collect.Range.closed(start, end), typeInfoForPosition); } - - @Override - public CompletableFuture>> codeAction( - CodeActionParams params) { - List> actions = new ArrayList<>(); - for (Diagnostic diagnostic : params.getContext().getDiagnostics()) { - if (!diagnostic.getMessage().contains("lsp.type.information")) { - if (diagnostic.getMessage().contains("dereference.of.nullable")) { - CodeAction codeAction = new CodeAction("Add nullcheck"); - codeAction.setKind(CodeActionKind.QuickFix); - String uri = params.getTextDocument().getUri(); - Range range = params.getRange(); - String str = getContentInRange(uri, range); - List editList = new ArrayList<>(); - TextEdit edit1 = - new TextEdit( - new Range( - new Position( - params.getRange().getStart().getLine(), - params.getRange().getStart().getCharacter()), - new Position( - params.getRange().getEnd().getLine(), - params.getRange().getEnd().getCharacter())), - " if (" - + str - + " != null) {\n" - + " " - + str - + ".toString();\n"); - TextEdit edit2 = - new TextEdit( - new Range( - new Position( - params.getRange().getStart().getLine() + 1, - params.getRange().getStart().getCharacter()), - new Position( - params.getRange().getEnd().getLine(), - params.getRange().getEnd().getCharacter())), - " } else {\n" - + " //TODO: Implement if the variable is null\n" - + " }\n" - + " }"); - editList.add(edit1); - editList.add(edit2); - codeAction.setEdit(new WorkspaceEdit(Collections.singletonMap(uri, editList))); - codeAction.setDiagnostics(Collections.singletonList(diagnostic)); - actions.add(Either.forRight(codeAction)); - } - } else { - break; - } - } - return CompletableFuture.completedFuture(actions); - } - - private static String getContentInRange(String uri, Range range) { - try { - URI uriObject = new URI(uri); - String filePath = Paths.get(uriObject).toFile().getAbsolutePath(); - String fileContent = - new String(Files.readAllBytes(Paths.get(filePath)), StandardCharsets.UTF_8); - int startLine = range.getStart().getLine(); - int startCharacter = range.getStart().getCharacter(); - int endLine = range.getEnd().getLine(); - int endCharacter = range.getEnd().getCharacter(); - - List lines = - Splitter.onPattern(System.lineSeparator()).splitToList(fileContent); - - StringBuilder textInRange = new StringBuilder(); - for (int i = startLine; i <= endLine; i++) { - String line = lines.get(i); - if (i == startLine) { - if (i == endLine) { - textInRange.append(line.substring(startCharacter, endCharacter)); - } else { - textInRange.append(line.substring(startCharacter)); - textInRange.append(System.lineSeparator()); - } - } else if (i == endLine) { - textInRange.append(line.substring(0, endCharacter)); - } else { - textInRange.append(line); - textInRange.append(System.lineSeparator()); - } - } - - return textInRange.toString(); - } catch (IOException e) { - e.printStackTrace(); - return ""; - } catch (URISyntaxException e) { - throw new RuntimeException(e); - } - } } From 5c9eeb3bee3c27c341ebd6b73b92d4d900595171 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 28 Feb 2024 13:18:41 -0500 Subject: [PATCH 10/15] Address naming comment --- .../checkerframework/languageserver/CheckerTypeKind.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java b/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java index 08c82aa..ccfa051 100644 --- a/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java +++ b/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java @@ -6,18 +6,18 @@ public class CheckerTypeKind { private String checkername; - private Map TypeKind; + private Map typeKind; CheckerTypeKind(String checkername, Map kindType) { this.checkername = checkername; - this.TypeKind = kindType; + this.typeKind = kindType; } - String getCheckername() { + /*package-private*/ String getCheckername() { return this.checkername; } Map getTypeKind() { - return this.TypeKind; + return this.typeKind; } } From d851dd7f38c8ceaded4fbb211b655fa6860e0663 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 28 Feb 2024 14:28:09 -0500 Subject: [PATCH 11/15] Add javadoc --- .../languageserver/CheckerTypeKind.java | 38 ++++++++++++++----- 1 file changed, 29 insertions(+), 9 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java b/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java index ccfa051..b4cea96 100644 --- a/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java +++ b/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java @@ -2,22 +2,42 @@ import java.util.Map; -/** This class is for processing type message. */ +/** This class is for storing the type information from Checker Framework. */ public class CheckerTypeKind { - private String checkername; + /** The string stores checker name e.g. Nullness, KeyFor. */ + private String checkerName; - private Map typeKind; + /** + * The map stores type information in the key of the map and type kind information e.g. + * used/declared in the value of the map. + */ + private Map typeToKindMap; - CheckerTypeKind(String checkername, Map kindType) { - this.checkername = checkername; - this.typeKind = kindType; + /** + * Constructor for creating the CheckerTypeKind class + * + * @param checkerName checker's name + * @param typeToKindMap type and kind pair + */ + CheckerTypeKind(String checkerName, Map typeToKindMap) { + this.checkerName = checkerName; + this.typeToKindMap = typeToKindMap; } + /** + * Return the name of the checker + * + * @return name of the checker + */ /*package-private*/ String getCheckername() { - return this.checkername; + return this.checkerName; } - Map getTypeKind() { - return this.typeKind; + /** + * Return the type and kind map + * @return type and kind map + */ + Map getTypeToKindMap() { + return this.typeToKindMap; } } From c84507efd548ce86b4648b215ad04ae33f49eefd Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 28 Feb 2024 14:28:24 -0500 Subject: [PATCH 12/15] Refactor code and add comment --- .../languageserver/CFTextDocumentService.java | 119 ++++++++++-------- 1 file changed, 69 insertions(+), 50 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 1f0bc8f..b748b81 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -228,37 +228,70 @@ private Map> processDiagnosticString( String type = getType(message); String positionInfo = getPosition(message); if (positionInfo != null) { - if (!TypeMessage.containsKey(positionInfo)) { - List checkerTypeKinds = new ArrayList<>(); - Map kindType = new HashMap<>(); - kindType.put(type, kind); - checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); - TypeMessage.put(positionInfo, checkerTypeKinds); - } else { - List checkerTypeKinds = TypeMessage.get(positionInfo); - boolean foundChecker = false; - for (CheckerTypeKind checkerTypeKind : checkerTypeKinds) { - if (checkerTypeKind.getCheckername().equals(checker)) { - foundChecker = true; - if (!checkerTypeKind.getTypeKind().containsKey(type)) { - checkerTypeKind.getTypeKind().put(type, kind); - } - break; - } - } - if (!foundChecker) { - Map kindType = new HashMap<>(); - kindType.put(type, kind); - checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); - } - } + // If the position is not in the map, add a new entry. + List checkerTypeKinds = TypeMessage.computeIfAbsent(positionInfo, k -> new ArrayList<>()); + // If the checker is not in the list, add a new entry. + CheckerTypeKind checkerTypeKind = checkerTypeKinds.stream() + .filter(c -> c.getCheckername().equals(checker)) + .findFirst() + .orElseGet(() -> { + CheckerTypeKind newCheckerTypeKind = new CheckerTypeKind(checker, new HashMap<>()); + checkerTypeKinds.add(newCheckerTypeKind); + return newCheckerTypeKind; + }); + // If the type is not in the map, add a new entry. + checkerTypeKind.getTypeToKindMap().putIfAbsent(type, kind); } } else { + // If is not type message, add to diagnostics. diagnostics.add(convertToLSPDiagnostic(diagnostic)); } } return TypeMessage; } +// private Map> processDiagnosticString( +// Map.Entry>> entry, +// List diagnostics) { +// Map> TypeMessage = new HashMap<>(); +// for (javax.tools.Diagnostic diagnostic : entry.getValue()) { +// String message = diagnostic.getMessage(Locale.getDefault()); +// if (message != null && message.contains("lsp.type.information")) { +// String checker = getChecker(message); +// String kind = getKind(message); +// String type = getType(message); +// String positionInfo = getPosition(message); +// if (positionInfo != null) { +// if (!TypeMessage.containsKey(positionInfo)) { +// List checkerTypeKinds = new ArrayList<>(); +// Map kindType = new HashMap<>(); +// kindType.put(type, kind); +// checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); +// TypeMessage.put(positionInfo, checkerTypeKinds); +// } else { +// List checkerTypeKinds = TypeMessage.get(positionInfo); +// boolean foundChecker = false; +// for (CheckerTypeKind checkerTypeKind : checkerTypeKinds) { +// if (checkerTypeKind.getCheckername().equals(checker)) { +// foundChecker = true; +// if (!checkerTypeKind.getTypeToKindMap().containsKey(type)) { +// checkerTypeKind.getTypeToKindMap().put(type, kind); +// } +// break; +// } +// } +// if (!foundChecker) { +// Map kindType = new HashMap<>(); +// kindType.put(type, kind); +// checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); +// } +// } +// } +// } else { +// diagnostics.add(convertToLSPDiagnostic(diagnostic)); +// } +// } +// return TypeMessage; +// } /** * Publish the given type message for the given file in non-verbose mode. @@ -270,34 +303,20 @@ private void publishTypeMessageWithFilter( Map.Entry>> entry, Map> diagnosticString) { for (Map.Entry> typeMessage : diagnosticString.entrySet()) { - String positionInfo = typeMessage.getKey(); + String location = typeMessage.getKey(); for (CheckerTypeKind checkerTypeKind : typeMessage.getValue()) { - if (checkerTypeKind.getTypeKind().entrySet().size() == 1) { - for (Map.Entry typeKind : - checkerTypeKind.getTypeKind().entrySet()) { - StringBuilder typeMessageBuilder = - new StringBuilder(checkerTypeKind.getCheckername()) - .append(": ") - .append(typeKind.getKey()) - .append(positionInfo); - publishTypeMessage( - new File(URI.create(entry.getKey())), - typeMessageBuilder.toString()); - } - } else { - for (Map.Entry typeKind : - checkerTypeKind.getTypeKind().entrySet()) { - StringBuilder typeMessageBuilder = - new StringBuilder(checkerTypeKind.getCheckername()) - .append(" ") - .append(typeKind.getValue()) - .append(":") - .append(typeKind.getKey()) - .append(positionInfo); - publishTypeMessage( - new File(URI.create(entry.getKey())), - typeMessageBuilder.toString()); + Map typeKinds = checkerTypeKind.getTypeToKindMap(); + for (Map.Entry typeKind : typeKinds.entrySet()) { + StringBuilder typeMessageBuilder = + new StringBuilder(checkerTypeKind.getCheckername()); + // If there are more than one type message from a checker, add the kind of type + // e.g. use/declared. If not, collapse the message. + if (typeKinds.size() > 1) { + typeMessageBuilder.append(" ").append(typeKind.getValue()); } + typeMessageBuilder.append(":").append(typeKind.getKey()).append(location); + publishTypeMessage( + new File(URI.create(entry.getKey())), typeMessageBuilder.toString()); } } } From 6d52076d27b6882218a9dd8d864565af001c03de Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 28 Feb 2024 14:33:57 -0500 Subject: [PATCH 13/15] Applied suggestions from IDE --- .../languageserver/CFTextDocumentService.java | 123 +++++++++--------- .../languageserver/CheckerTypeKind.java | 5 +- 2 files changed, 66 insertions(+), 62 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index b748b81..194ed3d 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -227,21 +227,23 @@ private Map> processDiagnosticString( String kind = getKind(message); String type = getType(message); String positionInfo = getPosition(message); - if (positionInfo != null) { - // If the position is not in the map, add a new entry. - List checkerTypeKinds = TypeMessage.computeIfAbsent(positionInfo, k -> new ArrayList<>()); - // If the checker is not in the list, add a new entry. - CheckerTypeKind checkerTypeKind = checkerTypeKinds.stream() - .filter(c -> c.getCheckername().equals(checker)) - .findFirst() - .orElseGet(() -> { - CheckerTypeKind newCheckerTypeKind = new CheckerTypeKind(checker, new HashMap<>()); - checkerTypeKinds.add(newCheckerTypeKind); - return newCheckerTypeKind; - }); - // If the type is not in the map, add a new entry. - checkerTypeKind.getTypeToKindMap().putIfAbsent(type, kind); - } + // If the position is not in the map, add a new entry. + List checkerTypeKinds = + TypeMessage.computeIfAbsent(positionInfo, k -> new ArrayList<>()); + // If the checker is not in the list, add a new entry. + CheckerTypeKind checkerTypeKind = + checkerTypeKinds.stream() + .filter(c -> c.getCheckername().equals(checker)) + .findFirst() + .orElseGet( + () -> { + CheckerTypeKind newCheckerTypeKind = + new CheckerTypeKind(checker, new HashMap<>()); + checkerTypeKinds.add(newCheckerTypeKind); + return newCheckerTypeKind; + }); + // If the type is not in the map, add a new entry. + checkerTypeKind.getTypeToKindMap().putIfAbsent(type, kind); } else { // If is not type message, add to diagnostics. diagnostics.add(convertToLSPDiagnostic(diagnostic)); @@ -249,49 +251,51 @@ private Map> processDiagnosticString( } return TypeMessage; } -// private Map> processDiagnosticString( -// Map.Entry>> entry, -// List diagnostics) { -// Map> TypeMessage = new HashMap<>(); -// for (javax.tools.Diagnostic diagnostic : entry.getValue()) { -// String message = diagnostic.getMessage(Locale.getDefault()); -// if (message != null && message.contains("lsp.type.information")) { -// String checker = getChecker(message); -// String kind = getKind(message); -// String type = getType(message); -// String positionInfo = getPosition(message); -// if (positionInfo != null) { -// if (!TypeMessage.containsKey(positionInfo)) { -// List checkerTypeKinds = new ArrayList<>(); -// Map kindType = new HashMap<>(); -// kindType.put(type, kind); -// checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); -// TypeMessage.put(positionInfo, checkerTypeKinds); -// } else { -// List checkerTypeKinds = TypeMessage.get(positionInfo); -// boolean foundChecker = false; -// for (CheckerTypeKind checkerTypeKind : checkerTypeKinds) { -// if (checkerTypeKind.getCheckername().equals(checker)) { -// foundChecker = true; -// if (!checkerTypeKind.getTypeToKindMap().containsKey(type)) { -// checkerTypeKind.getTypeToKindMap().put(type, kind); -// } -// break; -// } -// } -// if (!foundChecker) { -// Map kindType = new HashMap<>(); -// kindType.put(type, kind); -// checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); -// } -// } -// } -// } else { -// diagnostics.add(convertToLSPDiagnostic(diagnostic)); -// } -// } -// return TypeMessage; -// } + + // private Map> processDiagnosticString( + // Map.Entry>> entry, + // List diagnostics) { + // Map> TypeMessage = new HashMap<>(); + // for (javax.tools.Diagnostic diagnostic : entry.getValue()) { + // String message = diagnostic.getMessage(Locale.getDefault()); + // if (message != null && message.contains("lsp.type.information")) { + // String checker = getChecker(message); + // String kind = getKind(message); + // String type = getType(message); + // String positionInfo = getPosition(message); + // if (positionInfo != null) { + // if (!TypeMessage.containsKey(positionInfo)) { + // List checkerTypeKinds = new ArrayList<>(); + // Map kindType = new HashMap<>(); + // kindType.put(type, kind); + // checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); + // TypeMessage.put(positionInfo, checkerTypeKinds); + // } else { + // List checkerTypeKinds = + // TypeMessage.get(positionInfo); + // boolean foundChecker = false; + // for (CheckerTypeKind checkerTypeKind : checkerTypeKinds) { + // if (checkerTypeKind.getCheckername().equals(checker)) { + // foundChecker = true; + // if (!checkerTypeKind.getTypeToKindMap().containsKey(type)) { + // checkerTypeKind.getTypeToKindMap().put(type, kind); + // } + // break; + // } + // } + // if (!foundChecker) { + // Map kindType = new HashMap<>(); + // kindType.put(type, kind); + // checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); + // } + // } + // } + // } else { + // diagnostics.add(convertToLSPDiagnostic(diagnostic)); + // } + // } + // return TypeMessage; + // } /** * Publish the given type message for the given file in non-verbose mode. @@ -390,8 +394,7 @@ private static String getType(String typeMessage) { */ private static String getPosition(String typeMessage) { int lastDelimiter = typeMessage.lastIndexOf(';'); - String positionInfo = typeMessage.substring(lastDelimiter + 1).trim(); - return positionInfo; + return typeMessage.substring(lastDelimiter + 1).trim(); } /** diff --git a/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java b/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java index b4cea96..5b9bef4 100644 --- a/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java +++ b/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java @@ -5,13 +5,13 @@ /** This class is for storing the type information from Checker Framework. */ public class CheckerTypeKind { /** The string stores checker name e.g. Nullness, KeyFor. */ - private String checkerName; + private final String checkerName; /** * The map stores type information in the key of the map and type kind information e.g. * used/declared in the value of the map. */ - private Map typeToKindMap; + private final Map typeToKindMap; /** * Constructor for creating the CheckerTypeKind class @@ -35,6 +35,7 @@ public class CheckerTypeKind { /** * Return the type and kind map + * * @return type and kind map */ Map getTypeToKindMap() { From 7c33d4bd0d59422a2258964d34498f9f84b7de3e Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 28 Feb 2024 14:36:02 -0500 Subject: [PATCH 14/15] Remove no longer used method --- .../languageserver/CFTextDocumentService.java | 45 ------------------- 1 file changed, 45 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 194ed3d..82c391c 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -252,51 +252,6 @@ private Map> processDiagnosticString( return TypeMessage; } - // private Map> processDiagnosticString( - // Map.Entry>> entry, - // List diagnostics) { - // Map> TypeMessage = new HashMap<>(); - // for (javax.tools.Diagnostic diagnostic : entry.getValue()) { - // String message = diagnostic.getMessage(Locale.getDefault()); - // if (message != null && message.contains("lsp.type.information")) { - // String checker = getChecker(message); - // String kind = getKind(message); - // String type = getType(message); - // String positionInfo = getPosition(message); - // if (positionInfo != null) { - // if (!TypeMessage.containsKey(positionInfo)) { - // List checkerTypeKinds = new ArrayList<>(); - // Map kindType = new HashMap<>(); - // kindType.put(type, kind); - // checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); - // TypeMessage.put(positionInfo, checkerTypeKinds); - // } else { - // List checkerTypeKinds = - // TypeMessage.get(positionInfo); - // boolean foundChecker = false; - // for (CheckerTypeKind checkerTypeKind : checkerTypeKinds) { - // if (checkerTypeKind.getCheckername().equals(checker)) { - // foundChecker = true; - // if (!checkerTypeKind.getTypeToKindMap().containsKey(type)) { - // checkerTypeKind.getTypeToKindMap().put(type, kind); - // } - // break; - // } - // } - // if (!foundChecker) { - // Map kindType = new HashMap<>(); - // kindType.put(type, kind); - // checkerTypeKinds.add(new CheckerTypeKind(checker, kindType)); - // } - // } - // } - // } else { - // diagnostics.add(convertToLSPDiagnostic(diagnostic)); - // } - // } - // return TypeMessage; - // } - /** * Publish the given type message for the given file in non-verbose mode. * From bfaa7debffc57321f45b97a9da82ea50f7c4bc3c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 1 Mar 2024 18:04:27 -0500 Subject: [PATCH 15/15] Add space after : --- .../checkerframework/languageserver/CFTextDocumentService.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 82c391c..b328f0f 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -273,7 +273,7 @@ private void publishTypeMessageWithFilter( if (typeKinds.size() > 1) { typeMessageBuilder.append(" ").append(typeKind.getValue()); } - typeMessageBuilder.append(":").append(typeKind.getKey()).append(location); + typeMessageBuilder.append(": ").append(typeKind.getKey()).append(location); publishTypeMessage( new File(URI.create(entry.getKey())), typeMessageBuilder.toString()); }