| Age | Commit message (Collapse) | Author |
|---|
|
|
|
It now includes updating the effects so that morally pure recursive
functions can be turned into this impure termination-by-assertion form.
|
|
|
|
This only applies to recursive functions and uses the termination measure
merely as a limit to the recursive call depth, rather than proving the
measure correct.
|
|
|
|
* Improve type inference for numeric if statements (if_infer test)
* Correctly handle constraints for existentially quantified constructors (constraint_ctor test)
* Canonicalise all numeric types in function arguments, which
triggers some weird edge cases between parametric polymorphism and
subtyping of numeric arguments
* Because of this eq_int, eq_range, and eq_atom etc become identical
* Avoid duplicating destruct_exist in Env
* Handle some odd subtyping cases better
|
|
- Completely remove the nexp = nexp syntax in favour of nexp ==
nexp. All our existing specs have already switched over. As part of
this fix every test that used the old syntax, and update the
generated aarch64 specs
- Remove the `type when constraint` syntax. It just makes changing the
parser in any way really awkward.
- Change the syntax for declaring new types with multiple type
parameters from:
type foo('a : Type) ('n : Int), constraint = ...
to
type foo('a: Type, 'n: Int), constraint = ...
This makes type declarations mimic function declarations, and makes
the syntax for declaring types match the syntax for using types, as
foo is used as foo(type, nexp). None of our specifications use types
with multiple type parameters so this change doesn't actually break
anything, other than some tests. The brackets around the type
parameters are now mandatory.
- Experiment with splitting Type/Order type parameters from Int type
parameters in the parser.
Currently in a type bar(x, y, z) all of x, y, and z could be either
numeric expressions, orders, or types. This means that in the parser
we are severely restricted in what we can parse in numeric
expressions because everything has to be parseable as a type (atyp)
- it also means we can't introduce boolean type
variables/expressions or other minisail features (like removing
ticks from type variables!) because we are heavily constrained by
what we can parse unambigiously due to how these different type
parameters can be mixed and interleaved.
There is now experimental syntax: vector::<'o, 'a>('n) <-->
vector('n, 'o, 'a) which splits the type argument list into two
between Type/Order-polymorphic arguments and Int-polymorphic
arguments. The exact choice of delimiters isn't set in stone - ::<
and > match generics in Rust. The obvious choices of < and > / [ and
] are ambigious in various ways.
Using this syntax right now triggers a warning.
- Fix undefined behaviour in C compilation when concatenating a
0-length vector with a 64-length vector.
|
|
- Fix pretty printing nested constraints
- Add flow typing for if condition then { throw exn }; ... blocks
- Add optimisations for bitvector concatenation in C
|
|
Should hopefully fix memory leak in RISC-V.
Also adds an optimization pass that removes copying structs and allows
some structs to simply alias each other and avoid copying their
contents. This requires knowing certain things about the lifetimes of
the structs involved, as can't free the struct if another variable is
referencing it - therefore we conservatively only apply this
optimization for variables that are lifted outside function
definitions, and should therefore never get freed until the model
exits - however this may cause issues outside ARMv8, as there may be
cases where a struct can exist within a variant type (which are not
yet subject to this lifting optimisation), that would break these
assumptions - therefore this optimisation is only enabled with the
-Oexperimental flag.
|
|
Bitvectors that aren't fixed size, but can still be shown to fit
within 64-bits, now have a specialised representation. Still need to
introduce more optimized functions, as right now we mostly have to
convert them into large bitvectors to pass them into most
functions. Nevertheless, this doubles the performance of the TLBLookup
function in ARMv8.
|
|
- Propagate types more accurately to improve optimization on ANF
representation.
- Add a generic optimization pass to remove redundant variables that
simply alias other variables.
- Modify Sail interactive mode, so it can compile a specification with
the :compile command, view generated intermediate representation via
the :ir <function> command, and step-through the IR with :exec <exp>
(although this is very incomplete)
- Introduce a third bitvector representation, between fast
fixed-precision bitvectors, and variable length large
bitvectors. The bitvector types are now from most efficient to least
* CT_fbits for fixed precision, 64-bit or less bitvectors
* CT_sbits for 64-bit or less, variable length bitvectors
* CT_lbits for arbitrary variable length bitvectors
- Support for generating C code using CT_sbits is currently
incomplete, it just exists in the intermediate representation right
now.
- Include ctyp in AV_C_fragment, so we don't have to recompute it
|
|
|
|
|
|
|
|
Also fix a test with an insufficient constraint
|
|
|
|
|
|
|
|
|
|
Also add a special case for shift-left when we are shifting 8 by a two
bit opcode, or 32 by a one bit opcode.
|
|
The main changes so far are:
* Allow markdown formatting in doc comments. We parse the markdown
using Omd, which is a OCaml library for parsing markdown. The nice
thing about this library is it's pure OCaml and has no dependencies
other the the stdlib. Incidentally it was also developed at OCaml
labs. Using markdown keeps our doc-comments from becoming latex
specfic, and having an actual parser is _much_ nicer than trying to
hackily process latex in doc-comments using OCamls somewhat sub-par
regex support.
* More sane conversion latex identifiers the main approach is to
convert Sail identifiers to lowerCamelCase, replacing numbers with
words, and then add a 'category' code based on the type of
identifier, so for a function we'd have fnlowerCamelCase and for
type synonym typelowerCamelCase etc. Because this transformation is
non-injective we keep track of identifiers we've generated so we end
up with identifierA, identifierB, identifierC when there are
collisions.
* Because we parse markdown in doc comments doc comments can use Sail
identifiers directly in hyperlinks, without having to care about how
they are name-mangled down into TeX compatible things.
* Allow directives to be passed through the compiler to
backends. There are various $latex directives that modify the latex
output. Most usefully there's a
$latex newcommand name markdown
directive that uses the markdown parser to generate latex
commands. An example of why this is useful is bellow. We can also use
$latex noref id
To suppress automatically inserting links to an identifier
* Refactor the latex generator to make the overall generation process
cleaner
* Work around the fact that some operating systems consider
case-sensitive file names to be a good thing
* Fix a bug where latex generation wouldn't occur unless the directory
specified by -o didn't exist
This isn't quite all the requested features for good CHERI
documentation, but new features should be much easier to add now.
|
|
* Previously we allowed the following bizarre syntax for a forall
quantifier on a function:
val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit
this commit changes this to the more sane:
val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit
Having talked about it today, we could consider adding the syntax
val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit
which would avoid the forall (by implicitly quantifying variables in
the constraint), and be slightly more friendly especially for
documentation purposes. Only RISC-V used this syntax, so all uses of
it there have been switched to the new style.
* Second, there is a new (somewhat experimental) syntax for
existentials, that is hopefully more readable and closer to
minisail:
val foo(x: int, y: int) -> int('m) with 'm >= 2
"type('n) with constraint" is equivalent to minisail: {'n: type | constraint}
the type variables in typ are implicitly quantified, so this is equivalent to
{'n, constraint. typ('n)}
In order to make this syntax non-ambiguous we have to use == in
constraints rather than =, but this is a good thing anyway because
the previous situation where = was type level equality and == term
level equality was confusing. Now all the type type-level and
term-level operators can be consistent. However, to avoid breaking
anything = is still allowed in non-with constraints, and produces a
deprecated warning when parsed.
|
|
* Previously we allowed the following bizarre syntax for a forall
quantifier on a function:
val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit
this commit changes this to the more sane:
val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit
Having talked about it today, we could consider adding the syntax
val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit
which would avoid the forall (by implicitly quantifying variables in
the constraint), and be slightly more friendly especially for
documentation purposes. Only RISC-V used this syntax, so all uses of
it there have been switched to the new style.
* Second, there is a new (somewhat experimental) syntax for
existentials, that is hopefully more readable and closer to
minisail:
val foo(x: int, y: int) -> int('m) with 'm >= 2
"type('n) with constraint" is equivalent to minisail: {'n: type | constraint}
the type variables in typ are implicitly quantified, so this is equivalent to
{'n, constraint. typ('n)}
In order to make this syntax non-ambiguous we have to use == in
constraints rather than =, but this is a good thing anyway because
the previous situation where = was type level equality and == term
level equality was confusing. Now all the type type-level and
term-level operators can be consistent. However, to avoid breaking
anything = is still allowed in non-with constraints, and produces a
deprecated warning when parsed.
|
|
|
|
|
|
|
|
Uses new primop 'string_take' which is much easier to implement in e.g. C
|
|
When converting to A-normal form I just used the type of the then
branch of if statements to get the type of the whole if statement -
usually they'd be the same, but with flow typing one of the branches
can have a false constraint, which then allows the optimizer to fit
any integer into a 64-bit integer causing an overflow. The fix is to
correctly use the type the typechecker gives for the whole if
statement.
Also add decimal_string_of_bits to the C output.
Rename is_reftyp to is_ref_typ to be more consistent with other
is_X_typ functions in Ast_util.
|
|
- more hex_bits functions, add decimal_string_of_bits
- extra tuple unfolding in constructors
- note that variables can be redundant wildcard clauses
- update RISC-V patch
|
|
- implement set_slice and set_slice_int
- lemmas for more constraints
- make real sqrt visible
- unfolding list membership needs andb and orb to be handled first
|
|
- hints for dotp
- handle exists separately when trying eauto to keep search depth low
- more uniform existential handling (i.e., we now handle all existentials
in the way we used to only handle existentials around atoms)
|
|
|
|
|
|
|
|
The omega tactic doesn't like them
|
|
|
|
C: Don't print usage message and quit when called with no arguments,
as this is used for testing C output
OCaml: Fix generation of datatypes with multiple type arguments
OCaml: Generate P_cons pattern correctly
C: Fix constant propagation to not propagate letbindings with type
annotations. This behaviour could cause type errors due to how type
variables are introduced. Now we only propagate letbindings when the
type of the propagated variable is guaranteed to be the same as the
inferred type of the binding.
Tests: Add OCaml tests to the C end-to-end tests (which really
shouldn't be in test/c/ any more, something like test/compile might be
better). Currently some issues with reals there like interpreter.
Tests: Rename list.sail -> list_test.sail because ocaml doesn't want
to compile files called list.ml.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Revert a change to string_of_bits because it broke all the RISC-V
tests in OCaml. string_of_int (int_of_string x) is not valid because x may not
fit within an integer.
|
|
otherwise some other parts don't work properly.
Also update RISC-V patch.
|
|
Also required some solver fixes:
- make sure that ArithFacts are always cleared to avoid loops
- extract_properties should do the goal first because it might add extra
work to do in the hypotheses
- unfolding should come before extract_properties
|
|
constructed when a function call, cast, or binder demands them, removing
some ambiguous corner cases.
Also
- Don't simplify nexps before printing (note that we usually end up
needing a (8 * x) / 8 lemma as a result)
- More extraction of properties in the goal
- Splitting of conditionals/matches in goals (which can occur more often
because of the new positions of build_ex in definitions)
- Try simple solving first to improve speed / reduce proof sizes / help
fill in metavariables (because manipulating the goal can interfere with
instantiating them)
- Update RISC-V patch
|
|
Add some builtins to the C sail lib.
Enable some gcc warnings.
|
|
typing
Added a regression test as c/test/downcast_fn.sail
|
