1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     bv_size_reduction_tactic.cpp
7 
8 Abstract:
9 
10     Reduce the number of bits used to encode constants, by using signed bounds.
11     Example: suppose x is a bit-vector of size 8, and we have
12     signed bounds for x such that:
13         -2 <= x <= 2
14     Then, x can be replaced by  ((sign-extend 5) k)
15     where k is a fresh bit-vector constant of size 3.
16 
17 Author:
18 
19     Leonardo (leonardo) 2012-02-19
20 
21 Notes:
22 
23 --*/
24 #include "tactic/tactical.h"
25 #include "ast/bv_decl_plugin.h"
26 #include "ast/rewriter/expr_replacer.h"
27 #include "tactic/generic_model_converter.h"
28 #include "ast/ast_smt2_pp.h"
29 
30 namespace {
31 class bv_size_reduction_tactic : public tactic {
32     typedef rational numeral;
33     typedef generic_model_converter bv_size_reduction_mc;
34 
35     ast_manager &             m;
36     bv_util                   m_util;
37     obj_map<app, numeral>     m_signed_lowers;
38     obj_map<app, numeral>     m_signed_uppers;
39     obj_map<app, numeral>     m_unsigned_lowers;
40     obj_map<app, numeral>     m_unsigned_uppers;
41     ref<bv_size_reduction_mc> m_mc;
42     generic_model_converter_ref m_fmc;
43     scoped_ptr<expr_replacer> m_replacer;
44     bool                      m_produce_models;
45 
46 public:
bv_size_reduction_tactic(ast_manager & m)47     bv_size_reduction_tactic(ast_manager & m) :
48         m(m),
49         m_util(m),
50         m_replacer(mk_default_expr_replacer(m, false)) {
51     }
52 
translate(ast_manager & m)53     tactic * translate(ast_manager & m) override {
54         return alloc(bv_size_reduction_tactic, m);
55     }
56 
57     void operator()(goal_ref const & g, goal_ref_buffer & result) override;
58 
cleanup()59     void cleanup() override {
60         m_signed_lowers.reset();
61         m_signed_uppers.reset();
62         m_unsigned_lowers.reset();
63         m_unsigned_uppers.reset();
64         m_mc = nullptr;
65         m_fmc = nullptr;
66         m_replacer->reset();
67     }
68 
update_signed_lower(app * v,numeral const & k)69     void update_signed_lower(app * v, numeral const & k) {
70         // k <= v
71         auto& value = m_signed_lowers.insert_if_not_there(v, k);
72         if (value < k) {
73             // improve bound
74             value = k;
75         }
76     }
77 
update_signed_upper(app * v,numeral const & k)78     void update_signed_upper(app * v, numeral const & k) {
79         // v <= k
80         auto& value = m_signed_uppers.insert_if_not_there(v, k);
81         if (k < value) {
82             // improve bound
83             value = k;
84         }
85     }
86 
update_unsigned_lower(app * v,numeral const & k)87     void update_unsigned_lower(app * v, numeral const & k) {
88         SASSERT(k > numeral(0));
89         // k <= v
90         auto& value = m_unsigned_lowers.insert_if_not_there(v, k);
91         if (value < k) {
92             // improve bound
93             value = k;
94         }
95     }
96 
update_unsigned_upper(app * v,numeral const & k)97     void update_unsigned_upper(app * v, numeral const & k) {
98         SASSERT(k > numeral(0));
99         // v <= k
100         auto& value = m_unsigned_uppers.insert_if_not_there(v, k);
101         if (k < value) {
102             // improve bound
103             value = k;
104         }
105     }
106 
collect_bounds(goal const & g)107     void collect_bounds(goal const & g) {
108         unsigned sz = g.size();
109         numeral  val;
110         unsigned bv_sz;
111         expr * f, * lhs, * rhs;
112         for (unsigned i = 0; i < sz; i++) {
113             bool negated = false;
114             f = g.form(i);
115             if (m.is_not(f)) {
116                 negated = true;
117                 f = to_app(f)->get_arg(0);
118             }
119 
120             if (m_util.is_bv_sle(f, lhs, rhs)) {
121                 bv_sz = m_util.get_bv_size(lhs);
122                 if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
123                     TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
124                     // v <= k
125                     val = m_util.norm(val, bv_sz, true);
126                     if (negated) {
127                         val += numeral(1);
128                         if (m_util.norm(val, bv_sz, true) != val) {
129                             // bound is infeasible.
130                         }
131                         else {
132                             update_signed_lower(to_app(lhs), val);
133                         }
134                     }
135                     else update_signed_upper(to_app(lhs), val);
136                 }
137                 else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) {
138                     TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
139                     // k <= v
140                     val = m_util.norm(val, bv_sz, true);
141                     if (negated) {
142                         val -= numeral(1);
143                         if (m_util.norm(val, bv_sz, true) != val) {
144                             // bound is infeasible.
145                         }
146                         else {
147                             update_signed_upper(to_app(rhs), val);
148                         }
149                     }
150                     else update_signed_lower(to_app(rhs), val);
151                 }
152             }
153 
154 #if 0
155             else if (m_util.is_bv_ule(f, lhs, rhs)) {
156                 if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
157                     TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
158                     // v <= k
159                     if (negated) update_unsigned_lower(to_app(lhs), val+numeral(1));
160                     else update_unsigned_upper(to_app(lhs), val);
161                 }
162                 else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) {
163                     TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
164                     // k <= v
165                     if (negated) update_unsigned_upper(to_app(rhs), val-numeral(1));
166                     else update_unsigned_lower(to_app(rhs), val);
167                 }
168             }
169 #endif
170         }
171     }
172 
checkpoint()173     void checkpoint() {
174         if (!m.inc())
175             throw tactic_exception(m.limit().get_cancel_msg());
176     }
177 
run(goal & g,model_converter_ref & mc)178     void run(goal & g, model_converter_ref & mc) {
179         if (g.inconsistent())
180             return;
181         TRACE("before_bv_size_reduction", g.display(tout););
182         m_produce_models = g.models_enabled();
183         mc = nullptr;
184         m_mc = nullptr;
185         unsigned num_reduced = 0;
186         {
187             tactic_report report("reduce-bv-size", g);
188             collect_bounds(g);
189 
190             // create substitution
191             expr_substitution subst(m);
192 
193             if (!(m_signed_lowers.empty() || m_signed_uppers.empty())) {
194                 TRACE("bv_size_reduction",
195                         tout << "m_signed_lowers: " << std::endl;
196                         for (obj_map<app, numeral>::iterator it = m_signed_lowers.begin(); it != m_signed_lowers.end(); it++)
197                             tout << mk_ismt2_pp(it->m_key, m) << " >= " << it->m_value.to_string() << std::endl;
198                         tout << "m_signed_uppers: " << std::endl;
199                         for (obj_map<app, numeral>::iterator it = m_signed_uppers.begin(); it != m_signed_uppers.end(); it++)
200                             tout << mk_ismt2_pp(it->m_key, m) << " <= " << it->m_value.to_string() << std::endl;
201                         );
202 
203                 obj_map<app, numeral>::iterator it  = m_signed_lowers.begin();
204                 obj_map<app, numeral>::iterator end = m_signed_lowers.end();
205                 for (; it != end; ++it) {
206                     app * v = it->m_key;
207                     unsigned bv_sz = m_util.get_bv_size(v);
208                     numeral l = m_util.norm(it->m_value, bv_sz, true);
209                     obj_map<app, numeral>::obj_map_entry * entry = m_signed_uppers.find_core(v);
210                     if (entry != nullptr) {
211                         numeral u = m_util.norm(entry->get_data().m_value, bv_sz, true);
212                         TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
213                         expr * new_def = nullptr;
214                         app  * new_const = nullptr;
215                         if (l > u) {
216                             g.assert_expr(m.mk_false());
217                             return;
218                         }
219                         else if (l == u) {
220                             new_def = m_util.mk_numeral(l, m.get_sort(v));
221                         }
222                         else {
223                             // l < u
224                             if (l.is_neg()) {
225                                 unsigned l_nb = (-l).get_num_bits();
226                                 unsigned v_nb = m_util.get_bv_size(v);
227 
228                                 if (u.is_neg())
229                                 {
230                                     // l <= v <= u <= 0
231                                     unsigned i_nb = l_nb;
232                                     TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= u <= 0 " << " --> " << i_nb << " bits\n";);
233                                     if (i_nb < v_nb) {
234                                         new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(i_nb));
235                                         new_def = m_util.mk_concat(m_util.mk_numeral(numeral(-1), v_nb - i_nb), new_const);
236                                     }
237                                 }
238                                 else {
239                                     // l <= v <= 0 <= u
240                                     unsigned u_nb = u.get_num_bits();
241                                     unsigned i_nb = ((l_nb > u_nb) ? l_nb : u_nb) + 1;
242                                     TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= 0 <= u " << " --> " << i_nb << " bits\n";);
243                                     if (i_nb < v_nb) {
244                                         new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(i_nb));
245                                         new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
246                                     }
247                                 }
248                             }
249                             else {
250                                 // 0 <= l <= v <= u
251                                 unsigned u_nb = u.get_num_bits();
252                                 unsigned v_nb = m_util.get_bv_size(v);
253                                 TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << " --> " << u_nb << " bits\n";);
254                                 if (u_nb < v_nb) {
255                                     new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(u_nb));
256                                     new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
257                                 }
258                             }
259                         }
260 
261                         if (new_def) {
262                             subst.insert(v, new_def);
263                             if (m_produce_models) {
264                                 if (!m_mc)
265                                     m_mc = alloc(bv_size_reduction_mc, m, "bv_size_reduction");
266                                 m_mc->add(v, new_def);
267                                 if (!m_fmc && new_const)
268                                     m_fmc = alloc(generic_model_converter, m, "bv_size_reduction");
269                                 if (new_const)
270                                     m_fmc->hide(new_const);
271                             }
272                             num_reduced++;
273                         }
274                     }
275                 }
276             }
277 
278 #if 0
279             if (!(m_unsigned_lowers.empty() && m_unsigned_uppers.empty())) {
280                 TRACE("bv_size_reduction",
281                     tout << "m_unsigned_lowers: " << std::endl;
282                     for (obj_map<app, numeral>::iterator it = m_unsigned_lowers.begin(); it != m_unsigned_lowers.end(); it++)
283                         tout << mk_ismt2_pp(it->m_key, m) << " >= " << it->m_value.to_string() << std::endl;
284                     tout << "m_unsigned_uppers: " << std::endl;
285                     for (obj_map<app, numeral>::iterator it = m_unsigned_uppers.begin(); it != m_unsigned_uppers.end(); it++)
286                         tout << mk_ismt2_pp(it->m_key, m) << " <= " << it->m_value.to_string() << std::endl;
287                     );
288 
289                 obj_map<app, numeral>::iterator it  = m_unsigned_uppers.begin();
290                 obj_map<app, numeral>::iterator end = m_unsigned_uppers.end();
291                 for (; it != end; ++it) {
292                     app * v = it->m_key;
293                     unsigned bv_sz = m_util.get_bv_size(v);
294                     numeral u = m_util.norm(it->m_value, bv_sz, false);
295                     obj_map<app, numeral>::obj_map_entry * entry = m_signed_lowers.find_core(v);
296                     numeral l = (entry != 0) ? m_util.norm(entry->get_data().m_value, bv_sz, false) : numeral(0);
297 
298                     obj_map<app, numeral>::obj_map_entry * lse = m_signed_lowers.find_core(v);
299                     obj_map<app, numeral>::obj_map_entry * use = m_signed_uppers.find_core(v);
300                     if ((lse != 0 && lse->get_data().m_value > l) &&
301                         (use != 0 && use->get_data().m_value < u))
302                         continue; // Skip, we had better signed bounds.
303 
304                     if (lse != 0 && lse->get_data().m_value > l) l = lse->get_data().m_value;
305                     if (use != 0 && use->get_data().m_value < u) u = use->get_data().m_value;
306 
307                     TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
308                     expr * new_def = 0;
309                     app * new_const = 0;
310                     if (l > u) {
311                         g.assert_expr(m.mk_false());
312                         return;
313                     }
314                     else if (l == u) {
315                         new_def = m_util.mk_numeral(l, m.get_sort(v));
316                     }
317                     else {
318                         // 0 <= l <= v <= u
319                         unsigned u_nb = u.get_num_bits();
320                         unsigned v_nb = m_util.get_bv_size(v);
321                         if (u_nb < v_nb) {
322                             new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
323                             new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
324                         }
325                     }
326 
327                     if (new_def) {
328                         subst.insert(v, new_def);
329                         if (m_produce_models) {
330                             if (!m_mc)
331                                 m_mc = alloc(bv_size_reduction_mc, m);
332                             m_mc->insert(v->get_decl(), new_def);
333                             if (!m_fmc && new_const)
334                                 m_fmc = alloc(generic_model_converter, m, "bv_size_reduction");
335                             if (new_const)
336                                 m_fmc->hide(new_const);
337                         }
338                         num_reduced++;
339                         TRACE("bv_size_reduction", tout << "New definition = " << mk_ismt2_pp(new_def, m) << "\n";);
340                     }
341                 }
342             }
343 #endif
344 
345             if (subst.empty())
346                 return;
347 
348             m_replacer->set_substitution(&subst);
349 
350             unsigned sz = g.size();
351             expr * f;
352             expr_ref new_f(m);
353             for (unsigned i = 0; i < sz; i++) {
354                 if (g.inconsistent())
355                     return;
356                 f = g.form(i);
357                 (*m_replacer)(f, new_f);
358                 g.update(i, new_f);
359             }
360             mc   = m_mc.get();
361             if (m_fmc) {
362                 mc = concat(m_fmc.get(), mc.get());
363             }
364             m_mc = nullptr;
365             m_fmc = nullptr;
366         }
367         report_tactic_progress(":bv-reduced", num_reduced);
368         TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout););
369     }
370 
371 };
372 
operator ()(goal_ref const & g,goal_ref_buffer & result)373 void bv_size_reduction_tactic::operator()(goal_ref const & g,
374                                           goal_ref_buffer & result) {
375     fail_if_proof_generation("bv-size-reduction", g);
376     fail_if_unsat_core_generation("bv-size-reduction", g);
377     TRACE("goal", g->display(tout););
378     result.reset();
379     model_converter_ref mc;
380     run(*(g.get()), mc);
381     g->inc_depth();
382     g->add(mc.get());
383     result.push_back(g.get());
384 }
385 }
386 
mk_bv_size_reduction_tactic(ast_manager & m,params_ref const & p)387 tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p) {
388     return clean(alloc(bv_size_reduction_tactic, m));
389 }
390