From 10c4992e9c69fbea06eff269cc320c290963c915 Mon Sep 17 00:00:00 2001 From: yeom Date: Fri, 3 Jun 2011 23:03:56 +0000 Subject: [PATCH] improves the strategy of checkings: starting from ssjava outermost loop, then only checking methods reachable from that loop. Also, check that every method which overrides an annotated method is also annotated. --- Robust/src/Analysis/SSJava/FlowDownCheck.java | 23 +- .../SSJava/MethodAnnotationCheck.java | 402 ++++++++++++++++++ .../src/Analysis/SSJava/SSJavaAnalysis.java | 63 ++- Robust/src/Main/Main.java | 3 +- 4 files changed, 463 insertions(+), 28 deletions(-) create mode 100644 Robust/src/Analysis/SSJava/MethodAnnotationCheck.java diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index f213b81b..4fd0f108 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -45,7 +45,7 @@ import Util.Pair; public class FlowDownCheck { - static State state; + State state; static SSJavaAnalysis ssjava; HashSet toanalyze; @@ -62,7 +62,6 @@ public class FlowDownCheck { this.toanalyze = new HashSet(); this.d2loc = new Hashtable(); this.fieldLocName2cd = new Hashtable(); - init(); } public void init() { @@ -108,11 +107,8 @@ public class FlowDownCheck { checkDeclarationInClass(cd); for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { MethodDescriptor md = (MethodDescriptor) method_it.next(); - try { + if (ssjava.hasAnnotation(md)) { checkDeclarationInMethodBody(cd, md); - } catch (Error e) { - System.out.println("Error in " + md); - throw e; } } } @@ -130,11 +126,8 @@ public class FlowDownCheck { checkClass(cd); for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { MethodDescriptor md = (MethodDescriptor) method_it.next(); - try { + if (ssjava.hasAnnotation(md)) { checkMethodBody(cd, md); - } catch (Error e) { - System.out.println("Error in " + md); - throw e; } } } @@ -148,6 +141,11 @@ public class FlowDownCheck { SSJavaLattice superLattice = ssjava.getClassLattice(superCd); SSJavaLattice subLattice = ssjava.getClassLattice(cd); + if (superLattice != null && subLattice == null) { + throw new Error("If a parent class '" + superCd + "' has a ordering lattice, its subclass '" + + cd + "' should have one."); + } + Set> superPairSet = superLattice.getOrderingPairSet(); Set> subPairSet = subLattice.getOrderingPairSet(); @@ -230,6 +228,11 @@ public class FlowDownCheck { bn.getVarTable().setParent(nametable); // it will return the lowest location in the block node CompositeLocation lowestLoc = null; + + // if(bn.get(0).kind() == Kind.LoopNode){ + // System.out.println("####="+bn.get(0).printNode(0)); + // } + for (int i = 0; i < bn.size(); i++) { BlockStatementNode bsn = bn.get(i); CompositeLocation bLoc = checkLocationFromBlockStatementNode(md, bn.getVarTable(), bsn); diff --git a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java new file mode 100644 index 00000000..9ef4b4a8 --- /dev/null +++ b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java @@ -0,0 +1,402 @@ +package Analysis.SSJava; + +import java.util.HashSet; +import java.util.Hashtable; +import java.util.Iterator; +import java.util.Set; + +import IR.ClassDescriptor; +import IR.MethodDescriptor; +import IR.Operation; +import IR.State; +import IR.SymbolTable; +import IR.TypeUtil; +import IR.Tree.ArrayAccessNode; +import IR.Tree.ArrayInitializerNode; +import IR.Tree.AssignmentNode; +import IR.Tree.BlockExpressionNode; +import IR.Tree.BlockNode; +import IR.Tree.BlockStatementNode; +import IR.Tree.CastNode; +import IR.Tree.CreateObjectNode; +import IR.Tree.DeclarationNode; +import IR.Tree.ExpressionNode; +import IR.Tree.FieldAccessNode; +import IR.Tree.IfStatementNode; +import IR.Tree.InstanceOfNode; +import IR.Tree.Kind; +import IR.Tree.LoopNode; +import IR.Tree.MethodInvokeNode; +import IR.Tree.OpNode; +import IR.Tree.ReturnNode; +import IR.Tree.SubBlockNode; +import IR.Tree.TertiaryNode; +import Util.Pair; + +public class MethodAnnotationCheck { + + State state; + SSJavaAnalysis ssjava; + TypeUtil tu; + + Set annotatedMDSet; + Hashtable> caller2calleeSet; + + public MethodAnnotationCheck(SSJavaAnalysis ssjava, State state, TypeUtil tu) { + this.ssjava = ssjava; + this.state = state; + this.tu = tu; + caller2calleeSet = new Hashtable>(); + annotatedMDSet = new HashSet(); + } + + public void methodAnnoatationCheck() { + SymbolTable classtable = state.getClassSymbolTable(); + HashSet toanalyze = new HashSet(); + toanalyze.addAll(classtable.getValueSet()); + toanalyze.addAll(state.getTaskSymbolTable().getValueSet()); + while (!toanalyze.isEmpty()) { + Object obj = toanalyze.iterator().next(); + ClassDescriptor cd = (ClassDescriptor) obj; + toanalyze.remove(cd); + if (!cd.isInterface()) { + for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { + MethodDescriptor md = (MethodDescriptor) method_it.next(); + checkMethodBody(cd, md); + } + } + } + + for (Iterator iterator = annotatedMDSet.iterator(); iterator.hasNext();) { + MethodDescriptor md = (MethodDescriptor) iterator.next(); + ssjava.putHasAnnotation(md); + } + + Set visited = new HashSet(); + Set tovisit = new HashSet(); + tovisit.addAll(annotatedMDSet); + + while (!tovisit.isEmpty()) { + MethodDescriptor callerMD = tovisit.iterator().next(); + tovisit.remove(callerMD); + Set calleeSet = caller2calleeSet.get(callerMD); + if (calleeSet != null) { + for (Iterator iterator = calleeSet.iterator(); iterator.hasNext();) { + MethodDescriptor calleeMD = (MethodDescriptor) iterator.next(); + Pair p = new Pair(callerMD, calleeMD); + if (!visited.contains(p)) { + visited.add(p); + tovisit.add(calleeMD); + ssjava.putHasAnnotation(calleeMD); + } + } + } + } + + } + + public void methodAnnoataionInheritanceCheck() { + // check If a method is annotated, any method that overrides it should + // be annotated. + + Set tovisit = new HashSet(); + tovisit.addAll(ssjava.getMd2hasAnnotation().keySet()); + + while (!tovisit.isEmpty()) { + MethodDescriptor md = tovisit.iterator().next(); + tovisit.remove(md); + + ClassDescriptor cd = md.getClassDesc(); + + Set subClassSet = tu.getSubClasses(cd); + if (subClassSet != null) { + for (Iterator iterator2 = subClassSet.iterator(); iterator2.hasNext();) { + ClassDescriptor subCD = (ClassDescriptor) iterator2.next(); + Set possiblematches = subCD.getMethodTable().getSet(md.getSymbol()); + for (Iterator methodit = possiblematches.iterator(); methodit.hasNext();) { + MethodDescriptor matchmd = (MethodDescriptor) methodit.next(); + if (md.matches(matchmd)) { + if (matchmd.getClassDesc().equals(subCD)) { + ssjava.putHasAnnotation(matchmd); + } + } + } + } + } + } + + } + + private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) { + BlockNode bn = state.getMethodBody(md); + checkBlockNode(md, md.getParameterTable(), bn, false); + } + + private void checkBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn, boolean flag) { + bn.getVarTable().setParent(nametable); + String label = bn.getLabel(); + boolean isSSJavaLoop = flag; + if (label != null && label.equals(ssjava.SSJAVA)) { + if (isSSJavaLoop) { + throw new Error("Only outermost loop can be the self-stabilizing loop."); + } else { + annotatedMDSet.add(md); + isSSJavaLoop = true; + } + } + + for (int i = 0; i < bn.size(); i++) { + BlockStatementNode bsn = bn.get(i); + checkBlockStatementNode(md, bn.getVarTable(), bsn, isSSJavaLoop); + } + + } + + private void checkBlockStatementNode(MethodDescriptor md, SymbolTable nametable, + BlockStatementNode bsn, boolean flag) { + + switch (bsn.kind()) { + case Kind.SubBlockNode: + checkSubBlockNode(md, nametable, (SubBlockNode) bsn, flag); + return; + + case Kind.BlockExpressionNode: + checkBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn, flag); + break; + + case Kind.DeclarationNode: + // checkLocationFromDeclarationNode(md, nametable, (DeclarationNode) bsn); + break; + + case Kind.IfStatementNode: + checkIfStatementNode(md, nametable, (IfStatementNode) bsn, flag); + break; + + case Kind.LoopNode: + checkLoopNode(md, nametable, (LoopNode) bsn, flag); + break; + + case Kind.ReturnNode: + checkReturnNode(md, nametable, (ReturnNode) bsn, flag); + break; + + } + } + + void checkDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn, + boolean flag) { + if (dn.getExpression() != null) { + checkExpressionNode(md, nametable, dn.getExpression(), flag); + } + } + + void checkReturnNode(MethodDescriptor md, SymbolTable nametable, ReturnNode rn, boolean flag) { + if (rn.getReturnExpression() != null) { + if (md.getReturnType() != null) { + checkExpressionNode(md, nametable, rn.getReturnExpression(), flag); + } + } + } + + void checkLoopNode(MethodDescriptor md, SymbolTable nametable, LoopNode ln, boolean flag) { + if (ln.getType() == LoopNode.WHILELOOP || ln.getType() == LoopNode.DOWHILELOOP) { + checkExpressionNode(md, nametable, ln.getCondition(), flag); + checkBlockNode(md, nametable, ln.getBody(), flag); + } else { + // For loop case + /* Link in the initializer naming environment */ + BlockNode bn = ln.getInitializer(); + bn.getVarTable().setParent(nametable); + for (int i = 0; i < bn.size(); i++) { + BlockStatementNode bsn = bn.get(i); + checkBlockStatementNode(md, bn.getVarTable(), bsn, flag); + } + // check the condition + checkExpressionNode(md, bn.getVarTable(), ln.getCondition(), flag); + checkBlockNode(md, bn.getVarTable(), ln.getBody(), flag); + checkBlockNode(md, bn.getVarTable(), ln.getUpdate(), flag); + } + } + + void checkIfStatementNode(MethodDescriptor md, SymbolTable nametable, IfStatementNode isn, + boolean flag) { + checkExpressionNode(md, nametable, isn.getCondition(), flag); + checkBlockNode(md, nametable, isn.getTrueBlock(), flag); + if (isn.getFalseBlock() != null) { + checkBlockNode(md, nametable, isn.getFalseBlock(), flag); + } + } + + private void checkSubBlockNode(MethodDescriptor md, SymbolTable nametable, SubBlockNode sbn, + boolean flag) { + checkBlockNode(md, nametable.getParent(), sbn.getBlockNode(), flag); + } + + private void checkBlockExpressionNode(MethodDescriptor md, SymbolTable nametable, + BlockExpressionNode ben, boolean flag) { + checkExpressionNode(md, nametable, ben.getExpression(), flag); + } + + private void checkExpressionNode(MethodDescriptor md, SymbolTable nametable, ExpressionNode en, + boolean flag) { + switch (en.kind()) { + case Kind.AssignmentNode: + checkAssignmentNode(md, nametable, (AssignmentNode) en, flag); + return; + + case Kind.CastNode: + checkCastNode(md, nametable, (CastNode) en, flag); + return; + + case Kind.CreateObjectNode: + checkCreateObjectNode(md, nametable, (CreateObjectNode) en, flag); + return; + + case Kind.FieldAccessNode: + checkFieldAccessNode(md, nametable, (FieldAccessNode) en, flag); + return; + + case Kind.ArrayAccessNode: + checkArrayAccessNode(md, nametable, (ArrayAccessNode) en, flag); + return; + + // case Kind.LiteralNode: + // checkLiteralNode(md, nametable, (LiteralNode) en, flag); + // return; + + case Kind.MethodInvokeNode: + checkMethodInvokeNode(md, nametable, (MethodInvokeNode) en, flag); + return; + + // case Kind.NameNode: + // checkNameNode(md, nametable, (NameNode) en, flag); + // return; + + case Kind.OpNode: + checkOpNode(md, nametable, (OpNode) en, flag); + return; + + // case Kind.OffsetNode: + // checkOffsetNode(md, nametable, (OffsetNode) en, flag); + // return; + + case Kind.TertiaryNode: + checkTertiaryNode(md, nametable, (TertiaryNode) en, flag); + return; + + case Kind.InstanceOfNode: + checkInstanceOfNode(md, nametable, (InstanceOfNode) en, flag); + return; + + case Kind.ArrayInitializerNode: + checkArrayInitializerNode(md, nametable, (ArrayInitializerNode) en, flag); + return; + + // case Kind.ClassTypeNode: + // checkClassTypeNode(md, nametable, (ClassTypeNode) en, flag); + // return; + } + } + + private void checkArrayInitializerNode(MethodDescriptor md, SymbolTable nametable, + ArrayInitializerNode ain, boolean flag) { + + for (int i = 0; i < ain.numVarInitializers(); ++i) { + checkExpressionNode(md, nametable, ain.getVarInitializer(i), flag); + } + + } + + private void checkInstanceOfNode(MethodDescriptor md, SymbolTable nametable, InstanceOfNode tn, + boolean flag) { + checkExpressionNode(md, nametable, tn.getExpr(), flag); + } + + private void checkTertiaryNode(MethodDescriptor md, SymbolTable nametable, TertiaryNode tn, + boolean flag) { + checkExpressionNode(md, nametable, tn.getCond(), flag); + checkExpressionNode(md, nametable, tn.getTrueExpr(), flag); + checkExpressionNode(md, nametable, tn.getFalseExpr(), flag); + } + + private void checkOpNode(MethodDescriptor md, SymbolTable nametable, OpNode on, boolean flag) { + + checkExpressionNode(md, nametable, on.getLeft(), flag); + if (on.getRight() != null) { + checkExpressionNode(md, nametable, on.getRight(), flag); + } + + } + + private void checkMethodInvokeNode(MethodDescriptor md, SymbolTable nametable, + MethodInvokeNode min, boolean flag) { + for (int i = 0; i < min.numArgs(); i++) { + ExpressionNode en = min.getArg(i); + checkExpressionNode(md, nametable, en, flag); + } + + if (min.getExpression() != null) { + checkExpressionNode(md, nametable, min.getExpression(), flag); + } + + if (flag) { + annotatedMDSet.add(min.getMethod()); + } + + Set mdSet = caller2calleeSet.get(md); + if (mdSet == null) { + mdSet = new HashSet(); + caller2calleeSet.put(md, mdSet); + } + mdSet.add(min.getMethod()); + + } + + private void checkArrayAccessNode(MethodDescriptor md, SymbolTable nametable, + ArrayAccessNode aan, boolean flag) { + + ExpressionNode left = aan.getExpression(); + checkExpressionNode(md, nametable, left, flag); + checkExpressionNode(md, nametable, aan.getIndex(), flag); + + } + + private void checkFieldAccessNode(MethodDescriptor md, SymbolTable nametable, + FieldAccessNode fan, boolean flag) { + ExpressionNode left = fan.getExpression(); + checkExpressionNode(md, nametable, left, flag); + } + + private void checkCreateObjectNode(MethodDescriptor md, SymbolTable nametable, + CreateObjectNode con, boolean flag) { + + for (int i = 0; i < con.numArgs(); i++) { + ExpressionNode en = con.getArg(i); + checkExpressionNode(md, nametable, en, flag); + } + + } + + private void checkCastNode(MethodDescriptor md, SymbolTable nametable, CastNode cn, boolean flag) { + ExpressionNode en = cn.getExpression(); + checkExpressionNode(md, nametable, en, flag); + } + + private void checkAssignmentNode(MethodDescriptor md, SymbolTable nametable, AssignmentNode an, + boolean flag) { + boolean postinc = true; + + if (an.getOperation().getBaseOp() == null + || (an.getOperation().getBaseOp().getOp() != Operation.POSTINC && an.getOperation() + .getBaseOp().getOp() != Operation.POSTDEC)) + postinc = false; + + if (!postinc) { + checkExpressionNode(md, nametable, an.getSrc(), flag); + } + + checkExpressionNode(md, nametable, an.getDest(), flag); + + } + +} diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index f9790deb..772d6868 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -10,17 +10,25 @@ import IR.AnnotationDescriptor; import IR.ClassDescriptor; import IR.MethodDescriptor; import IR.State; +import IR.TypeUtil; public class SSJavaAnalysis { + public static final String SSJAVA = "SSJAVA"; public static final String LATTICE = "LATTICE"; public static final String METHODDEFAULT = "METHODDEFAULT"; public static final String THISLOC = "THISLOC"; public static final String GLOBALLOC = "GLOBALLOC"; + public static final String RETURNLOC = "RETURNLOC"; public static final String LOC = "LOC"; public static final String DELTA = "DELTA"; State state; + TypeUtil tu; FlowDownCheck flowDownChecker; + MethodAnnotationCheck methodAnnotationChecker; + + // if a method has annotations, the mapping has true + Hashtable md2hasAnnotation; // class -> field lattice Hashtable> cd2lattice; @@ -31,20 +39,29 @@ public class SSJavaAnalysis { // method -> local variable lattice Hashtable> md2lattice; - public SSJavaAnalysis(State state) { + public SSJavaAnalysis(State state, TypeUtil tu) { this.state = state; - cd2lattice = new Hashtable>(); - cd2methodDefault = new Hashtable>(); - md2lattice = new Hashtable>(); + this.tu = tu; + this.cd2lattice = new Hashtable>(); + this.cd2methodDefault = new Hashtable>(); + this.md2lattice = new Hashtable>(); + this.md2hasAnnotation = new Hashtable(); } public void doCheck() { + doMethodAnnotationCheck(); parseLocationAnnotation(); doFlowDownCheck(); doLoopCheck(); doSingleReferenceCheck(); } + private void doMethodAnnotationCheck() { + methodAnnotationChecker = new MethodAnnotationCheck(this, state, tu); + methodAnnotationChecker.methodAnnoatationCheck(); + methodAnnotationChecker.methodAnnoataionInheritanceCheck(); + } + public void doFlowDownCheck() { flowDownChecker = new FlowDownCheck(this, state); flowDownChecker.flowDownCheck(); @@ -81,23 +98,23 @@ public class SSJavaAnalysis { parseMethodLatticeDefinition(cd, an.getValue(), locOrder); } } - if (!cd2lattice.containsKey(cd)) { - throw new Error("Class " + cd.getSymbol() - + " doesn't have any location hierarchy declaration at " + cd.getSourceFileName()); - } for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { MethodDescriptor md = (MethodDescriptor) method_it.next(); // parsing location hierarchy declaration for the method - Vector methodAnnotations = md.getModifiers().getAnnotations(); - if (methodAnnotations != null) { - for (int i = 0; i < methodAnnotations.size(); i++) { - AnnotationDescriptor an = methodAnnotations.elementAt(i); - if (an.getMarker().equals(LATTICE)) { - MethodLattice locOrder = - new MethodLattice(SSJavaLattice.TOP, SSJavaLattice.BOTTOM); - md2lattice.put(md, locOrder); - parseMethodLatticeDefinition(cd, an.getValue(), locOrder); + + if (hasAnnotation(md)) { + Vector methodAnnotations = md.getModifiers().getAnnotations(); + if (methodAnnotations != null) { + for (int i = 0; i < methodAnnotations.size(); i++) { + AnnotationDescriptor an = methodAnnotations.elementAt(i); + if (an.getMarker().equals(LATTICE)) { + // developer explicitly defines method lattice + MethodLattice locOrder = + new MethodLattice(SSJavaLattice.TOP, SSJavaLattice.BOTTOM); + md2lattice.put(md, locOrder); + parseMethodLatticeDefinition(cd, an.getValue(), locOrder); + } } } } @@ -215,4 +232,16 @@ public class SSJavaAnalysis { } } + public boolean hasAnnotation(MethodDescriptor md) { + return md2hasAnnotation.containsKey(md); + } + + public void putHasAnnotation(MethodDescriptor md) { + md2hasAnnotation.put(md, new Boolean(true)); + } + + public Hashtable getMd2hasAnnotation() { + return md2hasAnnotation; + } + } diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java index 8f30c5a6..ff59d3d4 100644 --- a/Robust/src/Main/Main.java +++ b/Robust/src/Main/Main.java @@ -421,7 +421,7 @@ public class Main { State.logEvent("Done Parsing Commands"); System.out.println("Classpath: "+state.classpath); - SSJavaAnalysis ssjava=new SSJavaAnalysis(state); + TypeUtil tu; BuildFlat bf; @@ -480,6 +480,7 @@ public class Main { // SSJava if(state.SSJAVA) { + SSJavaAnalysis ssjava=new SSJavaAnalysis(state,tu); ssjava.doCheck(); State.logEvent("Done SSJava Checking"); } -- 2.34.1