Missile: An Interactive Tool for Modular Verification with Fissile Type Analysis

Devin Coughlin and Bor-Yuh Evan Chang

Missile is a plugin for the clang static analyzer that enables programmers to modularly specify and verify almost-everywhere invariants—invariants that generally hold but that programmers violate temporarily—with dependent refinement types in C and Objective-C.

News

Downloads

Bugs

Instructions

Missile requires OS X 10.8, Xcode 4.6, and z3.

Download Contents

The download tarball contains 6 items:

plugin_source/

This contains an Xcode project with the source of our plugin for the clang static analyzer. Perhaps the most interesting parts here are MethodReflectionTypeChecker.{cpp,h}, which contains our flow-insensitive analysis and SymbolicChecker.{cpp,h}, which contains our path-sensitive symbolic analysis.

2. benchmarks/

The benchmarks directory contains 9 Objective-C benchmarks which we have used to verify the safety of reflective method calls. We provide each of these benchmarks in their original, unaltered form and also with our annotations.

Of particular interest may be the TestCommandLineTool Xcode project in this directory, which contains a large number of tests for Missile. The ShouldAllPass target contains tests that should pass the flow-sensitive analysis (i.e., without the ability to switch to the symbolic analysis). The ShouldAllFail target contains tests that should fail the intertwined flow-insensitive/symbolic analysis and the ShouldAllPassSymbolic target contains tests that should pass the intertwined analysis.

The benchmark/run_benchmarks_cav.rb script contains the ruby script we used to generate the data.

data-cav-2014.tar.gz

This is a tarball of our logs from running the experiments for our CAV 2014 submission experiments, which we provide to aid reproduction. Be warned: uncompressed, it is larger than 3GB.

plugin_bin/

This directory contains a binary version of the plugin.

build/

The build directory contains binaries for our custom version of clang; adding support for new __attribute__ annotations required small modifications to the clang frontend.

Clang LLVM 1.0.xcspec

This file is a *modified* version of an Xcode configuration file that tells Xcode to use the custom version of clang and the Missile plugin.

CAV-demo/

This directory contains a simple Xcode project with the two examples from our CAV submission.

Instructions for Running


Step 1: Install Xcode 4.6, if you do not already have it.

Step 2: Modify the Missile version of Clang LLVM 1.0.xcspec:

Modify the 'Clang LLVM 1.0.xcspec' file to change the DefaultValue value of the option with name MISSILE_INSTALL_PATH (grep in the file for this) to the absolute path of your untar'd missile directory.

Step 3: Make a backup of the version of this file in the Xcode bundle:

'/Applications/Xcode.app/Contents/PlugIns/Xcode3Core.ideplugin/Contents/SharedSupport/Developer/Library/Xcode/Plug-ins/Clang LLVM 1.0.xcplugin/Contents/Resources/Clang LLVM 1.0.xcspec'

Step 4: Replace the version of that file in Xcode with your modified version.

Step 5: Install libz3.dylib in /usr/local/lib

Step 6: Double-click CAV-demo/CAV/CAV.xcodeproj

Step 7: Use Xcode to build the project (Product > Build)

Step 8: If all went well, you should see 'Global invariant could not be restored' in CallbackV2.m. Click on it (in the editor pane) to see the visualization.

You can now muck around with CAV.xcodeproj (or benchmarks/TestCommandLineTool/TestCommandLineTool.xcodeproj ) to explore the tool.