Skip to content

Commit

Permalink
Fix issue:#9 - Use smt2lib_bv instead of constante 0x
Browse files Browse the repository at this point in the history
  • Loading branch information
@JonathanSalwan
JonathanSalwan committed Jan 27, 2015
1 parent 32df227 commit b75bb94
Show file tree
Hide file tree
Showing 4 changed files with 26 additions and 68 deletions.
8 changes: 4 additions & 4 deletions src/ir/add.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,9 @@ VOID addRegImm(std::string insDis, ADDRINT insAddr, CONTEXT *ctx, REG reg1, UINT
UINT64 reg1_ID = translatePinRegToID(reg1);

if (symbolicEngine->symbolicReg[reg1_ID] != (UINT64)-1)
expr << "(+ #" << std::dec << symbolicEngine->symbolicReg[reg1_ID] << " 0x" << std::hex << imm << ")";
expr << "(+ #" << std::dec << symbolicEngine->symbolicReg[reg1_ID] << " " << smt2lib_bv(imm, REG_Size(reg1)) << ")";
else
expr << "(+ 0x" << std::hex << PIN_GetContextReg(ctx, getHighReg(reg1)) << " 0x" << imm << ")";
expr << "(+ " << smt2lib_bv(PIN_GetContextReg(ctx, getHighReg(reg1)), REG_Size(reg1)) << " " << smt2lib_bv(imm, REG_Size(reg1)) << ")";

symbolicElement *elem = symbolicEngine->newSymbolicElement(expr);
symbolicEngine->symbolicReg[reg1_ID] = elem->getID();
Expand Down Expand Up @@ -58,12 +58,12 @@ VOID addRegReg(std::string insDis, ADDRINT insAddr, CONTEXT *ctx, REG reg1, REG
if (symbolicEngine->symbolicReg[reg1_ID] != (UINT64)-1)
vr1 << "#" << std::dec << symbolicEngine->symbolicReg[reg1_ID];
else
vr1 << "0x" << std::hex << PIN_GetContextReg(ctx, getHighReg(reg1));
vr1 << smt2lib_bv(PIN_GetContextReg(ctx, getHighReg(reg1)), REG_Size(reg1));

if (symbolicEngine->symbolicReg[reg2_ID] != (UINT64)-1)
vr2 << "#" << std::dec << symbolicEngine->symbolicReg[reg2_ID];
else
vr2 << "0x" << std::hex << PIN_GetContextReg(ctx, getHighReg(reg2));
vr2 << smt2lib_bv(PIN_GetContextReg(ctx, getHighReg(reg2)), REG_Size(reg1));

expr << "(+ " << vr1.str() << " " << vr2.str() << ")";

Expand Down
70 changes: 14 additions & 56 deletions src/ir/mov.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,16 +30,17 @@ VOID movRegReg(std::string insDis, ADDRINT insAddr, CONTEXT *ctx, REG reg1, REG
else{
switch(opcode){
case XED_ICLASS_MOV:
expr << "0x" << std::hex << PIN_GetContextReg(ctx, getHighReg(reg2));
expr << smt2lib_bv(PIN_GetContextReg(ctx, getHighReg(reg2)), REG_Size(reg1));
break;
case XED_ICLASS_MOVSX:
expr << "((_ sign_extend " << std::dec << size << ") 0x" << std::hex << PIN_GetContextReg(ctx, getHighReg(reg2)) << ")";
expr << "((_ sign_extend " << std::dec << size << ") " << smt2lib_bv(PIN_GetContextReg(ctx, getHighReg(reg2)), REG_Size(reg2)) << ")";
break;
case XED_ICLASS_MOVZX:
expr << "((_ zero_extend " << std::dec << size << ") 0x" << std::hex << PIN_GetContextReg(ctx, getHighReg(reg2)) << ")";
expr << "((_ zero_extend " << std::dec << size << ") " << smt2lib_bv(PIN_GetContextReg(ctx, getHighReg(reg2)), REG_Size(reg2)) << ")";
break;
}
}


symbolicElement *elem = symbolicEngine->newSymbolicElement(expr);
symbolicEngine->symbolicReg[reg1_ID] = elem->getID();
Expand Down Expand Up @@ -69,7 +70,7 @@ VOID movRegImm(std::string insDis, ADDRINT insAddr, REG reg1, UINT64 imm, INT32

UINT64 reg1_ID = translatePinRegToID(reg1);

expr << "0x" << std::hex << imm;
expr << smt2lib_bv(imm, REG_Size(reg1));

symbolicElement *elem = symbolicEngine->newSymbolicElement(expr);
symbolicEngine->symbolicReg[reg1_ID] = elem->getID();
Expand Down Expand Up @@ -125,58 +126,15 @@ VOID movRegMem(std::string insDis, ADDRINT insAddr, REG reg1, UINT64 mem, UINT32
symbolicEngine->addSymVarMemoryReference(mem, symVarID);
}
else {
switch(readSize){
case 1:
switch(opcode){
case XED_ICLASS_MOV:
expr << "0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT8 *>(mem)));
break;
case XED_ICLASS_MOVSX:
expr << "((_ sign_extend " << std::dec << size << ") 0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT8 *>(mem))) << ")";
break;
case XED_ICLASS_MOVZX:
expr << "((_ zero_extend " << std::dec << size << ") 0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT8 *>(mem))) << ")";
break;
}
break;
case 2:
switch(opcode){
case XED_ICLASS_MOV:
expr << "0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT16 *>(mem)));
break;
case XED_ICLASS_MOVSX:
expr << "((_ sign_extend " << std::dec << size << ") 0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT16 *>(mem))) << ")";
break;
case XED_ICLASS_MOVZX:
expr << "((_ zero_extend " << std::dec << size << ") 0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT16 *>(mem))) << ")";
break;
}
switch(opcode){
case XED_ICLASS_MOV:
expr << smt2lib_bv(derefMem(mem, readSize), readSize);
break;
case 4:
switch(opcode){
case XED_ICLASS_MOV:
expr << "0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT32 *>(mem)));
break;
case XED_ICLASS_MOVSX:
expr << "((_ sign_extend " << std::dec << size << ") 0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT32 *>(mem))) << ")";
break;
case XED_ICLASS_MOVZX:
expr << "((_ zero_extend " << std::dec << size << ") 0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT32 *>(mem))) << ")";
break;
}
case XED_ICLASS_MOVSX:
expr << "((_ sign_extend " << std::dec << size << ") " << smt2lib_bv(derefMem(mem, readSize), readSize) << ")";
break;
case 8:
switch(opcode){
case XED_ICLASS_MOV:
expr << "0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT64 *>(mem)));
break;
case XED_ICLASS_MOVSX:
expr << "((_ sign_extend " << std::dec << size << ") 0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT64 *>(mem))) << ")";
break;
case XED_ICLASS_MOVZX:
expr << "((_ zero_extend " << std::dec << size << ") 0x" << std::hex << static_cast<UINT64>(*(reinterpret_cast<UINT64 *>(mem))) << ")";
break;
}
case XED_ICLASS_MOVZX:
expr << "((_ zero_extend " << std::dec << size << ") " << smt2lib_bv(derefMem(mem, readSize), readSize) << ")";
break;
}
}
Expand Down Expand Up @@ -215,7 +173,7 @@ VOID movMemReg(std::string insDis, ADDRINT insAddr, CONTEXT *ctx, REG reg1, UINT
if (symbolicEngine->symbolicReg[reg1_ID] != (UINT64)-1)
expr << "#" << symbolicEngine->symbolicReg[reg1_ID];
else
expr << "0x" << std::hex << PIN_GetContextReg(ctx, getHighReg(reg1));
expr << smt2lib_bv(PIN_GetContextReg(ctx, getHighReg(reg1)), writeSize);

symbolicElement *elem = symbolicEngine->newSymbolicElement(expr);
elem->isTainted = !TAINTED;
Expand Down Expand Up @@ -259,7 +217,7 @@ VOID movMemImm(std::string insDis, ADDRINT insAddr, UINT64 imm, UINT64 mem, UINT
std::list<UINT64>::iterator i;
std::stringstream expr, taint;

expr << "0x" << std::hex << imm;
expr << smt2lib_bv(imm, writeSize);

symbolicElement *elem = symbolicEngine->newSymbolicElement(expr);
elem->isTainted = !TAINTED;
Expand Down
8 changes: 4 additions & 4 deletions src/ir/pop.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ static VOID setMem(std::string insDis, ADDRINT insAddr, CONTEXT *ctx, REG reg1,
if (symbolicEngine->isMemoryReference(mem) != -1)
expr << "#" << std::dec << symbolicEngine->isMemoryReference(mem);
else
expr << "0x" << std::hex << derefMem(mem, readSize);
expr << smt2lib_bv(derefMem(mem, readSize), readSize);

symbolicElement *elem = symbolicEngine->newSymbolicElement(expr);
symbolicEngine->symbolicReg[reg1_ID] = elem->getID();
Expand All @@ -41,11 +41,11 @@ static VOID alignStack(std::string insDis, ADDRINT insAddr, CONTEXT *ctx, UINT64
{
std::stringstream expr, taint;

/* Sub RSP */
/* Add RSP */
if (symbolicEngine->symbolicReg[ID_RSP] != (UINT64)-1)
expr << "(+ #" << std::dec << symbolicEngine->symbolicReg[ID_RSP] << " 8)";
expr << "(+ #" << std::dec << symbolicEngine->symbolicReg[ID_RSP] << " " << smt2lib_bv(8, REG_Size(REG_RSP)) << ")";
else
expr << "(+ 0x" << std::hex << PIN_GetContextReg(ctx, REG_RSP) << " 8)";
expr << "(+ " << smt2lib_bv(PIN_GetContextReg(ctx, REG_RSP), REG_Size(REG_RSP)) << " " << smt2lib_bv(8, REG_Size(REG_RSP)) << ")";

symbolicElement *elem = symbolicEngine->newSymbolicElement(expr);
symbolicEngine->symbolicReg[ID_RSP] = elem->getID();
Expand Down
8 changes: 4 additions & 4 deletions src/ir/push.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@ static VOID alignStack(std::string insDis, ADDRINT insAddr, CONTEXT *ctx, UINT64

/* Sub RSP */
if (symbolicEngine->symbolicReg[ID_RSP] != (UINT64)-1)
expr << "(- #" << std::dec << symbolicEngine->symbolicReg[ID_RSP] << " 8)";
expr << "(- #" << std::dec << symbolicEngine->symbolicReg[ID_RSP] << " " << smt2lib_bv(8, REG_Size(REG_RSP)) << ")";
else
expr << "(- 0x" << std::hex << PIN_GetContextReg(ctx, REG_RSP) << " 8)";
expr << "(- " << smt2lib_bv(PIN_GetContextReg(ctx, REG_RSP), REG_Size(REG_RSP)) << " " << smt2lib_bv(8, REG_Size(REG_RSP)) << ")";

symbolicElement *elem = symbolicEngine->newSymbolicElement(expr);
symbolicEngine->symbolicReg[ID_RSP] = elem->getID();
Expand All @@ -36,7 +36,7 @@ static VOID setMemReg(std::string insDis, ADDRINT insAddr, CONTEXT *ctx, REG reg
if (symbolicEngine->symbolicReg[reg1_ID] != (UINT64)-1)
expr << "#" << std::dec << symbolicEngine->symbolicReg[reg1_ID];
else
expr << "0x" << std::hex << PIN_GetContextReg(ctx, getHighReg(reg1));
expr << smt2lib_bv(PIN_GetContextReg(ctx, getHighReg(reg1)), writeSize);

symbolicElement *elem = symbolicEngine->newSymbolicElement(expr);

Expand Down Expand Up @@ -64,7 +64,7 @@ static VOID setMemImm(std::string insDis, ADDRINT insAddr, CONTEXT *ctx, UINT64
{
std::stringstream expr, taint;

expr << "0x" << std::hex << imm;
expr << smt2lib_bv(imm, writeSize);

symbolicElement *elem = symbolicEngine->newSymbolicElement(expr);

Expand Down

0 comments on commit b75bb94

Please sign in to comment.