Support for general assertion frameworks

[wmdietl]

There are several frameworks that provide methods that take a boolean and throw an exception if the boolean is false. Instead of:

assert value != null && value.something(): "@AssumeAssertion(nullness)"

one might write:

Verify.verify(value != null && value.something());

Using Google Guava as an example: https://github.com/google/guava/blob/master/guava/src/com/google/common/base/Verify.java#L98

Methods like Verify.verifyNotNull https://github.com/google/guava/blob/master/guava/src/com/google/common/base/Verify.java#L137 can be annotated to require a non-null argument. (This was done in commit typetools/guava@eda5f9c .)

Methods that take an arbitrary boolean should similarly be annotatable somehow.
One possibility

@ThrowsIf(expression="#1", result=false, exception=VerifyException.class)
public static void verify(boolean expression);

or maybe as a generalization of the existing https://github.com/typetools/checker-framework/blob/master/dataflow/src/org/checkerframework/dataflow/qual/TerminatesExecution.java

@TerminatesExecutionIf(expression="#1", result=false)
public static void verify(boolean expression);

For assert we provide command-line flags to select whether they should be assumed enabled or disabled and require a special marker message "@AssumeAssertion(nullness)".
This flexibility doesn't seem necessary for such libraries.

Implementing the logic for these new specifications should be easily generalizable from the existing handling of assert.

[mernst]

Guava doesn't call Verify.verify (not even to test it), and doesn't call Verify.verifyNotNull except to test it. Is there a client (preferably one that is already annotated) that uses these, to help validate the design and implementation?

[mernst]

#2076 is more important and useful than this issue, and #2076 is also much easier to implement.

We are still not sure whether Verify.verify and Verify.verifyNotNull are used in the wild.

[Stephan202]

In our code base (worked on by 100+ developers) Guava's Verify.verify, Preconditions.checkArgument and Preconditions.checkState are used quite extensively; at scale their simpler syntax starts to matter quite a bit. Support for such methods would be very nice.

Since I already prepared example code before finding this ticket, I'll leave it here as a(nother) motivating example. Consider this code:

$ cat -n Dummy.java 
     1	import static com.google.common.base.Preconditions.checkArgument;
     2	
     3	import java.util.regex.Pattern;
     4	import org.checkerframework.checker.regex.RegexUtil;
     5	
     6	final class Dummy {
     7	  Pattern compile1(String input) {
     8	    checkArgument(RegexUtil.isRegex(input), "Pattern '%s' is not a valid regex", input);
     9	    return Pattern.compile(input);
    10	  }
    11	
    12	  Pattern compile2(String input) {
    13	    if (!RegexUtil.isRegex(input)) {
    14	      throw new IllegalArgumentException(String.format("Pattern '%s' is not a valid regex", input));
    15	    }
    16	    return Pattern.compile(input);
    17	  }
    18	}

These two methods are functionally equivalent, but the RegexChecker flags only the first (while it shouldn't flag either):

$ javac \
    -J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED \
    -processorpath ~/.m2/repository/org/checkerframework/checker/3.8.0/checker-3.8.0.jar \
    -cp $HOME/.m2/repository/com/google/guava/guava/30.0-j
re/guava-30.0-jre.jar:$HOME/.m2/repository/org/checkerframework/checker-qual/3.8.0/checker-qual-3.8.0.jar \
    -processor org.checkerframework.checker.regex.RegexChecker \
    Dummy.java
Dummy.java:9: error: [argument.type.incompatible] incompatible argument for parameter regex of compile.
    return Pattern.compile(input);
                           ^
  found   : String
  required: @Regex String
1 error

shell returned 1

[mernst]

Stephan, thank you for our first confirmation that these methods are used in the wild. I appreciate it, and that enables us to increase the priority of this issue.

For people not familiar with these Guava interfaces, all three behave the same, but they are intended to be called in different circumstances.

• Preconditions.checkArgument is for discovering that a caller passed an illegal argument.
• Preconditions.checkState maybe checks whether the receiver's internal state is corrupted. (The documentation uses the undefined term "calling instance".)
• Verify.verify is intended to be used in all other circumstances.

In your example, could you rewrite method compile1 as follows?

  Pattern compile1(@Regex String input) {
    checkArgument(RegexUtil.isRegex(input), "Pattern '%s' is not a valid regex", input);
    return Pattern.compile(input);
  }

That puts the method specification where it belongs (on the formal parameter type), while still providing run-time checks, and while suffering no false positives.

I realize that doesn't handle Verify.verify, but it does handle the example you gave, so maybe it is sufficient for your purposes.

[Stephan202]

@mernst thanks for the quick response. While in general a good idea, in my specific case adding @Regex just "pushes the problem away", with the Checker Framework then flagging the call site. What I failed to mention is that in my concrete case the method input comes from Error Prone's ErrorProneFlags#get, which indeed may return any arbitrary string (since it's user input).

[mernst]

From your description, it sounds like issuing a warning at the call site is the right thing, since the warning is a true positive.

