had a git problem, needed to clone again. Modification of the ExistHit to...

had a git problem, needed to clone again. Modification of the ExistHit to ExistHitPrev and adding a new class ACSSecurity

include/lrusecurity/features.h

-#ifndef LRUSECURITY_FEATURES_H_
-#define LRUSECURITY_FEATURES_H_
+#ifndef LRUMC_FEATURES_H_
+#define LRUMC_FEATURES_H_
+
+#include <string>
+
+#include <elm/data/Array.h>
 
 #include <otawa/proc/AbstractFeature.h>
+#include <otawa/icat3/features.h>
+
+namespace lrumc {
+
+// Exist-Hit
+extern otawa::p::feature EXIST_HIT_ANALYSIS_FEATURE;
+extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_HIT_INIT;
+extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_HIT_IN;
+
+// Exist-Miss
+extern otawa::p::feature EXIST_MISS_ANALYSIS_FEATURE;
+extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_MISS_INIT;
+extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_MISS_IN;
+
+// Definitely Unknown
+
+enum class DUCategory
+{
+	NC,
+	EH,
+	EM,
+	DU
+};
+
+extern otawa::p::feature DU_CATEGORY_FEATURE;
+extern otawa::p::id<DUCategory> DU_CATEGORY;
+
+// Model Checking Refinement Category
+enum class RefinementCategory
+{
+	CLASSIFIED,
+	AH_CANDIDATE,
+	AM_CANDIDATE,
+	AH_AM_CANDIDATE
+};
+
+extern otawa::p::feature REFINEMENT_CATEGORY_FEATURE;
+//hook: access
+extern otawa::p::id<RefinementCategory> REFINEMENT_CATEGORY;
+
+
+// MC Program Model Building
+
+class MCProgramModel;
+
+extern otawa::p::feature PROGRAM_MODEL_BUILDING_FEATURE;
+//hook: access
+extern otawa::p::id<MCProgramModel*> PROGRAM_MODEL;
+
+//hook: workspace
+extern otawa::p::id<MCProgramModel*> GLOBAL_MODEL;
+//hook: LBlockSet
+extern otawa::p::feature SET_SLICING_PROGRAM_MODEL_FEATURE;
+extern otawa::p::id<elm::AllocArray<MCProgramModel*> > SET_SLICED_PROGRAM_MODEL;
+//hook: LBlock
+extern otawa::p::feature LBLOCK_SLICING_PROGRAM_MODEL_FEATURE;
+extern otawa::p::id<elm::AllocArray<elm::AllocArray<MCProgramModel*> > > LBLOCK_SLICED_PROGRAM_MODEL;
+
+// MC Program Model Slicing
+
+enum class ProgramSlicing
+{
+	SET_SLICING,
+	CACHE_BLOCK_SLICING,
+	ACCESS_SLICING
+};
+
+extern otawa::p::id<ProgramSlicing> PROGRAM_SLICING;
+
+// MC Cache Model Building
+enum class CacheModelKind
+{
+	YOUNGER_SET,
+	YOUNGER_SET_BOUNDED_BITVECTOR,
+	YOUNGER_SET_BITVECTOR,
+	YOUNGER_SET_CLOSED_BITVECTOR,
+	MAP_BLOCK_AGE,
+	QUEUE
+};
+
+extern otawa::p::id<CacheModelKind> CACHE_MODEL_KIND;
+
+
+// Model Checking Analysis
+
+extern otawa::p::feature MODEL_CHECKING_ANALYSIS_FEATURE;
+extern otawa::p::id<elm::String> NUXMV_PATH;
+extern otawa::p::id<elm::String> NUXMV_WORKSPACE_PATH;
 
-namespace lrusecurity {
 
-extern otawa::p::feature EXAMPLE_FEATURE;
+// Classification printing
+extern otawa::p::id<bool> CLASSIFICATION_TO_FILE;
+extern otawa::p::id<elm::sys::Path> CLASSIFICATION_PATH;
 
-extern otawa::p::id< int > EXAMPLE_PROPERTY;
+} // namespace lrumc
 
-} // namespace lrusecurity
+namespace otawa
+{
+	template <> void from_string(const elm::string& s, lrumc::CacheModelKind& v);
+	template <> void from_string(const elm::string& s, lrumc::ProgramSlicing& v);
+} // namespace otawa
 
