| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Can now set a prefix for generated C functions with -c_prefix so
-c_prefix sail_ would give sail_execute_CGetPerm over
zexecute_CGetPerm. We still have to use our standard name-mangling
scheme to avoid possible collisions within the name.
Can build C that doesn't expect the standard runtime, which leaves
operations like read_memory, write_memory etc to be stubbed in by
another C program including the generated Sail. Things like
letbindings are still an issue because we rely on a very small runtime
to initialize global letbindings and similar.
-c_separate_execute splits the execute function apart in the generated C
|
|
|
|
|
|
The old check used the wrong part of the AST. It would stop when it
reached the actual effect, anyway, but this should improve performance.
|
|
Add a flag in C backend ctx that allows us to generate arbitrary
precision signed integer types, rather than just int64
|
|
|
|
|
|
|
|
If we want to use our low-level intermediate representation to generate
SMT, then we want to be more precise than just splitting integers into
64-bits and larger. This commit changes CT_int and CT_int64 into CT_lint
for large integers and CT_fint n for (signed) fixed precision integers
that fit within n bits. This follows the convention for bitvectors where
we have CT_fbits for fixed-length bitvectors and CT_lbits for large
arbitrary precision bitvectors.
|
|
|
|
Now builds for riscv duopod
|
|
|
|
Run C tests with -O -Oconstant_fold -auto_mono
|
|
Perhaps suprisingly to some, this did not mean that Sail was
unable to typecheck the identify function.
While doing this rename Effect_opt_pure to Effect_opt_none - as
Effect_opt_pure was the effect equivalent of Typ_annot_opt_none,
and actually means that the function definition lacks an effect
annnotation, not that the function is actually pure, so this was
*extremely* misleading. The effect_opt that actually indicated a
function is pure was (and still is) the succinct:
Effect_opt_aux (Effect_opt_effect (Effect_aux (Effect_set [], _)), _)
In fact because in the grammar we only specify effects on
valspecs (they can always be inferred for fundefs in the absence
of a valspec) effect_opts are basically vestigial and are always
Effect_opt_none.
What might actually be super nice would be to remove rec_opt,
effect_opt and typ_annot_opt from fundefs in ast.ml altogether
and if we want them in the syntax just have them in parse_ast.ml
and pull them into a valspec during the initial check.
|
|
Thanks to Mark for finding this bug. Regression test is
complex_exist_sat in test/typecheck/pass/
|
|
|
|
|
|
Specifically remove branches where flow-typing implies false, as this
allows the optimizer to prove anything, which can result in nonsense
code. This does incur something of a performance hit.
|
|
specialize functions now take a 'specialization' parameter that
specifies how they will specialize the AST. typ_ord_specialization
gives the previous behaviour, whereas int_specialization allows
specializing on Int-kinded arguments. Note that this can loop forever
unless the appropriate case splits are inserted beforehand, presumably
by monomorphisation.
rename is_nat_kopt -> is_int_kopt for consistency
|
|
Produces vaguely-correct-looking-but-untested code for riscv duopod
|
|
When adding a constraint such as `x <= 2^n-1` to an environment
containing e.g. `n in {32, 64}` or similar, we can enumerate all
values of n and add `n == 32 & x <= 2^32-1 | n == 64 & x <= 2^64-1`
instead. The exponentials then get simplified away, which means that
we stay on the SMT solver's happy path.
This is enabled by the (experimental, name subject to change) flag
-smt_linearize, as this both allows some things to typecheck that
didn't before (see pow_32_64.sail in test/typecheck/pass), but also
may potentially cause some things that typecheck to no longer
typecheck for SMT solvers like z3 that have some support for reasoning
with power functions, or where we could simply treat the exponential
as a uninterpreted function.
Also make the -dsmt_verbose option print the smtlib2 files for the
solve functions in constraint.ml. We currently ignore the -smt_solver
option for these, because smtlib does not guarantee a standard format
for the output of get-model, so we always use z3 in this case.
Following the last commit where solve got renamed solve_unique, there
are now 3 functions for solving constraints:
* Constraint.solve_smt, which finds a solution if one exists
* Constraint.solve_all_smt, which returns all possible
solutions. Currently there's no bound, so this could loop forever if
there are infinite solutions.
* Constraint.solve_unique, which returns a unique solution if one exists
Fix a bug where $option pragmas were dropped unnecessarily.
|
|
|
|
Fixes #34
|
|
Fixes #33
|
|
|
|
This should produce identical Lem and Coq output, but allow dumped Sail
ASTs from the final stages of rewriting to be reread with -dmagic_hash.
|
|
This uses the SMT solver to spot rich `atom_bool` types which don't contain
any information, replaces them with bool, and handles most of the
construction and projection of them.
The SMT part will be replaced by a simplification procedure soon, because
it can't handle some important cases.
|
|
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.
|
|
|
