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  if(operands.empty())
25  throw "mult without operands";
26 
27  const exprt &op0=expr.op0();
28 
29  bool no_overflow=expr.id()=="no-overflow-mult";
30 
31  if(expr.type().id()==ID_fixedbv)
32  {
33  if(op0.type()!=expr.type())
34  throw "multiplication with mixed types";
35 
36  bv=convert_bv(op0);
37 
38  if(bv.size()!=width)
39  throw "convert_mult: unexpected operand width";
40 
41  std::size_t fraction_bits=
42  to_fixedbv_type(expr.type()).get_fraction_bits();
43 
44  for(exprt::operandst::const_iterator it=operands.begin()+1;
45  it!=operands.end(); it++)
46  {
47  if(it->type()!=expr.type())
48  throw "multiplication with mixed types";
49 
50  // do a sign extension by fraction_bits bits
51  bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
52 
53  bvt op=convert_bv(*it);
54 
55  if(op.size()!=width)
56  throw "convert_mult: unexpected operand width";
57 
58  op=bv_utils.sign_extension(op, bv.size());
59 
60  bv=bv_utils.signed_multiplier(bv, op);
61 
62  // cut it down again
63  bv.erase(bv.begin(), bv.begin()+fraction_bits);
64  }
65 
66  return bv;
67  }
68  else if(expr.type().id()==ID_unsignedbv ||
69  expr.type().id()==ID_signedbv)
70  {
71  if(op0.type()!=expr.type())
72  throw "multiplication with mixed types";
73 
75  expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
77 
78  bv=convert_bv(op0);
79 
80  if(bv.size()!=width)
81  throw "convert_mult: unexpected operand width";
82 
83  for(exprt::operandst::const_iterator it=operands.begin()+1;
84  it!=operands.end(); it++)
85  {
86  if(it->type()!=expr.type())
87  throw "multiplication with mixed types";
88 
89  const bvt &op=convert_bv(*it);
90 
91  if(op.size()!=width)
92  throw "convert_mult: unexpected operand width";
93 
94  if(no_overflow)
95  bv=bv_utils.multiplier_no_overflow(bv, op, rep);
96  else
97  bv=bv_utils.multiplier(bv, op, rep);
98  }
99 
100  return bv;
101  }
102 
103  return conversion_failed(expr);
104 }
bv_utilst bv_utils
Definition: boolbv.h:93
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:804
exprt & op0()
Definition: expr.h:84
boolbv_widtht boolbv_width
Definition: boolbv.h:90
representationt
Definition: bv_utils.h:31
typet & type()
Definition: expr.h:60
virtual bvt convert_mult(const exprt &expr)
Definition: boolbv_mult.cpp:13
const irep_idt & id() const
Definition: irep.h:189
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:723
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:791
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
std::vector< exprt > operandst
Definition: expr.h:49
API to type classes.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1247
Base class for all expressions.
Definition: expr.h:46
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:175
operandst & operands()
Definition: expr.h:70
std::vector< literalt > bvt
Definition: literal.h:197