summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2020-10-14Support C coverage when sail_exit is usedBrian Campbell
2020-10-01pass pointer to g_elf_entry to get the ELF entrySander Huyghebaert
2020-09-30Tweak Coq proof to avoid incompatibility with IrisBrian Campbell
(in the previous proof script the intuition tactic found a strange proof involving a type-level dependent pair that imposed an unnecessary universe constraint, this doesn't)
2020-09-12Merge some of the gitignore filesColumbus240
Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq. This commit removes /lib/coq/.gitignore and moves all ignore-statements to /.gitignore . This should simplify the maintenance of gitignore files. The situation with /test/mono/.gitignore is analogous.
2020-09-07Fix typo a mono_rewrites definitionBrian Campbell
- add tests for a couple of related rewrites - accept same range of constants for sign extension in the rewrite as for the zero extension version (to make the test simpler)
2020-09-07Correct external declaration in mono_rewritesBrian Campbell
2020-08-26Coq: replace other uses of omega with liaBrian Campbell
Also remove omega workaround that lia doesn't need.
2020-08-26Coq: replace a lot of omega with liaBrian Campbell
2020-08-26Coq: Use proof mode for a couple of Fixpoints to avoid Coq 8.12 issueBrian Campbell
2020-08-26Coq: make some uses of auto in the library more robustBrian Campbell
2020-08-25Add function sail_set_coverage_file to sail_coverage headerAlasdair
Can be set by C emulator to control where coverage information is written
2020-08-18Move sail_state declaration into it's own fileAlasdair
Useful for RISC-V with it's custom C emulator
2020-08-07Merge branch 'monads' into sail2Brian Campbell
2020-07-02Define extz/s_vec in Sail for non-prover backendsBrian Campbell
2020-06-24Add tagged memory builtins to regfp.sailThomas Bauereiss
Implementations for backends other than Lem not yet implemented/hooked up.
2020-06-17Coq: implement shl_int_1Brian Campbell
2020-06-14Coq: tidy up scope in libraryBrian Campbell
Helps with Coq 8.11. Also fix BBVDIR default in test script.
2020-06-12Coq: fix matching bug in solverBrian Campbell
2020-06-11Coq: specialise the andor solvers to avoid excessive search and solve more goalsBrian Campbell
2020-06-10Prepare Coq library for packagingBrian Campbell
- rename files to get rid of prefix - use -Q to get package name right - add Base.v to make package imports simpler - add opam file for coq package
2020-05-21Merge branch 'mono-tweaks' of github.com:rems-project/sail into mono-tweaksAlasdair
2020-05-21Merge branch 'sail2' into mono-tweaksAlasdair
2020-05-15Add coverage headerAlasdair
2020-05-15Add coverage tracking toolAlasdair
See sailcov/README.md for a short description Fix many location info bugs discovered by eyeballing output
2020-05-14Merge remote-tracking branch 'origin' into codegenAlasdair
2020-05-14Various bugfixes and improvements for updated codegenAlasdair
2020-05-13Make Isabelle lemma generation work with grouped regstateThomas Bauereiss
2020-05-11Functorise and refactor C code generatorAlasdair
Currently uses the -c2 option Now generates a sail_state struct which is passed as a pointer to all generated functions. This contains all registers, letbindings, and the exception state. (Letbindings must be included as they can contain pointers to registers). This should make it possible to use sail models in a multi-threaded program by creating multiple sail_states, provided a suitable set of thread-safe memory builtins are provided. Currently the sail_state cannot be passed to the memory builtins. For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c. foo_emu.c wraps the generated library into an emulator that behaves the same as the one we previously generated. The sail_assert and sail_match_failure builtins are now in a separate file, as they must exist even when the RTS is not used. Name mangling can be controlled via the exports and exports_mangled fields of the configuration struct (currently not exposed outside of OCaml). exports allows specifying a name in C for any Sail identifier (before name mangling) and exports_mangled allows specifiying a name for a mangled Sail identifier - this is primarily useful for generic functions and data structures which have been specialised.
2020-04-28Add flooring division in preludeAlasdair
Defined in terms of tdiv so we don't have to add it to backends that don't already have it
2020-04-21Fix sub_bits interpreter bindingThomas Bauereiss
2020-04-21Add more monomorphisation rewritesThomas Bauereiss
Supporting more ASL idioms
2020-04-21Add support for some ASL idioms in mono rewritesThomas Bauereiss
2020-04-21Add more mono rewrites for bitvector subrangesThomas Bauereiss
2020-04-10Add Lem builtins for operations on realsThomas Bauereiss
... that match the names in lib/real.sail. Also fix the lem mapping for abs_int_atom and a Lem syntax error with nested record updates.
2020-04-10Update path for newer versions of BBV Coq libraryThomas Bauereiss
2020-02-24Allow overloading of subrange builtins for non-bitvectorsThomas Bauereiss
2020-02-21Add barriers to regfp.sail for full ARMv8Alasdair Armstrong
Again use an $ifdef to avoid breaking RMEM. We can't use the same barrier_kind, because we *really* want a plain enumeration both for its simple SMT representation and a simple 1 to 1 mapping to the cat models used by herd. Technically for Isla, all the read_kind/write_kind/barrier_kind etc types can be defined separately on a per-architecture basis anyway, so maybe using this file at all is a bit of an anachronism.
2020-02-05Tweak Coq scopes for 8.11Brian Campbell
2020-02-03Add an __instr_announce builtin in regfp.sailAlasdair Armstrong
Allows keeping track of which instructions actually get executed in a trace
2020-02-03Update regfp.sail with ifetch changes from poly_mapping branchAlasdair Armstrong
However, use an ifdef to make sure the ifetch changes only appear for the ARM spec, because otherwise the generated lem for RMEM will break.
2020-01-21Use hex/bin literals in Coq backendBrian Campbell
Also be more careful to avoid pattern bindings with identifiers to avoid parsing clashes, eg `let 'bytes := ...` which is confused with the notation for binary literals.
2020-01-17Merge branch 'coq-bool-props' into sail2Brian Campbell
2020-01-17Coq: add hex_strBrian Campbell
Now used in RISC-V model.
2020-01-07Coq: accelerate wp steps by improving application of existing specsBrian Campbell
2019-12-19Coq library improvementsBrian Campbell
- add liftRS support to tactics - define uint and sint in terms of functions without proof terms - eq_vec correctness - lemma that rounding up integers using reals is the obvious integer calculation - another proof irrelevance tactic - try lemmas in the sail hintdb both before and after goal processing
2019-12-09Coq: improve solver enough to handle arm specBrian Campbell
- break up goals more in unbool - remove intuition from guess_ex_solver because it can be too expensive - flip goals around because the side that evars appears on has changed - generalise the and/or tactics - make a couple of tactics more specific/robust
2019-12-06Don't introduce uneccesary control flow when compilingAlasdair Armstrong
2019-12-06Coq: use proof irrelevance for a few propertiesBrian Campbell
Includes removing an explicit use of a lemma generated by abstract, which was causing problems with different versions of Coq because the names change.
2019-12-05Coq: more solving support for boolean predicatesBrian Campbell
Mostly from making the aarch64 model compile again - switch order some arithmetic lemmas - move list membership rewrites alongside other comparisons to enable more rewriting - copy hypotheses used in other types/definitions so that they can be rewritten - lift boolean existentials out of implications in hypotheses so they can be used as witnesses without proving the condition - add negation to solve_bool_with_Z - add some new bool solving for goals from and_boolMP/or_boolMP
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
- ArithFact takes a boolean predicate - defined in terms of ArithFactP, which takes a Prop predicate, and is used directly for existentials - used abstract in more definitions with direct proofs - beef up solve_bool_with_Z to handle more equalities, andb and orb
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:28:49 +0000