/* ** 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 */ /* ** constraintGeneration.c */ /* #define DEBUGPRINT 1 */ # include /* for isdigit */ # include "splintMacros.nf" # include "basic.h" # include "cgrammar_tokens.h" # include "exprChecks.h" # include "exprNodeSList.h" /*drl We need to access the internal representation of exprNode because these functions walk down the parse tree and need a richer information than is accessible through the exprNode interface.*/ /*@access exprNode@*/ static /*@nullwhentrue@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e); static void exprNode_stmt (/*@temp@*/ /*@temp@*/ exprNode p_e); static void exprNode_multiStatement (/*@temp@*/ exprNode p_e); static constraintList exprNode_traverseTrueEnsuresConstraints (/*@temp@*/ exprNode p_e); static constraintList exprNode_traverseFalseEnsuresConstraints (/*@temp@*/ exprNode p_e); static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/; static constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist); static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e) { llassert(exprNode_isDefined(e)); switch (e->kind) { case XPR_INITBLOCK: case XPR_EMPTY: case XPR_LABEL: case XPR_CONST: case XPR_VAR: case XPR_BODY: case XPR_OFFSETOF: case XPR_ALIGNOFT: case XPR_ALIGNOF: case XPR_VAARG: case XPR_ITERCALL: case XPR_ITER: case XPR_GOTO: case XPR_CONTINUE: case XPR_BREAK: case XPR_COMMA: case XPR_COND: case XPR_TOK: case XPR_FTDEFAULT: case XPR_DEFAULT: case XPR_FTCASE: case XPR_CASE: case XPR_NODE: DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)))); return TRUE; /*@notreached@*/ break; default: return FALSE; } /*not reached*/ return FALSE; } /*@nullwhentrue@*/ bool exprNode_handleError (exprNode e) { if (exprNode_isError (e) || exprNode_isUnhandled (e)) { return TRUE; } return FALSE; } /* evans 2002-03-2 - parameter was dependent */ bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) { if (exprNode_isError (e)) return FALSE; if (exprNode_isUnhandled (e)) { DPRINTF((message("Warning ignoring %s", exprNode_unparse (e)))); return FALSE; } DPRINTF ((message ("exprNode_generateConstraints Analyzing %s at %s", exprNode_unparse(e), fileloc_unparse(exprNode_loc (e))))); if (exprNode_isMultiStatement (e)) { exprNode_multiStatement(e); } else { /* fileloc loc; */ /* loc = exprNode_getNextSequencePoint(e); */ /* exprNode_exprTraverse(e, FALSE, FALSE, loc); */ /* fileloc_free(loc); */ exprNode_stmt(e); return FALSE; } { constraintList c; c = constraintList_makeFixedArrayConstraints (e->uses); e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, c); constraintList_free(c); } DPRINTF ((message ("e->requiresConstraints %s", constraintList_unparseDetailed (e->requiresConstraints)))); return FALSE; } static void exprNode_stmt (/*@temp@*/ exprNode e) { exprNode snode; fileloc loc; DPRINTF (("Generating constraint for: %s", exprNode_unparse (e))); if (exprNode_isError(e)) { return; } /*e->requiresConstraints = constraintList_makeNew(); e->ensuresConstraints = constraintList_makeNew(); */ /*!! s = exprNode_unparse (e); */ if (e->kind == XPR_INIT) { constraintList tempList; DPRINTF (("Init: %s ", exprNode_unparse (e))); loc = exprNode_getNextSequencePoint (e); /* reduces to an expression */ DPRINTF (("Location: %s", fileloc_unparse (loc))); DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints))); exprNode_exprTraverse (e, FALSE, FALSE, loc); DPRINTF (("Ensures after: %s", constraintList_unparse (e->ensuresConstraints))); DPRINTF (("After traversing...")); fileloc_free(loc); tempList = e->requiresConstraints; DPRINTF (("Requires before: %s", constraintList_unparse (e->requiresConstraints))); e->requiresConstraints = exprNode_traverseRequiresConstraints (e); DPRINTF (("Requires after: %s", constraintList_unparse (e->requiresConstraints))); constraintList_free(tempList); tempList = e->ensuresConstraints; DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints))); e->ensuresConstraints = exprNode_traverseEnsuresConstraints(e); DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints))); constraintList_free(tempList); return; } /*drl 2/13/002 patched bug so return statement will be checked*/ /*return is a stmt not not expression ...*/ if (e->kind == XPR_RETURN) { constraintList tempList; loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ exprNode_exprTraverse (exprData_getSingle (e->edata), FALSE, TRUE, loc); fileloc_free(loc); tempList = e->requiresConstraints; e->requiresConstraints = exprNode_traverseRequiresConstraints(e); constraintList_free(tempList); } if (e->kind != XPR_STMT) { DPRINTF (("Not Stmt")); DPRINTF ((message ("%s ", exprNode_unparse (e)))); if (exprNode_isMultiStatement (e)) { exprNode_multiStatement (e); /* evans 2001-08-21: spurious return removed */ } else { loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ exprNode_exprTraverse (e, FALSE, TRUE, loc); fileloc_free(loc); } return; } DPRINTF (("Stmt")); DPRINTF ((message ("%s ", exprNode_unparse (e)))); snode = exprData_getUopNode (e->edata); /* could be stmt involving multiple statements: i.e. if, while for ect. */ if (exprNode_isMultiStatement (snode)) { exprNode_multiStatement (snode); (void) exprNode_copyConstraints (e, snode); return; } loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ exprNode_exprTraverse (snode, FALSE, FALSE, loc); fileloc_free(loc); constraintList_free (e->requiresConstraints); e->requiresConstraints = exprNode_traverseRequiresConstraints(snode); constraintList_free (e->ensuresConstraints); e->ensuresConstraints = exprNode_traverseEnsuresConstraints(snode); DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_unparse(e->requiresConstraints), constraintList_unparse(e->ensuresConstraints)))); return; } static void exprNode_stmtList (/*@dependent@*/ exprNode e) { exprNode stmt1, stmt2; if (exprNode_isError (e)) { return; } /* Handle case of stmtList with only one statement: The parse tree stores this as stmt instead of stmtList */ if (e->kind != XPR_STMTLIST) { exprNode_stmt(e); return; } llassert (e->kind == XPR_STMTLIST); DPRINTF(("exprNode_stmtList STMTLIST:")); DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)))); stmt1 = exprData_getPairA (e->edata); stmt2 = exprData_getPairB (e->edata); DPRINTF(("exprNode_stmtlist ")); DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2)))); exprNode_stmt (stmt1); DPRINTF(("\nstmt after stmtList call ")); exprNode_stmt (stmt2); exprNode_mergeResolve (e, stmt1, stmt2); DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_unparse(e->requiresConstraints), constraintList_unparse(e->ensuresConstraints)))); return; } static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body) { constraintList temp; DPRINTF ((message ("doIf: %s ", exprNode_unparse(e)))); llassert (exprNode_isDefined(test)); llassert (exprNode_isDefined (e)); llassert (exprNode_isDefined (body)); DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints)))); DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints)))); DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->trueEnsuresConstraints)))); DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->falseEnsuresConstraints)))); DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->ensuresConstraints)))); DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->ensuresConstraints)))); DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->trueEnsuresConstraints)))); DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->falseEnsuresConstraints)))); temp = test->trueEnsuresConstraints; test->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(test); constraintList_free(temp); temp = test->ensuresConstraints; test->ensuresConstraints = exprNode_traverseEnsuresConstraints (test); constraintList_free(temp); temp = test->requiresConstraints; test->requiresConstraints = exprNode_traverseRequiresConstraints (test); constraintList_free(temp); test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints); DPRINTF ((message ("doIf: test ensures %s ", constraintList_unparse(test->ensuresConstraints)))); DPRINTF ((message ("doIf: test true ensures %s ", constraintList_unparse(test->trueEnsuresConstraints)))); constraintList_free(e->requiresConstraints); e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints); e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->ensuresConstraints); temp = e->requiresConstraints; e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints); constraintList_free(temp); /* drl possible problem : warning bad */ constraintList_free(e->ensuresConstraints); e->ensuresConstraints = constraintList_copy (test->ensuresConstraints); if (exprNode_mayEscape (body)) { DPRINTF ((message("doIf: the if statement body %s returns or exits", exprNode_unparse(body)))); e->ensuresConstraints = constraintList_mergeEnsuresFreeFirst (e->ensuresConstraints, test->falseEnsuresConstraints); } DPRINTF ((message ("doIf: if requiers %s ", constraintList_unparse(e->requiresConstraints)))); return e; } /*drl added 3/4/2001 Also used for condition i.e. ?: operation Precondition This function assumes that p, trueBranch, falseBranch have have all been traversed for constraints i.e. we assume that exprNode_traverseEnsuresConstraints, exprNode_traverseRequiresConstraints, exprNode_traverseTrueEnsuresConstraints, exprNode_traverseFalseEnsuresConstraints have all been run */ static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch) { constraintList c1, cons, t, t2, f, f2; llassert (exprNode_isDefined (e)); llassert (exprNode_isDefined (p)); llassert (exprNode_isDefined (trueBranch)); llassert (exprNode_isDefined (falseBranch)); DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e)))); /* do requires clauses */ c1 = constraintList_copy (p->ensuresConstraints); t = constraintList_reflectChanges(trueBranch->requiresConstraints, p->trueEnsuresConstraints); t = constraintList_reflectChangesFreePre (t, p->ensuresConstraints); cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints); cons = constraintList_reflectChangesFreePre (cons, c1); constraintList_free (e->requiresConstraints); e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons); e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints); /* do ensures clauses find the the ensures lists for each subbranch */ t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints); t2 = t; t = constraintList_mergeEnsures (p->ensuresConstraints, t); constraintList_free(t2); f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints); f2 = f; f = constraintList_mergeEnsures (p->ensuresConstraints, f); constraintList_free(f2); /* find ensures for whole if/else statement */ constraintList_free(e->ensuresConstraints); e->ensuresConstraints = constraintList_logicalOr (t, f); constraintList_free(t); constraintList_free(f); constraintList_free(cons); constraintList_free(c1); DPRINTF ((message ("doIfElse: if requires %q ", constraintList_unparse(e->requiresConstraints)))); DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_unparse(e->ensuresConstraints)))); return e; } static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body) { DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e)))); return doIf (e, test, body); } /*@only@*/ constraintList constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s) { constraintList ret; constraint con; ret = constraintList_makeNew(); sRefSet_elements (s, el) { if (sRef_isFixedArray(el)) { size_t size; DPRINTF((message("%s is a fixed array", sRef_unparse(el)))); size = sRef_getArraySize(el); DPRINTF((message("%s is a fixed array with size %d", sRef_unparse(el), (int)size))); con = constraint_makeSRefSetBufferSize (el, size_toLong (size - 1)); ret = constraintList_add(ret, con); } else { DPRINTF((message("%s is not a fixed array", sRef_unparse(el)))); if (sRef_isExternallyVisible (el)) { /* DPRINTF((message("%s is externally visible", sRef_unparse(el)))); con = constraint_makeSRefWriteSafeInt(el, 0); ret = constraintList_add(ret, con); con = constraint_makeSRefReadSafeInt(el, 0); ret = constraintList_add(ret, con); */ } } } end_sRefSet_elements ; DPRINTF((message("constraintList_makeFixedArrayConstraints returning %s", constraintList_unparse(ret)))); return ret; } # if 0 exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e) { constraintList c; DPRINTF(("makeDataTypeConstraints")); c = constraintList_makeFixedArrayConstraints (e->uses); e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c); return e; } # endif static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, /*@dependent@*/ exprNode forBody) { exprNode init, test, inc; /* merge the constraints: modle as if statement */ /* init if (test) for body inc */ llassert (exprNode_isDefined (e)); llassert (exprNode_isDefined (forPred)); llassert (exprNode_isDefined (forBody)); init = exprData_getTripleInit (forPred->edata); test = exprData_getTripleTest (forPred->edata); inc = exprData_getTripleInc (forPred->edata); if (((exprNode_isError (test) /*|| (exprNode_isError(init))*/) || (exprNode_isError (inc)))) { DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e)))); return; } exprNode_forLoopHeuristics(e, forPred, forBody); constraintList_free(e->requiresConstraints); e->requiresConstraints = constraintList_reflectChanges(forBody->requiresConstraints, test->ensuresConstraints); e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints); e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints); if (!forBody->canBreak) { e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints)); e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy(test->falseEnsuresConstraints)); } else { DPRINTF(("Can break")); } } static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/ exprNode e) { /* !!! DRL - this is ridiculous! Read the manual on memory annotations please! */ return e; } static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switchExpr, /*@dependent@*/ exprNode body, /*@special@*/ constraintList *currentRequires, /*@special@*/ constraintList *currentEnsures, /*@special@*/ constraintList *savedRequires, /*@special@*/ constraintList *savedEnsures) /*@post:only *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/ /*@sets *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/ { exprNode stmt, stmtList; DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s", exprNode_unparse(switchExpr), exprNode_unparse(body) ))); if (exprNode_isError(body)) { *currentRequires = constraintList_makeNew (); *currentEnsures = constraintList_makeNew (); *savedRequires = constraintList_makeNew (); *savedEnsures = constraintList_makeNew (); /*@-onlytrans@*/ return; /*@=onlytrans@*/ } if (body->kind != XPR_STMTLIST) { DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s", exprNode_unparse(body)))); stmt = body; stmtList = exprNode_undefined; stmt = exprNode_makeDependent(stmt); stmtList = exprNode_makeDependent(stmtList); } else { stmt = exprData_getPairB(body->edata); stmtList = exprData_getPairA(body->edata); stmt = exprNode_makeDependent(stmt); stmtList = exprNode_makeDependent(stmtList); } DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s", exprNode_unparse(stmtList), exprNode_unparse(stmt)) )); exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures, savedRequires, savedEnsures); if (exprNode_isError(stmt)) /*@-onlytrans@*/ return; /*@=onlytrans@*/ exprNode_stmt(stmt); switchExpr = exprNode_makeDependent (switchExpr); if (! exprNode_isCaseMarker(stmt)) { constraintList temp; DPRINTF ((message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt), constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints)))); temp = constraintList_reflectChanges (stmt->requiresConstraints, *currentEnsures); *currentRequires = constraintList_mergeRequiresFreeFirst( *currentRequires, temp); constraintList_free(temp); *currentEnsures = constraintList_mergeEnsuresFreeFirst (*currentEnsures, stmt->ensuresConstraints); DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:" "%s currentEnsures:%s", exprNode_unparse(switchExpr), exprNode_unparse(body), constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures) ))); /*@-onlytrans@*/ return; /*@=onlytrans@*/ } if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList)) { /* ** merge current and saved constraint with Logical Or... ** make a constraint for ensures */ constraintList temp; constraint con; DPRINTF ((message("Got case marker"))); if (constraintList_isUndefined(*savedEnsures) && constraintList_isUndefined(*savedRequires)) { llassert(constraintList_isUndefined(*savedEnsures)); llassert(constraintList_isUndefined(*savedRequires)); *savedEnsures = constraintList_copy(*currentEnsures); *savedRequires = constraintList_copy(*currentRequires); } else { DPRINTF ((message("Doing logical or"))); temp = constraintList_logicalOr (*savedEnsures, *currentEnsures); constraintList_free (*savedEnsures); *savedEnsures = temp; *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires); } con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle (stmt->edata), exprNode_loc (stmt)); constraintList_free (*currentEnsures); *currentEnsures = constraintList_makeNew(); *currentEnsures = constraintList_add(*currentEnsures, con); constraintList_free(*currentRequires); *currentRequires = constraintList_makeNew(); DPRINTF (("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:" "%s savedEnsures:%s", exprNode_unparse(switchExpr), exprNode_unparse(body), constraintList_unparse(*savedRequires), constraintList_unparse(*savedEnsures) )); } else if (exprNode_isCaseMarker(stmt)) /* prior case has no break. */ { /* We don't do anything to the sved constraints because the case hasn't ended The new ensures constraints for the case will be: the constraint for the case statement (CASE_LABEL == SWITCH_EXPR) logicalOr currentEnsures */ constraintList temp; constraint con; constraintList ensuresTemp; con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle (stmt->edata), exprNode_loc (stmt)); ensuresTemp = constraintList_makeNew (); ensuresTemp = constraintList_add (ensuresTemp, con); if (exprNode_isError (stmtList)) { constraintList_free (*currentEnsures); *currentEnsures = constraintList_copy (ensuresTemp); constraintList_free (ensuresTemp); } else { temp = constraintList_logicalOr (*currentEnsures, ensuresTemp); constraintList_free (*currentEnsures); constraintList_free (ensuresTemp); *currentEnsures = temp; } constraintList_free (*currentRequires); *currentRequires = constraintList_makeNew(); } else { /* we handle the case of ! exprNode_isCaseMarker above the else if clause should always be true. */ BADEXIT; } DPRINTF (("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:" "%s currentEnsures:%s", exprNode_unparse(switchExpr), exprNode_unparse(body), constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures) )); /*@-onlytrans@*/ return; /*@=onlytrans@*/ } static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt) { constraintList constraintsRequires; constraintList constraintsEnsures; constraintList lastRequires; constraintList lastEnsures; exprNode body; exprNode switchExpr; switchExpr = exprData_getPairA (switchStmt->edata); body = exprData_getPairB (switchStmt->edata); if (!exprNode_isDefined (body)) { return; } DPRINTF((message(""))); if (body->kind == XPR_BLOCK) body = exprData_getSingle(body->edata); constraintsRequires = constraintList_undefined; constraintsEnsures = constraintList_undefined; lastRequires = constraintList_makeNew(); lastEnsures = constraintList_makeNew(); /*@-mustfree@*/ /* evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */ exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires, &lastEnsures, &constraintsRequires, &constraintsEnsures); /*@=mustfree@*/ /* merge current and saved constraint with Logical Or... make a constraint for ensures */ constraintList_free(switchStmt->requiresConstraints); constraintList_free(switchStmt->ensuresConstraints); if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires)) { switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures); switchStmt->requiresConstraints = constraintList_mergeRequires(constraintsRequires, lastRequires); constraintList_free (constraintsRequires); constraintList_free (constraintsEnsures); } else { switchStmt->ensuresConstraints = constraintList_copy(lastEnsures); switchStmt->requiresConstraints = constraintList_copy(lastRequires); } constraintList_free (lastRequires); constraintList_free (lastEnsures); DPRINTF(((message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s", constraintList_unparse(switchStmt->requiresConstraints), constraintList_unparse(switchStmt->ensuresConstraints) ) ))); } static exprNode doSwitch (/*@returned@*/ /*@notnull@*/ exprNode e) { exprNode body; exprData data; data = e->edata; DPRINTF ((message ("doSwitch for: switch (%s) %s", exprNode_unparse (exprData_getPairA (data)), exprNode_unparse (exprData_getPairB (data))))); body = exprData_getPairB (data); exprNode_generateConstraintSwitch (e); return e; } void exprNode_multiStatement (/*@dependent@*/ exprNode e) { bool ret; exprData data; exprNode e1, e2; exprNode p, trueBranch, falseBranch; exprNode forPred, forBody; exprNode test; constraintList temp; DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e), fileloc_unparse(exprNode_getNextSequencePoint(e))))); if (exprNode_handleError (e)) { return; } data = e->edata; ret = TRUE; switch (e->kind) { case XPR_FOR: forPred = exprData_getPairA (data); forBody = exprData_getPairB (data); /* First generate the constraints */ exprNode_generateConstraints (forPred); exprNode_generateConstraints (forBody); doFor (e, forPred, forBody); break; case XPR_FORPRED: exprNode_generateConstraints (exprData_getTripleInit (data)); test = exprData_getTripleTest (data); exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e)); exprNode_generateConstraints (exprData_getTripleInc (data)); if (!exprNode_isError(test)) { constraintList temp2; temp2 = test->trueEnsuresConstraints; test->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(test); constraintList_free(temp2); } exprNode_generateConstraints (exprData_getTripleInc (data)); break; case XPR_WHILE: e1 = exprData_getPairA (data); e2 = exprData_getPairB (data); exprNode_exprTraverse (e1, FALSE, FALSE, exprNode_loc(e1)); exprNode_generateConstraints (e2); e = doWhile (e, e1, e2); break; case XPR_IF: DPRINTF(("IF:")); DPRINTF ((exprNode_unparse(e))); e1 = exprData_getPairA (data); e2 = exprData_getPairB (data); exprNode_exprTraverse (e1, FALSE, FALSE, exprNode_loc(e1)); exprNode_generateConstraints (e2); e = doIf (e, e1, e2); break; case XPR_IFELSE: DPRINTF(("Starting IFELSE")); p = exprData_getTriplePred (data); trueBranch = exprData_getTripleTrue (data); falseBranch = exprData_getTripleFalse (data); exprNode_exprTraverse (p, FALSE, FALSE, exprNode_loc(p)); exprNode_generateConstraints (trueBranch); exprNode_generateConstraints (falseBranch); llassert (exprNode_isDefined (p)); temp = p->ensuresConstraints; p->ensuresConstraints = exprNode_traverseEnsuresConstraints (p); constraintList_free(temp); temp = p->requiresConstraints; p->requiresConstraints = exprNode_traverseRequiresConstraints (p); constraintList_free(temp); temp = p->trueEnsuresConstraints; p->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(p); constraintList_free(temp); DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_unparse(p->trueEnsuresConstraints) ) )); /*drl 10/10/2002 this is a bit of a hack but the reason why we do this is so that any function post conditions or similar things get applied correctly to each branch. e.g. in strlen(s) < 5 we want the trueEnsures to be maxRead(s) < 5*/ p->trueEnsuresConstraints = constraintList_substituteFreeTarget (p->trueEnsuresConstraints, p->ensuresConstraints); DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_unparse(p->trueEnsuresConstraints) ) )); temp = p->falseEnsuresConstraints; p->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(p); constraintList_free(temp); /*See comment on trueEnsures*/ p->falseEnsuresConstraints = constraintList_substituteFreeTarget (p->falseEnsuresConstraints, p->ensuresConstraints); e = doIfElse (e, p, trueBranch, falseBranch); DPRINTF(("Done IFELSE")); break; case XPR_DOWHILE: e2 = (exprData_getPairB (data)); e1 = (exprData_getPairA (data)); DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1)))); exprNode_generateConstraints (e2); exprNode_generateConstraints (e1); e = exprNode_copyConstraints (e, e2); DPRINTF ((message ("e = %s ", constraintList_unparse(e->requiresConstraints)))); break; case XPR_BLOCK: { exprNode tempExpr; tempExpr = exprData_getSingle (data); exprNode_generateConstraints (tempExpr); if (exprNode_isDefined(tempExpr) ) { constraintList_free(e->requiresConstraints); e->requiresConstraints = constraintList_copy (tempExpr->requiresConstraints); constraintList_free(e->ensuresConstraints); e->ensuresConstraints = constraintList_copy (tempExpr->ensuresConstraints); } else { llassert(FALSE); } } break; case XPR_SWITCH: e = doSwitch (e); break; case XPR_STMT: case XPR_STMTLIST: exprNode_stmtList (e); return ; /*@notreached@*/ break; default: ret=FALSE; } return; } static bool lltok_isBoolean_Op (lltok tok) { /*this should really be a switch statement but I don't want to violate the abstraction maybe this should go in lltok.c */ if (lltok_isEqOp (tok)) { return TRUE; } if (lltok_isAndOp (tok)) { return TRUE; } if (lltok_isOrOp (tok)) { return TRUE; } if (lltok_isGt_Op (tok)) { return TRUE; } if (lltok_isLt_Op (tok)) { return TRUE; } if (lltok_isLe_Op (tok)) { return TRUE; } if (lltok_isGe_Op (tok)) { return TRUE; } return FALSE; } static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint) { constraint cons; exprNode t1, t2; exprData data; lltok tok; constraintList tempList, temp; if (exprNode_isUndefined(e) ) { llassert (exprNode_isDefined(e) ); return; } data = e->edata; tok = exprData_getOpTok (data); t1 = exprData_getOpA (data); t2 = exprData_getOpB (data); /* drl 3/2/2003 we know this because of the type of expression*/ llassert( exprNode_isDefined(t1) && exprNode_isDefined(t2) ); tempList = constraintList_undefined; /* arithmetic tests */ if (lltok_isEqOp (tok)) { cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); } if (lltok_isLt_Op (tok)) { cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); } if (lltok_isGe_Op (tok)) { cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint); e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); } if (lltok_isGt_Op (tok)) { cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint); e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); } if (lltok_isLe_Op (tok)) { cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint); e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); } /* Logical operations */ if (lltok_isAndOp (tok)) { /* true ensures */ tempList = constraintList_copy (t1->trueEnsuresConstraints); tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList); /* false ensures: fens t1 or tens t1 and fens t2 */ tempList = constraintList_copy (t1->trueEnsuresConstraints); tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints); temp = tempList; tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints); constraintList_free (temp); /* evans - was constraintList_addList - memory leak detected by splint */ e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList); } else if (lltok_isOrOp (tok)) { /* false ensures */ tempList = constraintList_copy (t1->falseEnsuresConstraints); tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints); e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList); /* true ensures: tens t1 or fens t1 and tens t2 */ tempList = constraintList_copy (t1->falseEnsuresConstraints); tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); temp = tempList; tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints); constraintList_free(temp); e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList); tempList = constraintList_undefined; } else { DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok)))); } } void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint) { exprNode t1, t2, fcn; lltok tok; exprData data; constraint cons; constraintList temp; if (exprNode_isError(e)) { return; } DPRINTF (("exprNode_exprTraverse analyzing %s at %s", exprNode_unparse (e), fileloc_unparse (exprNode_loc (e)))); if (exprNode_isUnhandled (e)) { return; } data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint); e = exprNode_copyConstraints (e, t1); break; case XPR_FETCH: if (definatelv) { t1 = (exprData_getPairA (data)); t2 = (exprData_getPairB (data)); cons = constraint_makeWriteSafeExprNode (t1, t2); } else { t1 = (exprData_getPairA (data)); t2 = (exprData_getPairB (data)); cons = constraint_makeReadSafeExprNode (t1, t2); } e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); cons = constraint_makeEnsureLteMaxRead (t2, t1); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint); exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint); break; case XPR_PARENS: exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint); break; case XPR_INIT: { t2 = exprData_getInitNode (data); DPRINTF (("initialization ==> %s",exprNode_unparse (t2))); exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); /* This test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */ if (!exprNode_isError (e) && !exprNode_isError (t2)) { cons = constraint_makeEnsureEqual (e, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); } } break; case XPR_ASSIGN: t1 = exprData_getOpA (data); t2 = exprData_getOpB (data); DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints))); DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints))); exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint); DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints))); DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints))); exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints))); DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints))); /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */ if ((!exprNode_isError (t1)) && (!exprNode_isError(t2))) { cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); DPRINTF (("Ensure equal constraint: %s", constraint_unparse (cons))); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); DPRINTF (("Assignment constraints: %s", constraintList_unparse (e->ensuresConstraints))); } break; case XPR_OP: t1 = exprData_getOpA (data); t2 = exprData_getOpB (data); tok = exprData_getOpTok (data); if (lltok_getTok (tok) == ADD_ASSIGN) { exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint); exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); cons = constraint_makeAddAssign (t1, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); } else if (lltok_getTok (tok) == SUB_ASSIGN) { exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint); exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); cons = constraint_makeSubtractAssign (t1, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); } else { exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint); exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint); } if (lltok_isBoolean_Op (tok)) exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint); break; case XPR_SIZEOFT: /*drl 4-11-03 I think this is the same as the next case...*/ break; case XPR_SIZEOF: /* drl 7-16-01 C standard says operand to sizeof isn't evaluated unless its a variable length array. So we don't generate constraints. */ break; case XPR_CALL: fcn = exprData_getFcn(data); exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint); DPRINTF (("Got call that %s (%s)", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data)))); llassert( exprNode_isDefined(fcn) ); fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints, checkCall (fcn, exprData_getArgs (data))); fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints, exprNode_getPostConditions(fcn, exprData_getArgs (data),e )); t1 = exprNode_createNew (exprNode_getType (e)); checkArgumentList (t1, exprData_getArgs(data), sequencePoint); exprNode_mergeResolve (e, t1, fcn); exprNode_free(t1); break; case XPR_RETURN: exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint); break; case XPR_NULLRETURN: break; case XPR_FACCESS: exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint); break; case XPR_ARROW: exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint); break; case XPR_STRINGLITERAL: break; case XPR_NUMLIT: break; case XPR_PREOP: t1 = exprData_getUopNode(data); /* drl 3/2/2003 we know this because of the type of expression*/ llassert( exprNode_isDefined(t1) ); tok = (exprData_getUopTok (data)); exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint); /*handle * pointer access */ if (lltok_isIncOp (tok)) { DPRINTF(("doing ++(var)")); t1 = exprData_getUopNode (data); cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } else if (lltok_isDecOp (tok)) { DPRINTF(("doing --(var)")); t1 = exprData_getUopNode (data); cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } else if (lltok_isMult(tok )) { if (definatelv) { cons = constraint_makeWriteSafeInt (t1, 0); } else { cons = constraint_makeReadSafeInt (t1, 0); } e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); } else if (lltok_isNotOp (tok)) /* ! expr */ { constraintList_free(e->trueEnsuresConstraints); e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints); constraintList_free(e->falseEnsuresConstraints); e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints); } else if (lltok_isAmpersand_Op (tok)) { break; } else if (lltok_isMinus_Op (tok)) { break; } else if (lltok_isPlus_Op (tok)) { break; } else if (lltok_isExcl_Op (tok)) { break; } else if (lltok_isTilde_Op (tok)) { break; } else { llcontbug (message("Unsupported preop in %s", exprNode_unparse(e))); BADEXIT; } break; case XPR_POSTOP: exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint); if (lltok_isIncOp (exprData_getUopTok (data))) { DPRINTF(("doing ++")); t1 = exprData_getUopNode (data); cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } if (lltok_isDecOp (exprData_getUopTok (data))) { DPRINTF(("doing --")); t1 = exprData_getUopNode (data); cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } break; case XPR_CAST: { t2 = exprData_getCastNode (data); DPRINTF ((message ("Examining cast (%q)%s", qtype_unparse (exprData_getCastType (data)), exprNode_unparse (t2)) )); exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint); } break; case XPR_COND: { exprNode pred, trueBranch, falseBranch; llassert(FALSE); pred = exprData_getTriplePred (data); trueBranch = exprData_getTripleTrue (data); falseBranch = exprData_getTripleFalse (data); llassert (exprNode_isDefined (pred)); llassert (exprNode_isDefined (trueBranch)); llassert (exprNode_isDefined (falseBranch)); exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint); temp = pred->ensuresConstraints; pred->ensuresConstraints = exprNode_traverseEnsuresConstraints(pred); constraintList_free(temp); temp = pred->requiresConstraints; pred->requiresConstraints = exprNode_traverseRequiresConstraints(pred); constraintList_free(temp); temp = pred->trueEnsuresConstraints; pred->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(pred); constraintList_free(temp); temp = pred->falseEnsuresConstraints; pred->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(pred); constraintList_free(temp); exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint); temp = trueBranch->ensuresConstraints; trueBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(trueBranch); constraintList_free(temp); temp = trueBranch->requiresConstraints; trueBranch->requiresConstraints = exprNode_traverseRequiresConstraints(trueBranch); constraintList_free(temp); temp = trueBranch->trueEnsuresConstraints; trueBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(trueBranch); constraintList_free(temp); temp = trueBranch->falseEnsuresConstraints; trueBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(trueBranch); constraintList_free(temp); exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint); temp = falseBranch->ensuresConstraints; falseBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(falseBranch); constraintList_free(temp); temp = falseBranch->requiresConstraints; falseBranch->requiresConstraints = exprNode_traverseRequiresConstraints(falseBranch); constraintList_free(temp); temp = falseBranch->trueEnsuresConstraints; falseBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(falseBranch); constraintList_free(temp); temp = falseBranch->falseEnsuresConstraints; falseBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(falseBranch); constraintList_free(temp); /* if pred is true e equals true otherwise pred equals false */ cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint); trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons); cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint); falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons); e = doIfElse (e, pred, trueBranch, falseBranch); } break; case XPR_COMMA: llassert(FALSE); t1 = exprData_getPairA (data); t2 = exprData_getPairB (data); /* we essiantially treat this like expr1; expr2 of course sequencePoint isn't adjusted so this isn't completely accurate problems... */ exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint); exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint); exprNode_mergeResolve (e, t1, t2); break; default: break; } e->requiresConstraints = constraintList_preserveOrig (e->requiresConstraints); e->ensuresConstraints = constraintList_preserveOrig (e->ensuresConstraints); e->requiresConstraints = constraintList_addGeneratingExpr (e->requiresConstraints, e); e->ensuresConstraints = constraintList_addGeneratingExpr (e->ensuresConstraints, e); e->requiresConstraints = constraintList_removeSurpressed (e->requiresConstraints); DPRINTF (("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed (e->ensuresConstraints))); DPRINTF (("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))); DPRINTF (("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->trueEnsuresConstraints))); DPRINTF (("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->falseEnsuresConstraints))); return; } constraintList exprNode_traverseTrueEnsuresConstraints (exprNode e) { exprNode t1; bool handledExprNode; exprData data; constraintList ret; if (exprNode_handleError (e)) { ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->trueEnsuresConstraints); handledExprNode = TRUE; data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (t1)); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getPairA (data))); ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getPairB (data))); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getUopNode (data))); break; case XPR_INIT: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getInitNode (data))); break; case XPR_ASSIGN: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getOpB (data))); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getOpB (data))); break; case XPR_SIZEOFT: break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getSingle (data))); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getFcn (data))); break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getSingle (data))); break; case XPR_NULLRETURN: break; case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getFieldNode (data))); break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getFieldNode (data))); break; case XPR_STRINGLITERAL: break; case XPR_NUMLIT: break; case XPR_POSTOP: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getUopNode (data))); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (exprData_getCastNode (data))); break; default: break; } return ret; } constraintList exprNode_traverseFalseEnsuresConstraints (exprNode e) { exprNode t1; bool handledExprNode; exprData data; constraintList ret; if (exprNode_handleError (e)) { ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->falseEnsuresConstraints); handledExprNode = TRUE; data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); ret = constraintList_addListFree (ret,exprNode_traverseFalseEnsuresConstraints (t1)); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getPairA (data))); ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getPairB (data))); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getUopNode (data))); break; case XPR_INIT: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints ( exprData_getInitNode (data))); break; case XPR_ASSIGN: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getOpB (data))); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getOpB (data))); break; case XPR_SIZEOFT: break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getSingle (data))); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getFcn (data))); break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getSingle (data))); break; case XPR_NULLRETURN: break; case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getFieldNode (data))); break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getFieldNode (data))); break; case XPR_STRINGLITERAL: break; case XPR_NUMLIT: break; case XPR_POSTOP: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getUopNode (data))); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints (exprData_getCastNode (data))); break; default: break; } return ret; } /* walk down the tree and get all requires Constraints in each subexpression*/ /*@only@*/ constraintList exprNode_traverseRequiresConstraints (exprNode e) { exprNode t1; bool handledExprNode; exprData data; constraintList ret; if (exprNode_handleError (e)) { ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->requiresConstraints); handledExprNode = TRUE; data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (t1)); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getPairA (data))); ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getPairB (data))); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getUopNode (data))); break; case XPR_INIT: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getInitNode (data))); break; case XPR_ASSIGN: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getOpB (data))); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getOpB (data))); break; case XPR_SIZEOFT: break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getSingle (data))); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getFcn (data))); break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getSingle (data))); break; case XPR_NULLRETURN: break; case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getFieldNode (data))); break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getFieldNode (data))); break; case XPR_STRINGLITERAL: break; case XPR_NUMLIT: break; case XPR_POSTOP: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getUopNode (data))); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (exprData_getCastNode (data))); break; default: break; } return ret; } /* walk down the tree and get all Ensures Constraints in each subexpression*/ /*@only@*/ constraintList exprNode_traverseEnsuresConstraints (exprNode e) { exprNode t1; bool handledExprNode; exprData data; constraintList ret; if (exprNode_handleError (e)) { ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->ensuresConstraints); handledExprNode = TRUE; data = e->edata; DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with " "constraintList of %s", exprNode_unparse (e), constraintList_unparse(e->ensuresConstraints) ) )); switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); ret = constraintList_addListFree (ret,exprNode_traverseEnsuresConstraints (t1)); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getPairA (data))); ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getPairB (data))); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getUopNode (data))); break; case XPR_INIT: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getInitNode (data))); break; case XPR_ASSIGN: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getOpB (data))); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getOpB (data))); break; case XPR_SIZEOFT: break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getSingle (data))); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getFcn (data))); break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getSingle (data))); break; case XPR_NULLRETURN: break; case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getFieldNode (data))); break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getFieldNode (data))); break; case XPR_STRINGLITERAL: break; case XPR_NUMLIT: break; case XPR_POSTOP: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getUopNode (data))); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints (exprData_getCastNode (data))); break; default: break; } DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with " "constraintList of is returning %s", exprNode_unparse (e), constraintList_unparse(ret)))); return ret; } /*drl moved out of constraintResolve.c 07-02-001 */ void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint) { llassert(temp != NULL ); temp->requiresConstraints = constraintList_makeNew(); temp->ensuresConstraints = constraintList_makeNew(); temp->trueEnsuresConstraints = constraintList_makeNew(); temp->falseEnsuresConstraints = constraintList_makeNew(); exprNodeList_elements (arglist, el) { constraintList temp2; llassert(exprNode_isDefined(el) ); exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint); temp2 = el->requiresConstraints; el->requiresConstraints = exprNode_traverseRequiresConstraints(el); constraintList_free(temp2); temp2 = el->ensuresConstraints; el->ensuresConstraints = exprNode_traverseEnsuresConstraints(el); constraintList_free(temp2); temp->requiresConstraints = constraintList_addList(temp->requiresConstraints, el->requiresConstraints); temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints, el->ensuresConstraints); } end_exprNodeList_elements; } /*drl moved out of constraintResolve.c 07-03-001 */ constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall) { constraintList postconditions; uentry temp; DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist)))); temp = exprNode_getUentry (fcn); postconditions = uentry_getFcnPostconditions (temp); if (constraintList_isDefined (postconditions)) { postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist); postconditions = constraintList_doFixResult (postconditions, fcnCall); } else { postconditions = constraintList_makeNew(); } return postconditions; } /* comment this out for now we'll include it in a production release when its stable... void findStructs (exprNodeList arglist) { ctype ct, rt; DPRINTF(( message("doing findStructs: %s", exprNodeList_unparse(arglist)) )); exprNodeList_elements(arglist, expr) { ct = exprNode_getType(expr); rt = ctype_realType (ct); if (ctype_isStruct (rt)) DPRINTF((message("Found structure %s", exprNode_unparse(expr)) )); if (hasInvariants(ct)) { constraintList invars; invars = getInvariants(ct); DPRINTF((message ("findStructs has invariants %s ", constraintList_unparse (invars)) )); invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct); DPRINTF((message ("findStructs finded invariants to be %s ", constraintList_unparse (invars)) )); } } end_exprNodeList_elements; } */ /*drl moved out of constraintResolve.c 07-02-001 */ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist) { constraintList preconditions; uentry temp; DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist)))); temp = exprNode_getUentry (fcn); preconditions = uentry_getFcnPreconditions (temp); if (constraintList_isDefined(preconditions)) { preconditions = constraintList_togglePost (preconditions); preconditions = constraintList_preserveCallInfo(preconditions, fcn); preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist); } else { if (constraintList_isUndefined(preconditions)) preconditions = constraintList_makeNew(); } if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS)) { /* uentryList_elements (arglist, el) { sRef s; DPRINTF((message("setImplicitfcnConstraints doing: %s", uentry_unparse(el) ) )); s = uentry_getSref(el); if (sRef_isReference (s) ) { DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) )); } else { DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) )); } //drl 4/26/01 //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 c = constraint_makeSRefWriteSafeInt (s, 0); implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); //drl 10/23/2002 added support for out if (!uentry_isOut(el) ) { c = constraint_makeSRefReadSafeInt (s, 0); implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); } } */ } DPRINTF ((message("Done checkCall\n"))); DPRINTF ((message("Returning list %q ", constraintList_unparseDetailed(preconditions)))); /* drl we're going to comment this out for now we'll include it if we're sure it's working findStructs(arglist); */ return preconditions; } /*drl added this function 10.29.001 takes an exprNode of the form const + const and sets the value */ /*drl I'm a bit nervous about modifying the exprNode but this is the easy way to do this If I have time I'd like to cause the exprNode to get created correctly in the first place */ void exprNode_findValue(exprNode e) { exprData data; exprNode t1, t2; lltok tok; llassert(exprNode_isDefined(e) ); data = e->edata; if (exprNode_hasValue(e)) return; if (e->kind == XPR_OP) { t1 = exprData_getOpA (data); t2 = exprData_getOpB (data); tok = exprData_getOpTok (data); exprNode_findValue(t1); exprNode_findValue(t2); if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2)))) return; if (lltok_isPlus_Op (tok)) { long v1, v2; v1 = exprNode_getLongValue(t1); v2 = exprNode_getLongValue(t2); if (multiVal_isDefined(e->val)) multiVal_free (e->val); e->val = multiVal_makeInt (v1 + v2); } if (lltok_isMinus_Op (tok)) { long v1, v2; v1 = exprNode_getLongValue(t1); v2 = exprNode_getLongValue(t2); if (multiVal_isDefined(e->val)) { multiVal_free (e->val); } e->val = multiVal_makeInt (v1 - v2); } /*drl I should really do * and / at some point */ } }