| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Rather than each rewrite being an opaque function, with separate lists
of rewrites for each backend, instead put all the rewrites into a
single list then have each backend define which of those rewrites it
wants to use and in what order.
For example, rather than having
let rewrite_defs_ocaml = [
...
("rewrite_undefined", rewrite_undefined_if_gen false);
...
]
we would now have
let all_rewrites = [
...
("undefined", Bool_rewriter (fun b -> Basic_rewriter (rewrite_undefined_if_gen b)));
...
]
let rewriters_ocaml = [
...
("undefined", [Bool_arg false]);
...
]
let rewrite_defs_ocaml =
List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewriters_ocaml
This means we can introspect on the arguments required for each
rewrite, allowing a :rewrite command in the interactive mode which can
parse the arguments required for each rewrite, so we can invoke the
above rewrite as
sail> :rewrite undefined false
with completion for the rewrite name based on all_rewrites, and hints
for any arguments.
The idea behind this is if we want to generate a very custom slice of
a specification, we can set it up as a sequence of interpreter
commands, e.g.
...
:rewrite split execute
:slice_roots execute_LOAD
:slice_cuts rX wX
:slice
:rewrite tuple_assignments
...
where we slice a spec just after splitting the execute function. This
should help in avoiding an endless proliferation of additional options
and flags on the command line.
|
|
|
|
Copied from Coq backend.
|
|
These are the correct versions for div/mod in the SMT solver
|
|
inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.
|
|
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
|
|
Issue with pretty-printing mapping clauses types fixed by both
cf7eb8b83 and 0e2f1710a, so remove the redundant clauses. In the
parser we allow both
```
| Mapping id
{ mk_sd (SD_mapping ($2, mk_tannotn)) $startpos $endpos }
| Mapping id Colon funcl_typ
{ mk_sd (SD_mapping ($2, $4)) $startpos $endpos }
```
so we should probably use doc_binding to correctly print any
quantifier on the funcl_typ. Although since polymorphism and mappings
don't play nicely together right now this likely doesn't occur very
often in practice.
|
|
|
|
Add a test case to ensure variable types in l-expressions remain the
same with flow-sensitive constraints.
|
|
See comments on e92ff687.
|
|
Fix scattered mapping printing and output message for missing val spec
|
|
|
|
In particular, spot variable shadowing and handle (n as 'm) patterns.
|
|
|
|
Remove unused experimental optimizations
|
|
|
|
Add a function Jib_optimize.inline which can inline functions. To make
this more efficient, we can make identifiers unique on a per-function
basis.
|
|
- add dummy print_bits function
- support int(1) like types in axioms
|
|
- skip a few more that aren't supported yet
- produce better debugging information (in particular, in the right order)
- avoid some autocasts that aren't supported yet and are usually
unnecessary
- Handle more constraints like `8 * n = 8 * ?Goal`
|
|
It helps the Coq backend if the shape of constraints embedded in types
doesn't change too much.
|
|
|
|
These should be preserved for prover backends.
|
|
|
|
|
|
Propagating constants into mutually recursive calls and removing dead branches
might break mutually recursive cycles.
Also make constant propagation use the existing interpreter-based constant
folding to evaluate function calls with only constant arguments (as opposed to
a mixture of inlining and hard-coded rewrite rules).
|
|
Rewrite <> true/false in goals.
Correct implicits in record and variant types.
Use expanded valspecs from the type checker in axioms.
Allow list notations in type definitions.
Skip some not-yet-supported tests.
|
|
|
|
Mostly just a small quality-of-life improvement
|
|
|
|
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.
|
|
: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.
|
