// Compilation of types and expressions -*- c++ -*-

#include "snprintf.h"

#ifdef __GNUC__
# pragma implementation
# ifdef __sgi
#  define _POSIX_C_SOURCE 199309L
# endif
#endif // __GNUC__
#include "Compilation.h"
#include "Net.h"
#include "Place.h"
#include "Transition.h"
#include "Type.h"
#include "CExpression.h"
#include "Marking.h"
#include "BitBuffer.h"
#include "Property.h"
#include "util.h"
#include <stdio.h>
#include <stdlib.h>
#include <stdarg.h>
#include <dlfcn.h>
#include <sys/stat.h>
#include <sys/types.h>
#include <sys/wait.h>
#include <fcntl.h>
#include <unistd.h>

#include <sys/errno.h>
#include <signal.h>
#include <errno.h>

#if defined __APPLE__
/** External symbol */
# define E(s) "_" s
#else
/** External symbol */
# define E(s) s
#endif

#ifdef __OpenBSD__
# ifndef RTLD_NOW
#  define RTLD_NOW 0
# endif
#endif

/** Handle a child termination
 * @param pid		process number of the terminated child
 */
extern "C" void childterm (pid_t pid);
/** Handle a signal
 * @param num		number of the signal
 */
extern "C" void sig (int num);

/** @file Compilation.C
 * Interface to compiled code
 */

/* Copyright  2000-2003 Marko Mkel (msmakela@tcs.hut.fi).

   This file is part of MARIA, a reachability analyzer and model checker
   for high-level Petri nets.

   MARIA is free software; you can redistribute it and/or modify it
   under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   MARIA is distributed in the hope that it will be useful, but
   WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   General Public License for more details.

   The GNU General Public License is often shipped with GNU software, and
   is generally kept in a file called COPYING or LICENSE.  If you do not
   have a copy of the license, write to the Free Software Foundation,
   59 Temple Place, Suite 330, Boston, MA 02111 USA. */

Compilation::Compilation (const class Net& net,
			  const char* directory,
			  const char* prefix) :
  myNet (net), myDirectory (directory), myPrefix (prefix),
  myHandle (0),
  myMsetClean (0), myEventClean (0), myEventClear (0),
  myEventAnalyzers (0),
  myEventInflater (0), myEventDeflater (0), myEventDecoder (0),
  myStateClean (0), myStateProject (0), myStateDecoder (0),
  myFatal (0), myFlattened (0),
  myAddState (0), mySyncState (0), myAddArcs (0),
  myStateDeadlock (0), myWeaklyFair (0), myStronglyFair (0),
  myPropBits (0), myPropSucc (0),
  myPropHandle (0), myPropEval (0), myStateProps (0)
{
}

Compilation::~Compilation ()
{
  unlink ();
  delete[] myEventAnalyzers;
}

/** Ensure that a directory exists
 * @param directory	name of the directory
 * @return		true if the directory exists or could be created
 */
bool
dirExists (const char* directory)
{
  if (!mkdir (directory, 0777))
    return true;

  if (errno == EEXIST) {
    struct stat buf;
    if (!stat (directory, &buf) && S_ISDIR (buf.st_mode))
      return true;
    errno = ENOTDIR;
  }

  perror ("mkdir");
  return false;
}

/** Create a file name
 * @param directoryname	name of the directory
 * @param basefilename	(output) pointer to the full file name
 * @param maxnamelength	maximum number of characters in the file name part
 * @return		pointer to the file name part
 */
inline static char*
mkfilename (const char* directoryname,
	    char*& basefilename,
	    unsigned maxnamelength)
{
  size_t directorylength = strlen (directoryname);
  if (directoryname[directorylength - 1] != '/')
    directorylength++;
  basefilename = new char[directorylength + maxnamelength];
  memcpy (basefilename, directoryname, directorylength);
  basefilename[directorylength - 1] = '/';
  return basefilename + directorylength;
}

/** type definitions */
static const char typedefs[] = "mset.h";
/** type comparisons */
static const char typecomp[] = "mset.c";
/** event decoding dispatcher */
static const char events[] = "event.c";
/** state encoding and decoding */
static const char states[] = "state.c";

/** Initialize the index numbers for data type definitions
 * @param net	the net to be initialized
 */
static void
uncompileTypes (const class Net& net)
{
  for (unsigned i = net.getNumChildren (); i--; )
    uncompileTypes (net.getChild (i));
  for (Net::TypeList::const_iterator t = net.begin ();
       t != net.end (); t++)
    (*t)->uncompile ();
}

/** Generate code for data type definitions
 * @param net	the net for which to generate
 * @param out	the output buffer
 * @param file	the output file
 */
static void
generateTypes (const class Net& net,
	       class StringBuffer& out,
	       FILE* file)
{
  for (unsigned i = 0; i < net.getNumChildren (); i++)
    generateTypes (net.getChild (i), out, file);
  for (Net::TypeList::const_iterator t = net.begin ();
       t != net.end (); t++) {
    (*t)->compile (out);
    fwrite (out.getString (), 1, out.getLength (), file);
    out.create (0);
  }
}

/** Generate code for data item comparisons
 * @param net	the net for which to generate
 * @param out	the output buffer
 * @param file	the output file
 */
static void
generateComparisons (const class Net& net,
		     class StringBuffer& out,
		     FILE* file)
{
  for (unsigned i = 0; i < net.getNumChildren (); i++)
    generateComparisons (net.getChild (i), out, file);
  for (Net::TypeList::const_iterator t = net.begin ();
       t != net.end (); t++) {
    if ((*t)->isGenerated ())
      continue;
    out.append ("#define ID(id) id##");
    (*t)->appendIndex (out);
    out.append ("\n");
    (*t)->compileExtraDefinitions (out, 0, false);
    out.append ("#include\"bushfcn.h\"\n");
    fwrite (out.getString (), 1, out.getLength (), file);
    out.create (0);
  }
}

/** Generate code for synchronising transitions
 * @param net		the net for which to generate
 * @param basefilename	full path name to the generated files
 * @param filename	the changing part of the generated file names
 * @param decl		buffer for declarations
 * @param numcompiled	(in/out) number of transitions compiled
 * @return		true on success, false on failure
 */
static bool
generateSync (const class Net& net,
	      const char* basefilename,
	      char* filename,
	      class StringBuffer& decl,
	      unsigned& numcompiled)
{
  unsigned i;
  // transition files (synchronising transitions)
  for (i = net.getNumCallees (); i--; ) {
    /** the callee transition (synchronisation label) */
    const class Transition& t = net.getCallee (i);
    for (unsigned k = 0; k < t.getNumChildren (); k++) {
      class Transition& u = const_cast<class Transition&>(t.getChild (k));
      if (u.getLocalIndex () >= u.getNet ()->getNumCallees () ||
	  &u.getNet ()->getCallee (u.getLocalIndex ()) != &u) {
	// u is an ordinary transition that synchronises on t
	u.setRootIndex (numcompiled);
	snprintf (filename, 24, "t%u.c", numcompiled);
	if (FILE* file = fopen (basefilename, "w")) {
	  u.compile (decl);
	  fwrite (decl.getString (), 1, decl.getLength (), file);
	  decl.create (0);
	  fclose (file);
	}
	else
	  return false;
	numcompiled++;
      }
    }
  }
  for (i = net.getNumChildren (); i--; )
    if (!generateSync (net.getChild (i),
		       basefilename, filename, decl, numcompiled))
      return false;
  return true;
}

/** Generate code
 * @param net		the net for which to generate
 * @param directory	name of the directory containing the generated code
 * @return		true on success, false on failure
 */
