Extract 和 Concat 之间的 z3 endian-ness 混合

Question

我很难理解字节顺序在 Z3 位向量中的工作原理。它与基础 CPU 相关吗？我在英特尔 cpu 上，并且 Extract 似乎按预期工作小端，但是当连接值时，端序似乎颠倒了。例如 Concat(0xaa, 0xbb) 产生 0xaabb 而不是预期的 0xbbaa（小端，0xaa 在左边所以应该是最小的）

以下代码说明了我遇到的问题：

import z3

# running on intel os x, little-endian

s = z3.BitVecVal(0xbbaa, 16)
print( "s {}".format(hex(z3.simplify(s).as_long())) ) # 0xbbaa

# b1 and b2 are extracted little-endian, as expected

b1 = z3.Extract(7,  0, s)
b2 = z3.Extract(15, 8, s)
# 0xaa, first byte, smallest
print( "b1 {}".format(hex(z3.simplify(b1).as_long())) )
# 0xbb, second byte, biggest 
print( "b2 {}".format(hex(z3.simplify(b2).as_long())) ) 

# don't understand what is happening here, b1 is the left-most byte,
# should be smallest

j = z3.Concat(b1, b2)
print( "j {}".format(hex(z3.simplify(j).as_long())) ) 
# result 0xaabb position of bytes are reversed, 
# b2 (0xbb) is now smallest

Answer 1

好的，我想我明白了。它在任何地方都没有很好的记录，但 z3 是 big-endian。位总是从右开始索引，0 是最右边的最小位。这解释了 Extract ( Extract(high, low, from) ) 的参数顺序有些奇怪，因为 "high" 位实际上位于低位的左侧。

Concat 和 Extract 似乎具有不同的字节顺序，因为 Extract 切片是从右到左的，而 Concat 从左到右构建位向量。

Answer 2

Z3 在这里只是遵循位向量的 SMTLib 标准，它与体系结构无关。详情请看这里：http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml

特别是concat定义如下：

[[(concat s t)]] := λx:[0, n+m). if (x < m) then [[t]](x) else [[s]](x - m)
   where
   s and t are terms of sort (_ BitVec n) and (_ BitVec m), respectively,
   0 < n, 0 < m.

这有点啰嗦，但如果你仔细研究它，语义会清楚地表明 "lower" 部分来自 t，"upper" 部分来自 s。

同样，extract 定义为：

[[((_ extract i j) s))]] := λx:[0, i-j+1). [[s]](j + x)
   where s is of sort (_ BitVec l), 0 ≤ j ≤ i < l.

这基本上会丢弃第一个 j-1 位，并从那时起一直保持到第 i 位。

Extract 和 Concat 之间的 z3 endian-ness 混合

z3 endian-ness mixup between Extract and Concat

z3