From: weiyu <weiyuluo1232@gmail.com>
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://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=70acabc306bc3014b3698e394908faf23a66a0b8;p=c11tester.git
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<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:
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<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;
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<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__ */
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<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);
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<struct concrete_pred_expr> evaluate(inst_act_map_t * inst_act_map);
+
void print_predicate();
void print_pred_subtree();