code

dse/src/Runtime.cpp

@@ -13,14 +13,14 @@
 
 #define ICMP_EQ     32  ///< equal
 #define ICMP_NE     33  ///< not equal
-#define ICMP_UGT    34  ///< unsigned greater than
-#define ICMP_UGE    35  ///< unsigned greater or equal
-#define ICMP_ULT    36  ///< unsigned less than
-#define ICMP_ULE    37  ///< unsigned less or equal
 #define ICMP_SGT    38  ///< signed greater than
 #define ICMP_SGE    39  ///< signed greater or equal
 #define ICMP_SLT    40  ///< signed less than
 #define ICMP_SLE    41  ///< signed less or equal
+#define ICMP_UGT    34  ///< unsigned greater than
+#define ICMP_UGE    35  ///< unsigned greater or equal
+#define ICMP_ULT    36  ///< unsigned less than
+#define ICMP_ULE    37  ///< unsigned less or equal
 
 extern SymbolicInterpreter SI;
 using namespace z3;

dse/src/Strategy.cpp

@@ -16,11 +16,6 @@ void recordBranches(z3::expr_vector &OldVec){
             Branches.push_back(E.to_string().c_str());
         }
     }
-    /*
-    for(const auto  &E : Branches){
-        printf("%s\n", E.c_str());
-    }
-     */
 }
 
 void searchStrategy(z3::expr_vector &OldVec) {
@@ -34,34 +29,22 @@ void searchStrategy(z3::expr_vector &OldVec) {
         searchStrategy(OldVec);
         return;
     }
-    //printf("e%d:%s\n\n",i, e.to_string().c_str());
     if(e.to_string().substr(1, 3) != NOT){
         std::string newExpr = e.to_string();
-        //printf("expr0:%s\n", newExpr.c_str());
         if(newExpr.find("false") != std::string::npos){
             newExpr = newExpr.replace(newExpr.end()-6, newExpr.end()-1,"true");
         } else{
             newExpr = newExpr.replace(newExpr.end()-5, newExpr.end()-1,"false");
         }
-        //printf("expr1:%s\n", newExpr.c_str());
         if(std::find(Branches.begin(), Branches.end(), newExpr) == Branches.end()){
-            //printf("newpath\n");
             OldVec.pop_back();
             OldVec.push_back(not e);
-            //printf("new\n");
-            /*
-            for(auto EX : OldVec){
-                printf("%s\n", EX.to_string().c_str());
-            }
-             */
         } else{
-            //printf("back\n");
             OldVec.pop_back();
             searchStrategy(OldVec);
         }
     }
     else {
-        //printf("unsat\n");
         OldVec.pop_back();
         searchStrategy(OldVec);
     }

dse/test/branch0.c

@@ -11,16 +11,16 @@ int main() {
   DSE_Input(z);
 
   if (x == 1) {
-  //if(x + y == x - z) {
 	 if (y == z) {
 		x = x / (y-z);
 	 }
-  }
-  else {
+  } else {
   	if(x == 0){
-  		x = 0;
+  		x = 1;
   	}
   }
 
   return 0;
 }
+
+

dse/test/branch1.c

@@ -19,3 +19,5 @@ int main() {
 
   return 0;
 }
+
+

dse/test/branch2.c

@@ -15,14 +15,7 @@ int main() {
 	x = x / z;
   }
   
-  /*
-  if(x>y){
-  	if(y>z){
-  		if(z==0){
-  			x = x/z;
-  		}
-  	}
-  }
-	*/
   return 0;
 }
+
+