cprover
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/std_types.h>
12 
14 {
15  std::size_t width=boolbv_width(expr.type());
16 
17  if(width==0)
18  return conversion_failed(expr);
19 
20  bvt bv;
21  bv.resize(width);
22 
23  const exprt::operandst &operands=expr.operands();
24  DATA_INVARIANT(!operands.empty(), "multiplication must have operands");
25 
26  const exprt &op0=expr.op0();
27 
29  op0.type() == expr.type(),
30  "multiplication operands should have same type as expression");
31 
32  if(expr.type().id()==ID_fixedbv)
33  {
34  bv = convert_bv(op0, width);
35 
36  std::size_t fraction_bits=
37  to_fixedbv_type(expr.type()).get_fraction_bits();
38 
39  for(exprt::operandst::const_iterator it=operands.begin()+1;
40  it!=operands.end(); it++)
41  {
43  it->type() == expr.type(),
44  "multiplication operands should have same type as expression");
45 
46  // do a sign extension by fraction_bits bits
47  bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
48 
49  bvt op = convert_bv(*it, width);
50 
51  op=bv_utils.sign_extension(op, bv.size());
52 
53  bv=bv_utils.signed_multiplier(bv, op);
54 
55  // cut it down again
56  bv.erase(bv.begin(), bv.begin()+fraction_bits);
57  }
58 
59  return bv;
60  }
61  else if(expr.type().id()==ID_unsignedbv ||
62  expr.type().id()==ID_signedbv)
63  {
65  expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
67 
68  bv = convert_bv(op0, width);
69 
70  for(exprt::operandst::const_iterator it=operands.begin()+1;
71  it!=operands.end(); it++)
72  {
74  it->type() == expr.type(),
75  "multiplication operands should have same type as expression");
76 
77  const bvt &op = convert_bv(*it, width);
78 
79  bv = bv_utils.multiplier(bv, op, rep);
80  }
81 
82  return bv;
83  }
84 
85  return conversion_failed(expr);
86 }
bv_utilst bv_utils
Definition: boolbv.h:95
exprt & op0()
Definition: expr.h:84
boolbv_widtht boolbv_width
Definition: boolbv.h:92
representationt
Definition: bv_utils.h:31
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
const irep_idt & id() const
Definition: irep.h:259
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:744
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:812
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
std::vector< exprt > operandst
Definition: expr.h:57
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
Pre-defined types.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1380
Base class for all expressions.
Definition: expr.h:54
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:179
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
virtual bvt convert_mult(const mult_exprt &expr)
Definition: boolbv_mult.cpp:13
std::vector< literalt > bvt
Definition: literal.h:200