summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2018-08-30Annotate the RISC-V prelude for C builtins.Prashanth Mundkur
Add some builtins to the C sail lib. Enable some gcc warnings.
2018-08-30C: Fix a bug where function argument type becomes more specific due to flow ↵Alasdair Armstrong
typing Added a regression test as c/test/downcast_fn.sail
2018-08-30Coq: correct endianness reversal bugBrian Campbell
2018-08-29C: Fix some issues with tuples as arguments to polymorphic constructorsAlasdair Armstrong
Now all we need to do is make sure the RISC-V builtins are mapped to the correct C functions, and RISC-V in C should work (hopefully). We're still missing some of the functions in sail.c for the mappings so those have to be implemented.
2018-08-29Updated snapshots for Isabelle 2018Thomas Bauereiss
2018-08-28Coq: make some library definitions computeBrian Campbell
2018-08-28Adapt theory imports for Isabelle 2018Thomas Bauereiss
Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860
2018-08-20Add some more test cases for C compilationAlasdair Armstrong
Test that basic bi-directional mappings compile correctly Test that a minimal file importing the prelude compiles correctly
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell
- Fill in Coq builtins for more of the RISC-V prelude - Update Barriers - More general autocast - Temporary sub_nat definition (until the backend handles nat better) - Patch to bring results into a reasonable state - Use Let rather than Definition for non-dependent top-level values
2018-08-14Coq: attempt a quick proof before an indepth oneBrian Campbell
2018-08-14Merge remote-tracking branch 'origin/sail2' into polymorphic_variantsAlasdair Armstrong
2018-08-13Coq: more strings for RISC-VBrian Campbell
2018-08-13Coq: drop irrelevant definitions before constraint solvingBrian Campbell
(which were slowing down RISCV unacceptably because dealing with the xlen max/min values is surprisingly expensive)
2018-08-10Coq: add some of string libraryBrian Campbell
2018-08-09Coq: a bit more handling of unknown constraintsBrian Campbell
2018-08-07Improve cast introduction for LemBrian Campbell
Handles mutable variables and conditionals (there are still some corner cases that don't appear in Aarch64 to do). The pretty printer is now back to preferring to use concrete types, but has a special case for casts to print more general types.
2018-08-06Cast each argument to a polymorphic constructor into it's most general typeAlasdair Armstrong
2018-08-03Coq: use a dummy constraint when the real one is unknownBrian Campbell
Not really what we want, but a useful placeholder because of the widespread use of ex_int.
2018-08-03Coq: generalise dependent pair handling a littleBrian Campbell
1. for monadic values (not in a terribly useful way, though) 2. for more types
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 08:15:16 +0000