| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
checking that the type variables visible in the output aren't
existential
|
|
Also added some new utility functions in ast_util
|
|
Fixed an issue in ast.ml with uneccessary type variables
|
|
- Bitvector pattern rewriting had stopped working due to a line of code being
lost in some merge.
- Fix a bug in early return rewriting that caused returns getting pulled out of
if-statements to disappear.
- There were some variable name clashes with keywords because doc_lem_id was
not always called.
- Ast_util.is_number failed to check for "int" and "nat" built-in types,
causing pattern matching on natural number literals to fail.
|
|
Also improves flow typing in assert statements for ASL parser
This patch does currently introduce a few test failures, probably due
to the new way literals are handled in case statements, which needs to
be investigated and fixed if possible.
|
|
|
|
|
|
|
|
|
|
also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway)
|
|
just LB_val in AST
also rename functions in rewriter.ml appropriately.
|
|
|
|
Also fixed basic ocaml test suite
|
|
as GPR
This was wrongly translated as an update of the vector of references.
|
|
- Support tuples in lexps
- Rewrite trivial sizeofs
- Rewrite early returns more aggressively
- Support let bindings with ticked variables (binding both a type-level and
term-level variable at the same time)
|
|
syntactically correct ocaml
|
|
experiments
|
|
Also, rewrite expressions in global let bindings (not only function bodies)
|
|
Also generate a function which initializes all the registers in a spec to undefined. This gives us the information we need post-rewriting to generate registers of any arbitrary type.
|
|
backed.
Ocaml doesn't support undefined values, so we need a way to remove
them from the specification in order to generate good ocaml
code. There are more subtle issues to - like if we initialize a
mutable variable with an undefined list, then the ocaml runtime has no
way of telling what it's length should be (as this information is
removed by the simple_types pass).
We therefore rewrite undefined literals with calls to functions that
create undefined types, e.g.
(bool) undefined becomes undefined_bool ()
(vector<'n,'m,dec,bit>) undefined becomes undefined_vector(sizeof 'n, sizeof 'm, undefined_bit ())
We therefore have to generate undefined_X functions for any user
defined datatype X. initial_check seems to be the logical place for
this. This is straightforward provided the user defined types are
not-recursive (and it shouldn't be too bad even if they are).
|
|
|
|
Basically we needed to make the rewriting step for E_sizeof and
E_constraint more aggressively try to rewrite those expressions from
variables in scope, without adding new parameters to pass the type
variables at runtime, as this can break in the presence of existential
quantification. Still some cleanup to do in this code, but tests on
the arm spec show that it now introduces the minimal amount of new
parameters.
|
|
|
|
The reason you want this is to do something like (note new parser only):
*********
default Order dec
type bits 'n:Int = vector('n - 1, 'n, dec, bit)
val zeros : forall 'n. atom('n) -> bits('n)
val decode : bool -> unit
function decode b = {
let 'datasize: {|32, 64|} = if b then 32 else 64;
let imm: bits('datasize) = zeros(datasize);
()
}
*********
for the ASL decode functions, where the typechecker now knows that the
datasize variable and the length of imm are the same.
|
|
|
|
to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail.
|
|
Conflicts:
src/pretty_print_common.ml
|
|
- Add some missing "wreg" effect annotations in the type checker
- Improve pretty-printing of register type definitions: In addition to a
"build" function, output an actual type definition, and some getter/setter
functions for register fields
- Fix a bug in sizeof rewriting that caused it to fail when rewriting nested
calls of functions that contained sizeof expressions
- Fix pretty-printing of user-defined union types with type variables (cf. test
case option_either.sail)
- Simplify nexps, e.g. "(8 * 8) - 1" becomes "63", in order to be able to
output more type annotations with bitvector lengths
- Add (back) some support for specifying Lem bindings in val specs using
"val extern ... foo = bar"
- Misc bug fixes
|
|
|
|
|
|
|
|
|
|
|
|
|
|
generation.
|
|
|
|
|
|
Ast_util.string_of_exp
|
|
If some type-level variables in a sizeof expression in a function body cannot
be directly extracted from the parameters of the function, add a new parameter
for each unresolved parameter, and rewrite calls to the function accordingly
|
|
Tries to extract values of nexps from the (type annotations of) parameters
passed to the function. This seems to correspond to the behaviour of the
previous typechecker.
|
|
See test/typecheck/pass/cons_pattern.sail for an example.
Also cleaned up the propagating effects code by making some of the
variable names less verbose
|
|
1) Added a new construct to the expression level: constraint. This is the
essentially the boolean form of sizeof. Whereas sizeof takes a nexp
and has type [:'n:], constraint takes a n_constraint and returns a
boolean. The hope is this will allow for flow typing to be represented
more explicitly in the generatated sail from ASL.
For example we could have something like:
default Order dec
val bit[64] -> unit effect pure test64
val forall 'n, ('n = 32 | 'n = 64 | 'n = 10) & 'n != 43. bit['n] -> unit effect pure test
function forall 'n. unit test addr =
{
if constraint('n = 32) then {
()
} else {
assert(constraint('n = 64), "64-bit mode");
test64(addr)
}
}
2) The other thing this example demonstrates is that flow constraints
now work with assert and not just if. Even though flow typing will
only guarantee us that 'n != 32 in the else branch, the assert gives
us 'n = 64. This is very useful as it's a common idiom in the ARM
spec to guarantee such things with an assert.
3) Added != to the n_constraint language
4) Changed the n_constraint language to add or and and as constructs
in constraints. Previously one could have a list of conjuncts each of
which were simple inequalites or set constraints, now one can do for
example:
val forall 'n, ('n = 32 | 'n = 64) & 'n in {32, 64}. bit['n] -> unit effect pure test
This has the very nice upside that every n_constraint can now be
negatated when flow-typing if statements. Note also that 'in' has been
introduced as a synonym for 'IN' in the constraint 'n in {32,64}. The
use of a block capital keyword was a bit odd there because all the
other keywords are lowercase.
|
|
|
|
|
|
Introduces a when keyword for case statements, as the Pat_when constructor for pexp's in the AST. This allows us to write things like:
typedef T = const union { int C1; int C2 }
function int test ((int) x, (T) y) =
switch y {
case (C1(z)) when z == 0 -> 0
case (C1(z)) when z != 0 -> x quot z
case (C2(z)) -> z
}
this should make translation from ASL's patterns much more straightforward
|
|
|
