cprover
smt2_conv.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: SMT Backend
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "smt2_conv.h"
13
14#include <util/arith_tools.h>
15#include <util/bitvector_expr.h>
16#include <util/byte_operators.h>
17#include <util/c_types.h>
18#include <util/config.h>
19#include <util/expr_iterator.h>
20#include <util/expr_util.h>
21#include <util/fixedbv.h>
22#include <util/floatbv_expr.h>
23#include <util/format_expr.h>
24#include <util/ieee_float.h>
25#include <util/invariant.h>
27#include <util/namespace.h>
28#include <util/pointer_expr.h>
31#include <util/prefix.h>
32#include <util/range.h>
33#include <util/simplify_expr.h>
34#include <util/std_expr.h>
35#include <util/string2int.h>
37#include <util/threeval.h>
38
44
45// Mark different kinds of error conditions
46
47// Unexpected types and other combinations not implemented and not
48// expected to be needed
49#define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
50
51// General todos
52#define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
53
55 const namespacet &_ns,
56 const std::string &_benchmark,
57 const std::string &_notes,
58 const std::string &_logic,
59 solvert _solver,
60 std::ostream &_out)
61 : use_FPA_theory(false),
62 use_array_of_bool(false),
63 use_as_const(false),
64 use_check_sat_assuming(false),
65 use_datatypes(false),
66 use_lambda_for_array(false),
67 emit_set_logic(true),
68 ns(_ns),
69 out(_out),
70 benchmark(_benchmark),
71 notes(_notes),
72 logic(_logic),
73 solver(_solver),
74 boolbv_width(_ns),
75 pointer_logic(_ns),
76 no_boolean_variables(0)
77{
78 // We set some defaults differently
79 // for some solvers.
80
81 switch(solver)
82 {
84 break;
85
87 break;
88
90 use_FPA_theory = true;
91 use_array_of_bool = true;
92 use_as_const = true;
94 emit_set_logic = false;
95 break;
96
97 case solvert::CVC3:
98 break;
99
100 case solvert::CVC4:
101 logic = "ALL";
102 use_array_of_bool = true;
103 use_as_const = true;
104 break;
105
106 case solvert::MATHSAT:
107 break;
108
109 case solvert::YICES:
110 break;
111
112 case solvert::Z3:
113 use_array_of_bool = true;
114 use_as_const = true;
117 emit_set_logic = false;
118 use_datatypes = true;
119 break;
120 }
121
122 write_header();
123}
124
126{
127 return "SMT2";
128}
129
130void smt2_convt::print_assignment(std::ostream &os) const
131{
132 // Boolean stuff
133
134 for(std::size_t v=0; v<boolean_assignment.size(); v++)
135 os << "b" << v << "=" << boolean_assignment[v] << "\n";
136
137 // others
138}
139
141{
142 if(l.is_true())
143 return tvt(true);
144 if(l.is_false())
145 return tvt(false);
146
147 INVARIANT(
148 l.var_no() < boolean_assignment.size(),
149 "variable number shall be within bounds");
150 return tvt(boolean_assignment[l.var_no()]^l.sign());
151}
152
154{
155 out << "; SMT 2" << "\n";
156
157 switch(solver)
158 {
159 // clang-format off
160 case solvert::GENERIC: break;
161 case solvert::BOOLECTOR: out << "; Generated for Boolector\n"; break;
163 out << "; Generated for the CPROVER SMT2 solver\n"; break;
164 case solvert::CVC3: out << "; Generated for CVC 3\n"; break;
165 case solvert::CVC4: out << "; Generated for CVC 4\n"; break;
166 case solvert::MATHSAT: out << "; Generated for MathSAT\n"; break;
167 case solvert::YICES: out << "; Generated for Yices\n"; break;
168 case solvert::Z3: out << "; Generated for Z3\n"; break;
169 // clang-format on
170 }
171
172 out << "(set-info :source \"" << notes << "\")" << "\n";
173
174 out << "(set-option :produce-models true)" << "\n";
175
176 // We use a broad mixture of logics, so on some solvers
177 // its better not to declare here.
178 // set-logic should come after setting options
179 if(emit_set_logic && !logic.empty())
180 out << "(set-logic " << logic << ")" << "\n";
181}
182
184{
185 out << "\n";
186
187 // fix up the object sizes
188 for(const auto &object : object_sizes)
189 define_object_size(object.second, object.first);
190
191 if(use_check_sat_assuming && !assumptions.empty())
192 {
193 out << "(check-sat-assuming (";
194 for(const auto &assumption : assumptions)
195 convert_literal(to_literal_expr(assumption).get_literal());
196 out << "))\n";
197 }
198 else
199 {
200 // add the assumptions, if any
201 if(!assumptions.empty())
202 {
203 out << "; assumptions\n";
204
205 for(const auto &assumption : assumptions)
206 {
207 out << "(assert ";
208 convert_literal(to_literal_expr(assumption).get_literal());
209 out << ")"
210 << "\n";
211 }
212 }
213
214 out << "(check-sat)\n";
215 }
216
217 out << "\n";
218
220 {
221 for(const auto &id : smt2_identifiers)
222 out << "(get-value (|" << id << "|))"
223 << "\n";
224 }
225
226 out << "\n";
227
228 out << "(exit)\n";
229
230 out << "; end of SMT2 file"
231 << "\n";
232}
233
235 const irep_idt &id,
236 const exprt &expr)
237{
238 PRECONDITION(expr.id() == ID_object_size);
239 const exprt &ptr = to_unary_expr(expr).op();
240 std::size_t size_width = boolbv_width(expr.type());
241 std::size_t pointer_width = boolbv_width(ptr.type());
242 std::size_t number = 0;
243 std::size_t h=pointer_width-1;
244 std::size_t l=pointer_width-config.bv_encoding.object_bits;
245
246 for(const auto &o : pointer_logic.objects)
247 {
248 const typet &type = o.type();
249 auto size_expr = size_of_expr(type, ns);
250 const auto object_size =
251 numeric_cast<mp_integer>(size_expr.value_or(nil_exprt()));
252
253 if(
254 (o.id() != ID_symbol && o.id() != ID_string_constant) ||
255 !size_expr.has_value() || !object_size.has_value())
256 {
257 ++number;
258 continue;
259 }
260
261 out << "(assert (=> (= "
262 << "((_ extract " << h << " " << l << ") ";
263 convert_expr(ptr);
264 out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))"
265 << "(= |" << id << "| (_ bv" << *object_size << " " << size_width
266 << "))))\n";
267
268 ++number;
269 }
270}
271
273{
274 write_footer();
275 out.flush();
277}
278
279exprt smt2_convt::get(const exprt &expr) const
280{
281 if(expr.id()==ID_symbol)
282 {
283 const irep_idt &id=to_symbol_expr(expr).get_identifier();
284
285 identifier_mapt::const_iterator it=identifier_map.find(id);
286
287 if(it!=identifier_map.end())
288 return it->second.value;
289 return expr;
290 }
291 else if(expr.id()==ID_nondet_symbol)
292 {
294
295 identifier_mapt::const_iterator it=identifier_map.find(id);
296
297 if(it!=identifier_map.end())
298 return it->second.value;
299 }
300 else if(expr.id()==ID_member)
301 {
302 const member_exprt &member_expr=to_member_expr(expr);
303 exprt tmp=get(member_expr.struct_op());
304 if(tmp.is_nil())
305 return nil_exprt();
306 return member_exprt(tmp, member_expr.get_component_name(), expr.type());
307 }
308 else if(expr.id() == ID_literal)
309 {
310 auto l = to_literal_expr(expr).get_literal();
311 if(l_get(l).is_true())
312 return true_exprt();
313 else
314 return false_exprt();
315 }
316 else if(expr.id() == ID_not)
317 {
318 auto op = get(to_not_expr(expr).op());
319 if(op.is_true())
320 return false_exprt();
321 else if(op.is_false())
322 return true_exprt();
323 }
324 else if(expr.is_constant())
325 return expr;
326 else if(const auto &array = expr_try_dynamic_cast<array_exprt>(expr))
327 {
328 exprt array_copy = *array;
329 for(auto &element : array_copy.operands())
330 {
331 element = get(element);
332 }
333 return array_copy;
334 }
335
336 return nil_exprt();
337}
338
340 const irept &src,
341 const typet &type)
342{
343 // See http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf for the
344 // syntax of SMTlib2 literals.
345 //
346 // A literal expression is one of the following forms:
347 //
348 // * Numeral -- this is a natural number in decimal and is of the form:
349 // 0|([1-9][0-9]*)
350 // * Decimal -- this is a decimal expansion of a real number of the form:
351 // (0|[1-9][0-9]*)[.]([0-9]+)
352 // * Binary -- this is a natural number in binary and is of the form:
353 // #b[01]+
354 // * Hex -- this is a natural number in hexadecimal and is of the form:
355 // #x[0-9a-fA-F]+
356 //
357 // Right now I'm not parsing decimals. It'd be nice if we had a real YACC
358 // parser here, but whatever.
359
360 mp_integer value;
361
362 if(!src.id().empty())
363 {
364 const std::string &s=src.id_string();
365
366 if(s.size()>=2 && s[0]=='#' && s[1]=='b')
367 {
368 // Binary #b010101
369 value=string2integer(s.substr(2), 2);
370 }
371 else if(s.size()>=2 && s[0]=='#' && s[1]=='x')
372 {
373 // Hex #x012345
374 value=string2integer(s.substr(2), 16);
375 }
376 else
377 {
378 // Numeral
379 value=string2integer(s);
380 }
381 }
382 else if(src.get_sub().size()==2 &&
383 src.get_sub()[0].id()=="-") // (- 100)
384 {
385 value=-string2integer(src.get_sub()[1].id_string());
386 }
387 else if(src.get_sub().size()==3 &&
388 src.get_sub()[0].id()=="_" &&
389 // (_ bvDECIMAL_VALUE SIZE)
390 src.get_sub()[1].id_string().substr(0, 2)=="bv")
391 {
392 value=string2integer(src.get_sub()[1].id_string().substr(2));
393 }
394 else if(src.get_sub().size()==4 &&
395 src.get_sub()[0].id()=="fp") // (fp signbv exponentbv significandbv)
396 {
397 if(type.id()==ID_floatbv)
398 {
399 const floatbv_typet &floatbv_type=to_floatbv_type(type);
402 parse_literal(src.get_sub()[2], unsignedbv_typet(floatbv_type.get_e()));
403 constant_exprt s3 =
404 parse_literal(src.get_sub()[3], unsignedbv_typet(floatbv_type.get_f()));
405
406 const auto s1_int = numeric_cast_v<mp_integer>(s1);
407 const auto s2_int = numeric_cast_v<mp_integer>(s2);
408 const auto s3_int = numeric_cast_v<mp_integer>(s3);
409
410 // stitch the bits together
411 value = bitwise_or(
412 s1_int << (floatbv_type.get_e() + floatbv_type.get_f()),
413 bitwise_or((s2_int << floatbv_type.get_f()), s3_int));
414 }
415 else
416 value=0;
417 }
418 else if(src.get_sub().size()==4 &&
419 src.get_sub()[0].id()=="_" &&
420 src.get_sub()[1].id()=="+oo") // (_ +oo e s)
421 {
422 std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
423 std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
425 }
426 else if(src.get_sub().size()==4 &&
427 src.get_sub()[0].id()=="_" &&
428 src.get_sub()[1].id()=="-oo") // (_ -oo e s)
429 {
430 std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
431 std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
433 }
434 else if(src.get_sub().size()==4 &&
435 src.get_sub()[0].id()=="_" &&
436 src.get_sub()[1].id()=="NaN") // (_ NaN e s)
437 {
438 std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
439 std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
440 return ieee_floatt::NaN(ieee_float_spect(s - 1, e)).to_expr();
441 }
442
443 if(type.id()==ID_signedbv ||
444 type.id()==ID_unsignedbv ||
445 type.id()==ID_c_enum ||
446 type.id()==ID_c_bool)
447 {
448 return from_integer(value, type);
449 }
450 else if(type.id()==ID_c_enum_tag)
451 {
452 constant_exprt result =
454
455 // restore the c_enum_tag type
456 result.type() = type;
457 return result;
458 }
459 else if(type.id()==ID_fixedbv ||
460 type.id()==ID_floatbv)
461 {
462 std::size_t width=boolbv_width(type);
463 return constant_exprt(integer2bvrep(value, width), type);
464 }
465 else if(type.id()==ID_integer ||
466 type.id()==ID_range)
467 {
468 return from_integer(value, type);
469 }
470 else
471 INVARIANT(
472 false,
473 "smt2_convt::parse_literal should not be of unsupported type " +
474 type.id_string());
475}
476
478 const irept &src,
479 const array_typet &type)
480{
481 std::unordered_map<int64_t, exprt> operands_map;
482 walk_array_tree(&operands_map, src, type);
483 exprt::operandst operands;
484 // Try to find the default value, if there is none then set it
485 auto maybe_default_op = operands_map.find(-1);
486 exprt default_op;
487 if(maybe_default_op == operands_map.end())
488 default_op = nil_exprt();
489 else
490 default_op = maybe_default_op->second;
491 int64_t i = 0;
492 auto maybe_size = numeric_cast<std::int64_t>(type.size());
493 if(maybe_size.has_value())
494 {
495 while(i < maybe_size.value())
496 {
497 auto found_op = operands_map.find(i);
498 if(found_op != operands_map.end())
499 operands.emplace_back(found_op->second);
500 else
501 operands.emplace_back(default_op);
502 i++;
503 }
504 }
505 else
506 {
507 // Array size is unknown, keep adding with known indexes in order
508 // until we fail to find one.
509 auto found_op = operands_map.find(i);
510 while(found_op != operands_map.end())
511 {
512 operands.emplace_back(found_op->second);
513 i++;
514 found_op = operands_map.find(i);
515 }
516 operands.emplace_back(default_op);
517 }
518 return array_exprt(operands, type);
519}
520
522 std::unordered_map<int64_t, exprt> *operands_map,
523 const irept &src,
524 const array_typet &type)
525{
526 if(src.get_sub().size()==4 && src.get_sub()[0].id()=="store")
527 {
528 // This is the SMT syntax being parsed here
529 // (store array index value)
530 // Recurse
531 walk_array_tree(operands_map, src.get_sub()[1], type);
532 const auto index_expr = parse_rec(src.get_sub()[2], type.size().type());
533 const constant_exprt index_constant = to_constant_expr(index_expr);
534 mp_integer tempint;
535 bool failure = to_integer(index_constant, tempint);
536 if(failure)
537 return;
538 long index = tempint.to_long();
539 exprt value = parse_rec(src.get_sub()[3], type.element_type());
540 operands_map->emplace(index, value);
541 }
542 else if(src.get_sub().size() == 3 && src.get_sub()[0].id() == "let")
543 {
544 // This is produced by Z3
545 // (let (....) (....))
547 operands_map, src.get_sub()[1].get_sub()[0].get_sub()[1], type);
548 walk_array_tree(operands_map, src.get_sub()[2], type);
549 }
550 else if(src.get_sub().size()==2 &&
551 src.get_sub()[0].get_sub().size()==3 &&
552 src.get_sub()[0].get_sub()[0].id()=="as" &&
553 src.get_sub()[0].get_sub()[1].id()=="const")
554 {
555 // (as const type_info default_value)
556 exprt default_value = parse_rec(src.get_sub()[1], type.element_type());
557 operands_map->emplace(-1, default_value);
558 }
559}
560
562 const irept &src,
563 const union_typet &type)
564{
565 // these are always flat
566 PRECONDITION(!type.components().empty());
567 const union_typet::componentt &first=type.components().front();
568 std::size_t width=boolbv_width(type);
569 exprt value = parse_rec(src, unsignedbv_typet(width));
570 if(value.is_nil())
571 return nil_exprt();
572 const typecast_exprt converted(value, first.type());
573 return union_exprt(first.get_name(), converted, type);
574}
575
578{
579 const struct_typet::componentst &components =
580 type.components();
581
582 struct_exprt result(exprt::operandst(components.size(), nil_exprt()), type);
583
584 if(components.empty())
585 return result;
586
587 if(use_datatypes)
588 {
589 // Structs look like:
590 // (mk-struct.1 <component0> <component1> ... <componentN>)
591
592 if(src.get_sub().size()!=components.size()+1)
593 return result; // give up
594
595 for(std::size_t i=0; i<components.size(); i++)
596 {
597 const struct_typet::componentt &c=components[i];
598 result.operands()[i]=parse_rec(src.get_sub()[i+1], c.type());
599 }
600 }
601 else
602 {
603 // These are just flattened, i.e., we expect to see a monster bit vector.
604 std::size_t total_width=boolbv_width(type);
605 const auto l = parse_literal(src, unsignedbv_typet(total_width));
606
607 const irep_idt binary =
608 integer2binary(numeric_cast_v<mp_integer>(l), total_width);
609
610 CHECK_RETURN(binary.size() == total_width);
611
612 std::size_t offset=0;
613
614 for(std::size_t i=0; i<components.size(); i++)
615 {
616 std::size_t component_width=boolbv_width(components[i].type());
617
618 INVARIANT(
619 offset + component_width <= total_width,
620 "struct component bits shall be within struct bit vector");
621
622 std::string component_binary=
623 "#b"+id2string(binary).substr(
624 total_width-offset-component_width, component_width);
625
626 result.operands()[i]=
627 parse_rec(irept(component_binary), components[i].type());
628
629 offset+=component_width;
630 }
631 }
632
633 return result;
634}
635
636exprt smt2_convt::parse_rec(const irept &src, const typet &type)
637{
638 if(
639 type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
640 type.id() == ID_integer || type.id() == ID_rational ||
641 type.id() == ID_real || type.id() == ID_c_enum ||
642 type.id() == ID_c_enum_tag || type.id() == ID_fixedbv ||
643 type.id() == ID_floatbv)
644 {
645 return parse_literal(src, type);
646 }
647 else if(type.id()==ID_bool)
648 {
649 if(src.id()==ID_1 || src.id()==ID_true)
650 return true_exprt();
651 else if(src.id()==ID_0 || src.id()==ID_false)
652 return false_exprt();
653 }
654 else if(type.id()==ID_pointer)
655 {
656 // these come in as bit-vector literals
657 std::size_t width=boolbv_width(type);
658 constant_exprt bv_expr = parse_literal(src, unsignedbv_typet(width));
659
660 mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
661
662 // split into object and offset
665 ptr.object = numeric_cast_v<std::size_t>(v / pow);
666 ptr.offset=v%pow;
667 return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
668 }
669 else if(type.id()==ID_struct)
670 {
671 return parse_struct(src, to_struct_type(type));
672 }
673 else if(type.id() == ID_struct_tag)
674 {
675 auto struct_expr =
677 // restore the tag type
678 struct_expr.type() = type;
679 return std::move(struct_expr);
680 }
681 else if(type.id()==ID_union)
682 {
683 return parse_union(src, to_union_type(type));
684 }
685 else if(type.id() == ID_union_tag)
686 {
687 auto union_expr = parse_union(src, ns.follow_tag(to_union_tag_type(type)));
688 // restore the tag type
689 union_expr.type() = type;
690 return union_expr;
691 }
692 else if(type.id()==ID_array)
693 {
694 return parse_array(src, to_array_type(type));
695 }
696
697 return nil_exprt();
698}
699
701 const exprt &expr,
702 const pointer_typet &result_type)
703{
704 if(expr.id()==ID_symbol ||
705 expr.id()==ID_constant ||
706 expr.id()==ID_string_constant ||
707 expr.id()==ID_label)
708 {
709 out
710 << "(concat (_ bv"
711 << pointer_logic.add_object(expr) << " "
713 << " (_ bv0 "
714 << boolbv_width(result_type)-config.bv_encoding.object_bits << "))";
715 }
716 else if(expr.id()==ID_index)
717 {
718 const index_exprt &index_expr = to_index_expr(expr);
719
720 const exprt &array = index_expr.array();
721 const exprt &index = index_expr.index();
722
723 if(index.is_zero())
724 {
725 if(array.type().id()==ID_pointer)
726 convert_expr(array);
727 else if(array.type().id()==ID_array)
728 convert_address_of_rec(array, result_type);
729 else
731 }
732 else
733 {
734 // this is really pointer arithmetic
735 index_exprt new_index_expr = index_expr;
736 new_index_expr.index() = from_integer(0, index.type());
737
738 address_of_exprt address_of_expr(
739 new_index_expr,
741
742 plus_exprt plus_expr{address_of_expr, index};
743
744 convert_expr(plus_expr);
745 }
746 }
747 else if(expr.id()==ID_member)
748 {
749 const member_exprt &member_expr=to_member_expr(expr);
750
751 const exprt &struct_op=member_expr.struct_op();
752 const typet &struct_op_type = struct_op.type();
753
755 struct_op_type.id() == ID_struct || struct_op_type.id() == ID_struct_tag,
756 "member expression operand shall have struct type");
757
758 const struct_typet &struct_type = to_struct_type(ns.follow(struct_op_type));
759
760 const irep_idt &component_name = member_expr.get_component_name();
761
762 const auto offset = member_offset(struct_type, component_name, ns);
763 CHECK_RETURN(offset.has_value() && *offset >= 0);
764
766
767 // pointer arithmetic
768 out << "(bvadd ";
769 convert_address_of_rec(struct_op, result_type);
771 out << ")"; // bvadd
772 }
773 else if(expr.id()==ID_if)
774 {
775 const if_exprt &if_expr = to_if_expr(expr);
776
777 out << "(ite ";
778 convert_expr(if_expr.cond());
779 out << " ";
780 convert_address_of_rec(if_expr.true_case(), result_type);
781 out << " ";
782 convert_address_of_rec(if_expr.false_case(), result_type);
783 out << ")";
784 }
785 else
786 INVARIANT(
787 false,
788 "operand of address of expression should not be of kind " +
789 expr.id_string());
790}
791
793{
794 PRECONDITION(expr.type().id() == ID_bool);
795
796 // Three cases where no new handle is needed.
797
798 if(expr.is_true())
799 return const_literal(true);
800 else if(expr.is_false())
801 return const_literal(false);
802 else if(expr.id()==ID_literal)
803 return to_literal_expr(expr).get_literal();
804
805 // Need a new handle
806
807 out << "\n";
808
809 exprt prepared_expr = prepare_for_convert_expr(expr);
810
813
814 out << "; convert\n";
815 out << "; Converting var_no " << l.var_no() << " with expr ID of "
816 << expr.id_string() << "\n";
817 // We're converting the expression, so store it in the defined_expressions
818 // store and in future we use the literal instead of the whole expression
819 // Note that here we are always converting, so we do not need to consider
820 // other literal kinds, only "|B###|"
821 defined_expressions[expr] =
822 std::string{"|B"} + std::to_string(l.var_no()) + "|";
823 out << "(define-fun ";
825 out << " () Bool ";
826 convert_expr(prepared_expr);
827 out << ")" << "\n";
828
829 return l;
830}
831
833{
834 // We can only improve Booleans.
835 if(expr.type().id() != ID_bool)
836 return expr;
837
838 return literal_exprt(convert(expr));
839}
840
842{
843 if(l==const_literal(false))
844 out << "false";
845 else if(l==const_literal(true))
846 out << "true";
847 else
848 {
849 if(l.sign())
850 out << "(not ";
851
852 out << "|B" << l.var_no() << "|";
853
854 if(l.sign())
855 out << ")";
856
857 smt2_identifiers.insert("B"+std::to_string(l.var_no()));
858 }
859}
860
862{
864}
865
866void smt2_convt::push(const std::vector<exprt> &_assumptions)
867{
868 INVARIANT(assumptions.empty(), "nested contexts are not supported");
869
870 assumptions = _assumptions;
871}
872
874{
875 assumptions.clear();
876}
877
878std::string smt2_convt::convert_identifier(const irep_idt &identifier)
879{
880 // Backslashes are disallowed in quoted symbols just for simplicity.
881 // Otherwise, for Common Lisp compatibility they would have to be treated
882 // as escaping symbols.
883
884 std::string result;
885
886 for(std::size_t i=0; i<identifier.size(); i++)
887 {
888 char ch=identifier[i];
889
890 switch(ch)
891 {
892 case '|':
893 case '\\':
894 case '&': // we use the & for escaping
895 result+='&';
896 result+=std::to_string(ch);
897 result+=';';
898 break;
899
900 case '$': // $ _is_ allowed
901 default:
902 result+=ch;
903 }
904 }
905
906 return result;
907}
908
909std::string smt2_convt::type2id(const typet &type) const
910{
911 if(type.id()==ID_floatbv)
912 {
914 return "f"+std::to_string(spec.width())+"_"+std::to_string(spec.f);
915 }
916 else if(type.id()==ID_unsignedbv)
917 {
918 return "u"+std::to_string(to_unsignedbv_type(type).get_width());
919 }
920 else if(type.id()==ID_c_bool)
921 {
922 return "u"+std::to_string(to_c_bool_type(type).get_width());
923 }
924 else if(type.id()==ID_signedbv)
925 {
926 return "s"+std::to_string(to_signedbv_type(type).get_width());
927 }
928 else if(type.id()==ID_bool)
929 {
930 return "b";
931 }
932 else if(type.id()==ID_c_enum_tag)
933 {
934 return type2id(ns.follow_tag(to_c_enum_tag_type(type)).underlying_type());
935 }
936 else if(type.id() == ID_pointer)
937 {
938 return "p" + std::to_string(to_pointer_type(type).get_width());
939 }
940 else
941 {
943 }
944}
945
946std::string smt2_convt::floatbv_suffix(const exprt &expr) const
947{
948 PRECONDITION(!expr.operands().empty());
949 return "_" + type2id(to_multi_ary_expr(expr).op0().type()) + "->" +
950 type2id(expr.type());
951}
952
954{
956
957 if(expr.id()==ID_symbol)
958 {
959 const irep_idt &id = to_symbol_expr(expr).get_identifier();
960 out << '|' << convert_identifier(id) << '|';
961 return;
962 }
963
964 if(expr.id()==ID_smt2_symbol)
965 {
966 const irep_idt &id = to_smt2_symbol(expr).get_identifier();
967 out << id;
968 return;
969 }
970
971 INVARIANT(
972 !expr.operands().empty(), "non-symbol expressions shall have operands");
973
974 out << "(|float_bv." << expr.id()
975 << floatbv_suffix(expr)
976 << '|';
977
978 forall_operands(it, expr)
979 {
980 out << ' ';
981 convert_expr(*it);
982 }
983
984 out << ')';
985}
986
988{
989 // huge monster case split over expression id
990 if(expr.id()==ID_symbol)
991 {
992 const irep_idt &id = to_symbol_expr(expr).get_identifier();
993 DATA_INVARIANT(!id.empty(), "symbol must have identifier");
994 out << '|' << convert_identifier(id) << '|';
995 }
996 else if(expr.id()==ID_nondet_symbol)
997 {
999 DATA_INVARIANT(!id.empty(), "nondet symbol must have identifier");
1000 out << '|' << convert_identifier("nondet_"+id2string(id)) << '|';
1001 }
1002 else if(expr.id()==ID_smt2_symbol)
1003 {
1004 const irep_idt &id = to_smt2_symbol(expr).get_identifier();
1005 DATA_INVARIANT(!id.empty(), "smt2 symbol must have identifier");
1006 out << id;
1007 }
1008 else if(expr.id()==ID_typecast)
1009 {
1011 }
1012 else if(expr.id()==ID_floatbv_typecast)
1013 {
1015 }
1016 else if(expr.id()==ID_struct)
1017 {
1019 }
1020 else if(expr.id()==ID_union)
1021 {
1023 }
1024 else if(expr.id()==ID_constant)
1025 {
1027 }
1028 else if(expr.id() == ID_concatenation && expr.operands().size() == 1)
1029 {
1031 expr.type() == expr.operands().front().type(),
1032 "concatenation over a single operand should have matching types",
1033 expr.pretty());
1034
1035 convert_expr(expr.operands().front());
1036 }
1037 else if(expr.id()==ID_concatenation ||
1038 expr.id()==ID_bitand ||
1039 expr.id()==ID_bitor ||
1040 expr.id()==ID_bitxor ||
1041 expr.id()==ID_bitnand ||
1042 expr.id()==ID_bitnor)
1043 {
1045 expr.operands().size() >= 2,
1046 "given expression should have at least two operands",
1047 expr.id_string());
1048
1049 out << "(";
1050
1051 if(expr.id()==ID_concatenation)
1052 out << "concat";
1053 else if(expr.id()==ID_bitand)
1054 out << "bvand";
1055 else if(expr.id()==ID_bitor)
1056 out << "bvor";
1057 else if(expr.id()==ID_bitxor)
1058 out << "bvxor";
1059 else if(expr.id()==ID_bitnand)
1060 out << "bvnand";
1061 else if(expr.id()==ID_bitnor)
1062 out << "bvnor";
1063
1064 forall_operands(it, expr)
1065 {
1066 out << " ";
1067 flatten2bv(*it);
1068 }
1069
1070 out << ")";
1071 }
1072 else if(expr.id()==ID_bitnot)
1073 {
1074 const bitnot_exprt &bitnot_expr = to_bitnot_expr(expr);
1075
1076 if(bitnot_expr.type().id() == ID_vector)
1077 {
1078 if(use_datatypes)
1079 {
1080 const std::string &smt_typename = datatype_map.at(bitnot_expr.type());
1081
1082 // extract elements
1083 const vector_typet &vector_type = to_vector_type(bitnot_expr.type());
1084
1085 mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
1086
1087 out << "(let ((?vectorop ";
1088 convert_expr(bitnot_expr.op());
1089 out << ")) ";
1090
1091 out << "(mk-" << smt_typename;
1092
1093 typet index_type=vector_type.size().type();
1094
1095 // do bitnot component-by-component
1096 for(mp_integer i=0; i!=size; ++i)
1097 {
1098 out << " (bvnot (" << smt_typename << "." << (size-i-1)
1099 << " ?vectorop))";
1100 }
1101
1102 out << "))"; // mk-, let
1103 }
1104 else
1105 SMT2_TODO("bitnot for vectors");
1106 }
1107 else
1108 {
1109 out << "(bvnot ";
1110 convert_expr(bitnot_expr.op());
1111 out << ")";
1112 }
1113 }
1114 else if(expr.id()==ID_unary_minus)
1115 {
1116 const unary_minus_exprt &unary_minus_expr = to_unary_minus_expr(expr);
1117
1118 if(
1119 unary_minus_expr.type().id() == ID_rational ||
1120 unary_minus_expr.type().id() == ID_integer ||
1121 unary_minus_expr.type().id() == ID_real)
1122 {
1123 out << "(- ";
1124 convert_expr(unary_minus_expr.op());
1125 out << ")";
1126 }
1127 else if(unary_minus_expr.type().id() == ID_floatbv)
1128 {
1129 // this has no rounding mode
1130 if(use_FPA_theory)
1131 {
1132 out << "(fp.neg ";
1133 convert_expr(unary_minus_expr.op());
1134 out << ")";
1135 }
1136 else
1137 convert_floatbv(unary_minus_expr);
1138 }
1139 else if(unary_minus_expr.type().id() == ID_vector)
1140 {
1141 if(use_datatypes)
1142 {
1143 const std::string &smt_typename =
1144 datatype_map.at(unary_minus_expr.type());
1145
1146 // extract elements
1147 const vector_typet &vector_type =
1148 to_vector_type(unary_minus_expr.type());
1149
1150 mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
1151
1152 out << "(let ((?vectorop ";
1153 convert_expr(unary_minus_expr.op());
1154 out << ")) ";
1155
1156 out << "(mk-" << smt_typename;
1157
1158 typet index_type=vector_type.size().type();
1159
1160 // negate component-by-component
1161 for(mp_integer i=0; i!=size; ++i)
1162 {
1163 out << " (bvneg (" << smt_typename << "." << (size-i-1)
1164 << " ?vectorop))";
1165 }
1166
1167 out << "))"; // mk-, let
1168 }
1169 else
1170 SMT2_TODO("unary minus for vector");
1171 }
1172 else
1173 {
1174 out << "(bvneg ";
1175 convert_expr(unary_minus_expr.op());
1176 out << ")";
1177 }
1178 }
1179 else if(expr.id()==ID_unary_plus)
1180 {
1181 // A no-op (apart from type promotion)
1182 convert_expr(to_unary_plus_expr(expr).op());
1183 }
1184 else if(expr.id()==ID_sign)
1185 {
1186 const sign_exprt &sign_expr = to_sign_expr(expr);
1187
1188 const typet &op_type = sign_expr.op().type();
1189
1190 if(op_type.id()==ID_floatbv)
1191 {
1192 if(use_FPA_theory)
1193 {
1194 out << "(fp.isNegative ";
1195 convert_expr(sign_expr.op());
1196 out << ")";
1197 }
1198 else
1199 convert_floatbv(sign_expr);
1200 }
1201 else if(op_type.id()==ID_signedbv)
1202 {
1203 std::size_t op_width=to_signedbv_type(op_type).get_width();
1204
1205 out << "(bvslt ";
1206 convert_expr(sign_expr.op());
1207 out << " (_ bv0 " << op_width << "))";
1208 }
1209 else
1211 false,
1212 "sign should not be applied to unsupported type",
1213 sign_expr.type().id_string());
1214 }
1215 else if(expr.id()==ID_if)
1216 {
1217 const if_exprt &if_expr = to_if_expr(expr);
1218
1219 out << "(ite ";
1220 convert_expr(if_expr.cond());
1221 out << " ";
1222 convert_expr(if_expr.true_case());
1223 out << " ";
1224 convert_expr(if_expr.false_case());
1225 out << ")";
1226 }
1227 else if(expr.id()==ID_and ||
1228 expr.id()==ID_or ||
1229 expr.id()==ID_xor)
1230 {
1232 expr.type().id() == ID_bool,
1233 "logical and, or, and xor expressions should have Boolean type");
1235 expr.operands().size() >= 2,
1236 "logical and, or, and xor expressions should have at least two operands");
1237
1238 out << "(" << expr.id();
1239 forall_operands(it, expr)
1240 {
1241 out << " ";
1242 convert_expr(*it);
1243 }
1244 out << ")";
1245 }
1246 else if(expr.id()==ID_implies)
1247 {
1248 const implies_exprt &implies_expr = to_implies_expr(expr);
1249
1251 implies_expr.type().id() == ID_bool,
1252 "implies expression should have Boolean type");
1253
1254 out << "(=> ";
1255 convert_expr(implies_expr.op0());
1256 out << " ";
1257 convert_expr(implies_expr.op1());
1258 out << ")";
1259 }
1260 else if(expr.id()==ID_not)
1261 {
1262 const not_exprt &not_expr = to_not_expr(expr);
1263
1265 not_expr.type().id() == ID_bool,
1266 "not expression should have Boolean type");
1267
1268 out << "(not ";
1269 convert_expr(not_expr.op());
1270 out << ")";
1271 }
1272 else if(expr.id() == ID_equal)
1273 {
1274 const equal_exprt &equal_expr = to_equal_expr(expr);
1275
1277 equal_expr.op0().type() == equal_expr.op1().type(),
1278 "operands of equal expression shall have same type");
1279
1280 out << "(= ";
1281 convert_expr(equal_expr.op0());
1282 out << " ";
1283 convert_expr(equal_expr.op1());
1284 out << ")";
1285 }
1286 else if(expr.id() == ID_notequal)
1287 {
1288 const notequal_exprt &notequal_expr = to_notequal_expr(expr);
1289
1291 notequal_expr.op0().type() == notequal_expr.op1().type(),
1292 "operands of not equal expression shall have same type");
1293
1294 out << "(not (= ";
1295 convert_expr(notequal_expr.op0());
1296 out << " ";
1297 convert_expr(notequal_expr.op1());
1298 out << "))";
1299 }
1300 else if(expr.id()==ID_ieee_float_equal ||
1301 expr.id()==ID_ieee_float_notequal)
1302 {
1303 // These are not the same as (= A B)
1304 // because of NaN and negative zero.
1305 const auto &rel_expr = to_binary_relation_expr(expr);
1306
1308 rel_expr.lhs().type() == rel_expr.rhs().type(),
1309 "operands of float equal and not equal expressions shall have same type");
1310
1311 // The FPA theory properly treats NaN and negative zero.
1312 if(use_FPA_theory)
1313 {
1314 if(rel_expr.id() == ID_ieee_float_notequal)
1315 out << "(not ";
1316
1317 out << "(fp.eq ";
1318 convert_expr(rel_expr.lhs());
1319 out << " ";
1320 convert_expr(rel_expr.rhs());
1321 out << ")";
1322
1323 if(rel_expr.id() == ID_ieee_float_notequal)
1324 out << ")";
1325 }
1326 else
1327 convert_floatbv(expr);
1328 }
1329 else if(expr.id()==ID_le ||
1330 expr.id()==ID_lt ||
1331 expr.id()==ID_ge ||
1332 expr.id()==ID_gt)
1333 {
1335 }
1336 else if(expr.id()==ID_plus)
1337 {
1339 }
1340 else if(expr.id()==ID_floatbv_plus)
1341 {
1343 }
1344 else if(expr.id()==ID_minus)
1345 {
1347 }
1348 else if(expr.id()==ID_floatbv_minus)
1349 {
1351 }
1352 else if(expr.id()==ID_div)
1353 {
1354 convert_div(to_div_expr(expr));
1355 }
1356 else if(expr.id()==ID_floatbv_div)
1357 {
1359 }
1360 else if(expr.id()==ID_mod)
1361 {
1362 convert_mod(to_mod_expr(expr));
1363 }
1364 else if(expr.id() == ID_euclidean_mod)
1365 {
1367 }
1368 else if(expr.id()==ID_mult)
1369 {
1371 }
1372 else if(expr.id()==ID_floatbv_mult)
1373 {
1375 }
1376 else if(expr.id() == ID_floatbv_rem)
1377 {
1379 }
1380 else if(expr.id()==ID_address_of)
1381 {
1382 const address_of_exprt &address_of_expr = to_address_of_expr(expr);
1384 address_of_expr.object(), to_pointer_type(address_of_expr.type()));
1385 }
1386 else if(expr.id() == ID_array_of)
1387 {
1388 const auto &array_of_expr = to_array_of_expr(expr);
1389
1391 array_of_expr.type().id() == ID_array,
1392 "array of expression shall have array type");
1393
1394 if(use_as_const)
1395 {
1396 out << "((as const ";
1397 convert_type(array_of_expr.type());
1398 out << ") ";
1399 convert_expr(array_of_expr.what());
1400 out << ")";
1401 }
1402 else
1403 {
1404 defined_expressionst::const_iterator it =
1405 defined_expressions.find(array_of_expr);
1406 CHECK_RETURN(it != defined_expressions.end());
1407 out << it->second;
1408 }
1409 }
1410 else if(expr.id() == ID_array_comprehension)
1411 {
1412 const auto &array_comprehension = to_array_comprehension_expr(expr);
1413
1415 array_comprehension.type().id() == ID_array,
1416 "array_comprehension expression shall have array type");
1417
1419 {
1420 out << "(lambda ((";
1421 convert_expr(array_comprehension.arg());
1422 out << " ";
1423 convert_type(array_comprehension.type().size().type());
1424 out << ")) ";
1425 convert_expr(array_comprehension.body());
1426 out << ")";
1427 }
1428 else
1429 {
1430 const auto &it = defined_expressions.find(array_comprehension);
1431 CHECK_RETURN(it != defined_expressions.end());
1432 out << it->second;
1433 }
1434 }
1435 else if(expr.id()==ID_index)
1436 {
1438 }
1439 else if(expr.id()==ID_ashr ||
1440 expr.id()==ID_lshr ||
1441 expr.id()==ID_shl)
1442 {
1443 const shift_exprt &shift_expr = to_shift_expr(expr);
1444 const typet &type = shift_expr.type();
1445
1446 if(type.id()==ID_unsignedbv ||
1447 type.id()==ID_signedbv ||
1448 type.id()==ID_bv)
1449 {
1450 if(shift_expr.id() == ID_ashr)
1451 out << "(bvashr ";
1452 else if(shift_expr.id() == ID_lshr)
1453 out << "(bvlshr ";
1454 else if(shift_expr.id() == ID_shl)
1455 out << "(bvshl ";
1456 else
1458
1459 convert_expr(shift_expr.op());
1460 out << " ";
1461
1462 // SMT2 requires the shift distance to have the same width as
1463 // the value that is shifted -- odd!
1464
1465 if(shift_expr.distance().type().id() == ID_integer)
1466 {
1467 const mp_integer i =
1468 numeric_cast_v<mp_integer>(to_constant_expr(shift_expr.distance()));
1469
1470 // shift distance must be bit vector
1471 std::size_t width_op0 = boolbv_width(shift_expr.op().type());
1472 exprt tmp=from_integer(i, unsignedbv_typet(width_op0));
1473 convert_expr(tmp);
1474 }
1475 else if(
1476 shift_expr.distance().type().id() == ID_signedbv ||
1477 shift_expr.distance().type().id() == ID_unsignedbv ||
1478 shift_expr.distance().type().id() == ID_c_enum ||
1479 shift_expr.distance().type().id() == ID_c_bool)
1480 {
1481 std::size_t width_op0 = boolbv_width(shift_expr.op().type());
1482 std::size_t width_op1 = boolbv_width(shift_expr.distance().type());
1483
1484 if(width_op0==width_op1)
1485 convert_expr(shift_expr.distance());
1486 else if(width_op0>width_op1)
1487 {
1488 out << "((_ zero_extend " << width_op0-width_op1 << ") ";
1489 convert_expr(shift_expr.distance());
1490 out << ")"; // zero_extend
1491 }
1492 else // width_op0<width_op1
1493 {
1494 out << "((_ extract " << width_op0-1 << " 0) ";
1495 convert_expr(shift_expr.distance());
1496 out << ")"; // extract
1497 }
1498 }
1499 else
1501 "unsupported distance type for " + shift_expr.id_string() + ": " +
1502 type.id_string());
1503
1504 out << ")"; // bv*sh
1505 }
1506 else
1508 "unsupported type for " + shift_expr.id_string() + ": " +
1509 type.id_string());
1510 }
1511 else if(expr.id() == ID_rol || expr.id() == ID_ror)
1512 {
1513 const shift_exprt &shift_expr = to_shift_expr(expr);
1514 const typet &type = shift_expr.type();
1515
1516 if(
1517 type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
1518 type.id() == ID_bv)
1519 {
1520 // SMT-LIB offers rotate_left and rotate_right, but these require a
1521 // constant distance.
1522 if(shift_expr.id() == ID_rol)
1523 out << "((_ rotate_left";
1524 else if(shift_expr.id() == ID_ror)
1525 out << "((_ rotate_right";
1526 else
1528
1529 out << ' ';
1530
1531 auto distance_int_op = numeric_cast<mp_integer>(shift_expr.distance());
1532
1533 if(distance_int_op.has_value())
1534 {
1535 out << distance_int_op.value();
1536 }
1537 else
1539 "distance type for " + shift_expr.id_string() + "must be constant");
1540
1541 out << ") ";
1542 convert_expr(shift_expr.op());
1543
1544 out << ")"; // rotate_*
1545 }
1546 else
1548 "unsupported type for " + shift_expr.id_string() + ": " +
1549 type.id_string());
1550 }
1551 else if(expr.id()==ID_with)
1552 {
1554 }
1555 else if(expr.id()==ID_update)
1556 {
1557 convert_update(expr);
1558 }
1559 else if(expr.id()==ID_member)
1560 {
1562 }
1563 else if(expr.id()==ID_pointer_offset)
1564 {
1565 const auto &op = to_unary_expr(expr).op();
1566
1568 op.type().id() == ID_pointer,
1569 "operand of pointer offset expression shall be of pointer type");
1570
1571 std::size_t offset_bits =
1573 std::size_t result_width=boolbv_width(expr.type());
1574
1575 // max extract width
1576 if(offset_bits>result_width)
1577 offset_bits=result_width;
1578
1579 // too few bits?
1580 if(result_width>offset_bits)
1581 out << "((_ zero_extend " << result_width-offset_bits << ") ";
1582
1583 out << "((_ extract " << offset_bits-1 << " 0) ";
1584 convert_expr(op);
1585 out << ")";
1586
1587 if(result_width>offset_bits)
1588 out << ")"; // zero_extend
1589 }
1590 else if(expr.id()==ID_pointer_object)
1591 {
1592 const auto &op = to_unary_expr(expr).op();
1593
1595 op.type().id() == ID_pointer,
1596 "pointer object expressions should be of pointer type");
1597
1598 std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
1599 std::size_t pointer_width = boolbv_width(op.type());
1600
1601 if(ext>0)
1602 out << "((_ zero_extend " << ext << ") ";
1603
1604 out << "((_ extract "
1605 << pointer_width-1 << " "
1606 << pointer_width-config.bv_encoding.object_bits << ") ";
1607 convert_expr(op);
1608 out << ")";
1609
1610 if(ext>0)
1611 out << ")"; // zero_extend
1612 }
1613 else if(expr.id() == ID_is_dynamic_object)
1614 {
1616 }
1617 else if(expr.id() == ID_is_invalid_pointer)
1618 {
1619 const auto &op = to_unary_expr(expr).op();
1620 std::size_t pointer_width = boolbv_width(op.type());
1621 out << "(= ((_ extract "
1622 << pointer_width-1 << " "
1623 << pointer_width-config.bv_encoding.object_bits << ") ";
1624 convert_expr(op);
1625 out << ") (_ bv" << pointer_logic.get_invalid_object()
1626 << " " << config.bv_encoding.object_bits << "))";
1627 }
1628 else if(expr.id()==ID_string_constant)
1629 {
1630 defined_expressionst::const_iterator it=defined_expressions.find(expr);
1631 CHECK_RETURN(it != defined_expressions.end());
1632 out << it->second;
1633 }
1634 else if(expr.id()==ID_extractbit)
1635 {
1636 const extractbit_exprt &extractbit_expr = to_extractbit_expr(expr);
1637
1638 if(extractbit_expr.index().is_constant())
1639 {
1640 const mp_integer i =
1641 numeric_cast_v<mp_integer>(to_constant_expr(extractbit_expr.index()));
1642
1643 out << "(= ((_ extract " << i << " " << i << ") ";
1644 flatten2bv(extractbit_expr.src());
1645 out << ") #b1)";
1646 }
1647 else
1648 {
1649 out << "(= ((_ extract 0 0) ";
1650 // the arguments of the shift need to have the same width
1651 out << "(bvlshr ";
1652 flatten2bv(extractbit_expr.src());
1653 typecast_exprt tmp(extractbit_expr.index(), extractbit_expr.src().type());
1654 convert_expr(tmp);
1655 out << ")) bin1)"; // bvlshr, extract, =
1656 }
1657 }
1658 else if(expr.id()==ID_extractbits)
1659 {
1660 const extractbits_exprt &extractbits_expr = to_extractbits_expr(expr);
1661
1662 if(
1663 extractbits_expr.upper().is_constant() &&
1664 extractbits_expr.lower().is_constant())
1665 {
1666 mp_integer op1_i =
1667 numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.upper()));
1668 mp_integer op2_i =
1669 numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.lower()));
1670
1671 if(op2_i>op1_i)
1672 std::swap(op1_i, op2_i);
1673
1674 // now op1_i>=op2_i
1675
1676 out << "((_ extract " << op1_i << " " << op2_i << ") ";
1677 flatten2bv(extractbits_expr.src());
1678 out << ")";
1679 }
1680 else
1681 {
1682 #if 0
1683 out << "(= ((_ extract 0 0) ";
1684 // the arguments of the shift need to have the same width
1685 out << "(bvlshr ";
1686 convert_expr(expr.op0());
1687 typecast_exprt tmp(expr.op0().type());
1688 tmp.op0()=expr.op1();
1689 convert_expr(tmp);
1690 out << ")) bin1)"; // bvlshr, extract, =
1691 #endif
1692 SMT2_TODO("smt2: extractbits with non-constant index");
1693 }
1694 }
1695 else if(expr.id()==ID_replication)
1696 {
1697 const replication_exprt &replication_expr = to_replication_expr(expr);
1698
1699 mp_integer times = numeric_cast_v<mp_integer>(replication_expr.times());
1700
1701 out << "((_ repeat " << times << ") ";
1702 flatten2bv(replication_expr.op());
1703 out << ")";
1704 }
1705 else if(expr.id()==ID_byte_extract_little_endian ||
1706 expr.id()==ID_byte_extract_big_endian)
1707 {
1708 INVARIANT(
1709 false, "byte_extract ops should be lowered in prepare_for_convert_expr");
1710 }
1711 else if(expr.id()==ID_byte_update_little_endian ||
1712 expr.id()==ID_byte_update_big_endian)
1713 {
1714 INVARIANT(
1715 false, "byte_update ops should be lowered in prepare_for_convert_expr");
1716 }
1717 else if(expr.id()==ID_abs)
1718 {
1719 const abs_exprt &abs_expr = to_abs_expr(expr);
1720
1721 const typet &type = abs_expr.type();
1722
1723 if(type.id()==ID_signedbv)
1724 {
1725 std::size_t result_width = to_signedbv_type(type).get_width();
1726
1727 out << "(ite (bvslt ";
1728 convert_expr(abs_expr.op());
1729 out << " (_ bv0 " << result_width << ")) ";
1730 out << "(bvneg ";
1731 convert_expr(abs_expr.op());
1732 out << ") ";
1733 convert_expr(abs_expr.op());
1734 out << ")";
1735 }
1736 else if(type.id()==ID_fixedbv)
1737 {
1738 std::size_t result_width=to_fixedbv_type(type).get_width();
1739
1740 out << "(ite (bvslt ";
1741 convert_expr(abs_expr.op());
1742 out << " (_ bv0 " << result_width << ")) ";
1743 out << "(bvneg ";
1744 convert_expr(abs_expr.op());
1745 out << ") ";
1746 convert_expr(abs_expr.op());
1747 out << ")";
1748 }
1749 else if(type.id()==ID_floatbv)
1750 {
1751 if(use_FPA_theory)
1752 {
1753 out << "(fp.abs ";
1754 convert_expr(abs_expr.op());
1755 out << ")";
1756 }
1757 else
1758 convert_floatbv(abs_expr);
1759 }
1760 else
1762 }
1763 else if(expr.id()==ID_isnan)
1764 {
1765 const isnan_exprt &isnan_expr = to_isnan_expr(expr);
1766
1767 const typet &op_type = isnan_expr.op().type();
1768
1769 if(op_type.id()==ID_fixedbv)
1770 out << "false";
1771 else if(op_type.id()==ID_floatbv)
1772 {
1773 if(use_FPA_theory)
1774 {
1775 out << "(fp.isNaN ";
1776 convert_expr(isnan_expr.op());
1777 out << ")";
1778 }
1779 else
1780 convert_floatbv(isnan_expr);
1781 }
1782 else
1784 }
1785 else if(expr.id()==ID_isfinite)
1786 {
1787 const isfinite_exprt &isfinite_expr = to_isfinite_expr(expr);
1788
1789 const typet &op_type = isfinite_expr.op().type();
1790
1791 if(op_type.id()==ID_fixedbv)
1792 out << "true";
1793 else if(op_type.id()==ID_floatbv)
1794 {
1795 if(use_FPA_theory)
1796 {
1797 out << "(and ";
1798
1799 out << "(not (fp.isNaN ";
1800 convert_expr(isfinite_expr.op());
1801 out << "))";
1802
1803 out << "(not (fp.isInf ";
1804 convert_expr(isfinite_expr.op());
1805 out << "))";
1806
1807 out << ")";
1808 }
1809 else
1810 convert_floatbv(isfinite_expr);
1811 }
1812 else
1814 }
1815 else if(expr.id()==ID_isinf)
1816 {
1817 const isinf_exprt &isinf_expr = to_isinf_expr(expr);
1818
1819 const typet &op_type = isinf_expr.op().type();
1820
1821 if(op_type.id()==ID_fixedbv)
1822 out << "false";
1823 else if(op_type.id()==ID_floatbv)
1824 {
1825 if(use_FPA_theory)
1826 {
1827 out << "(fp.isInfinite ";
1828 convert_expr(isinf_expr.op());
1829 out << ")";
1830 }
1831 else
1832 convert_floatbv(isinf_expr);
1833 }
1834 else
1836 }
1837 else if(expr.id()==ID_isnormal)
1838 {
1839 const isnormal_exprt &isnormal_expr = to_isnormal_expr(expr);
1840
1841 const typet &op_type = isnormal_expr.op().type();
1842
1843 if(op_type.id()==ID_fixedbv)
1844 out << "true";
1845 else if(op_type.id()==ID_floatbv)
1846 {
1847 if(use_FPA_theory)
1848 {
1849 out << "(fp.isNormal ";
1850 convert_expr(isnormal_expr.op());
1851 out << ")";
1852 }
1853 else
1854 convert_floatbv(isnormal_expr);
1855 }
1856 else
1858 }
1859 else if(expr.id()==ID_overflow_plus ||
1860 expr.id()==ID_overflow_minus)
1861 {
1862 const auto &op0 = to_binary_expr(expr).op0();
1863 const auto &op1 = to_binary_expr(expr).op1();
1864
1866 expr.type().id() == ID_bool,
1867 "overflow plus and overflow minus expressions shall be of Boolean type");
1868
1869 bool subtract=expr.id()==ID_overflow_minus;
1870 const typet &op_type = op0.type();
1871 std::size_t width=boolbv_width(op_type);
1872
1873 if(op_type.id()==ID_signedbv)
1874 {
1875 // an overflow occurs if the top two bits of the extended sum differ
1876 out << "(let ((?sum (";
1877 out << (subtract?"bvsub":"bvadd");
1878 out << " ((_ sign_extend 1) ";
1879 convert_expr(op0);
1880 out << ")";
1881 out << " ((_ sign_extend 1) ";
1882 convert_expr(op1);
1883 out << ")))) "; // sign_extend, bvadd/sub let2
1884 out << "(not (= "
1885 "((_ extract " << width << " " << width << ") ?sum) "
1886 "((_ extract " << (width-1) << " " << (width-1) << ") ?sum)";
1887 out << ")))"; // =, not, let
1888 }
1889 else if(op_type.id()==ID_unsignedbv ||
1890 op_type.id()==ID_pointer)
1891 {
1892 // overflow is simply carry-out
1893 out << "(= ";
1894 out << "((_ extract " << width << " " << width << ") ";
1895 out << "(" << (subtract?"bvsub":"bvadd");
1896 out << " ((_ zero_extend 1) ";
1897 convert_expr(op0);
1898 out << ")";
1899 out << " ((_ zero_extend 1) ";
1900 convert_expr(op1);
1901 out << ")))"; // zero_extend, bvsub/bvadd, extract
1902 out << " #b1)"; // =
1903 }
1904 else
1906 false,
1907 "overflow check should not be performed on unsupported type",
1908 op_type.id_string());
1909 }
1910 else if(expr.id()==ID_overflow_mult)
1911 {
1912 const auto &op0 = to_binary_expr(expr).op0();
1913 const auto &op1 = to_binary_expr(expr).op1();
1914
1916 expr.type().id() == ID_bool,
1917 "overflow mult expression shall be of Boolean type");
1918
1919 // No better idea than to multiply with double the bits and then compare
1920 // with max value.
1921
1922 const typet &op_type = op0.type();
1923 std::size_t width=boolbv_width(op_type);
1924
1925 if(op_type.id()==ID_signedbv)
1926 {
1927 out << "(let ( (prod (bvmul ((_ sign_extend " << width << ") ";
1928 convert_expr(op0);
1929 out << ") ((_ sign_extend " << width << ") ";
1930 convert_expr(op1);
1931 out << ")) )) ";
1932 out << "(or (bvsge prod (_ bv" << power(2, width-1) << " "
1933 << width*2 << "))";
1934 out << " (bvslt prod (bvneg (_ bv" << power(2, width-1) << " "
1935 << width*2 << ")))))";
1936 }
1937 else if(op_type.id()==ID_unsignedbv)
1938 {
1939 out << "(bvuge (bvmul ((_ zero_extend " << width << ") ";
1940 convert_expr(op0);
1941 out << ") ((_ zero_extend " << width << ") ";
1942 convert_expr(op1);
1943 out << ")) (_ bv" << power(2, width) << " " << width*2 << "))";
1944 }
1945 else
1947 false,
1948 "overflow check should not be performed on unsupported type",
1949 op_type.id_string());
1950 }
1951 else if(expr.id()==ID_array)
1952 {
1953 defined_expressionst::const_iterator it=defined_expressions.find(expr);
1954 CHECK_RETURN(it != defined_expressions.end());
1955 out << it->second;
1956 }
1957 else if(expr.id()==ID_literal)
1958 {
1959 convert_literal(to_literal_expr(expr).get_literal());
1960 }
1961 else if(expr.id()==ID_forall ||
1962 expr.id()==ID_exists)
1963 {
1964 const quantifier_exprt &quantifier_expr = to_quantifier_expr(expr);
1965
1967 // NOLINTNEXTLINE(readability/throw)
1968 throw "MathSAT does not support quantifiers";
1969
1970 if(quantifier_expr.id() == ID_forall)
1971 out << "(forall ";
1972 else if(quantifier_expr.id() == ID_exists)
1973 out << "(exists ";
1974
1975 out << "( ";
1976 for(const auto &bound : quantifier_expr.variables())
1977 {
1978 out << "(";
1979 convert_expr(bound);
1980 out << " ";
1981 convert_type(bound.type());
1982 out << ") ";
1983 }
1984 out << ") ";
1985
1986 convert_expr(quantifier_expr.where());
1987
1988 out << ")";
1989 }
1990 else if(expr.id()==ID_vector)
1991 {
1992 const vector_exprt &vector_expr = to_vector_expr(expr);
1993 const vector_typet &vector_type = to_vector_type(vector_expr.type());
1994
1995 mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
1996
1998 size == vector_expr.operands().size(),
1999 "size indicated by type shall be equal to the number of operands");
2000
2001 if(use_datatypes)
2002 {
2003 const std::string &smt_typename = datatype_map.at(vector_type);
2004
2005 out << "(mk-" << smt_typename;
2006 }
2007 else
2008 out << "(concat";
2009
2010 // build component-by-component
2011 forall_operands(it, vector_expr)
2012 {
2013 out << " ";
2014 convert_expr(*it);
2015 }
2016
2017 out << ")"; // mk-... or concat
2018 }
2019 else if(expr.id()==ID_object_size)
2020 {
2021 out << "|" << object_sizes[expr] << "|";
2022 }
2023 else if(expr.id()==ID_let)
2024 {
2025 const let_exprt &let_expr=to_let_expr(expr);
2026 const auto &variables = let_expr.variables();
2027 const auto &values = let_expr.values();
2028
2029 out << "(let (";
2030 bool first = true;
2031
2032 for(auto &binding : make_range(variables).zip(values))
2033 {
2034 if(first)
2035 first = false;
2036 else
2037 out << ' ';
2038
2039 out << '(';
2040 convert_expr(binding.first);
2041 out << ' ';
2042 convert_expr(binding.second);
2043 out << ')';
2044 }
2045
2046 out << ") "; // bindings
2047
2048 convert_expr(let_expr.where());
2049 out << ')'; // let
2050 }
2051 else if(expr.id()==ID_constraint_select_one)
2052 {
2054 "smt2_convt::convert_expr: '" + expr.id_string() +
2055 "' is not yet supported");
2056 }
2057 else if(expr.id() == ID_bswap)
2058 {
2059 const bswap_exprt &bswap_expr = to_bswap_expr(expr);
2060
2062 bswap_expr.op().type() == bswap_expr.type(),
2063 "operand of byte swap expression shall have same type as the expression");
2064
2065 // first 'let' the operand
2066 out << "(let ((bswap_op ";
2067 convert_expr(bswap_expr.op());
2068 out << ")) ";
2069
2070 if(
2071 bswap_expr.type().id() == ID_signedbv ||
2072 bswap_expr.type().id() == ID_unsignedbv)
2073 {
2074 const std::size_t width =
2075 to_bitvector_type(bswap_expr.type()).get_width();
2076
2077 const std::size_t bits_per_byte = bswap_expr.get_bits_per_byte();
2078
2079 // width must be multiple of bytes
2081 width % bits_per_byte == 0,
2082 "bit width indicated by type of bswap expression should be a multiple "
2083 "of the number of bits per byte");
2084
2085 const std::size_t bytes = width / bits_per_byte;
2086
2087 if(bytes <= 1)
2088 out << "bswap_op";
2089 else
2090 {
2091 // do a parallel 'let' for each byte
2092 out << "(let (";
2093
2094 for(std::size_t byte = 0; byte < bytes; byte++)
2095 {
2096 if(byte != 0)
2097 out << ' ';
2098 out << "(bswap_byte_" << byte << ' ';
2099 out << "((_ extract " << (byte * bits_per_byte + (bits_per_byte - 1))
2100 << " " << (byte * bits_per_byte) << ") bswap_op)";
2101 out << ')';
2102 }
2103
2104 out << ") ";
2105
2106 // now stitch back together with 'concat'
2107 out << "(concat";
2108
2109 for(std::size_t byte = 0; byte < bytes; byte++)
2110 out << " bswap_byte_" << byte;
2111
2112 out << ')'; // concat
2113 out << ')'; // let bswap_byte_*
2114 }
2115 }
2116 else
2117 UNEXPECTEDCASE("bswap must get bitvector operand");
2118
2119 out << ')'; // let bswap_op
2120 }
2121 else if(expr.id() == ID_popcount)
2122 {
2124 }
2125 else if(expr.id() == ID_count_leading_zeros)
2126 {
2128 }
2129 else if(expr.id() == ID_count_trailing_zeros)
2130 {
2132 }
2133 else if(expr.id() == ID_empty_union)
2134 {
2135 out << "()";
2136 }
2137 else if(expr.id() == ID_bitreverse)
2138 {
2140 }
2141 else
2143 false,
2144 "smt2_convt::convert_expr should not be applied to unsupported type",
2145 expr.id_string());
2146}
2147
2149{
2150 const exprt &src = expr.op();
2151
2152 typet dest_type = expr.type();
2153 if(dest_type.id()==ID_c_enum_tag)
2154 dest_type=ns.follow_tag(to_c_enum_tag_type(dest_type));
2155
2156 typet src_type = src.type();
2157 if(src_type.id()==ID_c_enum_tag)
2158 src_type=ns.follow_tag(to_c_enum_tag_type(src_type));
2159
2160 if(dest_type.id()==ID_bool)
2161 {
2162 // this is comparison with zero
2163 if(src_type.id()==ID_signedbv ||
2164 src_type.id()==ID_unsignedbv ||
2165 src_type.id()==ID_c_bool ||
2166 src_type.id()==ID_fixedbv ||
2167 src_type.id()==ID_pointer ||
2168 src_type.id()==ID_integer)
2169 {
2170 out << "(not (= ";
2171 convert_expr(src);
2172 out << " ";
2173 convert_expr(from_integer(0, src_type));
2174 out << "))";
2175 }
2176 else if(src_type.id()==ID_floatbv)
2177 {
2178 if(use_FPA_theory)
2179 {
2180 out << "(not (fp.isZero ";
2181 convert_expr(src);
2182 out << "))";
2183 }
2184 else
2185 convert_floatbv(expr);
2186 }
2187 else
2188 {
2189 UNEXPECTEDCASE("TODO typecast1 "+src_type.id_string()+" -> bool");
2190 }
2191 }
2192 else if(dest_type.id()==ID_c_bool)
2193 {
2194 std::size_t to_width=boolbv_width(dest_type);
2195 out << "(ite ";
2196 out << "(not (= ";
2197 convert_expr(src);
2198 out << " ";
2199 convert_expr(from_integer(0, src_type));
2200 out << ")) "; // not, =
2201 out << " (_ bv1 " << to_width << ")";
2202 out << " (_ bv0 " << to_width << ")";
2203 out << ")"; // ite
2204 }
2205 else if(dest_type.id()==ID_signedbv ||
2206 dest_type.id()==ID_unsignedbv ||
2207 dest_type.id()==ID_c_enum ||
2208 dest_type.id()==ID_bv)
2209 {
2210 std::size_t to_width=boolbv_width(dest_type);
2211
2212 if(src_type.id()==ID_signedbv || // from signedbv
2213 src_type.id()==ID_unsignedbv || // from unsigedbv
2214 src_type.id()==ID_c_bool ||
2215 src_type.id()==ID_c_enum ||
2216 src_type.id()==ID_bv)
2217 {
2218 std::size_t from_width=boolbv_width(src_type);
2219
2220 if(from_width==to_width)
2221 convert_expr(src); // ignore
2222 else if(from_width<to_width) // extend
2223 {
2224 if(src_type.id()==ID_signedbv)
2225 out << "((_ sign_extend ";
2226 else
2227 out << "((_ zero_extend ";
2228
2229 out << (to_width-from_width)
2230 << ") "; // ind
2231 convert_expr(src);
2232 out << ")";
2233 }
2234 else // chop off extra bits
2235 {
2236 out << "((_ extract " << (to_width-1) << " 0) ";
2237 convert_expr(src);
2238 out << ")";
2239 }
2240 }
2241 else if(src_type.id()==ID_fixedbv) // from fixedbv to int
2242 {
2243 const fixedbv_typet &fixedbv_type=to_fixedbv_type(src_type);
2244
2245 std::size_t from_width=fixedbv_type.get_width();
2246 std::size_t from_integer_bits=fixedbv_type.get_integer_bits();
2247 std::size_t from_fraction_bits=fixedbv_type.get_fraction_bits();
2248
2249 // we might need to round up in case of negative numbers
2250 // e.g., (int)(-1.00001)==1
2251
2252 out << "(let ((?tcop ";
2253 convert_expr(src);
2254 out << ")) ";
2255
2256 out << "(bvadd ";
2257
2258 if(to_width>from_integer_bits)
2259 {
2260 out << "((_ sign_extend "
2261 << (to_width-from_integer_bits) << ") ";
2262 out << "((_ extract " << (from_width-1) << " "
2263 << from_fraction_bits << ") ";
2264 convert_expr(src);
2265 out << "))";
2266 }
2267 else
2268 {
2269 out << "((_ extract " << (from_fraction_bits+to_width-1)
2270 << " " << from_fraction_bits << ") ";
2271 convert_expr(src);
2272 out << ")";
2273 }
2274
2275 out << " (ite (and ";
2276
2277 // some fraction bit is not zero
2278 out << "(not (= ((_ extract " << (from_fraction_bits-1) << " 0) ?tcop) "
2279 "(_ bv0 " << from_fraction_bits << ")))";
2280
2281 // number negative
2282 out << " (= ((_ extract " << (from_width-1) << " " << (from_width-1)
2283 << ") ?tcop) #b1)";
2284
2285 out << ")"; // and
2286
2287 out << " (_ bv1 " << to_width << ") (_ bv0 " << to_width << "))"; // ite
2288 out << ")"; // bvadd
2289 out << ")"; // let
2290 }
2291 else if(src_type.id()==ID_floatbv) // from floatbv to int
2292 {
2293 if(dest_type.id()==ID_bv)
2294 {
2295 // this is _NOT_ a semantic conversion, but bit-wise
2296
2297 if(use_FPA_theory)
2298 {
2299 // This conversion is non-trivial as it requires creating a
2300 // new bit-vector variable and then asserting that it converts
2301 // to the required floating-point number.
2302 SMT2_TODO("bit-wise floatbv to bv");
2303 }
2304 else
2305 {
2306 // straight-forward if width matches
2307 convert_expr(src);
2308 }
2309 }
2310 else if(dest_type.id()==ID_signedbv)
2311 {
2312 // this should be floatbv_typecast, not typecast
2314 "typecast unexpected "+src_type.id_string()+" -> "+
2315 dest_type.id_string());
2316 }
2317 else if(dest_type.id()==ID_unsignedbv)
2318 {
2319 // this should be floatbv_typecast, not typecast
2321 "typecast unexpected "+src_type.id_string()+" -> "+
2322 dest_type.id_string());
2323 }
2324 }
2325 else if(src_type.id()==ID_bool) // from boolean to int
2326 {
2327 out << "(ite ";
2328 convert_expr(src);
2329
2330 if(dest_type.id()==ID_fixedbv)
2331 {
2332 fixedbv_spect spec(to_fixedbv_type(dest_type));
2333 out << " (concat (_ bv1 "
2334 << spec.integer_bits << ") " <<
2335 "(_ bv0 " << spec.get_fraction_bits() << ")) " <<
2336 "(_ bv0 " << spec.width << ")";
2337 }
2338 else
2339 {
2340 out << " (_ bv1 " << to_width << ")";
2341 out << " (_ bv0 " << to_width << ")";
2342 }
2343
2344 out << ")";
2345 }
2346 else if(src_type.id()==ID_pointer) // from pointer to int
2347 {
2348 std::size_t from_width=boolbv_width(src_type);
2349
2350 if(from_width<to_width) // extend
2351 {
2352 out << "((_ sign_extend ";
2353 out << (to_width-from_width)
2354 << ") ";
2355 convert_expr(src);
2356 out << ")";
2357 }
2358 else // chop off extra bits
2359 {
2360 out << "((_ extract " << (to_width-1) << " 0) ";
2361 convert_expr(src);
2362 out << ")";
2363 }
2364 }
2365 else if(src_type.id()==ID_integer) // from integer to bit-vector
2366 {
2367 // must be constant
2368 if(src.is_constant())
2369 {
2370 mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(src));
2371 out << "(_ bv" << i << " " << to_width << ")";
2372 }
2373 else
2374 SMT2_TODO("can't convert non-constant integer to bitvector");
2375 }
2376 else if(
2377 src_type.id() == ID_struct ||
2378 src_type.id() == ID_struct_tag) // flatten a struct to a bit-vector
2379 {
2380 if(use_datatypes)
2381 {
2382 INVARIANT(
2383 boolbv_width(src_type) == boolbv_width(dest_type),
2384 "bit vector with of source and destination type shall be equal");
2385 flatten2bv(src);
2386 }
2387 else
2388 {
2389 INVARIANT(
2390 boolbv_width(src_type) == boolbv_width(dest_type),
2391 "bit vector with of source and destination type shall be equal");
2392 convert_expr(src); // nothing else to do!
2393 }
2394 }
2395 else if(
2396 src_type.id() == ID_union ||
2397 src_type.id() == ID_union_tag) // flatten a union
2398 {
2399 INVARIANT(
2400 boolbv_width(src_type) == boolbv_width(dest_type),
2401 "bit vector with of source and destination type shall be equal");
2402 convert_expr(src); // nothing else to do!
2403 }
2404 else if(src_type.id()==ID_c_bit_field)
2405 {
2406 std::size_t from_width=boolbv_width(src_type);
2407
2408 if(from_width==to_width)
2409 convert_expr(src); // ignore
2410 else
2411 {
2413 typecast_exprt tmp(typecast_exprt(src, t), dest_type);
2414 convert_typecast(tmp);
2415 }
2416 }
2417 else
2418 {
2419 std::ostringstream e_str;
2420 e_str << src_type.id() << " -> " << dest_type.id()
2421 << " src == " << format(src);
2422 UNEXPECTEDCASE("TODO typecast2 " + e_str.str());
2423 }
2424 }
2425 else if(dest_type.id()==ID_fixedbv) // to fixedbv
2426 {
2427 const fixedbv_typet &fixedbv_type=to_fixedbv_type(dest_type);
2428 std::size_t to_fraction_bits=fixedbv_type.get_fraction_bits();
2429 std::size_t to_integer_bits=fixedbv_type.get_integer_bits();
2430
2431 if(src_type.id()==ID_unsignedbv ||
2432 src_type.id()==ID_signedbv ||
2433 src_type.id()==ID_c_enum)
2434 {
2435 // integer to fixedbv
2436
2437 std::size_t from_width=to_bitvector_type(src_type).get_width();
2438 out << "(concat ";
2439
2440 if(from_width==to_integer_bits)
2441 convert_expr(src);
2442 else if(from_width>to_integer_bits)
2443 {
2444 // too many integer bits
2445 out << "((_ extract " << (to_integer_bits-1) << " 0) ";
2446 convert_expr(src);
2447 out << ")";
2448 }
2449 else
2450 {
2451 // too few integer bits
2452 INVARIANT(
2453 from_width < to_integer_bits,
2454 "from_width should be smaller than to_integer_bits as other case "
2455 "have been handled above");
2456 if(dest_type.id()==ID_unsignedbv)
2457 {
2458 out << "(_ zero_extend "
2459 << (to_integer_bits-from_width) << ") ";
2460 convert_expr(src);
2461 out << ")";
2462 }
2463 else
2464 {
2465 out << "((_ sign_extend "
2466 << (to_integer_bits-from_width) << ") ";
2467 convert_expr(src);
2468 out << ")";
2469 }
2470 }
2471
2472 out << "(_ bv0 " << to_fraction_bits << ")";
2473 out << ")"; // concat
2474 }
2475 else if(src_type.id()==ID_bool) // bool to fixedbv
2476 {
2477 out << "(concat (concat"
2478 << " (_ bv0 " << (to_integer_bits-1) << ") ";
2479 flatten2bv(src); // produces #b0 or #b1
2480 out << ") (_ bv0 "
2481 << to_fraction_bits
2482 << "))";
2483 }
2484 else if(src_type.id()==ID_fixedbv) // fixedbv to fixedbv
2485 {
2486 const fixedbv_typet &from_fixedbv_type=to_fixedbv_type(src_type);
2487 std::size_t from_fraction_bits=from_fixedbv_type.get_fraction_bits();
2488 std::size_t from_integer_bits=from_fixedbv_type.get_integer_bits();
2489 std::size_t from_width=from_fixedbv_type.get_width();
2490
2491 out << "(let ((?tcop ";
2492 convert_expr(src);
2493 out << ")) ";
2494
2495 out << "(concat ";
2496
2497 if(to_integer_bits<=from_integer_bits)
2498 {
2499 out << "((_ extract "
2500 << (from_fraction_bits+to_integer_bits-1) << " "
2501 << from_fraction_bits
2502 << ") ?tcop)";
2503 }
2504 else
2505 {
2506 INVARIANT(
2507 to_integer_bits > from_integer_bits,
2508 "to_integer_bits should be greater than from_integer_bits as the"
2509 "other case has been handled above");
2510 out << "((_ sign_extend "
2511 << (to_integer_bits-from_integer_bits)
2512 << ") ((_ extract "
2513 << (from_width-1) << " "
2514 << from_fraction_bits
2515 << ") ?tcop))";
2516 }
2517
2518 out << " ";
2519
2520 if(to_fraction_bits<=from_fraction_bits)
2521 {
2522 out << "((_ extract "
2523 << (from_fraction_bits-1) << " "
2524 << (from_fraction_bits-to_fraction_bits)
2525 << ") ?tcop)";
2526 }
2527 else
2528 {
2529 INVARIANT(
2530 to_fraction_bits > from_fraction_bits,
2531 "to_fraction_bits should be greater than from_fraction_bits as the"
2532 "other case has been handled above");
2533 out << "(concat ((_ extract "
2534 << (from_fraction_bits-1) << " 0) ";
2535 convert_expr(src);
2536 out << ")"
2537 << " (_ bv0 " << to_fraction_bits-from_fraction_bits
2538 << "))";
2539 }
2540
2541 out << "))"; // concat, let
2542 }
2543 else
2544 UNEXPECTEDCASE("unexpected typecast to fixedbv");
2545 }
2546 else if(dest_type.id()==ID_pointer)
2547 {
2548 std::size_t to_width=boolbv_width(dest_type);
2549
2550 if(src_type.id()==ID_pointer) // pointer to pointer
2551 {
2552 // this just passes through
2553 convert_expr(src);
2554 }
2555 else if(
2556 src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv ||
2557 src_type.id() == ID_bv)
2558 {
2559 // integer to pointer
2560
2561 std::size_t from_width=boolbv_width(src_type);
2562
2563 if(from_width==to_width)
2564 convert_expr(src);
2565 else if(from_width<to_width)
2566 {
2567 out << "((_ sign_extend "
2568 << (to_width-from_width)
2569 << ") ";
2570 convert_expr(src);
2571 out << ")"; // sign_extend
2572 }
2573 else // from_width>to_width
2574 {
2575 out << "((_ extract " << to_width << " 0) ";
2576 convert_expr(src);
2577 out << ")"; // extract
2578 }
2579 }
2580 else
2581 UNEXPECTEDCASE("TODO typecast3 "+src_type.id_string()+" -> pointer");
2582 }
2583 else if(dest_type.id()==ID_range)
2584 {
2585 SMT2_TODO("range typecast");
2586 }
2587 else if(dest_type.id()==ID_floatbv)
2588 {
2589 // Typecast from integer to floating-point should have be been
2590 // converted to ID_floatbv_typecast during symbolic execution,
2591 // adding the rounding mode. See
2592 // smt2_convt::convert_floatbv_typecast.
2593 // The exception is bool and c_bool to float.
2594 const auto &dest_floatbv_type = to_floatbv_type(dest_type);
2595
2596 if(src_type.id()==ID_bool)
2597 {
2598 constant_exprt val(irep_idt(), dest_type);
2599
2600 ieee_floatt a(dest_floatbv_type);
2601
2602 mp_integer significand;
2603 mp_integer exponent;
2604
2605 out << "(ite ";
2606 convert_expr(src);
2607 out << " ";
2608
2609 significand = 1;
2610 exponent = 0;
2611 a.build(significand, exponent);
2612 val.set_value(integer2bvrep(a.pack(), a.spec.width()));
2613
2614 convert_constant(val);
2615 out << " ";
2616
2617 significand = 0;
2618 exponent = 0;
2619 a.build(significand, exponent);
2620 val.set_value(integer2bvrep(a.pack(), a.spec.width()));
2621
2622 convert_constant(val);
2623 out << ")";
2624 }
2625 else if(src_type.id()==ID_c_bool)
2626 {
2627 // turn into proper bool
2628 const typecast_exprt tmp(src, bool_typet());
2629 convert_typecast(typecast_exprt(tmp, dest_type));
2630 }
2631 else if(src_type.id() == ID_bv)
2632 {
2633 if(to_bv_type(src_type).get_width() != dest_floatbv_type.get_width())
2634 {
2635 UNEXPECTEDCASE("Typecast bv -> float with wrong width");
2636 }
2637
2638 if(use_FPA_theory)
2639 {
2640 out << "((_ to_fp " << dest_floatbv_type.get_e() << " "
2641 << dest_floatbv_type.get_f() + 1 << ") ";
2642 convert_expr(src);
2643 out << ')';
2644 }
2645 else
2646 convert_expr(src);
2647 }
2648 else
2649 UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
2650 }
2651 else if(dest_type.id()==ID_integer)
2652 {
2653 if(src_type.id()==ID_bool)
2654 {
2655 out << "(ite ";
2656 convert_expr(src);
2657 out <<" 1 0)";
2658 }
2659 else
2660 UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer");
2661 }
2662 else if(dest_type.id()==ID_c_bit_field)
2663 {
2664 std::size_t from_width=boolbv_width(src_type);
2665 std::size_t to_width=boolbv_width(dest_type);
2666
2667 if(from_width==to_width)
2668 convert_expr(src); // ignore
2669 else
2670 {
2672 typecast_exprt tmp(typecast_exprt(src, t), dest_type);
2673 convert_typecast(tmp);
2674 }
2675 }
2676 else
2678 "TODO typecast8 "+src_type.id_string()+" -> "+dest_type.id_string());
2679}
2680
2682{
2683 const exprt &src=expr.op();
2684 // const exprt &rounding_mode=expr.rounding_mode();
2685 const typet &src_type=src.type();
2686 const typet &dest_type=expr.type();
2687
2688 if(dest_type.id()==ID_floatbv)
2689 {
2690 if(src_type.id()==ID_floatbv)
2691 {
2692 // float to float
2693
2694 /* ISO 9899:1999
2695 * 6.3.1.5 Real floating types
2696 * 1 When a float is promoted to double or long double, or a
2697 * double is promoted to long double, its value is unchanged.
2698 *
2699 * 2 When a double is demoted to float, a long double is
2700 * demoted to double or float, or a value being represented in
2701 * greater precision and range than required by its semantic
2702 * type (see 6.3.1.8) is explicitly converted to its semantic
2703 * type, if the value being converted can be represented
2704 * exactly in the new type, it is unchanged. If the value
2705 * being converted is in the range of values that can be
2706 * represented but cannot be represented exactly, the result
2707 * is either the nearest higher or nearest lower representable
2708 * value, chosen in an implementation-defined manner. If the
2709 * value being converted is outside the range of values that
2710 * can be represented, the behavior is undefined.
2711 */
2712
2713 const floatbv_typet &dst=to_floatbv_type(dest_type);
2714
2715 if(use_FPA_theory)
2716 {
2717 out << "((_ to_fp " << dst.get_e() << " "
2718 << dst.get_f() + 1 << ") ";
2720 out << " ";
2721 convert_expr(src);
2722 out << ")";
2723 }
2724 else
2725 convert_floatbv(expr);
2726 }
2727 else if(src_type.id()==ID_unsignedbv)
2728 {
2729 // unsigned to float
2730
2731 /* ISO 9899:1999
2732 * 6.3.1.4 Real floating and integer
2733 * 2 When a value of integer type is converted to a real
2734 * floating type, if the value being converted can be
2735 * represented exactly in the new type, it is unchanged. If the
2736 * value being converted is in the range of values that can be
2737 * represented but cannot be represented exactly, the result is
2738 * either the nearest higher or nearest lower representable
2739 * value, chosen in an implementation-defined manner. If the
2740 * value being converted is outside the range of values that can
2741 * be represented, the behavior is undefined.
2742 */
2743
2744 const floatbv_typet &dst=to_floatbv_type(dest_type);
2745
2746 if(use_FPA_theory)
2747 {
2748 out << "((_ to_fp_unsigned " << dst.get_e() << " "
2749 << dst.get_f() + 1 << ") ";
2751 out << " ";
2752 convert_expr(src);
2753 out << ")";
2754 }
2755 else
2756 convert_floatbv(expr);
2757 }
2758 else if(src_type.id()==ID_signedbv)
2759 {
2760 // signed to float
2761
2762 const floatbv_typet &dst=to_floatbv_type(dest_type);
2763
2764 if(use_FPA_theory)
2765 {
2766 out << "((_ to_fp " << dst.get_e() << " "
2767 << dst.get_f() + 1 << ") ";
2769 out << " ";
2770 convert_expr(src);
2771 out << ")";
2772 }
2773 else
2774 convert_floatbv(expr);
2775 }
2776 else if(src_type.id()==ID_c_enum_tag)
2777 {
2778 // enum to float
2779
2780 // We first convert to 'underlying type'
2781 floatbv_typecast_exprt tmp=expr;
2782 tmp.op() = typecast_exprt(
2783 src, ns.follow_tag(to_c_enum_tag_type(src_type)).underlying_type());
2785 }
2786 else
2788 "TODO typecast11 "+src_type.id_string()+" -> "+dest_type.id_string());
2789 }
2790 else if(dest_type.id()==ID_signedbv)
2791 {
2792 if(use_FPA_theory)
2793 {
2794 std::size_t dest_width=to_signedbv_type(dest_type).get_width();
2795 out << "((_ fp.to_sbv " << dest_width << ") ";
2797 out << " ";
2798 convert_expr(src);
2799 out << ")";
2800 }
2801 else
2802 convert_floatbv(expr);
2803 }
2804 else if(dest_type.id()==ID_unsignedbv)
2805 {
2806 if(use_FPA_theory)
2807 {
2808 std::size_t dest_width=to_unsignedbv_type(dest_type).get_width();
2809 out << "((_ fp.to_ubv " << dest_width << ") ";
2811 out << " ";
2812 convert_expr(src);
2813 out << ")";
2814 }
2815 else
2816 convert_floatbv(expr);
2817 }
2818 else
2819 {
2821 "TODO typecast12 "+src_type.id_string()+" -> "+dest_type.id_string());
2822 }
2823}
2824
2826{
2827 const struct_typet &struct_type = to_struct_type(ns.follow(expr.type()));
2828
2829 const struct_typet::componentst &components=
2830 struct_type.components();
2831
2833 components.size() == expr.operands().size(),
2834 "number of struct components as indicated by the struct type shall be equal"
2835 "to the number of operands of the struct expression");
2836
2837 DATA_INVARIANT(!components.empty(), "struct shall have struct components");
2838
2839 if(use_datatypes)
2840 {
2841 const std::string &smt_typename = datatype_map.at(struct_type);
2842
2843 // use the constructor for the Z3 datatype
2844 out << "(mk-" << smt_typename;
2845
2846 std::size_t i=0;
2847 for(struct_typet::componentst::const_iterator
2848 it=components.begin();
2849 it!=components.end();
2850 it++, i++)
2851 {
2852 out << " ";
2853 convert_expr(expr.operands()[i]);
2854 }
2855
2856 out << ")";
2857 }
2858 else
2859 {
2860 if(components.size()==1)
2861 convert_expr(expr.op0());
2862 else
2863 {
2864 // SMT-LIB 2 concat is binary only
2865 for(std::size_t i=components.size(); i>1; i--)
2866 {
2867 out << "(concat ";
2868
2869 exprt op=expr.operands()[i-1];
2870
2871 // may need to flatten array-theory arrays in there
2872 if(op.type().id() == ID_array)
2873 flatten_array(op);
2874 else
2875 convert_expr(op);
2876
2877 out << " ";
2878 }
2879
2880 convert_expr(expr.op0());
2881
2882 for(std::size_t i=1; i<components.size(); i++)
2883 out << ")";
2884 }
2885 }
2886}
2887
2890{
2891 const array_typet &array_type = to_array_type(expr.type());
2892 const auto &size_expr = array_type.size();
2893 PRECONDITION(size_expr.id() == ID_constant);
2894
2895 mp_integer size = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
2896 CHECK_RETURN_WITH_DIAGNOSTICS(size != 0, "can't convert zero-sized array");
2897
2898 out << "(let ((?far ";
2899 convert_expr(expr);
2900 out << ")) ";
2901
2902 for(mp_integer i=size; i!=0; --i)
2903 {
2904 if(i!=1)
2905 out << "(concat ";
2906 out << "(select ?far ";
2907 convert_expr(from_integer(i-1, array_type.size().type()));
2908 out << ")";
2909 if(i!=1)
2910 out << " ";
2911 }
2912
2913 // close the many parentheses
2914 for(mp_integer i=size; i>1; --i)
2915 out << ")";
2916
2917 out << ")"; // let
2918}
2919
2921{
2922 const union_typet &union_type = to_union_type(ns.follow(expr.type()));
2923 const exprt &op=expr.op();
2924
2925 std::size_t total_width=boolbv_width(union_type);
2927 total_width != 0, "failed to get union width for union");
2928
2929 std::size_t member_width=boolbv_width(op.type());
2931 member_width != 0, "failed to get union member width for union");
2932
2933 if(total_width==member_width)
2934 {
2935 flatten2bv(op);
2936 }
2937 else
2938 {
2939 // we will pad with zeros, but non-det would be better
2940 INVARIANT(
2941 total_width > member_width,
2942 "total_width should be greater than member_width as member_width can be"
2943 "at most as large as total_width and the other case has been handled "
2944 "above");
2945 out << "(concat ";
2946 out << "(_ bv0 "
2947 << (total_width-member_width) << ") ";
2948 flatten2bv(op);
2949 out << ")";
2950 }
2951}
2952
2954{
2955 const typet &expr_type=expr.type();
2956
2957 if(expr_type.id()==ID_unsignedbv ||
2958 expr_type.id()==ID_signedbv ||
2959 expr_type.id()==ID_bv ||
2960 expr_type.id()==ID_c_enum ||
2961 expr_type.id()==ID_c_enum_tag ||
2962 expr_type.id()==ID_c_bool ||
2963 expr_type.id()==ID_c_bit_field)
2964 {
2965 const std::size_t width = boolbv_width(expr_type);
2966
2967 const mp_integer value = bvrep2integer(expr.get_value(), width, false);
2968
2969 out << "(_ bv" << value
2970 << " " << width << ")";
2971 }
2972 else if(expr_type.id()==ID_fixedbv)
2973 {
2974 const fixedbv_spect spec(to_fixedbv_type(expr_type));
2975
2976 const mp_integer v = bvrep2integer(expr.get_value(), spec.width, false);
2977
2978 out << "(_ bv" << v << " " << spec.width << ")";
2979 }
2980 else if(expr_type.id()==ID_floatbv)
2981 {
2982 const floatbv_typet &floatbv_type=
2983 to_floatbv_type(expr_type);
2984
2985 if(use_FPA_theory)
2986 {
2987 /* CBMC stores floating point literals in the most
2988 computationally useful form; biased exponents and
2989 significands including the hidden bit. Thus some encoding
2990 is needed to get to IEEE-754 style representations. */
2991
2992 ieee_floatt v=ieee_floatt(expr);
2993 size_t e=floatbv_type.get_e();
2994 size_t f=floatbv_type.get_f()+1;
2995
2996 /* Should be sufficient, but not currently supported by mathsat */
2997 #if 0
2998 mp_integer binary = v.pack();
2999
3000 out << "((_ to_fp " << e << " " << f << ")"
3001 << " #b" << integer2binary(v.pack(), v.spec.width()) << ")";
3002 #endif
3003
3004 if(v.is_NaN())
3005 {
3006 out << "(_ NaN " << e << " " << f << ")";
3007 }
3008 else if(v.is_infinity())
3009 {
3010 if(v.get_sign())
3011 out << "(_ -oo " << e << " " << f << ")";
3012 else
3013 out << "(_ +oo " << e << " " << f << ")";
3014 }
3015 else
3016 {
3017 // Zero, normal or subnormal
3018
3019 mp_integer binary = v.pack();
3020 std::string binaryString(integer2binary(v.pack(), v.spec.width()));
3021
3022 out << "(fp "
3023 << "#b" << binaryString.substr(0, 1) << " "
3024 << "#b" << binaryString.substr(1, e) << " "
3025 << "#b" << binaryString.substr(1+e, f-1) << ")";
3026 }
3027 }
3028 else
3029 {
3030 // produce corresponding bit-vector
3031 const ieee_float_spect spec(floatbv_type);
3032 const mp_integer v = bvrep2integer(expr.get_value(), spec.width(), false);
3033 out << "(_ bv" << v << " " << spec.width() << ")";
3034 }
3035 }
3036 else if(expr_type.id()==ID_pointer)
3037 {
3038 const irep_idt &value = expr.get_value();
3039
3040 if(value==ID_NULL)
3041 {
3042 out << "(_ bv0 " << boolbv_width(expr_type)
3043 << ")";
3044 }
3045 else
3046 UNEXPECTEDCASE("unknown pointer constant: "+id2string(value));
3047 }
3048 else if(expr_type.id()==ID_bool)
3049 {
3050 if(expr.is_true())
3051 out << "true";
3052 else if(expr.is_false())
3053 out << "false";
3054 else
3055 UNEXPECTEDCASE("unknown Boolean constant");
3056 }
3057 else if(expr_type.id()==ID_array)
3058 {
3059 defined_expressionst::const_iterator it=defined_expressions.find(expr);
3060 CHECK_RETURN(it != defined_expressions.end());
3061 out << it->second;
3062 }
3063 else if(expr_type.id()==ID_rational)
3064 {
3065 std::string value=id2string(expr.get_value());
3066 const bool negative = has_prefix(value, "-");
3067
3068 if(negative)
3069 out << "(- ";
3070
3071 size_t pos=value.find("/");
3072
3073 if(pos==std::string::npos)
3074 out << value << ".0";
3075 else
3076 {
3077 out << "(/ " << value.substr(0, pos) << ".0 "
3078 << value.substr(pos+1) << ".0)";
3079 }
3080
3081 if(negative)
3082 out << ')';
3083 }
3084 else if(expr_type.id()==ID_integer)
3085 {
3086 const auto value = id2string(expr.get_value());
3087
3088 // SMT2 has no negative integer literals
3089 if(has_prefix(value, "-"))
3090 out << "(- " << value.substr(1, std::string::npos) << ')';
3091 else
3092 out << value;
3093 }
3094 else
3095 UNEXPECTEDCASE("unknown constant: "+expr_type.id_string());
3096}
3097
3099{
3100 if(expr.type().id() == ID_integer)
3101 {
3102 out << "(mod ";
3103 convert_expr(expr.op0());
3104 out << ' ';
3105 convert_expr(expr.op1());
3106 out << ')';
3107 }
3108 else
3110 "unsupported type for euclidean_mod: " + expr.type().id_string());
3111}
3112
3114{
3115 if(expr.type().id()==ID_unsignedbv ||
3116 expr.type().id()==ID_signedbv)
3117 {
3118 if(expr.type().id()==ID_unsignedbv)
3119 out << "(bvurem ";
3120 else
3121 out << "(bvsrem ";
3122
3123 convert_expr(expr.op0());
3124 out << " ";
3125 convert_expr(expr.op1());
3126 out << ")";
3127 }
3128 else
3129 UNEXPECTEDCASE("unsupported type for mod: "+expr.type().id_string());
3130}
3131
3133{
3134 std::vector<std::size_t> dynamic_objects;
3135 pointer_logic.get_dynamic_objects(dynamic_objects);
3136
3137 if(dynamic_objects.empty())
3138 out << "false";
3139 else
3140 {
3141 std::size_t pointer_width = boolbv_width(expr.op().type());
3142
3143 out << "(let ((?obj ((_ extract "
3144 << pointer_width-1 << " "
3145 << pointer_width-config.bv_encoding.object_bits << ") ";
3146 convert_expr(expr.op());
3147 out << "))) ";
3148
3149 if(dynamic_objects.size()==1)
3150 {
3151 out << "(= (_ bv" << dynamic_objects.front()
3152 << " " << config.bv_encoding.object_bits << ") ?obj)";
3153 }
3154 else
3155 {
3156 out << "(or";
3157
3158 for(const auto &object : dynamic_objects)
3159 out << " (= (_ bv" << object
3160 << " " << config.bv_encoding.object_bits << ") ?obj)";
3161
3162 out << ")"; // or
3163 }
3164
3165 out << ")"; // let
3166 }
3167}
3168
3170{
3171 const typet &op_type=expr.op0().type();
3172
3173 if(op_type.id()==ID_unsignedbv ||
3174 op_type.id()==ID_bv)
3175 {
3176 out << "(";
3177 if(expr.id()==ID_le)
3178 out << "bvule";
3179 else if(expr.id()==ID_lt)
3180 out << "bvult";
3181 else if(expr.id()==ID_ge)
3182 out << "bvuge";
3183 else if(expr.id()==ID_gt)
3184 out << "bvugt";
3185
3186 out << " ";
3187 convert_expr(expr.op0());
3188 out << " ";
3189 convert_expr(expr.op1());
3190 out << ")";
3191 }
3192 else if(op_type.id()==ID_signedbv ||
3193 op_type.id()==ID_fixedbv)
3194 {
3195 out << "(";
3196 if(expr.id()==ID_le)
3197 out << "bvsle";
3198 else if(expr.id()==ID_lt)
3199 out << "bvslt";
3200 else if(expr.id()==ID_ge)
3201 out << "bvsge";
3202 else if(expr.id()==ID_gt)
3203 out << "bvsgt";
3204
3205 out << " ";
3206 convert_expr(expr.op0());
3207 out << " ";
3208 convert_expr(expr.op1());
3209 out << ")";
3210 }
3211 else if(op_type.id()==ID_floatbv)
3212 {
3213 if(use_FPA_theory)
3214 {
3215 out << "(";
3216 if(expr.id()==ID_le)
3217 out << "fp.leq";
3218 else if(expr.id()==ID_lt)
3219 out << "fp.lt";
3220 else if(expr.id()==ID_ge)
3221 out << "fp.geq";
3222 else if(expr.id()==ID_gt)
3223 out << "fp.gt";
3224
3225 out << " ";
3226 convert_expr(expr.op0());
3227 out << " ";
3228 convert_expr(expr.op1());
3229 out << ")";
3230 }
3231 else
3232 convert_floatbv(expr);
3233 }
3234 else if(op_type.id()==ID_rational ||
3235 op_type.id()==ID_integer)
3236 {
3237 out << "(";
3238 out << expr.id();
3239
3240 out << " ";
3241 convert_expr(expr.op0());
3242 out << " ";
3243 convert_expr(expr.op1());
3244 out << ")";
3245 }
3246 else if(op_type.id() == ID_pointer)
3247 {
3248 const exprt same_object = ::same_object(expr.op0(), expr.op1());
3249
3250 out << "(and ";
3252
3253 out << " (";
3254 if(expr.id() == ID_le)
3255 out << "bvsle";
3256 else if(expr.id() == ID_lt)
3257 out << "bvslt";
3258 else if(expr.id() == ID_ge)
3259 out << "bvsge";
3260 else if(expr.id() == ID_gt)
3261 out << "bvsgt";
3262
3263 out << ' ';
3265 out << ' ';
3267 out << ')';
3268
3269 out << ')';
3270 }
3271 else
3273 "unsupported type for "+expr.id_string()+": "+op_type.id_string());
3274}
3275
3277{
3278 if(
3279 expr.type().id() == ID_rational || expr.type().id() == ID_integer ||
3280 expr.type().id() == ID_real)
3281 {
3282 // these are multi-ary in SMT-LIB2
3283 out << "(+";
3284
3285 for(const auto &op : expr.operands())
3286 {
3287 out << ' ';
3288 convert_expr(op);
3289 }
3290
3291 out << ')';
3292 }
3293 else if(
3294 expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv ||
3295 expr.type().id() == ID_fixedbv)
3296 {
3297 // These could be chained, i.e., need not be binary,
3298 // but at least MathSat doesn't like that.
3299 if(expr.operands().size() == 2)
3300 {
3301 out << "(bvadd ";
3302 convert_expr(expr.op0());
3303 out << " ";
3304 convert_expr(expr.op1());
3305 out << ")";
3306 }
3307 else
3308 {
3310 }
3311 }
3312 else if(expr.type().id() == ID_floatbv)
3313 {
3314 // Floating-point additions should have be been converted
3315 // to ID_floatbv_plus during symbolic execution, adding
3316 // the rounding mode. See smt2_convt::convert_floatbv_plus.
3318 }
3319 else if(expr.type().id() == ID_pointer)
3320 {
3321 if(expr.operands().size() == 2)
3322 {
3323 exprt p = expr.op0(), i = expr.op1();
3324
3325 if(p.type().id() != ID_pointer)
3326 p.swap(i);
3327
3329 p.type().id() == ID_pointer,
3330 "one of the operands should have pointer type");
3331
3332 const auto &base_type = to_pointer_type(expr.type()).base_type();
3333
3334 mp_integer element_size;
3335 if(base_type.id() == ID_empty)
3336 {
3337 // This is a gcc extension.
3338 // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
3339 element_size = 1;
3340 }
3341 else
3342 {
3343 auto element_size_opt = pointer_offset_size(base_type, ns);
3344 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3345 element_size = *element_size_opt;
3346 }
3347
3348 out << "(bvadd ";
3349 convert_expr(p);
3350 out << " ";
3351
3352 if(element_size >= 2)
3353 {
3354 out << "(bvmul ";
3355 convert_expr(i);
3356 out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
3357 << "))";
3358 }
3359 else
3360 convert_expr(i);
3361
3362 out << ')';
3363 }
3364 else
3365 {
3367 }
3368 }
3369 else if(expr.type().id() == ID_vector)
3370 {
3371 const vector_typet &vector_type = to_vector_type(expr.type());
3372
3373 mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
3374
3375 typet index_type = vector_type.size().type();
3376
3377 if(use_datatypes)
3378 {
3379 const std::string &smt_typename = datatype_map.at(vector_type);
3380
3381 out << "(mk-" << smt_typename;
3382 }
3383 else
3384 out << "(concat";
3385
3386 // add component-by-component
3387 for(mp_integer i = 0; i != size; ++i)
3388 {
3389 exprt::operandst summands;
3390 summands.reserve(expr.operands().size());
3391 for(const auto &op : expr.operands())
3392 summands.push_back(index_exprt(
3393 op,
3394 from_integer(size - i - 1, index_type),
3395 vector_type.element_type()));
3396
3397 plus_exprt tmp(std::move(summands), vector_type.element_type());
3398
3399 out << " ";
3400 convert_expr(tmp);
3401 }
3402
3403 out << ")"; // mk-... or concat
3404 }
3405 else
3406 UNEXPECTEDCASE("unsupported type for +: " + expr.type().id_string());
3407}
3408
3413{
3415
3416 /* CProver uses the x86 numbering of the rounding-mode
3417 * 0 == FE_TONEAREST
3418 * 1 == FE_DOWNWARD
3419 * 2 == FE_UPWARD
3420 * 3 == FE_TOWARDZERO
3421 * These literal values must be used rather than the macros
3422 * the macros from fenv.h to avoid portability problems.
3423 */
3424
3425 if(expr.id()==ID_constant)
3426 {
3427 const constant_exprt &cexpr=to_constant_expr(expr);
3428
3429 mp_integer value = numeric_cast_v<mp_integer>(cexpr);
3430
3431 if(value==0)
3432 out << "roundNearestTiesToEven";
3433 else if(value==1)
3434 out << "roundTowardNegative";
3435 else if(value==2)
3436 out << "roundTowardPositive";
3437 else if(value==3)
3438 out << "roundTowardZero";
3439 else
3441 false,
3442 "Rounding mode should have value 0, 1, 2, or 3",
3443 id2string(cexpr.get_value()));
3444 }
3445 else
3446 {
3447 std::size_t width=to_bitvector_type(expr.type()).get_width();
3448
3449 // Need to make the choice above part of the model
3450 out << "(ite (= (_ bv0 " << width << ") ";
3451 convert_expr(expr);
3452 out << ") roundNearestTiesToEven ";
3453
3454 out << "(ite (= (_ bv1 " << width << ") ";
3455 convert_expr(expr);
3456 out << ") roundTowardNegative ";
3457
3458 out << "(ite (= (_ bv2 " << width << ") ";
3459 convert_expr(expr);
3460 out << ") roundTowardPositive ";
3461
3462 // TODO: add some kind of error checking here
3463 out << "roundTowardZero";
3464
3465 out << ")))";
3466 }
3467}
3468
3470{
3471 const typet &type=expr.type();
3472
3474 type.id() == ID_floatbv ||
3475 (type.id() == ID_complex &&
3476 to_complex_type(type).subtype().id() == ID_floatbv) ||
3477 (type.id() == ID_vector &&
3478 to_vector_type(type).element_type().id() == ID_floatbv));
3479
3480 if(use_FPA_theory)
3481 {
3482 if(type.id()==ID_floatbv)
3483 {
3484 out << "(fp.add ";
3486 out << " ";
3487 convert_expr(expr.lhs());
3488 out << " ";
3489 convert_expr(expr.rhs());
3490 out << ")";
3491 }
3492 else if(type.id()==ID_complex)
3493 {
3494 SMT2_TODO("+ for floatbv complex");
3495 }
3496 else if(type.id()==ID_vector)
3497 {
3498 SMT2_TODO("+ for floatbv vector");
3499 }
3500 else
3502 false,
3503 "type should not be one of the unsupported types",
3504 type.id_string());
3505 }
3506 else
3507 convert_floatbv(expr);
3508}
3509
3511{
3512 if(expr.type().id()==ID_integer)
3513 {
3514 out << "(- ";
3515 convert_expr(expr.op0());
3516 out << " ";
3517 convert_expr(expr.op1());
3518 out << ")";
3519 }
3520 else if(expr.type().id()==ID_unsignedbv ||
3521 expr.type().id()==ID_signedbv ||
3522 expr.type().id()==ID_fixedbv)
3523 {
3524 if(expr.op0().type().id()==ID_pointer &&
3525 expr.op1().type().id()==ID_pointer)
3526 {
3527 // Pointer difference
3528 auto element_size =
3530 CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3531
3532 if(*element_size >= 2)
3533 out << "(bvsdiv ";
3534
3535 INVARIANT(
3536 boolbv_width(expr.op0().type()) == boolbv_width(expr.type()),
3537 "bitvector width of operand shall be equal to the bitvector width of "
3538 "the expression");
3539
3540 out << "(bvsub ";
3541 convert_expr(expr.op0());
3542 out << " ";
3543 convert_expr(expr.op1());
3544 out << ")";
3545
3546 if(*element_size >= 2)
3547 out << " (_ bv" << *element_size << " " << boolbv_width(expr.type())
3548 << "))";
3549 }
3550 else
3551 {
3552 out << "(bvsub ";
3553 convert_expr(expr.op0());
3554 out << " ";
3555 convert_expr(expr.op1());
3556 out << ")";
3557 }
3558 }
3559 else if(expr.type().id()==ID_floatbv)
3560 {
3561 // Floating-point subtraction should have be been converted
3562 // to ID_floatbv_minus during symbolic execution, adding
3563 // the rounding mode. See smt2_convt::convert_floatbv_minus.
3565 }
3566 else if(expr.type().id()==ID_pointer)
3567 {
3568 SMT2_TODO("pointer subtraction");
3569 }
3570 else if(expr.type().id()==ID_vector)
3571 {
3572 const vector_typet &vector_type=to_vector_type(expr.type());
3573
3574 mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
3575
3576 typet index_type=vector_type.size().type();
3577
3578 if(use_datatypes)
3579 {
3580 const std::string &smt_typename = datatype_map.at(vector_type);
3581
3582 out << "(mk-" << smt_typename;
3583 }
3584 else
3585 out << "(concat";
3586
3587 // subtract component-by-component
3588 for(mp_integer i=0; i!=size; ++i)
3589 {
3590 exprt tmp(ID_minus, vector_type.element_type());
3591 forall_operands(it, expr)
3593 *it,
3594 from_integer(size - i - 1, index_type),
3595 vector_type.element_type()));
3596
3597 out << " ";
3598 convert_expr(tmp);
3599 }
3600
3601 out << ")"; // mk-... or concat
3602 }
3603 else
3604 UNEXPECTEDCASE("unsupported type for -: "+expr.type().id_string());
3605}
3606
3608{
3610 expr.type().id() == ID_floatbv,
3611 "type of ieee floating point expression shall be floatbv");
3612
3613 if(use_FPA_theory)
3614 {
3615 out << "(fp.sub ";
3617 out << " ";
3618 convert_expr(expr.lhs());
3619 out << " ";
3620 convert_expr(expr.rhs());
3621 out << ")";
3622 }
3623 else
3624 convert_floatbv(expr);
3625}
3626
3628{
3629 if(expr.type().id()==ID_unsignedbv ||
3630 expr.type().id()==ID_signedbv)
3631 {
3632 if(expr.type().id()==ID_unsignedbv)
3633 out << "(bvudiv ";
3634 else
3635 out << "(bvsdiv ";
3636
3637 convert_expr(expr.op0());
3638 out << " ";
3639 convert_expr(expr.op1());
3640 out << ")";
3641 }
3642 else if(expr.type().id()==ID_fixedbv)
3643 {
3644 fixedbv_spect spec(to_fixedbv_type(expr.type()));
3645 std::size_t fraction_bits=spec.get_fraction_bits();
3646
3647 out << "((_ extract " << spec.width-1 << " 0) ";
3648 out << "(bvsdiv ";
3649
3650 out << "(concat ";
3651 convert_expr(expr.op0());
3652 out << " (_ bv0 " << fraction_bits << ")) ";
3653
3654 out << "((_ sign_extend " << fraction_bits << ") ";
3655 convert_expr(expr.op1());
3656 out << ")";
3657
3658 out << "))";
3659 }
3660 else if(expr.type().id()==ID_floatbv)
3661 {
3662 // Floating-point division should have be been converted
3663 // to ID_floatbv_div during symbolic execution, adding
3664 // the rounding mode. See smt2_convt::convert_floatbv_div.
3666 }
3667 else
3668 UNEXPECTEDCASE("unsupported type for /: "+expr.type().id_string());
3669}
3670
3672{
3674 expr.type().id() == ID_floatbv,
3675 "type of ieee floating point expression shall be floatbv");
3676
3677 if(use_FPA_theory)
3678 {
3679 out << "(fp.div ";
3681 out << " ";
3682 convert_expr(expr.lhs());
3683 out << " ";
3684 convert_expr(expr.rhs());
3685 out << ")";
3686 }
3687 else
3688 convert_floatbv(expr);
3689}
3690
3692{
3693 // re-write to binary if needed
3694 if(expr.operands().size()>2)
3695 {
3696 // strip last operand
3697 exprt tmp=expr;
3698 tmp.operands().pop_back();
3699
3700 // recursive call
3701 return convert_mult(mult_exprt(tmp, expr.operands().back()));
3702 }
3703
3704 INVARIANT(
3705 expr.operands().size() == 2,
3706 "expression should have been converted to a variant with two operands");
3707
3708 if(expr.type().id()==ID_unsignedbv ||
3709 expr.type().id()==ID_signedbv)
3710 {
3711 // Note that bvmul is really unsigned,
3712 // but this is irrelevant as we chop-off any extra result
3713 // bits.
3714 out << "(bvmul ";
3715 convert_expr(expr.op0());
3716 out << " ";
3717 convert_expr(expr.op1());
3718 out << ")";
3719 }
3720 else if(expr.type().id()==ID_floatbv)
3721 {
3722 // Floating-point multiplication should have be been converted
3723 // to ID_floatbv_mult during symbolic execution, adding
3724 // the rounding mode. See smt2_convt::convert_floatbv_mult.
3726 }
3727 else if(expr.type().id()==ID_fixedbv)
3728 {
3729 fixedbv_spect spec(to_fixedbv_type(expr.type()));
3730 std::size_t fraction_bits=spec.get_fraction_bits();
3731
3732 out << "((_ extract "
3733 << spec.width+fraction_bits-1 << " "
3734 << fraction_bits << ") ";
3735
3736 out << "(bvmul ";
3737
3738 out << "((_ sign_extend " << fraction_bits << ") ";
3739 convert_expr(expr.op0());
3740 out << ") ";
3741
3742 out << "((_ sign_extend " << fraction_bits << ") ";
3743 convert_expr(expr.op1());
3744 out << ")";
3745
3746 out << "))"; // bvmul, extract
3747 }
3748 else if(expr.type().id()==ID_rational ||
3749 expr.type().id()==ID_integer ||
3750 expr.type().id()==ID_real)
3751 {
3752 out << "(*";
3753
3754 forall_operands(it, expr)
3755 {
3756 out << " ";
3757 convert_expr(*it);
3758 }
3759
3760 out << ")";
3761 }
3762 else
3763 UNEXPECTEDCASE("unsupported type for *: "+expr.type().id_string());
3764}
3765
3767{
3769 expr.type().id() == ID_floatbv,
3770 "type of ieee floating point expression shall be floatbv");
3771
3772 if(use_FPA_theory)
3773 {
3774 out << "(fp.mul ";
3776 out << " ";
3777 convert_expr(expr.lhs());
3778 out << " ";
3779 convert_expr(expr.rhs());
3780 out << ")";
3781 }
3782 else
3783 convert_floatbv(expr);
3784}
3785
3787{
3789 expr.type().id() == ID_floatbv,
3790 "type of ieee floating point expression shall be floatbv");
3791
3792 if(use_FPA_theory)
3793 {
3794 // Note that these do not have a rounding mode
3795 out << "(fp.rem ";
3796 convert_expr(expr.lhs());
3797 out << " ";
3798 convert_expr(expr.rhs());
3799 out << ")";
3800 }
3801 else
3802 {
3803 SMT2_TODO(
3804 "smt2_convt::convert_floatbv_rem to be implemented when not using "
3805 "FPA_theory");
3806 }
3807}
3808
3810{
3811 // get rid of "with" that has more than three operands
3812
3813 if(expr.operands().size()>3)
3814 {
3815 std::size_t s=expr.operands().size();
3816
3817 // strip off the trailing two operands
3818 with_exprt tmp = expr;
3819 tmp.operands().resize(s-2);
3820
3821 with_exprt new_with_expr(
3822 tmp, expr.operands()[s - 2], expr.operands().back());
3823
3824 // recursive call
3825 return convert_with(new_with_expr);
3826 }
3827
3828 INVARIANT(
3829 expr.operands().size() == 3,
3830 "with expression should have been converted to a version with three "
3831 "operands above");
3832
3833 const typet &expr_type = expr.type();
3834
3835 if(expr_type.id()==ID_array)
3836 {
3837 const array_typet &array_type=to_array_type(expr_type);
3838
3839 if(use_array_theory(expr))
3840 {
3841 out << "(store ";
3842 convert_expr(expr.old());
3843 out << " ";
3844 convert_expr(typecast_exprt(expr.where(), array_type.size().type()));
3845 out << " ";
3846 convert_expr(expr.new_value());
3847 out << ")";
3848 }
3849 else
3850 {
3851 // fixed-width
3852 std::size_t array_width=boolbv_width(array_type);
3853 std::size_t sub_width = boolbv_width(array_type.element_type());
3854 std::size_t index_width=boolbv_width(expr.where().type());
3855
3856 // We mask out the updated bits with AND,
3857 // and then OR-in the shifted new value.
3858
3859 out << "(let ((distance? ";
3860 out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
3861
3862 // SMT2 says that the shift distance needs to be as wide
3863 // as the stuff we are shifting.
3864 if(array_width>index_width)
3865 {
3866 out << "((_ zero_extend " << array_width-index_width << ") ";
3867 convert_expr(expr.where());
3868 out << ")";
3869 }
3870 else
3871 {
3872 out << "((_ extract " << array_width-1 << " 0) ";
3873 convert_expr(expr.where());
3874 out << ")";
3875 }
3876
3877 out << "))) "; // bvmul, distance?
3878
3879 out << "(bvor ";
3880 out << "(bvand ";
3881 out << "(bvnot ";
3882 out << "(bvshl (_ bv" << power(2, sub_width) - 1 << " " << array_width
3883 << ") ";
3884 out << "distance?)) "; // bvnot, bvlshl
3885 convert_expr(expr.old());
3886 out << ") "; // bvand
3887 out << "(bvshl ";
3888 out << "((_ zero_extend " << array_width-sub_width << ") ";
3889 convert_expr(expr.new_value());
3890 out << ") distance?)))"; // zero_extend, bvshl, bvor, let
3891 }
3892 }
3893 else if(expr_type.id() == ID_struct || expr_type.id() == ID_struct_tag)
3894 {
3895 const struct_typet &struct_type = to_struct_type(ns.follow(expr_type));
3896
3897 const exprt &index = expr.where();
3898 const exprt &value = expr.new_value();
3899
3900 const irep_idt &component_name=index.get(ID_component_name);
3901
3902 INVARIANT(
3903 struct_type.has_component(component_name),
3904 "struct should have accessed component");
3905
3906 if(use_datatypes)
3907 {
3908 const std::string &smt_typename = datatype_map.at(expr_type);
3909
3910 out << "(update-" << smt_typename << "." << component_name << " ";
3911 convert_expr(expr.old());
3912 out << " ";
3913 convert_expr(value);
3914 out << ")";
3915 }
3916 else
3917 {
3918 std::size_t struct_width=boolbv_width(struct_type);
3919
3920 // figure out the offset and width of the member
3922 boolbv_width.get_member(struct_type, component_name);
3923
3924 out << "(let ((?withop ";
3925 convert_expr(expr.old());
3926 out << ")) ";
3927
3928 if(m.width==struct_width)
3929 {
3930 // the struct is the same as the member, no concat needed,
3931 // ?withop won't be used
3932 convert_expr(value);
3933 }
3934 else if(m.offset==0)
3935 {
3936 // the member is at the beginning
3937 out << "(concat "
3938 << "((_ extract " << (struct_width-1) << " "
3939 << m.width << ") ?withop) ";
3940 convert_expr(value);
3941 out << ")"; // concat
3942 }
3943 else if(m.offset+m.width==struct_width)
3944 {
3945 // the member is at the end
3946 out << "(concat ";
3947 convert_expr(value);
3948 out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))";
3949 }
3950 else
3951 {
3952 // most general case, need two concat-s
3953 out << "(concat (concat "
3954 << "((_ extract " << (struct_width-1) << " "
3955 << (m.offset+m.width) << ") ?withop) ";
3956 convert_expr(value);
3957 out << ") ((_ extract " << (m.offset-1) << " 0) ?withop)";
3958 out << ")"; // concat
3959 }
3960
3961 out << ")"; // let ?withop
3962 }
3963 }
3964 else if(expr_type.id() == ID_union || expr_type.id() == ID_union_tag)
3965 {
3966 const union_typet &union_type = to_union_type(ns.follow(expr_type));
3967
3968 const exprt &value = expr.new_value();
3969
3970 std::size_t total_width=boolbv_width(union_type);
3972 total_width != 0, "failed to get union width for with");
3973
3974 std::size_t member_width=boolbv_width(value.type());
3976 member_width != 0, "failed to get union member width for with");
3977
3978 if(total_width==member_width)
3979 {
3980 flatten2bv(value);
3981 }
3982 else
3983 {
3984 INVARIANT(
3985 total_width > member_width,
3986 "total width should be greater than member_width as member_width is at "
3987 "most as large as total_width and the other case has been handled "
3988 "above");
3989 out << "(concat ";
3990 out << "((_ extract "
3991 << (total_width-1)
3992 << " " << member_width << ") ";
3993 convert_expr(expr.old());
3994 out << ") ";
3995 flatten2bv(value);
3996 out << ")";
3997 }
3998 }
3999 else if(expr_type.id()==ID_bv ||
4000 expr_type.id()==ID_unsignedbv ||
4001 expr_type.id()==ID_signedbv)
4002 {
4003 // Update bits in a bit-vector. We will use masking and shifts.
4004
4005 std::size_t total_width=boolbv_width(expr_type);
4007 total_width != 0, "failed to get total width");
4008
4009 const exprt &index=expr.operands()[1];
4010 const exprt &value=expr.operands()[2];
4011
4012 std::size_t value_width=boolbv_width(value.type());
4014 value_width != 0, "failed to get value width");
4015
4016 typecast_exprt index_tc(index, expr_type);
4017
4018 // TODO: SMT2-ify
4019 SMT2_TODO("SMT2-ify");
4020
4021#if 0
4022 out << "(bvor ";
4023 out << "(band ";
4024
4025 // the mask to get rid of the old bits
4026 out << " (bvnot (bvshl";
4027
4028 out << " (concat";
4029 out << " (repeat[" << total_width-value_width << "] bv0[1])";
4030 out << " (repeat[" << value_width << "] bv1[1])";
4031 out << ")"; // concat
4032
4033 // shift it to the index
4034 convert_expr(index_tc);
4035 out << "))"; // bvshl, bvot
4036
4037 out << ")"; // bvand
4038
4039 // the new value
4040 out << " (bvshl ";
4041 convert_expr(value);
4042
4043 // shift it to the index
4044 convert_expr(index_tc);
4045 out << ")"; // bvshl
4046
4047 out << ")"; // bvor
4048#endif
4049 }
4050 else
4052 "with expects struct, union, or array type, but got "+
4053 expr.type().id_string());
4054}
4055
4057{
4058 PRECONDITION(expr.operands().size() == 3);
4059
4060 SMT2_TODO("smt2_convt::convert_update to be implemented");
4061}
4062
4064{
4065 const typet &array_op_type = expr.array().type();
4066
4067 if(array_op_type.id()==ID_array)
4068 {
4069 const array_typet &array_type=to_array_type(array_op_type);
4070
4071 if(use_array_theory(expr.array()))
4072 {
4073 if(expr.type().id() == ID_bool && !use_array_of_bool)
4074 {
4075 out << "(= ";
4076 out << "(select ";
4077 convert_expr(expr.array());
4078 out << " ";
4079 convert_expr(typecast_exprt(expr.index(), array_type.size().type()));
4080 out << ")";
4081 out << " #b1)";
4082 }
4083 else
4084 {
4085 out << "(select ";
4086 convert_expr(expr.array());
4087 out << " ";
4088 convert_expr(typecast_exprt(expr.index(), array_type.size().type()));
4089 out << ")";
4090 }
4091 }
4092 else
4093 {
4094 // fixed size
4095 std::size_t array_width=boolbv_width(array_type);
4096 CHECK_RETURN(array_width != 0);
4097
4098 unflatten(wheret::BEGIN, array_type.element_type());
4099
4100 std::size_t sub_width = boolbv_width(array_type.element_type());
4101 std::size_t index_width=boolbv_width(expr.index().type());
4102
4103 out << "((_ extract " << sub_width-1 << " 0) ";
4104 out << "(bvlshr ";
4105 convert_expr(expr.array());
4106 out << " ";
4107 out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
4108
4109 // SMT2 says that the shift distance must be the same as
4110 // the width of what we shift.
4111 if(array_width>index_width)
4112 {
4113 out << "((_ zero_extend " << array_width-index_width << ") ";
4114 convert_expr(expr.index());
4115 out << ")"; // zero_extend
4116 }
4117 else
4118 {
4119 out << "((_ extract " << array_width-1 << " 0) ";
4120 convert_expr(expr.index());
4121 out << ")"; // extract
4122 }
4123
4124 out << ")))"; // mult, bvlshr, extract
4125
4126 unflatten(wheret::END, array_type.element_type());
4127 }
4128 }
4129 else if(array_op_type.id()==ID_vector)
4130 {
4131 const vector_typet &vector_type=to_vector_type(array_op_type);
4132
4133 if(use_datatypes)
4134 {
4135 const std::string &smt_typename = datatype_map.at(vector_type);
4136
4137 // this is easy for constant indicies
4138
4139 const auto index_int = numeric_cast<mp_integer>(expr.index());
4140 if(!index_int.has_value())
4141 {
4142 SMT2_TODO("non-constant index on vectors");
4143 }
4144 else
4145 {
4146 out << "(" << smt_typename << "." << *index_int << " ";
4147 convert_expr(expr.array());
4148 out << ")";
4149 }
4150 }
4151 else
4152 {
4153 SMT2_TODO("index on vectors");
4154 }
4155 }
4156 else
4157 INVARIANT(
4158 false, "index with unsupported array type: " + array_op_type.id_string());
4159}
4160
4162{
4163 const member_exprt &member_expr=to_member_expr(expr);
4164 const exprt &struct_op=member_expr.struct_op();
4165 const typet &struct_op_type = struct_op.type();
4166 const irep_idt &name=member_expr.get_component_name();
4167
4168 if(struct_op_type.id() == ID_struct || struct_op_type.id() == ID_struct_tag)
4169 {
4170 const struct_typet &struct_type = to_struct_type(ns.follow(struct_op_type));
4171
4172 INVARIANT(
4173 struct_type.has_component(name), "struct should have accessed component");
4174
4175 if(use_datatypes)
4176 {
4177 const std::string &smt_typename = datatype_map.at(struct_type);
4178
4179 out << "(" << smt_typename << "."
4180 << struct_type.get_component(name).get_name()
4181 << " ";
4182 convert_expr(struct_op);
4183 out << ")";
4184 }
4185 else
4186 {
4187 // we extract
4188 const std::size_t member_width = boolbv_width(expr.type());
4189 const auto member_offset = member_offset_bits(struct_type, name, ns);
4190
4192 member_offset.has_value(), "failed to get struct member offset");
4193
4194 out << "((_ extract " << (member_offset.value() + member_width - 1) << " "
4195 << member_offset.value() << ") ";
4196 convert_expr(struct_op);
4197 out << ")";
4198 }
4199 }
4200 else if(
4201 struct_op_type.id() == ID_union || struct_op_type.id() == ID_union_tag)
4202 {
4203 std::size_t width=boolbv_width(expr.type());
4205 width != 0, "failed to get union member width");
4206
4207 unflatten(wheret::BEGIN, expr.type());
4208
4209 out << "((_ extract "
4210 << (width-1)
4211 << " 0) ";
4212 convert_expr(struct_op);
4213 out << ")";
4214
4215 unflatten(wheret::END, expr.type());
4216 }
4217 else
4219 "convert_member on an unexpected type "+struct_op_type.id_string());
4220}
4221
4223{
4224 const typet &type = expr.type();
4225
4226 if(type.id()==ID_bool)
4227 {
4228 out << "(ite ";
4229 convert_expr(expr); // this returns a Bool
4230 out << " #b1 #b0)"; // this is a one-bit bit-vector
4231 }
4232 else if(type.id()==ID_vector)
4233 {
4234 if(use_datatypes)
4235 {
4236 const std::string &smt_typename = datatype_map.at(type);
4237
4238 // concatenate elements
4239 const vector_typet &vector_type=to_vector_type(type);
4240
4241 mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
4242
4243 out << "(let ((?vflop ";
4244 convert_expr(expr);
4245 out << ")) ";
4246
4247 out << "(concat";
4248
4249 for(mp_integer i=0; i!=size; ++i)
4250 {
4251 out << " (" << smt_typename << "." << i << " ?vflop)";
4252 }
4253
4254 out << "))"; // concat, let
4255 }
4256 else
4257 convert_expr(expr); // already a bv
4258 }
4259 else if(type.id()==ID_array)
4260 {
4261 convert_expr(expr);
4262 }
4263 else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4264 {
4265 if(use_datatypes)
4266 {
4267 const std::string &smt_typename = datatype_map.at(type);
4268
4269 // concatenate elements
4270 const struct_typet &struct_type = to_struct_type(ns.follow(type));
4271
4272 out << "(let ((?sflop ";
4273 convert_expr(expr);
4274 out << ")) ";
4275
4276 const struct_typet::componentst &components=
4277 struct_type.components();
4278
4279 // SMT-LIB 2 concat is binary only
4280 for(std::size_t i=components.size(); i>1; i--)
4281 {
4282 out << "(concat (" << smt_typename << "."
4283 << components[i-1].get_name() << " ?sflop)";
4284
4285 out << " ";
4286 }
4287
4288 out << "(" << smt_typename << "."
4289 << components[0].get_name() << " ?sflop)";
4290
4291 for(std::size_t i=1; i<components.size(); i++)
4292 out << ")"; // concat
4293
4294 out << ")"; // let
4295 }
4296 else
4297 convert_expr(expr);
4298 }
4299 else if(type.id()==ID_floatbv)
4300 {
4301 INVARIANT(
4303 "floatbv expressions should be flattened when using FPA theory");
4304
4305 convert_expr(expr);
4306 }
4307 else
4308 convert_expr(expr);
4309}
4310
4312 wheret where,
4313 const typet &type,
4314 unsigned nesting)
4315{
4316 if(type.id()==ID_bool)
4317 {
4318 if(where==wheret::BEGIN)
4319 out << "(= "; // produces a bool
4320 else
4321 out << " #b1)";
4322 }
4323 else if(type.id()==ID_vector)
4324 {
4325 if(use_datatypes)
4326 {
4327 const std::string &smt_typename = datatype_map.at(type);
4328
4329 // extract elements
4330 const vector_typet &vector_type=to_vector_type(type);
4331
4332 std::size_t subtype_width = boolbv_width(vector_type.element_type());
4333
4334 mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
4335
4336 if(where==wheret::BEGIN)
4337 out << "(let ((?ufop" << nesting << " ";
4338 else
4339 {
4340 out << ")) ";
4341
4342 out << "(mk-" << smt_typename;
4343
4344 std::size_t offset=0;
4345
4346 for(mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4347 {
4348 out << " ";
4349 unflatten(wheret::BEGIN, vector_type.element_type(), nesting + 1);
4350 out << "((_ extract " << offset+subtype_width-1 << " "
4351 << offset << ") ?ufop" << nesting << ")";
4352 unflatten(wheret::END, vector_type.element_type(), nesting + 1);
4353 }
4354
4355 out << "))"; // mk-, let
4356 }
4357 }
4358 else
4359 {
4360 // nop, already a bv
4361 }
4362 }
4363 else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4364 {
4365 if(use_datatypes)
4366 {
4367 // extract members
4368 if(where==wheret::BEGIN)
4369 out << "(let ((?ufop" << nesting << " ";
4370 else
4371 {
4372 out << ")) ";
4373
4374 const std::string &smt_typename = datatype_map.at(type);
4375
4376 out << "(mk-" << smt_typename;
4377
4378 const struct_typet &struct_type = to_struct_type(ns.follow(type));
4379
4380 const struct_typet::componentst &components=
4381 struct_type.components();
4382
4383 std::size_t offset=0;
4384
4385 std::size_t i=0;
4386 for(struct_typet::componentst::const_iterator
4387 it=components.begin();
4388 it!=components.end();
4389 it++, i++)
4390 {
4391 std::size_t member_width=boolbv_width(it->type());
4392
4393 out << " ";
4394 unflatten(wheret::BEGIN, it->type(), nesting+1);
4395 out << "((_ extract " << offset+member_width-1 << " "
4396 << offset << ") ?ufop" << nesting << ")";
4397 unflatten(wheret::END, it->type(), nesting+1);
4398 offset+=member_width;
4399 }
4400
4401 out << "))"; // mk-, let
4402 }
4403 }
4404 else
4405 {
4406 // nop, already a bv
4407 }
4408 }
4409 else
4410 {
4411 // nop
4412 }
4413}
4414
4415void smt2_convt::set_to(const exprt &expr, bool value)
4416{
4417 PRECONDITION(expr.type().id() == ID_bool);
4418
4419 if(expr.id()==ID_and && value)
4420 {
4421 forall_operands(it, expr)
4422 set_to(*it, true);
4423 return;
4424 }
4425
4426 if(expr.id()==ID_or && !value)
4427 {
4428 forall_operands(it, expr)
4429 set_to(*it, false);
4430 return;
4431 }
4432
4433 if(expr.id()==ID_not)
4434 {
4435 return set_to(to_not_expr(expr).op(), !value);
4436 }
4437
4438 out << "\n";
4439
4440 // special treatment for "set_to(a=b, true)" where
4441 // a is a new symbol
4442
4443 if(expr.id() == ID_equal && value)
4444 {
4445 const equal_exprt &equal_expr=to_equal_expr(expr);
4446 if(
4447 equal_expr.lhs().type().id() == ID_empty ||
4448 equal_expr.rhs().id() == ID_empty_union)
4449 {
4450 // ignore equality checking over expressions with empty (void) type
4451 return;
4452 }
4453
4454 if(equal_expr.lhs().id()==ID_symbol)
4455 {
4456 const irep_idt &identifier=
4457 to_symbol_expr(equal_expr.lhs()).get_identifier();
4458
4459 if(identifier_map.find(identifier)==identifier_map.end())
4460 {
4461 identifiert &id=identifier_map[identifier];
4462 CHECK_RETURN(id.type.is_nil());
4463
4464 id.type=equal_expr.lhs().type();
4465 find_symbols(id.type);
4466 exprt prepared_rhs = prepare_for_convert_expr(equal_expr.rhs());
4467
4468 std::string smt2_identifier=convert_identifier(identifier);
4469 smt2_identifiers.insert(smt2_identifier);
4470
4471 out << "; set_to true (equal)\n";
4472 out << "(define-fun |" << smt2_identifier << "| () ";
4473
4474 convert_type(equal_expr.lhs().type());
4475 out << " ";
4476 convert_expr(prepared_rhs);
4477
4478 out << ")" << "\n";
4479 return; // done
4480 }
4481 }
4482 }
4483
4484 exprt prepared_expr = prepare_for_convert_expr(expr);
4485
4486#if 0
4487 out << "; CONV: "
4488 << format(expr) << "\n";
4489#endif
4490
4491 out << "; set_to " << (value?"true":"false") << "\n"
4492 << "(assert ";
4493 if(!value)
4494 {
4495 out << "(not ";
4496 }
4497 const auto found_literal = defined_expressions.find(expr);
4498 if(!(found_literal == defined_expressions.end()))
4499 {
4500 // This is a converted expression, we can just assert the literal name
4501 // since the expression is already defined
4502 out << found_literal->second;
4503 set_values[found_literal->second] = value;
4504 }
4505 else
4506 {
4507 convert_expr(prepared_expr);
4508 }
4509 if(!value)
4510 {
4511 out << ")";
4512 }
4513 out << ")\n";
4514 return;
4515}
4516
4524{
4525 exprt lowered_expr = expr;
4526
4527 for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
4528 it != itend;
4529 ++it)
4530 {
4531 if(
4532 it->id() == ID_byte_extract_little_endian ||
4533 it->id() == ID_byte_extract_big_endian)
4534 {
4535 it.mutate() = lower_byte_extract(to_byte_extract_expr(*it), ns);
4536 }
4537 else if(
4538 it->id() == ID_byte_update_little_endian ||
4539 it->id() == ID_byte_update_big_endian)
4540 {
4541 it.mutate() = lower_byte_update(to_byte_update_expr(*it), ns);
4542 }
4543 }
4544
4545 return lowered_expr;
4546}
4547
4556{
4557 // First, replace byte operators, because they may introduce new array
4558 // expressions that must be seen by find_symbols:
4559 exprt lowered_expr = lower_byte_operators(expr);
4560 INVARIANT(
4561 !has_byte_operator(lowered_expr),
4562 "lower_byte_operators should remove all byte operators");
4563
4564 // Now create symbols for all composite expressions present in lowered_expr:
4565 find_symbols(lowered_expr);
4566
4567 return lowered_expr;
4568}
4569
4571{
4572 // recursive call on type
4573 find_symbols(expr.type());
4574
4575 if(expr.id() == ID_exists || expr.id() == ID_forall)
4576 {
4577 // do not declare the quantified symbol, but record
4578 // as 'bound symbol'
4579 const auto &q_expr = to_quantifier_expr(expr);
4580 for(const auto &symbol : q_expr.variables())
4581 {
4582 const auto identifier = symbol.get_identifier();
4583 identifiert &id = identifier_map[identifier];
4584 id.type = symbol.type();
4585 id.is_bound = true;
4586 }
4587 find_symbols(q_expr.where());
4588 return;
4589 }
4590
4591 // recursive call on operands
4592 forall_operands(it, expr)
4593 find_symbols(*it);
4594
4595 if(expr.id()==ID_symbol ||
4596 expr.id()==ID_nondet_symbol)
4597 {
4598 // we don't track function-typed symbols
4599 if(expr.type().id()==ID_code)
4600 return;
4601
4602 irep_idt identifier;
4603
4604 if(expr.id()==ID_symbol)
4605 identifier=to_symbol_expr(expr).get_identifier();
4606 else
4607 identifier="nondet_"+
4609
4610 identifiert &id=identifier_map[identifier];
4611
4612 if(id.type.is_nil())
4613 {
4614 id.type=expr.type();
4615
4616 std::string smt2_identifier=convert_identifier(identifier);
4617 smt2_identifiers.insert(smt2_identifier);
4618
4619 out << "; find_symbols\n";
4620 out << "(declare-fun |"
4621 << smt2_identifier
4622 << "| () ";
4623 convert_type(expr.type());
4624 out << ")" << "\n";
4625 }
4626 }
4627 else if(expr.id() == ID_array_of)
4628 {
4629 if(!use_as_const)
4630 {
4631 if(defined_expressions.find(expr) == defined_expressions.end())
4632 {
4633 const auto &array_of = to_array_of_expr(expr);
4634 const auto &array_type = array_of.type();
4635
4636 const irep_idt id =
4637 "array_of." + std::to_string(defined_expressions.size());
4638 out << "; the following is a substitute for lambda i. x\n";
4639 out << "(declare-fun " << id << " () ";
4640 convert_type(array_type);
4641 out << ")\n";
4642
4643 // use a quantifier-based initialization instead of lambda
4644 out << "(assert (forall ((i ";
4645 convert_type(array_type.size().type());
4646 out << ")) (= (select " << id << " i) ";
4647 if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
4648 {
4649 out << "(ite ";
4650 convert_expr(array_of.what());
4651 out << " #b1 #b0)";
4652 }
4653 else
4654 {
4655 convert_expr(array_of.what());
4656 }
4657 out << ")))\n";
4658
4659 defined_expressions[expr] = id;
4660 }
4661 }
4662 }
4663 else if(expr.id() == ID_array_comprehension)
4664 {
4666 {
4667 if(defined_expressions.find(expr) == defined_expressions.end())
4668 {
4669 const auto &array_comprehension = to_array_comprehension_expr(expr);
4670 const auto &array_type = array_comprehension.type();
4671 const auto &array_size = array_type.size();
4672
4673 const irep_idt id =
4674 "array_comprehension." + std::to_string(defined_expressions.size());
4675 out << "(declare-fun " << id << " () ";
4676 convert_type(array_type);
4677 out << ")\n";
4678
4679 out << "; the following is a substitute for lambda i . x(i)\n";
4680 out << "; universally quantified initialization of the array\n";
4681 out << "(assert (forall ((";
4682 convert_expr(array_comprehension.arg());
4683 out << " ";
4684 convert_type(array_size.type());
4685 out << ")) (=> (and (bvule (_ bv0 " << boolbv_width(array_size.type())
4686 << ") ";
4687 convert_expr(array_comprehension.arg());
4688 out << ") (bvult ";
4689 convert_expr(array_comprehension.arg());
4690 out << " ";
4691 convert_expr(array_size);
4692 out << ")) (= (select " << id << " ";
4693 convert_expr(array_comprehension.arg());
4694 out << ") ";
4695 if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
4696 {
4697 out << "(ite ";
4698 convert_expr(array_comprehension.body());
4699 out << " #b1 #b0)";
4700 }
4701 else
4702 {
4703 convert_expr(array_comprehension.body());
4704 }
4705 out << "))))\n";
4706
4707 defined_expressions[expr] = id;
4708 }
4709 }
4710 }
4711 else if(expr.id()==ID_array)
4712 {
4713 if(defined_expressions.find(expr)==defined_expressions.end())
4714 {
4715 const array_typet &array_type=to_array_type(expr.type());
4716
4717 const irep_idt id = "array." + std::to_string(defined_expressions.size());
4718 out << "; the following is a substitute for an array constructor" << "\n";
4719 out << "(declare-fun " << id << " () ";
4720 convert_type(array_type);
4721 out << ")" << "\n";
4722
4723 for(std::size_t i=0; i<expr.operands().size(); i++)
4724 {
4725 out << "(assert (= (select " << id << " ";
4726 convert_expr(from_integer(i, array_type.size().type()));
4727 out << ") "; // select
4728 if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
4729 {
4730 out << "(ite ";
4731 convert_expr(expr.operands()[i]);
4732 out << " #b1 #b0)";
4733 }
4734 else
4735 {
4736 convert_expr(expr.operands()[i]);
4737 }
4738 out << "))" << "\n"; // =, assert
4739 }
4740
4741 defined_expressions[expr]=id;
4742 }
4743 }
4744 else if(expr.id()==ID_string_constant)
4745 {
4746 if(defined_expressions.find(expr)==defined_expressions.end())
4747 {
4748 // introduce a temporary array.
4750 const array_typet &array_type=to_array_type(tmp.type());
4751
4752 const irep_idt id =
4753 "string." + std::to_string(defined_expressions.size());
4754 out << "; the following is a substitute for a string" << "\n";
4755 out << "(declare-fun " << id << " () ";
4756 convert_type(array_type);
4757 out << ")" << "\n";
4758
4759 for(std::size_t i=0; i<tmp.operands().size(); i++)
4760 {
4761 out << "(assert (= (select " << id;
4762 convert_expr(from_integer(i, array_type.size().type()));
4763 out << ") "; // select
4764 convert_expr(tmp.operands()[i]);
4765 out << "))" << "\n";
4766 }
4767
4768 defined_expressions[expr]=id;
4769 }
4770 }
4771 else if(expr.id() == ID_object_size)
4772 {
4773 const exprt &op = to_unary_expr(expr).op();
4774
4775 if(op.type().id()==ID_pointer)
4776 {
4777 if(object_sizes.find(expr)==object_sizes.end())
4778 {
4779 const irep_idt id =
4780 "object_size." + std::to_string(object_sizes.size());
4781 out << "(declare-fun |" << id << "| () ";
4782 convert_type(expr.type());
4783 out << ")" << "\n";
4784
4785 object_sizes[expr]=id;
4786 }
4787 }
4788 }
4789 // clang-format off
4790 else if(!use_FPA_theory &&
4791 expr.operands().size() >= 1 &&
4792 (expr.id() == ID_floatbv_plus ||
4793 expr.id() == ID_floatbv_minus ||
4794 expr.id() == ID_floatbv_mult ||
4795 expr.id() == ID_floatbv_div ||
4796 expr.id() == ID_floatbv_typecast ||
4797 expr.id() == ID_ieee_float_equal ||
4798 expr.id() == ID_ieee_float_notequal ||
4799 ((expr.id() == ID_lt ||
4800 expr.id() == ID_gt ||
4801 expr.id() == ID_le ||
4802 expr.id() == ID_ge ||
4803 expr.id() == ID_isnan ||
4804 expr.id() == ID_isnormal ||
4805 expr.id() == ID_isfinite ||
4806 expr.id() == ID_isinf ||
4807 expr.id() == ID_sign ||
4808 expr.id() == ID_unary_minus ||
4809 expr.id() == ID_typecast ||
4810 expr.id() == ID_abs) &&
4811 to_multi_ary_expr(expr).op0().type().id() == ID_floatbv)))
4812 // clang-format on
4813 {
4814 irep_idt function=
4815 "|float_bv."+expr.id_string()+floatbv_suffix(expr)+"|";
4816
4817 if(bvfp_set.insert(function).second)
4818 {
4819 out << "; this is a model for " << expr.id() << " : "
4820 << type2id(to_multi_ary_expr(expr).op0().type()) << " -> "
4821 << type2id(expr.type()) << "\n"
4822 << "(define-fun " << function << " (";
4823
4824 for(std::size_t i = 0; i < expr.operands().size(); i++)
4825 {
4826 if(i!=0)
4827 out << " ";
4828 out << "(op" << i << ' ';
4829 convert_type(expr.operands()[i].type());
4830 out << ')';
4831 }
4832
4833 out << ") ";
4834 convert_type(expr.type()); // return type
4835 out << ' ';
4836
4837 exprt tmp1=expr;
4838 for(std::size_t i = 0; i < tmp1.operands().size(); i++)
4839 tmp1.operands()[i]=
4840 smt2_symbolt("op"+std::to_string(i), tmp1.operands()[i].type());
4841
4842 exprt tmp2=float_bv(tmp1);
4843 tmp2=letify(tmp2);
4844 CHECK_RETURN(!tmp2.is_nil());
4845
4846 convert_expr(tmp2);
4847
4848 out << ")\n"; // define-fun
4849 }
4850 }
4851}
4852
4854{
4855 const typet &type = expr.type();
4856 PRECONDITION(type.id()==ID_array);
4857
4858 if(use_datatypes)
4859 {
4860 return true; // always use array theory when we have datatypes
4861 }
4862 else
4863 {
4864 // arrays inside structs get flattened
4865 if(expr.id()==ID_with)
4866 return use_array_theory(to_with_expr(expr).old());
4867 else if(expr.id()==ID_member)
4868 return false;
4869 else
4870 return true;
4871 }
4872}
4873
4875{
4876 if(type.id()==ID_array)
4877 {
4878 const array_typet &array_type=to_array_type(type);
4879 CHECK_RETURN(array_type.size().is_not_nil());
4880
4881 // we always use array theory for top-level arrays
4882 const typet &subtype = array_type.element_type();
4883
4884 out << "(Array ";
4885 convert_type(array_type.size().type());
4886 out << " ";
4887
4888 if(subtype.id()==ID_bool && !use_array_of_bool)
4889 out << "(_ BitVec 1)";
4890 else
4891 convert_type(array_type.element_type());
4892
4893 out << ")";
4894 }
4895 else if(type.id()==ID_bool)
4896 {
4897 out << "Bool";
4898 }
4899 else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4900 {
4901 if(use_datatypes)
4902 {
4903 out << datatype_map.at(type);
4904 }
4905 else
4906 {
4907 std::size_t width=boolbv_width(type);
4909 width != 0, "failed to get width of struct");
4910
4911 out << "(_ BitVec " << width << ")";
4912 }
4913 }
4914 else if(type.id()==ID_vector)
4915 {
4916 if(use_datatypes)
4917 {
4918 out << datatype_map.at(type);
4919 }
4920 else
4921 {
4922 std::size_t width=boolbv_width(type);
4924 width != 0, "failed to get width of vector");
4925
4926 out << "(_ BitVec " << width << ")";
4927 }
4928 }
4929 else if(type.id()==ID_code)
4930 {
4931 // These may appear in structs.
4932 // We replace this by "Bool" in order to keep the same
4933 // member count.
4934 out << "Bool";
4935 }
4936 else if(type.id() == ID_union || type.id() == ID_union_tag)
4937 {
4938 std::size_t width=boolbv_width(type);
4940 to_union_type(ns.follow(type)).components().empty() || width != 0,
4941 "failed to get width of union");
4942
4943 out << "(_ BitVec " << width << ")";
4944 }
4945 else if(type.id()==ID_pointer)
4946 {
4947 out << "(_ BitVec "
4948 << boolbv_width(type) << ")";
4949 }
4950 else if(type.id()==ID_bv ||
4951 type.id()==ID_fixedbv ||
4952 type.id()==ID_unsignedbv ||
4953 type.id()==ID_signedbv ||
4954 type.id()==ID_c_bool)
4955 {
4956 out << "(_ BitVec "
4957 << to_bitvector_type(type).get_width() << ")";
4958 }
4959 else if(type.id()==ID_c_enum)
4960 {
4961 // these have an underlying type
4962 out << "(_ BitVec "
4963 << to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width()
4964 << ")";
4965 }
4966 else if(type.id()==ID_c_enum_tag)
4967 {
4969 }
4970 else if(type.id()==ID_floatbv)
4971 {
4972 const floatbv_typet &floatbv_type=to_floatbv_type(type);
4973
4974 if(use_FPA_theory)
4975 out << "(_ FloatingPoint "
4976 << floatbv_type.get_e() << " "
4977 << floatbv_type.get_f() + 1 << ")";
4978 else
4979 out << "(_ BitVec "
4980 << floatbv_type.get_width() << ")";
4981 }
4982 else if(type.id()==ID_rational ||
4983 type.id()==ID_real)
4984 out << "Real";
4985 else if(type.id()==ID_integer)
4986 out << "Int";
4987 else if(type.id()==ID_complex)
4988 {
4989 if(use_datatypes)
4990 {
4991 out << datatype_map.at(type);
4992 }
4993 else
4994 {
4995 std::size_t width=boolbv_width(type);
4997 width != 0, "failed to get width of complex");
4998
4999 out << "(_ BitVec " << width << ")";
5000 }
5001 }
5002 else if(type.id()==ID_c_bit_field)
5003 {
5005 }
5006 else
5007 {
5008 UNEXPECTEDCASE("unsupported type: "+type.id_string());
5009 }
5010}
5011
5013{
5014 std::set<irep_idt> recstack;
5015 find_symbols_rec(type, recstack);
5016}
5017
5019 const typet &type,
5020 std::set<irep_idt> &recstack)
5021{
5022 if(type.id()==ID_array)
5023 {
5024 const array_typet &array_type=to_array_type(type);
5025 find_symbols(array_type.size());
5026 find_symbols_rec(array_type.element_type(), recstack);
5027 }
5028 else if(type.id()==ID_complex)
5029 {
5030 find_symbols_rec(to_complex_type(type).subtype(), recstack);
5031
5032 if(use_datatypes &&
5033 datatype_map.find(type)==datatype_map.end())
5034 {
5035 const std::string smt_typename =
5036 "complex." + std::to_string(datatype_map.size());
5037 datatype_map[type] = smt_typename;
5038
5039 out << "(declare-datatypes () ((" << smt_typename << " "
5040 << "(mk-" << smt_typename;
5041
5042 out << " (" << smt_typename << ".imag ";
5043 convert_type(to_complex_type(type).subtype());
5044 out << ")";
5045
5046 out << " (" << smt_typename << ".real ";
5047 convert_type(to_complex_type(type).subtype());
5048 out << ")";
5049
5050 out << "))))\n";
5051 }
5052 }
5053 else if(type.id()==ID_vector)
5054 {
5055 find_symbols_rec(to_vector_type(type).element_type(), recstack);
5056
5057 if(use_datatypes &&
5058 datatype_map.find(type)==datatype_map.end())
5059 {
5060 const vector_typet &vector_type=to_vector_type(type);
5061
5062 mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
5063
5064 const std::string smt_typename =
5065 "vector." + std::to_string(datatype_map.size());
5066 datatype_map[type] = smt_typename;
5067
5068 out << "(declare-datatypes () ((" << smt_typename << " "
5069 << "(mk-" << smt_typename;
5070
5071 for(mp_integer i=0; i!=size; ++i)
5072 {
5073 out << " (" << smt_typename << "." << i << " ";
5074 convert_type(to_vector_type(type).element_type());
5075 out << ")";
5076 }
5077
5078 out << "))))\n";
5079 }
5080 }
5081 else if(type.id() == ID_struct)
5082 {
5083 // Cater for mutually recursive struct types
5084 bool need_decl=false;
5085 if(use_datatypes &&
5086 datatype_map.find(type)==datatype_map.end())
5087 {
5088 const std::string smt_typename =
5089 "struct." + std::to_string(datatype_map.size());
5090 datatype_map[type] = smt_typename;
5091 need_decl=true;
5092 }
5093
5094 const struct_typet::componentst &components =
5095 to_struct_type(type).components();
5096
5097 for(const auto &component : components)
5098 find_symbols_rec(component.type(), recstack);
5099
5100 // Declare the corresponding SMT type if we haven't already.
5101 if(need_decl)
5102 {
5103 const std::string &smt_typename = datatype_map.at(type);
5104
5105 // We're going to create a datatype named something like `struct.0'.
5106 // It's going to have a single constructor named `mk-struct.0' with an
5107 // argument for each member of the struct. The declaration that
5108 // creates this type looks like:
5109 //
5110 // (declare-datatypes () ((struct.0 (mk-struct.0
5111 // (struct.0.component1 type1)
5112 // ...
5113 // (struct.0.componentN typeN)))))
5114 out << "(declare-datatypes () ((" << smt_typename << " "
5115 << "(mk-" << smt_typename << " ";
5116
5117 for(const auto &component : components)
5118 {
5119 out << "(" << smt_typename << "." << component.get_name()
5120 << " ";
5121 convert_type(component.type());
5122 out << ") ";
5123 }
5124
5125 out << "))))" << "\n";
5126
5127 // Let's also declare convenience functions to update individual
5128 // members of the struct whil we're at it. The functions are
5129 // named like `update-struct.0.component1'. Their declarations
5130 // look like:
5131 //
5132 // (declare-fun update-struct.0.component1
5133 // ((s struct.0) ; first arg -- the struct to update
5134 // (v type1)) ; second arg -- the value to update
5135 // struct.0 ; the output type
5136 // (mk-struct.0 ; build the new struct...
5137 // v ; the updated value
5138 // (struct.0.component2 s) ; retain the other members
5139 // ...
5140 // (struct.0.componentN s)))
5141
5142 for(struct_union_typet::componentst::const_iterator
5143 it=components.begin();
5144 it!=components.end();
5145 ++it)
5146 {
5148 out << "(define-fun update-" << smt_typename << "."
5149 << component.get_name() << " "
5150 << "((s " << smt_typename << ") "
5151 << "(v ";
5152 convert_type(component.type());
5153 out << ")) " << smt_typename << " "
5154 << "(mk-" << smt_typename
5155 << " ";
5156
5157 for(struct_union_typet::componentst::const_iterator
5158 it2=components.begin();
5159 it2!=components.end();
5160 ++it2)
5161 {
5162 if(it==it2)
5163 out << "v ";
5164 else
5165 {
5166 out << "(" << smt_typename << "."
5167 << it2->get_name() << " s) ";
5168 }
5169 }
5170
5171 out << "))" << "\n";
5172 }
5173
5174 out << "\n";
5175 }
5176 }
5177 else if(type.id() == ID_union)
5178 {
5179 const union_typet::componentst &components =
5180 to_union_type(type).components();
5181
5182 for(const auto &component : components)
5183 find_symbols_rec(component.type(), recstack);
5184 }
5185 else if(type.id()==ID_code)
5186 {
5187 const code_typet::parameterst &parameters=
5188 to_code_type(type).parameters();
5189 for(const auto &param : parameters)
5190 find_symbols_rec(param.type(), recstack);
5191
5192 find_symbols_rec(to_code_type(type).return_type(), recstack);
5193 }
5194 else if(type.id()==ID_pointer)
5195 {
5196 find_symbols_rec(to_pointer_type(type).base_type(), recstack);
5197 }
5198 else if(type.id() == ID_struct_tag)
5199 {
5200 const auto &struct_tag = to_struct_tag_type(type);
5201 const irep_idt &id = struct_tag.get_identifier();
5202
5203 if(recstack.find(id) == recstack.end())
5204 {
5205 const auto &base_struct = ns.follow_tag(struct_tag);
5206 recstack.insert(id);
5207 find_symbols_rec(base_struct, recstack);
5208 datatype_map[type] = datatype_map[base_struct];
5209 }
5210 }
5211 else if(type.id() == ID_union_tag)
5212 {
5213 const auto &union_tag = to_union_tag_type(type);
5214 const irep_idt &id = union_tag.get_identifier();
5215
5216 if(recstack.find(id) == recstack.end())
5217 {
5218 recstack.insert(id);
5219 find_symbols_rec(ns.follow_tag(union_tag), recstack);
5220 }
5221 }
5222}
5223
5225{
5227}
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
API to expression classes for bitvectors.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
int16_t s2
Definition: bytecode_info.h:60
int8_t s1
Definition: bytecode_info.h:59
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
bitvector_typet index_type()
Definition: c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:344
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:106
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
Absolute value.
Definition: std_expr.h:346
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
Array constructor from list of elements.
Definition: std_expr.h:1476
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
A base class for binary expressions.
Definition: std_expr.h:550
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
exprt & where()
Definition: std_expr.h:2931
variablest & variables()
Definition: std_expr.h:2921
Bit-wise negation of bit-vectors.
std::size_t get_width() const
Definition: std_types.h:864
The Boolean type.
Definition: std_types.h:36
const membert & get_member(const struct_typet &type, const irep_idt &member) const
The byte swap expression.
std::size_t get_bits_per_byte() const
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
struct configt::bv_encodingt bv_encoding
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
void set_value(const irep_idt &value)
Definition: std_expr.h:2820
resultt
Result of running the decision procedure.
Division.
Definition: std_expr.h:1064
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
size_t size() const
Definition: dstring.h:104
Equality.
Definition: std_expr.h:1225
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition: std_expr.h:1179
exprt & op0()
Definition: expr.h:99
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
depth_iteratort depth_end()
Definition: expr.cpp:267
depth_iteratort depth_begin()
Definition: expr.cpp:265
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition: std_expr.h:2865
std::size_t integer_bits
Definition: fixedbv.h:22
std::size_t width
Definition: fixedbv.h:22
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
Fixed-width bit-vector with signed fixed-point interpretation.
std::size_t get_fraction_bits() const
std::size_t get_integer_bits() const
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
Fixed-width bit-vector with IEEE floating-point interpretation.
std::size_t get_f() const
std::size_t get_e() const
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
exprt & rounding_mode()
Definition: floatbv_expr.h:395
std::size_t f
Definition: ieee_float.h:27
std::size_t width() const
Definition: ieee_float.h:51
ieee_float_spect spec
Definition: ieee_float.h:135
bool is_NaN() const
Definition: ieee_float.h:249
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
bool get_sign() const
Definition: ieee_float.h:248
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:212
static ieee_floatt NaN(const ieee_float_spect &_spec)
Definition: ieee_float.h:209
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:215
bool is_infinity() const
Definition: ieee_float.h:250
mp_integer pack() const
Definition: ieee_float.cpp:374
void build(const mp_integer &exp, const mp_integer &frac)
Definition: ieee_float.cpp:472
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
Boolean implication.
Definition: std_expr.h:2037
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
bool is_not_nil() const
Definition: irep.h:380
const std::string & id_string() const
Definition: irep.h:399
subt & get_sub()
Definition: irep.h:456
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
Evaluates to true if the operand is finite.
Definition: floatbv_expr.h:176
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
Evaluates to true if the operand is NaN.
Definition: floatbv_expr.h:88
Evaluates to true if the operand is a normal number.
Definition: floatbv_expr.h:220
A let expression.
Definition: std_expr.h:2973
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:3054
operandst & values()
Definition: std_expr.h:3043
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3066
literalt get_literal() const
Definition: literal_expr.h:26
bool is_true() const
Definition: literal.h:156
bool sign() const
Definition: literal.h:88
var_not var_no() const
Definition: literal.h:83
bool is_false() const
Definition: literal.h:161
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
irep_idt get_component_name() const
Definition: std_expr.h:2681
Binary minus.
Definition: std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
exprt & op1()
Definition: std_expr.h:850
exprt & op0()
Definition: std_expr.h:844
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
const irep_idt & get_identifier() const
Definition: std_expr.h:237
Boolean negation.
Definition: std_expr.h:2181
Disequality.
Definition: std_expr.h:1283
The plus expression Associativity is not specified.
Definition: std_expr.h:914
void get_dynamic_objects(std::vector< std::size_t > &objects) const
std::size_t get_invalid_object() const
Definition: pointer_logic.h:64
numberingt< exprt, irep_hash > objects
Definition: pointer_logic.h:26
std::size_t add_object(const exprt &expr)
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A base class for quantifier expressions.
Bit-vector replication.
constant_exprt & times()
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:506
const irep_idt & get_identifier() const
Definition: smt2_conv.h:194
void convert_relation(const binary_relation_exprt &)
Definition: smt2_conv.cpp:3169
bool use_lambda_for_array
Definition: smt2_conv.h:65
void convert_type(const typet &)
Definition: smt2_conv.cpp:4874
void unflatten(wheret, const typet &, unsigned nesting=0)
Definition: smt2_conv.cpp:4311
bool use_array_theory(const exprt &)
Definition: smt2_conv.cpp:4853
void find_symbols(const exprt &expr)
Definition: smt2_conv.cpp:4570
std::size_t number_of_solver_calls
Definition: smt2_conv.h:96
void convert_typecast(const typecast_exprt &expr)
Definition: smt2_conv.cpp:2148
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
Definition: smt2_conv.cpp:183
tvt l_get(literalt l) const
Definition: smt2_conv.cpp:140
void convert_floatbv_rem(const binary_exprt &expr)
Definition: smt2_conv.cpp:3786
void convert_update(const exprt &expr)
Definition: smt2_conv.cpp:4056
bool use_FPA_theory
Definition: smt2_conv.h:60
std::set< irep_idt > bvfp_set
Definition: smt2_conv.h:185
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
Definition: smt2_conv.cpp:700
void push() override
Unimplemented.
Definition: smt2_conv.cpp:861
void convert_is_dynamic_object(const unary_exprt &)
Definition: smt2_conv.cpp:3132
void convert_literal(const literalt)
Definition: smt2_conv.cpp:841
void convert_floatbv_div(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3671
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
Definition: smt2_conv.cpp:5224
const namespacet & ns
Definition: smt2_conv.h:88
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3766
boolbv_widtht boolbv_width
Definition: smt2_conv.h:94
void convert_constant(const constant_exprt &expr)
Definition: smt2_conv.cpp:2953
std::string floatbv_suffix(const exprt &) const
Definition: smt2_conv.cpp:946
void flatten2bv(const exprt &)
Definition: smt2_conv.cpp:4222
std::string notes
Definition: smt2_conv.h:90
void convert_div(const div_exprt &expr)
Definition: smt2_conv.cpp:3627
std::ostream & out
Definition: smt2_conv.h:89
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
Definition: smt2_conv.cpp:4523
std::string type2id(const typet &) const
Definition: smt2_conv.cpp:909
bool emit_set_logic
Definition: smt2_conv.h:66
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Definition: smt2_conv.cpp:3412
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: smt2_conv.cpp:2681
struct_exprt parse_struct(const irept &s, const struct_typet &type)
Definition: smt2_conv.cpp:577
std::string logic
Definition: smt2_conv.h:90
void convert_mult(const mult_exprt &expr)
Definition: smt2_conv.cpp:3691
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
Definition: smt2_conv.cpp:4555
void define_object_size(const irep_idt &id, const exprt &expr)
Definition: smt2_conv.cpp:234
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: smt2_conv.cpp:279
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_conv.cpp:125
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3607
bool use_check_sat_assuming
Definition: smt2_conv.h:63
bool use_datatypes
Definition: smt2_conv.h:64
datatype_mapt datatype_map
Definition: smt2_conv.h:244
void convert_mod(const mod_exprt &expr)
Definition: smt2_conv.cpp:3113
static std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:878
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3469
void convert_struct(const struct_exprt &expr)
Definition: smt2_conv.cpp:2825
std::unordered_map< irep_idt, bool > set_values
The values which boolean identifiers have been smt2_convt::set_to or in other words those which are a...
Definition: smt2_conv.h:257
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
Definition: smt2_conv.cpp:54
void convert_member(const member_exprt &expr)
Definition: smt2_conv.cpp:4161
void convert_euclidean_mod(const euclidean_mod_exprt &expr)
Definition: smt2_conv.cpp:3098
void convert_index(const index_exprt &expr)
Definition: smt2_conv.cpp:4063
pointer_logict pointer_logic
Definition: smt2_conv.h:215
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
Definition: smt2_conv.cpp:832
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: smt2_conv.cpp:130
void walk_array_tree(std::unordered_map< int64_t, exprt > *operands_map, const irept &src, const array_typet &type)
This function walks the SMT output and populates a map with index/value pairs for the array.
Definition: smt2_conv.cpp:521
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Definition: smt2_conv.cpp:4415
defined_expressionst object_sizes
Definition: smt2_conv.h:259
bool use_as_const
Definition: smt2_conv.h:62
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:636
void convert_union(const union_exprt &expr)
Definition: smt2_conv.cpp:2920
exprt parse_union(const irept &s, const union_typet &type)
Definition: smt2_conv.cpp:561
exprt parse_array(const irept &s, const array_typet &type)
This function is for parsing array output from SMT solvers when "(get-value |???|)" returns an array ...
Definition: smt2_conv.cpp:477
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:266
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
Definition: smt2_conv.cpp:2889
void convert_with(const with_exprt &expr)
Definition: smt2_conv.cpp:3809
letifyt letify
Definition: smt2_conv.h:157
bool use_array_of_bool
Definition: smt2_conv.h:61
std::vector< exprt > assumptions
Definition: smt2_conv.h:93
void convert_plus(const plus_exprt &expr)
Definition: smt2_conv.cpp:3276
defined_expressionst defined_expressions
Definition: smt2_conv.h:253
void pop() override
Currently, only implements a single stack element (no nested contexts)
Definition: smt2_conv.cpp:873
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt2_conv.cpp:5018
void write_header()
Definition: smt2_conv.cpp:153
solvert solver
Definition: smt2_conv.h:91
identifier_mapt identifier_map
Definition: smt2_conv.h:237
void convert_minus(const minus_exprt &expr)
Definition: smt2_conv.cpp:3510
void convert_expr(const exprt &)
Definition: smt2_conv.cpp:987
constant_exprt parse_literal(const irept &, const typet &type)
Definition: smt2_conv.cpp:339
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
Definition: smt2_conv.h:200
std::size_t no_boolean_variables
Definition: smt2_conv.h:265
smt2_identifierst smt2_identifiers
Definition: smt2_conv.h:262
void convert_floatbv(const exprt &expr)
Definition: smt2_conv.cpp:953
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: smt2_conv.cpp:272
literalt convert(const exprt &expr)
Definition: smt2_conv.cpp:792
array_exprt to_array_expr() const
convert string into array constant
Struct constructor from list of elements.
Definition: std_expr.h:1722
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const irep_idt & get_name() const
Definition: std_types.h:79
const componentst & components() const
Definition: std_types.h:147
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:57
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
std::vector< componentt > componentst
Definition: std_types.h:140
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The Boolean constant true.
Definition: std_expr.h:2856
Definition: threeval.h:20
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
The unary minus expression.
Definition: std_expr.h:390
Union constructor from single element.
Definition: std_expr.h:1611
The union type.
Definition: c_types.h:125
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
Definition: std_expr.h:1575
The vector type.
Definition: std_types.h:996
const constant_exprt & size() const
Definition: std_types.cpp:253
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
exprt & new_value()
Definition: std_expr.h:2342
exprt & where()
Definition: std_expr.h:2332
exprt & old()
Definition: std_expr.h:2322
configt config
Definition: config.cpp:25
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define forall_operands(it, expr)
Definition: expr.h:18
Forward depth-first search iterators These iterators' copy operations are expensive,...
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:35
Deprecated expression utility functions.
exprt float_bv(const exprt &src)
Definition: float_bv.h:187
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: floatbv_expr.h:245
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: floatbv_expr.h:157
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: floatbv_expr.h:201
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: floatbv_expr.h:113
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
static format_containert< T > format(const T &o)
Definition: format.h:37
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:206
bool is_true(const literalt &l)
Definition: literal.h:198
literalt const_literal(bool value)
Definition: literal.h:188
literalt pos(literalt a)
Definition: literal.h:194
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
Definition: literal_expr.h:56
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
Definition: mp_arith.cpp:215
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:64
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
exprt simplify_expr(exprt src, const namespacet &ns)
#define SMT2_TODO(S)
Definition: smt2_conv.cpp:52
#define UNEXPECTEDCASE(S)
Definition: smt2_conv.cpp:49
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
int solver(std::istream &in)
BigInt mp_integer
Definition: smt_terms.h:12
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
bool has_byte_operator(const exprt &src)
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define UNIMPLEMENTED
Definition: invariant.h:525
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:437
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:496
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1745
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1456
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:464
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1160
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1044
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:3249
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1595
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1308
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3097
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:370
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1657
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2062
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:260
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:531
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition: std_expr.h:1204
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
std::size_t unsafe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:40
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t object_bits
Definition: config.h:321