HIP/SLEEK is an automated program verification framework based on separation logic.

Building HIP and SLEEK

You will need opam and a recent OCaml compiler (tested on 4.14.1).

opam install . --deps-only
dune build @hipsleek

# To use ocamldebug
rake debug:hip debug:sleek

Try verifying some small programs. You will need Z3 (from opam, pip, or a system package manager) and Omega (below) on the PATH.

dune exec ./hip.exe dune-tests/hip/ll.t/ll.ss
dune exec ./sleek.exe dune-tests/sleek/sleek2.t/sleek2.ss

Installing SLEEK as a library

opam install .

Running tests

dune test

Installing external provers

Other external provers HIP/SLEEK uses can be built from source. They will be installed in their respective directories and should be made available on the PATH.

Here is an example .envrc file which makes all the provers available, after following the steps below to build each one:

eval "$(opam env --switch=4.14.1 --set-switch)"
PATH_add omega_modified/omega_calc/obj
PATH_add mona-1.4/bin
PATH_add fixcalc_src

Omega

(cd omega_modified; make oc)

Mona

tar -xvf mona-1.4-modif.tar.gz
cd mona-1.4
./configure --prefix=$(pwd)
make install
cp mona_predicates.mona ..
cd -

Try some tests:

./hip -tp mona dune-tests/hip/ll.t/ll.ss
./sleek -tp mona dune-tests/sleek/sleek2.t/sleek2.ss

Fixcalc

You will need GHC 9.4.8.

cabal install --lib regex-compat old-time
cabal install happy

Build Omega first. Then, in the hipsleek project directory,

git clone https://github.com/hipsleek/omega_stub.git
(cd omega_stub; make)

git clone https://github.com/hipsleek/fixcalc.git fixcalc_src
(cd fixcalc_src; make fixcalc)

Some user-facing aspects of the system are described in the following papers.

  • Automated Verification of Shape, Size and Bag Properties via User-Defined Predicates in Separation Logic (SCP 2012)
  • Structured Specifications for Better Verification of Heap-Manipulating Programs (FM 2011)
  • Immutable specifications for more concise and precise verification (OOPSLA 2011)
  • Translation and optimization for a core calculus with exceptions (PEPM 2009)
  • Enhancing Program Verification with Lemmas (CAV 2008)
  • Enhancing modular OO verification with separation logic (POPL 2008)
  • Multiple Pre/Post Specifications for Heap-Manipulating Methods. HASE 2007

Core Language

The following is an incomplete grammar of the core language.

Spec_var ::= string ;

Ident ::= string ;

Type ::= string ;

Ghost ::= | "assert" Formula ; assertion
          | "dprint" ; print current state (?)
          | "unfold" Spec_var ; unfold specification variables

Ident_tuple ::= "()" | "(" Ident ("," Ident)* ")"

Expr ::= | integer ; integer constant
         | float ; float constant
         | "true" | "false" ; boolean constant
         | "if" Ident "[" Expr "]" "else" "[" Expr "]" ; conditional
         | "bind" Ident "to" Ident_tuple "in" Expr ; bind
         | Ident Ident_tuple ; function application
         | Ident "=" Expr ; assignment
         | Expr ";" Expr ; sequence
         | Ghost ; ghost expressions
         | "{" Expr "}" ; block
         | Type " " Ident ; variable declaration
         | "(" Type ")" Expr ; type casting (?)
         | "debug on" | "debug off" ; turning on or off devel debug
         | "while" (" Ident ")" Expr ; loop
         | "try" Expr "catch" "(" Type " " Ident ")" Expr ; try-catch

(Note that for bind, the number of bound variables must be equal to the number of fields in the data declaration.)

Some important files

  • solver.ml
  • typechecker.ml
  • astsimp.ml

General Flow

Input file -- Parse --> Input Ast (Iast) -- Normalization --> Iast -- Translation --> Core Ast (Cast) -- Forward verification --> Cast -- Entailment checking --> Done.

Normalization

Relevant files : astsimp.ml
Relevant functions : case_normalize_program, case_normalize_proc, case_normalize_struc_formula

The following is a non-exhaustive list of normalization performed:

  • While loops.
while Cond { Body }
->
let v_bool = Cond in
while v_bool { Body }
  • Function application.
function_ident(expresssion_1,...,expression_n)
->
let v1 = expression_1 in
...
let vn = expression_n in
function_ident(v1,...,vn)

(Note the left to right evaluation of arguments)

Translation

Relevant files : astsimp.ml
Relevant functions : trans_prog, trans_proc, trans_views, trans_axiom, trans_I2C_struc_formula, trans_exp

