+ List<CompositeLocation> callerArgList = new ArrayList<CompositeLocation>();
+ List<CompositeLocation> calleeParamList = new ArrayList<CompositeLocation>();
+
+ MethodLattice<String> calleeLattice = ssjava.getMethodLattice(calleemd);
+ Location calleeThisLoc = new Location(calleemd, calleeLattice.getThisLoc());
+
+ for (int i = 0; i < min.numArgs(); i++) {
+ ExpressionNode en = min.getArg(i);
+ CompositeLocation callerArgLoc =
+ checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
+ false);
+ callerArgList.add(callerArgLoc);
+ }
+
+ // setup callee params set
+ for (int i = 0; i < calleemd.numParameters(); i++) {
+ VarDescriptor calleevd = (VarDescriptor) calleemd.getParameter(i);
+ CompositeLocation calleeLoc = d2loc.get(calleevd);
+ calleeParamList.add(calleeLoc);
+ }
+
+ String errorMsg = generateErrorMessage(md.getClassDesc(), min);
+
+ // System.out.println("checkCallerArgumentLocationConstraints=" +
+ // min.printNode(0));
+ // System.out.println("base location=" + callerBaseLoc + " constraint=" +
+ // constraint);
+
+ for (int i = 0; i < calleeParamList.size(); i++) {
+ CompositeLocation calleeParamLoc = calleeParamList.get(i);
+ if (calleeParamLoc.get(0).equals(calleeThisLoc) && calleeParamLoc.getSize() > 1) {
+
+ // callee parameter location has field information
+ CompositeLocation callerArgLoc = callerArgList.get(i);
+
+ CompositeLocation paramLocation =
+ translateCalleeParamLocToCaller(md, calleeParamLoc, callerBaseLoc, errorMsg);
+
+ Set<CompositeLocation> inputGLBSet = new HashSet<CompositeLocation>();
+ if (constraint != null) {
+ inputGLBSet.add(callerArgLoc);
+ inputGLBSet.add(constraint);
+ callerArgLoc =
+ CompositeLattice.calculateGLB(inputGLBSet,
+ generateErrorMessage(md.getClassDesc(), min));
+ }
+
+ Location argLastLoc = callerArgLoc.get(callerArgLoc.getSize() - 1);
+ Location paramLastLoc = paramLocation.get(paramLocation.getSize() - 1);
+
+ if (argLastLoc.equals(paramLastLoc) && ssjava.isSharedLocation(argLastLoc)
+ && ssjava.isSharedLocation(paramLastLoc)) {
+ continue;
+ }
+
+ // if (!CompositeLattice.isGreaterThan(callerArgLoc, paramLocation, errorMsg)) {
+ if (CompositeLattice.compare(callerArgLoc, paramLocation, true, errorMsg) == ComparisonResult.LESS) {
+ throw new Error("Caller argument '" + min.getArg(i).printNode(0) + " : " + callerArgLoc
+ + "' should be higher than corresponding callee's parameter : " + paramLocation
+ + " at " + errorMsg);
+ }
+
+ }
+ }
+
+ }
+
+ private CompositeLocation translateCalleeParamLocToCaller(MethodDescriptor md,
+ CompositeLocation calleeParamLoc, CompositeLocation callerBaseLocation, String errorMsg) {
+
+ CompositeLocation translate = new CompositeLocation();
+
+ for (int i = 0; i < callerBaseLocation.getSize(); i++) {
+ translate.addLocation(callerBaseLocation.get(i));
+ }
+
+ for (int i = 1; i < calleeParamLoc.getSize(); i++) {
+ translate.addLocation(calleeParamLoc.get(i));
+ }
+
+ // System.out.println("TRANSLATED=" + translate + " from calleeParamLoc=" +
+ // calleeParamLoc);
+
+ return translate;
+ }
+
+ private CompositeLocation computeCeilingLocationForCaller(MethodDescriptor md,
+ SymbolTable nametable, MethodInvokeNode min, CompositeLocation baseLocation,
+ CompositeLocation constraint) {
+ List<CompositeLocation> argList = new ArrayList<CompositeLocation>();
+
+ // by default, method has a THIS parameter
+ if (!min.getMethod().isStatic()) {
+ argList.add(baseLocation);
+ }
+
+ for (int i = 0; i < min.numArgs(); i++) {
+ ExpressionNode en = min.getArg(i);
+ CompositeLocation callerArg =
+ checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
+ false);
+ argList.add(callerArg);
+ }
+
+ // System.out.println("\n## computeReturnLocation=" + min.getMethod() + " argList=" + argList);
+ CompositeLocation ceilLoc = md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList);
+ // System.out.println("## ReturnLocation=" + ceilLoc);
+
+ return ceilLoc;
+
+ }
+
+ private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable,
+ MethodInvokeNode min, CompositeLocation callerBaseLoc, CompositeLocation constraint) {
+
+ MethodDescriptor calleemd = min.getMethod();
+
+ MethodLattice<String> calleeLattice = ssjava.getMethodLattice(calleemd);
+
+ System.out.println("checkCalleeConstraints=" + calleemd + " calleeLattice.getThisLoc()="
+ + calleeLattice.getThisLoc());
+
+ List<CompositeLocation> callerArgList = new ArrayList<CompositeLocation>();
+ List<CompositeLocation> calleeParamList = new ArrayList<CompositeLocation>();
+
+ if (min.numArgs() > 0) {
+ // caller needs to guarantee that it passes arguments in regarding to
+ // callee's hierarchy
+
+ // setup caller args set
+ // first, add caller's base(this) location
+ if (!calleemd.isStatic())
+ callerArgList.add(callerBaseLoc);
+ // second, add caller's arguments
+ for (int i = 0; i < min.numArgs(); i++) {
+ ExpressionNode en = min.getArg(i);
+ CompositeLocation callerArgLoc =
+ checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
+ false);
+ callerArgList.add(callerArgLoc);
+ }
+
+ // setup callee params set
+ // first, add callee's this location
+ if (!calleemd.isStatic()) {
+ CompositeLocation calleeThisLoc =
+ new CompositeLocation(new Location(calleemd, calleeLattice.getThisLoc()));
+ calleeParamList.add(calleeThisLoc);
+ }
+ // second, add callee's parameters
+ for (int i = 0; i < calleemd.numParameters(); i++) {
+ VarDescriptor calleevd = (VarDescriptor) calleemd.getParameter(i);
+ CompositeLocation calleeLoc = d2loc.get(calleevd);
+ // System.out.println("calleevd=" + calleevd + " loc=" + calleeLoc);
+ calleeParamList.add(calleeLoc);
+ }
+
+ // here, check if ordering relations among caller's args respect
+ // ordering relations in-between callee's args
+ CHECK: for (int i = 0; i < calleeParamList.size(); i++) {
+ CompositeLocation calleeLoc1 = calleeParamList.get(i);
+ CompositeLocation callerLoc1 = callerArgList.get(i);
+
+ for (int j = 0; j < calleeParamList.size(); j++) {
+ if (i != j) {
+ CompositeLocation calleeLoc2 = calleeParamList.get(j);
+ CompositeLocation callerLoc2 = callerArgList.get(j);
+
+ if (callerLoc1.get(callerLoc1.getSize() - 1).isTop()
+ || callerLoc2.get(callerLoc2.getSize() - 1).isTop()) {
+ continue CHECK;
+ }
+
+ // System.out.println("calleeLoc1=" + calleeLoc1);
+ // System.out.println("calleeLoc2=" + calleeLoc2 +
+ // "calleeParamList=" + calleeParamList);
+
+ int callerResult =
+ CompositeLattice.compare(callerLoc1, callerLoc2, true,
+ generateErrorMessage(md.getClassDesc(), min));
+ // System.out.println("callerResult=" + callerResult);
+ int calleeResult =
+ CompositeLattice.compare(calleeLoc1, calleeLoc2, true,
+ generateErrorMessage(md.getClassDesc(), min));
+ // System.out.println("calleeResult=" + calleeResult);
+
+ if (callerResult == ComparisonResult.EQUAL) {
+ if (ssjava.isSharedLocation(callerLoc1.get(callerLoc1.getSize() - 1))
+ && ssjava.isSharedLocation(callerLoc2.get(callerLoc2.getSize() - 1))) {
+ // if both of them are shared locations, promote them to
+ // "GREATER relation"
+ callerResult = ComparisonResult.GREATER;
+ }
+ }
+
+ if (calleeResult == ComparisonResult.GREATER
+ && callerResult != ComparisonResult.GREATER) {
+ // If calleeLoc1 is higher than calleeLoc2
+ // then, caller should have same ordering relation in-bet
+ // callerLoc1 & callerLoc2
+
+ String paramName1, paramName2;
+
+ if (!calleemd.isStatic()) {
+ if (i == 0) {
+ paramName1 = "'THIS'";
+ } else {
+ paramName1 = "'parameter " + calleemd.getParamName(i - 1) + "'";
+ }
+ } else {
+ paramName1 = "'parameter " + calleemd.getParamName(i) + "'";
+ }
+
+ if (!calleemd.isStatic()) {
+ if (j == 0 && !calleemd.isStatic()) {
+ paramName2 = "'THIS'";
+ } else {
+ paramName2 = "'parameter " + calleemd.getParamName(j - 1) + "'";
+ }
+ } else {
+ paramName2 = "'parameter " + calleemd.getParamName(j) + "'";
+ }
+
+ throw new Error(
+ "Caller doesn't respect an ordering relation among method arguments: callee expects that "
+ + paramName1 + " should be higher than " + paramName2 + " in " + calleemd
+ + " at " + md.getClassDesc().getSourceFileName() + ":" + min.getNumLine());
+ }
+ }
+
+ }
+ }
+
+ }
+
+ }
+
+ private CompositeLocation checkLocationFromArrayAccessNode(MethodDescriptor md,
+ SymbolTable nametable, ArrayAccessNode aan, CompositeLocation constraint, boolean isLHS) {
+ // System.out.println("aan=" + aan.printNode(0) + " line#=" + aan.getNumLine());
+ ClassDescriptor cd = md.getClassDesc();
+
+ CompositeLocation arrayLoc =
+ checkLocationFromExpressionNode(md, nametable, aan.getExpression(),
+ new CompositeLocation(), constraint, isLHS);
+
+ // addTypeLocation(aan.getExpression().getType(), arrayLoc);
+ CompositeLocation indexLoc =
+ checkLocationFromExpressionNode(md, nametable, aan.getIndex(), new CompositeLocation(),
+ constraint, isLHS);
+ // addTypeLocation(aan.getIndex().getType(), indexLoc);
+
+ 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<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
+ inputGLB.add(arrayLoc);
+ inputGLB.add(indexLoc);
+ return CompositeLattice.calculateGLB(inputGLB, generateErrorMessage(cd, aan));
+ }
+
+ }
+
+ private CompositeLocation checkLocationFromCreateObjectNode(MethodDescriptor md,
+ SymbolTable nametable, CreateObjectNode con) {
+
+ ClassDescriptor cd = md.getClassDesc();
+
+ CompositeLocation compLoc = new CompositeLocation();
+ compLoc.addLocation(Location.createTopLocation(md));
+ return compLoc;
+
+ }
+
+ private CompositeLocation checkLocationFromOpNode(MethodDescriptor md, SymbolTable nametable,
+ OpNode on, CompositeLocation constraint) {
+
+ ClassDescriptor cd = md.getClassDesc();
+ CompositeLocation leftLoc = new CompositeLocation();
+ 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, constraint, false);
+ // addTypeLocation(on.getRight().getType(), rightLoc);
+ }
+
+ // System.out.println("\n# OP NODE=" + on.printNode(0));
+ // System.out.println("# left loc=" + leftLoc + " from " +