klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
IntEvaluation.h
Go to the documentation of this file.
1 //===-- IntEvaluation.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_UTIL_INTEVALUATION_H
11 #define KLEE_UTIL_INTEVALUATION_H
12 
13 #include "klee/util/Bits.h"
14 
15 #define MAX_BITS (sizeof(uint64_t) * 8)
16 
17 // ASSUMPTION: invalid bits in each uint64_t are 0. the trade-off here is
18 // between making trunc/zext/sext fast and making operations that depend
19 // on the invalid bits being 0 fast.
20 
21 namespace klee {
22 namespace ints {
23 
24 // add of l and r
25 inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) {
26  return bits64::truncateToNBits(l + r, inWidth);
27 }
28 
29 // difference of l and r
30 inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) {
31  return bits64::truncateToNBits(l - r, inWidth);
32 }
33 
34 // product of l and r
35 inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) {
36  return bits64::truncateToNBits(l * r, inWidth);
37 }
38 
39 // truncation of l to outWidth bits
40 inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) {
41  return bits64::truncateToNBits(l, outWidth);
42 }
43 
44 // zero-extension of l from inWidth to outWidth bits
45 inline uint64_t zext(uint64_t l, unsigned outWidth, unsigned inWidth) {
46  return l;
47 }
48 
49 // sign-extension of l from inWidth to outWidth bits
50 inline uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth) {
51  uint32_t numInvalidBits = MAX_BITS - inWidth;
52  return bits64::truncateToNBits(((int64_t)(l << numInvalidBits)) >> numInvalidBits, outWidth);
53 }
54 
55 // unsigned divide of l by r
56 inline uint64_t udiv(uint64_t l, uint64_t r, unsigned inWidth) {
57  return bits64::truncateToNBits(l / r, inWidth);
58 }
59 
60 // unsigned mod of l by r
61 inline uint64_t urem(uint64_t l, uint64_t r, unsigned inWidth) {
62  return bits64::truncateToNBits(l % r, inWidth);
63 }
64 
65 // signed divide of l by r
66 inline uint64_t sdiv(uint64_t l, uint64_t r, unsigned inWidth) {
67  // sign extend operands so that signed operation on 64-bits works correctly
68  int64_t sl = sext(l, MAX_BITS, inWidth);
69  int64_t sr = sext(r, MAX_BITS, inWidth);
70  return bits64::truncateToNBits(sl / sr, inWidth);
71 }
72 
73 // signed mod of l by r
74 inline uint64_t srem(uint64_t l, uint64_t r, unsigned inWidth) {
75  // sign extend operands so that signed operation on 64-bits works correctly
76  int64_t sl = sext(l, MAX_BITS, inWidth);
77  int64_t sr = sext(r, MAX_BITS, inWidth);
78  return bits64::truncateToNBits(sl % sr, inWidth);
79 }
80 
81 // arithmetic shift right of l by r bits
82 inline uint64_t ashr(uint64_t l, uint64_t shift, unsigned inWidth) {
83  int64_t sl = sext(l, MAX_BITS, inWidth);
84  return bits64::truncateToNBits(sl >> shift, inWidth);
85 }
86 
87 // logical shift right of l by r bits
88 inline uint64_t lshr(uint64_t l, uint64_t shift, unsigned inWidth) {
89  return l >> shift;
90 }
91 
92 // shift left of l by r bits
93 inline uint64_t shl(uint64_t l, uint64_t shift, unsigned inWidth) {
94  return bits64::truncateToNBits(l << shift, inWidth);
95 }
96 
97 // logical AND of l and r
98 inline uint64_t land(uint64_t l, uint64_t r, unsigned inWidth) {
99  return l & r;
100 }
101 
102 // logical OR of l and r
103 inline uint64_t lor(uint64_t l, uint64_t r, unsigned inWidth) {
104  return l | r;
105 }
106 
107 // logical XOR of l and r
108 inline uint64_t lxor(uint64_t l, uint64_t r, unsigned inWidth) {
109  return l ^ r;
110 }
111 
112 // comparison operations
113 inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) {
114  return l == r;
115 }
116 
117 inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) {
118  return l != r;
119 }
120 
121 inline uint64_t ult(uint64_t l, uint64_t r, unsigned inWidth) {
122  return l < r;
123 }
124 
125 inline uint64_t ule(uint64_t l, uint64_t r, unsigned inWidth) {
126  return l <= r;
127 }
128 
129 inline uint64_t ugt(uint64_t l, uint64_t r, unsigned inWidth) {
130  return l > r;
131 }
132 
133 inline uint64_t uge(uint64_t l, uint64_t r, unsigned inWidth) {
134  return l >= r;
135 }
136 
137 inline uint64_t slt(uint64_t l, uint64_t r, unsigned inWidth) {
138  int64_t sl = sext(l, MAX_BITS, inWidth);
139  int64_t sr = sext(r, MAX_BITS, inWidth);
140  return sl < sr;
141 }
142 
143 inline uint64_t sle(uint64_t l, uint64_t r, unsigned inWidth) {
144  int64_t sl = sext(l, MAX_BITS, inWidth);
145  int64_t sr = sext(r, MAX_BITS, inWidth);
146  return sl <= sr;
147 }
148 
149 inline uint64_t sgt(uint64_t l, uint64_t r, unsigned inWidth) {
150  int64_t sl = sext(l, MAX_BITS, inWidth);
151  int64_t sr = sext(r, MAX_BITS, inWidth);
152  return sl > sr;
153 }
154 
155 inline uint64_t sge(uint64_t l, uint64_t r, unsigned inWidth) {
156  int64_t sl = sext(l, MAX_BITS, inWidth);
157  int64_t sr = sext(r, MAX_BITS, inWidth);
158  return sl >= sr;
159 }
160 
161 } // end namespace ints
162 } // end namespace klee
163 
164 #endif
uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth)
Definition: IntEvaluation.h:30
uint64_t zext(uint64_t l, unsigned outWidth, unsigned inWidth)
Definition: IntEvaluation.h:45
uint64_t add(uint64_t l, uint64_t r, unsigned inWidth)
Definition: IntEvaluation.h:25
uint64_t ugt(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t sle(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth)
Definition: IntEvaluation.h:35
uint64_t sdiv(uint64_t l, uint64_t r, unsigned inWidth)
Definition: IntEvaluation.h:66
uint64_t srem(uint64_t l, uint64_t r, unsigned inWidth)
Definition: IntEvaluation.h:74
uint64_t lor(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t slt(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t sgt(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t land(uint64_t l, uint64_t r, unsigned inWidth)
Definition: IntEvaluation.h:98
uint64_t sge(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t ule(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t uge(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t lshr(uint64_t l, uint64_t shift, unsigned inWidth)
Definition: IntEvaluation.h:88
uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth)
Definition: IntEvaluation.h:40
uint64_t ult(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth)
Definition: IntEvaluation.h:50
uint64_t urem(uint64_t l, uint64_t r, unsigned inWidth)
Definition: IntEvaluation.h:61
uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t truncateToNBits(uint64_t x, unsigned N)
Definition: Bits.h:71
#define MAX_BITS
Definition: IntEvaluation.h:15
uint64_t ashr(uint64_t l, uint64_t shift, unsigned inWidth)
Definition: IntEvaluation.h:82
uint64_t lxor(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t udiv(uint64_t l, uint64_t r, unsigned inWidth)
Definition: IntEvaluation.h:56
uint64_t shl(uint64_t l, uint64_t shift, unsigned inWidth)
Definition: IntEvaluation.h:93