search

UQ-PAC / aslp

Partial evaluator for Arm's Architecture Specification Language (ASL)
Other
7 stars 2 forks source link

Reordered Memory Operations #59

Open ncough opened 6 months ago

ncough commented 6 months ago

Paired memory reads may become reordered, as seen in 0x28400021:

constant bits ( 32 ) Exp18__5 = Mem.read.0 {{ 4 }} ( add_bits.0 {{ 64 }} ( __array _R [ 1 ],'0000000000000000000000000000000000000000000000000000000000000100' ),4,2 ) ;
__array _R [ 1 ] = ZeroExtend.0 {{ 32,64 }} ( Mem.read.0 {{ 4 }} ( __array _R [ 1 ],4,2 ),64 ) ;
__array _R [ 0 ] = ZeroExtend.0 {{ 32,64 }} ( Exp18__5,64 ) ;

The incremented access (stored in Exp18__5) appears to evaluate before the non-incremented, however the inverse is expected for aarch64_memory_pair_general_no_alloc. Likely due to copy prop.

ncough commented 6 months ago

This is linked to #25. Suspect we would prefer to keep memory operations in order, even if you can't depend on them evaluating in any given order.