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.
18 package gov.nasa.jpf.listener;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.JPF;
22 import gov.nasa.jpf.ListenerAdapter;
23 import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
24 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
25 import gov.nasa.jpf.jvm.bytecode.MONITORENTER;
26 import gov.nasa.jpf.jvm.bytecode.MONITOREXIT;
27 import gov.nasa.jpf.jvm.bytecode.JVMReturnInstruction;
28 import gov.nasa.jpf.report.ConsolePublisher;
29 import gov.nasa.jpf.report.Publisher;
30 import gov.nasa.jpf.report.PublisherExtension;
31 import gov.nasa.jpf.search.Search;
32 import gov.nasa.jpf.vm.BooleanChoiceGenerator;
33 import gov.nasa.jpf.vm.ChoiceGenerator;
34 import gov.nasa.jpf.vm.ClassInfo;
35 import gov.nasa.jpf.vm.DoubleChoiceGenerator;
36 import gov.nasa.jpf.vm.Instruction;
37 import gov.nasa.jpf.vm.IntChoiceGenerator;
38 import gov.nasa.jpf.vm.VM;
39 import gov.nasa.jpf.vm.MethodInfo;
40 import gov.nasa.jpf.vm.ThreadChoiceGenerator;
42 import java.io.PrintWriter;
43 import java.util.ArrayList;
44 import java.util.Collections;
45 import java.util.Comparator;
46 import java.util.HashMap;
47 import java.util.List;
51 * a listener that collects information about ChoiceGenerators, choices and
52 * where they are used. The purpose is to find out what causes the state space
53 * size, and to give hints of how to reduce it.
54 * The interesting part is that this is a listener that doesn't work off traces,
55 * but needs to collect info up to a point where we want it to report. That's
56 * state space or resource related, i.e. a combination of
58 * - number of transitions
59 * - memory consumption
62 * once the limit is reached, we stop the search and report.
64 * There are two parts we are interested in:
66 * - what CGs do we have
67 * - what creates those CGs (thread,insn,source) = last step insn
69 public class StateSpaceAnalyzer extends ListenerAdapter implements PublisherExtension {
70 // Search termination conditions
72 private final long m_maxTime;
73 private final long m_maxMemory;
74 private final int m_maxStates;
75 private final int m_maxChoices;
76 private final ArrayList<CGGrouper> m_groupers = new ArrayList<CGGrouper>();
77 private final int m_maxOutputLines; // how many detail lines do we display in the report
78 private long m_terminateTime;
79 private int m_choiceCount;
81 public StateSpaceAnalyzer(Config config, JPF jpf) {
82 m_maxStates = config.getInt("ssa.max_states", -1);
83 m_maxTime = config.getDuration("ssa.max_time", -1);
84 m_maxMemory = config.getMemorySize("ssa.max_memory", -1);
85 m_maxChoices = config.getInt("ssa.max_choices", -1);
86 m_maxOutputLines = config.getInt("ssa.max_output_lines", 10);
90 jpf.addPublisherExtension(ConsolePublisher.class, this);
93 private void initGroupers(Config config) {
94 HashMap<String, CGAccessor> accessors;
98 if (config.getStringArray("ssa.sort_order") == null) {
99 config.setProperty("ssa.sort_order", "type");
100 config.setProperty("ssa.sort_order2", "package,class,method,instruction,type");
103 accessors = new HashMap<String, CGAccessor>(5);
104 accessors.put("package", new CGPackageAccessor());
105 accessors.put("class", new CGClassAccessor());
106 accessors.put("method", new CGMethodAccessor());
107 accessors.put("instruction", new CGInstructionAccessor());
108 accessors.put("type", new CGTypeAccessor());
110 m_groupers.add(initGrouper(config, "ssa.sort_order", accessors));
112 for (i = 2; true; i++) {
113 grouper = initGrouper(config, "ssa.sort_order" + i, accessors);
114 if (grouper == null) {
118 m_groupers.add(grouper);
122 private CGGrouper initGrouper(Config config, String parameter, Map<String, CGAccessor> accessors) {
126 String key, sortOrder[];
129 sortOrder = config.getStringArray(parameter);
130 if ((sortOrder == null) || (sortOrder.length <= 0)) {
134 name = new StringBuilder();
135 list = new CGAccessor[sortOrder.length];
137 for (i = 0; i < sortOrder.length; i++) {
138 key = sortOrder[i].toLowerCase();
142 list[i] = accessors.get(key);
144 if (list[i] == null) {
145 config.exception("Unknown sort key: " + sortOrder[i] + ". Found in parameter: " + parameter);
149 name.setLength(name.length() - 2);
150 grouper = new CGGrouper(list, name.toString());
156 public void choiceGeneratorSet(VM vm, ChoiceGenerator<?> newCG) {
159 // NOTE: we get this from SystemState.nextSuccessor, i.e. when the CG
160 // is actually used (which doesn't necessarily mean it produces a new state,
161 // but it got created from a new state)
163 // The original code stored each choice generator in an ArrayList. For long
164 // running tests, this would grow and cause an OutOfMemoryError. Now, the
165 // generators are dealt with as they are created. This means a bit more
166 // processing up front but huge memory savings in the long run. If the
167 // machine has multiple processors, a better solution would be to have a
168 // background thread process the generators.
170 m_choiceCount += newCG.getTotalNumberOfChoices();
172 for (i = m_groupers.size(); --i >= 0; )
173 m_groupers.get(i).add(newCG);
177 public void searchStarted(Search search) {
180 for (i = m_groupers.size(); --i >= 0; )
181 m_groupers.get(i).clear();
184 m_terminateTime = m_maxTime + System.currentTimeMillis();
188 public void stateAdvanced(Search search) {
189 if (shouldTerminate(search)) {
194 private boolean shouldTerminate(Search search) {
195 if ((m_maxStates >= 0) && (search.getVM().getStateCount() >= m_maxStates)) {
199 if ((m_maxTime >= 0) && (System.currentTimeMillis() >= m_terminateTime)) {
203 if ((m_maxMemory >= 0) && (Runtime.getRuntime().totalMemory() >= m_maxMemory)) {
207 if ((m_maxChoices >= 0) && (m_choiceCount >= m_maxChoices)) {
215 public void publishFinished(Publisher publisher) {
216 CGGrouper groupers[];
218 groupers = new CGGrouper[m_groupers.size()];
219 m_groupers.toArray(groupers);
221 if (publisher instanceof ConsolePublisher) {
222 new PublishConsole((ConsolePublisher) publisher, groupers, m_maxOutputLines).publish();
226 private enum CGType {
243 private interface CGAccessor {
245 public Object getValue(ChoiceGenerator generator);
248 private static class CGPackageAccessor implements CGAccessor {
251 public Object getValue(ChoiceGenerator generator) {
254 Instruction instruction;
256 instruction = generator.getInsn();
257 if (instruction == null) {
261 mi = instruction.getMethodInfo();
266 ci = mi.getClassInfo();
271 return (ci.getPackageName());
275 private static class CGClassAccessor implements CGAccessor {
278 public Object getValue(ChoiceGenerator generator) {
281 Instruction instruction;
283 instruction = generator.getInsn();
284 if (instruction == null) {
288 mi = instruction.getMethodInfo();
293 ci = mi.getClassInfo();
298 return (ci.getName());
302 private static class CGMethodAccessor implements CGAccessor {
305 public Object getValue(ChoiceGenerator generator) {
307 Instruction instruction;
309 instruction = generator.getInsn();
310 if (instruction == null) {
314 mi = instruction.getMethodInfo();
319 return (mi.getFullName());
323 private static class CGInstructionAccessor implements CGAccessor {
326 public Object getValue(ChoiceGenerator generator) {
327 return (generator.getInsn());
331 private static class CGTypeAccessor implements CGAccessor {
333 private static final String OBJECT_CLASS_NAME = Object.class.getName();
334 private static final String THREAD_CLASS_NAME = Thread.class.getName();
337 public Object getValue(ChoiceGenerator generator) {
338 if (generator instanceof ThreadChoiceGenerator) {
339 return (getType((ThreadChoiceGenerator) generator));
342 if (generator instanceof BooleanChoiceGenerator) {
343 return (CGType.DataChoice);
346 if (generator instanceof DoubleChoiceGenerator) {
347 return (CGType.DataChoice);
350 if (generator instanceof IntChoiceGenerator) {
351 return (CGType.DataChoice);
354 if (generator instanceof BooleanChoiceGenerator) {
355 return (CGType.DataChoice);
361 private static CGType getType(ThreadChoiceGenerator generator) {
362 Instruction instruction;
364 instruction = generator.getInsn();
365 if (instruction == null) {
369 if (instruction instanceof JVMFieldInstruction) {
370 return (CGType.FieldAccess);
373 if (instruction instanceof JVMInvokeInstruction) {
374 return (getType((JVMInvokeInstruction) instruction));
377 if (instruction instanceof JVMReturnInstruction) {
378 return (getType(generator, (JVMReturnInstruction) instruction));
381 if (instruction instanceof MONITORENTER) {
382 return (CGType.SyncEnter);
385 if (instruction instanceof MONITOREXIT) {
386 return (CGType.SyncExit);
392 private static CGType getType(JVMInvokeInstruction instruction) {
395 if (is(instruction, OBJECT_CLASS_NAME, "wait")) {
396 return (CGType.ObjectWait);
399 if (is(instruction, OBJECT_CLASS_NAME, "notify")) {
400 return (CGType.ObjectNotify);
403 if (is(instruction, OBJECT_CLASS_NAME, "notifyAll")) {
404 return (CGType.ObjectNotify);
407 if (is(instruction, THREAD_CLASS_NAME, "start")) {
408 return (CGType.ThreadStart);
411 if (is(instruction, THREAD_CLASS_NAME, "suspend")) {
412 return (CGType.ThreadSuspend);
415 if (is(instruction, THREAD_CLASS_NAME, "resume")) {
416 return (CGType.ThreadResume);
419 mi = instruction.getInvokedMethod();
420 if (mi.getClassName().startsWith("java.util.concurrent.atomic.")) {
421 return (CGType.AtomicOp);
424 if (mi.isSynchronized()) {
425 return (CGType.SyncCall);
431 private static boolean is(JVMInvokeInstruction instruction, String className, String methodName) {
435 mi = instruction.getInvokedMethod();
436 if (!methodName.equals(mi.getName())) {
440 ci = mi.getClassInfo();
442 if (!className.equals(ci.getName())) {
449 private static CGType getType(ThreadChoiceGenerator generator, JVMReturnInstruction instruction) {
452 if (generator.getThreadInfo().getStackDepth() <= 1) // The main thread has 0 frames. Other threads have 1 frame.
454 return (CGType.ThreadTerminate);
457 mi = instruction.getMethodInfo();
458 if (mi.isSynchronized()) {
459 return (CGType.SyncReturn);
466 private static class TreeNode {
468 private final HashMap<Object, TreeNode> m_childNodes;
469 private final ArrayList<Object> m_sortedValues;
470 private final CGAccessor m_accessors[];
471 private final Object m_value;
472 private final int m_level;
473 private String m_sampleGeneratorClassName;
474 private Instruction m_sampleGeneratorInstruction;
475 private int m_choiceCount;
476 private int m_generatorCount;
478 TreeNode(CGAccessor accessors[], int level, Object value) {
479 m_accessors = accessors;
483 if (level >= accessors.length) {
485 m_sortedValues = null;
487 m_sortedValues = new ArrayList<Object>();
488 m_childNodes = new HashMap<Object, TreeNode>();
492 public void add(ChoiceGenerator generator) {
497 m_choiceCount += generator.getTotalNumberOfChoices();
500 if (m_sampleGeneratorClassName == null) {
501 m_sampleGeneratorClassName = generator.getClass().getName();
502 m_sampleGeneratorInstruction = generator.getInsn();
508 value = m_accessors[m_level].getValue(generator);
509 child = m_childNodes.get(value);
511 child = new TreeNode(m_accessors, m_level + 1, value);
512 m_childNodes.put(value, child);
515 child.add(generator);
518 public int getLevel() {
522 public Object getValue() {
526 public int getChoiceCount() {
527 return (m_choiceCount);
530 public int getGeneratorCount() {
531 return (m_generatorCount);
534 public String getSampleGeneratorClassName() {
535 return (m_sampleGeneratorClassName);
538 public Instruction getSampleGeneratorInstruction() {
539 return (m_sampleGeneratorInstruction);
542 public boolean isLeaf() {
543 return (m_childNodes == null);
547 Comparator<Object> comparator;
553 m_sortedValues.clear();
554 m_sortedValues.addAll(m_childNodes.keySet());
556 comparator = new Comparator<Object>() {
559 public int compare(Object value1, Object value2) {
560 TreeNode node1, node2;
562 node1 = m_childNodes.get(value1);
563 node2 = m_childNodes.get(value2);
565 return (node2.getChoiceCount() - node1.getChoiceCount()); // Sort descending
569 Collections.sort(m_sortedValues, comparator);
571 for (TreeNode child : m_childNodes.values()) {
576 public List<TreeNode> tour() {
577 List<TreeNode> result;
579 result = new ArrayList<TreeNode>();
585 public void tour(List<TreeNode> list) {
596 for (i = 0; i < m_sortedValues.size(); i++) {
597 value = m_sortedValues.get(i);
598 child = m_childNodes.get(value);
604 public String toString() {
605 StringBuilder result;
607 result = new StringBuilder();
609 if (m_value == null) {
610 result.append("(null)");
612 result.append(m_value);
615 result.append(" - L");
616 result.append(m_level);
617 result.append(" / C");
618 result.append(m_choiceCount);
619 result.append(" / G");
620 result.append(m_generatorCount);
621 result.append(" / N");
622 result.append(m_childNodes.size());
624 return (result.toString());
628 private static class CGGrouper {
630 private final CGAccessor m_accessors[];
631 private final String m_name;
632 private TreeNode m_root;
633 private boolean m_sorted;
635 CGGrouper(CGAccessor accessors[], String name) {
636 if (accessors.length <= 0) {
637 throw new IllegalArgumentException("accessors.length <= 0");
641 throw new NullPointerException("name == null");
644 m_accessors = accessors;
650 public void clear() {
652 m_root = new TreeNode(m_accessors, 0, "All");
655 public String getName() {
659 public int getLevelCount() {
660 return(m_accessors.length);
663 public TreeNode getTree() {
672 public void add(ChoiceGenerator generator) {
674 m_root.add(generator);
678 private static abstract class Publish {
680 protected final Publisher m_publisher;
681 protected final CGGrouper m_groupers[];
682 protected final int m_maxOutputLines;
683 protected PrintWriter m_output;
685 Publish(Publisher publisher, CGGrouper groupers[], int maxOutputLines) {
686 m_publisher = publisher;
687 m_groupers = groupers;
688 m_maxOutputLines = maxOutputLines;
691 public abstract void publish();
694 private static class PublishConsole extends Publish {
696 PublishConsole(ConsolePublisher publisher, CGGrouper[] groupers, int maxOutputLines) {
697 super(publisher, groupers, maxOutputLines);
698 m_output = publisher.getOut();
702 public void publish() {
705 for (i = 0; i < m_groupers.length; i++) {
706 publishSortedData(m_groupers[i]);
710 private void publishSortedData(CGGrouper grouper) {
713 int i, lines, levelCount;
716 levelCount = grouper.getLevelCount();
717 node = grouper.getTree();
720 m_publisher.publishTopicStart("Grouped By: " + grouper.getName());
722 for (i = 0; (i < tour.size()) && (lines < m_maxOutputLines); i++) {
725 publishTreeNode(node);
728 publishDetails(node, levelCount + 1);
733 if (lines >= m_maxOutputLines) {
734 m_output.println("...");
738 private void publishTreeNode(TreeNode node) {
742 publishPadding(node.getLevel());
744 value = node.getValue();
746 m_output.print("(null)");
748 m_output.print(value);
752 m_output.print(" (choices: ");
753 m_output.print(node.getChoiceCount());
756 m_output.print(", generators: ");
757 m_output.print(node.getGeneratorCount());
759 m_output.println(')');
762 private void publishDetails(TreeNode node, int levelCount) {
763 ChoiceGenerator generator;
764 Instruction instruction;
766 instruction = node.getSampleGeneratorInstruction();
769 publishPadding(levelCount);
770 m_output.print("Location: ");
771 m_output.println(instruction.getFileLocation());
774 publishPadding(levelCount);
775 m_output.print("Code: ");
776 m_output.println(instruction.getSourceOrLocation().trim());
779 publishPadding(levelCount);
780 m_output.print("Instruction: ");
781 m_output.println(instruction.getMnemonic());
784 publishPadding(levelCount);
785 m_output.print("Position: ");
786 m_output.println(instruction.getPosition());
789 publishPadding(levelCount);
790 m_output.print("Generator Class: ");
791 m_output.println(node.getSampleGeneratorClassName());
794 private void publishPadding(int levelCount) {
797 for (i = levelCount; i > 0; i--) {