| <!DOCTYPE html> |
| <html> |
| <head> |
| <meta name="generator" content= |
| "HTML Tidy for Linux (vers 25 March 2009), see www.w3.org"> |
| |
| <title>Checker Framework Tutorial - Validating User Input - Command |
| Line</title> |
| <link href="bootstrap/css/bootstrap.css" rel="stylesheet" type= |
| "text/css"> |
| <script type="text/javascript" src="bootstrap/js/bootstrap.min.js"> |
| </script> |
| <link href="css/main.css" rel="stylesheet" type="text/css"> |
| <link rel="icon" type="image/png" href= |
| "https://checkerframework.org/favicon-checkerframework.png"> |
| </head> |
| |
| <body> |
| <div class="top_liner"></div> |
| |
| <div class="navbar navbar-inverse navbar-fixed-top" style= |
| "border-bottom: 1px solid #66d;"> |
| <div class="navbar-inner"> |
| <div class="contained"> |
| <ul class="nav"> |
| <li class="heading">Checker Framework:</li> |
| |
| <li><a href="https://checkerframework.org/">Main Site</a></li> |
| |
| <li><a href= |
| "https://checkerframework.org/manual/"> |
| Manual</a></li> |
| |
| <li><a href= |
| "https://groups.google.com/forum/#!forum/checker-framework-discuss"> |
| Discussion List</a></li> |
| |
| <li><a href= |
| "https://github.com/typetools/checker-framework/issues">Issue |
| Tracker</a></li> |
| |
| <li><a href= |
| "https://github.com/typetools/checker-framework">Source |
| Code</a></li> |
| |
| <li class="active"><a href= |
| "https://checkerframework.org/tutorial/">Tutorial</a></li> |
| </ul> |
| </div> |
| </div> |
| </div><img src="https://checkerframework.org/CFLogo.png" alt="Checker Framework logo"> |
| |
| <div class="page-header short" style= |
| "border-bottom: 1px solid #EEE; border-top: none;"> |
| <h1>Checker Framework Tutorial</h1> |
| |
| <h2><small>Previous <a href="get-started-cmd.html">Getting |
| Started</a></small></h2> |
| </div> |
| |
| <div id="introduction"> |
| <div class="page-header short" style="border-top: none;"> |
| <h2>Validating User Input</h2> |
| </div> |
| |
| <p>This part of the tutorial shows how the Checker Framework can |
| detect and help correct missing input validation.</p> |
| |
| <div class="section"> |
| <div class="well"> |
| <h5>Outline</h5> |
| |
| <ol> |
| <li><a href="#regexexample">The RegexExample program</a></li> |
| |
| <li><a href="#runex1">Run the example with an invalid regular |
| expression</a></li> |
| |
| <li><a href="#run1">Run the Regex Checker to see how it could |
| have prevented the runtime error</a></li> |
| |
| <li><a href="#validate">Validate the user input</a></li> |
| |
| <li><a href="#run2">Run the Regex Checker to verify that the |
| error is corrected</a></li> |
| |
| <li><a href="#runex2">Run the example with an invalid regular |
| expression to see the warning</a></li> |
| </ol> |
| </div> |
| </div> |
| |
| <div class="section"> |
| <div id="regexexample"> |
| <h4>1. The RegexExample program</h4> |
| |
| <p>If you have not already done so, download |
| <a href="../sourcefiles.zip">the source files</a> for the tutorial. |
| </p> |
| |
| <p> |
| The <a href="../src/RegexExample.java">RegexExample.java</a> |
| 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. |
| <br/><b>Compile the program</b>: |
| </p> |
| <pre> |
| $ <strong>javac RegexExample.java</strong> |
| </pre> |
| </div> |
| |
| <div id="runex1"> |
| <h4>2. Run the RegexExample program</h4> |
| |
| <p><b>Run the program</b> with a <strong class= |
| "text-success">valid</strong> regular expression and a matching |
| string: |
| </p> |
| <pre> |
| $ <strong>java RegexExample '[01]?\d-([0123]?\d)-\d{4}+' '01-24-2013'</strong> |
| Group 1: 24 |
| </pre> |
| |
| <p><b>Run the program</b> with an <strong class= |
| "text-error">invalid</strong> regular expression and any |
| string:</p> |
| <pre> |
| $ <strong>java RegexExample '[01]?[\d-[0123]?\d-\d{4}+' '01-24-2013'</strong> |
| Exception in thread "main" java.util.regex.PatternSyntaxException: Unclosed character class near index 24 |
| [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.<init>(Pattern.java:1337) |
| at java.util.regex.Pattern.compile(Pattern.java:1022) |
| at RegexExample.main(RegexExample.java:13) |
| </pre> |
| |
| <p>Good programming style dictates that the user should not see a |
| stack trace, even if the user supplies invalid output.</p> |
| </div> |
| |
| <div id="run1"> |
| <h4>3. Run the Regex Checker</h4> |
| |
| <p>The Regex Checker prevents, at compile time, use of |
| syntactically invalid regular expressions and access of invalid |
| capturing groups. In other words, it prevents you from writing code |
| that would throw certain exceptions at run time. Next <b>run the Regex |
| Checker</b> to see how it could have spotted this issue at compile |
| time. |
| </p> |
| <pre> |
| $ <strong>javacheck -processor org.checkerframework.checker.regex.RegexChecker RegexExample.java</strong> |
| RegexExample.java:13: error: [argument] incompatible types in argument. |
| Pattern pat = Pattern.compile(regex); |
| ^ |
| found : String |
| required: @Regex String |
| 1 errors |
| </pre> |
| |
| <p>The "incompatible types" warning indicates that variable |
| <code>regex</code> is not of type <code>@Regex String</code> which |
| is required for strings passed to <a href="https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/util/regex/Pattern.html#compile(java.lang.String)"><code>Pattern.compile()</code></a>.</p> |
| </div> |
| |
| <div id="validate"> |
| <h4>4. Fix the Code</h4> |
| |
| <p>The right way to fix the problems is for the code to issue a |
| user-friendly message at run time. It should <b>verify the user |
| input</b> using the |
| <a href="https://checkerframework.org/api/org/checkerframework/checker/regex/RegexUtil.html#isRegex-java.lang.String-"><code>RegexUtil.isRegex(String, int)</code></a> method. |
| If the string is not a valid regular |
| expression, it should <b>print an error message and halt</b>. |
| If it <em>is</em> a valid regular expression, perform as before. |
| </p> |
| |
| <p> |
| You need to make two changes to <code>RegexExample.java</code> |
| to correctly handle invalid user input. At the top of the file, add</p> |
| <pre> |
| import org.checkerframework.checker.regex.RegexUtil; |
| </pre> |
| <p> |
| After variable <code>regex</code> is defined but before it is |
| used (that is, before <code>Pattern pat = Pattern.compile(regex);</code>), add</p> |
| <pre> |
| if (!RegexUtil.isRegex(regex, 1)) { |
| System.out.println("Input is not a regular expression \"" + regex |
| + "\": " + RegexUtil.regexException(regex).getMessage()); |
| System.exit(1); |
| } |
| </pre> |
| </div> |
| |
| <div id="run2"> |
| <h4>5. Re-run the Regex Checker</h4> |
| |
| <pre> |
| $ <strong>javacheck -processor org.checkerframework.checker.regex.RegexChecker RegexExample.java</strong> |
| </pre> |
| |
| <p>There should be no warnings. This shows that the code will not |
| throw a PatternSyntaxException at compile time.</p> |
| </div> |
| |
| <div id="runex2"> |
| <h4>6. Run the Example</h4> |
| |
| <p>Run the program as before (but adding <code>checker-qual.jar</code> to the classpath) |
| to verify that the program |
| prints a user-friendly warning.</p> |
| <pre> |
| $ <strong>java -cp ".:$CHECKERFRAMEWORK/checker/dist/checker-qual.jar" RegexExample '[01]?[\d-\([0123]?\d\)-\d{4}+' '01-24-2013'</strong> |
| Input is not a regular expression "[01]?[d-([0123]?d)-d{4}+": Illegal character range near index 24 |
| </pre> |
| |
| <p>For a full discussion of the Regex Checker, please see the <a href= |
| "https://checkerframework.org/manual/#regex-checker"> |
| Regex Checker chapter</a> of the Checker Framework manual.</p> |
| </div> |
| </div> |
| </div> |
| |
| <div id="next"> |
| <div class="page-header short"> |
| <h2><small>Next, try <a href="security-error-cmd.html">Finding a |
| Security Error</a>, a complex example using the Tainting |
| Checker.</small></h2> |
| </div> |
| </div><!-- |
| <div class="bottom_liner well"> |
| <a href="#">Top</a> |
| </div> |
| --> |
| <!-- LocalWords: Plugin plugin VM SDK plugins quals classpath |
| --> |
| <!-- LocalWords: NullnessChecker plugin's hg |
| --> |
| </body> |
| </html> |
