2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
19 package gov.nasa.jpf.listener;
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;
35 import java.util.ArrayList;
36 import java.util.HashMap;
37 import java.util.List;
40 * listener that removes CGs for specified locations, method calls or method bodies
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.
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
54 * NOTE: in its current implementation, this listener has to be registered
55 * before targeted classes are loaded
57 public class CGRemover extends ListenerAdapter {
59 static JPFLogger log = JPF.getLogger("gov.nasa.jpf.CGRemover");
61 static class Category {
66 ArrayList<LocationSpec> locations = new ArrayList<LocationSpec>();
67 ArrayList<MethodSpec> methodBodies = new ArrayList<MethodSpec>();
68 ArrayList<MethodSpec> methodCalls = new ArrayList<MethodSpec>();
74 boolean checkSpecification() {
75 return cgClass != null &&
76 (!locations.isEmpty() || !methodBodies.isEmpty() || !methodCalls.isEmpty());
80 List<Category> categories;
82 HashMap<MethodInfo,Category> methodBodies;
83 HashMap<MethodInfo,Category> methodCalls;
84 HashMap<Instruction,Category> locations;
87 public CGRemover (Config conf){
88 categories = parseCategories(conf);
91 protected List<Category> parseCategories (Config conf){
92 ArrayList<Category> list = new ArrayList<Category>();
93 Category category = null;
95 for (String key : conf.getKeysStartingWith("cgrm.")){
96 String[] kc = conf.getKeyComponents(key);
99 if (category != null){
100 if (!category.id.equals(k)){
101 addCategory(list, category);
103 category = new Category(k);
106 category = new Category(k);
111 if ("cg_class".equals(k)){
112 category.cgClass = conf.getClass(key);
114 } else if ("locations".equals(k)){
115 parseLocationSpecs(category.locations, conf.getStringArray(key));
117 } else if ("method_bodies".equals(k)){
118 parseMethodSpecs(category.methodBodies, conf.getStringArray(key));
120 } else if ("method_calls".equals(k)){
121 parseMethodSpecs(category.methodCalls, conf.getStringArray(key));
124 // we might have more options in the future
125 log.warning("illegal CGRemover option: ", key);
129 log.warning("illegal CGRemover key: ", key);
133 addCategory(list, category);
137 protected void addCategory (List<Category> list, Category cat){
139 if (cat.checkSpecification()) {
141 log.info("added category: ", cat.id);
143 log.warning("incomplete CGRemover category: ", cat.id);
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)");
158 log.warning("location spec did not parse: ", spec);
163 protected void parseMethodSpecs (List<MethodSpec> list, String[] specs){
164 for (String spec : specs) {
165 MethodSpec mthSpec = MethodSpec.createMethodSpec(spec);
166 if (mthSpec != null) {
169 log.warning("methos spec did not parse: ", spec);
175 protected void processClass (ClassInfo ci, Category cat){
176 String fname = ci.getSourceFileName();
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);
182 if (locations == null){
183 locations = new HashMap<Instruction,Category>();
185 for (Instruction insn : insns){
186 locations.put(insn, cat);
189 log.warning("no insns for location: ", loc, " in class: ", ci.getName());
194 for (MethodSpec ms : cat.methodBodies){
195 List<MethodInfo> list = ci.getMatchingMethodInfos(ms);
197 for (MethodInfo mi : list){
198 if (methodBodies == null){
199 methodBodies = new HashMap<MethodInfo,Category>();
201 methodBodies.put(mi, cat);
206 for (MethodSpec ms : cat.methodCalls){
207 List<MethodInfo> list = ci.getMatchingMethodInfos(ms);
209 for (MethodInfo mi : list){
210 if (methodCalls == null){
211 methodCalls = new HashMap<MethodInfo,Category>();
213 methodCalls.put(mi, cat);
219 protected boolean removeCG (VM vm, Category cat, ChoiceGenerator<?> cg){
221 if (cat.cgClass.isAssignableFrom(cg.getClass())){
222 vm.getSystemState().removeNextChoiceGenerator();
223 log.info("removed CG: ", cg);
231 //--- VMListener interface
233 // this is where we turn Categories into MethodInfos and Instructions to watch out for
235 public void classLoaded (VM vm, ClassInfo loadedClass){
236 for (Category cat : categories){
237 processClass(loadedClass, cat);
241 // this is our main purpose in life
243 public void choiceGeneratorRegistered (VM vm, ChoiceGenerator<?> nextCG, ThreadInfo ti, Instruction executedInsn){
244 ChoiceGenerator<?> cg = vm.getNextChoiceGenerator();
245 Instruction insn = cg.getInsn();
247 if (locations != null){
248 if ( removeCG(vm, locations.get(insn), cg)){
253 if (insn instanceof JVMInvokeInstruction){
254 MethodInfo invokedMi = ((JVMInvokeInstruction)insn).getInvokedMethod();
255 if (methodCalls != null) {
256 if (removeCG(vm, methodCalls.get(invokedMi), cg)) {
262 if (methodBodies != null){
263 if (removeCG(vm, methodBodies.get(insn.getMethodInfo()), cg)) {