Merge pull request #1020 from herd/asl-sync-reference

ASL synchronize reference with the implementation

asllib/StaticEnv.ml

@@ -269,15 +269,27 @@ let add_subtype s t env =
     global = { env.global with subtypes = IMap.add s t env.global.subtypes };
   }
 
+(* Begin IsGlobalUndefined *)
 let is_global_undefined x (genv : global) =
-  not
-    (IMap.mem x genv.storage_types
-    || IMap.mem x genv.subprograms
-    || IMap.mem x genv.declared_types)
+  (not
+     (IMap.mem x genv.storage_types
+     || IMap.mem x genv.subprograms
+     || IMap.mem x genv.declared_types))
+  |: TypingRule.IsGlobalUndefined
+(* End *)
 
-let is_local_undefined x (lenv : local) = not (IMap.mem x lenv.storage_types)
+(* Begin IsLocalUndefined *)
+let is_local_undefined x (lenv : local) =
+  (not (IMap.mem x lenv.storage_types)) |: TypingRule.IsLocalUndefined
+(* End *)
 
+(* Begin IsUndefined *)
 let is_undefined x env =
-  is_global_undefined x env.global && is_local_undefined x env.local
+  is_global_undefined x env.global
+  && is_local_undefined x env.local |: TypingRule.IsUndefined
+(* End *)
 
-let is_subprogram x env = IMap.mem x env.global.subprograms
+(* Begin IsSubprogram *)
+let is_subprogram x env =
+  IMap.mem x env.global.subprograms |: TypingRule.IsSubprogram
+(* End *)

asllib/Typing.ml

@@ -430,11 +430,13 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
     |: TypingRule.DisjointSlicesToPositions
   (* End *)
 
+  (* Begin TypingRule.CheckDisjointSlices *)
   let check_disjoint_slices loc env slices =
     if List.length slices <= 1 then ok
     else fun () ->
       let _ = disjoint_slices_to_diet loc env slices in
-      ()
+      () |: TypingRule.CheckDisjointSlices
+  (* End *)
 
   exception NoSingleField
 
@@ -974,13 +976,13 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
 
   (* Begin CheckVarNotInEnv *)
   let check_var_not_in_env loc env x () =
-    if is_undefined x env then ()
+    if is_undefined x env then () |: TypingRule.CheckVarNotInEnv
     else fatal_from loc (Error.AlreadyDeclaredIdentifier x)
   (* End *)
 
   (* Begin CheckVarNotInGEnv *)
   let check_var_not_in_genv loc genv x () =
-    if is_global_undefined x genv then ()
+    if is_global_undefined x genv then () |: TypingRule.CheckVarNotInGEnv
     else fatal_from loc (Error.AlreadyDeclaredIdentifier x)
   (* End *)
 

asllib/doc/ASLmacros.tex

@@ -1087,7 +1087,10 @@
 \newcommand\withemptylocal[0]{\hyperlink{def-withemptylocal}{\textfunc{with\_empty\_local}}}
 \newcommand\addnewfunc[0]{\hyperlink{def-addnewfunc}{\textfunc{add\_new\_func}}}
 \newcommand\addsubprogram[0]{\hyperlink{def-addsubprogram}{\textfunc{add\_subprogram}}}
+\newcommand\isglobalundefined[0]{\hyperlink{def-isglobalundefined}{\textfunc{is\_global\_undefined}}}
+\newcommand\islocalundefined[0]{\hyperlink{def-islocalundefined}{\textfunc{is\_local\_undefined}}}
 \newcommand\isundefined[0]{\hyperlink{def-isundefined}{\textfunc{is\_undefined}}}
+\newcommand\issubprogram[0]{\hyperlink{def-issubprogram}{\textfunc{is\_subprogram}}}
 \newcommand\lookupimmutableexpr[0]{\hyperlink{def-lookupimmutableexpr}{\textfunc{lookup\_immutable\_expr}}}
 \newcommand\addglobalimmutableexpr[0]{\hyperlink{def-addglobalimmutableexpr}{\textfunc{add\_global\_immutable\_expr}}}
 \newcommand\addlocalimmutableexpr[0]{\hyperlink{def-addlocalimmutableexpr}{\textfunc{add\_local\_immutable\_expr}}}
@@ -1336,7 +1339,7 @@
 \newcommand\checkpositionsinwidth[0]{\hyperlink{def-checkpositionsinwidth}{\textfunc{check\_positions\_in\_width}}}
 \newcommand\shouldslicesreducetocall[0]{\tododefine{should\_slices\_reduce\_to\_call}}
 \newcommand\shouldreducetocall[0]{\tododefine{should\_reduce\_to\_call}}
