HIP/SLEEK


HIP/SLEEK Overview

The HIP/SLEEK systems are aimed at automatic verification of functional correctness of heap manipulating programs. HIP is a separation logic based automated verification system for a simple imperative language, able to modularly verify the specifications of heap-manipulating programs. The specification language allows user defined inductive predicates used to model complex data structures. Specifications can contain both heap constraints and various pure constraints like arithmetic constraints, bag constraints. Based on given annotations for each method/loop, HIP will construct a set of separation logic proof obligations in the form of formula implications which are sent to the SLEEK separation logic prover. SLEEK is a fully automatic prover for separation logic with frame inferring capability.

Downloads

HIP/SLEEK Virtual Appliance

CS3234 HIP/SLEEK bundle -the version used during the CS3234 lecture on HIP/SLEEK

HIPTnT bundle -self contained bundle for hip with termination logic

HIP bundle -self contained for hip with solutions to VSTTE 2012 competition

Older HIP executable

SLEEK executable

SLEEK bundle -self contained for sleek to SMT 2014 competition

SCALA frontend for SLEEK

Work with provers, such as Omega Calculator, Isabelle, MONA, CVC Lite, Z3


Terms of Usage

HIP 1.0 software release is freely available for academic and non-commercial use. The tar file distributed contains hip executable and a brief manual for its usage. The bundle also contains for your convenience executables for third party provers, e.g. Omega calculator for which their original usage/licencing requirements apply.

Description

   HIP is a separation logic based automated verification system for a simple imperative language, able to modularly verify heap-manipulating programs. The system can handle programs with complex data structures. It accepts abstract descriptions for such structures in the form of inductive predicates. Predicates are represented as separation logic formulae that describe the shape of data structures together with their derived properties, such as length, height and bag of values.
   Given annotations for each method/loop with one or more pre/post conditions, the HIP verifier constructs a set of obligations in the form of implication checks between pairs of formulae which are then sent to the SLEEK prover to be discharged. The specification language allows rich specifications that contain both heap constraints expressed as separation logic formulae and several different logic fragments like Presburger arithmetic, bags, lists for the pure constraints. By making use of set/bag solvers, the user can also encode reachability conditions as a set/bag of values that can be collected from some given data structure. Such conditions are then automatically discharged by HIP.
   HIP relies on the SLEEK prover in order to discharge the verification conditions. SLEEK is a fully automatic prover for separation logic with frame inferring capability. It takes as input two heap states represented by separation formulae, and checks if one formula (the antecedent) entails the other (the consequent). The antecedent may cover more heap states than the consequent, so a residual heap state which represents the frame condition can be returned by the prover. This residual heap state will include the pure state of the antecedent. SLEEK also supports instantiation of logical variables that appear during the entailment as existential variables in the consequent. As part of the implication check, SLEEK discharges the heap obligations, the obligations pertaining to the shape of data structures and translates the remaining pure obligations to pure constraints that can be discharged by theorem provers. The list of possible pure provers includes Omega , MONA , CVC Lite, Z3, and Isabelle.

