Logo Search packages:      
Sourcecode: maria version File versions

Compilation.C

Go to the documentation of this file.
// 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 */
00040 # 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 Mäkelä (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. */

00082 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)
{
}

00099 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
00110 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*
00133 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 */
00147 static const char typedefs[] = "mset.h";
/** type comparisons */
00149 static const char typecomp[] = "mset.c";
/** event decoding dispatcher */
00151 static const char events[] = "event.c";
/** state encoding and decoding */
00153 static const char states[] = "state.c";

/** Initialize the index numbers for data type definitions
 * @param net     the net to be initialized
 */
static void
00159 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
00174 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
00194 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
00223 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
00266 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
00528 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
00539 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
00584 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 */
00626 static const char props[] = "p.c";
/** property library */
00628 static const char prop_so[] = "p.so";

bool
00631 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 */
00724 #define DLRET (dlclose (myHandle), myHandle = 0)
/** check for an error message */
00726 #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
 */
00732 #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
 */
00742 #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
 */
00753 #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
 */
00763 #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*
00769 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
00865 Compilation::unlink ()
{
  if (myPropHandle) {
    dlclose (myPropHandle);
    myPropHandle = 0, myPropEval = 0;
  }
  if (myHandle) {
    msetClean ();
    eventClean ();
    stateClean ();
    dlclose (myHandle);
    myHandle = 0;
  }
}

Generated by  Doxygen 1.6.0   Back to index