summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2018-07-11Fix off-by-one bugs in monomorphisation rewrites involving bitvector subrangesThomas Bauereiss
CHERI test suite now passes using Isabelle-generated emulator
2018-07-11Fix some signedness bugsThomas Bauereiss
add_vec_int and similar functions in the Lem library used unsigned instead of signed conversion.
2018-07-10Update HOL setupBrian Campbell
2018-07-10Add more Isabelle lemmas to libraryThomas Bauereiss
2018-07-09Changes for anonymisation. Ensure headers are in correct format. Remove some ↵Robert Norton
redundant files.
2018-07-09Update gitignoreThomas Bauereiss
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas 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-09Bits for bits of aarch64 in coqBrian Campbell
2018-07-07Coq: bbv have reorganised their repositoryBrian Campbell
2018-07-07Coq: precise generic vectorsBrian Campbell
(probably still some pattern matching to do, but I don't think the models use that)
2018-07-07Coq: supply index constraint in for loopsBrian Campbell
2018-07-07Coq: eq_range should take proofsBrian Campbell
2018-07-06Coq: use List.In predicates in constraint solving; make other bits robustBrian Campbell
2018-07-05Fix equality comparisons for variants in CAlasdair
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-05Coq: get index_list rightBrian Campbell
2018-07-05Fix equality comparisons for structsAlasdair
Add a test case in test/c/eq_struct.sail. Ensure that the macro EQUAL(type) will always give a valid equality function for any builtin type in sail.h.
2018-07-05restore missing RISC-V fence types in sail2; ignore io bits in fences more ↵Jon French
cleanly
2018-07-02Coq: add some string functionsBrian Campbell
2018-07-02Coq: replace simpl in a tactic with a more precise "change"Brian Campbell
Prevents partial unfolding of Z.pow.
2018-06-30RTS: fix replicate_bitsAlastair Reid
Fixes handling of Replicate(x, 0).
2018-06-30RTS: Add length asserts to bits opsAlastair Reid
Added assertions to check that length of bit operations is sensible (i.e., consistent with type system).
2018-06-30Fix an issue with vector_update_subrangeAlasdair
vector_update_subrange wasn't setting its return length correctly
2018-06-29RTS: tweak TIMEOUT messageAlastair Reid
Making the message more like archex messages simplifies tooling. Plus, it is a better message.
2018-06-28RTS: Fix utterly broken command line parsingAlastair Reid
2018-06-28RTS: Add --verbosity flag to C modelAlastair Reid
This is interpreted as a set of bits that control various bits of output. Bit 0 is print the PC on every cycle. (It would probably be useful to standardise a few of these flags across all models. Other candidates are accesses to physical memory, throwing SAIL exceptions, current privilege level, ...)
2018-06-28Add tagged memory to C rts to cheri can be compiled to CAlasdair Armstrong
2018-06-28Fix warning in rts.cRobert Norton
2018-06-28Add option to build ocaml with bisect_ppx coverage support. Add cheri ↵Robert Norton
targets using this.
2018-06-28RTS: Add missing #includeAlastair Reid
Every Unix is subtly different.
2018-06-27RTS/Main: tweaking cycle counter handlingAlastair Reid
2018-06-27Actually fix real literals, and add a test for various propertiesAlasdair Armstrong
2018-06-27Fix reading reals from strings in C libAlasdair Armstrong
2018-06-27libsail: optimise real_powerAlastair Reid
The Arm spec uses the value 2.0^1000000 to represent infinity so it is worth making real_power take logarithmic time.
2018-06-27Add 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-27Fix real implementation in C to use GMP rationalsAlasdair Armstrong
Implement square root function for rationals up to an arbitrary precision, currently 30 decimal places. May need to increase this for ARM tests.
2018-06-27RTS: __SetConfig support is off by defaultAlastair Reid
Use -DHAVE_SETCONFIG to enable __SetConfig support
2018-06-27RTS: Add support for __ListConfigAlastair Reid
2018-06-27RTS: Delete __SetConfig stub functionAlastair Reid
This is now directly supported from SAIL so we can call the SAIL __SetConfig function instead.
2018-06-26turn 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-26RTS: implement sleep primitivesAlastair Reid
Note that an alternative implementation choice is just to implement them as SAIL functions manipulating a global variable. Not sure which is better.
2018-06-26RTS: stub support for -C command line optionAlastair Reid
2018-06-26ELF: Restore error messages in ELF readerAlastair Reid
2018-06-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-25Use getopt rather than argp for Mac compatibility in C runtimeAlasdair Armstrong
Also further tweaks to Sail library for C and include sail lib files for tracing
2018-06-25flush stdout after putchar for terminal emulation purposes.Robert Norton
2018-06-22Precise bitvector subrange functions for Coq.Brian Campbell
Also fix the constraints in the standard prelude files, add a couple of useful cast rewriting lemmas.
2018-06-22Add coq builtins for MIPSBrian Campbell
2018-06-22Coq: library updates, esp extending bitvector multiplies, UndefinedBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:42:17 +0000