From 382d37dbf0ee8bf5af9594e922db6094e30ace2a Mon Sep 17 00:00:00 2001 From: aiju Date: Wed, 28 Mar 2018 17:08:30 +0000 Subject: [PATCH] add forp --- sys/src/cmd/forp/cvt.c | 525 +++++++++++++++++++++++++++++++++++++++ sys/src/cmd/forp/dat.h | 94 +++++++ sys/src/cmd/forp/fns.h | 18 ++ sys/src/cmd/forp/forp.c | 159 ++++++++++++ sys/src/cmd/forp/logic.c | 273 ++++++++++++++++++++ sys/src/cmd/forp/misc.c | 246 ++++++++++++++++++ sys/src/cmd/forp/mkfile | 14 ++ sys/src/cmd/forp/parse.c | 454 +++++++++++++++++++++++++++++++++ 8 files changed, 1783 insertions(+) create mode 100644 sys/src/cmd/forp/cvt.c create mode 100644 sys/src/cmd/forp/dat.h create mode 100644 sys/src/cmd/forp/fns.h create mode 100644 sys/src/cmd/forp/forp.c create mode 100644 sys/src/cmd/forp/logic.c create mode 100644 sys/src/cmd/forp/misc.c create mode 100644 sys/src/cmd/forp/mkfile create mode 100644 sys/src/cmd/forp/parse.c diff --git a/sys/src/cmd/forp/cvt.c b/sys/src/cmd/forp/cvt.c new file mode 100644 index 000000000..7f146c5c0 --- /dev/null +++ b/sys/src/cmd/forp/cvt.c @@ -0,0 +1,525 @@ +#include +#include +#include +#include +#include "dat.h" +#include "fns.h" + +SATSolve *sat; +int satvar = 3; /* 1 = false, 2 = true */ +#define SVAR(n, i) ((n)->vars[(i) < (n)->size ? (i) : (n)->size - 1]) +int nassertvar; +int *assertvar; + +static int +max(int a, int b) +{ + return a < b ? b : a; +} + +static int +min(int a, int b) +{ + return a > b ? b : a; +} + +static void +symsat(Node *n) +{ + Symbol *s; + int i; + + s = n->sym; + assert(s->type == SYMBITS); + n->size = s->size + ((s->flags & SYMFSIGNED) == 0); + n->vars = emalloc(sizeof(int) * n->size); + for(i = 0; i < s->size; i++){ + if(s->vars[i] == 0) + s->vars[i] = satvar++; + n->vars[i] = s->vars[i]; + } + if((s->flags & SYMFSIGNED) == 0) + n->vars[i] = 1; +} + +static void +numsat(Node *n) +{ + mpint *m; + int i, sz, j; + + m = n->num; + assert(m != nil); + assert(m->sign > 0); + sz = mpsignif(m) + 1; + n->size = sz; + n->vars = emalloc(sizeof(int) * sz); + for(i = 0; i < m->top; i++){ + for(j = 0; j < Dbits; j++) + if(i * Dbits + j < sz-1) + n->vars[i * Dbits + j] = 1 + ((m->p[i] >> j & 1) != 0); + } + n->vars[sz - 1] = 1; +} + +static void +nodevars(Node *n, int nv) +{ + int i; + + n->size = nv; + n->vars = emalloc(sizeof(int) * nv); + for(i = 0; i < nv; i++) + n->vars[i] = 1; +} + +static void +assign(Node *t, Node *n) +{ + Symbol *s; + int i; + + s = t->sym; + for(i = 0; i < s->size; i++){ + if(i < n->size) + s->vars[i] = n->vars[i]; + else + s->vars[i] = n->vars[n->size - 1]; + } +} + +static void +opeq(Node *r, Node *n1, Node *n2, int neq) +{ + int i, m, a, b, *t; + + nodevars(r, 2); + m = max(n1->size, n2->size); + t = malloc(m * sizeof(int)); + for(i = 0; i < m; i++){ + a = SVAR(n1, i); + b = SVAR(n2, i); + t[i] = satlogicv(sat, neq ? 6 : 9, a, b, 0); + } + if(neq) + r->vars[0] = sator1(sat, t, m); + else + r->vars[0] = satand1(sat, t, m); + free(t); +} + +static void +oplogic(Node *r, Node *n1, Node *n2, int op) +{ + int m, i, a, b, *t; + + m = max(n1->size, n2->size); + nodevars(r, m); + t = r->vars; + for(i = 0; i < m; i++){ + a = SVAR(n1, i); + b = SVAR(n2, i); + switch(op){ + case OPOR: + t[i] = satorv(sat, a, b, 0); + break; + case OPAND: + t[i] = satandv(sat, a, b, 0); + break; + case OPXOR: + t[i] = satlogicv(sat, 6, a, b, 0); + break; + default: abort(); + } + } +} + +static int +tologic(Node *n) +{ + int i; + + for(i = 1; i < n->size; i++) + if(n->vars[i] != 1) + break; + if(i == n->size) + return n->vars[0]; + return sator1(sat, n->vars, n->size); +} + +static void +opllogic(Node *rn, Node *n1, Node *n2, int op) +{ + int a, b; + + a = tologic(n1); + b = tologic(n2); + nodevars(rn, 2); + switch(op){ + case OPLAND: + rn->vars[0] = satandv(sat, a, b, 0); + break; + case OPLOR: + rn->vars[0] = satorv(sat, a, b, 0); + break; + case OPIMP: + rn->vars[0] = satorv(sat, -a, b, 0); + break; + case OPEQV: + rn->vars[0] = satlogicv(sat, 9, a, b, 0); + break; + default: + abort(); + } +} + +static void +opcom(Node *r, Node *n1) +{ + int i; + + nodevars(r, n1->size); + for(i = 0; i < n1->size; i++) + r->vars[i] = -n1->vars[i]; +} + +static void +opneg(Node *r, Node *n1) +{ + int i, c; + + nodevars(r, n1->size); + c = 2; + for(i = 0; i < n1->size; i++){ + r->vars[i] = satlogicv(sat, 9, n1->vars[i], c, 0); + if(i < n1->size - 1) + c = satandv(sat, -n1->vars[i], c, 0); + } +} + +static void +opnot(Node *r, Node *n1) +{ + nodevars(r, 2); + r->vars[0] = -tologic(n1); +} + +static void +opadd(Node *rn, Node *n1, Node *n2, int sub) +{ + int i, m, c, a, b; + + m = max(n1->size, n2->size) + 1; + nodevars(rn, m); + c = 1 + sub; + sub = 1 - 2 * sub; + for(i = 0; i < m; i++){ + a = SVAR(n1, i); + b = SVAR(n2, i) * sub; + rn->vars[i] = satlogicv(sat, 0x96, c, a, b, 0); + c = satlogicv(sat, 0xe8, c, a, b, 0); + } +} + +static void +oplt(Node *rn, Node *n1, Node *n2, int le) +{ + int i, m, a, b, t, *r; + + nodevars(rn, 2); + m = max(n1->size, n2->size); + r = emalloc(sizeof(int) * (m + le)); + t = 2; + for(i = m; --i >= 0; ){ + if(i == m - 1){ + a = SVAR(n2, i); + b = SVAR(n1, i); + }else{ + a = SVAR(n1, i); + b = SVAR(n2, i); + } + r[i] = satandv(sat, -a, b, t, 0); + t = satlogicv(sat, 0x90, a, b, t, 0); + } + if(le) + r[m] = t; + rn->vars[0] = sator1(sat, r, m + le); +} + +static void +opidx(Node *rn, Node *n1, Node *n2, Node *n3) +{ + int i, j, k, s; + + j = mptoi(n2->num); + if(n3 == nil) k = j; + else k = mptoi(n3->num); + if(j > k){ + nodevars(rn, 1); + return; + } + s = k - j + 1; + nodevars(rn, s + 1); + for(i = 0; i < s; i++) + rn->vars[i] = SVAR(n1, j + i); +} + +static void +oprsh(Node *rn, Node *n1, Node *n2) +{ + int i, j, a, b, q; + + nodevars(rn, n1->size); + memcpy(rn->vars, n1->vars, sizeof(int) * n1->size); + for(i = 0; i < n2->size; i++){ + if(n2->vars[i] == 1) continue; + if(n2->vars[i] == 2){ + for(j = 0; j < n1->size; j++) + rn->vars[j] = SVAR(rn, j + (1<size; j++){ + a = rn->vars[j]; + b = SVAR(rn, j + (1<vars[i]; + rn->vars[j] = satlogicv(sat, 0xca, a, b, q, 0); + } + } +} + +static void +oplsh(Node *rn, Node *n1, Node *n2, uint sz) +{ + int i, j, a, b, q; + u32int m; + + m = 0; + for(i = n2->size; --i >= 0; ) + m = m << 1 | n2->vars[i] != m; + m += n1->size; + if(m > sz) m = sz; + nodevars(rn, m); + for(i = 0; i < m; i++) + rn->vars[i] = SVAR(n1, i); + for(i = 0; i < n2->size; i++){ + if(n2->vars[i] == 1) continue; + if(n2->vars[i] == 2){ + for(j = m; --j >= 0; ) + rn->vars[j] = j >= 1<vars[j - (1<= 0; ){ + a = rn->vars[j]; + b = j >= 1<vars[j - (1<vars[i]; + rn->vars[j] = satlogicv(sat, 0xca, a, b, q, 0); + } + } +} + +static void +optern(Node *rn, Node *n1, Node *n2, Node *n3, uint sz) +{ + uint m; + int i, a, b, q; + + m = n1->size; + if(n2->size > m) m = n2->size; + if(m > sz) m = sz; + nodevars(rn, m); + q = tologic(n1); + for(i = 0; i < m; i++){ + a = SVAR(n3, i); + b = SVAR(n2, i); + rn->vars[i] = satlogicv(sat, 0xca, a, b, q, 0); + } +} + +static int * +opmul(int *n1v, int s1, int *n2v, int s2) +{ + int i, k, t, s; + int *r, *q0, *q1, *z, nq0, nq1, nq; + + s1--; + s2--; + r = emalloc(sizeof(int) * (s1 + s2 + 2)); + nq = 2 * (min(s1, s2) + 1); + q0 = emalloc(nq * sizeof(int)); + q1 = emalloc(nq * sizeof(int)); + nq0 = nq1 = 0; + for(k = 0; k <= s1 + s2 + 1; k++){ + if(k == s1 || k == s1 + s2 + 1){ assert(nq0 < nq); q0[nq0++] = 2; } + if(k == s2){ assert(nq0 < nq); q0[nq0++] = 2; } + for(i = max(0, k - s2); i <= k && i <= s1; i++){ + assert(nq0 < nq); + t = satandv(sat, n1v[i], n2v[k - i], 0); + q0[nq0++] = i == s1 ^ k-i == s2 ? -t : t; + } + assert(nq0 > 0); + while(nq0 > 1){ + if(nq0 == 2){ + t = satlogicv(sat, 0x6, q0[0], q0[1], 0); + s = satandv(sat, q0[0], q0[1], 0); + q0[0] = t; + assert(nq1 < nq); + q1[nq1++] = s; + break; + } + t = satlogicv(sat, 0x96, q0[nq0-3], q0[nq0-2], q0[nq0-1], 0); + s = satlogicv(sat, 0xe8, q0[nq0-3], q0[nq0-2], q0[nq0-1], 0); + q0[nq0-3] = t; + nq0 -= 2; + assert(nq1 < nq); + q1[nq1++] = s; + } + r[k] = q0[0]; + z=q0, q0=q1, q1=z; + nq0 = nq1; + nq1 = 0; + } + free(q0); + free(q1); + return r; +} + +static void +opabs(Node *q, Node *n) +{ + int i; + int s, c; + + nodevars(q, n->size + 1); + s = n->vars[n->size - 1]; + c = s; + for(i = 0; i < n->size; i++){ + q->vars[i] = satlogicv(sat, 0x96, n->vars[i], s, c, 0); + c = satandv(sat, -n->vars[i], c, 0); + } +} + +static void +opdiv(Node *q, Node *r, Node *n1, Node *n2) +{ + Node *s; + int i; + + if(q == nil) q = node(ASTTEMP); + if(r == nil) r = node(ASTTEMP); + nodevars(q, n1->size); + nodevars(r, n2->size); + for(i = 0; i < n1->size; i++) + q->vars[i] = satvar++; + for(i = 0; i < n2->size; i++) + r->vars[i] = satvar++; + s = node(ASTBIN, OPEQ, node(ASTBIN, OPADD, node(ASTBIN, OPMUL, q, n2), r), n1); convert(s, -1); assume(s); + s = node(ASTBIN, OPGE, r, node(ASTNUM, mpnew(0))); convert(s, -1); assume(s); + s = node(ASTBIN, OPLT, r, node(ASTUN, OPABS, n2)); convert(s, -1); assume(s); +} + +void +convert(Node *n, uint sz) +{ + if(n->size > 0) return; + switch(n->type){ + case ASTTEMP: + assert(n->size > 0); + break; + case ASTSYM: + symsat(n); + break; + case ASTNUM: + numsat(n); + break; + case ASTBIN: + if(n->op == OPASS){ + if(n->n1 == nil || n->n1->type != ASTSYM) + error(n, "convert: '%ε' invalid lval", n->n1); + convert(n->n2, n->n1->sym->size); + assert(n->n2->size > 0); + assign(n->n1, n->n2); + break; + } + switch(n->op){ + case OPAND: case OPOR: case OPXOR: + case OPADD: case OPSUB: case OPLSH: + case OPCOMMA: + convert(n->n1, sz); + convert(n->n2, sz); + break; + default: + convert(n->n1, -1); + convert(n->n2, -1); + } + assert(n->n1->size > 0); + assert(n->n2->size > 0); + switch(n->op){ + case OPCOMMA: n->size = n->n2->size; n->vars = n->n2->vars; break; + case OPEQ: opeq(n, n->n1, n->n2, 0); break; + case OPNEQ: opeq(n, n->n1, n->n2, 1); break; + case OPLT: oplt(n, n->n1, n->n2, 0); break; + case OPLE: oplt(n, n->n1, n->n2, 1); break; + case OPGT: oplt(n, n->n2, n->n1, 0); break; + case OPGE: oplt(n, n->n2, n->n1, 1); break; + case OPXOR: case OPAND: case OPOR: oplogic(n, n->n1, n->n2, n->op); break; + case OPLAND: case OPLOR: case OPIMP: case OPEQV: opllogic(n, n->n1, n->n2, n->op); break; + case OPADD: opadd(n, n->n1, n->n2, 0); break; + case OPSUB: opadd(n, n->n1, n->n2, 1); break; + case OPLSH: oplsh(n, n->n1, n->n2, sz); break; + case OPRSH: oprsh(n, n->n1, n->n2); break; + case OPMUL: n->vars = opmul(n->n1->vars, n->n1->size, n->n2->vars, n->n2->size); n->size = n->n1->size + n->n2->size; break; + case OPDIV: opdiv(n, nil, n->n1, n->n2); break; + case OPMOD: opdiv(nil, n, n->n1, n->n2); break; + default: + error(n, "convert: unimplemented op %O", n->op); + } + break; + case ASTUN: + convert(n->n1, sz); + switch(n->op){ + case OPCOM: opcom(n, n->n1); break; + case OPNEG: opneg(n, n->n1); break; + case OPNOT: opnot(n, n->n1); break; + case OPABS: opabs(n, n->n1); break; + default: + error(n, "convert: unimplemented op %O", n->op); + } + break; + case ASTIDX: + if(n->n2->type != ASTNUM || n->n3 != nil && n->n3->type != ASTNUM) + error(n, "non-constant in indexing expression"); + convert(n->n1, (n->n3 != nil ? mptoi(n->n3->num) : mptoi(n->n2->num)) + 1); + opidx(n, n->n1, n->n2, n->n3); + break; + case ASTTERN: + convert(n->n1, -1); + convert(n->n2, sz); + convert(n->n3, sz); + optern(n, n->n1, n->n2, n->n3, sz); + break; + default: + error(n, "convert: unimplemented %α", n->type); + } +} + +void +assume(Node *n) +{ + assert(n->size > 0); + satadd1(sat, n->vars, n->size); +} + +void +obviously(Node *n) +{ + assertvar = realloc(assertvar, sizeof(int) * (nassertvar + 1)); + assert(assertvar != nil); + assertvar[nassertvar++] = -tologic(n); +} + +void +cvtinit(void) +{ + sat = sataddv(nil, -1, 0); + sataddv(sat, 2, 0); +} diff --git a/sys/src/cmd/forp/dat.h b/sys/src/cmd/forp/dat.h new file mode 100644 index 000000000..32d8f0756 --- /dev/null +++ b/sys/src/cmd/forp/dat.h @@ -0,0 +1,94 @@ +typedef struct Line Line; +typedef struct Node Node; +typedef struct Symbol Symbol; +typedef struct Trie Trie; +typedef struct TrieHead TrieHead; + +struct Line { + char *filen; + int lineno; +}; + +struct TrieHead { + uvlong hash; + int l; +}; + +enum { TRIEB = 4 }; +struct Trie { + TrieHead; + Trie *n[1< +#include +#include +#include +#include "dat.h" +#include "fns.h" + +extern SATSolve *sat; +extern int *assertvar, nassertvar; + +int +printval(Symbol *s, Fmt *f) +{ + int i; + + if(s->type != SYMBITS) return 0; + fmtprint(f, "%s = ", s->name); + for(i = s->size - 1; i >= 0; i--) + switch(satval(sat, s->vars[i])){ + case 1: fmtrune(f, '1'); break; + case 0: fmtrune(f, '0'); break; + case -1: fmtrune(f, '?'); break; + default: abort(); + } + fmtprint(f, "\n"); + return 0; +} + +void +debugsat(void) +{ + int i, j, rc; + int *t; + int ta; + Fmt f; + char buf[256]; + + ta = 0; + t = nil; + fmtfdinit(&f, 1, buf, 256); + for(i = 0;;){ + rc = satget(sat, i, t, ta); + if(rc < 0) break; + if(rc > ta){ + ta = rc; + t = realloc(t, ta * sizeof(int)); + continue; + } + i++; + fmtprint(&f, "%d: ", i); + for(j = 0; j < rc; j++) + fmtprint(&f, "%s%d", j==0?"":" ∨ ", t[j]); + fmtprint(&f, "\n"); + } + free(t); + fmtfdflush(&f); +} + +void +tabheader(Fmt *f) +{ + Symbol *s; + int l, first; + + first = 0; + for(s = syms; s != nil; s = s->next){ + if(s->type != SYMBITS) continue; + l = strlen(s->name); + if(s->size > l) l = s->size; + fmtprint(f, "%s%*s", first++ != 0 ? " " : "", l, s->name); + } + fmtrune(f, '\n'); +} + +void +tabrow(Fmt *f) +{ + Symbol *s; + int i, l, first; + + first = 0; + for(s = syms; s != nil; s = s->next){ + if(s->type != SYMBITS) continue; + if(first++ != 0) fmtrune(f, ' '); + l = strlen(s->name); + if(s->size > l) l = s->size; + for(i = l - 1; i > s->size - 1; i--) + fmtrune(f, ' '); + for(; i >= 0; i--) + switch(satval(sat, s->vars[i])){ + case 1: fmtrune(f, '1'); break; + case 0: fmtrune(f, '0'); break; + case -1: fmtrune(f, '?'); break; + default: abort(); + } + } + fmtrune(f, '\n'); +} + +void +go(int mflag) +{ + Fmt f; + char buf[256]; + Symbol *s; + + if(nassertvar == 0) + sysfatal("left as an exercise to the reader"); + satadd1(sat, assertvar, nassertvar); +// debugsat(); + if(mflag){ + fmtfdinit(&f, 1, buf, sizeof(buf)); + tabheader(&f); + fmtfdflush(&f); + while(satmore(sat) > 0){ + tabrow(&f); + fmtfdflush(&f); + } + }else{ + if(satsolve(sat) == 0) + print("Proved.\n"); + else{ + fmtfdinit(&f, 1, buf, sizeof(buf)); + for(s = syms; s != nil; s = s->next) + printval(s, &f); + fmtfdflush(&f); + } + } +} + +void +usage(void) +{ + fprint(2, "usage: %s [ -m ] [ file ]\n", argv0); + exits("usage"); +} + +void +main(int argc, char **argv) +{ + typedef void init(void); + init miscinit, cvtinit, parsinit; + static int mflag; + + ARGBEGIN{ + case 'm': mflag++; break; + default: usage(); + }ARGEND; + + if(argc > 1) usage(); + + quotefmtinstall(); + fmtinstall('B', mpfmt); + miscinit(); + cvtinit(); + parsinit(); + parse(argc > 0 ? argv[0] : nil); + go(mflag); +} diff --git a/sys/src/cmd/forp/logic.c b/sys/src/cmd/forp/logic.c new file mode 100644 index 000000000..b266e3bca --- /dev/null +++ b/sys/src/cmd/forp/logic.c @@ -0,0 +1,273 @@ +#include +#include +#include +#include +#include "dat.h" +#include "fns.h" + +extern int satvar; + +int +satand1(SATSolve *sat, int *a, int n) +{ + int i, j, r; + int *b; + + if(n < 0) + for(n = 0; a[n] != 0; n++) + ; + r = 2; + for(i = j = 0; i < n; i++){ + if(a[i] == 1 || a[i] == -2) + return 1; + if(a[i] == 2 || a[i] == -1) + j++; + else + r = a[i]; + } + if(j >= n - 1) return r; + r = satvar++; + b = malloc(sizeof(int) * (n+1)); + for(i = j = 0; i < n; i++){ + if(a[i] == 2 || a[i] == -1) + continue; + b[j++] = -a[i]; + sataddv(sat, -r, a[i], 0); + } + b[j++] = r; + satadd1(sat, b, j); + return r; +} + +int +satandv(SATSolve *sat, ...) +{ + int r; + va_list va; + + va_start(va, sat); + r = satand1(sat, (int*)va, -1); + va_end(va); + return r; +} + +int +sator1(SATSolve *sat, int *a, int n) +{ + int i, j, r; + int *b; + + if(n < 0) + for(n = 0; a[n] != 0; n++) + ; + r = 1; + for(i = j = 0; i < n; i++){ + if(a[i] == 2 || a[i] == -1) + return 2; + if(a[i] == 1 || a[i] == -2) + j++; + else + r = a[i]; + } + if(j >= n-1) return r; + r = satvar++; + b = malloc(sizeof(int) * (n+1)); + for(i = j = 0; i < n; i++){ + if(a[i] == 1 || a[i] == -2) + continue; + b[j++] = a[i]; + sataddv(sat, r, -a[i], 0); + } + b[j++] = -r; + satadd1(sat, b, j); + return r; +} + +int +satorv(SATSolve *sat, ...) +{ + va_list va; + int r; + + va_start(va, sat); + r = sator1(sat, (int*)va, -1); + va_end(va); + return r; +} + +typedef struct { u8int x, m; } Pi; +static Pi *π; +static int nπ; +static u64int *πm; + +static void +pimp(u64int op, int n) +{ + int i, j, k; + u8int δ; + + nπ = 0; + for(i = 0; i < 1<> i & 1) != 0){ + π = realloc(π, sizeof(Pi) * (nπ + 1)); + π[nπ++] = (Pi){i, 0}; + } + for(i = 0; i < nπ; i++){ + for(j = 0; j < i; j++){ + δ = π[i].x ^ π[j].x; + if(δ == 0 || (δ & δ - 1) != 0 || π[i].m != π[j].m) continue; + if(((π[i].m | π[j].m) & δ) != 0) continue; + if(π[nπ-1].x == (π[i].x & π[j].x) && π[nπ-1].m == (π[i].m | δ)) continue; + π = realloc(π, sizeof(Pi) * (nπ + 1)); + π[nπ++] = (Pi){π[i].x & π[j].x, π[i].m | δ}; + } + } + for(i = k = 0; i < nπ; i++){ + for(j = i+1; j < nπ; j++) + if((π[i].m & ~π[j].m) == 0 && (π[i].x & ~π[j].m) == π[j].x) + break; + if(j == nπ) + π[k++] = π[i]; + } + nπ = k; + assert(nπ <= 1<> 1 & 0x5555555555555555ULL); + m = (m & 0x3333333333333333ULL) + (m >> 2 & 0x3333333333333333ULL); + m = (m & 0x0F0F0F0F0F0F0F0FULL) + (m >> 4 & 0x0F0F0F0F0F0F0F0FULL); + m = (m & 0x00FF00FF00FF00FFULL) + (m >> 8 & 0x00FF00FF00FF00FFULL); + m = (m & 0x0000FFFF0000FFFFULL) + (m >> 16 & 0x0000FFFF0000FFFFULL); + m = (u32int)m + (u32int)(m >> 32); + return m; +} + +static u64int +pimpcover(u64int op, int) +{ + int i, j, maxi, p, maxp; + u64int cov, yes, m; + + yes = 0; + cov = op; + for(i = 0; i < nπ; i++){ + if((yes & 1< maxp) + maxi = i, maxp = p; + } + assert(maxi >= 0); + yes |= 1<> j & 1) != 0 ? -a[j] : a[j]; +// for(i = 0; i < k; i++) print("%d ", cl[i]); print("\n"); + satadd1(sat, cl, k); + } + free(cl); +} + +int +satlogic1(SATSolve *sat, u64int op, int *a, int n) +{ + int i, j, o, r; + int s; + + if(n < 0) + for(n = 0; a[n] != 0; n++) + ; + assert(op >> (1<= 0; ){ + if((uint)(a[i] + 2) > 4){ + if(j >= 0) break; + j = i; + } + s = s << 1 | a[i] == 2 | a[i] == -1; + } + if(i < 0){ + if(j < 0) return 1 + (op >> s & 1); + o = op >> s & 1 | op >> s + (1<> 64-(1< +#include +#include +#include "dat.h" +#include "fns.h" + +char *astnames[] = { + [ASTINVAL] "ASTINVAL", + [ASTSYM] "ASTSYM", + [ASTNUM] "ASTNUM", + [ASTBIN] "ASTBIN", + [ASTUN] "ASTUN", + [ASTIDX] "ASTIDX", + [ASTTERN] "ASTTERN", + [ASTTEMP] "ASTTEMP", +}; + +char *opnames[] = { + [OPABS] "OPABS", + [OPADD] "OPADD", + [OPAND] "OPAND", + [OPASS] "OPASS", + [OPCOM] "OPCOM", + [OPCOMMA] "OPCOMMA", + [OPDIV] "OPDIV", + [OPEQ] "OPEQ", + [OPEQV] "OPEQV", + [OPGE] "OPGE", + [OPGT] "OPGT", + [OPIMP] "OPIMP", + [OPINVAL] "OPINVAL", + [OPLAND] "OPLAND", + [OPLE] "OPLE", + [OPLOR] "OPLOR", + [OPLSH] "OPLSH", + [OPLT] "OPLT", + [OPMOD] "OPMOD", + [OPMUL] "OPMUL", + [OPNEG] "OPNEG", + [OPNEQ] "OPNEQ", + [OPNOT] "OPNOT", + [OPOR] "OPOR", + [OPRSH] "OPRSH", + [OPSUB] "OPSUB", + [OPXOR] "OPXOR", +}; + +Trie *root; +Symbol *syms, **lastsymp = &syms; + +void * +emalloc(ulong sz) +{ + void *v; + + v = malloc(sz); + if(v == nil) sysfatal("malloc: %r"); + setmalloctag(v, getmalloctag(&sz)); + memset(v, 0, sz); + return v; +} + +void * +erealloc(void *v, ulong sz) +{ + v = realloc(v, sz); + if(v == nil) sysfatal("realloc: %r"); + setrealloctag(v, getmalloctag(&v)); + return v; +} + +static int +astfmt(Fmt *f) +{ + int t; + + t = va_arg(f->args, int); + if(t >= nelem(astnames) || astnames[t] == nil) + return fmtprint(f, "%d", t); + return fmtprint(f, "%s", astnames[t]); +} + +static int +opfmt(Fmt *f) +{ + int t; + + t = va_arg(f->args, int); + if(t >= nelem(opnames) || opnames[t] == nil) + return fmtprint(f, "%d", t); + return fmtprint(f, "%s", opnames[t]); +} + +static int +clz(uvlong v) +{ + int n; + + n = 0; + if(v >> 32 == 0) {n += 32; v <<= 32;} + if(v >> 48 == 0) {n += 16; v <<= 16;} + if(v >> 56 == 0) {n += 8; v <<= 8;} + if(v >> 60 == 0) {n += 4; v <<= 4;} + if(v >> 62 == 0) {n += 2; v <<= 2;} + if(v >> 63 == 0) {n += 1; v <<= 1;} + return n; +} + +static u64int +hash(char *s) +{ + u64int h; + + h = 0xcbf29ce484222325ULL; + for(; *s != 0; s++){ + h ^= *s; + h *= 0x100000001b3ULL; + } + return h; +} + +static Symbol * +trieget(uvlong hash) +{ + Trie **tp, *t, *s; + uvlong d; + + tp = &root; + for(;;){ + t = *tp; + if(t == nil){ + t = emalloc(sizeof(Symbol)); + t->hash = hash; + t->l = 64; + *tp = t; + return (Symbol *) t; + } + d = (hash ^ t->hash) & -(1ULL<<64 - t->l); + if(d == 0 || t->l == 0){ + if(t->l == 64) + return (Symbol *) t; + tp = &t->n[hash << t->l >> 64 - TRIEB]; + }else{ + s = emalloc(sizeof(Trie)); + s->hash = hash; + s->l = clz(d) & -TRIEB; + s->n[t->hash << s->l >> 64 - TRIEB] = t; + *tp = s; + tp = &s->n[hash << s->l >> 64 - TRIEB]; + } + } +} + +Symbol * +symget(char *name) +{ + uvlong h; + Symbol *s; + + h = hash(name); + while(s = trieget(h), s->name != nil && strcmp(s->name, name) != 0) + h++; + if(s->name == nil){ + s->name = strdup(name); + *lastsymp = s; + lastsymp = &s->next; + } + return s; +} + +void +trieprint(Trie *t, char *pref, int bits) +{ + int i; + + if(t == nil) {print("%snil\n", pref); return;} + if(t->l == 64) {print("%s%#.8p %.*llux '%s'\n", pref, t, (t->l - bits + 3) / 4, t->hash << bits >> bits >> 64 - t->l, ((Symbol*)t)->name); return;} + print("%s%#.8p %.*llux %d\n", pref, t, (t->l - bits + 3) / 4, t->hash << bits >> bits >> 64 - t->l, t->l); + for(i = 0; i < (1<n[i] == nil) continue; + print("%s%x:\n", pref, i); + trieprint(t->n[i], smprint("\t%s", pref), t->l); + } +} + +Node * +node(int t, ...) +{ + Node *n; + va_list va; + extern Line line; + + n = emalloc(sizeof(Node)); + n->type = t; + n->Line = line; + va_start(va, t); + switch(t){ + case ASTSYM: + n->sym = va_arg(va, Symbol *); + break; + case ASTNUM: + n->num = va_arg(va, mpint *); + break; + case ASTBIN: + n->op = va_arg(va, int); + n->n1 = va_arg(va, Node *); + n->n2 = va_arg(va, Node *); + break; + case ASTUN: + n->op = va_arg(va, int); + n->n1 = va_arg(va, Node *); + break; + case ASTIDX: + case ASTTERN: + n->n1 = va_arg(va, Node *); + n->n2 = va_arg(va, Node *); + n->n3 = va_arg(va, Node *); + break; + case ASTTEMP: + break; + default: + sysfatal("node: unknown type %α", t); + } + va_end(va); + return n; +} + +static int +triedesc(Trie *t, int(*f)(Symbol *, va_list), va_list va) +{ + int i, rc; + + if(t == nil) return 0; + if(t->l == 64) return f((Symbol *) t, va); + rc = 0; + for(i = 0; i < 1<n[i], f, va); + return rc; +} + +void +miscinit(void) +{ + fmtinstall(L'α', astfmt); + fmtinstall(L'O', opfmt); +} diff --git a/sys/src/cmd/forp/mkfile b/sys/src/cmd/forp/mkfile new file mode 100644 index 000000000..012e8e366 --- /dev/null +++ b/sys/src/cmd/forp/mkfile @@ -0,0 +1,14 @@ + +#include +#include +#include +#include +#include "dat.h" +#include "fns.h" + +Biobuf *bin; +Line line; +char lexbuf[512]; +int peektok; + +enum { + TEOF = -1, + TSYM = -2, + TNUM = -3, + TBIT = -4, + TOBVIOUSLY = -5, + TEQ = -6, + TNEQ = -7, + TLSH = -8, + TRSH = -9, + TLE = -10, + TGE = -11, + TLAND = -12, + TLOR = -13, + TASSUME = -14, + TIMP = -15, + TEQV = -16, + TSIGNED = -17, +}; + +typedef struct Keyword Keyword; +typedef struct Oper Oper; +struct Keyword { + char *name; + int tok; +}; +/* both tables must be sorted */ +static Keyword kwtab[] = { + "assume", TASSUME, + "bit", TBIT, + "obviously", TOBVIOUSLY, + "signed", TSIGNED, +}; +/* <=> is implemented through a hack below */ +static Keyword koptab[] = { + "!=", TNEQ, + "&&", TLAND, + "<<", TLSH, + "<=", TLE, + "==", TEQ, + "=>", TIMP, + ">=", TGE, + ">>", TRSH, + "||", TLOR, +}; +static Keyword *kwjmp[128]; +static Keyword *kopjmp[128]; +struct Oper { + int tok; + int type; + int pred; + char *str; +}; +#define MAXPREC 15 +static Oper optab[] = { + '*', OPMUL, 14, "*", + '/', OPDIV, 14, "/", + '%', OPMOD, 14, "%", + '+', OPADD, 13, "+", + '-', OPSUB, 13, "-", + TLSH, OPLSH, 12, "<<", + TRSH, OPRSH, 12, ">>", + '<', OPLT, 11, "<", + TLE, OPLE, 11, "<=", + '>', OPGT, 11, ">", + TGE, OPGE, 11, ">=", + TEQ, OPEQ, 10, "==", + TNEQ, OPNEQ, 10, "!=", + '&', OPAND, 9, "&", + '^', OPXOR, 8, "^", + '|', OPOR, 7, "|", + TLAND, OPLAND, 6, "&&", + TLOR, OPLOR, 5, "||", + TEQV, OPEQV, 4, "<=>", + TIMP, OPIMP, 4, "=>", + /* ?: */ + '=', OPASS, 2, "=", + ',', OPCOMMA, 1, ",", + -1, OPNOT, MAXPREC, "!", + -1, OPCOM, MAXPREC, "~", + -1, OPNEG, MAXPREC, "-", +}; + +void +error(Line *l, char *msg, ...) +{ + char buf[256]; + Fmt f; + va_list va; + + if(l == nil) l = &line; + fmtfdinit(&f, 2, buf, sizeof(buf)); + fmtprint(&f, "%s:%d: ", l->filen, l->lineno); + va_start(va, msg); + fmtvprint(&f, msg, va); + va_end(va); + fmtrune(&f, '\n'); + fmtfdflush(&f); + exits("error"); +} + +static int +tokfmt(Fmt *f) +{ + int t; + Keyword *k; + + t = va_arg(f->args, int); + if(t >= ' ' && t < 0x7f) return fmtprint(f, "%c", t); + for(k = kwtab; k < kwtab + nelem(kwtab); k++) + if(k->tok == t) + return fmtprint(f, "%s", k->name); + for(k = koptab; k < koptab + nelem(koptab); k++) + if(k->tok == t) + return fmtprint(f, "%s", k->name); + switch(t){ + case TSYM: return fmtprint(f, "TSYM"); break; + case TNUM: return fmtprint(f, "TNUM"); break; + case TEOF: return fmtprint(f, "eof"); break; + default: return fmtprint(f, "%d", t); break; + } +} + +static int +exprfmt(Fmt *f) +{ + Node *n; + Oper *o; + int w; + + n = va_arg(f->args, Node *); + if(n == nil) return fmtprint(f, "nil"); + switch(n->type){ + case ASTSYM: return fmtprint(f, "%s", n->sym->name); + case ASTBIN: + for(o = optab; o < optab + nelem(optab); o++) + if(o->type == n->op) + break; + if(o == optab + nelem(optab)) return fmtprint(f, "[unknown operation %O]", n->op); + w = f->width; + if(w > o->pred) fmtrune(f, '('); + fmtprint(f, "%*ε %s %*ε", o->pred, n->n1, o->str, o->pred + 1, n->n2); + if(w > o->pred) fmtrune(f, ')'); + return 0; + case ASTNUM: return fmtprint(f, "0x%B", n->num); + default: return fmtprint(f, "???(%α)", n->type); + } +} + +static int +issymchar(int c) +{ + return c >= 0 && (isalnum(c) || c == '_' || c >= 0x80); +} + +static int +lex(void) +{ + int c, d; + char *p; + Keyword *kw; + + if(peektok != 0){ + c = peektok; + peektok = 0; + return c; + } +loop: + do{ + c = Bgetc(bin); + if(c == '\n') line.lineno++; + }while(c >= 0 && isspace(c)); + if(c < 0) return TEOF; + if(c == '/'){ + c = Bgetc(bin); + if(c == '/'){ + do + c = Bgetc(bin); + while(c >= 0 && c != '\n'); + if(c < 0) return TEOF; + line.lineno++; + goto loop; + }else if(c == '*'){ + s0: + c = Bgetc(bin); + if(c != '*') goto s0; + s1: + c = Bgetc(bin); + if(c == '*') goto s1; + if(c != '/') goto s0; + goto loop; + }else{ + Bungetc(bin); + return '/'; + } + } + if(isdigit(c)){ + p = lexbuf; + *p++ = c; + while(c = Bgetc(bin), issymchar(c)) + if(p < lexbuf + sizeof(lexbuf) - 1) + *p++ = c; + Bungetc(bin); + *p = 0; + strtol(lexbuf, &p, 0); + if(p == lexbuf || *p != 0) + error(nil, "invalid number %q", lexbuf); + return TNUM; + } + if(issymchar(c)){ + p = lexbuf; + *p++ = c; + while(c = Bgetc(bin), issymchar(c)) + if(p < lexbuf + sizeof(lexbuf) - 1) + *p++ = c; + Bungetc(bin); + *p = 0; + c = lexbuf[0]; + if((signed char)c>= 0 && (kw = kwjmp[c], kw != nil)) + for(; kw < kwtab + nelem(kwtab) && kw->name[0] == c; kw++) + if(strcmp(lexbuf, kw->name) == 0) + return kw->tok; + return TSYM; + } + if(kw = kopjmp[c], kw != nil){ + d = Bgetc(bin); + for(; kw < koptab + nelem(koptab) && kw->name[0] == c; kw++) + if(kw->name[1] == d){ + if(kw->tok == TLE){ + c = Bgetc(bin); + if(c == '>') + return TEQV; + Bungetc(bin); + } + return kw->tok; + } + Bungetc(bin); + } + return c; +} + +static void +superman(int t) +{ + assert(peektok == 0); + peektok = t; +} + +static int +peek(void) +{ + if(peektok != 0) return peektok; + return peektok = lex(); +} + +static void +expect(int t) +{ + int s; + + s = lex(); + if(t != s) + error(nil, "expected %t, got %t", t, s); +} + +static int +got(int t) +{ + return peek() == t && (lex(), 1); +} + +static Node * +expr(int level) +{ + Node *a, *b, *c; + Oper *op; + Symbol *s; + mpint *num; + int t; + + if(level == MAXPREC+1){ + switch(t = lex()){ + case '~': return node(ASTUN, OPCOM, expr(level)); + case '!': return node(ASTUN, OPNOT, expr(level)); + case '+': return expr(level); + case '-': return node(ASTUN, OPNEG, expr(level)); + case '(': + a = expr(0); + expect(')'); + return a; + case TSYM: + s = symget(lexbuf); + switch(s->type){ + case SYMNONE: + error(nil, "%#q undefined", s->name); + default: + error(nil, "%#q symbol type error", s->name); + case SYMBITS: + break; + } + return node(ASTSYM, s); + case TNUM: + num = strtomp(lexbuf, nil, 0, nil); + return node(ASTNUM, num); + default: + error(nil, "unexpected %t", t); + } + }else if(level == MAXPREC){ + a = expr(level + 1); + if(got('[')){ + b = expr(0); + if(got(':')) + c = expr(0); + else + c = nil; + expect(']'); + a = node(ASTIDX, a, b, c); + } + return a; + }else if(level == 3){ + a = expr(level + 1); + if(got('?')){ + b = expr(level); + expect(':'); + c = expr(level); + a = node(ASTTERN, a, b, c); + } + return a; + } + a = expr(level+1); + for(;;){ + t = peek(); + for(op = optab; op < optab + nelem(optab); op++) + if(op->tok == t && op->pred >= level) + break; + if(op == optab+nelem(optab)) return a; + lex(); + a = node(ASTBIN, op->type, a, expr(level+1)); + } +} + +static void +vardecl(void) +{ + Symbol *s; + int l, flags; + + flags = 0; + for(;;) + switch(l = lex()){ + case TBIT: if((flags & 1) != 0) goto err; flags |= 1; break; + case TSIGNED: if((flags & 2) != 0) goto err; flags |= 2; break; + default: superman(l); goto out; + } +out: + do{ + expect(TSYM); + s = symget(lexbuf); + if(s->type != SYMNONE) error(nil, "%#q redefined", s->name); + s->type = SYMBITS; + if((flags & 2) != 0) + s->flags |= SYMFSIGNED; + s->size = 1; + if(got('[')){ + expect(TNUM); + s->type = SYMBITS; + s->size = strtol(lexbuf, nil, 0); + expect(']'); + } + s->vars = emalloc(sizeof(int) * s->size); + }while(got(',')); + expect(';'); + return; +err: error(nil, "syntax error"); +} + +static int +statement(void) +{ + Node *n; + int t; + + switch(t=peek()){ + case TEOF: + return 0; + case TBIT: + case TSIGNED: + vardecl(); + break; + case TASSUME: + case TOBVIOUSLY: + lex(); + n = expr(0); + expect(';'); + convert(n, -1); + if(t == TASSUME) + assume(n); + else + obviously(n); + break; + case ';': + lex(); + break; + default: + n = expr(0); + convert(n, -1); + expect(';'); + } + return 1; +} + +void +parsinit(void) +{ + Keyword *k; + + fmtinstall('t', tokfmt); + fmtinstall(L'ε', exprfmt); + for(k = kwtab; k < kwtab + nelem(kwtab); k++) + if(kwjmp[k->name[0]] == nil) + kwjmp[k->name[0]] = k; + for(k = koptab; k < koptab + nelem(koptab); k++) + if(kopjmp[k->name[0]] == nil) + kopjmp[k->name[0]] = k; +} + +void +parse(char *fn) +{ + if(fn == nil){ + bin = Bfdopen(0, OREAD); + line.filen = ""; + }else{ + bin = Bopen(fn, OREAD); + line.filen = strdup(fn); + } + if(bin == nil) sysfatal("open: %r"); + line.lineno = 1; + while(statement()) + ; +}