diff --git a/catalogue/aarch64-faults/shelf.py b/catalogue/aarch64-faults/shelf.py index c7c92f6a0c..d98bcc658a 100644 --- a/catalogue/aarch64-faults/shelf.py +++ b/catalogue/aarch64-faults/shelf.py @@ -20,6 +20,8 @@ "tests/MP+dmb.st+ctrl-svc.exs1eis1.litmus", "tests/SVC-ifetch.exs1eis0.litmus", "tests/SVC-ifetch.exs1eis1.litmus", + "tests/SVC-ifetch.dic0idc0-exs1eis0.litmus", + "tests/SVC-ifetch.dic0idc0-exs1eis1.litmus", # "tests/SVC-pte.exs1eis0.litmus", # "tests/SVC-pte.exs1eis1.litmus", ] diff --git a/catalogue/aarch64-faults/tests/@all b/catalogue/aarch64-faults/tests/@all index db68176e21..3cbb3fb94c 100644 --- a/catalogue/aarch64-faults/tests/@all +++ b/catalogue/aarch64-faults/tests/@all @@ -9,5 +9,7 @@ MP+dmb.st+ctrl-svc.exs1eis0.litmus MP+dmb.st+ctrl-svc.exs1eis1.litmus SVC-ifetch.exs1eis0.litmus SVC-ifetch.exs1eis1.litmus +SVC-ifetch.dic0idc0-exs1eis0.litmus +SVC-ifetch.dic0idc0-exs1eis1.litmus SVC-pte.exs1eis0.litmus SVC-pte.exs1eis1.litmus diff --git a/catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis0.litmus b/catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis0.litmus new file mode 100644 index 0000000000..ac3d32271d --- /dev/null +++ b/catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis0.litmus @@ -0,0 +1,18 @@ +AArch64 SVC-ifetch.dic0idc0-exs1eis0.litmus +variant=ifetch,exs +{ + 0:X0=instr:"NOP"; 0:X1=P0:L2; +} + P0 | P0.F ; + STR W0,[X1] | ERET ; + DC CVAU, X1 |; + DSB ISH |; + IC IVAU, X1 |; + DSB ISH |; + SVC #0 |; +L2: |; + B L1 |; + MOV W9,#1 |; +L1: |; + +exists(0:X9=0) \ No newline at end of file diff --git a/catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis1.litmus b/catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis1.litmus new file mode 100644 index 0000000000..0661d50c71 --- /dev/null +++ b/catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis1.litmus @@ -0,0 +1,18 @@ +AArch64 SVC-ifetch.dic0idc0-exs1eis1 +variant=ifetch,exs,eis +{ + 0:X0=instr:"NOP"; 0:X1=P0:L2; +} + P0 | P0.F ; + STR W0,[X1] | ERET ; + DC CVAU, X1 |; + DSB ISH |; + IC IVAU, X1 |; + DSB ISH |; + SVC #0 |; +L2: |; + B L1 |; + MOV W9,#1 |; +L1: |; + +exists(0:X9=0) \ No newline at end of file diff --git a/catalogue/aarch64-faults/tests/kinds.txt b/catalogue/aarch64-faults/tests/kinds.txt index 3e8da42eb9..9da11e2f25 100644 --- a/catalogue/aarch64-faults/tests/kinds.txt +++ b/catalogue/aarch64-faults/tests/kinds.txt @@ -11,3 +11,5 @@ SVC-pte.exs1eis0 Allowed SVC-pte.exs1eis1 Forbid SVC-ifetch.exs1eis0 Allowed SVC-ifetch.exs1eis1 Forbid +SVC-ifetch.dic0idc0-exs1eis0 Allowed +SVC-ifetch.dic0idc0-exs1eis1 Forbid diff --git a/litmus/dumpRun.ml b/litmus/dumpRun.ml index eff24b42ba..ddd18aacd9 100644 --- a/litmus/dumpRun.ml +++ b/litmus/dumpRun.ml @@ -139,6 +139,10 @@ end = struct if flags.Flags.memtag then "memtag.o"::utils else utils in + let utils = + if flags.Flags.exs then + "exs.o"::utils + else utils in let utils = if flags.Flags.pac then "auth.o"::utils @@ -210,10 +214,11 @@ let collect_flags names = let open Flags in { pac = flags.pac || some_flags.pac; self = flags.self || some_flags.self; - memtag = flags.memtag || some_flags.memtag;} + memtag = flags.memtag || some_flags.memtag; + exs = flags.exs || some_flags.exs;} | _ -> some_flags) names - {Flags.pac=false; Flags.self=false; Flags.memtag=false} + {Flags.pac=false; Flags.self=false; Flags.memtag=false; Flags.exs=false} let run_tests names flags out_chan = diff --git a/litmus/flags.mli b/litmus/flags.mli index 971f7b477e..685575fd96 100644 --- a/litmus/flags.mli +++ b/litmus/flags.mli @@ -21,4 +21,5 @@ type t = pac : bool ; (* Requires pointer authentification *) self : bool ; (* Self modying code *) memtag : bool ; (* Requires memory tagging *) + exs : bool ; (* Requires ExS helpers *) } diff --git a/litmus/libdir/_aarch64/_exs.c b/litmus/libdir/_aarch64/_exs.c new file mode 100644 index 0000000000..6de302f5fa --- /dev/null +++ b/litmus/libdir/_aarch64/_exs.c @@ -0,0 +1,40 @@ +/****************************************************************************/ +/* the diy toolsuite */ +/* */ +/* Jade Alglave, University College London, UK. */ +/* Luc Maranget, INRIA Paris-Rocquencourt, France. */ +/* */ +/* Copyright 2026-present Institut National de Recherche en Informatique et */ +/* en Automatique and the authors. 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, */ +/* modify and/ or redistribute the software under the terms of the CeCILL-B */ +/* license as circulated by CEA, CNRS and INRIA at the following URL */ +/* "http://www.cecill.info". We also give a copy in LICENSE.txt. */ +/****************************************************************************/ +#include "kvm-headers.h" +#include "exs.h" + +#define MMFR0_EXS_SHIFT 44 +#define MMFR0_EXS_MASK 0xf + +int check_exs(const char *tname) { + uint64_t mmfr0; + asm volatile("mrs %0, ID_AA64MMFR0_EL1" : "=r" (mmfr0)); + int exs = (mmfr0 >> MMFR0_EXS_SHIFT) & MMFR0_EXS_MASK; + if (exs == 0) { + printf("Test %s, ExS not supported on this system\n", tname); + return 0; + } + return 1; +} + +void init_exs(int eis_val, int eos_val) { + uint64_t sctlr; + asm volatile("mrs %0, SCTLR_EL1" : "=r" (sctlr)); + sctlr = eis_val ? (sctlr | SCTLR_EL1_EIS) : (sctlr & ~SCTLR_EL1_EIS); + sctlr = eos_val ? (sctlr | SCTLR_EL1_EOS) : (sctlr & ~SCTLR_EL1_EOS); + asm volatile("msr SCTLR_EL1, %0" :: "r" (sctlr)); + asm volatile("isb"); +} diff --git a/litmus/libdir/_aarch64/_exs.h b/litmus/libdir/_aarch64/_exs.h new file mode 100644 index 0000000000..576b94d0fb --- /dev/null +++ b/litmus/libdir/_aarch64/_exs.h @@ -0,0 +1,22 @@ +/****************************************************************************/ +/* the diy toolsuite */ +/* */ +/* Jade Alglave, University College London, UK. */ +/* Luc Maranget, INRIA Paris-Rocquencourt, France. */ +/* */ +/* Copyright 2026-present Institut National de Recherche en Informatique et */ +/* en Automatique and the authors. 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, */ +/* modify and/ or redistribute the software under the terms of the CeCILL-B */ +/* license as circulated by CEA, CNRS and INRIA at the following URL */ +/* "http://www.cecill.info". We also give a copy in LICENSE.txt. */ +/****************************************************************************/ +#ifndef _LITMUS_EXS_H +#define _LITMUS_EXS_H 1 + +int check_exs(const char *tname); +void init_exs(int eis_val, int eos_val); + +#endif diff --git a/litmus/objUtil.ml b/litmus/objUtil.ml index 488b8837a3..0659daf17d 100644 --- a/litmus/objUtil.ml +++ b/litmus/objUtil.ml @@ -272,6 +272,15 @@ module Make(O:Config)(Tar:Tar.S) = fnames end else fnames in + let fnames = + if flags.Flags.exs then + begin + let sub = dir_of_sysarch O.sysarch in + let fnames = cpy ~sub:sub fnames "exs" ".c" in + let fnames = cpy ~sub:sub fnames "exs" ".h" in + fnames + end + else fnames in let fnames = if flags.Flags.pac then let sub = dir_of_sysarch O.sysarch in diff --git a/litmus/preSi.ml b/litmus/preSi.ml index 7d9a8765c8..bedbcf090f 100644 --- a/litmus/preSi.ml +++ b/litmus/preSi.ml @@ -80,6 +80,11 @@ module Make if Cfg.variant Variant_litmus.ConstPacField && not (Cfg.variant Variant_litmus.Pac) then Warn.user_error "\"const-pac-field\" variant require \"pac\" variant" + let () = + if (Cfg.variant Variant_litmus.EIS || Cfg.variant Variant_litmus.EOS) + && not (Cfg.variant Variant_litmus.ExS) then + Warn.user_error "\"eis\"/\"eos\" variants require \"exs\" variant" + module Insert = ObjUtil.Insert (struct @@ -271,6 +276,9 @@ module Make if Cfg.variant Variant_litmus.MemTag then begin O.o "#include \"memtag.h\"" end; + if Cfg.variant Variant_litmus.ExS then begin + O.o "#include \"exs.h\"" + end; if Cfg.variant Variant_litmus.Pac then begin O.o "#include \"auth.h\"" end; @@ -2256,6 +2264,14 @@ module Make in O.fi "mte_init(%s);" (pp_tag_check Cfg.tagcheck); end; + if Cfg.variant Variant_litmus.ExS then + begin + let eis_val = + if Cfg.variant Variant_litmus.EIS then 1 else 0 in + let eos_val = + if Cfg.variant Variant_litmus.EOS then 1 else 0 in + O.fi "init_exs(%d, %d);" eis_val eos_val; + end; if Cfg.variant Variant_litmus.Pac then O.oi "init_pauth();" ; O.oi "int id = smp_processor_id();" ; @@ -2424,6 +2440,8 @@ module Make end ; if Cfg.variant Variant_litmus.ConstPacField then O.fi "if (!check_const_pac_field_variant(%S)) return 0;" doc.Name.name; + if Cfg.is_kvm && Cfg.variant Variant_litmus.ExS then + O.fi "if (!check_exs(%S)) return 0;" doc.Name.name ; if Cfg.is_kvm then begin match db with | None -> diff --git a/litmus/top_litmus.ml b/litmus/top_litmus.ml index 7b559f8ccd..490fcd9490 100644 --- a/litmus/top_litmus.ml +++ b/litmus/top_litmus.ml @@ -271,7 +271,8 @@ end = struct let flags = { Flags.pac = O.variant Variant_litmus.Pac; Flags.self = O.variant Variant_litmus.Self; - Flags.memtag = O.variant Variant_litmus.MemTag } in + Flags.memtag = O.variant Variant_litmus.MemTag; + Flags.exs = O.variant Variant_litmus.ExS } in dump src doc compiled; if not OT.is_out then begin let _utils = diff --git a/litmus/variant_litmus.ml b/litmus/variant_litmus.ml index e6b5b86e85..18f54d91b8 100644 --- a/litmus/variant_litmus.ml +++ b/litmus/variant_litmus.ml @@ -20,6 +20,9 @@ type t = | S128 (* 128 bit signed ints*) | Mixed (* Ignored *) | Vmsa (* Checked *) + | ExS (* Enhanced Exception Synchronization *) + | EIS (* Set SCTLR_EL1.EIS=1 when variant present *) + | EOS (* Set SCTLR_EL1.EOS=1 when variant present *) | Telechat (* Telechat idiosyncrasies *) | SVE (* Do nothing *) | SME (* Do nothing *) @@ -37,6 +40,9 @@ let (mode_variants, arch_variants) : t list * t list = | S128 -> S128 | Mixed -> Mixed | Vmsa -> Vmsa + | ExS -> ExS + | EIS -> EIS + | EOS -> EOS | Telechat -> Telechat | SVE -> SVE | SME -> SME @@ -50,7 +56,9 @@ let (mode_variants, arch_variants) : t list * t list = let base_modes = List.map f [NoInit; S128; Telechat] and archs = - List.map f [SVE; SME; Self; Mixed; Vmsa; Pac; FPac; ConstPacField; MemTag;] + List.map f + [SVE; SME; Self; Mixed; Vmsa; ExS; EIS; EOS; Pac; FPac; ConstPacField; + MemTag;] and mte_precisions = List.map (fun precision -> f (MTEPrecision precision)) Precision.all and fault_modes = @@ -71,6 +79,9 @@ let parse s = match Misc.lowercase s with | "ifetch"|"self" -> Some Self | "mixed" -> Some Mixed | "vmsa"|"kvm" -> Some Vmsa +| "exs" -> Some ExS +| "eis" -> Some EIS +| "eos" -> Some EOS | "telechat" -> Some Telechat | "sve" -> Some SVE | "sme" -> Some SME @@ -104,6 +115,9 @@ let pp = function | Mixed -> "mixed" | S128 -> "s128" | Vmsa -> "vmsa" + | ExS -> "exs" + | EIS -> "eis" + | EOS -> "eos" | Telechat -> "telechat" | FaultHandling p -> Fault.Handling.pp p | SVE -> "sve" diff --git a/litmus/variant_litmus.mli b/litmus/variant_litmus.mli index c8b7739ebb..ec01b6dde3 100644 --- a/litmus/variant_litmus.mli +++ b/litmus/variant_litmus.mli @@ -20,6 +20,9 @@ type t = | S128 (* 128 bit signed ints*) | Mixed (* Ignored *) | Vmsa (* Checked *) + | ExS (* Enhanced Exception Synchronization *) + | EIS (* Set SCTLR_EL1.EIS=1 when variant present *) + | EOS (* Set SCTLR_EL1.EOS=1 when variant present *) | Telechat (* Telechat idiosyncrasies *) | SVE (* Do nothing *) | SME (* Do nothing *)