Saffire is a static analysis program that detects bugs in programs that use the OCaml/C foreign function interface. Saffire works by performing type inference across both OCaml and C to make sure that values are used consistently across the language boundary. For instance, if a OCaml passes a record to a C function, that C function should not treat the data as an integer. Saffire also tracks what C variables point into the OCaml heap and ensure they are always registered with CAMLparam/local before any allocation functions are called.
In the OCaml FFI, C is able to view OCaml data at a very low level and a single C value could represent several OCaml types. For instance, the value Val_int(0) could represent ():unit or false:bool since they are represented identically in memory. C programs also perform pattern matching using tag tests and compute offsets into OCaml data blocks.
Saffire analyzes a program using a combination of dataflow analysis and type inference with representational types, which are based on the physical representation of a type in memory. The analysis tracks what possible integer elements (unboxed data) a type could have, and the size and shape of the boxed (pointer) data.
The first step in Saffire's analysis is to parse OCaml source files and pull out all of the external definitions. Saffire records these in an offline store and later converts all of the OCaml types into representational types. Next, Saffire parses the C source code and performs type inference and dataflow analysis to determine the representational types used there. The types from the first step are used as a starting point for C functions declared external in OCaml. A more complete description of Saffire is described in our upcoming PLDI paper.
Saffire is currently only a proof of concept implementation and does not handle every corner of the OCaml grammar. If you find that Saffire can't handle your code, drop me an email and I'll try to add support for it. Most common constructs and operations are supported:
In order to build Saffire, just run
./configure
make
The FFI type checker does not currently support installing into another location at this time. Therefore you have to use it from within its build directory.
To do this, simply add the bin/ directory in the build tree to
your path:
export PATH=$PATH:/path/to/saffire-cil/bin
Here is the basic overview of how to use our tool:
Shipped in the bin directory are several wrappers that attempt to make using the tool a little easier.
oc.wrap is used to wrap any calls to ocamlc or ocamlopt that are used for compilation. Therefore if your makefile has a target which uses "ocamlc," it should be replaced with "oc.wrap ocamlc." If your project builds both byte code and native code, it is only necessary to wrap one of the compilers, although wrapping them both won't create any problems. Additionally, it is not necessary to wrap any calls to ocamlc when it is used purely for linking (although doing so won't hurt).
mklibwrap is a wrapper around the OCaml utility ocamlmklib, that can be useful for creating mixed OCaml/C libraries. Therefore, if you use ocamlmklib, it should be replaced by "mklibwrap ocamlmklib" in your build environment.
saffire is used in place of your regular C compiler. Therefore any references to gcc or cc should be replaced with 'saffire' (NOT 'saffire gcc'). This includes using gcc as either a compiler or linker (ie: for creating shared libraries).
"saffire --mode=AR" is used to wrap the archive tool ar. If your project uses ar to create static C libraries, you must replace a line like:
ar cr libfoo.a obj1.o obj2.o ...
with
saffire --mode=AR cr libfoo.a obj1.o obj2.o ...
As an example, download this program. Then follow these steps to analyze it:
Saffire produced two errors in "saffire.checks" for this code. The first error is because f1 is passed a pair of integers, but treats them as a single integer. The second error is because the variable w points to the pair of integers passed to f2. If the call to caml_alloc() were to cause a garbage collection, this value may be moved and the location stored in w would not be updated. Note that v2 is now shown in the error message because it is not live at the call to indirect_alloc().
warning, global value decl: ...
Any and all global values produce this warning.
imprecision: unknown offset in ptr arithmetic: ((value*)equation +p i)
Issued when the analysis can not determine the offset into a memory block at compile time
Example:
func(value x, int y) { value v = Field(x,y); }
unify NoConstructors with Infinity
Issued when a boxed value is treated as an unboxed value
Example:
external f : (int*int) -> unit = "g"
value g(value v) { int z = Int_val(v); }
unify NoConstructors with some Constructors
Issued when an unboxed value is treated as a boxed value
Example:
external f : int -> unit = "g"
value g(value v) { value w = Field(v,0); }
one of these types is explicitly unboxed while the other has boxed elements
Issued when two types successfully unify their unboxed elements, but one has no boxed elements and the other does.
unify rep with custom failed: int <> Repr(Infinity,None)
Issued when a value is cast directly to an integer
Example:
g(value x) { int y = (int)x; }
non-pointer type in (value) cast
Issued when using an C type which is not a pointer (ie: the bottom bit could be 1)
Example:
g(int x) { value v = x; }
direct arithmetic operations on value type
Issued when arithmetic is performed on a OCaml value without a call to Int_val first.
Example:
func(value v) { long z = v + 2; }
arity mismatch. Expecting a function with sig:
t1 -> t2 -> t3 -> unit
but got instead:
x -> y -> z
Issued when the functions don't take the same number of arguments