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,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

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

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;

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(

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"
 

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"

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"

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);

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(

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"

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,

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);

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(

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"

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(