Z3py - 做一個卷

是否有推薦的方法來做一個按位滾動向左或向右的任何數額？Z3py - 做一個卷

例如一個字節 - 0x57 rolr 3 = 0xEA。

我還沒有在Z3py文檔中發現任何「滾動」操作。我正在考慮爲每一點使用BitVec s，但這似乎並不高效/可能無效。任何意見表示讚賞，謝謝。

編輯：謝謝你到目前爲止的答案。這更多的是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()

這不打印出來，模型不可用。

來源

2012-12-19 daybreak

什麼是從[SHIFT]不同（http://docs.python.org/2/library/stdtypes.html#bitwise-operations-on -integer類型）？ –

'''是算術轉換。這就是爲什麼它不起作用。這裏是一個鏈接的例子：http://rise4fun.com/Z3Py/5NwMR –

順便說一句，Z3Py的功能：'RotateLeft'和'RotateRight'。 z3.py模塊有一堆pydoc註釋。以下是由doxygen生成的在線API參考指南：http://research.microsoft.com/en-us/um/redmond/projects/z3/namespacez3py.html –

你可以做這樣的旋轉：

size = 0x100 # size of the bitvector 

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

來源

2012-12-19 15:25:56 Eric

Eric，您的解決方案几乎是正確的。問題在於Z3Py中的'''是算術轉換。對於邏輯移位，我們必須使用函數'LShR'。我們可以在網上嘗試http://rise4fun.com/Z3Py/kpd1 –

@LeonardodeMoura：因此'＆（size - 1）'在最後。嘗試我在我的答案中寫道：http://rise4fun.com/Z3Py/K58 – Eric

Eric：對不起。你是對的。 –

Z3py - 做一個卷

回答

相關問題