2972b86ed0e0ab037ade76d9589eebba2f90b7cb
[c11tester.git] / funcnode.cc
1 #include "action.h"
2 #include "history.h"
3 #include "funcnode.h"
4 #include "funcinst.h"
5 #include "predicate.h"
6 #include "concretepredicate.h"
7
8 #include "model.h"
9
10 FuncNode::FuncNode(ModelHistory * history) :
11         history(history),
12         exit_count(0),
13         marker(1),
14         func_inst_map(),
15         inst_list(),
16         entry_insts(),
17         predicate_tree_position(),
18         edge_table(32),
19         out_edges()
20 {
21         predicate_tree_entry = new Predicate(NULL, true);
22         predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
23         predicate_tree_exit = new Predicate(NULL, false, true);
24
25         /* Snapshot data structures below */
26         action_list_buffer = new SnapList<action_list_t *>();
27         read_locations = new loc_set_t();
28         write_locations = new loc_set_t();
29         val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
30         loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
31
32         //values_may_read_from = new value_set_t();
33 }
34
35 /* Reallocate snapshotted memories when new executions start */
36 void FuncNode::set_new_exec_flag()
37 {
38         action_list_buffer = new SnapList<action_list_t *>();
39         read_locations = new loc_set_t();
40         write_locations = new loc_set_t();
41         val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
42         loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
43
44         //values_may_read_from = new value_set_t();
45 }
46
47 /* Check whether FuncInst with the same type, position, and location
48  * as act has been added to func_inst_map or not. If not, add it.
49  *
50  * Note: currently, actions with the same position are filtered out by process_action,
51  * so the collision list of FuncInst is not used. May remove it later. 
52  */
53 void FuncNode::add_inst(ModelAction *act)
54 {
55         ASSERT(act);
56         const char * position = act->get_position();
57
58         /* THREAD* actions, ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK
59          * actions are not tagged with their source line numbers
60          */
61         if (position == NULL)
62                 return;
63
64         if ( func_inst_map.contains(position) ) {
65                 FuncInst * inst = func_inst_map.get(position);
66
67                 /* TODO: The assertion fails when encountering volatile variables that use ++ or -- syntax, i.e. read and write have the same position */
68                 ASSERT(inst->get_type() == act->get_type());
69                 int curr_execution_number = model->get_execution_number();
70
71                 /* Reset locations when new executions start */
72                 if (inst->get_execution_number() != curr_execution_number) {
73                         inst->set_location(act->get_location());
74                         inst->set_execution_number(curr_execution_number);
75                 }
76
77                 if (inst->get_location() != act->get_location())
78                         inst->not_single_location();
79
80                 return;
81         }
82
83         FuncInst * func_inst = new FuncInst(act, this);
84
85         func_inst_map.put(position, func_inst);
86         inst_list.push_back(func_inst);
87 }
88
89 /* Get the FuncInst with the same type, position, and location
90  * as act
91  *
92  * @return FuncInst with the same type, position, and location as act */
93 FuncInst * FuncNode::get_inst(ModelAction *act)
94 {
95         ASSERT(act);
96         const char * position = act->get_position();
97
98         /* THREAD* actions, ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK
99          * actions are not tagged with their source line numbers
100          */
101         if (position == NULL)
102                 return NULL;
103
104         FuncInst * inst = func_inst_map.get(position);
105         if (inst == NULL)
106                 return NULL;
107
108         action_type inst_type = inst->get_type();
109         action_type act_type = act->get_type();
110
111         // else if branch: an RMWRCAS action is converted to a RMW or READ action
112         if (inst_type == act_type)
113                 return inst;
114         else if (inst_type == ATOMIC_RMWRCAS &&
115                         (act_type == ATOMIC_RMW || act_type == ATOMIC_READ))
116                 return inst;
117
118         return NULL;
119 }
120
121
122 void FuncNode::add_entry_inst(FuncInst * inst)
123 {
124         if (inst == NULL)
125                 return;
126
127         mllnode<FuncInst *> * it;
128         for (it = entry_insts.begin(); it != NULL; it = it->getNext()) {
129                 if (inst == it->getVal())
130                         return;
131         }
132
133         entry_insts.push_back(inst);
134 }
135
136 /**
137  * @brief Convert ModelAdtion list to FuncInst list 
138  * @param act_list A list of ModelActions
139  */
140 void FuncNode::update_tree(action_list_t * act_list)
141 {
142         if (act_list == NULL || act_list->size() == 0)
143                 return;
144
145         HashTable<void *, value_set_t *, uintptr_t, 0> * write_history = history->getWriteHistory();
146
147         /* build inst_list from act_list for later processing */
148         func_inst_list_t inst_list;
149         action_list_t rw_act_list;
150
151         for (sllnode<ModelAction *> * it = act_list->begin(); it != NULL; it = it->getNext()) {
152                 ModelAction * act = it->getVal();
153                 FuncInst * func_inst = get_inst(act);
154                 void * loc = act->get_location();
155
156                 if (func_inst == NULL)
157                         continue;
158
159                 inst_list.push_back(func_inst);
160                 bool act_added = false;
161
162                 if (act->is_write()) {
163                         rw_act_list.push_back(act);
164                         act_added = true;
165                         if (!write_locations->contains(loc)) {
166                                 write_locations->add(loc);
167                                 history->update_loc_wr_func_nodes_map(loc, this);
168                         }
169                 }
170
171                 if (act->is_read()) {
172                         if (!act_added)
173                                 rw_act_list.push_back(act);
174
175                         /* If func_inst may only read_from a single location, then:
176                          *
177                          * The first time an action reads from some location,
178                          * import all the values that have been written to this
179                          * location from ModelHistory and notify ModelHistory
180                          * that this FuncNode may read from this location.
181                          */
182                         if (!read_locations->contains(loc) && func_inst->is_single_location()) {
183                                 read_locations->add(loc);
184                                 value_set_t * write_values = write_history->get(loc);
185                                 add_to_val_loc_map(write_values, loc);
186                                 history->update_loc_rd_func_nodes_map(loc, this);
187                         }
188                 }
189         }
190
191 //      model_print("function %s\n", func_name);
192 //      print_val_loc_map();
193
194         update_inst_tree(&inst_list);
195         update_predicate_tree(&rw_act_list);
196
197 //      print_predicate_tree();
198 }
199
200 /** 
201  * @brief Link FuncInsts in inst_list  - add one FuncInst to another's predecessors and successors
202  * @param inst_list A list of FuncInsts
203  */
204 void FuncNode::update_inst_tree(func_inst_list_t * inst_list)
205 {
206         if (inst_list == NULL)
207                 return;
208         else if (inst_list->size() == 0)
209                 return;
210
211         /* start linking */
212         sllnode<FuncInst *>* it = inst_list->begin();
213         sllnode<FuncInst *>* prev;
214
215         /* add the first instruction to the list of entry insts */
216         FuncInst * entry_inst = it->getVal();
217         add_entry_inst(entry_inst);
218
219         it = it->getNext();
220         while (it != NULL) {
221                 prev = it->getPrev();
222
223                 FuncInst * prev_inst = prev->getVal();
224                 FuncInst * curr_inst = it->getVal();
225
226                 prev_inst->add_succ(curr_inst);
227                 curr_inst->add_pred(prev_inst);
228
229                 it = it->getNext();
230         }
231 }
232
233 void FuncNode::update_predicate_tree(action_list_t * act_list)
234 {
235         if (act_list == NULL || act_list->size() == 0)
236                 return;
237
238         incr_marker();
239
240         /* Map a FuncInst to the its predicate */
241         HashTable<FuncInst *, Predicate *, uintptr_t, 0> inst_pred_map(128);
242
243         // Number FuncInsts to detect loops
244         HashTable<FuncInst *, uint32_t, uintptr_t, 0> inst_id_map(128);
245         uint32_t inst_counter = 0;
246
247         /* Only need to store the locations of read actions */
248         HashTable<void *, ModelAction *, uintptr_t, 0> loc_act_map(128);
249
250         sllnode<ModelAction *> *it = act_list->begin();
251         Predicate * curr_pred = predicate_tree_entry;
252         while (it != NULL) {
253                 ModelAction * next_act = it->getVal();
254                 FuncInst * next_inst = get_inst(next_act);
255                 next_inst->set_associated_act(next_act, marker);
256
257                 SnapVector<Predicate *> unset_predicates = SnapVector<Predicate *>();
258                 bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &unset_predicates);
259
260                 // A branch with unset predicate expression is detected
261                 if (!branch_found && unset_predicates.size() != 0) {
262                         ASSERT(unset_predicates.size() == 1);
263                         Predicate * one_branch = unset_predicates[0];
264
265                         bool amended = amend_predicate_expr(&curr_pred, next_inst, next_act);
266                         if (amended)
267                                 continue;
268                         else {
269                                 curr_pred = one_branch;
270                                 branch_found = true;
271                         }
272                 }
273
274                 // Detect loops
275                 if (!branch_found && inst_id_map.contains(next_inst)) {
276                         FuncInst * curr_inst = curr_pred->get_func_inst();
277                         uint32_t curr_id = inst_id_map.get(curr_inst);
278                         uint32_t next_id = inst_id_map.get(next_inst);
279
280                         if (curr_id >= next_id) {
281                                 Predicate * old_pred = inst_pred_map.get(next_inst);
282                                 Predicate * back_pred = old_pred->get_parent();
283
284                                 curr_pred->add_backedge(back_pred);
285                                 curr_pred = back_pred;
286                                 continue;
287                         }
288                 }
289
290                 // Generate new branches
291                 if (!branch_found) {
292                         SnapVector<struct half_pred_expr *> half_pred_expressions;
293                         infer_predicates(next_inst, next_act, &loc_act_map, &half_pred_expressions);
294                         generate_predicates(&curr_pred, next_inst, &half_pred_expressions);
295                         continue;
296                 }
297
298                 if (next_act->is_write())
299                         curr_pred->set_write(true);
300
301                 if (next_act->is_read()) {
302                         loc_act_map.put(next_act->get_location(), next_act);
303                 }
304
305                 inst_pred_map.put(next_inst, curr_pred);
306                 if (!inst_id_map.contains(next_inst))
307                         inst_id_map.put(next_inst, inst_counter++);
308
309                 it = it->getNext();
310                 curr_pred->incr_expl_count();
311         }
312
313         curr_pred->set_exit(predicate_tree_exit);
314 }
315
316 /* Given curr_pred and next_inst, find the branch following curr_pred that
317  * contains next_inst and the correct predicate. 
318  * @return true if branch found, false otherwise.
319  */
320 bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst,
321         ModelAction * next_act, SnapVector<Predicate *> * unset_predicates)
322 {
323         /* Check if a branch with func_inst and corresponding predicate exists */
324         bool branch_found = false;
325         ModelVector<Predicate *> * branches = (*curr_pred)->get_children();
326         for (uint i = 0; i < branches->size(); i++) {
327                 Predicate * branch = (*branches)[i];
328                 if (branch->get_func_inst() != next_inst)
329                         continue;
330
331                 /* Check against predicate expressions */
332                 bool predicate_correct = true;
333                 PredExprSet * pred_expressions = branch->get_pred_expressions();
334                 PredExprSetIter * pred_expr_it = pred_expressions->iterator();
335
336                 /* Only read and rmw actions my have unset predicate expressions */
337                 if (pred_expressions->getSize() == 0) {
338                         predicate_correct = false;
339                         unset_predicates->push_back(branch);
340                 }
341
342                 while (pred_expr_it->hasNext()) {
343                         pred_expr * pred_expression = pred_expr_it->next();
344                         uint64_t last_read, next_read;
345                         bool equality;
346
347                         switch(pred_expression->token) {
348                                 case NOPREDICATE:
349                                         predicate_correct = true;
350                                         break;
351                                 case EQUALITY:
352                                         FuncInst * to_be_compared;
353                                         ModelAction * last_act;
354
355                                         to_be_compared = pred_expression->func_inst;
356                                         last_act = to_be_compared->get_associated_act(marker);
357
358                                         last_read = last_act->get_reads_from_value();
359                                         next_read = next_act->get_reads_from_value();
360                                         equality = (last_read == next_read);
361                                         if (equality != pred_expression->value)
362                                                 predicate_correct = false;
363
364                                         break;
365                                 case NULLITY:
366                                         next_read = next_act->get_reads_from_value();
367                                         equality = ((void*)next_read == NULL);
368                                         if (equality != pred_expression->value)
369                                                 predicate_correct = false;
370                                         break;
371                                 default:
372                                         predicate_correct = false;
373                                         model_print("unkown predicate token\n");
374                                         break;
375                         }
376                 }
377
378                 if (predicate_correct) {
379                         *curr_pred = branch;
380                         branch_found = true;
381                         break;
382                 }
383         }
384
385         return branch_found;
386 }
387
388 /* Infer predicate expressions, which are generated in FuncNode::generate_predicates */
389 void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
390         HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map,
391         SnapVector<struct half_pred_expr *> * half_pred_expressions)
392 {
393         void * loc = next_act->get_location();
394
395         if (next_inst->is_read()) {
396                 /* read + rmw */
397                 if ( loc_act_map->contains(loc) ) {
398                         ModelAction * last_act = loc_act_map->get(loc);
399                         FuncInst * last_inst = get_inst(last_act);
400                         struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst);
401                         half_pred_expressions->push_back(expression);
402                 } else if ( next_inst->is_single_location() ){
403                         loc_set_t * loc_may_equal = loc_may_equal_map->get(loc);
404
405                         if (loc_may_equal != NULL) {
406                                 loc_set_iter * loc_it = loc_may_equal->iterator();
407                                 while (loc_it->hasNext()) {
408                                         void * neighbor = loc_it->next();
409                                         if (loc_act_map->contains(neighbor)) {
410                                                 ModelAction * last_act = loc_act_map->get(neighbor);
411                                                 FuncInst * last_inst = get_inst(last_act);
412
413                                                 struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst);
414                                                 half_pred_expressions->push_back(expression);
415                                         }
416                                 }
417                         }
418                 } else {
419                         // next_inst is not single location
420                         uint64_t read_val = next_act->get_reads_from_value();
421
422                         // only infer NULLITY predicate when it is actually NULL.
423                         if ( (void*)read_val == NULL) {
424                                 struct half_pred_expr * expression = new half_pred_expr(NULLITY, NULL);
425                                 half_pred_expressions->push_back(expression);
426                         }
427                 }
428         } else {
429                 /* Pure writes */
430                 // TODO: do anything here?
431         }
432 }
433
434 /* Able to generate complex predicates when there are multiple predciate expressions */
435 void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst,
436         SnapVector<struct half_pred_expr *> * half_pred_expressions)
437 {
438         if (half_pred_expressions->size() == 0) {
439                 Predicate * new_pred = new Predicate(next_inst);
440                 (*curr_pred)->add_child(new_pred);
441                 new_pred->set_parent(*curr_pred);
442
443                 /* entry predicates and predicates containing pure write actions
444                  * have no predicate expressions */
445                 if ( (*curr_pred)->is_entry_predicate() )
446                         new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
447                 else if (next_inst->is_write()) {
448                         /* next_inst->is_write() <==> pure writes */
449                         new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
450                 }
451
452                 return;
453         }
454
455         SnapVector<Predicate *> predicates;
456
457         struct half_pred_expr * half_expr = (*half_pred_expressions)[0];
458         predicates.push_back(new Predicate(next_inst));
459         predicates.push_back(new Predicate(next_inst));
460
461         predicates[0]->add_predicate_expr(half_expr->token, half_expr->func_inst, true);
462         predicates[1]->add_predicate_expr(half_expr->token, half_expr->func_inst, false);
463
464         for (uint i = 1; i < half_pred_expressions->size(); i++) {
465                 half_expr = (*half_pred_expressions)[i];
466
467                 uint old_size = predicates.size();
468                 for (uint j = 0; j < old_size; j++) {
469                         Predicate * pred = predicates[j];
470                         Predicate * new_pred = new Predicate(next_inst);
471                         new_pred->copy_predicate_expr(pred);
472
473                         pred->add_predicate_expr(half_expr->token, half_expr->func_inst, true);
474                         new_pred->add_predicate_expr(half_expr->token, half_expr->func_inst, false);
475
476                         predicates.push_back(new_pred);
477                 }
478         }
479
480         for (uint i = 0; i < predicates.size(); i++) {
481                 Predicate * pred= predicates[i];
482                 (*curr_pred)->add_child(pred);
483                 pred->set_parent(*curr_pred);
484         }
485
486         /* Free memories allocated by infer_predicate */
487         for (uint i = 0; i < half_pred_expressions->size(); i++) {
488                 struct half_pred_expr * tmp = (*half_pred_expressions)[i];
489                 snapshot_free(tmp);
490         }
491 }
492
493 /* Amend predicates that contain no predicate expressions. Currenlty only amend with NULLITY predicates */
494 bool FuncNode::amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act)
495 {
496         // there should only be only child
497         Predicate * unset_pred = (*curr_pred)->get_children()->back();
498         uint64_t read_val = next_act->get_reads_from_value();
499
500         // only generate NULLITY predicate when it is actually NULL.
501         if ( !next_inst->is_single_location() && (void*)read_val == NULL ) {
502                 Predicate * new_pred = new Predicate(next_inst);
503
504                 (*curr_pred)->add_child(new_pred);
505                 new_pred->set_parent(*curr_pred);
506
507                 unset_pred->add_predicate_expr(NULLITY, NULL, false);
508                 new_pred->add_predicate_expr(NULLITY, NULL, true);
509
510                 return true;
511         }
512
513         return false;
514 }
515
516 void FuncNode::add_to_val_loc_map(uint64_t val, void * loc)
517 {
518         loc_set_t * locations = val_loc_map->get(val);
519
520         if (locations == NULL) {
521                 locations = new loc_set_t();
522                 val_loc_map->put(val, locations);
523         }
524
525         update_loc_may_equal_map(loc, locations);
526         locations->add(loc);
527         // values_may_read_from->add(val);
528 }
529
530 void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc)
531 {
532         if (values == NULL)
533                 return;
534
535         value_set_iter * it = values->iterator();
536         while (it->hasNext()) {
537                 uint64_t val = it->next();
538                 add_to_val_loc_map(val, loc);
539         }
540 }
541
542 void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations)
543 {
544         if ( old_locations->contains(new_loc) )
545                 return;
546
547         loc_set_t * neighbors = loc_may_equal_map->get(new_loc);
548
549         if (neighbors == NULL) {
550                 neighbors = new loc_set_t();
551                 loc_may_equal_map->put(new_loc, neighbors);
552         }
553
554         loc_set_iter * loc_it = old_locations->iterator();
555         while (loc_it->hasNext()) {
556                 // new_loc: { old_locations, ... }
557                 void * member = loc_it->next();
558                 neighbors->add(member);
559
560                 // for each i in old_locations, i : { new_loc, ... }
561                 loc_set_t * _neighbors = loc_may_equal_map->get(member);
562                 if (_neighbors == NULL) {
563                         _neighbors = new loc_set_t();
564                         loc_may_equal_map->put(member, _neighbors);
565                 }
566                 _neighbors->add(new_loc);
567         }
568 }
569
570 /* Every time a thread enters a function, set its position to the predicate tree entry */
571 void FuncNode::init_predicate_tree_position(thread_id_t tid)
572 {
573         int thread_id = id_to_int(tid);
574         if (predicate_tree_position.size() <= (uint) thread_id)
575                 predicate_tree_position.resize(thread_id + 1);
576
577         predicate_tree_position[thread_id] = predicate_tree_entry;
578 }
579
580 void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred)
581 {
582         int thread_id = id_to_int(tid);
583         predicate_tree_position[thread_id] = pred;
584 }
585
586 /* @return The position of a thread in a predicate tree */
587 Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid)
588 {
589         int thread_id = id_to_int(tid);
590         return predicate_tree_position[thread_id];
591 }
592
593 /* Make sure elements of thrd_inst_act_map are initialized properly when threads enter functions */
594 void FuncNode::init_inst_act_map(thread_id_t tid)
595 {
596         int thread_id = id_to_int(tid);
597         SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
598         uint old_size = thrd_inst_act_map->size();
599
600         if (thrd_inst_act_map->size() <= (uint) thread_id) {
601                 uint new_size = thread_id + 1;
602                 thrd_inst_act_map->resize(new_size);
603
604                 for (uint i = old_size; i < new_size; i++)
605                         (*thrd_inst_act_map)[i] = new inst_act_map_t(128);
606         }
607 }
608
609 /* Reset elements of thrd_inst_act_map when threads exit functions */
610 void FuncNode::reset_inst_act_map(thread_id_t tid)
611 {
612         int thread_id = id_to_int(tid);
613         SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
614
615         inst_act_map_t * map = (*thrd_inst_act_map)[thread_id];
616         map->reset();
617 }
618
619 void FuncNode::update_inst_act_map(thread_id_t tid, ModelAction * read_act)
620 {
621         int thread_id = id_to_int(tid);
622         SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
623
624         inst_act_map_t * map = (*thrd_inst_act_map)[thread_id];
625         FuncInst * read_inst = get_inst(read_act);
626         map->put(read_inst, read_act);
627 }
628
629 inst_act_map_t * FuncNode::get_inst_act_map(thread_id_t tid)
630 {
631         int thread_id = id_to_int(tid);
632         SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
633
634         return (*thrd_inst_act_map)[thread_id];
635 }
636
637 /* Add FuncNodes that this node may follow */
638 void FuncNode::add_out_edge(FuncNode * other)
639 {
640         if ( !edge_table.contains(other) ) {
641                 edge_table.put(other, OUT_EDGE);
642                 out_edges.push_back(other);
643                 return;
644         }
645
646         edge_type_t edge = edge_table.get(other);
647         if (edge == IN_EDGE) {
648                 edge_table.put(other, BI_EDGE);
649                 out_edges.push_back(other);
650         }
651 }
652
653 /* Compute the distance between this FuncNode and the target node.
654  * Return -1 if the target node is unreachable or the actual distance
655  * is greater than max_step.
656  */
657 int FuncNode::compute_distance(FuncNode * target, int max_step)
658 {
659         if (target == NULL)
660                 return -1;
661         else if (target == this)
662                 return 0;
663
664         SnapList<FuncNode *> queue;
665         HashTable<FuncNode *, int, uintptr_t, 0> distances(128);
666
667         queue.push_back(this);
668         distances.put(this, 0);
669
670         while (!queue.empty()) {
671                 FuncNode * curr = queue.front();
672                 queue.pop_front();
673                 int dist = distances.get(curr);
674
675                 if (max_step <= dist)
676                         return -1;
677
678                 ModelList<FuncNode *> * outEdges = curr->get_out_edges();
679                 mllnode<FuncNode *> * it;
680                 for (it = outEdges->begin(); it != NULL; it = it->getNext()) {
681                         FuncNode * out_node = it->getVal();
682
683                         /* This node has not been visited before */
684                         if ( !distances.contains(out_node) ) {
685                                 if (out_node == target)
686                                         return dist + 1;
687
688                                 queue.push_back(out_node);
689                                 distances.put(out_node, dist + 1);
690                         }
691                 }
692         }
693
694         /* Target node is unreachable */
695         return -1;
696 }
697
698 void FuncNode::print_predicate_tree()
699 {
700         model_print("digraph function_%s {\n", func_name);
701         predicate_tree_entry->print_pred_subtree();
702         predicate_tree_exit->print_predicate();
703         model_print("}\n");     // end of graph
704 }
705
706 void FuncNode::print_val_loc_map()
707 {
708 /*
709         value_set_iter * val_it = values_may_read_from->iterator();
710         while (val_it->hasNext()) {
711                 uint64_t value = val_it->next();
712                 model_print("val %llx: ", value);
713
714                 loc_set_t * locations = val_loc_map->get(value);
715                 loc_set_iter * loc_it = locations->iterator();
716                 while (loc_it->hasNext()) {
717                         void * location = loc_it->next();
718                         model_print("%p ", location);
719                 }
720                 model_print("\n");
721         }
722 */
723 }