%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% File  : basics.tex
%
% Author: Stephan Schulz
%
% Contents
% 
%   Documentation for the BASIC sublibrary of CLIB.
% 
% Changes
%
% <1> Thu Apr 16 03:18:43 MET DST 1998
%     Added this comment header ;-)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Basic Services}
\label{sec:basics}

The BASICS part of the library implements general infrastructure
useful for most programs. This ranges from elementary things like a
\texttt{bool} data type and a NULL pointer to error handling and
memory management.


\subsection{Miscellaneous Stuff}
\label{sec:basics:elementary}


\subsubsection{Usage Information}

\begin{verbatim}
#include <clb_defines.h>

Requires: -
\end{verbatim}

\subsubsection{The \texttt{NULL} Pointer}

\ldots{} is defined as expected. 


\subsubsection{Booleans}

The \texttt{bool} data type can be used in specifications and offers
the two truth values \texttt{true} and \texttt{false} with a twist:
There exist multiple synonyms for both values, to enable the
programmer to put some semantic information into the program code.

The \texttt{bool} data type is currently defined as follows:

\begin{verbatim}
typedef enum
{
   false = 0,
   normal = 0,
   brief = 0,
   true = 1,
   special = 1,
   verbose = 1
}bool;
\end{verbatim}

The C language allows arbitrary values of integer data types
(\texttt{char}, \texttt{int}, \texttt{long} in signed and unsigned
variations, but also all pointer types) as truth values. Only
\texttt{0}\footnote{More exactly, the value that is generated by the
  compiler for the textual string ``\texttt{0}'' in the given type.}
is interpreted as \texttt{false}, all other values are conceptually
equivalent to \texttt{true}. \emph{This means that you cannot compare
  two truth values with \texttt{==} and expect a reasonable result}.
Think about it. \emph{You cannot compare two truth values with
  \texttt{==} and expect a reasonable result}. The various
representations of \texttt{true} are only useful for parameter passing
and variable assignements.


\subsubsection{Generic Integer Types}

The C programming language does not offer truly generic data types.
There are only two ways to manipulate data of more than one type:
Using macros as untyped functions, or using \texttt{void*} pointers as
generic pointers. Both solutions have disadvantages. However, in some
cases the advantages (avoiding the duplication of code) far outweight
the disadvantages of weakening the type concept. For these situations,
CLIB offers a generic data type that can store any pointer value, as
well as \texttt{long} integers (including, of course, values from
subtypes of \texttt{long}). For most implementations of the C
programming language, all of these data types have a 32 bit
representation, and there is no cost for converting between these
types.

The \texttt{IntOrP} data type is defined as a union of a
\texttt{void*} pointer and a \texttt{long} integer:

\begin{verbatim}
typedef union int_or_p
{
   long i_val;
   void *p_val;
}IntOrP;
\end{verbatim}

The two fields have the obvious meaning: Use \texttt{i\_val} to store
numeric values and \texttt{p\_val} for arbitrary pointer types.



\subsubsection{Simple Macros}

For all of these macros, arguments may possibly be evaluated more than
once, i.e. they should probably be free from side effects.

\begin{verbatim}
MACRO MAX(x,y)
MACRO MIN(x,y)
\end{verbatim}
\begin{quote}
  Maximum and minimum of two values for which the \texttt{>} and
  \texttt{<} operators are defined.
\end{quote}

\begin{verbatim}
MACRO ABS(x)
\end{verbatim}
\begin{quote}
  Absolute value of a numerical argument.
\end{quote}

\begin{verbatim}
MACRO XOR(x,y)
\end{verbatim}
\begin{quote}
  \emph{Exclusive or} of two values that are interpreted as truth
  values.
\end{quote}


\subsection{Errors and Runtime Information}
\label{sec:basics:errors}

Programs sometimes need to report special events, e.g. transistion
between different phases or, most importantly, errors during
execution. CLIB distinguishes between \emph{errors}, that always lead
to the termination of the program, \emph{warnings}, which warn the
user about expceptional, but non-critical conditions, and
\emph{verbose messages}, which result from the ordinary execution of
the program.

