diff options
| -rw-r--r-- | .SRCINFO | 19 | ||||
| -rw-r--r-- | .gitignore | 6 | ||||
| -rw-r--r-- | PKGBUILD | 34 | ||||
| -rw-r--r-- | jpf | 13 | ||||
| -rw-r--r-- | jpf.properties | 420 |
5 files changed, 492 insertions, 0 deletions
diff --git a/.SRCINFO b/.SRCINFO new file mode 100644 index 000000000000..b3d23dad7583 --- /dev/null +++ b/.SRCINFO @@ -0,0 +1,19 @@ +pkgbase = jpf-core-bin + pkgdesc = An extensible software model checking framework for Java bytecode programs + pkgver = r32 + pkgrel = 1 + url = https://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-core + arch = any + license = APACHE + depends = java-environment-openjdk>=8 + provides = jpf-core + conflicts = jpf-core + source = https://babelfish.arc.nasa.gov/trac/jpf/raw-attachment/wiki/projects/jpf-core/jpf-core-r32.zip + source = jpf + source = jpf.properties + md5sums = a9a3cff397180a533a93fd434241a225 + md5sums = 85a27d09ee9ec6137d5f7c43180c87e0 + md5sums = 31708844142d0b48a3227b113db0cb0f + +pkgname = jpf-core-bin + diff --git a/.gitignore b/.gitignore new file mode 100644 index 000000000000..aa5565735010 --- /dev/null +++ b/.gitignore @@ -0,0 +1,6 @@ +* +!.gitignore +!PKGBUILD +!.SRCINFO +!jpf +!jpf.properties
\ No newline at end of file diff --git a/PKGBUILD b/PKGBUILD new file mode 100644 index 000000000000..4053debab2cd --- /dev/null +++ b/PKGBUILD @@ -0,0 +1,34 @@ +# Maintainer: Baplar <baplar@gmail.com> +# Contributor: Drew Noel <drewmnoel@gmail.com> +pkgname=jpf-core-bin +pkgver=r32 +pkgrel=1 +pkgdesc="An extensible software model checking framework for Java bytecode programs" +arch=('any') +url="https://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-core" +license=('APACHE') +depends=('java-environment-openjdk>=8') +provides=("${pkgname%-bin}") +conflicts=("${pkgname%-bin}") +source=('https://babelfish.arc.nasa.gov/trac/jpf/raw-attachment/wiki/projects/jpf-core/jpf-core-r32.zip' + 'jpf' + 'jpf.properties') +md5sums=('a9a3cff397180a533a93fd434241a225' + '85a27d09ee9ec6137d5f7c43180c87e0' + '31708844142d0b48a3227b113db0cb0f') + +JPF_HOME=/usr/share/java/jpf +BIN_DIR=/usr/local/bin + +package() { + cd $srcdir + + # Copy the mandatory config + install -D -m644 -t $pkgdir/$JPF_HOME/ jpf.properties + + # Copy all the .JAR files + install -D -m644 -t $pkgdir/$JPF_HOME/ jpf-core/build/*.jar + + # Copy the jpf executable + install -D -m755 -t $pkgdir/$BIN_DIR/ jpf +} @@ -0,0 +1,13 @@ +#!/bin/bash +# +# unix shell script to run jpf +# + +JPF_HOME=/usr/share/java/jpf + +if test -z "$JVM_FLAGS"; then + JVM_FLAGS="-Xmx1024m -ea" +fi + +java $JVM_FLAGS -jar "$JPF_HOME/RunJPF.jar" "$@" + diff --git a/jpf.properties b/jpf.properties new file mode 100644 index 000000000000..0cd3e3f3105e --- /dev/null +++ b/jpf.properties @@ -0,0 +1,420 @@ +# JPF configuration for "jpf-core" component + +# path elements can either be relative to the property file location, or +# use the JPF component name (e.g. "jpf-core") as a variable prefix +# (e.g. "jpf-core.sourcepath=${jpf-core}/src/examples"). +# If a jpf.properties is to be used within NB, it has to use the variable prefix +# (prepending the project root is only done during JPF init) + +# we use the ';' separator here because it is recognized by NetBeans (as opposed +# to ',') + +# 'config_path' is set automatically by gov.nasa.jpf.Config during JPF init. +# If used from within an Ant build system, 'jpf-core' has to be set explicitly +# (ant does ${..} property expansion, but ignores property redefinition, so the +# following line will be ignored) + +jpf-core = /usr/share/java/jpf + +jpf-core.native_classpath=\ + ${jpf-core}/jpf.jar;\ + ${jpf-core}/jpf-annotations.jar + +jpf-core.classpath=\ + ${jpf-core}/jpf-classes.jar + +jpf-core.peer_packages = gov.nasa.jpf.vm,<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.vm.NotDeadlockedProperty,\ +gov.nasa.jpf.vm.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.vm.SingleProcessVM + +# the ClassLoaderInfo class used for startup +vm.classloader.class = gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo + +# class used to hash/store states (if not set, states are not matched) +vm.storage.class = gov.nasa.jpf.vm.JenkinsStateSet + +# class used to maintain the backtrack stack +vm.backtracker.class = gov.nasa.jpf.vm.DefaultBacktracker + +# serializer to be used by state set (vm.storage.class) +vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer +#vm.serializer.class = gov.nasa.jpf.vm.serialize.AdaptiveSerializer +#vm.serializer.class = gov.nasa.jpf.vm.serialize.FilteringSerializer + +# the class that models static fields and classes +vm.statics.class = gov.nasa.jpf.vm.OVStatics + +# the class that models the heap +#vm.heap.class = gov.nasa.jpf.vm.PSIMHeap +vm.heap.class = gov.nasa.jpf.vm.OVHeap + +# the class representing the list of all threads +vm.threadlist.class = gov.nasa.jpf.vm.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 = .vm.DefaultMementoRestorer + +# where do we get the standard libraries from? +# "<system>" is replaced by the host VM sun.boot.class.path setting +vm.boot_classpath = <system> + +# instruction factory +jvm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory + +# fields factory +vm.fields_factory.class = gov.nasa.jpf.vm.DefaultFieldsFactory + +# 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 + + +vm.scheduler.class = gov.nasa.jpf.vm.DelegatingScheduler +vm.scheduler.sync.class = gov.nasa.jpf.vm.AllRunnablesSyncPolicy +vm.scheduler.sharedness.class = gov.nasa.jpf.vm.PathSharednessPolicy + +# the following properties can be used to set filters for GenericSharednessPolicy instances + +# never break on exposure or shared field access from matching methods. +# NOTE - this is transitive and hence should only include a minimal set of trusted methods +vm.shared.never_break_methods=\ + java.util.concurrent.ThreadPoolExecutor.processWorkerExit,\ + java.util.concurrent.locks.Abstract*Synchronizer.*,\ + java.util.concurrent.ThreadPoolExecutor.getTask,\ + java.util.concurrent.atomic.Atomic*.*,\ + java.util.concurrent.Exchanger.doExchange,\ + java.util.concurrent.ThreadPoolExecutor.interruptIdleWorkers,\ + java.util.concurrent.TimeUnit.* + +vm.shared.never_break_types=\ + java.util.concurrent.TimeUnit + +# never break on shared access of the following fields. While this is less prone to +# masking defects than never_break_methods, it should also be used sparingly. +# NOTE - java.lang.Thread* fields should not be excluded if the SUT explicitly uses +# Thread or ThreadGroup objects +vm.shared.never_break_fields=\ + java.lang.Thread*.*,\ + java.lang.System.*,\ + java.lang.Runtime.*,\ + java.lang.Boolean.*,\ + java.lang.String.*,\ + java.lang.*.TYPE,\ + java.util.HashMap.EMPTY_TABLE,\ + java.util.HashSet.PRESENT,\ + java.util.concurrent.ThreadPoolExecutor*.*,\ + java.util.concurrent.ThreadPoolExecutor*.*,\ + java.util.concurrent.TimeUnit.*,\ + java.util.concurrent.Exchanger.CANCEL,\ + java.util.concurrent.Exchanger.NULL_ITEM,\ + java.util.concurrent.Executors$DefaultThreadFactory.*,\ + sun.misc.VM.*,\ + sun.misc.SharedSecrets.*,\ + sun.misc.Unsafe.theUnsafe,\ + gov.nasa.jpf.util.test.TestJPF.* + + +# do we also break transitions on reference field puts that could make the +# referenced objects shared +vm.shared.break_on_exposure = true + +# 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.shared.sync_detection = true + +# 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.shared.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.shared.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.shared.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 = 50000 + +# 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.vm.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.vm.SystemTime + +# if this is set to true, we throw an exception if we encounter any orphan native peer methods +vm.no_orphan_methods = false + +# if this is set to true, overriden finalize() methods execute upon objects garbage collections +vm.process_finalizers = false + + +### jvm specifics + +# di=o we model nested locks during class init (to detect possible hotspot dealocks during init) +# (off by default since it can cause state explosion) +jvm.nested_init=false + +# if so, for which classes (default is to exclude system classes) +jvm.nested_init.exclude=java.*,javax.*,sun.misc.* + + +############################### 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 set we break the transition on Thread.yield() +cg.threads.break_yield=true + +# if this option is set we break the transition on Thread.sleep() +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.probe=statistics + +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 |