Checker Framework Tutorial

1. Run the Example

To begin, open RegexExample.java. This program is called with two arguments; a regular expression and a string. The program prints the text from the string that matches the first capturing group in the regular expression. Run with a valid regular expression and a matching string such as [01]??\d-([0123]??\d)-\d{4}+ 01-24-2013 and then run with an invalid and a matching string one such as [01]??[\d-[0123]??\d-\d{4}+ 01-24-2013 .

java RegexExample [01]??[\d-[0123]??\d-\d{4}+ 01-24-2013
Exception in thread "main" java.util.regex.PatternSyntaxException: Unclosed character class near index 23
[01]??[d-[0123]??d-d{4}+
                       ^
	at java.util.regex.Pattern.error(Pattern.java:1924)
	at java.util.regex.Pattern.clazz(Pattern.java:2493)
	at java.util.regex.Pattern.sequence(Pattern.java:2030)
	at java.util.regex.Pattern.expr(Pattern.java:1964)
	at java.util.regex.Pattern.compile(Pattern.java:1665)
	at java.util.regex.Pattern.(Pattern.java:1337)
	at java.util.regex.Pattern.compile(Pattern.java:1022)
	at RegexExample.main(RegexExample.java:13)
				

The user has made an error by passing in an invalid regular expression; however, good programming style dictates that a user should not see a stack trace.

2. Run Regex Checker

The Regex Checker prevents, at compile-time, use of syntactically invalid regular expressions and access of invalid capturing groups. So, it can be used to catch an invalid regular expression. Next run the Regex Checker to see how it could have spotted this issue at compile time. The checker prints out an "incompatible types" warning, because regex is not of type @Regex String which is required for strings passed to Pattern.compile(). The checker also prints out an "group.count.invalid" warning because no groups are guaranteed to exist.

javacheck -processor org.checkerframework.checker.regex.RegexChecker RegexExample.java
RegexExample.java:13: error: [argument.type.incompatible] incompatible types in argument.
        Pattern pat = Pattern.compile(regex);
                                      ^
  found   : String
  required: @Regex String
RegexExample.java:18: error: [group.count.invalid] invalid groups parameter 1. Only 0 groups are guaranteed to exist for mat.
                System.out.println("Group: " + mat.group(1));
                                                         ^
2 errors

3. Fix the Code

To fix, verify the user input using the RegexUtil.isRegex(String, int) method. You must import org.checkerframework.checker.regex.RegexUtil. Please see the Regex chapter in the manual for a full discussion of RegexUtil class. If it is not a valid regular expression, print an error message and do not check for matches. If it is a valid regular expression, preform as before. It is not necessary to add an annotation to regex because the Regex Checker adds implicit qualifiers. Below are all the changes that need to be made to RegexExample.java to correctly handle the user input.

  import org.checkerframework.checker.regex.RegexUtil;
...
        if (!RegexUtil.isRegex(regex, 1)) {
            System.out.println("Input is not a regular expression \"" + regex
                    + "\": " + RegexUtil.regexException(regex).getMessage());
            System.exit(1);
        }

4. Run the Regex Checker

javacheck -processor org.checkerframework.checker.regex.RegexChecker RegexExample.java

5. Run the Example

Run the program exactly as before to verify that the program prints a user-friendly warning. The invalid regular expression and matching string used before are [01]??[\d-([0123]??\d)-\d{4}+ 01-24-2013 .

java -cp ".:$CHECKERFRAMEWORK/checker/dist/checker.jar" RegexExample  [01]??[\d-\([0123]??\d\)-\d{4}+ 01-24-2013
Input is not a regular expression "[01]??[d-([0123]??d)-d{4}+": Illegal character range near index 9
[01]??[d-([0123]??d)-d{4}+

For a full discussion of this checker, please see the Regex Checker section of the manual.