\subsubsection{Usage Information}

\begin{verbatim}
#include <clb_error.h>
#include <clb_verbose.h>

Requires: lib/BASICS.a
\end{verbatim}


\subsubsection{Errors}

Facilities for error handling fall into two classes: Initialization
routines and global state variables that remain constant after
initialization, and routines and variables that are used only in the
case of error. Initialization of the error handling module is very
simple:

\begin{verbatim}
void         InitError(char* progname)
extern char* ProgName
\end{verbatim}
\begin{quote}
  \texttt{InitError()} stores the name of the program for error
  reporting. The argument has to be a pointer to a constant string
  (giving the name of the program), typically \texttt{argv[0]}. The
  name is available to other parts of the program via the exported
  variable \texttt{ProgName}.
\end{quote}

CLIB always assumes that \emph{errors} are non-recoverable and should
terminate the program. In this case, the program should return an exit
code (via the standard library call \texttt{exit()}) describing the
error condition. Some exit codes are predefined in the enumeration
type \texttt{ErrorCodes}:

\begin{description}
\item[\texttt{NO\_ERROR}:] No error, successful termination of the
  program.
\item[\texttt{OUT\_OF\_MEMORY}:] The program was unable to allocate
  memory. This error will usually be generated by the memory
  management module if a request for memory cannot be satsified.
\item[\texttt{SYNTAX\_ERROR}:] Input to the program does not conform
  to the specification (or rather the implemented parser).
\item[\texttt{USAGE\_ERROR}:] The program was started with incorrect
  options or other arguments.
\item[\texttt{FILE\_ERROR}:] A file operation (usually opening or
  closing) failed.
\item[\texttt{SYS\_ERROR}:] An unspecified system call signalled an
  error.
\end{description}

Reporting an error requires an error code (used as an exit code for
the environment) and an error message for the user. Error messages are
often dynamically generated and include file names or other program
arguments. For simple cases, \texttt{sprintf()} is usually sufficient
to create an error message\footnote{See the \texttt{clb\_dstring}
  module (Sec.~\ref{sec:basics:strings}) for more general, but usually
  less convenient string manipulation functions.}.

\begin{verbatim}
extern char  ErrStr[]
\end{verbatim}
\begin{quote}
  This variable reserves at least \texttt{MAX\_ERRMSG\_LEN} characters
  for creating error messages. This space is always sufficient to
  store any valid UNIX file name and at least
  \texttt{MAX\_ERRMSG\_ADD} additional characters.  You can assume
  that \texttt{MAX\_ERRMSG\_ADD} is large enough for most practical
  considerations.
\end{quote}

\begin{verbatim}
VOLATILE void Error(char* message, ErrorCodes ret)
\end{verbatim}
\begin{quote}
  Print an error message (including the program name and the given
  message) to \texttt{stderr}, and exit the program with the exit code
  \texttt{ret}.
\end{quote}

Failing UNIX system calls or C library calls usually give some
indication about the reason why they failed in the global varible
\texttt{errno} (declared in the standard header file
\texttt{<errno.h>}). If you want to pass on this information to the
user, you should save this value in the CLIB global
variable\footnote{Using global variables for communication between
  functions is usually a bad idea. However, in this case there is a
  very good reason to break with this rule. After catching an error,
  it is usually unavoidable to do further system calls before
  reporting it (e.g.  calls to \texttt{sprintf()} for composing an
  error message). Not all implementations of the C standard library
  guarantee to save the original value of \texttt{errno} during
  successful library calls.  Therefore, it is necessary for the user
  program to save this value.  Using a local variable wherever
  \texttt{errno} is checked is extremely tedious and quite
  inefficient. Using a global variable, on the other hand, is quite
  simple. It also mirrors the standard use of \texttt{errno}.}
\texttt{TmpErrno} and call \texttt{SysError()} to exit the program.

