From 787e3f93151d33c504c93ce9d3d789fe0ab7cc30 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 Mar 2015 15:44:08 +0100 Subject: [PATCH] [buddy] fix undefined behavior 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. --- buddy/src/kernel.h | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/buddy/src/kernel.h b/buddy/src/kernel.h index 759d1cd07..10799c977 100644 --- a/buddy/src/kernel.h +++ b/buddy/src/kernel.h @@ -170,7 +170,33 @@ extern bddCacheStat bddcachestats; /* Stacking for garbage collector */ #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 POPREF(a) bddrefstacktop -= (a)