feat(Isla): Support page-table symbol alignment

cli/lib/isla/allocator.mli

@@ -52,6 +52,9 @@ val big_size : int
     address blocks the page containing it. *)
 val make : ?base:int -> ?reserved:int list -> unit -> t
 
+(** Allocate [size] bytes at an address aligned to [alignment]. *)
+val alloc_aligned : t -> size:int -> alignment:int -> int
+
 (** Allocate one 4KB page. *)
 val alloc_page : t -> int
 

cli/lib/isla/converter.ml

@@ -141,6 +141,46 @@ let symbolic_names ir =
        )
     ir.Ir.symbolic ir.Ir.page_table_setup
 
+let checked_virtual_alignment alignment =
+  let alignment =
+    try Z.to_int alignment
+    with Z.Overflow ->
+      eval_error Page_table_setup "page_table: virtual alignment is out of range"
+  in
+  if alignment <= 0 || alignment mod Allocator.page_size <> 0 then
+    eval_error Page_table_setup
+      "page_table: virtual alignment must be a positive multiple of page size: %d"
+      alignment;
+  alignment
+
+let symbolic_va_alignments ir =
+  let virtual_names = symbolic_names ir in
+  let alignment_requests =
+    List.concat_map
+      (function
+        | Page_table_ast.AlignedVirtual {alignment; names} ->
+            let alignment = checked_virtual_alignment alignment in
+            List.iter
+              (fun name ->
+                 if not (List.mem name virtual_names) then
+                   eval_error Page_table_setup "page_table: undeclared VA: %s"
+                     name
+               )
+              names;
+            List.map (fun name -> (name, alignment)) names
+        | _ -> []
+        )
+      ir.Ir.page_table_setup
+  in
+  let alignment_for name =
+    List.fold_left
+      (fun best (aligned_name, alignment) ->
+         if aligned_name = name then max best alignment else best
+       )
+      Allocator.page_size alignment_requests
+  in
+  List.map (fun name -> (name, alignment_for name)) virtual_names
+
 (* Build assembly input after assigning concrete addresses to every section and
    symbolic location. *)
 let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
@@ -168,11 +208,13 @@ let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
   in
   let symbols =
     List.map
-      (fun sym ->
-         let addr = Allocator.alloc_page allocator in
-         {Assembler.name = sym; addr}
+      (fun (name, alignment) ->
+         let addr =
+           Allocator.alloc_aligned allocator ~size:Allocator.page_size ~alignment
+         in
+         {Assembler.name; addr}
        )
-      (symbolic_names ir)
+      (symbolic_va_alignments ir)
   in
   {Assembler.sections = code_sections @ named_sections; symbols}
 

cli/lib/isla/lexer.mll

@@ -68,6 +68,7 @@ rule token = parse
   | ']' { RBRACKET }
   | ',' { COMMA }
   | '-' { MINUS }
+  | "aligned" { ALIGNED }
   | "virtual" { VIRTUAL }
   | "physical" { PHYSICAL }
   | "identity" { IDENTITY }

cli/lib/isla/page_table/page_table_ast.ml

@@ -41,7 +41,8 @@
 (** Page-table setup AST.
 
     VA-side names may be declared with [virtual] or the TOML [symbolic] list.
-    PA-side names may be declared with [physical], or allocated on first use by
+    [aligned ... virtual ...] statements constrain those VA-side names. PA-side
+    names may be declared with [physical], or allocated on first use by
     mapping/data-init statements. *)
 type attr =
   | Code
@@ -62,6 +63,11 @@ type stmt =
   | Virtual of string list
   (* [physical pa_x pa_y;] predeclares PA-side names. *)
   | Physical of string list
+  (* [aligned 2097152 virtual x y;] constrains VA-side names. *)
+  | AlignedVirtual of
+      { alignment : Z.t;
+        names : string list
+      }
   (* [x |-> pa_x;] maps an existing symbolic VA to a PA-side target.
      Optional [with ... and default] clauses override descriptor fields. *)
   | Mapping of

cli/lib/isla/page_table/page_table_builder.ml

@@ -64,10 +64,17 @@ let error fmt = Printf.ksprintf (fun msg -> raise (Error msg)) fmt
 
 type t =
   { allocator : Allocator.t;
+    (* Root translation-table address. *)
     root : pa;
+    (* Next free page in the translation-table pool. *)
     mutable next_table_pa : pa;
+    (* Page-table descriptors, keyed by their physical addresses. *)
     entries : (pa, descriptor) Hashtbl.t;
+    (* PA names declared by [physical]. *)
+    mutable declared_pas : string list;
+    (* PA names and their allocated physical addresses. *)
     mutable symbols_pa : (string * pa) list;
+    (* Initial data values, keyed by their allocated PAs. *)
     mutable data_inits : (pa * data_value) list
   }
 
@@ -77,6 +84,7 @@ let make allocator ~root =
     entries;
     root;
     next_table_pa = root + Allocator.page_size;
+    declared_pas = [];
     symbols_pa = [];
     data_inits = []
   }
