Classes
struct	GDOptimizer
	Gradient Descent Optimizer for Symbolic Path Constraints. More...

struct	Node
	Structure representing a node in the Abstract Syntax Tree (AST). More...

struct	PSExecutor
	Represents a derived class for symbolic execution engine for probabilistic programs. More...

struct	BaseExecutor
	Represents the base class for symbolic execution engine. More...

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

struct	Token
	Structure representing a token. More...

class	Instr
	Class representing an instruction. More...

struct	Grad
	Struct representing the gradient of a symbolic expression. More...

struct	Sym
	Struct representing a symbolic expression. More...

struct	DiscreteDist
	Represents a discrete probability distribution. More...

struct	DiscreteUniformDist
	Represents a discrete uniform distribution derived from DiscreteDist. More...

struct	BernoulliDist
	Represents a bernoulli distribution derived from DiscreteDist. More...

struct	BinomialDist
	Represents a binomial distribution derived from DiscreteDist. More...

struct	SymProb
	Represents a symbolic probability with a numerator and denominator. More...

struct	SymState
	Struct representing the symbolic state of the symbolic execution. More...

struct	Trace
	Struct representing a trace in symbolic execution. More...

class	LLNode
	Node for a Doubly Linked List. More...

class	Linkedlist
	Doubly Linked List Implementation. More...

Typedefs
using	Word32 = uint32_t
	Alias for 32-bit unsigned integer. More...

using	Prog = std::vector< Instr >
	Alias for a program, represented as a vector of instructions. More...

using	Mem = std::unordered_map< Word32, Word32 >
	Alias for memory, represented as an unordered map of 32-bit words. More...

using	SMem = std::unordered_map< Word32, Sym >
	Alias for symbolic memory, represented as an unordered map of symbolic expressions. More...

using	PathConstraintsTable = std::unordered_map< std::string, std::pair< bool, std::unordered_map< int, float > >>
	Alias for a table of path constraints. More...

using	ProbPathConstraintsTable = std::unordered_map< int, std::vector< std::tuple< Sym, Mem, SymProb > >>
	Alias for a table of probabilistic path constraints. More...

Enumerations
enum	NodeKind { ND_ADD , ND_SUB , ND_MUL , ND_DIV , ND_AND , ND_OR , ND_NOT , ND_EQ , ND_NE , ND_LT , ND_LE , ND_ASSIGN , ND_LVAR , ND_NUM , ND_RETURN , ND_IF , ND_FOR , ND_BLOCK }
	Enumeration representing different node kinds in the Abstract Syntax Tree (AST). More...

enum	TokenKind { TOKEN_RESERVED , TOKEN_RETURN , TOKEN_IF , TOKEN_ELSE , TOKEN_FOR , TOKEN_IDENT , TOKEN_NUM , TOKEN_EOF }
	Enumeration representing different token kinds. More...

enum class	InstrType { Add , Sub , Mul , JmpIf , Jmp , And , Or , Not , Lt , Le , Eq , Push , Store , Load , Pop , Read , Print , Swap , Dup , Over , RotL , Done , Nop }
	Enum representing different instruction types. More...

enum class	SymType { SAdd , SSub , SMul , SEq , SNot , SOr , SCon , SCnt , SAnd , SLt , SLe , SAny }
	Enum representing different symbolic expression types. More...

Functions
void	gen_lval (Node *node, Prog &prg)
	Generates virtual instructions for a given AST node, representing the left-hand side of a variable assignment expression. More...

void	gen (Node *node, Prog &prg)
	Generates virtual instructions for a given AST node. More...

void	compile_ast (std::vector< Node * > code, Prog &prg)
	Compile the Abstract Syntax Tree (AST) into a sequence of instructions. More...

Node *	assign (Token &token, char user_input)
	Parses an assignment statement from a C-like language program. More...

Node *	expr (Token &token, char user_input)
	Parses an expression from a C-like language program. More...

Node *	equality (Token &token, char user_input)
	Parses an equality expression from a C-like language program. More...

Node *	relational (Token &token, char user_input)
	Parses a relational expression from a C-like language program. More...

