From: weiyu <weiyuluo1232@gmail.com>
Date: Tue, 25 Feb 2020 03:12:13 +0000 (-0800)
Subject: Fix memory issue; ModelList should be cleared before deletion; use ModelVector instead
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=f8b9a9f560b0ea8e126ab1132dac5af4e5cdc8fa

Fix memory issue; ModelList should be cleared before deletion; use ModelVector instead
---

diff --git a/funcnode.h b/funcnode.h
index b167e4a1..35f1969d 100644
--- a/funcnode.h
+++ b/funcnode.h
@@ -9,7 +9,7 @@
 #define MAX_DIST 10
 
 typedef ModelList<FuncInst *> func_inst_list_mt;
-typedef ModelList<Predicate *> predicate_trace_t;
+typedef ModelVector<Predicate *> predicate_trace_t;
 
 typedef HashTable<void *, FuncInst *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_inst_map_t;
 typedef HashTable<FuncInst *, uint32_t, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_id_map_t;
@@ -51,8 +51,6 @@ public:
 
 	void add_predicate_to_trace(thread_id_t tid, Predicate *pred);
 
-	uint32_t get_marker(thread_id_t tid);
-	int get_recursion_depth(thread_id_t tid);
 	uint64_t get_associated_read(thread_id_t tid, FuncInst * inst);
 
 	void add_out_edge(FuncNode * other);
@@ -71,6 +69,7 @@ private:
 
 	uint32_t inst_counter;
 	uint32_t marker;
+	uint32_t exit_count;
 	ModelVector< ModelVector<uint32_t> *> thrd_markers;
 	ModelVector<int> thrd_recursion_depth;	// Recursion depth starts from 0 to match with vector indexes.
 
@@ -119,6 +118,9 @@ private:
 	/* Keeps track of locations that may share the same value as key, deduced from val_loc_map */
 	HashTable<void *, loc_set_t *, uintptr_t, 0> * loc_may_equal_map;
 
+	HashTable<FuncInst *, bool, uintptr_t, 0, model_malloc, model_calloc, model_free> likely_null_set;
+
+	bool likely_reads_from_null(ModelAction * read);
 	// value_set_t * values_may_read_from;
 
 	/* Run-time position in the predicate tree for each thread
diff --git a/history.cc b/history.cc
index 19354d74..f82d69db 100644
--- a/history.cc
+++ b/history.cc
@@ -14,10 +14,10 @@
 /** @brief Constructor */
 ModelHistory::ModelHistory() :
 	func_counter(1),	/* function id starts with 1 */
+	last_seq_number(-1),
 	func_map(),
 	func_map_rev(),
-	func_nodes(),
-	last_action(NULL)
+	func_nodes()
 {
 	/* The following are snapshot data structures */
 	write_history = new HashTable<void *, value_set_t *, uintptr_t, 0>();
@@ -148,7 +148,7 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
 	func_node->add_inst(act);
 
 	func_node->update_tree(act);
-	last_action = act;
+	last_seq_number = act->get_seq_number();
 }
 
 /* Return the FuncNode given its func_id  */
@@ -391,10 +391,8 @@ bool ModelHistory::skip_action(ModelAction * act)
 		return true;
 
 	/* Skip actions with the same sequence number */
-	if (last_action != NULL) {
-		if (last_action->get_seq_number() == curr_seq_number)
-			return true;
-	}
+	if (last_seq_number != -1 && last_seq_number == curr_seq_number)
+		return true;
 
 	/* Skip actions that are paused by fuzzer (sequence number is 0) */
 	if (curr_seq_number == 0)
diff --git a/history.h b/history.h
index 4670a65f..2a29273f 100644
--- a/history.h
+++ b/history.h
@@ -52,6 +52,7 @@ public:
 	MEMALLOC
 private:
 	uint32_t func_counter;
+	int last_seq_number;
 
 	/* Map function names to integer ids */
 	HashTable<const char *, uint32_t, uintptr_t, 4, model_malloc, model_calloc, model_free> func_map;
@@ -72,9 +73,6 @@ private:
 
 	HashTable<void *, SnapVector<ConcretePredicate *> *, uintptr_t, 0> * loc_waiting_writes_map;
 
-	/* The last action processed by ModelHistory */
-	ModelAction * last_action;
-
 	/* thrd_func_list stores a list of function ids for each thread.
 	 * Each element in thrd_func_list stores the functions that
 	 * thread i has entered and yet to exit from