summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2018-08-02Coq: limit eauto to ensure termination in reasonable timeBrian Campbell
2018-08-02Fill in more Coq builtins for aarch64Brian Campbell
2018-08-02Update a few prover gitignoresBrian Campbell
2018-08-01Coq: implicit range conversions for function arguments, debug tracingBrian Campbell
The new option -dcoq_debug_on takes a list of functions to output tracing on.
2018-07-23RTS: make g_cycle_count publicAlastair Reid
This allows debug messages to include the current cycle count which can be useful for debugging.
2018-07-18Coq: constraint solving improvementsBrian Campbell
Use eauto so that user-added hints are more flexible, example with Replicate in aarch64, dropped zbool to prevent slow proof searches (and preprocessing deals with boolean comparisons now). Report failed constraints after preprocessing; Separate preprocessing tactic out.
2018-07-17Coq: integer shiftsBrian Campbell
2018-07-17Coq: add printing stubsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
Adds missing constraints for aarch64
2018-07-16Coq: add support for more complex atom typesBrian Campbell
As a result, add proof to pow2.
2018-07-13Merge branch 'sail2' of github.com:rems-project/sail into sail2Brian Campbell
2018-07-12Add missing builtins needed for cheri128 C. Still doesn't build possibly due ↵Robert Norton
to code gen issue.
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ↵Robert Norton
interpreter implementations of same.
2018-07-12Coq: handle all bool conjunctions/disjunctionsBrian Campbell
2018-07-12Coq: remove unnecessary constraint on foreach loopsBrian Campbell
2018-07-11Partially revert change to add_vec_int et alThomas Bauereiss
On second thought, this change should not really make a difference; the CHERI test suite still passes without it. Moreover, using unsigned conversion of the vector argument leads to more convenient lemmas for the provers.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 19:49:20 +0000