fix parser error, add parser module test

CMakeLists.txt

@@ -1,5 +1,5 @@
 cmake_minimum_required (VERSION 2.8)
-set(Nv 3)
+set(Nv 2)
 add_definitions(-D__SELECTIVE_SAMPLING_ENABLED)
 project(zilu CXX)
 set(PRECISION 3)
@@ -62,7 +62,7 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/cmake/")
 find_package(Z3 REQUIRED)
 find_package(GSL REQUIRED)
 
-add_subdirectory(parser)
+#add_subdirectory(parser)
 
 configure_file(config.h.in ../include/config.h)
 # using for windows
@@ -74,7 +74,7 @@ configure_file(config.h.in ../include/config.h)
 # add include dir and source dir into project
 include_directories (include)
 aux_source_directory(src DIR_SRCS)
-add_executable(05 /home/lijiaying/Research/zilu/test/05.cpp ${DIR_SRCS})
-target_link_libraries(05 ${Z3_LIBRARY})
-target_link_libraries(05 ${GSL_LIBRARIES})
-target_link_libraries(05 gsl gslcblas m)
+add_executable(09 /home/lijiaying/Research/zilu/test/09.cpp ${DIR_SRCS})
+target_link_libraries(09 ${Z3_LIBRARY})
+target_link_libraries(09 ${GSL_LIBRARIES})
+target_link_libraries(09 gsl gslcblas m)

cfg/f2.cpp

@@ -0,0 +1,48 @@
+#include "iif.h"
+#include <iostream>
+using namespace std;
+using namespace iif;
+
+int loopFunction(int _reserved_input_[]) {
+	int x = _reserved_input_[0];
+	int y = _reserved_input_[1];
+	int z = _reserved_input_[2];
+	int w = _reserved_input_[3];
+
+	iif_assume(x==0&&y==0&&z==0&&w==0);
+
+	while(rand()%2) {
+		recordi(x, y, z, w);
+		if(rand()%2){
+		x++;
+		y=y+2;
+		}
+		else if(rand()%2){
+		if(x>=4){
+		x++;
+		y=y+3;
+		z=z+10;
+		w=w+10;
+		}
+		}
+		else if(x>=z&&w>=y+1){
+		x=-x;
+		y=-y;
+		}
+
+	}
+	recordi(x, y, z, w);
+
+	iif_assert(3*x>y-1);
+
+	return 0;
+}
+
+int main(int argc, char** argv) {
+	iifround = atoi(argv[1]);
+	initseed = atoi(argv[2]);
+	iifContext context("/home/lijiaying/Research/GitHub/zilu/tmp/f2.var", loopFunction, "loopFunction", "/home/lijiaying/Research/GitHub/zilu/tmp/f2.ds");
+	context.addLearner("conjunctive");
+	return context.learn("/home/lijiaying/Research/GitHub/zilu/tmp/f2.cnt", "/home/lijiaying/Research/GitHub/zilu/tmp/f2");
+}
+

include/config.h

@@ -20,7 +20,7 @@
  *		   This should be set in /CMakeLists.txt file
  *		   If it is not set correctly, you may come across a runtime error
  */
-#define Nv 3 
+#define Nv 2 
 
 /*#define Cv(i) do {int return_num##i = 1;\
   for (int tempi = 0; tempi < i; i++) return_num##i *= (Nv + i);\

parser/lex.l

@@ -5,12 +5,13 @@
 #include "parser.hpp"
 
 static int n_names = 0;
+static int n_symbs = 0;
 static int n_learners = 0;
 
 
 %}
 %option noyywrap
-%start NAMELIST LEARNERLIST STRSTART 
+%start NAMELIST LEARNERLIST SYMBLIST STRSTART 
 %%
 <INITIAL>[ \t]	    		;
 <INITIAL>#.*\n		 		;
@@ -32,13 +33,28 @@ static int n_learners = 0;
 <INITIAL>"postcondition="	{ BEGIN STRSTART; yylval.tag = PSTC; return TAG; }
 <INITIAL>"afterloop="       { BEGIN STRSTART; yylval.tag = ALOOP; return TAG; }
 <INITIAL>"invariant="       { BEGIN STRSTART; yylval.tag = INVR; /*printf("encounter INVARIANT.\n");*/ return TAG; }
