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] " 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