feat(Isla): Accept default page-table option

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,53 @@ 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 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 =
+    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
+        | Page_table_ast.Mapping {va_name; level = Some level; _} ->
+            [(va_name, checked_mapping_alignment level)]
+        | _ -> []
+        )
+      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 +215,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}
 
@@ -282,7 +331,11 @@ let build_lookup_addr asm_result page_table =
   let page_table_symbols =
     match page_table with
     | None -> []
-    | Some layout -> layout.Page_table_builder.symbols_pa
+    | Some layout ->
+        ("page_table_base", layout.Page_table_builder.root)
+        :: (layout.Page_table_builder.table_symbols_pa
+          @ layout.Page_table_builder.data_symbols_pa
+           )
   in
   let symbols_addr = asm_result.Assembler.symbols @ page_table_symbols in
   fun name ->
@@ -370,7 +423,7 @@ let build_page_table_memory ~default_mem_size ~symbol_sizes page_table =
          in
          data_memory_block ~step:mem_size ~symbol:sym pa value
        )
-      page_table.Page_table_builder.phys_symbols_pa
+      page_table.Page_table_builder.data_symbols_pa
   in
   table_memory @ phys_memory
 

cli/lib/isla/lexer.mll

@@ -66,8 +66,12 @@ rule token = parse
   | ';' { SEMICOLON }
   | '[' { LBRACKET }
   | ']' { RBRACKET }
+  | '{' { LBRACE }
+  | '}' { RBRACE }
   | ',' { COMMA }
   | '-' { MINUS }
+  | "aligned" { ALIGNED }
+  | "option" { OPTION }
   | "virtual" { VIRTUAL }
   | "physical" { PHYSICAL }
   | "identity" { IDENTITY }
@@ -78,6 +82,8 @@ rule token = parse
   | "data" { DATA }
   | "invalid" { INVALID }
   | "table" { TABLE }
+  | "s1table" { S1TABLE }
+  | "s2table" { S2TABLE }
   | "at" { AT }
   | "level" { LEVEL }
   | "true" { TRUE }

cli/lib/isla/page_table/page_table_ast.ml

@@ -41,12 +41,17 @@
 (** 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
   | Data
 
+type table_stage =
+  | S1
+  | S2
+
 type descriptor_field =
   { name : string;
     value : Z.t
@@ -58,10 +63,17 @@ type mapping_target =
   | Table of Z.t
 
 type stmt =
+  (* [option default_tables = true;] is accepted for Isla compatibility. *)
+  | OptionDefaultTablesTrue
   (* [virtual x y;] predeclares VA-side names. *)
   | 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
@@ -87,3 +99,9 @@ type stmt =
       { addr : Z.t;
         attr : attr
       }
+  | TableBlock of
+      { stage : table_stage;
+        name : string;
+        base : Z.t;
+        body : stmt list
+      }