| Age | Commit message (Collapse) | Author |
|---|
|
actually take a tuple argument
|
|
Changes the representation of function types in the ast from
Typ_fn : typ -> typ
to
Typ_fn : typ list -> typ
to more accurately represent their use in the various backends, where we often compile functions to either their curried representations as in Lem and Isabelle, or just
multiple argument functions in C. There's still some oddity because a single pattern in a function clause can bind against multiple arguments, and maybe we want to
forbid this in the future. The syntax also hasn't changed (yet), so in theory this change shouldn't break anything (but it invariably will...).
In the future we would ideally require that a function with N arguments has exactly N patterns in its declaration, one for each argument so
f : (x, y) -> z
f _ = ...
would be disallowed (as _ matches both x and y), forcing
f(_, _) = z
this would simply quite a few things,
Also we could have a different syntax for function argument lists and tuples, because it's rather hard to define a function that actually takes a tuple with the syntax
how it is now.
Some issues I noticed when doing this refactoring:
Line 1926 of Coq translation. untuple_args_pat is maybe no longer needed? However there's still some funnyness where a pattern can be used to bind multiple function
arguments so maybe it still is.
Line 2306 of monomorphisation. I simplified the logic here. I think it's equivalent now, but I could be wrong.
Line 4517 of rewrites. I'm not sure what make_cstr_mappings is doing here, but hopefully the simpler version is the same.
|
|
Now that Jenkins is updated to a newer version of OCaml we can finally
fix some warning with more recent versions of OCaml than 4.02.3. Also
fix a Lem test case that was failing.
|
|
|
|
|
|
|
|
Test the builtin functions by compiling them to C, OCaml, and OCaml
via Lem. Split up some of the longer builtin test programs to avoid
stack overflows when compiling to OCaml, as 3000+ line long blocks can
cause issues with some re-writing steps.
Also test constant-folding with builtins (this should reduce the
asserts in these files to assert true), and also test constant folding
with the C compilation.
Fix a bug whereby vectors with heap-allocated elements were not
initialized correctly.
Fix a bug caused by compiling and optimising empty vector literals.
Fix an OCaml test case that broke due to the ref type being used. Now
uses references to registers.
Fix a bug where Sail would output big integers that lem can't
parse. Checks if integer is between Int32.min_int and Int32.max_int
and if not, use integerOfString to represent the integer. Really this
should be fixed in Lem.
Make the python test runner script the default for testing builtins
and running the C compilation tests in test/run_tests.sh
Add a ocaml_build_dir option that sets a custom build directory for
OCaml. This is needed for running OCaml tests in parallel so the
builds don't clobber one another.
|
|
|
|
One day we will be free from the 4.02.3 menace, but today is not that day. :(
This should fix Sail on Jenkins
This reverts commit 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414.
|
|
Especially for return expressions, which fixes a test case
|
|
Handles mutable variables and conditionals (there are still some corner
cases that don't appear in Aarch64 to do).
The pretty printer is now back to preferring to use concrete types, but
has a special case for casts to print more general types.
|
|
Rather than exporting the implementation of type annotations as
type tannot = (Env.t * typ * effect) option
we leave it abstract as
type tannot
Some additional functions have been added to type_check.mli to work
with these abstract type annotations. Most use cases where the type
was constructed explicitly can be handled by using either mk_tannot or
empty_tannot. For pattern matching on a tannot there is a function
val destruct_tannot : tannot -> (Env.t * typ * effect) option
Note that it is specifically not guaranteed that using mk_tannot on
the elements returned by destruct_tannot re-constructs the same
tannot, as destruct_tannot is only used to give the old view of a type
annotation, and we may add additional information that will not be
returned by destruct_tannot.
|
|
Changes are:
- String.capitalize -> String.capitalize_ascii
- String.uppercase -> String.uppercase_ascii
- String.lowercase -> String.lowercase_ascii
Basically just making the change that the warning message suggested.
|
|
E_internal_cast, E_sizeof_internal, E_internal_exp,
E_internal_exp_user, E_comment, and E_comment_struc were all
unused. For a lem based interpreter, we want to be able to compile it
to iUsabelle, and due to slowness inherent in Isabelle's datatype
package we want to remove unused constructors in our AST type.
Also remove the lem_ast backend - it's heavily bitrotted, and for
loading the ARM ast into the interpreter it's just not viable to use
this approach as it just doesn't scale. We really need a way to be
able to serialise and deserialise the AST efficiently in Lem.
|
|
If we have an nexp that we can't print, look for an equivalent type
variable before looking for a constant - the constant may only be valid
locally (e.g., under an if) while the type variable will be valid
throughout the function.
Fixes a problem with aget_Mem on aarch64.
|
|
|
|
resolving the difference in type parameters between the prompt and state
monads, and allowing a single output file to be used with either.
Normally, the type alias is to the prompt monad, but for HOL4 we use the
state monad.
|
|
|
|
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.
|
|
Typechecking for-loops failed after the Lem rewriting passes in some cases: if
the lower bound for the loop may be greater than the upper bound, the loop
variable's type might be empty, and it cannot be initialised. This patch adds
a guard "lower <= upper" around the loop body, and removes it again during
pretty-printing.
|
|
|
|
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.
|
|
|
|
|
|
Now it just returns the actual arguments and a separate function
calculates the start index when required.
|
|
Turn on complex nexp rewriting for mono by default
(NB: solving is currently quite slow, will optimise)
|
|
(for monomorphisation, off for now because the analysis needs extended).
Also tighten up orig_nexp, make Lem backend replace # in type variables.
|
|
|
|
In particular, improve indentation of if-expressions, and provide infix syntax
for monadic binds in Isabelle, allowing Lem to preserve source whitespace.
|
|
Some functions are partial, e.g. converting a bitvector to an integer, which
might fail for the bit list representation due to undefined bits. Undefined
cases can be handled in different ways:
- call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the
default so far),
- return an option type,
- raise a failure in the monad, or
- use a bitstream oracle to resolve undefined bits.
This patch adds different versions of partial functions corresponding to those
options. The desired behaviour can be selected by choosing a binding in the
Sail prelude. The naming scheme is that the failwith version is the default,
while the other versions have the suffixes _maybe, _fail, and _oracle,
respectively.
|
|
For example, generates an auxiliary function execute_ADD (rs, rt, rd) for the
clause execute (ADD (rs,rt,rd)) = ...
Without this rewriting, the execute function easily becomes too large to be
handled by Isabelle (e.g., for CHERI-MIPS; for MIPS alone, it seems to be just
about small enough).
This used to be implemented in the pretty-printer, but that code was commented
out recently in order to support a recursive execute function for RISC-V
compressed instructions.
|
|
|
|
Previously union types could have no-argument constructors, for
example the option type was previously:
union option ('a : Type) = {
Some : 'a,
None
}
Now every union constructor must have a type, so option becomes:
union option ('a : Type) = {
Some : 'a,
None : unit
}
The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.
This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:
function is_none opt = match opt {
Some(_) => false,
None => true
}
it is now matched as
function is_none opt = match opt {
Some(_) => false,
None() => true
}
note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.
There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.
The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using
$include <option.sail>
|
|
Architecture-specific lemmas about concrete registers and types are generated
and written to a file <prefix>_lemmas.thy, generic lemmas are in the
theories *_extras.thy in lib/isabelle. In particular, State_extras contains
simplification lemmas about the lifting from prompt to state monad.
|
|
|
|
(so that we get enough type annotations for bitvectors)
|
|
Isabelle does not like nested annotations like "((exp :: typ) :: typ)".
|
|
Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad. Add some
Isabelle lemmas about the monad lifting.
Also drop the "_embed" and "_sequential" suffixes from names of generated
files.
|
|
- Use simplified monad type (e.g., without the with_aux constructors that are
not needed by the shallow embedding).
- Add support for registers with arbitrary types (e.g., records, enumerations,
vectors of vectors). Instead of using bit lists as the common representation
of register values at the monad interface, use a register_value type that is
generated per spec as a union of all register types that occur in the spec.
Conversion functions between register_value and concrete types are generated.
- Use the same representation of register references as the state monad, in
preparation of rebasing the state monad onto the prompt monad.
- Split out those types from sail_impl_base.lem that are used by the shallow
embedding into a new module sail_instr_kinds.lem, and import that. Removing
the dependency on Sail_impl_base from the shallow embedding avoids name clashes
between the different monad types.
Not yet done:
- Support for reading/writing register slices. Currently, a rewriting pass
pushes register slices in l-expressions to the right-hand side, turning a
write to a register slice into a read-modify-write. For interfacing with the
concurreny model, we will want to be more precise than that (in particular
since some specs represent register files as big single registers containing a
vector of bitvectors).
- Lemmas about the conversion functions to/from register_value should be
generated automatically.
|
|
|
|
|
|
It assumes that execute is non-recursive, which is not the case for RISC-V with
compressed instructions. Splitting execute into different auxiliary functions
for each clause is probably still useful, as Isabelle is likely to parse many
small functions faster than one big (potentially recursive) function, but this
splitting should be done in the rewriter instead of the pretty-printer, in
order to properly deal with recursion.
|
|
combinators)
Add Isabelle-specific theories imported directly after monad definitions, but
before other combinators. These theories contain lemmas that tell the function
package how to deal with monadic binds in function definitions.
|
|
Allow pretty-printing of existential types, if the existentially quantified
variables do not actually appear in the Lem output. This is useful for the bit
list representation of bitvectors, as it will print the type annotation "list
bitU" for bitvectors whose length depends on an existentially quantified
variable.
|
|
Uses the typechecker tests for now. Also fix two minor bugs in pretty-printer
and rewriter uncovered by the tests.
|
|
- Remove vector start indices
- Library refactoring: Definitions in sail_operators.lem now use Bitvector
type class and work for both bit list and machine word representations
- Add Lem bindings to AArch64 and RISC-V preludes
TODO: Merge specialised machine word operations from sail_operators_mwords into
sail_operators.
|
|
|
|
|
|
Keep track of which type variables have been bound in the function declaration,
and allow those to be pretty-printed
|
