/*
 *	icat3::MayAnalysis class implementation
 *	Copyright (c) 2017, IRIT UPS.
 *
 *	This file is part of OTAWA
 *
 *	OTAWA is free software; you can redistribute it and/or modify
 *	it under the terms of the GNU General Public License as published by
 *	the Free Software Foundation; either version 2 of the License, or
 *	(at your option) any later version.
 *
 *	OTAWA is distributed in the hope that it will be useful,
 *	but WITHOUT ANY WARRANTY; without even the implied warranty of
 *	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *	GNU General Public License for more details.
 *
 *	You should have received a copy of the GNU General Public License
 *	along with OTAWA; if not, write to the Free Software
 *	Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
 *	02110-1301  USA
 */

#include <chrono>
#include <otawa/ai/ArrayStore.h>
#include <otawa/ai/SimpleAI.h>
#include <otawa/cfg/CompositeCFG.h>
#include <otawa/cfg/features.h>
#include <otawa/icache/features.h>
#include <otawa/icat3/features.h>
#include <lruzdd/features.h>
#include <lruzdd/MayAnalysis/MayManager.h>
#include <lruexact/features.h>
#include "../ZDD/MayAbstractValuePolicy.h"
#include "../ZDD/ZDDMayDomainPolicy.h"
#include "../GeneratorsSet/GSMayAbstractValuePolicy.h"
#include "../GeneratorsSet/GSMayDomainPolicy.h"

#include "../Domain.h"

using namespace otawa;

namespace lruzdd
{

class MayAdapter
{
public:
	typedef Domain<ZDDMayDomainPolicy> domain_t;
	//typedef Domain<GSMayDomainPolicy> domain_t;
	typedef typename domain_t::t t;
	typedef CompositeCFG graph_t;
	typedef ai::ArrayStore<domain_t, graph_t> store_t;

	MayAdapter(const otawa::icat3::LBlock* focus,
	           int set,
	           const t* init,
	           const icat3::LBlockCollection& coll,
	           const CFGCollection& cfgs):
		m_domain(focus, coll, set, init),
		m_graph(cfgs),
		m_store(m_domain, m_graph) { }

	inline domain_t& domain(void) { return m_domain; }
	inline graph_t& graph(void) { return m_graph; }
	inline store_t& store(void) { return m_store; }

	void update(const Bag<icache::Access>& accs, t& d) {
		for(auto acc = *accs; acc; acc++)
			m_domain.update(acc, d);
	}

	void update(Block* v, t& d) {
		// ∀v ∈ V \ {ν}, IN(v) = ⊔{(w, v) ∈ E} 𝕀*(β(w, v), (v, w), IN(w))
		m_domain.copy(d, m_domain.bot());
		t s;

		// update and join along edges
		for(auto e = m_graph.preds(v); e; e++) {
			Block *w = e->source();
			m_domain.copy(s, m_store.get(w));

			// apply block
			{
				const Bag<icache::Access>& accs = icache::ACCESSES(w);
				if(accs.count() > 0)
					update(accs, s);
			}

			// apply edge
			{
				const Bag<icache::Access>& accs = icache::ACCESSES(e);
				if(accs.count() > 0)
					update(accs, s);
			}

			// merge result
			m_domain.join(d, s);
		}
	}

private:
	domain_t m_domain;
	graph_t m_graph;
	store_t m_store;
};


class MayAnalysis : public Processor
{
public:
	//using domain_t = Domain<ZDDMayDomainPolicy>;
	//using domain_t = Domain<GSMayDomainPolicy>;
	using domain_t = MayAdapter::domain_t;

	static p::declare reg;
	MayAnalysis(p::declare& r = reg) :
		Processor(r),
		//m_init_exact_may(nullptr),
		m_coll(nullptr),
		m_cfgs(nullptr)
	{
	}

protected:

	void configure(const PropList& props) override
	{
		Processor::configure(props);
//		if(props.hasProp(EXACT_MAY_INIT))
//			m_init_exact_may = &EXACT_MAY_INIT(props);
	}

	void setup(WorkSpace *ws) override
	{
		m_coll = icat3::LBLOCKS(ws);
		ASSERT(m_coll != nullptr);
		m_cfgs = otawa::INVOLVED_CFGS(ws);
		ASSERT(m_cfgs != nullptr);
//		for(CFGCollection::BlockIter b(m_cfgs); b; b++)
//			EXACT_MAY_IN(b) = Container<YoungerSetAntichain<AntichainType::MAY> >(*m_coll);
	}

	void processWorkSpace(WorkSpace*) override
	{
		auto start = std::chrono::system_clock::now();

		std::set<const icat3::LBlock*> toRefine;
		for(CFGCollection::BlockIter b(m_cfgs); b; b++) {
			if(!b->isBasic())
				continue;

			BasicBlock* bb = b->toBasic();

			for(Block::EdgeIter edgeIter(bb->ins()); edgeIter; ++edgeIter) {
				Edge* e = *edgeIter;
				Bag<icache::Access>& bag = icache::ACCESSES(e).ref();
				processBag(toRefine, bag);
			}
			Bag<icache::Access>& bag = icache::ACCESSES(bb).ref();
			processBag(toRefine, bag);
		}

		for(const icat3::LBlock* lb : toRefine)
			processLBlock(lb);

		auto end = std::chrono::system_clock::now();
		auto elapsed = std::chrono::duration_cast<std::chrono::seconds>(end - start);
		if(logFor(LOG_FUN))
			log << "\tExact May Analysis running time: " << elapsed.count() << " s" << io::endl;

//		for(int i = 0; i < m_coll->size(); ++i) {
//			const icat3::LBlockSet& s = (*m_coll)[i];
//			for(int j = 0; j < s.size(); ++j)
//				processLBlock(s[j]);
//		}
	}

