Module Goblint_lib.CongruenceClosure

2-Pointer Logic

Domains for C2poAnalysis.

OCaml implementation of a quantitative congruence closure. It is used by the C-2PO Analysis and based on the UnionFind implementation.

include module type of struct include UnionFind end

The Union Find is used by the C-2PO Analysis. This file contains the code for a quantitative union find and the quantitative finite automata. They will be necessary in order to construct the congruence closure of terms.

exception Unsat
val compare_exp : 'a -> 'b -> int
val equal_exp : 'a -> 'b -> bool
val hash_exp : 'a -> int
type term = UnionFind.term =
  1. | Addr of DuplicateVars.Var.t
  2. | Aux of DuplicateVars.Var.t * GoblintCil.exp
  3. | Deref of term * Z.t * GoblintCil.exp
val equal_term : term -> term -> Ppx_deriving_runtime.bool
val hash_term : term -> int
val compare_term : term -> term -> Ppx_deriving_runtime.int
val normal_form_tuple_3 : (term * term * Z.t) -> term * term * Z.t
val normal_form_tuple_2 : (term * term) -> term * term
val tuple3_equal : (term * term * Z.t) -> (term * term * Z.t) -> bool

Two propositions are equal if they are syntactically equal or if one is t_1 = z + t_2 and the other t_2 = - z + t_1.

val tuple3_cmp : (term * term * Z.t) -> (term * term * Z.t) -> int
val tuple3_hash : (term * term * Z.t) -> int
val tuple2_equal : (term * term) -> (term * term) -> bool
val tuple2_cmp : (term * term) -> (term * term) -> int
val tuple2_hash : (term * term) -> int
type term_offset_relation = term * term * Z.t
val equal_term_offset_relation : term_offset_relation -> term_offset_relation -> Ppx_deriving_runtime.bool
val hash_term_offset_relation : term_offset_relation -> int
val compare_term_offset_relation : term_offset_relation -> term_offset_relation -> Ppx_deriving_runtime.int
type block_relation = term * term
val equal_block_relation : block_relation -> block_relation -> Ppx_deriving_runtime.bool
val hash_block_relation : block_relation -> int
val compare_block_relation : block_relation -> block_relation -> Ppx_deriving_runtime.int
type prop = UnionFind.prop =
  1. | Equal of term_offset_relation
  2. | Nequal of term_offset_relation
  3. | BlNequal of block_relation
val equal_prop : prop -> prop -> Ppx_deriving_runtime.bool
val hash_prop : prop -> int
val compare_prop : prop -> prop -> Ppx_deriving_runtime.int
module T = UnionFind.T

The terms consist of address constants and dereferencing function with sum of an integer. The dereferencing function is parametrized by the size of the element in the memory. We store the CIL expression of the term in the data type, such that it it easier to find the types of the dereferenced elements. Also so that we can easily convert back from term to Cil expression.

module TMap = UnionFind.TMap
module TSet = UnionFind.TSet
module UnionFind = UnionFind.UnionFind

Quantitative union find

module ZMap = UnionFind.ZMap
module LookupMap = UnionFind.LookupMap

