UQ-PAC / aslp

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

Improving Rotation Translation #83

Open l-kent opened 1 month ago

l-kent commented 1 month ago

The ASL ROR() method currently does not translate ideally, due to having an internal assertion and branching.

https://github.com/UQ-PAC/aslp/blob/abd63cb88c81f34822dd3d0779517430d0aa9ba8/mra_tools/arch/arch.asl#L14483-L14489

It is analogous to the ASR(), LSL() and LSR() methods which are handled with the added asr_bits, lsl_bits and lsr_bits methods, and the approach taken with those seems possible to extend to ROR() as well. SMT-Lib has a rotate_right function that could serve as a translation target in a similar way to how the asr_bits function represents the SMT-Lib asr function.