Gymbo

Classes | Typedefs | Enumerations | Functions
gymbo Namespace Reference

## 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:

1. Tokenizes the input, counting occurrences of variables using var_counter.
2. Generates an Abstract Syntax Tree (AST) from the tokenized input.
3. 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.