sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2019-06-13	Add AST for greater-than and less-than constraints	Brian Campbell
	Mostly to make constraints sent to the SMT solver and Coq nicer, but also makes it easy to remove uninformative constraints in the Coq back-end.
2019-05-24	Add a :thin_slice command to isail to isolate a given set of functions	Brian Campbell

2019-05-20	Filter termination measures during slicing	Brian Campbell

2019-05-20	Speed up graph construction by always keeping graph in normalized form	Brian Campbell
	Only checks the leaves that were added in each add_edge/add_edges call. Slicing bits of the 8.5 model went (for me) from intractable to about one second.
2019-05-14	Add feature that allows functions to require type variables are constant	Alasdair Armstrong
	can now write e.g. forall (constant 'n : Int) rather than forall ('n: Int) which requires 'n to be a constant integer value whenever the function is called. I added this to the 'addrsize variable on memory reads/writes to absolutely guarantee in the SMT generation that we don't have to worry about the address being a variable length bitvector.
2019-03-27	C: Generate C from sliced specifications	Alasdair Armstrong

2019-03-26	Rewriter: Expose rewrite passes to interactive mode	Alasdair Armstrong
	Rather than each rewrite being an opaque function, with separate lists of rewrites for each backend, instead put all the rewrites into a single list then have each backend define which of those rewrites it wants to use and in what order. For example, rather than having let rewrite_defs_ocaml = [ ... ("rewrite_undefined", rewrite_undefined_if_gen false); ... ] we would now have let all_rewrites = [ ... ("undefined", Bool_rewriter (fun b -> Basic_rewriter (rewrite_undefined_if_gen b))); ... ] let rewriters_ocaml = [ ... ("undefined", [Bool_arg false]); ... ] let rewrite_defs_ocaml = List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewriters_ocaml This means we can introspect on the arguments required for each rewrite, allowing a :rewrite command in the interactive mode which can parse the arguments required for each rewrite, so we can invoke the above rewrite as sail> :rewrite undefined false with completion for the rewrite name based on all_rewrites, and hints for any arguments. The idea behind this is if we want to generate a very custom slice of a specification, we can set it up as a sequence of interpreter commands, e.g. ... :rewrite split execute :slice_roots execute_LOAD :slice_cuts rX wX :slice :rewrite tuple_assignments ... where we slice a spec just after splitting the execute function. This should help in avoiding an endless proliferation of additional options and flags on the command line.
2019-03-06	Improve AST slicing	Alasdair Armstrong

2019-03-06	Add option to slice out printing and tracing functions when generating C	Alasdair Armstrong
	Make instruction dependency graph use graph.ml Expose incremental graph building functions for performance in graph.mli
2019-03-01	WIP: Start working on being able to slice single instructions out of specs	Alasdair Armstrong