Design a method to select predicate branches based on exploration counts
[c11tester.git] / predicate.cc
index 2d7777783dac99e1f28553b416c969a0b34e4591..a64737e80e0dc511f93f2381583cddf207c04a86 100644 (file)
@@ -1,8 +1,12 @@
+#include "funcinst.h"
 #include "predicate.h"
+#include "concretepredicate.h"
 
 Predicate::Predicate(FuncInst * func_inst, bool is_entry) :
        func_inst(func_inst),
        entry_predicate(is_entry),
+       does_write(false),
+       exploration_count(0),
        pred_expressions(16),
        children(),
        parent(NULL),
@@ -57,6 +61,39 @@ void Predicate::copy_predicate_expr(Predicate * other)
        }
 }
 
+/* Evaluate predicate expressions against the given inst_act_map */
+ConcretePredicate * Predicate::evaluate(inst_act_map_t * inst_act_map, thread_id_t tid)
+{
+       ConcretePredicate * concrete = new ConcretePredicate(tid);
+       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->add_expression(ptr->token, value, ptr->value);
+       }
+
+       return concrete;
+}
+
 void Predicate::print_predicate()
 {
        model_print("\"%p\" [shape=box, label=\"\n", this);
@@ -89,6 +126,11 @@ void Predicate::print_predicate()
                                break;
                }
        }
+
+       if (does_write) {
+               model_print("Does write\n");
+       }
+       model_print("Count: %d\n", exploration_count);
        model_print("\"];\n");
 }