sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-02-05	Merge changes to type_check.ml	Alasdair Armstrong

2018-02-05	Add typ patterns for destructuring existentials	Alasdair Armstrong

2018-02-05	Allow type variables to be introduced by global let bindings.	Alasdair Armstrong
	This was technically allowed previously but the rules for type variable names in function types were too strict so it didn't work. Also fixed a bug where Nexp_app constructors were never considered identical and fixed a bug where top-level let bindings got annotated with the wrong environment
2018-02-05	riscv: slightly prettier register trace output	Robert Norton

2018-02-05	squash a warning.	Robert Norton

2018-02-02	Added remaining compressed instructions in Quadrant 0 and 1, Quadrant 2 remains.	Prashanth Mundkur

2018-02-02	Add M extension to RISCV. Slightly inelegant implementation for now but ↵	Robert Norton
	passing tests.
2018-02-02	Extra nexp simplification	Brian Campbell

2018-02-02	Add arithmetic shift right for aarch64 mono	Brian Campbell

2018-02-02	Move exp_lift_assign rewrite after fixing effects and retypechecking	Brian Campbell

2018-02-02	When cutting functions short at assertions, put an exit to correct types	Brian Campbell
	if necessary
2018-02-02	Also rewrite boolean terms in asserts during monomorphisation	Brian Campbell
	(otherwise wildcard cases won't be cut short at the assertion)
2018-02-02	Add aarch64 duopod...	Alasdair Armstrong
	... all 4500 lines of it. Need to figure out how to cut out some details to make more minimal.
2018-02-02	Add some more compressed instruction specs, and slightly clean up previous ones.	Prashanth Mundkur

2018-02-02	Allow global type variables	Alasdair Armstrong
	Wanted to know yesterday if possible to parameterise specification by 32/64 bits in context of RISCV - i.e. can we do something like let size = 32 type xlen = bits(size) This patch tweaks the typechecker slightly to allow type variables to be introduced by global let bindings in the same way they can be introduced by local let bindings (techically this was always allowed, but some bugs prevented it from really working), so let 'size : atom(32) = 32 means we have a global type variable 'size, with a global constraint 'size = 32 We can go further though... let 'size : {\|32, 64\|} = 32 means we have a global type variable 'size with a constraint 'size = 32 \| 'size = 64, in this case the specification will only typecheck if the specification is correct for BOTH 'size = 32 and 'size = 64. This also creates a global binding size (note no tick) with value 32 and type atom('size), one can also do let _ as 'size : {\|32, 64\|} = 32 which won't create the binding, only the type variable. These global type variables are bound to not be very well understood by certain parts of sail, so typical here be dragons warning etc.
2018-02-01	More work on C compilation	Alasdair Armstrong
	Can now compile things like early returns. The same approach should work for exception handling as well. Once that's in place, just need to work a bit more on getting union types to work + the library of builtins, then we should be able to compile and run some of our specs via C. Also added some documentation in comments for the general approach taken when compiling (need many more though).
2018-02-01	Fix atom -> itself transformation when clauses feature different set of sizes	Brian Campbell

2018-02-01	Curtail function bodies at known-false assertions during mono	Brian Campbell
	(preventing non-monomorphised sizes appearing in wildcard cases)
2018-02-01	Proper substitution and propagation of size from last commit	Brian Campbell

2018-02-01	Substitute extra size case splits into body in monomorphisation	Brian Campbell

2018-02-01	Make mono add case expressions for size tyvars without a corresponding arg	Brian Campbell

2018-02-01	Use the recursive execute for c.addi4spn.	Prashanth Mundkur
	Conversations with Alexandre/Jon indicate that a BSV generator should be able to deal with this recursion, and Thomas has fixed the Lem generator.
2018-02-01	badaddr is a misleading name, since it could contain what the PC points to ↵	Prashanth Mundkur
	for illegal-instruction exceptions. changed to excinfo.
2018-02-01	Comment out special casing of execute function in Lem pretty-printer	Thomas Bauereiss
	It assumes that execute is non-recursive, which is not the case for RISC-V with compressed instructions. Splitting execute into different auxiliary functions for each clause is probably still useful, as Isabelle is likely to parse many small functions faster than one big (potentially recursive) function, but this splitting should be done in the rewriter instead of the pretty-printer, in order to properly deal with recursion.
2018-02-01	riscv: avoid name clash with global function 'unsigned'.	Robert Norton

2018-02-01	Fix a bug where local variables could shadow functions	Alasdair Armstrong
	Currently the fix is to disallow this shadowing entirely, because it seems to cause trouble for ocaml.
2018-02-01	More work on running sail tests compiled to C	Alasdair Armstrong

2018-02-01	Remove trace viewer application from repository	Alasdair Armstrong

2018-02-01	Can now compile some simple sail programs to C	Alasdair Armstrong

2018-02-01	Clean up riscv_duopod sail and add make targets for ocaml and Isabelle.	Robert Norton

2018-02-01	Add c.addi4spn.	Prashanth Mundkur

2018-02-01	Fix encoding for compressed ILLEGAL.	Prashanth Mundkur

2018-02-01	Initial top-level support for compression instructions.	Prashanth Mundkur
	- introduce the misa register - check the appropriate instruction bits to decide whether it is compressed - check misa.C to decide whether we can execute compressed instructions - add a decodeCompressed function - add two of the most basic RVC instructions: NOP and ILLEGAL
2018-01-31	Try to make bitvector pattern rewriting more robust	Thomas Bauereiss
	Look deep into sub-patterns for identifiers and literals instead of relying on assumptions about possible nestings
2018-01-31	Fix bug in bitvector pattern rewriting	Thomas Bauereiss
	Make rewriter look into P_typ patterns instead of throwing them away.
2018-01-31	More updates to C backend - matching and tuples	Alasdair Armstrong

2018-01-31	Added test case for decode patterns that are currently failing	Alasdair Armstrong

2018-01-31	Find buried set constraints in asserts	Brian Campbell

2018-01-31	Fix mono continue away option	Brian Campbell

2018-01-31	Export arithmetic shift right from Lem library	Thomas Bauereiss

2018-01-31	Add Lem operator wrappers for bitlists	Thomas Bauereiss
	(accidentally committed the wrong file)
2018-01-31	Add wrappers around Lem operators using bitvector type class	Thomas Bauereiss
	Makes bitvector typeclass instance dictionaries disappear from generated Isabelle output.
2018-01-31	Split base definitions of Lem monads and further built-ins (e.g. loop ↵	Thomas Bauereiss
	combinators) Add Isabelle-specific theories imported directly after monad definitions, but before other combinators. These theories contain lemmas that tell the function package how to deal with monadic binds in function definitions.
2018-01-31	add very stripped down 2-instruction RISCV example with add and load.	Robert Norton

2018-01-31	add some elf files from riscv test suite and run them on riscv model.	Robert Norton

2018-01-30	Handle 'N == 1 \| 'N == 2 \| ... style set constraints in mono	Brian Campbell

2018-01-30	Optionally give all monomorphisation errors at once	Brian Campbell
	(and stop afterwards unless asked)
2018-01-30	Fix monomorphisation analysis to detect type variables which need to be	Brian Campbell
	concrete but aren't determined by one of the arguments.
2018-01-30	Fix failing Lem tests	Alasdair Armstrong

2018-01-30	Updates to C backend	Alasdair Armstrong