overhauls target/value abstraction and introduces roles (4/n) #1275
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is the continuation of the #1225, #1226, and #1227 series of
changes that were focused on substituting the old and inextensible
Arch.t
abstraction with the newTheory.Target.t
representation.This episode is instigated by the upcoming implementation of the
RISCV target. Since RISCV is the out target that is not supported with
Arch.t it became a good test of the new Theory.Target.t abstraction.
As the RISCV worked showed, we still have lots of code that depends on
Arch.t, most importantly Primus, which was fully dependent on
Arch.t. The main issue was that Theory.Target.t doesn't provide any
means to encode register classes, which prevented us from using it
everywhere in Primus, e.g., we need to know which register is the
stack pointer in order to setup the stack.
To implement this, we introduce a new abstraction called role. A
role could be generally applied to any entity but so far we are only
talking about the roles of registers in various targets. The target
definiton now acccepts the
regs
paramater that takes the registerfile specification with each register assigned one or more roles,
e.g., here is the register file specification for 8086,
I.e., we assign a set of roles to a set of registers. We also now have
two new functions
Theory.Target.regs
andTheory.Target.reg
thatenable querying the register file of the target for register that
fulfill one or more roles. Whilst we publish a limited number of
well-known (blessed) roles in the
Theory.Role.Register
module, moreroles could be added as user need it. For example, in the code snippet
above we have two non-standard roles that are specific to the x86
architectures,
Role.index
andRole.segment
.With roles we can drop the dependency on Target in most of the places
where it makes sense (I still left it in x86 and other target-specific
plugins, which obviously are independent on the newly added
architectures).