Remove the code that checks store visibility, not being used at this time
[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 #include <cmath>
10
11 FuncNode::FuncNode(ModelHistory * history) :
12         history(history),
13         exit_count(0),
14         marker(1),
15         func_inst_map(),
16         inst_list(),
17         entry_insts(),
18         inst_pred_map(128),
19         inst_id_map(128),
20         loc_act_map(128),
21         predicate_tree_position(),
22         predicate_leaves(),
23         leaves_tmp_storage(),
24         weight_debug_vec(),
25         edge_table(32),
26         out_edges()
27 {
28         predicate_tree_entry = new Predicate(NULL, true);
29         predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
30
31         predicate_tree_exit = new Predicate(NULL, false, true);
32         predicate_tree_exit->set_depth(MAX_DEPTH);
33
34         /* Snapshot data structures below */
35         action_list_buffer = new SnapList<action_list_t *>();
36         read_locations = new loc_set_t();
37         write_locations = new loc_set_t();
38         val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
39         loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
40
41         //values_may_read_from = new value_set_t();
42 }
43
44 /* Reallocate snapshotted memories when new executions start */
45 void FuncNode::set_new_exec_flag()
46 {
47         action_list_buffer = new SnapList<action_list_t *>();
48         read_locations = new loc_set_t();
49         write_locations = new loc_set_t();
50         val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
51         loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
52
53         //values_may_read_from = new value_set_t();
54 }
55
56 /* Check whether FuncInst with the same type, position, and location
57  * as act has been added to func_inst_map or not. If not, add it.
58  */
59 void FuncNode::add_inst(ModelAction *act)
60 {
61         ASSERT(act);
62         const char * position = act->get_position();
63
64         /* THREAD* actions, ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK
65          * actions are not tagged with their source line numbers
66          */
67         if (position == NULL)
68                 return;
69
70         FuncInst * func_inst = func_inst_map.get(position);
71
72         /* This position has not been inserted into hashtable before */
73         if (func_inst == NULL) {
74                 func_inst = create_new_inst(act);
75                 func_inst_map.put(position, func_inst);
76                 return;
77         }
78
79         /* Volatile variables that use ++ or -- syntax may result in read and write actions with the same position */
80         if (func_inst->get_type() != act->get_type()) {
81                 FuncInst * collision_inst = func_inst->search_in_collision(act);
82
83                 if (collision_inst == NULL) {
84                         collision_inst = create_new_inst(act);
85                         func_inst->add_to_collision(collision_inst);
86                         return;
87                 } else {
88                         func_inst = collision_inst;
89                 }
90         }
91
92         ASSERT(func_inst->get_type() == act->get_type());
93         int curr_execution_number = model->get_execution_number();
94
95         /* Reset locations when new executions start */
96         if (func_inst->get_execution_number() != curr_execution_number) {
97                 func_inst->set_location(act->get_location());
98                 func_inst->set_execution_number(curr_execution_number);
99         }
100
101         /* Mark the memory location of such inst as not unique */
102         if (func_inst->get_location() != act->get_location())
103                 func_inst->not_single_location();
104 }
105
106 FuncInst * FuncNode::create_new_inst(ModelAction * act)
107 {
108         FuncInst * func_inst = new FuncInst(act, this);
109         int exec_num = model->get_execution_number();
110         func_inst->set_execution_number(exec_num);
111
112         inst_list.push_back(func_inst);
113
114         return func_inst;
115 }
116
117
118 /* Get the FuncInst with the same type, position, and location
119  * as act
120  *
121  * @return FuncInst with the same type, position, and location as act */
122 FuncInst * FuncNode::get_inst(ModelAction *act)
123 {
124         ASSERT(act);
125         const char * position = act->get_position();
126
127         /* THREAD* actions, ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK
128          * actions are not tagged with their source line numbers
129          */
130         if (position == NULL)
131                 return NULL;
132
133         FuncInst * inst = func_inst_map.get(position);
134         if (inst == NULL)
135                 return NULL;
136
137         action_type inst_type = inst->get_type();
138         action_type act_type = act->get_type();
139
140         if (inst_type == act_type) {
141                 return inst;
142         }
143         /* RMWRCAS actions are converted to RMW or READ actions */
144         else if (inst_type == ATOMIC_RMWRCAS &&
145                                          (act_type == ATOMIC_RMW || act_type == ATOMIC_READ)) {
146                 return inst;
147         }
148         /* Return the FuncInst in the collision list */
149         else {
150                 return inst->search_in_collision(act);
151         }
152 }
153
154
155 void FuncNode::add_entry_inst(FuncInst * inst)
156 {
157         if (inst == NULL)
158                 return;
159
160         mllnode<FuncInst *> * it;
161         for (it = entry_insts.begin();it != NULL;it = it->getNext()) {
162                 if (inst == it->getVal())
163                         return;
164         }
165
166         entry_insts.push_back(inst);
167 }
168
169 /**
170  * @brief Convert ModelAdtion list to FuncInst list
171  * @param act_list A list of ModelActions
172  */
173 void FuncNode::update_tree(action_list_t * act_list)
174 {
175         if (act_list == NULL || act_list->size() == 0)
176                 return;
177
178         HashTable<void *, value_set_t *, uintptr_t, 0> * write_history = history->getWriteHistory();
179
180         /* build inst_list from act_list for later processing */
181         func_inst_list_t inst_list;
182         action_list_t rw_act_list;
183
184         for (sllnode<ModelAction *> * it = act_list->begin();it != NULL;it = it->getNext()) {
185                 ModelAction * act = it->getVal();
186                 FuncInst * func_inst = get_inst(act);
187                 void * loc = act->get_location();
188
189                 if (func_inst == NULL)
190                         continue;
191
192                 inst_list.push_back(func_inst);
193                 bool act_added = false;
194
195                 if (act->is_write()) {
196                         rw_act_list.push_back(act);
197                         act_added = true;
198                         if (!write_locations->contains(loc)) {
199                                 write_locations->add(loc);
200                                 history->update_loc_wr_func_nodes_map(loc, this);
201                         }
202                 }
203
204                 if (act->is_read()) {
205                         if (!act_added)
206                                 rw_act_list.push_back(act);
207
208                         /* If func_inst may only read_from a single location, then:
209                          *
210                          * The first time an action reads from some location,
211                          * import all the values that have been written to this
212                          * location from ModelHistory and notify ModelHistory
213                          * that this FuncNode may read from this location.
214                          */
215                         if (!read_locations->contains(loc) && func_inst->is_single_location()) {
216                                 read_locations->add(loc);
217                                 value_set_t * write_values = write_history->get(loc);
218                                 add_to_val_loc_map(write_values, loc);
219                                 history->update_loc_rd_func_nodes_map(loc, this);
220                         }
221                 }
222         }
223
224 //      model_print("function %s\n", func_name);
225 //      print_val_loc_map();
226
227         update_inst_tree(&inst_list);
228         update_predicate_tree(&rw_act_list);
229
230 //      print_predicate_tree();
231 }
232
233 /**
234  * @brief Link FuncInsts in inst_list  - add one FuncInst to another's predecessors and successors
235  * @param inst_list A list of FuncInsts
236  */
237 void FuncNode::update_inst_tree(func_inst_list_t * inst_list)
238 {
239         if (inst_list == NULL)
240                 return;
241         else if (inst_list->size() == 0)
242                 return;
243
244         /* start linking */
245         sllnode<FuncInst *>* it = inst_list->begin();
246         sllnode<FuncInst *>* prev;
247
248         /* add the first instruction to the list of entry insts */
249         FuncInst * entry_inst = it->getVal();
250         add_entry_inst(entry_inst);
251
252         it = it->getNext();
253         while (it != NULL) {
254                 prev = it->getPrev();
255
256                 FuncInst * prev_inst = prev->getVal();
257                 FuncInst * curr_inst = it->getVal();
258
259                 prev_inst->add_succ(curr_inst);
260                 curr_inst->add_pred(prev_inst);
261
262                 it = it->getNext();
263         }
264 }
265
266 void FuncNode::update_predicate_tree(action_list_t * act_list)
267 {
268         if (act_list == NULL || act_list->size() == 0)
269                 return;
270
271         incr_marker();
272         uint32_t inst_counter = 0;
273
274         // Clear hashtables
275         loc_act_map.reset();
276         inst_pred_map.reset();
277         inst_id_map.reset();
278
279         // Clear the set of leaves encountered in this path
280         leaves_tmp_storage.clear();
281
282         sllnode<ModelAction *> *it = act_list->begin();
283         Predicate * curr_pred = predicate_tree_entry;
284         while (it != NULL) {
285                 ModelAction * next_act = it->getVal();
286                 FuncInst * next_inst = get_inst(next_act);
287                 next_inst->set_associated_act(next_act, marker);
288
289                 Predicate * unset_predicate = NULL;
290                 bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &unset_predicate);
291
292                 // A branch with unset predicate expression is detected
293                 if (!branch_found && unset_predicate != NULL) {
294                         bool amended = amend_predicate_expr(curr_pred, next_inst, next_act);
295                         if (amended)
296                                 continue;
297                         else {
298                                 curr_pred = unset_predicate;
299                                 branch_found = true;
300                         }
301                 }
302
303                 // Detect loops
304                 if (!branch_found && inst_id_map.contains(next_inst)) {
305                         FuncInst * curr_inst = curr_pred->get_func_inst();
306                         uint32_t curr_id = inst_id_map.get(curr_inst);
307                         uint32_t next_id = inst_id_map.get(next_inst);
308
309                         if (curr_id >= next_id) {
310                                 Predicate * old_pred = inst_pred_map.get(next_inst);
311                                 Predicate * back_pred = old_pred->get_parent();
312
313                                 // For updating weights
314                                 leaves_tmp_storage.push_back(curr_pred);
315
316                                 // Add to the set of backedges
317                                 curr_pred->add_backedge(back_pred);
318                                 curr_pred = back_pred;
319                                 continue;
320                         }
321                 }
322
323                 // Generate new branches
324                 if (!branch_found) {
325                         SnapVector<struct half_pred_expr *> half_pred_expressions;
326                         infer_predicates(next_inst, next_act, &half_pred_expressions);
327                         generate_predicates(curr_pred, next_inst, &half_pred_expressions);
328                         continue;
329                 }
330
331                 if (next_act->is_write())
332                         curr_pred->set_write(true);
333
334                 if (next_act->is_read()) {
335                         /* Only need to store the locations of read actions */
336                         loc_act_map.put(next_act->get_location(), next_act);
337                 }
338
339                 inst_pred_map.put(next_inst, curr_pred);
340                 if (!inst_id_map.contains(next_inst))
341                         inst_id_map.put(next_inst, inst_counter++);
342
343                 it = it->getNext();
344                 curr_pred->incr_expl_count();
345         }
346
347         if (curr_pred->get_exit() == NULL) {
348                 // Exit predicate is unset yet
349                 curr_pred->set_exit(predicate_tree_exit);
350         }
351
352         leaves_tmp_storage.push_back(curr_pred);
353         update_predicate_tree_weight();
354 }
355
356 /* Given curr_pred and next_inst, find the branch following curr_pred that
357  * contains next_inst and the correct predicate.
358  * @return true if branch found, false otherwise.
359  */
360 bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst,
361 ModelAction * next_act, Predicate ** unset_predicate)
362 {
363         /* Check if a branch with func_inst and corresponding predicate exists */
364         bool branch_found = false;
365         ModelVector<Predicate *> * branches = (*curr_pred)->get_children();
366         for (uint i = 0;i < branches->size();i++) {
367                 Predicate * branch = (*branches)[i];
368                 if (branch->get_func_inst() != next_inst)
369                         continue;
370
371                 /* Check against predicate expressions */
372                 bool predicate_correct = true;
373                 PredExprSet * pred_expressions = branch->get_pred_expressions();
374
375                 /* Only read and rmw actions my have unset predicate expressions */
376                 if (pred_expressions->getSize() == 0) {
377                         predicate_correct = false;
378                         if (*unset_predicate == NULL)
379                                 *unset_predicate = branch;
380                         else
381                                 ASSERT(false);
382
383                         continue;
384                 }
385
386                 PredExprSetIter * pred_expr_it = pred_expressions->iterator();
387                 while (pred_expr_it->hasNext()) {
388                         pred_expr * pred_expression = pred_expr_it->next();
389                         uint64_t last_read, next_read;
390                         bool equality;
391
392                         switch(pred_expression->token) {
393                                 case NOPREDICATE:
394                                         predicate_correct = true;
395                                         break;
396                                 case EQUALITY:
397                                         FuncInst * to_be_compared;
398                                         ModelAction * last_act;
399
400                                         to_be_compared = pred_expression->func_inst;
401                                         last_act = to_be_compared->get_associated_act(marker);
402
403                                         last_read = last_act->get_reads_from_value();
404                                         next_read = next_act->get_reads_from_value();
405                                         equality = (last_read == next_read);
406                                         if (equality != pred_expression->value)
407                                                 predicate_correct = false;
408
409                                         break;
410                                 case NULLITY:
411                                         next_read = next_act->get_reads_from_value();
412                                         // TODO: implement likely to be null
413                                         equality = ( (void*) (next_read & 0xffffffff) == NULL);
414                                         if (equality != pred_expression->value)
415                                                 predicate_correct = false;
416                                         break;
417                                 default:
418                                         predicate_correct = false;
419                                         model_print("unkown predicate token\n");
420                                         break;
421                         }
422                 }
423
424                 delete pred_expr_it;
425
426                 if (predicate_correct) {
427                         *curr_pred = branch;
428                         branch_found = true;
429                         break;
430                 }
431         }
432
433         return branch_found;
434 }
435
436 /* Infer predicate expressions, which are generated in FuncNode::generate_predicates */
437 void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
438 SnapVector<struct half_pred_expr *> * half_pred_expressions)
439 {
440         void * loc = next_act->get_location();
441
442         if (next_inst->is_read()) {
443                 /* read + rmw */
444                 if ( loc_act_map.contains(loc) ) {
445                         ModelAction * last_act = loc_act_map.get(loc);
446                         FuncInst * last_inst = get_inst(last_act);
447                         struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst);
448                         half_pred_expressions->push_back(expression);
449                 } else if ( next_inst->is_single_location() ) {
450                         loc_set_t * loc_may_equal = loc_may_equal_map->get(loc);
451
452                         if (loc_may_equal != NULL) {
453                                 loc_set_iter * loc_it = loc_may_equal->iterator();
454                                 while (loc_it->hasNext()) {
455                                         void * neighbor = loc_it->next();
456                                         if (loc_act_map.contains(neighbor)) {
457                                                 ModelAction * last_act = loc_act_map.get(neighbor);
458                                                 FuncInst * last_inst = get_inst(last_act);
459
460                                                 struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst);
461                                                 half_pred_expressions->push_back(expression);
462                                         }
463                                 }
464
465                                 delete loc_it;
466                         }
467                 } else {
468                         // next_inst is not single location
469                         uint64_t read_val = next_act->get_reads_from_value();
470
471                         // only infer NULLITY predicate when it is actually NULL.
472                         if ( (void*)read_val == NULL) {
473                                 struct half_pred_expr * expression = new half_pred_expr(NULLITY, NULL);
474                                 half_pred_expressions->push_back(expression);
475                         }
476                 }
477         } else {
478                 /* Pure writes */
479                 // TODO: do anything here?
480         }
481 }
482
483 /* Able to generate complex predicates when there are multiple predciate expressions */
484 void FuncNode::generate_predicates(Predicate * curr_pred, FuncInst * next_inst,
485 SnapVector<struct half_pred_expr *> * half_pred_expressions)
486 {
487         if (half_pred_expressions->size() == 0) {
488                 Predicate * new_pred = new Predicate(next_inst);
489                 curr_pred->add_child(new_pred);
490                 new_pred->set_parent(curr_pred);
491
492                 /* Maintain predicate leaves */
493                 predicate_leaves.add(new_pred);
494                 predicate_leaves.remove(curr_pred);
495
496                 /* entry predicates and predicates containing pure write actions
497                  * have no predicate expressions */
498                 if ( curr_pred->is_entry_predicate() )
499                         new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
500                 else if (next_inst->is_write()) {
501                         /* next_inst->is_write() <==> pure writes */
502                         new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
503                 }
504
505                 return;
506         }
507
508         SnapVector<Predicate *> predicates;
509
510         struct half_pred_expr * half_expr = (*half_pred_expressions)[0];
511         predicates.push_back(new Predicate(next_inst));
512         predicates.push_back(new Predicate(next_inst));
513
514         predicates[0]->add_predicate_expr(half_expr->token, half_expr->func_inst, true);
515         predicates[1]->add_predicate_expr(half_expr->token, half_expr->func_inst, false);
516
517         for (uint i = 1;i < half_pred_expressions->size();i++) {
518                 half_expr = (*half_pred_expressions)[i];
519
520                 uint old_size = predicates.size();
521                 for (uint j = 0;j < old_size;j++) {
522                         Predicate * pred = predicates[j];
523                         Predicate * new_pred = new Predicate(next_inst);
524                         new_pred->copy_predicate_expr(pred);
525
526                         pred->add_predicate_expr(half_expr->token, half_expr->func_inst, true);
527                         new_pred->add_predicate_expr(half_expr->token, half_expr->func_inst, false);
528
529                         predicates.push_back(new_pred);
530                 }
531         }
532
533         for (uint i = 0;i < predicates.size();i++) {
534                 Predicate * pred= predicates[i];
535                 curr_pred->add_child(pred);
536                 pred->set_parent(curr_pred);
537
538                 /* Add new predicate leaves */
539                 predicate_leaves.add(pred);
540         }
541
542         /* Remove predicate node that has children */
543         predicate_leaves.remove(curr_pred);
544
545         /* Free memories allocated by infer_predicate */
546         for (uint i = 0;i < half_pred_expressions->size();i++) {
547                 struct half_pred_expr * tmp = (*half_pred_expressions)[i];
548                 snapshot_free(tmp);
549         }
550 }
551
552 /* Amend predicates that contain no predicate expressions. Currenlty only amend with NULLITY predicates */
553 bool FuncNode::amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act)
554 {
555         ModelVector<Predicate *> * children = curr_pred->get_children();
556         ASSERT(children->size() == 1);
557
558         // there should only be only child
559         Predicate * unset_pred = (*children)[0];
560         uint64_t read_val = next_act->get_reads_from_value();
561
562         // only generate NULLITY predicate when it is actually NULL.
563         if ( !next_inst->is_single_location() && (void*)read_val == NULL ) {
564                 Predicate * new_pred = new Predicate(next_inst);
565
566                 curr_pred->add_child(new_pred);
567                 new_pred->set_parent(curr_pred);
568
569                 unset_pred->add_predicate_expr(NULLITY, NULL, false);
570                 new_pred->add_predicate_expr(NULLITY, NULL, true);
571
572                 return true;
573         }
574
575         return false;
576 }
577
578 void FuncNode::add_to_val_loc_map(uint64_t val, void * loc)
579 {
580         loc_set_t * locations = val_loc_map->get(val);
581
582         if (locations == NULL) {
583                 locations = new loc_set_t();
584                 val_loc_map->put(val, locations);
585         }
586
587         update_loc_may_equal_map(loc, locations);
588         locations->add(loc);
589         // values_may_read_from->add(val);
590 }
591
592 void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc)
593 {
594         if (values == NULL)
595                 return;
596
597         value_set_iter * it = values->iterator();
598         while (it->hasNext()) {
599                 uint64_t val = it->next();
600                 add_to_val_loc_map(val, loc);
601         }
602
603         delete it;
604 }
605
606 void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations)
607 {
608         if ( old_locations->contains(new_loc) )
609                 return;
610
611         loc_set_t * neighbors = loc_may_equal_map->get(new_loc);
612
613         if (neighbors == NULL) {
614                 neighbors = new loc_set_t();
615                 loc_may_equal_map->put(new_loc, neighbors);
616         }
617
618         loc_set_iter * loc_it = old_locations->iterator();
619         while (loc_it->hasNext()) {
620                 // new_loc: { old_locations, ... }
621                 void * member = loc_it->next();
622                 neighbors->add(member);
623
624                 // for each i in old_locations, i : { new_loc, ... }
625                 loc_set_t * _neighbors = loc_may_equal_map->get(member);
626                 if (_neighbors == NULL) {
627                         _neighbors = new loc_set_t();
628                         loc_may_equal_map->put(member, _neighbors);
629                 }
630                 _neighbors->add(new_loc);
631         }
632
633         delete loc_it;
634 }
635
636 /* Every time a thread enters a function, set its position to the predicate tree entry */
637 void FuncNode::init_predicate_tree_position(thread_id_t tid)
638 {
639         int thread_id = id_to_int(tid);
640         if (predicate_tree_position.size() <= (uint) thread_id)
641                 predicate_tree_position.resize(thread_id + 1);
642
643         predicate_tree_position[thread_id] = predicate_tree_entry;
644 }
645
646 void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred)
647 {
648         int thread_id = id_to_int(tid);
649         predicate_tree_position[thread_id] = pred;
650 }
651
652 /* @return The position of a thread in a predicate tree */
653 Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid)
654 {
655         int thread_id = id_to_int(tid);
656         return predicate_tree_position[thread_id];
657 }
658
659 /* Make sure elements of thrd_inst_act_map are initialized properly when threads enter functions */
660 void FuncNode::init_inst_act_map(thread_id_t tid)
661 {
662         int thread_id = id_to_int(tid);
663         SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
664         uint old_size = thrd_inst_act_map->size();
665
666         if (thrd_inst_act_map->size() <= (uint) thread_id) {
667                 uint new_size = thread_id + 1;
668                 thrd_inst_act_map->resize(new_size);
669
670                 for (uint i = old_size;i < new_size;i++)
671                         (*thrd_inst_act_map)[i] = new inst_act_map_t(128);
672         }
673 }
674
675 /* Reset elements of thrd_inst_act_map when threads exit functions */
676 void FuncNode::reset_inst_act_map(thread_id_t tid)
677 {
678         int thread_id = id_to_int(tid);
679         SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
680
681         inst_act_map_t * map = (*thrd_inst_act_map)[thread_id];
682         map->reset();
683 }
684
685 void FuncNode::update_inst_act_map(thread_id_t tid, ModelAction * read_act)
686 {
687         int thread_id = id_to_int(tid);
688         SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
689
690         inst_act_map_t * map = (*thrd_inst_act_map)[thread_id];
691         FuncInst * read_inst = get_inst(read_act);
692         map->put(read_inst, read_act);
693 }
694
695 inst_act_map_t * FuncNode::get_inst_act_map(thread_id_t tid)
696 {
697         int thread_id = id_to_int(tid);
698         SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
699
700         return (*thrd_inst_act_map)[thread_id];
701 }
702
703 /* Add FuncNodes that this node may follow */
704 void FuncNode::add_out_edge(FuncNode * other)
705 {
706         if ( !edge_table.contains(other) ) {
707                 edge_table.put(other, OUT_EDGE);
708                 out_edges.push_back(other);
709                 return;
710         }
711
712         edge_type_t edge = edge_table.get(other);
713         if (edge == IN_EDGE) {
714                 edge_table.put(other, BI_EDGE);
715                 out_edges.push_back(other);
716         }
717 }
718
719 /* Compute the distance between this FuncNode and the target node.
720  * Return -1 if the target node is unreachable or the actual distance
721  * is greater than max_step.
722  */
723 int FuncNode::compute_distance(FuncNode * target, int max_step)
724 {
725         if (target == NULL)
726                 return -1;
727         else if (target == this)
728                 return 0;
729
730         SnapList<FuncNode *> queue;
731         HashTable<FuncNode *, int, uintptr_t, 0> distances(128);
732
733         queue.push_back(this);
734         distances.put(this, 0);
735
736         while (!queue.empty()) {
737                 FuncNode * curr = queue.front();
738                 queue.pop_front();
739                 int dist = distances.get(curr);
740
741                 if (max_step <= dist)
742                         return -1;
743
744                 ModelList<FuncNode *> * outEdges = curr->get_out_edges();
745                 mllnode<FuncNode *> * it;
746                 for (it = outEdges->begin();it != NULL;it = it->getNext()) {
747                         FuncNode * out_node = it->getVal();
748
749                         /* This node has not been visited before */
750                         if ( !distances.contains(out_node) ) {
751                                 if (out_node == target)
752                                         return dist + 1;
753
754                                 queue.push_back(out_node);
755                                 distances.put(out_node, dist + 1);
756                         }
757                 }
758         }
759
760         /* Target node is unreachable */
761         return -1;
762 }
763
764 /* Implement quick sort to sort leaves before assigning base scores */
765 template<typename _Tp>
766 static int partition(ModelVector<_Tp *> * arr, int low, int high)
767 {
768         unsigned int pivot = (*arr)[high]->get_depth();
769         int i = low - 1;
770
771         for (int j = low; j <= high - 1; j++) {
772                 if ( (*arr)[j]->get_depth() < pivot ) {
773                         i++;
774                         _Tp * tmp = (*arr)[i];
775                         (*arr)[i] = (*arr)[j];
776                         (*arr)[j] = tmp;
777                 }
778         }
779
780         _Tp * tmp = (*arr)[i + 1];
781         (*arr)[i + 1] = (*arr)[high];
782         (*arr)[high] = tmp;
783
784         return i + 1;
785 }
786
787 /* Implement quick sort to sort leaves before assigning base scores */
788 template<typename _Tp>
789 static void quickSort(ModelVector<_Tp *> * arr, int low, int high)
790 {
791         if (low < high) {
792                 int pi = partition(arr, low, high);
793
794                 quickSort(arr, low, pi - 1);
795                 quickSort(arr, pi + 1, high);
796         }
797 }
798
799 void FuncNode::assign_initial_weight()
800 {
801         PredSetIter * it = predicate_leaves.iterator();
802         leaves_tmp_storage.clear();
803
804         while (it->hasNext()) {
805                 Predicate * pred = it->next();
806                 double weight = 100.0 / sqrt(pred->get_expl_count() + 1);
807                 pred->set_weight(weight);
808                 leaves_tmp_storage.push_back(pred);
809         }
810         delete it;
811
812         quickSort(&leaves_tmp_storage, 0, leaves_tmp_storage.size() - 1);
813
814         // assign scores for internal nodes;
815         while ( !leaves_tmp_storage.empty() ) {
816                 Predicate * leaf = leaves_tmp_storage.back();
817                 leaves_tmp_storage.pop_back();
818
819                 Predicate * curr = leaf->get_parent();
820                 while (curr != NULL) {
821                         if (curr->get_weight() != 0) {
822                                 // Has been exlpored
823                                 break;
824                         }
825
826                         ModelVector<Predicate *> * children = curr->get_children();
827                         double weight_sum = 0;
828                         bool has_unassigned_node = false;
829
830                         for (uint i = 0; i < children->size(); i++) {
831                                 Predicate * child = (*children)[i];
832
833                                 // If a child has unassigned weight
834                                 double weight = child->get_weight();
835                                 if (weight == 0) {
836                                         has_unassigned_node = true;
837                                         break;
838                                 } else
839                                         weight_sum += weight;
840                         }
841
842                         if (!has_unassigned_node) {
843                                 double average_weight = (double) weight_sum / (double) children->size();
844                                 double weight = average_weight * pow(0.9, curr->get_depth());
845                                 curr->set_weight(weight);
846                         } else
847                                 break;
848
849                         curr = curr->get_parent();
850                 }
851         }
852 }
853
854 void FuncNode::update_predicate_tree_weight()
855 {
856         if (marker == 2) {
857                 // Predicate tree is initially built
858                 assign_initial_weight();
859                 return;
860         }
861
862         weight_debug_vec.clear();
863
864         quickSort(&leaves_tmp_storage, 0, leaves_tmp_storage.size() - 1);
865         for (uint i = 0; i < leaves_tmp_storage.size(); i++) {
866                 Predicate * pred = leaves_tmp_storage[i];
867                 double weight = 100.0 / sqrt(pred->get_expl_count() + 1);
868                 pred->set_weight(weight);
869         }
870
871         // Update weights in internal nodes
872         while ( !leaves_tmp_storage.empty() ) {
873                 Predicate * leaf = leaves_tmp_storage.back();
874                 leaves_tmp_storage.pop_back();
875
876                 Predicate * curr = leaf->get_parent();
877                 while (curr != NULL) {
878                         ModelVector<Predicate *> * children = curr->get_children();
879                         double weight_sum = 0;
880                         bool has_unassigned_node = false;
881
882                         for (uint i = 0; i < children->size(); i++) {
883                                 Predicate * child = (*children)[i];
884
885                                 double weight = child->get_weight();
886                                 if (weight != 0)
887                                         weight_sum += weight;
888                                 else if ( predicate_leaves.contains(child) ) {
889                                         // If this child is a leaf
890                                         double weight = 100.0 / sqrt(child->get_expl_count() + 1);
891                                         child->set_weight(weight);
892                                         weight_sum += weight;
893                                 } else {
894                                         has_unassigned_node = true;
895                                         weight_debug_vec.push_back(child);      // For debugging purpose
896                                         break;
897                                 }
898                         }
899
900                         if (!has_unassigned_node) {
901                                 double average_weight = (double) weight_sum / (double) children->size();
902                                 double weight = average_weight * pow(0.9, curr->get_depth());
903                                 curr->set_weight(weight);
904                         } else
905                                 break;
906
907                         curr = curr->get_parent();
908                 }
909         }
910
911         for (uint i = 0; i < weight_debug_vec.size(); i++) {
912                 Predicate * tmp = weight_debug_vec[i];
913                 ASSERT( tmp->get_weight() != 0 );
914         }
915 }
916
917 void FuncNode::print_predicate_tree()
918 {
919         model_print("digraph function_%s {\n", func_name);
920         predicate_tree_entry->print_pred_subtree();
921         predicate_tree_exit->print_predicate();
922         model_print("}\n");     // end of graph
923 }