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

#include <symbolic.h>

Inheritance diagram for gymbo::SExecutor:

Collaboration diagram for gymbo::SExecutor:

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

Public Member Functions

Public Attributes

Detailed Description

Member Function Documentation

◆ BaseExecutor()

◆ run()

◆ solve()

Member Data Documentation

◆ constraints_cache