SRI-CSL/llvm2smt

Not all instructions handle vector arguments

Opened this issue · 2 comments

Need to fix Trunc, Zext, Sext, Bitcast?, Inttoptr, Ptrtoint, Select, and Getelementptr?.
They are allowed to have vector operands and return vector values (all of the same
length). The instructions operate element wise in such cases.

Most have been fixed.
The only remaining ones are Bitcast and Getelementptr.
Bitcast is a bit of a puzzle, on the one hand they say:

"It is always a no-op cast because no bits change with this conversion."

but on the other hand they give examples like:

%Z = bitcast <2 x int> %V to i64;        ; yields i64: %V

so I don't think it can be a noop on the SMT side.

I haven't pondered GEP.

Ooops pressed the wrong button. This is NOT closed.