+<INITIAL>"fakesymbolic="    { BEGIN STRSTART; printf("-->fake[symlist]: \n");  yylval.tag = INVR; /*printf("encounter INVARIANT.\n");*/ return TAG; }
 <STRSTART>[^\n]*\n			{ yytext[yyleng-1] = '\0';
 							  /*printf("\t[%d]->%s\n", yylval.tag, yytext);*/ 
 							  yylval.pstr = new std::string(yytext); 
 							  BEGIN INITIAL;
 							  return STRING; 
 							}
 
+<INITIAL>"symbolic="     	{ /*printf("-->MODE[symlist]: \n");*/
+								BEGIN SYMBLIST; 
+								/*printf("-goto->SYMBLIST \n");*/
+								return SYMBS; }
+<SYMBLIST>[a-zA-Z_][a-zA-Z_0-9]*  { 
+								n_symbs++; 
+								/*printf("\t[%d]->%s\n", n_symbs, yytext);*/ 
+								yylval.pstr = new std::string(yytext); 
+								return STRING; 
+							}
+<SYMBLIST>[ \t]         	;
+<SYMBLIST>\n				{ /*printf("<--MODE[symblist]\n");*/ BEGIN INITIAL; }
+<SYMBLIST>.					{ printf("Unexpected char[%c] in symblist\n", yytext[0]); BEGIN INITIAL; }
+
 <INITIAL>"learners="        { BEGIN LEARNERLIST; return LEARNERS; }
 <LEARNERLIST>[a-zA-Z_][a-zA-Z_0-9]*  { 
 								n_learners++; 

parser/loop_handler.hpp

@@ -78,6 +78,7 @@ class LoopHandler {
 		std::string toCFile4Init(int positive) {
 			// used for verifying the invariant candidate
 			std::ostringstream stm;
+			//cout << "in cfile 4 init.\n";
 			stm << toKleeInclude() << "\n"
 				<< toKleeMain4Init(positive);
 			return stm.str();
@@ -89,6 +90,12 @@ class LoopHandler {
 				return ";";
 			ostringstream stm;
 			std::size_t last = -1;
+			for (int i = 0; i < loop->symbs->n; i++) {
+				for (int j=0; j<tabs; j++) {
+					stm << "\t";
+				}
+				stm << "\tint " << loop->symbs->u[i] << " = rand() % 2;\n";
+			}
 			while (true) {
 				for (int i=0; i<tabs; i++)
 					stm << "\t";
@@ -137,8 +144,12 @@ class LoopHandler {
 			stm << "int main() {\n"; 
 			for (int i = 0; i < loop->names->n; i++) 
 				stm << "\tint " << loop->names->u[i] << ";\n";
+			for (int i = 0; i < loop->symbs->n; i++) 
+				stm << "\tint " << loop->symbs->u[i] << ";\n";
 			for (int i = 0; i < loop->names->n; i++) 
 				stm << "\tklee_make_symbolic(&" << loop->names->u[i] <<", sizeof(" << loop->names->u[i] << "), \"" << loop->names->u[i] << "\");\n";
+			for (int i = 0; i < loop->symbs->n; i++) 
+				stm << "\tklee_make_symbolic(&" << loop->symbs->u[i] <<", sizeof(" << loop->symbs->u[i] << "), \"" << loop->symbs->u[i] << "\");\n";
 			// before loop statements;
 			if (loop->beforeloop && loop->beforeloop->compare("") != 0)
 				stm << "\t" << *loop->beforeloop << "\n";
@@ -179,8 +190,12 @@ class LoopHandler {
 			stm << "int main() {\n"; 
 			for (int i = 0; i < loop->names->n; i++) 
 				stm << "\tint " << loop->names->u[i] << ";\n";
+			for (int i = 0; i < loop->symbs->n; i++) 
+				stm << "\tint " << loop->symbs->u[i] << ";\n";
 			for (int i = 0; i < loop->names->n; i++) 
 				stm << "\tklee_make_symbolic(&" << loop->names->u[i] <<", sizeof(" << loop->names->u[i] << "), \"" << loop->names->u[i] << "\");\n";
+			for (int i = 0; i < loop->symbs->n; i++) 
+				stm << "\tklee_make_symbolic(&" << loop->symbs->u[i] <<", sizeof(" << loop->symbs->u[i] << "), \"" << loop->symbs->u[i] << "\");\n";
 			// before loop statements;
 			if (loop->beforeloop && loop->beforeloop->compare("") != 0)
 				stm << "\t" << *loop->beforeloop << "\n";
@@ -207,8 +222,12 @@ class LoopHandler {
 			stm << "int main() {\n"; 
 			for (int i = 0; i < loop->names->n; i++) 
 				stm << "\tint " + loop->names->u[i] + ";\n";
+			for (int i = 0; i < loop->symbs->n; i++) 
+				stm << "\tint " << loop->symbs->u[i] << ";\n";
 			for (int i = 0; i < loop->names->n; i++) 
 				stm << "\tklee_make_symbolic(&" << loop->names->u[i] <<", sizeof(" << loop->names->u[i] << "), \"" << loop->names->u[i] << "\");\n";
+			for (int i = 0; i < loop->symbs->n; i++) 
+				stm << "\tklee_make_symbolic(&" << loop->symbs->u[i] <<", sizeof(" << loop->symbs->u[i] << "), \"" << loop->symbs->u[i] << "\");\n";
 			// before loop statements;
 			if (loop->beforeloop && loop->beforeloop->compare("") != 0)
 				stm << "\t" << *loop->beforeloop << "\n";

parser/node.hpp

@@ -54,6 +54,7 @@ class Branch{
 class Loop{
 	public:
 		NameList* names;
+		NameList* symbs;
 		std::string* beforeloop;
 		std::string* beforeloopinit;
 		std::string* precondition;
@@ -69,6 +70,8 @@ class Loop{
 			cout << "Loop-------------------------------------\n";
 			cout << " |---[namelist]---------------" << endl;
 			names->print(5);
+			cout << " |---[symblist]---------------" << endl;
+			symbs->print(5);
 			BLANKS(start); 
 			cout << " |---" << "[beforeloop] [|" << (beforeloop? *beforeloop:"NULL") << "|]" << endl;
 			BLANKS(start); 

parser/parser.hpp

@@ -30,8 +30,8 @@
    This special exception was added by the Free Software Foundation in
    version 2.2 of Bison.  */
 
-#ifndef YY_YY_HOME_LIJIAYING_RESEARCH_ZILU_BUILD_PARSER_PARSER_HPP_INCLUDED
-# define YY_YY_HOME_LIJIAYING_RESEARCH_ZILU_BUILD_PARSER_PARSER_HPP_INCLUDED
+#ifndef YY_YY_HOME_LIJIAYING_RESEARCH_ZILU_PARSER_BUILD_PARSER_HPP_INCLUDED
+# define YY_YY_HOME_LIJIAYING_RESEARCH_ZILU_PARSER_BUILD_PARSER_HPP_INCLUDED
 /* Debug traces.  */
 #ifndef YYDEBUG
 # define YYDEBUG 0
@@ -47,8 +47,9 @@ extern int yydebug;
   {
     NAMES = 258,
     LEARNERS = 259,
-    TAG = 260,
-    STRING = 261
+    SYMBS = 260,
+    TAG = 261,
+    STRING = 262
   };
 #endif
 
@@ -62,9 +63,10 @@ union YYSTYPE
 	tag_type tag;
 	std::string* pstr;
 	NameList* names;
+	NameList* symbs;
 	NameList* learners;
 
-#line 68 "/home/lijiaying/Research/zilu/build/parser/parser.hpp" /* yacc.c:1909  */
+#line 70 "/home/lijiaying/Research/zilu/parser/build/parser.hpp" /* yacc.c:1909  */
 };
 
 typedef union YYSTYPE YYSTYPE;
@@ -77,4 +79,4 @@ extern YYSTYPE yylval;
 
 int yyparse (void);
 
-#endif /* !YY_YY_HOME_LIJIAYING_RESEARCH_ZILU_BUILD_PARSER_PARSER_HPP_INCLUDED  */
+#endif /* !YY_YY_HOME_LIJIAYING_RESEARCH_ZILU_PARSER_BUILD_PARSER_HPP_INCLUDED  */

parser/parser.y

@@ -16,16 +16,17 @@ extern const std::string tag_name[];
 	tag_type tag;
 	std::string* pstr;
 	NameList* names;
+	NameList* symbs;
 	NameList* learners;
 }
 
 /* Define our terminal symbols (tokens). This should
    match our tokens.l lex file. We also define the node type
    they represent.
  */
-%token <tag> NAMES LEARNERS TAG
+%token <tag> NAMES LEARNERS SYMBS TAG
 %token <pstr> STRING
-%type <names> namelist learnerlist
+%type <names> namelist symblist learnerlist
 /*%type <nodes> stmtlist*/
 /*%type <loop_type> stmtlist*/
 %start root
@@ -37,12 +38,27 @@ root	: namelist stmtlist
 			loop->names = $1;
 			loop->learners = new NameList();
 		}
+		| namelist symblist stmtlist
+		{ 
+			//printf("reduce to root.\n"); 
+			loop->names = $1;
+			loop->symbs = $2;
+			loop->learners = new NameList();
+		}
 		| namelist stmtlist learnerlist stmtlist
 		{ 
 			//printf("reduce to root.\n"); 
 			loop->names = $1;
+			loop->symbs = new NameList();
 			loop->learners = $3;
 		}
+		| namelist stmtlist symblist stmtlist learnerlist stmtlist
+		{ 
+			//printf("reduce to root.\n"); 
+			loop->names = $1;
+			loop->symbs = $3;
+			loop->learners = $5;
+		}
 		;
 
 namelist: namelist STRING
@@ -59,6 +75,20 @@ namelist: namelist STRING
 		}
 		;
 
+symblist: symblist STRING
+		{
+			//cout << "addSYM<" << *$2 << ">" << endl;
+			$$ = $1;
+			$$->addName(*$2);
+		}
+		| SYMBS STRING
+		{ 
+			//cout << "addSYM<" << *$2 << ">" << endl;
+			$$ = new NameList();
+			$$->addName(*$2);
+		}
+		;
+
 learnerlist: learnerlist STRING
 		{
 			$$ = $1;
@@ -84,8 +114,9 @@ stmtlist: stmtlist TAG STRING
 
 int yyerror(char const *str)
 {
+	//cout << "in yyerror.\n";
 	extern char* yytext;
-	fprintf(stderr, "parser error near %s\n", yytext);
+	fprintf(stderr, "parser error near \"%s\"\n", yytext);
 	return 0;
 }
 

parser/parser_test.sh

@@ -0,0 +1,25 @@
+#/bin/bash
+
+if [ $? -lt 2 ]; then
+	file="./test/03.cfg"
+else
+	file=$1
+fi
+##########################################################################
+# Generate C files to verify using cfg file and inv file
+##########################################################################
+dir_parser=./build
+dir_temp=./tmp
+mkdir -p $dir_parser $dir_temp
+
+cd $dir_parser
+cmake ..
+make | cp parser.hpp ..
+make
+cd ..
+
+#echo -n -e $blue"Generating C files to get initial positive/negative value by KLEE..."$normal
+cat $file | $dir_parser"/parser" -t 5 -c 1 -o $dir_temp"/last.c"
+#cat $path_cfg | $dir_parser"/parser" -t 5 -c -1 -o $dir_temp"/"$prefix"_init2/"$file_c_init
+#echo -n -e $green$bold"[Done]"$normal
+

test/03.cpp

@@ -13,6 +13,7 @@ int loopFunction(int _reserved_input_[]) {
 
 	while(rand()%2) {
 		recordi(i, j);
+			int flag = rand() % 2;
 		x++;
 		y++;
 		i+=x;
@@ -30,8 +31,8 @@ int loopFunction(int _reserved_input_[]) {
 int main(int argc, char** argv) {
 	iifround = atoi(argv[1]);
 	initseed = atoi(argv[2]);
-	iifContext context("/home/lijiaying/Research/GitHub/zilu/tmp/03.var", loopFunction, "loopFunction", "/home/lijiaying/Research/GitHub/zilu/tmp/03.ds");
+	iifContext context("/home/lijiaying/Research/zilu/tmp/03.var", loopFunction, "loopFunction", "/home/lijiaying/Research/zilu/tmp/03.ds");
 	context.addLearner("linear");
-	return context.learn("/home/lijiaying/Research/GitHub/zilu/tmp/03.cnt", "/home/lijiaying/Research/GitHub/zilu/tmp/03");
+	return context.learn("/home/lijiaying/Research/zilu/tmp/03.cnt", "/home/lijiaying/Research/zilu/tmp/03");
 }