sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2019-03-15	C: Wrap Jib identifiers	Alasdair
	Avoids duplication between l-expressions and expressions. Also means that special variables like current_exception and have_exception are treated normally by functions such as instr_reads and instr_writes etc. Furthermore we can now easily annotate Jib identifiers in ways that were not previously possible with plain sail ids.
2019-03-14	Add various useful methods to interactive mode	Alasdair Armstrong
	:def <definition> evaluates a top-level definition :(b)ind <id> : <type> creates an identifier within the interactive type-checking environment :let <id> = <expression> defines an identifier Using :def the following now works and brings the correct vector operations into scope. :def default Order dec :load lib/prelude.sail Also fix a type-variable shadowing bug
2019-03-14	C: Some further tweaks	Alasdair Armstrong

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-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-09	C: Fix miscompilation of constrained struct field access	Alasdair
	For a Int-parameterised struct F('x: Int) = ... the optimizer would attempt to optimize field access in cases where 'x was known to constrain the types of the struct fields only locally. Which would create a type error in the generated C. Now we always use the type from the global struct type. However, we previously weren't using struct type quantifiers to optimize the field representation, which we now do. Also rename some utility functions to better match the List functions in the OCaml stdlib.
2019-03-08	Rewriter: Cleanup old sizeof rewrites	Alasdair Armstrong
	Shouldn't affect anything as this is done by the typechecker now. Also remove some unfinished tracing code from c_backend.ml
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.