| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-10 | Avoid rejecting reasonable pattern matches in monomorphisation | Brian Campbell | |
| (when they're not relevant) | |||
| 2018-04-10 | Add basic reference support to monomorphisation | Brian Campbell | |
| 2018-04-09 | Update riscv to use the new system definitions, remove duplicates. | Prashanth Mundkur | |
| 2018-04-09 | Add some riscv arch definitions: privilege levels, exceptions, interrupts, ↵ | Prashanth Mundkur | |
| extension context, satp modes. | |||
| 2018-04-09 | Slightly re-org defs to move related things closer together. | Prashanth Mundkur | |
| 2018-04-09 | Better separate riscv-independent and riscv-specific parts between prelude ↵ | Prashanth Mundkur | |
| and riscv_types. Also remove an unused break(). | |||
| 2018-04-09 | Remove unnecessary restriction on complex nexp rewriting | Brian Campbell | |
| 2018-04-09 | Stop vector_typ_args_of from failing when order is a variable | Brian Campbell | |
| Now it just returns the actual arguments and a separate function calculates the start index when required. | |||
| 2018-04-09 | cheri: compute virtual address mod 2^64 when doing bounds check to avoid ↵ | Robert Norton | |
| failures with negative (i.e. large positive) offsets. | |||
| 2018-04-09 | remove unused functions from cher/mips prelude (step towards using standard ↵ | Robert Norton | |
| prelude). | |||
| 2018-04-06 | Fix some error msg typos. | Prashanth Mundkur | |
| 2018-04-06 | Fix emacs sail2-mode. | Prashanth Mundkur | |
| 2018-04-06 | Generate better tyvar names for complex nexps in monomorphisation | Brian Campbell | |
| 2018-04-06 | Test now passes | Brian Campbell | |
| 2018-04-06 | Add integer comparisons to overloads in flow typing library | Alasdair Armstrong | |
| 2018-04-06 | Update sail.tex for wip latex output | Alasdair Armstrong | |
| Fix a bug in initial check which caused X() = y to expect an additional parameter. Some tweaks to sail2 emacs mode | |||
| 2018-04-05 | Fix precedence printing and update aarch64 spec | Alasdair Armstrong | |
| More work on Latex output | |||
| 2018-04-05 | More work on latex output | Alasdair Armstrong | |
| Now generate commands for each toplevel definition, such that e.g. the function clause for execute LOAD could be inserted using \sailexecuteLOAD. Tries to generate fairly intuitive names while avoiding clashes where possible. | |||
| 2018-04-05 | Cleanup repository by removing old and generated files | Alasdair Armstrong | |
| Rename l2.ott to sail.ott | |||
| 2018-04-05 | Add generic prelude library that pulls in various basic sail | Alasdair Armstrong | |
| definitions from sail/lib. | |||
| 2018-04-04 | Fix another infinite loop in cast bit_to_bool. Following introduction of ↵ | Robert Norton | |
| eq_bool this was preferred over eq_bit when compiling the match on bit in bit_to_bool... Fix is to overload == before including flow.sail but feels a bit inelegant. | |||
| 2018-04-04 | Make Type_check.solve do obvious cases immediately | Brian Campbell | |
| 2018-04-04 | Use solver properly to simplify nexps in mono analysis, Lem printing | Brian Campbell | |
| Turn on complex nexp rewriting for mono by default (NB: solving is currently quite slow, will optimise) | |||
| 2018-04-04 | Instantiate type properly when introducing mono casts | Brian Campbell | |
| (also reorder the phases a little) | |||
| 2018-04-04 | Use valspec equations in monomorphisation analysis | Brian Campbell | |
| 2018-04-04 | Tweak Type_check.solve for this branch | Brian Campbell | |
| 2018-04-04 | Add a function to find unique solution for constraints | Alasdair Armstrong | |
| New function Type_check.solve : Env.t -> nexp -> Big_int.num option. Takes an environment and an n-expression (nexp), and returns either Some u, where u is a unique solution such that nexp = u, or None which indicates that either no unique solution could be found. It is technically possible that a unique solution could exist, but Z3 may not find it. Involves two calls to Z3, one of which cannot be memoised, so should be used carefully, as over-reliance could lead to performance issues. | |||
| 2018-04-04 | Add bitvector casts to funcl bodies when necessary | Brian Campbell | |
| 2018-04-04 | Initial rewrite to move complex nexps in fn sigs into constraints | Brian Campbell | |
| (for monomorphisation, off for now because the analysis needs extended). Also tighten up orig_nexp, make Lem backend replace # in type variables. | |||
| 2018-04-04 | Improve location information in mono dependency errors | Brian Campbell | |
| 2018-04-04 | Use simple equations in function specifications to instantiate tyvars | Brian Campbell | |
| Allows the type checker to deal with val foo : forall 'm 'n, 'n = 8 * 'm. atom('m) -> bits('n) for example | |||
| 2018-04-03 | Fix failing ARM test | Alasdair Armstrong | |
| 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 | Fix infinite loop in cheri/mips cast_unit_vec caused by lack of eq_bit in = ↵ | Robert Norton | |
| operator. Introduced by e33c8546. | |||
| 2018-03-27 | print IPS after running cheri model. | Robert Norton | |
| 2018-03-27 | remove some unneeded else clauses. | Robert Norton | |
| 2018-03-23 | Fix indentation of loops in generated Isabelle | Thomas Bauereiss | |
| 2018-03-23 | Fix build issue | Alasdair Armstrong | |
| 2018-03-22 | Fix cheri Makefile | Alasdair Armstrong | |
| 2018-03-22 | Fix C compilation for CHERI and MIPS | Alasdair Armstrong | |
| First, the specialisation of option types has been fixed by allowing the specialisation of constructor return types - this essentially means that a constructor, such as Some : 'a -> option('a) can get specialised to int -> option(int), rather than int -> option('a). This means that these constructors are treated like GADTs internally. Since this only happens just before the C translation, I haven't put much effort into making this very robust so far. Second, there was a bug in C compilation for the typing of return expressions in non-unit contexts, which has been fixed. Finally support for vector literals that are non-bitvectors has been added. | |||
| 2018-03-22 | Try removing superfluous returns more aggressively for Lem | Thomas Bauereiss | |
| 2018-03-22 | Tune Lem pretty-printing | Thomas Bauereiss | |
| In particular, improve indentation of if-expressions, and provide infix syntax for monadic binds in Isabelle, allowing Lem to preserve source whitespace. | |||
| 2018-03-21 | Patch AST datatypes in generated Isabelle theories | Thomas Bauereiss | |
| Deactivate plugins of the datatype package except for the size plugin in order to keep processing time reasonable. This is currently only needed for the big AST datatypes, so we just patch this using a sed command. | |||
| 2018-03-21 | Fix Lem generation for MIPS | Thomas Bauereiss | |
| 2018-03-19 | Fixes to C backend for RISCV-compilation | Alasdair Armstrong | |
| Can now compile RISCV. Requires some library tweaks before it'll pass any tests, Also adds hyperlinks to wip latex output | |||
| 2018-03-15 | Sail now exits with code 1 when OCaml fails to compile generated code | Alasdair Armstrong | |
| Fixes #11 | |||
| 2018-03-15 | add test that cheri specs build (ocaml). | Robert Norton | |
| 2018-03-15 | Some CHERI compilation fixes | Thomas Bauereiss | |
| 2018-03-14 | WIP Latex formatting | Alasdair Armstrong | |
| Added option -latex that outputs input to a latex document. Added doc comments that can be attached to certain AST nodes - right now just valspecs and function clauses, e.g. /*! Documentation for main */ val main : unit -> unit These comments are kept by the sail pretty printer, and used when generating latex | |||
| 2018-03-14 | Add and use execute_branch and execute_branch_pcc functions to align code ↵ | Robert Norton | |
| with existing MIPS and CHERI specs. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |