This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.
<!DOCTYPE html>
<htmlxmlns="http://www.w3.org/1999/xhtml"><head><title>Biabduction__Match (infer.Biabduction__Match)</title><linkrel="stylesheet"href="../../odoc.css"/><metacharset="utf-8"/><metaname="generator"content="odoc 1.5.0"/><metaname="viewport"content="width=device-width,initial-scale=1.0"/><scriptsrc="../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><divclass="content"><header><nav><ahref="../index.html">Up</a>–<ahref="../index.html">infer</a>» Biabduction__Match</nav><h1>Module <code>Biabduction__Match</code></h1></header><aside><p>Implementation of "Smart" Pattern Matching for higher order singly-linked list predicate.</p><p>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 <ahref="http://dx.doi.org/10.1007/978-3-540-73368-3_22">CAV 2007</a> for the therory involved.</p></aside><dl><dtclass="spec value"id="val-hpara_match_with_impl"><ahref="#val-hpara_match_with_impl"class="anchor"></a><code><spanclass="keyword">val</span> hpara_match_with_impl : <ahref="../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span> bool <span>-></span><ahref="../Biabduction/Predicates/index.html#type-hpara">Biabduction.Predicates.hpara</a><span>-></span><ahref="../Biabduction/Predicates/index.html#type-hpara">Biabduction.Predicates.hpara</a><span>-></span> bool</code></dt><dtclass="spec value"id="val-hpara_dll_match_with_impl"><ahref="#val-hpara_dll_match_with_impl"class="anchor"></a><code><spanclass="keyword">val</span> hpara_dll_match_with_impl : <ahref="../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span> bool <span>-></span><ahref="../Biabduction/Predicates/index.html#type-hpara_dll">Biabduction.Predicates.hpara_dll</a><span>-></span><ahref="../Biabduction/Predicates/index.html#type-hpara_dll">Biabduction.Predicates.hpara_dll</a><span>-></span> bool</code></dt></dl><dl><dtclass="spec type"id="type-hpred_pat"><ahref="#type-hpred_pat"class="anchor"></a><code><spanclass="keyword">type</span> hpred_pat</code><code> = </code><code>{</code><tableclass="record"><trid="type-hpred_pat.hpred"class="anchored"><tdclass="def field"><ahref="#type-hpred_pat.hpred"class="anchor"></a><code>hpred : <ahref="../Biabduction/Predicates/index.html#type-hpred">Biabduction.Predicates.hpred</a>;</code></td></tr><trid="type-hpred_pat.flag"class="anchored"><tdclass="def field"><ahref="#type-hpred_pat.flag"class="anchor"></a><code>flag : bool;</code></td></tr></table><code>}</code></dt><dd><p>Type for a hpred pattern. <code>flag=false</code> means that the implication between hpreds is not considered, and <code>flag = true</code> means that it is considered during pattern matching.</p></dd></dl><dl><dtclass="spec type"id="type-sidecondition"><ahref="#type-sidecondition"class="anchor"></a><code><spanclass="keyword">type</span> sidecondition</code><code> = <span><ahref="../Biabduction/Prop/index.html#type-normal">Biabduction.Prop.normal</a><ahref="../Biabduction/Prop/index.html#type-t">Biabduction.Prop.t</a></span><span>-></span><ahref="../Biabduction/Predicates/index.html#type-subst">Biabduction.Predicates.subst</a><span>-></span> bool</code></dt></dl><dl><dtclass="spec value"id="val-prop_match_with_impl"><ahref="#val-prop_match_with_impl"class="anchor"></a><code><spanclass="keyword">val</span> prop_match_with_impl : <ahref="../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><ahref="../Biabduction/Prop/index.html#type-normal">Biabduction.Prop.normal</a><ahref="../Biabduction/Prop/index.html#type-t">Biabduction.Prop.t</a></span><span>-></span><ahref="index.html#type-sidecondition">sidecondition</a><span>-></span><span><ahref="../IR/Ident/index.html#type-t">IR.Ident.t</a> list</span><span>-></span><ahref="index.html#type-hpred_pat">hpred_pat</a><span>-></span><span><ahref="index.html#type-hpred_pat">hpred_pat</a> list</span><span>-></span><span><span>(<ahref="../Biabduction/Predicates/index.html#type-subst">Biabduction.Predicates.subst</a> * <span><ahref="../Biabduction/Prop/index.html#type-normal">Biabduction.Prop.normal</a><ahref="../Biabduction/Prop/index.html#type-t">Biabduction.Prop.t</a></span>)</span> option</span></code></dt><dd><p><code>prop_match_with_impl p condition vars hpat hpats</code> returns <code>(subst, p_leftover)</code> such that</p><ol><li><code>dom(subst) = vars</code></li><li><code>p |- (hpat.hpred * hpats.hpred)[subst] * p_leftover</code>.</li></ol><p>Using the flag <code>field</code>, we can control the strength of |-.</p></dd></dl><dl><dtclass="spec value"id="val-find_partial_iso"><ahref="#val-find_partial_iso"class="anchor"></a><code><spanclass="keyword">val</span> find_partial_iso : <ahref="../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span>(<ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span> bool)</span><span>-></span><span><span>(<ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span><span>-></span><span><span>(<ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span><span>-></span><span><ahref="../Biabduction/Predicates/index.html#type-hpred">Biabduction.Predicates.hpred</a> list</span><span>-></span><span><span>(<span><span>(<ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span> * <span><ahref="../Biabduction/Predicates/index.html#type-hpred">Biabduction.Predicates.hpred</a> list</span> * <span><ahref="../Biabduction/Predicates/index.html#type-hpred">Biabduction.Predicates.hpred</a> list</span> * <span><ahref="../Biabduction/Predicates/index.html#type-hpred">Biabduction.Predicates.hpred</a> list</span>)</span> option</span></code></dt><dd><p><code>find_partial_iso</code> 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.</p></dd></dl><dl><dtclass="spec value"id="val-hpara_iso"><ahref="#val-hpara_iso"class="anchor"></a><code><spanclass="keyword">val</span> hpara_iso : <ahref="../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><ahref="../Biabduction/Predicates/index.html#type-hpara">Biabduction.Predicates.hpara</a><span>-></span><ahref="../Biabduction/Predicates/index.html#type-hpara">Biabduction.Predicates.hpara</a><span>-></span> bool</code></dt><dd><p><code>hpara_iso</code> soundly checks whether two hparas are isomorphic.</p></dd></dl><dl><dtclass="spec value"id="val-hpara_dll_iso"><ahref="#val-hpara_dll_iso"class="anchor"></a><code><spanclass="keyword">val</span> hpara_dll_iso : <ahref="../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><ahref="../Biabduction/Predicates/index.html#type-hpara_dll">Biabduction.Predicates.hpara_dll</a><span>-></span><ahref="../Biabduction/Predicates/index.html#type-hpara_dll">Biabduction.Predicates.hpara_dll</a><span>-></span> bool</code></dt><dd><p><code>hpara_dll_iso</code> soundly checks whether two hpara_dlls are isomorphic.</p></dd></dl><dl><dtclass="spec value"id="val-hpara_create"><ahref="#val-hpara_create"class="anchor"></a><code><spanclass="keyword">val</span> hpara_create : <ahref="../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><span>(<ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span><span>-></span><span><ahref="../Biabduction/Predicates/index.html#type-hpred">Biabduction.Predicates.hpred</a> list</span><span>-></span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../Biabduction/Predicates/index.html#type-hpara">Biabduction.Predicates.hpara</a> * <span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a> list</span></code></dt><dd><p><code>hpara_create</code> 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.</p></dd></dl><dl><dtclass="spec value"id="val-hpara_dll_create"><ahref="#val-hpara_dll_create"class="anchor"></a><code><spanclass="keyword">val</span> hpara_dll_create : <ahref="../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><span>(<ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span><span>-></span><span><ahref="../Biabduction/Predicates/index.html#type-hpred">Biabduction.Predicates.hpred</a> list</span><span>-></span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../Biabduction/Predicates/index.html#type-hpara_dll">Biabduction.Predicates.hpara_dll</a> * <span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a> list</span></code></dt><dd><p><code>hpara_dll_create</code> 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.</p></dd></dl></div></body></html>
