| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-08 | Correct dependencies of bytecode sail | Brian Campbell | |
| 2018-04-26 | Add a new SHARE_DIR argument to use when doing opam build. For non-opam ↵ | Robert Norton | |
| builds this defaults to git root. | |||
| 2018-04-26 | Opam packaging: add install and uninstall targets and code to find various ↵ | Robert Norton | |
| files in installed location. | |||
| 2018-04-26 | Remove obsolete mips/cheri rules from sail makefile. These are now built in ↵ | Robert Norton | |
| their respective subdirectories. | |||
| 2018-04-18 | Fix build on linux | Alasdair Armstrong | |
| Turns out that BSD sed is not a subset of GNU sed, GNU sed doesn't allow a space after the -i option. | |||
| 2018-04-18 | Port to Mac: BSD sed != GNU sed | Alastair Reid | |
| For GNU sed, the extension is optional in sed -i ... But in BSD sed, the extension is mandatory sed -i .bak ... | |||
| 2018-04-05 | Cleanup repository by removing old and generated files | Alasdair Armstrong | |
| Rename l2.ott to sail.ott | |||
| 2018-03-08 | rename mips_new_tc to mips | Robert Norton | |
| 2018-03-02 | Use sail_lib.lem values in C backend | Alasdair Armstrong | |
| Rather than just using strings to represent literals, now use value types from sail_lib.lem to represent them. This allows for expressions to be evaluated at compile time, which will be useful for future optimisations involving constant folding and propagation, and allows the intermediate bytecode to be interpreted using the same lem builtins that the shallow embedding uses. To get this to work I had to tweak the build process slightly to allow ml files to import lem files from gen_lib/. Hopefully this doesn't break anything! | |||
| 2018-02-22 | wip | Robert Norton | |
| 2018-02-17 | Merge master branch into sail2 for OCaml 4.06 compatibility | Thomas Bauereiss | |
| 2018-02-09 | Formalize C backend intermediate representation in Ott | Alasdair Armstrong | |
| Describes precisely the intermediate representation used in the C backend in an ott grammar, and also removes several C-isms where raw C code was inserted into the IR, so in theory this IR could be interpreted by a small VM/interpreter or compiled to LLVM bytecode etc. Currently the I_raw constructor for inserting C code is just used for inserting GCC attributes, so it can safely be ignored. Also augment and refactor the instruction type with an aux constructor so location information can be propagated down to this level. | |||
| 2018-02-08 | work in progress mips sail2 port. | Robert Norton | |
| 2018-01-31 | minor rename | Shaked Flur | |
| 2018-01-26 | Missing -ocamlfind | Brian Campbell | |
| 2018-01-25 | Fix building bytecode sail | Brian Campbell | |
| 2018-01-23 | Started working on C backend for sail | Alasdair Armstrong | |
| Also updated some of the documentation in the sail source code | |||
| 2017-12-30 | use linksem as a package | Shaked Flur | |
| 2017-12-28 | use ocamlfind to locate lem and zarith | Shaked Flur | |
| 2017-12-13 | Cleanup code by fixing compiler warnings, and fix ocaml compilation | Alasdair Armstrong | |
| Add the ast.sed script we need to build sail. Currently we just need this to fix up the locations in the AST but it will be removed once we can share locations between ocaml and lem. | |||
| 2017-12-13 | Merge remote-tracking branch 'origin/master' into interactive | Alasdair Armstrong | |
| 2017-12-13 | Use big_nums from Lem | Alasdair Armstrong | |
| 2017-12-13 | find zarith using ocamlfind instead of using the one in ocaml-lib which is ↵ | Shaked Flur | |
| no longer there | |||
| 2017-12-11 | Prototype interactive mode for sail. | Alasdair Armstrong | |
| Requires linenoise library (opam install linenoise) for readline support. Use 'make isail' to build sail with interactive support. Plain 'make sail' should work as before with no additional dependencies. Use 'sail -i <commands>' to run sail interactively, e.g. sail -new_parser -i test/ocaml/prelude.sail test/ocaml/trycatch/tc.sail then try some commands for typechecking and evaluation sail> :t main sail> main () Doesn't use the lem interpreter right now, instead has a small operational semantics in src/interpreter.ml, but this is not very complete and will be changed/removed. | |||
| 2017-12-05 | Update header files on master | Alasdair Armstrong | |
| 2017-12-05 | Update license headers for Sail source | Alasdair Armstrong | |
| 2017-11-29 | Switched to bytecode compiler for executing interpreter to avoid stack overflow | Alasdair Armstrong | |
| 2017-11-17 | Fix Makefile for interpreter and update instruction_extractor | Alasdair Armstrong | |
| Instruction extractor code that I commented out in this commit seems buggy anyway - it will claim that the length of all bitvectors is 64?! | |||
| 2017-11-17 | Fix interpreter to work with new typechecker | Alasdair Armstrong | |
| Need to map sail type annotations to interpreter type annotations in lem_ast ouput. This doesn't seem too hard. | |||
| 2017-10-25 | Point sail/src makefile at ott file in language/ | Alasdair Armstrong | |
| 2017-10-25 | Generate ast.ml from ott file and update makefile. | Alasdair Armstrong | |
| Fix until loop not being counted as sugar | |||
| 2017-09-29 | Add MIPS->Isabelle target to Makefile | Thomas Bauereiss | |
| 2017-09-14 | Fix a regression when writing to a register via a reference in a vector such ↵ | Thomas Bauereiss | |
| as GPR This was wrongly translated as an update of the vector of references. | |||
| 2017-09-02 | Add command line flags to toggle sequential monad and native machine words | Thomas Bauereiss | |
| 2017-08-29 | Make Lem export of CHERI(-256) typecheck | Thomas Bauereiss | |
| Note: The effect annotations of the execute function differ between CHERI and MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the initial declarations of ast, decode, and execute (with the right effects for MIPS). | |||
| 2017-08-24 | Use relative path in Makefile | Thomas Bauereiss | |
| 2017-08-24 | Fix some bugs related to the CHERI spec | Thomas Bauereiss | |
| - Correctly pass exponentials to Z3 - Infer types of functional record updates - Support "def Nat" | |||
| 2017-07-21 | Everything moved to new typechecker | Alasdair Armstrong | |
| Modified initial_check.ml so it no longer requires type_internal. It's still needs cleaned up in a few ways. Most of the things it's trying to do could be done nicer if we took some time to re-factor it, and some of the things should just be handled by the main typechecker, leaving it as a think layer between the parse_ast and the ast. Now that's done everything can be switched to the new typechecker and the _new suffixes were deleted from everything except the monomorphisation pass because I don't know the status of that. | |||
| 2017-06-29 | Ocamlbuild targets should always be remade | Brian Campbell | |
| 2017-05-10 | Build Cheri_embed_types.thy together with Cheri_embed_sequential.thy | Thomas Bauereiss | |
| 2017-05-08 | add make rules to (attempt to) build arm and power ml. | Robert Norton | |
| 2017-04-25 | Add support for uart terminal. Also add read_bit_reg function for faster and ↵ | Robert Norton | |
| neater access to registers of single bit. | |||
| 2017-04-21 | it turns out zarith has a function for printing big_ints in hex. Remove the ↵ | Robert Norton | |
| dependency on ocaml uint library by using it. | |||
| 2017-04-21 | add make variable for setting ocaml compilation options (e.g. set to -p to ↵ | Robert Norton | |
| enable gprof profiling) | |||
| 2017-04-20 | remove unnecessary lemlib include in compile. | Robert Norton | |
| 2017-04-20 | add support for cheri128 ocaml shallow embedding | Robert Norton | |
| 2017-04-20 | build a single run_embed.native with mips and cheri models linked and choose ↵ | Robert Norton | |
| between them using a command line switch. | |||
| 2017-04-06 | add support for address translation and exit handling in mips ocaml shallow ↵ | Robert Norton | |
| embedding test setup. | |||
| 2017-03-24 | Checkpoint work-in-progress mips sequential interpreter using ocaml shallow ↵ | Robert Norton | |
| embedding. | |||
| 2017-02-03 | replace bit vector return types in getCapX functions with equivalent integer ↵ | Robert Norton | |
| range types. This removes quite a few uses of unsigned() in cheri intsruction pseudocode. Could potentially take things furter. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |