diff options
author | Andrea Mattavelli <andreamattavelli@gmail.com> | 2017-02-06 12:10:05 +0000 |
---|---|---|
committer | Andrea Mattavelli <andreamattavelli@gmail.com> | 2017-02-14 13:10:13 +0000 |
commit | 44b24dac6a05ccde0e01b54fd2b787a31e5d8811 (patch) | |
tree | b776e909c66f2008e0c223f8aab911903ad3315a /unittests | |
parent | daf4eef5c3b99cdbc894f6bee40b4d047c5e6553 (diff) | |
download | klee-44b24dac6a05ccde0e01b54fd2b787a31e5d8811.tar.gz |
Added unit tests for ReadExpr::create() to check that constant folding is correctly applied
Diffstat (limited to 'unittests')
-rw-r--r-- | unittests/Expr/ExprTest.cpp | 151 |
1 files changed, 151 insertions, 0 deletions
diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp index 25129d8e..b1f593a5 100644 --- a/unittests/Expr/ExprTest.cpp +++ b/unittests/Expr/ExprTest.cpp @@ -113,4 +113,155 @@ TEST(ExprTest, ExtractConcat) { EXPECT_EQ(Expr::Extract, concat2->getKid(1)->getKind()); } +TEST(ExprTest, ReadExprFoldingBasic) { + unsigned size = 5; + + // Constant array + std::vector<ref<ConstantExpr> > Contents(size); + for (unsigned i = 0; i < size; ++i) + Contents[i] = ConstantExpr::create(i + 1, Expr::Int8); + ArrayCache ac; + const Array *array = + ac.CreateArray("arr", size, &Contents[0], &Contents[0] + size); + + // Basic constant folding rule + UpdateList ul(array, 0); + ref<Expr> read; + + for (unsigned i = 0; i < size; ++i) { + // Constant index (i) + read = ReadExpr::create(ul, ConstantExpr::create(i, Expr::Int32)); + EXPECT_EQ(Expr::Constant, read.get()->getKind()); + // Read - should be constant folded to Contents[i] + // Check that constant folding worked + ConstantExpr *c = static_cast<ConstantExpr *>(read.get()); + EXPECT_EQ(Contents[i]->getZExtValue(), c->getZExtValue()); + } +} + +TEST(ExprTest, ReadExprFoldingIndexOutOfBound) { + unsigned size = 5; + + // Constant array + std::vector<ref<ConstantExpr> > Contents(size); + for (unsigned i = 0; i < size; ++i) + Contents[i] = ConstantExpr::create(i + 1, Expr::Int8); + ArrayCache ac; + const Array *array = + ac.CreateArray("arr", size, &Contents[0], &Contents[0] + size); + + // Constant folding rule with index-out-of-bound + // Constant index (128) + ref<Expr> index = ConstantExpr::create(128, Expr::Int32); + UpdateList ul(array, 0); + ref<Expr> read = ReadExpr::create(ul, index); + // Read - should not be constant folded + // Check that constant folding was not applied + EXPECT_EQ(Expr::Read, read.get()->getKind()); +} + +TEST(ExprTest, ReadExprFoldingConstantUpdate) { + unsigned size = 5; + + // Constant array + std::vector<ref<ConstantExpr> > Contents(size); + for (unsigned i = 0; i < size; ++i) + Contents[i] = ConstantExpr::create(i + 1, Expr::Int8); + ArrayCache ac; + const Array *array = + ac.CreateArray("arr", size, &Contents[0], &Contents[0] + size); + + // Constant folding rule with constant update + // Constant index (0) + ref<Expr> index = ConstantExpr::create(0, Expr::Int32); + UpdateList ul(array, 0); + ref<Expr> updateValue = ConstantExpr::create(32, Expr::Int8); + ul.extend(index, updateValue); + ref<Expr> read = ReadExpr::create(ul, index); + // Read - should be constant folded to 32 + // Check that constant folding worked + EXPECT_EQ(Expr::Constant, read.get()->getKind()); + ConstantExpr *c = static_cast<ConstantExpr *>(read.get()); + EXPECT_EQ(32, c->getZExtValue()); +} + +TEST(ExprTest, ReadExprFoldingConstantMultipleUpdate) { + unsigned size = 5; + + // Constant array + std::vector<ref<ConstantExpr> > Contents(size); + for (unsigned i = 0; i < size; ++i) + Contents[i] = ConstantExpr::create(i + 1, Expr::Int8); + ArrayCache ac; + const Array *array = + ac.CreateArray("arr", size, &Contents[0], &Contents[0] + size); + + // Constant folding rule with constant update + // Constant index (0) + ref<Expr> index = ConstantExpr::create(0, Expr::Int32); + UpdateList ul(array, 0); + ref<Expr> updateValue = ConstantExpr::create(32, Expr::Int8); + ref<Expr> updateValue2 = ConstantExpr::create(64, Expr::Int8); + ul.extend(index, updateValue); + ul.extend(index, updateValue2); + ref<Expr> read = ReadExpr::create(ul, index); + // Read - should be constant folded to 64 + // Check that constant folding worked + EXPECT_EQ(Expr::Constant, read.get()->getKind()); + ConstantExpr *c = static_cast<ConstantExpr *>(read.get()); + EXPECT_EQ(64, c->getZExtValue()); +} + +TEST(ExprTest, ReadExprFoldingSymbolicValueUpdate) { + unsigned size = 5; + + // Constant array + std::vector<ref<ConstantExpr> > Contents(size); + for (unsigned i = 0; i < size; ++i) + Contents[i] = ConstantExpr::create(i + 1, Expr::Int8); + ArrayCache ac; + const Array *array = + ac.CreateArray("arr", size, &Contents[0], &Contents[0] + size); + + // Constant folding rule with symbolic update (value) + // Constant index (0) + ref<Expr> index = ConstantExpr::create(0, Expr::Int32); + UpdateList ul(array, 0); + const Array *array2 = ac.CreateArray("arr2", 256); + ref<Expr> updateValue = ReadExpr::createTempRead(array2, Expr::Int8); + ul.extend(index, updateValue); + ref<Expr> read = ReadExpr::create(ul, index); + // Read - should be constant folded to the symbolic value + // Check that constant folding worked + EXPECT_EQ(Expr::Read, read.get()->getKind()); + EXPECT_EQ(updateValue, read); +} + +TEST(ExprTest, ReadExprFoldingSymbolicIndexUpdate) { + unsigned size = 5; + + // Constant array + std::vector<ref<ConstantExpr> > Contents(size); + for (unsigned i = 0; i < size; ++i) + Contents[i] = ConstantExpr::create(i + 1, Expr::Int8); + ArrayCache ac; + const Array *array = + ac.CreateArray("arr", size, &Contents[0], &Contents[0] + size); + + // Constant folding rule with symbolic update (index) + UpdateList ul(array, 0); + const Array *array2 = ac.CreateArray("arr2", 256); + ref<Expr> updateIndex = ReadExpr::createTempRead(array2, Expr::Int32); + ref<Expr> updateValue = ConstantExpr::create(12, Expr::Int8); + ul.extend(updateIndex, updateValue); + ref<Expr> read; + + for (unsigned i = 0; i < size; ++i) { + // Constant index (i) + read = ReadExpr::create(ul, ConstantExpr::create(i, Expr::Int32)); + // Read - should not be constant folded + // Check that constant folding was not applied + EXPECT_EQ(Expr::Read, read.get()->getKind()); + } +} } |