From: weiyu <weiyuluo1232@gmail.com>
Date: Fri, 11 Oct 2019 23:09:13 +0000 (-0700)
Subject: Add an exit node in predicate trees
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=c80409d09fd1c97f798b5952a113c463b9b36805

Add an exit node in predicate trees
---

diff --git a/funcnode.cc b/funcnode.cc
index 75cb0cb8..d6672cb8 100644
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -20,6 +20,7 @@ FuncNode::FuncNode(ModelHistory * history) :
 {
 	predicate_tree_entry = new Predicate(NULL, true);
 	predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
+	predicate_tree_exit = new Predicate(NULL, false, true);
 
 	// Memories that are reclaimed after each execution
 	action_list_buffer = new SnapList<action_list_t *>();
@@ -281,7 +282,6 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 
 				curr_pred->add_backedge(back_pred);
 				curr_pred = back_pred;
-
 				continue;
 			}
 		}
@@ -308,6 +308,8 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 		it = it->getNext();
 		curr_pred->incr_count();
 	}
+
+	curr_pred->set_exit(predicate_tree_exit);
 }
 
 /* Given curr_pred and next_inst, find the branch following curr_pred that
@@ -696,6 +698,7 @@ void FuncNode::print_predicate_tree()
 {
 	model_print("digraph function_%s {\n", func_name);
 	predicate_tree_entry->print_pred_subtree();
+	predicate_tree_exit->print_predicate();
 	model_print("}\n");	// end of graph
 }
 
diff --git a/funcnode.h b/funcnode.h
index 7e7635ca..0bcc73b5 100644
--- a/funcnode.h
+++ b/funcnode.h
@@ -67,7 +67,9 @@ private:
 	uint32_t func_id;
 	const char * func_name;
 	ModelHistory * history;
-	Predicate * predicate_tree_entry;	// a dummy node whose children are the real entries
+	Predicate * predicate_tree_entry;	// A dummy node whose children are the real entries
+	Predicate * predicate_tree_exit;	// A dummy node
+
 
 	uint32_t exit_count;
 	uint32_t marker;
diff --git a/predicate.cc b/predicate.cc
index a64737e8..0f7c620d 100644
--- a/predicate.cc
+++ b/predicate.cc
@@ -2,14 +2,16 @@
 #include "predicate.h"
 #include "concretepredicate.h"
 
-Predicate::Predicate(FuncInst * func_inst, bool is_entry) :
+Predicate::Predicate(FuncInst * func_inst, bool is_entry, bool is_exit) :
 	func_inst(func_inst),
 	entry_predicate(is_entry),
+	exit_predicate(is_exit),
 	does_write(false),
 	exploration_count(0),
 	pred_expressions(16),
 	children(),
 	parent(NULL),
+	exit(NULL),
 	backedges(16)
 {}
 
@@ -102,6 +104,11 @@ void Predicate::print_predicate()
 		return;
 	}
 
+	if (exit_predicate) {
+		model_print("exit node\"];\n");
+		return;
+	}
+
 	func_inst->print();
 
 	PredExprSetIter * it = pred_expressions.iterator();
@@ -148,4 +155,8 @@ void Predicate::print_pred_subtree()
 		Predicate * backedge = it->next();
 		model_print("\"%p\" -> \"%p\"[style=dashed, color=grey]\n", this, backedge);
 	}
+
+	if (exit) {
+		model_print("\"%p\" -> \"%p\"[style=dashed, color=red]\n", this, exit);
+	}
 }
diff --git a/predicate.h b/predicate.h
index b85eab0d..fd1c768b 100644
--- a/predicate.h
+++ b/predicate.h
@@ -12,7 +12,7 @@ typedef HSIterator<struct pred_expr *, uintptr_t, 0, model_malloc, model_calloc,
 
 class Predicate {
 public:
-	Predicate(FuncInst * func_inst, bool is_entry = false);
+	Predicate(FuncInst * func_inst, bool is_entry = false, bool is_exit = false);
 	~Predicate();
 
 	FuncInst * get_func_inst() { return func_inst; }
@@ -21,11 +21,13 @@ public:
 	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_exit(Predicate * exit_pred) { exit = exit_pred; }
 	void add_backedge(Predicate * back_pred) { backedges.add(back_pred); }
 	void copy_predicate_expr(Predicate * other);
 
 	ModelVector<Predicate *> * get_children() { return &children; }
 	Predicate * get_parent() { return parent; }
+	Predicate * get_exit() { return exit; }
 	PredSet * get_backedges() { return &backedges; }
 
 	bool is_entry_predicate() { return entry_predicate; }
@@ -47,6 +49,7 @@ public:
 private:
 	FuncInst * func_inst;
 	bool entry_predicate;
+	bool exit_predicate;
 	bool does_write;
 	uint32_t exploration_count;
 
@@ -56,6 +59,7 @@ private:
 
 	/* Only a single parent may exist */
 	Predicate * parent;
+	Predicate * exit;
 
 	/* May have multiple back edges, e.g. nested loops */
 	PredSet backedges;