klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ConstantDivision.cpp
Go to the documentation of this file.
1 //===-- ConstantDivision.cpp ----------------------------------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #include "ConstantDivision.h"
11 
12 #include "klee/util/Bits.h"
13 
14 #include <algorithm>
15 #include <cassert>
16 
17 namespace klee {
18 
19 /* Macros and functions which define the basic bit-level operations
20  * needed to implement quick division operations.
21  *
22  * Based on Hacker's Delight (2003) by Henry S. Warren, Jr.
23  */
24 
25 /* 32 -- number of bits in the integer type on this architecture */
26 
27 /* 2^32 -- NUM_BITS=32 requires 64 bits to represent this unsigned value */
28 #define TWO_TO_THE_32_U64 (1ULL << 32)
29 
30 /* 2e31 -- NUM_BITS=32 requires 64 bits to represent this signed value */
31 #define TWO_TO_THE_31_S64 (1LL << 31)
32 
33 /* ABS(x) -- positive x */
34 #define ABS(x) ( ((x)>0)?x:-(x) ) /* fails if x is the min value of its type */
35 
36 /* XSIGN(x) -- -1 if x<0 and 0 otherwise */
37 #define XSIGN(x) ( (x) >> 31 )
38 
39 /* LOG2_CEIL(x) -- logarithm base 2 of x, rounded up */
40 #define LOG2_CEIL(x) ( 32 - ldz(x - 1) )
41 
42 /* ones(x) -- counts the number of bits in x with the value 1 */
43 static uint32_t ones( register uint32_t x ) {
44  x -= ((x >> 1) & 0x55555555);
45  x = (((x >> 2) & 0x33333333) + (x & 0x33333333));
46  x = (((x >> 4) + x) & 0x0f0f0f0f);
47  x += (x >> 8);
48  x += (x >> 16);
49 
50  return( x & 0x0000003f );
51 }
52 
53 /* ldz(x) -- counts the number of leading zeroes in a 32-bit word */
54 static uint32_t ldz( register uint32_t x ) {
55  x |= (x >> 1);
56  x |= (x >> 2);
57  x |= (x >> 4);
58  x |= (x >> 8);
59  x |= (x >> 16);
60 
61  return 32 - ones(x);
62 }
63 
64 /* exp_base_2(n) -- 2^n computed as an integer */
65 static uint32_t exp_base_2( register int32_t n ) {
66  register uint32_t x = ~n & (n - 32);
67  x = x >> 31;
68  return( x << n );
69 }
70 
71 // A simple algorithm: Iterate over all contiguous regions of 1 bits
72 // in x starting with the lowest bits.
73 //
74 // For a particular range where x is 1 for bits [low,high) then:
75 // 1) if the range is just one bit, simple add it
76 // 2) if the range is more than one bit, replace with an add
77 // of the high bit and a subtract of the low bit. we apply
78 // one useful optimization: if we were going to add the bit
79 // below the one we wish to subtract, we simply change that
80 // add to a subtract instead of subtracting the low bit itself.
81 // Obviously we must take care when high==64.
82 void ComputeMultConstants64(uint64_t multiplicand,
83  uint64_t &add, uint64_t &sub) {
84  uint64_t x = multiplicand;
85  add = sub = 0;
86 
87  while (x) {
88  // Determine rightmost contiguous region of 1s.
89  unsigned low = bits64::indexOfRightmostBit(x);
90  uint64_t lowbit = 1LL << low;
91  uint64_t p = x + lowbit;
92  uint64_t q = bits64::isolateRightmostBit(p);
93  unsigned high = q ? bits64::indexOfSingleBit(q) : 64;
94 
95  if (high==low+1) { // Just one bit...
96  add |= lowbit;
97  } else {
98  // Rewrite as +(1<<high) - (1<<low).
99 
100  // Optimize +(1<<x) - (1<<(x+1)) to -(1<<x).
101  if (low && (add & (lowbit>>1))) {
102  add ^= lowbit>>1;
103  sub ^= lowbit>>1;
104  } else {
105  sub |= lowbit;
106  }
107 
108  if (high!=64)
109  add |= 1LL << high;
110  }
111 
112  x = p ^ q;
113  }
114 
115  assert(multiplicand == add - sub);
116 }
117 
118 void ComputeUDivConstants32(uint32_t d, uint32_t &mprime, uint32_t &sh1,
119  uint32_t &sh2) {
120  int32_t l = LOG2_CEIL( d ); /* signed so l-1 => -1 when l=0 (see sh2) */
121  uint32_t mid = exp_base_2(l) - d;
122 
123  mprime = (TWO_TO_THE_32_U64 * mid / d) + 1;
124  sh1 = std::min( l, 1 );
125  sh2 = std::max( l-1, 0 );
126 }
127 
128 void ComputeSDivConstants32(int32_t d, int32_t &mprime, int32_t &dsign,
129  int32_t &shpost ) {
130  uint64_t abs_d = ABS( (int64_t)d ); /* use 64-bits in case d is INT32_MIN */
131 
132  /* LOG2_CEIL works on 32-bits, so we cast abs_d. The only possible value
133  * outside the 32-bit rep. is 2^31. This is special cased to save computer
134  * time since 64-bit routines would be overkill. */
135  int32_t l = std::max( 1U, LOG2_CEIL((uint32_t)abs_d) );
136  if( abs_d == TWO_TO_THE_31_S64 ) l = 31;
137 
138  uint32_t mid = exp_base_2( l - 1 );
139  uint64_t m = TWO_TO_THE_32_U64 * mid / abs_d + 1ULL;
140 
141  mprime = m - TWO_TO_THE_32_U64; /* implicit cast to 32-bits signed */
142  dsign = XSIGN( d );
143  shpost = l - 1;
144 }
145 
146 }
#define TWO_TO_THE_31_S64
void ComputeMultConstants64(uint64_t multiplicand, uint64_t &add, uint64_t &sub)
static uint32_t ldz(register uint32_t x)
#define XSIGN(x)
#define TWO_TO_THE_32_U64
uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth)
#define add(name, handler, ret)
void ComputeUDivConstants32(uint32_t d, uint32_t &mprime, uint32_t &sh1, uint32_t &sh2)
#define ABS(x)
uint64_t isolateRightmostBit(uint64_t x)
Definition: Bits.h:79
unsigned indexOfSingleBit(uint64_t x)
Definition: Bits.h:90
static uint32_t ones(register uint32_t x)
#define LOG2_CEIL(x)
void ComputeSDivConstants32(int32_t d, int32_t &mprime, int32_t &dsign, int32_t &shpost)
uint64_t indexOfRightmostBit(uint64_t x)
Definition: Bits.h:97
static uint32_t exp_base_2(register int32_t n)