feat(Isla): Support virtual page-table symbols

cli/lib/isla/converter.ml

@@ -131,6 +131,15 @@ let reserved_section_addrs sections =
 
 let thread_section_name tid = Printf.sprintf "__thread%d" tid
 
+let symbolic_names ir =
+  let add names name = if List.mem name names then names else names @ [name] in
+  List.fold_left
+    (fun names -> function
+       | Page_table_ast.Virtual stmt_names -> List.fold_left add names stmt_names
+       | _ -> names
+       )
+    ir.Ir.symbolic ir.Ir.page_table_setup
+
 (* Build assembly input after assigning concrete addresses to every section and
    symbolic location. *)
 let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
@@ -162,7 +171,7 @@ let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
          let addr = Allocator.alloc_page allocator in
          {Assembler.name = sym; addr}
        )
-      ir.symbolic
+      (symbolic_names ir)
   in
   {Assembler.sections = code_sections @ named_sections; symbols}
 

cli/lib/isla/lexer.mll

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

cli/lib/isla/page_table/page_table_ast.ml

@@ -40,6 +40,7 @@
 
 (** 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
     mapping/data-init statements. *)
 type attr =
@@ -57,6 +58,8 @@ type mapping_target =
   | Table of Z.t
 
 type stmt =
+  (* [virtual x y;] predeclares VA-side names. *)
+  | Virtual of string list
   (* [physical pa_x pa_y;] predeclares PA-side names. *)
   | Physical of string list
   (* [x |-> pa_x;] maps an existing symbolic VA to a PA-side target.

cli/lib/isla/page_table/page_table_builder.ml

@@ -212,6 +212,7 @@ let eval_mapping_target ?level ?(attrs = []) builder ~va = function
       write_descriptor ~level builder ~va desc
 
 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
   | Page_table_ast.Mapping {va_name; target; attrs; level} ->

cli/lib/isla/parser.mly

@@ -59,6 +59,7 @@
 %token RBRACKET "]"
 %token MAPS_TO "|->"
 %token MAYBE_MAPS_TO "?->"
+%token VIRTUAL
 %token PHYSICAL
 %token IDENTITY
 %token WITH
@@ -104,6 +105,8 @@ page_table_stmt:
   | s = page_table_stmt_inner; ";" { s }
 
 page_table_stmt_inner:
+  | VIRTUAL; names = nonempty_list(IDENT)
+    { Page_table_ast.Virtual names }
   | PHYSICAL; names = nonempty_list(IDENT)
     { Page_table_ast.Physical names }
   | va_name = IDENT; "|->"; rhs = page_table_mapping_rhs

cli/tests/arm/vm/STR+32.litmus.toml

@@ -1,8 +1,8 @@
 arch = "AArch64"
 name = "STR+32"
-symbolic = ["x"]
 
 page_table_setup = """
+virtual x;
 physical pa_x;
 x |-> pa_x;
 *pa_x = 0x000000010000000100000001;