cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
Using compilationLib with custom configs doesn't work because the library is hard-coded to use only the standard configs, see here: https://github.com/CakeML/cakeml/blob/master/compiler/compilationLib.sml#L165-L184. Here are some things that might differ between configs:...
This issue is about adding instructions, e.g., to developers/, for 1. Profiling a CakeML program (using @sorear 's symbol additions) 2. Extracting intermediate dataLang code from the compiler This was...
`good_dimindex` is defined in [labPropsScript.sml](https://github.com/CakeML/cakeml/blob/master/compiler/backend/semantics/labPropsScript.sml). This makes its usage elsewhere dependent on `labPropsTheory` and hence also the frontend files. It would be best to move the definition and related theorems...
Arthur Charguéraud has developed a new version of CFML based on weakest preconditions. Here are a few URLs: - [his course on separation logic ](http://www.chargueraud.org/teach/verif/) - [his construction of wpgen](http://www.chargueraud.org/teach/verif/slf/LibSepReference.html)...
r12 and r13 do not need to be avoided, but they are less efficient to use under some circumstances: memory accesses relative to r12 with no (register) index, or accesses...
We would like to be able to modify IRs at various levels to simulate the effects of a compiler change. In most cases the plumbing for this would be very...
If the stack can grow down to `lim`, and the first store value is at `lim`-2048, then an interrupt or signal handler can clobber data within a 2048-byte region immediately...
Right now adding a fundamentally new operation requires modifying all of the semantics and quite a few transformations. It's a very involved process, and it makes future maintenance more difficult....
I would like to be able to write code using Word64 or floats without having to deal with constant boxing. This requires some coarse grained tracking of types (I am...
Some numbers from a `--target=riscv --exp_cut=99999` build (9a0180e sexpr-bootstrap): ``` 1069060 cml_x64Prog_x64_enc_5306 990976 cml_arm7Prog_arm7_enc_5296 938348 cml_riscvProg_riscv_enc_5348 784956 cml_arm8Prog_arm8_enc_5342 373572 cml_mipsProg_mips_enc_5352 291168 cml_ag32_enc_5324 ``` Some of this is probably unavoidable with...