Improper shift left overflow handling

[ret2dir]

Dear developers,

Recently, when I ran symcc on the following program, trying to explore the two paths given the input g_617 = 32, symcc cannot successfully finds the case where if condition is false, and always fall into the case where if condition is true.

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

static uint16_t g_617;

static const uint8_t  func_1() {
    if (g_617 < 0 != 6 << g_617) {
        printf("test\n");   
    }
}
int  main () { 
    read(STDIN_FILENO, &g_617, sizeof(g_617));
    func_1();
}

I have investigated the reason. The Intel processor masks the shift count to 5 bits to make sure that the shift left count is at most 31. Therefore, the if condition will be false only when g_617 mod 32 = 31. If we provide initial input g_617 = 32, symcc will capture the result of if condition is true and trying to solve the following constraint to make the if condition be false.

Trying to solve:
(declare-fun stdin0 () (_ BitVec 8))
(declare-fun stdin1 () (_ BitVec 8))
(assert (= (ite (bvsle #x00000000 (concat #x0000 stdin1 stdin0)) #x00000000 #x00000001)
   (bvshl #x00000006 (concat #x0000 stdin1 stdin0))))

Found diverging input:
stdin0 -> #x01
stdin1 -> #x40

This constraint uses bvshl to perform shift left operation that corresponds to the if condition. However, when g_617 > 31, bvshl will compute the result as 0 (without mod 32 operation), which will satisfy the above constraint. In that case, symcc will generate an new input g_617 = 0x4001, which in fact, let the if the condition still be true in concrete execution.

The reason is the inconsistent handling for left shift overflow between shl opcode in machine code and bvshl in smt constraint. I'm wondering if symcc has been aware of such difference so that it can add an extra mod 32 operation for the left shift when collecting constraints.

This shift left overflow handling problem also exists in the qsym backend, and the generated constraints is shown as below:

(set-info :status unknown)
(declare-fun k!00 () (_ BitVec 8))
(declare-fun k!10 () (_ BitVec 8))
(assert
 (let ((?x15 (concat (_ bv0 16) k!10 k!00)))
 (let ((?x20 (bvshl (_ bv6 32) ?x15)))
 (let ((?x18 (ite (bvsle (_ bv0 32) ?x15) (_ bv0 32) (_ bv1 32))))
 (= ?x18 ?x20)))))
(check-sat)

Thank you.