microsoft
/
Komodo
зеркало из https://github.com/microsoft/Komodo.git
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность

fix main for vale changes; 'make verified' now completes

This commit is contained in:
Andrew Baumann 2017-02-21 09:58:35 -08:00
Родитель 777ba57877
Коммит 7005226e70
1 изменённых файлов: 15 добавлений и 12 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

27
verified/main.dfy
Просмотреть файл

@ -12,7 +12,7 @@ method printSMCHandlerReturn()
printInsFixed("MOVS", "pc, lr"); printInsFixed("MOVS", "pc, lr");
} }
method printAll() method printAll(smc_handler:va_code, svc_handler:va_code, abt_handler:va_code)
{ {
var n := 0; var n := 0;
var monitor_vectbl := emptyVecTbl().(svc_smc := Just("smc")); var monitor_vectbl := emptyVecTbl().(svc_smc := Just("smc"));
@ -31,13 +31,13 @@ method printAll()
nl(); nl();
print(".section .text"); nl(); print(".section .text"); nl();
n := printFunction("abort", sp_code_abort_handler(), n); n := printFunction("abort", abt_handler, n);
printExceptionHandlerReturn(); nl(); printExceptionHandlerReturn(); nl();
n := printFunction("svc", sp_code_svc_handler(), n); n := printFunction("svc", svc_handler, n);
printExceptionHandlerReturn(); nl(); printExceptionHandlerReturn(); nl();
n := printFunction("smc", sp_code_smc_handler(), n); n := printFunction("smc", smc_handler, n);
printSMCHandlerReturn(); nl(); printSMCHandlerReturn(); nl();
printBss(KomGlobalDecls()); printBss(KomGlobalDecls());
@ -59,9 +59,10 @@ predicate InitialState(s:state)
method Main() method Main()
{ {
var smc_handler := sp_code_smc_handler(); var smc_handler := va_code_smc_handler(OReg(R0), OReg(R1), OReg(R2),
var svc_handler := sp_code_svc_handler(); OReg(R3), OReg(R4), OReg(R0), OReg(R1));
var abt_handler := sp_code_abort_handler(); 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 // prove that the final state for an SMC call is valid
forall s1:state, p1:PageDb, s2:state forall s1:state, p1:PageDb, s2:state
@ -76,13 +77,15 @@ method Main()
{ {
var stack_bytes := KOM_STACK_SIZE - WORDSIZE; var stack_bytes := KOM_STACK_SIZE - WORDSIZE;
assert StackBytesRemaining(s1, stack_bytes); assert StackBytesRemaining(s1, stack_bytes);
reveal_sp_eval(); reveal_va_eval();
var block := sp_CCons(smc_handler, sp_CNil()); var block := va_CCons(smc_handler, va_CNil());
assert sp_eval(Block(block), s1, s2) by { assert evalBlock(block, s1, s2); } assert va_eval(Block(block), s1, s2) by { assert evalBlock(block, s1, s2); }
var _, _, p2' := sp_lemma_smc_handler(block, s1, s2, stack_bytes, p1); 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 smchandler(s1, p1, s2, p2');
assert validPageDb(p2') && pageDbCorresponds(s2.m, p2'); assert validPageDb(p2') && pageDbCorresponds(s2.m, p2');
} }
printAll(); printAll(smc_handler, svc_handler, abt_handler);
} }