| Age | Commit message (Collapse) | Author |
|---|
|
Need to get these working again before we can thing about merging back
into sail2
|
|
Get rid of separate V_op and V_unary constructors. jib.ott now defines
the valid operations for V_call including zero/sign extension, in such
a way that the operation ctyp can be inferred. Overall this makes the
IR less ad-hoc, and means we can share more code between SMT and C.
string_of_cval no longer used by c_backend, which now uses sgen_cval
following other sgen_ functions in the code generator, meaning
string_of_cval doesn't have to produce valid C code anymore and so can
be used for backend-agnostic debug and error messages.
|
|
Add an Assumption event that is true whenever a property's type
quantifier is true, rather than wrapping body in a if-statement that
ends up creating a dead branch.
|
|
|
|
Add a new AE_write_ref constructor in the ANF representation to
make writes to register references explicit in Jib_compile
|
|
If we have e.g.
$property
val prop : ...
let X = 0
function prop(...) = X == ...
then we need to ensure that let X is included when we generate the
property.
|
|
|
|
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).
|
|
Had to change the hundreds and hundreds of places such values were
used. However this now lets us automatically prove cheri-concentrate
properties. Such as showing
function prop_cap_round_trip(cap: bits(128)) -> bool = {
let cap_rt = capToBits(capBitsToCapability(true, cap));
cap == cap_rt
}
is always true.
|
|
- 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
|
|
Most such patterns are re-written away by various re-writing steps,
but for those that arn't they are fairly easy to handle by just having
as patterns directly in the ANF-patterns.
Fixes #39
|
|
Avoids duplication between l-expressions and expressions. Also means that
special variables like current_exception and have_exception are treated
normally by functions such as instr_reads and instr_writes etc. Furthermore
we can now easily annotate Jib identifiers in ways that were not previously
possible with plain sail ids.
|
|
Check in a slightly nicer stylesheet for OCamldoc generated
documentation in etc. Most just add a maximum width and increase the
font size because the default looks absolutely terrible on high-DPI
monitors.
Move val_spec_ids out of initial_check and into ast_util where it
probably belongs. Rename some functions in util.ml to better match the
OCaml stdlib.
|
|
Main change is splitting apart the Sail->IR compilation stage and the
C code generation and optimization phase. Rather than variously
calling the intermediate language either bytecode (when it's not
really) or simply IR, we give it a name: Jib (a type of Sail). Most of
the types are still prefixed by c/C, and I don't think it's worth
changing this.
The various parts of the C backend are now in the src/jib/ subdirectory
src/jib/anf.ml - Sail->ANF translation
src/jib/jib_util.ml - various Jib AST processing and helper functions (formerly bytecode_util)
src/jib/jib_compile.ml - Sail->Jib translation (using Sail->ANF)
src/jib/c_backend.ml - Jib->C code generator and optimizations
Further, bytecode.ott is now jib.ott and generates jib.ml (which still
lives in src/ for now)
The optimizations in c_backend.ml should eventually be moved in a
separate jib_optimization file.
The Sail->Jib compilation can be parameterised by two functions - one
is a custom ANF->ANF optimization pass that can be specified on a per
Jib backend basis, and the other is the rule for translating Sail
types in Jib types. This can be more or less precise depending on how
precise we want to be about bit-widths etc, i.e. we only care about <64
and >64 for C, but for SMT generation we would want to be as precise
as possible.
Additional improvements:
The Jib IR is now agnostic about whether arguments are allocated on
the heap vs the stack and this is handled by the C code generator.
jib.ott now has some more comments explaining various parts of the Jib
AST.
A Set module and comparison function for ctyps is defined, and some
functions now return ctyp sets rather than lists to avoid repeated
work.
|
