Skip to content

feat(Isla): Support named page-table roots - #239

Merged
tperami merged 1 commit into
feature/pgt-allocation-arenasfrom
feature/pgt-dsl-named-tables
Sep 14, 2026
Merged

tperami merged 1 commit into
feature/pgt-allocation-arenasfrom
feature/pgt-dsl-named-tables

Conversation

@febyeji

@febyeji febyeji commented Aug 31, 2026

Copy link
Copy Markdown
Collaborator
  • Parse nested s1table and s2table blocks whose explicit bases are actual physical addresses.

@febyeji
febyeji force-pushed the feature/pgt-dsl-named-tables branch from e230eb7 to 6cac9cd Compare September 7, 2026 19:52
@febyeji
febyeji force-pushed the feature/pgt-dsl-named-tables branch from 6cac9cd to 3c60c0e Compare September 8, 2026 10:24

@tperami tperami left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you rebase this patch so we can look at it tomorrow?

Comment thread cli/tests/arm/vm/SwitchTTBR+VM.litmus.toml Outdated
Comment thread cli/tests/arm/vm/SwitchTTBR+VM.litmus.toml Outdated
@febyeji
febyeji force-pushed the feature/pgt-dsl-named-tables branch from 3c60c0e to 3d422b5 Compare September 11, 2026 06:09

@tperami tperami left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just some minor nits but otherwise good to go

Comment thread cli/lib/isla/page_table/page_table_builder.ml
Comment thread cli/lib/isla/page_table/page_table_builder.ml
Comment thread cli/lib/isla/converter.ml Outdated
@tperami

tperami commented Sep 11, 2026

Copy link
Copy Markdown
Collaborator

Should also delete translate_va_to_pa function which is dead code, but also becoming incorrect with this PR

- 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.
@febyeji
febyeji force-pushed the feature/pgt-dsl-named-tables branch from 3d422b5 to 05f8134 Compare September 11, 2026 14:18
@tperami
tperami added this pull request to the merge queue Sep 14, 2026
Merged via the queue into main with commit 8917422 Sep 14, 2026
2 checks passed
@tperami
tperami deleted the feature/pgt-dsl-named-tables branch September 15, 2026 08:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants