Changeset 42d81a7 for doc/theses

Timestamp:

Oct 23, 2024, 3:04:47 PM (8 weeks ago)

Author:

Michael Brooks <mlbrooks@…>

Branches:

master

Children:

12c4a5f

Parents:

d3942b9

Message:

Thesis, array, C typing rules, add old C rules and case-comparison table.

Location:

doc/theses/mike_brooks_MMath

Files:

• array.tex (modified) (1 diff)
• uw-ethesis.tex (modified) (1 diff)

doc/theses/mike_brooks_MMath/array.tex

@@ -502 +502 @@
 \end{itemize}
 
-TODO: summarize the C rules and add the case-comparison table
+The traditional C rules are:
+\begin{itemize}
+\item
+        Reject a Statically Evaluable pair, if the expressions have two different values.
+\item
+        Otherwise, accept.
+\end{itemize}
+
+
+\newcommand{\falsealarm}{{\color{orange}\small{*}}}
+\newcommand{\allowmisuse}{{\color{red}\textbf{!}}}
+\newcommand{\cmark}{\ding{51}} % from pifont
+\newcommand{\xmark}{\ding{55}}
+\begin{figure}
+        \begin{tabular}{@{}l@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c}
+         & \multicolumn{2}{c}{\underline{Values Equal}}
+         & \multicolumn{2}{c}{\underline{Values Unequal}} 
+         & \\
+        \textbf{Case}                                & C      & \CFA                & C                      & \CFA    & Compat. \\
+        Both Statically Evaluable, Same Symbol       & Accept & Accept              &                        &         & \cmark \\
+        Both Statically Evaluable, Different Symbols & Accept & Accept              & Reject                 & Reject  & \cmark \\
+        Both Dynamic but Stable, Same Symbol         & Accept & Accept              &                        &         & \cmark \\
+        Both Dynamic but Stable, Different Symbols   & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark \\
+        Both Potentially Unstable, Same Symbol       & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark \\
+        Any other grouping, Different Symbol         & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark
+        \end{tabular}
+
+        \vspace{12pt}
+        \noindent\textbf{Legend:}
+        \begin{itemize}
+        \item
+                Each row gives the treatment of a test harness of the form
+                \begin{cfa}
+                        float x[ expr1 ];
+                        float (*xp)[ expr2 ] = &x;
+                \end{cfa}
+                where \lstinline{expr1} and \lstinline{expr2} are metavariables varying according to the row's Case.
+                Each row's claim applies to other harnesses too, including,
+                \begin{itemize}
+                \item
+                        calling a function with a paramter like \lstinline{x} and an argument of the \lstinline{xp} type,
+                \item
+                        assignment in place of initialization,
+                \item
+                        using references in place of pointers, and
+                \item
+                        for the \CFA array, calling a polymorphic function on two \lstinline{T}-typed parameters with \lstinline{&x}- and \lstinline{xp}-typed arguments.
+                \end{itemize}
+        \item
+                Each case's claim is symmetric (swapping \lstinline{expr1} with \lstinline{expr2} has no effect),
+                even though most test harnesses are asymetric.
+        \item
+                The table treats symbolic identity (Same/Different on rows)
+                apart from value eqality (Equal/Unequal on columns).
+                \begin{itemize}
+                \item
+                        The expressions \lstinline{1}, \lstinline{0+1} and \lstinline{n}
+                        (where \lstinline{n} is a variable with value 1),
+                        are all different symbols with the value 1.
+                \item
+                        The column distinction expresses ground truth about whether an omniscient analysis should accept or reject.
+                \item
+                        The row distinction expresses the simple static factors used by today's analyses.
+                \end{itemize}
+        \item
+                Accordingly, every Reject under Values Equal is a false alarm (\falsealarm),
+                while every Accept under Values Unequal is an allowed misuse (\allowmisuse).
+        \end{itemize}
+        \caption{Case comparison for array type compatibility, given pairs of dimension expressions.
+                TODO: get Peter's LaTeX help on overall appearance, probably including column spacing/centering and bullet indentation.}
+        \label{f:DimexprRuleCompare}
+\end{figure}
+
+
+Figure~\ref{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
+It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafely.
+It also shows that C-incompatibilities only occur in cases that C treats unsafely.
+
 
 The conservatism of the new rule set can leave a programmer needing a recourse,

doc/theses/mike_brooks_MMath/uw-ethesis.tex

@@ -87 +87 @@
 \usepackage{graphicx}
 \usepackage{tabularx}
+\usepackage{pifont}
 \usepackage[labelformat=simple,aboveskip=0pt,farskip=0pt,font=normalsize]{subfig}
 \renewcommand\thesubfigure{(\alph{subfigure})}