@@ -87,11 +95,28 @@ let check_arch = function
       error "page_table: only AArch64 is supported, got %s"
         (Litmus.Arch_id.to_string arch)
 
-let alloc_pa builder name =
+let alloc_pa ?(alignment = Allocator.page_size) ?mapping_level builder name =
+  if not (List.mem name builder.declared_pas) then
+    error "page_table: undeclared PA: %s" name;
   match List.assoc_opt name builder.symbols_pa with
-  | Some addr -> addr
+  | Some addr -> (
+      if addr mod alignment = 0 then addr
+      else
+        match mapping_level with
+        | Some level ->
+            error
+              "page_table: PA symbol %s at 0x%x is not aligned for a level %d \
+               mapping (requires %d bytes)"
+               name addr level alignment
+        | None ->
+            error "page_table: PA symbol %s at 0x%x is not aligned to %d bytes"
+              name addr alignment
+    )
   | None ->
-      let addr = Allocator.alloc_page builder.allocator in
+      let addr =
+        Allocator.alloc_aligned builder.allocator ~size:Allocator.page_size
+          ~alignment
+      in
       builder.symbols_pa <- (name, addr) :: builder.symbols_pa;
       addr
 
@@ -197,9 +222,14 @@ let addr_of_z name addr =
   with Z.Overflow ->
     error "page_table: %s out of range: %s" name (Z.format "%#x" addr)
 
+let mapping_alignment level =
+  try Desc.level_size level
+  with Invalid_argument _ -> error "page_table: invalid mapping level: %d" level
+
 let eval_mapping_target ?level ?(attrs = []) builder ~va = function
   | Page_table_ast.PaName pa_name ->
-      let pa = alloc_pa builder pa_name in
+      let alignment = Option.map mapping_alignment level in
+      let pa = alloc_pa ?alignment ?mapping_level:level builder pa_name in
       add_mapping ?level ~fields:attrs builder ~va ~pa Page_table_ast.Data
   | Page_table_ast.Invalid ->
       if attrs <> [] then
@@ -219,7 +249,8 @@ let eval_mapping_target ?level ?(attrs = []) builder ~va = function
 let eval_stmt builder ~symbolic_vas = function
   | Page_table_ast.Virtual _ -> ()
   | Page_table_ast.Physical names ->
-      List.iter (fun name -> ignore (alloc_pa builder name)) names
+      builder.declared_pas <- builder.declared_pas @ names
+  | Page_table_ast.AlignedVirtual _ -> ()
   | Page_table_ast.Mapping {va_name; target; attrs; level} ->
       let va =
         match List.assoc_opt va_name symbolic_vas with

cli/lib/isla/parser.mly

@@ -59,6 +59,7 @@
 %token RBRACKET "]"
 %token MAPS_TO "|->"
 %token MAYBE_MAPS_TO "?->"
+%token ALIGNED
 %token VIRTUAL
 %token PHYSICAL
 %token IDENTITY
@@ -109,6 +110,8 @@ page_table_stmt_inner:
     { Page_table_ast.Virtual names }
   | PHYSICAL; names = nonempty_list(IDENT)
     { Page_table_ast.Physical names }
