* src/bddop.c, src/bddx.h, src/cache.c, src/cache.h, src/kernel.c,
src/kernel.h, src/prime.c, src/prime.h, src/reorder.c: Use power of
two for the sizes of all hash tables, in order to reduce the amount of
divisions performed. Also allow bddhash to be smaller than bddnodes.
* src/fdd.c (fdd_intaddvarblock): Add missing addref.
Signed-off-by: Jaco van de Pol <J.C.vandepol@ewi.utwente.nl>
Signed-off-by: Michael Weber <michaelw@cs.utwente.nl>
* m4/gccwarns.m4: Add -Wno-gnu to workaround a diagnostic from
clang 3.9.1 on arch Linux. clang was complaining whtat assert()
is using a GNU extension.
* src/bddop.c: Empty macro arguments are undefined ISO C90 and
ISO C++98. Use '+' when calling APPLY_SHORTCUTS.
* src/fdd.c, src/kernel.c: Avoid constructs invalid in C90.
* src/bddop.c, src/bddx.h, src/kernel.c, src/kernel.h,
examples/cmilner/cmilner.c: Remove C++ comments.
This avoids dynamic lookups to resolve symbols inside the library, but
disallows symbol interposition.
* m4/symbolic.m4: New file.
* buddy/m4/symbolic.m4: New link.
* configure.ac, buddy/configure.ac: Add AX_SYMBOLIC.
* buddy/src/Makefile.am, iface/ltsmin/Makefile.am, src/Makefile.am,
wrap/python/Makefile.am: Link with $(SYMBOLIC_LDFLAGS).
The bug was found while running Spot's src/tgbatest/randpsl.test
on Debian i386 with gcc-4.9.2. The following call would crash:
./ltl2tgba -R3 -t '(!(F(({{{(p0) |
{[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) &
(G((!(p1)) | ((!(p2)) W (G(!(p0)))))))))'
On amd64 the call does not crash, but valgrind nonetheless
report that uninitialized memory is being read by bdd_gbc()
during the second garbage collect.
* src/kernel.h (PUSHREF): Define as a function rather than a macro
to avoid undefined behavior. See comments for details.
The double result is never used with a triple keys,
so we can pack the cache entry more tightly.
* src/cache.h: Reorganize the cache entry the structure.
* src/cache.c: Cleanup the code while we are at it.
* src/bddop.c: Adjust to accesses to cache entries.
This can only cause failure when running under valgrind (i.e., in the
test suite), but is not a problem in practice as the test is certain
to fail the entry->c check whenever entry->b is uninitialized.
* src/bddop.c (bdd_implies): Here.
* configure.ac: Enable C++11 mode.
* src/bdd.h: Use noexport, and add a move constructor and
move assignment operator. The move version of these method
do not have to increment the reference counter, saving time.
On a small test run, this change saved 24% of the calls to
bdd_addref_nc().
* configure.ac: Check gcc and g++ for -fvisibility and
-fvisibility-inlines-hidden. Add these options to
CFLAGS and CXXFLAGS.
* m4/ax_check_compile_flag.m4: New file.
* src/Makefile.am: Build BuDDy as a single library, reverting part of
the changes introduced in my previous patch to this file. Since
the options are set in CFLAGS/CXXFLAGS, there is no possibility
for -fvisibility-inlines-hidden to be passed to the C compiler.
* src/bdd.h, src/bvec.h, src/fdd.h: Declare all exported
symbols using BUDDY_API, a new macro that sets visibility=default.
* src/Makefile.am: Compile with -fvisibility=hidden by default,
and compile the C++ part with -fvisibility-inlines-hidden as well.
The unicity table was mixed with the bddNode table for now
apparent reason. After the hash of some node is computed,
bddnodes[hash] did only contain some random node (not the one
looked for) whose .hash member would point to the actual node with
this hash. So that's a two step lookup. With this patch, we sill
have a two step lookup, but the .hash member have been moved to a
separate array. A consequence is that bddNode is now 16-byte long
(instead of 20) so it will never span across two cache lines.
* src/kernel.h (bddNode): Remove the hash member, and move it...
(bddhash): ... as this new separate table.
* src/kernel.c, src/reorder.c: Adjust all code.
* examples/bddcalc/parser.yxx: Rename as ...
* examples/bddcalc/parser.y: ... this.
* examples/bddcalc/parser_.cxx: New file that includes parser.c.
* examples/bddcalc/Makefile.am: Adjust.
* examples/bddcalc/parser.hxx: Delete this unused file.
BddCache_lookup return an entry from a Not operation.
* src/bddop.c (apply_rec, simplify_rec): When checking the cache
entry, always check entry->a and entry->c before checking
entry->b, because the "not_rec()" function does not initialize
the latter.
This avoids a library call to bdd_addref or bdd_delref.
* src/kernel.c (bdd_delref_nc, bdd_addref_nc): New function,
that work only on BDD that are not constant.
* src/cpext.cxx (bdd::operator=): Move...
* src/bdd.hh (bdd::operator=): ... here.
(bdd::bdd, bdd::~bdd, bdd::operator=): Inline the "is bdd constant"
check and call bdd_delref_nc/bdd_addref_nc only otherwise.
