Ignore:
Timestamp:
Jan 8, 2026, 1:26:42 PM (4 weeks ago)
Author:
Michael Brooks <mlbrooks@…>
Branches:
master
Children:
fb7c9168
Parents:
79ba50c (diff), 4904b05 (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.
Message:

Merge branch 'master' of plg.uwaterloo.ca:software/cfa/cfa-cc

File:
1 edited

Legend:

Unmodified
Added
Removed

  • doc/theses/mike_brooks_MMath/array.tex

    r79ba50c r8614140  
    22\label{c:Array}
    33
    4 Arrays in C are possibly the single most misunderstood and incorrectly used feature in the language, resulting in the largest proportion of runtime errors and security violations.
     4Arrays in C are possibly the single most misunderstood and incorrectly used feature in the language \see{\VRef{s:Array}}, resulting in the largest proportion of runtime errors and security violations.
    55This chapter describes the new \CFA language and library features that introduce a length-checked array type, @array@, to the \CFA standard library~\cite{Cforall}.
    66
    … …  
    1313\label{s:ArrayIntro}
    1414
    15 The new \CFA array is declared by instantiating the generic @array@ type,
    16 much like instantiating any other standard-library generic type (such as \CC @vector@),
    17 though using a new style of generic parameter.
     15The new \CFA array is declared by instantiating the generic @array@ type, much like instantiating any other standard-library generic type (such as \CC @vector@), using a new style of generic parameter.
    1816\begin{cfa}
    1917@array( float, 99 )@ x;                                 $\C[2.5in]{// x contains 99 floats}$
    … …  
    2422void f( @array( float, 42 )@ & p ) {}   $\C{// p accepts 42 floats}$
    2523f( x );                                                                 $\C{// statically rejected: type lengths are different, 99 != 42}$
     24
    2625test2.cfa:3:1 error: Invalid application of existing declaration(s) in expression.
    2726Applying untyped:  Name: f ... to:  Name: x
    … …  
    3736g( x, 0 );                                                              $\C{// T is float, N is 99, dynamic subscript check succeeds}$
    3837g( x, 1000 );                                                   $\C{// T is float, N is 99, dynamic subscript check fails}$
     38
    3939Cforall Runtime error: subscript 1000 exceeds dimension range [0,99) $for$ array 0x555555558020.
    4040\end{cfa}
    … …  
    9292is a sufficient postcondition.
    9393In an imperative language like C and \CFA, it is also necessary to discuss side effects, for which an even heavier formalism, like separation logic, is required.
    94 Secondly, TODO: bash Rust.
    95 % TODO: cite the crap out of these claims.
     94Secondly: ... bash Rust.
     95... cite the crap out of these claims.
    9696\end{comment}
    9797
    … …  
    110110forall( T & | sized(T) )
    111111T * alloc() {
    112         return @(T *)@malloc( @sizeof(T)@ );
     112        return @(T *)@malloc( @sizeof(T)@ );    // C malloc
    113113}
    114114\end{cfa}
    … …  
    132132The loops follow the familiar pattern of using the variable @dim@ to iterate through the arrays.
    133133Most importantly, the type system implicitly captures @dim@ at the call of @f@ and makes it available throughout @f@ as @N@.
    134 The example shows @dim@ adapting into a type-system managed length at the declarations of @x@, @y@, and @result@, @N@ adapting in the same way at @f@'s loop bound, and a pass-thru use of @dim@ at @f@'s declaration of @ret@.
     134The example shows @dim@ adapting into a type-system managed length at the declarations of @x@, @y@, and @result@; @N@ adapting in the same way at @f@'s loop bound; and a pass-thru use of @dim@ at @f@'s declaration of @ret@.
    135135Except for the lifetime-management issue of @result@, \ie explicit @free@, this program has eliminated both the syntactic and semantic problems associated with C arrays and their usage.
    136136The result is a significant improvement in safety and usability.
    … …  
    148148\end{itemize}
    149149
    150 \VRef[Figure]{f:TemplateVsGenericType} shows @N@ is not the same as a @size_t@ declaration in a \CC \lstinline[language=C++]{template}.
     150\VRef[Figure]{f:TemplateVsGenericType} shows @N@ is not the same as a @size_t@ declaration in a \CC \lstinline[language=C++]{template}.\footnote{
     151The \CFA program requires a snapshot declaration for \lstinline{n} to compile, as described at the end of \Vref{s:ArrayTypingC}.}
    151152\begin{enumerate}[leftmargin=*]
    152153\item
    153154The \CC template @N@ can only be a compile-time value, while the \CFA @N@ may be a runtime value.
    154155\item
    155 \CC does not allow a template function to be nested, while \CFA lets its polymorphic functions to be nested.
     156\CC does not allow a template function to be nested, while \CFA allows polymorphic functions be nested.
    156157Hence, \CC precludes a simple form of information hiding.
    157158\item
    … …  
    176177% mycode/arrr/thesis-examples/check-peter/cs-cpp.cpp, v10
    177178\end{enumerate}
    178 The \CC template @array@ type mitigates points \VRef[]{p:DimensionPassing} and \VRef[]{p:ArrayCopy}, but it is also trying to accomplish a similar mechanism to \CFA @array@.
     179The \CC template @std::array@ tries to accomplish a similar mechanism to \CFA @array@.
     180It is an aggregate type with the same semantics as a @struct@ holding a C-style array \see{\VRef{s:ArraysCouldbeValues}}, which mitigates points \VRef[]{p:DimensionPassing} and \VRef[]{p:ArrayCopy}.
    179181
    180182\begin{figure}
    181 \begin{tabular}{@{}l@{\hspace{20pt}}l@{}}
     183\begin{tabular}{@{}ll@{}}
    182184\begin{c++}
    183185
    … …  
    187189}
    188190int main() {
    189 
    190         int ret[10], x[10];
    191         for ( int i = 0; i < 10; i += 1 ) x[i] = i;
    192         @copy<int, 10 >( ret, x );@
    193         for ( int i = 0; i < 10; i += 1 )
     191        const size_t  n = 10;   // must be constant
     192        int ret[n], x[n];
     193        for ( int i = 0; i < n; i += 1 ) x[i] = i;
     194        @copy<int, n >( ret, x );@
     195        for ( int i = 0; i < n; i += 1 )
    194196                cout << ret[i] << ' ';
    195197        cout << endl;
    … …  
    203205                for ( i; N ) ret[i] = x[i];
    204206        }
    205 
    206         const int n = promptForLength();
     207        size_t  n;
     208        sin | n;
    207209        array( int, n ) ret, x;
    208210        for ( i; n ) x[i] = i;
    … …  
    228230When the argument lengths themselves are statically unknown,
    229231the static check is conservative and, as always, \CFA's casting lets the programmer use knowledge not shared with the type system.
    230 \begin{tabular}{@{\hspace{0.5in}}l@{\hspace{1in}}l@{}}
    231 \lstinput{90-97}{hello-array.cfa}
    232 &
    233 \lstinput{110-117}{hello-array.cfa}
    234 \end{tabular}
    235 
    236 \noindent
    237 This static check's full rules are presented in \VRef[Section]{s:ArrayTypingC}.
     232\lstinput{90-96}{hello-array.cfa}
     233This static check's rules are presented in \VRef[Section]{s:ArrayTypingC}.
    238234
    239235Orthogonally, the \CFA array type works within generic \emph{types}, \ie @forall@-on-@struct@.
    240236The same argument safety and the associated implicit communication of array length occurs.
    241237Preexisting \CFA allowed aggregate types to be generalized with type parameters, enabling parameterizing of element types.
    242 This has been extended to allow parameterizing by dimension.
    243 Doing so gives a refinement of C's ``flexible array member''~\cite[\S~6.7.2.1.18]{C11}.
     238This feature is extended to allow parameterizing by dimension.
     239Doing so gives a refinement of C's ``flexible array member''~\cite[\S~6.7.2.1.18]{C11}:
    244240\begin{cfa}
    245241struct S {
    … …  
    264260\end{cfa}
    265261This ability to avoid casting and size arithmetic improves safety and usability over C flexible array members.
    266 Finally, inputs and outputs are given at the bottom for different sized schools.
     262Finally, inputs and outputs are given on the right for different sized schools.
    267263The example program prints the courses in each student's preferred order, all using the looked-up display names.
    268264
    269265\begin{figure}
    270 \begin{cquote}
    271 \lstinput{50-55}{hello-accordion.cfa}
     266\begin{lrbox}{\myboxA}
     267\begin{tabular}{@{}l@{}}
     268\lstinput{50-55}{hello-accordion.cfa} \\
    272269\lstinput{90-98}{hello-accordion.cfa}
    273 \ \\
    274 @$ cat school1@
    275 \lstinput{}{school1}
    276 
    277 @$ ./a.out < school1@
    278 \lstinput{}{school1.out}
    279 
    280 @$ cat school2@
    281 \lstinput{}{school2}
    282 
    283 @$ ./a.out < school2@
    284 \lstinput{}{school2.out}
    285 \end{cquote}
     270\end{tabular}
     271\end{lrbox}
     272
     273\begin{lrbox}{\myboxB}
     274\begin{tabular}{@{}l@{}}
     275@$ cat school1@ \\
     276\lstinputlisting{school1} \\
     277@$ ./a.out < school1@ \\
     278\lstinputlisting{school1.out} \\
     279@$ cat school2@ \\
     280\lstinputlisting{school2} \\
     281@$ ./a.out < school2@ \\
     282\lstinputlisting{school2.out}
     283\end{tabular}
     284\end{lrbox}
     285
     286\setlength{\tabcolsep}{10pt}
     287\begin{tabular}{@{}ll@{}}
     288\usebox\myboxA
     289&
     290\usebox\myboxB
     291\end{tabular}
    286292
    287293\caption{\lstinline{School} Example, Input and Output}
    … …  
    290296
    291297When a function operates on a @School@ structure, the type system handles its memory layout transparently.
    292 \lstinput{30-37}{hello-accordion.cfa}
     298\lstinput{30-36}{hello-accordion.cfa}
    293299In the example, function @getPref@ returns, for the student at position @is@, what is the position of their @pref@\textsuperscript{th}-favoured class?
    294300
    … …  
    296302\section{Dimension Parameter Implementation}
    297303
    298 The core of the preexisting \CFA compiler already had the ``heavy equipment'' needed to provide the feature set just reviewed (up to bugs in cases not yet exercised).
     304The core of the preexisting \CFA compiler already has the ``heavy equipment'' needed to provide the feature set just reviewed (up to bugs in cases not yet exercised).
    299305To apply this equipment in tracking array lengths, I encoded a dimension (array's length) as a type.
    300306The type in question does not describe any data that the program actually uses at runtime.
    … …  
    323329\begin{itemize}[leftmargin=*]
    324330\item
    325         Resolver provided values for a used declaration's type-system variables, gathered from type information in scope at the usage site.
    326 \item
    327         The box pass, encoding information about type parameters into ``extra'' regular parameters/arguments on declarations and calls.
     331        Resolver provided values for a declaration's type-system variables, gathered from type information in scope at the usage site.
     332\item
     333        The box pass, encoding information about type parameters into ``extra'' regular parameters and arguments on declarations and calls.
    328334        Notably, it conveys the size of a type @foo@ as a @__sizeof_foo@ parameter, and rewrites the @sizeof(foo)@ expression as @__sizeof_foo@, \ie a use of the parameter.
    329335\end{itemize}
    … …  
    331337The rules for resolution had to be restricted slightly, in order to achieve important refusal cases.
    332338This work is detailed in \VRef[Section]{s:ArrayTypingC}.
    333 However, the resolution--boxing scheme, in its preexisting state, was already equipped to work on (desugared) dimension parameters.
     339However, the resolution--boxing scheme, in its preexisting state, is equipped to work on (desugared) dimension parameters.
    334340The following discussion explains the desugaring and how correctly lowered code results.
    335341
    … …  
    357363\end{enumerate}
    358364The chosen solution is to encode the value @N@ \emph{as a type}, so items 1 and 2 are immediately available for free.
    359 Item 3 needs a way to recover the encoded value from a (valid) type (and to reject invalid types occurring here).
     365Item 3 needs a way to recover the encoded value from a (valid) type and to reject invalid types.
    360366Item 4 needs a way to produce a type that encodes the given value.
    361367
    … …  
    416422        The type @thing(N)@ is (replaced by @void *@, but thereby effectively) gone.
    417423\item
    418         The @sout...@ expression (being an application of the @?|?@ operator) has a regular variable (parameter) usage for its second argument.
     424        The @sout...@ expression has a regular variable (parameter) usage for its second argument.
    419425\item
    420426        Information about the particular @thing@ instantiation (value 10) is moved, from the type, to a regular function-call argument.
    … …  
    455461\begin{cfa}
    456462enum { n = 42 };
    457 float x[@n@];   // or just 42
    458 float (*xp1)[@42@] = &x;    // accept
    459 float (*xp2)[@999@] = &x;   // reject
     463float x[@n@];   $\C{// or just 42}$
     464float (*xp1)[@42@] = &x;    $\C{// accept}$
     465float (*xp2)[@999@] = &x;   $\C{// reject}$
    460466warning: initialization of 'float (*)[999]' from incompatible pointer type 'float (*)[42]'
    461467\end{cfa}
    462468When a variable is involved, C and \CFA take two different approaches.
    463 Today's C compilers accept the following without warning.
     469Today's C compilers accept the following without a warning.
    464470\begin{cfa}
    465471static const int n = 42;
    … …  
    482488The way the \CFA array is implemented, the type analysis for this case reduces to a case similar to the earlier C version.
    483489The \CFA compiler's compatibility analysis proceeds as:
    484 \begin{itemize}[parsep=0pt]
     490\begin{itemize}[leftmargin=*,parsep=0pt]
    485491\item
    486492        Is @array( float, 999 )@ type-compatible with @array( float, n )@?
    … …  
    510516        in order to preserve the length information that powers runtime bound-checking.}
    511517Therefore, the need to upgrade legacy C code is low.
    512 Finally, if this incompatibility is a problem onboarding C programs to \CFA, it is should be possible to change the C type check to a warning rather than an error, acting as a \emph{lint} of the original code for a missing type annotation.
     518Finally, if this incompatibility is a problem onboarding C programs to \CFA, it should be possible to change the C type check to a warning rather than an error, acting as a \emph{lint} of the original code for a missing type annotation.
    513519
    514520To handle two occurrences of the same variable, more information is needed, \eg, this is fine,
    … …  
    516522int n = 42;
    517523float x[@n@];
    518 float (*xp)[@n@] = x;   // accept
     524float (*xp)[@n@] = x;   $\C{// accept}$
    519525\end{cfa}
    520526where @n@ remains fixed across a contiguous declaration context.
    521 However, intervening dynamic statement cause failures.
     527However, intervening dynamic statements can cause failures.
    522528\begin{cfa}
    523529int n = 42;
    524530float x[@n@];
    525 @n@ = 999; // dynamic change
    526 float (*xp)[@n@] = x;   // reject
    527 \end{cfa}
    528 However, side-effects can occur in a contiguous declaration context.
     531@n@ = 999; $\C{// dynamic change}$
     532float (*xp)[@n@] = x;   $\C{// reject}$
     533\end{cfa}
     534As well, side-effects can even occur in a contiguous declaration context.
    529535\begin{cquote}
    530536\setlength{\tabcolsep}{20pt}
    … …  
    536542void f() {
    537543        float x[@n@] = { g() };
    538         float (*xp)[@n@] = x;   // reject
     544        float (*xp)[@n@] = x;                   // reject
    539545}
    540546\end{cfa}
    … …  
    544550int @n@ = 42;
    545551void g() {
    546         @n@ = 99;
     552        @n@ = 999;              // accept
    547553}
    548554
    … …  
    553559The issue here is that knowledge needed to make a correct decision is hidden by separate compilation.
    554560Even within a translation unit, static analysis might not be able to provide all the information.
    555 However, if the example uses @const@, the check is possible.
     561However, if the example uses @const@, the check is possible even though the value is unknown.
    556562\begin{cquote}
    557563\setlength{\tabcolsep}{20pt}
    … …  
    563569void f() {
    564570        float x[n] = { g() };
    565         float (*xp)[n] = x;   // reject
     571        float (*xp)[n] = x;             // accept
    566572}
    567573\end{cfa}
    … …  
    571577@const@ int n = 42;
    572578void g() {
    573         @n = 99@; // allowed
     579        @n = 999@;              // reject
    574580}
    575581
    … …  
    692698An expression-compatibility question is a new addition to the \CFA compiler, and occurs in the context of dimension expressions, and possibly enumerations assigns, which must be unique.
    693699
    694 % TODO: ensure these compiler implementation matters are treated under \CFA compiler background: type unification, cost calculation, GenPoly.
     700% ... ensure these compiler implementation matters are treated under \CFA compiler background: type unification, cost calculation, GenPoly.
    695701
    696702The relevant technical component of the \CFA compiler is the standard type-unification within the type resolver.
    … …  
    726732\end{cfa}
    727733when resolving a function call to @g@, the first unification stage compares the type @T@ of the parameter with @array( float, n + 1 )@, of the argument.
    728 \PAB{TODO: finish.}
    729734
    730735The actual rules for comparing two dimension expressions are conservative.
    … …  
    732737is to imply, ``all else being equal, allow an array with length calculated by $e_1$
    733738to be passed to a function expecting a length-$e_2$ array.''\footnote{
    734         TODO: Deal with directionality, that I'm doing exact-match, no ``at least as long as,'' no subtyping.
     739        ... Deal with directionality, that I'm doing exact-match, no ``at least as long as,'' no subtyping.
    735740        Should it be an earlier scoping principle?  Feels like it should matter in more places than here.}
    736741So, a ``yes'' answer must represent a guarantee that both expressions evaluate the
    … …  
    746751So, a variable and a literal can never match.
    747752
    748 TODO: Discuss the interaction of this dimension hoisting with the challenge of extra unification for cost calculation
     753... Discuss the interaction of this dimension hoisting with the challenge of extra unification for cost calculation
    749754\end{comment}
    750755
    751 The conservatism of the new rule set can leave a programmer needing a recourse, when needing to use a dimension expression whose stability argument is more subtle than current-state analysis.
     756The conservatism of the new rule set can leave a programmer requiring a recourse, when needing to use a dimension expression whose stability argument is more subtle than current-state analysis.
    752757This recourse is to declare an explicit constant for the dimension value.
    753758Consider these two dimension expressions, whose uses are rejected by the blunt current-state rules:
    … …  
    755760void f( int @&@ nr, @const@ int nv ) {
    756761        float x[@nr@];
    757         float (*xp)[@nr@] = &x;   // reject: nr varying (no references)
     762        float (*xp)[@nr@] = &x;                 // reject: nr varying (no references)
    758763        float y[@nv + 1@];
    759         float (*yp)[@nv + 1@] = &y;   // reject: ?+? unpredictable (no functions)
     764        float (*yp)[@nv + 1@] = &y;             // reject: ?+? unpredictable (no functions)
    760765}
    761766\end{cfa}
    762767Yet, both dimension expressions are reused safely.
    763 The @nr@ reference is never written, not volatile meaning no implicit code (load) between declarations, and control does not leave the function between the uses.
     768The @nr@ reference is never written, no implicit code (load) between declarations, and control does not leave the function between the uses.
    764769As well, the build-in @?+?@ function is predictable.
    765770To make these cases work, the programmer must add the follow constant declarations (cast does not work):
    … …  
    768773        @const int nx@ = nr;
    769774        float x[nx];
    770         float (*xp)[nx] = & x;   // accept
     775        float (*xp)[nx] = & x;                  // accept
    771776        @const int ny@ = nv + 1;
    772777        float y[ny];
    773         float (*yp)[ny] = & y;   // accept
     778        float (*yp)[ny] = & y;                  // accept
    774779}
    775780\end{cfa}
    … …  
    808813\end{cfa}
    809814Dimension hoisting already existed in the \CFA compiler.
    810 But its was buggy, particularly with determining, ``Can hoisting the expression be skipped here?'', for skipping this hoisting is clearly desirable in some cases.
     815However, it was buggy, particularly with determining, ``Can hoisting the expression be skipped here?'', for skipping this hoisting is clearly desirable in some cases.
    811816For example, when a programmer has already hoisted to perform an optimization to prelude duplicate code (expression) and/or expression evaluation.
    812817In the new implementation, these cases are correct, harmonized with the accept/reject criteria.
    … …  
    820825\item
    821826Flexible-stride memory:
    822 this model has complete independence between subscripting ordering and memory layout, offering the ability to slice by (provide an index for) any dimension, \eg slice a plane, row, or column, \eg @c[3][*][*]@, @c[3][4][*]@, @c[3][*][5]@.
     827this model has complete independence between subscript ordering and memory layout, offering the ability to slice by (provide an index for) any dimension, \eg slice a row, column, or plane, \eg @c[3][4][*]@, @c[3][*][5]@, @c[3][*][*]@.
    823828\item
    824829Fixed-stride memory:
    … …  
    839844Style 3 is the inevitable target of any array implementation.
    840845The hardware offers this model to the C compiler, with bytes as the unit of displacement.
    841 C offers this model to its programmer as pointer arithmetic, with arbitrary sizes as the unit.
     846C offers this model to programmers as pointer arithmetic, with arbitrary sizes as the unit.
    842847Casting a multidimensional array as a single-dimensional array/pointer, then using @x[i]@ syntax to access its elements, is still a form of pointer arithmetic.
    843848
    844 Now stepping into the implementation of \CFA's new type-1 multidimensional arrays in terms of C's existing type-2 multidimensional arrays, it helps to clarify that even the interface is quite low-level.
    845 A C/\CFA array interface includes the resulting memory layout.
    846 The defining requirement of a type-2 system is the ability to slice a column from a column-finest matrix.
    847 The required memory shape of such a slice is fixed, before any discussion of implementation.
    848 The implementation presented here is how the \CFA array-library wrangles the C type system, to make it do memory steps that are consistent with this layout while not affecting legacy C programs.
     849To step into the implementation of \CFA's new type-1 multidimensional arrays in terms of C's existing type-2 multidimensional arrays, it helps to clarify that the interface is low-level, \ie a C/\CFA array interface includes the resulting memory layout.
     850Specifically, the defining requirement of a type-2 system is the ability to slice a column from a column-finest matrix.
     851Hence, the required memory shape of such a slice is fixed, before any discussion of implementation.
     852The implementation presented here is how the \CFA array-library wrangles the C type system to make it do memory steps that are consistent with this layout while not affecting legacy C programs.
    849853% TODO: do I have/need a presentation of just this layout, just the semantics of -[all]?
    850854
    … …  
    874878\lstinput[aboveskip=0pt]{145-145}{hello-md.cfa}
    875879The nontrivial slicing in this example now allows passing a \emph{noncontiguous} slice to @print1d@, where the new-array library provides a ``subscript by all'' operation for this purpose.
    876 In a multi-dimensional subscript operation, any dimension given as @all@ is a placeholder, \ie ``not yet subscripted by a value'', waiting for such a value, implementing the @ar@ trait.
     880In a multi-dimensional subscript operation, any dimension given as @all@ is a placeholder, \ie ``not yet subscripted by a value'', waiting for a value implementing the @ar@ trait.
    877881\lstinput{150-151}{hello-md.cfa}
    878882
    … …  
    948952A column is almost ready to be arranged into a matrix;
    949953it is the \emph{contained value} of the next-level building block, but another lie about size is required.
    950 At first, an atom needs to be arranged as if it were bigger, but now a column needs to be arranged as if it is smaller (the left diagonal above it, shrinking upward).
     954At first, an atom needs to be arranged as if it is bigger, but now a column needs to be arranged as if it is smaller (the left diagonal above it, shrinking upward).
    951955These lying columns, arranged contiguously according to their size (as announced) form the matrix @x[all]@.
    952956Because @x[all]@ takes indices, first for the fine stride, then for the coarse stride, it achieves the requirement of representing the transpose of @x@.
    … …  
    10201024
    10211025
    1022 \section{Bound Checks, Added and Removed}
    1023 
     1026\section{Zero Overhead}
     1027
     1028At runtime, the \CFA array is exactly a C array.
    10241029\CFA array subscripting is protected with runtime bound checks.
    1025 The array dependent-typing provides information to the C optimizer allowing it remove many of the bound checks.
    1026 This section provides a demonstration of the effect.
    1027 
    1028 The experiment compares the \CFA array system with the padded-room system [TODO:xref] most typically exemplified by Java arrays, but also reflected in the \CC pattern where restricted vector usage models a checked array.
    1029 The essential feature of this padded-room system is the one-to-one correspondence between array instances and the symbolic bounds on which dynamic checks are based.
    1030 The experiment compares with the \CC version to keep access to generated assembly code simple.
     1030The array dependent-typing provides information to the C optimizer, allowing it remove many of the bound checks.
     1031This section provides a demonstration of these effects.
     1032
     1033The experiment compares the \CFA array system with the simple-safety system most typically exemplified by Java arrays (\VRef[Section]{JavaCompare}), but also reflected in the \CC pattern where restricted vector usage models a checked array (\VRef[Section]{CppCompare}).
     1034The essential feature of this simple system is the one-to-one correspondence between array instances and the symbolic bounds on which dynamic checks are based.
     1035The experiment uses the \CC version to simplify access to generated assembly code.
     1036While ``\CC'' labels a participant, it is really the simple-safety system (of @vector@ with @.at@) whose limitations are being explained, and not limitations of \CC optimization.
    10311037
    10321038As a control case, a simple loop (with no reused dimension sizes) is seen to get the same optimization treatment in both the \CFA and \CC versions.
    1033 When the programmer treats the array's bound correctly (making the subscript ``obviously fine''), no dynamic bound check is observed in the program's optimized assembly code.
    1034 But when the bounds are adjusted, such that the subscript is possibly invalid, the bound check appears in the optimized assembly, ready to catch an occurrence the mistake.
    1035 
    1036 TODO: paste source and assembly codes
    1037 
    1038 Incorporating reuse among dimension sizes is seen to give \CFA an advantage at being optimized.
    1039 The case is naive matrix multiplication over a row-major encoding.
    1040 
    1041 TODO: paste source codes
     1039Firstly, when the programmer treats the array's bound correctly (making the subscript ``obviously fine''), no dynamic bound check is observed in the program's optimized assembly code.
     1040But when the bounds are adjusted, such that the subscript is possibly invalid, the bound check appears in the optimized assembly, ready to catch a mistake.
     1041
     1042\VRef[Figure]{f:ovhd-ctl} gives a control-case example of summing values in an array, where each column shows the program in languages C (a,~d,~g), \CFA (b,~e,~h), and \CC (c,~f,~i).
     1043The C code has no bounds checking, while the \CFA and \CC can have bounds checking.
     1044The source-code functions in (a, b, c) can be compiled to have either correct or incorrect uses of bounds.
     1045When compiling for correct bound use, the @BND@ macro passes its argument through, so the loops cover exactly the passed array sizes.
     1046When compiling for possible incorrect bound use (a programming error), the @BND@ macro hardcodes the loops for 100 iterations, which implies out-of-bound access attempts when the passed array has fewer than 100 elements.
     1047The assembly code excerpts show optimized translations for correct-bound mode in (d, e, f) and incorrect-bound mode in (g, h, i).
     1048Because incorrect-bound mode hardcodes 100 iterations, the loop always executes a first time, so this mode does not have the @n == 0@ branch seen in correct-bound mode.
     1049For C, this difference is the only (d--g) difference.
     1050For correct bounds, the \CFA translation equals the C translation, \ie~there is no (d--e) difference, while \CC has an additional indirection to dereference the vector's auxiliary allocation.
     1051
     1052\begin{figure}
     1053\setlength{\tabcolsep}{10pt}
     1054\begin{tabular}{llll@{}}
     1055\multicolumn{1}{c}{C} &
     1056\multicolumn{1}{c}{\CFA} &
     1057\multicolumn{1}{c}{\CC (nested vector)}
     1058\\[1em]
     1059\lstinput{20-28}{ar-bchk/control.c} &
     1060\lstinput{20-28}{ar-bchk/control.cfa} &
     1061\lstinput{20-28}{ar-bchk/control.cc}
     1062\\
     1063\multicolumn{1}{c}{(a)} &
     1064\multicolumn{1}{c}{(b)} &
     1065\multicolumn{1}{c}{(c)}
     1066\\[1em]
     1067\multicolumn{4}{l}{
     1068        \includegraphics[page=1,trim=0 9.125in 2in 0,clip]{ar-bchk}
     1069}
     1070\\
     1071\multicolumn{1}{c}{(d)} &
     1072\multicolumn{1}{c}{(e)} &
     1073\multicolumn{1}{c}{(f)}
     1074\\[1em]
     1075\multicolumn{4}{l}{
     1076        \includegraphics[page=2,trim=0 8.75in 2in 0,clip]{ar-bchk}
     1077}
     1078\\
     1079\multicolumn{1}{c}{(g)} &
     1080\multicolumn{1}{c}{(h)} &
     1081\multicolumn{1}{c}{(i)}
     1082\end{tabular}
     1083\caption{Overhead comparison, control case.
     1084All three programs/compilers generate equally performant code when the programmer ``self-checks'' bounds via a loop's condition.
     1085Yet both \CFA and \CC versions generate code that is slower and safer than C's when the programmer might overrun the bounds.}
     1086\label{f:ovhd-ctl}
     1087\end{figure}
     1088
     1089Differences arise when the bound-incorrect programs are passed an array shorter than 100.
     1090The C version, (g), proceeds with undefined behaviour, reading past the end of the array.
     1091The \CFA and \CC versions, (h, i), flag the mistake with the runtime check, the @i >= n@ branch.
     1092This check is provided implicitly by the library types @array@ and @vector@, respectively.
     1093The significant result is the \emph{absence} of runtime checks from the bound-correct translations, (e, f).
     1094The code optimizer has removed them because, at the point where they would occur (immediately past @.L28@/@.L3@), it knows from the surrounding control flow either @i == 0 && 0 < n@ or @i < n@ (directly), \ie @i < n@ either way.
     1095So any repeated checks, \ie the branch and its consequent code (raise error), are removable.
     1096
     1097% Progressing from the control case, a deliberately bound-incorrect mode is no longer informative.
     1098% Rather, given a (well-typed) program that does good work on good data, the issue is whether it is (determinably) bound-correct on all data.
     1099
     1100When dimension sizes get reused, \CFA has an advantage over \CC-vector at getting simply written programs well optimized.
     1101The example case of \VRef[Figures]{f:ovhd-treat-src} and \VRef[]{f:ovhd-treat-asm} is a simple matrix multiplication over a row-major encoding.
     1102Simple means coding directly to the intuition of the mathematical definition without trying to optimize for memory layout.
     1103In the assembly code of \VRef[Figure]{f:ovhd-treat-asm}, the looping pattern of \VRef[Figure]{f:ovhd-ctl} (d, e, f), ``Skip ahead on zero; loop back for next,'' occurs with three nesting levels.
     1104Simultaneously, the dynamic bound-check pattern of \VRef[Figure]{f:ovhd-ctl} (h,~i), ``Get out on invalid,'' occurs, targeting @.L7@, @.L9@ and @.L8@ (bottom right).
     1105Here, \VRef[Figures]{f:ovhd-treat-asm} shows the \CFA solution optimizing into practically the C solution, while the \CC solution shows added runtime bound checks.
     1106Like in \VRef[Figure]{f:ovhd-ctl} (e), the significance is the \emph{absence} of library-imposed runtime checks, even though the source code is working through the the \CFA @array@ library.
     1107The optimizer removed the library-imposed checks because the data structure @array@-of-@array@ is constrained by its type to be shaped correctly for the intuitive looping.
     1108In \CC, the same constraint does not apply to @vector@-of-@vector@.
     1109Because every individual @vector@ carries its own size, two types of bound mistakes are possible.
     1110
     1111\begin{figure}
     1112\setlength{\tabcolsep}{10pt}
     1113\begin{tabular}{llll@{}}
     1114\multicolumn{1}{c}{C} &
     1115\multicolumn{1}{c}{\CFA} &
     1116\multicolumn{1}{c}{\CC (nested vector)}
     1117\\
     1118\lstinput{20-37}{ar-bchk/treatment.c} &
     1119\lstinput{20-37}{ar-bchk/treatment.cfa} &
     1120\lstinput{20-37}{ar-bchk/treatment.cc}
     1121\end{tabular}
     1122\caption{Overhead comparison, differentiation case, source.}
     1123\label{f:ovhd-treat-src}
     1124\end{figure}
     1125
     1126\begin{figure}
     1127\newcolumntype{C}[1]{>{\centering\arraybackslash}p{#1}}
     1128\begin{tabular}{C{1.5in}C{1.5in}C{1.5in}p{1in}}
     1129C &
     1130\CFA &
     1131\CC (nested vector)
     1132\\[1em]
     1133\multicolumn{4}{l}{
     1134        \includegraphics[page=3,trim=0 4in 2in 0,clip]{ar-bchk}
     1135}
     1136\end{tabular}
     1137\caption{Overhead comparison, differentiation case, assembly.
     1138}
     1139\label{f:ovhd-treat-asm}
     1140\end{figure}
     1141
     1142In detail, the three structures received may not be matrices at all, per the obvious/dense/total interpretation; rather, any one might be ragged-right in its rows.
     1143The \CFA solution guards against this possibility by encoding the minor length (number of columns) in the major element (row) type.
     1144In @res@, for example, each of the @M@ rows is @array(float, N)@, guaranteeing @N@ cells within it.
     1145Or more technically, guaranteeing @N@ as the basis for the imposed bound check \emph{of every row.}
     1146As well, the \CC type does not impose the mathematically familiar constraint of $(M \times P) (P \times N) \rightarrow (M \times N)$.
     1147Even assuming away the first issue, \eg that in @lhs@, all minor/cell counts agree, the data format allows the @rhs@ major/row count to disagree.
     1148Or, the possibility that the row count @res.size()@ disagrees with the row count @lhs.size()@ illustrates this bound-mistake type in isolation.
     1149The \CFA solution guards against this possibility by keeping length information separate from the array data, and therefore eligible for sharing.
     1150This capability lets \CFA escape the one-to-one correspondence between array instances and symbolic bounds, where this correspondence leaves a \CC-vector programmer stuck with a matrix representation that repeats itself.
     1151
     1152It is important to clarify that the \CFA solution does not become unsafe (like C) in losing its dynamic checks, even though it becomes fast (as C) in losing them.
     1153The dynamic checks are dismissed as unnecessary \emph{because} the program is safe to begin with.
     1154To achieve the same performance, a \CC programmer must state appropriate assertions or assumptions, to allow the optimizer to dismiss the runtime checks.
     1155% Especially considering that two of them are in the inner-most loop.
     1156The solution requires doing the work of the inner-loop checks as a \emph{preflight step}.
     1157But this step requires looping and doing it upfront gives too much separation for the optimizer to see ``has been checked already'' in the deep loop.
     1158So, the programmer must restate the preflight observation within the deep loop, but this time as an unchecked assumption.
     1159Such assumptions are risky because they introduce further undefined behaviour when misused.
     1160Only the programmer's discipline remains to ensure this work is done without error.
     1161
     1162In summary, the \CFA solution lets a simply stated program have dynamic guards that catch bugs, while letting a simply stated bug-free program run as fast as the unguarded C equivalent.
     1163
     1164\begin{comment}
     1165The ragged-right issue brings with it a source-of-truth difficulty: Where, in the \CC version, is one to find the value of $N$?  $M$ can come from either @res@'s or @lhs@'s major/row count, and checking these for equality is straightforward.  $P$ can come from @rhs@'s major/row count.  But $N$ is only available from columns, \ie minor/cell counts, which are ragged.  So any choice of initial source of truth, \eg
     1166\end{comment}
    10421167
    10431168
    … …  
    12091334However, it only needs @float@'s default constructor, as the other operations are never used.
    12101335Current work by the \CFA team aims to improve this situation.
    1211 Therefore, I had to construct a workaround.
    1212 
    12131336My workaround moves from otype (value) to dtype (pointer) with a default-constructor assertion, where dtype does not generate any constructors but the assertion claws back the default otype constructor.
    12141337\begin{cquote}
    … …  
    14081531
    14091532\subsection{Java}
     1533\label{JavaCompare}
    14101534
    14111535Java arrays are references, so multi-dimension arrays are arrays-of-arrays \see{\VRef{toc:mdimpl}}.
    … …  
    14961620
    14971621\subsection{\CC}
     1622\label{CppCompare}
    14981623
    14991624Because C arrays are difficult and dangerous, the mantra for \CC programmers is to use @std::vector@ in place of the C array.
    1500 While the vector size can grow and shrink dynamically, \vs a fixed-size dynamic size with VLAs, the cost of this extra feature is mitigated by preallocating the maximum size (like the VLA) at the declaration (one dynamic call) to avoid using @push_back@.
     1625While the vector size can grow and shrink dynamically, \vs an unchanging dynamic size with VLAs, the cost of this extra feature is mitigated by preallocating the maximum size (like the VLA) at the declaration.
     1626So, it costs one upfront dynamic allocation and avoids growing the array through pushing.
    15011627\begin{c++}
    15021628vector< vector< int > > m( 5, vector<int>(8) ); // initialize size of 5 x 8 with 6 dynamic allocations
    15031629\end{c++}
    15041630Multidimensional arrays are arrays-of-arrays with associated costs.
    1505 Each @vector@ array has an array descriptor contain the dimension, which allows bound checked using @x.at(i)@ in place of @x[i]@.
    1506 Used with these restrictions, out-of-bound accesses are caught, and in-bound accesses never exercise the vector's ability to grow, preventing costly reallocate and copy, and never invalidate references to contained values.
    1507 This scheme matches Java's safety and expressiveness exactly, but with the inherent costs.
    1508 
    1509 
     1631Each @vector@ array has an array descriptor containing the dimension, which allows bound checked using @x.at(i)@ in place of @x[i]@.
     1632Used with these restrictions, out-of-bound accesses are caught, and in-bound accesses never exercise the vector's ability to grow, preventing costly reallocate-and-copy, and never invalidating references to contained values.
     1633
     1634This scheme matches a Java array's safety and expressiveness exactly, with the same inherent costs.
     1635Notably, a \CC vector of vectors does not provide contiguous element storage (even when upfront allocation is done carefully) because a vector puts its elements in an auxiliary allocation.
     1636So, in spite of @vector< vector< int > >@ appearing to be ``everything by value,'' it is still a first array whose elements include pointers to further arrays.
     1637
     1638\CC has options for working with memory-adjacent data in desirable ways, particularly in recent revisions.
     1639But none makes an allocation with a dynamically given fixed size less awkward than the vector arrangement just described.
     1640
     1641\CC~26 adds @std::inplace_vector@, which provides an interesting vector--array hybrid,\footnote{
     1642  Like a vector, it lets a user construct elements in a loop, rather than imposing uniform construction.
     1643  Yet it preserves \lstinline{std::array}'s ability to be entirely stack-allocated, by avoiding an auxiliary elements' allocation.
     1644} but does not change the fundamental limit of \lstinline{std::array}, that the length, being a template parameter, must be a static value.
     1645
     1646\CC~20's @std::span@ is a view that unifies true arrays, vectors, static sizes and dynamic sizes, under a common API that adds bounds checking.
     1647When wrapping a vector, bounds checking occurs on regular subscripting, \ie one need not remember to use @.at@.
     1648When wrapping a locally declared fixed-size array, bound communication is implicit.
     1649But it has a soundness gap by offering construction from pointer and user-given length.
     1650
     1651\CC~23's @std::mdspan@ adds multidimensional indexing and reshaping capabilities analogous to those built into \CFA's @array@.
     1652Like @span@, it works over multiple underlying container types.
     1653But neither @span@ nor @mdspan@ augments the available allocation options.
     1654
     1655Thus, these options do not offer an allocation with a dynamically given fixed size.
     1656And furthermore, they do not provide any improvement to the C flexible array member pattern, for making a dynamic amount of storage contiguous with its header, as do \CFA's accordions.
     1657
     1658
     1659\begin{comment}
    15101660\subsection{Levels of Dependently Typed Arrays}
    15111661
     1662TODO: fix the position; checked c does not do linear types
    15121663\CFA's array is the first lightweight application of dependently-typed bound tracking to an extension of C.
    15131664Other extensions of C that apply dependently-typed bound tracking are heavyweight, in that the bound tracking is part of a linearly-typed ownership-system, which further helps guarantee statically the validity of every pointer deference.
    … …  
    15431694it can also do these other cool checks, but watch how I can mess with its conservativeness and termination
    15441695
    1545 Two current, state-of-the-art array languages, Dex\cite{arr:dex:long} and Futhark\cite{arr:futhark:tytheory}, offer novel contributions concerning similar, restricted dependent types for tracking array length.
     1696Two contemporary array-centric languages, Dex\cite{arr:dex:long} and Futhark\cite{arr:futhark:tytheory}, contribute similar, restricted dependent types for tracking array length.
    15461697Unlike \CFA, both are garbage-collected functional languages.
    15471698Because they are garbage-collected, referential integrity is built-in, meaning that the heavyweight analysis, that \CFA aims to avoid, is unnecessary.
    … …  
    15541705There is a particular emphasis on an existential type, enabling callee-determined return shapes.
    15551706
    1556 
    1557 Dex uses a novel conception of size, embedding its quantitative information completely into an ordinary type.
    1558 
    1559 Futhark and full-strength dependently typed languages treat array sizes are ordinary values.
     1707Dex uses an Ada-style conception of size, embedding quantitative information completely into an ordinary type.
     1708
     1709Futhark and full-strength dependently typed languages treat array sizes as ordinary values.
    15601710Futhark restricts these expressions syntactically to variables and constants, while a full-strength dependent system does not.
    15611711
    1562 \CFA's hybrid presentation, @forall( [N] )@, has @N@ belonging to the type system, yet has no instances.
     1712\CFA's hybrid presentation, @forall( [N] )@, has @N@ belonging to the type system, yet no objects of type @[N]@ occur.
    15631713Belonging to the type system means it is inferred at a call site and communicated implicitly, like in Dex and unlike in Futhark.
    15641714Having no instances means there is no type for a variable @i@ that constrains @i@ to be in the range for @N@, unlike Dex, [TODO: verify], but like Futhark.
    … …  
    15691719
    15701720In Ada and Dex, an array is conceived as a function whose domain must satisfy only certain structural assumptions, while in C, \CC, Java, Futhark and \CFA today, the domain is a prefix of the natural numbers.
    1571 The generality has obvious aesthetic benefits for programmers working on scheduling resources to weekdays, and for programmers who prefer to count from an initial number of their own choosing.
     1721The Ada--Dex generality has aesthetic benefits for certain programmers.  For those working on scheduling resources to weekdays:
     1722For those who prefer to count from an initial number of their own choosing:
    15721723
    15731724This change of perspective also lets us remove ubiquitous dynamic bound checks.
    … …  
    16051756(unsafe_from_ordinal a (idiv o bs), unsafe_from_ordinal b (rem o bs))
    16061757\end{cfa}
     1758% fix mike's syntax highlighter
    16071759and by a user-provided adapter expression at the call site that shows how to indexing with a tuple is backed by indexing each dimension at a time
    16081760\begin{cfa}
    … …  
    16161768
    16171769\subsection{Static Safety in C Extensions}
     1770\end{comment}
    16181771
    16191772
    16201773\section{Future Work}
    16211774
    1622 \subsection{Array Syntax}
    1623 
    1624 An important goal is to recast @array(...)@ syntax into C-style @[]@.
    1625 The proposal (which is partially implemented) is an alternate dimension and subscript syntax.
    1626 C multi-dimension and subscripting syntax uses multiple brackets.
    1627 \begin{cfa}
    1628 int m@[2][3]@;  // dimension
    1629 m@[0][1]@ = 3;  // subscript
    1630 \end{cfa}
    1631 Leveraging this syntax, the following (simpler) syntax should be intuitive to C programmers with only a small backwards compatibility issue.
    1632 \begin{cfa}
    1633 int m@[2, 3]@;  // dimension
    1634 m@[0, 1]@ = 3;  // subscript
    1635 \end{cfa}
    1636 However, the new subscript syntax is not backwards compatible, as @0, 1@ is a comma expression.
    1637 Interestingly, disallowed the comma expression in this context eliminates an unreported error: subscripting a matrix with @m[i, j]@ instead of @m[i][j]@, which selects the @j@th row not the @i, j@ element.
    1638 Hence, a comma expression in this context is rare.
    1639 Finally, it is possible to write @m[(i, j)]@ in the new syntax to achieve the equivalent of the old @m[i, j]@.
    1640 Note, the new subscript syntax can easily be internally lowered to @[-][-]...@ and handled as regular subscripting.
    1641 The only ambiguity with C syntax is for a single dimension array, where the syntax for old and new are the same.
    1642 \begin{cfa}
    1643 int m[2@,@];  // single dimension
    1644 m[0] = 3;  // subscript
    1645 \end{cfa}
    1646 The solution for the dimension is to use a terminating comma to denote a new single-dimension array.
    1647 This syntactic form is also used for the (rare) singleton tuple @[y@{\color{red},}@]@.
     1775% \subsection{Array Syntax}
     1776
     1777An important goal is to recast \CFA-style @array(...)@ syntax into C-style array syntax.
     1778The proposal (which is partially implemented) is an alternate dimension and subscript syntax for multi-dimension arrays.
     1779C multi-dimension and subscripting syntax uses multiple bracketed constants/expressions.
     1780\begin{cfa}
     1781int m@[2][3]@;   // dimension
     1782m@[0][1]@ = 3;   // subscript
     1783\end{cfa}
     1784The alternative \CFA syntax is a comma separated list:
     1785\begin{cfa}
     1786int m@[2, 3]@;   // dimension
     1787m@[0, 1]@ = 3;   // subscript
     1788\end{cfa}
     1789which should be intuitive to C programmers and is used in mathematics $M_{i,j}$ and other programing languages, \eg PL/I, Fortran.
     1790With respect to the dimension expressions, C only allows an assignment expression, not a comma expression.
     1791\begin{cfa}
     1792        a[i, j];
     1793test.c:3:16: error: expected ']' before ',' token
     1794\end{cfa}
     1795However, there is an ambiguity for a single dimension array, where the syntax for old and new arrays are the same, @int ar[10]@.
     1796The solution is to use a terminating comma to denote a \CFA-style single-dimension array.
     1797\begin{cfa}
     1798int ar[2$\Huge\color{red},$];  // single dimension new array
     1799\end{cfa}
     1800This syntactic form is also used for the (rare) singleton tuple @[y@{\Large\color{red},}@]@.
    16481801The extra comma in the dimension is only mildly annoying, and acts as eye-candy differentiating old and new arrays.
    1649 The subscript operator is not an issue as overloading selects the correct single-dimension operation for old/new array types.
    1650 The ultimately goal is to replace all C arrays with \CFA arrays, establishing a higher level of safety in C programs, and eliminating the need for the terminating comma.
    1651 
    1652 
     1802Hence, \CFA can repurpose the comma expression in this context for a list of dimensions.
     1803The ultimate goal is to replace all C arrays with \CFA arrays, establishing a higher level of safety in C programs, and eliminating the need for the terminating comma.
     1804With respect to the subscript expression, the comma expression is allowed.
     1805However, a comma expression in this context is rare, and is most commonly a (silent) mistake: subscripting a matrix with @m[i, j]@ instead of @m[i][j]@ selects the @j@th row not the @i, j@ element.
     1806It is still possible to write @m[(i, j)]@ in the new syntax to achieve the equivalent of the old @m[i, j]@.
     1807Internally, the compiler must de-sugar @[i, j, k]@ into @[i][j][k]@ to match with three calls to subscript operators.
     1808Note, there is no ambiguity for subscripting a single dimensional array, as the subscript operator selects the correct form from the array type.
     1809Currently, @array@ supports the old and new subscript syntax \see{\VRef[Figure]{f:ovhd-treat-src}}, including combinations of new and old, @arr[1, 2][3]@.
     1810The new subscript syntax can be extended to C arrays for uniformity, but requires the non-compatible removal of the (rare) comma-expression as a subscript.
     1811
     1812
     1813\begin{comment}
    16531814\subsection{Range Slicing}
    16541815
    … …  
    16591820
    16601821
    1661 \begin{comment}
    16621822\section{\texorpdfstring{\CFA}{Cforall}}
    16631823
    … …  
    16971857Using a compiler-produced value eliminates an opportunity for user error.
    16981858
    1699 TODO: fix in following: even the alloc call gives bad code gen: verify it was always this way; walk back the wording about things just working here; assignment (rebind) seems to offer workaround, as in bkgd-cfa-arrayinteract.cfa
     1859...someday... fix in following: even the alloc call gives bad code gen: verify it was always this way; walk back the wording about things just working here; assignment (rebind) seems to offer workaround, as in bkgd-cfa-arrayinteract.cfa
    17001860
    17011861Bringing in another \CFA feature, reference types, both resolves a sore spot of the last example, and gives a first example of an array-interaction bug.
    … …  
    17061866(*ar2)[5];
    17071867\end{cfa}
    1708 Using ``reference to array'' works at resolving this issue.  TODO: discuss connection with Doug-Lea \CC proposal.
     1868Using ``reference to array'' works at resolving this issue.  ...someday... discuss connection with Doug-Lea \CC proposal.
    17091869\begin{cfa}
    17101870tm (&ar3)[10] = *alloc();
    … …  
    17141874
    17151875Using proper array types (@ar2@ and @ar3@) addresses a concern about using raw element pointers (@ar1@), albeit a theoretical one.
    1716 TODO xref C standard does not claim that @ar1@ may be subscripted,
     1876...someday... xref C standard does not claim that @ar1@ may be subscripted,
    17171877because no stage of interpreting the construction of @ar1@ has it be that ``there is an \emph{array object} here.''
    17181878But both @*ar2@ and the referent of @ar3@ are the results of \emph{typed} @alloc@ calls,
    … …  
    17201880
    17211881The ``reference to array'' type has its sore spots too.
    1722 TODO see also @dimexpr-match-c/REFPARAM_CALL@ (under @TRY_BUG_1@)
    1723 
    1724 TODO: I fixed a bug associated with using an array as a T.  I think.  Did I really?  What was the bug?
     1882...someday... see also @dimexpr-match-c/REFPARAM_CALL@ (under @TRY_BUG_1@)
     1883
     1884...someday... I fixed a bug associated with using an array as a T.  I think.  Did I really?  What was the bug?
    17251885\end{comment}
Note: See TracChangeset for help on using the changeset viewer.