feat(Isla): Partition page-table allocation arenas

cli/lib/isla/allocator.ml

@@ -47,8 +47,6 @@ type t =
     limit : int option
   }
 
-let default_base = 0x1000
-
 let page_size = 0x1000
 
 let big_size = 1 lsl 21
@@ -60,7 +58,7 @@ let align_up addr alignment =
 
 let page_after addr = align_up (addr + 1) page_size
 
-let make ?(base = default_base) ?limit ?(reserved = []) () =
+let make ~base ?limit ?(reserved = []) () =
   let current =
     List.fold_left
       (fun current addr -> max current (page_after addr))

cli/lib/isla/allocator.mli

@@ -50,7 +50,7 @@ val big_size : int
 
 (** Make an allocator, optionally with an exclusive upper limit and reserved
     addresses. Each reserved address blocks the page containing it. *)
-val make : ?base:int -> ?limit:int -> ?reserved:int list -> unit -> t
+val make : base:int -> ?limit:int -> ?reserved:int list -> unit -> t
 
 (** Allocate [size] bytes at an address aligned to [alignment]. *)
 val alloc_aligned : t -> size:int -> alignment:int -> int

cli/lib/isla/converter.ml

@@ -153,6 +153,11 @@ let checked_virtual_alignment alignment =
       alignment;
   alignment
 
+let checked_mapping_alignment level =
+  try Page_table_desc.level_size level
+  with Invalid_argument _ ->
+    eval_error Page_table_setup "page_table: invalid mapping level: %d" level
+
 let symbolic_va_alignments ir =
   let virtual_names = symbolic_names ir in
   let alignment_requests =
@@ -168,6 +173,8 @@ let symbolic_va_alignments ir =
                )
               names;
             List.map (fun name -> (name, alignment)) names
+        | Page_table_ast.Mapping {va_name; level = Some level; _} ->
+            [(va_name, checked_mapping_alignment level)]
         | _ -> []
         )
       ir.Ir.page_table_setup
@@ -181,15 +188,29 @@ let symbolic_va_alignments ir =
   in
   List.map (fun name -> (name, alignment_for name)) virtual_names
 
+let make_arena ?(reserved = []) base =
+  assert (base land 0x1FFFFF == 0);
+  Allocator.make ~base ~limit:(base + Allocator.big_size) ~reserved ()
+
+(* Layout:
+   - Code: 0-2 MiB
+   - Page tables: 2-4 MiB
+   - Data: >= 4 MiB *)
+let table_base = Allocator.big_size
+
+let data_base = table_base + Allocator.big_size
+
 (* Build assembly input after assigning concrete addresses to every section and
    symbolic location. *)
-let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
+let to_assembly_input ~code_allocator ~symbol_allocator (ir : Ir.t) :
+  Assembler.assembly_input
+  =
   let code_sections =
     List.mapi
       (fun i (thread : Ir.thread) ->
          { Assembler.name = thread_section_name i;
            code = thread.code;
-           addr = Allocator.alloc_page allocator
+           addr = Allocator.alloc_page code_allocator
          }
        )
       ir.threads
@@ -200,7 +221,7 @@ let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
          let addr =
            match sec.address with
            | Some addr -> addr
-           | None -> Allocator.alloc_page allocator
+           | None -> Allocator.alloc_page code_allocator
          in
          {Assembler.name = sec.sec_name; code = sec.code; addr}
        )
@@ -210,14 +231,18 @@ let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
     List.map
       (fun (name, alignment) ->
          let addr =
-           Allocator.alloc_aligned allocator ~size:Allocator.page_size ~alignment
+           Allocator.alloc_aligned symbol_allocator ~size:alignment ~alignment
          in
          {Assembler.name; addr}
        )
       (symbolic_va_alignments ir)
   in
   {Assembler.sections = code_sections @ named_sections; symbols}
 
+let assemble ~filename ~code_allocator ~symbol_allocator ir =
+  let input = to_assembly_input ~code_allocator ~symbol_allocator ir in
+  (input, Assembler.assemble ~filename input)
+
 (** {2 Thread register construction} *)
 
 let find_section name (asm_result : Assembler.assembly_result) =
@@ -292,34 +317,24 @@ let build_threads
 
 (** {2 Page table setup construction} *)
 
