API tools faq
paste
Advertisement
saifcore7

SymbolicStringHandler

saifcore7
Apr 6th, 2025
341
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Java 200.45 KB | Source Code | 0 0
raw download clone embed print report
  1. /*
  2.  * Copyright (C) 2014, United States Government, as represented by the
  3.  * Administrator of the National Aeronautics and Space Administration.
  4.  * All rights reserved.
  5.  *
  6.  * Symbolic Pathfinder (jpf-symbc) is licensed under the Apache License,
  7.  * Version 2.0 (the "License"); you may not use this file except
  8.  * in compliance with the License. You may obtain a copy of the License at
  9.  *
  10.  *        http://www.apache.org/licenses/LICENSE-2.0.
  11.  *
  12.  * Unless required by applicable law or agreed to in writing, software
  13.  * distributed under the License is distributed on an "AS IS" BASIS,
  14.  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15.  * See the License for the specific language governing permissions and
  16.  * limitations under the License.
  17.  */
  18.  
  19. /*  Copyright (C) 2005 United States Government as represented by the
  20. Administrator of the National Aeronautics and Space Administration
  21. (NASA).  All Rights Reserved.
  22.  
  23. Copyright (C) 2009 Fujitsu Laboratories of America, Inc.
  24.  
  25. DISCLAIMER OF WARRANTIES AND LIABILITIES; WAIVER AND INDEMNIFICATION
  26.  
  27. A. No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY
  28. WARRANTY OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY,
  29. INCLUDING, BUT NOT LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE
  30. WILL CONFORM TO SPECIFICATIONS, ANY IMPLIED WARRANTIES OF
  31. MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR FREEDOM FROM
  32. INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE ERROR
  33. FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO
  34. THE SUBJECT SOFTWARE. NO SUPPORT IS WARRANTED TO BE PROVIDED AS IT IS PROVIDED "AS-IS".
  35.  
  36. B. Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS
  37. AGAINST FUJITSU LABORATORIES OF AMERICA AND ANY OF ITS AFFILIATES, THE
  38. UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL
  39. AS ANY PRIOR RECIPIENT.  IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE
  40. RESULTS IN ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING
  41. FROM SUCH USE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING
  42. FROM, RECIPIENT'S USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY
  43. AND HOLD HARMLESS FUJITSU LABORATORTIES OF AMERICA AND ANY OF ITS AFFILIATES,
  44. THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL
  45. AS ANY PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW.  RECIPIENT'S SOLE
  46. REMEDY FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL
  47. TERMINATION OF THIS AGREEMENT. */
  48.  
  49.  
  50.  
  51. package gov.nasa.jpf.symbc.bytecode;
  52.  
  53.  
  54.  
  55. import gov.nasa.jpf.symbc.numeric.*;
  56. import gov.nasa.jpf.vm.ChoiceGenerator;
  57. import gov.nasa.jpf.vm.ClassInfo;
  58. import gov.nasa.jpf.vm.ClassLoaderInfo;
  59. import gov.nasa.jpf.vm.ElementInfo;
  60. import gov.nasa.jpf.vm.FieldInfo;
  61. import gov.nasa.jpf.vm.Instruction;
  62. import gov.nasa.jpf.vm.MethodInfo;
  63. import gov.nasa.jpf.vm.SystemState;
  64. import gov.nasa.jpf.vm.Types;
  65. import gov.nasa.jpf.vm.VM;
  66. import gov.nasa.jpf.vm.StackFrame;
  67. import gov.nasa.jpf.vm.ThreadInfo;
  68. import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
  69. import gov.nasa.jpf.symbc.mixednumstrg.SpecialRealExpression;
  70. import gov.nasa.jpf.symbc.string.*;
  71. import gov.nasa.jpf.symbc.mixednumstrg.*;
  72.  
  73.  
  74. public class SymbolicStringHandler {
  75.     static int handlerStep = 0;
  76.     static Instruction handlerStepSavedNext = null;
  77.     static Object handlerStepSavedValue = null;
  78.  
  79.     public static final int intValueOffset = 5;
  80.  
  81.     /* this method checks if a method has as argument any symbolic strings */
  82.    
  83.     public boolean isMethodStringSymbolic(JVMInvokeInstruction invInst, ThreadInfo th) {
  84.         String cname = invInst.getInvokedMethodClassName();
  85.  
  86.         if (cname.equals("java.lang.String")
  87.                 || cname.equals("java.lang.StringBuilder")
  88.                 || cname.equals("java.lang.StringBuffer")
  89.                 || cname.equals("java.lang.CharSequence")
  90.                 || cname.equals("java.lang.Appendable")
  91.                 || cname.equals("java.io.PrintStream")
  92.                 || cname.equals("java.lang.Integer")
  93.                 || cname.equals("java.lang.Float")
  94.                 || cname.equals("java.lang.Double")
  95.                 || cname.equals("java.lang.Long")
  96.                 || cname.equals("java.lang.Short")
  97.                 || cname.equals("java.lang.Byte")
  98.                 || cname.equals("java.lang.Char")
  99.                 || cname.equals("java.lang.Boolean")
  100.                 || cname.equals("java.lang.Object")) {
  101.            
  102.             StackFrame sf = th.getModifiableTopFrame();
  103.  
  104.             int numStackSlots = invInst.getArgSize();
  105.  
  106.             for (int i = 0; i < numStackSlots; i++) {
  107.                 Expression sym_v1 = (Expression) sf.getOperandAttr(i);
  108.                 if (sym_v1 != null) {
  109.                     if (sym_v1 instanceof SymbolicStringBuilder) { // check if
  110.                         // StringBuilder has
  111.                         // empty attribute
  112.                         if (((SymbolicStringBuilder) sym_v1).getstr() != null) {
  113.                             return true;
  114.                         }
  115.                     } else if (sym_v1 instanceof IntegerExpression && cname.equals("java.lang.StringBuilder")){
  116.                         //to revise
  117.                         return true;
  118.                     } else {
  119.                         return true;
  120.                     }
  121.                    
  122.                 }
  123.             }
  124.             return false;
  125.         }  
  126.         else return false;
  127.     }
  128.  
  129.     public Instruction handleSymbolicStrings(JVMInvokeInstruction invInst, ThreadInfo th) {
  130.  
  131.         boolean needToHandle = isMethodStringSymbolic(invInst, th);
  132.  
  133.         if (needToHandle) {
  134.             // do the string manipulations
  135.             String mname = invInst.getInvokedMethodName();
  136.             String shortName = mname.substring(0, mname.indexOf("("));
  137.             if (shortName.equals("concat")) {
  138.                 Instruction handled = handleConcat(invInst, th);
  139.                 if (handled != null) {
  140.                     return handled;
  141.                 }
  142.             } else if (shortName.equals("equals")) {
  143.                 ChoiceGenerator<?> cg;
  144.                 if (!th.isFirstStepInsn()) { // first time around
  145.                     cg = new PCChoiceGenerator(2);
  146.                     th.getVM().setNextChoiceGenerator(cg);
  147.                     return invInst;
  148.                 } else {
  149.                     handleObjectEquals(invInst, th);
  150.                     return invInst.getNext(th);
  151.                 }
  152.             } else if (shortName.equals("equalsIgnoreCase")) {
  153.                 ChoiceGenerator<?> cg;
  154.                 if (!th.isFirstStepInsn()) { // first time around
  155.                     cg = new PCChoiceGenerator(2);
  156.                     th.getVM().setNextChoiceGenerator(cg);
  157.                     return invInst;
  158.                 } else {
  159.                     handleEqualsIgnoreCase(invInst,  th);
  160.                     return invInst.getNext(th);
  161.                 }
  162.             } else if (shortName.equals("endsWith")) {
  163.                 ChoiceGenerator<?> cg;
  164.                 if (!th.isFirstStepInsn()) { // first time around
  165.                     cg = new PCChoiceGenerator(2);
  166.                     th.getVM().setNextChoiceGenerator(cg);
  167.                     return invInst;
  168.                 } else {
  169.                     handleEndsWith(invInst, th);
  170.                     return invInst.getNext(th);
  171.                 }
  172.             } else if (shortName.equals("startsWith")) {
  173.                 ChoiceGenerator<?> cg;
  174.                 if (!th.isFirstStepInsn()) { // first time around
  175.                     cg = new PCChoiceGenerator(2);
  176.                     th.getVM().setNextChoiceGenerator(cg);
  177.                     return invInst;
  178.                 } else {
  179.                     handleStartsWith(invInst, th);
  180.                     return invInst.getNext(th);
  181.                 }
  182.             } else if (shortName.equals ("contains")) {
  183.                 ChoiceGenerator<?> cg;
  184.                 if (!th.isFirstStepInsn()) { // first time around
  185.                     cg = new PCChoiceGenerator(2);
  186.                     th.getVM().setNextChoiceGenerator(cg);
  187.                     return invInst;
  188.                 } else {
  189.                     handleContains(invInst, th);
  190.                     return invInst.getNext(th);
  191.                 }
  192.             } else if (shortName.equals("append")) {
  193.                 Instruction handled = handleAppend(invInst, th);
  194.                 if (handled != null) {
  195.                     return handled;
  196.                 }
  197.             } else if (shortName.equals("length")) {
  198.                 handleLength(invInst, th);
  199.             } else if (shortName.equals("indexOf")) {
  200.                 handleIndexOf(invInst, th);
  201.             } else if (shortName.equals("lastIndexOf")) {
  202.                 handleLastIndexOf(invInst, th);
  203.             } else if (shortName.equals("charAt")) {
  204.                 handleCharAt (invInst, th); // returns boolean that is ignored
  205.                 //return invInst;
  206.             } else if (shortName.equals("replace")) {
  207.                 Instruction handled = handleReplace(invInst, th);
  208.                 if (handled != null) {
  209.                     return handled;
  210.                 }
  211.             } else if (shortName.equals("replaceFirst")) {
  212.                 Instruction handled = handleReplaceFirst(invInst, th);
  213.                 if (handled != null) {
  214.                     return handled;
  215.                 }
  216.             } else if (shortName.equals("trim")) {
  217.                 handleTrim(invInst, th);
  218.             } else if (shortName.equals("substring")) {
  219.                 Instruction handled = handleSubString(invInst, th);
  220.                 if (handled != null) {
  221.                     return handled;
  222.                 }
  223.             } else if (shortName.equals("valueOf")) {
  224.                 Instruction handled = handleValueOf(invInst, th);
  225.                 if (handled != null) {
  226.                     return handled;
  227.                 }
  228.             } else if (shortName.equals("parseInt")) {
  229.                 ChoiceGenerator<?> cg;
  230.                 if (!th.isFirstStepInsn()) { // first time around
  231.                     cg = new PCChoiceGenerator(2);
  232.                     th.getVM().setNextChoiceGenerator(cg);
  233.                     return invInst;
  234.                 } else {
  235.                     handleParseInt(invInst, th);
  236.                     return invInst.getNext(th);
  237.                 }
  238.             } else if (shortName.equals("parseFloat")) {
  239.                 ChoiceGenerator<?> cg;
  240.                 if (!th.isFirstStepInsn()) { // first time around
  241.                     cg = new PCChoiceGenerator(2);
  242.                     th.getVM().setNextChoiceGenerator(cg);
  243.                     return invInst;
  244.                 } else {
  245.                     handleParseFloat(invInst, th);
  246.                     return invInst.getNext(th);
  247.                 }
  248.             } else if (shortName.equals("parseLong")) {
  249.                 ChoiceGenerator<?> cg;
  250.                 if (!th.isFirstStepInsn()) { // first time around
  251.                     cg = new PCChoiceGenerator(2);
  252.                     th.getVM().setNextChoiceGenerator(cg);
  253.                     return invInst;
  254.                 } else {
  255.                     handleParseLong(invInst, th);
  256.                     return invInst.getNext(th);
  257.                 }
  258.             } else if (shortName.equals("parseDouble")) {
  259.                 ChoiceGenerator<?> cg;
  260.                 if (!th.isFirstStepInsn()) { // first time around
  261.                     cg = new PCChoiceGenerator(2);
  262.                     th.getVM().setNextChoiceGenerator(cg);
  263.                     return invInst;
  264.                 } else {
  265.                     handleParseDouble(invInst, th);
  266.                     return invInst.getNext(th);
  267.                 }
  268.             } else if (shortName.equals("parseBoolean")) {
  269.                 ChoiceGenerator<?> cg;
  270.                 if (!th.isFirstStepInsn()) { // first time around
  271.                     cg = new PCChoiceGenerator(2);
  272.                     th.getVM().setNextChoiceGenerator(cg);
  273.                     return invInst;
  274.                 } else {
  275.                     handleParseBoolean(invInst, th);
  276.                     return invInst.getNext(th);
  277.                 }
  278.             } else if (shortName.equals("toString")) {
  279.                 Instruction handled = handletoString(invInst, th);
  280.                 if (handled != null) {
  281.                     return handled;
  282.                 }
  283.             } else if (shortName.equals("println")) {
  284.                 handleprintln(invInst, th, true);
  285.             } else if (shortName.equals("print")) {
  286.                 handleprintln(invInst, th, false);
  287.             } else if (shortName.equals("<init>")) {
  288.                 Instruction handled = handleInit(invInst, th);
  289.                 if (handled != null) {
  290.                     return handled;
  291.                 } else {
  292.                     return null;
  293.                 }
  294.             } else if (shortName.equals("intValue")) {
  295.                 handleintValue(invInst, th);
  296.             } else if (shortName.equals("floatValue")) {
  297.                 handlefloatValue(invInst, th);
  298.             } else if (shortName.equals("longValue")) {
  299.                 handlelongValue(invInst, th);
  300.             } else if (shortName.equals("doubleValue")) {
  301.                 handledoubleValue(invInst, th);
  302.             } else if (shortName.equals("booleanValue")) {
  303.                 handlefloatValue(invInst, th);
  304.             } else if (shortName.equals("isEmpty")) {
  305.                 ChoiceGenerator<?> cg;
  306.                 if (!th.isFirstStepInsn()){
  307.                     cg = new PCChoiceGenerator(2);
  308.                     th.getVM().setNextChoiceGenerator(cg);
  309.                     return invInst;
  310.                 } else {
  311.                     handleIsEmpty(invInst, th);
  312.                     return invInst.getNext(th);
  313.                 }
  314.             }else {
  315.                 throw new RuntimeException("ERROR: symbolic method not handled: " + shortName);
  316.                 //return null;
  317.             }
  318.             return invInst.getNext(th);
  319.         } else {
  320.             return null;
  321.         }
  322.  
  323.     }
  324.  
  325.     private boolean handleCharAt (JVMInvokeInstruction invInst, ThreadInfo th) {
  326.         StackFrame sf = th.getModifiableTopFrame();
  327.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  328.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  329.         boolean bresult = false;
  330.         if ((sym_v1 == null) & (sym_v2 == null)) {
  331.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleCharAt");
  332.         } else {
  333.             int s1 = sf.pop();
  334.             int s2 = sf.pop();
  335.  
  336.             IntegerExpression result = null;
  337.             if (sym_v1 == null) { // operand 0 is concrete
  338.  
  339.                 int val = s1;
  340.                 result = sym_v2._charAt(new IntegerConstant(val));
  341.             } else {
  342.  
  343.                 if (sym_v2 == null) {
  344.                     ElementInfo e1 = th.getElementInfo(s2);
  345.                     String val2 = e1.asString();
  346.                     sym_v2 = new StringConstant(val2);
  347.                     result = sym_v2._charAt(sym_v1);
  348.                 } else {
  349.                     result = sym_v2._charAt(sym_v1);
  350.                 }
  351.                 bresult = true;
  352.                 //System.out.println("[handleCharAt] Ignoring: " + result.toString());
  353.                 //th.push(0, false);
  354.             }
  355.             sf.push(0, false);
  356.             sf.setOperandAttr(result);
  357.         }
  358.         return bresult; // not used
  359.  
  360.     }
  361.  
  362.     public void handleLength(JVMInvokeInstruction invInst, ThreadInfo th) {
  363.         StackFrame sf = th.getModifiableTopFrame();
  364.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  365.         if (sym_v1 == null) {
  366.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleLength");
  367.         } else {
  368.             sf.pop();
  369.             sf.push(0, false); /* dont care value for length */
  370.             IntegerExpression sym_v2 = sym_v1._length();
  371.             sf.setOperandAttr(sym_v2);
  372.         }
  373.  
  374.     }
  375.  
  376.     public void handleIndexOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  377.         int numStackSlots = invInst.getArgSize();
  378.         if (numStackSlots == 2) {
  379.             handleIndexOf1(invInst, th);
  380.         } else {
  381.             handleIndexOf2(invInst, th);
  382.         }
  383.  
  384.     }
  385.  
  386.     /* two possibilities int, or String in parameter */
  387.     public void handleIndexOf1(JVMInvokeInstruction invInst, ThreadInfo th) {
  388.         StackFrame sf = th.getModifiableTopFrame();
  389.        
  390.         //boolean castException = false;
  391.         StringExpression sym_v1 = null;
  392.         Expression sym_v2 = null; // could be String or Char
  393.         sym_v1 = (StringExpression)sf.getOperandAttr(1);
  394.         sym_v2 = (Expression) sf.getOperandAttr(0);
  395.         if (sym_v1 == null && sym_v2 == null) {
  396.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleIndexOf1");
  397.         } else {
  398.             boolean s2char = true; //argument is char
  399.             if (sf.isOperandRef()) {
  400.                 s2char = false; //argument is string
  401.             }
  402.            
  403.             int s1 = sf.pop();
  404.             int s2 = sf.pop();
  405.  
  406.             IntegerExpression result = null;
  407.             if (sym_v1 != null) {
  408.                     if (sym_v2 != null) { // both are symbolic values
  409.                         if (s2char)
  410.                             result = sym_v1._indexOf((IntegerExpression)sym_v2);
  411.                         else
  412.                             result = sym_v1._indexOf((StringExpression)sym_v2);
  413.                     } else { // sym_v2 is null
  414.                         if (s2char) {
  415.                             result = sym_v1._indexOf(new IntegerConstant(s2));
  416.                         }
  417.                         else {
  418.                             ElementInfo e2 = th.getElementInfo(s2);
  419.                             String val = e2.asString();
  420.                             result = sym_v1._indexOf(new StringConstant(val));
  421.                         }
  422.                     }
  423.             } else { // sym_v1 is null, sym_v2 must be not null
  424.                     assert(sym_v2!=null);
  425.                     ElementInfo e1 = th.getElementInfo(s2);
  426.                     String val = e1.asString();
  427.                     if (s2char)
  428.                         result = new StringConstant(val)._indexOf((IntegerExpression)sym_v2);
  429.                     else
  430.                         result = new StringConstant(val)._indexOf((StringExpression)sym_v2);
  431.             }
  432.             sf.push(0, false);
  433.             assert result != null;
  434.             sf.setOperandAttr(result);
  435.  
  436.  
  437.         }
  438.     }
  439.  
  440.     /* two possibilities int, int or int, String in parameters */
  441.     public void handleIndexOf2(JVMInvokeInstruction invInst, ThreadInfo th) {
  442.  
  443.         StackFrame sf = th.getModifiableTopFrame();
  444.  
  445.         StringExpression sym_v1 = null;
  446.         Expression sym_v2 = null;
  447.         IntegerExpression intExp = null;
  448.         sym_v1 = (StringExpression) sf.getOperandAttr(2);
  449.         intExp = (IntegerExpression) sf.getOperandAttr(0);
  450.         sym_v2 = (Expression) sf.getOperandAttr(1);
  451.  
  452.         if (sym_v1 == null && sym_v2 == null && intExp == null) {
  453.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleIndexOf2");
  454.         } else {
  455.  
  456.             int i1 = sf.pop();
  457.             boolean s2char = true;
  458.             if (sf.isOperandRef()) {
  459.                 //System.out.println("[handleIndexOf2] string detected");
  460.                 s2char = false;
  461.             }
  462.            
  463.             int s2 = sf.pop();
  464.             int s1 = sf.pop();
  465.  
  466.             IntegerExpression result = null;
  467.             if (intExp != null) {
  468.                 if (sym_v1 != null) {
  469.                     if (sym_v2 != null) { // both are symbolic values
  470.                         if (s2char)
  471.                             result = sym_v1._indexOf((IntegerExpression)sym_v2, intExp);
  472.                         else
  473.                             result = sym_v1._indexOf((StringExpression)sym_v2, intExp);
  474.                     } else { //sym_v2 is null
  475.                         if (s2char) {
  476.                             result = sym_v1._indexOf(new IntegerConstant(s2), intExp);
  477.                         }
  478.                         else {
  479.                             ElementInfo e2 = th.getElementInfo(s2);
  480.                             String val = e2.asString();
  481.                             result = sym_v1._indexOf(new StringConstant(val), intExp);
  482.                         }
  483.                     }
  484.                 } else { // sym_v1 is null
  485.                     ElementInfo e1 = th.getElementInfo(s1);
  486.                     String val = e1.asString();
  487.  
  488.                     if (sym_v2 != null) {
  489.                         if(s2char)
  490.                             result = new StringConstant(val)._indexOf((IntegerExpression)sym_v2, intExp);
  491.                         else
  492.                             result = new StringConstant(val)._indexOf((StringExpression)sym_v2, intExp);
  493.                     } else {
  494.                         if (s2char) {
  495.                             result = new StringConstant(val)._indexOf(new IntegerConstant(s2), intExp);
  496.                         }
  497.                         else {
  498.                             ElementInfo e2 = th.getElementInfo(s2);
  499.                             String val2 = e2.asString();
  500.                             result = new StringConstant(val)._indexOf(new StringConstant(val2), intExp);
  501.                         }
  502.                     }
  503.                 }
  504.             }
  505.             else { //intExp is null
  506.                 if (sym_v1 != null) {
  507.                     if (sym_v2 != null) { // both are symbolic values
  508.                         if(s2char)
  509.                             result = sym_v1._indexOf((IntegerExpression)sym_v2, new IntegerConstant(i1));
  510.                         else
  511.                             result = sym_v1._indexOf((StringExpression)sym_v2, new IntegerConstant(i1));
  512.                     } else { //sym_v1 is null
  513.                         if (s2char) {
  514.                             result = sym_v1._indexOf(new IntegerConstant(s2), new IntegerConstant(i1));
  515.                         }
  516.                         else {
  517.                             ElementInfo e2 = th.getElementInfo(s2);
  518.                             String val = e2.asString();
  519.                             result = sym_v1._indexOf(new StringConstant(val), new IntegerConstant(i1));
  520.                             //System.out.println("[handleIndexOf2] Special push");
  521.                             //Special push?
  522.                             //th.push(s1, true);
  523.                         }
  524.                     }
  525.                 } else {//sym_v1 is null
  526.                     ElementInfo e1 = th.getElementInfo(s1);
  527.                     String val = e1.asString();
  528.  
  529.                     if (sym_v2 != null) {
  530.                         if(s2char)
  531.                             result = new StringConstant(val)._indexOf((IntegerExpression)sym_v2, new IntegerConstant(i1));
  532.                         else
  533.                             result = new StringConstant(val)._indexOf((StringExpression)sym_v2, new IntegerConstant(i1));
  534.                     } else {
  535.                         if (s2char) {
  536.                             result = new StringConstant(val)._indexOf(new IntegerConstant(s2), new IntegerConstant(i1));
  537.                         }
  538.                         else {
  539.                             ElementInfo e2 = th.getElementInfo(s2);
  540.                             String val2 = e2.asString();
  541.                             result = new StringConstant(val)._indexOf(new StringConstant(val2), new IntegerConstant(i1));
  542.                         }
  543.                     }
  544.                 }
  545.             }
  546.             sf.push(0, false);
  547.             assert result != null;
  548.             sf.setOperandAttr(result);
  549.  
  550.         }
  551.     }
  552.    
  553.     public void handleLastIndexOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  554.         int numStackSlots = invInst.getArgSize();
  555.         if (numStackSlots == 2) {
  556.             handleLastIndexOf1(invInst, th);
  557.         } else {
  558.             handleLastIndexOf2(invInst, th);
  559.         }
  560.     }
  561.  
  562.     public void handleLastIndexOf1(JVMInvokeInstruction invInst, ThreadInfo th) {
  563.         StackFrame sf = th.getModifiableTopFrame();
  564.         //boolean castException = false;
  565.         StringExpression sym_v1 = null;
  566.         StringExpression sym_v2 = null;
  567.         sym_v1 = (StringExpression) sf.getOperandAttr(1);
  568.         /*  */
  569.         sym_v2 = (StringExpression) sf.getOperandAttr(0);
  570.         if (sym_v1 == null && sym_v2 == null) {
  571.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleLastIndexOf1");
  572.         } else {
  573.             boolean s1char = true; //argument is char
  574.             if (sf.isOperandRef()) {
  575.                 s1char = false; //argument is string
  576.             }
  577.             int s1 = sf.pop();
  578.             int s2 = sf.pop();
  579.  
  580.             IntegerExpression result = null;
  581.                 if (sym_v1 != null) {
  582.                     if (sym_v2 != null) { // both are symbolic values
  583.                         result = sym_v1._lastIndexOf(sym_v2);
  584.                     } else {
  585.                         if (s1char) {
  586.                             result = sym_v1._lastIndexOf(new IntegerConstant(s1));
  587.                         }
  588.                         else {
  589.                             ElementInfo e2 = th.getElementInfo(s1);
  590.                             String val = e2.asString();
  591.                             result = sym_v1._lastIndexOf(new StringConstant(val));
  592.                         }
  593.                     }
  594.                 } else {//sym_v1 is null
  595.                     ElementInfo e1 = th.getElementInfo(s2);
  596.                     String val = e1.asString();
  597.                     assert(sym_v2!=null);
  598.                     result = new StringConstant(val)._lastIndexOf(sym_v2);
  599.                    
  600.                 }
  601.            
  602.             sf.push(0, false);
  603.             assert result != null;
  604.             sf.setOperandAttr(result);
  605.  
  606.         }
  607.     }
  608.  
  609.     public void handleLastIndexOf2(JVMInvokeInstruction invInst, ThreadInfo th) {
  610.         StackFrame sf = th.getModifiableTopFrame();
  611.  
  612.         StringExpression sym_v1 = null;
  613.         StringExpression sym_v2 = null;
  614.         IntegerExpression intExp = null;
  615.         sym_v1 = (StringExpression) sf.getOperandAttr(2);
  616.         intExp = (IntegerExpression) sf.getOperandAttr(0);
  617.         sym_v2 = (StringExpression) sf.getOperandAttr(1);
  618.  
  619.         if (sym_v1 == null && sym_v2 == null && intExp == null) {
  620.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleLastIndexOf2");
  621.         } else {
  622.             int i1 = sf.pop();
  623.             boolean s2char = true;
  624.             if (th.getModifiableTopFrame().isOperandRef()) {
  625.                 s2char = false;
  626.             }
  627.            
  628.             int s2 = sf.pop();
  629.             int s1 = sf.pop();
  630.  
  631.             IntegerExpression result = null;
  632.             if (intExp != null) {
  633.                 if (sym_v1 != null) {
  634.                     if (sym_v2 != null) { // both are symbolic values
  635.                         result = sym_v1._lastIndexOf(sym_v2, intExp);
  636.                     } else {
  637.                         if (s2char) {
  638.                             result = sym_v1._lastIndexOf(new IntegerConstant(s2), intExp);
  639.                         }
  640.                         else {
  641.                             ElementInfo e2 = th.getElementInfo(s2);
  642.                             String val = e2.asString();
  643.                             result = sym_v1._lastIndexOf(new StringConstant(val), intExp);
  644.                         }
  645.                     }
  646.                 } else { //sym_v1 is null
  647.                     ElementInfo e1 = th.getElementInfo(s1);
  648.                     String val = e1.asString();
  649.  
  650.                     if (sym_v2 != null) {
  651.                         result = new StringConstant(val)._lastIndexOf(sym_v2, intExp);
  652.                     } else {
  653.                         if (s2char) {
  654.                             result = new StringConstant(val)._lastIndexOf(new IntegerConstant(s2), intExp);
  655.                         }
  656.                         else {
  657.                             ElementInfo e2 = th.getElementInfo(s2);
  658.                             String val2 = e2.asString();
  659.                             result = new StringConstant(val)._lastIndexOf(new StringConstant(val2), intExp);
  660.                         }
  661.                     }
  662.                 }
  663.             }
  664.             else { // intExp is null
  665.                 if (sym_v1 != null) {
  666.                     if (sym_v2 != null) { // both are symbolic values
  667.                         result = sym_v1._lastIndexOf(sym_v2, new IntegerConstant(i1));
  668.                     } else {
  669.                         if (s2char) {
  670.                             result = sym_v1._lastIndexOf(new IntegerConstant(s2), new IntegerConstant(i1));
  671.                         }
  672.                         else {
  673.                             ElementInfo e2 = th.getElementInfo(s2);
  674.                             String val = e2.asString();
  675.                             result = sym_v1._lastIndexOf(new StringConstant(val), new IntegerConstant(i1));
  676.                             //System.out.println("[handleIndexOf2] Special push");
  677.                             //Special push?
  678.                             //th.push(s1, true);
  679.                         }
  680.                     }
  681.                 } else { // sym_v1 is null
  682.                     ElementInfo e1 = th.getElementInfo(s1);
  683.                     String val = e1.asString();
  684.                     assert(sym_v2!=null);
  685.                     result = new StringConstant(val)._lastIndexOf(sym_v2, new IntegerConstant(i1));
  686.                 }
  687.             }
  688.            
  689.             sf.push(0, false);
  690.             assert result != null;
  691.             sf.setOperandAttr(result);
  692.  
  693.         }
  694.     }
  695.  
  696.  
  697.    
  698.  
  699.     public void handlebooleanValue(JVMInvokeInstruction invInst, SystemState ss, ThreadInfo th) {
  700.         StackFrame sf = th.getModifiableTopFrame();
  701.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  702.  
  703.         if (sym_v3 == null) {
  704.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandlebooleanValue");
  705.         } else {
  706.             if (sym_v3 instanceof IntegerExpression) {
  707.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  708.                 sf.pop();
  709.                 sf.push(0, false);
  710.                 sf.setOperandAttr(sym_v2);
  711.             } else {
  712.                 throw new RuntimeException("ERROR: operand type not tackled - booleanValue");
  713.             }
  714.  
  715.         }
  716.  
  717.     }
  718.  
  719.     public void handleintValue(JVMInvokeInstruction invInst,  ThreadInfo th) {
  720.         StackFrame sf = th.getModifiableTopFrame();
  721.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  722.  
  723.         if (sym_v3 == null) {
  724.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleintValue");
  725.         } else {
  726.             if (sym_v3 instanceof IntegerExpression) {
  727.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  728.                 sf.pop();
  729.                 sf.push(0, false);
  730.                 sf.setOperandAttr(sym_v2);
  731.             } else {
  732.                 th.printStackTrace();
  733.                 throw new RuntimeException("ERROR: operand type not tackled - intValue");
  734.             }
  735.         }
  736.     }
  737.  
  738.     public void handlelongValue(JVMInvokeInstruction invInst,  ThreadInfo th) {
  739.         StackFrame sf = th.getModifiableTopFrame();
  740.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  741.  
  742.         if (sym_v3 == null) {
  743.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: hanldeLongValue");
  744.         } else {
  745.             if (sym_v3 instanceof IntegerExpression) {
  746.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  747.                 sf.pop();
  748.                 sf.pushLong((long) 0);
  749.                 sf.setLongOperandAttr(sym_v2);
  750.             } else {
  751.                 throw new RuntimeException("ERROR: operand type not tackled - longValue");
  752.             }
  753.  
  754.         }
  755.  
  756.     }
  757.  
  758.     public void handlefloatValue(JVMInvokeInstruction invInst,  ThreadInfo th) {
  759.         StackFrame sf = th.getModifiableTopFrame();
  760.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  761.  
  762.         if (sym_v3 == null) {
  763.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand: hanldeFloatValue");
  764.         } else {
  765.             if (sym_v3 instanceof RealExpression) {
  766.                 RealExpression sym_v2 = (RealExpression) sym_v3;
  767.                 sf.pop();
  768.                 sf.push(0, false);
  769.                 sf.setOperandAttr(sym_v2);
  770.             } else {
  771.                 throw new RuntimeException("ERROR: operand type not tackled - floatValue");
  772.             }
  773.  
  774.         }
  775.  
  776.     }
  777.  
  778.     public void handledoubleValue(JVMInvokeInstruction invInst,  ThreadInfo th) {
  779.         StackFrame sf = th.getModifiableTopFrame();
  780.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  781.  
  782.         if (sym_v3 == null) {
  783.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand: hanldeDoubleValue");
  784.         } else {
  785.             if (sym_v3 instanceof RealExpression) {
  786.                 RealExpression sym_v2 = (RealExpression) sym_v3;
  787.                 sf.pop();
  788.                 sf.pushLong((long) 0);
  789.                 sf.setLongOperandAttr(sym_v2);
  790.             } else {
  791.                 throw new RuntimeException("ERROR: operand type not tackled - doubleValue");
  792.             }
  793.  
  794.         }
  795.  
  796.     }
  797.  
  798.     /*
  799.      * StringBuilder or StringBuffer or BigDecimal initiation with symbolic
  800.      * primitives
  801.      */
  802.  
  803.     public Instruction handleInit(JVMInvokeInstruction invInst,  ThreadInfo th) {
  804.  
  805.         String cname = invInst.getInvokedMethodClassName();
  806.         if (cname.equals("java.lang.StringBuilder") || cname.equals("java.lang.StringBuffer")) {
  807.             StackFrame sf = th.getModifiableTopFrame();
  808.             StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  809.             SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  810.             if (sym_v1 == null) {
  811.                 throw new RuntimeException("ERROR: symbolic StringBuilder method must have one symbolic operand in Init");
  812.             } else {
  813.                 sf.pop(); /* string object */
  814.                 sf.pop(); /* one stringBuilder Object */
  815.                 sym_v2.putstr(sym_v1);
  816.                 sf.setOperandAttr(sym_v2);
  817.                 return invInst.getNext();
  818.             }
  819.         } else {
  820.             // Corina TODO: we should allow symbolic string analysis to kick in only when desired
  821.             //throw new RuntimeException("Warning Symbolic String Analysis: Initialization type not handled in symbc/bytecode/SymbolicStringHandler init");
  822.             return null;
  823.         }
  824.     }
  825.  
  826.     /***************************** Symbolic Big Decimal Routines end ****************/
  827.  
  828.  
  829.     private void handleBooleanStringInstructions(JVMInvokeInstruction invInst,  ThreadInfo th, StringComparator comp) {
  830.         StackFrame sf = th.getModifiableTopFrame();
  831.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  832.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  833.  
  834.         if ((sym_v1 == null) & (sym_v2 == null)) {
  835.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleStartsWith");
  836.         } else {
  837.             ChoiceGenerator<?> cg;
  838.             boolean conditionValue;
  839.  
  840.             cg = th.getVM().getChoiceGenerator();
  841.             assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  842.             conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  843.  
  844.             // System.out.println("conditionValue: " + conditionValue);
  845.  
  846.             int s1 = sf.pop();
  847.             int s2 = sf.pop();
  848.             PathCondition pc;
  849.  
  850.             // pc is updated with the pc stored in the choice generator above
  851.             // get the path condition from the
  852.             // previous choice generator of the same type
  853.  
  854.             ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  855.             while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  856.                 prev_cg = prev_cg.getPreviousChoiceGenerator();
  857.             }
  858.  
  859.             if (prev_cg == null) {
  860.                 pc = new PathCondition();
  861.             } else {
  862.                 pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  863.             }
  864.  
  865.             assert pc != null;
  866.  
  867.             if (conditionValue) {
  868.                 if (sym_v1 != null) {
  869.                     if (sym_v2 != null) { // both are symbolic values
  870.                         pc.spc._addDet(comp, sym_v1, sym_v2);
  871.                     } else {
  872.                         ElementInfo e2 = th.getElementInfo(s2);
  873.                         String val = e2.asString();
  874.                         pc.spc._addDet(comp, sym_v1, val);
  875.                     }
  876.                 } else {
  877.                     ElementInfo e1 = th.getElementInfo(s1);
  878.                     String val = e1.asString();
  879.                     pc.spc._addDet(comp, val, sym_v2);
  880.                 }
  881.                 if (!pc.simplify()) {// not satisfiable
  882.                     th.getVM().getSystemState().setIgnored(true);
  883.                 } else {
  884.                     // pc.solve();
  885.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  886.                     // System.out.println(((PCChoiceGenerator) cg).getCurrentPC());
  887.                 }
  888.             } else {
  889.                 if (sym_v1 != null) {
  890.                     if (sym_v2 != null) { // both are symbolic values
  891.                         pc.spc._addDet(comp.not(), sym_v1, sym_v2);
  892.                     } else {
  893.                         ElementInfo e2 = th.getElementInfo(s2);
  894.                         String val = e2.asString();
  895.                         pc.spc._addDet(comp.not(), sym_v1, val);
  896.  
  897.                     }
  898.                 } else {
  899.                     ElementInfo e1 = th.getElementInfo(s1);
  900.                     String val = e1.asString();
  901.                     pc.spc._addDet(comp.not(), val, sym_v2);
  902.                 }
  903.                 if (!pc.simplify()) {// not satisfiable
  904.                     th.getVM().getSystemState().setIgnored(true);
  905.                 } else {
  906.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  907.                 }
  908.             }
  909.  
  910.             sf.push(conditionValue ? 1 : 0, true);
  911.  
  912.         }
  913.  
  914.     }
  915.  
  916.     public void handleEqualsIgnoreCase(JVMInvokeInstruction invInst,  ThreadInfo th) {
  917.         throw new RuntimeException("ERROR: symbolic string method not Implemented - EqualsIgnoreCase");
  918.     }
  919.  
  920.     public void handleEndsWith(JVMInvokeInstruction invInst,  ThreadInfo th) {
  921.         //throw new RuntimeException("ERROR: symbolic string method not Implemented - EndsWith");
  922.         handleBooleanStringInstructions(invInst,  th, StringComparator.ENDSWITH);
  923.     }
  924.  
  925.     public void handleContains (JVMInvokeInstruction invInst,  ThreadInfo th) {
  926.         handleBooleanStringInstructions(invInst,  th, StringComparator.CONTAINS);
  927.     }
  928.  
  929.  
  930.     public void handleStartsWith(JVMInvokeInstruction invInst,  ThreadInfo th) {
  931.         //throw new RuntimeException("ERROR: symbolic string method not Implemented - StartsWith");
  932.         handleBooleanStringInstructions(invInst, th, StringComparator.STARTSWITH);
  933.     }
  934.  
  935.     //Only supports character for character
  936.     public Instruction handleReplace(JVMInvokeInstruction invInst, ThreadInfo th) {
  937.         StackFrame sf = th.getModifiableTopFrame();
  938.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  939.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  940.         StringExpression sym_v3 = (StringExpression) sf.getOperandAttr(2);
  941.  
  942.         if ((sym_v1 == null) & (sym_v2 == null) & (sym_v3 == null)) {
  943.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleReplace");
  944.         } else {
  945.             int s1 = sf.pop();
  946.             int s2 = sf.pop();
  947.             int s3 = sf.pop();
  948.             //System.out.println("[handleReplace] " + s1 + " " + s2 + " " + s3);
  949.             StringExpression result = null;
  950.             if (sym_v1 == null) { // operand 0 is concrete
  951.                 //ElementInfo e1 = th.getElementInfo(s1);
  952.                 String val = String.valueOf((char) s1);
  953.                 if (sym_v2 == null) { // sym_v3 has to be symbolic
  954.                     //ElementInfo e2 = th.getElementInfo(s2);
  955.                     //String val1 = e2.asString();
  956.                     result = sym_v3._replace(val, String.valueOf((char)s2));
  957.                 } else {
  958.                     if (sym_v3 == null) { // only sym_v2 is symbolic
  959.                         ElementInfo e3 = th.getElementInfo(s3);
  960.                         String val2 = e3.asString();
  961.                         sym_v3 = new StringConstant(val2);
  962.                         result = sym_v3._replace(val, sym_v2);
  963.                     } else {
  964.                         result = sym_v3._replace(val, sym_v2);
  965.                     }
  966.                 }
  967.             } else { // sym_v1 is symbolic
  968.                 if (sym_v2 == null) {
  969.                     if (sym_v3 == null) {
  970.                         //ElementInfo e2 = th.getElementInfo(s2);
  971.                         String val1 = String.valueOf((char) s2);
  972.                         //ElementInfo e3 = th.getElementInfo(s3);
  973.                         String val2 = String.valueOf((char) s3);
  974.                         sym_v3 = new StringConstant(val2);
  975.                         result = sym_v3._replace(sym_v1, val1);
  976.                     } else {
  977.                         //ElementInfo e2 = th.getElementInfo(s2);
  978.                         String val1 = String.valueOf((char) s2);
  979.                         result = sym_v3._replace(sym_v1, val1);
  980.                     }
  981.                 } else {
  982.                     if (sym_v3 == null) {
  983.                         ElementInfo e3 = th.getElementInfo(s3);
  984.                         String val2 = e3.asString();
  985.                         sym_v3 = new StringConstant(val2);
  986.                         result = sym_v3._replace(sym_v1, sym_v2);
  987.                     } else {
  988.                         result = sym_v3._replace(sym_v1, sym_v2);
  989.                     }
  990.                 }
  991.             }
  992.             ElementInfo objRef = th.getHeap().newString("", th); /*
  993.                                                                                                                                      * dummy
  994.                                                                                                                                      * String
  995.                                                                                                                                      * Object
  996.                                                                                                                                      */
  997.             sf.push(objRef.getObjectRef(), true);
  998.             sf.setOperandAttr(result);
  999.         }
  1000.         return null;
  1001.     }
  1002.  
  1003.     public Instruction handleSubString(JVMInvokeInstruction invInst, ThreadInfo th) {
  1004.         int numStackSlots = invInst.getArgSize();
  1005.         if (numStackSlots == 2) {
  1006.             return handleSubString1(invInst, th);
  1007.         } else {
  1008.             return handleSubString2(invInst, th);
  1009.         }
  1010.     }
  1011.  
  1012.     public Instruction handleSubString1(JVMInvokeInstruction invInst, ThreadInfo th) {
  1013.         StackFrame sf = th.getModifiableTopFrame();
  1014.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  1015.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  1016.  
  1017.         if ((sym_v1 == null) & (sym_v2 == null)) {
  1018.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleSubString1");
  1019.         } else {
  1020.             int s1 = sf.pop();
  1021.             int s2 = sf.pop();
  1022.  
  1023.             StringExpression result = null;
  1024.             if (sym_v1 == null) { // operand 0 is concrete
  1025.                 int val = s1;
  1026.                 result = sym_v2._subString(val);
  1027.             } else {
  1028.                 if (sym_v2 == null) {
  1029.                     ElementInfo e1 = th.getElementInfo(s2);
  1030.                     String val2 = e1.asString();
  1031.                     sym_v2 = new StringConstant(val2);
  1032.                     result = sym_v2._subString(sym_v1);
  1033.                 } else {
  1034.                     result = sym_v2._subString(sym_v1);
  1035.                 }
  1036.             }
  1037.             ElementInfo objRef = th.getHeap().newString("", th); /*
  1038.                                                                                                                                      * dummy
  1039.                                                                                                                                      * String
  1040.                                                                                                                                      * Object
  1041.                                                                                                                                      */
  1042.             sf.push(objRef.getObjectRef(), true);
  1043.             sf.setOperandAttr(result);
  1044.         }
  1045.         return null;
  1046.     }
  1047.  
  1048.     public Instruction handleSubString2(JVMInvokeInstruction invInst, ThreadInfo th) {
  1049.         //System.out.println("[SymbolicStringHandler] doing");
  1050.         StackFrame sf = th.getModifiableTopFrame();
  1051.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  1052.         IntegerExpression sym_v2 = (IntegerExpression) sf.getOperandAttr(1);
  1053.         StringExpression sym_v3 = (StringExpression) sf.getOperandAttr(2);
  1054.  
  1055.         if ((sym_v1 == null) & (sym_v2 == null) & (sym_v3 == null)) {
  1056.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleSubString2");
  1057.         } else {
  1058.             int s1 = sf.pop();
  1059.             int s2 = sf.pop();
  1060.             int s3 = sf.pop();
  1061.             //System.out.printf("[SymbolicStringHandler] popped %d %d %d\n", s1, s2, s3);
  1062.             StringExpression result = null;
  1063.             if (sym_v1 == null) { // operand 0 is concrete
  1064.                 int val = s1;
  1065.                 if (sym_v2 == null) { // sym_v3 has to be symbolic
  1066.                     int val1 = s2;
  1067.                     result = sym_v3._subString(val, val1);
  1068.                     //System.out.println("[SymbolicStringHandler] special push");
  1069.                     /* Only if both arguments are concrete, something else needs
  1070.                      * to be pushed?
  1071.                      */
  1072.                     //sf.push(s3, true); /* symbolic string element */
  1073.                 } else {
  1074.                     if (sym_v3 == null) { // only sym_v2 is symbolic
  1075.                         ElementInfo e3 = th.getElementInfo(s3);
  1076.                         String val2 = e3.asString();
  1077.                         sym_v3 = new StringConstant(val2);
  1078.                         result = sym_v3._subString(val, sym_v2);
  1079.                     } else {
  1080.                         result = sym_v3._subString(val, sym_v2);
  1081.                     }
  1082.                 }
  1083.             } else { // sym_v1 is symbolic
  1084.                 if (sym_v2 == null) {
  1085.                     if (sym_v3 == null) {
  1086.                         int val1 = s2;
  1087.                         ElementInfo e3 = th.getElementInfo(s3);
  1088.                         String val2 = e3.asString();
  1089.                         sym_v3 = new StringConstant(val2);
  1090.                         result = sym_v3._subString(sym_v1, val1);
  1091.                     } else {
  1092.                         int val1 = s2;
  1093.                         result = sym_v3._subString(sym_v1, val1);
  1094.                     }
  1095.                 } else {
  1096.                     if (sym_v3 == null) {
  1097.                         ElementInfo e3 = th.getElementInfo(s3);
  1098.                         String val2 = e3.asString();
  1099.                         sym_v3 = new StringConstant(val2);
  1100.                         result = sym_v3._subString(sym_v1, sym_v2);
  1101.                     } else {
  1102.                         result = sym_v3._subString(sym_v1, sym_v2);
  1103.                     }
  1104.                 }
  1105.             }
  1106.             ElementInfo objRef = th.getHeap().newString("", th);
  1107.             //System.out.println("[SymbolicStringHandler] " + sf.toString());
  1108.             sf.push(objRef.getObjectRef(), true);
  1109.             //System.out.println("[SymbolicStringHandler] " + sf.toString());
  1110.             sf.setOperandAttr(result);
  1111.         }
  1112.  
  1113.         return null;
  1114.     }
  1115.  
  1116.     public Instruction handleReplaceFirst(JVMInvokeInstruction invInst, ThreadInfo th) {
  1117.         StackFrame sf = th.getModifiableTopFrame();
  1118.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  1119.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  1120.         StringExpression sym_v3 = (StringExpression) sf.getOperandAttr(2);
  1121.  
  1122.         if ((sym_v1 == null) & (sym_v2 == null) & (sym_v3 == null)) {
  1123.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HanldeReplaceFirst");
  1124.         } else {
  1125.             int s1 = sf.pop();
  1126.             int s2 = sf.pop();
  1127.             int s3 = sf.pop();
  1128.  
  1129.             StringExpression result = null;
  1130.             if (sym_v1 == null) { // operand 0 is concrete
  1131.                 ElementInfo e1 = th.getElementInfo(s1);
  1132.                 String val = e1.asString();
  1133.                 if (sym_v2 == null) { // sym_v3 has to be symbolic
  1134.                     ElementInfo e2 = th.getElementInfo(s2);
  1135.                     String val1 = e2.asString();
  1136.                     result = sym_v3._replaceFirst(val, val1);
  1137.  
  1138.                 } else {
  1139.                     if (sym_v3 == null) { // only sym_v2 is symbolic
  1140.                         ElementInfo e3 = th.getElementInfo(s3);
  1141.                         String val2 = e3.asString();
  1142.                         sym_v3 = new StringConstant(val2);
  1143.                         result = sym_v3._replaceFirst(val, sym_v2);
  1144.                     } else {
  1145.                         result = sym_v3._replaceFirst(val, sym_v2);
  1146.                     }
  1147.                 }
  1148.             } else { // sym_v1 is symbolic
  1149.                 if (sym_v2 == null) {
  1150.                     if (sym_v3 == null) {
  1151.                         ElementInfo e2 = th.getElementInfo(s2);
  1152.                         String val1 = e2.asString();
  1153.                         ElementInfo e3 = th.getElementInfo(s3);
  1154.                         String val2 = e3.asString();
  1155.                         sym_v3 = new StringConstant(val2);
  1156.                         result = sym_v3._replaceFirst(sym_v1, val1);
  1157.                     } else {
  1158.                         ElementInfo e2 = th.getElementInfo(s2);
  1159.                         String val1 = e2.asString();
  1160.                         result = sym_v3._replaceFirst(sym_v1, val1);
  1161.                     }
  1162.                 } else {
  1163.                     if (sym_v3 == null) {
  1164.                         ElementInfo e3 = th.getElementInfo(s3);
  1165.                         String val2 = e3.asString();
  1166.                         sym_v3 = new StringConstant(val2);
  1167.                         result = sym_v3._replaceFirst(sym_v1, sym_v2);
  1168.                     } else {
  1169.                         result = sym_v3._replaceFirst(sym_v1, sym_v2);
  1170.                     }
  1171.                 }
  1172.             }
  1173.             ElementInfo objRef = th.getHeap().newString("", th); /*
  1174.                                                                                                                                      * dummy
  1175.                                                                                                                                      * String
  1176.                                                                                                                                      * Object
  1177.                                                                                                                                      */
  1178.             sf.push(objRef.getObjectRef(), true);
  1179.             sf.setOperandAttr(result);
  1180.         }
  1181.         return null;
  1182.     }
  1183.  
  1184.     public void handleTrim(JVMInvokeInstruction invInst, ThreadInfo th) {
  1185.         // throw new RuntimeException("ERROR: symbolic string method not Implemented - Trim");
  1186.         StackFrame sf = th.getModifiableTopFrame();
  1187.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  1188.         int s1 = sf.pop();
  1189.  
  1190.         if (sym_v1 == null) {
  1191.             ElementInfo e1 = th.getElementInfo(s1);
  1192.             String val1 = e1.asString();
  1193.             sym_v1 = new StringConstant(val1);
  1194.         }
  1195.         StringExpression result = sym_v1._trim();
  1196.  
  1197.         ElementInfo  objRef = th.getHeap().newString("", th); /*
  1198.                                                                                                                                  * dummy String
  1199.                                                                                                                                  * Object
  1200.                                                                                                                                  */
  1201.         sf.push(objRef.getObjectRef(), true);
  1202.         sf.setOperandAttr(result);
  1203.     }
  1204.  
  1205.     public Instruction handleValueOf(JVMInvokeInstruction invInst,  ThreadInfo th) {
  1206.         MethodInfo mi = invInst.getInvokedMethod(th);
  1207.         String cname = invInst.getInvokedMethodClassName();
  1208.         String[] argTypes = mi.getArgumentTypeNames();
  1209.         if (cname.equals("java.lang.String")) {
  1210.             // System.out.println(argTypes[0]);
  1211.             if (argTypes[0].equals("int")) {
  1212.                 return handleIntValueOf(invInst,  th);
  1213.             } else if (argTypes[0].equals("float")) {
  1214.                 return handleFloatValueOf(invInst, th);
  1215.             } else if (argTypes[0].equals("long")) {
  1216.                 return handleLongValueOf(invInst, th);
  1217.             } else if (argTypes[0].equals("double")) {
  1218.                 return handleDoubleValueOf(invInst, th);
  1219.             } else if (argTypes[0].equals("char")) {
  1220.                 return handleCharValueOf(invInst, th);
  1221.             } else if (argTypes[0].equals("chararray")) {
  1222.                 return handleCharArrayValueOf(invInst, th);
  1223.             } else if (argTypes[0].equals("boolean")) {
  1224.                 return handleBooleanValueOf(invInst, th);
  1225.             } else if (argTypes[0].equals("java.lang.Object")) {
  1226.                 return handleObjectValueOf(invInst, th);
  1227.             } else {
  1228.                 throw new RuntimeException("ERROR: Input parameter type not handled in Symbolic String ValueOf");
  1229.             }
  1230.         } else { // value of non-string types
  1231.             if (cname.equals("java.lang.Integer")) {
  1232.                 if (!(argTypes[0].equals("int"))) { // converting String to Integer
  1233.                     ChoiceGenerator<?> cg;
  1234.                     if (!th.isFirstStepInsn()) { // first time around
  1235.                         cg = new PCChoiceGenerator(2);
  1236.                         th.getVM().setNextChoiceGenerator(cg);
  1237.                         return invInst;
  1238.                     } else {
  1239.                         handleParseIntValueOf(invInst, th);
  1240.                     }
  1241.                 } else { // converting int to Integer
  1242.                     handleParseIntValueOf(invInst,  th);
  1243.                 }
  1244.             } else if (cname.equals("java.lang.Float")) {
  1245.                 if (!(argTypes[0].equals("float"))) { // converting String to Float
  1246.                     ChoiceGenerator<?> cg;
  1247.                     if (!th.isFirstStepInsn()) { // first time around
  1248.                         cg = new PCChoiceGenerator(2);
  1249.                         th.getVM().setNextChoiceGenerator(cg);
  1250.                         return invInst;
  1251.                     } else {
  1252.                         handleParseFloatValueOf(invInst, th);
  1253.                     }
  1254.                 } else { // converting int to Integer
  1255.                     handleParseFloatValueOf(invInst, th);
  1256.                 }
  1257.             } else if (cname.equals("java.lang.Long")) {
  1258.                 if (!(argTypes[0].equals("long"))) { // converting String to Long
  1259.                     ChoiceGenerator<?> cg;
  1260.                     if (!th.isFirstStepInsn()) { // first time around
  1261.                         cg = new PCChoiceGenerator(2);
  1262.                         th.getVM().setNextChoiceGenerator(cg);
  1263.                         return invInst;
  1264.                     } else {
  1265.                         handleParseLongValueOf(invInst, th);
  1266.                     }
  1267.                 } else { // converting int to Integer
  1268.                     handleParseLongValueOf(invInst, th);
  1269.                 }
  1270.             } else if (cname.equals("java.lang.Double")) {
  1271.                 if (!(argTypes[0].equals("double"))) { // converting String to Double
  1272.                     ChoiceGenerator<?> cg;
  1273.                     if (!th.isFirstStepInsn()) { // first time around
  1274.                         cg = new PCChoiceGenerator(2);
  1275.                         th.getVM().getSystemState().setNextChoiceGenerator(cg);
  1276.                         return invInst;
  1277.                     } else {
  1278.                         handleParseDoubleValueOf(invInst, th);
  1279.                     }
  1280.                 } else { // converting int to Integer
  1281.                     handleParseLongValueOf(invInst, th);
  1282.                 }
  1283.             } else if (cname.equals("java.lang.Boolean")) {
  1284.                 if (!(argTypes[0].equals("boolean"))) { // converting String to Boolean
  1285.                     ChoiceGenerator<?> cg;
  1286.                     if (!th.isFirstStepInsn()) { // first time around
  1287.                         cg = new PCChoiceGenerator(2);
  1288.                         th.getVM().setNextChoiceGenerator(cg);
  1289.                         return invInst;
  1290.                     } else {
  1291.                         handleParseBooleanValueOf(invInst, th);
  1292.                     }
  1293.                 } else { // converting int to Integer
  1294.                     handleParseBooleanValueOf(invInst, th);
  1295.                 }
  1296.             } else {
  1297.                 throw new RuntimeException("ERROR: Type not handled in Symbolic Type ValueOf: " + cname);
  1298.             }
  1299.         }
  1300.         return null;
  1301.     }
  1302.     public void handleIsEmpty(JVMInvokeInstruction invInst,  ThreadInfo th) {
  1303.         StackFrame sf = th.getModifiableTopFrame();
  1304.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  1305.         if (sym_v1 == null) {
  1306.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleIsEmpty");
  1307.         } else {
  1308.             IntegerExpression sym_v2 = sym_v1._length();
  1309.             ChoiceGenerator<?> cg;
  1310.             boolean conditionValue;
  1311.             cg = th.getVM().getChoiceGenerator();
  1312.  
  1313.             assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1314.             conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1315.  
  1316.             sf.pop();
  1317.             PathCondition pc;
  1318.  
  1319.             ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1320.             while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1321.                 prev_cg = prev_cg.getPreviousChoiceGenerator();
  1322.             }
  1323.  
  1324.             if (prev_cg == null) {
  1325.                 pc = new PathCondition();
  1326.             } else {
  1327.                 pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1328.             }
  1329.  
  1330.             assert pc != null;
  1331.  
  1332.             if(conditionValue){
  1333.                 pc._addDet(Comparator.EQ, sym_v2, (IntegerExpression)(new IntegerConstant(0)));
  1334.                 if(!pc.simplify()) {
  1335.                     th.getVM().getSystemState().setIgnored(true);
  1336.                 } else {
  1337.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1338.                 }
  1339.             }else{
  1340.                 pc._addDet(Comparator.NE, sym_v2, (IntegerExpression)(new IntegerConstant(0)));
  1341.                 if(!pc.simplify()) {
  1342.                     th.getVM().getSystemState().setIgnored(true);
  1343.                 } else {
  1344.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1345.                 }
  1346.             }
  1347.  
  1348.             sf.push(conditionValue ? 1 : 0, true);
  1349.         }
  1350.     }
  1351.  
  1352.     public void handleParseLongValueOf(JVMInvokeInstruction invInst,  ThreadInfo th) {
  1353.         StackFrame sf = th.getModifiableTopFrame();
  1354.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  1355.  
  1356.         if (sym_v3 == null) {
  1357.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  1358.         } else {
  1359.             if (sym_v3 instanceof IntegerExpression) {
  1360.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  1361.                 sf.popLong();
  1362.                 int objRef = getNewObjRef(invInst, th); /* dummy Long Object */
  1363.                 sf.push(objRef, true);
  1364.                 sf.setOperandAttr(sym_v2);
  1365.             } else {
  1366.                 IntegerExpression result = null;
  1367.                 ChoiceGenerator<?> cg;
  1368.                 boolean conditionValue;
  1369.                 cg = th.getVM().getChoiceGenerator();
  1370.  
  1371.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1372.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1373.  
  1374.                 sf.pop();
  1375.                 PathCondition pc;
  1376.  
  1377.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1378.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1379.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  1380.                 }
  1381.  
  1382.                 if (prev_cg == null)
  1383.                     pc = new PathCondition();
  1384.                 else
  1385.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1386.  
  1387.                 assert pc != null;
  1388.  
  1389.                 if (conditionValue) {
  1390.                     pc.spc._addDet(StringComparator.ISLONG, (StringExpression) sym_v3);
  1391.                     if (!pc.simplify()) {// not satisfiable
  1392.                         th.getVM().getSystemState().setIgnored(true);
  1393.                     } else {
  1394.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1395.                         result = ((StringExpression) sym_v3)._IvalueOf();
  1396.                         sf = th.getModifiableTopFrame();
  1397.                         int objRef = getNewObjRef(invInst, th); /* dummy Long Object */
  1398.                         sf.push(objRef, true);
  1399.                         sf.setOperandAttr(result);
  1400.                     }
  1401.                 } else {
  1402.                     pc.spc._addDet(StringComparator.NOTLONG, (StringExpression) sym_v3);
  1403.                     if (!pc.simplify()) {// not satisfiable
  1404.                         th.getVM().getSystemState().setIgnored(true);
  1405.                     } else {
  1406.                         throw new RuntimeException("ERROR: Long Format Type Exception");
  1407.                         //th.getVM().getSystemState().setIgnored(true); TODO: needs revision
  1408.                         //sf.push(0, true);
  1409.                     }
  1410.                 }
  1411.             }
  1412.         }
  1413.     }
  1414.  
  1415.     public void handleParseBooleanValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  1416.         StackFrame sf = th.getModifiableTopFrame();
  1417.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  1418.  
  1419.         if (sym_v3 == null) {
  1420.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  1421.         } else {
  1422.             if (sym_v3 instanceof IntegerExpression) {
  1423.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  1424.                 sf.pop();
  1425.                 int objRef = getNewObjRef(invInst, th); /* dummy Boolean Object */
  1426.                 sf.push(objRef, true);
  1427.                 sf.setOperandAttr(sym_v2);
  1428.             } else {
  1429.                 IntegerExpression result = null;
  1430.                 ChoiceGenerator<?> cg;
  1431.                 boolean conditionValue;
  1432.                 cg = th.getVM().getChoiceGenerator();
  1433.  
  1434.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1435.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1436.  
  1437.                 sf.pop();
  1438.                 PathCondition pc;
  1439.  
  1440.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1441.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1442.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  1443.                 }
  1444.  
  1445.                 if (prev_cg == null)
  1446.                     pc = new PathCondition();
  1447.                 else
  1448.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1449.  
  1450.                 assert pc != null;
  1451.  
  1452.                 if (conditionValue) {
  1453.                     pc.spc._addDet(StringComparator.ISBOOLEAN, (StringExpression) sym_v3);
  1454.                     if (!pc.simplify()) {// not satisfiable
  1455.                         th.getVM().getSystemState().setIgnored(true);
  1456.                     } else {
  1457.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1458.                         result = ((StringExpression) sym_v3)._IvalueOf();
  1459.                         sf = th.getModifiableTopFrame();
  1460.                         int objRef = getNewObjRef(invInst, th); /* dummy Boolean Object */
  1461.                         sf.push(objRef, true);
  1462.                         sf.setOperandAttr(result);
  1463.                     }
  1464.                 } else {
  1465.                     pc.spc._addDet(StringComparator.NOTBOOLEAN, (StringExpression) sym_v3);
  1466.                     if (!pc.simplify()) {// not satisfiable
  1467.                         th.getVM().getSystemState().setIgnored(true);
  1468.                     } else {
  1469.                         throw new RuntimeException("ERROR: Boolean Format Type Exception");
  1470.                         // TODO: to review; there should be no backtracking here
  1471.                         //th.getVM().getSystemState().setIgnored(true);
  1472.                         //sf.push(0, true);
  1473.                     }
  1474.                 }
  1475.             }
  1476.         }
  1477.     }
  1478.  
  1479.     public void handleParseIntValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  1480.         StackFrame sf = th.getModifiableTopFrame();
  1481.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  1482.  
  1483.         if (sym_v3 == null) {
  1484.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  1485.         } else {
  1486.             if (sym_v3 instanceof IntegerExpression) {
  1487.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  1488.                 sf.pop();
  1489.                 int objRef = getNewObjRef(invInst, th); /* dummy Integer Object */
  1490.                 sf.push(objRef, true);
  1491.                 sf.setOperandAttr(sym_v2);
  1492.             } else {
  1493.                 IntegerExpression result = null;
  1494.                 ChoiceGenerator<?> cg;
  1495.                 boolean conditionValue;
  1496.                 cg = th.getVM().getChoiceGenerator();
  1497.  
  1498.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1499.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1500.  
  1501.                 sf.pop();
  1502.                 PathCondition pc;
  1503.  
  1504.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1505.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1506.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  1507.                 }
  1508.  
  1509.                 if (prev_cg == null)
  1510.                     pc = new PathCondition();
  1511.                 else
  1512.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1513.  
  1514.                 assert pc != null;
  1515.  
  1516.                 if (conditionValue) {
  1517.                     pc.spc._addDet(StringComparator.ISINTEGER, (StringExpression) sym_v3);
  1518.                     if (!pc.simplify()) {// not satisfiable
  1519.                         th.getVM().getSystemState().setIgnored(true);
  1520.                     } else {
  1521.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1522.                         result = ((StringExpression) sym_v3)._IvalueOf();
  1523.                         sf = th.getModifiableTopFrame();
  1524.                         int objRef = getNewObjRef(invInst, th); /* dummy Integer Object */
  1525.                         sf.push(objRef, true);
  1526.                         sf.setOperandAttr(result);
  1527.                     }
  1528.                 } else {
  1529.                     pc.spc._addDet(StringComparator.NOTINTEGER, (StringExpression) sym_v3);
  1530.                     if (!pc.simplify()) {// not satisfiable
  1531.                         th.getVM().getSystemState().setIgnored(true);
  1532.                     } else {
  1533.                         throw new RuntimeException("ERROR: Integer Format Type Exception");
  1534.                         //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  1535.                         //sf.push(0, true);
  1536.                     }
  1537.                 }
  1538.             }
  1539.         }
  1540.     }
  1541.  
  1542.     public void handleParseInt(JVMInvokeInstruction invInst, ThreadInfo th) {
  1543.         StackFrame sf = th.getModifiableTopFrame();
  1544.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  1545.  
  1546.         if (sym_v3 == null) {
  1547.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  1548.         } else {
  1549.             IntegerExpression result = null;
  1550.             ChoiceGenerator<?> cg;
  1551.             boolean conditionValue;
  1552.             cg = th.getVM().getChoiceGenerator();
  1553.  
  1554.             assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1555.             conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1556.  
  1557.             sf.pop();
  1558.             PathCondition pc;
  1559.             ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1560.             while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1561.                 prev_cg = prev_cg.getPreviousChoiceGenerator();
  1562.             }
  1563.  
  1564.             if (prev_cg == null)
  1565.                 pc = new PathCondition();
  1566.             else
  1567.                 pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1568.  
  1569.             assert pc != null;
  1570.  
  1571.             if (conditionValue) {
  1572.                 pc.spc._addDet(StringComparator.ISINTEGER, (StringExpression) sym_v3);
  1573.                 if (!pc.simplify()) {// not satisfiable
  1574.                     th.getVM().getSystemState().setIgnored(true);
  1575.                 } else {
  1576.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1577.                     result = ((StringExpression) sym_v3)._IvalueOf();
  1578.                     sf.push(0, false); /* Result is don't care and an int */
  1579.                     sf = th.getModifiableTopFrame();
  1580.                     sf.setOperandAttr(result);
  1581.                 }
  1582.             } else {
  1583.                 pc.spc._addDet(StringComparator.NOTINTEGER, (StringExpression) sym_v3);
  1584.                 if (!pc.simplify()) {// not satisfiable
  1585.                     th.getVM().getSystemState().setIgnored(true);
  1586.                 } else {
  1587.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1588.                     th.createAndThrowException("java.lang.NumberFormatException");
  1589. //                  throw new RuntimeException("ERROR: Integer Format Type Exception");
  1590. //                  //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  1591. //                  //sf.push(0, true);
  1592.                 }
  1593.             }
  1594.         }
  1595.  
  1596.     }
  1597.  
  1598.     public void handleParseFloat(JVMInvokeInstruction invInst, ThreadInfo th) {
  1599.         StackFrame sf = th.getModifiableTopFrame();
  1600.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  1601.  
  1602.         if (sym_v3 == null) {
  1603.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  1604.         } else {
  1605.             RealExpression result = null;
  1606.             ChoiceGenerator<?> cg;
  1607.             boolean conditionValue;
  1608.             cg = th.getVM().getChoiceGenerator();
  1609.  
  1610.             assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1611.             conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1612.  
  1613.             sf.pop();
  1614.             PathCondition pc;
  1615.             ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1616.             while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1617.                 prev_cg = prev_cg.getPreviousChoiceGenerator();
  1618.             }
  1619.  
  1620.             if (prev_cg == null)
  1621.                 pc = new PathCondition();
  1622.             else
  1623.                 pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1624.  
  1625.             assert pc != null;
  1626.             if (conditionValue) {
  1627.                 pc.spc._addDet(StringComparator.ISFLOAT, (StringExpression) sym_v3);
  1628.                 if (!pc.simplify()) {// not satisfiable
  1629.                     th.getVM().getSystemState().setIgnored(true);
  1630.                 } else {
  1631.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1632.                     result = ((StringExpression) sym_v3)._RvalueOf();
  1633.                     sf.push(0, false); /* Result is don't care and a float */
  1634.                     sf = th.getModifiableTopFrame();
  1635.                     sf.setOperandAttr(result);
  1636.                 }
  1637.             } else {
  1638.                 pc.spc._addDet(StringComparator.NOTFLOAT, (StringExpression) sym_v3);
  1639.                 if (!pc.simplify()) {// not satisfiable
  1640.                     th.getVM().getSystemState().setIgnored(true);
  1641.                 } else {
  1642.                     throw new RuntimeException("ERROR: Possible Float Format Type Exception - Path Terminated");
  1643.                    
  1644.                     //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  1645.                 }
  1646.             }
  1647.         }
  1648.  
  1649.     }
  1650.  
  1651.     public void handleParseFloatValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  1652.         StackFrame sf = th.getModifiableTopFrame();
  1653.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  1654.  
  1655.         if (sym_v3 == null) {
  1656.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  1657.         } else {
  1658.             if (sym_v3 instanceof RealExpression) {
  1659.                 RealExpression sym_v2 = (RealExpression) sym_v3;
  1660.                 sf.pop();
  1661.                 int objRef = getNewObjRef(invInst, th); /* dummy Float Object */
  1662.                 sf.push(objRef, true);
  1663.                 sf.setOperandAttr(sym_v2);
  1664.             } else {
  1665.                 RealExpression result = null;
  1666.                 ChoiceGenerator<?> cg;
  1667.                 boolean conditionValue;
  1668.                 cg = th.getVM().getChoiceGenerator();
  1669.  
  1670.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1671.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1672.  
  1673.                 sf.pop();
  1674.                 PathCondition pc;
  1675.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1676.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1677.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  1678.                 }
  1679.  
  1680.                 if (prev_cg == null)
  1681.                     pc = new PathCondition();
  1682.                 else
  1683.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1684.  
  1685.                 assert pc != null;
  1686.                 if (conditionValue) {
  1687.                     pc.spc._addDet(StringComparator.ISFLOAT, (StringExpression) sym_v3);
  1688.                     if (!pc.simplify()) {// not satisfiable
  1689.                         th.getVM().getSystemState().setIgnored(true);
  1690.                     } else {
  1691.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1692.                         result = ((StringExpression) sym_v3)._RvalueOf();
  1693.                         int objRef = getNewObjRef(invInst, th); /* dummy Float Object */
  1694.                         sf.push(objRef, true);
  1695.                         sf = th.getModifiableTopFrame();
  1696.                         sf.setOperandAttr(result);
  1697.                     }
  1698.                 } else {
  1699.                     pc.spc._addDet(StringComparator.NOTFLOAT, (StringExpression) sym_v3);
  1700.                     if (!pc.simplify()) {// not satisfiable
  1701.                         th.getVM().getSystemState().setIgnored(true);
  1702.                     } else {
  1703.                         throw new RuntimeException("ERROR: Possible Float Format Type Exception - Path Terminated");
  1704.                        
  1705.                         //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  1706.                     }
  1707.                 }
  1708.             }
  1709.         }
  1710.  
  1711.     }
  1712.  
  1713.     public void handleParseDoubleValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  1714.         StackFrame sf = th.getModifiableTopFrame();
  1715.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  1716.  
  1717.         if (sym_v3 == null) {
  1718.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  1719.         } else {
  1720.             if (sym_v3 instanceof RealExpression) {
  1721.                 RealExpression sym_v2 = (RealExpression) sym_v3;
  1722.                 sf.popLong();
  1723.                 int objRef = getNewObjRef(invInst, th); /* dummy Double Object */
  1724.                 sf.push(objRef, true);
  1725.                 sf.setOperandAttr(sym_v2);
  1726.             } else {
  1727.                 RealExpression result = null;
  1728.                 ChoiceGenerator<?> cg;
  1729.                 boolean conditionValue;
  1730.                 cg = th.getVM().getChoiceGenerator();
  1731.  
  1732.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1733.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1734.  
  1735.                 sf.pop();
  1736.                 PathCondition pc;
  1737.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1738.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1739.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  1740.                 }
  1741.  
  1742.                 if (prev_cg == null)
  1743.                     pc = new PathCondition();
  1744.                 else
  1745.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1746.  
  1747.                 assert pc != null;
  1748.  
  1749.                 if (conditionValue) {
  1750.                     pc.spc._addDet(StringComparator.ISDOUBLE, (StringExpression) sym_v3);
  1751.                     if (!pc.simplify()) {// not satisfiable
  1752.                         th.getVM().getSystemState().setIgnored(true);
  1753.                     } else {
  1754.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1755.                         result = ((StringExpression) sym_v3)._RvalueOf();
  1756.                         int objRef = getNewObjRef(invInst, th); /* dummy Double Object */
  1757.                         sf.push(objRef, true);
  1758.                         sf = th.getModifiableTopFrame();
  1759.                         sf.setOperandAttr(result);
  1760.                     }
  1761.                 } else {
  1762.                     pc.spc._addDet(StringComparator.NOTDOUBLE, (StringExpression) sym_v3);
  1763.                     if (!pc.simplify()) {// not satisfiable
  1764.                         th.getVM().getSystemState().setIgnored(true);
  1765.                     } else {
  1766.                         throw new RuntimeException("ERROR: Double Format Type Exception");
  1767.                         //th.getVM().getSystemState().setIgnored(true);
  1768.                         //sf.push(0, true); // TODO: to review
  1769.                     }
  1770.                 }
  1771.             }
  1772.         }
  1773.  
  1774.     }
  1775.  
  1776.     public void handleParseDouble(JVMInvokeInstruction invInst, ThreadInfo th) {
  1777.         StackFrame sf = th.getModifiableTopFrame();
  1778.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  1779.  
  1780.         if (sym_v3 == null) {
  1781.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  1782.         } else {
  1783.             if (sym_v3 instanceof RealExpression) {
  1784.                 return;
  1785.             } else {
  1786.                 StringExpression sym_v1 = (StringExpression) sym_v3;
  1787.                 ChoiceGenerator<?> cg;
  1788.                 boolean conditionValue;
  1789.                 cg = th.getVM().getChoiceGenerator();
  1790.  
  1791.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1792.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1793.                 sf.pop();
  1794.                 PathCondition pc;
  1795.  
  1796.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1797.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1798.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  1799.                 }
  1800.  
  1801.                 if (prev_cg == null)
  1802.                     pc = new PathCondition();
  1803.                 else
  1804.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1805.  
  1806.                 assert pc != null;
  1807.  
  1808.                 if (conditionValue) {
  1809.                     pc.spc._addDet(StringComparator.ISDOUBLE, sym_v1);
  1810.                     if (!pc.simplify()) {// not satisfiable
  1811.                         th.getVM().getSystemState().setIgnored(true);
  1812.                     } else {
  1813.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1814.                         RealExpression sym_v2 = new SpecialRealExpression(sym_v1);
  1815.                         sf.pushLong((long) 0); /* Result is don't care and 0 */
  1816.                         //sf = th.getModifiableTopFrame(); ??
  1817.                         sf.setLongOperandAttr(sym_v2);
  1818.                     }
  1819.                 } else {
  1820.                     pc.spc._addDet(StringComparator.NOTDOUBLE, sym_v1);
  1821.                     if (!pc.simplify()) {// not satisfiable
  1822.                         th.getVM().getSystemState().setIgnored(true);
  1823.                     } else {
  1824.                         throw new RuntimeException("ERROR: Double Format Type Exception");
  1825.                         //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  1826.                     }
  1827.                 }
  1828.             }
  1829.         }
  1830.     }
  1831.  
  1832.     public void handleParseLong(JVMInvokeInstruction invInst, ThreadInfo th) {
  1833.         StackFrame sf = th.getModifiableTopFrame();
  1834.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  1835.  
  1836.         if (sym_v3 == null) {
  1837.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  1838.         } else {
  1839.             if (sym_v3 instanceof IntegerExpression) {
  1840.                 return;
  1841.             } else {
  1842.                 StringExpression sym_v1 = (StringExpression) sym_v3;
  1843.                 ChoiceGenerator<?> cg;
  1844.                 boolean conditionValue;
  1845.                 cg = th.getVM().getChoiceGenerator();
  1846.  
  1847.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1848.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1849.                 sf.pop();
  1850.                 PathCondition pc;
  1851.  
  1852.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1853.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1854.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  1855.                 }
  1856.  
  1857.                 if (prev_cg == null)
  1858.                     pc = new PathCondition();
  1859.                 else
  1860.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1861.  
  1862.                 assert pc != null;
  1863.  
  1864.                 if (conditionValue) {
  1865.                     pc.spc._addDet(StringComparator.ISLONG, sym_v1);
  1866.                     if (!pc.simplify()) {// not satisfiable
  1867.                         th.getVM().getSystemState().setIgnored(true);
  1868.                     } else {
  1869.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1870.                         IntegerExpression sym_v2 = new SpecialIntegerExpression(sym_v1);
  1871.                         sf.pushLong((long) 0); /* result is don't care */
  1872.                         //sf = th.getModifiableTopFrame(); ??
  1873.                         sf.setLongOperandAttr(sym_v2);
  1874.                     }
  1875.                 } else {
  1876.                     pc.spc._addDet(StringComparator.NOTLONG, sym_v1);
  1877.                     if (!pc.simplify()) {// not satisfiable
  1878.                         th.getVM().getSystemState().setIgnored(true);
  1879.                     } else {
  1880.                         throw new RuntimeException("ERROR: Long Format Type Exception");
  1881.                         //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  1882.                     }
  1883.                 }
  1884.             }
  1885.         }
  1886.     }
  1887.  
  1888.     public void handleParseBoolean(JVMInvokeInstruction invInst, ThreadInfo th) {
  1889.         StackFrame sf = th.getModifiableTopFrame();
  1890.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  1891.  
  1892.         if (sym_v1 == null) {
  1893.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  1894.         } else {
  1895.             ChoiceGenerator<?> cg;
  1896.             boolean conditionValue;
  1897.             cg = th.getVM().getChoiceGenerator();
  1898.  
  1899.             assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  1900.             conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  1901.             sf.pop();
  1902.             PathCondition pc;
  1903.  
  1904.             ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  1905.             while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  1906.                 prev_cg = prev_cg.getPreviousChoiceGenerator();
  1907.             }
  1908.  
  1909.             if (prev_cg == null)
  1910.                 pc = new PathCondition();
  1911.             else
  1912.                 pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  1913.  
  1914.             assert pc != null;
  1915.  
  1916.             if (conditionValue) {
  1917.                 pc.spc._addDet(StringComparator.ISBOOLEAN, sym_v1);
  1918.                 if (!pc.simplify()) {// not satisfiable
  1919.                     th.getVM().getSystemState().setIgnored(true);
  1920.                 } else {
  1921.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  1922.                     IntegerExpression sym_v2 = new SpecialIntegerExpression(sym_v1);
  1923.                     sf.push(0, false); /* result is don't care and 0 */
  1924.                     sf = th.getModifiableTopFrame();
  1925.                     sf.setOperandAttr(sym_v2);
  1926.                 }
  1927.             } else {
  1928.                 pc.spc._addDet(StringComparator.NOTBOOLEAN, sym_v1);
  1929.                 if (!pc.simplify()) {// not satisfiable
  1930.                     th.getVM().getSystemState().setIgnored(true);
  1931.                 } else {
  1932.                     throw new RuntimeException("ERROR: Boolean Format Type Exception");
  1933.                     //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  1934.                 }
  1935.             }
  1936.         }
  1937.     }
  1938.  
  1939.     public int getNewObjRef(JVMInvokeInstruction invInst, ThreadInfo th) {
  1940.        
  1941.         //DynamicArea da = th.getVM().getDynamicArea();
  1942.         MethodInfo mi = invInst.getInvokedMethod();
  1943.         ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(mi.getReturnTypeName());
  1944.         ElementInfo objRef = th.getHeap().newObject(ci, th);
  1945.         return objRef.getObjectRef();
  1946.     }
  1947.  
  1948.     // works for BigDecimal
  1949.     public Instruction getBigDecimalValue(JVMInvokeInstruction invInst, ThreadInfo th) {
  1950.         MethodInfo mi = invInst.getInvokedMethod();
  1951.         ClassInfo ci = mi.getClassInfo();
  1952.         MethodInfo miInit = ci.getMethod("toString()V", false);
  1953.         if (miInit == null) {
  1954.             return null;
  1955.         }
  1956.         //Instruction initPC = miInit.execute(th);
  1957.         //return initPC;
  1958.         throw new RuntimeException("not handled; to review");
  1959.     }
  1960.  
  1961.     // works for String, StringBuilder, StringBuffer
  1962.     public Instruction init1NewStringObjRef(JVMInvokeInstruction invInst, ThreadInfo th) {
  1963.         MethodInfo mi = invInst.getInvokedMethod();
  1964.         ClassInfo ci = mi.getClassInfo();
  1965.         MethodInfo miInit = ci.getMethod("<init>()V", false);
  1966.         if (miInit == null) {
  1967.             return null;
  1968.         }
  1969.         //Instruction initPC = miInit.execute(th); // TODO: to review
  1970.         //return initPC;
  1971.         throw new RuntimeException("not handled; to review");
  1972.     }
  1973.  
  1974.     public Instruction handleIntValueOf(JVMInvokeInstruction invInst,  ThreadInfo th) {
  1975.         StackFrame sf = th.getModifiableTopFrame();
  1976.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  1977.  
  1978.         if (sym_v1 == null) {
  1979.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleIntValueOf");
  1980.         } else {
  1981.             sf.pop();
  1982.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  1983.             int objRef = th.getHeap().newString("", th).getObjectRef();
  1984.             /*
  1985.              * dummy
  1986.              * string
  1987.              * Object
  1988.              */
  1989.             sf.push(objRef, true);
  1990.             sf.setOperandAttr(sym_v2);
  1991.         }
  1992.         return null;
  1993.     }
  1994.  
  1995.     public Instruction handleFloatValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  1996.         StackFrame sf = th.getModifiableTopFrame();
  1997.         RealExpression sym_v1 = (RealExpression) sf.getOperandAttr(0);
  1998.  
  1999.         if (sym_v1 == null) {
  2000.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleFloatValueOf");
  2001.         } else {
  2002.             sf.pop();
  2003.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  2004.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  2005.                                                                                                                                      * dummy
  2006.                                                                                                                                      * string
  2007.                                                                                                                                      * Object
  2008.                                                                                                                                      */
  2009.             sf.push(objRef, true);
  2010.             sf.setOperandAttr(sym_v2);
  2011.         }
  2012.         return null;
  2013.     }
  2014.  
  2015.     public Instruction handleLongValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  2016.         StackFrame sf = th.getModifiableTopFrame();
  2017.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  2018.  
  2019.         if (sym_v1 == null) {
  2020.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleLongValueOf");
  2021.         } else {
  2022.             sf.popLong();
  2023.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  2024.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  2025.                                                                                                                                      * dummy
  2026.                                                                                                                                      * string
  2027.                                                                                                                                      * Object
  2028.                                                                                                                                      */
  2029.             sf.push(objRef, true);
  2030.             sf.setOperandAttr(sym_v2);
  2031.         }
  2032.         return null;
  2033.     }
  2034.  
  2035.     public Instruction handleDoubleValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  2036.         StackFrame sf = th.getModifiableTopFrame();
  2037.         RealExpression sym_v1 = (RealExpression) sf.getOperandAttr(0);
  2038.  
  2039.         if (sym_v1 == null) {
  2040.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleDoubleValueOf");
  2041.         } else {
  2042.             sf.popLong();
  2043.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  2044.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  2045.                                                                                                                                      * dummy
  2046.                                                                                                                                      * string
  2047.                                                                                                                                      * Object
  2048.                                                                                                                                      */
  2049.             sf.push(objRef, true);
  2050.             sf.setOperandAttr(sym_v2);
  2051.         }
  2052.         return null;
  2053.     }
  2054.  
  2055.     public Instruction handleBooleanValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  2056.         StackFrame sf = th.getModifiableTopFrame();
  2057.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  2058.  
  2059.         if (sym_v1 == null) {
  2060.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleBooleanValueOf");
  2061.         } else {
  2062.             sf.pop();
  2063.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  2064.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  2065.                                                                                                                                      * dummy
  2066.                                                                                                                                      * string
  2067.                                                                                                                                      * Object
  2068.                                                                                                                                      */
  2069.             sf.push(objRef, true);
  2070.             sf.setOperandAttr(sym_v2);
  2071.         }
  2072.         return null;
  2073.     }
  2074.  
  2075.     public Instruction handleCharValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  2076.         //throw new RuntimeException("ERROR: symbolic string method not Implemented - CharValueOf");
  2077.         StackFrame sf = th.getModifiableTopFrame();
  2078.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  2079.  
  2080.         if (sym_v1 == null) {
  2081.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleIntValueOf");
  2082.         } else {
  2083.             sf.pop();
  2084.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  2085.             int objRef = th.getHeap().newString("", th).getObjectRef();
  2086.             sf.push(objRef, true);
  2087.             sf.setOperandAttr(sym_v2);
  2088.         }
  2089.  
  2090.         return null;
  2091.     }
  2092.  
  2093.     public Instruction handleCharArrayValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  2094.         throw new RuntimeException("ERROR: symbolic string method not Implemented - CharArrayValueof");
  2095.     }
  2096.  
  2097.     public Instruction handleObjectValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  2098.         StackFrame sf = th.getModifiableTopFrame();
  2099.         Expression sym_v1 = (Expression) sf.getOperandAttr(0);
  2100.         if (sym_v1 instanceof SymbolicStringBuilder) {
  2101.             sf.pop();
  2102.             SymbolicStringBuilder sym_v3 = (SymbolicStringBuilder) sym_v1;
  2103.             StringExpression sym_v2 = StringExpression._valueOf((StringExpression) sym_v3.getstr());
  2104.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  2105.                                                                                                                                      * dummy
  2106.                                                                                                                                      * String
  2107.                                                                                                                                      * Object
  2108.                                                                                                                                      */
  2109.             sf.push(objRef, true);
  2110.             sf.setOperandAttr(sym_v2);
  2111.         } else if (sym_v1 instanceof StringExpression) {
  2112.             sf.pop();
  2113.             StringExpression sym_v2 = StringExpression._valueOf((StringExpression) sym_v1);
  2114.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  2115.                                                                                                                                      * dummy
  2116.                                                                                                                                      * String
  2117.                                                                                                                                      * Object
  2118.                                                                                                                                      */
  2119.             sf.push(objRef, true);
  2120.             sf.setOperandAttr(sym_v2);
  2121.         } else {
  2122.             throw new RuntimeException("ERROR: symbolic string method not Implemented - ObjectValueof");
  2123.         }
  2124.         return null;
  2125.     }
  2126.  
  2127.     public Instruction handleConcat(JVMInvokeInstruction invInst, ThreadInfo th) {
  2128.         StackFrame sf = th.getModifiableTopFrame();
  2129.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  2130.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  2131.  
  2132.         if ((sym_v1 == null) & (sym_v2 == null)) {
  2133.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleConcat");
  2134.         } else {
  2135.             int s1 = sf.pop();
  2136.             int s2 = sf.pop();
  2137.  
  2138.             StringExpression result = null;
  2139.             if (sym_v1 == null) { // operand 0 is concrete
  2140.                 ElementInfo e1 = th.getElementInfo(s1);
  2141.                 String val = e1.asString();
  2142.                 result = sym_v2._concat(val);
  2143.             } else if (sym_v2 == null) { // operand 1 is concrete
  2144.                 ElementInfo e2 = th.getElementInfo(s2);
  2145.                 String val = e2.asString();
  2146.                 sym_v2 = new StringConstant(val);
  2147.                 result = sym_v2._concat(sym_v1);
  2148.             } else { // both operands are symbolic
  2149.                 result = sym_v2._concat(sym_v1);
  2150.             }
  2151.             int objRef = th.getHeap().newString("", th).getObjectRef();
  2152.             /*
  2153.             * dummy
  2154.             * String
  2155.             * Object
  2156.             */
  2157.             sf.push(objRef, true);
  2158.             sf.setOperandAttr(result);
  2159.         }
  2160.         return null;
  2161.     }
  2162.  
  2163.     public void handleObjectEquals(JVMInvokeInstruction invInst,  ThreadInfo th) {
  2164.         StackFrame sf = th.getModifiableTopFrame();
  2165.         Expression sym_v1 = (Expression) sf.getOperandAttr(0);
  2166.         Expression sym_v2 = (Expression) sf.getOperandAttr(1);
  2167.  
  2168.         if (sym_v1 != null) {
  2169.             // System.out.println("*" + sym_v1.toString());
  2170.             if (!(sym_v1 instanceof StringExpression)) {
  2171.                 throw new RuntimeException("ERROR: expressiontype not handled: ObjectEquals");
  2172.             }
  2173.         }
  2174.  
  2175.         if (sym_v2 != null) {
  2176.             // System.out.println("***" + sym_v2.toString());
  2177.             if (!(sym_v2 instanceof StringExpression)) {
  2178.                 throw new RuntimeException("ERROR: expressiontype not handled: ObjectEquals");
  2179.             }
  2180.         }
  2181.  
  2182.         handleEquals(invInst, th);
  2183.     }
  2184.  
  2185.     public void handleEquals(JVMInvokeInstruction invInst,  ThreadInfo th) {
  2186.         handleBooleanStringInstructions(invInst,  th, StringComparator.EQUALS);
  2187.        
  2188.     }
  2189.  
  2190.     public Instruction handleAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2191.         Instruction handled = null;
  2192.        
  2193.         MethodInfo mi = invInst.getInvokedMethod(th);
  2194.         String[] argTypes = mi.getArgumentTypeNames();
  2195.         // System.out.println(argTypes[0]);
  2196.        
  2197.         boolean isCharSequence = false;
  2198.         //check what is the concrete type of the charsequence
  2199.         if(argTypes[0].equals("java.lang.CharSequence")) {
  2200.             isCharSequence = true;
  2201.             StackFrame sf = th.getModifiableTopFrame();
  2202.             int firstParamIndex = mi.isStatic() ? 0 : 1;
  2203.             Object firstParam = sf.getArgumentAttrs(mi)[firstParamIndex];
  2204.             if(firstParam instanceof StringExpression || firstParam == null /*possibly an string constant*/) {
  2205.                 argTypes[0] = "java.lang.String";
  2206.             } else if (firstParam instanceof SymbolicStringBuilder) {
  2207.                 //TODO and if it is a StringBuffer?
  2208.                 argTypes[0] = "java.lang.StringBuilder";
  2209.             } else {
  2210.                 throw new RuntimeException("Unhandled CharSequence at Symbolic String Append; concrete type is:" + firstParam.getClass());
  2211.             }
  2212.         }
  2213.         if (isCharSequence && argTypes.length == 3) { //append(charSequence,int,int)
  2214.             if(argTypes[0].equals("java.lang.String")) {
  2215.                 handled = handleStringAppend3(invInst, th);
  2216.             } else { //stringbuilder
  2217.                 handled = handleStringBuilderAppend3(invInst, th);
  2218.             }
  2219.         } else if (argTypes[0].equals("java.lang.String")) {
  2220.             handleStringAppend(invInst, th);
  2221.         } else if ((argTypes[0].equals("java.lang.StringBuilder")) || (argTypes[0].equals("java.lang.StringBuffer"))) {
  2222.             handleStringBuilderAppend(invInst, th);
  2223.         } else if (argTypes[0].equals("int")) {
  2224.             handleIntAppend(invInst, th);
  2225.         } else if (argTypes[0].equals("char")) {
  2226.             handleCharAppend(invInst, th);
  2227.         } else if (argTypes[0].equals("byte")) {
  2228.             handleByteAppend(invInst, th);
  2229.         } else if (argTypes[0].equals("short")) {
  2230.             handleShortAppend(invInst, th);
  2231.         } else if (argTypes[0].equals("float")) {
  2232.             handleFloatAppend(invInst, th);
  2233.         } else if (argTypes[0].equals("long")) {
  2234.             handleLongAppend(invInst, th);
  2235.         } else if (argTypes[0].equals("double")) {
  2236.             handleDoubleAppend(invInst, th);
  2237.         } else if (argTypes[0].equals("boolean")) {
  2238.             handleBooleanAppend(invInst, th);
  2239.         } else if (argTypes[0].equals("java.lang.Object")) {
  2240.             handleObjectAppend(invInst, th);
  2241.         } else {
  2242.             throw new RuntimeException("ERROR: Input parameter type not handled in Symbolic String Append");
  2243.         }
  2244.  
  2245.         return handled;
  2246.     }
  2247.  
  2248.     public void handleStringAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2249.         StackFrame sf = th.getModifiableTopFrame();
  2250.         // int objRef = sf.getThis();
  2251.         // ElementInfo ei = th.getElementInfo(objRef);
  2252.  
  2253.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  2254.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  2255.  
  2256.         if (sym_v2 == null)
  2257.             sym_v2 = new SymbolicStringBuilder();
  2258.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  2259.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleStringAppend");
  2260.         } else {
  2261.             int s1 = sf.pop();
  2262.             int s2 = sf.pop();
  2263.  
  2264.             if (sym_v1 == null) { // operand 0 is concrete
  2265.                 ElementInfo e1 = th.getElementInfo(s1);
  2266.                 String val = e1.asString();
  2267.                 sym_v2._append(val);
  2268.                 sf.push(s2, true); /* symbolic string Builder element */
  2269.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2270.                 // from String builder object
  2271.                 ElementInfo e1 = th.getElementInfo(s2);
  2272.                 String val = getStringEquiv(e1);
  2273.                 sym_v2.putstr(new StringConstant(val));
  2274.                 sym_v2._append(sym_v1);
  2275.                 // setVariableAttribute(ei, invInst, th, sf, s2, sym_v2); //set the
  2276.                 // value of the attribute of local StringBuilder element as sym_v2
  2277.                 sf.push(s2, true); /* symbolic string Builder element */
  2278.             } else { // both operands are symbolic
  2279.                 sym_v2._append(sym_v1);
  2280.                 sf.push(s2, true); /* string Builder element can continue */
  2281.             }
  2282.  
  2283.             sf.setOperandAttr(sym_v2);
  2284.         }
  2285.     }
  2286.    
  2287.     public Instruction handleStringAppend3(JVMInvokeInstruction invInst, ThreadInfo th) {
  2288.         StackFrame sf = th.getModifiableTopFrame();
  2289.        
  2290.         IntegerExpression sym_end = (IntegerExpression) sf.getOperandAttr(0);
  2291.         IntegerExpression sym_start = (IntegerExpression) sf.getOperandAttr(1);
  2292.         StringExpression sym_string = (StringExpression) sf.getOperandAttr(2);
  2293.         SymbolicStringBuilder sym_builder = (SymbolicStringBuilder) sf.getOperandAttr(3);
  2294.  
  2295.         if (sym_builder == null) {
  2296.             sym_builder = new SymbolicStringBuilder();
  2297.         }
  2298.        
  2299.         //check if all parameters are concrete
  2300.         boolean concreteSubstring = (sym_end == null & sym_start == null & sym_string == null);
  2301.        
  2302.         if (concreteSubstring & sym_builder.getstr() == null) {
  2303.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleStringAppend3");
  2304.         } else {
  2305.             int endRef = sf.pop();
  2306.             int startRef = sf.pop();
  2307.             int stringRef = sf.pop();
  2308.             int builderRef = sf.pop();
  2309.    
  2310.             //prepare the substring
  2311.             StringExpression substring;
  2312.             if(concreteSubstring) {
  2313.                 try {
  2314.                     ElementInfo eiString = th.getElementInfo(stringRef);
  2315.                     String concreteString = eiString.asString();
  2316.                     String slice = concreteString.substring(startRef, endRef);
  2317.                     substring = new StringConstant(slice);
  2318.                 } catch (IndexOutOfBoundsException e) {
  2319.                     return th.createAndThrowException("java.lang.IndexOutOfBoundsException",e.getMessage());
  2320.                 }
  2321.             } else {
  2322.                 if(sym_string == null) {
  2323.                     ElementInfo eString = th.getElementInfo(stringRef);
  2324.                     String concreteString = eString.asString();
  2325.                     sym_string = new StringConstant(concreteString);
  2326.                 }
  2327.                 substring = createSymbolicSubstring(sym_string, sym_start, sym_end, startRef, endRef);
  2328.             }
  2329.            
  2330.             //append to the symbolic string
  2331.             if(sym_builder.getstr() == null) { //stringbuilder is concrete
  2332.                 ElementInfo eiBuilder = th.getElementInfo(builderRef);
  2333.                 String builderContents = getStringEquiv(eiBuilder);
  2334.                 sym_builder.putstr(new StringConstant(builderContents));
  2335.             }
  2336.            
  2337.             sym_builder._append(substring);
  2338.             sf.push(builderRef,true);
  2339.         }
  2340.        
  2341.         sf.setOperandAttr(sym_builder);
  2342.        
  2343.         return null;
  2344.     }
  2345.    
  2346.     //helper
  2347.     private StringExpression createSymbolicSubstring(StringExpression sym_str,
  2348.             IntegerExpression sym_start, IntegerExpression sym_end,
  2349.             int startRef, int endRef) {
  2350.        
  2351.         StringExpression result;
  2352.        
  2353.         //'end' is the first parameter (something with stack representation, maybe?)
  2354.         if(sym_start == null && sym_end == null) {
  2355.             result = sym_str._subString(endRef, startRef);
  2356.         } else if (sym_start == null) {
  2357.             result = sym_str._subString(sym_end, startRef);
  2358.         } else { //sym_end == null
  2359.             result = sym_str._subString(endRef, sym_start);
  2360.         }
  2361.        
  2362.         return result;
  2363.     }
  2364.    
  2365.     public Instruction handleStringBuilderAppend3(JVMInvokeInstruction invInst, ThreadInfo th) {
  2366.         throw new RuntimeException("implement this");
  2367.     }
  2368.  
  2369.     public void setVariableAttribute(ElementInfo ei, JVMInvokeInstruction invInst, ThreadInfo th, StackFrame sf, int idx,
  2370.             Object sym_v2) {
  2371.         int count = sf.getLocalVariableCount();
  2372.         for (int i = 0; i < count; i++) {
  2373.             int idx1 = sf.getLocalVariable(i);
  2374.             if (idx1 == idx) {
  2375.                 sf.setLocalAttr(i, sym_v2);
  2376.                 return;
  2377.             }
  2378.         }
  2379.         // If variable is a static field and not local variable
  2380.         ClassInfo ci = sf.getClassInfo();
  2381.         FieldInfo[] fields = ci.getDeclaredStaticFields();
  2382.         int fieldid = -1;
  2383.         for (int i = 0; i < fields.length; i++) {
  2384.             if (fields[i].isReference()) {
  2385.                 fieldid = ci.getStaticElementInfo().getReferenceField(fields[i]);
  2386.             }
  2387.             if (fieldid == idx) {
  2388.                 ci.getStaticElementInfo().setFieldAttr(fields[i], sym_v2);
  2389.                 return;
  2390.             }
  2391.         }
  2392.  
  2393.         // If variable is an instance field and not local variable
  2394.         FieldInfo[] fields1 = ci.getDeclaredInstanceFields();
  2395.         fieldid = -1;
  2396.         for (int i = 0; i < fields1.length; i++) {
  2397.             if (fields1[i].isReference()) {
  2398.                 fieldid = ei.getReferenceField(fields1[i]);
  2399.             }
  2400.             if (fieldid == idx) {
  2401.                 ei.setFieldAttr(fields1[i], sym_v2);
  2402.                 return;
  2403.             }
  2404.         }
  2405.         // if method does not return anything then
  2406.         MethodInfo mi = invInst.getInvokedMethod();
  2407.         byte b = mi.getReturnTypeCode();
  2408.         if (b == Types.T_VOID)
  2409.             System.out.println("WARNING: Could not set variable attribute");
  2410.  
  2411.     }
  2412.  
  2413.     public void handleCharAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2414.  
  2415.         StackFrame sf = th.getModifiableTopFrame();
  2416.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  2417.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  2418.  
  2419.         if (sym_v2 == null)
  2420.             sym_v2 = new SymbolicStringBuilder();
  2421.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  2422.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleCharAppend");
  2423.         } else {
  2424.             char s1 = (char) sf.pop();
  2425.             int s2 = sf.pop();
  2426.             if (sym_v1 == null) { // operand 0 is concrete
  2427.                 String val = Character.toString(s1);
  2428.                 sym_v2._append(val);
  2429.                 sf.push(s2, true); /* symbolic string Builder element */
  2430.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2431.                 // from String builder object
  2432.                 ElementInfo e1 = th.getElementInfo(s2);
  2433.                 String val = getStringEquiv(e1);
  2434.                 sym_v2.putstr(new StringConstant(val));
  2435.                 sym_v2._append(sym_v1);
  2436.                 sf.push(s2, true); /* symbolic string Builder element */
  2437.             } else { // both operands are symbolic
  2438.                 sym_v2._append(sym_v1);
  2439.                 sf.push(s2, true); /* string Builder element can continue */
  2440.             }
  2441.  
  2442.             sf.setOperandAttr(sym_v2);
  2443.         }
  2444.     }
  2445.  
  2446.     public void handleByteAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2447.  
  2448.         StackFrame sf = th.getModifiableTopFrame();
  2449.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  2450.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  2451.  
  2452.         if (sym_v2 == null)
  2453.             sym_v2 = new SymbolicStringBuilder();
  2454.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  2455.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleByteAppend");
  2456.         } else {
  2457.             byte s1 = (byte) sf.pop();
  2458.             int s2 = sf.pop();
  2459.             if (sym_v1 == null) { // operand 0 is concrete
  2460.                 String val = Byte.toString(s1);
  2461.                 sym_v2._append(val);
  2462.                 sf.push(s2, true); /* symbolic string Builder element */
  2463.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2464.                 // from String builder object
  2465.                 ElementInfo e1 = th.getElementInfo(s2);
  2466.                 String val = getStringEquiv(e1);
  2467.                 sym_v2.putstr(new StringConstant(val));
  2468.                 sym_v2._append(sym_v1);
  2469.                 sf.push(s2, true); /* symbolic string Builder element */
  2470.             } else { // both operands are symbolic
  2471.                 sym_v2._append(sym_v1);
  2472.                 sf.push(s2, true); /* string Builder element can continue */
  2473.             }
  2474.  
  2475.             sf.setOperandAttr(sym_v2);
  2476.         }
  2477.     }
  2478.  
  2479.     public void handleShortAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2480.  
  2481.         StackFrame sf = th.getModifiableTopFrame();
  2482.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  2483.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  2484.  
  2485.         if (sym_v2 == null)
  2486.             sym_v2 = new SymbolicStringBuilder();
  2487.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  2488.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleShortAppend");
  2489.         } else {
  2490.             short s1 = (short) sf.pop();
  2491.             int s2 = sf.pop();
  2492.             if (sym_v1 == null) { // operand 0 is concrete
  2493.                 String val = Short.toString(s1);
  2494.                 sym_v2._append(val);
  2495.                 sf.push(s2, true); /* symbolic string Builder element */
  2496.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2497.                 // from String builder object
  2498.                 ElementInfo e1 = th.getElementInfo(s2);
  2499.                 String val = getStringEquiv(e1);
  2500.                 sym_v2.putstr(new StringConstant(val));
  2501.                 sym_v2._append(sym_v1);
  2502.                 sf.push(s2, true); /* symbolic string Builder element */
  2503.             } else { // both operands are symbolic
  2504.                 sym_v2._append(sym_v1);
  2505.                 sf.push(s2, true); /* string Builder element can continue */
  2506.             }
  2507.  
  2508.             sf.setOperandAttr(sym_v2);
  2509.         }
  2510.     }
  2511.  
  2512.     public void handleIntAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2513.  
  2514.         StackFrame sf = th.getModifiableTopFrame();
  2515.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  2516.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  2517.  
  2518.         if (sym_v2 == null)
  2519.             sym_v2 = new SymbolicStringBuilder();
  2520.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  2521.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: hanldeIntAppend");
  2522.         } else {
  2523.             int s1 = sf.pop();
  2524.             int s2 = sf.pop();
  2525.             if (sym_v1 == null) { // operand 0 is concrete
  2526.                 String val = Integer.toString(s1);
  2527.                 sym_v2._append(val);
  2528.                 sf.push(s2, true); /* symbolic string Builder element */
  2529.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2530.                 // from String builder object
  2531.                 ElementInfo e1 = th.getElementInfo(s2);
  2532.                 String val = getStringEquiv(e1);
  2533.                 sym_v2.putstr(new StringConstant(val));
  2534.                 sym_v2._append(sym_v1);
  2535.                 sf.push(s2, true); /* symbolic string Builder element */
  2536.             } else { // both operands are symbolic
  2537.                 sym_v2._append(sym_v1);
  2538.                 sf.push(s2, true); /* string Builder element can continue */
  2539.             }
  2540.  
  2541.             sf.setOperandAttr(sym_v2);
  2542.         }
  2543.     }
  2544.  
  2545.     public void handleFloatAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2546.  
  2547.         StackFrame sf = th.getModifiableTopFrame();
  2548.         RealExpression sym_v1 = (RealExpression) sf.getOperandAttr(0);
  2549.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  2550.  
  2551.         if (sym_v2 == null)
  2552.             sym_v2 = new SymbolicStringBuilder();
  2553.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  2554.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: hanldeFloatAppend");
  2555.         } else {
  2556.             float s1 = Types.intToFloat(sf.pop());
  2557.             int s2 = sf.pop();
  2558.             if (sym_v1 == null) { // operand 0 is concrete
  2559.                 String val = Float.toString(s1);
  2560.                 sym_v2._append(val);
  2561.                 sf.push(s2, true); /* symbolic string Builder element */
  2562.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2563.                 // from String builder object
  2564.                 ElementInfo e1 = th.getElementInfo(s2);
  2565.                 String val = getStringEquiv(e1);
  2566.                 sym_v2.putstr(new StringConstant(val));
  2567.                 sym_v2._append(sym_v1);
  2568.                 sf.push(s2, true); /* symbolic string Builder element */
  2569.             } else { // both operands are symbolic
  2570.                 sym_v2._append(sym_v1);
  2571.                 sf.push(s2, true); /* string Builder element can continue */
  2572.             }
  2573.  
  2574.             sf.setOperandAttr(sym_v2);
  2575.         }
  2576.     }
  2577.  
  2578.     public void handleBooleanAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2579.         StackFrame sf = th.getModifiableTopFrame();
  2580.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  2581.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  2582.  
  2583.         if (sym_v2 == null)
  2584.             sym_v2 = new SymbolicStringBuilder();
  2585.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  2586.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: hanldeBooleanAppend");
  2587.         } else {
  2588.             boolean s1 = Types.intToBoolean(sf.pop());
  2589.             int s2 = sf.pop();
  2590.             if (sym_v1 == null) { // operand 0 is concrete
  2591.                 String val = Boolean.toString(s1);
  2592.                 sym_v2._append(val);
  2593.                 sf.push(s2, true); /* symbolic string Builder element */
  2594.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2595.                 // from String builder object
  2596.                 ElementInfo e1 = th.getElementInfo(s2);
  2597.                 String val = getStringEquiv(e1);
  2598.                 sym_v2.putstr(new StringConstant(val));
  2599.                 sym_v2._append(sym_v1); /*
  2600.                                                                  * String s1 =
  2601.                                                                  * AbstractionUtilityMethods.unknownString();
  2602.                                                                  * String s2 =
  2603.                                                                  * AbstractionUtilityMethods.unknownString();
  2604.                                                                  * String s4 =
  2605.                                                                  * AbstractionUtilityMethods.unknownString();
  2606.                                                                  * String s5 =
  2607.                                                                  * AbstractionUtilityMethods.unknownString();
  2608.                                                                  */
  2609.  
  2610.                 sf.push(s2, true); /* symbolic string Builder element */
  2611.             } else { // both operands are symbolic
  2612.                 sym_v2._append(sym_v1);
  2613.                 sf.push(s2, true); /* string Builder element can continue */
  2614.             }
  2615.  
  2616.             sf.setOperandAttr(sym_v2);
  2617.         }
  2618.     }
  2619.  
  2620.     public void handleLongAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2621.  
  2622.         StackFrame sf = th.getModifiableTopFrame();
  2623.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  2624.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(2);
  2625.  
  2626.         if (sym_v2 == null)
  2627.             sym_v2 = new SymbolicStringBuilder();
  2628.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  2629.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleLongAppend");
  2630.         } else {
  2631.             long s1 = sf.popLong();
  2632.             int s2 = sf.pop();
  2633.             if (sym_v1 == null) { // operand 0 is concrete
  2634.                 String val = Long.toString(s1);
  2635.                 sym_v2._append(val);
  2636.                 sf.push(s2, true); /* symbolic string Builder element */
  2637.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2638.                 // from String builder object
  2639.                 ElementInfo e1 = th.getElementInfo(s2);
  2640.                 String val = getStringEquiv(e1);
  2641.                 sym_v2.putstr(new StringConstant(val));
  2642.                 sym_v2._append(sym_v1);
  2643.                 sf.push(s2, true); /* symbolic string Builder element */
  2644.             } else { // both operands are symbolic
  2645.                 sym_v2._append(sym_v1);
  2646.                 sf.push(s2, true); /* string Builder element can continue */
  2647.             }
  2648.  
  2649.             sf.setOperandAttr(sym_v2);
  2650.         }
  2651.     }
  2652.  
  2653.     public void handleDoubleAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2654.  
  2655.         StackFrame sf = th.getModifiableTopFrame();
  2656.  
  2657.         RealExpression sym_v1 = (RealExpression) sf.getLongOperandAttr();
  2658.         double s1 = Types.longToDouble(sf.popLong());
  2659.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr();
  2660.         int s2 = sf.pop();
  2661.  
  2662.         if (sym_v2 == null)
  2663.             sym_v2 = new SymbolicStringBuilder();
  2664.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  2665.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand");
  2666.         } else {
  2667.  
  2668.             if (sym_v1 == null) { // operand 0 is concrete
  2669.                 String val = Double.toString(s1);
  2670.                 sym_v2._append(val);
  2671.                 sf.push(s2, true); /* symbolic string Builder element */
  2672.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2673.                 // from String builder object
  2674.                 ElementInfo e1 = th.getElementInfo(s2);
  2675.                 String val = getStringEquiv(e1);
  2676.                 sym_v2.putstr(new StringConstant(val));
  2677.                 sym_v2._append(sym_v1);
  2678.                 sf.push(s2, true); /* symbolic string Builder element */
  2679.             } else { // both operands are symbolic
  2680.                 sym_v2._append(sym_v1);
  2681.                 sf.push(s2, true); /* string Builder element can continue */
  2682.             }
  2683.  
  2684.             sf.setOperandAttr(sym_v2);
  2685.         }
  2686.     }
  2687.  
  2688.     /*
  2689.      * String s1 = AbstractionUtilityMethods.unknownString(); String s2 =
  2690.      * AbstractionUtilityMethods.unknownString(); String s4 =
  2691.      * AbstractionUtilityMethods.unknownString(); String s5 =
  2692.      * AbstractionUtilityMethods.unknownString();
  2693.      */
  2694.  
  2695.     public void handleObjectAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2696.         StackFrame sf = th.getModifiableTopFrame();
  2697.  
  2698.         Expression sym_v1 = (Expression) sf.getOperandAttr(0);
  2699.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  2700.         // System.out.println(invInst.getSourceLocation());
  2701.         if (sym_v2 == null)
  2702.             sym_v2 = new SymbolicStringBuilder();
  2703.         if ((sym_v1 == null) && (sym_v2.getstr() == null)) {
  2704.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleObjectAppend");
  2705.         } else {
  2706.             int s1 = sf.pop();
  2707.             ElementInfo e2 = th.getElementInfo(s1);
  2708.             int s2 = sf.pop();
  2709.             if (sym_v1 == null || (sym_v1 instanceof SymbolicStringBuilder
  2710.                     && ((SymbolicStringBuilder) sym_v1).getstr() == null)) { // operand 0 is concrete
  2711.                 String val = getStringEquiv(e2);
  2712.                 sym_v2._append(val);
  2713.                 sf.push(s2, true); /* symbolic string Builder element */
  2714.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2715.                 // from String builder object
  2716.                 ElementInfo e1 = th.getElementInfo(s2);
  2717.                 String val = getStringEquiv(e1);
  2718.                 sym_v2.putstr(new StringConstant(val));
  2719.                 if (sym_v1 instanceof SymbolicStringBuilder)
  2720.                     sym_v2._append((SymbolicStringBuilder) sym_v1);
  2721.                 else if (sym_v1 instanceof StringExpression)
  2722.                     sym_v2._append((StringExpression) sym_v1);
  2723.                 else {
  2724.                     throw new RuntimeException("Object not handled in ObjectAppend");
  2725.                 }
  2726.                 // setVariableAttribute(ei, invInst, th, sf, s2, sym_v2); //set the
  2727.                 // value of the attribute of local StringBuilder element as sym_v2
  2728.                 sf.push(s2, true); /* symbolic string Builder element */
  2729.             } else { // both operands are symbolic
  2730.                 if (sym_v1 instanceof SymbolicStringBuilder)
  2731.                     sym_v2._append((SymbolicStringBuilder) sym_v1);
  2732.                 else if (sym_v1 instanceof StringExpression)
  2733.                     sym_v2._append((StringExpression) sym_v1);
  2734.                 else {
  2735.                     throw new RuntimeException("Object not handled in ObjectAppend");
  2736.                 }
  2737.  
  2738.                 sf.push(s2, true); /* string Builder element can continue */
  2739.             }
  2740.             sf.setOperandAttr(sym_v2);
  2741.         }
  2742.     }
  2743.  
  2744.     public void handleStringBuilderAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  2745.  
  2746.         StackFrame sf = th.getModifiableTopFrame();
  2747.         SymbolicStringBuilder sym_v1 = (SymbolicStringBuilder) sf.getOperandAttr(0);
  2748.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  2749.  
  2750.         if (sym_v2 == null)
  2751.             sym_v2 = new SymbolicStringBuilder();
  2752.         if (sym_v1 == null)
  2753.             sym_v1 = new SymbolicStringBuilder();
  2754.  
  2755.         if ((sym_v1.getstr() == null) & (sym_v2.getstr() == null)) {
  2756.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: hanldeStringBuilderAppend");
  2757.         } else {
  2758.             int s1 = sf.pop();
  2759.             int s2 = sf.pop();
  2760.  
  2761.             if (sym_v1.getstr() == null) { // operand 0 is concrete
  2762.                 ElementInfo e1 = th.getElementInfo(s1);
  2763.                 String val = getStringEquiv(e1);
  2764.                 sym_v2._append(val);
  2765.                 sf.push(s2, true); /* symbolic string Builder element */
  2766.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  2767.                 // from String builder object
  2768.                 ElementInfo e1 = th.getElementInfo(s2);
  2769.                 String val = getStringEquiv(e1);
  2770.                 sym_v2.putstr(new StringConstant(val));
  2771.                 sym_v2._append(sym_v1);
  2772.                 sf.push(s2, true); /* symbolic string Builder element */
  2773.             } else { // both operands are symbolic
  2774.                 sym_v2._append(sym_v1);
  2775.                 sf.push(s2, true); /* string Builder element can continue */
  2776.             }
  2777.  
  2778.             sf.setOperandAttr(sym_v2);
  2779.         }
  2780.     }
  2781.  
  2782.     public String getStringEquiv(ElementInfo ei) {
  2783.         String objectType = ei.getType();
  2784.         if (objectType.equals("Ljava/lang/StringBuilder;")) {
  2785.             int idx = ei.getReferenceField("value");
  2786.             int length = ei.getIntField("count");
  2787.             ElementInfo e1 = VM.getVM().getHeap().get(idx);
  2788.             char[] str = e1.asCharArray();
  2789.             String val = new String(str, 0, length);
  2790.             return val;
  2791.         } else if (objectType.equals("Ljava/lang/StringBuffer;")) {
  2792.             int idx = ei.getReferenceField("value");
  2793.             int length = ei.getIntField("count");
  2794.             ElementInfo e1 = VM.getVM().getHeap().get(idx);
  2795.             char[] str = e1.asCharArray();
  2796.             String val = new String(str, 0, length);
  2797.             return val;
  2798.         } else if (objectType.equals("Ljava/lang/Integer;")) {
  2799.             int val = ei.getIntField("value");
  2800.             return Integer.toString(val);
  2801.         } else if (objectType.equals("Ljava/lang/Float;")) {
  2802.             float val = ei.getFloatField("value");
  2803.             return Float.toString(val);
  2804.         } else if (objectType.equals("Ljava/lang/Long;")) {
  2805.             long val = ei.getLongField("value");
  2806.             return Long.toString(val);
  2807.         } else if (objectType.equals("Ljava/lang/Double;")) {
  2808.             double val = ei.getDoubleField("value");
  2809.             return Double.toString(val);
  2810.         } else if (objectType.equals("Ljava/lang/Boolean;")) {
  2811.             boolean val = ei.getBooleanField("value");
  2812.             return Boolean.toString(val);
  2813.         } else {
  2814.             throw new RuntimeException("ERROR: Object Type Not Handled in getStringVal");
  2815.         }
  2816.     }
  2817.  
  2818.     public Instruction handletoString(JVMInvokeInstruction invInst,  ThreadInfo th) {
  2819.         StackFrame sf = th.getModifiableTopFrame();
  2820.         Object sym_obj_v2 = sf.getOperandAttr(0);
  2821.         if (sym_obj_v2 instanceof StringExpression) {
  2822.             return null;
  2823.         }
  2824.         StringExpression sym_v1 = null;
  2825.         if (sym_obj_v2 instanceof SymbolicStringBuilder) {
  2826.             SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sym_obj_v2;
  2827.             sym_v1 = sym_v2.getstr();
  2828.         } else {
  2829.             throw new RuntimeException("ERROR: symbolic type not Handled: toString");
  2830.         }
  2831.  
  2832.         if ((sym_v1 == null)) {
  2833.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: toString");
  2834.         } else {
  2835.             sf.pop();
  2836.             ElementInfo ei = th.getHeap().newString("", th);
  2837.             int objRef = ei.getObjectRef();
  2838.             sf.push(objRef, true);
  2839.             sf.setOperandAttr(sym_v1);
  2840.         }
  2841.         return null;
  2842.     }
  2843.  
  2844.     public void handleprintln(JVMInvokeInstruction invInst, ThreadInfo th, boolean doPrintln) {
  2845.         StackFrame sf = th.getModifiableTopFrame();
  2846.         MethodInfo mi = invInst.getInvokedMethod(th);
  2847.         String[] argTypes = mi.getArgumentTypeNames();
  2848.         Expression sym_v1 = null;
  2849.         boolean flag = false;
  2850.         if ((argTypes[0].equals("long")) || (argTypes[0].equals("double"))) {
  2851.             sym_v1 = (Expression) sf.getLongOperandAttr();
  2852.             flag = true;
  2853.         } else {
  2854.             sym_v1 = (Expression) sf.getOperandAttr(0);
  2855.         }
  2856.  
  2857.         if ((sym_v1 == null)) {
  2858.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: println");
  2859.         } else {
  2860.             if (flag)
  2861.                 sf.popLong();
  2862.             else
  2863.                 sf.pop(); // clear out operand stack
  2864.             sf.pop();
  2865.             String result = sym_v1.toString();
  2866.             if (doPrintln) {
  2867.                 System.out.println("Symbolic Exp [ " + result + "]");
  2868.             } else {
  2869.                 System.out.print("Symbolic Exp [ " + result + " ]");
  2870.             }
  2871.             th.getHeap().newString("", th); //Corina this code is so broken
  2872.             //th.push(objRef, true);
  2873.             //sf.setOperandAttr(sym_v1);
  2874.         }
  2875.     }
  2876. }/*
  2877.  * Copyright (C) 2014, United States Government, as represented by the
  2878.  * Administrator of the National Aeronautics and Space Administration.
  2879.  * All rights reserved.
  2880.  *
  2881.  * Symbolic Pathfinder (jpf-symbc) is licensed under the Apache License,
  2882.  * Version 2.0 (the "License"); you may not use this file except
  2883.  * in compliance with the License. You may obtain a copy of the License at
  2884.  *
  2885.  *        http://www.apache.org/licenses/LICENSE-2.0.
  2886.  *
  2887.  * Unless required by applicable law or agreed to in writing, software
  2888.  * distributed under the License is distributed on an "AS IS" BASIS,
  2889.  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  2890.  * See the License for the specific language governing permissions and
  2891.  * limitations under the License.
  2892.  */
  2893.  
  2894. /*  Copyright (C) 2005 United States Government as represented by the
  2895. Administrator of the National Aeronautics and Space Administration
  2896. (NASA).  All Rights Reserved.
  2897.  
  2898. Copyright (C) 2009 Fujitsu Laboratories of America, Inc.
  2899.  
  2900. DISCLAIMER OF WARRANTIES AND LIABILITIES; WAIVER AND INDEMNIFICATION
  2901.  
  2902. A. No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY
  2903. WARRANTY OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY,
  2904. INCLUDING, BUT NOT LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE
  2905. WILL CONFORM TO SPECIFICATIONS, ANY IMPLIED WARRANTIES OF
  2906. MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR FREEDOM FROM
  2907. INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE ERROR
  2908. FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO
  2909. THE SUBJECT SOFTWARE. NO SUPPORT IS WARRANTED TO BE PROVIDED AS IT IS PROVIDED "AS-IS".
  2910.  
  2911. B. Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS
  2912. AGAINST FUJITSU LABORATORIES OF AMERICA AND ANY OF ITS AFFILIATES, THE
  2913. UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL
  2914. AS ANY PRIOR RECIPIENT.  IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE
  2915. RESULTS IN ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING
  2916. FROM SUCH USE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING
  2917. FROM, RECIPIENT'S USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY
  2918. AND HOLD HARMLESS FUJITSU LABORATORTIES OF AMERICA AND ANY OF ITS AFFILIATES,
  2919. THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL
  2920. AS ANY PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW.  RECIPIENT'S SOLE
  2921. REMEDY FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL
  2922. TERMINATION OF THIS AGREEMENT. */
  2923.  
  2924.  
  2925.  
  2926. package gov.nasa.jpf.symbc.bytecode;
  2927.  
  2928.  
  2929.  
  2930. import gov.nasa.jpf.symbc.numeric.*;
  2931. import gov.nasa.jpf.vm.ChoiceGenerator;
  2932. import gov.nasa.jpf.vm.ClassInfo;
  2933. import gov.nasa.jpf.vm.ClassLoaderInfo;
  2934. import gov.nasa.jpf.vm.ElementInfo;
  2935. import gov.nasa.jpf.vm.FieldInfo;
  2936. import gov.nasa.jpf.vm.Instruction;
  2937. import gov.nasa.jpf.vm.MethodInfo;
  2938. import gov.nasa.jpf.vm.SystemState;
  2939. import gov.nasa.jpf.vm.Types;
  2940. import gov.nasa.jpf.vm.VM;
  2941. import gov.nasa.jpf.vm.StackFrame;
  2942. import gov.nasa.jpf.vm.ThreadInfo;
  2943. import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
  2944. import gov.nasa.jpf.symbc.mixednumstrg.SpecialRealExpression;
  2945. import gov.nasa.jpf.symbc.string.*;
  2946. import gov.nasa.jpf.symbc.mixednumstrg.*;
  2947.  
  2948.  
  2949. public class SymbolicStringHandler {
  2950.     static int handlerStep = 0;
  2951.     static Instruction handlerStepSavedNext = null;
  2952.     static Object handlerStepSavedValue = null;
  2953.  
  2954.     public static final int intValueOffset = 5;
  2955.  
  2956.     /* this method checks if a method has as argument any symbolic strings */
  2957.    
  2958.     public boolean isMethodStringSymbolic(JVMInvokeInstruction invInst, ThreadInfo th) {
  2959.         String cname = invInst.getInvokedMethodClassName();
  2960.  
  2961.         if (cname.equals("java.lang.String")
  2962.                 || cname.equals("java.lang.StringBuilder")
  2963.                 || cname.equals("java.lang.StringBuffer")
  2964.                 || cname.equals("java.lang.CharSequence")
  2965.                 || cname.equals("java.lang.Appendable")
  2966.                 || cname.equals("java.io.PrintStream")
  2967.                 || cname.equals("java.lang.Integer")
  2968.                 || cname.equals("java.lang.Float")
  2969.                 || cname.equals("java.lang.Double")
  2970.                 || cname.equals("java.lang.Long")
  2971.                 || cname.equals("java.lang.Short")
  2972.                 || cname.equals("java.lang.Byte")
  2973.                 || cname.equals("java.lang.Char")
  2974.                 || cname.equals("java.lang.Boolean")
  2975.                 || cname.equals("java.lang.Object")) {
  2976.            
  2977.             StackFrame sf = th.getModifiableTopFrame();
  2978.  
  2979.             int numStackSlots = invInst.getArgSize();
  2980.  
  2981.             for (int i = 0; i < numStackSlots; i++) {
  2982.                 Expression sym_v1 = (Expression) sf.getOperandAttr(i);
  2983.                 if (sym_v1 != null) {
  2984.                     if (sym_v1 instanceof SymbolicStringBuilder) { // check if
  2985.                         // StringBuilder has
  2986.                         // empty attribute
  2987.                         if (((SymbolicStringBuilder) sym_v1).getstr() != null) {
  2988.                             return true;
  2989.                         }
  2990.                     } else if (sym_v1 instanceof IntegerExpression && cname.equals("java.lang.StringBuilder")){
  2991.                         //to revise
  2992.                         return true;
  2993.                     } else {
  2994.                         return true;
  2995.                     }
  2996.                    
  2997.                 }
  2998.             }
  2999.             return false;
  3000.         }  
  3001.         else return false;
  3002.     }
  3003.  
  3004.     public Instruction handleSymbolicStrings(JVMInvokeInstruction invInst, ThreadInfo th) {
  3005.  
  3006.         boolean needToHandle = isMethodStringSymbolic(invInst, th);
  3007.  
  3008.         if (needToHandle) {
  3009.             // do the string manipulations
  3010.             String mname = invInst.getInvokedMethodName();
  3011.             String shortName = mname.substring(0, mname.indexOf("("));
  3012.             if (shortName.equals("concat")) {
  3013.                 Instruction handled = handleConcat(invInst, th);
  3014.                 if (handled != null) {
  3015.                     return handled;
  3016.                 }
  3017.             } else if (shortName.equals("equals")) {
  3018.                 ChoiceGenerator<?> cg;
  3019.                 if (!th.isFirstStepInsn()) { // first time around
  3020.                     cg = new PCChoiceGenerator(2);
  3021.                     th.getVM().setNextChoiceGenerator(cg);
  3022.                     return invInst;
  3023.                 } else {
  3024.                     handleObjectEquals(invInst, th);
  3025.                     return invInst.getNext(th);
  3026.                 }
  3027.             } else if (shortName.equals("equalsIgnoreCase")) {
  3028.                 ChoiceGenerator<?> cg;
  3029.                 if (!th.isFirstStepInsn()) { // first time around
  3030.                     cg = new PCChoiceGenerator(2);
  3031.                     th.getVM().setNextChoiceGenerator(cg);
  3032.                     return invInst;
  3033.                 } else {
  3034.                     handleEqualsIgnoreCase(invInst,  th);
  3035.                     return invInst.getNext(th);
  3036.                 }
  3037.             } else if (shortName.equals("endsWith")) {
  3038.                 ChoiceGenerator<?> cg;
  3039.                 if (!th.isFirstStepInsn()) { // first time around
  3040.                     cg = new PCChoiceGenerator(2);
  3041.                     th.getVM().setNextChoiceGenerator(cg);
  3042.                     return invInst;
  3043.                 } else {
  3044.                     handleEndsWith(invInst, th);
  3045.                     return invInst.getNext(th);
  3046.                 }
  3047.             } else if (shortName.equals("startsWith")) {
  3048.                 ChoiceGenerator<?> cg;
  3049.                 if (!th.isFirstStepInsn()) { // first time around
  3050.                     cg = new PCChoiceGenerator(2);
  3051.                     th.getVM().setNextChoiceGenerator(cg);
  3052.                     return invInst;
  3053.                 } else {
  3054.                     handleStartsWith(invInst, th);
  3055.                     return invInst.getNext(th);
  3056.                 }
  3057.             } else if (shortName.equals ("contains")) {
  3058.                 ChoiceGenerator<?> cg;
  3059.                 if (!th.isFirstStepInsn()) { // first time around
  3060.                     cg = new PCChoiceGenerator(2);
  3061.                     th.getVM().setNextChoiceGenerator(cg);
  3062.                     return invInst;
  3063.                 } else {
  3064.                     handleContains(invInst, th);
  3065.                     return invInst.getNext(th);
  3066.                 }
  3067.             } else if (shortName.equals("append")) {
  3068.                 Instruction handled = handleAppend(invInst, th);
  3069.                 if (handled != null) {
  3070.                     return handled;
  3071.                 }
  3072.             } else if (shortName.equals("length")) {
  3073.                 handleLength(invInst, th);
  3074.             } else if (shortName.equals("indexOf")) {
  3075.                 handleIndexOf(invInst, th);
  3076.             } else if (shortName.equals("lastIndexOf")) {
  3077.                 handleLastIndexOf(invInst, th);
  3078.             } else if (shortName.equals("charAt")) {
  3079.                 handleCharAt (invInst, th); // returns boolean that is ignored
  3080.                 //return invInst;
  3081.             } else if (shortName.equals("replace")) {
  3082.                 Instruction handled = handleReplace(invInst, th);
  3083.                 if (handled != null) {
  3084.                     return handled;
  3085.                 }
  3086.             } else if (shortName.equals("replaceFirst")) {
  3087.                 Instruction handled = handleReplaceFirst(invInst, th);
  3088.                 if (handled != null) {
  3089.                     return handled;
  3090.                 }
  3091.             } else if (shortName.equals("trim")) {
  3092.                 handleTrim(invInst, th);
  3093.             } else if (shortName.equals("substring")) {
  3094.                 Instruction handled = handleSubString(invInst, th);
  3095.                 if (handled != null) {
  3096.                     return handled;
  3097.                 }
  3098.             } else if (shortName.equals("valueOf")) {
  3099.                 Instruction handled = handleValueOf(invInst, th);
  3100.                 if (handled != null) {
  3101.                     return handled;
  3102.                 }
  3103.             } else if (shortName.equals("parseInt")) {
  3104.                 ChoiceGenerator<?> cg;
  3105.                 if (!th.isFirstStepInsn()) { // first time around
  3106.                     cg = new PCChoiceGenerator(2);
  3107.                     th.getVM().setNextChoiceGenerator(cg);
  3108.                     return invInst;
  3109.                 } else {
  3110.                     handleParseInt(invInst, th);
  3111.                     return invInst.getNext(th);
  3112.                 }
  3113.             } else if (shortName.equals("parseFloat")) {
  3114.                 ChoiceGenerator<?> cg;
  3115.                 if (!th.isFirstStepInsn()) { // first time around
  3116.                     cg = new PCChoiceGenerator(2);
  3117.                     th.getVM().setNextChoiceGenerator(cg);
  3118.                     return invInst;
  3119.                 } else {
  3120.                     handleParseFloat(invInst, th);
  3121.                     return invInst.getNext(th);
  3122.                 }
  3123.             } else if (shortName.equals("parseLong")) {
  3124.                 ChoiceGenerator<?> cg;
  3125.                 if (!th.isFirstStepInsn()) { // first time around
  3126.                     cg = new PCChoiceGenerator(2);
  3127.                     th.getVM().setNextChoiceGenerator(cg);
  3128.                     return invInst;
  3129.                 } else {
  3130.                     handleParseLong(invInst, th);
  3131.                     return invInst.getNext(th);
  3132.                 }
  3133.             } else if (shortName.equals("parseDouble")) {
  3134.                 ChoiceGenerator<?> cg;
  3135.                 if (!th.isFirstStepInsn()) { // first time around
  3136.                     cg = new PCChoiceGenerator(2);
  3137.                     th.getVM().setNextChoiceGenerator(cg);
  3138.                     return invInst;
  3139.                 } else {
  3140.                     handleParseDouble(invInst, th);
  3141.                     return invInst.getNext(th);
  3142.                 }
  3143.             } else if (shortName.equals("parseBoolean")) {
  3144.                 ChoiceGenerator<?> cg;
  3145.                 if (!th.isFirstStepInsn()) { // first time around
  3146.                     cg = new PCChoiceGenerator(2);
  3147.                     th.getVM().setNextChoiceGenerator(cg);
  3148.                     return invInst;
  3149.                 } else {
  3150.                     handleParseBoolean(invInst, th);
  3151.                     return invInst.getNext(th);
  3152.                 }
  3153.             } else if (shortName.equals("toString")) {
  3154.                 Instruction handled = handletoString(invInst, th);
  3155.                 if (handled != null) {
  3156.                     return handled;
  3157.                 }
  3158.             } else if (shortName.equals("println")) {
  3159.                 handleprintln(invInst, th, true);
  3160.             } else if (shortName.equals("print")) {
  3161.                 handleprintln(invInst, th, false);
  3162.             } else if (shortName.equals("<init>")) {
  3163.                 Instruction handled = handleInit(invInst, th);
  3164.                 if (handled != null) {
  3165.                     return handled;
  3166.                 } else {
  3167.                     return null;
  3168.                 }
  3169.             } else if (shortName.equals("intValue")) {
  3170.                 handleintValue(invInst, th);
  3171.             } else if (shortName.equals("floatValue")) {
  3172.                 handlefloatValue(invInst, th);
  3173.             } else if (shortName.equals("longValue")) {
  3174.                 handlelongValue(invInst, th);
  3175.             } else if (shortName.equals("doubleValue")) {
  3176.                 handledoubleValue(invInst, th);
  3177.             } else if (shortName.equals("booleanValue")) {
  3178.                 handlefloatValue(invInst, th);
  3179.             } else if (shortName.equals("isEmpty")) {
  3180.                 ChoiceGenerator<?> cg;
  3181.                 if (!th.isFirstStepInsn()){
  3182.                     cg = new PCChoiceGenerator(2);
  3183.                     th.getVM().setNextChoiceGenerator(cg);
  3184.                     return invInst;
  3185.                 } else {
  3186.                     handleIsEmpty(invInst, th);
  3187.                     return invInst.getNext(th);
  3188.                 }
  3189.             }else {
  3190.                 throw new RuntimeException("ERROR: symbolic method not handled: " + shortName);
  3191.                 //return null;
  3192.             }
  3193.             return invInst.getNext(th);
  3194.         } else {
  3195.             return null;
  3196.         }
  3197.  
  3198.     }
  3199.  
  3200.     private boolean handleCharAt (JVMInvokeInstruction invInst, ThreadInfo th) {
  3201.         StackFrame sf = th.getModifiableTopFrame();
  3202.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  3203.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  3204.         boolean bresult = false;
  3205.         if ((sym_v1 == null) & (sym_v2 == null)) {
  3206.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleCharAt");
  3207.         } else {
  3208.             int s1 = sf.pop();
  3209.             int s2 = sf.pop();
  3210.  
  3211.             IntegerExpression result = null;
  3212.             if (sym_v1 == null) { // operand 0 is concrete
  3213.  
  3214.                 int val = s1;
  3215.                 result = sym_v2._charAt(new IntegerConstant(val));
  3216.             } else {
  3217.  
  3218.                 if (sym_v2 == null) {
  3219.                     ElementInfo e1 = th.getElementInfo(s2);
  3220.                     String val2 = e1.asString();
  3221.                     sym_v2 = new StringConstant(val2);
  3222.                     result = sym_v2._charAt(sym_v1);
  3223.                 } else {
  3224.                     result = sym_v2._charAt(sym_v1);
  3225.                 }
  3226.                 bresult = true;
  3227.                 //System.out.println("[handleCharAt] Ignoring: " + result.toString());
  3228.                 //th.push(0, false);
  3229.             }
  3230.             sf.push(0, false);
  3231.             sf.setOperandAttr(result);
  3232.         }
  3233.         return bresult; // not used
  3234.  
  3235.     }
  3236.  
  3237.     public void handleLength(JVMInvokeInstruction invInst, ThreadInfo th) {
  3238.         StackFrame sf = th.getModifiableTopFrame();
  3239.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  3240.         if (sym_v1 == null) {
  3241.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleLength");
  3242.         } else {
  3243.             sf.pop();
  3244.             sf.push(0, false); /* dont care value for length */
  3245.             IntegerExpression sym_v2 = sym_v1._length();
  3246.             sf.setOperandAttr(sym_v2);
  3247.         }
  3248.  
  3249.     }
  3250.  
  3251.     public void handleIndexOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  3252.         int numStackSlots = invInst.getArgSize();
  3253.         if (numStackSlots == 2) {
  3254.             handleIndexOf1(invInst, th);
  3255.         } else {
  3256.             handleIndexOf2(invInst, th);
  3257.         }
  3258.  
  3259.     }
  3260.  
  3261.     /* two possibilities int, or String in parameter */
  3262.     public void handleIndexOf1(JVMInvokeInstruction invInst, ThreadInfo th) {
  3263.         StackFrame sf = th.getModifiableTopFrame();
  3264.        
  3265.         //boolean castException = false;
  3266.         StringExpression sym_v1 = null;
  3267.         Expression sym_v2 = null; // could be String or Char
  3268.         sym_v1 = (StringExpression)sf.getOperandAttr(1);
  3269.         sym_v2 = (Expression) sf.getOperandAttr(0);
  3270.         if (sym_v1 == null && sym_v2 == null) {
  3271.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleIndexOf1");
  3272.         } else {
  3273.             boolean s2char = true; //argument is char
  3274.             if (sf.isOperandRef()) {
  3275.                 s2char = false; //argument is string
  3276.             }
  3277.            
  3278.             int s1 = sf.pop();
  3279.             int s2 = sf.pop();
  3280.  
  3281.             IntegerExpression result = null;
  3282.             if (sym_v1 != null) {
  3283.                     if (sym_v2 != null) { // both are symbolic values
  3284.                         if (s2char)
  3285.                             result = sym_v1._indexOf((IntegerExpression)sym_v2);
  3286.                         else
  3287.                             result = sym_v1._indexOf((StringExpression)sym_v2);
  3288.                     } else { // sym_v2 is null
  3289.                         if (s2char) {
  3290.                             result = sym_v1._indexOf(new IntegerConstant(s2));
  3291.                         }
  3292.                         else {
  3293.                             ElementInfo e2 = th.getElementInfo(s2);
  3294.                             String val = e2.asString();
  3295.                             result = sym_v1._indexOf(new StringConstant(val));
  3296.                         }
  3297.                     }
  3298.             } else { // sym_v1 is null, sym_v2 must be not null
  3299.                     assert(sym_v2!=null);
  3300.                     ElementInfo e1 = th.getElementInfo(s2);
  3301.                     String val = e1.asString();
  3302.                     if (s2char)
  3303.                         result = new StringConstant(val)._indexOf((IntegerExpression)sym_v2);
  3304.                     else
  3305.                         result = new StringConstant(val)._indexOf((StringExpression)sym_v2);
  3306.             }
  3307.             sf.push(0, false);
  3308.             assert result != null;
  3309.             sf.setOperandAttr(result);
  3310.  
  3311.  
  3312.         }
  3313.     }
  3314.  
  3315.     /* two possibilities int, int or int, String in parameters */
  3316.     public void handleIndexOf2(JVMInvokeInstruction invInst, ThreadInfo th) {
  3317.  
  3318.         StackFrame sf = th.getModifiableTopFrame();
  3319.  
  3320.         StringExpression sym_v1 = null;
  3321.         Expression sym_v2 = null;
  3322.         IntegerExpression intExp = null;
  3323.         sym_v1 = (StringExpression) sf.getOperandAttr(2);
  3324.         intExp = (IntegerExpression) sf.getOperandAttr(0);
  3325.         sym_v2 = (Expression) sf.getOperandAttr(1);
  3326.  
  3327.         if (sym_v1 == null && sym_v2 == null && intExp == null) {
  3328.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleIndexOf2");
  3329.         } else {
  3330.  
  3331.             int i1 = sf.pop();
  3332.             boolean s2char = true;
  3333.             if (sf.isOperandRef()) {
  3334.                 //System.out.println("[handleIndexOf2] string detected");
  3335.                 s2char = false;
  3336.             }
  3337.            
  3338.             int s2 = sf.pop();
  3339.             int s1 = sf.pop();
  3340.  
  3341.             IntegerExpression result = null;
  3342.             if (intExp != null) {
  3343.                 if (sym_v1 != null) {
  3344.                     if (sym_v2 != null) { // both are symbolic values
  3345.                         if (s2char)
  3346.                             result = sym_v1._indexOf((IntegerExpression)sym_v2, intExp);
  3347.                         else
  3348.                             result = sym_v1._indexOf((StringExpression)sym_v2, intExp);
  3349.                     } else { //sym_v2 is null
  3350.                         if (s2char) {
  3351.                             result = sym_v1._indexOf(new IntegerConstant(s2), intExp);
  3352.                         }
  3353.                         else {
  3354.                             ElementInfo e2 = th.getElementInfo(s2);
  3355.                             String val = e2.asString();
  3356.                             result = sym_v1._indexOf(new StringConstant(val), intExp);
  3357.                         }
  3358.                     }
  3359.                 } else { // sym_v1 is null
  3360.                     ElementInfo e1 = th.getElementInfo(s1);
  3361.                     String val = e1.asString();
  3362.  
  3363.                     if (sym_v2 != null) {
  3364.                         if(s2char)
  3365.                             result = new StringConstant(val)._indexOf((IntegerExpression)sym_v2, intExp);
  3366.                         else
  3367.                             result = new StringConstant(val)._indexOf((StringExpression)sym_v2, intExp);
  3368.                     } else {
  3369.                         if (s2char) {
  3370.                             result = new StringConstant(val)._indexOf(new IntegerConstant(s2), intExp);
  3371.                         }
  3372.                         else {
  3373.                             ElementInfo e2 = th.getElementInfo(s2);
  3374.                             String val2 = e2.asString();
  3375.                             result = new StringConstant(val)._indexOf(new StringConstant(val2), intExp);
  3376.                         }
  3377.                     }
  3378.                 }
  3379.             }
  3380.             else { //intExp is null
  3381.                 if (sym_v1 != null) {
  3382.                     if (sym_v2 != null) { // both are symbolic values
  3383.                         if(s2char)
  3384.                             result = sym_v1._indexOf((IntegerExpression)sym_v2, new IntegerConstant(i1));
  3385.                         else
  3386.                             result = sym_v1._indexOf((StringExpression)sym_v2, new IntegerConstant(i1));
  3387.                     } else { //sym_v1 is null
  3388.                         if (s2char) {
  3389.                             result = sym_v1._indexOf(new IntegerConstant(s2), new IntegerConstant(i1));
  3390.                         }
  3391.                         else {
  3392.                             ElementInfo e2 = th.getElementInfo(s2);
  3393.                             String val = e2.asString();
  3394.                             result = sym_v1._indexOf(new StringConstant(val), new IntegerConstant(i1));
  3395.                             //System.out.println("[handleIndexOf2] Special push");
  3396.                             //Special push?
  3397.                             //th.push(s1, true);
  3398.                         }
  3399.                     }
  3400.                 } else {//sym_v1 is null
  3401.                     ElementInfo e1 = th.getElementInfo(s1);
  3402.                     String val = e1.asString();
  3403.  
  3404.                     if (sym_v2 != null) {
  3405.                         if(s2char)
  3406.                             result = new StringConstant(val)._indexOf((IntegerExpression)sym_v2, new IntegerConstant(i1));
  3407.                         else
  3408.                             result = new StringConstant(val)._indexOf((StringExpression)sym_v2, new IntegerConstant(i1));
  3409.                     } else {
  3410.                         if (s2char) {
  3411.                             result = new StringConstant(val)._indexOf(new IntegerConstant(s2), new IntegerConstant(i1));
  3412.                         }
  3413.                         else {
  3414.                             ElementInfo e2 = th.getElementInfo(s2);
  3415.                             String val2 = e2.asString();
  3416.                             result = new StringConstant(val)._indexOf(new StringConstant(val2), new IntegerConstant(i1));
  3417.                         }
  3418.                     }
  3419.                 }
  3420.             }
  3421.             sf.push(0, false);
  3422.             assert result != null;
  3423.             sf.setOperandAttr(result);
  3424.  
  3425.         }
  3426.     }
  3427.    
  3428.     public void handleLastIndexOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  3429.         int numStackSlots = invInst.getArgSize();
  3430.         if (numStackSlots == 2) {
  3431.             handleLastIndexOf1(invInst, th);
  3432.         } else {
  3433.             handleLastIndexOf2(invInst, th);
  3434.         }
  3435.     }
  3436.  
  3437.     public void handleLastIndexOf1(JVMInvokeInstruction invInst, ThreadInfo th) {
  3438.         StackFrame sf = th.getModifiableTopFrame();
  3439.         //boolean castException = false;
  3440.         StringExpression sym_v1 = null;
  3441.         StringExpression sym_v2 = null;
  3442.         sym_v1 = (StringExpression) sf.getOperandAttr(1);
  3443.         /*  */
  3444.         sym_v2 = (StringExpression) sf.getOperandAttr(0);
  3445.         if (sym_v1 == null && sym_v2 == null) {
  3446.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleLastIndexOf1");
  3447.         } else {
  3448.             boolean s1char = true; //argument is char
  3449.             if (sf.isOperandRef()) {
  3450.                 s1char = false; //argument is string
  3451.             }
  3452.             int s1 = sf.pop();
  3453.             int s2 = sf.pop();
  3454.  
  3455.             IntegerExpression result = null;
  3456.                 if (sym_v1 != null) {
  3457.                     if (sym_v2 != null) { // both are symbolic values
  3458.                         result = sym_v1._lastIndexOf(sym_v2);
  3459.                     } else {
  3460.                         if (s1char) {
  3461.                             result = sym_v1._lastIndexOf(new IntegerConstant(s1));
  3462.                         }
  3463.                         else {
  3464.                             ElementInfo e2 = th.getElementInfo(s1);
  3465.                             String val = e2.asString();
  3466.                             result = sym_v1._lastIndexOf(new StringConstant(val));
  3467.                         }
  3468.                     }
  3469.                 } else {//sym_v1 is null
  3470.                     ElementInfo e1 = th.getElementInfo(s2);
  3471.                     String val = e1.asString();
  3472.                     assert(sym_v2!=null);
  3473.                     result = new StringConstant(val)._lastIndexOf(sym_v2);
  3474.                    
  3475.                 }
  3476.            
  3477.             sf.push(0, false);
  3478.             assert result != null;
  3479.             sf.setOperandAttr(result);
  3480.  
  3481.         }
  3482.     }
  3483.  
  3484.     public void handleLastIndexOf2(JVMInvokeInstruction invInst, ThreadInfo th) {
  3485.         StackFrame sf = th.getModifiableTopFrame();
  3486.  
  3487.         StringExpression sym_v1 = null;
  3488.         StringExpression sym_v2 = null;
  3489.         IntegerExpression intExp = null;
  3490.         sym_v1 = (StringExpression) sf.getOperandAttr(2);
  3491.         intExp = (IntegerExpression) sf.getOperandAttr(0);
  3492.         sym_v2 = (StringExpression) sf.getOperandAttr(1);
  3493.  
  3494.         if (sym_v1 == null && sym_v2 == null && intExp == null) {
  3495.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleLastIndexOf2");
  3496.         } else {
  3497.             int i1 = sf.pop();
  3498.             boolean s2char = true;
  3499.             if (th.getModifiableTopFrame().isOperandRef()) {
  3500.                 s2char = false;
  3501.             }
  3502.            
  3503.             int s2 = sf.pop();
  3504.             int s1 = sf.pop();
  3505.  
  3506.             IntegerExpression result = null;
  3507.             if (intExp != null) {
  3508.                 if (sym_v1 != null) {
  3509.                     if (sym_v2 != null) { // both are symbolic values
  3510.                         result = sym_v1._lastIndexOf(sym_v2, intExp);
  3511.                     } else {
  3512.                         if (s2char) {
  3513.                             result = sym_v1._lastIndexOf(new IntegerConstant(s2), intExp);
  3514.                         }
  3515.                         else {
  3516.                             ElementInfo e2 = th.getElementInfo(s2);
  3517.                             String val = e2.asString();
  3518.                             result = sym_v1._lastIndexOf(new StringConstant(val), intExp);
  3519.                         }
  3520.                     }
  3521.                 } else { //sym_v1 is null
  3522.                     ElementInfo e1 = th.getElementInfo(s1);
  3523.                     String val = e1.asString();
  3524.  
  3525.                     if (sym_v2 != null) {
  3526.                         result = new StringConstant(val)._lastIndexOf(sym_v2, intExp);
  3527.                     } else {
  3528.                         if (s2char) {
  3529.                             result = new StringConstant(val)._lastIndexOf(new IntegerConstant(s2), intExp);
  3530.                         }
  3531.                         else {
  3532.                             ElementInfo e2 = th.getElementInfo(s2);
  3533.                             String val2 = e2.asString();
  3534.                             result = new StringConstant(val)._lastIndexOf(new StringConstant(val2), intExp);
  3535.                         }
  3536.                     }
  3537.                 }
  3538.             }
  3539.             else { // intExp is null
  3540.                 if (sym_v1 != null) {
  3541.                     if (sym_v2 != null) { // both are symbolic values
  3542.                         result = sym_v1._lastIndexOf(sym_v2, new IntegerConstant(i1));
  3543.                     } else {
  3544.                         if (s2char) {
  3545.                             result = sym_v1._lastIndexOf(new IntegerConstant(s2), new IntegerConstant(i1));
  3546.                         }
  3547.                         else {
  3548.                             ElementInfo e2 = th.getElementInfo(s2);
  3549.                             String val = e2.asString();
  3550.                             result = sym_v1._lastIndexOf(new StringConstant(val), new IntegerConstant(i1));
  3551.                             //System.out.println("[handleIndexOf2] Special push");
  3552.                             //Special push?
  3553.                             //th.push(s1, true);
  3554.                         }
  3555.                     }
  3556.                 } else { // sym_v1 is null
  3557.                     ElementInfo e1 = th.getElementInfo(s1);
  3558.                     String val = e1.asString();
  3559.                     assert(sym_v2!=null);
  3560.                     result = new StringConstant(val)._lastIndexOf(sym_v2, new IntegerConstant(i1));
  3561.                 }
  3562.             }
  3563.            
  3564.             sf.push(0, false);
  3565.             assert result != null;
  3566.             sf.setOperandAttr(result);
  3567.  
  3568.         }
  3569.     }
  3570.  
  3571.  
  3572.    
  3573.  
  3574.     public void handlebooleanValue(JVMInvokeInstruction invInst, SystemState ss, ThreadInfo th) {
  3575.         StackFrame sf = th.getModifiableTopFrame();
  3576.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  3577.  
  3578.         if (sym_v3 == null) {
  3579.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandlebooleanValue");
  3580.         } else {
  3581.             if (sym_v3 instanceof IntegerExpression) {
  3582.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  3583.                 sf.pop();
  3584.                 sf.push(0, false);
  3585.                 sf.setOperandAttr(sym_v2);
  3586.             } else {
  3587.                 throw new RuntimeException("ERROR: operand type not tackled - booleanValue");
  3588.             }
  3589.  
  3590.         }
  3591.  
  3592.     }
  3593.  
  3594.     public void handleintValue(JVMInvokeInstruction invInst,  ThreadInfo th) {
  3595.         StackFrame sf = th.getModifiableTopFrame();
  3596.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  3597.  
  3598.         if (sym_v3 == null) {
  3599.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleintValue");
  3600.         } else {
  3601.             if (sym_v3 instanceof IntegerExpression) {
  3602.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  3603.                 sf.pop();
  3604.                 sf.push(0, false);
  3605.                 sf.setOperandAttr(sym_v2);
  3606.             } else {
  3607.                 th.printStackTrace();
  3608.                 throw new RuntimeException("ERROR: operand type not tackled - intValue");
  3609.             }
  3610.         }
  3611.     }
  3612.  
  3613.     public void handlelongValue(JVMInvokeInstruction invInst,  ThreadInfo th) {
  3614.         StackFrame sf = th.getModifiableTopFrame();
  3615.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  3616.  
  3617.         if (sym_v3 == null) {
  3618.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: hanldeLongValue");
  3619.         } else {
  3620.             if (sym_v3 instanceof IntegerExpression) {
  3621.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  3622.                 sf.pop();
  3623.                 sf.pushLong((long) 0);
  3624.                 sf.setLongOperandAttr(sym_v2);
  3625.             } else {
  3626.                 throw new RuntimeException("ERROR: operand type not tackled - longValue");
  3627.             }
  3628.  
  3629.         }
  3630.  
  3631.     }
  3632.  
  3633.     public void handlefloatValue(JVMInvokeInstruction invInst,  ThreadInfo th) {
  3634.         StackFrame sf = th.getModifiableTopFrame();
  3635.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  3636.  
  3637.         if (sym_v3 == null) {
  3638.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand: hanldeFloatValue");
  3639.         } else {
  3640.             if (sym_v3 instanceof RealExpression) {
  3641.                 RealExpression sym_v2 = (RealExpression) sym_v3;
  3642.                 sf.pop();
  3643.                 sf.push(0, false);
  3644.                 sf.setOperandAttr(sym_v2);
  3645.             } else {
  3646.                 throw new RuntimeException("ERROR: operand type not tackled - floatValue");
  3647.             }
  3648.  
  3649.         }
  3650.  
  3651.     }
  3652.  
  3653.     public void handledoubleValue(JVMInvokeInstruction invInst,  ThreadInfo th) {
  3654.         StackFrame sf = th.getModifiableTopFrame();
  3655.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  3656.  
  3657.         if (sym_v3 == null) {
  3658.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand: hanldeDoubleValue");
  3659.         } else {
  3660.             if (sym_v3 instanceof RealExpression) {
  3661.                 RealExpression sym_v2 = (RealExpression) sym_v3;
  3662.                 sf.pop();
  3663.                 sf.pushLong((long) 0);
  3664.                 sf.setLongOperandAttr(sym_v2);
  3665.             } else {
  3666.                 throw new RuntimeException("ERROR: operand type not tackled - doubleValue");
  3667.             }
  3668.  
  3669.         }
  3670.  
  3671.     }
  3672.  
  3673.     /*
  3674.      * StringBuilder or StringBuffer or BigDecimal initiation with symbolic
  3675.      * primitives
  3676.      */
  3677.  
  3678.     public Instruction handleInit(JVMInvokeInstruction invInst,  ThreadInfo th) {
  3679.  
  3680.         String cname = invInst.getInvokedMethodClassName();
  3681.         if (cname.equals("java.lang.StringBuilder") || cname.equals("java.lang.StringBuffer")) {
  3682.             StackFrame sf = th.getModifiableTopFrame();
  3683.             StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  3684.             SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  3685.             if (sym_v1 == null) {
  3686.                 throw new RuntimeException("ERROR: symbolic StringBuilder method must have one symbolic operand in Init");
  3687.             } else {
  3688.                 sf.pop(); /* string object */
  3689.                 sf.pop(); /* one stringBuilder Object */
  3690.                 sym_v2.putstr(sym_v1);
  3691.                 sf.setOperandAttr(sym_v2);
  3692.                 return invInst.getNext();
  3693.             }
  3694.         } else {
  3695.             // Corina TODO: we should allow symbolic string analysis to kick in only when desired
  3696.             //throw new RuntimeException("Warning Symbolic String Analysis: Initialization type not handled in symbc/bytecode/SymbolicStringHandler init");
  3697.             return null;
  3698.         }
  3699.     }
  3700.  
  3701.     /***************************** Symbolic Big Decimal Routines end ****************/
  3702.  
  3703.  
  3704.     private void handleBooleanStringInstructions(JVMInvokeInstruction invInst,  ThreadInfo th, StringComparator comp) {
  3705.         StackFrame sf = th.getModifiableTopFrame();
  3706.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  3707.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  3708.  
  3709.         if ((sym_v1 == null) & (sym_v2 == null)) {
  3710.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleStartsWith");
  3711.         } else {
  3712.             ChoiceGenerator<?> cg;
  3713.             boolean conditionValue;
  3714.  
  3715.             cg = th.getVM().getChoiceGenerator();
  3716.             assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  3717.             conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  3718.  
  3719.             // System.out.println("conditionValue: " + conditionValue);
  3720.  
  3721.             int s1 = sf.pop();
  3722.             int s2 = sf.pop();
  3723.             PathCondition pc;
  3724.  
  3725.             // pc is updated with the pc stored in the choice generator above
  3726.             // get the path condition from the
  3727.             // previous choice generator of the same type
  3728.  
  3729.             ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  3730.             while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  3731.                 prev_cg = prev_cg.getPreviousChoiceGenerator();
  3732.             }
  3733.  
  3734.             if (prev_cg == null) {
  3735.                 pc = new PathCondition();
  3736.             } else {
  3737.                 pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  3738.             }
  3739.  
  3740.             assert pc != null;
  3741.  
  3742.             if (conditionValue) {
  3743.                 if (sym_v1 != null) {
  3744.                     if (sym_v2 != null) { // both are symbolic values
  3745.                         pc.spc._addDet(comp, sym_v1, sym_v2);
  3746.                     } else {
  3747.                         ElementInfo e2 = th.getElementInfo(s2);
  3748.                         String val = e2.asString();
  3749.                         pc.spc._addDet(comp, sym_v1, val);
  3750.                     }
  3751.                 } else {
  3752.                     ElementInfo e1 = th.getElementInfo(s1);
  3753.                     String val = e1.asString();
  3754.                     pc.spc._addDet(comp, val, sym_v2);
  3755.                 }
  3756.                 if (!pc.simplify()) {// not satisfiable
  3757.                     th.getVM().getSystemState().setIgnored(true);
  3758.                 } else {
  3759.                     // pc.solve();
  3760.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  3761.                     // System.out.println(((PCChoiceGenerator) cg).getCurrentPC());
  3762.                 }
  3763.             } else {
  3764.                 if (sym_v1 != null) {
  3765.                     if (sym_v2 != null) { // both are symbolic values
  3766.                         pc.spc._addDet(comp.not(), sym_v1, sym_v2);
  3767.                     } else {
  3768.                         ElementInfo e2 = th.getElementInfo(s2);
  3769.                         String val = e2.asString();
  3770.                         pc.spc._addDet(comp.not(), sym_v1, val);
  3771.  
  3772.                     }
  3773.                 } else {
  3774.                     ElementInfo e1 = th.getElementInfo(s1);
  3775.                     String val = e1.asString();
  3776.                     pc.spc._addDet(comp.not(), val, sym_v2);
  3777.                 }
  3778.                 if (!pc.simplify()) {// not satisfiable
  3779.                     th.getVM().getSystemState().setIgnored(true);
  3780.                 } else {
  3781.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  3782.                 }
  3783.             }
  3784.  
  3785.             sf.push(conditionValue ? 1 : 0, true);
  3786.  
  3787.         }
  3788.  
  3789.     }
  3790.  
  3791.     public void handleEqualsIgnoreCase(JVMInvokeInstruction invInst,  ThreadInfo th) {
  3792.         throw new RuntimeException("ERROR: symbolic string method not Implemented - EqualsIgnoreCase");
  3793.     }
  3794.  
  3795.     public void handleEndsWith(JVMInvokeInstruction invInst,  ThreadInfo th) {
  3796.         //throw new RuntimeException("ERROR: symbolic string method not Implemented - EndsWith");
  3797.         handleBooleanStringInstructions(invInst,  th, StringComparator.ENDSWITH);
  3798.     }
  3799.  
  3800.     public void handleContains (JVMInvokeInstruction invInst,  ThreadInfo th) {
  3801.         handleBooleanStringInstructions(invInst,  th, StringComparator.CONTAINS);
  3802.     }
  3803.  
  3804.  
  3805.     public void handleStartsWith(JVMInvokeInstruction invInst,  ThreadInfo th) {
  3806.         //throw new RuntimeException("ERROR: symbolic string method not Implemented - StartsWith");
  3807.         handleBooleanStringInstructions(invInst, th, StringComparator.STARTSWITH);
  3808.     }
  3809.  
  3810.     //Only supports character for character
  3811.     public Instruction handleReplace(JVMInvokeInstruction invInst, ThreadInfo th) {
  3812.         StackFrame sf = th.getModifiableTopFrame();
  3813.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  3814.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  3815.         StringExpression sym_v3 = (StringExpression) sf.getOperandAttr(2);
  3816.  
  3817.         if ((sym_v1 == null) & (sym_v2 == null) & (sym_v3 == null)) {
  3818.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleReplace");
  3819.         } else {
  3820.             int s1 = sf.pop();
  3821.             int s2 = sf.pop();
  3822.             int s3 = sf.pop();
  3823.             //System.out.println("[handleReplace] " + s1 + " " + s2 + " " + s3);
  3824.             StringExpression result = null;
  3825.             if (sym_v1 == null) { // operand 0 is concrete
  3826.                 //ElementInfo e1 = th.getElementInfo(s1);
  3827.                 String val = String.valueOf((char) s1);
  3828.                 if (sym_v2 == null) { // sym_v3 has to be symbolic
  3829.                     //ElementInfo e2 = th.getElementInfo(s2);
  3830.                     //String val1 = e2.asString();
  3831.                     result = sym_v3._replace(val, String.valueOf((char)s2));
  3832.                 } else {
  3833.                     if (sym_v3 == null) { // only sym_v2 is symbolic
  3834.                         ElementInfo e3 = th.getElementInfo(s3);
  3835.                         String val2 = e3.asString();
  3836.                         sym_v3 = new StringConstant(val2);
  3837.                         result = sym_v3._replace(val, sym_v2);
  3838.                     } else {
  3839.                         result = sym_v3._replace(val, sym_v2);
  3840.                     }
  3841.                 }
  3842.             } else { // sym_v1 is symbolic
  3843.                 if (sym_v2 == null) {
  3844.                     if (sym_v3 == null) {
  3845.                         //ElementInfo e2 = th.getElementInfo(s2);
  3846.                         String val1 = String.valueOf((char) s2);
  3847.                         //ElementInfo e3 = th.getElementInfo(s3);
  3848.                         String val2 = String.valueOf((char) s3);
  3849.                         sym_v3 = new StringConstant(val2);
  3850.                         result = sym_v3._replace(sym_v1, val1);
  3851.                     } else {
  3852.                         //ElementInfo e2 = th.getElementInfo(s2);
  3853.                         String val1 = String.valueOf((char) s2);
  3854.                         result = sym_v3._replace(sym_v1, val1);
  3855.                     }
  3856.                 } else {
  3857.                     if (sym_v3 == null) {
  3858.                         ElementInfo e3 = th.getElementInfo(s3);
  3859.                         String val2 = e3.asString();
  3860.                         sym_v3 = new StringConstant(val2);
  3861.                         result = sym_v3._replace(sym_v1, sym_v2);
  3862.                     } else {
  3863.                         result = sym_v3._replace(sym_v1, sym_v2);
  3864.                     }
  3865.                 }
  3866.             }
  3867.             ElementInfo objRef = th.getHeap().newString("", th); /*
  3868.                                                                                                                                      * dummy
  3869.                                                                                                                                      * String
  3870.                                                                                                                                      * Object
  3871.                                                                                                                                      */
  3872.             sf.push(objRef.getObjectRef(), true);
  3873.             sf.setOperandAttr(result);
  3874.         }
  3875.         return null;
  3876.     }
  3877.  
  3878.     public Instruction handleSubString(JVMInvokeInstruction invInst, ThreadInfo th) {
  3879.         int numStackSlots = invInst.getArgSize();
  3880.         if (numStackSlots == 2) {
  3881.             return handleSubString1(invInst, th);
  3882.         } else {
  3883.             return handleSubString2(invInst, th);
  3884.         }
  3885.     }
  3886.  
  3887.     public Instruction handleSubString1(JVMInvokeInstruction invInst, ThreadInfo th) {
  3888.         StackFrame sf = th.getModifiableTopFrame();
  3889.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  3890.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  3891.  
  3892.         if ((sym_v1 == null) & (sym_v2 == null)) {
  3893.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleSubString1");
  3894.         } else {
  3895.             int s1 = sf.pop();
  3896.             int s2 = sf.pop();
  3897.  
  3898.             StringExpression result = null;
  3899.             if (sym_v1 == null) { // operand 0 is concrete
  3900.                 int val = s1;
  3901.                 result = sym_v2._subString(val);
  3902.             } else {
  3903.                 if (sym_v2 == null) {
  3904.                     ElementInfo e1 = th.getElementInfo(s2);
  3905.                     String val2 = e1.asString();
  3906.                     sym_v2 = new StringConstant(val2);
  3907.                     result = sym_v2._subString(sym_v1);
  3908.                 } else {
  3909.                     result = sym_v2._subString(sym_v1);
  3910.                 }
  3911.             }
  3912.             ElementInfo objRef = th.getHeap().newString("", th); /*
  3913.                                                                                                                                      * dummy
  3914.                                                                                                                                      * String
  3915.                                                                                                                                      * Object
  3916.                                                                                                                                      */
  3917.             sf.push(objRef.getObjectRef(), true);
  3918.             sf.setOperandAttr(result);
  3919.         }
  3920.         return null;
  3921.     }
  3922.  
  3923.     public Instruction handleSubString2(JVMInvokeInstruction invInst, ThreadInfo th) {
  3924.         //System.out.println("[SymbolicStringHandler] doing");
  3925.         StackFrame sf = th.getModifiableTopFrame();
  3926.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  3927.         IntegerExpression sym_v2 = (IntegerExpression) sf.getOperandAttr(1);
  3928.         StringExpression sym_v3 = (StringExpression) sf.getOperandAttr(2);
  3929.  
  3930.         if ((sym_v1 == null) & (sym_v2 == null) & (sym_v3 == null)) {
  3931.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleSubString2");
  3932.         } else {
  3933.             int s1 = sf.pop();
  3934.             int s2 = sf.pop();
  3935.             int s3 = sf.pop();
  3936.             //System.out.printf("[SymbolicStringHandler] popped %d %d %d\n", s1, s2, s3);
  3937.             StringExpression result = null;
  3938.             if (sym_v1 == null) { // operand 0 is concrete
  3939.                 int val = s1;
  3940.                 if (sym_v2 == null) { // sym_v3 has to be symbolic
  3941.                     int val1 = s2;
  3942.                     result = sym_v3._subString(val, val1);
  3943.                     //System.out.println("[SymbolicStringHandler] special push");
  3944.                     /* Only if both arguments are concrete, something else needs
  3945.                      * to be pushed?
  3946.                      */
  3947.                     //sf.push(s3, true); /* symbolic string element */
  3948.                 } else {
  3949.                     if (sym_v3 == null) { // only sym_v2 is symbolic
  3950.                         ElementInfo e3 = th.getElementInfo(s3);
  3951.                         String val2 = e3.asString();
  3952.                         sym_v3 = new StringConstant(val2);
  3953.                         result = sym_v3._subString(val, sym_v2);
  3954.                     } else {
  3955.                         result = sym_v3._subString(val, sym_v2);
  3956.                     }
  3957.                 }
  3958.             } else { // sym_v1 is symbolic
  3959.                 if (sym_v2 == null) {
  3960.                     if (sym_v3 == null) {
  3961.                         int val1 = s2;
  3962.                         ElementInfo e3 = th.getElementInfo(s3);
  3963.                         String val2 = e3.asString();
  3964.                         sym_v3 = new StringConstant(val2);
  3965.                         result = sym_v3._subString(sym_v1, val1);
  3966.                     } else {
  3967.                         int val1 = s2;
  3968.                         result = sym_v3._subString(sym_v1, val1);
  3969.                     }
  3970.                 } else {
  3971.                     if (sym_v3 == null) {
  3972.                         ElementInfo e3 = th.getElementInfo(s3);
  3973.                         String val2 = e3.asString();
  3974.                         sym_v3 = new StringConstant(val2);
  3975.                         result = sym_v3._subString(sym_v1, sym_v2);
  3976.                     } else {
  3977.                         result = sym_v3._subString(sym_v1, sym_v2);
  3978.                     }
  3979.                 }
  3980.             }
  3981.             ElementInfo objRef = th.getHeap().newString("", th);
  3982.             //System.out.println("[SymbolicStringHandler] " + sf.toString());
  3983.             sf.push(objRef.getObjectRef(), true);
  3984.             //System.out.println("[SymbolicStringHandler] " + sf.toString());
  3985.             sf.setOperandAttr(result);
  3986.         }
  3987.  
  3988.         return null;
  3989.     }
  3990.  
  3991.     public Instruction handleReplaceFirst(JVMInvokeInstruction invInst, ThreadInfo th) {
  3992.         StackFrame sf = th.getModifiableTopFrame();
  3993.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  3994.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  3995.         StringExpression sym_v3 = (StringExpression) sf.getOperandAttr(2);
  3996.  
  3997.         if ((sym_v1 == null) & (sym_v2 == null) & (sym_v3 == null)) {
  3998.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HanldeReplaceFirst");
  3999.         } else {
  4000.             int s1 = sf.pop();
  4001.             int s2 = sf.pop();
  4002.             int s3 = sf.pop();
  4003.  
  4004.             StringExpression result = null;
  4005.             if (sym_v1 == null) { // operand 0 is concrete
  4006.                 ElementInfo e1 = th.getElementInfo(s1);
  4007.                 String val = e1.asString();
  4008.                 if (sym_v2 == null) { // sym_v3 has to be symbolic
  4009.                     ElementInfo e2 = th.getElementInfo(s2);
  4010.                     String val1 = e2.asString();
  4011.                     result = sym_v3._replaceFirst(val, val1);
  4012.  
  4013.                 } else {
  4014.                     if (sym_v3 == null) { // only sym_v2 is symbolic
  4015.                         ElementInfo e3 = th.getElementInfo(s3);
  4016.                         String val2 = e3.asString();
  4017.                         sym_v3 = new StringConstant(val2);
  4018.                         result = sym_v3._replaceFirst(val, sym_v2);
  4019.                     } else {
  4020.                         result = sym_v3._replaceFirst(val, sym_v2);
  4021.                     }
  4022.                 }
  4023.             } else { // sym_v1 is symbolic
  4024.                 if (sym_v2 == null) {
  4025.                     if (sym_v3 == null) {
  4026.                         ElementInfo e2 = th.getElementInfo(s2);
  4027.                         String val1 = e2.asString();
  4028.                         ElementInfo e3 = th.getElementInfo(s3);
  4029.                         String val2 = e3.asString();
  4030.                         sym_v3 = new StringConstant(val2);
  4031.                         result = sym_v3._replaceFirst(sym_v1, val1);
  4032.                     } else {
  4033.                         ElementInfo e2 = th.getElementInfo(s2);
  4034.                         String val1 = e2.asString();
  4035.                         result = sym_v3._replaceFirst(sym_v1, val1);
  4036.                     }
  4037.                 } else {
  4038.                     if (sym_v3 == null) {
  4039.                         ElementInfo e3 = th.getElementInfo(s3);
  4040.                         String val2 = e3.asString();
  4041.                         sym_v3 = new StringConstant(val2);
  4042.                         result = sym_v3._replaceFirst(sym_v1, sym_v2);
  4043.                     } else {
  4044.                         result = sym_v3._replaceFirst(sym_v1, sym_v2);
  4045.                     }
  4046.                 }
  4047.             }
  4048.             ElementInfo objRef = th.getHeap().newString("", th); /*
  4049.                                                                                                                                      * dummy
  4050.                                                                                                                                      * String
  4051.                                                                                                                                      * Object
  4052.                                                                                                                                      */
  4053.             sf.push(objRef.getObjectRef(), true);
  4054.             sf.setOperandAttr(result);
  4055.         }
  4056.         return null;
  4057.     }
  4058.  
  4059.     public void handleTrim(JVMInvokeInstruction invInst, ThreadInfo th) {
  4060.         // throw new RuntimeException("ERROR: symbolic string method not Implemented - Trim");
  4061.         StackFrame sf = th.getModifiableTopFrame();
  4062.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  4063.         int s1 = sf.pop();
  4064.  
  4065.         if (sym_v1 == null) {
  4066.             ElementInfo e1 = th.getElementInfo(s1);
  4067.             String val1 = e1.asString();
  4068.             sym_v1 = new StringConstant(val1);
  4069.         }
  4070.         StringExpression result = sym_v1._trim();
  4071.  
  4072.         ElementInfo  objRef = th.getHeap().newString("", th); /*
  4073.                                                                                                                                  * dummy String
  4074.                                                                                                                                  * Object
  4075.                                                                                                                                  */
  4076.         sf.push(objRef.getObjectRef(), true);
  4077.         sf.setOperandAttr(result);
  4078.     }
  4079.  
  4080.     public Instruction handleValueOf(JVMInvokeInstruction invInst,  ThreadInfo th) {
  4081.         MethodInfo mi = invInst.getInvokedMethod(th);
  4082.         String cname = invInst.getInvokedMethodClassName();
  4083.         String[] argTypes = mi.getArgumentTypeNames();
  4084.         if (cname.equals("java.lang.String")) {
  4085.             // System.out.println(argTypes[0]);
  4086.             if (argTypes[0].equals("int")) {
  4087.                 return handleIntValueOf(invInst,  th);
  4088.             } else if (argTypes[0].equals("float")) {
  4089.                 return handleFloatValueOf(invInst, th);
  4090.             } else if (argTypes[0].equals("long")) {
  4091.                 return handleLongValueOf(invInst, th);
  4092.             } else if (argTypes[0].equals("double")) {
  4093.                 return handleDoubleValueOf(invInst, th);
  4094.             } else if (argTypes[0].equals("char")) {
  4095.                 return handleCharValueOf(invInst, th);
  4096.             } else if (argTypes[0].equals("chararray")) {
  4097.                 return handleCharArrayValueOf(invInst, th);
  4098.             } else if (argTypes[0].equals("boolean")) {
  4099.                 return handleBooleanValueOf(invInst, th);
  4100.             } else if (argTypes[0].equals("java.lang.Object")) {
  4101.                 return handleObjectValueOf(invInst, th);
  4102.             } else {
  4103.                 throw new RuntimeException("ERROR: Input parameter type not handled in Symbolic String ValueOf");
  4104.             }
  4105.         } else { // value of non-string types
  4106.             if (cname.equals("java.lang.Integer")) {
  4107.                 if (!(argTypes[0].equals("int"))) { // converting String to Integer
  4108.                     ChoiceGenerator<?> cg;
  4109.                     if (!th.isFirstStepInsn()) { // first time around
  4110.                         cg = new PCChoiceGenerator(2);
  4111.                         th.getVM().setNextChoiceGenerator(cg);
  4112.                         return invInst;
  4113.                     } else {
  4114.                         handleParseIntValueOf(invInst, th);
  4115.                     }
  4116.                 } else { // converting int to Integer
  4117.                     handleParseIntValueOf(invInst,  th);
  4118.                 }
  4119.             } else if (cname.equals("java.lang.Float")) {
  4120.                 if (!(argTypes[0].equals("float"))) { // converting String to Float
  4121.                     ChoiceGenerator<?> cg;
  4122.                     if (!th.isFirstStepInsn()) { // first time around
  4123.                         cg = new PCChoiceGenerator(2);
  4124.                         th.getVM().setNextChoiceGenerator(cg);
  4125.                         return invInst;
  4126.                     } else {
  4127.                         handleParseFloatValueOf(invInst, th);
  4128.                     }
  4129.                 } else { // converting int to Integer
  4130.                     handleParseFloatValueOf(invInst, th);
  4131.                 }
  4132.             } else if (cname.equals("java.lang.Long")) {
  4133.                 if (!(argTypes[0].equals("long"))) { // converting String to Long
  4134.                     ChoiceGenerator<?> cg;
  4135.                     if (!th.isFirstStepInsn()) { // first time around
  4136.                         cg = new PCChoiceGenerator(2);
  4137.                         th.getVM().setNextChoiceGenerator(cg);
  4138.                         return invInst;
  4139.                     } else {
  4140.                         handleParseLongValueOf(invInst, th);
  4141.                     }
  4142.                 } else { // converting int to Integer
  4143.                     handleParseLongValueOf(invInst, th);
  4144.                 }
  4145.             } else if (cname.equals("java.lang.Double")) {
  4146.                 if (!(argTypes[0].equals("double"))) { // converting String to Double
  4147.                     ChoiceGenerator<?> cg;
  4148.                     if (!th.isFirstStepInsn()) { // first time around
  4149.                         cg = new PCChoiceGenerator(2);
  4150.                         th.getVM().getSystemState().setNextChoiceGenerator(cg);
  4151.                         return invInst;
  4152.                     } else {
  4153.                         handleParseDoubleValueOf(invInst, th);
  4154.                     }
  4155.                 } else { // converting int to Integer
  4156.                     handleParseLongValueOf(invInst, th);
  4157.                 }
  4158.             } else if (cname.equals("java.lang.Boolean")) {
  4159.                 if (!(argTypes[0].equals("boolean"))) { // converting String to Boolean
  4160.                     ChoiceGenerator<?> cg;
  4161.                     if (!th.isFirstStepInsn()) { // first time around
  4162.                         cg = new PCChoiceGenerator(2);
  4163.                         th.getVM().setNextChoiceGenerator(cg);
  4164.                         return invInst;
  4165.                     } else {
  4166.                         handleParseBooleanValueOf(invInst, th);
  4167.                     }
  4168.                 } else { // converting int to Integer
  4169.                     handleParseBooleanValueOf(invInst, th);
  4170.                 }
  4171.             } else {
  4172.                 throw new RuntimeException("ERROR: Type not handled in Symbolic Type ValueOf: " + cname);
  4173.             }
  4174.         }
  4175.         return null;
  4176.     }
  4177.     public void handleIsEmpty(JVMInvokeInstruction invInst,  ThreadInfo th) {
  4178.         StackFrame sf = th.getModifiableTopFrame();
  4179.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  4180.         if (sym_v1 == null) {
  4181.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleIsEmpty");
  4182.         } else {
  4183.             IntegerExpression sym_v2 = sym_v1._length();
  4184.             ChoiceGenerator<?> cg;
  4185.             boolean conditionValue;
  4186.             cg = th.getVM().getChoiceGenerator();
  4187.  
  4188.             assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4189.             conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4190.  
  4191.             sf.pop();
  4192.             PathCondition pc;
  4193.  
  4194.             ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4195.             while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4196.                 prev_cg = prev_cg.getPreviousChoiceGenerator();
  4197.             }
  4198.  
  4199.             if (prev_cg == null) {
  4200.                 pc = new PathCondition();
  4201.             } else {
  4202.                 pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4203.             }
  4204.  
  4205.             assert pc != null;
  4206.  
  4207.             if(conditionValue){
  4208.                 pc._addDet(Comparator.EQ, sym_v2, (IntegerExpression)(new IntegerConstant(0)));
  4209.                 if(!pc.simplify()) {
  4210.                     th.getVM().getSystemState().setIgnored(true);
  4211.                 } else {
  4212.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4213.                 }
  4214.             }else{
  4215.                 pc._addDet(Comparator.NE, sym_v2, (IntegerExpression)(new IntegerConstant(0)));
  4216.                 if(!pc.simplify()) {
  4217.                     th.getVM().getSystemState().setIgnored(true);
  4218.                 } else {
  4219.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4220.                 }
  4221.             }
  4222.  
  4223.             sf.push(conditionValue ? 1 : 0, true);
  4224.         }
  4225.     }
  4226.  
  4227.     public void handleParseLongValueOf(JVMInvokeInstruction invInst,  ThreadInfo th) {
  4228.         StackFrame sf = th.getModifiableTopFrame();
  4229.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  4230.  
  4231.         if (sym_v3 == null) {
  4232.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  4233.         } else {
  4234.             if (sym_v3 instanceof IntegerExpression) {
  4235.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  4236.                 sf.popLong();
  4237.                 int objRef = getNewObjRef(invInst, th); /* dummy Long Object */
  4238.                 sf.push(objRef, true);
  4239.                 sf.setOperandAttr(sym_v2);
  4240.             } else {
  4241.                 IntegerExpression result = null;
  4242.                 ChoiceGenerator<?> cg;
  4243.                 boolean conditionValue;
  4244.                 cg = th.getVM().getChoiceGenerator();
  4245.  
  4246.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4247.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4248.  
  4249.                 sf.pop();
  4250.                 PathCondition pc;
  4251.  
  4252.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4253.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4254.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  4255.                 }
  4256.  
  4257.                 if (prev_cg == null)
  4258.                     pc = new PathCondition();
  4259.                 else
  4260.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4261.  
  4262.                 assert pc != null;
  4263.  
  4264.                 if (conditionValue) {
  4265.                     pc.spc._addDet(StringComparator.ISLONG, (StringExpression) sym_v3);
  4266.                     if (!pc.simplify()) {// not satisfiable
  4267.                         th.getVM().getSystemState().setIgnored(true);
  4268.                     } else {
  4269.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4270.                         result = ((StringExpression) sym_v3)._IvalueOf();
  4271.                         sf = th.getModifiableTopFrame();
  4272.                         int objRef = getNewObjRef(invInst, th); /* dummy Long Object */
  4273.                         sf.push(objRef, true);
  4274.                         sf.setOperandAttr(result);
  4275.                     }
  4276.                 } else {
  4277.                     pc.spc._addDet(StringComparator.NOTLONG, (StringExpression) sym_v3);
  4278.                     if (!pc.simplify()) {// not satisfiable
  4279.                         th.getVM().getSystemState().setIgnored(true);
  4280.                     } else {
  4281.                         throw new RuntimeException("ERROR: Long Format Type Exception");
  4282.                         //th.getVM().getSystemState().setIgnored(true); TODO: needs revision
  4283.                         //sf.push(0, true);
  4284.                     }
  4285.                 }
  4286.             }
  4287.         }
  4288.     }
  4289.  
  4290.     public void handleParseBooleanValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4291.         StackFrame sf = th.getModifiableTopFrame();
  4292.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  4293.  
  4294.         if (sym_v3 == null) {
  4295.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  4296.         } else {
  4297.             if (sym_v3 instanceof IntegerExpression) {
  4298.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  4299.                 sf.pop();
  4300.                 int objRef = getNewObjRef(invInst, th); /* dummy Boolean Object */
  4301.                 sf.push(objRef, true);
  4302.                 sf.setOperandAttr(sym_v2);
  4303.             } else {
  4304.                 IntegerExpression result = null;
  4305.                 ChoiceGenerator<?> cg;
  4306.                 boolean conditionValue;
  4307.                 cg = th.getVM().getChoiceGenerator();
  4308.  
  4309.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4310.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4311.  
  4312.                 sf.pop();
  4313.                 PathCondition pc;
  4314.  
  4315.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4316.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4317.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  4318.                 }
  4319.  
  4320.                 if (prev_cg == null)
  4321.                     pc = new PathCondition();
  4322.                 else
  4323.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4324.  
  4325.                 assert pc != null;
  4326.  
  4327.                 if (conditionValue) {
  4328.                     pc.spc._addDet(StringComparator.ISBOOLEAN, (StringExpression) sym_v3);
  4329.                     if (!pc.simplify()) {// not satisfiable
  4330.                         th.getVM().getSystemState().setIgnored(true);
  4331.                     } else {
  4332.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4333.                         result = ((StringExpression) sym_v3)._IvalueOf();
  4334.                         sf = th.getModifiableTopFrame();
  4335.                         int objRef = getNewObjRef(invInst, th); /* dummy Boolean Object */
  4336.                         sf.push(objRef, true);
  4337.                         sf.setOperandAttr(result);
  4338.                     }
  4339.                 } else {
  4340.                     pc.spc._addDet(StringComparator.NOTBOOLEAN, (StringExpression) sym_v3);
  4341.                     if (!pc.simplify()) {// not satisfiable
  4342.                         th.getVM().getSystemState().setIgnored(true);
  4343.                     } else {
  4344.                         throw new RuntimeException("ERROR: Boolean Format Type Exception");
  4345.                         // TODO: to review; there should be no backtracking here
  4346.                         //th.getVM().getSystemState().setIgnored(true);
  4347.                         //sf.push(0, true);
  4348.                     }
  4349.                 }
  4350.             }
  4351.         }
  4352.     }
  4353.  
  4354.     public void handleParseIntValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4355.         StackFrame sf = th.getModifiableTopFrame();
  4356.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  4357.  
  4358.         if (sym_v3 == null) {
  4359.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  4360.         } else {
  4361.             if (sym_v3 instanceof IntegerExpression) {
  4362.                 IntegerExpression sym_v2 = (IntegerExpression) sym_v3;
  4363.                 sf.pop();
  4364.                 int objRef = getNewObjRef(invInst, th); /* dummy Integer Object */
  4365.                 sf.push(objRef, true);
  4366.                 sf.setOperandAttr(sym_v2);
  4367.             } else {
  4368.                 IntegerExpression result = null;
  4369.                 ChoiceGenerator<?> cg;
  4370.                 boolean conditionValue;
  4371.                 cg = th.getVM().getChoiceGenerator();
  4372.  
  4373.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4374.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4375.  
  4376.                 sf.pop();
  4377.                 PathCondition pc;
  4378.  
  4379.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4380.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4381.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  4382.                 }
  4383.  
  4384.                 if (prev_cg == null)
  4385.                     pc = new PathCondition();
  4386.                 else
  4387.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4388.  
  4389.                 assert pc != null;
  4390.  
  4391.                 if (conditionValue) {
  4392.                     pc.spc._addDet(StringComparator.ISINTEGER, (StringExpression) sym_v3);
  4393.                     if (!pc.simplify()) {// not satisfiable
  4394.                         th.getVM().getSystemState().setIgnored(true);
  4395.                     } else {
  4396.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4397.                         result = ((StringExpression) sym_v3)._IvalueOf();
  4398.                         sf = th.getModifiableTopFrame();
  4399.                         int objRef = getNewObjRef(invInst, th); /* dummy Integer Object */
  4400.                         sf.push(objRef, true);
  4401.                         sf.setOperandAttr(result);
  4402.                     }
  4403.                 } else {
  4404.                     pc.spc._addDet(StringComparator.NOTINTEGER, (StringExpression) sym_v3);
  4405.                     if (!pc.simplify()) {// not satisfiable
  4406.                         th.getVM().getSystemState().setIgnored(true);
  4407.                     } else {
  4408.                         throw new RuntimeException("ERROR: Integer Format Type Exception");
  4409.                         //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  4410.                         //sf.push(0, true);
  4411.                     }
  4412.                 }
  4413.             }
  4414.         }
  4415.     }
  4416.  
  4417.     public void handleParseInt(JVMInvokeInstruction invInst, ThreadInfo th) {
  4418.         StackFrame sf = th.getModifiableTopFrame();
  4419.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  4420.  
  4421.         if (sym_v3 == null) {
  4422.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  4423.         } else {
  4424.             IntegerExpression result = null;
  4425.             ChoiceGenerator<?> cg;
  4426.             boolean conditionValue;
  4427.             cg = th.getVM().getChoiceGenerator();
  4428.  
  4429.             assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4430.             conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4431.  
  4432.             sf.pop();
  4433.             PathCondition pc;
  4434.             ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4435.             while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4436.                 prev_cg = prev_cg.getPreviousChoiceGenerator();
  4437.             }
  4438.  
  4439.             if (prev_cg == null)
  4440.                 pc = new PathCondition();
  4441.             else
  4442.                 pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4443.  
  4444.             assert pc != null;
  4445.  
  4446.             if (conditionValue) {
  4447.                 pc.spc._addDet(StringComparator.ISINTEGER, (StringExpression) sym_v3);
  4448.                 if (!pc.simplify()) {// not satisfiable
  4449.                     th.getVM().getSystemState().setIgnored(true);
  4450.                 } else {
  4451.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4452.                     result = ((StringExpression) sym_v3)._IvalueOf();
  4453.                     sf.push(0, false); /* Result is don't care and an int */
  4454.                     sf = th.getModifiableTopFrame();
  4455.                     sf.setOperandAttr(result);
  4456.                 }
  4457.             } else {
  4458.                 pc.spc._addDet(StringComparator.NOTINTEGER, (StringExpression) sym_v3);
  4459.                 if (!pc.simplify()) {// not satisfiable
  4460.                     th.getVM().getSystemState().setIgnored(true);
  4461.                 } else {
  4462.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4463.                     th.createAndThrowException("java.lang.NumberFormatException");
  4464. //                  throw new RuntimeException("ERROR: Integer Format Type Exception");
  4465. //                  //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  4466. //                  //sf.push(0, true);
  4467.                 }
  4468.             }
  4469.         }
  4470.  
  4471.     }
  4472.  
  4473.     public void handleParseFloat(JVMInvokeInstruction invInst, ThreadInfo th) {
  4474.         StackFrame sf = th.getModifiableTopFrame();
  4475.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  4476.  
  4477.         if (sym_v3 == null) {
  4478.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  4479.         } else {
  4480.             RealExpression result = null;
  4481.             ChoiceGenerator<?> cg;
  4482.             boolean conditionValue;
  4483.             cg = th.getVM().getChoiceGenerator();
  4484.  
  4485.             assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4486.             conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4487.  
  4488.             sf.pop();
  4489.             PathCondition pc;
  4490.             ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4491.             while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4492.                 prev_cg = prev_cg.getPreviousChoiceGenerator();
  4493.             }
  4494.  
  4495.             if (prev_cg == null)
  4496.                 pc = new PathCondition();
  4497.             else
  4498.                 pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4499.  
  4500.             assert pc != null;
  4501.             if (conditionValue) {
  4502.                 pc.spc._addDet(StringComparator.ISFLOAT, (StringExpression) sym_v3);
  4503.                 if (!pc.simplify()) {// not satisfiable
  4504.                     th.getVM().getSystemState().setIgnored(true);
  4505.                 } else {
  4506.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4507.                     result = ((StringExpression) sym_v3)._RvalueOf();
  4508.                     sf.push(0, false); /* Result is don't care and a float */
  4509.                     sf = th.getModifiableTopFrame();
  4510.                     sf.setOperandAttr(result);
  4511.                 }
  4512.             } else {
  4513.                 pc.spc._addDet(StringComparator.NOTFLOAT, (StringExpression) sym_v3);
  4514.                 if (!pc.simplify()) {// not satisfiable
  4515.                     th.getVM().getSystemState().setIgnored(true);
  4516.                 } else {
  4517.                     throw new RuntimeException("ERROR: Possible Float Format Type Exception - Path Terminated");
  4518.                    
  4519.                     //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  4520.                 }
  4521.             }
  4522.         }
  4523.  
  4524.     }
  4525.  
  4526.     public void handleParseFloatValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4527.         StackFrame sf = th.getModifiableTopFrame();
  4528.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  4529.  
  4530.         if (sym_v3 == null) {
  4531.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  4532.         } else {
  4533.             if (sym_v3 instanceof RealExpression) {
  4534.                 RealExpression sym_v2 = (RealExpression) sym_v3;
  4535.                 sf.pop();
  4536.                 int objRef = getNewObjRef(invInst, th); /* dummy Float Object */
  4537.                 sf.push(objRef, true);
  4538.                 sf.setOperandAttr(sym_v2);
  4539.             } else {
  4540.                 RealExpression result = null;
  4541.                 ChoiceGenerator<?> cg;
  4542.                 boolean conditionValue;
  4543.                 cg = th.getVM().getChoiceGenerator();
  4544.  
  4545.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4546.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4547.  
  4548.                 sf.pop();
  4549.                 PathCondition pc;
  4550.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4551.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4552.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  4553.                 }
  4554.  
  4555.                 if (prev_cg == null)
  4556.                     pc = new PathCondition();
  4557.                 else
  4558.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4559.  
  4560.                 assert pc != null;
  4561.                 if (conditionValue) {
  4562.                     pc.spc._addDet(StringComparator.ISFLOAT, (StringExpression) sym_v3);
  4563.                     if (!pc.simplify()) {// not satisfiable
  4564.                         th.getVM().getSystemState().setIgnored(true);
  4565.                     } else {
  4566.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4567.                         result = ((StringExpression) sym_v3)._RvalueOf();
  4568.                         int objRef = getNewObjRef(invInst, th); /* dummy Float Object */
  4569.                         sf.push(objRef, true);
  4570.                         sf = th.getModifiableTopFrame();
  4571.                         sf.setOperandAttr(result);
  4572.                     }
  4573.                 } else {
  4574.                     pc.spc._addDet(StringComparator.NOTFLOAT, (StringExpression) sym_v3);
  4575.                     if (!pc.simplify()) {// not satisfiable
  4576.                         th.getVM().getSystemState().setIgnored(true);
  4577.                     } else {
  4578.                         throw new RuntimeException("ERROR: Possible Float Format Type Exception - Path Terminated");
  4579.                        
  4580.                         //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  4581.                     }
  4582.                 }
  4583.             }
  4584.         }
  4585.  
  4586.     }
  4587.  
  4588.     public void handleParseDoubleValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4589.         StackFrame sf = th.getModifiableTopFrame();
  4590.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  4591.  
  4592.         if (sym_v3 == null) {
  4593.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  4594.         } else {
  4595.             if (sym_v3 instanceof RealExpression) {
  4596.                 RealExpression sym_v2 = (RealExpression) sym_v3;
  4597.                 sf.popLong();
  4598.                 int objRef = getNewObjRef(invInst, th); /* dummy Double Object */
  4599.                 sf.push(objRef, true);
  4600.                 sf.setOperandAttr(sym_v2);
  4601.             } else {
  4602.                 RealExpression result = null;
  4603.                 ChoiceGenerator<?> cg;
  4604.                 boolean conditionValue;
  4605.                 cg = th.getVM().getChoiceGenerator();
  4606.  
  4607.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4608.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4609.  
  4610.                 sf.pop();
  4611.                 PathCondition pc;
  4612.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4613.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4614.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  4615.                 }
  4616.  
  4617.                 if (prev_cg == null)
  4618.                     pc = new PathCondition();
  4619.                 else
  4620.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4621.  
  4622.                 assert pc != null;
  4623.  
  4624.                 if (conditionValue) {
  4625.                     pc.spc._addDet(StringComparator.ISDOUBLE, (StringExpression) sym_v3);
  4626.                     if (!pc.simplify()) {// not satisfiable
  4627.                         th.getVM().getSystemState().setIgnored(true);
  4628.                     } else {
  4629.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4630.                         result = ((StringExpression) sym_v3)._RvalueOf();
  4631.                         int objRef = getNewObjRef(invInst, th); /* dummy Double Object */
  4632.                         sf.push(objRef, true);
  4633.                         sf = th.getModifiableTopFrame();
  4634.                         sf.setOperandAttr(result);
  4635.                     }
  4636.                 } else {
  4637.                     pc.spc._addDet(StringComparator.NOTDOUBLE, (StringExpression) sym_v3);
  4638.                     if (!pc.simplify()) {// not satisfiable
  4639.                         th.getVM().getSystemState().setIgnored(true);
  4640.                     } else {
  4641.                         throw new RuntimeException("ERROR: Double Format Type Exception");
  4642.                         //th.getVM().getSystemState().setIgnored(true);
  4643.                         //sf.push(0, true); // TODO: to review
  4644.                     }
  4645.                 }
  4646.             }
  4647.         }
  4648.  
  4649.     }
  4650.  
  4651.     public void handleParseDouble(JVMInvokeInstruction invInst, ThreadInfo th) {
  4652.         StackFrame sf = th.getModifiableTopFrame();
  4653.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  4654.  
  4655.         if (sym_v3 == null) {
  4656.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  4657.         } else {
  4658.             if (sym_v3 instanceof RealExpression) {
  4659.                 return;
  4660.             } else {
  4661.                 StringExpression sym_v1 = (StringExpression) sym_v3;
  4662.                 ChoiceGenerator<?> cg;
  4663.                 boolean conditionValue;
  4664.                 cg = th.getVM().getChoiceGenerator();
  4665.  
  4666.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4667.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4668.                 sf.pop();
  4669.                 PathCondition pc;
  4670.  
  4671.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4672.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4673.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  4674.                 }
  4675.  
  4676.                 if (prev_cg == null)
  4677.                     pc = new PathCondition();
  4678.                 else
  4679.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4680.  
  4681.                 assert pc != null;
  4682.  
  4683.                 if (conditionValue) {
  4684.                     pc.spc._addDet(StringComparator.ISDOUBLE, sym_v1);
  4685.                     if (!pc.simplify()) {// not satisfiable
  4686.                         th.getVM().getSystemState().setIgnored(true);
  4687.                     } else {
  4688.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4689.                         RealExpression sym_v2 = new SpecialRealExpression(sym_v1);
  4690.                         sf.pushLong((long) 0); /* Result is don't care and 0 */
  4691.                         //sf = th.getModifiableTopFrame(); ??
  4692.                         sf.setLongOperandAttr(sym_v2);
  4693.                     }
  4694.                 } else {
  4695.                     pc.spc._addDet(StringComparator.NOTDOUBLE, sym_v1);
  4696.                     if (!pc.simplify()) {// not satisfiable
  4697.                         th.getVM().getSystemState().setIgnored(true);
  4698.                     } else {
  4699.                         throw new RuntimeException("ERROR: Double Format Type Exception");
  4700.                         //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  4701.                     }
  4702.                 }
  4703.             }
  4704.         }
  4705.     }
  4706.  
  4707.     public void handleParseLong(JVMInvokeInstruction invInst, ThreadInfo th) {
  4708.         StackFrame sf = th.getModifiableTopFrame();
  4709.         Expression sym_v3 = (Expression) sf.getOperandAttr(0);
  4710.  
  4711.         if (sym_v3 == null) {
  4712.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  4713.         } else {
  4714.             if (sym_v3 instanceof IntegerExpression) {
  4715.                 return;
  4716.             } else {
  4717.                 StringExpression sym_v1 = (StringExpression) sym_v3;
  4718.                 ChoiceGenerator<?> cg;
  4719.                 boolean conditionValue;
  4720.                 cg = th.getVM().getChoiceGenerator();
  4721.  
  4722.                 assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4723.                 conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4724.                 sf.pop();
  4725.                 PathCondition pc;
  4726.  
  4727.                 ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4728.                 while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4729.                     prev_cg = prev_cg.getPreviousChoiceGenerator();
  4730.                 }
  4731.  
  4732.                 if (prev_cg == null)
  4733.                     pc = new PathCondition();
  4734.                 else
  4735.                     pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4736.  
  4737.                 assert pc != null;
  4738.  
  4739.                 if (conditionValue) {
  4740.                     pc.spc._addDet(StringComparator.ISLONG, sym_v1);
  4741.                     if (!pc.simplify()) {// not satisfiable
  4742.                         th.getVM().getSystemState().setIgnored(true);
  4743.                     } else {
  4744.                         ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4745.                         IntegerExpression sym_v2 = new SpecialIntegerExpression(sym_v1);
  4746.                         sf.pushLong((long) 0); /* result is don't care */
  4747.                         //sf = th.getModifiableTopFrame(); ??
  4748.                         sf.setLongOperandAttr(sym_v2);
  4749.                     }
  4750.                 } else {
  4751.                     pc.spc._addDet(StringComparator.NOTLONG, sym_v1);
  4752.                     if (!pc.simplify()) {// not satisfiable
  4753.                         th.getVM().getSystemState().setIgnored(true);
  4754.                     } else {
  4755.                         throw new RuntimeException("ERROR: Long Format Type Exception");
  4756.                         //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  4757.                     }
  4758.                 }
  4759.             }
  4760.         }
  4761.     }
  4762.  
  4763.     public void handleParseBoolean(JVMInvokeInstruction invInst, ThreadInfo th) {
  4764.         StackFrame sf = th.getModifiableTopFrame();
  4765.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  4766.  
  4767.         if (sym_v1 == null) {
  4768.             throw new RuntimeException("ERROR: symbolic method must have symbolic string operand");
  4769.         } else {
  4770.             ChoiceGenerator<?> cg;
  4771.             boolean conditionValue;
  4772.             cg = th.getVM().getChoiceGenerator();
  4773.  
  4774.             assert (cg instanceof PCChoiceGenerator) : "expected PCChoiceGenerator, got: " + cg;
  4775.             conditionValue = (Integer) cg.getNextChoice() == 0 ? false : true;
  4776.             sf.pop();
  4777.             PathCondition pc;
  4778.  
  4779.             ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
  4780.             while (!((prev_cg == null) || (prev_cg instanceof PCChoiceGenerator))) {
  4781.                 prev_cg = prev_cg.getPreviousChoiceGenerator();
  4782.             }
  4783.  
  4784.             if (prev_cg == null)
  4785.                 pc = new PathCondition();
  4786.             else
  4787.                 pc = ((PCChoiceGenerator) prev_cg).getCurrentPC();
  4788.  
  4789.             assert pc != null;
  4790.  
  4791.             if (conditionValue) {
  4792.                 pc.spc._addDet(StringComparator.ISBOOLEAN, sym_v1);
  4793.                 if (!pc.simplify()) {// not satisfiable
  4794.                     th.getVM().getSystemState().setIgnored(true);
  4795.                 } else {
  4796.                     ((PCChoiceGenerator) cg).setCurrentPC(pc);
  4797.                     IntegerExpression sym_v2 = new SpecialIntegerExpression(sym_v1);
  4798.                     sf.push(0, false); /* result is don't care and 0 */
  4799.                     sf = th.getModifiableTopFrame();
  4800.                     sf.setOperandAttr(sym_v2);
  4801.                 }
  4802.             } else {
  4803.                 pc.spc._addDet(StringComparator.NOTBOOLEAN, sym_v1);
  4804.                 if (!pc.simplify()) {// not satisfiable
  4805.                     th.getVM().getSystemState().setIgnored(true);
  4806.                 } else {
  4807.                     throw new RuntimeException("ERROR: Boolean Format Type Exception");
  4808.                     //th.getVM().getSystemState().setIgnored(true);TODO: needs revision
  4809.                 }
  4810.             }
  4811.         }
  4812.     }
  4813.  
  4814.     public int getNewObjRef(JVMInvokeInstruction invInst, ThreadInfo th) {
  4815.        
  4816.         //DynamicArea da = th.getVM().getDynamicArea();
  4817.         MethodInfo mi = invInst.getInvokedMethod();
  4818.         ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(mi.getReturnTypeName());
  4819.         ElementInfo objRef = th.getHeap().newObject(ci, th);
  4820.         return objRef.getObjectRef();
  4821.     }
  4822.  
  4823.     // works for BigDecimal
  4824.     public Instruction getBigDecimalValue(JVMInvokeInstruction invInst, ThreadInfo th) {
  4825.         MethodInfo mi = invInst.getInvokedMethod();
  4826.         ClassInfo ci = mi.getClassInfo();
  4827.         MethodInfo miInit = ci.getMethod("toString()V", false);
  4828.         if (miInit == null) {
  4829.             return null;
  4830.         }
  4831.         //Instruction initPC = miInit.execute(th);
  4832.         //return initPC;
  4833.         throw new RuntimeException("not handled; to review");
  4834.     }
  4835.  
  4836.     // works for String, StringBuilder, StringBuffer
  4837.     public Instruction init1NewStringObjRef(JVMInvokeInstruction invInst, ThreadInfo th) {
  4838.         MethodInfo mi = invInst.getInvokedMethod();
  4839.         ClassInfo ci = mi.getClassInfo();
  4840.         MethodInfo miInit = ci.getMethod("<init>()V", false);
  4841.         if (miInit == null) {
  4842.             return null;
  4843.         }
  4844.         //Instruction initPC = miInit.execute(th); // TODO: to review
  4845.         //return initPC;
  4846.         throw new RuntimeException("not handled; to review");
  4847.     }
  4848.  
  4849.     public Instruction handleIntValueOf(JVMInvokeInstruction invInst,  ThreadInfo th) {
  4850.         StackFrame sf = th.getModifiableTopFrame();
  4851.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  4852.  
  4853.         if (sym_v1 == null) {
  4854.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleIntValueOf");
  4855.         } else {
  4856.             sf.pop();
  4857.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  4858.             int objRef = th.getHeap().newString("", th).getObjectRef();
  4859.             /*
  4860.              * dummy
  4861.              * string
  4862.              * Object
  4863.              */
  4864.             sf.push(objRef, true);
  4865.             sf.setOperandAttr(sym_v2);
  4866.         }
  4867.         return null;
  4868.     }
  4869.  
  4870.     public Instruction handleFloatValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4871.         StackFrame sf = th.getModifiableTopFrame();
  4872.         RealExpression sym_v1 = (RealExpression) sf.getOperandAttr(0);
  4873.  
  4874.         if (sym_v1 == null) {
  4875.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleFloatValueOf");
  4876.         } else {
  4877.             sf.pop();
  4878.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  4879.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  4880.                                                                                                                                      * dummy
  4881.                                                                                                                                      * string
  4882.                                                                                                                                      * Object
  4883.                                                                                                                                      */
  4884.             sf.push(objRef, true);
  4885.             sf.setOperandAttr(sym_v2);
  4886.         }
  4887.         return null;
  4888.     }
  4889.  
  4890.     public Instruction handleLongValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4891.         StackFrame sf = th.getModifiableTopFrame();
  4892.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  4893.  
  4894.         if (sym_v1 == null) {
  4895.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleLongValueOf");
  4896.         } else {
  4897.             sf.popLong();
  4898.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  4899.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  4900.                                                                                                                                      * dummy
  4901.                                                                                                                                      * string
  4902.                                                                                                                                      * Object
  4903.                                                                                                                                      */
  4904.             sf.push(objRef, true);
  4905.             sf.setOperandAttr(sym_v2);
  4906.         }
  4907.         return null;
  4908.     }
  4909.  
  4910.     public Instruction handleDoubleValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4911.         StackFrame sf = th.getModifiableTopFrame();
  4912.         RealExpression sym_v1 = (RealExpression) sf.getOperandAttr(0);
  4913.  
  4914.         if (sym_v1 == null) {
  4915.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleDoubleValueOf");
  4916.         } else {
  4917.             sf.popLong();
  4918.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  4919.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  4920.                                                                                                                                      * dummy
  4921.                                                                                                                                      * string
  4922.                                                                                                                                      * Object
  4923.                                                                                                                                      */
  4924.             sf.push(objRef, true);
  4925.             sf.setOperandAttr(sym_v2);
  4926.         }
  4927.         return null;
  4928.     }
  4929.  
  4930.     public Instruction handleBooleanValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4931.         StackFrame sf = th.getModifiableTopFrame();
  4932.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  4933.  
  4934.         if (sym_v1 == null) {
  4935.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleBooleanValueOf");
  4936.         } else {
  4937.             sf.pop();
  4938.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  4939.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  4940.                                                                                                                                      * dummy
  4941.                                                                                                                                      * string
  4942.                                                                                                                                      * Object
  4943.                                                                                                                                      */
  4944.             sf.push(objRef, true);
  4945.             sf.setOperandAttr(sym_v2);
  4946.         }
  4947.         return null;
  4948.     }
  4949.  
  4950.     public Instruction handleCharValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4951.         //throw new RuntimeException("ERROR: symbolic string method not Implemented - CharValueOf");
  4952.         StackFrame sf = th.getModifiableTopFrame();
  4953.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  4954.  
  4955.         if (sym_v1 == null) {
  4956.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: handleIntValueOf");
  4957.         } else {
  4958.             sf.pop();
  4959.             StringExpression sym_v2 = StringExpression._valueOf(sym_v1);
  4960.             int objRef = th.getHeap().newString("", th).getObjectRef();
  4961.             sf.push(objRef, true);
  4962.             sf.setOperandAttr(sym_v2);
  4963.         }
  4964.  
  4965.         return null;
  4966.     }
  4967.  
  4968.     public Instruction handleCharArrayValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4969.         throw new RuntimeException("ERROR: symbolic string method not Implemented - CharArrayValueof");
  4970.     }
  4971.  
  4972.     public Instruction handleObjectValueOf(JVMInvokeInstruction invInst, ThreadInfo th) {
  4973.         StackFrame sf = th.getModifiableTopFrame();
  4974.         Expression sym_v1 = (Expression) sf.getOperandAttr(0);
  4975.         if (sym_v1 instanceof SymbolicStringBuilder) {
  4976.             sf.pop();
  4977.             SymbolicStringBuilder sym_v3 = (SymbolicStringBuilder) sym_v1;
  4978.             StringExpression sym_v2 = StringExpression._valueOf((StringExpression) sym_v3.getstr());
  4979.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  4980.                                                                                                                                      * dummy
  4981.                                                                                                                                      * String
  4982.                                                                                                                                      * Object
  4983.                                                                                                                                      */
  4984.             sf.push(objRef, true);
  4985.             sf.setOperandAttr(sym_v2);
  4986.         } else if (sym_v1 instanceof StringExpression) {
  4987.             sf.pop();
  4988.             StringExpression sym_v2 = StringExpression._valueOf((StringExpression) sym_v1);
  4989.             int objRef = th.getHeap().newString("", th).getObjectRef(); /*
  4990.                                                                                                                                      * dummy
  4991.                                                                                                                                      * String
  4992.                                                                                                                                      * Object
  4993.                                                                                                                                      */
  4994.             sf.push(objRef, true);
  4995.             sf.setOperandAttr(sym_v2);
  4996.         } else {
  4997.             throw new RuntimeException("ERROR: symbolic string method not Implemented - ObjectValueof");
  4998.         }
  4999.         return null;
  5000.     }
  5001.  
  5002.     public Instruction handleConcat(JVMInvokeInstruction invInst, ThreadInfo th) {
  5003.         StackFrame sf = th.getModifiableTopFrame();
  5004.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  5005.         StringExpression sym_v2 = (StringExpression) sf.getOperandAttr(1);
  5006.  
  5007.         if ((sym_v1 == null) & (sym_v2 == null)) {
  5008.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleConcat");
  5009.         } else {
  5010.             int s1 = sf.pop();
  5011.             int s2 = sf.pop();
  5012.  
  5013.             StringExpression result = null;
  5014.             if (sym_v1 == null) { // operand 0 is concrete
  5015.                 ElementInfo e1 = th.getElementInfo(s1);
  5016.                 String val = e1.asString();
  5017.                 result = sym_v2._concat(val);
  5018.             } else if (sym_v2 == null) { // operand 1 is concrete
  5019.                 ElementInfo e2 = th.getElementInfo(s2);
  5020.                 String val = e2.asString();
  5021.                 sym_v2 = new StringConstant(val);
  5022.                 result = sym_v2._concat(sym_v1);
  5023.             } else { // both operands are symbolic
  5024.                 result = sym_v2._concat(sym_v1);
  5025.             }
  5026.             int objRef = th.getHeap().newString("", th).getObjectRef();
  5027.             /*
  5028.             * dummy
  5029.             * String
  5030.             * Object
  5031.             */
  5032.             sf.push(objRef, true);
  5033.             sf.setOperandAttr(result);
  5034.         }
  5035.         return null;
  5036.     }
  5037.  
  5038.     public void handleObjectEquals(JVMInvokeInstruction invInst,  ThreadInfo th) {
  5039.         StackFrame sf = th.getModifiableTopFrame();
  5040.         Expression sym_v1 = (Expression) sf.getOperandAttr(0);
  5041.         Expression sym_v2 = (Expression) sf.getOperandAttr(1);
  5042.  
  5043.         if (sym_v1 != null) {
  5044.             // System.out.println("*" + sym_v1.toString());
  5045.             if (!(sym_v1 instanceof StringExpression)) {
  5046.                 throw new RuntimeException("ERROR: expressiontype not handled: ObjectEquals");
  5047.             }
  5048.         }
  5049.  
  5050.         if (sym_v2 != null) {
  5051.             // System.out.println("***" + sym_v2.toString());
  5052.             if (!(sym_v2 instanceof StringExpression)) {
  5053.                 throw new RuntimeException("ERROR: expressiontype not handled: ObjectEquals");
  5054.             }
  5055.         }
  5056.  
  5057.         handleEquals(invInst, th);
  5058.     }
  5059.  
  5060.     public void handleEquals(JVMInvokeInstruction invInst,  ThreadInfo th) {
  5061.         handleBooleanStringInstructions(invInst,  th, StringComparator.EQUALS);
  5062.        
  5063.     }
  5064.  
  5065.     public Instruction handleAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5066.         Instruction handled = null;
  5067.        
  5068.         MethodInfo mi = invInst.getInvokedMethod(th);
  5069.         String[] argTypes = mi.getArgumentTypeNames();
  5070.         // System.out.println(argTypes[0]);
  5071.        
  5072.         boolean isCharSequence = false;
  5073.         //check what is the concrete type of the charsequence
  5074.         if(argTypes[0].equals("java.lang.CharSequence")) {
  5075.             isCharSequence = true;
  5076.             StackFrame sf = th.getModifiableTopFrame();
  5077.             int firstParamIndex = mi.isStatic() ? 0 : 1;
  5078.             Object firstParam = sf.getArgumentAttrs(mi)[firstParamIndex];
  5079.             if(firstParam instanceof StringExpression || firstParam == null /*possibly an string constant*/) {
  5080.                 argTypes[0] = "java.lang.String";
  5081.             } else if (firstParam instanceof SymbolicStringBuilder) {
  5082.                 //TODO and if it is a StringBuffer?
  5083.                 argTypes[0] = "java.lang.StringBuilder";
  5084.             } else {
  5085.                 throw new RuntimeException("Unhandled CharSequence at Symbolic String Append; concrete type is:" + firstParam.getClass());
  5086.             }
  5087.         }
  5088.         if (isCharSequence && argTypes.length == 3) { //append(charSequence,int,int)
  5089.             if(argTypes[0].equals("java.lang.String")) {
  5090.                 handled = handleStringAppend3(invInst, th);
  5091.             } else { //stringbuilder
  5092.                 handled = handleStringBuilderAppend3(invInst, th);
  5093.             }
  5094.         } else if (argTypes[0].equals("java.lang.String")) {
  5095.             handleStringAppend(invInst, th);
  5096.         } else if ((argTypes[0].equals("java.lang.StringBuilder")) || (argTypes[0].equals("java.lang.StringBuffer"))) {
  5097.             handleStringBuilderAppend(invInst, th);
  5098.         } else if (argTypes[0].equals("int")) {
  5099.             handleIntAppend(invInst, th);
  5100.         } else if (argTypes[0].equals("char")) {
  5101.             handleCharAppend(invInst, th);
  5102.         } else if (argTypes[0].equals("byte")) {
  5103.             handleByteAppend(invInst, th);
  5104.         } else if (argTypes[0].equals("short")) {
  5105.             handleShortAppend(invInst, th);
  5106.         } else if (argTypes[0].equals("float")) {
  5107.             handleFloatAppend(invInst, th);
  5108.         } else if (argTypes[0].equals("long")) {
  5109.             handleLongAppend(invInst, th);
  5110.         } else if (argTypes[0].equals("double")) {
  5111.             handleDoubleAppend(invInst, th);
  5112.         } else if (argTypes[0].equals("boolean")) {
  5113.             handleBooleanAppend(invInst, th);
  5114.         } else if (argTypes[0].equals("java.lang.Object")) {
  5115.             handleObjectAppend(invInst, th);
  5116.         } else {
  5117.             throw new RuntimeException("ERROR: Input parameter type not handled in Symbolic String Append");
  5118.         }
  5119.  
  5120.         return handled;
  5121.     }
  5122.  
  5123.     public void handleStringAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5124.         StackFrame sf = th.getModifiableTopFrame();
  5125.         // int objRef = sf.getThis();
  5126.         // ElementInfo ei = th.getElementInfo(objRef);
  5127.  
  5128.         StringExpression sym_v1 = (StringExpression) sf.getOperandAttr(0);
  5129.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  5130.  
  5131.         if (sym_v2 == null)
  5132.             sym_v2 = new SymbolicStringBuilder();
  5133.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  5134.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleStringAppend");
  5135.         } else {
  5136.             int s1 = sf.pop();
  5137.             int s2 = sf.pop();
  5138.  
  5139.             if (sym_v1 == null) { // operand 0 is concrete
  5140.                 ElementInfo e1 = th.getElementInfo(s1);
  5141.                 String val = e1.asString();
  5142.                 sym_v2._append(val);
  5143.                 sf.push(s2, true); /* symbolic string Builder element */
  5144.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5145.                 // from String builder object
  5146.                 ElementInfo e1 = th.getElementInfo(s2);
  5147.                 String val = getStringEquiv(e1);
  5148.                 sym_v2.putstr(new StringConstant(val));
  5149.                 sym_v2._append(sym_v1);
  5150.                 // setVariableAttribute(ei, invInst, th, sf, s2, sym_v2); //set the
  5151.                 // value of the attribute of local StringBuilder element as sym_v2
  5152.                 sf.push(s2, true); /* symbolic string Builder element */
  5153.             } else { // both operands are symbolic
  5154.                 sym_v2._append(sym_v1);
  5155.                 sf.push(s2, true); /* string Builder element can continue */
  5156.             }
  5157.  
  5158.             sf.setOperandAttr(sym_v2);
  5159.         }
  5160.     }
  5161.    
  5162.     public Instruction handleStringAppend3(JVMInvokeInstruction invInst, ThreadInfo th) {
  5163.         StackFrame sf = th.getModifiableTopFrame();
  5164.        
  5165.         IntegerExpression sym_end = (IntegerExpression) sf.getOperandAttr(0);
  5166.         IntegerExpression sym_start = (IntegerExpression) sf.getOperandAttr(1);
  5167.         StringExpression sym_string = (StringExpression) sf.getOperandAttr(2);
  5168.         SymbolicStringBuilder sym_builder = (SymbolicStringBuilder) sf.getOperandAttr(3);
  5169.  
  5170.         if (sym_builder == null) {
  5171.             sym_builder = new SymbolicStringBuilder();
  5172.         }
  5173.        
  5174.         //check if all parameters are concrete
  5175.         boolean concreteSubstring = (sym_end == null & sym_start == null & sym_string == null);
  5176.        
  5177.         if (concreteSubstring & sym_builder.getstr() == null) {
  5178.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: HandleStringAppend3");
  5179.         } else {
  5180.             int endRef = sf.pop();
  5181.             int startRef = sf.pop();
  5182.             int stringRef = sf.pop();
  5183.             int builderRef = sf.pop();
  5184.    
  5185.             //prepare the substring
  5186.             StringExpression substring;
  5187.             if(concreteSubstring) {
  5188.                 try {
  5189.                     ElementInfo eiString = th.getElementInfo(stringRef);
  5190.                     String concreteString = eiString.asString();
  5191.                     String slice = concreteString.substring(startRef, endRef);
  5192.                     substring = new StringConstant(slice);
  5193.                 } catch (IndexOutOfBoundsException e) {
  5194.                     return th.createAndThrowException("java.lang.IndexOutOfBoundsException",e.getMessage());
  5195.                 }
  5196.             } else {
  5197.                 if(sym_string == null) {
  5198.                     ElementInfo eString = th.getElementInfo(stringRef);
  5199.                     String concreteString = eString.asString();
  5200.                     sym_string = new StringConstant(concreteString);
  5201.                 }
  5202.                 substring = createSymbolicSubstring(sym_string, sym_start, sym_end, startRef, endRef);
  5203.             }
  5204.            
  5205.             //append to the symbolic string
  5206.             if(sym_builder.getstr() == null) { //stringbuilder is concrete
  5207.                 ElementInfo eiBuilder = th.getElementInfo(builderRef);
  5208.                 String builderContents = getStringEquiv(eiBuilder);
  5209.                 sym_builder.putstr(new StringConstant(builderContents));
  5210.             }
  5211.            
  5212.             sym_builder._append(substring);
  5213.             sf.push(builderRef,true);
  5214.         }
  5215.        
  5216.         sf.setOperandAttr(sym_builder);
  5217.        
  5218.         return null;
  5219.     }
  5220.    
  5221.     //helper
  5222.     private StringExpression createSymbolicSubstring(StringExpression sym_str,
  5223.             IntegerExpression sym_start, IntegerExpression sym_end,
  5224.             int startRef, int endRef) {
  5225.        
  5226.         StringExpression result;
  5227.        
  5228.         //'end' is the first parameter (something with stack representation, maybe?)
  5229.         if(sym_start == null && sym_end == null) {
  5230.             result = sym_str._subString(endRef, startRef);
  5231.         } else if (sym_start == null) {
  5232.             result = sym_str._subString(sym_end, startRef);
  5233.         } else { //sym_end == null
  5234.             result = sym_str._subString(endRef, sym_start);
  5235.         }
  5236.        
  5237.         return result;
  5238.     }
  5239.    
  5240.     public Instruction handleStringBuilderAppend3(JVMInvokeInstruction invInst, ThreadInfo th) {
  5241.         throw new RuntimeException("implement this");
  5242.     }
  5243.  
  5244.     public void setVariableAttribute(ElementInfo ei, JVMInvokeInstruction invInst, ThreadInfo th, StackFrame sf, int idx,
  5245.             Object sym_v2) {
  5246.         int count = sf.getLocalVariableCount();
  5247.         for (int i = 0; i < count; i++) {
  5248.             int idx1 = sf.getLocalVariable(i);
  5249.             if (idx1 == idx) {
  5250.                 sf.setLocalAttr(i, sym_v2);
  5251.                 return;
  5252.             }
  5253.         }
  5254.         // If variable is a static field and not local variable
  5255.         ClassInfo ci = sf.getClassInfo();
  5256.         FieldInfo[] fields = ci.getDeclaredStaticFields();
  5257.         int fieldid = -1;
  5258.         for (int i = 0; i < fields.length; i++) {
  5259.             if (fields[i].isReference()) {
  5260.                 fieldid = ci.getStaticElementInfo().getReferenceField(fields[i]);
  5261.             }
  5262.             if (fieldid == idx) {
  5263.                 ci.getStaticElementInfo().setFieldAttr(fields[i], sym_v2);
  5264.                 return;
  5265.             }
  5266.         }
  5267.  
  5268.         // If variable is an instance field and not local variable
  5269.         FieldInfo[] fields1 = ci.getDeclaredInstanceFields();
  5270.         fieldid = -1;
  5271.         for (int i = 0; i < fields1.length; i++) {
  5272.             if (fields1[i].isReference()) {
  5273.                 fieldid = ei.getReferenceField(fields1[i]);
  5274.             }
  5275.             if (fieldid == idx) {
  5276.                 ei.setFieldAttr(fields1[i], sym_v2);
  5277.                 return;
  5278.             }
  5279.         }
  5280.         // if method does not return anything then
  5281.         MethodInfo mi = invInst.getInvokedMethod();
  5282.         byte b = mi.getReturnTypeCode();
  5283.         if (b == Types.T_VOID)
  5284.             System.out.println("WARNING: Could not set variable attribute");
  5285.  
  5286.     }
  5287.  
  5288.     public void handleCharAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5289.  
  5290.         StackFrame sf = th.getModifiableTopFrame();
  5291.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  5292.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  5293.  
  5294.         if (sym_v2 == null)
  5295.             sym_v2 = new SymbolicStringBuilder();
  5296.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  5297.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleCharAppend");
  5298.         } else {
  5299.             char s1 = (char) sf.pop();
  5300.             int s2 = sf.pop();
  5301.             if (sym_v1 == null) { // operand 0 is concrete
  5302.                 String val = Character.toString(s1);
  5303.                 sym_v2._append(val);
  5304.                 sf.push(s2, true); /* symbolic string Builder element */
  5305.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5306.                 // from String builder object
  5307.                 ElementInfo e1 = th.getElementInfo(s2);
  5308.                 String val = getStringEquiv(e1);
  5309.                 sym_v2.putstr(new StringConstant(val));
  5310.                 sym_v2._append(sym_v1);
  5311.                 sf.push(s2, true); /* symbolic string Builder element */
  5312.             } else { // both operands are symbolic
  5313.                 sym_v2._append(sym_v1);
  5314.                 sf.push(s2, true); /* string Builder element can continue */
  5315.             }
  5316.  
  5317.             sf.setOperandAttr(sym_v2);
  5318.         }
  5319.     }
  5320.  
  5321.     public void handleByteAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5322.  
  5323.         StackFrame sf = th.getModifiableTopFrame();
  5324.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  5325.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  5326.  
  5327.         if (sym_v2 == null)
  5328.             sym_v2 = new SymbolicStringBuilder();
  5329.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  5330.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleByteAppend");
  5331.         } else {
  5332.             byte s1 = (byte) sf.pop();
  5333.             int s2 = sf.pop();
  5334.             if (sym_v1 == null) { // operand 0 is concrete
  5335.                 String val = Byte.toString(s1);
  5336.                 sym_v2._append(val);
  5337.                 sf.push(s2, true); /* symbolic string Builder element */
  5338.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5339.                 // from String builder object
  5340.                 ElementInfo e1 = th.getElementInfo(s2);
  5341.                 String val = getStringEquiv(e1);
  5342.                 sym_v2.putstr(new StringConstant(val));
  5343.                 sym_v2._append(sym_v1);
  5344.                 sf.push(s2, true); /* symbolic string Builder element */
  5345.             } else { // both operands are symbolic
  5346.                 sym_v2._append(sym_v1);
  5347.                 sf.push(s2, true); /* string Builder element can continue */
  5348.             }
  5349.  
  5350.             sf.setOperandAttr(sym_v2);
  5351.         }
  5352.     }
  5353.  
  5354.     public void handleShortAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5355.  
  5356.         StackFrame sf = th.getModifiableTopFrame();
  5357.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  5358.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  5359.  
  5360.         if (sym_v2 == null)
  5361.             sym_v2 = new SymbolicStringBuilder();
  5362.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  5363.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleShortAppend");
  5364.         } else {
  5365.             short s1 = (short) sf.pop();
  5366.             int s2 = sf.pop();
  5367.             if (sym_v1 == null) { // operand 0 is concrete
  5368.                 String val = Short.toString(s1);
  5369.                 sym_v2._append(val);
  5370.                 sf.push(s2, true); /* symbolic string Builder element */
  5371.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5372.                 // from String builder object
  5373.                 ElementInfo e1 = th.getElementInfo(s2);
  5374.                 String val = getStringEquiv(e1);
  5375.                 sym_v2.putstr(new StringConstant(val));
  5376.                 sym_v2._append(sym_v1);
  5377.                 sf.push(s2, true); /* symbolic string Builder element */
  5378.             } else { // both operands are symbolic
  5379.                 sym_v2._append(sym_v1);
  5380.                 sf.push(s2, true); /* string Builder element can continue */
  5381.             }
  5382.  
  5383.             sf.setOperandAttr(sym_v2);
  5384.         }
  5385.     }
  5386.  
  5387.     public void handleIntAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5388.  
  5389.         StackFrame sf = th.getModifiableTopFrame();
  5390.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  5391.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  5392.  
  5393.         if (sym_v2 == null)
  5394.             sym_v2 = new SymbolicStringBuilder();
  5395.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  5396.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: hanldeIntAppend");
  5397.         } else {
  5398.             int s1 = sf.pop();
  5399.             int s2 = sf.pop();
  5400.             if (sym_v1 == null) { // operand 0 is concrete
  5401.                 String val = Integer.toString(s1);
  5402.                 sym_v2._append(val);
  5403.                 sf.push(s2, true); /* symbolic string Builder element */
  5404.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5405.                 // from String builder object
  5406.                 ElementInfo e1 = th.getElementInfo(s2);
  5407.                 String val = getStringEquiv(e1);
  5408.                 sym_v2.putstr(new StringConstant(val));
  5409.                 sym_v2._append(sym_v1);
  5410.                 sf.push(s2, true); /* symbolic string Builder element */
  5411.             } else { // both operands are symbolic
  5412.                 sym_v2._append(sym_v1);
  5413.                 sf.push(s2, true); /* string Builder element can continue */
  5414.             }
  5415.  
  5416.             sf.setOperandAttr(sym_v2);
  5417.         }
  5418.     }
  5419.  
  5420.     public void handleFloatAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5421.  
  5422.         StackFrame sf = th.getModifiableTopFrame();
  5423.         RealExpression sym_v1 = (RealExpression) sf.getOperandAttr(0);
  5424.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  5425.  
  5426.         if (sym_v2 == null)
  5427.             sym_v2 = new SymbolicStringBuilder();
  5428.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  5429.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: hanldeFloatAppend");
  5430.         } else {
  5431.             float s1 = Types.intToFloat(sf.pop());
  5432.             int s2 = sf.pop();
  5433.             if (sym_v1 == null) { // operand 0 is concrete
  5434.                 String val = Float.toString(s1);
  5435.                 sym_v2._append(val);
  5436.                 sf.push(s2, true); /* symbolic string Builder element */
  5437.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5438.                 // from String builder object
  5439.                 ElementInfo e1 = th.getElementInfo(s2);
  5440.                 String val = getStringEquiv(e1);
  5441.                 sym_v2.putstr(new StringConstant(val));
  5442.                 sym_v2._append(sym_v1);
  5443.                 sf.push(s2, true); /* symbolic string Builder element */
  5444.             } else { // both operands are symbolic
  5445.                 sym_v2._append(sym_v1);
  5446.                 sf.push(s2, true); /* string Builder element can continue */
  5447.             }
  5448.  
  5449.             sf.setOperandAttr(sym_v2);
  5450.         }
  5451.     }
  5452.  
  5453.     public void handleBooleanAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5454.         StackFrame sf = th.getModifiableTopFrame();
  5455.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  5456.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  5457.  
  5458.         if (sym_v2 == null)
  5459.             sym_v2 = new SymbolicStringBuilder();
  5460.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  5461.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: hanldeBooleanAppend");
  5462.         } else {
  5463.             boolean s1 = Types.intToBoolean(sf.pop());
  5464.             int s2 = sf.pop();
  5465.             if (sym_v1 == null) { // operand 0 is concrete
  5466.                 String val = Boolean.toString(s1);
  5467.                 sym_v2._append(val);
  5468.                 sf.push(s2, true); /* symbolic string Builder element */
  5469.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5470.                 // from String builder object
  5471.                 ElementInfo e1 = th.getElementInfo(s2);
  5472.                 String val = getStringEquiv(e1);
  5473.                 sym_v2.putstr(new StringConstant(val));
  5474.                 sym_v2._append(sym_v1); /*
  5475.                                                                  * String s1 =
  5476.                                                                  * AbstractionUtilityMethods.unknownString();
  5477.                                                                  * String s2 =
  5478.                                                                  * AbstractionUtilityMethods.unknownString();
  5479.                                                                  * String s4 =
  5480.                                                                  * AbstractionUtilityMethods.unknownString();
  5481.                                                                  * String s5 =
  5482.                                                                  * AbstractionUtilityMethods.unknownString();
  5483.                                                                  */
  5484.  
  5485.                 sf.push(s2, true); /* symbolic string Builder element */
  5486.             } else { // both operands are symbolic
  5487.                 sym_v2._append(sym_v1);
  5488.                 sf.push(s2, true); /* string Builder element can continue */
  5489.             }
  5490.  
  5491.             sf.setOperandAttr(sym_v2);
  5492.         }
  5493.     }
  5494.  
  5495.     public void handleLongAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5496.  
  5497.         StackFrame sf = th.getModifiableTopFrame();
  5498.         IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0);
  5499.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(2);
  5500.  
  5501.         if (sym_v2 == null)
  5502.             sym_v2 = new SymbolicStringBuilder();
  5503.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  5504.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleLongAppend");
  5505.         } else {
  5506.             long s1 = sf.popLong();
  5507.             int s2 = sf.pop();
  5508.             if (sym_v1 == null) { // operand 0 is concrete
  5509.                 String val = Long.toString(s1);
  5510.                 sym_v2._append(val);
  5511.                 sf.push(s2, true); /* symbolic string Builder element */
  5512.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5513.                 // from String builder object
  5514.                 ElementInfo e1 = th.getElementInfo(s2);
  5515.                 String val = getStringEquiv(e1);
  5516.                 sym_v2.putstr(new StringConstant(val));
  5517.                 sym_v2._append(sym_v1);
  5518.                 sf.push(s2, true); /* symbolic string Builder element */
  5519.             } else { // both operands are symbolic
  5520.                 sym_v2._append(sym_v1);
  5521.                 sf.push(s2, true); /* string Builder element can continue */
  5522.             }
  5523.  
  5524.             sf.setOperandAttr(sym_v2);
  5525.         }
  5526.     }
  5527.  
  5528.     public void handleDoubleAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5529.  
  5530.         StackFrame sf = th.getModifiableTopFrame();
  5531.  
  5532.         RealExpression sym_v1 = (RealExpression) sf.getLongOperandAttr();
  5533.         double s1 = Types.longToDouble(sf.popLong());
  5534.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr();
  5535.         int s2 = sf.pop();
  5536.  
  5537.         if (sym_v2 == null)
  5538.             sym_v2 = new SymbolicStringBuilder();
  5539.         if ((sym_v1 == null) & (sym_v2.getstr() == null)) {
  5540.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand");
  5541.         } else {
  5542.  
  5543.             if (sym_v1 == null) { // operand 0 is concrete
  5544.                 String val = Double.toString(s1);
  5545.                 sym_v2._append(val);
  5546.                 sf.push(s2, true); /* symbolic string Builder element */
  5547.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5548.                 // from String builder object
  5549.                 ElementInfo e1 = th.getElementInfo(s2);
  5550.                 String val = getStringEquiv(e1);
  5551.                 sym_v2.putstr(new StringConstant(val));
  5552.                 sym_v2._append(sym_v1);
  5553.                 sf.push(s2, true); /* symbolic string Builder element */
  5554.             } else { // both operands are symbolic
  5555.                 sym_v2._append(sym_v1);
  5556.                 sf.push(s2, true); /* string Builder element can continue */
  5557.             }
  5558.  
  5559.             sf.setOperandAttr(sym_v2);
  5560.         }
  5561.     }
  5562.  
  5563.     /*
  5564.      * String s1 = AbstractionUtilityMethods.unknownString(); String s2 =
  5565.      * AbstractionUtilityMethods.unknownString(); String s4 =
  5566.      * AbstractionUtilityMethods.unknownString(); String s5 =
  5567.      * AbstractionUtilityMethods.unknownString();
  5568.      */
  5569.  
  5570.     public void handleObjectAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5571.         StackFrame sf = th.getModifiableTopFrame();
  5572.  
  5573.         Expression sym_v1 = (Expression) sf.getOperandAttr(0);
  5574.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  5575.         // System.out.println(invInst.getSourceLocation());
  5576.         if (sym_v2 == null)
  5577.             sym_v2 = new SymbolicStringBuilder();
  5578.         if ((sym_v1 == null) && (sym_v2.getstr() == null)) {
  5579.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: handleObjectAppend");
  5580.         } else {
  5581.             int s1 = sf.pop();
  5582.             ElementInfo e2 = th.getElementInfo(s1);
  5583.             int s2 = sf.pop();
  5584.             if (sym_v1 == null || (sym_v1 instanceof SymbolicStringBuilder
  5585.                     && ((SymbolicStringBuilder) sym_v1).getstr() == null)) { // operand 0 is concrete
  5586.                 String val = getStringEquiv(e2);
  5587.                 sym_v2._append(val);
  5588.                 sf.push(s2, true); /* symbolic string Builder element */
  5589.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5590.                 // from String builder object
  5591.                 ElementInfo e1 = th.getElementInfo(s2);
  5592.                 String val = getStringEquiv(e1);
  5593.                 sym_v2.putstr(new StringConstant(val));
  5594.                 if (sym_v1 instanceof SymbolicStringBuilder)
  5595.                     sym_v2._append((SymbolicStringBuilder) sym_v1);
  5596.                 else if (sym_v1 instanceof StringExpression)
  5597.                     sym_v2._append((StringExpression) sym_v1);
  5598.                 else {
  5599.                     throw new RuntimeException("Object not handled in ObjectAppend");
  5600.                 }
  5601.                 // setVariableAttribute(ei, invInst, th, sf, s2, sym_v2); //set the
  5602.                 // value of the attribute of local StringBuilder element as sym_v2
  5603.                 sf.push(s2, true); /* symbolic string Builder element */
  5604.             } else { // both operands are symbolic
  5605.                 if (sym_v1 instanceof SymbolicStringBuilder)
  5606.                     sym_v2._append((SymbolicStringBuilder) sym_v1);
  5607.                 else if (sym_v1 instanceof StringExpression)
  5608.                     sym_v2._append((StringExpression) sym_v1);
  5609.                 else {
  5610.                     throw new RuntimeException("Object not handled in ObjectAppend");
  5611.                 }
  5612.  
  5613.                 sf.push(s2, true); /* string Builder element can continue */
  5614.             }
  5615.             sf.setOperandAttr(sym_v2);
  5616.         }
  5617.     }
  5618.  
  5619.     public void handleStringBuilderAppend(JVMInvokeInstruction invInst, ThreadInfo th) {
  5620.  
  5621.         StackFrame sf = th.getModifiableTopFrame();
  5622.         SymbolicStringBuilder sym_v1 = (SymbolicStringBuilder) sf.getOperandAttr(0);
  5623.         SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sf.getOperandAttr(1);
  5624.  
  5625.         if (sym_v2 == null)
  5626.             sym_v2 = new SymbolicStringBuilder();
  5627.         if (sym_v1 == null)
  5628.             sym_v1 = new SymbolicStringBuilder();
  5629.  
  5630.         if ((sym_v1.getstr() == null) & (sym_v2.getstr() == null)) {
  5631.             throw new RuntimeException("ERROR: symbolic string method must have one symbolic operand: hanldeStringBuilderAppend");
  5632.         } else {
  5633.             int s1 = sf.pop();
  5634.             int s2 = sf.pop();
  5635.  
  5636.             if (sym_v1.getstr() == null) { // operand 0 is concrete
  5637.                 ElementInfo e1 = th.getElementInfo(s1);
  5638.                 String val = getStringEquiv(e1);
  5639.                 sym_v2._append(val);
  5640.                 sf.push(s2, true); /* symbolic string Builder element */
  5641.             } else if (sym_v2.getstr() == null) { // operand 1 is concrete; get string
  5642.                 // from String builder object
  5643.                 ElementInfo e1 = th.getElementInfo(s2);
  5644.                 String val = getStringEquiv(e1);
  5645.                 sym_v2.putstr(new StringConstant(val));
  5646.                 sym_v2._append(sym_v1);
  5647.                 sf.push(s2, true); /* symbolic string Builder element */
  5648.             } else { // both operands are symbolic
  5649.                 sym_v2._append(sym_v1);
  5650.                 sf.push(s2, true); /* string Builder element can continue */
  5651.             }
  5652.  
  5653.             sf.setOperandAttr(sym_v2);
  5654.         }
  5655.     }
  5656.  
  5657.     public String getStringEquiv(ElementInfo ei) {
  5658.         String objectType = ei.getType();
  5659.         if (objectType.equals("Ljava/lang/StringBuilder;")) {
  5660.             int idx = ei.getReferenceField("value");
  5661.             int length = ei.getIntField("count");
  5662.             ElementInfo e1 = VM.getVM().getHeap().get(idx);
  5663.             char[] str = e1.asCharArray();
  5664.             String val = new String(str, 0, length);
  5665.             return val;
  5666.         } else if (objectType.equals("Ljava/lang/StringBuffer;")) {
  5667.             int idx = ei.getReferenceField("value");
  5668.             int length = ei.getIntField("count");
  5669.             ElementInfo e1 = VM.getVM().getHeap().get(idx);
  5670.             char[] str = e1.asCharArray();
  5671.             String val = new String(str, 0, length);
  5672.             return val;
  5673.         } else if (objectType.equals("Ljava/lang/Integer;")) {
  5674.             int val = ei.getIntField("value");
  5675.             return Integer.toString(val);
  5676.         } else if (objectType.equals("Ljava/lang/Float;")) {
  5677.             float val = ei.getFloatField("value");
  5678.             return Float.toString(val);
  5679.         } else if (objectType.equals("Ljava/lang/Long;")) {
  5680.             long val = ei.getLongField("value");
  5681.             return Long.toString(val);
  5682.         } else if (objectType.equals("Ljava/lang/Double;")) {
  5683.             double val = ei.getDoubleField("value");
  5684.             return Double.toString(val);
  5685.         } else if (objectType.equals("Ljava/lang/Boolean;")) {
  5686.             boolean val = ei.getBooleanField("value");
  5687.             return Boolean.toString(val);
  5688.         } else {
  5689.             throw new RuntimeException("ERROR: Object Type Not Handled in getStringVal");
  5690.         }
  5691.     }
  5692.  
  5693.     public Instruction handletoString(JVMInvokeInstruction invInst,  ThreadInfo th) {
  5694.         StackFrame sf = th.getModifiableTopFrame();
  5695.         Object sym_obj_v2 = sf.getOperandAttr(0);
  5696.         if (sym_obj_v2 instanceof StringExpression) {
  5697.             return null;
  5698.         }
  5699.         StringExpression sym_v1 = null;
  5700.         if (sym_obj_v2 instanceof SymbolicStringBuilder) {
  5701.             SymbolicStringBuilder sym_v2 = (SymbolicStringBuilder) sym_obj_v2;
  5702.             sym_v1 = sym_v2.getstr();
  5703.         } else {
  5704.             throw new RuntimeException("ERROR: symbolic type not Handled: toString");
  5705.         }
  5706.  
  5707.         if ((sym_v1 == null)) {
  5708.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: toString");
  5709.         } else {
  5710.             sf.pop();
  5711.             ElementInfo ei = th.getHeap().newString("", th);
  5712.             int objRef = ei.getObjectRef();
  5713.             sf.push(objRef, true);
  5714.             sf.setOperandAttr(sym_v1);
  5715.         }
  5716.         return null;
  5717.     }
  5718.  
  5719.     public void handleprintln(JVMInvokeInstruction invInst, ThreadInfo th, boolean doPrintln) {
  5720.         StackFrame sf = th.getModifiableTopFrame();
  5721.         MethodInfo mi = invInst.getInvokedMethod(th);
  5722.         String[] argTypes = mi.getArgumentTypeNames();
  5723.         Expression sym_v1 = null;
  5724.         boolean flag = false;
  5725.         if ((argTypes[0].equals("long")) || (argTypes[0].equals("double"))) {
  5726.             sym_v1 = (Expression) sf.getLongOperandAttr();
  5727.             flag = true;
  5728.         } else {
  5729.             sym_v1 = (Expression) sf.getOperandAttr(0);
  5730.         }
  5731.  
  5732.         if ((sym_v1 == null)) {
  5733.             throw new RuntimeException("ERROR: symbolic string method must have symbolic operand: println");
  5734.         } else {
  5735.             if (flag)
  5736.                 sf.popLong();
  5737.             else
  5738.                 sf.pop(); // clear out operand stack
  5739.             sf.pop();
  5740.             String result = sym_v1.toString();
  5741.             if (doPrintln) {
  5742.                 System.out.println("Symbolic Exp [ " + result + "]");
  5743.             } else {
  5744.                 System.out.print("Symbolic Exp [ " + result + " ]");
  5745.             }
  5746.             th.getHeap().newString("", th); //Corina this code is so broken
  5747.             //th.push(objRef, true);
  5748.             //sf.setOperandAttr(sym_v1);
  5749.         }
  5750.     }
  5751. }
Tags: Java
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!