Merge pull request #814 from herd/asl-getfields-to-call

[asl] Can call a setter or getter on bitfields with field access syntax.

Check for existing getter (resp. setter) when typing field access (resp .update).

This feature is useful to view subfields of bitfields as distinct objects. For instance, the fields `X` and `Y` below apparently belong to a single bitfield `STATE`, as we write `STATE.X` and `STATE.Y`. However they in fact correspond to different bitfields `_X` and `_STATE`.

```
type State of bits(2) {
  [0] X,
  [1] Y,
};

var _X:State;
var _STATE:State;

// Defining the following canonical getter is mandatory to bridge the gap
// between the name STATE and te type State.
getter STATE[] => State
begin
 return _STATE;
end

setter STATE[] = v : State
begin
  _STATE = v;
end

getter STATE[n:integer] => bits(1)
begin
  if n <= 0 then
    return _X[n];
  else
    return _STATE[n];
  end
end

setter STATE[n:integer] = v : bits(1)
begin
  if n <= 0 then
    _X[n] = v;
  else
    _STATE[n] = v;
  end
end

func main() => integer
begin
  STATE.X = '1';
  STATE.Y = '1';
  print(STATE.X,STATE.Y);
  print(_X,_STATE);
  return 0;
end
```
As a result the above program will print two lines `'1' '1'` and `'01' '10'`.

The framework is slightly more generic : multiple field accesses, such as `STATE.[X,Y]` are handled, provided the appropriate getter and setters are defined. Here, one should for instance define `getter STATE[n:integer,m:integer] => bits(2)` with whatever adequate body.

asllib/Interpreter.ml

@@ -199,8 +199,13 @@ module Make (B : Backend.S) (C : Config) = struct
                 | None, Some t -> base_value env t
               in
               let* () =
+(*
+ * Those identifiers are initialised to their current value
+ * before executing each instruction. Hence, we discard
+ * the initial values from `.asl` files.
+ *)
                 match name with
-                | "PSTATE" | "RESADDR" -> return ()
+                | "RESADDR" | "_NZCV" -> return ()
                 | _ -> B.on_write_identifier name Scope_Global v
               in
               IEnv.declare_global name v env |> return

asllib/Typing.ml

@@ -102,7 +102,7 @@ let rename_ty_eqs : (AST.identifier * AST.expr) list -> AST.ty -> AST.ty =
         T_Int (WellConstrained constraints) |> add_pos_from_st ty
     | _ -> ty
 
-(* Begin Lit *)    
+(* Begin Lit *)
 let annotate_literal = function
   | L_Int _ as v -> integer_exact' (literal v)
   | L_Bool _ -> T_Bool
@@ -349,6 +349,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
                   PP.pp_pos loc name;
               ([], name, callee_arg_types, return_type)
         with Error.ASLException _ -> raise error)