+  | ALIGNED; alignment = NUM; VIRTUAL; names = nonempty_list(IDENT)
+    { Page_table_ast.AlignedVirtual {alignment; names} }
   | va_name = IDENT; "|->"; rhs = page_table_mapping_rhs
     { let (target, attrs, level) = rhs in
       Page_table_ast.Mapping {va_name; target; attrs; level}

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

@@ -3,6 +3,7 @@ name = "Alias+VM"
 symbolic = ["x", "y", "z"]
 
 page_table_setup = """
+physical pa_x;
 x |-> pa_x;
 y |-> pa_x;
 """

cli/tests/arm/vm/Inval+LDR.litmus.toml

@@ -3,6 +3,7 @@ name = "Inval+LDR"
 symbolic = ["x", "y"]
 
 page_table_setup = """
+physical pa_x;
 x |-> pa_x;
 
 *pa_x = 3;

cli/tests/arm/vm/LDR+size+VM.litmus.toml

@@ -0,0 +1,25 @@
+arch = "AArch64"
+name = "LDR+size+VM"
+
+page_table_setup = """
+virtual x y;
+aligned 2097152 virtual x;
+aligned 65536 virtual y;
+physical pa_pad pa_x;
+*pa_pad = 0;
+x |-> pa_x at level 2;
+*pa_x = 0x000000010000000100000001;
+"""
+
+[sizes]
+pa_x = 12
+
+[thread.0]
+init = { X1 = "x", X2 = "y", SCTLR_EL1 = 1, CurrentEL = 1 }
+code = """
+LDR W0,[X1,#8]
+"""
+
+[final]
+kind = "exists"
+assertion = "0:X0 = 1 & 0:X2 = y & *pa_x = 0x000000010000000100000001"

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

@@ -3,6 +3,7 @@ name = "MP+VM"
 symbolic = ["x", "y"]
 
 page_table_setup = """
+physical pa_x pa_y;
 x |-> pa_x;
 y |-> pa_y;
 x ?-> pa_y;

cli/tests/converter/expect/arm/vm/STR+32.litmus.toml → cli/tests/converter/expect/arm/vm/LDR+size+VM.litmus.toml

@@ -1,5 +1,5 @@
 arch = "Arm"
-name = "STR+32"
+name = "LDR+size+VM"
 
 [[memory]]
   sym = "__thread0"
@@ -10,43 +10,49 @@ name = "STR+32"
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x200000
+  addr = 0x400000
   step = 8
-  data = 0x201003
+  data = 0x401003
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x201000
+  addr = 0x401000
   step = 8
-  data = 0x202003
+  data = 0x402003
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x202000
+  addr = 0x402000
   step = 8
-  data = 0x203003
+  data = 0x403003
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x202008
+  addr = 0x402008
   step = 8
-  data = 0x200441
+  data = 0x800441
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x203008
+  addr = 0x402010
   step = 8
-  data = 0x14c3
+  data = 0x400441
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x203010
+  addr = 0x403008
   step = 8
-  data = 0x400443
+  data = 0x14c3
+
+[[memory]]
+  sym = "pa_pad"
+  addr = 0x600000
+  step = 8
+  data = 0
 
 [[memory]]
   sym = "pa_x"
-  addr = 0x400000
+  addr = 0x800000
   step = 12
   data = 0x10000000100000001
 
@@ -57,12 +63,12 @@ name = "STR+32"
 
 [thread."0".regs]
   _PC = 0x1000
-  "R1" = 0x2000
+  "R1" = 0x200000
+  "R2" = 0x210000
   "SCTLR_EL1" = 1
   CurrentEL = 1
-  "TTBR0_EL1" = 0x200000
+  "TTBR0_EL1" = 0x400000
   "R0" = 0
-  "R2" = 0
   "R3" = 0
   "R4" = 0
   "R5" = 0
@@ -98,4 +104,4 @@ name = "STR+32"
   DAIF = 0
 
 [final]
-  assertion = {and = [{"0:X0" = 1}, {pa_x = 0x10000000100000001}]}
+  assertion = {and = [{"0:X0" = 1}, {"0:X2" = 0x210000}, {pa_x = 0x10000000100000001}]}

cli/tests/errors/errors.t

@@ -192,6 +192,13 @@ Page table DSL rejects duplicate VA mappings
   page_table: conflicting mapping for VA 0x2000: existing descriptor 0x400443, new descriptor 0x401443
   [1]
 
+Page table DSL reports a stricter mapping alignment after PA assignment
+  $ archsem seq page-table-pa-alignment.litmus.toml
+  archsem: eval error:
+  File "page-table-pa-alignment.litmus.toml", path "page_table_setup":
+  page_table: PA symbol pa_x at 0x601000 is not aligned for a level 2 mapping (requires 2097152 bytes)
+  [1]
+
 Page table DSL rejects locations with page tables
   $ archsem seq conflicting-page-table-data-init.litmus.toml
   archsem: eval error: