Add method to deal with matrix and fix comment

[LoiNguyenCS]

Professor @kelloggm, I have updated the removing curly braces method that we discussed, I have also changed the way to ignore comments, instead of finding the index of "\ ", I check if it's in a string literal. However, I am receiving some warnings from Checker Framework. Please help me take a look. Thank you.

 C:\Users\nguye\Desktop\wpi-paper-main\experiments\inferred-annos-counter\app\src\main\java\org\checkerframework\wholeprograminference\inferredannoscounter\InferredAnnosCounter.java:336: error: [argument] incompatible argument for parameter Index of checkInString.
      if (checkInString(indexOfClose, result)){
                        ^
  found   : @LTEqLengthOf("result") int
  required: @LTLengthOf("result") int 
  
  
C:\Users\nguye\Desktop\wpi-paper-main\experiments\inferred-annos-counter\app\src\main\java\org\checkerframework\wholeprograminference\inferredannoscounter\InferredAnnosCounter.java:369: error: [argument] incompatible argument for parameter Index of checkInString.
      } else if (checkInString(indexDash, line)) {
                               ^
  found   : @LTEqLengthOf("line") int
  required: @LTLengthOf("line") int

[kelloggm]

Notes/suggestions on what to do about Index Checker warnings.

[kelloggm]

This Javadoc comment should explain why we need to do this - i.e., what the problem was with how we were doing it before.

[LoiNguyenCS]

Professor, I have modified the codes based on your second approach. I have updated the checkInString method to throw an exception if the index given is not valid. I think this approach will make the whole program more logically connected than suppressing a warning. Please take a look. Thank you.

[kelloggm]

Adding dynamic index checking to these methods is a clever way to subvert the Index Checker, but it doesn't actually make our code that much safer: we will just get a RuntimeException instead of an IndexOutOfBoundsException if there is an invalid index. That would still cause the program to crash, which is undesirable.

It is more useful to try to avoid passing a bad index into these routines rather than crashing if such an index is passed in.

[kelloggm]

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).

[LoiNguyenCS]

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?

[LoiNguyenCS]

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.

[LoiNguyenCS]

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

[kelloggm]

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

[LoiNguyenCS]

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

[LoiNguyenCS]

Professor, I have added some SuppressWarnings statement, but I'm still not able to suppress the warning on line 346. Please help me with this case. Thank you.

Here is the warning that I received:

C:\Users\nguye\Desktop\wpi-paper-main\experiments\inferred-annos-counter\app\src\main\java\org\checkerframework\wholeprograminference\inferredannoscounter\InferredAnnosCounter.java:346: error: [assignment] incompatible types in assignment.
        indexOfClose = result.indexOf("},");
                                     ^
  found   : @LTEqLengthOf("result") int
  required: @LTLengthOf("result") int

[kelloggm]

Professor, I have added some SuppressWarnings statement, but I'm still not able to suppress the warning on line 346. Please help me with this case. Thank you.

Here is the warning that I received:

C:\Users\nguye\Desktop\wpi-paper-main\experiments\inferred-annos-counter\app\src\main\java\org\checkerframework\wholeprograminference\inferredannoscounter\InferredAnnosCounter.java:346: error: [assignment] incompatible types in assignment.
        indexOfClose = result.indexOf("},");
                                     ^
  found   : @LTEqLengthOf("result") int
  required: @LTLengthOf("result") int

This is the same issue (i.e., typetools/checker-framework#5471), but there's no declaration to attach the warning suppression to, because this re-assigns a variable. In this case, the right thing to do is to create a temporary variable with the correct type, and add the warning suppression on its declaration. So, change line 346 to the following:

@SuppressWarnings("index:assignment") // https://github.com/typetools/checker-framework/issues/5471
@LTLengthOf("result") int temp = result.indexOf("},");
indexOfClose = temp;

[kelloggm]

No - it will be closed automatically when my PR is merged. Martin

…

On Wed, Dec 28, 2022, 12:40 PM LoiNguyenCS ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In experiments/inferred-annos-counter/app/src/main/java/org/checkerframework/wholeprograminference/inferredannoscounter/InferredAnnosCounter.java <#34 (comment)>: > */ - private static boolean ***@***.***("#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"); thank you Professor. In that case, should I close the issue that I have made? — Reply to this email directly, view it on GitHub <#34 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA6G5NQM4AI7KCYX7QQE2L3WPR3PXANCNFSM6AAAAAATGHYBQQ> . You are receiving this because you were mentioned.Message ID: ***@***.***>