src/imports.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2003 University of Virginia,
   4 **         Massachusetts Institute of Technology
   5 **
   6 ** This program is free software; you can redistribute it and/or modify it
   7 ** under the terms of the GNU General Public License as published by the
   8 ** Free Software Foundation; either version 2 of the License, or (at your
   9 ** option) any later version.
  10 **
  11 ** This program is distributed in the hope that it will be useful, but
  12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
  13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  14 ** General Public License for more details.
  15 **
  16 ** The GNU General Public License is available from http://www.gnu.org/ or
  17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  18 ** MA 02111-1307, USA.
  19 **
  20 ** For information on splint: info@splint.org
  21 ** To report a bug: splint-bug@splint.org
  22 ** For more information: http://www.splint.org
  23 */
  24 /*
  25 ** imports.c
  26 **
  27 ** module for importing LCL specs.
  28 **
  29 **  AUTHOR:
  30 **      Yang Meng Tan,
  31 **         Massachusetts Institute of Technology
  32 */
  33
  34 # include "splintMacros.nf"
  35 # include "llbasic.h"
  36 # include "osd.h"
  37 # include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */
  38 # include "lclscan.h"
  39 # include "checking.h"
  40 # include "imports.h"
  41 # include "lslparse.h"
  42 # include "lh.h"
  43 # include "llmain.h"
  44 # include "portab.h"
  45
  46 void
  47 outputLCSFile (char *path, char *msg, char *specname)
  48 {
  49   static bool haserror = FALSE;
  50   char *sfile = mstring_concat (specname, ".lcs");
  51   char *outfile = mstring_concat (path, sfile);
  52   char *s;
  53   FILE *outfptr = fileTable_openWriteFile (context_fileTable (), cstring_fromChars (outfile));
  54   sfree (sfile);
  55
  56   DPRINTF (("Output lcl file: %s / %s / %s", path, specname, outfile));
  57
  58   /* check write permission */
  59
  60   if (outfptr == NULL)  /* Cannot open file */
  61     {
  62       if (!haserror)
  63         {
  64           lclplainerror (message ("Cannot write to output file: %s",
  65                                   cstring_fromChars (outfile)));
  66           haserror = TRUE;
  67         }
  68       sfree (outfile);
  69       return;
  70     }
  71
  72   fprintf (outfptr, "%s", msg);
  73   fprintf (outfptr, "%s\n", LCL_PARSE_VERSION);
  74
  75   /* output line %LCLimports foo bar ... */
  76   fprintf (outfptr, "%%LCLimports ");
  77
  78   lsymbolSet_elements (g_currentImports, sym)
  79     {
  80       s = lsymbol_toChars (sym);
  81
  82       if (s != NULL && !mstring_equal (s, specname))
  83         {
  84           fprintf (outfptr, "%s ", s);
  85         }
  86     } end_lsymbolSet_elements;
  87
  88   fprintf (outfptr, "\n");
  89
  90   sort_dump (outfptr, TRUE);
  91   symtable_dump (g_symtab, outfptr, TRUE);
  92
  93   check (fileTable_closeFile (context_fileTable (), outfptr));
  94   sfree (outfile);
  95 }
  96
  97 void
  98 importCTrait (void)
  99 {
 100   cstring infile = cstring_undefined;
 101   filestatus status = osd_findOnLarchPath (cstring_makeLiteralTemp (CTRAITSYMSNAME),
 102                                            &infile);
 103
 104   switch (status)
 105     {
 106     case OSD_FILEFOUND:
 107       /*
 108       ** This line was missing before version 2.3f.  Bug fix by Mike Smith.
 109       **    This looks like a bug - infile is already fully qualified path
 110       **    parseSignatures() adds another path to the front and fails to
 111       **    open the file.
 112       */
 113
 114       (void) parseSignatures (cstring_fromCharsNew (CTRAITSYMSNAME));
 115       (void) parseSignatures (infile);
 116       break;
 117     case OSD_FILENOTFOUND:
 118       /* try spec name */
 119       status = osd_findOnLarchPath (cstring_makeLiteralTemp (CTRAITSPECNAME),
 120                                     &infile);
 121
 122       if (status == OSD_FILEFOUND)
 123         {
 124           callLSL (cstring_makeLiteralTemp (CTRAITSPECNAME),
 125                    message ("includes %s (%s for String)",
 126                             cstring_fromChars (CTRAITFILENAMEN),
 127                             cstring_fromChars (sort_getName (g_sortCstring))));
 128           cstring_free (infile);
 129           break;
 130         }
 131       else
 132         {
 133           lldiagmsg
 134             (message ("Unable to find %s or %s.  Check LARCH_PATH environment variable.",
 135                       cstring_fromChars (CTRAITSYMSNAME),
 136                       cstring_fromChars (CTRAITSPECNAME)));
 137           cstring_free (infile);
 138           llexit (LLFAILURE);
 139         }
 140     case OSD_PATHTOOLONG:
 141       lclbug (message ("importCTrait: the concatenated directory and file "
 142                        "name are too long: %s: "
 143                        "continuing without it",
 144                        cstring_fromChars (CTRAITSPECNAME)));
 145       cstring_free (infile);
 146       break;
 147     }
 148 }
 149
 150 /*
 151 ** processImport --- load imports from file
 152 **
 153 **    impkind: IMPPLAIN  file on SPEC_PATH
 154 **                       # include "./file.h" if it exists,
 155 **                       # include "<directory where spec was found>/file.h" if not.
 156 **                         (warn if neither exists)
 157 **            IMPBRACKET file in default LCL imports directory
 158 **                       # include <file.h>
 159 **            IMPQUOTE   file directly
 160 **                       # include "file.h"
 161 */
 162
 163 void
 164 processImport (lsymbol importSymbol, ltoken tok, impkind kind)
 165 {
 166   bool readableP, oldexporting;
 167   bool compressedFormat = FALSE;
 168   inputStream imported, imported2, lclsource;
 169   char *bufptr;
 170   char *tmpbufptr;
 171   char *cptr;
 172   cstring name;
 173   lsymbol sym;
 174   char importName[MAX_NAME_LENGTH + 1];
 175   cstring importFileName;
 176   cstring path = cstring_undefined;
 177   cstring fpath, fpath2;
 178   mapping map;
 179   filestatus ret;
 180
 181   importFileName = lsymbol_toString (importSymbol);
 182   name = cstring_concat (importFileName, cstring_makeLiteralTemp (IO_SUFFIX));
 183
 184   /*
 185   ** find .lcs file
 186   */
 187
 188   switch (kind)
 189     {
 190     case IMPPLAIN:
 191       path = message ("%s%c%s", cstring_fromChars (g_localSpecPath), PATH_SEPARATOR,
 192                       context_getLarchPath ());
 193
 194       break;
 195     case IMPBRACKET:
 196       path = cstring_copy (context_getLCLImportDir ());
 197       break;
 198     case IMPQUOTE:
 199       path = cstring_fromCharsNew (g_localSpecPath);
 200       break;
 201     default:
 202       llbuglit ("bad imports case\n");
 203     }
 204
 205   if ((ret = osd_getPath (path, name, &fpath)) != OSD_FILEFOUND)
 206     {
 207       cstring fname2;
 208
 209       if (ret == OSD_PATHTOOLONG)
 210         {
 211           llfatalerrorLoc (cstring_makeLiteral ("Path too long"));
 212         }
 213
 214       imported2 = inputStream_create (cstring_copy (importFileName),
 215                                       LCL_EXTENSION, FALSE);
 216       fname2 = inputStream_fileName (imported2);
 217
 218       if (osd_getPath (path, fname2, &fpath2) == OSD_FILEFOUND)
 219         {
 220           llfatalerrorLoc
 221             (message ("Specs must be processed before it can be imported: %s",
 222                       fpath2));
 223         }
 224       else
 225         {
 226           if (kind == IMPPLAIN || kind == IMPQUOTE)
 227             {
 228               llfatalerrorLoc (message ("Cannot find file to import: %s", name));
 229             }
 230           else
 231             {
 232               llfatalerrorLoc (message ("Cannot find standard import file: %s", name));
 233             }
 234         }
 235     }
 236
 237
 238   imported = inputStream_create (fpath, cstring_makeLiteralTemp (IO_SUFFIX), FALSE);
 239
 240   readableP = inputStream_open (imported);
 241
 242   if (!readableP)
 243     {                   /* can't read ? */
 244       llfatalerrorLoc (message ("Cannot open import file for reading: %s",
 245                                 inputStream_fileName (imported)));
 246     }
 247
 248   bufptr = inputStream_nextLine (imported);
 249
 250   if (bufptr == 0)
 251     {
 252       llerror (FLG_SYNTAX, message ("Import file is empty: %s",
 253                                     inputStream_fileName (imported)));
 254       cstring_free (name);
 255       (void) inputStream_close (imported);
 256       inputStream_free (imported);
 257
 258       cstring_free (path);
 259       return;
 260     }
 261
 262   /* was it processed successfully ? */
 263   if (firstWord (bufptr, "%FAILED"))
 264     {
 265       llfatalerrorLoc
 266         (message ("Imported file was not checked successfully: %s.", name));
 267     }
 268
 269   /*
 270   ** Is it generated by the right version of the checker?
 271   **
 272   ** Uncompressed  .lcs files start with %PASSED
 273   ** Compressed files start with %LCS
 274   */
 275
 276   if (firstWord (bufptr, "%PASSED"))
 277     {
 278       /* %PASSED Output from LCP Version 2.* and 3.* */
 279       /*                     1234567890123*/
 280       /*                                 +*/
 281
 282       cptr = strstr (bufptr, "LCP Version");
 283
 284       if (cptr != NULL)
 285         {
 286           /*
 287           ** Only really old files start this way!
 288           */
 289
 290           cptr += 12;
 291           if (*cptr != '2' && *cptr != '3')
 292             {
 293               llfatalerrorLoc (message ("Imported file %s is obsolete: %s.",
 294                                         inputStream_fileName (imported),
 295                                         cstring_fromChars (bufptr)));
 296             }
 297         }
 298
 299       compressedFormat = FALSE;
 300     }
 301   else
 302     {
 303       if (!firstWord (bufptr, "%LCS"))
 304         {
 305           llfatalerrorLoc (message ("Imported file %s is not in correct format: %s",
 306                                     inputStream_fileName (imported),
 307                                     cstring_fromChars (bufptr)));
 308         }
 309
 310       compressedFormat = TRUE;
 311     }
 312
 313   /* push the imported LCL spec onto g_currentImports */
 314
 315   context_enterImport ();
 316
 317   bufptr = inputStream_nextLine (imported);
 318   llassert (bufptr != NULL);
 319
 320   tmpbufptr = bufptr;
 321
 322     /* expect %LCLimports foo bar ... */
 323   if (firstWord (bufptr, "%LCLimports "))
 324     {
 325       bufptr = bufptr + strlen ("%LCLimports ");
 326       while (sscanf (bufptr, "%s", importName) == 1)
 327         {
 328           bufptr = bufptr + strlen (importName) + 1;    /* 1 for space */
 329           sym = lsymbol_fromChars (importName);
 330           if (sym == importSymbol ||
 331               lsymbolSet_member (g_currentImports, sym))
 332             {
 333               /* ensure that the import list does not contain itself: an
 334                  invariant useful for checking imports cycles. */
 335               lclsource = LCLScanSource ();
 336               lclfatalerror (tok,
 337                              message ("Imports cycle: %s%s imports %s",
 338                                       importFileName,
 339                                       LCL_EXTENSION,
 340                                       cstring_fromChars (importName)));
 341             }
 342           /* push them onto g_currentImports */
 343           /* evs - 94 Apr 3:  I don't think it should do this! */
 344           /* (void) lsymbolSet_insert (g_currentImports, sym); */
 345         }
 346     }
 347   else
 348     {
 349       lclsource = LCLScanSource ();
 350       lclfatalerror (tok, message ("Unexpected line in imported file %s: %s",
 351                                    name,
 352                                    cstring_fromChars (bufptr)));
 353     }
 354
 355   /* read in the imported info */
 356   oldexporting = sort_setExporting (TRUE);
 357
 358   map = mapping_create ();
 359
 360   /* tok for error line numbering */
 361
 362   if (!compressedFormat)
 363     {
 364       sort_import (imported, tok, map);
 365     }
 366
 367   (void) sort_setExporting (oldexporting);
 368
 369   /* sort_import updates a mapping of old anonymous sorts to new
 370      anonymous sort that is needed in symtable_import */
 371   /* mapping_print (map); */
 372
 373   if (!compressedFormat)
 374     {
 375       symtable_import (imported, tok, map);
 376     }
 377   else
 378     {
 379       /* symtable_loadImport (imported, tok, map); */
 380     }
 381
 382   check (inputStream_close (imported));
 383   inputStream_free (imported);
 384
 385   mapping_free (map);
 386   cstring_free (name);
 387   cstring_free (path);
 388
 389   context_leaveImport ();
 390 }
 391
 392
 393