From e7caefee9d631755018e59f815881a58f1abdf5a Mon Sep 17 00:00:00 2001
From: Sebastian Poeplau <sebastian.poeplau@eurecom.fr>
Date: Wed, 27 Mar 2019 11:54:49 +0100
Subject: [PATCH] Measure the time spent in symbolic mode

---
 qsym/pintool/instrument.cpp | 522 +++++++++++++++++++++++++++++++++++-
 qsym/pintool/main.cpp       |   4 +
 2 files changed, 519 insertions(+), 7 deletions(-)

diff --git a/qsym/pintool/instrument.cpp b/qsym/pintool/instrument.cpp
index 5c178ee..73ee750 100644
--- a/qsym/pintool/instrument.cpp
+++ b/qsym/pintool/instrument.cpp
@@ -1,15 +1,19 @@
 #include <atomic>
 #include <cassert>
+#include <chrono>
 #include "thread_context.h"
 #include "instrument.h"
 #include "expr.h"
 #include "solver.h"
 #include "third_party/pin/utils.h"
 
+using namespace std::chrono;
+
 // bit position
 namespace qsym {
 
-  std::atomic<uint64_t> g_symbolic_instructions{0};
+std::atomic<uint64_t> g_symbolic_instructions{0};
+std::atomic<nanoseconds::rep> g_symbolic_execution_time{0};
 
 void instrumentBBL(
     ThreadContext *thread_ctx,
@@ -650,8 +654,12 @@ instrumentShiftRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doShift(thread_ctx, kind, op_kind, expr_dst, expr_src, bits);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -677,8 +685,12 @@ instrumentShiftRegCl(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doShift(thread_ctx, kind, op_kind, expr_dst, expr_src, bits);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -705,8 +717,12 @@ instrumentShiftMemImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doShift(thread_ctx, kind, op_kind, expr_dst, expr_src, bits);
   g_memory.setExprToMem(addr, size, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -732,8 +748,12 @@ instrumentShiftMemCl(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doShift(thread_ctx, kind, op_kind, expr_dst, expr_src, bits);
   g_memory.setExprToMem(addr, size, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static ExprRef
@@ -792,8 +812,12 @@ instrumentShiftdRegRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doShiftd(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_imm, bits);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -823,8 +847,12 @@ instrumentShiftdRegRegCl(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doShiftd(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_imm, bits);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -855,8 +883,12 @@ instrumentShiftdMemRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doShiftd(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_imm, bits);
   g_memory.setExprToMem(addr, size, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -886,8 +918,12 @@ instrumentShiftdMemRegCl(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doShiftd(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_imm, bits);
   g_memory.setExprToMem(addr, size, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static OpKind
@@ -942,9 +978,13 @@ instrumentBinaryRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doBinary(thread_ctx, kind, op_kind, expr_dst, expr_src);
   if (write)
     thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -971,9 +1011,13 @@ instrumentBinaryRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doBinary(thread_ctx, kind, op_kind, expr_dst, expr_src);
   if (write)
     thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1000,9 +1044,13 @@ instrumentBinaryRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doBinary(thread_ctx, kind, op_kind, expr_dst, expr_src);
   if (write)
     thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1029,9 +1077,13 @@ instrumentBinaryMemReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doBinary(thread_ctx, kind, op_kind, expr_dst, expr_src);
   if (write)
     g_memory.setExprToMem(addr, size, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1058,9 +1110,13 @@ instrumentBinaryMemImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doBinary(thread_ctx, kind, op_kind, expr_dst, expr_src);
   if (write)
     g_memory.setExprToMem(addr, size, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static ExprRef
@@ -1103,8 +1159,12 @@ instrumentCarryRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doCarry(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_cf);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1133,8 +1193,12 @@ instrumentCarryRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doCarry(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_cf);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1163,8 +1227,12 @@ instrumentCarryRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doCarry(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_cf);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1193,8 +1261,12 @@ instrumentCarryMemReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doCarry(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_cf);
   g_memory.setExprToMem(addr, size, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1223,8 +1295,12 @@ instrumentCarryMemImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doCarry(thread_ctx, kind, op_kind, expr_dst, expr_src, expr_cf);
   g_memory.setExprToMem(addr, size, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1252,8 +1328,12 @@ instrumentCbw(ThreadContext* thread_ctx,
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   expr_to = g_expr_builder->createSExt(expr_from, bits);
   thread_ctx->setExprToReg(to, expr_to);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1270,9 +1350,13 @@ instrumentCwd(ThreadContext* thread_ctx,
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   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);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static ExprRef
@@ -1349,7 +1433,11 @@ instrumentBsRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doBs(thread_ctx, dst, expr_src, inv);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1369,7 +1457,11 @@ instrumentBsRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doBs(thread_ctx, dst, expr_src, inv);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1379,12 +1471,18 @@ instrumentBswapReg(ThreadContext* thread_ctx, const CONTEXT* ctx,
   std::list<ExprRef> exprs;
 
   if (expr_dst) {
+    g_symbolic_instructions++;
+    auto start = steady_clock::now();
+
     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);
+
+    auto end = steady_clock::now();
+    auto time_span = duration_cast<nanoseconds>(end - start);
+    g_symbolic_execution_time.fetch_add(time_span.count());
   }
 }
 
@@ -1435,6 +1533,7 @@ instrumentBtRegReg(ThreadContext* thread_ctx, const CONTEXT* ctx,
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   expr_dst = doBt(thread_ctx, expr_dst, getRegValue(ctx, src).getZExtValue(),
                   bits, kind);
 
@@ -1442,6 +1541,9 @@ instrumentBtRegReg(ThreadContext* thread_ctx, const CONTEXT* ctx,
     assert(expr_dst != NULL);
     thread_ctx->setExprToReg(dst, expr_dst);
   }
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1455,12 +1557,16 @@ instrumentBtRegImm(ThreadContext* thread_ctx,
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   expr_dst = doBt(thread_ctx, expr_dst, imm, REG_Size(dst) * CHAR_BIT, kind);
 
   if (kind != Invalid) {
     assert(expr_dst != NULL);
     thread_ctx->setExprToReg(dst, expr_dst);
   }
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1480,12 +1586,16 @@ instrumentBtMemReg(ThreadContext* thread_ctx,
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   expr_dst = doBt(thread_ctx, expr_dst, imm, bits, kind);
 
   if (kind != Invalid) {
     assert(expr_dst != NULL);
     g_memory.setExprToMem(addr, size, expr_dst);
   }
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1500,12 +1610,16 @@ instrumentBtMemImm(ThreadContext* thread_ctx,
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   expr_dst = doBt(thread_ctx, expr_dst, imm, bits, kind);
 
   if (kind != Invalid) {
     assert(expr_dst != NULL);
     g_memory.setExprToMem(addr, size, expr_dst);
   }
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1566,8 +1680,12 @@ instrumentCmps(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = g_expr_builder->createBinaryExpr(Sub, expr_dst, expr_src);
   thread_ctx->setEflags(CC_OP_SUB, expr_res, expr_dst, expr_src);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1588,7 +1706,6 @@ instrumentCmpxchgRegReg(ThreadContext* thread_ctx,
     return;
   }
 
-  g_symbolic_instructions++;
   llvm::APInt val_dst = getRegValue(ctx, dst);
   llvm::APInt val_ax = getRegValue(ctx, ax);
 
@@ -1625,7 +1742,6 @@ instrumentCmpxchgMemReg(ThreadContext* thread_ctx,
     return;
   }
 
-  g_symbolic_instructions++;
   llvm::APInt val_dst = getMemValue(addr, size);
   llvm::APInt val_ax = getRegValue(ctx, ax);
 
@@ -1681,9 +1797,13 @@ doIncDec(ThreadContext* thread_ctx, ExprRef expr_dst, Kind kind, OpKind op_kind)
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   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);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
   return expr_res;
 }
 
@@ -1775,8 +1895,12 @@ instrumentDivReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   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);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void
@@ -1807,8 +1931,12 @@ instrumentDivMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   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);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -1838,7 +1966,11 @@ instrumentMulReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMul(thread_ctx, ctx, reg_l, reg_h, expr_src, expr_reg_l, bits, sign);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -1868,7 +2000,11 @@ instrumentMulMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMul(thread_ctx, ctx, reg_l, reg_h, expr_src, expr_reg_l, bits, sign);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1941,7 +2077,11 @@ instrumentIMulRegRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMul(thread_ctx, expr_src, expr_imm, dst);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1967,7 +2107,11 @@ instrumentIMulRegMemImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMul(thread_ctx, expr_src, expr_imm, dst);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -1976,8 +2120,12 @@ instrumentLeaRegMem(ThreadContext* thread_ctx,
     REG dst,
     REG base, REG index, ADDRINT disp, UINT32 scale) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef e = thread_ctx->getAddrExpr(ctx, base, index, disp, scale);
   thread_ctx->setExprToReg(dst, e);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -2002,7 +2150,11 @@ instrumentMovRegReg(
     REG dst,
     REG src) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMovRegReg(thread_ctx, ctx, dst, src, 0, 0, REG_Size(dst));
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2033,8 +2185,12 @@ instrumentMovRegMem(
     REG dst,
     MEM_ARG) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMovRegMem(thread_ctx, ctx, dst,
     base, index, addr, size, disp, scale, 0);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2042,8 +2198,12 @@ instrumentMovMemImm(ThreadContext *thread_ctx, const CONTEXT* ctx,
     MEM_ARG,
     ADDRINT imm) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   makeAddrConcrete(thread_ctx, ctx, base, index, addr, size, disp, scale);
   g_memory.clearExprFromMem(addr, size);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -2066,9 +2226,13 @@ instrumentMovMemReg(ThreadContext *thread_ctx, const CONTEXT* ctx,
     MEM_ARG,
     REG src) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMovMemReg(thread_ctx, ctx,
       base, index, addr, size, disp, scale,
       src, 0);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2079,9 +2243,13 @@ instrumentMovhRegMem(
     MEM_ARG) {
   QSYM_ASSERT(REG_Size(dst) == 16);
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMovRegMem(thread_ctx, ctx, dst,
     base, index, addr, size, disp, scale,
     8);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2092,9 +2260,13 @@ instrumentMovhMemReg(
     REG src) {
   QSYM_ASSERT(REG_Size(src) == 16);
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMovMemReg(thread_ctx, ctx,
     base, index, addr, size, disp, scale,
     src, 8);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2106,8 +2278,12 @@ instrumentMovlzRegReg(
     UINT width) {
   UINT size = REG_Size(src);
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMovRegReg(thread_ctx, ctx, dst, src, 0, 0, width);
   thread_ctx->clearExprFromReg(dst, size, REG_Size(dst) - size);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2118,10 +2294,14 @@ instrumentMovlzRegMem(
     MEM_ARG,
     UINT width) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMovRegMem(thread_ctx, ctx, dst,
                 base, index, addr, size, disp, scale, 0);
   QSYM_ASSERT(REG_Size(dst) >= size);
   thread_ctx->clearExprFromReg(dst, size, REG_Size(dst) - size);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2132,9 +2312,13 @@ instrumentMovlzMemReg(
     REG src,
     UINT width) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doMovMemReg(thread_ctx, ctx,
       base, index, addr, size, disp, scale,
       src, 0);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2149,10 +2333,14 @@ instrumentMovs(
   concretizeReg(thread_ctx, ctx, REG_GDI);
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   for (UINT32 i = 0; i < size; i++) {
     ExprRef e = g_memory.getExprFromMemAlways(src_addr + i);
     g_memory.setExprToMem(dst_addr + i, e);
   }
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2165,6 +2353,10 @@ instrumentMovsxRegMem(ThreadContext *thread_ctx,
   if (e != NULL) {
     e = g_expr_builder->createSExt(e, REG_Size(dst) * 8);
     g_symbolic_instructions++;
+    auto start = steady_clock::now();
+    auto end = steady_clock::now();
+    auto time_span = duration_cast<nanoseconds>(end - start);
+    g_symbolic_execution_time.fetch_add(time_span.count());
   }
   thread_ctx->setExprToReg(dst, e);
 }
@@ -2177,6 +2369,10 @@ instrumentMovsxRegReg(ThreadContext* thread_ctx,
   if (e != NULL){
     e = g_expr_builder->createSExt(e, REG_Size(dst) * 8);
     g_symbolic_instructions++;
+    auto start = steady_clock::now();
+    auto end = steady_clock::now();
+    auto time_span = duration_cast<nanoseconds>(end - start);
+    g_symbolic_execution_time.fetch_add(time_span.count());
   }
   thread_ctx->setExprToReg(dst, e);
 }
@@ -2190,6 +2386,10 @@ instrumentMovzxRegMem(ThreadContext *thread_ctx,
   if (e != NULL) {
     e = g_expr_builder->createZExt(e, REG_Size(dst) * 8);
     g_symbolic_instructions++;
+    auto start = steady_clock::now();
+    auto end = steady_clock::now();
+    auto time_span = duration_cast<nanoseconds>(end - start);
+    g_symbolic_execution_time.fetch_add(time_span.count());
   }
   thread_ctx->setExprToReg(dst, e);
 }
@@ -2201,7 +2401,11 @@ instrumentMovzxRegReg(ThreadContext* thread_ctx,
   ExprRef e = thread_ctx->getExprFromReg(ctx, src);
   if (e != NULL) {
     e = g_expr_builder->createZExt(e, REG_Size(dst) * 8);
+    auto start = steady_clock::now();
     g_symbolic_instructions++;
+    auto end = steady_clock::now();
+    auto time_span = duration_cast<nanoseconds>(end - start);
+    g_symbolic_execution_time.fetch_add(time_span.count());
   }
   thread_ctx->setExprToReg(dst, e);
 }
@@ -2233,9 +2437,13 @@ doNegNot(ThreadContext* thread_ctx, ExprRef expr_dst, Kind kind) {
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = g_expr_builder->createUnaryExpr(kind, expr_dst);
   thread_ctx->setEflags(CC_OP_LOGIC, expr_res, expr_dst, NULL);
   return expr_res;
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2273,12 +2481,16 @@ instrumentJcc(ThreadContext* thread_ctx,
   ExprRef e = thread_ctx->computeJcc(ctx, jcc_c, inv);
   if (e) {
     g_symbolic_instructions++;
+    auto start = steady_clock::now();
     ADDRINT pc = PIN_GetContextReg(ctx, REG_INST_PTR);
     LOG_DEBUG("Symbolic branch at " + hexstr(pc) + ": " + e->toString() + "\n");
 #ifdef CONFIG_TRACE
     trace_addJcc(e, ctx, taken);
 #endif
     g_solver->addJcc(e, taken, pc);
+    auto end = steady_clock::now();
+    auto time_span = duration_cast<nanoseconds>(end - start);
+    g_symbolic_execution_time.fetch_add(time_span.count());
   }
 }
 
@@ -2287,10 +2499,14 @@ instrumentJmpReg(ThreadContext* thread_ctx, const CONTEXT* ctx, REG r) {
   ExprRef e = thread_ctx->getExprFromReg(ctx, r);
   if (e != NULL) {
     g_symbolic_instructions++;
+    auto start = steady_clock::now();
     LOG_DEBUG("Symbolic jmp: " + e->toString() + "\n");
     llvm::APInt val = getRegValue(ctx, r);
     g_solver->solveAll(e, val);
     thread_ctx->clearExprFromReg(r);
+    auto end = steady_clock::now();
+    auto time_span = duration_cast<nanoseconds>(end - start);
+    g_symbolic_execution_time.fetch_add(time_span.count());
   }
 }
 
@@ -2299,10 +2515,14 @@ instrumentJmpMem(ThreadContext* thread_ctx, const CONTEXT* ctx, MEM_ARG) {
   ExprRef e = g_memory.getExprFromMem(addr, size);
   if (e != NULL) {
     g_symbolic_instructions++;
+    auto start = steady_clock::now();
     LOG_DEBUG("Symbolic jmp: " + e->toString() + "\n");
     llvm::APInt val = getMemValue(addr, size);
     g_solver->solveAll(e, val);
     g_memory.clearExprFromMem(addr, size);
+    auto end = steady_clock::now();
+    auto time_span = duration_cast<nanoseconds>(end - start);
+    g_symbolic_execution_time.fetch_add(time_span.count());
   }
 }
 
@@ -2404,8 +2624,12 @@ instrumentPackRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPack(thread_ctx, dst, expr_dst, expr_src,
       width, sign);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2429,8 +2653,12 @@ instrumentPackRegMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPack(thread_ctx, dst, expr_dst, expr_src,
       width, sign);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2444,6 +2672,7 @@ instrumentPalignrReg(ThreadContext* thread_ctx, const CONTEXT* ctx,
     return ;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   fixRegExpr(&expr_src, ctx, src);
   fixRegExpr(&expr_dst, ctx, dst);
 
@@ -2452,6 +2681,9 @@ instrumentPalignrReg(ThreadContext* thread_ctx, const CONTEXT* ctx,
       off * CHAR_BIT,
       bits);
   thread_ctx->setExprToReg(dst, e);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2467,6 +2699,7 @@ instrumentPalignrMem(ThreadContext* thread_ctx, const CONTEXT* ctx,
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   fixMemExpr(&expr_src, addr, size);
   fixRegExpr(&expr_dst, ctx, dst);
 
@@ -2475,6 +2708,9 @@ instrumentPalignrMem(ThreadContext* thread_ctx, const CONTEXT* ctx,
       off * CHAR_BIT,
       bits);
   thread_ctx->setExprToReg(dst, e);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -2518,7 +2754,11 @@ instrumentParithRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doParith(thread_ctx, dst, expr_dst, expr_src, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2539,7 +2779,11 @@ instrumentParithRegMem(
       return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doParith(thread_ctx, dst, expr_dst, expr_src, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -2589,7 +2833,11 @@ instrumentPcmpRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPcmp(thread_ctx, dst, expr_dst, expr_src, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void
@@ -2610,7 +2858,11 @@ instrumentPcmpRegMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPcmp(thread_ctx, dst, expr_dst, expr_src, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static ExprRef
@@ -2650,9 +2902,13 @@ instrumentPextrRegRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doPextr(thread_ctx, expr_src, imm,
       REG_Size(dst) * CHAR_BIT, width);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2671,9 +2927,13 @@ instrumentPextrMemRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doPextr(thread_ctx, expr_src, imm,
       size * CHAR_BIT, width);
   g_memory.setExprToMem(addr, size, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -2729,7 +2989,11 @@ instrumentPmaddwdRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmaddwd(thread_ctx, dst, expr_dst, expr_src);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2748,7 +3012,11 @@ instrumentPmaddwdRegMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmaddwd(thread_ctx, dst, expr_dst, expr_src);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -2798,7 +3066,11 @@ instrumentPcmpxchgRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPcmpxchg(thread_ctx, dst, expr_dst, expr_src, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2819,7 +3091,11 @@ instrumentPcmpxchgRegMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPcmpxchg(thread_ctx, dst, expr_dst, expr_src, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -2861,7 +3137,11 @@ instrumentPmulRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmul(thread_ctx, dst, expr_dst, expr_src, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2880,7 +3160,11 @@ instrumentPmulRegMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmul(thread_ctx, dst, expr_dst, expr_src, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -2924,7 +3208,11 @@ instrumentPmulhwRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmulhw(thread_ctx, dst, expr_dst, expr_src, sign);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2943,7 +3231,11 @@ instrumentPmulhwRegMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmulhw(thread_ctx, dst, expr_dst, expr_src, sign);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -2960,6 +3252,7 @@ instrumentPmovmskb(ThreadContext* thread_ctx,
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_dst = NULL;
   for (UINT i = 0; i < REG_Size(src); i++) {
     exprs.push_front(
@@ -2974,6 +3267,9 @@ instrumentPmovmskb(ThreadContext* thread_ctx,
               g_expr_builder->createConcat(exprs),
               REG_Size(dst) * CHAR_BIT);
   thread_ctx->setExprToReg(dst, expr_dst);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -3023,7 +3319,11 @@ instrumentPshufRegRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPshuf(thread_ctx, dst, expr_src, imm, REG_Size(dst), width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3042,7 +3342,11 @@ instrumentPshufRegMemImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPshuf(thread_ctx, dst, expr_src, imm, size, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -3120,7 +3424,11 @@ instrumentPshufbRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPshufb(thread_ctx, dst, expr_dst, expr_src);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3145,7 +3453,11 @@ instrumentPshufbRegMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPshufb(thread_ctx, dst, expr_dst, expr_src);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -3196,9 +3508,13 @@ instrumentPshiftRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   llvm::APInt value = getRegValue(ctx, src);
   doPshift(thread_ctx, dst,
       kind, expr_dst, value.getLimitedValue(), width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3215,7 +3531,11 @@ instrumentPshiftRegImm(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPshift(thread_ctx, dst, kind, expr_dst, imm, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3234,8 +3554,12 @@ instrumentPshiftRegMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   llvm::APInt value = getMemValue(addr, size);
   doPshift(thread_ctx, dst, kind, expr_dst, value.getLimitedValue(), width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -3277,7 +3601,11 @@ instrumentPunpckhRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPunpckh(thread_ctx, dst, expr_dst, expr_src, width, REG_Size(dst));
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3296,7 +3624,11 @@ instrumentPunpckhRegMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPunpckh(thread_ctx, dst, expr_dst, expr_src, width, size);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -3335,7 +3667,11 @@ instrumentPunpcklRegReg(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPunpckl(thread_ctx, dst, expr_dst, expr_src, width, REG_Size(dst));
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3354,7 +3690,11 @@ instrumentPunpcklRegMem(
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPunpckl(thread_ctx, dst, expr_dst, expr_src, width, size);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3368,10 +3708,14 @@ instrumentPushReg(
   concretizeReg(thread_ctx, ctx, REG_STACK_PTR);
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   for (UINT i = 0; i < dst_size; i++) {
     ExprRef e = thread_ctx->getExprFromReg(ctx, src, i, 1);
     g_memory.setExprToMem(dst_addr + i, e);
   }
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3382,8 +3726,12 @@ instrumentPushImm(
     UINT dst_size) {
   // keep stack non-symbolic
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   concretizeReg(thread_ctx, ctx, REG_STACK_PTR);
   g_memory.clearExprFromMem(dst_addr, dst_size);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3394,6 +3742,7 @@ instrumentPushMem(
     MEM_ARG) {
   // keep stack non-symbolic
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   concretizeReg(thread_ctx, ctx, REG_STACK_PTR);
   makeAddrConcrete(thread_ctx, ctx, base, index, addr, size, disp, scale);
 
@@ -3401,6 +3750,9 @@ instrumentPushMem(
     ExprRef e = g_memory.getExprFromMem(addr + i);
     g_memory.setExprToMem(dst_addr + i, e);
   }
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3412,11 +3764,15 @@ instrumentPopReg(
     UINT src_size) {
   // keep stack non-symbolic
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   concretizeReg(thread_ctx, ctx, REG_STACK_PTR);
   for (UINT i = 0; i < src_size; i++) {
     ExprRef e = g_memory.getExprFromMem(src_addr + i);
     thread_ctx->setExprToReg(dst, e, i, 1);
   }
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3427,6 +3783,7 @@ instrumentPopMem(
     ADDRINT src_addr) {
   // keep stack non-symbolic
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   concretizeReg(thread_ctx, ctx, REG_STACK_PTR);
   makeAddrConcrete(thread_ctx, ctx, base, index, addr, size, disp, scale);
 
@@ -3434,6 +3791,9 @@ instrumentPopMem(
     ExprRef e = g_memory.getExprFromMem(src_addr + i);
     g_memory.setExprToMem(addr + i, e);
   }
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 
@@ -3475,8 +3835,12 @@ instrumentScas(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = g_expr_builder->createBinaryExpr(Sub, expr_ax, expr_src);
   thread_ctx->setEflags(CC_OP_SUB, expr_res, expr_ax, expr_src);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static ExprRef
@@ -3496,8 +3860,12 @@ instrumentSetReg(
     JccKind jcc_c,
     bool inv) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doSet(thread_ctx, ctx, jcc_c, inv);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3508,9 +3876,13 @@ instrumentSetMem(
     JccKind jcc_c,
     bool inv) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   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);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3519,6 +3891,7 @@ instrumentStos(ThreadContext *thread_ctx,
     ADDRINT dst_addr,
     REG src) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   UINT32 size = REG_Size(src);
   concretizeReg(thread_ctx, ctx, REG_GDI);
 
@@ -3526,6 +3899,9 @@ instrumentStos(ThreadContext *thread_ctx,
     ExprRef e = thread_ctx->getExprFromReg(ctx, src, i, 1);
     g_memory.setExprToMem(dst_addr + i, e);
   }
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3548,9 +3924,13 @@ instrumentXaddRegReg(ThreadContext* thread_ctx, const CONTEXT *ctx,
   // destination = temporary;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_tmp = g_expr_builder->createBinaryExpr(Add, expr_src, expr_dst);
   thread_ctx->setExprToReg(dst, expr_tmp);
   thread_ctx->setExprToReg(src, expr_dst);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3569,9 +3949,13 @@ instrumentXaddMemReg(ThreadContext* thread_ctx, const CONTEXT *ctx,
     return;
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   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);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3580,12 +3964,16 @@ instrumentXchgRegReg(
     const CONTEXT *ctx,
     REG dst,
     REG src) {
+  g_symbolic_instructions++;
+  auto start = steady_clock::now();
   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);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3594,12 +3982,16 @@ instrumentXchgRegMem(
     const CONTEXT *ctx,
     REG dst,
     MEM_ARG) {
+  g_symbolic_instructions++;
+  auto start = steady_clock::now();
   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);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3608,12 +4000,16 @@ instrumentXchgMemReg(
     const CONTEXT *ctx,
     MEM_ARG,
     REG src) {
+  g_symbolic_instructions++;
+  auto start = steady_clock::now();
   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);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 // default instrumentation
@@ -3643,13 +4039,21 @@ void PIN_FAST_ANALYSIS_CALL
 instrumentClrReg(ThreadContext* thread_ctx,
     const CONTEXT* ctx, REG r) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   thread_ctx->clearExprFromReg(r);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
 instrumentClrMem(ADDRINT addr, INT32 size) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   g_memory.clearExprFromMem(addr, size);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void
@@ -3676,8 +4080,12 @@ instrumentTernaryRegRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = g_expr_builder->createBinaryExpr(kind, expr_src1, expr_src2);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void
@@ -3704,8 +4112,12 @@ instrumentTernaryRegRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = g_expr_builder->createBinaryExpr(kind, expr_src1, expr_src2);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 
@@ -3738,10 +4150,14 @@ instrumentVmovlRegRegMem(
     REG src,
     MEM_ARG) {
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   QSYM_ASSERT(REG_Size(dst) == 16);
   doMovRegReg(thread_ctx, ctx, dst, src, 8, 8, 8);
   doMovRegMem(thread_ctx, ctx, dst,
       base, index, addr, size, disp, scale, 0);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3762,7 +4178,11 @@ instrumentVparithRegRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doParith(thread_ctx, dst, expr_src1, expr_src2, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3786,7 +4206,11 @@ instrumentVparithRegRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doParith(thread_ctx, dst, expr_src1, expr_src2, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3807,7 +4231,11 @@ instrumentVpcmpRegRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPcmp(thread_ctx, dst, expr_src1, expr_src2, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3831,7 +4259,11 @@ instrumentVpcmpRegRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPcmp(thread_ctx, dst, expr_src1, expr_src2, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3857,8 +4289,12 @@ instrumentVinsert128iRegRegRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doVinsert128i(expr_src1, expr_src2, imm);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3884,8 +4320,12 @@ instrumentVinsert128iRegRegMemImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   ExprRef expr_res = doVinsert128i(expr_src1, expr_src2, imm);
   thread_ctx->setExprToReg(dst, expr_res);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3904,7 +4344,11 @@ instrumentVpmaddwdRegRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmaddwd(thread_ctx, dst, expr_src1, expr_src2);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3926,7 +4370,11 @@ instrumentVpmaddwdRegRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmaddwd(thread_ctx, dst, expr_src1, expr_src2);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3947,7 +4395,11 @@ instrumentVpcmpxchgRegRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPcmpxchg(thread_ctx, dst, expr_src1, expr_src2, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3971,7 +4423,11 @@ instrumentVpcmpxchgRegRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPcmpxchg(thread_ctx, dst, expr_src1, expr_src2, kind, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -3991,7 +4447,11 @@ instrumentVpmulhwRegRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmulhw(thread_ctx, dst, expr_src1, expr_src2, sign);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4014,7 +4474,11 @@ instrumentVpmulhwRegRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmulhw(thread_ctx, dst, expr_src1, expr_src2, sign);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4034,7 +4498,11 @@ instrumentVpmulRegRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmul(thread_ctx, dst, expr_src1, expr_src2, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4057,7 +4525,11 @@ instrumentVpmulRegRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPmul(thread_ctx, dst, expr_src1, expr_src2, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4076,7 +4548,11 @@ instrumentVpshufbRegRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPshufb(thread_ctx, dst, expr_src1, expr_src2);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4098,7 +4574,11 @@ instrumentVpshufbRegRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPshufb(thread_ctx, dst, expr_src1, expr_src2);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 static void
@@ -4157,7 +4637,11 @@ instrumentPshufwRegRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPshufw(thread_ctx, dst, expr_src, imm, high);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4176,7 +4660,11 @@ instrumentPshufwRegMemImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPshufw(thread_ctx, dst, expr_src, imm, high);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4199,9 +4687,13 @@ instrumentVpshiftRegRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   llvm::APInt value = getRegValue(ctx, src2);
   doPshift(thread_ctx, dst,
       kind, expr_src1, value.getLimitedValue(), width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4221,7 +4713,11 @@ instrumentVpshiftRegRegImm(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPshift(thread_ctx, dst, kind, expr_src1, imm, width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4243,8 +4739,12 @@ instrumentVpshiftRegRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   llvm::APInt value = getMemValue(addr, size);
   doPshift(thread_ctx, dst, kind, expr_src1, value.getLimitedValue(), width);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4265,7 +4765,11 @@ instrumentVpackRegRegReg(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPack(thread_ctx, dst, expr_src1, expr_src2, width, sign);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
@@ -4289,7 +4793,11 @@ instrumentVpackRegRegMem(
   }
 
   g_symbolic_instructions++;
+  auto start = steady_clock::now();
   doPack(thread_ctx, dst, expr_src1, expr_src2, width, sign);
+  auto end = steady_clock::now();
+  auto time_span = duration_cast<nanoseconds>(end - start);
+  g_symbolic_execution_time.fetch_add(time_span.count());
 }
 
 void PIN_FAST_ANALYSIS_CALL
diff --git a/qsym/pintool/main.cpp b/qsym/pintool/main.cpp
index f1404a6..7b7117a 100644
--- a/qsym/pintool/main.cpp
+++ b/qsym/pintool/main.cpp
@@ -1,4 +1,5 @@
 #include <atomic>
+#include <chrono>
 #include <cstdio>
 #include <errno.h>
 #include <sys/socket.h>
@@ -26,6 +27,7 @@ namespace qsym {
   CallStackManager g_call_stack_manager;
 
   extern std::atomic<uint64_t> g_symbolic_instructions;
+  extern std::atomic<std::chrono::nanoseconds::rep> g_symbolic_execution_time;
 }
 
 #define SYS_SOCKET 1
@@ -93,6 +95,8 @@ void initializeGlobalContext(
 }
 
 VOID writeInstructionCount(INT32 code, VOID* data) {
+  // print the time in seconds with millisecond precision
+  LOG_INFO("Time in symbolic mode: " + std::to_string((double)(g_symbolic_execution_time.load() / (1000 * 1000)) / 1000) + "\n");
   LOG_INFO("Number of instructions: " + std::to_string(g_symbolic_instructions.load()) + "\n");
 }
 
-- 
2.23.0

