Z3py - 滚动答案

【问题标题】：Z3py - do a rollZ3py - 滚动
【发布时间】：2012-12-19 15:14:56
【问题描述】：

有没有推荐的方法来向左或向右按位滚动任意数量？

例如带有一个字节 - 0x57 rolr 3 = 0xEA。

我在 Z3py 文档中没有找到任何“滚动”操作。我正在考虑为每个位使用BitVecs，但这似乎效率不高/可能行不通。任何建议表示赞赏，谢谢。

编辑：感谢到目前为止的答案。这更像是一个 API 问题，因为我现在很讨厌它。这是我的出发点。

def roll(bt):
count = BitVecVal(int('0x03', 16), 8)
s.add(bt == (bt << count | bt >> (8 - count)) & 0xFF)

a = BitVec('a', 8)
s = Solver()
roll(a)
s.add(a == BitVecVal(int('0xEA', 16), 8))
s.check()

这没有打印出来，模型不可用。

【问题讨论】：

与shift 有什么不同？
>> 是算术移位。这就是为什么它不起作用。这是一个示例链接：rise4fun.com/Z3Py/5NwMR
顺便说一句，Z3Py 有函数：RotateLeft 和 RotateRight。 z3.py 模块有一堆 pydoc 注释。这里是doxygen出品的在线API参考指南：research.microsoft.com/en-us/um/redmond/projects/z3/…
@LeonardodeMoura 这段代码没有打印出任何东西，是不是有问题？ a = BitVec('a', 8)s = Solver()s.add(RotateLeft(a, 3) == BitVecVal(int('0xEA', 16), 8))s.check()s.model()
您必须添加print。这是您的示例链接，prints：rise4fun.com/Z3Py/v6D

标签： python z3 smt

【解决方案1】：

你可以这样旋转：

size = 0x100  # size of the bitvector

rotated = (x << n) | (x >> (size - n)) & (size - 1)

【讨论】：

Eric，您的解决方案几乎是正确的。问题是 Z3Py 中的 >> 是算术移位。对于逻辑移位，我们必须使用函数LShR。我们可以在线试用rise4fun.com/Z3Py/kpd1
@LeonardodeMoura：因此最后是& (size - 1)。尝试我在回答中写的内容：rise4fun.com/Z3Py/K58
@LeonardodeMoura：实际上，我不知道为什么这段代码有效。如果设置了 x 的最高位，(x >> (size - n)) 不会用 1 填充所有高位吗？
Eric：你说得对，(x >> (size - n)) 将用 1 填充高位。也就是说，为什么我说它是不正确的。我们可以通过按位与((1 << n) - 1) 擦除高位。这将擦除除第一个n 位之外的所有位。与(size - 1) 的按位与仅在((1 << n) - 1) == (size - 1) 时有效。 n == 5 和 size == 32 确实是这种情况。这是普通版的链接：rise4fun.com/Z3Py/g127
@LeonardodeMoura：我不知道我在想什么。当我写(size - 1) 时，我的意思是(1 << size - 1)，目的是屏蔽溢出的位。