| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
Allows us to track the last version of the return variable when the AST
in in SSA form.
|
|
|
|
Remove unused experimental optimizations
|
|
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.
|
|
Add a CL_void l-expression so we don't have redundant unit-typed
variables everywhere, and add an optimization in Jib_optimize called
optimize_unit which introduces these.
Remove the basic control-flow graph in Jib_util and add a new mutable
control-flow graph type in Jib_ssa which allows the IR to be converted
into SSA form. The mutable graph allows for more efficient updates,
and includes both back and forwards references making it much more
convenient to traverse.
Having an SSA representation should make some optimizations much
simpler, and is also probably more natural for SMT generation where
variables have to be defined once using declare-const anyway.
Debug option -ddump_flow_graphs now outputs SSA'd graphs of the
functions in a specification.
|
|
Shouldn't affect anything as this is done by the typechecker now.
Also remove some unfinished tracing code from c_backend.ml
|
|
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.
|
