

Gymbo is a Proof of Concept for a Gradient-\/based Symbolic Execution Engine, implemented from scratch. Building on recent advancements that utilize gradient descent to solve SMT formulas {\ttfamily \mbox{[}1, 2\mbox{]}}, Gymbo leverages gradient descent to discover input values that fulfill each path constraint during symbolic execution.

Compared to other prominent symbolic execution tools, Gymbo\textquotesingle{}s implementation is notably simpler and more compact. We hope that this project will assist individuals in grasping the fundamental principles of symbolic execution and SMT problem-\/solving through gradient descent.

One practical usage of Gymbo is debugging ML models like neural networks to detect unexpected behaviors. For example, you can generate adversarial examples with Gymbo by converting neural networks to imperative programs.



Another unique feature of Gymbo is that it can track the probabilistic symbolic variables. We adopt the PBRANCH algorithm proposed in {\ttfamily \mbox{[}3\mbox{]}} and currently support the discrete uniform, bernoulli, and binomial distributions.



\begin{quote}
Please note that Gymbo is currently under development and may have bugs. \end{quote}
Your feedback and contributions are always greatly appreciated.\hypertarget{index_install_sec}{}\doxysection{Install}\label{index_install_sec}

\begin{DoxyCode}{0}
\DoxyCodeLine{git clone https://github.com/Koukyosyumei/Gymbo.git}
\DoxyCodeLine{./script/build.sh}

\end{DoxyCode}
\hypertarget{index_grammar_sec}{}\doxysection{Input Source Code Grammar}\label{index_grammar_sec}
Gymbo presently supports C-\/like programs with the following BNF grammar\+:


\begin{DoxyCode}{0}
\DoxyCodeLine{program    = \mbox{\hyperlink{namespacegymbo_a0269bd238863b0c8e036e5fb7d66fa79}{stmt}}*}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a0269bd238863b0c8e036e5fb7d66fa79}{stmt}}       = \mbox{\hyperlink{namespacegymbo_a9e2a8633fd8ee1ed723406efc5a82b06}{expr}} \textcolor{stringliteral}{"{};"{}}}
\DoxyCodeLine{         | \textcolor{stringliteral}{"{}\{"{}} \mbox{\hyperlink{namespacegymbo_a0269bd238863b0c8e036e5fb7d66fa79}{stmt}}* \textcolor{stringliteral}{"{}\}"{}}}
\DoxyCodeLine{         | \textcolor{stringliteral}{"{}if"{}} \textcolor{stringliteral}{"{}("{}} \mbox{\hyperlink{namespacegymbo_a9e2a8633fd8ee1ed723406efc5a82b06}{expr}} \textcolor{stringliteral}{"{})"{}} \mbox{\hyperlink{namespacegymbo_a0269bd238863b0c8e036e5fb7d66fa79}{stmt}} (\textcolor{stringliteral}{"{}else"{}} \mbox{\hyperlink{namespacegymbo_a0269bd238863b0c8e036e5fb7d66fa79}{stmt}})?}
\DoxyCodeLine{         | \textcolor{stringliteral}{"{}return"{}} \mbox{\hyperlink{namespacegymbo_a9e2a8633fd8ee1ed723406efc5a82b06}{expr}} \textcolor{stringliteral}{"{};"{}}}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a9e2a8633fd8ee1ed723406efc5a82b06}{expr}}       = \mbox{\hyperlink{namespacegymbo_a47b7251f53d2ee3e14494fb9f7a2bc72}{assign}}}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a47b7251f53d2ee3e14494fb9f7a2bc72}{assign}}     = \mbox{\hyperlink{namespacegymbo_aee43a52e33ae6335a16161d16abd1079}{logical}} (\textcolor{stringliteral}{"{}="{}} \mbox{\hyperlink{namespacegymbo_a47b7251f53d2ee3e14494fb9f7a2bc72}{assign}})?}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_aee43a52e33ae6335a16161d16abd1079}{logical}}    = \mbox{\hyperlink{namespacegymbo_a93198308f32bb09209f19ea243dfbd7e}{equality}} (\textcolor{stringliteral}{"{}\&\&"{}} \mbox{\hyperlink{namespacegymbo_a93198308f32bb09209f19ea243dfbd7e}{equality}} | \textcolor{stringliteral}{"{}||"{}} \mbox{\hyperlink{namespacegymbo_a93198308f32bb09209f19ea243dfbd7e}{equality}})*}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a93198308f32bb09209f19ea243dfbd7e}{equality}}   = \mbox{\hyperlink{namespacegymbo_a7782376e331d91dd967f5a7b1c23c1ba}{relational}} (\textcolor{stringliteral}{"{}=="{}} \mbox{\hyperlink{namespacegymbo_a7782376e331d91dd967f5a7b1c23c1ba}{relational}} | \textcolor{stringliteral}{"{}!="{}} \mbox{\hyperlink{namespacegymbo_a7782376e331d91dd967f5a7b1c23c1ba}{relational}})*}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a7782376e331d91dd967f5a7b1c23c1ba}{relational}} = \mbox{\hyperlink{namespacegymbo_a7b0b70c62f575e191b45877710aecc9c}{add}} (\textcolor{stringliteral}{"{}<"{}} \mbox{\hyperlink{namespacegymbo_a7b0b70c62f575e191b45877710aecc9c}{add}} | \textcolor{stringliteral}{"{}<="{}} \mbox{\hyperlink{namespacegymbo_a7b0b70c62f575e191b45877710aecc9c}{add}} | \textcolor{stringliteral}{"{}>"{}} \mbox{\hyperlink{namespacegymbo_a7b0b70c62f575e191b45877710aecc9c}{add}} | \textcolor{stringliteral}{"{}>="{}} \mbox{\hyperlink{namespacegymbo_a7b0b70c62f575e191b45877710aecc9c}{add}})*}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a7b0b70c62f575e191b45877710aecc9c}{add}}        = \mbox{\hyperlink{namespacegymbo_a586e5510f2ba9c76f7bcb78a3dafd69a}{mul}} (\textcolor{stringliteral}{"{}+"{}} \mbox{\hyperlink{namespacegymbo_a586e5510f2ba9c76f7bcb78a3dafd69a}{mul}} | \textcolor{stringliteral}{"{}-\/"{}} \mbox{\hyperlink{namespacegymbo_a586e5510f2ba9c76f7bcb78a3dafd69a}{mul}})*}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a586e5510f2ba9c76f7bcb78a3dafd69a}{mul}}        = \mbox{\hyperlink{namespacegymbo_ac29372113d1f5d63e50aec27aa2bab58}{unary}} (\textcolor{stringliteral}{"{}*"{}} \mbox{\hyperlink{namespacegymbo_ac29372113d1f5d63e50aec27aa2bab58}{unary}} | \textcolor{stringliteral}{"{}/"{}} \mbox{\hyperlink{namespacegymbo_ac29372113d1f5d63e50aec27aa2bab58}{unary}})*}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_ac29372113d1f5d63e50aec27aa2bab58}{unary}}      = (\textcolor{stringliteral}{"{}+"{}} | \textcolor{stringliteral}{"{}-\/"{}})? \mbox{\hyperlink{namespacegymbo_aab835796afd998bcd50e272c9eb29d00}{primary}}}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_aab835796afd998bcd50e272c9eb29d00}{primary}}    = num | ident | \textcolor{stringliteral}{"{}("{}} \mbox{\hyperlink{namespacegymbo_a9e2a8633fd8ee1ed723406efc5a82b06}{expr}} \textcolor{stringliteral}{"{})"{}}}

