This file contains invisible Unicode characters that may be processed differently from what appears below. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to reveal hidden characters.
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>InferIR__Exp (InferIR.InferIR__Exp)</title><linkrel="stylesheet"href="../../odoc.css"/><metacharset="utf-8"/><metaname="generator"content="odoc %%VERSION%%"/><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">InferIR</a>» InferIR__Exp</nav><h1>Module <code>InferIR__Exp</code></h1><p>The Smallfoot Intermediate Language: Expressions</p><p>NOTE: For doing substitutionson expressions, there are some functions in <code>Sil</code>.</p><navclass="toc"><ul><li><ahref="#utility-functions-for-expressions">Utility Functions for Expressions</a></li></ul></nav></header><divclass="spec module"id="module-F"><ahref="#module-F"class="anchor"></a><code><spanclass="keyword">module</span> F = Stdlib.Format</code></div><dl><dtclass="spec type"id="type-closure"><ahref="#type-closure"class="anchor"></a><code><spanclass="keyword">type</span> closure</code><code> = </code><code>{</code><tableclass="record"><trid="type-closure.name"class="anchored"><tdclass="def field"><ahref="#type-closure.name"class="anchor"></a><code>name : <ahref="../InferIR/Typ/Procname/index.html#type-t">InferIR.Typ.Procname.t</a>;</code></td></tr><trid="type-closure.captured_vars"class="anchored"><tdclass="def field"><ahref="#type-closure.captured_vars"class="anchor"></a><code>captured_vars : <span><span>(<ahref="index.html#type-t">t</a> * <ahref="../InferIR/Pvar/index.html#type-t">InferIR.Pvar.t</a> * <ahref="../InferIR/Typ/index.html#type-t">InferIR.Typ.t</a>)</span> list</span>;</code></td></tr></table><code>}</code></dt><dtclass="spec type"id="type-sizeof_data"><ahref="#type-sizeof_data"class="anchor"></a><code><spanclass="keyword">and</span> sizeof_data</code><code> = </code><code>{</code><tableclass="record"><trid="type-sizeof_data.typ"class="anchored"><tdclass="def field"><ahref="#type-sizeof_data.typ"class="anchor"></a><code>typ : <ahref="../InferIR/Typ/index.html#type-t">InferIR.Typ.t</a>;</code></td></tr><trid="type-sizeof_data.nbytes"class="anchored"><tdclass="def field"><ahref="#type-sizeof_data.nbytes"class="anchor"></a><code>nbytes : <span>int option</span>;</code></td></tr><trid="type-sizeof_data.dynamic_length"class="anchored"><tdclass="def field"><ahref="#type-sizeof_data.dynamic_length"class="anchor"></a><code>dynamic_length : <span><ahref="index.html#type-t">t</a> option</span>;</code></td></tr><trid="type-sizeof_data.subtype"class="anchored"><tdclass="def field"><ahref="#type-sizeof_data.subtype"class="anchor"></a><code>subtype : <ahref="../InferIR/Subtype/index.html#type-t">InferIR.Subtype.t</a>;</code></td></tr></table><code>}</code></dt><dd><p>This records information about a <code>sizeof(typ)</code> expression.</p><p><code>nbytes</code> represents the result of the evaluation of <code>sizeof(typ)</code> if it is statically known.</p><p>If <code>typ</code> is of the form <code>Tarray elt (Some static_length)</code>, then <code>dynamic_length</code> is the number of elements of type <code>elt</code> in the array. The <code>dynamic_length</code>, tracked by symbolic execution, may differ from the <code>static_length</code> obtained from the type definition, e.g. when an array is over-allocated.</p><p>If <code>typ</code> is a struct type, the <code>dynamic_length</code> is that of the final extensible array, if any.</p></dd></dl><dl><dtclass="spec type"id="type-t"><ahref="#type-t"class="anchor"></a><code><spanclass="keyword">and</span> t</code><code> = </code><tableclass="variant"><trid="type-t.Var"class="anchored"><tdclass="def constructor"><ahref="#type-t.Var"class="anchor"></a><code>| </code><code><spanclass="constructor">Var</span><spanclass="keyword">of</span><ahref="../InferIR/Ident/index.html#type-t">InferIR.Ident.t</a></code></td><tdclass="doc"><p>Pure variable: it is not an lvalue</p></td></tr><trid="type-t.UnOp"class="anchored"><tdclass="def constructor"><ahref="#type-t.UnOp"class="anchor"></a><code>| </code><code><spanclass="constructor">UnOp</span><spanclass="keyword">of</span><ahref="../InferIR/Unop/index.html#type-t">InferIR.Unop.t</a> * <ahref="index.html#type-t">t</a> * <span><ahref="../InferIR/Typ/index.html#type-t">InferIR.Typ.t</a> option</span></code></td><tdclass="doc"><p>Unary operator with type of the result if known</p></td></tr><trid="type-t.BinOp"class="anchored"><tdclass="def constructor"><ahref="#type-t.BinOp"class="anchor"></a><code>| </code><code><spanclass="constructor">BinOp</span><spanclass="keyword">of</span><ahref="../InferIR/Binop/index.html#type-t">InferIR.Binop.t</a> * <ahref="index.html#type-t">t</a> * <ahref="index.html#type-t">t</a></code></td><tdclass="doc"><p>Binary operator</p></td></tr><trid="type-t.Exn"class="anchored"><tdclass="def constructor"><ahref="#type-t.Exn"class="anchor"></a><code>| </code><code><spanclass="constructor">Exn</span><spanclass="keyword">of</span><ahref="index.html#type-t">t</a></code></td><tdclass="doc"><p>Exception</p></td></tr><trid="type-t.Closure"class="anchored"><tdclass="def constructor"><ahref="#type-t.Closure"class="anchor"></a><code>| </code><code><spanclass="constructor">Closure</span><spanclass="keyword">of</span><ahref="index.html#type-closure">closure</a></code></td><tdclass="doc"><p>Anonymous function</p></td></tr><trid="type-t.Const"class="anchored"><tdclass="def constructor"><ahref="#type-t.Const"class="anchor"></a><code>| </code><code><spanclass="constructor">Const</span><spanclass="keyword">of</span><ahref="../InferIR/Const/index.html#type-t">InferIR.Const.t</a></code></td><tdclass="doc"><p>Constants</p></td></tr><trid="type-t.Cast"class="anchored"><tdclass="def constructor"><ahref="#type-t.Cast"class="anchor"></a><code>| </code><code><spanclass="constructor">Cast</span><spanclass="keyword">of</span><ahref="../InferIR/Typ/index.html#type-t">InferIR.Typ.t</a> * <ahref="index.html#type-t">t</a></code></td><tdclass="doc"><p>Type cast</p></td></tr><trid="type-t.Lvar"class="anchored"><tdclass="def constructor"><ahref="#type-t.Lvar"class="anchor"></a><code>| </code><code><spanclass="constructor">Lvar</span><spanclass="keyword">of</span><ahref="../InferIR/Pvar/index.html#type-t">InferIR.Pvar.t</a></code></td><tdclass="doc"><p>The address of a program variable</p></td></tr><trid="type-t.Lfield"class="anchored"><tdclass="def constructor"><ahref="#type-t.Lfield"class="anchor"></a><code>| </code><code><spanclass="constructor">Lfield</span><spanclass="keyword">of</span><ahref="index.html#type-t">t</a> * <ahref="../InferIR/Typ/Fieldname/index.html#type-t">InferIR.Typ.Fieldname.t</a> * <ahref="../InferIR/Typ/index.html#type-t">InferIR.Typ.t</a></code></td><tdclass="doc"><p>A field offset, the type is the surrounding struct type</p></td></tr><trid="type-t.Lindex"class="anchored"><tdclass="def constructor"><ahref="#type-t.Lindex"class="anchor"></a><code>| </code><code><spanclass="constructor">Lindex</span><spanclass="keyword">of</span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-t">t</a></code></td><tdclass="doc"><p>An array index offset: <code>exp1[exp2]</code></p></td></tr><trid="type-t.Sizeof"class="anchored"><tdclass="def constructor"><ahref="#type-t.Sizeof"class="anchor"></a><code>| </code><code><spanclass="constructor">Sizeof</span><spanclass="keyword">of</span><ahref="index.html#type-sizeof_data">sizeof_data</a></code></td></tr></table></dt><dd><p>Program expressions.</p></dd></dl><div><divclass="spec include"><divclass="doc"><dl><dtclass="spec value"id="val-compare_closure"><ahref="#val-compare_closure"class="anchor"></a><code><spanclass="keyword">val</span> compare_closure : <ahref="index.html#type-closure">closure</a><span>-></span><ahref="index.html#type-closure">closure</a><span>-></span> int</code></dt><dtclass="spec value"id="val-compare_sizeof_data"><ahref="#val-compare_sizeof_data"class="anchor"></a><code><spanclass="keyword">val</span> compare_sizeof_data : <ahref="index.html#type-sizeof_data">sizeof_data</a><span>-></span><ahref="index.html#type-sizeof_data">sizeof_data</a><span>-></span> int</code></dt><dtclass="spec value"id="val-compare"><ahref="#val-compare"class="anchor"></a><code><spanclass="keyword">val</span> compare : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span> int</code></dt></dl></div></div></div><dl><dtclass="spec value"id="val-equal"><ahref="#val-equal"class="anchor"></a><code><spanclass="keyword">val</span> equal : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dd><p>Equality for expressions.</p></dd></dl><dl><dtclass="spec module"id="module-Set"><ahref="#module-Set"class="anchor"></a><code><spanclass="keyword">module</span> Set : <ahref="../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Caml.Set.S <spanclass="keyword">with</span><spanclass="keyword">type</span><ahref="index.html#module-Set">Set</a>.elt = <ahref="index.html#type-t">t</a></code></dt><dd><p>Set of expressions.</p></dd></dl><dl><dtclass="spec module"id="module-Map"><ahref="#module-Map"class="anchor"></a><code><spanclass="keyword">module</span> Map : <ahref="../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Caml.Map.S <spanclass="keyword">with</span><spanclass="keyword">type</span><ahref="index.html#module-Map">Map</a>.key = <ahref="index.html#type-t">t</a></code></dt><dd><p>Map with expression keys.</p></dd></dl><dl><dtclass="spec module"id="module-Hash"><ahref="#module-Hash"class="anchor"></a><code><spanclass="keyword">module</span> Hash : <ahref="../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Caml.Hashtbl.S <spanclass="keyword">with</span><spanclass="keyword">type</span><ahref="index.html#module-Hash">Hash</a>.key = <ahref="index.html#type-t">t</a></code></dt><dd><p>Hashtable with expression keys.</p></dd></dl><dl><dtclass="spec value"id="val-is_null_literal"><ahref="#val-is_null_literal"class="anchor"></a><code><spanclass="keyword">val</span> is_null_literal : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dtclass="spec value"id="val-is_this"><ahref="#val-is_this"class="anchor"></a><code><spanclass="keyword">val</span> is_this : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dd><p>return true if <code>exp</code> is the special this/self expression</p></dd></dl><dl><dtclass="spec value"id="val-is_zero"><ahref="#val-is_zero"class="anchor"></a><code><spanclass="keyword">val</span> is_zero : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dtclass="spec value"id="val-is_const"><ahref="#val-is_const"class="anchor"></a><code><spanclass="keyword">val</span> is_const : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt></dl><section><header><h3id="utility-functions-for-expressions"><ahref="#utility-functions-for-expressions"class="anchor"></a>Utility Functions for Expressions</h3></header><dl><dtclass="spec value"id="val-texp_to_typ"><ahref="#val-texp_to_typ"class="anchor"></a><code><spanclass="keyword">val</span> texp_to_typ : <span><ahref="../InferIR/Typ/index.html#type-t">InferIR.Typ.t</a> option</span><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="../InferIR/Typ/index.html#type-t">InferIR.Typ.t</a></code></dt><dd><p>Turn an expression representing a type into the type it represents If not a sizeof, return the default type if given, otherwise raise an exception</p></dd></dl><dl><dtclass="spec value"id="val-root_of_lexp"><ahref="#val-root_of_lexp"class="anchor"></a><code><spanclass="keyword">val</span> root_of_lexp : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Return the root of <code>lexp</code>.</p></dd></dl><dl><dtclass="spec value"id="val-get_undefined"><ahref="#val-get_undefined"class="anchor"></a><code><spanclass="keyword">val</span> get_undefined : bool <span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Get an expression "undefined", the boolean indicates whether the undefined value goest into the footprint</p></dd></dl><dl><dtclass="spec value"id="val-pointer_arith"><ahref="#val-pointer_arith"class="anchor"></a><code><spanclass="keyword">val</span> pointer_arith : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dd><p>Checks whether an expression denotes a location using pointer arithmetic. Currently, catches array - indexing expressions such as a<code>i</code> only.</p></dd></dl><dl><dtclass="spec value"id="val-has_local_addr"><ahref="#val-has_local_addr"class="anchor"></a><code><spanclass="keyword">val</span> has_local_addr : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dd><p>returns true if the expression operates on address of local variable</p></dd></dl><dl><dtclass="spec value"id="val-zero"><ahref="#val-zero"class="anchor"></a><code><spanclass="keyword">val</span> zero : <ahref="index.html#type-t">t</a></code></dt><dd><p>Integer constant 0</p></dd></dl><dl><dtclass="spec value"id="val-null"><ahref="#val-null"class="anchor"></a><code><spanclass="keyword">val</span> null : <ahref="index.html#type-t">t</a></code></dt><dd><p>Null constant</p></dd></dl><dl><dtclass="spec value"id="val-one"><ahref="#val-one"class="anchor"></a><code><spanclass="keyword">val</span> one : <ahref="index.html#type-t">t</a></code></dt><dd><p>Integer constant 1</p></dd></dl><dl><dtclass="spec value"id="val-minus_one"><ahref="#val-minus_one"class="anchor"></a><code><spanclass="keyword">val</span> minus_one : <ahref="index.html#type-t">t</a></code></dt><dd><p>Integer constant -1</p></dd></dl><dl><dtclass="spec value"id="val-int"><ahref="#val-int"class="anchor"></a><code><spanclass="keyword">val</span> int : <ahref="../InferIR/IntLit/index.html#type-t">InferIR.IntLit.t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Create integer constant</p></dd></dl><dl><dtclass="spec value"id="val-float"><ahref="#val-float"class="anchor"></a><code><spanclass="keyword">val</span> float : float <span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Create float constant</p></dd></dl><dl><dtclass="spec value"id="val-bool"><ahref="#val-bool"class="anchor"></a><code><spanclass="keyword">val</span> bool : bool <span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Create integer constant corresponding to the boolean value</p></dd></dl><dl><dtclass="spec value"id="val-eq"><ahref="#val-eq"class="anchor"></a><code><spanclass="keyword">val</span> eq : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Create expression <code>e1 == e2</code></p></dd></dl><dl><dtclass="spec value"id="val-ne"><ahref="#val-ne"class="anchor"></a><code><spanclass="keyword">val</span> ne : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Create expression <code>e1 != e2</code></p></dd></dl><dl><dtclass="spec value"id="val-le"><ahref="#val-le"class="anchor"></a><code><spanclass="keyword">val</span> le : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Create expression <code>e1 <= e2</code></p></dd></dl><dl><dtclass="spec value"id="val-lt"><ahref="#val-lt"class="anchor"></a><code><spanclass="keyword">val</span> lt : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Create expression <code>e1 < e2</code></p></dd></dl><dl><dtclass="spec value"id="val-and_nary"><ahref="#val-and_nary"class="anchor"></a><code><spanclass="keyword">val</span> and_nary : <span><ahref="index.html#type-t">t</a> list</span><span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Create expression <code>e1 && e2 && e3 && ...</code></p></dd></dl><dl><dtclass="spec value"id="val-free_vars"><ahref="#val-free_vars"class="anchor"></a><code><spanclass="keyword">val</span> free_vars : <ahref="index.html#type-t">t</a><span>-></span><span><ahref="../InferIR/Ident/index.html#type-t">InferIR.Ident.t</a><ahref="../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</span></code></dt><dd><p>all the idents appearing in the expression</p></dd></dl><dl><dtclass="spec value"id="val-gen_free_vars"><ahref="#val-gen_free_vars"class="anchor"></a><code><spanclass="keyword">val</span> gen_free_vars : <ahref="index.html#type-t">t</a><span>-></span><span><span>(unit,<ahref="../InferIR/Ident/index.html#type-t">InferIR.Ident.t</a>)</span><ahref="../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.Generator.t</span></code></dt><dtclass="spec value"id="val-ident_mem"><ahref="#val-ident_mem"class="anchor"></a><code><spanclass="keyword">val</span> ident_mem : <ahref="index.html#type-t">t</a><span>-></span><ahref="../InferIR/Ident/index.html#type-t">InferIR.Ident.t</a><span>-></span> bool</code></dt><dd><p>true if the identifier appears in the expression</p></dd></dl><dl><dtclass="spec value"id="val-program_vars"><ahref="#val-program_vars"class="anchor"></a><code><spanclass="keyword">val</span> program_vars : <ahref="index.html#type-t">t</a><span>-></span><span><ahref="../InferIR/Pvar/index.html#type-t">InferIR.Pvar.t</a><ahref="../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</span></code></dt><dd><p>all the program variables appearing in the expression</p></dd></dl><dl><dtclass="spec value"id="val-rename_pvars"><ahref="#val-rename_pvars"class="anchor"></a><code><spanclass="keyword">val</span> rename_pvars : <span>f:<span>(string <span>-></span> string)</span></span><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>Rename all Pvars according to the function <code>f</code>. WARNING: You want to rename pvars before you combine expressions from different symbolic states, which you RARELY want to.</p></dd></dl><dl><dtclass="spec value"id="val-fold_captured"><ahref="#val-fold_captured"class="anchor"></a><code><spanclass="keyword">val</span> fold_captured : <span>f:<span>(<spanclass="type-var">'a</span><span>-></span><ahref="index.html#type-t">t</a><span>-></span><spanclass="type-var">'a</span>)</span></span><span>-></span><ahref="index.html#type-t">t</a><span>-></span><spanclass="type-var">'a</span><span>-></span><spanclass="type-var">'a</span></code></dt><dd><p>Fold over the expressions captured by this expression.</p></dd></dl><dl><dtclass="spec value"id="val-pp_printenv"><ahref="#val-pp_printenv"class="anchor"></a><code><spanclass="keyword">val</span> pp_printenv : <span>print_types:bool</span><span>-></span><ahref="../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a><span>-></span><ahref="index.html#module-F">F</a>.formatter <span>-></span><ahref="index.html#type-t">t</a><span>-></span> unit</code></dt><dtclass="spec value"id="val-pp"><ahref="#val-pp"class="anchor"></a><code><spanclass="keyword">val</span> pp : <ahref="index.html#module-F">F</a>.formatter <span>-></span><ahref="index.html#type-t">t</a><span>-></span> unit</code></dt><dtclass="spec value"id="val-to_string"><ahref="#val-to_string"class="anchor"></a><code><spanclass="keyword">val</span> to_string : <ahref="index.html#type-t">t</a><span>-></span> string</code></dt><dtclass="spec value"id="val-is_objc_block_closure"><ahref="#val-is_objc_block_closure"class="anchor"></a><code><spanclass="keyword">val</span> is_objc_block_closure : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dtclass="spec value"id="val-zero_of_type"><ahref="#val-zero_of_type"class="anchor"></a><code><spanclass="keyword">val</span> zero_of_type : <ahref="../InferIR/Typ/index.html#type-t">InferIR.Typ.t</a><span>-></span><span><ahref="index.html#type-t">t</a> option</span></code></dt><dd><p>Returns the zero value of a type, for int, float and ptr types</p></dd></dl><dl><dtclass="spec value"id="val-zero_of_type_exn"><ahref="#val-zero_of_type_exn"class="anchor"></a><code><spanclass="keyword">val</span> zero_of_type_exn : <ahref="../InferIR/Typ/index.html#type-t">InferIR.Typ.t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-ignore_cast"><ahref="#val-ignore_cast"class="anchor"></a><code><spanclass="keyword">val</span> ignore_cast : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-ignore_integer_cast"><ahref="#val-ignore_integer_cast"class="anchor"></a><code><spanclass="keyword">val</span> ignore_integer_cast : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt></dl></section></div></body></html>
