Cleanup pointer arithmetic for storing information in pointers.

Boolector · Oct 10, 2019 · 66d0f7b · 66d0f7b
1 parent 5a3b5c8
commit 66d0f7b
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 15 deletions.
diff --git a/src/btoraig.h b/src/btoraig.h
@@ -74,17 +74,18 @@ typedef struct BtorAIGMgr BtorAIGMgr;
 
 /*------------------------------------------------------------------------*/
 
-#define BTOR_AIG_FALSE ((BtorAIG *) 0ul)
+#define BTOR_AIG_FALSE ((BtorAIG *) (uintptr_t) 0)
 
-#define BTOR_AIG_TRUE ((BtorAIG *) 1ul)
+#define BTOR_AIG_TRUE ((BtorAIG *) (uintptr_t) 1)
 
-#define BTOR_INVERT_AIG(aig) ((BtorAIG *) (1ul ^ (uintptr_t) (aig)))
+#define BTOR_INVERT_AIG(aig) ((BtorAIG *) ((uintptr_t) 1 ^ (uintptr_t) (aig)))
 
-#define BTOR_IS_INVERTED_AIG(aig) (1ul & (uintptr_t) (aig))
+#define BTOR_IS_INVERTED_AIG(aig) ((uintptr_t) 1 & (uintptr_t) (aig))
 
-#define BTOR_REAL_ADDR_AIG(aig) ((BtorAIG *) (~1ul & (uintptr_t) (aig)))
+#define BTOR_REAL_ADDR_AIG(aig) \
+  ((BtorAIG *) ((~(uintptr_t) 1) & (uintptr_t) (aig)))
 
-#define BTOR_IS_REGULAR_AIG(aig) (!(1ul & (uintptr_t) (aig)))
+#define BTOR_IS_REGULAR_AIG(aig) (!((uintptr_t) 1 & (uintptr_t) (aig)))
 
 /*------------------------------------------------------------------------*/
 

diff --git a/src/btornode.h b/src/btornode.h
@@ -208,37 +208,38 @@ typedef struct BtorArgsNode BtorArgsNode;
 static inline BtorNode *
 btor_node_set_tag (BtorNode *node, uintptr_t tag)
 {
+  assert (tag <= 3);
   return (BtorNode *) (tag | (uintptr_t) node);
 }
 
 static inline BtorNode *
 btor_node_invert (const BtorNode *node)
 {
-  return (BtorNode *) (1ul ^ (uintptr_t) node);
+  return (BtorNode *) ((uintptr_t) 1 ^ (uintptr_t) node);
 }
 
 static inline BtorNode *
 btor_node_cond_invert (const BtorNode *cond, const BtorNode *node)
 {
-  return (BtorNode *) (((uintptr_t) cond & 1ul) ^ (uintptr_t) node);
+  return (BtorNode *) (((uintptr_t) cond & (uintptr_t) 1) ^ (uintptr_t) node);
 }
 
 static inline bool
 btor_node_is_inverted (const BtorNode *node)
 {
-  return (1ul & (uintptr_t) node) != 0;
+  return ((uintptr_t) 1 & (uintptr_t) node) != 0;
 }
 
 static inline BtorNode *
 btor_node_real_addr (const BtorNode *node)
 {
-  return (BtorNode *) (~3ul & (uintptr_t) node);
+  return (BtorNode *) (~(uintptr_t) 3 & (uintptr_t) node);
 }
 
 static inline bool
 btor_node_is_regular (const BtorNode *node)
 {
-  return (3ul & (uintptr_t) node) == 0;
+  return ((uintptr_t) 3 & (uintptr_t) node) == 0;
 }
 
 static inline bool
@@ -541,7 +542,7 @@ btor_node_get_id (const BtorNode *exp)
 static inline int32_t
 btor_node_get_tag (const BtorNode *exp)
 {
-  return (int32_t) (3ul & (uintptr_t) exp);
+  return (int32_t) ((uintptr_t) 3 & (uintptr_t) exp);
 }
 
 /*========================================================================*/

diff --git a/src/parser/btorsmt.c b/src/parser/btorsmt.c
@@ -243,9 +243,9 @@ cdr (BtorSMTNode *node)
   return node->tail;
 }
 
-#define isleaf(l) (1lu & (unsigned long) (l))
-#define leaf(l) ((void *) (1lu | (unsigned long) (l)))
-#define strip(l) ((BtorSMTSymbol *) ((~1lu) & (unsigned long) (l)))
+#define isleaf(l) ((uintptr_t) 1 & (uintptr_t) (l))
+#define leaf(l) ((void *) ((uintptr_t) 1 | (uintptr_t) (l)))
+#define strip(l) ((BtorSMTSymbol *) ((~(uintptr_t) 1) & (uintptr_t) (l)))
 
 static BtorSMTNode *
 cons (BtorSMTParser *parser, void *h, void *t)