\end{DoxyCode}


\begin{quote}
Please note that Gymbo currently ignores {\ttfamily /} when solving path constraints. \end{quote}
\hypertarget{index_algorithm_sec}{}\doxysection{Internal Algorithm}\label{index_algorithm_sec}
Gymbo converts the path constraint into a numerical loss function, which becomes negative only when the path constraint is satisfied. Gymbo uses the following transformation rule\+:


\begin{DoxyCode}{0}
\DoxyCodeLine{!(a)     => -\/a + eps}
\DoxyCodeLine{(a < b)  => a -\/ b + eps}
\DoxyCodeLine{(a <= b) => a -\/ b}
\DoxyCodeLine{(a > b)  => b -\/ a + eps}
\DoxyCodeLine{(a >= b) => b -\/ a}
\DoxyCodeLine{(a == b) => abs(a -\/ b)}
\DoxyCodeLine{(a != b) => -\/abs(a -\/ b) + eps}
\DoxyCodeLine{(a \&\& b) => max(a, b)}
\DoxyCodeLine{(a || b) => min(a, b)}

\end{DoxyCode}


Here, {\ttfamily eps} is the smallest positive value of the type for a and b.

Optionally, Gymbo can use DPLL (SAT solver) to decide the assignment for each unique term, sometimes resulting in better scalability.\hypertarget{index_cli_sec}{}\doxysection{CLI Tool}\label{index_cli_sec}
{\ttfamily gymbo} command accepts the following command-\/line options\+:


