feat(Isla): Support named page-table walks

cli/lib/isla/bv_fns.ml

@@ -52,7 +52,7 @@ let int_of_bit_arg name arg value =
 
     Any error during evaluation should be reported with [Failure] which will be
     converted into a [eval_error] in [Term.eval] *)
-let functions : Fn_registry.positional_fn list =
+let functions : (string * (Z.t list -> Z.t)) list =
   [ ( "bvand",
       function
       | [a; b] -> Z.logand a b

cli/lib/isla/eval_state.ml

@@ -44,10 +44,12 @@ type page_table = (int, int64) Hashtbl.t
 
 type t =
   { symbols : (string, int) Hashtbl.t;
+    walks : (string, int list) Hashtbl.t; (* PTE addresses from level 0. *)
     mutable page_table : page_table option
   }
 
-let create () = {symbols = Hashtbl.create 32; page_table = None}
+let create () =
+  {symbols = Hashtbl.create 32; walks = Hashtbl.create 16; page_table = None}
 
 (** Decides if a string is an Archsem symbol: must start with a ASCII letter or
     [_] and followed by alphanumeric character (or [_]).
@@ -70,7 +72,7 @@ let check_symbol_name name =
 
 let check_fresh_symbol state name =
   check_symbol_name name;
-  if Hashtbl.mem state.symbols name then
+  if Hashtbl.mem state.symbols name || Hashtbl.mem state.walks name then
     Printf.ksprintf failwith "Symbol %s is already defined" name
 
 let add_symbol state name addr =
@@ -80,4 +82,11 @@ let add_symbol state name addr =
 let lookup_addr state name =
   match Hashtbl.find_opt state.symbols name with
   | Some addr -> addr
+  | None when Hashtbl.mem state.walks name ->
+      Printf.ksprintf failwith "Symbol %s is a table walk, expected an address"
+        name
   | None -> Printf.ksprintf failwith "Symbol %s not found" name
+
+let add_walk state name walk =
+  check_fresh_symbol state name;
+  Hashtbl.add state.walks name walk

cli/lib/isla/fn_registry.ml

@@ -44,13 +44,23 @@
     Any error during evaluation should be reported with [Failure] which will be
     converted into a [eval_error] in [Term.eval] *)
 
-type positional_fn = string * (Z.t list -> Z.t)
+type value =
+  | Num of Z.t
+  | Walk of string * int list
 
-type keyword_fn = string * ((string * Z.t) list -> Z.t)
+type positional_fn = string * (value list -> value)
+
+type keyword_fn = string * ((string * value) list -> value)
 
 (** Raise a function-scoped evaluation error. *)
 let error fmt = Litmus.Error.failwith ("function: " ^^ fmt)
 
+(** Require a numeric value for an ordinary function or expression. *)
+let number name : value -> Z.t = function
+  | Num z -> z
+  | Walk (walk_name, _) ->
+      error "%s: table walk %s used where a number is required" name walk_name
+
 (** Convert a Zarith argument to an OCaml [int], preserving function context. *)
 let int_arg name arg value =
   match Z.to_int value with

cli/lib/isla/lexer.mll

@@ -76,6 +76,7 @@ rule token = parse
   | "physical" { PHYSICAL }
   | "identity" { IDENTITY }
   | "with" { WITH }
+  | "as" { AS }
   | "and" { AND_KW }
   | "default" { DEFAULT }
   | "code" { CODE }

cli/lib/isla/page_table/page_table_ast.ml

@@ -80,19 +80,23 @@ type stmt =
         names : string list
       }
   (* [x |-> pa_x;] maps a named address to a physical-address target.
-     Optional [with ... and default] clauses override descriptor fields. *)
+     Optional [with ... and default] clauses override descriptor fields.
+     [as name] records the mapping's table and PTE addresses. *)
   | Mapping of
       { va_name : string;
         target : mapping_target;
         attrs : descriptor_expr_field list;
-        level : int option
+        level : int option;
+        walk_name : string option
       }
-  (* [x ?-> pa_x;] is accepted for Isla compatibility, but ignored entirely. *)
+  (* [x ?-> pa_x;] is accepted for Isla compatibility and ignored,
+     including any [as name] annotation. *)
   | MaybeMapping of
       { va_name : string;
         target : mapping_target;
         attrs : descriptor_expr_field list;
-        level : int option
+        level : int option;
+        walk_name : string option
       }
   (* [*pa_name = value;] allocates the PA on first use and evaluates the value. *)
   | DataInit of
@@ -102,7 +106,8 @@ type stmt =
   (* [identity addr with attr;] maps one page to itself. *)
   | IdentityMapping of
       { addr : Term_ast.t;
-        attr : attr
+        attr : attr;
+        walk_name : string option
       }
   (* [s1table name 0x280000 { ... }] immediately binds the name to its fixed
      root PA before executing the body. *)

cli/lib/isla/page_table/page_table_builder.ml

@@ -213,6 +213,8 @@ let check_aligned_at_level name level addr =
 
 (** Write an encoded descriptor at [va], allocating intermediate tables. *)
 let write_descriptor ?(level = Desc.last_level) builder ~root ~va desc =
+  if level < Desc.root_level || level > Desc.last_level then
+    error "page_table: invalid mapping level: %d" level;
   let rec walk table_addr current_level =
     let idx = Desc.va_index va current_level in
     if current_level = level then
@@ -335,6 +337,23 @@ let require_root = function
         "page_table: top-level mapping requires an implicit default table, but \
          default_tables = false"
 
+(** Record PTE addresses through [level] or the end of the existing path. *)
+let record_walk ?(level = Desc.last_level) builder ~root ~va name =
+  match name with
+  | None -> ()
+  | Some name ->
+      let rec walk table current_level =
+        let idx = Desc.va_index va current_level in
+        let addr = entry_addr table idx in
+        if current_level = level then [addr]
+        else
+          match child_table_addr builder table idx with
+          | None -> [addr]
+          | Some child -> addr :: walk child (current_level + 1)
+      in
+      Eval_state.add_walk builder.state name
+        (walk (require_root root) Desc.root_level)
+
 let rec eval_stmt builder ~table_block ~root = function
   | Page_table_ast.OptionDefaultTables _ -> ()
   | Page_table_ast.Virtual _ -> ()
@@ -346,24 +365,31 @@ let rec eval_stmt builder ~table_block ~root = function
          )
         names
   | Page_table_ast.AlignedVirtual _ -> ()
