-
Notifications
You must be signed in to change notification settings - Fork 61
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[ASL+AArch64] Allow access to UDF under variant #1001
Conversation
Thanks for this Hadrien! Just to check that my understanding is correct. I did the following:
and then edited it to look like this:
Then I run the following test:
But I get
|
Hi @relokin, Sorry for this, bad litmus syntax that somehow I did not test. The syntax for variants is: With:
and the rest similar to what you did, I get:
|
ofc! I saw that space in Variant and I thought ah I didn't know this was allowed but never checked :) Thanks Hadrien! |
@@ -730,6 +730,8 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : | |||
"domain" ^= var (barrier_domain dom); | |||
"types" ^= var (barrier_typ btyp); | |||
] ) | |||
| I_UDF k when C.variant Variant.ASL_AArch64_UDF -> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Out of curiosity, can't unconditionally handle UDF with that ASL code? Because if that's the case you don't really need the variant either, do you?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well the problem is that I'm really not able to match the behaviour of herd without the variant ASL:
In herd/AArch64Sem.ml
:
| I_UDF _ ->
let (>>!) = M.(>>!) in
let ft = Some FaultType.AArch64.UndefinedInstruction in
let m_fault = mk_fault None Dir.R Annot.N ii ft None in
let lbl_v = get_instr_label ii in
m_fault >>| set_elr_el1 lbl_v ii >>! B.Fault [AArch64Base.elr_el1, lbl_v]
In the Arm ARM downloaded by herd (a bit out of date):
// Execute
// =======
// No operation.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ah yes, I think this something that happens in decode.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, thanks @HadrienRenaud!
@@ -730,6 +730,8 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : | |||
"domain" ^= var (barrier_domain dom); | |||
"types" ^= var (barrier_typ btyp); | |||
] ) | |||
| I_UDF k when C.variant Variant.ASL_AArch64_UDF -> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ah yes, I think this something that happens in decode.
4e158bb
to
c7a7be8
Compare
c7a7be8
to
8ab8b26
Compare
How to run an instruction not implemented in herd?
For example, for
FADD
, a how-to.Then edit the file to add the correct variables as the decode part of the instruction would usually do.
Then run
make install
or run with the correct-libdir
, and a test like: