Store the set of predicate leaves in FuncNode
authorweiyu <weiyuluo1232@gmail.com>
Tue, 10 Dec 2019 19:09:27 +0000 (11:09 -0800)
committerweiyu <weiyuluo1232@gmail.com>
Tue, 10 Dec 2019 19:09:27 +0000 (11:09 -0800)
funcnode.cc
funcnode.h
predicate.cc
predicate.h

index 663447bf17fed96f8eea6e8cb02e48d84595c828..5bb73b9868765a534515dd461f6ed954e2911f93 100644 (file)
@@ -16,6 +16,7 @@ FuncNode::FuncNode(ModelHistory * history) :
        inst_list(),
        entry_insts(),
        predicate_tree_position(),
+       predicate_leaves(),
        edge_table(32),
        out_edges()
 {
@@ -23,7 +24,6 @@ FuncNode::FuncNode(ModelHistory * history) :
        predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
 
        predicate_tree_exit = new Predicate(NULL, false, true);
-       predicate_tree_exit->alloc_pre_exit_predicates();
        predicate_tree_exit->set_depth(MAX_DEPTH);
 
        /* Snapshot data structures below */
@@ -290,7 +290,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                        ASSERT(unset_predicates.size() == 1);
                        Predicate * one_branch = unset_predicates[0];
 
-                       bool amended = amend_predicate_expr(&curr_pred, next_inst, next_act);
+                       bool amended = amend_predicate_expr(curr_pred, next_inst, next_act);
                        if (amended)
                                continue;
                        else {
@@ -319,7 +319,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                if (!branch_found) {
                        SnapVector<struct half_pred_expr *> half_pred_expressions;
                        infer_predicates(next_inst, next_act, &loc_act_map, &half_pred_expressions);
-                       generate_predicates(&curr_pred, next_inst, &half_pred_expressions);
+                       generate_predicates(curr_pred, next_inst, &half_pred_expressions);
                        continue;
                }
 
@@ -464,17 +464,21 @@ SnapVector<struct half_pred_expr *> * half_pred_expressions)
 }
 
 /* Able to generate complex predicates when there are multiple predciate expressions */
