sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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.