sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2019-01-31	Merge branch 'monads' into asl_flow2	Thomas Bauereiss

2019-01-31	Further restrict attention to Int kids	Thomas Bauereiss

2019-01-30	Cache compilation results to improve build times for repeated builds	Alasdair

2019-01-29	Fixes for full v8.5	Alasdair Armstrong

2019-01-29	Add an option to crudely slice a function out of a Sail model	Brian Campbell
	Not ideal because it keeps everything that's not a function, but good enough for quick tests extracted from arm.
2019-01-29	Monomorphisation: add missing tyvar substitution during constrant propagation	Brian Campbell

2019-01-29	Add a few more type annotations after mono rewrites	Thomas Bauereiss

2019-01-29	Merge branch 'sail2' into asl_flow2	Thomas Bauereiss

2019-01-29	Improve generation of initial register state	Thomas Bauereiss
	Define initial values for record types once instead of repeating them in the initial register state.
2019-01-29	Monomorphisation: restrict our attention to Int kids	Brian Campbell

2019-01-28	Lem: Be more careful about nexps occurring in the function signature	Thomas Bauereiss
	Don't ask Z3 to simplify them, as flow typing might lead to different results in different if-branches, for example, leading to type errors in Lem.
2019-01-25	Monomorphisation: update a built-in name	Brian Campbell

2019-01-25	Fix solution finding using SMT by looking for the right variable	Brian Campbell

2019-01-25	Coq: add enough to generate some output for arm-v8.5-a	Brian Campbell
	Now supports mutual recursion, configuration registers (in the same way as Lem), boolean constraints (but produces some ugly stuff that the solver can't handle).
2019-01-24	Start supporting informative bool types in Coq backend	Brian Campbell

2019-01-24	Make recheck_defs_without_effects restore old flag properly	Brian Campbell

2019-01-23	Minor opam release to fix #26. Also includes new unrolling pragma.	Robert Norton

2019-01-23	Don't let "make" fail unnecessarily in lib/isabelle	Thomas Bauereiss
	Only check for availability of Lem library if actually trying to build an Isabelle heap image.
2019-01-23	Make rewriting of E_assign a bit more robust	Thomas Bauereiss

2019-01-23	Add another flow-typing case for E_internal_plet	Thomas Bauereiss
	Copied from a corresponding case for E_block, so that this flow typing still gets picked up after E_block has been rewritten away.
2019-01-22	Add some more test cases	Alasdair Armstrong

2019-01-22	Add a pragma for unrolling recursive functions	Alasdair Armstrong
	For example in RISC-V for the translation table walk: $optimize unroll 2 val walk32 ... function walk32 ... would create two extra copies of the walk_32 function, walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2 being recursive. Currently we only support the case where we have $optimize unroll, directly followed by a valspec, then a function, but this should be generalised in future. This optimization nearly doubles the performance of RISC-V It is implemented using a new Optimize.recheck rewrite that replaces the ordinary recheck_defs pass. It uses a new typechecker check_with_envs function that allows re-writes to utilise intermediate typechecking environments to minimize the amount of AST checking that occurs, for performance reasons. Note that older Sail versions including the current OPAM release will complain about the optimize pragma, so this cannot be used until they become up to date with this change.
2019-01-22	Bump opam version for release.	Robert Norton

2019-01-22	Build isabelle and hol files in lib from lem before opam install.	Robert Norton

2019-01-22	Don't hardcode location of BBV library	Thomas Bauereiss

2019-01-22	Make sure there is an ocaml representation for optimized memory read for	Alasdair
	RISC-V
2019-01-22	Make sure we optimize constrained union constructors	Alasdair

2019-01-21	The RISCV environment variable collides with common usage by the RISC-V ↵	Prashanth Mundkur
	toolchain; use SAIL_RISCV instead to refer to sail-riscv.
2019-01-21	Pass Lem library path to Isabelle	Thomas Bauereiss

2019-01-21	Don't require manual set up of Isabelle session directories	Thomas Bauereiss
	Since Isabelle 2018, specifying the same directory both on the command line and persistently in the user's ROOTS file is allowed, so we don't have to choose between one or the other any more.
2019-01-21	Fix typo in install instructions	Alasdair Armstrong

2019-01-21	Remove old emacs mode to avoid confusion	Alasdair Armstrong

2019-01-21	Update manual snapshot and add basic sail -latex documentation	Alasdair Armstrong

2019-01-21	Fix build of Isabelle documentation	Thomas Bauereiss

2019-01-21	Add output directory option for generated Isabelle auxiliary theories	Thomas Bauereiss

2019-01-21	Fix some issues with latex generation so manual builds again	Alasdair Armstrong
	since riscv is no longer in this repository, and we use the RISC-V duopod as an example, you need to build as: make RISCV=directory manual.pdf if directory is not equal to ../../sail-riscv (which is where it would be if sail and sail-riscv are checked out in the same respository together)
2019-01-21	Fix a bug with type-checking and latex generation	Alasdair Armstrong
	We should maybe just make the -latex option behavior the default to avoid this kind of thing
2019-01-19	wib	Shaked Flur

2019-01-17	Work around an issue with type abbreviations in HOL	Thomas Bauereiss
	If we use the bitlist representation of bitvectors, the type argument in type abbreviations such as "bits('n)" becomes dead, which confuses HOL; as a workaround, expand type synonyms in this case.
2019-01-17	Output configuration registers for Lem	Thomas Bauereiss
	Treat them as constants for now (with their initial value); in order to support updates, we would have to embed them properly into the monads.
2019-01-17	Fix bug in letbind_effects rewrite	Thomas Bauereiss
	Don't wrap effectful expressions in E_internal_return
2019-01-16	Latex: handle underscores when generating latex names.	Prashanth Mundkur

2019-01-14	Add options for output directories for the lem and coq backends.	Prashanth Mundkur

2019-01-14	Add a function to perform re-writes in parallel	Alasdair
	rewrite_defs_base_parallel j is the same as rewrite_defs_base except it performs the re-writes in j parallel processes. Currently only the trivial_sizeof re-write is parallelised this way with a default of 4. This works on my machine (TM) but may fail elsewhere. Because 2019 OCaml concurrency support is lacking, we use Unix.fork and Marshal.to_channel to send the info from the child processes performing the re-write back to the parent. Also fix a missing case in pretty_print_lem
2019-01-14	Support some more unification cases	Thomas Bauereiss

2019-01-14	Make rewriting of foreach loops for Lem more robust	Thomas Bauereiss
	Bind loop bounds to type variables, and don't pull existential variables out of context
2019-01-14	Merge remote-tracking branch 'origin/sail2' into asl_flow2	Alasdair

2019-01-13	update README	Peter Sewell

2019-01-13	update README with current model repos	Peter Sewell

2019-01-11	Updates for sail-arm release	Alasdair Armstrong
	We want to ensure that no_devices.sail and devices.sail have the same effect footprint, because with a snapshot-type release in sail-arm, we can't rebuild the spec with asl_to_sail every time we switch from running elf binaries to booting OS's. This commit allows registers to have arbitrary effects, so registers that are really representing memory-mapped devices don't have to have the wmem/rmem effect.