CBMC
expr_enumerator.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 Module: Enumerator Interface
3 Author: Qinheping Hu
4 \*******************************************************************/
5 
6 #include "expr_enumerator.h"
7 
8 #include <util/bitvector_types.h>
9 #include <util/format_expr.h>
10 #include <util/simplify_expr.h>
11 #include <util/std_expr.h>
12 
13 #include <climits>
14 
15 expr_sett leaf_enumeratort::enumerate(const std::size_t size) const
16 {
17  // Size of leaf expressions must be 1.
18  if(size != 1)
19  return {};
20 
21  return leaf_exprs;
22 }
23 
24 expr_sett non_leaf_enumeratort::enumerate(const std::size_t size) const
25 {
26  expr_sett result;
27 
28  // Enumerate nothing when `size` is too small to be partitioned.
29  if(size - 1 < arity)
30  return result;
31 
32  // For every possible partition, set `size` of
33  // each sub-enumerator to be the corresponding component in the partition.
34  for(const auto &partition : get_partitions(size - 1, arity))
35  {
36  if(!is_good_partition(partition))
37  continue;
38 
39  // Compute the Cartesian product as result.
40  for(const auto &product_tuple : cartesian_product_of_enumerators(
42  sub_enumerators.begin(),
43  partition,
44  partition.begin()))
45  {
46  // Optimization: rule out equivalent expressions
47  // using certain equivalence class.
48  // Keep only representation tuple of each equivalence class.
49  if(is_equivalence_class_representation(product_tuple))
50  result.insert(simplify_expr(instantiate(product_tuple), ns));
51  }
52  }
53 
54  return result;
55 }
56 
58  const enumeratorst &enumerators,
59  const enumeratorst::const_iterator &it_enumerators,
60  const partitiont &partition,
61  const partitiont::const_iterator &it_partition) const
62 {
63  INVARIANT(
64  std::distance(it_enumerators, enumerators.end()) ==
65  std::distance(it_partition, partition.end()),
66  "Partition should have the same size as enumerators.");
67 
68  std::set<expr_listt> result;
69 
70  if(std::next(it_enumerators) == enumerators.end())
71  {
74  for(const auto &e : enumerators.back()->enumerate(*it_partition))
75  {
76  result.insert({e});
77  }
78  }
79  else
80  {
84  for(const auto &sub_tuple : cartesian_product_of_enumerators(
85  enumerators,
86  std::next(it_enumerators),
87  partition,
88  std::next(it_partition)))
89  {
90  for(const auto &elem : (*it_enumerators)->enumerate(*it_partition))
91  {
92  expr_listt new_tuple(sub_tuple);
93  new_tuple.emplace_front(elem);
94  result.insert(new_tuple);
95  }
96  }
97  }
98  return result;
99 }
100 
101 std::list<partitiont>
102 get_partitions_long(const std::size_t n, const std::size_t k)
103 {
104  std::list<partitiont> result;
105  // Cuts are an increasing vector of distinct indexes between 0 and n.
106  // Note that cuts[0] is always 0 and cuts[k+1] is always n.
107  // There is a bijection between partitions and cuts, i.e., for a given cuts,
108  // (cuts[1]-cuts[0], cuts[2]-cuts[1], ..., cuts[k+1]-cuts[k])
109  // is a partition of n into k components.
110  std::vector<std::size_t> cuts;
111 
112  // Initialize cuts as (0, n-k+1, n-k+2, ..., n).
113  // O: elements
114  // |: cuts
115  // Initial cuts
116  // 000...0111...1
117  // So the first partition is (n-k+1, 1, 1, ..., 1).
118  cuts.emplace_back(0);
119  cuts.emplace_back(n - k + 1);
120  for(std::size_t i = 0; i < k - 1; i++)
121  {
122  cuts.emplace_back(n - k + 2 + i);
123  }
124 
125  // Done when all cuts were enumerated.
126  bool done = false;
127 
128  while(!done)
129  {
130  // Construct a partition from cuts using the bijection described above.
131  partitiont new_partition = partitiont();
132  for(std::size_t i = 1; i < k + 1; i++)
133  {
134  new_partition.emplace_back(cuts[i] - cuts[i - 1]);
135  }
136 
137  // We move to the next cuts. The idea is that
138  // 1. we first find the largest index i such that there are space before
139  // cuts[i] where cuts[i] can be moved to;
140  // The index i is the rightmost index we move in this iteration.
141  // 2. we then move cuts[i] to its left by 1;
142  // 3. move all cuts next to cuts[rightmost_to_move].
143  //
144  // O: filler
145  // |: cuts
146  //
147  // Example:
148  // Before moving:
149  // 00000010010111110
150  // ^
151  // rightmost_to_move
152  std::size_t rightmost_to_move = 0;
153  for(std::size_t i = 1; i < k; i++)
154  {
155  if(cuts[i] - cuts[i - 1] > 1)
156  {
157  rightmost_to_move = i;
158  }
159  }
160 
161  // Move cuts[rightmost_to_move] to its left:
162  // 00000010011011110
163  // ^
164  // rightmost_to_move
165  cuts[rightmost_to_move] = cuts[rightmost_to_move] - 1;
166 
167  // No cut can be moved---we have enumerated all cuts.
168  if(rightmost_to_move == 0)
169  done = true;
170  else
171  {
172  // Move all cuts (except for cuts[0]) after rightmost_to_move to their
173  // rightmost.
174  // 00000010011001111
175  // ^
176  // rightmost_to_move
177  std::size_t accum = 1;
178  for(std::size_t i = k - 1; i > rightmost_to_move; i--)
179  {
180  cuts[i] = n - accum;
181  accum++;
182  }
183  }
184  result.emplace_back(new_partition);
185  }
186  return result;
187 }
188 
190 std::vector<std::size_t> get_ones_pos(std::size_t v)
191 {
192  const std::size_t length = sizeof(std::size_t) * CHAR_BIT;
193  std::vector<std::size_t> result;
194 
195  // Start from the lowest bit at position `length`
196  std::size_t curr_pos = length;
197  while(v != 0)
198  {
199  if(v % 2)
200  {
201  result.insert(result.begin(), curr_pos);
202  }
203 
204  // Move to the next bit.
205  v = v >> 1;
206  curr_pos--;
207  }
208 
209  return result;
210 }
211 
217 partitiont from_bits_to_partition(std::size_t v, std::size_t n)
218 {
219  const std::vector<std::size_t> ones_pos = get_ones_pos(v);
220 
221  INVARIANT(ones_pos.size() >= 1, "There should be at least one bit set in v");
222 
223  partitiont result = {ones_pos[0]};
224 
225  for(std::size_t i = 1; i < ones_pos.size(); i++)
226  {
227  result.emplace_back(ones_pos[i] - ones_pos[i - 1]);
228  }
229  result.emplace_back(n - ones_pos[ones_pos.size() - 1]);
230 
231  return result;
232 }
233 
235  const std::size_t n,
236  const std::size_t k) const
237 {
238  // Every component should contain at least one element.
239  if(n < k)
240  return {};
241 
242  // Number of bits at all.
243  const std::size_t length = sizeof(std::size_t) * CHAR_BIT;
244 
245  // This bithack-based implementation works only for `n` no larger than
246  // `length`. Use the vector-based implementation `n` is too large.
247  if(n > length)
248  return get_partitions_long(n, k);
249 
250  // We enumerate all bit vectors `v` with k-1 one's such that each component
251  // corresponds to one unique partition.
252  // For a bit vector with ones at positions (computed by `get_ones_pos`)
253  // (ones[0], ones[1], ..., ones[k-2]),
254  // the corresponding partition is
255  // (ones[0], ones[1]-ones[0], ..., ones[k-2]-ones[k-3], n-ones[k-2]).
256 
257  // Initial `v` is with ones at positions (n-k+1, n-k+2, ..., n-2, n-1).
258  std::size_t v = 0;
259  // Initial `end` (the last bit vector we enumerate) is with ones at
260  // positions (1, 2, 3, ..., k-1).
261  std::size_t end = 0;
262  for(size_t i = 0; i < k - 1; i++)
263  {
264  v++;
265  v = v << 1;
266  end++;
267  end = end << 1;
268  }
269  v = v << (length - n);
270  end = end << (length - k);
271 
272  std::list<partitiont> result;
273  while(v != end)
274  {
275  // Construct the partition for current bit vector and add it to `result`
276  result.emplace_back(from_bits_to_partition(v, n));
277 
278  // https://graphics.stanford.edu/~seander/bithacks.html#NextBitPermutation
279  // Compute the lexicographically next bit permutation.
280  std::size_t t = (v | (v - 1)) + 1;
281  v = t | ((((t & -t) / (v & -v)) >> 1) - 1);
282  }
283  result.emplace_back(from_bits_to_partition(v, n));
284 
285  return result;
286 }
287 
289 {
290  return op_id == ID_equal || op_id == ID_plus || op_id == ID_notequal ||
291  op_id == ID_or || op_id == ID_and || op_id == ID_xor ||
292  op_id == ID_bitand || op_id == ID_bitor || op_id == ID_bitxor ||
293  op_id == ID_mult;
294 }
295 
297  const expr_listt &exprs) const
298 {
299  std::stringstream left, right;
300  left << format(exprs.front());
301  right << format(exprs.back());
302  // When the two sub-enumerators are exchangeable---they enumerate the same
303  // set of expressions---, and the operator is commutative, `exprs` is a
304  // representation if its sub-expressions are sorted.
305  if(is_exchangeable && is_commutative(op_id) && left.str() > right.str())
306  {
307  return false;
308  }
309 
311  return true;
312 }
313 
314 // Handle mix of unsigned and signed leafs in one expression.
315 // From the C99 standard, section 6.3.1.8:
316 // "if the operand that has unsigned integer type has rank greater or equal to
317 // the rank of the type of the other operand, then the operand with signed
318 // integer type is converted to the type of the operand with unsigned integer
319 // type."
320 static std::pair<const exprt, const exprt>
321 widen_bitvector(const exprt &lhs, const exprt &rhs)
322 {
323  // Widening conversion.
324  if(
325  lhs.type() != rhs.type() &&
326  (lhs.type().id() == ID_unsignedbv || lhs.type().id() == ID_signedbv) &&
327  (rhs.type().id() == ID_unsignedbv || rhs.type().id() == ID_signedbv))
328  {
329  const auto &lhs_type = type_try_dynamic_cast<bitvector_typet>(lhs.type());
330  const auto &rhs_type = type_try_dynamic_cast<bitvector_typet>(rhs.type());
331 
332  // Same rank, unsigned win.
333  if(lhs_type->get_width() == rhs_type->get_width())
334  {
335  if((lhs.type().id() == ID_unsignedbv || rhs.type().id() == ID_unsignedbv))
336  {
337  return std::pair<const exprt, const exprt>(
339  lhs, unsignedbv_typet(lhs_type->get_width())),
341  rhs, unsignedbv_typet(lhs_type->get_width())));
342  }
343  else
344  {
345  return std::pair<const exprt, const exprt>(
347  lhs, signedbv_typet(lhs_type->get_width())),
349  rhs, signedbv_typet(lhs_type->get_width())));
350  }
351  }
352 
353  // Different rank, higher rank win.
354  if(lhs_type->get_width() > rhs_type->get_width())
355  {
356  return std::pair<const exprt, const exprt>(
357  lhs, typecast_exprt::conditional_cast(rhs, *lhs_type));
358  }
359  else
360  {
361  return std::pair<const exprt, const exprt>(
362  typecast_exprt::conditional_cast(lhs, *rhs_type), rhs);
363  }
364  }
365  // no need of bitvector conversion.
366  else
367  {
368  return std::pair<const exprt, const exprt>(lhs, rhs);
369  }
370 }
371 
373 {
374  INVARIANT(
375  exprs.size() == 2,
376  "number of arguments should be 2: " + integer2string(exprs.size()));
377 
378  // Make two operands the same type if they are of different bitvector types.
379  auto operands = widen_bitvector(exprs.front(), exprs.back());
380 
381  if(op_id == ID_equal)
382  return equal_exprt(operands.first, operands.second);
383  if(op_id == ID_notequal)
384  return notequal_exprt(operands.first, operands.second);
385  if(op_id == ID_le)
386  return less_than_or_equal_exprt(operands.first, operands.second);
387  if(op_id == ID_lt)
388  return less_than_exprt(operands.first, operands.second);
389  if(op_id == ID_gt)
390  return greater_than_exprt(operands.first, operands.second);
391  if(op_id == ID_ge)
392  return greater_than_or_equal_exprt(operands.first, operands.second);
393  if(op_id == ID_and)
394  return and_exprt(exprs.front(), exprs.back());
395  if(op_id == ID_or)
396  return or_exprt(exprs.front(), exprs.back());
397  if(op_id == ID_plus)
398  return plus_exprt(operands.first, operands.second);
399  if(op_id == ID_minus)
400  return minus_exprt(operands.first, operands.second);
401 
402  return binary_exprt(operands.first, op_id, operands.second);
403 }
404 
405 expr_sett alternatives_enumeratort::enumerate(const std::size_t size) const
406 {
407  expr_sett result;
408  for(const auto &enumerator : sub_enumerators)
409  {
410  for(const auto &e : enumerator->enumerate(size))
411  {
412  result.insert(e);
413  }
414  }
415  return result;
416 }
417 
418 expr_sett
419 recursive_enumerator_placeholdert::enumerate(const std::size_t size) const
420 {
421  const auto &it = factory.productions_map.find(identifier);
422  INVARIANT(it != factory.productions_map.end(), "No nonterminal found.");
423  alternatives_enumeratort actual_enumerator(it->second, ns);
424  return actual_enumerator.enumerate(size);
425 }
426 
428  const recursive_enumerator_placeholdert &placeholder)
429 {
430  // The new placeholder (nonterminal) belongs to this factory (grammar).
431  const auto &ret = nonterminal_set.insert(placeholder.identifier);
432  INVARIANT(ret.second, "Duplicated non-terminals");
433 }
434 
436  const std::string &id,
437  const enumeratorst &enumerators)
438 {
439  const auto &ret = productions_map.insert({id, enumerators});
440  INVARIANT(
441  ret.second, "Cannot attach enumerators to a non-existing nonterminal.");
442 }
std::list< exprt > expr_listt
Pre-defined bitvector types.
Enumerators that enumerates expressions in the union of enumerated expressions of sub-enumerators.
const enumeratorst sub_enumerators
expr_sett enumerate(const std::size_t size) const override
Boolean AND.
Definition: std_expr.h:2120
A base class for binary expressions.
Definition: std_expr.h:638
bool is_equivalence_class_representation(const expr_listt &exprs) const override
Determine whether a tuple of expressions is the representation of some equivalence class.
exprt instantiate(const expr_listt &exprs) const override
Combine a list of sub-expressions to construct the top-level expression.
bool is_commutative(const irep_idt &op) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
const namespacet & ns
void add_placeholder(const recursive_enumerator_placeholdert &placeholder)
Add a new placeholder/nonterminal to the grammar.
std::set< std::string > nonterminal_set
Set of nonterminals in the grammar.
std::map< std::string, const enumeratorst > productions_map
Map from names of nonterminals to rhs of productions with lhs being them.
void attach_productions(const std::string &id, const enumeratorst &enumerators)
Attach enumerators to the placeholder with id.
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
Binary greater than operator expression.
Definition: std_expr.h:807
Binary greater than or equal operator expression.
Definition: std_expr.h:828
const irep_idt & id() const
Definition: irep.h:388
expr_sett enumerate(const std::size_t size) const override
Enumerate expressions in the set of leaf_exprs.
const expr_sett leaf_exprs
Binary less than operator expression.
Definition: std_expr.h:849
Binary less than or equal operator expression.
Definition: std_expr.h:870
Binary minus.
Definition: std_expr.h:1061
expr_sett enumerate(const std::size_t size) const override
const std::size_t arity
std::list< partitiont > get_partitions(const std::size_t n, const std::size_t k) const
Enumerate all partitions of n into k components.
virtual exprt instantiate(const expr_listt &exprs) const =0
Combine a list of sub-expressions to construct the top-level expression.
const std::function< bool(const partitiont &)> is_good_partition
const enumeratorst sub_enumerators
std::set< expr_listt > cartesian_product_of_enumerators(const enumeratorst &enumerators, const enumeratorst::const_iterator &it, const partitiont &partition, const partitiont::const_iterator &it_partition) const
Given a list enumerators of enumerators, return the Cartesian product of expressions enumerated by ea...
virtual bool is_equivalence_class_representation(const expr_listt &es) const
As default, keep all expression tuples.
Disequality.
Definition: std_expr.h:1420
Boolean OR.
Definition: std_expr.h:2228
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
Placeholders for actual enumerators, which represent nonterminals.
const enumerator_factoryt & factory
expr_sett enumerate(const std::size_t size) const override
Fixed-width bit-vector with two's complement interpretation.
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
Fixed-width bit-vector with unsigned binary interpretation.
std::unordered_set< exprt, irep_hash > expr_sett
std::list< partitiont > get_partitions_long(const std::size_t n, const std::size_t k)
static std::pair< const exprt, const exprt > widen_bitvector(const exprt &lhs, const exprt &rhs)
partitiont from_bits_to_partition(std::size_t v, std::size_t n)
Construct partition of n elements from a bit vector v.
std::vector< std::size_t > get_ones_pos(std::size_t v)
Compute all positions of ones in the bit vector v (1-indexed).
Enumerator Interface.
std::list< const enumerator_baset * > enumeratorst
std::list< std::size_t > partitiont
static format_containert< T > format(const T &o)
Definition: format.h:37
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
exprt simplify_expr(exprt src, const namespacet &ns)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
API to expression classes.