From: yeom Date: Sat, 6 Aug 2011 01:36:10 +0000 (+0000) Subject: buildflat exposes new interface that maps from a tree node to the set of flatnodes... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=82896c3e8ba574153f74dcc8bfad08748cdb86a8;p=IRC.git buildflat exposes new interface that maps from a tree node to the set of flatnodes that implements + revising linear type checking --- diff --git a/Robust/src/Analysis/SSJava/LinearTypeCheck.java b/Robust/src/Analysis/SSJava/LinearTypeCheck.java index 90aee1e7..2a6d905a 100644 --- a/Robust/src/Analysis/SSJava/LinearTypeCheck.java +++ b/Robust/src/Analysis/SSJava/LinearTypeCheck.java @@ -6,33 +6,34 @@ import java.util.Iterator; import java.util.Set; import java.util.Vector; +import Analysis.Liveness; import IR.AnnotationDescriptor; import IR.ClassDescriptor; -import IR.Descriptor; import IR.MethodDescriptor; +import IR.NameDescriptor; +import IR.Operation; import IR.State; import IR.SymbolTable; -import IR.TaskDescriptor; import IR.TypeDescriptor; import IR.VarDescriptor; +import IR.Flat.FKind; +import IR.Flat.FlatMethod; +import IR.Flat.FlatNode; +import IR.Flat.FlatOpNode; +import IR.Flat.TempDescriptor; import IR.Tree.ArrayAccessNode; import IR.Tree.ArrayInitializerNode; import IR.Tree.AssignmentNode; -import IR.Tree.AtomicNode; import IR.Tree.BlockExpressionNode; import IR.Tree.BlockNode; import IR.Tree.BlockStatementNode; import IR.Tree.CastNode; -import IR.Tree.ClassTypeNode; -import IR.Tree.ContinueBreakNode; 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.LiteralNode; import IR.Tree.LoopNode; import IR.Tree.MethodInvokeNode; import IR.Tree.NameNode; @@ -41,25 +42,33 @@ import IR.Tree.OpNode; import IR.Tree.ReturnNode; import IR.Tree.SubBlockNode; import IR.Tree.SwitchBlockNode; -import IR.Tree.SwitchLabelNode; import IR.Tree.SwitchStatementNode; import IR.Tree.SynchronizedNode; -import IR.Tree.TagDeclarationNode; -import IR.Tree.TaskExitNode; import IR.Tree.TertiaryNode; +import IR.Tree.TreeNode; public class LinearTypeCheck { State state; SSJavaAnalysis ssjava; String needToNullify = null; + AssignmentNode prevAssignNode; Hashtable> md2DelegateParamSet; + Set linearTypeCheckSet; + + Hashtable mapTreeNode2FlatMethod; + + Liveness liveness; + public LinearTypeCheck(SSJavaAnalysis ssjava, State state) { this.ssjava = ssjava; this.state = state; - md2DelegateParamSet = new Hashtable>(); + this.md2DelegateParamSet = new Hashtable>(); + this.linearTypeCheckSet = new HashSet(); + this.mapTreeNode2FlatMethod = new Hashtable(); + this.liveness = new Liveness(); } public void linearTypeCheck() { @@ -73,8 +82,6 @@ public class LinearTypeCheck { parseAnnotations(md); } } - System.out.println("###"); - System.out.println("md2DelegateParamSet=" + md2DelegateParamSet); // second, check the linear type it = state.getClassSymbolTable().getDescriptorsIterator(); @@ -82,14 +89,44 @@ public class LinearTypeCheck { ClassDescriptor cd = (ClassDescriptor) it.next(); for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { MethodDescriptor md = (MethodDescriptor) method_it.next(); - if (ssjava.needTobeAnnotated(md)) { - checkMethodBody(cd, md); + checkMethodBody(cd, md); + } + } + + // third, check if original references are destroyed after creating new + // alias + + for (Iterator iterator = linearTypeCheckSet.iterator(); iterator.hasNext();) { + TreeNode tn = iterator.next(); + Set fnSet = ssjava.getBuildFlat().getFlatNodeSet(tn); + if (fnSet != null) { + for (Iterator iterator2 = fnSet.iterator(); iterator2.hasNext();) { + FlatNode fn = (FlatNode) iterator2.next(); + if (isLiveOut(tn, fn)) { + throw new Error( + "Local variable '" + + tn.printNode(0) + + "', which is read by a method, should be destroyed after introducing new alias at " + + mapTreeNode2FlatMethod.get(tn).getMethod().getClassDesc().getSourceFileName() + + "::" + tn.getNumLine()); + } + } } + } } + private boolean isLiveOut(TreeNode tn, FlatNode fn) { + Set liveOutTemp = liveness.getLiveOutTemps(mapTreeNode2FlatMethod.get(tn), fn); + if (fn.kind() == FKind.FlatOpNode) { + FlatOpNode fon = (FlatOpNode) fn; + return liveOutTemp.contains(fon.getLeft()); + } + return false; + } + private void parseAnnotations(MethodDescriptor md) { for (int i = 0; i < md.numParameters(); i++) { @@ -133,8 +170,10 @@ public class LinearTypeCheck { if (needToNullify != null) { if (!checkNullifying(bsn)) { throw new Error( - "Reference field, which is read by a method, should be assigned to null before executing any following statement of the reference copy statement at " - + md.getClassDesc().getSourceFileName() + "::" + bsn.getNumLine()); + "Reference field '" + + needToNullify + + "', which is read by a method, should be assigned to null before executing any following statement of the reference copy statement at " + + md.getClassDesc().getSourceFileName() + "::" + prevAssignNode.getNumLine()); } } @@ -173,7 +212,6 @@ public class LinearTypeCheck { return; } - throw new Error(); } private void checkSynchronizedNode(MethodDescriptor md, SymbolTable nametable, @@ -278,7 +316,6 @@ public class LinearTypeCheck { // checkClassTypeNode(md, nametable, (ClassTypeNode) ens); // return; } - throw new Error(); } private void checkTertiaryNode(MethodDescriptor md, SymbolTable nametable, TertiaryNode en) { @@ -317,6 +354,7 @@ public class LinearTypeCheck { private void checkCreateObjectNode(MethodDescriptor md, SymbolTable nametable, CreateObjectNode con) { + TypeDescriptor[] tdarray = new TypeDescriptor[con.numArgs()]; for (int i = 0; i < con.numArgs(); i++) { ExpressionNode en = con.getArg(i); @@ -348,7 +386,12 @@ public class LinearTypeCheck { if (en.kind() == Kind.AssignmentNode) { AssignmentNode an = (AssignmentNode) en; - if (an.getSrc().getType().isNull() && an.getDest().printNode(0).equals(needToNullify)) { + String destName = an.getDest().printNode(0); + if (destName.startsWith("this.")) { + destName = destName.substring(5); + } + + if (an.getSrc().getType().isNull() && destName.equals(needToNullify)) { needToNullify = null; return true; } @@ -377,12 +420,63 @@ public class LinearTypeCheck { } } - private void checkAssignmentNode(Descriptor md, SymbolTable nametable, AssignmentNode an) { - needToNullify(an.getSrc()); + private void checkAssignmentNode(MethodDescriptor md, SymbolTable nametable, AssignmentNode an) { + + boolean postinc = true; + if (an.getOperation().getBaseOp() == null + || (an.getOperation().getBaseOp().getOp() != Operation.POSTINC && an.getOperation() + .getBaseOp().getOp() != Operation.POSTDEC)) + postinc = false; + + if (!postinc) { + if (!an.getSrc().getType().isImmutable()) { + if (an.getSrc().kind() == Kind.NameNode) { + + NameNode nn = (NameNode) an.getSrc(); + + if (nn.getField() != null) { + needToNullify = nn.getField().getSymbol(); + prevAssignNode = an; + } else if (nn.getExpression() != null) { + if (nn.getExpression() instanceof FieldAccessNode) { + FieldAccessNode fan = (FieldAccessNode) nn.getExpression(); + needToNullify = fan.printNode(0); + prevAssignNode = an; + + } + + } else { + // local variable case + linearTypeCheckSet.add(an.getSrc()); + mapTreeNode2FlatMethod.put(an.getSrc(), state.getMethodFlat(md)); + } + } else if (an.getSrc().kind() == Kind.FieldAccessNode) { + FieldAccessNode fan = (FieldAccessNode) an.getSrc(); + needToNullify = fan.printNode(0); + if (needToNullify.startsWith("this.")) { + needToNullify = needToNullify.substring(5); + } + prevAssignNode = an; + } + + } + } + + // needToNullify(an.getSrc()); } - private void checkDeclarationNode(Descriptor md, SymbolTable nametable, DeclarationNode dn) { - needToNullify(dn.getExpression()); + private String getVarNameFromNameNode(NameNode nn) { + NameDescriptor nd = nn.getName(); + String varName = nd.toString(); + return varName; + } + + private void checkDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn) { + if (dn.getExpression() != null) { + checkExpressionNode(md, nametable, dn.getExpression()); + } + + // needToNullify(dn.getExpression()); } private void needToNullify(ExpressionNode en) { diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index 41396e96..ee47d041 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -21,7 +21,7 @@ import IR.State; import IR.TypeUtil; import IR.Flat.BuildFlat; import IR.Flat.FlatMethod; -import IR.Flat.TempDescriptor; +import IR.Tree.TreeNode; import Util.Pair; public class SSJavaAnalysis { @@ -41,6 +41,7 @@ public class SSJavaAnalysis { TypeUtil tu; FlowDownCheck flowDownChecker; MethodAnnotationCheck methodAnnotationChecker; + BuildFlat bf; // set containing method requires to be annoated Set annotationRequireSet; @@ -65,7 +66,9 @@ public class SSJavaAnalysis { CallGraph callgraph; - public SSJavaAnalysis(State state, TypeUtil tu, CallGraph callgraph) { + LinearTypeCheck checker; + + public SSJavaAnalysis(State state, TypeUtil tu, BuildFlat bf, CallGraph callgraph) { this.state = state; this.tu = tu; this.callgraph = callgraph; @@ -76,10 +79,12 @@ public class SSJavaAnalysis { this.annotationRequireClassSet = new HashSet(); this.skipLoopTerminate = new Hashtable(); this.mapSharedLocation2DescriptorSet = new Hashtable>(); + this.bf = bf; } public void doCheck() { doLinearTypeCheck(); + System.exit(0); doMethodAnnotationCheck(); if (state.SSJAVADEBUG) { debugPrint(); @@ -402,4 +407,8 @@ public class SSJavaAnalysis { set.add(d); } + public BuildFlat getBuildFlat() { + return bf; + } + } diff --git a/Robust/src/Analysis/SSJava/SSJavaType.java b/Robust/src/Analysis/SSJava/SSJavaType.java new file mode 100644 index 00000000..60e7068b --- /dev/null +++ b/Robust/src/Analysis/SSJava/SSJavaType.java @@ -0,0 +1,30 @@ +package Analysis.SSJava; + +import IR.TypeExtension; + +public class SSJavaType implements TypeExtension { + + private boolean isOwned; + private CompositeLocation compLoc; + + public SSJavaType(boolean isOwned) { + this.isOwned = isOwned; + } + + public CompositeLocation getCompLoc() { + return compLoc; + } + + public void setCompLoc(CompositeLocation compLoc) { + this.compLoc = compLoc; + } + + public boolean isOwned() { + return isOwned; + } + + public void setOwned(boolean isOwned) { + this.isOwned = isOwned; + } + +} diff --git a/Robust/src/IR/Flat/BuildFlat.java b/Robust/src/IR/Flat/BuildFlat.java index 71f48019..dab3af93 100644 --- a/Robust/src/IR/Flat/BuildFlat.java +++ b/Robust/src/IR/Flat/BuildFlat.java @@ -16,6 +16,10 @@ public class BuildFlat { // for synchronized blocks Stack lockStack; + + // maps tree node to the set of flat node that is translated from the tree node + // WARNING: ONLY DID FOR NAMENODE NOW! + Hashtable> mapNode2FlatNodeSet; public BuildFlat(State st, TypeUtil typeutil) { state=st; @@ -24,6 +28,7 @@ public class BuildFlat { this.breakset=new HashSet(); this.continueset=new HashSet(); this.lockStack = new Stack(); + this.mapNode2FlatNodeSet=new Hashtable>(); } public Hashtable getMap() { @@ -1018,6 +1023,7 @@ public class BuildFlat { } FlatFieldNode ffn=new FlatFieldNode(nn.getField(), tmp, out_temp); ffn.setNumLine(nn.getNumLine()); + addMapNode2FlatNodeSet(nn,ffn); return new NodePair(ffn,ffn); } else { TempDescriptor tmp=getTempforVar(nn.isTag()?nn.getTagVar():nn.getVar()); @@ -1027,6 +1033,7 @@ public class BuildFlat { } FlatOpNode fon=new FlatOpNode(out_temp, tmp, null, new Operation(Operation.ASSIGN)); fon.setNumLine(nn.getNumLine()); + addMapNode2FlatNodeSet(nn,fon); return new NodePair(fon,fon); } } @@ -1750,4 +1757,20 @@ public class BuildFlat { } throw new Error(); } + + private void addMapNode2FlatNodeSet(TreeNode tn, FlatNode fn){ + Set fnSet=mapNode2FlatNodeSet.get(tn); + if(fnSet==null){ + fnSet=new HashSet(); + mapNode2FlatNodeSet.put(tn, fnSet); + } + fnSet.add(fn); + } + + public Set getFlatNodeSet(TreeNode tn){ + // WARNING: ONLY DID FOR NAMENODE NOW! + assert(tn instanceof NameNode); + return mapNode2FlatNodeSet.get(tn); + } + } diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java index 026c2cfd..0b994ec2 100644 --- a/Robust/src/Main/Main.java +++ b/Robust/src/Main/Main.java @@ -483,7 +483,7 @@ public class Main { CallGraph callgraph=jb!=null?jb:(state.TASK?new BaseCallGraph(state, tu):new JavaCallGraph(state, tu)); // SSJava - SSJavaAnalysis ssjava=new SSJavaAnalysis(state,tu,callgraph); + SSJavaAnalysis ssjava=new SSJavaAnalysis(state,tu,bf,callgraph); if(state.SSJAVA) { ssjava.doCheck(); State.logEvent("Done SSJava Checking");