isl_input_omega.c

   1 #include <ctype.h>
   2 #include <string.h>
   3 #include <strings.h>
   4 #include "isl_input_omega.h"
   5
   6 enum token_type { TOKEN_UNKNOWN = 256, TOKEN_VALUE, TOKEN_IDENT, TOKEN_GE,
   7                   TOKEN_LE, TOKEN_TO, TOKEN_AND, TOKEN_EXISTS };
   8
   9 struct token {
  10         enum token_type  type;
  11
  12         unsigned int on_new_line : 1;
  13         int line;
  14         int col;
  15
  16         union {
  17                 isl_int v;
  18                 char    *s;
  19         } u;
  20 };
  21
  22 static struct token *token_new(struct isl_ctx *ctx,
  23         int line, int col, unsigned on_new_line)
  24 {
  25         struct token *tok = isl_alloc_type(ctx, struct token);
  26         if (!tok)
  27                 return NULL;
  28         tok->line = line;
  29         tok->col = col;
  30         tok->on_new_line = on_new_line;
  31         return tok;
  32 }
  33
  34 void token_free(struct token *tok)
  35 {
  36         if (!tok)
  37                 return;
  38         if (tok->type == TOKEN_VALUE)
  39                 isl_int_clear(tok->u.v);
  40         else if (tok->type == TOKEN_IDENT)
  41                 free(tok->u.s);
  42         free(tok);
  43 }
  44
  45 struct stream {
  46         struct isl_ctx  *ctx;
  47         FILE            *file;
  48         const char      *str;
  49         int             line;
  50         int             col;
  51         int             eof;
  52
  53         char            *buffer;
  54         size_t          size;
  55         size_t          len;
  56         int             c;
  57
  58         struct token    *tokens[5];
  59         int             n_token;
  60 };
  61
  62 void stream_error(struct stream *s, struct token *tok, char *msg)
  63 {
  64         int line = tok ? tok->line : s->line;
  65         int col = tok ? tok->col : s->col;
  66         fprintf(stderr, "syntax error (%d, %d): %s\n", line, col, msg);
  67         if (tok) {
  68                 if (tok->type < 256)
  69                         fprintf(stderr, "got '%c'\n", tok->type);
  70                 else
  71                         fprintf(stderr, "got token type %d\n", tok->type);
  72         }
  73 }
  74
  75 static void stream_free(struct stream *s);
  76
  77 static struct stream* stream_new(struct isl_ctx *ctx)
  78 {
  79         int i;
  80         struct stream *s = isl_alloc_type(ctx, struct stream);
  81         if (!s)
  82                 return NULL;
  83         s->ctx = ctx;
  84         s->size = 256;
  85         s->file = NULL;
  86         s->str = NULL;
  87         s->buffer = isl_alloc_array(ctx, char, s->size);
  88         if (!s->buffer)
  89                 goto error;
  90         s->len = 0;
  91         s->line = 1;
  92         s->col = 0;
  93         s->eof = 0;
  94         s->c = -1;
  95         for (i = 0; i < 5; ++i)
  96                 s->tokens[i] = NULL;
  97         s->n_token = 0;
  98         return s;
  99 error:
 100         stream_free(s);
 101         return NULL;
 102 }
 103
 104 static struct stream* stream_new_file(struct isl_ctx *ctx, FILE *file)
 105 {
 106         struct stream *s = stream_new(ctx);
 107         if (!s)
 108                 return NULL;
 109         s->file = file;
 110         return s;
 111 }
 112
 113 static int stream_getc(struct stream *s)
 114 {
 115         int c;
 116         if (s->eof)
 117                 return -1;
 118         if (s->file)
 119                 c = fgetc(s->file);
 120         else {
 121                 c = *s->str++;
 122                 if (c == '\0')
 123                         c = -1;
 124         }
 125         if (c == -1)
 126                 s->eof = 1;
 127         if (!s->eof) {
 128                 if (s->c == '\n') {
 129                         s->line++;
 130                         s->col = 0;
 131                 } else
 132                         s->col++;
 133         }
 134         s->c = c;
 135         return c;
 136 }
 137
 138 static void stream_ungetc(struct stream *s, int c)
 139 {
 140         if (s->file)
 141                 ungetc(c, s->file);
 142         else
 143                 --s->str;
 144         s->c = -1;
 145 }
 146
 147 static int stream_push_char(struct stream *s, int c)
 148 {
 149         if (s->len >= s->size) {
 150                 s->size = (3*s->size)/2;
 151                 s->buffer = isl_realloc_array(ctx, s->buffer, char, s->size);
 152                 if (!s->buffer)
 153                         return -1;
 154         }
 155         s->buffer[s->len++] = c;
 156         return 0;
 157 }
 158
 159 static void stream_push_token(struct stream *s, struct token *tok)
 160 {
 161         isl_assert(s->ctx, s->n_token < 5, return);
 162         s->tokens[s->n_token++] = tok;
 163 }
 164
 165 static struct token *stream_next_token(struct stream *s)
 166 {
 167         int c;
 168         struct token *tok = NULL;
 169         int line, col;
 170         int old_line = s->line;
 171
 172         if (s->n_token)
 173                 return s->tokens[--s->n_token];
 174
 175         s->len = 0;
 176
 177         /* skip spaces */
 178         while ((c = stream_getc(s)) != -1 && isspace(c))
 179                 /* nothing */
 180                 ;
 181
 182         line = s->line;
 183         col = s->col;
 184
 185         if (c == -1)
 186                 return NULL;
 187         if (c == '(' ||
 188             c == ')' ||
 189             c == '+' ||
 190             c == '/' ||
 191             c == '*' ||
 192             c == '^' ||
 193             c == '=' ||
 194             c == ',' ||
 195             c == ':' ||
 196             c == '[' ||
 197             c == ']' ||
 198             c == '{' ||
 199             c == '}') {
 200                 tok = token_new(s->ctx, line, col, old_line != line);
 201                 if (!tok)
 202                         return NULL;
 203                 tok->type = (enum token_type)c;
 204                 return tok;
 205         }
 206         if (c == '-') {
 207                 int c;
 208                 if ((c = stream_getc(s)) == '>') {
 209                         tok = token_new(s->ctx, line, col, old_line != line);
 210                         if (!tok)
 211                                 return NULL;
 212                         tok->type = TOKEN_TO;
 213                         return tok;
 214                 }
 215                 if (c != -1)
 216                         stream_ungetc(s, c);
 217         }
 218         if (c == '-' || isdigit(c)) {
 219                 tok = token_new(s->ctx, line, col, old_line != line);
 220                 if (!tok)
 221                         return NULL;
 222                 tok->type = TOKEN_VALUE;
 223                 isl_int_init(tok->u.v);
 224                 if (stream_push_char(s, c))
 225                         goto error;
 226                 while ((c = stream_getc(s)) != -1 && isdigit(c))
 227                         if (stream_push_char(s, c))
 228                                 goto error;
 229                 if (c != -1)
 230                         stream_ungetc(s, c);
 231                 if (s->len == 1 && s->buffer[0] == '-')
 232                         isl_int_set_si(tok->u.v, -1);
 233                 else {
 234                         stream_push_char(s, '\0');
 235                         isl_int_read(tok->u.v, s->buffer);
 236                 }
 237                 return tok;
 238         }
 239         if (isalpha(c)) {
 240                 tok = token_new(s->ctx, line, col, old_line != line);
 241                 if (!tok)
 242                         return NULL;
 243                 stream_push_char(s, c);
 244                 while ((c = stream_getc(s)) != -1 && isalnum(c))
 245                         stream_push_char(s, c);
 246                 if (c != -1)
 247                         stream_ungetc(s, c);
 248                 stream_push_char(s, '\0');
 249                 if (!strcasecmp(s->buffer, "exists"))
 250                         tok->type = TOKEN_EXISTS;
 251                 else {
 252                         tok->type = TOKEN_IDENT;
 253                         tok->u.s = strdup(s->buffer);
 254                 }
 255                 return tok;
 256         }
 257         if (c == '>') {
 258                 int c;
 259                 if ((c = stream_getc(s)) == '=') {
 260                         tok = token_new(s->ctx, line, col, old_line != line);
 261                         if (!tok)
 262                                 return NULL;
 263                         tok->type = TOKEN_GE;
 264                         return tok;
 265                 }
 266                 if (c != -1)
 267                         stream_ungetc(s, c);
 268         }
 269         if (c == '<') {
 270                 int c;
 271                 if ((c = stream_getc(s)) == '=') {
 272                         tok = token_new(s->ctx, line, col, old_line != line);
 273                         if (!tok)
 274                                 return NULL;
 275                         tok->type = TOKEN_LE;
 276                         return tok;
 277                 }
 278                 if (c != -1)
 279                         stream_ungetc(s, c);
 280         }
 281         if (c == '&') {
 282                 tok = token_new(s->ctx, line, col, old_line != line);
 283                 if (!tok)
 284                         return NULL;
 285                 tok->type = TOKEN_AND;
 286                 if ((c = stream_getc(s)) != '&' && c != -1)
 287                         stream_ungetc(s, c);
 288                 return tok;
 289         }
 290
 291         tok = token_new(s->ctx, line, col, old_line != line);
 292         if (!tok)
 293                 return NULL;
 294         tok->type = TOKEN_UNKNOWN;
 295         return tok;
 296 error:
 297         token_free(tok);
 298         return NULL;
 299 }
 300
 301 static int stream_eat(struct stream *s, int type)
 302 {
 303         struct token *tok;
 304
 305         tok = stream_next_token(s);
 306         if (!tok)
 307                 return -1;
 308         if (tok->type == type) {
 309                 token_free(tok);
 310                 return 0;
 311         }
 312         stream_error(s, tok, "expecting other token");
 313         stream_push_token(s, tok);
 314         return -1;
 315 }
 316
 317 static void stream_free(struct stream *s)
 318 {
 319         if (!s)
 320                 return;
 321         free(s->buffer);
 322         if (s->n_token != 0) {
 323                 struct token *tok = stream_next_token(s);
 324                 stream_error(s, tok, "unexpected token");
 325                 token_free(tok);
 326         }
 327         free(s);
 328 }
 329
 330 struct variable {
 331         char                    *name;
 332         int                      pos;
 333         struct variable         *next;
 334 };
 335
 336 struct vars {
 337         struct isl_ctx  *ctx;
 338         int              n;
 339         struct variable *v;
 340 };
 341
 342 static struct vars *vars_new(struct isl_ctx *ctx)
 343 {
 344         struct vars *v;
 345         v = isl_alloc_type(ctx, struct vars);
 346         if (!v)
 347                 return NULL;
 348         v->ctx = ctx;
 349         v->n = 0;
 350         v->v = NULL;
 351         return v;
 352 }
 353
 354 void variable_free(struct variable *var)
 355 {
 356         while (var) {
 357                 struct variable *next = var->next;
 358                 free(var->name);
 359                 free(var);
 360                 var = next;
 361         }
 362 }
 363
 364 static void vars_free(struct vars *v)
 365 {
 366         if (!v)
 367                 return;
 368         variable_free(v->v);
 369         free(v);
 370 }
 371
 372 struct variable *variable_new(struct vars *v, const char *name, int len,
 373                                 int pos)
 374 {
 375         struct variable *var;
 376         var = isl_alloc_type(v->ctx, struct variable);
 377         if (!var)
 378                 goto error;
 379         var->name = strdup(name);
 380         var->name[len] = '\0';
 381         var->pos = pos;
 382         var->next = v->v;
 383         return var;
 384 error:
 385         variable_free(v->v);
 386         return NULL;
 387 }
 388
 389 static int vars_pos(struct vars *v, const char *s, int len)
 390 {
 391         int pos;
 392         struct variable *q;
 393
 394         if (len == -1)
 395                 len = strlen(s);
 396         for (q = v->v; q; q = q->next) {
 397                 if (strncmp(q->name, s, len) == 0 && q->name[len] == '\0')
 398                         break;
 399         }
 400         if (q)
 401                 pos = q->pos;
 402         else {
 403                 pos = v->n;
 404                 v->v = variable_new(v, s, len, v->n);
 405                 if (!v)
 406                         return -1;
 407                 v->n++;
 408         }
 409         return pos;
 410 }
 411
 412 static struct vars *read_var_list(struct stream *s, struct vars *v)
 413 {
 414         struct token *tok;
 415
 416         while ((tok = stream_next_token(s)) != NULL) {
 417                 int p;
 418                 int n = v->n;
 419
 420                 if (tok->type != TOKEN_IDENT)
 421                         break;
 422
 423                 p = vars_pos(v, tok->u.s, -1);
 424                 if (p < 0)
 425                         goto error;
 426                 if (p < n) {
 427                         stream_error(s, tok, "expecting unique identifier");
 428                         goto error;
 429                 }
 430                 token_free(tok);
 431                 tok = stream_next_token(s);
 432                 if (!tok || tok->type != ',')
 433                         break;
 434
 435                 token_free(tok);
 436         }
 437         if (tok)
 438                 stream_push_token(s, tok);
 439
 440         return v;
 441 error:
 442         token_free(tok);
 443         vars_free(v);
 444         return NULL;
 445 }
 446
 447 static struct vars *read_tuple(struct stream *s, struct vars *v)
 448 {
 449         struct token *tok;
 450
 451         tok = stream_next_token(s);
 452         if (!tok || tok->type != '[') {
 453                 stream_error(s, tok, "expecting '['");
 454                 goto error;
 455         }
 456         token_free(tok);
 457         v = read_var_list(s, v);
 458         tok = stream_next_token(s);
 459         if (!tok || tok->type != ']') {
 460                 stream_error(s, tok, "expecting ']'");
 461                 goto error;
 462         }
 463         token_free(tok);
 464
 465         return v;
 466 error:
 467         if (tok)
 468                 token_free(tok);
 469         vars_free(v);
 470         return NULL;
 471 }
 472
 473 static struct isl_basic_map *add_constraints(struct stream *s,
 474         struct vars **v, struct isl_basic_map *bmap);
 475
 476 static struct isl_basic_map *add_exists(struct stream *s,
 477         struct vars **v, struct isl_basic_map *bmap)
 478 {
 479         struct token *tok;
 480         int n = (*v)->n;
 481         int extra;
 482         int seen_paren = 0;
 483         int i;
 484         unsigned total;
 485
 486         tok = stream_next_token(s);
 487         if (!tok)
 488                 goto error;
 489         if (tok->type == '(') {
 490                 seen_paren = 1;
 491                 token_free(tok);
 492         } else
 493                 stream_push_token(s, tok);
 494         *v = read_var_list(s, *v);
 495         if (!*v)
 496                 goto error;
 497         extra = (*v)->n - n;
 498         bmap = isl_basic_map_extend(s->ctx, bmap, bmap->nparam,
 499                         bmap->n_in, bmap->n_out, extra, 0, 0);
 500         total = bmap->nparam+bmap->n_in+bmap->n_out+bmap->extra;
 501         for (i = 0; i < extra; ++i) {
 502                 int k;
 503                 if ((k = isl_basic_map_alloc_div(s->ctx, bmap)) < 0)
 504                         goto error;
 505                 isl_seq_clr(bmap->div[k], 1+1+total);
 506         }
 507         if (!bmap)
 508                 return NULL;
 509         if (stream_eat(s, ':'))
 510                 goto error;
 511         bmap = add_constraints(s, v, bmap);
 512         if (seen_paren && stream_eat(s, ')'))
 513                 goto error;
 514         return bmap;
 515 error:
 516         isl_basic_map_free(s->ctx, bmap);
 517         return NULL;
 518 }
 519
 520 static struct isl_basic_map *add_constraint(struct stream *s,
 521         struct vars **v, struct isl_basic_map *bmap)
 522 {
 523         unsigned total = bmap->nparam+bmap->n_in+bmap->n_out+bmap->extra;
 524         int k;
 525         int sign = 1;
 526         int equality = 0;
 527         int op = 0;
 528         struct token *tok = NULL;
 529
 530         tok = stream_next_token(s);
 531         if (!tok)
 532                 goto error;
 533         if (tok->type == TOKEN_EXISTS) {
 534                 token_free(tok);
 535                 return add_exists(s, v, bmap);
 536         }
 537         stream_push_token(s, tok);
 538
 539         bmap = isl_basic_map_extend(s->ctx, bmap, bmap->nparam,
 540                         bmap->n_in, bmap->n_out, 0, 0, 1);
 541         k = isl_basic_map_alloc_inequality(s->ctx, bmap);
 542         if (k < 0)
 543                 goto error;
 544         isl_seq_clr(bmap->ineq[k], 1+total);
 545
 546         for (;;) {
 547                 tok = stream_next_token(s);
 548                 if (!tok) {
 549                         stream_error(s, NULL, "unexpected EOF");
 550                         goto error;
 551                 }
 552                 if (tok->type == TOKEN_IDENT) {
 553                         int n = (*v)->n;
 554                         int pos = vars_pos(*v, tok->u.s, -1);
 555                         if (pos < 0)
 556                                 goto error;
 557                         if (pos >= n) {
 558                                 stream_error(s, tok, "unknown identifier");
 559                                 goto error;
 560                         }
 561                         if (sign > 0)
 562                                 isl_int_add_ui(bmap->ineq[k][1+pos],
 563                                                 bmap->ineq[k][1+pos], 1);
 564                         else
 565                                 isl_int_sub_ui(bmap->ineq[k][1+pos],
 566                                                 bmap->ineq[k][1+pos], 1);
 567                 } else if (tok->type == TOKEN_VALUE) {
 568                         struct token *tok2;
 569                         int n = (*v)->n;
 570                         int pos = -1;
 571                         tok2 = stream_next_token(s);
 572                         if (tok2 && tok2->type == TOKEN_IDENT) {
 573                                 pos = vars_pos(*v, tok2->u.s, -1);
 574                                 if (pos < 0)
 575                                         goto error;
 576                                 if (pos >= n) {
 577                                         stream_error(s, tok2,
 578                                                 "unknown identifier");
 579                                         token_free(tok2);
 580                                         goto error;
 581                                 }
 582                                 token_free(tok2);
 583                         } else if (tok2)
 584                                 stream_push_token(s, tok2);
 585                         if (sign < 0)
 586                                 isl_int_neg(tok->u.v, tok->u.v);
 587                         isl_int_add(bmap->ineq[k][1+pos],
 588                                         bmap->ineq[k][1+pos], tok->u.v);
 589                 } else if (tok->type == TOKEN_LE) {
 590                         op = 1;
 591                         isl_seq_neg(bmap->ineq[k], bmap->ineq[k], 1+total);
 592                 } else if (tok->type == TOKEN_GE) {
 593                         op = 1;
 594                         sign = -1;
 595                 } else if (tok->type == '=') {
 596                         if (op) {
 597                                 stream_error(s, tok, "too many operators");
 598                                 goto error;
 599                         }
 600                         op = 1;
 601                         equality = 1;
 602                         sign = -1;
 603                 } else {
 604                         stream_push_token(s, tok);
 605                         break;
 606                 }
 607                 token_free(tok);
 608         }
 609         tok = NULL;
 610         if (!op) {
 611                 stream_error(s, tok, "missing operator");
 612                 goto error;
 613         }
 614         if (equality)
 615                 isl_basic_map_inequality_to_equality(s->ctx, bmap, k);
 616         return bmap;
 617 error:
 618         if (tok)
 619                 token_free(tok);
 620         isl_basic_map_free(s->ctx, bmap);
 621         return NULL;
 622 }
 623
 624 static struct isl_basic_map *add_constraints(struct stream *s,
 625         struct vars **v, struct isl_basic_map *bmap)
 626 {
 627         struct token *tok;
 628
 629         for (;;) {
 630                 bmap = add_constraint(s, v, bmap);
 631                 if (!bmap)
 632                         return NULL;
 633                 tok = stream_next_token(s);
 634                 if (!tok) {
 635                         stream_error(s, NULL, "unexpected EOF");
 636                         goto error;
 637                 }
 638                 if (tok->type != TOKEN_AND)
 639                         break;
 640                 token_free(tok);
 641         }
 642         stream_push_token(s, tok);
 643
 644         return bmap;
 645 error:
 646         if (tok)
 647                 token_free(tok);
 648         isl_basic_map_free(s->ctx, bmap);
 649         return NULL;
 650 }
 651
 652 static struct isl_basic_map *basic_map_read(struct stream *s)
 653 {
 654         struct isl_basic_map *bmap = NULL;
 655         struct token *tok;
 656         struct vars *v = NULL;
 657         int n1;
 658         int n2;
 659
 660         tok = stream_next_token(s);
 661         if (!tok || tok->type != '{') {
 662                 stream_error(s, tok, "expecting '{'");
 663                 if (tok)
 664                         stream_push_token(s, tok);
 665                 goto error;
 666         }
 667         token_free(tok);
 668         v = vars_new(s->ctx);
 669         v = read_tuple(s, v);
 670         if (!v)
 671                 return NULL;
 672         n1 = v->n;
 673         tok = stream_next_token(s);
 674         if (tok && tok->type == TOKEN_TO) {
 675                 token_free(tok);
 676                 v = read_tuple(s, v);
 677                 if (!v)
 678                         return NULL;
 679                 n2 = v->n - n1;
 680         } else {
 681                 if (tok)
 682                         stream_push_token(s, tok);
 683                 n2 = n1;
 684                 n1 = 0;
 685         }
 686         bmap = isl_basic_map_alloc(s->ctx, 0, n1, n2, 0, 0,0);
 687         if (!bmap)
 688                 goto error;
 689         tok = stream_next_token(s);
 690         if (tok && tok->type == ':') {
 691                 token_free(tok);
 692                 bmap = add_constraints(s, &v, bmap);
 693                 tok = stream_next_token(s);
 694         }
 695         if (tok && tok->type == '}') {
 696                 token_free(tok);
 697         } else {
 698                 stream_error(s, tok, "unexpected token");
 699                 if (tok)
 700                         token_free(tok);
 701                 goto error;
 702         }
 703         vars_free(v);
 704
 705         return bmap;
 706 error:
 707         isl_basic_map_free(s->ctx, bmap);
 708         if (v)
 709                 vars_free(v);
 710         return NULL;
 711 }
 712
 713 struct isl_basic_map *isl_basic_map_read_from_file_omega(
 714                 struct isl_ctx *ctx, FILE *input)
 715 {
 716         struct isl_basic_map *bmap;
 717         struct stream *s = stream_new_file(ctx, input);
 718         if (!s)
 719                 return NULL;
 720         bmap = basic_map_read(s);
 721         stream_free(s);
 722         return bmap;
 723 }
 724
 725 struct isl_basic_set *isl_basic_set_read_from_file_omega(
 726                 struct isl_ctx *ctx, FILE *input)
 727 {
 728         struct isl_basic_map *bmap;
 729         bmap = isl_basic_map_read_from_file_omega(ctx, input);
 730         if (!bmap)
 731                 return NULL;
 732         isl_assert(ctx, bmap->n_in == 0, goto error);
 733         return (struct isl_basic_set *)bmap;
 734 error:
 735         isl_basic_map_free(ctx, bmap);
 736         return NULL;
 737 }