From: yeom Date: Wed, 27 Apr 2011 23:54:45 +0000 (+0000) Subject: changes to get the tiny class library for ssjava X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=c7f531ddf7a7d0dd1500b11ab6e3108c8924f796;p=IRC.git changes to get the tiny class library for ssjava --- diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index 5d0b3dc7..e4472229 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -61,12 +61,12 @@ public class FlowDownCheck { Hashtable cd2lattice = state.getCd2LocationOrder(); Set cdSet = cd2lattice.keySet(); - for (Iterator iterator = cdSet.iterator(); iterator.hasNext(); ) { + for (Iterator iterator = cdSet.iterator(); iterator.hasNext();) { ClassDescriptor cd = (ClassDescriptor) iterator.next(); - Lattice lattice = (Lattice)cd2lattice.get(cd); + Lattice lattice = (Lattice) cd2lattice.get(cd); Set locIdSet = lattice.getKeySet(); - for (Iterator iterator2 = locIdSet.iterator(); iterator2.hasNext(); ) { + for (Iterator iterator2 = locIdSet.iterator(); iterator2.hasNext();) { String locID = (String) iterator2.next(); id2cd.put(locID, cd); } @@ -85,27 +85,27 @@ public class FlowDownCheck { Object obj = toanalyze.iterator().next(); ClassDescriptor cd = (ClassDescriptor) obj; toanalyze.remove(cd); -// if (cd.isClassLibrary()) { - // doesn't care about class libraries now -// continue; -// } - checkDeclarationInClass(cd); - for (Iterator method_it = cd.getMethods(); method_it.hasNext(); ) { - MethodDescriptor md = (MethodDescriptor) method_it.next(); - try { - checkDeclarationInMethodBody(cd, md); - } catch (Error e) { - System.out.println("Error in " + md); - throw e; + + if(!cd.isInterface()){ + checkDeclarationInClass(cd); + for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { + MethodDescriptor md = (MethodDescriptor) method_it.next(); + try { + checkDeclarationInMethodBody(cd, md); + } catch (Error e) { + System.out.println("Error in " + md); + throw e; + } } } + } // post-processing for delta location // for a nested delta location, assigning a concrete reference to delta // operand Set tdSet = td2loc.keySet(); - for (Iterator iterator = tdSet.iterator(); iterator.hasNext(); ) { + for (Iterator iterator = tdSet.iterator(); iterator.hasNext();) { Descriptor td = (Descriptor) iterator.next(); Location loc = td2loc.get(td); @@ -114,17 +114,17 @@ public class FlowDownCheck { CompositeLocation compLoc = (CompositeLocation) loc; Location locElement = compLoc.getTuple().at(0); - assert(locElement instanceof DeltaLocation); + assert (locElement instanceof DeltaLocation); DeltaLocation delta = (DeltaLocation) locElement; Descriptor refType = delta.getRefLocationId(); if (refType != null) { Location refLoc = td2loc.get(refType); - assert(refLoc instanceof CompositeLocation); + assert (refLoc instanceof CompositeLocation); CompositeLocation refCompLoc = (CompositeLocation) refLoc; - assert(refCompLoc.getTuple().at(0) instanceof DeltaLocation); + assert (refCompLoc.getTuple().at(0) instanceof DeltaLocation); DeltaLocation refDelta = (DeltaLocation) refCompLoc.getTuple().at(0); delta.addDeltaOperand(refDelta); @@ -141,12 +141,9 @@ public class FlowDownCheck { Object obj = toanalyze.iterator().next(); ClassDescriptor cd = (ClassDescriptor) obj; toanalyze.remove(cd); -// if (cd.isClassLibrary()) { - // doesn't care about class libraries now -// continue; -// } + checkClass(cd); - for (Iterator method_it = cd.getMethods(); method_it.hasNext(); ) { + for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { MethodDescriptor md = (MethodDescriptor) method_it.next(); try { checkMethodBody(cd, md); @@ -182,7 +179,7 @@ public class FlowDownCheck { } private void checkDeclarationInBlockStatementNode(MethodDescriptor md, SymbolTable nametable, - BlockStatementNode bsn) { + BlockStatementNode bsn) { switch (bsn.kind()) { case Kind.SubBlockNode: @@ -221,7 +218,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromBlockNode(MethodDescriptor md, SymbolTable nametable, - BlockNode bn) { + BlockNode bn) { // it will return the lowest location in the block node CompositeLocation lowestLoc = null; for (int i = 0; i < bn.size(); i++) { @@ -240,7 +237,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromBlockStatementNode(MethodDescriptor md, - SymbolTable nametable, BlockStatementNode bsn) { + SymbolTable nametable, BlockStatementNode bsn) { CompositeLocation compLoc = null; switch (bsn.kind()) { @@ -268,23 +265,23 @@ public class FlowDownCheck { compLoc = checkLocationFromSubBlockNode(md, nametable, (SubBlockNode) bsn); break; - // case Kind.ContinueBreakNode: - // checkLocationFromContinueBreakNode(md, nametable,(ContinueBreakNode) - // bsn); - // return null; + // case Kind.ContinueBreakNode: + // checkLocationFromContinueBreakNode(md, nametable,(ContinueBreakNode) + // bsn); + // return null; } return compLoc; } private CompositeLocation checkLocationFromLoopNode(MethodDescriptor md, SymbolTable nametable, - LoopNode ln) { + LoopNode ln) { ClassDescriptor cd = md.getClassDesc(); if (ln.getType() == LoopNode.WHILELOOP || ln.getType() == LoopNode.DOWHILELOOP) { CompositeLocation condLoc = - checkLocationFromExpressionNode(md, nametable, ln.getCondition(), new CompositeLocation( - cd)); + checkLocationFromExpressionNode(md, nametable, ln.getCondition(), new CompositeLocation( + cd)); addTypeLocation(ln.getCondition().getType(), (condLoc)); CompositeLocation bodyLoc = checkLocationFromBlockNode(md, nametable, ln.getBody()); @@ -292,8 +289,8 @@ public class FlowDownCheck { if (!CompositeLattice.isGreaterThan(condLoc, bodyLoc, cd)) { // 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()); + "The location of the while-condition statement is lower than the loop body at " + + cd.getSourceFileName() + ":" + ln.getCondition().getNumLine()); } return bodyLoc; @@ -304,12 +301,12 @@ public class FlowDownCheck { // calculate glb location of condition and update statements CompositeLocation condLoc = - checkLocationFromExpressionNode(md, bn.getVarTable(), ln.getCondition(), - new CompositeLocation(cd)); + checkLocationFromExpressionNode(md, bn.getVarTable(), ln.getCondition(), + new CompositeLocation(cd)); addTypeLocation(ln.getCondition().getType(), condLoc); CompositeLocation updateLoc = - checkLocationFromBlockNode(md, bn.getVarTable(), ln.getUpdate()); + checkLocationFromBlockNode(md, bn.getVarTable(), ln.getUpdate()); Set glbInputSet = new HashSet(); glbInputSet.add(condLoc); @@ -325,8 +322,8 @@ public class FlowDownCheck { if (!CompositeLattice.isGreaterThan(glbLocOfForLoopCond, blockLoc, cd)) { throw new Error( - "The location of the for-condition statement is lower than the for-loop body at " - + cd.getSourceFileName() + ":" + ln.getCondition().getNumLine()); + "The location of the for-condition statement is lower than the for-loop body at " + + cd.getSourceFileName() + ":" + ln.getCondition().getNumLine()); } return blockLoc; } @@ -334,20 +331,20 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromSubBlockNode(MethodDescriptor md, - SymbolTable nametable, SubBlockNode sbn) { + SymbolTable nametable, SubBlockNode sbn) { CompositeLocation compLoc = checkLocationFromBlockNode(md, nametable, sbn.getBlockNode()); return compLoc; } private CompositeLocation checkLocationFromIfStatementNode(MethodDescriptor md, - SymbolTable nametable, IfStatementNode isn) { + SymbolTable nametable, IfStatementNode isn) { ClassDescriptor localCD = md.getClassDesc(); Set glbInputSet = new HashSet(); CompositeLocation condLoc = - checkLocationFromExpressionNode(md, nametable, isn.getCondition(), new CompositeLocation( - localCD)); + checkLocationFromExpressionNode(md, nametable, isn.getCondition(), new CompositeLocation( + localCD)); addTypeLocation(isn.getCondition().getType(), condLoc); glbInputSet.add(condLoc); @@ -360,20 +357,20 @@ public class FlowDownCheck { if (!CompositeLattice.isGreaterThan(condLoc, locTrueBlock, localCD)) { // error throw new Error( - "The location of the if-condition statement is lower than the conditional block at " - + localCD.getSourceFileName() + ":" + isn.getCondition().getNumLine()); + "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()); + checkLocationFromBlockNode(md, nametable, isn.getFalseBlock()); glbInputSet.add(locFalseBlock); if (!CompositeLattice.isGreaterThan(condLoc, locFalseBlock, localCD)) { // error throw new Error( - "The location of the if-condition statement is lower than the conditional block at " - + localCD.getSourceFileName() + ":" + isn.getCondition().getNumLine()); + "The location of the if-condition statement is lower than the conditional block at " + + localCD.getSourceFileName() + ":" + isn.getCondition().getNumLine()); } } @@ -385,7 +382,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromDeclarationNode(MethodDescriptor md, - SymbolTable nametable, DeclarationNode dn) { + SymbolTable nametable, DeclarationNode dn) { VarDescriptor vd = dn.getVarDescriptor(); Location destLoc = td2loc.get(vd); @@ -393,15 +390,15 @@ public class FlowDownCheck { ClassDescriptor localCD = md.getClassDesc(); if (dn.getExpression() != null) { CompositeLocation expressionLoc = - checkLocationFromExpressionNode(md, nametable, dn.getExpression(), new CompositeLocation( - localCD)); + checkLocationFromExpressionNode(md, nametable, dn.getExpression(), new CompositeLocation( + localCD)); addTypeLocation(dn.getExpression().getType(), expressionLoc); if (expressionLoc != null) { // checking location order if (!CompositeLattice.isGreaterThan(expressionLoc, destLoc, localCD)) { throw new Error("The value flow from " + expressionLoc + " to " + destLoc - + " does not respect location hierarchy on the assignment " + dn.printNode(0)); + + " does not respect location hierarchy on the assignment " + dn.printNode(0)); } } return expressionLoc; @@ -413,20 +410,20 @@ public class FlowDownCheck { } private void checkDeclarationInSubBlockNode(MethodDescriptor md, SymbolTable nametable, - SubBlockNode sbn) { + SubBlockNode sbn) { checkDeclarationInBlockNode(md, nametable, sbn.getBlockNode()); } private CompositeLocation checkLocationFromBlockExpressionNode(MethodDescriptor md, - SymbolTable nametable, BlockExpressionNode ben) { + SymbolTable nametable, BlockExpressionNode ben) { CompositeLocation compLoc = - checkLocationFromExpressionNode(md, nametable, ben.getExpression(), null); + checkLocationFromExpressionNode(md, nametable, ben.getExpression(), null); 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 compLoc = null; switch (en.kind()) { @@ -495,30 +492,30 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromTertiaryNode(MethodDescriptor md, - SymbolTable nametable, TertiaryNode tn) { + SymbolTable nametable, TertiaryNode tn) { ClassDescriptor cd = md.getClassDesc(); CompositeLocation condLoc = - checkLocationFromExpressionNode(md, nametable, tn.getCond(), new CompositeLocation(cd)); + checkLocationFromExpressionNode(md, nametable, tn.getCond(), new CompositeLocation(cd)); addTypeLocation(tn.getCond().getType(), condLoc); CompositeLocation trueLoc = - checkLocationFromExpressionNode(md, nametable, tn.getTrueExpr(), new CompositeLocation(cd)); + checkLocationFromExpressionNode(md, nametable, tn.getTrueExpr(), new CompositeLocation(cd)); addTypeLocation(tn.getTrueExpr().getType(), trueLoc); CompositeLocation falseLoc = - checkLocationFromExpressionNode(md, nametable, tn.getFalseExpr(), new CompositeLocation(cd)); + checkLocationFromExpressionNode(md, nametable, tn.getFalseExpr(), new CompositeLocation(cd)); addTypeLocation(tn.getFalseExpr().getType(), falseLoc); // check if condLoc is higher than trueLoc & falseLoc if (!CompositeLattice.isGreaterThan(condLoc, trueLoc, cd)) { throw new Error( - "The location of the condition expression is lower than the true expression at " - + cd.getSourceFileName() + ":" + tn.getCond().getNumLine()); + "The location of the condition expression is lower than the true expression at " + + cd.getSourceFileName() + ":" + tn.getCond().getNumLine()); } if (!CompositeLattice.isGreaterThan(condLoc, falseLoc, cd)) { throw new Error( - "The location of the condition expression is lower than the true expression at " - + cd.getSourceFileName() + ":" + tn.getCond().getNumLine()); + "The location of the condition expression is lower than the true expression at " + + cd.getSourceFileName() + ":" + tn.getCond().getNumLine()); } // then, return glb of trueLoc & falseLoc @@ -530,7 +527,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromMethodInvokeNode(MethodDescriptor md, - SymbolTable nametable, MethodInvokeNode min) { + SymbolTable nametable, MethodInvokeNode min) { ClassDescriptor cd = md.getClassDesc(); @@ -542,7 +539,7 @@ public class FlowDownCheck { for (int i = 0; i < min.numArgs(); i++) { ExpressionNode en = min.getArg(i); CompositeLocation callerArg1 = - checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(cd)); + checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(cd)); ClassDescriptor calleecd = min.getMethod().getClassDesc(); VarDescriptor calleevd = (VarDescriptor) min.getMethod().getParameter(i); @@ -555,13 +552,13 @@ public class FlowDownCheck { if (currentIdx != i) { // skip itself ExpressionNode argExp = min.getArg(currentIdx); CompositeLocation callerArg2 = - checkLocationFromExpressionNode(md, nametable, argExp, new CompositeLocation(cd)); + checkLocationFromExpressionNode(md, nametable, argExp, new CompositeLocation(cd)); VarDescriptor calleevd2 = (VarDescriptor) min.getMethod().getParameter(currentIdx); Location calleeLoc2 = td2loc.get(calleevd2); boolean callerResult = CompositeLattice.isGreaterThan(callerArg1, callerArg2, cd); boolean calleeResult = - CompositeLattice.isGreaterThan(calleeLoc1, calleeLoc2, calleecd); + CompositeLattice.isGreaterThan(calleeLoc1, calleeLoc2, calleecd); if (calleeResult && !callerResult) { // in callee, calleeLoc1 is higher than calleeLoc2 @@ -569,7 +566,7 @@ public class FlowDownCheck { // callerLoc1 & callerLoc2 throw new Error("Caller doesn't respect ordering relations among method arguments:" - + cd.getSourceFileName() + ":" + min.getNumLine()); + + cd.getSourceFileName() + ":" + min.getNumLine()); } } @@ -587,7 +584,7 @@ public class FlowDownCheck { for (int i = 0; i < min.numArgs(); i++) { ExpressionNode en = min.getArg(i); CompositeLocation argLoc = - checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(cd)); + checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(cd)); addTypeLocation(en.getType(), argLoc); argLocSet.add(argLoc); } @@ -604,7 +601,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromArrayAccessNode(MethodDescriptor md, - SymbolTable nametable, ArrayAccessNode aan) { + SymbolTable nametable, ArrayAccessNode aan) { // return glb location of array itself and index @@ -613,13 +610,13 @@ public class FlowDownCheck { Set glbInputSet = new HashSet(); CompositeLocation arrayLoc = - checkLocationFromExpressionNode(md, nametable, aan.getExpression(), new CompositeLocation( - cd)); + checkLocationFromExpressionNode(md, nametable, aan.getExpression(), new CompositeLocation( + cd)); addTypeLocation(aan.getExpression().getType(), arrayLoc); glbInputSet.add(arrayLoc); CompositeLocation indexLoc = - checkLocationFromExpressionNode(md, nametable, aan.getIndex(), new CompositeLocation(cd)); + checkLocationFromExpressionNode(md, nametable, aan.getIndex(), new CompositeLocation(cd)); glbInputSet.add(indexLoc); addTypeLocation(aan.getIndex().getType(), indexLoc); @@ -628,7 +625,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromCreateObjectNode(MethodDescriptor md, - SymbolTable nametable, CreateObjectNode con) { + SymbolTable nametable, CreateObjectNode con) { ClassDescriptor cd = md.getClassDesc(); @@ -637,7 +634,7 @@ public class FlowDownCheck { for (int i = 0; i < con.numArgs(); i++) { ExpressionNode en = con.getArg(i); CompositeLocation argLoc = - checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(cd)); + checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(cd)); glbInputSet.add(argLoc); addTypeLocation(en.getType(), argLoc); } @@ -659,7 +656,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromOpNode(MethodDescriptor md, SymbolTable nametable, - OpNode on) { + OpNode on) { ClassDescriptor cd = md.getClassDesc(); CompositeLocation leftLoc = new CompositeLocation(cd); @@ -724,7 +721,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromLiteralNode(MethodDescriptor md, - SymbolTable nametable, LiteralNode en, CompositeLocation loc) { + SymbolTable nametable, LiteralNode en, CompositeLocation loc) { // literal value has the top location so that value can be flowed into any // location @@ -735,7 +732,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromNameNode(MethodDescriptor md, SymbolTable nametable, - NameNode nn, CompositeLocation loc) { + NameNode nn, CompositeLocation loc) { NameDescriptor nd = nn.getName(); if (nd.getBase() != null) { @@ -754,7 +751,7 @@ public class FlowDownCheck { FieldDescriptor fd = (FieldDescriptor) d; localLoc = td2loc.get(fd); } - assert(localLoc != null); + assert (localLoc != null); if (localLoc instanceof CompositeLocation) { loc = (CompositeLocation) localLoc; @@ -767,7 +764,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromFieldAccessNode(MethodDescriptor md, - SymbolTable nametable, FieldAccessNode fan, CompositeLocation loc) { + SymbolTable nametable, FieldAccessNode fan, CompositeLocation loc) { FieldDescriptor fd = fan.getField(); Location fieldLoc = td2loc.get(fd); @@ -780,7 +777,7 @@ public class FlowDownCheck { } private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md, - SymbolTable nametable, AssignmentNode an, CompositeLocation loc) { + SymbolTable nametable, AssignmentNode an, CompositeLocation loc) { ClassDescriptor cd = md.getClassDesc(); boolean postinc = true; @@ -790,7 +787,7 @@ public class FlowDownCheck { postinc = false; CompositeLocation destLocation = - checkLocationFromExpressionNode(md, nametable, an.getDest(), new CompositeLocation(cd)); + checkLocationFromExpressionNode(md, nametable, an.getDest(), new CompositeLocation(cd)); CompositeLocation srcLocation = new CompositeLocation(cd); if (!postinc) { @@ -799,20 +796,20 @@ public class FlowDownCheck { if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, cd)) { throw new Error("The value flow from " + srcLocation + " to " + destLocation - + " does not respect location hierarchy on the assignment " + an.printNode(0)); + + " does not respect location hierarchy on the assignment " + an.printNode(0)); } } else { destLocation = - srcLocation = checkLocationFromExpressionNode(md, nametable, an.getDest(), srcLocation); + srcLocation = checkLocationFromExpressionNode(md, nametable, an.getDest(), srcLocation); - if (!((Set)state.getCd2LocationPropertyMap().get(cd)).contains(destLocation - .getLocation(cd).getLocIdentifier())) { + if (!((Set) state.getCd2LocationPropertyMap().get(cd)).contains(destLocation + .getLocation(cd).getLocIdentifier())) { throw new Error("Location " + destLocation + " is not allowed to have spinning values at " - + cd.getSourceFileName() + ":" + an.getNumLine()); + + cd.getSourceFileName() + ":" + an.getNumLine()); } } - if(an.getSrc()!=null) { + if (an.getSrc() != null) { addTypeLocation(an.getSrc().getType(), srcLocation); } addTypeLocation(an.getDest().getType(), destLocation); @@ -821,7 +818,7 @@ public class FlowDownCheck { } private void assignLocationOfVarDescriptor(VarDescriptor vd, MethodDescriptor md, - SymbolTable nametable, TreeNode n) { + SymbolTable nametable, TreeNode n) { ClassDescriptor cd = md.getClassDesc(); Vector annotationVec = vd.getType().getAnnotationMarkers(); @@ -829,7 +826,7 @@ public class FlowDownCheck { // currently enforce every variable to have corresponding location if (annotationVec.size() == 0) { throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method " - + md.getSymbol() + " of the class " + cd.getSymbol()); + + md.getSymbol() + " of the class " + cd.getSymbol()); } if (annotationVec.size() > 1) { @@ -839,37 +836,35 @@ public class FlowDownCheck { AnnotationDescriptor ad = annotationVec.elementAt(0); - if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) { - - // check if location is defined - String locationID = ad.getMarker(); - Lattice lattice = (Lattice)state.getCd2LocationOrder().get(cd); - - if (lattice == null || (!lattice.containsKey(locationID))) { - throw new Error("Location " + locationID - + " is not defined in the location hierarchy of class " + cd.getSymbol() + "."); - } - - Location loc = new Location(cd, locationID); - td2loc.put(vd, loc); - addTypeLocation(vd.getType(), loc); + if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) { - } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) { - if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) { + if (ad.getMarker().equals(SSJavaAnalysis.LOC)) { + String locationID = ad.getValue(); + // check if location is defined + Lattice lattice = (Lattice) state.getCd2LocationOrder().get(cd); + if (lattice == null || (!lattice.containsKey(locationID))) { + throw new Error("Location " + locationID + + " is not defined in the location hierarchy of class " + cd.getSymbol() + "."); + } + Location loc = new Location(cd, locationID); + td2loc.put(vd, loc); + addTypeLocation(vd.getType(), loc); + + } else if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) { CompositeLocation compLoc = new CompositeLocation(cd); - if (ad.getData().length() == 0) { + if (ad.getValue().length() == 0) { throw new Error("Delta function of " + vd.getSymbol() + " does not have any locations: " - + cd.getSymbol() + "."); + + cd.getSymbol() + "."); } - String deltaStr = ad.getData(); + String deltaStr = ad.getValue(); if (deltaStr.startsWith("LOC(")) { if (!deltaStr.endsWith(")")) { throw new Error("The declaration of the delta location is wrong at " - + cd.getSourceFileName() + ":" + n.getNumLine()); + + cd.getSourceFileName() + ":" + n.getNumLine()); } String locationOperand = deltaStr.substring(4, deltaStr.length() - 1); @@ -883,7 +878,7 @@ public class FlowDownCheck { compLoc.addLocation(deltaLoc); } else if (d instanceof FieldDescriptor) { throw new Error("Applying delta operation to the field " + locationOperand - + " is not allowed at " + cd.getSourceFileName() + ":" + n.getNumLine()); + + " is not allowed at " + cd.getSourceFileName() + ":" + n.getNumLine()); } } else { StringTokenizer token = new StringTokenizer(deltaStr, ","); @@ -895,7 +890,7 @@ public class FlowDownCheck { if (deltaCD == null) { // delta operand is not defined in the location hierarchy throw new Error("Delta operand '" + deltaOperand + "' of declaration node '" + vd - + "' is not defined by location hierarchies."); + + "' is not defined by location hierarchies."); } Location loc = new Location(deltaCD, deltaOperand); @@ -920,7 +915,7 @@ public class FlowDownCheck { private void checkClass(ClassDescriptor cd) { // Check to see that methods respects ss property - for (Iterator method_it = cd.getMethods(); method_it.hasNext(); ) { + for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { MethodDescriptor md = (MethodDescriptor) method_it.next(); checkMethodDeclaration(cd, md); } @@ -928,7 +923,7 @@ public class FlowDownCheck { private void checkDeclarationInClass(ClassDescriptor cd) { // Check to see that fields are okay - for (Iterator field_it = cd.getFields(); field_it.hasNext(); ) { + for (Iterator field_it = cd.getFields(); field_it.hasNext();) { FieldDescriptor fd = (FieldDescriptor) field_it.next(); checkFieldDeclaration(cd, fd); } @@ -945,24 +940,24 @@ public class FlowDownCheck { // currently enforce every variable to have corresponding location if (annotationVec.size() == 0) { throw new Error("Location is not assigned to the field " + fd.getSymbol() + " of the class " - + cd.getSymbol()); + + cd.getSymbol()); } if (annotationVec.size() > 1) { // variable can have at most one location throw new Error("Field " + fd.getSymbol() + " of class " + cd - + " has more than one location."); + + " has more than one location."); } // check if location is defined AnnotationDescriptor ad = annotationVec.elementAt(0); if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) { String locationID = annotationVec.elementAt(0).getMarker(); - Lattice lattice = (Lattice)state.getCd2LocationOrder().get(cd); + Lattice lattice = (Lattice) state.getCd2LocationOrder().get(cd); if (lattice == null || (!lattice.containsKey(locationID))) { throw new Error("Location " + locationID - + " is not defined in the location hierarchy of class " + cd.getSymbol() + "."); + + " is not defined in the location hierarchy of class " + cd.getSymbol() + "."); } Location localLoc = new Location(cd, locationID); @@ -972,22 +967,22 @@ public class FlowDownCheck { } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) { if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) { - if (ad.getData().length() == 0) { + if (ad.getValue().length() == 0) { throw new Error("Delta function of " + fd.getSymbol() + " does not have any locations: " - + cd.getSymbol() + "."); + + cd.getSymbol() + "."); } CompositeLocation compLoc = new CompositeLocation(cd); DeltaLocation deltaLoc = new DeltaLocation(cd); - StringTokenizer token = new StringTokenizer(ad.getData(), ","); + StringTokenizer token = new StringTokenizer(ad.getValue(), ","); while (token.hasMoreTokens()) { String deltaOperand = token.nextToken(); ClassDescriptor deltaCD = id2cd.get(deltaOperand); if (deltaCD == null) { // delta operand is not defined in the location hierarchy throw new Error("Delta operand '" + deltaOperand + "' of field node '" + fd - + "' is not defined by location hierarchies."); + + "' is not defined by location hierarchies."); } Location loc = new Location(deltaCD, deltaOperand); @@ -1060,7 +1055,7 @@ public class FlowDownCheck { } private static int compareBaseLocationSet(CompositeLocation compLoc1, - CompositeLocation compLoc2, ClassDescriptor priorityCD) { + CompositeLocation compLoc2, ClassDescriptor priorityCD) { // if compLoc1 is greater than compLoc2, return true // else return false; @@ -1072,22 +1067,22 @@ public class FlowDownCheck { Location priorityLoc1 = cd2loc1.get(priorityCD); Location priorityLoc2 = cd2loc2.get(priorityCD); - assert(priorityLoc1.getClassDescriptor().equals(priorityLoc2.getClassDescriptor())); + assert (priorityLoc1.getClassDescriptor().equals(priorityLoc2.getClassDescriptor())); ClassDescriptor cd = priorityLoc1.getClassDescriptor(); - Lattice locationOrder = (Lattice)state.getCd2LocationOrder().get(cd); + Lattice locationOrder = (Lattice) state.getCd2LocationOrder().get(cd); if (priorityLoc1.getLocIdentifier().equals(priorityLoc2.getLocIdentifier())) { // have the same level of local hierarchy - Set spinSet = (Set)state.getCd2LocationPropertyMap().get(cd); + Set spinSet = (Set) state.getCd2LocationPropertyMap().get(cd); if (spinSet != null && spinSet.contains(priorityLoc1.getLocIdentifier())) { // this location can be spinning return ComparisonResult.GREATER; } } else if (locationOrder.isGreaterThan(priorityLoc1.getLocIdentifier(), - priorityLoc2.getLocIdentifier())) { + priorityLoc2.getLocIdentifier())) { // if priority loc of compLoc1 is higher than compLoc2 // then, compLoc 1 is higher than compLoc2 return ComparisonResult.GREATER; @@ -1101,7 +1096,7 @@ public class FlowDownCheck { Set keySet1 = cd2loc1.keySet(); int numEqualLoc = 0; - for (Iterator iterator = keySet1.iterator(); iterator.hasNext(); ) { + for (Iterator iterator = keySet1.iterator(); iterator.hasNext();) { ClassDescriptor cd1 = (ClassDescriptor) iterator.next(); Location loc1 = cd2loc1.get(cd1); @@ -1118,8 +1113,8 @@ public class FlowDownCheck { } System.out.println("lattice comparison:" + loc1.getLocIdentifier() + " ? " - + loc2.getLocIdentifier()); - locationOrder = (Lattice)state.getCd2LocationOrder().get(cd1); + + loc2.getLocIdentifier()); + locationOrder = (Lattice) state.getCd2LocationOrder().get(cd1); if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) { // have the same level of local hierarchy numEqualLoc++; @@ -1143,7 +1138,7 @@ public class FlowDownCheck { } public static CompositeLocation calculateGLB(ClassDescriptor cd, - Set inputSet, ClassDescriptor priorityCD) { + Set inputSet, ClassDescriptor priorityCD) { CompositeLocation glbCompLoc = new CompositeLocation(cd); int maxDeltaFunction = 0; @@ -1151,10 +1146,10 @@ public class FlowDownCheck { // calculate GLB of priority element first Hashtable> cd2locSet = - new Hashtable>(); + new Hashtable>(); // creating mapping from class to set of locations - for (Iterator iterator = inputSet.iterator(); iterator.hasNext(); ) { + for (Iterator iterator = inputSet.iterator(); iterator.hasNext();) { CompositeLocation compLoc = (CompositeLocation) iterator.next(); int numOfDelta = compLoc.getNumofDelta(); @@ -1163,7 +1158,7 @@ public class FlowDownCheck { } Set baseLocationSet = compLoc.getBaseLocationSet(); - for (Iterator iterator2 = baseLocationSet.iterator(); iterator2.hasNext(); ) { + for (Iterator iterator2 = baseLocationSet.iterator(); iterator2.hasNext();) { Location locElement = (Location) iterator2.next(); ClassDescriptor locCD = locElement.getClassDescriptor(); @@ -1181,19 +1176,19 @@ public class FlowDownCheck { Set locSetofClass = cd2locSet.get(priorityCD); Set locIdentifierSet = new HashSet(); - for (Iterator locIterator = locSetofClass.iterator(); locIterator.hasNext(); ) { + for (Iterator locIterator = locSetofClass.iterator(); locIterator.hasNext();) { Location locElement = locIterator.next(); locIdentifierSet.add(locElement.getLocIdentifier()); } - Lattice locOrder = (Lattice)state.getCd2LocationOrder().get(priorityCD); + Lattice locOrder = (Lattice) state.getCd2LocationOrder().get(priorityCD); String glbLocIdentifer = locOrder.getGLB(locIdentifierSet); Location priorityGLB = new Location(priorityCD, glbLocIdentifer); Set sameGLBLoc = new HashSet(); - for (Iterator iterator = inputSet.iterator(); iterator.hasNext(); ) { + for (Iterator iterator = inputSet.iterator(); iterator.hasNext();) { CompositeLocation inputComploc = iterator.next(); Location locElement = inputComploc.getLocation(priorityCD); @@ -1208,18 +1203,18 @@ public class FlowDownCheck { Set glbElementSet = new HashSet(); - for (Iterator iterator = cd2locSet.keySet().iterator(); iterator.hasNext(); ) { + for (Iterator iterator = cd2locSet.keySet().iterator(); iterator.hasNext();) { ClassDescriptor localCD = iterator.next(); if (!localCD.equals(priorityCD)) { Set localLocSet = cd2locSet.get(localCD); Set LocalLocIdSet = new HashSet(); - for (Iterator locIterator = localLocSet.iterator(); locIterator.hasNext(); ) { + for (Iterator locIterator = localLocSet.iterator(); locIterator.hasNext();) { Location locElement = locIterator.next(); LocalLocIdSet.add(locElement.getLocIdentifier()); } - Lattice localOrder = (Lattice)state.getCd2LocationOrder().get(localCD); + Lattice localOrder = (Lattice) state.getCd2LocationOrder().get(localCD); Location localGLBLoc = new Location(localCD, localOrder.getGLB(LocalLocIdSet)); glbCompLoc.addLocation(localGLBLoc); } @@ -1228,7 +1223,7 @@ public class FlowDownCheck { // if priority glb loc is lower than all of input loc // assign top location to the rest of loc element - for (Iterator iterator = cd2locSet.keySet().iterator(); iterator.hasNext(); ) { + for (Iterator iterator = cd2locSet.keySet().iterator(); iterator.hasNext();) { ClassDescriptor localCD = iterator.next(); if (!localCD.equals(priorityCD)) { Location localGLBLoc = Location.createTopLocation(localCD); diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index 6206b147..86e10841 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -8,6 +8,7 @@ import IR.Tree.TreeNode; public class SSJavaAnalysis { + public static final String LOC="LOC"; public static final String DELTA = "delta"; State state; FlowDownCheck flowDownChecker; diff --git a/Robust/src/ClassLibrary/SSJava/Object.java b/Robust/src/ClassLibrary/SSJava/Object.java index e509356b..df78349d 100644 --- a/Robust/src/ClassLibrary/SSJava/Object.java +++ b/Robust/src/ClassLibrary/SSJava/Object.java @@ -1,4 +1,9 @@ public class Object { + + locdef{ + data + } + public native int hashCode(); /* DON'T USE THIS METHOD UNLESS NECESSARY */ @@ -9,7 +14,7 @@ public class Object { return "Object"+hashCode(); } - public boolean equals(Object o) { + public boolean equals(@LOC("data") Object o) { if (o==this) return true; return false; diff --git a/Robust/src/ClassLibrary/SSJava/System.java b/Robust/src/ClassLibrary/SSJava/System.java index f02562b1..aceead97 100644 --- a/Robust/src/ClassLibrary/SSJava/System.java +++ b/Robust/src/ClassLibrary/SSJava/System.java @@ -1,4 +1,9 @@ public class System { + + locdef{ + in + } + public static void printInt(int x) { String s=String.valueOf(x); printString(s); @@ -14,23 +19,23 @@ public class System { public static native void printString(String s); - public static void println(String s) { + public static void println(@LOC("in") String s) { System.printString(s+"\n"); } - public static void println(Object o) { + public static void println(@LOC("in") Object o) { System.printString(""+o+"\n"); } - public static void println(int o) { + public static void println(@LOC("in") int o) { System.printString(""+o+"\n"); } - public static void println(double o) { + public static void println(@LOC("in") double o) { System.printString(""+o+"\n"); } - public static void println(long o) { + public static void println(@LOC("in") long o) { System.printString(""+o+"\n"); } @@ -38,23 +43,23 @@ public class System { System.printString("\n"); } - public static void print(String s) { + public static void print(@LOC("in") String s) { System.printString(s); } - public static void print(Object o) { + public static void print(@LOC("in") Object o) { System.printString(""+o); } - public static void print(int o) { + public static void print(@LOC("in") int o) { System.printString(""+o); } - public static void print(double o) { + public static void print(@LOC("in") double o) { System.printString(""+o); } - public static void print(long o) { + public static void print(@LOC("in") long o) { System.printString(""+o); } diff --git a/Robust/src/IR/AnnotationDescriptor.java b/Robust/src/IR/AnnotationDescriptor.java index b7282d95..b68a3d64 100644 --- a/Robust/src/IR/AnnotationDescriptor.java +++ b/Robust/src/IR/AnnotationDescriptor.java @@ -9,7 +9,7 @@ public class AnnotationDescriptor extends Descriptor { public static final int FULL_ANNOTATION = 3; private String marker; - private String data; // for single annotation + private String value; // for single annotation private int type; public AnnotationDescriptor(String annotationName) { @@ -19,12 +19,12 @@ public class AnnotationDescriptor extends Descriptor { this.type = MARKER_ANNOTATION; } - public AnnotationDescriptor(String annotationName, String data) { + public AnnotationDescriptor(String annotationName, String value) { // constructor for marker annotation super(annotationName); this.marker = annotationName; this.type = SINGLE_ANNOTATION; - this.data = data; + this.value = value; } public int getType() { @@ -47,8 +47,8 @@ public class AnnotationDescriptor extends Descriptor { return marker; } - public String getData() { - return data; + public String getValue() { + return value; } public boolean equals(Object o) { @@ -68,7 +68,7 @@ public class AnnotationDescriptor extends Descriptor { if (type == MARKER_ANNOTATION) { return "@" + name; } else { - return "@" + name + "()"; + return "@" + name + "(\""+getValue()+"\")"; } } diff --git a/Robust/src/IR/Tree/BuildIR.java b/Robust/src/IR/Tree/BuildIR.java index 6aca57d4..9dedbe76 100644 --- a/Robust/src/IR/Tree/BuildIR.java +++ b/Robust/src/IR/Tree/BuildIR.java @@ -856,7 +856,6 @@ public class BuildIR { ParseNode tn=pn.getChild("type"); TypeDescriptor t=parseTypeDescriptor(tn); - assignAnnotationsToType(m,t); ParseNode vn=pn.getChild("variables").getChild("variable_declarators_list"); ParseNodeVector pnv=vn.getChildren(); boolean isglobal=pn.getChild("global")!=null; @@ -915,6 +914,7 @@ public class BuildIR { } cn.addField(new FieldDescriptor(m, arrayt, identifier, en, isglobal)); + assignAnnotationsToType(m,arrayt); } } @@ -1384,12 +1384,7 @@ public class BuildIR { blockstatements.add(tdn); } else if (isNode(pn,"local_variable_declaration")) { - ParseNode mn=pn.getChild("modifiers"); TypeDescriptor t=parseTypeDescriptor(pn); - if(mn!=null) { - Modifiers m=parseModifiersList(mn); - assignAnnotationsToType(m, t); - } ParseNode vn=pn.getChild("variable_declarators_list"); ParseNodeVector pnv=vn.getChildren(); for(int i=0; i