From f993558b2c7d5cb38b3059f3676803eae424e1a7 Mon Sep 17 00:00:00 2001 From: Pavel Kirienko Date: Tue, 14 Jul 2020 00:32:56 +0300 Subject: [PATCH] Final fixes for #75 --- dsdl | 2 +- specification/dsdl/attributes.tex | 9 ++++----- specification/dsdl/serializable_types.tex | 7 ++++--- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/dsdl b/dsdl index c1191d36..0db3739d 160000 --- a/dsdl +++ b/dsdl @@ -1 +1 @@ -Subproject commit c1191d36b19a082f85c74be24131e6b205e46e8f +Subproject commit 0db3739d2a68e8c3ab9e9506132ad12243d37bac diff --git a/specification/dsdl/attributes.tex b/specification/dsdl/attributes.tex index 5831b4cd..2bf92005 100644 --- a/specification/dsdl/attributes.tex +++ b/specification/dsdl/attributes.tex @@ -160,7 +160,7 @@ \subsubsection{Offset attribute} $$ \texttt{\_offset\_}_\text{union} = \bigcup\limits_{i=1}^{n} - \left\{ \lceil{}\log_2 n\rceil{} + b : b \in B_i \right\} + \left\{ 2^{\lceil\log_2 \text{max}\left(8, \lceil\log_2 n\rceil\right)\rceil} + b : b \in B_i \right\} $$ where $n$ is the number of fields defined in the current union definition, and $B_i$ is the bit length set of the data type of the field number $i$. @@ -186,7 +186,7 @@ \subsubsection{Offset attribute} uint8 a #@print _offset_ # Would fail: it's a tagged union, _offset_ is undefined until after the last field uint16 b - @assert _offset_ == {1 + 8, 1 + 16} + @assert _offset_ == {8 + 8, 8 + 16} --- @assert _offset_ == {0} float16 a @@ -196,12 +196,11 @@ \subsubsection{Offset attribute} int4 b @assert _offset_ == {24} uint8[<4] c - @assert _offset_ == 2 + {24, 32, 40, 48} - void6 + @assert _offset_ == 8 + {24, 32, 40, 48} @assert _offset_ % 8 == {0} # One of the main usages for _offset_ is statically proving that the following field is byte-aligned # for all possible valid serialized representations of the preceding fields. It is done by computing - # a remainder as shown below. If the field is aligned, the remainder set will equal {0}. If the + # a remainder as shown above. If the field is aligned, the remainder set will equal {0}. If the # remainder set contains other elements, the field may be misaligned under some circumstances. # If the remainder set does not contain zero, the field is never aligned. uint8 well_aligned # Proven to be byte-aligned. diff --git a/specification/dsdl/serializable_types.tex b/specification/dsdl/serializable_types.tex index 67803dfe..724251e7 100644 --- a/specification/dsdl/serializable_types.tex +++ b/specification/dsdl/serializable_types.tex @@ -317,7 +317,8 @@ \subsubsection{Type polymorphism and equivalency} \item both $B$ and $D$ define tagged unions; \item $B$ is not $D$; \item $b \leq d$; - \item $\lceil{}\log_2 b\rceil{} = \lceil{}\log_2 d\rceil{}$; + \item $2^{\lceil\log_2 \text{max}\left(8, \lceil\log_2 b\rceil\right)\rceil} = + 2^{\lceil\log_2 \text{max}\left(8, \lceil\log_2 d\rceil\right)\rceil}$; \item for $i \in \left[0, b\right)$, the type of the field attribute of $D$ at index $i$ is the same or is a subtype of the type of the field attribute of $B$ at index $i$. \item for $i \in \left[0, b\right)$, the name of the field attribute of $D$ at index $i$ @@ -352,7 +353,7 @@ \subsubsection{Type polymorphism and equivalency} Subtyping example for union types. First type: \begin{minted}{python} - @union # The implicit union tag field is 2 bits wide + @union # The implicit union tag field is 8 bits wide uavcan.primitive.Empty.1.0 foo float16 bar uint8 zoo @@ -361,7 +362,7 @@ \subsubsection{Type polymorphism and equivalency} The second type is a structural subtype of the first type: \begin{minted}{python} - @union # The implicit union tag field is 2 bits wide + @union # The implicit union tag field is 8 bits wide uavcan.diagnostic.Record.1.0 foo # Subtype float16 bar # Same uint8 zoo # Same