src/main/gov/nasa/jpf/util/test/TestMultiProcessJPF.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
  19 package gov.nasa.jpf.util.test;
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.Property;
  23 import gov.nasa.jpf.util.TypeRef;
  24 import gov.nasa.jpf.vm.NotDeadlockedProperty;
  25
  26 /**
  27  * @author Nastaran Shafiei <nastaran.shafiei@gmail.com>
  28  *
  29  * This is a root class for testing multi-processes code. This forces
  30  * JPF to use MultiProcessVM and DistributedSchedulerFactory
  31  */
  32 public abstract class TestMultiProcessJPF extends TestJPF {
  33   int numOfPrc;
  34
  35   @Override
  36   protected void setTestTargetKeys(Config conf, StackTraceElement testMethod) {
  37     conf.put("target.entry", "runTestMethod([Ljava/lang/String;)V");
  38     conf.put("target.replicate", Integer.toString(numOfPrc));
  39     conf.put("target", testMethod.getClassName());
  40     conf.put("target.test_method", testMethod.getMethodName());
  41     conf.put("vm.class", "gov.nasa.jpf.vm.MultiProcessVM");
  42     conf.put("vm.scheduler_factory.class", "gov.nasa.jpf.vm.DistributedSchedulerFactory");
  43   }
  44
  45   protected native int getProcessId();
  46
  47   protected boolean mpVerifyAssertionErrorDetails (int prcNum, String details, String... args){
  48     if (runDirectly) {
  49       return true;
  50     } else {
  51       numOfPrc = prcNum;
  52       unhandledException( getCaller(), "java.lang.AssertionError", details, args);
  53       return false;
  54     }
  55   }
  56
  57   protected boolean mpVerifyAssertionError (int prcNum, String... args){
  58     if (runDirectly) {
  59       return true;
  60     } else {
  61       numOfPrc = prcNum;
  62       unhandledException( getCaller(), "java.lang.AssertionError", null, args);
  63       return false;
  64     }
  65   }
  66
  67   protected boolean mpVerifyNoPropertyViolation (int prcNum, String...args){
  68     if (runDirectly) {
  69       return true;
  70     } else {
  71       numOfPrc = prcNum;
  72       noPropertyViolation(getCaller(), args);
  73       return false;
  74     }
  75   }
  76
  77   protected boolean mpVerifyUnhandledExceptionDetails (int prcNum, String xClassName, String details, String... args){
  78     if (runDirectly) {
  79       return true;
  80     } else {
  81       numOfPrc = prcNum;
  82       unhandledException( getCaller(), xClassName, details, args);
  83       return false;
  84     }
  85   }
  86
  87   protected boolean mpVerifyUnhandledException (int prcNum, String xClassName, String... args){
  88     if (runDirectly) {
  89       return true;
  90     } else {
  91       numOfPrc = prcNum;
  92       unhandledException( getCaller(), xClassName, null, args);
  93       return false;
  94     }
  95   }
  96
  97   protected boolean mpVerifyJPFException (int prcNum, TypeRef xClsSpec, String... args){
  98     if (runDirectly) {
  99       return true;
 100
 101     } else {
 102       numOfPrc = prcNum;
 103       try {
 104         Class<? extends Throwable> xCls = xClsSpec.asNativeSubclass(Throwable.class);
 105
 106         jpfException( getCaller(), xCls, args);
 107
 108       } catch (ClassCastException ccx){
 109         fail("not a property type: " + xClsSpec);
 110       } catch (ClassNotFoundException cnfx){
 111         fail("property class not found: " + xClsSpec);
 112       }
 113       return false;
 114     }
 115   }
 116
 117   protected boolean mpVerifyPropertyViolation (int prcNum, TypeRef propertyClsSpec, String... args){
 118     if (runDirectly) {
 119       return true;
 120
 121     } else {
 122       numOfPrc = prcNum;
 123       try {
 124         Class<? extends Property> propertyCls = propertyClsSpec.asNativeSubclass(Property.class);
 125         propertyViolation( getCaller(), propertyCls, args);
 126
 127       } catch (ClassCastException ccx){
 128         fail("not a property type: " + propertyClsSpec);
 129       } catch (ClassNotFoundException cnfx){
 130         fail("property class not found: " + propertyClsSpec);
 131       }
 132       return false;
 133     }
 134   }
 135
 136   protected boolean mpVerifyDeadlock (int prcNum, String... args){
 137     if (runDirectly) {
 138       return true;
 139     } else {
 140       numOfPrc = prcNum;
 141       propertyViolation( getCaller(), NotDeadlockedProperty.class, args);
 142       return false;
 143     }
 144   }
 145 }