CBMC
boolbv_mult.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <util/bitvector_types.h>
12 
14 {
15  std::size_t width=boolbv_width(expr.type());
16 
17  bvt bv;
18  bv.resize(width);
19 
20  const exprt::operandst &operands=expr.operands();
21  DATA_INVARIANT(!operands.empty(), "multiplication must have operands");
22 
23  const exprt &op0=expr.op0();
24 
26  op0.type() == expr.type(),
27  "multiplication operands should have same type as expression");
28 
29  if(expr.type().id()==ID_fixedbv)
30  {
31  bv = convert_bv(op0, width);
32 
33  std::size_t fraction_bits=
35 
36  for(exprt::operandst::const_iterator it=operands.begin()+1;
37  it!=operands.end(); it++)
38  {
40  it->type() == expr.type(),
41  "multiplication operands should have same type as expression");
42 
43  // do a sign extension by fraction_bits bits
44  bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
45 
46  bvt op = convert_bv(*it, width);
47 
48  op=bv_utils.sign_extension(op, bv.size());
49 
50  bv=bv_utils.signed_multiplier(bv, op);
51 
52  // cut it down again
53  bv.erase(bv.begin(), bv.begin()+fraction_bits);
54  }
55 
56  return bv;
57  }
58  else if(expr.type().id()==ID_unsignedbv ||
59  expr.type().id()==ID_signedbv)
60  {
62  expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
64 
65  bv = convert_bv(op0, width);
66 
67  for(exprt::operandst::const_iterator it=operands.begin()+1;
68  it!=operands.end(); it++)
69  {
71  it->type() == expr.type(),
72  "multiplication operands should have same type as expression");
73 
74  const bvt &op = convert_bv(*it, width);
75 
76  bv = bv_utils.multiplier(bv, op, rep);
77  }
78 
79  return bv;
80  }
81 
82  return conversion_failed(expr);
83 }
Pre-defined bitvector types.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:37
virtual bvt convert_mult(const mult_exprt &expr)
Definition: boolbv_mult.cpp:13
bv_utilst bv_utils
Definition: boolbv.h:116
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:83
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:101
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:1003
representationt
Definition: bv_utils.h:28
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:1069
static bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:182
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
std::size_t get_fraction_bits() const
const irep_idt & id() const
Definition: irep.h:384
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1107
exprt & op0()
Definition: std_expr.h:932
std::vector< literalt > bvt
Definition: literal.h:201
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534