Change the return type of Predicate::evaluate

diff --git a/Makefile b/Makefile
index edff29be9cf236a9ca9323819a6b7bb16bc3fc52..6a57d4a9902a469c4745c7ea20373b4ce3e8ed91 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -5,7 +5,8 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
           datarace.o impatomic.o cmodelint.o \
           snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \
           context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o \
-          sleeps.o history.o funcnode.o funcinst.o predicate.o printf.o newfuzzer.o
+          sleeps.o history.o funcnode.o funcinst.o predicate.o printf.o newfuzzer.o \
+          concretepredicate.o
 
 CPPFLAGS += -Iinclude -I.
 LDFLAGS := -ldl -lrt -rdynamic -lpthread

diff --git a/classlist.h b/classlist.h
index 65ac08df62da8bb64cdab4955bcdc8f5172de7d1..4cd97b3753e1075094de848f59a041c288748bd9 100644 (file)
--- a/classlist.h
+++ b/classlist.h
@@ -19,6 +19,7 @@ class NewFuzzer;
 class FuncNode;
 class FuncInst;
 class Predicate;
+class ConcretePredicate;
 
 struct model_snapshot_members;
 struct bug_message;

diff --git a/concretepredicate.cc b/concretepredicate.cc
index e3cbcac6f1922a692945d4c2dbb2f6dd8cf86509..9633e6c7aded1c991bad063749eb1e18d1225ecc 100644 (file)
--- a/concretepredicate.cc
+++ b/concretepredicate.cc
@@ -1,7 +1,7 @@
 #include "concretepredicate.h"
 
-ConcretePredicate::ConcretePredicate(void * loc) :
-       location(loc),
+ConcretePredicate::ConcretePredicate(thread_id_t tid) :
+       tid(tid),
        expressions()
 {}
 

diff --git a/concretepredicate.h b/concretepredicate.h
index 2ec4e85d1870d2a644f3d71b78947fd62fdb356e..6319a2ee23abbd29b97dcfd0938f00256fb501ff 100644 (file)
--- a/concretepredicate.h
+++ b/concretepredicate.h
@@ -2,12 +2,13 @@
 #define __CONCRETE_PREDICATE_H__
 
 #include <inttypes.h>
+#include "modeltypes.h"
 #include "classlist.h"
 #include "predicatetypes.h"
 
 class ConcretePredicate {
 public:
-       ConcretePredicate(void * loc);
+       ConcretePredicate(thread_id_t tid);
        ~ConcretePredicate();
 
        void add_expression(token_t token, uint64_t value, bool equality);
@@ -16,6 +17,7 @@ public:
 
        SNAPSHOTALLOC
 private:
+       thread_id_t tid;
        void * location;
        SnapVector<struct concrete_pred_expr> expressions;
 };

diff --git a/funcnode.cc b/funcnode.cc
index d328a4c5d24f6753fe0faf9338e153bc7284072a..8cd81423f710e9fa222ce3892ab2f91808cbb8a9 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -1,4 +1,6 @@
+#include "history.h"
 #include "funcnode.h"
+#include "concretepredicate.h"
 
 FuncNode::FuncNode(ModelHistory * history) :
        history(history),
@@ -331,9 +333,10 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
                        unset_predicates->push_back(branch);
                }
 
-               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];
+               ConcretePredicate * concrete_pred = branch->evaluate(inst_act_map, next_act->get_tid());
+               SnapVector<struct concrete_pred_expr> * concrete_exprs = concrete_pred->getExpressions();
+               for (uint i = 0; i < concrete_exprs->size(); i++) {
+                       struct concrete_pred_expr concrete = (*concrete_exprs)[i];
                        uint64_t next_read;
                        bool equality;
 

diff --git a/newfuzzer.cc b/newfuzzer.cc
index 1fdc7d85f91f2b5b121b242b9c84ece0e987594d..eefd553ec565ea2c70553cc260ce145c2b08c861 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -3,6 +3,7 @@
 #include "model.h"
 #include "action.h"
 #include "execution.h"
+#include "history.h"
 #include "funcnode.h"
 #include "schedule.h"
 #include "concretepredicate.h"
@@ -149,15 +150,17 @@ 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);
+
+       ConcretePredicate * concrete_pred = pred->evaluate(inst_act_map, tid);
+       SnapVector<struct concrete_pred_expr> * concrete_exprs = concrete_pred->getExpressions();
 
        while ( index < rf_set->size() ) {
                ModelAction * write_act = (*rf_set)[index];
                uint64_t write_val = write_act->get_write_value();
                bool satisfy_predicate = true;
 
-               for (uint i = 0; i < concrete_exprs.size(); i++) {
-                       struct concrete_pred_expr concrete = concrete_exprs[i];
+               for (uint i = 0; i < concrete_exprs->size(); i++) {
+                       struct concrete_pred_expr concrete = (*concrete_exprs)[i];
                        bool equality;
 
                        switch (concrete.token) {

diff --git a/predicate.cc b/predicate.cc
index a5ba11c928f661176d47c9feb0e9abc5fe379ec2..94eedfd52253382a46e659488346bd596fa397dd 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -1,4 +1,5 @@
 #include "predicate.h"
+#include "concretepredicate.h"
 
 Predicate::Predicate(FuncInst * func_inst, bool is_entry) :
        func_inst(func_inst),
@@ -59,9 +60,9 @@ 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)
+ConcretePredicate * Predicate::evaluate(inst_act_map_t * inst_act_map, thread_id_t tid)
 {
-       SnapVector<struct concrete_pred_expr> concrete_exprs;
+       ConcretePredicate * concrete = new ConcretePredicate(tid);
        PredExprSetIter * it = pred_expressions.iterator();
 
        while (it->hasNext()) {
@@ -85,12 +86,13 @@ SnapVector<struct concrete_pred_expr> Predicate::evaluate(inst_act_map_t * inst_
                                break;
                }
 
-               concrete_exprs.push_back(concrete_pred_expr(ptr->token, value, ptr->value));
+               concrete->add_expression(ptr->token, value, ptr->value);
        }
 
-       return concrete_exprs;
+       return concrete;
 }
 
+
 void Predicate::print_predicate()
 {
        model_print("\"%p\" [shape=box, label=\"\n", this);

diff --git a/predicate.h b/predicate.h
index 4bb3039b2ced7c62d9feb945614ec6340c6f75cb..1600cc8a9f5f7e26d628ef17b155e775a40b657a 100644 (file)
--- a/predicate.h
+++ b/predicate.h
@@ -4,6 +4,7 @@
 #include "funcinst.h"
 #include "hashset.h"
 #include "predicatetypes.h"
+#include "classlist.h"
 
 unsigned int pred_expr_hash (struct pred_expr *);
 bool pred_expr_equal(struct pred_expr *, struct pred_expr *);
@@ -35,7 +36,7 @@ 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);
+       ConcretePredicate * evaluate(inst_act_map_t * inst_act_map, thread_id_t tid);
 
        void print_predicate();
        void print_pred_subtree();