src/main/gov/nasa/jpf/listener/CoverageAnalyzer.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.GOTO;
  24 import gov.nasa.jpf.jvm.bytecode.IfInstruction;
  25 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
  26 import gov.nasa.jpf.jvm.bytecode.JVMReturnInstruction;
  27 import gov.nasa.jpf.report.ConsolePublisher;
  28 import gov.nasa.jpf.report.Publisher;
  29 import gov.nasa.jpf.report.PublisherExtension;
  30 import gov.nasa.jpf.util.Misc;
  31 import gov.nasa.jpf.util.StringSetMatcher;
  32 import gov.nasa.jpf.vm.AnnotationInfo;
  33 import gov.nasa.jpf.vm.ChoiceGenerator;
  34 import gov.nasa.jpf.vm.ClassInfo;
  35 import gov.nasa.jpf.vm.ClassInfoException;
  36 import gov.nasa.jpf.vm.ClassLoaderInfo;
  37 import gov.nasa.jpf.vm.ExceptionHandler;
  38 import gov.nasa.jpf.vm.Instruction;
  39 import gov.nasa.jpf.vm.VM;
  40 import gov.nasa.jpf.vm.MethodInfo;
  41 import gov.nasa.jpf.vm.ThreadInfo;
  42
  43 import java.io.File;
  44 import java.io.IOException;
  45 import java.io.PrintWriter;
  46 import java.util.ArrayList;
  47 import java.util.BitSet;
  48 import java.util.Comparator;
  49 import java.util.Enumeration;
  50 import java.util.HashMap;
  51 import java.util.HashSet;
  52 import java.util.List;
  53 import java.util.Map;
  54 import java.util.jar.JarEntry;
  55 import java.util.jar.JarFile;
  56 import java.util.logging.Logger;
  57
  58 /**
  59  * a listener to report coverage statistics
  60  *
  61  * The idea is to collect per-class/-method/-thread information about
  62  * executed instructions, and then analyze this deeper when it comes to
  63  * report time (e.g. branch coverage, basic blocks, ..)
  64  *
  65  * Keep in mind that this is potentially a concurrent, model checked program,
  66  * i.e. there is more to coverage than what hits the eye of a static analyzer
  67  * (exceptions, data and thread CGs)
  68  */
  69 public class CoverageAnalyzer extends ListenerAdapter implements PublisherExtension {
  70
  71   static Logger log = JPF.getLogger("gov.nasa.jpf.listener.CoverageAnalyzer");
  72
  73   static class Coverage {
  74
  75     int total;
  76     int covered;
  77
  78     Coverage(int total, int covered) {
  79       this.total = total;
  80       this.covered = covered;
  81     }
  82
  83     public void add(Coverage cov) {
  84       total += cov.total;
  85       covered += cov.covered;
  86     }
  87
  88     public int percent() {
  89       if (total > 0) {
  90         return covered * 100 / total;
  91       }
  92
  93       return (Integer.MIN_VALUE);
  94     }
  95
  96     public int covered() {
  97       return covered;
  98     }
  99
 100     public int total() {
 101       return total;
 102     }
 103
 104     public boolean isPartiallyCovered() {
 105       return ((covered > 0) && (covered < total));
 106     }
 107
 108     public boolean isNotCovered() {
 109       return (covered == 0);
 110     }
 111
 112     public boolean isFullyCovered() {
 113       return (covered == total);
 114     }
 115   }
 116
 117   static class MethodCoverage {
 118
 119     MethodInfo mi;
 120
 121     // we base everything else on bytecode instruction coverage
 122     BitSet[] covered;
 123     BitSet basicBlocks; // set on demand
 124     BitSet handlers; // set on demand
 125     BitSet branches; // set on demand
 126     BitSet branchTrue;
 127     BitSet branchFalse;
 128
 129     MethodCoverage(MethodInfo mi) {
 130       this.mi = mi;
 131       log.info("add method: " + mi.getUniqueName());
 132     }
 133
 134     MethodInfo getMethodInfo() {
 135       return mi;
 136     }
 137
 138     void setExecuted(ThreadInfo ti, Instruction insn) {
 139       int idx = ti.getId();
 140
 141       if (covered == null) {
 142         covered = new BitSet[idx + 1];
 143       } else if (idx >= covered.length) {
 144         BitSet[] a = new BitSet[idx + 1];
 145         System.arraycopy(covered, 0, a, 0, covered.length);
 146         covered = a;
 147       }
 148
 149       if (covered[idx] == null) {
 150         covered[idx] = new BitSet(mi.getInstructions().length);
 151       }
 152
 153       int off = insn.getInstructionIndex();
 154       covered[idx].set(off);
 155
 156       if (showBranchCoverage && (insn instanceof IfInstruction)) {
 157         if (branchTrue == null) {
 158           branchTrue = new BitSet(mi.getInstructions().length);
 159           branchFalse = new BitSet(branchTrue.size());
 160         }
 161         if (!((IfInstruction) insn).getConditionValue()) {
 162           branchTrue.set(off);
 163         } else {
 164           branchFalse.set(off);
 165         }
 166       }
 167     }
 168
 169     void setCGed(ThreadInfo ti, Instruction insn) {
 170       ti = null;  // Remove IDE warning about unused variable.
 171       // Hmm, we have to store the bb set at this point
 172       BitSet bb = getBasicBlocks();
 173       Instruction next = insn.getNext();
 174       if (next != null) { // insn might be a sync return
 175         bb.set(next.getInstructionIndex());
 176       }
 177     }
 178
 179     BitSet getExecutedInsn() {
 180       int nTotal = mi.getInstructions().length;
 181       BitSet bUnion = new BitSet(nTotal);
 182
 183       if (covered != null) {
 184         for (BitSet b : covered) {
 185           if (b != null) {
 186             bUnion.or(b);
 187           }
 188         }
 189       }
 190
 191       return bUnion;
 192     }
 193
 194     Coverage getCoveredInsn() {
 195       int nTotal = mi.getInstructions().length;
 196
 197       if (excludeHandlers) {
 198         nTotal -= getHandlers().cardinality();
 199       }
 200
 201       if (covered != null) {
 202         BitSet bExec = getExecutedInsn();
 203         if (excludeHandlers) {
 204           bExec.andNot(getHandlers());
 205         }
 206         return new Coverage(nTotal, bExec.cardinality());
 207       } else {
 208         return new Coverage(nTotal, 0);
 209       }
 210     }
 211
 212     Coverage getCoveredLines() {
 213       BitSet executable = new BitSet();
 214       BitSet covered = new BitSet();
 215
 216       getCoveredLines(executable, covered);
 217
 218       return new Coverage(executable.cardinality(), covered.cardinality());
 219     }
 220
 221     boolean getCoveredLines(BitSet executable, BitSet covered) {
 222       Instruction inst[] = mi.getInstructions();
 223       BitSet insn;
 224       int i, line;
 225
 226       if (covered == null) {
 227         return false;
 228       }
 229
 230       insn = getExecutedInsn();
 231       if (excludeHandlers) {
 232         insn.andNot(getHandlers());
 233       }
 234
 235       if (branchTrue != null) {
 236         for (i = branchTrue.length() - 1; i >= 0; i--) {
 237           boolean cTrue = branchTrue.get(i);
 238           boolean cFalse = branchFalse.get(i);
 239
 240           if ((!cTrue || !cFalse) && (inst[i] instanceof IfInstruction)) {
 241             insn.clear(i);
 242           }
 243         }
 244       }
 245
 246       for (i = inst.length - 1; i >= 0; i--) {
 247         line = inst[i].getLineNumber();
 248
 249         if (line > 0) {
 250           executable.set(line);
 251           covered.set(line);
 252         }
 253       }
 254
 255       for (i = inst.length - 1; i >= 0; i--) {
 256         line = inst[i].getLineNumber();
 257         if ((!insn.get(i)) && (line > 0)) {         // TODO What do we do with instructions that don't have a line number.  Is this even possible?
 258           covered.clear(line);
 259         }
 260       }
 261
 262       return true;
 263     }
 264
 265     Coverage getCoveredBranches() {
 266       BitSet b = getBranches();
 267       int nTotal = b.cardinality();
 268       int nCovered = 0;
 269
 270       if (branchTrue != null) {
 271         int n = branchTrue.size();
 272
 273         for (int i = 0; i < n; i++) {
 274           boolean cTrue = branchTrue.get(i);
 275           boolean cFalse = branchFalse.get(i);
 276
 277           if (cTrue && cFalse) {
 278             nCovered++;
 279           }
 280         }
 281       }
 282
 283       return new Coverage(nTotal, nCovered);
 284     }
 285
 286     BitSet getHandlerStarts() {
 287       BitSet b = new BitSet(mi.getInstructions().length);
 288       ExceptionHandler[] handler = mi.getExceptions();
 289
 290       if (handler != null) {
 291         for (int i = 0; i < handler.length; i++) {
 292           Instruction hs = mi.getInstructionAt(handler[i].getHandler());
 293           b.set(hs.getInstructionIndex());
 294         }
 295       }
 296
 297       return b;
 298     }
 299
 300     BitSet getHandlers() {
 301       // this algorithm is a bit subtle - we walk through the code until
 302       // we hit a forward GOTO (or RETURN). If the insn following the goto is the
 303       // beginning of a handler, we mark everything up to the jump address
 304       // as a handler block
 305
 306       if (handlers == null) {
 307         BitSet hs = getHandlerStarts();
 308         Instruction[] code = mi.getInstructions();
 309         BitSet b = new BitSet(code.length);
 310
 311         if (!hs.isEmpty()) {
 312           for (int i = 0; i < code.length; i++) {
 313             Instruction insn = code[i];
 314             if (insn instanceof GOTO) {
 315               GOTO gotoInsn = (GOTO) insn;
 316               if (!gotoInsn.isBackJump() && hs.get(i + 1)) { // jump around handler
 317                 int handlerEnd = gotoInsn.getTarget().getInstructionIndex();
 318                 for (i++; i < handlerEnd; i++) {
 319                   b.set(i);
 320                 }
 321               }
 322             } else if (insn instanceof JVMReturnInstruction) { // everything else is handler
 323               for (i++; i < code.length; i++) {
 324                 b.set(i);
 325               }
 326             }
 327           }
 328         }
 329
 330         handlers = b;
 331       }
 332
 333       return handlers;
 334     }
 335
 336     // that's kind of redundant with basic blocks, but not really - here
 337     // we are interested in the logic behind branches, i.e. we want to know
 338     // what the condition values were. We are not interested in GOTOs and exceptions
 339     BitSet getBranches() {
 340       if (branches == null) {
 341         Instruction[] code = mi.getInstructions();
 342         BitSet br = new BitSet(code.length);
 343
 344         for (int i = 0; i < code.length; i++) {
 345           Instruction insn = code[i];
 346           if (insn instanceof IfInstruction) {
 347             br.set(i);
 348           }
 349         }
 350
 351         branches = br;
 352       }
 353
 354       return branches;
 355     }
 356
 357     BitSet getBasicBlocks() {
 358       if (basicBlocks == null) {
 359         Instruction[] code = mi.getInstructions();
 360         BitSet bb = new BitSet(code.length);
 361
 362         bb.set(0); // first insn is always a bb start
 363
 364         // first, look at the insn type
 365         for (int i = 0; i < code.length; i++) {
 366           Instruction insn = code[i];
 367           if (insn instanceof IfInstruction) {
 368             IfInstruction ifInsn = (IfInstruction) insn;
 369
 370             Instruction tgt = ifInsn.getTarget();
 371             bb.set(tgt.getInstructionIndex());
 372
 373             tgt = ifInsn.getNext();
 374             bb.set(tgt.getInstructionIndex());
 375           } else if (insn instanceof GOTO) {
 376             Instruction tgt = ((GOTO) insn).getTarget();
 377             bb.set(tgt.getInstructionIndex());
 378           } else if (insn instanceof JVMInvokeInstruction) {
 379             // hmm, this might be a bit too conservative, but who says we
 380             // don't jump out of a caller into a handler, or even that we
 381             // ever return from the call?
 382             Instruction tgt = insn.getNext();
 383             bb.set(tgt.getInstructionIndex());
 384           }
 385         }
 386
 387         // and now look at the handlers (every first insn is a bb start)
 388         ExceptionHandler[] handlers = mi.getExceptions();
 389         if (handlers != null) {
 390           for (int i = 0; i < handlers.length; i++) {
 391             Instruction tgt = mi.getInstructionAt(handlers[i].getHandler());
 392             bb.set(tgt.getInstructionIndex());
 393           }
 394         }
 395
 396         basicBlocks = bb;
 397
 398       /** dump
 399       System.out.println();
 400       System.out.println(mi.getFullName());
 401       for (int i=0; i<code.length; i++) {
 402       System.out.print(String.format("%1$2d %2$c ",i, bb.get(i) ? '>' : ' '));
 403       System.out.println(code[i]);
 404       }
 405        **/
 406       }
 407
 408       return basicBlocks;
 409     }
 410
 411     Coverage getCoveredBasicBlocks() {
 412       BitSet bExec = getExecutedInsn();
 413       BitSet bb = getBasicBlocks();
 414       int nCov = 0;
 415
 416       if (excludeHandlers) {
 417         BitSet handlers = getHandlers();
 418         bb.and(handlers);
 419       }
 420
 421       if (bExec != null) {
 422         BitSet bCov = new BitSet(bb.size());
 423         bCov.or(bb);
 424         bCov.and(bExec);
 425         nCov = bCov.cardinality();
 426       }
 427
 428       return new Coverage(bb.cardinality(), nCov);
 429     }
 430   }
 431
 432   static class ClassCoverage {
 433
 434     String className; // need to store since we never might get a ClassInfo
 435     ClassInfo ci;     // not initialized before the class is loaded
 436     boolean covered;
 437     HashMap<MethodInfo, MethodCoverage> methods;
 438
 439     ClassCoverage(String className) {
 440       this.className = className;
 441     }
 442
 443     void setLoaded(ClassInfo ci) {
 444       if (methods == null) {
 445         this.ci = ci;
 446         covered = true;
 447         log.info("used class: " + className);
 448
 449         methods = new HashMap<MethodInfo, MethodCoverage>();
 450         for (MethodInfo mi : ci.getDeclaredMethodInfos()) {
 451           // <2do> what about MJI methods? we should report why we don't cover them
 452           if (!mi.isNative() && !mi.isAbstract()) {
 453             MethodCoverage mc = new MethodCoverage(mi);
 454             methods.put(mi, mc);
 455           }
 456         }
 457       }
 458     }
 459
 460     boolean isInterface() {
 461       if (ci == null)           // never loaded
 462         if (!isCodeLoaded())    // can it be loaded?
 463           return false;         // will never load
 464
 465       return ci.isInterface();
 466     }
 467
 468     boolean isCodeLoaded() {
 469       if (ci != null)
 470         return true;
 471
 472       try {
 473         ci = ClassLoaderInfo.getCurrentResolvedClassInfo(className);
 474       } catch (ClassInfoException cie) {
 475         log.warning("CoverageAnalyzer problem: " + cie);   // Just log the problem but don't fail.  We still want the report to be written.
 476       }
 477
 478       return ci != null;
 479     }
 480
 481     MethodCoverage getMethodCoverage(MethodInfo mi) {
 482       if (methods == null) {
 483         setLoaded(ci);
 484       }
 485       return methods.get(mi);
 486     }
 487
 488     Coverage getCoveredMethods() {
 489       Coverage cov = new Coverage(0, 0);
 490
 491       if (methods != null) {
 492         cov.total = methods.size();
 493
 494         for (MethodCoverage mc : methods.values()) {
 495           if (mc.covered != null) {
 496             cov.covered++;
 497           }
 498         }
 499       }
 500
 501       return cov;
 502     }
 503
 504     Coverage getCoveredInsn() {
 505       Coverage cov = new Coverage(0, 0);
 506
 507       if (methods != null) {
 508         for (MethodCoverage mc : methods.values()) {
 509           Coverage c = mc.getCoveredInsn();
 510           cov.total += c.total;
 511           cov.covered += c.covered;
 512         }
 513       }
 514
 515       return cov;
 516     }
 517
 518     boolean getCoveredLines(BitSet executable, BitSet covered) {
 519       boolean result = false;
 520
 521       if (methods == null) {
 522         return false;
 523       }
 524
 525       for (MethodCoverage mc : methods.values()) {
 526         result = mc.getCoveredLines(executable, covered) || result;
 527       }
 528
 529       return result;
 530     }
 531
 532     Coverage getCoveredLines() {
 533       BitSet executable = new BitSet();
 534       BitSet covered = new BitSet();
 535
 536       getCoveredLines(executable, covered);
 537
 538       return new Coverage(executable.cardinality(), covered.cardinality());
 539     }
 540
 541     Coverage getCoveredBasicBlocks() {
 542       Coverage cov = new Coverage(0, 0);
 543
 544       if (methods != null) {
 545         for (MethodCoverage mc : methods.values()) {
 546           Coverage c = mc.getCoveredBasicBlocks();
 547           cov.total += c.total;
 548           cov.covered += c.covered;
 549         }
 550       }
 551
 552       return cov;
 553     }
 554
 555     Coverage getCoveredBranches() {
 556       Coverage cov = new Coverage(0, 0);
 557
 558       if (methods != null) {
 559         for (MethodCoverage mc : methods.values()) {
 560           Coverage c = mc.getCoveredBranches();
 561           cov.total += c.total;
 562           cov.covered += c.covered;
 563         }
 564       }
 565
 566       return cov;
 567     }
 568   }
 569
 570   StringSetMatcher includes = null; //  means all
 571   StringSetMatcher excludes = null; //  means none
 572   StringSetMatcher loaded;
 573   static boolean loadedOnly; // means we only check loaded classes that are not filtered
 574   static boolean showMethods;      // do we want to show per-method coverage?
 575   static boolean showMethodBodies;
 576   static boolean excludeHandlers;  // do we count the handlers in? (off-nominal CF)
 577   static boolean showBranchCoverage; // makes only sense with showMethods
 578   static boolean showRequirements; // report requirements coverage
 579   HashMap<String, ClassCoverage> classes = new HashMap<String, ClassCoverage>();
 580
 581   public CoverageAnalyzer(Config conf, JPF jpf) {
 582     includes = StringSetMatcher.getNonEmpty(conf.getStringArray("coverage.include"));
 583     excludes = StringSetMatcher.getNonEmpty(conf.getStringArray("coverage.exclude"));
 584
 585     showMethods = conf.getBoolean("coverage.show_methods", false);
 586     showMethodBodies = conf.getBoolean("coverage.show_bodies", false);
 587     excludeHandlers = conf.getBoolean("coverage.exclude_handlers", false);
 588     showBranchCoverage = conf.getBoolean("coverage.show_branches", true);
 589     loadedOnly = conf.getBoolean("coverage.loaded_only", true);
 590     showRequirements = conf.getBoolean("coverage.show_requirements", false);
 591
 592     if (!loadedOnly) {
 593       getCoverageCandidates(); // this might take a little while
 594     }
 595
 596     jpf.addPublisherExtension(ConsolePublisher.class, this);
 597   }
 598
 599   void getCoverageCandidates() {
 600
 601     // doesn't matter in which order we process this, since we
 602     // just store one entry per qualified class name (i.e. there won't be
 603     // multiple entries)
 604     // NOTE : this doesn't yet deal with ClassLoaders, but that's also true for BCEL
 605     ClassLoaderInfo cl = ClassLoaderInfo.getCurrentClassLoader();
 606     for (String s : cl.getClassPathElements()) {
 607       log.fine("analyzing classpath element: " + s);
 608       File f = new File(s);
 609       if (f.exists()) {
 610         if (f.isDirectory()) {
 611           traverseDir(f, null);
 612         } else if (s.endsWith(".jar")) {
 613           traverseJar(f);
 614         }
 615       }
 616     }
 617   }
 618
 619   void addClassEntry(String clsName) {
 620     ClassCoverage cc = new ClassCoverage(clsName);
 621     classes.put(clsName, cc);
 622     log.info("added class candidate: " + clsName);
 623   }
 624
 625   boolean isAnalyzedClass(String clsName) {
 626     return StringSetMatcher.isMatch(clsName, includes, excludes);
 627   }
 628
 629   void traverseDir(File dir, String pkgPrefix) {
 630     for (File f : dir.listFiles()) {
 631       if (f.isDirectory()) {
 632         String prefix = f.getName();
 633         if (pkgPrefix != null) {
 634           prefix = pkgPrefix + '.' + prefix;
 635         }
 636         traverseDir(f, prefix);
 637       } else {
 638         String fname = f.getName();
 639         if (fname.endsWith(".class")) {
 640           if (f.canRead() && (f.length() > 0)) {
 641             String clsName = fname.substring(0, fname.length() - 6);
 642             if (pkgPrefix != null) {
 643               clsName = pkgPrefix + '.' + clsName;
 644             }
 645
 646             if (isAnalyzedClass(clsName)) {
 647               addClassEntry(clsName);
 648             }
 649           } else {
 650             log.warning("cannot read class file: " + fname);
 651           }
 652         }
 653       }
 654     }
 655   }
 656
 657   void traverseJar(File jar) {
 658     try {
 659       JarFile jf = new JarFile(jar);
 660       for (Enumeration<JarEntry> entries = jf.entries(); entries.hasMoreElements();) {
 661         JarEntry e = entries.nextElement();
 662         if (!e.isDirectory()) {
 663           String eName = e.getName();
 664           if (eName.endsWith(".class")) {
 665             if (e.getSize() > 0) {
 666               String clsName = eName.substring(0, eName.length() - 6);
 667               clsName = clsName.replace('/', '.');
 668               if (isAnalyzedClass(clsName)) {
 669                 addClassEntry(clsName);
 670               }
 671             } else {
 672               log.warning("cannot read jar entry: " + eName);
 673             }
 674           }
 675         }
 676       }
 677     } catch (IOException iox) {
 678       iox.printStackTrace();
 679     }
 680   }
 681
 682
 683   HashMap<String, Integer> getGlobalRequirementsMethods() {
 684     HashMap<String, Integer> map = new HashMap<String, Integer>();
 685
 686     // <2do> this is extremely braindead, since inefficient
 687     // it would be much better to do this with Class<?> instead of ClassInfo, but
 688     // then we need a JPF- ClassLoader, since the path might be different. As a
 689     // middle ground, we could use BCEL
 690
 691     for (ClassCoverage cc : classes.values()) {
 692       ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(cc.className);
 693       for (MethodInfo mi : ci.getDeclaredMethodInfos()) {
 694         AnnotationInfo ai = getRequirementsAnnotation(mi);
 695         if (ai != null) {
 696           for (String id : ai.getValueAsStringArray()) {
 697             Integer n = map.get(id);
 698             if (n == null) {
 699               map.put(id, 1);
 700             } else {
 701               map.put(id, n + 1);
 702             }
 703           }
 704         }
 705       }
 706     }
 707
 708     return map;
 709   }
 710
 711   int computeTotalRequirementsMethods(HashMap<String, Integer> map) {
 712     int n = 0;
 713     for (Integer i : map.values()) {
 714       n += i;
 715     }
 716     return n;
 717   }
 718
 719   private void computeCoverages(String packageFilter, List<Map.Entry<String, ClassCoverage>> clsEntries, Coverage cls, Coverage mth, Coverage branch, Coverage block, Coverage line, Coverage insn) {
 720     for (Map.Entry<String, ClassCoverage> e : clsEntries) {
 721       if (e.getKey().startsWith(packageFilter)) {
 722         ClassCoverage cc = e.getValue();
 723
 724         if (cc.isInterface()) {
 725           continue; // no code
 726         }
 727
 728         cls.total++;
 729
 730         if (cc.covered) {
 731           cls.covered++;
 732         }
 733
 734         insn.add(cc.getCoveredInsn());
 735         line.add(cc.getCoveredLines());
 736         block.add(cc.getCoveredBasicBlocks());
 737         branch.add(cc.getCoveredBranches());
 738         mth.add(cc.getCoveredMethods());
 739       }
 740     }
 741   }
 742
 743
 744   /**
 745    * print uncovered source ranges
 746    */
 747
 748   //-------- the listener interface
 749   @Override
 750   public void classLoaded(VM vm, ClassInfo ci) {
 751     String clsName = ci.getName();
 752
 753     if (loadedOnly) {
 754       if (isAnalyzedClass(clsName)) {
 755         addClassEntry(clsName);
 756       }
 757     }
 758
 759     ClassCoverage cc = classes.get(clsName);
 760     if (cc != null) {
 761       cc.setLoaded(ci);
 762     }
 763   }
 764   MethodInfo lastMi = null;
 765   MethodCoverage lastMc = null;
 766
 767   MethodCoverage getMethodCoverage(Instruction insn) {
 768
 769     if (!insn.isExtendedInstruction()) {
 770       MethodInfo mi = insn.getMethodInfo();
 771       if (mi != lastMi) {
 772         lastMc = null;
 773         lastMi = mi;
 774         ClassInfo ci = mi.getClassInfo();
 775         if (ci != null) {
 776           ClassCoverage cc = classes.get(ci.getName());
 777           if (cc != null) {
 778             lastMc = cc.getMethodCoverage(mi);
 779           }
 780         }
 781       }
 782
 783       return lastMc;
 784     }
 785
 786     return null;
 787   }
 788   HashMap<String, HashSet<MethodCoverage>> requirements;
 789
 790   void updateRequirementsCoverage(String[] ids, MethodCoverage mc) {
 791     if (requirements == null) {
 792       requirements = new HashMap<String, HashSet<MethodCoverage>>();
 793     }
 794
 795     for (String id : ids) {
 796       HashSet<MethodCoverage> mcs = requirements.get(id);
 797       if (mcs == null) {
 798         mcs = new HashSet<MethodCoverage>();
 799         requirements.put(id, mcs);
 800       }
 801
 802       if (!mcs.contains(mc)) {
 803         mcs.add(mc);
 804       }
 805     }
 806   }
 807
 808   AnnotationInfo getRequirementsAnnotation(MethodInfo mi) {
 809     // <2do> should probably look for overridden method annotations
 810     return mi.getAnnotation("gov.nasa.jpf.Requirement");
 811   }
 812
 813   @Override
 814   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 815     MethodCoverage mc = getMethodCoverage(executedInsn);
 816
 817     if (mc != null) {
 818       mc.setExecuted(ti, executedInsn);
 819
 820       if (showRequirements) {
 821         if (executedInsn.getPosition() == 0) { // first insn in method, check for Requirements
 822           AnnotationInfo ai = getRequirementsAnnotation(mc.getMethodInfo());
 823           if (ai != null) {
 824             String[] ids = ai.getValueAsStringArray();
 825             updateRequirementsCoverage(ids, mc);
 826           }
 827         }
 828       }
 829     }
 830   }
 831
 832   @Override
 833   public void choiceGeneratorSet(VM vm, ChoiceGenerator<?> newCG) {
 834     /*** should be an option
 835     Instruction insn = vm.getLastInstruction();
 836     MethodCoverage mc = getMethodCoverage(vm);
 837     mc.setCGed(vm.getLastThreadInfo(),insn);
 838      ***/
 839   }
 840
 841   //-------- the publisher interface
 842   private Publisher publisher;
 843   private ArrayList<Map.Entry<String, ClassCoverage>> clsEntries;
 844
 845
 846   abstract class Publish {
 847     PrintWriter pw;
 848
 849     Publish () {}
 850     Publish (Publisher p){
 851       pw = p.getOut();
 852     }
 853
 854     abstract void publish();
 855     abstract void printClassCoverages();
 856     abstract void printRequirementsCoverage();
 857   }
 858
 859   class PublishConsole extends Publish {
 860     PublishConsole (ConsolePublisher p){
 861       super(p);
 862     }
 863
 864     @Override
 865         void publish() {
 866       publisher.publishTopicStart("coverage statistics");
 867
 868       printClassCoverages();
 869
 870       if (showRequirements) {
 871         printRequirementsCoverage();
 872       }
 873
 874     }
 875
 876     void printCoverage (Coverage cov){
 877       int nTotal = cov.total();
 878       int nCovered = cov.covered();
 879
 880       String s;
 881       if (nTotal <= 0) {
 882         s = " -  ";
 883       } else {
 884         s = String.format("%.2f (%d/%d)", ((double) nCovered / nTotal), nCovered, nTotal);
 885       }
 886       pw.print(String.format("%1$-18s", s));
 887     }
 888
 889
 890     @Override
 891         void printClassCoverages() {
 892       String space = "  ";
 893       Coverage clsCoverage = new Coverage(0, 0);
 894       Coverage mthCoverage = new Coverage(0, 0);
 895       Coverage bbCoverage = new Coverage(0, 0);
 896       Coverage lineCoverage = new Coverage(0, 0);
 897       Coverage insnCoverage = new Coverage(0, 0);
 898       Coverage branchCoverage = new Coverage(0, 0);
 899
 900       computeCoverages("", clsEntries, clsCoverage, mthCoverage, branchCoverage, bbCoverage, lineCoverage, insnCoverage);
 901
 902       pw.println();
 903       pw.println("-------------------------------------------- class coverage ------------------------------------------------");
 904       pw.println("bytecode            line                basic-block         branch              methods             location");
 905       pw.println("------------------------------------------------------------------------------------------------------------");
 906
 907       // Write Body
 908       for (Map.Entry<String, ClassCoverage> e : clsEntries) {
 909         ClassCoverage cc = e.getValue();
 910
 911         printCoverage(cc.getCoveredInsn());
 912         pw.print(space);
 913
 914         printCoverage(cc.getCoveredLines());
 915         pw.print(space);
 916
 917         printCoverage(cc.getCoveredBasicBlocks());
 918         pw.print(space);
 919
 920         printCoverage(cc.getCoveredBranches());
 921         pw.print(space);
 922
 923         printCoverage(cc.getCoveredMethods());
 924         pw.print(space);
 925
 926         pw.println(e.getKey());
 927
 928         if (showMethods) {
 929           printMethodCoverages(cc);
 930         }
 931       }
 932
 933       pw.println();
 934       pw.println("------------------------------------------------------------------------------------------------------------");
 935
 936       printCoverage(insnCoverage);
 937       pw.print(space);
 938       printCoverage(lineCoverage);
 939       pw.print(space);
 940       printCoverage(bbCoverage);
 941       pw.print(space);
 942       printCoverage(branchCoverage);
 943       pw.print(space);
 944       printCoverage(mthCoverage);
 945       pw.print(space);
 946       printCoverage(clsCoverage);
 947       pw.println(" total");
 948
 949     }
 950
 951     @Override
 952         void printRequirementsCoverage() {
 953       HashMap<String, Integer> reqMethods = getGlobalRequirementsMethods();
 954
 955       String space = "  ";
 956       Coverage bbAll = new Coverage(0, 0);
 957       Coverage insnAll = new Coverage(0, 0);
 958       Coverage branchAll = new Coverage(0, 0);
 959       Coverage mthAll = new Coverage(0, 0);
 960       Coverage reqAll = new Coverage(0, 0);
 961
 962       reqAll.total = reqMethods.size();
 963       mthAll.total = computeTotalRequirementsMethods(reqMethods);
 964
 965       pw.println();
 966       pw.println();
 967       pw.println("--------------------------------- requirements coverage -----------------------------------");
 968       pw.println("bytecode            basic-block         branch              methods             requirement");
 969       pw.println("-------------------------------------------------------------------------------------------");
 970
 971       for (String id : Misc.getSortedKeyStrings(reqMethods)) {
 972
 973         Coverage bbCoverage = new Coverage(0, 0);
 974         Coverage insnCoverage = new Coverage(0, 0);
 975         Coverage branchCoverage = new Coverage(0, 0);
 976         Coverage reqMth = new Coverage(reqMethods.get(id), 0);
 977
 978         if (requirements != null && requirements.containsKey(id)) {
 979           reqAll.covered++;
 980           for (MethodCoverage mc : requirements.get(id)) {
 981             insnCoverage.add(mc.getCoveredInsn());
 982             bbCoverage.add(mc.getCoveredBasicBlocks());
 983             branchCoverage.add(mc.getCoveredBranches());
 984
 985             mthAll.covered++;
 986             reqMth.covered++;
 987           }
 988
 989
 990           printCoverage(insnCoverage);
 991           pw.print(space);
 992           printCoverage(bbCoverage);
 993           pw.print(space);
 994           printCoverage(branchCoverage);
 995           pw.print(space);
 996           printCoverage(reqMth);
 997           pw.print("\"" + id + "\"");
 998
 999
1000           pw.println();
1001
1002           if (showMethods) {
1003             for (MethodCoverage mc : requirements.get(id)) {
1004
1005               pw.print(space);
1006               printCoverage(mc.getCoveredInsn());
1007               pw.print(space);
1008               printCoverage(mc.getCoveredBasicBlocks());
1009               pw.print(space);
1010               printCoverage(mc.getCoveredBranches());
1011               pw.print(space);
1012
1013               pw.print(mc.getMethodInfo().getFullName());
1014               pw.println();
1015             }
1016           }
1017         } else { // requirement not covered
1018           pw.print(" -                   -                   -                  ");
1019
1020           printCoverage(reqMth);
1021           pw.print("\"" + id + "\"");
1022           pw.println();
1023         }
1024
1025         insnAll.add(insnCoverage);
1026         bbAll.add(bbCoverage);
1027         branchAll.add(branchCoverage);
1028       }
1029
1030       pw.println();
1031       pw.println("------------------------------------------------------------------------------------------");
1032
1033       printCoverage(insnAll);
1034       pw.print(space);
1035       printCoverage(bbAll);
1036       pw.print(space);
1037       printCoverage(branchAll);
1038       pw.print(space);
1039       printCoverage(mthAll);
1040       pw.print(space);
1041       printCoverage(reqAll);
1042       pw.print(" total");
1043
1044       pw.println();
1045     }
1046
1047     void printMethodCoverages(ClassCoverage cc) {
1048       String space = "  ";
1049       boolean result = true;
1050
1051       if (cc.methods == null) {
1052         return;
1053       }
1054
1055       ArrayList<Map.Entry<MethodInfo, MethodCoverage>> mthEntries =
1056               Misc.createSortedEntryList(cc.methods, new Comparator<Map.Entry<MethodInfo, MethodCoverage>>() {
1057
1058         @Override
1059                 public int compare(Map.Entry<MethodInfo, MethodCoverage> o1,
1060                 Map.Entry<MethodInfo, MethodCoverage> o2) {
1061           int a = o2.getValue().getCoveredInsn().percent();
1062           int b = o1.getValue().getCoveredInsn().percent();
1063
1064           if (a == b) {
1065             return o2.getKey().getUniqueName().compareTo(o1.getKey().getUniqueName());
1066           } else {
1067             return a - b;
1068           }
1069         }
1070       });
1071
1072       Coverage emptyCoverage = new Coverage(0, 0);
1073
1074       for (Map.Entry<MethodInfo, MethodCoverage> e : mthEntries) {
1075         MethodCoverage mc = e.getValue();
1076         MethodInfo mi = mc.getMethodInfo();
1077         Coverage insnCoverage = mc.getCoveredInsn();
1078         Coverage lineCoverage = mc.getCoveredLines();
1079         Coverage branchCoverage = mc.getCoveredBranches();
1080
1081         result = result && insnCoverage.isFullyCovered();
1082
1083
1084         pw.print(space);
1085         printCoverage(insnCoverage);
1086
1087         pw.print(space);
1088         printCoverage(lineCoverage);
1089
1090         pw.print(space);
1091         printCoverage(mc.getCoveredBasicBlocks());
1092
1093         pw.print(space);
1094         printCoverage(branchCoverage);
1095
1096         pw.print(space);
1097         printCoverage(emptyCoverage);
1098
1099         pw.print(space);
1100         pw.print(mi.getLongName());
1101         pw.println();
1102
1103         if (showMethodBodies &&
1104                 (!insnCoverage.isFullyCovered() || !branchCoverage.isFullyCovered())) {
1105           printBodyCoverage(mc);
1106         }
1107       }
1108     }
1109
1110     void printBodyCoverage(MethodCoverage mc) {
1111       MethodInfo mi = mc.getMethodInfo();
1112       Instruction[] code = mi.getInstructions();
1113       BitSet cov = mc.getExecutedInsn();
1114       int i, start = -1;
1115
1116       BitSet handlers = mc.getHandlers();
1117
1118       if (excludeHandlers) {
1119         cov.andNot(handlers);
1120       }
1121
1122       for (i = 0; i < code.length; i++) {
1123         if (!cov.get(i)) { // not covered
1124           if (start == -1) {
1125             start = i;
1126           }
1127         } else { // covered
1128           if (start != -1) {
1129             printSourceRange(code, handlers, start, i - 1, "");
1130             start = -1;
1131           }
1132         }
1133       }
1134       if (start != -1) {
1135         printSourceRange(code, handlers, start, i - 1, "");
1136       }
1137
1138       // now print the missing branches
1139       BitSet branches = mc.getBranches();
1140       lastStart = -1; // reset in case condition and branch are in same line
1141       for (i = 0; i < code.length; i++) {
1142         if (branches.get(i)) {
1143           String prefix = "";
1144           BitSet bTrue = mc.branchTrue;
1145           BitSet bFalse = mc.branchFalse;
1146           if (bTrue != null) { // means we have condition bit sets
1147             boolean cTrue = bTrue.get(i);
1148             boolean cFalse = bFalse.get(i);
1149             if (cTrue) {
1150               prefix = cFalse ? "" : "F "; // covered or false missing
1151             } else {
1152               prefix = cFalse ? "T " : "N "; // true or both missing
1153             }
1154           } else {
1155             prefix = "N ";                   // not covered at all
1156           }
1157
1158           if (prefix != null) {
1159             printSourceRange(code, handlers, i, i, prefix);
1160           }
1161         }
1162       }
1163     }
1164
1165     // there might be several ranges within the same source line
1166     int lastStart = -1;
1167
1168     void printSourceRange(Instruction[] code, BitSet handlers,
1169             int start, int end, String prefix) {
1170
1171       int line = code[start].getLineNumber();
1172
1173       if (lastStart == line) {
1174         return;
1175       }
1176
1177       lastStart = line;
1178
1179       printLocation(prefix, "at", code[start].getSourceLocation(), handlers.get(start) ? "x" : "");
1180
1181       if (line != code[end].getLineNumber()) {
1182         printLocation(prefix, "..", code[end].getSourceLocation(), handlers.get(end) ? "x" : "");
1183       }
1184     // we need the "(..)" wrapper so that Eclipse parses this
1185     // as a source location when displaying the report in a console
1186     }
1187
1188     private void printLocation(String prefix, String at, String location, String suffix) {
1189
1190       printBlanks(pw, 84);
1191       pw.print(prefix);
1192       pw.print(at);
1193       pw.print(' ');
1194       pw.print(location);
1195       pw.print(' ');
1196       pw.println(suffix);
1197     }
1198
1199     void printBlanks(PrintWriter pw, int n) {
1200       for (int i = 0; i < n; i++) {
1201         pw.print(' ');
1202       }
1203     }
1204
1205   }
1206
1207
1208   @Override
1209   public void publishFinished(Publisher publisher) {
1210
1211     if (clsEntries == null) {
1212       clsEntries = Misc.createSortedEntryList(classes, new Comparator<Map.Entry<String, ClassCoverage>>() {
1213
1214         @Override
1215                 public int compare(Map.Entry<String, ClassCoverage> o1,
1216                 Map.Entry<String, ClassCoverage> o2) {
1217           return o2.getKey().compareTo(o1.getKey());
1218         }
1219       });
1220     }
1221
1222     this.publisher = publisher;
1223
1224     if (publisher instanceof ConsolePublisher) {
1225       new PublishConsole((ConsolePublisher) publisher).publish();
1226     }
1227   }
1228 }