From 17da27d3a2d7fecf023f383f922887c7de91a105 Mon Sep 17 00:00:00 2001 From: Roman-Manevich Date: Sun, 10 Mar 2024 16:33:15 +0000 Subject: [PATCH] [asl][semantics] Rules for evaluating function calls. Added a (missing) rule for `eval_call`, which in turn calls `eval_func`. Fixes to `eval_expr_list` and 'eval_expr_list_m'. Fixes to the list of output configurations. --- asllib/ASTUtils.ml | 2 +- asllib/Interpreter.ml | 25 +- asllib/Native.ml | 14 +- asllib/bitvector.ml | 2 +- asllib/doc/ASL.bib | 2 +- asllib/doc/ASLNotations.tex | 37 +- asllib/doc/ASLSemanticsReference.tex | 2652 +++++++++++++++++++------- asllib/doc/ASLTypingReference.tex | 1 - asllib/doc/ASLmacros.tex | 16 +- asllib/instrumentation.ml | 3 + 10 files changed, 2021 insertions(+), 733 deletions(-) diff --git a/asllib/ASTUtils.ml b/asllib/ASTUtils.ml index dbb57ed1cf..66e5daa8ac 100644 --- a/asllib/ASTUtils.ml +++ b/asllib/ASTUtils.ml @@ -156,7 +156,7 @@ let inv_mask = let slices_to_positions as_int = let one_slice (start, length) = let start = as_int start and length = as_int length in - (* Reversed interval *) + (* Reversed interval - recall that bitvectors are reversed. *) List.init length (( - ) (start + length - 1)) in fun positions -> List.map one_slice positions |> List.flatten diff --git a/asllib/Interpreter.ml b/asllib/Interpreter.ml index ac79ca3cef..7bbd486e11 100644 --- a/asllib/Interpreter.ml +++ b/asllib/Interpreter.ml @@ -307,9 +307,9 @@ module Make (B : Backend.S) (C : Config) = struct let lexpr_is_var le = match le.desc with LE_Var _ | LE_Discard -> true | _ -> false - let declare_local_identifier env x v = - let* () = B.on_write_identifier x (IEnv.get_scope env) v in - IEnv.declare_local x v env |> return + let declare_local_identifier env name v = + let* () = B.on_write_identifier name (IEnv.get_scope env) v in + IEnv.declare_local name v env |> return let declare_local_identifier_m env x m = m >>= declare_local_identifier env x @@ -693,7 +693,8 @@ module Make (B : Backend.S) (C : Config) = struct (* Evaluation of Expression Lists *) (* ------------------------------ *) - and eval_expr_list_m env es = fold_parm_list eval_expr env es + and eval_expr_list_m env es = + fold_parm_list eval_expr env es and eval_expr_list env es = fold_par_list eval_expr env es (* Evaluation of Slices *) @@ -1150,15 +1151,17 @@ module Make (B : Backend.S) (C : Config) = struct (** [eval_call pos name env args named_args] evaluate the call to function [name] with arguments [args] and parameters [named_args] *) + (* Begin Call *) and eval_call pos name env args named_args = - let names, nargs = List.split named_args in + let names, nargs1 = List.split named_args in let*^ vargs, env1 = eval_expr_list_m env args in - let*^ nargs, env2 = eval_expr_list_m env1 nargs in - let* vargs = vargs and* nargs = nargs in - let nargs = List.combine names nargs in - let**| ms, global = eval_func env2.global name pos vargs nargs in - let ms = List.map read_value_from ms and env' = { env2 with global } in - return_normal (ms, env') + let*^ nargs2 , env2 = eval_expr_list_m env1 nargs1 in + let* vargs = vargs and* nargs2 = nargs2 in + let nargs3 = List.combine names nargs2 in + let**| ms, global = eval_func env2.global name pos vargs nargs3 in + let ms2 = List.map read_value_from ms and env' = { env2 with global } in + return_normal (ms2, env') |: SemanticsRule.Call + (* End *) (* Evaluation of Functions *) (* ----------------------- *) diff --git a/asllib/Native.ml b/asllib/Native.ml index 6198ad48b3..4fbeab4e45 100644 --- a/asllib/Native.ml +++ b/asllib/Native.ml @@ -188,8 +188,8 @@ module NativeBackend = struct let bitvector_to_value bv = L_BitVector bv |> nv_literal |> return let int_max x y = if x >= y then x else y - let read_from_bitvector positions bv = - let positions = slices_to_positions as_int positions in + let read_from_bitvector slices bv = + let positions = slices_to_positions as_int slices in let max_pos = List.fold_left int_max 0 positions in let () = List.iter @@ -220,11 +220,11 @@ module NativeBackend = struct let res = Bitvector.extract_slice bv positions in bitvector_to_value res - let write_to_bitvector positions bits bv = - let bv = as_bitvector bv - and bits = as_bitvector bits - and positions = slices_to_positions as_int positions in - Bitvector.write_slice bv bits positions |> bitvector_to_value + let write_to_bitvector slices src dst = + let dst = as_bitvector dst + and src = as_bitvector src + and positions = slices_to_positions as_int slices in + Bitvector.write_slice dst src positions |> bitvector_to_value let concat_bitvectors bvs = let bvs = List.map as_bitvector bvs in diff --git a/asllib/bitvector.ml b/asllib/bitvector.ml index 2e03844e8b..e7ab788500 100644 --- a/asllib/bitvector.ml +++ b/asllib/bitvector.ml @@ -429,7 +429,7 @@ let write_slice (length_dst, data_dst) (length_src, data_src) positions = let min x y = if x <= y then x else y in let length_src = min (List.length positions) length_src in let result = Bytes.of_string data_dst in - (* Same effect than [List.rev positions], as we build those from the end. *) + (* Same effect as [List.rev positions], since we build those from the end. *) let copy_bit_here i pos = copy_bit result data_src (length_src - 1 - i) pos in let () = List.iteri copy_bit_here positions in remask (length_dst, Bytes.unsafe_to_string result) diff --git a/asllib/doc/ASL.bib b/asllib/doc/ASL.bib index fa62a1f3c6..477ac20cab 100644 --- a/asllib/doc/ASL.bib +++ b/asllib/doc/ASL.bib @@ -23,7 +23,7 @@ @article{AlglaveDGHM21 Antoine Hacquard and Luc Maranget}, title = {Armed Cats: Formal Concurrency Modelling at Arm}, - journal = {{ACM} Trans. Program. Lang. Syst.}, + journal = {{ACM} Transactions on Programming Languages and Systems}, volume = {43}, number = {2}, pages = {8:1--8:54}, diff --git a/asllib/doc/ASLNotations.tex b/asllib/doc/ASLNotations.tex index 6593198b37..693340f08d 100644 --- a/asllib/doc/ASLNotations.tex +++ b/asllib/doc/ASLNotations.tex @@ -1,5 +1,5 @@ -\paragraph{Functions and Products.} -The notation $A \partialto B$ denotes a partial function from a subset of $A$, denoted $\dom(A)$, to $B$. +\paragraph{Functions and Products} +The notation $A \partialto B$ denotes a partial function from a \underline{subset} of $A$, denoted $\dom(A)$, to $B$. For a partial function $f$, we write $f(x) = \bot$ to denote that $x$ is not in the domain of $f$. % The notation $f[x \mapsto v]$ is the function $f$ modified so that $x$ is bound @@ -8,26 +8,41 @@ v & \text{if } z = x \enspace . \end{cases}$ % +The notation $\{i=1..k: a_i\mapsto b_i\}$ stands for the function formed from the corresponding input-output pairs: +$\emptyfunc[a_1\mapsto b_1]\ldots[a_k\mapsto b_k]$. + The notation $A \times B$ stands for the Cartesian product of sets $A$ and $B$: $A \times B \triangleq \{(a,b) \;|\; a \in A, b \in B\}$. -\paragraph{Sequences and Lists.} -We use the notation $a..b$ as a shorthand for the sequence $a,\ldots,b$ and $x_{a..b}$ as a shorthand for the sequence $x_a,\ldots,x_b$. +\paragraph{Sequences and Lists} +We use the notation $a..b$ as a shorthand for the sequence $a\ldots b$ and $x_{a..b}$ as a shorthand for the sequence $x_a \ldots x_b$. % -In particular, we use the notation $p(x_{1..k})$ to denote that a predicate $p$ holds for the list of arguments $x_{1..k}$. +We use the notation $p(x_{1..k})$ to denote that a predicate $p$ holds for the list of arguments $x_1,\ldots,x_k$. % We write $i=1..k: V(i)$, where $V(i)$ is a mathematical expression parameterized by $i$, to denote the sequence of expressions $V(1) \ldots V(k)$. -The expression $[i=1..k: V(i)]$, denotes the list $[V(1),\ldots,V(k)]$. +The notation $[i=1..k: V(i)]$ stands the list $[V(1),\ldots,V(k)]$. +The notation $\seq{v\in r: f(v)}$, where $r$ is a sequence, stands for $\epsilon$ when $r=\epsilon$ and +$f(v_1) \ldots f(v_k)$ when $r=v_{1..k}$ and $f$ is a mathematical expression over $v$. % We use `+' to denote concatenation of lists, defined as follows: $\emptylist + L = L$, $L + \emptylist = L$, and $[i=1..k: l_i] + [j=1..n: m_j] = [l_{1..k}, m_{1..n}]$. -We write $T^*$ for a sequence of zero or more values from $T$ and $T^+$ for a sequences of one or more values from $T$. +We write $\epsilon$ for an empty sequence, +$a_{1..k} \cdot b_{1..n} \triangleq a_1\ldots a_k b_1 \ldots b_n$ for the concatenation of two sequences, +$T^*$ for a sequence of zero or more values from $T$, and $T^+$ for a sequences of one or more values from $T$. -\paragraph{Rules.} +\paragraph{Rules} The following notation states that when the \emph{premises} $P_{1..k}$ hold then the \emph{verdict} $C$ holds as well: \begin{mathpar} \inferrule{P_1 \and \ldots \and P_k}{C} \end{mathpar} -% -We write `$\Ignore$' for a fresh universally quantified variable whose name is irrelevant for understanding the rule, -and can thus be omitted. + +To keep rules succinct, we will write `$\Ignore$' for a fresh universally quantified variable whose name is +irrelevant for understanding the rule, and can thus be omitted. + +We will often want to deconstruct compound values in order to refer to their internal values. +To achieve that, we will write $v \eqname \textit{deconstructed}(v)$ where the expression on the right +exposes the internal structure of $v$, allowing us to alias its internal components. +For example, suppose we know that $v$ is a pair of values. +Then, $v \eqname (a, b)$ allows us to alias $a$ and $b$. +Similarly, if $v$ is a non-empty list, then $v \eqname [h] + t$ deconstructs the list into the +head of the list $h$ and its tail $t$. diff --git a/asllib/doc/ASLSemanticsReference.tex b/asllib/doc/ASLSemanticsReference.tex index 2de92a1912..954ef9c503 100644 --- a/asllib/doc/ASLSemanticsReference.tex +++ b/asllib/doc/ASLSemanticsReference.tex @@ -5,8 +5,16 @@ \newcommand\semantic[1]{\llbracket #1 \rrbracket} \newcommand\tododefine[1]{\texttt{#1}} +\usepackage{relsize} +%\newcommand\eqname[0]{=} +\newcommand\eqname[0]{\stackrel{\mathsmaller{\mathsf{name}}}{=}} +%\newcommand\overname[2]{#1} +\newcommand\overname[2]{\overbracket{#1}^{#2}} + +\newcommand\eq[0]{\textsf{eq}} +\newcommand\emptyfunc[0]{{\emptyset}_\lambda} \newcommand\xgraph[0]{\textsf{g}} -\newcommand\emptygraph[0]{\xgraph_{\emptyset}} +\newcommand\emptygraph[0]{{\emptyset}_\xgraph} \newcommand\Nodes[0]{\mathcal{N}} \newcommand\Read[0]{\text{Read}} \newcommand\Write[0]{\text{Write}} @@ -15,13 +23,27 @@ \newcommand\WriteEffect[0]{\textsf{WriteEffect}} \newcommand\ReadEffect[0]{\textsf{ReadEffect}} +\newcommand\emptyenv[0]{\underline{e}} \newcommand\tenv[0]{\textsf{tenv}} \newcommand\denv[0]{\textsf{denv}} +\newcommand\denvtwo[0]{\textsf{denv2}} \newcommand\vals[0]{\mathcal{V}} \newcommand\ordered[3]{{#1}\xrightarrow{#2}{#3}} \newcommand\nvliteral[1]{\texttt{NV\_Literal}(#1)} \newcommand\nvvector[1]{\texttt{NV\_Vector}(#1)} \newcommand\nvrecord[1]{\texttt{NV\_Record}(#1)} +\newcommand\nvint[0]{\texttt{Int}} +\newcommand\nvbool[0]{\texttt{Bool}} +\newcommand\nvreal[0]{\texttt{Real}} +\newcommand\nvstring[0]{\texttt{String}} +\newcommand\nvbitvector[0]{\texttt{Bitvector}} +\newcommand\tint[0]{\mathcal{Z}} +\newcommand\tbool[0]{\mathcal{B}} +\newcommand\treal[0]{\mathcal{R}} +\newcommand\tstring[0]{\mathcal{S}\mathcal{T}\mathcal{R}} +\newcommand\tbitvector[0]{\mathcal{B}\mathcal{V}} +\newcommand\tvector[0]{\mathcal{V}\mathcal{E}\mathcal{C}} +\newcommand\trecord[0]{\mathcal{R}\mathcal{E}\mathcal{C}} \newcommand\configmode[1]{\texttt{mode}({#1})} \newcommand\graphof[1]{\texttt{graph}({#1})} @@ -29,13 +51,21 @@ \newcommand\environof[1]{\texttt{environ}({#1})} \newcommand\withenviron[2]{{#1}(\texttt{environ}\mapsto{#2})} -\newcommand\evalarrow[0]{\rightsquigarrow} +\newcommand\evalarrow[0]{\stackrel{\mathsf{asl}}{\rightsquigarrow}} +\newcommand\aslrel[0]{\bigtimes} +\newcommand\aslsep[0]{\mathbf{,}} +\newcommand\evalprimitivearrow[0]{\stackrel{\mathsf{primitive}}{\rightsquigarrow}} \newcommand\sslash[0]{\mathbin{/\mkern-6mu/}} \newcommand\rightdownarrow[0]{\rotatebox[origin=c]{270}{$\Rsh$}} \newcommand\terminateas[0]{\;\sslash\;} -\newcommand\ExprThrowsConfig[0]{\texttt{\#T}} +\newcommand\ThrowingConfig[0]{\texttt{\#T}} \newcommand\ErrorConfig[0]{\texttt{\#E}} -\newcommand\OrAbnormal[0]{\terminateas \ExprThrowsConfig, \ErrorConfig} +\newcommand\OrAbnormal[0]{\terminateas \ThrowingConfig, \ErrorConfig} +\newcommand\TError[0]{\textsf{TError}} +\newcommand\TThrowing[0]{\textsf{TThrowing}} +\newcommand\TContinuing[0]{\textsf{TContinuing}} +\newcommand\TReturning[0]{\textsf{TReturning}} +\newcommand\TOutConfig[0]{\textsf{TOutConfig}} \newcommand\evalexpr[1]{\texttt{eval\_expr}(#1)} \newcommand\evalexprsef[1]{\texttt{eval\_expr\_sef}(#1)} @@ -52,13 +82,25 @@ \newcommand\evalfor[1]{\texttt{eval\_for}(#1)} \newcommand\evalcatchers[1]{\texttt{eval\_catchers}(#1)} \newcommand\evalfunc[1]{\texttt{eval\_func}(#1)} -\newcommand\evalconstraint[1]{\texttt{eval\_constraint}(#1)} \newcommand\evalcall[1]{\texttt{eval\_call}(#1)} +\newcommand\evalprimitive[1]{\texttt{eval\_primitive}(#1)} \newcommand\evalmultiassignment[1]{\texttt{multi\_assign}(#1)} \newcommand\rethrowimplicit[0]{\texttt{rethrow\_implicit}} +\newcommand\assignargs[0]{\texttt{assign\_args}} +\newcommand\assignnamedargs[0]{\texttt{assign\_named\_args}} +\newcommand\matchfuncres[0]{\texttt{match\_func\_res}} +\newcommand\emptytenv[0]{\emptyset_{\tenv}} +\newcommand\parsedspec[0]{\texttt{parsed\_spec}} +\newcommand\parsedstd[0]{\texttt{parsed\_std}} +\newcommand\parsedast[0]{\texttt{parsed\_ast}} +\newcommand\typedspec[0]{\texttt{typed\_spec}} +\newcommand\buildgenv[0]{\texttt{build\_genv}} +\newcommand\topologicaldecls[0]{\texttt{topological\_decls}} +\newcommand\evalglobals[0]{\texttt{eval\_globals}} +\newcommand\evalspec[1]{\texttt{eval\_spec}(#1)} +\newcommand\lexprisvar[0]{\texttt{lexpr\_is\_var}} \newcommand\findfunc[0]{\texttt{find\_func}} -%\newcommand\baseval[0]{\textsf{base\_val}} \newcommand\unknownval[0]{\texttt{unknown\_val}} \newcommand\typesatisfies[0]{\texttt{type\_satisfies}} @@ -86,15 +128,20 @@ \newcommand\vgp[0]{\texttt{g'}} \newcommand\vvp[0]{\texttt{v'}} \newcommand\vep[0]{\texttt{e'}} +\newcommand\vl[0]{\texttt{l}} \newcommand\vm[0]{\texttt{m}} +\newcommand\vn[0]{\texttt{n}} \newcommand\vp[0]{\texttt{p}} \newcommand\vv[0]{\texttt{v}} \newcommand\vx[0]{\texttt{x}} \newcommand\vs[0]{\texttt{s}} \newcommand\vt[0]{\texttt{t}} +\newcommand\vu[0]{\texttt{u}} +\newcommand\vw[0]{\texttt{w}} \newcommand\vvsg[0]{\texttt{vsg}} \newcommand\vvs[0]{\texttt{vs}} \newcommand\vms[0]{\texttt{ms}} +\newcommand\vmstwo[0]{\texttt{ms2}} \newcommand\vle[0]{\texttt{le}} \newcommand\vles[0]{\texttt{les}} \newcommand\vre[0]{\texttt{re}} @@ -117,11 +164,20 @@ \newcommand\vbv[0]{\texttt{v\_bv}} \newcommand\mpositions[0]{\texttt{m\_positions}} \newcommand\slices[0]{\texttt{slices}} +\newcommand\indices[0]{\texttt{indices}} \newcommand\positions[0]{\texttt{positions}} \newcommand\name[0]{\texttt{name}} \newcommand\args[0]{\texttt{args}} \newcommand\actualargs[0]{\texttt{actual\_args}} +\newcommand\argdecls[0]{\texttt{arg\_decls}} \newcommand\namedargs[0]{\texttt{named\_args}} +\newcommand\nargs[0]{\texttt{nargs}} +\newcommand\nargsm[0]{\texttt{nargs\_m}} +\newcommand\nargsone[0]{\texttt{nargs1}} +\newcommand\nargstwo[0]{\texttt{nargs2}} +\newcommand\nargsthree[0]{\texttt{nargs3}} +\newcommand\vargs[0]{\texttt{vargs}} +\newcommand\vargsm[0]{\texttt{vargs\_m}} \newcommand\params[0]{\texttt{params}} \newcommand\earray[0]{\texttt{e\_array}} \newcommand\eindex[0]{\texttt{e\_index}} @@ -143,11 +199,13 @@ \newcommand\rearray[0]{\texttt{re\_array}} \newcommand\rvarray[0]{\texttt{rv\_array}} \newcommand\rmarray[0]{\texttt{rm\_array}} +\newcommand\record[0]{\texttt{record}} \newcommand\rerecord[0]{\texttt{re\_record}} \newcommand\rmrecord[0]{\texttt{rm\_record}} \newcommand\rvrecord[0]{\texttt{rv\_record}} \newcommand\vlelist[0]{\texttt{le\_list}} \newcommand\vmlist[0]{\texttt{vm\_list}} +\newcommand\nmonads[0]{\texttt{nmonads}} \newcommand\start[0]{\texttt{start}} \newcommand\mstart[0]{\texttt{m\_start}} \newcommand\vstart[0]{\texttt{v\_start}} @@ -174,7 +232,8 @@ \newcommand\wid[0]{\texttt{wid}} \newcommand\es[0]{\texttt{es}} \newcommand\ms[0]{\texttt{ms}} -\newcommand\body[0]{\texttt{body}} +\newcommand\body[0]{\text{body}} +\newcommand\vbody[0]{\texttt{body}} \newcommand\dir[0]{\texttt{dir}} \newcommand\catchers[0]{\texttt{catchers}} \newcommand\otherwiseopt[0]{\texttt{otherwise\_opt}} @@ -197,6 +256,24 @@ \newcommand\vbtwo[0]{\texttt{b2}} \newcommand\vps[0]{\texttt{ps}} \newcommand\vbs[0]{\texttt{bs}} +\newcommand\xs[0]{\texttt{xs}} +\newcommand\retenv[0]{\texttt{ret\_env}} +\newcommand\vglobal[0]{\texttt{global}} +\newcommand\rid[0]{\texttt{rid}} +\newcommand\genv[0]{\texttt{genv}} +\newcommand\envm[0]{\texttt{envm}} +\newcommand\vacc[0]{\texttt{acc}} +\newcommand\vvsm[0]{\texttt{vsm}} +\newcommand\vd[0]{\texttt{d}} +\newcommand\vdecls[0]{\texttt{decls}} +\newcommand\bv[0]{\texttt{bv}} +\newcommand\src[0]{\texttt{src}} +\newcommand\dst[0]{\texttt{dst}} +\newcommand\vvec[0]{\texttt{vec}} +\newcommand\fieldmap[0]{\textit{field\_map}} +\newcommand\velem[0]{\texttt{v\_elem}} +\newcommand\vcs[0]{\texttt{cs}} +\newcommand\bits[0]{\texttt{bits}} \input{ASLSemanticsLines} @@ -220,67 +297,78 @@ \chapter{Preamble} The semantics of ASL defines all valid behaviors of a given ASL specification. More precisely, an ASL specification is first parsed into an \emph{abstract syntax tree}, -or AST, for short. Second, a type checker analyzes the \emph{parsed AST} for correctness and, if successful, -returns a \emph{static environment} and a \emph{typed AST}. Finally, tools such as interpreters and verifiers -can operate over the typed AST, based on the definition of the semantics, to test and analyze a given specification. +or AST, for short. Second, a type checker analyzes the \emph{parsed AST} for correctness and, +if successful, returns a \emph{static environment} and a \emph{typed AST}. +An ASL speicification that fails the type-checker is not associated with a static environment +and the semantics is undefined for that specification. + +Tools such as interpreters and verifiers can operate over the typed AST, based on the definition +of the semantics, to test and analyze a given specification. The abstract syntax, parsed AST, and typed AST are defined in the abstract syntax reference~\cite{ASLAbstractSyntaxReference}. The ASL type system, which defines the set of parsed ASTs that are considered valid and how to produce the corresponding typed ASTs and static environments is defined in the typing reference~\cite{ASLTypingReference}. -\paragraph{Basic Semantic Concepts.} -The semantics is constructively defined via \emph{configurations}, \emph{transitions}, and \emph{semantic rules}. -Intuitively, configurations represent intermediate states during the execution of a program and they encapsulate -the information needed to transition into other configurations. -Configurations include a \emph{dynamic environment}, which binds variables to values; -the typed AST node that needs to be ``evaluated''; a \emph{mode}, which distinguishes between different kinds of states, for example -states where an exception was raised and states where no exception was raised; a \herd\ \emph{execution graph} in the case of a -\emph{concurrent semantics}; and possible other bits of information, for example intermediate expression values. -Semantic rules define the set of possible transitions. - -\paragraph{Execution.} -A valid execution of an ASL specification transitions from an \emph{initial configuration} to an output configuration. -Such a transition is defined by transitions over the AST nodes making up the specification. - -\paragraph{Primitive Subprograms.} +\paragraph{Basic Semantic Concepts} +The ASL semantics is given by a set of \emph{semantic relations} between \emph{configurations}. +Intuitively, configurations encapsulate the information needed to transition into other configurations, +such as: +\begin{itemize} + \item a \emph{dynamic environment}, which binds variables to values; + \item the typed AST node that needs to be evaluated; + \item a \emph{concurrent execution graph}, as per a given memory model; and + \item values resulting from evaluating expressions. +\end{itemize} +The semantic relations are constructively defined via \emph{semantic rules}. +These semantic rules are defined by induction over the typed AST. + +\paragraph{Execution} +A valid execution of an ASL specification transitions from an \emph{initial configuration}, +which consists of the given specification and the standard library specification, to an output configuration +consisting of an output value and a concurrent execution graph. + +\paragraph{Primitive Subprograms} The semantics of ASL is parameterized by a set of primitive subprograms --- subprograms whose implementation is not defined by an ASL body and whose effect on the dynamic environment is defined externally. Critically, access to memory is given by primitive subprograms. We define two types of semantics --- a \emph{sequential semantics} and a \emph{concurrent semantics}. -Each semantics operates over a different kind of environment. -\paragraph{Sequential Semantics.} -The sequential semantics corresponds to executing an ASL specification in the context of a single (conceptual) process -of execution --- notice that ASL does not contain any concurrency constructs. Access to memory is hidden away -in primitive subprograms that interface with a map-like memory implementation that does not reorder memory accesses -and serves one access at a time. +\paragraph{Concurrent Semantics} +The concurrent semantics includes concurrent execution graphs. +Intuitively, these graphs define Read Effects and Write Effects to variables and constraints over those effects. +Together with the constraints that define a given memory model (such as the ARM memory model~\cite{AlglaveDGHM21}), +these graphs axiomatically define +the valid interactions of shared variables of a given specification. -\paragraph{Concurrent Semantics.} -The concurrent semantics extends the sequential semantics with \herd\ execution graphs. -Intuitively, these graphs define read and write effects to variables and constraints over those effects. -Together with the constraints that define the ARM memory model~\cite{AlglaveDGHM21}, these graphs axiomatically define -the valid sequences of read and write operations induced by a given specification. +\paragraph{Sequential Semantics} +The sequential semantics corresponds to executing an ASL specification in the context of a single (conceptual) process +of execution --- notice that ASL does not contain any concurrency constructs. +% +Technically, the sequential semantics is defined by omitting the concurrent execution graph components +from configurations. -\section{Mathematical Notations and Conventions} +\section{Mathematical Definitions and Notations} \input{ASLNotations.tex} -\paragraph{OCaml-style Notations.} -We use the notation $L(v_{1..k})$, where $L$ is a label and $v_{1..k}$ is a (possibly-singleton) tuple of abstract values, +\paragraph{OCaml-style Notations} +We use the notation $L(v_{1..k})$, where $L$ is a label and $v_{1..k}$ is a (possibly singleton) tuple of mathematical values, to denote the tuple $(L,v_{1..k})$. We also write $L(T_{1..k})$, where $T_{1..k}$ denote mathematical type of values, to stand for $\{L\} \times T_1 \times \ldots \times T_k$. % -We later use these notations to define \emph{semantic configurations} and \emph{native values}, \underline{not to be confused with labelled AST nodes}. +We later use these notations to define \emph{semantic configurations} (for example, $\Normal(\vv, \vg)$) +and \emph{native values} (for example $\nvint(\lint(1))$). % -The notation $\langle \cdot \rangle$ stands for empty-or-singleton sets, where $\None\triangleq\langle\rangle$ denotes -an empty set and $\langle v \rangle$ denotes a set containing the single element $v$. +The notation $\langle \cdot \rangle$ stands for either an empty set or a singleton set, +where $\None\triangleq\langle\rangle$ denotes an empty set +and $\langle v \rangle$ denotes a set containing the single element $v$. % -The notation $\langle T \rangle$, where $T$ denotes a mathematical type of values, stands for +The notation $\langle T \rangle$, where $T$ denotes a mathematical types of values, stands for $\{ \langle\rangle \} \cup \{\langle v \rangle \;|\; v \in T\}$. -\paragraph{Misclleaneous.} +\paragraph{Miscellaneous} We define the following shorthand notations for the true and false expressions: \newcommand\etrue[0]{\texttt{ETrue}} \newcommand\efalse[0]{\texttt{EFalse}} @@ -291,39 +379,71 @@ \section{Mathematical Notations and Conventions} \end{array} \] -We write $Z(z)$ as a shorthand for an integer $\nvliteral{\lint(z)}$, -$B(b)$ as a shorthand for a Boolean native value $\nvliteral{\lbool(b)}$, -and $R(r)$ for a real native value $\nvliteral{\lreal(r)}$. - \section{Configurations} -Configurations express intermediate states related by \emph{semantic transitions}. -Configurations wrap together elements such as environments and AST nodes -and associate them with a \emph{mode}, which helps determine how to semantic transitions. +Configurations express intermediate states related by \emph{semantic relations}. % -More precisely, semantic transitions relate two sets of configurations --- +More precisely, semantic relations relate two distinct sets of configurations --- \emph{input configurations} and \emph{output configurations}. Input configurations consist of an environment and an AST node. Output configurations consist of an output environment, values, -and \herd\ execution graphs. +and concurrent execution graphs. +% +Configurations wrap together elements such as environments and AST nodes +and associate them with a \emph{mode}. Input configurations use modes +that determine the semantic relation they pertain to, while output configurations +use modes to distinguish between conceptually different kinds of outputs, for example +ones where an exception was raised, ones when a dynamic error occurred, etc. -We now explain the components appearing in configurations. +We now explain the components over which configurations are defined: +\begin{itemize} + \item Native Values~\ref{sec:nativevalues}, which correspond values associated with ASL types. + \item Dynamic Environments~\ref{sec:dynamicenvironments}, which associate native values to variables. + \item Static Environments~\ref{sec:staticenvironments}, consist of the information inferred + by the type-checker for the specification. Also referred to as \emph{type environments}. + \item Concurrent Execution Graphs~\ref{sec:concurrentexecutiongraphs}, which track Read and Write Effects over variables. +\end{itemize} -\subsection{Native Values} +\subsection{Native Values \label{sec:nativevalues}} The semantics of an ASL specification associates \emph{native values} to variables. The set of native values is the minimal set defined by the following recursive rules (\texttt{NV} stands for Native Value): \begin{mathpar} - \inferrule[Basis Set: Integers, Reals, Booleans, Strings, and Bitvectors]{\vv \in \literal} + \inferrule[(Basis Set: Integers, Reals, Booleans, Strings, and Bitvectors)]{\vv \in \literal} { \nvliteral{v} \in \vals } \and - \inferrule[Tuple Values and Array Values]{i=1..k: v_i \in \vals} + \inferrule[(Tuple Values and Array Values)]{i=1..k: v_i \in \vals} { \nvvector{v_{1..k}} \in \vals } \and - \inferrule[Record Values]{i=1..k: \id_i \in \identifier \\ i=1..k: v_i \in \vals} - { \nvrecord{[i=1..k: \id_i\mapsto v_i]} \in \vals } + \inferrule[(Record Values)]{m \in \identifier \rightarrow_{\text{fin}} \vals} + { \nvrecord{m} \in \vals } \end{mathpar} +(The notation $\rightarrow_{\text{fin}}$ stands for a function over a finite domain.) + +We use the following shorthands for native value literals: +\[ +\begin{array}{rcl} +\nvint(z) &\triangleq& \nvliteral{\lint(z)}\\ +\nvbool(b) &\triangleq& \nvliteral{\lbool(b)}\\ +\nvreal(r) &\triangleq& \nvliteral{\lreal(r)}\\ +\nvstring(s) &\triangleq& \nvliteral{\lstring(s)}\\ +\nvbitvector(v) &\triangleq& \nvliteral{\lbitvector(v)}\\ +\end{array} +\] + +We use the following shorthands for different types of native values: +\[ +\begin{array}{rcl} +\tint &\triangleq& \{ \nvint(z) \;|\; z \in \Z\}\\ +\tbool &\triangleq& \{ \nvbool(\True), \nvbool(\False) \}\\ +\treal &\triangleq& \{ \nvreal(r) \;|\; r \in \Q\}\\ +\tstring &\triangleq& \{ \nvstring(s) \;|\; \texttt{"}s\texttt{"} \in \texttt{}\}\\ +\tbitvector &\triangleq& \{ \nvbitvector(\textit{bits}) \;|\; \textit{bits} \in \{0,1\}^+\}\\ +\tvector &\triangleq& \{ \nvvector{\textit{vals}} \;|\; \textit{vals} \in \vals^*\}\\ +\trecord &\triangleq& \{ \nvrecord{\fieldmap} \;|\; \fieldmap \in \identifier\rightarrow\vals\}\\ +\end{array} +\] -\subsection{Dynamic Environments} +\subsection{Dynamic Environments \label{sec:dynamicenvironments}} A \emph{sequential dynamic environment}, or \emph{dynamic environment}, for short, is a structure which, amongst other things, associates native values to variables. @@ -338,48 +458,16 @@ \subsection{Dynamic Environments} \end{array} \] -The native value associated with a variable $\vx$ in an environment $\denv = (G^\denv, L^\denv)$, -denoted as $\denv[\vx]$, is defined as follows: -\begin{mathpar} - \denv[\vx] \triangleq - \left\{ - \begin{array}{ll} - G^\denv(\vx) & \text{if}\ \vx \in \dom(G^\denv) \\ - L^\denv(\vx) & \text{otherwise} \\ - \end{array} - \right. -\end{mathpar} -We note that this function will always be well-defined in our semantics, since the typed AST -disallows referencing variables that have not been declared, and we will only reference a local -variable in the context of the function containing it. - -Updating the native value of a variable $\vx$ to $\vv$ in an an environment $\denv$, denoted as -$\denv[\vx \mapsto \vv]$, is defined as follows: -% -\begin{mathpar} - \denv[\vx \mapsto \vv] \triangleq - \left\{ - \begin{array}{ll} - (G^\denv[\vx \mapsto v], L^\denv) & \text{if}\ \vx \in \dom(G^\denv) \\ - (G^\denv, L^\denv[\vx \mapsto \vv]) & \text{otherwise} \\ - \end{array} - \right. -\end{mathpar} - -% Furthermore, $v?$ refers to $v$ or $\bot$, and the usage of $v$ without a -% question mark implies that $v \neq \bot$. - -\subsection{Static Environments} +\subsection{Static Environments \label{sec:staticenvironments}} -A \emph{static environment} $\tenv \in \staticenvs$ (also referred to as a \emph{type environment}) +A \emph{static environment}~\cite{ASLTypingReference} $\tenv \in \staticenvs$ (also referred to as a \emph{type environment}) is produced by the type-checker from the parsed AST. % -The ASL semantics requires a static environment in order to select the right catch clause for a thrown exception +The ASL semantics requires a static environment to select the right catch clause for a thrown exception and find the AST for a called subprogram from its name: \[ \begin{array}{rcl} - \findfunc &:& \staticenvs \times \identifier \partialto \subprogrambody\\ - % \baseval &:& \ty \partialto \vals\\ + \findfunc &:& \staticenvs \times \identifier \partialto \func\\ \typesatisfies &:& \staticenvs \times (\ty \times \ty) \rightarrow \{\True, \False\} \end{array} \] @@ -388,17 +476,20 @@ \subsection{Static Environments} We assume that the typed AST renames each function uniquely so that it can be accessed based on its name alone. % -The function $\typesatisfies(\texttt{t}, \texttt{s})$ returns true if the type \texttt{t} type-satisfies the type \texttt{s}. +The function $\typesatisfies(\texttt{t}, \texttt{s})$ returns true +if the type \texttt{t} \emph{type-satisfies} the type \texttt{s} +(see TypingRule.TypeSatisfaction~\cite{ASLTypingReference}). Environments simply pair static environments with dynamic environments: $\envs = \staticenvs \times \dynamicenvs$. We write $\env \in \envs$ to range over environments. % -We note that our semantics always maintains the same static environment. +We note that this semantics always maintains the same static environment. -\subsection{Execution Graphs} +\subsection{Concurrent Execution Graphs \label{sec:concurrentexecutiongraphs}} -The concurrent semantics of an ASL specification utilizes \herd\ \emph{execution graphs}~\cite{AlglaveDGHM21}, -which track the read/write effects over variables, yielded by the sequential semantics, and the \emph{ordering constraints} +The concurrent semantics of an ASL specification utilizes \emph{concurrent execution graphs}~\cite{AlglaveDGHM21} +(\emph{execution graphs}, for short), +which track the Read and Write Effects over variables, yielded by the sequential semantics, and the \emph{ordering constraints} between those effects. Formally, an execution graph $\xgraph = (N^\xgraph, E^\xgraph, O^\xgraph) \in \XGraphs$ @@ -411,18 +502,18 @@ \subsection{Execution Graphs} \end{array} \] -Nodes represent unique read/write effects. Formally, a node $(u,l,\id)$ associates a unique instance counter $u$ -to an \emph{ordering label} $l$, which specifies whether it represents a read or write effect to a variable named $\id$. +Nodes represent unique Read and Write Effects. Formally, a node $(u,l,\id)$ associates a unique instance counter $u$ +to an \emph{ordering label} $l$, which specifies whether it represents a Read Effect of a Write Effect to a variable named $\id$. -An edges represents an ordering constraint between two effects, which can be one of the following: +An edge represents an ordering constraint between two effects, which can be one of the following: \begin{description} \item[$\asldata$] Represents a \emph{data dependency}. -That is, when a write effect reads/write over the data written by another write effect. +That is, when a Write Effect reads/write over the data written by another Write Effect. \item[$\aslctrl$] Represents a \emph{control dependency}. -That is, when a read effect to a variable determines the flow of control (e.g., which condition of a branch is taken), -which then leads to another read/write effect. +That is, when a Read Effect to a variable determines the flow of control (e.g., which condition of a branch is taken), +which then leads to another Read/Write Effect. \item[$\aslpo$] Represents a \emph{program order}. -That is, when two effects are defined to be ordered according to the sequential semantics of the program. +That is, when two effects are defined to be ordered according to the sequential semantics. \end{description} An execution graph is \emph{well-formed} if all nodes have unique instance counters, edges connect graph nodes, @@ -437,7 +528,7 @@ \subsection{Execution Graphs} We denote the empty execution graph $\emptygraph \triangleq (\emptyset, \emptyset, \emptyset)$. % -We define the following functions, which return an execution graph that represents a single read/write effect to a variable \texttt{x}: +We define the following functions, which return an execution graph that represents a single Read/Write Effect to a variable \texttt{x}: \[ \begin{array}{rclll} \WriteEffect(\texttt{x}) &\triangleq& (\{n\}, \emptyset, \{n\}) & \text{where } n=(u, \Write, \texttt{x}), & u\in\N \text{ is fresh}\\ @@ -465,25 +556,26 @@ \subsection{Execution Graphs} \subsection{Input Configurations and Output Configurations} -Each input configuration corresponds to a group of AST node types that is associated with a corresponding -label, for example the label \texttt{expr} corresponds to the semantic relation for the expression AST node type. -We write $\texttt{label}(n)$ to denote that an AST node $n$ belongs to label \texttt{label}. +Input configuration modes are unique to the semantic relation that uses them. +For that reason, we (re-)use the name for both the semantic relation and the mode of its input configurations. +For example, the input configurations of the $\texttt{eval\_expr}$ relation +will use the $\texttt{eval\_expr}$ mode. % -We use configuration modes of the form $\texttt{eval\_label}$ for input configurations to express the intuition -that the input configuration $\texttt{eval\_label}(\env, n)$, where $\env$ is an environment -and $n$ belongs to \texttt{label}, -should be ``semantically evaluated'' (to yield an output configuration $L'(v'_{1..n})$). +We will often use the prefix \texttt{eval} for semantic relations with the intuition being that their input configurations +should be ``semantically evaluated'', yielding an output configuration. ASL semantics mainly utilizes the following types of output configurations: \begin{description} - \item[Normal Values.] Configurations representing intermediate results - (values and/or mutated environments) generated while evaluating statements: + \item[Normal Values.] Configurations consisting of different combinations of values, + execution graphs, and environments, representing intermediate results + generated while evaluating statements: \begin{itemize} \item $\Normal(\vals \times \XGraphs)$, \item $\Normal((\vals \times \XGraphs), \envs)$, \item $\Normal(((\vals \times \vals)^* \times \XGraphs), \envs)$, - \item $\Normal(\XGraphs, \envs)$, and - \item $\Normal((\vals^* \times \XGraphs), \envs)$. + \item $\Normal(\XGraphs, \envs)$, + \item $\Normal((\vals^* \times \XGraphs), \envs)$, and + \item $\Normal((\vals\times\XGraphs)^*, \envs)$. \end{itemize} \item[Exceptions.] Configurations in $\Throwing((\langle\vals \times \ty\rangle \times \XGraphs, \envs)$ @@ -491,8 +583,7 @@ \subsection{Input Configurations and Output Configurations} either without an exception value (as in \texttt{throw;}) or ones with an exception value and an associated type. \item[Returned Values.] Configurations in $\Returning((\vals^* \times \XGraphs), \envs)$ - represent values being returned by the currently executing subprogram - (which might be tuples of values). + represent (tuples of) values being returned by the currently executing subprogram. \item[Subprogram In-flight.] Configurations in $\Continuing(\XGraphs, \envs)$ represent the fact that a subprogram has more statements to execute. @@ -502,14 +593,33 @@ \subsection{Input Configurations and Output Configurations} The actual strings in an error configuration are not considered part of the specification. That is, an implementation of the semantics may use other strings. \end{description} +Helper relations often have output configurations that are just tuples, without an associated mode +(or error configurations). + +We define the following shorthands for types of output configurations: +\[ + \begin{array}{rcl} + \TThrowing &\triangleq& \Throwing(\langle\vals \times \ty\rangle \times \XGraphs, \envs)\\ + \TContinuing &\triangleq& \Continuing(\XGraphs, \envs)\\ + \TReturning &\triangleq& \Returning((\vals^* \times \XGraphs), \envs)\\ + \TError &\triangleq& \Error(\texttt{})\\ + \end{array} +\] + +We will say that a semantic transition \emph{terminates normally} when the mode of the output configuration is $\Normal$, +\emph{terminates exceptionally} when the mode of the output configuration is $\Throwing$, +\emph{terminates erroneously} when the mode of the output configuration is $\Error$, +and \emph{terminates abnormally} when it either terminates exceptionally or erroneously. -We refer to configurations with the $\Throwing$ mode and $\Error$ mode as \emph{abnormal configurations}. +When an input configuration does not satisfy any semantic rule, +there is no output configuration for it to transition to, and we will say that +the configuration is \emph{stuck}. \subsection{Extracting and Substituting Elements of Configurations} We define the \emph{mode} of a configuration $C=M(\ldots)$, denoted $\configmode{C}$, as the mode label $M$. -Given a configuration $C$, we define the the graph component of the configuration, $\graphof{C}$, +Given a configuration $C$, we define the graph component of the configuration, $\graphof{C}$, and the environment of the configuration, $\environof{C}$, as follows: \[ \begin{array}{lcc} @@ -517,11 +627,12 @@ \subsection{Extracting and Substituting Elements of Configurations} \hline \Normal(\vv,\vg) & \vg & \text{undefined}\\ \Normal((\vv,\vg), \env) & \vg & \env\\ - \Normal((i=1..k: (\texttt{va}_i,\texttt{vb}),\vg), \env) & \vg & \env\\ + \Normal(([i=1..k: (\texttt{va}_i,\texttt{vb})],\vg), \env) & \vg & \env\\ \Normal(\vg, \env) & \vg & \env\\ - \Normal(i=1..k: \vv_i, \vg) & \vg & \env\\ + \Normal([\vv_{1..k}], \vg) & \vg & \env\\ + \Normal([i=1..k: (\vv_i,\vg_i)], \env) & \text{undefined} & \env\\ \Throwing((\vx,\vg), \env) & \vg & \env\\ - \Returning((i=1..k: \vv_i,\vg), \env) & \vg & \env\\ + \Returning(([\vv_{1..k}],\vg), \env) & \vg & \env\\ \Continuing(\vg, \env) & \vg & \env\\ \end{array} \] @@ -537,6 +648,7 @@ \subsection{Extracting and Substituting Elements of Configurations} \Normal((i=1..k: (\texttt{va}_i,\texttt{vb}),\vg), \env) & \Normal((i=1..k: (\texttt{va}_i,\texttt{vb}),\vgp), \env)\\ \Normal(\vg, \env) & \Normal(\vgp, \env)\\ \Normal(i=1..k: \vv_i, \vg) & \Normal(i=1..k: \vv_i, \vgp)\\ + \Normal([i=1..k: (\vv_i,\vg_i)], \env) & \text{undefined}\\ \Throwing((\vx,\vg), \env) & \Throwing((\vx,\vgp), \env)\\ \Returning((i=1..k: \vv_i,\vg), \env) & \Returning((i=1..k: \vv_i,\vgp), \env)\\ \Continuing(\vg, \env) & \Continuing(\vgp, \env)\\ @@ -553,6 +665,7 @@ \subsection{Extracting and Substituting Elements of Configurations} \Normal((i=1..k: (\texttt{va}_i,\texttt{vb}),\vg), \env) & \Normal((i=1..k: (\texttt{va}_i,\texttt{vb}),\vg), \envp)\\ \Normal(\vg, \env) & \Normal(\vg, \envp)\\ \Normal(i=1..k: \vv_i, \vg) & \Normal(i=1..k: \vv_i, \vg)\\ + \Normal([i=1..k: (\vv_i,\vg_i)], \env) & \Normal([i=1..k: (\vv_i,\vg_i)], \envp)\\ \Throwing((\vx,\vg), \env) & \Throwing((\vx,\vg), \envp)\\ \Returning((i=1..k: \vv_i,\vg), \env) & \Returning((i=1..k: \vv_i,\vg), \envp)\\ \Continuing(\vg, \env) & \Continuing(\vg, \envp)\\ @@ -561,81 +674,75 @@ \subsection{Extracting and Substituting Elements of Configurations} \section{Semantic Evaluation} -The semantics of the various types of AST nodes is given by a set of \emph{semantic relations} between -input configurations and output configurations. -The reason that relations, rather than functions, are used is due to the +The semantics of ASL is given by the relations\footnote{The reason that relations, rather than functions, are used is due to the non-determinism inherent in the \texttt{UNKOWN} expression, the choice of execution graph node identifiers, -and potential non-determinism in the primitive subprograms. - -\newcommand\TError[0]{\textsf{TError}} -\newcommand\TNormal[0]{\textsf{TNormal}} -\newcommand\TThrowing[0]{\textsf{TThrowing}} -\newcommand\TContinuing[0]{\textsf{TContinuing}} -\newcommand\TReturning[0]{\textsf{TReturning}} -\newcommand\TConfig[0]{\textsf{TConfig}} -We define the following shorthands for the types of different configurations: -\[ - \begin{array}{rcl} - \TNormal &\triangleq& \Normal(\XGraphs, \envs)\\ - \TNormal(\vals) &\triangleq& \Normal((\vals \times \XGraphs), \envs)\\ - \TNormal((\vals \times \vals)^*) &\triangleq& \Normal(((\vals \times \vals)^* \times \XGraphs), \envs)\\ - \TNormal(\vals^*) &\triangleq& \Normal((\vals^* \times \XGraphs), \envs)\\ - \TThrowing &\triangleq& \Throwing(\langle\vals \times \ty\rangle \times \XGraphs, \envs)\\ - \TContinuing &\triangleq& \Continuing(\XGraphs, \envs)\\ - \TReturning &\triangleq& \Returning((\vals^* \times \XGraphs), \envs)\\ - \TError &\triangleq& \Error(\texttt{})\\ - \hline - \TConfig &\triangleq& \TNormal \cup \TNormal(\vals) \cup \TNormal((\vals \times \vals)^*) \cup \\ - & & \TNormal(\vals^*) \cup \TThrowing \cup \TContinuing \cup \\ - & & \TReturning \cup \TError - \end{array} -\] - -ASL defines the following relations between input configurations and output configurations -for the corresponding labels (input configurations reference AST elements~\cite{ASLAbstractSyntaxReference} -\expr, \lexpr, \stmt, \slice, \localdeclitem, \identifier, \fordirection, and \catcher): - -\begin{tabular}{ll} - \textbf{\texttt{label}} & \textbf{Input Configurations $\bigtimes$} \\ - & \textbf{Output Configurations} \\ - \hline - \hline - \texttt{expr} & $\evalexpr{\envs \times \expr} \bigtimes$\\ - & $\TNormal(\vals) \cup \TThrowing \cup \TError$\\ - \hline - \texttt{lexpr} & $\evallexpr{\envs \times \lexpr \times (\vals \times \XGraphs)} \bigtimes$\\ - & $\TNormal \cup \TThrowing \cup \TError$\\ - \hline - \texttt{slices} & $\evalslices{\envs \times \slice^*} \bigtimes$\\ - & $\TNormal((\vals \times \vals)^*) \cup \Throwing \cup \TError$ \\ - \hline - \texttt{pattern} & $\evalpattern{\envs \times \vals \times \pattern} \bigtimes$\\ - & $\TNormal(\vals)$ \\ - \hline - \texttt{local\_decl} & $\evallocaldecl{\envs \times \localdeclitem \times \langle\vals\times\XGraphs\rangle} \bigtimes$\\ - & $\TNormal$ \\ - \hline - \texttt{stmt} & $\evalstmt{\envs \times \stmt} \bigtimes$\\ - & $\TReturning \cup \TContinuing \cup \TThrowing \cup \TError$ \\ - \hline - \texttt{block} & $\evalblock{\envs \times \stmt} \bigtimes$\\ - & $\TReturning \cup \TContinuing \cup \TThrowing \cup \TError$ \\ - \hline - \texttt{loop} & $\evalloop{\envs \times \{\True,\False\} \times \expr \times \stmt} \bigtimes$\\ - & $\TReturning \cup \TContinuing \cup \TThrowing \cup \TError$ \\ - \hline - \texttt{for} & $\evalfor{\envs \times \identifier \times \vals \times \fordirection \times \vals} \bigtimes$\\ - & $\TReturning \cup \TContinuing \cup \TThrowing \cup \TError$ \\ - \hline - \texttt{catchers} & $\evalcatchers{\envs \times \catcher^* \times \langle\stmt\rangle \times \TConfig} \bigtimes$\\ - & $\TReturning \cup \TContinuing \cup \TThrowing \cup \TError$ \\ - \hline - \texttt{func} & $\evalfunc{\envs \times \identifier \times (\vals \times \XGraphs)^* \times (\identifier\times\vals)^*} \bigtimes$ \\ - & $\TNormal(\vals^*) \cup \TThrowing \cup \TError$ \\ - \end{tabular} +and potential non-determinism in the primitive subprograms.} +$\evalarrow$ and $\evalprimitivearrow$. +The latter relation provides the semantics of primitive functions and is not otherwise defined +constructively. +The relation $\evalarrow$ is defined as the disjoint union of the relations defined in this document. +% \[ +% \begin{array}{rcl} +% \evalarrow &\triangleq& \textit{main\_asl\_relations} \cupdot \textit{secondary\_asl\_relations}\\ +% \textit{main\_asl\_relations} &\triangleq& \texttt{eval\_expr} \cupdot \texttt{eval\_lexpr} \cupdot \texttt{eval\_slices}\\ +% & & \texttt{eval\_pattern} \cupdot \texttt{eval\_local\_decl} \cupdot \texttt{eval\_stmt}\\ +% & & \texttt{eval\_block} \cup \texttt{eval\_loop}\\ +% & & \texttt{eval\_catchers} \cupdot \texttt{eval\_call} \cupdot \texttt{eval\_spec}\\ +% \textit{secondary\_asl\_relations} &\triangleq& ... +% \end{array} +% \] +The semantics of the various types of AST nodes is given by a set of \emph{semantic relations} between +input configurations and output configurations. - We use the notation $C \evalarrow C'$ for an element of a semantic relation. +% ASL defines the following relations between input configurations and output configurations +% for the corresponding labels (input configurations reference AST elements~\cite{ASLAbstractSyntaxReference} +% \expr, \lexpr, \stmt, \slice, \localdeclitem, \identifier, \fordirection, and \catcher): + +% \begin{tabular}{ll} +% \textbf{\texttt{label}} & \textbf{Input Configurations $\aslrel$} \\ +% & \textbf{Output Configurations} \\ +% \hline +% \hline +% \texttt{eval\_expr} & $\evalexpr{\envs \times \expr} \aslrel$\\ +% & $\Normal(\vals \times \XGraphs) \cup \TThrowing \cup \TError$\\ +% \hline +% \texttt{eval\_lexpr} & $\evallexpr{\envs \times \lexpr \times (\vals \times \XGraphs)} \aslrel$\\ +% & $\Normal(\XGraphs,\envs) \cup \TThrowing \cup \TError$\\ +% \hline +% \texttt{eval\_slices} & $\evalslices{\envs \times \slice^*} \aslrel$\\ +% & $\Normal((\vals \times \vals)^*, \envs) \cup \Throwing \cup \TError$ \\ +% \hline +% \texttt{eval\_pattern} & $\evalpattern{\envs \times \vals \times \pattern} \aslrel$\\ +% & $\Normal(\vals, \XGraphs)$ \\ +% \hline +% \texttt{eval\_local\_decl} & $\evallocaldecl{\envs \times \localdeclitem \times \langle\vals\times\XGraphs\rangle} \aslrel$\\ +% & $\Normal(\XGraphs, \envs)$ \\ +% \hline +% \texttt{eval\_stmt} & $\evalstmt{\envs \times \stmt} \aslrel$\\ +% & $\TReturning \cup \TContinuing \cup \TThrowing \cup \TError$ \\ +% \hline +% \texttt{eval\_block} & $\evalblock{\envs \times \stmt} \aslrel$\\ +% & $\TReturning \cup \TContinuing \cup \TThrowing \cup \TError$ \\ +% \hline +% \texttt{eval\_loop} & $\evalloop{\envs \times \{\True,\False\} \times \expr \times \stmt} \aslrel$\\ +% & $\TReturning \cup \TContinuing \cup \TThrowing \cup \TError$ \\ +% \hline +% \texttt{eval\_for} & $\evalfor{\envs \times \identifier \times \vals \times \fordirection \times \vals} \aslrel$\\ +% & $\TReturning \cup \TContinuing \cup \TThrowing \cup \TError$ \\ +% \hline +% \texttt{eval\_catchers} & $\evalcatchers{\envs \times \catcher^* \times \langle\stmt\rangle \times \TOutConfig} \aslrel$\\ +% & $\TReturning \cup \TContinuing \cup \TThrowing \cup \TError$ \\ +% \hline +% \texttt{eval\_call} & $\evalcall{\envs \times \identifier \times \expr^* \times (\identifier\times\expr)^*} \aslrel$ \\ +% & $\Normal((\vals\times\XGraphs)^* \times \envs) \cup \TThrowing \cup \TError$ \\ +% \hline +% \texttt{eval\_spec} & $\evalspec{\program\times\program} \aslrel$ \\ +% & $((\vals\times \XGraphs) \cup \TError)$ \\ +% \end{tabular} + + We use the notation $C \evalarrow C'$ to denote a transition between input and output configurations. + That is, $(C, C') \in\ \evalarrow$. % We denote elements of a semantic relation by $\texttt{eval\_