sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-07-07	Warn when we can't monomorphise a constructor application	Brian Campbell

2017-07-07	Correct variable mapping when splitting constructor patterns for ↵	Brian Campbell
	monomorphisation
2017-07-07	Implement basic monomorphisation of constructors	Brian Campbell

2017-07-03	Cleanup, and add support for variable bindings in bitvector patterns	Thomas Bauereiss

2017-06-30	Split bit patterns for monomorphisation, do equality checks	Brian Campbell
	(e.g., for some ARM decoding functions)
2017-06-29	Rewrite bitvector patterns	Thomas Bauereiss
	Seems to work for CHERI-MIPS, but still a few things to be done, e.g. collecting let bindings for variables bound in bitvector patterns
2017-06-29	Propagate type information from reducing case expressions	Brian Campbell

2017-06-29	Ocamlbuild targets should always be remade	Brian Campbell

2017-06-28	Reduce simple enumeration cases during monomorphisation	Brian Campbell

2017-06-28	Use more plausible type for E_case	Brian Campbell
	(Previously it used the last branch's type!)
2017-06-23	Get rid of bogus singleton pattern warnings	Brian Campbell

2017-06-23	Add option for monomorphisation splitting	Brian Campbell

2017-06-23	Basic constant propagation for partial monomorphisation	Brian Campbell

2017-06-22	Initial partial monomorphisation work	Brian Campbell
	Splits specified pattern matches on enumerations (other types to be added later); no constant propogation yet.
2017-06-21	Merge	Thomas Bauereiss

2017-06-21	Pretty-print bitvector expressions	Thomas Bauereiss
	- Add case distinctions between bitvector types and vectors of other element types (e.g. registers) and use the corresponding operations (i.e. "bvslice", "bvaccess", etc for the former, and "slice", "access", etc for the latter) when pretty-printing expressions - Add type annotations to expressions when the type includes bitvectors with concretely known length - Update state.lem to use bitvectors (in the interface, at least; internally, bitvectors are still stored as bit lists for now, since that makes it easier to support storing different registers with different lengths) This has been tested with the CHERI-MIPS model with some success, but some things are still missing: - Bitvector patterns are not handled yet - Some bitvector length monomorphisation is needed in a few places of the model - Some type annotations are missing, because the (old) Sail type checker does not infer bitvector lengths in some instances where one would hope it to do that; this should be checked with the new type checker
2017-06-19	Fix Show on Lem bitvector	Brian Campbell

2017-06-16	Some Isabelle fixes for word version of sail_values	Brian Campbell

2017-06-15	Pretty-print bitvector types	Thomas Bauereiss
	Next up: Expressions, patterns
2017-06-15	Replace sail_values.lem with Brian's machine word version	Thomas Bauereiss

2017-06-14	Add a work-in-progress version of sail_values.lem	Brian Campbell
	that uses the new Lem machine words library.
2017-06-13	Add Makefile and ROOT for Isabelle library	Thomas Bauereiss

2017-06-05	Attempt to make Lem-prettyprinting of function clauses more robust	Thomas Bauereiss
	Instead of abusing patterns as expressions, bind patterns to names (if they are more complex than an identifier or literal and don't have a name already) and generate expressions referring to those names (which we then pass as arguments to the auxiliary functions).
2017-06-05	Fix pretty-printing of function clauses with wildcards for Lem	Thomas Bauereiss
	Before, wildcards sometimes ended up in the arguments to the function call on the RHS, in particular when using vector patterns (which implicitly introduce wildcards for the order and index parameters).
2017-06-02	Add tag memory to Lem shallow embedding	Thomas Bauereiss

2017-05-28	fixed exmem	Shaked Flur

2017-05-26	fix run_with builds after build_context gained an extra argument.	Robert Norton

2017-05-26	add cmovz and cmovn conditional capability move instructions new in ISAv6.	Robert Norton

2017-05-26	Update ctoptr instruction to check that all of ct is within bounds of cb and ↵	Robert Norton
	that cb is not sealed as per ISAv6.
2017-05-26	in ISAv6 cjr and cjalr are permitted on local capabilities.	Robert Norton

2017-05-26	add support for the new ccall selector 1 implementation that directly ↵	Robert Norton
	unseals capabilities.
2017-05-24	fixed missing _tag bits	Shaked Flur

2017-05-24	Merge branch 'master' of bitbucket.org:Peter_Sewell/sail	Shaked Flur
	# Conflicts: # src/lem_interp/interp.lem # src/lem_interp/interp_inter_imp.lem # src/lem_interp/interp_interface.lem # src/parser.mly # src/pretty_print_lem.ml
2017-05-24	added the exmem effect for AArch64 store-exclusive	Shaked Flur

2017-05-24	Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from ↵	Robert Norton
	data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
2017-05-24	it turns out that Zarith has a divide function which does truncation towards ↵	Robert Norton
	zero but it is not exposed via Bit_int_Z. Use it instead of rolling our own. Also ocaml / and mod already do the right thing.
2017-05-10	Fix type error in CGetLen	Thomas Bauereiss
	For some reason, Lem did not like the call to "min" when exporting to Isabelle. Replacing "min" with an if-then-else expression solves this. This is also in line with the CHERI spec, which actually uses an if block.
2017-05-10	Further to Thomas's commit remove the duplicate declarations of max_otype ↵	Robert Norton
	and have_cp2.
2017-05-10	Add stubs for TAGw	Thomas Bauereiss
	Tagged memory seems to be currently missing in the Lem shallow embedding of (CHERI-)MIPS.
2017-05-10	Comment out duplicate definitions in cheri_types.sail	Thomas Bauereiss
	They are already defined in cheri_prelude_common.sail
2017-05-10	Build Cheri_embed_types.thy together with Cheri_embed_sequential.thy	Thomas Bauereiss

2017-05-08	add make rules to (attempt to) build arm and power ml.	Robert Norton

2017-05-08	add target for building ocaml shallow embed for arm.	Robert Norton

2017-05-08	add some missing things in sail_values and make big_int version the default ↵	Robert Norton
	for set_vector_subrange_bit.
2017-05-08	add error messages for unhandled pattern match nodes in ocaml pretty printer.	Robert Norton

2017-05-08	put failwith in brackets to avoid parse error.	Robert Norton

2017-05-02	doc	Peter Sewell

2017-04-27	avoid out of bounds indicies in cheri128 decompression functions.	Robert Norton

2017-04-27	also trace memory writes.	Robert Norton

2017-04-27	remove undefined value from cheri 128 spec. The ocaml shallow embedding ↵	Robert Norton
	cannot handle undef structs and the value should not be used (could be option type but wanted a similar interface to incCapOffset and setCapOffset).