Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add method to deal with matrix and fix comment #34

Merged
merged 12 commits into from
Jan 9, 2023
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import org.checkerframework.checker.index.qual.IndexFor;

/**
* The entry point for the inferred annos counter. Run this by passing arguments, with the first
Expand Down Expand Up @@ -68,7 +67,7 @@ private static boolean checkGoogleFormatOpenCase(String line) {
}
String elements[] = line.split(" ");
int n = elements.length;
if (n >= 1 && elements[n - 1].contains("@org.checkerframework")) {
if (n >= 1 && elements[n - 1].contains("@org")) {
String breaks[] = elements[n - 1].split("[.]");
int numberOfParts = breaks.length;
if (numberOfParts < 2) {
Expand Down Expand Up @@ -270,18 +269,21 @@ private static int countAnnos(String line) {
* This method checks if a particular index in a line belongs to a string literal
*
* @param line a line
* @param Index index of line
* @return true if Index belong to a string literal, false otherwise
* @param index index of line
* @return false if index belongs to a string literal, true otherwise
*/
private static boolean checkInString(@IndexFor("#2") int Index, String line) {
private static boolean checkInString(int index, String line) {
if (index >= line.length() || index < 0) {
throw new RuntimeException("The index provided for checkInString is not valid");
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While adding this check here isn't a bad thing to do, the specification of checkInString should still be that the index parameter ought to be @IndexFor("#2"): the goal of the checker is to prevent crashes, and the change you've made here just turns an IndexOutOfBoundsException into a RuntimeException.

We should retain the @IndexFor annotation on line 275 above: we still need to deal with the possibility that the index used at some call sites might not be valid (ie, the checker warnings).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Got it. So then I should stick to first approach, which is to suppress the warning and provide a link to the bug report. Is that correct, Professor?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Professor, I tried to build a simple test case for the bug report. But then the test case appeared to work, here is the test case:


import org.checkerframework.checker.index.qual.IndexFor;

public class InferredAnnosCounter
{
  /**
   * This method checks if a particular index in a line belongs to a string literal
   *
   * @param line a line
   * @param index index of line
   * @return false if index belongs to a string literal, true otherwise
   */
  private static boolean checkInString(@IndexFor("#2") int index, String line) {
    int before = 0;
    int after = 0;
    for (int i = 0; i < index; i++) {
      if (line.charAt(i) == '\"') {
        before++;
      }
    }
    for (int i = index + 1; i < line.length(); i++) {
      if (line.charAt(i) == '\"') {
        after++;
      }
    }
    if (before % 2 == 0 && after % 2 == 0) {
      return true;
    }
    return false;
  }

  public static void main(String[] args) {
    String x = "Hello@World, this is our new program";
    int indexToCheck = x.indexOf("d, ");
    if (indexToCheck != -1 && checkInString(indexToCheck, x))
      System.out.println("TRUE");
  }
}

So I guess maybe there're some problems with my codes that I'm not aware of, I will try to investigate more.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

UPDATE: Professor, I have found a test case where we would receive the warning. Here is the test case.

import org.checkerframework.checker.index.qual.IndexFor;
public class SimpleTestCase
{
  private static boolean atTheBeginning(@IndexFor("#2") int index, String line) {
    return (index==0);
  }

  private static boolean hasDoubleQuestionMarkAtTheBeginning (String line) {
    int i = line.indexOf("??");
    if (i!=-1) {
      return (atTheBeginning(i, line));
    }
    return false;
  }

  public static void main(String[] args) {
    String x = "Hello?World, this is our new program";
    if (hasDoubleQuestionMarkAtTheBeginning(x))
      System.out.println("TRUE");
  }
}

and the warning is

return (atTheBeginning(i, line));
                             ^
  found   : @LTEqLengthOf("line") int
  required: @LTLengthOf("line") int

I have made a bug report, here is the link: typetools/checker-framework#5471

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FYI I've fixed the bug, so when we make the next Checker Framework release we'll be able to remove these warning suppressions.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

thank you Professor. In that case, should I close the issue that I have made?

}
int before = 0;
int after = 0;
for (int i = 0; i < Index; i++) {
for (int i = 0; i < index; i++) {
if (line.charAt(i) == '\"') {
before++;
}
}
for (int i = Index + 1; i < line.length(); i++) {
for (int i = index + 1; i < line.length(); i++) {
if (line.charAt(i) == '\"') {
after++;
}
Expand All @@ -292,6 +294,70 @@ private static boolean checkInString(@IndexFor("#2") int Index, String line) {
return false;
}

/**
* This method replaces a particular character at an index of a string with a new symbol.
*
* @param line a line that needs to be modified
* @param index a valid index of that line, which is non-negative and less than the length of line
* @param symbol the new character
* @return the line with the character at index replaced by symbol
*/
private static String replaceAtIndex(String line, int index, String symbol) {
LoiNguyenCS marked this conversation as resolved.
Show resolved Hide resolved
if (index < 0 || index > line.length()) {
throw new RuntimeException("The index provided for replaceAtIndex is not valid");
}
String result = line;
String firstPart = result.substring(0, index);
if (index + 1 < result.length()) {
String secondPart = result.substring(index + 1, result.length());
result = firstPart + symbol + secondPart;
} else // the element at index is also the last element of the string
{
result = firstPart + symbol;
}

return result;
}

/**
* This method formats annotations that contain arguments, such as @EnsuresNonNull("tz1").
* Previously, we had a problem when working with these types of annotations. The
* computer-generated files sometimes put an additional pair of curly braces. Initially, we
* approached this problem by adding a pair of curly braces to every annotation having a pair of
* parentheses but no curly braces. But then we might run into a problem if there are parentheses
* inside the arguments. This new method has two parts. First, we check if the annotation contains
* a matrix and format the matrix if we found one. We format it by changing all "}, {" pattern to
* "|, |". Second, we'll remove all curly braces in that annotation. By this way way, we make sure
* that we will not mess up the important curly braces, otherwise something like ({3, 4}) and
* ({3}, {4}) will both end up being (3,4).
*
* @param annotation an annotation to be formatted
* @return formatted annotation
*/
private static String formatAnnotaionsWithArguments(String annotation) {
String result = annotation;
/*
First, we format cases involving matrix by changing all "}, {" to "|, |"
*/
int indexOfClose = result.indexOf("},");
while (indexOfClose != -1) {
int indexOfOpen = result.indexOf('{', indexOfClose);
if (checkInString(indexOfClose, result)) {
kelloggm marked this conversation as resolved.
Show resolved Hide resolved
result = replaceAtIndex(result, indexOfClose, "|");
result = replaceAtIndex(result, indexOfOpen, "|");
indexOfClose = result.indexOf("},");
} else {
indexOfOpen = result.indexOf("},", indexOfClose + 1);
}
}
/*
Second, we will remove all curly braces
*/
result = result.replace("{", "");
result = result.replace("}", "");
return result;
}

/**
* This method trims out all the comments in a line from the input files
*
Expand All @@ -301,13 +367,13 @@ private static boolean checkInString(@IndexFor("#2") int Index, String line) {
private static String ignoreComment(String line) {
int indexComment = line.length() + 1;
String finalLine = line;
int indexDash = line.indexOf("// ");
int indexDash = line.indexOf("//");
int indexStar = line.indexOf("*");
int indexDashStar = line.indexOf("/*");
if (indexDash != -1) {
if (indexDash == 0) {
finalLine = line.substring(0, indexDash);
} else {
} else if (checkInString(indexDash, line)) {
kelloggm marked this conversation as resolved.
Show resolved Hide resolved
finalLine = line.substring(0, indexDash - 1);
}
}
Expand Down Expand Up @@ -473,15 +539,11 @@ public static void main(String[] args) {
// since it's too difficult to keep the length of whitespace at the beginning of each line the
// same
originalFileLine = originalFileLine.trim();
originalFile.add(originalFileLine);
String specialAnno = trimParen(originalFileLine);
// the fact that this if statement's condition is true means that this line contains exactly
// one CF annotation and nothing else.
if (checkerPackage.contains(specialAnno)) {
if (originalFileLine.contains("(") && !originalFileLine.contains("{")) {
originalFileLine = originalFileLine.replace("(", "({");
originalFileLine = originalFileLine.replace(")", "})");
}
originalFileLine = formatAnnotaionsWithArguments(originalFileLine);
if (annoCount.containsKey(specialAnno)) {
int numberOfAnno = annoCount.get(specialAnno);
annoCount.put(specialAnno, numberOfAnno + 1);
Expand All @@ -492,6 +554,7 @@ public static void main(String[] args) {
// we want the keys in the map annoLocate has this following format: type_position
annoLocate.put(originalFileLine + "_" + originalFileLineIndex, 0);
}
originalFile.add(originalFileLine);
originalFileLineCount = originalFileLineIndex;
}
// Iterate over the arguments from 1 to the end and diff each with the original,
Expand All @@ -506,6 +569,10 @@ public static void main(String[] args) {
List<String> newFile = new ArrayList<>();
for (String ajavaFileLine : inputFileWithEachAnnoOnOneLine2) {
ajavaFileLine = ignoreComment(ajavaFileLine);
// if the condition is true, this line contains only one single annotation and nothing else.
if (ajavaFileLine.contains("@org")) {
ajavaFileLine = formatAnnotaionsWithArguments(ajavaFileLine);
}
ajavaFileLine = extractCheckerPackage(ajavaFileLine);
ajavaFileLine = ajavaFileLine.trim();
newFile.add(ajavaFileLine);
Expand Down