alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[buddy] fix undefined behavior

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2015-03-10 15:44:08 +01:00
parent ffabbfb048
commit 787e3f9315
1 changed files with 27 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

28
buddy/src/kernel.h
View file

@ -170,7 +170,33 @@ extern bddCacheStat bddcachestats;
/* Stacking for garbage collector */ /* Stacking for garbage collector */
#define INITREF bddrefstacktop = bddrefstack #define INITREF bddrefstacktop = bddrefstack
#define PUSHREF(a) *(bddrefstacktop++) = (a) /*
** The following (original) definition of PUSHREF is incorrect
** when (a) can trigger a garbage collect:
**
** #define PUSHREF(a) *(bddrefstacktop++) = (a)
**
** The reason is that bddrefstacktop can be incremented before computing
** (a) and assigning its value to bddrefstacktop[-1]. So if the garbage
** collector is triggered during the computation of (a), it will find
** uninitialized values in the stack.
**
** Such a situation occur in most algorithms of the form:
**
** static int restrict_rec(int r) {
** // ...
** PUSHREF( restrict_rec(LOW(r)) );
** PUSHREF( restrict_rec(HIGH(r)) );
** res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
** POPREF(2);
**
** Using a function forces the value of a to be computed before pushing
** it to the stack.
*/
static inline int PUSHREF(int a)
{
return *bddrefstacktop++ = a;
}
#define READREF(a) *(bddrefstacktop-(a)) #define READREF(a) *(bddrefstacktop-(a))
#define POPREF(a) bddrefstacktop -= (a) #define POPREF(a) bddrefstacktop -= (a)