Node *	logical (Token &token, char user_input)
	Parses a logical expression from a C-like language program. More...

Node *	add (Token &token, char user_input)
	Parse and construct an AST node representing addition or subtraction. More...

Node *	mul (Token &token, char user_input)
	Parse and construct an AST node representing multiplication or division. More...

Node *	unary (Token &token, char user_input)
	Parse and construct an AST node representing unary operations. More...

Node *	primary (Token &token, char user_input)
	Parse and construct an AST node representing primary expressions. More...

Node *	stmt (Token &token, char user_input)
	Parse and construct an AST node representing a statement. More...

Node *	new_node (NodeKind kind)
	Create a new AST node with the given kind. More...

Node *	new_binary (NodeKind kind, Node lhs, Node rhs)
	Create a new binary AST node with the given kind, left-hand side, and right-hand side. More...

Node *	new_num (float val)
	Create a new AST node representing a numeric value with the given value. More...

void	generate_ast (Token &token, char user_input, std::vector< Node * > &code)
	Parses a C-like language program into an AST. More...

std::pair< std::unordered_map< std::string, int >, Prog >	gcompile (char *user_input)
	Compiles user input into a program, returning variable counts and the compiled program. More...

void	pbranch (SymState &state)
	Perform probabilistic branching based on symbolic execution. More...

void	verbose_pconstraints (int verbose_level, bool is_unknown_path_constraint, bool is_target, bool is_sat, int pc, std::string constraints_str, SymState &state, const std::unordered_map< int, float > &params)
	Prints verbose information about probabilistic path constraints. More...

void	update_prob_constraints_table (int pc, SymState &state, ProbPathConstraintsTable &prob_constraints_table)
	Updates the table of probabilistic path constraints. More...

void	initialize_params (std::unordered_map< int, float > &params, SymState &state, bool ignore_memory)
	Initialize Parameter Values from Memory. More...

void	smt_union_solver (bool &is_sat, SymState &state, std::unordered_map< int, float > &params, GDOptimizer &optimizer, int max_num_trials, bool ignore_memory)
	SMT Solver with Unified Loss Function. More...

void	smt_dpll_solver (bool &is_sat, SymState &state, std::unordered_map< int, float > &params, GDOptimizer &optimizer, int max_num_trials, bool ignore_memory)
	SMT Solver using DPLL as its backend. More...

bool	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	explore_further (int maxDepth, int maxSAT, int maxUNSAT)
	Checks if further exploration is allowed based on maximum depth and satisfiability conditions. More...

void	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	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	verbose_pre (int verbose_level, int pc, Prog &prog, SymState &state)
	Prints a verbose representation before solving constraints. More...

void	verbose_post (int verbose_level)
	Prints a verbose representation after solving constraints. More...

void	symStep (SymState state, Instr &instr, std::vector< SymState > &result)
	Symbolically Execute a Single Instruction of a Program. More...

bool	is_alpha (char c)
	Checks if a character is an alphabetical character or underscore. More...

bool	is_alnum (char c)
	Checks if a character is an alphanumeric character. More...

void	error (char *fmt,...)
	Reports an error and exits the program. More...

void	error_at (char user_input, char loc, char *fmt,...)
	Reports an error location and exits the program. More...

bool	consume (Token &token, char op)
	Consumes the current token if it matches `op`. More...

bool	consume_tok (Token *&token, TokenKind tok)
	Consumes the current token if it matches `tok`. More...

Token *	consume_ident (Token *&token)
	Consumes the current token if it is an identifier. More...

void	expect (Token &token, char user_input, char *op)
	Ensures that the current token matches `op`. More...

float	expect_number (Token &token, char user_input)
	Ensures that the current token is a number. More...

bool	at_eof (Token *token)
	Checks if the current token is at the end of the program. More...

Token *	new_token (TokenKind kind, Token cur, char str, int len)
	Creates a new token and adds it as the next token of `cur`. More...

bool	startswith (char p, char q)
	Checks if the string `p` starts with the string `q`. More...

Token *	tokenize (char *user_input, std::unordered_map< std::string, int > &var_counter)
	Tokenizes a given string and returns a linked list of tokens. More...

bool	is_integer (float x)
	Checks if a float is an integer. More...

uint32_t	FloatToWord (float val)
	Converts a float value to a 32-bit word representation. More...

float	wordToFloat (uint32_t word)
	Converts a 32-bit word representation to a float value. More...

int	wordToInt (uint32_t word)
	Converts a 32-bit word representation to an integer value. More...

int	wordToSignedInt (uint32_t word)
	Converts a uint32_t word to a signed int. More...

bool	wordToBool (uint32_t word)
	Converts a uint32_t word to a bool. More...

uint32_t	boolToWord (bool value)
	Converts a bool to a uint32_t word. More...

uint32_t	twosComplement (uint32_t i)
	Returns the twos complement of a uint32_t word. More...

bool	isNegative (uint32_t word)
	Checks if a uint32_t word is negative. More...

std::string	valName (int i)
	Generates a name for a variable based on its index. More...

std::vector< std::vector< int > >	cartesianProduct (const std::vector< std::vector< int >> &vectors)
	Compute the Cartesian product of a vector of vectors of integers. More...

Typedef Documentation

◆ Mem

using gymbo::Mem = typedef std::unordered_map<Word32, Word32>

Alias for memory, represented as an unordered map of 32-bit words.

◆ PathConstraintsTable

using gymbo::PathConstraintsTable = typedef std::unordered_map<std::string, std::pair<bool, std::unordered_map<int, float> >>

Alias for a table of path constraints.

This table uses the string representation of the constraint as the key. The corresponding value is a pair consisting of:

The satisfiability of the constraint.
A map where the key is the variable ID, and the value is the concrete value that makes the constraint true.

The overall structure of the table is as follows: {str_of_constraints: {is_sat: {var_id: var_val}}}

◆ ProbPathConstraintsTable

using gymbo::ProbPathConstraintsTable = typedef std::unordered_map<int, std::vector<std::tuple<Sym, Mem, SymProb> >>

Alias for a table of probabilistic path constraints.

This table uses the program counter as the key, and the corresponding values are vectors of tuples. Each tuple contains three elements:

The first element is the path constraint.
The second element is the concrete memory.
The third element is the probability of reachability under satisfying universal variables.

The overall structure of the table is as follows: {pc: {(constraints, memory, probability)}}

◆ Prog

using gymbo::Prog = typedef std::vector<Instr>

Alias for a program, represented as a vector of instructions.

◆ SMem

using gymbo::SMem = typedef std::unordered_map<Word32, Sym>

Alias for symbolic memory, represented as an unordered map of symbolic expressions.

◆ Word32

using gymbo::Word32 = typedef uint32_t

Alias for 32-bit unsigned integer.

Enumeration Type Documentation

◆ InstrType

enum gymbo::InstrType

strong

Enum representing different instruction types.

Enumerator
Add
Sub
Mul
JmpIf
Jmp
And
Or
Not
Lt
Le
Eq
Push
Store
Load
Pop
Read
Print
Swap
Dup
Over
RotL
Done
Nop

◆ NodeKind

enum gymbo::NodeKind

Enumeration representing different node kinds in the Abstract Syntax Tree (AST).

Enumerator
ND_ADD
ND_SUB
ND_MUL
ND_DIV
ND_AND
ND_OR
ND_NOT
ND_EQ
ND_NE
ND_LT
ND_LE
ND_ASSIGN
ND_LVAR
ND_NUM
ND_RETURN
ND_IF
ND_FOR
ND_BLOCK

◆ SymType

enum gymbo::SymType

strong

Enum representing different symbolic expression types.

Enumerator
SAdd
SSub
SMul
SEq
SNot
SOr
SCon
SCnt
SAnd
SLt
SLe
SAny

◆ TokenKind

enum gymbo::TokenKind

Enumeration representing different token kinds.

