| Age | Commit message (Collapse) | Author |
|---|
|
Useful to see what constraints we are generating that are particularly
hard, and which of our specs work with different solvers.
Refactor code to use smt in names rather than specifically z3
|
|
Simple heuristic to try local variables with the same name as type
variables first, roughly doubles typechecking speed.
|
|
Some versions of z3 do not like any constraints with the form 2^f(n),
even when such constraints are completely trivial, or only exist in
the environment yet no bearing on the current goal. Unfortunately the
z3 in Ubuntu LTS has these issues.
We can mitigate these issues somewhat by removing any 2^f(n)
containing conjuncts from the environment when z3 returns unknown, and
attempting to reprove the goal. In practice Type_check.prove only
guarantees that the goal is provable when it returns true, and does
not guarantee that it is false when it returns false, only that it
wasn't provable in the specified timeout. Similarly for
Type_check.solve. Mostly this is fine, because prove returning false
usually triggers a type error, or e.g. in the C optimizer always has a
sensible fallback (where it just won't optimize that specific
case). What is slightly concerning is that this z3 issues means that
Sail written using the latest z3 from git may not compile using Ubuntu
LTS z3.
We could if we wanted to put additional restrictions on Nexp_exp to
avoid this issue. We should also look over uses of Type_check.prove in
Sail to make sure callers are using it correctly.
|
|
Make type-at-cursor work for scattered function clauses in emacs
|
|
This makes sure we don't do any kind of re-writing or de-scatter any
definitions when loading files into emacs. The difference here is that
normally all files are processed together, but the emacs mode loads
each file one by one. This is probably what we want to be doing
anyway, so location information stays accurate for scattered
functions for things like type-at-cursor commands and similar.
Also fix some warnings.
Fixes #32
|
|
Reduces the current arm model output from 268MB to 15MB.
|
|
in opam file in anticipation of release and add yojson dependency.
|
|
Fix a bug where we generated empty definitions which pre 4.07 versions
of OCaml don't appear to support.
|
|
|
|
|
|
Make LEXP_deref an inference rule. This should allow strictly more programs to type-check.
|
|
|
|
|
|
|
|
When we are building from git, we put the git version info in manifest.ml, so
we'll get the following from sail -v
Sail $last_git_tag ($branch @ $commit_sha)
If we are be built from opam we can't assume we are in a git repository as
opam downloads specific tags as tarballs, so instead we check for the precense
of SHARE_DIR which is set by our opam build script, and instead output
Sail 0.8 (sail2 @ opam)
which is the next git tag (current is 0.7.1, this must be updated by hand),
the branch name from which opam releases are generated and then opam rather
than the commit SHA.
I also removed the Makefile-non-opam file as it's bitrotted and unused
|
|
|
|
This supports the following syntax:
type xlen : Int = 64
type ylen : Int = 1
type xlenbits = bits(xlen)
bitfield Mstatus : xlenbits = {
SD : xlen - ylen,
SXL : xlen - ylen - 1 .. xlen - ylen - 3
}
|
|
Also make the rewriter keep failed assertions in output when pruning
blocks.
|
|
|
|
Previously it would quietly throw away all definitions for an id except one.
This usually doesn't matter, but some rewrites use overloaded identifiers
and can break if the definition is lost.
|
|
|
|
Tweak colours of monomorphistion test output
|
|
For example, in
type xlen : Int = 64
type xlenbits = bits(xlen)
rewrite the 'xlen' in the definition of 'xlenbits' to the constant 64 in
order to simplify Lem generation. In order to facilitate this, pass
through the global typing environment to the rewriting steps (in the AST
itself, type definitions don't carry annotations with environments).
|
|
add_num_def and get_num_def are no longer used. The rewrite pass that
used them would fail on Nexp_ids because of this, but seeing as that
never happened we can probably assume that particular line of code is
simply never touched by any of our models or test suite?
|
|
|
|
Various tweaks to the monomorphisation rewrites. Disable old sizeof
rewriting for Lem backend and rely on the type checker rewriting
implicit arguments. Also avoid unifying nexps with sums, as this can
easily fail due to commutativity and associativity.
|
|
Fix monomorphisation tests
|
|
|
|
Allow a file sail.json in the same directory as the sail source file
which contains the ordering and options needed for sail files involved
in a specific ISA definition. I have an example for v8.5 in sail-arm.
The interactive Sail process running within emacs then knows about the
relationship between Sail files, so C-c C-l works for files in the ARM
spec. Also added a C-c C-x command to jump to a type error. Requires
yojson library to build interactive Sail.
|
|
Can now use C-c C-s to start an interactive Sail process, C-c C-l to
load a file, and C-c C-q to kill the sail process. Type errors are
highlighted in the emacs buffer (like with merlin for OCaml) with a
tooltip for the type-error, as well as being displayed in the
minibuffer. Need to add a C-c C-x command like merlin to jump to the
error, and figure out how to handle multiple files nicely, as well as
hooking the save function like tuareg/merlin, but this is already
enough to make working with small examples quite a bit more pleasant.
|
|
|
|
|
|
All sizeof expressions now removed by the type-checker, so it's now
properly a type error if they cannot be removed rather than a bizarre
re-write error. This also greatly improves compilation speed overall, at
the expense of the first type-checking pass.
|
|
Rather than using sizeof-rewriting which is slow and error-prone, just
make implicit function arguments explicit, so:
val ZeroExtend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
let x : bits(32) = ZeroExtend(0xFFFF)
would be re-written (by the typechecker itself) into
val ZeroExtend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
let x : bits(32) = ZeroExtend(32, 0xFFFF)
then all we need to do is map implicit -> int in a rewrite, and use
trivial sizeof-rewriting only. We pretty much never want to use the
form of sizeof-rewriting that propagates function arguments through
multiple functions because it's extremely error-prone. Anything that
isn't re-writable via trivial sizeof rewriting should be a type error,
so it would be good to re-write sizeof expressions within the
type-checker.
|
|
|
|
This reduces the amount of unnecessary complex existentials that appear
during rewriting.
|
|
|
|
|
|
|
|
|
|
|
|
Make all backends behave the same when a catch block does not catch a
specific exception.
|
|
Usually we want to unify on return types, but in the case of
constraint unification (especially during rewriting) we can find
ourselves in the situation where unifying too eagerly on a return
type like bool('p & 'q) can cause us to instantiate 'p and 'q in the
wrong order (as & should really respect commutativity and
associativity during typechecking to avoid being overly brittle).
Originally I simply avoided adding cases for unify on NC_and/NC_or
and similar to avoid these cases, but this lead to the undesirable
situation where identical types wouldn't unify with each other for
an empty set of goals, which should be a trivial property of the
unification functions.
The solution is therefore to identify type variables in ambiguous
positions, and remove them from the list of goals during
unification. All type variables still have to be resolved by the
time we finish checking each application, but this has the added
bonus of making order much less important when it comes to
instantiating type variables.
Currently I am overly conservative about what qualifies as
ambigious, but this set should be expanded
|
|
|
|
|
|
|
|
|
|
Fix pretty printer bug
|
|
|
|
now that cast insertion can handle RISC-V
Also inserts specs for casts in they're not present
|
