From b6d7725741429143d40e3d895e3ebab1a76e0a90 Mon Sep 17 00:00:00 2001 From: Yeji Han Date: Thu, 2 Jul 2026 16:52:39 +0100 Subject: [PATCH 1/3] feat(Isla): Support page-table symbol alignment - Parse aligned virtual declarations in page_table_setup. - Treat explicit mapping levels as alignment requests for VA and PA symbols. - Apply VA alignment before assembly layout and PA alignment during page-table construction. - Cover the level-2 VA/PA shorthand with a VM fixture. --- cli/lib/isla/allocator.mli | 3 + cli/lib/isla/converter.ml | 57 ++++++++++++++++-- cli/lib/isla/lexer.mll | 1 + cli/lib/isla/page_table/page_table_ast.ml | 8 ++- cli/lib/isla/page_table/page_table_builder.ml | 38 ++++++++++-- cli/lib/isla/parser.mly | 3 + cli/tests/arm/vm/LDR+size+VM.litmus.toml | 24 ++++++++ cli/tests/arm/vm/STR+32.litmus.toml | 22 ------- ...32.litmus.toml => LDR+size+VM.litmus.toml} | 42 +++++++------ cli/tests/errors/errors.t | 7 +++ .../page-table-pa-alignment.litmus.toml | 14 +++++ cli/tests/unit/isla/dune | 2 +- .../unit/isla/page_table_builder_test.ml | 60 +++++++++++++++++++ 13 files changed, 230 insertions(+), 51 deletions(-) create mode 100644 cli/tests/arm/vm/LDR+size+VM.litmus.toml delete mode 100644 cli/tests/arm/vm/STR+32.litmus.toml rename cli/tests/converter/expect/arm/vm/{STR+32.litmus.toml => LDR+size+VM.litmus.toml} (69%) create mode 100644 cli/tests/errors/page-table-pa-alignment.litmus.toml create mode 100644 cli/tests/unit/isla/page_table_builder_test.ml diff --git a/cli/lib/isla/allocator.mli b/cli/lib/isla/allocator.mli index c0fe2e7e..c9214ccd 100644 --- a/cli/lib/isla/allocator.mli +++ b/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 diff --git a/cli/lib/isla/converter.ml b/cli/lib/isla/converter.ml index c2644fa6..5c7e7ffd 100644 --- a/cli/lib/isla/converter.ml +++ b/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} diff --git a/cli/lib/isla/lexer.mll b/cli/lib/isla/lexer.mll index 39fb8f8a..54ed5800 100644 --- a/cli/lib/isla/lexer.mll +++ b/cli/lib/isla/lexer.mll @@ -68,6 +68,7 @@ rule token = parse | ']' { RBRACKET } | ',' { COMMA } | '-' { MINUS } + | "aligned" { ALIGNED } | "virtual" { VIRTUAL } | "physical" { PHYSICAL } | "identity" { IDENTITY } diff --git a/cli/lib/isla/page_table/page_table_ast.ml b/cli/lib/isla/page_table/page_table_ast.ml index 342b85f8..210a0ddd 100644 --- a/cli/lib/isla/page_table/page_table_ast.ml +++ b/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 diff --git a/cli/lib/isla/page_table/page_table_builder.ml b/cli/lib/isla/page_table/page_table_builder.ml index 6f963f9a..17499a68 100644 --- a/cli/lib/isla/page_table/page_table_builder.ml +++ b/cli/lib/isla/page_table/page_table_builder.ml @@ -67,6 +67,7 @@ type t = root : pa; mutable next_table_pa : pa; entries : (pa, descriptor) Hashtbl.t; + mutable declared_pa_names_rev : string list; mutable symbols_pa : (string * pa) list; mutable data_inits : (pa * data_value) list } @@ -77,6 +78,7 @@ let make allocator ~root = entries; root; next_table_pa = root + Allocator.page_size; + declared_pa_names_rev = []; symbols_pa = []; data_inits = [] } @@ -87,11 +89,26 @@ 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 = 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 +214,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 +241,9 @@ 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_pa_names_rev <- + List.rev_append names builder.declared_pa_names_rev + | Page_table_ast.AlignedVirtual _ -> () | Page_table_ast.Mapping {va_name; target; attrs; level} -> let va = match List.assoc_opt va_name symbolic_vas with @@ -264,6 +288,10 @@ let build ~arch ~allocator ~symbolic_vas ~code_pages stmts = add_mapping ~level:2 builder ~va:root ~pa:root Page_table_ast.Data; (* Evaluate each statement, using symbolic VAs to resolve virtual names. *) List.iter (eval_stmt builder ~symbolic_vas) stmts; + (* Materialize PA symbols that were declared but never otherwise used. *) + List.iter + (fun name -> ignore (alloc_pa builder name)) + (List.rev builder.declared_pa_names_rev); (* Add code identity mappings after explicit page-table statements. *) add_code_mappings builder code_pages; (* Put data initializers back in source order. *) diff --git a/cli/lib/isla/parser.mly b/cli/lib/isla/parser.mly index 823b051a..75168784 100644 --- a/cli/lib/isla/parser.mly +++ b/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} diff --git a/cli/tests/arm/vm/LDR+size+VM.litmus.toml b/cli/tests/arm/vm/LDR+size+VM.litmus.toml new file mode 100644 index 00000000..22161110 --- /dev/null +++ b/cli/tests/arm/vm/LDR+size+VM.litmus.toml @@ -0,0 +1,24 @@ +arch = "AArch64" +name = "LDR+size+VM" + +page_table_setup = """ +virtual x y; +aligned 65536 virtual y; +*pa_pad = 0; +physical pa_x; +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" diff --git a/cli/tests/arm/vm/STR+32.litmus.toml b/cli/tests/arm/vm/STR+32.litmus.toml deleted file mode 100644 index 0bdaae36..00000000 --- a/cli/tests/arm/vm/STR+32.litmus.toml +++ /dev/null @@ -1,22 +0,0 @@ -arch = "AArch64" -name = "STR+32" - -page_table_setup = """ -virtual x; -physical pa_x; -x |-> pa_x; -*pa_x = 0x000000010000000100000001; -""" - -[sizes] -pa_x = 12 - -[thread.0] -init = { X1 = "x", SCTLR_EL1 = 1, CurrentEL = 1 } -code = """ -LDR W0,[X1,#8] -""" - -[final] -kind = "exists" -assertion = "0:X0 = 1 & *pa_x = 0x000000010000000100000001" diff --git a/cli/tests/converter/expect/arm/vm/STR+32.litmus.toml b/cli/tests/converter/expect/arm/vm/LDR+size+VM.litmus.toml similarity index 69% rename from cli/tests/converter/expect/arm/vm/STR+32.litmus.toml rename to cli/tests/converter/expect/arm/vm/LDR+size+VM.litmus.toml index 7cdd1d0b..b43e96d3 100644 --- a/cli/tests/converter/expect/arm/vm/STR+32.litmus.toml +++ b/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}]} diff --git a/cli/tests/errors/errors.t b/cli/tests/errors/errors.t index 0bbf7456..e936e2dc 100644 --- a/cli/tests/errors/errors.t +++ b/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: diff --git a/cli/tests/errors/page-table-pa-alignment.litmus.toml b/cli/tests/errors/page-table-pa-alignment.litmus.toml new file mode 100644 index 00000000..462fcdbf --- /dev/null +++ b/cli/tests/errors/page-table-pa-alignment.litmus.toml @@ -0,0 +1,14 @@ +arch = "AArch64" +name = "page-table-pa-alignment" + +page_table_setup = """ +virtual x; +*pa_pad = 0; +*pa_x = 1; +x |-> pa_x at level 2; +""" + +[thread.0] +code = """ +nop +""" diff --git a/cli/tests/unit/isla/dune b/cli/tests/unit/isla/dune index c8b1738b..7ae8ec28 100644 --- a/cli/tests/unit/isla/dune +++ b/cli/tests/unit/isla/dune @@ -1,5 +1,5 @@ (tests - (names assembler_test assertion_test) + (names assembler_test assertion_test page_table_builder_test) (libraries archsem isla test_utils ounit2) (deps (source_tree ../../../../config))) diff --git a/cli/tests/unit/isla/page_table_builder_test.ml b/cli/tests/unit/isla/page_table_builder_test.ml new file mode 100644 index 00000000..64e4f2ce --- /dev/null +++ b/cli/tests/unit/isla/page_table_builder_test.ml @@ -0,0 +1,60 @@ +(******************************************************************************) +(* ArchSem *) +(* *) +(* Copyright (c) 2021 *) +(* Thibaut Pérami, University of Cambridge *) +(* Yeji Han, Seoul National University *) +(* Shreeka Lohani, University of Cambridge *) +(* Zongyuan Liu, Aarhus University *) +(* Nils Lauermann, University of Cambridge *) +(* Jean Pichon-Pharabod, University of Cambridge, Aarhus University *) +(* Brian Campbell, University of Edinburgh *) +(* Alasdair Armstrong, University of Cambridge *) +(* Ben Simner, University of Cambridge *) +(* Peter Sewell, University of Cambridge *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *) +(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *) +(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *) +(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *) +(* COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *) +(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *) +(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS *) +(* OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR *) +(* TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE *) +(* USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* *) +(******************************************************************************) + +(** Unit tests for Isla.Page_table_builder. *) + +open OUnit2 + +let test_materialize_physical_declaration _ = + let layout = + Isla.Page_table_builder.build ~arch:Litmus.Arch_id.Arm + ~allocator:(Isla.Allocator.make ()) ~symbolic_vas:[] ~code_pages:[] + [Isla.Page_table_ast.Physical ["pa_unused"]] + in + assert_bool "physical-only symbol is allocated" + (List.mem_assoc "pa_unused" layout.phys_symbols_pa) + +let tests = + "Isla.Page_table_builder" + >::: [ "materialize physical declaration" + >:: test_materialize_physical_declaration + ] + +let () = run_test_tt_main tests From 79ee16307ca0de40f9347bb7a5b1f3f9d94a13fa Mon Sep 17 00:00:00 2001 From: Yeji Han Date: Thu, 2 Jul 2026 15:30:07 +0100 Subject: [PATCH 2/3] feat(Isla): Support named page-table roots - Parse named s1table/s2table roots with explicit bases. - Keep explicit roots reserved while building page tables. - Cover switching between named roots with a VM smoke test. --- cli/lib/isla/converter.ml | 8 +- cli/lib/isla/lexer.mll | 4 + cli/lib/isla/page_table/page_table_ast.ml | 10 + cli/lib/isla/page_table/page_table_builder.ml | 178 ++++++++++++------ .../isla/page_table/page_table_builder.mli | 8 +- cli/lib/isla/parser.mly | 16 ++ cli/tests/arm/vm/SwitchTTBR+VM.litmus.toml | 30 +++ .../expect/arm/vm/SwitchTTBR+VM.litmus.toml | 161 ++++++++++++++++ .../unit/isla/page_table_builder_test.ml | 2 +- 9 files changed, 357 insertions(+), 60 deletions(-) create mode 100644 cli/tests/arm/vm/SwitchTTBR+VM.litmus.toml create mode 100644 cli/tests/converter/expect/arm/vm/SwitchTTBR+VM.litmus.toml diff --git a/cli/lib/isla/converter.ml b/cli/lib/isla/converter.ml index 5c7e7ffd..e260cb5c 100644 --- a/cli/lib/isla/converter.ml +++ b/cli/lib/isla/converter.ml @@ -331,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 -> @@ -419,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 diff --git a/cli/lib/isla/lexer.mll b/cli/lib/isla/lexer.mll index 54ed5800..cc282cfc 100644 --- a/cli/lib/isla/lexer.mll +++ b/cli/lib/isla/lexer.mll @@ -66,6 +66,8 @@ rule token = parse | ';' { SEMICOLON } | '[' { LBRACKET } | ']' { RBRACKET } + | '{' { LBRACE } + | '}' { RBRACE } | ',' { COMMA } | '-' { MINUS } | "aligned" { ALIGNED } @@ -79,6 +81,8 @@ rule token = parse | "data" { DATA } | "invalid" { INVALID } | "table" { TABLE } + | "s1table" { S1TABLE } + | "s2table" { S2TABLE } | "at" { AT } | "level" { LEVEL } | "true" { TRUE } diff --git a/cli/lib/isla/page_table/page_table_ast.ml b/cli/lib/isla/page_table/page_table_ast.ml index 210a0ddd..1b5c6ff8 100644 --- a/cli/lib/isla/page_table/page_table_ast.ml +++ b/cli/lib/isla/page_table/page_table_ast.ml @@ -48,6 +48,10 @@ type attr = | Code | Data +type table_stage = + | S1 + | S2 + type descriptor_field = { name : string; value : Z.t @@ -93,3 +97,9 @@ type stmt = { addr : Z.t; attr : attr } + | TableBlock of + { stage : table_stage; + name : string; + base : Z.t; + body : stmt list + } diff --git a/cli/lib/isla/page_table/page_table_builder.ml b/cli/lib/isla/page_table/page_table_builder.ml index 17499a68..5dd722c0 100644 --- a/cli/lib/isla/page_table/page_table_builder.ml +++ b/cli/lib/isla/page_table/page_table_builder.ml @@ -53,8 +53,8 @@ type data_value = Z.t type layout = { root : pa; table_entries : (pa * descriptor) list; - symbols_pa : (string * pa) list; - phys_symbols_pa : (string * pa) list; + table_symbols_pa : (string * pa) list; + data_symbols_pa : (string * pa) list; data_inits : (pa * data_value) list } @@ -62,24 +62,39 @@ exception Error of string let error fmt = Printf.ksprintf (fun msg -> raise (Error msg)) fmt +type table_root = + { stage : Page_table_ast.table_stage; + name : string option; + base : pa; + mutable next_table_pa : pa + } + type t = { allocator : Allocator.t; - root : pa; - mutable next_table_pa : pa; + default_root : table_root; + mutable roots : table_root list; + mutable table_pages : pa list; entries : (pa, descriptor) Hashtbl.t; mutable declared_pa_names_rev : string list; - mutable symbols_pa : (string * pa) list; + mutable data_symbols_pa : (string * pa) list; mutable data_inits : (pa * data_value) list } let make allocator ~root = - let entries = Hashtbl.create 256 in + let default_root = + { stage = Page_table_ast.S1; + name = None; + base = root; + next_table_pa = root + Allocator.page_size + } + in { allocator; - entries; - root; - next_table_pa = root + Allocator.page_size; + default_root; + roots = [default_root]; + table_pages = [root]; + entries = Hashtbl.create 256; declared_pa_names_rev = []; - symbols_pa = []; + data_symbols_pa = []; data_inits = [] } @@ -89,8 +104,8 @@ let check_arch = function error "page_table: only AArch64 is supported, got %s" (Litmus.Arch_id.to_string arch) -let alloc_pa ?(alignment = Allocator.page_size) ?mapping_level builder name = - match List.assoc_opt name builder.symbols_pa with +let alloc_physical ?(alignment = Allocator.page_size) ?mapping_level builder name = + match List.assoc_opt name builder.data_symbols_pa with | Some addr -> ( if addr mod alignment = 0 then addr else @@ -109,17 +124,62 @@ let alloc_pa ?(alignment = Allocator.page_size) ?mapping_level builder name = Allocator.alloc_aligned builder.allocator ~size:Allocator.page_size ~alignment in - builder.symbols_pa <- (name, addr) :: builder.symbols_pa; + builder.data_symbols_pa <- (name, addr) :: builder.data_symbols_pa; addr (** {1 Table page allocation} *) -(** Allocate a fresh table page. *) -let create_table_page builder = - if builder.next_table_pa >= builder.root + Allocator.big_size then - error "page_table: 2MB page-table pool exhausted"; - let addr = builder.next_table_pa in - builder.next_table_pa <- addr + Allocator.page_size; +let addr_of_z name addr = + try Z.to_int addr + with Z.Overflow -> + error "page_table: %s out of range: %s" name (Z.format "%#x" addr) + +let find_root builder ~stage ~name = + match + List.find_opt + (fun root -> root.stage = stage && root.name = Some name) + builder.roots + with + | Some root -> root + | None -> error "page_table: unknown table root: %s" name + +let reserve_root builder ~stage ~name ~base = + let base = addr_of_z "table base" base in + if base mod Allocator.page_size <> 0 then + error "page_table: table base 0x%x is not page aligned" base; + if + List.exists + (fun root -> root.stage = stage && root.name = Some name) + builder.roots + then error "page_table: duplicate table root: %s" name; + if List.exists (fun root -> root.base = base) builder.roots then + error "page_table: duplicate table base: 0x%x" base; + let root = + {stage; name = Some name; base; next_table_pa = base + Allocator.page_size} + in + builder.roots <- root :: builder.roots; + builder.table_pages <- base :: builder.table_pages + +let rec reserve_table_roots builder = function + | [] -> () + | Page_table_ast.TableBlock {stage; name; base; body} :: stmts -> + reserve_root builder ~stage ~name ~base; + reserve_table_roots builder body; + reserve_table_roots builder stmts + | _ :: stmts -> reserve_table_roots builder stmts + +(** Allocate a fresh table page in [root]'s 2MB table pool. *) +let create_table_page builder root = + let rec find_free addr = + if addr >= root.base + Allocator.big_size then + error "page_table: 2MB page-table pool exhausted"; + if List.mem addr builder.table_pages then + find_free (addr + Allocator.page_size) + else addr + in + let addr = find_free root.next_table_pa in + root.next_table_pa <- addr + Allocator.page_size; + builder.table_pages <- addr :: builder.table_pages; addr let entry_addr table_addr idx = table_addr + (idx * Desc.entry_size) @@ -138,8 +198,8 @@ let write_entry builder table_addr idx desc = ); Hashtbl.replace builder.entries slot_addr desc -let create_child_table builder parent_addr idx = - let child_addr = create_table_page builder in +let create_child_table builder root parent_addr idx = + let child_addr = create_table_page builder root in try write_entry builder parent_addr idx (Desc.table_descriptor child_addr); child_addr @@ -155,10 +215,10 @@ let child_table_addr builder table_addr idx = (** {1 Mapping path construction} *) (** Reuse an existing child table descriptor, or install a new child table. *) -let ensure_child_table builder parent_addr idx = +let ensure_child_table builder root parent_addr idx = match child_table_addr builder parent_addr idx with | Some next_addr -> next_addr - | None -> create_child_table builder parent_addr idx + | None -> create_child_table builder root parent_addr idx (** Align a VA or PA for the descriptor level being inserted. *) let check_aligned_at_level name level addr = @@ -169,7 +229,7 @@ let check_aligned_at_level name level addr = level (** Write an encoded descriptor at [va], allocating intermediate tables. *) -let write_descriptor ?(level = Desc.last_level) builder ~va desc = +let write_descriptor ?(level = Desc.last_level) builder ~root ~va desc = let rec walk table_addr current_level = let idx = Desc.va_index va current_level in if current_level = level then @@ -180,24 +240,32 @@ let write_descriptor ?(level = Desc.last_level) builder ~va desc = 0x%Lx, new descriptor 0x%Lx" va existing desc else - let child_addr = ensure_child_table builder table_addr idx in + let child_addr = ensure_child_table builder root table_addr idx in walk child_addr (current_level + 1) in - walk builder.root Desc.root_level + walk root.base Desc.root_level (** Add the requested mapping, allocating intermediate tables on demand. *) -let add_mapping ?(fields = []) ?(level = Desc.last_level) builder ~va ~pa kind = +let add_mapping + ?(fields = []) + ?(level = Desc.last_level) + builder + ~root + ~va + ~pa + kind + = let va = check_aligned_at_level "VA" level va in let pa = check_aligned_at_level "PA" level pa in let desc = try Desc.make_descriptor ~fields ~level ~oa:pa ~kind () with Failure msg -> error "page_table: %s" msg in - write_descriptor ~level builder ~va desc + write_descriptor ~level builder ~root ~va desc -let add_code_mappings builder code_pages = +let add_code_mappings builder ~root code_pages = List.iter - (fun addr -> add_mapping builder ~va:addr ~pa:addr Page_table_ast.Code) + (fun addr -> add_mapping builder ~root ~va:addr ~pa:addr Page_table_ast.Code) code_pages (** {1 Statement evaluation} *) @@ -209,24 +277,19 @@ let check_table_level = function Desc.root_level (Desc.last_level - 1) | Some level -> level -let addr_of_z name addr = - try Z.to_int 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 +let eval_mapping_target ?level ?(attrs = []) builder ~root ~va = function | Page_table_ast.PaName pa_name -> 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 + let pa = alloc_physical ?alignment ?mapping_level:level builder pa_name in + add_mapping ?level ~fields:attrs builder ~root ~va ~pa Page_table_ast.Data | Page_table_ast.Invalid -> if attrs <> [] then error "page_table: descriptor fields are only supported on PA mappings"; - write_descriptor ?level builder ~va 0L + write_descriptor ?level builder ~root ~va 0L | Page_table_ast.Table addr -> if attrs <> [] then error "page_table: descriptor fields are only supported on PA mappings"; @@ -236,9 +299,9 @@ let eval_mapping_target ?level ?(attrs = []) builder ~va = function try Desc.table_descriptor table_pa with Failure msg -> error "page_table: %s" msg in - write_descriptor ~level builder ~va desc + write_descriptor ~level builder ~root ~va desc -let eval_stmt builder ~symbolic_vas = function +let rec eval_stmt builder ~symbolic_vas ~root = function | Page_table_ast.Virtual _ -> () | Page_table_ast.Physical names -> builder.declared_pa_names_rev <- @@ -250,14 +313,17 @@ let eval_stmt builder ~symbolic_vas = function | Some addr -> addr | None -> error "page_table: undeclared VA: %s" va_name in - eval_mapping_target ?level ~attrs builder ~va target + eval_mapping_target ?level ~attrs builder ~root ~va target | Page_table_ast.MaybeMapping _ -> () | Page_table_ast.DataInit {pa_name; value} -> - let pa = alloc_pa builder pa_name in + let pa = alloc_physical builder pa_name in builder.data_inits <- (pa, value) :: builder.data_inits | Page_table_ast.IdentityMapping {addr; attr} -> let addr = addr_of_z "address" addr in - add_mapping builder ~va:addr ~pa:addr attr + add_mapping builder ~root ~va:addr ~pa:addr attr + | Page_table_ast.TableBlock {stage; name; base = _; body} -> + let root = find_root builder ~stage ~name in + List.iter (eval_stmt builder ~symbolic_vas ~root) body (** {1 Layout construction} *) @@ -270,13 +336,17 @@ let to_entries builder = (** Freeze the builder state into the immutable layout used downstream. *) let to_layout builder = - let root = builder.root in + let root = builder.default_root.base in let table_entries = to_entries builder in - (* Generated PA alias for the root translation-table page. *) - let symbols_pa = ("page_table_base", root) :: builder.symbols_pa in - let phys_symbols_pa = List.rev builder.symbols_pa in + let table_symbols_pa = + List.filter_map + (fun root -> Option.map (fun name -> (name, root.base)) root.name) + builder.roots + |> List.rev + in + let data_symbols_pa = List.rev builder.data_symbols_pa in let data_inits = builder.data_inits in - {root; table_entries; symbols_pa; phys_symbols_pa; data_inits} + {root; table_entries; table_symbols_pa; data_symbols_pa; data_inits} let build ~arch ~allocator ~symbolic_vas ~code_pages stmts = check_arch arch; @@ -284,16 +354,18 @@ let build ~arch ~allocator ~symbolic_vas ~code_pages stmts = (* [root] is the TTBR0 value and the base of the 2MB page-table pool. *) let root = Allocator.alloc_big allocator in let builder = make allocator ~root in + reserve_table_roots builder stmts; (* Page tables are identity-mapped so generated PTE VAs can access them. *) - add_mapping ~level:2 builder ~va:root ~pa:root Page_table_ast.Data; + add_mapping ~level:2 builder ~root:builder.default_root ~va:root ~pa:root + Page_table_ast.Data; (* Evaluate each statement, using symbolic VAs to resolve virtual names. *) - List.iter (eval_stmt builder ~symbolic_vas) stmts; + List.iter (eval_stmt builder ~symbolic_vas ~root:builder.default_root) stmts; (* Materialize PA symbols that were declared but never otherwise used. *) List.iter - (fun name -> ignore (alloc_pa builder name)) + (fun name -> ignore (alloc_physical builder name)) (List.rev builder.declared_pa_names_rev); (* Add code identity mappings after explicit page-table statements. *) - add_code_mappings builder code_pages; + add_code_mappings builder ~root:builder.default_root code_pages; (* Put data initializers back in source order. *) builder.data_inits <- List.rev builder.data_inits; to_layout builder diff --git a/cli/lib/isla/page_table/page_table_builder.mli b/cli/lib/isla/page_table/page_table_builder.mli index 55d9a3ac..337e6cc2 100644 --- a/cli/lib/isla/page_table/page_table_builder.mli +++ b/cli/lib/isla/page_table/page_table_builder.mli @@ -54,10 +54,10 @@ type data_value = Z.t type layout = { root : pa; table_entries : (pa * descriptor) list; - (* Mapping from PA-side symbols to concrete PAs: pa_x -> PA. *) - symbols_pa : (string * pa) list; - (* PA-side data symbols, excluding generated root aliases. *) - phys_symbols_pa : (string * pa) list; + (* PA-side table root symbols. *) + table_symbols_pa : (string * pa) list; + (* PA-side data symbols. *) + data_symbols_pa : (string * pa) list; (* [*pa = value] initialisers resolved to concrete PAs. *) data_inits : (pa * data_value) list } diff --git a/cli/lib/isla/parser.mly b/cli/lib/isla/parser.mly index 75168784..32b612d2 100644 --- a/cli/lib/isla/parser.mly +++ b/cli/lib/isla/parser.mly @@ -57,6 +57,8 @@ %token SEMICOLON ";" %token LBRACKET "[" %token RBRACKET "]" +%token LBRACE "{" +%token RBRACE "}" %token MAPS_TO "|->" %token MAYBE_MAPS_TO "?->" %token ALIGNED @@ -70,6 +72,8 @@ %token DATA %token INVALID %token TABLE +%token S1TABLE +%token S2TABLE %token AT %token LEVEL %token TRUE @@ -83,12 +87,14 @@ %start binding %start page_table_setup %type page_table_stmt page_table_stmt_inner + page_table_block %type page_table_mapping_rhs %type page_table_mapping_target %type page_table_attr %type page_table_descriptor_attrs %type page_table_mapping_level +%type page_table_stage %type kw_name %% @@ -104,6 +110,7 @@ page_table_setup: page_table_stmt: | s = page_table_stmt_inner; ";" { s } + | b = page_table_block; option(";") { b } page_table_stmt_inner: | VIRTUAL; names = nonempty_list(IDENT) @@ -125,6 +132,15 @@ page_table_stmt_inner: | IDENTITY; addr = NUM; WITH; attr = page_table_attr { Page_table_ast.IdentityMapping {addr; attr} } +page_table_block: + | stage = page_table_stage; name = IDENT; base = NUM; "{"; + body = list(page_table_stmt); "}" + { Page_table_ast.TableBlock {stage; name; base; body} } + +page_table_stage: + | S1TABLE { Page_table_ast.S1 } + | S2TABLE { Page_table_ast.S2 } + page_table_mapping_rhs: | target = page_table_mapping_target; attrs = option(page_table_descriptor_attrs); diff --git a/cli/tests/arm/vm/SwitchTTBR+VM.litmus.toml b/cli/tests/arm/vm/SwitchTTBR+VM.litmus.toml new file mode 100644 index 00000000..33f31466 --- /dev/null +++ b/cli/tests/arm/vm/SwitchTTBR+VM.litmus.toml @@ -0,0 +1,30 @@ +arch = "AArch64" +name = "SwitchTTBR+VM" +symbolic = ["x"] + +page_table_setup = """ +physical pa0 pa1; +*pa0 = 0; +*pa1 = 1; + +s1table table0 0x2C0000 { + identity 0x1000 with code; + x |-> pa0; +} + +s1table table1 0x300000 { + identity 0x1000 with code; + x |-> pa1; +} +""" + +[thread.0] +init = { X0 = "table1", X2 = "x", TTBR0_EL1 = "table0", SCTLR_EL1 = 1, CurrentEL = 1 } +code = """ +MSR TTBR0_EL1, X0 +MRS X3, TTBR0_EL1 +LDR X1, [X2] +""" + +[final] +assertion = "0:X1 = 1 & 0:X3 = table1" diff --git a/cli/tests/converter/expect/arm/vm/SwitchTTBR+VM.litmus.toml b/cli/tests/converter/expect/arm/vm/SwitchTTBR+VM.litmus.toml new file mode 100644 index 00000000..9e444ef7 --- /dev/null +++ b/cli/tests/converter/expect/arm/vm/SwitchTTBR+VM.litmus.toml @@ -0,0 +1,161 @@ +arch = "Arm" +name = "SwitchTTBR+VM" + +[[memory]] + sym = "__thread0" + kind = "code" + addr = 0x1000 + step = 4 + data = [0xd5182000, 0xd5382003, 0xf9400041] + +[[memory]] + kind = "pagetable" + addr = 0x200000 + step = 8 + data = 0x201003 + +[[memory]] + kind = "pagetable" + addr = 0x201000 + step = 8 + data = 0x202003 + +[[memory]] + kind = "pagetable" + addr = 0x202000 + step = 8 + data = 0x203003 + +[[memory]] + kind = "pagetable" + addr = 0x202008 + step = 8 + data = 0x200441 + +[[memory]] + kind = "pagetable" + addr = 0x203008 + step = 8 + data = 0x14c3 + +[[memory]] + kind = "pagetable" + addr = 0x2c0000 + step = 8 + data = 0x2c1003 + +[[memory]] + kind = "pagetable" + addr = 0x2c1000 + step = 8 + data = 0x2c2003 + +[[memory]] + kind = "pagetable" + addr = 0x2c2000 + step = 8 + data = 0x2c3003 + +[[memory]] + kind = "pagetable" + addr = 0x2c3008 + step = 8 + data = 0x14c3 + +[[memory]] + kind = "pagetable" + addr = 0x2c3010 + step = 8 + data = 0x400443 + +[[memory]] + kind = "pagetable" + addr = 0x300000 + step = 8 + data = 0x301003 + +[[memory]] + kind = "pagetable" + addr = 0x301000 + step = 8 + data = 0x302003 + +[[memory]] + kind = "pagetable" + addr = 0x302000 + step = 8 + data = 0x303003 + +[[memory]] + kind = "pagetable" + addr = 0x303008 + step = 8 + data = 0x14c3 + +[[memory]] + kind = "pagetable" + addr = 0x303010 + step = 8 + data = 0x401443 + +[[memory]] + sym = "pa0" + addr = 0x400000 + step = 8 + data = 0 + +[[memory]] + sym = "pa1" + addr = 0x401000 + step = 8 + data = 1 + +[thread] + +[thread."0"] + breakpoints = [0x100c] + +[thread."0".regs] + _PC = 0x1000 + "R0" = 0x300000 + "R2" = 0x2000 + "TTBR0_EL1" = 0x2c0000 + "SCTLR_EL1" = 1 + CurrentEL = 1 + "R1" = 0 + "R3" = 0 + "R4" = 0 + "R5" = 0 + "R6" = 0 + "R7" = 0 + "R8" = 0 + "R9" = 0 + "R10" = 0 + "R11" = 0 + "R12" = 0 + "R13" = 0 + "R14" = 0 + "R15" = 0 + "R16" = 0 + "R17" = 0 + "R18" = 0 + "R19" = 0 + "R20" = 0 + "R21" = 0 + "R22" = 0 + "R23" = 0 + "R24" = 0 + "R25" = 0 + "R26" = 0 + "R27" = 0 + "R28" = 0 + "R29" = 0 + "R30" = 0 + "TCR_EL1" = 0 + "ID_AA64MMFR1_EL1" = 0 + SPSel = 0 + NZCV = 0 + DAIF = 0 + +[final] + assertion = {and = [{"0:X1" = 1}, {"0:X3" = 0x300000}]} diff --git a/cli/tests/unit/isla/page_table_builder_test.ml b/cli/tests/unit/isla/page_table_builder_test.ml index 64e4f2ce..6561de9b 100644 --- a/cli/tests/unit/isla/page_table_builder_test.ml +++ b/cli/tests/unit/isla/page_table_builder_test.ml @@ -49,7 +49,7 @@ let test_materialize_physical_declaration _ = [Isla.Page_table_ast.Physical ["pa_unused"]] in assert_bool "physical-only symbol is allocated" - (List.mem_assoc "pa_unused" layout.phys_symbols_pa) + (List.mem_assoc "pa_unused" layout.data_symbols_pa) let tests = "Isla.Page_table_builder" From 05e08883cea81019f4d190807ed1b167b4783f53 Mon Sep 17 00:00:00 2001 From: Yeji Han Date: Fri, 3 Jul 2026 14:43:42 +0100 Subject: [PATCH 3/3] feat(Isla): Accept default page-table option - Parse option default_tables = true statements in page_table_setup. - Preserve Isla compatibility while keeping the option as a builder no-op. - Reject default_tables = false and unsupported page-table option names. - Cover accepted and rejected values with parser unit tests. --- cli/lib/isla/lexer.mll | 1 + cli/lib/isla/page_table/page_table_ast.ml | 2 + cli/lib/isla/page_table/page_table_builder.ml | 1 + cli/lib/isla/parser.mly | 13 ++++ cli/tests/unit/isla/dune | 6 +- cli/tests/unit/isla/page_table_test.ml | 65 +++++++++++++++++++ 6 files changed, 87 insertions(+), 1 deletion(-) create mode 100644 cli/tests/unit/isla/page_table_test.ml diff --git a/cli/lib/isla/lexer.mll b/cli/lib/isla/lexer.mll index cc282cfc..0ea21c34 100644 --- a/cli/lib/isla/lexer.mll +++ b/cli/lib/isla/lexer.mll @@ -71,6 +71,7 @@ rule token = parse | ',' { COMMA } | '-' { MINUS } | "aligned" { ALIGNED } + | "option" { OPTION } | "virtual" { VIRTUAL } | "physical" { PHYSICAL } | "identity" { IDENTITY } diff --git a/cli/lib/isla/page_table/page_table_ast.ml b/cli/lib/isla/page_table/page_table_ast.ml index 1b5c6ff8..495cf435 100644 --- a/cli/lib/isla/page_table/page_table_ast.ml +++ b/cli/lib/isla/page_table/page_table_ast.ml @@ -63,6 +63,8 @@ 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. *) diff --git a/cli/lib/isla/page_table/page_table_builder.ml b/cli/lib/isla/page_table/page_table_builder.ml index 5dd722c0..393253fa 100644 --- a/cli/lib/isla/page_table/page_table_builder.ml +++ b/cli/lib/isla/page_table/page_table_builder.ml @@ -302,6 +302,7 @@ let eval_mapping_target ?level ?(attrs = []) builder ~root ~va = function write_descriptor ~level builder ~root ~va desc let rec eval_stmt builder ~symbolic_vas ~root = function + | Page_table_ast.OptionDefaultTablesTrue -> () | Page_table_ast.Virtual _ -> () | Page_table_ast.Physical names -> builder.declared_pa_names_rev <- diff --git a/cli/lib/isla/parser.mly b/cli/lib/isla/parser.mly index 32b612d2..e6d8e1b3 100644 --- a/cli/lib/isla/parser.mly +++ b/cli/lib/isla/parser.mly @@ -61,6 +61,7 @@ %token RBRACE "}" %token MAPS_TO "|->" %token MAYBE_MAPS_TO "?->" +%token OPTION %token ALIGNED %token VIRTUAL %token PHYSICAL @@ -93,6 +94,7 @@ %type page_table_mapping_target %type page_table_attr %type page_table_descriptor_attrs +%type page_table_bool %type page_table_mapping_level %type page_table_stage %type kw_name @@ -113,6 +115,13 @@ page_table_stmt: | b = page_table_block; option(";") { b } page_table_stmt_inner: + | OPTION; name = IDENT; "="; value = page_table_bool + { if name <> "default_tables" then + failwith ("unsupported page-table option: " ^ name); + if not value then + failwith "unsupported page-table option: default_tables = false"; + Page_table_ast.OptionDefaultTablesTrue + } | VIRTUAL; names = nonempty_list(IDENT) { Page_table_ast.Virtual names } | PHYSICAL; names = nonempty_list(IDENT) @@ -173,6 +182,10 @@ page_table_mapping_level: with Z.Overflow -> failwith "page-table level is out of range" } +page_table_bool: + | TRUE { true } + | FALSE { false } + prop: | e1 = prop; "|"; e2 = prop { Or [e1; e2] } | e1 = prop; "&"; e2 = prop { And [e1; e2] } diff --git a/cli/tests/unit/isla/dune b/cli/tests/unit/isla/dune index 7ae8ec28..c88e42b4 100644 --- a/cli/tests/unit/isla/dune +++ b/cli/tests/unit/isla/dune @@ -1,5 +1,9 @@ (tests - (names assembler_test assertion_test page_table_builder_test) + (names + assembler_test + assertion_test + page_table_builder_test + page_table_test) (libraries archsem isla test_utils ounit2) (deps (source_tree ../../../../config))) diff --git a/cli/tests/unit/isla/page_table_test.ml b/cli/tests/unit/isla/page_table_test.ml new file mode 100644 index 00000000..93e8b765 --- /dev/null +++ b/cli/tests/unit/isla/page_table_test.ml @@ -0,0 +1,65 @@ +(******************************************************************************) +(* ArchSem *) +(* *) +(* Copyright (c) 2021 *) +(* Thibaut Pérami, University of Cambridge *) +(* Yeji Han, Seoul National University *) +(* Shreeka Lohani, University of Cambridge *) +(* Zongyuan Liu, Aarhus University *) +(* Nils Lauermann, University of Cambridge *) +(* Jean Pichon-Pharabod, University of Cambridge, Aarhus University *) +(* Brian Campbell, University of Edinburgh *) +(* Alasdair Armstrong, University of Cambridge *) +(* Ben Simner, University of Cambridge *) +(* Peter Sewell, University of Cambridge *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *) +(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *) +(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *) +(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *) +(* COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *) +(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *) +(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS *) +(* OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR *) +(* TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE *) +(* USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* *) +(******************************************************************************) + +(** Unit tests for the Isla page-table setup parser. *) + +open OUnit2 + +let parse input = + let lexbuf = Lexing.from_string input in + Isla.Parser.page_table_setup Isla.Lexer.token lexbuf + +let test_default_tables_true _ = + assert_equal + [Isla.Page_table_ast.OptionDefaultTablesTrue] + (parse "option default_tables = true;") + +let test_default_tables_false _ = + assert_raises (Failure "unsupported page-table option: default_tables = false") + (fun () -> parse "option default_tables = false;" + ) + +let tests = + "Isla.Page_table" + >::: [ "accept default_tables = true" >:: test_default_tables_true; + "reject default_tables = false" >:: test_default_tables_false + ] + +let () = run_test_tt_main tests