[fix] tests

UnitTestBot · Oct 12, 2023 · 495cbf7 · 495cbf7
1 parent c4472cd
commit 495cbf7
Show file tree

Hide file tree

Showing 16 changed files with 468 additions and 442 deletions.
diff --git a/include/klee/Expr/ArrayCache.h b/include/klee/Expr/ArrayCache.h
@@ -64,6 +64,9 @@ class ArrayCache {
   typedef std::vector<const Array *> ArrayPtrVec;
   ArrayPtrVec concreteArrays;
 
+  // Number of arrays of each source allocated
+  std::unordered_map<SymbolicSource::Kind, unsigned> allocatedCount;
+
   unsigned getNextID() const;
 };
 } // namespace klee

diff --git a/lib/ADT/SparseStorage.cpp b/lib/ADT/SparseStorage.cpp
@@ -32,7 +32,7 @@ template <>
 void SparseStorage<unsigned char>::print(llvm::raw_ostream &os, Density d) const {
   if (d == Density::Sparse) {
     // "Sparse representation"
-    os << "[";
+    os << "{";
     bool firstPrinted = false;
     auto ordered = calculateOrderedStorage();
     for (const auto &element : ordered) {
@@ -42,7 +42,7 @@ void SparseStorage<unsigned char>::print(llvm::raw_ostream &os, Density d) const
       os << element.first << ": " << element.second;
       firstPrinted = true;
     }
-    os << "] DV: ";
+    os << "} DV: ";
     os << defaultValue;
   } else {
     // "Dense representation"
@@ -62,9 +62,9 @@ void SparseStorage<unsigned char>::print(llvm::raw_ostream &os, Density d) const
 
 template<>
 void SparseStorage<ref<ConstantExpr>>::print(llvm::raw_ostream &os, Density d) const {
-  os << "[";
   if (d == Density::Sparse) {
     // "Sparse representation"
+    os << "{";
     bool firstPrinted = false;
     auto ordered = calculateOrderedStorage();
     for (const auto &element : ordered) {
@@ -79,8 +79,10 @@ void SparseStorage<ref<ConstantExpr>>::print(llvm::raw_ostream &os, Density d) c
       }
       firstPrinted = true;
     }
+    os << "} DV: ";
   } else {
     // "Dense representation"
+    os << "[";
     bool firstPrinted = false;
     for (size_t i = 0; i < sizeOfSetRange(); i++) {
       if (firstPrinted) {
@@ -94,8 +96,8 @@ void SparseStorage<ref<ConstantExpr>>::print(llvm::raw_ostream &os, Density d) c
       }
       firstPrinted = true;
     }
+    os << "] DV: ";
   }
-  os << "] DV: ";
   if (defaultValue) {
     os << defaultValue;
   } else {

diff --git a/lib/Expr/ArrayCache.cpp b/lib/Expr/ArrayCache.cpp
@@ -22,12 +22,14 @@ const Array *ArrayCache::CreateArray(ref<Expr> _size,
                                      ref<SymbolicSource> _source,
                                      Expr::Width _domain, Expr::Width _range) {
 
-  const Array *array = new Array(_size, _source, _domain, _range, getNextID());
+  auto id = allocatedCount[_source->getKind()];
+  const Array *array = new Array(_size, _source, _domain, _range, id);
   if (array->isSymbolicArray()) {
     std::pair<ArrayHashSet::const_iterator, bool> success =
         cachedSymbolicArrays.insert(array);
     if (success.second) {
       // Cache miss
+      allocatedCount[_source->getKind()]++;
       return array;
     }
     // Cache hit
@@ -40,6 +42,7 @@ const Array *ArrayCache::CreateArray(ref<Expr> _size,
     // Treat every constant array as distinct so we never cache them
     assert(array->isConstantArray());
     concreteArrays.push_back(array); // For deletion later
+    allocatedCount[_source->getKind()]++;
     return array;
   }
 }

diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
@@ -386,9 +386,7 @@ class PPrinter : public ExprPPrinter {
     PC << "(";
     PC << source->getName() << " ";
     if (auto s = dyn_cast<ConstantSource>(source)) {
-      PC << " [";
       s->constantValues.print(PC.getStream(), Density::Sparse);
-      PC << "]";
     } else if (auto s = dyn_cast<SymbolicSizeConstantAddressSource>(source)) {
       PC << "UNIMPLEMENTED";
     } else if (auto s = dyn_cast<MakeSymbolicSource>(source)) {

diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
@@ -508,24 +508,44 @@ SourceResult ParserImpl::ParseSource() {
 SourceResult ParserImpl::ParseConstantSource() {
   std::unordered_map<size_t, ref<ConstantExpr>> storage;
   ref<ConstantExpr> defaultValue = nullptr;
-  ConsumeLSquare();
 
-  ConsumeLSquare();
-  while (Tok.kind != Token::RSquare) {
-    if (Tok.kind == Token::EndOfFile) {
-      Error("unexpected end of file.");
-      assert(0);
+  if (Tok.kind == Token::LSquare) {
+    ConsumeLSquare();
+    unsigned index = 0;
+    while (Tok.kind != Token::RSquare) {
+      if (Tok.kind == Token::EndOfFile) {
+        Error("unexpected end of file.");
+        assert(0);
+      }
+      ExprResult Res = ParseNumber(8).get(); // Should be Range Type
+      storage.insert({index, cast<ConstantExpr>(Res.get())});
+      if (Tok.kind == Token::Comma) {
+        ConsumeExpectedToken(Token::Comma);
+      }
+      index++;
     }
-    ExprResult Index = ParseNumber(64).get();
-    ConsumeExpectedToken(Token::Colon);
-    ExprResult Res = ParseNumber(8).get(); // Should be Range Type
-    storage.insert({cast<ConstantExpr>(Index.get())->getZExtValue(),
-                    cast<ConstantExpr>(Res.get())});
-    if (Tok.kind == Token::Comma) {
-      ConsumeExpectedToken(Token::Comma);
+    ConsumeRSquare();
+  } else if (Tok.kind == Token::LBrace) {
+    ConsumeExpectedToken(Token::LBrace);
+    while (Tok.kind != Token::RBrace) {
+      if (Tok.kind == Token::EndOfFile) {
+        Error("unexpected end of file.");
+        assert(0);
+      }
+      ExprResult Index = ParseNumber(64).get();
+      ConsumeExpectedToken(Token::Colon);
+      ExprResult Res = ParseNumber(8).get(); // Should be Range Type
+      storage.insert({cast<ConstantExpr>(Index.get())->getZExtValue(),
+                      cast<ConstantExpr>(Res.get())});
+      if (Tok.kind == Token::Comma) {
+        ConsumeExpectedToken(Token::Comma);
+      }
     }
+    ConsumeExpectedToken(Token::RBrace);
+  } else {
+    assert(0 && "Parsing error");
   }
-  ConsumeRSquare();
+
   ConsumeExpectedToken(Token::KWDV);
   ConsumeExpectedToken(Token::Colon);
 
@@ -536,8 +556,6 @@ SourceResult ParserImpl::ParseConstantSource() {
     ConsumeExpectedToken(Token::KWNull);
   }
 
-  ConsumeRSquare();
-
   SparseStorage<ref<ConstantExpr>> Values(storage, defaultValue);
   return SourceBuilder::constant(Values);
 }

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
@@ -426,6 +426,14 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n,
 ::VCExpr STPBuilder::getInitialArray(const Array *root) {
 
   assert(root);
+
+  if (ref<ConstantSource> constantSource =
+          dyn_cast<ConstantSource>(root->source)) {
+    if (!isa<ConstantExpr>(root->size)) {
+      assert(0 && "STP does not support symsize constant arrays");
+    }
+  }
+
   ::VCExpr array_expr;
   bool hashed = _arr_hash.lookupArrayExpr(root, array_expr);
 
@@ -435,12 +443,6 @@ ::VCExpr STPBuilder::getInitialArray(const Array *root) {
     std::string unique_id = llvm::utostr(_arr_hash._array_hash.size());
     std::string unique_name = root->getName() + unique_id;
 
-    if (isa<ConstantSource>(root->source)) {
-      llvm::report_fatal_error(
-          "STP does not support constant arrays or quantifiers to instantiate "
-          "constant array of symbolic size!");
-    }
-
     array_expr =
         buildArray(unique_name.c_str(), root->getDomain(), root->getRange());
 
@@ -451,14 +453,14 @@ ::VCExpr STPBuilder::getInitialArray(const Array *root) {
       // to work correctly in that case.
 
       // TODO: usage of `constantValues.size()` seems unconvinient.
-      // for (unsigned i = 0, e = constantSource->constantValues.size(); i != e;
-      //      ++i) {
-      //   ::VCExpr prev = array_expr;
-      //   array_expr = vc_writeExpr(
-      //       vc, prev, construct(ConstantExpr::alloc(i, root->getDomain()), 0),
-      //       construct(constantSource->constantValues[i], 0));
-      //   vc_DeleteExpr(prev);
-      // }
+      for (const auto &[index, value] : constantSource->constantValues.storage()) {
+        ::VCExpr prev = array_expr;
+        array_expr = vc_writeExpr(
+            vc, prev,
+            construct(ConstantExpr::alloc(index, root->getDomain()), 0),
+            construct(value, 0));
+        vc_DeleteExpr(prev);
+      }
     }
 
     _arr_hash.hashArrayExpr(root, array_expr);

diff --git a/test/Expr/Evaluate.kquery b/test/Expr/Evaluate.kquery
@@ -17,7 +17,7 @@ arr12 : (array (w64 8) (makeSymbolic arr1 0))
 
 # RUN: grep "Query 2:	VALID" %t.log
 # Query 2
-constant0 : (array (w64 4) (constant [[0: 1, 1: 2, 2: 3, 3: 5] DV: 0]))
+constant0 : (array (w64 4) (constant {0: 1, 1: 2, 2: 3, 3: 5} DV: 0))
 (query [] (Eq (Add w8 (Read w8 0 constant0)
                       (Read w8 3 constant0))
               6))

diff --git a/test/Expr/print-smt-let.kquery b/test/Expr/print-smt-let.kquery
@@ -1069,7 +1069,7 @@ makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0))
        [makeSymbolic0])
 
 # Query 72 -- Type: InitialValues, Instructions: 30
-constant2 : (array (w64 4) (constant [[0: 121, 1: 101, 2: 115, 3: 0] DV: 0]))
+constant2 : (array (w64 4) (constant {0: 121, 1: 101, 2: 115, 3: 0} DV: 0))
 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0))
 makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0))
 (query [(Eq false
@@ -1105,7 +1105,7 @@ makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0))
 # Query 74 -- Type: InitialValues, Instructions: 37
 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0))
 makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0))
-constant2 : (array (w64 4) (constant [[0: 171, 1: 171, 2: 171, 3: 171] DV: 0]))
+constant2 : (array (w64 4) (constant {0: 171, 1: 171, 2: 171, 3: 171} DV: 0))
 (query [(Eq false
             (Ult N0:(Mul w64 4
                              (SExt w64 (ReadLSB w32 0 makeSymbolic0)))
@@ -1128,7 +1128,7 @@ constant2 : (array (w64 4) (constant [[0: 171, 1: 171, 2: 171, 3: 171] DV: 0]))
 # Query 75 -- Type: InitialValues, Instructions: 40
 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0))
 makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0))
-constant2 : (array (w64 16) (constant [[0: 12, 4: 13, 8: 14, 12: 15] DV: 0]))
+constant2 : (array (w64 16) (constant {0: 12, 4: 13, 8: 14, 12: 15} DV: 0))
 (query [(Ult N0:(Mul w64 4
                          (SExt w64 (ReadLSB w32 0 makeSymbolic0)))
              13)]
@@ -1141,7 +1141,7 @@ constant2 : (array (w64 16) (constant [[0: 12, 4: 13, 8: 14, 12: 15] DV: 0]))
 # Query 76 -- Type: InitialValues, Instructions: 50
 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0))
 makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0))
-constant2 : (array (w64 4) (constant [[0: 171, 1: 171, 2: 171, 3: 171] DV: 0]))
+constant2 : (array (w64 4) (constant {0: 171, 1: 171, 2: 171, 3: 171} DV: 0))
 (query [(Eq false
             (Ult N0:(Mul w64 4
                              (SExt w64 (ReadLSB w32 0 makeSymbolic0)))
@@ -1160,7 +1160,7 @@ constant2 : (array (w64 4) (constant [[0: 171, 1: 171, 2: 171, 3: 171] DV: 0]))
 # Query 77 -- Type: InitialValues, Instructions: 51
 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0))
 makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0))
-constant2 : (array (w64 16) (constant [[0: 12, 4: 13, 8: 14, 12: 15] DV: 0]))
+constant2 : (array (w64 16) (constant {0: 12, 4: 13, 8: 14, 12: 15} DV: 0))
 (query [(Eq false
             (Ult N0:(Mul w64 4
                              (SExt w64 (ReadLSB w32 0 makeSymbolic0)))