Gymbo

smt.h
Go to the documentation of this file.
1
7 #pragma once
8 #include "gd.h"
9 #include "sat.h"
10 namespace gymbo {
11
23 inline void initialize_params(std::unordered_map<int, float> &params,
24 SymState &state, bool ignore_memory) {
25 params = {};
26 if (!ignore_memory) {
27 for (auto &p : state.mem) {
28 params.emplace(std::make_pair(p.first, wordToFloat(p.second)));
29 }
30 }
31 }
32
44 inline void smt_union_solver(bool &is_sat, SymState &state,
45 std::unordered_map<int, float> &params,
46 GDOptimizer &optimizer, int max_num_trials,
47 bool ignore_memory) {
48 for (int j = 0; j < max_num_trials; j++) {
49 is_sat = optimizer.solve(state.path_constraints, params);
50 if (is_sat) {
51 break;
52 }
53 optimizer.seed += 1;
54 int total_num_params = params.size();
55 initialize_params(params, state, ignore_memory);
56 int total_num_consts = params.size();
57 if (total_num_consts == total_num_params) {
58 break;
59 }
60 }
61 }
62
74 inline void smt_dpll_solver(bool &is_sat, SymState &state,
75 std::unordered_map<int, float> &params,
76 GDOptimizer &optimizer, int max_num_trials,
77 bool ignore_memory) {
78 std::unordered_map<std::string, gymbo::Sym *> unique_terms_map;
79 std::unordered_map<std::string, bool> assignments_map;
80 std::shared_ptr<gymbosat::Expr> path_constraints_expr =
81 gymbosat::pathconstraints2expr(state.path_constraints,
82 unique_terms_map);
83
84 while (satisfiableDPLL(path_constraints_expr, assignments_map)) {
85 std::vector<Sym> new_constraints;
86 for (auto &ass : assignments_map) {
87 if (ass.second) {
88 new_constraints.emplace_back(*unique_terms_map[ass.first]);
89 } else {
90 new_constraints.emplace_back(
91 Sym(SymType::SNot, unique_terms_map[ass.first]));
92 }
93 }
94
95 for (int j = 0; j < max_num_trials; j++) {
96 is_sat = optimizer.solve(new_constraints, params);
97 if (is_sat) {
98 break;
99 }
100 optimizer.seed += 1;
101 initialize_params(params, state, ignore_memory);
102 }
103
104 if (is_sat) {
105 break;
106 }
107
108 // add feedback
109 std::shared_ptr<gymbosat::Expr> learnt_constraints =
110 std::make_shared<gymbosat::Const>(false);
111 for (auto &ass : assignments_map) {
112 if (ass.second) {
113 learnt_constraints = std::make_shared<gymbosat::Or>(
114 learnt_constraints,
115 std::make_shared<gymbosat::Not>(
116 std::make_shared<gymbosat::Var>(ass.first)));
117 } else {
118 learnt_constraints = std::make_shared<gymbosat::Or>(
119 learnt_constraints,
120 std::make_shared<gymbosat::Var>(ass.first));
121 }
122 }
123
124 path_constraints_expr = std::make_shared<gymbosat::And>(
125 path_constraints_expr, learnt_constraints);
126 }
127 }
128
129 } // namespace gymbo
gd.h
Implementation of gradient descent optimizer.
gymbo
Definition: compiler.h:11
gymbo::wordToFloat
float wordToFloat(uint32_t word)
Converts a 32-bit word representation to a float value.
Definition: utils.h:51
gymbo::SymType::SNot
@ SNot
gymbo::initialize_params
void initialize_params(std::unordered_map< int, float > &params, SymState &state, bool ignore_memory)
Initialize Parameter Values from Memory.
Definition: smt.h:23
gymbo::smt_union_solver
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.
Definition: smt.h:44
gymbo::smt_dpll_solver
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.
Definition: smt.h:74
gymbosat::satisfiableDPLL
bool satisfiableDPLL(std::shared_ptr< Expr > expr, std::unordered_map< std::string, bool > &assignments_map)
Check satisfiability of a logical expression using the DPLL algorithm.
Definition: sat.h:685
gymbosat::pathconstraints2expr
std::shared_ptr< Expr > pathconstraints2expr(std::vector< gymbo::Sym > &constraints, std::unordered_map< std::string, gymbo::Sym * > &unique_sym_map)
Convert a vector of symbolic path constraints to a logical expression.
Definition: sat.h:765
sat.h
Implementation of SAT solver.
gymbo::GDOptimizer
Gradient Descent Optimizer for Symbolic Path Constraints.
Definition: gd.h:28
gymbo::GDOptimizer::seed
int seed
Random seed for initializing parameter values.
Definition: gd.h:42
gymbo::GDOptimizer::solve
bool solve(std::vector< Sym > &path_constraints, std::unordered_map< int, float > &params, bool is_init_params_const=true)
Solve path constraints using gradient descent optimization.
Definition: gd.h:110
gymbo::SymState
Struct representing the symbolic state of the symbolic execution.
Definition: type.h:1042
gymbo::SymState::path_constraints
std::vector< Sym > path_constraints
Definition: type.h:1049
gymbo::SymState::mem
Mem mem
Definition: type.h:1045
gymbo::Sym
Struct representing a symbolic expression.
Definition: type.h:265