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