Module Goblint_lib.UnionFind

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.

module M = Messages
exception Unsat
val compare_exp : 'a -> 'b -> int
val equal_exp : 'a -> 'b -> bool
val hash_exp : 'a -> int
type 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 =
  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 : sig ... end

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 : sig ... end
module TSet : sig ... end
module UnionFind : sig ... end

Quantitative union find

module ZMap : sig ... end
module LookupMap : sig ... end

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').