From f813c88c8cb868fc9c0be78fbf92a94d72ac02b0 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Mon, 20 Nov 2023 22:41:19 +0000 Subject: Avoid generating array names in solver builders that could accidently collide If an array name ended with a number, adding a number-only suffix could generate the same name used as part of the solvers. In the specific testcase `val_1` became solver array `val_111` which collided with array `val_11` that became `val_111` as well. Using an `_` as prefix for the suffix, solves that problem in general, i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`. Fixes #1668 --- lib/Solver/STPBuilder.cpp | 4 +++- lib/Solver/Z3Builder.cpp | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) (limited to 'lib/Solver') diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 9a38183d..69a247c2 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -438,7 +438,9 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width // 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::utostr(_arr_hash._array_hash.size()); - std::string unique_name = root->name + unique_id; + // Prefix unique ID with '_' to avoid name collision if name ends with + // number + std::string unique_name = root->name + "_" + unique_id; array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index e1937158..0e51967e 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -394,7 +394,9 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { // Unique 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::utostr(_arr_hash._array_hash.size()); - std::string unique_name = root->name + unique_id; + // Prefix unique ID with '_' to avoid name collision if name ends with + // number + std::string unique_name = root->name + "_" + unique_id; array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); -- cgit 1.4.1