diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-11-25 18:10:50 +0000 |
|---|---|---|
| committer | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-11-26 13:41:42 +0000 |
| commit | fa707da94d0329e7d1b7520d876ad85953f2fdd5 (patch) | |
| tree | 696de6520fe7780b6e92a0191f9f53f4decbbf35 /model | |
| parent | 09acf70118de41e04dab37977daae56c6349dfec (diff) | |
| download | sail-riscv-fa707da94d0329e7d1b7520d876ad85953f2fdd5.zip sail-riscv-fa707da94d0329e7d1b7520d876ad85953f2fdd5.tar.gz sail-riscv-fa707da94d0329e7d1b7520d876ad85953f2fdd5.tar.bz2 | |
Tweak base case of PTW functions
Make termination of the page table walk functions provable
unconditionally in Isabelle by catching the case when "level" becomes
negative. On the Sail level, this case cannot occur, because "level"
has type "nat", but we currently don't automatically carry over the
non-negativity constraint of the Sail type "nat" into Isabelle.
Diffstat (limited to 'model')
| -rw-r--r-- | model/riscv_vmem_sv32.sail | 8 | ||||
| -rw-r--r-- | model/riscv_vmem_sv39.sail | 8 | ||||
| -rw-r--r-- | model/riscv_vmem_sv48.sail | 8 |
3 files changed, 12 insertions, 12 deletions
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index bf43f6f..1a27072 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -37,13 +37,13 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { if isPTEPtr(pbits, ext_pte) then { - if level == 0 then { + if level > 0 then { + /* walk down the pointer to the next level */ + walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk32: last-level pte contains a ptr"); */ PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else { - /* walk down the pointer to the next level */ - walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } } else { /* leaf PTE */ match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 6f9d7f0..37c98a2 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -31,13 +31,13 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { if isPTEPtr(pbits, ext_pte) then { - if level == 0 then { + if level > 0 then { + /* walk down the pointer to the next level */ + walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk39: last-level pte contains a ptr"); */ PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else { - /* walk down the pointer to the next level */ - walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } } else { /* leaf PTE */ match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 03d22c6..36304cf 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -31,13 +31,13 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { if isPTEPtr(pbits, ext_pte) then { - if level == 0 then { + if level > 0 then { + /* walk down the pointer to the next level */ + walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk48: last-level pte contains a ptr"); */ PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else { - /* walk down the pointer to the next level */ - walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } } else { /* leaf PTE */ match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { |