[asl][reference] Documenting renaming of arguments in standard librar…

…y functions

asllib/ASTUtils.ml

@@ -755,37 +755,42 @@ let find_bitfields_slices_opt name bitfields =
 (* End *)
 
 let rename_locals map_name ast =
+  (* Begin RenameLocalsExpr *)
   let rec map_e e =
     map_desc_st' e @@ function
     | E_Literal _ -> e.desc
     | E_Arbitrary t -> E_Arbitrary (map_t t)
     | E_Var x -> E_Var (map_name x)
-    | E_ATC (e', t) -> E_ATC (map_e e', map_t t)
+    | E_ATC (e1, t) -> E_ATC (map_e e1, map_t t)
     | E_Binop (op, e1, e2) -> E_Binop (op, map_e e1, map_e e2)
-    | E_Unop (op, e') -> E_Unop (op, map_e e')
+    | E_Unop (op, e1) -> E_Unop (op, map_e e1)
     | E_Call { name; args; params; call_type } ->
         E_Call { name; args = map_es args; params = map_es params; call_type }
-    | E_Slice (e', slices) -> E_Slice (map_e e', map_slices slices)
+    | E_Slice (e1, slices) -> E_Slice (map_e e1, map_slices slices)
     | E_Cond (e1, e2, e3) -> E_Cond (map_e e1, map_e e2, map_e e3)
     | E_GetArray (e1, e2) -> E_GetArray (map_e e1, map_e e2)
     | E_GetEnumArray (e1, e2) -> E_GetEnumArray (map_e e1, map_e e2)
-    | E_GetField (e', f) -> E_GetField (map_e e', f)
-    | E_GetFields (e', li) -> E_GetFields (map_e e', li)
-    | E_GetItem (e', i) -> E_GetItem (map_e e', i)
+    | E_GetField (e1, f) -> E_GetField (map_e e1, f)
+    | E_GetFields (e1, li) -> E_GetFields (map_e e1, li)
+    | E_GetItem (e1, i) -> E_GetItem (map_e e1, i)
     | E_Record (t, li) -> E_Record (t, List.map (fun (f, e) -> (f, map_e e)) li)
     | E_Tuple li -> E_Tuple (map_es li)
     | E_Array { length; value } ->
         E_Array { length = map_e length; value = map_e value }
     | E_EnumArray { enum; labels; value } ->
         E_EnumArray { enum; labels; value = map_e value }
     | E_Pattern (_, _) -> failwith "Not yet implemented: obfuscate patterns"
+  (* End *)
   and map_es li = List.map map_e li
   and map_slices slices = List.map map_slice slices
+  (* Begin RenameLocalsSlice *)
   and map_slice = function
     | Slice_Length (e1, e2) -> Slice_Length (map_e e1, map_e e2)
     | Slice_Single e -> Slice_Single (map_e e)
     | Slice_Range (e1, e2) -> Slice_Range (map_e e1, map_e e2)
     | Slice_Star (e1, e2) -> Slice_Star (map_e e1, map_e e2)
+  (* End *)
+  (* Begin RenameLocalsType *)
   and map_t t =
     map_desc_st' t @@ function
     | T_Real | T_String | T_Bool | T_Enum _ | T_Named _
@@ -799,10 +804,14 @@ let rename_locals map_name ast =
     | T_Array (_, _) -> failwith "Not yet implemented: obfuscate array types"
     | T_Record li -> T_Record (List.map (fun (f, t) -> (f, map_t t)) li)
     | T_Exception li -> T_Exception (List.map (fun (f, t) -> (f, map_t t)) li)
+  (* End *)
   and map_cs cs = List.map map_c cs
+  (* Begin RenameLocalsConstraint *)
   and map_c = function
     | Constraint_Exact e -> Constraint_Exact (map_e e)
     | Constraint_Range (e1, e2) -> Constraint_Range (map_e e1, map_e e2)
+  (* End *)
+  (* Begin RenameLocalsStmt *)
   and map_s s =
     map_desc_st' s @@ function
     | S_Pass -> s.desc
@@ -822,7 +831,8 @@ let rename_locals map_name ast =
         and limit = Option.map map_e limit
         and body = map_s body in
         S_For { index_name; start_e; dir; end_e; body; limit }
-    | S_While (e, limit, s) -> S_While (map_e e, Option.map map_e limit, map_s s)
+    | S_While (e, limit, body) ->
+        S_While (map_e e, Option.map map_e limit, map_s body)
     | S_Repeat (s, e, limit) ->
         S_Repeat (map_s s, map_e e, Option.map map_e limit)
     | S_Throw (Some (e, t)) -> S_Throw (Some (map_e e, Option.map map_t t))
@@ -834,6 +844,8 @@ let rename_locals map_name ast =
     | S_Pragma (name, args) ->
         let args = map_es args in
         S_Pragma (name, args)
+  (* End *)
+  (* Begin RenameLocalsLexpr *)
   and map_le le =
     map_desc_st' le @@ function
     | LE_Discard -> le.desc
@@ -844,16 +856,24 @@ let rename_locals map_name ast =
     | LE_SetField (le, f) -> LE_SetField (map_le le, f)
     | LE_SetFields (le, f, annot) -> LE_SetFields (map_le le, f, annot)
     | LE_Destructuring les -> LE_Destructuring (List.map map_le les)
+  (* End *)
+  (* Begin RenameLocalsLDI *)
   and map_ldi = function
     | LDI_Var x -> LDI_Var (map_name x)
     | LDI_Tuple names -> LDI_Tuple (List.map map_name names)
+  (* End *)
   and map_body = function
     | SB_Primitive _ as b -> b
     | SB_ASL s -> SB_ASL (map_s s)
+  (* Begin RenameLocalsFunc *)
   and map_func f =
+    (* RenameLocalsArgs( *)
     let map_args li = List.map (fun (name, t) -> (map_name name, map_t t)) li in
+    (* RenameLocalsArgs) *)
+    (* RenameLocalsNamedArgs( *)
     let map_nargs li =
       List.map (fun (name, t) -> (map_name name, Option.map map_t t)) li
+      (* RenameLocalsNamedArgs) *)
     in
     {
       f with
@@ -862,10 +882,13 @@ let rename_locals map_name ast =
       body = map_body f.body;
       return_type = Option.map map_t f.return_type;
     }
+  (* End *)
+  (* Begin RenameLocals *)
   and map_decl d =
     map_desc_st' d @@ function D_Func f -> D_Func (map_func f) | d -> d
   in
   List.map map_decl ast
+(* End *)
 
 (* Taken from lib/innerRel.ml *)
 let rec transitive_closure m0 =

asllib/doc/ASLFormal.tex

@@ -361,6 +361,15 @@ \subsection{Lists}
 \]
 \end{definition}
 
+\subsection{Strings}
+\hypertarget{def-stringconcat}{}
+The function $\stringconcat : \Strings \times \Strings \rightarrow \Strings$
+concatenates two strings.
+
+\hypertarget{def-stringofnat}{}
+The function $\stringofnat : \N \rightarrow \Strings$ converts a natural number
+to the corresponding string.
+
 \subsection{OCaml-style Notations}
 We use the following notations, which are in the style of the OCaml programming language,
 to facilitate correspondence with our
@@ -373,11 +382,12 @@ \subsection{OCaml-style Notations}
 \hypertarget{def-optional}{}
 \begin{definition}[Optional]
 \hypertarget{def-none}{}
-The notation $\langle \cdot \rangle$ stands for either an empty set or a singleton set,
+\hypertarget{def-some}
+The notation $\Some{\cdot}$ 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$.
+and $\Some{v}$ denotes a set containing the single element $v$.
 %
-The notation $\langle T \rangle$, where $T$ denotes a mathematical type, stands for
+The notation $\Some{T}$, where $T$ denotes a mathematical type, stands for
 $\{ \langle\rangle \} \cup \{\langle v \rangle \;|\; v \in T\}$.
 
 We refer to $\langle T\rangle$ as an \emph{optional}.
@@ -893,15 +903,49 @@ \subsection{Boolean Transition Assertions}
 \end{mathpar}
 This is useful in that it allows us to use assertions in rule macros.
 
-% \begin{mathpar}
-%   \inferrule{
-%     \exprequalnorm(\tenv, \veone, \vetwo) \typearrow \False \terminateas \True\\\\
-%     \exprequalcase(\tenv, \veone, \vetwo) \typearrow \vb
-%   }
-%   {
-%     \exprequal(\tenv, \veone, \vetwo) \typearrow \vb
-%   }
-% \end{mathpar}
+\subsection{Assertions Over Optional Data Types}
+\hypertarget{def-mapopt}{}
+Optional data types are prevalent in the AST.
+To facilitate transition assertions over optional data types,
+we introduce the parametric function,
+which accepts a one-argument relation (or function) $f : A \aslrel B$
+and applies it to an optional value $A?$:
+\[
+\mapopt{\cdot} : \overname{A?}{\vvopt} \aslrel \overname{B?}{\vvoptnew}
+\]
+
+\ProseParagraph
+\OneApplies
+\begin{itemize}
+  \item \AllApplyCase{Some}
+  \begin{itemize}
+    \item $\vvopt$ consists of the value $v$;
+    \item applying $f$ to $v$ yields $v'$;
+    \item \Proseeqdef{$\vvoptnew$}{the singleton set consisting of $v'$}.
+  \end{itemize}
+
+  \item \AllApplyCase{None}
+  \begin{itemize}
+    \item $\vvopt$ is $\None$;
+    \item \Proseeqdef{$\vvoptnew$}{$\None$}.
+  \end{itemize}
+\end{itemize}
+
+\FormallyParagraph
+\begin{mathpar}
+\inferrule[Some]{
+  f(v) \longrightarrow v'
+}{
+  \mapopt{f}(\overname{\Some{v}}{\vvopt}) \longrightarrow{r} \Some{v'}
+}
+\end{mathpar}
+
+\begin{mathpar}
+\inferrule[None]{}{
+  \mapopt{f}(\None) \longrightarrow \None
+}
+\end{mathpar}
+
 
 \subsection{Rule Naming}
 To name a rule, we place it in a section with its name.