about summary refs log tree commit diff homepage
path: root/lib/Expr
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Expr')
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp42
-rw-r--r--lib/Expr/ArrayExprRewriter.cpp209
-rw-r--r--lib/Expr/ArrayExprVisitor.cpp10
-rw-r--r--lib/Expr/AssignmentGenerator.cpp12
4 files changed, 161 insertions, 112 deletions
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 86c19a81..b3e8bca0 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -1,3 +1,12 @@
+//===-- ArrayExprOptimizer.cpp --------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
 #include "klee/ArrayExprOptimizer.h"
 
 #include "klee/ArrayExprRewriter.h"
@@ -91,7 +100,7 @@ void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result,
   if (OptimizeArray == VALUE ||
       (OptimizeArray == ALL && (!result.get() || valueOnly))) {
     std::vector<const ReadExpr *> reads;
-    std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > readInfo;
+    std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> readInfo;
     ArrayReadExprVisitor are(reads, readInfo);
     are.visit(e);
     std::reverse(reads.begin(), reads.end());
@@ -147,7 +156,7 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
     for (size_t aIdx = 0; aIdx < arr->constantValues.size(); aIdx += width) {
       Assignment *a = new Assignment();
       v_arr_ty objects;
-      std::vector<std::vector<unsigned char> > values;
+      std::vector<std::vector<unsigned char>> values;
 
       // For each symbolic index Expr(k) found
       for (auto &index_it : element.second) {
@@ -162,7 +171,7 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
         ref<Expr> evaluation = a->evaluate(e);
         if (assignmentSuccess && evaluation->isTrue()) {
           if (idx_valIdx.find(idx) == idx_valIdx.end()) {
-            idx_valIdx.insert(std::make_pair(idx, std::vector<ref<Expr> >()));
+            idx_valIdx.insert(std::make_pair(idx, std::vector<ref<Expr>>()));
           }
           idx_valIdx[idx]
               .push_back(ConstantExpr::alloc(aIdx, arr->getDomain()));
@@ -176,14 +185,14 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
 
 ref<Expr> ExprOptimizer::getSelectOptExpr(
     const ref<Expr> &e, std::vector<const ReadExpr *> &reads,
-    std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &readInfo,
+    std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &readInfo,
     bool isSymbolic) {
   ref<Expr> notFound;
   ref<Expr> toReturn;
 
   // Array is concrete
   if (!isSymbolic) {
-    std::map<unsigned, ref<Expr> > optimized;
+    std::map<unsigned, ref<Expr>> optimized;
     for (auto &read : reads) {
       auto info = readInfo[read];
       auto cached = cacheReadExprOptimized.find(read->hash());
@@ -249,7 +258,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
   // OR
   //       array is symbolic && updatelist contains at least one concrete value
   else {
-    std::map<unsigned, ref<Expr> > optimized;
+    std::map<unsigned, ref<Expr>> optimized;
     for (auto &read : reads) {
       auto info = readInfo[read];
       auto cached = cacheReadExprOptimized.find(read->hash());
@@ -290,7 +299,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
         }
       }
 
-      std::vector<std::pair<uint64_t, bool> > arrayValues;
+      std::vector<std::pair<uint64_t, bool>> arrayValues;
       unsigned symByteNum = 0;
       for (unsigned i = 0; i < elementsInArray; i++) {
         uint64_t val = 0;
@@ -316,7 +325,8 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
         }
       }
 
-      if (((double)symByteNum / (double)elementsInArray) <= ArrayValueSymbRatio) {
+      if (((double)symByteNum / (double)elementsInArray) <=
+          ArrayValueSymbRatio) {
         // If the optimization can be applied we apply it
         // Build the dynamic select expression
         ref<Expr> opt =
@@ -337,7 +347,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
 ref<Expr> ExprOptimizer::buildConstantSelectExpr(
     const ref<Expr> &index, std::vector<uint64_t> &arrayValues,
     Expr::Width width, unsigned arraySize) const {
-  std::vector<std::pair<uint64_t, uint64_t> > ranges;
+  std::vector<std::pair<uint64_t, uint64_t>> ranges;
   std::vector<uint64_t> values;
   std::set<uint64_t> unique_array_values;
   ExprBuilder *builder = createDefaultExprBuilder();
@@ -373,11 +383,12 @@ ref<Expr> ExprOptimizer::buildConstantSelectExpr(
     }
   }
 
-  if (((double)unique_array_values.size() / (double)(arraySize)) >= ArrayValueRatio) {
+  if (((double)unique_array_values.size() / (double)(arraySize)) >=
+      ArrayValueRatio) {
     return result;
   }
 
-  std::map<uint64_t, std::vector<std::pair<uint64_t, uint64_t> > > exprMap;
+  std::map<uint64_t, std::vector<std::pair<uint64_t, uint64_t>>> exprMap;
   for (size_t i = 0; i < ranges.size(); i++) {
     if (exprMap.find(values[i]) != exprMap.end()) {
       exprMap[values[i]]
@@ -385,7 +396,7 @@ ref<Expr> ExprOptimizer::buildConstantSelectExpr(
     } else {
       if (exprMap.find(values[i]) == exprMap.end()) {
         exprMap.insert(std::make_pair(
-            values[i], std::vector<std::pair<uint64_t, uint64_t> >()));
+            values[i], std::vector<std::pair<uint64_t, uint64_t>>()));
       }
       exprMap.find(values[i])
           ->second.push_back(std::make_pair(ranges[i].first, ranges[i].second));
@@ -476,11 +487,11 @@ ref<Expr> ExprOptimizer::buildConstantSelectExpr(
 }
 
 ref<Expr> ExprOptimizer::buildMixedSelectExpr(
-    const ReadExpr *re, std::vector<std::pair<uint64_t, bool> > &arrayValues,
+    const ReadExpr *re, std::vector<std::pair<uint64_t, bool>> &arrayValues,
     Expr::Width width, unsigned elementsInArray) const {
   ExprBuilder *builder = createDefaultExprBuilder();
   std::vector<uint64_t> values;
-  std::vector<std::pair<uint64_t, uint64_t> > ranges;
+  std::vector<std::pair<uint64_t, uint64_t>> ranges;
   std::vector<uint64_t> holes;
   std::set<uint64_t> unique_array_values;
 
@@ -527,7 +538,8 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr(
   assert(ranges.size() > 0 && "No ranges");
 
   ref<Expr> result;
-  if (((double)unique_array_values.size() / (double)(arraySize)) <= ArrayValueRatio) {
+  if (((double)unique_array_values.size() / (double)(arraySize)) <=
+      ArrayValueRatio) {
     // The final "else" expression will be the original unoptimized array read
     // expression
     unsigned range_start = 0;
diff --git a/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp
index d4dc9a21..5e5dac0d 100644
--- a/lib/Expr/ArrayExprRewriter.cpp
+++ b/lib/Expr/ArrayExprRewriter.cpp
@@ -1,3 +1,12 @@
+//===-- ArrayExprRewriter.cpp ---------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
 #include "klee/ArrayExprRewriter.h"
 
 #include "klee/util/BitArray.h"
@@ -6,119 +15,127 @@
 
 using namespace klee;
 
-ref<Expr> ExprRewriter::createOptExpr(const ref<Expr> &e,
-		const array2idx_ty &arrays,
-		const mapIndexOptimizedExpr_ty &idx_valIdx) {
-    return rewrite(e, arrays, idx_valIdx);
+ref<Expr>
+ExprRewriter::createOptExpr(const ref<Expr> &e, const array2idx_ty &arrays,
+                            const mapIndexOptimizedExpr_ty &idx_valIdx) {
+  return rewrite(e, arrays, idx_valIdx);
 }
 
-ref<Expr>
-ExprRewriter::rewrite(const ref<Expr> &e,
-                                   const array2idx_ty &arrays,
-                                   const mapIndexOptimizedExpr_ty &idx_valIdx) {
+ref<Expr> ExprRewriter::rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
+                                const mapIndexOptimizedExpr_ty &idx_valIdx) {
   ref<Expr> notFound;
-  std::vector<ref<Expr> > eqExprs;
+  std::vector<ref<Expr>> eqExprs;
   bool invert = false;
   for (auto &element : arrays) {
-	const Array* arr = element.first;
-	std::vector<ref<Expr> > indexes = element.second;
+    const Array *arr = element.first;
+    std::vector<ref<Expr>> indexes = element.second;
 
-	IndexTransformationExprVisitor idxt_v(arr);
-	idxt_v.visit(e);
+    IndexTransformationExprVisitor idxt_v(arr);
+    idxt_v.visit(e);
 
-	assert((idxt_v.getWidth() % element.first->range == 0) && "Read is not aligned");
+    assert((idxt_v.getWidth() % element.first->range == 0) &&
+           "Read is not aligned");
 
-	Expr::Width width = idxt_v.getWidth() / element.first->range;
-	if (idxt_v.getMul().get()) {
-	  // If we have a MulExpr in the index, we can optimize our search by
-	  // skipping all those indexes that are not multiple of such value.
-	  // In fact, they will be rejected by the MulExpr interpreter since it
-	  // will not find any integer solution
-	  Expr &e = *idxt_v.getMul();
-	  ConstantExpr &ce = static_cast<ConstantExpr &>(e);
-	  llvm::APInt val = ce.getAPValue();
-	  uint64_t mulVal = val.getZExtValue();
-	  // So far we try to limit this optimization, but we may try some more
-	  // aggressive conditions (i.e. mulVal > width)
-	  if (width == 1 && mulVal > 1)
-		width = mulVal;
-	}
+    Expr::Width width = idxt_v.getWidth() / element.first->range;
+    if (idxt_v.getMul().get()) {
+      // If we have a MulExpr in the index, we can optimize our search by
+      // skipping all those indexes that are not multiple of such value.
+      // In fact, they will be rejected by the MulExpr interpreter since it
+      // will not find any integer solution
+      Expr &e = *idxt_v.getMul();
+      ConstantExpr &ce = static_cast<ConstantExpr &>(e);
+      llvm::APInt val = ce.getAPValue();
+      uint64_t mulVal = val.getZExtValue();
+      // So far we try to limit this optimization, but we may try some more
+      // aggressive conditions (i.e. mulVal > width)
+      if (width == 1 && mulVal > 1)
+        width = mulVal;
+    }
 
-	for (std::vector<ref<Expr> >::const_iterator index_it = indexes.begin();
-		 index_it != indexes.end(); ++index_it) {
-	  if (idx_valIdx.find((*index_it)) == idx_valIdx.end()) {
-		continue;
-	  }
-	  auto opt_indexes = idx_valIdx.at((*index_it));
-	  if (opt_indexes.size() == 0) {
-		// We continue with other solutions
-		continue;
-	  } else if (opt_indexes.size() == 1) {
-		// We treat this case as a special one, and we create an EqExpr (e.g. k==i)
-		eqExprs.push_back(createEqExpr((*index_it), opt_indexes[0]));
-	  } else {
-		Expr::Width idxWidth = (*index_it).get()->getWidth();
-		unsigned set = 0;
-		BitArray ba(arr->size/width);
-		for (auto &vals : opt_indexes) {
-		  ConstantExpr &ce = static_cast<ConstantExpr &>(*vals);
-		  llvm::APInt v = ce.getAPValue();
-		  ba.set(v.getZExtValue() / width);
-		  set++;
-		}
-		if (set > 0 && set < arr->size/width)
-		  invert = ((float)set / (float)(arr->size/width)) > 0.5 ? true : false;
-		int start = -1;
-		for (unsigned i = 0; i < arr->size/width; ++i) {
-		  if ((!invert && ba.get(i)) || (invert && !ba.get(i))) {
-			if (start < 0)
-			  start = i;
-		  } else {
-			if (start >= 0) {
-			  if (i - start == 1) {
-				eqExprs.push_back(createEqExpr((*index_it), ConstantExpr::create(start*width, idxWidth)));
-			  } else {
-				// create range expr
-				ref<Expr> s = ConstantExpr::create(start*width, idxWidth);
-				ref<Expr> e = ConstantExpr::create((i-1)*width, idxWidth);
-				eqExprs.push_back(createRangeExpr((*index_it), s, e));
-			  }
-			  start = -1;
-			}
-		  }
-		}
-		if (start >= 0) {
-		  if ((arr->size/width) - start == 1) {
-			eqExprs.push_back(createEqExpr((*index_it), ConstantExpr::create(start*width, idxWidth)));
-		  } else {
-			// create range expr
-			ref<Expr> s = ConstantExpr::create(start*width, idxWidth);
-			ref<Expr> e = ConstantExpr::create(((arr->size/width) - 1)*width, idxWidth);
-			eqExprs.push_back(createRangeExpr((*index_it), s, e));
-		  }
-		}
-	  }
-	}
+    for (std::vector<ref<Expr>>::const_iterator index_it = indexes.begin();
+         index_it != indexes.end(); ++index_it) {
+      if (idx_valIdx.find((*index_it)) == idx_valIdx.end()) {
+        continue;
+      }
+      auto opt_indexes = idx_valIdx.at((*index_it));
+      if (opt_indexes.size() == 0) {
+        // We continue with other solutions
+        continue;
+      } else if (opt_indexes.size() == 1) {
+        // We treat this case as a special one, and we create an EqExpr (e.g.
+        // k==i)
+        eqExprs.push_back(createEqExpr((*index_it), opt_indexes[0]));
+      } else {
+        Expr::Width idxWidth = (*index_it).get()->getWidth();
+        unsigned set = 0;
+        BitArray ba(arr->size / width);
+        for (auto &vals : opt_indexes) {
+          ConstantExpr &ce = static_cast<ConstantExpr &>(*vals);
+          llvm::APInt v = ce.getAPValue();
+          ba.set(v.getZExtValue() / width);
+          set++;
+        }
+        if (set > 0 && set < arr->size / width)
+          invert =
+              ((float)set / (float)(arr->size / width)) > 0.5 ? true : false;
+        int start = -1;
+        for (unsigned i = 0; i < arr->size / width; ++i) {
+          if ((!invert && ba.get(i)) || (invert && !ba.get(i))) {
+            if (start < 0)
+              start = i;
+          } else {
+            if (start >= 0) {
+              if (i - start == 1) {
+                eqExprs.push_back(createEqExpr(
+                    (*index_it),
+                    ConstantExpr::create(start * width, idxWidth)));
+              } else {
+                // create range expr
+                ref<Expr> s = ConstantExpr::create(start * width, idxWidth);
+                ref<Expr> e = ConstantExpr::create((i - 1) * width, idxWidth);
+                eqExprs.push_back(createRangeExpr((*index_it), s, e));
+              }
+              start = -1;
+            }
+          }
+        }
+        if (start >= 0) {
+          if ((arr->size / width) - start == 1) {
+            eqExprs.push_back(createEqExpr(
+                (*index_it), ConstantExpr::create(start * width, idxWidth)));
+          } else {
+            // create range expr
+            ref<Expr> s = ConstantExpr::create(start * width, idxWidth);
+            ref<Expr> e = ConstantExpr::create(
+                ((arr->size / width) - 1) * width, idxWidth);
+            eqExprs.push_back(createRangeExpr((*index_it), s, e));
+          }
+        }
+      }
+    }
   }
   if (eqExprs.size() == 0) {
-	return notFound;
+    return notFound;
   } else if (eqExprs.size() == 1) {
-	if (isa<AndExpr>(eqExprs[0])) {
-	  return EqExpr::alloc(ConstantExpr::alloc(invert ? 0 : 1, (eqExprs[0])->getWidth()),
-						   eqExprs[0]);
-	}
-	return invert ? NotExpr::alloc(eqExprs[0]) : eqExprs[0];
+    if (isa<AndExpr>(eqExprs[0])) {
+      return EqExpr::alloc(
+          ConstantExpr::alloc(invert ? 0 : 1, (eqExprs[0])->getWidth()),
+          eqExprs[0]);
+    }
+    return invert ? NotExpr::alloc(eqExprs[0]) : eqExprs[0];
   } else {
-	// We have found at least 2 indexes, we combine them using an OrExpr (e.g. k==i|k==j)
-	ref<Expr> orExpr = concatenateOrExpr(eqExprs.begin(), eqExprs.end());
-	// Create Eq expression for true branch
-	return EqExpr::alloc(ConstantExpr::alloc(invert ? 0 : 1, (orExpr)->getWidth()), orExpr);
+    // We have found at least 2 indexes, we combine them using an OrExpr (e.g.
+    // k==i|k==j)
+    ref<Expr> orExpr = concatenateOrExpr(eqExprs.begin(), eqExprs.end());
+    // Create Eq expression for true branch
+    return EqExpr::alloc(
+        ConstantExpr::alloc(invert ? 0 : 1, (orExpr)->getWidth()), orExpr);
   }
 }
 
 ref<Expr> ExprRewriter::concatenateOrExpr(
-    const std::vector<ref<Expr> >::const_iterator begin,
-    const std::vector<ref<Expr> >::const_iterator end) {
+    const std::vector<ref<Expr>>::const_iterator begin,
+    const std::vector<ref<Expr>>::const_iterator end) {
   if (begin + 2 == end) {
     return OrExpr::alloc(ZExtExpr::alloc((*begin), Expr::Int32),
                          ZExtExpr::alloc((*(begin + 1)), Expr::Int32));
diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp
index fa92b66c..dae4c451 100644
--- a/lib/Expr/ArrayExprVisitor.cpp
+++ b/lib/Expr/ArrayExprVisitor.cpp
@@ -1,3 +1,12 @@
+//===-- ArrayExprVisitor.cpp ----------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
 #include "klee/util/ArrayExprVisitor.h"
 
 #include "klee/Internal/Support/ErrorHandling.h"
@@ -258,6 +267,7 @@ ExprVisitor::Action IndexCleanerVisitor::visitMul(const MulExpr &e) {
   }
   return Action::doChildren();
 }
+
 ExprVisitor::Action IndexCleanerVisitor::visitRead(const ReadExpr &re) {
   mul = false;
   return Action::doChildren();
diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp
index 755263f0..4a1d68d8 100644
--- a/lib/Expr/AssignmentGenerator.cpp
+++ b/lib/Expr/AssignmentGenerator.cpp
@@ -1,3 +1,12 @@
+//===-- AssignmentGenerator.cpp -------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
 #include "klee/AssignmentGenerator.h"
 
 #include "llvm/Support/raw_ostream.h"
@@ -32,7 +41,8 @@ bool AssignmentGenerator::helperGenerateAssignment(const ref<Expr> &e,
     } else {
       return false;
     }
-    if (!ExtractExpr::create(kid_val, kid_val.get()->getWidth() - 1, 1).get()->isZero()) {
+    if (!ExtractExpr::create(kid_val, kid_val.get()->getWidth() - 1,
+                             1).get()->isZero()) {
       // FIXME: really bad hack to support those cases in which KLEE creates
       // Add expressions with negative values
       val = createAddExpr(kid_val, val);
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-12-14 17:38:53 +0000