libTriton version 1.0 build 1588
Loading...
Searching...
No Matches
bitwuzlaSolver.cpp
Go to the documentation of this file.
1
2/*
3** Copyright (C) - Triton
4**
5** This program is under the terms of the Apache License 2.0.
6*/
7
8#include <fstream>
9#include <regex>
10#include <string>
11
12#include <triton/astContext.hpp>
14#include <triton/exceptions.hpp>
20
21
22namespace triton {
23 namespace engines {
24 namespace solver {
25
27 this->timeout = 0;
28 this->memoryLimit = 0;
29
30 // Set bitwuzla abort function.
31 bitwuzla_set_abort_callback(this->abortCallback);
32 }
33
34
35 int32_t BitwuzlaSolver::terminateCallback(void* state) {
36 auto p = reinterpret_cast<SolverParams*>(state);
37
38 // Count elapsed time.
39 auto delta = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::system_clock::now() - p->start).count();
40
41 // Check timeout expired.
42 if (p->timeout && delta > p->timeout) {
44 return 1;
45 }
46
47 // Check memory limit.
48 #if defined(__unix__)
49
50 // Complete seconds elapsed from the start of solving.
51 auto delta_s = delta / 1000;
52
53 // Check memory limit every second. Don't perform check in first 100ms of solving.
54 if (p->memory_limit && delta > 100 && delta_s > p->last_mem_check) {
55 p->last_mem_check = delta_s;
56
57 // Parse system file to get current process memory consumption (VmRSS field).
58 size_t memory_usage = 0;
59 std::ifstream str("/proc/self/status");
60 if (str.is_open()) {
61 std::string line;
62 static std::regex vmsize("VmRSS:\\s*([0-9]+)\\s*kB");
63 while (std::getline(str, line)) {
64 std::smatch match;
65 if (std::regex_match(line, match, vmsize)) {
66 memory_usage = strtoul(match.str(1).c_str(), NULL, 10) / 1024;
67 break;
68 }
69 }
70 }
71 if (!memory_usage) {
72 return 0;
73 }
74 if (memory_usage > p->memory_limit) {
76 return 1;
77 }
78 }
79 #endif
80
81 return 0;
82 }
83
84
85 void BitwuzlaSolver::abortCallback(const char* msg) {
87 }
88
89
90 std::vector<std::unordered_map<triton::usize, SolverModel>> BitwuzlaSolver::getModels(const triton::ast::SharedAbstractNode& node,
91 triton::uint32 limit,
93 triton::uint32 timeout,
94 triton::uint32* solvingTime) const {
95 if (node == nullptr)
96 throw triton::exceptions::SolverEngine("BitwuzlaSolver::getModels(): Node cannot be null.");
97
98 if (node->isLogical() == false)
99 throw triton::exceptions::SolverEngine("BitwuzlaSolver::getModels(): Must be a logical node.");
100
101 // Create solver.
102 auto bzla = bitwuzla_new();
103 bitwuzla_set_option(bzla, BITWUZLA_OPT_PRODUCE_MODELS, 1);
104 if (limit > 1) {
105 bitwuzla_set_option(bzla, BITWUZLA_OPT_INCREMENTAL, 1);
106 }
107
108 // Convert Triton' AST to solver terms.
109 auto bzlaAst = triton::ast::TritonToBitwuzla();
110 bitwuzla_assert(bzla, bzlaAst.convert(node, bzla));
111
112 // Set solving params.
113 SolverParams p(this->timeout, this->memoryLimit);
114 if (this->timeout || this->memoryLimit) {
115 bitwuzla_set_termination_callback(bzla, this->terminateCallback, reinterpret_cast<void*>(&p));
116 }
117
118 // Get time of solving start.
119 auto start = std::chrono::system_clock::now();
120
121 // Check result.
122 auto res = bitwuzla_check_sat(bzla);
123
124 // Write back status.
125 if (status) {
126 switch (res) {
127 case BITWUZLA_SAT:
129 break;
130 case BITWUZLA_UNSAT:
132 break;
133 case BITWUZLA_UNKNOWN:
134 *status = p.status;
135 break;
136 }
137 }
138
139 std::vector<std::unordered_map<triton::usize, SolverModel>> ret;
140 while(res == BITWUZLA_SAT && limit >= 1) {
141 std::vector<const BitwuzlaTerm*> solution;
142 solution.reserve(bzlaAst.getVariables().size());
143
144 // Parse model.
145 std::unordered_map<triton::usize, SolverModel> model;
146 for (const auto& it : bzlaAst.getVariables()) {
147 const char* svalue = bitwuzla_get_bv_value(bzla, it.first);
148 auto value = this->fromBvalueToUint512(svalue);
149 auto m = SolverModel(it.second, value);
150 model[m.getId()] = m;
151
152 // Negate current model to escape duplication in the next solution.
153 const auto& symvar_sort = bzlaAst.getBitvectorSorts().at(it.second->getSize());
154 auto cur_val = bitwuzla_mk_bv_value(bzla, symvar_sort, svalue, BITWUZLA_BV_BASE_BIN);
155 auto n = bitwuzla_mk_term2(bzla, BITWUZLA_KIND_EQUAL, it.first, cur_val);
156 solution.push_back(bitwuzla_mk_term1(bzla, BITWUZLA_KIND_NOT, n));
157 }
158
159 // Check that model is available.
160 if (model.empty()) {
161 break;
162 }
163
164 // Push model.
165 ret.push_back(model);
166
167 if (--limit) {
168 // Escape last model.
169 if (solution.size() > 1) {
170 bitwuzla_assert(bzla, bitwuzla_mk_term(bzla, BITWUZLA_KIND_OR, solution.size(), solution.data()));
171 }
172 else {
173 bitwuzla_assert(bzla, solution.front());
174 }
175
176 // Get next model.
177 res = bitwuzla_check_sat(bzla);
178 }
179 }
180
181 // Get time of solving end.
182 auto end = std::chrono::system_clock::now();
183
184 if (solvingTime)
185 *solvingTime = std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count();
186
187 bitwuzla_delete(bzla);
188
189 return ret;
190 }
191
192
195
196 this->getModels(node, 0, &st, timeout, solvingTime);
197
198 if (status) {
199 *status = st;
200 }
201 return st == triton::engines::solver::SAT;
202 }
203
204
205 std::unordered_map<triton::usize, SolverModel> BitwuzlaSolver::getModel(const triton::ast::SharedAbstractNode& node, triton::engines::solver::status_e* status, triton::uint32 timeout, triton::uint32* solvingTime) const {
206 auto models = this->getModels(node, 1, status, timeout, solvingTime);
207 return models.empty() ? std::unordered_map<triton::usize, SolverModel>() : models.front();
208 }
209
210
212 if (node == nullptr) {
213 throw triton::exceptions::AstLifting("BitwuzlaSolver::evaluate(): node cannot be null.");
214 }
215
216 auto bzla = bitwuzla_new();
217 bitwuzla_set_option(bzla, BITWUZLA_OPT_PRODUCE_MODELS, 1);
218
219 // Query check-sat on empty solver to put Bitwuzla in SAT-state. Thus, it should be able to evaluate concrete formulas.
220 if (bitwuzla_check_sat(bzla) != BITWUZLA_SAT) {
221 bitwuzla_delete(bzla);
222 throw triton::exceptions::SolverEngine("BitwuzlaSolver::evaluate(): empty solver didn't return SAT.");
223 }
224
225 // Evaluate concrete AST in solver.
226 auto bzlaAst = triton::ast::TritonToBitwuzla(true);
227 auto bv_value = bitwuzla_get_bv_value(bzla, bitwuzla_get_value(bzla, bzlaAst.convert(node, bzla)));
228 auto res = this->fromBvalueToUint512(bv_value);
229
230 bitwuzla_delete(bzla);
231 return res;
232 }
233
234
235 std::string BitwuzlaSolver::getName(void) const {
236 return "Bitwuzla";
237 }
238
239
241 this->timeout = ms;
242 }
243
244
246 this->memoryLimit = limit;
247 }
248
249
250 triton::uint512 BitwuzlaSolver::fromBvalueToUint512(const char* value) const {
251 triton::usize len = strlen(value);
252 triton::usize pos = 0;
253 triton::uint512 res = 0;
254
255 // Convert short bitvector string directly.
256 if (len <= 64) {
257 return std::strtoull(value, 0, 2L);
258 }
259
260 // Convert long bitvector string by 64-bit chunks.
261 while (pos < len) {
262 triton::usize sublen = std::min(len - pos, (triton::usize) 64UL);
263 char* substr = new char[sublen + 1];
264 std::memcpy(substr, value + pos, sublen);
265 substr[sublen] = '\0';
266 res = (res << sublen) + std::strtoull(substr, 0, 2L);
267 pos += sublen;
268 delete[] substr;
269 }
270
271 return res;
272 }
273
274 };
275 };
276};
Converts a Triton's AST to Bitwuzla's AST.
TRITON_EXPORT std::unordered_map< triton::usize, SolverModel > getModel(const triton::ast::SharedAbstractNode &node, triton::engines::solver::status_e *status=nullptr, triton::uint32 timeout=0, triton::uint32 *solvingTime=nullptr) const
Computes and returns a model from a symbolic constraint.
TRITON_EXPORT std::string getName(void) const
Returns the name of this solver.
TRITON_EXPORT std::vector< std::unordered_map< triton::usize, SolverModel > > getModels(const triton::ast::SharedAbstractNode &node, triton::uint32 limit, triton::engines::solver::status_e *status=nullptr, triton::uint32 timeout=0, triton::uint32 *solvingTime=nullptr) const
Computes and returns several models from a symbolic constraint. The limit is the number of models ret...
TRITON_EXPORT BitwuzlaSolver()
Constructor.
TRITON_EXPORT triton::uint512 evaluate(const triton::ast::SharedAbstractNode &node) const
Evaluates a Triton's AST via Bitwuzla and returns a concrete value.
TRITON_EXPORT void setTimeout(triton::uint32 ms)
Defines a solver timeout (in milliseconds).
TRITON_EXPORT void setMemoryLimit(triton::uint32 mem)
Defines a solver memory consumption limit (in megabytes).
static void abortCallback(const char *msg)
Callback function that implements aborting of Bitwuzla solver with throwing exception.
static int32_t terminateCallback(void *state)
Callback function that implements termination of Bitwuzla solver on timeout and memory limit.
TRITON_EXPORT bool isSat(const triton::ast::SharedAbstractNode &node, triton::engines::solver::status_e *status=nullptr, triton::uint32 timeout=0, triton::uint32 *solvingTime=nullptr) const
Returns true if an expression is satisfiable.
This class is used to represent a constraint model solved.
Definition: solverModel.hpp:42
The exception class used by all AST lifting (e.g z3 <-> triton).
Definition: exceptions.hpp:413
The exception class used by the solver engine.
Definition: exceptions.hpp:185
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition: ast.hpp:59
std::size_t usize
unsigned MAX_INT 32 or 64 bits according to the CPU.
std::uint32_t uint32
unisgned 32-bits
Definition: tritonTypes.hpp:39
The Triton namespace.