summarylogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--.SRCINFO19
-rw-r--r--.gitignore6
-rw-r--r--PKGBUILD34
-rw-r--r--jpf13
-rw-r--r--jpf.properties420
5 files changed, 492 insertions, 0 deletions
diff --git a/.SRCINFO b/.SRCINFO
new file mode 100644
index 00000000000..b3d23dad758
--- /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 00000000000..aa556573501
--- /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 00000000000..4053debab2c
--- /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
+}
diff --git a/jpf b/jpf
new file mode 100644
index 00000000000..d4375aba205
--- /dev/null
+++ b/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 00000000000..0cd3e3f3105
--- /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