cprover
Loading...
Searching...
No Matches
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>
30#include <util/prefix.h>
31#include <util/range.h>
32#include <util/simplify_expr.h>
33#include <util/std_expr.h>
34#include <util/string2int.h>
36#include <util/threeval.h>
37
42
43#include "smt2_tokenizer.h"
44
45#include <cstdint>
46
47// Mark different kinds of error conditions
48
49// Unexpected types and other combinations not implemented and not
50// expected to be needed
51#define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
52
53// General todos
54#define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
55
57 const namespacet &_ns,
58 const std::string &_benchmark,
59 const std::string &_notes,
60 const std::string &_logic,
61 solvert _solver,
62 std::ostream &_out)
63 : use_FPA_theory(false),
64 use_array_of_bool(false),
65 use_as_const(false),
67 use_datatypes(false),
69 emit_set_logic(true),
70 ns(_ns),
71 out(_out),
72 benchmark(_benchmark),
73 notes(_notes),
74 logic(_logic),
75 solver(_solver),
76 boolbv_width(_ns),
77 pointer_logic(_ns),
79{
80 // We set some defaults differently
81 // for some solvers.
82
83 switch(solver)
84 {
86 break;
87
89 use_FPA_theory = true;
90 use_array_of_bool = true;
91 use_as_const = true;
94 emit_set_logic = false;
95 break;
96
98 break;
99
101 use_FPA_theory = true;
102 use_array_of_bool = true;
103 use_as_const = true;
105 emit_set_logic = false;
106 break;
107
108 case solvert::CVC3:
109 break;
110
111 case solvert::CVC4:
112 logic = "ALL";
113 use_array_of_bool = true;
114 use_as_const = true;
115 break;
116
117 case solvert::CVC5:
118 logic = "ALL";
119 use_FPA_theory = true;
120 use_array_of_bool = true;
121 use_as_const = true;
123 use_datatypes = true;
124 break;
125
126 case solvert::MATHSAT:
127 break;
128
129 case solvert::YICES:
130 break;
131
132 case solvert::Z3:
133 use_array_of_bool = true;
134 use_as_const = true;
137 emit_set_logic = false;
138 use_datatypes = true;
139 break;
140 }
141
142 write_header();
143}
144
146{
147 return "SMT2";
148}
149
150void smt2_convt::print_assignment(std::ostream &os) const
151{
152 // Boolean stuff
153
154 for(std::size_t v=0; v<boolean_assignment.size(); v++)
155 os << "b" << v << "=" << boolean_assignment[v] << "\n";
156
157 // others
158}
159
161{
162 if(l.is_true())
163 return tvt(true);
164 if(l.is_false())
165 return tvt(false);
166
167 INVARIANT(
168 l.var_no() < boolean_assignment.size(),
169 "variable number shall be within bounds");
170 return tvt(boolean_assignment[l.var_no()]^l.sign());
171}
172
174{
175 out << "; SMT 2" << "\n";
176
177 switch(solver)
178 {
179 // clang-format off
180 case solvert::GENERIC: break;
181 case solvert::BITWUZLA: out << "; Generated for Bitwuzla\n"; break;
182 case solvert::BOOLECTOR: out << "; Generated for Boolector\n"; break;
184 out << "; Generated for the CPROVER SMT2 solver\n"; break;
185 case solvert::CVC3: out << "; Generated for CVC 3\n"; break;
186 case solvert::CVC4: out << "; Generated for CVC 4\n"; break;
187 case solvert::CVC5: out << "; Generated for CVC 5\n"; break;
188 case solvert::MATHSAT: out << "; Generated for MathSAT\n"; break;
189 case solvert::YICES: out << "; Generated for Yices\n"; break;
190 case solvert::Z3: out << "; Generated for Z3\n"; break;
191 // clang-format on
192 }
193
194 out << "(set-info :source \"" << notes << "\")" << "\n";
195
196 out << "(set-option :produce-models true)" << "\n";
197
198 // We use a broad mixture of logics, so on some solvers
199 // its better not to declare here.
200 // set-logic should come after setting options
201 if(emit_set_logic && !logic.empty())
202 out << "(set-logic " << logic << ")" << "\n";
203}
204
206{
207 out << "\n";
208
209 // fix up the object sizes
210 for(const auto &object : object_sizes)
211 define_object_size(object.second, object.first);
212
213 if(use_check_sat_assuming && !assumptions.empty())
214 {
215 out << "(check-sat-assuming (";
216 for(const auto &assumption : assumptions)
217 convert_literal(assumption);
218 out << "))\n";
219 }
220 else
221 {
222 // add the assumptions, if any
223 if(!assumptions.empty())
224 {
225 out << "; assumptions\n";
226
227 for(const auto &assumption : assumptions)
228 {
229 out << "(assert ";
230 convert_literal(assumption);
231 out << ")"
232 << "\n";
233 }
234 }
235
236 out << "(check-sat)\n";
237 }
238
239 out << "\n";
240
242 {
243 for(const auto &id : smt2_identifiers)
244 out << "(get-value (" << id << "))"
245 << "\n";
246 }
247
248 out << "\n";
249
250 out << "(exit)\n";
251
252 out << "; end of SMT2 file"
253 << "\n";
254}
255
257static bool is_zero_width(const typet &type, const namespacet &ns)
258{
259 if(type.id() == ID_empty)
260 return true;
261 else if(type.id() == ID_struct_tag)
262 return is_zero_width(ns.follow_tag(to_struct_tag_type(type)), ns);
263 else if(type.id() == ID_union_tag)
264 return is_zero_width(ns.follow_tag(to_union_tag_type(type)), ns);
265 else if(type.id() == ID_struct || type.id() == ID_union)
266 {
267 for(const auto &comp : to_struct_union_type(type).components())
268 {
269 if(!is_zero_width(comp.type(), ns))
270 return false;
271 }
272 return true;
273 }
274 else if(auto array_type = type_try_dynamic_cast<array_typet>(type))
275 {
276 // we ignore array_type->size().is_zero() for now as there may be
277 // out-of-bounds accesses that we need to model
278 return is_zero_width(array_type->element_type(), ns);
279 }
280 else
281 return false;
282}
283
285 const irep_idt &id,
286 const object_size_exprt &expr)
287{
288 const exprt &ptr = expr.pointer();
289 std::size_t pointer_width = boolbv_width(ptr.type());
290 std::size_t number = 0;
291 std::size_t h=pointer_width-1;
292 std::size_t l=pointer_width-config.bv_encoding.object_bits;
293
294 for(const auto &o : pointer_logic.objects)
295 {
296 const typet &type = o.type();
297 auto size_expr = size_of_expr(type, ns);
298
299 if(
300 (o.id() != ID_symbol && o.id() != ID_string_constant) ||
301 !size_expr.has_value())
302 {
303 ++number;
304 continue;
305 }
306
307 find_symbols(*size_expr);
308 out << "(assert (=> (= "
309 << "((_ extract " << h << " " << l << ") ";
310 convert_expr(ptr);
311 out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))"
312 << "(= " << id << " ";
313 convert_expr(*size_expr);
314 out << ")))\n";
315
316 ++number;
317 }
318}
319
321{
322 if(assumption.is_nil())
323 write_footer();
324 else
325 {
326 assumptions.push_back(convert(assumption));
327 write_footer();
328 assumptions.pop_back();
329 }
330
331 out.flush();
333}
334
335exprt smt2_convt::get(const exprt &expr) const
336{
337 if(expr.id()==ID_symbol)
338 {
339 const irep_idt &id=to_symbol_expr(expr).get_identifier();
340
341 identifier_mapt::const_iterator it=identifier_map.find(id);
342
343 if(it!=identifier_map.end())
344 return it->second.value;
345 return expr;
346 }
347 else if(expr.id()==ID_nondet_symbol)
348 {
350
351 identifier_mapt::const_iterator it=identifier_map.find(id);
352
353 if(it!=identifier_map.end())
354 return it->second.value;
355 }
356 else if(expr.id() == ID_literal)
357 {
358 auto l = to_literal_expr(expr).get_literal();
359 if(l_get(l).is_true())
360 return true_exprt();
361 else
362 return false_exprt();
363 }
364 else if(expr.id() == ID_not)
365 {
366 auto op = get(to_not_expr(expr).op());
367 if(op.is_true())
368 return false_exprt();
369 else if(op.is_false())
370 return true_exprt();
371 }
372 else if(
373 expr.is_constant() || expr.id() == ID_empty_union ||
374 (!expr.has_operands() && (expr.id() == ID_struct || expr.id() == ID_array)))
375 {
376 return expr;
377 }
378 else if(expr.has_operands())
379 {
380 exprt copy = expr;
381 for(auto &op : copy.operands())
382 {
383 exprt eval_op = get(op);
384 if(eval_op.is_nil())
385 return nil_exprt{};
386 op = std::move(eval_op);
387 }
388 return copy;
389 }
390
391 return nil_exprt();
392}
393
395 const irept &src,
396 const typet &type)
397{
398 // See http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf for the
399 // syntax of SMTlib2 literals.
400 //
401 // A literal expression is one of the following forms:
402 //
403 // * Numeral -- this is a natural number in decimal and is of the form:
404 // 0|([1-9][0-9]*)
405 // * Decimal -- this is a decimal expansion of a real number of the form:
406 // (0|[1-9][0-9]*)[.]([0-9]+)
407 // * Binary -- this is a natural number in binary and is of the form:
408 // #b[01]+
409 // * Hex -- this is a natural number in hexadecimal and is of the form:
410 // #x[0-9a-fA-F]+
411 //
412 // Right now I'm not parsing decimals. It'd be nice if we had a real YACC
413 // parser here, but whatever.
414
415 mp_integer value;
416
417 if(!src.id().empty())
418 {
419 const std::string &s=src.id_string();
420
421 if(s.size()>=2 && s[0]=='#' && s[1]=='b')
422 {
423 // Binary #b010101
424 value=string2integer(s.substr(2), 2);
425 }
426 else if(s.size()>=2 && s[0]=='#' && s[1]=='x')
427 {
428 // Hex #x012345
429 value=string2integer(s.substr(2), 16);
430 }
431 else
432 {
433 // Numeral
434 value=string2integer(s);
435 }
436 }
437 else if(src.get_sub().size()==2 &&
438 src.get_sub()[0].id()=="-") // (- 100)
439 {
440 value=-string2integer(src.get_sub()[1].id_string());
441 }
442 else if(src.get_sub().size()==3 &&
443 src.get_sub()[0].id()=="_" &&
444 // (_ bvDECIMAL_VALUE SIZE)
445 src.get_sub()[1].id_string().substr(0, 2)=="bv")
446 {
447 value=string2integer(src.get_sub()[1].id_string().substr(2));
448 }
449 else if(src.get_sub().size()==4 &&
450 src.get_sub()[0].id()=="fp") // (fp signbv exponentbv significandbv)
451 {
452 if(type.id()==ID_floatbv)
453 {
454 const floatbv_typet &floatbv_type=to_floatbv_type(type);
457 parse_literal(src.get_sub()[2], unsignedbv_typet(floatbv_type.get_e()));
458 constant_exprt s3 =
459 parse_literal(src.get_sub()[3], unsignedbv_typet(floatbv_type.get_f()));
460
461 const auto s1_int = numeric_cast_v<mp_integer>(s1);
462 const auto s2_int = numeric_cast_v<mp_integer>(s2);
463 const auto s3_int = numeric_cast_v<mp_integer>(s3);
464
465 // stitch the bits together
466 value = bitwise_or(
467 s1_int << (floatbv_type.get_e() + floatbv_type.get_f()),
468 bitwise_or((s2_int << floatbv_type.get_f()), s3_int));
469 }
470 else
471 value=0;
472 }
473 else if(src.get_sub().size()==4 &&
474 src.get_sub()[0].id()=="_" &&
475 src.get_sub()[1].id()=="+oo") // (_ +oo e s)
476 {
477 std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
478 std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
480 .to_expr();
481 }
482 else if(src.get_sub().size()==4 &&
483 src.get_sub()[0].id()=="_" &&
484 src.get_sub()[1].id()=="-oo") // (_ -oo e s)
485 {
486 std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
487 std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
489 .to_expr();
490 }
491 else if(src.get_sub().size()==4 &&
492 src.get_sub()[0].id()=="_" &&
493 src.get_sub()[1].id()=="NaN") // (_ NaN e s)
494 {
495 std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
496 std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
498 }
499
500 if(type.id()==ID_signedbv ||
501 type.id()==ID_unsignedbv ||
502 type.id()==ID_c_enum ||
503 type.id()==ID_c_bool)
504 {
505 return from_integer(value, type);
506 }
507 else if(type.id()==ID_c_enum_tag)
508 {
509 constant_exprt result =
510 from_integer(value, ns.follow_tag(to_c_enum_tag_type(type)));
511
512 // restore the c_enum_tag type
513 result.type() = type;
514 return result;
515 }
516 else if(type.id()==ID_fixedbv ||
517 type.id()==ID_floatbv)
518 {
519 std::size_t width=boolbv_width(type);
520 return constant_exprt(integer2bvrep(value, width), type);
521 }
522 else if(type.id() == ID_integer)
523 {
524 return from_integer(value, type);
525 }
526 else if(type.id() == ID_range)
527 {
528 return from_integer(value + to_range_type(type).get_from(), type);
529 }
530 else
532 "smt2_convt::parse_literal should not be of unsupported type " +
533 type.id_string());
534}
535
537 const irept &src,
538 const array_typet &type)
539{
540 std::unordered_map<int64_t, exprt> operands_map;
541 walk_array_tree(&operands_map, src, type);
542 exprt::operandst operands;
543 // Try to find the default value, if there is none then set it
544 auto maybe_default_op = operands_map.find(-1);
545 exprt default_op;
546 if(maybe_default_op == operands_map.end())
547 default_op = nil_exprt();
548 else
549 default_op = maybe_default_op->second;
550 int64_t i = 0;
551 auto maybe_size = numeric_cast<std::int64_t>(type.size());
552 if(maybe_size.has_value())
553 {
554 while(i < maybe_size.value())
555 {
556 auto found_op = operands_map.find(i);
557 if(found_op != operands_map.end())
558 operands.emplace_back(found_op->second);
559 else
560 operands.emplace_back(default_op);
561 i++;
562 }
563 }
564 else
565 {
566 // Array size is unknown, keep adding with known indexes in order
567 // until we fail to find one.
568 auto found_op = operands_map.find(i);
569 while(found_op != operands_map.end())
570 {
571 operands.emplace_back(found_op->second);
572 i++;
573 found_op = operands_map.find(i);
574 }
575 operands.emplace_back(default_op);
576 }
577 return array_exprt(operands, type);
578}
579
581 std::unordered_map<int64_t, exprt> *operands_map,
582 const irept &src,
583 const array_typet &type)
584{
585 if(src.get_sub().size()==4 && src.get_sub()[0].id()=="store")
586 {
587 // This is the SMT syntax being parsed here
588 // (store array index value)
589 // Recurse
590 walk_array_tree(operands_map, src.get_sub()[1], type);
591 const auto index_expr = parse_rec(src.get_sub()[2], type.size().type());
592 const constant_exprt index_constant = to_constant_expr(index_expr);
593 mp_integer tempint;
594 bool failure = to_integer(index_constant, tempint);
595 if(failure)
596 return;
597 long index = tempint.to_long();
598 exprt value = parse_rec(src.get_sub()[3], type.element_type());
599 operands_map->emplace(index, value);
600 }
601 else if(src.get_sub().size()==2 &&
602 src.get_sub()[0].get_sub().size()==3 &&
603 src.get_sub()[0].get_sub()[0].id()=="as" &&
604 src.get_sub()[0].get_sub()[1].id()=="const")
605 {
606 // (as const type_info default_value)
607 exprt default_value = parse_rec(src.get_sub()[1], type.element_type());
608 operands_map->emplace(-1, default_value);
609 }
610 else
611 {
612 auto bindings_it = current_bindings.find(src.id());
613 if(bindings_it != current_bindings.end())
614 walk_array_tree(operands_map, bindings_it->second, type);
615 }
616}
617
619 const irept &src,
620 const union_typet &type)
621{
622 // these are always flat
623 PRECONDITION(!type.components().empty());
624 const union_typet::componentt &first=type.components().front();
625 std::size_t width=boolbv_width(type);
626 exprt value = parse_rec(src, unsignedbv_typet(width));
627 if(value.is_nil())
628 return nil_exprt();
629 const typecast_exprt converted(value, first.type());
630 return union_exprt(first.get_name(), converted, type);
631}
632
635{
636 const struct_typet::componentst &components =
637 type.components();
638
639 struct_exprt result(exprt::operandst(components.size(), nil_exprt()), type);
640
641 if(components.empty())
642 return result;
643
644 if(use_datatypes)
645 {
646 // Structs look like:
647 // (mk-struct.1 <component0> <component1> ... <componentN>)
648 std::size_t j = 1;
649 for(std::size_t i=0; i<components.size(); i++)
650 {
651 const struct_typet::componentt &c=components[i];
652 if(is_zero_width(components[i].type(), ns))
653 {
654 result.operands()[i] = nil_exprt{};
655 }
656 else
657 {
659 src.get_sub().size() > j, "insufficient number of component values");
660 result.operands()[i] = parse_rec(src.get_sub()[j], c.type());
661 ++j;
662 }
663 }
664 }
665 else
666 {
667 // These are just flattened, i.e., we expect to see a monster bit vector.
668 std::size_t total_width=boolbv_width(type);
669 const auto l = parse_literal(src, unsignedbv_typet(total_width));
670
671 const irep_idt binary =
673
674 CHECK_RETURN(binary.size() == total_width);
675
676 std::size_t offset=0;
677
678 for(std::size_t i=0; i<components.size(); i++)
679 {
680 if(is_zero_width(components[i].type(), ns))
681 continue;
682
683 std::size_t component_width=boolbv_width(components[i].type());
684
685 INVARIANT(
686 offset + component_width <= total_width,
687 "struct component bits shall be within struct bit vector");
688
689 std::string component_binary=
690 "#b"+id2string(binary).substr(
691 total_width-offset-component_width, component_width);
692
693 result.operands()[i]=
694 parse_rec(irept(component_binary), components[i].type());
695
696 offset+=component_width;
697 }
698 }
699
700 return result;
701}
702
703exprt smt2_convt::parse_rec(const irept &src, const typet &type)
704{
705 if(src.get_sub().size() == 3 && src.get_sub()[0].id() == ID_let)
706 {
707 // This is produced by Z3
708 // (let (....) (....))
709 auto previous_bindings = current_bindings;
710 for(const auto &binding : src.get_sub()[1].get_sub())
711 {
712 const irep_idt &name = binding.get_sub()[0].id();
713 current_bindings.emplace(name, binding.get_sub()[1]);
714 }
715 exprt result = parse_rec(src.get_sub()[2], type);
716 current_bindings = std::move(previous_bindings);
717 return result;
718 }
719
720 auto bindings_it = current_bindings.find(src.id());
721 if(bindings_it != current_bindings.end())
722 {
723 return parse_rec(bindings_it->second, type);
724 }
725
726 if(
727 type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
728 type.id() == ID_integer || type.id() == ID_rational ||
729 type.id() == ID_real || type.id() == ID_c_enum ||
730 type.id() == ID_c_enum_tag || type.id() == ID_fixedbv ||
731 type.id() == ID_floatbv || type.id() == ID_c_bool || type.id() == ID_range)
732 {
733 return parse_literal(src, type);
734 }
735 else if(type.id()==ID_bool)
736 {
737 if(src.id()==ID_1 || src.id()==ID_true)
738 return true_exprt();
739 else if(src.id()==ID_0 || src.id()==ID_false)
740 return false_exprt();
741 }
742 else if(type.id()==ID_pointer)
743 {
744 // these come in as bit-vector literals
745 std::size_t width=boolbv_width(type);
746 constant_exprt bv_expr = parse_literal(src, unsignedbv_typet(width));
747
749
750 // split into object and offset
751 mp_integer pow=power(2, width-config.bv_encoding.object_bits);
754 bv_expr.get_value(),
755 pointer_logic.pointer_expr(ptr, to_pointer_type(type)));
756 }
757 else if(type.id()==ID_struct)
758 {
759 return parse_struct(src, to_struct_type(type));
760 }
761 else if(type.id() == ID_struct_tag)
762 {
763 auto struct_expr =
764 parse_struct(src, ns.follow_tag(to_struct_tag_type(type)));
765 // restore the tag type
766 struct_expr.type() = type;
767 return std::move(struct_expr);
768 }
769 else if(type.id()==ID_union)
770 {
771 return parse_union(src, to_union_type(type));
772 }
773 else if(type.id() == ID_union_tag)
774 {
775 auto union_expr = parse_union(src, ns.follow_tag(to_union_tag_type(type)));
776 // restore the tag type
777 union_expr.type() = type;
778 return union_expr;
779 }
780 else if(type.id()==ID_array)
781 {
782 return parse_array(src, to_array_type(type));
783 }
784
785 return nil_exprt();
786}
787
789 const exprt &expr,
790 const pointer_typet &result_type)
791{
792 if(
793 expr.id() == ID_symbol || expr.is_constant() ||
794 expr.id() == ID_string_constant || expr.id() == ID_label)
795 {
796 const std::size_t object_bits = config.bv_encoding.object_bits;
797 const std::size_t max_objects = std::size_t(1) << object_bits;
798 const mp_integer object_id = pointer_logic.add_object(expr);
799
800 if(object_id >= max_objects)
801 {
803 "too many addressed objects: maximum number of objects is set to 2^n=" +
804 std::to_string(max_objects) +
805 " (with n=" + std::to_string(object_bits) + "); " +
806 "use the `--object-bits n` option to increase the maximum number"};
807 }
808
809 out << "(concat (_ bv" << object_id << " " << object_bits << ")"
810 << " (_ bv0 " << boolbv_width(result_type) - object_bits << "))";
811 }
812 else if(expr.id()==ID_index)
813 {
814 const index_exprt &index_expr = to_index_expr(expr);
815
816 const exprt &array = index_expr.array();
817 const exprt &index = index_expr.index();
818
819 if(index.is_zero())
820 {
821 if(array.type().id()==ID_pointer)
822 convert_expr(array);
823 else if(array.type().id()==ID_array)
824 convert_address_of_rec(array, result_type);
825 else
827 }
828 else
829 {
830 // this is really pointer arithmetic
831 index_exprt new_index_expr = index_expr;
832 new_index_expr.index() = from_integer(0, index.type());
833
834 address_of_exprt address_of_expr(
835 new_index_expr,
837
838 plus_exprt plus_expr{address_of_expr, index};
839
840 convert_expr(plus_expr);
841 }
842 }
843 else if(expr.id()==ID_member)
844 {
845 const member_exprt &member_expr=to_member_expr(expr);
846
847 const exprt &struct_op=member_expr.struct_op();
848 const typet &struct_op_type = struct_op.type();
849
851 struct_op_type.id() == ID_struct || struct_op_type.id() == ID_struct_tag,
852 "member expression operand shall have struct type");
853
854 const struct_typet &struct_type =
855 struct_op_type.id() == ID_struct_tag
856 ? ns.follow_tag(to_struct_tag_type(struct_op_type))
857 : to_struct_type(struct_op_type);
858
859 const irep_idt &component_name = member_expr.get_component_name();
860
861 const auto offset = member_offset(struct_type, component_name, ns);
862 CHECK_RETURN(offset.has_value() && *offset >= 0);
863
864 unsignedbv_typet index_type(boolbv_width(result_type));
865
866 // pointer arithmetic
867 out << "(bvadd ";
868 convert_address_of_rec(struct_op, result_type);
869 convert_expr(from_integer(*offset, index_type));
870 out << ")"; // bvadd
871 }
872 else if(expr.id()==ID_if)
873 {
874 const if_exprt &if_expr = to_if_expr(expr);
875
876 out << "(ite ";
877 convert_expr(if_expr.cond());
878 out << " ";
879 convert_address_of_rec(if_expr.true_case(), result_type);
880 out << " ";
881 convert_address_of_rec(if_expr.false_case(), result_type);
882 out << ")";
883 }
884 else
885 INVARIANT(
886 false,
887 "operand of address of expression should not be of kind " +
888 expr.id_string());
889}
890
891static bool has_quantifier(const exprt &expr)
892{
893 bool result = false;
894 expr.visit_post([&result](const exprt &node) {
895 if(node.id() == ID_exists || node.id() == ID_forall)
896 result = true;
897 });
898 return result;
899}
900
902{
903 PRECONDITION(expr.is_boolean());
904
905 // Three cases where no new handle is needed.
906
907 if(expr.is_true())
908 return const_literal(true);
909 else if(expr.is_false())
910 return const_literal(false);
911 else if(expr.id()==ID_literal)
912 return to_literal_expr(expr).get_literal();
913
914 // Need a new handle
915
916 out << "\n";
917
918 exprt prepared_expr = prepare_for_convert_expr(expr);
919
922
923 out << "; convert\n";
924 out << "; Converting var_no " << l.var_no() << " with expr ID of "
925 << expr.id_string() << "\n";
926 // We're converting the expression, so store it in the defined_expressions
927 // store and in future we use the literal instead of the whole expression
928 // Note that here we are always converting, so we do not need to consider
929 // other literal kinds, only "|B###|"
930
931 // Z3 refuses get-value when a defined symbol contains a quantifier.
932 if(has_quantifier(prepared_expr))
933 {
934 out << "(declare-fun ";
936 out << " () Bool)\n";
937 out << "(assert (= ";
939 out << ' ';
940 convert_expr(prepared_expr);
941 out << "))\n";
942 }
943 else
944 {
945 auto identifier =
946 convert_identifier(std::string{"B"} + std::to_string(l.var_no()));
947 defined_expressions[expr] = identifier;
948 smt2_identifiers.insert(identifier);
949 out << "(define-fun " << identifier << " () Bool ";
950 convert_expr(prepared_expr);
951 out << ")\n";
952 }
953
954 return l;
955}
956
958{
959 // We can only improve Booleans.
960 if(!expr.is_boolean())
961 return expr;
962
963 return literal_exprt(convert(expr));
964}
965
967{
968 if(l==const_literal(false))
969 out << "false";
970 else if(l==const_literal(true))
971 out << "true";
972 else
973 {
974 if(l.sign())
975 out << "(not ";
976
977 const auto identifier =
978 convert_identifier("B" + std::to_string(l.var_no()));
979
980 out << identifier;
981
982 if(l.sign())
983 out << ")";
984
985 smt2_identifiers.insert(identifier);
986 }
987}
988
990{
992}
993
994void smt2_convt::push(const std::vector<exprt> &_assumptions)
995{
996 INVARIANT(assumptions.empty(), "nested contexts are not supported");
997
998 assumptions.reserve(_assumptions.size());
999 for(auto &assumption : _assumptions)
1000 assumptions.push_back(convert(assumption));
1001}
1002
1004{
1005 assumptions.clear();
1006}
1007
1008static bool is_smt2_simple_identifier(const std::string &identifier)
1009{
1010 if(identifier.empty())
1011 return false;
1012
1013 if(isdigit(identifier[0]))
1014 return false;
1015
1016 for(auto ch : id2string(identifier))
1017 {
1019 return false;
1020 }
1021
1022 return true;
1023}
1024
1025std::string smt2_convt::convert_identifier(const irep_idt &identifier)
1026{
1027 // Is this a "simple identifier"?
1028 if(is_smt2_simple_identifier(id2string(identifier)))
1029 return id2string(identifier);
1030
1031 // Backslashes are disallowed in quoted symbols just for simplicity.
1032 // Otherwise, for Common Lisp compatibility they would have to be treated
1033 // as escaping symbols.
1034
1035 std::string result = "|";
1036
1037 for(auto ch : identifier)
1038 {
1039 switch(ch)
1040 {
1041 case '|':
1042 case '\\':
1043 case '&': // we use the & for escaping
1044 result+='&';
1045 result+=std::to_string(ch);
1046 result+=';';
1047 break;
1048
1049 case '$': // $ _is_ allowed
1050 default:
1051 result+=ch;
1052 }
1053 }
1054
1055 result += '|';
1056
1057 return result;
1058}
1059
1060std::string smt2_convt::type2id(const typet &type) const
1061{
1062 if(type.id()==ID_floatbv)
1063 {
1065 return "f"+std::to_string(spec.width())+"_"+std::to_string(spec.f);
1066 }
1067 else if(type.id() == ID_bv)
1068 {
1069 return "B" + std::to_string(to_bitvector_type(type).get_width());
1070 }
1071 else if(type.id()==ID_unsignedbv)
1072 {
1073 return "u"+std::to_string(to_unsignedbv_type(type).get_width());
1074 }
1075 else if(type.id()==ID_c_bool)
1076 {
1077 return "u"+std::to_string(to_c_bool_type(type).get_width());
1078 }
1079 else if(type.id()==ID_signedbv)
1080 {
1081 return "s"+std::to_string(to_signedbv_type(type).get_width());
1082 }
1083 else if(type.id()==ID_bool)
1084 {
1085 return "b";
1086 }
1087 else if(type.id()==ID_c_enum_tag)
1088 {
1089 return type2id(ns.follow_tag(to_c_enum_tag_type(type)).underlying_type());
1090 }
1091 else if(type.id() == ID_pointer)
1092 {
1093 return "p" + std::to_string(to_pointer_type(type).get_width());
1094 }
1095 else if(type.id() == ID_struct_tag)
1096 {
1097 if(use_datatypes)
1098 return datatype_map.at(type);
1099 else
1100 return "S" + std::to_string(boolbv_width(type));
1101 }
1102 else if(type.id() == ID_union_tag)
1103 {
1104 return "U" + std::to_string(boolbv_width(type));
1105 }
1106 else if(type.id() == ID_array)
1107 {
1108 return "A" + type2id(to_array_type(type).element_type());
1109 }
1110 else
1111 {
1113 }
1114}
1115
1116std::string smt2_convt::floatbv_suffix(const exprt &expr) const
1117{
1118 PRECONDITION(!expr.operands().empty());
1119 return "_" + type2id(to_multi_ary_expr(expr).op0().type()) + "->" +
1120 type2id(expr.type());
1121}
1122
1124{
1126
1127 if(expr.id()==ID_symbol)
1128 {
1129 const irep_idt &id = to_symbol_expr(expr).get_identifier();
1130 out << convert_identifier(id);
1131 return;
1132 }
1133
1134 if(expr.id()==ID_smt2_symbol)
1135 {
1136 const irep_idt &id = to_smt2_symbol(expr).get_identifier();
1137 out << id;
1138 return;
1139 }
1140
1141 INVARIANT(
1142 !expr.operands().empty(), "non-symbol expressions shall have operands");
1143
1144 out << '('
1146 "float_bv." + expr.id_string() + floatbv_suffix(expr));
1147
1148 for(const auto &op : expr.operands())
1149 {
1150 out << ' ';
1151 convert_expr(op);
1152 }
1153
1154 out << ')';
1155}
1156
1157void smt2_convt::convert_string_literal(const std::string &s)
1158{
1159 out << '"';
1160 for(auto ch : s)
1161 {
1162 // " is escaped by double-quoting
1163 if(ch == '"')
1164 out << '"';
1165 out << ch;
1166 }
1167 out << '"';
1168}
1169
1171{
1172 // try hash table first
1173 auto converter_result = converters.find(expr.id());
1174 if(converter_result != converters.end())
1175 {
1176 converter_result->second(expr);
1177 return; // done
1178 }
1179
1180 // huge monster case split over expression id
1181 if(expr.id()==ID_symbol)
1182 {
1183 const irep_idt &id = to_symbol_expr(expr).get_identifier();
1184 DATA_INVARIANT(!id.empty(), "symbol must have identifier");
1185 out << convert_identifier(id);
1186 }
1187 else if(expr.id()==ID_nondet_symbol)
1188 {
1189 const irep_idt &id = to_nondet_symbol_expr(expr).get_identifier();
1190 DATA_INVARIANT(!id.empty(), "nondet symbol must have identifier");
1191 out << convert_identifier("nondet_" + id2string(id));
1192 }
1193 else if(expr.id()==ID_smt2_symbol)
1194 {
1195 const irep_idt &id = to_smt2_symbol(expr).get_identifier();
1196 DATA_INVARIANT(!id.empty(), "smt2 symbol must have identifier");
1197 out << id;
1198 }
1199 else if(expr.id()==ID_typecast)
1200 {
1202 }
1203 else if(expr.id()==ID_floatbv_typecast)
1204 {
1206 }
1207 else if(expr.id() == ID_floatbv_round_to_integral)
1208 {
1210 }
1211 else if(expr.id()==ID_struct)
1212 {
1214 }
1215 else if(expr.id()==ID_union)
1216 {
1218 }
1219 else if(expr.is_constant())
1220 {
1222 }
1223 else if(expr.id() == ID_concatenation && expr.operands().size() == 1)
1224 {
1226 expr.type() == expr.operands().front().type(),
1227 "concatenation over a single operand should have matching types",
1228 expr.pretty());
1229
1230 convert_expr(expr.operands().front());
1231 }
1232 else if(
1233 expr.id() == ID_concatenation || expr.id() == ID_bitand ||
1234 expr.id() == ID_bitor || expr.id() == ID_bitxor)
1235 {
1237 expr.operands().size() >= 2,
1238 "given expression should have at least two operands",
1239 expr.id_string());
1240
1241 out << "(";
1242
1243 if(expr.id()==ID_concatenation)
1244 out << "concat";
1245 else if(expr.id()==ID_bitand)
1246 out << "bvand";
1247 else if(expr.id()==ID_bitor)
1248 out << "bvor";
1249 else if(expr.id()==ID_bitxor)
1250 out << "bvxor";
1251 else if(expr.id()==ID_bitnand)
1252 out << "bvnand";
1253 else if(expr.id()==ID_bitnor)
1254 out << "bvnor";
1255
1256 for(const auto &op : expr.operands())
1257 {
1258 out << " ";
1259 flatten2bv(op);
1260 }
1261
1262 out << ")";
1263 }
1264 else if(
1265 expr.id() == ID_bitxnor || expr.id() == ID_bitnand ||
1266 expr.id() == ID_bitnor)
1267 {
1268 // SMT-LIB only has these as a binary expression,
1269 // owing to their ambiguity.
1270 if(expr.operands().size() == 2)
1271 {
1272 const auto &binary_expr = to_binary_expr(expr);
1273
1274 out << '(';
1275 if(binary_expr.id() == ID_bitxnor)
1276 out << "bvxnor";
1277 else if(binary_expr.id() == ID_bitnand)
1278 out << "bvnand";
1279 else if(binary_expr.id() == ID_bitnor)
1280 out << "bvnor";
1281 out << ' ';
1282 flatten2bv(binary_expr.op0());
1283 out << ' ';
1284 flatten2bv(binary_expr.op1());
1285 out << ')';
1286 }
1287 else if(expr.operands().size() == 1)
1288 {
1289 out << "(bvnot ";
1290 flatten2bv(to_unary_expr(expr).op());
1291 out << ')';
1292 }
1293 else if(expr.operands().size() >= 3)
1294 {
1295 out << "(bvnot (";
1296 if(expr.id() == ID_bitxnor)
1297 out << "bvxor";
1298 else if(expr.id() == ID_bitnand)
1299 out << "bvand";
1300 else if(expr.id() == ID_bitnor)
1301 out << "bvor";
1302
1303 for(const auto &op : expr.operands())
1304 {
1305 out << ' ';
1306 flatten2bv(op);
1307 }
1308
1309 out << "))"; // bvX, bvnot
1310 }
1311 else
1312 {
1314 expr.operands().size() >= 1,
1315 expr.id_string() + " should have at least one operand");
1316 }
1317 }
1318 else if(expr.id()==ID_bitnot)
1319 {
1320 const bitnot_exprt &bitnot_expr = to_bitnot_expr(expr);
1321
1322 out << "(bvnot ";
1323 convert_expr(bitnot_expr.op());
1324 out << ")";
1325 }
1326 else if(expr.id()==ID_unary_minus)
1327 {
1328 const unary_minus_exprt &unary_minus_expr = to_unary_minus_expr(expr);
1329 const auto &type = expr.type();
1330
1331 if(
1332 type.id() == ID_rational || type.id() == ID_integer ||
1333 type.id() == ID_real)
1334 {
1335 out << "(- ";
1336 convert_expr(unary_minus_expr.op());
1337 out << ")";
1338 }
1339 else if(type.id() == ID_range)
1340 {
1341 auto &range_type = to_range_type(type);
1342 PRECONDITION(type == unary_minus_expr.op().type());
1343 // turn -x into 0-x
1344 auto minus_expr =
1345 minus_exprt{range_type.zero_expr(), unary_minus_expr.op()};
1346 convert_expr(minus_expr);
1347 }
1348 else if(type.id() == ID_floatbv)
1349 {
1350 // this has no rounding mode
1351 if(use_FPA_theory)
1352 {
1353 out << "(fp.neg ";
1354 convert_expr(unary_minus_expr.op());
1355 out << ")";
1356 }
1357 else
1358 convert_floatbv(unary_minus_expr);
1359 }
1360 else
1361 {
1362 out << "(bvneg ";
1363 convert_expr(unary_minus_expr.op());
1364 out << ")";
1365 }
1366 }
1367 else if(expr.id()==ID_unary_plus)
1368 {
1369 // A no-op (apart from type promotion)
1370 convert_expr(to_unary_plus_expr(expr).op());
1371 }
1372 else if(expr.id()==ID_sign)
1373 {
1374 const sign_exprt &sign_expr = to_sign_expr(expr);
1375
1376 const typet &op_type = sign_expr.op().type();
1377
1378 if(op_type.id()==ID_floatbv)
1379 {
1380 if(use_FPA_theory)
1381 {
1382 out << "(fp.isNegative ";
1383 convert_expr(sign_expr.op());
1384 out << ")";
1385 }
1386 else
1387 convert_floatbv(sign_expr);
1388 }
1389 else if(op_type.id()==ID_signedbv)
1390 {
1391 std::size_t op_width=to_signedbv_type(op_type).get_width();
1392
1393 out << "(bvslt ";
1394 convert_expr(sign_expr.op());
1395 out << " (_ bv0 " << op_width << "))";
1396 }
1397 else
1399 false,
1400 "sign should not be applied to unsupported type",
1401 sign_expr.type().id_string());
1402 }
1403 else if(expr.id()==ID_if)
1404 {
1405 const if_exprt &if_expr = to_if_expr(expr);
1406
1407 out << "(ite ";
1408 convert_expr(if_expr.cond());
1409 out << " ";
1410 convert_expr(if_expr.true_case());
1411 out << " ";
1412 convert_expr(if_expr.false_case());
1413 out << ")";
1414 }
1415 else if(expr.id()==ID_and ||
1416 expr.id()==ID_or ||
1417 expr.id()==ID_xor)
1418 {
1420 expr.is_boolean(),
1421 "logical and, or, and xor expressions should have Boolean type");
1423 expr.operands().size() >= 2,
1424 "logical and, or, and xor expressions should have at least two operands");
1425
1426 out << "(" << expr.id();
1427 for(const auto &op : expr.operands())
1428 {
1429 out << " ";
1430 convert_expr(op);
1431 }
1432 out << ")";
1433 }
1434 else if(expr.id() == ID_nand || expr.id() == ID_nor || expr.id() == ID_xnor)
1435 {
1437 expr.is_boolean(),
1438 "logical nand, nor, xnor expressions should have Boolean type");
1440 expr.operands().size() >= 1,
1441 "logical nand, nor, xnor expressions should have at least one operand");
1442
1443 // SMT-LIB doesn't have nand, nor, xnor
1444 out << "(not ";
1445 if(expr.operands().size() == 1)
1446 convert_expr(to_multi_ary_expr(expr).op0());
1447 else
1448 {
1449 if(expr.id() == ID_nand)
1450 out << "(and";
1451 else if(expr.id() == ID_nor)
1452 out << "(and";
1453 else if(expr.id() == ID_xnor)
1454 out << "(xor";
1455 else
1456 DATA_INVARIANT(false, "unexpected expression");
1457 for(const auto &op : expr.operands())
1458 {
1459 out << ' ';
1460 convert_expr(op);
1461 }
1462 out << ')'; // or, and, xor
1463 }
1464 out << ')'; // not
1465 }
1466 else if(expr.id()==ID_implies)
1467 {
1468 const implies_exprt &implies_expr = to_implies_expr(expr);
1469
1471 implies_expr.is_boolean(), "implies expression should have Boolean type");
1472
1473 out << "(=> ";
1474 convert_expr(implies_expr.op0());
1475 out << " ";
1476 convert_expr(implies_expr.op1());
1477 out << ")";
1478 }
1479 else if(expr.id()==ID_not)
1480 {
1481 const not_exprt &not_expr = to_not_expr(expr);
1482
1484 not_expr.is_boolean(), "not expression should have Boolean type");
1485
1486 out << "(not ";
1487 convert_expr(not_expr.op());
1488 out << ")";
1489 }
1490 else if(expr.id() == ID_equal)
1491 {
1492 const equal_exprt &equal_expr = to_equal_expr(expr);
1493
1495 equal_expr.op0().type() == equal_expr.op1().type(),
1496 "operands of equal expression shall have same type");
1497
1498 if(is_zero_width(equal_expr.lhs().type(), ns))
1499 {
1501 }
1502 else
1503 {
1504 out << "(= ";
1505 convert_expr(equal_expr.op0());
1506 out << " ";
1507 convert_expr(equal_expr.op1());
1508 out << ")";
1509 }
1510 }
1511 else if(expr.id() == ID_notequal)
1512 {
1513 const notequal_exprt &notequal_expr = to_notequal_expr(expr);
1514
1516 notequal_expr.op0().type() == notequal_expr.op1().type(),
1517 "operands of not equal expression shall have same type");
1518
1519 out << "(not (= ";
1520 convert_expr(notequal_expr.op0());
1521 out << " ";
1522 convert_expr(notequal_expr.op1());
1523 out << "))";
1524 }
1525 else if(expr.id()==ID_ieee_float_equal ||
1526 expr.id()==ID_ieee_float_notequal)
1527 {
1528 // These are not the same as (= A B)
1529 // because of NaN and negative zero.
1530 const auto &rel_expr = to_binary_relation_expr(expr);
1531
1533 rel_expr.lhs().type() == rel_expr.rhs().type(),
1534 "operands of float equal and not equal expressions shall have same type");
1535
1536 // The FPA theory properly treats NaN and negative zero.
1537 if(use_FPA_theory)
1538 {
1539 if(rel_expr.id() == ID_ieee_float_notequal)
1540 out << "(not ";
1541
1542 out << "(fp.eq ";
1543 convert_expr(rel_expr.lhs());
1544 out << " ";
1545 convert_expr(rel_expr.rhs());
1546 out << ")";
1547
1548 if(rel_expr.id() == ID_ieee_float_notequal)
1549 out << ")";
1550 }
1551 else
1552 convert_floatbv(expr);
1553 }
1554 else if(expr.id()==ID_le ||
1555 expr.id()==ID_lt ||
1556 expr.id()==ID_ge ||
1557 expr.id()==ID_gt)
1558 {
1560 }
1561 else if(expr.id()==ID_plus)
1562 {
1564 }
1565 else if(expr.id()==ID_floatbv_plus)
1566 {
1568 }
1569 else if(expr.id()==ID_minus)
1570 {
1572 }
1573 else if(expr.id()==ID_floatbv_minus)
1574 {
1576 }
1577 else if(expr.id()==ID_div)
1578 {
1579 convert_div(to_div_expr(expr));
1580 }
1581 else if(expr.id()==ID_floatbv_div)
1582 {
1584 }
1585 else if(expr.id()==ID_mod)
1586 {
1587 convert_mod(to_mod_expr(expr));
1588 }
1589 else if(expr.id() == ID_euclidean_mod)
1590 {
1592 }
1593 else if(expr.id()==ID_mult)
1594 {
1596 }
1597 else if(expr.id()==ID_floatbv_mult)
1598 {
1600 }
1601 else if(expr.id() == ID_floatbv_rem)
1602 {
1604 }
1605 else if(expr.id()==ID_address_of)
1606 {
1607 const address_of_exprt &address_of_expr = to_address_of_expr(expr);
1609 address_of_expr.object(), to_pointer_type(address_of_expr.type()));
1610 }
1611 else if(expr.id() == ID_array_of)
1612 {
1613 const auto &array_of_expr = to_array_of_expr(expr);
1614
1616 array_of_expr.type().id() == ID_array,
1617 "array of expression shall have array type");
1618
1619 if(use_as_const)
1620 {
1621 out << "((as const ";
1622 convert_type(array_of_expr.type());
1623 out << ") ";
1624 convert_expr(array_of_expr.what());
1625 out << ")";
1626 }
1627 else
1628 {
1629 defined_expressionst::const_iterator it =
1630 defined_expressions.find(array_of_expr);
1631 CHECK_RETURN(it != defined_expressions.end());
1632 out << it->second;
1633 }
1634 }
1635 else if(expr.id() == ID_array_comprehension)
1636 {
1637 const auto &array_comprehension = to_array_comprehension_expr(expr);
1638
1640 array_comprehension.type().id() == ID_array,
1641 "array_comprehension expression shall have array type");
1642
1644 {
1645 out << "(lambda ((";
1646 convert_expr(array_comprehension.arg());
1647 out << " ";
1648 convert_type(array_comprehension.type().size().type());
1649 out << ")) ";
1650 convert_expr(array_comprehension.body());
1651 out << ")";
1652 }
1653 else
1654 {
1655 const auto &it = defined_expressions.find(array_comprehension);
1656 CHECK_RETURN(it != defined_expressions.end());
1657 out << it->second;
1658 }
1659 }
1660 else if(expr.id()==ID_index)
1661 {
1663 }
1664 else if(expr.id()==ID_ashr ||
1665 expr.id()==ID_lshr ||
1666 expr.id()==ID_shl)
1667 {
1668 const shift_exprt &shift_expr = to_shift_expr(expr);
1669 const typet &type = shift_expr.type();
1670
1671 if(type.id()==ID_unsignedbv ||
1672 type.id()==ID_signedbv ||
1673 type.id()==ID_bv)
1674 {
1675 if(shift_expr.id() == ID_ashr)
1676 out << "(bvashr ";
1677 else if(shift_expr.id() == ID_lshr)
1678 out << "(bvlshr ";
1679 else if(shift_expr.id() == ID_shl)
1680 out << "(bvshl ";
1681 else
1683
1684 convert_expr(shift_expr.op());
1685 out << " ";
1686
1687 // SMT2 requires the shift distance to have the same width as
1688 // the value that is shifted -- odd!
1689
1690 const auto &distance_type = shift_expr.distance().type();
1691 if(distance_type.id() == ID_integer || distance_type.id() == ID_natural)
1692 {
1693 const mp_integer i =
1695
1696 // shift distance must be bit vector
1697 std::size_t width_op0 = boolbv_width(shift_expr.op().type());
1698 exprt tmp=from_integer(i, unsignedbv_typet(width_op0));
1699 convert_expr(tmp);
1700 }
1701 else if(
1702 distance_type.id() == ID_signedbv ||
1703 distance_type.id() == ID_unsignedbv ||
1704 distance_type.id() == ID_c_enum || distance_type.id() == ID_c_bool)
1705 {
1706 std::size_t width_op0 = boolbv_width(shift_expr.op().type());
1707 std::size_t width_op1 = boolbv_width(distance_type);
1708
1709 if(width_op0==width_op1)
1710 convert_expr(shift_expr.distance());
1711 else if(width_op0>width_op1)
1712 {
1713 out << "((_ zero_extend " << width_op0-width_op1 << ") ";
1714 convert_expr(shift_expr.distance());
1715 out << ")"; // zero_extend
1716 }
1717 else // width_op0<width_op1
1718 {
1719 out << "((_ extract " << width_op0-1 << " 0) ";
1720 convert_expr(shift_expr.distance());
1721 out << ")"; // extract
1722 }
1723 }
1724 else
1725 {
1727 "unsupported distance type for " + shift_expr.id_string() + ": " +
1728 distance_type.id_string());
1729 }
1730
1731 out << ")"; // bv*sh
1732 }
1733 else
1735 "unsupported type for " + shift_expr.id_string() + ": " +
1736 type.id_string());
1737 }
1738 else if(expr.id() == ID_rol || expr.id() == ID_ror)
1739 {
1740 const shift_exprt &shift_expr = to_shift_expr(expr);
1741 const typet &type = shift_expr.type();
1742
1743 if(
1744 type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
1745 type.id() == ID_bv)
1746 {
1747 // SMT-LIB offers rotate_left and rotate_right, but these require a
1748 // constant distance.
1749 if(shift_expr.id() == ID_rol)
1750 out << "((_ rotate_left";
1751 else if(shift_expr.id() == ID_ror)
1752 out << "((_ rotate_right";
1753 else
1755
1756 out << ' ';
1757
1758 auto distance_int_op = numeric_cast<mp_integer>(shift_expr.distance());
1759
1760 if(distance_int_op.has_value())
1761 {
1762 out << distance_int_op.value();
1763 }
1764 else
1766 "distance type for " + shift_expr.id_string() + "must be constant");
1767
1768 out << ") ";
1769 convert_expr(shift_expr.op());
1770
1771 out << ")"; // rotate_*
1772 }
1773 else
1775 "unsupported type for " + shift_expr.id_string() + ": " +
1776 type.id_string());
1777 }
1778 else if(expr.id() == ID_named_term)
1779 {
1780 const auto &named_term_expr = to_named_term_expr(expr);
1781 out << "(! ";
1782 convert(named_term_expr.value());
1783 out << " :named "
1784 << convert_identifier(named_term_expr.symbol().get_identifier()) << ')';
1785 }
1786 else if(expr.id()==ID_with)
1787 {
1789 }
1790 else if(expr.id()==ID_update)
1791 {
1793 }
1794 else if(expr.id() == ID_update_bit)
1795 {
1797 }
1798 else if(expr.id() == ID_update_bits)
1799 {
1801 }
1802 else if(expr.id() == ID_object_address)
1803 {
1804 out << "(object-address ";
1806 id2string(to_object_address_expr(expr).object_identifier()));
1807 out << ')';
1808 }
1809 else if(expr.id() == ID_element_address)
1810 {
1811 // We turn this binary expression into a ternary expression
1812 // by adding the size of the array elements as third argument.
1813 const auto &element_address_expr = to_element_address_expr(expr);
1814
1815 auto element_size_expr_opt =
1816 ::size_of_expr(element_address_expr.element_type(), ns);
1817 CHECK_RETURN(element_size_expr_opt.has_value());
1818
1819 out << "(element-address-" << type2id(expr.type()) << ' ';
1820 convert_expr(element_address_expr.base());
1821 out << ' ';
1822 convert_expr(element_address_expr.index());
1823 out << ' ';
1825 *element_size_expr_opt, element_address_expr.index().type()));
1826 out << ')';
1827 }
1828 else if(expr.id() == ID_field_address)
1829 {
1830 const auto &field_address_expr = to_field_address_expr(expr);
1831 out << "(field-address-" << type2id(expr.type()) << ' ';
1832 convert_expr(field_address_expr.base());
1833 out << ' ';
1834 convert_string_literal(id2string(field_address_expr.component_name()));
1835 out << ')';
1836 }
1837 else if(expr.id()==ID_member)
1838 {
1840 }
1841 else if(expr.id()==ID_pointer_offset)
1842 {
1843 const auto &op = to_pointer_offset_expr(expr).pointer();
1844
1846 op.type().id() == ID_pointer,
1847 "operand of pointer offset expression shall be of pointer type");
1848
1849 std::size_t offset_bits =
1850 boolbv_width(op.type()) - config.bv_encoding.object_bits;
1851 std::size_t result_width=boolbv_width(expr.type());
1852
1853 // max extract width
1854 if(offset_bits>result_width)
1855 offset_bits=result_width;
1856
1857 // too few bits?
1858 if(result_width>offset_bits)
1859 out << "((_ zero_extend " << result_width-offset_bits << ") ";
1860
1861 out << "((_ extract " << offset_bits-1 << " 0) ";
1862 convert_expr(op);
1863 out << ")";
1864
1865 if(result_width>offset_bits)
1866 out << ")"; // zero_extend
1867 }
1868 else if(expr.id()==ID_pointer_object)
1869 {
1870 const auto &op = to_pointer_object_expr(expr).pointer();
1871
1873 op.type().id() == ID_pointer,
1874 "pointer object expressions should be of pointer type");
1875
1876 std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
1877 std::size_t pointer_width = boolbv_width(op.type());
1878
1879 if(ext>0)
1880 out << "((_ zero_extend " << ext << ") ";
1881
1882 out << "((_ extract "
1883 << pointer_width-1 << " "
1884 << pointer_width-config.bv_encoding.object_bits << ") ";
1885 convert_expr(op);
1886 out << ")";
1887
1888 if(ext>0)
1889 out << ")"; // zero_extend
1890 }
1891 else if(expr.id() == ID_is_dynamic_object)
1892 {
1894 }
1895 else if(expr.id() == ID_is_invalid_pointer)
1896 {
1897 const auto &op = to_unary_expr(expr).op();
1898 std::size_t pointer_width = boolbv_width(op.type());
1899 out << "(= ((_ extract "
1900 << pointer_width-1 << " "
1901 << pointer_width-config.bv_encoding.object_bits << ") ";
1902 convert_expr(op);
1903 out << ") (_ bv" << pointer_logic.get_invalid_object()
1904 << " " << config.bv_encoding.object_bits << "))";
1905 }
1906 else if(expr.id()==ID_string_constant)
1907 {
1908 defined_expressionst::const_iterator it=defined_expressions.find(expr);
1909 CHECK_RETURN(it != defined_expressions.end());
1910 out << it->second;
1911 }
1912 else if(expr.id()==ID_extractbit)
1913 {
1914 const extractbit_exprt &extractbit_expr = to_extractbit_expr(expr);
1915
1916 if(extractbit_expr.index().is_constant())
1917 {
1918 const mp_integer i =
1920
1921 out << "(= ((_ extract " << i << " " << i << ") ";
1922 flatten2bv(extractbit_expr.src());
1923 out << ") #b1)";
1924 }
1925 else
1926 {
1927 out << "(= ((_ extract 0 0) ";
1928 // the arguments of the shift need to have the same width
1929 out << "(bvlshr ";
1930 flatten2bv(extractbit_expr.src());
1931 out << ' ';
1932 typecast_exprt tmp(extractbit_expr.index(), extractbit_expr.src().type());
1933 convert_expr(tmp);
1934 out << ")) #b1)"; // bvlshr, extract, =
1935 }
1936 }
1937 else if(expr.id() == ID_onehot)
1938 {
1939 convert_expr(to_onehot_expr(expr).lower());
1940 }
1941 else if(expr.id() == ID_onehot0)
1942 {
1943 convert_expr(to_onehot0_expr(expr).lower());
1944 }
1945 else if(expr.id()==ID_extractbits)
1946 {
1947 const extractbits_exprt &extractbits_expr = to_extractbits_expr(expr);
1948 auto width = boolbv_width(expr.type());
1949
1950 if(extractbits_expr.index().is_constant())
1951 {
1952 mp_integer index_i =
1954
1955 out << "((_ extract " << (width + index_i - 1) << " " << index_i << ") ";
1956 flatten2bv(extractbits_expr.src());
1957 out << ")";
1958 }
1959 else
1960 {
1961 #if 0
1962 out << "(= ((_ extract 0 0) ";
1963 // the arguments of the shift need to have the same width
1964 out << "(bvlshr ";
1965 convert_expr(expr.op0());
1966 typecast_exprt tmp(expr.op0().type());
1967 tmp.op0()=expr.op1();
1968 convert_expr(tmp);
1969 out << ")) bin1)"; // bvlshr, extract, =
1970 #endif
1971 SMT2_TODO("smt2: extractbits with non-constant index");
1972 }
1973 }
1974 else if(expr.id()==ID_replication)
1975 {
1976 const replication_exprt &replication_expr = to_replication_expr(expr);
1977
1978 mp_integer times = numeric_cast_v<mp_integer>(replication_expr.times());
1979
1980 out << "((_ repeat " << times << ") ";
1981 flatten2bv(replication_expr.op());
1982 out << ")";
1983 }
1984 else if(expr.id()==ID_byte_extract_little_endian ||
1985 expr.id()==ID_byte_extract_big_endian)
1986 {
1987 INVARIANT(
1988 false, "byte_extract ops should be lowered in prepare_for_convert_expr");
1989 }
1990 else if(expr.id()==ID_byte_update_little_endian ||
1991 expr.id()==ID_byte_update_big_endian)
1992 {
1993 INVARIANT(
1994 false, "byte_update ops should be lowered in prepare_for_convert_expr");
1995 }
1996 else if(expr.id()==ID_abs)
1997 {
1998 const abs_exprt &abs_expr = to_abs_expr(expr);
1999
2000 const typet &type = abs_expr.type();
2001
2002 if(type.id()==ID_signedbv)
2003 {
2004 std::size_t result_width = to_signedbv_type(type).get_width();
2005
2006 out << "(ite (bvslt ";
2007 convert_expr(abs_expr.op());
2008 out << " (_ bv0 " << result_width << ")) ";
2009 out << "(bvneg ";
2010 convert_expr(abs_expr.op());
2011 out << ") ";
2012 convert_expr(abs_expr.op());
2013 out << ")";
2014 }
2015 else if(type.id()==ID_fixedbv)
2016 {
2017 std::size_t result_width=to_fixedbv_type(type).get_width();
2018
2019 out << "(ite (bvslt ";
2020 convert_expr(abs_expr.op());
2021 out << " (_ bv0 " << result_width << ")) ";
2022 out << "(bvneg ";
2023 convert_expr(abs_expr.op());
2024 out << ") ";
2025 convert_expr(abs_expr.op());
2026 out << ")";
2027 }
2028 else if(type.id()==ID_floatbv)
2029 {
2030 if(use_FPA_theory)
2031 {
2032 out << "(fp.abs ";
2033 convert_expr(abs_expr.op());
2034 out << ")";
2035 }
2036 else
2037 convert_floatbv(abs_expr);
2038 }
2039 else
2041 }
2042 else if(expr.id()==ID_isnan)
2043 {
2044 const isnan_exprt &isnan_expr = to_isnan_expr(expr);
2045
2046 const typet &op_type = isnan_expr.op().type();
2047
2048 if(op_type.id()==ID_fixedbv)
2049 out << "false";
2050 else if(op_type.id()==ID_floatbv)
2051 {
2052 if(use_FPA_theory)
2053 {
2054 out << "(fp.isNaN ";
2055 convert_expr(isnan_expr.op());
2056 out << ")";
2057 }
2058 else
2059 convert_floatbv(isnan_expr);
2060 }
2061 else
2063 }
2064 else if(expr.id()==ID_isfinite)
2065 {
2066 const isfinite_exprt &isfinite_expr = to_isfinite_expr(expr);
2067
2068 const typet &op_type = isfinite_expr.op().type();
2069
2070 if(op_type.id()==ID_fixedbv)
2071 out << "true";
2072 else if(op_type.id()==ID_floatbv)
2073 {
2074 if(use_FPA_theory)
2075 {
2076 out << "(and ";
2077
2078 out << "(not (fp.isNaN ";
2079 convert_expr(isfinite_expr.op());
2080 out << "))";
2081
2082 out << "(not (fp.isInfinite ";
2083 convert_expr(isfinite_expr.op());
2084 out << "))";
2085
2086 out << ")";
2087 }
2088 else
2089 convert_floatbv(isfinite_expr);
2090 }
2091 else
2093 }
2094 else if(expr.id()==ID_isinf)
2095 {
2096 const isinf_exprt &isinf_expr = to_isinf_expr(expr);
2097
2098 const typet &op_type = isinf_expr.op().type();
2099
2100 if(op_type.id()==ID_fixedbv)
2101 out << "false";
2102 else if(op_type.id()==ID_floatbv)
2103 {
2104 if(use_FPA_theory)
2105 {
2106 out << "(fp.isInfinite ";
2107 convert_expr(isinf_expr.op());
2108 out << ")";
2109 }
2110 else
2111 convert_floatbv(isinf_expr);
2112 }
2113 else
2115 }
2116 else if(expr.id()==ID_isnormal)
2117 {
2118 const isnormal_exprt &isnormal_expr = to_isnormal_expr(expr);
2119
2120 const typet &op_type = isnormal_expr.op().type();
2121
2122 if(op_type.id()==ID_fixedbv)
2123 out << "true";
2124 else if(op_type.id()==ID_floatbv)
2125 {
2126 if(use_FPA_theory)
2127 {
2128 out << "(fp.isNormal ";
2129 convert_expr(isnormal_expr.op());
2130 out << ")";
2131 }
2132 else
2133 convert_floatbv(isnormal_expr);
2134 }
2135 else
2137 }
2138 else if(
2141 expr.id() == ID_overflow_result_plus ||
2142 expr.id() == ID_overflow_result_minus)
2143 {
2144 const bool keep_result = can_cast_expr<overflow_result_exprt>(expr);
2145
2146 const auto &op0 = to_binary_expr(expr).op0();
2147 const auto &op1 = to_binary_expr(expr).op1();
2148
2150 keep_result || expr.is_boolean(),
2151 "overflow plus and overflow minus expressions shall be of Boolean type");
2152
2153 bool subtract = can_cast_expr<minus_overflow_exprt>(expr) ||
2154 expr.id() == ID_overflow_result_minus;
2155 const typet &op_type = op0.type();
2156 std::size_t width=boolbv_width(op_type);
2157
2158 if(op_type.id()==ID_signedbv)
2159 {
2160 // an overflow occurs if the top two bits of the extended sum differ
2161 out << "(let ((?sum (";
2162 out << (subtract?"bvsub":"bvadd");
2163 out << " ((_ sign_extend 1) ";
2164 convert_expr(op0);
2165 out << ")";
2166 out << " ((_ sign_extend 1) ";
2167 convert_expr(op1);
2168 out << ")))) "; // sign_extend, bvadd/sub
2169 if(keep_result)
2170 {
2171 if(use_datatypes)
2172 {
2173 const std::string &smt_typename = datatype_map.at(expr.type());
2174
2175 // use the constructor for the Z3 datatype
2176 out << "(mk-" << smt_typename;
2177 }
2178 else
2179 out << "(concat";
2180
2181 out << " ((_ extract " << width - 1 << " 0) ?sum) ";
2182 if(!use_datatypes)
2183 out << "(ite ";
2184 }
2185 out << "(not (= "
2186 "((_ extract " << width << " " << width << ") ?sum) "
2187 "((_ extract " << (width-1) << " " << (width-1) << ") ?sum)";
2188 out << "))"; // =, not
2189 if(keep_result)
2190 {
2191 if(!use_datatypes)
2192 out << " #b1 #b0)";
2193 out << ")"; // concat
2194 }
2195 out << ")"; // let
2196 }
2197 else if(op_type.id()==ID_unsignedbv ||
2198 op_type.id()==ID_pointer)
2199 {
2200 // overflow is simply carry-out
2201 out << "(let ((?sum (" << (subtract ? "bvsub" : "bvadd");
2202 out << " ((_ zero_extend 1) ";
2203 convert_expr(op0);
2204 out << ")";
2205 out << " ((_ zero_extend 1) ";
2206 convert_expr(op1);
2207 out << "))))"; // zero_extend, bvsub/bvadd
2208 if(keep_result && !use_datatypes)
2209 out << " ?sum";
2210 else
2211 {
2212 if(keep_result && use_datatypes)
2213 {
2214 const std::string &smt_typename = datatype_map.at(expr.type());
2215
2216 // use the constructor for the Z3 datatype
2217 out << "(mk-" << smt_typename;
2218 out << " ((_ extract " << width - 1 << " 0) ?sum) ";
2219 }
2220
2221 out << "(= ";
2222 out << "((_ extract " << width << " " << width << ") ?sum)";
2223 out << "#b1)"; // =
2224
2225 if(keep_result && use_datatypes)
2226 out << ")"; // mk
2227 }
2228 out << ")"; // let
2229 }
2230 else
2232 false,
2233 "overflow check should not be performed on unsupported type",
2234 op_type.id_string());
2235 }
2236 else if(
2238 expr.id() == ID_overflow_result_mult)
2239 {
2240 const bool keep_result = can_cast_expr<overflow_result_exprt>(expr);
2241
2242 const auto &op0 = to_binary_expr(expr).op0();
2243 const auto &op1 = to_binary_expr(expr).op1();
2244
2246 keep_result || expr.is_boolean(),
2247 "overflow mult expression shall be of Boolean type");
2248
2249 // No better idea than to multiply with double the bits and then compare
2250 // with max value.
2251
2252 const typet &op_type = op0.type();
2253 std::size_t width=boolbv_width(op_type);
2254
2255 if(op_type.id()==ID_signedbv)
2256 {
2257 out << "(let ( (prod (bvmul ((_ sign_extend " << width << ") ";
2258 convert_expr(op0);
2259 out << ") ((_ sign_extend " << width << ") ";
2260 convert_expr(op1);
2261 out << ")) )) ";
2262 if(keep_result)
2263 {
2264 if(use_datatypes)
2265 {
2266 const std::string &smt_typename = datatype_map.at(expr.type());
2267
2268 // use the constructor for the Z3 datatype
2269 out << "(mk-" << smt_typename;
2270 }
2271 else
2272 out << "(concat";
2273
2274 out << " ((_ extract " << width - 1 << " 0) prod) ";
2275 if(!use_datatypes)
2276 out << "(ite ";
2277 }
2278 out << "(or (bvsge prod (_ bv" << power(2, width-1) << " "
2279 << width*2 << "))";
2280 out << " (bvslt prod (bvneg (_ bv" << power(2, width - 1) << " "
2281 << width * 2 << "))))";
2282 if(keep_result)
2283 {
2284 if(!use_datatypes)
2285 out << " #b1 #b0)";
2286 out << ")"; // concat
2287 }
2288 out << ")";
2289 }
2290 else if(op_type.id()==ID_unsignedbv)
2291 {
2292 out << "(let ((prod (bvmul ((_ zero_extend " << width << ") ";
2293 convert_expr(op0);
2294 out << ") ((_ zero_extend " << width << ") ";
2295 convert_expr(op1);
2296 out << ")))) ";
2297 if(keep_result)
2298 {
2299 if(use_datatypes)
2300 {
2301 const std::string &smt_typename = datatype_map.at(expr.type());
2302
2303 // use the constructor for the Z3 datatype
2304 out << "(mk-" << smt_typename;
2305 }
2306 else
2307 out << "(concat";
2308
2309 out << " ((_ extract " << width - 1 << " 0) prod) ";
2310 if(!use_datatypes)
2311 out << "(ite ";
2312 }
2313 out << "(bvuge prod (_ bv" << power(2, width) << " " << width * 2 << "))";
2314 if(keep_result)
2315 {
2316 if(!use_datatypes)
2317 out << " #b1 #b0)";
2318 out << ")"; // concat
2319 }
2320 out << ")";
2321 }
2322 else
2324 false,
2325 "overflow check should not be performed on unsupported type",
2326 op_type.id_string());
2327 }
2328 else if(expr.id() == ID_saturating_plus || expr.id() == ID_saturating_minus)
2329 {
2330 const bool subtract = expr.id() == ID_saturating_minus;
2331 const auto &op_type = expr.type();
2332 const auto &op0 = to_binary_expr(expr).op0();
2333 const auto &op1 = to_binary_expr(expr).op1();
2334
2335 if(op_type.id() == ID_signedbv)
2336 {
2337 auto width = to_signedbv_type(op_type).get_width();
2338
2339 // compute sum with one extra bit
2340 out << "(let ((?sum (";
2341 out << (subtract ? "bvsub" : "bvadd");
2342 out << " ((_ sign_extend 1) ";
2343 convert_expr(op0);
2344 out << ")";
2345 out << " ((_ sign_extend 1) ";
2346 convert_expr(op1);
2347 out << ")))) "; // sign_extend, bvadd/sub
2348
2349 // pick one of MAX, MIN, or the sum
2350 out << "(ite (= "
2351 "((_ extract "
2352 << width << " " << width
2353 << ") ?sum) "
2354 "((_ extract "
2355 << (width - 1) << " " << (width - 1) << ") ?sum)";
2356 out << ") "; // =
2357
2358 // no overflow and no underflow case, return the sum
2359 out << "((_ extract " << width - 1 << " 0) ?sum) ";
2360
2361 // MAX
2362 out << "(ite (= ((_ extract " << width << " " << width << ") ?sum) #b0) ";
2363 convert_expr(to_signedbv_type(op_type).largest_expr());
2364
2365 // MIN
2366 convert_expr(to_signedbv_type(op_type).smallest_expr());
2367 out << ")))"; // ite, ite, let
2368 }
2369 else if(op_type.id() == ID_unsignedbv)
2370 {
2371 auto width = to_unsignedbv_type(op_type).get_width();
2372
2373 // compute sum with one extra bit
2374 out << "(let ((?sum (" << (subtract ? "bvsub" : "bvadd");
2375 out << " ((_ zero_extend 1) ";
2376 convert_expr(op0);
2377 out << ")";
2378 out << " ((_ zero_extend 1) ";
2379 convert_expr(op1);
2380 out << "))))"; // zero_extend, bvsub/bvadd
2381
2382 // pick one of MAX, MIN, or the sum
2383 out << "(ite (= ((_ extract " << width << " " << width << ") ?sum) #b0) ";
2384
2385 // no overflow and no underflow case, return the sum
2386 out << " ((_ extract " << width - 1 << " 0) ?sum) ";
2387
2388 // overflow when adding, underflow when subtracting
2389 if(subtract)
2390 convert_expr(to_unsignedbv_type(op_type).smallest_expr());
2391 else
2392 convert_expr(to_unsignedbv_type(op_type).largest_expr());
2393
2394 // MIN
2395 out << "))"; // ite, let
2396 }
2397 else
2399 false,
2400 "saturating_plus/minus on unsupported type",
2401 op_type.id_string());
2402 }
2403 else if(expr.id()==ID_array)
2404 {
2405 defined_expressionst::const_iterator it=defined_expressions.find(expr);
2406 CHECK_RETURN(it != defined_expressions.end());
2407 out << it->second;
2408 }
2409 else if(expr.id()==ID_literal)
2410 {
2411 convert_literal(to_literal_expr(expr).get_literal());
2412 }
2413 else if(expr.id()==ID_forall ||
2414 expr.id()==ID_exists)
2415 {
2416 const quantifier_exprt &quantifier_expr = to_quantifier_expr(expr);
2417
2419 // NOLINTNEXTLINE(readability/throw)
2420 throw "MathSAT does not support quantifiers";
2421
2422 if(quantifier_expr.id() == ID_forall)
2423 out << "(forall ";
2424 else if(quantifier_expr.id() == ID_exists)
2425 out << "(exists ";
2426
2427 out << '(';
2428 bool first = true;
2429 for(const auto &bound : quantifier_expr.variables())
2430 {
2431 if(first)
2432 first = false;
2433 else
2434 out << ' ';
2435 out << '(';
2436 convert_expr(bound);
2437 out << ' ';
2438 convert_type(bound.type());
2439 out << ')';
2440 }
2441 out << ") ";
2442
2443 convert_expr(quantifier_expr.where());
2444
2445 out << ')';
2446 }
2447 else if(
2449 {
2451 }
2452 else if(expr.id()==ID_let)
2453 {
2454 const let_exprt &let_expr=to_let_expr(expr);
2455 const auto &variables = let_expr.variables();
2456 const auto &values = let_expr.values();
2457
2458 out << "(let (";
2459 bool first = true;
2460
2461 for(auto &binding : make_range(variables).zip(values))
2462 {
2463 if(first)
2464 first = false;
2465 else
2466 out << ' ';
2467
2468 out << '(';
2469 convert_expr(binding.first);
2470 out << ' ';
2471 convert_expr(binding.second);
2472 out << ')';
2473 }
2474
2475 out << ") "; // bindings
2476
2477 convert_expr(let_expr.where());
2478 out << ')'; // let
2479 }
2480 else if(expr.id()==ID_constraint_select_one)
2481 {
2483 "smt2_convt::convert_expr: '" + expr.id_string() +
2484 "' is not yet supported");
2485 }
2486 else if(expr.id() == ID_bswap)
2487 {
2488 const bswap_exprt &bswap_expr = to_bswap_expr(expr);
2489
2491 bswap_expr.op().type() == bswap_expr.type(),
2492 "operand of byte swap expression shall have same type as the expression");
2493
2494 // first 'let' the operand
2495 out << "(let ((bswap_op ";
2496 convert_expr(bswap_expr.op());
2497 out << ")) ";
2498
2499 if(
2500 bswap_expr.type().id() == ID_signedbv ||
2501 bswap_expr.type().id() == ID_unsignedbv)
2502 {
2503 const std::size_t width =
2504 to_bitvector_type(bswap_expr.type()).get_width();
2505
2506 const std::size_t bits_per_byte = bswap_expr.get_bits_per_byte();
2507
2508 // width must be multiple of bytes
2510 width % bits_per_byte == 0,
2511 "bit width indicated by type of bswap expression should be a multiple "
2512 "of the number of bits per byte");
2513
2514 const std::size_t bytes = width / bits_per_byte;
2515
2516 if(bytes <= 1)
2517 out << "bswap_op";
2518 else
2519 {
2520 // do a parallel 'let' for each byte
2521 out << "(let (";
2522
2523 for(std::size_t byte = 0; byte < bytes; byte++)
2524 {
2525 if(byte != 0)
2526 out << ' ';
2527 out << "(bswap_byte_" << byte << ' ';
2528 out << "((_ extract " << (byte * bits_per_byte + (bits_per_byte - 1))
2529 << " " << (byte * bits_per_byte) << ") bswap_op)";
2530 out << ')';
2531 }
2532
2533 out << ") ";
2534
2535 // now stitch back together with 'concat'
2536 out << "(concat";
2537
2538 for(std::size_t byte = 0; byte < bytes; byte++)
2539 out << " bswap_byte_" << byte;
2540
2541 out << ')'; // concat
2542 out << ')'; // let bswap_byte_*
2543 }
2544 }
2545 else
2546 UNEXPECTEDCASE("bswap must get bitvector operand");
2547
2548 out << ')'; // let bswap_op
2549 }
2550 else if(expr.id() == ID_popcount)
2551 {
2553 }
2554 else if(expr.id() == ID_count_leading_zeros)
2555 {
2557 }
2558 else if(expr.id() == ID_count_trailing_zeros)
2559 {
2561 }
2562 else if(expr.id() == ID_find_first_set)
2563 {
2565 }
2566 else if(expr.id() == ID_bitreverse)
2567 {
2569 }
2570 else if(expr.id() == ID_zero_extend)
2571 {
2572 convert_expr(to_zero_extend_expr(expr).lower());
2573 }
2574 else if(expr.id() == ID_function_application)
2575 {
2576 const auto &function_application_expr = to_function_application_expr(expr);
2577 // do not use parentheses if there function is a constant
2578 if(function_application_expr.arguments().empty())
2579 {
2580 convert_expr(function_application_expr.function());
2581 }
2582 else
2583 {
2584 out << '(';
2585 convert_expr(function_application_expr.function());
2586 for(auto &op : function_application_expr.arguments())
2587 {
2588 out << ' ';
2589 convert_expr(op);
2590 }
2591 out << ')';
2592 }
2593 }
2594 else if(expr.id() == ID_cond)
2595 {
2596 // use the lowering
2597 convert_expr(to_cond_expr(expr).lower());
2598 }
2599 else
2601 false,
2602 "smt2_convt::convert_expr should not be applied to unsupported "
2603 "expression",
2604 expr.id_string());
2605}
2606
2608{
2609 const exprt &src = expr.op();
2610
2611 typet dest_type = expr.type();
2612 if(dest_type.id()==ID_c_enum_tag)
2613 dest_type=ns.follow_tag(to_c_enum_tag_type(dest_type));
2614
2615 typet src_type = src.type();
2616 if(src_type.id()==ID_c_enum_tag)
2617 src_type=ns.follow_tag(to_c_enum_tag_type(src_type));
2618
2619 if(dest_type.id()==ID_bool)
2620 {
2621 // this is comparison with zero
2622 if(src_type.id()==ID_signedbv ||
2623 src_type.id()==ID_unsignedbv ||
2624 src_type.id()==ID_c_bool ||
2625 src_type.id()==ID_fixedbv ||
2626 src_type.id()==ID_pointer ||
2627 src_type.id()==ID_integer)
2628 {
2629 out << "(not (= ";
2630 convert_expr(src);
2631 out << " ";
2632 convert_expr(from_integer(0, src_type));
2633 out << "))";
2634 }
2635 else if(src_type.id()==ID_floatbv)
2636 {
2637 if(use_FPA_theory)
2638 {
2639 out << "(not (fp.isZero ";
2640 convert_expr(src);
2641 out << "))";
2642 }
2643 else
2644 convert_floatbv(expr);
2645 }
2646 else
2647 {
2648 UNEXPECTEDCASE("TODO typecast1 "+src_type.id_string()+" -> bool");
2649 }
2650 }
2651 else if(dest_type.id()==ID_c_bool)
2652 {
2653 std::size_t to_width=boolbv_width(dest_type);
2654 out << "(ite ";
2655 out << "(not (= ";
2656 convert_expr(src);
2657 out << " ";
2658 convert_expr(from_integer(0, src_type));
2659 out << "))"; // not, =
2660 out << " (_ bv1 " << to_width << ")";
2661 out << " (_ bv0 " << to_width << ")";
2662 out << ")"; // ite
2663 }
2664 else if(dest_type.id()==ID_signedbv ||
2665 dest_type.id()==ID_unsignedbv ||
2666 dest_type.id()==ID_c_enum ||
2667 dest_type.id()==ID_bv)
2668 {
2669 std::size_t to_width=boolbv_width(dest_type);
2670
2671 if(src_type.id()==ID_signedbv || // from signedbv
2672 src_type.id()==ID_unsignedbv || // from unsigedbv
2673 src_type.id()==ID_c_bool ||
2674 src_type.id()==ID_c_enum ||
2675 src_type.id()==ID_bv)
2676 {
2677 std::size_t from_width=boolbv_width(src_type);
2678
2679 if(from_width==to_width)
2680 convert_expr(src); // ignore
2681 else if(from_width<to_width) // extend
2682 {
2683 if(src_type.id()==ID_signedbv)
2684 out << "((_ sign_extend ";
2685 else
2686 out << "((_ zero_extend ";
2687
2688 out << (to_width-from_width)
2689 << ") "; // ind
2690 convert_expr(src);
2691 out << ")";
2692 }
2693 else // chop off extra bits
2694 {
2695 out << "((_ extract " << (to_width-1) << " 0) ";
2696 convert_expr(src);
2697 out << ")";
2698 }
2699 }
2700 else if(src_type.id()==ID_fixedbv) // from fixedbv to int
2701 {
2702 const fixedbv_typet &fixedbv_type=to_fixedbv_type(src_type);
2703
2704 std::size_t from_width=fixedbv_type.get_width();
2705 std::size_t from_integer_bits=fixedbv_type.get_integer_bits();
2706 std::size_t from_fraction_bits=fixedbv_type.get_fraction_bits();
2707
2708 // we might need to round up in case of negative numbers
2709 // e.g., (int)(-1.00001)==1
2710
2711 out << "(let ((?tcop ";
2712 convert_expr(src);
2713 out << ")) ";
2714
2715 out << "(bvadd ";
2716
2717 if(to_width>from_integer_bits)
2718 {
2719 out << "((_ sign_extend "
2720 << (to_width-from_integer_bits) << ") ";
2721 out << "((_ extract " << (from_width-1) << " "
2722 << from_fraction_bits << ") ";
2723 convert_expr(src);
2724 out << "))";
2725 }
2726 else
2727 {
2728 out << "((_ extract " << (from_fraction_bits+to_width-1)
2729 << " " << from_fraction_bits << ") ";
2730 convert_expr(src);
2731 out << ")";
2732 }
2733
2734 out << " (ite (and ";
2735
2736 // some fraction bit is not zero
2737 out << "(not (= ((_ extract " << (from_fraction_bits-1) << " 0) ?tcop) "
2738 "(_ bv0 " << from_fraction_bits << ")))";
2739
2740 // number negative
2741 out << " (= ((_ extract " << (from_width-1) << " " << (from_width-1)
2742 << ") ?tcop) #b1)";
2743
2744 out << ")"; // and
2745
2746 out << " (_ bv1 " << to_width << ") (_ bv0 " << to_width << "))"; // ite
2747 out << ")"; // bvadd
2748 out << ")"; // let
2749 }
2750 else if(src_type.id()==ID_floatbv) // from floatbv to int
2751 {
2752 if(dest_type.id()==ID_bv)
2753 {
2754 // this is _NOT_ a semantic conversion, but bit-wise
2755
2756 if(use_FPA_theory)
2757 {
2758 defined_expressionst::const_iterator it =
2759 defined_expressions.find(expr);
2760 CHECK_RETURN(it != defined_expressions.end());
2761 out << it->second;
2762 }
2763 else
2764 {
2765 // straight-forward if width matches
2766 convert_expr(src);
2767 }
2768 }
2769 else if(dest_type.id()==ID_signedbv)
2770 {
2771 // this should be floatbv_typecast, not typecast
2773 "typecast unexpected "+src_type.id_string()+" -> "+
2774 dest_type.id_string());
2775 }
2776 else if(dest_type.id()==ID_unsignedbv)
2777 {
2778 // this should be floatbv_typecast, not typecast
2780 "typecast unexpected "+src_type.id_string()+" -> "+
2781 dest_type.id_string());
2782 }
2783 }
2784 else if(src_type.id()==ID_bool) // from boolean to int
2785 {
2786 out << "(ite ";
2787 convert_expr(src);
2788
2789 if(dest_type.id()==ID_fixedbv)
2790 {
2791 fixedbv_spect spec(to_fixedbv_type(dest_type));
2792 out << " (concat (_ bv1 "
2793 << spec.integer_bits << ") " <<
2794 "(_ bv0 " << spec.get_fraction_bits() << ")) " <<
2795 "(_ bv0 " << spec.width << ")";
2796 }
2797 else
2798 {
2799 out << " (_ bv1 " << to_width << ")";
2800 out << " (_ bv0 " << to_width << ")";
2801 }
2802
2803 out << ")";
2804 }
2805 else if(src_type.id()==ID_pointer) // from pointer to int
2806 {
2807 std::size_t from_width=boolbv_width(src_type);
2808
2809 if(from_width<to_width) // extend
2810 {
2811 out << "((_ sign_extend ";
2812 out << (to_width-from_width)
2813 << ") ";
2814 convert_expr(src);
2815 out << ")";
2816 }
2817 else // chop off extra bits
2818 {
2819 out << "((_ extract " << (to_width-1) << " 0) ";
2820 convert_expr(src);
2821 out << ")";
2822 }
2823 }
2824 else if(src_type.id()==ID_integer) // from integer to bit-vector
2825 {
2826 // must be constant
2827 if(src.is_constant())
2828 {
2830 out << "(_ bv" << i << " " << to_width << ")";
2831 }
2832 else
2833 SMT2_TODO("can't convert non-constant integer to bitvector");
2834 }
2835 else if(
2836 src_type.id() == ID_struct ||
2837 src_type.id() == ID_struct_tag) // flatten a struct to a bit-vector
2838 {
2839 if(use_datatypes)
2840 {
2841 INVARIANT(
2842 boolbv_width(src_type) == boolbv_width(dest_type),
2843 "bit vector with of source and destination type shall be equal");
2844 flatten2bv(src);
2845 }
2846 else
2847 {
2848 INVARIANT(
2849 boolbv_width(src_type) == boolbv_width(dest_type),
2850 "bit vector with of source and destination type shall be equal");
2851 convert_expr(src); // nothing else to do!
2852 }
2853 }
2854 else if(
2855 src_type.id() == ID_union ||
2856 src_type.id() == ID_union_tag) // flatten a union
2857 {
2858 INVARIANT(
2859 boolbv_width(src_type) == boolbv_width(dest_type),
2860 "bit vector with of source and destination type shall be equal");
2861 convert_expr(src); // nothing else to do!
2862 }
2863 else if(src_type.id()==ID_c_bit_field)
2864 {
2865 std::size_t from_width=boolbv_width(src_type);
2866
2867 if(from_width==to_width)
2868 convert_expr(src); // ignore
2869 else
2870 {
2872 typecast_exprt tmp(typecast_exprt(src, t), dest_type);
2873 convert_typecast(tmp);
2874 }
2875 }
2876 else
2877 {
2878 std::ostringstream e_str;
2879 e_str << src_type.id() << " -> " << dest_type.id()
2880 << " src == " << format(src);
2881 UNEXPECTEDCASE("TODO typecast2 " + e_str.str());
2882 }
2883 }
2884 else if(dest_type.id()==ID_fixedbv) // to fixedbv
2885 {
2886 const fixedbv_typet &fixedbv_type=to_fixedbv_type(dest_type);
2887 std::size_t to_fraction_bits=fixedbv_type.get_fraction_bits();
2888 std::size_t to_integer_bits=fixedbv_type.get_integer_bits();
2889
2890 if(src_type.id()==ID_unsignedbv ||
2891 src_type.id()==ID_signedbv ||
2892 src_type.id()==ID_c_enum)
2893 {
2894 // integer to fixedbv
2895
2896 std::size_t from_width=to_bitvector_type(src_type).get_width();
2897 out << "(concat ";
2898
2899 if(from_width==to_integer_bits)
2900 convert_expr(src);
2901 else if(from_width>to_integer_bits)
2902 {
2903 // too many integer bits
2904 out << "((_ extract " << (to_integer_bits-1) << " 0) ";
2905 convert_expr(src);
2906 out << ")";
2907 }
2908 else
2909 {
2910 // too few integer bits
2911 INVARIANT(
2912 from_width < to_integer_bits,
2913 "from_width should be smaller than to_integer_bits as other case "
2914 "have been handled above");
2915 if(dest_type.id()==ID_unsignedbv)
2916 {
2917 out << "(_ zero_extend "
2918 << (to_integer_bits-from_width) << ") ";
2919 convert_expr(src);
2920 out << ")";
2921 }
2922 else
2923 {
2924 out << "((_ sign_extend "
2925 << (to_integer_bits-from_width) << ") ";
2926 convert_expr(src);
2927 out << ")";
2928 }
2929 }
2930
2931 out << "(_ bv0 " << to_fraction_bits << ")";
2932 out << ")"; // concat
2933 }
2934 else if(src_type.id()==ID_bool) // bool to fixedbv
2935 {
2936 out << "(concat (concat"
2937 << " (_ bv0 " << (to_integer_bits-1) << ") ";
2938 flatten2bv(src); // produces #b0 or #b1
2939 out << ") (_ bv0 "
2940 << to_fraction_bits
2941 << "))";
2942 }
2943 else if(src_type.id()==ID_fixedbv) // fixedbv to fixedbv
2944 {
2945 const fixedbv_typet &from_fixedbv_type=to_fixedbv_type(src_type);
2946 std::size_t from_fraction_bits=from_fixedbv_type.get_fraction_bits();
2947 std::size_t from_integer_bits=from_fixedbv_type.get_integer_bits();
2948 std::size_t from_width=from_fixedbv_type.get_width();
2949
2950 out << "(let ((?tcop ";
2951 convert_expr(src);
2952 out << ")) ";
2953
2954 out << "(concat ";
2955
2956 if(to_integer_bits<=from_integer_bits)
2957 {
2958 out << "((_ extract "
2959 << (from_fraction_bits+to_integer_bits-1) << " "
2960 << from_fraction_bits
2961 << ") ?tcop)";
2962 }
2963 else
2964 {
2965 INVARIANT(
2966 to_integer_bits > from_integer_bits,
2967 "to_integer_bits should be greater than from_integer_bits as the"
2968 "other case has been handled above");
2969 out << "((_ sign_extend "
2970 << (to_integer_bits-from_integer_bits)
2971 << ") ((_ extract "
2972 << (from_width-1) << " "
2973 << from_fraction_bits
2974 << ") ?tcop))";
2975 }
2976
2977 out << " ";
2978
2979 if(to_fraction_bits<=from_fraction_bits)
2980 {
2981 out << "((_ extract "
2982 << (from_fraction_bits-1) << " "
2983 << (from_fraction_bits-to_fraction_bits)
2984 << ") ?tcop)";
2985 }
2986 else
2987 {
2988 INVARIANT(
2989 to_fraction_bits > from_fraction_bits,
2990 "to_fraction_bits should be greater than from_fraction_bits as the"
2991 "other case has been handled above");
2992 out << "(concat ((_ extract "
2993 << (from_fraction_bits-1) << " 0) ";
2994 convert_expr(src);
2995 out << ")"
2996 << " (_ bv0 " << to_fraction_bits-from_fraction_bits
2997 << "))";
2998 }
2999
3000 out << "))"; // concat, let
3001 }
3002 else
3003 UNEXPECTEDCASE("unexpected typecast to fixedbv");
3004 }
3005 else if(dest_type.id()==ID_pointer)
3006 {
3007 std::size_t to_width=boolbv_width(dest_type);
3008
3009 if(src_type.id()==ID_pointer) // pointer to pointer
3010 {
3011 // this just passes through
3012 convert_expr(src);
3013 }
3014 else if(
3015 src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv ||
3016 src_type.id() == ID_bv)
3017 {
3018 // integer to pointer
3019
3020 std::size_t from_width=boolbv_width(src_type);
3021
3022 if(from_width==to_width)
3023 convert_expr(src);
3024 else if(from_width<to_width)
3025 {
3026 out << "((_ sign_extend "
3027 << (to_width-from_width)
3028 << ") ";
3029 convert_expr(src);
3030 out << ")"; // sign_extend
3031 }
3032 else // from_width>to_width
3033 {
3034 out << "((_ extract " << to_width << " 0) ";
3035 convert_expr(src);
3036 out << ")"; // extract
3037 }
3038 }
3039 else
3040 UNEXPECTEDCASE("TODO typecast3 "+src_type.id_string()+" -> pointer");
3041 }
3042 else if(dest_type.id()==ID_range)
3043 {
3044 auto &dest_range_type = to_range_type(dest_type);
3045 const auto dest_size =
3046 dest_range_type.get_to() - dest_range_type.get_from() + 1;
3047 const auto dest_width = address_bits(dest_size);
3048 if(src_type.id() == ID_range)
3049 {
3050 auto &src_range_type = to_range_type(src_type);
3051 const auto src_size =
3052 src_range_type.get_to() - src_range_type.get_from() + 1;
3053 const auto src_width = address_bits(src_size);
3054 if(src_width < dest_width)
3055 {
3056 out << "((_ zero_extend " << dest_width - src_width << ") ";
3057 convert_expr(src);
3058 out << ')'; // zero_extend
3059 }
3060 else if(src_width > dest_width)
3061 {
3062 out << "((_ extract " << dest_width - 1 << " 0) ";
3063 convert_expr(src);
3064 out << ')'; // extract
3065 }
3066 else // src_width == dest_width
3067 {
3068 convert_expr(src);
3069 }
3070 }
3071 else
3072 SMT2_TODO("typecast from " + src_type.id_string() + " to range");
3073 }
3074 else if(dest_type.id()==ID_floatbv)
3075 {
3076 // Typecast from integer to floating-point should have be been
3077 // converted to ID_floatbv_typecast during symbolic execution,
3078 // adding the rounding mode. See
3079 // smt2_convt::convert_floatbv_typecast.
3080 // The exception is bool and c_bool to float.
3081 const auto &dest_floatbv_type = to_floatbv_type(dest_type);
3082
3083 if(src_type.id()==ID_bool)
3084 {
3085 out << "(ite ";
3086 convert_expr(src);
3087 out << ' ';
3088 convert_constant(ieee_floatt::one(dest_floatbv_type).to_expr());
3089 out << ' ';
3090 convert_constant(ieee_floatt::zero(dest_floatbv_type).to_expr());
3091 out << ')';
3092 }
3093 else if(src_type.id()==ID_c_bool)
3094 {
3095 // turn into proper bool
3096 const typecast_exprt tmp(src, bool_typet());
3097 convert_typecast(typecast_exprt(tmp, dest_type));
3098 }
3099 else if(src_type.id() == ID_bv)
3100 {
3101 if(to_bv_type(src_type).get_width() != dest_floatbv_type.get_width())
3102 {
3103 UNEXPECTEDCASE("Typecast bv -> float with wrong width");
3104 }
3105
3106 if(use_FPA_theory)
3107 {
3108 out << "((_ to_fp " << dest_floatbv_type.get_e() << " "
3109 << dest_floatbv_type.get_f() + 1 << ") ";
3110 convert_expr(src);
3111 out << ')';
3112 }
3113 else
3114 convert_expr(src);
3115 }
3116 else
3117 UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
3118 }
3119 else if(dest_type.id()==ID_integer)
3120 {
3121 if(src_type.id()==ID_bool)
3122 {
3123 out << "(ite ";
3124 convert_expr(src);
3125 out <<" 1 0)";
3126 }
3127 else
3128 UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer");
3129 }
3130 else if(dest_type.id()==ID_c_bit_field)
3131 {
3132 std::size_t from_width=boolbv_width(src_type);
3133 std::size_t to_width=boolbv_width(dest_type);
3134
3135 if(from_width==to_width)
3136 convert_expr(src); // ignore
3137 else
3138 {
3140 typecast_exprt tmp(typecast_exprt(src, t), dest_type);
3141 convert_typecast(tmp);
3142 }
3143 }
3144 else
3146 "TODO typecast8 "+src_type.id_string()+" -> "+dest_type.id_string());
3147}
3148
3150{
3151 const exprt &src=expr.op();
3152 // const exprt &rounding_mode=expr.rounding_mode();
3153 const typet &src_type=src.type();
3154 const typet &dest_type=expr.type();
3155
3156 if(dest_type.id()==ID_floatbv)
3157 {
3158 if(src_type.id()==ID_floatbv)
3159 {
3160 // float to float
3161
3162 /* ISO 9899:1999
3163 * 6.3.1.5 Real floating types
3164 * 1 When a float is promoted to double or long double, or a
3165 * double is promoted to long double, its value is unchanged.
3166 *
3167 * 2 When a double is demoted to float, a long double is
3168 * demoted to double or float, or a value being represented in
3169 * greater precision and range than required by its semantic
3170 * type (see 6.3.1.8) is explicitly converted to its semantic
3171 * type, if the value being converted can be represented
3172 * exactly in the new type, it is unchanged. If the value
3173 * being converted is in the range of values that can be
3174 * represented but cannot be represented exactly, the result
3175 * is either the nearest higher or nearest lower representable
3176 * value, chosen in an implementation-defined manner. If the
3177 * value being converted is outside the range of values that
3178 * can be represented, the behavior is undefined.
3179 */
3180
3181 const floatbv_typet &dst=to_floatbv_type(dest_type);
3182
3183 if(use_FPA_theory)
3184 {
3185 out << "((_ to_fp " << dst.get_e() << " "
3186 << dst.get_f() + 1 << ") ";
3188 out << " ";
3189 convert_expr(src);
3190 out << ")";
3191 }
3192 else
3193 convert_floatbv(expr);
3194 }
3195 else if(src_type.id()==ID_unsignedbv)
3196 {
3197 // unsigned to float
3198
3199 /* ISO 9899:1999
3200 * 6.3.1.4 Real floating and integer
3201 * 2 When a value of integer type is converted to a real
3202 * floating type, if the value being converted can be
3203 * represented exactly in the new type, it is unchanged. If the
3204 * value being converted is in the range of values that can be
3205 * represented but cannot be represented exactly, the result is
3206 * either the nearest higher or nearest lower representable
3207 * value, chosen in an implementation-defined manner. If the
3208 * value being converted is outside the range of values that can
3209 * be represented, the behavior is undefined.
3210 */
3211
3212 const floatbv_typet &dst=to_floatbv_type(dest_type);
3213
3214 if(use_FPA_theory)
3215 {
3216 out << "((_ to_fp_unsigned " << dst.get_e() << " "
3217 << dst.get_f() + 1 << ") ";
3219 out << " ";
3220 convert_expr(src);
3221 out << ")";
3222 }
3223 else
3224 convert_floatbv(expr);
3225 }
3226 else if(src_type.id()==ID_signedbv)
3227 {
3228 // signed to float
3229
3230 const floatbv_typet &dst=to_floatbv_type(dest_type);
3231
3232 if(use_FPA_theory)
3233 {
3234 out << "((_ to_fp " << dst.get_e() << " "
3235 << dst.get_f() + 1 << ") ";
3237 out << " ";
3238 convert_expr(src);
3239 out << ")";
3240 }
3241 else
3242 convert_floatbv(expr);
3243 }
3244 else if(src_type.id()==ID_c_enum_tag)
3245 {
3246 // enum to float
3247
3248 // We first convert to 'underlying type'
3249 floatbv_typecast_exprt tmp=expr;
3250 tmp.op() = typecast_exprt(
3251 src, ns.follow_tag(to_c_enum_tag_type(src_type)).underlying_type());
3253 }
3254 else
3256 "TODO typecast11 "+src_type.id_string()+" -> "+dest_type.id_string());
3257 }
3258 else if(dest_type.id()==ID_signedbv)
3259 {
3260 if(use_FPA_theory)
3261 {
3262 std::size_t dest_width=to_signedbv_type(dest_type).get_width();
3263 out << "((_ fp.to_sbv " << dest_width << ") ";
3265 out << " ";
3266 convert_expr(src);
3267 out << ")";
3268 }
3269 else
3270 convert_floatbv(expr);
3271 }
3272 else if(dest_type.id()==ID_unsignedbv)
3273 {
3274 if(use_FPA_theory)
3275 {
3276 std::size_t dest_width=to_unsignedbv_type(dest_type).get_width();
3277 out << "((_ fp.to_ubv " << dest_width << ") ";
3279 out << " ";
3280 convert_expr(src);
3281 out << ")";
3282 }
3283 else
3284 convert_floatbv(expr);
3285 }
3286 else
3287 {
3289 "TODO typecast12 "+src_type.id_string()+" -> "+dest_type.id_string());
3290 }
3291}
3292
3295{
3296 PRECONDITION(expr.type().id() == ID_floatbv);
3297
3298 if(use_FPA_theory)
3299 {
3300 out << "(fp.roundToIntegral ";
3302 out << ' ';
3303 convert_expr(expr.op());
3304 out << ")";
3305 }
3306 else
3307 UNEXPECTEDCASE("TODO floatbv_round_to_integral without FPA");
3308}
3309
3311{
3312 const struct_typet &struct_type =
3313 expr.type().id() == ID_struct_tag
3314 ? ns.follow_tag(to_struct_tag_type(expr.type()))
3315 : to_struct_type(expr.type());
3316
3317 const struct_typet::componentst &components=
3318 struct_type.components();
3319
3321 components.size() == expr.operands().size(),
3322 "number of struct components as indicated by the struct type shall be equal"
3323 "to the number of operands of the struct expression");
3324
3325 DATA_INVARIANT(!components.empty(), "struct shall have struct components");
3326
3327 if(use_datatypes)
3328 {
3329 const std::string &smt_typename = datatype_map.at(struct_type);
3330
3331 // use the constructor for the Z3 datatype
3332 out << "(mk-" << smt_typename;
3333
3334 std::size_t i=0;
3335 for(struct_typet::componentst::const_iterator
3336 it=components.begin();
3337 it!=components.end();
3338 it++, i++)
3339 {
3340 if(is_zero_width(it->type(), ns))
3341 continue;
3342 out << " ";
3343 convert_expr(expr.operands()[i]);
3344 }
3345
3346 out << ")";
3347 }
3348 else
3349 {
3350 auto convert_operand = [this](const exprt &op) {
3351 // may need to flatten array-theory arrays in there
3352 if(op.type().id() == ID_array && use_array_theory(op))
3353 flatten_array(op);
3354 else if(op.type().id() == ID_bool)
3355 flatten2bv(op);
3356 else
3357 convert_expr(op);
3358 };
3359
3360 // SMT-LIB 2 concat is binary only
3361 std::size_t n_concat = 0;
3362 for(std::size_t i = components.size(); i > 1; i--)
3363 {
3364 if(is_zero_width(components[i - 1].type(), ns))
3365 continue;
3366 else if(i > 2 || !is_zero_width(components[0].type(), ns))
3367 {
3368 ++n_concat;
3369 out << "(concat ";
3370 }
3371
3372 convert_operand(expr.operands()[i - 1]);
3373
3374 out << " ";
3375 }
3376
3377 if(!is_zero_width(components[0].type(), ns))
3378 convert_operand(expr.op0());
3379
3380 out << std::string(n_concat, ')');
3381 }
3382}
3383
3386{
3387 const array_typet &array_type = to_array_type(expr.type());
3388 const auto &size_expr = array_type.size();
3389 PRECONDITION(size_expr.is_constant());
3390
3392 CHECK_RETURN_WITH_DIAGNOSTICS(size != 0, "can't convert zero-sized array");
3393
3394 out << "(let ((?far ";
3395 convert_expr(expr);
3396 out << ")) ";
3397
3398 for(mp_integer i=size; i!=0; --i)
3399 {
3400 if(i!=1)
3401 out << "(concat ";
3402 out << "(select ?far ";
3403 convert_expr(from_integer(i - 1, array_type.index_type()));
3404 out << ")";
3405 if(i!=1)
3406 out << " ";
3407 }
3408
3409 // close the many parentheses
3410 for(mp_integer i=size; i>1; --i)
3411 out << ")";
3412
3413 out << ")"; // let
3414}
3415
3417{
3418 const exprt &op=expr.op();
3419
3420 std::size_t total_width = boolbv_width(expr.type());
3421
3422 std::size_t member_width=boolbv_width(op.type());
3423
3424 if(total_width==member_width)
3425 {
3426 flatten2bv(op);
3427 }
3428 else
3429 {
3430 // we will pad with zeros, but non-det would be better
3431 INVARIANT(
3432 total_width > member_width,
3433 "total_width should be greater than member_width as member_width can be"
3434 "at most as large as total_width and the other case has been handled "
3435 "above");
3436 out << "(concat ";
3437 out << "(_ bv0 "
3438 << (total_width-member_width) << ") ";
3439 flatten2bv(op);
3440 out << ")";
3441 }
3442}
3443
3445{
3446 const typet &expr_type=expr.type();
3447
3448 if(expr_type.id()==ID_unsignedbv ||
3449 expr_type.id()==ID_signedbv ||
3450 expr_type.id()==ID_bv ||
3451 expr_type.id()==ID_c_enum ||
3452 expr_type.id()==ID_c_enum_tag ||
3453 expr_type.id()==ID_c_bool ||
3454 expr_type.id()==ID_c_bit_field)
3455 {
3456 const std::size_t width = boolbv_width(expr_type);
3457
3458 const mp_integer value = bvrep2integer(expr.get_value(), width, false);
3459
3460 out << "(_ bv" << value
3461 << " " << width << ")";
3462 }
3463 else if(expr_type.id()==ID_fixedbv)
3464 {
3465 const fixedbv_spect spec(to_fixedbv_type(expr_type));
3466
3467 const mp_integer v = bvrep2integer(expr.get_value(), spec.width, false);
3468
3469 out << "(_ bv" << v << " " << spec.width << ")";
3470 }
3471 else if(expr_type.id()==ID_floatbv)
3472 {
3473 const floatbv_typet &floatbv_type=
3474 to_floatbv_type(expr_type);
3475
3476 if(use_FPA_theory)
3477 {
3478 /* CBMC stores floating point literals in the most
3479 computationally useful form; biased exponents and
3480 significands including the hidden bit. Thus some encoding
3481 is needed to get to IEEE-754 style representations. */
3482
3484 size_t e=floatbv_type.get_e();
3485 size_t f=floatbv_type.get_f()+1;
3486
3487 /* Should be sufficient, but not currently supported by mathsat */
3488 #if 0
3489 mp_integer binary = v.pack();
3490
3491 out << "((_ to_fp " << e << " " << f << ")"
3492 << " #b" << integer2binary(v.pack(), v.spec.width()) << ")";
3493 #endif
3494
3495 if(v.is_NaN())
3496 {
3497 out << "(_ NaN " << e << " " << f << ")";
3498 }
3499 else if(v.is_infinity())
3500 {
3501 if(v.get_sign())
3502 out << "(_ -oo " << e << " " << f << ")";
3503 else
3504 out << "(_ +oo " << e << " " << f << ")";
3505 }
3506 else
3507 {
3508 // Zero, normal or subnormal
3509
3510 mp_integer binary = v.pack();
3511 std::string binaryString(integer2binary(v.pack(), v.spec.width()));
3512
3513 out << "(fp "
3514 << "#b" << binaryString.substr(0, 1) << " "
3515 << "#b" << binaryString.substr(1, e) << " "
3516 << "#b" << binaryString.substr(1+e, f-1) << ")";
3517 }
3518 }
3519 else
3520 {
3521 // produce corresponding bit-vector
3522 const ieee_float_spect spec(floatbv_type);
3523 const mp_integer v = bvrep2integer(expr.get_value(), spec.width(), false);
3524 out << "(_ bv" << v << " " << spec.width() << ")";
3525 }
3526 }
3527 else if(expr_type.id()==ID_pointer)
3528 {
3529 if(expr.is_null_pointer())
3530 {
3531 out << "(_ bv0 " << boolbv_width(expr_type)
3532 << ")";
3533 }
3534 else
3535 {
3536 // just treat the pointer as a bit vector
3537 const std::size_t width = boolbv_width(expr_type);
3538
3539 const mp_integer value = bvrep2integer(expr.get_value(), width, false);
3540
3541 out << "(_ bv" << value << " " << width << ")";
3542 }
3543 }
3544 else if(expr_type.id()==ID_bool)
3545 {
3546 if(expr.is_true())
3547 out << "true";
3548 else if(expr.is_false())
3549 out << "false";
3550 else
3551 UNEXPECTEDCASE("unknown Boolean constant");
3552 }
3553 else if(expr_type.id()==ID_array)
3554 {
3555 defined_expressionst::const_iterator it=defined_expressions.find(expr);
3556 CHECK_RETURN(it != defined_expressions.end());
3557 out << it->second;
3558 }
3559 else if(expr_type.id()==ID_rational)
3560 {
3561 std::string value=id2string(expr.get_value());
3562 const bool negative = has_prefix(value, "-");
3563
3564 if(negative)
3565 out << "(- ";
3566
3567 size_t pos=value.find("/");
3568
3569 if(pos==std::string::npos)
3570 out << value << ".0";
3571 else
3572 {
3573 out << "(/ " << value.substr(0, pos) << ".0 "
3574 << value.substr(pos+1) << ".0)";
3575 }
3576
3577 if(negative)
3578 out << ')';
3579 }
3580 else if(expr_type.id()==ID_integer)
3581 {
3582 const auto value = id2string(expr.get_value());
3583
3584 // SMT2 has no negative integer literals
3585 if(has_prefix(value, "-"))
3586 out << "(- " << value.substr(1, std::string::npos) << ')';
3587 else
3588 out << value;
3589 }
3590 else if(expr_type.id() == ID_range)
3591 {
3592 auto &range_type = to_range_type(expr_type);
3593 const auto size = range_type.get_to() - range_type.get_from() + 1;
3594 const auto width = address_bits(size);
3595 const auto value_int = numeric_cast_v<mp_integer>(expr);
3596 out << "(_ bv" << (value_int - range_type.get_from()) << " " << width
3597 << ")";
3598 }
3599 else
3600 UNEXPECTEDCASE("unknown constant: "+expr_type.id_string());
3601}
3602
3604{
3605 if(expr.type().id() == ID_integer)
3606 {
3607 out << "(mod ";
3608 convert_expr(expr.op0());
3609 out << ' ';
3610 convert_expr(expr.op1());
3611 out << ')';
3612 }
3613 else
3615 "unsupported type for euclidean_mod: " + expr.type().id_string());
3616}
3617
3619{
3620 if(expr.type().id()==ID_unsignedbv ||
3621 expr.type().id()==ID_signedbv)
3622 {
3623 if(expr.type().id()==ID_unsignedbv)
3624 out << "(bvurem ";
3625 else
3626 out << "(bvsrem ";
3627
3628 convert_expr(expr.op0());
3629 out << " ";
3630 convert_expr(expr.op1());
3631 out << ")";
3632 }
3633 else
3634 UNEXPECTEDCASE("unsupported type for mod: "+expr.type().id_string());
3635}
3636
3638{
3639 std::vector<mp_integer> dynamic_objects;
3640 pointer_logic.get_dynamic_objects(dynamic_objects);
3641
3642 if(dynamic_objects.empty())
3643 out << "false";
3644 else
3645 {
3646 std::size_t pointer_width = boolbv_width(expr.op().type());
3647
3648 out << "(let ((?obj ((_ extract "
3649 << pointer_width-1 << " "
3650 << pointer_width-config.bv_encoding.object_bits << ") ";
3651 convert_expr(expr.op());
3652 out << "))) ";
3653
3654 if(dynamic_objects.size()==1)
3655 {
3656 out << "(= (_ bv" << dynamic_objects.front()
3657 << " " << config.bv_encoding.object_bits << ") ?obj)";
3658 }
3659 else
3660 {
3661 out << "(or";
3662
3663 for(const auto &object : dynamic_objects)
3664 out << " (= (_ bv" << object
3665 << " " << config.bv_encoding.object_bits << ") ?obj)";
3666
3667 out << ")"; // or
3668 }
3669
3670 out << ")"; // let
3671 }
3672}
3673
3675{
3676 const typet &op_type=expr.op0().type();
3677
3678 if(
3679 op_type.id() == ID_unsignedbv || op_type.id() == ID_bv ||
3680 op_type.id() == ID_range)
3681 {
3682 // The range type is encoded in binary
3683 out << "(";
3684 if(expr.id()==ID_le)
3685 out << "bvule";
3686 else if(expr.id()==ID_lt)
3687 out << "bvult";
3688 else if(expr.id()==ID_ge)
3689 out << "bvuge";
3690 else if(expr.id()==ID_gt)
3691 out << "bvugt";
3692
3693 out << " ";
3694 convert_expr(expr.op0());
3695 out << " ";
3696 convert_expr(expr.op1());
3697 out << ")";
3698 }
3699 else if(op_type.id()==ID_signedbv ||
3700 op_type.id()==ID_fixedbv)
3701 {
3702 out << "(";
3703 if(expr.id()==ID_le)
3704 out << "bvsle";
3705 else if(expr.id()==ID_lt)
3706 out << "bvslt";
3707 else if(expr.id()==ID_ge)
3708 out << "bvsge";
3709 else if(expr.id()==ID_gt)
3710 out << "bvsgt";
3711
3712 out << " ";
3713 convert_expr(expr.op0());
3714 out << " ";
3715 convert_expr(expr.op1());
3716 out << ")";
3717 }
3718 else if(op_type.id()==ID_floatbv)
3719 {
3720 if(use_FPA_theory)
3721 {
3722 out << "(";
3723 if(expr.id()==ID_le)
3724 out << "fp.leq";
3725 else if(expr.id()==ID_lt)
3726 out << "fp.lt";
3727 else if(expr.id()==ID_ge)
3728 out << "fp.geq";
3729 else if(expr.id()==ID_gt)
3730 out << "fp.gt";
3731
3732 out << " ";
3733 convert_expr(expr.op0());
3734 out << " ";
3735 convert_expr(expr.op1());
3736 out << ")";
3737 }
3738 else
3739 convert_floatbv(expr);
3740 }
3741 else if(op_type.id()==ID_rational ||
3742 op_type.id()==ID_integer)
3743 {
3744 out << "(";
3745 out << expr.id();
3746
3747 out << " ";
3748 convert_expr(expr.op0());
3749 out << " ";
3750 convert_expr(expr.op1());
3751 out << ")";
3752 }
3753 else if(op_type.id() == ID_pointer)
3754 {
3755 const exprt same_object = ::same_object(expr.op0(), expr.op1());
3756
3757 out << "(and ";
3759
3760 out << " (";
3761 if(expr.id() == ID_le)
3762 out << "bvsle";
3763 else if(expr.id() == ID_lt)
3764 out << "bvslt";
3765 else if(expr.id() == ID_ge)
3766 out << "bvsge";
3767 else if(expr.id() == ID_gt)
3768 out << "bvsgt";
3769
3770 out << ' ';
3772 out << ' ';
3774 out << ')';
3775
3776 out << ')';
3777 }
3778 else
3780 "unsupported type for "+expr.id_string()+": "+op_type.id_string());
3781}
3782
3784{
3785 if(
3786 expr.type().id() == ID_rational || expr.type().id() == ID_integer ||
3787 expr.type().id() == ID_real)
3788 {
3789 // these are multi-ary in SMT-LIB2
3790 out << "(+";
3791
3792 for(const auto &op : expr.operands())
3793 {
3794 out << ' ';
3795 convert_expr(op);
3796 }
3797
3798 out << ')';
3799 }
3800 else if(
3801 expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv ||
3802 expr.type().id() == ID_fixedbv)
3803 {
3804 // These could be chained, i.e., need not be binary,
3805 // but at least MathSat doesn't like that.
3806 if(expr.operands().size() == 2)
3807 {
3808 out << "(bvadd ";
3809 convert_expr(expr.op0());
3810 out << " ";
3811 convert_expr(expr.op1());
3812 out << ")";
3813 }
3814 else
3815 {
3817 }
3818 }
3819 else if(expr.type().id() == ID_range)
3820 {
3821 auto &range_type = to_range_type(expr.type());
3822
3823 // These could be chained, i.e., need not be binary,
3824 // but at least MathSat doesn't like that.
3825 if(expr.operands().size() == 2)
3826 {
3827 // add: lhs + from + rhs + from - from = lhs + rhs + from
3828 mp_integer from = range_type.get_from();
3829 const auto size = range_type.get_to() - range_type.get_from() + 1;
3830 const auto width = address_bits(size);
3831
3832 out << "(bvadd ";
3833 convert_expr(expr.op0());
3834 out << " (bvadd ";
3835 convert_expr(expr.op1());
3836 out << " (_ bv" << range_type.get_from() << ' ' << width
3837 << ")))"; // bv, bvadd, bvadd
3838 }
3839 else
3840 {
3842 }
3843 }
3844 else if(expr.type().id() == ID_floatbv)
3845 {
3846 // Floating-point additions should have be been converted
3847 // to ID_floatbv_plus during symbolic execution, adding
3848 // the rounding mode. See smt2_convt::convert_floatbv_plus.
3850 }
3851 else if(expr.type().id() == ID_pointer)
3852 {
3853 if(expr.operands().size() == 2)
3854 {
3855 exprt p = expr.op0(), i = expr.op1();
3856
3857 if(p.type().id() != ID_pointer)
3858 p.swap(i);
3859
3861 p.type().id() == ID_pointer,
3862 "one of the operands should have pointer type");
3863
3864 const auto &base_type = to_pointer_type(expr.type()).base_type();
3866 base_type.id() != ID_empty, "no pointer arithmetic over void pointers");
3867
3868 auto element_size_opt = pointer_offset_size(base_type, ns);
3869 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 0);
3870 mp_integer element_size = *element_size_opt;
3871
3872 // First convert the pointer operand
3873 out << "(let ((?pointerop ";
3874 convert_expr(p);
3875 out << ")) ";
3876
3877 // The addition is done on the offset part only.
3878 const std::size_t pointer_width = boolbv_width(p.type());
3879 const std::size_t offset_bits =
3880 pointer_width - config.bv_encoding.object_bits;
3881
3882 out << "(concat ";
3883 out << "((_ extract " << pointer_width - 1 << ' ' << offset_bits
3884 << ") ?pointerop) ";
3885 out << "(bvadd ((_ extract " << offset_bits - 1 << " 0) ?pointerop) ";
3886
3887 if(element_size >= 2)
3888 {
3889 out << "(bvmul ((_ extract " << offset_bits - 1 << " 0) ";
3890 convert_expr(i);
3891 out << ") (_ bv" << element_size << " " << offset_bits << "))";
3892 }
3893 else
3894 {
3895 out << "((_ extract " << offset_bits - 1 << " 0) ";
3896 convert_expr(i);
3897 out << ')'; // extract
3898 }
3899
3900 out << ")))"; // bvadd, concat, let
3901 }
3902 else
3903 {
3905 }
3906 }
3907 else
3908 UNEXPECTEDCASE("unsupported type for +: " + expr.type().id_string());
3909}
3910
3915{
3917
3918 /* CProver uses the x86 numbering of the rounding-mode
3919 * 0 == FE_TONEAREST
3920 * 1 == FE_DOWNWARD
3921 * 2 == FE_UPWARD
3922 * 3 == FE_TOWARDZERO
3923 * These literal values must be used rather than the macros
3924 * the macros from fenv.h to avoid portability problems.
3925 */
3926
3927 if(expr.is_constant())
3928 {
3929 const constant_exprt &cexpr=to_constant_expr(expr);
3930
3932
3933 if(value==0)
3934 out << "roundNearestTiesToEven";
3935 else if(value==1)
3936 out << "roundTowardNegative";
3937 else if(value==2)
3938 out << "roundTowardPositive";
3939 else if(value==3)
3940 out << "roundTowardZero";
3941 else if(value == 4)
3942 out << "roundNearestTiesToAway";
3943 else
3945 false,
3946 "Rounding mode should have value 0, 1, 2, 3, or 4",
3947 id2string(cexpr.get_value()));
3948 }
3949 else
3950 {
3951 std::size_t width=to_bitvector_type(expr.type()).get_width();
3952
3953 // Need to make the choice above part of the model
3954 out << "(ite (= (_ bv0 " << width << ") ";
3955 convert_expr(expr);
3956 out << ") roundNearestTiesToEven ";
3957
3958 out << "(ite (= (_ bv1 " << width << ") ";
3959 convert_expr(expr);
3960 out << ") roundTowardNegative ";
3961
3962 out << "(ite (= (_ bv2 " << width << ") ";
3963 convert_expr(expr);
3964 out << ") roundTowardPositive ";
3965
3966 out << "(ite (= (_ bv3 " << width << ") ";
3967 convert_expr(expr);
3968 out << ") roundTowardZero ";
3969
3970 // TODO: add some kind of error checking here
3971 out << "roundNearestTiesToAway";
3972
3973 out << "))))";
3974 }
3975}
3976
3978{
3979 const typet &type=expr.type();
3980
3982 type.id() == ID_floatbv ||
3983 (type.id() == ID_complex &&
3984 to_complex_type(type).subtype().id() == ID_floatbv));
3985
3986 if(use_FPA_theory)
3987 {
3988 if(type.id()==ID_floatbv)
3989 {
3990 out << "(fp.add ";
3992 out << " ";
3993 convert_expr(expr.lhs());
3994 out << " ";
3995 convert_expr(expr.rhs());
3996 out << ")";
3997 }
3998 else if(type.id()==ID_complex)
3999 {
4000 SMT2_TODO("+ for floatbv complex");
4001 }
4002 else
4004 false,
4005 "type should not be one of the unsupported types",
4006 type.id_string());
4007 }
4008 else
4009 convert_floatbv(expr);
4010}
4011
4013{
4014 if(expr.type().id()==ID_integer)
4015 {
4016 out << "(- ";
4017 convert_expr(expr.op0());
4018 out << " ";
4019 convert_expr(expr.op1());
4020 out << ")";
4021 }
4022 else if(expr.type().id()==ID_unsignedbv ||
4023 expr.type().id()==ID_signedbv ||
4024 expr.type().id()==ID_fixedbv)
4025 {
4026 if(expr.op0().type().id()==ID_pointer &&
4027 expr.op1().type().id()==ID_pointer)
4028 {
4029 // Pointer difference
4030 const auto &base_type = to_pointer_type(expr.op0().type()).base_type();
4032 base_type.id() != ID_empty, "no pointer arithmetic over void pointers");
4033 auto element_size_opt = pointer_offset_size(base_type, ns);
4034 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
4035 mp_integer element_size = *element_size_opt;
4036
4037 if(element_size >= 2)
4038 out << "(bvsdiv ";
4039
4040 INVARIANT(
4041 boolbv_width(expr.op0().type()) == boolbv_width(expr.type()),
4042 "bitvector width of operand shall be equal to the bitvector width of "
4043 "the expression");
4044
4045 out << "(bvsub ";
4046 convert_expr(expr.op0());
4047 out << " ";
4048 convert_expr(expr.op1());
4049 out << ")";
4050
4051 if(element_size >= 2)
4052 out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
4053 << "))";
4054 }
4055 else
4056 {
4057 out << "(bvsub ";
4058 convert_expr(expr.op0());
4059 out << " ";
4060 convert_expr(expr.op1());
4061 out << ")";
4062 }
4063 }
4064 else if(expr.type().id()==ID_floatbv)
4065 {
4066 // Floating-point subtraction should have be been converted
4067 // to ID_floatbv_minus during symbolic execution, adding
4068 // the rounding mode. See smt2_convt::convert_floatbv_minus.
4070 }
4071 else if(expr.type().id()==ID_pointer)
4072 {
4073 if(
4074 expr.op0().type().id() == ID_pointer &&
4075 (expr.op1().type().id() == ID_unsignedbv ||
4076 expr.op1().type().id() == ID_signedbv))
4077 {
4078 // rewrite p-o to p+(-o)
4079 return convert_plus(
4080 plus_exprt(expr.op0(), unary_minus_exprt(expr.op1())));
4081 }
4082 else
4084 "unsupported operand types for -: " + expr.op0().type().id_string() +
4085 " and " + expr.op1().type().id_string());
4086 }
4087 else if(expr.type().id() == ID_range)
4088 {
4089 auto &range_type = to_range_type(expr.type());
4090
4091 // sub: lhs + from - (rhs + from) - from = lhs - rhs - from
4092 mp_integer from = range_type.get_from();
4093 const auto size = range_type.get_to() - range_type.get_from() + 1;
4094 const auto width = address_bits(size);
4095
4096 out << "(bvsub (bvsub ";
4097 convert_expr(expr.op0());
4098 out << ' ';
4099 convert_expr(expr.op1());
4100 out << ") (_ bv" << range_type.get_from() << ' ' << width
4101 << "))"; // bv, bvsub
4102 }
4103 else
4104 UNEXPECTEDCASE("unsupported type for -: "+expr.type().id_string());
4105}
4106
4108{
4110 expr.type().id() == ID_floatbv,
4111 "type of ieee floating point expression shall be floatbv");
4112
4113 if(use_FPA_theory)
4114 {
4115 out << "(fp.sub ";
4117 out << " ";
4118 convert_expr(expr.lhs());
4119 out << " ";
4120 convert_expr(expr.rhs());
4121 out << ")";
4122 }
4123 else
4124 convert_floatbv(expr);
4125}
4126
4128{
4129 if(expr.type().id()==ID_unsignedbv ||
4130 expr.type().id()==ID_signedbv)
4131 {
4132 if(expr.type().id()==ID_unsignedbv)
4133 out << "(bvudiv ";
4134 else
4135 out << "(bvsdiv ";
4136
4137 convert_expr(expr.op0());
4138 out << " ";
4139 convert_expr(expr.op1());
4140 out << ")";
4141 }
4142 else if(expr.type().id()==ID_fixedbv)
4143 {
4144 fixedbv_spect spec(to_fixedbv_type(expr.type()));
4145 std::size_t fraction_bits=spec.get_fraction_bits();
4146
4147 out << "((_ extract " << spec.width-1 << " 0) ";
4148 out << "(bvsdiv ";
4149
4150 out << "(concat ";
4151 convert_expr(expr.op0());
4152 out << " (_ bv0 " << fraction_bits << ")) ";
4153
4154 out << "((_ sign_extend " << fraction_bits << ") ";
4155 convert_expr(expr.op1());
4156 out << ")";
4157
4158 out << "))";
4159 }
4160 else if(expr.type().id()==ID_floatbv)
4161 {
4162 // Floating-point division should have be been converted
4163 // to ID_floatbv_div during symbolic execution, adding
4164 // the rounding mode. See smt2_convt::convert_floatbv_div.
4166 }
4167 else
4168 UNEXPECTEDCASE("unsupported type for /: "+expr.type().id_string());
4169}
4170
4172{
4174 expr.type().id() == ID_floatbv,
4175 "type of ieee floating point expression shall be floatbv");
4176
4177 if(use_FPA_theory)
4178 {
4179 out << "(fp.div ";
4181 out << " ";
4182 convert_expr(expr.lhs());
4183 out << " ";
4184 convert_expr(expr.rhs());
4185 out << ")";
4186 }
4187 else
4188 convert_floatbv(expr);
4189}
4190
4192{
4193 // re-write to binary if needed
4194 if(expr.operands().size()>2)
4195 {
4196 // strip last operand
4197 exprt tmp=expr;
4198 tmp.operands().pop_back();
4199
4200 // recursive call
4201 return convert_mult(mult_exprt(tmp, expr.operands().back()));
4202 }
4203
4204 INVARIANT(
4205 expr.operands().size() == 2,
4206 "expression should have been converted to a variant with two operands");
4207
4208 if(expr.type().id()==ID_unsignedbv ||
4209 expr.type().id()==ID_signedbv)
4210 {
4211 // Note that bvmul is really unsigned,
4212 // but this is irrelevant as we chop-off any extra result
4213 // bits.
4214 out << "(bvmul ";
4215 convert_expr(expr.op0());
4216 out << " ";
4217 convert_expr(expr.op1());
4218 out << ")";
4219 }
4220 else if(expr.type().id()==ID_floatbv)
4221 {
4222 // Floating-point multiplication should have be been converted
4223 // to ID_floatbv_mult during symbolic execution, adding
4224 // the rounding mode. See smt2_convt::convert_floatbv_mult.
4226 }
4227 else if(expr.type().id()==ID_fixedbv)
4228 {
4229 fixedbv_spect spec(to_fixedbv_type(expr.type()));
4230 std::size_t fraction_bits=spec.get_fraction_bits();
4231
4232 out << "((_ extract "
4233 << spec.width+fraction_bits-1 << " "
4234 << fraction_bits << ") ";
4235
4236 out << "(bvmul ";
4237
4238 out << "((_ sign_extend " << fraction_bits << ") ";
4239 convert_expr(expr.op0());
4240 out << ") ";
4241
4242 out << "((_ sign_extend " << fraction_bits << ") ";
4243 convert_expr(expr.op1());
4244 out << ")";
4245
4246 out << "))"; // bvmul, extract
4247 }
4248 else if(expr.type().id()==ID_rational ||
4249 expr.type().id()==ID_integer ||
4250 expr.type().id()==ID_real)
4251 {
4252 out << "(*";
4253
4254 for(const auto &op : expr.operands())
4255 {
4256 out << " ";
4257 convert_expr(op);
4258 }
4259
4260 out << ")";
4261 }
4262 else
4263 UNEXPECTEDCASE("unsupported type for *: "+expr.type().id_string());
4264}
4265
4267{
4269 expr.type().id() == ID_floatbv,
4270 "type of ieee floating point expression shall be floatbv");
4271
4272 if(use_FPA_theory)
4273 {
4274 out << "(fp.mul ";
4276 out << " ";
4277 convert_expr(expr.lhs());
4278 out << " ";
4279 convert_expr(expr.rhs());
4280 out << ")";
4281 }
4282 else
4283 convert_floatbv(expr);
4284}
4285
4287{
4289 expr.type().id() == ID_floatbv,
4290 "type of ieee floating point expression shall be floatbv");
4291
4292 if(use_FPA_theory)
4293 {
4294 // Note that these do not have a rounding mode
4295 out << "(fp.rem ";
4296 convert_expr(expr.lhs());
4297 out << " ";
4298 convert_expr(expr.rhs());
4299 out << ")";
4300 }
4301 else
4302 {
4303 SMT2_TODO(
4304 "smt2_convt::convert_floatbv_rem to be implemented when not using "
4305 "FPA_theory");
4306 }
4307}
4308
4310{
4311 INVARIANT(
4312 expr.operands().size() == 3,
4313 "with expression should have exactly three operands");
4314
4315 const typet &expr_type = expr.type();
4316
4317 if(expr_type.id()==ID_array)
4318 {
4319 const array_typet &array_type=to_array_type(expr_type);
4320
4321 if(use_array_theory(expr))
4322 {
4323 out << "(store ";
4324 convert_expr(expr.old());
4325 out << " ";
4326 convert_expr(typecast_exprt(expr.where(), array_type.index_type()));
4327 out << " ";
4328 convert_expr(expr.new_value());
4329 out << ")";
4330 }
4331 else
4332 {
4333 // fixed-width
4334 std::size_t array_width=boolbv_width(array_type);
4335 std::size_t sub_width = boolbv_width(array_type.element_type());
4336 std::size_t index_width=boolbv_width(expr.where().type());
4337
4338 // We mask out the updated bits with AND,
4339 // and then OR-in the shifted new value.
4340
4341 out << "(let ((distance? ";
4342 out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
4343
4344 // SMT2 says that the shift distance needs to be as wide
4345 // as the stuff we are shifting.
4346 if(array_width>index_width)
4347 {
4348 out << "((_ zero_extend " << array_width-index_width << ") ";
4349 convert_expr(expr.where());
4350 out << ")";
4351 }
4352 else
4353 {
4354 out << "((_ extract " << array_width-1 << " 0) ";
4355 convert_expr(expr.where());
4356 out << ")";
4357 }
4358
4359 out << "))) "; // bvmul, distance?
4360
4361 out << "(bvor ";
4362 out << "(bvand ";
4363 out << "(bvnot ";
4364 out << "(bvshl (_ bv" << power(2, sub_width) - 1 << " " << array_width
4365 << ") ";
4366 out << "distance?)) "; // bvnot, bvlshl
4367 convert_expr(expr.old());
4368 out << ") "; // bvand
4369 out << "(bvshl ";
4370 out << "((_ zero_extend " << array_width-sub_width << ") ";
4371 convert_expr(expr.new_value());
4372 out << ") distance?)))"; // zero_extend, bvshl, bvor, let
4373 }
4374 }
4375 else if(expr_type.id() == ID_struct || expr_type.id() == ID_struct_tag)
4376 {
4377 const struct_typet &struct_type =
4378 expr_type.id() == ID_struct_tag
4379 ? ns.follow_tag(to_struct_tag_type(expr_type))
4380 : to_struct_type(expr_type);
4381
4382 const exprt &index = expr.where();
4383 const exprt &value = expr.new_value();
4384
4385 const irep_idt &component_name=index.get(ID_component_name);
4386
4387 INVARIANT(
4388 struct_type.has_component(component_name),
4389 "struct should have accessed component");
4390
4391 if(use_datatypes)
4392 {
4393 const std::string &smt_typename = datatype_map.at(expr_type);
4394
4395 out << "(update-" << smt_typename << "." << component_name << " ";
4396 convert_expr(expr.old());
4397 out << " ";
4398 convert_expr(value);
4399 out << ")";
4400 }
4401 else
4402 {
4403 std::size_t struct_width=boolbv_width(struct_type);
4404
4405 // figure out the offset and width of the member
4406 const boolbv_widtht::membert &m =
4407 boolbv_width.get_member(struct_type, component_name);
4408
4409 out << "(let ((?withop ";
4410 convert_expr(expr.old());
4411 out << ")) ";
4412
4413 if(m.width==struct_width)
4414 {
4415 // the struct is the same as the member, no concat needed,
4416 // ?withop won't be used
4417 convert_expr(value);
4418 }
4419 else if(m.offset==0)
4420 {
4421 // the member is at the beginning
4422 out << "(concat "
4423 << "((_ extract " << (struct_width-1) << " "
4424 << m.width << ") ?withop) ";
4425 convert_expr(value);
4426 out << ")"; // concat
4427 }
4428 else if(m.offset+m.width==struct_width)
4429 {
4430 // the member is at the end
4431 out << "(concat ";
4432 convert_expr(value);
4433 out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))";
4434 }
4435 else
4436 {
4437 // most general case, need two concat-s
4438 out << "(concat (concat "
4439 << "((_ extract " << (struct_width-1) << " "
4440 << (m.offset+m.width) << ") ?withop) ";
4441 convert_expr(value);
4442 out << ") ((_ extract " << (m.offset-1) << " 0) ?withop)";
4443 out << ")"; // concat
4444 }
4445
4446 out << ")"; // let ?withop
4447 }
4448 }
4449 else if(expr_type.id() == ID_union || expr_type.id() == ID_union_tag)
4450 {
4451 const exprt &value = expr.new_value();
4452
4453 std::size_t total_width = boolbv_width(expr_type);
4454
4455 std::size_t member_width=boolbv_width(value.type());
4456
4457 if(total_width==member_width)
4458 {
4459 flatten2bv(value);
4460 }
4461 else
4462 {
4463 INVARIANT(
4464 total_width > member_width,
4465 "total width should be greater than member_width as member_width is at "
4466 "most as large as total_width and the other case has been handled "
4467 "above");
4468 out << "(concat ";
4469 out << "((_ extract "
4470 << (total_width-1)
4471 << " " << member_width << ") ";
4472 convert_expr(expr.old());
4473 out << ") ";
4474 flatten2bv(value);
4475 out << ")";
4476 }
4477 }
4478 else if(expr_type.id()==ID_bv ||
4479 expr_type.id()==ID_unsignedbv ||
4480 expr_type.id()==ID_signedbv)
4481 {
4482 if(expr.new_value().type().id() == ID_bool)
4483 {
4485 update_bit_exprt(expr.old(), expr.where(), expr.new_value()));
4486 }
4487 else
4488 {
4490 update_bits_exprt(expr.old(), expr.where(), expr.new_value()));
4491 }
4492 }
4493 else
4495 "with expects struct, union, or array type, but got "+
4496 expr.type().id_string());
4497}
4498
4500{
4501 PRECONDITION(expr.operands().size() == 3);
4502
4503 SMT2_TODO("smt2_convt::convert_update to be implemented");
4504}
4505
4507{
4508 return convert_expr(expr.lower());
4509}
4510
4512{
4513 return convert_expr(expr.lower());
4514}
4515
4517{
4518 const typet &array_op_type = expr.array().type();
4519
4520 if(array_op_type.id()==ID_array)
4521 {
4522 const array_typet &array_type=to_array_type(array_op_type);
4523
4524 if(use_array_theory(expr.array()))
4525 {
4526 if(expr.is_boolean() && !use_array_of_bool)
4527 {
4528 out << "(= ";
4529 out << "(select ";
4530 convert_expr(expr.array());
4531 out << " ";
4532 convert_expr(typecast_exprt(expr.index(), array_type.index_type()));
4533 out << ")";
4534 out << " #b1)";
4535 }
4536 else
4537 {
4538 out << "(select ";
4539 convert_expr(expr.array());
4540 out << " ";
4541 convert_expr(typecast_exprt(expr.index(), array_type.index_type()));
4542 out << ")";
4543 }
4544 }
4545 else
4546 {
4547 // fixed size
4548 std::size_t array_width=boolbv_width(array_type);
4549
4550 unflatten(wheret::BEGIN, array_type.element_type());
4551
4552 std::size_t sub_width = boolbv_width(array_type.element_type());
4553 std::size_t index_width=boolbv_width(expr.index().type());
4554
4555 out << "((_ extract " << sub_width-1 << " 0) ";
4556 out << "(bvlshr ";
4557 convert_expr(expr.array());
4558 out << " ";
4559 out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
4560
4561 // SMT2 says that the shift distance must be the same as
4562 // the width of what we shift.
4563 if(array_width>index_width)
4564 {
4565 out << "((_ zero_extend " << array_width-index_width << ") ";
4566 convert_expr(expr.index());
4567 out << ")"; // zero_extend
4568 }
4569 else
4570 {
4571 out << "((_ extract " << array_width-1 << " 0) ";
4572 convert_expr(expr.index());
4573 out << ")"; // extract
4574 }
4575
4576 out << ")))"; // mult, bvlshr, extract
4577
4578 unflatten(wheret::END, array_type.element_type());
4579 }
4580 }
4581 else
4582 INVARIANT(
4583 false, "index with unsupported array type: " + array_op_type.id_string());
4584}
4585
4587{
4588 const member_exprt &member_expr=to_member_expr(expr);
4589 const exprt &struct_op=member_expr.struct_op();
4590 const typet &struct_op_type = struct_op.type();
4591 const irep_idt &name=member_expr.get_component_name();
4592
4593 if(struct_op_type.id() == ID_struct || struct_op_type.id() == ID_struct_tag)
4594 {
4595 const struct_typet &struct_type =
4596 struct_op_type.id() == ID_struct_tag
4597 ? ns.follow_tag(to_struct_tag_type(struct_op_type))
4598 : to_struct_type(struct_op_type);
4599
4600 INVARIANT(
4601 struct_type.has_component(name), "struct should have accessed component");
4602
4603 if(use_datatypes)
4604 {
4605 const std::string &smt_typename = datatype_map.at(struct_type);
4606
4607 out << "(" << smt_typename << "."
4608 << struct_type.get_component(name).get_name()
4609 << " ";
4610 convert_expr(struct_op);
4611 out << ")";
4612 }
4613 else
4614 {
4615 // we extract
4616 const auto &member_offset = boolbv_width.get_member(struct_type, name);
4617
4618 if(expr.type().id() == ID_bool)
4619 out << "(= ";
4620 out << "((_ extract " << (member_offset.offset + member_offset.width - 1)
4621 << " " << member_offset.offset << ") ";
4622 convert_expr(struct_op);
4623 out << ")";
4624 if(expr.type().id() == ID_bool)
4625 out << " #b1)";
4626 }
4627 }
4628 else if(
4629 struct_op_type.id() == ID_union || struct_op_type.id() == ID_union_tag)
4630 {
4631 std::size_t width=boolbv_width(expr.type());
4633 width != 0, "failed to get union member width");
4634
4635 if(use_datatypes)
4636 {
4637 unflatten(wheret::BEGIN, expr.type());
4638
4639 out << "((_ extract " << (width - 1) << " 0) ";
4640 convert_expr(struct_op);
4641 out << ")";
4642
4643 unflatten(wheret::END, expr.type());
4644 }
4645 else
4646 {
4647 out << "((_ extract " << (width - 1) << " 0) ";
4648 convert_expr(struct_op);
4649 out << ")";
4650 }
4651 }
4652 else
4654 "convert_member on an unexpected type "+struct_op_type.id_string());
4655}
4656
4658{
4659 const typet &type = expr.type();
4660
4661 if(type.id()==ID_bool)
4662 {
4663 out << "(ite ";
4664 convert_expr(expr); // this returns a Bool
4665 out << " #b1 #b0)"; // this is a one-bit bit-vector
4666 }
4667 else if(type.id()==ID_array)
4668 {
4669 if(use_array_theory(expr))
4670 {
4671 // concatenate elements
4672 const array_typet &array_type = to_array_type(type);
4673
4674 mp_integer size =
4676
4677 // SMT-LIB 2 concat is binary only
4678 std::size_t n_concat = 0;
4679 for(mp_integer i = size; i > 1; --i)
4680 {
4681 ++n_concat;
4682 out << "(concat ";
4683
4684 flatten2bv(
4685 index_exprt{expr, from_integer(i - 1, array_type.index_type())});
4686
4687 out << " ";
4688 }
4689
4690 flatten2bv(index_exprt{expr, from_integer(0, array_type.index_type())});
4691
4692 out << std::string(n_concat, ')'); // concat
4693 }
4694 else
4695 convert_expr(expr);
4696 }
4697 else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4698 {
4699 if(use_datatypes)
4700 {
4701 // concatenate elements
4702 const struct_typet &struct_type =
4703 type.id() == ID_struct_tag ? ns.follow_tag(to_struct_tag_type(type))
4704 : to_struct_type(type);
4705
4706 const struct_typet::componentst &components=
4707 struct_type.components();
4708
4709 // SMT-LIB 2 concat is binary only
4710 std::size_t n_concat = 0;
4711 for(std::size_t i=components.size(); i>1; i--)
4712 {
4713 if(is_zero_width(components[i - 1].type(), ns))
4714 continue;
4715 else if(i > 2 || !is_zero_width(components[0].type(), ns))
4716 {
4717 ++n_concat;
4718 out << "(concat ";
4719 }
4720
4721 flatten2bv(member_exprt{expr, components[i - 1]});
4722
4723 out << " ";
4724 }
4725
4726 if(!is_zero_width(components[0].type(), ns))
4727 {
4728 flatten2bv(member_exprt{expr, components[0]});
4729 }
4730
4731 out << std::string(n_concat, ')'); // concat
4732 }
4733 else
4734 convert_expr(expr);
4735 }
4736 else if(type.id()==ID_floatbv)
4737 {
4738 INVARIANT(
4740 "floatbv expressions should be flattened when using FPA theory");
4741
4742 convert_expr(expr);
4743 }
4744 else
4745 convert_expr(expr);
4746}
4747
4749 wheret where,
4750 const typet &type,
4751 unsigned nesting)
4752{
4753 if(type.id()==ID_bool)
4754 {
4755 if(where==wheret::BEGIN)
4756 out << "(= "; // produces a bool
4757 else
4758 out << " #b1)";
4759 }
4760 else if(type.id() == ID_array)
4761 {
4763
4764 if(where == wheret::BEGIN)
4765 out << "(let ((?ufop" << nesting << " ";
4766 else
4767 {
4768 out << ")) ";
4769
4770 const array_typet &array_type = to_array_type(type);
4771
4772 std::size_t subtype_width = boolbv_width(array_type.element_type());
4773
4775 array_type.size().is_constant(),
4776 "cannot unflatten arrays of non-constant size");
4777 mp_integer size =
4779
4780 for(mp_integer i = 1; i < size; ++i)
4781 out << "(store ";
4782
4783 out << "((as const ";
4784 convert_type(array_type);
4785 out << ") ";
4786 // use element at index 0 as default value
4787 unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1);
4788 out << "((_ extract " << subtype_width - 1 << " "
4789 << "0) ?ufop" << nesting << ")";
4790 unflatten(wheret::END, array_type.element_type(), nesting + 1);
4791 out << ") ";
4792
4793 std::size_t offset = subtype_width;
4794 for(mp_integer i = 1; i < size; ++i, offset += subtype_width)
4795 {
4796 convert_expr(from_integer(i, array_type.index_type()));
4797 out << ' ';
4798 unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1);
4799 out << "((_ extract " << offset + subtype_width - 1 << " " << offset
4800 << ") ?ufop" << nesting << ")";
4801 unflatten(wheret::END, array_type.element_type(), nesting + 1);
4802 out << ")"; // store
4803 }
4804
4805 out << ")"; // let
4806 }
4807 }
4808 else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4809 {
4810 if(use_datatypes)
4811 {
4812 // extract members
4813 if(where==wheret::BEGIN)
4814 out << "(let ((?ufop" << nesting << " ";
4815 else
4816 {
4817 out << ")) ";
4818
4819 const std::string &smt_typename = datatype_map.at(type);
4820
4821 out << "(mk-" << smt_typename;
4822
4823 const struct_typet &struct_type =
4824 type.id() == ID_struct_tag ? ns.follow_tag(to_struct_tag_type(type))
4825 : to_struct_type(type);
4826
4827 const struct_typet::componentst &components=
4828 struct_type.components();
4829
4830 std::size_t offset=0;
4831
4832 std::size_t i=0;
4833 for(struct_typet::componentst::const_iterator
4834 it=components.begin();
4835 it!=components.end();
4836 it++, i++)
4837 {
4838 if(is_zero_width(it->type(), ns))
4839 continue;
4840
4841 std::size_t member_width=boolbv_width(it->type());
4842
4843 out << " ";
4844 unflatten(wheret::BEGIN, it->type(), nesting+1);
4845 out << "((_ extract " << offset+member_width-1 << " "
4846 << offset << ") ?ufop" << nesting << ")";
4847 unflatten(wheret::END, it->type(), nesting+1);
4848 offset+=member_width;
4849 }
4850
4851 out << "))"; // mk-, let
4852 }
4853 }
4854 else
4855 {
4856 // nop, already a bv
4857 }
4858 }
4859 else
4860 {
4861 // nop
4862 }
4863}
4864
4865void smt2_convt::set_to(const exprt &expr, bool value)
4866{
4867 PRECONDITION(expr.is_boolean());
4868
4869 if(expr.id()==ID_and && value)
4870 {
4871 for(const auto &op : expr.operands())
4872 set_to(op, true);
4873 return;
4874 }
4875
4876 if(expr.id()==ID_or && !value)
4877 {
4878 for(const auto &op : expr.operands())
4879 set_to(op, false);
4880 return;
4881 }
4882
4883 if(expr.id()==ID_not)
4884 {
4885 return set_to(to_not_expr(expr).op(), !value);
4886 }
4887
4888 out << "\n";
4889
4890 // special treatment for "set_to(a=b, true)" where
4891 // a is a new symbol
4892
4893 if(expr.id() == ID_equal && value)
4894 {
4895 const equal_exprt &equal_expr=to_equal_expr(expr);
4896 if(is_zero_width(equal_expr.lhs().type(), ns))
4897 {
4898 // ignore equality checking over expressions with empty (void) type
4899 return;
4900 }
4901
4902 if(equal_expr.lhs().id()==ID_symbol)
4903 {
4904 const irep_idt &identifier=
4905 to_symbol_expr(equal_expr.lhs()).get_identifier();
4906
4907 if(
4908 identifier_map.find(identifier) == identifier_map.end() &&
4909 equal_expr.lhs() != equal_expr.rhs())
4910 {
4911 auto id_entry = identifier_map.insert(
4912 {identifier, identifiert{equal_expr.lhs().type(), false}});
4913 CHECK_RETURN(id_entry.second);
4914
4915 find_symbols(id_entry.first->second.type);
4916 exprt prepared_rhs = prepare_for_convert_expr(equal_expr.rhs());
4917
4918 std::string smt2_identifier=convert_identifier(identifier);
4919 smt2_identifiers.insert(smt2_identifier);
4920
4921 out << "; set_to true (equal)\n";
4922
4923 if(equal_expr.lhs().type().id() == ID_mathematical_function)
4924 {
4925 // We avoid define-fun, since it has been reported to cause
4926 // trouble with Z3's parser.
4927 out << "(declare-fun " << smt2_identifier;
4928
4929 auto &mathematical_function_type =
4930 to_mathematical_function_type(equal_expr.lhs().type());
4931
4932 out << " (";
4933 bool first = true;
4934
4935 for(auto &t : mathematical_function_type.domain())
4936 {
4937 if(first)
4938 first = false;
4939 else
4940 out << ' ';
4941
4942 convert_type(t);
4943 }
4944
4945 out << ") ";
4946 convert_type(mathematical_function_type.codomain());
4947 out << ")\n";
4948
4949 out << "(assert (= " << smt2_identifier << ' ';
4950 convert_expr(prepared_rhs);
4951 out << ')' << ')' << '\n';
4952 }
4953 else
4954 {
4955 out << "(define-fun " << smt2_identifier;
4956 out << " () ";
4957 convert_type(equal_expr.lhs().type());
4958 out << ' ';
4959 if(
4960 equal_expr.lhs().type().id() != ID_array ||
4961 use_array_theory(prepared_rhs))
4962 {
4963 convert_expr(prepared_rhs);
4964 }
4965 else
4966 {
4967 unflatten(wheret::BEGIN, equal_expr.lhs().type());
4968
4969 convert_expr(prepared_rhs);
4970
4971 unflatten(wheret::END, equal_expr.lhs().type());
4972 }
4973 out << ')' << '\n';
4974 }
4975
4976 return; // done
4977 }
4978 }
4979 }
4980
4981 exprt prepared_expr = prepare_for_convert_expr(expr);
4982
4983#if 0
4984 out << "; CONV: "
4985 << format(expr) << "\n";
4986#endif
4987
4988 out << "; set_to " << (value?"true":"false") << "\n"
4989 << "(assert ";
4990 if(!value)
4991 {
4992 out << "(not ";
4993 }
4994 const auto found_literal = defined_expressions.find(expr);
4995 if(!(found_literal == defined_expressions.end()))
4996 {
4997 // This is a converted expression, we can just assert the literal name
4998 // since the expression is already defined
4999 out << found_literal->second;
5000 set_values[found_literal->second] = value;
5001 }
5002 else
5003 {
5004 convert_expr(prepared_expr);
5005 }
5006 if(!value)
5007 {
5008 out << ")";
5009 }
5010 out << ")\n";
5011 return;
5012}
5013
5021{
5022 exprt lowered_expr = expr;
5023
5024 for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
5025 it != itend;
5026 ++it)
5027 {
5028 if(
5029 it->id() == ID_byte_extract_little_endian ||
5030 it->id() == ID_byte_extract_big_endian)
5031 {
5032 it.mutate() = lower_byte_extract(to_byte_extract_expr(*it), ns);
5033 }
5034 else if(
5035 it->id() == ID_byte_update_little_endian ||
5036 it->id() == ID_byte_update_big_endian)
5037 {
5038 it.mutate() = lower_byte_update(to_byte_update_expr(*it), ns);
5039 }
5040 }
5041
5042 return lowered_expr;
5043}
5044
5053{
5054 // First, replace byte operators, because they may introduce new array
5055 // expressions that must be seen by find_symbols:
5056 exprt lowered_expr = lower_byte_operators(expr);
5057 INVARIANT(
5058 !has_byte_operator(lowered_expr),
5059 "lower_byte_operators should remove all byte operators");
5060
5061 // Perform rewrites that may introduce new symbols
5062 for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
5063 it != itend;) // no ++it
5064 {
5065 if(
5066 auto prophecy_r_or_w_ok =
5068 {
5069 exprt lowered = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns);
5070 it.mutate() = lowered;
5071 it.next_sibling_or_parent();
5072 }
5073 else if(
5074 auto prophecy_pointer_in_range =
5076 {
5077 exprt lowered = simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
5078 it.mutate() = lowered;
5079 it.next_sibling_or_parent();
5080 }
5081 else
5082 ++it;
5083 }
5084
5085 // Now create symbols for all composite expressions present in lowered_expr:
5086 find_symbols(lowered_expr);
5087
5088 return lowered_expr;
5089}
5090
5092{
5093 if(is_zero_width(expr.type(), ns))
5094 return;
5095
5096 // recursive call on type
5097 find_symbols(expr.type());
5098
5099 if(expr.id() == ID_exists || expr.id() == ID_forall)
5100 {
5101 std::unordered_map<irep_idt, std::optional<identifiert>> shadowed_syms;
5102
5103 // do not declare the quantified symbol, but record
5104 // as 'bound symbol'
5105 const auto &q_expr = to_quantifier_expr(expr);
5106 for(const auto &symbol : q_expr.variables())
5107 {
5108 const auto identifier = symbol.get_identifier();
5109 auto id_entry =
5110 identifier_map.insert({identifier, identifiert{symbol.type(), true}});
5111 shadowed_syms.insert(
5112 {identifier,
5113 id_entry.second ? std::nullopt
5114 : std::optional{id_entry.first->second}});
5115 }
5116 find_symbols(q_expr.where());
5117 for(const auto &[id, shadowed_val] : shadowed_syms)
5118 {
5119 auto previous_entry = identifier_map.find(id);
5120 if(!shadowed_val.has_value())
5121 identifier_map.erase(previous_entry);
5122 else
5123 previous_entry->second = std::move(*shadowed_val);
5124 }
5125 return;
5126 }
5127
5128 // recursive call on operands
5129 for(const auto &op : expr.operands())
5130 find_symbols(op);
5131
5132 if(expr.id()==ID_symbol ||
5133 expr.id()==ID_nondet_symbol)
5134 {
5135 // we don't track function-typed symbols
5136 if(expr.type().id()==ID_code)
5137 return;
5138
5139 irep_idt identifier;
5140
5141 if(expr.id()==ID_symbol)
5142 identifier=to_symbol_expr(expr).get_identifier();
5143 else
5144 identifier="nondet_"+
5145 id2string(to_nondet_symbol_expr(expr).get_identifier());
5146
5147 auto id_entry =
5148 identifier_map.insert({identifier, identifiert{expr.type(), false}});
5149
5150 if(id_entry.second)
5151 {
5152 std::string smt2_identifier=convert_identifier(identifier);
5153 smt2_identifiers.insert(smt2_identifier);
5154
5155 out << "; find_symbols\n";
5156 out << "(declare-fun " << smt2_identifier;
5157
5158 if(expr.type().id() == ID_mathematical_function)
5159 {
5160 auto &mathematical_function_type =
5162 out << " (";
5163 bool first = true;
5164
5165 for(auto &type : mathematical_function_type.domain())
5166 {
5167 if(first)
5168 first = false;
5169 else
5170 out << ' ';
5171 convert_type(type);
5172 }
5173
5174 out << ") ";
5175 convert_type(mathematical_function_type.codomain());
5176 }
5177 else
5178 {
5179 out << " () ";
5180 convert_type(expr.type());
5181 }
5182
5183 out << ")" << "\n";
5184 }
5185 }
5186 else if(expr.id() == ID_array_of)
5187 {
5188 if(!use_as_const)
5189 {
5190 if(defined_expressions.find(expr) == defined_expressions.end())
5191 {
5192 const auto &array_of = to_array_of_expr(expr);
5193 const auto &array_type = array_of.type();
5194
5195 const irep_idt id =
5196 "array_of." + std::to_string(defined_expressions.size());
5197 out << "; the following is a substitute for lambda i. x\n";
5198 out << "(declare-fun " << id << " () ";
5199 convert_type(array_type);
5200 out << ")\n";
5201
5202 if(!is_zero_width(array_type.element_type(), ns))
5203 {
5204 // use a quantifier-based initialization instead of lambda
5205 out << "(assert (forall ((i ";
5206 convert_type(array_type.index_type());
5207 out << ")) (= (select " << id << " i) ";
5208 if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
5209 {
5210 out << "(ite ";
5211 convert_expr(array_of.what());
5212 out << " #b1 #b0)";
5213 }
5214 else
5215 {
5216 convert_expr(array_of.what());
5217 }
5218 out << ")))\n";
5219 }
5220
5221 defined_expressions[expr] = id;
5222 }
5223 }
5224 }
5225 else if(expr.id() == ID_array_comprehension)
5226 {
5228 {
5229 if(defined_expressions.find(expr) == defined_expressions.end())
5230 {
5231 const auto &array_comprehension = to_array_comprehension_expr(expr);
5232 const auto &array_type = array_comprehension.type();
5233 const auto &array_size = array_type.size();
5234
5235 const irep_idt id =
5236 "array_comprehension." + std::to_string(defined_expressions.size());
5237 out << "(declare-fun " << id << " () ";
5238 convert_type(array_type);
5239 out << ")\n";
5240
5241 out << "; the following is a substitute for lambda i . x(i)\n";
5242 out << "; universally quantified initialization of the array\n";
5243 out << "(assert (forall ((";
5244 convert_expr(array_comprehension.arg());
5245 out << " ";
5246 convert_type(array_size.type());
5247 out << ")) (=> (and (bvule (_ bv0 " << boolbv_width(array_size.type())
5248 << ") ";
5249 convert_expr(array_comprehension.arg());
5250 out << ") (bvult ";
5251 convert_expr(array_comprehension.arg());
5252 out << " ";
5253 convert_expr(array_size);
5254 out << ")) (= (select " << id << " ";
5255 convert_expr(array_comprehension.arg());
5256 out << ") ";
5257 if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
5258 {
5259 out << "(ite ";
5260 convert_expr(array_comprehension.body());
5261 out << " #b1 #b0)";
5262 }
5263 else
5264 {
5265 convert_expr(array_comprehension.body());
5266 }
5267 out << "))))\n";
5268
5269 defined_expressions[expr] = id;
5270 }
5271 }
5272 }
5273 else if(expr.id()==ID_array)
5274 {
5275 if(defined_expressions.find(expr)==defined_expressions.end())
5276 {
5277 const array_typet &array_type=to_array_type(expr.type());
5278
5279 const irep_idt id = "array." + std::to_string(defined_expressions.size());
5280 out << "; the following is a substitute for an array constructor" << "\n";
5281 out << "(declare-fun " << id << " () ";
5282 convert_type(array_type);
5283 out << ")" << "\n";
5284
5285 if(!is_zero_width(array_type.element_type(), ns))
5286 {
5287 for(std::size_t i = 0; i < expr.operands().size(); i++)
5288 {
5289 out << "(assert (= (select " << id << " ";
5290 convert_expr(from_integer(i, array_type.index_type()));
5291 out << ") "; // select
5292 if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
5293 {
5294 out << "(ite ";
5295 convert_expr(expr.operands()[i]);
5296 out << " #b1 #b0)";
5297 }
5298 else
5299 {
5300 convert_expr(expr.operands()[i]);
5301 }
5302 out << "))"
5303 << "\n"; // =, assert
5304 }
5305 }
5306
5307 defined_expressions[expr]=id;
5308 }
5309 }
5310 else if(expr.id()==ID_string_constant)
5311 {
5312 if(defined_expressions.find(expr)==defined_expressions.end())
5313 {
5314 // introduce a temporary array.
5316 const array_typet &array_type=to_array_type(tmp.type());
5317
5318 const irep_idt id =
5319 "string." + std::to_string(defined_expressions.size());
5320 out << "; the following is a substitute for a string" << "\n";
5321 out << "(declare-fun " << id << " () ";
5322 convert_type(array_type);
5323 out << ")" << "\n";
5324
5325 for(std::size_t i=0; i<tmp.operands().size(); i++)
5326 {
5327 out << "(assert (= (select " << id << ' ';
5328 convert_expr(from_integer(i, array_type.index_type()));
5329 out << ") "; // select
5330 convert_expr(tmp.operands()[i]);
5331 out << "))" << "\n";
5332 }
5333
5334 defined_expressions[expr]=id;
5335 }
5336 }
5337 else if(
5339 {
5340 if(object_sizes.find(*object_size) == object_sizes.end())
5341 {
5342 const irep_idt id = convert_identifier(
5343 "object_size." + std::to_string(object_sizes.size()));
5344 out << "(declare-fun " << id << " () ";
5345 convert_type(object_size->type());
5346 out << ")"
5347 << "\n";
5348
5350 }
5351 }
5352 // clang-format off
5353 else if(!use_FPA_theory &&
5354 expr.operands().size() >= 1 &&
5355 (expr.id() == ID_floatbv_plus ||
5356 expr.id() == ID_floatbv_minus ||
5357 expr.id() == ID_floatbv_mult ||
5358 expr.id() == ID_floatbv_div ||
5359 expr.id() == ID_floatbv_typecast ||
5360 expr.id() == ID_ieee_float_equal ||
5361 expr.id() == ID_ieee_float_notequal ||
5362 ((expr.id() == ID_lt ||
5363 expr.id() == ID_gt ||
5364 expr.id() == ID_le ||
5365 expr.id() == ID_ge ||
5366 expr.id() == ID_isnan ||
5367 expr.id() == ID_isnormal ||
5368 expr.id() == ID_isfinite ||
5369 expr.id() == ID_isinf ||
5370 expr.id() == ID_sign ||
5371 expr.id() == ID_unary_minus ||
5372 expr.id() == ID_typecast ||
5373 expr.id() == ID_abs) &&
5374 to_multi_ary_expr(expr).op0().type().id() == ID_floatbv)))
5375 // clang-format on
5376 {
5377 irep_idt function =
5378 convert_identifier("float_bv." + expr.id_string() + floatbv_suffix(expr));
5379
5380 if(bvfp_set.insert(function).second)
5381 {
5382 out << "; this is a model for " << expr.id() << " : "
5383 << type2id(to_multi_ary_expr(expr).op0().type()) << " -> "
5384 << type2id(expr.type()) << "\n"
5385 << "(define-fun " << function << " (";
5386
5387 for(std::size_t i = 0; i < expr.operands().size(); i++)
5388 {
5389 if(i!=0)
5390 out << " ";
5391 out << "(op" << i << ' ';
5392 convert_type(expr.operands()[i].type());
5393 out << ')';
5394 }
5395
5396 out << ") ";
5397 convert_type(expr.type()); // return type
5398 out << ' ';
5399
5400 exprt tmp1=expr;
5401 for(std::size_t i = 0; i < tmp1.operands().size(); i++)
5402 tmp1.operands()[i]=
5403 smt2_symbolt("op"+std::to_string(i), tmp1.operands()[i].type());
5404
5405 exprt tmp2=float_bv(tmp1);
5406 tmp2=letify(tmp2);
5407 CHECK_RETURN(!tmp2.is_nil());
5408
5409 convert_expr(tmp2);
5410
5411 out << ")\n"; // define-fun
5412 }
5413 }
5414 else if(
5415 use_FPA_theory && expr.id() == ID_typecast &&
5416 to_typecast_expr(expr).op().type().id() == ID_floatbv &&
5417 expr.type().id() == ID_bv)
5418 {
5419 // This is _NOT_ a semantic conversion, but bit-wise.
5420 if(defined_expressions.find(expr) == defined_expressions.end())
5421 {
5422 // This conversion is non-trivial as it requires creating a
5423 // new bit-vector variable and then asserting that it converts
5424 // to the required floating-point number.
5425 const irep_idt id =
5426 "bvfromfloat." + std::to_string(defined_expressions.size());
5427 out << "(declare-fun " << id << " () ";
5428 convert_type(expr.type());
5429 out << ')' << '\n';
5430
5431 const typecast_exprt &tc = to_typecast_expr(expr);
5432 const auto &floatbv_type = to_floatbv_type(tc.op().type());
5433 out << "(assert (= ";
5434 out << "((_ to_fp " << floatbv_type.get_e() << " "
5435 << floatbv_type.get_f() + 1 << ") " << id << ')';
5436 convert_expr(tc.op());
5437 out << ')'; // =
5438 out << ')' << '\n';
5439
5440 defined_expressions[expr] = id;
5441 }
5442 }
5443 else if(expr.id() == ID_initial_state)
5444 {
5445 irep_idt function = "initial-state";
5446
5447 if(state_fkt_declared.insert(function).second)
5448 {
5449 out << "(declare-fun " << function << " (";
5450 convert_type(to_unary_expr(expr).op().type());
5451 out << ") ";
5452 convert_type(expr.type()); // return type
5453 out << ")\n"; // declare-fun
5454 }
5455 }
5456 else if(expr.id() == ID_evaluate)
5457 {
5458 irep_idt function = "evaluate-" + type2id(expr.type());
5459
5460 if(state_fkt_declared.insert(function).second)
5461 {
5462 out << "(declare-fun " << function << " (";
5463 convert_type(to_binary_expr(expr).op0().type());
5464 out << ' ';
5465 convert_type(to_binary_expr(expr).op1().type());
5466 out << ") ";
5467 convert_type(expr.type()); // return type
5468 out << ")\n"; // declare-fun
5469 }
5470 }
5471 else if(
5472 expr.id() == ID_state_is_cstring ||
5473 expr.id() == ID_state_is_dynamic_object ||
5474 expr.id() == ID_state_live_object || expr.id() == ID_state_writeable_object)
5475 {
5476 irep_idt function =
5477 expr.id() == ID_state_is_cstring ? "state-is-cstring"
5478 : expr.id() == ID_state_is_dynamic_object ? "state-is-dynamic-object"
5479 : expr.id() == ID_state_live_object ? "state-live-object"
5480 : "state-writeable-object";
5481
5482 if(state_fkt_declared.insert(function).second)
5483 {
5484 out << "(declare-fun " << function << " (";
5485 convert_type(to_binary_expr(expr).op0().type());
5486 out << ' ';
5487 convert_type(to_binary_expr(expr).op1().type());
5488 out << ") ";
5489 convert_type(expr.type()); // return type
5490 out << ")\n"; // declare-fun
5491 }
5492 }
5493 else if(
5494 expr.id() == ID_state_r_ok || expr.id() == ID_state_w_ok ||
5495 expr.id() == ID_state_rw_ok)
5496 {
5497 irep_idt function = expr.id() == ID_state_r_ok ? "state-r-ok"
5498 : expr.id() == ID_state_w_ok ? "state-w-ok"
5499 : "state-rw-ok";
5500
5501 if(state_fkt_declared.insert(function).second)
5502 {
5503 out << "(declare-fun " << function << " (";
5504 convert_type(to_ternary_expr(expr).op0().type());
5505 out << ' ';
5506 convert_type(to_ternary_expr(expr).op1().type());
5507 out << ' ';
5508 convert_type(to_ternary_expr(expr).op2().type());
5509 out << ") ";
5510 convert_type(expr.type()); // return type
5511 out << ")\n"; // declare-fun
5512 }
5513 }
5514 else if(expr.id() == ID_update_state)
5515 {
5516 irep_idt function =
5517 "update-state-" + type2id(to_multi_ary_expr(expr).op2().type());
5518
5519 if(state_fkt_declared.insert(function).second)
5520 {
5521 out << "(declare-fun " << function << " (";
5522 convert_type(to_multi_ary_expr(expr).op0().type());
5523 out << ' ';
5524 convert_type(to_multi_ary_expr(expr).op1().type());
5525 out << ' ';
5526 convert_type(to_multi_ary_expr(expr).op2().type());
5527 out << ") ";
5528 convert_type(expr.type()); // return type
5529 out << ")\n"; // declare-fun
5530 }
5531 }
5532 else if(expr.id() == ID_enter_scope_state)
5533 {
5534 irep_idt function =
5535 "enter-scope-state-" + type2id(to_binary_expr(expr).op1().type());
5536
5537 if(state_fkt_declared.insert(function).second)
5538 {
5539 out << "(declare-fun " << function << " (";
5540 convert_type(to_binary_expr(expr).op0().type());
5541 out << ' ';
5542 convert_type(to_binary_expr(expr).op1().type());
5543 out << ' ';
5545 out << ") ";
5546 convert_type(expr.type()); // return type
5547 out << ")\n"; // declare-fun
5548 }
5549 }
5550 else if(expr.id() == ID_exit_scope_state)
5551 {
5552 irep_idt function =
5553 "exit-scope-state-" + type2id(to_binary_expr(expr).op1().type());
5554
5555 if(state_fkt_declared.insert(function).second)
5556 {
5557 out << "(declare-fun " << function << " (";
5558 convert_type(to_binary_expr(expr).op0().type());
5559 out << ' ';
5560 convert_type(to_binary_expr(expr).op1().type());
5561 out << ") ";
5562 convert_type(expr.type()); // return type
5563 out << ")\n"; // declare-fun
5564 }
5565 }
5566 else if(expr.id() == ID_allocate)
5567 {
5568 irep_idt function = "allocate";
5569
5570 if(state_fkt_declared.insert(function).second)
5571 {
5572 out << "(declare-fun " << function << " (";
5573 convert_type(to_binary_expr(expr).op0().type());
5574 out << ' ';
5575 convert_type(to_binary_expr(expr).op1().type());
5576 out << ") ";
5577 convert_type(expr.type()); // return type
5578 out << ")\n"; // declare-fun
5579 }
5580 }
5581 else if(expr.id() == ID_reallocate)
5582 {
5583 irep_idt function = "reallocate";
5584
5585 if(state_fkt_declared.insert(function).second)
5586 {
5587 out << "(declare-fun " << function << " (";
5588 convert_type(to_ternary_expr(expr).op0().type());
5589 out << ' ';
5590 convert_type(to_ternary_expr(expr).op1().type());
5591 out << ' ';
5592 convert_type(to_ternary_expr(expr).op2().type());
5593 out << ") ";
5594 convert_type(expr.type()); // return type
5595 out << ")\n"; // declare-fun
5596 }
5597 }
5598 else if(expr.id() == ID_deallocate_state)
5599 {
5600 irep_idt function = "deallocate";
5601
5602 if(state_fkt_declared.insert(function).second)
5603 {
5604 out << "(declare-fun " << function << " (";
5605 convert_type(to_binary_expr(expr).op0().type());
5606 out << ' ';
5607 convert_type(to_binary_expr(expr).op1().type());
5608 out << ") ";
5609 convert_type(expr.type()); // return type
5610 out << ")\n"; // declare-fun
5611 }
5612 }
5613 else if(expr.id() == ID_object_address)
5614 {
5615 irep_idt function = "object-address";
5616
5617 if(state_fkt_declared.insert(function).second)
5618 {
5619 out << "(declare-fun " << function << " (String) ";
5620 convert_type(expr.type()); // return type
5621 out << ")\n"; // declare-fun
5622 }
5623 }
5624 else if(expr.id() == ID_field_address)
5625 {
5626 irep_idt function = "field-address-" + type2id(expr.type());
5627
5628 if(state_fkt_declared.insert(function).second)
5629 {
5630 out << "(declare-fun " << function << " (";
5631 convert_type(to_field_address_expr(expr).op().type());
5632 out << ' ';
5633 out << "String";
5634 out << ") ";
5635 convert_type(expr.type()); // return type
5636 out << ")\n"; // declare-fun
5637 }
5638 }
5639 else if(expr.id() == ID_element_address)
5640 {
5641 irep_idt function = "element-address-" + type2id(expr.type());
5642
5643 if(state_fkt_declared.insert(function).second)
5644 {
5645 out << "(declare-fun " << function << " (";
5646 convert_type(to_element_address_expr(expr).base().type());
5647 out << ' ';
5648 convert_type(to_element_address_expr(expr).index().type());
5649 out << ' '; // repeat, for the element size
5650 convert_type(to_element_address_expr(expr).index().type());
5651 out << ") ";
5652 convert_type(expr.type()); // return type
5653 out << ")\n"; // declare-fun
5654 }
5655 }
5656}
5657
5659{
5660 const typet &type = expr.type();
5661 PRECONDITION(type.id()==ID_array);
5662
5663 // arrays inside structs get flattened, unless we have datatypes
5664 if(expr.id() == ID_with)
5665 return use_array_theory(to_with_expr(expr).old());
5666 else
5667 return use_datatypes || expr.id() != ID_member;
5668}
5669
5671{
5672 if(type.id()==ID_array)
5673 {
5674 const array_typet &array_type=to_array_type(type);
5675 CHECK_RETURN(array_type.size().is_not_nil());
5676
5677 // we always use array theory for top-level arrays
5678 const typet &subtype = array_type.element_type();
5679
5680 // Arrays map the index type to the element type.
5681 out << "(Array ";
5682 convert_type(array_type.index_type());
5683 out << " ";
5684
5685 if(subtype.id()==ID_bool && !use_array_of_bool)
5686 out << "(_ BitVec 1)";
5687 else
5688 convert_type(array_type.element_type());
5689
5690 out << ")";
5691 }
5692 else if(type.id()==ID_bool)
5693 {
5694 out << "Bool";
5695 }
5696 else if(type.id() == ID_struct || type.id() == ID_struct_tag)
5697 {
5698 if(use_datatypes)
5699 {
5700 out << datatype_map.at(type);
5701 }
5702 else
5703 {
5704 std::size_t width=boolbv_width(type);
5705
5706 out << "(_ BitVec " << width << ")";
5707 }
5708 }
5709 else if(type.id()==ID_code)
5710 {
5711 // These may appear in structs.
5712 // We replace this by "Bool" in order to keep the same
5713 // member count.
5714 out << "Bool";
5715 }
5716 else if(type.id() == ID_union || type.id() == ID_union_tag)
5717 {
5718 std::size_t width=boolbv_width(type);
5719 const union_typet &union_type = type.id() == ID_union_tag
5720 ? ns.follow_tag(to_union_tag_type(type))
5721 : to_union_type(type);
5723 union_type.components().empty() || width != 0,
5724 "failed to get width of union");
5725
5726 out << "(_ BitVec " << width << ")";
5727 }
5728 else if(type.id()==ID_pointer)
5729 {
5730 out << "(_ BitVec "
5731 << boolbv_width(type) << ")";
5732 }
5733 else if(type.id()==ID_bv ||
5734 type.id()==ID_fixedbv ||
5735 type.id()==ID_unsignedbv ||
5736 type.id()==ID_signedbv ||
5737 type.id()==ID_c_bool)
5738 {
5739 out << "(_ BitVec "
5740 << to_bitvector_type(type).get_width() << ")";
5741 }
5742 else if(type.id()==ID_c_enum)
5743 {
5744 // these have an underlying type
5745 out << "(_ BitVec "
5746 << to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width()
5747 << ")";
5748 }
5749 else if(type.id()==ID_c_enum_tag)
5750 {
5751 convert_type(ns.follow_tag(to_c_enum_tag_type(type)));
5752 }
5753 else if(type.id()==ID_floatbv)
5754 {
5755 const floatbv_typet &floatbv_type=to_floatbv_type(type);
5756
5757 if(use_FPA_theory)
5758 out << "(_ FloatingPoint "
5759 << floatbv_type.get_e() << " "
5760 << floatbv_type.get_f() + 1 << ")";
5761 else
5762 out << "(_ BitVec "
5763 << floatbv_type.get_width() << ")";
5764 }
5765 else if(type.id()==ID_rational ||
5766 type.id()==ID_real)
5767 out << "Real";
5768 else if(type.id()==ID_integer)
5769 out << "Int";
5770 else if(type.id()==ID_complex)
5771 {
5772 if(use_datatypes)
5773 {
5774 out << datatype_map.at(type);
5775 }
5776 else
5777 {
5778 std::size_t width=boolbv_width(type);
5779
5780 out << "(_ BitVec " << width << ")";
5781 }
5782 }
5783 else if(type.id()==ID_c_bit_field)
5784 {
5786 }
5787 else if(type.id() == ID_state)
5788 {
5789 out << "state";
5790 }
5791 else if(type.id() == ID_range)
5792 {
5793 auto &range_type = to_range_type(type);
5794 mp_integer size = range_type.get_to() - range_type.get_from() + 1;
5795 if(size <= 0)
5796 UNEXPECTEDCASE("unsuppored range type");
5797 out << "(_ BitVec " << address_bits(size) << ")";
5798 }
5799 else
5800 {
5801 UNEXPECTEDCASE("unsupported type: "+type.id_string());
5802 }
5803}
5804
5806{
5807 std::set<irep_idt> recstack;
5808 find_symbols_rec(type, recstack);
5809}
5810
5812 const typet &type,
5813 std::set<irep_idt> &recstack)
5814{
5815 if(type.id()==ID_array)
5816 {
5817 const array_typet &array_type=to_array_type(type);
5818 find_symbols(array_type.size());
5819 find_symbols_rec(array_type.element_type(), recstack);
5820 }
5821 else if(type.id()==ID_complex)
5822 {
5823 find_symbols_rec(to_complex_type(type).subtype(), recstack);
5824
5825 if(use_datatypes &&
5826 datatype_map.find(type)==datatype_map.end())
5827 {
5828 const std::string smt_typename =
5829 "complex." + std::to_string(datatype_map.size());
5830 datatype_map[type] = smt_typename;
5831
5832 out << "(declare-datatypes ((" << smt_typename << " 0)) "
5833 << "(((mk-" << smt_typename;
5834
5835 out << " (" << smt_typename << ".imag ";
5836 convert_type(to_complex_type(type).subtype());
5837 out << ")";
5838
5839 out << " (" << smt_typename << ".real ";
5840 convert_type(to_complex_type(type).subtype());
5841 out << ")";
5842
5843 out << "))))\n";
5844 }
5845 }
5846 else if(type.id() == ID_struct)
5847 {
5848 // Cater for mutually recursive struct types
5849 bool need_decl=false;
5850 if(use_datatypes &&
5851 datatype_map.find(type)==datatype_map.end())
5852 {
5853 const std::string smt_typename =
5854 "struct." + std::to_string(datatype_map.size());
5855 datatype_map[type] = smt_typename;
5856 need_decl=true;
5857 }
5858
5859 const struct_typet::componentst &components =
5860 to_struct_type(type).components();
5861
5862 for(const auto &component : components)
5863 find_symbols_rec(component.type(), recstack);
5864
5865 // Declare the corresponding SMT type if we haven't already.
5866 if(need_decl)
5867 {
5868 const std::string &smt_typename = datatype_map.at(type);
5869
5870 // We're going to create a datatype named something like `struct.0'.
5871 // It's going to have a single constructor named `mk-struct.0' with an
5872 // argument for each member of the struct. The declaration that
5873 // creates this type looks like:
5874 //
5875 // (declare-datatypes ((struct.0 0)) (((mk-struct.0
5876 // (struct.0.component1 type1)
5877 // ...
5878 // (struct.0.componentN typeN)))))
5879 out << "(declare-datatypes ((" << smt_typename << " 0)) "
5880 << "(((mk-" << smt_typename << " ";
5881
5882 for(const auto &component : components)
5883 {
5884 if(is_zero_width(component.type(), ns))
5885 continue;
5886
5887 out << "(" << smt_typename << "." << component.get_name()
5888 << " ";
5889 convert_type(component.type());
5890 out << ") ";
5891 }
5892
5893 out << "))))" << "\n";
5894
5895 // Let's also declare convenience functions to update individual
5896 // members of the struct whil we're at it. The functions are
5897 // named like `update-struct.0.component1'. Their declarations
5898 // look like:
5899 //
5900 // (declare-fun update-struct.0.component1
5901 // ((s struct.0) ; first arg -- the struct to update
5902 // (v type1)) ; second arg -- the value to update
5903 // struct.0 ; the output type
5904 // (mk-struct.0 ; build the new struct...
5905 // v ; the updated value
5906 // (struct.0.component2 s) ; retain the other members
5907 // ...
5908 // (struct.0.componentN s)))
5909
5910 for(struct_union_typet::componentst::const_iterator
5911 it=components.begin();
5912 it!=components.end();
5913 ++it)
5914 {
5915 if(is_zero_width(it->type(), ns))
5916 continue;
5917
5919 out << "(define-fun update-" << smt_typename << "."
5920 << component.get_name() << " "
5921 << "((s " << smt_typename << ") "
5922 << "(v ";
5923 convert_type(component.type());
5924 out << ")) " << smt_typename << " "
5925 << "(mk-" << smt_typename
5926 << " ";
5927
5928 for(struct_union_typet::componentst::const_iterator
5929 it2=components.begin();
5930 it2!=components.end();
5931 ++it2)
5932 {
5933 if(it==it2)
5934 out << "v ";
5935 else if(!is_zero_width(it2->type(), ns))
5936 {
5937 out << "(" << smt_typename << "."
5938 << it2->get_name() << " s) ";
5939 }
5940 }
5941
5942 out << "))" << "\n";
5943 }
5944
5945 out << "\n";
5946 }
5947 }
5948 else if(type.id() == ID_union)
5949 {
5950 const union_typet::componentst &components =
5951 to_union_type(type).components();
5952
5953 for(const auto &component : components)
5954 find_symbols_rec(component.type(), recstack);
5955 }
5956 else if(type.id()==ID_code)
5957 {
5958 const code_typet::parameterst &parameters=
5959 to_code_type(type).parameters();
5960 for(const auto &param : parameters)
5961 find_symbols_rec(param.type(), recstack);
5962
5963 find_symbols_rec(to_code_type(type).return_type(), recstack);
5964 }
5965 else if(type.id()==ID_pointer)
5966 {
5967 find_symbols_rec(to_pointer_type(type).base_type(), recstack);
5968 }
5969 else if(type.id() == ID_struct_tag)
5970 {
5971 const auto &struct_tag = to_struct_tag_type(type);
5972 const irep_idt &id = struct_tag.get_identifier();
5973
5974 if(recstack.find(id) == recstack.end())
5975 {
5976 const auto &base_struct = ns.follow_tag(struct_tag);
5977 recstack.insert(id);
5978 find_symbols_rec(base_struct, recstack);
5979 datatype_map[type] = datatype_map[base_struct];
5980 }
5981 }
5982 else if(type.id() == ID_union_tag)
5983 {
5984 const auto &union_tag = to_union_tag_type(type);
5985 const irep_idt &id = union_tag.get_identifier();
5986
5987 if(recstack.find(id) == recstack.end())
5988 {
5989 recstack.insert(id);
5990 find_symbols_rec(ns.follow_tag(union_tag), recstack);
5991 }
5992 }
5993 else if(type.id() == ID_state)
5994 {
5995 if(datatype_map.find(type) == datatype_map.end())
5996 {
5997 datatype_map[type] = "state";
5998 out << "(declare-sort state 0)\n";
5999 }
6000 }
6001 else if(type.id() == ID_mathematical_function)
6002 {
6003 const auto &mathematical_function_type =
6005 for(auto &d_type : mathematical_function_type.domain())
6006 find_symbols_rec(d_type, recstack);
6007
6008 find_symbols_rec(mathematical_function_type.codomain(), recstack);
6009 }
6010}
6011
6013{
6015}
configt config
Definition config.cpp:25
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)
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
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.
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
API to expression classes for bitvectors.
const onehot0_exprt & to_onehot0_expr(const exprt &expr)
Cast an exprt to a onehot0_exprt.
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 update_bits_exprt & to_update_bits_expr(const exprt &expr)
Cast an exprt to an update_bits_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const onehot_exprt & to_onehot_expr(const exprt &expr)
Cast an exprt to a onehot_exprt.
bool can_cast_expr< minus_overflow_exprt >(const exprt &base)
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
bool can_cast_expr< overflow_result_exprt >(const exprt &base)
const update_bit_exprt & to_update_bit_expr(const exprt &expr)
Cast an exprt to an update_bit_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 zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_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.
bool has_byte_operator(const exprt &src)
Return true iff src or one of its operands contain a byte extract or byte update expression.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
Rewrite a byte update expression to more fundamental operations.
int16_t s2
int8_t s1
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
unsignedbv_typet size_type()
Definition c_types.cpp:50
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
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:80
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
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:377
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition c_types.h:128
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
Absolute value.
Definition std_expr.h:442
Operator to return the address of an object.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
Array constructor from list of elements.
Definition std_expr.h:1621
Arrays with given size.
Definition std_types.h:807
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:34
const exprt & size() const
Definition std_types.h:840
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
A base class for binary expressions.
Definition std_expr.h:638
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
exprt & where()
Definition std_expr.h:3266
variablest & variables()
Definition std_expr.h:3256
Bit-wise negation of bit-vectors.
std::size_t get_width() const
Definition std_types.h:925
The Boolean type.
Definition std_types.h:36
The byte swap expression.
std::size_t get_bits_per_byte() const
std::vector< parametert > parameterst
Definition std_types.h:586
const parameterst & parameters() const
Definition std_types.h:699
A constant literal expression.
Definition std_expr.h:3118
const irep_idt & get_value() const
Definition std_expr.h:3126
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition std_expr.cpp:25
resultt
Result of running the decision procedure.
Division.
Definition std_expr.h:1157
bool empty() const
Definition dstring.h:89
Equality.
Definition std_expr.h:1366
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1296
exprt & op0()
Definition expr.h:133
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:91
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
depth_iteratort depth_end()
Definition expr.cpp:249
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
depth_iteratort depth_begin()
Definition expr.cpp:247
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
void visit_post(std::function< void(exprt &)>)
These are post-order traversal visitors, i.e., the visitor is executed on a node after its children h...
Definition expr.cpp:198
operandst & operands()
Definition expr.h:94
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:3200
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
Round a floating-point number to an integral value considering the given rounding mode.
Semantic type conversion from/to floating-point formats.
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)...
std::size_t f
Definition ieee_float.h:26
std::size_t width() const
Definition ieee_float.h:50
An IEEE 754 floating-point value, including specificiation.
Definition ieee_float.h:117
static ieee_float_valuet minus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:209
bool is_NaN() const
Definition ieee_float.h:259
static ieee_float_valuet one(const floatbv_typet &)
ieee_float_spect spec
Definition ieee_float.h:119
constant_exprt to_expr() const
mp_integer pack() const
bool get_sign() const
Definition ieee_float.h:254
static ieee_float_valuet zero(const floatbv_typet &type)
Definition ieee_float.h:172
static ieee_float_valuet NaN(const ieee_float_spect &_spec)
Definition ieee_float.h:195
static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:202
bool is_infinity() const
Definition ieee_float.h:260
The trinary if-then-else operator.
Definition std_expr.h:2502
exprt & cond()
Definition std_expr.h:2519
exprt & false_case()
Definition std_expr.h:2539
exprt & true_case()
Definition std_expr.h:2529
Boolean implication.
Definition std_expr.h:2230
Array index operator.
Definition std_expr.h:1470
exprt & index()
Definition std_expr.h:1510
exprt & array()
Definition std_expr.h:1500
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
bool is_not_nil() const
Definition irep.h:372
const std::string & id_string() const
Definition irep.h:391
subt & get_sub()
Definition irep.h:448
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
A let expression.
Definition std_expr.h:3332
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3413
operandst & values()
Definition std_expr.h:3402
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3425
literalt get_literal() const
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:2972
const exprt & struct_op() const
Definition std_expr.h:3010
irep_idt get_component_name() const
Definition std_expr.h:2994
Binary minus.
Definition std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1228
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
exprt & op1()
Definition std_expr.h:938
exprt & op0()
Definition std_expr.h:932
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
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:3209
const irep_idt & get_identifier() const
Definition std_expr.h:320
Boolean negation.
Definition std_expr.h:2459
Disequality.
Definition std_expr.h:1425
Expression for finding the size (in bytes) of the object a pointer points to.
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
A base class for quantifier expressions.
Bit-vector replication.
constant_exprt & times()
A base class for shift and rotate operators.
exprt & distance()
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:596
const irep_idt & get_identifier() const
Definition smt2_conv.h:219
void convert_relation(const binary_relation_exprt &)
bool use_lambda_for_array
Definition smt2_conv.h:72
void convert_type(const typet &)
void unflatten(wheret, const typet &, unsigned nesting=0)
bool use_array_theory(const exprt &)
void find_symbols(const exprt &expr)
std::size_t number_of_solver_calls
Definition smt2_conv.h:111
void convert_typecast(const typecast_exprt &expr)
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
tvt l_get(literalt l) const
std::string benchmark
Definition smt2_conv.h:102
void convert_floatbv_rem(const binary_exprt &expr)
std::unordered_map< irep_idt, irept > current_bindings
Definition smt2_conv.h:200
bool use_FPA_theory
Definition smt2_conv.h:67
resultt dec_solve(const exprt &) override
Implementation of the decision procedure.
std::set< irep_idt > bvfp_set
Definition smt2_conv.h:206
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
void push() override
Unimplemented.
void convert_is_dynamic_object(const unary_exprt &)
void convert_literal(const literalt)
void convert_floatbv_div(const ieee_float_op_exprt &expr)
void convert_string_literal(const std::string &)
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
const namespacet & ns
Definition smt2_conv.h:100
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
boolbv_widtht boolbv_width
Definition smt2_conv.h:109
void convert_constant(const constant_exprt &expr)
std::string floatbv_suffix(const exprt &) const
void flatten2bv(const exprt &)
std::string notes
Definition smt2_conv.h:102
void convert_div(const div_exprt &expr)
std::ostream & out
Definition smt2_conv.h:101
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
std::string type2id(const typet &) const
bool emit_set_logic
Definition smt2_conv.h:73
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
struct_exprt parse_struct(const irept &s, const struct_typet &type)
std::string logic
Definition smt2_conv.h:102
void convert_mult(const mult_exprt &expr)
void convert_update_bit(const update_bit_exprt &)
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
bool use_check_sat_assuming
Definition smt2_conv.h:70
std::map< object_size_exprt, irep_idt > object_sizes
Definition smt2_conv.h:287
void define_object_size(const irep_idt &id, const object_size_exprt &expr)
bool use_datatypes
Definition smt2_conv.h:71
datatype_mapt datatype_map
Definition smt2_conv.h:272
void convert_mod(const mod_exprt &expr)
static std::string convert_identifier(const irep_idt &identifier)
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
void convert_struct(const struct_exprt &expr)
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:285
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:56
void convert_member(const member_exprt &expr)
void convert_euclidean_mod(const euclidean_mod_exprt &expr)
void convert_index(const index_exprt &expr)
converterst converters
Definition smt2_conv.h:106
pointer_logict pointer_logic
Definition smt2_conv.h:240
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...
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
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.
void convert_floatbv_round_to_integral(const floatbv_round_to_integral_exprt &)
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'.
bool use_as_const
Definition smt2_conv.h:69
exprt parse_rec(const irept &s, const typet &type)
void convert_union(const union_exprt &expr)
exprt parse_union(const irept &s, const union_typet &type)
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 ...
std::vector< bool > boolean_assignment
Definition smt2_conv.h:294
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
void convert_with(const with_exprt &expr)
letifyt letify
Definition smt2_conv.h:177
bool use_array_of_bool
Definition smt2_conv.h:68
std::vector< literalt > assumptions
Definition smt2_conv.h:108
void convert_plus(const plus_exprt &expr)
defined_expressionst defined_expressions
Definition smt2_conv.h:281
void pop() override
Currently, only implements a single stack element (no nested contexts)
void convert_update_bits(const update_bits_exprt &)
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
void convert_update(const update_exprt &)
void write_header()
std::set< irep_idt > state_fkt_declared
Definition smt2_conv.h:210
solvert solver
Definition smt2_conv.h:103
identifier_mapt identifier_map
Definition smt2_conv.h:265
void convert_minus(const minus_exprt &expr)
void convert_expr(const exprt &)
constant_exprt parse_literal(const irept &, const typet &type)
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
Definition smt2_conv.h:225
std::size_t no_boolean_variables
Definition smt2_conv.h:293
smt2_identifierst smt2_identifiers
Definition smt2_conv.h:290
void convert_floatbv(const exprt &expr)
literalt convert(const exprt &expr)
array_exprt to_array_expr() const
convert string into array constant
Struct constructor from list of elements.
Definition std_expr.h:1877
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:64
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:160
The Boolean constant true.
Definition std_expr.h:3191
Definition threeval.h:20
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
const exprt & op() const
Definition std_expr.h:391
The unary minus expression.
Definition std_expr.h:484
Union constructor from single element.
Definition std_expr.h:1770
The union type.
Definition c_types.h:147
Fixed-width bit-vector with unsigned binary interpretation.
Replaces a sub-range of a bit-vector operand.
exprt lower() const
A lowering to masking, shifting, or.
Replaces a sub-range of a bit-vector operand.
exprt lower() const
A lowering to masking, shifting, or.
Operator to update elements in structs and arrays.
Definition std_expr.h:2783
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
exprt & new_value()
Definition std_expr.h:2633
exprt & where()
Definition std_expr.h:2623
exprt & old()
Definition std_expr.h:2613
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
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:38
Deprecated expression utility functions.
exprt float_bv(const exprt &src)
Definition float_bv.h:188
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.
const floatbv_round_to_integral_exprt & to_floatbv_round_to_integral_expr(const exprt &expr)
Cast an exprt to a floatbv_round_to_integral_exprt.
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
static format_containert< T > format(const T &o)
Definition format.h:37
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
static std::string binary(const constant_exprt &src)
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &src)
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.
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
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
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, 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:522
exprt simplify_expr(exprt src, const namespacet &ns)
static bool has_quantifier(const exprt &expr)
#define SMT2_TODO(S)
Definition smt2_conv.cpp:54
static bool is_zero_width(const typet &type, const namespacet &ns)
Returns true iff type has effective width of zero bits.
static bool is_smt2_simple_identifier(const std::string &identifier)
#define UNEXPECTEDCASE(S)
Definition smt2_conv.cpp:51
bool is_smt2_simple_symbol_character(char ch)
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define UNIMPLEMENTED
Definition invariant.h:558
#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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:496
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition invariant.h:535
#define UNREACHABLE_BECAUSE(REASON)
Definition invariant.h:526
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:122
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1900
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1603
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:895
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition std_expr.h:556
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1277
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1137
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3611
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
Definition std_expr.h:116
const named_term_exprt & to_named_term_expr(const exprt &expr)
Cast an exprt to a named_term_exprt.
Definition std_expr.h:3793
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition std_expr.h:3518
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1206
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition std_expr.h:1450
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3456
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition std_expr.h:466
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2582
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1086
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1816
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3173
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2484
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2661
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2255
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2866
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:514
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition std_expr.h:343
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition std_expr.h:621
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition std_expr.h:1345
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_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:788
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:518
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
std::size_t unsafe_string2size_t(const std::string &str, int base)
const string_constantt & to_string_constant(const exprt &expr)
dstringt irep_idt