| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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. | |||
| 2017-02-03 | fix headers | Peter Sewell | |
| 2017-01-25 | merge cheri 256 and 128 together factoring out differing parts into separate ↵ | Robert Norton | |
| cheri_prelude files. | |||
| 2017-01-24 | first pass at cheri128 sail. | Robert Norton | |
| 2016-12-12 | cheri sail export progress | Christopher Pulte | |
| 2016-12-08 | add target for building cheri_notlb.lem | Robert Norton | |
| 2016-11-28 | make sail produce prompt and state version of shallow embedding files at the ↵ | Christopher Pulte | |
| same time with the types both have in common factored out into separate file, rename one mips shallow embedding _extras file as required by this | |||
| 2016-11-23 | Make type checker not run to fix point on resolving case-split type ↵ | Kathy Gray | |
| variables; modern implementation of nexp unification seems not to need it | |||
| 2016-11-22 | fix mips Makefile | Christopher Pulte | |
| 2016-11-14 | add option -lem_sequential for producing shallow embedding that refers to ↵ | Christopher Pulte | |
| state monad, library fixes | |||
| 2016-11-08 | fixes | Christopher Pulte | |
| 2016-11-07 | factor out regfp analysis types into etc/regfp.sail | Christopher Pulte | |
| 2016-11-03 | split out RI node so that ppcmem model does not implement reserved ↵ | Robert Norton | |
| instruction exception behaviour but sequential model does (for test suite). | |||
| 2016-10-20 | changes to support get_model for ppcmem. | Robert Norton | |
| 2016-09-23 | Add register footprint function needed by ppcmem (mips only for now) | Robert Norton | |
| 2016-06-03 | Change path inside sail Makefile to look for sail directory instead of l2 | Kathy Gray | |
| 2016-05-26 | add makery for mips/cheir LOC count. | Robert Norton | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |