rgse.jpf

jpf-core = ${config_path}

jpf-core.native_classpath=\
  ./lib/jpf.jar;\
  ./lib/jpf-annotations.jar;\
  ./lib/junit-4.10.jar

jpf-core.classpath=\
  ./lib/jpf-classes.jar

jpf-symbc = ${config_path}

jpf-symbc.native_classpath=\
  ./lib/jpf-symbc.jar;\
  ./lib/jpf-symbc-annotations.jar
  
jpf-symbc.classpath=\
  ./lib/jpf-symbc-classes.jar
 
 
jpf-jdart = ${config_path}

jpf-jdart.native_classpath=\
  ./lib/jpf-jdart.jar
  
jpf-jdart.classpath=\
  ./lib/jpf-jdart-classes.jar  


jpf-nhandler = ${config_path}

jpf-nhandler.native_classpath =\
   ./lib/jpf-nhandler.jar

jpf-nhandler.classpath =\
   ./lib/jpf-nhandler-classes.jar


jpf-core.peer_packages = gov.nasa.jpf.jvm,<model>,<default>

# the default jpf-core properties file with keys for which we need mandatory defaults

########################### 0. global part ###############################

# instances that are both search and VM listeners
#listener = ..

# do we want JPF exceptions to print their stack traces (that's only for
# debugging)
jpf.print_exception_stack = true


# this is where we can specify additional classpath entries that are
# not in the system property class.path (e.g. when running JPF from
# an environment that uses it's own loaders, like Eclipse plugins etc.)
#jpf.native_classpath = ..


########################### 1. Search part ###############################
search.class = gov.nasa.jpf.search.DFSearch


# This flag indicates whether state matching will only be done when a state
# is revisited at a lower depth. By default this is false. If it is set to
# true and no error is found in a limited-depth search then it is guaranteed
# not to have such error below that depth. Note that for traditional
# depth limited search this does not hold
search.match_depth = false

# This flag indicates whether JPF should produce more than one error
# or stop at the first one
search.multiple_errors = false

# the minimum free memory bounds. If we fall below that threshold, we
# stop the search
search.min_free = 1M

# name of the file in which we store error paths. If not set, we don't store
#search.error_path = error.xml

# the standard properties we want to check for
search.properties=\
gov.nasa.jpf.jvm.NotDeadlockedProperty,\
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty


# various heuristic parameters

# This number specifies the maximum number of states to keep on the queue
# during a heuristic search. By default it is set to -1
search.heuristic.queue_limit = -1

# This flag indicates whether branches with counts less than branch-start
# are to be ranked according to how many times they have been taken.
# It is set to true by default. If it is set to false, they are all valued
# the same
search.heuristic.branch.count_early = true

# This number determines at what point branches are heuristically valued as worse
# than non-branching transitions. By default this value is 1.
branch_start = 1


# This number if greater than 0 is returned as the heuristic value for
# non-branching transitions. By default it is set to -1 in which case the
# value of branch-start is returned instead
search.heuristic.branch.no_branch_return = -1

# exclusive search listeners
# search.listener =


############################### 2. VM part ###############################


# this is an ordered list of packages from which we try to locate native peers.
# "<model>" means JPF tries the same package like the model class
# "<default>" means no package at all
# (this is going to be extended by jpf.properties files)
#peer_packages = <model>,<default>


vm.class = gov.nasa.jpf.jvm.JVM

# class used to hash/store states (if not set, states are not matched)
vm.storage.class = gov.nasa.jpf.jvm.JenkinsStateSet

# class used to maintain the backtrack stack
vm.backtracker.class = gov.nasa.jpf.jvm.DefaultBacktracker

# serializer to be used by state set (vm.storage.class)
vm.serializer.class = gov.nasa.jpf.jvm.serialize.CFSerializer
#vm.serializer.class = gov.nasa.jpf.jvm.serialize.AdaptiveSerializer
#vm.serializer.class = gov.nasa.jpf.jvm.serialize.FilteringSerializer

# the class that models static fields and classes
vm.static.class = gov.nasa.jpf.jvm.StaticArea

# the class that models the heap
#vm.heap.class = gov.nasa.jpf.jvm.DynamicArea
vm.heap.class = gov.nasa.jpf.jvm.SparseClusterArrayHeap

# the class representing the list of all threads
vm.threadlist.class = gov.nasa.jpf.jvm.ThreadList

# restorer to be used by backtracker such as DefaultBacktracker UNLESS a
# serializer that is also a restorer (such as CollapsingSerializer) is used.
# I.e. this is only read if serializer is not used or it's not a StateRestorer
vm.restorer.class = .jvm.DefaultMementoRestorer

# instruction factory
vm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory

# fields factory
vm.fields_factory.class = gov.nasa.jpf.jvm.DefaultFieldsFactory

# class used to set method and field attributes at class load time
vm.attributor.class = gov.nasa.jpf.jvm.DefaultAttributor

# pattern list for assertion enabled/disabled classes
#vm.enable_assertions = *
#vm.disable_assertions=

# do we support the Verify.ignorePath() API (to imperatively ignore paths in modeled/instrumented programs)?
vm.verify.ignore_path = true

# do we want on-the-fly partial order reduction?
vm.por = true

# do we treat field access of objects that are reachable from different threads as
# transaction boundaries (in case there is more tha one thread)?
vm.por.field_boundaries = true

# access to fields with these patterns we never treat as transition boundaries
vm.por.field_boundaries.never = java.*,javax.*,sun.*

# access to fields with these patterns we break on (if object is shared and
# vm.por.field_boundaries is set - note it's only meaningful if sync_detection
# is set because otherwse we would break anyways)
vm.por.field_boundaries.break =

# do we try to deduce if a field is supposed to be protected by a lock? In this
# case, we stop to treat this field as a boundary step, but only if we see the lock
vm.por.sync_detection = true

# used to detect if a field is lock protected - only required if we use on-the-fly POR
# with sync-detection
vm.por.fli_factory.class = gov.nasa.jpf.jvm.StatisticFieldLockInfoFactory

# do we assume final fields to be race-safe (not really true, esp. for
# instance fields with references leaking from a ctor, but a good starting point)
vm.por.skip_finals=true

# ClassLoaders synchronize the loading of a class.
# 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.
# Defaulted to false to maintain backward compatibility in JPF
vm.por.skip_static_finals=false

# When an object's constructor has returned, then the final fields can not be changed.
# Thus, instance final fields can never be included in a race condition (unless the this reference is leaked from a constructor)
# Defaulted to false to maintain backward compatibility in JPF
vm.por.skip_constructed_finals=false

# do we ignore explicitly set Thread.UncaughtHandlers
vm.ignore_uncaught_handler=false

# do we treat returned Thread.UncaughtHandler.uncaughtException() calls as normal thread termination
vm.pass_uncaught_handler=true

# do we reclaim unused memory (run garbage collection)
vm.gc = true

# threshold after which number of allocations to perform a garbage collection
# (even within the same transition, to avoid lots of short living objects)
# -1 means never
vm.max_alloc_gc = -1 

# do we run finalizers on collected objects (only makes sense with garbage collection)
vm.finalize = false

# this is a preemption boundary specifying the max number of instructions after which we
# break the current transition if there are other runnable threads
vm.max_transition_length = 5000

# are thread ids of terminated threads with recycled thread objects reused when creating new
# threads. This is required for programs that sequentially create many short living threads
vm.reuse_tid = false

# do we want to halt execution on each throw of an exception that matches
# one of the given classname wildcard patterns w/o looking for exception handlers?
# (useful for empty handler blocks, over-permissive catches or generally
# misused exceptions)
#vm.halt_on_throw = *

# class that is used to create scheduling relevant choice generators.
# this will replace the scheduler
vm.scheduler_factory.class = gov.nasa.jpf.jvm.DefaultSchedulerFactory

# print output as it is generated during the search (for all paths)
vm.tree_output = true

# collect output inside the stored path (to create program trace outout)
vm.path_output = false

# do we want to store the whole path no matter if we report them
vm.store_steps=false

# untracked property
vm.untracked = true

# from where do we initialize the system properties
#   SELECTED - keys specified as vm.system.properties, values from host
#   FILE - Java properties file (key=value pairs)
#   HOST - all system properties from underlying host VM
vm.sysprop.source = SELECTED

# pathname of property file with system properties
#vm.sysprop.file =

# list of key names to load from host VM
#vm.sysprop.keys =

# class we use to model execution time
vm.time.class = gov.nasa.jpf.jvm.SystemTime

# if this is set to true, we throw an exception if we encounter any orphan native peer methods
vm.no_orphan_methods = false

############################### 3. CG part ###############################

# choice randomization policy in effect:
#   "NONE" - choice sets are not randomized
#   "FIXED_SEED" - choice sets are randomized using a fixed seed for each JPF run (reproducible)
#   "VAR_SEED" - choice sets are randomized using a variable seed for each JPF run
cg.randomize_choices = NONE

# the standard seed value used for the FIXED_SEED policy
cg.seed = 42


# if this is set, we create choice generators even if there is only a single
# choice. This is to ensure state storage/matching at all locations where a
# choice generator *could* be created. The default should be to turn it off though,
# since this can produce a lot of additional states (esp. with threads)
cg.break_single_choice = false


