From 087eef7d9455c74b75550df4c91a2ac289ed85ec Mon Sep 17 00:00:00 2001 From: Andrew Baumann Date: Wed, 15 Feb 2017 17:03:53 -0800 Subject: [PATCH] started manually updating vale code to use framing / new decls still plenty of work to do; memset and kom_utils are the only completed files --- verified/allocate_page.sdfy | 2 +- verified/entry.sdfy | 2 +- verified/exception_handlers.sdfy | 15 ++++++-- verified/finalise.sdfy | 2 +- verified/init_addrspace.sdfy | 2 +- verified/init_dispatcher.sdfy | 2 +- verified/init_l2ptable.sdfy | 2 +- verified/kom_utils.sdfy | 66 ++++++++++++++++---------------- verified/map_insecure.sdfy | 2 +- verified/map_secure.sdfy | 2 +- verified/map_utils.sdfy | 2 +- verified/memset.sdfy | 19 ++++----- verified/remove.sdfy | 2 +- verified/smc_handler.sdfy | 2 +- verified/stop.sdfy | 2 +- 15 files changed, 63 insertions(+), 61 deletions(-) diff --git a/verified/allocate_page.sdfy b/verified/allocate_page.sdfy index dc0a089..fa478d4 100644 --- a/verified/allocate_page.sdfy +++ b/verified/allocate_page.sdfy @@ -2,7 +2,7 @@ include {:verbatim} "Sets.dfy" include {:verbatim} "kom_common.i.dfy" include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "kom_utils.sdfy" #verbatim diff --git a/verified/entry.sdfy b/verified/entry.sdfy index 599e60d..0bc71b3 100644 --- a/verified/entry.sdfy +++ b/verified/entry.sdfy @@ -3,7 +3,7 @@ include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" include {:verbatim} "entry.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "kom_utils.sdfy" #verbatim diff --git a/verified/exception_handlers.sdfy b/verified/exception_handlers.sdfy index 9ed63dd..517bbfd 100644 --- a/verified/exception_handlers.sdfy +++ b/verified/exception_handlers.sdfy @@ -3,17 +3,17 @@ include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" include {:verbatim} "entry.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" procedure switch_to_monitor() + modifies + cpsr; requires SaneConstants() && ValidState(this) && SaneStack(this) && SaneMem(this.m); priv_of_state(this) == PL1 && world_of_state(this) == Secure; this.ok; ensures SaneState(this); - AllMemInvariant(old(this), this); - this.regs == old(this.regs); { assert ValidPsrWord(cpsr) by { reveal_ValidSRegState(); } CPSID_IAF(const(encode_mode(Monitor))); @@ -21,11 +21,14 @@ procedure switch_to_monitor() } procedure svc_handler( - inout {:register OReg(R0)} retval:int, ghost user_state: state, ghost stack_bytes: int, ghost pagedb_in: PageDb, ghost dispPg: PageNr) returns (ghost pagedb: PageDb) + reads + globals; r0; + modifies + mem; r0; r1; r2; cpsr; requires SaneConstants() && ValidState(this) && SaneStack(this) && SaneMem(this.m); this.ok; @@ -94,6 +97,10 @@ procedure abort_handler( ghost stack_bytes: int, ghost pagedb_in: PageDb, ghost dispPg: PageNr) returns (ghost pagedb: PageDb) + reads + globals; r0; + modifies + mem; r0; r1; r2; cpsr; requires SaneConstants() && ValidState(this) && SaneStack(this) && SaneMem(this.m); this.ok; diff --git a/verified/finalise.sdfy b/verified/finalise.sdfy index 8367ddf..ce1e856 100644 --- a/verified/finalise.sdfy +++ b/verified/finalise.sdfy @@ -2,7 +2,7 @@ include {:verbatim} "kom_common.i.dfy" include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "kom_utils.sdfy" procedure kom_smc_finalise( diff --git a/verified/init_addrspace.sdfy b/verified/init_addrspace.sdfy index b00aebe..0c43386 100644 --- a/verified/init_addrspace.sdfy +++ b/verified/init_addrspace.sdfy @@ -2,7 +2,7 @@ include {:verbatim} "kom_common.i.dfy" include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "kom_utils.sdfy" include "memset.sdfy" diff --git a/verified/init_dispatcher.sdfy b/verified/init_dispatcher.sdfy index 52a0c13..6d1398b 100644 --- a/verified/init_dispatcher.sdfy +++ b/verified/init_dispatcher.sdfy @@ -2,7 +2,7 @@ include {:verbatim} "kom_common.i.dfy" include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "kom_utils.sdfy" include "allocate_page.sdfy" include "memset.sdfy" diff --git a/verified/init_l2ptable.sdfy b/verified/init_l2ptable.sdfy index 68a5d9c..661aaf9 100644 --- a/verified/init_l2ptable.sdfy +++ b/verified/init_l2ptable.sdfy @@ -4,7 +4,7 @@ include {:verbatim} "smcapi.i.dfy" include {:verbatim} "bitvectors.i.dfy" include {:verbatim} "ptebits.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "kom_utils.sdfy" include "allocate_page.sdfy" include "memset.sdfy" diff --git a/verified/kom_utils.sdfy b/verified/kom_utils.sdfy index e9e5e9e..f7192dc 100644 --- a/verified/kom_utils.sdfy +++ b/verified/kom_utils.sdfy @@ -1,14 +1,13 @@ include {:verbatim} "kom_common.i.dfy" include {:verbatim} "bitvectors.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" -procedure page_paddr_impl(out operand phys:int, operand pagenr:int, out operand tmp:int) +procedure page_paddr_impl(out operand phys:reg, operand pagenr:reg, out operand tmp:reg) + reads + globals; requires/ensures SaneState(this); requires - ValidRegOperand(@phys); - ValidRegOperand(@pagenr); - ValidRegOperand(@tmp); // NB: @phys == @pagenr is supported @phys != @tmp; @pagenr != @tmp; @@ -16,9 +15,7 @@ procedure page_paddr_impl(out operand phys:int, operand pagenr:int, out operand @tmp != OSP; validPageNr(pagenr); ensures - AllMemInvariant(old(this),this); - RegPreservingExcept(old(this), this, set(@phys, @tmp)); - SmcProcedureInvariant(old(this), this); + //SmcProcedureInvariant(old(this), this); phys == page_paddr(old(pagenr)); PageAligned(phys); { @@ -33,13 +30,12 @@ procedure page_paddr_impl(out operand phys:int, operand pagenr:int, out operand ADD(phys, phys, tmp); } -procedure paddr_page_impl(out operand pagenr:int, operand phys:int, out operand tmp:int) +procedure paddr_page_impl(out operand pagenr:reg, operand phys:reg, out operand tmp:reg) + reads + globals; requires/ensures SaneState(this); requires - ValidRegOperand(@phys); - ValidRegOperand(@pagenr); - ValidRegOperand(@tmp); // NB: @phys == @pagenr is supported @phys != @tmp; @pagenr != @tmp; @@ -48,9 +44,7 @@ procedure paddr_page_impl(out operand pagenr:int, operand phys:int, out operand PageAligned(phys); SecurePhysBase() <= phys < SecurePhysBase() + KOM_SECURE_RESERVE; ensures - GlobalsInvariant(old(this),this); - RegPreservingExcept(old(this), this, set(@pagenr, @tmp)); - SmcProcedureInvariant(old(this), this); + //SmcProcedureInvariant(old(this), this); pagenr == paddr_page(old(phys)); validPageNr(pagenr); { @@ -65,13 +59,12 @@ procedure paddr_page_impl(out operand pagenr:int, operand phys:int, out operand assert pagenr == oldpagenr / PAGESIZE; } -procedure page_monvaddr_impl(out operand virt:int, operand pagenr:int, out operand tmp:int) +procedure page_monvaddr_impl(out operand virt:reg, operand pagenr:reg, out operand tmp:reg) + reads + globals; requires/ensures SaneState(this); requires - ValidRegOperand(@virt); - ValidRegOperand(@pagenr); - ValidRegOperand(@tmp); // NB: @pagenr == @virt is supported @pagenr != @tmp; @virt != @tmp; @@ -79,17 +72,18 @@ procedure page_monvaddr_impl(out operand virt:int, operand pagenr:int, out opera @tmp != OSP; validPageNr(pagenr); ensures - AllMemInvariant(old(this),this); - RegPreservingExcept(old(this), this, set(@virt, @tmp)); - SmcProcedureInvariant(old(this), this); + //SmcProcedureInvariant(old(this), this); virt == page_monvaddr(old(pagenr)); - isUInt32(virt); { page_paddr_impl(virt, pagenr, tmp); ADD(virt, virt, const(KOM_DIRECTMAP_VBASE)); } procedure stack_nonvolatiles(ghost stack_bytes:int) returns (ghost stack_bytes_ret:int) + reads + r4; r5; r6; r7; r8; r9; r10; r11; r12; lr; + modifies + sp; mem; requires/ensures SaneState(this); requires @@ -99,7 +93,7 @@ procedure stack_nonvolatiles(ghost stack_bytes:int) returns (ghost stack_bytes_r sp == old(sp-40); //preserves registers - RegPreservingExcept(old(this), this, set(@sp)); + //RegPreservingExcept(old(this), this, set(@sp)); // pushes r4-r11, sp, lr MemContents(this.m, sp) == old(r12); @@ -113,9 +107,9 @@ procedure stack_nonvolatiles(ghost stack_bytes:int) returns (ghost stack_bytes_r MemContents(this.m, sp+32) == old(r4); MemContents(this.m, sp+36) == old(lr); - GlobalsInvariant(old(this),this); - BankedRegsInvariant(old(this),this); - SRegsInvariant(old(this),this); + //GlobalsInvariant(old(this),this); + //BankedRegsInvariant(old(this),this); + //SRegsInvariant(old(this),this); NonStackMemPreserving(old(this),this); ParentStackPreserving(old(this),this); @@ -139,6 +133,10 @@ procedure stack_nonvolatiles(ghost stack_bytes:int) returns (ghost stack_bytes_r } procedure unstack_nonvolatiles(ghost stack_bytes:int) returns (ghost stack_bytes_ret:int) + reads + mem; + modifies + r4; r5; r6; r7; r8; r9; r10; r11; r12; lr; sp; requires/ensures SaneState(this); requires @@ -149,10 +147,10 @@ procedure unstack_nonvolatiles(ghost stack_bytes:int) returns (ghost stack_bytes sp == old(sp+40); // fcall argument regs preserved. - r0 == old(r0); - r1 == old(r1); - r2 == old(r2); - r3 == old(r3); + //r0 == old(r0); + //r1 == old(r1); + //r2 == old(r2); + //r3 == old(r3); // pop lr, r4-r11 from stack. lr == old(MemContents(this.m, sp+36)); @@ -166,9 +164,9 @@ procedure unstack_nonvolatiles(ghost stack_bytes:int) returns (ghost stack_bytes r11 == old(MemContents(this.m, sp+4)); r12 == old(MemContents(this.m, sp)); - AllMemInvariant(old(this),this); - BankedRegsInvariant(old(this),this); - SRegsInvariant(old(this),this); + //AllMemInvariant(old(this),this); + //BankedRegsInvariant(old(this),this); + //SRegsInvariant(old(this),this); stack_bytes_ret == stack_bytes + 40; StackBytesRemaining(this, stack_bytes_ret); diff --git a/verified/map_insecure.sdfy b/verified/map_insecure.sdfy index bb1c765..844fdc2 100644 --- a/verified/map_insecure.sdfy +++ b/verified/map_insecure.sdfy @@ -3,7 +3,7 @@ include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" include {:verbatim} "ptebits.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "map_secure.sdfy" procedure mkl2pte_insecure( diff --git a/verified/map_secure.sdfy b/verified/map_secure.sdfy index 5ed25be..f5c51de 100644 --- a/verified/map_secure.sdfy +++ b/verified/map_secure.sdfy @@ -3,7 +3,7 @@ include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" include {:verbatim} "ptebits.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "kom_utils.sdfy" include "allocate_page.sdfy" include "map_utils.sdfy" diff --git a/verified/map_utils.sdfy b/verified/map_utils.sdfy index 839f4aa..cc92068 100644 --- a/verified/map_utils.sdfy +++ b/verified/map_utils.sdfy @@ -1,7 +1,7 @@ include {:verbatim} "kom_common.i.dfy" include {:verbatim} "bitvectors.i.dfy" include {:verbatim} "pagedb.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" procedure fetch_l1pte( operand l1pt_va:addr, diff --git a/verified/memset.sdfy b/verified/memset.sdfy index 330f81d..34233a0 100644 --- a/verified/memset.sdfy +++ b/verified/memset.sdfy @@ -1,23 +1,21 @@ include {:verbatim} "kom_common.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" -procedure memcpy(operand dst:addr, operand src:addr, inout operand size:addr, - out operand tmp:int) +procedure memcpy(operand dst:addr, operand src:addr, inout operand size:reg, + out operand tmp:reg) + modifies + mem; requires/ensures SaneState(this); requires DistinctRegOperands(set(@dst, @src, @size, @tmp), 4); - WordAligned(dst); - WordAligned(src); WordAligned(size); ValidMemRange(dst, dst + size); ValidMemRange(src, src + size); dst + size <= src || src + size <= dst; dst >= StackBase() || dst + size <= StackLimit(); ensures - GlobalsInvariant(old(this),this); SmcProcedureInvariant(old(this),this); - RegPreservingExcept(old(this), this, set(@size, @tmp)); MemPreservingExcept(old(this), this, old(dst), old(dst + size)); //forall i :: 0 <= i < old(size) && WordAligned(i) // ==> MemContents(this.m, old(dst) + i) == old(MemContents(this.m, src + i)); @@ -51,19 +49,18 @@ procedure memcpy(operand dst:addr, operand src:addr, inout operand size:addr, } } -procedure memset(operand base:addr, operand val:word, inout operand size:addr) +procedure memset(operand base:addr, operand val:word, inout operand size:reg) + modifies + mem; requires/ensures SaneState(this); requires DistinctRegOperands(set(@base, @val, @size), 3); - WordAligned(base); WordAligned(size); ValidMemRange(base, base + size); base >= StackBase() || base + size <= StackLimit(); ensures - GlobalsInvariant(old(this),this); SmcProcedureInvariant(old(this),this); - RegPreservingExcept(old(this), this, set(@size)); MemPreservingExcept(old(this), this, old(base), old(base + size)); forall a :: old(base) <= a < old(base + size) && WordAligned(a) ==> MemContents(this.m, a) == old(val); diff --git a/verified/remove.sdfy b/verified/remove.sdfy index 127e28c..f8981ad 100644 --- a/verified/remove.sdfy +++ b/verified/remove.sdfy @@ -2,7 +2,7 @@ include {:verbatim} "kom_common.i.dfy" include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "kom_utils.sdfy" procedure kom_smc_remove_non_addr_success( diff --git a/verified/smc_handler.sdfy b/verified/smc_handler.sdfy index 05b0287..b5b3c39 100644 --- a/verified/smc_handler.sdfy +++ b/verified/smc_handler.sdfy @@ -2,7 +2,7 @@ include {:verbatim} "kom_common.i.dfy" include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "kom_utils.sdfy" include "init_addrspace.sdfy" include "init_dispatcher.sdfy" diff --git a/verified/stop.sdfy b/verified/stop.sdfy index f826603..e0c2784 100644 --- a/verified/stop.sdfy +++ b/verified/stop.sdfy @@ -2,7 +2,7 @@ include {:verbatim} "kom_common.i.dfy" include {:verbatim} "pagedb.i.dfy" include {:verbatim} "smcapi.i.dfy" -include "ARMdecls-unrefined.sdfy" +include "ARMdecls.sdfy" include "kom_utils.sdfy" procedure kom_smc_stop(