feat(Isla): Support TTBR page-table helper

cli/lib/isla/page_table/page_table_fns.ml

@@ -158,6 +158,31 @@ let mkdesc_function level =
   in
   (name, eval)
 
+let check_unsigned name arg bits value =
+  if Z.sign value < 0 || Z.numbits value > bits then
+    Fn_registry.error "%s: argument %s does not fit in %d bits" name arg bits
+
+(** [ttbr(asid=..., base=...)] and [ttbr(vmid=..., base=...)] combine a
+    concrete translation-table root PA with its 16-bit address-space ID. *)
+let ttbr_function =
+  let name = "ttbr" in
+  let eval kwargs =
+    Fn_registry.check_kwargs name ["asid"; "vmid"; "base"] kwargs;
+    let base = Fn_registry.required_kwarg name "base" kwargs in
+    let (id_name, id) =
+      match (List.assoc_opt "asid" kwargs, List.assoc_opt "vmid" kwargs) with
+      | (Some id, None) -> ("asid", id)
+      | (None, Some id) -> ("vmid", id)
+      | _ -> Fn_registry.error "%s: expected exactly one of asid or vmid" name
+    in
+    check_unsigned name id_name 16 id;
+    check_unsigned name "base" 48 base;
+    if not (Z.equal (Z.extract base 0 12) Z.zero) then
+      Fn_registry.error "%s: argument base must be 4KB aligned" name;
+    Z.((id lsl 48) lor base)
+  in
+  (name, eval)
+
 let positional_functions ?page_table_entries () =
   let functions = [page_function; asid_function] in
   match page_table_entries with
@@ -170,4 +195,4 @@ let positional_functions ?page_table_entries () =
 
 let keyword_functions : Fn_registry.keyword_fn list =
   let levels = [0; 1; 2; 3] in
-  List.map mkdesc_function levels
+  ttbr_function :: List.map mkdesc_function levels

cli/tests/arm/vm/SwitchTTBR+VM.litmus.toml

@@ -18,12 +18,12 @@ s1table table1 0x300000 {
 """
 
 [thread.0]
-init = { X0 = "table1", X2 = "x", TTBR0_EL1 = "table0", SCTLR_EL1 = 1, CurrentEL = 1 }
+init = { X0 = "ttbr(asid=0x2, base=table1)", X2 = "x", TTBR0_EL1 = "ttbr(asid=0x1, base=table0)", SCTLR_EL1 = 1, CurrentEL = 1 }
 code = """
 MSR TTBR0_EL1, X0
 MRS X3, TTBR0_EL1
 LDR X1, [X2]
 """
 
 [final]
-assertion = "0:X1 = 1 & 0:X3 = table1"
+assertion = "0:X1 = 1 & 0:X3 = ttbr(asid=0x2, base=table1) & 0:TTBR0_EL1 = 0:X3"

cli/tests/converter/expect/arm/vm/SwitchTTBR+VM.litmus.toml

@@ -99,9 +99,9 @@ name = "SwitchTTBR+VM"
 
 [thread."0".regs]
   _PC = 0x1000
-  "R0" = 0x300000
+  "R0" = 0x2000000300000
   "R2" = 0x400000
-  "TTBR0_EL1" = 0x2c0000
+  "TTBR0_EL1" = 0x10000002c0000
   "SCTLR_EL1" = 1
   CurrentEL = 1
   "R1" = 0
@@ -140,4 +140,4 @@ name = "SwitchTTBR+VM"
   DAIF = 0
 
 [final]
-  assertion = {and = [{"0:X1" = 1}, {"0:X3" = 0x300000}]}
+  assertion = {and = [{"0:X1" = 1}, {"0:X3" = 0x2000000300000}, {"0:TTBR0_EL1" = "0:X3"}]}