klee
Bits.h
Go to the documentation of this file.
1//===-- Bits.h --------------------------------------------------*- C++ -*-===//
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#ifndef KLEE_BITS_H
11#define KLEE_BITS_H
12
13#include "klee/Config/Version.h"
14#include "llvm/Support/DataTypes.h"
15#include <assert.h>
16
17namespace klee {
18 namespace bits32 {
19 // @pre(0 <= N <= 32)
20 // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
21 inline unsigned maxValueOfNBits(unsigned N) {
22 assert(N <= 32);
23 if (N==0)
24 return 0;
25 return (UINT32_C(-1)) >> (32 - N);
26 }
27
28 // @pre(0 < N <= 32)
29 inline unsigned truncateToNBits(unsigned x, unsigned N) {
30 assert(N > 0 && N <= 32);
31 return x&((UINT32_C(-1)) >> (32 - N));
32 }
33
34 inline unsigned withoutRightmostBit(unsigned x) {
35 return x&(x-1);
36 }
37
38 inline unsigned isolateRightmostBit(unsigned x) {
39 return x&-x;
40 }
41
42 inline unsigned isPowerOfTwo(unsigned x) {
43 if (x==0) return 0;
44 return !(x&(x-1));
45 }
46
47 // @pre(withoutRightmostBit(x) == 0)
48 // @post((1 << retval) == x)
49 inline unsigned indexOfSingleBit(unsigned x) {
50 assert(withoutRightmostBit(x) == 0);
51 unsigned res = 0;
52 if (x&0xFFFF0000) res += 16;
53 if (x&0xFF00FF00) res += 8;
54 if (x&0xF0F0F0F0) res += 4;
55 if (x&0xCCCCCCCC) res += 2;
56 if (x&0xAAAAAAAA) res += 1;
57 assert(res < 32);
58 assert((UINT32_C(1) << res) == x);
59 return res;
60 }
61
62 inline unsigned indexOfRightmostBit(unsigned x) {
64 }
65 }
66
67 namespace bits64 {
68 // @pre(0 <= N <= 64)
69 // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
70 inline uint64_t maxValueOfNBits(unsigned N) {
71 assert(N <= 64);
72 if (N==0)
73 return 0;
74 return ((UINT64_C(-1)) >> (64 - N));
75 }
76
77 // @pre(0 < N <= 64)
78 inline uint64_t truncateToNBits(uint64_t x, unsigned N) {
79 assert(N > 0 && N <= 64);
80 return x&((UINT64_C(-1)) >> (64 - N));
81 }
82
83 inline uint64_t withoutRightmostBit(uint64_t x) {
84 return x&(x-1);
85 }
86
87 inline uint64_t isolateRightmostBit(uint64_t x) {
88 return x&-x;
89 }
90
91 inline uint64_t isPowerOfTwo(uint64_t x) {
92 if (x==0) return 0;
93 return !(x&(x-1));
94 }
95
96 // @pre((x&(x-1)) == 0)
97 // @post((1 << retval) == x)
98 inline unsigned indexOfSingleBit(uint64_t x) {
99 assert((x & (x - 1)) == 0);
100 unsigned res = bits32::indexOfSingleBit((unsigned) (x | (x>>32)));
101 if (x & (UINT64_C(0xFFFFFFFF) << 32))
102 res += 32;
103 assert(res < 64);
104 assert((UINT64_C(1) << res) == x);
105 return res;
106 }
107
108 inline uint64_t indexOfRightmostBit(uint64_t x) {
110 }
111 }
112} // End klee namespace
113
114#endif /* KLEE_BITS_H */
unsigned indexOfRightmostBit(unsigned x)
Definition: Bits.h:62
unsigned withoutRightmostBit(unsigned x)
Definition: Bits.h:34
unsigned maxValueOfNBits(unsigned N)
Definition: Bits.h:21
unsigned indexOfSingleBit(unsigned x)
Definition: Bits.h:49
unsigned isolateRightmostBit(unsigned x)
Definition: Bits.h:38
unsigned isPowerOfTwo(unsigned x)
Definition: Bits.h:42
unsigned truncateToNBits(unsigned x, unsigned N)
Definition: Bits.h:29
uint64_t truncateToNBits(uint64_t x, unsigned N)
Definition: Bits.h:78
uint64_t isolateRightmostBit(uint64_t x)
Definition: Bits.h:87
uint64_t maxValueOfNBits(unsigned N)
Definition: Bits.h:70
unsigned indexOfSingleBit(uint64_t x)
Definition: Bits.h:98
uint64_t indexOfRightmostBit(uint64_t x)
Definition: Bits.h:108
uint64_t withoutRightmostBit(uint64_t x)
Definition: Bits.h:83
uint64_t isPowerOfTwo(uint64_t x)
Definition: Bits.h:91
Definition: main.cpp:291