mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 15:02:09 +00:00
Code Activity

Fix vector byte-size overflow during expansion

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-08-07 06:36:13 +00:00 • committed by GitHub
parent c4fbb948ff
commit a37f306cb4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/test/vector.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include "util/vector.h"
#include "util/rational.h"
#include <iostream>
#include <cstdint>
static void tst_resize_rational() {
// grow from empty using default initialization (zero)
@ -141,8 +142,16 @@ static void tst1() {
}
}
static void tst_expand_vector_byte_count() {
vector<uint16_t, true, uint8_t> v;
for (unsigned i = 0; i < 192; ++i)
v.push_back(i);
ENSURE(v.size() == 192);
}
void tst_vector() {
tst_resize_rational();
tst_resize();
tst1();
tst_expand_vector_byte_count();
}

4
src/util/vector.h
View file

@ -80,9 +80,9 @@ class vector {
static_assert(std::is_nothrow_move_constructible<T>::value);
SASSERT(capacity() > 0);
SZ old_capacity = reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
size_t old_capacity_T = sizeof(T) * static_cast<size_t>(old_capacity) + sizeof(SZ) * 2;
SZ new_capacity = (3 * old_capacity + 1) >> 1;
SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
size_t new_capacity_T = sizeof(T) * static_cast<size_t>(new_capacity) + sizeof(SZ) * 2;
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
throw default_exception("Overflow encountered when expanding vector");
}