-\newcommand\checkdisjointslices[0]{\tododefine{check\_disjoint\_slices}}
+\newcommand\checkdisjointslices[0]{\hyperlink{def-checkdisjointslices}{\textfunc{check\_disjoint\_slices}}}
 \newcommand\annotatetype[1]{\hyperlink{def-annotatetype}{\textfunc{annotate\_type}}(#1)}
 \newcommand\annotateconstraint[0]{\hyperlink{def-annotateconstraint}{\textfunc{annotate\_constraint}}}
 \newcommand\getvariableenum[0]{\hyperlink{def-getvariableenum}{\textfunc{get\_variable\_enum}}}
@@ -1363,7 +1366,6 @@
 \newcommand\annotatelocaldeclitemuninit[0]{\hyperlink{def-annotatelocaldeclitemuninit}{\textfunc{annotate\_local\_decl\_item\_uninit}}}
 \newcommand\checkvarnotinenv[1]{\hyperlink{def-checkvarnotinenv}{\textfunc{check\_var\_not\_in\_env}}(#1)}
 \newcommand\checkvarnotingenv[1]{\hyperlink{def-checkvarnotingenv}{\textfunc{check\_var\_not\_in\_genv}}(#1)}
-\newcommand\varinenv[1]{\hyperlink{def-varinenv}{\textfunc{var\_in\_env}}(#1)}
 \newcommand\annotatesubprogram[1]{\hyperlink{def-annotatesubprogram}{\textfunc{annotate\_subprogram}}(#1)}
 \newcommand\annotatedecl[1]{\hyperlink{def-annotatedecl}{\textfunc{annotate\_decl}}(#1)}
 \newcommand\declaredecl[1]{\hyperlink{def-declaredecl}{\textfunc{declare\_decl}}(#1)}
@@ -1423,6 +1425,7 @@
 %% Type Error Codes
 \newcommand\TypeErrorCode[1]{\texttt{TE\_#1}}
 \newcommand\UndefinedIdentifier[0]{\hyperlink{def-undefinedidentifier}{\TypeErrorCode{UI}}}
+\newcommand\IdentifierAlreadyDeclared[0]{\hyperlink{def-identifieralreadydeclared}{\TypeErrorCode{IAD}}}
 \newcommand\LengthsMismatch[0]{\hyperlink{def-lengthsmismatch}{\TypeErrorCode{LMM}}}
 \newcommand\SetterWithoutGetter[0]{\hyperlink{def-setterwithoutgetter}{\TypeErrorCode{SWG}}}
 \newcommand\ExpectedBitvectorType[0]{\hyperlink{def-expectedbitvectortype}{\TypeErrorCode{EBT}}}
@@ -1451,6 +1454,7 @@
 \newcommand\BitfieldSlicesOverlap[0]{\hyperlink{def-bso}{\TypeErrorCode{BSO}}}
 \newcommand\BitfieldSliceReversed[0]{\hyperlink{def-bsr}{\TypeErrorCode{BSR}}}
 \newcommand\IntConstantExpected[0]{\hyperlink{def-icc}{\TypeErrorCode{ICC}}}
+\newcommand\EmptySlice[0]{\hyperlink{def-es}{\TypeErrorCode{ES}}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Semantics/Typing Shared macros

asllib/doc/AssignableExpressions.tex

@@ -562,6 +562,7 @@ \subsubsection{Prose}
   \item checking whether $\vte$ \typesatisfies\ $\vt$ yields $\True$\ProseOrTypeError;
   \item annotating $\slices$ in $\tenv$ yields $\slicestwo$\ProseOrTypeError;
   \item checking that the slices $\slicestwo$ are all disjoint yields $\True$\ProseOrTypeError;
+  \item checking that $\slices$ is not empty yields $\True$\ProseTerminateAs{\EmptySlice};
   \item $\newle$ is the slicing of $\vletwo$ by $\slicestwo$, that is, $\LESlice(\vletwo, \slicestwo)$.
 \end{itemize}
 \subsubsection{Formally}
@@ -577,13 +578,40 @@ \subsubsection{Formally}
   \checktypesat(\tenv, \vte, \vt) \typearrow \True \OrTypeError\\\\
   \annotateslices(\tenv, \slices) \typearrow \slicestwo \OrTypeError\\\\
   \checkdisjointslices(\tenv, \slicestwo) \typearrow \True \OrTypeError\\\\
+  \checktrans{\slices \neq \emptylist}{\EmptySlice} \typearrow \True \OrTypeError\\\\
   \newle \eqdef \LESlice(\vletwo, \slicestwo)
 }{
   \annotatelexpr{\tenv, \overname{\LESlice(\vleone, \slices)}{\vle}, \vte} \typearrow \newle
 }
 \end{mathpar}
 \CodeSubsection{\LESliceBegin}{\LESliceEnd}{../Typing.ml}
 
+\subsubsection{TypingRule.CheckDisjointSlices\label{sec:}TypingRule.CheckDisjointSlices}
+\hypertarget{def-checkdisjointslices}{}
+The function
+\[
+\checkdisjointslices(\overname{\staticenvs}{\tenv} \aslsep \overname{\slice^*}{\slices})
+\aslto \True \cup \overname{\TTypeError}{\TypeErrorConfig}
+\]
+tests whether the list of slices $\slices$ do not overlap in $\tenv$, yielding $\True$.
+\ProseOtherwiseTypeError
+
+\subsubsection{Prose}
+All of the following apply:
+\begin{itemize}
+  \item applying $\disjointslicestopositions$ to $\slices$ in $\tenv$ yields a set of positions\ProseOrTypeError.
+  \item the result is $\True$.
+\end{itemize}
+\subsubsection{Formally}
+\begin{mathpar}
+\inferrule{
+  \disjointslicestopositions(\tenv, \slices) \typearrow \positions \OrTypeError
+}{
+  \checkdisjointslices(\tenv, \slices) \typearrow \True
+}
+\end{mathpar}
+\CodeSubsection{\CheckDisjointSlicesBegin}{\CheckDisjointSlicesEnd}{../Typing.ml}
+
 \subsection{Semantics}
 \subsubsection{SemanticsRule.LESlice\label{sec:SemanticsRule.LESlice}}
 \subsubsection{Example}

asllib/doc/ErrorCodes.tex

@@ -36,6 +36,13 @@ \section{Static Error Codes}
 An identifier that is missing a definition of the appropriate kind.
 See TypingRule.SubprogramForName (\secref{TypingRule.SubprogramForName}) for an example.
 
+\hypertarget{def-identifieralreadydeclared}{}
+\item[$\IdentifierAlreadyDeclared$]
+This error indicates an attempt to declare an identifier where it has already been declared.
+The context makes it clear whether this error relates to the local static environment or to the
+entire static environment.
+See \nameref{sec:TypingRule.CheckVarNotInEnv} and \nameref{sec:TypingRule.CheckVarNotInGEnv}.
+
 \hypertarget{def-lengthsmismatch}{}
 \item[$\LengthsMismatch$]
 This error indicates that two lists that are expected to have the same length have different lengths.
@@ -174,6 +181,13 @@ \section{Static Error Codes}
 or could not be statically evaluated to a literal.
 This is checked by \nameref{sec:TypingRule.BitfieldSliceToPositions}.
 
+\hypertarget{def-es}{}
+\item[$\EmptySlice$]
+This error indicates that an expression is either a slice with an empty list of slice sub-expressions
+or an incorrect way of invoking a getter or a setter with the wrong list of arguments, a missing
+list of arguments, or a list of arguments where the getter or setter are declared with no arguments.
+This is checked by \nameref{sec:TypingRule.ESlice}.
+
 \end{description}
 
 \section{Dynamic Error Codes}

asllib/doc/Expressions.tex

@@ -1072,6 +1072,7 @@ \subsubsection{Prose}
   \item annotating the expression $\vep$ in $\tenv$ yields $(\tep,\vepp)$\ProseOrTypeError;
   \item obtaining the \structure\ of $\tep$ in $\tenv$ yields $\structtep$\ProseOrTypeError;
   \item $\structtep$ is either a bitvector or an integer;
+  \item checking that $\slices$ is not empty yields $\True$\ProseTerminateAs{\EmptySlice};
   \item obtaining the width of $\slices$ in $\tenv$ via $\sliceswidth$ yields $\vw$\ProseOrTypeError;
   \item $\slicesp$ is the result of annotating $\slices$ in $\tenv$;
   \item $\vt$ is the bitvector type of width $\vw$, that is, $\TBits(\vw, \emptylist)$;
@@ -1085,6 +1086,7 @@ \subsubsection{Formally}
   \annotateexpr{\tenv, \vep} \typearrow (\tep, \vepp) \OrTypeError\\\\
   \tstruct(\tenv, \tep) \typearrow \structtep \OrTypeError\\\\
   \astlabel(\structtep) \in \{\TInt, \TBits\}\\
+  \checktrans{\slices \neq \emptylist}{\EmptySlice} \typearrow \True \OrTypeError\\\\
   \sliceswidth(\tenv, \slices) \typearrow \vw \OrTypeError\\\\
   \annotateslices(\tenv, \slices) \typearrow \slicesp \OrTypeError
 }{
@@ -1819,7 +1821,7 @@ \subsubsection{Prose}
   \item obtaining the \structure\ of $\tty'$ in $\tenv$ yields $\vtystruct$\ProseOrTypeError;
   \item applying $\checkatc$ to $\vtstruct$ and $\vtystruct$ in $\tenv$ to check whether the type assertion
         will always fail yields $\True$\ProseOrTypeError;
-  \item checking whether $\vt$ \subtypesatisfies\ $\ttyp$ in $\tenv$ yields $\vb$\ProseOrTypeError;
+  \item checking whether $\vtstruct$ \subtypesatisfies\ $\vtystruct$ in $\tenv$ yields $\vb$\ProseOrTypeError;
   \item $\newe$ is $\vepp$ if $\vb$ is $\True$ and $\EATC(\ttyp, \vepp)$ otherwise;
   \item $\vt$ is $\ttyp$.
 \end{itemize}
@@ -1831,7 +1833,7 @@ \subsubsection{Formally}
   \annotatetype{\tenv, \tty} \typearrow \ttyp \OrTypeError\\\\
   \tstruct(\tenv, \ttyp) \typearrow \vtystruct \OrTypeError\\\\
   \checkatc(\tenv, \vtstruct, \vtystruct) \typearrow \True \OrTypeError\\\\
-  \subtypesat(\tenv, \vt, \ttyp) \typearrow \vb \OrTypeError\\\\
+  \subtypesat(\tenv, \vtstruct, \vtystruct) \typearrow \vb \OrTypeError\\\\
   \newe \eqdef \choice{\vb}{\vepp}{\EATC(\ttyp, \vepp)}
 }{
   \annotateexpr{\tenv, \overname{\EATC(\vep, \tty)}{\ve}} \typearrow (\overname{\ttyp}{\vt}, \newe)

asllib/doc/GlobalStorageDeclarations.tex

@@ -326,48 +326,7 @@ \subsubsection{Formally}
   \addglobalstorage(\genv, \name, \keyword, \declaredt) \typearrow \newgenv
 }
 \end{mathpar}
-\CodeSubsection{\CheckVarNotInGEnvBegin}{\CheckVarNotInGEnvEnd}{../Interpreter.ml}
-
-\subsubsection{TypingRule.CheckVarNotInGEnv}
-\hypertarget{def-checkvarnotingenv}{}
-The function
-\[
-  \checkvarnotingenv{\overname{\globalstaticenvs}{\genv} \aslsep \overname{\Strings}{\id}}
-  \aslto \{\True\} \cup \overname{\TTypeError}{\TypeErrorConfig}
-\]
-checks whether $\id$ is already declared in the global static environment $\genv$.
-If it is, the result is a type error, and otherwise the result is $\True$.
-
-\subsubsection{Prose}
-All of the following apply:
-\begin{itemize}
-  \item $\vb$ is $\True$ if and only if one of the following applies:
-  \begin{itemize}
-    \item $\id$ is declared as a global identifier in $\genv$ via the $\globalstoragetypes$ map;
-    \item $\id$ is declared as a subprogram in $\genv$ via the $\subprograms$ map;
-    \item $\id$ is declared as a type in $\genv$ via the $\declaredtypes$ map.
-  \end{itemize}
-
-  \item checking whether $\vb$ is $\False$ yields $\True$ or a type error indicating
-        that $\id$ has already been declared, thereby short-circuiting the rule.
-\end{itemize}
-
-\subsubsection{Formally}
-\begin{mathpar}
-\inferrule{
-{
-  \begin{array}{rl}
-  \vb \eqdef  & \genv.\globalstoragetypes(\id) \neq \bot \lor\\
-              & \genv.\subprograms(\id) \neq \bot\ \lor\\
-              & \genv.\declaredtypes(\id) \neq \bot
-  \end{array}
-}\\
-\checktrans{\neg\vb}{IdentifierAlreadyDeclared} \checktransarrow \True \OrTypeError
-}{
-  \checkvarnotingenv{\genv, \id} \typearrow \True
-}
-\end{mathpar}
-\CodeSubsection{\CheckVarNotInGEnvBegin}{\CheckVarNotInGEnvEnd}{../Interpreter.ml}
+\CodeSubsection{\AddGlobalStorageBegin}{\AddGlobalStorageEnd}{../Interpreter.ml}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Semantics\label{sec:GlobalStorageDeclarationsSemantics}}