ROSE  0.9.6a
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Groups Pages
yicesParserLib.h
Go to the documentation of this file.
1 #include <iostream>
2 #include <fstream>
3 #include <string>
4 #include <err.h>
5 #include <SgGraphTemplate.h>
6 #include <graphProcessing.h>
7 #include <staticCFG.h>
8 #include <yices_c.h>
9 /* Testing the graph traversal mechanism now implementing in AstProcessing.h (inside src/midend/astProcessing/)*/
10 
11 
12 using namespace std;
13 using namespace boost;
14 int FORLOOPS;
15 bool inconsistent;
16 yices_expr mainParse(vector<SgGraphNode*> expr, yices_context& ctx);
17 int qst;
18 
19 typedef myGraph CFGforT;
20 bool unknown_flag;
21 std::map<SgInitializedName*, yices_var_decl> unknowns;
22 std::map<yices_var_decl, SgInitializedName*> IName;
23 std::vector<yices_var_decl> unknownvdeclis;
24 bool usingNots;
25 std::map<SgInitializedName*, std::vector<int> > notMap;
26 //std::vector<yices_var_decl> unknowndecls;
27 
28 std::map<std::vector<SgGraphNode*>, std::set<int> > calledMap;
29 std::set<SgNode*> unknownFunctions;
30 
31 string getGraphNodeType(SgGraphNode* sn);
32 class visitorTraversalFunc : public SgGraphTraversal<CFGforT>
33  {
34  public:
35  int tltnodes;
36  std::vector<std::vector<SgGraphNode*> > vpaths;
37  void analyzePath(std::vector<VertexID>& pth);
38  CFGforT* orig;
39  //std::map<SgVariableSymbol, string> nameOf;
40  //int nvars;
41  };
42 
43 
44 void visitorTraversalFunc::analyzePath(std::vector<VertexID>& pathR) {
45  //ROSE_ASSERT(pathcheck.find(pathR) == pathcheck.end());
46  //pathcheck.insert(pathR);
47 
48  //std::cout << "funcAnalyze" << std::endl;
49  std::vector<SgGraphNode*> path;
50  for (unsigned int j = 0; j < pathR.size(); j++) {
51  SgGraphNode* R = (*orig)[pathR[j]].sg;
52  path.push_back(R);
53  }
54  ROSE_ASSERT(isSgFunctionDefinition(path[0]->get_SgNode()));
55  //int curr = 0;
56  //std::cout << "a vpath" << std::endl;
57  // for (int q = 0; q < path.size(); q++) {
58  // std::cout << getGraphNodeType(path[q]) << std::endl;
59  // }
60  // std::cout << "\n\n";
61  if (path.back()->get_SgNode() == path.front()->get_SgNode()) {
62  vpaths.push_back(path);
63  }
64 }
65 
66 
67 std::map<SgNode*, std::vector<std::vector<SgGraphNode*> > > FuncPathMap;
68 
69 bool forFlag;
70 
71 int nvars;
72 std::map<SgName, string> nameOf;
73 bool noAssert;
74 std::map<SgNode*, int> forsts;
75 
76 std::map<int, std::vector<SgGraphNode*> > intvecmap;
77 std::map<std::vector<SgGraphNode*>, int> vecintmap;
78 
79 typedef myGraph CFGforT;
80 
81 std::vector<std::vector<SgGraphNode*> > paths;
82 
83 struct Vertex2 {
84  SgGraphNode* sg;
85  bool vardec;
86  string varstr;
87  bool expr;
88  string exprstr;
89 };
90 
91 struct Edge2 {
92  SgDirectedGraphEdge* gedge;
93 };
94 
95 typedef boost::adjacency_list<
96  boost::vecS,
97  boost::vecS,
98  boost::bidirectionalS,
99  Vertex2,
100  Edge2
101 > newGraph;
102 
103 typedef newGraph::vertex_descriptor VertexID2;
104 typedef newGraph::edge_descriptor EdgeID2;
105 
106  typedef boost::graph_traits<newGraph>::vertex_iterator vertex_iterator;
107  typedef boost::graph_traits<newGraph>::out_edge_iterator out_edge_iterator;
108  typedef boost::graph_traits<newGraph>::in_edge_iterator in_edge_iterator;
109  typedef boost::graph_traits<newGraph>::edge_iterator edge_iterator;
110 
111 
163 //Process CFG representation into SMT
164 
165 
166 
167 void propagateFunctionCall(std::vector<SgGraphNode*> path, int i, int pathnum) {
168  SgFunctionDeclaration* sgfd = isSgFunctionCallExp(path[i]->get_SgNode())->getAssociatedFunctionDeclaration();
169  SgName nam = sgfd->get_qualified_name();
170  //std::cout << "function: " << nam.getString() << std::endl;
171  ROSE_ASSERT(sgfd != NULL);
172  SgFunctionDefinition* sgfdef = sgfd->get_definition();
173  ROSE_ASSERT(sgfdef != NULL);
174  int kk = i + 1;
175  int indiec = 0;
176  std::vector<std::vector<SgGraphNode*> > funcPaths = FuncPathMap[sgfdef];
177  ROSE_ASSERT(funcPaths.size() > 0);
178  int funcIndEnd = path[i]->get_SgNode()->cfgIndexForEnd();
179  if (path.size() > 1) {
180  // std::cout << "funcIndEnd: " << funcIndEnd << std::endl;
181 
182  while (indiec < funcIndEnd) {
183 
184  if (path[kk]->get_SgNode() == path[i]->get_SgNode()) {
185  indiec++;
186  if (indiec == funcIndEnd) {
187  break;
188  }
189  }
190  kk++;
191  }
192  }
193  int startingpoint = kk;
194 
195 
196  //std::vector<SgGraphNode*>::iterator it = path.begin();
197  //it += kk;
198  std::vector<SgGraphNode*> oldpath = path;
199  std::vector<SgGraphNode*> newpath;
200  // std::cout << "oldpath.size(): " << oldpath.size() << std::endl;
201  for (int qe = 0; qe < startingpoint; qe++) {
202  newpath.push_back(path[qe]);
203  }
204  for (size_t qe2 = 0; qe2 < funcPaths[0].size(); qe2++) {
205  newpath.push_back(funcPaths[0][qe2]);
206  }
207  for (size_t qe3 = startingpoint; qe3 < path.size(); qe3++) {
208  newpath.push_back(path[qe3]);
209  }
210  //path = newpath;
211  paths[pathnum] = newpath;
212  calledMap[newpath] = calledMap[path];
213  calledMap[newpath].insert(i);
214  //npaths.push_back(newpath);
215  //path.insert(it, funcPaths[0].begin(), funcPaths[0].end());
216  //std::cout << "newpath.size(): " << newpath.size() << std::endl;
217  //std::cout << "funcPaths.size(): " << funcPaths.size() << std::endl;
218  if (funcPaths.size() == 1) {
219  return;
220  }
221  for (size_t qw = 1; qw < funcPaths.size(); qw++) {
222  //if (qw != pathnum) {
223  std::vector<SgGraphNode*> npath;// = oldpath;
224  for (int qe = 0; qe < startingpoint; qe++) {
225  npath.push_back(path[qe]);
226  }
227  for (size_t qe2 = 0; qe2 < funcPaths[qw].size(); qe2++) {
228  npath.push_back(funcPaths[qw][qe2]);
229  }
230  for (size_t qe3 = startingpoint; qe3 < path.size(); qe3++) {
231  npath.push_back(path[qe3]);
232  }
233  calledMap[npath] = calledMap[newpath];
234 
235 
236 
237 
238  //npath.insert(it, funcPaths[qw].begin(), funcPaths[qw].end());
239  paths.push_back(npath);
240  }
241  //}
242  //std::cout << "paths.size(): " << paths.size() << std::endl;
243  std::vector<std::vector<SgGraphNode*> >::iterator tt = paths.begin();
244  //tt += pathnum;
245  // (*tt) = npaths[0];
246  // tt+=1;
247  // paths.insert((*tt),
248  //called.push_back(path[i+1]->get_SgNode());
249  }
250 
251 
252 
253 std::map<SgName, yices_expr> getExpr;
254 //string getGraphNodeType(SgGraphNode* sn);
255 
256 class visitorTraversal : public SgGraphTraversal<CFGforT>
257  {
258  public:
259  int tltnodes;
260  // int paths;
261  //std::map<SgName, yices_expr> getExpr;
262  std::set<SgNode*> knownNodes;
263  // std::vector<std::vector<SgGraphNode*> > pathstore;
264  void analyzePath(std::vector<VertexID>& pth);
265  SgIncidenceDirectedGraph* g;
266  myGraph* orig;
267  StaticCFG::CFG* cfg;
268  int pathnumber;
269  //std::map<SgVariableSymbol, string> nameOf;
270  //int nvars;
271  };
272 
273 class visitorTraversal2 : public SgGraphTraversal<newGraph>
274  {
275  public:
276  int tltnodes;
277  int paths;
278  void analyzePath(std::vector<VertexID>& pth);
279  //std::map<SgVariableSymbol, string> nameOf;
280  //int nvars;
281  };
282 
283 newGraph* nGraph;
284  SgIncidenceDirectedGraph* openg;
285  myGraph* openorig;
286  StaticCFG::CFG* opencfg;
287 
288 
289 
290 long getIndex(SgGraphNode* n) {
291  unsigned int i = n->get_index();
292  return i;
293 }
294 
295 
296 //yices_expr mainParse(vector<SgGraphNode*> expr, yices_context& ctx);
297 
298 int rounds;
299 int pathnum;
300 //std::set<SgGraphNode*> knownGraphNodes;
301 std::set<std::pair<VertexID2, VertexID2> > knownEdges;
302 std::map<SgGraphNode*, VertexID2> graphVertex;
303 
304 void visitorTraversal2::analyzePath(std::vector<VertexID2>& pathR) {
305  tltnodes += pathR.size();
306  paths++;
307  //std::cout << "path: " << paths << std::endl;
308 }
309 
310 
311 std::map<int, EdgeID2> intedgemap;
312 std::map<EdgeID2, int> edgeintmap;
313 std::map<VertexID2, int> intmap;
314 
315 int
316 getSource(int& edge, newGraph*& g)
317 {
318  EdgeID2 e = intedgemap[edge];
319  VertexID2 v = boost::source(e, *g);
320  return(intmap[v]);
321 }
322 
323 
324 
325 int getTarget(int& edge, newGraph*& g)
326 {
327  EdgeID2 e = intedgemap[edge];
328  VertexID2 v = boost::target(e, *g);
329  return (intmap[v]);
330 }
331 
332  void printCFGNode2(int& cf, VertexID2 v, newGraph*& g, std::ofstream& o)
333  {
334  stringstream str;
335  if ((*g)[v].expr) {
336  //std::cout << cf << "expr: " << (*g)[v].exprstr << std::endl;
337  str << cf << " expr: " << (*g)[v].exprstr;
338  }
339  else if ((*g)[v].vardec) {
340  //std::cout << cf << " vardec: " << (*g)[v].varstr << std::endl;
341  str << cf << " vardec: " << (*g)[v].varstr;
342  }
343  else {
344  str << cf;
345  }
346  std::string nodeColor = "black";
347  o << cf << " [label=\"" << " num:" << str.str() << "\", color=\"" << nodeColor << "\", style=\"" << "solid" << "\"];\n";
348  }
349 
350  void printCFGEdge2(int& cf, newGraph*& cfg, std::ofstream& o)
351  {
352  int src = getSource(cf, cfg);
353  int tar = getTarget(cf, cfg);
354  o << src << " -> " << tar << " [label=\"" << src << " " << tar << "\", style=\"" << "solid" << "\"];\n";
355  }
356 
357  void printHotness2(newGraph*& g)
358  {
359  //const newGraph* gc = g;
360  int currhot = 0;
361 
362  std::ofstream mf;
363  std::stringstream filenam;
364  filenam << "hotness2" << currhot << ".dot";
365  std::string fn = filenam.str();
366  mf.open(fn.c_str());
367 
368  mf << "digraph defaultName { \n";
369  vertex_iterator v, vend;
370  edge_iterator e, eend;
371  int intcurr = 1;
372  int intcurr2 = 1;
373  for (tie(v, vend) = vertices(*g); v != vend; ++v)
374  {
375  intmap[*v] = intcurr;
376  printCFGNode2(intcurr, *v, g, mf);
377  intcurr++;
378  }
379  for (tie(e, eend) = edges(*g); e != eend; ++e)
380  {
381  edgeintmap[*e] = intcurr2;
382  intedgemap[intcurr2] = *e;
383  printCFGEdge2(intcurr2, g, mf);
384  intcurr2++;
385  }
386  mf.close();
387  }
388 
389 
390 string getType(SgNode* n) {
391  if (isSgTypeInt(n)) {
392  return "int";
393  }
394  else if (isSgTypeDouble(n)) {
395  return "double";
396  }
397  else if (isSgTypeFloat(n)) {
398  return "float";
399  }
400  else if (isSgTypeShort(n)) {
401  return "short";
402  }
403  else if (isSgTypeLong(n)) {
404  return "long";
405  }
406  else if (isSgTypeLongLong(n)) {
407  return "long long int";
408  }
409  else if (isSgTypeLongDouble(n)) {
410  return "long double";
411  }
412  else if (isSgTypeBool(n)) {
413  return "bool";
414  }
415  return "";
416 }
417 
418 //string getSentence(SgGraphNode* n, std::vector<SgGraphNode*> nodesentence) {
419 
420 
421 yices_expr evalFunction(std::vector<SgGraphNode*> path, yices_context& ctx, bool mainFlag);
422 
423 std::vector<VertexID> exprs;
424 
425 int ipaths;
426 
427 
428 //std::vector<std::vector<SgGraphNode*> > paths;
429 
430 std::set<std::vector<SgGraphNode*> > globalPaths;
431 
432 //std::map<std::vector<SgGraphNode*>, std::set<SgNode*> > calledMap;
433 
434 void visitorTraversal::analyzePath(std::vector<VertexID>& pathR) {
435  //ROSE_ASSERT(globalPaths.find(pathR) == globalPaths.end());
436  //globalPaths.insert(pathR);
437  //yices_context ctx;
438  paths.clear();
439  usingNots=false;
440  //FuncPathMap.clear();
441  openg = g;
442  opencfg = cfg;
443  openorig = orig;
444  //unsigned int i = 0;
445  noAssert = false;
446  rounds = 0;
447  forFlag = false;
448  stringstream pathstream;
449  //std::set<SgNode*> knownNodes;
450  nameOf.clear();
451  getExpr.clear();
452  //VertexID2 start = boost::add_vertex(*nGraph);
453  //graphVertex[(*orig)[pathR[0]]] = start;
454  //std::cout << "path: " << pathnum << std::endl;
455  //for (int i = 0; i < pathR.size(); i++) {
456  // std::cout << vertintmap[pathR[i]] << ", ";
457  // }
458  //std::cout << std::endl;
459  pathnum++;
460  inconsistent = false;
461  std::vector<SgGraphNode*> path;
462  //std::vector<SgGraphNode*> pathR;
463  std::vector<SgGraphNode*> exprPath;
464  for (unsigned int j = 0; j < pathR.size(); j++) {
465  SgGraphNode* R = (*orig)[pathR[j]].sg;
466  path.push_back(R);
467  }
468  if (path.back()->get_SgNode() != path.front()->get_SgNode()) {
469  return;
470  }
471  //ROSE_ASSERT(globalPaths.find(path) == globalPaths.end());
472  //globalPaths.insert(path);
473  // std::cout << "path: " << std::endl;
474  // ofstream fout;
475  // string fileSaver = "pathsets";
476  // fout.open(fileSaver.c_str(),ios::app);
477  // for (int qr = 0; qr < path.size(); qr++) {
478  // fout << getGraphNodeType(path[qr]) << std::endl;
479  // }
480  // fout << "************************\n";
481  // fout.close();
482  //graphVertex[path[0]] = start;
483  //yices_context ctx = yices_mk_context();
484 bool noadd = false;
485 size_t jjf = 0;
486 paths.push_back(path);
487 std::vector<SgNode*> called;
488  while (jjf != paths.size()) {
489  //std::cout << "propagating" << std::endl;
490  std::vector<SgGraphNode*> pathc = paths[jjf];
491  size_t jj = 0;
492  while (jj != pathc.size()) {
493  if (isSgFunctionCallExp(pathc[jj]->get_SgNode()) && calledMap[pathc].find(jj) == calledMap[pathc].end() && opencfg->toCFGNode(pathc[jj]).getIndex() == 0) { //find(called.begin(), called.end(), pathc[jj]->get_SgNode()) == called.end()) {
494  SgFunctionDeclaration* sgfd = isSgFunctionCallExp(pathc[jj]->get_SgNode())->getAssociatedFunctionDeclaration();
495  SgName nam = sgfd->get_qualified_name();
496  // std::cout << "function: " << nam.getString() << std::endl;
497  ROSE_ASSERT(sgfd != NULL);
498  SgFunctionDefinition* sgfdef = sgfd->get_definition();
499  //ROSE_ASSERT(sgfdef != NULL);
500 
501  if (sgfdef != NULL) {
502  //std::cout << "index: " << opencfg->toCFGNode(pathc[jj]).getIndex() << std::endl;//pathc[jj]->get_index() << std::endl;
503  ROSE_ASSERT(opencfg->toCFGNode(pathc[jj]).getIndex() == 0);
504  //ROSE_ASSERT(pathc[jj]->get_index() == 0);
505  propagateFunctionCall(pathc, jj, jjf);
506 
507  //called.push_back(pathc[jj]->get_SgNode());
508  //jjf = 0;
509  noadd = true;
510  //jj = 0;
511  break;
512  }
513  else {
514  //std::cout << "ufunc: " << nam.getString() << std::endl;
515  unknownFunctions.insert(pathc[jj]->get_SgNode());
516  jj++;
517  }
518  }
519  else {
520  jj++;
521  }
522  }
523  if (noadd) {
524  jjf = 0;
525  noadd = false;
526  }
527 
528  else {
529  jjf++;
530  }
531  }
532 
533  //std::cout << "paths.size(): " << paths.size() << std::endl;
534  //ROSE_ASSERT(false);
535  pathnumber += paths.size();
536  std::vector<SgNode*> ncalled;
537 
538 for (size_t q = 0; q < paths.size(); q++) {
539  stringstream y;
540  y << "yices" << qst + q << ".txt";
541  ofstream fout;
542  string fileSaver = "pathsets";
543  fout.open(fileSaver.c_str(),ios::app);
544  for (size_t qr = 0; qr < paths[q].size(); qr++) {
545  fout << getGraphNodeType(paths[q][qr]) << std::endl;
546  }
547  fout << "************************\n";
548  fout.close();
549 
550  yices_enable_log_file((char*) y.str().c_str());
551 
552  nameOf.clear();
553  getExpr.clear();
554  //std::cout << "q=" << q << std::endl;
555  //std::cout << "path: " << std::endl;
556  //for (int q1 = 0; q1 < paths[q].size(); q1++) {
557  // std::cout << getGraphNodeType(paths[q][q1]);
558  //}
559  //std::cout << "endpath" << std::endl;
560  // std::cout << "evalFunction" << std::endl;
561  std::vector<SgGraphNode*> path = paths[q];
562  //yices_reset(ctx);
563  //for (int j = 0; j < 4; j++) {
564  ROSE_ASSERT(path.front()->get_SgNode() == path.back()->get_SgNode());
565  yices_context ctx = yices_mk_context();
566  //yices_expr ye = evalFunction(path, ctx, true);
567  //for (int j = 0; j < 4; j++) {
568  // yices_model ym = yices_get_model(ctx);
569  //yices_dump_context(ctx);
570  switch(yices_check(ctx)) {
571  case l_true:
572  {
573  if (unknownvdeclis.size() != 0) {
574  //printf("satisfiable\n");
575  yices_model m = yices_get_model(ctx);
576  //printf("e1 = %d\n", yices_get_value(m, yices_get_var_decl(e1)));
577  //printf("e2 = %d\n", yices_get_value(m, yices_get_var_decl(e2)));
578  //yices_display_model(m);
579  usingNots = true;
580  //if (unknownvdeclis.size() != 0) {
581  for (int yy = 0; yy < 4; yy++) {
582  std::cout << "unknownvdeclis.size(): " << unknownvdeclis.size() << std::endl;
583  for (size_t yy2 = 0; yy2 < unknownvdeclis.size(); yy2++) {
584  yices_var_decl vdecli = new yices_var_decl();
585  vdecli = unknownvdeclis[yy2];
586  SgInitializedName* sg = new SgInitializedName();
587  sg = IName[vdecli];
588  ROSE_ASSERT(sg != NULL);
589  ROSE_ASSERT(IName.find(vdecli) != IName.end());
590  long* val = new long;
591  yices_get_int_value(m,vdecli,val);
592  SgName sn = sg->get_qualified_name();
593 
594  std::cout << "unknown " << sn.getString() << " is: " << *val << std::endl;
595  notMap[sg].push_back(int(*val));
596  }
597  yices_reset(ctx);
598  //yices_del_context(ctx);
599  // ctx = yices_mk_context();
600  nameOf.clear();
601  getExpr.clear();
602  unknowns.clear();
603  unknownvdeclis.clear();
604  IName.clear();
605 
606  inconsistent = false;
607  evalFunction(path, ctx, true);
608 
609  if (yices_inconsistent(ctx)) {
610  std::cout << "********************" << std::endl;
611  std::cout << "inconsistent at yy: " << yy << std::endl;
612  std::cout << "********************" << std::endl;
613  break;
614  }
615  else {
616  // yices_dump_context(ctx);
617  yices_check(ctx);
618  //yices_model m = yices_get_model(ctx);
619  std::cout << "*****************" << std::endl;
620  std::cout << "consistent at yy: " << yy << std::endl;
621  std::cout << "*****************" << std::endl;
622  // yices_display_model(m);
623  }
624  }
625  //unknownvdeclis.clear();
626  usingNots = false;
627  // break;
628  }
629  break;
630  }
631  case l_false:
632  // printf("unsatisfiable\n");
633  break;
634  case l_undef:
635  printf("unknown\n");
636  break;
637  }
638 
639  usingNots = false;
640  yices_reset(ctx);
641  notMap.clear();
642  nameOf.clear();
643  getExpr.clear();
644  unknowns.clear();
645  unknownvdeclis.clear();
646 }
647 //}
648 qst += paths.size();
649 }
650 
651 //bool inconsistent;
652 
653 yices_expr evalFunction(std::vector<SgGraphNode*> path, yices_context& ctx, bool mainFlag) {
654  int i = 0;
655  //bool noAssert = false;
656  //int rounds = 0;
657  //bool forFlag = false;
658  //int defscount = 0;
659  //bool inconsistent = false;
660  std::vector<SgGraphNode*> exprPath;
661 /*
662  if (!mainFlag && isSgFunctionCallExp(path.front()->get_SgNode())) {
663  path.pop_back();
664  int qq = 0;
665  while (defscount < 2) {
666  while (path[qq]->get_SgNode() != path[0]->get_SgNode()) {
667  qq++;
668  }
669  defscount++;
670  }
671  std::vector<SgGraphNode*> npath;
672  for (int qw = qq; qw < path.size(); qw++) {
673  npath.push_back(path[qw]);
674  }
675  path = npath;
676 
677  }
678 */
679 /*
680  if (unknownFunctions.find(isSgFunctionCallExp(path[0]->get_SgNode())) != unknownFunctions.end()) {
681  SgFunctionDeclaration* afd = (isSgFunctionCallExp(path[0]->get_SgNode()))->getAssociatedFunctionDeclaration();
682  SgType* ty = afd.get_orig_return_type();
683  string ty_str = getType(ty);
684  SgInitializedNamePtrList* sipl = afd->get_args();
685  yices_type dom[sipl->size()]
686  int iic = 0;;
687  for (SgInitializedNamePtrList::iterator ii = sipl.begin(); ii != sipl.end(); ii++) {
688  dom[iic] = (*ii)->get_type();
689 
690  iic++;
691  }
692  int ds = iic;
693  yices_type fty = yices_mk_function_type(ctx, dom, ds, ty);
694  yices_var_decl ftydecl = (ctx, afd->get_qualified_name()->getString(),fty);
695  yices_expr f = yices_mk_var_from_decl(ctx, ftydecl);
696 
697 
698 
699 
700  }
701 */
702  while (i < (int)path.size()) {
703  // std::cout << "in evalFunction" << std::endl;
704  // std::cout << "ith node: " << getGraphNodeType(path[i]) << "at i = " << i << std::endl;
705  // std::cout << "path.size(): " << path.size() << std::endl;
706 /*
707  if (inconsistent) {
708  if (!mainFlag) {
709  yices_expr wrong;
710  return wrong;
711  }
712  else {
713  inconsistent = false;
714  yices_expr zrong;
715  return zrong;
716  }
717  }*/
718  if (yices_inconsistent(ctx)/* || inconsistent*/) {
719  inconsistent = true;
720  // std::cout << "inconsistent" << std::endl;
721  if (mainFlag) {
722  // std::cout << "*****************************************" << std::endl;
723  // std::cout << "inconsistent path: " << std::endl;
724  //for (int q4 = 0; q4 < path.size(); q4++) {
725  // std::cout << getGraphNodeType(path[q4]);
726  //}
727  //std::cout << "end path" << std::endl;
728  //std::cout << "******************************************" << std::endl;
729  if (!usingNots) {
730  ipaths++;
731  }
732  inconsistent = false;
733  }
734  yices_expr ywrong = yices_mk_fresh_bool_var(ctx);
735  return ywrong;
736  }
737  //std::cout << "i: " << i << std::endl;
738  exprPath.clear();
739  //VertexID2 v1;
740  //VertexID2 v2;
741  //std::cout << "in while" << std::endl;
742  if (isSgReturnStmt(path[i]->get_SgNode())) {
743  // std::cout << "retstmt" << std::endl;
744  // std::cout << "i: " << i << ", path.size(): " << path.size() << std::endl;
745  std::vector<SgGraphNode*> retpath;
746  //retpath.push_back(path[i]);
747 
748  int j = i+1;
749  while (path[j]->get_SgNode() != path[i]->get_SgNode()) {
750  retpath.push_back(path[j]);
751  // std::cout << "path[j]: " << getGraphNodeType(path[j]) << std::endl;
752  j++;
753  if (j == (int)path.size()) {
754  break;
755  }
756  }
757  //retpath.push_back(path[j]);
758  yices_expr retparse = mainParse(retpath, ctx);
759  if (!mainFlag) {
760  return retparse;
761  //yices_assert(retparse, ctx);
762  }
763  i += retpath.size()+2;
764  }
765 
766  if (isSgInitializedName(path[i]->get_SgNode()) /*&& knownNodes.find(path[i]->get_SgNode()) == knownNodes.end()*/) {
767  // exprs.push_back(path[i]);
768  exprPath.clear();
769  exprPath.push_back(path[i]);
770  if (path[i]->get_SgNode()->cfgIndexForEnd() == 0) {
771 
772  SgName svs = (isSgInitializedName(exprPath[0]->get_SgNode()))->get_qualified_name();
773  if (nameOf.find(svs) == nameOf.end()) {
774  SgType* typ = (isSgInitializedName(exprPath[0]->get_SgNode()))->get_type();
775  string typ_str = getType(typ);
776  stringstream funN;
777  //funN << "V" << nvars;
778  nvars++;
779  funN << svs.getString() << nvars;
780  char* fun = (char*) funN.str().c_str();
781  char* valTypeCh = (char*) typ_str.c_str();
782  yices_type ty = yices_mk_type(ctx, valTypeCh);
783  yices_var_decl vdecl = yices_mk_var_decl(ctx, fun, ty);
784  yices_expr e1 = yices_mk_var_from_decl(ctx, vdecl);
785  getExpr[svs] = e1;
786  nameOf[svs] = funN.str();
787  }
788  i++;
789  }
790  else {
791  unsigned int k = i+1;
792  //while (k < path.size() && (!isSgInitializedName(path[k]->get_SgNode()) || path[k]->get_SgNode() != path[i]->get_SgNode())) {
793  // exprPath.push_back(path[k]);
794  // k++;
795  // }
796  // exprPath.push_back(path[i]);
797  size_t check = 0;
798  while (check < path[i]->get_SgNode()->cfgIndexForEnd()) {//path[k]->get_SgNode() != path[i]->get_SgNode()) {
799  if (path[i]->get_SgNode() == path[k]->get_SgNode()) {
800  check++;
801  if (check == path[i]->get_SgNode()->cfgIndexForEnd()) {
802  break;
803  }
804  }
805  exprPath.push_back(path[k]);
806  k++;
807  }
808  exprPath.push_back(path[k]);
809  //std::cout << "EXPRPATH: " << std::endl;
810  //for (int oo = 0; oo < exprPath.size(); oo++) {
811  // std::cout << getGraphNodeType(exprPath[oo]) << std::endl;
812  // }
813  // std::cout << std::endl;
814  // SE_ASSERT(y1 != NULL);
815  yices_expr y1;
816  //std::cout << "exprPath.size(): " << exprPath.size() << std::endl;
817  // if (isSgIfStmt(exprPath[0]->get_SgNode()) || isSgForStatement(exprPath[0]->get_SgNode())) {
818  // y1 = evalFunction(exprPath,ctx,false);
819  // }
820  // else {
821  y1 = mainParse(exprPath, ctx);
822  // }
823  ROSE_ASSERT(y1 != NULL);
824  if (!unknown_flag && unknowns.find(isSgInitializedName(path[i]->get_SgNode())) == unknowns.end()) {//find(unknowns.begin(), unknowns.end(), path[i]->get_SgNode()) == unknowns.end()) {
825  //if (y1 != NULL) {
826 
827  yices_assert(ctx, y1);
828  //}
829  }
830  else {
831  // if (find(unknowns.begin(), unknowns.end(), path[i]->get_SgNode()) == unknowns.end()) {
832  // unknowns.push_back(path[i]->get_SgNode());
833  // }
834  unknown_flag = false;
835  }
836  i += exprPath.size()+1;
837  exprPath.clear();
838  k = 0;
839  }
840  }
841  else if (isSgWhileStmt(path[i]->get_SgNode()) && opencfg->toCFGNode(path[i]).getIndex() == 0) {
842  std::vector<SgGraphNode*> internals;
843  std::vector<SgGraphNode*> exitStmt;
844  int iorig = i;
845  i = i + 2;
846  // std::cout << "path[i+1]: " << getGraphNodeType(path[iorig+1]) << ", " << "path[i+2]: " << getGraphNodeType(path[iorig+2]) << std::endl;
847  // std::cout << "exitStmt" << std::endl;
848  // std::cout << "internals" << std::endl;
849  while (i < (int)path.size() && path[i]->get_SgNode() != path[iorig]->get_SgNode()) {
850  if (isSgBasicBlock(path[i]->get_SgNode())) {
851  i++;
852  }
853  else {
854  exitStmt.push_back(path[i]);
855 
856  // std::cout << getGraphNodeType(path[i]) << std::endl;
857  i++;
858  }
859  }
860  exitStmt.pop_back();
861  i++;
862  //std::cout << "end exitStmt" << std::endl;//end internals" << std::endl;
863  // std::cout << "exitStmt" << std::endl;
864  // std::cout << "internals" << std::endl;
865  while (i < (int)path.size() && path[iorig]->get_SgNode() != path[i]->get_SgNode()) {
867  // if (!isSgBasicBlock(path[i]->get_SgNode())) {
868  internals.push_back(path[i]);
869  // }
870  // std::cout << getGraphNodeType(path[i]) << std::endl;
871  i++;
872  }
873  //std::cout << "end internals" << std::endl;
874  // std::cout << "end exit stmt" << std::endl;
875  if (internals.size() == 0) {
876  yices_expr wh = mainParse(exitStmt, ctx);
877  yices_expr nwhile = yices_mk_not(ctx,wh);
878  yices_assert(ctx,nwhile);
879  i++;
880  }
881 
882  else {
883  iorig = i;
884  i++;
885  while (path[i]->get_SgNode() != path[iorig]->get_SgNode()) {
886  i++;
887  }
888  bool good = false;
889  int n = 0;
890  while (n < FORLOOPS) {
891  // std::cout << "n = " << n << std::endl;
892  yices_push(ctx);
893  yices_expr exityi = mainParse(exitStmt, ctx);
894  yices_assert(ctx, exityi);
895  if (yices_inconsistent(ctx)) {
896  yices_pop(ctx);
897  if (!yices_inconsistent(ctx)) {
898  good = true;
899  break;
900  }
901  else {
902  good = false;
903  break;
904  }
905  }
906  else {
907  yices_pop(ctx);
908  //yices_expr ev = evalFunction(internals, ctx, false);
909  //yices_expr eupdate = mainParse(update, ctx);
910  //yices_assert(ctx, eupdate);
911  //yices_expr ev = evalFunction(internals, ctx, false);
912  //yices_assert(ctx,ev);
913  n++;
914  }
915  //else {
916  // yices_pop(ctx);
917  // good = true;
918  // break;
919  // }
920  }
921  if (good) {
922  yices_expr mP = mainParse(exitStmt, ctx);
923  yices_expr nmP = yices_mk_not(ctx, mP);
924  yices_assert(ctx, nmP);
925  // std::cout << "while, good in: " << n << " loops" << std::endl;
926  }
927  else {
928  yices_expr yf = yices_mk_false(ctx);
929  yices_assert(ctx,yf);
930  }
931  //while (i < path.size() && !isSgWhileStmt(path[i]->get_SgNode())) {
932  // i++;
933  // }
934  //std::cout << "i+2" << getGraphNodeType(path[i+2]) << std::endl;
935  i++;
936  while (isSgBasicBlock(path[i]->get_SgNode())) {
937  i++;
938  }
939 
940  }
941  }
942 
943 
944  else if (isSgForStatement(path[i]->get_SgNode()) && opencfg->toCFGNode(path[i]).getIndex() == 0) {
945  std::vector<SgGraphNode*> internals;
946  std::vector<SgGraphNode*> initStmt;
947  std::vector<SgGraphNode*> exitStmt;
948  std::vector<SgGraphNode*> update;
949  //std::cout << "ForStmt" << std::endl;
950  ROSE_ASSERT(isSgForInitStatement(path[i+1]->get_SgNode()));
951  int k = i+3;
952  // std::cout << "i: " << getGraphNodeType(path[i]) << std::endl;
953  // std::cout << "k: " << getGraphNodeType(path[k]) << std::endl;
954  //std::cout << "path[i+3]: " << getGraphNodeType(path[i+3]) << ", path[i+2]: " << getGraphNodeType(path[i+2]) << std::endl;
955  //std::cout << "initStmt: " << std::endl;
956  while (path[i+1]->get_SgNode() != path[k]->get_SgNode()) {
957  initStmt.push_back(path[k]);
958  // std::cout << getGraphNodeType(path[k]) << std::endl;
959  k++;
960  }
961  initStmt.pop_back();
962  //std::cout << std::endl;
963  k++;
964  //forFlag = true;
965  yices_expr yk = mainParse(initStmt, ctx);
966  //forFlag = true;
967  // forFlag = false;
968  yices_assert(ctx, yk);
969  ROSE_ASSERT(isSgForStatement(path[k]->get_SgNode()));
970  int j = k+2;
971  while (path[j]->get_SgNode() != path[k]->get_SgNode()) {
972  exitStmt.push_back(path[j]);
973  j++;
974  }
975  j++;
976  // std::cout << "exitStmt.front(): " << getGraphNodeType(exitStmt.front()) << std::endl;
977  // std::cout << "exitStmt.back(): " << getGraphNodeType(exitStmt.back()) << std::endl;
978  exitStmt.pop_back();
979  //ROSE_ASSERT(exitStmt.size() != 0);
980  //std::cout << "**********************" << std::endl;
981  //std::cout << "exitStmt" << std::endl;
982  //for (int j2 = 0; j2 < exitStmt.size(); j2++) {
983  // std::cout << getGraphNodeType(exitStmt[j2]) << std::endl;
984  // }
985  // std::cout << "end exitStmt" << std::endl;
986  // std::cout << "***********************" << std::endl;
987  //j = j+1;
988  while (isSgBasicBlock(path[j]->get_SgNode())) {
989  j++;
990  }
991  //std::cout << "j type: " << getGraphNodeType(path[j]) << std::endl;
992  if (isSgForStatement(path[j]->get_SgNode()) && opencfg->toCFGNode(path[j]).getIndex() == 4) {// == path[i]->get_SgNode()) {
993  // forFlag = true;
994  //std::cout << "path btwn i and j: " << std::endl;
995  //for (int k = i; k < j+1; k++) {
996  // std::cout << getGraphNodeType(path[k]) << std::endl;
997  //}
998  //std::cout << "endpath" << std::endl;
999  yices_expr exity = mainParse(exitStmt, ctx);
1000  // forFlag = true;
1001  // yices_assert(ctx, exity);
1002  yices_expr notexp = yices_mk_not(ctx, exity);
1003  yices_assert(ctx, notexp);
1004  i++;
1005  //i = j+1;
1006 
1007  }
1008  else {
1009  while (path[j]->get_SgNode() != path[i]->get_SgNode() && j < (int)path.size()-1) {
1010  // std::cout << "currj: " << getGraphNodeType(path[j]) << std::endl;
1011  // if (!isSgBasicBlock(path[j]->get_SgNode())) {
1012  internals.push_back(path[j]);
1013  // }
1014  j++;
1015  }
1016  //std::cout << "currj: " << j << ", path.size(): " << path.size() << ", node type: " << getGraphNodeType(path[j]) << std::endl;
1017  j++;
1018  // std::cout << "XXXXXXXXXXXXXXXX" << std::endl;
1019  // std::cout << "internals.size(): " << internals.size() << std::endl;
1020  // for (int qr = 0; qr < internals.size(); qr++) {
1021  // std::cout << getGraphNodeType(internals[qr]) << std::endl;
1022  // }
1023  // std::cout << "internals done" << std::endl;
1024  // std::cout << "XXXXXXXXXXXXXX" << std::endl;
1025  // forFlag = true;
1026  // yices_expr ev = evalFunction(internals, ctx, false);
1027  //yices_assert(ctx,ev);
1028  // forFlag = true;
1029  //if (ev == NULL) {
1030  while (path[j]->get_SgNode() != path[i]->get_SgNode()) {
1031  update.push_back(path[j]);
1032  j++;
1033  }
1034  // yices_expr updatey = mainParse(update, ctx);
1035  // j++;
1036 
1037  ROSE_ASSERT(path[j]->get_SgNode() == path[i]->get_SgNode());
1038  j++;
1039  while(path[j]->get_SgNode() != path[i]->get_SgNode()) {
1040  j++;
1041  }
1042  i = j+1;
1043  // forFlag = true;
1044 
1045  // yices_expr exity2 = mainParse(exitStmt, ctx);
1046  // forFlag = true;
1047  int n = 0;
1048  //yices_push(ctx);
1049  bool good = false;
1050  while (n < FORLOOPS) {
1051  //std::cout << "n = " << n << std::endl;
1052  yices_push(ctx);
1053  yices_expr exityi = mainParse(exitStmt, ctx);
1054  yices_assert(ctx, exityi);
1055  if (yices_inconsistent(ctx)) {
1056  yices_pop(ctx);
1057  if (!yices_inconsistent(ctx)) {
1058  good = true;
1059  break;
1060  }
1061  else {
1062  good = false;
1063  break;
1064  }
1065  }
1066  else {
1067  yices_pop(ctx);
1068  evalFunction(internals, ctx, false);
1069  yices_expr eupdate = mainParse(update, ctx);
1070  yices_assert(ctx, eupdate);
1071  //yices_expr ev = evalFunction(internals, ctx, false);
1072  //yices_assert(ctx,ev);
1073  n++;
1074  }
1075  //else {
1076  // yices_pop(ctx);
1077  // good = true;
1078  // break;
1079  // }
1080  }
1081  if (good) {
1082  //std::cout << "for, good in: " << n << " loops" << std::endl;
1083  yices_expr ey = mainParse(exitStmt, ctx);
1084  yices_expr eyn = yices_mk_not(ctx,ey);
1085  yices_assert(ctx,eyn);
1086  }
1087  else {
1088  //std::cout << "bad loop" << std::endl;
1089  yices_expr yf = yices_mk_false(ctx);
1090  yices_assert(ctx,yf);
1091  }
1092  //yices_assert(ctx, exity2);
1093  // }
1094  //}
1095  // {
1096  //ROSE_ASSERT(false);
1097  // forFlag = false;
1098  // return ev;
1099  // }
1100  }
1101  //i++;
1102  if (isSgForInitStatement(path[i]->get_SgNode())) {
1103  i--;
1104  }
1105  // std::cout << "i: " << getGraphNodeType(path[i]) << std::endl;
1106  forFlag = false;
1107  }
1108 
1109  // yices_expr yexit = mainParse(exitStmt);
1110  //yices_assert(yexit);
1111 
1112 
1113 
1114 
1115 
1116 /*
1117  else if (isSgForStatement(path[i]->get_SgNode()) && isSgForInitStatement(path[i+1]->get_SgNode())) {
1118  forFlag = true;
1119  std::vector<SgGraphNode*> vec1;
1120  unsigned int j = i+2;
1121  int w = 2;
1122  while (!isSgInitializedName(path[j]->get_SgNode()) && !isSgAssignOp(path[j]->get_SgNode())) {
1123  j++;
1124  w++;
1125  }
1126  vec1.push_back(path[j]);
1127  int k = j+1;
1128  while (k < path.size() && !isSgInitializedName(path[k]->get_SgNode())) {
1129  vec1.push_back(path[k]);
1130  k++;
1131  }
1132  vec1.push_back(path[k]);
1133  int q = 0;
1134  while (k < path.size() && !isSgForInitStatement(path[k]->get_SgNode())) {
1135  q++;
1136  k++;
1137  }
1138  yices_expr y1 = mainParse(vec1, ctx);
1139  yices_assert(ctx, y1);
1140  forFlag = false;
1141  i += vec1.size() + w + q;
1142  }
1143 */
1144  else if (isSgIfStmt(path[i]->get_SgNode()) && opencfg->toCFGNode(path[i]).getIndex() == 0) {
1145  //std::cout << "ifstmt" << std::endl;
1146  //for (int wq = i; wq < path.size(); wq++) {
1147  //std::cout << getGraphNodeType(path[wq]) << std::endl;
1148  // }
1149  // std::cout << "endifstmt" << std::endl;
1150  // std::cout << "next node: " << getGraphNodeType(path[i+1]) << std::endl;
1151  while (isSgBasicBlock(path[i+1]->get_SgNode())) {
1152  i++;
1153  }
1154  if (!isSgExprStatement(path[i+1]->get_SgNode())) {
1155  i++;
1156  }
1157  else {
1158  ROSE_ASSERT(isSgExprStatement(path[i+1]->get_SgNode()));
1159  int k = i+2;
1160  std::vector<SgGraphNode*> fpath;
1161  while (path[k]->get_SgNode() != path[i+1]->get_SgNode()) {
1162  if (!isSgBasicBlock(path[k]->get_SgNode())) {
1163  fpath.push_back(path[k]);
1164  }
1165  k++;
1166  }
1167  //fpath.push_back(path[k]);
1168  ROSE_ASSERT(isSgExprStatement(path[k]->get_SgNode()));;
1169  //std::cout << "fpath: " << std::endl;
1170  // for (int xx = 0; xx < fpath.size(); xx++) {
1171  // std::cout << getGraphNodeType(fpath[xx]) << std::endl;
1172  //}
1173  //std::cout << "endfpath" << std::endl;
1174  yices_expr y1 = mainParse(fpath, ctx);
1175  int kk = k+1;
1176  ROSE_ASSERT(isSgIfStmt(path[kk]->get_SgNode()));
1177  std::set<SgDirectedGraphEdge*> ifoeds = openg->computeEdgeSetOut(path[kk]);
1178  CFGNode cn = opencfg->toCFGNode(path[kk+1]);
1179  std::vector<CFGEdge> ed = cn.inEdges();
1180 
1181  //int qw = 0;
1182  EdgeConditionKind kn;
1183  CFGEdge needEdge;
1184  for (size_t qt = 0; qt < ed.size(); qt++) {
1185  if (ed[qt].source() == opencfg->toCFGNode(path[kk])) {
1186  needEdge = ed[qt];
1187  kn = needEdge.condition();
1188  }
1189  }
1190  while (isSgBasicBlock(path[kk+1]->get_SgNode())) {
1191  kk++;
1192  }
1193  //std::cout << "currnode: " << getGraphNodeType(path[kk+1]) << std::endl;
1194  // for (int q2 = 0; q2 < path.size(); q2++) {
1195  // iqw = 0;
1196  // while (ed[qw].source() != opencfg->toCFGNode(path[q2])) {
1197  // qw++;
1198  // if (qw >= ed.size()) {
1199  // break;
1200  // }
1201  // }
1202  // qw = 0;
1203  //}
1204  //CFGEdge needEdge = ed[qw];
1205  if (unknown_flag) {
1206  unknown_flag = false;
1207  yices_expr uf;
1208  return uf;
1209  }
1210  //std::cout << "condition" << std::endl;
1211  //std::cout << getGraphNodeType(path[kk+1]) << std::endl;
1212  //std::cout << "end condition" << std::endl;
1213  //EdgeConditionKind kn = needEdge.condition();
1214  if (kn == eckTrue) {
1215  yices_assert(ctx, y1);
1216  }
1217  else {
1218  ROSE_ASSERT(kn == eckFalse);
1219  yices_expr ynot = yices_mk_not(ctx,y1);
1220  yices_assert(ctx,ynot);
1221  }
1222  int kk2 = kk+1;
1223  //while (isSgBasicBlock(path[kk2]->get_SgNode())) {
1224  // kk2++;
1225  // }
1226 
1227  //int kk2 = kk+1;
1228  //std::cout << "kk: " << getGraphNodeType(path[kk]) << std::endl;
1229  //std::cout << "kk2: " << getGraphNodeType(path[kk2]) << std::endl;
1230  //std::cout << "path.back(): " << getGraphNodeType(path.back()) << std::endl;
1231  std::vector<SgGraphNode*> fpath2;
1232  fpath2.push_back(path[kk2]);
1233  kk2++;
1234  while (path[kk2]->get_SgNode() != path[kk+1]->get_SgNode() || opencfg->toCFGNode(path[kk2]).getIndex() != path[kk+1]->get_SgNode()->cfgIndexForEnd()) {//&& yicesParser_LDFLAGS = -fopenmp -O3 -L/home/hoffman34/yices/yices-1.0.292/lib -lyices
1235  // while (path[kk2]->get_SgNode() != path[kk]->get_SgNode() && kk2 < path.size()) {
1236  // if (!isSgBasicBlock(path[kk2]->get_SgNode())) {
1237  fpath2.push_back(path[kk2]);
1238  // }
1239  kk2++;
1240  if (kk2 == (int)path.size()) {
1241  break;
1242  }
1243 
1244  }
1245  // std::cout << "kk2: " << getGraphNodeType(path[kk2]) << std::endl;
1246  if (kk2 < (int)path.size()) {
1247  fpath2.push_back(path[kk2]);
1248  }
1249  if (kk2 == (int)path.size()) {
1250  //std::cout << "kk2 path: " << std::endl;
1251  // for (int u = kk+1; u < kk2; u++) {
1252  // std::cout << getGraphNodeType(path[u]) << std::endl;
1253  // }
1254  // std::cout << "kk2 end: " << std::endl;
1255  i = kk2;
1256  yices_expr ewe = evalFunction(fpath2,ctx,false);
1257  return ewe;
1258  // return;
1259  }
1260  else {
1261  int kk3 = kk2+1;
1262 
1263  // while (path[kk3]->get_SgNode() != path[kk2]->get_SgNode()) {
1264  // kk3++;
1265  // }
1266  if (fpath2.size() != 0) {
1267  evalFunction(fpath2,ctx,false);
1268 
1269  //std::cout << "fpath2" << std::endl;
1270  // std::cout << std::endl;
1271  // for (int qp = 0; qp < fpath2.size(); qp++) {
1272  // std::cout << getGraphNodeType(fpath2[qp]) << std::endl;
1273  // }
1274  //std::cout << "fpath2end" << std::endl;
1275  // if (isSgExprStatement(fpath2[0]->get_SgNode())) {
1276  // std::vector<SgGraphNode*> fpathnew;
1277  // ROSE_ASSERT(isSgExprStatement(fpath2.back()->get_SgNode()));
1278  // for (int qq = 1; qq < fpath2.size()-1; qq++) {
1279  // fpathnew.push_back(fpath2[qq]);
1280  // }
1281  // fpath2 = fpathnew;
1282  // }
1283  //if (fpath2.size() != 0) {
1284  // SgGraphNode* pathj = fpath2.front();
1285  // if (isSgWhileStmt(pathj->get_SgNode()) || isSgIfStmt(pathj->get_SgNode()) || isSgForStatement(pathj->get_SgNode()) || isSgInitializedName(pathj->get_SgNode()) /*|| isSgReturnStmt(pathj->get_SgNode())*/) {
1286  // yices_expr y3 = evalFunction(fpath2, ctx, false);
1287  // }
1288  // else if (isSgReturnStmt(pathj->get_SgNode())) {
1289  // std::vector<SgGraphNode*> ffpath;
1290  // for (int ff = 1; ff < fpath2.size()-1; ff++) {
1291  // ffpath.push_back(fpath2[ff]);
1292  // }
1293  // yices_expr y3 = mainParse(ffpath, ctx);
1294  // yices_expr y3 = evalFunction(fpath2, ctx, false);
1295  // return y3;
1296  // }
1297  // else {
1298  //std::cout << "fpath2: " << std::endl;
1299  //for (int wq = 0; wq < fpath2.size(); wq++) {
1300  // std::cout << getGraphNodeType(fpath2[wq]) << std::endl;
1302  // std::cout << "\n\n" << std::endl;
1303  // yices_expr y3 = mainParse(fpath2, ctx);
1304  // yices_assert(ctx, y3);
1305  }
1306 
1307  //else {
1308  // ROSE_ASSERT(false);
1309  // }
1310 
1311  i = kk3;
1312  }
1313  }
1314  }
1315 
1316  else if (isSgExprStatement(path[i]->get_SgNode()) && opencfg->toCFGNode(path[i]).getIndex() == 0 /*&& knownNodes.find(path[i]->get_SgNode()) == knownNodes.end()*/) {
1317  int j = i+1;
1318  std::vector<SgGraphNode*> ses;
1319  ses.push_back(path[i]);
1320  while (path[i]->get_SgNode() != path[j]->get_SgNode()) {
1321  // std::cout << "ses[j]: " << getGraphNodeType(path[j]) << std::endl;
1322  ses.push_back(path[j]);
1323  j++;
1324  }
1325  //std::cout << "ses end" << std::endl;
1326  ses.push_back(path[j]);
1327  yices_expr mP = mainParse(ses, ctx);
1328  yices_assert(ctx, mP);
1329  i = j+1;
1330  // std::vector<SgGraphNode*> eStmt;
1331  // eStmt.push_back(path[i]);
1332  // while (path[j]->get_SgNode() != path[i]->get_SgNode()) {
1333  // eStmt.push_back(path[j]);
1334  // j++;
1335  // }
1336  // eStmt.push_back(path[j]);
1337  // yices_expr ee = mainParse(eStmt, ctx);
1338  // yices_assert(ctx,ee);
1339  //yices_expr ymain = mainParse(eStmt, ctx);
1340  //yices_assert(ctx, ymain);
1341  // i = j+1;
1342  }
1343 /*
1344  unsigned int j = i+1;
1345  while (path[j]->get_SgNode() != path[i]->get_SgNode()) {
1346  exprPath.push_back(path[j]);
1347  j++;
1348  }
1349  if (isSgIfStmt(path[j]->get_SgNode()) || isSgForStatement(path[j]->get_SgNode()) || isSgInitializedName(path[j]->get_SgNode()) || isSgReturnStmt(path[j]->get_SgNode())) {
1350  i = j;
1351  }
1352  else {
1353  // std::cout << "Exprpath: " << std::endl;
1354  // for (int qq = 0; qq < exprPath.size(); qq++) {
1355  // std::cout << getGraphNodeType(exprPath[qq]) << std::endl;
1356  // }
1357  //std::cout << std::endl;
1358  // if (!unknown_flag) {
1359  yices_expr y1 = mainParse(exprPath, ctx);
1360  if (!unknown_flag) {
1361  yices_assert(ctx,y1);
1362  }
1363  else {
1364  unknown_flag = false;
1365  }
1366  i += exprPath.size()+2;
1367  }
1368  }
1369 */
1370 
1371 /*
1372  ROSE_ASSERT(j < path.size());
1373  yices_expr y2 = mainParse(exprPath, ctx);
1374  ROSE_ASSERT(y2 != NULL);
1375  //std::cout << "exprPath.size(): " << exprPath.size() << std::endl;
1376  std::set<SgDirectedGraphEdge*> oeds = openg->computeEdgeSetOut(path[j]);
1377  ROSE_ASSERT(oeds.size() == 1);
1378  SgGraphNode* onn = (*(oeds.begin()))->get_to();
1379 
1380 
1381  ROSE_ASSERT(onn == path[j+1]);
1382  std::set<SgDirectedGraphEdge*> ifoeds = openg->computeEdgeSetOut(path[j+1]);
1383  if ((isSgForStatement(onn->get_SgNode()) || (isSgIfStmt(onn->get_SgNode())) && ifoeds.size() >= 2)) {
1384  //std::cout << "got a for or if" << std::endl;
1385 
1386  CFGNode cn = opencfg->toCFGNode(path[j+2]);
1387  std::vector<CFGEdge> ed = cn.inEdges();
1388  //ROSE_ASSERT(ed.size() == 1);
1389  int qw = 0;
1390  while (ed[qw].source() != opencfg->toCFGNode(path[j+1])) {
1391  qw++;
1392  }
1393  CFGEdge needEdge = ed[qw];
1394  EdgeConditionKind kn = needEdge.condition();
1395  ROSE_ASSERT(kn == eckTrue || kn == eckFalse);
1396  if (kn == eckFalse) {
1397  yices_expr y2n = yices_mk_not(ctx, y2);
1398 
1399  yices_assert(ctx, y2n);
1400  }
1401  else {
1402  ROSE_ASSERT(kn == eckTrue);
1403  //std::cout << "got a eckTrue" << std::endl;
1404  if (isSgForStatement(onn->get_SgNode())) {
1405  // int yr = yices_assert_retractable(ctx, y2);
1406  // forsts[onn->get_SgNode()] = yr;
1407  }
1408  else {
1409  yices_assert(ctx, y2);
1410  }
1411  }
1412  }
1413  else {
1414  yices_assert(ctx, y2);
1415  }
1416  i += exprPath.size()+2;
1417  j = 0;
1418 
1419 
1420  }
1421 */
1422  else {
1423  //std::cout << "elsed: " << getGraphNodeType(path[i]) << std::endl;
1424 
1425  i++;
1426  }
1427 
1428  }
1429  //if (yices_inconsistent(ctx)) {
1430  // std::cout << "inconsistent path: " << ipaths << std::endl;
1431  // ipaths++;
1432  // inconsistent = false;
1433 
1434  // }
1435  if (mainFlag) {
1436  //yices_del_context(ctx);
1437  }
1438 }
1439 
1440 StaticCFG::CFG* cfg;
1441 
1442 
1443 std::vector<int> breakTriple(std::vector<SgGraphNode*> expr) {
1444  SgNode* index = expr[0]->get_SgNode();
1445  std::vector<int> bounds(3, 0);
1446  bounds[0] = 0;
1447  size_t i = 1;
1448  while (expr[i]->get_SgNode() != index) {
1449  //std::cout << "expr[i]: " << cfg->toCFGNode(expr[i]).toString() << std::endl;
1450  ROSE_ASSERT(i < expr.size());
1451  i++;
1452  }
1453  bounds[1] = i;
1454  bounds[2] = expr.size()-1;
1455 
1456  return bounds;
1457  }
1458 
1459 
1460 
1461 //string mainParse(vector<SgGraphNode*> expr);
1462 string isAtom(SgNode*);
1463 bool isLogicalSplit(SgNode*);
1464 string getLogicalSplit(SgNode*);
1465 string getBinaryLogicOp(SgNode*);
1466 bool isBinaryLogicOp(SgNode*);
1467 bool isBinaryOp(SgNode*);
1468 string getBinaryOp(SgNode*);
1469 
1470 
1471 std::vector<SgGraphNode*> getSlice(std::vector<SgGraphNode*> vv, int i) {
1472  int cfgEnd = vv[i]->get_SgNode()->cfgIndexForEnd();
1473  int ind = 0;
1474  std::vector<SgGraphNode*> slice;
1475  if (cfgEnd == 0) {
1476  //std::cout << "nullend" << std::endl;
1477  slice.push_back(vv[i]);
1478  return slice;
1479  }
1480  slice.push_back(vv[i]);
1481  int k = i+1;
1482  while (true) {
1483  ROSE_ASSERT(cfgEnd != ind);
1484  //ROSE_ASSERT(k < vv.size());
1485  if (vv[i]->get_SgNode() == vv[k]->get_SgNode()) {
1486  ind++;
1487  if (ind == cfgEnd) {
1488  slice.push_back(vv[k]);
1489  return slice;
1490  }
1491  }
1492  slice.push_back(vv[k]);
1493  k++;
1494  }
1495 }
1496 
1497 //yices_expr evalFunction(vector<SgGraphNode*> funcLine, yices_context& ctx) {
1498 
1499 string getGraphNodeType(SgGraphNode* sn) {
1500  CFGNode cf = opencfg->toCFGNode(sn);
1501  string str = cf.toString();
1502  return str;
1503 }
1504 
1505 
1506 
1507 yices_expr mainParse(vector<SgGraphNode*> expr, yices_context& ctx) {
1508  //std::cout << "rounds" << rounds << std::endl;
1509  string typ = getGraphNodeType(expr[0]);
1510  //std::cout << "nodetype: " << typ << std::endl;
1511  //std::cout << "mainParse" << std::endl;
1512  rounds++;
1513  //bool yices = true;
1514  std::stringstream stst;
1515  string parsed;
1516  //bool unknown_flag = false;
1517  std::vector<SgGraphNode*> vec1;
1518  std::vector<SgGraphNode*> vec2;
1519  stringstream ss;
1520  yices_expr ret;
1521  if (expr.size() == 0) {
1522  yices_expr empty = new yices_expr;
1523  return empty;
1524  }
1525  //if (unknown_flag) {
1526  // yices_expr empty;
1527  // return empty;
1528  // }
1529  //else
1530  if (isSgReturnStmt(expr[0]->get_SgNode())) {
1531  ROSE_ASSERT(isSgReturnStmt(expr.back()));
1532  std::vector<SgGraphNode*> toSolve;
1533  for (size_t j = 1; j < expr.size()-1; j++) {
1534  toSolve.push_back(expr[j]);
1535  }
1536  yices_expr ts = mainParse(toSolve, ctx);
1537  return ts;
1538  }
1539  else if (isSgFunctionCallExp(expr[0]->get_SgNode())) {
1540  //yices_type ty;
1541  yices_type fty;
1542  yices_var_decl ftydecl;
1543  yices_expr f;
1544  bool ufunc = false;
1545  if (unknownFunctions.find(expr[0]->get_SgNode()) != unknownFunctions.end()) {
1546  //yices_expr unknown;;
1547  //return unknown;
1548 
1549  SgFunctionDeclaration* afd = (isSgFunctionCallExp(expr[0]->get_SgNode()))->getAssociatedFunctionDeclaration();
1550  SgType* ty = afd->get_orig_return_type();
1551  string ty_str = getType(ty);
1552  const char* ty_const_char = ty_str.c_str();
1553  yices_type rty = yices_mk_type(ctx,(char*)ty_const_char);
1554  SgInitializedNamePtrList sipl = afd->get_args();
1555  yices_type dom[sipl.size()];
1556  int iic = 0;;
1557  for (SgInitializedNamePtrList::iterator ii = sipl.begin(); ii != sipl.end(); ii++) {
1558  string domY = getType((*ii)->get_type());
1559  yices_type typdom = yices_mk_type(ctx,(char*)domY.c_str());
1560  dom[iic] = typdom;
1561 
1562  iic++;
1563  }
1564  int ds = iic;
1565  stringstream nam;
1566  nvars++;
1567  nam << afd->get_qualified_name().getString();
1568  nam << nvars;
1569  fty = yices_mk_function_type(ctx, dom, ds, rty);;
1570  ftydecl = yices_mk_var_decl(ctx, (char*) nam.str().c_str(),fty);
1571  f = yices_mk_var_from_decl(ctx, ftydecl);
1572 
1573  //yices_type fty = yices_mk_function_type(ctx, domain, 1, ty);
1574  // yices_var_decl fdecl = yices_mk_var_decl(ctx, "f", fty);
1575 
1576  ufunc = true;
1577  }
1578  int i = 1;
1579  while (!isSgExprListExp(expr[i]->get_SgNode())) {
1580  i++;
1581  if (i > (int)expr.size()) {
1582  ROSE_ASSERT(false);
1583  yices_expr empty = new yices_expr;
1584  return empty;
1585  }
1586  }
1587  int j = i+1;
1588  int checks = 0;
1589  std::vector<yices_expr> argsyices;
1590  std::vector<SgGraphNode*> yexp;
1591  while (checks != (int)expr[i]->get_SgNode()->cfgIndexForEnd()) {
1592  //std::vector<SgGraphNode*> yexp;
1593  while (expr[j]->get_SgNode() != expr[i]->get_SgNode()) {
1594  yexp.push_back(expr[j]);
1595  j++;
1596  if (j >= (int)expr.size()) {
1597  ROSE_ASSERT(false);
1598  yices_expr empty = new yices_expr;
1599  return empty;
1600  }
1601  }
1602  j++;
1603  //yices_expr argsaryices[argsyices.size()];
1604  //std::cout << "yexp: " << std::endl;
1605  //for (int qy = 0; qy < yexp.size(); qy++) {
1606  // std::cout << getGraphNodeType(yexp[qy]) << std::endl;
1607  // }
1608  //ROSE_ASSERT(false);
1609  // std::cout << std::endl;
1610  yices_expr yex = mainParse(yexp,ctx);
1611  //yices_assert(ctx, yex);
1612  ROSE_ASSERT(yex != NULL);
1613  argsyices.push_back(yex);
1614  checks++;
1615  }
1616  if (ufunc) {
1617  //yices_expr argsaryyices[argsyices.size()];
1618  // std::cout << "ufunc" << std::endl;
1619  yices_expr argsaryices[argsyices.size()];
1620  for (size_t tt = 0; tt < argsyices.size(); tt++) {
1621  argsaryices[tt] = argsyices[tt];
1622  }
1623 
1624  yices_expr app = yices_mk_app(ctx,f,argsaryices,argsyices.size());
1625  return app;
1626  }
1627  SgFunctionDeclaration* sgfd = isSgFunctionCallExp(expr[0]->get_SgNode())->getAssociatedFunctionDeclaration();
1628  SgFunctionParameterList* sfpl = sgfd->get_parameterList();
1629  SgInitializedNamePtrList sinp = sfpl->get_args();
1630  SgInitializedNamePtrList::iterator ite = sinp.begin();
1631  int argnum = 0;
1632  for (ite = sinp.begin(); ite != sinp.end(); ite++) {
1633  SgName svs = (isSgInitializedName((*ite)))->get_qualified_name();
1634  stringstream funN;
1635  nvars++;
1636  funN << svs.getString() << nvars;
1637  //funN << "V" << nvars;
1638  nameOf[svs] = funN.str();//funN.str();
1639  string valType = getType(isSgInitializedName(*ite)->get_type());
1640  yices_type ty1 = yices_mk_type(ctx, (char*) valType.c_str());
1641  yices_var_decl decl1 = yices_mk_var_decl(ctx, (char*) funN.str().c_str(), ty1);
1642  yices_expr e1 = yices_mk_var_from_decl(ctx, decl1);
1643  //yices_expr e2 = mainParse(vec2, ctx);
1644 
1645  //if (isSgVarRefExp(yexp[0]->get_SgNode())) {
1646  //getExpr[svs] = getExpr[isSgVarRefExp(yexp[0]->get_SgNode())->get_symbol()->get_name()];//argsyices[argnum];
1647  // }
1648  // else {
1649  ROSE_ASSERT(argsyices[argnum] != NULL);
1650  getExpr[svs] = argsyices[argnum];
1651 
1652  yices_expr exp = yices_mk_eq(ctx,e1,argsyices[argnum]);
1653  yices_assert(ctx,exp);
1654 
1655  // ROSE_ASSERT(false);
1656  //}
1657  argnum++;
1658  }
1659  //std::cout << "argnum: " << argnum << std::endl;
1660  //std::cout << std::endl;
1661  //for (int ww = 0; ww < expr.size(); ww++) {
1662  // std::cout << getGraphNodeType(expr[ww]) << std::endl;
1663  // }
1664  // std::cout << std::endl;
1665  ROSE_ASSERT(isSgFunctionCallExp(expr[j]->get_SgNode()));
1666  // std::cout << "graphnodeafterexp: " << getGraphNodeType(expr[j+1]) << std::endl;
1667  //ROSE_ASSERT(isSgFunctionCallExp(expr[j+1]->get_SgNode()));
1668  int k = j;
1669  //j+=2;
1670  //int k = j-2;
1671  std::vector<SgGraphNode*> funcLine;
1672  int check2 = 2;
1673  // std::cout << "k-1: " << getGraphNodeType(expr[k]) << std::endl;
1674  j++;
1675  //std::cout << "funcLinePath: " << std::endl;
1676  //for (int qt = 0; qt < expr.size(); qt++) {
1677  // std::cout << getGraphNodeType(expr[qt]) << std::endl;
1678  // }
1679  //std::cout << "endpath" << std::endl;
1680  //std::cout << std::endl;
1681  while (check2 < (int)expr[k]->get_SgNode()->cfgIndexForEnd()) {
1682  if (expr[k]->get_SgNode() == expr[j]->get_SgNode()) {
1683  check2++;
1684  //if (check2 >= expr[k]->get_SgNode()->cfgIndexForEnd()) {
1685  // break;
1686  //}
1687  //check2++;
1688  // funcLine.push_back(expr[j]);
1689  // j++;
1690  }
1691  //check2++;
1692  funcLine.push_back(expr[j]);
1693  j++;
1694  }
1695  // std::cout << "funcLine.size(): " << funcLine.size() << std::endl;
1696  //std::cout << "formed funcLine" << std::endl;
1697  std::vector<SgGraphNode*> funcLine2;
1698  for (size_t kk = 1; kk < funcLine.size()-1; kk++) {
1699  funcLine2.push_back(funcLine[kk]);
1700  }
1701  //std::cout << std::endl;
1702  // std::cout << "funcLine1 size: " << funcLine.size() << std::endl;
1703  // for (int ww2 = 0; ww2 < funcLine.size(); ww2++) {
1704  // std::cout << getGraphNodeType(funcLine[ww2]) << std::endl;
1705  // }
1706  // std::cout << std::endl;
1707  ROSE_ASSERT(!unknown_flag);
1708 
1709  yices_expr funcexp = evalFunction(funcLine2, ctx, false);
1710  ROSE_ASSERT(funcexp != NULL);
1711  return funcexp;
1712 
1713 
1714 
1715  }
1716  else if (isSgNotOp(expr[0]->get_SgNode())) {
1717  ret = yices_mk_fresh_bool_var(ctx);
1718  int i = 1;
1719  SgGraphNode* curr = expr[1];
1720  while (curr->get_SgNode() != expr[0]->get_SgNode()) {
1721  vec1.push_back(curr);
1722  i++;
1723  curr = expr[i];
1724  }
1725  yices_expr e1 = yices_mk_fresh_bool_var(ctx);
1726  e1 = mainParse(vec1, ctx);
1727  ret = yices_mk_not(ctx, e1);
1728  return ret;
1729  }
1730  else if (isLogicalSplit(expr[0]->get_SgNode())) {
1731  ret = yices_mk_fresh_bool_var(ctx);
1732  string ls = getLogicalSplit(expr[0]->get_SgNode());
1733  // std::vector<int> bounds = breakTriple(expr);
1734  std::map<int, std::vector<SgGraphNode*> > vec;
1735  std::vector<SgGraphNode*> vecX;
1736  int qt = 1;
1737  int curr = 0;
1738  //std::cout << "expr logical split: " << std::endl;
1739  //for (int qy = 0; qy < expr.size(); qy++) {
1740  // std::cout << getGraphNodeType(expr[qy]) << std::endl;
1741  // }
1742  // std::cout << std::endl;
1743  while (curr < 2) {
1744  if (expr[qt]->get_SgNode() == expr[0]->get_SgNode()) {
1745  vec[curr] = vecX;
1746  vecX.clear();
1747  curr++;
1748  }
1749  else {
1750  vecX.push_back(expr[qt]);
1751  }
1752  qt++;
1753  }
1754  vec1 = vec[0];
1755  vec2 = vec[1];
1756 /*
1757  for (int i = bounds[0]+1; i < bounds[1]; i++) {
1758  vec1.push_back(expr[i]);
1759  }
1760  for (int j = bounds[1]+1; j < bounds[2]; j++) {
1761  vec2.push_back(expr[j]);
1762  }
1763 */
1764  //if (yices) {
1765  yices_expr e1 = yices_mk_fresh_bool_var(ctx);
1766  yices_expr e2 = yices_mk_fresh_bool_var(ctx);
1767  // std::cout << "vec1: " << std::endl;
1768  //for (int qw = 0; qw < vec1.size(); qw++) {
1769  // std::cout << getGraphNodeType(vec1[qw]) << std::endl;
1770  // }
1771  // std::cout << "vec2: " << std::endl;
1772  // for (int qw2 = 0; qw2 < vec2.size(); qw2++) {
1773  // std::cout << getGraphNodeType(vec2[qw2]) << std::endl;
1774  // }
1775  // std::cout << "\n\n";
1776  e1 = mainParse(vec1, ctx);
1777  if (vec2.size() != 0) {
1778  e2 = mainParse(vec2, ctx);
1779  }
1780  //std::cout << "vec1.size()" << vec1.size() << " vec2.size(): " << vec2.size() << std::endl;
1781 
1782  if (vec1.size() == 0 && ls == "and") {
1783  e1 = yices_mk_false(ctx);
1784  }
1785  else if (vec1.size() == 0 && ls == "or") {
1786  e1 = yices_mk_true(ctx);
1787  }
1788  else if (vec2.size() == 0 && ls == "and") {
1789  e2 = yices_mk_false(ctx);
1790  }
1791  else if (vec2.size() == 0 && ls == "or") {
1792  e2 = yices_mk_true(ctx);
1793  }
1794 
1795  yices_expr arr[2];
1796  arr[0] = e1;
1797  arr[1] = e2;
1798  // yices_expr ret = yices_mk_fresh_bool_var(ctx);
1799  if (ls == "or") {
1800  ret = yices_mk_or(ctx, arr, 2);
1801  }
1802  else if (ls == "and") {
1803  ret = yices_mk_and(ctx, arr, 2);
1804  }
1805  else {
1806  //std::cout << "bad logical command" << std::endl;
1807  ROSE_ASSERT(false);
1808  }
1809  //yices_assert(ctx, ret);
1810  return ret;
1811  //}
1812  //stst << "( "<< ls << " " << mainParse(vec1) << " " << mainParse(vec2) << ")";
1813  //parsed = stst.str();
1814  //stst << "and " << mainParse(vec2) << ")\n";
1815 
1816  }
1817  else if (isBinaryLogicOp(expr[0]->get_SgNode()) || isBinaryOp(expr[0]->get_SgNode())) {
1818  //std::vector<int> bounds = breakTriple(expr);
1819  int i = 1;
1820  int check = 0;
1821  // std::cout << "binarylogic vec: " << std::endl;
1822  // for (int ws = 0; ws < expr.size(); ws++) {
1823  // std::cout << getGraphNodeType(expr[ws]) << std::endl;
1824  // }
1825  // std::cout << "endlogic" << std::endl;
1826  // std::cout << "\n";
1827  std::vector<SgGraphNode*> vecX;
1828  std::map<int, std::vector<SgGraphNode*> > vec;
1829  while (check < (int)expr[0]->get_SgNode()->cfgIndexForEnd()) {
1830  if (expr[0]->get_SgNode() == expr[i]->get_SgNode()) {
1831  vec[check] = vecX;
1832  vecX.clear();
1833  check++;
1834  if (check == (int)expr[0]->get_SgNode()->cfgIndexForEnd()) {
1835  break;
1836  }
1837  }
1838  if (expr[0]->get_SgNode() != expr[i]->get_SgNode()) {
1839  vecX.push_back(expr[i]);
1840  }
1841  i++;
1842  }
1843  vec1 = vec[0];
1844  vec2 = vec[1];
1845 /*
1846  for (int i = bounds[0]+1; i < bounds[1]; i++) {
1847  vec1.push_back(expr[i]);
1848  }
1849  for (int j = bounds[1]+1; j < bounds[2]; j++) {
1850  vec2.push_back(expr[j]);
1851  }
1852 */
1853  if (isBinaryLogicOp(expr[0]->get_SgNode())) {
1854  parsed = getBinaryLogicOp(expr[0]->get_SgNode());
1855  }
1856  else {
1857  parsed = getBinaryOp(expr[0]->get_SgNode());
1858  }
1859  //yices_expr ret;
1860  if (isBinaryLogicOp(expr[0]->get_SgNode())) {
1861  ret = yices_mk_fresh_bool_var(ctx);
1862  yices_expr e1 = mainParse(vec1, ctx);
1863  yices_expr e2 = mainParse(vec2, ctx);
1864  if (parsed == ">") {
1865  ret = yices_mk_gt(ctx,e1, e2);
1866  }
1867  else if (parsed == "<") {
1868  ret = yices_mk_lt(ctx, e1, e2);
1869  }
1870  else if (parsed == "=") {
1871  ret = yices_mk_eq(ctx, e1, e2);
1872  }
1873  else if (parsed == "!=") {
1874  ret = yices_mk_diseq(ctx, e1, e2);
1875  }
1876  else if (parsed == "<=") {
1877  ret = yices_mk_le(ctx, e1, e2);
1878  }
1879  else if (parsed == ">=") {
1880  ret = yices_mk_ge(ctx, e1, e2);
1881  }
1882  else {
1883  //std::cout << "unknown binary logic op" << std::endl;
1884  return ret;
1885  }
1886  //std::cout << "parsed: " << parsed << std::endl;
1887  ROSE_ASSERT(ret != NULL);
1888  //yices_assert(ctx, ret);
1889  return ret;
1890  }
1891  // stst << "( " << parsed << " " << mainParse(vec1) << " " << mainParse(vec2) << ")";
1892  else {
1893  yices_expr e1 = mainParse(vec1, ctx);
1894  yices_expr e2 = mainParse(vec2, ctx);
1895  yices_expr yicesarr[2];
1896  yicesarr[0] = e1;
1897  yicesarr[1] = e2;
1898  string bop = getBinaryOp(expr[0]->get_SgNode());
1899  if (bop == "+") {
1900 
1901  ret = yices_mk_sum(ctx, yicesarr, 2);
1902  }
1903  else if (bop == "-") {
1904  ret = yices_mk_sub(ctx, yicesarr, 2);
1905  }
1906  else if (bop == "*") {
1907  ret = yices_mk_mul(ctx, yicesarr, 2);
1908  }
1909  //else if (bop == "/") {
1910  // ret = yices_mk_div(ctx, e1, e2);
1911  // }
1912  else {
1913  //std::cout << "bad binary op: " << bop << endl;
1914  ROSE_ASSERT(false);
1915  }
1916  return ret;
1917  //stst << "( " << parsed << " " << mainParse(vec1) << " " << mainParse(vec2) << " ) ";
1918  }
1919  //parsed = stst.str();
1920  }
1921  else if (isSgPlusPlusOp(expr[0]->get_SgNode())) {
1922  for (size_t i = 1; i < expr.size() - 1; i++) {
1923  vec1.push_back(expr[i]);
1924  }
1925  yices_expr e1 = mainParse(vec1, ctx);
1926  stringstream funN;
1927  nvars++;
1928  funN << "V" << nvars;
1929 
1930  //char* fun = (char*) funN.str().c_str();
1931  //yices_type ty = yices_mk_type(ctx, "int");
1932  //yices_var_decl vdecl = yices_mk_var_decl(ctx, fun, ty);
1933  //yices_expr e2 = yices_mk_var_from_decl(ctx, vdecl);
1934  yices_expr arr[2];
1935  yices_expr en = yices_mk_num(ctx, 1);
1936  arr[0] = e1;
1937  arr[1] = en;
1938  ret = yices_mk_sum(ctx, arr, 2);
1939  return ret;
1940  }
1941  else if (isAtom(expr[0]->get_SgNode()) != "") {
1942  string ty = isAtom(expr[0]->get_SgNode());
1943  if (ty == "int") {
1944  int ival = isSgIntVal(expr[0]->get_SgNode())->get_value();
1945  ret = yices_mk_num(ctx, ival);
1946  //std::cout << "ival: " << ival << std::endl;
1947 
1948  //parsed = ss.str();
1949  }
1950  else if (ty == "double") {
1951  double dval = isSgDoubleVal(expr[0]->get_SgNode())->get_value();
1952  //ss << dval;
1953  //parsed = ss.str();
1954  ret = yices_mk_num(ctx, dval);
1955  }
1956  else if (ty == "float") {
1957  float fval = isSgFloatVal(expr[0]->get_SgNode())->get_value();
1958  // ss << fval;
1959  // parsed = ss.str();
1960  ret = yices_mk_num(ctx, fval);
1961  }
1962  else if (ty == "short") {
1963  short sval = isSgShortVal(expr[0]->get_SgNode())->get_value();
1964  //ss << sval;
1965  //parsed = ss.str();
1966  ret = yices_mk_num(ctx, sval);
1967  }
1968  else if (ty == "long") {
1969  long lval = isSgLongIntVal(expr[0]->get_SgNode())->get_value();
1970  //ss << lval;
1971  //parsed = ss.str();
1972  ret = yices_mk_num(ctx, lval);
1973  }
1974  else if (ty == "long long int") {
1975  long long llval = isSgLongLongIntVal(expr[0]->get_SgNode())->get_value();
1976  //ss << llval;
1977  //parsed = ss.str();
1978  ret = yices_mk_num(ctx, llval);
1979  }
1980  else if (ty == "long double") {
1981  long double lldval = isSgLongDoubleVal(expr[0]->get_SgNode())->get_value();
1982  //ss << lldval;
1983  //parsed = ss.str();
1984  ret = yices_mk_num(ctx, lldval);
1985  }
1986  else if (ty == "bool") {
1987  bool bval = isSgBoolValExp(expr[0]->get_SgNode())->get_value();
1988  if (bval == true) {
1989  parsed = "true";
1990  ret = yices_mk_true(ctx);
1991  }
1992  else {
1993  parsed = "false";
1994  ret = yices_mk_false(ctx);
1995  }
1996  }
1997  else {
1998  //cout << "unsupported atomic type";
1999  ROSE_ASSERT(false);
2000  }
2001  return ret;
2002  }
2003  else if (isSgVarRefExp((expr[0])->get_SgNode())) {
2004  SgName svs = isSgVarRefExp(expr[0]->get_SgNode())->get_symbol()->get_declaration()->get_qualified_name();
2005  //stringstream ss;
2006  ROSE_ASSERT(getExpr.find(svs) != getExpr.end());
2007  ROSE_ASSERT(nameOf.find(svs) != nameOf.end());
2008  // parsed = nameOf[svs];
2009  //}
2010  //else {
2011  // ss << "V" << nvars;
2012  // nvars++;
2013  // nameOf[svs] = ss.str();
2014  // parsed = nameOf[svs];
2015  //}
2016  //std::cout << "nameOf[svs]: " << nameOf[svs] << std::endl;
2017  yices_expr e1;// = new yices_expr;
2018  if (getExpr.find(svs) != getExpr.end()) {
2019  e1 = getExpr[svs];
2020  }
2021  else {
2022  SgType* typ = isSgVarRefExp(expr[0]->get_SgNode())->get_type();
2023  string valType = getType(typ);
2024  char* valTypeCh = (char*) valType.c_str();
2025  stringstream stst;
2026  nvars++;
2027  stst << svs.getString() << nvars;
2028  nameOf[svs] = stst.str();
2029 
2030  char* fun = (char*) stst.str().c_str();
2031  yices_type ty = yices_mk_type(ctx, valTypeCh);
2032  yices_var_decl vdecl = yices_mk_var_decl(ctx, fun, ty);
2033  e1 = yices_mk_var_from_decl(ctx, vdecl);
2034  getExpr[svs] = e1;
2035  }
2036  ret = e1;
2037  return ret;
2038 
2039  }
2040  else if (isSgInitializedName(expr[0]->get_SgNode())) {
2041  stringstream stst;
2042  std::vector<SgGraphNode*> vec1;
2043  //ROSE_ASSERT(isAtom((expr[2])->get_SgNode()) != "");
2044  // string valType = isAtom((expr[2])->get_SgNode());
2045  int p = 3;
2046 
2047 
2048  SgName svs = (isSgInitializedName(expr[0]->get_SgNode()))->get_qualified_name();
2049  SgType* typ = (isSgInitializedName(expr[0]->get_SgNode()))->get_type();
2050  string valType = getType(typ);
2051  //stringstream funN;
2052 /*
2053  funN << "V" << nvars;
2054  nvars++;
2055  char* fun = (char*) funN.str().c_str();
2056  char* valTypeCh = (char*) typ_str.c_str();
2057  yices_type ty = yices_mk_type(ctx, valTypeCh);
2058  yices_var_decl vdecl = yices_mk_var_decl(ctx, fun, ty);
2059  yices_expr e1 = yices_mk_var_from_decl(ctx, vdecl);
2060  getExpr[svs] = e1;
2061  nameOf[svs] = fun;
2062 */
2063 
2064 
2065 
2066  // SgName svs = (isSgInitializedName(expr[0]->get_SgNode()))->get_qualified_name();
2067 
2068  // if (isAtom(expr[2]) == "") {
2069 // SgName svs = (isSgInitializedName(expr[0]->get_SgNode()))->get_qualified_name();
2070  int check = 0;
2071  vec1.push_back(expr[2]);
2072  //std::cout << "expr[2]: " << getGraphNodeType(expr[2]) << std::endl;
2073  if (!isSgVarRefExp(vec1[0])) {
2074 
2075  while (/*expr[2]->get_SgNode() != expr[p]->get_SgNode()) { &&*/ check < (int)expr[2]->get_SgNode()->cfgIndexForEnd()) {
2076  if (expr[2]->get_SgNode() == expr[p]->get_SgNode()) {
2077  check++;
2078  if (check >= (int)expr[2]->get_SgNode()->cfgIndexForEnd()) {
2079  break;
2080  }
2081  }
2082  vec1.push_back(expr[p]);
2083  p++;
2084  //vec1.push_back(expr[p]);
2085  // p++;
2086  }
2087  vec1.push_back(expr[p]);
2088  }
2089  stringstream funN;
2090  string ss;
2091  //std::cout << "vec1: " << std::endl;
2092  // for (int tt = 0; tt < vec1.size(); tt++) {
2093  // std::cout << getGraphNodeType(vec1[tt]) << std::endl;
2094  // }
2095  // std::cout << "\n\n";
2096  //if (nameOf.find(svs) != nameOf.end()) {
2097  // ss = nameOf[svs];
2098  //}
2099  //else {
2100  nvars++;
2101  funN << svs.getString() << nvars;
2102  nameOf[svs] = funN.str();
2103  //ss = funN.str();
2104  //nvars++;
2105  //stst << "(declare-fun " << ss << " () " << valType << ")\n";
2106  //}i
2107  char* fun = (char*) funN.str().c_str();//funN.str().c_str();
2108  //for (int i = 0; i < funN.str().size(); i++) {
2109  // fun[i] = funN.str()[i];
2110  //}
2111  //std::cout << "fun: " << fun << std::endl;
2112  char* valTypeCh = (char*) valType.c_str();
2113  //for (int j = 0; j < valType.size(); j++) {
2114  // valTypeCh[j] = valType[j];
2115  //}
2116  //std::cout << "valTypeCh: " << valTypeCh << std::endl;
2117  //std::cout << "fun" << fun << std::endl;
2118  //char* fun = (char*)(funN.str().c_str());
2119  yices_type ty = yices_mk_type(ctx, valTypeCh);
2120  yices_var_decl vdecl = yices_mk_var_decl(ctx, fun, ty);
2121  yices_expr e1 = yices_mk_var_from_decl(ctx, vdecl);
2122  //getType[e1] = valType;
2123  //getExpr[svs] = e1;
2124  //std::cout << "vec1.size(): " << vec1.size() << std::endl;
2125  //std::cout << "vec1[0]: " << getGraphNodeType(vec1[0]) << std::endl;
2126 
2127  //ROSE_ASSERT(e2 != NULL);
2128  //ret = yices_mk_eq(ctx,e1,e1);
2129  /*yices_expr e2 =*/ mainParse(vec1,ctx);
2130  if (unknown_flag || unknowns.find(isSgInitializedName(expr[0]->get_SgNode())) != unknowns.end()) {
2131  if (unknown_flag || unknowns.find(isSgInitializedName(expr[0]->get_SgNode())) != unknowns.end()) {
2132  unknowns[isSgInitializedName(expr[0]->get_SgNode())] = vdecl;
2133  //if (!usingNots) {
2134  unknownvdeclis.push_back(vdecl);
2135 
2136  IName[vdecl] = isSgInitializedName(expr[0]->get_SgNode());
2137  //}
2138  if (usingNots) {
2139  //std::cout << "uN" << std::endl;
2140  ROSE_ASSERT(notMap.find(isSgInitializedName(expr[0]->get_SgNode())) != notMap.end());
2141  for (size_t j = 0; j < notMap[isSgInitializedName(expr[0]->get_SgNode())].size(); j++) {
2142  int jv = notMap[isSgInitializedName(expr[0]->get_SgNode())][j];
2143  yices_expr jvexpr =yices_mk_num(ctx, jv);
2144  yices_expr ei = yices_mk_diseq(ctx, e1, jvexpr);
2145  yices_assert(ctx,ei);
2146  }
2147  }
2148  // unknowndecls.push_back(vdecl);
2149  }
2150  getExpr[svs] = e1;
2151  unknown_flag = false;
2152  ret = yices_mk_eq(ctx, e1, e1);
2153  }
2154  else {
2155  yices_expr e2 = mainParse(vec1, ctx);
2156  // std::cout << "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n";
2157  // std::cout << "valType: " << valType << std::endl;
2158  // std::cout << "vec1: " << std::endl;
2159  // for (int rr = 0; rr < vec1.size(); rr++) {
2160  // std::cout << getGraphNodeType(vec1[rr]) << std::endl;
2161  // }
2162  // std::cout << "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n\n";
2163 
2164  //yices_expr e2 = mainParse(vec1, ctx);
2165  ROSE_ASSERT(e1 != NULL);
2166  ROSE_ASSERT(e2 != NULL);
2167  ret = yices_mk_eq(ctx, e1, e2);
2168  getExpr[svs] = e2;
2169 
2170  }
2171  //yices_assert(ctx, ret);
2172  //stst << "(let (" << ss << " " << mainParse(vec1) << ")\n";
2173  //parsed = stst.str();
2174 
2175  return ret;
2176  }
2177  else if (isSgVariableDeclaration(expr[0]->get_SgNode())) {
2178  // ROSE_ASSERT(isSgVariableDeclaration(expr.back()->get_SgNode()));
2179  std::vector<SgGraphNode*> expr2;
2180  //std::cout << "back node: " << getGraphNodeType(expr.back()) << std::endl;
2181  ROSE_ASSERT(isSgVariableDeclaration(expr.back()->get_SgNode()));
2182  for (size_t tt = 1; tt < expr.size()-1; tt++) {
2183  expr2.push_back(expr[tt]);
2184  }
2185  yices_expr y2 = mainParse(expr2, ctx);
2186  ret = y2;
2187  return ret;
2188  }
2189 
2190  else if (isSgAssignOp(expr[0]->get_SgNode())) {
2191  stringstream stst;
2192  ROSE_ASSERT(isSgVarRefExp(expr[1]->get_SgNode()));
2193  //ROSE_ASSERT(isAtom(expr[3]->get_SgNode()) != "");
2194  //string valType = isAtom(expr[3]->get_SgNode());
2195  std::vector<int> bounds = breakTriple(expr);
2196  //for (int i = bounds[0]+1; i < bounds[1]; i++) {
2197  // vec1.push_back(expr[i]);
2198  //}
2199  SgName svs = (isSgVarRefExp((expr[1]->get_SgNode()))->get_symbol()->get_declaration()->get_qualified_name());
2200  SgType* typ = isSgVarRefExp((expr[1]->get_SgNode()))->get_symbol()->get_declaration()->get_type();
2201  string valType = getType(typ);
2202  for (int j = bounds[1]+1; j < bounds[2]; j++) {
2203  vec2.push_back(expr[j]);
2204  }
2205  if (nameOf.find(svs) != nameOf.end()) {
2206  stringstream ss;
2207  nvars++;
2208  ss << svs.getString();
2209  ss << nvars;
2210  //nvars++;
2211  yices_type ty1 = yices_mk_type(ctx, (char*) valType.c_str());
2212  yices_var_decl decl1 = yices_mk_var_decl(ctx, (char*) ss.str().c_str(), ty1);
2213  yices_expr e1 = yices_mk_var_from_decl(ctx, decl1);
2214  yices_expr e2 = mainParse(vec2, ctx);
2215  if (unknown_flag) {
2216  unknown_flag = false;
2217  ret = yices_mk_eq(ctx, e1, e1);
2218  getExpr[svs] = e1;
2219  }
2220  else {
2221  ret = yices_mk_eq(ctx, e1, e2);
2222  getExpr[svs] = e2;
2223  }
2224  nameOf[svs] = ss.str();
2225  //getExpr[svs] = e2;
2226  return ret;
2227  }
2228  else {
2229  stringstream ss;
2230  // ss << "V";
2231  // ss << nvars;
2232  nvars++;
2233  ss << svs.getString();
2234  ss << nvars;
2235  char valTypeCh[valType.size()];
2236  for (size_t k = 0; k < valType.size(); k++) {
2237  valTypeCh[k] = valType[k];
2238  }
2239  char nam[ss.str().size()];
2240  for (size_t q = 0; q < ss.str().size(); q++) {
2241  nam[q] = ss.str()[q];
2242  }
2243  string fun = valType;
2244  //char* funC = fun.c_str();
2245  yices_type ty = yices_mk_type(ctx, (char*) valType.c_str());
2246  yices_var_decl decl1 = yices_mk_var_decl(ctx,(char*) ss.str().c_str(), ty);
2247  yices_expr e1 = yices_mk_var_from_decl(ctx, decl1);
2248  yices_expr e2 = mainParse(vec2, ctx);
2249  //if (forFlag) {
2250  // ret = yices_mk_eq(ctx, e1, e1);
2251  // }
2252  // else {
2253  ret = yices_mk_eq(ctx, e1, e2);
2254  // }
2255  getExpr[svs] = e2;
2256  nameOf[svs] = ss.str();//svs.getString();//fun;
2257  }
2258  //yices_assert(ctx, ret);
2259  //getExpr[svs] = e1;
2260  //stringstream stst;
2261  //noAssert = true;
2262 
2263  // stst << "(let (" << mainParse(vec1) << " " << mainParse(vec2) << ") )";
2264  //parsed = stst.str();
2265  return ret;
2266  }
2267  else if (isSgExprStatement(expr[0]->get_SgNode())) {
2268 
2269  ROSE_ASSERT(isSgExprStatement(expr.back()->get_SgNode()));
2270  std::vector<SgGraphNode*> nexpr;
2271  for (size_t q = 1; q < expr.size()-1; q++) {
2272  nexpr.push_back(expr[q]);
2273  }
2274  yices_expr y2 = mainParse(nexpr, ctx);
2275  return y2;
2276  }
2277  else {
2278  //cout << "unknown type" << endl;
2279  //cout << getGraphNodeType(expr[0]) << std::endl;//cfg->toCFGNode(expr[0]).toString() << std::endl;
2280  //ROSE_ASSERT(false);
2281  //ROSE_ASSERT(false);
2282  unknown_flag = true;
2283  yices_expr y1 = yices_mk_fresh_bool_var(ctx);
2284  return y1;
2285  }
2286  //std::cout << "parsed: " << parsed << std::endl;
2287  return ret;
2288 }
2289 
2290 string isAtom(SgNode* n) {
2291  if (isSgIntVal(n)) {
2292  return "int";
2293  }
2294  else if (isSgDoubleVal(n)) {
2295  return "double";
2296  }
2297  else if (isSgFloatVal(n)) {
2298  return "float";
2299  }
2300  else if (isSgShortVal(n)) {
2301  return "short";
2302  }
2303  else if (isSgLongIntVal(n)) {
2304  return "long";
2305  }
2306  else if (isSgLongLongIntVal(n)) {
2307  return "long long int";
2308  }
2309  else if (isSgLongDoubleVal(n)) {
2310  return "long double";
2311  }
2312  else if (isSgBoolValExp(n)) {
2313  return "bool";
2314  }
2315  return "";
2316 }
2317 
2318 bool isLogicalSplit(SgNode* n) {
2319  if (isSgAndOp(n) || isSgOrOp(n) || isSgNotOp(n)) {
2320  return true;
2321  }
2322  return false;
2323 }
2324 
2325 std::string getLogicalSplit(SgNode* n) {
2326  if (isSgAndOp(n)) {
2327  return "and";
2328  }
2329  else if (isSgOrOp(n)) {
2330  return "or";
2331  }
2332  else if (isSgNotOp(n)) {
2333  return "not";
2334  }
2335  else {
2336  // cout << "not a logicalSplit Operator" << std::endl;
2337  ROSE_ASSERT(false);
2338  }
2339 }
2340 
2341 std::string getBinaryLogicOp(SgNode* n) {
2342  std::string ss;
2343  if (isSgEqualityOp(n)) {
2344  ss = "=";
2345  }
2346  else if (isSgLessThanOp(n)) {
2347  ss = "<";
2348  }
2349  else if (isSgGreaterThanOp(n)) {
2350  ss = ">";
2351  }
2352  else if (isSgNotEqualOp(n)) {
2353  ss = "/=";
2354  }
2355  else {
2356  //std::cout << "bad eqOp" << std::endl;
2357  ROSE_ASSERT(false);
2358  }
2359  return ss;
2360 }
2361 
2362 bool isBinaryLogicOp(SgNode* n) {
2363  if (isSgEqualityOp(n) || isSgLessThanOp(n) || isSgGreaterThanOp(n) || isSgNotEqualOp(n)) {
2364  return true;
2365  }
2366  else {
2367  return false;
2368  }
2369 }
2370 
2371 bool isBinaryOp(SgNode* n) {
2372  if (isSgAddOp(n) || isSgSubtractOp(n) || isSgMultiplyOp(n) || isSgDivideOp(n)) {
2373  return true;
2374  }
2375  else {
2376  return false;
2377  }
2378 }
2379 
2380 std::string getBinaryOp(SgNode* n) {
2381  std::string ss;
2382  if (isSgAddOp(n)) {
2383  ss = "+";
2384  }
2385  else if (isSgSubtractOp(n)) {
2386  ss = "-";
2387  }
2388  else if (isSgMultiplyOp(n)) {
2389  ss = "*";
2390  }
2391  else if (isSgDivideOp(n)) {
2392  ss = "/";
2393  }
2394  else {
2395  //std::cout << "unknown op in getBinaryOp" << std::endl;
2396  ROSE_ASSERT(false);
2397  }
2398  return ss;
2399 }
2400 
2401 
2402 /*
2403 int main(int argc, char *argv[]) {
2404 
2405  struct timeval t1, t2;
2406  SgProject* proj = frontend(argc,argv);
2407  ROSE_ASSERT (proj != NULL);
2408 
2409  SgFunctionDeclaration* mainDefDecl = SageInterface::findMain(proj);
2410 
2411  SgFunctionDefinition* mainDef = mainDefDecl->get_definition();
2412  visitorTraversal* vis = new visitorTraversal();
2413  StaticCFG::CFG cfg(mainDef);
2414  //cfg.buildFullCFG();
2415  stringstream ss;
2416  string fileName= StringUtility::stripPathFromFileName(mainDef->get_file_info()->get_filenameString());
2417  string dotFileName1=fileName+"."+ mainDef->get_declaration()->get_name() +".dot";
2418 
2419  cfgToDot(mainDef,dotFileName1);
2420  //cfg->buildFullCFG();
2421  SgIncidenceDirectedGraph* g = new SgIncidenceDirectedGraph();
2422  g = cfg.getGraph();
2423  myGraph* mg = new myGraph();
2424  mg = instantiateGraph(g, cfg);
2425  vis->tltnodes = 0;
2426  vis->paths = 0;
2427  ipaths = 0;
2428  vis->orig = mg;
2429  vis->g = g;
2430  //vis->firstPrepGraph(constcfg);
2431  //t1 = getCPUTime();
2432  vis->constructPathAnalyzer(mg, true);
2433  //t2 = getCPUTime();
2434  //std::cout << "took: " << timeDifference(t2, t1) << std::endl;
2435  //cfg.clearNodesAndEdges();
2436  std::cout << "finished" << std::endl;
2437  std::cout << "tltnodes: " << vis->tltnodes << " paths: " << vis->paths << " ipaths: " << ipaths << std::endl;
2438  //delete vis;
2439  return 0;
2440 }
2441 */
2442 
2443 int yicesCheck(int argc, char **argv) {
2444 //int main(int argc, char *argv[]) {
2445  FORLOOPS = 10;
2446  string y = "yices.txt";
2447  yices_enable_log_file((char*) y.c_str());
2448  qst = 0;
2449  string fileSaver = "saviorStuff";
2450  //ofstream fout;
2451  // fout.open(fileSaver.c_str(),ios::app);
2452 
2453  SgProject* proj = frontend(argc,argv);
2454  ROSE_ASSERT (proj != NULL);
2455 
2456 SgFunctionDefinition* mainDef = SageInterface::findMain(proj)->get_definition();
2457  Rose_STL_Container<SgNode*> functionDeclarationList = NodeQuery::querySubTree(proj,V_SgFunctionDeclaration);
2458  Rose_STL_Container<SgNode*> functionDefinitionList = NodeQuery::querySubTree(proj, V_SgFunctionDefinition);
2459  // std::cout << "functionDeclarationList.size(): " << functionDeclarationList.size() << std::endl;
2460  // std::cout << "functionDefinitionList.size(): " << functionDefinitionList.size() << std::endl;
2461  //ROSE_ASSERT(false);
2462  std::vector<SgNode*> funcs;
2463  for (Rose_STL_Container<SgNode*>::iterator i = functionDefinitionList.begin(); i != functionDefinitionList.end(); i++) {
2464  if (isSgFunctionDefinition(*i) != mainDef) {
2465  SgFunctionDefinition* fni = isSgFunctionDefinition(*i);
2466  ROSE_ASSERT(fni != NULL);
2467  //ROSE_ASSERT(find(funcs.begin(), funcs.end(), fni) == funcs.end());
2468  funcs.push_back(fni);
2469  }
2470  }
2471  //std::cout << "funcs.size(): " << funcs.size() << std::endl;
2472  //ROSE_ASSERT(false);
2473  //int jj = 0;
2474  for (unsigned int i = 0; i < funcs.size(); i++) {
2475  // if (funcs[i] != mainDef) {
2476  visitorTraversalFunc* visfunc = new visitorTraversalFunc();
2477  //SgFunctionDeclaration* sfd = isSgFunctionDeclaration(funcs[i]);
2478  SgFunctionDefinition* sfdd = isSgFunctionDefinition(funcs[i]);
2479  //}
2480 int counter = i;
2481  SgFunctionDefinition* fnc = isSgFunctionDefinition(sfdd);
2482  if (fnc != NULL) {
2483  stringstream ss;
2484  SgFunctionDeclaration* functionDeclaration = fnc->get_declaration();
2485 
2486  string fileName= functionDeclaration->get_name().str();//StringUtility::stripPathFromFileName(mainDef->get_file_info()->get_filenameString());
2487  string dotFileName1;
2488 ss << fileName << "." << counter << ".dot";
2489  counter++;
2490  dotFileName1 = ss.str();
2491  StaticCFG::InterproceduralCFG* cfg = new StaticCFG::InterproceduralCFG(fnc);
2492  SgIncidenceDirectedGraph* g = new SgIncidenceDirectedGraph();
2493 // visitorTraversalFunc* vis = new visitorTraversalFunc();
2494  g = cfg->getGraph();
2495  CFGforT* mg = new CFGforT();
2496  mg = instantiateGraph(g, *cfg, fnc);
2497  visfunc->tltnodes = 0;
2498  //visfunc->paths = 0;
2499  //std::vector<std::vector<VertexID> > pt;
2500  //visfunc->paths = pt;
2501  visfunc->orig = mg;
2502  //visfunc->cfg = cfg;
2503  //visfunc->g = g;
2504  visfunc->constructPathAnalyzer(mg, true, 0, 0, true);
2505  std::vector<std::vector<SgGraphNode*> > vp = visfunc->vpaths;
2506  ROSE_ASSERT(sfdd != NULL);
2507  FuncPathMap[sfdd] = vp;
2508  //std::cout << "vp.size(): " << vp.size() << std::endl;
2509 
2510 }
2511 }
2512 /*
2513 int jjf = 0;
2514 std::vector<SgGraphNode*> paths;
2515 paths.push_back(path);
2516 std::vector<SgNode*> called;
2517  while (jjf != paths.size()) {
2518  std::cout << "propagating" << std::endl;
2519  path = paths[jjf];
2520  int jj = 0;
2521  while (jj != path.size()) {
2522  if (isSgFunctionCallExp(path[jj]->get_SgNode()) && find(called.begin(), called.end(), path[jj]->get_SgNode()) == called.end()) {
2523  propagateFunctionCall(path, jj, jjf);
2524  called.push_back(path[jj]->get_SgNode());
2525  jjf = 0;
2526  // noadd = true;
2527  jj = 0;
2528  break;
2529  }
2530  else {
2531  jj++;
2532  }
2533  }
2534  if (noadd) {
2535  noadd = false;
2536  }
2537 
2538  else {
2539  jjf++;
2540  }
2541  }
2542 
2543  std::cout << "paths.size(): " << paths.size() << std::endl;
2544  //ROSE_ASSERT(false);
2545  pathnumber += paths.size();
2546  std::vector<SgNode*> ncalled;
2547 
2548 for (int q = 0; q < paths.size(); q++) {
2549  std::vector<SgGraphNode*> path = path[q];
2550  ROSE_ASSERT(mainDef != NULL);
2551  //if (mainDefDecl != NULL) {
2552 */
2553  //SgFunctionDefinition* mainDef = mainDefDecl->get_definition();
2554  visitorTraversal* vis = new visitorTraversal();
2555  StaticCFG::CFG* cfg = new StaticCFG::CFG(mainDef);
2556  vis->pathnumber = 0;
2557  stringstream ss;
2558  string fileName= StringUtility::stripPathFromFileName(mainDef->get_file_info()->get_filenameString());
2559  string dotFileName1=fileName+"."+ mainDef->get_declaration()->get_name() +".dot";
2560 
2561  SgIncidenceDirectedGraph* g = new SgIncidenceDirectedGraph();
2562  g = cfg->getGraph();
2563  myGraph* mg = new myGraph();
2564  mg = instantiateGraph(g, *cfg);
2565  vis->tltnodes = 0;
2566  //vis->pathnumber = 0;
2567  ipaths = 0;
2568  vis->orig = mg;
2569  //openorig = mg;
2570  vis->g = g;
2571  //openg = g;
2572  vis->cfg = cfg;
2573  //opencfg = cfg;
2574 
2575  vis->constructPathAnalyzer(mg, true);
2576  //if (ipaths > 0) {
2577  cout << "filename: " << fileName << std::endl;
2578  cout << "finished" << std::endl;
2579  cout << "paths: " << vis->pathnumber << " ipaths: " << ipaths << std::endl;
2580  //}
2581  // }
2582  // fout.close();
2583  return 0;
2584 }
2585 
2586 
2587 
2588 // int main(int argc, char *argv[]) {
2589 // pathnum = 0;
2590 // ipaths = 0;
2591 // SgProject* proj = frontend(argc,argv);
2592 // ROSE_ASSERT (proj != NULL);
2593 //
2594 // SgFunctionDeclaration* mainDefDecl = SageInterface::findMain(proj);
2595 //
2596 // SgFunctionDefinition* mainDef = mainDefDecl->get_definition();
2597 // visitorTraversal* vis = new visitorTraversal();
2598 // visitorTraversal* vis2 = new visitorTraversal();
2599 // nGraph = new newGraph();
2600 // //vis->nGraph = nGraph;
2601 // //newGraph* nnGraph = new newGraph();
2602 // StaticCFG::CFG* cfg1 = new StaticCFG::CFG(mainDef);
2603 // //cfg.buildFullCFG();
2604 // stringstream ss;
2605 // string fileName= StringUtility::stripPathFromFileName(mainDef->get_file_info()->get_filenameString());
2606 // string dotFileName1=fileName+"."+ mainDef->get_declaration()->get_name() +".dot";
2607 //
2608 // cfgToDot(mainDef,dotFileName1);
2609 // //cfg->buildFullCFG();
2610 // //SgIncidenceDirectedGraph* cf = new SgIncidenceDirectedGraph();
2611 // SgIncidenceDirectedGraph* cf = cfg1->getGraph();
2612 // myGraph* mg = new myGraph();
2613 // mg = instantiateGraph(cf, *cfg1);
2614 // vis2->tltnodes = 0;
2615 // vis2->paths = 0;
2616 // vis->tltnodes = 0;
2617 // vis->paths = 0;
2618 // //vis->firstPrepGraph(constcfg);
2619 // vis->g = cf;
2620 // vis2->g = cf;
2621 // vis2->orig = mg;
2622 // cfg = cfg1;
2623 // vis->orig = mg;
2624 // vis->constructPathAnalyzer(mg, true);
2625 // std::cout << "constructed" << std::endl;
2626 // std::cout << "ipaths: " << ipaths << std::endl;
2627 // // printHotness2(nGraph);
2628 // // std::cout << "mapped" << std::endl;i
2629 // std::vector<std::vector<int> > pts;
2630 // std::vector<int> ptsP;
2631 // //std::vector<SgExpressionStmt*> exprs = SageInterface::querySubTree<SgExpressionStmt>(proj);
2632 // for (int q1 = 0; q1 < exprs.size(); q1++) {
2633 // ptsP.clear();
2634 // for (int q2 = 0; q2 < exprs.size(); q2++) {
2635 // if (q1 != q2) {
2636 // vis->paths = 0;
2637 // vis->tltnodes = 0;
2638 // vis->constructPathAnalyzer(mg, exprs[q1], exprs[q2]);
2639 // std::cout << vis->paths << " between expr" << q1 << " and expr" << q2 << std::endl;
2640 // ptsP.push_back(vis->paths);
2641 // }
2642 // pts.push_back(ptsP);
2643 // }
2644 // }
2645 // for (int i = 0; i < pts.size(); i++) {
2646 // for (int j = 0; j < pts[i].size(); j++) {
2647 // std::cout << "between expr" << i << "and expr" << j << " there are " << pts[i][j] << std::endl;
2648 // }
2649 // }
2650 //
2651 // //cfg.clearNodesAndEdges();
2652 // //std::cout << "finished" << std::endl;
2653 // //std::cout << "tltnodes: " << vis->tltnodes << " paths: " << vis->paths << std::endl;
2654 // //delete vis;
2655 // //}
2656 
2657 
2658 /*
2659 std::vector<SgExprStatement*> exprList = SageInterface::querySubTree<SgExprStatement>(project);
2660 for (Rose_STL_Container<SgGraphNode*>::iterator i = exprList.begin(); i != exprList.end(); i++) {
2661 */
2662 
2663 // SgExprStatement* expr = isSgExprStatement(*i);
2664