| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
to code gen issue.
|
|
interpreter implementations of same.
|
|
Recent change made them proper matches rather than conditionals, and
Coq rejects incomplete matches.
(Will need a proper solution later...)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz.
|
|
to match new constraints in prelude
|
|
functions ready to go.
|
|
|
|
to correct place in main.sail. Remove add_atom and sub_atom from prelude as we get them from arith.sail.
|
|
ocaml main so that we can have simboot + kernel. Support UART output only.
|
|
Move mono_rewrites into lib
|
|
In order to use up-to-date sequential CHERI model for test suite
|
|
Found bugs by running CHERI test suite on Isabelle-exported model: signed
less-than for bit lists was missing negations for the two's complement, and
unsigned less-than compared the reverse lists.
Since all other backends implement this in Sail, it seems best to just remove
this code.
Also add support for infix operators to Lem backend, by z-encoding their
identifiers like the other backends do.
|
|
hack. Also some minor code cleanups and comments.
|
|
|
|
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
|
|
prelude).
|
|
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.
|
|
operator. Introduced by e33c8546.
|
|
|
|
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.
|
|
|
|
obviosu and to more closely match existing cheri pseudocode.
|
|
- 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
|
|
|
