Merge pull request #1142 from herd/asl-reference-synch-for-1140

[asl][reference] Synchronize reference for #1140

asllib/doc/ASLmacros.tex

@@ -1591,6 +1591,7 @@
 
 \newcommand\basevalueterm[0]{\hyperlink{def-basevalueterm}{base value}}
 \newcommand\controlflowsymbolterm[0]{\hyperlink{def-controlflowsymbolterm}{control flow state}}
+\newcommand\controlflowsymbolsterm[0]{\hyperlink{def-controlflowsymbolterm}{control flow states}}
 
 \newcommand\defusedependencyterm[0]{\hyperlink{def-builddependencies}{def-use dependency}}
 \newcommand\defusedependenciesterm[0]{\hyperlink{def-builddependencies}{def-use dependencies}}
@@ -1807,6 +1808,7 @@
 \newcommand\interrupt[0]{\hyperlink{def-interrupt}{\textsf{Interrupt}}}
 \newcommand\maynotinterrupt[0]{\hyperlink{def-maynotinterrupt}{\textsf{MayNotInterrupt}}}
 \newcommand\controlflowstate[0]{\hyperlink{def-controlflowstate}{\textsf{ControlFlow}}}
+\newcommand\controlflowleq[0]{\hyperlink{def-controlflowleq}{<_{\textsf{CF}}}}
 
 \newcommand\Prosetypecheckast[4]{\hyperlink{def-typecheckast}{type-checking} #1 in #2 yields the typed AST #3 and static environment #4}
 \newcommand\typecheckast[0]{\hyperlink{def-typecheckast}{\textfunc{type\_check\_ast}}}
@@ -2459,6 +2461,7 @@
 \newcommand\vdeclnew[0]{\texttt{decl\_new}}
 \newcommand\vdeclx[0]{\texttt{decl\_x}}
 \newcommand\vadecls[0]{\texttt{adecls}}
+\newcommand\vcf[0]{\texttt{cf}}
 \newcommand\vctrlflow[0]{\texttt{ctrl\_flow}}
 \newcommand\vctrlflowone[0]{\texttt{ctrl\_flow1}}
 \newcommand\vctrlflowtwo[0]{\texttt{ctrl\_flow2}}
@@ -2808,6 +2811,8 @@
 \newcommand\vrecurselimit[0]{\texttt{recurse\_limit}}
 \newcommand\vreone[0]{\texttt{re1}}
 \newcommand\vres[0]{\texttt{res}}
+\newcommand\vreszero[0]{\texttt{res0}}
+\newcommand\vresone[0]{\texttt{res1}}
 \newcommand\vret[0]{\texttt{ret}}
 \newcommand\vreturntype[0]{\texttt{return\_type}}
 \newcommand\vs[0]{\texttt{s}}

asllib/doc/GlobalDeclarations.tex

@@ -267,10 +267,15 @@ \subsubsection{Formally}
 \TypingRuleDef{ControlFlowFromStmt}
 \hypertarget{def-controlflowsymbolterm}{}
 \hypertarget{def-controlflowstate}{}
-We define \controlflowsymbolterm\ as follows:
+We define \controlflowsymbolsterm\ as follows:
 \[
   \controlflowstate \eqdef \{\assertednotinterrupt, \interrupt, \maynotinterrupt\}
 \]
+\hypertarget{def-controlflowleq}{}
+\controlflowsymbolsterm\ are totally ordered via the relation $\controlflowleq$, defined as follows:
+\[
+  \assertednotinterrupt\ \controlflowleq \interrupt \controlflowleq \maynotinterrupt \enspace.
+\]
 
 \hypertarget{def-controlflowfromstmt}{}
 The helper function
@@ -343,8 +348,17 @@ \subsubsection{Prose}
 
   \item All of the following apply (\textsc{s\_try}):
   \begin{itemize}
-    \item $\vs$ is the \trystatementterm\ for the statement $\vbody$;
-    \item applying $\controlflowfromstmt$ to $\vbody$ yields $\vctrlflow$.
+    \item $\vs$ is the \trystatement{$\vbody$}{\\ $\catchers$}{$\votherwiseopt$};
+    \item applying $\controlflowfromstmt$ to $\vbody$ yields $\vreszero$;
+    \item \Proseeqdef{$\vresone$}{
+          the application of $\controlflowjoin$ to $\controlflowfromstmt(\vo)$
+          and $\vreszero$, if $\votherwiseopt = \langle\vo\rangle$,
+          and $\vreszero$, otherwise};
+    \item for each catcher in $\catchers$ associated with a statement $\vs$,
+          applying \\
+          $\controlflowfromstmt$ to $\vs$ yields $\vcf_\vs$;
+    \item \Proseeqdef{$\vctrlflow$}{the application of $\controlflowjoin$ to $\vresone$,
+          and $\vcf_\vs$, for each catcher in $\catchers$ associated with a statement $\vs$}.
   \end{itemize}
 \end{itemize}
 
@@ -385,7 +399,7 @@ \subsubsection{Formally}
 \inferrule[s\_cond]{
   \controlflowfromstmt(\vsone) \typearrow \vctrlflowone\\
   \controlflowfromstmt(\vstwo) \typearrow \vctrlflowtwo\\
-  \controlflowjoin(\vctrlflowone, \vctrlflowtwo) \typearrow \vctrlflow
+  \controlflowjoin(\{\vctrlflowone, \vctrlflowtwo\}) \typearrow \vctrlflow
 }{
   \controlflowfromstmt(\overname{\SCond(\Ignore, \vsone, \vstwo)}{\vs}) \typearrow \vctrlflow
 }
@@ -397,8 +411,9 @@ \subsubsection{Formally}
     a $\SWhile$ loop, and a $\SFor$ are like a conditional statement that either executes
     $\SPass$ (when the loop condition does not hold) or executes the body and then loops back.
   \item The control flow state for $\SPass$ is $\maynotinterrupt$.
-  \item The overall control flow state is then $\controlflowjoin(\maynotinterrupt, \Ignore)$,
-    which is always $\maynotinterrupt$.
+  \item The overall control flow state is then $\controlflowjoin(\{\maynotinterrupt, \Ignore\})$,
+    which is always $\maynotinterrupt$, since $\maynotinterrupt$ is the maximal element,
+    with respect to $\controlflowleq$.
 \end{itemize}
 
 \begin{mathpar}
@@ -431,11 +446,24 @@ \subsubsection{Formally}
 }
 \end{mathpar}
 
