From 4e242912105047e96dda58155a4fdb664f57ceaa Mon Sep 17 00:00:00 2001 From: Luc Maranget Date: Tue, 8 Oct 2024 17:23:58 +0200 Subject: [PATCH] [herd,asl,vmsa] Hardware management of the access flag Very slow... Uses a lot of memory... --- asllib/Interpreter.ml | 4 +- asllib/bitvector.ml | 2 + asllib/bitvector.mli | 10 +++- asllib/env.ml | 4 +- asllib/env.mli | 4 +- herd/AArch64ASLSem.ml | 31 ++++++------ herd/AArch64Sem.ml | 5 +- herd/ASLParseTest.ml | 11 ++-- herd/ASLSem.ml | 43 +++++++++++----- herd/libdir/asl-pseudocode/patches-vmsa.asl | 56 +++++++++++++++++++-- herd/libdir/asl-pseudocode/physmem-vmsa.asl | 2 +- lib/ASLOp.ml | 12 ++++- lib/ASLScalar.ml | 12 ++++- 13 files changed, 149 insertions(+), 47 deletions(-) diff --git a/asllib/Interpreter.ml b/asllib/Interpreter.ml index 0680317ba..7cfd4f114 100644 --- a/asllib/Interpreter.ml +++ b/asllib/Interpreter.ml @@ -974,7 +974,7 @@ module Make (B : Backend.S) (C : Config) = struct (* Begin EvalSRepeat *) | S_Repeat (body, e, _limit) -> let*> env1 = eval_block env body in - let env2 = IEnv.tick_push_bis env1 in + let env2 = IEnv.tick_push_bis env1 1 in eval_loop false env2 e body |: SemanticsRule.SRepeat (* End *) (* Begin EvalSFor *) @@ -984,7 +984,7 @@ module Make (B : Backend.S) (C : Config) = struct (* By typing *) let undet = B.is_undetermined start_v || B.is_undetermined end_v in let*| env1 = declare_local_identifier env index_name start_v in - let env2 = if undet then IEnv.tick_push_bis env1 else env1 in + let env2 = if undet then IEnv.tick_push_bis env1 1 else env1 in let loop_msg = if undet then Printf.sprintf "for %s" index_name else diff --git a/asllib/bitvector.ml b/asllib/bitvector.ml index 3b8d04851..89eb5f135 100644 --- a/asllib/bitvector.ml +++ b/asllib/bitvector.ml @@ -557,11 +557,13 @@ let ones length = let zero = zeros 1 let one = ones 1 let empty = (0, "") +let is_zero = equal zero let is_zeros bv = let _length, data = remask bv in string_for_all (( = ) char_0) data +let is_one = equal one let is_ones bv = length bv |> ones |> equal bv type mask = { diff --git a/asllib/bitvector.mli b/asllib/bitvector.mli index 414f66f69..f47330088 100644 --- a/asllib/bitvector.mli +++ b/asllib/bitvector.mli @@ -31,11 +31,17 @@ val length : t -> int (* --------------------------------------------------------------------------*) (** {2 Constructors} *) +val zero : t +(** A length 1 bitvector with a 0 bit inside. *) + +val is_zero : t -> bool +(** zero predicate *) + val one : t (** A length 1 bitvector with a 1 bit inside. *) -val zero : t -(** A length 1 bitvector with a 0 bit inside. *) +val is_one : t -> bool +(** one predicate *) val empty : t (** A length 0 bitvector. *) diff --git a/asllib/env.ml b/asllib/env.ml index aa0e7ba13..df74065fe 100644 --- a/asllib/env.ml +++ b/asllib/env.ml @@ -73,9 +73,9 @@ module RunTime (C : RunTimeConf) = struct (** [tick_push env] is [env] with [C.unroll] pushed on its unrolling stack. *) let tick_push env = set_unroll env (C.unroll :: env.local.unroll) - (** [tick_push_bis env] is [env] with [C.unroll -1] pushed on its unrolling + (** [tick_push_bis env k] is [env] with [C.unroll-k] pushed on its unrolling stack. *) - let tick_push_bis env = set_unroll env ((C.unroll - 1) :: env.local.unroll) + let tick_push_bis env k = set_unroll env ((C.unroll - k) :: env.local.unroll) (** [tick_pop env] is [env] with removed the unrolling stack first element. *) let tick_pop env = diff --git a/asllib/env.mli b/asllib/env.mli index c099fa813..1e70ce0c1 100644 --- a/asllib/env.mli +++ b/asllib/env.mli @@ -112,9 +112,9 @@ module RunTime (C : RunTimeConf) : sig (** Push a new unrolling counter on the stack. The associated loop will be unrolled [C.unroll] times. *) - val tick_push_bis : env -> env + val tick_push_bis : env -> int -> env (** Push a new unrolling counter on the stack. The associated loop will be - unrolled [C.unroll - 1] times. *) + unrolled [C.unroll - k] times. *) val tick_pop : env -> env (** Discards the last unrolling counter of the stack. *) diff --git a/herd/AArch64ASLSem.ml b/herd/AArch64ASLSem.ml index 169784cf8..a5e097920 100644 --- a/herd/AArch64ASLSem.ml +++ b/herd/AArch64ASLSem.ml @@ -57,18 +57,21 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : [ aarch64_iico_ctrl; aarch64_iico_data; aarch64_iico_order ] module ASLConf = struct - include TopConf.C + module C = struct + include TopConf.C + module PC = struct + include TopConf.C.PC - module PC = struct - include TopConf.C.PC - - let doshow = aarch64_iico - let showevents = PrettyConf.AllEvents - let showpo = true - let showraw = aarch64_iico + let doshow = aarch64_iico + let showevents = PrettyConf.AllEvents + let showpo = true + let showraw = aarch64_iico + end + let variant = function Variant.ASL_AArch64 -> true | c -> variant c end - let variant = function Variant.ASL_AArch64 -> true | c -> variant c + let libfind = TopConf.C.libfind + let dirty = TopConf.dirty end module ASLS = ASLSem.Make (ASLConf) @@ -79,7 +82,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : module ASLTH = Test_herd.Make (ASLS.A) module MCConf = struct - include ASLConf + include ASLConf.C let byte = SZ.byte let dirty = TopConf.dirty @@ -1154,12 +1157,12 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : let check_event_structure model = let module MemConfig = struct - include ASLConf + include ASLConf.C let model = model let bell_model_info = None - let debug = ASLConf.debug.Debug_herd.barrier - let debug_files = ASLConf.debug.Debug_herd.files + let debug = ASLConf.C.debug.Debug_herd.barrier + let debug_files = ASLConf.C.debug.Debug_herd.files let showsome = true let skipchecks = StringSet.empty let strictskip = true @@ -1287,6 +1290,6 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : | [] -> Warn.fatal "No possible ASL execution." | h :: t -> List.fold_left M.altT h t) - let spurious_setaf _ = assert false + let spurious_setaf _ = M.unitT () end end diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index a6e198835..74a39161c 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -5,7 +5,8 @@ (* Luc Maranget, INRIA Paris-Rocquencourt, France. *) (* *) (* Copyright 2015-present Institut National de Recherche en Informatique et *) -(* en Automatique, ARM Ltd and the authors. All rights reserved. *) +(* en Automatique, ARM Ltd and the authoes + rs. All rights reserved. *) (* *) (* This software is governed by the CeCILL-B license under French law and *) (* abiding by the rules of distribution of free software. You can use, *) @@ -863,7 +864,7 @@ module Make and hd = dirty.hd proc in let ha = ha || hd in (* As far as we know hd => ha *) let mfault (_,ipte) m = - let open FaultType.AArch64 in + let open FaultType.AArch64 in (is_zero ipte.valid_v) >>= (fun c -> M.choiceT c diff --git a/herd/ASLParseTest.ml b/herd/ASLParseTest.ml index 78195a819..0bf18d2f4 100644 --- a/herd/ASLParseTest.ml +++ b/herd/ASLParseTest.ml @@ -33,6 +33,11 @@ module Make (Conf : RunTest.Config) (ModelConfig : MemCat.Config) = struct module ArchConfig = SemExtra.ConfigToArchConfig (Conf) + module Conf = struct + module C = Conf + let libfind = Conf.libfind + let dirty = None + end module ASLS = ASLSem.Make (Conf) module ASLA = ASLS.A @@ -44,14 +49,14 @@ module Make (Conf : RunTest.Config) (ModelConfig : MemCat.Config) = struct let parser = let version = - if Conf.variant (Variant.ASLVersion `ASLv0) then `ASLv0 else `ASLv1 + if Conf.C.variant (Variant.ASLVersion `ASLv0) then `ASLv0 else `ASLv1 in ASLBase.asl_generic_parser version end module ASLM = MemCat.Make (ModelConfig) (ASLS) - module P = GenParser.Make (Conf) (ASLA) (ASLLexParse) - module X = RunTest.Make (ASLS) (P) (ASLM) (Conf) + module P = GenParser.Make (Conf.C) (ASLA) (ASLLexParse) + module X = RunTest.Make (ASLS) (P) (ASLM) (Conf.C) let run = X.run end diff --git a/herd/ASLSem.ml b/herd/ASLSem.ml index d6788b26b..4cca51084 100644 --- a/herd/ASLSem.ml +++ b/herd/ASLSem.ml @@ -79,18 +79,20 @@ module AST = Asllib.AST module ASTUtils = Asllib.ASTUtils module type Config = sig - include Sem.Config - + module C : Sem.Config + val dirty : DirtyBit.t option val libfind : string -> string end -module Make (C : Config) = struct +module Make (Conf : Config) = struct module V = ASLValue.V + let variant = Conf.C.variant + module ConfLoc = struct - include SemExtra.ConfigToArchConfig (C) + include SemExtra.ConfigToArchConfig (Conf.C) - let default_to_symb = C.variant Variant.ASL + let default_to_symb = variant Variant.ASL end module ASL64AH = struct @@ -101,12 +103,12 @@ module Make (C : Config) = struct end module Act = ASLAction.Make (ASL64AH) - include SemExtra.Make (C) (ASL64AH) (Act) + include SemExtra.Make (Conf.C) (ASL64AH) (Act) module TypeCheck = Asllib.Typing.Annotate (struct let check : Asllib.Typing.strictness = - if C.variant (Variant.ASLType `Warn) then `Warn - else if C.variant (Variant.ASLType `TypeCheck) then `TypeCheck + if variant (Variant.ASLType `Warn) then `Warn + else if variant (Variant.ASLType `TypeCheck) then `TypeCheck else `Silence let output_format = Asllib.Error.Silence @@ -114,13 +116,13 @@ module Make (C : Config) = struct module ASLInterpreterConfig = struct let unroll = - match C.unroll with None -> Opts.unroll_default `ASL | Some u -> u + match Conf.C.unroll with None -> Opts.unroll_default `ASL | Some u -> u module Instr = Asllib.Instrumentation.SemanticsNoInstr end - let is_experimental = C.variant Variant.ASLExperimental - and is_kvm = C.variant Variant.VMSA + let is_experimental = variant Variant.ASLExperimental + and is_kvm = variant Variant.VMSA let barriers = [] let isync = None let atomic_pair_allowed _ _ = true @@ -597,6 +599,10 @@ module Make (C : Config) = struct (use_ii_with_poi ii poi) >>! [] + let write_pte ii addr_m val_m = + do_write_memory ii addr_m (M.unitT (V.intToV 64)) val_m + aneutral (AArch64Explicit.(NExp AF)) apte + let write_memory ii addr_m datasize_m value_m = do_write_memory ii addr_m datasize_m value_m aneutral aexp avir @@ -657,6 +663,14 @@ module Make (C : Config) = struct and loc = A.Location_global loc in M.mk_singleton_es (Act.Fault (ii,loc,d,ft)) ii >>! [] + let get_ha (ii,_) () = + let dirty = + match Conf.dirty with + | None -> DirtyBit.soft + | Some f -> f in + let ha = dirty.DirtyBit.ha ii.A.proc in + V.Val (Constant.Concrete (ASLScalar.bv_of_bool ha)) |> M.unitT + (**************************************************************************) (* ASL environment *) (**************************************************************************) @@ -815,6 +829,9 @@ module Make (C : Config) = struct p3 "DataAbortPrimitive" ("addr",bv_64) ("write",boolean) ("statuscode",integer) data_abort_fault; + p0r "GetHaPrimitive" ~returns:(bv_lit 1) get_ha; + p2 "WritePtePrimitive" + ("addr", bv_64) ("data",bv_64) write_pte; (* Translations *) p1r "UInt" ~parameters:[ ("N", None) ] @@ -856,7 +873,7 @@ module Make (C : Config) = struct in let build ?ast_type version fname = Filename.concat "asl-pseudocode" fname - |> C.libfind + |> Conf.libfind |> ASLBase.build_ast_from_file ?ast_type version in let patches = @@ -938,7 +955,7 @@ module Make (C : Config) = struct in fun () -> Lazy.force - @@ if C.variant Variant.ASL_AArch64 then if_asl_aarch64 else otherwise + @@ if variant Variant.ASL_AArch64 then if_asl_aarch64 else otherwise (**************************************************************************) (* Execution *) diff --git a/herd/libdir/asl-pseudocode/patches-vmsa.asl b/herd/libdir/asl-pseudocode/patches-vmsa.asl index 96cecbba8..bb2dc8517 100644 --- a/herd/libdir/asl-pseudocode/patches-vmsa.asl +++ b/herd/libdir/asl-pseudocode/patches-vmsa.asl @@ -1,9 +1,9 @@ // AArch64.S1Enabled() // =================== // Determine if stage 1 is enabled for the access type for this translation regime -// Stage 1 is the onlt translation regime implemented +// Stage 1 is the only translation regime implemented -func AArch64_S1Enabled(regme : Regime,acctype : AccessType) => boolean +func AArch64_S1Enabled(regime : Regime,acctype : AccessType) => boolean begin return TRUE; end @@ -191,14 +191,25 @@ end // Perform HW update of table descriptor as an atomic operation // Modified -> disabled at the moment -func AArch64_MemSwapTableDesc +func No_AArch64_MemSwapTableDesc (fault_in:FaultRecord,prev_desc:bits(N),new_desc:bits(N), ee:bit,descaccess:AccessDescriptor,descpaddr:AddressDescriptor) => (FaultRecord, bits(N)) begin + __debug__('1111'); return (fault_in,new_desc); end +func AArch64_MemSwapTableDesc + (fault_in:FaultRecord,prev_desc:bits(N),new_desc:bits(N), + ee:bit,descaccess:AccessDescriptor,descpaddr:AddressDescriptor) +=> (FaultRecord, bits(N)) +begin + let addr = descpaddr.paddress.address; + WritePtePrimitive(addr,new_desc); + return (fault_in,new_desc); +end + // AArch64.DataAbort() // =================== @@ -263,3 +274,42 @@ begin // assert FALSE; return; end + +// +// Previous walkparams +// {aie:'0',amec:'0',cmow:'0',d128:'0',dc:'0',dct:'0',disch:'0',ds:'0', +// e0pd:'0',ee:'0',emec:'0',epan:'0',fng:'0',ha:'0',haft:'0',hd:'0', +// hpd:'0',irgn:'01', +// mair:'0000000000000000000000000000000000000000000000000000000000000000', +// mair2:'0000000000000000000000000000000000000000000000000000000000000000', +// mtx:'0',nfd:'0',ntlsmd:'1',nv1:'0',orgn:'01',pie:'0',pir:'',pire0:'', +// pnch:'0',ps:'100',sh:'11',sif:'0',skl:'00',t0sz:'000',t1sz:'000', +// tbi:'0',tbid:'0',tgx:2,txsz:'010000',uwxn:'0',wxn:'0',} + + +// AArch64.GetS1TTWParams() +// ======================== +// Returns stage 1 translation table walk parameters from respective controlling +// System registers. +// Luc: we assume EL10 regime, return minimal parameters +func AArch64_GetS1TTWParams + (regime:Regime, ss:SecurityState, va:bits(64)) + => S1TTWParams +begin + var walkparams : S1TTWParams; + assert (regime == Regime_EL10); + walkparams.ha = GetHaPrimitive(); +// __debug__(walkparams); + return walkparams; +end + + +// AArch64.S1TxSZFaults() +// ====================== +// Detect whether configuration of stage 1 TxSZ field generates a fault +// Luc: Override: does not occur, never. + +func AArch64_S1TxSZFaults (regime:Regime,walkparams:S1TTWParams) => boolean +begin + return FALSE; +end diff --git a/herd/libdir/asl-pseudocode/physmem-vmsa.asl b/herd/libdir/asl-pseudocode/physmem-vmsa.asl index 42f9cc3a0..03bf35de8 100644 --- a/herd/libdir/asl-pseudocode/physmem-vmsa.asl +++ b/herd/libdir/asl-pseudocode/physmem-vmsa.asl @@ -19,7 +19,7 @@ begin else eventaccess = PHY_PTE; end -// No, we can write, physically. +// Now, we can write, physically. write_memory_gen (desc.paddress.address, size*8, value,accdesc,eventaccess); return PhysMemRetStatus { statuscode = Fault_None, diff --git a/lib/ASLOp.ml b/lib/ASLOp.ml index d2e3d6bab..c1816852a 100644 --- a/lib/ASLOp.ml +++ b/lib/ASLOp.ml @@ -176,8 +176,16 @@ let do_op op c1 c2 = match c1 with | Constant.PteVal _ -> return c1 | _ -> set_slice positions c1 c2 - end else - set_slice positions c1 c2 + end else match c1,c2 with + | Constant.PteVal pte,Constant.Concrete s2 -> + begin match positions with + | [10] -> + let af = ASLScalar.bit_of_bv s2 in + Constant.PteVal { pte with AArch64PteVal.af;} |> return + | _ -> + set_slice positions c1 c2 + end + | _ -> set_slice positions c1 c2 let do_op1 op cst = match op with diff --git a/lib/ASLScalar.ml b/lib/ASLScalar.ml index 995119469..69687fd1f 100644 --- a/lib/ASLScalar.ml +++ b/lib/ASLScalar.ml @@ -299,7 +299,6 @@ let to_caml_bool = function let as_bool sc = Some (to_caml_bool sc) let convert_to_bool sc = S_Bool (to_caml_bool sc) - let convert_to_bv = function | S_BitVector _ as bv -> bv | S_Int i -> S_BitVector (BV.of_z 64 i) @@ -352,6 +351,17 @@ let do_bv_of_bit = function let bv_of_bit b = S_BitVector (do_bv_of_bit b) +and bit_of_bv s = + let bv = + match s with + | S_BitVector bv -> bv + | S_Bool true -> BV.one + | S_Bool false -> BV.zero + | S_Int z -> if Z.equal Z.zero z then BV.zero else BV.one in + if BV.is_zero bv then 0 + else if BV.is_one bv then 1 + else Warn.fatal "bit_of_bv on illegal input %s" (BV.to_string bv) + let bv_of_bits bs = let bv = List.map do_bv_of_bit bs |> BV.concat in S_BitVector bv