sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-07-24	Merge remote-tracking branch 'origin/sail2' into c_fixes	Alasdair Armstrong

2018-07-24	Now builds mips spec again.	Alasdair
	Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging
2018-07-23	Coq: faster MIPS extras without confusing message	Brian Campbell

2018-07-12	Add missing builtins needed for cheri128 C. Still doesn't build possibly due ↵	Robert Norton
	to code gen issue.
2018-07-12	update arm and mips models for new type of write_ram builtin. Also fix c and ↵	Robert Norton
	interpreter implementations of same.
2018-07-11	Update CHERI code extraction from Isabelle	Thomas Bauereiss
	Also use zero-initialised memory. Apparently some tests access unitialised memory, and the default behaviour of the Lem shallow embedding is to fail in this case.
2018-07-10	Make HOL build properly again for all of the models	Brian Campbell

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	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-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-06	changes to increase MIPS coverage -- remove optional/unused PREF instruction ↵	Robert Norton
	and unused cases in ll/sc match
2018-07-05	mips: ignore unused functions warnings caused by making some functions static.	Robert Norton

2018-07-04	mips: move rmem integration instructions into separate file (disabled for ↵	Robert Norton
	now) to avoid coverage noise.
2018-07-03	cheri: refine lwl/lwr cap length checks to be exact. They were previously a ↵	Robert Norton
	bit loose, but conservative.
2018-07-03	mips: just whitespace.	Robert Norton

2018-07-03	Fill in a few Coq functions for CHERI from the MIPS prelude	Brian Campbell

2018-07-02	Coq modulus operation that fits the type	Brian Campbell

2018-07-02	Coq building rule in MIPS makefile	Brian Campbell

2018-06-29	Try to fix some tricky C compilation bugs, break everything instead	Alasdair Armstrong

2018-06-28	Add tagged memory to C rts to cheri can be compiled to C	Alasdair Armstrong

2018-06-27	Add a mips_c_gcov target that builds mips_c model with coverage reporting.	Robert Norton

2018-06-27	Add a new function cycle_limit_reached that returns bool, allowing for ↵	Robert Norton
	graceful exit on reaching cycle limit. This aids coverage and valgrind instrumentation.
2018-06-26	mips: fix duplication of cycle_count call that arose due to git merge.	Robert Norton

2018-06-26	mips: comment out printing of EXCEPTION on every ISA exception.	Robert Norton

2018-06-26	turn on warnings when compiling mips c then dial back ones that are ↵	Robert Norton
	triggered by generated code (probably false positives). Fix some warnings in rts.c
2018-06-25	Support bitlist representation in Sail2_string	Thomas Bauereiss

2018-06-25	Coq: add typeclass based comparison, and instantiate for enums	Brian Campbell

2018-06-25	Use getopt rather than argp for Mac compatibility in C runtime	Alasdair Armstrong
	Also further tweaks to Sail library for C and include sail lib files for tracing
2018-06-25	add device tree file for mips.	Robert Norton

2018-06-25	mips: add optional tracing of register writes (commented out).	Robert Norton

2018-06-25	Fix bugs in mips ldl/ldr that were probably introduced in porting to sail2.	Robert Norton

2018-06-22	Fix Lem build of MIPS/CHERI	Thomas Bauereiss

2018-06-22	Add current state of mips_extras.v	Brian Campbell

2018-06-22	Add bitvector size constraints in MIPS	Brian Campbell

2018-06-22	Add coq builtins for MIPS	Brian Campbell

2018-06-22	Add coq generation rule for mips	Brian Campbell

2018-06-22	add support for new cycle_limit feature in mips.	Robert Norton

2018-06-21	Remove loading kernel from mips main	Alasdair Armstrong

2018-06-21	Merge branch 'tracing' into sail2	Alasdair Armstrong

2018-06-21	Fix MIPS wrt changes to C runtime	Alasdair Armstrong
	This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz.
2018-06-18	Add bitvector length constraints to mips inequalities	Brian Campbell
	to match new constraints in prelude
2018-06-11	More efficient bitfield implementation	Alasdair Armstrong

2018-06-08	add sail as dependency of mips targets.	Robert Norton

2018-06-07	Refactor mips main a little to work around apparent bug in c generation. ↵	Robert Norton
	Generated c Works with no gcc optimisation but fails when optimisation is on, implying undefined behaviour. Probably due to control reaching end of non-void function in exception case.
2018-06-07	Use the vector_dec standard library for mips. This means we get all the c ↵	Robert Norton
	functions ready to go.
2018-06-07	add mips_c target.	Robert Norton

2018-06-04	Add mips.c target in Makefile. Currently triggers assertion failure in ↵	Robert Norton
	c_backend. still need to merge changes to prelude.sail.
2018-06-04	cheri: print debug trace info to stderr to keep it separate from uart output.	Robert Norton

2018-05-18	mips: add support for CP0 Config0.K0 field because a test has appeared for ↵	Robert Norton
	it. This concerns cache behaviour of kernel segment k0 but since we dont have a cache we just store the value. It could be relevant to RMEM if we ever want to support kernel mode there.