| Age | Commit message (Collapse) | Author |
|---|
|
(Adds 'interpreter' externs as appropriate.)
|
|
Uses new primop 'string_take' which is much easier to implement in e.g. C
|
|
When converting to A-normal form I just used the type of the then
branch of if statements to get the type of the whole if statement -
usually they'd be the same, but with flow typing one of the branches
can have a false constraint, which then allows the optimizer to fit
any integer into a 64-bit integer causing an overflow. The fix is to
correctly use the type the typechecker gives for the whole if
statement.
Also add decimal_string_of_bits to the C output.
Rename is_reftyp to is_ref_typ to be more consistent with other
is_X_typ functions in Ast_util.
|
|
- more hex_bits functions, add decimal_string_of_bits
- extra tuple unfolding in constructors
- note that variables can be redundant wildcard clauses
- update RISC-V patch
|
|
- implement set_slice and set_slice_int
- lemmas for more constraints
- make real sqrt visible
- unfolding list membership needs andb and orb to be handled first
|
|
- hints for dotp
- handle exists separately when trying eauto to keep search depth low
- more uniform existential handling (i.e., we now handle all existentials
in the way we used to only handle existentials around atoms)
|
|
|
|
|
|
|
|
The omega tactic doesn't like them
|
|
|
|
C: Don't print usage message and quit when called with no arguments,
as this is used for testing C output
OCaml: Fix generation of datatypes with multiple type arguments
OCaml: Generate P_cons pattern correctly
C: Fix constant propagation to not propagate letbindings with type
annotations. This behaviour could cause type errors due to how type
variables are introduced. Now we only propagate letbindings when the
type of the propagated variable is guaranteed to be the same as the
inferred type of the binding.
Tests: Add OCaml tests to the C end-to-end tests (which really
shouldn't be in test/c/ any more, something like test/compile might be
better). Currently some issues with reals there like interpreter.
Tests: Rename list.sail -> list_test.sail because ocaml doesn't want
to compile files called list.ml.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Revert a change to string_of_bits because it broke all the RISC-V
tests in OCaml. string_of_int (int_of_string x) is not valid because x may not
fit within an integer.
|
|
otherwise some other parts don't work properly.
Also update RISC-V patch.
|
|
Also required some solver fixes:
- make sure that ArithFacts are always cleared to avoid loops
- extract_properties should do the goal first because it might add extra
work to do in the hypotheses
- unfolding should come before extract_properties
|
|
constructed when a function call, cast, or binder demands them, removing
some ambiguous corner cases.
Also
- Don't simplify nexps before printing (note that we usually end up
needing a (8 * x) / 8 lemma as a result)
- More extraction of properties in the goal
- Splitting of conditionals/matches in goals (which can occur more often
because of the new positions of build_ex in definitions)
- Try simple solving first to improve speed / reduce proof sizes / help
fill in metavariables (because manipulating the goal can interfere with
instantiating them)
- Update RISC-V patch
|
|
Add some builtins to the C sail lib.
Enable some gcc warnings.
|
|
typing
Added a regression test as c/test/downcast_fn.sail
|
|
|
|
Now all we need to do is make sure the RISC-V builtins are mapped to
the correct C functions, and RISC-V in C should work
(hopefully). We're still missing some of the functions in sail.c for
the mappings so those have to be implemented.
|
|
|
|
|
|
Requires a recent Lem version that supports generating session-qualified
imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860
|
|
Test that basic bi-directional mappings compile correctly
Test that a minimal file importing the prelude compiles correctly
|
|
- Fill in Coq builtins for more of the RISC-V prelude
- Update Barriers
- More general autocast
- Temporary sub_nat definition (until the backend handles nat better)
- Patch to bring results into a reasonable state
- Use Let rather than Definition for non-dependent top-level values
|
|
|
|
|
|
|
|
(which were slowing down RISCV unacceptably because dealing with the
xlen max/min values is surprisingly expensive)
|
|
|
|
|
|
Handles mutable variables and conditionals (there are still some corner
cases that don't appear in Aarch64 to do).
The pretty printer is now back to preferring to use concrete types, but
has a special case for casts to print more general types.
|
|
|
|
Not really what we want, but a useful placeholder because of the
widespread use of ex_int.
|
|
1. for monadic values (not in a terribly useful way, though)
2. for more types
|
|
|
|
|
|
|
|
The new option -dcoq_debug_on takes a list of functions to output tracing
on.
|
|
This allows debug messages to include the current cycle count
which can be useful for debugging.
|
|
Use eauto so that user-added hints are more flexible,
example with Replicate in aarch64, dropped zbool to prevent slow
proof searches (and preprocessing deals with boolean comparisons now).
Report failed constraints after preprocessing;
Separate preprocessing tactic out.
|
|
|
|
|
