arm+arm-hyp spec+proofs: use UserContext datatype like other arches #757
Conversation
Xaphiosis
added
cleanup
proof engineering
| (* FIXME MOVE *) | ||
| lemma all_Not_False[simp]: | ||
| "All Not = False" | ||
| by blast | ||
|
|
There was a problem hiding this comment.
Have you tried if moving this to somewhere in Lib breaks stuff? It looks like a generally useful thing we should always have in scope.
There was a problem hiding this comment.
I'm going to do that now. Since I can't access pcr I'll use the PR check to see if/where it fails.
There was a problem hiding this comment.
This causes a bunch of failure, might want to do it separately.
| @@ -1220,7 +1220,10 @@ lemma getSyscallArg_ccorres_foo: | |||
| apply (simp add: word_less_nat_alt split: if_split) | |||
| apply (rule ccorres_add_return2) | |||
| apply (rule ccorres_symb_exec_l) | |||
| apply (rule_tac P="\<lambda>s. n < unat (scast n_msgRegisters :: word32) \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (ARM_HYP_H.msgRegisters!n) = x!n) (ksCurThread s) s" | |||
| apply (rule_tac P="\<lambda>s. n < unat (scast n_msgRegisters :: word32) | |||
There was a problem hiding this comment.
Should this one be word32 or machine_word?
There was a problem hiding this comment.
I have no idea. It's casting n_msgRegisters which is an int due to being an enumeration, so that's 32 signed word ... then it's trying to do a unat, so it's casting the signed away with scast, so technically that's to 32 word or whatever we call it on other arches (int_len word?), which is 32 even on 64 bit arches? Then again machine_word is a suitably large word to carry it, so it seems arbitrary in this case. Since you pointed it out, what do you think? :)
There was a problem hiding this comment.
I was mostly checking if you had thought about it. If it's not really tied to machine_word it's fine to leave as is. We'll get to think properly about this bit when we attempt splitting in CRefine
There was a problem hiding this comment.
ok, will leave it for now
| "getRegister r = (\<lambda>con. ({(con r, con)}, False))" | ||
| "getRegister r = (\<lambda>con. ({(user_regs con r, con)}, False))" |
There was a problem hiding this comment.
Had forgotten that we did these monad unfoldings here. Those are going to bite when we move to the concurrency monad, but that's a problem for future us. Nothing to do with this PR in any case.
There was a problem hiding this comment.
I don't know anything about how they're used but I don't think that it will be hard to write a similar unfolding for the trace monad. It would be a bit fiddly if we couldn't make the function atomic but even that shouldn't be too bad.
| @@ -1186,7 +1187,10 @@ lemma getSyscallArg_ccorres_foo: | |||
| apply (simp add: word_less_nat_alt split: if_split) | |||
| apply (rule ccorres_add_return2) | |||
| apply (rule ccorres_symb_exec_l) | |||
| apply (rule_tac P="\<lambda>s. n < unat (scast n_msgRegisters :: word32) \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (ARM_H.msgRegisters!n) = x!n) (ksCurThread s) s" | |||
| apply (rule_tac P="\<lambda>s. n < unat (scast n_msgRegisters :: word32) | |||
There was a problem hiding this comment.
machine_word? (same as on ARM_HYP)
| setRegister :: "register \<Rightarrow> machine_word \<Rightarrow> unit user_monad" | ||
| where | ||
| "setRegister r v \<equiv> modify (\<lambda>uc. uc (r := v))" | ||
| "modify_registers f uc \<equiv> UserContext (f (user_regs uc))" |
There was a problem hiding this comment.
A very minor style question; do we want to explicitly state the type here like we do for getRegister and setRegister?
| "getRegister r = (\<lambda>con. ({(con r, con)}, False))" | ||
| "getRegister r = (\<lambda>con. ({(user_regs con r, con)}, False))" |
There was a problem hiding this comment.
I don't know anything about how they're used but I don't think that it will be hard to write a similar unfolding for the trace monad. It would be a bit fiddly if we couldn't make the function atomic but even that shouldn't be too bad.
Xaphiosis
force-pushed
the
arm_user_context
branch
3 times, most recently
from
25c3ef8 to
c1843c6
Compare
This reduces the diff to other architectures and FPU versions by having a UserContext datatype that contains the register state, instead of assuming the context is only the state of the registers. Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
force-pushed
the
arm_user_context
branch
from
c1843c6 to
78379bc
Compare
|
Squashed commits down to 1 and hopefully addressed all PR feedback. Will now wait for tests to make sure I didn't mess something up. |
This reduces the diff to other architectures and FPU versions by having a UserContext datatype that contains the register state, instead of assuming the context is only the state of the registers.
Some of this touches old proofs and fitting in with style is wonky. Thoughts welcome.
This will break the FPU Arm platform port proofs, but once fixed the diff will be smaller.
Will squash commits to the above commit message (and same header as this PR) once people are ok with the changes.