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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
//===-- IntEvaluation.h -----------------------------------------*- C++ -*-===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#ifndef KLEE_INTEVALUATION_H
#define KLEE_INTEVALUATION_H
#include "klee/ADT/Bits.h"
#define MAX_BITS (sizeof(uint64_t) * 8)
// ASSUMPTION: invalid bits in each uint64_t are 0. the trade-off here is
// between making trunc/zext/sext fast and making operations that depend
// on the invalid bits being 0 fast.
namespace klee {
namespace ints {
// add of l and r
inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) {
return bits64::truncateToNBits(l + r, inWidth);
}
// difference of l and r
inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) {
return bits64::truncateToNBits(l - r, inWidth);
}
// product of l and r
inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) {
return bits64::truncateToNBits(l * r, inWidth);
}
// truncation of l to outWidth bits
inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) {
return bits64::truncateToNBits(l, outWidth);
}
// zero-extension of l from inWidth to outWidth bits
inline uint64_t zext(uint64_t l, unsigned outWidth, unsigned inWidth) {
return l;
}
// sign-extension of l from inWidth to outWidth bits
inline uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth) {
uint32_t numInvalidBits = MAX_BITS - inWidth;
return bits64::truncateToNBits(((int64_t)(l << numInvalidBits)) >> numInvalidBits, outWidth);
}
// unsigned divide of l by r
inline uint64_t udiv(uint64_t l, uint64_t r, unsigned inWidth) {
return bits64::truncateToNBits(l / r, inWidth);
}
// unsigned mod of l by r
inline uint64_t urem(uint64_t l, uint64_t r, unsigned inWidth) {
return bits64::truncateToNBits(l % r, inWidth);
}
// signed divide of l by r
inline uint64_t sdiv(uint64_t l, uint64_t r, unsigned inWidth) {
// sign extend operands so that signed operation on 64-bits works correctly
int64_t sl = sext(l, MAX_BITS, inWidth);
int64_t sr = sext(r, MAX_BITS, inWidth);
return bits64::truncateToNBits(sl / sr, inWidth);
}
// signed mod of l by r
inline uint64_t srem(uint64_t l, uint64_t r, unsigned inWidth) {
// sign extend operands so that signed operation on 64-bits works correctly
int64_t sl = sext(l, MAX_BITS, inWidth);
int64_t sr = sext(r, MAX_BITS, inWidth);
return bits64::truncateToNBits(sl % sr, inWidth);
}
// arithmetic shift right of l by r bits
inline uint64_t ashr(uint64_t l, uint64_t shift, unsigned inWidth) {
int64_t sl = sext(l, MAX_BITS, inWidth);
return bits64::truncateToNBits(sl >> shift, inWidth);
}
// logical shift right of l by r bits
inline uint64_t lshr(uint64_t l, uint64_t shift, unsigned inWidth) {
return l >> shift;
}
// shift left of l by r bits
inline uint64_t shl(uint64_t l, uint64_t shift, unsigned inWidth) {
return bits64::truncateToNBits(l << shift, inWidth);
}
// logical AND of l and r
inline uint64_t land(uint64_t l, uint64_t r, unsigned inWidth) {
return l & r;
}
// logical OR of l and r
inline uint64_t lor(uint64_t l, uint64_t r, unsigned inWidth) {
return l | r;
}
// logical XOR of l and r
inline uint64_t lxor(uint64_t l, uint64_t r, unsigned inWidth) {
return l ^ r;
}
// comparison operations
inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) {
return l == r;
}
inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) {
return l != r;
}
inline uint64_t ult(uint64_t l, uint64_t r, unsigned inWidth) {
return l < r;
}
inline uint64_t ule(uint64_t l, uint64_t r, unsigned inWidth) {
return l <= r;
}
inline uint64_t ugt(uint64_t l, uint64_t r, unsigned inWidth) {
return l > r;
}
inline uint64_t uge(uint64_t l, uint64_t r, unsigned inWidth) {
return l >= r;
}
inline uint64_t slt(uint64_t l, uint64_t r, unsigned inWidth) {
int64_t sl = sext(l, MAX_BITS, inWidth);
int64_t sr = sext(r, MAX_BITS, inWidth);
return sl < sr;
}
inline uint64_t sle(uint64_t l, uint64_t r, unsigned inWidth) {
int64_t sl = sext(l, MAX_BITS, inWidth);
int64_t sr = sext(r, MAX_BITS, inWidth);
return sl <= sr;
}
inline uint64_t sgt(uint64_t l, uint64_t r, unsigned inWidth) {
int64_t sl = sext(l, MAX_BITS, inWidth);
int64_t sr = sext(r, MAX_BITS, inWidth);
return sl > sr;
}
inline uint64_t sge(uint64_t l, uint64_t r, unsigned inWidth) {
int64_t sl = sext(l, MAX_BITS, inWidth);
int64_t sr = sext(r, MAX_BITS, inWidth);
return sl >= sr;
}
} // end namespace ints
} // end namespace klee
#endif /* KLEE_INTEVALUATION_H */
|
