Allocation

Vampire has an atypical heap allocation profile, allocating large numbers of small objects which live either indefinitely or for a very short time. The size of (de)allocations is almost always available externally to the memory allocator. All allocations are single-threaded, but must be signal-safe.

System allocators do not typically handle this case well. Vampire therefore partially handles its own memory allocation in Lib::Allocator, wrapping the underlying system allocator with a simple small-object allocator.

Vampire developers should not have to interact with Vampire's allocator unless they suspect it would improve performance. However, historically this was not the case and all allocations had to be routed via Vampire's allocator. The following information no longer applies, but is preserved for historical interest.

---

Hi all,

Attempt to use global operator new, thus bypassing Allocator!

since my recent pull request has been merged into master you may possibly encounter the above error message (in fact, it's a string associated with an asserted violation) or similar when running your version of vampire.

What it means is that the execution has reached a point where a call to operator new (new[] / delete, delete[]) has been made for a class which is not registered by vampire's Allocator. Since we strive to channel all allocations to Allocator for various reasons, this shouldn't be happening. The standard remedy is to decorate the offending class by the famous two lines in its public section

CLASS_NAME(XXX); USE_ALLOCATOR(XXX);

where XXX is the name of the class. (There is also USE_ALLOCATOR_ARRAY(XXX) for the cases where we want to call new[] for a particular class. It happens very seldom.)

For the cases, where the class is not from vampire and so cannot be modified, there are two possibilities.

1. It is a string, ostringstream, istringstream, stringstream from the namespace std.

Solution: Use vstring, vostringstream, vistringstream, vstringstream (header Lib/VString.hpp) instead.

2. it is another stl class or a third party class.

Solution: Mark the closest scope by a call to a magical macro BYPASSING_ALLOCATOR; This serves as documentation and it will also disable the said assertion within the scope and below.

Example:

bool System::fileExists(vstring fname) { CALL("System::fileExists"); BYPASSING_ALLOCATOR;

ifstream ifile(fname.c_str()); return ifile; }

Note that the assertion is only working in VDEBUG mode so it should never bother our users with release executables. In release, the offending calls silently channel to system's new/delete and BYPASSING_ALLOCATOR is a no-op.

Please let me know if you encounter any problems when dealing with this.

Cheers,

Martin