lingeling/code/lgldimacs.c

   1 #include "lgldimacs.h"
   2
   3 #include <assert.h>
   4 #include <ctype.h>
   5 #include <stdlib.h>
   6 #include <string.h>
   7 #include <sys/stat.h>
   8 #include <sys/types.h>
   9 #include <unistd.h>
  10 #include <limits.h>
  11
  12 struct LDR {
  13   struct {
  14     void * state;
  15     ldralloc alloc;
  16     ldrdealloc dealloc;
  17   } mem;
  18   struct { void * state; ldropt fun; } opt;
  19   struct { void * state; ldrheader fun; } header;
  20   struct { void * state; ldradd fun; } add;
  21   char * path;
  22   char * errmsg;
  23   int closefile;
  24   FILE * file;
  25   int lineno;
  26 };
  27
  28 static void * ldrstdalloc (void * mem, size_t bytes) {
  29   (void) mem;
  30   return malloc (bytes);
  31 }
  32
  33 static void ldrstdealloc (void * mem, void * ptr, size_t bytes) {
  34   (void) mem;
  35   (void) bytes;
  36   free (ptr);
  37 }
  38
  39 static void * ldrstdrealloc (void * mem, void * ptr, size_t ob, size_t nb) {
  40   (void) mem;
  41   (void) ob;
  42   return realloc (ptr, nb);
  43 }
  44
  45 LDR * ldrinit () {
  46   return ldrminit (0, ldrstdalloc, ldrstdrealloc, ldrstdealloc);
  47 }
  48
  49 LDR * ldrminit (void * state,
  50                 ldralloc alloc, ldrealloc realloc, ldrdealloc dealloc) {
  51   LDR * res = alloc (state, sizeof *res);
  52   if (!res) return res;
  53   memset (res, 0, sizeof *res);
  54   res->mem.state = state;
  55   res->mem.alloc = alloc;
  56   res->mem.dealloc = dealloc;
  57   return res;
  58 }
  59
  60 static void ldrdelstr (LDR * ldr, char * str) {
  61   if (str) ldr->mem.dealloc (ldr->mem.state, str, strlen (str) + 1);
  62 }
  63
  64 static char * ldrstrdup (LDR * ldr, const char* str) {
  65   size_t bytes = strlen (str) + 1;
  66   char * res = ldr->mem.alloc (ldr->mem.state, bytes);
  67   return strcpy (res, str);
  68 }
  69
  70 void ldrelease (LDR * ldr) {
  71   if (ldr->file) {
  72     if (ldr->closefile == 1) fclose (ldr->file);
  73     if (ldr->closefile == 2) pclose (ldr->file);
  74   }
  75   ldrdelstr (ldr, ldr->errmsg);
  76   ldrdelstr (ldr, ldr->path);
  77   ldr->mem.dealloc (ldr->mem.state, ldr, sizeof *ldr);
  78 }
  79
  80 void ldrsetopt (LDR * ldr, void * state, ldropt fun) {
  81   ldr->opt.fun = fun;
  82   ldr->opt.state = state;
  83 }
  84
  85 void ldrsetheader (LDR * ldr, void * state, ldrheader fun) {
  86   ldr->header.fun = fun;
  87   ldr->header.state = state;
  88 }
  89
  90 void ldrsetadd (LDR * ldr, void * state, ldradd fun) {
  91   ldr->add.fun = fun;
  92   ldr->add.state = state;
  93 }
  94
  95 static int ldrfilexists (const char * path) {
  96   struct stat buf;
  97   return !stat (path, &buf);
  98 }
  99
 100 static int ldrperr (LDR * ldr, const char * msg) {
 101   size_t bytes, len;
 102   char * str;
 103   assert (!ldr->errmsg);
 104   assert (ldr->path);
 105   bytes = strlen (msg) + strlen (ldr->path) + 20;
 106   str = ldr->mem.alloc (ldr->mem.state, bytes);
 107   sprintf (str, "%s:%d: %s", ldr->path, ldr->lineno, msg);
 108   len = strlen (str) + 1;
 109   ldr->errmsg = strcpy (ldr->mem.alloc (ldr->mem.state, len), str);
 110   ldr->mem.dealloc (ldr->mem.state, str, bytes);
 111   return 0;
 112 }
 113
 114 static int ldrhas (const char * str, const char * suffix) {
 115   int l = strlen (str), k = strlen (suffix);
 116   if (l < k) return 0;
 117   return !strcmp (str + l - k, suffix);
 118 }
 119
 120 static FILE * ldrcmd (LDR * ldr, const char * fmt, const char * name) {
 121   FILE * res;
 122   int len = strlen (fmt) + strlen (name) + 1;
 123   char * s = ldr->mem.alloc (ldr->mem.state, len);
 124   sprintf (s, fmt, name);
 125   res = popen (s, "r");
 126   ldr->mem.dealloc (ldr->mem.state, s, len);
 127   return res;
 128 }
 129
 130 void ldrsetpath (LDR * ldr, const char * path) {
 131   assert (!ldr->file);
 132   assert (!ldr->path);
 133   assert (!ldr->closefile);
 134   ldr->path = ldrstrdup (ldr, path);
 135   if (!ldrfilexists (path))
 136     return (void) ldrperr (ldr, "file does not exist");
 137   ldr->closefile = 2;
 138   if (ldrhas (path, ".gz"))
 139     ldr->file = ldrcmd  (ldr, "gunzip -c %s", path);
 140   else if (ldrhas (path, ".bz2"))
 141     ldr->file = ldrcmd (ldr, "bzcat %s", path);
 142   else if (ldrhas (path, ".7z"))
 143     ldr->file = ldrcmd (ldr, "7z x -so %s 2>/dev/null", path);
 144   else if (ldrhas (path, ".lzma"))
 145     ldr->file = ldrcmd (ldr, "lzcat %s", path);
 146   else ldr->file = fopen (path, "r"), ldr->closefile = 1;
 147   if (!ldr->file) return (void) ldrperr (ldr, "can not open file");
 148 }
 149
 150 void ldrsetfile (LDR * ldr, FILE * file) {
 151   assert (!ldr->file);
 152   assert (!ldr->path);
 153   assert (!ldr->closefile);
 154   ldr->file = file;
 155   ldr->path = ldrstrdup (ldr, "<unspecified-path>");
 156 }
 157
 158 void ldrsetnamedfile (LDR * ldr, FILE * file, const char * path) {
 159   assert (!ldr->file);
 160   assert (!ldr->path);
 161   assert (!ldr->closefile);
 162   ldr->file = file;
 163   ldr->path = ldrstrdup (ldr, path);
 164 }
 165
 166 const char * ldrerr (LDR * ldr) { return ldr->errmsg; }
 167
 168 static int ldrnext (LDR * ldr) {
 169   int ch;
 170   assert (ldr);
 171   assert (ldr->file);
 172   ch = getc (ldr->file);
 173   if (ch == '\n') ldr->lineno++;
 174   return ch;
 175 }
 176
 177 int ldrparse (LDR * ldr) {
 178   struct { int parsed, specified; } vars, clauses;
 179   int ch, sign, lit, digit;
 180   if (ldr->errmsg) return 0;
 181   while ((ch = ldrnext (ldr)) == 'c') {
 182     // TODO parse embedded options
 183     while ((ch = ldrnext (ldr)) != '\n')
 184       if (ch == EOF)
 185         return ldrperr (ldr, "end-of-file in comment before header");
 186   }
 187   if (ch != 'p') return ldrperr (ldr, "expected 'p' or 'c'");
 188   if (ldrnext (ldr) != ' ') return ldrperr (ldr, "expected space after 'p'");
 189   if (ldrnext (ldr) != 'c') return ldrperr (ldr, "expected 'c' after 'p '");
 190   if (ldrnext (ldr) != 'n') return ldrperr (ldr, "expected 'n' after 'p c'");
 191   if (ldrnext (ldr) != 'f') return ldrperr (ldr, "expected 'f' after 'p cn'");
 192   if (ldrnext (ldr) != ' ')
 193     return ldrperr (ldr, "expected space after 'p cnf'");
 194   ch = ldrnext (ldr);
 195   if (!isdigit (ch)) return ldrperr (ldr, "expected digit after 'p cnf '");
 196   vars.specified = ch - '0';
 197   while (isdigit (ch = ldrnext (ldr))) {
 198     if (INT_MAX/10 < vars.specified)
 199 NUMBER_TOO_LARGE:
 200       return ldrperr (ldr, "number too large");
 201     vars.specified *= 10;
 202     digit = (ch - '0');
 203     if (INT_MAX - digit < vars.specified) goto NUMBER_TOO_LARGE;
 204     vars.specified += digit;
 205   }
 206   if (ch != ' ')
 207     return ldrperr (ldr, "expected space after maximum variable index");
 208   if (!isdigit (ch = ldrnext (ldr)))
 209     return ldrperr (ldr, "expected digit after space after variable index");
 210   clauses.specified = ch - '0';
 211   while (isdigit (ch = ldrnext (ldr))) {
 212     if (INT_MAX/10 < clauses.specified) goto NUMBER_TOO_LARGE;
 213     clauses.specified *= 10;
 214     digit = (ch - '0');
 215     if (INT_MAX - digit < clauses.specified) goto NUMBER_TOO_LARGE;
 216     clauses.specified += digit;
 217   }
 218   while (ch == ' ' || ch == '\t' || ch == '\r')
 219     ch = ldrnext (ldr);
 220   if (ch != '\n') return ldrperr (ldr, "expected new line after header");
 221   if (ldr->header.fun)
 222     ldr->header.fun (ldr->header.state, vars.specified, clauses.specified);
 223   vars.parsed = clauses.parsed = 0;
 224   lit = 0;
 225   for (;;) {
 226     ch = ldrnext (ldr);
 227     if (ch == ' ' || ch == '\t' || ch == '\r' || ch == '\n') continue;
 228     if (ch == 'c') {
 229       while ((ch = ldrnext (ldr)) != '\n') {
 230         if (ch == EOF)
 231           return ldrperr (ldr, "end-of-file in comment after header");
 232       }
 233       continue;
 234     }
 235     if (ch == EOF) {
 236       if (lit) return ldrperr (ldr, "zero sentinel missing at end-of-file");
 237       assert (clauses.parsed <= clauses.specified);
 238       if (clauses.parsed + 1 == clauses.specified)
 239         return ldrperr (ldr, "one clause is missing");
 240       if (clauses.parsed < clauses.specified)
 241         return ldrperr (ldr, "clauses are missing");
 242       break;
 243     }
 244     if (ch == '-') {
 245       ch = ldrnext (ldr);
 246       if (!isdigit (ch)) return ldrperr (ldr, "expected digit after '-'");
 247       sign = -1;
 248     } else if (!isdigit (ch)) return ldrperr (ldr, "expected digit or '-'");
 249     else sign = 1;
 250     assert (clauses.parsed <= clauses.specified);
 251     if (clauses.specified == clauses.parsed)
 252       return ldrperr (ldr, "too many clauses");
 253     lit = ch - '0';
 254     while (isdigit (ch = ldrnext (ldr))) {
 255       if (INT_MAX/10 < lit) goto NUMBER_TOO_LARGE;
 256       lit *= 10;
 257       digit = (ch - '0');
 258       if (INT_MAX - digit < lit) goto NUMBER_TOO_LARGE;
 259       lit += digit;
 260     }
 261     assert (0 <= lit);
 262     if (lit > vars.specified)
 263       return ldrperr (ldr, "maximum variable index exceeded");
 264     lit *= sign;
 265     assert ((sign < 0) == (lit < 0));
 266     if (ldr->add.fun) ldr->add.fun (ldr->add.state, lit);
 267     if (lit) continue;
 268     clauses.parsed++;
 269     assert (clauses.parsed <= clauses.specified);
 270   }
 271   return 1;
 272 }