# default BooleanChoiceGenerator sequence: do we start with 'false'
cg.boolean.false_first = true

# do we want java.util.Random. nextXX() enumerate choices, or just return a single value?
# (isn't implemented for all types yet)
cg.enumerate_random=false

# maximum number of processors returned by Runtime.availableProcessors(). If this is
# greater than 1, the call represents a ChoiceGenerator
cg.max_processors=1

# creates a CG upon Thread.start, i.e. breaks the starting transition. Note this is
# required for data race detection (which depends on detecting access of shared objects)
cg.threads.break_start=true

# if this option is true, CG is not created when yield() (Thread API)
# is called
cg.threads.break_yield=true

# if this option is true, CG is not created when sleep() (Thread API)
# is called
cg.threads.break_sleep=true

# set if we shold also break on array instructions, e.g. to detect races
# for array elements. This is off by default because it can cause serious
# state explosion
cg.threads.break_arrays=false

# do we support atomic sections. If set to false, Verify.beginAtomic()/endAtomic()
# will not do anything
cg.enable_atomic=true

############################### 3. Report Part ###############################
log.handler.class=gov.nasa.jpf.util.LogHandler

# Windows seem to have a different default
log.level=warning

report.class=gov.nasa.jpf.report.Reporter
report.publisher=console

report.console.class=gov.nasa.jpf.report.ConsolePublisher

# this prints out repository information if the 'jpf' topic is set (for debugging)
#jpf.report.show_repository=true

#property violation reporting is configured separately
report.console.start=jpf,sut

report.console.transition=
report.console.constraint=constraint,snapshot

report.console.property_violation=error,snapshot
report.console.show_steps=true
report.console.show_method=true
report.console.show_code=false

report.console.finished=result,statistics

#jpf.report.console.show_steps=true
#jpf.report.console.show_method=true
#jpf.report.console.show_code=true

report.xml.class=gov.nasa.jpf.report.XMLPublisher

report.html.class=gov.nasa.jpf.report.HTMLPublisher
report.html.start=jpf,sut,platform,user,dtg,config
report.html.constraint=constraint
report.html.property_violation=
report.html.finished=result,statistics,error,snapshot,output


############################### 4. Listener part #############################

# imperative list of listeners
#listener=

listener.autoload=\
  gov.nasa.jpf.NonNull,\
  gov.nasa.jpf.Const

listener.gov.nasa.jpf.NonNull=gov.nasa.jpf.tools.NonNullChecker
listener.gov.nasa.jpf.Const=gov.nasa.jpf.tools.ConstChecker


### PreciseRaceDetector

# we don't check for races in standard libraries
race.exclude=java.*,javax.*


############################### 5. test part #############################

test.report.console.finished=result


### configurations specific to the symbc project

# note we have to use the "+<key>=.." prepend notation since the NetBeans/Ant
# property parser doesn't like recursion
+peer_packages = gov.nasa.jpf.symbc;

#vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
# no state matching
vm.storage.class=nil

# zyf: test Green
#symbolic.green=true
#symbolic.solver.slicing=true
#symbolic.solver.canonization=true
#symbolic.solver.store=true
#solver
#symbolic.solver.dp=choco



##########################zyf: SSE experiments################################
# no state matching
vm.storage.class=nil  


symbolic.dp=yices
#symbolic.dp=cvc3
#choco.time_bound=60000

#on lazy initialization 
symbolic.lazy=false


#symbolic.debug=true
#symbolic.speculative.debug=true 

#multiple errors
search.multiple_errors=true  

# original SPF SE
search.class = gov.nasa.jpf.symbc.speculative.search.DefaultDFSearch
vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory

#search.class = gov.nasa.jpf.search.heuristic.DFSHeuristic
  
# search depth limit for large programs
search.depth_limit=27
 
#speculative SE  
#symbolic.speculative.depth=2
#vm.class=gov.nasa.jpf.symbc.speculative.vm.SpeculativeJVM
#search.class = gov.nasa.jpf.symbc.speculative.search.SpeculativeSegmentDFSearch
#vm.insn_factory.class=gov.nasa.jpf.symbc.speculative.SpeculativeSymbolicInstructionFactory
  

#speculation + heuristic search
#symbolic.speculative.depth=20
#vm.class=gov.nasa.jpf.symbc.speculative.vm.SpeculativeJVM
#vm.insn_factory.class=gov.nasa.jpf.symbc.speculative.SpeculativeHeuristicSymbolicInstructionFactory
#search.class = gov.nasa.jpf.symbc.speculative.search.SpeculativeDFSHeuristic
#search.class = gov.nasa.jpf.symbc.speculative.search.SpeculativeBFSHeuristic
 
