| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
sloccount or cloc. sloccount seems to be reliable but lacks a way to tell it that sail files can be treated like ocaml without renaming the files. cloc has a nicer interface is lower quality in other regards like broken ocaml support in versions shipped with Ubuntu (e.g. treats {...} as comment, no nested comments support). For sail2 syntax this is OK because we use the C parser instead which gives the same results as sloccount.
|
|
|
|
The datatype package of HOL4 does not support the prompt monad, so this patch
restores the option to generate a model that only uses the state monad. Also
add a Makefile target cheri_sequential.lem in the cheri/ directory.
|
|
|
|
They are used in various specs and test cases.
|
|
|
|
present but read was missing except via rdhwr.
|
|
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.
|
|
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.
|
|
|
|
with existing MIPS and CHERI specs.
|
|
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
|
|
The state monad currently assumes that tags are written to and read from
properly aligned addresses (since it does not know the capability size used in
the Sail model). This change allows the Sail model to pass in the aligned
address(es) even if data is written to an unaligned address. There might be
better ways to model tag writing, but this approach seems rather general.
|
|
|
|
Hopefully thiis will help git to spot the rename and hence preserve history.
|
|
intialising and dumping CHERI state. Somewhat working cheri sail2 model.
|
|
|
|
removed IK_cond_branch, and added IK_branch
|
|
|
|
|
|
|
|
|
|
delay slot of a ccall selector 1 call.
|
|
registers is no longer xored with 48 so need to initialise it. Also use E and T values used by CHERI hw and adjust decoding functions appropriately. Fix shift functions for ocaml shallow embedding which failed to handle shifts greater than vector length.
|
|
generation for dubious casting enumeration to int.
|
|
# Conflicts:
# src/type_internal.ml
|
|
|
|
|
|
|
|
- Add case distinctions between bitvector types and vectors of other element
types (e.g. registers) and use the corresponding operations (i.e. "bvslice",
"bvaccess", etc for the former, and "slice", "access", etc for the latter) when
pretty-printing expressions
- Add type annotations to expressions when the type includes bitvectors with
concretely known length
- Update state.lem to use bitvectors (in the interface, at least; internally,
bitvectors are still stored as bit lists for now, since that makes it easier
to support storing different registers with different lengths)
This has been tested with the CHERI-MIPS model with some success, but some
things are still missing:
- Bitvector patterns are not handled yet
- Some bitvector length monomorphisation is needed in a few places of the model
- Some type annotations are missing, because the (old) Sail type checker does
not infer bitvector lengths in some instances where one would hope it to do
that; this should be checked with the new type checker
|
|
|
|
|
|
data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
|
|
Tagged memory seems to be currently missing in the Lem shallow embedding of
(CHERI-)MIPS.
|
|
|
