Flow typing and l-expression changes for ASL parser

1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.

2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.

The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.

3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.

4. Include a newly generated version of aarch64_no_vector

5. Update the Ocaml test suite to use builtins in lib/

1 files changed, 35 insertions, 25 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 62c1af02..1ba1b9e6 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -539,35 +539,45 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     ), (l,()))
 
 and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp =
-  LEXP_aux(
-    (match exp with
-     | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id)
-     | Parse_ast.E_deref(exp) -> LEXP_deref(to_ast_exp k_env def_ord exp)
-     | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) ->
-       LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id)
-     | Parse_ast.E_tuple(tups) ->
+  let lexp = match exp with
+    | Parse_ast.E_id id -> LEXP_id (to_ast_id id)
+    | Parse_ast.E_deref exp -> LEXP_deref (to_ast_exp k_env def_ord exp)
+    | Parse_ast.E_cast (typ, Parse_ast.E_aux (Parse_ast.E_id id, l')) ->
+       LEXP_cast (to_ast_typ k_env def_ord typ, to_ast_id id)
+    | Parse_ast.E_tuple tups ->
        let ltups = List.map (to_ast_lexp k_env def_ord) tups in
-       let is_ok_in_tup (LEXP_aux (le,(l,_))) =
+       let is_ok_in_tup (LEXP_aux (le, (l, _))) =
          match le with
-         | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> ()
+         | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_vector_concat _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> ()
          | LEXP_memory _ | LEXP_deref _ ->
-           typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in
+            typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None
+       in
        List.iter is_ok_in_tup ltups;
-       LEXP_tup(ltups)
-    | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),args) ->
-      (match f with
-      | Parse_ast.Id(id) ->
-	(match List.map (to_ast_exp k_env def_ord) args with
-          | [E_aux(E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory(to_ast_id f',[])
-	  | [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps)
-	  | args -> LEXP_memory(to_ast_id f', args))
-      | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None)
-    | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp)
-    | Parse_ast.E_vector_subrange(vexp,exp1,exp2) ->
-      LEXP_vector_range(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
-    | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env def_ord fexp, to_ast_id id)
-    | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None)
-      , (l,()))
+       LEXP_tup ltups
+    | Parse_ast.E_app ((Parse_ast.Id_aux (f, l') as f'), args) ->
+       begin match f with
+       | Parse_ast.Id(id) ->
+          (match List.map (to_ast_exp k_env def_ord) args with
+           | [E_aux (E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory (to_ast_id f', [])
+           | [E_aux (E_tuple exps,_)] -> LEXP_memory (to_ast_id f', exps)
+           | args -> LEXP_memory(to_ast_id f', args))
+       | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None
+       end
+    | Parse_ast.E_vector_append (exp1, exp2) ->
+       LEXP_vector_concat (to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2)
+    | Parse_ast.E_vector_access (vexp, exp) -> LEXP_vector (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp)
+    | Parse_ast.E_vector_subrange (vexp, exp1, exp2) ->
+       LEXP_vector_range (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
+    | Parse_ast.E_field (fexp, id) -> LEXP_field (to_ast_lexp k_env def_ord fexp, to_ast_id id)
+    | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None
+  in
+  LEXP_aux (lexp, (l, ()))
+
+and to_ast_lexp_vector_concat k_env def_ord (Parse_ast.E_aux (exp_aux, l) as exp) =
+  match exp_aux with
+  | Parse_ast.E_vector_append (exp1, exp2) ->
+     to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2
+  | _ -> [to_ast_lexp k_env def_ord exp]
 
 and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : unit pexp =
   match pex with