inline static bool
generate (const class Net& net,
	  const char* directory)
{
  if (!dirExists (directory))
    return false;

  char* basefilename;
  char* filename = mkfilename (directory, basefilename, 24);
  /** output file */
  FILE* file;

  /** buffer for declarations */
  class StringBuffer decl;

  // type definitions
  memcpy (filename, typedefs, sizeof typedefs);
  if (!(file = fopen (basefilename, "w"))) {
  fopenError:
    perror ("fopen");
    delete[] basefilename;
    return false;
  }

  decl.append ("#include\"bush.h\"\n");
  uncompileTypes (net);
  generateTypes (net, decl, file);

  unsigned i;
  decl.append ("extern struct marking {\n");
  for (i = 0; i < net.getNumPlaces (); i++) {
    const class Place& place = *net.getPlace (i);
    decl.indent (2);
    if (place.getMaxNumTokens () == 1)
      place.getType ().appendName (decl);
    else
      place.getType ().appendMSetName (decl);
    decl.append ("* p");
    decl.append (i);
    decl.append (";\n");
  }
  decl.append ("} mSrc, mIn, mDest;\n"
	       "extern card_t numTokens[");
  decl.append (net.getNumPlaces ());
  decl.append ("];\n"
	       "void\n"
	       "initm (void);\n"
	       "void\n"
	       "freem (struct marking* m);\n"
	       "void\n"
	       "mset_clean (void);\n");
  net.compileConstantDecl (decl, "extern ");
  fwrite (decl.getString (), 1, decl.getLength (), file);
  decl.create (0);
  fclose (file);

  // type comparisons
  memcpy (filename, typecomp, sizeof typecomp);
  if (!(file = fopen (basefilename, "w")))
    goto fopenError;

  decl.append ("#include\"bushpriv.h\"\n");

  generateComparisons (net, decl, file);

  net.compileConstantDecl (decl, 0);
  for (i = 0; i < net.getNumAllTransitions (); i++) {
    decl.append ("void i");
    decl.append (i);
    decl.append (" (void);\n");
  }
  decl.append ("extern void\n"
	       "init (void)\n"
	       "{\n");
  net.compileConstantInit (decl);
  for (i = 0; i < net.getNumAllTransitions (); i++) {
    decl.append ("  i");
    decl.append (i);
    decl.append (" ();\n");
  }
  decl.append ("}\n");
  fwrite (decl.getString (), 1, decl.getLength (), file);
  decl.create (0);

  decl.append ("void\n"
	       "initm (void)\n"
	       "{\n"
	       "  freem (&mDest);\n");
  for (i = 0; i < net.getNumPlaces (); i++) {
    const class Type& type = net.getPlace (i)->getType ();
    if (net.getPlace (i)->getMaxNumTokens () == 1) {
      decl.append ("  if (mSrc.p");
      decl.append (i);
      decl.append (") *(mDest.p");
      decl.append (i);
      decl.append (" = malloc (sizeof (");
      type.appendName (decl);
      decl.append ("))) = *mSrc.p");
      decl.append (i);
      decl.append (";\n");
    }
    else {
      decl.append ("  mDest.p");
      decl.append (i);
      decl.append (" = copy");
      type.appendIndex (decl);
      decl.append (" (0, mSrc.p");
      decl.append (i);
      decl.append (");\n");
    }
  }
  decl.append ("}\n"
	       "void\n"
	       "freem (struct marking* m)\n"
	       "{\n");
  for (i = 0; i < net.getNumPlaces (); i++) {
    if (net.getPlace (i)->getMaxNumTokens () == 1) {
      decl.append ("  free (m->p");
      decl.append (i);
      decl.append ("), m->p");
      decl.append (i);
      decl.append (" = 0;\n");
    }
    else {
      decl.append ("  FREE (m->p");
      decl.append (i);
      decl.append (");\n");
    }
  }
  decl.append ("}\n"
	       "void\n"
	       "mset_clean (void)\n"
	       "{\n"
	       "  freem (&mSrc); freem (&mIn); freem (&mDest);\n"
	       "}\n");
  fwrite (decl.getString (), 1, decl.getLength (), file);
  decl.create (0);
  fclose (file);

  // event decoding dispatcher
  memcpy (filename, events, sizeof events);
  if (!(file = fopen (basefilename, "w")))
    goto fopenError;

  decl.append ("#include\"Error.h\"\n"
	       "#include\"eventpriv.h\"\n"
	       "unsigned wfair[");
  decl.append (1 + net.getNumWeaklyFair ());
  decl.append ("], sfair[");
  decl.append (1 + net.getNumStronglyFair ());
  decl.append ("];\n");
  for (i = 0; i < net.getNumAllTransitions (); i++) {
    decl.append ("enum Error d");
    decl.append (i);
    decl.append (" (unsigned sf);\n");
  }
  decl.append ("extern enum Error\n"
	       "event_decode (unsigned sf)\n"
	       "{\n");
  switch (net.getNumAllTransitions ()) {
  case 1:
    decl.append ("  return d0 (sf);\n");
    break;
  case 0:
    decl.append ("  return errNone;\n");
    break;
  default:
    decl.append ("  unsigned tr = FCN (dec) (");
    decl.append (log2 (net.getNumAllTransitions ()));
    decl.append (");\n"
		 "  switch (tr) {\n");
    for (i = 0; i < net.getNumAllTransitions (); i++) {
      decl.append ("  case ");
      decl.append (i);
      decl.append (": return d");
      decl.append (i);
      decl.append (" (sf);\n");
    }
    decl.append ("  }\n"
		 "  return errFatal;\n");
  }
  decl.append ("}\n");
  fwrite (decl.getString (), 1, decl.getLength (), file);
  decl.create (0);
  fclose (file);

  // state encoding and decoding
  memcpy (filename, states, sizeof states);
  if (!(file = fopen (basefilename, "w")))
    goto fopenError;

  class CExpression cexpr (decl, net, 0);
  decl.append ("#include\"statefcn.h\"\n"
	       "card_t numTokens[");
  decl.append (net.getNumPlaces ());
  decl.append ("];\n");
  cexpr.setMultiset ("mSrc");
  net.compileDeadlock (cexpr);
  decl.append ("extern enum Error\n"
	       "deadlock (unsigned net)\n"
	       "{\n");
  cexpr.generate ();
  cexpr.setMultiset ("mDest");
  net.compileReject (cexpr);
  decl.append ("}\n"
	       "static enum Error\n"
	       "reject (unsigned net)\n"
	       "{\n");
  cexpr.generate ();
  net.compileProps (cexpr, "op", "data");
  decl.append ("}\n"
	       "extern int\n"
	       "stateprop (int (*op) (unsigned, void*), void* data)\n"
	       "{\n");
  cexpr.generate ();
  net.compileEncoder (cexpr);
  decl.append ("}\n"
	       "enum Error\n"
	       "encode (unsigned net, unsigned tr, unsigned ftr,"
	       " int hide, void* ctx)\n"
	       "{\n");
  cexpr.generate ();
  cexpr.setMultiset ("mSrc");
  net.compileDecoder (cexpr);
  decl.append ("}\n"
	       "extern void\n"
	       "decode (unsigned net, void* buf, unsigned size)\n"
	       "{\n");
  cexpr.generate ();
  net.compileProjection (cexpr);
  decl.append ("}\n"
	       "extern const void*\n"
	       "project (unsigned net, unsigned d, unsigned dbits,"
	       " unsigned* size)\n"
	       "{\n");
  cexpr.generate ();
  decl.append ("}\n");

  fwrite (decl.getString (), 1, decl.getLength (), file);
  decl.create (0);
  fclose (file);

  // transition files (original and fused transitions in root net)
  assert (!net.getIndex ());
  for (i = 0; i < net.getNumAllTransitions (); i++) {
    snprintf (filename, 24, "t%u.c", i);
    if (!(file = fopen (basefilename, "w")))
      goto fopenError;
    net.getTransition (i).compile (decl);
    fwrite (decl.getString (), 1, decl.getLength (), file);
    decl.create (0);
    fclose (file);
  }
  unsigned numcompiled = i;
  if (!generateSync (net, basefilename, filename, decl, numcompiled))
    goto fopenError;
  net.setNumCompiled (numcompiled);

  delete[] basefilename;
  return true;
}