+The rule for \textsc{s\_try} conservatively approximates the results from all control flows
+passing through the statement by returning the maximal $\controlflowsymbolterm$,
+with respect to $\controlflowleq$,
+computed for each control flow path.
 \begin{mathpar}
 \inferrule[s\_try]{
-  \controlflowfromstmt(\vbody) \typearrow \vctrlflow
+  \controlflowfromstmt(\vbody) \typearrow \vreszero\\
+  {
+  \vresone \eqdef
+  \begin{cases}
+    \controlflowjoin(\{\controlflowfromstmt(\vo), \vreszero\}) & \text{if }\votherwiseopt = \langle\vo\rangle\\
+    \vreszero & \text{otherwise}
+  \end{cases}
+  }\\
+  (\Ignore,\Ignore,\vs)\in\catchers: \controlflowfromstmt(\vs) \typearrow \vcf_\vs\\
+  \vctrlflow \eqdef \controlflowjoin(\{(\Ignore,\Ignore,\vs)\in\catchers: \vcf_\vs\} \cup \{\vresone\})
 }{
-  \controlflowfromstmt(\overname{\STry(\vbody, \Ignore, \Ignore)}{\vs}) \typearrow \vctrlflow
+  \controlflowfromstmt(\overname{\STry(\vbody, \catchers, \votherwiseopt)}{\vs}) \typearrow \vctrlflow
 }
 \end{mathpar}
 
@@ -465,12 +493,21 @@ \subsubsection{Formally}
 \TypingRuleDef{ControlFlowJoin}
 \hypertarget{def-controlflowjoin}{}
 The helper function
+The helper function
 \[
-\controlflowjoin(\overname{\controlflowstate}{\vtone} \aslsep
-                \overname{\controlflowstate}{\vttwo})
+\controlflowjoin(\overname{\pow{\controlflowstate}}{\vs})
 \aslto \overname{\controlflowstate}{\vctrlflow}
 \]
-returns in $\vctrlflow$ the maximal element of $\vtone$ and $\vttwo$ in the following ordering:
-\[
-  \assertednotinterrupt\ \sqsubset \interrupt \sqsubset \maynotinterrupt \enspace.
-\]
+returns the maximal element in the set of \controlflowsymbolsterm\ $\vs$,
+with respect to $\controlflowleq$ in $\vctrlflow$.
+
+\ProseParagraph
+\Proseeqdef{$\vctrlflow$}{the maximal element in the set of \controlflowsymbolsterm\ $\vs$,
+with respect to $\controlflowleq$}.
+
+\FormallyParagraph
+\begin{mathpar}
+\inferrule{}{
+  \controlflowjoin(\vs) \typearrow \overname{\max_{\controlflowleq}(\vs)}{\vctrlflow}
+}
+\end{mathpar}