aboutsummaryrefslogtreecommitdiff
path: root/model/prelude.sail
AgeCommit message (Collapse)AuthorFilesLines
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