-(* Build the page-table layout from concrete section/symbol VAs.
-   Thread code pages are included so the DSL can request code mappings. *)
-let build_page_table_setup ir allocator asm_result =
-  match ir.Ir.page_table_setup with
-  | [] -> None
-  | page_table_setup -> (
-      if ir.Ir.locations <> [] then
-        eval_error Page_table_setup
-          "page_table: [locations] is not supported with page_table_setup";
-      let symbolic_vas = asm_result.Assembler.symbols in
-      let code_pages =
-        List.map
-          (fun (thread : Ir.thread) ->
-             let sec = find_section (thread_section_name thread.tid) asm_result in
-             sec.addr
-           )
-          ir.Ir.threads
-      in
-      try
-        Some
-          (Page_table_builder.build ~arch:ir.arch ~allocator ~symbolic_vas
-             ~code_pages page_table_setup
-          )
-      with Page_table_builder.Error msg -> eval_error Page_table_setup "%s" msg
-    )
-
-(* Terms may refer to VA-side assembly symbols and PA-side symbols created by
-   page_table_setup. *)
+(* Build the page-table layout from concrete section/symbol VAs. *)
+let build_page_table_setup
+      ir
+      ~symbol_allocator
+      ~table_allocator
+      ~table_block
+      asm_result
+  =
+  if ir.Ir.locations <> [] then
+    eval_error Page_table_setup
+      "page_table: [locations] is not supported with page_table_setup";
+  try
+    Page_table_builder.build ~arch:ir.arch ~symbol_allocator ~table_allocator
+      ~table_block ~symbolic_vas:asm_result.Assembler.symbols ir.page_table_setup
+  with Page_table_builder.Error msg -> eval_error Page_table_setup "%s" msg
+
+(* Terms may refer to assembly symbols denoting virtual addresses and to symbols
+   whose physical addresses are assigned by page_table_setup. *)
 let build_lookup_addr asm_result page_table =
   let page_table_symbols =
     match page_table with
@@ -444,11 +459,32 @@ let build_memory
 
 let to_testrepr ~filename (ir : Ir.t) : Testrepr.t =
   let default_mem_size = default_memory_size () in
-  let reserved_addrs = reserved_section_addrs ir.sections in
-  let allocator = Allocator.make ~reserved:reserved_addrs () in
-  let asm_input = to_assembly_input allocator ir in
-  let asm_result = Assembler.assemble ~filename asm_input in
-  let page_table = build_page_table_setup ir allocator asm_result in
+  let (asm_input, asm_result, page_table) =
+    if ir.page_table_setup = [] then
+      let allocator =
+        Allocator.make ~base:0
+          ~reserved:(0 :: reserved_section_addrs ir.sections)
+          ()
+      in
+      let (asm_input, asm_result) =
+        assemble ~filename ~code_allocator:allocator ~symbol_allocator:allocator
+          ir
+      in
+      (asm_input, asm_result, None)
+    else
+      let reserved_code_pages = reserved_section_addrs ir.sections in
+      let code_allocator = make_arena ~reserved:(0 :: reserved_code_pages) 0 in
+      let symbol_allocator = Allocator.make ~base:data_base () in
+      let (asm_input, asm_result) =
+        assemble ~filename ~code_allocator ~symbol_allocator ir
+      in
+      let page_table =
+        build_page_table_setup ir ~symbol_allocator
+          ~table_allocator:(make_arena table_base) ~table_block:table_base
+          asm_result
+      in
+      (asm_input, asm_result, Some page_table)
+  in
   let page_table_entries =
     Option.map (fun layout -> layout.Page_table_builder.table_entries) page_table
   in

cli/lib/isla/page_table/page_table_ast.ml

@@ -40,10 +40,10 @@
 
 (** Page-table setup AST.
 
-    VA-side names may be declared with [virtual] or the TOML [symbolic] list.
-    [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. *)
+    Virtual-address names may be declared with [virtual] or the TOML [symbolic]
+    list. [aligned ... virtual ...] statements constrain those names. Names for
+    physical addresses may be declared with [physical], or allocated on first
+    use by mapping/data-init statements. *)
 type attr =
   | Code
   | Data
@@ -59,16 +59,16 @@ type mapping_target =
   | Table of Z.t
 
 type stmt =
-  (* [virtual x y;] predeclares VA-side names. *)
+  (* [virtual x y;] predeclares virtual-address names. *)
   | Virtual of string list
-  (* [physical pa_x pa_y;] predeclares PA-side names. *)
+  (* [physical pa_x pa_y;] predeclares physical-address names. *)
   | Physical of string list
-  (* [aligned 2097152 virtual x y;] constrains VA-side names. *)
+  (* [aligned 2097152 virtual x y;] constrains virtual-address names. *)
   | AlignedVirtual of
       { alignment : Z.t;
         names : string list
       }
-  (* [x |-> pa_x;] maps an existing symbolic VA to a PA-side target.
+  (* [x |-> pa_x;] maps a symbolic virtual address to a physical-address target.
      Optional [with ... and default] clauses override descriptor fields. *)
   | Mapping of
       { va_name : string;
@@ -83,7 +83,7 @@ type stmt =
         attrs : descriptor_field list;
         level : int option
       }
-  (* [*pa_x = value;] initialises data at a PA-side name. *)
+  (* [*pa_x = value;] initialises data at a named physical address. *)
   | DataInit of
       { pa_name : string;
         value : Z.t