| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 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 | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |