src/lslparse.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 ** lslparse.c
  26 **
  27 ** Module for calling LSL checker.
  28 **
  29 **  AUTHOR:
  30 **      Yang Meng Tan,
  31 **         Massachusetts Institute of Technology
  32 */
  33
  34 # include "splintMacros.nf"
  35 # include "basic.h"
  36 # include "osd.h"
  37
  38 # include "lslgrammar.h"
  39 # include "lslscan.h"
  40 # include "lslscanline.h"
  41 # include "lsltokentable.h"
  42 # include "lslparse.h"
  43
  44 /*@+ignorequals@*/
  45
  46 /*@dependent@*/ /*@null@*/ lslOp g_importedlslOp = NULL;
  47 bool g_lslParsingTraits = FALSE;
  48
  49 static void invokeLSL (cstring p_infile, cstring p_outfile, bool p_deletep);
  50
  51 int
  52 parseSignatures (cstring infile)
  53 {
  54   inputStream sourceFile;
  55   ltoken *id = (ltoken *) dmalloc (sizeof (*id));
  56   int status = 0;
  57
  58   /* parse traits */
  59   *id = LSLInsertToken (LST_SIMPLEID, lsymbol_fromString (infile), 0, FALSE);
  60   ltoken_setFileName (*id, infile);
  61   ltoken_setLine (*id, 0);
  62   ltoken_setCol (*id, 0);
  63
  64   sourceFile = inputStream_create (infile, cstring_undefined, FALSE);
  65
  66   if (!inputStream_getPath (context_getLarchPath (), sourceFile))
  67     {
  68       lclplainerror
  69         (message ("LSL signature parsing: can't find file %s containing trait",
  70                   inputStream_fileName (sourceFile)));
  71       status = 1;
  72
  73       sfree (id);
  74       inputStream_free (sourceFile);
  75       return status;
  76     }
  77
  78   if (!inputStream_open (sourceFile))
  79     {
  80       lclplainerror
  81         (cstring_makeLiteral ("LSL parsing: can't open file containing trait"));
  82       status = 2;
  83       sfree (id);
  84       inputStream_free (sourceFile);
  85
  86       return status;
  87     }
  88
  89   g_lslParsingTraits = TRUE;
  90   LSLScanReset (sourceFile);
  91   LSLReportEolTokens (FALSE);
  92
  93   status = lslparse ();
  94
  95   /* symtable_dump (symtab, stdout, TRUE); */
  96   g_lslParsingTraits = FALSE;
  97
  98   (void) inputStream_close (sourceFile);
  99   inputStream_free (sourceFile);
 100
 101   sfree (id);
 102
 103
 104   return status;
 105 }
 106
 107 /*@only@*/ lslOp
 108 parseOpLine (cstring fname, cstring line)
 109 {
 110   inputStream sourceFile;
 111   bool status;
 112
 113   sourceFile = inputStream_fromString (fname, line);
 114
 115   if (check (inputStream_open (sourceFile)))
 116     {
 117       LSLScanReset (sourceFile);
 118       LSLReportEolTokens (FALSE); /* 0 by default, lslParsingTraits = 0; */
 119
 120       /*
 121       ** lsl parsing and importing .lcs files are expected to be mutually
 122       ** exclusive.
 123       **
 124       ** lslparse sets importedlslOp
 125       */
 126
 127       status = (lslparse () != 0);
 128
 129       if (status)
 130         {
 131           lclplainfatalerror (message ("Error in parsing line: %s", line));
 132         }
 133
 134       (void) inputStream_close (sourceFile);
 135     }
 136
 137   inputStream_free (sourceFile);
 138
 139   llassert (g_importedlslOp != NULL);
 140   return (lslOp_copy (g_importedlslOp));
 141 }
 142
 143 lsymbol
 144 processTraitSortId (lsymbol sortid)
 145 {
 146   lsymbol out = lsymbol_sortFromType (g_symtab, sortid);
 147   if (out == sortid)
 148     { /* may be a new sort */
 149       (void) sort_fromLsymbol (sortid);
 150     }
 151   return out;
 152 }
 153
 154 /* formerly from check.c module */
 155
 156 static /*@only@*/ cstring
 157 printTypeName2 (typeNameNode n)
 158 {
 159   cstring s = cstring_undefined;
 160   sortNode sn;
 161   lsymbol lclSort;
 162   ltoken err;
 163
 164   if (n != (typeNameNode) 0)
 165     {
 166       if (n->isTypeName)
 167         {
 168           /* does not process opForm renaming, pass on to LSL
 169              and hope that it works for now. */
 170           typeNamePack p = n->typename;
 171
 172           llassert (p != NULL);
 173
 174           /* get the LCL type, assume LCL type has already been mentioned. */
 175           lclSort = lclTypeSpecNode2sort (p->type);
 176           lclSort = sort_getUnderlying (lclSort);
 177           /* lclsource = LCLSLScanSource (); */
 178           if (!sort_isValidSort (lclSort))
 179             {
 180               err = lclTypeSpecNode_errorToken (p->type);
 181               /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (err)); */
 182               lclerror (err, message ("Unrecognized type in uses: %q",
 183                                       typeNameNode_unparse (n)));
 184             }
 185           else
 186             {
 187               /*
 188               ** Below is necessary because this is one place where an LCL mutable
 189               ** type name is mapped directly into its value sort, not obj sort.
 190               ** Allows us to support only one qualifying "obj", rather
 191               ** than "val" as well.
 192               */
 193
 194               lclSort = typeExpr2ptrSort (lclSort, p->abst);
 195               lclSort = sort_makeVal (lclSort);
 196
 197               /*
 198               ** Check that lclSort is not a HOFSort ...
 199               ** Propagation of HOFSort should stop here.
 200               */
 201
 202               if (sort_isHOFSortKind (lclSort))
 203                 {
 204                   err = lclTypeSpecNode_errorToken (p->type);
 205
 206                   lclfatalerror
 207                     (err,
 208                      cstring_makeLiteral
 209                      ("LCL uses cannot handle higher-order types"));
 210                 }
 211               if (p->isObj)
 212                 lclSort = sort_makeObj (lclSort);
 213
 214               /*        if (!p->isObj) {
 215                         lclSort = sort_makeVal (lclSort);
 216                         } */
 217
 218               sn = sort_lookup (lclSort);
 219               s = cstring_copy (cstring_fromChars (lsymbol_toChars (sn->name)));
 220               /* s = string_paste (s, AbstDeclaratorNode_unparse (p->abst)); */
 221             }
 222         }
 223       else
 224         {
 225           /* s = OpFormNode_unparse (n->opform); */
 226           if (n->opform != 0)
 227             {
 228               lclfatalerror
 229                 (n->opform->tok,
 230                  cstring_makeLiteral ("Attempt to rename operator with uses: "
 231                                      "use LSL includes renaming facility"));
 232             }
 233           else
 234             {
 235               BADEXIT;
 236             }
 237         }
 238     }
 239   return s;
 240 }
 241
 242 static /*@only@*/ cstring
 243 replaceNode_unparseAlt (replaceNode x)
 244 {
 245   cstring s = cstring_undefined;
 246
 247   if (x != (replaceNode) 0)
 248     {
 249       s = printTypeName2 (x->typename);
 250       s = cstring_concatChars (s, " for ");
 251
 252       if (x->isCType)
 253         {
 254           s = cstring_concatFree1 (s, ltoken_unparse (x->content.ctype));
 255         }
 256       else
 257         {
 258           s = cstring_concatFree (s, nameNode_unparse (x->content.renamesortname.name));
 259           s = cstring_concatFree (s,
 260                                   sigNode_unparse (x->content.renamesortname.signature));
 261         }
 262     }
 263
 264   return s;
 265 }
 266
 267 static /*@only@*/ cstring
 268 replaceNodeList_unparseAlt (replaceNodeList x)
 269 {
 270   cstring s = cstring_undefined;
 271   bool first = TRUE;
 272
 273   replaceNodeList_elements (x, i)
 274     {
 275       if (first)
 276         {
 277           s = replaceNode_unparseAlt (i);
 278           first = FALSE;
 279         }
 280       else
 281         {
 282           s = message ("%q, %q", s, replaceNode_unparseAlt (i));
 283         }
 284     } end_replaceNodeList_elements;
 285
 286   return s;
 287 }
 288
 289 static /*@only@*/ cstring
 290 printNameList2 (typeNameNodeList x)
 291 {
 292   /* printing a list of typeNameNode's, not nameNode's */
 293   bool first = TRUE;
 294   cstring s = cstring_undefined;
 295
 296   typeNameNodeList_elements (x, i)
 297   {
 298     if (first)
 299       {
 300         s = printTypeName2 (i);
 301         first = FALSE;
 302       }
 303     else
 304       {
 305         s = message ("%q, %q", s, printTypeName2 (i));
 306       }
 307     } end_typeNameNodeList_elements;
 308
 309   return s;
 310 }
 311
 312 static /*@only@*/ cstring
 313 printRenamingNode2 (renamingNode x)
 314 {
 315   cstring s = cstring_undefined;
 316
 317   if (x != (renamingNode) 0)
 318     {
 319       if (x->is_replace)
 320         {
 321           replaceNodeList r = x->content.replace;
 322           s = replaceNodeList_unparseAlt (r);
 323         }
 324       else
 325         {
 326           nameAndReplaceNode n = x->content.name;
 327           bool printComma = TRUE;
 328           if (typeNameNodeList_size (n->namelist) == 0)
 329             {
 330               printComma = FALSE;
 331             }
 332           s = printNameList2 (n->namelist);
 333           if (printComma)
 334             if (replaceNodeList_isDefined (n->replacelist) &&
 335                 replaceNodeList_size (n->replacelist) != 0)
 336               {
 337                 s = cstring_appendChar (s, ',');
 338                 s = cstring_appendChar (s, ' ');
 339               }
 340           s = cstring_concatFree (s, replaceNodeList_unparseAlt (n->replacelist));
 341         }
 342     }
 343   return s;
 344 }
 345
 346 static /*@only@*/ cstring
 347 printTraitRefList2 (traitRefNodeList x) /*@*/
 348 {
 349   cstring s = cstring_undefined;
 350
 351   traitRefNodeList_elements (x, i)
 352   {
 353     s = message ("%qincludes (%q)", s, printRawLeaves2 (i->traitid));
 354
 355     if (i->rename != 0)
 356       {
 357         s = message ("%q(%q)", s, printRenamingNode2 (i->rename));
 358       }
 359
 360     s = message ("%q\n", s);
 361   } end_traitRefNodeList_elements;
 362
 363   return s;
 364 }
 365
 366 void
 367 callLSL (/*@unused@*/ cstring specfile, /*@only@*/ cstring text)
 368 {
 369   /* specfile is the name of the LCL file that contains "uses"
 370      Create an intermediate file named
 371      specfile_<TEMP_LSL_SUFFIX>.<TEMP_LSL_IN_SUFFIX>.
 372      put text in the file, run lsl on it and direct
 373      output to specfile_<TEMP_LSL_SUFFIX>.<TEMP_LSL_OUT_SUFFIX>.
 374      specfile can be a full pathname.
 375      Note: LSL does not support traitnames that are pathnames, only
 376      symbols.
 377      */
 378
 379   cstring infile;
 380   cstring outfile;
 381   cstring nopath;
 382   cstring noext;
 383   FILE *inptr;
 384
 385   infile = fileTable_fileName (fileTable_addTempFile (context_fileTable (), FILE_LSLTEMP, fileId_invalid));
 386   inptr = fileTable_createTempFile (context_fileTable (), infile, FALSE);
 387
 388   if (inptr == NULL)
 389     {
 390       /* fopen fails */
 391       llfatalerror (message ("Unable to write intermediate file: %s",
 392                              infile));
 393     }
 394
 395   nopath = fileLib_removePath (infile);
 396   noext = fileLib_removeAnyExtension (nopath);
 397
 398   fprintf (inptr, "%s : trait\n", cstring_toCharsSafe (noext));
 399
 400   cstring_free (noext);
 401   cstring_free (nopath);
 402
 403   fprintf (inptr, "%s", cstring_toCharsSafe (text));
 404   check (fileTable_closeFile (context_fileTable (), inptr));
 405
 406   /* the default is to delete the input file */
 407
 408   outfile = fileTable_fileName (fileTable_addTempFile (context_fileTable (), FILE_LSLTEMP, fileId_invalid));
 409   invokeLSL (infile, outfile, context_getFlag (FLG_KEEP));
 410   cstring_free (text);
 411 }
 412
 413 static void invokeLSL (cstring infile, cstring outfile, bool deletep)
 414 {
 415   /* run lsl on infile and leave result in outfile */
 416   FILE *outptr;
 417   filestatus status;
 418   int callstatus;
 419   cstring call;
 420   cstring returnPath = cstring_undefined;
 421
 422   /*
 423   ** Ensures that outfile can be written into, should find a better
 424   ** way to do this.
 425   */
 426
 427   outptr = fileTable_createTempFile (context_fileTable (), outfile, FALSE);
 428
 429   if (outptr == NULL)
 430     {
 431       /* fopen fails */
 432       llfatalerror (message ("Unable to write intermediate file: %s",
 433                              outfile));
 434     }
 435
 436   check (fileTable_closeFile (context_fileTable (), outptr));
 437
 438   /* set call to the right command */
 439   status = osd_getExePath (cstring_makeLiteralTemp (getenv ("PATH")),
 440                            cstring_makeLiteralTemp ("lsl"),
 441                            &returnPath);
 442
 443
 444   if (status == OSD_FILEFOUND)
 445     {
 446       call = message ("%s -syms %s > %s", returnPath, infile, outfile);
 447
 448       /* before calling, make sure old file is removed */
 449       (void) osd_unlink (outfile);
 450
 451       callstatus = osd_system (call);
 452
 453       cstring_free (call);
 454
 455       if (callstatus != CALL_SUCCESS)
 456         {
 457           /*
 458           ** lsl errors: call lsl again without -syms, sending output to stdout
 459           */
 460           cstring syscal = message ("%s %s", returnPath, infile);
 461           (void) osd_system (syscal);
 462           cstring_free (syscal);
 463
 464           llfatalerror (cstring_makeLiteral ("LSL trait used contains errors."));
 465         }
 466       else
 467         {                       /* ok, go ahead */
 468          /* Now parse the LSL output and store info in symbol table */
 469           callstatus = parseSignatures (cstring_copy (outfile));
 470
 471           if (callstatus == 0)
 472             {
 473               /* all went well */
 474               if (!context_getFlag (FLG_KEEP))
 475                 {
 476                   /* delete temporary files */
 477                   if (deletep)
 478                     {
 479                       (void) osd_unlink (infile);
 480                     }
 481
 482                   (void) osd_unlink (outfile);
 483                 }
 484             }
 485         }
 486     }
 487   else if (status == OSD_FILENOTFOUND)
 488     {
 489       llfatalerror
 490         (cstring_makeLiteral ("Cannot find LSL checker: check your command search path."));
 491     }
 492   else                          /* must be (status == OSD_PATHTOOLONG) */
 493     {
 494       lclfatalbug ("invokeLSL: lsl plus directory from search path is too long");
 495     }
 496 }
 497
 498 /* callLSL ("MySet", "includes Set (CC for C, EE for E)");  */
 499
 500 void
 501 readlsignatures (interfaceNode n)
 502 {
 503   /* assume n->kind = usesKIND */
 504   callLSL (g_currentSpec, printTraitRefList2 (n->content.uses));
 505 }