+
   end
 
   (* -------------------------------------------------------------------------
@@ -402,6 +403,59 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
     in
     List.fold_left (one_slice loc env) Diet.Int.empty slices
 
+  exception NoSingleField
+
+  let to_singles env =
+    let eval e =
+      match reduce_constants env e with
+      | L_Int z -> Z.to_int z
+      | _ -> raise NoSingleField in
+    let one slice k =
+      match slice with
+      | Slice_Single e -> e::k
+      | Slice_Length (e1,e2) ->
+         let i1 = eval e1 and i2 = eval e2 in
+         let rec do_rec n =
+           if n >= i2 then k
+           else
+             let e =
+               E_Literal (L_Int (Z.of_int (i1+n))) |> add_dummy_pos in
+             e::do_rec (n+1) in
+         do_rec 0
+      | Slice_Range (e1,e2) ->
+         let i1 = eval e1 and i2 = eval e2 in
+         let rec do_rec i =
+           if i > i1 then k
+         else
+           let e =  E_Literal (L_Int (Z.of_int i)) |> add_dummy_pos in
+           e::do_rec (i+1) in
+         do_rec i2
+      | Slice_Star _ ->
+         raise NoSingleField in
+    fun slices -> List.fold_right one slices []
+
+
+  let slices_of_bitfield = function
+    | BitField_Simple (_, slices)
+    | BitField_Nested (_, slices, _)
+    | BitField_Type (_, slices, _) ->
+        slices
+
+  let field_to_single env bf field =
+    match find_bitfield_opt field bf with
+    | Some bitfield -> to_singles env (slices_of_bitfield bitfield)
+    | None -> raise NoSingleField
+
+  let should_fields_reduce_to_call env name ty fields =
+    match ty.desc with
+    | T_Bits (_, bf) when should_reduce_to_call env name -> (
+        try Some (name, list_concat_map (field_to_single env bf) fields)
+        with NoSingleField -> None)
+    | _ -> None
+
+  let should_field_reduce_to_call env name ty field =
+    should_fields_reduce_to_call env name ty [field]
+
   (* -------------------------------------------------------------------------
 
                               Annotate AST
@@ -1192,73 +1246,103 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
                 |: TypingRule.EGetArray))
     (* End *)
     | E_GetField (e1, field_name) -> (
-        let t_e1, e2 = annotate_expr env e1 in
-        let t_e2 = Types.make_anonymous env t_e1 in
-        match t_e2.desc with
-        | T_Exception fields | T_Record fields -> (
-            match List.assoc_opt field_name fields with
-            (* Begin EGetBadRecordField *)
-            | None ->
+      let t_e1, e2 = annotate_expr env e1 in
+      let t_e2 = Types.make_anonymous env t_e1 in
+      let reduced =
+        match e1.desc with
+        | E_Var x ->
+           should_field_reduce_to_call env x t_e2 field_name
+        | _ -> None in
+      match reduced with
+      | Some (name,args) ->
+         let name, args, eqs, ty =
+           annotate_call (to_pos e) env name args [] ST_Getter
+         in
+         let ty = match ty with Some ty -> ty | None -> assert false in
+         (ty, E_Call (name, args, eqs) |> here)
+      | None ->
+         begin
+           match t_e2.desc with
+           | T_Exception fields | T_Record fields -> (
+             match List.assoc_opt field_name fields with
+             (* Begin EGetBadRecordField *)
+             | None ->
                 fatal_from e (Error.BadField (field_name, t_e2))
                 |: TypingRule.EGetBadRecordField
-            (* End *)
-            (* Begin EGetRecordField *)
-            | Some t ->
+             (* End *)
+             (* Begin EGetRecordField *)
+             | Some t ->
                 (t, E_GetField (e2, field_name) |> here)
                 |: TypingRule.EGetRecordField
-                (* End *))
-        | T_Bits (_, bitfields) -> (
-            match find_bitfield_opt field_name bitfields with
-            (* Begin EGetBadBitField *)
-            | None ->
+           (* End *))
+           | T_Bits (_, bitfields) -> (
+             match find_bitfield_opt field_name bitfields with
+             (* Begin EGetBadBitField *)
+             | None ->
                 fatal_from e (Error.BadField (field_name, t_e2))
                 |: TypingRule.EGetBadBitField
-            (* End *)
-            (* Begin EGetBitField *)
-            | Some (BitField_Simple (_field, slices)) ->
+             (* End *)
+             (* Begin EGetBitField *)
+             | Some (BitField_Simple (_field, slices)) ->
                 let e3 = E_Slice (e1, slices) |> here in
                 annotate_expr env e3 |: TypingRule.EGetBitField
-            (* End *)
-            (* Begin EGetBitFieldNested *)
-            | Some (BitField_Nested (_field, slices, bitfields')) ->
+             (* End *)
+             (* Begin EGetBitFieldNested *)
+             | Some (BitField_Nested (_field, slices, bitfields')) ->
                 let t_e3, e3 =
                   E_Slice (e2, slices) |> here |> annotate_expr env
                 in
                 let t_e4 =
                   match t_e3.desc with
                   | T_Bits (width, _bitfields) ->
-                      T_Bits (width, bitfields') |> add_pos_from t_e2
+                     T_Bits (width, bitfields') |> add_pos_from t_e2
                   | _ -> assert false
                 in
                 (t_e4, e3) |: TypingRule.EGetBitFieldNested
-            (* End *)
-            (* Begin EGetBitFieldTyped *)
-            | Some (BitField_Type (_field, slices, t)) ->
+             (* End *)
+             (* Begin EGetBitFieldTyped *)
+             | Some (BitField_Type (_field, slices, t)) ->
                 let t_e3, e3 =
                   E_Slice (e2, slices) |> here |> annotate_expr env
                 in
                 let+ () = check_type_satisfies e3 env t_e3 t in
                 (t, e3) |: TypingRule.EGetBitFieldTyped)
-        (* Begin EGetBadField *)
-        | _ ->
-            conflict e [ default_t_bits; T_Record []; T_Exception [] ] t_e1
-            |: TypingRule.EGetBadField
-        (* End *))
-    | E_GetFields (e', fields) ->
-        let t_e', e' = annotate_expr env e' in
-        let t_e' = Types.make_anonymous env t_e' in
-        let bitfields =
-          match t_e'.desc with
-          | T_Bits (_, bitfields) -> bitfields
-          | _ -> conflict e [ default_t_bits ] t_e'
-        in
-        let one_field field =
-          match find_bitfields_slices_opt field bitfields with
-          | None -> fatal_from e (Error.BadField (field, t_e'))
-          | Some slices -> slices
-        in
-        E_Slice (e', list_concat_map one_field fields)
-        |> here |> annotate_expr env |: TypingRule.EGetBitFields
+           (* Begin EGetBadField *)
+           | _ ->
+              conflict e [ default_t_bits; T_Record []; T_Exception [] ] t_e1
+              |: TypingRule.EGetBadField
+         end
+    (* End *))
+    | E_GetFields (e_1, fields) ->
+       let t_e', e_2 = annotate_expr env e_1 in
+       let t_e' = Types.make_anonymous env t_e' in
+       let reduced =
+         match e_1.desc with
+         | E_Var x ->
+            should_fields_reduce_to_call env x t_e' fields
+         | _ -> None in
+       begin
+         match reduced with
+         | Some (name,args) ->
+            let name, args, eqs, ty =
+              annotate_call (to_pos e) env name args [] ST_Getter
+            in
+            let ty = match ty with Some ty -> ty | None -> assert false in
+            (ty, E_Call (name, args, eqs) |> here)
+         | None ->
+            let bitfields =
+              match t_e'.desc with
+              | T_Bits (_, bitfields) -> bitfields
+              | _ -> conflict e [ default_t_bits ] t_e'
+            in
+            let one_field field =
+              match find_bitfields_slices_opt field bitfields with
+              | None -> fatal_from e (Error.BadField (field, t_e'))
+              | Some slices -> slices
+            in
+            E_Slice (e_2, list_concat_map one_field fields)
+            |> here |> annotate_expr env |: TypingRule.EGetBitFields
+       end
     (* End *)
     (* Begin EPattern *)
     | E_Pattern (e', patterns) ->
@@ -1283,8 +1367,8 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
            |  { p0 , ... pN }         ->       e IN p0 || ... e IN pN
            | !{ p0 , ... pN }         ->       not (e IN p0) && ... e IN pN
 
-         We cannot reduce them here (as otherwise e might be evaluated a 
-         bad number of times), but we will apply the same typing rules as for 
+         We cannot reduce them here (as otherwise e might be evaluated a
+         bad number of times), but we will apply the same typing rules as for
          those desugared expressions.
          *)
         let t_e', e'' = annotate_expr env e' in
@@ -1830,11 +1914,11 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
   and try_annotate_block env s =
     (*
         See rule JFRD:
-           A local identifier declared with var, let or constant 
-           is in scope from the point immediately after its declaration 
+           A local identifier declared with var, let or constant
+           is in scope from the point immediately after its declaration
            until the end of the immediately enclosing block.
 
-        From that follows that we can discard the environment at the end 
+        From that follows that we can discard the environment at the end
         of an enclosing block.
     *)
     best_effort s (fun _ -> annotate_stmt env s |> fst) |: TypingRule.Block
@@ -1843,6 +1927,26 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
   and try_annotate_stmt env s =
     best_effort (s, env) (fun _ -> annotate_stmt env s)
 
+  and set_fields_should_reduce_to_call env le x fields e =
+    (*
+     * Field indices are extracted from the return type
+     * of "associated" getter.
+     *)
+    if not (should_reduce_to_call env x) then None
+    else
+      let ( let* ) = Option.bind in
+      let _, _, _, ty_opt =
+        try FunctionRenaming.try_find_name le env x []
+        with Error.ASLException _ -> assert false in
+      let* ty = ty_opt in
+      let ty = Types.make_anonymous env ty in
+      let* name, args = should_fields_reduce_to_call env x ty fields in
+      let name, args, eqs, ret_ty =
+        annotate_call (to_pos le) env name (e :: args) [] ST_Setter
+      in
+      let () = assert (ret_ty = None) in
+      Some (S_Call (name, args, eqs) |> add_pos_from le)
+
   and setter_should_reduce_to_call_s env le e : stmt option =
     let () =
       if false then
@@ -1867,9 +1971,13 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
     in
     match le.desc with
     | LE_Discard -> None
+    | LE_SetField ( { desc=LE_Var x; _ }, field) ->
+       set_fields_should_reduce_to_call env le x [field] e
     | LE_SetField (sub_le, field) ->
         let old_le le' = LE_SetField (le', field) |> here in
         with_temp old_le sub_le
+    | LE_SetFields ({ desc = LE_Var x; _ }, fields) ->
+        set_fields_should_reduce_to_call env le x fields e
     | LE_SetFields (sub_le, fields) ->
         let old_le le' = LE_SetFields (le', fields) |> here in
         with_temp old_le sub_le

herd/AArch64ASLSem.ml

@@ -808,12 +808,12 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
               | _ -> st)
             ASLS.A.state_empty ASLBase.gregs
         in
-        let nzcv = AArch64Base.NZCV and pstate = global_loc "PSTATE" in
+        let nzcv = AArch64Base.NZCV and _nzcv = global_loc "_NZCV" in
         let st =
           match A.look_reg nzcv ii.A.env.A.regs with
           | Some v ->
               let v = aarch64_to_asl_bv v in
-              ASLS.A.state_add st pstate v
+              ASLS.A.state_add st _nzcv v
           | _ -> st
         in
         let regq = AArch64Base.ResAddr and resaddr = global_loc "RESADDR" in

herd/ASLSem.ml

@@ -309,17 +309,17 @@ module Make (C : Config) = struct
             let* v1 = m1 () and* v2 = m2 () and* v = to_int_signed v in
             M.op3 Op.If v v1 v2
 
-    (* Any access to PSTATE emits an access to NZCV.
+    (* Any access to `_NZCV` emits an access to NZCV.
      * Notice that the value is casted into an integer.
      *)
-    let is_pstate x scope =
-      match (x, scope) with "PSTATE", AST.Scope_Global -> true | _ -> false
+    let is_nzcv x scope =
+      match (x, scope) with "_NZCV", AST.Scope_Global -> true | _ -> false
 
     let is_resaddr x scope =
       match (x, scope) with "RESADDR", AST.Scope_Global -> true | _ -> false
 
     let loc_of_scoped_id ii x scope =
-      if is_pstate x scope then
+      if is_nzcv x scope then
         A.Location_reg (ii.A.proc, ASLBase.ArchReg AArch64Base.NZCV)
       else if is_resaddr x scope then
         A.Location_reg (ii.A.proc, ASLBase.ArchReg AArch64Base.ResAddr)
@@ -331,7 +331,7 @@ module Make (C : Config) = struct
         let action = Act.Access (dir, loc, v, MachSize.Quad, aneutral) in
         M.mk_singleton_es action (use_ii_with_poi ii poi)
       in
-      if is_pstate x scope then M.op1 (Op.ArchOp1 ASLOp.ToIntU) v >>= m else m v
+      if is_nzcv x scope then M.op1 (Op.ArchOp1 ASLOp.ToIntU) v >>= m else m v
 
     let on_write_identifier = on_access_identifier Dir.W
     and on_read_identifier = on_access_identifier Dir.R