From fef5893503cd35786a15485406bb08cd1c031b9e Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Sun, 26 Apr 2020 17:27:24 +0100 Subject: [Solver:STP] Fix handling of array names Array names used for STP queries used to be restricted to 32 characters, with the last characters replaced by a unique number. Similarly, an array is made unique by `klee_make_symbolic`. Unfortunately, both combined can lead to the generation of the same STP array name for different arrays. This leads to wrong queries with invalid results. This is more likely be triggered with longer names for `klee_make_symbolic` Fixes #1257 --- lib/Solver/STPBuilder.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'lib/Solver/STPBuilder.cpp') diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 9fd9dc8e..13a42513 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -436,12 +436,8 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width if (!hashed) { // STP uniques arrays by name, so we make sure the name is unique by // using the size of the array hash as a counter. - std::string unique_id = llvm::itostr(_arr_hash._array_hash.size()); - unsigned const uid_length = unique_id.length(); - unsigned const space = (root->name.length() > 32 - uid_length) - ? (32 - uid_length) - : root->name.length(); - std::string unique_name = root->name.substr(0, space) + unique_id; + std::string unique_id = llvm::utostr(_arr_hash._array_hash.size()); + std::string unique_name = root->name + unique_id; array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); -- cgit 1.4.1