Gymbo

psymbolic.h
Go to the documentation of this file.
1
7 #pragma once
8 #include "symbolic.h"
9
10 namespace gymbo {
11
21 inline void pbranch(SymState &state) {
22 int n_path_constraints = state.path_constraints.size();
23 if (state.has_observed_p_cond) {
24 Sym *n_cond = &state.path_constraints[0];
25 Sym *d_cond = &state.path_constraints[0];
26 for (int i = 1; i < n_path_constraints - 1; i++) {
27 n_cond = new Sym(SymType::SAnd, n_cond, &state.path_constraints[i]);
28 d_cond = new Sym(SymType::SAnd, d_cond, &state.path_constraints[i]);
29 }
30 n_cond = new Sym(SymType::SAnd, n_cond,
31 &state.path_constraints[n_path_constraints - 1]);
32 state.cond_p = new SymProb(n_cond, d_cond);
33 state.p = state.p->pmul(state.cond_p);
34 } else {
35 Sym *n_cond;
36 if (n_path_constraints == 0) {
37 n_cond = new Sym(SymType::SCon, FloatToWord(0.0f));
38 } else {
39 n_cond = &state.path_constraints[0];
40 }
41 for (int i = 1; i < n_path_constraints; i++) {
42 n_cond = new Sym(SymType::SAnd, n_cond, &state.path_constraints[i]);
43 }
44 Sym *d_cond = new Sym(SymType::SCon, FloatToWord(1.0f));
45 state.p = new SymProb(n_cond, d_cond);
46 state.cond_p = state.p;
47 state.has_observed_p_cond = true;
48 }
49 }
50
67 inline void verbose_pconstraints(int verbose_level,
68 bool is_unknown_path_constraint,
69 bool is_target, bool is_sat, int pc,
70 std::string constraints_str, SymState &state,
71 const std::unordered_map<int, float> &params) {
72 if (verbose_level >= 1) {
73 if ((verbose_level >= 1 && is_unknown_path_constraint && is_target) ||
74 (verbose_level >= 2)) {
75 if (!is_sat) {
76 printf("\x1b[31m");
77 } else {
78 printf("\x1b[32m");
79 }
80 printf("pc=%d, IS_SAT - %d\x1b[39m, Pr.REACH - %s, %s, params = {",
81 pc, is_sat, state.cond_p->toString().c_str(),
82 constraints_str.c_str());
83 for (auto &p : params) {
84 // ignore concrete variables
85 if (state.mem.find(p.first) != state.mem.end()) {
86 continue;
87 }
88 // only show symbolic variables
89 if (is_integer(p.second)) {
90 printf("%d: %d, ", p.first, (int)p.second);
91 } else {
92 printf("%d: %f, ", p.first, p.second);
93 }
94 }
95 printf("}\n");
96 }
97 }
98 }
99
111 inline void update_prob_constraints_table(
112 int pc, SymState &state, ProbPathConstraintsTable &prob_constraints_table) {
113 Sym cc = state.path_constraints[0];
114 for (int i = 1; i < state.path_constraints.size(); i++) {
115 cc = Sym(SymType::SAnd, cc.copy(), &state.path_constraints[i]);
116 }
117 if (prob_constraints_table.find(pc) == prob_constraints_table.end()) {
118 std::vector<std::tuple<Sym, Mem, SymProb>> tmp = {
119 std::make_tuple(cc, state.mem, *state.p)};
120 prob_constraints_table.emplace(pc, tmp);
121 } else {
122 prob_constraints_table[pc].emplace_back(
123 std::make_tuple(cc, state.mem, *state.p));
124 }
125 }
126
132 struct PSExecutor : public BaseExecutor {
133 std::unordered_set<int> random_vars;
134 PathConstraintsTable
135 constraints_cache;
136 ProbPathConstraintsTable
137 prob_constraints_table;
139
140 using BaseExecutor::BaseExecutor;
141
142 void register_random_var(int var_id) { random_vars.emplace(var_id); }
143
157 bool solve(bool is_target, int pc, SymState &state) {
158 std::string constraints_str = state.toString(false);
159
160 std::unordered_map<int, float> params = {};
161 initialize_params(params, state, ignore_memory);
162
163 bool is_sat = true;
164 bool is_unknown_path_constraint = true;
165
166 if (constraints_cache.find(constraints_str) !=
167 constraints_cache.end()) {
168 is_sat = constraints_cache[constraints_str].first;
169 params = constraints_cache[constraints_str].second;
170 is_unknown_path_constraint = false;
171 } else {
172 bool is_contain_prob_var = false;
173 std::unordered_set<int> unique_var_ids;
174 for (int i = 0; i < state.path_constraints.size(); i++) {
175 state.path_constraints[i].gather_var_ids(unique_var_ids);
176 }
177 for (int i : unique_var_ids) {
178 if (random_vars.find(i) != random_vars.end()) {
179 is_contain_prob_var = true;
180 break;
181 }
182 }
183
184 if (is_contain_prob_var) {
185 // call probabilistic branch algorithm
186 pbranch(state);
187 is_sat = true;
188 } else {
189 // solve deterministic path constraints
190 call_smt_solver(is_sat, state, params, optimizer,
191 max_num_trials, ignore_memory, use_dpll);
192 if (is_sat) {
193 maxSAT--;
194 } else {
195 maxUNSAT--;
196 }
197
198 if (is_sat) {
199 state.p =
200 new SymProb(new Sym(SymType::SCon, FloatToWord(0.0f)),
201 new Sym(SymType::SCon, FloatToWord(0.0f)));
202 state.cond_p = state.p;
203 }
204 }
205
206 constraints_cache.emplace(constraints_str,
207 std::make_pair(is_sat, params));
208 }
209
210 if (verbose_level >= 1) {
211 verbose_pconstraints(verbose_level, is_unknown_path_constraint,
212 is_target, is_sat, pc, constraints_str, state,
213 params);
214 }
215
216 return is_sat;
217 }
218
235 Trace run(Prog &prog, std::unordered_set<int> &target_pcs, SymState &state,
236 int maxDepth = 256) {
237 int pc = state.pc;
238 bool is_target = is_target_pc(target_pcs, pc);
239 bool is_sat = true;
240
241 verbose_pre(verbose_level, pc, prog, state);
242 if (state.path_constraints.size() != 0 && is_target) {
243 is_sat = solve(is_target, pc, state);
244 }
245 verbose_post(verbose_level);
246
247 if (prog[pc].instr == InstrType::Done &&
248 state.path_constraints.size() > 0) {
249 update_prob_constraints_table(pc, state, prob_constraints_table);
250 }
251
252 if ((prog[pc].instr == InstrType::Done) || (!is_sat)) {
253 return Trace(state, {});
254 } else if (explore_further(maxDepth, maxSAT, maxUNSAT)) {
255 Instr instr = prog[pc];
256 std::vector<SymState *> newStates;
257 symStep(&state, instr, newStates);
258 std::vector<Trace> children;
259 for (SymState *newState : newStates) {
260 Trace child = run(prog, target_pcs, *newState, maxDepth - 1);
261 if (return_trace) {
262 children.push_back(child);
263 }
264 }
265 return Trace(state, children);
266 } else {
267 return Trace(state, {});
268 }
269 }
270 };
271 } // namespace gymbo
272
gymbo::Instr
Class representing an instruction.
Definition: type.h:53
gymbo
Definition: compiler.h:11
gymbo::ProbPathConstraintsTable
std::unordered_map< int, std::vector< std::tuple< Sym, Mem, SymProb > >> ProbPathConstraintsTable
Alias for a table of probabilistic path constraints.
Definition: type.h:1205
gymbo::explore_further
bool explore_further(int maxDepth, int maxSAT, int maxUNSAT)
Checks if further exploration is allowed based on maximum depth and satisfiability conditions.
Definition: symbolic.h:40
gymbo::call_smt_solver
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.
Definition: symbolic.h:58
gymbo::InstrType::Done
@ Done
gymbo::pbranch
void pbranch(SymState &state)
Perform probabilistic branching based on symbolic execution.
Definition: psymbolic.h:21
gymbo::is_integer
bool is_integer(float x)
Checks if a float is an integer.
Definition: utils.h:25
gymbo::SymType::SAnd
@ SAnd
gymbo::SymType::SCon
@ SCon
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::is_target_pc
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.
Definition: symbolic.h:22
gymbo::verbose_pre
void verbose_pre(int verbose_level, int pc, Prog &prog, SymState &state)
Prints a verbose representation before solving constraints.
Definition: symbolic.h:128
gymbo::FloatToWord
uint32_t FloatToWord(float val)
Converts a float value to a 32-bit word representation.
Definition: utils.h:36
gymbo::symStep
void symStep(SymState *state, Instr &instr, std::vector< SymState * > &result)
Symbolically Execute a Single Instruction of a Program.
Definition: symbolic.h:164
gymbo::Prog
std::vector< Instr > Prog
Alias for a program, represented as a vector of instructions.
Definition: type.h:143
gymbo::update_prob_constraints_table
void update_prob_constraints_table(int pc, SymState &state, ProbPathConstraintsTable &prob_constraints_table)
Updates the table of probabilistic path constraints.
Definition: psymbolic.h:111
gymbo::verbose_post
void verbose_post(int verbose_level)
Prints a verbose representation after solving constraints.
Definition: symbolic.h:146
gymbo::verbose_pconstraints
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.
Definition: psymbolic.h:67
gymbo::PathConstraintsTable
std::unordered_map< std::string, std::pair< bool, std::unordered_map< int, float > >> PathConstraintsTable
Alias for a table of path constraints.
Definition: type.h:1189
gymbo::BaseExecutor
Represents the base class for symbolic execution engine.
Definition: symbolic.h:397
gymbo::BaseExecutor::max_num_trials
int max_num_trials
Definition: symbolic.h:402
gymbo::BaseExecutor::return_trace
bool return_trace
Definition: symbolic.h:409
gymbo::BaseExecutor::ignore_memory
bool ignore_memory
Definition: symbolic.h:405
gymbo::BaseExecutor::maxUNSAT
int maxUNSAT
The maximum number of UNSAT constraints to collect.
Definition: symbolic.h:401
gymbo::BaseExecutor::optimizer
GDOptimizer optimizer
Definition: symbolic.h:398
gymbo::BaseExecutor::maxSAT
int maxSAT
The maximum number of SAT constraints to collect.
Definition: symbolic.h:400
gymbo::BaseExecutor::verbose_level
int verbose_level
The level of verbosity.
Definition: symbolic.h:404
gymbo::BaseExecutor::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.
Definition: symbolic.h:429
gymbo::BaseExecutor::use_dpll
bool use_dpll
Definition: symbolic.h:407
gymbo::PSExecutor
Represents a derived class for symbolic execution engine for probabilistic programs.
Definition: psymbolic.h:132
gymbo::PSExecutor::random_vars
std::unordered_set< int > random_vars
Set of random variables'IDs.
Definition: psymbolic.h:133
gymbo::PSExecutor::run
Trace run(Prog &prog, std::unordered_set< int > &target_pcs, SymState &state, int maxDepth=256)
Run probabilistic symbolic execution on a program.
Definition: psymbolic.h:235
gymbo::PSExecutor::constraints_cache
PathConstraintsTable constraints_cache
Cache for storing and reusing path constraints.
Definition: psymbolic.h:135
gymbo::PSExecutor::register_random_var
void register_random_var(int var_id)
Definition: psymbolic.h:142
gymbo::PSExecutor::prob_constraints_table
ProbPathConstraintsTable prob_constraints_table
Definition: psymbolic.h:137
gymbo::PSExecutor::solve
bool solve(bool is_target, int pc, SymState &state)
Solves path constraints and updates the symbolic state.
Definition: psymbolic.h:157
gymbo::SymProb
Represents a symbolic probability with a numerator and denominator.
Definition: type.h:878
gymbo::SymProb::toString
std::string toString()
Converts SymProb to a string.
Definition: type.h:910
gymbo::SymProb::pmul
SymProb * pmul(SymProb *other)
Multiplies two SymProb instances.
Definition: type.h:940
gymbo::SymState
Struct representing the symbolic state of the symbolic execution.
Definition: type.h:1042
gymbo::SymState::p
SymProb * p
Definition: type.h:1050
gymbo::SymState::cond_p
SymProb * cond_p
Definition: type.h:1051
gymbo::SymState::has_observed_p_cond
bool has_observed_p_cond
Definition: type.h:1055
gymbo::SymState::path_constraints
std::vector< Sym > path_constraints
Definition: type.h:1049
gymbo::SymState::pc
int pc
Definition: type.h:1043
gymbo::SymState::toString
std::string toString(bool include_memory=true) const
Returns the human-redable string representation of concrete memory, symbolic memory and path constrai...
Definition: type.h:1119
gymbo::SymState::mem
Mem mem
Definition: type.h:1045
gymbo::Sym
Struct representing a symbolic expression.
Definition: type.h:265
gymbo::Sym::copy
Sym * copy()
Definition: type.h:319
gymbo::Trace
Struct representing a trace in symbolic execution.
Definition: type.h:1210
symbolic.h
Core implementation of gradient-based symbolic execution.