From e450b43a318890ae4ac823577743ead625fd4c24 Mon Sep 17 00:00:00 2001
From: Sebastian Poeplau <sebastian.poeplau@eurecom.fr>
Date: Wed, 20 Mar 2019 12:14:05 +0100
Subject: [PATCH] Log the number of instructions that trigger symbolic
 computation

---
 qsym/pintool/instrument.cpp | 145 +++++++++++++++++++++++++++++++++++-
 qsym/pintool/main.cpp       |   9 +++
 2 files changed, 150 insertions(+), 4 deletions(-)

diff --git a/qsym/pintool/instrument.cpp b/qsym/pintool/instrument.cpp
index a11a954..5c178ee 100644
--- a/qsym/pintool/instrument.cpp
+++ b/qsym/pintool/instrument.cpp
@@ -1,3 +1,4 @@
+#include <atomic>
 #include <cassert>
 #include "thread_context.h"
 #include "instrument.h"
@@ -8,6 +9,8 @@
 // bit position
 namespace qsym {
 
+  std::atomic<uint64_t> g_symbolic_instructions{0};
+
 void instrumentBBL(
     ThreadContext *thread_ctx,
     const CONTEXT* ctx) {
@@ -646,6 +649,7 @@ instrumentShiftRegImm(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doShift(thread_ctx, kind, op_kind, expr_dst, expr_src, bits);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -672,6 +676,7 @@ instrumentShiftRegCl(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doShift(thread_ctx, kind, op_kind, expr_dst, expr_src, bits);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -699,6 +704,7 @@ instrumentShiftMemImm(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doShift(thread_ctx, kind, op_kind, expr_dst, expr_src, bits);
   g_memory.setExprToMem(addr, size, expr_res);
 }
@@ -725,6 +731,7 @@ instrumentShiftMemCl(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doShift(thread_ctx, kind, op_kind, expr_dst, expr_src, bits);
   g_memory.setExprToMem(addr, size, expr_res);
 }
@@ -784,6 +791,7 @@ instrumentShiftdRegRegImm(
       return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doShiftd(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_imm, bits);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -814,6 +822,7 @@ instrumentShiftdRegRegCl(
       return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doShiftd(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_imm, bits);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -845,6 +854,7 @@ instrumentShiftdMemRegImm(
       return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doShiftd(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_imm, bits);
   g_memory.setExprToMem(addr, size, expr_res);
 }
@@ -875,6 +885,7 @@ instrumentShiftdMemRegCl(
       return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doShiftd(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_imm, bits);
   g_memory.setExprToMem(addr, size, expr_res);
 }
@@ -930,6 +941,7 @@ instrumentBinaryRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doBinary(thread_ctx, kind, op_kind, expr_dst, expr_src);
   if (write)
     thread_ctx->setExprToReg(dst, expr_res);
@@ -958,6 +970,7 @@ instrumentBinaryRegImm(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doBinary(thread_ctx, kind, op_kind, expr_dst, expr_src);
   if (write)
     thread_ctx->setExprToReg(dst, expr_res);
@@ -986,6 +999,7 @@ instrumentBinaryRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doBinary(thread_ctx, kind, op_kind, expr_dst, expr_src);
   if (write)
     thread_ctx->setExprToReg(dst, expr_res);
@@ -1014,6 +1028,7 @@ instrumentBinaryMemReg(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doBinary(thread_ctx, kind, op_kind, expr_dst, expr_src);
   if (write)
     g_memory.setExprToMem(addr, size, expr_res);
@@ -1042,6 +1057,7 @@ instrumentBinaryMemImm(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doBinary(thread_ctx, kind, op_kind, expr_dst, expr_src);
   if (write)
     g_memory.setExprToMem(addr, size, expr_res);
@@ -1086,6 +1102,7 @@ instrumentCarryRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doCarry(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_cf);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -1115,6 +1132,7 @@ instrumentCarryRegImm(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doCarry(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_cf);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -1144,6 +1162,7 @@ instrumentCarryRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doCarry(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_cf);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -1173,6 +1192,7 @@ instrumentCarryMemReg(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doCarry(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_cf);
   g_memory.setExprToMem(addr, size, expr_res);
 }
@@ -1202,6 +1222,7 @@ instrumentCarryMemImm(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doCarry(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_cf);
   g_memory.setExprToMem(addr, size, expr_res);
 }
@@ -1230,6 +1251,7 @@ instrumentCbw(ThreadContext* thread_ctx,
     return;
   }
 
+  g_symbolic_instructions++;
   expr_to = g_expr_builder->createSExt(expr_from, bits);
   thread_ctx->setExprToReg(to, expr_to);
 }
@@ -1247,6 +1269,7 @@ instrumentCwd(ThreadContext* thread_ctx,
     return;
   }
 
+  g_symbolic_instructions++;
   expr_dx = g_expr_builder->createSExt(expr_ax, bits * 2);
   expr_dx = g_expr_builder->createExtract(expr_dx, bits, bits);
   thread_ctx->setExprToReg(dx, expr_dx);
@@ -1325,6 +1348,7 @@ instrumentBsRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   doBs(thread_ctx, dst, expr_src, inv);
 }
 
@@ -1344,6 +1368,7 @@ instrumentBsRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   doBs(thread_ctx, dst, expr_src, inv);
 }
 
@@ -1357,6 +1382,7 @@ instrumentBswapReg(ThreadContext* thread_ctx, const CONTEXT* ctx,
     for (UINT32 i = 0; i < expr_dst->bits() / CHAR_BIT; i++)
       exprs.push_back(g_expr_builder->createExtract(expr_dst, i * CHAR_BIT, CHAR_BIT));
 
+    g_symbolic_instructions++;
     ExprRef expr_res = g_expr_builder->createConcat(exprs);
     thread_ctx->setExprToReg(dst, expr_res);
   }
@@ -1408,6 +1434,7 @@ instrumentBtRegReg(ThreadContext* thread_ctx, const CONTEXT* ctx,
     return;
   }
 
+  g_symbolic_instructions++;
   expr_dst = doBt(thread_ctx, expr_dst, getRegValue(ctx, src).getZExtValue(),
                   bits, kind);
 
@@ -1427,6 +1454,7 @@ instrumentBtRegImm(ThreadContext* thread_ctx,
     return;
   }
 
+  g_symbolic_instructions++;
   expr_dst = doBt(thread_ctx, expr_dst, imm, REG_Size(dst) * CHAR_BIT, kind);
 
   if (kind != Invalid) {
@@ -1451,6 +1479,7 @@ instrumentBtMemReg(ThreadContext* thread_ctx,
     return;
   }
 
+  g_symbolic_instructions++;
   expr_dst = doBt(thread_ctx, expr_dst, imm, bits, kind);
 
   if (kind != Invalid) {
@@ -1470,6 +1499,7 @@ instrumentBtMemImm(ThreadContext* thread_ctx,
     return;
   }
 
+  g_symbolic_instructions++;
   expr_dst = doBt(thread_ctx, expr_dst, imm, bits, kind);
 
   if (kind != Invalid) {
@@ -1535,6 +1565,7 @@ instrumentCmps(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = g_expr_builder->createBinaryExpr(Sub, expr_dst, expr_src);
   thread_ctx->setEflags(CC_OP_SUB, expr_res, expr_dst, expr_src);
 }
@@ -1557,6 +1588,7 @@ instrumentCmpxchgRegReg(ThreadContext* thread_ctx,
     return;
   }
 
+  g_symbolic_instructions++;
   llvm::APInt val_dst = getRegValue(ctx, dst);
   llvm::APInt val_ax = getRegValue(ctx, ax);
 
@@ -1593,6 +1625,7 @@ instrumentCmpxchgMemReg(ThreadContext* thread_ctx,
     return;
   }
 
+  g_symbolic_instructions++;
   llvm::APInt val_dst = getMemValue(addr, size);
   llvm::APInt val_ax = getRegValue(ctx, ax);
 
@@ -1621,6 +1654,8 @@ instrumentCpuid(ThreadContext* thread_ctx, CONTEXT* ctx) {
   thread_ctx->clearExprFromReg(REG_ECX);
   thread_ctx->clearExprFromReg(REG_EDX);
 
+  g_symbolic_instructions++;
+
   // Set 'FAKE' cpuid to prevent that glibc uses optimized libraries
   PIN_SetContextReg(ctx, REG_GBX, 0x46414b45);
   PIN_ExecuteAt(ctx);
@@ -1645,6 +1680,7 @@ doIncDec(ThreadContext* thread_ctx, ExprRef expr_dst, Kind kind, OpKind op_kind)
     return NULL;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_src = g_expr_builder->createConstant(1, expr_dst->bits());
   ExprRef expr_res = g_expr_builder->createBinaryExpr(kind, expr_dst, expr_src);
   thread_ctx->setEflags(op_kind, expr_res, expr_dst, expr_src);
@@ -1738,6 +1774,7 @@ instrumentDivReg(
       &expr_reg_h))
     return;
 
+  g_symbolic_instructions++;
   ExprRef expr_div = g_expr_builder->createConcat(expr_reg_h, expr_reg_l);
   doDiv(thread_ctx, reg_h, reg_l, expr_src, expr_div, sign);
 }
@@ -1769,6 +1806,7 @@ instrumentDivMem(
       &expr_reg_h))
     return;
 
+  g_symbolic_instructions++;
   ExprRef expr_div = g_expr_builder->createConcat(expr_reg_h, expr_reg_l);
   doDiv(thread_ctx, reg_h, reg_l, expr_src, expr_div, sign);
 }
@@ -1799,6 +1837,7 @@ instrumentMulReg(
     return;
   }
 
+  g_symbolic_instructions++;
   doMul(thread_ctx, ctx, reg_l, reg_h, expr_src, expr_reg_l, bits, sign);
 }
 
@@ -1828,6 +1867,7 @@ instrumentMulMem(
     return;
   }
 
+  g_symbolic_instructions++;
   doMul(thread_ctx, ctx, reg_l, reg_h, expr_src, expr_reg_l, bits, sign);
 }
 
@@ -1900,6 +1940,7 @@ instrumentIMulRegRegImm(
     return;
   }
 
+  g_symbolic_instructions++;
   doMul(thread_ctx, expr_src, expr_imm, dst);
 }
 
@@ -1925,6 +1966,7 @@ instrumentIMulRegMemImm(
     return;
   }
 
+  g_symbolic_instructions++;
   doMul(thread_ctx, expr_src, expr_imm, dst);
 }
 
@@ -1933,6 +1975,7 @@ instrumentLeaRegMem(ThreadContext* thread_ctx,
     const CONTEXT* ctx,
     REG dst,
     REG base, REG index, ADDRINT disp, UINT32 scale) {
+  g_symbolic_instructions++;
   ExprRef e = thread_ctx->getAddrExpr(ctx, base, index, disp, scale);
   thread_ctx->setExprToReg(dst, e);
 }
@@ -1958,6 +2001,7 @@ instrumentMovRegReg(
     const CONTEXT* ctx,
     REG dst,
     REG src) {
+  g_symbolic_instructions++;
   doMovRegReg(thread_ctx, ctx, dst, src, 0, 0, REG_Size(dst));
 }
 
@@ -1988,6 +2032,7 @@ instrumentMovRegMem(
     const CONTEXT* ctx,
     REG dst,
     MEM_ARG) {
+  g_symbolic_instructions++;
   doMovRegMem(thread_ctx, ctx, dst,
     base, index, addr, size, disp, scale, 0);
 }
@@ -1996,6 +2041,7 @@ void PIN_FAST_ANALYSIS_CALL
 instrumentMovMemImm(ThreadContext *thread_ctx, const CONTEXT* ctx,
     MEM_ARG,
     ADDRINT imm) {
+  g_symbolic_instructions++;
   makeAddrConcrete(thread_ctx, ctx, base, index, addr, size, disp, scale);
   g_memory.clearExprFromMem(addr, size);
 }
@@ -2019,6 +2065,7 @@ void PIN_FAST_ANALYSIS_CALL
 instrumentMovMemReg(ThreadContext *thread_ctx, const CONTEXT* ctx,
     MEM_ARG,
     REG src) {
+  g_symbolic_instructions++;
   doMovMemReg(thread_ctx, ctx,
       base, index, addr, size, disp, scale,
       src, 0);
@@ -2031,6 +2078,7 @@ instrumentMovhRegMem(
     REG dst,
     MEM_ARG) {
   QSYM_ASSERT(REG_Size(dst) == 16);
+  g_symbolic_instructions++;
   doMovRegMem(thread_ctx, ctx, dst,
     base, index, addr, size, disp, scale,
     8);
@@ -2043,6 +2091,7 @@ instrumentMovhMemReg(
     MEM_ARG,
     REG src) {
   QSYM_ASSERT(REG_Size(src) == 16);
+  g_symbolic_instructions++;
   doMovMemReg(thread_ctx, ctx,
     base, index, addr, size, disp, scale,
     src, 8);
@@ -2056,6 +2105,7 @@ instrumentMovlzRegReg(
     REG src,
     UINT width) {
   UINT size = REG_Size(src);
+  g_symbolic_instructions++;
   doMovRegReg(thread_ctx, ctx, dst, src, 0, 0, width);
   thread_ctx->clearExprFromReg(dst, size, REG_Size(dst) - size);
 }
@@ -2067,6 +2117,7 @@ instrumentMovlzRegMem(
     REG dst,
     MEM_ARG,
     UINT width) {
+  g_symbolic_instructions++;
   doMovRegMem(thread_ctx, ctx, dst,
                 base, index, addr, size, disp, scale, 0);
   QSYM_ASSERT(REG_Size(dst) >= size);
@@ -2080,6 +2131,7 @@ instrumentMovlzMemReg(
     MEM_ARG,
     REG src,
     UINT width) {
+  g_symbolic_instructions++;
   doMovMemReg(thread_ctx, ctx,
       base, index, addr, size, disp, scale,
       src, 0);
@@ -2096,6 +2148,7 @@ instrumentMovs(
   concretizeReg(thread_ctx, ctx, REG_GSI);
   concretizeReg(thread_ctx, ctx, REG_GDI);
 
+  g_symbolic_instructions++;
   for (UINT32 i = 0; i < size; i++) {
     ExprRef e = g_memory.getExprFromMemAlways(src_addr + i);
     g_memory.setExprToMem(dst_addr + i, e);
@@ -2109,8 +2162,10 @@ instrumentMovsxRegMem(ThreadContext *thread_ctx,
     MEM_ARG) {
   // TODO: merge with movzx
   ExprRef e = getExprFromMemSrc(thread_ctx, ctx, base, index, addr, size, disp, scale);
-  if (e != NULL)
+  if (e != NULL) {
     e = g_expr_builder->createSExt(e, REG_Size(dst) * 8);
+    g_symbolic_instructions++;
+  }
   thread_ctx->setExprToReg(dst, e);
 }
 
@@ -2119,8 +2174,10 @@ instrumentMovsxRegReg(ThreadContext* thread_ctx,
   const CONTEXT* ctx,
   REG dst, REG src) {
   ExprRef e = thread_ctx->getExprFromReg(ctx, src);
-  if (e != NULL)
+  if (e != NULL){
     e = g_expr_builder->createSExt(e, REG_Size(dst) * 8);
+    g_symbolic_instructions++;
+  }
   thread_ctx->setExprToReg(dst, e);
 }
 
@@ -2130,8 +2187,10 @@ instrumentMovzxRegMem(ThreadContext *thread_ctx,
     REG dst,
     MEM_ARG) {
   ExprRef e = getExprFromMemSrc(thread_ctx, ctx, base, index, addr, size, disp, scale);
-  if (e != NULL)
+  if (e != NULL) {
     e = g_expr_builder->createZExt(e, REG_Size(dst) * 8);
+    g_symbolic_instructions++;
+  }
   thread_ctx->setExprToReg(dst, e);
 }
 
@@ -2140,8 +2199,10 @@ instrumentMovzxRegReg(ThreadContext* thread_ctx,
   const CONTEXT* ctx,
   REG dst, REG src) {
   ExprRef e = thread_ctx->getExprFromReg(ctx, src);
-  if (e != NULL)
+  if (e != NULL) {
     e = g_expr_builder->createZExt(e, REG_Size(dst) * 8);
+    g_symbolic_instructions++;
+  }
   thread_ctx->setExprToReg(dst, e);
 }
 
@@ -2171,6 +2232,7 @@ doNegNot(ThreadContext* thread_ctx, ExprRef expr_dst, Kind kind) {
     return NULL;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = g_expr_builder->createUnaryExpr(kind, expr_dst);
   thread_ctx->setEflags(CC_OP_LOGIC, expr_res, expr_dst, NULL);
   return expr_res;
@@ -2210,6 +2272,7 @@ instrumentJcc(ThreadContext* thread_ctx,
     JccKind jcc_c, bool inv) {
   ExprRef e = thread_ctx->computeJcc(ctx, jcc_c, inv);
   if (e) {
+    g_symbolic_instructions++;
     ADDRINT pc = PIN_GetContextReg(ctx, REG_INST_PTR);
     LOG_DEBUG("Symbolic branch at " + hexstr(pc) + ": " + e->toString() + "\n");
 #ifdef CONFIG_TRACE
@@ -2223,6 +2286,7 @@ void PIN_FAST_ANALYSIS_CALL
 instrumentJmpReg(ThreadContext* thread_ctx, const CONTEXT* ctx, REG r) {
   ExprRef e = thread_ctx->getExprFromReg(ctx, r);
   if (e != NULL) {
+    g_symbolic_instructions++;
     LOG_DEBUG("Symbolic jmp: " + e->toString() + "\n");
     llvm::APInt val = getRegValue(ctx, r);
     g_solver->solveAll(e, val);
@@ -2234,6 +2298,7 @@ void PIN_FAST_ANALYSIS_CALL
 instrumentJmpMem(ThreadContext* thread_ctx, const CONTEXT* ctx, MEM_ARG) {
   ExprRef e = g_memory.getExprFromMem(addr, size);
   if (e != NULL) {
+    g_symbolic_instructions++;
     LOG_DEBUG("Symbolic jmp: " + e->toString() + "\n");
     llvm::APInt val = getMemValue(addr, size);
     g_solver->solveAll(e, val);
@@ -2338,6 +2403,7 @@ instrumentPackRegReg(
         &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPack(thread_ctx, dst, expr_dst, expr_src,
       width, sign);
 }
@@ -2362,6 +2428,7 @@ instrumentPackRegMem(
         &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPack(thread_ctx, dst, expr_dst, expr_src,
       width, sign);
 }
@@ -2376,6 +2443,7 @@ instrumentPalignrReg(ThreadContext* thread_ctx, const CONTEXT* ctx,
   if (expr_src == NULL && expr_dst == NULL)
     return ;
 
+  g_symbolic_instructions++;
   fixRegExpr(&expr_src, ctx, src);
   fixRegExpr(&expr_dst, ctx, dst);
 
@@ -2398,6 +2466,7 @@ instrumentPalignrMem(ThreadContext* thread_ctx, const CONTEXT* ctx,
   if (expr_src == NULL && expr_dst == NULL)
     return;
 
+  g_symbolic_instructions++;
   fixMemExpr(&expr_src, addr, size);
   fixRegExpr(&expr_dst, ctx, dst);
 
@@ -2448,6 +2517,7 @@ instrumentParithRegReg(
   if (!getExprFromRegReg(thread_ctx, ctx, dst, src, &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doParith(thread_ctx, dst, expr_dst, expr_src, kind, width);
 }
 
@@ -2468,6 +2538,7 @@ instrumentParithRegMem(
         &expr_dst, &expr_src))
       return;
 
+  g_symbolic_instructions++;
   doParith(thread_ctx, dst, expr_dst, expr_src, kind, width);
 }
 
@@ -2517,6 +2588,7 @@ instrumentPcmpRegReg(
   if (!getExprFromRegReg(thread_ctx, ctx, dst, src, &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPcmp(thread_ctx, dst, expr_dst, expr_src, kind, width);
 }
 
@@ -2537,6 +2609,7 @@ instrumentPcmpRegMem(
         &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPcmp(thread_ctx, dst, expr_dst, expr_src, kind, width);
 }
 
@@ -2576,6 +2649,7 @@ instrumentPextrRegRegImm(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doPextr(thread_ctx, expr_src, imm,
       REG_Size(dst) * CHAR_BIT, width);
   thread_ctx->setExprToReg(dst, expr_res);
@@ -2596,6 +2670,7 @@ instrumentPextrMemRegImm(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doPextr(thread_ctx, expr_src, imm,
       size * CHAR_BIT, width);
   g_memory.setExprToMem(addr, size, expr_res);
@@ -2653,6 +2728,7 @@ instrumentPmaddwdRegReg(
         &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPmaddwd(thread_ctx, dst, expr_dst, expr_src);
 }
 
@@ -2671,6 +2747,7 @@ instrumentPmaddwdRegMem(
         &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPmaddwd(thread_ctx, dst, expr_dst, expr_src);
 }
 
@@ -2720,6 +2797,7 @@ instrumentPcmpxchgRegReg(
         &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPcmpxchg(thread_ctx, dst, expr_dst, expr_src, kind, width);
 }
 
@@ -2740,6 +2818,7 @@ instrumentPcmpxchgRegMem(
         &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPcmpxchg(thread_ctx, dst, expr_dst, expr_src, kind, width);
 }
 
@@ -2781,6 +2860,7 @@ instrumentPmulRegReg(
   if (!getExprFromRegReg(thread_ctx, ctx, dst, src, &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPmul(thread_ctx, dst, expr_dst, expr_src, width);
 }
 
@@ -2799,6 +2879,7 @@ instrumentPmulRegMem(
         &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPmul(thread_ctx, dst, expr_dst, expr_src, width);
 }
 
@@ -2842,6 +2923,7 @@ instrumentPmulhwRegReg(
   if (!getExprFromRegReg(thread_ctx, ctx, dst, src, &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPmulhw(thread_ctx, dst, expr_dst, expr_src, sign);
 }
 
@@ -2860,6 +2942,7 @@ instrumentPmulhwRegMem(
         &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPmulhw(thread_ctx, dst, expr_dst, expr_src, sign);
 }
 
@@ -2876,6 +2959,7 @@ instrumentPmovmskb(ThreadContext* thread_ctx,
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_dst = NULL;
   for (UINT i = 0; i < REG_Size(src); i++) {
     exprs.push_front(
@@ -2938,6 +3022,7 @@ instrumentPshufRegRegImm(
     return;
   }
 
+  g_symbolic_instructions++;
   doPshuf(thread_ctx, dst, expr_src, imm, REG_Size(dst), width);
 }
 
@@ -2956,6 +3041,7 @@ instrumentPshufRegMemImm(
     return;
   }
 
+  g_symbolic_instructions++;
   doPshuf(thread_ctx, dst, expr_src, imm, size, width);
 }
 
@@ -3033,6 +3119,7 @@ instrumentPshufbRegReg(
       &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPshufb(thread_ctx, dst, expr_dst, expr_src);
 }
 
@@ -3057,6 +3144,7 @@ instrumentPshufbRegMem(
       &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPshufb(thread_ctx, dst, expr_dst, expr_src);
 }
 
@@ -3107,6 +3195,7 @@ instrumentPshiftRegReg(
   if (expr_dst == NULL)
     return;
 
+  g_symbolic_instructions++;
   llvm::APInt value = getRegValue(ctx, src);
   doPshift(thread_ctx, dst,
       kind, expr_dst, value.getLimitedValue(), width);
@@ -3125,6 +3214,7 @@ instrumentPshiftRegImm(
   if (expr_dst == NULL)
     return;
 
+  g_symbolic_instructions++;
   doPshift(thread_ctx, dst, kind, expr_dst, imm, width);
 }
 
@@ -3143,6 +3233,7 @@ instrumentPshiftRegMem(
   if (expr_dst == NULL)
     return;
 
+  g_symbolic_instructions++;
   llvm::APInt value = getMemValue(addr, size);
   doPshift(thread_ctx, dst, kind, expr_dst, value.getLimitedValue(), width);
 }
@@ -3185,6 +3276,7 @@ instrumentPunpckhRegReg(
   if (!getExprFromRegReg(thread_ctx, ctx, dst, src, &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPunpckh(thread_ctx, dst, expr_dst, expr_src, width, REG_Size(dst));
 }
 
@@ -3203,6 +3295,7 @@ instrumentPunpckhRegMem(
         &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPunpckh(thread_ctx, dst, expr_dst, expr_src, width, size);
 }
 
@@ -3241,6 +3334,7 @@ instrumentPunpcklRegReg(
   if (!getExprFromRegReg(thread_ctx, ctx, dst, src, &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPunpckl(thread_ctx, dst, expr_dst, expr_src, width, REG_Size(dst));
 }
 
@@ -3259,6 +3353,7 @@ instrumentPunpcklRegMem(
         &expr_dst, &expr_src))
     return;
 
+  g_symbolic_instructions++;
   doPunpckl(thread_ctx, dst, expr_dst, expr_src, width, size);
 }
 
@@ -3272,6 +3367,7 @@ instrumentPushReg(
   // keep stack non-symbolic
   concretizeReg(thread_ctx, ctx, REG_STACK_PTR);
 
+  g_symbolic_instructions++;
   for (UINT i = 0; i < dst_size; i++) {
     ExprRef e = thread_ctx->getExprFromReg(ctx, src, i, 1);
     g_memory.setExprToMem(dst_addr + i, e);
@@ -3285,6 +3381,7 @@ instrumentPushImm(
     ADDRINT dst_addr,
     UINT dst_size) {
   // keep stack non-symbolic
+  g_symbolic_instructions++;
   concretizeReg(thread_ctx, ctx, REG_STACK_PTR);
   g_memory.clearExprFromMem(dst_addr, dst_size);
 }
@@ -3296,6 +3393,7 @@ instrumentPushMem(
     ADDRINT dst_addr,
     MEM_ARG) {
   // keep stack non-symbolic
+  g_symbolic_instructions++;
   concretizeReg(thread_ctx, ctx, REG_STACK_PTR);
   makeAddrConcrete(thread_ctx, ctx, base, index, addr, size, disp, scale);
 
@@ -3313,6 +3411,7 @@ instrumentPopReg(
     ADDRINT src_addr,
     UINT src_size) {
   // keep stack non-symbolic
+  g_symbolic_instructions++;
   concretizeReg(thread_ctx, ctx, REG_STACK_PTR);
   for (UINT i = 0; i < src_size; i++) {
     ExprRef e = g_memory.getExprFromMem(src_addr + i);
@@ -3327,6 +3426,7 @@ instrumentPopMem(
     MEM_ARG,
     ADDRINT src_addr) {
   // keep stack non-symbolic
+  g_symbolic_instructions++;
   concretizeReg(thread_ctx, ctx, REG_STACK_PTR);
   makeAddrConcrete(thread_ctx, ctx, base, index, addr, size, disp, scale);
 
@@ -3374,6 +3474,7 @@ instrumentScas(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = g_expr_builder->createBinaryExpr(Sub, expr_ax, expr_src);
   thread_ctx->setEflags(CC_OP_SUB, expr_res, expr_ax, expr_src);
 }
@@ -3394,6 +3495,7 @@ instrumentSetReg(
     REG dst,
     JccKind jcc_c,
     bool inv) {
+  g_symbolic_instructions++;
   ExprRef expr_res = doSet(thread_ctx, ctx, jcc_c, inv);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -3405,6 +3507,7 @@ instrumentSetMem(
     MEM_ARG,
     JccKind jcc_c,
     bool inv) {
+  g_symbolic_instructions++;
   makeAddrConcrete(thread_ctx, ctx, base, index, addr, size, disp, scale);
   ExprRef expr_res = doSet(thread_ctx, ctx, jcc_c, inv);
   g_memory.setExprToMem(addr, expr_res);
@@ -3415,6 +3518,7 @@ instrumentStos(ThreadContext *thread_ctx,
     const CONTEXT* ctx,
     ADDRINT dst_addr,
     REG src) {
+  g_symbolic_instructions++;
   UINT32 size = REG_Size(src);
   concretizeReg(thread_ctx, ctx, REG_GDI);
 
@@ -3443,6 +3547,7 @@ instrumentXaddRegReg(ThreadContext* thread_ctx, const CONTEXT *ctx,
   // source = destination;
   // destination = temporary;
 
+  g_symbolic_instructions++;
   ExprRef expr_tmp = g_expr_builder->createBinaryExpr(Add, expr_src, expr_dst);
   thread_ctx->setExprToReg(dst, expr_tmp);
   thread_ctx->setExprToReg(src, expr_dst);
@@ -3463,6 +3568,7 @@ instrumentXaddMemReg(ThreadContext* thread_ctx, const CONTEXT *ctx,
         &expr_src))
     return;
 
+  g_symbolic_instructions++;
   ExprRef expr_tmp = g_expr_builder->createBinaryExpr(Add, expr_src, expr_dst);
   g_memory.setExprToMem(addr, size, expr_tmp);
   thread_ctx->setExprToReg(src, expr_dst);
@@ -3477,6 +3583,7 @@ instrumentXchgRegReg(
   ExprRef expr_src = thread_ctx->getExprFromReg(ctx, src);
   ExprRef expr_dst = thread_ctx->getExprFromReg(ctx, dst);
 
+  g_symbolic_instructions++;
   thread_ctx->setExprToReg(dst, expr_src);
   thread_ctx->setExprToReg(src, expr_dst);
 }
@@ -3490,6 +3597,7 @@ instrumentXchgRegMem(
   ExprRef expr_src = g_memory.getExprFromMem(addr, size);
   ExprRef expr_dst = thread_ctx->getExprFromReg(ctx, dst);
 
+  g_symbolic_instructions++;
   g_memory.setExprToMem(addr, size, expr_dst);
   thread_ctx->setExprToReg(dst, expr_src);
 }
@@ -3503,6 +3611,7 @@ instrumentXchgMemReg(
   ExprRef expr_dst = g_memory.getExprFromMem(addr, size);
   ExprRef expr_src = thread_ctx->getExprFromReg(ctx, src);
 
+  g_symbolic_instructions++;
   thread_ctx->setExprToReg(src, expr_dst);
   g_memory.setExprToMem(addr, size, expr_src);
 }
@@ -3533,11 +3642,13 @@ instrumentConcretizeEflags(ThreadContext* thread_ctx,
 void PIN_FAST_ANALYSIS_CALL
 instrumentClrReg(ThreadContext* thread_ctx,
     const CONTEXT* ctx, REG r) {
+  g_symbolic_instructions++;
   thread_ctx->clearExprFromReg(r);
 }
 
 void PIN_FAST_ANALYSIS_CALL
 instrumentClrMem(ADDRINT addr, INT32 size) {
+  g_symbolic_instructions++;
   g_memory.clearExprFromMem(addr, size);
 }
 
@@ -3564,6 +3675,7 @@ instrumentTernaryRegRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = g_expr_builder->createBinaryExpr(kind, expr_src1, expr_src2);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -3591,6 +3703,7 @@ instrumentTernaryRegRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = g_expr_builder->createBinaryExpr(kind, expr_src1, expr_src2);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -3624,6 +3737,7 @@ instrumentVmovlRegRegMem(
     REG dst,
     REG src,
     MEM_ARG) {
+  g_symbolic_instructions++;
   QSYM_ASSERT(REG_Size(dst) == 16);
   doMovRegReg(thread_ctx, ctx, dst, src, 8, 8, 8);
   doMovRegMem(thread_ctx, ctx, dst,
@@ -3647,6 +3761,7 @@ instrumentVparithRegRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   doParith(thread_ctx, dst, expr_src1, expr_src2, kind, width);
 }
 
@@ -3670,6 +3785,7 @@ instrumentVparithRegRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   doParith(thread_ctx, dst, expr_src1, expr_src2, kind, width);
 }
 
@@ -3690,6 +3806,7 @@ instrumentVpcmpRegRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   doPcmp(thread_ctx, dst, expr_src1, expr_src2, kind, width);
 }
 
@@ -3713,6 +3830,7 @@ instrumentVpcmpRegRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   doPcmp(thread_ctx, dst, expr_src1, expr_src2, kind, width);
 }
 
@@ -3738,6 +3856,7 @@ instrumentVinsert128iRegRegRegImm(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doVinsert128i(expr_src1, expr_src2, imm);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -3764,6 +3883,7 @@ instrumentVinsert128iRegRegMemImm(
     return;
   }
 
+  g_symbolic_instructions++;
   ExprRef expr_res = doVinsert128i(expr_src1, expr_src2, imm);
   thread_ctx->setExprToReg(dst, expr_res);
 }
@@ -3783,6 +3903,7 @@ instrumentVpmaddwdRegRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   doPmaddwd(thread_ctx, dst, expr_src1, expr_src2);
 }
 
@@ -3804,6 +3925,7 @@ instrumentVpmaddwdRegRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   doPmaddwd(thread_ctx, dst, expr_src1, expr_src2);
 }
 
@@ -3824,6 +3946,7 @@ instrumentVpcmpxchgRegRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   doPcmpxchg(thread_ctx, dst, expr_src1, expr_src2, kind, width);
 }
 
@@ -3847,6 +3970,7 @@ instrumentVpcmpxchgRegRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   doPcmpxchg(thread_ctx, dst, expr_src1, expr_src2, kind, width);
 }
 
@@ -3866,6 +3990,7 @@ instrumentVpmulhwRegRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   doPmulhw(thread_ctx, dst, expr_src1, expr_src2, sign);
 }
 
@@ -3888,6 +4013,7 @@ instrumentVpmulhwRegRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   doPmulhw(thread_ctx, dst, expr_src1, expr_src2, sign);
 }
 
@@ -3907,6 +4033,7 @@ instrumentVpmulRegRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   doPmul(thread_ctx, dst, expr_src1, expr_src2, width);
 }
 
@@ -3929,6 +4056,7 @@ instrumentVpmulRegRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   doPmul(thread_ctx, dst, expr_src1, expr_src2, width);
 }
 
@@ -3947,6 +4075,7 @@ instrumentVpshufbRegRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   doPshufb(thread_ctx, dst, expr_src1, expr_src2);
 }
 
@@ -3968,6 +4097,7 @@ instrumentVpshufbRegRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   doPshufb(thread_ctx, dst, expr_src1, expr_src2);
 }
 
@@ -4026,6 +4156,7 @@ instrumentPshufwRegRegImm(
     return;
   }
 
+  g_symbolic_instructions++;
   doPshufw(thread_ctx, dst, expr_src, imm, high);
 }
 
@@ -4044,6 +4175,7 @@ instrumentPshufwRegMemImm(
     return;
   }
 
+  g_symbolic_instructions++;
   doPshufw(thread_ctx, dst, expr_src, imm, high);
 }
 
@@ -4066,6 +4198,7 @@ instrumentVpshiftRegRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   llvm::APInt value = getRegValue(ctx, src2);
   doPshift(thread_ctx, dst,
       kind, expr_src1, value.getLimitedValue(), width);
@@ -4087,6 +4220,7 @@ instrumentVpshiftRegRegImm(
     return;
   }
 
+  g_symbolic_instructions++;
   doPshift(thread_ctx, dst, kind, expr_src1, imm, width);
 }
 
@@ -4108,6 +4242,7 @@ instrumentVpshiftRegRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   llvm::APInt value = getMemValue(addr, size);
   doPshift(thread_ctx, dst, kind, expr_src1, value.getLimitedValue(), width);
 }
@@ -4129,6 +4264,7 @@ instrumentVpackRegRegReg(
     return;
   }
 
+  g_symbolic_instructions++;
   doPack(thread_ctx, dst, expr_src1, expr_src2, width, sign);
 }
 
@@ -4152,6 +4288,7 @@ instrumentVpackRegRegMem(
     return;
   }
 
+  g_symbolic_instructions++;
   doPack(thread_ctx, dst, expr_src1, expr_src2, width, sign);
 }
 
diff --git a/qsym/pintool/main.cpp b/qsym/pintool/main.cpp
index d9b6a1a..f1404a6 100644
--- a/qsym/pintool/main.cpp
+++ b/qsym/pintool/main.cpp
@@ -1,3 +1,4 @@
+#include <atomic>
 #include <cstdio>
 #include <errno.h>
 #include <sys/socket.h>
@@ -23,6 +24,8 @@ namespace qsym {
   Solver        *g_solver;
   ExprBuilder   *g_expr_builder;
   CallStackManager g_call_stack_manager;
+
+  extern std::atomic<uint64_t> g_symbolic_instructions;
 }
 
 #define SYS_SOCKET 1
@@ -89,6 +92,10 @@ void initializeGlobalContext(
     g_expr_builder = SymbolicExprBuilder::create();
 }
 
+VOID writeInstructionCount(INT32 code, VOID* data) {
+  LOG_INFO("Number of instructions: " + std::to_string(g_symbolic_instructions.load()) + "\n");
+}
+
 } // anonymous namespace
 
 int main(int argc, char** argv) {
@@ -100,6 +107,8 @@ int main(int argc, char** argv) {
   if (!checkOpt())
     goto err;
 
+  PIN_AddFiniFunction(writeInstructionCount, NULL);
+
   hookSyscalls(
         g_opt_stdin.Value() != 0,
         g_opt_fs.Value() != 0,
-- 
2.23.0

