mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

safe sat clause_offset in debug mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-08-19 08:42:40 -07:00
parent b2383a481a
commit e132c5eae8
2 changed files with 18 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/sat/sat_clause.cpp
View file

@ -131,10 +131,12 @@ namespace sat {
clause * clause_allocator::get_clause(clause_offset cls_off) const { clause * clause_allocator::get_clause(clause_offset cls_off) const {
#if defined(_AMD64_) #if defined(_AMD64_)
#if defined (Z3DEBUG)
clause const* result; clause const* result;
if (m_overflow_valid && m_cls_offset2ptr.find(cls_off, result)) { if (m_overflow_valid && m_cls_offset2ptr.find(cls_off, result)) {
return const_cast<clause*>(result); return const_cast<clause*>(result);
} }
#endif
return reinterpret_cast<clause *>(m_segments[cls_off & c_aligment_mask] + (static_cast<size_t>(cls_off) & ~c_aligment_mask)); return reinterpret_cast<clause *>(m_segments[cls_off & c_aligment_mask] + (static_cast<size_t>(cls_off) & ~c_aligment_mask));
#else #else
return reinterpret_cast<clause *>(cls_off); return reinterpret_cast<clause *>(cls_off);
@ -152,7 +154,8 @@ namespace sat {
if (m_segments[i] == ptr) if (m_segments[i] == ptr)
return i; return i;
i = m_num_segments; i = m_num_segments;
SASSERT(m_num_segments < c_max_segments); #if defined(Z3DEBUG)
SASSERT(i < c_max_segments);
if (i + 1 == c_max_segments) { if (i + 1 == c_max_segments) {
m_overflow_valid = true; m_overflow_valid = true;
i += c_max_segments * m_cls_offset2ptr.size(); i += c_max_segments * m_cls_offset2ptr.size();
@ -160,9 +163,17 @@ namespace sat {
m_cls_offset2ptr.insert(i, cls); m_cls_offset2ptr.insert(i, cls);
} }
else { else {
m_num_segments++; ++m_num_segments;
m_segments[i] = ptr; m_segments[i] = ptr;
} }
#else
SASSERT(i <= c_max_segments);
if (i == c_max_segments) {
throw default_exception("segment out of range");
}
m_segments[i] = ptr;
++m_num_segments;
#endif
return i; return i;
} }
#endif #endif
@ -170,12 +181,12 @@ namespace sat {
clause_offset clause_allocator::get_offset(clause const * ptr) const { clause_offset clause_allocator::get_offset(clause const * ptr) const {
#if defined(_AMD64_) #if defined(_AMD64_)
unsigned segment = const_cast<clause_allocator*>(this)->get_segment(ptr); unsigned segment = const_cast<clause_allocator*>(this)->get_segment(ptr);
#if defined(Z3DEBUG)
if (segment >= c_max_segments) { if (segment >= c_max_segments) {
return m_ptr2cls_offset.find(reinterpret_cast<size_t>(ptr)); return m_ptr2cls_offset.find(reinterpret_cast<size_t>(ptr));
} }
else { #endif
return static_cast<unsigned>(reinterpret_cast<size_t>(ptr)) + segment; return static_cast<unsigned>(reinterpret_cast<size_t>(ptr)) + segment;
}
#else #else
return reinterpret_cast<size_t>(ptr); return reinterpret_cast<size_t>(ptr);
#endif #endif

2
src/sat/sat_clause.h
View file

@ -132,9 +132,11 @@ namespace sat {
static const size_t c_aligment_mask = (1ull << c_cls_alignment) - 1ull; static const size_t c_aligment_mask = (1ull << c_cls_alignment) - 1ull;
unsigned m_num_segments; unsigned m_num_segments;
size_t m_segments[c_max_segments]; size_t m_segments[c_max_segments];
#if defined(Z3DEBUG)
bool m_overflow_valid; bool m_overflow_valid;
size_t_map<unsigned> m_ptr2cls_offset; size_t_map<unsigned> m_ptr2cls_offset;
u_map<clause const*> m_cls_offset2ptr; u_map<clause const*> m_cls_offset2ptr;
#endif
#endif #endif
public: public:
clause_allocator(); clause_allocator();