return FALSE;
}
+static bool isZeroBinaryOp (constraintExpr expr)
+{
+ constraintExpr e2;
+
+ if (!constraintExpr_isBinaryExpr (expr) )
+ {
+ return FALSE;
+ }
+
+
+ e2 = constraintExprData_binaryExprGetExpr2(expr->data);
+
+ if (constraintExpr_isBinaryExpr (e2) )
+ {
+ constraintExpr e1;
+ constraintExprBinaryOpKind op;
+
+ op = constraintExprData_binaryExprGetOp (e2->data);
+
+ e1 = constraintExprData_binaryExprGetExpr1(e2->data);
+
+ if (constraintExpr_isLit(e1) )
+ {
+ if (constraintExpr_getValue(e1) == 0 )
+ {
+ return TRUE;
+ }
+ }
+ }
+ return FALSE;
+}
+
+/* change expr + (o - expr) to (expr -expr) */
+
+/*@only@*/ static constraintExpr removeZero (/*@only@*/ /*@returned@*/ constraintExpr expr)
+{
+ constraintExpr expr1, expr2;
+
+ constraintExpr temp;
+
+ constraintExprBinaryOpKind op;
+
+ constraintExprBinaryOpKind tempOp;
+
+ if (!isZeroBinaryOp(expr) )
+ return expr;
+
+
+ expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
+ expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
+ op = constraintExprData_binaryExprGetOp(expr->data);
+
+ llassert( constraintExpr_isBinaryExpr(expr2) );
+
+ temp = constraintExprData_binaryExprGetExpr2 (expr2->data);
+ temp = constraintExpr_copy (temp);
+
+ tempOp = constraintExprData_binaryExprGetOp (expr2->data);
+
+ if (op == PLUS)
+ op = tempOp;
+ else if (op == MINUS)
+ {
+ if (tempOp == PLUS)
+ op = MINUS;
+ else if (tempOp == MINUS)
+ op = PLUS;
+ else
+ BADEXIT;
+ }
+ else
+ BADEXIT;
+
+ constraintExpr_free(expr2);
+
+
+
+ expr->data = constraintExprData_binaryExprSetExpr2(expr->data, temp);
+ expr->data = constraintExprData_binaryExprSetOp(expr->data, op);
+
+ return expr;
+}
+
/*@only@*/ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
/*@out@*/ bool * propagate,
op = constraintExprData_binaryExprGetOp (expr->data);
DPRINTF( (message("constraintExpr_propagateConstants: binaryexpr: %s", constraintExpr_unparse(expr) ) ) );
+
+ expr = removeZero(expr);
expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
expr2 = constraintExpr_propagateConstants (expr2, &propagate2, &literal2);
*propagate = propagate1 || propagate2;
- *literal = literal1 + literal2;
-
+
+ if (op == PLUS)
+ *literal = literal1 + literal2;
+ else if (op == MINUS)
+ *literal = literal1 - literal2;
+ else
+ BADEXIT;
+
if ( constraintExpr_isLit (expr1) && constraintExpr_isLit (expr2) )
{
int t1, t2;
t1 = constraintExpr_getValue (expr1);
t2 = constraintExpr_getValue (expr2);
+ llassert(*propagate == FALSE);
*propagate = FALSE;
constraintExpr_free (expr);
}
-
-
if (constraintExpr_isLit (expr1) )
{
*propagate = TRUE;
- if (op == PLUS )
- *literal += constraintExpr_getValue (expr1);
- else
- *literal -= constraintExpr_getValue (expr1);
+ *literal += constraintExpr_getValue (expr1);
- constraintExpr_free(expr1);
- constraintExpr_free(expr);
- return expr2;
+ if (op == PLUS)
+ {
+ constraintExpr_free(expr1);
+ constraintExpr_free(expr);
+ return expr2;
+ }
+ else if (op == MINUS)
+ {
+ constraintExpr temp;
+
+ /* this is an ugly kludge to deal with not
+ having a unary minus operation...*/
+
+ temp = constraintExpr_makeIntLiteral (0);
+ temp = constraintExpr_makeSubtractExpr (temp, expr2);
+
+ constraintExpr_free(expr1);
+ constraintExpr_free(expr);
+
+ return temp;
+ }
}
if (constraintExpr_isLit (expr2) )
if ( op == PLUS )
*literal += constraintExpr_getValue (expr2);
- else
+ else if (op == MINUS)
*literal -= constraintExpr_getValue (expr2);
+ else
+ BADEXIT;
+
constraintExpr_free(expr2);
constraintExpr_free(expr);
expr->data = constraintExprData_binaryExprSetExpr1 (expr->data, expr1);
expr->data = constraintExprData_binaryExprSetExpr2 (expr->data, expr2);
+ expr = removeZero(expr);
return expr;
}
}
-/*@only@*/ static constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e)
+/*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e)
{
return oldconstraintExpr_makeTermExprNode(e); //constraintExpr_makeExprNode (e);
}
static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/constraintExpr c)
{
constraintExpr e1, e2;
-
+ constraintExprBinaryOpKind op;
+
e1 = constraintExprData_binaryExprGetExpr1 (c->data);
e2 = constraintExprData_binaryExprGetExpr2 (c->data);
i = constraintExpr_getValue(e1) + constraintExpr_getValue (e2);
constraintExpr_free(c);
c = constraintExpr_makeIntLiteral (i);
-
}
+ else
+ {
+ op = constraintExprData_binaryExprGetOp (c->data);
+ if (op == MINUS)
+ if (constraintExpr_similar(e1, e2) )
+ {
+ constraintExpr_free(c);
+ c = constraintExpr_makeIntLiteral (0);
+ }
+ }
+
return c;
}
}
+static void exprNode_doGenerateConstraintSwitch ( exprNode switchExpr,
+ exprNode body, constraintList * currentRequires, constraintList *
+ currentEnsures, constraintList * savedRequires, constraintList *
+ savedEnsures)
+{
+ exprNode stmt, stmtList;
+
+ DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
+ exprNode_unparse(switchExpr), exprNode_unparse(body)
+ ) ));
+
+ if (exprNode_isError(body) )
+ {
+ return;
+ }
+
+ if (body->kind != XPR_STMTLIST )
+ {
+ DPRINTF((message("exprNode_doGenerateConstraintSwitch: non
+stmtlist: %s",
+ exprNode_unparse(body) )
+ ));
+ // llassert(body->kind == XPR_STMT );
+ stmt = body;
+ stmtList = exprNode_undefined;
+ }
+ else
+ {
+ stmt = exprData_getPairB(body->edata);
+ stmtList = exprData_getPairA(body->edata);
+ }
+
+ 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) )
+ return;
+
+ exprNode_stmt(stmt);
+ //, FALSE, FALSE, exprNode_getfileloc(stmt) );
+
+ 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_print(*currentRequires), constraintList_print(*currentEnsures)
+ ) ));
+ return;
+ }
+
+ 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) )
+ {
+ *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_getfileloc(stmt) );
+
+
+ constraintList_free(*currentEnsures);
+ *currentEnsures = constraintList_makeNew();
+ *currentEnsures = constraintList_add(*currentEnsures, con);
+
+ constraintList_free(*currentRequires);
+ *currentRequires = constraintList_makeNew();
+ DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
+ "%s savedEnsures:%s",
+ exprNode_unparse(switchExpr), exprNode_unparse(body),
+ constraintList_print(*savedRequires), constraintList_print(*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;
+
+ DPRINTF (( message("Got case marker with no prior break") ));
+
+ con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
+ (stmt->edata), exprNode_getfileloc(stmt) );
+
+ ensuresTemp = constraintList_makeNew();
+
+ ensuresTemp = constraintList_add (ensuresTemp, con);
+
+ if (exprNode_isError(stmtList) )
+ {
+ constraintList_free(*currentEnsures);
+ *currentEnsures = constraintList_copy(ensuresTemp);
+ }
+ else
+ {
+
+ temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
+
+ constraintList_free(*currentEnsures);
+ constraintList_free(ensuresTemp);
+
+ *currentEnsures = temp;
+ }
+ constraintList_free(*currentRequires);
+
+ *currentRequires = constraintList_makeNew();
+ }
+
+ DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
+ "%s currentEnsures:%s",
+ exprNode_unparse(switchExpr), exprNode_unparse(body),
+ constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
+ ) ));
+ return;
+
+}
+
+
+static void exprNode_generateConstraintSwitch ( exprNode switchStmt)
+{
+ constraintList constraintsRequires;
+ constraintList constraintsEnsures;
+ constraintList lastRequires;
+ constraintList lastEnsures;
+
+ exprNode body;
+ exprNode switchExpr;
+
+ switchExpr = exprData_getPairA(switchStmt->edata);
+ body = exprData_getPairB(switchStmt->edata);
+
+ //*@i22*/
+ if ( body->kind == XPR_BLOCK)
+ body = exprData_getSingle(body->edata);
+
+ constraintsRequires = constraintList_undefined;
+ constraintsEnsures = constraintList_undefined;
+
+ lastRequires = constraintList_makeNew();
+ lastEnsures = constraintList_makeNew();
+
+
+ exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires, &lastEnsures, &constraintsRequires, &constraintsEnsures);
+
+ // 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_print( switchStmt->requiresConstraints),
+ constraintList_print( switchStmt->ensuresConstraints)
+ )
+ ) ));
+}
+
static exprNode doSwitch (/*@returned@*/ exprNode e)
{
exprNode body;
data = e->edata;
// llassert(FALSE);
- DPRINTF (( message ("doSwitch for: switch (%s) %s",
+ DPRINTF (( message ("doSwitch for: switch (%s) %s",
exprNode_unparse (exprData_getPairA (data)),
exprNode_unparse (exprData_getPairB (data))) ));
-
+
body = exprData_getPairB (data);
-
+
exprNode_generateConstraints(body);
-
- constraintList_free(e->requiresConstraints);
- constraintList_free(e->ensuresConstraints);
-
- e->requiresConstraints = NULL;
- e->ensuresConstraints = NULL;
- e->requiresConstraints = constraintList_copy ( body->requiresConstraints );
- e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints );
-
+ exprNode_generateConstraintSwitch (e);
+
+ // e->requiresConstraints = constraintList_copy (body->requiresConstraints );
+ // e->ensuresConstraints = constraintList_copy (body->ensuresConstraints );
+
return e;
}
+
+
void exprNode_multiStatement (/*@dependent@*/ exprNode e)
{
andersk / splint.git / commitdiff
