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