To have simpler rules for forward verification, HIPSLEEK first performs some transformation on the Iast before translating it to Cast which is a simplified version of Iast.

The following is a non-exhaustive list of transformation performed:

  • Transform while statements to tail recursive top level functions.
while Cond { Body }
->
while_rec = if Cond [ Body; while_rec ]
            else []

(Note that while_rec is the new tail recursive function introduced during transformation.)

  • Transform break/continue to try-catch block.
while Cond {... break; ...}
->
while_rec =
try ( if Cond [ try { ... throw brk_default ... }
                catch (cnt_default) { };
                while_rec ]
     else [] )
catch (brk_default) { }

while Cond {... continue; ...}
->
while_rec =
try ( if Cond [ try { ... throw cnt_default ... }
                catch (cnt_default) { };
                while_rec ]
     else [] )
catch (brk_default) { }
  • Transform field accesses to bind.
x.f_i
->
bind x to (v_1,...,v_i,...,v_n) in v_i

x.f_i = v
->
bind x to (v_1,...,v_i,...,v_n) in v_i = v
  • Transform primitive operations to function calls.
x + y
->
add___$int~int(x, y)

(Note that these primitive functions are defined in prelude.ss.)

These transformations are done in trans_exp before translating to Cast.

Forward verification

Relevant files : typechecker.ml
Relevant functions : check_proc, check_specs_infer, check_exp

check_proc is applied to every procedure/function in the program to be verified.

check_exp essentially implements the forward verification rules. It will initialize a proof state (Cformula.list_failesc_context) that contains the pre condition of the function and walk through the body of the function. While walking through the body of the function, it will update the proof state according to the forward verification rules and the kind of expression in the body.

If there is a function call within the body of the function, check_exp will check whether the proof state at the call site entails the pre condition of the function being called. If it does, then the proof state after the call will be the composition of the residue from the entailment checking and the post condition of the function being called.

Entailment checking

Relevant files : typechecker.ml, solver.ml
Relevant functions : check_proc, check_specs_infer, check_post, heap_entail_struc_list_partial_context_init

After check_exp returns the final proof state after walking through the entire body of the function, check_post will be called with the final proof state. It will then call heap_entail_struc_list_partial_context_init which will check whether the final proof state entails the post condition of the function. It it does, then the verification of the function succeeds. Otherwise, verification of the function fails.

Pure logic verification conditions

Relevant files : smtsolver.ml, z3.ml

Currently, by default, the prover discharges pure logic conditions to Z3 via invoking the instance present on the PATH. Each formula is translated into an equivalent statement in SMTLIB format, and the entailment (along with all custom relations, axioms, etc.) is verified via Z3. Each possible return value (sat, unsat, unknown) is then converted into either a proof success, or indicator of a may-failure or must-failure (indicating an unknown result, or a known invalid entailment, respectively.)

For some pure values, some type information is necessary to properly generate monomorphic SMT statements. Although type checking is done earlier in the process, (in typeinfer.ml during the Iast-to-Cast lowering, and the aforementioned typechecker.ml), the AST itself only contains partial type information (e.g. in spec var annotations.) cpure_ast_typeinfer.ml attempts to extend these annotations to something more fully usable by the SMT generator.

API docs

Limitations of API/ Possible improvements

  • Ghost statements (e.g. assert)
  • OOP
  • Termination checking
  • Better handling of failed proving than just throwing an exception

Miscellaneous

Q: What is a view?

A: Views are predicates.

Q: What is Iast.proc_decl.proc_ho_arg?

A: Higher order arguments. They are currently not supported in the api. Check out rho/web/cdl-ex3-fm.ss for example of these higher order arguments. They are variables prefixed with % symbol. (e.g. %P).

Q: What is the difference between dynamic and static specs?

A: Dynamic specs are used for OOP where dynamic binding is used to resolve method calls at runtime and therefore function specs. Static specs should be used most of the time.

**Q: What are instance call (Cast.ICall) and static calls (Cast.SCall)?

A: Instance calls are used for method calls in OOP and static calls are used for both static method calls in OOP and regular function calls.

Q: What is para continuation analysis?

A: Continuation analysis for views. To find out the continuation parameters for each view in the program and insert them into the Cast.view_cont_vars field of Cast.view_decl. Examples for views with continuation parameters are WFSegN and WFSeg in prelude.ss.

Q: What does Astsimp.compute_view_x_formula do?

A: Uses Xpure approximation on predicate to compute predicate invariant.