📄 uno_bounds.c
字号:
/***** uno: uno_bounds.c *****//* Copyright (c) 2000-2003 by Lucent Technologies - Bell Laboratories *//* All Rights Reserved. This software is for educational purposes only. *//* Permission is given to distribute this code provided that this intro- *//* ductory message is not removed and no monies are exchanged. *//* No guarantee is expressed or implied by the distribution of this code. *//* Software written by Gerard J. Holzmann based on the public domain *//* ANSI-C parser Ctree Version 0.14 from Shaun Flisakowski */#include <stdio.h>#include <string.h>#include "symtab.h"#include "uno_lts.h"#include "gram.h"static int debug = 0;static BoundStack *boundstack = (BoundStack *) 0;static BoundStack *freestack = (BoundStack *) 0;static ArBound *bounded = (ArBound *) 0;static ArBound *freebounds = (ArBound *) 0;static ArSize *arsize = (ArSize *) 0, *freears = (ArSize *) 0;static ArSize *arnosize = (ArSize *) 0; int nogood;static int size_seen, size_notfound, size_outofscope, size_is_simple, simple_checked, size_other;static int size_dunno, size_deref, size_zero, size_zero_resolved, simple_known; int size_ok, size_nok;extern int check_bounds(ArBound *, int, treenode *);extern int infeasible(treenode *, treenode *);extern int merge_bounds(ArBound *, ArBound *);extern int same_bounds(ArBound *, ArBound *);extern int uno_ignore(symentry_t *);extern void negate_bound(ArBound *);extern void uno_assert(int, char *);extern int eval_fct(treenode *, treenode *);extern void print_recur(treenode *, FILE *);extern void dump_defuse(DefUse *, FILE *);extern char *toksym(int, int);extern int unsatisfiable(ArBound *);extern State *uno_prop;void explain_bound(char *, ArBound *, treenode *);extern int Verbose, depth, uno, lintlike;extern void could_be_fct(char *);static intcount_leafs(treenode *n){ if (!n) return 0; if (n->hdr.which == LEAF_T) { if (n->hdr.type == TN_IDENT) could_be_fct(((leafnode*)n)->data.sval->str); return 1; } return count_leafs(n->lnode)+count_leafs(n->rnode);}static inthas_right_decl(symentry_t *s, treenode *n){ if (n->hdr.type == TN_ARRAY_DECL && n->lnode->hdr.type == TN_IDENT && ((leafnode *)(n->lnode))->syment == s) return 1; if (n->hdr.type == TN_DECL && n->lnode->hdr.type == TN_PNTR && has_right_decl(s, n->rnode)) return 1; return 0;}static intfind_ininode(symentry_t *s, treenode *n){ /* find a TN_ASSIGN with lnode equal to b and rnode TN_INIT_BLK */ if (!n || n->hdr.which == LEAF_T) return 0; if (n->hdr.type == TN_ASSIGN && n->rnode->hdr.type == TN_INIT_BLK && has_right_decl(s, n->lnode)) return count_leafs(n->rnode); return find_ininode(s, n->lnode) + find_ininode(s, n->rnode);}static ArSize *getars(void){ ArSize *a; if (freears) { a = freears; freears = freears->nxt; memset(a, 0, sizeof(ArSize)); } else a = (ArSize *) emalloc(sizeof(ArSize)); return a;}static voidadd_size(symentry_t *s, treenode *b, treenode *n){ ArSize *a; int cnt; leafnode *q; for (a = arsize; a; a = a->nxt) if (a->s == s) return; if (!b) { if (cnt = find_ininode(s, n)) { size_zero_resolved++; if (debug > 1) printf("uno: static initializer for %s\tresolved: %d\n", s->nme->str, cnt); q = (leafnode *) emalloc(sizeof(leafnode)); q->hdr.which = LEAF_T; q->hdr.type = TN_INT; q->data.ival = cnt; b = (treenode *) q; } else { size_zero++; if (debug > 1) printf("uno: zerobound %s\tnot resolved\n", s->nme->str); return; } } a = getars(); a->s = s; a->b = b; a->nxt = arsize; arsize = a;}static treenode *find_size(symentry_t *s, treenode *nn){ ArSize *a, *r; int cnt = 0; if (!s) return ZT; for (a = arsize; a; a = a->nxt) { if (a->s == s) return a->b; else if (strcmp(a->s->nme->str, s->nme->str) == 0 && a->s->decl_level == s->decl_level) { cnt++; r = a;#if 0 printf("same name %s, different symbol:\n", s->nme->str); printf(" level %d %d\n", a->s->decl_level, s->decl_level); printf(" line %d %d\n", a->s->ln, s->ln); printf(" scopetab %u %u\n", a->s->nes, s->nes); printf(" tree %u %u\n", a->s->node, s->node); printf(" tree ln %u %u\n", a->s->node->hdr.line, s->node->hdr.line);#endif } } if (cnt == 1) return r->b; /* uno can't tell that r is initialized here */ for (a = arnosize; a; a = a->nxt) if (strcmp(a->s->nme->str, s->nme->str) == 0) break; /* somehow the symentry's may differ */ if (!a) { a = getars(); a->s = s; a->nxt = arnosize; arnosize = a; /* avoid reporting more than once */ if (Verbose) printf("uno: %s:%d could not determine array bound for %s\n", nn->hdr.fnm, nn->hdr.line, s->nme->str); size_other++; } return ZT;}inthas_node_type(treenode *n, int t){ if (!n) return 0; if (n->hdr.type == t) return 1; if (n->hdr.which == LEAF_T) return 0; return (has_node_type(n->lnode, t) || has_node_type(n->rnode, t));}static symentry_t *simple_node_type(treenode *n){ if (n && n->hdr.type == TN_IDENT) return n->syment; return (symentry_t *) 0;}inteval_const_expr(treenode *n, treenode *m){ int a=0, b=0; extern int get_state_val(void); extern char *statename; if (!n) return 0; if (n->hdr.type == TN_INT) return ((leafnode *)n)->data.ival; if (n->hdr.type == TN_IDENT) { if (strcmp(((leafnode *)n)->data.sval->str, statename) == 0) return get_state_val(); } if (uno_prop && n->hdr.type == TN_FUNC_CALL) { return eval_fct(n, m); } if (n->hdr.type == TN_EXPR) { if (n->lnode) a = eval_const_expr(n->lnode, m); if (n->rnode) b = eval_const_expr(n->rnode, m); if (!nogood) switch (n->hdr.tok) { case NOT: return !b; case B_NOT: return ~b; case CASE: return b; case PLUS: return a+b; case MINUS: return a-b; case STAR: return a*b; case DIV: if (b == 0) { fprintf(stderr, "uno: %s:%d division by zero error\n", n->hdr.fnm, n->hdr.line); break; } return a/b; case MOD: if (b == 0) { fprintf(stderr, "uno: %s:%d division by zero error\n", n->hdr.fnm, n->hdr.line); break; } return a%b; case EQUAL: return (a == b); case LESS: return (a < b); case LESS_EQ: return (a <= b); case GRTR: return (a > b); case GRTR_EQ: return (a >= b); case NOT_EQ: return (a != b); case AND: return (a && b); case OR: return (a || b); case B_OR: return (a | b); case B_AND: return (a & b); case B_XOR: return (a ^ b); case B_NOT_EQ: return (a != b); case L_SHIFT: return (a << b); case R_SHIFT: return (a >> b); default: printf("saw token type: %s (%s)\n", (char *) toksym(n->hdr.tok,0), x_stmnt(n)); break; } } nogood = 1; return 0;}static inteval_cond(treenode *a, treenode *b) /* is a < b ? */{ int ix, bnd; nogood = 0; ix = eval_const_expr(a, ZT); if (ix < 0) return 0; /* definitely wrong */ bnd = eval_const_expr(b, ZT); if (nogood) return -2; /* can't tell */ if (ix == bnd) return -1; /* equal to bound */ return (ix < bnd); /* satisfied */}static Stack *v_reps = (Stack *) 0;intv_matched(treenode *n){ Stack *w; for (w = v_reps; w; w = w->nxt) if (n == w->n) return 1; return 0;}intv_reported(treenode *n){ Stack *w; if (v_matched(n)) return 1; w = (Stack *) emalloc(sizeof(Stack)); w->n = n; w->nxt = v_reps; v_reps = w; return 0;}static voidana_aio_ix(State *s, treenode *tn){ treenode *nn = s->n; treenode *n; symentry_t *v; ArBound *b; int x = -2; if (tn->lnode->hdr.type != TN_IDENT /* basename is not simple */ || tn->hdr.type != TN_INDEX) /* decls are handled elsewhere */ return; if (debug>1) { printf("uno: ana_aio for %s\t(stmnt %s)\tbase:", tn->lnode->syment->nme->str, x_stmnt(nn)); print_recur(tn->lnode, stdout); printf("\tindex: "); print_recur(tn->rnode, stdout); printf("\n"); } size_seen++; if (has_node_type(tn->rnode, TN_DEREF)) { if (debug>1) printf(" cannot handle\n"); size_deref++; return; } if (!(n = find_size(tn->lnode->syment, nn))) /* assign */ { if (debug>1) printf(" no bound\n"); size_notfound++; return; } if (has_node_type(tn->rnode, TN_IDENT)) { if (!(v = simple_node_type(tn->rnode))) /* assignment */ { if (debug>1) printf(" not simple\n"); size_outofscope++; } else { size_is_simple++; if (debug>1) printf(" simple\n"); nogood = 0; x = eval_const_expr(n, ZT); if (nogood) { if (debug>1) printf("\tsimple bound, but no simple size\n"); size_outofscope++; } else { simple_checked++; if (debug>1) { printf("\tsimple bound for %s\t(stmnt %s)\tbase:", tn->lnode->syment->nme->str, x_stmnt(nn)); print_recur(tn->lnode, stdout); printf("\tindex: "); print_recur(tn->rnode, stdout); printf("\n"); if (!boundstack->curbounds) printf(" no known bounds\n"); } for (b = boundstack->curbounds; b; b = b->nxt) { if (debug>1) explain_bound("Known:", b, nn); if (b->s == v && !(b->bounds & UNK)) { /* the value of v has to be >= 0 and <= x */ simple_known++; /* should equal simple_checked */ check_bounds(b, x, nn); break; } } if (debug>1) { if (!b) { printf("simple check for %s, but no known bound\n", v->nme->str); for (b = boundstack->curbounds; b; b = b->nxt) explain_bound("knew:", b, nn); } } } } } else { x = eval_cond(tn->rnode, n); if (x == 1) /* satisfied */ { if (debug>1) printf(" satisfied.\n");isok: size_ok++; return; } if (x == -1) /* equal to bound */ { /* likely used to find end of array */ if (lintlike) goto nok; else goto isok; } if (x == 0) /* not satisfied */ {nok: if (!v_reported(tn)) { fprintf(stderr, "uno: %s:%4d array index error '%s", tn->hdr.fnm, tn->hdr.line, x_stmnt(tn->lnode)); fprintf(stderr, "[%s]'", x_stmnt(tn->rnode)); fprintf(stderr, " (array-size: %s)\n", x_stmnt(n)); size_nok++; } return; } /* else cannot tell */ if (debug>1) printf(" cannot tell\n"); size_dunno++; } /* else cannot tell */ if (debug>1) { printf("uno: %s:%4d bound-check %s", tn->hdr.fnm, tn->hdr.line, x_stmnt(tn->lnode)); printf("[ %s", x_stmnt(tn->rnode)); printf(" < %s ? ]\n", x_stmnt(n)); /* within bound? */ }}static voidana_aio_decl(SymList *s, treenode *tn, treenode *nn){ if (!tn) return; if (tn->hdr.type == TN_DECL && tn->rnode && tn->lnode && tn->lnode->hdr.type == TN_PNTR) { ana_aio_decl(s, tn->rnode, nn); return; } if (tn->hdr.type == TN_ARRAY_DECL && tn->lnode->hdr.type == TN_IDENT && tn->lnode->syment == s->sm) { add_size(s->sm, tn->rnode, nn); if (debug>1) { printf("uno: set bound ana_aio for %s\n", s->sm->nme->str); printf("uno: %s:%d basename %s", tn->hdr.fnm, tn->hdr.line, x_stmnt(tn->lnode)); printf("[ %s ]\t", x_stmnt(tn->rnode)); printf("=====%s\n\t", name_of_node(nn->hdr.type)); print_recur(nn, stdout); printf("\n"); } }}static ArBound *uno_freshbound(void){ ArBound *b; if (freebounds) { b = freebounds; freebounds = freebounds->nxt; b->sameas = (symentry_t *) 0; b->dup = (ArBound *) 0; b->nxt = (ArBound *) 0; } else b = (ArBound *) emalloc(sizeof(ArBound)); b->level_set = depth; return b;}static ArBound *loose_bound(symentry_t *s, int lb, int ub, int bounds){ ArBound *b; uno_assert((int) s, "saw bound without name"); b = uno_freshbound(); b->s = s; b->ub = ub; b->lb = lb; b->bounds = bounds; return b;}static ArBound *add_bound(symentry_t *s, int lb, int ub, int bounds){ ArBound *b; if (!s) return (ArBound *) 0; /* probably undeclared var such as 'errno' */ for (b = bounded; b; b = b->nxt) /* record best guess at values of vars */ if (b->s == s && !(b->bounds & UNK)) { if (bounds & FROMASGN) /* new bound is definitive */ { if (debug>1) printf(" old bound on %s removed\n", s->nme->str); b->bounds |= UNK; /* continue, there may be more */ } else if (b->bounds & FROMASGN) /* and bounds&FORMEXPR */ { if (debug>1) printf(" ignore new non-asgn bound on %s\n", s->nme->str); /* new bound was not from asgn */ return (ArBound *) 0; /* already have a definitive value */ } } b = loose_bound(s, lb, ub, bounds); /* this can add multiple FROMEXPR bounds on a var */ b->nxt = bounded; bounded = b; return b;}static ArBound *bound_from_asgn(symentry_t *s, treenode *nn){ ArBound *b = (ArBound *) 0; int n; if (!nn || !nn->lnode || nn->lnode->hdr.type != TN_IDENT || (nn->lnode->syment != s && s)) return b; if (nn->rnode->hdr.type == TN_IDENT) { /* see if we have a bound on this ident already * if so, copy the bounds over to the lnode var */ if (s != nn->rnode->syment) { b = add_bound(nn->lnode->syment, 0, 0, DUP|FROMASGN); b->sameas = nn->rnode->syment; /* b->dup set later in fix_dups */ } } else { nogood = 0; n = eval_const_expr(nn->rnode, ZT); if (!nogood) b = add_bound(nn->lnode->syment, n, n+1, (LB|UB|FROMASGN)); } if (debug && b) printf("UU: set bound from asignment\n"); return b;}static ArBound *uno_dig(symentry_t *s, treenode *n){ ArBound *b = (ArBound *) 0; switch (n->hdr.type) { case TN_ASSIGN: b = bound_from_asgn(s, n); break; case TN_DECL: case TN_DECLS: b = uno_dig(s, n->lnode); if (!b) b = uno_dig(s, n->rnode); break; } return b;}static voiddual_work(State *z){ SymList *s; leafnode *l; ArBound *b; treenode *n;
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -