Improved l-expressions

- Fixed a bug where some l-expressions which wrote registers wern't
picking up register writes.

- Can now write to registers with record types. e.g. ARM's ProcState
record from ASL.

7 files changed, 145 insertions, 10 deletions

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index e410eb4b..e6162a68 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -81,7 +81,7 @@ let doc_qi (QI_aux(qi,_)) = match qi with
 (* typ_doc is the doc for the type being quantified *)
 let doc_typquant (TypQ_aux(tq,_)) typ_doc = match tq with
   | TypQ_no_forall -> typ_doc
-  | TypQ_tq [] -> failwith "TypQ_tq with empty list"
+  | TypQ_tq [] -> typ_doc
   | TypQ_tq qlist ->
     (* include trailing break because the caller doesn't know if tq is empty *)
     doc_op dot
diff --git a/src/sail.ml b/src/sail.ml
index bb2fdaa5..3500b213 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -103,6 +103,9 @@ let options = Arg.align ([
   ( "-dno_cast",
     Arg.Set opt_dno_cast,
     " (debug) typecheck without any implicit casting");
+  ( "-no_effects",
+    Arg.Set Type_check.opt_no_effects,
+    " turn off effect checking");
   ( "-v",
     Arg.Set opt_print_version,
     " print version");
diff --git a/src/type_check.ml b/src/type_check.ml
index a7d44544..ee88f746 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -47,6 +47,7 @@ open Ast_util
 open Big_int
 
 let opt_tc_debug = ref 0
+let opt_no_effects = ref false
 let depth = ref 0
 
 let rec indent n = match n with
@@ -83,6 +84,8 @@ let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
 let inc_ord = Ord_aux (Ord_inc, Parse_ast.Unknown)
 let dec_ord = Ord_aux (Ord_dec, Parse_ast.Unknown)
 
+let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown)
+
 let int_typ = mk_id_typ (mk_id "int")
 let nat_typ = mk_id_typ (mk_id "nat")
 let unit_typ = mk_id_typ (mk_id "unit")
@@ -177,6 +180,27 @@ let string_of_index_sort = function
      ^ string_of_list " & " (fun (x, y) -> string_of_nexp x ^ " <= " ^ string_of_nexp y) constraints
      ^ "}"
 
+let quant_items : typquant -> quant_item list = function
+  | TypQ_aux (TypQ_tq qis, _) -> qis
+  | TypQ_aux (TypQ_no_forall, _) -> []
+
+let kopt_kid (KOpt_aux (kopt_aux, _)) =
+  match kopt_aux with
+  | KOpt_none kid | KOpt_kind (_, kid) -> kid
+
+let is_nat_kopt = function
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), _), _) -> true
+  | KOpt_aux (KOpt_none _, _) -> true
+  | _ -> false
+
+let is_order_kopt = function
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), _), _) -> true
+  | _ -> false
+
+let is_typ_kopt = function
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), _), _) -> true
+  | _ -> false
+
 (**************************************************************************)
 (* 1. Substitutions                                                       *)
 (**************************************************************************)
@@ -481,6 +505,7 @@ end = struct
     || Id.compare id (mk_id "bool") = 0
     || Id.compare id (mk_id "real") = 0
     || Id.compare id (mk_id "list") = 0
+    || Id.compare id (mk_id "string") = 0
 
   (* Check if a type, order, or n-expression is well-formed. Throws a
      type error if the type is badly formed. FIXME: Add arity to type
@@ -554,8 +579,22 @@ end = struct
     else
       begin
         typ_print ("Adding record " ^ string_of_id id);
+        let rec record_typ_args = function
+          | [] -> []
+          | ((QI_aux (QI_id kopt, _)) :: qis) when is_nat_kopt kopt ->
+             mk_typ_arg (Typ_arg_nexp (nvar (kopt_kid kopt))) :: record_typ_args qis
+          | ((QI_aux (QI_id kopt, _)) :: qis) when is_typ_kopt kopt ->
+             mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kopt)))) :: record_typ_args qis
+          | ((QI_aux (QI_id kopt, _)) :: qis) when is_order_kopt kopt ->
+             mk_typ_arg (Typ_arg_order (mk_ord (Ord_var (kopt_kid kopt)))) :: record_typ_args qis
+          | (_ :: qis) -> record_typ_args qis
+        in
+        let rectyp = match record_typ_args (quant_items typq) with
+          | [] -> mk_id_typ id
+          | args -> mk_typ (Typ_app (id, args))
+        in
         let fold_accessors accs (typ, fid) =
-          let acc_typ = mk_typ (Typ_fn (mk_id_typ id, typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
+          let acc_typ = mk_typ (Typ_fn (rectyp, typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
           typ_print (indent 1 ^ "Adding accessor " ^ string_of_id fid ^ " :: " ^ string_of_bind (typq, acc_typ));
           Bindings.add fid (typq, acc_typ) accs
         in
@@ -1365,10 +1404,6 @@ let infer_lit env (L_aux (lit_aux, l) as lit) =
      end
   | L_undef -> typ_error l "Cannot infer the type of undefined"
 
-let quant_items : typquant -> quant_item list = function
-  | TypQ_aux (TypQ_tq qis, _) -> qis
-  | TypQ_aux (TypQ_no_forall, _) -> []
-
 let is_nat_kid kid = function
   | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), kid'), _) -> Kid.compare kid kid' = 0
   | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0
@@ -1908,6 +1943,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
             end
        in
        let regtyp, inferred_flexp = infer_flexp flexp in
+       typ_debug ("REGTYP: " ^ string_of_typ regtyp ^ " / " ^ string_of_typ (Env.expand_synonyms env regtyp));
        match Env.expand_synonyms env regtyp with
        | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env ->
           let base, top, ranges = Env.get_regtyp regtyp_id env in
@@ -1924,6 +1960,12 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
           in
           let checked_exp = crule check_exp env exp vec_typ in
           annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp (mk_effect [BE_wreg]), field)) vec_typ) checked_exp, env
+       | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
+          let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor field env in
+          let unifiers = try unify l env rectyp_q regtyp with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+          let field_typ' = subst_unifiers unifiers field_typ in
+          let checked_exp = crule check_exp env exp field_typ' in
+          annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp (mk_effect [BE_wreg]), field)) field_typ') checked_exp, env
        | _ ->  typ_error l "Field l-expression has invalid type"
      end
   | LEXP_memory (f, xs) ->
@@ -1997,11 +2039,12 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
      end
   | LEXP_vector_range (LEXP_aux (LEXP_id v, _), exp1, exp2) ->
      begin
-       let is_immutable, vtyp = match Env.lookup_id v env with
+       let is_immutable, is_register, vtyp = match Env.lookup_id v env with
          | Unbound -> typ_error l "Cannot assign to element of unbound vector"
          | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
-         | Local (Immutable, vtyp) -> true, vtyp
-         | Local (Mutable, vtyp) | Register vtyp -> false, vtyp
+         | Local (Immutable, vtyp) -> true, false, vtyp
+         | Local (Mutable, vtyp) -> false, false, vtyp
+         | Register vtyp -> false, true, vtyp
        in
        let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in
        let E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) = access in
@@ -2009,6 +2052,9 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
        | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" ->
           subtyp l env typ deref_typ;
           annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env
+       | _ when not is_immutable && is_register ->
+          subtyp l env typ (typ_of access);
+          annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env
        | _ when not is_immutable ->
           subtyp l env typ (typ_of access);
           annot_lexp (LEXP_vector_range (annot_lexp (LEXP_id v) vtyp, inferred_exp1, inferred_exp2)) typ, env
@@ -2560,7 +2606,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
       [mk_val_spec quant typ id], Env.add_val_spec id (quant, typ) env, eff
     else [], env, declared_eff
   in
-  if equal_effects eff declared_eff
+  if (equal_effects eff declared_eff || !opt_no_effects)
   then
     vs_def @ [DEF_fundef (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, None)))], env
   else typ_error l ("Effects do not match: " ^ string_of_effect declared_eff ^ " declared and " ^ string_of_effect eff ^ " found")
