Module Assertions

module Assertions: sig .. end

Separation logic assertions (symbolic heaps)

This module defines:

the internal representation of assertions & actions
constructors for such assertions
common operations (free variables, substitution, basic simplification)
interference computation (generalization of septraction)
the theorem prover interface

TODO: Only |->'s and singly-linked lists are implemented properly. Doubly-linked lists and user-defined predicates are not.

type link_kind =

`\|`	`SINGLE of Misc.component * Exp.Fld.t`	`(*`	Node name, common fields	`*)`
`\|`	`DOUBLE of Misc.component * Misc.component`
`\|`	`XOR of Misc.component`

Kind of link for linked lists

type can_isemp =

`\|`	`Cem_PE`	`(*`	possibly empty	`*)`
`\|`	`Cem_NE`	`(*`	definitely non-empty	`*)`

type tag

Tags for spatial predicates. (These are for internal use in this module only: use the default tag constructor, default_tag, to get a tag.)

type tag2

type pstate =

`\|`	`Pstate_one of Misc.component * Exp.exp list`
`\|`	`Pstate_max of pstate * pstate`

type can_spred =

`\|`	`Csp_listsegi of tag * link_kind * Exp.exp * Exp.exp * Exp.exp * Exp.exp * can_isemp * Exp.Dset.t`
`\|`	`Csp_arr of tag * Exp.exp * Exp.exp * Exp.exp * Exp.Fld.t * can_isemp * Exp.Dset.t`
`\|`	`Csp_node of tag * Misc.component * Exp.exp * Exp.Fld.t * tag2`
`\|`	`Csp_indpred of tag * string * Exp.exp list`
`\|`	`Csp_atomic_fld of tag * Exp.exp * Misc.component * Misc.component * pstate`
`\|`	`Csp_escrow of tag * Misc.component * Exp.exp list`
`\|`	`Csp_token of tag * Exp.exp`

Canonical heap predicate.

NB: Unlike Smallfoot, the list segments of CAVE (Csp_listsegi) are "imprecise". For justification, read the SAS 2007 paper on SmallfootRG.

type can_spatial = can_spred list

Star-conjunction of heap predicates

type uform = Pure.t * can_spatial

Canonical formulas without boxes

type cform = uform * (Misc.component, cprop) Misc.plist

Canonical formulas with boxes

type cprop = cform list

Canonical proposition: disjunction of canonical formulas

type act

Type of RGSep actions used for interference calculations

exception No_frame_found of string

exception Junk

Operations on spatial formulas

val tag_default : tag

val tag2_default : tag2

val spred_fold : (Exp.exp -> 'a -> 'a) -> can_spred -> 'a -> 'a

val spat_empty : can_spatial

val spat_one : can_spred -> can_spatial

val spat_star_one : can_spred -> can_spatial -> can_spatial

val spat_star : can_spatial -> can_spatial -> can_spatial

val spat_remove : can_spatial -> can_spred -> can_spatial

val spat_fold : (Exp.exp -> 'a -> 'a) -> can_spatial -> 'a -> 'a

val spat_fold_spred : (can_spred -> 'a -> 'a) -> can_spatial -> 'a -> 'a

val spat_get : Exp.exp ->
       can_spatial ->
       (can_spred * can_spatial) option

val compare_can_spred : can_spred -> can_spred -> int

val abs_compare_can_spred : can_spred -> can_spred -> int

Constructors

val uform_false : uform

val cform_false : cform

val cprop_false : cprop

val uform_empty : uform

val cprop_empty : cprop

val is_cprop_empty : cprop -> bool

val cprop_pure : Pure.t -> cprop

val cprop_spred : can_spatial -> cprop

val cprop_uform : uform -> cprop

val cprop_cform : cform -> cprop

val mk_array : tag ->
       Exp.exp ->
       Exp.exp ->
       Exp.exp -> Exp.Fld.t -> Exp.Dset.t -> uform -> uform

val cform_star : cform -> cform -> cform option

cform_star cf1 cf2 may return None if the result is inconsistent

val cprop_star : cprop -> cprop -> cprop

val and_cprop_pure : cprop -> Pure.t -> cprop

val cprop_or : cprop -> cprop -> cprop

val cprop_box : Misc.component -> cprop -> cprop

val aggr_remove_cform_duplicates : cprop -> cprop

Removes duplicates and combines boxes

Comparisons

val compare_uform : uform -> uform -> int

val compare_cform : cform -> cform -> int

val compare_cprop : cprop -> cprop -> int

val compare_component_cprop : Misc.component * cprop -> Misc.component * cprop -> int

val remove_uform_duplicates : uform list -> uform list

val remove_cform_duplicates : cform list -> cform list

