Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/context/context_mm.cpp	Lines:	58	62	93.5 %
Date:	2021-09-19	Branches:	36	100	36.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Clark Barrett, Andres Noetzli, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of Context Memory Manager
 */

#include <cstdlib>
#include <deque>
#include <limits>
#include <new>
#include <ostream>
#include <vector>

#ifdef CVC5_VALGRIND
#include <valgrind/memcheck.h>
#endif /* CVC5_VALGRIND */

#include "base/check.h"
#include "base/output.h"
#include "context/context_mm.h"

namespace cvc5 {
namespace context {

#ifndef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER

void ContextMemoryManager::newChunk() {

  // Increment index to chunk list
  ++d_indexChunkList;
  Assert(d_chunkList.size() == d_indexChunkList)
      << "Index should be at the end of the list";

  // Create new chunk if no free chunk available
  if(d_freeChunks.empty()) {
    d_chunkList.push_back((char*)malloc(chunkSizeBytes));
    if(d_chunkList.back() == NULL) {
      throw std::bad_alloc();
    }

#ifdef CVC5_VALGRIND
    VALGRIND_MAKE_MEM_NOACCESS(d_chunkList.back(), chunkSizeBytes);
#endif /* CVC5_VALGRIND */
  }
  // If there is a free chunk, use that
  else {
    d_chunkList.push_back(d_freeChunks.back());
    d_freeChunks.pop_back();
  }
  // Set up the current chunk pointers
  d_nextFree = d_chunkList.back();
  d_endChunk = d_nextFree + chunkSizeBytes;
}


ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) {
  // Create initial chunk
  d_chunkList.push_back((char*)malloc(chunkSizeBytes));
  d_nextFree = d_chunkList.back();
  if(d_nextFree == NULL) {
    throw std::bad_alloc();
  }
  d_endChunk = d_nextFree + chunkSizeBytes;

#ifdef CVC5_VALGRIND
  VALGRIND_CREATE_MEMPOOL(this, 0, false);
  VALGRIND_MAKE_MEM_NOACCESS(d_nextFree, chunkSizeBytes);
  d_allocations.push_back(std::vector<char*>());
#endif /* CVC5_VALGRIND */
}


ContextMemoryManager::~ContextMemoryManager() {
#ifdef CVC5_VALGRIND
  VALGRIND_DESTROY_MEMPOOL(this);
#endif /* CVC5_VALGRIND */

  // Delete all chunks
  while(!d_chunkList.empty()) {
    free(d_chunkList.back());
    d_chunkList.pop_back();
  }
  while(!d_freeChunks.empty()) {
    free(d_freeChunks.back());
    d_freeChunks.pop_back();
  }
}


void* ContextMemoryManager::newData(size_t size) {
  // Use next available free location in current chunk
  void* res = (void*)d_nextFree;
  d_nextFree += size;
  // Check if the request is too big for the chunk
  if(d_nextFree > d_endChunk) {
    newChunk();
    res = (void*)d_nextFree;
    d_nextFree += size;
    AlwaysAssert(d_nextFree <= d_endChunk)
        << "Request is bigger than memory chunk size";
  }
  Debug("context") << "ContextMemoryManager::newData(" << size
                   << ") returning " << res << " at level "
                   << d_chunkList.size() << std::endl;

#ifdef CVC5_VALGRIND
  VALGRIND_MEMPOOL_ALLOC(this, static_cast<char*>(res), size);
  d_allocations.back().push_back(static_cast<char*>(res));
#endif /* CVC5_VALGRIND */

  return res;
}


void ContextMemoryManager::push() {
#ifdef CVC5_VALGRIND
  d_allocations.push_back(std::vector<char*>());
#endif /* CVC5_VALGRIND */

  // Store current state on the stack
  d_nextFreeStack.push_back(d_nextFree);
  d_endChunkStack.push_back(d_endChunk);
  d_indexChunkListStack.push_back(d_indexChunkList);
}


void ContextMemoryManager::pop() {
#ifdef CVC5_VALGRIND
  for (auto allocation : d_allocations.back())
  {
    VALGRIND_MEMPOOL_FREE(this, allocation);
  }
  d_allocations.pop_back();
#endif /* CVC5_VALGRIND */

  Assert(d_nextFreeStack.size() > 0 && d_endChunkStack.size() > 0);

  // Restore state from stack
  d_nextFree = d_nextFreeStack.back();
  d_nextFreeStack.pop_back();
  d_endChunk = d_endChunkStack.back();
  d_endChunkStack.pop_back();

  // Free all the new chunks since the last push
  while(d_indexChunkList > d_indexChunkListStack.back()) {
    d_freeChunks.push_back(d_chunkList.back());
#ifdef CVC5_VALGRIND
    VALGRIND_MAKE_MEM_NOACCESS(d_chunkList.back(), chunkSizeBytes);
#endif /* CVC5_VALGRIND */
    d_chunkList.pop_back();
    --d_indexChunkList;
  }
  d_indexChunkListStack.pop_back();

  // Delete excess free chunks
  while(d_freeChunks.size() > maxFreeChunks) {
    free(d_freeChunks.front());
    d_freeChunks.pop_front();
  }
}
#else

unsigned ContextMemoryManager::getMaxAllocationSize()
{
  return std::numeric_limits<unsigned>::max();
}

#endif /* CVC5_DEBUG_CONTEXT_MEMORY_MANAGER */

}  // namespace context
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Clark Barrett, Andres Noetzli, Morgan Deters
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of Context Memory Manager
14		*/
15
16		#include <cstdlib>
17		#include <deque>
18		#include <limits>
19		#include <new>
20		#include <ostream>
21		#include <vector>
22
23		#ifdef CVC5_VALGRIND
24		#include <valgrind/memcheck.h>
25		#endif /* CVC5_VALGRIND */
26
27		#include "base/check.h"
28		#include "base/output.h"
29		#include "context/context_mm.h"
30
31		namespace cvc5 {
32		namespace context {
33
34		#ifndef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER
35
36	598843	void ContextMemoryManager::newChunk() {
37
38		// Increment index to chunk list
39	598843	++d_indexChunkList;
40	598843	Assert(d_chunkList.size() == d_indexChunkList)
41		<< "Index should be at the end of the list";
42
43		// Create new chunk if no free chunk available
44	598843	if(d_freeChunks.empty()) {
45	95772	d_chunkList.push_back((char*)malloc(chunkSizeBytes));
46	95772	if(d_chunkList.back() == NULL) {
47		throw std::bad_alloc();
48		}
49
50		#ifdef CVC5_VALGRIND
51		VALGRIND_MAKE_MEM_NOACCESS(d_chunkList.back(), chunkSizeBytes);
52		#endif /* CVC5_VALGRIND */
53		}
54		// If there is a free chunk, use that
55		else {
56	503071	d_chunkList.push_back(d_freeChunks.back());
57	503071	d_freeChunks.pop_back();
58		}
59		// Set up the current chunk pointers
60	598843	d_nextFree = d_chunkList.back();
61	598843	d_endChunk = d_nextFree + chunkSizeBytes;
62	598843	}
63
64
65	1909270	ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) {
66		// Create initial chunk
67	1909270	d_chunkList.push_back((char*)malloc(chunkSizeBytes));
68	1909270	d_nextFree = d_chunkList.back();
69	1909270	if(d_nextFree == NULL) {
70		throw std::bad_alloc();
71		}
72	1909270	d_endChunk = d_nextFree + chunkSizeBytes;
73
74		#ifdef CVC5_VALGRIND
75		VALGRIND_CREATE_MEMPOOL(this, 0, false);
76		VALGRIND_MAKE_MEM_NOACCESS(d_nextFree, chunkSizeBytes);
77		d_allocations.push_back(std::vector<char*>());
78		#endif /* CVC5_VALGRIND */
79	1909270	}
80
81
82	5680020	ContextMemoryManager::~ContextMemoryManager() {
83		#ifdef CVC5_VALGRIND
84		VALGRIND_DESTROY_MEMPOOL(this);
85		#endif /* CVC5_VALGRIND */
86
87		// Delete all chunks
88	5680020	while(!d_chunkList.empty()) {
89	1893340	free(d_chunkList.back());
90	1893340	d_chunkList.pop_back();
91		}
92	52477	while(!d_freeChunks.empty()) {
93	52477	free(d_freeChunks.back());
94	52477	d_freeChunks.pop_back();
95		}
96	1893340	}
97
98
99	127970690	void* ContextMemoryManager::newData(size_t size) {
100		// Use next available free location in current chunk
101	127970690	void* res = (void*)d_nextFree;
102	127970690	d_nextFree += size;
103		// Check if the request is too big for the chunk
104	127970690	if(d_nextFree > d_endChunk) {
105	598843	newChunk();
106	598843	res = (void*)d_nextFree;
107	598843	d_nextFree += size;
108	598843	AlwaysAssert(d_nextFree <= d_endChunk)
109		<< "Request is bigger than memory chunk size";
110		}
111	255941380	Debug("context") << "ContextMemoryManager::newData(" << size
112	127970690	<< ") returning " << res << " at level "
113	127970690	<< d_chunkList.size() << std::endl;
114
115		#ifdef CVC5_VALGRIND
116		VALGRIND_MEMPOOL_ALLOC(this, static_cast<char*>(res), size);
117		d_allocations.back().push_back(static_cast<char*>(res));
118		#endif /* CVC5_VALGRIND */
119
120	127970690	return res;
121		}
122
123
124	3578616	void ContextMemoryManager::push() {
125		#ifdef CVC5_VALGRIND
126		d_allocations.push_back(std::vector<char*>());
127		#endif /* CVC5_VALGRIND */
128
129		// Store current state on the stack
130	3578616	d_nextFreeStack.push_back(d_nextFree);
131	3578616	d_endChunkStack.push_back(d_endChunk);
132	3578616	d_indexChunkListStack.push_back(d_indexChunkList);
133	3578616	}
134
135
136	3578607	void ContextMemoryManager::pop() {
137		#ifdef CVC5_VALGRIND
138		for (auto allocation : d_allocations.back())
139		{
140		VALGRIND_MEMPOOL_FREE(this, allocation);
141		}
142		d_allocations.pop_back();
143		#endif /* CVC5_VALGRIND */
144
145	3578607	Assert(d_nextFreeStack.size() > 0 && d_endChunkStack.size() > 0);
146
147		// Restore state from stack
148	3578607	d_nextFree = d_nextFreeStack.back();
149	3578607	d_nextFreeStack.pop_back();
150	3578607	d_endChunk = d_endChunkStack.back();
151	3578607	d_endChunkStack.pop_back();
152
153		// Free all the new chunks since the last push
154	4776293	while(d_indexChunkList > d_indexChunkListStack.back()) {
155	598843	d_freeChunks.push_back(d_chunkList.back());
156		#ifdef CVC5_VALGRIND
157		VALGRIND_MAKE_MEM_NOACCESS(d_chunkList.back(), chunkSizeBytes);
158		#endif /* CVC5_VALGRIND */
159	598843	d_chunkList.pop_back();
160	598843	--d_indexChunkList;
161		}
162	3578607	d_indexChunkListStack.pop_back();
163
164		// Delete excess free chunks
165	3665197	while(d_freeChunks.size() > maxFreeChunks) {
166	43295	free(d_freeChunks.front());
167	43295	d_freeChunks.pop_front();
168		}
169	3578607	}
170		#else
171
172		unsigned ContextMemoryManager::getMaxAllocationSize()
173		{
174		return std::numeric_limits<unsigned>::max();
175		}
176
177		#endif /* CVC5_DEBUG_CONTEXT_MEMORY_MANAGER */
178
179		} // namespace context
180	29583	} // namespace cvc5