| Age | Commit message (Collapse) | Author |
|---|
|
|
|
In particular tuple types containing bitvectors.
|
|
Also add support for intialising variables with an "undefined" literal;
make the SMT solver treat the value as arbitrary but fixed.
|
|
|
|
Supporting more ASL idioms
|
|
For example, in
let datasize = e in ...
the typechecker will generate a kid '_datasize if e has an existential
type (with one kid), and in
let 'datasize = e in ...
the typechecker will bind both 'datasize and '_datasize. If we
substitute one as part of constant propagation, this patch will make
constant propagation also substitute the other.
|
|
... and try to resolve them using constant propagation.
|
|
Ask the type checker instead of looking at the expression syntax. This
also discovers implied instantiations, e.g. if we previously knew
('N in {32, 64}) and we have an assertion ('N != 32), then we know
('N == 64).
|
|
This will propagate constant assignments in chosen branches of case
expressions after applying pattern choices, e.g. the assignment to
datasize in
match size {
[bitone, _] => datasize = 64,
...
}
when pattern [bitone, _] is chosen for size.
|
|
This will constant-fold letbindings such as
let LOG2_TAG_GRANULE : int(4) = 4
let TAG_GRANULE : int = (1 << LOG2_TAG_GRANULE)
which is useful for the translation to Lem if TAG_GRANULE is used in
bitvector lengths.
|
|
- Handle more combinations of patterns and expressions in constant
propagation
- Remove dead code after throw() in monomorphisation
- Use correct val specs and environments when analysing and
pretty-printing function clauses
|
|
This check is used in the guarded pattern rewrite step, which would
previously generate some impossible matches (e.g. matching expression
"true" against pattern "false").
|
|
|
|
Add casts for function arguments using the constraints in the
environment of the function clause (not just assertions within the
function body). Also pass in the global typing environment for
comparison with the environment within the function clause (and make a
corresponding change in the Lem pretty-printer so that it uses the right
environments).
|
|
|
|
Split the variable (tuple) type into an input and output type. They are
meant to be the same, but due to the way function types are
instantiated, unification can fail in the case of existential types, as
in the added test case (when trying to generate Lem definitions from
it). The output of the loop will be checked against the expected type,
though, due to a type annotation outside the loop added by the rewrite
pass for variable updates.
|
|
|
|
|
|
... instead of a tuple assignment. This makes the rewrite independent
of the tuple assignment rewrite and allows it to be moved after the
latter (nesting vector concat lexps into tuple lexps is an idiom in ASL,
but the other way around doesn't make sense).
|
|
In particular, don't add annotations for types with existentially
quantified variables that only occur in constraints, not in the type,
e.g. {'i1 'i2, 'i1 == div('i2, 8). int('i1)}. These seem to confuse the
type checker when pulled out into the source AST.
|
|
In the new version of the ASL-generated Sail, some vector operators are
also overloaded for integers to match idioms of ASL (e.g. i[31:0], where
i is an integer), so check in the monomorphisation rewrites that we use
bitvector helper functions only for actual bitvectors.
|
|
|
|
... instead of dying with "Syntax error".
|
|
... that match the names in lib/real.sail.
Also fix the lem mapping for abs_int_atom and a Lem syntax error with
nested record updates.
|
|
Check that indices are within bounds, not just in the right
(increasing/decreasing) order.
|
|
|
|
|
|
|
|
Asserting constraints from the loop condition in the body is fine for
while-loops, but doesn't make sense for until-loops.
|
|
Mention robert's workaround for z3 on WSL
|
|
|
|
|
|
Add documentation for CLion/PyCharm/IntelliJ syntax highlighting
|
|
|
|
From:
No type variable 'ex14#
to:
Type error:
[../and_let_bool.sail]:6:19-50
6 | and_bool(let y : bool = x in not_bool(y), x)
| ^-----------------------------^
| The type variable 'ex14# would leak into an outer scope.
|
| Try adding a type annotation to this expression.
| This error was caused by:
| [../and_let_bool.sail]:6:23-24
| 6 | and_bool(let y : bool = x in not_bool(y), x)
| | ^
| | Type variable 'ex14# was introduced here
|
|
|
Turns out the TextMate Bundles plugin can load the vscode extension and
provide some basic syntax highlighting.
|
|
Allows ASL-to-Sail translation to automatically patch lexp bounds check
errors.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Again use an $ifdef to avoid breaking RMEM. We can't use the same
barrier_kind, because we *really* want a plain enumeration both for
its simple SMT representation and a simple 1 to 1 mapping to the cat
models used by herd.
Technically for Isla, all the read_kind/write_kind/barrier_kind etc
types can be defined separately on a per-architecture basis anyway, so
maybe using this file at all is a bit of an anachronism.
|
|
|
|
Fixes #61
|
|
|
|
|