bool
Compilation::compile () const
{
  return ::generate (myNet, myDirectory);
}

/** Execute an external program
 * @param progname	name of the program
 * @param argv		arguments of the program
 * @return		true if everything succeeded
 */
inline static bool
execute (const char* progname,
	 char*const* argv)
{
  signal (SIGCHLD, SIG_DFL);
  if (pid_t pid = fork ()) {
    if (pid < 0)
      perror ("fork");
    else {
      for (;;) {
	int status = 0;
	pid_t child = wait (&status);
	if (child == pid) {
	  if (!status) {
	    signal (SIGCHLD, sig);
	    return true;
	  }
	  fprintf (stderr, "%s returned %d\n", progname, status);
	  break;
	}
	else if (child < 0) {
	  perror ("wait");
	  break;
	}
	else
	  childterm (pid);
      }
    }
  }
  else {
    execvp (progname, argv);
    perror (progname);
    exit (127);
  }
  signal (SIGCHLD, sig);
  return false;
}

/** Compile the files
 * @param prefix	prefix for invoking the compiler
 * @param directory	name of the directory containing the generated code
 * @param object	name of the object file
 * @param numTrans	number of transition files
 * @param ...		names of modules to compile, terminated by NULL
 */
inline static bool
compile (const char* prefix,
	 const char* directory,
	 const char* object,
	 unsigned numTrans,
	 ...)
{
  size_t prefixlength = strlen (prefix);
  char* progname = new char[prefixlength + 5];
  if (!progname) return false;
  memcpy (progname, prefix, prefixlength);
  memcpy (progname + prefixlength, "-cso", 5);
  char** argv = new char*[numTrans + 7];
  if (!argv) return false;
  argv[0] = progname;
  argv[1] = newString (directory);
  argv[2] = newString (object);
  /** number of extra modules */
  unsigned numModules = 0;
  /** the extra modules */
  va_list modules;
  va_start (modules, numTrans);
  while (const char* mod = va_arg (modules, const char*))
    argv[3 + numModules++] = newString (mod);
  va_end (modules);
  argv[3 + numTrans + numModules] = 0;
  char tname[24];
  unsigned i;
  bool status = false;
  for (i = 0; i < numTrans; i++) {
    snprintf (tname, sizeof tname, "t%u.c", i);
    if (!(argv[3 + numModules + i] = newString (tname)))
      goto cleanup;
  }

  status = execute (progname, argv);
 cleanup:
  for (i += 3 + numModules; i--; ) delete[] argv[i];
  delete[] argv;
  return status;
}

/** property automaton */
static const char props[] = "p.c";
/** property library */
static const char prop_so[] = "p.so";

bool
Compilation::compile (const class Property& property)
{
  *myPropBits = property.isFinite () ? log2 (property.getNumStates ()) : 0;

  /** a state of the property automaton */
  unsigned state;
  /** file name including the directory name */
  char* basefilename;
  /** file name excluding the directory name */
  char* filename = mkfilename (myDirectory, basefilename, sizeof prop_so);
  memcpy (filename, props, sizeof props);

  if (FILE* file = fopen (basefilename, "w")) {
    /** buffer for declarations */
    class StringBuffer decl;
    /** the compilation */
    class CExpression cexpr (decl, myNet, 0);
    /** accepting state of the property automaton */
    const unsigned final = property.getFinalState ();
    cexpr.setMultiset ("mSrc");
    decl.append ("#include \"mset.h\"\n"
		 "#define ERROR(err) return err\n"
		 "unsigned succ[");
    decl.append (1 + property.getNumStates ());
    decl.append ("];\n");
    for (state = 0; state < property.getNumStates (); state++) {
      property[state].compileGates (cexpr, 2, "succ", final);
      decl.append ("static enum Error\nprop"), decl.append (state);
      decl.append (" (void)\n{\n");
      cexpr.generate ();
      decl.append ("}\n");
      fwrite (decl.getString (), 1, decl.getLength (), file);
      decl.create (0);
    }
    fputs ("enum Error (*prop[]) (void) = {", file);
    /** line wrap thresold */
    const unsigned wrap = 75;
    /** column counter */
    register unsigned column = wrap;
    for (state = 0; state < property.getNumStates (); state++) {
      if (column >= wrap)
	column = fprintf (file, "\n  prop%u,", state) - 1;
      else
	column += fprintf (file, " prop%u,", state);
    }
    fputs ("\n};\n", file);
    fclose (file);

    memcpy (filename, prop_so, sizeof prop_so);
    if (::compile (myPrefix, myDirectory, basefilename, 0, props, 0)) {
      if (myPropHandle)
	dlclose (myPropHandle);
      myPropHandle = dlopen (basefilename, RTLD_NOW);
      delete[] basefilename;
      const char* err = dlerror ();
      if (err)
	fputs (err, stderr), putc ('\n', stderr);
      else if (!myPropHandle)
	fputs ("could not open shared library\n", stderr);
      else {
	const unsigned* succ =
	  reinterpret_cast<const unsigned*>(dlsym (myPropHandle, E ("succ")));
	if ((err = dlerror ())) {
	  fputs (err, stderr), putc ('\n', stderr);
	  return false;
	}
	else if (!succ) {
	  fputs ("could not bind symbol `succ'\n", stderr);
	  return false;
	}
	myPropEval =
	  reinterpret_cast<eval_t*>(dlsym (myPropHandle, E ("prop")));
	if ((err = dlerror ())) {
	  fputs (err, stderr), putc ('\n', stderr);
	  return false;
	}
	else if (!myPropEval) {
	  fputs ("could not bind symbol `prop'\n", stderr);
	  return false;
	}
	*myPropSucc = succ;
	return true;
      }
      return false;
    }
  }
  else
    perror ("fopen");
  delete[] basefilename;
  return false;
}

