add forp
This commit is contained in:
aiju
parent
80474f7f59
commit
382d37dbf0
525
sys/src/cmd/forp/cvt.c
Normal file
525
sys/src/cmd/forp/cvt.c
Normal file
|
|
@ -0,0 +1,525 @@
|
|||
#include <u.h>
|
||||
#include <libc.h>
|
||||
#include <mp.h>
|
||||
#include <sat.h>
|
||||
#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<<i));
|
||||
continue;
|
||||
}
|
||||
for(j = 0; j < n1->size; j++){
|
||||
a = rn->vars[j];
|
||||
b = SVAR(rn, j + (1<<i));
|
||||
q = n2->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<<i ? rn->vars[j - (1<<i)] : 1;
|
||||
continue;
|
||||
}
|
||||
for(j = m; --j >= 0; ){
|
||||
a = rn->vars[j];
|
||||
b = j >= 1<<i ? rn->vars[j - (1<<i)] : 1;
|
||||
q = n2->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);
|
||||
}
|
||||
94
sys/src/cmd/forp/dat.h
Normal file
94
sys/src/cmd/forp/dat.h
Normal file
|
|
@ -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<<TRIEB];
|
||||
};
|
||||
|
||||
struct Symbol {
|
||||
TrieHead;
|
||||
char *name;
|
||||
int type;
|
||||
int size;
|
||||
int flags;
|
||||
int *vars;
|
||||
Symbol *next;
|
||||
};
|
||||
enum {
|
||||
SYMNONE,
|
||||
SYMBITS,
|
||||
};
|
||||
enum {
|
||||
SYMFSIGNED = 1,
|
||||
};
|
||||
|
||||
struct Node {
|
||||
int type;
|
||||
Line;
|
||||
int op;
|
||||
mpint *num;
|
||||
Symbol *sym;
|
||||
Node *n1, *n2, *n3;
|
||||
int size;
|
||||
int *vars;
|
||||
};
|
||||
enum {
|
||||
ASTINVAL,
|
||||
ASTSYM,
|
||||
ASTNUM,
|
||||
ASTBIN,
|
||||
ASTUN,
|
||||
ASTIDX,
|
||||
ASTTERN,
|
||||
ASTTEMP,
|
||||
};
|
||||
enum {
|
||||
OPINVAL,
|
||||
OPABS,
|
||||
OPADD,
|
||||
OPAND,
|
||||
OPASS,
|
||||
OPCOM,
|
||||
OPCOMMA,
|
||||
OPDIV,
|
||||
OPEQ,
|
||||
OPEQV,
|
||||
OPGE,
|
||||
OPGT,
|
||||
OPIMP,
|
||||
OPLAND,
|
||||
OPLE,
|
||||
OPLOR,
|
||||
OPLSH,
|
||||
OPLT,
|
||||
OPMOD,
|
||||
OPMUL,
|
||||
OPNEG,
|
||||
OPNEQ,
|
||||
OPNOT,
|
||||
OPOR,
|
||||
OPRSH,
|
||||
OPSUB,
|
||||
OPXOR,
|
||||
};
|
||||
|
||||
extern Symbol *syms;
|
||||
|
||||
#pragma varargck type "ε" Node*
|
||||
#pragma varargck type "α" int
|
||||
#pragma varargck type "O" int
|
||||
18
sys/src/cmd/forp/fns.h
Normal file
18
sys/src/cmd/forp/fns.h
Normal file
|
|
@ -0,0 +1,18 @@
|
|||
typedef struct SATSolve SATSolve;
|
||||
|
||||
void *emalloc(ulong);
|
||||
void *erealloc(void *, ulong);
|
||||
void parse(char *);
|
||||
void error(Line *, char *, ...);
|
||||
Node *node(int t, ...);
|
||||
Symbol *symget(char *);
|
||||
void convert(Node *, uint);
|
||||
void obviously(Node *);
|
||||
void go(int);
|
||||
void assume(Node *);
|
||||
int satand1(SATSolve *, int *, int);
|
||||
int satandv(SATSolve *, ...);
|
||||
int sator1(SATSolve *, int *, int);
|
||||
int satorv(SATSolve *, ...);
|
||||
int satlogic1(SATSolve *, u64int, int *, int);
|
||||
int satlogicv(SATSolve *, u64int, ...);
|
||||
159
sys/src/cmd/forp/forp.c
Normal file
159
sys/src/cmd/forp/forp.c
Normal file
|
|
@ -0,0 +1,159 @@
|
|||
#include <u.h>
|
||||
#include <libc.h>
|
||||
#include <mp.h>
|
||||
#include <sat.h>
|
||||
#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);
|
||||
}
|
||||
273
sys/src/cmd/forp/logic.c
Normal file
273
sys/src/cmd/forp/logic.c
Normal file
|
|
@ -0,0 +1,273 @@
|
|||
#include <u.h>
|
||||
#include <libc.h>
|
||||
#include <mp.h>
|
||||
#include <sat.h>
|
||||
#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<<n; i++)
|
||||
if((op >> 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<<n);
|
||||
}
|
||||
|
||||
static void
|
||||
pimpmask(void)
|
||||
{
|
||||
int i, j;
|
||||
u64int m;
|
||||
|
||||
πm = realloc(πm, sizeof(u64int) * nπ);
|
||||
for(i = 0; i < nπ; i++){
|
||||
m = 0;
|
||||
for(j = π[i].m; ; j = j - 1 & π[i].m){
|
||||
m |= 1ULL<<(π[i].x | j);
|
||||
if(j == 0) break;
|
||||
}
|
||||
πm[i] = m;
|
||||
}
|
||||
}
|
||||
|
||||
static int
|
||||
popcnt(u64int m)
|
||||
{
|
||||
m = (m & 0x5555555555555555ULL) + (m >> 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<<i) != 0) continue;
|
||||
m = πm[i];
|
||||
for(j = 0; j < nπ; j++){
|
||||
if(j == i) continue;
|
||||
m &= ~πm[j];
|
||||
if(m == 0) break;
|
||||
}
|
||||
if(j == nπ){
|
||||
yes |= 1<<i;
|
||||
cov &= ~πm[i];
|
||||
}
|
||||
}
|
||||
while(cov != 0){
|
||||
j = popcnt(~cov & cov - 1);
|
||||
maxi = -1;
|
||||
maxp = 0;
|
||||
for(i = 0; i < nπ; i++){
|
||||
if((πm[i] & 1<<j) == 0) continue;
|
||||
if((p = popcnt(πm[i] & cov)) > maxp)
|
||||
maxi = i, maxp = p;
|
||||
}
|
||||
assert(maxi >= 0);
|
||||
yes |= 1<<maxi;
|
||||
cov &= ~πm[maxi];
|
||||
}
|
||||
return yes;
|
||||
}
|
||||
|
||||
static void
|
||||
pimpsat(SATSolve *sat, u64int yes, int *a, int n, int r)
|
||||
{
|
||||
int i, j, k;
|
||||
int *cl;
|
||||
|
||||
cl = emalloc(sizeof(int) * (n + 1));
|
||||
while(yes != 0){
|
||||
i = popcnt(~yes & yes - 1);
|
||||
yes &= yes - 1;
|
||||
k = 0;
|
||||
cl[k++] = r;
|
||||
for(j = 0; j < n; j++)
|
||||
if((π[i].m & 1<<j) == 0)
|
||||
cl[k++] = (π[i].x >> 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<<n) == 0);
|
||||
s = 0;
|
||||
j = -1;
|
||||
for(i = n; --i >= 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<<j) - 1 & 2;
|
||||
switch(o){
|
||||
case 0: return 1;
|
||||
case 1: return -a[j];
|
||||
case 2: return a[j];
|
||||
case 3: return 2;
|
||||
}
|
||||
}
|
||||
r = satvar++;
|
||||
pimp(op, n);
|
||||
pimpmask();
|
||||
pimpsat(sat, pimpcover(op, n), a, n, r);
|
||||
op ^= (u64int)-1 >> 64-(1<<n);
|
||||
pimp(op, n);
|
||||
pimpmask();
|
||||
pimpsat(sat, pimpcover(op, n), a, n, -r);
|
||||
return r;
|
||||
}
|
||||
|
||||
int
|
||||
satlogicv(SATSolve *sat, u64int op, ...)
|
||||
{
|
||||
va_list va;
|
||||
int r;
|
||||
|
||||
va_start(va, op);
|
||||
r = satlogic1(sat, op, (int*)va, -1);
|
||||
va_end(va);
|
||||
return r;
|
||||
}
|
||||
246
sys/src/cmd/forp/misc.c
Normal file
246
sys/src/cmd/forp/misc.c
Normal file
|
|
@ -0,0 +1,246 @@
|
|||
#include <u.h>
|
||||
#include <libc.h>
|
||||
#include <mp.h>
|
||||
#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<<TRIEB); i++){
|
||||
if(t->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<<TRIEB; i++)
|
||||
rc += triedesc(t->n[i], f, va);
|
||||
return rc;
|
||||
}
|
||||
|
||||
void
|
||||
miscinit(void)
|
||||
{
|
||||
fmtinstall(L'α', astfmt);
|
||||
fmtinstall(L'O', opfmt);
|
||||
}
|
||||
14
sys/src/cmd/forp/mkfile
Normal file
14
sys/src/cmd/forp/mkfile
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
</$objtype/mkfile
|
||||
|
||||
BIN=/$objtype/bin
|
||||
TARG=forp
|
||||
OFILES=\
|
||||
forp.$O\
|
||||
parse.$O\
|
||||
misc.$O\
|
||||
cvt.$O\
|
||||
logic.$O\
|
||||
|
||||
HFILES=dat.h fns.h
|
||||
|
||||
</sys/src/cmd/mkone
|
||||
454
sys/src/cmd/forp/parse.c
Normal file
454
sys/src/cmd/forp/parse.c
Normal file
|
|
@ -0,0 +1,454 @@
|
|||
#include <u.h>
|
||||
#include <libc.h>
|
||||
#include <bio.h>
|
||||
#include <ctype.h>
|
||||
#include <mp.h>
|
||||
#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 = "<stdin>";
|
||||
}else{
|
||||
bin = Bopen(fn, OREAD);
|
||||
line.filen = strdup(fn);
|
||||
}
|
||||
if(bin == nil) sysfatal("open: %r");
|
||||
line.lineno = 1;
|
||||
while(statement())
|
||||
;
|
||||
}
|
||||
Loading…
Reference in a new issue