Module Biabduction.Match

Implementation of "Smart" Pattern Matching for higher order singly-linked list predicate.

Used for detecting on a given program if some data scructures are matching some predefined higher-order list predicates. When it is the case, these predicates can be used as possible candidates for abstracting the data-structures. See CAV 2007 for the therory involved.

val hpara_match_with_impl : IR.Tenv.t -> bool -> Predicates.hpara -> Predicates.hpara -> bool
val hpara_dll_match_with_impl : IR.Tenv.t -> bool -> Predicates.hpara_dll -> Predicates.hpara_dll -> bool
type hpred_pat = {
  1. hpred : Predicates.hpred;
  2. flag : bool;
}

Type for a hpred pattern. flag=false means that the implication between hpreds is not considered, and flag = true means that it is considered during pattern matching.

type sidecondition = Prop.normal Prop.t -> Predicates.subst -> bool
val prop_match_with_impl : IR.Tenv.t -> Prop.normal Prop.t -> sidecondition -> IR.Ident.t list -> hpred_pat -> hpred_pat list -> (Predicates.subst * Prop.normal Prop.t) option

prop_match_with_impl p condition vars hpat hpats returns (subst, p_leftover) such that

  1. dom(subst) = vars
  2. p |- (hpat.hpred * hpats.hpred)[subst] * p_leftover.

Using the flag field, we can control the strength of |-.

val find_partial_iso : IR.Tenv.t -> (IR.Exp.t -> IR.Exp.t -> bool) -> (IR.Exp.t * IR.Exp.t) list -> (IR.Exp.t * IR.Exp.t) list -> Predicates.hpred list -> ((IR.Exp.t * IR.Exp.t) list * Predicates.hpred list * Predicates.hpred list * Predicates.hpred list) option

find_partial_iso finds disjoint isomorphic sub-sigmas inside a given sigma. The first argument is an equality checker. The function returns a partial iso and three sigmas. The first sigma is the first copy of the two isomorphic sigmas, so it uses expressions in the domain of the returned isomorphism. The second is the second copy of the two isomorphic sigmas, and it uses expressions in the range of the isomorphism. The third is the unused part of the input sigma.

val hpara_iso : IR.Tenv.t -> Predicates.hpara -> Predicates.hpara -> bool

hpara_iso soundly checks whether two hparas are isomorphic.

val hpara_dll_iso : IR.Tenv.t -> Predicates.hpara_dll -> Predicates.hpara_dll -> bool

hpara_dll_iso soundly checks whether two hpara_dlls are isomorphic.

val hpara_create : IR.Tenv.t -> (IR.Exp.t * IR.Exp.t) list -> Predicates.hpred list -> IR.Exp.t -> IR.Exp.t -> Predicates.hpara * IR.Exp.t list

hpara_create takes a correspondence, and a sigma, a root and a next for the first part of this correspondence. Then, it creates a hpara and discovers a list of shared expressions that are passed as arguments to hpara. Both of them are returned as a result.

val hpara_dll_create : IR.Tenv.t -> (IR.Exp.t * IR.Exp.t) list -> Predicates.hpred list -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t -> Predicates.hpara_dll * IR.Exp.t list

hpara_dll_create takes a correspondence, and a sigma, a root, a blink and a flink for the first part of this correspondence. Then, it creates a hpara_dll and discovers a list of shared expressions that are passed as arguments to hpara. Both of them are returned as a result.