/** close the shared library at exit */
#define DLRET (dlclose (myHandle), myHandle = 0)
/** check for an error message */
#define DLERR if ((er0 = dlerror ())) return err = newString (er0), DLRET, err
/** Bind a symbol of the specified type from a shared object
 * @param sym_t		type of the symbol to be bound
 * @param sym		name of the symbol to be bound
 * @param var		name of the variable to be bound
 */
#define DLBIND(sym_t, sym, var)						\
  var = *reinterpret_cast<sym_t*>(&(f = dlsym (myHandle, E (#sym))));	\
  DLERR;								\
  if (!var) return DLRET, newString ("cannot bind symbol " E (#sym))

/** Bind a symbol of the specified type from a shared object to a table
 * @param sym_t		type of the symbol to be bound
 * @param symfmt	format string for the symbol name
 * @param var		name of the table
 */
#define DLBINDT(sym_t, symfmt, var)					\
    snprintf (snam, sizeof snam, E (symfmt), i);			\
    var[i] = *reinterpret_cast<sym_t*>(&(f = dlsym (myHandle, snam)));	\
    DLERR;								\
    if (!var) return DLRET, newString ("cannot bind symbol " symfmt)

/** Bind a symbol of the specified type backwards to a shared object
 * @param sym_t		type of the symbol to be bound
 * @param sym		name of the symbol to be bound
 * @param var		name of the variable to be bound
 */
#define DLBINDB(sym_t, sym, var)					\
  f = dlsym (myHandle, E (#sym)); DLERR;				\
  if (!f) return DLRET, newString ("cannot bind symbol " E (#sym));	\
  *reinterpret_cast<sym_t*>(f) = var

/** Bind a symbol of the specified type to a pointer in the shared object
 * @param sym_t		type of the symbol to be bound
 * @param sym		name of the symbol to be bound
 * @param var		name of the variable to be bound
 */
#define DLBINDP(sym_t, sym, var)					\
  f = dlsym (myHandle, E (#sym)); DLERR;				\
  if (!f) return DLRET, newString ("cannot bind symbol " E (#sym));	\
  var = reinterpret_cast<sym_t*>(f)

char*
Compilation::link ()
{
  unlink ();
  {
    size_t directorylength = strlen (myDirectory);
    char* so_name = new char[directorylength + 6];
    memcpy (so_name, myDirectory, directorylength);
    memcpy (so_name + directorylength, "/a.so", 6);

    if (::compile (myPrefix, myDirectory, so_name,
		   myNet.getNumCompiled (),
		   events, states, typecomp, 0))
      myHandle = dlopen (so_name,
			 RTLD_NOW
#ifdef RTLD_GLOBAL
			 | RTLD_GLOBAL
#endif // RTLD_GLOBAL
			 );
    else {
      delete[] so_name;
      return newString ("could not create shared library");
    }
    delete[] so_name;
  }

  /** error message */
  const char* er0;
  /** copied error message */
  char* err;

  if ((er0 = dlerror ())) {
    if (myHandle) dlclose (myHandle), myHandle = 0;
    return err = newString (er0);
  }
  if (!myHandle)
    return newString ("could not open shared library");

  /** auxiliary variable for type conversions */
  void* f;

  DLBIND (vf_t, mset_clean, myMsetClean);
  DLBIND (vf_t, event_cleanup, myEventClean);
  DLBIND (vf_t, event_clear, myEventClear);
  DLBIND (inf_t, inflate, myEventInflater);
  DLBIND (def_t, deflate, myEventDeflater);
  DLBIND (fair_t, event_decode, myEventDecoder);
  DLBIND (vf_t, cleanup, myStateClean);
  DLBIND (sproj_t, project, myStateProject);
  DLBIND (sdec_t, decode, myStateDecoder);
  DLBIND (deval_t, deadlock, myStateDeadlock);
  DLBIND (prop_t, stateprop, myStateProps);

  myWeaklyFair = reinterpret_cast<unsigned*>(dlsym (myHandle, E ("wfair")));
  DLERR;
  if (!myWeaklyFair)
    return DLRET, newString ("cannot bind symbol " E ("wfair"));
  myStronglyFair = reinterpret_cast<unsigned*>(dlsym (myHandle, E ("sfair")));
  DLERR;
  if (!myStronglyFair)
    return DLRET, newString ("cannot bind symbol " E ("sfair"));
  myPropBits = reinterpret_cast<unsigned*>(dlsym (myHandle, E ("propBits")));
  DLERR;
  if (!myPropBits)
    return DLRET, newString ("cannot bind symbol " E ("propBits"));
  myPropSucc =
    reinterpret_cast<const unsigned**>(dlsym (myHandle, E ("propSucc")));
  DLERR;
  if (!myPropSucc)
    return DLRET, newString ("cannot bind symbol " E ("propSucc"));

  unsigned i = myNet.getNumCompiled ();
  delete[] myEventAnalyzers;
  myEventAnalyzers = new uf_t[i];
  for (unsigned i = myNet.getNumCompiled (); i--; ) {
    char snam[23];
    DLBINDT (uf_t, "a%u", myEventAnalyzers);
  }

  *myPropBits = 0;

  extern volatile bool interrupted;
  DLBINDB (volatile bool*, intr, &interrupted);
  DLBINDP (bool*, fatal, myFatal);
  DLBINDP (bool, flattened, myFlattened);
  DLBINDP (sadd_t, addstate, myAddState);
  DLBINDP (ssync_t, syncstate, mySyncState);
  DLBINDP (char, arcs, myAddArcs);

  vf_t init;
  DLBIND (vf_t, init, init);
  (*init) ();

  return 0;
}

void
Compilation::unlink ()
{
  if (myPropHandle) {
    dlclose (myPropHandle);
    myPropHandle = 0, myPropEval = 0;
  }
  if (myHandle) {
    msetClean ();
    eventClean ();
    stateClean ();
    dlclose (myHandle);
    myHandle = 0;
  }
}