From b4e6e0711b5e84501f1ad8da75ab64c02a503d05 Mon Sep 17 00:00:00 2001 From: Luc Maranget Date: Mon, 25 Mar 2024 15:19:12 +0100 Subject: [PATCH 1/2] [asl] Check get and set field(s) for getters and setters --- asllib/Typing.ml | 210 +++++++++++++++++++++++++++++++++++------------ 1 file changed, 159 insertions(+), 51 deletions(-) diff --git a/asllib/Typing.ml b/asllib/Typing.ml index ac1f2714e..9c15494cc 100644 --- a/asllib/Typing.ml +++ b/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 From 50436ed0332d6111cc874cf121528c24543005e7 Mon Sep 17 00:00:00 2001 From: Luc Maranget Date: Mon, 25 Mar 2024 17:48:02 +0100 Subject: [PATCH 2/2] [asl] Partition PSTATE accesses. Accesses to PSTATE get partitioned: + Accesses to the N,Z,C and V fields are to variable `_NZCV`. + Other accesses and to the variable `_PSTATE`. We use the previous reduction of some get and set fields to function calls. Overall the trick works but remains quite brittle. 1. _NZCV is targetted when all fields are in {N,Z,C,V}. 2. Getters are setters are defined only up to four bit accesses. --- asllib/Interpreter.ml | 7 +- herd/AArch64ASLSem.ml | 4 +- herd/ASLSem.ml | 10 +-- herd/libdir/asl-pseudocode/patches.asl | 91 +++++++++++++++++++++++++- 4 files changed, 103 insertions(+), 9 deletions(-) diff --git a/asllib/Interpreter.ml b/asllib/Interpreter.ml index 7935a6bc3..18e1405e5 100644 --- a/asllib/Interpreter.ml +++ b/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 diff --git a/herd/AArch64ASLSem.ml b/herd/AArch64ASLSem.ml index bf26dd359..a0340d48d 100644 --- a/herd/AArch64ASLSem.ml +++ b/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 diff --git a/herd/ASLSem.ml b/herd/ASLSem.ml index 9b394bd11..3cf1c2fed 100644 --- a/herd/ASLSem.ml +++ b/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 diff --git a/herd/libdir/asl-pseudocode/patches.asl b/herd/libdir/asl-pseudocode/patches.asl index a2e2ddc86..8dbe38dbe 100644 --- a/herd/libdir/asl-pseudocode/patches.asl +++ b/herd/libdir/asl-pseudocode/patches.asl @@ -89,7 +89,96 @@ type ProcState of bits(64) { [47:42] M // Mode field [AArch32 only] }; -var PSTATE : ProcState; +var _PSTATE : ProcState; +var _NZCV : ProcState; + +func isNZCV(n:integer) => boolean +begin + return 0 <= n && n < 4 ; +end + +getter PSTATE[] => ProcState +begin + return _PSTATE; +end + +setter PSTATE[] = v : ProcState +begin + _PSTATE = v; +end + +getter PSTATE[n:integer] => bits(1) +begin + if isNZCV(n) then + return _NZCV[n]; + else + return _PSTATE[n]; + end +end + +setter PSTATE[n:integer] = v : bits(1) +begin + if isNZCV(n) then + _NZCV[n] = v; + else + _PSTATE[n] = v; + end +end + + +getter PSTATE[n:integer,m:integer] => bits(2) +begin + if isNZCV(n) && isNZCV(m) then + return _NZCV[n,m]; + else + return _PSTATE[n,m]; + end +end + +setter PSTATE[n:integer,m:integer] = v : bits(2) +begin + if isNZCV(n) && isNZCV(m) then + _NZCV[n,m] = v; + else + _PSTATE[n,m] = v; + end +end + +getter PSTATE[n:integer,m:integer,o:integer] => bits(3) +begin + if isNZCV(n) && isNZCV(m) && isNZCV(o) then + return _NZCV[n,m,o]; + else + return _PSTATE[n,m,o]; + end +end + +setter PSTATE[n:integer,m:integer,o:integer] = v : bits(3) +begin + if isNZCV(n) && isNZCV(m) && isNZCV(o) then + _NZCV[n,m,o] = v; + else + _PSTATE[n,m,o] = v; + end +end + +getter PSTATE[n:integer,m:integer,o:integer,p:integer] => bits(4) +begin + if isNZCV(n) && isNZCV(m) && isNZCV(o) && isNZCV(p) then + return _NZCV[n,m,o,p]; + else + return _PSTATE[n,m,o,p]; + end +end + +setter PSTATE[n:integer,m:integer,o:integer,p:integer] = v : bits(4) +begin + if isNZCV(n) && isNZCV(m) && isNZCV(o) && isNZCV(p) then + _NZCV[n,m,o,p] = v; + else + _PSTATE[n,m,o,p] = v; + end +end // GenerateAddress() // =================