I got an error when compiling symqume, and I searched google but no luck. Thanks!

make[1]: Leaving directory '/home/ubuntu/sym/symqume/symqemu/slirp' LEX convert-dtsv0-lexer.lex.c make[1]: flex: Command not found BISON dtc-parser.tab.c make[1]: bison: Command not found LEX dtc-lexer.lex.c make[1]: flex: Command not found CC alpha-softmmu/tcg/tcg.o In file included from /usr/include/sched.h:29:0, from /usr/include/pthread.h:23, from /usr/include/glib-2.0/glib/deprecated/gthread.h:128, from /usr/include/glib-2.0/glib.h:108, from /home/ubuntu/sym/symqume/symqemu/include/glib-compat.h:32, from /home/ubuntu/sym/symqume/symqemu/include/qemu/osdep.h:140, from /home/ubuntu/sym/symqume/symqemu/tcg/tcg.c:28: /home/ubuntu/sym/symqume/symqemu/tcg/tcg.c: In function ‘tcg_context_init’: /home/ubuntu/sym/symqume/symqemu/tcg/tcg.c:1000:9: error: ‘ArchCPU {aka struct AlphaCPU}’ has no member named ‘env_exprs’ offsetof(ArchCPU, env_exprs) - offsetof(ArchCPU, env), "env"); ^ /home/ubuntu/sym/symqume/symqemu/rules.mak:69: recipe for target 'tcg/tcg.o' failed

This small set of bugfixes improves compatibility with 32-bit architectures, especially MIPS.

• Fixed symbolic load not working for some 32-bit arch
• Backported a bugfix for a deprecated syscall usage
• Added env symbolic expressions in MIPS CPU

Note about symbolic load : When tcg_gen_qemu_ld_i32 is invoked during translation, the addr and val (ret) operands are getting simplified/folded into one TCG variable after the concrete operation. Thus, this prevents the later symbolic operation from retrieving the correct address value. It has probably something to do with the optimization feature of QEMU and the way a given target CPU (TCG frontend) invokes tcg_gen_qemu_ld_i32 (use of TCG temporaries, constants). A tiny bugfix is proposed before finding the actual root cause.

I'm currently reading the source code of symqemu to understand how it works by printing some information about the instrumented symbolic expressions.

// In accel/tcg/tcg-runtime-sym.c
// Here I try to print arg1_expr and arg2_expr
static void *sym_setcond_internal(CPUArchState *env,
                                  uint64_t arg1, void *arg1_expr,
                                  uint64_t arg2, void *arg2_expr,
                                  int32_t cond, uint64_t result,
                                  uint8_t result_bits)
{
    printf("[debug] In Runtime: pc:0x%lx,expr1:%p,expr2:%p\n",get_pc(env),arg1_expr,arg2_expr);
    BINARY_HELPER_ENSURE_EXPRESSIONS;
    printf("[debug] calling sym_setcond_internal...success!\n");
    printf("[debug] After ensure_expr: expr1:%p,expr2:%p\n",arg1_expr,arg2_expr);
    printf("arg1 expr:%s\n",_sym_expr_to_string(arg1_expr));
    printf("arg2 expr:%s\n",_sym_expr_to_string(arg2_expr));
...

However, when I run the modified symqemu on arbitrary binary, I noticed there are lots of nil pointers:

I wonder why would that happen? What does it mean when a sym_expr is nil? Does it mean that symqemu fails to build symbolic expressions for some variables in tcg ir?

Hi; it looks like you've licensed the new files you've added as GPL-v3-or-later (eg accel/tcg/tcg-runtime-sym.c). Unfortunately the GPLv3 is not compatible with the GPLv2, and some existing parts of QEMU are licensed as GPLv2-only (not v2-or-later) (eg util/qemu-sockets.c).

I'm guessing this was unintentional -- the easiest fix would be for you to relicense the code you've added as GPL-v2-or-later.

I follow the README but compilation fails:

$ cd /
$ git clone --depth=1 https://github.com/eurecom-s3/symcc
$ cd symcc
$ git submodule update --init && mkdir build && cd build
$  cmake -G Ninja -DQSYM_BACKEND=ON -DZ3_TRUST_SYSTEM_VERSION=on ..
$  ninja
$ cargo install --path util/symcc_fuzzing_helper
[this all succeeds]

$ git clone --depth=1 https://github.com/eurecom-s3/symqemu
$ cd symqemu
$ ./configure --audio-drv-list= --disable-bluez --disable-sdl --disable-gtk --disable-vte --disable-opengl --disable-virglrenderer --target-list=x86_64-linux-user --disable-werror --enable-capstone=git --symcc-source=/symcc/ --symcc-build=/symcc/build
[...]
$ make
[...]
  CC      x86_64-linux-user/trace/control-target.o
  CC      x86_64-linux-user/gdbstub-xml.o
  CC      x86_64-linux-user/trace/generated-helpers.o
  LINK    x86_64-linux-user/symqemu-x86_64
/usr/bin/ld: accel/tcg/tcg-runtime-sym.o: in function `sym_setcond_internal':
/symcc/symqemu/accel/tcg/tcg-runtime-sym.c:618: undefined reference to `_sym_build_bool_to_bits'
collect2: error: ld returned 1 exit status
make[1]: *** [Makefile:209: symqemu-x86_64] Error 1
make: *** [Makefile:472: x86_64-linux-user/all] Error 2

We found that the movsx assembly instruction is not correctly translated by syqemu. More specifically, the movsx istruction copies the contents of the source operand to the destination operand with sign extension, however, the translated tcg ops conduct a zero extension, as shown below:

// g_26 is an int8_t variable 
// the value of g_26 is 0xae
0x40126D: movsx   r9d, g_26
// will be translated into -->
 ---- 000000000040126d 0000000000000018
 movi_i64 tmp2_expr,$0x0
 movi_i64 tmp2,$0x404044
 qemu_ld_i64 tmp0,tmp2,sb,0
 movi_i64 tmp12_expr,$0x0
 movi_i64 tmp12,$0x0
 movi_i64 tmp13_expr,$0x0
 movi_i64 tmp13,$0x1
 call sym_load_guest_i64,$0x1,$1,tmp0_expr,env,tmp2,tmp2_expr,tmp13,tmp12
 movi_i64 tmp12_expr,$0x0
 movi_i64 tmp12,$0x4
 call sym_zext,$0x5,$1,r9_expr,tmp0_expr,tmp12
 ext32u_i64 r9,tmp0

The sym_zext and ext32u_i64 at the end is inconsitent with the semantic of movsx instruction and could lead to inaccurate symbolic constraints.

After cheking the source code of symqemu, we found that the sym_load_guest_internal function does not distinguish between the signed value and the unsigned value and it will zero extend the loaded value whenever the load_length is not equal to result_length. This behavior is unusual and potentially buggy.

We found a possible bug while using symqemu to execute following program:

#include <unistd.h>
#include "csmith.h"
/* --- GLOBAL VARIABLES --- */
static uint16_t g_5[4] = {2,2,6,2};
static int16_t g_81 = 5;
static int32_t g_318 = 6;
/* --- FORWARD DECLARATIONS --- */
static uint32_t  func_1();
static uint8_t  func_2(int16_t  p_3, uint16_t  p_4);

static uint32_t  func_1()
{ /* block id 0 */
    int32_t *l_317 = &g_318;
    *l_317 = func_2(g_5, g_5[3]) != 0;
}
static uint8_t  func_2(int16_t  p_3, uint16_t  p_4)
{ /* block id 1 */
    if (g_5[3])
    { /* block id 3 */
        int32_t l_152[7][2] ;
        l_152[6][0] = 0 > (5 % (0 , p_4) != g_81);
    }
}
/* 
 */
void  main ()
{
    read(STDIN_FILENO, &g_5, sizeof(g_5));
    read(STDIN_FILENO, &g_81, sizeof(g_81));
    read(STDIN_FILENO, &g_318, sizeof(g_318));
    int print_hash_value = 0;
    func_1();
    exit(0);
}

If we compile this code with clang-10, the % operation at line 21 will be trasnlated into idiv assembly instruction.

.text:0000000000401210 55                                      push    rbp
.text:0000000000401211 48 89 E5                                mov     rbp, rsp
.text:0000000000401214 66 89 7D FC                             mov     [rbp+var_4], di
.text:0000000000401218 66 89 75 FA                             mov     [rbp+var_6], si
.text:000000000040121C 66 83 3C 25 3E 40 40 00+                cmp     word_40403E, 0
.text:0000000000401225 0F 84 3D 00 00 00                       jz      loc_401268
.text:000000000040122B 31 C0                                   xor     eax, eax
.text:000000000040122D 0F B7 4D FA                             movzx   ecx, [rbp+var_6]
.text:0000000000401231 BA 05 00 00 00                          mov     edx, 5
.text:0000000000401236 89 45 BC                                mov     [rbp+var_44], eax
.text:0000000000401239 89 D0                                   mov     eax, edx
.text:000000000040123B 99                                      cdq
.text:000000000040123C F7 F9                                   idiv    ecx
.text:000000000040123E 0F BF 0C 25 40 40 40 00                 movsx   ecx, g_81
.text:0000000000401246 39 CA                                   cmp     edx, ecx
.text:0000000000401248 40 0F 95 C6                             setnz   sil
.text:000000000040124C 40 80 E6 01                             and     sil, 1
.text:0000000000401250 40 0F B6 CE                             movzx   ecx, sil
.text:0000000000401254 8B 55 BC                                mov     edx, [rbp+var_44]
.text:0000000000401257 39 CA                                   cmp     edx, ecx
.text:0000000000401259 40 0F 9F C6                             setnle  sil
.text:000000000040125D 40 80 E6 01                             and     sil, 1
.text:0000000000401261 40 0F B6 CE                             movzx   ecx, sil
.text:0000000000401265 89 4D F0                                mov     [rbp+var_10], ecx

However, we noticed that the idiv instruction will be translated into a function call to idivl_EAX by QEMU (see the translation), and this kind of translation is not handled by symqemu, i.e., the divisor and dividend are treated as concrete values, the tcg_gen_div_i32 function defined at tcg-op.c is not used.

For example, the above idiv ecx instruction will be converted to following tcg ops by symqemu:

...

---- 000000000040123b 0000000000000031
 movi_i64 tmp12,$0x4                      pref=0x40
 call sym_sext,$0x5,$1,tmp0_expr,rax_expr,tmp12  dead: 1 2  pref=none
 movi_i64 tmp12_expr,$0x0                 pref=0x2
 movi_i64 tmp12,$0x1f                     pref=0x4
 call sym_arithmetic_shift_right_i64,$0x5,$1,tmp0_expr,rdx,tmp0_expr,tmp12,tmp12_expr  dead: 1 2 3 4  pref=none
 movi_i64 tmp12,$0x4                      pref=0x40
 call sym_zext,$0x5,$1,rdx_expr,tmp0_expr,tmp12  sync: 0  dead: 0 1 2  pref=none
 movi_i64 rdx,$0x0                        sync: 0  dead: 0  pref=0xffff

 ---- 000000000040123c 0000000000000031
 call idivl_EAX,$0x0,$0,env,rcx           dead: 0 1

 ---- 000000000040123e 0000000000000031
 movi_i64 tmp2_expr,$0x0                  pref=0xf038
 movi_i64 tmp2,$0x404040                  pref=0xf038
 qemu_ld_i64 tmp0,tmp2,lesw,0             pref=0xf038
 movi_i64 tmp12,$0x0                      pref=0x100
 movi_i64 tmp13,$0x2                      pref=0x2
 call sym_load_guest_i64,$0x1,$1,tmp0_expr,env,tmp2,tmp2_expr,tmp13,tmp12  dead: 2 3 4 5  pref=none
 movi_i64 tmp12,$0x4                      pref=0x40
 call sym_zext,$0x5,$1,rcx_expr,tmp0_expr,tmp12  dead: 1 2  pref=none
 ext32u_i64 rcx,tmp0                      dead: 1  pref=0xf03c

 ...

The rdx will be updated by idivl_EAX, but the rdx_expr is not updated, so the symbolic chain is broken, and some variables become constant in constraints generated by symqemu.

The same issue exists for the div instruction.

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.

Hi,

I noticed that when invoking get_pc(env) at sym_setcond_internal. The result of get_pc(env) is the old pc from the previous tb. I tried to update. Could you help me to verify my fix at https://github.com/sgzeng/symqemu/commit/405f4329f51ffe8a88fc2e8b5306a8572ec089dc Thanks!