From: weiyu Date: Fri, 27 Sep 2019 00:30:01 +0000 (-0700) Subject: Able to evaluate predicate expression against a 'context' and generate concrete predi... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=70acabc306bc3014b3698e394908faf23a66a0b8;hp=35ebf30f42f46d47fbec1db62acc453733dfb2e1 Able to evaluate predicate expression against a 'context' and generate concrete predicates --- diff --git a/funcnode.cc b/funcnode.cc index e08ca1b8..d328a4c5 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -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 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: diff --git a/newfuzzer.cc b/newfuzzer.cc index 98d56f21..4e0d69db 100644 --- a/newfuzzer.cc +++ b/newfuzzer.cc @@ -25,6 +25,8 @@ void NewFuzzer::register_engine(ModelHistory * history, ModelExecution *executio int NewFuzzer::selectWrite(ModelAction *read, SnapVector * 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 * 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 * 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 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; diff --git a/newfuzzer.h b/newfuzzer.h index db25cfd8..d6fa3a4f 100644 --- a/newfuzzer.h +++ b/newfuzzer.h @@ -6,16 +6,12 @@ #include "mymemory.h" #include "stl-model.h" -typedef HashTable inst_act_map_t; - class NewFuzzer : public Fuzzer { public: NewFuzzer(); int selectWrite(ModelAction *read, SnapVector* 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 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__ */ diff --git a/predicate.cc b/predicate.cc index 5cc0219c..a5ba11c9 100644 --- a/predicate.cc +++ b/predicate.cc @@ -58,6 +58,39 @@ void Predicate::copy_predicate_expr(Predicate * other) } } +/* Evaluate predicate expressions against the given inst_act_map */ +SnapVector Predicate::evaluate(inst_act_map_t * inst_act_map) +{ + SnapVector 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); diff --git a/predicate.h b/predicate.h index 4243a0d8..6c83683d 100644 --- a/predicate.h +++ b/predicate.h @@ -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 evaluate(inst_act_map_t * inst_act_map); + void print_predicate(); void print_pred_subtree();