-#endif // LRUSECURITY_FEATURES_H
+#endif // LRUMC_FEATURES_H

src/ACSSecurity.h

+#ifndef LRUSECURITY_ACSSECURITY_H_
+#define LRUSECURITY_ACSSECURITY_H_
+
+#include <otawa/icache/features.h>
+#include <otawa/icat3/features.h>
+#include <otawa/basics/Bag.h>
+#include <lrusecurity/features.h>
+
+namespace lrusecurity
+public class ACSSecurity : class otawa::icat3::ACS
+{
+ public:
+  otawa::Bag<icache::Access> _prev;
+}
+
+#endif //LRUSECURITY_ACSSECURITY_H

src/Prev/ExistHitPrevAdapter.h

+#ifndef LRUSECURITY_EXIST_HIT_PREV_ADAPTER_H_
+#define LRUSECURITY_EXIST_HIT_PREV_ADAPTER_H_
+
+#include <otawa/ai/ArrayStore.h>
+#include <otawa/icat3/features.h>
+#include <otawa/cfg/CompositeCFG.h>
+#include <otawa/cfg/features.h>
+
+#include <lrupreanalysis/features.h>
+
+#include "ExistHitPrevDomain.h"
+
+namespace lrusecurity
+{
+
+class ExistHitPrevAdapter
+{
+public:
+	using domain_t = ExistHitPrevDomain;
+	using t = typename domain_t::t;
+	using graph_t = otawa::CompositeCFG;
+	using store_t = otawa::ai::ArrayStore<domain_t, graph_t>;
+
+	ExistHitPrevAdapter(int set, const t* init, const otawa::icat3::LBlockCollection& coll, const otawa::CFGCollection& cfgs, otawa::WorkSpace* ws);
+
+	inline domain_t& domain(void) { return _domain; }
+	inline graph_t& graph(void) { return _graph; }
+	inline store_t& store(void) { return _store; }
+
+	void update(const otawa::Bag<otawa::icache::Access>& accs, t& d);
+	void update(otawa::Block *v, t& d);
+
+private:
+	lrupreanalysis::ACSManager _mustManager;
+	domain_t _domain;
+	graph_t _graph;
+	store_t _store;
+};
+
+} // namespace lrusecurity
+
+#endif // LRUSECURITY_EXIST_HIT_ADAPTER_H_

src/Prev/ExistHitPrevAnalysis.h

+#ifndef LRUMC_EXIST_HIT_ANALYSIS_H_
+#define LRUMC_EXIST_HIT_ANALYSIS_H_
+
+#include <otawa/proc/Processor.h>
+#include <otawa/icat3/features.h>
+#include <otawa/cfg/features.h>
+
+namespace lrumc
+{
+
+class ExistHitAnalysis: public otawa::Processor
+{
+public:
+	static otawa::p::declare reg;
+	ExistHitAnalysis(otawa::p::declare& r = reg);
+
+protected:
+
+	void configure(const otawa::PropList& props) override;
+	void setup(otawa::WorkSpace* ws) override;
+	void processWorkSpace(otawa::WorkSpace* ws) override;
+	void destroy(otawa::WorkSpace* ws) override;
+
+private:
+	void processSet(int i, otawa::WorkSpace* ws);
+
+	const otawa::icat3::Container<otawa::icat3::ACS>* _initExistHit;
+	const otawa::icat3::LBlockCollection* _coll;
+	const otawa::CFGCollection* _cfgs;
+};
+
+/**
+ * Perform the ACS analysis for the Exist-Hit domain. For cache block, it associates an upper bound on block age that holds on at least on path
+ * @par Properties
+ * @li @ref EXIST_HIT_IN
+ *
+ * @par Configuraiton
+ * @li @ref EXIST_HIT_INIT
+ *
+ * @par Implementation
+ * @li @ref ExistHitAnalysis
+ *
+ * @ingroup lrumc
+ */
+extern otawa::p::feature EXIST_HIT_ANALYSIS_FEATURE;
+
+/**
+ * ACS for the Exist-Hit analysis at the entry of the corresponding block or edge.
+ *
+ * @par Feature
+ * @li @ref EXIST_HIT_ANALYSIS_FEATURE
+ *
+ * @par Hooks
+ * @li @ref Block
+ * @li @ref Edge
+ *
+ * @ingroup lrumc
+ */
+extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_HIT_IN;
+
+
+/**
+ * Initial state for Exist-Miss instruction cache analysis.
+ *
+ * @par Hook
+ * @li Feature configuration.
+ *
+ * @par Feature
+ * @li @ref EXIST_HIT_ANALYSIS_FEATURE
+ *
+ * @ingroup lrumc
+ */
+extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_HIT_INIT;
+
+}; // namespace lrumc
+
+#endif // LRUMC_EXIST_HIT_ANALYSIS_H_

