50 if(op.
type().
id()==ID_signedbv)
55 if(from_width==to_width)
57 else if(from_width<to_width)
61 out <<
", " << to_width <<
")";
67 out <<
")[" << (to_width-1) <<
":0]";
70 else if(op.
type().
id()==ID_unsignedbv)
75 if(from_width==to_width)
77 else if(from_width<to_width)
81 if(to_width > from_width)
82 out << std::string(to_width-from_width,
'0');
94 out <<
")[" << (to_width-1) <<
":0]";
97 else if(op.
type().
id()==ID_bool)
104 out << std::string(to_width-1,
'0');
110 out <<
" THEN 0bin1 ELSE 0bin0 ENDIF)";
116 out <<
" THEN 0bin1 ELSE 0bin0 ENDIF";
128 if(expr.
type().
id()==ID_unsignedbv ||
129 expr.
type().
id()==ID_signedbv ||
134 if(value.
size()==8 ||
139 std::size_t w=value.
size()/4;
147 out <<
"0hex" << hex;
151 out <<
"0bin" << value;
154 else if(expr.
type().
id()==ID_pointer)
166 throw "unknown pointer constant: "+
id2string(value);
168 else if(expr.
type().
id()==ID_bool)
175 throw "unknown boolean constant";
177 else if(expr.
type().
id()==ID_array)
200 else if(expr.
type().
id()==ID_integer ||
201 expr.
type().
id()==ID_natural ||
202 expr.
type().
id()==ID_range)
204 out << expr.
get(ID_value);
214 if(expr.
type().
id()==ID_unsignedbv ||
215 expr.
type().
id()==ID_signedbv)
217 out <<
"BVPLUS(" << expr.
type().
get(ID_width);
227 else if(expr.
type().
id()==ID_pointer)
230 throw "pointer arithmetic with more than two operands";
239 else if(expr.
op1().
type().
id()==ID_pointer)
245 throw "unexpected mixture in pointer arithmetic";
249 out <<
" IN P WITH .offset:=BVPLUS(" 271 if(expr.
type().
id()==ID_bool)
273 if(op.type().id()==ID_signedbv ||
274 op.type().id()==ID_unsignedbv ||
275 op.type().id()==ID_pointer)
283 throw "todo typecast1 "+op.type().id_string()+
" -> bool";
286 else if(expr.
type().
id()==ID_signedbv ||
287 expr.
type().
id()==ID_unsignedbv)
291 else if(expr.
type().
id()==ID_pointer)
293 if(op.type().id()==ID_pointer)
298 throw "todo typecast3 "+op.type().id_string()+
" -> pointer";
313 assert(components.size()==expr.
operands().size());
321 out << component.get(ID_name);
337 if(expr.
id()==ID_notequal)
345 if(expr.
id()==ID_notequal)
353 out << (expr.
id()==ID_equal?
"=":
"/=");
366 if(op_type.id()==ID_unsignedbv)
370 else if(expr.
id()==ID_lt)
372 else if(expr.
id()==ID_ge)
374 else if(expr.
id()==ID_gt)
383 else if(op_type.id()==ID_signedbv)
387 else if(expr.
id()==ID_lt)
389 else if(expr.
id()==ID_ge)
391 else if(expr.
id()==ID_gt)
402 throw "unsupported type for "+expr.
id_string()+
": "+
411 if(expr.
type().
id()==ID_unsignedbv ||
412 expr.
type().
id()==ID_signedbv)
414 out <<
"BVSUB(" << expr.
type().
get(ID_width) <<
", ";
438 for(
unsigned i=1; i<expr.
operands().size(); i+=2)
440 assert((i+1)<expr.
operands().size());
444 if(expr.
type().
id()==ID_struct)
446 out <<
" WITH ." << index.get(ID_component_name);
451 else if(expr.
type().
id()==ID_union)
453 out <<
" WITH ." << index.get(ID_component_name);
458 else if(expr.
type().
id()==ID_array)
468 throw "with expects struct or array type, but got "+
493 std::string
result=
"0bin";
505 return "[# object: INT, offset: BITVECTOR("+
511 return std::string(
"BITVECTOR(")+
512 std::to_string(32)+
")";
517 typet t(ID_signedbv);
543 if(expr.
id()==ID_symbol ||
544 expr.
id()==ID_constant ||
545 expr.
id()==ID_string_constant)
553 else if(expr.
id()==ID_index)
556 throw "index takes two operands";
563 if(array.
type().
id()==ID_pointer)
565 else if(array.
type().
id()==ID_array)
576 if(array.
type().
id()==ID_pointer)
578 else if(array.
type().
id()==ID_array)
583 out <<
" IN P WITH .offset:=BVPLUS(" 590 else if(expr.
id()==ID_member)
593 throw "member takes one operand";
617 out <<
" IN P WITH .offset:=BVPLUS(" 624 throw "don't know how to take address of: "+expr.
id_string();
629 if(expr.
type().
id()!=ID_bool)
631 std::string msg=
"cvc_convt::convert got " 632 "non-boolean expression: ";
644 else if(expr.
id()==ID_literal)
666 for(std::string::const_iterator
667 it=identifier.begin();
668 it!=identifier.end();
673 if(isalnum(ch) || ch==
'$' || ch==
'?')
677 std::string::const_iterator next_it(it);
679 if(next_it!=identifier.end() && *next_it==
':')
702 if(expr.
type().
id()==ID_bool)
712 out <<
" THEN 0bin1 ELSE 0bin0 ENDIF";
728 if(expr.
id()==ID_implies)
731 throw "implication takes two operands";
739 else if(expr.
id()==ID_constraint_select_one)
742 throw "constraint_select_one takes at least two operands";
745 throw "cvc_convt::convert_expr needs constraint_select_one";
747 else if(expr.
id()==ID_or || expr.
id()==ID_and || expr.
id()==ID_xor ||
748 expr.
id()==ID_nor || expr.
id()==ID_nand)
751 throw "operator `"+expr.
id_string()+
"' takes at least one operand";
752 else if(op.size()==1)
762 else if(expr.
id()==ID_nor)
764 else if(expr.
id()==ID_and)
766 else if(expr.
id()==ID_nand)
768 else if(expr.
id()==ID_xor)
780 else if(expr.
id()==ID_not)
783 throw "not takes one operand";
789 else if(expr.
id()==ID_symbol)
793 else if(expr.
id()==ID_nondet_symbol)
797 else if(expr.
id()==ID_typecast)
801 else if(expr.
id()==ID_struct)
805 else if(expr.
id()==ID_constant)
809 else if(expr.
id()==ID_concatenation ||
810 expr.
id()==ID_bitand ||
819 if(expr.
id()==ID_concatenation)
821 else if(expr.
id()==ID_bitand)
823 else if(expr.
id()==ID_bitor)
832 else if(expr.
id()==ID_bitxor)
853 tmp.operands().resize(tmp.operands().size()-1);
862 else if(expr.
id()==ID_bitnand)
872 else if(expr.
id()==ID_bitnot)
879 else if(expr.
id()==ID_unary_minus)
882 if(expr.
type().
id()==ID_unsignedbv ||
883 expr.
type().
id()==ID_signedbv)
890 throw "unsupported type for unary-: "+expr.
type().
id_string();
892 else if(expr.
id()==ID_if)
903 else if(expr.
id()==ID_and ||
907 assert(expr.
type().
id()==ID_bool);
915 if(expr.
id()==ID_and)
917 else if(expr.
id()==ID_or)
919 else if(expr.
id()==ID_xor)
935 else if(expr.
id()==ID_not)
942 else if(expr.
id()==ID_equal ||
943 expr.
id()==ID_notequal)
947 else if(expr.
id()==ID_le ||
954 else if(expr.
id()==ID_plus)
958 else if(expr.
id()==ID_minus)
962 else if(expr.
id()==ID_div)
966 if(expr.
type().
id()==ID_unsignedbv ||
967 expr.
type().
id()==ID_signedbv)
969 if(expr.
type().
id()==ID_unsignedbv)
974 out <<
"(" << expr.
type().
get(ID_width) <<
", ";
983 else if(expr.
id()==ID_mod)
987 if(expr.
type().
id()==ID_unsignedbv ||
988 expr.
type().
id()==ID_signedbv)
990 if(expr.
type().
id()==ID_unsignedbv)
995 out <<
"(" << expr.
type().
get(ID_width) <<
", ";
1004 else if(expr.
id()==ID_mult)
1008 if(expr.
type().
id()==ID_unsignedbv ||
1009 expr.
type().
id()==ID_signedbv)
1011 out <<
"BVMULT(" << expr.
type().
get(ID_width) <<
", ";
1027 else if(expr.
id()==ID_address_of ||
1028 expr.
id()==
"reference_to")
1031 assert(expr.
type().
id()==ID_pointer);
1034 else if(expr.
id()==ID_array_of)
1036 assert(expr.
type().
id()==ID_array);
1042 else if(expr.
id()==ID_index)
1051 else if(expr.
id()==ID_ashr ||
1052 expr.
id()==ID_lshr ||
1057 if(expr.
type().
id()==ID_unsignedbv ||
1058 expr.
type().
id()==ID_signedbv)
1060 if(expr.
id()==ID_ashr)
1062 else if(expr.
id()==ID_lshr)
1064 else if(expr.
id()==ID_shl)
1069 out <<
"(" << expr.
type().
get(ID_width) <<
", ";
1077 throw "unsupported type for "+expr.
id_string()+
": "+
1081 else if(expr.
id()==ID_with)
1085 else if(expr.
id()==ID_member)
1090 out << expr.
get(ID_component_name);
1092 else if(expr.
id()==ID_pointer_offset)
1100 else if(expr.
id()==ID_pointer_object)
1109 else if(expr.
id()==ID_string_constant)
1113 else if(expr.
id()==ID_extractbit)
1117 if(expr.
op0().
type().
id()==ID_unsignedbv ||
1125 throw "extractbit takes constant as second parameter";
1127 out <<
"[" << i <<
":" << i <<
"]=0bin1)";
1131 throw "unsupported type for "+expr.
id_string()+
": "+
1135 else if(expr.
id()==ID_replication)
1141 throw "replication takes constant as first parameter";
1143 out <<
"(LET v: BITVECTOR(1) = ";
1159 throw "convert_expr: "+expr.
id_string()+
" is unsupported";
1164 if(value && expr.
id()==ID_and)
1171 out <<
"%% set_to " << (value?
"true":
"false") <<
'\n';
1173 if(expr.
id()==ID_equal && value)
1177 if(expr.
op0().
id()==ID_symbol)
1183 if(
id.type.is_nil())
1185 std::unordered_set<irep_idt, irep_id_hash> s_set;
1189 if(s_set.find(identifier)==s_set.end())
1230 if(expr.
id()==ID_symbol)
1232 if(expr.
type().
id()==ID_code)
1235 const irep_idt &identifier=expr.
get(ID_identifier);
1239 if(
id.type.is_nil())
1241 id.type=expr.
type();
1249 else if(expr.
id()==ID_nondet_symbol)
1251 if(expr.
type().
id()==ID_code)
1258 if(
id.type.is_nil())
1260 id.type=expr.
type();
1272 if(type.
id()==ID_array)
1280 out <<
"BITVECTOR(1)";
1284 else if(type.
id()==ID_bool)
1288 else if(type.
id()==ID_struct ||
1289 type.
id()==ID_union)
1300 if(component!=components.front())
1304 out << component.get_name();
1311 else if(type.
id()==ID_pointer ||
1312 type.
id()==ID_reference)
1316 else if(type.
id()==ID_integer)
1320 else if(type.
id()==ID_signedbv)
1325 throw "zero-width vector type: "+type.
id_string();
1327 out <<
"BITVECTOR(" << width <<
")";
1329 else if(type.
id()==ID_unsignedbv)
1334 throw "zero-width vector type: "+type.
id_string();
1336 out <<
"BITVECTOR(" << width <<
")";
1339 throw "unsupported type: "+type.
id_string();
1344 if(type.
id()==ID_array)
1349 else if(type.
id()==ID_struct ||
1350 type.
id()==ID_union)
void convert_minus_expr(const exprt &expr)
The type of an expression.
std::size_t get_null_object() const
struct configt::ansi_ct ansi_c
void convert_comparison_expr(const exprt &expr)
const std::string & id2string(const irep_idt &d)
void convert_binary_expr(const exprt &expr, const exprt &op)
const std::string integer2string(const mp_integer &n, unsigned base)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void convert_plus_expr(const exprt &expr)
unsigned unsafe_string2unsigned(const std::string &str, int base)
void copy_to_operands(const exprt &expr)
#define forall_expr(it, expr)
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::vector< componentt > componentst
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
const componentst & components() const
virtual void convert_address_of_rec(const exprt &expr)
static std::string array_index(unsigned i)
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
void convert_constant_expr(const exprt &expr)
static std::string bin_zero(unsigned bits)
API to expression classes.
virtual literalt convert(const exprt &expr)
const irep_idt & get(const irep_namet &name) const
void convert_literal(const literalt l)
const exprt & size() const
#define forall_operands(it, expr)
identifier_mapt identifier_map
void convert_with_expr(const exprt &expr)
bitvector_typet index_type()
virtual void print_assignment(std::ostream &out) const
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
std::size_t get_width() const
static typet gen_array_index_type()
std::vector< exprt > operandst
static std::string cvc_pointer_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
literalt const_literal(bool value)
void convert_array_value(const exprt &expr)
void convert_as_bv(const exprt &expr)
void convert_identifier(const std::string &identifier)
const string_constantt & to_string_constant(const exprt &expr)
literalt get_literal() const
void convert_equality_expr(const exprt &expr)
virtual void convert_type(const typet &type)
Base class for all expressions.
void convert_struct_expr(const exprt &expr)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
irep_idt get_component_name() const
const std::string integer2binary(const mp_integer &n, std::size_t width)
virtual tvt l_get(literalt) const
std::vector< bool > boolean_assignment
unsigned no_boolean_variables
const std::string & get_string(const irep_namet &name) const
const std::string & id_string() const
static std::string array_index_type()
void find_symbols(const exprt &expr)
void convert_typecast_expr(const exprt &expr)
pointer_logict pointer_logic
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
void convert_array_index(const exprt &expr)
const typet & subtype() const
virtual void set_to(const exprt &expr, bool value)
std::size_t add_object(const exprt &expr)
void set(const irep_namet &name, const irep_idt &value)
virtual void convert_expr(const exprt &expr)