Able to evaluate predicate expression against a 'context' and generate concrete predi...
authorweiyu <weiyuluo1232@gmail.com>
Fri, 27 Sep 2019 00:30:01 +0000 (17:30 -0700)
committerweiyu <weiyuluo1232@gmail.com>
Fri, 27 Sep 2019 00:30:01 +0000 (17:30 -0700)
funcnode.cc
newfuzzer.cc
newfuzzer.h
predicate.cc
predicate.h

index e08ca1b..d328a4c 100644 (file)
@@ -321,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) {
@@ -332,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:
index 98d56f2..4e0d69d 100644 (file)
@@ -25,6 +25,8 @@ void NewFuzzer::register_engine(ModelHistory * history, ModelExecution *executio
 
 int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set)
 {
+//     return random() % rf_set->size();
+
        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);
 
@@ -46,8 +48,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                prune_writes(tid, selected_branch, rf_set, inst_act_map);
        }
 
-       // TODO: make this thread sleep if no write satisfies the chosen predicate
-       // if no read satisfies the selected predicate
+       // No write satisfies the selected predicate
        if ( rf_set->size() == 0 ) {
                Thread * read_thread = execution->get_thread(tid);
                model_print("the %d read action of thread %d is unsuccessful\n", read->get_seq_number(), read_thread->get_id());
@@ -56,7 +57,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                read_thread->set_pending(read);
                read->reset_seq_number();
                execution->restore_last_seq_num();
-               
+
                conditional_sleep(read_thread);
                return -1;
 /*
@@ -147,39 +148,30 @@ bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred,
 
        bool pruned = false;
        uint index = 0;
+       SnapVector<struct concrete_pred_expr> concrete_exprs = pred->evaluate(inst_act_map);
+
        while ( index < rf_set->size() ) {
                ModelAction * write_act = (*rf_set)[index];
+               uint64_t write_val = write_act->get_write_value();
                bool satisfy_predicate = true;
 
-               PredExprSetIter * pred_expr_it = pred_expressions->iterator();
-               while (pred_expr_it->hasNext()) {
-                       struct pred_expr * expression = pred_expr_it->next();
-                       uint64_t write_val = write_act->get_write_value();
+               for (uint i = 0; i < concrete_exprs.size(); i++) {
+                       struct concrete_pred_expr concrete = concrete_exprs[i];
                        bool equality;
 
-                       // No predicate, return false
-                       if (expression->token == NOPREDICATE)
-                               return pruned;
-
-                       switch(expression->token) {
+                       switch (concrete.token) {
+                               case NOPREDICATE:
+                                       return false;
                                case EQUALITY:
-                                       FuncInst * to_be_compared;
-                                       ModelAction * last_act;
-                                       uint64_t last_read;
-
-                                       to_be_compared = expression->func_inst;
-                                       last_act = inst_act_map->get(to_be_compared);
-                                       last_read = last_act->get_reads_from_value();
-
-                                       equality = (write_val == last_read);
-                                       if (equality != expression->value)
+                                       equality = (write_val == concrete.value);
+                                       if (equality != concrete.equality)
                                                satisfy_predicate = false;
                                        break;
                                case NULLITY:
                                        equality = ((void*)write_val == NULL);
-                                       if (equality != expression->value)
-                                               satisfy_predicate = false;
-                                       break;
+                                        if (equality != concrete.equality)
+                                                satisfy_predicate = false;
+                                        break;
                                default:
                                        model_print("unknown predicate token\n");
                                        break;
@@ -231,6 +223,7 @@ Thread * NewFuzzer::selectThread(int * threadlist, int numthreads)
        return model->get_thread(curr_tid);
 }
 
+/* Force waking up one of threads paused by Fuzzer */
 void NewFuzzer::wake_up_paused_threads(int * threadlist, int * numthreads)
 {
        int random_index = random() % paused_thread_set.size();
@@ -245,6 +238,12 @@ void NewFuzzer::wake_up_paused_threads(int * threadlist, int * numthreads)
        (*numthreads)++;
 }
 
+/* Notify one of conditional sleeping threads if the desired write is available */
+bool NewFuzzer::notify_conditional_sleep(Thread * thread)
+{
+
+}
+
 bool NewFuzzer::shouldWait(const ModelAction * act)
 {
        return random() & 1;
index db25cfd..d6fa3a4 100644 (file)
@@ -6,16 +6,12 @@
 #include "mymemory.h"
 #include "stl-model.h"
 
-typedef HashTable<FuncInst *, ModelAction *, uintptr_t, 0> inst_act_map_t;
-
 class NewFuzzer : public Fuzzer {
 public:
        NewFuzzer();
        int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
        Predicate * get_selected_child_branch(thread_id_t tid);
-       void conditional_sleep(Thread * thread);
        bool has_paused_threads();
-       void wake_up_paused_threads(int * threadlist, int * numthreads);
 
        Thread * selectThread(int * threadlist, int numthreads);
        Thread * selectNotify(action_list_t * waiters);
@@ -42,6 +38,10 @@ private:
         * Only used by selectWrite;
         */
        SnapVector<Thread *> paused_thread_set;
+
+       void conditional_sleep(Thread * thread);
+       void wake_up_paused_threads(int * threadlist, int * numthreads);
+       bool notify_conditional_sleep(Thread * thread);
 };
 
 #endif /* end of __NEWFUZZER_H__ */
index 5cc0219..a5ba11c 100644 (file)
@@ -58,6 +58,39 @@ void Predicate::copy_predicate_expr(Predicate * other)
        }
 }
 
+/* Evaluate predicate expressions against the given inst_act_map */
+SnapVector<struct concrete_pred_expr> Predicate::evaluate(inst_act_map_t * inst_act_map)
+{
+       SnapVector<struct concrete_pred_expr> concrete_exprs;
+       PredExprSetIter * it = pred_expressions.iterator();
+
+       while (it->hasNext()) {
+               struct pred_expr * ptr = it->next();
+               uint64_t value = 0;
+
+               switch(ptr->token) {
+                       case NOPREDICATE:
+                               break;
+                       case EQUALITY:
+                               FuncInst * to_be_compared;
+                               ModelAction * last_act;
+
+                               to_be_compared = ptr->func_inst;
+                               last_act = inst_act_map->get(to_be_compared);
+                               value = last_act->get_reads_from_value();
+                               break;
+                       case NULLITY:
+                               break;
+                       default:
+                               break;
+               }
+
+               concrete_exprs.push_back(concrete_pred_expr(ptr->token, value, ptr->value));
+       }
+
+       return concrete_exprs;
+}
+
 void Predicate::print_predicate()
 {
        model_print("\"%p\" [shape=box, label=\"\n", this);
index 4243a0d..6c83683 100644 (file)
@@ -44,6 +44,19 @@ struct half_pred_expr {
        SNAPSHOTALLOC
 };
 
+struct concrete_pred_expr {
+       concrete_pred_expr(token_t token, uint64_t value, bool equality) :
+               token(token),
+               value(value),
+               equality(equality)
+       {}
+
+       token_t token;
+       uint64_t value;
+       bool equality;
+
+       SNAPSHOTALLOC
+};
 
 class Predicate {
 public:
@@ -70,6 +83,8 @@ public:
        bool is_write() { return does_write; }
        void set_write(bool is_write) { does_write = is_write; }
 
+       SnapVector<struct concrete_pred_expr> evaluate(inst_act_map_t * inst_act_map);
+
        void print_predicate();
        void print_pred_subtree();