Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/listener/CoverageAnalyzer.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:61d41facf527
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 }