-  | Page_table_ast.Mapping {va_name; target; attrs; level} ->
+  | Page_table_ast.Mapping {va_name; target; attrs; level; walk_name} ->
+      Option.iter (Eval_state.check_fresh_symbol builder.state) walk_name;
       let root = require_root root in
       let va = Eval_state.lookup_addr builder.state va_name in
-      eval_mapping_target ?level ~attrs builder ~root ~va target
+      eval_mapping_target ?level ~attrs builder ~root ~va target;
+      record_walk ?level builder ~root:(Some root) ~va walk_name
   | Page_table_ast.MaybeMapping _ -> ()
   | Page_table_ast.DataInit {pa_name; value} ->
       let pa = alloc_pa builder pa_name in
       let value = Term.eval ~state:builder.state value in
       Hashtbl.replace builder.data_inits pa value
-  | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Code} ->
+  | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Code; walk_name}
+    ->
       let addr = addr_of_z "address" (Term.eval ~state:builder.state addr) in
       if addr < Allocator.page_size || addr >= Allocator.big_size then
         error "page_table: identity code address 0x%x is outside the code arena"
-          addr
-  | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Data} ->
+          addr;
+      record_walk builder ~root ~va:addr walk_name
+  | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Data; walk_name}
+    ->
+      Option.iter (Eval_state.check_fresh_symbol builder.state) walk_name;
       let root = require_root root in
       let addr = addr_of_z "address" (Term.eval ~state:builder.state addr) in
-      add_mapping builder ~root ~va:addr ~pa:addr Page_table_ast.Data
+      add_mapping builder ~root ~va:addr ~pa:addr Page_table_ast.Data;
+      record_walk builder ~root:(Some root) ~va:addr walk_name
   | Page_table_ast.TableBlock {name; base; body; _} ->
       let base = table_addr "table base" base in
       if Hashtbl.mem builder.named_roots name then

cli/lib/isla/page_table/page_table_builder.mli

@@ -63,9 +63,7 @@ type layout =
 exception Error of string
 
 (** Build a concrete page-table layout by executing statements in source order.
-    Symbols are registered as they are allocated. Expressions query the live
-    entries built so far. After setup, [state] retains these entries for register
-    and assertion evaluation. *)
+    [state] retains symbols, entries and named walks for expression evaluation. *)
 val build :
    arch:Litmus.Arch_id.t ->
   (* Allocate physical addresses for data symbols. *)

cli/lib/isla/page_table/page_table_fns.ml

@@ -41,15 +41,15 @@
 (** Page-table helper functions available in Isla expressions. *)
 
 (** [page(a)] extracts a 4KB page number from an address. *)
-let page_function =
+let page_function : string * (Z.t list -> Z.t) =
   ( "page",
     function
     | [a] -> Z.extract a 12 36
     | args -> Fn_registry.arity_error "page" 1 (List.length args)
   )
 
 (** [asid(v)] shifts an ASID value into bits [63:48]. *)
-let asid_function =
+let asid_function : string * (Z.t list -> Z.t) =
   ( "asid",
     function
     | [v] -> Z.shift_left v 48
@@ -79,28 +79,52 @@ let pte_addr name entries ~base ~va ~level =
   in
   walk base Page_table_desc.root_level
 
-(** [pteN(va, base)] treats [base] as the root translation-table PA, then
-    returns the identity-mapped VA of the matching PTE. *)
-let pte_function entries level =
-  let name = Printf.sprintf "pte%d" level in
-  ( name,
-    function
+(** [pteN(walk)] and [tableN(walk)] use recorded addresses;
+    [pteN(va, base)] and [tableN(va, base)] query the current tables. *)
+let entry_function ~pte entries level : Fn_registry.positional_fn =
+  let name = Printf.sprintf "%s%d" (if pte then "pte" else "table") level in
+  let eval : Fn_registry.value list -> int = function
+    | [Fn_registry.Walk (walk_name, walk)] -> (
+      match List.nth_opt walk level with
+      | Some addr -> addr
+      | None ->
+          Fn_registry.error "%s: table walk %s has no level %d" name walk_name
+            level
+    )
+    | [_] -> Fn_registry.error "%s: expected a table walk" name
     | [va; base] ->
-        let va = Fn_registry.int_arg name "va" va in
-        let base = Fn_registry.int_arg name "base" base in
-        let pte_pa = pte_addr name entries ~base ~va ~level in
-        if pte_pa < Allocator.big_size || pte_pa >= 2 * Allocator.big_size then
+        let va = Fn_registry.int_arg name "va" (Fn_registry.number name va) in
+        let base =
+          Fn_registry.int_arg name "base" (Fn_registry.number name base)
+        in
+        let addr = pte_addr name entries ~base ~va ~level in
+        if pte && (addr < Allocator.big_size || addr >= 2 * Allocator.big_size)
+        then
           Fn_registry.error
             "%s: PTE level %d for VA 0x%x was resolved at PA 0x%x which is \
              outside page-table storage, for root 0x%x"
-             name level va pte_pa base;
-        Z.of_int pte_pa
-    | args -> Fn_registry.arity_error name 2 (List.length args)
+             name level va addr base;
+        addr
+    | args ->
+        Fn_registry.error "%s: expected 1 or 2 arguments, got %d" name
+          (List.length args)
+  in
+  ( name,
+    fun args ->
+      let addr = eval args in
+      Fn_registry.Num
+        (Z.of_int (if pte then addr else Page_table_desc.align_page_addr addr))
   )
 
+let pte_function entries level : Fn_registry.positional_fn =
+  entry_function ~pte:true entries level
+
+let table_function entries level : Fn_registry.positional_fn =
+  entry_function ~pte:false entries level
+
 (** [descN(va, base)] treats [base] as the root translation-table PA and
     returns the descriptor stored in the matching level-[N] PTE. *)
-let desc_function entries level =
+let desc_function entries level : string * (Z.t list -> Z.t) =
   let name = Printf.sprintf "desc%d" level in
   ( name,
     function
@@ -119,21 +143,8 @@ let desc_function entries level =
     | args -> Fn_registry.arity_error name 2 (List.length args)
   )
 
-(** [tableN(va, base)] returns the page containing the level-[N] PTE. *)
-let table_function entries level =
-  let name = Printf.sprintf "table%d" level in
-  ( name,
-    function
-    | [va; base] ->
-        let va = Fn_registry.int_arg name "va" va in
-        let base = Fn_registry.int_arg name "base" base in
-        let addr = pte_addr name entries ~base ~va ~level in
-        Z.of_int (Page_table_desc.align_page_addr addr)
-    | args -> Fn_registry.arity_error name 2 (List.length args)
-  )
-
 (** [mkdescN(oa=..., ...)] encodes a level-[N] block/page descriptor. *)
-let eval_desc name level kwargs =
+let eval_desc name level (kwargs : (string * Z.t) list) : Z.t =
   Fn_registry.check_kwargs name ["oa"; "Valid"; "AF"; "AP"; "DBM"; "nG"] kwargs;
   let oa = Fn_registry.required_kwarg name "oa" kwargs in
   let fields =
@@ -151,7 +162,7 @@ let eval_desc name level kwargs =
     )
 
 (** [mkdescN(table=...)] encodes a next-level table descriptor. *)
-let eval_table_desc name kwargs =
+let eval_table_desc name (kwargs : (string * Z.t) list) : Z.t =
   Fn_registry.check_kwargs name ["table"; "APTable"] kwargs;
   let table_addr = Fn_registry.required_kwarg name "table" kwargs in
   let fields = [descriptor_field_arg kwargs "APTable" Z.zero] in
@@ -160,7 +171,7 @@ let eval_table_desc name kwargs =
        (Fn_registry.int_arg name "table" table_addr)
     )
 
-let mkdesc_function level =
+let mkdesc_function level : string * ((string * Z.t) list -> Z.t) =
   let name = Printf.sprintf "mkdesc%d" level in
   let eval kwargs =
     match (List.mem_assoc "oa" kwargs, List.mem_assoc "table" kwargs) with
@@ -178,7 +189,7 @@ let check_unsigned name arg bits value =
 
 (** [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 ttbr_function : string * ((string * Z.t) list -> Z.t) =
   let name = "ttbr" in
   let eval kwargs =
     Fn_registry.check_kwargs name ["asid"; "vmid"; "base"] kwargs;
@@ -197,17 +208,44 @@ let ttbr_function =
   in
   (name, eval)
 
-let positional_functions ~state =
-  let functions = [page_function; asid_function] in
+let positional_functions ~state : Fn_registry.positional_fn list =
+  let functions =
+    List.map
+      (fun (name, eval) ->
+         ( name,
+           fun args ->
+             Fn_registry.Num (eval (List.map (Fn_registry.number name) args))
+         )
+       )
+      [page_function; asid_function]
+  in
   match state.Eval_state.page_table with
   | None -> functions
   | Some entries ->
       let levels = [0; 1; 2; 3] in
       functions
       @ List.map (pte_function entries) levels
-      @ List.map (desc_function entries) levels
+      @ List.map
+          (fun level ->
+             let (name, eval) = desc_function entries level in
+             ( name,
+               fun args ->
+                 Fn_registry.Num (eval (List.map (Fn_registry.number name) args))
+             )
+           )
+          levels
       @ List.map (table_function entries) levels
 
 let keyword_functions : Fn_registry.keyword_fn list =
   let levels = [0; 1; 2; 3] in
-  ttbr_function :: List.map mkdesc_function levels
+  List.map
+    (fun (name, eval) ->
+       ( name,
+         fun kwargs ->
+           let args =
+             List.map (fun (k, v) -> (k, Fn_registry.number name v)) kwargs
+           in
+           Fn_registry.Num (eval args)
+       )
+     )
+    (ttbr_function :: List.map mkdesc_function levels)