[ASL+AArch64] Allow access to UDF under variant

[HadrienRenaud]

How to run an instruction not implemented in herd?

For example, for FADD, a how-to.

cd herd/libdir/asl-pseudocode/aarch64/instrs
mv udf/UDF_only_perm_undef.opn udf/UDF_only_perm_undef.opn.bak
cp float/arithmetic/add-sub/FADD_D_floatdp2.opn udf/UDF_only_perm_undef.opn

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:

AArch64 UDF
variant=ASL+AArch64+UDF
{}
P0     ;
UDF 1  ;

[relokin]

Thanks for this Hadrien!

Just to check that my understanding is correct.

I did the following:

cp integer/arithmetic/add-sub/extendedreg/ADD_32_addsub_ext.opn udf/UDF_only_perm_undef.opn

and then edited it to look like this:

// Execute
// =======

bits(datasize) result;
bits(datasize) operand1 = X[0, 32];
bits(datasize) operand2 = ExtendReg(1, ExtendType_UXTH, 0, 32);

(result, -) = AddWithCarry(operand1, operand2, '0');

X[2, 32] = result;

Then I run the following test:

AArch64 UDF
Variant ASL+AArch64+UDF
{
0:X0=21;
0:X1=42;
}
P0     ;
UDF 1  ;
locations[0:X2;]

But I get

Test UDF Required
States 1
0:X2=0;
Ok
Witnesses
Positive: 1 Negative: 0
Condition forall (true)
Observation UDF Always 1 0
Time UDF 0.01
Hash=53bb635e83af9884274b948b0c2a6276

[HadrienRenaud]

Hi @relokin,

Sorry for this, bad litmus syntax that somehow I did not test. The syntax for variants is: variants=foo,bar.

With:

AArch64 UDF
variant=ASL+AArch64+UDF
{
0:X0=21;
0:X1=42;
}
P0     ;
UDF 1  ;
locations[0:X2;]

and the rest similar to what you did, I get:

❯ dune exec herd7 -- -set-libdir herd/libdir ./tests-aarch64/udf1.litmus
Test UDF Required                        
States 1
0:X2=63;
Ok
Witnesses
Positive: 1 Negative: 0
Condition forall (true)
Observation UDF Always 1 0
Time UDF 0.21
Hash=53bb635e83af9884274b948b0c2a6276

[relokin]

ofc! I saw that space in Variant and I thought ah I didn't know this was allowed but never checked :)

Thanks Hadrien!

[relokin]

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?

[HadrienRenaud]

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.

[relokin]

ah yes, I think this something that happens in decode.

[relokin]

LGTM, thanks @HadrienRenaud!

[relokin]

ah yes, I think this something that happens in decode.