summaryrefslogtreecommitdiff
path: root/src/c_backend.mli
AgeCommit message (Collapse)Author
2019-02-01Add tracing instrumention for SMTAlasdair Armstrong
Fix pretty printer bug
2019-01-30Cache compilation results to improve build times for repeated buildsAlasdair
2018-11-27Fix memory leak in string_of_bitsAlasdair Armstrong
Should hopefully fix memory leak in RISC-V. Also adds an optimization pass that removes copying structs and allows some structs to simply alias each other and avoid copying their contents. This requires knowing certain things about the lifetimes of the structs involved, as can't free the struct if another variable is referencing it - therefore we conservatively only apply this optimization for variables that are lifted outside function definitions, and should therefore never get freed until the model exits - however this may cause issues outside ARMv8, as there may be cases where a struct can exist within a variant type (which are not yet subject to this lifting optimisation), that would break these assumptions - therefore this optimisation is only enabled with the -Oexperimental flag.
2018-11-23C backend improvementsAlasdair Armstrong
- Propagate types more accurately to improve optimization on ANF representation. - Add a generic optimization pass to remove redundant variables that simply alias other variables. - Modify Sail interactive mode, so it can compile a specification with the :compile command, view generated intermediate representation via the :ir <function> command, and step-through the IR with :exec <exp> (although this is very incomplete) - Introduce a third bitvector representation, between fast fixed-precision bitvectors, and variable length large bitvectors. The bitvector types are now from most efficient to least * CT_fbits for fixed precision, 64-bit or less bitvectors * CT_sbits for 64-bit or less, variable length bitvectors * CT_lbits for arbitrary variable length bitvectors - Support for generating C code using CT_sbits is currently incomplete, it just exists in the intermediate representation right now. - Include ctyp in AV_C_fragment, so we don't have to recompute it
2018-11-06Fix bug with loop indices not being mapped to int64 in CAlasdair Armstrong
This should fix the issue in cheri128 Also introduce a feature to more easily debug the C backend: sail -dfunction Name will pretty-print the ANF and IR representation of just the Name function. I want to make this work for the type-checker as well, but it's a bit hard to get that to not fire during re-writing passes right now.
2018-09-04C: add an option to control generation of main().Prashanth Mundkur
2018-08-30Allow additional includes to be specified for C backend.Prashanth Mundkur
2018-08-16Various cleanups to ott grammarAlasdair Armstrong
Add additional well-formedness check when calling typing rules