Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Code quality improvements #460

Open
3 of 8 tasks
msprotz opened this issue Jul 2, 2021 · 1 comment
Open
3 of 8 tasks

Code quality improvements #460

msprotz opened this issue Jul 2, 2021 · 1 comment

Comments

@msprotz
Copy link
Contributor

msprotz commented Jul 2, 2021

While trying to minimize the generated C code for @NikolajBjorner:

  • too many files include libintvector.h indiscriminately
  • evercrypt_targetconfig.h, ibid.
  • kremlib (minimal) depends on compat.h which is nonsensical -- all of the stuff that mentions Prims from the machine integers should just be marked as noextract
  • cruft shipped in the kremlib directories: Makefile.{basic,include} and .def file
  • lots of stuff in types.h that should go in "full" kremlib, or maybe not even be there except for bootstrapping?
  • purpose of KRML_HOST_SNPRINTF?
  • excessive inclusion of Hacl_Kremlib.h in numerous files... spurious?
  • too many unused variable errors -- maintaining a list in Helpers.ml that's hardcoded is not scalable, can we add an F* attribute somewhere for assumed definitions that in addition to assuming their types, assume that they are pure for the sake of triggering kremlin's unused variable elimination?
@msprotz
Copy link
Contributor Author

msprotz commented Dec 15, 2022

Ongoing work for unused variable elimination going on in #582 (it's tricky, so need to iterate before we have something that works just fine)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants