Up  

Functor Sigma.Make

module Make: 
functor (C : Sigs.Chunk) -> 
functor (H : Qed.Collection.S  with type t = C.t) -> Sigs.Sigma  with type chunk = C.t
              and module Chunk = H
Parameters:
C : Sigs.Chunk
H : Qed.Collection.S with type t = C.t 
type chunk

The type of memory chunks.

module Chunk: Qed.Collection.S  with type t = chunk
type domain = Chunk.Set.t

Memory footprint.

type t

Environment assigning logic variables to chunk.

Memory chunk variables are assigned lazily. Hence, the vector is empty unless a chunk is accessed. Pay attention to this when you merge or havoc chunks.

New chunks are generated from the context pool of Lang.freshvar.

val pretty : Stdlib.Format.formatter -> t -> unit

For debugging purpose

val create : unit -> t

Initially empty environment.

val mem : t -> chunk -> bool

Whether a chunk has been assigned.

val get : t -> chunk -> Lang.F.var

Lazily get the variable for a chunk.

val value : t -> chunk -> Lang.F.term

Same as Lang.F.e_var of get.

val copy : t -> t

Duplicate the environment. Fresh chunks in the copy are not duplicated into the source environment.

val join : t -> t -> Passive.t

Make two environment pairwise equal via the passive form.

Missing chunks in one environment are added with the corresponding variable of the other environment. When both environments don't agree on a chunk, their variables are added to the passive form.

val assigned : pre:t ->
       post:t -> domain -> Lang.F.pred Bag.t

Make chunks equal outside of some domain.

This is similar to join, but outside the given footprint of an assigns clause. Although, the function returns the equality predicates instead of a passive form.

Like in join, missing chunks are reported from one side to the other one, and common chunks are added to the equality bag.

val choose : t -> t -> t

Make the union of each sigma, choosing the minimal variable in case of conflict. Both initial environments are kept unchanged.

val merge : t -> t -> t * Passive.t * Passive.t

Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins. Both initial environments are kept unchanged.

val merge_list : t list -> t * Passive.t list

Same than Sigs.Sigma.merge but for a list of sigmas. Much more efficient than folding merge step by step.

val iter : (chunk -> Lang.F.var -> unit) -> t -> unit

Iterates over the chunks and associated variables already accessed so far in the environment.

val iter2 : (chunk -> Lang.F.var option -> Lang.F.var option -> unit) ->
       t -> t -> unit

Same as iter for both environments.

val havoc_chunk : t -> chunk -> t

Generate a new fresh variable for the given chunk.

val havoc : t -> domain -> t

All the chunks in the provided footprint are generated and made fresh.

Existing chunk variables outside the footprint are copied into the new environment. The original environement itself is kept unchanged. More efficient than iterating havoc_chunk over the footprint.

val havoc_any : call:bool -> t -> t

All the chunks are made fresh. As an optimisation, when ~call:true is set, only non-local chunks are made fresh. Local chunks are those for which Chunk.is_frame returns true.

val remove_chunks : t -> domain -> t

Return a copy of the environment where chunks in the footprint have been removed. Keep the original environment unchanged.

val domain : t -> domain

Footprint of a memory environment. That is, the set of accessed chunks so far in the environment.

val union : domain -> domain -> domain

Same as Chunk.Set.union

val empty : domain

Same as Chunk.Set.empty

val writes : t Sigs.sequence -> domain

writes s indicates which chunks are new in s.post compared to s.pre.