summaryrefslogtreecommitdiff
path: root/src/bytecode_util.ml
AgeCommit message (Collapse)Author
2018-08-14Improve error messages from C backend, and fix issues with assigning to pointersAlasdair Armstrong
2018-08-13Sort ctype_defs in dependency order after specialisationAlasdair
We now generate anonymous types in the correct order, but post specialisation more dependencies can occur between named types, so an additional sorting step is needed to ensure that these happen in the correct order. In theory we could end up with circular dependencies here that don't exist at the Sail source level, but this shouldn't occur often (or ever) in practice. I think this is fixable but it would require some code generator changes.
2018-08-08Fix ordering of generated anonymous types for each cdefAlasdair Armstrong
2018-08-06Cast each argument to a polymorphic constructor into it's most general typeAlasdair Armstrong
2018-08-06More fixes for polymorphic data typesAlasdair Armstrong
2018-08-02Start working on a solution for correctly monomorphising polymorphic variant ↵Alasdair Armstrong
types
2018-07-05Passes all tests and now builds mips and cheri againAlasdair
2018-06-29Try to fix some tricky C compilation bugs, break everything insteadAlasdair Armstrong
2018-06-27Fix reading reals from strings in C libAlasdair Armstrong
2018-06-26Add configuration registers so __SetConfig ASL can be translatedAlasdair Armstrong
Registers can now be marked as configuration registers, for example: register configuration CFG_RVBAR = 0x1300000 They work like ordinary registers except they can only be set by functions with the 'configuration' effect and have no effect when read. They also have an initialiser, like a let-binding. Internally there is a new reg_dec constructor DEC_config. They are intended to represent configuration parameters for the model, which can change between runs, but don't change during execution. Currently they'll only work when compiled to C. Internally registers can now have custom effects for reads and writes rather than just rreg and wreg, so the type signatures of Env.add_register and Env.get_register have changed, as well as the Register lvar, so in the type checker we now write: Env.add_register id read_effect write_effect typ rather than Env.add_register id typ For the corresponding change to ASL parser there's a function is_config in asl_to_sail.ml which controls what becomes a configuration register for ARM. Some things we have to keep as let-bindings because Sail can't handle them changing at runtime - e.g. the length of vectors in other top-level definitions. Luckily __SetConfig doesn't (yet) try to change those options. Together these changes allow us to translate the ASL __SetConfig function, which means we should get command-line option compatibility with ArchEx for running the ARM conformance tests.
2018-06-23Split Sail->ANF translation into its own fileAlasdair
Refactor the C compilation process by moving out the conversion to A-normal form into its own file. Also make the A-normal form AST parameterised by the type of the types annotating it. The idea being we can have a typ aexp -> ctyp aexp translation, converting to low-level types at a slightly higher level before mapping into our low-level IR. This would fix some issues we have where the type of variables change due to flow typing, because we could map the sail types to low-level types in the ANF ast where we still have some knowledge about the structure of the original Sail.
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-21Simplify the ANF->IR translationAlasdair Armstrong
Previously the ANF->IR translation cared too much about how things were allocated in C, so it had to constantly check whether things needed to be allocated on the stack or heap, and generate different cequences of IR instructions depending on either. This change removes the ialloc IR instruction, and changes iinit and idecl so that the code generator now generates different C for the same IR instructions based on the variable types involved. The next change in this vein would be to merge icopy and iconvert at the IR level so that conversions between uint64_t and large-bitvectors are inserted by the code generator. This would be good because it would make the ANF->IR translation more robust to changes in the types of variables caused by flow-typing, and optimization passes could convert large bitvectors to uint64_t as local changes.
2018-06-14rename all lem support files to sail2_foo to avoid conflict with sail1 in rmemJon French
2018-06-14Refactor C backend, and split RTS into multiple filesAlasdair
2018-06-06Factor utility functions for IR into separate file and struct update ↵Alasdair Armstrong
optimizations. Move the utility functions for graph generation and pretty printing of intermediate representation instructions into a separate file, bytecode_util.ml, by analogy with ast_util.ml. Add an optimization pass that searches for specific patterns of struct updates and removes uncessary copying of the structs involved. With this optimisation pass the time taken for u-boot to run approx 57,000,000 instructions goes down from about 11-12 minutes to 8 minutes (about 120,000 IPS).