Ignore:
Timestamp:
Oct 23, 2024, 3:04:47 PM (4 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:
2 edited

Legend:

Unmodified
Added
Removed
  • doc/theses/mike_brooks_MMath/array.tex

    rd3942b9 r42d81a7  
    502502\end{itemize}
    503503
    504 TODO: summarize the C rules and add the case-comparison table
     504The traditional C rules are:
     505\begin{itemize}
     506\item
     507        Reject a Statically Evaluable pair, if the expressions have two different values.
     508\item
     509        Otherwise, accept.
     510\end{itemize}
     511
     512
     513\newcommand{\falsealarm}{{\color{orange}\small{*}}}
     514\newcommand{\allowmisuse}{{\color{red}\textbf{!}}}
     515\newcommand{\cmark}{\ding{51}} % from pifont
     516\newcommand{\xmark}{\ding{55}}
     517\begin{figure}
     518        \begin{tabular}{@{}l@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c}
     519         & \multicolumn{2}{c}{\underline{Values Equal}}
     520         & \multicolumn{2}{c}{\underline{Values Unequal}}
     521         & \\
     522        \textbf{Case}                                & C      & \CFA                & C                      & \CFA    & Compat. \\
     523        Both Statically Evaluable, Same Symbol       & Accept & Accept              &                        &         & \cmark \\
     524        Both Statically Evaluable, Different Symbols & Accept & Accept              & Reject                 & Reject  & \cmark \\
     525        Both Dynamic but Stable, Same Symbol         & Accept & Accept              &                        &         & \cmark \\
     526        Both Dynamic but Stable, Different Symbols   & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark \\
     527        Both Potentially Unstable, Same Symbol       & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark \\
     528        Any other grouping, Different Symbol         & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark
     529        \end{tabular}
     530
     531        \vspace{12pt}
     532        \noindent\textbf{Legend:}
     533        \begin{itemize}
     534        \item
     535                Each row gives the treatment of a test harness of the form
     536                \begin{cfa}
     537                        float x[ expr1 ];
     538                        float (*xp)[ expr2 ] = &x;
     539                \end{cfa}
     540                where \lstinline{expr1} and \lstinline{expr2} are metavariables varying according to the row's Case.
     541                Each row's claim applies to other harnesses too, including,
     542                \begin{itemize}
     543                \item
     544                        calling a function with a paramter like \lstinline{x} and an argument of the \lstinline{xp} type,
     545                \item
     546                        assignment in place of initialization,
     547                \item
     548                        using references in place of pointers, and
     549                \item
     550                        for the \CFA array, calling a polymorphic function on two \lstinline{T}-typed parameters with \lstinline{&x}- and \lstinline{xp}-typed arguments.
     551                \end{itemize}
     552        \item
     553                Each case's claim is symmetric (swapping \lstinline{expr1} with \lstinline{expr2} has no effect),
     554                even though most test harnesses are asymetric.
     555        \item
     556                The table treats symbolic identity (Same/Different on rows)
     557                apart from value eqality (Equal/Unequal on columns).
     558                \begin{itemize}
     559                \item
     560                        The expressions \lstinline{1}, \lstinline{0+1} and \lstinline{n}
     561                        (where \lstinline{n} is a variable with value 1),
     562                        are all different symbols with the value 1.
     563                \item
     564                        The column distinction expresses ground truth about whether an omniscient analysis should accept or reject.
     565                \item
     566                        The row distinction expresses the simple static factors used by today's analyses.
     567                \end{itemize}
     568        \item
     569                Accordingly, every Reject under Values Equal is a false alarm (\falsealarm),
     570                while every Accept under Values Unequal is an allowed misuse (\allowmisuse).
     571        \end{itemize}
     572        \caption{Case comparison for array type compatibility, given pairs of dimension expressions.
     573                TODO: get Peter's LaTeX help on overall appearance, probably including column spacing/centering and bullet indentation.}
     574        \label{f:DimexprRuleCompare}
     575\end{figure}
     576
     577
     578Figure~\ref{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
     579It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafely.
     580It also shows that C-incompatibilities only occur in cases that C treats unsafely.
     581
    505582
    506583The conservatism of the new rule set can leave a programmer needing a recourse,
  • doc/theses/mike_brooks_MMath/uw-ethesis.tex

    rd3942b9 r42d81a7  
    8787\usepackage{graphicx}
    8888\usepackage{tabularx}
     89\usepackage{pifont}
    8990\usepackage[labelformat=simple,aboveskip=0pt,farskip=0pt,font=normalsize]{subfig}
    9091\renewcommand\thesubfigure{(\alph{subfigure})}
Note: See TracChangeset for help on using the changeset viewer.