src/Prev/ExistHitPrevDomain.h

+#ifndef LRUSECURITY_EXIST_HIT_DOMAIN_H_
+#define LRUSECURITY_EXIST_HIT_DOMAIN_H_
+
+#include <otawa/icat3/features.h>
+#include <otawa/icache/features.h>
+#include <elm/io/Output.h>
+
+#include <lrupreanalysis/features.h>
+#include "ACSSecurity.h"
+namespace lrusecurity
+{
+
+class ExistHitDomain {
+public:
+	using t = ACSSecurity;
+
+	ExistHitDomain(const otawa::icat3::LBlockCollection& coll, int set, const t* init);
+	inline const t& bot(void) const { return _bot; }
+	inline const t& top(void) const { return _top; }
+	inline const t& init(void) const { return _init; }
+	inline void print(const t& a, otawa::io::Output& out) const { a.print(_set, _coll, out); }
+	inline elm::io::Printable<t, ExistHitDomain> print(const t& a) const { return elm::io::p(a, *this); }
+	inline bool contains(const t& a, int i) { return(a[i] != otawa::icat3::BOT_AGE); }
+	inline void copy(t& d, const t& s) { d.copy(s); }
+	bool equals(const t& a, const t& b) const;
+	void join(t& d, const t& s);
+	void fetch(t& a, const otawa::icat3::LBlock *lb, lrupreanalysis::ACSManager& mustManager);
+	void update(const otawa::icache::Access& access, t& a, lrupreanalysis::ACSManager& mustManager);
+
+private:
+	int _n;
+	t _bot, _top;
+	otawa::hard::Cache::set_t _set;
+	const otawa::icat3::LBlockCollection& _coll;
+	int _A;
+	const t& _init;
+	t _tmp;
+};
+
+} // namespace lrusecurity
+
+#endif // LRUSECURITY_EXIST_HIT_DOMAIN_H_

src/Prev/lrusecurity_ExistHitPrevAdapter.cpp