diff --git a/src/type_check.mli b/src/type_check.mli
index 723f796a..0c943f6f 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -45,6 +45,7 @@ open Ast
 open Ast_util
 
 val opt_tc_debug : int ref
+val opt_no_effects : bool ref
 
 exception Type_error of l * string;;
 
diff --git a/test/typecheck/fail/procstate1.sail b/test/typecheck/fail/procstate1.sail
new file mode 100644
index 00000000..00dc1ab1
--- /dev/null
+++ b/test/typecheck/fail/procstate1.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+typedef ProcState = const struct forall Num 'n.
+{
+  bit['n] N;
+  bit[1] Z;
+  bit[1] C;
+  bit[1] V
+}
+
+register ProcState<2> PSTATE
+
+function unit test () =
+{
+  PSTATE.N := 0b1
+}
diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail
new file mode 100644
index 00000000..cfae86a1
--- /dev/null
+++ b/test/typecheck/pass/arm_FPEXC1.sail
@@ -0,0 +1,53 @@
+default Order dec
+
+val forall Num 'n. (bit['n], int) -> bit effect pure vector_access
+
+val forall Num 'n, Num 'm, Num 'o, 'm >= 'o, 'o >= 0, 'n >= 'm + 1.
+  (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange
+
+register vector<32 - 1, 32, dec, bit>  _FPEXC32_EL2
+
+val vector<32 - 1, 32, dec, bit>  -> unit effect {wreg} set_FPEXC32_EL2
+
+function set_FPEXC32_EL2 value_name =
+  {
+    _FPEXC32_EL2[0..0] := [value_name[0]];
+    _FPEXC32_EL2[1..1] := [value_name[1]];
+    _FPEXC32_EL2[2..2] := [value_name[2]];
+    _FPEXC32_EL2[3..3] := [value_name[3]];
+    _FPEXC32_EL2[4..4] := [value_name[4]];
+    _FPEXC32_EL2[6..5] := value_name[6 .. 5];
+    _FPEXC32_EL2[7..7] := [value_name[7]];
+    _FPEXC32_EL2[20..11] := value_name[20 .. 11];
+    _FPEXC32_EL2[29..29] := [value_name[29]];
+    _FPEXC32_EL2[30..30] := [value_name[30]]
+  }
+
+val unit -> vector<32 - 1, 32, dec, bit>  effect {rreg} get_FPEXC32_EL2
+
+function get_FPEXC32_EL2 () =
+  {
+    (vector<32 - 1, 32, dec, bit> ) value_name := 0x04000700;
+    value_name[0..0] := [_FPEXC32_EL2[0]];
+    value_name[1..1] := [_FPEXC32_EL2[1]];
+    value_name[2..2] := [_FPEXC32_EL2[2]];
+    value_name[3..3] := [_FPEXC32_EL2[3]];
+    value_name[4..4] := [_FPEXC32_EL2[4]];
+    value_name[6..5] := _FPEXC32_EL2[6 .. 5];
+    value_name[7..7] := [_FPEXC32_EL2[7]];
+    value_name[20..11] := _FPEXC32_EL2[20 .. 11];
+    value_name[26..26] := [_FPEXC32_EL2[26]];
+    value_name[29..29] := [_FPEXC32_EL2[29]];
+    value_name[30..30] := [_FPEXC32_EL2[30]];
+    value_name
+  }
+
+val vector<32 - 1, 32, dec, bit>  -> unit effect {rreg, wreg} set_FPEXC
+
+function set_FPEXC val_name =
+  {
+    (vector<32 - 1, 32, dec, bit> ) r := val_name;
+    (vector<32 - 1, 32, dec, bit> ) __tmp_45 := get_FPEXC32_EL2();
+    __tmp_45[31..0] := r;
+    set_FPEXC32_EL2(__tmp_45)
+  }
diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail
new file mode 100644
index 00000000..95ba97db
--- /dev/null
+++ b/test/typecheck/pass/procstate1.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+typedef ProcState = const struct forall Num 'n.
+{
+  bit['n] N;
+  bit[1] Z;
+  bit[1] C;
+  bit[1] V
+}
+
+register ProcState<1> PSTATE
+
+function unit test () =
+{
+  PSTATE.N := 0b1
+}