From e230eb789da04100201c11be4b1d9158e13aa59b Mon Sep 17 00:00:00 2001 From: Yeji Han Date: Thu, 27 Aug 2026 13:00:24 +0900 Subject: [PATCH] feat(Isla): Support named page-table roots - Parse nested s1table and s2table blocks whose explicit bases are actual physical addresses. - Reserve named roots and explicit table targets before allocating shared child-table pages. - Build code and page-table arena mappings in every root while keeping named roots available as term symbols. - Track Stage-2 roots separately and document the remaining Stage-2 descriptor-encoding work. --- cli/lib/isla/converter.ml | 89 +++++++--- cli/lib/isla/lexer.mll | 4 + cli/lib/isla/page_table/page_table_ast.ml | 11 ++ cli/lib/isla/page_table/page_table_builder.ml | 149 +++++++++++----- .../isla/page_table/page_table_builder.mli | 6 +- cli/lib/isla/parser.mly | 16 ++ cli/tests/arm/vm/SwitchTTBR+VM.litmus.toml | 30 ++++ .../expect/arm/vm/SwitchTTBR+VM.litmus.toml | 167 ++++++++++++++++++ 8 files changed, 393 insertions(+), 79 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 d6be6326..e2c26f30 100644 --- a/cli/lib/isla/converter.ml +++ b/cli/lib/isla/converter.ml @@ -134,12 +134,15 @@ 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 + let rec collect names = function + | [] -> names + | Page_table_ast.Virtual stmt_names :: stmts -> + collect (List.fold_left add names stmt_names) stmts + | Page_table_ast.TableBlock {body; _} :: stmts -> + collect (collect names body) stmts + | _ :: stmts -> collect names stmts + in + collect ir.Ir.symbolic ir.Ir.page_table_setup let checked_virtual_alignment alignment = let alignment = @@ -160,25 +163,23 @@ let checked_mapping_alignment 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 + let rec collect = function + | [] -> [] + | Page_table_ast.AlignedVirtual {alignment; names} :: stmts -> + 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 @ collect stmts + | Page_table_ast.Mapping {va_name; level = Some level; _} :: stmts -> + (va_name, checked_mapping_alignment level) :: collect stmts + | Page_table_ast.TableBlock {body; _} :: stmts -> collect body @ collect stmts + | _ :: stmts -> collect stmts in + let alignment_requests = collect ir.Ir.page_table_setup in let alignment_for name = List.fold_left (fun best (aligned_name, alignment) -> @@ -196,6 +197,30 @@ let table_base = Allocator.big_size let data_base = table_base + Allocator.big_size +let checked_table_root_page value = + let addr = + try Z.to_int value + with Z.Overflow -> + eval_error Page_table_setup "page_table: table base is out of range" + in + if addr mod Allocator.page_size <> 0 then + eval_error Page_table_setup "page_table: table base 0x%x is not page aligned" + addr; + if addr < table_base || addr >= data_base then + eval_error Page_table_setup + "page_table: table base 0x%x is outside table storage [0x%x, 0x%x)" addr + table_base data_base; + addr + +(* Named roots occupy fixed pages in the shared table arena. Reserve those + pages before allocating the default root and child tables. *) +let rec table_root_pages = function + | [] -> [] + | Page_table_ast.TableBlock {base; body; _} :: stmts -> + checked_table_root_page base + :: (table_root_pages body @ table_root_pages stmts) + | _ :: stmts -> table_root_pages stmts + (* Build assembly input after assigning concrete addresses to every section and symbolic location. *) let to_assembly_input ~code_allocator ~symbol_allocator (ir : Ir.t) : @@ -335,7 +360,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 -> @@ -423,7 +452,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 @@ -470,13 +499,15 @@ let to_testrepr ~filename (ir : Ir.t) : Testrepr.t = 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 table_allocator = + make_arena ~reserved:(table_root_pages ir.page_table_setup) table_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 + build_page_table_setup ir ~symbol_allocator ~table_allocator + ~table_block:table_base asm_result in (asm_input, asm_result, Some page_table) in 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 4eb54d4d..7ab700ff 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,10 @@ type stmt = { addr : Z.t; attr : attr } + (* [s1table name 0x280000 { ... }] defines a root at that actual PA. *) + | 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 5a1e6ac8..409c9216 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,31 +62,40 @@ exception Error of string let error fmt = Printf.ksprintf (fun msg -> raise (Error msg)) fmt +type table_root = + { name : string option; + base : pa + } + type t = { (* Allocates physical addresses for data symbols. *) symbol_allocator : Allocator.t; (* Allocates root and child translation-table pages. *) table_allocator : Allocator.t; - (* Root translation-table address. *) - root : pa; + (* Default root translation-table used when statements are not nested in a + named table block. *) + default_root : table_root; + (* Named translation-table roots. *) + mutable named_roots : table_root list; (* Page-table descriptors, keyed by their physical addresses. *) entries : (pa, descriptor) Hashtbl.t; (* Required alignment for each physical-address symbol. *) pa_alignments : (string * int) list; (* PA names and their allocated physical addresses. *) - mutable symbols_pa : (string * pa) list; + mutable data_symbols_pa : (string * pa) list; (* Initial data values, keyed by their allocated PAs. *) mutable data_inits : (pa * data_value) list } let make ~symbol_allocator ~table_allocator ~pa_alignments ~root = - let entries = Hashtbl.create 256 in + let default_root = {name = None; base = root} in { symbol_allocator; table_allocator; - entries; - root; + default_root; + named_roots = []; + entries = Hashtbl.create 256; pa_alignments; - symbols_pa = []; + data_symbols_pa = []; data_inits = [] } @@ -103,7 +112,7 @@ let alloc_pa ?(alignment = Allocator.page_size) ?mapping_level builder name = |> Option.value ~default:Allocator.page_size ) in - match List.assoc_opt name builder.symbols_pa with + match List.assoc_opt name builder.data_symbols_pa with | Some addr -> ( if addr mod alignment = 0 then addr else @@ -122,12 +131,33 @@ let alloc_pa ?(alignment = Allocator.page_size) ?mapping_level builder name = Allocator.alloc_aligned builder.symbol_allocator ~size:alignment ~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} *) +(** {1 Table roots and page allocation} *) + +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 table_storage_base = Allocator.big_size + +let table_storage_limit = table_storage_base + Allocator.big_size + +let check_table_addr name addr = + if addr < table_storage_base || addr >= table_storage_limit then + error "page_table: %s 0x%x is outside table storage [0x%x, 0x%x)" name addr + table_storage_base table_storage_limit + +let table_addr name value = + let addr = addr_of_z name value in + if addr mod Allocator.page_size <> 0 then + error "page_table: %s 0x%x is not page aligned" name addr; + check_table_addr name addr; + addr -(** Allocate a fresh table page. *) +(** Allocate a fresh child translation-table page. *) let create_table_page builder = let addr = try Allocator.alloc_page builder.table_allocator @@ -182,7 +212,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 @@ -196,17 +226,30 @@ let write_descriptor ?(level = Desc.last_level) builder ~va desc = let child_addr = ensure_child_table builder 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 initialise_root builder ~table_block root = + add_mapping ~level:2 builder ~root ~va:0 ~pa:0 Page_table_ast.Code; + add_mapping ~level:2 builder ~root ~va:table_block ~pa:table_block + Page_table_ast.Data (** {1 Statement evaluation} *) @@ -217,26 +260,21 @@ 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 pa_alignment_requests stmts = - let requests = - List.filter_map - (function - | Page_table_ast.Mapping - {target = Page_table_ast.PaName name; level = Some level; _} -> - Some (name, mapping_alignment level) - | _ -> None - ) - stmts + let rec collect = function + | [] -> [] + | Page_table_ast.Mapping + {target = Page_table_ast.PaName name; level = Some level; _} + :: stmts -> + (name, mapping_alignment level) :: collect stmts + | Page_table_ast.TableBlock {body; _} :: stmts -> collect body @ collect stmts + | _ :: stmts -> collect stmts in + let requests = collect stmts in List.fold_left (fun alignments (name, alignment) -> let previous = @@ -247,27 +285,27 @@ let pa_alignment_requests stmts = ) [] requests -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 + 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"; let level = check_table_level level in - let table_pa = addr_of_z "table address" addr in + let table_pa = table_addr "table address" addr in let desc = 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 ~table_block ~root = function | Page_table_ast.Virtual _ -> () | Page_table_ast.Physical _ -> () | Page_table_ast.AlignedVirtual _ -> () @@ -277,7 +315,7 @@ 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 @@ -289,7 +327,19 @@ let eval_stmt builder ~symbolic_vas = function addr | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Data} -> let addr = addr_of_z "address" addr in - add_mapping builder ~va:addr ~pa:addr Page_table_ast.Data + add_mapping builder ~root ~va:addr ~pa:addr Page_table_ast.Data + | Page_table_ast.TableBlock {name; base; body; _} -> + let base = table_addr "table base" base in + if List.exists (fun root -> root.name = Some name) builder.named_roots then + error "page_table: duplicate table root: %s" name; + if + builder.default_root.base = base + || List.exists (fun root -> root.base = base) builder.named_roots + then error "page_table: duplicate table base: 0x%x" base; + let root = {name = Some name; base} in + builder.named_roots <- root :: builder.named_roots; + initialise_root builder ~table_block root; + List.iter (eval_stmt builder ~symbolic_vas ~table_block ~root) body (** {1 Layout construction} *) @@ -302,13 +352,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.named_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 @@ -329,10 +383,11 @@ let build ~pa_alignments:(pa_alignment_requests stmts) ~root in - add_mapping ~level:2 builder ~va:0 ~pa:0 Page_table_ast.Code; - add_mapping ~level:2 builder ~va:table_block ~pa:table_block Page_table_ast.Data; + initialise_root builder ~table_block builder.default_root; (* 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 ~table_block ~root:builder.default_root) + stmts; (* 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 948e0d36..4180c4cc 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; - (* Symbol names and their concrete physical addresses. *) - symbols_pa : (string * pa) list; + (* Named table roots and their physical addresses. *) + table_symbols_pa : (string * pa) list; (* Data symbols and their allocated physical addresses. *) - phys_symbols_pa : (string * pa) list; + 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..85c399e4 --- /dev/null +++ b/cli/tests/converter/expect/arm/vm/SwitchTTBR+VM.litmus.toml @@ -0,0 +1,167 @@ +arch = "Arm" +name = "SwitchTTBR+VM" + +[[memory]] + sym = "__thread0" + kind = "code" + addr = 0x1000 + step = 4 + data = [0xd5182000, 0xd5382003, 0xf9400041] + +[[memory]] + kind = "pagetable" + addr = 0x2c0000 + step = 8 + data = 0x304003 + +[[memory]] + kind = "pagetable" + addr = 0x300000 + step = 8 + data = 0x307003 + +[[memory]] + kind = "pagetable" + addr = 0x301000 + step = 8 + data = 0x302003 + +[[memory]] + kind = "pagetable" + addr = 0x302000 + step = 8 + data = 0x303003 + +[[memory]] + kind = "pagetable" + addr = 0x303000 + step = 8 + data = 0x4c1 + +[[memory]] + kind = "pagetable" + addr = 0x303008 + step = 8 + data = 0x200441 + +[[memory]] + kind = "pagetable" + addr = 0x304000 + step = 8 + data = 0x305003 + +[[memory]] + kind = "pagetable" + addr = 0x305000 + step = 8 + data = 0x4c1 + +[[memory]] + kind = "pagetable" + addr = 0x305008 + step = 8 + data = 0x200441 + +[[memory]] + kind = "pagetable" + addr = 0x305010 + step = 8 + data = 0x306003 + +[[memory]] + kind = "pagetable" + addr = 0x306000 + step = 8 + data = 0x401443 + +[[memory]] + kind = "pagetable" + addr = 0x307000 + step = 8 + data = 0x308003 + +[[memory]] + kind = "pagetable" + addr = 0x308000 + step = 8 + data = 0x4c1 + +[[memory]] + kind = "pagetable" + addr = 0x308008 + step = 8 + data = 0x200441 + +[[memory]] + kind = "pagetable" + addr = 0x308010 + step = 8 + data = 0x309003 + +[[memory]] + kind = "pagetable" + addr = 0x309000 + step = 8 + data = 0x402443 + +[[memory]] + sym = "pa0" + addr = 0x401000 + step = 8 + data = 0 + +[[memory]] + sym = "pa1" + addr = 0x402000 + step = 8 + data = 1 + +[thread] + +[thread."0"] + breakpoints = [0x100c] + +[thread."0".regs] + _PC = 0x1000 + "R0" = 0x300000 + "R2" = 0x400000 + "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}]}