mirror of
				https://github.com/Z3Prover/z3
				synced 2025-10-31 11:42:28 +00:00 
			
		
		
		
	Migrate string_buffer to use C++ smart pointer.
				
					
				
			string_buffer class is now migrated to use smart pointers instead of manually allocated and deallocated memory. The `buffer` function decides and returns if the buffer is currently using initial buffer or the allocated buffer.
This commit is contained in:
		
							parent
							
								
									c1454dc31c
								
							
						
					
					
						commit
						c56a7dff1f
					
				
					 1 changed files with 21 additions and 28 deletions
				
			
		|  | @ -27,33 +27,32 @@ | ||||||
| // This string buffer will not use the heap if the data consumes less than INITIAL_SIZE bytes. 
 | // This string buffer will not use the heap if the data consumes less than INITIAL_SIZE bytes. 
 | ||||||
| template<unsigned INITIAL_SIZE=64> | template<unsigned INITIAL_SIZE=64> | ||||||
| class string_buffer { | class string_buffer { | ||||||
|     char   m_initial_buffer[INITIAL_SIZE]; |     char m_initial_buffer[INITIAL_SIZE]; | ||||||
|     char * m_buffer; |     std::unique_ptr<char[]> m_buffer = nullptr; | ||||||
|     size_t m_pos; |     size_t m_pos; | ||||||
|     size_t m_capacity; |     size_t m_capacity; | ||||||
| 
 | 
 | ||||||
|     void expand() { |     void expand() { | ||||||
|         size_t new_capacity = m_capacity << 1; |         size_t new_capacity = m_capacity << 1; | ||||||
|         char * new_buffer   = alloc_svect(char, new_capacity); |         std::unique_ptr<char[]> new_buffer = std::make_unique<char[]>(new_capacity); | ||||||
|         memcpy(new_buffer, m_buffer, m_pos); |         memcpy(new_buffer.get(), buffer(), m_pos); | ||||||
|         if (m_capacity > INITIAL_SIZE) { |         m_buffer = std::move(new_buffer); | ||||||
|             dealloc_svect(m_buffer); |  | ||||||
|         } |  | ||||||
|         m_capacity = new_capacity; |         m_capacity = new_capacity; | ||||||
|         m_buffer   = new_buffer; |     } | ||||||
|  | 
 | ||||||
|  |     char* buffer() { | ||||||
|  |         return m_buffer ? m_buffer.get() : m_initial_buffer; | ||||||
|  |     } | ||||||
|  | 
 | ||||||
|  |     const char* buffer() const { | ||||||
|  |         return m_buffer ? m_buffer.get() : m_initial_buffer; | ||||||
|     } |     } | ||||||
| 
 | 
 | ||||||
| public:   | public:   | ||||||
|     string_buffer(): |     string_buffer(): | ||||||
|         m_buffer(m_initial_buffer), |  | ||||||
|         m_pos(0), |         m_pos(0), | ||||||
|         m_capacity(INITIAL_SIZE) { |         m_capacity(INITIAL_SIZE) { | ||||||
|     } |         // Initially, no dynamic allocation, so m_buffer is null.
 | ||||||
| 
 |  | ||||||
|     ~string_buffer() { |  | ||||||
|         if (m_capacity > INITIAL_SIZE) { |  | ||||||
|             dealloc_svect(m_buffer); |  | ||||||
|         } |  | ||||||
|     } |     } | ||||||
| 
 | 
 | ||||||
|     void reset() { |     void reset() { | ||||||
|  | @ -64,28 +63,22 @@ public: | ||||||
|         if (m_pos >= m_capacity) { |         if (m_pos >= m_capacity) { | ||||||
|             expand(); |             expand(); | ||||||
|         } |         } | ||||||
|         m_buffer[m_pos] = c; |         buffer()[m_pos] = c; | ||||||
|         m_pos++; |         m_pos++; | ||||||
|     } |     } | ||||||
| 
 | 
 | ||||||
|     void append(const char * str) { |     void append(const char * str) { | ||||||
|         size_t len       = strlen(str); |         size_t len = strlen(str); | ||||||
|         size_t new_pos = m_pos + len; |         size_t new_pos = m_pos + len; | ||||||
|         while (new_pos > m_capacity) { |         while (new_pos > m_capacity) { | ||||||
|             expand(); |             expand(); | ||||||
|         } |         } | ||||||
|         memcpy(m_buffer + m_pos, str, len); |         memcpy(buffer() + m_pos, str, len); | ||||||
|         m_pos += len; |         m_pos += len; | ||||||
|     } |     } | ||||||
| 
 | 
 | ||||||
|     void append(const std::string &str) { |     void append(const std::string &str) { | ||||||
|         size_t len     = str.size(); |         append(str.c_str()); | ||||||
|         size_t new_pos = m_pos + len; |  | ||||||
|         while (new_pos > m_capacity) { |  | ||||||
|             expand(); |  | ||||||
|         } |  | ||||||
|         memcpy(m_buffer + m_pos, str.c_str(), len); |  | ||||||
|         m_pos += len; |  | ||||||
|     } |     } | ||||||
| 
 | 
 | ||||||
|     void append(int n) { |     void append(int n) { | ||||||
|  | @ -117,10 +110,10 @@ public: | ||||||
|      |      | ||||||
|     const char * c_str() const { |     const char * c_str() const { | ||||||
|         if (m_pos >= m_capacity) { |         if (m_pos >= m_capacity) { | ||||||
|             const_cast<string_buffer * const>(this)->expand(); |             const_cast<string_buffer*>(this)->expand(); | ||||||
|         } |         } | ||||||
|         const_cast<string_buffer * const>(this)->m_buffer[m_pos] = 0; |         const_cast<string_buffer*>(this)->buffer()[m_pos] = 0; | ||||||
|         return m_buffer; |         return buffer(); | ||||||
|     } |     } | ||||||
| }; | }; | ||||||
| 
 | 
 | ||||||
|  |  | ||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue