Merge pull request #31 from kelloggm/merge-with-sri-csl

Unify my fork and this project

README.md

@@ -8,7 +8,7 @@ analysis tools, including:
 
 * [Randoop](https://randoop.github.io/randoop/)
 * [Bixie](http://sri-csl.github.io/bixie/)
-* [Checker Framework](http://types.cs.washington.edu/checker-framework/)
+* the [Checker Framework](https://checkerframework.org/)
 
 `do-like-javac` supports projects built with:
 
@@ -111,6 +111,37 @@ You will also need Daikon built and installed somewhere, with the environment va
 
     dljc --lib path/to/libs/ -t dyntrace -- mvn compile
 
+Checker Framework whole-program inference
+---------
+
+The Checker Framework's whole-program inference tool will iteratively type-check your
+program using the specified Checker Framework checker until the set of annotations reaches
+a fix-point (note that this process may not terminate). You will need the Checker Framework's
+`checker.jar` file. An example of invoking this tool might look like this:
+
+    dljc --lib path/to/checker.jar -t wpi --checker org.checkerframework.checker.nullness.NullnessChecker -- ./gradlew compileJava
+
+The `--checker` option is usually required. Its argument is the name(s) of the checker you want to run, separated by commas
+(identically to the standard syntax used by the -processor argument to javac). If no `--checker` argument is supplied,
+then the classpath will be searched for annotation processors using javac's standard annotation processor discovery
+mechanism; from the javac documentation:
+> The search path can be specified with the -processorpath option. If no path is specified, then the user
+> class path is used. Processors are located by means of service provider-configuration files named
+> `META-INF/services/javax.annotation.processing.Processor` on the search path. Such files should
+> contain the names of any annotation processors to be used, listed one per line.
+
+This tool also supports some other tool-specific optional arguments:
+* `--stubs /path/to/stubs` tells the checker to run with the specified stub files.
+* `--ajava /path/to/ajava` tells the checker to run with the specified ajava files.
+* `--jdkVersion 8/11/17` tells the Checker Framework to run using JDK8, JDK11, or JDK17..
+* `--quals /path/to/qual.jar` tells the Checker Framework where to find qualifiers (annotations) to put on the classpath.
+* `--extraJavacArgs='-AcustomArg1 -AcustomArg2'` passes the given arguments to invocations of `javac` that run
+  a Checker Framework checker as an annotation processor (i.e., the arguments are NOT passed to the `javac` used while
+  building the target project without running the analysis). This option is intended for Checker Framework options,
+  such as `-AassumeSideEffectFree` or
+  [others documented in the Checker Framework manual](https://checkerframework.org/manual/#checker-options), but you
+  can also use it to pass standard `javac` options (e.g. [those documented by Oracle](
+  https://docs.oracle.com/javase/8/docs/technotes/tools/windows/javac.html)).
 
 LICENSE
 =======

do_like_javac/arg.py

@@ -57,6 +57,14 @@ def __call__(self, parser, namespace, values, option_string=None):
                         # default='NullnessChecker',
                         help='A checker to check (for checker/inference tools)')
 
+base_group.add_argument('--stubs', metavar='<stubs>',
+                        action=AbsolutePathAction,
+                        help='Location of stub files to use for the Checker Framework')
+
+base_group.add_argument('--ajava', metavar='<ajava>',
+                        action=AbsolutePathAction,
+                        help='Location of ajava files to use for the Checker Framework')
+
 base_group.add_argument('-l', '--lib', metavar='<lib_dir>',
                         action='store',dest='lib_dir',
                         help='Library directory with JARs for tools that need them.')
@@ -65,6 +73,15 @@ def __call__(self, parser, namespace, values, option_string=None):
                         action='store',
                         help='Version of the JDK to use with the Checker Framework.')
 
+base_group.add_argument('--quals', metavar='<quals>',
+                        action='store',
+                        help='Path to custom annotations to put on the classpath when using the Checker Framework.')
+
+base_group.add_argument('--extraJavacArgs', metavar='<extraJavacArgs>',
+                        action='store',
+                        help='List of extra arguments to pass to javac when running a Checker Framework checker. Use this for '
+                             'arguments that are only needed when running a checker, such as -AassumeSideEffectFree.')
+
 def split_args_to_parse():
     split_index = len(sys.argv)
     if CMD_MARKER in sys.argv:

do_like_javac/capture/generic.py

@@ -7,6 +7,8 @@
 
 def is_switch(s):
     return s != None and s.startswith('-')
+def is_switch_first_part(s):
+    return s != None and s.startswith('-') and ("=" not in s)
 
 ## brought this from github.com/kelloggm/do-like-javac
 def is_switch_first_part(s):
@@ -101,8 +103,7 @@ def javac_parse(self, javac_command):
 
             if is_switch(a):
                 possible_switch_arg = False
-
-            if a.endswith('.java'):
+            elif a.endswith('.java'):
                 files.append(a)
                 possible_switch_arg = False
 

do_like_javac/capture/mvn.py

@@ -6,19 +6,24 @@
 # additional grant of patent rights can be found in the PATENTS_Facebook file
 # in the same directory.
 
+import os
 import re
 
 from . import generic
 
-supported_commands = ['mvn']
+supported_commands = ['mvn', 'mvnw']
 
 def gen_instance(cmd, args):
     return MavenCapture(cmd, args)
 
 class MavenCapture(generic.GenericCapture):
     def __init__(self, cmd, args):
         super(MavenCapture, self).__init__(cmd, args)
-        self.build_cmd = ['mvn', '-X', '-B'] + cmd[1:]
+        self.build_cmd = [cmd[0], '-X', '-B'] + cmd[1:]
+
+        # Automatically promote to mvnw if available
+        if os.path.exists('mvnw'):
+          self.build_cmd[0] = './mvnw'
 
     def get_target_jars(self, verbose_output):
         jar_pattern = '[INFO] Building jar: '

do_like_javac/tools/__init__.py

@@ -1,10 +1,11 @@
 # import soot
 from . import (bixie, check, chicory, dyntrace, dyntracecounts, graphtools,
-               infer, jprint, randoop)
+               infer, jprint, randoop, wpi)
 
 TOOLS = {
   # 'soot'      : soot,
   'checker'   : check,
+  'wpi'       : wpi,
   'inference' : infer,
   'print'     : jprint,
   'randoop'   : randoop,

do_like_javac/tools/check.py

@@ -46,22 +46,70 @@ def get_arguments_by_version(jdk_version, other_args = None):
 
 def run(args, javac_commands, jars):
     # checker-framework javac.
-    javacheck = os.environ['CHECKERFRAMEWORK'] + "/checker/bin/javac"
-    checker_command = [javacheck, "-processor", args.checker]
-
-    checker_command += get_arguments_by_version(args.jdkVersion)
+    javacheck = os.environ['CHECKERFRAMEWORK']+"/checker/bin/javac"
+    if args.checker is not None:
+        checker_command = [
+            javacheck,
+            "-processor", args.checker,
+            "-Astubs=" + str(args.stubs),
+            "-Aajava=" + str(args.ajava)
+        ]
+    else:
+        # checker should run via auto-discovery
+        checker_command = [javacheck, "-Astubs=" + str(args.stubs),
+                           "-Aajava=" + str(args.ajava)]
+
+    checker_command += getArgumentsByVersion(args.jdkVersion)
 
     for jc in javac_commands:
+        ## What is the point of this pprint command, whose result is not used?
         pprint.pformat(jc)
         javac_switches = jc['javac_switches']
         cp = javac_switches['classpath']
 
+        if args.quals:
+            cp += args.quals + ':'
+        paths = ['-classpath', cp]
+        pp = ''
+        if 'processorpath' in javac_switches:
+            pp = javac_switches['processorpath'] + ':'
         if args.lib_dir:
-            cp += args.lib_dir + ':'
-
-        java_files = ' '.join(jc['java_files'])
-        cmd = checker_command + ["-classpath", cp, java_files]
-
-        print("Running command", " ".join(cmd))
-
+            cp += pp + args.lib_dir + ':'
+        java_files = jc['java_files']
+        cmd = checker_command + ["-classpath", cp] + java_files
         common.run_cmd(cmd, args, 'check')
+
+## other_args is other command-line arguments to javac
+def getArgumentsByVersion(jdkVersion, other_args=[]):
+    if jdkVersion is not None:
+        version = int(jdkVersion)
+    else:
+        version = 8
+    # add arguments depending on requested JDK version (default 8)
+    result = []
+    if version == 8:
+        result += ['-J-Xbootclasspath/p:' + os.environ['CHECKERFRAMEWORK'] + '/checker/dist/javac.jar']
+    elif version == 11 or version >= 16:
+        release_8 = False
+        for i, str in enumerate(other_args):
+            if str == '--release' and other_args[i+1] == "8":
+                release_8 = True
+        if not release_8:
+            # Avoid javac "error: option --add-opens not allowed with target 1.8"
+            if version == 11:
+                result += ['-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED']
+            elif version >= 16:
+                result += ['-J--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED',
+                           '-J--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED',
+                           '-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED',
+                           '-J--add-opens=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED',
+                           '-J--add-opens=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED',
+                           '-J--add-opens=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED',
+                           '-J--add-opens=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED',
+                           '-J--add-opens=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED',
+                           '-J--add-opens=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED']
+
+    else:
+        raise ValueError("the Checker Framework only supports Java versions 8, 11 and 17")
+
+    return result

do_like_javac/tools/common.py

@@ -60,6 +60,7 @@ def run_cmd(cmd, args=None, tool=None):
   # timer = None
   out = None
   out_file = None
+  # Without quoting, empty arguments don't appear in friendly_cmd
   friendly_cmd = ' '.join("'" + elt + "'" for elt in cmd)
 
   if args and args.verbose and args.log_to_stderr: