From f5c0f8c645082b1f439d2e69c3a1f05b957c4a3c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 3 Sep 2023 23:29:36 -0400 Subject: [PATCH 01/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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 57e14a2be601798e2cbc862766c686b3d122f081 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 22 Mar 2024 01:03:41 -0400 Subject: [PATCH 08/11] Stash simplify type information and keep only quick fix --- build.gradle | 2 +- .../languageserver/CFTextDocumentService.java | 175 +----------------- .../languageserver/CheckerTypeKind.java | 23 --- 3 files changed, 10 insertions(+), 190 deletions(-) delete mode 100644 src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java 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 { diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 4040808..f82d928 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -215,177 +215,20 @@ 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)); - } - } - - /** - * 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 = 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)); - } - } - } - } 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 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()); - } + 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())); + publishTypeMessage(file, message); } 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()); - } + diagnostics.add(convertToLSPDiagnostic(diagnostic)); } } - } - } - - /** - * Get checker name from type message 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; - } - - /** - * Get message kind from type message in checkerframework. - * - * @param typeMessage Type message string from checkerframework - * @return Lower case message kind from checkerframework e.g. use/declared - */ - 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; - } - /** - * Get type information from type message in checkerframework. - * - * @param typeMessage Type Message String from checkerframework - * @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() + "; "; + server.publishDiagnostics(new PublishDiagnosticsParams(entry.getKey(), diagnostics)); } - return null; - } - - /** - * Get position range from type message in checkerframework. - * - * @param typeMessage Type Message String from checkerframework - * @return Position range from checkerframework e.g. range=(11, 8, 11, 9) - */ - private static String getPosition(String typeMessage) { - int lastDelimiter = typeMessage.lastIndexOf(';'); - String positionInfo = typeMessage.substring(lastDelimiter + 1).trim(); - return positionInfo; } /** @@ -549,4 +392,4 @@ private static String getContentInRange(String uri, Range range) { throw new RuntimeException(e); } } -} +} \ No newline at end of file diff --git a/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java b/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java deleted file mode 100644 index 08c82aa..0000000 --- a/src/main/java/org/checkerframework/languageserver/CheckerTypeKind.java +++ /dev/null @@ -1,23 +0,0 @@ -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 bf8f696b6eebacf40143c212d8a835bd8477c213 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 22 Mar 2024 15:07:25 -0400 Subject: [PATCH 09/11] Refactor code --- .../languageserver/CFTextDocumentService.java | 66 ++++++++----------- 1 file changed, 26 insertions(+), 40 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index f82d928..18a4177 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -299,50 +299,12 @@ private void publishTypeMessage(File file, String msg) { } @Override - public CompletableFuture>> codeAction( - CodeActionParams params) { + 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)); + CodeAction codeAction = createNullCheckCodeAction(params, diagnostic); actions.add(Either.forRight(codeAction)); } } else { @@ -352,6 +314,30 @@ public CompletableFuture>> codeAction( return CompletableFuture.completedFuture(actions); } + private CodeAction createNullCheckCodeAction(CodeActionParams params, Diagnostic diagnostic) { + 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)); + return codeAction; + } + private static String getContentInRange(String uri, Range range) { try { URI uriObject = new URI(uri); From 74529c7f511996689f7ce40568bc838dbe9e68dc Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 22 Mar 2024 16:48:34 -0400 Subject: [PATCH 10/11] Reset up and add NPE quick fix --- .../languageserver/CFTextDocumentService.java | 97 +++---------------- ...ullPointerDereferenceQuickFixProvider.java | 78 +++++++++++++++ .../quickfix/QuickFixProvider.java | 86 ++++++++++++++++ .../quickfix/QuickFixRegistry.java | 52 ++++++++++ 4 files changed, 230 insertions(+), 83 deletions(-) create mode 100644 src/main/java/org/checkerframework/languageserver/quickfix/NullPointerDereferenceQuickFixProvider.java create mode 100644 src/main/java/org/checkerframework/languageserver/quickfix/QuickFixProvider.java create mode 100644 src/main/java/org/checkerframework/languageserver/quickfix/QuickFixRegistry.java diff --git a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java index 18a4177..bff21ba 100644 --- a/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java +++ b/src/main/java/org/checkerframework/languageserver/CFTextDocumentService.java @@ -1,12 +1,13 @@ 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.checkerframework.languageserver.quickfix.NullPointerDereferenceQuickFixProvider; +import org.checkerframework.languageserver.quickfix.QuickFixProvider; +import org.checkerframework.languageserver.quickfix.QuickFixRegistry; 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; @@ -22,18 +23,11 @@ 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; @@ -80,9 +74,14 @@ public class CFTextDocumentService implements TextDocumentService, Publisher { private final Map>> filesToTypeInfo = new HashMap<>(); + /** The quick fix registry for the Checker Framework document service. */ + QuickFixRegistry quickFixRegistry = new QuickFixRegistry(); + /** Default constructor for Checker Framework document service. */ CFTextDocumentService(CFLanguageServer server) { this.server = server; + quickFixRegistry.registerProvider( + "dereference.of.nullable", new NullPointerDereferenceQuickFixProvider()); } /** Setter for the executor field. */ @@ -299,83 +298,15 @@ private void publishTypeMessage(File file, String msg) { } @Override - public CompletableFuture>> codeAction(CodeActionParams params) { + 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 = createNullCheckCodeAction(params, diagnostic); - actions.add(Either.forRight(codeAction)); - } - } else { - break; + QuickFixProvider provider = quickFixRegistry.getProvider(diagnostic); + if (provider != null && provider.canHandle(diagnostic)) { + actions.addAll(provider.getQuickFixes(diagnostic, params)); } } return CompletableFuture.completedFuture(actions); } - - private CodeAction createNullCheckCodeAction(CodeActionParams params, Diagnostic diagnostic) { - 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)); - return codeAction; - } - - 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); - } - } -} \ No newline at end of file +} diff --git a/src/main/java/org/checkerframework/languageserver/quickfix/NullPointerDereferenceQuickFixProvider.java b/src/main/java/org/checkerframework/languageserver/quickfix/NullPointerDereferenceQuickFixProvider.java new file mode 100644 index 0000000..39b615e --- /dev/null +++ b/src/main/java/org/checkerframework/languageserver/quickfix/NullPointerDereferenceQuickFixProvider.java @@ -0,0 +1,78 @@ +package org.checkerframework.languageserver.quickfix; + +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.Position; +import org.eclipse.lsp4j.Range; +import org.eclipse.lsp4j.TextEdit; +import org.eclipse.lsp4j.WorkspaceEdit; +import org.eclipse.lsp4j.jsonrpc.messages.Either; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +/** Quick fix provider for null pointer dereference diagnostics. */ +public class NullPointerDereferenceQuickFixProvider implements QuickFixProvider { + /** + * Check if the provider can handle a diagnostic. + * + * @param diagnostic the diagnostic + * @return true if the provider can handle the diagnostic + */ + @Override + public boolean canHandle(Diagnostic diagnostic) { + return diagnostic.getMessage().contains("dereference.of.nullable"); + } + + /** + * Get the quick fixes for a diagnostic. + * + * @param diagnostic the diagnostic + * @param params the code action parameters + * @return the quick fixes + */ + @Override + public List> getQuickFixes( + Diagnostic diagnostic, CodeActionParams params) { + CodeAction codeAction = new CodeAction("Add null check"); + codeAction.setKind(CodeActionKind.QuickFix); + String uri = params.getTextDocument().getUri(); + Range range = params.getRange(); + String str = QuickFixProvider.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)); + List> code = new ArrayList<>(); + code.add(Either.forRight(codeAction)); + return code; + } +} diff --git a/src/main/java/org/checkerframework/languageserver/quickfix/QuickFixProvider.java b/src/main/java/org/checkerframework/languageserver/quickfix/QuickFixProvider.java new file mode 100644 index 0000000..88a394c --- /dev/null +++ b/src/main/java/org/checkerframework/languageserver/quickfix/QuickFixProvider.java @@ -0,0 +1,86 @@ +package org.checkerframework.languageserver.quickfix; + +import com.google.common.base.Splitter; + +import org.eclipse.lsp4j.CodeAction; +import org.eclipse.lsp4j.CodeActionParams; +import org.eclipse.lsp4j.Command; +import org.eclipse.lsp4j.Diagnostic; +import org.eclipse.lsp4j.Range; +import org.eclipse.lsp4j.jsonrpc.messages.Either; + +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.List; + +/** Interface for quick fix providers. */ +public interface QuickFixProvider { + /** + * Check if the provider can handle a diagnostic. + * + * @param diagnostic the diagnostic + * @return true if the provider can handle the diagnostic + */ + boolean canHandle(Diagnostic diagnostic); + + /** + * Get the quick fixes for a diagnostic. + * + * @param diagnostic the diagnostic + * @param params the code action parameters + * @return the quick fixes + */ + List> getQuickFixes(Diagnostic diagnostic, CodeActionParams params); + + /** + * Get the content in a range. + * + * @param uri the URI of the file + * @param range the range + * @return the content in the range + */ + 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); + } + } +} diff --git a/src/main/java/org/checkerframework/languageserver/quickfix/QuickFixRegistry.java b/src/main/java/org/checkerframework/languageserver/quickfix/QuickFixRegistry.java new file mode 100644 index 0000000..04d3e74 --- /dev/null +++ b/src/main/java/org/checkerframework/languageserver/quickfix/QuickFixRegistry.java @@ -0,0 +1,52 @@ +package org.checkerframework.languageserver.quickfix; + +import org.eclipse.lsp4j.Diagnostic; + +import java.util.HashMap; +import java.util.Map; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +/** Registry for quick fix providers. */ +public class QuickFixRegistry { + /** Map from diagnostic code to quick fix provider. */ + private static final Map providers = new HashMap<>(); + + /** + * Register a quick fix provider for a diagnostic code. + * + * @param diagnosticCode the diagnostic code + * @param provider the quick fix provider + */ + public void registerProvider(String diagnosticCode, QuickFixProvider provider) { + providers.put(diagnosticCode, provider); + } + + /** + * Get the quick fix provider for a diagnostic. + * + * @param diagnostic the diagnostic + * @return the quick fix provider + */ + public QuickFixProvider getProvider(Diagnostic diagnostic) { + return providers.get(extractMessage(diagnostic.getMessage())); + } + + /** + * Extract the message from a diagnostic. Example: "[dereference.of.nullable] ..." -> + * "dereference.of.nullable" + * + * @param input the diagnostic message + * @return the extracted message + */ + private static String extractMessage(String input) { + Pattern pattern = Pattern.compile("\\[([^]]+)\\]"); + Matcher matcher = pattern.matcher(input); + + if (matcher.find()) { + return matcher.group(1); // Returns the first capturing group + } + + return "No match found"; // Or any appropriate default/fallback value + } +} From 226a213628f024d4e920553b5927c87149164797 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 22 Mar 2024 17:36:35 -0400 Subject: [PATCH 11/11] Add suppress warning option --- ...ullPointerDereferenceQuickFixProvider.java | 76 ++++++++++++++----- 1 file changed, 58 insertions(+), 18 deletions(-) diff --git a/src/main/java/org/checkerframework/languageserver/quickfix/NullPointerDereferenceQuickFixProvider.java b/src/main/java/org/checkerframework/languageserver/quickfix/NullPointerDereferenceQuickFixProvider.java index 39b615e..6d07bc0 100644 --- a/src/main/java/org/checkerframework/languageserver/quickfix/NullPointerDereferenceQuickFixProvider.java +++ b/src/main/java/org/checkerframework/languageserver/quickfix/NullPointerDereferenceQuickFixProvider.java @@ -12,6 +12,7 @@ import org.eclipse.lsp4j.jsonrpc.messages.Either; import java.util.ArrayList; +import java.util.Arrays; import java.util.Collections; import java.util.List; @@ -43,36 +44,75 @@ public List> getQuickFixes( String uri = params.getTextDocument().getUri(); Range range = params.getRange(); String str = QuickFixProvider.getContentInRange(uri, range); - List editList = new ArrayList<>(); - TextEdit edit1 = + int startLine = range.getStart().getLine(); + int startCharacter = range.getStart().getCharacter(); + int endLine = range.getEnd().getLine(); + int endCharacter = range.getEnd().getCharacter(); + TextEdit editBefore = new TextEdit( new Range( - new Position( - params.getRange().getStart().getLine(), - params.getRange().getStart().getCharacter()), - new Position( - params.getRange().getEnd().getLine(), - params.getRange().getEnd().getCharacter())), + new Position(startLine, startCharacter), + new Position(endLine, endCharacter)), " if (" + str + " != null) {\n" + " " + str + ".toString();\n"); - TextEdit edit2 = + TextEdit editAfter = 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())), + new Position(startLine + 1, startCharacter), + new Position(endLine, endCharacter)), " } 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.setEdit(createWorkspaceEdit(uri, editBefore, editAfter)); codeAction.setDiagnostics(Collections.singletonList(diagnostic)); List> code = new ArrayList<>(); code.add(Either.forRight(codeAction)); + code.add(Either.forRight(addSuppressWarning(diagnostic, params))); return code; } + + /** + * Add a suppress warning quick fix. + * + * @param diagnostic the diagnostic + * @param params the code action parameters + * @return the code action + */ + public CodeAction addSuppressWarning(Diagnostic diagnostic, CodeActionParams params) { + CodeAction codeAction = new CodeAction("Suppress nullness warning"); + codeAction.setKind(CodeActionKind.QuickFix); + String uri = params.getTextDocument().getUri(); + Range range = params.getRange(); + String str = QuickFixProvider.getContentInRange(uri, range); + TextEdit suppressWarningEdit = createSuppressWarningEdit(str, params.getRange()); + codeAction.setEdit(createWorkspaceEdit(uri, suppressWarningEdit)); + codeAction.setDiagnostics(Collections.singletonList(diagnostic)); + return codeAction; + } + + /** + * Create a SuppressWarningEdit. + * + * @param str the string to insert + * @param range the range + * @return the text edit + */ + private TextEdit createSuppressWarningEdit(String str, Range range) { + return new TextEdit( + new Range( + new Position(range.getStart().getLine(), range.getStart().getCharacter()), + new Position(range.getEnd().getLine(), range.getEnd().getCharacter())), + "@SuppressWarnings(\"nullness\")\n" + " " + str); + } + + /** + * Create a workspace edit. + * + * @param uri the URI of the file + * @param edits the text edits + * @return the workspace edit + */ + private WorkspaceEdit createWorkspaceEdit(String uri, TextEdit... edits) { + return new WorkspaceEdit(Collections.singletonMap(uri, Arrays.asList(edits))); + } }