src/main/gov/nasa/jpf/listener/AssertionProperty.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.PropertyListenerAdapter;
  23 import gov.nasa.jpf.jvm.bytecode.ATHROW;
  24 import gov.nasa.jpf.search.Search;
  25 import gov.nasa.jpf.util.JPFLogger;
  26 import gov.nasa.jpf.vm.ClassInfo;
  27 import gov.nasa.jpf.vm.ElementInfo;
  28 import gov.nasa.jpf.vm.Heap;
  29 import gov.nasa.jpf.vm.Instruction;
  30 import gov.nasa.jpf.vm.VM;
  31 import gov.nasa.jpf.vm.StackFrame;
  32 import gov.nasa.jpf.vm.ThreadInfo;
  33
  34 /**
  35  * this is a property listener that turns thrown AssertionErrors into
  36  * property violations before they are caught (i.e. potentially
  37  * change the stack).
  38  * Besides serving the purpose of eliminating the "catch(Throwable)" case,
  39  * it can be used in conjunction with "search.multiple_errors=true" to
  40  * report assertions but otherwise ignore them and go on searching the
  41  * same path (otherwise, multiple_errors would cause a backtrack)
  42  */
  43 public class AssertionProperty extends PropertyListenerAdapter {
  44
  45   static JPFLogger log = JPF.getLogger("gov.nasa.jpf.listener.AssertionProperty");
  46
  47   boolean goOn;
  48   String msg;
  49
  50   public AssertionProperty (Config config) {
  51     goOn = config.getBoolean("ap.go_on",false);
  52   }
  53
  54   @Override
  55   public boolean check(Search search, VM vm) {
  56     return (msg == null);
  57   }
  58
  59   @Override
  60   public String getErrorMessage() {
  61     return msg;
  62   }
  63
  64   protected String getMessage (String details, Instruction insn){
  65     String s = "failed assertion";
  66
  67     if (details != null){
  68       s += ": \"";
  69       s += details;
  70       s += '"';
  71     }
  72
  73     s += " at ";
  74     s += insn.getSourceLocation();
  75
  76     return s;
  77   }
  78
  79   @Override
  80   public void executeInstruction (VM vm, ThreadInfo ti, Instruction insn){
  81
  82     if (insn instanceof ATHROW) {
  83
  84       Heap heap = vm.getHeap();
  85       StackFrame frame = ti.getTopFrame();
  86       int xobjref = frame.peek();
  87       ElementInfo ei = heap.get(xobjref);
  88       ClassInfo ci = ei.getClassInfo();
  89
  90       if (ci.getName().equals("java.lang.AssertionError")) {
  91         int msgref = ei.getReferenceField("detailMessage");
  92         ElementInfo eiMsg = heap.get(msgref);
  93         String details = eiMsg != null ? eiMsg.asString() : null;
  94
  95         // Ok, arm ourselves
  96         msg = getMessage( details, insn.getNext());
  97
  98         if (goOn) {
  99           log.warning(msg);
 100
 101           frame = ti.getModifiableTopFrame();
 102           frame.pop(); // ensure operand stack integrity (ATHROW pops)
 103
 104           ti.skipInstruction(insn.getNext());
 105
 106         } else {
 107           ti.skipInstruction(insn);
 108           ti.breakTransition("assertion");
 109         }
 110       }
 111     }
 112   }
 113
 114   @Override
 115   public void reset() {
 116     msg = null;
 117   }
 118 }