| Age | Commit message (Collapse) | Author |
|---|
|
... and try to resolve them using constant propagation.
|
|
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.
|
|
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.
|
|
|
|
Also be more careful to avoid pattern bindings with identifiers to avoid
parsing clashes, eg `let 'bytes := ...` which is confused with the
notation for binary literals.
|
|
|
|
|
|
... not just in type abbreviations.
Fixes an error in the RV32 build of CHERI-RISC-V.
|
|
|
|
If, for example, we have a bidirectional encoding-decoding mapping as in
sail-riscv, but want to translate only the decoder to a theorem prover,
this commit allows us to stub out the the encoder by splicing in dummy
definitions.
|
|
:fixed_registers command
|
|
accordingly
|
|
|
|
Remove P_record as it's never been implemented in
parser/typechecker/rewriter, and is not likely to be. This also means
we can get rid of some ugliness with the fpat and mfpat types. Stubs
for P_or and P_not are left as they still may get added to ASL and we
might want to support them, although there are good reasons to keep
our patterns simple.
The lem warning for while -> while0 for ocaml doesn't matter because
it's only used in lem, and the 32-bit number warning is just noise.
|
|
|
|
Fixes #53
|
|
|
|
|
|
sail definitions
Definitions can be made external on a per-backend basis, so we need to
make sure constant folding doesn't inline external functions that have
sail definitions for backends other than the ones we are currently
targetting
|
|
Do this by making sure that generic pattern literal re-writing gets
applied to top-level function clauses. This requires re-ordering the
rewrites for most backends otherwise they break, which hopefully wo
anything.
After doing this re-ordering I had to turn off casting when rewriting
bitvector patterns, otherwise insane things can happen.
|
|
- allow disjoint_pat to be used on patterns that have just been introduced
by the rewrite without rechecking
- don't rebuild the matched expression in the generated fallthrough case
(or any wildcard fall-through) - it may be dead code and generate badly
typed Lem
- update the type environment passed to rewrites whenever type checking
is performed; stale information broke some rewrites
|
|
|
|
A missing type annotation in rewrite_guarded_clauses caused a crash in
some cases. Also fix an effect propagation bug in
rewrite_letbind_effects.
|
|
Add a fallthrough case that fails to potentially partial pattern
matches. This also helps to preserve any guard in the final match case,
which might be needed for flow typing (see the discussion on issue #51).
TODO: Merge with the MakeExhaustive rewrite, which currently does not
support guarded patterns.
|
|
Fixes #47.
Also adjust the nexp substitution so that the error message points to a
useful location, and replace the empty environment with the initial
environment in a few functions that do type checking to ensure that the
prover is set up (which may be needed for the wf check).
|
|
|
|
|
|
Clean up ott grammar a bit
|
|
|
|
|
|
|
|
Only change that should be needed for 99.9% of uses is to change
vector('n, 'ord, bit) to bitvector('n, 'ord), and adding
$ifndef FEATURE_BITVECTOR_TYPE
type bitvector('n, dec) = vector('n, dec, bit)
$endif
for to support any Sail before this
Currently I have all C, Typechecking, and SMT tests passing, as well
as the RISC-V spec building OCaml and C completely unmodified.
|
|
|
|
|
|
With the new interpreter changes computing the initial state for the
interpreter does some significant work. The existing code was
re-computing the initial state for every subexpression in the
specification (not even just the ones due to be constant-folded away).
Now we just compute the initial state once and use it for all constant
folds.
Also reduce the time taken for the simple_assignments rewrite from 20s
to under 1s for ARMv8.5, by skipping l-expressions that are already in
the simplest form.
|
|
|
|
|
|
|
|
Currently only supports pure termination measures for loops with effects.
The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
|
|
|
|
Rather than generating SMT from a function called check_sat, now find
any function with a $property directive and generate SMT for it, e.g.
$property
function prop_cap_round_trip(cap: bits(128)) -> bool = {
let cap_rt = capToBits(capBitsToCapability(true, cap));
cap == cap_rt
}
$property
function prop_base_lteq_top(capbits: bits(128)) -> bool = {
let c = capBitsToCapability(true, capbits);
let (base, top) = getCapBounds(c);
let e = unsigned(c.E);
e >= 51 | base <= top
}
The file property.ml has a function for gathering all the properties
in a file, as well as a rewrite-pass for properties with type
quantifiers, which allows us to handle properties like
function prop forall 'n, 'n <= 100. (bv: bits('n)) -> bool = exp
by rewriting to (conceptually)
function prop(bv: bits(MAX_BIT_WIDTH)) -> bool =
if length(bv) > 100 then true else exp
The function return is now automatically negated (i.e. always true =
unsat, sometimes false = sat), which makes sense for quickcheck-type
properties.
|
|
Allows a quick hack where you can give a termination limit rather than a
proper measure for functions with awkward termination properties.
|
|
Currently only works with CVC4, test cases are in test/smt. Can prove
that RISC-V add instruction actually adds values in registers and
that's about it for now.
|
|
- Rename DeIid to Operator. It corresponds to operator <string> in the
syntax. The previous name is from when it was called deinfix in
sail1.
- Removed things that weren't actually common from
pretty_print_common.ml, e.g. printing identifiers is backend
specific. The doc_id function here was only used for a very specific
use case in pretty_print_lem, so I simplified it and renamed it to
doc_sia_id, as it is always used for a SIA.Id whatever that is.
- There is some support for anonymous records in constructors, e.g.
union Foo ('a : Type) = {
MkFoo : { field1 : 'a, field2 : int }
}
somewhat similar to the enum syntax in Rust. I'm not sure when this
was added, but there were a few odd things about it. It was
desugared in the preprocessor, rather than initial_check, and the
desugaring generated incorrect code for polymorphic anonymous
records as above.
I moved the code to initial_check, so the pre-processor now just
deals with pre-processor things and not generating types, and I
fixed the code to work with polymorphic types. This revealed some
issues in the C backend w.r.t. polymorphic structs, which is the
bulk of this commit. I also added some tests for this feature.
- OCaml backend can now generate a valid string_of function for
polymorphic structs, previously this would cause the ocaml to fail
to compile.
- Some cleanup in the Sail ott definition
- Add support for E_var in interpreter previously this would just
cause the interpreter to fail
|
|
|
|
Separate calling the rewriter from the backend-specific parts of
sail.ml
|
