| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Previously the specialization would remove any polymorphic union
constructor that was never created anywhere in the
specification. While this wasn't usually problematic, it does leave an
edge case where such a constructor could be matched upon in a pattern,
and then the resulting match would fail to compile as it would be
matching on a constructor kind that doesn't exists.
This should fix that issue by chaging the V_ctor_kind value into an
F_ctor_kind fragment. Previously a polymorphic constructor-kind would
have been represented by its mangled name, e.g.
V_ctor_kind "zSome_unit"
would now be represented as
V_ctor_kind ("Some", unifiers, ty)
where ty is a monomorphic version of the original constructor's type
such that
ctyp_unify original_ty ty = unifiers
and the mangled name we generate is
zencode_string ("Some_" ^ string_of_list "_" string_of_ctyp unifiers)
|
|
|
|
Add a new short_loc_to_string function that produces just the file and line number as
a single line. loc_to_string adds a bunch of terminal color codes and other formatting
designed for producing pretty error-messages in the terminal, which isn't ideal when
the string appears in prover output as part of an assert statement. This is should be
purely an aesthetic change.
|
|
|
|
|
|
Prevents some type variables that came from unpacking existentials
leaking into generated Coq types.
|
|
|
|
Allows us to track the last version of the return variable when the AST
in in SSA form.
|
|
|
|
Separate calling the rewriter from the backend-specific parts of
sail.ml
|
|
Rather than having a separate variable for each backend X,
opt_print_X, just have a single variable opt_print_target, where
target contains a string option, such as `Some "lem"` or `Some
"ocaml"`, then we have a function target that takes that string and
invokes the appropriate backend, so the main function in sail.ml goes
from being a giant if-then-else block to a single call to
target !opt_target ast env
This allows us to implement a :compile <target> command in the
interactive toplevel
Also implement a :rewrites <target> command which performs all the
rewrites for a specific target, so rather than doing e.g.
> sail -c -O -o out $FILES
one could instead interactively do
> sail -i
:option -undefined_gen
:load $FILES
:option -O
:option -o out
:rewrites c
:compile c
:quit
for the same result.
To support this the behavior of the interactive mode has changed
slightly. It no longer performs any rewrites at all, so a :rewrites
interpreter is currently needed to interpret functions in the
interactive toplevel, nor does it automatically set any other flags,
so -undefined_gen is needed in this case, which is usually implied by
the -c flag.
|
|
|
|
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.
|
|
|
|
|
