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