Able to evaluate predicate expression against a 'context' and generate concrete predi...

[c11tester.git] / funcnode.cc

diff --git a/funcnode.cc b/funcnode.cc
index 3db022695ece62edb0e775f7ea1746fc1b83319c..d328a4c5d24f6753fe0faf9338e153bc7284072a 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -230,13 +230,14 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
        if (act_list == NULL || act_list->size() == 0)
                return;
 
-       /* map a FuncInst to the its predicate */
+       /* Map a FuncInst to the its predicate */
        HashTable<FuncInst *, Predicate *, uintptr_t, 0> inst_pred_map(128);
 
-       // number FuncInsts to detect loops
+       // Number FuncInsts to detect loops
        HashTable<FuncInst *, uint32_t, uintptr_t, 0> inst_id_map(128);
        uint32_t inst_counter = 0;
 
+       /* Only need to store the locations of read actions */
        HashTable<void *, ModelAction *, uintptr_t, 0> loc_act_map(128);
        HashTable<FuncInst *, ModelAction *, uintptr_t, 0> inst_act_map(128);
 
@@ -291,12 +292,15 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                if (next_act->is_write())
                        curr_pred->set_write(true);
 
+               if (next_act->is_read()) {
+                       loc_act_map.put(next_act->get_location(), next_act);
+               }
+
+               inst_act_map.put(next_inst, next_act);
                inst_pred_map.put(next_inst, curr_pred);
                if (!inst_id_map.contains(next_inst))
                        inst_id_map.put(next_inst, inst_counter++);
 
-               loc_act_map.put(next_act->get_location(), next_act);
-               inst_act_map.put(next_inst, next_act);
                it = it->getNext();
        }
 }
@@ -317,10 +321,9 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
                if (branch->get_func_inst() != next_inst)
                        continue;
 
-               /* check against predicate expressions */
+               /* Check against predicate expressions */
                bool predicate_correct = true;
                PredExprSet * pred_expressions = branch->get_pred_expressions();
-               PredExprSetIter * pred_expr_it = pred_expressions->iterator();
 
                /* Only read and rmw actions my have unset predicate expressions */
                if (pred_expressions->getSize() == 0) {
@@ -328,33 +331,26 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
                        unset_predicates->push_back(branch);
                }
 
-               while (pred_expr_it->hasNext()) {
-                       pred_expr * pred_expression = pred_expr_it->next();
-                       uint64_t last_read, next_read;
+               SnapVector<struct concrete_pred_expr> concrete_exprs = branch->evaluate(inst_act_map);
+               for (uint i = 0; i < concrete_exprs.size(); i++) {
+                       struct concrete_pred_expr concrete = concrete_exprs[i];
+                       uint64_t next_read;
                        bool equality;
 
-                       switch(pred_expression->token) {
+                       switch (concrete.token) {
                                case NOPREDICATE:
                                        predicate_correct = true;
                                        break;
                                case EQUALITY:
-                                       FuncInst * to_be_compared;
-                                       ModelAction * last_act;
-
-                                       to_be_compared = pred_expression->func_inst;
-                                       last_act = inst_act_map->get(to_be_compared);
-
-                                       last_read = last_act->get_reads_from_value();
                                        next_read = next_act->get_reads_from_value();
-                                       equality = (last_read == next_read);
-                                       if (equality != pred_expression->value)
+                                       equality = (next_read == concrete.value);
+                                       if (equality != concrete.equality)
                                                predicate_correct = false;
-
                                        break;
                                case NULLITY:
                                        next_read = next_act->get_reads_from_value();
                                        equality = ((void*)next_read == NULL);
-                                       if (equality != pred_expression->value)
+                                       if (equality != concrete.equality)
                                                predicate_correct = false;
                                        break;
                                default:
@@ -471,6 +467,12 @@ void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst,
                (*curr_pred)->add_child(pred);
                pred->set_parent(*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];
+               snapshot_free(tmp);
+       }
 }
 
 /* Amend predicates that contain no predicate expressions. Currenlty only amend with NULLITY predicates */