CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/accelerate/util.cpp Source File

20 signedbv_typet signed_poly_type()

21{

22 return signed_int_type();

23}

25 unsignedbv_typet unsigned_poly_type()

26{

27 return unsigned_int_type();

28}

33 bool is_bitvector(const typet &t)

34{

35 return t.id()==ID_bv ||

36 t.id()==ID_signedbv ||

37 t.id()==ID_unsignedbv ||

38 t.id()==ID_pointer ||

39 t.id()==ID_bool;

40}

45 bool is_signed(const typet &t)

46{

47 return t.id()==ID_signedbv;

48}

52 bool is_unsigned(const typet &t)

53{

54 return t.id()==ID_bv ||

55 t.id()==ID_unsignedbv ||

56 t.id()==ID_pointer ||

57 t.id()==ID_bool;

58}

70 typet join_types(const typet &t1, const typet &t2)

71{

72 // Handle the simple case first...

73 if(t1==t2)

74 {

75 return t1;

76 }

77

78 // OK, they're not the same type. Are they both bitvectors?

79 if(is_bitvector(t1) && is_bitvector(t2))

80 {

81 // They are. That makes things easy! There are three cases to consider:

82 // both types are unsigned, both types are signed or there's one of each.

83

84 bitvector_typet b1=to_bitvector_type(t1);

85 bitvector_typet b2=to_bitvector_type(t2);

86

87 if(is_unsigned(b1) && is_unsigned(b2))

88 {

89 // We just need to take the max of their widths.

90 std::size_t width=std::max(b1.get_width(), b2.get_width());

91 return unsignedbv_typet(width);

92 }

93 else if(is_signed(b1) && is_signed(b2))

94 {

95 // Again, just need to take the max of the widths.

96 std::size_t width=std::max(b1.get_width(), b2.get_width());

97 return signedbv_typet(width);

98 }

99 else

100 {

101 // This is the (slightly) tricky case. If we have a signed and an

102 // unsigned type, we're going to return a signed type. And to cast

103 // an unsigned type to a signed type, we need the signed type to be

104 // at least one bit wider than the unsigned type we're casting from.

105 std::size_t signed_width=is_signed(t1) ? b1.get_width() :

106 b2.get_width();

107 std::size_t unsigned_width=is_signed(t1) ? b2.get_width() :

108 b1.get_width();

109 // unsigned_width++;

110

111 std::size_t width=std::max(signed_width, unsigned_width);

112

113 return signedbv_typet(width);

114 }

115 }

116

117 std::cerr << "Tried to join types: "

118 << t1.pretty() << " and " << t2.pretty()

119 << '\n';

120

121 INVARIANT(false, "failed to join types");

122}

to_bitvector_type

const bitvector_typet & to_bitvector_type(const typet &type)

Cast a typet to a bitvector_typet.

Definition bitvector_types.h:99

unsigned_int_type

unsignedbv_typet unsigned_int_type()

Definition c_types.cpp:36

signed_int_type

signedbv_typet signed_int_type()

Definition c_types.cpp:22

c_types.h

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

bitvector_typet

Base class of fixed-width bit-vector types.

Definition bitvector_types.h:27

irept::id

const irep_idt & id() const

Definition irep.h:388

signedbv_typet

Fixed-width bit-vector with two's complement interpretation.

Definition bitvector_types.h:285

typet

The type of an expression, extends irept.

Definition type.h:29

unsignedbv_typet

Fixed-width bit-vector with unsigned binary interpretation.

Definition bitvector_types.h:231

INVARIANT

#define INVARIANT(CONDITION, REASON)

This macro uses the wrapper function 'invariant_violated_string'.

Definition invariant.h:423

std_types.h

Pre-defined types.

join_types

typet join_types(const typet &t1, const typet &t2)

Return the smallest type that both t1 and t2 can be cast to without losing information.

Definition util.cpp:70

unsigned_poly_type

unsignedbv_typet unsigned_poly_type()

Definition util.cpp:25

is_bitvector

bool is_bitvector(const typet &t)

Convenience function – is the type a bitvector of some kind?

Definition util.cpp:33

is_signed

bool is_signed(const typet &t)

Convenience function – is the type signed?

Definition util.cpp:45

signed_poly_type

signedbv_typet signed_poly_type()

Definition util.cpp:20

is_unsigned

bool is_unsigned(const typet &t)

Convenience function – is the type unsigned?

Definition util.cpp:52

util.h

Loop Acceleration.