sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2020-09-28	Refactor: Rename 'a defs to 'a ast	Alasdair
	Change internal terminology so we more clearly distinguish between a list of definitions 'defs' and functions that take an entire abstract syntax trees 'ast'.
2020-09-28	Move the ast defs wrapper into it's own file	Alasdair
	This refactoring is intended to allow this type to have more than just a list of definitions in future.
2020-08-25	Add function sail_set_coverage_file to sail_coverage header	Alasdair
	Can be set by C emulator to control where coverage information is written
2020-06-12	Use output file for generated branch information.	Prashanth Mundkur

2020-05-15	Add coverage tracking tool	Alasdair
	See sailcov/README.md for a short description Fix many location info bugs discovered by eyeballing output
2020-05-11	Functorise and refactor C code generator	Alasdair
	Currently uses the -c2 option Now generates a sail_state struct which is passed as a pointer to all generated functions. This contains all registers, letbindings, and the exception state. (Letbindings must be included as they can contain pointers to registers). This should make it possible to use sail models in a multi-threaded program by creating multiple sail_states, provided a suitable set of thread-safe memory builtins are provided. Currently the sail_state cannot be passed to the memory builtins. For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c. foo_emu.c wraps the generated library into an emulator that behaves the same as the one we previously generated. The sail_assert and sail_match_failure builtins are now in a separate file, as they must exist even when the RTS is not used. Name mangling can be controlled via the exports and exports_mangled fields of the configuration struct (currently not exposed outside of OCaml). exports allows specifying a name in C for any Sail identifier (before name mangling) and exports_mangled allows specifiying a name for a mangled Sail identifier - this is primarily useful for generic functions and data structures which have been specialised.
2019-11-08	Refactor Jib compilation	Alasdair Armstrong
	Split the dynamic context into the ctx struct, and the static configuration into a module which parameterises the sail->jib compilation step rather than just having a giant ctx struct.
2019-10-17	Allow generating C that doesn't hard code any libraries	Alasdair Armstrong

2019-10-14	Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and ↵	Alasdair Armstrong
	bitvectors in C Assumes a Sail C library that has functions with the right types to support this. Currently lib/int128 supports the -Ofixed_int option, which was previously -Oint128. Add a version of Sail C library that can be built with -nostdlib and -ffreestanding, assuming the above options. Currently just a header file without any implementation, but with the right types
2019-05-05	C: Add option to compile using __int128 rather than GMP	Alasdair
	Only requires a very small change to c_backend.ml. Most of this commit is duplication of the builtins and runtime in lib/int128. But the actual differences in those files is also fairly minor could be handled by some simple ifdefs for the integer builtins.
2019-03-19	C: Some simplification	Alasdair Armstrong
	Remove unused experimental optimizations
2019-03-13	C: Improve Jib IR, add SSA representation	Alasdair Armstrong
	Add a CL_void l-expression so we don't have redundant unit-typed variables everywhere, and add an optimization in Jib_optimize called optimize_unit which introduces these. Remove the basic control-flow graph in Jib_util and add a new mutable control-flow graph type in Jib_ssa which allows the IR to be converted into SSA form. The mutable graph allows for more efficient updates, and includes both back and forwards references making it much more convenient to traverse. Having an SSA representation should make some optimizations much simpler, and is also probably more natural for SMT generation where variables have to be defined once using declare-const anyway. Debug option -ddump_flow_graphs now outputs SSA'd graphs of the functions in a specification.
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.