[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

@@ -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

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 *)
   (* ----------------------- *)

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

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)

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},

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$.