\begin{verbatim}
extern   int  TmpErrno
VOLATILE void SysError(char* message, ErrorCodes ret)
\end{verbatim}
\begin{quote}
  \texttt{SysError()} will print an error message, including the
  program name and the message passed to it, to \texttt{stderr}. It
  will then print the system error message associated with the value
  in \texttt{TmpErrno} and exit the program with the exit code
  \texttt{ret}.
\end{quote}

For less drastic exceptional conditions, you can also issue a warning
instead of an error. Warnings will not terminate the program.

\begin{verbatim}
void Warning(char* message)
\end{verbatim}
\begin{quote}
  Print a message, containing the program name and the passed message,
  to \texttt{stderr}.
\end{quote}


\subsubsection{Example}

The following example (taken from \texttt{cio\_output.c} in the INOUT
part of the library) illustrates the use of \texttt{ErrStr} and the
\texttt{SysError()} routine:

\begin{verbatim}
  char *name;
  ...
  if(! (out = fopen(name,"w")))
  {
     TmpErrno = errno; /* Save error number, the following call
                          to sprintf() can theoretically alter
                          the value !*/
     sprintf(ErrStr, "Cannot open file %s", name);
     SysError(ErrStr, FILE_ERROR);
  }
  ...
\end{verbatim}



\subsection{Memory Management}
\label{sec:basics:memory}

General memory management routines as offered by most operating
systems or standard libraries have to cater for the demands of many
different programs. Theorem provers, on the other hand, have very
regular memory allocation patterns: The vast majority of all memory
requests is for small blocks of only very few different sizes (terms
cells, literals, clauses). Such request patterns can be served more
efficiently by a specialized memory managment interface as implemented
in the clib module \texttt{clb\_memory}.

\subsubsection{Usage Information}

\begin{verbatim}
#include <clb_memory.h>

Requires: lib/BASICS.a
\end{verbatim}

\subsubsection{Allocating and Freeing Memory Blocks}

CLIB offers different replacements for the simple UNIX
\texttt{malloc()} and \texttt{free()} functions. Currently, all memory
blocks allocated via calls to CLIB specific memory functions can be
deallocated via the conventional memory menagement interface, and vice
versa\footnote{This is of course not a good idea, as it wastes all the
  advantages of a specialized memory management module.}.

\begin{verbatim}
void* SizeMalloc(int size)
void  SizeFree(void* junk, int size)
\end{verbatim}
\begin{quote}
  Allocate or deallocate a memory block of a given size. These
  functions should be used to deal with blocks of constant, predicable
  size. This can be most conveniently be ensured by defining macro
  allocators and deallocators for all (or most) data types. See the
  \texttt{DataCellAlloc()} and \texttt{DataCellFree()} macros in
  \texttt{clb\_memory.h} for an example.
\end{quote}

\begin{verbatim}
void MemFlushFreeList()
\end{verbatim}
\begin{quote}
  This function will release all memory stored by the internal free
  lists of the memory management module, allowing the reorganization
  of this memory. The function will automatically be called if the
  memory management functions cannot get new memory from the standard
  operation system memory management. It makes sense for the user
  program to call this function if the programmer expects a marked
  change in the memory request patterns.
\end{quote}

\begin{verbatim}
void* SecureMalloc(int size)
void* SecureRealloc(void *ptr, int size)
char* SecureStrdup(char* source)
\end{verbatim}
\begin{quote}
  These functions are replacements for the standard library functions
  \texttt{malloc()}, \texttt{realloc()} and \texttt{strdup()}. These
  functions should be used for general memory requests. They are about
  as efficient as their standard counterparts (there is a \emph{very}
  small overhead), but they are integrated with the internal data
  structures of the memory management module.  The main difference to
  the traditional functions is that they will try to reorganize the
  internal memory free lists of the memory management module if a
  first request to get memory fails, and that they will terminate the
  program with an error message if a memory request cannot be
  fulfilled.
\end{quote}

\begin{verbatim}
MACRO FREE(void* junk)
\end{verbatim}
\begin{quote}
  This is a plug in for the \texttt{free()} function. Contrary to
  \texttt{free()}, it will assert that it is not passed a
  \texttt{NULL} pointer (the behaviour of \texttt{free()} in this case
  is undefined, usually it will just proceed silently). If CLIB is
  compiled to support memory debugging (see
  Sec.~\ref{sec:basics:memory:debug}), \texttt{FREE()} will also count
  deallocated blocks.
