| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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.
|
|
|
|
|
|
Adds missing constraints for aarch64
|
|
As a result, add proof to pow2.
|
|
|
|
to code gen issue.
|
|
interpreter implementations of same.
|
|
|
|
|
|
On second thought, this change should not really make a difference; the CHERI
test suite still passes without it. Moreover, using unsigned conversion of the
vector argument leads to more convenient lemmas for the provers.
|
|
CHERI test suite now passes using Isabelle-generated emulator
|
|
add_vec_int and similar functions in the Lem library used unsigned instead of
signed conversion.
|
|
|
|
|
|
redundant files.
|
|
|
|
|
|
Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state. The previous behaviour can be
implemented as Sail code, if desired.
Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
|
|
|
