klee
ArrayExprOptimizer.cpp
Go to the documentation of this file.
1//===-- ArrayExprOptimizer.cpp --------------------------------------------===//
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
11
12#include "klee/ADT/BitArray.h"
13#include "klee/Config/Version.h"
22
23#include <llvm/ADT/APInt.h>
24#include <llvm/Support/CommandLine.h>
25
26#include <algorithm>
27#include <cassert>
28#include <cstddef>
29#include <set>
30
31using namespace klee;
32
33namespace klee {
34llvm::cl::opt<ArrayOptimizationType> OptimizeArray(
35 "optimize-array",
36 llvm::cl::values(clEnumValN(ALL, "all",
37 "Combining index and value transformations"),
38 clEnumValN(INDEX, "index", "Index-based transformation"),
39 clEnumValN(VALUE, "value",
40 "Value-based transformation at branch (both "
41 "concrete and concrete/symbolic)")),
42 llvm::cl::init(NONE),
43 llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic "
44 "arrays. (default=false)"),
45 llvm::cl::cat(klee::SolvingCat));
46
47llvm::cl::opt<double> ArrayValueRatio(
48 "array-value-ratio",
49 llvm::cl::desc("Maximum ratio of unique values to array size for which the "
50 "value-based transformations are applied."),
51 llvm::cl::init(1.0), llvm::cl::value_desc("Unique Values / Array Size"),
52 llvm::cl::cat(klee::SolvingCat));
53
54llvm::cl::opt<double> ArrayValueSymbRatio(
55 "array-value-symb-ratio",
56 llvm::cl::desc("Maximum ratio of symbolic values to array size for which "
57 "the mixed value-based transformations are applied."),
58 llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size"),
59 llvm::cl::cat(klee::SolvingCat));
60}; // namespace klee
61
63 Expr::Width w) {
64 switch (w) {
65 default:
66 assert(0 && "invalid width");
67 case Expr::Int8:
68 return ReadExpr::alloc(ul, index);
69 case Expr::Int16:
70 return ConcatExpr::create(
71 ReadExpr::alloc(
72 ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
73 ReadExpr::alloc(ul, index));
74 case Expr::Int32:
75 return ConcatExpr::create4(
76 ReadExpr::alloc(
77 ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)),
78 ReadExpr::alloc(
79 ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)),
80 ReadExpr::alloc(
81 ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
82 ReadExpr::alloc(ul, index));
83 case Expr::Int64:
84 return ConcatExpr::create8(
85 ReadExpr::alloc(
86 ul, AddExpr::create(ConstantExpr::create(7, Expr::Int32), index)),
87 ReadExpr::alloc(
88 ul, AddExpr::create(ConstantExpr::create(6, Expr::Int32), index)),
89 ReadExpr::alloc(
90 ul, AddExpr::create(ConstantExpr::create(5, Expr::Int32), index)),
91 ReadExpr::alloc(
92 ul, AddExpr::create(ConstantExpr::create(4, Expr::Int32), index)),
93 ReadExpr::alloc(
94 ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)),
95 ReadExpr::alloc(
96 ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)),
97 ReadExpr::alloc(
98 ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
99 ReadExpr::alloc(ul, index));
100 }
101}
102
103ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) {
104 // Nothing to optimise for constant expressions
105 if (isa<ConstantExpr>(e))
106 return e;
107
108 // If no is optimization enabled, return early avoid cache lookup
109 if (OptimizeArray == NONE)
110 return e;
111
112 if (cacheExprUnapplicable.count(e) > 0)
113 return e;
114
115 // Find cached expressions
116 auto cached = cacheExprOptimized.find(e);
117 if (cached != cacheExprOptimized.end())
118 return cached->second;
119
120 ref<Expr> result;
121 // ----------------------- INDEX-BASED OPTIMIZATION -------------------------
122 if (!valueOnly && (OptimizeArray == ALL || OptimizeArray == INDEX)) {
123 array2idx_ty arrays;
124 ConstantArrayExprVisitor aev(arrays);
125 aev.visit(e);
126
127 if (arrays.empty() || aev.isIncompatible()) {
128 // We do not optimize expressions other than those with concrete
129 // arrays with a symbolic index
130 // If we cannot optimize the expression, we return a failure only
131 // when we are not combining the optimizations
132 if (OptimizeArray == INDEX) {
133 cacheExprUnapplicable.insert(e);
134 return e;
135 }
136 } else {
137 mapIndexOptimizedExpr_ty idx_valIdx;
138
139 // Compute those indexes s.t. orig_expr =equisat= (k==i|k==j|..)
140 if (computeIndexes(arrays, e, idx_valIdx)) {
141 if (!idx_valIdx.empty()) {
142 // Create new expression on indexes
143 result = ExprRewriter::createOptExpr(e, arrays, idx_valIdx);
144 } else {
145 klee_warning("OPT_I: infeasible branch!");
146 result = ConstantExpr::create(0, Expr::Bool);
147 }
148 // Add new expression to cache
149 if (result) {
150 klee_warning("OPT_I: successful");
151 cacheExprOptimized[e] = result;
152 } else {
153 klee_warning("OPT_I: unsuccessful");
154 }
155 } else {
156 klee_warning("OPT_I: unsuccessful");
157 cacheExprUnapplicable.insert(e);
158 }
159 }
160 }
161 // ----------------------- VALUE-BASED OPTIMIZATION -------------------------
162 if (OptimizeArray == VALUE ||
163 (OptimizeArray == ALL && (!result || valueOnly))) {
164 std::vector<const ReadExpr *> reads;
165 std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width>> readInfo;
166 ArrayReadExprVisitor are(reads, readInfo);
167 are.visit(e);
168 std::reverse(reads.begin(), reads.end());
169
170 if (reads.empty() || are.isIncompatible()) {
171 cacheExprUnapplicable.insert(e);
172 return e;
173 }
174
175 ref<Expr> selectOpt =
176 getSelectOptExpr(e, reads, readInfo, are.containsSymbolic());
177 if (selectOpt) {
178 klee_warning("OPT_V: successful");
179 result = selectOpt;
180 cacheExprOptimized[e] = result;
181 } else {
182 klee_warning("OPT_V: unsuccessful");
183 cacheExprUnapplicable.insert(e);
184 }
185 }
186 if (!result)
187 return e;
188 return result;
189}
190
192 mapIndexOptimizedExpr_ty &idx_valIdx) const {
193 bool success = false;
194 // For each constant array found
195 for (auto &element : arrays) {
196 const Array *arr = element.first;
197
198 assert(arr->isConstantArray() && "Array is not concrete");
199 assert(element.second.size() == 1 && "Multiple indexes on the same array");
200
202 idxt_v.visit(e);
203 assert((idxt_v.getWidth() % arr->range == 0) && "Read is not aligned");
204 Expr::Width width = idxt_v.getWidth() / arr->range;
205
206 if (auto e = idxt_v.getMul()) {
207 // If we have a MulExpr in the index, we can optimize our search by
208 // skipping all those indexes that are not multiple of such value.
209 // In fact, they will be rejected by the MulExpr interpreter since it
210 // will not find any integer solution
211 auto ce = dyn_cast<ConstantExpr>(e);
212 assert(ce && "Not a constant expression");
213 uint64_t mulVal = (*ce->getAPValue().getRawData());
214 // So far we try to limit this optimization, but we may try some more
215 // aggressive conditions (i.e. mulVal > width)
216 if (width == 1 && mulVal > 1)
217 width = mulVal;
218 }
219
220 // For each concrete value 'i' stored in the array
221 for (size_t aIdx = 0; aIdx < arr->constantValues.size(); aIdx += width) {
222 auto *a = new Assignment();
223 std::vector<const Array *> objects;
224 std::vector<std::vector<unsigned char>> values;
225
226 // For each symbolic index Expr(k) found
227 for (auto &index_it : element.second) {
228 ref<Expr> idx = index_it;
229 ref<Expr> val = ConstantExpr::alloc(aIdx, arr->getDomain());
230 // We create a partial assignment on 'k' s.t. Expr(k)==i
231 bool assignmentSuccess =
233 success |= assignmentSuccess;
234
235 // If the assignment satisfies both the expression 'e' and the PC
236 ref<Expr> evaluation = a->evaluate(e);
237 if (assignmentSuccess && evaluation->isTrue()) {
238 if (idx_valIdx.find(idx) == idx_valIdx.end()) {
239 idx_valIdx.insert(std::make_pair(idx, std::vector<ref<Expr>>()));
240 }
241 idx_valIdx[idx].emplace_back(
242 ConstantExpr::alloc(aIdx, arr->getDomain()));
243 }
244 }
245 delete a;
246 }
247 }
248 return success;
249}
250
252 const ref<Expr> &e, std::vector<const ReadExpr *> &reads,
253 std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width>> &readInfo,
254 bool isSymbolic) {
255 ref<Expr> notFound;
256 ref<Expr> toReturn;
257
258 // Array is concrete
259 if (!isSymbolic) {
260 ExprHashMap<ref<Expr>> optimized;
261 for (auto &read : reads) {
262 auto info = readInfo[read];
263 auto cached = cacheReadExprOptimized.find(const_cast<ReadExpr *>(read));
264 if (cached != cacheReadExprOptimized.end()) {
265 optimized.insert(std::make_pair(info.first, (*cached).second));
266 continue;
267 }
268 Expr::Width width = read->getWidth();
269 if (info.second > width) {
270 width = info.second;
271 }
272 unsigned size = read->updates.root->getSize();
273 unsigned bytesPerElement = width / 8;
274 unsigned elementsInArray = size / bytesPerElement;
275
276 // Note: we already filtered the ReadExpr, so here we can safely
277 // assume that the UpdateNodes contain ConstantExpr indexes and values
278 assert(read->updates.root->isConstantArray() &&
279 "Expected concrete array, found symbolic array");
280
281 // We need to read updates from lest recent to most recent, therefore
282 // reverse the list
283 std::vector<const UpdateNode *> us;
284 us.reserve(read->updates.getSize());
285 for (const UpdateNode *un = read->updates.head.get(); un;
286 un = un->next.get())
287 us.push_back(un);
288
289 auto arrayConstValues = read->updates.root->constantValues;
290 for (auto it = us.rbegin(); it != us.rend(); it++) {
291 const UpdateNode *un = *it;
292 auto ce = dyn_cast<ConstantExpr>(un->index);
293 assert(ce && "Not a constant expression");
294 uint64_t index = ce->getAPValue().getZExtValue();
295 assert(index < arrayConstValues.size());
296 auto arrayValue = dyn_cast<ConstantExpr>(un->value);
297 assert(arrayValue && "Not a constant expression");
298 arrayConstValues[index] = arrayValue;
299 }
300 std::vector<uint64_t> arrayValues;
301 // Get the concrete values from the array
302 for (unsigned i = 0; i < elementsInArray; i++) {
303 uint64_t val = 0;
304 for (unsigned j = 0; j < bytesPerElement; j++) {
305 val |= (*(
306 arrayConstValues[(i * bytesPerElement) + j]
307 .get()
308 ->getAPValue()
309 .getRawData())
310 << (j * 8));
311 }
312 arrayValues.push_back(val);
313 }
314
315 ref<Expr> index = UDivExpr::create(
316 read->index,
317 ConstantExpr::create(bytesPerElement, read->index->getWidth()));
318
319 ref<Expr> opt =
320 buildConstantSelectExpr(index, arrayValues, width, elementsInArray);
321 if (opt) {
322 cacheReadExprOptimized[const_cast<ReadExpr *>(read)] = opt;
323 optimized.insert(std::make_pair(info.first, opt));
324 }
325 }
326 ArrayValueOptReplaceVisitor replacer(optimized);
327 toReturn = replacer.visit(e);
328 }
329
330 // Array is mixed concrete/symbolic
331 // \pre: array is concrete && updatelist contains at least one symbolic value
332 // OR
333 // array is symbolic && updatelist contains at least one concrete value
334 else {
335 ExprHashMap<ref<Expr>> optimized;
336 for (auto &read : reads) {
337 auto info = readInfo[read];
338 auto cached = cacheReadExprOptimized.find(const_cast<ReadExpr *>(read));
339 if (cached != cacheReadExprOptimized.end()) {
340 optimized.insert(std::make_pair(info.first, (*cached).second));
341 continue;
342 }
343 Expr::Width width = read->getWidth();
344 if (info.second > width) {
345 width = info.second;
346 }
347 unsigned size = read->updates.root->getSize();
348 unsigned bytesPerElement = width / 8;
349 unsigned elementsInArray = size / bytesPerElement;
350 bool symbArray = read->updates.root->isSymbolicArray();
351
352 BitArray ba(size, symbArray);
353 // Note: we already filtered the ReadExpr, so here we can safely
354 // assume that the UpdateNodes contain ConstantExpr indexes, but in
355 // this case we *cannot* assume anything on the values
356 auto arrayConstValues = read->updates.root->constantValues;
357 if (arrayConstValues.size() < size) {
358 // We need to "force" initialization of the values
359 for (size_t i = arrayConstValues.size(); i < size; i++) {
360 arrayConstValues.push_back(ConstantExpr::create(0, Expr::Int8));
361 }
362 }
363
364 // We need to read updates from lest recent to most recent, therefore
365 // reverse the list
366 std::vector<const UpdateNode *> us;
367 us.reserve(read->updates.getSize());
368 for (const UpdateNode *un = read->updates.head.get(); un; un = un->next.get())
369 us.push_back(un);
370
371 for (auto it = us.rbegin(); it != us.rend(); it++) {
372 const UpdateNode *un = *it;
373 auto ce = dyn_cast<ConstantExpr>(un->index);
374 assert(ce && "Not a constant expression");
375 uint64_t index = ce->getAPValue().getLimitedValue();
376 if (!isa<ConstantExpr>(un->value)) {
377 ba.set(index);
378 } else {
379 ba.unset(index);
380 auto arrayValue =
381 dyn_cast<ConstantExpr>(un->value);
382 assert(arrayValue && "Not a constant expression");
383 arrayConstValues[index] = arrayValue;
384 }
385 }
386
387 std::vector<std::pair<uint64_t, bool>> arrayValues;
388 unsigned symByteNum = 0;
389 for (unsigned i = 0; i < elementsInArray; i++) {
390 uint64_t val = 0;
391 bool elementIsConcrete = true;
392 for (unsigned j = 0; j < bytesPerElement; j++) {
393 if (ba.get((i * bytesPerElement) + j)) {
394 elementIsConcrete = false;
395 break;
396 } else {
397 val |= (*(
398 arrayConstValues[(i * bytesPerElement) + j]
399 .get()
400 ->getAPValue()
401 .getRawData())
402 << (j * 8));
403 }
404 }
405 if (elementIsConcrete) {
406 arrayValues.emplace_back(val, true);
407 } else {
408 symByteNum++;
409 arrayValues.emplace_back(0, false);
410 }
411 }
412
413 if (((double)symByteNum / (double)elementsInArray) <=
415 // If the optimization can be applied we apply it
416 // Build the dynamic select expression
417 ref<Expr> opt =
418 buildMixedSelectExpr(read, arrayValues, width, elementsInArray);
419 if (opt) {
420 cacheReadExprOptimized[const_cast<ReadExpr *>(read)] = opt;
421 optimized.insert(std::make_pair(info.first, opt));
422 }
423 }
424 }
425 ArrayValueOptReplaceVisitor replacer(optimized, false);
426 toReturn = replacer.visit(e);
427 }
428
429 return toReturn ? toReturn : notFound;
430}
431
433 const ref<Expr> &index, std::vector<uint64_t> &arrayValues,
434 Expr::Width width, unsigned arraySize) const {
435 std::vector<std::pair<uint64_t, uint64_t>> ranges;
436 std::vector<uint64_t> values;
437 std::set<uint64_t> unique_array_values;
439 Expr::Width valWidth = width;
440 ref<Expr> result;
441
442 ref<Expr> actualIndex;
443 if (index->getWidth() > Expr::Int32) {
444 actualIndex = ExtractExpr::alloc(index, 0, Expr::Int32);
445 } else {
446 actualIndex = index;
447 }
448 Expr::Width idxWidth = actualIndex->getWidth();
449
450 // Calculate the repeating values ranges in the constant array
451 unsigned curr_idx = 0;
452 uint64_t curr_val = arrayValues[0];
453 for (unsigned i = 0; i < arraySize; i++) {
454 uint64_t temp = arrayValues[i];
455 unique_array_values.insert(curr_val);
456 if (temp != curr_val) {
457 ranges.emplace_back(curr_idx, i);
458 values.push_back(curr_val);
459 curr_val = temp;
460 curr_idx = i;
461 if (i == (arraySize - 1)) {
462 ranges.emplace_back(curr_idx, i + 1);
463 values.push_back(curr_val);
464 }
465 } else if (i == (arraySize - 1)) {
466 ranges.emplace_back(curr_idx, i + 1);
467 values.push_back(curr_val);
468 }
469 }
470
471 if (((double)unique_array_values.size() / (double)(arraySize)) >=
473 return result;
474 }
475
476 std::map<uint64_t, std::vector<std::pair<uint64_t, uint64_t>>> exprMap;
477 for (size_t i = 0; i < ranges.size(); i++) {
478 if (exprMap.find(values[i]) != exprMap.end()) {
479 exprMap[values[i]].emplace_back(ranges[i].first, ranges[i].second);
480 } else {
481 if (exprMap.find(values[i]) == exprMap.end()) {
482 exprMap.insert(std::make_pair(
483 values[i], std::vector<std::pair<uint64_t, uint64_t>>()));
484 }
485 exprMap.find(values[i])->second.emplace_back(ranges[i].first,
486 ranges[i].second);
487 }
488 }
489
490 int ct = 0;
491 // For each range appropriately build the Select expression.
492 for (auto range : exprMap) {
493 ref<Expr> temp;
494 if (ct == 0) {
495 temp = builder->Constant(llvm::APInt(valWidth, range.first, false));
496 } else {
497 if (range.second.size() == 1) {
498 if (range.second[0].first == (range.second[0].second - 1)) {
499 temp = SelectExpr::create(
500 EqExpr::create(actualIndex,
501 builder->Constant(llvm::APInt(
502 idxWidth, range.second[0].first, false))),
503 builder->Constant(llvm::APInt(valWidth, range.first, false)),
504 result);
505
506 } else {
507 temp = SelectExpr::create(
508 AndExpr::create(
509 SgeExpr::create(actualIndex,
510 builder->Constant(llvm::APInt(
511 idxWidth, range.second[0].first, false))),
512 SltExpr::create(
513 actualIndex,
514 builder->Constant(llvm::APInt(
515 idxWidth, range.second[0].second, false)))),
516 builder->Constant(llvm::APInt(valWidth, range.first, false)),
517 result);
518 }
519
520 } else {
521 ref<Expr> currOr;
522 if (range.second[0].first == (range.second[0].second - 1)) {
523 currOr = EqExpr::create(actualIndex,
524 builder->Constant(llvm::APInt(
525 idxWidth, range.second[0].first, false)));
526 } else {
527 currOr = AndExpr::create(
528 SgeExpr::create(actualIndex,
529 builder->Constant(llvm::APInt(
530 idxWidth, range.second[0].first, false))),
531 SltExpr::create(actualIndex,
532 builder->Constant(llvm::APInt(
533 idxWidth, range.second[0].second, false))));
534 }
535 for (size_t i = 1; i < range.second.size(); i++) {
536 ref<Expr> tempOr;
537 if (range.second[i].first == (range.second[i].second - 1)) {
538 tempOr = OrExpr::create(
539 EqExpr::create(actualIndex,
540 builder->Constant(llvm::APInt(
541 idxWidth, range.second[i].first, false))),
542 currOr);
543
544 } else {
545 tempOr = OrExpr::create(
546 AndExpr::create(
547 SgeExpr::create(
548 actualIndex,
549 builder->Constant(llvm::APInt(
550 idxWidth, range.second[i].first, false))),
551 SltExpr::create(
552 actualIndex,
553 builder->Constant(llvm::APInt(
554 idxWidth, range.second[i].second, false)))),
555 currOr);
556 }
557 currOr = tempOr;
558 }
559 temp = SelectExpr::create(currOr, builder->Constant(llvm::APInt(
560 valWidth, range.first, false)),
561 result);
562 }
563 }
564 result = temp;
565 ct++;
566 }
567
568 delete (builder);
569
570 return result;
571}
572
574 const ReadExpr *re, std::vector<std::pair<uint64_t, bool>> &arrayValues,
575 Expr::Width width, unsigned elementsInArray) const {
577 std::vector<uint64_t> values;
578 std::vector<std::pair<uint64_t, uint64_t>> ranges;
579 std::vector<uint64_t> holes;
580 std::set<uint64_t> unique_array_values;
581
582 unsigned arraySize = elementsInArray;
583 unsigned curr_idx = 0;
584 uint64_t curr_val = arrayValues[0].first;
585
586 bool emptyRange = true;
587 // Calculate Range values
588 for (size_t i = 0; i < arrayValues.size(); i++) {
589 // If the value is concrete
590 if (arrayValues[i].second) {
591 // The range contains a concrete value
592 emptyRange = false;
593 uint64_t temp = arrayValues[i].first;
594 unique_array_values.insert(temp);
595 if (temp != curr_val) {
596 ranges.emplace_back(curr_idx, i);
597 values.push_back(curr_val);
598 curr_val = temp;
599 curr_idx = i;
600 if (i == (arraySize - 1)) {
601 ranges.emplace_back(curr_idx, curr_idx + 1);
602 values.push_back(curr_val);
603 }
604 } else if (i == (arraySize - 1)) {
605 ranges.emplace_back(curr_idx, i + 1);
606 values.push_back(curr_val);
607 }
608 } else {
609 holes.push_back(i);
610 // If this is not an empty range
611 if (!emptyRange) {
612 ranges.emplace_back(curr_idx, i);
613 values.push_back(curr_val);
614 }
615 curr_val = arrayValues[i + 1].first;
616 curr_idx = i + 1;
617 emptyRange = true;
618 }
619 }
620
621 assert(!unique_array_values.empty() && "No unique values");
622 assert(!ranges.empty() && "No ranges");
623
624 ref<Expr> result;
625 if (((double)unique_array_values.size() / (double)(arraySize)) <=
627 // The final "else" expression will be the original unoptimized array read
628 // expression
629 unsigned range_start = 0;
630 if (holes.empty()) {
631 result = builder->Constant(llvm::APInt(width, values[0], false));
632 range_start = 1;
633 } else {
634 ref<Expr> firstIndex = MulExpr::create(
635 ConstantExpr::create(holes[0], re->index->getWidth()),
636 ConstantExpr::create(width / 8, re->index->getWidth()));
637 result = extendRead(re->updates, firstIndex, width);
638 for (size_t i = 1; i < holes.size(); i++) {
639 ref<Expr> temp_idx = MulExpr::create(
640 ConstantExpr::create(holes[i], re->index->getWidth()),
641 ConstantExpr::create(width / 8, re->index->getWidth()));
642 ref<Expr> cond = EqExpr::create(re->index, temp_idx);
644 cond, extendRead(re->updates, temp_idx, width), result);
645 result = temp;
646 }
647 }
648
649 ref<Expr> new_index = UDivExpr::create(
650 re->index, ConstantExpr::create(width / 8, re->index->getWidth()));
651
652 int new_index_width = new_index->getWidth();
653 // Iterate through all the ranges
654 for (size_t i = range_start; i < ranges.size(); i++) {
655 ref<Expr> temp;
656 if (ranges[i].second - 1 == ranges[i].first) {
657 ref<Expr> cond = EqExpr::create(
658 new_index, ConstantExpr::create(ranges[i].first, new_index_width));
659 ref<Expr> t = ConstantExpr::create(values[i], width);
660 ref<Expr> f = result;
661 temp = SelectExpr::create(cond, t, f);
662 } else {
663 // Create the select constraint
664 ref<Expr> cond = AndExpr::create(
665 SgeExpr::create(new_index, ConstantExpr::create(ranges[i].first,
666 new_index_width)),
667 SltExpr::create(new_index, ConstantExpr::create(ranges[i].second,
668 new_index_width)));
669 ref<Expr> t = ConstantExpr::create(values[i], width);
670 ref<Expr> f = result;
671 temp = SelectExpr::create(cond, t, f);
672 }
673 result = temp;
674 }
675 }
676
677 delete (builder);
678
679 return result;
680}
ref< Expr > extendRead(const UpdateList &ul, const ref< Expr > index, Expr::Width w)
bool isConstantArray() const
Definition: Expr.h:525
const std::vector< ref< ConstantExpr > > constantValues
Definition: Expr.h:498
Expr::Width getDomain() const
Definition: Expr.h:529
const Expr::Width range
Definition: Expr.h:493
static bool generatePartialAssignment(const ref< Expr > &e, ref< Expr > &val, Assignment *&a)
bool get(unsigned idx)
Definition: BitArray.h:34
void unset(unsigned idx)
Definition: BitArray.h:36
void set(unsigned idx)
Definition: BitArray.h:35
static ref< ConstantExpr > create(uint64_t v, Width w)
Definition: Expr.h:1079
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:1065
ExprBuilder - Base expression builder class.
Definition: ExprBuilder.h:17
virtual ref< Expr > Constant(const llvm::APInt &Value)=0
ref< Expr > getSelectOptExpr(const ref< Expr > &e, std::vector< const ReadExpr * > &reads, std::map< const ReadExpr *, std::pair< ref< Expr >, Expr::Width > > &readInfo, bool isSymbolic)
ExprHashSet cacheExprUnapplicable
ExprHashMap< ref< Expr > > cacheExprOptimized
ref< Expr > buildMixedSelectExpr(const ReadExpr *re, std::vector< std::pair< uint64_t, bool > > &arrayValues, Expr::Width width, unsigned elementsInArray) const
bool computeIndexes(array2idx_ty &arrays, const ref< Expr > &e, mapIndexOptimizedExpr_ty &idx_valIdx) const
ref< Expr > buildConstantSelectExpr(const ref< Expr > &index, std::vector< uint64_t > &arrayValues, Expr::Width width, unsigned elementsInArray) const
ExprHashMap< ref< Expr > > cacheReadExprOptimized
static ref< Expr > createOptExpr(const ref< Expr > &e, const array2idx_ty &arrays, const mapIndexOptimizedExpr_ty &idx_valIdx)
ref< Expr > visit(const ref< Expr > &e)
Definition: ExprVisitor.cpp:26
static const Width Int32
Definition: Expr.h:103
virtual Width getWidth() const =0
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:97
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:1156
static const Width Bool
Definition: Expr.h:100
static const Width Int8
Definition: Expr.h:101
static ref< Expr > alloc(const ref< Expr > &e, unsigned o, Width w)
Definition: Expr.h:750
Class representing a one byte read from an array.
Definition: Expr.h:565
ref< Expr > index
Definition: Expr.h:572
UpdateList updates
Definition: Expr.h:571
static ref< Expr > create(ref< Expr > c, ref< Expr > t, ref< Expr > f)
Definition: Expr.cpp:592
Class representing a complete list of updates into an array.
Definition: Expr.h:539
Class representing a byte update of an array.
Definition: Expr.h:451
ref< Expr > index
Definition: Expr.h:459
const ref< UpdateNode > next
Definition: Expr.h:458
ref< Expr > value
Definition: Expr.h:459
Definition: main.cpp:291
ExprBuilder * createDefaultExprBuilder()
llvm::cl::opt< double > ArrayValueSymbRatio("array-value-symb-ratio", llvm::cl::desc("Maximum ratio of symbolic values to array size for which " "the mixed value-based transformations are applied."), llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size"), llvm::cl::cat(klee::SolvingCat))
std::map< ref< Expr >, std::vector< ref< Expr > > > mapIndexOptimizedExpr_ty
llvm::cl::opt< ArrayOptimizationType > OptimizeArray("optimize-array", llvm::cl::values(clEnumValN(ALL, "all", "Combining index and value transformations"), clEnumValN(INDEX, "index", "Index-based transformation"), clEnumValN(VALUE, "value", "Value-based transformation at branch (both " "concrete and concrete/symbolic)")), llvm::cl::init(NONE), llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic " "arrays. (default=false)"), llvm::cl::cat(klee::SolvingCat))
std::map< const Array *, std::vector< ref< Expr > > > array2idx_ty
llvm::cl::opt< double > ArrayValueRatio("array-value-ratio", llvm::cl::desc("Maximum ratio of unique values to array size for which the " "value-based transformations are applied."), llvm::cl::init(1.0), llvm::cl::value_desc("Unique Values / Array Size"), llvm::cl::cat(klee::SolvingCat))
llvm::cl::OptionCategory SolvingCat
void void void klee_warning(const char *msg,...) __attribute__((format(printf