Add an exit node in predicate trees

diff --git a/funcnode.cc b/funcnode.cc
index 75cb0cb82fa1b9d4ea9e35e5f6671d0e4054f67b..d6672cb8901c4dbdb72d1db84c3f6cd1e401a53d 100644 (file)
--- 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 7e7635cae3af792249b9561c0157eb168385bb2d..0bcc73b58e2f59324e4d6aefd99d49816f6ff257 100644 (file)
--- 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 a64737e80e0dc511f93f2381583cddf207c04a86..0f7c620d5e48a471c94ad9ee3e5d070900d51712 100644 (file)
--- 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 b85eab0d0af58f2fa342991721fc03f91e244e57..fd1c768bbc3cba726260042e4e1c405688b70a0a 100644 (file)
--- 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;