diff --git a/cli/lib/isla/bv_fns.ml b/cli/lib/isla/bv_fns.ml index f030b3e4..f4351b20 100644 --- a/cli/lib/isla/bv_fns.ml +++ b/cli/lib/isla/bv_fns.ml @@ -52,7 +52,7 @@ let int_of_bit_arg name arg value = Any error during evaluation should be reported with [Failure] which will be converted into a [eval_error] in [Term.eval] *) -let functions : Fn_registry.positional_fn list = +let functions : (string * (Z.t list -> Z.t)) list = [ ( "bvand", function | [a; b] -> Z.logand a b diff --git a/cli/lib/isla/eval_state.ml b/cli/lib/isla/eval_state.ml index 30d92409..cd1a7f60 100644 --- a/cli/lib/isla/eval_state.ml +++ b/cli/lib/isla/eval_state.ml @@ -44,10 +44,12 @@ type page_table = (int, int64) Hashtbl.t type t = { symbols : (string, int) Hashtbl.t; + walks : (string, int list) Hashtbl.t; (* PTE addresses from level 0. *) mutable page_table : page_table option } -let create () = {symbols = Hashtbl.create 32; page_table = None} +let create () = + {symbols = Hashtbl.create 32; walks = Hashtbl.create 16; page_table = None} (** Decides if a string is an Archsem symbol: must start with a ASCII letter or [_] and followed by alphanumeric character (or [_]). @@ -70,7 +72,7 @@ let check_symbol_name name = let check_fresh_symbol state name = check_symbol_name name; - if Hashtbl.mem state.symbols name then + if Hashtbl.mem state.symbols name || Hashtbl.mem state.walks name then Printf.ksprintf failwith "Symbol %s is already defined" name let add_symbol state name addr = @@ -80,4 +82,11 @@ let add_symbol state name addr = let lookup_addr state name = match Hashtbl.find_opt state.symbols name with | Some addr -> addr + | None when Hashtbl.mem state.walks name -> + Printf.ksprintf failwith "Symbol %s is a table walk, expected an address" + name | None -> Printf.ksprintf failwith "Symbol %s not found" name + +let add_walk state name walk = + check_fresh_symbol state name; + Hashtbl.add state.walks name walk diff --git a/cli/lib/isla/fn_registry.ml b/cli/lib/isla/fn_registry.ml index f85eb1e3..d3bac66e 100644 --- a/cli/lib/isla/fn_registry.ml +++ b/cli/lib/isla/fn_registry.ml @@ -44,13 +44,23 @@ Any error during evaluation should be reported with [Failure] which will be converted into a [eval_error] in [Term.eval] *) -type positional_fn = string * (Z.t list -> Z.t) +type value = + | Num of Z.t + | Walk of string * int list -type keyword_fn = string * ((string * Z.t) list -> Z.t) +type positional_fn = string * (value list -> value) + +type keyword_fn = string * ((string * value) list -> value) (** Raise a function-scoped evaluation error. *) let error fmt = Litmus.Error.failwith ("function: " ^^ fmt) +(** Require a numeric value for an ordinary function or expression. *) +let number name : value -> Z.t = function + | Num z -> z + | Walk (walk_name, _) -> + error "%s: table walk %s used where a number is required" name walk_name + (** Convert a Zarith argument to an OCaml [int], preserving function context. *) let int_arg name arg value = match Z.to_int value with diff --git a/cli/lib/isla/lexer.mll b/cli/lib/isla/lexer.mll index b64cc990..310043e8 100644 --- a/cli/lib/isla/lexer.mll +++ b/cli/lib/isla/lexer.mll @@ -76,6 +76,7 @@ rule token = parse | "physical" { PHYSICAL } | "identity" { IDENTITY } | "with" { WITH } + | "as" { AS } | "and" { AND_KW } | "default" { DEFAULT } | "code" { CODE } diff --git a/cli/lib/isla/page_table/page_table_ast.ml b/cli/lib/isla/page_table/page_table_ast.ml index 67b64886..397d0caa 100644 --- a/cli/lib/isla/page_table/page_table_ast.ml +++ b/cli/lib/isla/page_table/page_table_ast.ml @@ -80,19 +80,23 @@ type stmt = names : string list } (* [x |-> pa_x;] maps a named address to a physical-address target. - Optional [with ... and default] clauses override descriptor fields. *) + Optional [with ... and default] clauses override descriptor fields. + [as name] records the mapping's table and PTE addresses. *) | Mapping of { va_name : string; target : mapping_target; attrs : descriptor_expr_field list; - level : int option + level : int option; + walk_name : string option } - (* [x ?-> pa_x;] is accepted for Isla compatibility, but ignored entirely. *) + (* [x ?-> pa_x;] is accepted for Isla compatibility and ignored, + including any [as name] annotation. *) | MaybeMapping of { va_name : string; target : mapping_target; attrs : descriptor_expr_field list; - level : int option + level : int option; + walk_name : string option } (* [*pa_name = value;] allocates the PA on first use and evaluates the value. *) | DataInit of @@ -102,7 +106,8 @@ type stmt = (* [identity addr with attr;] maps one page to itself. *) | IdentityMapping of { addr : Term_ast.t; - attr : attr + attr : attr; + walk_name : string option } (* [s1table name 0x280000 { ... }] immediately binds the name to its fixed root PA before executing the body. *) diff --git a/cli/lib/isla/page_table/page_table_builder.ml b/cli/lib/isla/page_table/page_table_builder.ml index 4be99eb8..70899ff8 100644 --- a/cli/lib/isla/page_table/page_table_builder.ml +++ b/cli/lib/isla/page_table/page_table_builder.ml @@ -213,6 +213,8 @@ let check_aligned_at_level name level addr = (** Write an encoded descriptor at [va], allocating intermediate tables. *) let write_descriptor ?(level = Desc.last_level) builder ~root ~va desc = + if level < Desc.root_level || level > Desc.last_level then + error "page_table: invalid mapping level: %d" level; let rec walk table_addr current_level = let idx = Desc.va_index va current_level in if current_level = level then @@ -335,6 +337,23 @@ let require_root = function "page_table: top-level mapping requires an implicit default table, but \ default_tables = false" +(** Record PTE addresses through [level] or the end of the existing path. *) +let record_walk ?(level = Desc.last_level) builder ~root ~va name = + match name with + | None -> () + | Some name -> + let rec walk table current_level = + let idx = Desc.va_index va current_level in + let addr = entry_addr table idx in + if current_level = level then [addr] + else + match child_table_addr builder table idx with + | None -> [addr] + | Some child -> addr :: walk child (current_level + 1) + in + Eval_state.add_walk builder.state name + (walk (require_root root) Desc.root_level) + let rec eval_stmt builder ~table_block ~root = function | Page_table_ast.OptionDefaultTables _ -> () | Page_table_ast.Virtual _ -> () @@ -346,24 +365,31 @@ let rec eval_stmt builder ~table_block ~root = function ) names | Page_table_ast.AlignedVirtual _ -> () - | Page_table_ast.Mapping {va_name; target; attrs; level} -> + | Page_table_ast.Mapping {va_name; target; attrs; level; walk_name} -> + Option.iter (Eval_state.check_fresh_symbol builder.state) walk_name; let root = require_root root in let va = Eval_state.lookup_addr builder.state va_name in - eval_mapping_target ?level ~attrs builder ~root ~va target + eval_mapping_target ?level ~attrs builder ~root ~va target; + record_walk ?level builder ~root:(Some root) ~va walk_name | Page_table_ast.MaybeMapping _ -> () | Page_table_ast.DataInit {pa_name; value} -> let pa = alloc_pa builder pa_name in let value = Term.eval ~state:builder.state value in Hashtbl.replace builder.data_inits pa value - | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Code} -> + | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Code; walk_name} + -> let addr = addr_of_z "address" (Term.eval ~state:builder.state addr) in if addr < Allocator.page_size || addr >= Allocator.big_size then error "page_table: identity code address 0x%x is outside the code arena" - addr - | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Data} -> + addr; + record_walk builder ~root ~va:addr walk_name + | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Data; walk_name} + -> + Option.iter (Eval_state.check_fresh_symbol builder.state) walk_name; let root = require_root root in let addr = addr_of_z "address" (Term.eval ~state:builder.state addr) in - add_mapping builder ~root ~va:addr ~pa:addr Page_table_ast.Data + add_mapping builder ~root ~va:addr ~pa:addr Page_table_ast.Data; + record_walk builder ~root:(Some root) ~va:addr walk_name | Page_table_ast.TableBlock {name; base; body; _} -> let base = table_addr "table base" base in if Hashtbl.mem builder.named_roots name then diff --git a/cli/lib/isla/page_table/page_table_builder.mli b/cli/lib/isla/page_table/page_table_builder.mli index cfb8be39..cad648a3 100644 --- a/cli/lib/isla/page_table/page_table_builder.mli +++ b/cli/lib/isla/page_table/page_table_builder.mli @@ -63,9 +63,7 @@ type layout = exception Error of string (** Build a concrete page-table layout by executing statements in source order. - Symbols are registered as they are allocated. Expressions query the live - entries built so far. After setup, [state] retains these entries for register - and assertion evaluation. *) + [state] retains symbols, entries and named walks for expression evaluation. *) val build : arch:Litmus.Arch_id.t -> (* Allocate physical addresses for data symbols. *) diff --git a/cli/lib/isla/page_table/page_table_fns.ml b/cli/lib/isla/page_table/page_table_fns.ml index ddaf1424..b5bc6443 100644 --- a/cli/lib/isla/page_table/page_table_fns.ml +++ b/cli/lib/isla/page_table/page_table_fns.ml @@ -41,7 +41,7 @@ (** Page-table helper functions available in Isla expressions. *) (** [page(a)] extracts a 4KB page number from an address. *) -let page_function = +let page_function : string * (Z.t list -> Z.t) = ( "page", function | [a] -> Z.extract a 12 36 @@ -49,7 +49,7 @@ let page_function = ) (** [asid(v)] shifts an ASID value into bits [63:48]. *) -let asid_function = +let asid_function : string * (Z.t list -> Z.t) = ( "asid", function | [v] -> Z.shift_left v 48 @@ -79,28 +79,52 @@ let pte_addr name entries ~base ~va ~level = in walk base Page_table_desc.root_level -(** [pteN(va, base)] treats [base] as the root translation-table PA, then - returns the identity-mapped VA of the matching PTE. *) -let pte_function entries level = - let name = Printf.sprintf "pte%d" level in - ( name, - function +(** [pteN(walk)] and [tableN(walk)] use recorded addresses; + [pteN(va, base)] and [tableN(va, base)] query the current tables. *) +let entry_function ~pte entries level : Fn_registry.positional_fn = + let name = Printf.sprintf "%s%d" (if pte then "pte" else "table") level in + let eval : Fn_registry.value list -> int = function + | [Fn_registry.Walk (walk_name, walk)] -> ( + match List.nth_opt walk level with + | Some addr -> addr + | None -> + Fn_registry.error "%s: table walk %s has no level %d" name walk_name + level + ) + | [_] -> Fn_registry.error "%s: expected a table walk" name | [va; base] -> - let va = Fn_registry.int_arg name "va" va in - let base = Fn_registry.int_arg name "base" base in - let pte_pa = pte_addr name entries ~base ~va ~level in - if pte_pa < Allocator.big_size || pte_pa >= 2 * Allocator.big_size then + let va = Fn_registry.int_arg name "va" (Fn_registry.number name va) in + let base = + Fn_registry.int_arg name "base" (Fn_registry.number name base) + in + let addr = pte_addr name entries ~base ~va ~level in + if pte && (addr < Allocator.big_size || addr >= 2 * Allocator.big_size) + then Fn_registry.error "%s: PTE level %d for VA 0x%x was resolved at PA 0x%x which is \ outside page-table storage, for root 0x%x" - name level va pte_pa base; - Z.of_int pte_pa - | args -> Fn_registry.arity_error name 2 (List.length args) + name level va addr base; + addr + | args -> + Fn_registry.error "%s: expected 1 or 2 arguments, got %d" name + (List.length args) + in + ( name, + fun args -> + let addr = eval args in + Fn_registry.Num + (Z.of_int (if pte then addr else Page_table_desc.align_page_addr addr)) ) +let pte_function entries level : Fn_registry.positional_fn = + entry_function ~pte:true entries level + +let table_function entries level : Fn_registry.positional_fn = + entry_function ~pte:false entries level + (** [descN(va, base)] treats [base] as the root translation-table PA and returns the descriptor stored in the matching level-[N] PTE. *) -let desc_function entries level = +let desc_function entries level : string * (Z.t list -> Z.t) = let name = Printf.sprintf "desc%d" level in ( name, function @@ -119,21 +143,8 @@ let desc_function entries level = | args -> Fn_registry.arity_error name 2 (List.length args) ) -(** [tableN(va, base)] returns the page containing the level-[N] PTE. *) -let table_function entries level = - let name = Printf.sprintf "table%d" level in - ( name, - function - | [va; base] -> - let va = Fn_registry.int_arg name "va" va in - let base = Fn_registry.int_arg name "base" base in - let addr = pte_addr name entries ~base ~va ~level in - Z.of_int (Page_table_desc.align_page_addr addr) - | args -> Fn_registry.arity_error name 2 (List.length args) - ) - (** [mkdescN(oa=..., ...)] encodes a level-[N] block/page descriptor. *) -let eval_desc name level kwargs = +let eval_desc name level (kwargs : (string * Z.t) list) : Z.t = Fn_registry.check_kwargs name ["oa"; "Valid"; "AF"; "AP"; "DBM"; "nG"] kwargs; let oa = Fn_registry.required_kwarg name "oa" kwargs in let fields = @@ -151,7 +162,7 @@ let eval_desc name level kwargs = ) (** [mkdescN(table=...)] encodes a next-level table descriptor. *) -let eval_table_desc name kwargs = +let eval_table_desc name (kwargs : (string * Z.t) list) : Z.t = Fn_registry.check_kwargs name ["table"; "APTable"] kwargs; let table_addr = Fn_registry.required_kwarg name "table" kwargs in let fields = [descriptor_field_arg kwargs "APTable" Z.zero] in @@ -160,7 +171,7 @@ let eval_table_desc name kwargs = (Fn_registry.int_arg name "table" table_addr) ) -let mkdesc_function level = +let mkdesc_function level : string * ((string * Z.t) list -> Z.t) = let name = Printf.sprintf "mkdesc%d" level in let eval kwargs = match (List.mem_assoc "oa" kwargs, List.mem_assoc "table" kwargs) with @@ -178,7 +189,7 @@ let check_unsigned name arg bits value = (** [ttbr(asid=..., base=...)] and [ttbr(vmid=..., base=...)] combine a concrete translation-table root PA with its 16-bit address-space ID. *) -let ttbr_function = +let ttbr_function : string * ((string * Z.t) list -> Z.t) = let name = "ttbr" in let eval kwargs = Fn_registry.check_kwargs name ["asid"; "vmid"; "base"] kwargs; @@ -197,17 +208,44 @@ let ttbr_function = in (name, eval) -let positional_functions ~state = - let functions = [page_function; asid_function] in +let positional_functions ~state : Fn_registry.positional_fn list = + let functions = + List.map + (fun (name, eval) -> + ( name, + fun args -> + Fn_registry.Num (eval (List.map (Fn_registry.number name) args)) + ) + ) + [page_function; asid_function] + in match state.Eval_state.page_table with | None -> functions | Some entries -> let levels = [0; 1; 2; 3] in functions @ List.map (pte_function entries) levels - @ List.map (desc_function entries) levels + @ List.map + (fun level -> + let (name, eval) = desc_function entries level in + ( name, + fun args -> + Fn_registry.Num (eval (List.map (Fn_registry.number name) args)) + ) + ) + levels @ List.map (table_function entries) levels let keyword_functions : Fn_registry.keyword_fn list = let levels = [0; 1; 2; 3] in - ttbr_function :: List.map mkdesc_function levels + List.map + (fun (name, eval) -> + ( name, + fun kwargs -> + let args = + List.map (fun (k, v) -> (k, Fn_registry.number name v)) kwargs + in + Fn_registry.Num (eval args) + ) + ) + (ttbr_function :: List.map mkdesc_function levels) diff --git a/cli/lib/isla/parser.mly b/cli/lib/isla/parser.mly index 2d1fcc26..f9af037b 100644 --- a/cli/lib/isla/parser.mly +++ b/cli/lib/isla/parser.mly @@ -67,6 +67,7 @@ %token PHYSICAL %token IDENTITY %token WITH +%token AS %token DEFAULT %token AND_KW %token CODE @@ -89,7 +90,7 @@ %start page_table_setup %type page_table_stmt page_table_stmt_inner page_table_block -%type +%type page_table_mapping_rhs %type page_table_mapping_target %type page_table_attr @@ -127,17 +128,18 @@ page_table_stmt_inner: | 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} + { let (target, attrs, level, walk_name) = rhs in + Page_table_ast.Mapping {va_name; target; attrs; level; walk_name} } | va_name = IDENT; "?->"; rhs = page_table_mapping_rhs - { let (target, attrs, level) = rhs in - Page_table_ast.MaybeMapping {va_name; target; attrs; level} + { let (target, attrs, level, walk_name) = rhs in + Page_table_ast.MaybeMapping {va_name; target; attrs; level; walk_name} } | "*"; pa_name = IDENT; "="; value = term { Page_table_ast.DataInit {pa_name; value} } - | IDENTITY; addr = term; WITH; attr = page_table_attr - { Page_table_ast.IdentityMapping {addr; attr} } + | IDENTITY; addr = term; WITH; attr = page_table_attr; + walk_name = option(page_table_walk_name) + { Page_table_ast.IdentityMapping {addr; attr; walk_name} } page_table_block: | stage = page_table_stage; name = IDENT; base = NUM; "{"; @@ -151,8 +153,12 @@ page_table_stage: page_table_mapping_rhs: | target = page_table_mapping_target; attrs = option(page_table_descriptor_attrs); - level = option(page_table_mapping_level) - { (target, Option.value ~default:[] attrs, level) } + level = option(page_table_mapping_level); + walk_name = option(page_table_walk_name) + { (target, Option.value ~default:[] attrs, level, walk_name) } + +page_table_walk_name: + | AS; name = IDENT { name } page_table_mapping_target: | name = IDENT { Page_table_ast.PaName name } diff --git a/cli/lib/isla/term.ml b/cli/lib/isla/term.ml index 44f5f693..df0b5dda 100644 --- a/cli/lib/isla/term.ml +++ b/cli/lib/isla/term.ml @@ -43,13 +43,25 @@ include Term_ast let eval ~state term = - let positional_functions = - Bv_fns.functions @ Page_table_fns.positional_functions ~state + let positional_functions : Fn_registry.positional_fn list = + List.map + (fun (name, eval) -> + ( name, + fun args -> + Fn_registry.Num (eval (List.map (Fn_registry.number name) args)) + ) + ) + Bv_fns.functions + @ Page_table_fns.positional_functions ~state in let keyword_functions = Page_table_fns.keyword_functions in let rec eval_term = function - | Const z -> z - | Sym sym -> Z.of_int (Eval_state.lookup_addr state sym) + | Const z -> Fn_registry.Num z + | Sym sym -> ( + match Hashtbl.find_opt state.Eval_state.walks sym with + | Some walk -> Fn_registry.Walk (sym, walk) + | None -> Fn_registry.Num (Z.of_int (Eval_state.lookup_addr state sym)) + ) | Fn (name, args) -> let evaluated = List.map eval_term args in Fn_registry.eval ~fns:positional_functions name evaluated @@ -57,4 +69,4 @@ let eval ~state term = let evaluated = List.map (fun (k, v) -> (k, eval_term v)) kwargs in Fn_registry.eval ~fns:keyword_functions name evaluated in - eval_term term + Fn_registry.number "expression" (eval_term term)