Gymbo

Classes | Namespaces | Functions
symbolic.h File Reference

Core implementation of gradient-based symbolic execution. More...

`#include "smt.h"`
Include dependency graph for symbolic.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

## Classes
struct | gymbo::BaseExecutor
| Represents the base class for symbolic execution engine. More...
struct | gymbo::SExecutor
| Represents a derived class for symbolic execution engine for deterministic programs. More...

## Namespaces
| gymbo

## Functions
bool | gymbo::is_target_pc (const std::unordered_set< int > &target_pcs, int pc)
| Checks if the given program counter (pc) is a target program counter. More...
bool | gymbo::explore_further (int maxDepth, int maxSAT, int maxUNSAT)
| Checks if further exploration is allowed based on maximum depth and satisfiability conditions. More...
void | gymbo::call_smt_solver (bool &is_sat, SymState &state, std::unordered_map< int, float > &params, GDOptimizer &optimizer, int max_num_trials, bool ignore_memory, bool use_dpll)
| Calls the SMT solver based on the specified options. More...
void | gymbo::verbose_constraints (int verbose_level, bool is_unknown_path_constraint, bool is_target, bool is_sat, int pc, std::string constraints_str, const SymState &state, const std::unordered_map< int, float > &params)
| Prints a verbose for conflicts solving if conditions are met. More...
void | gymbo::verbose_pre (int verbose_level, int pc, Prog &prog, SymState &state)
| Prints a verbose representation before solving constraints. More...
void | gymbo::verbose_post (int verbose_level)
| Prints a verbose representation after solving constraints. More...
void | gymbo::symStep (SymState *state, Instr &instr, std::vector< SymState * > &result)
| Symbolically Execute a Single Instruction of a Program. More...

## Detailed Description

Core implementation of gradient-based symbolic execution.

Author
  Hideaki Takahashi