From: yeom Date: Wed, 1 Aug 2012 22:50:30 +0000 (+0000) Subject: Allow to declare a composite location for the initial program counter location. X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=bb1740841625c379adb5c9220b165109adc13650;p=IRC.git Allow to declare a composite location for the initial program counter location. The developer can declare the program counter location as a composite location that starts with the location type of the current object 'this'. It provides more specific constraints on value flows between fields in the current object. --- diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index a851b020..2e879b18 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -6,7 +6,6 @@ import java.util.Comparator; import java.util.HashSet; import java.util.Hashtable; import java.util.Iterator; -import java.util.LinkedList; import java.util.List; import java.util.Set; import java.util.StringTokenizer; @@ -227,8 +226,7 @@ public class FlowDownCheck { if (state.SSJAVADEBUG) { System.out.println("SSJAVA: Checking Flow-down Rules: " + md); } - CompositeLocation calleePCLOC = - new CompositeLocation(new Location(md, ssjava.getMethodLattice(md).getPCLoc())); + CompositeLocation calleePCLOC = ssjava.getPCLocation(md); checkMethodBody(cd, md, calleePCLOC); } } @@ -327,8 +325,8 @@ public class FlowDownCheck { String globalLoc = an.getValue(); ssjava.getMethodLattice(md).setGlobalLoc(globalLoc); } else if (an.getMarker().equals(ssjava.PCLOC)) { - String pcLoc = an.getValue(); - ssjava.getMethodLattice(md).setPCLoc(pcLoc); + String pcLocDeclaration = an.getValue(); + ssjava.setPCLocation(md, parseLocationDeclaration(md, null, pcLocDeclaration)); } } } @@ -977,30 +975,35 @@ public class FlowDownCheck { // annotation that declares the program counter that is higher than // corresponding parameter - CompositeLocation calleePCLOC = - new CompositeLocation(new Location(calleemd, calleeLattice.getPCLoc())); + CompositeLocation calleePCLOC = ssjava.getPCLocation(calleemd); for (int idx = 0; idx < callerArgList.size(); idx++) { CompositeLocation argLocation = callerArgList.get(idx); int compareResult = CompositeLattice - .compare(constraint, argLocation, true, generateErrorMessage(cd, min)); + .compare(argLocation, constraint, true, generateErrorMessage(cd, min)); // need to check that param is higher than PCLOC - if (compareResult != ComparisonResult.GREATER) { + if (compareResult == ComparisonResult.GREATER) { CompositeLocation paramLocation = calleeParamList.get(idx); int paramCompareResult = - CompositeLattice.compare(paramLocation, calleePCLOC, true, + CompositeLattice.compare(calleePCLOC, paramLocation, true, generateErrorMessage(cd, min)); - if (paramCompareResult != ComparisonResult.GREATER) { - throw new Error("The program counter location " + constraint - + " is lower than the argument location " + argLocation - + ". Need to specify that the initial PC location of the callee is lower than " - + paramLocation + ":" + min.getNumLine()); + if (paramCompareResult == ComparisonResult.GREATER) { + throw new Error( + "The program counter location " + + constraint + + " is lower than the argument(idx=" + + idx + + ") location " + + argLocation + + ". Need to specify that the initial PC location of the callee, which is currently set to " + + calleePCLOC + ", is lower than " + paramLocation + " in the method " + + calleeMD.getSymbol() + ":" + min.getNumLine()); } } diff --git a/Robust/src/Analysis/SSJava/MethodLattice.java b/Robust/src/Analysis/SSJava/MethodLattice.java index 1b04d77a..88eb7b70 100644 --- a/Robust/src/Analysis/SSJava/MethodLattice.java +++ b/Robust/src/Analysis/SSJava/MethodLattice.java @@ -1,17 +1,13 @@ package Analysis.SSJava; -import IR.MethodDescriptor; - public class MethodLattice extends SSJavaLattice { private T thisLoc; private T globalLoc; private T returnLoc; - private T pcLoc; public MethodLattice(T top, T bottom) { super(top, bottom); - pcLoc = top; } public void setThisLoc(T thisLoc) { @@ -38,12 +34,4 @@ public class MethodLattice extends SSJavaLattice { return returnLoc; } - public T getPCLoc() { - return pcLoc; - } - - public void setPCLoc(T pcLoc) { - this.pcLoc = pcLoc; - } - } diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index 121e4cb5..b18edaf4 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -6,18 +6,19 @@ import java.io.IOException; import java.util.ArrayList; import java.util.Collections; import java.util.Comparator; +import java.util.HashMap; import java.util.HashSet; import java.util.Hashtable; import java.util.Iterator; import java.util.LinkedList; import java.util.List; +import java.util.Map; import java.util.Set; import java.util.StringTokenizer; import java.util.Vector; import Analysis.CallGraph.CallGraph; import Analysis.Loops.GlobalFieldType; -import Analysis.Loops.LoopFinder; import Analysis.Loops.LoopOptimize; import Analysis.Loops.LoopTerminate; import IR.AnnotationDescriptor; @@ -85,6 +86,9 @@ public class SSJavaAnalysis { // the set of method descriptors annotated as "TRUST" Set trustWorthyMDSet; + // method -> the initial program counter location + Map md2pcLoc; + // points to method containing SSJAVA Loop private MethodDescriptor methodContainingSSJavaLoop; @@ -124,6 +128,7 @@ public class SSJavaAnalysis { this.sameHeightWriteFlatNodeSet = new HashSet(); this.mapDescriptorToSetDependents = new Hashtable>(); this.sortedDescriptors = new LinkedList(); + this.md2pcLoc = new HashMap(); } public void doCheck() { @@ -407,9 +412,6 @@ public class SSJavaAnalysis { } else if (orderElement.startsWith(RETURNLOC + "=")) { String returnLoc = orderElement.substring(10); locOrder.setReturnLoc(returnLoc); - } else if (orderElement.startsWith(PCLOC + "=")) { - String pcLoc = orderElement.substring(6); - locOrder.setPCLoc(pcLoc); } else if (orderElement.endsWith("*")) { // spin loc definition locOrder.addSharedLoc(orderElement.substring(0, orderElement.length() - 1)); @@ -504,6 +506,19 @@ public class SSJavaAnalysis { } } + public CompositeLocation getPCLocation(MethodDescriptor md) { + if (!md2pcLoc.containsKey(md)) { + // by default, the initial pc location is TOP + CompositeLocation pcLoc = new CompositeLocation(new Location(md, Location.TOP)); + md2pcLoc.put(md, pcLoc); + } + return md2pcLoc.get(md); + } + + public void setPCLocation(MethodDescriptor md, CompositeLocation pcLoc) { + md2pcLoc.put(md, pcLoc); + } + public boolean needToCheckLinearType(MethodDescriptor md) { return linearTypeCheckMethodSet.contains(md); }