|
|
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>BufferOverrunSemantics (infer.BO.BufferOverrunSemantics)</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> » <a href="../index.html">BO</a> » BufferOverrunSemantics</nav><h1>Module <code>BO.BufferOverrunSemantics</code></h1></header><dl><dt class="spec value" id="val-is_stack_exp"><a href="#val-is_stack_exp" class="anchor"></a><code><span class="keyword">val</span> is_stack_exp : <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="../BufferOverrunDomain/Mem/index.html#type-t">BufferOverrunDomain.Mem.t</a> <span>-></span> bool</code></dt><dd><p>Check if an expression is a stack variable such as <code>n$0</code> or local variable for C array</p></dd></dl><dl><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="../../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="../BufferOverrunDomain/Mem/index.html#type-t">BufferOverrunDomain.Mem.t</a> <span>-></span> <a href="../BufferOverrunDomain/Val/index.html#type-t">BufferOverrunDomain.Val.t</a></code></dt><dd><p>Evalute an expression</p></dd></dl><dl><dt class="spec value" id="val-eval_locs"><a href="#val-eval_locs" class="anchor"></a><code><span class="keyword">val</span> eval_locs : <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="../BufferOverrunDomain/Mem/index.html#type-t">BufferOverrunDomain.Mem.t</a> <span>-></span> <a href="../AbsLoc/PowLoc/index.html#type-t">AbsLoc.PowLoc.t</a></code></dt><dd><p><code>eval_locs exp mem</code> is like <code>eval exp mem |> Val.get_all_locs</code> but takes some shortcuts to avoid computing useless and/or problematic intermediate values</p></dd></dl><dl><dt class="spec value" id="val-eval_arr"><a href="#val-eval_arr" class="anchor"></a><code><span class="keyword">val</span> eval_arr : <a href="../../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="../BufferOverrunDomain/Mem/index.html#type-t">BufferOverrunDomain.Mem.t</a> <span>-></span> <a href="../BufferOverrunDomain/Val/index.html#type-t">BufferOverrunDomain.Val.t</a></code></dt><dd><p>Return the array value of the input expression. For example, when <code>x</code> is a program variable, <code>eval_arr x</code> returns array blocks the <code>x</code> is pointing to, on the other hand, <code>eval x</code> returns the abstract location of <code>x</code>.</p></dd></dl><dl><dt class="spec value" id="val-eval_lindex"><a href="#val-eval_lindex" class="anchor"></a><code><span class="keyword">val</span> eval_lindex : <a href="../../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="../BufferOverrunDomain/Mem/index.html#type-t">BufferOverrunDomain.Mem.t</a> <span>-></span> <a href="../BufferOverrunDomain/Val/index.html#type-t">BufferOverrunDomain.Val.t</a></code></dt><dd><p>Evaluate array location with index, i.e., <code>eval_lindex integer_type_widths array_exp index_exp mem</code></p></dd></dl><dl><dt class="spec value" id="val-eval_array_locs_length"><a href="#val-eval_array_locs_length" class="anchor"></a><code><span class="keyword">val</span> eval_array_locs_length : <a href="../AbsLoc/PowLoc/index.html#type-t">AbsLoc.PowLoc.t</a> <span>-></span> <span><span class="type-var">_</span> <a href="../BufferOverrunDomain/Mem/index.html#type-t0">BufferOverrunDomain.Mem.t0</a></span> <span>-></span> <a href="../BufferOverrunDomain/Val/index.html#type-t">BufferOverrunDomain.Val.t</a></code></dt><dd><p>Evaluate length of array locations</p></dd></dl><dl><dt class="spec value" id="val-eval_string_len"><a href="#val-eval_string_len" class="anchor"></a><code><span class="keyword">val</span> eval_string_len : <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="../BufferOverrunDomain/Mem/index.html#type-t">BufferOverrunDomain.Mem.t</a> <span>-></span> <a href="../BufferOverrunDomain/Val/index.html#type-t">BufferOverrunDomain.Val.t</a></code></dt><dd><p>Evaluate length of C string</p></dd></dl><dl><dt class="spec value" id="val-conservative_array_length"><a href="#val-conservative_array_length" class="anchor"></a><code><span class="keyword">val</span> conservative_array_length : <span>?⁠traces:<a href="../BufferOverrunTrace/Set/index.html#type-t">BufferOverrunTrace.Set.t</a></span> <span>-></span> <a href="../AbsLoc/PowLoc/index.html#type-t">AbsLoc.PowLoc.t</a> <span>-></span> <span><span class="type-var">_</span> <a href="../BufferOverrunDomain/Mem/index.html#type-t0">BufferOverrunDomain.Mem.t0</a></span> <span>-></span> <a href="../BufferOverrunDomain/Val/index.html#type-t">BufferOverrunDomain.Val.t</a></code></dt><dd><p>Evaluate the array length conservatively, which is useful when there are multiple array locations and their lengths are joined to top. For example, if the <code>arr_locs</code> points to two arrays <code>a</code> and <code>b</code> and if their lengths are <code>a.length</code> and <code>b.length</code>, this function evaluates its length as <code>[0, a.length.ub + b.length.ub]</code>.</p></dd></dl><dl><dt class="spec type" id="type-eval_mode"><a href="#type-eval_mode" class="anchor"></a><code><span class="keyword">type</span> eval_mode</code><code> = </code><table class="variant"><tr id="type-eval_mode.EvalNormal" class="anchored"><td class="def constructor"><a href="#type-eval_mode.EvalNormal" class="anchor"></a><code>| </code><code><span class="constructor">EvalNormal</span></code></td><td class="doc"><p>Given a symbolic value of an unknown function <code>Symb.SymbolPath.Callsite</code>, it returns a symbolic interval value.</p></td></tr><tr id="type-eval_mode.EvalPOCond" class="anchored"><td class="def constructor"><a href="#type-eval_mode.EvalPOCond" class="anchor"></a><code>| </code><code><span class="constructor">EvalPOCond</span></code></td><td class="doc"><p>Given a symbolic value of an unknown function, it returns the top interval value. This is used when substituting condition expressions of proof obligations.</p></td></tr><tr id="type-eval_mode.EvalPOReachability" class="anchored"><td class="def constructor"><a href="#type-eval_mode.EvalPOReachability" class="anchor"></a><code>| </code><code><span class="constructor">EvalPOReachability</span></code></td><td class="doc"><p>This is similar to <code>EvalPOCond</code>, but it returns the bottom location, instead of the unknown location, when a location to substitute is not found. This is used when substituting reachabilities of proof obligations.</p></td></tr><tr id="type-eval_mode.EvalCost" class="anchored"><td class="def constructor"><a href="#type-eval_mode.EvalCost" class="anchor"></a><code>| </code><code><span class="constructor">EvalCost</span></code></td><td class="doc"><p>This is similar to <code>EvalNormal</code>, but it is designed to be used in substitutions of the cost results, avoiding precision loss by joining of symbolic values. Normal join of two different symbolic values, <code>s1</code> and <code>s2</code>, becomes top due to the limitation of our domain. On the other hand, in this mode, it returns an upperbound <code>s1+s2</code> for the case, because the cost values only care about the upperbounds.</p></td></tr></table></dt><dd><p>Several modes of ondemand evaluations</p></dd></dl><dl><dt class="spec value" id="val-mk_eval_sym_trace"><a href="#val-mk_eval_sym_trace" class="anchor"></a><code><span class="keyword">val</span> mk_eval_sym_trace : <span>?⁠is_params_ref:bool</span> <span>-></span> <a href="../../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a> <span>-></span> <span><span>(<a href="../../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span> <span>-></span> <span><span>(<a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span> <span>-></span> <a href="../BufferOverrunDomain/Mem/index.html#type-t">BufferOverrunDomain.Mem.t</a> <span>-></span> <span>mode:<a href="index.html#type-eval_mode">eval_mode</a></span> <span>-></span> <a href="../BufferOverrunDomain/index.html#type-eval_sym_trace">BufferOverrunDomain.eval_sym_trace</a></code></dt><dd><p>Make <code>eval_sym</code> function for on-demand symbol evaluation</p></dd></dl><dl><dt class="spec value" id="val-mk_eval_sym_cost"><a href="#val-mk_eval_sym_cost" class="anchor"></a><code><span class="keyword">val</span> mk_eval_sym_cost : <a href="../../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a> <span>-></span> <span><span>(<a href="../../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span> <span>-></span> <span><span>(<a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span> <span>-></span> <a href="../BufferOverrunDomain/Mem/index.html#type-t">BufferOverrunDomain.Mem.t</a> <span>-></span> <a href="../BufferOverrunDomain/index.html#type-eval_sym_trace">BufferOverrunDomain.eval_sym_trace</a></code></dt><dd><p>Make <code>eval_sym</code> function of <code>EvalCost</code> mode for on-demand symbol evaluation</p></dd></dl><div class="spec module" id="module-Prune"><a href="#module-Prune" class="anchor"></a><code><span class="keyword">module</span> <a href="Prune/index.html">Prune</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div></div></body></html> |
