Merge pull request #196 from hzeller/20221121-fix-ub

Fix undefined behavior in signed/unsigned shifting.

src/aig/aig/aig.h

@@ -225,7 +225,7 @@ static inline Aig_Cut_t *  Aig_CutNext( Aig_Cut_t * pCut )              { return
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline unsigned     Aig_ObjCutSign( unsigned ObjId )       { return (1 << (ObjId & 31));                            }
+static inline unsigned     Aig_ObjCutSign( unsigned ObjId )       { return (1U << (ObjId & 31));                            }
 static inline int          Aig_WordCountOnes( unsigned uWord )
 {
     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);

src/bool/kit/kit.h

@@ -175,10 +175,10 @@ static inline unsigned        Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )
 #define KIT_MAX(a,b)       (((a) > (b))? (a) : (b))
 #define KIT_INFINITY       (100000000)
 
-static inline int          Kit_CubeHasLit( unsigned uCube, int i )                        { return(uCube &  (unsigned)(1<<i)) > 0;  }
-static inline unsigned     Kit_CubeSetLit( unsigned uCube, int i )                        { return uCube |  (unsigned)(1<<i);       }
-static inline unsigned     Kit_CubeXorLit( unsigned uCube, int i )                        { return uCube ^  (unsigned)(1<<i);       }
-static inline unsigned     Kit_CubeRemLit( unsigned uCube, int i )                        { return uCube & ~(unsigned)(1<<i);       }
+static inline int          Kit_CubeHasLit( unsigned uCube, int i )                        { return(uCube &  (unsigned)(1U<<i)) > 0;  }
+static inline unsigned     Kit_CubeSetLit( unsigned uCube, int i )                        { return uCube |  (unsigned)(1U<<i);       }
+static inline unsigned     Kit_CubeXorLit( unsigned uCube, int i )                        { return uCube ^  (unsigned)(1U<<i);       }
+static inline unsigned     Kit_CubeRemLit( unsigned uCube, int i )                        { return uCube & ~(unsigned)(1U<<i);       }
 
 static inline int          Kit_CubeContains( unsigned uLarge, unsigned uSmall )           { return (uLarge & uSmall) == uSmall;     }
 static inline unsigned     Kit_CubeSharp( unsigned uCube, unsigned uMask )                { return uCube & ~uMask;                  }

src/sat/bsat/satSolver.c

@@ -511,13 +511,14 @@ static void sortrnd(void** array, int size, int(*comp)(const void *, const void
 
 static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
 {
-    int i, lev, minl = 0, lbd = 0;
-    for (i = 0; i < (int)c->size; i++)
+    unsigned int i, lev, minl = 0;
+    int lbd = 0;
+    for (i = 0; i < c->size; i++)
     {
         lev = var_level(s, lit_var(c->lits[i]));
-        if ( !(minl & (1 << (lev & 31))) )
+        if ( !(minl & (1U << (lev & 31))) )
         {
-            minl |= 1 << (lev & 31);
+            minl |= 1U << (lev & 31);
             lbd++;
 //            printf( "%d ", lev );
         }