ROSE  0.11.145.0
yicesParserLib.h
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_ABORT();
1583  }
1584  }
1585  int j = i+1;
1586  int checks = 0;
1587  std::vector<yices_expr> argsyices;
1588  std::vector<SgGraphNode*> yexp;
1589  while (checks != (int)expr[i]->get_SgNode()->cfgIndexForEnd()) {
1590  //std::vector<SgGraphNode*> yexp;
1591  while (expr[j]->get_SgNode() != expr[i]->get_SgNode()) {
1592  yexp.push_back(expr[j]);
1593  j++;
1594  if (j >= (int)expr.size()) {
1595  ROSE_ABORT();
1596  }
1597  }
1598  j++;
1599  //yices_expr argsaryices[argsyices.size()];
1600  //std::cout << "yexp: " << std::endl;
1601  //for (int qy = 0; qy < yexp.size(); qy++) {
1602  // std::cout << getGraphNodeType(yexp[qy]) << std::endl;
1603  // }
1604  //ROSE_ASSERT(false);
1605  // std::cout << std::endl;
1606  yices_expr yex = mainParse(yexp,ctx);
1607  //yices_assert(ctx, yex);
1608  ROSE_ASSERT(yex != NULL);
1609  argsyices.push_back(yex);
1610  checks++;
1611  }
1612  if (ufunc) {
1613  //yices_expr argsaryyices[argsyices.size()];
1614  // std::cout << "ufunc" << std::endl;
1615  yices_expr argsaryices[argsyices.size()];
1616  for (size_t tt = 0; tt < argsyices.size(); tt++) {
1617  argsaryices[tt] = argsyices[tt];
1618  }
1619 
1620  yices_expr app = yices_mk_app(ctx,f,argsaryices,argsyices.size());
1621  return app;
1622  }
1623  SgFunctionDeclaration* sgfd = isSgFunctionCallExp(expr[0]->get_SgNode())->getAssociatedFunctionDeclaration();
1624  SgFunctionParameterList* sfpl = sgfd->get_parameterList();
1625  SgInitializedNamePtrList sinp = sfpl->get_args();
1626  SgInitializedNamePtrList::iterator ite = sinp.begin();
1627  int argnum = 0;
1628  for (ite = sinp.begin(); ite != sinp.end(); ite++) {
1629  SgName svs = (isSgInitializedName((*ite)))->get_qualified_name();
1630  stringstream funN;
1631  nvars++;
1632  funN << svs.getString() << nvars;
1633  //funN << "V" << nvars;
1634  nameOf[svs] = funN.str();//funN.str();
1635  string valType = getType(isSgInitializedName(*ite)->get_type());
1636  yices_type ty1 = yices_mk_type(ctx, (char*) valType.c_str());
1637  yices_var_decl decl1 = yices_mk_var_decl(ctx, (char*) funN.str().c_str(), ty1);
1638  yices_expr e1 = yices_mk_var_from_decl(ctx, decl1);
1639  //yices_expr e2 = mainParse(vec2, ctx);
1640 
1641  //if (isSgVarRefExp(yexp[0]->get_SgNode())) {
1642  //getExpr[svs] = getExpr[isSgVarRefExp(yexp[0]->get_SgNode())->get_symbol()->get_name()];//argsyices[argnum];
1643  // }
1644  // else {
1645  ROSE_ASSERT(argsyices[argnum] != NULL);
1646  getExpr[svs] = argsyices[argnum];
1647 
1648  yices_expr exp = yices_mk_eq(ctx,e1,argsyices[argnum]);
1649  yices_assert(ctx,exp);
1650 
1651  // ROSE_ASSERT(false);
1652  //}
1653  argnum++;
1654  }
1655  //std::cout << "argnum: " << argnum << std::endl;
1656  //std::cout << std::endl;
1657  //for (int ww = 0; ww < expr.size(); ww++) {
1658  // std::cout << getGraphNodeType(expr[ww]) << std::endl;
1659  // }
1660  // std::cout << std::endl;
1661  ROSE_ASSERT(isSgFunctionCallExp(expr[j]->get_SgNode()));
1662  // std::cout << "graphnodeafterexp: " << getGraphNodeType(expr[j+1]) << std::endl;
1663  //ROSE_ASSERT(isSgFunctionCallExp(expr[j+1]->get_SgNode()));
1664  int k = j;
1665  //j+=2;
1666  //int k = j-2;
1667  std::vector<SgGraphNode*> funcLine;
1668  int check2 = 2;
1669  // std::cout << "k-1: " << getGraphNodeType(expr[k]) << std::endl;
1670  j++;
1671  //std::cout << "funcLinePath: " << std::endl;
1672  //for (int qt = 0; qt < expr.size(); qt++) {
1673  // std::cout << getGraphNodeType(expr[qt]) << std::endl;
1674  // }
1675  //std::cout << "endpath" << std::endl;
1676  //std::cout << std::endl;
1677  while (check2 < (int)expr[k]->get_SgNode()->cfgIndexForEnd()) {
1678  if (expr[k]->get_SgNode() == expr[j]->get_SgNode()) {
1679  check2++;
1680  //if (check2 >= expr[k]->get_SgNode()->cfgIndexForEnd()) {
1681  // break;
1682  //}
1683  //check2++;
1684  // funcLine.push_back(expr[j]);
1685  // j++;
1686  }
1687  //check2++;
1688  funcLine.push_back(expr[j]);
1689  j++;
1690  }
1691  // std::cout << "funcLine.size(): " << funcLine.size() << std::endl;
1692  //std::cout << "formed funcLine" << std::endl;
1693  std::vector<SgGraphNode*> funcLine2;
1694  for (size_t kk = 1; kk < funcLine.size()-1; kk++) {
1695  funcLine2.push_back(funcLine[kk]);
1696  }
1697  //std::cout << std::endl;
1698  // std::cout << "funcLine1 size: " << funcLine.size() << std::endl;
1699  // for (int ww2 = 0; ww2 < funcLine.size(); ww2++) {
1700  // std::cout << getGraphNodeType(funcLine[ww2]) << std::endl;
1701  // }
1702  // std::cout << std::endl;
1703  ROSE_ASSERT(!unknown_flag);
1704 
1705  yices_expr funcexp = evalFunction(funcLine2, ctx, false);
1706  ROSE_ASSERT(funcexp != NULL);
1707  return funcexp;
1708 
1709 
1710 
1711  }
1712  else if (isSgNotOp(expr[0]->get_SgNode())) {
1713  ret = yices_mk_fresh_bool_var(ctx);
1714  int i = 1;
1715  SgGraphNode* curr = expr[1];
1716  while (curr->get_SgNode() != expr[0]->get_SgNode()) {
1717  vec1.push_back(curr);
1718  i++;
1719  curr = expr[i];
1720  }
1721  yices_expr e1 = yices_mk_fresh_bool_var(ctx);
1722  e1 = mainParse(vec1, ctx);
1723  ret = yices_mk_not(ctx, e1);
1724  return ret;
1725  }
1726  else if (isLogicalSplit(expr[0]->get_SgNode())) {
1727  ret = yices_mk_fresh_bool_var(ctx);
1728  string ls = getLogicalSplit(expr[0]->get_SgNode());
1729  // std::vector<int> bounds = breakTriple(expr);
1730  std::map<int, std::vector<SgGraphNode*> > vec;
1731  std::vector<SgGraphNode*> vecX;
1732  int qt = 1;
1733  int curr = 0;
1734  //std::cout << "expr logical split: " << std::endl;
1735  //for (int qy = 0; qy < expr.size(); qy++) {
1736  // std::cout << getGraphNodeType(expr[qy]) << std::endl;
1737  // }
1738  // std::cout << std::endl;
1739  while (curr < 2) {
1740  if (expr[qt]->get_SgNode() == expr[0]->get_SgNode()) {
1741  vec[curr] = vecX;
1742  vecX.clear();
1743  curr++;
1744  }
1745  else {
1746  vecX.push_back(expr[qt]);
1747  }
1748  qt++;
1749  }
1750  vec1 = vec[0];
1751  vec2 = vec[1];
1752 /*
1753  for (int i = bounds[0]+1; i < bounds[1]; i++) {
1754  vec1.push_back(expr[i]);
1755  }
1756  for (int j = bounds[1]+1; j < bounds[2]; j++) {
1757  vec2.push_back(expr[j]);
1758  }
1759 */
1760  //if (yices) {
1761  yices_expr e1 = yices_mk_fresh_bool_var(ctx);
1762  yices_expr e2 = yices_mk_fresh_bool_var(ctx);
1763  // std::cout << "vec1: " << std::endl;
1764  //for (int qw = 0; qw < vec1.size(); qw++) {
1765  // std::cout << getGraphNodeType(vec1[qw]) << std::endl;
1766  // }
1767  // std::cout << "vec2: " << std::endl;
1768  // for (int qw2 = 0; qw2 < vec2.size(); qw2++) {
1769  // std::cout << getGraphNodeType(vec2[qw2]) << std::endl;
1770  // }
1771  // std::cout << "\n\n";
1772  e1 = mainParse(vec1, ctx);
1773  if (vec2.size() != 0) {
1774  e2 = mainParse(vec2, ctx);
1775  }
1776  //std::cout << "vec1.size()" << vec1.size() << " vec2.size(): " << vec2.size() << std::endl;
1777 
1778  if (vec1.size() == 0 && ls == "and") {
1779  e1 = yices_mk_false(ctx);
1780  }
1781  else if (vec1.size() == 0 && ls == "or") {
1782  e1 = yices_mk_true(ctx);
1783  }
1784  else if (vec2.size() == 0 && ls == "and") {
1785  e2 = yices_mk_false(ctx);
1786  }
1787  else if (vec2.size() == 0 && ls == "or") {
1788  e2 = yices_mk_true(ctx);
1789  }
1790 
1791  yices_expr arr[2];
1792  arr[0] = e1;
1793  arr[1] = e2;
1794  // yices_expr ret = yices_mk_fresh_bool_var(ctx);
1795  if (ls == "or") {
1796  ret = yices_mk_or(ctx, arr, 2);
1797  }
1798  else if (ls == "and") {
1799  ret = yices_mk_and(ctx, arr, 2);
1800  }
1801  else {
1802  //std::cout << "bad logical command" << std::endl;
1803  ROSE_ABORT();
1804  }
1805  //yices_assert(ctx, ret);
1806  return ret;
1807  //}
1808  //stst << "( "<< ls << " " << mainParse(vec1) << " " << mainParse(vec2) << ")";
1809  //parsed = stst.str();
1810  //stst << "and " << mainParse(vec2) << ")\n";
1811 
1812  }
1813  else if (isBinaryLogicOp(expr[0]->get_SgNode()) || isBinaryOp(expr[0]->get_SgNode())) {
1814  //std::vector<int> bounds = breakTriple(expr);
1815  int i = 1;
1816  int check = 0;
1817  // std::cout << "binarylogic vec: " << std::endl;
1818  // for (int ws = 0; ws < expr.size(); ws++) {
1819  // std::cout << getGraphNodeType(expr[ws]) << std::endl;
1820  // }
1821  // std::cout << "endlogic" << std::endl;
1822  // std::cout << "\n";
1823  std::vector<SgGraphNode*> vecX;
1824  std::map<int, std::vector<SgGraphNode*> > vec;
1825  while (check < (int)expr[0]->get_SgNode()->cfgIndexForEnd()) {
1826  if (expr[0]->get_SgNode() == expr[i]->get_SgNode()) {
1827  vec[check] = vecX;
1828  vecX.clear();
1829  check++;
1830  if (check == (int)expr[0]->get_SgNode()->cfgIndexForEnd()) {
1831  break;
1832  }
1833  }
1834  if (expr[0]->get_SgNode() != expr[i]->get_SgNode()) {
1835  vecX.push_back(expr[i]);
1836  }
1837  i++;
1838  }
1839  vec1 = vec[0];
1840  vec2 = vec[1];
1841 /*
1842  for (int i = bounds[0]+1; i < bounds[1]; i++) {
1843  vec1.push_back(expr[i]);
1844  }
1845  for (int j = bounds[1]+1; j < bounds[2]; j++) {
1846  vec2.push_back(expr[j]);
1847  }
1848 */
1849  if (isBinaryLogicOp(expr[0]->get_SgNode())) {
1850  parsed = getBinaryLogicOp(expr[0]->get_SgNode());
1851  }
1852  else {
1853  parsed = getBinaryOp(expr[0]->get_SgNode());
1854  }
1855  //yices_expr ret;
1856  if (isBinaryLogicOp(expr[0]->get_SgNode())) {
1857  ret = yices_mk_fresh_bool_var(ctx);
1858  yices_expr e1 = mainParse(vec1, ctx);
1859  yices_expr e2 = mainParse(vec2, ctx);
1860  if (parsed == ">") {
1861  ret = yices_mk_gt(ctx,e1, e2);
1862  }
1863  else if (parsed == "<") {
1864  ret = yices_mk_lt(ctx, e1, e2);
1865  }
1866  else if (parsed == "=") {
1867  ret = yices_mk_eq(ctx, e1, e2);
1868  }
1869  else if (parsed == "!=") {
1870  ret = yices_mk_diseq(ctx, e1, e2);
1871  }
1872  else if (parsed == "<=") {
1873  ret = yices_mk_le(ctx, e1, e2);
1874  }
1875  else if (parsed == ">=") {
1876  ret = yices_mk_ge(ctx, e1, e2);
1877  }
1878  else {
1879  //std::cout << "unknown binary logic op" << std::endl;
1880  return ret;
1881  }
1882  //std::cout << "parsed: " << parsed << std::endl;
1883  ROSE_ASSERT(ret != NULL);
1884  //yices_assert(ctx, ret);
1885  return ret;
1886  }
1887  // stst << "( " << parsed << " " << mainParse(vec1) << " " << mainParse(vec2) << ")";
1888  else {
1889  yices_expr e1 = mainParse(vec1, ctx);
1890  yices_expr e2 = mainParse(vec2, ctx);
1891  yices_expr yicesarr[2];
1892  yicesarr[0] = e1;
1893  yicesarr[1] = e2;
1894  string bop = getBinaryOp(expr[0]->get_SgNode());
1895  if (bop == "+") {
1896 
1897  ret = yices_mk_sum(ctx, yicesarr, 2);
1898  }
1899  else if (bop == "-") {
1900  ret = yices_mk_sub(ctx, yicesarr, 2);
1901  }
1902  else if (bop == "*") {
1903  ret = yices_mk_mul(ctx, yicesarr, 2);
1904  }
1905  //else if (bop == "/") {
1906  // ret = yices_mk_div(ctx, e1, e2);
1907  // }
1908  else {
1909  //std::cout << "bad binary op: " << bop << endl;
1910  ROSE_ABORT();
1911  }
1912  return ret;
1913  //stst << "( " << parsed << " " << mainParse(vec1) << " " << mainParse(vec2) << " ) ";
1914  }
1915  //parsed = stst.str();
1916  }
1917  else if (isSgPlusPlusOp(expr[0]->get_SgNode())) {
1918  for (size_t i = 1; i < expr.size() - 1; i++) {
1919  vec1.push_back(expr[i]);
1920  }
1921  yices_expr e1 = mainParse(vec1, ctx);
1922  stringstream funN;
1923  nvars++;
1924  funN << "V" << nvars;
1925 
1926  //char* fun = (char*) funN.str().c_str();
1927  //yices_type ty = yices_mk_type(ctx, "int");
1928  //yices_var_decl vdecl = yices_mk_var_decl(ctx, fun, ty);
1929  //yices_expr e2 = yices_mk_var_from_decl(ctx, vdecl);
1930  yices_expr arr[2];
1931  yices_expr en = yices_mk_num(ctx, 1);
1932  arr[0] = e1;
1933  arr[1] = en;
1934  ret = yices_mk_sum(ctx, arr, 2);
1935  return ret;
1936  }
1937  else if (isAtom(expr[0]->get_SgNode()) != "") {
1938  string ty = isAtom(expr[0]->get_SgNode());
1939  if (ty == "int") {
1940  int ival = isSgIntVal(expr[0]->get_SgNode())->get_value();
1941  ret = yices_mk_num(ctx, ival);
1942  //std::cout << "ival: " << ival << std::endl;
1943 
1944  //parsed = ss.str();
1945  }
1946  else if (ty == "double") {
1947  double dval = isSgDoubleVal(expr[0]->get_SgNode())->get_value();
1948  //ss << dval;
1949  //parsed = ss.str();
1950  ret = yices_mk_num(ctx, dval);
1951  }
1952  else if (ty == "float") {
1953  float fval = isSgFloatVal(expr[0]->get_SgNode())->get_value();
1954  // ss << fval;
1955  // parsed = ss.str();
1956  ret = yices_mk_num(ctx, fval);
1957  }
1958  else if (ty == "short") {
1959  short sval = isSgShortVal(expr[0]->get_SgNode())->get_value();
1960  //ss << sval;
1961  //parsed = ss.str();
1962  ret = yices_mk_num(ctx, sval);
1963  }
1964  else if (ty == "long") {
1965  long lval = isSgLongIntVal(expr[0]->get_SgNode())->get_value();
1966  //ss << lval;
1967  //parsed = ss.str();
1968  ret = yices_mk_num(ctx, lval);
1969  }
1970  else if (ty == "long long int") {
1971  long long llval = isSgLongLongIntVal(expr[0]->get_SgNode())->get_value();
1972  //ss << llval;
1973  //parsed = ss.str();
1974  ret = yices_mk_num(ctx, llval);
1975  }
1976  else if (ty == "long double") {
1977  long double lldval = isSgLongDoubleVal(expr[0]->get_SgNode())->get_value();
1978  //ss << lldval;
1979  //parsed = ss.str();
1980  ret = yices_mk_num(ctx, lldval);
1981  }
1982  else if (ty == "bool") {
1983  bool bval = isSgBoolValExp(expr[0]->get_SgNode())->get_value();
1984  if (bval == true) {
1985  parsed = "true";
1986  ret = yices_mk_true(ctx);
1987  }
1988  else {
1989  parsed = "false";
1990  ret = yices_mk_false(ctx);
1991  }
1992  }
1993  else {
1994  //cout << "unsupported atomic type";
1995  ROSE_ABORT();
1996  }
1997  return ret;
1998  }
1999  else if (isSgVarRefExp((expr[0])->get_SgNode())) {
2000  SgName svs = isSgVarRefExp(expr[0]->get_SgNode())->get_symbol()->get_declaration()->get_qualified_name();
2001  //stringstream ss;
2002  ROSE_ASSERT(getExpr.find(svs) != getExpr.end());
2003  ROSE_ASSERT(nameOf.find(svs) != nameOf.end());
2004  // parsed = nameOf[svs];
2005  //}
2006  //else {
2007  // ss << "V" << nvars;
2008  // nvars++;
2009  // nameOf[svs] = ss.str();
2010  // parsed = nameOf[svs];
2011  //}
2012  //std::cout << "nameOf[svs]: " << nameOf[svs] << std::endl;
2013  yices_expr e1;// = new yices_expr;
2014  if (getExpr.find(svs) != getExpr.end()) {
2015  e1 = getExpr[svs];
2016  }
2017  else {
2018  SgType* typ = isSgVarRefExp(expr[0]->get_SgNode())->get_type();
2019  string valType = getType(typ);
2020  char* valTypeCh = (char*) valType.c_str();
2021  stringstream stst;
2022  nvars++;
2023  stst << svs.getString() << nvars;
2024  nameOf[svs] = stst.str();
2025 
2026  char* fun = (char*) stst.str().c_str();
2027  yices_type ty = yices_mk_type(ctx, valTypeCh);
2028  yices_var_decl vdecl = yices_mk_var_decl(ctx, fun, ty);
2029  e1 = yices_mk_var_from_decl(ctx, vdecl);
2030  getExpr[svs] = e1;
2031  }
2032  ret = e1;
2033  return ret;
2034 
2035  }
2036  else if (isSgInitializedName(expr[0]->get_SgNode())) {
2037  stringstream stst;
2038  std::vector<SgGraphNode*> vec1;
2039  //ROSE_ASSERT(isAtom((expr[2])->get_SgNode()) != "");
2040  // string valType = isAtom((expr[2])->get_SgNode());
2041  int p = 3;
2042 
2043 
2044  SgName svs = (isSgInitializedName(expr[0]->get_SgNode()))->get_qualified_name();
2045  SgType* typ = (isSgInitializedName(expr[0]->get_SgNode()))->get_type();
2046  string valType = getType(typ);
2047  //stringstream funN;
2048 /*
2049  funN << "V" << nvars;
2050  nvars++;
2051  char* fun = (char*) funN.str().c_str();
2052  char* valTypeCh = (char*) typ_str.c_str();
2053  yices_type ty = yices_mk_type(ctx, valTypeCh);
2054  yices_var_decl vdecl = yices_mk_var_decl(ctx, fun, ty);
2055  yices_expr e1 = yices_mk_var_from_decl(ctx, vdecl);
2056  getExpr[svs] = e1;
2057  nameOf[svs] = fun;
2058 */
2059 
2060 
2061 
2062  // SgName svs = (isSgInitializedName(expr[0]->get_SgNode()))->get_qualified_name();
2063 
2064  // if (isAtom(expr[2]) == "") {
2065 // SgName svs = (isSgInitializedName(expr[0]->get_SgNode()))->get_qualified_name();
2066  int check = 0;
2067  vec1.push_back(expr[2]);
2068  //std::cout << "expr[2]: " << getGraphNodeType(expr[2]) << std::endl;
2069  if (!isSgVarRefExp(vec1[0])) {
2070 
2071  while (/*expr[2]->get_SgNode() != expr[p]->get_SgNode()) { &&*/ check < (int)expr[2]->get_SgNode()->cfgIndexForEnd()) {
2072  if (expr[2]->get_SgNode() == expr[p]->get_SgNode()) {
2073  check++;
2074  if (check >= (int)expr[2]->get_SgNode()->cfgIndexForEnd()) {
2075  break;
2076  }
2077  }
2078  vec1.push_back(expr[p]);
2079  p++;
2080  //vec1.push_back(expr[p]);
2081  // p++;
2082  }
2083  vec1.push_back(expr[p]);
2084  }
2085  stringstream funN;
2086  string ss;
2087  //std::cout << "vec1: " << std::endl;
2088  // for (int tt = 0; tt < vec1.size(); tt++) {
2089  // std::cout << getGraphNodeType(vec1[tt]) << std::endl;
2090  // }
2091  // std::cout << "\n\n";
2092  //if (nameOf.find(svs) != nameOf.end()) {
2093  // ss = nameOf[svs];
2094  //}
2095  //else {
2096  nvars++;
2097  funN << svs.getString() << nvars;
2098  nameOf[svs] = funN.str();
2099  //ss = funN.str();
2100  //nvars++;
2101  //stst << "(declare-fun " << ss << " () " << valType << ")\n";
2102  //}i
2103  char* fun = (char*) funN.str().c_str();//funN.str().c_str();
2104  //for (int i = 0; i < funN.str().size(); i++) {
2105  // fun[i] = funN.str()[i];
2106  //}
2107  //std::cout << "fun: " << fun << std::endl;
2108  char* valTypeCh = (char*) valType.c_str();
2109  //for (int j = 0; j < valType.size(); j++) {
2110  // valTypeCh[j] = valType[j];
2111  //}
2112  //std::cout << "valTypeCh: " << valTypeCh << std::endl;
2113  //std::cout << "fun" << fun << std::endl;
2114  //char* fun = (char*)(funN.str().c_str());
2115  yices_type ty = yices_mk_type(ctx, valTypeCh);
2116  yices_var_decl vdecl = yices_mk_var_decl(ctx, fun, ty);
2117  yices_expr e1 = yices_mk_var_from_decl(ctx, vdecl);
2118  //getType[e1] = valType;
2119  //getExpr[svs] = e1;
2120  //std::cout << "vec1.size(): " << vec1.size() << std::endl;
2121  //std::cout << "vec1[0]: " << getGraphNodeType(vec1[0]) << std::endl;
2122 
2123  //ROSE_ASSERT(e2 != NULL);
2124  //ret = yices_mk_eq(ctx,e1,e1);
2125  /*yices_expr e2 =*/ mainParse(vec1,ctx);
2126  if (unknown_flag || unknowns.find(isSgInitializedName(expr[0]->get_SgNode())) != unknowns.end()) {
2127  if (unknown_flag || unknowns.find(isSgInitializedName(expr[0]->get_SgNode())) != unknowns.end()) {
2128  unknowns[isSgInitializedName(expr[0]->get_SgNode())] = vdecl;
2129  //if (!usingNots) {
2130  unknownvdeclis.push_back(vdecl);
2131 
2132  IName[vdecl] = isSgInitializedName(expr[0]->get_SgNode());
2133  //}
2134  if (usingNots) {
2135  //std::cout << "uN" << std::endl;
2136  ROSE_ASSERT(notMap.find(isSgInitializedName(expr[0]->get_SgNode())) != notMap.end());
2137  for (size_t j = 0; j < notMap[isSgInitializedName(expr[0]->get_SgNode())].size(); j++) {
2138  int jv = notMap[isSgInitializedName(expr[0]->get_SgNode())][j];
2139  yices_expr jvexpr =yices_mk_num(ctx, jv);
2140  yices_expr ei = yices_mk_diseq(ctx, e1, jvexpr);
2141  yices_assert(ctx,ei);
2142  }
2143  }
2144  // unknowndecls.push_back(vdecl);
2145  }
2146  getExpr[svs] = e1;
2147  unknown_flag = false;
2148  ret = yices_mk_eq(ctx, e1, e1);
2149  }
2150  else {
2151  yices_expr e2 = mainParse(vec1, ctx);
2152  // std::cout << "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n";
2153  // std::cout << "valType: " << valType << std::endl;
2154  // std::cout << "vec1: " << std::endl;
2155  // for (int rr = 0; rr < vec1.size(); rr++) {
2156  // std::cout << getGraphNodeType(vec1[rr]) << std::endl;
2157  // }
2158  // std::cout << "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n\n";
2159 
2160  //yices_expr e2 = mainParse(vec1, ctx);
2161  ROSE_ASSERT(e1 != NULL);
2162  ROSE_ASSERT(e2 != NULL);
2163  ret = yices_mk_eq(ctx, e1, e2);
2164  getExpr[svs] = e2;
2165 
2166  }
2167  //yices_assert(ctx, ret);
2168  //stst << "(let (" << ss << " " << mainParse(vec1) << ")\n";
2169  //parsed = stst.str();
2170 
2171  return ret;
2172  }
2173  else if (isSgVariableDeclaration(expr[0]->get_SgNode())) {
2174  // ROSE_ASSERT(isSgVariableDeclaration(expr.back()->get_SgNode()));
2175  std::vector<SgGraphNode*> expr2;
2176  //std::cout << "back node: " << getGraphNodeType(expr.back()) << std::endl;
2177  ROSE_ASSERT(isSgVariableDeclaration(expr.back()->get_SgNode()));
2178  for (size_t tt = 1; tt < expr.size()-1; tt++) {
2179  expr2.push_back(expr[tt]);
2180  }
2181  yices_expr y2 = mainParse(expr2, ctx);
2182  ret = y2;
2183  return ret;
2184  }
2185 
2186  else if (isSgAssignOp(expr[0]->get_SgNode())) {
2187  stringstream stst;
2188  ROSE_ASSERT(isSgVarRefExp(expr[1]->get_SgNode()));
2189  //ROSE_ASSERT(isAtom(expr[3]->get_SgNode()) != "");
2190  //string valType = isAtom(expr[3]->get_SgNode());
2191  std::vector<int> bounds = breakTriple(expr);
2192  //for (int i = bounds[0]+1; i < bounds[1]; i++) {
2193  // vec1.push_back(expr[i]);
2194  //}
2195  SgName svs = (isSgVarRefExp((expr[1]->get_SgNode()))->get_symbol()->get_declaration()->get_qualified_name());
2196  SgType* typ = isSgVarRefExp((expr[1]->get_SgNode()))->get_symbol()->get_declaration()->get_type();
2197  string valType = getType(typ);
2198  for (int j = bounds[1]+1; j < bounds[2]; j++) {
2199  vec2.push_back(expr[j]);
2200  }
2201  if (nameOf.find(svs) != nameOf.end()) {
2202  stringstream ss;
2203  nvars++;
2204  ss << svs.getString();
2205  ss << nvars;
2206  //nvars++;
2207  yices_type ty1 = yices_mk_type(ctx, (char*) valType.c_str());
2208  yices_var_decl decl1 = yices_mk_var_decl(ctx, (char*) ss.str().c_str(), ty1);
2209  yices_expr e1 = yices_mk_var_from_decl(ctx, decl1);
2210  yices_expr e2 = mainParse(vec2, ctx);
2211  if (unknown_flag) {
2212  unknown_flag = false;
2213  ret = yices_mk_eq(ctx, e1, e1);
2214  getExpr[svs] = e1;
2215  }
2216  else {
2217  ret = yices_mk_eq(ctx, e1, e2);
2218  getExpr[svs] = e2;
2219  }
2220  nameOf[svs] = ss.str();
2221  //getExpr[svs] = e2;
2222  return ret;
2223  }
2224  else {
2225  stringstream ss;
2226  // ss << "V";
2227  // ss << nvars;
2228  nvars++;
2229  ss << svs.getString();
2230  ss << nvars;
2231  char valTypeCh[valType.size()];
2232  for (size_t k = 0; k < valType.size(); k++) {
2233  valTypeCh[k] = valType[k];
2234  }
2235  char nam[ss.str().size()];
2236  for (size_t q = 0; q < ss.str().size(); q++) {
2237  nam[q] = ss.str()[q];
2238  }
2239  string fun = valType;
2240  //char* funC = fun.c_str();
2241  yices_type ty = yices_mk_type(ctx, (char*) valType.c_str());
2242  yices_var_decl decl1 = yices_mk_var_decl(ctx,(char*) ss.str().c_str(), ty);
2243  yices_expr e1 = yices_mk_var_from_decl(ctx, decl1);
2244  yices_expr e2 = mainParse(vec2, ctx);
2245  //if (forFlag) {
2246  // ret = yices_mk_eq(ctx, e1, e1);
2247  // }
2248  // else {
2249  ret = yices_mk_eq(ctx, e1, e2);
2250  // }
2251  getExpr[svs] = e2;
2252  nameOf[svs] = ss.str();//svs.getString();//fun;
2253  }
2254  //yices_assert(ctx, ret);
2255  //getExpr[svs] = e1;
2256  //stringstream stst;
2257  //noAssert = true;
2258 
2259  // stst << "(let (" << mainParse(vec1) << " " << mainParse(vec2) << ") )";
2260  //parsed = stst.str();
2261  return ret;
2262  }
2263  else if (isSgExprStatement(expr[0]->get_SgNode())) {
2264 
2265  ROSE_ASSERT(isSgExprStatement(expr.back()->get_SgNode()));
2266  std::vector<SgGraphNode*> nexpr;
2267  for (size_t q = 1; q < expr.size()-1; q++) {
2268  nexpr.push_back(expr[q]);
2269  }
2270  yices_expr y2 = mainParse(nexpr, ctx);
2271  return y2;
2272  }
2273  else {
2274  //cout << "unknown type" << endl;
2275  //cout << getGraphNodeType(expr[0]) << std::endl;//cfg->toCFGNode(expr[0]).toString() << std::endl;
2276  //ROSE_ASSERT(false);
2277  //ROSE_ASSERT(false);
2278  unknown_flag = true;
2279  yices_expr y1 = yices_mk_fresh_bool_var(ctx);
2280  return y1;
2281  }
2282  //std::cout << "parsed: " << parsed << std::endl;
2283  return ret;
2284 }
2285 
2286 string isAtom(SgNode* n) {
2287  if (isSgIntVal(n)) {
2288  return "int";
2289  }
2290  else if (isSgDoubleVal(n)) {
2291  return "double";
2292  }
2293  else if (isSgFloatVal(n)) {
2294  return "float";
2295  }
2296  else if (isSgShortVal(n)) {
2297  return "short";
2298  }
2299  else if (isSgLongIntVal(n)) {
2300  return "long";
2301  }
2302  else if (isSgLongLongIntVal(n)) {
2303  return "long long int";
2304  }
2305  else if (isSgLongDoubleVal(n)) {
2306  return "long double";
2307  }
2308  else if (isSgBoolValExp(n)) {
2309  return "bool";
2310  }
2311  return "";
2312 }
2313 
2314 bool isLogicalSplit(SgNode* n) {
2315  if (isSgAndOp(n) || isSgOrOp(n) || isSgNotOp(n)) {
2316  return true;
2317  }
2318  return false;
2319 }
2320 
2321 std::string getLogicalSplit(SgNode* n) {
2322  if (isSgAndOp(n)) {
2323  return "and";
2324  }
2325  else if (isSgOrOp(n)) {
2326  return "or";
2327  }
2328  else if (isSgNotOp(n)) {
2329  return "not";
2330  }
2331  else {
2332  // cout << "not a logicalSplit Operator" << std::endl;
2333  ROSE_ABORT();
2334  }
2335 }
2336 
2337 std::string getBinaryLogicOp(SgNode* n) {
2338  std::string ss;
2339  if (isSgEqualityOp(n)) {
2340  ss = "=";
2341  }
2342  else if (isSgLessThanOp(n)) {
2343  ss = "<";
2344  }
2345  else if (isSgGreaterThanOp(n)) {
2346  ss = ">";
2347  }
2348  else if (isSgNotEqualOp(n)) {
2349  ss = "/=";
2350  }
2351  else {
2352  //std::cout << "bad eqOp" << std::endl;
2353  ROSE_ABORT();
2354  }
2355  return ss;
2356 }
2357 
2358 bool isBinaryLogicOp(SgNode* n) {
2359  if (isSgEqualityOp(n) || isSgLessThanOp(n) || isSgGreaterThanOp(n) || isSgNotEqualOp(n)) {
2360  return true;
2361  }
2362  else {
2363  return false;
2364  }
2365 }
2366 
2367 bool isBinaryOp(SgNode* n) {
2368  if (isSgAddOp(n) || isSgSubtractOp(n) || isSgMultiplyOp(n) || isSgDivideOp(n)) {
2369  return true;
2370  }
2371  else {
2372  return false;
2373  }
2374 }
2375 
2376 std::string getBinaryOp(SgNode* n) {
2377  std::string ss;
2378  if (isSgAddOp(n)) {
2379  ss = "+";
2380  }
2381  else if (isSgSubtractOp(n)) {
2382  ss = "-";
2383  }
2384  else if (isSgMultiplyOp(n)) {
2385  ss = "*";
2386  }
2387  else if (isSgDivideOp(n)) {
2388  ss = "/";
2389  }
2390  else {
2391  //std::cout << "unknown op in getBinaryOp" << std::endl;
2392  ROSE_ABORT();
2393  }
2394  return ss;
2395 }
2396 
2397 
2398 /*
2399 int main(int argc, char *argv[]) {
2400 
2401  struct timeval t1, t2;
2402  SgProject* proj = frontend(argc,argv);
2403  ROSE_ASSERT (proj != NULL);
2404 
2405  SgFunctionDeclaration* mainDefDecl = SageInterface::findMain(proj);
2406 
2407  SgFunctionDefinition* mainDef = mainDefDecl->get_definition();
2408  visitorTraversal* vis = new visitorTraversal();
2409  StaticCFG::CFG cfg(mainDef);
2410  //cfg.buildFullCFG();
2411  stringstream ss;
2412  string fileName= StringUtility::stripPathFromFileName(mainDef->get_file_info()->get_filenameString());
2413  string dotFileName1=fileName+"."+ mainDef->get_declaration()->get_name() +".dot";
2414 
2415  cfgToDot(mainDef,dotFileName1);
2416  //cfg->buildFullCFG();
2417  SgIncidenceDirectedGraph* g = new SgIncidenceDirectedGraph();
2418  g = cfg.getGraph();
2419  myGraph* mg = new myGraph();
2420  mg = instantiateGraph(g, cfg);
2421  vis->tltnodes = 0;
2422  vis->paths = 0;
2423  ipaths = 0;
2424  vis->orig = mg;
2425  vis->g = g;
2426  //vis->firstPrepGraph(constcfg);
2427  //t1 = getCPUTime();
2428  vis->constructPathAnalyzer(mg, true);
2429  //t2 = getCPUTime();
2430  //std::cout << "took: " << timeDifference(t2, t1) << std::endl;
2431  //cfg.clearNodesAndEdges();
2432  std::cout << "finished" << std::endl;
2433  std::cout << "tltnodes: " << vis->tltnodes << " paths: " << vis->paths << " ipaths: " << ipaths << std::endl;
2434  //delete vis;
2435  return 0;
2436 }
2437 */
2438 
2439 int yicesCheck(int argc, char **argv) {
2440 //int main(int argc, char *argv[]) {
2441  FORLOOPS = 10;
2442  string y = "yices.txt";
2443  yices_enable_log_file((char*) y.c_str());
2444  qst = 0;
2445  string fileSaver = "saviorStuff";
2446  //ofstream fout;
2447  // fout.open(fileSaver.c_str(),ios::app);
2448 
2449  SgProject* proj = frontend(argc,argv);
2450  ROSE_ASSERT (proj != NULL);
2451 
2452 SgFunctionDefinition* mainDef = SageInterface::findMain(proj)->get_definition();
2453  Rose_STL_Container<SgNode*> functionDeclarationList = NodeQuery::querySubTree(proj,V_SgFunctionDeclaration);
2454  Rose_STL_Container<SgNode*> functionDefinitionList = NodeQuery::querySubTree(proj, V_SgFunctionDefinition);
2455  // std::cout << "functionDeclarationList.size(): " << functionDeclarationList.size() << std::endl;
2456  // std::cout << "functionDefinitionList.size(): " << functionDefinitionList.size() << std::endl;
2457  //ROSE_ASSERT(false);
2458  std::vector<SgNode*> funcs;
2459  for (Rose_STL_Container<SgNode*>::iterator i = functionDefinitionList.begin(); i != functionDefinitionList.end(); i++) {
2460  if (isSgFunctionDefinition(*i) != mainDef) {
2461  SgFunctionDefinition* fni = isSgFunctionDefinition(*i);
2462  ROSE_ASSERT(fni != NULL);
2463  //ROSE_ASSERT(find(funcs.begin(), funcs.end(), fni) == funcs.end());
2464  funcs.push_back(fni);
2465  }
2466  }
2467  //std::cout << "funcs.size(): " << funcs.size() << std::endl;
2468  //ROSE_ASSERT(false);
2469  //int jj = 0;
2470  for (unsigned int i = 0; i < funcs.size(); i++) {
2471  // if (funcs[i] != mainDef) {
2472  visitorTraversalFunc* visfunc = new visitorTraversalFunc();
2473  //SgFunctionDeclaration* sfd = isSgFunctionDeclaration(funcs[i]);
2474  SgFunctionDefinition* sfdd = isSgFunctionDefinition(funcs[i]);
2475  //}
2476 int counter = i;
2477  SgFunctionDefinition* fnc = isSgFunctionDefinition(sfdd);
2478  if (fnc != NULL) {
2479  stringstream ss;
2480  SgFunctionDeclaration* functionDeclaration = fnc->get_declaration();
2481 
2482  string fileName= functionDeclaration->get_name().str();//StringUtility::stripPathFromFileName(mainDef->get_file_info()->get_filenameString());
2483  string dotFileName1;
2484 ss << fileName << "." << counter << ".dot";
2485  counter++;
2486  dotFileName1 = ss.str();
2487  StaticCFG::InterproceduralCFG* cfg = new StaticCFG::InterproceduralCFG(fnc);
2488  SgIncidenceDirectedGraph* g = new SgIncidenceDirectedGraph();
2489 // visitorTraversalFunc* vis = new visitorTraversalFunc();
2490  g = cfg->getGraph();
2491  CFGforT* mg = new CFGforT();
2492  mg = instantiateGraph(g, *cfg, fnc);
2493  visfunc->tltnodes = 0;
2494  //visfunc->paths = 0;
2495  //std::vector<std::vector<VertexID> > pt;
2496  //visfunc->paths = pt;
2497  visfunc->orig = mg;
2498  //visfunc->cfg = cfg;
2499  //visfunc->g = g;
2500  visfunc->constructPathAnalyzer(mg, true, 0, 0, true);
2501  std::vector<std::vector<SgGraphNode*> > vp = visfunc->vpaths;
2502  ROSE_ASSERT(sfdd != NULL);
2503  FuncPathMap[sfdd] = vp;
2504  //std::cout << "vp.size(): " << vp.size() << std::endl;
2505 
2506 }
2507 }
2508 /*
2509 int jjf = 0;
2510 std::vector<SgGraphNode*> paths;
2511 paths.push_back(path);
2512 std::vector<SgNode*> called;
2513  while (jjf != paths.size()) {
2514  std::cout << "propagating" << std::endl;
2515  path = paths[jjf];
2516  int jj = 0;
2517  while (jj != path.size()) {
2518  if (isSgFunctionCallExp(path[jj]->get_SgNode()) && find(called.begin(), called.end(), path[jj]->get_SgNode()) == called.end()) {
2519  propagateFunctionCall(path, jj, jjf);
2520  called.push_back(path[jj]->get_SgNode());
2521  jjf = 0;
2522  // noadd = true;
2523  jj = 0;
2524  break;
2525  }
2526  else {
2527  jj++;
2528  }
2529  }
2530  if (noadd) {
2531  noadd = false;
2532  }
2533 
2534  else {
2535  jjf++;
2536  }
2537  }
2538 
2539  std::cout << "paths.size(): " << paths.size() << std::endl;
2540  //ROSE_ASSERT(false);
2541  pathnumber += paths.size();
2542  std::vector<SgNode*> ncalled;
2543 
2544 for (int q = 0; q < paths.size(); q++) {
2545  std::vector<SgGraphNode*> path = path[q];
2546  ROSE_ASSERT(mainDef != NULL);
2547  //if (mainDefDecl != NULL) {
2548 */
2549  //SgFunctionDefinition* mainDef = mainDefDecl->get_definition();
2550  visitorTraversal* vis = new visitorTraversal();
2551  StaticCFG::CFG* cfg = new StaticCFG::CFG(mainDef);
2552  vis->pathnumber = 0;
2553  stringstream ss;
2554  string fileName= Rose::StringUtility::stripPathFromFileName(mainDef->get_file_info()->get_filenameString());
2555  string dotFileName1=fileName+"."+ mainDef->get_declaration()->get_name() +".dot";
2556 
2557  SgIncidenceDirectedGraph* g = new SgIncidenceDirectedGraph();
2558  g = cfg->getGraph();
2559  myGraph* mg = new myGraph();
2560  mg = instantiateGraph(g, *cfg);
2561  vis->tltnodes = 0;
2562  //vis->pathnumber = 0;
2563  ipaths = 0;
2564  vis->orig = mg;
2565  //openorig = mg;
2566  vis->g = g;
2567  //openg = g;
2568  vis->cfg = cfg;
2569  //opencfg = cfg;
2570 
2571  vis->constructPathAnalyzer(mg, true);
2572  //if (ipaths > 0) {
2573  cout << "filename: " << fileName << std::endl;
2574  cout << "finished" << std::endl;
2575  cout << "paths: " << vis->pathnumber << " ipaths: " << ipaths << std::endl;
2576  //}
2577  // }
2578  // fout.close();
2579  return 0;
2580 }
2581 
2582 
2583 
2584 // int main(int argc, char *argv[]) {
2585 // pathnum = 0;
2586 // ipaths = 0;
2587 // SgProject* proj = frontend(argc,argv);
2588 // ROSE_ASSERT (proj != NULL);
2589 //
2590 // SgFunctionDeclaration* mainDefDecl = SageInterface::findMain(proj);
2591 //
2592 // SgFunctionDefinition* mainDef = mainDefDecl->get_definition();
2593 // visitorTraversal* vis = new visitorTraversal();
2594 // visitorTraversal* vis2 = new visitorTraversal();
2595 // nGraph = new newGraph();
2596 // //vis->nGraph = nGraph;
2597 // //newGraph* nnGraph = new newGraph();
2598 // StaticCFG::CFG* cfg1 = new StaticCFG::CFG(mainDef);
2599 // //cfg.buildFullCFG();
2600 // stringstream ss;
2601 // string fileName= StringUtility::stripPathFromFileName(mainDef->get_file_info()->get_filenameString());
2602 // string dotFileName1=fileName+"."+ mainDef->get_declaration()->get_name() +".dot";
2603 //
2604 // cfgToDot(mainDef,dotFileName1);
2605 // //cfg->buildFullCFG();
2606 // //SgIncidenceDirectedGraph* cf = new SgIncidenceDirectedGraph();
2607 // SgIncidenceDirectedGraph* cf = cfg1->getGraph();
2608 // myGraph* mg = new myGraph();
2609 // mg = instantiateGraph(cf, *cfg1);
2610 // vis2->tltnodes = 0;
2611 // vis2->paths = 0;
2612 // vis->tltnodes = 0;
2613 // vis->paths = 0;
2614 // //vis->firstPrepGraph(constcfg);
2615 // vis->g = cf;
2616 // vis2->g = cf;
2617 // vis2->orig = mg;
2618 // cfg = cfg1;
2619 // vis->orig = mg;
2620 // vis->constructPathAnalyzer(mg, true);
2621 // std::cout << "constructed" << std::endl;
2622 // std::cout << "ipaths: " << ipaths << std::endl;
2623 // // printHotness2(nGraph);
2624 // // std::cout << "mapped" << std::endl;i
2625 // std::vector<std::vector<int> > pts;
2626 // std::vector<int> ptsP;
2627 // //std::vector<SgExpressionStmt*> exprs = SageInterface::querySubTree<SgExpressionStmt>(proj);
2628 // for (int q1 = 0; q1 < exprs.size(); q1++) {
2629 // ptsP.clear();
2630 // for (int q2 = 0; q2 < exprs.size(); q2++) {
2631 // if (q1 != q2) {
2632 // vis->paths = 0;
2633 // vis->tltnodes = 0;
2634 // vis->constructPathAnalyzer(mg, exprs[q1], exprs[q2]);
2635 // std::cout << vis->paths << " between expr" << q1 << " and expr" << q2 << std::endl;
2636 // ptsP.push_back(vis->paths);
2637 // }
2638 // pts.push_back(ptsP);
2639 // }
2640 // }
2641 // for (int i = 0; i < pts.size(); i++) {
2642 // for (int j = 0; j < pts[i].size(); j++) {
2643 // std::cout << "between expr" << i << "and expr" << j << " there are " << pts[i][j] << std::endl;
2644 // }
2645 // }
2646 //
2647 // //cfg.clearNodesAndEdges();
2648 // //std::cout << "finished" << std::endl;
2649 // //std::cout << "tltnodes: " << vis->tltnodes << " paths: " << vis->paths << std::endl;
2650 // //delete vis;
2651 // //}
2652 
2653 
2654 /*
2655 std::vector<SgExprStatement*> exprList = SageInterface::querySubTree<SgExprStatement>(project);
2656 for (Rose_STL_Container<SgGraphNode*>::iterator i = exprList.begin(); i != exprList.end(); i++) {
2657 */
2658 
2659 // SgExprStatement* expr = isSgExprStatement(*i);
2660 
SgFunctionParameterList
This class represents the concept of a declaration list.
Definition: Cxx_Grammar.h:144012
VirtualCFG::CFGNode::getIndex
unsigned int getIndex() const
An identifying index within the AST node given by getNode()
Definition: virtualCFG.h:91
SgType
This class represents the base class for all types.
Definition: Cxx_Grammar.h:52473
VirtualCFG::CFGNode::inEdges
std::vector< CFGEdge > inEdges() const
Incoming control flow edges to this node.
SgInitializedName
This class represents the notion of a declared variable.
Definition: Cxx_Grammar.h:97176
SgFunctionDeclaration
This class represents the concept of a function declaration statement.
Definition: Cxx_Grammar.h:164666
std
STL namespace.
SgFunctionDefinition
This class represents the concept of a scope in C++ (e.g. global scope, fuction scope, etc.).
Definition: Cxx_Grammar.h:125592
SgGraphTraversal::constructPathAnalyzer
void constructPathAnalyzer(CFG *g, bool unbounded=false, Vertex end=0, Vertex begin=0, bool ns=true)
This is the function that is used by the user directly to start the algorithm.
Definition: graphProcessing.h:1119
SgFunctionDeclaration::get_orig_return_type
SgType * get_orig_return_type() const
Support for C++ covariant return types (used in virtual function overloading).
SgFunctionCallExp::getAssociatedFunctionDeclaration
SgFunctionDeclaration * getAssociatedFunctionDeclaration() const
Returns the associated function declaration, if it can be resolved statically.
SgFunctionParameterList::get_args
const SgInitializedNamePtrList & get_args() const
Access function for p_args.
SgName
This class represents strings within the IR nodes.
Definition: Cxx_Grammar.h:20553
SgVarRefExp::get_type
SgType * get_type() const override
Get the type associated with this expression.
SgInitializedName::get_qualified_name
SgName get_qualified_name() const
Returns the name with appropriate qualified names representing nested scopes.
SageInterface::findMain
ROSE_DLL_API SgFunctionDeclaration * findMain(SgNode *currentNode)
top-down traversal from current node to find the main() function declaration
SgNode
This class represents the base class for all IR nodes within Sage III.
Definition: Cxx_Grammar.h:9846
Rose::StringUtility::stripPathFromFileName
ROSE_UTIL_API std::string stripPathFromFileName(const std::string &fileNameWithPath)
Returns the last component of a path in a filesystem.
StaticCFG::CFG::toCFGNode
CFGNode toCFGNode(SgGraphNode *node)
Turn a graph node into a CFGNode which is defined in VirtualCFG namespace.
sg
This namespace contains template functions that operate on the ROSE AST.
Definition: sageFunctors.h:15
StaticCFG::CFG::getGraph
SgIncidenceDirectedGraph * getGraph() const
Get the pointer pointing to the graph used by static CFG.
Definition: staticCFG.h:66
graphProcessing.h
Brief Overview of Algorithm:
SgProject
This class represents a source project, with a list of SgFile objects and global information about th...
Definition: Cxx_Grammar.h:29782
SgLocatedNode::get_file_info
virtual Sg_File_Info * get_file_info() const override
Interface function to implement original SAGE interface to SgFile_Info objects.
VirtualCFG::CFGNode::toString
std::string toString() const
Pretty string for Dot node labels, etc.
Generated on Mon Oct 23 2023 02:35:03 for ROSE by   doxygen 1.8.10