I suspect I'm missing something. Do you want your routine to take any input, and to throw an exception if the input is not a regular expression? It would be helpful if you could expand your example to a use case where writing @Regex on the formal parameter is not desirable.

[Stephan202]

From your description, it sounds like issuing a warning at the call site is the right thing, since the warning is a true positive.

In the absence of the RegexUtil.isRegex check, that's correct. But with the RegexUtil.isRegex guard in place I should be able to write the code such that no warning is emitted. The if variant indeed avoids the warning, while the equivalent checkArgument variant doesn't.

Do you want your routine to take any input, and to throw an exception if the input is not a regular expression?

That's correct: I can't prevent the user from making a mistake, so the next best thing is to throw a helpful exception when they do. As a result Pattern.compile never receives invalid input, which in turn means that no warning should be emitted.

It would be helpful if you could expand your example to a use case where writing @Regex on the formal parameter is not desirable.

Hmm, I wonder whether we have different expectations about when @Regex is suitable. "Somewhere" I need to translate the user input from "String" to "@Regex String or exception". IIUC, whatever method holds said logic should not require an @Regex input, since it has well-defined/appropriate behavior on malformed inputs. Of course, one could add @Regex anyway, but then the code at the call site will be flagged.

Put another way: as a user I'd expect there to be "some" way to take arbitrary-but-well-formed user input and pass it to Pattern.compile without triggering a compiler warning.

[mernst]

Thank you for the explanation. That is very helpful. I believe I now understand where our perspectives differ.

When I write a program, I consider any user-visible exception to be a bug in the program.
If the user makes a mistake, the program should issue a helpful message and terminate gracefully.
Throwing a user-visible exception is not as helpful. Not only is it scary and confusing, it also lacks important information. In your example, it lacks the specific file and line number from which the user string was read.

Your perspective is different: You don't want the Checker Framework to prevent all exceptions caused by illegal regular expressions. Rather, you want to guarantee that such exceptions only occur at certain source-code constructs (namely, Preconditions.checkArgument).

A few more notes about my perspective, where I think we agree:

• Not all exceptions are evil: within a program, it may be useful to throw and catch exceptions to centralize the code that prints helpful messages and terminates gracefully. But I don't want the user to ever see them.
• Every string that will be passed to Pattern.compile should be annotated as @Regex, whether it came from the user or not. I now see that does not include the formal parameter of your copmile1 and compile2 methods, because of their contract "If the argument is a regular expression, compile it; otherwise throw an exception". That contract was not clear to me before.

I'd like to find a way to make the Checker Framework support your use case. I have a few questions first.

Question 1. Did I accurately characterize your point of view and the contract of the compile1 method?

Question 2. If you are OK with throwing an exception, could you use the asRegex method rather than calling checkArgument?

This code:

return Pattern.compile(RegexUtil.asRegex(input));

is even shorter and simpler than your version:

checkArgument(RegexUtil.isRegex(input), "Pattern '%s' is not a valid regex", input);
return Pattern.compile(input);

and you mentioned that concision was your reason for preferring checkArgument over if.

Question 3. Can you suppress the warning? That is the recommended approach when there are just a few potential exceptions that you don't want the Checker Framework to warn you about. Your compile1 method whose contract is "If the argument is a regular expression, compile it; otherwise throw an exception" is an example of this. You could write @SuppressWarnings on it, and you probably wouldn't need to write @SuppressWarnings anywhere else. That is how asRegex() is implemented.

Maybe these suggestions don't handle all your uses of checkArgument, but they do seem to handle the one we are talking about. Feel free to continue educating me by fleshing out your use case. Thanks again!

[Stephan202]

Hi @mernst. Apologies for my slow response; it's been a busy week. Going over your questions:

1. Yes, I agree with that characterization :). One observation: there seem to be cases where a "scary exception message" is the best we can do. The concrete case in which this issue came up is an Error Prone plugin, and there isn't really a friendly way to inform the user that they provided a malformed flag. (Only logging something would very likely make the issue go unnoticed, and silently refusing operation isn't better.)
2. Nice; this works for me. I somehow overlooked this method. In my specific case I don't care too much about the precise exception message, so it's fine to let the error thrown by RegexUtil.asRegex bubble up. That said, if I put on my puristic hat then this method does come with a flaw: it throws an Error, which is not a type one should generally use when rejecting (user) input. (Nor should one generally catch it "further up" the call stack.) I can see how Error makes sense from CF's perspective as a "this should not happen if the program is correct" case, but here I'd use it to cover a "the user is holding it wrong and this can totally happen" case.
3. Yep, when I filed this issue (and before I knew about RegexUtil.asRegex) indeed I went for @SuppressWarnings. The reason I wasn't really satisfied with that solution is that (a) my use case felt "common enough" and (b) it forced me to refactor the code a bit so that I could apply the suppression to a minimal scope.

Thanks a lot for all the help; while I feel that Preconditions/Verify support would still be very helpful (if only because they are semantically equivalent to an explicit if-statement, which is supported) I can work with RegexUtil.asRegex. 👍