sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-07-09	Initialize fresh memory to 0 in the OCaml backend.	Prashanth Mundkur
	This makes it consistent with the C backend, and also makes it easier to compare traces across execution re-runs.
2018-07-09	Log some timing info at the end of riscv execution.	Prashanth Mundkur

2018-07-09	Lem: prefer type variables to constants when looking for equivalent nexps	Brian Campbell
	If we have an nexp that we can't print, look for an equivalent type variable before looking for a constant - the constant may only be valid locally (e.g., under an if) while the type variable will be valid throughout the function. Fixes a problem with aget_Mem on aarch64.
2018-07-09	Add no_devices.sail to be compatible with latest AArch64 prelude and	Alasdair Armstrong
	update aarch64 model
2018-07-09	anonymise another github link.	Robert Norton

2018-07-09	anonymise github link in sail manual.	Robert Norton

2018-07-09	Remove awkward constraints on GetSlice_int for now	Brian Campbell

2018-07-09	Changes for anonymisation. Ensure headers are in correct format. Remove some ↵	Robert Norton
	redundant files.
2018-07-09	Tweak bit casting definitions in MIPS to avoid non-exhaustive patterns	Brian Campbell
	Recent change made them proper matches rather than conditionals, and Coq rejects incomplete matches. (Will need a proper solution later...)
2018-07-09	Coq: remove some unnecessary casts	Brian Campbell

2018-07-09	Support building an anonymised version of manual. Fix sail example in ↵	Robert Norton
	manual. Remove incomplete types chapter from manual per AA's recommendation.
2018-07-09	Update gitignore	Thomas Bauereiss

2018-07-09	Fix bug in rewriting of try-catch-blocks with variable updates	Thomas Bauereiss

2018-07-09	Tweak rewriting of literal patterns for Lem	Thomas Bauereiss

2018-07-09	Add explanatory comment to guard rewriting	Thomas Bauereiss

2018-07-09	Update CHERI code generation from Isabelle	Thomas Bauereiss

2018-07-09	Add some syntactic sugar for Isabelle	Thomas Bauereiss

2018-07-09	Patch some potential uses of uninitialised variables in AArch64	Thomas Bauereiss

2018-07-09	Simplify treating of undefined_bool in Lem library	Thomas Bauereiss
	Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list.
2018-07-09	add riscv_analysis.sail to SAIL_SRCS	Jon French

2018-07-09	add LOADRES, STORECON, AMO to analysis	Jon French

2018-07-09	Bits for bits of aarch64 in coq	Brian Campbell

2018-07-09	Support writes to misa.C in riscv.	Prashanth Mundkur

2018-07-08	Make the riscv fetch-execute loop return instead of exiting when done.	Prashanth Mundkur

2018-07-08	Move the riscv analysis function into its own file for coverage purposes.	Prashanth Mundkur

2018-07-08	Add a riscv coverage target using bisect-ppx.	Prashanth Mundkur

2018-07-08	Add -static flag that controls whether generated C functions are static	Alasdair
	By default generated functions are non-static, using the -static flag makes them static which is useful for measuring coverage using generated code. Some utility helper functions will always be static, but the compiled versions of sail functions won't be unless this flag is set.
2018-07-07	Add reservation traces to riscv tracecmp tool.	Prashanth Mundkur

2018-07-07	Cancel riscv reservation before i/o scheduling, tweak reservation tracing.	Prashanth Mundkur

2018-07-07	Add the lrsc tests from riscv-tests.	Prashanth Mundkur

2018-07-07	An initial fix to riscv lr/sc, needs a review.	Prashanth Mundkur
	This uses a stronger model than the version in Sail-1 in order to perform address alignment checks. The reservation is kept on virtual addresses, and maintained in the platform model, but now the lr/sc definitions need calls to externs to update this state. An alternative was to reserve physical addresses, but that appeared to be more complicated without a lot more changes. Ideally, the model should be parameterizable over both options.
2018-07-07	Add some tracing to riscv address translation.	Prashanth Mundkur

2018-07-07	Coq: bbv have reorganised their repository	Brian Campbell

2018-07-07	Coq: precise generic vectors	Brian Campbell
	(probably still some pattern matching to do, but I don't think the models use that)
2018-07-07	Coq: supply index constraint in for loops	Brian Campbell

2018-07-07	Coq: eq_range should take proofs	Brian Campbell

2018-07-06	Coq: support assertions inside and outside of blocks	Brian Campbell

2018-07-06	Coq: avoid nexp simplification when deciding whether a cast is needed	Brian Campbell

2018-07-06	Coq: Avoid clashes with the monad name, M	Brian Campbell

2018-07-06	Coq: feed assertions into the context	Brian Campbell

2018-07-06	Coq: use List.In predicates in constraint solving; make other bits robust	Brian Campbell

2018-07-06	Coq: reduce use of sumbool_of_bool to relevant constraints	Brian Campbell

2018-07-06	Coq: missing existential building for ranges	Brian Campbell

2018-07-06	Coq: turn off partial support for dropping true constraints, fix strings	Brian Campbell

2018-07-06	Change HighestSetBit into a form that can be handled by c backend. There are ↵	Robert Norton
	still a few builtins missing before cheri128 will work.
2018-07-06	add gcov option for cheri_c. Add cheri128_c target.	Robert Norton

2018-07-06	changes to increase MIPS coverage -- remove optional/unused PREF instruction ↵	Robert Norton
	and unused cases in ll/sc match
2018-07-05	Fix printing of aq/rl flags in risc-v lr/sc.	Prashanth Mundkur

2018-07-05	Fix equality comparisons for variants in C	Alasdair
	Makes sure equality comparisons for variants are compiled correctly. Needed for CHERI and mips, which have structs containing variants. Also make sure that struct equality works for structs containing other structs.
2018-07-05	Coq: get index_list right	Brian Campbell