| Age | Commit message (Collapse) | Author |
|---|
|
Use E_read_memt for reading tagged memory, as in sail2_impl_base.lem,
and rename E_write_mem to E_write_memt, since it always writes a tag.
|
|
It is used for nondeterministic choice, so Undefined might be
misleading.
|
|
Lets one distinguish in a trace whether an instruction tried to read
tagged memory or just read data without caring about the tag; this is
useful for formulating predicates on traces.
|
|
|
|
Removes some friction by back-and-forth conversion when handling events
|
|
Running traces, directly accessing memory state
|
|
|
|
- Merge tag reading/writing outcomes into memory value reading/writing outcomes
- Add effective address to Write_mem; this duplicates information in the
Write_ea outcome that should come before, but it makes the effective address
more conveniently available in events and traces, and it allows the following
simplification in the state monad:
- Remove write_ea field from state record; the effective address is now
expected as a parameter to the write_memS function
- Remove last_exclusive_operation_was_load field from state record; this was
used to keep track of exclusive loads, but this was a a relatively coarse
approximation anyway, so it might make more sense to track this in
(architecture-specific) Sail code. Overall, the state record now simply
contains the fields regstate, memstate, tagstate.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(aimed at RISC-V)
|
|
|
|
|
|
Handles the common case of a single level string append pattern in a
way designed to be friendlier to Coq etc, by generating an auxiliary
function for each pattern rather than emitting a massive nested
pattern match twice.
|
|
|
|
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.
|
|
When constructing expressions, we need to provide locations for the
generated expressions to give useful error messages. However adding
these at every mk_X function in ast_util would be very verbose,
especially for complex expressions.
Add new locate_X functions (with the one for expressions simply being
called locate), which take a location and recursively apply it to
every child node, e.g.
locate (gen_loc l) (mk_exp (... (mk_exp ..., mk_exp ...)))
would mark every part of the constructed expression as being generated
from code at location l.
|
|
|
|
|
|
|
|
(This leads to more redundant uses, but I'll tackle that later)
|
|
|
|
|
|
- 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
|
|
|
|
|
|
hex_bits_N_matches_prefix
|
|
This really demonstrates why we should switch to Typ_fn being a typ
list * typ constructor because the implementation here feels *really*
hacky with dummy Typ_tup constructors being used to enforce single
arguments for constructors.
|
|
|
|
|
|
|
|
- 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)
|
|
Broke E_internal_plet on some simple existential types
|
|
|
|
the generated pattern so re-typechecking works
|
|
than binary
|
|
|
|
int_of_string
This fixes e.g. problems with 64-bit bitmask immediates in ARM assembly.
|
|
I got bored of this so I wrote a Python script to generate all of them
between 1 and 33, plus 48 and 64. It's in a comment.
We should really get around to making the typechecker work with
polymorphic mappings...
|
|
|