	void destroy(WorkSpace*) override
	{
//		for(CFGCollection::BlockIter b(m_cfgs); b; b++)
//			EXACT_MAY_IN(b).remove();
	}

private:
	void processBag(std::set<const icat3::LBlock*>& set, Bag<icache::Access>& bag)
	{
		for(int i = 0; i < bag.size(); ++i) {
			lruexact::RefinementCategory refCat = lruexact::REFINEMENT_CATEGORY(bag[i]);
			MissCategory e = MissCategory::NC;

			if(refCat == lruexact::RefinementCategory::CLASSIFIED &&
			   icat3::CATEGORY(bag[i]) == icat3::AM)
					e = MissCategory::AM;

			MISS_CATEGORY(bag[i]) = e;

			if(refCat == lruexact::RefinementCategory::AM_CANDIDATE ||
			   refCat == lruexact::RefinementCategory::AH_AM_CANDIDATE)
			set.insert(icat3::LBLOCK(&bag[i]));
		}
	}

	void processLBlock(const icat3::LBlock* lb)
	{
		if(logFor(LOG_BLOCK))
			log << "\tAnalyzing Block " << lb->index() << " (" << lb->address() << ")" << io::endl;

		MayAdapter ada(lb, lb->set(), nullptr, *m_coll, *m_cfgs);
		ai::SimpleAI<MayAdapter> ana(ada);
		ana.run();

		for(CFGCollection::BlockIter b(m_cfgs); b; b++)
			classifyBlock(lb, ada.domain(), b, ada.store().get(b));

		ada.store().clear();
	}

	void classifyBlock(const icat3::LBlock* focus,
	                   MayAdapter::domain_t& d,
	                   Block* b,
	                   const MayAdapter::t& v)
	{
		MayManager<domain_t> man(d, v);

		Bag<icache::Access>& bAccs = icache::ACCESSES(b).ref();
		MayAdapter::t save = classifyAccesses(b, focus, man, bAccs);
		for(Block::EdgeIter e = b->outs(); e; e++) {
			Bag<icache::Access>& eAccs = icache::ACCESSES(e).ref();
			man.restart(save);
			classifyAccesses(b, focus, man, eAccs);
		}
	}

	MayAdapter::t classifyAccesses(const Block* b,
	                               const icat3::LBlock* focus,
	                               MayManager<domain_t>& man,
	                               Bag<icache::Access>& accs)
	{
		for(int i = 0; i < accs.size(); ++i) {
			icat3::LBlock* lb = icat3::LBLOCK(accs[i]);
			if(lb == focus)  {
//				if(logFor(LOG_BLOCK)) {
//					log << "\t\tFunction " << b->cfg()->label() << ", ";
//					log << const_cast<Block*>(b) << ": " << io::endl;
//					log << "\t\t\tAccess (" << accs[i] << ") is ";
//				}
				if(man.alwaysMiss()) {
					MISS_CATEGORY(accs[i]) = MissCategory::AM;
//					if(logFor(LOG_BLOCK))
//						log << "AM" << elm::io::endl;
				}
				else {
					MISS_CATEGORY(accs[i]) = MissCategory::NC;
//					if(logFor(LOG_BLOCK))
//						log << "NC" << elm::io::endl;
				}
			}
			man.update(accs[i]);
		}
		return man.current();
	}

	//const Container<YoungerSetAntichain<AntichainType::MAY> >* m_init_exact_may;
	const icat3::LBlockCollection* m_coll;
	const CFGCollection* m_cfgs;
};

p::declare MayAnalysis::reg = p::init("lruzdd::MayAnalysis", Version(1, 0, 0))
	.require(icat3::LBLOCKS_FEATURE)
	.require(lruexact::REFINEMENT_CATEGORY_FEATURE)
	.require(COLLECTED_CFG_FEATURE)
	.provide(EXACT_MAY_ANALYSIS_FEATURE)
	.make<MayAnalysis>();


/**
 * Perform the ACS analysis for the Exact-May domain, that is, computes for each cache
 * block the highest age it may have considering all execution paths.
 *
 * @par Properties
 * @li @ref EXACT_MAY_IN
 *
 * @par Configuraiton
 * @li @ref EXACT_MAY_INIT
 *
 * @par Implementation
 * @li @ref ExactMayAnalysis
 *
 * @ingroup lruzdd
 */
p::feature EXACT_MAY_ANALYSIS_FEATURE("lruzdd::EXACT_MAY_ANALYSIS_FEATURE", p::make<MayAnalysis>());


/**
 * ACS for the Exact-May analysis at the entry of the corresponding block or edge.
 *
 * @par Feature
 * @li @ref EXACT_MAY_ANALYSIS_FEATURE
 *
 * @par Hooks
 * @li @ref Block
 * @li @ref Edge
 *
 * @ingroup lruzdd
 */
//p::id<Container<YoungerSetAntichain<AntichainType::MAY> > > EXACT_MAY_IN("lruzdd::EXACT_MAY_IN");

p::id<MissCategory> MISS_CATEGORY("lruzdd::MISS_CATEGORY");

/**
 * Initial state for Exact-May instruction cache analysis.
 *
 * @par Hook
 * @li Feature configuration.
 *
 * @par Feature
 * @li @ref EXACT_MAY_ANALYSIS_FEATURE
 *
 * @ingroup lruzdd
 */
//p::id<Container<YoungerSetAntichain<AntichainType::MAY> > > EXACT_MAY_INIT("lruzdd::EXACT_MAY_INIT");

} // namespace lruzdd