aboutsummaryrefslogtreecommitdiff
path: root/model/prelude.sail
AgeCommit message (Collapse)AuthorFilesLines
2023-05-29apply_headers: regenerate copyright headersupdate-copyright-headersPhilipp Tomsich1-1/+3
2023-03-14Use not() instead of ~() for boolean negation (#210)Alexander Richardson1-0/+2
This may be more readable and also matches the sail-cheri-riscv model. For now this keeps ~ overloaded to accept bool, but in the future we may want to consider removing it (which is what I did to find all uses modified in this patch)
2022-01-21Add support for Scalar Cryptography Zbkb, Zbkc and Zbkx Extensions (#135)Bilal Sakhawat1-0/+9
2021-10-18scalar-crypto: Initial commit of 1.0.0-rc2 spec work. (#99)Ben Marshall1-0/+22
Merged scalar-crypto pull request #99 of 1.0.0-rc2 spec work from Ben Marshall. See https://github.com/riscv/sail-riscv/pull/99.
2021-07-29Use headache to apply copyright header at request of Peter Sewell.Robert Norton1-0/+68
2020-03-03Add bit negation to preludeThomas Bauereiss1-1/+5
For bounds calculation in sail-cheri-riscv.
2020-02-28Make types of min/max more preciseThomas Bauereiss1-8/+6
Might help typechecking sail-cheri-riscv code.
2019-08-19RISC-V spec, without implicit castsAlasdair Armstrong1-9/+10
2019-07-11Undo get_config workarounds.Prashanth Mundkur1-4/+10
2019-07-11Fix an issue where zeros function defined in sail conflicted with lem ↵Robert Norton1-24/+7
builtin (lem backend does not do z encoding) and add default get_config_print_xxx builtins mappings to lem build (now there is no longer a sail definition of the function because of -Oconstant_fold bug). Also remove FEATURE_IMPLICITS ifdef that was required for backwards compatibility with long obsolete sail versions.
2019-07-09Move the get_config_ print defaults to the backend preludes, since it seems ↵Prashanth Mundkur1-7/+0
to get optimized out by sail, making the emulator the command-line options ineffective.
2019-07-01Merge remote-tracking branch 'origin/master' into master-cleanupRobert Norton1-2/+2
2019-06-28Rename zeros and ones implicit functions to something that sail ↵Robert Norton1-7/+4
monomorphisation pass recognises. We don't need the overload.
2019-06-28add interpreter extern for string_of_intJon French1-1/+1
2019-06-28Avoid implicit casts to stringAlasdair1-1/+1
Can have unintended consequences, due to how overloading interacts with casts. For example, x : X == y : X can be interpreted as eq_string(cast(x), cast(y)) if x and y are both castable to string, even when there is an equality function (X, X) -> bool. Sail->SMT can't handle strings very well so it's best to just ensure that this can never occur. Rather than implicitly casting in logging statements like: print("xyz" ^ x ^ " foo " ^ y) it's now print("xyz" ^ to_str(x) ^ " foo " ^ to_str(y)) which ensures that the conversion to strings only happens where intended. I also added a warning to Sail itself to try to catch these cases in future.
2019-06-26Merge branch 'master-cleanup' into pmpPrashanth Mundkur1-11/+17
2019-06-26Add command line option in c_emulator for disabling tracing. Add builtins ↵Robert Norton1-0/+12
for getting values of config_print_xxx variables to speed up emulation when not tracing.
2019-06-20Add interpreter builtin for min_nat. Should min/max be in standard library?Robert Norton1-1/+1
2019-06-14Use sail's built-in ones functions for compatibility with smt backend.Robert Norton1-10/+4
2019-06-11Fill in a few missing Coq built-insBrian Campbell1-3/+3
2019-04-24Add extended model from cheri-merge.Prashanth Mundkur1-12/+34
2019-04-12Merge branch 'master' into rmem_interpreterrmem_interpreterJon French1-7/+7
2019-04-03Tweak print_* bindings for LemThomas Bauereiss1-4/+4
Map to a function that does not actuaylly output anything, in order to not confuse rmem.
2019-03-25Fix prelude for new names of div and mod functions.Robert Norton1-3/+3
2019-03-14Merge branch 'master' into rmem_interpreterJon French1-940/+39
2019-03-12refactor memory access to use new sail intrinsicsJon French1-39/+2
2019-03-12prelude.sail: fix print_foo externs in interpreterJon French1-4/+4
2019-03-08Another prelude cleanup.Prashanth Mundkur1-2/+0
2019-03-07Minor prelude cleanup.Prashanth Mundkur1-2/+0
2019-03-04Add defaults for platform values for use when interpretingJon French1-59/+60
2019-02-26Merge branch 'master' into rv32Prashanth Mundkur1-0/+8
2019-02-26Initial cleanup of the prelude, using standard prelude instead when possible.Prashanth Mundkur1-229/+33
2019-02-15More RV32 fixes.Prashanth Mundkur1-4/+0
2019-02-12Compatability fixes from Sail 0.7.1 to Sail 0.8Alasdair Armstrong1-0/+8
Two small compatability fixes: Small change to the prelude to make sure we are forwards compatable with the next release of Sail, which has slightly different syntax for implicit arguments. Due to changes in the monad embedding in the latest git version of Sail, we disable generating Lem by default when we detect we are on that version. It's a small one line fix to correct, but we want to keep the Lem definitions in this repository compatible with the opam release 0.7.1 for now.
2019-02-11More refactoring for RV32Prashanth Mundkur1-67/+0
- split out memory access definitions in prelude that depend on xlen - make riscv_xlen now part of the prelude set, so that riscv_duopod can use the definition - update xlen use in riscv_duopod so that it can now support rv32
2019-02-08Change implicits on monad branchAlasdair Armstrong1-4/+4
2019-02-08Adapt to changes in Sail's Lem shallow embeddingThomas Bauereiss1-5/+28
In the monads branch of Sail, writing a memory value now requires address and write_kind (instead of relying on parameters announced earlier).
2019-02-08Split out the mapping prelude into its own file.Prashanth Mundkur1-690/+0
2019-01-21Remove temporary workaround for Lem generationThomas Bauereiss1-4/+0
Reverts 7df2149
2019-01-21Clean up duopodAlasdair Armstrong1-14/+4
Remove functions in prelude that are duplicates from those in Sail library as this causes issues for the latex generation
2019-01-14Reorganize directory structure.Prashanth Mundkur1-0/+1161
generated by cgit v1.1 at 2024-11-16 22:51:37 +0000