\end{quote}


\subsubsection{Debugging Memory Leaks}
\label{sec:basics:memory:debug}

\emph{Memory leaks} occur when unused data structures are not returned
to the memory management module (via calls to \texttt{free()}, or, in
our case, \texttt{SizeFree()} and \texttt{FREE()}). A similar class of
errors occurs if a single block of memory is deallocated more than
once. These errors are easy to make and hard to detect. Memory leaks,
in particular, will not usually be found by testing, as they do not
change the semantics of the program, but only lead to a steady
increase in used memory. Multiple freeing of memory, on the other
hand, can lead to segmentation faults and, even worse, to
unpredictable behaviour of the program.

The memory management module of CLIB offers some help in tracing
errors in memory handling by counting calls (and bytes allocated and
freed) to allocating and deallocating routines if compiled with
\texttt{CLB\_MEMORY\_DEBUG} defined. The function
\texttt{MemDebugPrintStats()} will print memory statistics.

\begin{verbatim}
void MemDebugPrintStats(FILE* out)
\end{verbatim}
\begin{quote}
  Print information about the number and size of memory chunks
  allocated and deallocated by the CLIB memory managment functions to
  the output channel described by \texttt{out} (usually
  \texttt{stdout} or \texttt{stderr}).
\end{quote}





\subsection{Dynamic Strings}
\label{sec:basics:strings}

The C programming language offers only rudimentary support for
strings. In particular, there is no simple way to deal with strings
whose lenght may change dynamically (termed \texttt{dynamic strings}
here). CLIB implements a dynamic string type with efficient
conversation to and from traditional C strings and the rudimentary
ability to share strings between independent data structures.


\subsubsection{Usage Information}

\begin{verbatim}
#include <clb_dstrings.h>

Requires: lib/BASICS.a
\end{verbatim}


\subsubsection{Allocation and Handling of Strings}

CLIB dynamic strings are implemted by the \texttt{DStrCell} data type
(with the corresponding \texttt{DStr\_p} pointer type). They consist
of a pointer to a memory block that is interpreted as a conventional,
\texttt{'$\backslash{}$0'}-terminated C string, information about the current
length of the string, the size of the currently allocated memory
block, and a reference counter. However, detailed knowledge about the
implementation is unneccessary for using the data type.

Strings are usually manipulated via pointers:

\begin{verbatim}
DStr_p DStrAlloc()
\end{verbatim}
\begin{quote}
  Create a dynamic string (with a single reference) and return the
  pointer to it. The string is initialized to the empty string "".
\end{quote}

\begin{verbatim}
void DStrFree(DStr_p junk)
\end{verbatim}
\begin{quote}
  Decrease the number of references to the given string by one. If
  there is no remaining reference, free the memory taken by the
  string.
\end{quote}

If you do not use references for sharing strings (via
\texttt{DStrGetRef()} and \texttt{DStrReleaseRef()}), you can ignore
the remarks about references. In this case, allocation and
deallocation defaults to the usual behavior.

The most common usage for dynamic strings is the accumulation of
several parts (most often read from an input file or user
interaction). The following set of functions allows easy appending of
the most common data objects to a dynamic string.

\begin{verbatim}
char* DStrAppendStr(DStr_p strdes, char* newpart)
\end{verbatim}
\begin{quote}
  Append a \texttt{'$\backslash{}$0'}-terminated C string to a dynamic
  string. Return the resulting string (as a C string).
\end{quote}

\begin{verbatim}
char* DStrAppendChar(DStr_p strdes, char newch)
\end{verbatim}
\begin{quote}
  Append a single character to a dynamic string. This is a special
  case of the above function that is handled separately because it is
  an extremely common operation during parsing of input and thus
  deserves a particularly efficient implementation.
\end{quote}

