101 строка
5.1 KiB
TeX
101 строка
5.1 KiB
TeX
\chapter{Propagation Rules}
|
|
\label{app:propagation-rules}
|
|
|
|
These are the algebraic definitions of our propagation algorithm to go
|
|
with the descriptions in~\autoref{sec:propagation-rules}. Certain
|
|
helper functions are explained in the text, rather than
|
|
algebraically.
|
|
|
|
\begin{figure}[ht]
|
|
\begin{align*}
|
|
% Lvalue Bounds
|
|
\lbounds(e_l) &\in \mbounds(e_v, e_v) \tag*{Lvalue Bounds} \\[1ex]
|
|
\lbounds(x) &= \abounds(x, \mv{N}) \tag*{Variables} \\
|
|
& \qquad \text{when } \typeof(x) = \arr(\mv{T}, \mv{N}) \\
|
|
&= \sbounds(\addrof x) \text{ otherwise.} \\[1ex]
|
|
\lbounds(\deref e_v) &= \vbounds(e_v) \tag*{Dereference} \\[1ex]
|
|
\lbounds(e_1[e_2]) &= \vbounds(e_{base}) \tag*{Index} \\
|
|
& \qquad \text{where } e_{base} = base(e_1, e_2) \\[1ex]
|
|
\lbounds(e_l \member m) &= \abounds(e_l \member m, \mv{N}) \tag*{Struct Member Access} \\
|
|
&\qquad \text{when } \typeof(e_l \member m) = \arr(\mv{T}, \mv{N}) \\
|
|
&= \sbounds(\addrof (e_l \member m)) \text{ otherwise.} \\[1ex]
|
|
\lbounds(e_v \arrow m) &= \abounds(e_v \arrow m, \mv{N}) \tag*{Pointer Member Access} \\
|
|
&\qquad \text{when } \typeof(e_v \arrow m) = \arr(\mv{T}, \mv{N}) \\
|
|
&= \sbounds(\addrof (e_v \arrow m)) \text{ otherwise.} \\[1em]
|
|
%% Bounds Helpers/Sugar
|
|
\sbounds(e_v) &= \mbounds(e_v, e_v + 1) \tag*{Single Object Bounds} \\
|
|
\abounds(e_l, N) &= \mbounds(e_l, e_l + N) \tag*{Constant-sized Array Bounds} \\
|
|
& \qquad \text{when } N \text{ is constant.} \\
|
|
&= \mbounds(\text{unknown}) \text{ otherwise.}
|
|
\end{align*}
|
|
\caption[Lvalue Bounds Propagation]{Lvalue Bounds Propagation Rules (Mutually
|
|
Recursive with~\autoref{fig:val-bounds-prop})}
|
|
\label{fig:lval-bounds-prop}
|
|
\end{figure}
|
|
|
|
|
|
\begin{figure}[ht]
|
|
\begin{align*}
|
|
% Value Bounds
|
|
\vbounds(e_v) &\in \mbounds(e_v, e_v) \tag*{Value Bounds} \\[1ex]
|
|
\vbounds(\mathtt{NULL}) &= \mbounds(\text{any}) \tag*{Null Pointer Literal} \\[1ex]
|
|
\vbounds(l) &= \mbounds(\text{unknown}) \tag*{Other Literals} \\[1ex]
|
|
\vbounds(\addrof e_l) &= \lbounds(e_l) \tag*{Address-of} \\[1ex]
|
|
\vbounds(e_l \assign e_v) &= \vbounds(e_v) \tag*{Assignment} \\[1ex]
|
|
\vbounds(e_l \compassign e_v) &= \ltbounds(e_l) \tag*{Compound Assignment} \\[1ex]
|
|
\vbounds(e_l \inc) &= \ltbounds(e_l) \tag*{Increment \& Decrement} \\
|
|
&\qquad \text{Likewise for all Increment \& Decrement operators} \\[1ex]
|
|
\vbounds(e_v\member m) &= \srbounds(e_v, m) \tag*{Struct Member Operator} \\[1ex]
|
|
\vbounds(e_f(\overline{e_{arg}})) &= \rbounds(e_f) \left[ \textrm{params}(f) \middle/ \overline{e_{arg}}\right] \tag*{Function Call}\\[1ex]
|
|
\vbounds(e_{v1} , e_{v2}) &= \vbounds(e_{v2}) \tag*{Comma Expression} \\[1ex]
|
|
\vbounds(e_l) &= \lbounds(e_l) \tag*{Array Conversion} \\
|
|
&\qquad \text{when } \typeof(e_l) = \arr(\mv{T}, \mv{N}) \\
|
|
&= \ltbounds(e_l) \text{ otherwise}
|
|
\tag*{Lvalue Conversion} \\[1ex]
|
|
\vbounds(e_1 \binop e_2) &= \vbounds(e_{base}) \tag*{Pointer Arithmetic} \\
|
|
&\qquad \text{when } e_1 \binop e_2 \text{ has pointer type} \\
|
|
&\qquad \text{where } e_{base} = base(e_1, e_2) \\[1ex]
|
|
\vbounds(e_1 \mathrel{R} e_2) &= \mbounds(\text{unknown}) \tag*{Binary Relational Operators} \\[1ex]
|
|
\vbounds(! e_v) &= \mbounds(\text{unknown}) \tag*{Logical Negation Operator} \\[1ex]
|
|
\vbounds(e_v) &= \vbounds(e_{vi}) \tag*{Other Expressions} \\
|
|
&\qquad
|
|
\text{where } e_{vi}
|
|
\text{ is the subexpression of } e_v
|
|
\text{ with known bounds} \\
|
|
&\qquad
|
|
\text{If more than one subexpression of } e_v
|
|
\text{ has known bounds,}\\
|
|
&\qquad\quad
|
|
\text{all calculated bounds must be equal.} \\[1ex]
|
|
&= \mbounds(\text{unknown}) \text{ otherwise}\\[1em]
|
|
\rbounds(f) &\in \mbounds(e_v, e_v) \tag*{Bounds on Function Return} \\[1em]
|
|
\srbounds(e_v, m) &\in \mbounds(e_v', e_v') \tag*{Struct Relative Bounds}
|
|
\end{align*}
|
|
\caption[Value Bounds Propagation Rules]{Value Bounds Propagation Rules (Mutually
|
|
Recursive with~\autoref{fig:lval-bounds-prop}
|
|
and~\autoref{fig:lval-target-bounds-prop})}
|
|
\label{fig:val-bounds-prop}
|
|
\end{figure}
|
|
|
|
\begin{figure}[ht]
|
|
\begin{align*}
|
|
%% Lvalue Target Bounds
|
|
\ltbounds(e_l) &\in \mbounds(e_v, e_v) \tag*{Lvalue Target Bounds} \\[1ex]
|
|
\ltbounds(e_l) &= \sbounds(e_l) \tag*{Checked Singleton Pointer Bounds}\\
|
|
&\qquad \text{where } \typeof(e_l) = \PtrT \\[1ex]
|
|
\ltbounds(x) &= \dbounds(x) \tag*{Variable Target Bounds}\\[1ex]
|
|
\ltbounds(e_l \member m) &= \srbounds(e_l, m) \tag*{Struct Member Target Bounds}\\
|
|
\ltbounds(e_v \arrow m) &= \srbounds(e_v, m) \tag*{Pointer Member Target Bounds}\\[1ex]
|
|
\ltbounds(\_) &= \mbounds(\text{unknown}) \\[1em]
|
|
\dbounds(x) &\in \mbounds(e_v, e_v) \tag*{Declared Bounds}
|
|
\end{align*}
|
|
\caption[Lvalue Target Bounds Propagation Rules]{Lvalue Target Bounds
|
|
Propagation Rules}
|
|
\label{fig:lval-target-bounds-prop}
|
|
\end{figure}
|
|
|
|
%%% Local Variables:
|
|
%%% mode: latex
|
|
%%% TeX-master: "tr02"
|
|
%%% End:
|