Nana is a library that provides support for assertion checking and logging in a space and time efficient manner. The aim is to put common good practice1 into a library that can be reused rather than writing this stuff every time you begin a new project.
In addition assertion checking and logging code can be implemented using a debugger rather than as inline code with a large saving in code space.
Nana aims to solve the following problems:
The code space and time costs of having assertion checking and detailed logging code in a program can be high. Normally people construct two versions of the program, one with checking code for testing and one without checking code for production use.
With nana one version of the executable can be built for both testing and release since debugger based checking has negligible space and time impact.
This is an old embedded systems trick and is very useful for production systems. The time cost of logging into memory is not large and when your production system in the field has problems you can then see what was happening in the minutes before its unfortunate demise rather than asking some user what was happening before it died.
For example the GNU ‘assert.h’ implementation uses 53 bytes for ‘assert(i>=0)’ on a i386. The nana version using the i386 ‘stp’ instruction on assert fail uses 10 bytes. If you're willing to accept the time penalty this can be reduced to 0 or 1 byte by using debugger based assertions.
Specifications are often written in terms of the state of variables before and after an operation. For example the ‘isempty’ operation on a stack should leave the stack unchanged. To verify this in nana we could use:
bool isempty(){ /* true iff stack is empty */ DS($s = s); /* copy s into $s in the debugger */ ...; /* code to do the operation */ DI($s == s); /* verify that s hasn't been changed */ }
These ‘$..’ variables are called convenience variables and are implemented by gdb. They have a global scope and are dynamically typed and initialised automatically to 0.
In addition a C only version of before and after state is provided. For example:
bool isempty() { /* true iff stack is empty */ ID(int olds); /* declare variable to hold old value */ IS(olds = s); /* copy s into $s in the debugger */ ...; /* code to do the operation */ I(olds == s); /* verify that s hasn't been changed */ }
Nana provides some support for universal (forall) and existential (exists one or more) quantification. For example to specify that the string v contains only lower case letters we could use:
I(A(char *p = v, *p != '\0', p++, islower(*p)));
These macros can be nested and used as normal boolean values in control constructs as well as assertions. Unfortunately they depend on the GNU CC statement value extensions and so are not portable. The following macros are defined in ‘Q.h’:
A
E
E1
C
S
P
The shortform of a program consists of the function headers together with their preconditions2 and postconditions3
A small package which measures the time and space overhead of code fragments is provided. This is used to analyse the space/time requirements of the nana library and could be used for other types of measurement.
As well as using nana to verify timings with assertions using a hardware supported timer you can also a simulator (e.g. the PSIM power pc simulator by Cagney) with gdb. These simulators can model time and provide a register called ‘$cycles’ which represents the current cycle count of the program. This can be used to check that timing constraints are being meet.
void process_events() { for(;;){ DS($start = $cycles); switch(get_event()){ case TOO_HOT: ...; DI($cycles - $start <= 120); break; case TOO_COLD: ...; DI($cycles - $start <= 240); break; } } }
The intended audience for Nana includes:
[1] Which is unfortunately quite uncommon in the authors experience.
[2] Precondition: a boolean expression which must be true if the operation is to succeed. For example the ‘sort(int *v, int n)’ might have have precondition that ‘v != NULL && n >= 0’.
[3] Postcondition: a boolean expression that must be true if the operation is correct (and the precondition was true on entry).