\begin{verbatim}
char* DStrAppendInt(DStr_p strdes, long newpart)
\end{verbatim}
\begin{quote}
  Append the print representation of a \texttt{long int} value to the
  dynamic string.
\end{quote}

\begin{verbatim}
MACRO char* DStrAppendDStr(DStr_p strdes, DStr_p str)
\end{verbatim}
\begin{quote}
  Append the dynamic string \texttt{str} to the dynamic string
  \texttt{strdes}.
\end{quote}

The following two functions allow the conversion of a dynamic CLIB
string to a conventional C string.

\begin{verbatim}
char* DStrView(DStr_p strdes)
\end{verbatim}
\begin{quote}
  Return a pointer to a \texttt{'$\backslash{}$0'} terminated string
  of the same value as the dynamic string. This operation is very
  efficient -- it returns only an existing pointer --, however, the
  resulting pointer is only guaranteed to be valid as long as no other
  operation is performed on the dynamic string.
\end{quote}

\begin{verbatim}
char* DStrCopy(DStr_p strdes)
\end{verbatim}
\begin{quote}
  Return a pointer to a newly created C string of the same value as
  the dynamic string. The pointer will be valid forever, and the
  caller is responsible for deallocating the memory pointed to via
  \texttt{FREE()}.
\end{quote}

You can also set the value of a string to specific values.

\begin{verbatim}
char* DStrSet(DStr_p strdes, char* string)
\end{verbatim}
\begin{quote}
  Set the dynamic string to the value of the C string provided.
\end{quote}

\begin{verbatim}
void DStrReset(DStr_p strdes)
\end{verbatim}
\begin{quote}
  Set the dynamic string to the empty string.
\end{quote}

The internal memory used by dynamic strings sometimes can be bigger
than the space actually taken up by the string. If you use a large
number od dynamic strings, it can be useful to reclaim this space.

\begin{verbatim}
void DStrMinimize(DStr_p strdes)
\end{verbatim}
\begin{quote}
  Reconfigure the dynamic string to use only the minimal space
  necessary to represent the string stored.
\end{quote}

Finally, as dynamic strings need to store their length for certain
operations anyways, there is a more efficient equivalent of
\texttt{strlen()} for them.

\begin{verbatim}
long DStrLen(DStr_p strdes)
\end{verbatim}
\begin{quote}
  Return the length (number of characters) in the dynamic string.
\end{quote}



\subsubsection{String Sharing}

CLIB dynamic strings can be shared between different data structures,
i.e. there can be more than one reference to a string. The dynamic
string functions administrate these references by simple
\emph{reference counting}, and will release the memory allocated for a
string only when no more references exist. 

Compared to many other implementation of shared strings, the CLIB
version is extremely rudimentary. In particular, all references have
the same access to the string, and all references can modify the
common value of the string.

\begin{verbatim}
MACRO DStr_p DStrGetRef(DStr_p strdes)
\end{verbatim}
\begin{quote}
  Obtain an additional reference to the dynamic string at
  \texttt{strdes}. This really only increases the reference counter in
  the string by one.
\end{quote}


\begin{verbatim}
MACRO DStr_p DStrReleaseRef(DStr_p strdes)
\end{verbatim}
\begin{quote}
  Delete a reference to \texttt{strdes}. Delete the dynamic string if
  the reference count reaches 0. This is actually only an alias for
  \texttt{DStrFree()}, which already takes care if the reference
  counter. It is, however, good style to use \texttt{DStrFree()} on
  pointers obtained by \texttt{DStrAlloc()} and to use
  \texttt{DStrReleaseRef()} on pointers obtained by
  \texttt{DStrGetRef()}.
\end{quote}


A typical application of this feature can be found in
\texttt{INOUT/cio\_scanner.c}, where this is used to associate the
file name of the current input stream with the currently processed
token. In general, it is impossible to decide a priori which of the
two references will survive longer. By using a shared string, both
refences have equal access to this string, and it is released when
both references to it are released.

\subsection{Tree-Based Data Structures}
\label{sec:basics:trees}


\subsection{Stacks}
\label{sec:basics:stacks}





%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "clib"
%%% End: 