Enumerator
TOKEN_RESERVED	Keywords or punctuators.
TOKEN_RETURN	Token representing the 'return' keyword.
TOKEN_IF	Token representing the 'if' keyword.
TOKEN_ELSE	Token representing the 'else' keyword.
TOKEN_FOR	Token representing the 'for' keyword.
TOKEN_IDENT	Token representing an identifier.
TOKEN_NUM	Token representing integer literals.
TOKEN_EOF	Token representing end-of-file markers.

Function Documentation

◆ add()

Node * gymbo::add	(	Token *&	token,
		char *	user_input
	)

inline

Parse and construct an AST node representing addition or subtraction.

add = mul ("+" mul | "-" mul)*

Parameters

token	A reference to the current token.
user_input	The user input string.

Returns: A pointer to the constructed AST node.

◆ assign()

Node * gymbo::assign	(	Token *&	token,
		char *	user_input
	)

Parses an assignment statement from a C-like language program.

assign = logical ("=" assign)?

Parameters

token	The first token in the assignment statement.
user_input	The source code of the program.

Returns: An AST node representing the assignment statement.

◆ at_eof()

bool gymbo::at_eof ( Token * token )

inline

Checks if the current token is at the end of the program.

Parameters

token A pointer to the current token.

Returns: True if the current token is at the end of the program, false otherwise.

◆ boolToWord()

uint32_t gymbo::boolToWord ( bool value )

inline

Converts a bool to a uint32_t word.

Parameters

value The bool to convert.

Returns: The uint32_t word equivalent of the bool.

◆ call_smt_solver()

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
	)

inline

Calls the SMT solver based on the specified options.

This function calls the SMT solver, either DPLL solver or union solver, based on the specified options.

Parameters

is_sat	Reference to a boolean indicating satisfiability.
state	Reference to the symbolic state.
params	Reference to a map containing parameters.
optimizer	Reference to the optimizer.
max_num_trials	Maximum number of solver trials.
ignore_memory	Flag indicating whether to ignore memory.
use_dpll	Flag indicating whether to use the DPLL solver.

◆ cartesianProduct()

std::vector<std::vector<int> > gymbo::cartesianProduct ( const std::vector< std::vector< int >> & vectors )

inline

Compute the Cartesian product of a vector of vectors of integers.

This function takes a vector of vectors of integers and computes their Cartesian product. The result is a vector of vectors, where each inner vector represents a combination of elements from the input vectors.

Parameters

vectors A vector of vectors of integers for which the Cartesian product is computed.

Returns: The Cartesian product as a vector of vectors of integers.

◆ compile_ast()

void gymbo::compile_ast	(	std::vector< Node * >	code,
		Prog &	prg
	)

inline

Compile the Abstract Syntax Tree (AST) into a sequence of instructions.

This function traverses the provided AST and generates corresponding instructions to be executed in the virtual stack machine.

Parameters

code	A vector containing pointers to AST nodes.
prg	A reference to the program (sequence of instructions) being generated.

◆ consume()

bool gymbo::consume	(	Token *&	token,
		char *	op
	)

inline

Consumes the current token if it matches op.

Parameters

token	A pointer to the current token.
op	The token to consume.

Returns: True if the token was consumed, false otherwise.

◆ consume_ident()

Token* gymbo::consume_ident ( Token *& token )

inline

Consumes the current token if it is an identifier.

Parameters

token A pointer to the current token.

Returns: A pointer to the consumed identifier token, or NULL if the current token is not an identifier.

◆ consume_tok()

bool gymbo::consume_tok	(	Token *&	token,
		TokenKind	tok
	)

inline

Consumes the current token if it matches tok.

Parameters

token	A pointer to the current token.
tok	The token to consume.

Returns: True if the token was consumed, false otherwise.

◆ equality()

Node * gymbo::equality	(	Token *&	token,
		char *	user_input
	)

Parses an equality expression from a C-like language program.

equality = relational ("==" relational | "!=" relational)*

Parameters

token	The first token in the equality expression.
user_input	The source code of the program.

Returns: An AST node representing the equality expression.

◆ error()

void gymbo::error	(	char *	fmt,
			...
	)

inline

Reports an error and exits the program.

Parameters

fmt	The format string for the error message.
...	Additional arguments for the format string.

◆ error_at()

void gymbo::error_at	(	char *	user_input,
		char *	loc,
		char *	fmt,
			...
	)

inline

Reports an error location and exits the program.

Parameters

user_input	The input string.
loc	The location of the error.
fmt	The format string for the error message.
...	Additional arguments for the format string.

◆ expect()

void gymbo::expect	(	Token *&	token,
		char *	user_input,
		char *	op
	)

inline

Ensures that the current token matches op.

Parameters

token	A pointer to the current token.
user_input	The source code of the program.
op	The token to expect.

Exceptions

An	error if the current token does not match `op`.

◆ expect_number()

float gymbo::expect_number	(	Token *&	token,
		char *	user_input
	)

inline

Ensures that the current token is a number.

Parameters

token	A pointer to the current token.
user_input	The source code of the program.

Exceptions

An	error if the current token is not a number.

◆ explore_further()

bool gymbo::explore_further	(	int	maxDepth,
		int	maxSAT,
		int	maxUNSAT
	)

inline

Checks if further exploration is allowed based on maximum depth and satisfiability conditions.

This function determines whether further exploration is allowed based on the specified maximum depth and satisfiability conditions.

Parameters

maxDepth	The maximum depth for exploration.
maxSAT	The maximum satisfiability limit.
maxUNSAT	The maximum unsatisfiability limit.

Returns: True if further exploration is allowed, false otherwise.

◆ expr()

Node * gymbo::expr	(	Token *&	token,
		char *	user_input
	)

Parses an expression from a C-like language program.

expr = assign

Parameters

token	The first token in the expression.
user_input	The source code of the program.

Returns: An AST node representing the expression.

◆ FloatToWord()

uint32_t gymbo::FloatToWord ( float val )

inline

Converts a float value to a 32-bit word representation.

The FloatToWord function converts a float value to its 32-bit word representation using memcpy.

Parameters

val	The float value to convert.

Returns: The 32-bit word representation of the float.

◆ gcompile()

std::pair<std::unordered_map<std::string, int>, Prog> gymbo::gcompile ( char * user_input )

inline

Compiles user input into a program, returning variable counts and the compiled program.

This function takes a user-provided input in the form of a character array and performs the following steps:

Tokenizes the input, counting occurrences of variables using var_counter.
Generates an Abstract Syntax Tree (AST) from the tokenized input.
Compiles the AST into a program using gymbo::Node objects.

Parameters

user_input A character array representing the user-provided input.

Returns

A std::pair containing:

First element: An std::unordered_map<std::string, int> representing variable counts.
Second element: A Prog object representing the compiled program.

See also: tokenize() Function used for tokenization.; generate_ast() Function used for AST generation.; compile_ast() Function used for compiling the AST into a program.

◆ gen()

void gymbo::gen	(	Node *	node,
		Prog &	prg
	)

inline

Generates virtual instructions for a given AST node.

Parameters

node	The AST node to generate LLVM instructions for.
prg	The virtual program to append the generated instructions to.

◆ gen_lval()

void gymbo::gen_lval	(	Node *	node,
		Prog &	prg
	)

inline

Generates virtual instructions for a given AST node, representing the left-hand side of a variable assignment expression.

Parameters

node	The AST node representing the left-hand side of a variable assignment expression.
prg	The virtual program to append the generated instructions to.

◆ generate_ast()

void gymbo::generate_ast	(	Token *&	token,
		char *	user_input,
		std::vector< Node * > &	code
	)

inline

Parses a C-like language program into an AST.

Parameters

token	The first token in the program.
user_input	The source code of the program.
code	The vector to store Ast nodes

◆ initialize_params()

void gymbo::initialize_params	(	std::unordered_map< int, float > &	params,
		SymState &	state,
		bool	ignore_memory
	)

inline

Initialize Parameter Values from Memory.

This function initializes parameter values from memory, provided that ignore_memory is set to false.

Parameters

params	A map to store parameter values.
state	The symbolic state of the program.
ignore_memory	A flag indicating whether memory constraints should be ignored.