#absurdity based optimization in (speculative) SE 
#absurdity.based.optimization=false
#absurdity.based.optimization=true  

#use yices' instant checking functionality to trim the speculation segment
#indeed, this is based on the incremental solving facility of Yices
#use.yices.instant.checking.result.to.trim.segment=true 

#explore which side of the branch instruction first?.It should be 0 or 1
#0: explore false side first
#1: explore true side first
###### ==0, true side first for the java program, false side first for bytecode
#explore.branchSide.first=0  
###### ==1, false side first for the java program, true side first for bytecode
#explore.branchSide.first=1
 

#############record constraint solving time? 
constraint.solving.time.record=true
 
#symbolic.choco_time_bound=60000
#Djava.library.path=${jpf-symbc}/jpf-symbc/lib 
#symbolic.minreal=-1000000.0
#symbolic.maxreal=1000000.0

#symbolic.minint=-10
#symbolic.maxint=10

 
 
#listeners
## comments: if multiple listeners, use  ;  between them, can not use multiple +listener 
#+listener=gov.nasa.jpf.listener.InsnCounter;
#+listener=gov.nasa.jpf.listener.CoverageAnalyzer
 
#unsatisfiable core based backtracking optimization in speculative SE
#UC.based.backtracking.optimization=true

 
##################use yices fast check facility################
#zyf comments: yices fast check means that if yices output unsat, we don't add the rest constraints
#in the same problem. This is used to save time in every unsat solving. But it does not used to
#trim the speculative segment. For example, in the binary search backtracking, the fast check can
#be used to save every unsat solving time.
# In the UC backtracking mode, this fast check can also be used.
#yices.fast.check=true                
###############################################################

  
 
#################### zyf: use symbolic array with symbolic length

##############array with symbolic length 
#symbolic.array.length=true
##############array with symbolic region, means that a symbolic array may ref to multiple regions, handled as lazy SE
#symbolic.array.region=true
##############heap supporting symbolic array storage
#vm.heap.class = gov.nasa.jpf.symbc.array.SparseClusterArrayHeapWithSymArray
##############exploration order: which path first
#symbolic.array.exploreLegalIndexFirst=false

##############how to solve for array
#symbolic.array.element.expression=ite
#symbolic.array.element.expression=arraytheory // not available now


vm.insn_factory.class=gov.nasa.jpf.jdart.ConcolicInstructionFactory

# using jpf-nhandler to delegate native method
# @using=jpf-nhandler

jpf-nhandler.peer_packages = test.converter

vm.sysprop.source=host

listener+=,gov.nasa.jpf.vm.JVMForwarder

#################################################################################

## By setting this to true, all the peers (both classes and source files) created 
## on the fly, in the onthefly dir, are removed once the search starts.
nhandler.clean = true

## By setting this to false, the map keeping JVM objects on the host VM side is
## not reset after each delegation.
## <todo> - note that we don't maintain the states of JVM objects for now, i.e.
## if a JPF object changes we do not affect the similar changes on the JVM side.
nhandler.resetVMState = true

## By setting this to true the source code for native peers will be generated.
## To compile the edited sources, run the script jpf-nhandler/bin/compileOTF
nhandler.genSource = true

## By setting this to true the body of the methods will be commented.
nhandler.addComment = false

## By setting this to true states of JPF objects are updated from their corresponding
## JVM objects
nhandler.updateJPFState = true

## By setting this to true all unhandled native calls will be handled.
# nhandler.delegateUnhandledNative = true

## By setting this to true all unhandled native calls will be skipped, i.e. they
## are executed as they are empty and return some dummey value.
# nhandler.skipNative = true

#################################################################################
## Using the following three options user can configure which methods to delegate,
## to skip, and to ignore. You should follow the same format as in MethodSpec 
## that can match methods/args against specs
##
## some examples:
##   "x.y.Foo.*"
##   "x.y.F*"
#################################################################################

## List of the methods to be delegated by jpf-nhandler.
nhandler.spec.delegate = 

## Only native methods among this list will be delegated by jpf-nhandler.
nhandler.spec.delegateNative = 

## List of the methods to be skipped, i.e. they are executed as they are empty
## and return some dummey value.
nhandler.spec.skip = 

## List of methods to be filtered.
nhandler.spec.filter = 

#################################################################################
## <2do> - this option has not been implemented yet.
## by setting this to true, nhandler creates the on-the-fly peer classes while 
## handling & skipping the methods, OW it just execute them directly outside of 
## on-the-fly peers
# nhandler.create.OTF_peers = true