src/main/gov/nasa/jpf/tool/RunJPF.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.tool;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPFShell;
  22 import gov.nasa.jpf.util.JPFSiteUtils;
  23
  24 import java.io.File;
  25 import java.io.IOException;
  26 import java.io.InputStream;
  27 import java.lang.reflect.InvocationTargetException;
  28 import java.util.Map;
  29 import java.util.Properties;
  30
  31 /**
  32  * This class is a wrapper for loading JPF or a JPFShell through a classloader
  33  * that got initialized from a Config object (i.e. 'native_classpath').
  34  *
  35  * This is the main-class entry in the executable RunJPF.jar, which does not
  36  * require any JPF specific classpath settings, provided the site.properties
  37  * is configured correctly
  38  *
  39  * NOTE this class is not allowed to use any types that would require
  40  * loading JPF classes during class resolution - this would result in
  41  * NoClassDefFoundErrors if the respective class is not in RunJPF.jar
  42  */
  43 public class RunJPF extends Run {
  44
  45   public static final int HELP         = 0x1;
  46   public static final int SHOW         = 0x2;
  47   public static final int LOG          = 0x4;
  48   public static final int BUILD_INFO   = 0x8;
  49   public static final int ADD_PROJECT  = 0x10;
  50   public static final int VERSION      = 0x20;
  51   public static final int DELAY_START  = 0x40;
  52   public static final int DELAY_EXIT   = 0x80;
  53
  54   static final String JPF_CLASSNAME = "gov.nasa.jpf.JPF";
  55
  56   static void delay (String msg) {
  57     System.out.println(msg);
  58     try {
  59       System.in.read();
  60     } catch (IOException iox) {
  61       // we don't care
  62     }
  63   }
  64
  65   public static void main (String[] args) {
  66     try {
  67       int options = getOptions(args);
  68
  69       if (args.length == 0 || isOptionEnabled(HELP, options)) {
  70         showUsage();
  71         return;
  72       }
  73
  74       if (isOptionEnabled(ADD_PROJECT, options)){
  75         addProject(args);
  76         return;
  77       }
  78
  79       if (isOptionEnabled(DELAY_START, options)) {
  80         delay("press any key to start");
  81       }
  82
  83       if (isOptionEnabled(LOG, options)) {
  84         Config.enableLogging(true);
  85       }
  86
  87       Config conf = new Config(args);
  88
  89       if (isOptionEnabled(SHOW, options)) {
  90         conf.printEntries();
  91       }
  92
  93       ClassLoader cl = conf.initClassLoader(RunJPF.class.getClassLoader());
  94
  95       if (isOptionEnabled(VERSION, options)) {
  96         showVersion(cl);
  97       }
  98
  99       if (isOptionEnabled(BUILD_INFO, options)) {
 100         showBuild(cl);
 101       }
 102
 103       // using JPFShell is Ok since it is just a simple non-derived interface
 104       // note this uses a <init>(Config) ctor in the shell class if there is one, i.e. there is no need for a separate
 105       // start(Config,..) or re-loading the config itself
 106       JPFShell shell = conf.getInstance("shell", JPFShell.class);
 107       if (shell != null) {
 108         shell.start( removeConfigArgs(args)); // responsible for exception handling itself
 109
 110       } else {
 111         // we have to load JPF explicitly through the URLClassLoader, and
 112         // call its start() via reflection - interfaces would only work if
 113         // we instantiate a JPF object here, which would force us to duplicate all
 114         // the logging and event handling that preceedes JPF instantiation
 115         Class<?> jpfCls = cl.loadClass(JPF_CLASSNAME);
 116         if (!call( jpfCls, "start", new Object[] {conf,args})){
 117           error("cannot find 'public static start(Config,String[])' in " + JPF_CLASSNAME);
 118         }
 119       }
 120
 121       if (isOptionEnabled(DELAY_EXIT, options)) {
 122         delay("press any key to exit");
 123       }
 124
 125
 126     } catch (NoClassDefFoundError ncfx){
 127       ncfx.printStackTrace();
 128     } catch (ClassNotFoundException cnfx){
 129       error("cannot find " + JPF_CLASSNAME);
 130     } catch (InvocationTargetException ix){
 131       // should already be handled by JPF
 132       ix.getCause().printStackTrace();
 133     }
 134
 135   }
 136
 137   public static int getOptions (String[] args){
 138     int mask = 0;
 139
 140     if (args != null){
 141
 142       for (int i = 0; i < args.length; i++) {
 143         String a = args[i];
 144         if ("-help".equals(a)){
 145           args[i] = null;
 146           mask |= HELP;
 147
 148         } else if ("-show".equals(a)) {
 149           args[i] = null;
 150           mask |= SHOW;
 151
 152         } else if ("-log".equals(a)){
 153           args[i] = null;
 154           mask |= LOG;
 155
 156         } else if ("-buildinfo".equals(a)){
 157           args[i] = null;
 158           mask |= BUILD_INFO;
 159
 160         } else if ("-addproject".equals(a)){
 161           args[i] = null;
 162           mask |= ADD_PROJECT;
 163
 164         } else if ("-delay-start".equals(a)) {
 165           args[i] = null;
 166           mask |= DELAY_START;
 167
 168         } else if ("-delay-exit".equals(a)) {
 169           args[i] = null;
 170           mask |= DELAY_EXIT;
 171
 172         } else if ("-version".equals(a)){
 173           args[i] = null;
 174           mask |= VERSION;
 175         }
 176       }
 177     }
 178
 179     return mask;
 180   }
 181
 182   public static boolean isOptionEnabled (int option, int mask){
 183     return ((mask & option) != 0);
 184   }
 185
 186   public static void showUsage() {
 187     System.out.println("Usage: \"java [<vm-option>..] -jar ...RunJPF.jar [<jpf-option>..] [<app> [<app-arg>..]]");
 188     System.out.println("  <jpf-option> : -help : print usage information and exit");
 189     System.out.println("               | -version : print JPF version information");
 190     System.out.println("               | -buildinfo : print build and runtime information");
 191     System.out.println("               | -addproject [init] [<pathname>] : add project to site properties and exit");
 192     System.out.println("               | -log : print configuration initialization steps");
 193     System.out.println("               | -show : print configuration dictionary contents");
 194     System.out.println("               | +<key>=<value>  : add or override key/value pair to config dictionary");
 195     System.out.println("  <app>        : *.jpf application properties file pathname | fully qualified application class name");
 196     System.out.println("  <app-arg>    : arguments passed into main() method of application class");
 197   }
 198
 199   public static void addProject(String[] args){
 200     boolean init = false;
 201     int i=0;
 202     String sitePathName = null;
 203
 204     // check if the first non-null arg is 'init', which means this project
 205     // should be added to the 'extensions' list
 206     for(; i<args.length; i++){
 207       if (args[i] != null){
 208         if ("init".equals(args[i])){
 209           init = true;
 210           continue;
 211         } else {
 212           sitePathName = args[i];
 213         }
 214         break;
 215       }
 216     }
 217
 218     File siteProps = (sitePathName == null) ? JPFSiteUtils.getStandardSiteProperties() : new File(sitePathName);
 219     if (siteProps == null) {
 220       siteProps = new File(JPFSiteUtils.getGlobalSitePropertiesPath());
 221     }
 222
 223     File curDir = new File( System.getProperty("user.dir"));
 224     String pid = JPFSiteUtils.getCurrentProjectId();
 225     if (pid == null){
 226       error("current dir not a valid JPF project: " + curDir);
 227     }
 228
 229     if ("jpf-core".equals(pid)){ // jpf-core always needs to be in the extensions list
 230       init = true;
 231     }
 232
 233     if (JPFSiteUtils.addProject( siteProps, pid, curDir, init)){
 234       System.out.println("added project '" + pid + "' to site properties at: " + siteProps);
 235     } else {
 236       error("failed to add project: '" + pid + "' to site properties at: " + siteProps);
 237     }
 238   }
 239
 240   public static void showVersion (ClassLoader cl){
 241     try {
 242       InputStream is = cl.getResourceAsStream("gov/nasa/jpf/.version");
 243       if (is != null){
 244         System.out.print("JPF version: ");
 245
 246         int len = is.available();
 247         byte[] data = new byte[len];
 248         is.read(data);
 249         is.close();
 250         String version = new String(data);
 251         System.out.println(version);
 252
 253       } else {
 254         System.out.println("no JPF version information available");
 255       }
 256
 257
 258     } catch (Throwable t){
 259       System.err.println("error reading version information: " + t.getMessage());
 260     }
 261   }
 262
 263   // print out the build.properties settings
 264   public static void showBuild(ClassLoader cl) {
 265     try {
 266       InputStream is = cl.getResourceAsStream("gov/nasa/jpf/build.properties");
 267       if (is != null){
 268         System.out.println("JPF build information:");
 269
 270         Properties buildProperties = new Properties();
 271         buildProperties.load(is);
 272
 273         for (Map.Entry<Object, Object> e : buildProperties.entrySet()) {
 274           System.out.print('\t');
 275           System.out.print(e.getKey());
 276           System.out.print(" = ");
 277           System.out.println(e.getValue());
 278         }
 279
 280         is.close();
 281
 282       } else {
 283         System.out.println("no JPF build information available");
 284       }
 285
 286     } catch (Throwable t){
 287       System.err.println("error reading build information: " + t.getMessage());
 288     }
 289   }
 290
 291 }