Usage

  • Installation: unpack the archive and run ./make install
  • Starting :
    • ./hip [options] <source_file>
    • ./sleek [options] <source_file>

  • The underlying pure provers can be chosen with the -tp option :
    • cvcl - Cvc Lite
    • oc - Omega Calculator {default}
    • co - Try first Cvc Lite if fail then try Omega Calculator
    • isabelle - Isabelle
    • mona - Mona
    • om - Try first Omega Calculator if fail then try Mona
    • oi - Try first Omega Calculator if fail then try Isabelle
    • set - Use Mona in set mode
    • cm - CVC Lite then Mona
    • z3 - Z3

  • HIP input format

        The input file will be made up of three main parts:

    • data declarations
      • Base types:

        int, bool, float, arrays

      • Structures:    

        The structure definition syntax :
            data struc_name { (base_type field_name;)*}

            e.g. the definition: data node { int val ; node next; } describes a structure called node with an integer field, val and a recursive node field next.

    • predicate definitions (including user-specified lemmas)
          The predicate definition syntax :
             pred_name <v* > == Φ inv π ;
          The predicate body Φ is a separation logic formula that provides information about the variables in the argument list. The predicate invariant π is a heap independent(pure) formula.
      • The syntax for separation logic formulae is given below. By (x)* we denote x zero or more times, (x)+ at least once, (x)? at most once.
        Φ := ψ    |    φ
        ψ := χ    |    [or)+ ]
        χ := case {(π -> Ψ ;)+}    |    [v*] φ (ψ)?
        φ := φ or φ    |    (φ)    |    ω     |     exists (v,)+: ω
        ω := (κ)? & π ξ
        ξ := (& FLOW= flow_name)?
        κ := True | κ * κ | v::struc_name < v* > (@I)? | v::pred_name < v* > (@I)?
        π := True | False | exists (v+:π)| forall(v+:π)| π & π | (π | π) | ε < ε |ε <= ε | ε > ε | ε >= ε | ε = ε | ε != ε | ε in ε | ε notin ε | ε subset ε | bagmax(ε, ε) | bagmin (ε, ε)
           |ε inlist ε | ε notinlist ε | alln (ε , ε) | perm (ε , ε)
        ε := id | null | int_const | float_const | (ε) | -ε | ε+ε| ε-ε| ε*ε| ε/ε | max(ε, ε) | min(ε, ε) | {ε*}| union(ε*)| intersect(ε*)| diff(ε,ε)| [ε*]| ε:::ε| tail(ε) | head(ε) | app(ε) | len(ε) | rev(ε)

      • A formula can be given either in a disjunctive normal form (φ) or in a richer syntax with staging and case constructs (ψ). In either case, the basic disjunct (ω) describes the heap shape (κ) pure constraints on the memory content (π) and possibly flow information. The basic heap node is described by a v::node_type<list_of_arguments> where v denotes a pointer to the node. If the node is an instance of a data structure, the arguments will refer to the structure fields else if the node is a predicate instance, the arguments will capture the predicate arguments. Immutability can be enforced for each heap node by the use of the @I annotations.
      • This format can be used to declare predicates for a wide range data structures. An example of a predicate is lseg which describes a list segment of specified length. Its formal definition in HIP is as follows:
        lseg<n, p> == self=p & n=0 or self::node<_,r> * r::lseg<n-1,p> inv n>=0
        It states that either the list segment is empty with length n=0, or or it is made up of a node linked to a smaller list segment of length n-1. Predicate invariants can be specified, for the lseg predicate, it's pure formulae (without heap) n>=0. If not specified, the pure invariant is just assumed to be true.
      • Lemmas relating heap predicates can also be defined. There are three classes of lemmas of simple form. By simple form we mean a lemma that has a single predicate instance in its LHS (φL). The lemma definition syntax is :
        • lemma φL -> φR
        • lemma φL <- φR
        • lemma φL <-> φR
    • method declarations (with multiple pre/post conditions)

  • A HIP input example:
    The example given bellow defines a node structure, a predicate describing a singly linked list, predicate that describes a sorted linked list and an append function that adds list y to the end of list x. The sortl predicate also captures the smallest and the largest elements in the list. The append method specification captures the fact that if given two linked lists then the result is a linked list of size equal to the sum of the two lists lengths. Also if the input lists are sorted and the smallest element in y is larger than the largest in x, then the resulting list is sorted.

          data node { int val; node next; }

               

          ll<n> == self=null & n=0 or  self::node<_,p> * p::ll<n-1> inv n>=0;

     

          sortl<mi,mx> == self::node<mi,null> & mi=mx  or  self::node<mi,p> * p::sortl<m,mx> & mi<=m inv mi<=mx & self!=null;

               

          node append(node x, node y)

           requires x::ll<n>*y::ll<m> & n>0

           ensures res::ll<n+m> & res=x;

           requires x::sortl<s1,b1> * y::sortl<s2,b2> & b1<=s2

           ensures res::sortl<s1,b2> ;

           requires x::sortl<s1,b1> & y=null

           ensures res::sortl<s1,b1>;

          {

            node t;

              t=x.next;

              if (t==null) x.next=y;

              else x.next=append(t,y);

              return x;

          }


    Papers

    • Cristina David, Wei-Ngan Chin : Immutable Specifications for More Concise and Precise Verification . OOPSLA 2011. [pdf]
    • Cristian Gherghina, Cristina David, Shengchao Qin and Wei-Ngan Chin : Structured Specifications for Better Verification of Heap-Manipulating Programs. FM 2011. [pdf]
    • Wei-Ngan Chin, Cristian Gherghina, Razvan Voicu, Quang Loc Le, Florin Craciun, Shengchao Qin : A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification. CAV 2011. [pdf]
    • Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin : Automated Verification of Shape, Size and Bag Properties via User-Defined Predicates in Separation Logic. Science of Computer Programming 2011.
    • Cristian Gherghina, Cristina David : A Specification Logic for Exceptions and Beyond. ATVA 2010. [pdf]
    • Cristina David, Cristian Gherghina, Wei-Ngan Chin : Translation and Optimization for a Core Calculus with Exceptions. PEPM 2009. [pdf]
    • Huu Hai Nguyen and Wei-Ngan Chin : Enhancing Program Verification with Lemmas. CAV 2008 [ps]
    • Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin : Automated Verification of Shape and Size Properties via Separation Logic. VMCAI 2007. [ps]
    People

    Contributors to HIP are: