formula: fix valgrind error in is_Kleene_star() with clang++
* spot/tl/formula.hh, spot/tl/formula.cc: Rework the initialization of fnode. * NEWS: Mention the bug.
This commit is contained in:
parent
633906e347
commit
01d84c4d52
3 changed files with 34 additions and 19 deletions
5
NEWS
5
NEWS
|
|
@ -1,6 +1,9 @@
|
|||
New in spot 2.1.1a (not yet released)
|
||||
|
||||
Nothing yet.
|
||||
Bug fixes:
|
||||
|
||||
- Fix spurious uninitialized read reported by valgrind when
|
||||
is_Kleene_star() is compiled by clang++.
|
||||
|
||||
New in spot 2.1.1 (2016-09-20)
|
||||
|
||||
|
|
|
|||
|
|
@ -1025,16 +1025,15 @@ namespace spot
|
|||
|
||||
void fnode::setup_props(op o)
|
||||
{
|
||||
op_ = o;
|
||||
id_ = next_id_++;
|
||||
// If the counter of formulae ever loops, we want to skip the
|
||||
// first three values, because they are permanently associated
|
||||
// to constants, and it is convenient to have constants
|
||||
// smaller than all other formulas.
|
||||
if (next_id_ == 0)
|
||||
if (SPOT_UNLIKELY(next_id_ == 0))
|
||||
next_id_ = 3;
|
||||
|
||||
switch (op_)
|
||||
switch (o)
|
||||
{
|
||||
case op::ff:
|
||||
case op::tt:
|
||||
|
|
|
|||
|
|
@ -492,6 +492,21 @@ namespace spot
|
|||
|
||||
template<class iter>
|
||||
fnode(op o, iter begin, iter end)
|
||||
// Clang has some optimization where is it able to combine the
|
||||
// 4 movb initializing op_,min_,max_,saturated_ into a single
|
||||
// movl. Also it can optimize the three byte-comparisons of
|
||||
// is_Kleene_star() into a single masked 32-bit comparison.
|
||||
// The latter optimization triggers warnings from valgrind if
|
||||
// min_ and max_ are not initialized. So to benefit from the
|
||||
// initialization optimization and the is_Kleene_star()
|
||||
// optimization in Clang, we always initialize min_ and max_
|
||||
// with this compiler. Do not do it the rest of the time,
|
||||
// since the optimization is not done.
|
||||
: op_(o),
|
||||
#if __llvm__
|
||||
min_(0), max_(0),
|
||||
#endif
|
||||
saturated_(0)
|
||||
{
|
||||
size_t s = std::distance(begin, end);
|
||||
if (s > (size_t) UINT16_MAX)
|
||||
|
|
@ -509,11 +524,9 @@ namespace spot
|
|||
}
|
||||
|
||||
fnode(op o, const fnode* f, uint8_t min, uint8_t max)
|
||||
: op_(o), min_(min), max_(max), saturated_(0), size_(1)
|
||||
{
|
||||
size_ = 1;
|
||||
children[0] = f;
|
||||
min_ = min;
|
||||
max_ = max;
|
||||
setup_props(o);
|
||||
}
|
||||
|
||||
|
|
@ -525,7 +538,7 @@ namespace spot
|
|||
op op_; // operator
|
||||
uint8_t min_; // range minimum (for star-like operators)
|
||||
uint8_t max_; // range maximum;
|
||||
mutable uint8_t saturated_ = 0;
|
||||
mutable uint8_t saturated_;
|
||||
uint16_t size_; // number of children
|
||||
mutable uint16_t refs_ = 0; // reference count - 1;
|
||||
size_t id_; // Also used as hash.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue