Avoid redundant extends/truncations during normalization

[danmatichuk]

Part of normalization post-processing step is to strip all integers out of the final specification. This is done fairly naively by representing all integers as 65-bit bitvectors (capable of representing a 64-bit value that is unambiguously meant to be signed or unsigned).

Often arithmetic on bitvector values is performed in the ASL by first casting a bitvector to an unsigned integer, performing the necessary arithmetic on the integers, and then casting the final result back into a bitvector. After normalization, this then has the odd structure of extending a bitvector to 65 bits, performing some arithmetic, then truncating back down to its original length.

let r2085 := (uext _R11_0 65)
    r2087 := (bv_add r2085 (0xfffffffc :: [65]))
    r2088 := (trunc r2087 32)

The resulting expression becomes cumbersome during verification (i.e. in macaw). In many cases, it should be possible to instead avoid this pattern and represent the above as a single bv_add.

r2088 := (bv_add _R11_0 (0xfffffffc :: [32]))

This can likely be handled during translation/normalization by more carefully choosing the bitwidth of an integer-as-bitvector based on its usage.