From 4c177b09af4fa0540df9a645602dc3b6a1bdb167 Mon Sep 17 00:00:00 2001 From: Luc Maranget Date: Wed, 4 Sep 2024 16:55:33 +0200 Subject: [PATCH] [herd,asl] PTE accesses in ASL+VMSA mode. Notice that page table are accessed in PTE2 mode. That is, PTE accesses undergo the vrtual to physical translation, as the mode that is naturally compatible with existing ASL code. --- herd/AArch64ASLSem.ml | 3 +- herd/AArch64Sem.ml | 2 +- herd/ASLSem.ml | 62 ++++++++++++------- herd/Pretty.ml | 1 - herd/eventsMonad.ml | 5 +- .../libdir/asl-pseudocode/implementations.asl | 15 ++++- herd/libdir/asl-pseudocode/physmem-std.asl | 4 +- herd/libdir/asl-pseudocode/physmem-vmsa.asl | 22 ++++++- herd/mem.ml | 4 +- lib/ASLOp.ml | 2 + lib/ASLScalar.ml | 15 ++--- lib/genParser.ml | 1 - 12 files changed, 93 insertions(+), 43 deletions(-) diff --git a/herd/AArch64ASLSem.ml b/herd/AArch64ASLSem.ml index 270581596..ad9291bd6 100644 --- a/herd/AArch64ASLSem.ml +++ b/herd/AArch64ASLSem.ml @@ -737,8 +737,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : None let tr_cst tr = - Constant.map tr - (fun _ -> Warn.fatal "Cannot translate PTE") + Constant.map tr Misc.identity (fun _ -> Warn.fatal "Cannot translate instruction") let aarch64_to_asl_bv = function diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index b613701ea..f6cda6c93 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -38,7 +38,7 @@ module Make let neon = C.variant Variant.Neon || sve let kvm = C.variant Variant.VMSA let is_branching = kvm && not (C.variant Variant.NoPteBranch) - let pte2 = kvm && C.variant Variant.PTE2 + let pte2 = kvm && (C.variant Variant.PTE2 || C.variant Variant.ASL) let do_cu = C.variant Variant.ConstrainedUnpredictable let self = C.variant Variant.Ifetch diff --git a/herd/ASLSem.ml b/herd/ASLSem.ml index f99fc02f2..1873ad130 100644 --- a/herd/ASLSem.ml +++ b/herd/ASLSem.ml @@ -250,6 +250,18 @@ module Make (C : Config) = struct in an + let access_to_access acc = + let open Access in + match v_as_int acc with + | 0 -> REG + | 1 -> VIR + | 2 -> PHY + | 3 -> PTE + | 4 -> TLB + | 5 -> TAG + | 6 -> PHY_PTE + | i -> Warn.fatal "Bad access code from ASL: %d" i + let wrap_op1_symb_as_var op1 = function | V.Val (Constant.Symbolic _) as v -> let v' = V.fresh_var () in @@ -555,7 +567,7 @@ module Make (C : Config) = struct (use_ii_with_poi ii poi) let write_pc (ii,poi) v_m = - let* v = v_m >>= to_int_unsigned in + let* v = v_m >>= to_aarch64_val in write_loc MachSize.Quad (loc_pc ii) v aneutral aexp areg (use_ii_with_poi ii poi) >>! [] @@ -572,11 +584,10 @@ module Make (C : Config) = struct do_read_memory ii (M.unitT addr) (M.unitT (V.intToV 64)) aneutral (AArch64Explicit.(NExp Other)) apte - let vir_or_phy = if is_kvm then Access.PHY else Access.VIR - - let read_memory_gen ii addr_m datasize_m accdesc_m = - let* accdesc = accdesc_m in - do_read_memory ii addr_m datasize_m (accdesc_to_annot true accdesc) aexp vir_or_phy + let read_memory_gen ii addr_m datasize_m accdesc_m access_m = + let* accdesc = accdesc_m and* access = access_m in + do_read_memory ii addr_m datasize_m (accdesc_to_annot true accdesc) + aexp (access_to_access access) let do_write_memory (ii, poi) addr_m datasize_m value_m an aexp acc = let value_m = M.as_data_port value_m in @@ -589,10 +600,10 @@ module Make (C : Config) = struct let write_memory ii addr_m datasize_m value_m = do_write_memory ii addr_m datasize_m value_m aneutral aexp avir - let write_memory_gen ii addr_m datasize_m value_m accdesc_m = - let* accdesc = accdesc_m in + let write_memory_gen ii addr_m datasize_m value_m accdesc_m access_m = + let* accdesc = accdesc_m and* access = access_m in do_write_memory ii addr_m datasize_m value_m - (accdesc_to_annot false accdesc) aexp vir_or_phy + (accdesc_to_annot false accdesc) aexp (access_to_access access) let loc_sp ii = A.Location_reg (ii.A.proc, ASLBase.ArchReg AArch64Base.SP) @@ -601,7 +612,7 @@ module Make (C : Config) = struct (use_ii_with_poi ii poi) let write_sp (ii, poi) v_m = - let* v = v_m >>= to_int_signed in + let* v = v_m >>= to_aarch64_val in write_loc MachSize.Quad (loc_sp ii) v aneutral aexp areg (use_ii_with_poi ii poi) >>! [] @@ -609,6 +620,10 @@ module Make (C : Config) = struct let uint _ bv_m = bv_m >>= to_int_unsigned let sint _ bv_m = bv_m >>= to_int_signed let processor_id (ii, _poi) () = return (V.intToV ii.A.proc) + let is_virtual _ addr_m = + addr_m + >>= M.op1 Op.IsVirtual + >>= M.op1 (Op.ArchOp1 ASLOp.ToBool) let can_predict_from _ v_m w_m = let diff_case = v_m in @@ -718,22 +733,22 @@ module Make (C : Config) = struct in build_primitive ~args:[ arg1; arg2; arg3 ] ?parameters name f - (** Build a primitive with arity 3 and a return value. *) - let p3r name arg1 arg2 arg3 ~returns ?parameters f = + (** Build a primitive with arity 4 and a return value. *) + let p4r name arg1 arg2 arg3 arg4 ~returns ?parameters f = let f ii_env = function - | [ v1; v2; v3 ] -> return [ f ii_env v1 v2 v3 ] + | [ v1; v2; v3; v4; ] -> return [ f ii_env v1 v2 v3 v4 ] | _ -> Warn.fatal "Arity error for function %s." name in - build_primitive ?returns:(Some returns) ~args:[ arg1; arg2; arg3 ] + build_primitive ?returns:(Some returns) ~args:[ arg1; arg2; arg3; arg4 ] ?parameters name f - (** Build a primitive with arity 4 and no return value. *) - let p4 name arg1 arg2 arg3 arg4 ?parameters f = + (** Build a primitive with arity 5 and no return value. *) + let p5 name arg1 arg2 arg3 arg4 arg5 ?parameters f = let f ii_env = function - | [ v1; v2; v3; v4 ] -> f ii_env v1 v2 v3 v4 + | [ v1; v2; v3; v4; v5; ] -> f ii_env v1 v2 v3 v4 v5 | _ -> Warn.fatal "Arity error for function %s." name in - build_primitive ~args:[ arg1; arg2; arg3; arg4 ] ?parameters name f + build_primitive ~args:[ arg1; arg2; arg3; arg4; arg5; ] ?parameters name f (* Primitives *) let extra_funcs = @@ -777,15 +792,16 @@ module Make (C : Config) = struct (* Memory *) p2r "read_memory" ("addr", bv_64) ("size", integer) ~returns:bv_64 read_memory; - p3r "read_memory_gen" ("addr", bv_64) ("size", integer) - ("accdesc", t_named "AccessDescriptor") + p4r "read_memory_gen" ("addr", bv_64) ("size", integer) + ("accdesc", t_named "AccessDescriptor") ("access", t_named "EventAccess") ~returns:bv_64 read_memory_gen; p3 "write_memory" ("addr", bv_64) ("size", integer) ("data", bv_var "size") write_memory; - p4 "write_memory_gen" ("addr", bv_64) ("size", integer) + p5 "write_memory_gen" ("addr", bv_64) ("size", integer) ("data", bv_var "size") ("accdesc", t_named "AccessDescriptor") + ("access", t_named "EventAccess") write_memory_gen; (* VMSA *) p1r "ComputePtePrimitive" @@ -808,8 +824,10 @@ module Make (C : Config) = struct ~parameters:[ ("N", None) ] ("x", bv_var "N") ~returns:sint_returns sint; - (* Misc *) +(* Misc *) p0r "ProcessorID" ~returns:integer processor_id; + p1r "IsVirtual" + ("addr",bv_64) ~returns:boolean is_virtual; p2r "CanPredictFrom" ~parameters:[ ("N", None) ] ("predicted", bv_var "N") diff --git a/herd/Pretty.ml b/herd/Pretty.ml index 66697c1d7..8ccdafa87 100644 --- a/herd/Pretty.ml +++ b/herd/Pretty.ml @@ -1594,7 +1594,6 @@ module Make (S:SemExtra.S) : S with module S = S = struct module SHOW = Show.Make(PC) let show_es_rfm test es rfm = - prerr_endline "Bingo" ; SHOW.show (fun chan -> dump_es_rfm chan test es rfm) let show_legend test legend conc ?(sets = StringMap.empty) vbs = diff --git a/herd/eventsMonad.ml b/herd/eventsMonad.ml index 2450d3344..de70f41ad 100644 --- a/herd/eventsMonad.ml +++ b/herd/eventsMonad.ml @@ -1266,6 +1266,9 @@ Monad type: let memtag = C.variant Variant.MemTag let morello = C.variant Variant.Morello let kvm = C.variant Variant.VMSA + let is_asl = C.variant Variant.ASL + (* Combining the ASL and VMSA variant implies PTE2 mode *) + let is_pte2 = kvm && (is_asl || C.variant Variant.PTE2) module AM = A.Mixed(SZ) @@ -1520,7 +1523,7 @@ Monad type: else (pte_loc s,default_pteval s)::env) virt env in let env = - if C.variant Variant.PTE2 then + if is_pte2 then List.fold_right (fun (loc,_ as bd) env -> match loc with | A.Location_global (V.Val (Symbolic (System (PTE,s)))) diff --git a/herd/libdir/asl-pseudocode/implementations.asl b/herd/libdir/asl-pseudocode/implementations.asl index df55f2023..1b2b0a16d 100644 --- a/herd/libdir/asl-pseudocode/implementations.asl +++ b/herd/libdir/asl-pseudocode/implementations.asl @@ -607,4 +607,17 @@ end func EndOfInstruction() begin return; -end \ No newline at end of file +end + +// Type of underlying accesses (same order as lib/access.mli), +// as recorder un events. + +type EventAccess of enumeration { + REG, + VIR, + PHY, + PTE, + TLB, + TAG, + PHY_PTE, +}; diff --git a/herd/libdir/asl-pseudocode/physmem-std.asl b/herd/libdir/asl-pseudocode/physmem-std.asl index a725222ad..27b2e0271 100644 --- a/herd/libdir/asl-pseudocode/physmem-std.asl +++ b/herd/libdir/asl-pseudocode/physmem-std.asl @@ -9,7 +9,7 @@ func PhysMemWrite( value::bits(8*size) ) => PhysMemRetStatus begin - write_memory_gen (desc.vaddress, size*8, value,accdesc); + write_memory_gen (desc.vaddress, size*8, value,accdesc,VIR); return PhysMemRetStatus { statuscode = Fault_None, extflag = '0', @@ -27,7 +27,7 @@ func PhysMemRead( ) => (PhysMemRetStatus, bits(8*size)) begin let value = - read_memory_gen (desc.vaddress,size*8,accdesc)[8*size-1:0]; + read_memory_gen (desc.vaddress,size*8,accdesc,VIR)[8*size-1:0]; let ret_status = PhysMemRetStatus { statuscode = Fault_None, extflag = '0', diff --git a/herd/libdir/asl-pseudocode/physmem-vmsa.asl b/herd/libdir/asl-pseudocode/physmem-vmsa.asl index a0adb9920..42f9cc3a0 100644 --- a/herd/libdir/asl-pseudocode/physmem-vmsa.asl +++ b/herd/libdir/asl-pseudocode/physmem-vmsa.asl @@ -9,7 +9,18 @@ func PhysMemWrite( value::bits(8*size) ) => PhysMemRetStatus begin - write_memory_gen (desc.paddress.address, size*8, value,accdesc); +// Event level access, there differ for standard (virtual) addresses +// and PTE's. +// We cannot use conditional expresssion, +// because write_memory_gen needs a concrete argument. + var eventaccess : EventAccess; + if IsVirtual(desc.vaddress) then + eventaccess = PHY; + else + eventaccess = PHY_PTE; + end +// No, we can write, physically. + write_memory_gen (desc.paddress.address, size*8, value,accdesc,eventaccess); return PhysMemRetStatus { statuscode = Fault_None, extflag = '0', @@ -26,8 +37,15 @@ func PhysMemRead( accdesc::AccessDescriptor ) => (PhysMemRetStatus, bits(8*size)) begin + var eventaccess : EventAccess; + if IsVirtual(desc.vaddress) then + eventaccess = PHY; + else + eventaccess = PHY_PTE; + end let value = - read_memory_gen (desc.paddress.address,size*8,accdesc)[8*size-1:0]; + read_memory_gen + (desc.paddress.address,size*8,accdesc,eventaccess)[8*size-1:0]; let ret_status = PhysMemRetStatus { statuscode = Fault_None, extflag = '0', diff --git a/herd/mem.ml b/herd/mem.ml index 93b733a51..11c4d60ad 100644 --- a/herd/mem.ml +++ b/herd/mem.ml @@ -859,10 +859,12 @@ let match_reg_events es = let solve_regs test es csn = match do_solve_regs test es csn with - | Some (es,rfm,_) as r -> + | Some (es,rfm,cns) as r -> if C.debug.Debug_herd.solver && C.verbose > 0 then begin let module PP = Pretty.Make(S) in prerr_endline "Reg solved, direct" ; + Printf.eprintf "++++ Remaing equations:\n%s\n++++++\n%!" + (VC.pp_cnstrnts cns) ; PP.show_es_rfm test es rfm end ; r diff --git a/lib/ASLOp.ml b/lib/ASLOp.ml index cb88bfaff..d2e3d6bab 100644 --- a/lib/ASLOp.ml +++ b/lib/ASLOp.ml @@ -87,6 +87,7 @@ let pp_op1 _hexa = function | ToAArch64 -> "ToAArch64" | FromAArch64 -> "FromAArch64" + let ( let* ) = Option.bind let return c = Some c let return_concrete s = Constant.Concrete s |> return @@ -249,6 +250,7 @@ let do_op1 op cst = (* Valid *) let valid = pte.AArch64PteVal.valid in Some (Constant.Concrete (ASLScalar.bv_of_bit valid)) + | _ when is_address_mask positions -> Some cst | _ -> None end | Constant.Symbolic x -> diff --git a/lib/ASLScalar.ml b/lib/ASLScalar.ml index c92443474..cdd29e8b4 100644 --- a/lib/ASLScalar.ml +++ b/lib/ASLScalar.ml @@ -289,16 +289,13 @@ let convert_to_int_unsigned = function | S_Bool true -> S_Int Z.one | S_BitVector bv -> S_Int (BV.to_z_unsigned bv) -let as_bool = function - | S_Int i -> Some (not (Z.equal i Z.zero)) - | S_Bool b -> Some b - | S_BitVector _ -> None +let to_caml_bool = function + | S_Bool b -> b + | S_Int _|S_BitVector _ as sc -> not (is_zero sc) + +let as_bool sc = Some (to_caml_bool sc) +let convert_to_bool sc = S_Bool (to_caml_bool sc) -let convert_to_bool c = - match as_bool c with - | Some b -> S_Bool b - | None -> - Warn.fatal "ASLScalar invalid op: to_bool %s" (pp false c) let convert_to_bv = function | S_BitVector _ as bv -> bv diff --git a/lib/genParser.ml b/lib/genParser.ml index 09f63cd93..1adec85a6 100644 --- a/lib/genParser.ml +++ b/lib/genParser.ml @@ -225,7 +225,6 @@ module Make | _ -> assert false end in - if O.verbose > 0 then prerr_endline "Bingo" ; ConstrGen.map_constr map_atom cond with Not_found -> cond in { parsed with