+#include "ExistHitAdapter.h"
+
+using namespace otawa;
+
+namespace lrusecurity
+{
+
+ExistHitAdapter::ExistHitAdapter(
+		int set,
+		const t* init,
+		const icat3::LBlockCollection& coll,
+		const CFGCollection& cfgs,
+		otawa::WorkSpace* ws) :
+	_mustManager(ws),
+	_domain(coll, set, init),
+	_graph(cfgs),
+	_store(_domain, _graph)
+{
+}
+
+void ExistHitAdapter::update(const Bag<icache::Access>& accs, t& d)
+{
+	for(int i = 0; i < accs.count(); i++) {
+		_domain.update(accs[i], d, _mustManager);
+		_mustManager.update(accs[i]);
+	}
+}
+
+void ExistHitAdapter::update(Block *v, t& d)
+{
+	_domain.copy(d, _domain.bot());
+	t s;
+
+	// update and join along edges
+	for(auto e = _graph.preds(v); e; e++) {
+		Block *w = e->source();
+		_domain.copy(s, _store.get(w));
+
+		_mustManager.start(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
+		_domain.join(d, s);
+	}
+}
+
+} // namespace lrusecurity

src/Prev/lrusecurity_ExistHitPrevAnalysis.cpp

+#include "ExistHitPrevAnalysis.h"
+
+#include <chrono>
+
+#include <otawa/ai/ArrayStore.h>
+#include <otawa/ai/SimpleAI.h>
+#include <otawa/icache/features.h>
+#include <otawa/icat3/features.h>
+
+#include <lrusecurity/features.h>
+
+#include "ExistHitPrevAdapter.h"
+#include "ExistHitPrevDomain.h"
+
+using namespace otawa;
+
+namespace lrusecurity
+{
+
+ExistHitPrevAnalysis::ExistHitPrevAnalysis(p::declare& r) :
+		Processor(r),
+		_initExistHitPrev(nullptr),
+		_coll(nullptr),
+		_cfgs(nullptr)
+{
+}
+
+void ExistHitPrevAnalysis::configure(const PropList& props)
+{
+	Processor::configure(props);
+	if(props.hasProp(EXIST_HIT_INIT))
+		_initExistHitPrev = &EXIST_HIT_INIT(props);
+}
+
+void ExistHitPrevAnalysis::setup(WorkSpace* ws)
+{
+	_coll = icat3::LBLOCKS(ws);
+	ASSERT(_coll != nullptr);
+	_cfgs = INVOLVED_CFGS(ws);
+	ASSERT(_cfgs != nullptr);
+}
+
+  void ExistHitPrevAnalysis::processWorkSpace(WorkSpace* ws) //changer les ACS en ACSSecurity
+{
+	auto start = std::chrono::system_clock::now();
+
+	// prepare containers
+	for(CFGCollection::BlockIter b(_cfgs); b; b++)
+		(*EXIST_HIT_IN(b)).configure(*_coll);
+
+	// compute ACS
+	for(int i = 0; i < _coll->cache()->setCount(); i++) {
+		if((*_coll)[i].count()) {
+			if(logFor(LOG_FUN))
+				log << "\tanalyzing set " << i << io::endl;
+			processSet(i, ws);
+		}
+	}
+
+	auto end = std::chrono::system_clock::now();
+	auto elapsed = std::chrono::duration_cast<std::chrono::seconds>(end - start);
+	if(logFor(LOG_FUN))
+		log << "\tExist Hit Analysis running time: " << elapsed.count() << " s" << io::endl;
+}
+
+void ExistHitPrevAnalysis::destroy(WorkSpace*)
+{
+	for(CFGCollection::BlockIter b(_cfgs); b; b++)
+		EXIST_HIT_IN(b).remove();
+}
+
+void ExistHitPrevAnalysis::processSet(int set, WorkSpace* ws)
+{
+	// perform the analysis
+	ExistHitPrevAdapter ada(set, _initExistHitPrev ? &_initExistHitPrev->get(set) : nullptr, *_coll, *_cfgs, ws);
+	ai::SimpleAI<ExistHitPrevAdapter> ana(ada);
+	ana.run();
+
+	// store the results
+	for(CFGCollection::BlockIter b(_cfgs); b; b++)
+		if(b->isBasic()) {
+			ada.domain().copy((*EXIST_HIT_IN(b))[set], ada.store().get(b));
+			if(logFor(LOG_BLOCK))
+				log << "\t\t\t" << *b << ": " << ada.domain().print(ada.store().get(b)) << io::endl;
+		}
+}
+
+p::declare ExistHitPrevAnalysis::reg = p::init("lrusecurity::ExistHitPrevAnalysis", Version(1, 0, 0))
+	.require(icat3::LBLOCKS_FEATURE)
+	.require(COLLECTED_CFG_FEATURE)
+	.require(icat3::MUST_PERS_ANALYSIS_FEATURE)
+	.require(icat3::CATEGORY_FEATURE)
+	.provide(EXIST_HIT_ANALYSIS_FEATURE)
+	.make<ExistHitPrevAnalysis>();
+
+p::feature EXIST_HIT_ANALYSIS_FEATURE("lrusecurity::EXIST_HIT_ANALYSIS_FEATURE", p::make<ExistHitPrevAnalysis>());
+
+p::id<icat3::Container<icat3::ACS> > EXIST_HIT_IN("lrusecurity::EXIST_HIT_IN");
+
+p::id<icat3::Container<icat3::ACS> > EXIST_HIT_INIT("lrusecurity::EXIST_HIT_INIT");
+
+}; // namespace lrusecurity

src/Prev/lrusecurity_ExistHitPrevDomain.cpp

+#include "ExistHitPrevDomain.h"
+
+using namespace otawa;
+
+namespace lrusecurity
+{
+
+ExistHitPrevDomain::ExistHitPrevDomain(
+		const icat3::LBlockCollection& coll,
+		int set,
+		const t *init) :
+	_n(coll[set].count()),
+	_bot(_n, icat3::BOT_AGE),
+	_top(_n, 0),
+	_set(set),
+	_coll(coll),
+	_A(coll.A()),
+	_init(init ? *init : _top),
+	_tmp(_n)
+{
+}
+
+bool ExistHitPrevDomain::equals(const t& a, const t& b) const
+{
+	for(int i = 0; i < _n; i++)
+		if(a[i] != b[i])
+			return false;
+
+	return true;
+}
+void ExistHitPrevDomain::join(t& d, const t& s)
+{
+	for(int i = 0; i < _n; i++) {
+		// d[i] = min(d[i], s[i])
+		if(d[i] == icat3::BOT_AGE)
+			d[i] = s[i];
+		else if(s[i] != icat3::BOT_AGE)
+			d[i] = min(d[i], s[i]);
+
+	}
+
+	//join of the Prev is a union
+	d._prev = d._prev << s._prev;
+}
+
+void ExistHitPrevDomain::fetch(t& a, const icat3::Access ac, lrupreanalysis::ACSManager& mustManager)
+{
+        icat3::LBlock *lb = icat3::LBLOCK(ac);
+	int b = lb->index();
+
+	if(a[0] == icat3::BOT_AGE)
+		return;
+
+	for(int i = 0; i < _n; i++) {
+		ASSERT(a[i] != icat3::BOT_AGE);
+		if(i == b)
+			continue;
+
+		if(a[i] < mustManager.mustAge(lb) && a[i] < _A)
+			a[i]++;
+	}
+	a[b] = 0;
+
+	//Updating prev
+	for(int i = 0; i < _n; i++) {
+	  if (a[i] == icat3::BOT_AGE)
+	    a._prev = otawa::Bag<icache::Access>::Bag();
+
+	  if (i == b)
+	    a._prev = otawa::Bag<icache::Access>::Bag(1, &ac);
+	}
+}
+
+void ExistHitPrevDomain::update(const icache::Access& access, t& a, lrupreanalysis::ACSManager& mustManager)
+{
+	switch(access.kind()) {
+
+	case icache::FETCH:
+		if(_coll.cache()->set(access.address()) == _set)
+			fetch(a, icat3::LBLOCK(access), mustManager);
+		break;
+
+	case icache::PREFETCH:
+		if(_coll.cache()->set(access.address()) == _set) {
+			copy(_tmp, a);
+			fetch(a, icat3::LBLOCK(access), mustManager);
+			join(a, _tmp);
+		}
+		break;
+
+	case icache::NONE:
+		break;
+
+	default:
+		ASSERT(false);
+	}
+}
+
+} // namespace lrusecurity

src/lrusecurity.cpp

-#include <otawa/proc/ProcessorPlugin.h>
-
-namespace lrusecurity {
-
-using namespace elm;
-using namespace otawa;
-
-class Plugin: public ProcessorPlugin {
-public:
-	Plugin(void): ProcessorPlugin("lrusecurity", Version(1, 0, 0), OTAWA_PROC_VERSION) { }
-};
-
-} // namespace lrusecurity
-
-lrusecurity::Plugin lrusecurity_plugin;
-ELM_PLUGIN(lrusecurity_plugin, OTAWA_PROC_HOOK);
-