val can_spred_leq : can_spred -> can_spred -> Exp.exp

val equal_pstate : pstate -> pstate -> bool

Free variables

val uform_fhd : uform -> Exp.IdSet.t -> Exp.IdSet.t

val spred_fv : can_spred -> Exp.IdSet.t -> Exp.IdSet.t

Return the free variables of a spatial predicate

val spred_exfv : can_spred -> Exp.IdSet.t -> Exp.IdSet.t

val prop_fv : cprop -> Exp.IdSet.t -> Exp.IdSet.t

Return the free variables of an assertion

val fv_norm_cprop : cprop -> Exp.IdSet.t

Return the non-existential free variables of an assertion

val prop_exfv : cprop -> Exp.IdSet.t -> Exp.IdSet.t

Return the existential free variables of an assertion

val form_exfv : cform -> Exp.IdSet.t -> Exp.IdSet.t

val abs_fv_uform : uform -> Exp.Id.t list

Returns existential free variables in a canonical order

Substitutions

val map_spat : (Exp.exp -> Exp.exp) -> can_spatial -> can_spatial

val map_uform : (Exp.exp -> Exp.exp) -> uform -> uform list

val map_cform : (Exp.exp -> Exp.exp) -> cform -> cprop

val map_cprop : (Exp.exp -> Exp.exp) -> cprop -> cprop

val map_ip_body : (Exp.exp -> Exp.exp) ->
       (Pure.t * cform) list -> (Pure.t * cform) list

val naive_map_cform : (Exp.exp -> Exp.exp) -> cform -> cform

Normalization

val form_kill_hd_vars : cform -> cform

val prop_kill_can_return : cprop -> cprop

val normalize_uform : uform -> uform list

val normalize_cform : cform -> cprop

val normalize_cform_aggr : cform -> cprop

val normalize_cprop : cprop -> cprop

val kill_garbage_vars : cprop -> cprop

val kill_garbage_vars_ufl : uform list -> uform list

val aggr_kill_garbage_vars : cprop -> cprop

val kill_dead_vars : Exp.IdSet.t -> cprop -> cprop

Kill the variables of cp that are not directly reachable from the set s

Theorem prover interface

type prover = {

	`find_ptsto : Misc.component -> Exp.exp -> can_spatial -> Exp.Fld.t * can_spatial;`
	`expose_ptsto : cprop -> Exp.exp -> cprop;`
	`nf_cprop : can_spatial -> cprop -> cprop;`
	`nf_cform : cform -> cprop;`
	`entails_cprop : cprop -> cprop -> Pure.t list;`
	`find_frame_cprop : can_spatial -> cprop -> cprop -> cprop;`
	`adv_entails_atom : cprop -> Exp.exp -> bool;`

}

Interface provided by the theorem provers:

find_ptsto and expose_ptsto: used by symbolic execution, but should be removed.
nf_cprop sl_context eq cp = cp' where cp' is a normal form of cp.
nf_cform cf returns cprop_false if cf is inconsistent, or cp' such that cf <==> cp' and nf_cprop [] empty_eq cp' = cp'
entails_cprop cp cp' returns inst if cp * inst |- cp'
find_frame_cprop fr cp1 cp2 returns res such that cp1 |- cp2 * res in context fr (i.e. for all R, (fr /\ R) * cp1 |- (fr /\ R) * cp2 * res) or raises No_frame_found

Actions

val new_acts : string ->
       cprop ->
       cprop -> cprop -> act list

Create a new set of actions: new_acts name ctx pre post

val new_acts_one : string ->
       Pure.t ->
       can_spatial ->
       can_spatial -> can_spatial -> act list

Create a new set of actions: new_acts name pure ctx pre post

val new_act_opt : string ->
       Pure.t ->
       can_spatial ->
       (Exp.exp * Exp.Fld.t * Exp.Fld.t) list ->
       can_spatial -> cprop -> act

val act_name : act -> string

Return the name of an action

val act_conj : Exp.exp -> act -> act

val act_changes : Exp.exp -> Misc.component -> act list -> act list

val interfere_once : prover -> act -> cprop -> cprop

interfere_once prover act cp calculate the effect of applying interference act to cp.

Pretty printing

val pp_spred : Format.formatter -> can_spred -> unit

val pp_uform : Format.formatter -> uform -> unit

val pp_cform : Format.formatter -> cform -> unit

val pp_cprop : Format.formatter -> cprop -> unit

val pp_act : Format.formatter -> act -> unit

val pp_pstate : Format.formatter -> pstate -> unit

Configuration parameters

val allow_leaks : bool Pervasives.ref

val disable_pure_code_checking : bool Pervasives.ref

val args : (Arg.key * Arg.spec * Arg.doc) list

Imprint | Data protection