From 7005226e70e1b346204cf5286df1644935850115 Mon Sep 17 00:00:00 2001 From: Andrew Baumann Date: Tue, 21 Feb 2017 09:58:35 -0800 Subject: [PATCH] fix main for vale changes; 'make verified' now completes --- verified/main.dfy | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/verified/main.dfy b/verified/main.dfy index 0ae3ec0..ebb27c7 100644 --- a/verified/main.dfy +++ b/verified/main.dfy @@ -12,7 +12,7 @@ method printSMCHandlerReturn() printInsFixed("MOVS", "pc, lr"); } -method printAll() +method printAll(smc_handler:va_code, svc_handler:va_code, abt_handler:va_code) { var n := 0; var monitor_vectbl := emptyVecTbl().(svc_smc := Just("smc")); @@ -31,13 +31,13 @@ method printAll() nl(); print(".section .text"); nl(); - n := printFunction("abort", sp_code_abort_handler(), n); + n := printFunction("abort", abt_handler, n); printExceptionHandlerReturn(); nl(); - n := printFunction("svc", sp_code_svc_handler(), n); + n := printFunction("svc", svc_handler, n); printExceptionHandlerReturn(); nl(); - n := printFunction("smc", sp_code_smc_handler(), n); + n := printFunction("smc", smc_handler, n); printSMCHandlerReturn(); nl(); printBss(KomGlobalDecls()); @@ -59,9 +59,10 @@ predicate InitialState(s:state) method Main() { - var smc_handler := sp_code_smc_handler(); - var svc_handler := sp_code_svc_handler(); - var abt_handler := sp_code_abort_handler(); + var smc_handler := va_code_smc_handler(OReg(R0), OReg(R1), OReg(R2), + OReg(R3), OReg(R4), OReg(R0), OReg(R1)); + var svc_handler := va_code_svc_handler(); + var abt_handler := va_code_abort_handler(); // prove that the final state for an SMC call is valid forall s1:state, p1:PageDb, s2:state @@ -76,13 +77,15 @@ method Main() { var stack_bytes := KOM_STACK_SIZE - WORDSIZE; assert StackBytesRemaining(s1, stack_bytes); - reveal_sp_eval(); - var block := sp_CCons(smc_handler, sp_CNil()); - assert sp_eval(Block(block), s1, s2) by { assert evalBlock(block, s1, s2); } - var _, _, p2' := sp_lemma_smc_handler(block, s1, s2, stack_bytes, p1); + reveal_va_eval(); + var block := va_CCons(smc_handler, va_CNil()); + assert va_eval(Block(block), s1, s2) by { assert evalBlock(block, s1, s2); } + var _, _, p2' := va_lemma_smc_handler(block, s1, s2, + OReg(R0), OReg(R1), OReg(R2), OReg(R3), OReg(R4), OReg(R0), + OReg(R1), stack_bytes, p1); assert smchandler(s1, p1, s2, p2'); assert validPageDb(p2') && pageDbCorresponds(s2.m, p2'); } - printAll(); + printAll(smc_handler, svc_handler, abt_handler); }