| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The inter-instruction semantics is responsible for correctly handling memory
writes without tags; the lifting to the state monad handles it as writing a
value with a zero tag bit.
|
|
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.
|
|
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.
|
|
|
