src/main/gov/nasa/jpf/report/Reporter.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.report;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.Error;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.JPFListener;
  24 import gov.nasa.jpf.search.Search;
  25 import gov.nasa.jpf.search.SearchListenerAdapter;
  26 import gov.nasa.jpf.vm.VM;
  27 import gov.nasa.jpf.vm.Path;
  28
  29 import java.io.IOException;
  30 import java.io.InputStream;
  31 import java.net.InetAddress;
  32 import java.util.ArrayList;
  33 import java.util.Date;
  34 import java.util.List;
  35 import java.util.Properties;
  36 import java.util.logging.Logger;
  37
  38 /**
  39  * this is our default report generator, which is heavily configurable
  40  * via our standard properties. Note this gets instantiated and
  41  * registered automatically via JPF.addListeners(), so you don't
  42  * have to add it explicitly
  43  */
  44
  45 public class Reporter extends SearchListenerAdapter {
  46
  47   public static Logger log = JPF.getLogger("report");
  48
  49   protected Config conf;
  50   protected JPF jpf;
  51   protected Search search;
  52   protected VM vm;
  53
  54   protected Date started, finished;
  55   protected Statistics stat; // the object that collects statistics
  56   protected List<Publisher> publishers = new ArrayList<Publisher>();
  57
  58   protected Thread probeTimer;
  59
  60   public Reporter (Config conf, JPF jpf) {
  61     this.conf = conf;
  62     this.jpf = jpf;
  63     search = jpf.getSearch();
  64     vm = jpf.getVM();
  65     int probeInterval = conf.getInt("report.probe_interval");
  66     boolean reportStats = conf.getBoolean("report.statistics", false) || (probeInterval > 0);
  67
  68     started = new Date();
  69
  70     addConfiguredPublishers(conf);
  71
  72     for (Publisher publisher : publishers) {
  73       if (reportStats || publisher.hasToReportStatistics()) {
  74         reportStats = true;
  75       }
  76
  77       if (publisher instanceof JPFListener) {
  78         jpf.addListener((JPFListener)publisher);
  79       }
  80     }
  81
  82     if (reportStats){
  83       getRegisteredStatistics();
  84     }
  85
  86     if (probeInterval > 0){
  87       probeTimer = createProbeIntervalTimer(probeInterval);
  88     }
  89   }
  90
  91   protected Thread createProbeIntervalTimer (final int probeInterval){
  92     Thread timer = new Thread( new Runnable(){
  93         @Override
  94                 public void run(){
  95           log.info("probe timer running");
  96           while (!search.isDone()){
  97             try {
  98               Thread.sleep( probeInterval * 1000);
  99               search.probeSearch(); // this is only a request
 100             } catch (InterruptedException ix) {
 101               // nothing
 102             }
 103           }
 104           log.info("probe timer terminating");
 105         }
 106      }, "probe-timer");
 107     timer.setDaemon(true);
 108
 109     // we don't start before the Search is started
 110
 111     return timer;
 112   }
 113
 114   /**
 115    * called after the JPF run is finished. Shouldn't be public, but is called by JPF
 116    */
 117   public void cleanUp(){
 118     // nothing yet
 119   }
 120
 121   public Statistics getRegisteredStatistics(){
 122
 123     if (stat == null){ // none yet, initialize
 124       // first, check if somebody registered one explicitly
 125       stat = vm.getNextListenerOfType(Statistics.class, null);
 126       if (stat == null){
 127         stat = conf.getInstance("report.statistics.class@stat", Statistics.class);
 128         if (stat == null) {
 129           stat = new Statistics();
 130         }
 131         jpf.addListener(stat);
 132       }
 133     }
 134
 135     return stat;
 136   }
 137
 138
 139   void addConfiguredPublishers (Config conf) {
 140     String[] def = { "console" };
 141
 142     Class<?>[] argTypes = { Config.class, Reporter.class };
 143     Object[] args = { conf, this };
 144
 145     for (String id : conf.getStringArray("report.publisher", def)){
 146       Publisher p = conf.getInstance("report." + id + ".class",
 147                                      Publisher.class, argTypes, args);
 148       if (p != null){
 149         publishers.add(p);
 150       } else {
 151         log.warning("could not instantiate publisher class: " + id);
 152       }
 153     }
 154   }
 155
 156   public void addPublisher( Publisher newPublisher){
 157     publishers.add(newPublisher);
 158   }
 159
 160   public List<Publisher> getPublishers() {
 161     return publishers;
 162   }
 163
 164   public boolean hasToReportTrace() {
 165     for (Publisher p : publishers) {
 166       if (p.hasTopic("trace")) {
 167         return true;
 168       }
 169     }
 170
 171     return false;
 172   }
 173
 174   public boolean hasToReportOutput() {
 175     for (Publisher p : publishers) {
 176       if (p.hasTopic("output")) {
 177         return true;
 178       }
 179     }
 180
 181     return false;
 182   }
 183
 184
 185   public <T extends Publisher> boolean addPublisherExtension (Class<T> publisherCls, PublisherExtension e) {
 186     boolean added = false;
 187     for (Publisher p : publishers) {
 188       Class<?> pCls = p.getClass();
 189       if (publisherCls.isAssignableFrom(pCls)) {
 190         p.addExtension(e);
 191         added = true;
 192       }
 193     }
 194
 195     return added;
 196   }
 197
 198   public <T extends Publisher> void setPublisherItems (Class<T> publisherCls,
 199                                                         int category, String[] topics){
 200     for (Publisher p : publishers) {
 201       if (publisherCls.isInstance(p)) {
 202         p.setItems(category,topics);
 203         return;
 204       }
 205     }
 206   }
 207
 208   boolean contains (String key, String[] list) {
 209     for (String s : list) {
 210       if (s.equalsIgnoreCase(key)){
 211         return true;
 212       }
 213     }
 214     return false;
 215   }
 216
 217
 218   //--- the publishing phases
 219
 220   protected void publishStart() {
 221     for (Publisher publisher : publishers) {
 222       publisher.openChannel();
 223       publisher.publishProlog();
 224       publisher.publishStart();
 225     }
 226   }
 227
 228   protected void publishTransition() {
 229     for (Publisher publisher : publishers) {
 230       publisher.publishTransition();
 231     }
 232   }
 233
 234   protected void publishPropertyViolation() {
 235     for (Publisher publisher : publishers) {
 236       publisher.publishPropertyViolation();
 237     }
 238   }
 239
 240   protected void publishConstraintHit() {
 241     for (Publisher publisher : publishers) {
 242       publisher.publishConstraintHit();
 243     }
 244   }
 245
 246   protected void publishFinished() {
 247     for (Publisher publisher : publishers) {
 248       publisher.publishFinished();
 249       publisher.publishEpilog();
 250       publisher.closeChannel();
 251     }
 252   }
 253
 254   protected void publishProbe(){
 255     for (Publisher publisher : publishers) {
 256       publisher.publishProbe();
 257     }
 258   }
 259
 260   //--- the listener interface that drives report generation
 261
 262   @Override
 263   public void searchStarted (Search search){
 264     publishStart();
 265
 266     if (probeTimer != null){
 267       probeTimer.start();
 268     }
 269   }
 270
 271   @Override
 272   public void stateAdvanced (Search search) {
 273     publishTransition();
 274   }
 275
 276   @Override
 277   public void searchConstraintHit(Search search) {
 278     publishConstraintHit();
 279   }
 280
 281   @Override
 282   public void searchProbed (Search search){
 283     publishProbe();
 284   }
 285
 286   @Override
 287   public void propertyViolated (Search search) {
 288     publishPropertyViolation();
 289   }
 290
 291   @Override
 292   public void searchFinished (Search search){
 293     finished = new Date();
 294
 295     publishFinished();
 296
 297     if (probeTimer != null){
 298       // we could interrupt, but it's a daemon anyways
 299       probeTimer = null;
 300     }
 301   }
 302
 303
 304   //--- various getters
 305
 306   public Date getStartDate() {
 307     return started;
 308   }
 309
 310   public Date getFinishedDate () {
 311     return finished;
 312   }
 313
 314   public VM getVM() {
 315     return vm;
 316   }
 317
 318   public Search getSearch() {
 319     return search;
 320   }
 321
 322   public List<Error> getErrors () {
 323     return search.getErrors();
 324   }
 325
 326   public Error getCurrentError () {
 327     return search.getCurrentError();
 328   }
 329
 330   public String getLastSearchConstraint () {
 331     return search.getLastSearchConstraint();
 332   }
 333
 334   public String getCurrentErrorId () {
 335     Error e = getCurrentError();
 336     if (e != null) {
 337       return "#" + e.getId();
 338     } else {
 339       return "";
 340     }
 341   }
 342
 343   public int getNumberOfErrors() {
 344     return search.getErrors().size();
 345   }
 346
 347   public Statistics getStatistics() {
 348     return stat;
 349   }
 350
 351   public Statistics getStatisticsSnapshot () {
 352     return stat.clone();
 353   }
 354
 355   /**
 356    * in ms
 357    */
 358   public long getElapsedTime () {
 359     Date d = (finished != null) ? finished : new Date();
 360     long t = d.getTime() - started.getTime();
 361     return t;
 362   }
 363
 364   public Path getPath (){
 365     return vm.getClonedPath();
 366   }
 367
 368   public String getJPFBanner () {
 369     StringBuilder sb = new StringBuilder();
 370
 371     sb.append("JavaPathfinder core system v");
 372     sb.append(JPF.VERSION);
 373
 374     String rev = getRevision();
 375     if (rev != null){
 376       sb.append(" (rev ");
 377       sb.append(rev);
 378       sb.append(')');
 379     }
 380
 381     sb.append(" - (C) 2005-2014 United States Government. All rights reserved.");
 382
 383     if (conf.getBoolean("report.show_repository", false)) {
 384       String repInfo =  getRepositoryInfo();
 385       if (repInfo != null) {
 386         sb.append( repInfo);
 387       }
 388     }
 389
 390     return sb.toString();
 391   }
 392
 393
 394   protected String getRevision() {
 395     try {
 396       InputStream is = JPF.class.getResourceAsStream(".version");
 397       if (is != null){
 398         int len = is.available();
 399         byte[] data = new byte[len];
 400         is.read(data);
 401         is.close();
 402         return new String(data).trim();
 403
 404       } else {
 405         return null;
 406       }
 407
 408     } catch (Throwable t){
 409       return null;
 410     }
 411   }
 412
 413   protected String getRepositoryInfo() {
 414     try {
 415       InputStream is = JPF.class.getResourceAsStream("build.properties");
 416       if (is != null){
 417         Properties revInfo = new Properties();
 418         revInfo.load(is);
 419
 420         StringBuffer sb = new StringBuffer();
 421         String date = revInfo.getProperty("date");
 422         String author = revInfo.getProperty("author");
 423         String rev = revInfo.getProperty("rev");
 424         String machine = revInfo.getProperty("hostname");
 425         String loc = revInfo.getProperty("location");
 426         String upstream = revInfo.getProperty("upstream");
 427
 428         return String.format("%s %s %s %s %s", date,author,rev,machine,loc);
 429       }
 430     } catch (IOException iox) {
 431       return null;
 432     }
 433
 434     return null;
 435   }
 436
 437
 438   public String getHostName () {
 439     try {
 440       InetAddress in = InetAddress.getLocalHost();
 441       String hostName = in.getHostName();
 442       return hostName;
 443     } catch (Throwable t) {
 444       return "localhost";
 445     }
 446   }
 447
 448   public String getUser() {
 449     return System.getProperty("user.name");
 450   }
 451
 452   public String getSuT() {
 453     return vm.getSUTDescription();
 454   }
 455
 456   public String getJava (){
 457     String vendor = System.getProperty("java.vendor");
 458     String version = System.getProperty("java.version");
 459     return vendor + "/" + version;
 460   }
 461
 462   public String getArch () {
 463     String arch = System.getProperty("os.arch");
 464     Runtime rt = Runtime.getRuntime();
 465     String type = arch + "/" + rt.availableProcessors();
 466
 467     return type;
 468   }
 469
 470   public String getOS () {
 471     String name = System.getProperty("os.name");
 472     String version = System.getProperty("os.version");
 473     return name + "/" + version;
 474   }
 475
 476 }