Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 9a24ed1c authored by Valentin Touzeau's avatar Valentin Touzeau Committed by Valentin Touzeau
Browse files

Copy form lrumc

parent fe6791b8
CMAKE_MINIMUM_REQUIRED(VERSION 2.6)
# configuration
set(PLUGIN "lrumc") # plugin name
set(PLUGIN "exactlru") # plugin name
set(NAMESPACE "") # namespace
set(SOURCES "src/lrumc/lrumc.cpp"
"src/lrumc/MC/lrumc_MCProgramModelBuilding.cpp"
"src/lrumc/MC/lrumc_MCProgramModelSlicing.cpp"
"src/lrumc/MC/lrumc_MCProgramModelNode.cpp"
"src/lrumc/MC/lrumc_MCProgramModel.cpp"
"src/lrumc/MC/lrumc_MCCacheModel.cpp"
"src/lrumc/MC/lrumc_MCException.cpp"
"src/lrumc/MC/lrumc_MCNuxmvCommand.cpp"
"src/lrumc/MC/lrumc_MCInstance.cpp"
"src/lrumc/MC/lrumc_MCAnalysis.cpp"
"src/lrumc/MC/lrumc_MCQueryManager.cpp"
"src/lrumc/EM/lrumc_ExistMissDomain.cpp"
"src/lrumc/EM/lrumc_ExistMissAdapter.cpp"
"src/lrumc/EM/lrumc_ExistMissAnalysis.cpp"
"src/lrumc/EH/lrumc_ExistHitDomain.cpp"
"src/lrumc/EH/lrumc_ExistHitAdapter.cpp"
"src/lrumc/EH/lrumc_ExistHitAnalysis.cpp"
"src/lrumc/lrumc_ACSManager.cpp"
"src/lrumc/lrumc_DUCatBuilder.cpp"
set(SOURCES "src/exactlru.cpp"
"src/Generator.cpp"
"src/MayAnalysis/MayDomain.cpp"
"src/MayAnalysis/MayGeneratorsAntichain.cpp"
"src/MayAnalysis/MayAnalysis.cpp"
"src/MustAnalysis/MustDomain.cpp"
"src/MustAnalysis/MustGeneratorsAntichain.cpp"
"src/MustAnalysis/MustAnalysis.cpp"
"src/ClassificationBuilder.cpp"
)
# script
project(${PLUGIN})
......@@ -45,8 +35,8 @@ set(ORIGIN $ORIGIN)
include_directories("${CMAKE_SOURCE_DIR}" "include")
add_library(${PLUGIN} SHARED ${SOURCES})
set_property(TARGET ${PLUGIN} PROPERTY PREFIX "")
set_property(TARGET ${PLUGIN} PROPERTY COMPILE_FLAGS "${OTAWA_CFLAGS} --std=c++11 -g -Wall -Wextra")
target_link_libraries(${PLUGIN} "${OTAWA_LDFLAGS}")
set_property(TARGET ${PLUGIN} PROPERTY COMPILE_FLAGS "${OTAWA_CFLAGS} --std=c++11 -g -Wall -Wextra -pedantic")
target_link_libraries(${PLUGIN} PRIVATE cudd epd extra)
# installation
set(PLUGIN_PATH "${OTAWA_PREFIX}/lib/otawa/${NAMESPACE}")
......
[elm-plugin]
name=exactlru
deps=otawa/icat3;otawalru
description=Perform an exact May/Must analysis of L1 I cache
author=Valentin Touzeau
#ifndef EXACTLRU_CACHESTATE_H
#define EXACTLRU_CACHESTATE_H
#include <elm/io/Output.h>
#include <otawa/icat3/features.h>
#include <otawa/icache/features.h>
#include <exactlru/ExactMust/ExactMustDomain.h>
#include <exactlru/ExactMay/ExactMayDomain.h>
namespace exactlru
{
class CacheState {
public:
CacheState(const otawa::icat3::LBlock* focus,
const otawa::icat3::LBlockCollection& coll,
int set,
typename ExactMustDomain::t& initMustState,
typename ExactMayDomain::t& initMayState) :
m_focus(focus),
m_coll(coll),
m_mustDom(focus, coll, set, nullptr),
m_mayDom(focus, coll, set, nullptr),
m_mustState(initMustState),
m_mayState(initMayState)
{ }
void update(const otawa::icache::Access& acc)
{
m_mustDom.update(acc, m_mustState);
m_mayDom.update(acc, m_mayState);
}
otawa::icat3::category_t classify()
{
bool ah = m_mustState.alwaysHit(m_coll.A(), m_focus);
bool am = m_mayState.alwaysMiss(m_coll.A(), m_focus);
ASSERT(!am || !ah || "Classification cannot be AH and AM for the same access");
if(ah)
return otawa::icat3::AH;
else if(am)
return otawa::icat3::AM;
else
return otawa::icat3::NC;
}
private:
const otawa::icat3::LBlock* m_focus;
const otawa::icat3::LBlockCollection& m_coll;
ExactMustDomain m_mustDom;
ExactMayDomain m_mayDom;
typename ExactMustDomain::t m_mustState;
typename ExactMayDomain::t m_mayState;
};
} // namespace exactlru
#endif // EXACTLRU_CACHESTATE_H
#ifndef GENERATORS_H
#define GENERATORS_H
#include <set>
#include <otawa/icat3/features.h>
namespace exactlru
{
class LexicalOrder;
class Generator
{
public:
friend class LexicalOrder;
using Block = otawa::icat3::LBlock;
using BlockSet = std::set<const Block*>;
Generator(const Block* focus,
const unsigned int ways,
bool focusEvicted);
void update(const Block* block);
bool contains(const Generator& generator) const;
inline bool isFocusedBlockEvicted() const
{
return _focusEvicted;
}
inline bool contains(const Block* block) const
{
return _focusEvicted ||
(_youngerBlocks.find(block) != _youngerBlocks.end());
}
inline bool operator==(const Generator& rhs) const
{
if(_focusEvicted)
return rhs._focusEvicted;
return ((!rhs._focusEvicted) && _youngerBlocks == rhs._youngerBlocks);
}
inline bool operator!=(const Generator& rhs) const
{
return !(*this == rhs);
}
private:
const Block* _focus;
const unsigned int _ways;
bool _focusEvicted;
BlockSet _youngerBlocks;
};
class LexicalOrder
{
public:
inline bool operator()(const Generator& lhs,
const Generator& rhs) const
{
if(lhs.isFocusedBlockEvicted())
return true;
if(rhs.isFocusedBlockEvicted())
return false;
return std::lexicographical_compare(
lhs._youngerBlocks.begin(),
lhs._youngerBlocks.end(),
rhs._youngerBlocks.begin(),
rhs._youngerBlocks.end());
}
};
} // namespace exactlru
#endif // GENERATORS_H
#ifndef MAY_ABSTRACT_VALUE_H
#define MAY_ABSTRACT_VALUE_H
#include <exactlru/MayAnalysis/MayGeneratorsAntichain.h>
namespace exactlru
{
using MayAbstractValue = MayGeneratorsAntichain;
} // namespace exactlru
#endif // MAY_ABSTRACT_VALUE_H
/*
* ExactMustDomain class interface
* 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
*/
#ifndef MAY_DOMAIN_H_
#define MAY_DOMAIN_H_
#include <exactlru/MayAnalysis/MayGeneratorsAntichain.h>
namespace exactlru
{
class MayDomain {
public:
using t = MayGeneratorsAntichain;
MayDomain(const otawa::icat3::LBlock* focus,
const otawa::icat3::LBlockCollection& coll,
int set,
const t *init);
inline const t& bot(void) const { return m_bot; }
inline const t& top(void) const { return m_top; }
inline const t& init(void) const { return m_init; }
inline void copy(t& d, const t& s) { d = s; }
inline bool equals(const t& a, const t& b) { return a == b; }
void join(t& d, const t& s);
void fetch(t& a, const otawa::icat3::LBlock *lb);
void update(const otawa::icache::Access& access, t& a);
bool isAlwaysMiss(const t& a) const;
private:
const otawa::icat3::LBlock* m_focus;
t m_bot, m_top;
otawa::hard::Cache::set_t m_set;
const otawa::icat3::LBlockCollection& m_coll;
const t& m_init;
t m_tmp;
};
} // namespace exactlru
#endif /* MAY_DOMAIN_H_ */
#ifndef MAY_GENERATORS_ANTICHAIN_H
#define MAY_GENERATORS_ANTICHAIN_H
#include <set>
#include <exactlru/Generator.h>
namespace exactlru
{
class MayComparator
{
public:
inline bool operator()(const Generator& lhs, const Generator& rhs) const
{
return rhs.contains(lhs);
}
};
class MayGeneratorsAntichain
{
public:
using Block = Generator::Block;
using GeneratorsSet = std::set<Generator, LexicalOrder>;
using PartialOrder = MayComparator;
MayGeneratorsAntichain(const GeneratorsSet& g = {});
void update(const Block* block);
void join(const MayGeneratorsAntichain& rhs);
bool isAlwaysMiss() const;
inline bool operator==(const MayGeneratorsAntichain& rhs) const
{
return _generators == rhs._generators;
}
inline bool operator!=(const MayGeneratorsAntichain& rhs) const
{
return !(*this == rhs);
}
private:
void insert(const Generator& generator)
{
// Check if "generator" is subsumed.
for(const auto& g : _generators)
if(_less(g, generator))
return;
// Remove old generators that are subsumed
typename GeneratorsSet::const_iterator it = _generators.begin();
while(it != _generators.end()) {
if(_less(generator, *it))
it = _generators.erase(it);
else
++it;
}
_generators.insert(generator);
}
GeneratorsSet _generators;
PartialOrder _less;
};
} // namespace exactlru
#endif // MAY_GENERATORS_ANTICHAIN_H
#ifndef MAY_MANAGER_H
#define MAY_MANAGER_H
#include <exactlru/MayAnalysis/MayDomain.h>
namespace exactlru
{
class MayManager
{
public:
MayManager(MayDomain& domain,
const MayDomain::t& value) :
m_domain(domain),
m_current(value)
{
}
inline void update(const otawa::icache::Access& acc)
{
m_domain.update(acc, m_current);
}
inline void restart(const MayDomain::t& value)
{
m_domain.copy(m_current, value);
}
inline MayDomain::t current() const
{
return m_current;
}
inline bool alwaysMiss() const
{
return m_domain.isAlwaysMiss(m_current);
}
private:
MayDomain& m_domain;
MayDomain::t m_current;
};
} // namespace exactlru
#endif // MAY_MANAGER_H
#ifndef MUST_ABSTRACT_VALUE_H
#define MUST_ABSTRACT_VALUE_H
#include <exactlru/MayAnalysis/MayGeneratorsAntichain.h>
namespace exactlru
{
using MustAbstractValue = MayGeneratorsAntichain;
} // namespace exactlru
#endif // MUST_ABSTRACT_VALUE_H
/*
* ExactMustDomain class interface
* 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
*/
#ifndef MUST_DOMAIN_H_
#define MUST_DOMAIN_H_
#include <exactlru/MustAnalysis/MustGeneratorsAntichain.h>
namespace exactlru
{
class MustDomain {
public:
using t = MustGeneratorsAntichain;
MustDomain(const otawa::icat3::LBlock* focus,
const otawa::icat3::LBlockCollection& coll,
int set,
const t *init);
inline const t& bot(void) const { return m_bot; }
inline const t& top(void) const { return m_top; }
inline const t& init(void) const { return m_init; }
inline void copy(t& d, const t& s) { d = s; }
inline bool equals(const t& a, const t& b) { return a == b; }
void join(t& d, const t& s);
void fetch(t& a, const otawa::icat3::LBlock *lb);
void update(const otawa::icache::Access& access, t& a);
bool isAlwaysHit(const t& a) const;
private:
const otawa::icat3::LBlock* m_focus;
t m_bot, m_top;
otawa::hard::Cache::set_t m_set;
const otawa::icat3::LBlockCollection& m_coll;
const t& m_init;
t m_tmp;
};
} // namespace exactlru
#endif /* MUST_DOMAIN_H_ */
#ifndef MUST_GENERATORS_ANTICHAIN_H
#define MUST_GENERATORS_ANTICHAIN_H
#include <set>
#include <exactlru/Generator.h>
namespace exactlru
{
class MustComparator
{
public:
inline bool operator()(const Generator& lhs, const Generator& rhs) const
{
return lhs.contains(rhs);
}
};
class MustGeneratorsAntichain
{
public:
using Block = Generator::Block;
using GeneratorsSet = std::set<Generator, LexicalOrder>;
using PartialOrder = MustComparator;
MustGeneratorsAntichain(const GeneratorsSet& g = {});
void update(const Block* block);
void join(const MustGeneratorsAntichain& rhs);
bool isAlwaysHit() const;
inline bool operator==(const MustGeneratorsAntichain& rhs) const
{
return _generators == rhs._generators;
}
inline bool operator!=(const MustGeneratorsAntichain& rhs) const
{
return !(*this == rhs);
}
private:
void insert(const Generator& generator)
{
// Check if "generator" is subsumed.
for(const auto& g : _generators)
if(_less(g, generator))
return;
// Remove old generators that are subsumed
typename GeneratorsSet::const_iterator it = _generators.begin();
while(it != _generators.end()) {
if(_less(generator, *it))
it = _generators.erase(it);
else
++it;
}
_generators.insert(generator);
}
GeneratorsSet _generators;
PartialOrder _less;
};
} // namespace exactlru
#endif // MUST_GENERATORS_ANTICHAIN_H
#ifndef MUST_MANAGER_H
#define MUST_MANAGER_H
#include <exactlru/MustAnalysis/MustDomain.h>
namespace exactlru
{
class MustManager
{
public:
MustManager(MustDomain& domain,
const MustDomain::t& value) :
m_domain(domain),
m_current(value)
{
}
inline void update(const otawa::icache::Access& acc)
{
m_domain.update(acc, m_current);
}
inline void restart(const MustDomain::t& value)
{
m_domain.copy(m_current, value);
}
inline MustDomain::t current() const
{
return m_current;
}
inline bool alwaysHit() const
{
return m_domain.isAlwaysHit(m_current);
}
private:
MustDomain& m_domain;
MustDomain::t m_current;
};
} // namespace exactlru
#endif // MAY_MANAGER_H
//FIXME: Change copyright
/*
* features of exactlru
* Copyright (c) 2016, 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
*/
#ifndef EXACTLRU_FEATURES_H_
#define EXACTLRU_FEATURES_H_
</