From 74740dc894ad50f4aa44a2c82b72a17501f11e0a Mon Sep 17 00:00:00 2001
From: Henner Zeller <hzeller@google.com>
Date: Mon, 21 Nov 2022 12:36:41 -0800
Subject: [PATCH] Fix undefined behavior in signed/unsigned shifting.

Discovered by UBSAN as invalid attempts at shifting signed integers.

Signed-off-by: Henner Zeller <hzeller@google.com>
---
 src/aig/aig/aig.h        | 2 +-
 src/bool/kit/kit.h       | 8 ++++----
 src/sat/bsat/satSolver.c | 9 +++++----
 3 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index e92e512c4..5285ae72b 100644
--- a/src/aig/aig/aig.h
+++ b/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);
diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h
index ee82b0841..3be9b14f8 100644
--- a/src/bool/kit/kit.h
+++ b/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;                  }
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 2f3a84db7..eea280293 100644
--- a/src/sat/bsat/satSolver.c
+++ b/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 );
         }