| 187 | namespace |
| 188 | { |
| 189 | bool fillArray(smtutil::Expression const& _expr, std::vector<std::string>& _array, ArrayType const& _type) |
| 190 | { |
| 191 | // Base case |
| 192 | if (_expr.name == "const_array") |
| 193 | { |
| 194 | auto length = _array.size(); |
| 195 | std::optional<std::string> elemStr = expressionToString(_expr.arguments.at(1), _type.baseType()); |
| 196 | if (!elemStr) |
| 197 | return false; |
| 198 | _array.clear(); |
| 199 | _array.resize(length, *elemStr); |
| 200 | return true; |
| 201 | } |
| 202 | |
| 203 | // Recursive case. |
| 204 | if (_expr.name == "store") |
| 205 | { |
| 206 | if (!fillArray(_expr.arguments.at(0), _array, _type)) |
| 207 | return false; |
| 208 | std::optional<std::string> indexStr = expressionToString(_expr.arguments.at(1), TypeProvider::uint256()); |
| 209 | if (!indexStr) |
| 210 | return false; |
| 211 | // Sometimes the solver assigns huge lengths that are not related, |
| 212 | // we should catch and ignore those. |
| 213 | unsigned long index; |
| 214 | try |
| 215 | { |
| 216 | index = stoul(*indexStr); |
| 217 | } |
| 218 | catch (std::out_of_range const&) |
| 219 | { |
| 220 | return true; |
| 221 | } |
| 222 | catch (std::invalid_argument const&) |
| 223 | { |
| 224 | return true; |
| 225 | } |
| 226 | std::optional<std::string> elemStr = expressionToString(_expr.arguments.at(2), _type.baseType()); |
| 227 | if (!elemStr) |
| 228 | return false; |
| 229 | if (index < _array.size()) |
| 230 | _array.at(index) = *elemStr; |
| 231 | return true; |
| 232 | } |
| 233 | |
| 234 | // Special base case, not supported yet. |
| 235 | if (_expr.name.rfind("(_ as-array") == 0) |
| 236 | { |
| 237 | // Z3 expression representing reinterpretation of a different term as an array |
| 238 | return false; |
| 239 | } |
| 240 | |
| 241 | solAssert(false); |
| 242 | } |
| 243 | } |
| 244 | |
| 245 | std::optional<std::string> expressionToString(smtutil::Expression const& _expr, frontend::Type const* _type) |
no test coverage detected