Q registers on sail-arm

[Trolldemorted]

My compiler is generating code that puts a 192bit (3x usize) struct into a Q register and pushes it on the stack:

; preamble
.text:00000000002116E4 SUB             SP, SP, #0x70
.text:00000000002116E8 STR             X30, [SP,#0x70+var_10]
; X8 = pointer to default values
.text:00000000002116EC ADRP            X8, #xmmword_200240@PAGE
; Q0 = default values
.text:00000000002116F0 LDR             Q0, [X8,#xmmword_200240@PAGEOFF]
[...]
; push q0 to stack
.text:000000000021170C STR             Q0, [SP,#0x70+var_70]

I looked at the output and saw that the ADRP emulation causes two separate 8 byte reads:

[log]: Read: Enum(EnumMember { enum_id: 5, member: 0 }) Bits(B64 { len: 64, bits: 2097728 }) I128(8) false
[log]: Read: Enum(EnumMember { enum_id: 5, member: 0 }) Bits(B64 { len: 64, bits: 2097736 }) I128(8) false

I verified with a debugger that read_concrete returns the correct byte_vec with Ok(Val::Bits(B::from_bytes(&byte_vec))) for both reads.

However when isla-lib executes the push it writes a Symbolic(Sym { id: 20084 }) to the stack, and I don't really know why. I wanted to look at Q0's value, but I didn't find any SIMD-registers in local_state.regs:

for (reg_name, reg_val) in &frame.local_state.regs {
    println!("{:?}={:?}", shared_state.symtab.to_str(*reg_name), reg_val)
}

A rg -i "register " over the sail model suggest that those registers are not defined. Is that the case, and if yes shouldn't isla-lib return an exec error when they are erroneously being accessed?

[Alasdair]

The vector registers are defined as one big register called _V, that's a vector of bitvectors. Originally R0-R31 were similar but I manually split them apart. In Sail/ASL there are accessor functions so you can write Q(n) = value.

However when isla-lib executes the push it writes a Symbolic(Sym { id: 20084 }) to the stack, and I don't really know why. I wanted to look at Q0's value, but I didn't find any SIMD-registers in local_state.regs:

Probably just means we are representing its value in the SMT solver because it's more than 64 bits long. Rather than implement arbitrary precision bitvectors ourselves we just use Z3's arbitrary precision bitvectors. Currently I have support for either a max bitvector length (in Isla) of either 64-bits or 129-bits (for making CHERI capabilities a bit easier to work with), and everything larger is left to Z3.

[Trolldemorted]

So if the values are being split into smaller parts when they are being loaded, those will contain the correct values? That's neat!