| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-17 | Fix slicing in constant propagation | Brian Campbell | |
| 2018-04-17 | Move some Lem library vector operations so that we also have mword versions | Brian Campbell | |
| 2018-04-16 | Implement the s-mode views of mie/mip, and their legalizers. | Prashanth Mundkur | |
| 2018-04-16 | Add the satp legalizer. | Prashanth Mundkur | |
| 2018-04-13 | Add <=_u to riscv prelude. | Prashanth Mundkur | |
| 2018-04-13 | Add some checks of current state, and use for the xepc write legalizer. | Prashanth Mundkur | |
| 2018-04-13 | Some initial legalizers for writes to S-mode CSRs. | Prashanth Mundkur | |
| 2018-04-13 | Define legalizers for writes to M-mode CSRs, and hook these writes to use them. | Prashanth Mundkur | |
| 2018-04-13 | Move riscv memory definitions into a separate file. | Prashanth Mundkur | |
| 2018-04-13 | Fix access checks to riscv CSRs. | Prashanth Mundkur | |
| 2018-04-13 | Add a few more generated file to gitignore | Brian Campbell | |
| 2018-04-13 | Update aarch64 no vector monomorphisation source for current type checker | Brian Campbell | |
| 2018-04-13 | Check all patterns inside functions with -dsanity | Brian Campbell | |
| 2018-04-12 | Fill in some minor missing cases in monomorphisation | Brian Campbell | |
| 2018-04-12 | remove cheri128 backwards compatibility hack that extended ↵ | Robert Norton | |
| access_system_regs perm into bits 14-11 -- it looks like spec is heading that way. | |||
| 2018-04-12 | implement new permit_unseal used for CUnseal instead of permit_seal. | Robert Norton | |
| 2018-04-12 | add a cheri_trace target for conveniently building a debug build. | Robert Norton | |
| 2018-04-12 | Add implementations of CReadHwr and CWriteHwr | Robert Norton | |
| 2018-04-12 | Add missing read of UserLocal register using dmtc0 4, sel 2. Write was ↵ | Robert Norton | |
| present but read was missing except via rdhwr. | |||
| 2018-04-11 | Initial bits of supervisor state. | Prashanth Mundkur | |
| 2018-04-11 | Add some misc informational m-mode registers that are used in a test. | Prashanth Mundkur | |
| 2018-04-11 | More structured riscv trap vector handling. | Prashanth Mundkur | |
| 2018-04-11 | Fix test prelude | Brian Campbell | |
| 2018-04-11 | Avoid unnecessary rechecking in remove numeral pats rewrite | Brian Campbell | |
| (especially as the environment previously used was a bit dodgy) | |||
| 2018-04-11 | Use more robust method of finding deps of new tyvars in mono analysis | Brian Campbell | |
| 2018-04-11 | Make the atom to singleton type rewriter replace literals with guards | Brian Campbell | |
| (previously the typechecker did this for all literal patterns, but now it's only necessary for the rewritten arguments) | |||
| 2018-04-11 | Fix neq_range in flow.sail | Alasdair Armstrong | |
| 2018-04-10 | Porting some minisail changes to sail2 branch | Alasdair Armstrong | |
| This commit primarily changes how existential types are bound in letbindings. Essentially, the constraints on both numeric and existentially quantified types are lifted into the surrounding type context automatically, so in ``` val f : nat -> nat let x = f(3) ``` whereas x would have had type nat by default before, it'll now have type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh type variable). This has several advantages: x can be passed to functions expecting an atom argument, such as a vector indexing operation without any clunky cast functions - ex_int, ex_nat, and ex_range are no longer required. The let 'x = something() syntax is also less needed, and is now only really required when we specifically want a name to refer to x's type. This changes slightly the nature of the type pattern syntax---whereas previously it was used to cause an existential to be destructured, it now just provides names for an automatically destructured binding. Usually however, this just works the same. Also: - Fixed an issue where the rewrite_split_fun_constr_pats rewriting pass didn't add type paramemters for newly added type variables in generated function parameters. - Updated string_of_ functions in ast_util to reflect syntax changes - Fixed a C compilation issue where elements of union type constructors were not being coerced between big integers and 64-bit integers where appropriate - Type annotations in patterns now generalise, rather than restrict the type of the pattern. This should be safer and easier to handle in the various backends. I don't think any code we had was relying on this behaviour anyway. - Add inequality operator to lib/flow.sail - Fix an issue whereby top-level let bindings with annotations were checked incorrectly | |||
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |