Missing arithmetic operations in constraints

[ret2dir]

Hi, we tried to execute a simple program with symqemu:

#include <unistd.h>
#include <stdint.h>

static int8_t g_36 = 0;
static uint16_t g_431 = 3;

static int16_t  func_20();

static int32_t  func_1()
{ 
    int32_t l_458 = 4;
    l_458 = func_20(2, g_36 ^ (- 56 * g_431) % (uint32_t)-1L) != (g_431 >> 2 < 2 < 0 && 5);
}

static int16_t  func_20(int32_t  p_21, uint32_t  p_22)
{
    return p_22;
}

int main () {
    read(STDIN_FILENO, &g_36, sizeof(g_36));
    read(STDIN_FILENO, &g_431, sizeof(g_431));
    func_1();
}

However, we found that given the input where g_36 = 0 and g_431 = 0, the generated constraint were different from what we expected:

// command: command: cat test0.input | ./symqemu/build_simple/x86_64-linux-user/symqemu-x86_64 testcase.out
(set-logic QF_AUFBV)
(declare-fun g_431$0 () (_ BitVec 8))
(declare-fun g_431$1 () (_ BitVec 8))
(declare-fun g_36$0 () (_ BitVec 8))
// assert (g_431 >> 2 < 2)
(assert (let ((a!1 (concat ((_ extract 31 0)
                     (bvashr (concat #x0000 g_431$1 g_431$0 #x00000000)
                             #x0000000000000022))
                   #x00000000)))
  (not (bvsle #x0000000000000002 (bvashr a!1 #x0000000000000020)))))
// assert (g_431 >> 2 < 2 >= 0)
(assert (let ((a!1 (concat ((_ extract 31 0)
                     (bvashr (concat #x0000 g_431$1 g_431$0 #x00000000)
                             #x0000000000000022))
                   #x00000000)))
(let ((a!2 (concat #b0000000000000000000000000000000
                   (ite (bvsle #x0000000000000002
                               (bvashr a!1 #x0000000000000020))
                        #b0
                        #b1)
                   #x00000000)))
  (bvsle #x0000000000000000 (bvashr a!2 #x0000000000000020)))))
// cannot understand the following constraints regarding g_36
// no multiplication and modules operations are found
(assert (let ((a!1 (bvashr (concat #xff
                           ((_ extract 7 7) g_36$0)
                           (bvnot ((_ extract 6 6) g_36$0))
                           ((_ extract 5 5) g_36$0)
                           (bvnot ((_ extract 4 3) g_36$0))
                           ((_ extract 2 0) g_36$0)
                           #x000000000000)
                   #x0000000000000030)))
(let ((a!2 ((_ extract 31 0)
             (bvashr (concat ((_ extract 15 0) a!1) #x000000000000)
                     #x0000000000000030))))
  (not (= a!2 #x00000000)))))
(check-sat)
(exit)

For example, we cannot find the corresponding multiplication operation and modulus operation in the constraint. Can you kindly explain why? Is this as expected or a bug?

Further, I logged the result of each cmp instruction. When given the input g_36 = 1 and g_431 = 0, the executable takes exactly the same branches at each cmp instruction, however, the generated constraints are not the same as above.

// command: cat test3.input | ./symqemu/build_simple/x86_64-linux-user/symqemu-x86_64 testcase.out
(set-logic QF_AUFBV)
(declare-fun g_431$0 () (_ BitVec 8))
(declare-fun g_431$1 () (_ BitVec 8))
(declare-fun g_36$0 () (_ BitVec 8))
// assert (g_431 >> 2 < 2)
(assert (let ((a!1 (concat ((_ extract 31 0)
                     (bvashr (concat #x0000 g_431$1 g_431$0 #x00000000)
                             #x0000000000000022))
                   #x00000000)))
  (not (bvsle #x0000000000000002 (bvashr a!1 #x0000000000000020)))))
// assert (g_431 >> 2 < 2 >= 0)
(assert (let ((a!1 (concat ((_ extract 31 0)
                     (bvashr (concat #x0000 g_431$1 g_431$0 #x00000000)
                             #x0000000000000022))
                   #x00000000)))
(let ((a!2 (concat #b0000000000000000000000000000000
                   (ite (bvsle #x0000000000000002
                               (bvashr a!1 #x0000000000000020))
                        #b0
                        #b1)
                   #x00000000)))
  (bvsle #x0000000000000000 (bvashr a!2 #x0000000000000020)))))
// not the same as above, even always take the same branch
(assert (let ((a!1 (concat ((_ extract 15 0)
                     (bvashr (concat #x00 g_36$0 #x000000000000)
                             #x0000000000000030))
                   #x000000000000)))
  (not (= ((_ extract 31 0) (bvashr a!1 #x0000000000000030)) #x00000000))))
(check-sat)
(exit)

I'm wondering if symqemu mis-handles the multiplication operation and modulus operation.

The source code is compiled with clang-10 with option -O0. The compiled executable file and inputs to generated the above constraints are attached. output-186.zip

Thanks.