From: weiyu <weiyuluo1232@gmail.com>
Date: Thu, 15 Aug 2019 02:16:47 +0000 (-0700)
Subject: change the structure of predicate expressions, and modify the way nullity predicates...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f8a45d8d10f16533c926096c7538b4d9be73240b;p=c11tester.git
change the structure of predicate expressions, and modify the way nullity predicates are added
---
diff --git a/funcnode.cc b/funcnode.cc
index 5b6fb355..2bdd946d 100644
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -225,6 +225,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
/* map a FuncInst to the parent of its predicate */
HashTable<FuncInst *, Predicate *, uintptr_t, 0> inst_pred_map(128);
HashTable<void *, ModelAction *, uintptr_t, 0> loc_act_map(128);
+ HashTable<FuncInst *, ModelAction *, uintptr_t, 0> inst_act_map(128);
sllnode<ModelAction *> *it = act_list->begin();
Predicate * curr_pred = predicate_tree_entry;
@@ -234,7 +235,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
FuncInst * next_inst = get_inst(next_act);
Predicate * old_pred = curr_pred;
- bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &loc_act_map);
+ bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map);
// check back edges
if (!branch_found) {
@@ -257,18 +258,20 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
if (!branch_found) {
if ( loc_act_map.contains(next_act->get_location()) ) {
+ ModelAction * last_act = loc_act_map.get(next_act->get_location());
+ FuncInst * last_inst = get_inst(last_act);
+
Predicate * new_pred1 = new Predicate(next_inst);
- new_pred1->add_predicate(EQUALITY, next_act->get_location(), true);
+ new_pred1->add_predicate_expr(EQUALITY, last_inst, true);
Predicate * new_pred2 = new Predicate(next_inst);
- new_pred2->add_predicate(EQUALITY, next_act->get_location(), false);
+ new_pred2->add_predicate_expr(EQUALITY, last_inst, false);
curr_pred->add_child(new_pred1);
curr_pred->add_child(new_pred2);
new_pred1->set_parent(curr_pred);
new_pred2->set_parent(curr_pred);
- ModelAction * last_act = loc_act_map.get(next_act->get_location());
uint64_t last_read = last_act->get_reads_from_value();
uint64_t next_read = next_act->get_reads_from_value();
@@ -286,6 +289,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
}
loc_act_map.put(next_act->get_location(), next_act);
+ inst_act_map.put(next_inst, next_act);
it = it->getNext();
}
}
@@ -307,11 +311,12 @@ void FuncNode::deep_update(Predicate * curr_pred)
if (!has_null_pred) {
// func_inst->print();
- Predicate * parent = curr_pred->get_parent();
- curr_pred->add_predicate(NULLITY, NULL, 0);
-
Predicate * another_branch = new Predicate(func_inst);
- another_branch->add_predicate(NULLITY, NULL, 1);
+ another_branch->copy_predicate_expr(curr_pred);
+ another_branch->add_predicate_expr(NULLITY, NULL, 1);
+ curr_pred->add_predicate_expr(NULLITY, NULL, 0);
+
+ Predicate * parent = curr_pred->get_parent();
parent->add_child(another_branch);
// another_branch.add_children(i);
}
@@ -324,11 +329,12 @@ void FuncNode::deep_update(Predicate * curr_pred)
}
}
-/* Given curr_pred and next_inst, find the branch following curr_pred that contains next_inst and the correct predicate
+/* Given curr_pred and next_inst, find the branch following curr_pred that
+ * contains next_inst and the correct predicate.
* @return true if branch found, false otherwise.
*/
bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act,
- HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map)
+ HashTable<FuncInst *, ModelAction *, uintptr_t, 0> * inst_act_map)
{
/* check if a branch with func_inst and corresponding predicate exists */
bool branch_found = false;
@@ -351,12 +357,16 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
while (pred_expr_it->hasNext()) {
pred_expr * pred_expression = pred_expr_it->next();
uint64_t last_read, next_read;
- ModelAction * last_act;
bool equality;
switch(pred_expression->token) {
case EQUALITY:
- last_act = loc_act_map->get(next_act->get_location());
+ 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();
diff --git a/funcnode.h b/funcnode.h
index 730a7b7c..4e1f98d3 100644
--- a/funcnode.h
+++ b/funcnode.h
@@ -38,7 +38,7 @@ public:
/* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */
void update_predicate_tree(action_list_t * act_list);
void deep_update(Predicate * pred);
- bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable<void *, ModelAction *, uintptr_t, 0>* loc_act_map);
+ bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable<FuncInst *, ModelAction *, uintptr_t, 0>* inst_act_map);
void print_predicate_tree();
void print_last_read(uint32_t tid);
diff --git a/predicate.cc b/predicate.cc
index 128ac3dc..9ba69d38 100644
--- a/predicate.cc
+++ b/predicate.cc
@@ -18,16 +18,16 @@ bool pred_expr_equal(struct pred_expr * p1, struct pred_expr * p2)
{
if (p1->token != p2->token)
return false;
- if (p1->token == EQUALITY && p1->location != p2->location)
+ if (p1->token == EQUALITY && p1->func_inst != p2->func_inst)
return false;
if (p1->value != p2->value)
return false;
return true;
}
-void Predicate::add_predicate(token_t token, void * location, bool value)
+void Predicate::add_predicate_expr(token_t token, FuncInst * func_inst, bool value)
{
- struct pred_expr *ptr = new pred_expr(token, location, value);
+ struct pred_expr *ptr = new pred_expr(token, func_inst, value);
pred_expressions.add(ptr);
}
@@ -37,6 +37,18 @@ void Predicate::add_child(Predicate * child)
children.push_back(child);
}
+void Predicate::copy_predicate_expr(Predicate * other)
+{
+ PredExprSet * other_pred_expressions = other->get_pred_expressions();
+ PredExprSetIter * it = other_pred_expressions->iterator();
+
+ while (it->hasNext()) {
+ struct pred_expr * ptr = it->next();
+ struct pred_expr * copy = new pred_expr(ptr->token, ptr->func_inst, ptr->value);
+ pred_expressions.add(copy);
+ }
+}
+
void Predicate::print_predicate()
{
model_print("\"%p\" [shape=box, label=\"\n", this);
@@ -54,7 +66,18 @@ void Predicate::print_predicate()
while (it->hasNext()) {
struct pred_expr * expr = it->next();
- model_print("predicate: token: %d, location: %p, value: %d\n", expr->token, expr->location, expr->value);
+ FuncInst * inst = expr->func_inst;
+ switch (expr->token) {
+ case EQUALITY:
+ model_print("predicate token: equality, position: %s, value: %d\n", inst->get_position(), expr->value);
+ break;
+ case NULLITY:
+ model_print("predicate token: nullity, value: %d\n", expr->value);
+ break;
+ default:
+ model_print("unknown predicate token\n");
+ break;
+ }
}
model_print("\"];\n");
}
diff --git a/predicate.h b/predicate.h
index dbb959ea..3efd8905 100644
--- a/predicate.h
+++ b/predicate.h
@@ -18,14 +18,14 @@ typedef enum predicate_token {
* read at memory location specified in predicate_expr.
*/
struct pred_expr {
- pred_expr(token_t token, void * location, bool value) :
+ pred_expr(token_t token, FuncInst * inst, bool value) :
token(token),
- location(location),
+ func_inst(inst),
value(value)
{}
token_t token;
- void * location;
+ FuncInst * func_inst;
bool value;
MEMALLOC
@@ -39,10 +39,12 @@ public:
FuncInst * get_func_inst() { return func_inst; }
PredExprSet * get_pred_expressions() { return &pred_expressions; }
- void add_predicate(token_t token, void * location, bool value);
+
+ void add_predicate_expr(token_t token, FuncInst * func_inst, bool value);
void add_child(Predicate * child);
void set_parent(Predicate * parent_pred) { parent = parent_pred; }
void set_backedge(Predicate * back_pred) { backedge = back_pred; }
+ void copy_predicate_expr(Predicate * other);
ModelVector<Predicate *> * get_children() { return &children; }
Predicate * get_parent() { return parent; }