Smallfoot 0.1
2005-12-15
Copyright 2001-2005
Cristiano Calcagno (ccris@doc.ic.ac.uk),
Josh Berdine (berdine@dcs.qmul.ac.uk),
Peter O'Hearn (ohearn@dcs.qmul.ac.uk)

Smallfoot is an automatic verification tool which checks separation
logic specifications of concurrent programs which manipulate
dynamically-allocated recursive data structures.  For further
information see:
http://www.dcs.qmul.ac.uk/research/logic/theory/projects/smallfoot/

This is a developmental release, intended only for experimentation.


Installation
============

Precompiled MacOS X PPC and Linux x86 executables can be found in bin.

OCaml (version 3.07 or later) is required to compile.  After unpacking
the tarball, performing "cd smallfoot ; make" will build the native
code executable "smallfoot", and "make smallfoot.byte" will build the
bytecode executable "smallfoot.byte".  These programs do not hardcode
any paths, so can be moved anywhere after compilation.


Usage
=====

"smallfoot [options] <file>" where the following command line options
are accepted:
  -verbose         Display additional internal information
  -all_states      Display intermediate states
  -show_induction  Indicate when induction is used during verification
  -very_verbose    Display more additional internal information
  -help            Display usage message

See the EXAMPLES directory for some sample programs.  For instance:
    $ ./smallfoot EXAMPLES/parallel_tree_deallocate.sf 

    Function tree_deallocate

    Valid
    $
indicates a successful verification, while:
    $ ./smallfoot EXAMPLES/heap_race.sf 

    Function update

    Function heap_race
    File "EXAMPLES/heap_race.sf", line 9, characters 2-31:
    ERROR cannot find frame: parallel call
    0!=c * c |-> tl:0 |- c |->  * c |-> 

    NOT Valid
    $
indicates a failed verification, identifying the source code location
associated with the error, and a brief description.

Note that the source code locations are printed in standard form, and
so e.g. emacs can parse them.  That is, after executing the M-x
compile function with "./smallfoot EXAMPLES/heap_race.sf" as the
compile command, M-x next-error will indicate the source locations.
This is particularly useful with e.g. "./smallfoot -all_states
EXAMPLES/queue.sf".


Input Language
==============

Lexical structure
-----------------

whitespace ::= blank | comment
blank      ::= horizontal tab | linefeed | vertical tab | formfeed
             | carriage return | space
comment    ::= "/*" anything "*/"

    Whitespace delimits tokens but is otherwise ignored.  Comments nest.

keywords: NULL dispose dlseg else emp false if list lseg local new
          resource then tree true when while with xlseg

    NULL is a synonym for 0

ident    ::= letter alphanum*
field    ::= ident
number   ::= digit+
letter   ::= "A"--"Z" | "_" | "a"--"z"
alphanum ::= digit | letter
digit    ::= "0"--"9"


Grammar
-------

program ::= (field_seq ";")? (resource_decl | fun_decl)*

    The field_seq declares the valid field names, which by default
    includes the default fields of all the predicates, see below.

resource_decl ::= "resource" ident "(" ident_seq ")" "[" formula "]"
fun_decl      ::= ident "(" formals ")" ("[" formula "]")?
                  "{" local_decl* statement* "}" ("[" formula "]")?
formals       ::= (ident_seq ";")? ident_seq
ident_seq     ::= /* empty */ | ident ("," ident)*
local_decl    ::= "local" ident ("," ident)* ";"

    The formals consist of the reference parameters (which are
    optional) followed by the value parameters.  If a function pre- or
    post-condition is omitted, it defaults to "emp".

statement    ::= ident "=" stmt_exp ";"
	       | ident "=" stmt_exp "->" field ";"
	       | stmt_exp "->" field "=" stmt_exp ";"
	       | ident "=" "new" "(" ")" ";"
	       | "dispose" stmt_exp ";"
	       | "{" statement* "}"
	       | "if" "(" stmt_exp ")" statement ("else" statement)?
	       | "while" "(" stmt_exp ")" ("[" formula "]")? statement
	       | "with" ident "when" "(" stmt_exp ")" statement
	       | ident "(" actuals ")" ";"
	       | ident "(" actuals ")" "||" ident "(" actuals ")" ";"
actuals      ::= stmt_exp_seq (";" stmt_exp_seq)?
stmt_exp     ::= "(" stmt_exp ")"
	       | ident | number | "true" | "false"
	       | prefix_op stmt_exp | stmt_exp infix_op stmt_exp
stmt_exp_seq ::= /* empty */ | stmt_exp ("," stmt_exp)*
infix_op     ::= "==" | "!=" | "^"
               | "&&" | "*" | "/" | "%" | "+" | "-" | "<" | "<=" | ">" | ">="
prefix_op    ::= "+" | "-"

    If a loop invariant is omitted, it defaults to "emp".  All of the
    infix_op's except equality "==", non-equality "!=", and
    exclusive-or "^" are essentially unimplemented.

formula  ::= "(" formula ")"
           | "false"
           | form_exp "==" form_exp
           | form_exp "!=" form_exp
           | "emp"
           | formula "*" formula
           | form_exp "|->" ((field ":" form_exp)*
                           | form_exp | form_exp "," form_exp)
           | "list" "(" (field ";")? form_exp ")"
           | "lseg" "(" (field ";")? form_exp "," form_exp ")"
           | ("dlseg" | "xlseg") "(" (field ";" field ";")?
             form_exp "," form_exp "," form_exp "," form_exp ")"
           | "tree" "(" (field ";" field ";")? form_exp ")"
           | "if" form_exp ("==" | "!=") form_exp "then" formula "else" formula
form_exp ::= "(" form_exp ")" | ident | number | form_exp "^" form_exp

    Here, unlike in the related papers, formulae are not composed of
    distinct boolean (pure) and heap (spatial) parts.  Instead "E==F"
    and "E!=F" are only satisfied by the empty heap, like "emp", and
    "*" is the only conjunction.

    For the "|->" predicate, in the second alternative the "tl" field
    is assumed, and in the third alternative "l" and "r" fields are
    assumed.  For the inductive predicates, omitted fields default to:
    - "hd" and "tl" for lists;
    - "d", "l", and "r" for doubly-linked lists;
    - "d" and "l" for xor-linked lists; and
    - "d", "l", and "r" for trees.


precedences (increasing) and associativities:
1  * &&         L
2  == !=        L
3  = < <= > >=  L
4  + -          L
5  ^ |-> / %    L