module type Recycle =sig
..end
MemExec is a global cache for the complete analysis of functions. It avoids repeating the analysis of a function in equivalent entry states. It uses an over-approximation of the locations possibly read and written by a function, and compare the entry states for these locations.
type
t
Type of states.
val relate : Cil_types.kernel_function ->
Base.Hptset.t -> t -> Base.SetLattice.t
relate kf bases state
returns the set of bases bases
in relation with
bases
in state
— i.e. all bases other than bases
whose value may
affect the properties inferred on bases
in state
.
state
is the initial state of an analysis of kf
.
For a non-relational domain, it is always safe to return empty
.
For a relational domain, it is always safe to return top
, but it
disables MemExec.
val filter : Cil_types.kernel_function ->
[ `Post | `Pre ] ->
Base.Hptset.t -> t -> t
filter kf kind bases states
reduces the state state
to only keep
properties about bases
— it is a projection on the set of bases
.
It allows reusing an analysis of kf
from an initial state pre
to a
final state post
.
If kind
is `Pre, state
is the initial state pre
, and bases
includes all inputs of kf
and satisfies relate kf bases state = bases
.
If kind
is `Post, state
is the final state post
, and bases
includes all inputs and outputs of kf
.
Afterwards, the two resulting states reduced_pre
and reduced_post
are
used as follow: when kf
should be analyzed with the initial state s
,
if filter kf `Pre s = reduced_pre
, then the analysis is skipped, and
reuse kf s reduced_post
is used as its final state instead.
val reuse : Cil_types.kernel_function ->
Base.Hptset.t ->
current_input:t ->
previous_output:t -> t
reuse kf bases current_input previous_output
merges the initial state
current_input
with a final state previous_output
from a previous
analysis of kf
started with an equivalent initial state.
reuse
must overwrite the properties on bases
in current_input
with
the ones in previous_output
. Properties on other bases must be left
unchanged from current_input
.
The simplest implementation of filter
and reuse
is:
let filter _ _ _ state = state
let reuse _ _ ~current_input:_ ~previous_output = previous_output
This is correct as the cache will be triggered only for an initial state
exactly equal to the previous initial state, in which case the previous
output state is indeed a correct final state on its own.