src/main/gov/nasa/jpf/listener/StateSpaceAnalyzer.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 package gov.nasa.jpf.listener;
  19
  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;
  41
  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;
  48 import java.util.Map;
  49
  50 /**
  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
  57  *
  58  *  - number of transitions
  59  *  - memory consumption
  60  *  - elapsed time
  61  *
  62  * once the limit is reached, we stop the search and report.
  63  *
  64  * There are two parts we are interested in:
  65  *
  66  *  - what CGs do we have
  67  *  - what creates those CGs (thread,insn,source) = last step insn
  68  */
  69 public class StateSpaceAnalyzer extends ListenerAdapter implements PublisherExtension {
  70   // Search termination conditions
  71
  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;
  80
  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);
  87
  88     initGroupers(config);
  89
  90     jpf.addPublisherExtension(ConsolePublisher.class, this);
  91   }
  92
  93   private void initGroupers(Config config) {
  94     HashMap<String, CGAccessor> accessors;
  95     CGGrouper grouper;
  96     int i;
  97
  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");
 101     }
 102
 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());
 109
 110     m_groupers.add(initGrouper(config, "ssa.sort_order", accessors));
 111
 112     for (i = 2; true; i++) {
 113       grouper = initGrouper(config, "ssa.sort_order" + i, accessors);
 114       if (grouper == null) {
 115         break;
 116       }
 117
 118       m_groupers.add(grouper);
 119     }
 120   }
 121
 122   private CGGrouper initGrouper(Config config, String parameter, Map<String, CGAccessor> accessors) {
 123     CGGrouper grouper;
 124     CGAccessor list[];
 125     StringBuilder name;
 126     String key, sortOrder[];
 127     int i;
 128
 129     sortOrder = config.getStringArray(parameter);
 130     if ((sortOrder == null) || (sortOrder.length <= 0)) {
 131       return (null);
 132     }
 133
 134     name = new StringBuilder();
 135     list = new CGAccessor[sortOrder.length];
 136
 137     for (i = 0; i < sortOrder.length; i++) {
 138       key = sortOrder[i].toLowerCase();
 139       name.append(key);
 140       name.append(", ");
 141
 142       list[i] = accessors.get(key);
 143
 144       if (list[i] == null) {
 145         config.exception("Unknown sort key: " + sortOrder[i] + ".  Found in parameter: " + parameter);
 146       }
 147     }
 148
 149     name.setLength(name.length() - 2);
 150     grouper = new CGGrouper(list, name.toString());
 151
 152     return (grouper);
 153   }
 154
 155   @Override
 156   public void choiceGeneratorSet(VM vm, ChoiceGenerator<?> newCG) {
 157     int i;
 158
 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)
 162
 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.
 169
 170     m_choiceCount += newCG.getTotalNumberOfChoices();
 171
 172     for (i = m_groupers.size(); --i >= 0; )
 173       m_groupers.get(i).add(newCG);
 174   }
 175
 176   @Override
 177   public void searchStarted(Search search) {
 178     int i;
 179
 180     for (i = m_groupers.size(); --i >= 0; )
 181       m_groupers.get(i).clear();
 182
 183     m_choiceCount = 0;
 184     m_terminateTime = m_maxTime + System.currentTimeMillis();
 185   }
 186
 187   @Override
 188   public void stateAdvanced(Search search) {
 189     if (shouldTerminate(search)) {
 190       search.terminate();
 191     }
 192   }
 193
 194   private boolean shouldTerminate(Search search) {
 195     if ((m_maxStates >= 0) && (search.getVM().getStateCount() >= m_maxStates)) {
 196       return (true);
 197     }
 198
 199     if ((m_maxTime >= 0) && (System.currentTimeMillis() >= m_terminateTime)) {
 200       return (true);
 201     }
 202
 203     if ((m_maxMemory >= 0) && (Runtime.getRuntime().totalMemory() >= m_maxMemory)) {
 204       return (true);
 205     }
 206
 207     if ((m_maxChoices >= 0) && (m_choiceCount >= m_maxChoices)) {
 208       return (true);
 209     }
 210
 211     return (false);
 212   }
 213
 214   @Override
 215   public void publishFinished(Publisher publisher) {
 216     CGGrouper groupers[];
 217
 218     groupers = new CGGrouper[m_groupers.size()];
 219     m_groupers.toArray(groupers);
 220
 221     if (publisher instanceof ConsolePublisher) {
 222       new PublishConsole((ConsolePublisher) publisher, groupers, m_maxOutputLines).publish();
 223     }
 224   }
 225
 226   private enum CGType {
 227
 228     FieldAccess,
 229     ObjectWait,
 230     ObjectNotify,
 231     SyncEnter,
 232     SyncExit,
 233     ThreadStart,
 234     ThreadTerminate,
 235     ThreadSuspend,
 236     ThreadResume,
 237     SyncCall,
 238     SyncReturn,
 239     AtomicOp,
 240     DataChoice
 241   }
 242
 243   private interface CGAccessor {
 244
 245     public Object getValue(ChoiceGenerator generator);
 246   }
 247
 248   private static class CGPackageAccessor implements CGAccessor {
 249
 250     @Override
 251         public Object getValue(ChoiceGenerator generator) {
 252       ClassInfo ci;
 253       MethodInfo mi;
 254       Instruction instruction;
 255
 256       instruction = generator.getInsn();
 257       if (instruction == null) {
 258         return (null);
 259       }
 260
 261       mi = instruction.getMethodInfo();
 262       if (mi == null) {
 263         return (null);
 264       }
 265
 266       ci = mi.getClassInfo();
 267       if (ci == null) {
 268         return (null);
 269       }
 270
 271       return (ci.getPackageName());
 272     }
 273   }
 274
 275   private static class CGClassAccessor implements CGAccessor {
 276
 277     @Override
 278         public Object getValue(ChoiceGenerator generator) {
 279       ClassInfo ci;
 280       MethodInfo mi;
 281       Instruction instruction;
 282
 283       instruction = generator.getInsn();
 284       if (instruction == null) {
 285         return (null);
 286       }
 287
 288       mi = instruction.getMethodInfo();
 289       if (mi == null) {
 290         return (null);
 291       }
 292
 293       ci = mi.getClassInfo();
 294       if (ci == null) {
 295         return (null);
 296       }
 297
 298       return (ci.getName());
 299     }
 300   }
 301
 302   private static class CGMethodAccessor implements CGAccessor {
 303
 304     @Override
 305         public Object getValue(ChoiceGenerator generator) {
 306       MethodInfo mi;
 307       Instruction instruction;
 308
 309       instruction = generator.getInsn();
 310       if (instruction == null) {
 311         return (null);
 312       }
 313
 314       mi = instruction.getMethodInfo();
 315       if (mi == null) {
 316         return (null);
 317       }
 318
 319       return (mi.getFullName());
 320     }
 321   }
 322
 323   private static class CGInstructionAccessor implements CGAccessor {
 324
 325     @Override
 326         public Object getValue(ChoiceGenerator generator) {
 327       return (generator.getInsn());
 328     }
 329   }
 330
 331   private static class CGTypeAccessor implements CGAccessor {
 332
 333     private static final String OBJECT_CLASS_NAME = Object.class.getName();
 334     private static final String THREAD_CLASS_NAME = Thread.class.getName();
 335
 336     @Override
 337         public Object getValue(ChoiceGenerator generator) {
 338       if (generator instanceof ThreadChoiceGenerator) {
 339         return (getType((ThreadChoiceGenerator) generator));
 340       }
 341
 342       if (generator instanceof BooleanChoiceGenerator) {
 343         return (CGType.DataChoice);
 344       }
 345
 346       if (generator instanceof DoubleChoiceGenerator) {
 347         return (CGType.DataChoice);
 348       }
 349
 350       if (generator instanceof IntChoiceGenerator) {
 351         return (CGType.DataChoice);
 352       }
 353
 354       if (generator instanceof BooleanChoiceGenerator) {
 355         return (CGType.DataChoice);
 356       }
 357
 358       return (null);
 359     }
 360
 361     private static CGType getType(ThreadChoiceGenerator generator) {
 362       Instruction instruction;
 363
 364       instruction = generator.getInsn();
 365       if (instruction == null) {
 366         return (null);
 367       }
 368
 369       if (instruction instanceof JVMFieldInstruction) {
 370         return (CGType.FieldAccess);
 371       }
 372
 373       if (instruction instanceof JVMInvokeInstruction) {
 374         return (getType((JVMInvokeInstruction) instruction));
 375       }
 376
 377       if (instruction instanceof JVMReturnInstruction) {
 378         return (getType(generator, (JVMReturnInstruction) instruction));
 379       }
 380
 381       if (instruction instanceof MONITORENTER) {
 382         return (CGType.SyncEnter);
 383       }
 384
 385       if (instruction instanceof MONITOREXIT) {
 386         return (CGType.SyncExit);
 387       }
 388
 389       return (null);
 390     }
 391
 392     private static CGType getType(JVMInvokeInstruction instruction) {
 393       MethodInfo mi;
 394
 395       if (is(instruction, OBJECT_CLASS_NAME, "wait")) {
 396         return (CGType.ObjectWait);
 397       }
 398
 399       if (is(instruction, OBJECT_CLASS_NAME, "notify")) {
 400         return (CGType.ObjectNotify);
 401       }
 402
 403       if (is(instruction, OBJECT_CLASS_NAME, "notifyAll")) {
 404         return (CGType.ObjectNotify);
 405       }
 406
 407       if (is(instruction, THREAD_CLASS_NAME, "start")) {
 408         return (CGType.ThreadStart);
 409       }
 410
 411       if (is(instruction, THREAD_CLASS_NAME, "suspend")) {
 412         return (CGType.ThreadSuspend);
 413       }
 414
 415       if (is(instruction, THREAD_CLASS_NAME, "resume")) {
 416         return (CGType.ThreadResume);
 417       }
 418
 419       mi = instruction.getInvokedMethod();
 420       if (mi.getClassName().startsWith("java.util.concurrent.atomic.")) {
 421         return (CGType.AtomicOp);
 422       }
 423
 424       if (mi.isSynchronized()) {
 425         return (CGType.SyncCall);
 426       }
 427
 428       return (null);
 429     }
 430
 431     private static boolean is(JVMInvokeInstruction instruction, String className, String methodName) {
 432       MethodInfo mi;
 433       ClassInfo ci;
 434
 435       mi = instruction.getInvokedMethod();
 436       if (!methodName.equals(mi.getName())) {
 437         return (false);
 438       }
 439
 440       ci = mi.getClassInfo();
 441
 442       if (!className.equals(ci.getName())) {
 443         return (false);
 444       }
 445
 446       return (true);
 447     }
 448
 449     private static CGType getType(ThreadChoiceGenerator generator, JVMReturnInstruction instruction) {
 450       MethodInfo mi;
 451
 452       if (generator.getThreadInfo().getStackDepth() <= 1) // The main thread has 0 frames.  Other threads have 1 frame.
 453       {
 454         return (CGType.ThreadTerminate);
 455       }
 456
 457       mi = instruction.getMethodInfo();
 458       if (mi.isSynchronized()) {
 459         return (CGType.SyncReturn);
 460       }
 461
 462       return (null);
 463     }
 464   }
 465
 466   private static class TreeNode {
 467
 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;
 477
 478     TreeNode(CGAccessor accessors[], int level, Object value) {
 479       m_accessors = accessors;
 480       m_level = level;
 481       m_value = value;
 482
 483       if (level >= accessors.length) {
 484         m_childNodes = null;
 485         m_sortedValues = null;
 486       } else {
 487         m_sortedValues = new ArrayList<Object>();
 488         m_childNodes = new HashMap<Object, TreeNode>();
 489       }
 490     }
 491
 492     public void add(ChoiceGenerator generator) {
 493       TreeNode child;
 494       Object value;
 495
 496       m_generatorCount++;
 497       m_choiceCount += generator.getTotalNumberOfChoices();
 498
 499       if (isLeaf()) {
 500         if (m_sampleGeneratorClassName == null) {
 501           m_sampleGeneratorClassName = generator.getClass().getName();
 502           m_sampleGeneratorInstruction = generator.getInsn();
 503         }
 504
 505         return;
 506       }
 507
 508       value = m_accessors[m_level].getValue(generator);
 509       child = m_childNodes.get(value);
 510       if (child == null) {
 511         child = new TreeNode(m_accessors, m_level + 1, value);
 512         m_childNodes.put(value, child);
 513       }
 514
 515       child.add(generator);
 516     }
 517
 518     public int getLevel() {
 519       return (m_level);
 520     }
 521
 522     public Object getValue() {
 523       return (m_value);
 524     }
 525
 526     public int getChoiceCount() {
 527       return (m_choiceCount);
 528     }
 529
 530     public int getGeneratorCount() {
 531       return (m_generatorCount);
 532     }
 533
 534     public String getSampleGeneratorClassName() {
 535       return (m_sampleGeneratorClassName);
 536     }
 537
 538     public Instruction getSampleGeneratorInstruction() {
 539       return (m_sampleGeneratorInstruction);
 540     }
 541
 542     public boolean isLeaf() {
 543       return (m_childNodes == null);
 544     }
 545
 546     public void sort() {
 547       Comparator<Object> comparator;
 548
 549       if (isLeaf()) {
 550         return;
 551       }
 552
 553       m_sortedValues.clear();
 554       m_sortedValues.addAll(m_childNodes.keySet());
 555
 556       comparator = new Comparator<Object>() {
 557
 558         @Override
 559                 public int compare(Object value1, Object value2) {
 560           TreeNode node1, node2;
 561
 562           node1 = m_childNodes.get(value1);
 563           node2 = m_childNodes.get(value2);
 564
 565           return (node2.getChoiceCount() - node1.getChoiceCount());  // Sort descending
 566         }
 567       };
 568
 569       Collections.sort(m_sortedValues, comparator);
 570
 571       for (TreeNode child : m_childNodes.values()) {
 572         child.sort();
 573       }
 574     }
 575
 576     public List<TreeNode> tour() {
 577       List<TreeNode> result;
 578
 579       result = new ArrayList<TreeNode>();
 580       tour(result);
 581
 582       return (result);
 583     }
 584
 585     public void tour(List<TreeNode> list) {
 586       TreeNode child;
 587       Object value;
 588       int i;
 589
 590       list.add(this);
 591
 592       if (isLeaf()) {
 593         return;
 594       }
 595
 596       for (i = 0; i < m_sortedValues.size(); i++) {
 597         value = m_sortedValues.get(i);
 598         child = m_childNodes.get(value);
 599         child.tour(list);
 600       }
 601     }
 602
 603     @Override
 604         public String toString() {
 605       StringBuilder result;
 606
 607       result = new StringBuilder();
 608
 609       if (m_value == null) {
 610         result.append("(null)");
 611       } else {
 612         result.append(m_value);
 613       }
 614
 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());
 623
 624       return (result.toString());
 625     }
 626   }
 627
 628   private static class CGGrouper {
 629
 630     private final CGAccessor m_accessors[];
 631     private final String m_name;
 632     private       TreeNode m_root;
 633     private       boolean m_sorted;
 634
 635     CGGrouper(CGAccessor accessors[], String name) {
 636       if (accessors.length <= 0) {
 637         throw new IllegalArgumentException("accessors.length <= 0");
 638       }
 639
 640       if (name == null) {
 641         throw new NullPointerException("name == null");
 642       }
 643
 644       m_accessors = accessors;
 645       m_name = name;
 646
 647       clear();
 648     }
 649
 650     public void clear() {
 651       m_sorted = false;
 652       m_root = new TreeNode(m_accessors, 0, "All");
 653     }
 654
 655     public String getName() {
 656       return(m_name);
 657     }
 658
 659     public int getLevelCount() {
 660       return(m_accessors.length);
 661     }
 662
 663     public TreeNode getTree() {
 664       if (!m_sorted) {
 665         m_sorted = true;
 666         m_root.sort();
 667       }
 668
 669       return(m_root);
 670     }
 671
 672     public void add(ChoiceGenerator generator) {
 673       m_sorted = false;
 674       m_root.add(generator);
 675     }
 676   }
 677
 678   private static abstract class Publish {
 679
 680     protected final Publisher m_publisher;
 681     protected final CGGrouper m_groupers[];
 682     protected final int m_maxOutputLines;
 683     protected PrintWriter m_output;
 684
 685     Publish(Publisher publisher, CGGrouper groupers[], int maxOutputLines) {
 686       m_publisher = publisher;
 687       m_groupers = groupers;
 688       m_maxOutputLines = maxOutputLines;
 689     }
 690
 691     public abstract void publish();
 692   }
 693
 694   private static class PublishConsole extends Publish {
 695
 696     PublishConsole(ConsolePublisher publisher, CGGrouper[] groupers, int maxOutputLines) {
 697       super(publisher, groupers, maxOutputLines);
 698       m_output = publisher.getOut();
 699     }
 700
 701     @Override
 702         public void publish() {
 703       int i;
 704
 705       for (i = 0; i < m_groupers.length; i++) {
 706         publishSortedData(m_groupers[i]);
 707       }
 708     }
 709
 710     private void publishSortedData(CGGrouper grouper) {
 711       List<TreeNode> tour;
 712       TreeNode node;
 713       int i, lines, levelCount;
 714
 715       lines = 0;
 716       levelCount = grouper.getLevelCount();
 717       node = grouper.getTree();
 718       tour = node.tour();
 719
 720       m_publisher.publishTopicStart("Grouped By: " + grouper.getName());
 721
 722       for (i = 0; (i < tour.size()) && (lines < m_maxOutputLines); i++) {
 723         node = tour.get(i);
 724
 725         publishTreeNode(node);
 726
 727         if (node.isLeaf()) {
 728           publishDetails(node, levelCount + 1);
 729           lines++;
 730         }
 731       }
 732
 733       if (lines >= m_maxOutputLines) {
 734         m_output.println("...");
 735       }
 736     }
 737
 738     private void publishTreeNode(TreeNode node) {
 739       Object value;
 740
 741       // Tree
 742       publishPadding(node.getLevel());
 743
 744       value = node.getValue();
 745       if (value == null) {
 746         m_output.print("(null)");
 747       } else {
 748         m_output.print(value);
 749       }
 750
 751       // Choices
 752       m_output.print("  (choices: ");
 753       m_output.print(node.getChoiceCount());
 754
 755       // Generators
 756       m_output.print(", generators: ");
 757       m_output.print(node.getGeneratorCount());
 758
 759       m_output.println(')');
 760     }
 761
 762     private void publishDetails(TreeNode node, int levelCount) {
 763       ChoiceGenerator generator;
 764       Instruction instruction;
 765
 766       instruction = node.getSampleGeneratorInstruction();
 767
 768       // Location
 769       publishPadding(levelCount);
 770       m_output.print("Location:  ");
 771       m_output.println(instruction.getFileLocation());
 772
 773       // Code
 774       publishPadding(levelCount);
 775       m_output.print("Code:  ");
 776       m_output.println(instruction.getSourceOrLocation().trim());
 777
 778       // Instruction
 779       publishPadding(levelCount);
 780       m_output.print("Instruction:  ");
 781       m_output.println(instruction.getMnemonic());
 782
 783       // Position
 784       publishPadding(levelCount);
 785       m_output.print("Position:  ");
 786       m_output.println(instruction.getPosition());
 787
 788       // Generator Class
 789       publishPadding(levelCount);
 790       m_output.print("Generator Class:  ");
 791       m_output.println(node.getSampleGeneratorClassName());
 792     }
 793
 794     private void publishPadding(int levelCount) {
 795       int i;
 796
 797       for (i = levelCount; i > 0; i--) {
 798         m_output.print("   ");
 799       }
 800     }
 801   }
 802 }