mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Adding overflow checks

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-02 19:43:22 -07:00
parent fcc351eba6
commit 878905c13c
4 changed files with 30 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/muz/rel/dl_sparse_table.cpp
View file

@ -1066,11 +1066,14 @@ namespace datalog {
unsigned res_fact_size = res->m_fact_size;
unsigned res_data_size = res_fact_size*t.row_count();
if (res_fact_size != 0 && (res_data_size / res_fact_size) != t.row_count()) {
throw default_exception("multiplication overflow");
}
res->m_data.resize_data(res_data_size);
//here we can separate data creatin and insertion into hashmap, since we know
//that no row will become duplicit
//here we can separate data creating and insertion into hashmap, since we know
//that no row will become duplicate
//create the data
const char* t_ptr = t.m_data.begin();

3
src/muz/rel/dl_sparse_table.h
View file

@ -275,6 +275,9 @@ namespace datalog {
//the following two operations allow breaking of the object invariant!
void resize_data(unsigned sz) {
m_data_size = sz;
if (sz + sizeof(uint64) < sz) {
throw default_exception("overflow resizing data section for sparse table");
}
m_data.resize(sz + sizeof(uint64));
}

18
src/test/vector.cpp
View file

@ -19,7 +19,7 @@ Revision History:
#include"vector.h"
static void tst1() {
vector<int> v1;
svector<int> v1;
SASSERT(v1.empty());
for (unsigned i = 0; i < 1000; i++) {
v1.push_back(i + 3);
@ -30,8 +30,8 @@ static void tst1() {
for (unsigned i = 0; i < 1000; i++) {
SASSERT(static_cast<unsigned>(v1[i]) == i + 3);
}
vector<int>::iterator it = v1.begin();
vector<int>::iterator end = v1.end();
svector<int>::iterator it = v1.begin();
svector<int>::iterator end = v1.end();
for (int i = 0; it != end; ++it, ++i) {
SASSERT(*it == i + 3);
}
@ -42,6 +42,18 @@ static void tst1() {
}
SASSERT(v1.empty());
SASSERT(v1.size() == 0);
unsigned i = 1000000000;
while (true) {
std::cout << "resize " << i << "\n";
try {
v1.resize(i);
}
catch (z3_exception& e) {
std::cout << e.msg() << "\n";
break;
}
i *= 2;
}
}
void tst_vector() {

8
src/util/vector.h
View file

@ -29,6 +29,7 @@ Revision History:
#include<memory.h>
#include"memory_manager.h"
#include"hash.h"
#include"z3_exception.h"
// disable warning for constant 'if' expressions.
// these are used heavily in templates.
@ -67,9 +68,14 @@ class vector {
else {
SASSERT(capacity() > 0);
unsigned old_capacity = reinterpret_cast<unsigned *>(m_data)[CAPACITY_IDX];
unsigned old_capacity_T = sizeof(T) * old_capacity + sizeof(unsigned) * 2;
unsigned new_capacity = (3 * old_capacity + 1) >> 1;
unsigned new_capacity_T = sizeof(T) * new_capacity + sizeof(unsigned) * 2;
unsigned size = reinterpret_cast<unsigned *>(m_data)[SIZE_IDX];
unsigned * mem = reinterpret_cast<unsigned*>(memory::allocate(sizeof(T) * new_capacity + sizeof(unsigned) * 2));
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
throw default_exception("Overflow encountered when expanding vector");
}
unsigned * mem = reinterpret_cast<unsigned*>(memory::allocate(new_capacity_T));
*mem = new_capacity;
mem ++;
*mem = size;