Lab2/Assignment2 comments and tips + launch.json

Author: yuleisui

.vscode/launch.json

@@ -2,8 +2,8 @@
   "version": "0.2.0",
   "configurations": [
     {
-      "name": "(lldb) Launch",
-      "type": "lldb",
+      "name": "(debug) Launch",
+      "type": "cppdbg",
       "request": "launch",
       // Please change to the executable of your current lab or assignment
       // |  Lab/Assignment  | "program"                          | "args"  |
@@ -16,7 +16,8 @@
       "program": "${workspaceFolder}/bin/hello",
       "args": [], // may input the test llvm bc file or other options and flags the program may use
       "cwd": "${workspaceFolder}",
-      "preLaunchTask": "C/C++: cpp build active file"
+      "preLaunchTask": "C/C++: cpp build active file",
+      "MIMode": "lldb"
     }
   ]
 }

Assignment-2/Assignment-2.cpp

@@ -35,16 +35,16 @@ using namespace z3;
 
 /// TODO: Implement your context-sensitive ICFG traversal here to traverse each program path (once for any loop) from
 /// You will need to collect each path from src node to snk node and then add the path to the `paths` set by
-/// implementing the `collectICFGPath` method. This implementation, slightly different from Assignment-1, requires
-/// ICFGNode* as the first argument.
+/// calling the `collectAndTranslatePath` method which is then trigger the path translation. 
+/// This implementation, slightly different from Assignment-1, requires ICFGNode* as the first argument.
 void SSE::reachability(const ICFGEdge* curEdge, const ICFGNode* snk) {
 	/// TODO: your code starts from here
 }
 
 /// TODO: collect each path once this method is called during reachability analysis, and
 /// Collect each program path from the entry to each assertion of the program. In this function,
 /// you will need (1) add each path into the paths set, (2) call translatePath to convert each path into Z3 expressions.
-/// Note that translatePath returns true if the path is feasible, infeasible otherwise. (3) If a path is feasible,
+/// Note that translatePath returns true if the path is feasible, false if the path is infeasible. (3) If a path is feasible,
 /// you will need to call assertchecking to verify the assertion (which is the last ICFGNode of this path).
 void SSE::collectAndTranslatePath() {
 	/// TODO: your code starts from here
@@ -64,8 +64,16 @@ bool SSE::handleRet(const RetCFGEdge* retEdge) {
 	return true;
 }
 
-/// TODO: Implement handling of branch statement inside a function
-/// Return true means a feasible path, false otherwise
+/// 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:
+///       	     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). 
+/// 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
 bool SSE::handleBranch(const IntraCFGEdge* edge) {
 	/// TODO: your code starts from here
 	return true;
@@ -100,6 +108,12 @@ bool SSE::handleNonBranch(const IntraCFGEdge* edge) {
 		{
 			// TODO: implement GepStmt handler here
 		}
+		/// Given a CmpStmt "r = a > b"
+		/// cmp->getOpVarID(0)/cmp->getOpVarID(1) returns the first/second operand, i.e., "a" and "b"
+		/// cmp->getResID() returns the result operand "r" and cmp->getPredicate() gives you the predicate ">"
+		/// Find the comparison predicates in "class CmpStmt:Predicate" under SVF/svf/include/SVFIR/SVFStatements.h
+		/// You are only required to handle integer predicates, including ICMP_EQ, ICMP_NE, ICMP_UGT, ICMP_UGE, ICMP_ULT, ICMP_ULE, ICMP_SGT, ICMP_SGE, ICMP_SLE
+		/// We assume integer-overflow-free in this assignment
 		else if (const CmpStmt *cmp = SVFUtil::dyn_cast<CmpStmt>(stmt))
 		{
 			// TODO: implement CmpStmt handler here
@@ -201,9 +215,9 @@ void SSE::analyse() {
 		assert(SVFUtil::isa<GlobalICFGNode>(src) && "reachability should start with GlobalICFGNode!");
 		for (const ICFGNode* sink : identifySinks()) {
 			const IntraCFGEdge startEdge(nullptr, const_cast<ICFGNode*>(src));
-			handleIntra(&startEdge);
+			/// start traversing from the entry to each assertion and translate each path
 			reachability(&startEdge, sink);
 			resetSolver();
 		}
 	}
-}
+}

Dockerfile

@@ -15,7 +15,7 @@ ENV HOME=/home/SVF-tools
 
 # Define dependencies.
 ENV lib_deps="cmake g++ gcc git zlib1g-dev libncurses5-dev libtinfo6 build-essential libssl-dev libpcre2-dev zip libzstd-dev"
-ENV build_deps="wget xz-utils git tcl software-properties-common"
+ENV build_deps="wget xz-utils git gdb tcl software-properties-common"
 
 # Fetch dependencies.
 RUN apt-get update --fix-missing
@@ -56,5 +56,6 @@ WORKDIR ${HOME}
 RUN git clone "https://github.com/SVF-tools/Software-Security-Analysis.git"
 WORKDIR ${HOME}/Software-Security-Analysis
 RUN echo "Building Software-Security-Analysis ..."
+RUN sed -i 's/lldb/gdb/g' ${HOME}/Software-Security-Analysis/.vscode/launch.json
 RUN cmake -DCMAKE_BUILD_TYPE=MinSizeRel .
 RUN make -j8

Lab-Exercise-2/CMakeLists.txt

@@ -8,10 +8,10 @@ target_link_libraries(lab2 ${SVF_LIB} ${llvm_libs} ${Z3_LIBRARIES})
 set_target_properties(lab2 PROPERTIES
         RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin )
 
-foreach (i RANGE 1 7)
+foreach (i RANGE 1 10)
     add_test(
             NAME lab2_test${i}
             COMMAND lab2 test${i}
             WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
     )
-endforeach ()
+endforeach ()

Lab-Exercise-2/test.cpp

@@ -98,10 +98,10 @@ int main(int argc, char** argv) {
 	}
 
 	if (result) {
-		std::cout << "The test-" << test_name << " passed!!" << std::endl;
+		std::cout << test_name << " passed!!" << std::endl;
 	}
 	else {
-		std::cout << SVFUtil::errMsg("The test-") << SVFUtil::errMsg(test_name)
+		std::cout << SVFUtil::errMsg(test_name)
 		          << SVFUtil::errMsg(" assertion is unsatisfiable!!") << std::endl;
 		assert(result);
 	}