Gymbo

Public Member Functions | Public Attributes | List of all members
gymbo::SExecutor Struct Reference

Represents a derived class for symbolic execution engine for deterministic programs. More...

`#include <symbolic.h>`

Inheritance diagram for gymbo::SExecutor:
[legend]
Collaboration diagram for gymbo::SExecutor:
[legend]

## Public Member Functions
bool | solve (bool is_target, int pc, SymState &state)
| Solves path constraints and updates the cache. More...
Trace | run (Prog &prog, std::unordered_set< int > &target_pcs, SymState &state, int maxDepth=256)
| Symbolically Execute a Program with Gradient Descent Optimization. More...
| BaseExecutor (GDOptimizer optimizer, int maxSAT=256, int maxUNSAT=256, int max_num_trials=10, bool ignore_memory=false, bool use_dpll=false, int verbose_level=0, bool return_trace=false)
| Constructor for BaseExecutor. More...
Public Member Functions inherited from gymbo::BaseExecutor
| BaseExecutor (GDOptimizer optimizer, int maxSAT=256, int maxUNSAT=256, int max_num_trials=10, bool ignore_memory=false, bool use_dpll=false, int verbose_level=0, bool return_trace=false)
| Constructor for BaseExecutor. More...

## Public Attributes
PathConstraintsTable | constraints_cache
| Cache for storing and reusing path constraints. More...
Public Attributes inherited from gymbo::BaseExecutor
GDOptimizer | optimizer
int | maxSAT
| The maximum number of SAT constraints to collect. More...
int | maxUNSAT
| The maximum number of UNSAT constraints to collect. More...
int | max_num_trials
int | verbose_level
| The level of verbosity. More...
bool | ignore_memory
bool | use_dpll
bool | return_trace

## Detailed Description

Represents a derived class for symbolic execution engine for deterministic programs.

## Member Function Documentation

## ◆ BaseExecutor()

gymbo::BaseExecutor::BaseExecutor
| inline

Constructor for BaseExecutor.

Parameters

  optimizer | The gradient descent optimizer for parameter optimization.
  maxSAT | The maximum number of SAT constraints to collect.
  maxUNSAT | The maximum number of UNSAT constraints to collect.
  max_num_trials | The maximum number of trials for each gradient descent.
  ignore_memory | If set to true, constraints derived from memory will be ignored.
  use_dpll | If set to true, use DPLL to decide the initial assignment for each term.
  verbose_level | The level of verbosity.
  return_trace | If set to true, save the trace at each pc and return them (default false).

## ◆ run()

Trace gymbo::SExecutor::run | ( | Prog & | prog,
|  | std::unordered_set< int > & | target_pcs,
|  | SymState & | state,
|  | int | maxDepth = `256`
| ) |  |
| inlinevirtual

Symbolically Execute a Program with Gradient Descent Optimization.

This function conducts symbolic execution of a given program while simultaneously optimizing the path constraints using the provided gradient descent optimizer, `GDOptimizer`.

Parameters

  prog | The program to symbolically execute.
  target_pcs | The set of pc where gymbo executes path-constraints solving. If this set is empty or contains -1, gymbo solves all path-constraints.
  state | The initial symbolic state of the program.
  maxDepth | The maximum depth of symbolic exploration.

Returns
  A trace of the symbolic execution.

Implements gymbo::BaseExecutor.

## ◆ solve()

bool gymbo::SExecutor::solve | ( | bool | is_target,
|  | int | pc,
|  | SymState & | state
| ) |  |
| inlinevirtual

Solves path constraints and updates the cache.

This function solves path constraints, updates the cache, and prints verbose information if conditions are met.

Parameters

  is_target | Flag indicating whether the program counter is a target.
  pc | The program counter.
  state | Reference to the symbolic state.

Returns
  The flag indicating satisfifiability.

Implements gymbo::BaseExecutor.

## Member Data Documentation

## ◆ constraints_cache

PathConstraintsTable gymbo::SExecutor::constraints_cache

Cache for storing and reusing path constraints.

The documentation for this struct was generated from the following file:

- libgymbo/symbolic.h