X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/361091ccc3ff7e62a4817ef6400e752fef38f3c2..7a8641bf3e56e9e557f91056dfcd128326ebfd33:/src/constraintTerm.c?ds=sidebyside diff --git a/src/constraintTerm.c b/src/constraintTerm.c index 8f2418e..f083460 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -1,202 +1,324 @@ +/* +** Splint - annotation-assisted static program checker +** Copyright (C) 1994-2003 University of Virginia, +** Massachusetts Institute of Technology +** +** This program is free software; you can redistribute it and/or modify it +** under the terms of the GNU General Public License as published by the +** Free Software Foundation; either version 2 of the License, or (at your +** option) any later version. +** +** This program is distributed in the hope that it will be useful, but +** WITHOUT ANY WARRANTY; without even the implied warranty of +** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +** General Public License for more details. +** +** The GNU General Public License is available from http://www.gnu.org/ or +** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, +** MA 02111-1307, USA. +** +** For information on splint: info@splint.org +** To report a bug: splint-bug@splint.org +** For more information: http://www.splint.org +*/ + /* ** constraintTerm.c */ +/* #define DEBUGPRINT 1 */ + # include /* for isdigit */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "basic.h" # include "cgrammar.h" # include "cgrammar_tokens.h" # include "exprChecks.h" -# include "aliasChecks.h" # include "exprNodeSList.h" -# include "exprData.i" -int constraintTerm_getValue (constraintTerm term) +bool constraintTerm_isDefined (constraintTerm t) { - if (term->kind == EXPRNODE) - { - return (multiVal_forceInt (term->value.expr->val) ); - } - if (term->kind == INTLITERAL ) + return t != NULL; +} + +void constraintTerm_free (/*@only@*/ constraintTerm term) +{ + llassert (constraintTerm_isDefined (term)); + + fileloc_free (term->loc); + + switch (term->kind) { - return (term->value.intlit); + case CTT_EXPR: + /* we don't free an exprNode*/ + break; + case CTT_SREF: + /* sref */ + sRef_free (term->value.sref); + break; + case CTT_INTLITERAL: + /* don't free an int */ + break; + case CTT_ERRORBADCONSTRAINTTERMTYPE: + default: + /* type was set incorrectly */ + llcontbug (message("constraintTerm_free type was set incorrectly")); } - llassert(FALSE); - return 0; + + term->kind = CTT_ERRORBADCONSTRAINTTERMTYPE; + free (term); } -/*@out@*/ static constraintTerm new_constraintTermExpr (void) +/*@only@*/ static/*@out@*/ constraintTerm new_constraintTermExpr (void) { constraintTerm ret; ret = dmalloc (sizeof (* ret ) ); + ret->value.intlit = 0; return ret; } -constraintTerm constraintTerm_simplify (constraintTerm term) + +bool constraintTerm_isIntLiteral (constraintTerm term) { - if (term->constrType == VALUE) + llassert(term != NULL); + + if (term->kind == CTT_INTLITERAL) + return TRUE; + + return FALSE; +} + + +bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ +{ + llassert (c != NULL); + + if (c->kind == CTT_EXPR) { - if (term->kind == EXPRNODE) + if (exprNode_isInitBlock (c->value.expr)) { - if ( exprNode_knownIntValue (term->value.expr ) ) - { - int temp; - temp = exprNode_getLongValue (term->value.expr); - term->value.intlit = temp; - term->kind = INTLITERAL; - } - + return TRUE; } + } + return FALSE; +} + +bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ +{ + llassert (c != NULL); + + if (c->kind == CTT_EXPR) + { + return TRUE; } - return term; + return FALSE; } -constraintTerm constraintTerm_copy (constraintTerm term) +/*@access exprNode@*/ +int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ { - constraintTerm ret; - ret = new_constraintTermExpr(); - ret->constrType = term->constrType; - ret->loc = fileloc_copy (term->loc); - ret->value= term->value; - ret->kind = term->kind; - return ret; + exprNodeList list; + int ret; + llassert (c != NULL); + llassert (constraintTerm_isInitBlock (c) ); + llassert (c->kind == CTT_EXPR); + + llassert(exprNode_isDefined(c->value.expr) ); + + if (exprNode_isUndefined(c->value.expr) ) + { + return 1; + } + + if (c->value.expr->edata == exprData_undefined) + { + return 1; + } + list = exprData_getArgs(c->value.expr->edata); + + ret = exprNodeList_size(list); + + return ret; } +/*@noaccess exprNode@*/ + -constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e) +bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/ { - constraintTerm ret = new_constraintTermExpr(); - ret->loc = exprNode_getfileloc(e); - ret->value.expr = e; - ret->kind = EXPRNODE; - return ret; + llassert (c != NULL); + if (c->kind == CTT_EXPR) + { + if (exprNode_knownStringValue(c->value.expr) ) + { + return TRUE; + } + } + return FALSE; } -constraintTerm constraintTerm_makeMaxSetexpr (exprNode e) + +cstring constraintTerm_getStringLiteral (constraintTerm c) { - constraintTerm ret; - ret = exprNode_makeConstraintTerm (e); - ret->constrType = MAXSET; - return ret; + llassert (c != NULL); + llassert (constraintTerm_isStringLiteral (c) ); + llassert (c->kind == CTT_EXPR); + + return (cstring_copy ( multiVal_forceString (exprNode_getValue (c->value.expr) ) ) ); } -constraintTerm constraintTerm_makeMinSetexpr (exprNode e) +constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@modifies term@*/ { - constraintTerm ret; - ret = exprNode_makeConstraintTerm (e); - ret->constrType = MINSET; - return ret; + if (term->kind == CTT_EXPR) + { + if ( exprNode_knownIntValue (term->value.expr ) ) + { + long int temp; + + temp = exprNode_getLongValue (term->value.expr); + term->value.intlit = (int)temp; + term->kind = CTT_INTLITERAL; + } + } + return term; } -constraintTerm constraintTerm_makeMaxReadexpr (exprNode e) +fileloc constraintTerm_getFileloc (constraintTerm t) { - constraintTerm ret; - ret = exprNode_makeConstraintTerm (e); - ret->constrType = MAXREAD; - return ret; + llassert (constraintTerm_isDefined (t)); + return (fileloc_copy (t->loc) ); } -constraintTerm constraintTerm_makeMinReadexpr (exprNode e) +constraintTermType constraintTerm_getKind (constraintTerm t) { - constraintTerm ret; - ret = exprNode_makeConstraintTerm (e); - ret->constrType = MINREAD; - return ret; + llassert (constraintTerm_isDefined(t) ); + + return (t->kind); } -constraintTerm constraintTerm_makeValueexpr (exprNode e) +/*@exposed@*/ sRef constraintTerm_getSRef (constraintTerm t) { - constraintTerm ret; - ret = exprNode_makeConstraintTerm (e); - ret->constrType = VALUE; - ret = constraintTerm_simplify (ret); - return ret; + llassert (constraintTerm_isDefined(t) ); + llassert (t->kind == CTT_SREF); + + return (t->value.sref); } +/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/ exprNode e) +{ + constraintTerm ret = new_constraintTermExpr(); + ret->loc = fileloc_copy(exprNode_getfileloc(e)); + ret->value.expr = e; + ret->kind = CTT_EXPR; + ret = constraintTerm_simplify(ret); + return ret; +} -constraintTerm intLit_makeConstraintTerm (int i) +/*@only@*/ constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef s) { constraintTerm ret = new_constraintTermExpr(); - ret->value.intlit = i; - ret->kind = INTLITERAL; ret->loc = fileloc_undefined; + ret->value.sref = sRef_saveCopy(s); + ret->kind = CTT_SREF; + ret = constraintTerm_simplify(ret); return ret; } -constraintTerm constraintTerm_makeIntLitValue (int i) + +constraintTerm constraintTerm_copy (constraintTerm term) { constraintTerm ret; - ret = intLit_makeConstraintTerm (i); - ret->constrType = VALUE; + ret = new_constraintTermExpr(); + ret->loc = fileloc_copy (term->loc); + + switch (term->kind) + { + case CTT_EXPR: + ret->value.expr = term->value.expr; + break; + case CTT_INTLITERAL: + ret->value.intlit = term->value.intlit; + break; + + case CTT_SREF: + ret->value.sref = sRef_saveCopy(term->value.sref); + break; + default: + BADEXIT; + } + ret->kind = term->kind; return ret; - } -/* constraintTerm constraintTerm_makeMinSetexpr (int i) */ -/* { */ -/* constraintTerm ret; */ -/* ret = intLit_makeConstraintTerm (i); */ -/* ret->constrType = MINSET; */ -/* } */ - -/* constraintTerm constraintTerm_makeMaxReadexpr (int i) */ -/* { */ -/* constraintTerm ret; */ -/* ret = intLit_makeConstraintTerm (i); */ -/* ret->constrType = MAXREAD; */ -/* } */ -/* constraintTerm constraintTerm_makeMinReadexpr (int i) */ -/* { */ -/* constraintTerm ret; */ -/* ret = exprNode_makeConstraintTerm (i); */ -/* ret->constrType = MINREAD; */ -/* } */ +constraintTerm constraintTerm_setFileloc (/*@returned@*/ constraintTerm term, fileloc loc) +{ + llassert(term != NULL); + if ( fileloc_isDefined( term->loc ) ) + fileloc_free(term->loc); + term->loc = fileloc_copy(loc); + return term; +} -cstring constraintType_print (constraintType constrType) +static cstring constraintTerm_getName (constraintTerm term) { - cstring st = cstring_undefined; + cstring s; + s = cstring_undefined; - switch (constrType) + llassert (term != NULL); + + switch (term->kind) { - case VALUE: - st = cstring_makeLiteral("VALUE"); - break; - case CALLSAFE: - st = cstring_makeLiteral("CALLSAFE"); + case CTT_EXPR: + + s = message ("%s", exprNode_unparse (term->value.expr) ); break; - case MAXSET: - st = cstring_makeLiteral ("MAXSET"); + case CTT_INTLITERAL: + s = message (" %d ", (int) term->value.intlit); break; - case MINSET: - st = cstring_makeLiteral ("MINSET"); + + case CTT_SREF: + s = message ("%q", sRef_unparse (term->value.sref) ); + break; - case MAXREAD: - st = cstring_makeLiteral ("MAXREAD"); + default: + BADEXIT; + /*@notreached@*/ break; - case MINREAD: - st = cstring_makeLiteral ("MINREAD"); + } + + return s; +} + +constraintTerm +constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeList arglist) /*@modifies term@*/ +{ + llassert (term != NULL); + + switch (term->kind) + { + case CTT_EXPR: + break; - case NULLTERMINATED: - st = cstring_makeLiteral ("NULLTERMINATED"); + case CTT_INTLITERAL: break; - case UNDEFINED: - st = cstring_makeLiteral (("Unhandled value for constraintType")); - llassert(FALSE); + + case CTT_SREF: + term->value.sref = sRef_fixBaseParam (term->value.sref, arglist); break; default: - st = cstring_makeLiteral (("Unhandled value for constraintType")); - llassert(FALSE); + BADEXIT; } - return st; + return term; + } -cstring constraintTerm_print (constraintTerm term) + +cstring constraintTerm_unparse (constraintTerm term) /*@*/ { cstring s; s = cstring_undefined; @@ -205,57 +327,460 @@ cstring constraintTerm_print (constraintTerm term) switch (term->kind) { - case EXPRNODE: - /*@i334*/ //wtf - s = message ("%s @ %s ", exprNode_unparse (term->value.expr), + case CTT_EXPR: + + s = message ("%s @ %q", exprNode_unparse (term->value.expr), fileloc_unparse (term->loc) ); break; - case INTLITERAL: - { - s = message (" %d ", term->value.intlit); + case CTT_INTLITERAL: + s = message ("%d", (int)term->value.intlit); break; - } - case SREF: - s = cstring_makeLiteral("Not Implemented\n"); - llassert(FALSE); + + case CTT_SREF: + s = message ("%q", sRef_unparseDebug (term->value.sref) ); + break; + default: + BADEXIT; } - s = message (" %s %s ", constraintType_print (term->constrType), s); - return s; + return s; } +constraintTerm constraintTerm_makeIntLiteral (long i) +{ + constraintTerm ret = new_constraintTermExpr(); + ret->value.intlit = i; + ret->kind = CTT_INTLITERAL; + ret->loc = fileloc_undefined; + return ret; +} -bool constraintTerm_same (constraintTerm term1, constraintTerm term2) +bool constraintTerm_canGetValue (constraintTerm term) { - llassert (term1 !=NULL && term2 !=NULL); + if (term->kind == CTT_INTLITERAL) + { + return TRUE; + } + else if (term->kind == CTT_SREF) + { + if (sRef_hasValue (term->value.sref)) + { + multiVal mval = sRef_getValue (term->value.sref); - if (term1->constrType != term2->constrType) + return multiVal_isInt (mval); /* for now, only try to deal with int values */ + } + else + { + return FALSE; + } + } + else if (term->kind == CTT_EXPR) { return FALSE; } - if ( (term1->kind != term2->kind) || (term1->kind != EXPRNODE) ) + else { return FALSE; } - - DPRINTF ( (message +} + +long constraintTerm_getValue (constraintTerm term) +{ + llassert (constraintTerm_canGetValue (term)); + + if (term->kind == CTT_INTLITERAL) + { + return term->value.intlit; + } + else if (term->kind == CTT_SREF) + { + if (sRef_hasValue (term->value.sref)) + { + multiVal mval = sRef_getValue (term->value.sref); + + return multiVal_forceInt (mval); /* for now, only try to deal with int values */ + } + else + { + BADBRANCH; + } + } + else if (term->kind == CTT_EXPR) + { + BADBRANCH; + } + else + { + BADBRANCH; + } + + BADEXIT; +} + +/*drl added this 10.30.001 + */ + +/*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t) +{ + llassert (t != NULL); + + llassert (t->kind == CTT_EXPR); + + return t->value.expr; + +} + + /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t) +{ + llassert (t != NULL); + if (t->kind == CTT_EXPR) + { + return exprNode_getSref(t->value.expr); + } + + if (t->kind == CTT_SREF) + { + return t->value.sref; + } + + return sRef_undefined; +} + +bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2) +{ + cstring s1, s2; + + llassert (term1 !=NULL && term2 !=NULL); + + DPRINTF ((message ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2) ) ) ); - - if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) ) - { - TPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + + s1 = constraintTerm_getName (term1); + s2 = constraintTerm_getName (term2); + + if (cstring_equal (s1, s2) ) + { + DPRINTF ((message (" %q and %q are same", s1, s2 ) ) ); return TRUE; } - else - { - TPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + else + { + DPRINTF ((message (" %q and %q are not same", s1, s2 ) ) ); return FALSE; - } - + } +} + +bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) +{ + sRef s1, s2; + + llassert (term1 !=NULL && term2 !=NULL); + + if (constraintTerm_canGetValue (term1) && constraintTerm_canGetValue (term2)) + + /*3/30/2003 comment updated to reflect name change form INTLITERAL to CTT_INTLITERAL*/ + /* evans 2001-07-24: was (term1->kind == CTT_INTLITERAL) && (term2->kind == CTT_INTLITERAL) ) */ + { + long t1, t2; + + t1 = constraintTerm_getValue (term1); + t2 = constraintTerm_getValue (term2); + + return (t1 == t2); + } + + /*drl this if statement handles the case where constraintTerm_canGetValue only returns + true for term1 or term2 but no both + if constraintTerm_canGetValue returned tru for both we would have returned in the previous if statement + I suppose this could be done with xor but I've never used xor and don't feel like starting now + besides this way is more effecient. + */ + if (constraintTerm_canGetValue (term1) || constraintTerm_canGetValue (term2)) + { + + return FALSE; + } + + s1 = constraintTerm_getsRef (term1); + s2 = constraintTerm_getsRef (term2); + + if (!(sRef_isValid(s1) && sRef_isValid(s2))) + { + return FALSE; + } + + DPRINTF((message + ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2) + ) + ) + ); + + if (sRef_similarRelaxed(s1, s2) || sRef_sameName (s1, s2) ) + { + DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + return TRUE; + } + else + { + DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + return FALSE; + } +} + +void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f) +{ + fileloc loc; + constraintTermValue value; + constraintTermType kind; + uentry u; + + loc = t->loc; + + value = t->value; + + kind = t->kind; + + fprintf(f, "%d\n", (int) kind); + + switch (kind) + { + + case CTT_EXPR: + u = exprNode_getUentry(t->value.expr); + fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u))); + break; + + case CTT_SREF: + { + sRef s; + + s = t->value.sref; + + if (sRef_isResult (s ) ) + { + fprintf(f, "Result\n"); + } + else if (sRef_isParam (s)) + { + int param; + ctype ct; + cstring ctString; + + + ct = sRef_getType (s); + param = sRef_getParam(s); + + ctString = ctype_dump(ct); + + fprintf(f, "Param %s %d\n", cstring_toCharsSafe(ctString), (int) param ); + cstring_free(ctString); + } + else if (sRef_isField (s) ) + { + fprintf(f, "sRef_dump %s\n", cstring_toCharsSafe(sRef_dump(s)) ); + } + else + { + u = sRef_getUentry(s); + fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u))); + } + + } + break; + + case CTT_INTLITERAL: + fprintf (f, "%ld\n", t->value.intlit); + break; + + default: + BADEXIT; + } + } + +/*@only@*/ constraintTerm constraintTerm_undump (FILE *f) +{ + constraintTermType kind; + constraintTerm ret; + + uentry ue; + + char *str; + char *os; + + os = mstring_create (MAX_DUMP_LINE_LENGTH); + + str = fgets (os, MAX_DUMP_LINE_LENGTH, f); + + llassert (str != NULL); + + kind = (constraintTermType) reader_getInt(&str); + str = fgets(os, MAX_DUMP_LINE_LENGTH, f); + + llassert (str != NULL); + + switch (kind) + { + + case CTT_SREF: + { + sRef s; + char * term; + term = reader_getWord(&str); + + if (term == NULL) + { + llfatalbug (message ("Library file appears to be corrupted.") ); + } + if (strcmp (term, "Result") == 0 ) + { + s = sRef_makeResult (ctype_unknown); + } + else if (strcmp (term, "Param" ) == 0 ) + { + int param; + char *str2, *ostr2; + + ctype t; + + reader_checkChar(&str, ' '); + str2 = reader_getWord(&str); + param = reader_getInt(&str); + + if (str2 == NULL) + { + llfatalbug (message ("Library file appears to be corrupted.") ); + } + + ostr2 = str2; + t = ctype_undump(&str2) ; + s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc, SA_CREATED)); + free (ostr2); + } + else if (strcmp (term, "sRef_dump" ) == 0 ) + { + reader_checkChar(&str, ' '); + s = sRef_undump (&str); + } + else /* This must be an identified that we can search for in usymTab */ + { + cstring termStr = cstring_makeLiteralTemp(term); + + ue = usymtab_lookup (termStr); + s = uentry_getSref(ue); + } + + ret = constraintTerm_makesRef(s); + + free(term); + } + break; + + case CTT_EXPR: + { + sRef s; + char * term; + cstring termStr; + + term = reader_getWord(&str); + + if (term == NULL) + { + llfatalbug (message ("Library file appears to be corrupted.") ); + } + + /* This must be an identifier that we can search for in usymTab */ + termStr = cstring_makeLiteralTemp(term); + + ue = usymtab_lookup (termStr); + s = uentry_getSref(ue); + ret = constraintTerm_makesRef(s); + + free (term); + } + break; + + + case CTT_INTLITERAL: + { + int i; + + i = reader_getInt(&str); + ret = constraintTerm_makeIntLiteral (i); + } + break; + + default: + BADEXIT; + } + free (os); + + return ret; +} + + + +/* drl added sometime before 10/17/001*/ +ctype constraintTerm_getCType (constraintTerm term) +{ + ctype ct; + + switch (term->kind) + { + case CTT_EXPR: + ct = exprNode_getType (term->value.expr); + break; + + case CTT_INTLITERAL: + ct = ctype_signedintegral; + break; + + case CTT_SREF: + ct = sRef_getType (term->value.sref) ; + break; + default: + BADEXIT; + } + return ct; +} + +bool constraintTerm_isConstantOnly (constraintTerm term) +{ + switch (term->kind) + { + case CTT_EXPR: + if (exprNode_isNumLiteral (term->value.expr) || + exprNode_isStringLiteral (term->value.expr) || + exprNode_isCharLiteral (term->value.expr) ) + { + return TRUE; + } + else + { + return FALSE; + } + + case CTT_INTLITERAL: + return TRUE; + + case CTT_SREF: + if ( sRef_isConst (term->value.sref) ) + { + return TRUE; + } + else + { + return FALSE; + } + default: + BADEXIT; + } + + BADEXIT; +}