Assertion Failed in qsym/pintool/solver.cpp

[xupeng1231]

You may know, Symcc use qsym as a backend to realize symbolic execution. Particularly, it utilize the pintool code of qsym.

When I use Symcc to fuzz some software, it always crash in qsym's pintool code.

The crash point is as below. https://github.com/sslab-gatech/qsym/blob/4b7fa3c93d341a015c015fe33b2818160401474e/qsym/pintool/solver.cpp#L173

At crash point, it assert that the Expr e is relational. However, in our failure case, thee->kind() value is 4(Extract, not in the Relational range), so the assertion failed.

Could you please help give some information and solve this problem. Is it reasonable that the Extract kind Expr is used in void Solver::addJcc(ExprRef e, bool taken, ADDRINT pc).

void Solver::addJcc(ExprRef e, bool taken, ADDRINT pc) {
  // Save the last instruction pointer for debugging
  last_pc_ = pc;

  if (e->isConcrete())
    return;

  // if e == Bool(true), then ignore
  if (e->kind() == Bool) {
    assert(!(castAs<BoolExpr>(e)->value()  ^ taken));
    return;
  }

  assert(isRelational(e.get()));

bool isRelational(const Expr* e) {
  switch (e->kind()) {
    case Distinct:
    case Equal:
    case Ult:
    case Ule:
    case Ugt:
    case Uge:
    case Slt:
    case Sle:
    case Sgt:
    case Sge:
    case LAnd:
    case LOr:
    case LNot:
      return true;
    default:
      return false;
  }
}

enum Kind {
  Bool, // 0
  Constant, // 1
  Read, // 2
  Concat, // 3
  Extract, // 4

  ZExt, // 5
  SExt, // 6

The following is the back trace of the assertion failure case:

[****] e->kind():4
jasper: /home/sentosa/test/symcc/runtime/qsym_backend/qsym/qsym/pintool/solver.cpp:175: void qsym::Solver::addJcc(qsym::ExprRef, bool, ADDRINT): Assertion `isRelational(e.get())' failed.
--Type <RET> for more, q to quit, c to continue without paging--

Thread 1 "jasper" received signal SIGABRT, Aborted.
__GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:50
50	../sysdeps/unix/sysv/linux/raise.c: No such file or directory.
(gdb) bt
#0  __GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:50
#1  0x00007ffff79c8859 in __GI_abort () at abort.c:79
#2  0x00007ffff79c8729 in __assert_fail_base (fmt=0x7ffff7b5e588 "%s%s%s:%u: %s%sAssertion `%s' failed.\n%n", 
    assertion=0x7ffff7dd19b6 "isRelational(e.get())", 
    file=0x7ffff7dd1898 "/home/sentosa/test/symcc/runtime/qsym_backend/qsym/qsym/pintool/solver.cpp", line=175, 
    function=<optimized out>) at assert.c:92
#3  0x00007ffff79d9fd6 in __GI___assert_fail (assertion=0x7ffff7dd19b6 "isRelational(e.get())", 
    file=0x7ffff7dd1898 "/home/sentosa/test/symcc/runtime/qsym_backend/qsym/qsym/pintool/solver.cpp", line=175, 
    function=0x7ffff7dd1940 "void qsym::Solver::addJcc(qsym::ExprRef, bool, ADDRINT)") at assert.c:101
#4  0x00007ffff7d1ea75 in qsym::Solver::addJcc(std::shared_ptr<qsym::Expr>, bool, unsigned long) ()
   from /home/sentosa/test/symcc/SymRuntime-prefix/src/SymRuntime-build/libSymRuntime.so
#5  0x00007ffff7d40d3e in _sym_push_path_constraint ()
   from /home/sentosa/test/symcc/SymRuntime-prefix/src/SymRuntime-build/libSymRuntime.so
#6  0x00000000005531b7 in jas_stream_copy ()
#7  0x00000000008e0144 in jp2_box_get ()
#8  0x0000000000589e41 in jp2_decode ()
#9  0x00000000004be292 in jas_image_decode ()
#10 0x0000000000408e30 in main ()
(gdb) 

Thanks.

[insuyun]

Hi, @xupeng1231. It seems like constraint generation is done by SymCC. So I believe that SymCC has some issues (maybe they don't wrap a Extract constraint with boolean?)