sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2020-08-10	Fix a C backend bug with letbindings in guards shadowing body definitions	Alasdair

2020-05-22	Fix atomicity of register field writes	Alasdair
	Previous merge commit caused some code that was generating register.field = value to instead generate temp = register temp.field = value register = temp This was caused by rewriter changes affecting the ANF form, and the Jib compilation was sensitive to small changes in the ANF form when compiling l-expressions. Rather than applying a band-aid fix in the rewriter this commit re-factors the ANF translation of l-expressions to ensure that the jib compilation is more robust and able to consistently generate the correct l-expressions without introducing additional read-modify-write expressions in the code.
2020-05-12	Add support for instrumenting generated C with branch coverage metrics	Alasdair
	Will call: void sail_branch_reached(int branch_id, char source_file, int l1, int c1, int l2, int c2); on each branch caused by a match or if statement in the source code For each branch that is taken, will call: void sail_branch_taken(int branch_id, char source_file, int l1, int c1, int l2, int c2) Every branch gets a unique identifier, and the functions are called with the source file location and line/character information for the start and end of each match case or then/else branch. sail_branch_reached is given the location info for the whole match statement.
2019-10-28	Some C backend refactoring	Alasdair
	Make it so that jib_compile.ml never relies on specific string encodings for various constructs in C. Previously this happened when monomorphisation occured for union constructors and fields, i.e. x.foo -> x.zfoo_bitsz632z7 Now identifiers that can be modified are represented as (id, ctyp list) tuples, so we can keep the types x.foo -> x.foo::<bits(32)> This then enables us to do jib IR -> jib IR rewrites that modify types In particular there is now a rewrite that removes tuples as an IR->IR pass rather than doing it ad-hoc in the C code generation, although this is not on by default Note that this change seems to have triggered an Ott bug so jib.lem is now checked in and not generated from Ott
2019-10-25	Remove global symbol generator	Alasdair
	Rather than having a global symbol generating function gensym used throughout the C backend, instead 'generate' them as needed like: let (gensym, reset_gensym_counter) = symbol_generator "gs" This just makes things a bit neater and means we can reset the counter between definitions in jib_compile without worrying about other modules relying on global uniqueness
2019-04-20	SMT: Support writing to register references	Alasdair Armstrong
	Add a new AE_write_ref constructor in the ANF representation to make writes to register references explicit in Jib_compile
2019-04-17	SMT: Unroll simple foreach loops	Alasdair Armstrong

2019-04-09	SMT: Refactor Jib values to make inlining work	Alasdair Armstrong
	Had to change the hundreds and hundreds of places such values were used. However this now lets us automatically prove cheri-concentrate properties. Such as showing function prop_cap_round_trip(cap: bits(128)) -> bool = { let cap_rt = capToBits(capBitsToCapability(true, cap)); cap == cap_rt } is always true.
2019-03-22	C: Fix as-patterns in C output	Alasdair Armstrong
	Most such patterns are re-written away by various re-writing steps, but for those that arn't they are fairly easy to handle by just having as patterns directly in the ANF-patterns. Fixes #39
2019-03-11	Improve ocamldoc comments	Alasdair Armstrong
	Check in a slightly nicer stylesheet for OCamldoc generated documentation in etc. Most just add a maximum width and increase the font size because the default looks absolutely terrible on high-DPI monitors. Move val_spec_ids out of initial_check and into ast_util where it probably belongs. Rename some functions in util.ml to better match the OCaml stdlib.
2019-03-08	C: Refactor C backend	Alasdair Armstrong
	Main change is splitting apart the Sail->IR compilation stage and the C code generation and optimization phase. Rather than variously calling the intermediate language either bytecode (when it's not really) or simply IR, we give it a name: Jib (a type of Sail). Most of the types are still prefixed by c/C, and I don't think it's worth changing this. The various parts of the C backend are now in the src/jib/ subdirectory src/jib/anf.ml - Sail->ANF translation src/jib/jib_util.ml - various Jib AST processing and helper functions (formerly bytecode_util) src/jib/jib_compile.ml - Sail->Jib translation (using Sail->ANF) src/jib/c_backend.ml - Jib->C code generator and optimizations Further, bytecode.ott is now jib.ott and generates jib.ml (which still lives in src/ for now) The optimizations in c_backend.ml should eventually be moved in a separate jib_optimization file. The Sail->Jib compilation can be parameterised by two functions - one is a custom ANF->ANF optimization pass that can be specified on a per Jib backend basis, and the other is the rule for translating Sail types in Jib types. This can be more or less precise depending on how precise we want to be about bit-widths etc, i.e. we only care about <64 and >64 for C, but for SMT generation we would want to be as precise as possible. Additional improvements: The Jib IR is now agnostic about whether arguments are allocated on the heap vs the stack and this is handled by the C code generator. jib.ott now has some more comments explaining various parts of the Jib AST. A Set module and comparison function for ctyps is defined, and some functions now return ctyp sets rather than lists to avoid repeated work.