Module `Checker__Location.ConstrSet`

the ConstrSet submodule provides a data type for tracking constraints on abstract locations. Let l1, l2 be two locations. Here l2 must start with an abstract location, hence represents a set of locations. Now constraints are of the form l1 in l2, meaning that the set of locations denoted by l2 must contain l1. l2 is called the superset and l1 is called the subset in the constraint

type constr = location * abstract_loc: the type for constraints, every constraint subset in supset is represented as a (subset, supset) pair.

type t: the abstract type for a constraint set

val empty : t: an empty constraint set

val singleton : sub:location -> sup:abstract_loc -> t: create a constraint set with only one constraint. The superset must be a plain abstract_loc without any path

val add : sub:location -> sup:abstract_loc -> t -> t: add a new constraint to a constraint set The superset must be a plain abstract_loc without any path

val merge : t -> t -> t: merge t1 t2 merges t1 and t2. The resulting constraint set is equivalent to the union of the constraints in t1 and t2.

val find_supsets : location -> t -> (path * location) Stdlib.Seq.t

find_supsets loc t calculates all supersets of loc, i.e. all locations loc' that satisfy loc in loc' w.r.t. the constraints in t, taking transitivity (if l1 in l2 and l2 in l3, then l1 in l3) and closure property (if l1 in l2, then l1.field in l2.field) of constraints into account.

Every pair (path, sup) in the result indicates that a constraint loc.path < sup is deducible from t

val find_subsets : abstract_loc -> t -> location Stdlib.Seq.t: find_subsets loc t calculates all subsets of loc, i.e. all locations loc' that satisfy loc' in loc w.r.t. the constraints in t, taking transitivity (if l1 in l2 and l2 in l3, then l1 in l3) and closure property (if l1 in l2, then l1.field in l2.field) of constraints into account

val simplify : wrt:abstract_loc list -> t -> t

simplify ~wrt:abs_locs t creates a simplified constraint set from t that only contains constraint about the abstract locations in abs_locs. The new constraint set is equivalent to t on relations between locations starting with abs_locs.

Constraints not containing abs_locs may affect the simplified constraint set via transitivity. For example, if abs_locs = [l1, l2], with l1 in l3 and l3 in l2 in t, then simplify ~wrt:abs_locs t will contain l1 in l2.

val to_seq : t -> constr Stdlib.Seq.t: convert a constraint set to a sequence of (subset, superset) pairs

val of_seq : constr Stdlib.Seq.t -> t: create a constraint set from a sequence of (subset, superset) pairs