| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-22 | add support for new cycle_limit feature in mips. | Robert Norton | |
| 2018-06-21 | Merge branch 'tracing' into sail2 | Alasdair Armstrong | |
| 2018-06-14 | provide impl of int_of_string_opt in Sail_lib to support older Ocaml versions | Jon French | |
| 2018-06-13 | Tracing instrumentation for C backend | Alasdair Armstrong | |
| 2018-06-11 | add 'pat as id' mapping-patterns | Jon French | |
| 2018-06-11 | Merge branch 'sail2' into mappings | Jon French | |
| (involved some manual tinkering with gitignore, type_check, riscv) | |||
| 2018-06-04 | switch to using a Map data structure for cheri tags in ocaml backend. This ↵ | Robert Norton | |
| solves a problem where the Hashtbl module was encountering a stack overflow booting CheriBSD. There seems to be little or no performance impact. | |||
| 2018-06-04 | Use Util.split_on_char in sail_lib.ml | Alasdair Armstrong | |
| 2018-05-31 | Fix for Jenkins build | Alasdair Armstrong | |
| Looks like Jenkins is still on OCaml 4.02.3. We should probably upgrade to 4.05 at some point. | |||
| 2018-05-31 | Fixes to get ARM u-boot working in Sail. | Alasdair Armstrong | |
| Also fixes to C backend for compiling MIPS spec to C - Fix an issue with const correctness in internal_vector_update functions generated by C backend - Add builtins for MIPS to sail.h - Fix an issue where reg_deref didn't work when called on pointers to large bitvectors, i.e. vectors containing references to large bitfields as in the MIPS TLB code - Various bug fixes and changes for running U-boot on ARM model, including for interpreter and OCaml compilation. - Fix memory leak issues and incorrect shadowing for foreach loops - Update C header file. Fixes memory leak in memory read/write builtins. - Add aux constructor to ANF representation to hold environment information. - Fix undefined behavior caused by optimisation left shifting uint64_t vectors 64 or more times. Unfortunately there's more issues because the same happens for X >> 64 right shifts. It would make sense for this to be zero, because that would guarantee the property that ((X >> n) >> m) == (X >> (n + m)) but we probably need to do (X >> (n - 1) >> 1) in the optimisation to ensure that we don't cause UB. Shifting by 63 and then by 1 is well-defined, but shifting by 64 in one go isn't according to the C standard. This issue with right-shifts only occurs for zero-length vectors, so it's not a huge deal, but it's still annoying. - Add versions of print_bits and print_int that print to stderr. Follows OCaml convention of print/prerr. Should make things more explicit. Different backends had different ideas about where print should output to, not every backend needs to have this (e.g. theorem prover backends don't need to print) but having both stderr and stdout seperate and clear is useful for executable models (UART needs to be stdout, debug messages should be stderr). | |||
| 2018-05-31 | Some tweaks to ocaml compilation and sail_lib for ARM with system registers | Alasdair Armstrong | |
| 2018-05-25 | Use paged memory storage for ocaml backend memory. This is slightly slower ↵ | Robert Norton | |
| (<5% on a simple test) but dramatically reduces memory usage compared to having a hash table entry per byte! | |||
| 2018-05-23 | riscv decode now uses mapping-decode and passes tests | Jon French | |
| 2018-05-21 | further RISCV mapping: all extant non-compressed instructions done | Jon French | |
| 2018-05-18 | more riscv mappings; riscv now builds successfully to lem which builds to ↵ | Jon French | |
| isabelle (but isabelle almost certainly broken) | |||
| 2018-05-17 | changes to for testing FreeBSD boot on MIPS: allowing loading raw file in ↵ | Robert Norton | |
| ocaml main so that we can have simboot + kernel. Support UART output only. | |||
| 2018-05-11 | further riscv mapping | Jon French | |
| 2018-05-10 | more mapping | Jon French | |
| 2018-05-10 | hacky monomorphic bits-string-parser for now | Jon French | |
| 2018-05-10 | add space handling mappings to riscv prelude and sail_lib.ml | Jon French | |
| 2018-05-03 | support sub-mappings in string-append-patterns | Jon French | |
| 2018-05-02 | refactor string append pattern ast to be based on lists rather than pairs | Jon French | |
| 2018-05-01 | it works | Jon French | |
| 2018-05-01 | rewriting of builtin mappings e.g. int | Jon French | |
| 2018-05-01 | further progress but confounds the type checker? | Jon French | |
| 2018-05-01 | progress on debugging string pattern matching | Jon French | |
| 2018-05-01 | starting to also do integer support | Jon French | |
| 2018-05-01 | start of string pattern matching: currently only literals | Jon French | |
| 2018-04-03 | Added test cases for builtins | Alasdair Armstrong | |
| Added library for simple integer arithmetic functions in lib/arith.sail WIP TeX file for formatting latex output included in lib/sail.tex Fixes for bugs in sail_lib | |||
| 2018-03-27 | print IPS after running cheri model. | Robert Norton | |
| 2018-03-15 | Some CHERI compilation fixes | Thomas Bauereiss | |
| 2018-03-14 | Fix Lem generation for CHERI-MIPS and Aarch64 | Thomas Bauereiss | |
| - Update Lem bindings and extras files - Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's (used for cap_size in the CHERI spec) - Add Lem and Isabelle Makefile targets for CHERI | |||
| 2018-03-14 | fix riscv build: missing eq_bit implementation. | Robert Norton | |
| 2018-03-12 | ELF loading for C backend | Alasdair Armstrong | |
| Add a flag to Sail that allows for an image of an elf file to be dumped in a simple format using linksem, used as sail -elf test.elf -o test.bin This image file can then be used by a compiled C version of a sail spec as with ocaml simply by ./a.out test.bin | |||
| 2018-03-06 | finish port of cheri128 spec. to sail2. | Robert Norton | |
| 2018-03-01 | Add support for read_tag and write_tag in sail_lib.ml. and support for ↵ | Robert Norton | |
| intialising and dumping CHERI state. Somewhat working cheri sail2 model. | |||
| 2018-02-27 | Get MIPS translated to Lem | Thomas Bauereiss | |
| 2018-02-23 | Fix some bugs in C compilation | Alasdair Armstrong | |
| Fixed an issue with pattern matching on enums Fixed an issue whereby fix_early_returns would cause memory leaks Added optimizations for some of the builtins used in the decode function. Optimizations are turned on with the -O flag. | |||
| 2018-02-23 | Some tidy up of sail library - use extract_num from Big_int to implement ↵ | Robert Norton | |
| to_get_slice_int in less confusing way. Add arithmetic shift right. | |||
| 2018-02-15 | Update duopod spec so it has no address translation | Alasdair Armstrong | |
| Also update the main aarch64 (no_vector) spec with latest asl_parser | |||
| 2018-02-13 | Support for large bitvector literals in C backend | Alasdair Armstrong | |
| 2018-02-06 | fix backwards arguments to pow2. | Robert Norton | |
| 2018-02-02 | Add M extension to RISCV. Slightly inelegant implementation for now but ↵ | Robert Norton | |
| passing tests. | |||
| 2018-01-29 | Add some initial exception handling to the riscv execution loop. | Prashanth Mundkur | |
| 2018-01-29 | implement shift primitives in sail_lib.ml | Robert Norton | |
| 2018-01-24 | Fixed riscv ocaml compilation | Alasdair Armstrong | |
| 2018-01-22 | Added rewriter that specializes all function calls in a specification. | Alasdair Armstrong | |
| This removes all type polymorphism, so we can generate optimized bitvector code and compile to languages without parametric polymorphism. | |||
| 2018-01-22 | Update and fix test suite | Alasdair Armstrong | |
| 2018-01-18 | Modified ocaml backend to use ocamlfind for linksem and lem | Alasdair Armstrong | |
| Fixed test cases for ocaml backend and interpreter | |||
| 2018-01-12 | OCaml interactive mode can now run full aarch64 examples, and ocaml test cases. | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |