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