[asl] fixed Typing.CheckCommonBitfieldsAlign.check

asllib/AST.mli

@@ -200,7 +200,7 @@ and pattern_desc =
 
 and pattern = pattern_desc annotated
 
-(** Indexes an array, a bitvector. *)
+(** Slices define lists of indices into arrays and bitvectors. *)
 and slice =
   | Slice_Single of expr
       (** [Slice_Single i] is the slice of length [1] at position [i]. *)
@@ -212,7 +212,7 @@ and slice =
   | Slice_Star of expr * expr
       (** [Slice_Start (factor, length)] denotes the slice starting at [factor
           * length] of length [n]. *)
-(** All position mentionned above are included. *)
+(** All positions mentioned above are inclusive. *)
 
 and call = {
   name : identifier;

asllib/doc/ASLFormal.tex

@@ -223,7 +223,8 @@ \subsection{Lists}
 $\listlen{\emptylist} \triangleq 0$ and $\listlen{v_1,\ldots,v_k}=k$.
 \end{definition}
 
-We use the notation $a..b$, where $a,b\in\Z$ and $a\leq b$, as a shorthand for the interval $[a\ldots b]$.
+We use the notation $a..b$, where $a,b\in\Z$ and as a shorthand for the interval $[a\ldots b]$
+(counting up when $a \leq b$ and counting down when $a \geq b$).
 We write $x_{a..b}$ as a shorthand for the sequence $x_a \ldots x_b$.
 %
 We write $i=1..k: V(i)$, where $V(i)$ is a mathematical expression parameterized by $i$,

asllib/doc/ASLmacros.tex

@@ -1830,7 +1830,7 @@
 \newcommand\Prosecheckcommonbitfieldsalign[3]{\hyperlink{def-checkcommonbitfieldsalign}{checking} that all pairs of bitfields in #2 that are in the same scope
   and share the same name correspond to the same slice of the containing bitvector type in the static environment #1 yields $\True$}
 \newcommand\checkcommonbitfieldsalign[0]{\hyperlink{def-checkcommonbitfieldsalign}{\textfunc{check\_common\_bitfields\_align}}}
-\newcommand\absolutefieldsalign[0]{\hyperlink{def-absolutefieldsalign}{\textfunc{absolute\_fields\_align}}}
+\newcommand\absolutebitfieldsalign[0]{\hyperlink{def-absolutefieldsalign}{\textfunc{absolute\_bitfields\_align}}}
 \newcommand\TAbsField[0]{\hyperlink{def-tabsfield}{\mathbb{A}\mathbb{B}\mathbb{F}}}
 \newcommand\Prosebitfieldstoabsolute[4]{\hyperlink{def-bitfieldstoabsolute}{generating} the \absolutebitfields\ for the list of bitfields #2 and its nested bitfields
   with #3 as the parent \absolutebitfield\ in the static environment #1 yields the set of fields #4}
@@ -1839,7 +1839,7 @@
 \newcommand\Proseslicetoindices[3]{\hyperlink{def-slicetoindices}{obtaining} the sequence of indices for a slice #1 in the static environment #2 yields #3}
 \newcommand\slicetoindices[0]{\hyperlink{def-slicetoindices}{\textfunc{slice\_to\_indices}}}
 \newcommand\Prosesliceindicesbyslices[3]{\hyperlink{def-sliceindicesbyslices}{slicing} the list of indices #1 according to #2 yields #3}
-\newcommand\sliceindicesbyslices[0]{\hyperlink{def-sliceindicesbyslices}{\textfunc{slice\_indices\_by\_slices}}}
+\newcommand\selectbyslices[0]{\hyperlink{def-sliceindicesbyslices}{\textfunc{select\_by\_slices}}}
 
 \newcommand\checknoduplicates[0]{\hyperlink{def-checknoduplicates}{\textfunc{check\_no\_duplicates}}}
 \newcommand\filteroptionlist[0]{\hyperlink{def-filteroptionlist}{\textfunc{filter\_option\_list}}}

asllib/doc/Bitfields.tex

@@ -10,13 +10,14 @@ \subsection{Example}
 \listingref{bitfields1} declares a global variable whose type is a bitvector with bitfields.
 \ASLListing{A bitvector type with bitfields}{bitfields1}{\definitiontests/Bitfields.asl}
 \begin{itemize}
-  \item The expression \texttt{myData.flag} evaluates to the value \texttt{myData[4]} of type \texttt{bits(1)};
-  \item The expression \texttt{myData.data} evaluates to the value \texttt{[myData[3:0], myData[8:5]]} of type \texttt{bits(8)};
-  \item There is no bitfield which accesses \texttt{myData[15:10]};
+  \item The expression \texttt{myData.flag} evaluates to the same value as \verb|myData[4]|, with type \verb|bits(1)|;
+  \item The expression \texttt{myData.data} evaluates to the same value as \\
+        \verb|myData[3:0] :: myData[8:5]|, with type \verb|bits(8)|;
+  \item There is no bitfield which accesses \verb|myData[15:10]|;
   \item The value field overlaps with the other fields;
-  \item The slices \texttt{3:0} and \texttt{8:5} which define \texttt{data} do not overlap.
+  \item The slices \verb|3:0| and \verb|8:5| which define \texttt{data} do not overlap.
 \end{itemize}
-Note that in the \texttt{data} bitfield, bits \texttt{3:0} come before bits \texttt{8:5},
+Note that in the \texttt{data} bitfield, bits |3:0| come before bits |8:5|,
 which is a different order from their occurrence in \texttt{myData}.
 
 \hypertarget{def-singleslice}{}
@@ -44,7 +45,7 @@ \section{Nested Bitfields}
 bitvector type.
 %
 The \hypertarget{def-absolutebitfield}{\absolutebitfield} of a given bitfield consists of bits absolute name and its
-absolute slices.
+\absoluteslices.
 
 Further, the \hypertarget{def-bitfieldscope}{\bitfieldscope} of a bitfield is its \absolutename, with the last
 identifier (the bitfield's name) removed.
@@ -617,6 +618,17 @@ \subsubsection{Formally}
 
 Premises in \TypingRuleRef{TBits} guarantee that $\vwidth > 0$ holds.
 
+\subsubsection{Example}
+\listingref{CommonBitfieldsAlignError} shows an example where the two bitfields named \texttt{common}
+exist in the same \bitfieldscope, but their \absoluteslices\ are not the same.
+Specifically, the \absoluteslice\ for the bitfield \texttt{common} is \texttt{[1:0]}
+whereas the \absoluteslice\ for the bitfield \texttt{sub.common} is \texttt{[0, 1]}.
+Typechecking this example results in the type error \BadSlices.
+
+\ASLListing{An example where two bitfields of the same name (\texttt{common}) exist in the same scope
+but have different absolute slices}
+{CommonBitfieldsAlignError}{\typingtests/TypingRule.CheckCommonBitfieldsAlign.Error.asl}
+
 \subsubsection{Prose}
 One of the following applies:
 \begin{itemize}
@@ -631,12 +643,12 @@ \subsubsection{Prose}
     \item $\vbitfields$ is not the empty list;
     \item define $\vlastindex$ as $\vwidth - 1$;
     \item define $\vtopabsolute$ as an \absolutebitfield\ with the empty list
-          for a name and a the interval $0..\vlastindex$ (that is, the entire range
+          for a name and a the interval $\vlastindex..0$ (that is, the entire range
           of indices for the containing bitvector type),
           as an artificial top-level \absolutebitfield\ for the entire bitvector type;
     \item \Prosebitfieldstoabsolute{$\tenv$}{$\vbitfields$}{$\vtopabsolute$}{$\vfs$};
     \item checking that \absolutebitfields\ $\vfone$ and $\vftwo$ align via
-          $\absolutefieldsalign$ in $\tenv$, for every $\vfone$ and $\vftwo$ in $\vfs$,
+          $\absolutebitfieldsalign$ in $\tenv$, for every $\vfone$ and $\vftwo$ in $\vfs$,
           yields $\True$\ProseTerminateAs{\BadSlices};
     \item the result is $\True$.
   \end{itemize}
@@ -655,9 +667,9 @@ \subsubsection{Formally}
 \inferrule[non\_empty]{
   \vbitfields \neq \emptylist\\
   \vlastindex \eqdef \vwidth - 1\\
-  \vtopabsolute \eqdef (\emptylist, 0..\vlastindex)\\
+  \vtopabsolute \eqdef (\emptylist, \vlastindex..0)\\
   \bitfieldstoabsolute(\tenv, \vbitfields, \vtopabsolute) \typearrow \vfs\\
-  \checktrans{\forall \vfone, \vftwo \in \vfs: \absolutefieldsalign(\vfone, \vftwo)}{\BadSlices} \typearrow \True \OrTypeError
+  \checktrans{\forall \vfone, \vftwo \in \vfs: \absolutebitfieldsalign(\vfone, \vftwo)}{\BadSlices} \typearrow \True \OrTypeError
 }{
   \checkcommonbitfieldsalign(\tenv, \vbitfields, \vwidth) \typearrow \True
 }
@@ -735,7 +747,7 @@ \subsubsection{Formally}
   \bitfieldgetslices(\vbf) \typearrow \vslices\\
   \vs \in \vslices: \slicetoindices(\tenv, \vs) \typearrow \indices_\vs\\
   \vslicesasindices \eqdef [\vs \in \vslices: \indices_\vs]\\
-  \sliceindicesbyslices(\vabsslices, \vslicesasindices) \typearrow \vbfindices\\
+  \selectbyslices(\vabsslices, \vslicesasindices) \typearrow \vbfindices\\
   \vbfabsolute \eqdef (\vbfname, \vbfindices)\\
   \bitfieldgetnested(\vbf) \typearrow \vnested\\
   \bitfieldstoabsolute(\tenv, \vnested, \vbfabsolute) \typearrow \vabsbitfieldsone
@@ -753,33 +765,36 @@ \subsubsection{Formally}
 \hypertarget{def-sliceindicesbyslices}{}
 The function
 \[
-\sliceindicesbyslices(\overname{\N^+}{\indices}, \overname{\N^+}{\sliceindices})
+\selectbyslices(\overname{\N^+}{\indices}, \overname{\N^+}{\sliceindices})
 \aslto \overname{\N^*}{\vabsslice}
 \]
 considers the list $\indices$ as a list of indices into a bitvector type (essentially, a slice of it),
-and the list $\sliceindices$ as a list of indices into $\indices$ (essentially a slice of a slice),
+and the list $\sliceindices$ as a list of indices into $\indices$ (a slice of a slice),
 and returns the sub-list of $\indices$ indicated by the indices in $\sliceindices$.
-% The reference abstract away the implementation, which represents sequence of indices via intervals.
+% The reference abstracts away from the implementation,
+% which represents sequence of indices via intervals.
 
 \subsubsection{Prose}
 All of the following apply:
 \begin{itemize}
-  \item view $\sliceindices$ as the list $S_{1..m}$;
-  \item define $\vabsslice$ as the list $\indices[S_i]$ for $i=1..m$.
+  \item view $\sliceindices$ as the list $S_{m..0}$;
+  \item view $\indices$ as the list $I_{n..0}$;
+  \item define $\vabsslice$ as the list $I[S_m] \ldots I[S_0]$.
 \end{itemize}
 
 \subsubsection{Formally}
 \begin{mathpar}
 \inferrule{}{
-  \sliceindicesbyslices(\indices, \overname{S_{1..m}}{\sliceindices}) \typearrow \overname{i=1..m: \indices[S_i]}{\vabsslice}
+  \selectbyslices(\overname{I_{n..0}}{\indices}, \overname{S_{m..0}}{\sliceindices}) \typearrow
+    \overname{I[S_m] \ldots I[S_0]}{\vabsslice}
 }
 \end{mathpar}
 
-\TypingRuleDef{AbsoluteFieldsAlign}
+\TypingRuleDef{AbsoluteBitfieldsAlign}
 \hypertarget{def-absolutefieldsalign}{}
 The function
 \[
-\absolutefieldsalign(\overname{\TAbsField}{\vf}, \overname{\TAbsField}{\vg})
+\absolutebitfieldsalign(\overname{\TAbsField}{\vf}, \overname{\TAbsField}{\vg})
 \aslto \overname{\Bool}{\vb}
 \]
 tests whether the \absolutebitfields\ $\vfone$ and $\vftwo$ share the same name
@@ -810,7 +825,7 @@ \subsubsection{Formally}
   \vsamescope \eqdef \listprefix(\vscopeone, \vscopetwo) \lor \listprefix(\vscopetwo, \vscopeone)\\
   \vb \eqdef (\nameone = \nametwo\ \land\ \vsamescope) \Longrightarrow (\vsliceone = \vslicetwo)
 }{
-  \absolutefieldsalign(\overname{(\vf_{1..k}, \vsliceone)}{\vf}, \overname{(\vg_{1..n}, \vslicetwo)}{\vf})
+  \absolutebitfieldsalign(\overname{(\vf_{1..k}, \vsliceone)}{\vf}, \overname{(\vg_{1..n}, \vslicetwo)}{\vf})
   \typearrow \vb
 }
 \end{mathpar}
@@ -831,7 +846,7 @@ \subsubsection{Prose}
   \item \Prosestaticeval{$\tenv$}{$\vw$}{the literal for the integer $\vz_\vw$};
   \item define $\vstart$ as $\vz_\vi$;
   \item define $\vend$ as $\vz_\vi + \vz_\vw - 1$;
-  \item define $\indices$ as the list of integers greater or equal to $\vstart$ and less than or equal to $\vend$.
+  \item define $\indices$ as the list of integers starting at $\vend$ and counting down to $\vstart$.
 \end{itemize}
 
 \subsubsection{Formally}
@@ -842,6 +857,6 @@ \subsubsection{Formally}
   \vstart \eqdef \vz_\vi\\
   \vend \eqdef \vz_\vi + \vz_\vw - 1\\
 }{
-  \slicetoindices(\tenv, \overname{\SliceLength(\vi, \vw)}{\vs}) \typearrow \overname{\vstart..\vend}{\indices}
+  \slicetoindices(\tenv, \overname{\SliceLength(\vi, \vw)}{\vs}) \typearrow \overname{\vend..\vstart}{\indices}
 }
 \end{mathpar}

asllib/doc/Slicing.tex

@@ -153,7 +153,7 @@ \subsection{Abstract Syntax}
   |\ & \SliceStar(\overname{\expr}{\vi}, \overname{\expr}{\vn}) &
 \end{flalign*}
 
-Note that the syntax \texttt{[:width]} is a shorthand for \texttt{x[0:width]}.
+Note that the syntax \texttt{[:width]} is a shorthand for \texttt{x[width-1:0]}.
 
 \ASTRuleDef{Slice}
 \hypertarget{build-slice}{}
@@ -463,7 +463,7 @@ \subsubsection{Example (Length Slice)}
 \subsubsection{Example (Scaled Slice)}
 In \listingref{semantics-scaledslice},
 \texttt{x[3*:2]} evaluates to \texttt{'11'}.
-\ASLListing{A scaled lice}{semantics-scaledslice}{\semanticstests/SemanticsRule.SliceStar.asl}
+\ASLListing{A scaled slice}{semantics-scaledslice}{\semanticstests/SemanticsRule.SliceStar.asl}
 
 \subsubsection{Prose}
 One of the following applies:

asllib/tests/ASLDefinition.t/Bitfields_nested.asl

@@ -1,20 +1,20 @@
-type Nested_Type of bits(32) {      // absolute fields
-   [31:16] fmt0 {                   // [31:16] fmt0
-        [15] common,                // [31:31] fmt0.common
-        [14:0] layer1 {             // [30:16] fmt0.layer1
-            [14:13] remainder {     // [30:29] fmt0.layer1.remainder
-               [1]  moving,         // [30:30] fmt0.layer1.remainder.moving
-               [0]  extra           // [29:29] fmt0.layer1.remainder.extra
+type Nested_Type of bits(32) {       // absolute fields
+   [31:16] fmt0 {                    // [31:16] fmt0
+        [15] common,                 // [31:31] fmt0.common
+        [14:13, 12:2, 1, 0] layer1 { // [30:16] fmt0.layer1
+            [14:13] remainder {      // [30:29] fmt0.layer1.remainder
+               [1]  moving,          // [30:30] fmt0.layer1.remainder.moving
+               [0]  extra            // [29:29] fmt0.layer1.remainder.extra
             },
         },
-        [13] extra                  // [29:29] fmt0.extra
+        [13] extra                   // [29:29] fmt0.extra
    },
-   [31:16] fmt1 {                   // [31:16] fmt1
-       [15] common,                 // [31:31] fmt1.common
-       [0]  moving                  // [16:16] fmt1.moving
+   [31:16] fmt1 {                    // [31:16] fmt1
+       [15] common,                  // [31:31] fmt1.common
+       [0]  moving                   // [16:16] fmt1.moving
    },
-   [31] common,                     // [31:31] common
-   [0]  fmt                         // [0:0] fmt
+   [31] common,                      // [31:31] common
+   [0]  fmt                          // [0:0] fmt
 };
 
 var nested : Nested_Type = '10101010101010101010101010101010';

asllib/tests/ASLDefinition.t/Bitvector_slices.asl

@@ -1,6 +1,12 @@
 func main() => integer
 begin
     let bv : bits(6) = '110010';
+    assert  bv[5] == '1' &&
+            bv[4] == '1' &&
+            bv[3] == '0' &&
+            bv[2] == '0' &&
+            bv[1] == '1' &&
+            bv[0] == '0';
     assert bv == bv[5,4,3,2,1,0];
     assert bv != bv[0,1,2,3,4,5];
     assert bv == bv[5:0];

asllib/tests/ASLTypingReference.t/TypingRule.CheckCommonBitfieldsAlign.Error.asl

@@ -0,0 +1,6 @@
+type Nested_Type of bits(2) {
+    [1:0] sub {
+        [0,1] common
+    },
+    [1:0] common
+};

asllib/tests/ASLTypingReference.t/run.t

@@ -18,6 +18,12 @@ ASL Typing Tests:
   $ aslref TypingRule.LDTyped.asl
   $ aslref TypingRule.LDTuple.asl
   $ aslref TypingRule.Lit.asl
+  $ aslref TypingRule.CheckCommonBitfieldsAlign.Error.asl
+  File TypingRule.CheckCommonBitfieldsAlign.Error.asl, line 1, character 20 to
+    line 6, character 1:
+  ASL Typing error:
+    bitfields `sub.common` and `common` are in the same scope but define different slices of the containing bitvector type: [0, 1] and [1:0], respectively.
+  [1]
 
 ASL Typing Tests / annotating types:
   $ aslref TypingRule.TReal.asl

asllib/tests/bitfield-alignment.t/good-scope1.asl

@@ -1,7 +1,7 @@
 type Nested_Type of bits(2) {
     [1:0] sub {
         [1:0] sub {
-            [0,1] lowest
+            [1,0] lowest
         }
     },
 

asllib/tests/bitfield-alignment.t/good-slice_equivalence.asl

@@ -1,11 +1,14 @@
 type Nested_Type of bits(16) {
-    [12:9, 7:2] slices {    // [12:9, 7:2] slices
-        [5:2, 7:6, 9:8] sub // [12:11, 7:2] slices.sub
+    [15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0] all,
+    // [12, 11, 10, 9] [7, 6, 5, 4, 3, 2]
+    [12:9, 7:2] slices { // slices = [12:9, 7:2]
+        [5:2, 9:8, 7:6] sub // [7:4][12:9] slices.sub
     },
 
-    [9+:4, 2+:6] slices1 {  // [12:9, 7:2] slices1
-        [5:2, 7:6, 9:8] sub // [12:11, 7:2] slices1.sub
+    // [12, 11, 10, 9] [7, 6, 5, 4, 3, 2]
+    [9+:4, 2+:6] slices1 {  // slices1 = [12:9, 7:2]
+        [5:2, 9:8, 7:6] sub // [7:4][12:9] slices1.sub
     },
 
-    [12:11, 7:2] sub        // [12:11, 7:2] sub
+    [7:4, 12:9] sub
 };

asllib/tests/bitfield-alignment.t/run.t

@@ -4,17 +4,17 @@
   $ aslref --no-exec bad-scope1.asl
   File bad-scope1.asl, line 1, character 20 to line 5, character 1:
   ASL Typing error:
-    bitfields `sub` and `sub.sub` are in the same scope but define different slices of the containing bitvector type: [1:0] and [0:0], respectively.
+    bitfields `sub` and `sub.sub` are in the same scope but define different slices of the containing bitvector type: [1:0] and [0], respectively.
   [1]
 
   $ aslref --no-exec bad-scope2.asl
   File bad-scope2.asl, line 1, character 20 to line 7, character 1:
   ASL Typing error:
-    bitfields `sub` and `sub.sub.sub` are in the same scope but define different slices of the containing bitvector type: [1:0] and [1:1], respectively.
+    bitfields `sub` and `sub.sub.sub` are in the same scope but define different slices of the containing bitvector type: [1:0] and [1], respectively.
   [1]
 
   $ aslref --no-exec bad-scope3.asl
   File bad-scope3.asl, line 1, character 20 to line 9, character 1:
   ASL Typing error:
-    bitfields `sub.sub.lowest` and `lowest` are in the same scope but define different slices of the containing bitvector type: [1:0] and [1:1, 0:0], respectively.
+    bitfields `sub.sub.lowest` and `lowest` are in the same scope but define different slices of the containing bitvector type: [0, 1] and [1:0], respectively.
   [1]