Release Assignment-2

Author: yuleisui

Assignment-2/Assignment-2.cpp

@@ -66,11 +66,11 @@ bool SSE::handleRet(const RetCFGEdge* retEdge) {
 
 /// TODO: Implement handling of branch statements inside a function
 /// Return true if the path is feasible, false otherwise.
-/// A given branch on the ICFG looks like the following:
+/// A given if/else branch on the ICFG looks like the following:
 ///       	     ICFGNode1 (condition %cmp)
 ///       	     1	/    \  0
 ///       	  ICFGNode2   ICFGNode3
-/// edge->getCondition() returns the branch condition variable (%cmp) of type SVFValue* (for if/else) or a numeric condition variable (for switch). 
+/// edge->getCondition() returns the branch condition variable (%cmp) of type SVFValue* (for if/else) or a numeric condition variable (for switch).
 /// Given the condition variable, you could obtain the SVFVar ID via "svfir->getValueNode(edge->getCondition())""
 /// edge->getCondition() returns nullptr if this IntraCFGEdge is not a branch.
 /// edge->getSuccessorCondValue() returns the actual condition value (1/0 for if/else) when this branch/IntraCFGEdge is executed. For example, the successorCondValue is 1 on the edge from ICFGNode1 to ICFGNode2, and 0 on the edge from ICFGNode1 to ICFGNode3
@@ -159,10 +159,6 @@ bool SSE::handleNonBranch(const IntraCFGEdge* edge) {
 				assert(false && "implement this part");
 			}
 		}
-		else if (const BranchStmt *br = SVFUtil::dyn_cast<BranchStmt>(stmt))
-		{
-			DBOP(std::cout << "\t skip handled when traversal Conditional IntraCFGEdge \n");
-		}
 		else if (const SelectStmt *select = SVFUtil::dyn_cast<SelectStmt>(stmt)) {
 			expr res = getZ3Expr(select->getResID());
 			expr tval = getZ3Expr(select->getTrueValue()->getId());
@@ -184,6 +180,9 @@ bool SSE::handleNonBranch(const IntraCFGEdge* edge) {
 			}
 			assert(opINodeFound && "predecessor ICFGNode of this PhiStmt not found?");
 		}
+		else {
+			DBOP(std::cout << "\t skip handling BranchStmt/Call/Ret as they have been processed \n");
+		}
 	}
 
 	return true;
@@ -220,4 +219,4 @@ void SSE::analyse() {
 			resetSolver();
 		}
 	}
-}
+}

Assignment-2/Assignment-2.h

@@ -72,9 +72,9 @@ namespace SVF {
 			        && (fun->getName() == "assert" || fun->getName() == "svf_assert" || fun->getName() == "sink"));
 		}
 
-		/// clear visited and callstack
+		/// reset z3 solver
 		virtual void resetSolver() {
-			visited.clear();
+			getSolver().reset();
 		}
 
 		/// TODO: Implementing the collection the ICFG paths
@@ -114,19 +114,20 @@ namespace SVF {
 			       && "last node is not an assert call?");
 			DBOP(std::cout << "\n## Analyzing " << callnode->toString() << "\n");
 			z3::expr arg0 = getZ3Expr(callnode->getActualParms().at(0)->getId());
-			addToSolver(arg0 > 0);
-			if (getSolver().check() == z3::unsat) {
+			addToSolver(arg0 == getCtx().int_val(0));
+			if (getSolver().check() != z3::unsat) {
 				DBOP(printExprValues());
 				std::stringstream ss;
 				ss << "The assertion is unsatisfiable!! ("<< inode->toString() << ")" << "\n";
+				ss << "Counterexample: " << getSolver().get_model() << "\n";
 				SVFUtil::outs() << ss.str() << std::endl;
 				assert(false);
 				return false;
 			}
 			else {
 				DBOP(printExprValues());
 				std::stringstream ss;
-                ss << "The assertion is successfully verified!! ("<< inode->toString() << ")" << "\n";
+				ss << "The assertion is successfully verified!! ("<< inode->toString() << ")" << "\n";
 				SVFUtil::outs() << ss.str() << std::endl;
 				return true;
 			}
@@ -136,6 +137,14 @@ namespace SVF {
 			return paths;
 		}
 
+		void pushCallingCtx(const SVFInstruction* c) {
+			callingCtx.push_back(c);
+		}
+
+		void popCallingCtx() {
+			callingCtx.pop_back();
+		}
+
 		inline z3::solver& getSolver() {
 			return z3Mgr->getSolver();
 		}
@@ -152,7 +161,7 @@ namespace SVF {
 
 		/// Return Z3 expression based on ValVar ID
 		inline z3::expr getZ3Expr(NodeID idx) const {
-			return z3Mgr->getZ3Expr(idx);
+			return z3Mgr->getZ3Expr(idx, callingCtx);
 		}
 
 		/// Return Z3 expression based on ObjVar ID
@@ -166,7 +175,7 @@ namespace SVF {
 
 		/// Dump values of all exprs
 		inline void printExprValues() {
-			z3Mgr->printExprValues();
+			z3Mgr->printExprValues(callingCtx);
 		}
 
 		static u32_t assert_checked;
@@ -181,6 +190,7 @@ namespace SVF {
 		SVFIR* svfir;
 		Set<ICFGEdgeStackPair> visited;
 		CallStack callstack;
+		CallStack callingCtx;
 		std::vector<const ICFGEdge*> path;
 
 		std::set<const ICFGNode*> sources;

Assignment-2/Z3SSEMgr.cpp

@@ -39,59 +39,18 @@ using namespace z3;
 Z3SSEMgr::Z3SSEMgr(SVFIR* ir)
 : Z3Mgr(ir->getPAGNodeNum() * 10)
 , svfir(ir) {
-	initMap();
 }
 
-/*
- * (1) Create Z3 expressions for top-level variables and objects, and (2) create loc2val map
- */
-void Z3SSEMgr::initMap() {
-	for (SVFIR::iterator nIter = svfir->begin(); nIter != svfir->end(); ++nIter) {
-		if (const ValVar* val = SVFUtil::dyn_cast<ValVar>(nIter->second))
-			createExprForValVar(val);
-		else if (const ObjVar* obj = SVFUtil::dyn_cast<ObjVar>(nIter->second))
-			createExprForObjVar(obj);
-		else
-			assert(false && "SVFVar type not supported");
-	}
-	DBOP(printExprValues());
-}
-
-/*
- * We initialize all ValVar to be an int expression.
- * ValVar of PointerTy/isFunctionTy is assigned with an ID to represent the address of an object
- * ValVar of IntegerTy is assigned with an integer value
- * ValVar of FloatingPointTy is assigned with an integer value casted from a float
- * ValVar of StructTy/ArrayTy is assigned with their elements of the above types in the form of integer values
- */
-z3::expr Z3SSEMgr::createExprForValVar(const ValVar* valVar) {
-	std::string str;
-	raw_string_ostream rawstr(str);
-	rawstr << "ValVar" << valVar->getId();
-	expr e(ctx);
-	if (const SVFType* type = valVar->getType()) {
-		e = ctx.int_const(rawstr.str().c_str());
-	}
-	else {
-		e = ctx.int_const(rawstr.str().c_str());
-		assert(SVFUtil::isa<DummyValVar>(valVar) && "not a DummValVar if it has no type?");
-	}
-
-	updateZ3Expr(valVar->getId(), e);
-	return e;
-}
 
 /*
- * Object must be either a constraint data or a location value (address-taken variable)
+ * Object must be either a constaint data or a location value (address-taken variable)
  * Constant data includes ConstantInt, ConstantFP, ConstantPointerNull and ConstantAggregate
  * Locations includes pointers to globals, heaps, stacks
  */
 z3::expr Z3SSEMgr::createExprForObjVar(const ObjVar* objVar) {
 	std::string str;
 	raw_string_ostream rawstr(str);
-	rawstr << "ObjVar" << objVar->getId();
-
-	expr e = ctx.int_const(rawstr.str().c_str());
+	expr e(ctx);
 	if (objVar->hasValue()) {
 		const MemObj* obj = objVar->getMemObj();
 		/// constant data
@@ -122,30 +81,63 @@ z3::expr Z3SSEMgr::createExprForObjVar(const ObjVar* objVar) {
 		       && "it should either be a blackhole or constant dummy if this obj has no value?");
 		e = ctx.int_val(getVirtualMemAddress(objVar->getId()));
 	}
-
-	updateZ3Expr(objVar->getId(), e);
 	return e;
 }
 
+std::string Z3SSEMgr::callingCtxToStr(const CallStack& callingCtx) {
+	std::string str;
+	std::stringstream rawstr(str);
+	rawstr << "ctx:[ ";
+	for (const auto &inst : callingCtx) {
+
+		rawstr << svfir->getICFG()->getICFGNode(inst)->getId() << " ";
+	}
+	rawstr << "] ";
+	return rawstr.str();
+}
+
+z3::expr Z3SSEMgr::getZ3Expr(SVF::u32_t idx, const CallStack& callingCtx) {
+	u32_t varId = getInternalID(idx);
+	assert(varId == idx && "SVFVar idx overflow > 0x7f000000?");
+	std::string str;
+	std::stringstream rawstr(str);
+	const SVFVar *svfVar = svfir->getGNode(varId);
+	if (const ObjVar* objVar = SVFUtil::dyn_cast<ObjVar>(svfVar)) {
+		return createExprForObjVar(objVar);
+	} else {
+
+		// Check if svfVar does not have a value or it has a constant value
+		if (svfVar->hasValue() && !SVFUtil::isa<SVFConstant>(svfVar->getValue())) {
+			// If there is a non-constant value, add callingCtx to z3 expr
+			rawstr << callingCtxToStr(callingCtx);
+		} else {
+			// If there's no value or it's a constant, we do not add the callingCtx to z3 expr
+		}
+		rawstr << "ValVar" << varId;
+		std::string name = rawstr.str();
+		return ctx.int_const(name.c_str());
+	}
+}
+
 /// Return the address expr of a ObjVar
-z3::expr Z3SSEMgr::getMemObjAddress(u32_t idx) const {
+z3::expr Z3SSEMgr::getMemObjAddress(u32_t idx) {
 	NodeID objIdx = getInternalID(idx);
 	assert(SVFUtil::isa<ObjVar>(svfir->getGNode(objIdx)) && "Fail to get the MemObj!");
-	return getZ3Expr(objIdx);
+	return createExprForObjVar(SVFUtil::cast<ObjVar>(svfir->getGNode(objIdx)));
 }
 
 z3::expr Z3SSEMgr::getGepObjAddress(z3::expr pointer, u32_t offset) {
-	NodeID baseObj = getInternalID(z3Expr2NumValue(pointer));
-	assert(SVFUtil::isa<ObjVar>(svfir->getGNode(baseObj)) && "Fail to get the base object address!");
-	NodeID gepObj = svfir->getGepObjVar(baseObj, offset);
+	NodeID obj = getInternalID(z3Expr2NumValue(pointer));
+	assert(SVFUtil::isa<ObjVar>(svfir->getGNode(obj)) && "Fail to get the base object address!");
+	NodeID gepObj = svfir->getGepObjVar(obj, offset);
 	/// TODO: check whether this node has been created before or not to save creation time
-	if (baseObj == gepObj)
-		return getZ3Expr(baseObj);
+	if (obj == gepObj)
+		return createExprForObjVar(SVFUtil::cast<ObjVar>(svfir->getGNode(obj)));
 	else
 		return createExprForObjVar(SVFUtil::cast<GepObjVar>(svfir->getGNode(gepObj)));
 }
 
-s32_t Z3SSEMgr::getGepOffset(const GepStmt* gep) {
+s32_t Z3SSEMgr::getGepOffset(const GepStmt* gep, const CallStack& callingCtx) {
 	if (gep->getOffsetVarAndGepTypePairVec().empty())
 		return gep->getConstantStructFldIdx();
 
@@ -160,14 +152,14 @@ s32_t Z3SSEMgr::getGepOffset(const GepStmt* gep) {
 			offset = op->getSExtValue();
 		/// variable as the offset
 		else
-			offset = z3Expr2NumValue(getZ3Expr(svfir->getValueNode(value)));
+			offset = z3Expr2NumValue(getZ3Expr(svfir->getValueNode(value), callingCtx));
 
 		if (type == nullptr) {
 			totalOffset += offset;
 			continue;
 		}
 
-		/// Calculate the offset
+		/// Caculate the offset
 		if (const SVFPointerType* pty = SVFUtil::dyn_cast<SVFPointerType>(type))
 			totalOffset += offset * gep->getAccessPath().getElementNum(gep->getAccessPath().gepSrcPointeeType());
 		else
@@ -176,14 +168,14 @@ s32_t Z3SSEMgr::getGepOffset(const GepStmt* gep) {
 	return totalOffset;
 }
 
-void Z3SSEMgr::printExprValues() {
+void Z3SSEMgr::printExprValues(const CallStack& callingCtx) {
 	std::cout.flags(std::ios::left);
-	std::cout << "-----------SVFVar and Value-----------\n";
+	std::cout << "\n-----------SVFVar and Value-----------\n";
 	std::map<std::string, std::string> printValMap;
 	std::map<NodeID, std::string> objKeyMap;
 	std::map<NodeID, std::string> valKeyMap;
 	for (SVFIR::iterator nIter = svfir->begin(); nIter != svfir->end(); ++nIter) {
-		expr e = getEvalExpr(getZ3Expr(nIter->first));
+		expr e = getEvalExpr(getZ3Expr(nIter->first, callingCtx));
 		if (e.is_numeral()) {
 			NodeID varID = nIter->second->getId();
 			s32_t value = e.get_numeral_int64();
@@ -230,4 +222,4 @@ void Z3SSEMgr::printExprValues() {
 		std::cout << std::setw(25) << printKey << printValMap[printKey];
 	}
 	std::cout << "-----------------------------------------\n";
-}
+}

Assignment-2/Z3SSEMgr.h

@@ -29,6 +29,7 @@
 #define SOFTWARE_SECURITY_ANALYSIS_Z3SSEMGR_H
 
 #include "Z3Mgr.h"
+#include "SVFIR/SVFIR.h"
 
 namespace SVF {
 
@@ -38,38 +39,35 @@ namespace SVF {
 	class GepStmt;
 
 	class Z3SSEMgr : public Z3Mgr {
+		typedef std::vector<const SVFInstruction*> CallStack;
 	 public:
 		/// Constructor
 		Z3SSEMgr(SVFIR* ir);
 
-		/// Initialize map (varID2ExprMap: ID->expr)from VARID to z3 expr                                            ---
-		/// Using elements from 0 to lastSlot Initialize map (loc2ValMap: ID->ID) from Location (pointer address) to
-		/// Value    --- Using the last slot V = L U C    (V is SVFVar, L is Pointers + Nonconst Objects, C is Constants
-		/// ) loc2ValMap : IDX(L) -> IDX(V) idx \in IDX(V) (IDX is a set of Indices of all SVFVars)
-		void initMap();
 
-		/// Declare the expr type for each top-level pointers
-		z3::expr createExprForValVar(const ValVar* val);
+		std::string callingCtxToStr(const CallStack& callingCtx);
+
+		z3::expr getZ3Expr(u32_t idx, const CallStack& callingCtx);
 
 		/// Initialize the expr value for each objects (address-taken variables and constants)
 		z3::expr createExprForObjVar(const ObjVar* obj);
 
 		/// Return the address expr of a ObjVar
-		z3::expr getMemObjAddress(u32_t idx) const;
+		z3::expr getMemObjAddress(u32_t idx);
 
 		/// Return the field address given a pointer points to a struct object and an offset
 		z3::expr getGepObjAddress(z3::expr pointer, u32_t offset);
 
 		/// Return the offset expression of a GepStmt
-		s32_t getGepOffset(const GepStmt* gep);
+		s32_t getGepOffset(const GepStmt* gep, const CallStack& callingCtx);
 
 		/// Dump values of all exprs
-		virtual void printExprValues();
+		virtual void printExprValues(const CallStack& callingCtx);
 
 	 private:
 		SVFIR* svfir;
 	};
 
 } // namespace SVF
 
-#endif // SOFTWARE_SECURITY_ANALYSIS_Z3MGR_H
+#endif // SOFTWARE_SECURITY_ANALYSIS_Z3MGR_H