◆ is_alnum()

bool gymbo::is_alnum ( char c )

inline

Checks if a character is an alphanumeric character.

Parameters

c	The character to check.

Returns: true if the character is an alphanumeric character, false otherwise.

◆ is_alpha()

bool gymbo::is_alpha ( char c )

inline

Checks if a character is an alphabetical character or underscore.

Parameters

c	The character to check.

Returns: true if the character is an alphabetical character or underscore, false otherwise.

◆ is_integer()

bool gymbo::is_integer ( float x )

inline

Checks if a float is an integer.

The is_integer function checks if a given float value is an integer.

Parameters

x	The float value to check.

Returns: true if the float is an integer, otherwise false.

◆ is_target_pc()

bool gymbo::is_target_pc	(	const std::unordered_set< int > &	target_pcs,
		int	pc
	)

inline

Checks if the given program counter (pc) is a target program counter.

This function checks whether the provided program counter (pc) is part of the set of target program counters.

Parameters

target_pcs	The set of target program counters.
pc	The program counter to be checked.

Returns: True if the pc is a target program counter, false otherwise.

◆ isNegative()

bool gymbo::isNegative ( uint32_t word )

inline

Checks if a uint32_t word is negative.

Parameters

word	The uint32_t word to check.

Returns: True if the word is negative, false otherwise.

◆ logical()

Node * gymbo::logical	(	Token *&	token,
		char *	user_input
	)

Parses a logical expression from a C-like language program.

logical = equality ("&&" equality | "||" equality)*

Parameters

token	The first token in the logical expression.
user_input	The source code of the program.

Returns: An AST node representing the logical expression.

◆ mul()

Node * gymbo::mul	(	Token *&	token,
		char *	user_input
	)

inline

Parse and construct an AST node representing multiplication or division.

mul = unary ("*" unary | "/" unary)*

Parameters

token	A reference to the current token.
user_input	The user input string.

Returns: A pointer to the constructed AST node.

◆ new_binary()

Node* gymbo::new_binary	(	NodeKind	kind,
		Node *	lhs,
		Node *	rhs
	)

Create a new binary AST node with the given kind, left-hand side, and right-hand side.

Parameters

kind	The kind of the node.
lhs	The left-hand side of the binary operation.
rhs	The right-hand side of the binary operation.

Returns: A pointer to the newly created binary node.

◆ new_node()

Node* gymbo::new_node ( NodeKind kind )

Create a new AST node with the given kind.

Parameters

kind	The kind of the node.

Returns: A pointer to the newly created node.

◆ new_num()

Node* gymbo::new_num ( float val )

Create a new AST node representing a numeric value with the given value.

Parameters

val	The numeric value of the node.

Returns: A pointer to the newly created numeric node.

◆ new_token()

Token* gymbo::new_token	(	TokenKind	kind,
		Token *	cur,
		char *	str,
		int	len
	)

inline

Creates a new token and adds it as the next token of cur.

Parameters

kind	The kind of token to create.
cur	A pointer to the current token.
str	The string of the token to create.
len	The length of the token to create.

Returns: A pointer to the newly created token.

◆ pbranch()

void gymbo::pbranch ( SymState & state )

inline

Perform probabilistic branching based on symbolic execution.

Given the symbolic state, this function performs probabilistic branching. It computes the symbolic probability of the state being reached and updates the symbolic state accordingly.

Parameters

state The symbolic state for the current execution.

◆ primary()

Node * gymbo::primary	(	Token *&	token,
		char *	user_input
	)

inline

Parse and construct an AST node representing primary expressions.

primary = "(" expr ")" | num | ident

Parameters

token	A reference to the current token.
user_input	The user input string.

Returns: A pointer to the constructed AST node.

◆ relational()

Node * gymbo::relational	(	Token *&	token,
		char *	user_input
	)

Parses a relational expression from a C-like language program.

relational = add ("<" add | "<=" add | ">" add | ">=" add)*

Parameters

token	The first token in the relational expression.
user_input	The source code of the program.

