SEGRegionNode.h

/*
 * SEGRegionNode.h
 *
 * Andy
 *
 * This node is to model a region.
 */
 
#ifndef IR_SEG_SEGREGIONNODE_H
#define IR_SEG_SEGREGIONNODE_H
 
#include <llvm/IR/BasicBlock.h>
#include <llvm/IR/Function.h>
#include <llvm/IR/Instructions.h>
#include <llvm/IR/Value.h>
 
#include <unordered_set>
 
#include "IR/SEG/SEGMapBase.h"
#include "IR/SEG/SymbolicExprGraph.h"
 
using namespace llvm;
 
//. This means that the region node is an iter-face region node, which uses a
// condition from other functions
class SEGRegionNode : public SEGOperandNode {
  class Clause {
  private:
    std::unordered_set<SEGNodeBase *> positive_items;
    std::unordered_set<SEGNodeBase *> negative_items;
 
  public:
    // return true if the clause is satisfiable after the change
    // return false if the clause is infeasible after the change
    bool add_positive(SEGNodeBase *);
    bool add_negative(SEGNodeBase *);
 
    // insert the constraints c into this clause
    bool and_clause(Clause *c);
 
    // result = c1 && c2
    // return true if the result is satisfiable
    // return false if the result is not satisfiable
    static bool and_clause(Clause *c1, Clause *c2, Clause *result);
 
    friend class SEGRegionNode;
    friend class SEGSerializer;
    friend class SEGHash;
  };
 
private:
  // The region is valid when value_of(cond_node) == cond is satisfied
  SEGNodeBase *cond_node;
  bool cond;
 
  bool is_always_true;
  bool is_always_false;
 
  // Cache the constraints for quick elimination of invalid/unsatisfiable
  // regions
  std::unordered_set<Clause *> constraints;
  Clause constraint;
  // SMTExpr constraint_expr;
 
  std::string dbg_str;
 
  // static SMTFactory sfty;
 
  // Set the composed constraint of a region node for fast elimination of
  // infeasible regions "is_and = true" means region1 and region2 otherwise, it
  // means region1 or region2 We compare three types of implementations
  void set_constraint_complex(SEGRegionNode *region1, SEGRegionNode *region2,
                              bool is_and);
  void set_constraint_simple(SEGRegionNode *region1, SEGRegionNode *region2,
                             bool is_and);
  void set_constraint_sat(SEGRegionNode *region1, SEGRegionNode *region2,
                          bool is_and);
  void set_constraint_baseline(SEGRegionNode *region1, SEGRegionNode *region2,
                               bool is_and);
 
  // Initialize constraint
  void set_default_constraint();
 
  // seg : the parent SEG
  // cond_node: the SEG node generating the control dependence constraint
  // cond: the condition (true/false) of cond_node for this region to be valid
  SEGRegionNode(SymbolicExprGraph *SEG, SEGNodeBase *CondNode = nullptr,
                bool Cond = false, bool fromDisk = false);
 
  friend class SymbolicExprGraph;
  friend class SEGSerializer;
  friend class SEGHash;
 
public:
  ~SEGRegionNode();
 
  // Get the cond given that the constraint for the region node is
  // "cond_node==cond"
  bool get_cond() const { return cond; }
 
  // wrapper to set constraint
  // see comments on "set_constraint_complex"
  void set_constraint(SEGRegionNode *region1, SEGRegionNode *region2,
                      bool is_and);
 
  void clear_constraint();
 
  // Get the cond_node given that the constraint for the region node is
  // "cond_node==cond"
  SEGNodeBase *get_cond_node() const { return cond_node; }
 
  // Set the debug str
  void set_dbg_str(std::string str);
 
  // get the debug str
  std::string get_dbg_str() const;
 
  // Return if the region constraint is satisfiable
  bool is_satisfiable() const;
 
  // Return if the region constraint is always satisfied
  bool is_always_satisfied() const;
 
  // Return if the region is a compound region derived from other regions
  bool is_compound() const;
 
  // Check if the region is an interface region
  // If the region is an interface region, the cond_node(condition) is from
  // another function, which may require additional treatment
  bool is_interface_region();
 
  // Return true if the regions (1st argument) and the singled region (2nd
  // argument) have contradict constraints
  static bool has_contradictory(kvec<SEGRegionNode *> &regions,
                                SEGRegionNode *additional_region = nullptr);
 
  // Dump the clauses for debugging
  void dump_clause();
 
public:
  static bool classof(const SEGObject *O) {
    return O->getKind() == SEGOBJK_Region;
  }
};
 
#endif