don't convert icmp to logical node; operator is applied to arguments of the wrong sort

[archercreat]

terminate called after throwing an instance of 'triton::exceptions::SolverEngine'
  what():  Z3Solver::getModels(): operator is applied to arguments of the wrong sort

Hello. I encountered a bug when trying to lift llvm ir to triton and then to z3 expression. llvm:

%a = trunc i64 %rdx to i32
%b = icmp eq %a, 0
%c = zext i1 %b to i64
ret i64 %c

Invalid z3 expression:

((_ zero_extend 63) (distinct ((_ extract 31 0) rdx) (_ bv0 32)))

I'm not z3 expert but not using logical node in icmp handler fixes this error.

[JonathanSalwan]

%a = trunc i64 %rdx to i32
%b = icmp eq %a, 0
%c = zext i1 a to i64
ret i64 %c

Is the line at %c correct? Isn't it something like : %c = zext i1 %b to i64?

[archercreat]

yea, my bad. The %c = zext i1 %b to i64 is correct.

[JonathanSalwan]

I think this patch could break other things. In fact, if we provide a logical node as input, we should get back a logical node as output. With this patch, we get a bit vector as output. This is why the unit tests fail. I think we should do like a cast when we want to extend an i1 value to something bigger.

What about this patch (those additions are for ZExt and SExt)? Can you try on your side to see if it solves your issue?

diff --git a/src/libtriton/ast/llvm/llvmToTriton.cpp b/src/libtriton/ast/llvm/llvmToTriton.cpp
index c3ad38c7..16894433 100644
--- a/src/libtriton/ast/llvm/llvmToTriton.cpp
+++ b/src/libtriton/ast/llvm/llvmToTriton.cpp
@@ -131,6 +131,12 @@ namespace triton {
             /* Final size */
             auto size = instruction->getType()->getIntegerBitWidth();
             auto node = this->do_convert(instruction->getOperand(0));
+
+            /* Handle the case where node is logical */
+            if (node->isLogical()) {
+              node = this->actx->ite(node, this->actx->bvtrue(), this->actx->bvfalse());
+            }
+
             /* Size of the child */
             auto csze = instruction->getOperand(0)->getType()->getIntegerBitWidth();
             return this->actx->sx(size - csze, node);
@@ -203,6 +209,12 @@ namespace triton {
             /* Final size */
             auto size = instruction->getType()->getIntegerBitWidth();
             auto node = this->do_convert(instruction->getOperand(0));
+
+            /* Handle the case where node is logical */
+            if (node->isLogical()) {
+              node = this->actx->ite(node, this->actx->bvtrue(), this->actx->bvfalse());
+            }
+
             /* Size of the child */
             auto csze = instruction->getOperand(0)->getType()->getIntegerBitWidth();
             return this->actx->zx(size - csze, node);

[archercreat]

The patch solves this issue. I'll update pr to this :)