jpf.properties

   1 # JPF configuration for "jpf-core" component
   2
   3 # path elements can either be relative to the property file location, or
   4 # use the JPF component name (e.g. "jpf-core") as a variable prefix
   5 # (e.g. "jpf-core.sourcepath=${jpf-core}/src/examples").
   6 # If a jpf.properties is to be used within NB, it has to use the variable prefix
   7 # (prepending the project root is only done during JPF init)
   8
   9 # we use the ';' separator here because it is recognized by NetBeans (as opposed
  10 # to ',')
  11
  12 # 'config_path' is set automatically by gov.nasa.jpf.Config during JPF init.
  13 # If used from within an Ant build system, 'jpf-core' has to be set explicitly
  14 # (ant does ${..} property expansion, but ignores property redefinition, so the
  15 # following line will be ignored)
  16
  17 jpf-core = ${config_path}
  18
  19 jpf-core.native_classpath=\
  20   ${jpf-core}/build/jpf.jar;\
  21   ${jpf-core}/build/jpf-annotations.jar
  22
  23 jpf-core.classpath=\
  24   ${jpf-core}/build/jpf-classes.jar;\
  25   ${jpf-core}/build/examples
  26
  27 jpf-core.sourcepath=\
  28   ${jpf-core}/src/examples
  29
  30 jpf-core.test_classpath=\
  31   ${jpf-core}/build/tests
  32
  33 jpf-core.peer_packages = gov.nasa.jpf.vm,<model>,<default>
  34
  35
  36
  37 # the default jpf-core properties file with keys for which we need mandatory defaults
  38
  39 ########################### 0. global part ###############################
  40
  41 # instances that are both search and VM listeners
  42 #listener = ..
  43
  44 # do we want JPF exceptions to print their stack traces (that's only for
  45 # debugging)
  46 jpf.print_exception_stack = true
  47
  48
  49 # this is where we can specify additional classpath entries that are
  50 # not in the system property class.path (e.g. when running JPF from
  51 # an environment that uses it's own loaders, like Eclipse plugins etc.)
  52 #jpf.native_classpath = ..
  53
  54
  55 ########################### 1. Search part ###############################
  56 search.class = gov.nasa.jpf.search.DFSearch
  57
  58
  59 # This flag indicates whether state matching will only be done when a state
  60 # is revisited at a lower depth. By default this is false. If it is set to
  61 # true and no error is found in a limited-depth search then it is guaranteed
  62 # not to have such error below that depth. Note that for traditional
  63 # depth limited search this does not hold
  64 search.match_depth = false
  65
  66 # This flag indicates whether JPF should produce more than one error
  67 # or stop at the first one
  68 search.multiple_errors = false
  69
  70 # the minimum free memory bounds. If we fall below that threshold, we
  71 # stop the search
  72 search.min_free = 1M
  73
  74 # name of the file in which we store error paths. If not set, we don't store
  75 #search.error_path = error.xml
  76
  77 # the standard properties we want to check for
  78 search.properties=\
  79 gov.nasa.jpf.vm.NotDeadlockedProperty,\
  80 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
  81
  82
  83 # various heuristic parameters
  84
  85 # This number specifies the maximum number of states to keep on the queue
  86 # during a heuristic search. By default it is set to -1
  87 search.heuristic.queue_limit = -1
  88
  89 # This flag indicates whether branches with counts less than branch-start
  90 # are to be ranked according to how many times they have been taken.
  91 # It is set to true by default. If it is set to false, they are all valued
  92 # the same
  93 search.heuristic.branch.count_early = true
  94
  95 # This number determines at what point branches are heuristically valued as worse
  96 # than non-branching transitions. By default this value is 1.
  97 branch_start = 1
  98
  99
 100 # This number if greater than 0 is returned as the heuristic value for
 101 # non-branching transitions. By default it is set to -1 in which case the
 102 # value of branch-start is returned instead
 103 search.heuristic.branch.no_branch_return = -1
 104
 105 # exclusive search listeners
 106 # search.listener =
 107
 108
 109 ############################### 2. VM part ###############################
 110
 111
 112 # this is an ordered list of packages from which we try to locate native peers.
 113 # "<model>" means JPF tries the same package like the model class
 114 # "<default>" means no package at all
 115 # (this is going to be extended by jpf.properties files)
 116 #peer_packages = <model>,<default>
 117
 118
 119 vm.class = gov.nasa.jpf.vm.SingleProcessVM
 120
 121 # the ClassLoaderInfo class used for startup
 122 vm.classloader.class = gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo
 123
 124 # class used to hash/store states (if not set, states are not matched)
 125 vm.storage.class = gov.nasa.jpf.vm.JenkinsStateSet
 126
 127 # class used to maintain the backtrack stack
 128 vm.backtracker.class = gov.nasa.jpf.vm.DefaultBacktracker
 129
 130 # serializer to be used by state set (vm.storage.class)
 131 vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer
 132 #vm.serializer.class = gov.nasa.jpf.vm.serialize.AdaptiveSerializer
 133 #vm.serializer.class = gov.nasa.jpf.vm.serialize.FilteringSerializer
 134
 135 # the class that models static fields and classes
 136 vm.statics.class = gov.nasa.jpf.vm.OVStatics
 137
 138 # the class that models the heap
 139 #vm.heap.class = gov.nasa.jpf.vm.PSIMHeap
 140 vm.heap.class = gov.nasa.jpf.vm.OVHeap
 141
 142 # the class representing the list of all threads
 143 vm.threadlist.class = gov.nasa.jpf.vm.ThreadList
 144
 145 # restorer to be used by backtracker such as DefaultBacktracker UNLESS a
 146 # serializer that is also a restorer (such as CollapsingSerializer) is used.
 147 # I.e. this is only read if serializer is not used or it's not a StateRestorer
 148 vm.restorer.class = .vm.DefaultMementoRestorer
 149
 150 # where do we get the standard libraries from?
 151 # "<system>" is replaced by the host VM sun.boot.class.path setting
 152 vm.boot_classpath = <system>
 153
 154 # instruction factory
 155 jvm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory
 156
 157 # fields factory
 158 vm.fields_factory.class = gov.nasa.jpf.vm.DefaultFieldsFactory
 159
 160 # pattern list for assertion enabled/disabled classes
 161 #vm.enable_assertions = *
 162 #vm.disable_assertions=
 163
 164 # do we support the Verify.ignorePath() API (to imperatively ignore paths in modeled/instrumented programs)?
 165 vm.verify.ignore_path = true
 166
 167
 168 vm.scheduler.class = gov.nasa.jpf.vm.DelegatingScheduler
 169 vm.scheduler.sync.class = gov.nasa.jpf.vm.AllRunnablesSyncPolicy
 170 vm.scheduler.sharedness.class = gov.nasa.jpf.vm.PathSharednessPolicy
 171
 172 # the following properties can be used to set filters for GenericSharednessPolicy instances
 173
 174 # never break on exposure or shared field access from matching methods.
 175 # NOTE - this is transitive and hence should only include a minimal set of trusted methods
 176 vm.shared.never_break_methods=\
 177       java.util.concurrent.ThreadPoolExecutor.processWorkerExit,\
 178       java.util.concurrent.locks.Abstract*Synchronizer.*,\
 179       java.util.concurrent.ThreadPoolExecutor.getTask,\
 180       java.util.concurrent.atomic.Atomic*.*,\
 181       java.util.concurrent.Exchanger.doExchange,\
 182       java.util.concurrent.ThreadPoolExecutor.interruptIdleWorkers,\
 183       java.util.concurrent.TimeUnit.*
 184
 185 vm.shared.never_break_types=\
 186       java.util.concurrent.TimeUnit
 187
 188 # never break on shared access of the following fields. While this is less prone to
 189 # masking defects than never_break_methods, it should also be used sparingly.
 190 # NOTE - java.lang.Thread* fields should not be excluded if the SUT explicitly uses
 191 # Thread or ThreadGroup objects
 192 vm.shared.never_break_fields=\
 193       java.lang.Thread*.*,\
 194       java.lang.System.*,\
 195       java.lang.Runtime.*,\
 196       java.lang.Boolean.*,\
 197       java.lang.String.*,\
 198       java.lang.*.TYPE,\
 199       java.util.HashMap.EMPTY_TABLE,\
 200       java.util.HashSet.PRESENT,\
 201       java.util.concurrent.ThreadPoolExecutor*.*,\
 202       java.util.concurrent.ThreadPoolExecutor*.*,\
 203       java.util.concurrent.TimeUnit.*,\
 204       java.util.concurrent.Exchanger.CANCEL,\
 205       java.util.concurrent.Exchanger.NULL_ITEM,\
 206       java.util.concurrent.Executors$DefaultThreadFactory.*,\
 207       sun.misc.VM.*,\
 208       sun.misc.SharedSecrets.*,\
 209       sun.misc.Unsafe.theUnsafe,\
 210       gov.nasa.jpf.util.test.TestJPF.*
 211
 212
 213 # do we also break transitions on reference field puts that could make the
 214 # referenced objects shared
 215 vm.shared.break_on_exposure = true
 216
 217 # do we try to deduce if a field is supposed to be protected by a lock? In this
 218 # case, we stop to treat this field as a boundary step, but only if we see the lock
 219 vm.shared.sync_detection = true
 220
 221 # do we assume final fields to be race-safe (not really true, esp. for
 222 # instance fields with references leaking from a ctor, but a good starting point)
 223 vm.shared.skip_finals=true
 224
 225 # ClassLoaders synchronize the loading of a class.
 226 # Thus, static final fields can never be included in a race condition since only 1 thread is allowed to access the class while it is loading.
 227 # Defaulted to false to maintain backward compatibility in JPF
 228 vm.shared.skip_static_finals=false
 229
 230 # When an object's constructor has returned, then the final fields can not be changed.
 231 # Thus, instance final fields can never be included in a race condition (unless the this reference is leaked from a constructor)
 232 # Defaulted to false to maintain backward compatibility in JPF
 233 vm.shared.skip_constructed_finals=false
 234
 235
 236 # do we ignore explicitly set Thread.UncaughtHandlers
 237 vm.ignore_uncaught_handler=false
 238
 239 # do we treat returned Thread.UncaughtHandler.uncaughtException() calls as normal thread termination
 240 vm.pass_uncaught_handler=true
 241
 242 # do we reclaim unused memory (run garbage collection)
 243 vm.gc = true
 244
 245 # threshold after which number of allocations to perform a garbage collection
 246 # (even within the same transition, to avoid lots of short living objects)
 247 # -1 means never
 248 vm.max_alloc_gc = -1
 249
 250 # do we run finalizers on collected objects (only makes sense with garbage collection)
 251 vm.finalize = false
 252
 253 # this is a preemption boundary specifying the max number of instructions after which we
 254 # break the current transition if there are other runnable threads
 255 vm.max_transition_length = 50000
 256
 257 # are thread ids of terminated threads with recycled thread objects reused when creating new
 258 # threads. This is required for programs that sequentially create many short living threads
 259 vm.reuse_tid = false
 260
 261 # do we want to halt execution on each throw of an exception that matches
 262 # one of the given classname wildcard patterns w/o looking for exception handlers?
 263 # (useful for empty handler blocks, over-permissive catches or generally
 264 # misused exceptions)
 265 #vm.halt_on_throw = *
 266
 267 # class that is used to create scheduling relevant choice generators.
 268 # this will replace the scheduler
 269 vm.scheduler_factory.class = gov.nasa.jpf.vm.DefaultSchedulerFactory
 270
 271 # print output as it is generated during the search (for all paths)
 272 vm.tree_output = true
 273
 274 # collect output inside the stored path (to create program trace outout)
 275 vm.path_output = false
 276
 277 # do we want to store the whole path no matter if we report them
 278 vm.store_steps=false
 279
 280 # untracked property
 281 vm.untracked = true
 282
 283 # from where do we initialize the system properties
 284 #   SELECTED - keys specified as vm.system.properties, values from host
 285 #   FILE - Java properties file (key=value pairs)
 286 #   HOST - all system properties from underlying host VM
 287 vm.sysprop.source = SELECTED
 288
 289 # pathname of property file with system properties
 290 #vm.sysprop.file =
 291
 292 # list of key names to load from host VM
 293 #vm.sysprop.keys =
 294
 295 # class we use to model execution time
 296 vm.time.class = gov.nasa.jpf.vm.SystemTime
 297
 298 # if this is set to true, we throw an exception if we encounter any orphan native peer methods
 299 vm.no_orphan_methods = false
 300
 301 # if this is set to true, overriden finalize() methods execute upon objects garbage collections
 302 vm.process_finalizers = false
 303
 304
 305 ### jvm specifics
 306
 307 # di=o we model nested locks during class init (to detect possible hotspot dealocks during init)
 308 # (off by default since it can cause state explosion)
 309 jvm.nested_init=false
 310
 311 # if so, for which classes (default is to exclude system classes)
 312 jvm.nested_init.exclude=java.*,javax.*,sun.misc.*
 313
 314
 315 ############################### 3. CG part ###############################
 316
 317 # choice randomization policy in effect:
 318 #   "NONE" - choice sets are not randomized
 319 #   "FIXED_SEED" - choice sets are randomized using a fixed seed for each JPF run (reproducible)
 320 #   "VAR_SEED" - choice sets are randomized using a variable seed for each JPF run
 321 cg.randomize_choices = NONE
 322
 323 # the standard seed value used for the FIXED_SEED policy
 324 cg.seed = 42
 325
 326
 327 # if this is set, we create choice generators even if there is only a single
 328 # choice. This is to ensure state storage/matching at all locations where a
 329 # choice generator *could* be created. The default should be to turn it off though,
 330 # since this can produce a lot of additional states (esp. with threads)
 331 cg.break_single_choice = false
 332
 333
 334 # default BooleanChoiceGenerator sequence: do we start with 'false'
 335 cg.boolean.false_first = true
 336
 337 # do we want java.util.Random. nextXX() enumerate choices, or just return a single value?
 338 # (isn't implemented for all types yet)
 339 cg.enumerate_random=false
 340
 341 # maximum number of processors returned by Runtime.availableProcessors(). If this is
 342 # greater than 1, the call represents a ChoiceGenerator
 343 cg.max_processors=1
 344
 345 # creates a CG upon Thread.start, i.e. breaks the starting transition. Note this is
 346 # required for data race detection (which depends on detecting access of shared objects)
 347 cg.threads.break_start=true
 348
 349 # if this option is set we break the transition on Thread.yield()
 350 cg.threads.break_yield=true
 351
 352 # if this option is set we break the transition on Thread.sleep()
 353 cg.threads.break_sleep=true
 354
 355 # set if we shold also break on array instructions, e.g. to detect races
 356 # for array elements. This is off by default because it can cause serious
 357 # state explosion
 358 cg.threads.break_arrays=false
 359
 360 # do we support atomic sections. If set to false, Verify.beginAtomic()/endAtomic()
 361 # will not do anything
 362 cg.enable_atomic=true
 363
 364 ############################### 3. Report Part ###############################
 365 log.handler.class=gov.nasa.jpf.util.LogHandler
 366
 367 # Windows seem to have a different default
 368 log.level=warning
 369
 370 report.class=gov.nasa.jpf.report.Reporter
 371 report.publisher=console
 372
 373 report.console.class=gov.nasa.jpf.report.ConsolePublisher
 374
 375 # this prints out repository information if the 'jpf' topic is set (for debugging)
 376 #jpf.report.show_repository=true
 377
 378 #property violation reporting is configured separately
 379 report.console.start=jpf,sut
 380
 381 report.console.transition=
 382 report.console.constraint=constraint,snapshot
 383
 384 report.console.probe=statistics
 385
 386 report.console.property_violation=error,snapshot
 387 report.console.show_steps=true
 388 report.console.show_method=true
 389 report.console.show_code=false
 390
 391 report.console.finished=result,statistics
 392
 393 #jpf.report.console.show_steps=true
 394 #jpf.report.console.show_method=true
 395 #jpf.report.console.show_code=true
 396
 397 report.xml.class=gov.nasa.jpf.report.XMLPublisher
 398
 399 report.html.class=gov.nasa.jpf.report.HTMLPublisher
 400 report.html.start=jpf,sut,platform,user,dtg,config
 401 report.html.constraint=constraint
 402 report.html.property_violation=
 403 report.html.finished=result,statistics,error,snapshot,output
 404
 405
 406 ############################### 4. Listener part #############################
 407
 408 # imperative list of listeners
 409 #listener=
 410
 411 listener.autoload=\
 412   gov.nasa.jpf.NonNull,\
 413   gov.nasa.jpf.Const
 414
 415 listener.gov.nasa.jpf.NonNull=gov.nasa.jpf.tools.NonNullChecker
 416 listener.gov.nasa.jpf.Const=gov.nasa.jpf.tools.ConstChecker
 417
 418
 419 ### PreciseRaceDetector
 420
 421 # we don't check for races in standard libraries
 422 race.exclude=java.*,javax.*
 423
 424
 425 ############################### 5. test part #############################
 426
 427 test.report.console.finished=result