\begin{DoxyItemize}
\item {\ttfamily -\/d}\+: Set the maximum depth for symbolic execution (default\+: 256).
\item {\ttfamily -\/v}\+: Set the verbosity level (default\+: 1). Use -\/1 for minimal output.
\item {\ttfamily -\/i}\+: Set the number of iterations for gradient descent (default\+: 100).
\item {\ttfamily -\/a}\+: Set the step size for gradient descent (default\+: 1.\+0).
\item {\ttfamily -\/e}\+: Set the eps for the differentiable expression (default\+: 1.\+0).
\item {\ttfamily -\/t}\+: Set the maximum number of trials of gradient descent (default\+: 3)
\item {\ttfamily -\/l}\+: Set the minimum value of initial parameters (default\+: -\/10)
\item {\ttfamily -\/h}\+: Set the maximum value of initial parameters (default\+: 10)
\item {\ttfamily -\/s}\+: Set the random seed (default\+: 42)
\item {\ttfamily -\/p}\+: (optional) If set, use DPLL to determine the assignment for each term. Otherwise, solve the loss function directly transformed from the path constraints.
\end{DoxyItemize}


\begin{DoxyCode}{0}
\DoxyCodeLine{./gymbo "{}if (a < 3) if (a > 4) return 1;"{} -\/v 0}
\DoxyCodeLine{}
\DoxyCodeLine{>Compiling the input program...}
\DoxyCodeLine{>Start Symbolic Execution...}
\DoxyCodeLine{>-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/}
\DoxyCodeLine{>Result Summary}
\DoxyCodeLine{>\#Total Path Constraints: 4}
\DoxyCodeLine{>\#SAT: 3}
\DoxyCodeLine{>\#UNSAT: 1}
\DoxyCodeLine{>List of UNSAT Path Constraints}
\DoxyCodeLine{>\# var\_1 < 3 and 4 < var\_1 and  1}

\end{DoxyCode}
\hypertarget{index_lib_sec}{}\doxysection{libgymbo\+: Header-\/only Library}\label{index_lib_sec}
Since gymbo consists of the header-\/only library, you can easily create your own symbolic execution tool.


\begin{DoxyCode}{0}
\DoxyCodeLine{\textcolor{preprocessor}{\#include "{}\mbox{\hyperlink{compiler_8h}{libgymbo/compiler.h}}"{}}}
\DoxyCodeLine{\textcolor{preprocessor}{\#include "{}\mbox{\hyperlink{gd_8h}{libgymbo/gd.h}}"{}}}
\DoxyCodeLine{\textcolor{preprocessor}{\#include "{}\mbox{\hyperlink{parser_8h}{libgymbo/parser.h}}"{}}}
\DoxyCodeLine{\textcolor{preprocessor}{\#include "{}\mbox{\hyperlink{tokenizer_8h}{libgymbo/tokenizer.h}}"{}}}
\DoxyCodeLine{\textcolor{preprocessor}{\#include "{}\mbox{\hyperlink{type_8h}{libgymbo/type.h}}"{}}}
\DoxyCodeLine{}
\DoxyCodeLine{\textcolor{keywordtype}{char} user\_input[] = \textcolor{stringliteral}{"{}if (a < 3) return 1;"{}}}
\DoxyCodeLine{}
\DoxyCodeLine{std::vector<gymbo::Node *> code;}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a9b6a88c2be45a5e3fd3f053681f89733}{gymbo::Prog}} prg;}
\DoxyCodeLine{\mbox{\hyperlink{structgymbo_1_1GDOptimizer}{gymbo::GDOptimizer}} optimizer(num\_itrs, step\_size);}
\DoxyCodeLine{\mbox{\hyperlink{structgymbo_1_1SymState}{gymbo::SymState}} init;}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_aea0120f1cdc1417f9b6b8480ac562389}{gymbo::PathConstraintsTable}} cache\_constraints;}
\DoxyCodeLine{}
\DoxyCodeLine{\textcolor{comment}{// tokenize the input source code}}
\DoxyCodeLine{\mbox{\hyperlink{structgymbo_1_1Token}{gymbo::Token}} *token = \mbox{\hyperlink{namespacegymbo_a89c8cb7e3b04d3d02f0cba69ab593981}{gymbo::tokenize}}(user\_input);}
\DoxyCodeLine{\textcolor{comment}{// generate AST from the tokens}}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a5e7728b7fbac9bf79ae665cf9b94f443}{gymbo::generate\_ast}}(token, user\_input, code);}
\DoxyCodeLine{\textcolor{comment}{// construct virtual stack machine from AST}}
\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a1af6d97f4c122833601a9b054a23009a}{gymbo::compile\_ast}}(code, prg);}
\DoxyCodeLine{}
\DoxyCodeLine{\textcolor{comment}{// execute gradient-\/based symbolie execution}}
\DoxyCodeLine{\mbox{\hyperlink{structgymbo_1_1SExecutor}{gymbo::SExecutor}} executor(optimizer, maxSAT, maxUNSAT, max\_num\_trials,}
\DoxyCodeLine{                          ignore\_memory, use\_dpll, verbose\_level);}
\DoxyCodeLine{executor.run(prg, target\_pcs, init, max\_depth);}

\end{DoxyCode}
\hypertarget{index_python_sec}{}\doxysection{Python API}\label{index_python_sec}
\hypertarget{index_install_py}{}\doxysubsection{Install}\label{index_install_py}

\begin{DoxyCode}{0}
\DoxyCodeLine{pip install git+https:\textcolor{comment}{//github.com/Koukyosyumei/Gymbo}}

\end{DoxyCode}
\hypertarget{index_pylibgymbo_sec}{}\doxysubsection{pylibgymbo\+: Python Wrapper for libgymbo}\label{index_pylibgymbo_sec}

\begin{DoxyCode}{0}
\DoxyCodeLine{import pylibgymbo as plg}
\DoxyCodeLine{}
\DoxyCodeLine{inp = "{}a = 1; if (a == 1) return 2;"{}}
\DoxyCodeLine{var\_counter, prg = plg.gcompile(inp)}
\DoxyCodeLine{}
\DoxyCodeLine{optimizer = plg.GDOptimizer(num\_itrs, step\_size, ...)}
\DoxyCodeLine{executor = plg.SExecutor(optimizer, maxSAT, maxUNSAT, max\_num\_trials,}
\DoxyCodeLine{                         ignore\_memory, use\_dpll, verbose\_level)}
\DoxyCodeLine{executor.run(prg, target\_pcs, init, max\_depth)}

\end{DoxyCode}
\hypertarget{index_pymlgymbo_sec}{}\doxysubsection{pymlgymbo\+: Debugging Machine Learning Models}\label{index_pymlgymbo_sec}
We offer some helper functions within {\ttfamily pymlgymbo} library to convert the ML models of famous Python library like sklearn and Py\+Torch to the program that gymbo can process.

The following code generates the adversarial examples against a neural network, as proposed in \mbox{[}3\mbox{]}


\begin{DoxyCode}{0}
\DoxyCodeLine{from sklearn.neural\_network import MLPClassifier}
\DoxyCodeLine{}
\DoxyCodeLine{import pylibgymbo as plg}
\DoxyCodeLine{import pymlgymbo as pmg}
\DoxyCodeLine{}
\DoxyCodeLine{clf = MLPClassifier(activation="{}relu"{})}
\DoxyCodeLine{clf.fit(X\_train, y\_train)}
\DoxyCodeLine{}
\DoxyCodeLine{}
\DoxyCodeLine{mlp\_code = pmg.dump\_sklearn\_MLP(clf, feature\_names)}
\DoxyCodeLine{adv\_condition = (}
\DoxyCodeLine{      "{}("{}}
\DoxyCodeLine{      + "{} || "{}.join(}
\DoxyCodeLine{          [f"{}(y\_\{c\} > y\_\{y\_pred\})"{} for c in range(len(clf.classes\_)) if}
\DoxyCodeLine{y\_pred != c]}
\DoxyCodeLine{      )}
\DoxyCodeLine{      + "{})"{}}
\DoxyCodeLine{  )}
\DoxyCodeLine{}
\DoxyCodeLine{optimizer = plg.GDOptimizer(num\_itrs, step\_size, ...)}
\DoxyCodeLine{var\_counter, prg = plg.gcompile(mlp\_code)}
\DoxyCodeLine{}
\DoxyCodeLine{executor = plg.SExecutor(optimizer, maxSAT, maxUNSAT, max\_num\_trials,}
\DoxyCodeLine{                         ignore\_memory, use\_dpll, verbose\_level)}
\DoxyCodeLine{executor.run(prg, target\_pcs, init, max\_depth)}

\end{DoxyCode}
\hypertarget{index_acknowledgement_sec}{}\doxysection{Acknowledgement}\label{index_acknowledgement_sec}
Gymbo is entirely implemented in C++ and requires only standard libraries. The process of compiling from source code to stack machines is based on the implementation of {\ttfamily rui314/chibicc \mbox{[}4\mbox{]}}, while the symbolic execution approach is inspired by {\ttfamily beala/symbolic \mbox{[}5\mbox{]}}.\hypertarget{index_reference_sec}{}\doxysection{Reference}\label{index_reference_sec}

\begin{DoxyCode}{0}
\DoxyCodeLine{-\/ [1] Chen, Peng, Jianzhong Liu, and Hao Chen. \textcolor{stringliteral}{"{}Matryoshka: fuzzing deeply}}
\DoxyCodeLine{\textcolor{stringliteral}{nested branches."{}} Proceedings of the 2019 ACM SIGSAC Conference on Computer}
\DoxyCodeLine{and Communications Security. 2019.}
\DoxyCodeLine{-\/ [2] Minghao Liu, Kunhang Lv, Pei Huang, Rui Han, Fuqi Jia, Yu Zhang, Feifei}
\DoxyCodeLine{Ma, Jian Zhang. \textcolor{stringliteral}{"{}NRAgo: Solving SMT(NRA) Formulas with Gradient-\/based}}
\DoxyCodeLine{\textcolor{stringliteral}{Optimization."{}} IEEE/ACM International Conference on Automated Software}
\DoxyCodeLine{Engineering, 2023}
\DoxyCodeLine{-\/ [3] Gopinath, Divya, et al. \textcolor{stringliteral}{"{}Symbolic execution for importance analysis and}}
\DoxyCodeLine{\textcolor{stringliteral}{adversarial generation in neural networks."{}} 2019 IEEE 30th International}
\DoxyCodeLine{Symposium on Software Reliability Engineering (ISSRE). IEEE, 2019.}
\DoxyCodeLine{-\/ [4] https:\textcolor{comment}{//github.com/rui314/chibicc}}
\DoxyCodeLine{-\/ [5] https:\textcolor{comment}{//github.com/beala/symbolic}}

\end{DoxyCode}
 