Merge branch 'devel'

.gitignore

@@ -8,4 +8,5 @@ bin/
 build/
 cov-int/
 **/*.log
-*.txt
+*.txt
+*.pyc

README.md

@@ -10,7 +10,7 @@
 
 Check our the **[Online Demo](http://csl.sri.com/projects/bixie/)**.
 
-Bixie is a static analysis tool that detects inconsistencies in Java bytecode. An inconsistency occurs if code must throw an exception or is unreachable because because of assumptions made by other statements. 
+Bixie is a static analysis tool that detects inconsistencies in Java bytecode. An inconsistency occurs when code must throw an exception or is unreachable because because of assumptions made by other statements. 
 
 ##### Examples
 
@@ -27,28 +27,31 @@ In this example from Cassandra:
 		return identityDistribution.next() % 1 == 0;
 	}
 
-There is an inconsistency in the bytecode because the expression `identityDistribution.next() % 1 == 0` appears as a conditional choice in the bytecode where one case is unreachable because `identityDistribution.next() % 1` returns a constant value.
+There is an inconsistency in the bytecode because the expression `identityDistribution.next() % 1 == 0` appears as a conditional choice in the bytecode, and one case is unreachable because `identityDistribution.next() % 1` returns a constant value.
 
 
-#### Build instructions:
+#### Build instructions
 
 Bixie uses gradle to build:
 
 	git clone https://github.com/SRI-CSL/bixie.git
 	cd bixie
     ./gradlew shadowJar
 
-#### Usage example:
+#### Usage example
 To check if everything is working, run Bixie on itself:
 
 	cd build/libs/
 	java -jar bixie.jar -j ../classes/main/
 
-#### Soundness remarks:
-Bixie is not sound. Many Java features, such as concurrency and reflection, are not handled by Bixie and may result in false alarms. Bixie also sometimes detects inconsistencies in the bytecode that have no corresponding inconsistency in the source code. For example, conditional choices with conjunctions in the condition sometimes raise false alarms.
-
-
-
+#### Bixie runner
+For your convenience, there is a Python script (runner/runner.py) that will automatically determine what classpaths to use and where class files are generated, and then invoke Bixie. It works for projects built with ant, maven, or gradle. For example:
 
+	cd <path-to-project>
+	mvn clean
+	python <path-to-bixie>/runner/runner.py -- mvn compile
 
+This command will execute the maven build process for the project and scrape its output for instances where javac was called, then feed that information to Bixie. Be sure to clean before building, as the tool can only detect files that were actually compiled while it is observing.
 
+#### Soundness remarks
+Bixie is not sound. Many Java features, such as concurrency and reflection, are not handled by Bixie and may result in false alarms. Bixie also sometimes detects inconsistencies in the bytecode that have no corresponding inconsistency in the source code. For example, conditional choices with conjunctions in the condition sometimes raise false alarms.

build.gradle

@@ -69,7 +69,6 @@ buildscript {
 
     dependencies {
         classpath 'org.kt3k.gradle.plugin:coveralls-gradle-plugin:2.0.1'
-        classpath 'net.ltgt.gradle:gradle-errorprone-plugin:latest.release'
         classpath 'com.github.jengelman.gradle.plugins:shadow:1.2.2'
     }
 }
@@ -92,28 +91,40 @@ dependencies {
 
 
 // building the jar ---------------------
+
 jar {
   println("WARNING: jar does not create an executable jar. Use shadowJar instead.")
-  baseName = 'bixie'
+  	baseName = 'bixie'
+
+    from configurations.compile.collect { it.isDirectory() ? it : zipTree(it) }
+
+    from('src/main/resources'){ include('log4j.properties')}
+  	from('src/main/resources'){ include('basic_prelude.bpl')}
+  	from('src/main/resources'){ include('java_lang.bpl')}
 
+
+
     manifest {
         attributes 'Main-Class': mainClassName,
                    'Class-Path': '.',
                    'Implementation-Title': 'Bixie',
                    'Implementation-Version': version
     }
+}
 
-    from('src/main/resorces'){ include('log4j.properties')}
-
-    from configurations.compile.collect { it.isDirectory() ? it : zipTree(it) }
+shadowJar {
+  	append('src/main/resources/report_html.zip')
 }
 
-jar.dependsOn shadowJar
+
+//jar.dependsOn shadowJar
 
 // testing related activities -----------------
 tasks.withType(FindBugs) {
-    effort = "default"
+    effort = "max"
     reportLevel = "medium"
+
+	findbugs.excludeFilter = file("$rootProject.projectDir/config/findbugs/excludeFilter.xml")
 
     reports {
         xml.enabled = false

config/findbugs/excludeFilter.xml

@@ -0,0 +1,7 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<FindBugsFilter>
+  <Match>
+    <Package name="~bixie\.boogie\..*"/>
+  </Match>
+
+</FindBugsFilter>

runner/arg.py

@@ -0,0 +1,95 @@
+import argparse
+import os
+import sys
+import imp
+
+# token that identifies the end of the options for infer and the beginning
+# of the compilation command
+CMD_MARKER = '--'
+
+# insert here the correspondence between module name and the list of
+# compiler/build-systems it handles.
+# All supported commands should be listed here
+MODULE_TO_COMMAND = {
+    'ant': ['ant'],
+    'gradle': ['gradle', 'gradlew'],
+    'mvn': ['mvn']
+}
+
+CAPTURE_PACKAGE = 'capture'
+DEFAULT_JAR_LOCATION = os.path.abspath(
+  os.path.join (os.path.dirname(__file__),
+                os.pardir,
+                'build',
+                'libs',
+                'bixie.jar'))
+
+class AbsolutePathAction(argparse.Action):
+    """Convert a path from relative to absolute in the arg parser"""
+    def __call__(self, parser, namespace, values, option_string=None):
+        setattr(namespace, self.dest, os.path.abspath(values))
+
+base_parser = argparse.ArgumentParser(add_help=False)
+base_group = base_parser.add_argument_group('global arguments')
+base_group.add_argument('-o', '--out', metavar='<directory>',
+                        dest='output_directory',
+                        action=AbsolutePathAction,
+                        help='Set the results directory')
+base_group.add_argument('--jar', action=AbsolutePathAction,
+                        help='The location of the bixie jar file.',
+                        default=DEFAULT_JAR_LOCATION)
+
+base_group.add_argument(
+    CMD_MARKER,
+    metavar='<cmd>',
+    dest='nullarg',
+    default=None,
+    help=('Command to run the compiler/build-system.'),
+)
+
+def get_module_name(command):
+    """ Return module that is able to handle the command. None if
+    there is no such module."""
+    for module, commands in MODULE_TO_COMMAND.iteritems():
+        if command in commands:
+            return module
+    return None
+
+def split_args_to_parse():
+    dd_index = \
+        sys.argv.index(CMD_MARKER) if CMD_MARKER in sys.argv else len(sys.argv)
+
+    args, cmd = sys.argv[1:dd_index], sys.argv[dd_index + 1:]
+    capture_module_name = os.path.basename(cmd[0]) if len(cmd) > 0 else None
+    mod_name = get_module_name(capture_module_name)
+    return args, cmd, mod_name
+
+def load_module(mod_name):
+    # load the 'capture' package in lib
+    pkg_info = imp.find_module(CAPTURE_PACKAGE)
+    imported_pkg = imp.load_module(CAPTURE_PACKAGE, *pkg_info)
+    # load the requested module (e.g. make)
+    mod_file, mod_path, mod_descr = \
+        imp.find_module(mod_name, imported_pkg.__path__)
+    try:
+        return imp.load_module(
+            '{pkg}.{mod}'.format(pkg=imported_pkg.__name__, mod=mod_name),
+            mod_file, mod_path, mod_descr)
+    finally:
+        if mod_file:
+            mod_file.close()
+
+def parse_args():
+    to_parse, cmd, mod_name = split_args_to_parse()
+    # get the module name (if any), then load it
+    imported_module = None
+    if mod_name:
+        imported_module = load_module(mod_name)
+
+    args = base_parser.parse_args(to_parse)
+
+    if imported_module:
+        return args, cmd, imported_module
+    else:
+        base_parser.print_help()
+        sys.exit(os.EX_OK)

runner/capture/ant.py

@@ -0,0 +1,54 @@
+# Copyright (c) 2015 - present Facebook, Inc.
+# All rights reserved.
+#
+# This source code is licensed under the BSD style license found in the
+# LICENSE file in the root directory of this source tree. An additional grant
+# of patent rights can be found in the PATENTS file in the same directory.
+
+import util
+import generic
+
+def gen_instance(cmd):
+    return AntCapture(cmd)
+
+class AntCapture(generic.GenericCapture):
+
+    def __init__(self, cmd):
+        self.build_cmd = ['ant', '-verbose'] + cmd[1:]
+
+    def is_interesting(self, content):
+        return self.is_quoted(content) or content.endswith('.java')
+
+    def is_quoted(self, argument):
+        quote = '\''
+        return len(argument) > 2 and argument[0] == quote\
+            and argument[-1] == quote
+
+    def remove_quotes(self, argument):
+        if self.is_quoted(argument):
+            return argument[1:-1]
+        else:
+            return argument
+
+    def get_javac_commands(self, verbose_output):
+        javac_pattern = '[javac]'
+        argument_start_pattern = 'Compilation arguments'
+        javac_arguments = []
+        javac_commands = []
+        collect = False
+        for line in verbose_output:
+            if javac_pattern in line:
+                if argument_start_pattern in line:
+                    collect = True
+                    if javac_arguments != []:
+                        javac_commands.append(javac_arguments)
+                        javac_arguments = []
+                if collect:
+                    pos = line.index(javac_pattern) + len(javac_pattern)
+                    content = line[pos:].strip()
+                    if self.is_interesting(content):
+                        arg = self.remove_quotes(content)
+                        javac_arguments.append(arg)
+        if javac_arguments != []:
+            javac_commands.append(javac_arguments)
+        return map(self.javac_parse, javac_commands)

runner/capture/generic.py

@@ -0,0 +1,45 @@
+import util
+
+def is_switch(s):
+    return s != None and s.startswith('-')
+
+class GenericCapture:
+    def __init__(self, cmd):
+        self.build_cmd = cmd
+
+    def get_javac_commands(self, verbose_output):
+        return []
+
+    def capture(self):
+        build_output = util.get_build_output(self.build_cmd)
+        javac_commands = self.get_javac_commands(build_output)
+        return javac_commands
+
+    def javac_parse(self, javac_command):
+        files = []
+        switches = {}
+
+        prev_arg = None
+
+        for a in javac_command:
+            possible_switch_arg = True
+
+            if is_switch(a):
+                possible_switch_arg = False
+
+            if a.endswith('.java'):
+                files.append(a)
+                possible_switch_arg = False
+
+            if is_switch(prev_arg):
+                if possible_switch_arg:
+                    switches[prev_arg[1:]] = a
+                else:
+                    switches[prev_arg[1:]] = True
+
+            if is_switch(a):
+                prev_arg = a
+            else:
+                prev_arg = None
+
+        return dict(java_files=files, javac_switches=switches)

runner/capture/gradle.py

@@ -0,0 +1,28 @@
+# Copyright (c) 2015 - present Facebook, Inc.
+# All rights reserved.
+#
+# This source code is licensed under the BSD style license found in the
+# LICENSE file in the root directory of this source tree. An additional grant
+# of patent rights can be found in the PATENTS file in the same directory.
+
+import util
+import generic
+
+def gen_instance(cmd):
+    return GradleCapture(cmd)
+
+class GradleCapture(generic.GenericCapture):
+
+    def __init__(self, cmd):
+        self.build_cmd = [cmd[0], '--debug'] + cmd[1:]
+
+    def get_javac_commands(self, verbose_output):
+        argument_start_pattern = ' Compiler arguments: '
+        results = []
+
+        for line in verbose_output:
+            if argument_start_pattern in line:
+                content = line.partition(argument_start_pattern)[2].strip()
+                results.append(content.split(' '))
+
+        return map(self.javac_parse, results)

runner/capture/mvn.py

@@ -0,0 +1,43 @@
+# Copyright (c) 2015 - present Facebook, Inc.
+# All rights reserved.
+#
+# This source code is licensed under the BSD style license found in the
+# LICENSE file in the root directory of this source tree. An additional grant
+# of patent rights can be found in the PATENTS file in the same directory.
+
+import re
+import util
+import generic
+
+def gen_instance(cmd):
+    return MavenCapture(cmd)
+
+class MavenCapture(generic.GenericCapture):
+    def __init__(self, cmd):
+        self.build_cmd = ['mvn', '-X'] + cmd[1:]
+
+    def get_javac_commands(self, verbose_output):
+        file_pattern = r'\[DEBUG\] Stale source detected: ([^ ]*\.java)'
+        options_pattern = '[DEBUG] Command line options:'
+
+        javac_commands = []
+        files_to_compile = []
+        options_next = False
+
+        for line in verbose_output:
+            if options_next:
+                #  line has format [Debug] <space separated options>
+                javac_args = line.split(' ')[1:] + files_to_compile
+                javac_commands.append(javac_args)
+                options_next = False
+                files_to_compile = []
+            elif options_pattern in line:
+                #  Next line will have javac options to run
+                options_next = True
+
+            else:
+                found = re.match(file_pattern, line)
+                if found:
+                    files_to_compile.append(found.group(1))
+
+        return map(self.javac_parse, javac_commands)