1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     region.cpp
7 
8 Abstract:
9 
10     Region/Arena memory manager
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2006-09-18.
15 
16 Revision History:
17 
18 --*/
19 #include "util/region.h"
20 
21 #ifdef Z3DEBUG
22 
display_mem_stats(std::ostream & out) const23 void region::display_mem_stats(std::ostream & out) const {
24     out << "num. objects:      " << m_chunks.size() << "\n";
25 }
26 
allocate(size_t size)27 void * region::allocate(size_t size) {
28     char * r = alloc_svect(char, size);
29     m_chunks.push_back(r);
30     return r;
31 }
32 
reset()33 void region::reset() {
34     for (auto* c : m_chunks)
35         dealloc_svect(c);
36     m_chunks.reset();
37     m_scopes.reset();
38 }
39 
pop_scope()40 void region::pop_scope() {
41     unsigned old_size = m_scopes.back();
42     m_scopes.pop_back();
43     ptr_vector<char>::iterator it  = m_chunks.begin() + old_size;
44     ptr_vector<char>::iterator end = m_chunks.end();
45     for (; it != end; ++it)
46         dealloc_svect(*it);
47     m_chunks.shrink(old_size);
48 }
49 
50 
51 #else
52 
53 #include "util/tptr.h"
54 #include "util/debug.h"
55 #include "util/memory_manager.h"
56 #include "util/page.h"
57 
allocate_page()58 inline void region::allocate_page() {
59     m_curr_page     = allocate_default_page(m_curr_page, m_free_pages);
60     m_curr_ptr      = m_curr_page;
61     m_curr_end_ptr  = end_of_default_page(m_curr_page);
62 }
63 
region()64 region::region() {
65     m_curr_page    = nullptr;
66     m_curr_ptr     = nullptr;
67     m_curr_end_ptr = nullptr;
68     m_free_pages   = nullptr;
69     m_mark         = nullptr;
70     allocate_page();
71 }
72 
~region()73 region::~region() {
74     del_pages(m_curr_page);
75     del_pages(m_free_pages);
76 }
77 
allocate(size_t size)78 void * region::allocate(size_t size) {
79     char * new_curr_ptr = m_curr_ptr + size;
80     if (new_curr_ptr < m_curr_end_ptr) {
81         char * result = m_curr_ptr;
82         m_curr_ptr = ALIGN(char *, new_curr_ptr);
83         return result;
84     }
85     else if (size < DEFAULT_PAGE_SIZE) {
86         allocate_page();
87         char * result = m_curr_ptr;
88         m_curr_ptr += size;
89         m_curr_ptr = ALIGN(char *, m_curr_ptr);
90         return result;
91     }
92     else {
93         // big page
94         m_curr_page = ::allocate_page(m_curr_page, size);
95         char * result = m_curr_page;
96         allocate_page();
97         return result;
98     }
99 }
100 
recycle_curr_page()101 inline void region::recycle_curr_page() {
102     char * prev = prev_page(m_curr_page);
103     recycle_page(m_curr_page, m_free_pages);
104     m_curr_page = prev;
105 }
106 
reset()107 void region::reset() {
108     while (m_curr_page != nullptr) {
109         recycle_curr_page();
110     }
111     SASSERT(m_curr_page == 0);
112     m_curr_ptr     = nullptr;
113     m_curr_end_ptr = nullptr;
114     m_mark         = nullptr;
115     allocate_page();
116 }
117 
push_scope()118 void region::push_scope() {
119     char * curr_page = m_curr_page;
120     char * curr_ptr  = m_curr_ptr;
121     m_mark = new (*this) mark(curr_page, curr_ptr, m_mark);
122 }
123 
pop_scope()124 void region::pop_scope() {
125     SASSERT(m_mark);
126     char * old_curr_page = m_mark->m_curr_page;
127     SASSERT(is_default_page(old_curr_page));
128     m_curr_ptr           = m_mark->m_curr_ptr;
129     m_mark               = m_mark->m_prev_mark;
130     while (m_curr_page != old_curr_page) {
131         recycle_curr_page();
132     }
133     SASSERT(is_default_page(m_curr_page));
134     m_curr_end_ptr       = end_of_default_page(m_curr_page);
135 }
136 
display_mem_stats(std::ostream & out) const137 void region::display_mem_stats(std::ostream & out) const {
138     unsigned n = 0;
139     char * page = m_curr_page;
140     while (page != nullptr) {
141         n++;
142         page = prev_page(page);
143     }
144     out << "num. pages:      " << n << "\n";
145 }
146 
147 #endif
148 
149