summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-10Start adding c-backend bits for riscv.Prashanth Mundkur
2018-07-10Support riscv atomic accesses to mmio regions, used by linux to access ↵Prashanth Mundkur
device registers.
2018-07-10remove sim.dts when anonymising.Robert Norton
2018-07-10Make HOL build properly again for all of the modelsBrian Campbell
2018-07-10RISCV load-acquire in Lem (-> rmem)Jon French
2018-07-10fix constructor typoJon French
2018-07-10Only put static qualifier on valspecs when -static flag is usedAlasdair Armstrong
2018-07-10correct pretty-printing using mappingsJon French
2018-07-10disable printing when compiling to Lem to keep rmem happyJon French
2018-07-10Merge branch 'sail2' of github.com:rems-project/sail into sail2Robert Norton
2018-07-10remove obsolete files from language directory.Robert Norton
2018-07-10Update HOL setupBrian Campbell
2018-07-10Another AArch64 patchThomas Bauereiss
Makes CheckAndUpdateDescriptor respect endianness
2018-07-10Add more Isabelle lemmas to libraryThomas Bauereiss
2018-07-10Tweak to anonymous copyright header.Robert Norton
2018-07-10further anonymisation work.Robert Norton
2018-07-10Aarch64 mono script updateBrian Campbell
2018-07-09Initialize fresh memory to 0 in the OCaml backend.Prashanth Mundkur
This makes it consistent with the C backend, and also makes it easier to compare traces across execution re-runs.
2018-07-09Log some timing info at the end of riscv execution.Prashanth Mundkur
2018-07-09Lem: prefer type variables to constants when looking for equivalent nexpsBrian Campbell
If we have an nexp that we can't print, look for an equivalent type variable before looking for a constant - the constant may only be valid locally (e.g., under an if) while the type variable will be valid throughout the function. Fixes a problem with aget_Mem on aarch64.
2018-07-09Add no_devices.sail to be compatible with latest AArch64 prelude andAlasdair Armstrong
update aarch64 model
2018-07-09anonymise another github link.Robert Norton
2018-07-09anonymise github link in sail manual.Robert Norton
2018-07-09Remove awkward constraints on GetSlice_int for nowBrian Campbell
2018-07-09Changes for anonymisation. Ensure headers are in correct format. Remove some ↵Robert Norton
redundant files.
2018-07-09Tweak bit casting definitions in MIPS to avoid non-exhaustive patternsBrian Campbell
Recent change made them proper matches rather than conditionals, and Coq rejects incomplete matches. (Will need a proper solution later...)
2018-07-09Coq: remove some unnecessary castsBrian Campbell
2018-07-09Support building an anonymised version of manual. Fix sail example in ↵Robert Norton
manual. Remove incomplete types chapter from manual per AA's recommendation.
2018-07-09Update gitignoreThomas Bauereiss
2018-07-09Fix bug in rewriting of try-catch-blocks with variable updatesThomas Bauereiss
2018-07-09Tweak rewriting of literal patterns for LemThomas Bauereiss
2018-07-09Add explanatory comment to guard rewritingThomas Bauereiss
2018-07-09Update CHERI code generation from IsabelleThomas Bauereiss
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-09Patch some potential uses of uninitialised variables in AArch64Thomas 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-09add riscv_analysis.sail to SAIL_SRCSJon French
2018-07-09add LOADRES, STORECON, AMO to analysisJon French
2018-07-09Bits for bits of aarch64 in coqBrian Campbell
2018-07-09Support writes to misa.C in riscv.Prashanth Mundkur
2018-07-08Make the riscv fetch-execute loop return instead of exiting when done.Prashanth Mundkur
2018-07-08Move the riscv analysis function into its own file for coverage purposes.Prashanth Mundkur
2018-07-08Add a riscv coverage target using bisect-ppx.Prashanth Mundkur
2018-07-08Add -static flag that controls whether generated C functions are staticAlasdair
By default generated functions are non-static, using the -static flag makes them static which is useful for measuring coverage using generated code. Some utility helper functions will always be static, but the compiled versions of sail functions won't be unless this flag is set.
2018-07-07Add reservation traces to riscv tracecmp tool.Prashanth Mundkur
2018-07-07Cancel riscv reservation before i/o scheduling, tweak reservation tracing.Prashanth Mundkur
2018-07-07Add the lrsc tests from riscv-tests.Prashanth Mundkur
2018-07-07An initial fix to riscv lr/sc, needs a review.Prashanth Mundkur
This uses a stronger model than the version in Sail-1 in order to perform address alignment checks. The reservation is kept on virtual addresses, and maintained in the platform model, but now the lr/sc definitions need calls to externs to update this state. An alternative was to reserve physical addresses, but that appeared to be more complicated without a lot more changes. Ideally, the model should be parameterizable over both options.
2018-07-07Add some tracing to riscv address translation.Prashanth Mundkur
2018-07-07Coq: bbv have reorganised their repositoryBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 08:56:16 +0000