Dsc: Configuration

Dsc is a dynamic symbolic execution engine and test case generator for Java (bytecode) programs. This page describes Dsc's configuration options.

Warning

Options may change or disappear in subsequent Dsc releases.

Setup

Following is an example setup that works on my machine. Now we do the following: 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 logging information and writes each new execution path as a JUnit test case to disk. We now should have the following directory.

Roops Integration

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.

Configuration Options

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.
NAME = default value in Dsc
Description.
RoopsDsc has slightly different default options. They can be printed via: Similarly, the following Dsc default options can be printed via:
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.