src/main/gov/nasa/jpf/listener/CGRemover.java

   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  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, 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 package gov.nasa.jpf.listener;
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.ListenerAdapter;
  24 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
  25 import gov.nasa.jpf.util.JPFLogger;
  26 import gov.nasa.jpf.util.LocationSpec;
  27 import gov.nasa.jpf.util.MethodSpec;
  28 import gov.nasa.jpf.vm.ChoiceGenerator;
  29 import gov.nasa.jpf.vm.ClassInfo;
  30 import gov.nasa.jpf.vm.Instruction;
  31 import gov.nasa.jpf.vm.ThreadInfo;
  32 import gov.nasa.jpf.vm.VM;
  33 import gov.nasa.jpf.vm.MethodInfo;
  34
  35 import java.util.ArrayList;
  36 import java.util.HashMap;
  37 import java.util.List;
  38
  39 /**
  40  * listener that removes CGs for specified locations, method calls or method bodies
  41  *
  42  * This is an application specific state space optimizer that should be used
  43  * carefully since it has to be aware of which CGs can be removed, and which
  44  * ones can't (e.g. blocking sync or wait). You also have to be aware of the
  45  * order of listener registration, since subsequently registered listeners can
  46  * still add new CGs after they got removed here. THIS IS ONLY AN OPTIMIZATION
  47  * TOOL THAT SHOULD BE USED IN A WELL KNOWN APPLICATION CONTEXT.
  48  *
  49  *  cgrm.thread.cg_class = gov.nasa.jpf.vm.ThreadChoiceGenerator
  50  *  cgrm.thread.locations = Foobar.java:42                // either a LocationSpec
  51  *  cgrm.thread.method_bodies = a.SomeClass.someMethod()  // ..or a MethodSpec for a body
  52  *  cgrm.thread.method_calls = b.A.foo(int)               // ..or a MethodSpec for a call
  53  *
  54  * NOTE: in its current implementation, this listener has to be registered
  55  * before targeted classes are loaded
  56  */
  57 public class CGRemover extends ListenerAdapter {
  58
  59   static JPFLogger log = JPF.getLogger("gov.nasa.jpf.CGRemover");
  60
  61   static class Category {
  62     String id;
  63
  64     Class<?> cgClass;
  65
  66     ArrayList<LocationSpec> locations = new ArrayList<LocationSpec>();
  67     ArrayList<MethodSpec> methodBodies = new ArrayList<MethodSpec>();
  68     ArrayList<MethodSpec> methodCalls = new ArrayList<MethodSpec>();
  69
  70     Category (String id){
  71       this.id = id;
  72     }
  73
  74     boolean checkSpecification() {
  75       return cgClass != null &&
  76               (!locations.isEmpty() || !methodBodies.isEmpty() || !methodCalls.isEmpty());
  77     }
  78   }
  79
  80   List<Category> categories;
  81
  82   HashMap<MethodInfo,Category> methodBodies;
  83   HashMap<MethodInfo,Category> methodCalls;
  84   HashMap<Instruction,Category> locations;
  85
  86
  87   public CGRemover (Config conf){
  88     categories = parseCategories(conf);
  89   }
  90
  91   protected List<Category> parseCategories (Config conf){
  92     ArrayList<Category> list = new ArrayList<Category>();
  93     Category category = null;
  94
  95     for (String key : conf.getKeysStartingWith("cgrm.")){
  96       String[] kc = conf.getKeyComponents(key);
  97       if (kc.length == 3){
  98         String k = kc[1];
  99         if (category != null){
 100           if (!category.id.equals(k)){
 101             addCategory(list, category);
 102
 103             category = new Category(k);
 104           }
 105         } else {
 106           category = new Category(k);
 107         }
 108
 109         k = kc[2];
 110
 111         if ("cg_class".equals(k)){
 112           category.cgClass = conf.getClass(key);
 113
 114         } else if ("locations".equals(k)){
 115           parseLocationSpecs(category.locations, conf.getStringArray(key));
 116
 117         } else if ("method_bodies".equals(k)){
 118           parseMethodSpecs(category.methodBodies, conf.getStringArray(key));
 119
 120         } else if ("method_calls".equals(k)){
 121           parseMethodSpecs(category.methodCalls, conf.getStringArray(key));
 122
 123         } else {
 124           // we might have more options in the future
 125           log.warning("illegal CGRemover option: ", key);
 126         }
 127
 128       } else {
 129         log.warning("illegal CGRemover key: ", key);
 130       }
 131     }
 132
 133     addCategory(list, category);
 134     return list;
 135   }
 136
 137   protected void addCategory (List<Category> list, Category cat){
 138     if (cat != null) {
 139       if (cat.checkSpecification()) {
 140         list.add(cat);
 141         log.info("added category: ", cat.id);
 142       } else {
 143         log.warning("incomplete CGRemover category: ", cat.id);
 144       }
 145     }
 146   }
 147
 148   protected void parseLocationSpecs (List<LocationSpec> list, String[] specs){
 149     for (String spec : specs) {
 150       LocationSpec locSpec = LocationSpec.createLocationSpec(spec);
 151       if (locSpec != null) {
 152         if (locSpec.isAnyLine()){
 153           log.warning("whole file location specs not supported by CGRemover (use cgrm...method_bodies)");
 154         } else {
 155           list.add(locSpec);
 156         }
 157       } else {
 158         log.warning("location spec did not parse: ", spec);
 159       }
 160     }
 161   }
 162
 163   protected void parseMethodSpecs (List<MethodSpec> list, String[] specs){
 164     for (String spec : specs) {
 165       MethodSpec mthSpec = MethodSpec.createMethodSpec(spec);
 166       if (mthSpec != null) {
 167         list.add(mthSpec);
 168       } else {
 169         log.warning("methos spec did not parse: ", spec);
 170       }
 171     }
 172   }
 173
 174
 175   protected void processClass (ClassInfo ci, Category cat){
 176     String fname = ci.getSourceFileName();
 177
 178     for (LocationSpec loc : cat.locations){
 179       if (loc.matchesFile(fname)){ // Ok, we have to dig out the corresponding insns (if any)
 180         Instruction[] insns = ci.getMatchingInstructions(loc);
 181         if (insns != null){
 182           if (locations == null){
 183             locations = new HashMap<Instruction,Category>();
 184           }
 185           for (Instruction insn : insns){
 186             locations.put(insn, cat);
 187           }
 188         } else {
 189           log.warning("no insns for location: ", loc, " in class: ", ci.getName());
 190         }
 191       }
 192     }
 193
 194     for (MethodSpec ms : cat.methodBodies){
 195       List<MethodInfo> list = ci.getMatchingMethodInfos(ms);
 196       if (list != null){
 197         for (MethodInfo mi : list){
 198           if (methodBodies == null){
 199             methodBodies = new HashMap<MethodInfo,Category>();
 200           }
 201           methodBodies.put(mi, cat);
 202         }
 203       }
 204     }
 205
 206     for (MethodSpec ms : cat.methodCalls){
 207       List<MethodInfo> list = ci.getMatchingMethodInfos(ms);
 208       if (list != null){
 209         for (MethodInfo mi : list){
 210           if (methodCalls == null){
 211             methodCalls = new HashMap<MethodInfo,Category>();
 212           }
 213           methodCalls.put(mi, cat);
 214         }
 215       }
 216     }
 217   }
 218
 219   protected boolean removeCG (VM vm, Category cat, ChoiceGenerator<?> cg){
 220     if (cat != null){
 221       if (cat.cgClass.isAssignableFrom(cg.getClass())){
 222         vm.getSystemState().removeNextChoiceGenerator();
 223         log.info("removed CG: ", cg);
 224         return true;
 225       }
 226     }
 227
 228     return false;
 229   }
 230
 231   //--- VMListener interface
 232
 233   // this is where we turn Categories into MethodInfos and Instructions to watch out for
 234   @Override
 235   public void classLoaded (VM vm, ClassInfo loadedClass){
 236     for (Category cat : categories){
 237       processClass(loadedClass, cat);
 238     }
 239   }
 240
 241   // this is our main purpose in life
 242   @Override
 243   public void choiceGeneratorRegistered (VM vm, ChoiceGenerator<?> nextCG, ThreadInfo ti, Instruction executedInsn){
 244     ChoiceGenerator<?> cg = vm.getNextChoiceGenerator();
 245     Instruction insn = cg.getInsn();
 246
 247     if (locations != null){
 248       if ( removeCG(vm, locations.get(insn), cg)){
 249         return;
 250       }
 251     }
 252
 253     if (insn instanceof JVMInvokeInstruction){
 254       MethodInfo invokedMi = ((JVMInvokeInstruction)insn).getInvokedMethod();
 255       if (methodCalls != null) {
 256         if (removeCG(vm, methodCalls.get(invokedMi), cg)) {
 257           return;
 258         }
 259       }
 260     }
 261
 262     if (methodBodies != null){
 263       if (removeCG(vm, methodBodies.get(insn.getMethodInfo()), cg)) {
 264         return;
 265       }
 266     }
 267   }
 268 }