Returns: An AST node representing the relational expression.

◆ smt_dpll_solver()

void gymbo::smt_dpll_solver	(	bool &	is_sat,
		SymState &	state,
		std::unordered_map< int, float > &	params,
		GDOptimizer &	optimizer,
		int	max_num_trials,
		bool	ignore_memory
	)

inline

SMT Solver using DPLL as its backend.

Parameters

is_sat	Flag to store the result of satisfiability.
state	The current symbolic state.
params	The map from the variable IDs to the concrete values.
optimizer	The gradient descent optimizer for parameter optimization.
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.

◆ smt_union_solver()

void gymbo::smt_union_solver	(	bool &	is_sat,
		SymState &	state,
		std::unordered_map< int, float > &	params,
		GDOptimizer &	optimizer,
		int	max_num_trials,
		bool	ignore_memory
	)

inline

SMT Solver with Unified Loss Function.

Parameters

is_sat	Flag to store the result of satisfiability.
state	The current symbolic state.
params	The map from the variable IDs to the concrete values.
optimizer	The gradient descent optimizer for parameter optimization.
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.

◆ startswith()

bool gymbo::startswith	(	char *	p,
		char *	q
	)

inline

Checks if the string p starts with the string q.

Parameters

p	A pointer to the string to check.
q	A pointer to the string to check against.

Returns: True if p starts with q, false otherwise.

◆ stmt()

Node * gymbo::stmt	(	Token *&	token,
		char *	user_input
	)

inline

Parse and construct an AST node representing a statement.

Parameters

token	A reference to the current token.
user_input	The user input string.

Returns: A pointer to the constructed AST node.

◆ symStep()

void gymbo::symStep	(	SymState *	state,
		Instr &	instr,
		std::vector< SymState * > &	result
	)

inline

Symbolically Execute a Single Instruction of a Program.

This function symbolically executes a single instruction of a program and generates new symbolic states, representing possible outcomes of the instruction's execution.

Parameters

state	The state of the program before the instruction is executed.
instr	The instruction to be executed.
result	A list of new symbolic states, each representing a possible outcome.

◆ tokenize()

Token* gymbo::tokenize	(	char *	user_input,
		std::unordered_map< std::string, int > &	var_counter
	)

inline

Tokenizes a given string and returns a linked list of tokens.

Parameters

user_input	The string to be tokenized.
var_counter	The map to store the mapping from variable name to variable id.

Returns: A linked list of tokens.

◆ twosComplement()

uint32_t gymbo::twosComplement ( uint32_t i )

inline

Returns the twos complement of a uint32_t word.

Parameters

i	The uint32_t word to get the twos complement of.

Returns: The twos complement of the word.

◆ unary()

Node * gymbo::unary	(	Token *&	token,
		char *	user_input
	)

inline

Parse and construct an AST node representing unary operations.

unary = ("+" | "-")? unary | primary

Parameters

token	A reference to the current token.
user_input	The user input string.

Returns: A pointer to the constructed AST node.

◆ update_prob_constraints_table()

void gymbo::update_prob_constraints_table	(	int	pc,
		SymState &	state,
		ProbPathConstraintsTable &	prob_constraints_table
	)

inline

Updates the table of probabilistic path constraints.

This function stores the path constraints and the corresponding probability of reaching the current state in a table for future reference.

Parameters

pc	The program counter.
state	The symbolic state.
prob_constraints_table	Table for storing probabilistic path constraints.

◆ valName()

std::string gymbo::valName ( int i )

inline

Generates a name for a variable based on its index.

Parameters

i	The index of the variable.

Returns: A name for the variable.

◆ verbose_constraints()

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
	)

inline

Prints a verbose for conflicts solving if conditions are met.

This function prints a verbose for conflicts solving if the specified conditions are met.

Parameters

verbose_level	The verbosity level.
is_unknown_path_constraint	Flag indicating whether the path constraint is unknown.
is_target	Flag indicating whether the program counter is a target.
is_sat	Flag indicating satisfiability.
pc	The program counter.
constraints_str	String representation of path constraints.
state	Reference to the symbolic state.
params	Reference to the map containing parameters.

