make valgrind understand our memory pools
Annotate pools with valgrind macros so that it detects errors in pool usage. Typically, we wish valgrind to detect a leak when the user fails to call proper deallocation function. * spot/misc/fixpool.hh, spot/misc/mspool.hh: here * configure.ac: ensure that valgrind header exists * tests/Makefile.am, tests/core/mempool.cc, tests/core/mempool.test, tests/core/.gitignore: add tests to ensure valgrind accurately detects leaks
This commit is contained in:
parent
b7e77743db
commit
3fe74f1cb9
7 changed files with 234 additions and 10 deletions
|
|
@ -141,7 +141,7 @@ fi
|
||||||
|
|
||||||
AX_CHECK_BUDDY
|
AX_CHECK_BUDDY
|
||||||
|
|
||||||
AC_CHECK_HEADERS([sys/times.h])
|
AC_CHECK_HEADERS([sys/times.h valgrind/memcheck.h])
|
||||||
AC_CHECK_FUNCS([times kill alarm sigaction])
|
AC_CHECK_FUNCS([times kill alarm sigaction])
|
||||||
|
|
||||||
LT_CONFIG_LTDL_DIR([ltdl])
|
LT_CONFIG_LTDL_DIR([ltdl])
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2011, 2015, 2016 Laboratoire de Recherche et
|
// Copyright (C) 2011, 2015, 2016, 2018 Laboratoire de Recherche et
|
||||||
// Développement de l'Epita (LRDE)
|
// Développement de l'Epita (LRDE)
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -20,9 +20,10 @@
|
||||||
#pragma once
|
#pragma once
|
||||||
|
|
||||||
#include <spot/misc/common.hh>
|
#include <spot/misc/common.hh>
|
||||||
#include <new>
|
|
||||||
#include <cstddef>
|
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
|
||||||
#include <cstdlib>
|
#include <valgrind/memcheck.h>
|
||||||
|
#endif
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
|
@ -60,6 +61,12 @@ namespace spot
|
||||||
// If we have free blocks available, return the first one.
|
// If we have free blocks available, return the first one.
|
||||||
if (f)
|
if (f)
|
||||||
{
|
{
|
||||||
|
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
|
||||||
|
VALGRIND_MALLOCLIKE_BLOCK(f, size_, 0, false);
|
||||||
|
// field f->next is initialized: prevents valgrind from complaining
|
||||||
|
// about jumps depending on uninitialized memory
|
||||||
|
VALGRIND_MAKE_MEM_DEFINED(f, sizeof(block_*));
|
||||||
|
#endif
|
||||||
freelist_ = f->next;
|
freelist_ = f->next;
|
||||||
return f;
|
return f;
|
||||||
}
|
}
|
||||||
|
|
@ -83,6 +90,9 @@ namespace spot
|
||||||
|
|
||||||
void* res = free_start_;
|
void* res = free_start_;
|
||||||
free_start_ += size_;
|
free_start_ += size_;
|
||||||
|
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
|
||||||
|
VALGRIND_MALLOCLIKE_BLOCK(res, size_, 0, false);
|
||||||
|
#endif
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -99,6 +109,9 @@ namespace spot
|
||||||
block_* b = reinterpret_cast<block_*>(const_cast<void*>(ptr));
|
block_* b = reinterpret_cast<block_*>(const_cast<void*>(ptr));
|
||||||
b->next = freelist_;
|
b->next = freelist_;
|
||||||
freelist_ = b;
|
freelist_ = b;
|
||||||
|
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
|
||||||
|
VALGRIND_FREELIKE_BLOCK(ptr, 0);
|
||||||
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
private:
|
private:
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2011, 2013, 2015, 2016 Laboratoire de Recherche et
|
// Copyright (C) 2011, 2013, 2015, 2016, 2018 Laboratoire de Recherche et
|
||||||
// Developpement de l'Epita (LRDE)
|
// Developpement de l'Epita (LRDE)
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -20,10 +20,11 @@
|
||||||
#pragma once
|
#pragma once
|
||||||
|
|
||||||
#include <spot/misc/common.hh>
|
#include <spot/misc/common.hh>
|
||||||
#include <spot/misc/hash.hh>
|
#include <unordered_map>
|
||||||
#include <new>
|
|
||||||
#include <cstddef>
|
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
|
||||||
#include <cstdlib>
|
#include <valgrind/memcheck.h>
|
||||||
|
#endif
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
|
@ -69,6 +70,12 @@ namespace spot
|
||||||
if (f)
|
if (f)
|
||||||
{
|
{
|
||||||
block_* first = f;
|
block_* first = f;
|
||||||
|
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
|
||||||
|
VALGRIND_MALLOCLIKE_BLOCK(f, size, 0, false);
|
||||||
|
// field f->next is initialized: prevents valgrind from complaining
|
||||||
|
// about jumps depending on uninitialized memory
|
||||||
|
VALGRIND_MAKE_MEM_DEFINED(f, sizeof(block_*));
|
||||||
|
#endif
|
||||||
f = f->next;
|
f = f->next;
|
||||||
return first;
|
return first;
|
||||||
}
|
}
|
||||||
|
|
@ -92,6 +99,9 @@ namespace spot
|
||||||
|
|
||||||
void* res = free_start_;
|
void* res = free_start_;
|
||||||
free_start_ += size;
|
free_start_ += size;
|
||||||
|
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
|
||||||
|
VALGRIND_MALLOCLIKE_BLOCK(res, size, 0, false);
|
||||||
|
#endif
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -113,6 +123,9 @@ namespace spot
|
||||||
block_*& f = freelist_[size];
|
block_*& f = freelist_[size];
|
||||||
b->next = f;
|
b->next = f;
|
||||||
f = b;
|
f = b;
|
||||||
|
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
|
||||||
|
VALGRIND_FREELIKE_BLOCK(ptr, 0);
|
||||||
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
private:
|
private:
|
||||||
|
|
|
||||||
|
|
@ -81,6 +81,7 @@ check_PROGRAMS = \
|
||||||
core/ltl2text \
|
core/ltl2text \
|
||||||
core/ltlrel \
|
core/ltlrel \
|
||||||
core/lunabbrev \
|
core/lunabbrev \
|
||||||
|
core/mempool \
|
||||||
core/nequals \
|
core/nequals \
|
||||||
core/nenoform \
|
core/nenoform \
|
||||||
core/ngraph \
|
core/ngraph \
|
||||||
|
|
@ -112,6 +113,7 @@ core_ikwiad_SOURCES = core/ikwiad.cc
|
||||||
core_intvcomp_SOURCES = core/intvcomp.cc
|
core_intvcomp_SOURCES = core/intvcomp.cc
|
||||||
core_intvcmp2_SOURCES = core/intvcmp2.cc
|
core_intvcmp2_SOURCES = core/intvcmp2.cc
|
||||||
core_kripkecat_SOURCES = core/kripkecat.cc
|
core_kripkecat_SOURCES = core/kripkecat.cc
|
||||||
|
core_mempool_SOURCES = core/mempool.cc
|
||||||
core_ngraph_SOURCES = core/ngraph.cc
|
core_ngraph_SOURCES = core/ngraph.cc
|
||||||
core_randtgba_SOURCES = core/randtgba.cc
|
core_randtgba_SOURCES = core/randtgba.cc
|
||||||
core_taatgba_SOURCES = core/taatgba.cc
|
core_taatgba_SOURCES = core/taatgba.cc
|
||||||
|
|
@ -186,6 +188,7 @@ TESTS_tl = \
|
||||||
core/eventuniv.test \
|
core/eventuniv.test \
|
||||||
core/stutter-ltl.test \
|
core/stutter-ltl.test \
|
||||||
core/hierarchy.test \
|
core/hierarchy.test \
|
||||||
|
core/mempool.test \
|
||||||
core/format.test
|
core/format.test
|
||||||
|
|
||||||
TESTS_graph = \
|
TESTS_graph = \
|
||||||
|
|
|
||||||
1
tests/core/.gitignore
vendored
1
tests/core/.gitignore
vendored
|
|
@ -40,6 +40,7 @@ lunabbrev
|
||||||
Makefile
|
Makefile
|
||||||
Makefile.in
|
Makefile.in
|
||||||
maskacc
|
maskacc
|
||||||
|
mempool
|
||||||
mixprod
|
mixprod
|
||||||
nequals
|
nequals
|
||||||
nenoform
|
nenoform
|
||||||
|
|
|
||||||
160
tests/core/mempool.cc
Normal file
160
tests/core/mempool.cc
Normal file
|
|
@ -0,0 +1,160 @@
|
||||||
|
// -*- coding: utf-8 -*-
|
||||||
|
// Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement
|
||||||
|
// de l'Epita.
|
||||||
|
//
|
||||||
|
// This file is part of Spot, a model checking library.
|
||||||
|
//
|
||||||
|
// Spot 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 3 of the License, or
|
||||||
|
// (at your option) any later version.
|
||||||
|
//
|
||||||
|
// Spot 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 this program. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
|
#include "config.h"
|
||||||
|
|
||||||
|
#define SPOT_DEBUG 1
|
||||||
|
|
||||||
|
#include <spot/misc/fixpool.hh>
|
||||||
|
#include <spot/misc/mspool.hh>
|
||||||
|
|
||||||
|
namespace
|
||||||
|
{
|
||||||
|
struct boxint
|
||||||
|
{
|
||||||
|
int i;
|
||||||
|
};
|
||||||
|
|
||||||
|
class foo
|
||||||
|
{
|
||||||
|
boxint* b;
|
||||||
|
public:
|
||||||
|
foo(int i): b(new boxint{i}) {}
|
||||||
|
~foo() { delete b; }
|
||||||
|
|
||||||
|
void incr() { ++b->i; }
|
||||||
|
};
|
||||||
|
|
||||||
|
// use a fixpool for allocation
|
||||||
|
class bar
|
||||||
|
{
|
||||||
|
int i;
|
||||||
|
|
||||||
|
static spot::fixed_size_pool& pool()
|
||||||
|
{
|
||||||
|
static spot::fixed_size_pool p{sizeof(bar)};
|
||||||
|
return p;
|
||||||
|
}
|
||||||
|
|
||||||
|
public:
|
||||||
|
bar(int i): i(i) {}
|
||||||
|
|
||||||
|
static void* operator new(size_t)
|
||||||
|
{
|
||||||
|
return pool().allocate();
|
||||||
|
}
|
||||||
|
static void operator delete(void* ptr)
|
||||||
|
{
|
||||||
|
pool().deallocate(ptr);
|
||||||
|
}
|
||||||
|
|
||||||
|
void incr() { ++i; }
|
||||||
|
};
|
||||||
|
|
||||||
|
// use a mspool for allocation
|
||||||
|
class baz
|
||||||
|
{
|
||||||
|
int i;
|
||||||
|
|
||||||
|
static spot::multiple_size_pool& pool()
|
||||||
|
{
|
||||||
|
static spot::multiple_size_pool p{};
|
||||||
|
return p;
|
||||||
|
}
|
||||||
|
|
||||||
|
public:
|
||||||
|
baz(int i): i(i) {}
|
||||||
|
|
||||||
|
static void* operator new(size_t)
|
||||||
|
{
|
||||||
|
return pool().allocate(sizeof(baz));
|
||||||
|
}
|
||||||
|
static void operator delete(void* ptr)
|
||||||
|
{
|
||||||
|
pool().deallocate(ptr, sizeof(baz));
|
||||||
|
}
|
||||||
|
|
||||||
|
void incr() { ++i; }
|
||||||
|
};
|
||||||
|
|
||||||
|
|
||||||
|
} // anonymous namespace
|
||||||
|
|
||||||
|
|
||||||
|
int main()
|
||||||
|
{
|
||||||
|
|
||||||
|
#ifndef HAVE_VALGRIND_MEMCHECK_H
|
||||||
|
return 77;
|
||||||
|
#endif
|
||||||
|
|
||||||
|
{
|
||||||
|
spot::fixed_size_pool p(sizeof(foo));
|
||||||
|
|
||||||
|
foo* a = new (p.allocate()) foo(1);
|
||||||
|
a->incr();
|
||||||
|
// delete and deallocate, no problem
|
||||||
|
a->~foo();
|
||||||
|
p.deallocate(a);
|
||||||
|
|
||||||
|
a = new (p.allocate()) foo(2);
|
||||||
|
a->incr();
|
||||||
|
// delete but do not deallocate: valgrind should find a leak
|
||||||
|
a->~foo();
|
||||||
|
|
||||||
|
a = new (p.allocate()) foo(3);
|
||||||
|
a->incr();
|
||||||
|
// deallocate but do not delete: valgrind should find a leak
|
||||||
|
p.deallocate(a);
|
||||||
|
}
|
||||||
|
|
||||||
|
{
|
||||||
|
spot::multiple_size_pool p;
|
||||||
|
|
||||||
|
foo* a = new (p.allocate(sizeof(foo))) foo(1);
|
||||||
|
a->incr();
|
||||||
|
// delete and deallocate, no problem
|
||||||
|
a->~foo();
|
||||||
|
p.deallocate(a, sizeof(foo));
|
||||||
|
|
||||||
|
a = new (p.allocate(sizeof(foo))) foo(2);
|
||||||
|
a->incr();
|
||||||
|
// delete but do not deallocate: valgrind should find a leak
|
||||||
|
a->~foo();
|
||||||
|
|
||||||
|
a = new (p.allocate(sizeof(foo))) foo(3);
|
||||||
|
a->incr();
|
||||||
|
// deallocate but do not delete: valgrind should find a leak
|
||||||
|
p.deallocate(a, sizeof(foo));
|
||||||
|
}
|
||||||
|
|
||||||
|
{
|
||||||
|
bar* b = new bar(1);
|
||||||
|
b->incr();
|
||||||
|
// no delete: valgrind should find a leak
|
||||||
|
}
|
||||||
|
{
|
||||||
|
baz* c = new baz(1);
|
||||||
|
c->incr();
|
||||||
|
// no delete: valgrind should find a leak
|
||||||
|
}
|
||||||
|
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
34
tests/core/mempool.test
Normal file
34
tests/core/mempool.test
Normal file
|
|
@ -0,0 +1,34 @@
|
||||||
|
#!/bin/sh
|
||||||
|
# -*- coding: utf-8 -*-
|
||||||
|
# Copyright (C) 2018 Laboratoire de Recherche et Développement de l'Epita.
|
||||||
|
#
|
||||||
|
# This file is part of Spot, a model checking library.
|
||||||
|
#
|
||||||
|
# Spot 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 3 of the License, or
|
||||||
|
# (at your option) any later version.
|
||||||
|
#
|
||||||
|
# Spot 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 this program. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
|
. ./defs
|
||||||
|
|
||||||
|
set -e
|
||||||
|
|
||||||
|
cat >exp <<EOF
|
||||||
|
ERROR SUMMARY: 6 errors from 6 contexts (suppressed: 0 from 0)
|
||||||
|
EOF
|
||||||
|
|
||||||
|
if test -n "$VALGRIND"; then
|
||||||
|
$top_builddir/libtool --mode=execute \
|
||||||
|
$VALGRIND --tool=memcheck --leak-check=yes ../mempool 2> err
|
||||||
|
grep "ERROR SUMMARY" err | sed 's/^==[0-9]*==\s*//' > out
|
||||||
|
diff exp out
|
||||||
|
fi
|
||||||
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue