Move tutorial tools to main directory structure #130
Conversation
There was a problem hiding this comment.
Nice restructuring collection. Could we make the adjustments to the README file in this PR and keep the three other bullet points for a new PR?
Otherwise, some comments:
- not for this PR, but general comment: we need more tests. at least some basic three tests per module. otherwise it's hard to notice if something breaks and also hard to find what exactly breaks from a change: e.g. backlifter and comp (at the moment they are indirectly tested by the tutorial test, but more fine grained testing would be helpful. even if tests are simple and really basic they help to spot some problems and narrow down the search for causes)
- backlifter sounds fancy :)
- maybe subprogram lib is not really a lifter thing. but maybe it is because it works together with programs that are lifted with the current version of the lifter. but then, when we change the lifter to produce multiple blocks per instruction, then this way of extracting subprograms doesn't work anymore. unsure. anyways, the reason why i comment on it is that the idea of having a subprogram lib doesn't sound like a "lifter thing" to me
|
Ok, just patched up |
|
From the look of the file, I would say that I did create it manually. My rationale must have been that this directory structure does not change often, and it's super easy to fix the file. |
Yes, that was what I suspected. Thanks for the quick reply. |
|
Just to not keep you waiting: Should I give this one another review already to merge it or are you still working on it? |
I pushed a commit with a few further changes to the README just now. You can review them, and maybe make an issue for fixing a new dependency graph if you want. |
README.md
Outdated
| ├─ doc: Documentation material | ||
| ├─ examples: Showcasing HolBA | ||
| │ ├─ aes: lifting + WP of AES on Cortex-M0 | ||
| │ ├─ bsl-wp-smt: Simplified BIR generation and SMT interface |
There was a problem hiding this comment.
It does also have wp generation inside. In this way it tests the whole chain for simple example programs. Maybe we want to add one word somewhere to capture this fact?
There was a problem hiding this comment.
It does also have wp generation inside. In this way it tests the whole chain for simple example programs. Maybe we want to add one word somewhere to capture this fact?
Sure, you can suggest a change to this effect.
There was a problem hiding this comment.
Not exactly one extra word, but what about:
Small BIR example programs to test Simplified BIR generation, WP propagation and SMT interface
or
Small BIR example programs to test BSL, WP, and the extended HolSMT
or append "libraries together" to the last one
There was a problem hiding this comment.
I went with the first suggestion.
# Conflicts: # src/theory/tools/backlifter/bir_backlifterScript.sml # src/tools/Holmakefile.gen # src/tools/backlifter/bir_backlifterLib.sml
|
Ahh. Probably because of the git file rename detection and similar path names, I merged wrong. I am fixing it now and will then check it properly. |
This PR moves tools from the tutorial support directories to the other tools.
A few questions remain:
bir_lifter_simple_interfaceLib.smlandbir_lifter_interfaceLib.sml? I suggest these be merged, while checking names of functions to be consistent.bir_wp_interfaceLib.smlandeasy_noproof_wpLib.sml(currently not used)? Here, functionality seems to be more overlapping.supportandsupport2directories of the tutorial. We need to decide where to place these things.We also need to change the main README to take these changes into account. I think that can be done when this is finalized.