◆ verbose_pconstraints()

void gymbo::verbose_pconstraints	(	int	verbose_level,
		bool	is_unknown_path_constraint,
		bool	is_target,
		bool	is_sat,
		int	pc,
		std::string	constraints_str,
		SymState &	state,
		const std::unordered_map< int, float > &	params
	)

inline

Prints verbose information about probabilistic path constraints.

This function prints the path constraints, whether they are satisfiable, the probability of reaching the current state, and other relevant information.

Parameters

verbose_level	The level of verbosity.
is_unknown_path_constraint	Whether the path constraint is unknown.
is_target	Whether the program counter is a target.
is_sat	Whether the path constraint is satisfiable.
pc	The program counter.
constraints_str	String representation of the path constraints.
state	The symbolic state.
params	Dictionary of symbolic variable values.

◆ verbose_post()

void gymbo::verbose_post ( int verbose_level )

inline

Prints a verbose representation after solving constraints.

This function prints a verbose representation after solving constraints.

Parameters

verbose_level The verbosity level.

◆ verbose_pre()

void gymbo::verbose_pre	(	int	verbose_level,
		int	pc,
		Prog &	prog,
		SymState &	state
	)

inline

Prints a verbose representation before solving constraints.

This function prints a verbose representation before solving constraints.

Parameters

verbose_level	The verbosity level.
pc	The program counter.
prog	Reference to the program.
state	Reference to the symbolic state.

◆ wordToBool()

bool gymbo::wordToBool ( uint32_t word )

inline

Converts a uint32_t word to a bool.

Parameters

word	The uint32_t word to convert.

Returns: The bool equivalent of the word.

◆ wordToFloat()

float gymbo::wordToFloat ( uint32_t word )

inline

Converts a 32-bit word representation to a float value.

The wordToFloat function converts a 32-bit word representation to its corresponding float value using memcpy.

Parameters

word	The 32-bit word representation.

Returns: The float value.

◆ wordToInt()

int gymbo::wordToInt ( uint32_t word )

inline

Converts a 32-bit word representation to an integer value.

The wordToInt function converts a 32-bit word representation to its corresponding integer value using static_cast.

Parameters

word	The 32-bit word representation.

Returns: The integer value.

◆ wordToSignedInt()

int gymbo::wordToSignedInt ( uint32_t word )

inline

Converts a uint32_t word to a signed int.

Parameters

word	The uint32_t word to convert.

Returns: The signed int equivalent of the word.

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ Mem

◆ PathConstraintsTable

◆ ProbPathConstraintsTable

◆ Prog

◆ SMem

◆ Word32

Enumeration Type Documentation

◆ InstrType

◆ NodeKind

◆ SymType

◆ TokenKind

Function Documentation

◆ add()

◆ assign()

◆ at_eof()

◆ boolToWord()

◆ call_smt_solver()

◆ cartesianProduct()

◆ compile_ast()

◆ consume()

◆ consume_ident()

◆ consume_tok()

◆ equality()

◆ error()

◆ error_at()

◆ expect()

◆ expect_number()

◆ explore_further()

◆ expr()

◆ FloatToWord()

◆ gcompile()

◆ gen()

◆ gen_lval()

◆ generate_ast()

◆ initialize_params()

◆ is_alnum()

◆ is_alpha()

◆ is_integer()

◆ is_target_pc()

◆ isNegative()

◆ logical()

◆ mul()

◆ new_binary()

◆ new_node()

◆ new_num()

◆ new_token()

◆ pbranch()

◆ primary()

◆ relational()

◆ smt_dpll_solver()

◆ smt_union_solver()

◆ startswith()

◆ stmt()

◆ symStep()

◆ tokenize()

◆ twosComplement()

◆ unary()

◆ update_prob_constraints_table()

◆ valName()

◆ verbose_constraints()

◆ verbose_pconstraints()

◆ verbose_post()

◆ verbose_pre()

◆ wordToBool()

◆ wordToFloat()

◆ wordToInt()

◆ wordToSignedInt()