move write_history to funcnode.cc and do experiment

[c11tester.git] / funcnode.h

diff --git a/funcnode.h b/funcnode.h
index d2d3c427331632574dd70a648cce47c356aeab4c..b8562d3ed368852f2f289661ced175f84e5a39a9 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -8,6 +8,7 @@
 
 typedef ModelList<FuncInst *> func_inst_list_mt;
 typedef HashTable<void *, uint64_t, uintptr_t, 4, model_malloc, model_calloc, model_free> read_map_t;
+typedef HashSet<uint64_t, uint64_t, 0, model_malloc, model_calloc, model_free> write_set_t;
 
 class FuncNode {
 public:
@@ -31,10 +32,13 @@ public:
        uint64_t query_last_read(void * location, uint32_t tid);
        void clear_read_map(uint32_t tid);
 
+       void add_to_write_history(void * location, uint64_t write_val);
+
        /* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */
        void generate_predicate(FuncInst * func_inst);
 
        void print_last_read(uint32_t tid);
+       void print_write();
 
        MEMALLOC
 private:
@@ -54,7 +58,9 @@ private:
 
        /* Store the values read by atomic read actions per memory location for each thread */
        ModelVector<read_map_t *> thrd_read_map;
-       HashSet<void *, uintptr_t, 4, model_malloc, model_calloc, model_free> read_locations;
+
+       HashTable<void *, write_set_t *, uintptr_t, 4, model_malloc, model_calloc, model_free> write_history;
+       HashSet<void *, uintptr_t, 4, model_malloc, model_calloc, model_free> write_locations;
 };
 
 #endif /* __FUNCNODE_H__ */