You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
21 lines
12 KiB
21 lines
12 KiB
5 years ago
|
<!DOCTYPE html>
|
||
|
|
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Match (infer.InferModules.Match)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><meta name="generator" content="doc-ock-html v1.0.0-1-g1fc9bf0"/></head><body><nav id="top"><a href="../index.html">Up</a> — <span class="package">package <a href="../../index.html">infer</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">InferModules.Match</span></h1></header><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 <a href="http://dx.doi.org/10.1007/978-3-540-73368-3_22">CAV 2007</a> for the therory involved.</p><div class="spec val" id="val-hpara_match_with_impl"><a href="#val-hpara_match_with_impl" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hpara_match_with_impl : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> bool <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara">InferIR.Sil.hpara</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara">InferIR.Sil.hpara</a> <span class="keyword">‑></span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-hpara_dll_match_with_impl"><a href="#val-hpara_dll_match_with_impl" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hpara_dll_match_with_impl : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> bool <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara_dll">InferIR.Sil.hpara_dll</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara_dll">InferIR.Sil.hpara_dll</a> <span class="keyword">‑></span> bool</code></div><div class="doc"></div></div><div class="spec type" id="type-hpred_pat"><a href="#type-hpred_pat" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hpred_pat</code><code></code><code><span class="keyword"> = </span></code><code>{</code><table class="record"><tr id="type-hpred_pat.hpred" class="anchored"><td class="def field"><a href="#type-hpred_pat.hpred" class="anchor"></a><code>hpred : <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a>;</code></td></tr><tr id="type-hpred_pat.flag" class="anchored"><td class="def field"><a href="#type-hpred_pat.flag" class="anchor"></a><code>flag : bool;</code></td></tr></table><code>}</code><code></code></div><div class="doc"><p>Type for a hpred pattern. <code class="code">flag=false</code> means that the implication
|
||
|
|
between hpreds is not considered, and <code class="code">flag = true</code> means that it is
|
||
|
|
considered during pattern matching.</p></div></div><div class="spec type" id="type-sidecondition"><a href="#type-sidecondition" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>sidecondition</code><code><span class="keyword"> = </span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-exp_subst">InferIR.Sil.exp_subst</a> <span class="keyword">‑></span> bool</code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-prop_match_with_impl"><a href="#val-prop_match_with_impl" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_match_with_impl : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a> <span class="keyword">‑></span> <a href="index.html#type-sidecondition">sidecondition</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a> list <span class="keyword">‑></span> <a href="index.html#type-hpred_pat">hpred_pat</a> <span class="keyword">‑></span> <a href="index.html#type-hpred_pat">hpred_pat</a> list <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Sil/index.html#type-exp_subst">InferIR.Sil.exp_subst</a><span class="keyword"> * </span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a>) option</code></div><div class="doc"><p><code class="code">prop_match_with_impl p condition vars hpat hpats</code>
|
||
|
|
returns <code class="code">(subst, p_leftover)</code> such that
|
||
|
|
1) <code class="code">dom(subst) = vars</code>
|
||
|
|
2) <code class="code">p |- (hpat.hpred * hpats.hpred)[subst] * p_leftover</code>.
|
||
|
|
Using the flag <code class="code">field</code>, we can control the strength of |-.</p></div></div><div class="spec val" id="val-find_partial_iso"><a href="#val-find_partial_iso" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>find_partial_iso : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> bool) <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a>) list <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a>) list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list <span class="keyword">‑></span> ((<a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a>) list<span class="keyword"> * </span><a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list<span class="keyword"> * </span><a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list<span class="keyword"> * </span><a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list) option</code></div><div class="doc"><p><code class="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></div></div><div class="spec val" id="val-hpara_iso"><a href="#val-hpara_iso" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hpara_iso : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara">InferIR.Sil.hpara</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara">InferIR.Sil.hpara</a> <span class="keyword">‑></span> bool</code></div><div class="doc"><p><code class="code">hpara_iso</code> soundly checks whether two hparas are isomorphic.</p></div></div><div class="spec val" id="val-hpara_dll_iso"><a href="#val-hpara_dll_iso" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hpara_dll_iso : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara_dll">InferIR.Sil.hpara_dll</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara_dll">InferIR.Sil.hpara_dll</a> <span class="keyword">‑></span> bool</code></div><div class="doc"><p><code class="code">hpara_dll_iso</code> soundly checks whether two hpara_dlls are isomorphic.</p></div></div><div class="spec val" id="val-hpara_create"><a href="#val-hpara_create" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hpara_create : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a>) list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara">InferIR.Sil.hpara</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> list</code></div><div class="doc"><p><code class="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></div></div><div class="spec val" id="val-hpara_dll_create"><a href="#val-hpara_dll_create" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hpara_dll_create : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a>) list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara_dll">InferIR.Sil.hpara_dll</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> list</code></div><div class="doc"><p><code class="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></div></div></body></html>
|