| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This refactoring is intended to allow this type to have more than just a
list of definitions in future.
|
|
Accidentally broken by e1a2b0d2 because the Coq backend looks at the
wrong type to decide when a proof is needed.
|
|
Helps with Coq 8.11. Also fix BBVDIR default in test script.
|
|
|
|
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.
|
|
(using match rather than let-and-projections because the latter would
be reduced by tactics like unfold)
|
|
(plus test, as it wasn't covered before)
|
|
- 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
|
|
|
|
|
|
- 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
|
|
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)
|
|
-coq_alt_modules2 <filename> provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default definitions of MR and M monads
|
|
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.
|
|
Mostly in the Coq backend, plus a few testcases that use bitvector
builtins on poly-vectors (which works on some backends, but not Coq).
Also handle some additional list inclusion proofs in Coq.
|
|
|
|
Loops measures are now abstracted over the variables so that they can be
used in proofs. Add total Hoare logic rules for until.
|
|
|
|
These don't appear much, but are now showing up in the sail-arm model
due to an innocent change elsewhere.
|
|
If they're merged with a type variable then we still need to name the
argument so that it can be used in other types.
|
|
|
|
|
|
Mostly to make constraints sent to the SMT solver and Coq nicer, but
also makes it easy to remove uninformative constraints in the Coq
back-end.
|
|
Also get rid of the notation warnings for single element records.
|
|
|
|
Clean up ott grammar a bit
|
|
|
|
|
|
|
|
Previously we only checked at atom, now use destruct_atom_nexp to pick
up implicit too.
|
|
Usually we do this at function applications and casts, but occasionally
a variable is used at a different type.
|
|
The former is useful when a bitvector variable is cast to an equivalent
length, and the latter is easier for Coq's unification to deal with.
|
|
|
|
|
|
can now write e.g.
forall (constant 'n : Int) rather than forall ('n: Int)
which requires 'n to be a constant integer value whenever the function
is called. I added this to the 'addrsize variable on memory
reads/writes to absolutely guarantee in the SMT generation that we
don't have to worry about the address being a variable length
bitvector.
|
|
|
|
(in particular, to cope with Type_check.simp_typ)
|
|
|
|
This can massively reduce Coq's typechecking time on assertion heavy code,
such as the builtins tests.
|
|
|
|
|
|
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).
|
|
- 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
|
|
|
|
|
|
|
|
Prevents some type variables that came from unpacking existentials
leaking into generated Coq types.
|
|
|
