how to use bitVec as a list index

[GUANCAIBAN]

here are my code
f2 = BitVec('f2', 32) f3 = BitVec('f3', 32) f4 = BitVec('f4', 32) v11 = dword_405420[(v9&0xff00)] ^ dword_405820[(v8&0xff0000)] ^ dword_405C20[(0xff000000&v7)] ^ dword_405020[(0xff&i)]
it make a error that is:
TypeError: list indices must be integers or slices, not BitVecRef

I need to get the index by Z3,I used to use BV2Int ,but it can‘t work as well

[GUANCAIBAN]

when I used BV2Int,it made a error:

v11 = dword_405420[BV2Int(v9&0xff00)] ^ dword_405820[BV2Int(v8&0xff0000)] ^ dword_405C20[BV2Int(0xff000000&v7)] ^ dword_405020[BV2Int(0xff&i)]
TypeError: list indices must be integers or slices, not ArithRef

[aytey]

What is dword_405820? A Python list? You cannot index into Python types with Z3 data-types.

Either dword_405820 should be an SMT array, or what you're trying to do can't work.

[GUANCAIBAN]

Oh....
I have a loop like this:
v11 = dword_405420[BYTE1(v9)] ^ dword_405820[BYTE2(v8)] ^ dword_405C20[HIBYTE(v7)] ^ dword_405020[BYTE0(i)]; v13 = dword_405420[BYTE1(i)] ^ dword_405820[BYTE2(v9)] ^ dword_405C20[HIBYTE(v8)] ^ dword_405020[BYTE0(v7)]; v15 = dword_405420[BYTE1(v7)] ^ dword_405820[BYTE2(i)] ^ dword_405C20[HIBYTE(v9)] ^ dword_405020[BYTE0(v8)]; v9 = dword_405420[BYTE1(v8)] ^ dword_405820[BYTE2(v7)] ^ dword_405C20[HIBYTE(i)] ^ dword_405020[(BYTE0(v9)]
i want to use z3 to solve it... or how to convert my python list to smt array

[aytey]

You really need to share a MWE if you want help. We have no idea what type you're using for dword_405820 or what you think it might represent.

Are you trying to access individual bits in another bit-vector?

[GUANCAIBAN]

hwo can i do?
a MWE here:
`
from z3 import *

f1 = BitVec('v6', 32)
f2 = BitVec('v7', 32)
f3 = BitVec('v8', 32)
f4 = BitVec('v9', 32)

dword_405420 = [0x0A7F45150, 0x65417E53, 0x0A4171AC3, 0x5E273A96, 0x6BAB3BCB, 0x459D1FF1,0x58FAACAB, 0x3E34B93]
dword_405820 = [0x0F45150A7, 0x417E5365, 0x171AC3A4, 0x273A965E, 0xAB3BCB6B, 0x9D1FF145,0xFAACAB58, 0xE34B9303]
dword_405C20 = [0x5150A7F4, 0x7E536541, 0x1AC3A417, 0x3A965E27, 0x3BCB6BAB, 0x1FF1459D, 0x0ACAB58FA,0x4B9303E3]
dword_405020 = [0x50A7F451, 0x5365417E, 0x0C3A4171A, 0x965E273A, 0x0CB6BAB3B, 0x0F1459D1F,0x0AB58FAAC]

for d in range(d):
v11 = dword_405420[(v9&0xff00)] ^ dword_405820[(v8&0xff0000)] ^ dword_405C20[(0xff000000&v7)] ^ dword_405020[(0xff&v6)]
v13 = dword_405420[(v6&0xff00)] ^ dword_405820[(0xff0000&v9)] ^ dword_405C20[(0xff000000&v8)] ^ dword_405020[(0xff&v7)]
v15 = dword_405420[(v7&0xff00)] ^ dword_405820[(v60xff0000&i)] ^ dword_405C20[BVInt(0xff000000&v9)] ^ dword_405020[(0xff&v8)]
v9 = dword_405420[(v8&0xff00)] ^ dword_405820[(0xff0000&v7)] ^ dword_405C20[(0xff000000&v6)] ^ dword_405020[(0xff&v9)]

s.add(v9 == 0x2836973B)
s.add(v8 == 0x241BCCFE)
s.add(v7 == 0x83EA91DE)
s.add(v6 == 0xE82BA79E)

if s.check() == sat:
m = s.model()
print("v6: ",f1)
print("v7: ",f2)
print("v8: ",f3)
print("v9: ",f4)
else:
print("fail to solve")
`
thanks

[NikolajBjorner]

The error message suggests you have created dword_405... as a python list.
You are using it in a symbolic context where you index into what amounts to an Array.
Your indices seem to be symbolic (z3 expressions) and not integers or slices.
You could initialize dword_405... as an uninterpreted constant of Array sort.