For each representative t' of an equivalence class, the LookupMap maps t' to a map that maps z to a term in the data structure that is equal to *(z + t').

module M = Messages
module TUF = UnionFind
module LMap = LookupMap
module BlDis : sig ... end
module Disequalities : sig ... end
module SSet : sig ... end

Set of subterms which are present in the current data structure.

module MRMap : sig ... end

Minimal representatives map. It maps each representative term of an equivalence class to the minimal term of this representative class. rep -> (t, z) means that t = rep + z

val get_transitions : (((Goblint_lib__UnionFind.term * Z.t) * 'a) TUF.ValMap.t * TUF.ValMap.key BatMap.Make(Z).t BatMap.Make(Goblint_lib__UnionFind.T).t) -> (Z.t * term * (Goblint_lib__UnionFind.term * Z.t)) list

Returns a list of all the transition that are present in the automata.

val show_conj : Goblint_lib__UnionFind.prop list -> string
type data = {
  1. uf : TUF.t;
  2. set : SSet.t;
  3. map : LMap.t;
  4. diseq : Disequalities.t;
  5. bldis : BlDis.t;
}
val equal_data : data -> data -> Ppx_deriving_runtime.bool
val compare_data : data -> data -> Ppx_deriving_runtime.int
val hash_data : data -> int
val get_normal_conjunction : data -> (Goblint_lib__UnionFind.term -> term * Z.t) -> T.v_prop list

Converts the domain representation to a conjunction, using the function `get_normal_repr` to compute the representatives that need to be used in the conjunction.

module NormalFormEval : sig ... end
module LazyNormalFormEval : sig ... end
type t = {
  1. data : data;
  2. normal_form : LazyNormalFormEval.t;
}

This is the type for the abstract domain.

  • `uf` is the union find tree
  • `set` is the set of terms that are currently considered. It is the set of terms that have a mapping in the `uf` tree.
  • `map` maps reference variables v to a map that maps integers z to terms that are equivalent to *(v + z). It represents the transitions of the quantitative finite automata.
  • `normal_form` is the unique normal form of the domain element, it is a lazily computed when needed and stored such that it can be used again later.
  • `diseq` represents the disequalities. It is a map from a term t1 to a map from an integer z to a set of terms T, which represents the disequality t1 != z + t2 for each t2 in T.
  • `bldis` represents the block disequalities. It is a map that maps each term to a set of terms that are definitely in a different block.
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val hash : t -> int
val exactly_equal : data -> data -> bool
val get_normal_form : t -> NormalFormEval.result

Returns the canonical normal form of the data structure in form of a sorted list of conjunctions.

val show_normal_form : LazyNormalFormEval.t -> string

Converts the normal form to string, but only if it was already computed.

val get_conjunction_from_data : data -> T.v_prop list
val get_conjunction : t -> T.v_prop list

Returns a list of conjunctions that follow from the data structure in form of a sorted list of conjunctions. This is not a normal form, but it is useful to print information about the current state of the analysis.

val reset_normal_form : t -> t

Sets the normal_form to an uncomputed value, that will be lazily computed when it is needed.

val data_to_t : data -> t
val show_all : t -> string
val split : prop list -> term_offset_relation list * term_offset_relation list * block_relation list

Splits the conjunction into three groups: the first one contains all equality propositions, the second one contains all inequality propositions and the third one contains all block disequality propositions.

val init_cc : unit -> data

Returns {uf, set, map, normal_form, bldis, diseq}, where all data structures are initialized with an empty map/set.

val congruence_neq : data -> term_offset_relation list -> data

Computes the closure of disequalities.

val update_bldis : TMap.key TMap.t -> TSet.t TMap.t -> TSet.t TMap.t

Update block disequalities with the new representatives.

val closure : data -> (TUF.ValMap.key * TUF.ValMap.key * Z.t) list -> data

Parameters: cc conjunctions.

returns updated cc, where:

  • `uf` is the new union find data structure after having added all equalities.
  • `set` doesn't change
  • `map` maps reference variables v to a map that maps integers z to terms that are equivalent to *(v + z).
  • `diseq` doesn't change (it must be updated later to the new representatives).
  • `bldis` are the block disequalities between the new representatives.

Throws "Unsat" if a contradiction is found. This does NOT update the disequalities. They need to be updated with `congruence_neq`.

val add_normalized_bl_diseqs : data -> (TUF.ValMap.key * TUF.ValMap.key) list -> data

Adds the block disequalities to the cc, but first rewrites them such that they are disequalities between representatives. The cc should already contain all the terms that are present in those block disequalities.

val insert : data -> TSet.elt -> (Goblint_lib__UnionFind.term * Z.t) * data

Add a term to the data structure.

Returns (reference variable, offset), updated congruence closure

val insert_set : data -> TSet.t -> data

Add all terms in a specific set to the data structure.

Returns updated cc.

val eq_query : data -> (TSet.elt * TSet.elt * Z.t) -> bool * data

Returns true if t1 and t2 are equivalent.

val block_neq_query : data -> (TSet.elt * TSet.elt) -> bool
val neq_query : data -> (TSet.elt * TSet.elt * Z.t) -> bool

Returns true if t1 and t2 are not equivalent.

val meet_pos_conjs : data -> (TUF.ValMap.key * TUF.ValMap.key * Z.t) list -> data

Adds equalities to the data structure. Throws "Unsat" if a contradiction is found. Does not update disequalities.

val meet_conjs_opt : prop list -> data -> data

Adds propositions to the data structure. Returns None if a contradiction is found.

val add_eq : data -> (TSet.elt * TSet.elt * Z.t) -> data

Add proposition t1 = t2 + r to the data structure. Does not update the disequalities.

val add_block_diseqs : data -> TMap.key -> data

Adds block disequalities to cc: for each representative t in cc it adds the disequality bl(lterm) != bl(t)

val remove_terms_from_eq : (Goblint_lib__UnionFind.term -> bool) -> data -> (term * Z.t) BatMap.Make(Goblint_lib__UnionFind.T).t * data

Removes terms from the union find and the lookup map.

val find_new_root : (TUF.ValMap.key * Z.t) TMap.t -> ((Goblint_lib__UnionFind.term * Z.t) * int) TUF.ValMap.t -> TMap.key -> ((Goblint_lib__UnionFind.term * Z.t) * int) TUF.ValMap.t * (Goblint_lib__UnionFind.term * Z.t) option

Find the representative term of the equivalence classes of an element that has already been deleted from the data structure. Returns None if there are no elements in the same equivalence class as t before it was deleted.

val remove_terms_from_diseq : TSet.t ZMap.t TMap.t -> (TUF.ValMap.key * Z.t) TMap.t -> data -> data
val remove_terms_from_bldis : BlDis.t -> (TUF.ValMap.key * Z.t) TMap.t -> data -> TUF.t * TSet.t TMap.t
val remove_terms : (Goblint_lib__UnionFind.term -> bool) -> data -> data
val join_eq : data -> data -> data * (Goblint_lib__UnionFind.term * Goblint_lib__UnionFind.term * Z.t, TSet.elt * Z.t) Batteries.Map.t

Join version 1: by using the automaton. The product automaton of cc1 and cc2 is computed and then we add the terms to the right equivalence class. We also add new terms in order to have some terms for each state in the automaton.

val product_no_automata_over_terms : data -> data -> TSet.t -> data * (Goblint_lib__UnionFind.term * Goblint_lib__UnionFind.term * Z.t, TSet.elt * Z.t) Batteries.Map.t

Join version 2: just look at equivalence classes and not the automaton.

val join_eq_no_automata : data -> data -> data * (Goblint_lib__UnionFind.term * Goblint_lib__UnionFind.term * Z.t, TSet.elt * Z.t) Batteries.Map.t

Here we do the join without using the automata. We construct a new cc that contains the elements of cc1.set U cc2.set. and two elements are in the same equivalence class iff they are in the same eq. class both in cc1 and in cc2.

val widen_eq_no_automata : data -> data -> data * (Goblint_lib__UnionFind.term * Goblint_lib__UnionFind.term * Z.t, TSet.elt * Z.t) Batteries.Map.t

Same as join, but we only take the terms from the left argument.

val join_neq : TSet.t ZMap.t TMap.t -> TSet.t ZMap.t TMap.t -> data -> data -> data -> BatSet.Make(Goblint_lib__UnionFind.T).t BatMap.Make(Z).t BatMap.Make(Goblint_lib__UnionFind.T).t -> BatSet.Make(Goblint_lib__UnionFind.T).t BatMap.Make(Z).t BatMap.Make(Goblint_lib__UnionFind.T).t -> data

Joins the disequalities diseq1 and diseq2, given a congruence closure data structure.

This is done by checking for each disequality if it is implied by both cc.

val join_bldis : TSet.t TMap.t -> TSet.t TMap.t -> data -> data -> data -> BatSet.Make(Goblint_lib__UnionFind.T).t BatMap.Make(Z).t BatMap.Make(Goblint_lib__UnionFind.T).t -> BatSet.Make(Goblint_lib__UnionFind.T).t BatMap.Make(Z).t BatMap.Make(Goblint_lib__UnionFind.T).t -> data

Joins the block disequalities bldiseq1 and bldiseq2, given a congruence closure data structure.

This is done by checking for each block disequality if it is implied by both cc.

val equal_eq_classes : data -> data -> bool

Check for equality of two congruence closures, by comparing the equivalence classes instead of computing the minimal_representative.

val equal_diseqs : data -> data -> bool
val equal_bldis : data -> data -> bool
module MayBeEqual : sig ... end

Find out if two addresses are not equal by using the MayPointTo query