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:

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...

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.

Classes