Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java @ 21:caa0924e093d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reshuffled Event hierarchy, introducing SystemEvent, with CheckEvent and ControlEvent being subclasses of SystemEvent added Loggable.setLogLevel changed old UserHeuristic to use a Verify.heuristicValue instead of a hardwired "Main" class with hardwired fields (which was just an outdated leftover). Call Verify.setHeuristicValue() to control state priorities from the SUT. This also fixes the bug that UserHeuristic was not properly checking for "Main" resolution.
author Peter Mehlitz <pcmehlitz@gmail.com>
date Fri, 10 Apr 2015 20:53:11 -0700
parents f6886b2bda4a
children cd7880ab73c7
comparison
equal deleted inserted replaced
20:b1790909ebb1 21:caa0924e093d
51 * 51 *
52 * this peer is a bit different in that it only uses static fields and methods because 52 * this peer is a bit different in that it only uses static fields and methods because
53 * its use is supposed to be JPF global (without classloader namespaces) 53 * its use is supposed to be JPF global (without classloader namespaces)
54 */ 54 */
55 public class JPF_gov_nasa_jpf_vm_Verify extends NativePeer { 55 public class JPF_gov_nasa_jpf_vm_Verify extends NativePeer {
56 static final int MAX_COUNTERS = 10; 56 static final int MAX_COUNTERS = 127;
57 57
58 static boolean isInitialized; 58 static boolean isInitialized;
59 59
60 // those are used to store search global int values (e.g. from TestJPF derived classes) 60 // those are used to store search global int values (e.g. from TestJPF derived classes)
61 static int[] counter; 61 static int[] counter;
62 static IntTable<String> map; 62 static IntTable<String> map;
63 63
64 public static int heuristicSearchValue;
64 65
65 static boolean supportIgnorePath; 66 static boolean supportIgnorePath;
66 static boolean breakSingleChoice; 67 static boolean breakSingleChoice;
67 static boolean enableAtomic; 68 static boolean enableAtomic;
68 69
82 83
83 if (!isInitialized){ 84 if (!isInitialized){
84 supportIgnorePath = conf.getBoolean("vm.verify.ignore_path"); 85 supportIgnorePath = conf.getBoolean("vm.verify.ignore_path");
85 breakSingleChoice = conf.getBoolean("cg.break_single_choice"); 86 breakSingleChoice = conf.getBoolean("cg.break_single_choice");
86 enableAtomic = conf.getBoolean("cg.enable_atomic", true); 87 enableAtomic = conf.getBoolean("cg.enable_atomic", true);
88
89 heuristicSearchValue = conf.getInt("search.heuristic.default_value");
87 90
88 counter = null; 91 counter = null;
89 map = null; 92 map = null;
90 93
91 config = conf; 94 config = conf;
104 107
105 Verify.setPeerClass( JPF_gov_nasa_jpf_vm_Verify.class); 108 Verify.setPeerClass( JPF_gov_nasa_jpf_vm_Verify.class);
106 109
107 RunRegistry.getDefaultRegistry().addListener( new RunListener() { 110 RunRegistry.getDefaultRegistry().addListener( new RunListener() {
108 @Override 111 @Override
109 public void reset (RunRegistry reg){ 112 public void reset (RunRegistry reg){
110 isInitialized = false; 113 isInitialized = false;
111 } 114 }
112 }); 115 });
113 } 116 }
114 return true; 117 return true;
953 /** 956 /**
954 * deprecated, use getInt 957 * deprecated, use getInt
955 */ 958 */
956 @MJI 959 @MJI
957 public static int random__I__I (MJIEnv env, int clsObjRef, int x) { 960 public static int random__I__I (MJIEnv env, int clsObjRef, int x) {
958 return getInt__II__I( env, clsObjRef, 0, x); 961 return getInt__II__I(env, clsObjRef, 0, x);
959 } 962 }
960 963
961 static void boring__Z__V (MJIEnv env, int clsObjRef, boolean b) { 964 static void boring__Z__V (MJIEnv env, int clsObjRef, boolean b) {
962 env.getSystemState().setBoring(b); 965 env.getSystemState().setBoring(b);
963 } 966 }
983 @MJI 986 @MJI
984 public static void terminateSearch____V (MJIEnv env, int clsObjRef) { 987 public static void terminateSearch____V (MJIEnv env, int clsObjRef) {
985 JPF jpf = env.getVM().getJPF(); 988 JPF jpf = env.getVM().getJPF();
986 jpf.getSearch().terminate(); 989 jpf.getSearch().terminate();
987 } 990 }
991
992 @MJI public static void setHeuristicSearchValue__I__V (MJIEnv env, int clsObjRef, int val){
993 heuristicSearchValue = val;
994 }
995
996 @MJI public static int getHeuristicSearchValue____I (MJIEnv env, int clsObjRef){
997 return heuristicSearchValue;
998 }
999
1000 @MJI public static void resetHeuristicSearchValue____V (MJIEnv env, int clsObjRef){
1001 heuristicSearchValue = config.getInt("search.heuristic.default_value");
1002 }
1003
1004
988 1005
989 @MJI 1006 @MJI
990 public static boolean isTraceReplay____Z (MJIEnv env, int clsObjRef) { 1007 public static boolean isTraceReplay____Z (MJIEnv env, int clsObjRef) {
991 return env.getVM().isTraceReplay(); 1008 return env.getVM().isTraceReplay();
992 } 1009 }