Commit 0827eee5 authored by Ballabriga Clément's avatar Ballabriga Clément
Browse files

fusion du bordel en cours... 1/3

parent 3f107ec8
......@@ -12,6 +12,7 @@
#include <ppl.hh>
#include "PolyCommon.h"
#include "PolyWrap.h"
namespace otawa {
namespace poly {
......@@ -21,7 +22,6 @@ using namespace otawa::util;
namespace PPL = Parma_Polyhedra_Library;
using Variable = PPL::Variable;
Output &operator<<(Output &o, Variable pv);
enum bound_t : signed long {
UNREACHABLE = -1,
......@@ -132,7 +132,7 @@ class PPLDomain {
private:
/* Abstract state */
PPL::C_Polyhedron poly;
WPoly poly;
MyHTable<Ident, int, HashIdent>
id2axis; ///< Mapping from identifier (register/pointers) to polyhedron variable
......@@ -165,16 +165,10 @@ class PPLDomain {
template <class F> class MapHelper {
public:
MapHelper(F &pfunc, int max_in_domain);
inline PPL::dimension_type max_in_codomain() const { return _max_in_codomain; }
inline PPL::dimension_type max_in_domain() const { return _max_in_domain; }
inline bool maps(PPL::dimension_type i, PPL::dimension_type &j) const { return _pfunc.maps(i, j); }
inline bool has_empty_codomain() const { return _empty; }
inline bool maps(guid_t i, guid_t &j) const { return _pfunc.maps(i, j); }
private:
F &_pfunc;
PPL::dimension_type _max_in_domain;
PPL::dimension_type _max_in_codomain;
bool _empty;
};
/**
......@@ -187,7 +181,7 @@ class PPLDomain {
public:
inline ~RemoveMarked() = default;
inline RemoveMarked(BitVector &bv, int size) : _bv(bv), _size(size) {}
bool maps(PPL::dimension_type i, PPL::dimension_type &j) const;
bool maps(guid_t i, guid_t &j) const;
private:
BitVector &_bv;
......@@ -203,7 +197,7 @@ class PPLDomain {
class MapWithHash {
public:
inline explicit MapWithHash(MyHTable<int, int> &map) : _map(map) {}
inline bool maps(PPL::dimension_type i, PPL::dimension_type &j) const {
inline bool maps(guid_t i, guid_t &j) const {
if (_map.hasKey(i)) {
j = _map[i];
return true;
......@@ -217,8 +211,8 @@ class PPLDomain {
class MapShift {
public:
inline explicit MapShift(PPL::dimension_type domsize, PPL::dimension_type shift) : _domsize(domsize), _shift(shift) {}
inline bool maps(PPL::dimension_type i, PPL::dimension_type &j) const {
inline explicit MapShift(guid_t domsize, guid_t shift) : _domsize(domsize), _shift(shift) {}
inline bool maps(guid_t i, guid_t &j) const {
if (i < _domsize) {
j = i + _shift;
return true;
......@@ -226,8 +220,8 @@ class PPLDomain {
}
private:
PPL::dimension_type _domsize;
PPL::dimension_type _shift;
guid_t _domsize;
guid_t _shift;
};
public:
......@@ -238,7 +232,7 @@ class PPLDomain {
*/
inline PPLDomain() {
num_axis = -1;
poly = PPL::C_Polyhedron(0, PPL::EMPTY);
poly = WPoly(true);
compare_reg = Ident();
compare_op = sem::EQ;
_ws = nullptr;
......@@ -254,7 +248,7 @@ class PPLDomain {
mem_ref = 0;
trash = BitVector(maxAxis);
_ws = ws;
poly = PPL::C_Polyhedron(0, PPL::UNIVERSE);
poly = WPoly(true);
compare_reg = Ident();
compare_op = sem::EQ;
_summary = summary;
......@@ -370,7 +364,7 @@ class PPLDomain {
* @param bsup_n Reference for storing the numerator for the upper bound
* @param bsup_d eference for storing the denominator for the upper bound
*/
void getRange(const Variable &var, PPL::Coefficient &binf_n, PPL::Coefficient &binf_d, PPL::Coefficient &bsup_n,
void getRange(const WVar &var, PPL::Coefficient &binf_n, PPL::Coefficient &binf_d, PPL::Coefficient &bsup_n,
PPL::Coefficient &bsup_d) const;
/**
......@@ -424,7 +418,7 @@ class PPLDomain {
* @param v2 Second variable
* @return true if may be equal, false otherwise
*/
bool mayAlias(const Variable &v1, const Variable &v2) const;
bool mayAlias(const WVar &v1, const WVar &v2) const;
/**
* Tests if two variables must be equal (i.e. they are equal for all concrete states in this abstract state)
......@@ -433,7 +427,7 @@ class PPLDomain {
* @param v2 Second variable
* @return true if must be equal, false otherwise
*/
bool mustAlias(const Variable &v1, const Variable &v2, int offset = 0) const;
bool mustAlias(const WVar &v1, const WVar &v2, int offset = 0) const;
/**
* Attempts to get the value of a a variable mapped to an identifier, if this value can be statically determined,
......@@ -454,7 +448,7 @@ class PPLDomain {
* @param cst_d Reference for storing the denominator
* @return true if successful, false if the value cannot be determined.
*/
bool getConstant(const Variable &var, PPL::Coefficient &cst_n, PPL::Coefficient &cst_d) const;
bool getConstant(const WVar &var, PPL::Coefficient &cst_n, PPL::Coefficient &cst_d) const;
/* TODO documenter */
PPLDomain getLinearExpr(const Ident &id);
......@@ -619,7 +613,7 @@ class PPLDomain {
*
* @param c The new constraint to add.
*/
void doNewConstraint(const PPL::Constraint &c) { poly.add_constraint(c); }
void doNewConstraint(const WCons &c) { poly.add_constraint(c); }
/* Variable/Idents handling operations */
......@@ -630,7 +624,7 @@ class PPLDomain {
* @param allow_replace true if we allow replacing an existing variable that was mapped to id, false otherwise
* @return The new variable.
*/
Variable varNew(const Ident &id, bool allow_replace = false, bool create_damaged = false);
WVar varNew(const Ident &id, bool allow_replace = false, bool create_damaged = false);
/**
* Schedule a variable (associated with an identifier) to be destroyed.
......@@ -646,7 +640,7 @@ class PPLDomain {
*
* @param v Target variable
*/
inline void varKill(const Variable &v) { return _doFreeAxis(v.id()); }
inline void varKill(const WVar &v) { return _doFreeAxis(v.guid()); }
/**
* Gets the variable associated with an identifier, creating a new variable if it doesn't exists (i.e. lookup).
......@@ -655,7 +649,7 @@ class PPLDomain {
* @param create_input if true, and the identifier is unknown, and we are summarizing, create an input
* @return The variable.
*/
Variable getVarOrNew(const Ident &id, bool create_input = false);
WVar getVarOrNew(const Ident &id, bool create_input = false);
/**
* Gets the variable associated with an identifier, aborting if the variables doesn't exists (i.e. lookup).
......@@ -663,7 +657,7 @@ class PPLDomain {
* @param id The target identifier
* @return The variable.
*/
Variable getVar(const Ident &id) const;
WVar getVar(const Ident &id) const;
/**
* Tests if a variable is associated with an identifier.
......@@ -671,9 +665,9 @@ class PPLDomain {
* @param v Variable to test
* @return true if the variable is mapped to an identifier, false otherwise
*/
inline bool isVarMapped(const Variable &v) const {
return ((unsigned)axis2id.length() > v.id()) && (axis2id[v.id()].getType() != Ident::ID_INVALID) &&
id2axis.hasKey(axis2id[v.id()]);
inline bool isVarMapped(const WVar &v) const {
return ((unsigned)axis2id.length() > v.guid()) && (axis2id[v.guid()].getType() != Ident::ID_INVALID) &&
id2axis.hasKey(axis2id[v.guid()]);
}
/**
......@@ -682,7 +676,7 @@ class PPLDomain {
* @param v The variable
* @return The identifier
*/
inline const Ident &getIdent(const Variable &v) const { return axis2id[v.id()]; }
inline const Ident &getIdent(const WVar &v) const { return axis2id[v.guid()]; }
/**
* Tests if an identifier exists
......@@ -734,7 +728,7 @@ class PPLDomain {
* @param newValue A variable representing the new memory value.
* @return new address variable
*/
Variable memReplace(const Variable & address, const Variable & newValue);
WVar memReplace(const WVar & address, const WVar & newValue);
/**
* Create a new abstract memory location at specified address, with the specified value.
......@@ -744,7 +738,7 @@ class PPLDomain {
* @param dmg If summarizing, mark address as damaged
* @return new address variable
*/
Variable memCreate(const PPL::Linear_Expression & address , const PPL::Linear_Expression &newValue, bool dmg = true);
WVar memCreate(const WLinExpr & address , const WLinExpr &newValue, bool dmg = true);
/**
* Associate a new value to the address variable, merging with existing value.
......@@ -757,7 +751,7 @@ class PPLDomain {
* @param newValue A variable representing the new memory value.
* @return new address variable
*/
Variable memMerge(const Variable &address, const Variable &newValue);
WVar memMerge(const WVar &address, const WVar &newValue);
/**
* Attempts to use process initial state to discover value associated with a constant address-variable
......@@ -779,28 +773,24 @@ class PPLDomain {
inline void _sanityChecks(bool allow_holes = false) {}
#endif
const PPL::Constraint *_getConstraintFor(int axis) const;
const WCons *_getConstraintFor(int axis) const;
/**
* Indexes the pointer in dom, by their expression in terms of registers referenced in map_regs.
* Stores the result in map_ptr.
*/
void _indexPointersByExpr(MyHTable<PPL::Constraint, int, HashCons> &map_ptr,
void _indexPointersByExpr(MyHTable<WCons, int, HashCons> &map_ptr,
MyHTable<int, int> &commonRegs) const;
void _identifyAncestorVars(PPLDomain &l, MyHTable<int, int> &commonVarsL, PPLDomain &r,
MyHTable<int, int> &commonVarsR) const;
/**
* Computes the convex hull of two polyhedron of different space dimension, extending the smaller if needed.
*/
void _extendAndHull(PPL::C_Polyhedron &poly1, PPL::C_Polyhedron &poly2) const;
/**
* Computes the join or widening of two abstract states
* @param this The first abstract state (will not be modified)
* @param r The second abstract state (will not be modified)
* @return Join or widening result
*/
void _doBinaryOp(int op, Variable *v, Variable *vs1, Variable *vs2);
void _doBinaryOp(int op, WVar *v, WVar *vs1, WVar *vs2);
/**
* Unify the two states so that variables refering to the same object (register, memory location, ...) have the same
......@@ -821,8 +811,8 @@ class PPLDomain {
*/
void _doMatchSummaries(PPLDomain &l1, PPLDomain &r1, unsigned int &axis,
MyHTable <int,int> &mappingL, MyHTable<int,int> &mappingR,
MyHTable<PPL::Constraint, int, HashCons>&,
MyHTable<PPL::Constraint, int, HashCons>&) const;
MyHTable<WCons, int, HashCons>&,
MyHTable<WCons, int, HashCons>&) const;
};
......
......@@ -2,15 +2,17 @@
#define POLYWRAP_H 1
#include <ppl.hh>
namespace polywrap {
#include <elm/io/Output.h>
namespace otawa {
namespace poly {
using namespace std;
namespace PPL = Parma_Polyhedra_Library;
typedef unsigned long long guid_t;
typedef GMP_Integer coef_t;
typedef std::GMP_Integer coef_t;
typedef PPL::dimension_type dim_t;
typedef std::ostream output_t;
typedef elm::io::Output output_t;
class WVar;
class WCons;
......@@ -21,13 +23,13 @@ output_t& operator<< (output_t& stream, const coef_t&);
output_t& operator<< (output_t& stream, const WLinExpr&);
output_t& operator<< (output_t& stream, const WCons&);
output_t& operator<< (output_t& stream, const WPoly&);
output_t& operator<< (output_t& stream, const coef_t& coef);
output_t& operator<< (output_t& stream, const WLinExpr& le);
output_t& operator<< (output_t& stream, const WCons& c);
output_t& operator<< (output_t& stream, const WPoly& p);
WCons operator==(const WLinExpr &a, const WLinExpr &b);
bool operator==(const WPoly &a, const WPoly &b);
bool operator!=(const WPoly &a, const WPoly &b);
WCons operator>=(const WLinExpr &a, const WLinExpr &b);
WCons operator<=(const WLinExpr &a, const WLinExpr &b);
WCons operator>(const WLinExpr &a, const WLinExpr &b);
WCons operator<(const WLinExpr &a, const WLinExpr &b);
WLinExpr operator+(const WLinExpr &a, const WLinExpr &b);
WLinExpr operator*(const WLinExpr &a, const coef_t b);
WLinExpr operator*(const coef_t b, const WLinExpr &a);
......@@ -43,6 +45,7 @@ class WVar {
}
inline WVar(guid_t guid) { _guid = guid; }
inline guid_t guid() const { return _guid; }
inline guid_t id() const { return _guid; }
private:
static guid_t _guid_generator;
......@@ -51,8 +54,6 @@ class WVar {
// WVar
//
guid_t WVar::_guid_generator = 0;
class WLinExpr {
public:
friend WLinExpr operator+(const WLinExpr &a, const WLinExpr &b);
......@@ -67,11 +68,23 @@ class WLinExpr {
const PPL::Linear_Expression toPPL(WPoly &poly) const;
const PPL::Linear_Expression toPPL(const WPoly &poly) const;
inline coef_t inhomogeneous_term() { return cst; }
inline coef_t coefficient(const WVar &v) { return coefs[v.guid()]; }
inline guid_t space_dimension() {
std::cout << "warning: WLinExpr::space_dimension() is deprecated" << std::endl;
guid_t res = 0;
for (std::map<guid_t,coef_t>::const_iterator it=coefs.begin(); it!=coefs.end(); ++it) {
if (res < it->first)
res = it->first;
}
return res + 1;
}
void print(output_t &out) const;
private:
map<guid_t,coef_t> coefs;
std::map<guid_t,coef_t> coefs;
coef_t cst;
};
......@@ -83,6 +96,9 @@ enum ctype_t {CONS_EQ, CONS_GE};
class WCons {
public:
inline WCons(const WLinExpr &l, ctype_t t) { expr = l; ctype = t; }
inline WCons() {
ctype = CONS_EQ;
}
inline void print(output_t &out) const {
if (ctype == CONS_EQ) {
out << "0 == ";
......@@ -91,8 +107,12 @@ class WCons {
} else abort();
expr.print(out);
}
inline coef_t inhomogeneous_term() { return expr.inhomogeneous_term(); }
inline coef_t coefficient(const WVar &v) { return expr.coefficient(v); }
inline guid_t space_dimension() { return expr.space_dimension(); }
inline const WLinExpr& getLE() const { return expr; }
inline ctype_t getType() const { return ctype; }
inline bool is_equality() const { return ctype == CONS_EQ; }
private:
ctype_t ctype;
WLinExpr expr;
......@@ -103,7 +123,7 @@ class WPoly {
private:
class Eliminator {
public:
inline Eliminator(const vector<PPL::dimension_type> &victims,
inline Eliminator(const std::vector<PPL::dimension_type> &victims,
PPL::C_Polyhedron &p) : _victims(victims), _p(p) {
}
......@@ -111,7 +131,7 @@ class WPoly {
inline PPL::dimension_type max_in_domain() const { return _p.space_dimension() - 1; }
inline bool maps(PPL::dimension_type i, PPL::dimension_type &j) const {
PPL::dimension_type k = 0;
for (vector<PPL::dimension_type>::const_iterator it = _victims.begin(); it != _victims.end(); it++) {
for (std::vector<PPL::dimension_type>::const_iterator it = _victims.begin(); it != _victims.end(); it++) {
if ((*it) == i)
return false;
if ((*it) < i)
......@@ -122,12 +142,12 @@ class WPoly {
}
inline bool has_empty_codomain() const { return _p.space_dimension() == _victims.size(); }
private:
const vector<PPL::dimension_type> &_victims;
const std::vector<PPL::dimension_type> &_victims;
const PPL::C_Polyhedron & _p;
};
class MapHash {
public:
inline MapHash(const map<dim_t,dim_t> remap) : _remap(remap) {
inline MapHash(const std::map<dim_t,dim_t> remap) : _remap(remap) {
_max_co = 0;
_max_dom = 0;
......@@ -150,7 +170,7 @@ class WPoly {
inline bool has_empty_codomain() const { return false; }
private:
map<dim_t,dim_t> _remap;
std::map<dim_t,dim_t> _remap;
dim_t _max_co, _max_dom;
};
void combine(WPoly &src, bool keep);
......@@ -180,31 +200,8 @@ class WPoly {
PPL::Constraint_System::const_iterator real_it;
};
inline WPoly() {
poly = PPL::C_Polyhedron(0, PPL::UNIVERSE);
}
// intersection
inline void intersection_assign(const WPoly &src) {
WPoly copie = src;
combine(copie, true);
poly.intersection_assign(copie.poly);
}
// join
inline void poly_hull_assign(const WPoly &src) {
WPoly copie = src;
combine(copie, false);
poly.poly_hull_assign(copie.poly);
}
// widening
inline void bounded_H79_extrapolation_assign(WPoly &src) {
WPoly copie = src;
combine(copie, false);
PPL::Constraint_System dummy;
poly.bounded_H79_extrapolation_assign(copie.poly, dummy);
inline WPoly(bool empty = false) {
poly = PPL::C_Polyhedron(0, empty ? PPL::EMPTY : PPL::UNIVERSE);
}
......@@ -247,7 +244,7 @@ class WPoly {
return ppl_c;
}
map<dim_t,guid_t> invMap() const;
std::map<dim_t,guid_t> invMap() const;
void add_constraint(const WCons &c) {
poly.add_constraint(translate(c));
......@@ -262,12 +259,66 @@ class WPoly {
return poly.maximize(translate(expr), sup_n, sup_d, maximum);
}
inline bool minimize(const WLinExpr&expr, coef_t &sup_n, coef_t &sup_d, bool &maximum) const {
return poly.minimize(translate(expr), sup_n, sup_d, maximum);
}
inline void unconstrain(const WVar &var) {
eliminate(translate(var).id());
}
/* Wrapper around PPL methods */
PPL::Poly_Con_Relation relation_with(const WCons &c) const {
return poly.relation_with(translate(c));
}
inline bool is_empty() const {
return poly.is_empty();
}
inline bool is_universe() const {
return poly.is_universe();
}
inline dim_t space_dimension() const {
return poly.space_dimension();
}
// Mapping (projection)
template <class F> void map_vars(F pfunc);
// equality
inline bool equals(const WPoly &src) const {
WPoly copie1 = src;
WPoly copie2 = *this;
copie1.combine(copie2, true);
return copie1.poly == copie2.poly;
}
// intersection
inline void intersection_assign(const WPoly &src) {
WPoly copie = src;
combine(copie, true);
poly.intersection_assign(copie.poly);
}
// join
inline void poly_hull_assign(const WPoly &src) {
WPoly copie = src;
combine(copie, false);
poly.poly_hull_assign(copie.poly);
}
// widening
inline void bounded_H79_extrapolation_assign(WPoly &src) {
WPoly copie = src;
combine(copie, false);
PPL::Constraint_System dummy;
poly.bounded_H79_extrapolation_assign(copie.poly, dummy);
}
private:
template <class F> void map_adapter_dim(F pfunc);
......@@ -277,13 +328,13 @@ class WPoly {
}
inline void eliminate(PPL::dimension_type id) {
vector<PPL::dimension_type> victims;
std::vector<PPL::dimension_type> victims;
victims.push_back(id);
Eliminator el(victims, poly);
map_with_dim(el);
}
map<guid_t,dim_t> adapter;
std::map<guid_t,dim_t> adapter;
dim_t next = 0;
PPL::C_Polyhedron poly;
};
......@@ -306,8 +357,8 @@ template <class F> void WPoly::map_adapter_dim(F pfunc) {
}
template <class F> void WPoly::map_vars(F pfunc) {
map<guid_t,dim_t> new_adapter;
vector<dim_t> victims;
std::map<guid_t,dim_t> new_adapter;
std::vector<dim_t> victims;
for (std::map<guid_t,dim_t>::iterator it=adapter.begin(); it!=adapter.end(); ++it) {
guid_t i = it->first;
guid_t j = i;
......@@ -323,5 +374,6 @@ template <class F> void WPoly::map_vars(F pfunc) {
map_with_dim(el);
}
} // namespace polywrap
} // end namespace poly
} // end namespace otawa
#endif
This diff is collapsed.
......@@ -25,14 +25,13 @@ using namespace util;
*/
PPLManager::PPLManager(const PropList &props, WorkSpace *ws)
: _init(MAX_AXIS(props), ws), _bot(), _top(MAX_AXIS(props), ws) {
PPL::Constraint_System initcons;
Variable var_sp = _init.varNew(Ident(13, Ident::ID_REG));
Variable var_fp = _init.varNew(Ident(11, Ident::ID_REG));
Variable var_lr = _init.varNew(Ident(14, Ident::ID_REG));
Variable var_ssp = _init.varNew(Ident(Ident::ID_START_SP, Ident::ID_SPECIAL));
Variable var_sfp = _init.varNew(Ident(Ident::ID_START_FP, Ident::ID_SPECIAL));
Variable var_slr = _init.varNew(Ident(Ident::ID_START_LR, Ident::ID_SPECIAL));
WVar var_sp = _init.varNew(Ident(13, Ident::ID_REG));
WVar var_fp = _init.varNew(Ident(11, Ident::ID_REG));
WVar var_lr = _init.varNew(Ident(14, Ident::ID_REG));
WVar var_ssp = _init.varNew(Ident(Ident::ID_START_SP, Ident::ID_SPECIAL));
WVar var_sfp = _init.varNew(Ident(Ident::ID_START_FP, Ident::ID_SPECIAL));
WVar var_slr = _init.varNew(Ident(Ident::ID_START_LR, Ident::ID_SPECIAL));
_init.doNewConstraint(var_ssp == var_sp);
_init.doNewConstraint(var_sfp == var_fp);
......
#include "include/PolyWrap.h"
namespace polywrap {
namespace otawa {
namespace poly {
/* Display operators */
using namespace elm::io;
using namespace PPL;
output_t& operator<< (output_t& stream, const coef_t& coef) {
char buf[128];
gmp_snprintf(buf, sizeof(buf), "%Zd", &PPL::raw_value(coef));
gmp_snprintf(buf, sizeof(buf), "%Zd", &raw_value(coef));
buf[sizeof(buf) - 1] = 0;
stream << buf;
return stream;
......@@ -23,6 +27,12 @@ output_t& operator<< (output_t& stream, const WPoly& p) {
p.print(stream);
return stream;
}
/*
output_t& operator<< (output_t& stream, const WVar& p) {
stream << "v" << p.guid();
return stream;
}
*/
void WLinExpr::print(output_t &out) const {
bool first = true;
......@@ -48,7 +58,7 @@ void WPoly::print(output_t &out) const {
}
out << "]" << endl;
poly.print();
cout << endl;
out << endl;
}
/* Constraint & Linear combination building operators */
......@@ -68,6 +78,12 @@ WCons operator>=(const WLinExpr &a, const WLinExpr &b) {
WCons operator<=(const WLinExpr &a, const WLinExpr &b) {
return (b >= a);
}
WCons operator<(const WLinExpr &a, const WLinExpr &b) {
return (a + 1 <= b);
}
WCons operator>(const WLinExpr &a, const WLinExpr &b) {
return (a >= b + 1);
}
WLinExpr operator+(const WLinExpr &a, const WLinExpr &b) {
WLinExpr res;