Dsc is a dynamic symbolic execution engine and test case generator for Java (bytecode) programs. This page describes Dsc's configuration options.
Options may change or disappear in subsequent Dsc releases.
Following is an example setup that works on my machine.
Now we do the following:
c:\java\dsc contains the contents of the Dsc binary distribution zip file, i.e.:
dsc.jar contains the main Dsc Java classes plus third-party Java libraries
instrument.jar contains the Dsc JvmAgent instrumentation agent class and the Asm library
z3.dll is the Z3 Windows x86 library
Z3Wrap.dll is the SWIG-generated Z3 wrapper library
conf_basic.txt is an example Dsc configuration file
c:\java\proj\bin\please contains a class file we want Dsc to analyze.
is an example
public class file that contains a public static method named
me. This class file has been compiled from source file
. There are five distinct execution paths through the
method, if we take into account int overflow and implicit branches triggered by Jvm instructions throwing runtime exceptions.
Pop quiz: Write down five test cases that cover the five execution paths through the method :)
Dsc should now be executing the Cover.me method several times and cover all execution paths through this particular method. (In general, Dsc obviously cannot cover all paths through any given method.) During execution, Dsc emits some
java -cp dsc.jar;c:\java\proj\bin -javaagent:instrument.jar edu.uta.cse.dsc.Dsc please.Cover me
logging information and writes each new execution path as a JUnit test case to disk. We now should have the following directory.
c:\java\dsc\generated\please contains the generated JUnit test classes, i.e.:
Roops is an attempt at providing a common benchmark for program analysis tools such as Pex and Dsc. Currently, Dsc supports only very basic Roops features.
RoopsDsc explores each public static method that is annotated with the
roops.util.BenchmarkMethod annotation, if that method is contained in a public class annotated with the roops.util.BenchmarkClass annotation. Such a benchmark method may contain goal statements, in the form of calls of the roops.util.Goals.reached(int) method.
The Roops infrastructure counts the goals that are reached during a RoopsDsc exploration and RoopsDsc reports those goals to the user.
Dsc and RoopsDsc have several configuration options. These can be set via a configuration text file (property file), for which Dsc and RoopsDsc currently search on the class path. An example configuration file is conf_basic.txt. In the above example, we can use the configuration file as follows.
The following lists the current configuration options that can be used in such a configuration file. Each option is given in the following format.
java -cp .;dsc.jar;c:\java\proj\bin -javaagent:instrument.jar edu.uta.cse.dsc.Dsc conf_basic.txt
RoopsDsc has slightly different default options. They can be printed via:
NAME = default value in Dsc Description.
Similarly, the following Dsc default options can be printed via:
java -cp c:\java\dsc\dsc.jar edu.uta.cse.dsc.RoopsDsc --help
java -cp c:\java\dsc\dsc.jar edu.uta.cse.dsc.Dsc --help
Z3_WRAP_PATH = /java/dsc/ Full directory of Z3Wrap.dll. Set this option if Dsc cannot locate Z3Wrap.dll
BASIC_DSC_CLASS_CP = please.Cover Basic Dsc explores method BASIC_DSC_CLASS_CP_METHOD in this class from the class path. Ignored by RoopsDsc.
BASIC_DSC_CLASS_CP_METHOD = me Basic Dsc explores this method in BASIC_DSC_CLASS_CP. Ignored by RoopsDsc.
ROOPS_DSC_CLASSES_CP = RoopsDsc explores these Roops classes from the class path (independently of ROOPS_DSC_DIRS). Ignored by basic Dsc.
ROOPS_DSC_DIRS = RoopsDsc explores all Roops classes in ROOPS_DSC_DIRS that match a pattern in the ROOPS_DSC_DIRS_PACKAGES property (independently of ROOPS_DSC_CLASSES). Ignored by basic Dsc.
ROOPS_DSC_DIRS_PACKAGES = Patterns of package prefixes RoopsDsc uses for ROOPS_DSC_DIRS. E.g.,: 'a.' or 'a.b.' etc. Ignored by basic Dsc.
DO_NOT_INSTRUMENT_PREFIXES = java., javax., sun., com.sun., $, org.eclipse., gnu.trove., org.junit., junit., spoon., edu.uta.cse.dsc., edu.uta.cse.dbtest., edu.uta.cse.tada., edu.uta.cse.z3., org.objectweb.asm., roops.util., org.apache.derby., tada.sqlparser., Zql., org.jcp., org.postgresql., edu.umass.cs., woda2010., ecoop2010., com.accenture.lab.crest.vm., com.mysql. Do not instrument any of the classes that have any of these prefixes. IMPORTANT: InstrumentConfig maintains the same list. Both lists have to be updated for Dsc to work properly! TODO: Merge these two lists.
DO_INSTRUMENT_PREFIXES = com.sun.javadoc., roops.util.RoopsArray Prefixes of classes that will always be explored symbolically, regardless if they appear in DO_NOT_INSTRUMENT_PREFIXES. IMPORTANT: InstrumentConfig maintains the same list. Both lists have to be updated for Dsc to work properly! TODO: Merge these two lists.
DO_NOT_PLACE_MOCKCLASS_IN_PACKAGE_PREFIXES = java., javax.
OUT_DIR_SRC = generated Dsc writes Java source code into this directory, i.e., JUnit test cases.
OUT_DIR_BIN = generated-bin Dsc writes Java bytecode into this directory, i.e., mock classes.
JUNIT_TEST_CLASS_COMMENT = JavaDoc comment for each generated class
JUNIT_TEST_TAB_SIZE = 2 Tab size used in the generated JUnit test files
JUNIT_AFTER_CLASS_METHOD = false Add an @AfterClass method to each generated test class
JUNIT_AFTER_CLASS_ANNOTATION = org.junit.AfterClass @AfterClass annotation
JUNIT_TEST_CASE_ANNOTATED_TEST = true Annotate each generated test case method as a test, e.g., with @Test
JUNIT_TEST_CASE_ANNOTATION_TEST = org.junit.Test Annotation of a test case, e.g., @Test
JUNIT_TEST_CASE_ANNOTATED_GENERATED = false Annotate each generated test case method as generated, e.g., with @Generated
JUNIT_TEST_CASE_ANNOTATION_GENERATED_GENERATOR = edu.uta.cse.dsc Mandatory parameter of the @Generated annotation
JUNIT_LOCAL_VARIABLE_PREFIX = local Prefix of each local variable in generated JUnit test case
MOCK_CLASS_METHOD_RETURN_VAR_POSTFIX = #MCRV Postfix for mock class method return value variable names
MOCK_CLASS_NAME_PREFIX = MockClass Prefix of generated mock class names
MOCK_CLASS_MAY_EXTEND_MOCK_CLASS = false Allow a mock class to extend another mock class
MOCK_NR_MOCK_CLASSES_MIN = 0 Minimum number of mock classes. Only relevant in MOCK_MODE.
MOCK_NR_MOCK_CLASSES_MAX = 2 Maximum number of mock classes. Only relevant in MOCK_MODE.
MOCK_NR_MOCK_CLASSES_STEP = 1 Delta for subsequent nr of mock classes. Only relevant in MOCK_MODE.
MOCK_MINIMIZE_NR_MOCK_CLASSES_USED = false After finding a solution with mock classes, try find another one using fewer mock classes.
MOCK_NR_MOCK_CLASSES_AT_MOST_NR_REF_PARAMS = true Number of mock classes cannot be larger than the number of reference parameters of the explored method.
MOCK_FALLBACK_PACKAGE_NAME_FOR_MOCK_CLASSES = mock Package name used for mock classes in case we cannot infer one.
ENCODE_HARD_TO_SUBCLASS_AS_FINAL = true Encode hard-to-subclass classes as final
MODE = DSC Dsc mode. Also see REPAIR_MODE and MOCK_MODE
REPAIR_MODE = false Data-structure repair mode. Also see MODE. Maintained by Ishtiaque.
DUMPER_MODE = false Only monitor execution and dump each symbolic expression immediately to disk.
REQ_1_MODE = false REQ-1 mode.
REPAIR_ATTEMPTED = false Simulate multiple repair by Dsc
REPAIR_LOG_REFLECTION = true Log debug information during repair reflection
REPAIR_LOG_CONSTRAINTS = true Log constraints collected during repair
REPAIR_NO_OF_NODES = 10 Repair: Number of nodes in a binary tree
CREST_MODE = false CREST: Combinatorial testing with Dsc. Maintained by Ishtiaque.
CARFAST_MAX_ITERATION = 10 CarFast: Maximum iteration for CarFast
DUMP_FILE_NAME = cond.txt File to which Dsc dumps its output in dumper mode.
MOCK_MODE = false Mock class generation. Also see MODE. Maintained by Mainul.
USE_MAX = false Guard for any bounds-checking for the following exploration bounds.
MAX_CALLBACKS_METHOD = 100000 USE_MAX ==> max #callbacks Dsc will process for one exploration (set of execution paths through a single user entry method)
MAX_CALLBACKS_PATH = 20000 USE_MAX ==> max #callbacks Dsc will process for a single execution path through user code
MAX_SAT_CALLS_METHOD = 20 USE_MAX ==> Maximum number of SAT calls Dsc will issue for any given exploration (= entry method)
MAX_ARRAY_SIZE_CREATION = 10000 Array creations with more elements will trigger to discard this path and search for a cheaper one.This is a coarse model of OutOfMemoryError triggered by JVM.
SIMPLIFY_SELECT_EXPRESSIONS = true Rewrite select expressions
SUPPRESS_TRIVIAL_UNSAT_QUERIES = true Do not ask SAT solver queries that are trivially UNSAT.Our own light-weight SAT checker.
ARRAY_LENGTH_MAX = 128 Maximum sum of array variable lengths to try
ARRAY_LENGTH_MINIMIZE = true Try to minimize sum of array lengths in generated test cases
ARRAY_LENGTH_MINIMIZE_FACTOR = 4 Factor for subsequent array length
MAX_LOCALS_DEFAULT = 200 Artificial maximum number of local variables in a method/constructor
CONTEXT_HEIGHT_BASE_OF_ALL_EXPLORATIONS = 0 Base context shared by all explorations. At this level, Dsc persists, for example, types.
CONTEXT_HEIGHT_BASE_OF_SINGLE_METHOD_EXPLORATION = 1 Base context of a single method exploration. At this level, Dsc persists, for example, variables representing method parameters.
TYPE_CONSTRAINTS = true include reference type constraints in generated constraint systems
TYPE_MAPPED_TO_SUBTYPES = false map each type to its subtypes, instead of to its super types
LOG_DIR_NAME = log Directory to which Dsc writes its log files.
LOG_ALL_CONSTRAINTS = false log all constraints (branch conditions, type encoding, etc.) issued to Z3 to standard out.
LOG_ALL_CONSTRAINTS_TO_FILE = false log all constraints to file, write files to LOG_DIR_NAME.
LOG_SECTION_PREFIX = -------------------- log separator for standard out.
LOG_BRANCH_CONDITIONS = false log branch conditions issued to Z3 to standard out.
LOG_TYPE_IDENTIFIERS = false log each id Dsc assigns to each type to standard out.
LOG_TYPE_PROPERTIES = false log type properties (super-types, abstract/public/etc.) to standard out.
LOG_TYPE_OF_VALUES = false log type of variables etc. to standard out.
LOG_AST_COUNTS = true log number of Dsc Ast nodes created
LOG_AST_Z3 = false log Z3 Ast creation
LOG_BRANCH_FILE_NAME = C:\BranchOutput.txt log branch id
LOG_BACKGROUND_AXIOM_INSTANCES_ARRAYS = false Log every concrete (asserted) instance of a (universally quantified) background axiom that pertains to arrays.
LOG_BYTECODE = false log each executed bytecode instruction
LOG_CLINIT = false log each user class initialization
LOG_EXCEPTIONS = false log stack trace of any exceptions during execution
LOG_EXEC_RESULTS = false log path condition and result of each execution
LOG_EXPLORATION = false log Dsc exploration: push/pop.
LOG_INPUT = false log input values (variable assignments) used for each execution
LOG_MALLOC_PERSIST_DISCARD = false log Dsc exploration: malloc/persist/assert. -- broken.
LOG_MODEL_COUNTS = true log number of times we ask Z3 to check SAT of a constraint system, how many of those Z3 found a model for, and how many of those lead to a new execution path.
LOG_MODEL_DSC = false log each solution in Dsc notation
LOG_MODEL_Z3 = false log each solution in the Z3 notation
LOG_NULL_CHECKS = false log path condition on null check
LOG_PATH_COND_DSC_NOT_NULL = true log (not (x==null)) conjuncts when logging the path condition in Dsc notation
LOG_ROOPS_FILE_NAME = c:\DscOutput.txt File name for Roops output [Mainul]
LOG_ROOPS_TO_FILE = false log Roops output to file
LOG_SUMMARY = true log summary of the entire exploration
LOG_SUMMARY_INSTANCE_FIELDS = false log instance fields with summary.
LOG_Z3_TIMES = false log Z3 execution times
LOG_Z3_TRACE_FILE_NAME = log\z3-1319905598739.out Filename for Z3 log, write file to LOG_DIR_NAME
LOG_Z3_TRACE_TO_FILE = false Make Z3 log into a text file
LOG_Z3_TRACE_TO_STD_ERR = false Log Z3 trace messages to standard error
Z3PARAM_SOFT_TIMEOUT = 5000 Approximate timeout for each solver query (milliseconds), 0 = no timeout.
Z3PARAM_MODEL = true Model construction.