Frama-C:
Plug-ins:
Libraries:

Frama-C API - Caching

Functions used to interpret at once multiple effects on abstract states:

  • the MemExec analysis cache avoids repeating analyses of a same function in equivalent entry states, by directly computing the new final state.
  • the analysis of concurrent programs injects in abstract states all potential interferences coming from other threads.
type t

Type of states.

relate bases state returns the set of 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. For a non-relational domain, it is always sound to return empty. For a relational domain, it is always sound to return top, but this disables the MemExec cache.

val filter : Frama_c_kernel.Base.Hptset.t -> t -> t

filter bases state returns a state that must contain exactly the same properties about bases as state. All properties about other bases can be removed from the state. If S' = filter B S, S' must satisfy proj(γ(S'), B) = proj(γ(S), B). Defined by Domain_builder.Complete as the identity, which is sound but decreases the performance of the MemExec cache. If you implement filter, you must also provide a sound implementation of reuse.

val reuse : Frama_c_kernel.Base.Hptset.t -> current_input:t -> previous_output:t -> t

reuse bases ~current_input ~previous_output returns a state equal to current_input, except that all properties about bases must be replaced by the ones in previous_output. It must be exact to ensure that the MemExec cache does not impact the analysis precision. reuse is only applied to re-interpret a code <C> already analyzed with an equivalent initial state. current_input is the new input state for the analysis of <C>, and previous_output was the final state of the former analysis of <C>. See below for details. Defined by Domain_builder.Complete with a naive implementation which is only sound when filter is implemented as the identity.

val project : Frama_c_kernel.Base.Hptset.t -> t -> t

project bases state returns an over-approximation of the projection of state on bases. If S' = project B S, S' must satisfy proj(γ(S), B) ⊆ γ(S'). Defined by Domain_builder.Complete by always returning top.

val overwrite : Frama_c_kernel.Base.Hptset.t -> on:t -> by:t -> t

overwrite bases ~on ~by returns a state equal to on, except that all properties about bases are replaced by the ones in by. Unlike reuse, overwrite can compute an over-approximation, but cannot use any assumption about state on. State by is the result of a projection on bases bases. A sound but imprecise implementation can remove all properties about bases from state on (and ignore state by). More formally, this function must compute an over-approximation of proj(γ(on), complement(bases)) ∩ proj(γ(by), bases), where complement(bases) are all memory bases other than bases.

About the MemExec cache: Assuming a former analysis of function F has computed F(S1) = S1' by reading only bases R and writing only bases W (S1 is the initial state, S1' the final state). For a new initial state S2, if filter R S1 = filter R S2 (the new entry state is exactly the same as the previous one on all read bases), then the analysis S2' = F(S2) is skipped and the final state is computed as S2' = reuse W S2 (filter W S1').

The implementation of reuse can use these assumptions on the set of written bases W, the new initial state S2 and the former final state S1' to compute its result S2'.