|
|
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Pulselib__PulseAbductiveDomain (infer.Pulselib__PulseAbductiveDomain)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../index.html">infer</a> » Pulselib__PulseAbductiveDomain</nav><h1>Module <code>Pulselib__PulseAbductiveDomain</code></h1></header><div class="spec module" id="module-BaseDomain"><a href="#module-BaseDomain" class="anchor"></a><code><span class="keyword">module</span> BaseDomain = <a href="../Pulselib/index.html#module-PulseBaseDomain">Pulselib.PulseBaseDomain</a></code></div><div class="spec module" id="module-BaseMemory"><a href="#module-BaseMemory" class="anchor"></a><code><span class="keyword">module</span> BaseMemory = <a href="../Pulselib/index.html#module-PulseBaseMemory">Pulselib.PulseBaseMemory</a></code></div><div class="spec module" id="module-BaseStack"><a href="#module-BaseStack" class="anchor"></a><code><span class="keyword">module</span> BaseStack = <a href="../Pulselib/index.html#module-PulseBaseStack">Pulselib.PulseBaseStack</a></code></div><aside><p>Layer on top of <a href="BaseDomain/index.html"><code>BaseDomain</code></a> to propagate operations on the current state to the pre-condition when necessary</p><p>The abstract type <code>t</code> is a pre/post pair in the style of biabduction.</p></aside><dl><dt class="spec module-type" id="module-type-BaseDomainSig"><a href="#module-type-BaseDomainSig" class="anchor"></a><code><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-BaseDomainSig/index.html">BaseDomainSig</a> = <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>signature common to the "normal" <code>Domain</code>, representing the post at the current program point, and the inverted <code>PreDomain</code>, representing the inferred pre-condition</p></dd></dl><dl><dt class="spec module" id="module-PostDomain"><a href="#module-PostDomain" class="anchor"></a><code><span class="keyword">module</span> <a href="PostDomain/index.html">PostDomain</a> : <a href="index.html#module-type-BaseDomainSig">BaseDomainSig</a></code></dt><dd><p>The post abstract state at each program point, or current state.</p></dd></dl><dl><dt class="spec module" id="module-PreDomain"><a href="#module-PreDomain" class="anchor"></a><code><span class="keyword">module</span> <a href="PreDomain/index.html">PreDomain</a> : <a href="index.html#module-type-BaseDomainSig">BaseDomainSig</a></code></dt><dd><p>The inferred pre-condition at each program point, biabduction style.</p></dd></dl><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <span class="keyword">private</span> </code><code>{</code><table class="record"><tr id="type-t.post" class="anchored"><td class="def field"><a href="#type-t.post" class="anchor"></a><code>post : <a href="PostDomain/index.html#type-t">PostDomain.t</a>;</code></td><td class="doc"><p>state at the current program point</p></td></tr><tr id="type-t.pre" class="anchored"><td class="def field"><a href="#type-t.pre" class="anchor"></a><code>pre : <a href="PreDomain/index.html#type-t">PreDomain.t</a>;</code></td><td class="doc"><p>inferred procedure pre-condition leading to the current program point</p></td></tr><tr id="type-t.path_condition" class="anchored"><td class="def field"><a href="#type-t.path_condition" class="anchor"></a><code>path_condition : <a href="../Pulselib/PulsePathCondition/index.html#type-t">Pulselib.PulseBasicInterface.PathCondition.t</a>;</code></td><td class="doc"><p>arithmetic facts true along the path (holding for both <code>pre</code> and <code>post</code> since abstract values are immutable)</p></td></tr><tr id="type-t.topl" class="anchored"><td class="def field"><a href="#type-t.topl" class="anchor"></a><code>topl : <a href="../Pulselib/PulseTopl/index.html#type-state">Pulselib.PulseTopl.state</a>;</code></td><td class="doc"><p>state at of the Topl monitor at the current program point, when Topl is enabled</p></td></tr><tr id="type-t.skipped_calls" class="anchored"><td class="def field"><a href="#type-t.skipped_calls" class="anchor"></a><code>skipped_calls : <a href="../Pulselib/PulseSkippedCalls/index.html#type-t">Pulselib.PulseBasicInterface.SkippedCalls.t</a>;</code></td><td class="doc"><p>metadata: procedure calls for which no summary was found</p></td></tr></table><code>}</code></dt><dd><p>pre/post on a single program path</p></dd></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> bool</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <span>lhs:<a href="index.html#type-t">t</a></span> <span>-></span> <span>rhs:<a href="index.html#type-t">t</a></span> <span>-></span> bool</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : Stdlib.Format.formatter <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> unit</code></dt><dt class="spec value" id="val-mk_initial"><a href="#val-mk_initial" class="anchor"></a><code><span class="keyword">val</span> mk_initial : <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <a href="../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-get_pre"><a href="#val-get_pre" class="anchor"></a><code><span class="keyword">val</span> get_pre : <a href="index.html#type-t">t</a> <span>-></span> <a href="../Pulselib/PulseBaseDomain/index.html#type-t">BaseDomain.t</a></code></dt><dt class="spec value" id="val-get_post"><a href="#val-get_post" class="anchor"></a><code><span class="keyword">val</span> get_post : <a href="index.html#type-t">t</a> <span>-></span> <a href="../Pulselib/PulseBaseDomain/index.html#type-t">BaseDomain.t</a></code></dt></dl><dl><dt class="spec module" id="module-Stack"><a href="#module-Stack" class="anchor"></a><code><span class="keyword">module</span> <a href="Stack/index.html">Stack</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>stack operations like <a href="BaseStack/index.html"><code>BaseStack</code></a> but that also take care of propagating facts to the precondition</p></dd></dl><dl><dt class="spec module" id="module-Memory"><a href="#module-Memory" class="anchor"></a><code><span class="keyword">module</span> <a href="Memory/index.html">Memory</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>memory operations like <a href="BaseMemory/index.html"><code>BaseMemory</code></a> but that also take care of propagating facts to the precondition</p></dd></dl><dl><dt class="spec module" id="module-AddressAttributes"><a href="#module-AddressAttributes" class="anchor"></a><code><span class="keyword">module</span> <a href="AddressAttributes/index.html">AddressAttributes</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>attribute operations like <code>BaseAddressAttributes</code> but that also take care of propagating facts to the precondition</p></dd></dl><dl><dt class="spec value" id="val-is_local"><a href="#val-is_local" class="anchor"></a><code><span class="keyword">val</span> is_local : <a href="../IR/Var/index.html#type-t">IR.Var.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> bool</code></dt><dt class="spec value" id="val-find_post_cell_opt"><a href="#val-find_post_cell_opt" class="anchor"></a><code><span class="keyword">val</span> find_post_cell_opt : <a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="../Pulselib/PulseBaseDomain/index.html#type-cell">BaseDomain.cell</a> option</span></code></dt><dt class="spec value" id="val-get_unreachable_attributes"><a href="#val-get_unreachable_attributes" class="anchor"></a><code><span class="keyword">val</span> get_unreachable_attributes : <a href="index.html#type-t">t</a> <span>-></span> <span><a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> list</span></code></dt><dd><p>collect the addresses that have attributes but are unreachable in the current post-condition</p></dd></dl><dl><dt class="spec value" id="val-add_skipped_call"><a href="#val-add_skipped_call" class="anchor"></a><code><span class="keyword">val</span> add_skipped_call : <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>-></span> <a href="../Pulselib/PulseTrace/index.html#type-t">Pulselib.PulseBasicInterface.Trace.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-add_skipped_calls"><a href="#val-add_skipped_calls" class="anchor"></a><code><span class="keyword">val</span> add_skipped_calls : <a href="../Pulselib/PulseSkippedCalls/index.html#type-t">Pulselib.PulseBasicInterface.SkippedCalls.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-set_path_condition"><a href="#val-set_path_condition" class="anchor"></a><code><span class="keyword">val</span> set_path_condition : <a href="../Pulselib/PulsePathCondition/index.html#type-t">Pulselib.PulseBasicInterface.PathCondition.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-is_isl_without_allocation"><a href="#val-is_isl_without_allocation" class="anchor"></a><code><span class="keyword">val</span> is_isl_without_allocation : <a href="index.html#type-t">t</a> <span>-></span> bool</code></dt><dt class="spec value" id="val-is_pre_without_isl_abduced"><a href="#val-is_pre_without_isl_abduced" class="anchor"></a><code><span class="keyword">val</span> is_pre_without_isl_abduced : <a href="index.html#type-t">t</a> <span>-></span> bool</code></dt></dl><dl><dt class="spec type" id="type-summary"><a href="#type-summary" class="anchor"></a><code><span class="keyword">type</span> summary</code><code> = <span class="keyword">private</span> <a href="index.html#type-t">t</a></code></dt><dd><p>private type to make sure <a href="index.html#val-summary_of_post"><code>summary_of_post</code></a> is always called when creating summaries</p></dd></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_summary"><a href="#val-compare_summary" class="anchor"></a><code><span class="keyword">val</span> compare_summary : <a href="index.html#type-summary">summary</a> <span>-></span> <a href="index.html#type-summary">summary</a> <span>-></span> int</code></dt><dt class="spec value" id="val-equal_summary"><a href="#val-equal_summary" class="anchor"></a><code><span class="keyword">val</span> equal_summary : <a href="index.html#type-summary">summary</a> <span>-></span> <a href="index.html#type-summary">summary</a> <span>-></span> bool</code></dt><dt class="spec value" id="val-yojson_of_summary"><a href="#val-yojson_of_summary" class="anchor"></a><code><span class="keyword">val</span> yojson_of_summary : <a href="index.html#type-summary">summary</a> <span>-></span> Ppx_yojson_conv_lib.Yojson.Safe.t</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-skipped_calls_match_pattern"><a href="#val-skipped_calls_match_pattern" class="anchor"></a><code><span class="keyword">val</span> skipped_calls_match_pattern : <a href="index.html#type-summary">summary</a> <span>-></span> bool</code></dt><dt class="spec value" id="val-summary_of_post"><a href="#val-summary_of_post" class="anchor"></a><code><span class="keyword">val</span> summary_of_post : <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <a href="../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> <span>-></span> <a href="../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><span><span>(<a href="index.html#type-summary">summary</a>, <span>[> <span>`MemoryLeak of <a href="index.html#type-summary">summary</a> * <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a> * <a href="../Pulselib/PulseTrace/index.html#type-t">Pulselib.PulseBasicInterface.Trace.t</a> * <a href="../IBase/Location/index.html#type-t">IBase.Location.t</a></span> <span><span>| `PotentialInvalidAccessSummary</span> of <a href="index.html#type-summary">summary</a> * <a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <span>(<a href="../Pulselib/PulseTrace/index.html#type-t">Pulselib.PulseBasicInterface.Trace.t</a> * <span><a href="../Pulselib/PulseInvalidation/index.html#type-must_be_valid_reason">Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason</a> option</span>)</span></span> ]</span>)</span> <a href="../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.result</span> <a href="../Pulselib/PulseSatUnsat/index.html#type-t">Pulselib.PulseBasicInterface.SatUnsat.t</a></span></code></dt><dd><p>Trim the state down to just the procedure's interface (formals and globals), and simplify and normalize the state.</p></dd></dl><dl><dt class="spec value" id="val-set_post_edges"><a href="#val-set_post_edges" class="anchor"></a><code><span class="keyword">val</span> set_post_edges : <a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> <span>-></span> <a href="../Pulselib__PulseBaseMemory/Edges/index.html#type-t">BaseMemory.Edges.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dd><p>directly set the edges for the given address, bypassing abduction altogether</p></dd></dl><dl><dt class="spec value" id="val-set_post_cell"><a href="#val-set_post_cell" class="anchor"></a><code><span class="keyword">val</span> set_post_cell : <span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> <span>-></span> <a href="../Pulselib/PulseBaseDomain/index.html#type-cell">BaseDomain.cell</a> <span>-></span> <a href="../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dd><p>directly set the edges and attributes for the given address, bypassing abduction altogether</p></dd></dl><dl><dt class="spec value" id="val-incorporate_new_eqs"><a href="#val-incorporate_new_eqs" class="anchor"></a><code><span class="keyword">val</span> incorporate_new_eqs : <a href="../Pulselib/PulsePathCondition/index.html#type-new_eqs">Pulselib.PulseBasicInterface.PathCondition.new_eqs</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><span>(<a href="index.html#type-t">t</a>, <span>[> <span>`PotentialInvalidAccess of <a href="index.html#type-t">t</a> * <a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <span>(<a href="../Pulselib/PulseTrace/index.html#type-t">Pulselib.PulseBasicInterface.Trace.t</a> * <span><a href="../Pulselib/PulseInvalidation/index.html#type-must_be_valid_reason">Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason</a> option</span>)</span></span> ]</span>)</span> <a href="../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.result</span></code></dt><dd><p>Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. <code>x = 0</code> is not compatible with <code>x</code> being allocated, and <code>x = y</code> is not compatible with <code>x</code> and <code>y</code> being allocated separately. In those cases, the resulting path condition is <span class="xref-unresolved" title="unresolved reference to "PathCondition.false_""><code>PathCondition</code>.false_</span>.</p></dd></dl><dl><dt class="spec value" id="val-initialize"><a href="#val-initialize" class="anchor"></a><code><span class="keyword">val</span> initialize : <a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dd><p>Remove "Uninitialized" attribute of the given address</p></dd></dl><dl><dt class="spec value" id="val-set_uninitialized"><a href="#val-set_uninitialized" class="anchor"></a><code><span class="keyword">val</span> set_uninitialized : <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span>[ <span>`LocalDecl of <a href="../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <span><a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> option</span></span> <span><span>| `Malloc</span> of <a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a></span> ]</span> <span>-></span> <a href="../IR/Typ/index.html#type-t">IR.Typ.t</a> <span>-></span> <a href="../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dd><p>Add "Uninitialized" attributes when a variable is declared or a memory is allocated by malloc.</p></dd></dl><div class="spec module" id="module-Topl"><a href="#module-Topl" class="anchor"></a><code><span class="keyword">module</span> <a href="Topl/index.html">Topl</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div></div></body></html> |
