| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
See sailcov/README.md for a short description
Fix many location info bugs discovered by eyeballing output
|
|
|
|
|
|
|
|
Currently uses the -c2 option
Now generates a sail_state struct which is passed as a pointer to all
generated functions. This contains all registers, letbindings, and the
exception state. (Letbindings must be included as they can contain
pointers to registers). This should make it possible to use sail models
in a multi-threaded program by creating multiple sail_states, provided a
suitable set of thread-safe memory builtins are provided. Currently the
sail_state cannot be passed to the memory builtins.
For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c.
foo_emu.c wraps the generated library into an emulator that behaves the
same as the one we previously generated.
The sail_assert and sail_match_failure builtins are now in a separate
file, as they must exist even when the RTS is not used.
Name mangling can be controlled via the exports and exports_mangled
fields of the configuration struct (currently not exposed outside of
OCaml). exports allows specifying a name in C for any Sail identifier
(before name mangling) and exports_mangled allows specifiying a name for
a mangled Sail identifier - this is primarily useful for generic
functions and data structures which have been specialised.
|
|
Defined in terms of tdiv so we don't have to add it to backends that
don't already have it
|
|
|
|
Supporting more ASL idioms
|
|
|
|
|
|
... 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.
|
|
|
|
|
|
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.
|
|
|
|
Allows keeping track of which instructions actually get executed in a trace
|
|
However, use an ifdef to make sure the ifetch changes only appear for the ARM spec, because
otherwise the generated lem for RMEM will break.
|
|
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.
|
|
|
|
Now used in RISC-V model.
|
|
|
|
- add liftRS support to tactics
- define uint and sint in terms of functions without proof terms
- eq_vec correctness
- lemma that rounding up integers using reals is the obvious integer calculation
- another proof irrelevance tactic
- try lemmas in the sail hintdb both before and after goal processing
|
|
- break up goals more in unbool
- remove intuition from guess_ex_solver because it can be too expensive
- flip goals around because the side that evars appears on has changed
- generalise the and/or tactics
- make a couple of tactics more specific/robust
|
|
|
|
Includes removing an explicit use of a lemma generated by abstract, which
was causing problems with different versions of Coq because the names
change.
|
|
Mostly from making the aarch64 model compile again
- switch order some arithmetic lemmas
- move list membership rewrites alongside other comparisons to enable more
rewriting
- copy hypotheses used in other types/definitions so that they can be
rewritten
- lift boolean existentials out of implications in hypotheses so they can
be used as witnesses without proving the condition
- add negation to solve_bool_with_Z
- add some new bool solving for goals from and_boolMP/or_boolMP
|
|
- ArithFact takes a boolean predicate
- defined in terms of ArithFactP, which takes a Prop predicate,
and is used directly for existentials
- used abstract in more definitions with direct proofs
- beef up solve_bool_with_Z to handle more equalities, andb and orb
|
|
|
|
|
|
|
|
(which might not be present).
|
|
- add state versions of foreach combinators
- support dependent sumbool pattern matching (i.e., those where the
property is actually used)
- add rewriting congruence rules, state monad lifting rules,
and invariant proof rules for these
|
|
|
|
|
|
- requires fixpoint definitions containing proofs to be processed in proof
mode (due to a bug in Coq), so change libraries and pretty printing to
do that
- adjust some lemmas to avoid extra evars
|
|
|
|
|
|
Some builtins need properly implementing still
Use modified spinlock implementation from hafnium with stdatomic,
rather than assembly
|
|
|
|
|
|
bitvectors in C
Assumes a Sail C library that has functions with the right types to
support this. Currently lib/int128 supports the -Ofixed_int option,
which was previously -Oint128.
Add a version of Sail C library that can be built with -nostdlib and
-ffreestanding, assuming the above options. Currently just a header
file without any implementation, but with the right types
|
|
It only produces them when necessary (because some types do not have
decidable equality due to embedded proofs).
Also add trivial instance for the unit type.
|
|
- in particular at monadic interfaces (i.e., sufficient for instruction
ast types)
- see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an
example that's not currently supported
- generate definitions for type-level Bool definitions (i.e., predicates)
|
|
In particular, shift state lambdas outside of if/match/let which avoids
unnecessary abstraction/applications. Add more rules to the tactic.
|
|
Also tweak the informative and/or boolean definitions so that they use
the same proofs in both monads.
|
|
|
|
(otherwise Sail uses the type from one and the extern from the other)
|