-void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst,
+void FuncNode::generate_predicates(Predicate * curr_pred, FuncInst * next_inst,
 SnapVector<struct half_pred_expr *> * half_pred_expressions)
 {
        if (half_pred_expressions->size() == 0) {
                Predicate * new_pred = new Predicate(next_inst);
-               (*curr_pred)->add_child(new_pred);
-               new_pred->set_parent(*curr_pred);
+               curr_pred->add_child(new_pred);
+               new_pred->set_parent(curr_pred);
+
+               /* Maintain predicate leaves */
+               predicate_leaves.add(new_pred);
+               predicate_leaves.remove(curr_pred);
 
                /* entry predicates and predicates containing pure write actions
                 * have no predicate expressions */
-               if ( (*curr_pred)->is_entry_predicate() )
+               if ( curr_pred->is_entry_predicate() )
                        new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
                else if (next_inst->is_write()) {
                        /* next_inst->is_write() <==> pure writes */
@@ -511,10 +515,16 @@ SnapVector<struct half_pred_expr *> * half_pred_expressions)
 
        for (uint i = 0;i < predicates.size();i++) {
                Predicate * pred= predicates[i];
-               (*curr_pred)->add_child(pred);
-               pred->set_parent(*curr_pred);
+               curr_pred->add_child(pred);
+               pred->set_parent(curr_pred);
+
+               /* Add new predicate leaves */
+               predicate_leaves.add(pred);
        }
 
+       /* Remove predicate node that has children */
+       predicate_leaves.remove(curr_pred);
+
        /* Free memories allocated by infer_predicate */
        for (uint i = 0;i < half_pred_expressions->size();i++) {
                struct half_pred_expr * tmp = (*half_pred_expressions)[i];
@@ -523,18 +533,18 @@ SnapVector<struct half_pred_expr *> * half_pred_expressions)
 }
 
 /* Amend predicates that contain no predicate expressions. Currenlty only amend with NULLITY predicates */
-bool FuncNode::amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act)
+bool FuncNode::amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act)
 {
        // there should only be only child
-       Predicate * unset_pred = (*curr_pred)->get_children()->back();
+       Predicate * unset_pred = curr_pred->get_children()->back();
        uint64_t read_val = next_act->get_reads_from_value();
 
        // only generate NULLITY predicate when it is actually NULL.
        if ( !next_inst->is_single_location() && (void*)read_val == NULL ) {
                Predicate * new_pred = new Predicate(next_inst);
 
-               (*curr_pred)->add_child(new_pred);
-               new_pred->set_parent(*curr_pred);
+               curr_pred->add_child(new_pred);
+               new_pred->set_parent(curr_pred);
 
                unset_pred->add_predicate_expr(NULLITY, NULL, false);
                new_pred->add_predicate_expr(NULLITY, NULL, true);
@@ -727,26 +737,50 @@ int FuncNode::compute_distance(FuncNode * target, int max_step)
        return -1;
 }
 
-void FuncNode::assign_base_score()
+/* Implement quick sort to sort leaves before assigning base scores */
+static int partition(SnapVector<Predicate *> * arr, int low, int high)
 {
-       SnapVector<Predicate *> leaves;
-       SnapList<Predicate *> queue;
-       queue.push_front(predicate_tree_entry);
-
-       // assign leaf score
-       while ( !queue.empty() ) {
-               Predicate * node = queue.back();
-               queue.pop_back();
-
-               ModelVector<Predicate *> * children = node->get_children();
-               if (children->empty()) {
-                       node->set_weight(1);
-                       leaves.push_back(node);
+       unsigned int pivot = (*arr)[high]->get_depth();
+       int i = low - 1;
+
+       for (int j = low; j <= high - 1; j++) {
+               if ( (*arr)[j]->get_depth() < pivot ) {
+                       i++;
+                       Predicate *tmp = (*arr)[i];
+                       (*arr)[i] = (*arr)[j];
+                       (*arr)[j] = tmp;
                }
+       }
+
+       Predicate * tmp = (*arr)[i + 1];
+       (*arr)[i + 1] = (*arr)[high];
+       (*arr)[high] = tmp;
 
-               for (uint i = 0; i < children->size(); i++)
-                       queue.push_front( (*children)[i] );
+       return i + 1;
+}
+
+/* Implement quick sort to sort leaves before assigning base scores */
+static void quickSort(SnapVector<Predicate *> * arr, int low, int high)
+{
+       if (low < high) {
+               int pi = partition(arr, low, high);
+
+               quickSort(arr, low, pi - 1);
+               quickSort(arr, pi + 1, high);
        }
+}
+
+void FuncNode::assign_base_score()
+{
+       PredSetIter * it = predicate_leaves.iterator();
+       SnapVector<Predicate *> leaves;
+       while (it->hasNext()) {
+               Predicate * pred = it->next();
+               pred->set_weight(1);
+               leaves.push_back(pred);
+       }
+
+       quickSort(&leaves, 0, leaves.size() - 1);
 
        // assign scores for internal nodes;
        while ( !leaves.empty() ) {
index ea0be0298d81b9a86b591f5666ce1005aa221dd2..ecb270b0625194d8d745cc45ad191a4f43aa54ce 100644 (file)
@@ -88,8 +88,8 @@ private:
        func_inst_list_mt entry_insts;
 
        void infer_predicates(FuncInst * next_inst, ModelAction * next_act, HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map, SnapVector<struct half_pred_expr *> * half_pred_expressions);
-       void generate_predicates(Predicate ** curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
-       bool amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act);
+       void generate_predicates(Predicate * curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
+       bool amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act);
 
        /* Store action_lists when calls to update_tree are deferred */
        SnapList<action_list_t *> * action_list_buffer;
@@ -110,6 +110,7 @@ private:
 
        /* Run-time position in the predicate tree for each thread */
        ModelVector<Predicate *> predicate_tree_position;
+       PredSet predicate_leaves;
 
        /* Store the relation between this FuncNode and other FuncNodes */
        HashTable<FuncNode *, edge_type_t, uintptr_t, 0, model_malloc, model_calloc, model_free> edge_table;
index eb979f8868a9de8097ca5cbb6c4be24a0bbaa2f8..b2c6e605c3354c91903115fa9385840970a1763c 100644 (file)
@@ -64,17 +64,6 @@ void Predicate::set_parent(Predicate * parent_pred)
 void Predicate::set_exit(Predicate * exit_pred)
 {
        exit = exit_pred;
-       exit_pred->add_pre_exit_predicate(this);
-}
-
-void Predicate::alloc_pre_exit_predicates()
-{
-       pre_exit_predicates = new ModelVector<Predicate *>();
-}
-
-void Predicate::add_pre_exit_predicate(Predicate * pred)
-{
-       pre_exit_predicates->push_back(pred);
 }
 
 void Predicate::copy_predicate_expr(Predicate * other)
index 0512835f6aadfbcab4ce7689dfd3e43ce689a863..8b1e7c8172ccbf97ec99d71e9f45133d609bfd86 100644 (file)
@@ -38,9 +38,6 @@ public:
        bool is_entry_predicate() { return entry_predicate; }
        void set_entry_predicate() { entry_predicate = true; }
 
-       void alloc_pre_exit_predicates();
-       void add_pre_exit_predicate(Predicate * pred);
-
        /* Whether func_inst does write or not */
        bool is_write() { return does_write; }
        void set_write(bool is_write) { does_write = is_write; }
@@ -84,9 +81,6 @@ private:
        Predicate * parent;
        Predicate * exit;
 
-       /* Predicates precede exit nodes. Only used by exit predicates */
-       ModelVector<Predicate *> * pre_exit_predicates;
-
        /* May have multiple back edges, e.g. nested loops */
        PredSet backedges;
 };