Configuration
- class tritondse.Config(seed_format: ~tritondse.seed.SeedFormat = SeedFormat.RAW, pipe_stdout: bool = False, pipe_stderr: bool = False, skip_sleep_routine: bool = False, smt_solver: ~tritondse.types.SmtSolver = SmtSolver.Z3, smt_timeout: int = 5000, execution_timeout: int = 0, exploration_timeout: int = 0, exploration_limit: int = 0, thread_scheduling: int = 200, smt_queries_limit: int = 1200, smt_enumeration_limit: int = 40, coverage_strategy: ~tritondse.coverage.CoverageStrategy = CoverageStrategy.BLOCK, branch_solving_strategy: ~tritondse.coverage.BranchSolvingStrategy = <BranchSolvingStrategy.FIRST_LAST_NOT_COVERED: 2>, workspace: str = '', workspace_reset=False, program_argv: ~typing.List[str] = None, time_inc_coefficient: float = 1e-05, skip_unsupported_import: bool = False, skip_unsupported_instruction: bool = False, memory_segmentation: bool = True)[source]
Data class holding tritondse configuration parameter
- branch_solving_strategy: BranchSolvingStrategy
Branch solving strategy to apply for a single execution. For a given non-covered branch allows changing whether we try to solve it at all occurrences or more seldomly. default:
BranchSolvingStrategy.FIRST_LAST_NOT_COVERED
- coverage_strategy: CoverageStrategy
Coverage strategy to apply for the whole exploration, default:
CoverageStrategy.BLOCK
- custom
Custom carrier field enabling user to add parameters of their own.
- execution_timeout: int
Timeout of a single execution. If it is triggered the associated input file is marked as ‘hanging’. In seconds, 0 means unlimited (default: 0)
- exploration_timeout: int
Overall timeout of the exploration in seconds. 0 means unlimited (default: 0)
- static from_file(file: str) Config[source]
Load a configuration from a file to a new instance of Config
- Parameters:
file – The path name
- Returns:
A fresh instance of Config
- static from_json(s: str) Config[source]
Load a configuration from a json input to a new instance of Config
- Parameters:
s – The JSON text
- Returns:
A fresh instance of Config
- memory_segmentation: bool
This option defines whether or not memory segmentation is enforced. If activated all memory accesses must belong to a mapped memory area.
- seed_format: SeedFormat
Seed type is either Raw (raw bytes) or Composite (more expressive). See seeds.py for more information on each format.
- skip_unsupported_import: bool
Whether or not to stop the emulation when hitting a external call to a function that is not supported.
- skip_unsupported_instruction: bool
Whether or not to stop the emulation when hitting an instruction for which the semantic is not defined.
- smt_enumeration_limit: int
Limit of model values retrieved when enumerating a dynamic jump or symbolic memory accesses
- thread_scheduling: int
Number of instructions to execute before switching to the next thread. At the moment all threads are scheduled in a round-robin manner (default: 200)
- time_inc_coefficient: float
Time increment coefficient at each instruction to provide a deterministic behavior when calling time functions (e.g gettimeofday(), clock_gettime(), …). For example, if 0.0001 is defined, each instruction will increment the time representation of the execution by 100us. (default: 0.00001)