Minor improvements to CRefine #699
Conversation
proof/crefine/ARM/SR_lemmas_C.thy
Outdated
| @@ -905,6 +905,8 @@ lemma valid_mdb_ctes_of_prev: | |||
|
|
|||
| end | |||
|
|
|||
| lemmas ThreadState_defs = StrictC'_thread_state_defs | |||
There was a problem hiding this comment.
It wasn't obvious where to put this. It ended up here purely because I wanted it outside of the kernel locale so that it could be used in ADT_C. Suggestions for a more sensible location are welcome.
There was a problem hiding this comment.
Would Kernel_C in cspec make sense or is that too far up?
There was a problem hiding this comment.
That could work, although there isn't anything directly comparable there after the install_C_file command.
The other option I just thought of is cspec/KernelState_C. That also doesn't have anything directly comparable but has the benefit of being arch-generic so there's less duplication.
There was a problem hiding this comment.
I don't know how directly comparable you need it to be, but from my perspective the Hide unqualified names conflicting with Kernel_Config names. Force use of Kernel_C prefix sounds like it's along the lines of what you're trying to do. It does have the downside of being duplicated across arches, being in Kernel_C. I've never touched KernelState_C before, it looks ancient. @lsf37 might remember what its role is supposed to be. I'd still prefer it in Kernel_C for now, given it's somewhere we might find it again.
There was a problem hiding this comment.
That's a good point about being able to find this again. I'm not sure if I've seen KernelState_C before either, I only found it now because I was looking at the arch-generic cspec files to decide whether any were suitable.
There was a problem hiding this comment.
KernelState_C was introduced by Simon in 2008 with the commit message "Changes for new bitfields", so I guess we can take it as whatever we like :-), but it looks like it is not actually included anywhere and the definitions in there are unused.
I like the idea of a theory where we could put some generic things that work for all kernel versions, but introducing that will mess with the theory include graph a bit. Not a major problem, but might be better to defer to a point where we want to think about arch splitting CRefine a bit more.
So I propose to put ThreadState_defs into Kernel_C instead and to remove KernelState_C from ROOT and the repo.
There was a problem hiding this comment.
Hm, correction. As Corey points out: the file is used, from generated bitfield theories (which git grep doesn't see), and those do use the definitions. In that case we should not remove it, of course. And the commit message actually makes sense with that.
Ok, new proposal: I'd still add ThreadState_defs to Kernel_C, and add a comment to KernelState_C saying that it is the base theory for generated bitfield proofs about the kernel.
There was a problem hiding this comment.
I support this proposal.
At some point the idea of a generic theory that happens right after install_C_file might be useful, we should keep our eyes open for further demand for this.
There was a problem hiding this comment.
I like the proposal as well and have implemented it. Is there anything else to do before merging this PR?
corlewis
force-pushed
the
crefine_improvements
branch
from
c9acf88
to
21014ea
Compare
|
This has been updated to also include AArch64. I think it's now ready to merge, pending a decision on the location of |
corlewis
force-pushed
the
crefine_improvements
branch
from
21014ea
to
d390c76
Compare
This allows these lemmas to be used for goals with slightly more complicated return relations. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
This is just an alias for the c-parser generated StrictC'_thread_state_defs, but is hopefully easier to remember. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
corlewis
force-pushed
the
crefine_improvements
branch
from
d390c76
to
2a83c2c
Compare
No description provided.