| Age | Commit message (Collapse) | Author |
|---|
|
:def <definition> evaluates a top-level definition
:(b)ind <id> : <type> creates an identifier within the interactive type-checking environment
:let <id> = <expression> defines an identifier
Using :def the following now works and brings the correct vector
operations into scope.
:def default Order dec
:load lib/prelude.sail
Also fix a type-variable shadowing bug
|
|
Some SMT goals in unification would generate problems with missing
variables. Turns out the SMT solver would happily ignore this and
return the correct unsat/sat result anyway. However, this does affect
the error code from the solver so if we now check the return code we
must make sure that we don't generate any smtlib files that generate
warnings or errors.
Now that kopts_of_X functions exist in ast_util we can just use those
to get well-kinded variables from the constraint itself rather than
relying on the typechecker to pass in a list of variables which makes
things simpler to boot!
|
|
|
|
|
|
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.
|
|
|
|
|
|
Fixes bad precedence issues, removes an out-of-date special case that's
not necessary, and solves more goals.
|
|
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.
|
|
For a Int-parameterised struct F('x: Int) = ... the optimizer would
attempt to optimize field access in cases where 'x was known to
constrain the types of the struct fields only locally. Which would
create a type error in the generated C. Now we always use the type
from the global struct type.
However, we previously weren't using struct type quantifiers to
optimize the field representation, which we now do.
Also rename some utility functions to better match the List
functions in the OCaml stdlib.
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
Previously instrs_graph would return the control-flow graph, as well
as some data-flow by including reads and writes to variables
represented as a node type in the graph (G_id). However, this was not
particularly useful, and since the graph isn't in SSA form (so
identifiers are non-unique) potentially inaccurate too. This
simplifies the code so instrs_graph just returns control flow
dependencies, which in turn simplifies the instr_reads and
instr_writes functions.
|
|
(e.g., for the dual 32/64 bit RISC-V model)
Apply this rewrite in Coq backend.
|
|
|
|
This shouldn't change any functionality.
|
|
|
|
|
|
Make instruction dependency graph use graph.ml
Expose incremental graph building functions for performance in graph.mli
|
|
|
|
Add some comments in constant_fold.ml
|
|
|
|
|
|
|
|
|
|
Rename rewrite_split_fun_constr_pats to rewrite_split_fun_ctor_pats as
constr is commonly used as an abbreviation for constraint rather than
constructor, and add a more descriptive comment.
|
|
Previously any constraints on constructors were just outright dropped
when splitting the execute function in Lem generation. Now we get the
constraints and type signature for each execute clause from the type
given by Env.get_union_constructor, rather than by inferring the type
of the pattern in each function clause.
Currently this can still fail in the case where we have
union U('x: Int), C1('x) = { ctor: {'y. C2('x, 'y), T('x, 'y)} }
and
val execute : forall 'z, C3('z). U('z) -> unit
when C3 implies C1, and the body of an excute clause relies on the
fact that C3 is stronger than C1, as each split function execute_ctor
is only guaranteed to be constrained by some subset of C1. This seems
unlikely to happen in practice though.
Also fix a bug when binding P as int('T) against int('T) and similar
cases, where the new type variable would cause the old type variable
to become shadowed, but the constraint that the bound type variable
and the old type variable are equal would not take this into account.
|
|
|
|
|
|
|
|
Fixes some bugs found by doing this
|
|
|
|
Also make unifying int against int('n) work as expected for
constructor applications.
|
|
|
|
Issues came up with Christophers translation of hand-written ARM into
Sail2 where we were being overly pedantic about the exact position of
existential quantifiers in constructors with multiple arguments. This
commit generalises unify_typ and type_coercion_unify to be more
flexible and support this. Should think at some point if unify_typ can
be generalised further.
This fix should fix the decode side of things, but may be some issues
with the executes that still need looking into when existentials and
multiple argument constructors are mixed.
|
|
|
|
|
|
Also drop unused implication function
|
|
|
|
Now generates something vaguely sensible for RISC-V, although the solver
needs a little work.
Adds type annotations around effectful, rich and/or expressions.
|
|
Make internal_plet produce annotations (with code to replace unusable
type variables)
Add mappings for bool kids at bindings
Add version of and_bool that proves a property
|
|
|
|
|
|
|
|
Also make pretty printing more keen on line breaking
|
