Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
OTAWA-plugins
Polymalys
Commits
72e14727
Commit
72e14727
authored
Jul 13, 2018
by
Ballabriga Clément
Browse files
[WIP] Debut des travaux sur le nouveau join
parent
9fbcdb02
Changes
5
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
72e14727
...
...
@@ -2,7 +2,7 @@ CXXFLAGS=`otawa-config otawa/oslice --cflags`
LIBS
=
`
otawa-config otawa/oslice
--libs
`
LIBS
+=
-lppl
CXXFLAGS
+=
-fPIC
-Wall
-DUSE_CLANG_COMPLETER
-std
=
c++1
1
-O0
-g
CXXFLAGS
+=
-fPIC
-Wall
-DUSE_CLANG_COMPLETER
-std
=
c++1
4
-O0
-g
all
:
poly.so
...
...
include/PPLDomain.h
View file @
72e14727
...
...
@@ -89,6 +89,21 @@ class HashIdent {
static
inline
bool
equals
(
const
Ident
&
key1
,
const
Ident
&
key2
)
{
return
key1
.
equals
(
key2
);
}
};
class
VectCoefIdent
{
public:
static
inline
t
::
hash
hash
(
const
Vector
<
PPL
::
Coefficient
>
&
v
)
{
int
prime
=
31
;
t
::
hash
result
=
1
;
for
(
int
i
=
0
;
i
<
v
.
length
();
i
++
)
{
result
=
prime
*
result
+
PPL
::
raw_value
(
v
[
i
]).
get_ui
();
}
return
0
;
}
static
inline
bool
equals
(
const
Vector
<
PPL
::
Coefficient
>
&
v1
,
const
Vector
<
PPL
::
Coefficient
>
&
v2
)
{
return
v1
==
v2
;
}
};
class
HashCons
{
public:
static
t
::
hash
hash
(
const
PPL
::
Constraint
&
key
);
...
...
@@ -269,6 +284,7 @@ private:
int
_size
;
};
/**
* @class MapWithHash
*
...
...
@@ -860,6 +876,12 @@ private:
private:
/* Private helper functions. Subject to changes, and should not be used directly. */
std
::
set
<
guid_t
>
_collectPolyVars
(
const
WPoly
&
poly
)
const
;
void
_identifyPolyVars
(
const
PPLDomain
&
d
,
const
std
::
set
<
guid_t
>
&
vars
,
const
std
::
set
<
guid_t
>
&
indep
,
MyHTable
<
guid_t
,
Vector
<
PPL
::
Coefficient
>
>
&
vmap
)
const
;
// int _doAllocAxis(const Ident & /*ident*/, bool allow_replace = false);
// void _doFreeAxis(int axis);
#ifdef POLY_DEBUG
...
...
include/PolyCommon.h
View file @
72e14727
...
...
@@ -11,7 +11,7 @@
#include
"MyHTable.h"
//
#define POLY_DEBUG 1
#define POLY_DEBUG 1
namespace
otawa
{
namespace
poly
{
...
...
include/PolyWrap.h
View file @
72e14727
...
...
@@ -366,6 +366,10 @@ class WPoly {
// Mapping (projection)
template
<
class
F
>
void
map_vars
(
F
pfunc
);
template
<
class
F
>
void
map_lambda
(
F
lambda
);
template
<
class
F
>
void
filter_lambda
(
F
lambda
);
// equality
inline
bool
equals
(
const
WPoly
&
src
)
const
{
WPoly
copie1
=
src
;
...
...
@@ -427,6 +431,42 @@ class WPoly {
PPL
::
C_Polyhedron
poly
;
};
/**
* @class FilterLambda
*
* Partial mapping function that filters according to lambda function
*/
template
<
class
F
>
class
FilterLambda
{
public:
inline
explicit
FilterLambda
(
F
&
lambda
)
:
_lambda
(
lambda
)
{}
inline
bool
maps
(
guid_t
i
,
guid_t
&
j
)
const
{
if
(
_lambda
(
i
))
{
j
=
i
;
return
true
;
}
else
return
false
;
}
private:
F
&
_lambda
;
};
/**
* @class FilterLambda
*
* Partial mapping function that filters according to lambda function
*/
template
<
class
F
>
class
MapLambda
{
public:
inline
explicit
MapLambda
(
F
&
lambda
)
:
_lambda
(
lambda
)
{}
inline
bool
maps
(
guid_t
i
,
guid_t
&
j
)
const
{
return
_lambda
(
i
,
j
);
}
private:
F
&
_lambda
;
};
/* Template implementations */
template
<
class
F
>
void
WPoly
::
map_adapter_dim
(
F
pfunc
)
{
...
...
@@ -468,6 +508,17 @@ template <class F> void WPoly::map_vars(F pfunc) {
// print(elm::cout);
}
template
<
class
F
>
void
WPoly
::
map_lambda
(
F
lambda
)
{
MapLambda
<
F
>
helper
(
lambda
);
map_vars
(
helper
);
}
template
<
class
F
>
void
WPoly
::
filter_lambda
(
F
lambda
)
{
FilterLambda
<
F
>
helper
(
lambda
);
map_vars
(
helper
);
}
}
// end namespace poly
}
// end namespace otawa
#endif
poly_PPLDomain.cpp
View file @
72e14727
...
...
@@ -2204,12 +2204,122 @@ void PPLDomain::_doUnify(PPLDomain &l1, PPLDomain &r1, bool noPtr) const {
cout
<<
"Right state: "
<<
endl
;
cout
<<
r1
;
#endif
MyHTable
<
guid_t
,
guid_t
>
rename
;
if
(
!
noPtr
)
{
std
::
set
<
guid_t
>
leftVars
=
_collectPolyVars
(
l1
.
poly
);
// aka V1 dans l'algo
std
::
set
<
guid_t
>
rightVars
=
_collectPolyVars
(
r1
.
poly
);
// aka V2 dans l'algo
std
::
set
<
guid_t
>
commonVars
/* C dans l'algo */
,
leftOnlyVars
/* V1' dans l'algo */
,
rightOnlyVars
/* V2' dans l'algo */
;
std
::
set_intersection
(
leftVars
.
begin
(),
leftVars
.
end
(),
rightVars
.
begin
(),
rightVars
.
end
(),
std
::
inserter
(
commonVars
,
commonVars
.
begin
()));
std
::
set_difference
(
leftVars
.
begin
(),
leftVars
.
end
(),
rightVars
.
begin
(),
rightVars
.
end
(),
std
::
inserter
(
leftOnlyVars
,
leftOnlyVars
.
begin
()));
std
::
set_difference
(
rightVars
.
begin
(),
rightVars
.
end
(),
leftVars
.
begin
(),
leftVars
.
end
(),
std
::
inserter
(
rightOnlyVars
,
rightOnlyVars
.
begin
()));
WPoly
commonPoly
=
l1
.
poly
;
commonPoly
.
poly_hull_assign
(
r1
.
poly
);
/* TODO PERF : maybe we can avoid this operation */
#ifdef POLY_DEBUG
cout
<<
"Common vars: "
;
for
(
std
::
set
<
guid_t
>::
const_iterator
it
=
commonVars
.
begin
();
it
!=
commonVars
.
end
();
it
++
)
cout
<<
"v"
<<
*
it
<<
" "
;
cout
<<
endl
;
#endif
std
::
set
<
guid_t
>
indepVars
;
/* C' dans l'algo */
for
(
std
::
set
<
guid_t
>::
const_iterator
it
=
commonVars
.
begin
();
it
!=
commonVars
.
end
();
it
++
)
{
WPoly
temp
=
commonPoly
;
WVar
v
(
*
it
);
temp
.
filter_lambda
([
v
,
&
indepVars
](
guid_t
guid
)
{
return
((
guid
==
v
.
guid
())
||
(
indepVars
.
find
(
guid
)
!=
indepVars
.
end
()));
});
WPoly
::
ConsIterator
it2
(
temp
);
for
(;
it2
&&
!
(
*
it2
).
is_equality
();
it2
++
);
if
(
!
it2
)
indepVars
.
insert
(
*
it
);
}
#ifdef POLY_DEBUG
cout
<<
"Independant common vars: "
;
for
(
std
::
set
<
guid_t
>::
const_iterator
it
=
indepVars
.
begin
();
it
!=
indepVars
.
end
();
it
++
)
cout
<<
"v"
<<
*
it
<<
" "
;
cout
<<
endl
;
#endif
MyHTable
<
guid_t
,
Vector
<
PPL
::
Coefficient
>
>
leftVMap
;
MyHTable
<
guid_t
,
Vector
<
PPL
::
Coefficient
>
>
rightVMap
;
_identifyPolyVars
(
l1
,
leftOnlyVars
,
indepVars
,
leftVMap
);
_identifyPolyVars
(
r1
,
rightOnlyVars
,
indepVars
,
rightVMap
);
MyHTable
<
Vector
<
PPL
::
Coefficient
>
,
guid_t
,
VectCoefIdent
>
invLeftVMap
;
for
(
MyHTable
<
guid_t
,
Vector
<
PPL
::
Coefficient
>
>::
PairIterator
it
(
leftVMap
);
it
;
it
++
)
{
invLeftVMap
.
put
((
*
it
).
snd
,
(
*
it
).
fst
);
}
for
(
MyHTable
<
guid_t
,
Vector
<
PPL
::
Coefficient
>
>::
PairIterator
it
(
rightVMap
);
it
;
it
++
)
{
if
(
invLeftVMap
.
hasKey
((
*
it
).
snd
))
{
#ifdef POLY_DEBUG
cout
<<
"Variable "
<<
WVar
(
invLeftVMap
[(
*
it
).
snd
])
<<
"(left) == "
<<
WVar
((
*
it
).
fst
)
<<
"(right)"
<<
endl
;
#endif
// rename memory address variable
rename
.
add
(
invLeftVMap
[(
*
it
).
snd
],
(
*
it
).
fst
);
// also rename memory value variable
Ident
leftIdAddr
=
l1
.
getIdent
(
WVar
(
invLeftVMap
[(
*
it
).
snd
]));
Ident
rightIdAddr
=
r1
.
getIdent
(
WVar
((
*
it
).
fst
));
Ident
leftIdVal
=
Ident
(
leftIdAddr
.
getId
(),
Ident
::
ID_MEM_VAL
);
Ident
rightIdVal
=
Ident
(
rightIdAddr
.
getId
(),
Ident
::
ID_MEM_VAL
);
rename
.
add
(
l1
.
getVar
(
leftIdVal
).
guid
(),
r1
.
getVar
(
rightIdVal
).
guid
());
}
}
// take care of memory variables that were already same()
for
(
MyHTable
<
Ident
,
guid_t
,
HashIdent
>::
PairIterator
it
=
l1
.
idmap
.
getPairIter
();
it
;
it
++
)
{
for
(
MyHTable
<
Ident
,
guid_t
,
HashIdent
>::
PairIterator
it2
=
r1
.
idmap
.
getPairIter
();
it2
;
it2
++
)
{
WVar
x1
((
*
it
).
snd
);
WVar
x2
((
*
it2
).
snd
);
if
(((
*
it
).
fst
.
getType
()
==
Ident
::
ID_MEM_ADDR
)
||
((
*
it
).
fst
.
getType
()
==
Ident
::
ID_MEM_VAL
))
{
if
(
x1
.
guid
()
==
x2
.
guid
())
{
rename
.
add
(
x1
.
guid
(),
x2
.
guid
());
}
}
}
}
}
// rename register variables
for
(
MyHTable
<
Ident
,
guid_t
,
HashIdent
>::
PairIterator
it
=
l1
.
idmap
.
getPairIter
();
it
;
it
++
)
{
if
(((
*
it
).
fst
.
getType
()
!=
Ident
::
ID_MEM_ADDR
)
&&
((
*
it
).
fst
.
getType
()
!=
Ident
::
ID_MEM_VAL
))
if
(
r1
.
idmap
.
has1
((
*
it
).
fst
))
{
rename
.
add
((
*
it
).
snd
,
r1
.
idmap
.
find1
((
*
it
).
fst
));
// cout << "[R] mapping " << (*it).snd << " to " << r1.idmap.find1((*it).fst) << endl;
}
}
MapGuid
mg
(
rename
);
l1
.
doMap
(
mg
);
#ifdef POLY_DEBUG
cout
<<
"Unified:"
<<
endl
;
cout
<<
"Left state: "
<<
endl
;
cout
<<
l1
;
fflush
(
stdout
);
cout
<<
"Right state: "
<<
endl
;
cout
<<
r1
;
#endif
return
;
exit
(
0
);
WPoly
inter
=
l1
.
poly
;
Ident
cmp
(
16
,
Ident
::
ID_REG
);
if
(
!
noPtr
)
{
inter
.
intersection_assign
(
r1
.
poly
);
}
MyHTable
<
guid_t
,
guid_t
>
rename
;
/*
cout << "Inter: " << inter << endl;
if (!noPtr) {
...
...
@@ -2243,21 +2353,6 @@ void PPLDomain::_doUnify(PPLDomain &l1, PPLDomain &r1, bool noPtr) const {
}
}
MapGuid
mg
(
rename
);
l1
.
doMap
(
mg
);
#ifdef POLY_DEBUG
cout
<<
"Unified:"
<<
endl
;
cout
<<
"Left state: "
<<
endl
;
cout
<<
l1
;
fflush
(
stdout
);
cout
<<
"Right state: "
<<
endl
;
cout
<<
r1
;
#endif
return
;
l1
.
poly
.
poly_hull_assign
(
r1
.
poly
);
#ifdef POLY_DEBUG
...
...
@@ -2482,6 +2577,81 @@ void PPLDomain::_doBinaryOp(int op, WVar *v, WVar *vs1, WVar *vs2) {
}
}
void
PPLDomain
::
_identifyPolyVars
(
const
PPLDomain
&
d
,
const
std
::
set
<
guid_t
>
&
vars
,
const
std
::
set
<
guid_t
>
&
indep
,
MyHTable
<
guid_t
,
Vector
<
PPL
::
Coefficient
>
>
&
vmap
)
const
{
const
WPoly
&
poly
=
d
.
poly
;
for
(
std
::
set
<
guid_t
>::
const_iterator
it
=
vars
.
begin
();
it
!=
vars
.
end
();
it
++
)
{
WVar
v
(
*
it
);
if
(
!
d
.
isVarMapped
(
v
)
||
d
.
getIdent
(
v
).
getType
()
!=
Ident
::
ID_MEM_ADDR
)
continue
;
WPoly
temp
=
poly
;
temp
.
filter_lambda
([
&
indep
,
v
](
guid_t
guid
)
{
return
((
guid
==
v
.
guid
())
||
(
indep
.
find
(
guid
)
!=
indep
.
end
()));
});
WPoly
::
ConsIterator
it2
(
temp
);
for
(;
it2
&&
!
(
*
it2
).
is_equality
();
it2
++
);
if
(
it2
)
{
WCons
c
=
*
it2
;
Vector
<
PPL
::
Coefficient
>
vect
;
vect
.
setLength
(
indep
.
size
()
+
2
);
/* vector format: [Indep. vars coefs, Current var (v) coef, Constant] */
for
(
int
i
=
0
;
i
<
vect
.
length
();
i
++
)
vect
[
i
]
=
0
;
PPL
::
Coefficient
curVarCoef
=
c
.
coefficient
(
v
);
PPL
::
Coefficient
constant
=
c
.
inhomogeneous_term
();
ASSERT
(
curVarCoef
);
// curVarCoef==0 would imply that the indep set contains non-independant variables
bool
normalizeSign
=
curVarCoef
<
0
;
vect
[
vect
.
length
()
-
2
]
=
normalizeSign
?
-
curVarCoef
:
curVarCoef
;
vect
[
vect
.
length
()
-
1
]
=
normalizeSign
?
-
constant
:
constant
;
for
(
WCons
::
TermIterator
it3
(
c
);
it3
;
it3
++
)
{
WVar
v2
(
*
it3
);
if
((
v2
.
guid
()
!=
v
.
guid
())
&&
(
c
.
coefficient
(
v2
)
!=
0
))
{
ASSERT
(
indep
.
find
(
v2
.
guid
())
!=
indep
.
end
());
// must be true because of projection, and because v2!=v
PPL
::
Coefficient
coef
=
c
.
coefficient
(
v2
);
vect
[
std
::
distance
(
indep
.
begin
(),
indep
.
find
(
v2
.
guid
()))]
=
normalizeSign
?
-
coef
:
coef
;
}
}
PPL
::
Coefficient
pgcd
=
vect
[
vect
.
length
()
-
1
];
for
(
int
i
=
0
;
i
<
vect
.
length
()
-
1
;
i
++
)
{
PPL
::
Coefficient
coef2
=
vect
[
i
];
while
(
coef2
!=
0
)
{
PPL
::
Coefficient
tmp
=
pgcd
;
pgcd
=
coef2
;
coef2
=
tmp
%
coef2
;
}
}
if
(
pgcd
!=
1
)
{
for
(
int
i
=
0
;
i
<
vect
.
length
();
i
++
)
{
vect
[
i
]
/=
pgcd
;
}
}
#ifdef POLY_DEBUG
cout
<<
"variable "
<<
v
<<
" has vect: "
;
for
(
int
i
=
0
;
i
<
vect
.
length
();
i
++
)
cout
<<
vect
[
i
]
<<
", "
;
cout
<<
endl
;
#endif
vmap
.
put
(
v
.
guid
(),
vect
);
}
}
}
std
::
set
<
guid_t
>
PPLDomain
::
_collectPolyVars
(
const
WPoly
&
poly
)
const
{
std
::
set
<
guid_t
>
result
;
for
(
WPoly
::
ConsIterator
it
(
poly
);
it
;
it
++
)
{
WCons
c
=
*
it
;
for
(
WCons
::
TermIterator
it2
(
c
);
it2
;
it2
++
)
{
if
(
c
.
coefficient
(
*
it2
)
!=
0
)
result
.
insert
((
*
it2
).
guid
());
}
}
return
result
;
}
void
PPLDomain
::
enableSummary
()
{
_summary
=
new
PPLSummary
();
/*
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment