From 58d1592fa3fd84aded956801183949b9c710490e Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Tue, 9 Jun 2009 08:42:08 +0000 Subject: More constant Array support. - The are parsed, printed, and solved now. - Remove some members of ArrayDecl which are only duplicates of Array members. - KLEE still doesn't create these, but you can write them by hand. The EXE style constant array optimization for STP (turning the initial writes into asserts) is now only a stones throw away, but I need to leave something fun to do tomorrow. :) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73133 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Solver/STPBuilder.cpp | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) (limited to 'lib/Solver/STPBuilder.cpp') diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 6d0a1b62..ab65f254 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -385,8 +385,6 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width } ::VCExpr STPBuilder::getInitialArray(const Array *root) { - assert(root->isSymbolicArray() && "FIXME: Support constant arrays!"); - if (root->stpInitialArray) { return root->stpInitialArray; } else { @@ -395,6 +393,21 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width char buf[32]; sprintf(buf, "%s_%p", root->name.c_str(), (void*) root); root->stpInitialArray = buildArray(buf, 32, 8); + + if (root->isConstantArray()) { + // FIXME: Flush the concrete values into STP. Ideally we would do this + // using assertions, which is much faster, but we need to fix the caching + // to work correctly in that case. + for (unsigned i = 0, e = root->size; i != e; ++i) { + ::VCExpr prev = root->stpInitialArray; + root->stpInitialArray = + vc_writeExpr(vc, prev, + construct(ConstantExpr::alloc(i, root->getDomain()), 0), + construct(root->constantValues[i], 0)); + vc_DeleteExpr(prev); + } + } + return root->stpInitialArray; } } -- cgit 1.4.1