#ifndef BOUND_FACTS_CALCULATOR_H
#define BOUND_FACTS_CALCULATOR_H

#include "ThunkData.h"
#include "BoundFactData.h"
#include "CFG.h"
#include "SymbolicExpression.h"
#include "slicing.h"

#include <unordered_set>
#include <unordered_map>

using namespace Dyninst;
using namespace Dyninst::ParseAPI;

// To avoid the bound fact calculation from deadlock
#define IN_QUEUE_LIMIT 10



class BoundFactsCalculator {
    BoundFactsType boundFactsIn, boundFactsOut;
    ParseAPI::Function *func;
    GraphPtr slice;
    bool firstBlock;
    bool handleOneByteRead;
    SymbolicExpression &se;

    void ThunkBound(BoundFact*& curFact, Node::Ptr src, Node::Ptr trg, bool &newCopy);
    BoundFact* Meet(Node::Ptr curNode);
    void CalcTransferFunction(Node::Ptr curNode, BoundFact *newFact);

    std::unordered_map<Node::Ptr, int, Node::NodePtrHasher> analysisOrder, nodeColor;
    vector<Node::Ptr> reverseOrder;
    int orderStamp;
    
    void DetermineAnalysisOrder();
    void NaturalDFS(Node::Ptr);
    void ReverseDFS(Node::Ptr);
    bool HasIncomingEdgesFromLowerLevel(int curOrder, std::vector<Node::Ptr>& curNodes);

public:
    bool CalculateBoundedFacts(); 

    BoundFactsCalculator(ParseAPI::Function *f, 
                         GraphPtr s, 
			 bool first, 
			 bool oneByteRead,
			 SymbolicExpression &sym):
        func(f), slice(s), firstBlock(first), handleOneByteRead(oneByteRead), se(sym) {}

    BoundFact *GetBoundFactIn(Node::Ptr node);
    BoundFact *GetBoundFactOut(Node::Ptr node);
    ~BoundFactsCalculator();
};

#endif
