From 529f71a38512813b93d68dadf8ab1f3677527639 Mon Sep 17 00:00:00 2001 From: yeom Date: Fri, 22 Jul 2011 18:24:59 +0000 Subject: [PATCH] changes on the flow down rule checking: 1) only check a relation bet array and index value when array access node is the LHS of the assignment node. When an array access is RHS, index and array should be independent. 2) have a better way to check implicit flow. after conditional branch, keep conditional location as a constraint location and then check if an assignment located inside the conditional branch block respects this constraint. --- Robust/src/Analysis/SSJava/FlowDownCheck.java | 376 ++++++++---------- Robust/src/Tests/ssJava/flowdown/makefile | 2 +- 2 files changed, 173 insertions(+), 205 deletions(-) diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index d095bc39..fa4c5d72 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -134,7 +134,6 @@ public class FlowDownCheck { ClassDescriptor cd = (ClassDescriptor) obj; toanalyze.remove(cd); - checkClass(cd); for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { MethodDescriptor md = (MethodDescriptor) method_it.next(); if (ssjava.needTobeAnnotated(md)) { @@ -209,6 +208,7 @@ public class FlowDownCheck { BlockNode bn = state.getMethodBody(md); if (ssjava.needTobeAnnotated(md)) { + // first, check annotations on method declaration // parsing returnloc annotation Vector methodAnnotations = md.getModifiers().getAnnotations(); @@ -339,7 +339,7 @@ public class FlowDownCheck { private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) { BlockNode bn = state.getMethodBody(md); - checkLocationFromBlockNode(md, md.getParameterTable(), bn); + checkLocationFromBlockNode(md, md.getParameterTable(), bn, null); } private String generateErrorMessage(ClassDescriptor cd, TreeNode tn) { @@ -352,62 +352,45 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromBlockNode(MethodDescriptor md, SymbolTable nametable, - BlockNode bn) { + BlockNode bn, CompositeLocation constraint) { bn.getVarTable().setParent(nametable); - // it will return the lowest location in the block node - CompositeLocation lowestLoc = null; - for (int i = 0; i < bn.size(); i++) { BlockStatementNode bsn = bn.get(i); - CompositeLocation bLoc = checkLocationFromBlockStatementNode(md, bn.getVarTable(), bsn); - if (!bLoc.isEmpty()) { - if (lowestLoc == null) { - lowestLoc = bLoc; - } else { - if (CompositeLattice.isGreaterThan(lowestLoc, bLoc, - generateErrorMessage(md.getClassDesc(), bn))) { - lowestLoc = bLoc; - } - } - } - - } - - if (lowestLoc == null) { - lowestLoc = new CompositeLocation(Location.createBottomLocation(md)); + checkLocationFromBlockStatementNode(md, bn.getVarTable(), bsn, constraint); } + return new CompositeLocation(); - return lowestLoc; } private CompositeLocation checkLocationFromBlockStatementNode(MethodDescriptor md, - SymbolTable nametable, BlockStatementNode bsn) { + SymbolTable nametable, BlockStatementNode bsn, CompositeLocation constraint) { CompositeLocation compLoc = null; switch (bsn.kind()) { case Kind.BlockExpressionNode: - compLoc = checkLocationFromBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn); + compLoc = + checkLocationFromBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn, constraint); break; case Kind.DeclarationNode: - compLoc = checkLocationFromDeclarationNode(md, nametable, (DeclarationNode) bsn); + compLoc = checkLocationFromDeclarationNode(md, nametable, (DeclarationNode) bsn, constraint); break; case Kind.IfStatementNode: - compLoc = checkLocationFromIfStatementNode(md, nametable, (IfStatementNode) bsn); + compLoc = checkLocationFromIfStatementNode(md, nametable, (IfStatementNode) bsn, constraint); break; case Kind.LoopNode: - compLoc = checkLocationFromLoopNode(md, nametable, (LoopNode) bsn); + compLoc = checkLocationFromLoopNode(md, nametable, (LoopNode) bsn, constraint); break; case Kind.ReturnNode: - compLoc = checkLocationFromReturnNode(md, nametable, (ReturnNode) bsn); + compLoc = checkLocationFromReturnNode(md, nametable, (ReturnNode) bsn, constraint); break; case Kind.SubBlockNode: - compLoc = checkLocationFromSubBlockNode(md, nametable, (SubBlockNode) bsn); + compLoc = checkLocationFromSubBlockNode(md, nametable, (SubBlockNode) bsn, constraint); break; case Kind.ContinueBreakNode: @@ -415,24 +398,26 @@ public class FlowDownCheck { break; case Kind.SwitchStatementNode: - compLoc = checkLocationFromSwitchStatementNode(md, nametable, (SwitchStatementNode) bsn); + compLoc = + checkLocationFromSwitchStatementNode(md, nametable, (SwitchStatementNode) bsn, constraint); } return compLoc; } private CompositeLocation checkLocationFromSwitchStatementNode(MethodDescriptor md, - SymbolTable nametable, SwitchStatementNode ssn) { + SymbolTable nametable, SwitchStatementNode ssn, CompositeLocation constraint) { ClassDescriptor cd = md.getClassDesc(); CompositeLocation condLoc = - checkLocationFromExpressionNode(md, nametable, ssn.getCondition(), new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, ssn.getCondition(), new CompositeLocation(), + constraint, false); BlockNode sbn = ssn.getSwitchBody(); Set blockLocSet = new HashSet(); for (int i = 0; i < sbn.size(); i++) { CompositeLocation blockLoc = - checkLocationFromSwitchBlockNode(md, nametable, (SwitchBlockNode) sbn.get(i)); + checkLocationFromSwitchBlockNode(md, nametable, (SwitchBlockNode) sbn.get(i), constraint); if (!CompositeLattice.isGreaterThan(condLoc, blockLoc, generateErrorMessage(cd, ssn.getCondition()))) { throw new Error( @@ -446,24 +431,25 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromSwitchBlockNode(MethodDescriptor md, - SymbolTable nametable, SwitchBlockNode sbn) { + SymbolTable nametable, SwitchBlockNode sbn, CompositeLocation constraint) { CompositeLocation blockLoc = - checkLocationFromBlockNode(md, nametable, sbn.getSwitchBlockStatement()); + checkLocationFromBlockNode(md, nametable, sbn.getSwitchBlockStatement(), constraint); return blockLoc; } private CompositeLocation checkLocationFromReturnNode(MethodDescriptor md, SymbolTable nametable, - ReturnNode rn) { + ReturnNode rn, CompositeLocation constraint) { ExpressionNode returnExp = rn.getReturnExpression(); CompositeLocation returnValueLoc; if (returnExp != null) { returnValueLoc = - checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation(), + constraint, false); // check if return value is equal or higher than RETRUNLOC of method // declaration annotation @@ -492,138 +478,86 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromLoopNode(MethodDescriptor md, SymbolTable nametable, - LoopNode ln) { + LoopNode ln, CompositeLocation constraint) { ClassDescriptor cd = md.getClassDesc(); if (ln.getType() == LoopNode.WHILELOOP || ln.getType() == LoopNode.DOWHILELOOP) { CompositeLocation condLoc = - checkLocationFromExpressionNode(md, nametable, ln.getCondition(), new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, ln.getCondition(), + new CompositeLocation(), constraint, false); addLocationType(ln.getCondition().getType(), (condLoc)); - CompositeLocation bodyLoc = checkLocationFromBlockNode(md, nametable, ln.getBody()); + constraint = generateNewConstraint(constraint, condLoc); + checkLocationFromBlockNode(md, nametable, ln.getBody(), constraint); - if (!CompositeLattice.isGreaterThan(condLoc, bodyLoc, generateErrorMessage(cd, ln))) { - // loop condition should be higher than loop body - throw new Error( - "The location of the while-condition statement is lower than the loop body at " - + cd.getSourceFileName() + ":" + ln.getCondition().getNumLine()); - } - - return bodyLoc; + return new CompositeLocation(); } else { - // check for loop case + // check 'for loop' case BlockNode bn = ln.getInitializer(); bn.getVarTable().setParent(nametable); // calculate glb location of condition and update statements CompositeLocation condLoc = checkLocationFromExpressionNode(md, bn.getVarTable(), ln.getCondition(), - new CompositeLocation()); + new CompositeLocation(), constraint, false); addLocationType(ln.getCondition().getType(), condLoc); - CompositeLocation updateLoc = - checkLocationFromBlockNode(md, bn.getVarTable(), ln.getUpdate()); - - Set glbInputSet = new HashSet(); - glbInputSet.add(condLoc); - // glbInputSet.add(updateLoc); - - CompositeLocation glbLocOfForLoopCond = CompositeLattice.calculateGLB(glbInputSet); - - // check location of 'forloop' body - CompositeLocation blockLoc = checkLocationFromBlockNode(md, bn.getVarTable(), ln.getBody()); + constraint = generateNewConstraint(constraint, condLoc); - // compute glb of body including loop body and update statement - glbInputSet.clear(); + checkLocationFromBlockNode(md, bn.getVarTable(), ln.getUpdate(), constraint); + checkLocationFromBlockNode(md, bn.getVarTable(), ln.getBody(), constraint); - if (blockLoc == null) { - // when there is no statement in the loop body - - if (updateLoc == null) { - // also there is no update statement in the loop body - return glbLocOfForLoopCond; - } - glbInputSet.add(updateLoc); - - } else { - glbInputSet.add(blockLoc); - glbInputSet.add(updateLoc); - } - - CompositeLocation loopBodyLoc = CompositeLattice.calculateGLB(glbInputSet); + return new CompositeLocation(); - if (!CompositeLattice.isGreaterThan(glbLocOfForLoopCond, loopBodyLoc, - generateErrorMessage(cd, ln))) { - throw new Error( - "The location of the for-condition statement is lower than the for-loop body at " - + cd.getSourceFileName() + ":" + ln.getCondition().getNumLine()); - } - return blockLoc; } } private CompositeLocation checkLocationFromSubBlockNode(MethodDescriptor md, - SymbolTable nametable, SubBlockNode sbn) { - CompositeLocation compLoc = checkLocationFromBlockNode(md, nametable, sbn.getBlockNode()); + SymbolTable nametable, SubBlockNode sbn, CompositeLocation constraint) { + CompositeLocation compLoc = + checkLocationFromBlockNode(md, nametable, sbn.getBlockNode(), constraint); return compLoc; } - private CompositeLocation checkLocationFromIfStatementNode(MethodDescriptor md, - SymbolTable nametable, IfStatementNode isn) { + private CompositeLocation generateNewConstraint(CompositeLocation currentCon, + CompositeLocation newCon) { - ClassDescriptor localCD = md.getClassDesc(); - Set glbInputSet = new HashSet(); + if (currentCon == null) { + return newCon; + } else { + // compute GLB of current constraint and new constraint + Set inputSet = new HashSet(); + inputSet.add(currentCon); + inputSet.add(newCon); + return CompositeLattice.calculateGLB(inputSet); + } + + } + + private CompositeLocation checkLocationFromIfStatementNode(MethodDescriptor md, + SymbolTable nametable, IfStatementNode isn, CompositeLocation constraint) { CompositeLocation condLoc = - checkLocationFromExpressionNode(md, nametable, isn.getCondition(), new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, isn.getCondition(), new CompositeLocation(), + constraint, false); addLocationType(isn.getCondition().getType(), condLoc); - glbInputSet.add(condLoc); - - CompositeLocation locTrueBlock = checkLocationFromBlockNode(md, nametable, isn.getTrueBlock()); - if (locTrueBlock != null) { - glbInputSet.add(locTrueBlock); - // here, the location of conditional block should be higher than the - // location of true/false blocks - if (locTrueBlock != null - && !CompositeLattice.isGreaterThan(condLoc, locTrueBlock, - generateErrorMessage(localCD, isn.getCondition()))) { - // error - throw new Error( - "The location of the if-condition statement is lower than the conditional block at " - + localCD.getSourceFileName() + ":" + isn.getCondition().getNumLine()); - } - } - if (isn.getFalseBlock() != null) { - CompositeLocation locFalseBlock = - checkLocationFromBlockNode(md, nametable, isn.getFalseBlock()); - - if (locFalseBlock != null) { - glbInputSet.add(locFalseBlock); - - if (!CompositeLattice.isGreaterThan(condLoc, locFalseBlock, - generateErrorMessage(localCD, isn.getCondition()))) { - // error - throw new Error( - "The location of the if-condition statement is lower than the conditional block at " - + localCD.getSourceFileName() + ":" + isn.getCondition().getNumLine()); - } - } + constraint = generateNewConstraint(constraint, condLoc); + checkLocationFromBlockNode(md, nametable, isn.getTrueBlock(), constraint); + if (isn.getFalseBlock() != null) { + checkLocationFromBlockNode(md, nametable, isn.getFalseBlock(), constraint); } - // return GLB location of condition, true, and false block - CompositeLocation glbLoc = CompositeLattice.calculateGLB(glbInputSet); - - return glbLoc; + return new CompositeLocation(); } private CompositeLocation checkLocationFromDeclarationNode(MethodDescriptor md, - SymbolTable nametable, DeclarationNode dn) { + SymbolTable nametable, DeclarationNode dn, CompositeLocation constraint) { VarDescriptor vd = dn.getVarDescriptor(); @@ -632,7 +566,7 @@ public class FlowDownCheck { if (dn.getExpression() != null) { CompositeLocation expressionLoc = checkLocationFromExpressionNode(md, nametable, dn.getExpression(), - new CompositeLocation()); + new CompositeLocation(), constraint, false); // addTypeLocation(dn.getExpression().getType(), expressionLoc); if (expressionLoc != null) { @@ -660,33 +594,36 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromBlockExpressionNode(MethodDescriptor md, - SymbolTable nametable, BlockExpressionNode ben) { + SymbolTable nametable, BlockExpressionNode ben, CompositeLocation constraint) { CompositeLocation compLoc = - checkLocationFromExpressionNode(md, nametable, ben.getExpression(), null); + checkLocationFromExpressionNode(md, nametable, ben.getExpression(), null, constraint, false); // addTypeLocation(ben.getExpression().getType(), compLoc); return compLoc; } private CompositeLocation checkLocationFromExpressionNode(MethodDescriptor md, - SymbolTable nametable, ExpressionNode en, CompositeLocation loc) { + SymbolTable nametable, ExpressionNode en, CompositeLocation loc, + CompositeLocation constraint, boolean isLHS) { CompositeLocation compLoc = null; switch (en.kind()) { case Kind.AssignmentNode: - compLoc = checkLocationFromAssignmentNode(md, nametable, (AssignmentNode) en, loc); + compLoc = + checkLocationFromAssignmentNode(md, nametable, (AssignmentNode) en, loc, constraint); break; case Kind.FieldAccessNode: - compLoc = checkLocationFromFieldAccessNode(md, nametable, (FieldAccessNode) en, loc); + compLoc = + checkLocationFromFieldAccessNode(md, nametable, (FieldAccessNode) en, loc, constraint); break; case Kind.NameNode: - compLoc = checkLocationFromNameNode(md, nametable, (NameNode) en, loc); + compLoc = checkLocationFromNameNode(md, nametable, (NameNode) en, loc, constraint); break; case Kind.OpNode: - compLoc = checkLocationFromOpNode(md, nametable, (OpNode) en); + compLoc = checkLocationFromOpNode(md, nametable, (OpNode) en, constraint); break; case Kind.CreateObjectNode: @@ -694,7 +631,8 @@ public class FlowDownCheck { break; case Kind.ArrayAccessNode: - compLoc = checkLocationFromArrayAccessNode(md, nametable, (ArrayAccessNode) en); + compLoc = + checkLocationFromArrayAccessNode(md, nametable, (ArrayAccessNode) en, constraint, isLHS); break; case Kind.LiteralNode: @@ -702,15 +640,16 @@ public class FlowDownCheck { break; case Kind.MethodInvokeNode: - compLoc = checkLocationFromMethodInvokeNode(md, nametable, (MethodInvokeNode) en, loc); + compLoc = + checkLocationFromMethodInvokeNode(md, nametable, (MethodInvokeNode) en, loc, constraint); break; case Kind.TertiaryNode: - compLoc = checkLocationFromTertiaryNode(md, nametable, (TertiaryNode) en); + compLoc = checkLocationFromTertiaryNode(md, nametable, (TertiaryNode) en, constraint); break; case Kind.CastNode: - compLoc = checkLocationFromCastNode(md, nametable, (CastNode) en); + compLoc = checkLocationFromCastNode(md, nametable, (CastNode) en, constraint); break; // case Kind.InstanceOfNode: @@ -740,25 +679,29 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromCastNode(MethodDescriptor md, SymbolTable nametable, - CastNode cn) { + CastNode cn, CompositeLocation constraint) { ExpressionNode en = cn.getExpression(); - return checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation()); + return checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint, + false); } private CompositeLocation checkLocationFromTertiaryNode(MethodDescriptor md, - SymbolTable nametable, TertiaryNode tn) { + SymbolTable nametable, TertiaryNode tn, CompositeLocation constraint) { ClassDescriptor cd = md.getClassDesc(); CompositeLocation condLoc = - checkLocationFromExpressionNode(md, nametable, tn.getCond(), new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, tn.getCond(), new CompositeLocation(), + constraint, false); addLocationType(tn.getCond().getType(), condLoc); CompositeLocation trueLoc = - checkLocationFromExpressionNode(md, nametable, tn.getTrueExpr(), new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, tn.getTrueExpr(), new CompositeLocation(), + constraint, false); addLocationType(tn.getTrueExpr().getType(), trueLoc); CompositeLocation falseLoc = - checkLocationFromExpressionNode(md, nametable, tn.getFalseExpr(), new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, tn.getFalseExpr(), new CompositeLocation(), + constraint, false); addLocationType(tn.getFalseExpr().getType(), falseLoc); // locations from true/false branches can be TOP when there are only literal @@ -790,15 +733,16 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromMethodInvokeNode(MethodDescriptor md, - SymbolTable nametable, MethodInvokeNode min, CompositeLocation loc) { + SymbolTable nametable, MethodInvokeNode min, CompositeLocation loc, + CompositeLocation constraint) { - checkCalleeConstraints(md, nametable, min); + checkCalleeConstraints(md, nametable, min, constraint); CompositeLocation baseLocation = null; if (min.getExpression() != null) { baseLocation = checkLocationFromExpressionNode(md, nametable, min.getExpression(), - new CompositeLocation()); + new CompositeLocation(), constraint, false); } else { String thisLocId = ssjava.getMethodLattice(md).getThisLoc(); baseLocation = new CompositeLocation(new Location(md, thisLocId)); @@ -808,7 +752,7 @@ public class FlowDownCheck { // If method has a return value, compute the highest possible return // location in the caller's perspective CompositeLocation ceilingLoc = - computeCeilingLocationForCaller(md, nametable, min, baseLocation); + computeCeilingLocationForCaller(md, nametable, min, baseLocation, constraint); return ceilingLoc; } @@ -817,7 +761,8 @@ public class FlowDownCheck { } private CompositeLocation computeCeilingLocationForCaller(MethodDescriptor md, - SymbolTable nametable, MethodInvokeNode min, CompositeLocation baseLocation) { + SymbolTable nametable, MethodInvokeNode min, CompositeLocation baseLocation, + CompositeLocation constraint) { List argList = new ArrayList(); // by default, method has a THIS parameter @@ -826,7 +771,8 @@ public class FlowDownCheck { for (int i = 0; i < min.numArgs(); i++) { ExpressionNode en = min.getArg(i); CompositeLocation callerArg = - checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint, + false); argList.add(callerArg); } @@ -840,7 +786,7 @@ public class FlowDownCheck { } private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable, - MethodInvokeNode min) { + MethodInvokeNode min, CompositeLocation constraint) { if (min.numArgs() > 1) { // caller needs to guarantee that it passes arguments in regarding to @@ -848,7 +794,8 @@ public class FlowDownCheck { for (int i = 0; i < min.numArgs(); i++) { ExpressionNode en = min.getArg(i); CompositeLocation callerArg1 = - checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint, + false); VarDescriptor calleevd = (VarDescriptor) min.getMethod().getParameter(i); CompositeLocation calleeLoc1 = d2loc.get(calleevd); @@ -861,7 +808,8 @@ public class FlowDownCheck { ExpressionNode argExp = min.getArg(currentIdx); CompositeLocation callerArg2 = - checkLocationFromExpressionNode(md, nametable, argExp, new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, argExp, new CompositeLocation(), + constraint, false); VarDescriptor calleevd2 = (VarDescriptor) min.getMethod().getParameter(currentIdx); CompositeLocation calleeLoc2 = d2loc.get(calleevd2); @@ -894,25 +842,32 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromArrayAccessNode(MethodDescriptor md, - SymbolTable nametable, ArrayAccessNode aan) { - - // return glb location of array itself and index + SymbolTable nametable, ArrayAccessNode aan, CompositeLocation constraint, boolean isLHS) { ClassDescriptor cd = md.getClassDesc(); - Set glbInputSet = new HashSet(); - CompositeLocation arrayLoc = - checkLocationFromExpressionNode(md, nametable, aan.getExpression(), new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, aan.getExpression(), + new CompositeLocation(), constraint, isLHS); // addTypeLocation(aan.getExpression().getType(), arrayLoc); - glbInputSet.add(arrayLoc); CompositeLocation indexLoc = - checkLocationFromExpressionNode(md, nametable, aan.getIndex(), new CompositeLocation()); - glbInputSet.add(indexLoc); + checkLocationFromExpressionNode(md, nametable, aan.getIndex(), new CompositeLocation(), + constraint, isLHS); // addTypeLocation(aan.getIndex().getType(), indexLoc); - CompositeLocation glbLoc = CompositeLattice.calculateGLB(glbInputSet); - return glbLoc; + if (isLHS) { + if (!CompositeLattice.isGreaterThan(indexLoc, arrayLoc, generateErrorMessage(cd, aan))) { + throw new Error("Array index value is not higher than array location at " + + generateErrorMessage(cd, aan)); + } + return arrayLoc; + } else { + Set inputGLB = new HashSet(); + inputGLB.add(arrayLoc); + inputGLB.add(indexLoc); + return CompositeLattice.calculateGLB(inputGLB); + } + } private CompositeLocation checkLocationFromCreateObjectNode(MethodDescriptor md, @@ -927,16 +882,18 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromOpNode(MethodDescriptor md, SymbolTable nametable, - OpNode on) { + OpNode on, CompositeLocation constraint) { ClassDescriptor cd = md.getClassDesc(); CompositeLocation leftLoc = new CompositeLocation(); - leftLoc = checkLocationFromExpressionNode(md, nametable, on.getLeft(), leftLoc); + leftLoc = + checkLocationFromExpressionNode(md, nametable, on.getLeft(), leftLoc, constraint, false); // addTypeLocation(on.getLeft().getType(), leftLoc); CompositeLocation rightLoc = new CompositeLocation(); if (on.getRight() != null) { - rightLoc = checkLocationFromExpressionNode(md, nametable, on.getRight(), rightLoc); + rightLoc = + checkLocationFromExpressionNode(md, nametable, on.getRight(), rightLoc, constraint, false); // addTypeLocation(on.getRight().getType(), rightLoc); } @@ -1004,11 +961,12 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromNameNode(MethodDescriptor md, SymbolTable nametable, - NameNode nn, CompositeLocation loc) { + NameNode nn, CompositeLocation loc, CompositeLocation constraint) { NameDescriptor nd = nn.getName(); if (nd.getBase() != null) { - loc = checkLocationFromExpressionNode(md, nametable, nn.getExpression(), loc); + loc = + checkLocationFromExpressionNode(md, nametable, nn.getExpression(), loc, constraint, false); } else { String varname = nd.toString(); if (varname.equals("this")) { @@ -1086,7 +1044,8 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromFieldAccessNode(MethodDescriptor md, - SymbolTable nametable, FieldAccessNode fan, CompositeLocation loc) { + SymbolTable nametable, FieldAccessNode fan, CompositeLocation loc, + CompositeLocation constraint) { ExpressionNode left = fan.getExpression(); TypeDescriptor ltd = left.getType(); @@ -1107,7 +1066,7 @@ public class FlowDownCheck { } } - loc = checkLocationFromExpressionNode(md, nametable, left, loc); + loc = checkLocationFromExpressionNode(md, nametable, left, loc, constraint, false); if (!left.getType().isPrimitive()) { Location fieldLoc = getFieldLocation(fd); loc.addLocation(fieldLoc); @@ -1131,44 +1090,65 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md, - SymbolTable nametable, AssignmentNode an, CompositeLocation loc) { + SymbolTable nametable, AssignmentNode an, CompositeLocation loc, CompositeLocation constraint) { + + System.out.println("\n# ASSIGNMENTNODE=" + an.printNode(0)); ClassDescriptor cd = md.getClassDesc(); + Set inputGLBSet = new HashSet(); + boolean postinc = true; if (an.getOperation().getBaseOp() == null || (an.getOperation().getBaseOp().getOp() != Operation.POSTINC && an.getOperation() .getBaseOp().getOp() != Operation.POSTDEC)) postinc = false; + // if LHS is array access node, need to check if array index is higher + // than array itself CompositeLocation destLocation = - checkLocationFromExpressionNode(md, nametable, an.getDest(), new CompositeLocation()); + checkLocationFromExpressionNode(md, nametable, an.getDest(), new CompositeLocation(), + constraint, true); - CompositeLocation srcLocation = new CompositeLocation(); + CompositeLocation rhsLocation; + CompositeLocation srcLocation; if (!postinc) { - if (hasOnlyLiteralValue(an.getSrc())) { - // if source is literal value, src location is TOP. so do not need to - // compare! - return destLocation; + rhsLocation = + checkLocationFromExpressionNode(md, nametable, an.getSrc(), new CompositeLocation(), + constraint, false); + + System.out.println("dstLocation=" + destLocation); + System.out.println("rhsLocation=" + rhsLocation); + System.out.println("constraint=" + constraint); + + if (constraint != null) { + inputGLBSet.add(rhsLocation); + inputGLBSet.add(constraint); + srcLocation = CompositeLattice.calculateGLB(inputGLBSet); + } else { + srcLocation = rhsLocation; } - srcLocation = new CompositeLocation(); - srcLocation = checkLocationFromExpressionNode(md, nametable, an.getSrc(), srcLocation); - - System.out.println("\n an= " + an.printNode(0) + " an.getSrc()=" + - an.getSrc().getClass() - + " at " + cd.getSourceFileName() + "::" + an.getNumLine()); - System.out.println("srcLocation=" + srcLocation); - System.out.println("dstLocation=" + destLocation); if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) { throw new Error("The value flow from " + srcLocation + " to " + destLocation + " does not respect location hierarchy on the assignment " + an.printNode(0) + " at " + cd.getSourceFileName() + "::" + an.getNumLine()); } + } else { destLocation = - srcLocation = checkLocationFromExpressionNode(md, nametable, an.getDest(), srcLocation); + rhsLocation = + checkLocationFromExpressionNode(md, nametable, an.getDest(), new CompositeLocation(), + constraint, false); + + if (constraint != null) { + inputGLBSet.add(rhsLocation); + inputGLBSet.add(constraint); + srcLocation = CompositeLattice.calculateGLB(inputGLBSet); + } else { + srcLocation = rhsLocation; + } if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) { throw new Error("Location " + destLocation @@ -1322,14 +1302,6 @@ public class FlowDownCheck { assignLocationOfVarDescriptor(vd, md, nametable, dn); } - private void checkClass(ClassDescriptor cd) { - // Check to see that methods respects ss property - for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { - MethodDescriptor md = (MethodDescriptor) method_it.next(); - checkMethodDeclaration(cd, md); - } - } - private void checkDeclarationInClass(ClassDescriptor cd) { // Check to see that fields are okay for (Iterator field_it = cd.getFields(); field_it.hasNext();) { @@ -1345,10 +1317,6 @@ public class FlowDownCheck { } } - private void checkMethodDeclaration(ClassDescriptor cd, MethodDescriptor md) { - // TODO - } - private Location checkFieldDeclaration(ClassDescriptor cd, FieldDescriptor fd) { Vector annotationVec = fd.getType().getAnnotationMarkers(); @@ -1491,9 +1459,9 @@ public class FlowDownCheck { if (d1 == null && d2 == null) { throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2 + " because they are not comparable at " + msg); - } else if (d1 != null && d1SubClassesSet.contains(d2)) { + } else if (d1SubClassesSet != null && d1SubClassesSet.contains(d2)) { descriptor = d1; - } else if (d2 != null && d2SubClassesSet.contains(d1)) { + } else if (d2SubClassesSet != null && d2SubClassesSet.contains(d1)) { descriptor = d2; } else { throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2 diff --git a/Robust/src/Tests/ssJava/flowdown/makefile b/Robust/src/Tests/ssJava/flowdown/makefile index bcb8fdc9..b6d1119d 100644 --- a/Robust/src/Tests/ssJava/flowdown/makefile +++ b/Robust/src/Tests/ssJava/flowdown/makefile @@ -3,7 +3,7 @@ BUILDSCRIPT=../../../buildscript PROGRAM=test SOURCE_FILES=test.java -BSFLAGS= -32bit -ssjava -printlinenum -mainclass $(PROGRAM) -heapsize-mb 1000 -garbagestats -joptimize -optimize -debug #-nooptimize #src-after-pp #-debug +BSFLAGS= -32bit -ssjava -ssjavadebug -printlinenum -mainclass $(PROGRAM) -heapsize-mb 1000 -garbagestats -joptimize -optimize -debug #-nooptimize #src-after-pp #-debug default: $(PROGRAM)s.bin -- 2.34.1