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