FreeSafeTy

FreeSafeTy (Free is made Safe by Types) is a type-based verifier for safe memory deallocation. FreeSafeTy can verify the following properties on memory usage.

• Lack of memory leak.
• Lack of double free.
• Lack of read/write to deallocated memory cell.

Download

Install

You need GLPK, ocaml-glpk and OMake to install FreeSafeTy. After expanding the downloaded archive, first replace the value of OCAMLGLPKPATH in OMakefile with the path of ocaml-glpk. Then, type omake in the directory. An executable file freesafety will be created.

Usage

To verify a program test.ml, execute ./freesafety test.ml.

Syntax

[program] ::= let rec [fundefs] in [stmt] | [stmt]
[fundefs] ::= [fundef] | [fundef] and [fundefs]
[fundef] ::= f x1 x2 ... xn = [stmt]
[stmt] ::= skip                                (do nothing)
        | x := y                               (assign y to x)
        | free x                               (deallocate x)
        | [stmt];[stmt]                        (sequential execution)
        | let x = null in [stmt]               (bind x to null)
        | let x = y in [stmt]                  (bind x to y)
        | let x = !y in [stmt]                 (bind x to the content of y)
        | let x = malloc() in [stmt]           (allocate a size 2 cell and bind x to it)
        | let x = y + 1 in [stmt]              (pointer arithmetics)
        | if x = null then [stmt] else [stmt]  (branch with x = null)
        | if * then [stmt] else [stmt]         (nondeterministic branch)
        | f x1 x2 ... xn                       (function call)
        | assert(x = y)                        (asserts x = y, used to pass obligations/capabilities between x and y)
        | assert(x = !y)                       (asserts x = !y, obligations/capabilities are passed between x and !y)
        | assert(x = y + 1)                    (asserts x = y + 1, obligations/capabilities are passed between x and y + 1)

Sample

The following program appends two linked lists p and q, and returns the appended list to a reference r

let rec app p q r = 
  if p = null then 
    r := q 
  else 
    (r := p; 
     (let nextp = p + 1 in 
      let next = !nextp in 
        app next q nextp; assert(next = !nextp); assert(nextp = p + 1)); 
      assert(p = !r)) 
in 
  skip 

For more samples, see test directory in the archive.

Command-line options

  --debugGenConstr dump behaviour of constraint generating function
  --noMinimize do not minimize unsatisfiable inequalities
  --displaySolution display a solution of linear inequalities
  --outputLinearProg output linear inequalities
  -help  Display this list of options
  --help  Display this list of options

Papers

• Naoki Kobayashi and Kohei Suenaga. Fractional Ownerships for Safe Memory Deallocation. Submitted to ESOP 2009. (short version) (full version)