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)
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_function_application)
2460 {
2461 const auto &function_application_expr = to_function_application_expr(expr);
2462 // do not use parentheses if there function is a constant
2463 if(function_application_expr.arguments().empty())
2464 {
2465 convert_expr(function_application_expr.function());
2466 }
2467 else
2468 {
2469 out << '(';
2470 convert_expr(function_application_expr.function());
2471 for(auto &op : function_application_expr.arguments())
2472 {
2473 out << ' ';
2474 convert_expr(op);
2475 }
2476 out << ')';
2477 }
2478 }
2479 else
2481 false,
2482 "smt2_convt::convert_expr should not be applied to unsupported type",
2483 expr.id_string());
2484}
2485
2487{
2488 const exprt &src = expr.op();
2489
2490 typet dest_type = expr.type();
2491 if(dest_type.id()==ID_c_enum_tag)
2492 dest_type=ns.follow_tag(to_c_enum_tag_type(dest_type));
2493
2494 typet src_type = src.type();
2495 if(src_type.id()==ID_c_enum_tag)
2496 src_type=ns.follow_tag(to_c_enum_tag_type(src_type));
2497
2498 if(dest_type.id()==ID_bool)
2499 {
2500 // this is comparison with zero
2501 if(src_type.id()==ID_signedbv ||
2502 src_type.id()==ID_unsignedbv ||
2503 src_type.id()==ID_c_bool ||
2504 src_type.id()==ID_fixedbv ||
2505 src_type.id()==ID_pointer ||
2506 src_type.id()==ID_integer)
2507 {
2508 out << "(not (= ";
2509 convert_expr(src);
2510 out << " ";
2511 convert_expr(from_integer(0, src_type));
2512 out << "))";
2513 }
2514 else if(src_type.id()==ID_floatbv)
2515 {
2516 if(use_FPA_theory)
2517 {
2518 out << "(not (fp.isZero ";
2519 convert_expr(src);
2520 out << "))";
2521 }
2522 else
2523 convert_floatbv(expr);
2524 }
2525 else
2526 {
2527 UNEXPECTEDCASE("TODO typecast1 "+src_type.id_string()+" -> bool");
2528 }
2529 }
2530 else if(dest_type.id()==ID_c_bool)
2531 {
2532 std::size_t to_width=boolbv_width(dest_type);
2533 out << "(ite ";
2534 out << "(not (= ";
2535 convert_expr(src);
2536 out << " ";
2537 convert_expr(from_integer(0, src_type));
2538 out << "))"; // not, =
2539 out << " (_ bv1 " << to_width << ")";
2540 out << " (_ bv0 " << to_width << ")";
2541 out << ")"; // ite
2542 }
2543 else if(dest_type.id()==ID_signedbv ||
2544 dest_type.id()==ID_unsignedbv ||
2545 dest_type.id()==ID_c_enum ||
2546 dest_type.id()==ID_bv)
2547 {
2548 std::size_t to_width=boolbv_width(dest_type);
2549
2550 if(src_type.id()==ID_signedbv || // from signedbv
2551 src_type.id()==ID_unsignedbv || // from unsigedbv
2552 src_type.id()==ID_c_bool ||
2553 src_type.id()==ID_c_enum ||
2554 src_type.id()==ID_bv)
2555 {
2556 std::size_t from_width=boolbv_width(src_type);
2557
2558 if(from_width==to_width)
2559 convert_expr(src); // ignore
2560 else if(from_width<to_width) // extend
2561 {
2562 if(src_type.id()==ID_signedbv)
2563 out << "((_ sign_extend ";
2564 else
2565 out << "((_ zero_extend ";
2566
2567 out << (to_width-from_width)
2568 << ") "; // ind
2569 convert_expr(src);
2570 out << ")";
2571 }
2572 else // chop off extra bits
2573 {
2574 out << "((_ extract " << (to_width-1) << " 0) ";
2575 convert_expr(src);
2576 out << ")";
2577 }
2578 }
2579 else if(src_type.id()==ID_fixedbv) // from fixedbv to int
2580 {
2581 const fixedbv_typet &fixedbv_type=to_fixedbv_type(src_type);
2582
2583 std::size_t from_width=fixedbv_type.get_width();
2584 std::size_t from_integer_bits=fixedbv_type.get_integer_bits();
2585 std::size_t from_fraction_bits=fixedbv_type.get_fraction_bits();
2586
2587 // we might need to round up in case of negative numbers
2588 // e.g., (int)(-1.00001)==1
2589
2590 out << "(let ((?tcop ";
2591 convert_expr(src);
2592 out << ")) ";
2593
2594 out << "(bvadd ";
2595
2596 if(to_width>from_integer_bits)
2597 {
2598 out << "((_ sign_extend "
2599 << (to_width-from_integer_bits) << ") ";
2600 out << "((_ extract " << (from_width-1) << " "
2601 << from_fraction_bits << ") ";
2602 convert_expr(src);
2603 out << "))";
2604 }
2605 else
2606 {
2607 out << "((_ extract " << (from_fraction_bits+to_width-1)
2608 << " " << from_fraction_bits << ") ";
2609 convert_expr(src);
2610 out << ")";
2611 }
2612
2613 out << " (ite (and ";
2614
2615 // some fraction bit is not zero
2616 out << "(not (= ((_ extract " << (from_fraction_bits-1) << " 0) ?tcop) "
2617 "(_ bv0 " << from_fraction_bits << ")))";
2618
2619 // number negative
2620 out << " (= ((_ extract " << (from_width-1) << " " << (from_width-1)
2621 << ") ?tcop) #b1)";
2622
2623 out << ")"; // and
2624
2625 out << " (_ bv1 " << to_width << ") (_ bv0 " << to_width << "))"; // ite
2626 out << ")"; // bvadd
2627 out << ")"; // let
2628 }
2629 else if(src_type.id()==ID_floatbv) // from floatbv to int
2630 {
2631 if(dest_type.id()==ID_bv)
2632 {
2633 // this is _NOT_ a semantic conversion, but bit-wise
2634
2635 if(use_FPA_theory)
2636 {
2637 defined_expressionst::const_iterator it =
2638 defined_expressions.find(expr);
2639 CHECK_RETURN(it != defined_expressions.end());
2640 out << it->second;
2641 }
2642 else
2643 {
2644 // straight-forward if width matches
2645 convert_expr(src);
2646 }
2647 }
2648 else if(dest_type.id()==ID_signedbv)
2649 {
2650 // this should be floatbv_typecast, not typecast
2652 "typecast unexpected "+src_type.id_string()+" -> "+
2653 dest_type.id_string());
2654 }
2655 else if(dest_type.id()==ID_unsignedbv)
2656 {
2657 // this should be floatbv_typecast, not typecast
2659 "typecast unexpected "+src_type.id_string()+" -> "+
2660 dest_type.id_string());
2661 }
2662 }
2663 else if(src_type.id()==ID_bool) // from boolean to int
2664 {
2665 out << "(ite ";
2666 convert_expr(src);
2667
2668 if(dest_type.id()==ID_fixedbv)
2669 {
2670 fixedbv_spect spec(to_fixedbv_type(dest_type));
2671 out << " (concat (_ bv1 "
2672 << spec.integer_bits << ") " <<
2673 "(_ bv0 " << spec.get_fraction_bits() << ")) " <<
2674 "(_ bv0 " << spec.width << ")";
2675 }
2676 else
2677 {
2678 out << " (_ bv1 " << to_width << ")";
2679 out << " (_ bv0 " << to_width << ")";
2680 }
2681
2682 out << ")";
2683 }
2684 else if(src_type.id()==ID_pointer) // from pointer to int
2685 {
2686 std::size_t from_width=boolbv_width(src_type);
2687
2688 if(from_width<to_width) // extend
2689 {
2690 out << "((_ sign_extend ";
2691 out << (to_width-from_width)
2692 << ") ";
2693 convert_expr(src);
2694 out << ")";
2695 }
2696 else // chop off extra bits
2697 {
2698 out << "((_ extract " << (to_width-1) << " 0) ";
2699 convert_expr(src);
2700 out << ")";
2701 }
2702 }
2703 else if(src_type.id()==ID_integer) // from integer to bit-vector
2704 {
2705 // must be constant
2706 if(src.is_constant())
2707 {
2709 out << "(_ bv" << i << " " << to_width << ")";
2710 }
2711 else
2712 SMT2_TODO("can't convert non-constant integer to bitvector");
2713 }
2714 else if(
2715 src_type.id() == ID_struct ||
2716 src_type.id() == ID_struct_tag) // flatten a struct to a bit-vector
2717 {
2718 if(use_datatypes)
2719 {
2720 INVARIANT(
2721 boolbv_width(src_type) == boolbv_width(dest_type),
2722 "bit vector with of source and destination type shall be equal");
2723 flatten2bv(src);
2724 }
2725 else
2726 {
2727 INVARIANT(
2728 boolbv_width(src_type) == boolbv_width(dest_type),
2729 "bit vector with of source and destination type shall be equal");
2730 convert_expr(src); // nothing else to do!
2731 }
2732 }
2733 else if(
2734 src_type.id() == ID_union ||
2735 src_type.id() == ID_union_tag) // flatten a union
2736 {
2737 INVARIANT(
2738 boolbv_width(src_type) == boolbv_width(dest_type),
2739 "bit vector with of source and destination type shall be equal");
2740 convert_expr(src); // nothing else to do!
2741 }
2742 else if(src_type.id()==ID_c_bit_field)
2743 {
2744 std::size_t from_width=boolbv_width(src_type);
2745
2746 if(from_width==to_width)
2747 convert_expr(src); // ignore
2748 else
2749 {
2751 typecast_exprt tmp(typecast_exprt(src, t), dest_type);
2752 convert_typecast(tmp);
2753 }
2754 }
2755 else
2756 {
2757 std::ostringstream e_str;
2758 e_str << src_type.id() << " -> " << dest_type.id()
2759 << " src == " << format(src);
2760 UNEXPECTEDCASE("TODO typecast2 " + e_str.str());
2761 }
2762 }
2763 else if(dest_type.id()==ID_fixedbv) // to fixedbv
2764 {
2765 const fixedbv_typet &fixedbv_type=to_fixedbv_type(dest_type);
2766 std::size_t to_fraction_bits=fixedbv_type.get_fraction_bits();
2767 std::size_t to_integer_bits=fixedbv_type.get_integer_bits();
2768
2769 if(src_type.id()==ID_unsignedbv ||
2770 src_type.id()==ID_signedbv ||
2771 src_type.id()==ID_c_enum)
2772 {
2773 // integer to fixedbv
2774
2775 std::size_t from_width=to_bitvector_type(src_type).get_width();
2776 out << "(concat ";
2777
2778 if(from_width==to_integer_bits)
2779 convert_expr(src);
2780 else if(from_width>to_integer_bits)
2781 {
2782 // too many integer bits
2783 out << "((_ extract " << (to_integer_bits-1) << " 0) ";
2784 convert_expr(src);
2785 out << ")";
2786 }
2787 else
2788 {
2789 // too few integer bits
2790 INVARIANT(
2791 from_width < to_integer_bits,
2792 "from_width should be smaller than to_integer_bits as other case "
2793 "have been handled above");
2794 if(dest_type.id()==ID_unsignedbv)
2795 {
2796 out << "(_ zero_extend "
2797 << (to_integer_bits-from_width) << ") ";
2798 convert_expr(src);
2799 out << ")";
2800 }
2801 else
2802 {
2803 out << "((_ sign_extend "
2804 << (to_integer_bits-from_width) << ") ";
2805 convert_expr(src);
2806 out << ")";
2807 }
2808 }
2809
2810 out << "(_ bv0 " << to_fraction_bits << ")";
2811 out << ")"; // concat
2812 }
2813 else if(src_type.id()==ID_bool) // bool to fixedbv
2814 {
2815 out << "(concat (concat"
2816 << " (_ bv0 " << (to_integer_bits-1) << ") ";
2817 flatten2bv(src); // produces #b0 or #b1
2818 out << ") (_ bv0 "
2819 << to_fraction_bits
2820 << "))";
2821 }
2822 else if(src_type.id()==ID_fixedbv) // fixedbv to fixedbv
2823 {
2824 const fixedbv_typet &from_fixedbv_type=to_fixedbv_type(src_type);
2825 std::size_t from_fraction_bits=from_fixedbv_type.get_fraction_bits();
2826 std::size_t from_integer_bits=from_fixedbv_type.get_integer_bits();
2827 std::size_t from_width=from_fixedbv_type.get_width();
2828
2829 out << "(let ((?tcop ";
2830 convert_expr(src);
2831 out << ")) ";
2832
2833 out << "(concat ";
2834
2835 if(to_integer_bits<=from_integer_bits)
2836 {
2837 out << "((_ extract "
2838 << (from_fraction_bits+to_integer_bits-1) << " "
2839 << from_fraction_bits
2840 << ") ?tcop)";
2841 }
2842 else
2843 {
2844 INVARIANT(
2845 to_integer_bits > from_integer_bits,
2846 "to_integer_bits should be greater than from_integer_bits as the"
2847 "other case has been handled above");
2848 out << "((_ sign_extend "
2849 << (to_integer_bits-from_integer_bits)
2850 << ") ((_ extract "
2851 << (from_width-1) << " "
2852 << from_fraction_bits
2853 << ") ?tcop))";
2854 }
2855
2856 out << " ";
2857
2858 if(to_fraction_bits<=from_fraction_bits)
2859 {
2860 out << "((_ extract "
2861 << (from_fraction_bits-1) << " "
2862 << (from_fraction_bits-to_fraction_bits)
2863 << ") ?tcop)";
2864 }
2865 else
2866 {
2867 INVARIANT(
2868 to_fraction_bits > from_fraction_bits,
2869 "to_fraction_bits should be greater than from_fraction_bits as the"
2870 "other case has been handled above");
2871 out << "(concat ((_ extract "
2872 << (from_fraction_bits-1) << " 0) ";
2873 convert_expr(src);
2874 out << ")"
2875 << " (_ bv0 " << to_fraction_bits-from_fraction_bits
2876 << "))";
2877 }
2878
2879 out << "))"; // concat, let
2880 }
2881 else
2882 UNEXPECTEDCASE("unexpected typecast to fixedbv");
2883 }
2884 else if(dest_type.id()==ID_pointer)
2885 {
2886 std::size_t to_width=boolbv_width(dest_type);
2887
2888 if(src_type.id()==ID_pointer) // pointer to pointer
2889 {
2890 // this just passes through
2891 convert_expr(src);
2892 }
2893 else if(
2894 src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv ||
2895 src_type.id() == ID_bv)
2896 {
2897 // integer to pointer
2898
2899 std::size_t from_width=boolbv_width(src_type);
2900
2901 if(from_width==to_width)
2902 convert_expr(src);
2903 else if(from_width<to_width)
2904 {
2905 out << "((_ sign_extend "
2906 << (to_width-from_width)
2907 << ") ";
2908 convert_expr(src);
2909 out << ")"; // sign_extend
2910 }
2911 else // from_width>to_width
2912 {
2913 out << "((_ extract " << to_width << " 0) ";
2914 convert_expr(src);
2915 out << ")"; // extract
2916 }
2917 }
2918 else
2919 UNEXPECTEDCASE("TODO typecast3 "+src_type.id_string()+" -> pointer");
2920 }
2921 else if(dest_type.id()==ID_range)
2922 {
2923 SMT2_TODO("range typecast");
2924 }
2925 else if(dest_type.id()==ID_floatbv)
2926 {
2927 // Typecast from integer to floating-point should have be been
2928 // converted to ID_floatbv_typecast during symbolic execution,
2929 // adding the rounding mode. See
2930 // smt2_convt::convert_floatbv_typecast.
2931 // The exception is bool and c_bool to float.
2932 const auto &dest_floatbv_type = to_floatbv_type(dest_type);
2933
2934 if(src_type.id()==ID_bool)
2935 {
2936 constant_exprt val(irep_idt(), dest_type);
2937
2938 ieee_floatt a(dest_floatbv_type);
2939
2940 mp_integer significand;
2941 mp_integer exponent;
2942
2943 out << "(ite ";
2944 convert_expr(src);
2945 out << " ";
2946
2947 significand = 1;
2948 exponent = 0;
2949 a.build(significand, exponent);
2950 val.set_value(integer2bvrep(a.pack(), a.spec.width()));
2951
2952 convert_constant(val);
2953 out << " ";
2954
2955 significand = 0;
2956 exponent = 0;
2957 a.build(significand, exponent);
2958 val.set_value(integer2bvrep(a.pack(), a.spec.width()));
2959
2960 convert_constant(val);
2961 out << ")";
2962 }
2963 else if(src_type.id()==ID_c_bool)
2964 {
2965 // turn into proper bool
2966 const typecast_exprt tmp(src, bool_typet());
2967 convert_typecast(typecast_exprt(tmp, dest_type));
2968 }
2969 else if(src_type.id() == ID_bv)
2970 {
2971 if(to_bv_type(src_type).get_width() != dest_floatbv_type.get_width())
2972 {
2973 UNEXPECTEDCASE("Typecast bv -> float with wrong width");
2974 }
2975
2976 if(use_FPA_theory)
2977 {
2978 out << "((_ to_fp " << dest_floatbv_type.get_e() << " "
2979 << dest_floatbv_type.get_f() + 1 << ") ";
2980 convert_expr(src);
2981 out << ')';
2982 }
2983 else
2984 convert_expr(src);
2985 }
2986 else
2987 UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
2988 }
2989 else if(dest_type.id()==ID_integer)
2990 {
2991 if(src_type.id()==ID_bool)
2992 {
2993 out << "(ite ";
2994 convert_expr(src);
2995 out <<" 1 0)";
2996 }
2997 else
2998 UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer");
2999 }
3000 else if(dest_type.id()==ID_c_bit_field)
3001 {
3002 std::size_t from_width=boolbv_width(src_type);
3003 std::size_t to_width=boolbv_width(dest_type);
3004
3005 if(from_width==to_width)
3006 convert_expr(src); // ignore
3007 else
3008 {
3010 typecast_exprt tmp(typecast_exprt(src, t), dest_type);
3011 convert_typecast(tmp);
3012 }
3013 }
3014 else
3016 "TODO typecast8 "+src_type.id_string()+" -> "+dest_type.id_string());
3017}
3018
3020{
3021 const exprt &src=expr.op();
3022 // const exprt &rounding_mode=expr.rounding_mode();
3023 const typet &src_type=src.type();
3024 const typet &dest_type=expr.type();
3025
3026 if(dest_type.id()==ID_floatbv)
3027 {
3028 if(src_type.id()==ID_floatbv)
3029 {
3030 // float to float
3031
3032 /* ISO 9899:1999
3033 * 6.3.1.5 Real floating types
3034 * 1 When a float is promoted to double or long double, or a
3035 * double is promoted to long double, its value is unchanged.
3036 *
3037 * 2 When a double is demoted to float, a long double is
3038 * demoted to double or float, or a value being represented in
3039 * greater precision and range than required by its semantic
3040 * type (see 6.3.1.8) is explicitly converted to its semantic
3041 * type, if the value being converted can be represented
3042 * exactly in the new type, it is unchanged. If the value
3043 * being converted is in the range of values that can be
3044 * represented but cannot be represented exactly, the result
3045 * is either the nearest higher or nearest lower representable
3046 * value, chosen in an implementation-defined manner. If the
3047 * value being converted is outside the range of values that
3048 * can be represented, the behavior is undefined.
3049 */
3050
3051 const floatbv_typet &dst=to_floatbv_type(dest_type);
3052
3053 if(use_FPA_theory)
3054 {
3055 out << "((_ to_fp " << dst.get_e() << " "
3056 << dst.get_f() + 1 << ") ";
3058 out << " ";
3059 convert_expr(src);
3060 out << ")";
3061 }
3062 else
3063 convert_floatbv(expr);
3064 }
3065 else if(src_type.id()==ID_unsignedbv)
3066 {
3067 // unsigned to float
3068
3069 /* ISO 9899:1999
3070 * 6.3.1.4 Real floating and integer
3071 * 2 When a value of integer type is converted to a real
3072 * floating type, if the value being converted can be
3073 * represented exactly in the new type, it is unchanged. If the
3074 * value being converted is in the range of values that can be
3075 * represented but cannot be represented exactly, the result is
3076 * either the nearest higher or nearest lower representable
3077 * value, chosen in an implementation-defined manner. If the
3078 * value being converted is outside the range of values that can
3079 * be represented, the behavior is undefined.
3080 */
3081
3082 const floatbv_typet &dst=to_floatbv_type(dest_type);
3083
3084 if(use_FPA_theory)
3085 {
3086 out << "((_ to_fp_unsigned " << dst.get_e() << " "
3087 << dst.get_f() + 1 << ") ";
3089 out << " ";
3090 convert_expr(src);
3091 out << ")";
3092 }
3093 else
3094 convert_floatbv(expr);
3095 }
3096 else if(src_type.id()==ID_signedbv)
3097 {
3098 // signed to float
3099
3100 const floatbv_typet &dst=to_floatbv_type(dest_type);
3101
3102 if(use_FPA_theory)
3103 {
3104 out << "((_ to_fp " << dst.get_e() << " "
3105 << dst.get_f() + 1 << ") ";
3107 out << " ";
3108 convert_expr(src);
3109 out << ")";
3110 }
3111 else
3112 convert_floatbv(expr);
3113 }
3114 else if(src_type.id()==ID_c_enum_tag)
3115 {
3116 // enum to float
3117
3118 // We first convert to 'underlying type'
3119 floatbv_typecast_exprt tmp=expr;
3120 tmp.op() = typecast_exprt(
3121 src, ns.follow_tag(to_c_enum_tag_type(src_type)).underlying_type());
3123 }
3124 else
3126 "TODO typecast11 "+src_type.id_string()+" -> "+dest_type.id_string());
3127 }
3128 else if(dest_type.id()==ID_signedbv)
3129 {
3130 if(use_FPA_theory)
3131 {
3132 std::size_t dest_width=to_signedbv_type(dest_type).get_width();
3133 out << "((_ fp.to_sbv " << dest_width << ") ";
3135 out << " ";
3136 convert_expr(src);
3137 out << ")";
3138 }
3139 else
3140 convert_floatbv(expr);
3141 }
3142 else if(dest_type.id()==ID_unsignedbv)
3143 {
3144 if(use_FPA_theory)
3145 {
3146 std::size_t dest_width=to_unsignedbv_type(dest_type).get_width();
3147 out << "((_ fp.to_ubv " << dest_width << ") ";
3149 out << " ";
3150 convert_expr(src);
3151 out << ")";
3152 }
3153 else
3154 convert_floatbv(expr);
3155 }
3156 else
3157 {
3159 "TODO typecast12 "+src_type.id_string()+" -> "+dest_type.id_string());
3160 }
3161}
3162
3164{
3165 const struct_typet &struct_type =
3166 expr.type().id() == ID_struct_tag
3168 : to_struct_type(expr.type());
3169
3170 const struct_typet::componentst &components=
3171 struct_type.components();
3172
3174 components.size() == expr.operands().size(),
3175 "number of struct components as indicated by the struct type shall be equal"
3176 "to the number of operands of the struct expression");
3177
3178 DATA_INVARIANT(!components.empty(), "struct shall have struct components");
3179
3180 if(use_datatypes)
3181 {
3182 const std::string &smt_typename = datatype_map.at(struct_type);
3183
3184 // use the constructor for the Z3 datatype
3185 out << "(mk-" << smt_typename;
3186
3187 std::size_t i=0;
3188 for(struct_typet::componentst::const_iterator
3189 it=components.begin();
3190 it!=components.end();
3191 it++, i++)
3192 {
3193 if(is_zero_width(it->type(), ns))
3194 continue;
3195 out << " ";
3196 convert_expr(expr.operands()[i]);
3197 }
3198
3199 out << ")";
3200 }
3201 else
3202 {
3203 auto convert_operand = [this](const exprt &op) {
3204 // may need to flatten array-theory arrays in there
3205 if(op.type().id() == ID_array && use_array_theory(op))
3206 flatten_array(op);
3207 else if(op.type().id() == ID_bool)
3208 flatten2bv(op);
3209 else
3210 convert_expr(op);
3211 };
3212
3213 // SMT-LIB 2 concat is binary only
3214 std::size_t n_concat = 0;
3215 for(std::size_t i = components.size(); i > 1; i--)
3216 {
3217 if(is_zero_width(components[i - 1].type(), ns))
3218 continue;
3219 else if(i > 2 || !is_zero_width(components[0].type(), ns))
3220 {
3221 ++n_concat;
3222 out << "(concat ";
3223 }
3224
3225 convert_operand(expr.operands()[i - 1]);
3226
3227 out << " ";
3228 }
3229
3230 if(!is_zero_width(components[0].type(), ns))
3231 convert_operand(expr.op0());
3232
3233 out << std::string(n_concat, ')');
3234 }
3235}
3236
3239{
3240 const array_typet &array_type = to_array_type(expr.type());
3241 const auto &size_expr = array_type.size();
3242 PRECONDITION(size_expr.is_constant());
3243
3245 CHECK_RETURN_WITH_DIAGNOSTICS(size != 0, "can't convert zero-sized array");
3246
3247 out << "(let ((?far ";
3248 convert_expr(expr);
3249 out << ")) ";
3250
3251 for(mp_integer i=size; i!=0; --i)
3252 {
3253 if(i!=1)
3254 out << "(concat ";
3255 out << "(select ?far ";
3256 convert_expr(from_integer(i - 1, array_type.index_type()));
3257 out << ")";
3258 if(i!=1)
3259 out << " ";
3260 }
3261
3262 // close the many parentheses
3263 for(mp_integer i=size; i>1; --i)
3264 out << ")";
3265
3266 out << ")"; // let
3267}
3268
3270{
3271 const exprt &op=expr.op();
3272
3273 std::size_t total_width = boolbv_width(expr.type());
3274
3275 std::size_t member_width=boolbv_width(op.type());
3276
3277 if(total_width==member_width)
3278 {
3279 flatten2bv(op);
3280 }
3281 else
3282 {
3283 // we will pad with zeros, but non-det would be better
3284 INVARIANT(
3285 total_width > member_width,
3286 "total_width should be greater than member_width as member_width can be"
3287 "at most as large as total_width and the other case has been handled "
3288 "above");
3289 out << "(concat ";
3290 out << "(_ bv0 "
3291 << (total_width-member_width) << ") ";
3292 flatten2bv(op);
3293 out << ")";
3294 }
3295}
3296
3298{
3299 const typet &expr_type=expr.type();
3300
3301 if(expr_type.id()==ID_unsignedbv ||
3302 expr_type.id()==ID_signedbv ||
3303 expr_type.id()==ID_bv ||
3304 expr_type.id()==ID_c_enum ||
3305 expr_type.id()==ID_c_enum_tag ||
3306 expr_type.id()==ID_c_bool ||
3307 expr_type.id()==ID_c_bit_field)
3308 {
3309 const std::size_t width = boolbv_width(expr_type);
3310
3311 const mp_integer value = bvrep2integer(expr.get_value(), width, false);
3312
3313 out << "(_ bv" << value
3314 << " " << width << ")";
3315 }
3316 else if(expr_type.id()==ID_fixedbv)
3317 {
3318 const fixedbv_spect spec(to_fixedbv_type(expr_type));
3319
3320 const mp_integer v = bvrep2integer(expr.get_value(), spec.width, false);
3321
3322 out << "(_ bv" << v << " " << spec.width << ")";
3323 }
3324 else if(expr_type.id()==ID_floatbv)
3325 {
3326 const floatbv_typet &floatbv_type=
3327 to_floatbv_type(expr_type);
3328
3329 if(use_FPA_theory)
3330 {
3331 /* CBMC stores floating point literals in the most
3332 computationally useful form; biased exponents and
3333 significands including the hidden bit. Thus some encoding
3334 is needed to get to IEEE-754 style representations. */
3335
3336 ieee_floatt v=ieee_floatt(expr);
3337 size_t e=floatbv_type.get_e();
3338 size_t f=floatbv_type.get_f()+1;
3339
3340 /* Should be sufficient, but not currently supported by mathsat */
3341 #if 0
3342 mp_integer binary = v.pack();
3343
3344 out << "((_ to_fp " << e << " " << f << ")"
3345 << " #b" << integer2binary(v.pack(), v.spec.width()) << ")";
3346 #endif
3347
3348 if(v.is_NaN())
3349 {
3350 out << "(_ NaN " << e << " " << f << ")";
3351 }
3352 else if(v.is_infinity())
3353 {
3354 if(v.get_sign())
3355 out << "(_ -oo " << e << " " << f << ")";
3356 else
3357 out << "(_ +oo " << e << " " << f << ")";
3358 }
3359 else
3360 {
3361 // Zero, normal or subnormal
3362
3363 mp_integer binary = v.pack();
3364 std::string binaryString(integer2binary(v.pack(), v.spec.width()));
3365
3366 out << "(fp "
3367 << "#b" << binaryString.substr(0, 1) << " "
3368 << "#b" << binaryString.substr(1, e) << " "
3369 << "#b" << binaryString.substr(1+e, f-1) << ")";
3370 }
3371 }
3372 else
3373 {
3374 // produce corresponding bit-vector
3375 const ieee_float_spect spec(floatbv_type);
3376 const mp_integer v = bvrep2integer(expr.get_value(), spec.width(), false);
3377 out << "(_ bv" << v << " " << spec.width() << ")";
3378 }
3379 }
3380 else if(expr_type.id()==ID_pointer)
3381 {
3382 if(is_null_pointer(expr))
3383 {
3384 out << "(_ bv0 " << boolbv_width(expr_type)
3385 << ")";
3386 }
3387 else
3388 {
3389 // just treat the pointer as a bit vector
3390 const std::size_t width = boolbv_width(expr_type);
3391
3392 const mp_integer value = bvrep2integer(expr.get_value(), width, false);
3393
3394 out << "(_ bv" << value << " " << width << ")";
3395 }
3396 }
3397 else if(expr_type.id()==ID_bool)
3398 {
3399 if(expr.is_true())
3400 out << "true";
3401 else if(expr.is_false())
3402 out << "false";
3403 else
3404 UNEXPECTEDCASE("unknown Boolean constant");
3405 }
3406 else if(expr_type.id()==ID_array)
3407 {
3408 defined_expressionst::const_iterator it=defined_expressions.find(expr);
3409 CHECK_RETURN(it != defined_expressions.end());
3410 out << it->second;
3411 }
3412 else if(expr_type.id()==ID_rational)
3413 {
3414 std::string value=id2string(expr.get_value());
3415 const bool negative = has_prefix(value, "-");
3416
3417 if(negative)
3418 out << "(- ";
3419
3420 size_t pos=value.find("/");
3421
3422 if(pos==std::string::npos)
3423 out << value << ".0";
3424 else
3425 {
3426 out << "(/ " << value.substr(0, pos) << ".0 "
3427 << value.substr(pos+1) << ".0)";
3428 }
3429
3430 if(negative)
3431 out << ')';
3432 }
3433 else if(expr_type.id()==ID_integer)
3434 {
3435 const auto value = id2string(expr.get_value());
3436
3437 // SMT2 has no negative integer literals
3438 if(has_prefix(value, "-"))
3439 out << "(- " << value.substr(1, std::string::npos) << ')';
3440 else
3441 out << value;
3442 }
3443 else
3444 UNEXPECTEDCASE("unknown constant: "+expr_type.id_string());
3445}
3446
3448{
3449 if(expr.type().id() == ID_integer)
3450 {
3451 out << "(mod ";
3452 convert_expr(expr.op0());
3453 out << ' ';
3454 convert_expr(expr.op1());
3455 out << ')';
3456 }
3457 else
3459 "unsupported type for euclidean_mod: " + expr.type().id_string());
3460}
3461
3463{
3464 if(expr.type().id()==ID_unsignedbv ||
3465 expr.type().id()==ID_signedbv)
3466 {
3467 if(expr.type().id()==ID_unsignedbv)
3468 out << "(bvurem ";
3469 else
3470 out << "(bvsrem ";
3471
3472 convert_expr(expr.op0());
3473 out << " ";
3474 convert_expr(expr.op1());
3475 out << ")";
3476 }
3477 else
3478 UNEXPECTEDCASE("unsupported type for mod: "+expr.type().id_string());
3479}
3480
3482{
3483 std::vector<mp_integer> dynamic_objects;
3484 pointer_logic.get_dynamic_objects(dynamic_objects);
3485
3486 if(dynamic_objects.empty())
3487 out << "false";
3488 else
3489 {
3490 std::size_t pointer_width = boolbv_width(expr.op().type());
3491
3492 out << "(let ((?obj ((_ extract "
3493 << pointer_width-1 << " "
3494 << pointer_width-config.bv_encoding.object_bits << ") ";
3495 convert_expr(expr.op());
3496 out << "))) ";
3497
3498 if(dynamic_objects.size()==1)
3499 {
3500 out << "(= (_ bv" << dynamic_objects.front()
3501 << " " << config.bv_encoding.object_bits << ") ?obj)";
3502 }
3503 else
3504 {
3505 out << "(or";
3506
3507 for(const auto &object : dynamic_objects)
3508 out << " (= (_ bv" << object
3509 << " " << config.bv_encoding.object_bits << ") ?obj)";
3510
3511 out << ")"; // or
3512 }
3513
3514 out << ")"; // let
3515 }
3516}
3517
3519{
3520 const typet &op_type=expr.op0().type();
3521
3522 if(op_type.id()==ID_unsignedbv ||
3523 op_type.id()==ID_bv)
3524 {
3525 out << "(";
3526 if(expr.id()==ID_le)
3527 out << "bvule";
3528 else if(expr.id()==ID_lt)
3529 out << "bvult";
3530 else if(expr.id()==ID_ge)
3531 out << "bvuge";
3532 else if(expr.id()==ID_gt)
3533 out << "bvugt";
3534
3535 out << " ";
3536 convert_expr(expr.op0());
3537 out << " ";
3538 convert_expr(expr.op1());
3539 out << ")";
3540 }
3541 else if(op_type.id()==ID_signedbv ||
3542 op_type.id()==ID_fixedbv)
3543 {
3544 out << "(";
3545 if(expr.id()==ID_le)
3546 out << "bvsle";
3547 else if(expr.id()==ID_lt)
3548 out << "bvslt";
3549 else if(expr.id()==ID_ge)
3550 out << "bvsge";
3551 else if(expr.id()==ID_gt)
3552 out << "bvsgt";
3553
3554 out << " ";
3555 convert_expr(expr.op0());
3556 out << " ";
3557 convert_expr(expr.op1());
3558 out << ")";
3559 }
3560 else if(op_type.id()==ID_floatbv)
3561 {
3562 if(use_FPA_theory)
3563 {
3564 out << "(";
3565 if(expr.id()==ID_le)
3566 out << "fp.leq";
3567 else if(expr.id()==ID_lt)
3568 out << "fp.lt";
3569 else if(expr.id()==ID_ge)
3570 out << "fp.geq";
3571 else if(expr.id()==ID_gt)
3572 out << "fp.gt";
3573
3574 out << " ";
3575 convert_expr(expr.op0());
3576 out << " ";
3577 convert_expr(expr.op1());
3578 out << ")";
3579 }
3580 else
3581 convert_floatbv(expr);
3582 }
3583 else if(op_type.id()==ID_rational ||
3584 op_type.id()==ID_integer)
3585 {
3586 out << "(";
3587 out << expr.id();
3588
3589 out << " ";
3590 convert_expr(expr.op0());
3591 out << " ";
3592 convert_expr(expr.op1());
3593 out << ")";
3594 }
3595 else if(op_type.id() == ID_pointer)
3596 {
3597 const exprt same_object = ::same_object(expr.op0(), expr.op1());
3598
3599 out << "(and ";
3601
3602 out << " (";
3603 if(expr.id() == ID_le)
3604 out << "bvsle";
3605 else if(expr.id() == ID_lt)
3606 out << "bvslt";
3607 else if(expr.id() == ID_ge)
3608 out << "bvsge";
3609 else if(expr.id() == ID_gt)
3610 out << "bvsgt";
3611
3612 out << ' ';
3614 out << ' ';
3616 out << ')';
3617
3618 out << ')';
3619 }
3620 else
3622 "unsupported type for "+expr.id_string()+": "+op_type.id_string());
3623}
3624
3626{
3627 if(
3628 expr.type().id() == ID_rational || expr.type().id() == ID_integer ||
3629 expr.type().id() == ID_real)
3630 {
3631 // these are multi-ary in SMT-LIB2
3632 out << "(+";
3633
3634 for(const auto &op : expr.operands())
3635 {
3636 out << ' ';
3637 convert_expr(op);
3638 }
3639
3640 out << ')';
3641 }
3642 else if(
3643 expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv ||
3644 expr.type().id() == ID_fixedbv)
3645 {
3646 // These could be chained, i.e., need not be binary,
3647 // but at least MathSat doesn't like that.
3648 if(expr.operands().size() == 2)
3649 {
3650 out << "(bvadd ";
3651 convert_expr(expr.op0());
3652 out << " ";
3653 convert_expr(expr.op1());
3654 out << ")";
3655 }
3656 else
3657 {
3659 }
3660 }
3661 else if(expr.type().id() == ID_floatbv)
3662 {
3663 // Floating-point additions should have be been converted
3664 // to ID_floatbv_plus during symbolic execution, adding
3665 // the rounding mode. See smt2_convt::convert_floatbv_plus.
3667 }
3668 else if(expr.type().id() == ID_pointer)
3669 {
3670 if(expr.operands().size() == 2)
3671 {
3672 exprt p = expr.op0(), i = expr.op1();
3673
3674 if(p.type().id() != ID_pointer)
3675 p.swap(i);
3676
3678 p.type().id() == ID_pointer,
3679 "one of the operands should have pointer type");
3680
3681 const auto &base_type = to_pointer_type(expr.type()).base_type();
3683 base_type.id() != ID_empty, "no pointer arithmetic over void pointers");
3684
3685 auto element_size_opt = pointer_offset_size(base_type, ns);
3686 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 0);
3687 mp_integer element_size = *element_size_opt;
3688
3689 // First convert the pointer operand
3690 out << "(let ((?pointerop ";
3691 convert_expr(p);
3692 out << ")) ";
3693
3694 // The addition is done on the offset part only.
3695 const std::size_t pointer_width = boolbv_width(p.type());
3696 const std::size_t offset_bits =
3697 pointer_width - config.bv_encoding.object_bits;
3698
3699 out << "(concat ";
3700 out << "((_ extract " << pointer_width - 1 << ' ' << offset_bits
3701 << ") ?pointerop) ";
3702 out << "(bvadd ((_ extract " << offset_bits - 1 << " 0) ?pointerop) ";
3703
3704 if(element_size >= 2)
3705 {
3706 out << "(bvmul ((_ extract " << offset_bits - 1 << " 0) ";
3707 convert_expr(i);
3708 out << ") (_ bv" << element_size << " " << offset_bits << "))";
3709 }
3710 else
3711 {
3712 out << "((_ extract " << offset_bits - 1 << " 0) ";
3713 convert_expr(i);
3714 out << ')'; // extract
3715 }
3716
3717 out << ")))"; // bvadd, concat, let
3718 }
3719 else
3720 {
3722 }
3723 }
3724 else
3725 UNEXPECTEDCASE("unsupported type for +: " + expr.type().id_string());
3726}
3727
3732{
3734
3735 /* CProver uses the x86 numbering of the rounding-mode
3736 * 0 == FE_TONEAREST
3737 * 1 == FE_DOWNWARD
3738 * 2 == FE_UPWARD
3739 * 3 == FE_TOWARDZERO
3740 * These literal values must be used rather than the macros
3741 * the macros from fenv.h to avoid portability problems.
3742 */
3743
3744 if(expr.is_constant())
3745 {
3746 const constant_exprt &cexpr=to_constant_expr(expr);
3747
3749
3750 if(value==0)
3751 out << "roundNearestTiesToEven";
3752 else if(value==1)
3753 out << "roundTowardNegative";
3754 else if(value==2)
3755 out << "roundTowardPositive";
3756 else if(value==3)
3757 out << "roundTowardZero";
3758 else
3760 false,
3761 "Rounding mode should have value 0, 1, 2, or 3",
3762 id2string(cexpr.get_value()));
3763 }
3764 else
3765 {
3766 std::size_t width=to_bitvector_type(expr.type()).get_width();
3767
3768 // Need to make the choice above part of the model
3769 out << "(ite (= (_ bv0 " << width << ") ";
3770 convert_expr(expr);
3771 out << ") roundNearestTiesToEven ";
3772
3773 out << "(ite (= (_ bv1 " << width << ") ";
3774 convert_expr(expr);
3775 out << ") roundTowardNegative ";
3776
3777 out << "(ite (= (_ bv2 " << width << ") ";
3778 convert_expr(expr);
3779 out << ") roundTowardPositive ";
3780
3781 // TODO: add some kind of error checking here
3782 out << "roundTowardZero";
3783
3784 out << ")))";
3785 }
3786}
3787
3789{
3790 const typet &type=expr.type();
3791
3793 type.id() == ID_floatbv ||
3794 (type.id() == ID_complex &&
3795 to_complex_type(type).subtype().id() == ID_floatbv));
3796
3797 if(use_FPA_theory)
3798 {
3799 if(type.id()==ID_floatbv)
3800 {
3801 out << "(fp.add ";
3803 out << " ";
3804 convert_expr(expr.lhs());
3805 out << " ";
3806 convert_expr(expr.rhs());
3807 out << ")";
3808 }
3809 else if(type.id()==ID_complex)
3810 {
3811 SMT2_TODO("+ for floatbv complex");
3812 }
3813 else
3815 false,
3816 "type should not be one of the unsupported types",
3817 type.id_string());
3818 }
3819 else
3820 convert_floatbv(expr);
3821}
3822
3824{
3825 if(expr.type().id()==ID_integer)
3826 {
3827 out << "(- ";
3828 convert_expr(expr.op0());
3829 out << " ";
3830 convert_expr(expr.op1());
3831 out << ")";
3832 }
3833 else if(expr.type().id()==ID_unsignedbv ||
3834 expr.type().id()==ID_signedbv ||
3835 expr.type().id()==ID_fixedbv)
3836 {
3837 if(expr.op0().type().id()==ID_pointer &&
3838 expr.op1().type().id()==ID_pointer)
3839 {
3840 // Pointer difference
3841 const auto &base_type = to_pointer_type(expr.op0().type()).base_type();
3843 base_type.id() != ID_empty, "no pointer arithmetic over void pointers");
3844 auto element_size_opt = pointer_offset_size(base_type, ns);
3845 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3846 mp_integer element_size = *element_size_opt;
3847
3848 if(element_size >= 2)
3849 out << "(bvsdiv ";
3850
3851 INVARIANT(
3852 boolbv_width(expr.op0().type()) == boolbv_width(expr.type()),
3853 "bitvector width of operand shall be equal to the bitvector width of "
3854 "the expression");
3855
3856 out << "(bvsub ";
3857 convert_expr(expr.op0());
3858 out << " ";
3859 convert_expr(expr.op1());
3860 out << ")";
3861
3862 if(element_size >= 2)
3863 out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
3864 << "))";
3865 }
3866 else
3867 {
3868 out << "(bvsub ";
3869 convert_expr(expr.op0());
3870 out << " ";
3871 convert_expr(expr.op1());
3872 out << ")";
3873 }
3874 }
3875 else if(expr.type().id()==ID_floatbv)
3876 {
3877 // Floating-point subtraction should have be been converted
3878 // to ID_floatbv_minus during symbolic execution, adding
3879 // the rounding mode. See smt2_convt::convert_floatbv_minus.
3881 }
3882 else if(expr.type().id()==ID_pointer)
3883 {
3884 if(
3885 expr.op0().type().id() == ID_pointer &&
3886 (expr.op1().type().id() == ID_unsignedbv ||
3887 expr.op1().type().id() == ID_signedbv))
3888 {
3889 // rewrite p-o to p+(-o)
3890 return convert_plus(
3891 plus_exprt(expr.op0(), unary_minus_exprt(expr.op1())));
3892 }
3893 else
3895 "unsupported operand types for -: " + expr.op0().type().id_string() +
3896 " and " + expr.op1().type().id_string());
3897 }
3898 else
3899 UNEXPECTEDCASE("unsupported type for -: "+expr.type().id_string());
3900}
3901
3903{
3905 expr.type().id() == ID_floatbv,
3906 "type of ieee floating point expression shall be floatbv");
3907
3908 if(use_FPA_theory)
3909 {
3910 out << "(fp.sub ";
3912 out << " ";
3913 convert_expr(expr.lhs());
3914 out << " ";
3915 convert_expr(expr.rhs());
3916 out << ")";
3917 }
3918 else
3919 convert_floatbv(expr);
3920}
3921
3923{
3924 if(expr.type().id()==ID_unsignedbv ||
3925 expr.type().id()==ID_signedbv)
3926 {
3927 if(expr.type().id()==ID_unsignedbv)
3928 out << "(bvudiv ";
3929 else
3930 out << "(bvsdiv ";
3931
3932 convert_expr(expr.op0());
3933 out << " ";
3934 convert_expr(expr.op1());
3935 out << ")";
3936 }
3937 else if(expr.type().id()==ID_fixedbv)
3938 {
3939 fixedbv_spect spec(to_fixedbv_type(expr.type()));
3940 std::size_t fraction_bits=spec.get_fraction_bits();
3941
3942 out << "((_ extract " << spec.width-1 << " 0) ";
3943 out << "(bvsdiv ";
3944
3945 out << "(concat ";
3946 convert_expr(expr.op0());
3947 out << " (_ bv0 " << fraction_bits << ")) ";
3948
3949 out << "((_ sign_extend " << fraction_bits << ") ";
3950 convert_expr(expr.op1());
3951 out << ")";
3952
3953 out << "))";
3954 }
3955 else if(expr.type().id()==ID_floatbv)
3956 {
3957 // Floating-point division should have be been converted
3958 // to ID_floatbv_div during symbolic execution, adding
3959 // the rounding mode. See smt2_convt::convert_floatbv_div.
3961 }
3962 else
3963 UNEXPECTEDCASE("unsupported type for /: "+expr.type().id_string());
3964}
3965
3967{
3969 expr.type().id() == ID_floatbv,
3970 "type of ieee floating point expression shall be floatbv");
3971
3972 if(use_FPA_theory)
3973 {
3974 out << "(fp.div ";
3976 out << " ";
3977 convert_expr(expr.lhs());
3978 out << " ";
3979 convert_expr(expr.rhs());
3980 out << ")";
3981 }
3982 else
3983 convert_floatbv(expr);
3984}
3985
3987{
3988 // re-write to binary if needed
3989 if(expr.operands().size()>2)
3990 {
3991 // strip last operand
3992 exprt tmp=expr;
3993 tmp.operands().pop_back();
3994
3995 // recursive call
3996 return convert_mult(mult_exprt(tmp, expr.operands().back()));
3997 }
3998
3999 INVARIANT(
4000 expr.operands().size() == 2,
4001 "expression should have been converted to a variant with two operands");
4002
4003 if(expr.type().id()==ID_unsignedbv ||
4004 expr.type().id()==ID_signedbv)
4005 {
4006 // Note that bvmul is really unsigned,
4007 // but this is irrelevant as we chop-off any extra result
4008 // bits.
4009 out << "(bvmul ";
4010 convert_expr(expr.op0());
4011 out << " ";
4012 convert_expr(expr.op1());
4013 out << ")";
4014 }
4015 else if(expr.type().id()==ID_floatbv)
4016 {
4017 // Floating-point multiplication should have be been converted
4018 // to ID_floatbv_mult during symbolic execution, adding
4019 // the rounding mode. See smt2_convt::convert_floatbv_mult.
4021 }
4022 else if(expr.type().id()==ID_fixedbv)
4023 {
4024 fixedbv_spect spec(to_fixedbv_type(expr.type()));
4025 std::size_t fraction_bits=spec.get_fraction_bits();
4026
4027 out << "((_ extract "
4028 << spec.width+fraction_bits-1 << " "
4029 << fraction_bits << ") ";
4030
4031 out << "(bvmul ";
4032
4033 out << "((_ sign_extend " << fraction_bits << ") ";
4034 convert_expr(expr.op0());
4035 out << ") ";
4036
4037 out << "((_ sign_extend " << fraction_bits << ") ";
4038 convert_expr(expr.op1());
4039 out << ")";
4040
4041 out << "))"; // bvmul, extract
4042 }
4043 else if(expr.type().id()==ID_rational ||
4044 expr.type().id()==ID_integer ||
4045 expr.type().id()==ID_real)
4046 {
4047 out << "(*";
4048
4049 for(const auto &op : expr.operands())
4050 {
4051 out << " ";
4052 convert_expr(op);
4053 }
4054
4055 out << ")";
4056 }
4057 else
4058 UNEXPECTEDCASE("unsupported type for *: "+expr.type().id_string());
4059}
4060
4062{
4064 expr.type().id() == ID_floatbv,
4065 "type of ieee floating point expression shall be floatbv");
4066
4067 if(use_FPA_theory)
4068 {
4069 out << "(fp.mul ";
4071 out << " ";
4072 convert_expr(expr.lhs());
4073 out << " ";
4074 convert_expr(expr.rhs());
4075 out << ")";
4076 }
4077 else
4078 convert_floatbv(expr);
4079}
4080
4082{
4084 expr.type().id() == ID_floatbv,
4085 "type of ieee floating point expression shall be floatbv");
4086
4087 if(use_FPA_theory)
4088 {
4089 // Note that these do not have a rounding mode
4090 out << "(fp.rem ";
4091 convert_expr(expr.lhs());
4092 out << " ";
4093 convert_expr(expr.rhs());
4094 out << ")";
4095 }
4096 else
4097 {
4098 SMT2_TODO(
4099 "smt2_convt::convert_floatbv_rem to be implemented when not using "
4100 "FPA_theory");
4101 }
4102}
4103
4105{
4106 // get rid of "with" that has more than three operands
4107
4108 if(expr.operands().size()>3)
4109 {
4110 std::size_t s=expr.operands().size();
4111
4112 // strip off the trailing two operands
4113 with_exprt tmp = expr;
4114 tmp.operands().resize(s-2);
4115
4116 with_exprt new_with_expr(
4117 tmp, expr.operands()[s - 2], expr.operands().back());
4118
4119 // recursive call
4120 return convert_with(new_with_expr);
4121 }
4122
4123 INVARIANT(
4124 expr.operands().size() == 3,
4125 "with expression should have been converted to a version with three "
4126 "operands above");
4127
4128 const typet &expr_type = expr.type();
4129
4130 if(expr_type.id()==ID_array)
4131 {
4132 const array_typet &array_type=to_array_type(expr_type);
4133
4134 if(use_array_theory(expr))
4135 {
4136 out << "(store ";
4137 convert_expr(expr.old());
4138 out << " ";
4139 convert_expr(typecast_exprt(expr.where(), array_type.index_type()));
4140 out << " ";
4141 convert_expr(expr.new_value());
4142 out << ")";
4143 }
4144 else
4145 {
4146 // fixed-width
4147 std::size_t array_width=boolbv_width(array_type);
4148 std::size_t sub_width = boolbv_width(array_type.element_type());
4149 std::size_t index_width=boolbv_width(expr.where().type());
4150
4151 // We mask out the updated bits with AND,
4152 // and then OR-in the shifted new value.
4153
4154 out << "(let ((distance? ";
4155 out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
4156
4157 // SMT2 says that the shift distance needs to be as wide
4158 // as the stuff we are shifting.
4159 if(array_width>index_width)
4160 {
4161 out << "((_ zero_extend " << array_width-index_width << ") ";
4162 convert_expr(expr.where());
4163 out << ")";
4164 }
4165 else
4166 {
4167 out << "((_ extract " << array_width-1 << " 0) ";
4168 convert_expr(expr.where());
4169 out << ")";
4170 }
4171
4172 out << "))) "; // bvmul, distance?
4173
4174 out << "(bvor ";
4175 out << "(bvand ";
4176 out << "(bvnot ";
4177 out << "(bvshl (_ bv" << power(2, sub_width) - 1 << " " << array_width
4178 << ") ";
4179 out << "distance?)) "; // bvnot, bvlshl
4180 convert_expr(expr.old());
4181 out << ") "; // bvand
4182 out << "(bvshl ";
4183 out << "((_ zero_extend " << array_width-sub_width << ") ";
4184 convert_expr(expr.new_value());
4185 out << ") distance?)))"; // zero_extend, bvshl, bvor, let
4186 }
4187 }
4188 else if(expr_type.id() == ID_struct || expr_type.id() == ID_struct_tag)
4189 {
4190 const struct_typet &struct_type =
4191 expr_type.id() == ID_struct_tag
4192 ? ns.follow_tag(to_struct_tag_type(expr_type))
4193 : to_struct_type(expr_type);
4194
4195 const exprt &index = expr.where();
4196 const exprt &value = expr.new_value();
4197
4198 const irep_idt &component_name=index.get(ID_component_name);
4199
4200 INVARIANT(
4201 struct_type.has_component(component_name),
4202 "struct should have accessed component");
4203
4204 if(use_datatypes)
4205 {
4206 const std::string &smt_typename = datatype_map.at(expr_type);
4207
4208 out << "(update-" << smt_typename << "." << component_name << " ";
4209 convert_expr(expr.old());
4210 out << " ";
4211 convert_expr(value);
4212 out << ")";
4213 }
4214 else
4215 {
4216 std::size_t struct_width=boolbv_width(struct_type);
4217
4218 // figure out the offset and width of the member
4219 const boolbv_widtht::membert &m =
4220 boolbv_width.get_member(struct_type, component_name);
4221
4222 out << "(let ((?withop ";
4223 convert_expr(expr.old());
4224 out << ")) ";
4225
4226 if(m.width==struct_width)
4227 {
4228 // the struct is the same as the member, no concat needed,
4229 // ?withop won't be used
4230 convert_expr(value);
4231 }
4232 else if(m.offset==0)
4233 {
4234 // the member is at the beginning
4235 out << "(concat "
4236 << "((_ extract " << (struct_width-1) << " "
4237 << m.width << ") ?withop) ";
4238 convert_expr(value);
4239 out << ")"; // concat
4240 }
4241 else if(m.offset+m.width==struct_width)
4242 {
4243 // the member is at the end
4244 out << "(concat ";
4245 convert_expr(value);
4246 out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))";
4247 }
4248 else
4249 {
4250 // most general case, need two concat-s
4251 out << "(concat (concat "
4252 << "((_ extract " << (struct_width-1) << " "
4253 << (m.offset+m.width) << ") ?withop) ";
4254 convert_expr(value);
4255 out << ") ((_ extract " << (m.offset-1) << " 0) ?withop)";
4256 out << ")"; // concat
4257 }
4258
4259 out << ")"; // let ?withop
4260 }
4261 }
4262 else if(expr_type.id() == ID_union || expr_type.id() == ID_union_tag)
4263 {
4264 const exprt &value = expr.new_value();
4265
4266 std::size_t total_width = boolbv_width(expr_type);
4267
4268 std::size_t member_width=boolbv_width(value.type());
4269
4270 if(total_width==member_width)
4271 {
4272 flatten2bv(value);
4273 }
4274 else
4275 {
4276 INVARIANT(
4277 total_width > member_width,
4278 "total width should be greater than member_width as member_width is at "
4279 "most as large as total_width and the other case has been handled "
4280 "above");
4281 out << "(concat ";
4282 out << "((_ extract "
4283 << (total_width-1)
4284 << " " << member_width << ") ";
4285 convert_expr(expr.old());
4286 out << ") ";
4287 flatten2bv(value);
4288 out << ")";
4289 }
4290 }
4291 else if(expr_type.id()==ID_bv ||
4292 expr_type.id()==ID_unsignedbv ||
4293 expr_type.id()==ID_signedbv)
4294 {
4295 if(expr.new_value().type().id() == ID_bool)
4296 {
4298 update_bit_exprt(expr.old(), expr.where(), expr.new_value()));
4299 }
4300 else
4301 {
4303 update_bits_exprt(expr.old(), expr.where(), expr.new_value()));
4304 }
4305 }
4306 else
4308 "with expects struct, union, or array type, but got "+
4309 expr.type().id_string());
4310}
4311
4313{
4314 PRECONDITION(expr.operands().size() == 3);
4315
4316 SMT2_TODO("smt2_convt::convert_update to be implemented");
4317}
4318
4320{
4321 return convert_expr(expr.lower());
4322}
4323
4325{
4326 return convert_expr(expr.lower());
4327}
4328
4330{
4331 const typet &array_op_type = expr.array().type();
4332
4333 if(array_op_type.id()==ID_array)
4334 {
4335 const array_typet &array_type=to_array_type(array_op_type);
4336
4337 if(use_array_theory(expr.array()))
4338 {
4339 if(expr.is_boolean() && !use_array_of_bool)
4340 {
4341 out << "(= ";
4342 out << "(select ";
4343 convert_expr(expr.array());
4344 out << " ";
4345 convert_expr(typecast_exprt(expr.index(), array_type.index_type()));
4346 out << ")";
4347 out << " #b1)";
4348 }
4349 else
4350 {
4351 out << "(select ";
4352 convert_expr(expr.array());
4353 out << " ";
4354 convert_expr(typecast_exprt(expr.index(), array_type.index_type()));
4355 out << ")";
4356 }
4357 }
4358 else
4359 {
4360 // fixed size
4361 std::size_t array_width=boolbv_width(array_type);
4362
4363 unflatten(wheret::BEGIN, array_type.element_type());
4364
4365 std::size_t sub_width = boolbv_width(array_type.element_type());
4366 std::size_t index_width=boolbv_width(expr.index().type());
4367
4368 out << "((_ extract " << sub_width-1 << " 0) ";
4369 out << "(bvlshr ";
4370 convert_expr(expr.array());
4371 out << " ";
4372 out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
4373
4374 // SMT2 says that the shift distance must be the same as
4375 // the width of what we shift.
4376 if(array_width>index_width)
4377 {
4378 out << "((_ zero_extend " << array_width-index_width << ") ";
4379 convert_expr(expr.index());
4380 out << ")"; // zero_extend
4381 }
4382 else
4383 {
4384 out << "((_ extract " << array_width-1 << " 0) ";
4385 convert_expr(expr.index());
4386 out << ")"; // extract
4387 }
4388
4389 out << ")))"; // mult, bvlshr, extract
4390
4391 unflatten(wheret::END, array_type.element_type());
4392 }
4393 }
4394 else
4395 INVARIANT(
4396 false, "index with unsupported array type: " + array_op_type.id_string());
4397}
4398
4400{
4401 const member_exprt &member_expr=to_member_expr(expr);
4402 const exprt &struct_op=member_expr.struct_op();
4403 const typet &struct_op_type = struct_op.type();
4404 const irep_idt &name=member_expr.get_component_name();
4405
4406 if(struct_op_type.id() == ID_struct || struct_op_type.id() == ID_struct_tag)
4407 {
4408 const struct_typet &struct_type =
4409 struct_op_type.id() == ID_struct_tag
4410 ? ns.follow_tag(to_struct_tag_type(struct_op_type))
4411 : to_struct_type(struct_op_type);
4412
4413 INVARIANT(
4414 struct_type.has_component(name), "struct should have accessed component");
4415
4416 if(use_datatypes)
4417 {
4418 const std::string &smt_typename = datatype_map.at(struct_type);
4419
4420 out << "(" << smt_typename << "."
4421 << struct_type.get_component(name).get_name()
4422 << " ";
4423 convert_expr(struct_op);
4424 out << ")";
4425 }
4426 else
4427 {
4428 // we extract
4429 const auto &member_offset = boolbv_width.get_member(struct_type, name);
4430
4431 if(expr.type().id() == ID_bool)
4432 out << "(= ";
4433 out << "((_ extract " << (member_offset.offset + member_offset.width - 1)
4434 << " " << member_offset.offset << ") ";
4435 convert_expr(struct_op);
4436 out << ")";
4437 if(expr.type().id() == ID_bool)
4438 out << " #b1)";
4439 }
4440 }
4441 else if(
4442 struct_op_type.id() == ID_union || struct_op_type.id() == ID_union_tag)
4443 {
4444 std::size_t width=boolbv_width(expr.type());
4446 width != 0, "failed to get union member width");
4447
4448 if(use_datatypes)
4449 {
4450 unflatten(wheret::BEGIN, expr.type());
4451
4452 out << "((_ extract " << (width - 1) << " 0) ";
4453 convert_expr(struct_op);
4454 out << ")";
4455
4456 unflatten(wheret::END, expr.type());
4457 }
4458 else
4459 {
4460 out << "((_ extract " << (width - 1) << " 0) ";
4461 convert_expr(struct_op);
4462 out << ")";
4463 }
4464 }
4465 else
4467 "convert_member on an unexpected type "+struct_op_type.id_string());
4468}
4469
4471{
4472 const typet &type = expr.type();
4473
4474 if(type.id()==ID_bool)
4475 {
4476 out << "(ite ";
4477 convert_expr(expr); // this returns a Bool
4478 out << " #b1 #b0)"; // this is a one-bit bit-vector
4479 }
4480 else if(type.id()==ID_array)
4481 {
4482 if(use_array_theory(expr))
4483 {
4484 // concatenate elements
4485 const array_typet &array_type = to_array_type(type);
4486
4487 mp_integer size =
4489
4490 // SMT-LIB 2 concat is binary only
4491 std::size_t n_concat = 0;
4492 for(mp_integer i = size; i > 1; --i)
4493 {
4494 ++n_concat;
4495 out << "(concat ";
4496
4497 flatten2bv(
4498 index_exprt{expr, from_integer(i - 1, array_type.index_type())});
4499
4500 out << " ";
4501 }
4502
4503 flatten2bv(index_exprt{expr, from_integer(0, array_type.index_type())});
4504
4505 out << std::string(n_concat, ')'); // concat
4506 }
4507 else
4508 convert_expr(expr);
4509 }
4510 else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4511 {
4512 if(use_datatypes)
4513 {
4514 // concatenate elements
4515 const struct_typet &struct_type =
4516 type.id() == ID_struct_tag ? ns.follow_tag(to_struct_tag_type(type))
4517 : to_struct_type(type);
4518
4519 const struct_typet::componentst &components=
4520 struct_type.components();
4521
4522 // SMT-LIB 2 concat is binary only
4523 std::size_t n_concat = 0;
4524 for(std::size_t i=components.size(); i>1; i--)
4525 {
4526 if(is_zero_width(components[i - 1].type(), ns))
4527 continue;
4528 else if(i > 2 || !is_zero_width(components[0].type(), ns))
4529 {
4530 ++n_concat;
4531 out << "(concat ";
4532 }
4533
4534 flatten2bv(member_exprt{expr, components[i - 1]});
4535
4536 out << " ";
4537 }
4538
4539 if(!is_zero_width(components[0].type(), ns))
4540 {
4541 flatten2bv(member_exprt{expr, components[0]});
4542 }
4543
4544 out << std::string(n_concat, ')'); // concat
4545 }
4546 else
4547 convert_expr(expr);
4548 }
4549 else if(type.id()==ID_floatbv)
4550 {
4551 INVARIANT(
4553 "floatbv expressions should be flattened when using FPA theory");
4554
4555 convert_expr(expr);
4556 }
4557 else
4558 convert_expr(expr);
4559}
4560
4562 wheret where,
4563 const typet &type,
4564 unsigned nesting)
4565{
4566 if(type.id()==ID_bool)
4567 {
4568 if(where==wheret::BEGIN)
4569 out << "(= "; // produces a bool
4570 else
4571 out << " #b1)";
4572 }
4573 else if(type.id() == ID_array)
4574 {
4576
4577 if(where == wheret::BEGIN)
4578 out << "(let ((?ufop" << nesting << " ";
4579 else
4580 {
4581 out << ")) ";
4582
4583 const array_typet &array_type = to_array_type(type);
4584
4585 std::size_t subtype_width = boolbv_width(array_type.element_type());
4586
4588 array_type.size().is_constant(),
4589 "cannot unflatten arrays of non-constant size");
4590 mp_integer size =
4592
4593 for(mp_integer i = 1; i < size; ++i)
4594 out << "(store ";
4595
4596 out << "((as const ";
4597 convert_type(array_type);
4598 out << ") ";
4599 // use element at index 0 as default value
4600 unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1);
4601 out << "((_ extract " << subtype_width - 1 << " "
4602 << "0) ?ufop" << nesting << ")";
4603 unflatten(wheret::END, array_type.element_type(), nesting + 1);
4604 out << ") ";
4605
4606 std::size_t offset = subtype_width;
4607 for(mp_integer i = 1; i < size; ++i, offset += subtype_width)
4608 {
4609 convert_expr(from_integer(i, array_type.index_type()));
4610 out << ' ';
4611 unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1);
4612 out << "((_ extract " << offset + subtype_width - 1 << " " << offset
4613 << ") ?ufop" << nesting << ")";
4614 unflatten(wheret::END, array_type.element_type(), nesting + 1);
4615 out << ")"; // store
4616 }
4617
4618 out << ")"; // let
4619 }
4620 }
4621 else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4622 {
4623 if(use_datatypes)
4624 {
4625 // extract members
4626 if(where==wheret::BEGIN)
4627 out << "(let ((?ufop" << nesting << " ";
4628 else
4629 {
4630 out << ")) ";
4631
4632 const std::string &smt_typename = datatype_map.at(type);
4633
4634 out << "(mk-" << smt_typename;
4635
4636 const struct_typet &struct_type =
4637 type.id() == ID_struct_tag ? ns.follow_tag(to_struct_tag_type(type))
4638 : to_struct_type(type);
4639
4640 const struct_typet::componentst &components=
4641 struct_type.components();
4642
4643 std::size_t offset=0;
4644
4645 std::size_t i=0;
4646 for(struct_typet::componentst::const_iterator
4647 it=components.begin();
4648 it!=components.end();
4649 it++, i++)
4650 {
4651 if(is_zero_width(it->type(), ns))
4652 continue;
4653
4654 std::size_t member_width=boolbv_width(it->type());
4655
4656 out << " ";
4657 unflatten(wheret::BEGIN, it->type(), nesting+1);
4658 out << "((_ extract " << offset+member_width-1 << " "
4659 << offset << ") ?ufop" << nesting << ")";
4660 unflatten(wheret::END, it->type(), nesting+1);
4661 offset+=member_width;
4662 }
4663
4664 out << "))"; // mk-, let
4665 }
4666 }
4667 else
4668 {
4669 // nop, already a bv
4670 }
4671 }
4672 else
4673 {
4674 // nop
4675 }
4676}
4677
4678void smt2_convt::set_to(const exprt &expr, bool value)
4679{
4680 PRECONDITION(expr.is_boolean());
4681
4682 if(expr.id()==ID_and && value)
4683 {
4684 for(const auto &op : expr.operands())
4685 set_to(op, true);
4686 return;
4687 }
4688
4689 if(expr.id()==ID_or && !value)
4690 {
4691 for(const auto &op : expr.operands())
4692 set_to(op, false);
4693 return;
4694 }
4695
4696 if(expr.id()==ID_not)
4697 {
4698 return set_to(to_not_expr(expr).op(), !value);
4699 }
4700
4701 out << "\n";
4702
4703 // special treatment for "set_to(a=b, true)" where
4704 // a is a new symbol
4705
4706 if(expr.id() == ID_equal && value)
4707 {
4708 const equal_exprt &equal_expr=to_equal_expr(expr);
4709 if(is_zero_width(equal_expr.lhs().type(), ns))
4710 {
4711 // ignore equality checking over expressions with empty (void) type
4712 return;
4713 }
4714
4715 if(equal_expr.lhs().id()==ID_symbol)
4716 {
4717 const irep_idt &identifier=
4718 to_symbol_expr(equal_expr.lhs()).get_identifier();
4719
4720 if(
4721 identifier_map.find(identifier) == identifier_map.end() &&
4722 equal_expr.lhs() != equal_expr.rhs())
4723 {
4724 auto id_entry = identifier_map.insert(
4725 {identifier, identifiert{equal_expr.lhs().type(), false}});
4726 CHECK_RETURN(id_entry.second);
4727
4728 find_symbols(id_entry.first->second.type);
4729 exprt prepared_rhs = prepare_for_convert_expr(equal_expr.rhs());
4730
4731 std::string smt2_identifier=convert_identifier(identifier);
4732 smt2_identifiers.insert(smt2_identifier);
4733
4734 out << "; set_to true (equal)\n";
4735
4736 if(equal_expr.lhs().type().id() == ID_mathematical_function)
4737 {
4738 // We avoid define-fun, since it has been reported to cause
4739 // trouble with Z3's parser.
4740 out << "(declare-fun " << smt2_identifier;
4741
4742 auto &mathematical_function_type =
4743 to_mathematical_function_type(equal_expr.lhs().type());
4744
4745 out << " (";
4746 bool first = true;
4747
4748 for(auto &t : mathematical_function_type.domain())
4749 {
4750 if(first)
4751 first = false;
4752 else
4753 out << ' ';
4754
4755 convert_type(t);
4756 }
4757
4758 out << ") ";
4759 convert_type(mathematical_function_type.codomain());
4760 out << ")\n";
4761
4762 out << "(assert (= " << smt2_identifier << ' ';
4763 convert_expr(prepared_rhs);
4764 out << ')' << ')' << '\n';
4765 }
4766 else
4767 {
4768 out << "(define-fun " << smt2_identifier;
4769 out << " () ";
4770 convert_type(equal_expr.lhs().type());
4771 out << ' ';
4772 if(
4773 equal_expr.lhs().type().id() != ID_array ||
4774 use_array_theory(prepared_rhs))
4775 {
4776 convert_expr(prepared_rhs);
4777 }
4778 else
4779 {
4780 unflatten(wheret::BEGIN, equal_expr.lhs().type());
4781
4782 convert_expr(prepared_rhs);
4783
4784 unflatten(wheret::END, equal_expr.lhs().type());
4785 }
4786 out << ')' << '\n';
4787 }
4788
4789 return; // done
4790 }
4791 }
4792 }
4793
4794 exprt prepared_expr = prepare_for_convert_expr(expr);
4795
4796#if 0
4797 out << "; CONV: "
4798 << format(expr) << "\n";
4799#endif
4800
4801 out << "; set_to " << (value?"true":"false") << "\n"
4802 << "(assert ";
4803 if(!value)
4804 {
4805 out << "(not ";
4806 }
4807 const auto found_literal = defined_expressions.find(expr);
4808 if(!(found_literal == defined_expressions.end()))
4809 {
4810 // This is a converted expression, we can just assert the literal name
4811 // since the expression is already defined
4812 out << found_literal->second;
4813 set_values[found_literal->second] = value;
4814 }
4815 else
4816 {
4817 convert_expr(prepared_expr);
4818 }
4819 if(!value)
4820 {
4821 out << ")";
4822 }
4823 out << ")\n";
4824 return;
4825}
4826
4834{
4835 exprt lowered_expr = expr;
4836
4837 for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
4838 it != itend;
4839 ++it)
4840 {
4841 if(
4842 it->id() == ID_byte_extract_little_endian ||
4843 it->id() == ID_byte_extract_big_endian)
4844 {
4845 it.mutate() = lower_byte_extract(to_byte_extract_expr(*it), ns);
4846 }
4847 else if(
4848 it->id() == ID_byte_update_little_endian ||
4849 it->id() == ID_byte_update_big_endian)
4850 {
4851 it.mutate() = lower_byte_update(to_byte_update_expr(*it), ns);
4852 }
4853 }
4854
4855 return lowered_expr;
4856}
4857
4866{
4867 // First, replace byte operators, because they may introduce new array
4868 // expressions that must be seen by find_symbols:
4869 exprt lowered_expr = lower_byte_operators(expr);
4870 INVARIANT(
4871 !has_byte_operator(lowered_expr),
4872 "lower_byte_operators should remove all byte operators");
4873
4874 // Perform rewrites that may introduce new symbols
4875 for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
4876 it != itend;) // no ++it
4877 {
4878 if(
4879 auto prophecy_r_or_w_ok =
4881 {
4882 exprt lowered = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns);
4883 it.mutate() = lowered;
4884 it.next_sibling_or_parent();
4885 }
4886 else if(
4887 auto prophecy_pointer_in_range =
4889 {
4890 exprt lowered = simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
4891 it.mutate() = lowered;
4892 it.next_sibling_or_parent();
4893 }
4894 else
4895 ++it;
4896 }
4897
4898 // Now create symbols for all composite expressions present in lowered_expr:
4899 find_symbols(lowered_expr);
4900
4901 return lowered_expr;
4902}
4903
4905{
4906 if(is_zero_width(expr.type(), ns))
4907 return;
4908
4909 // recursive call on type
4910 find_symbols(expr.type());
4911
4912 if(expr.id() == ID_exists || expr.id() == ID_forall)
4913 {
4914 std::unordered_map<irep_idt, std::optional<identifiert>> shadowed_syms;
4915
4916 // do not declare the quantified symbol, but record
4917 // as 'bound symbol'
4918 const auto &q_expr = to_quantifier_expr(expr);
4919 for(const auto &symbol : q_expr.variables())
4920 {
4921 const auto identifier = symbol.get_identifier();
4922 auto id_entry =
4923 identifier_map.insert({identifier, identifiert{symbol.type(), true}});
4924 shadowed_syms.insert(
4925 {identifier,
4926 id_entry.second ? std::nullopt
4927 : std::optional{id_entry.first->second}});
4928 }
4929 find_symbols(q_expr.where());
4930 for(const auto &[id, shadowed_val] : shadowed_syms)
4931 {
4932 auto previous_entry = identifier_map.find(id);
4933 if(!shadowed_val.has_value())
4934 identifier_map.erase(previous_entry);
4935 else
4936 previous_entry->second = std::move(*shadowed_val);
4937 }
4938 return;
4939 }
4940
4941 // recursive call on operands
4942 for(const auto &op : expr.operands())
4943 find_symbols(op);
4944
4945 if(expr.id()==ID_symbol ||
4946 expr.id()==ID_nondet_symbol)
4947 {
4948 // we don't track function-typed symbols
4949 if(expr.type().id()==ID_code)
4950 return;
4951
4952 irep_idt identifier;
4953
4954 if(expr.id()==ID_symbol)
4955 identifier=to_symbol_expr(expr).get_identifier();
4956 else
4957 identifier="nondet_"+
4958 id2string(to_nondet_symbol_expr(expr).get_identifier());
4959
4960 auto id_entry =
4961 identifier_map.insert({identifier, identifiert{expr.type(), false}});
4962
4963 if(id_entry.second)
4964 {
4965 std::string smt2_identifier=convert_identifier(identifier);
4966 smt2_identifiers.insert(smt2_identifier);
4967
4968 out << "; find_symbols\n";
4969 out << "(declare-fun " << smt2_identifier;
4970
4971 if(expr.type().id() == ID_mathematical_function)
4972 {
4973 auto &mathematical_function_type =
4975 out << " (";
4976 bool first = true;
4977
4978 for(auto &type : mathematical_function_type.domain())
4979 {
4980 if(first)
4981 first = false;
4982 else
4983 out << ' ';
4984 convert_type(type);
4985 }
4986
4987 out << ") ";
4988 convert_type(mathematical_function_type.codomain());
4989 }
4990 else
4991 {
4992 out << " () ";
4993 convert_type(expr.type());
4994 }
4995
4996 out << ")" << "\n";
4997 }
4998 }
4999 else if(expr.id() == ID_array_of)
5000 {
5001 if(!use_as_const)
5002 {
5003 if(defined_expressions.find(expr) == defined_expressions.end())
5004 {
5005 const auto &array_of = to_array_of_expr(expr);
5006 const auto &array_type = array_of.type();
5007
5008 const irep_idt id =
5009 "array_of." + std::to_string(defined_expressions.size());
5010 out << "; the following is a substitute for lambda i. x\n";
5011 out << "(declare-fun " << id << " () ";
5012 convert_type(array_type);
5013 out << ")\n";
5014
5015 if(!is_zero_width(array_type.element_type(), ns))
5016 {
5017 // use a quantifier-based initialization instead of lambda
5018 out << "(assert (forall ((i ";
5019 convert_type(array_type.index_type());
5020 out << ")) (= (select " << id << " i) ";
5021 if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
5022 {
5023 out << "(ite ";
5024 convert_expr(array_of.what());
5025 out << " #b1 #b0)";
5026 }
5027 else
5028 {
5029 convert_expr(array_of.what());
5030 }
5031 out << ")))\n";
5032 }
5033
5034 defined_expressions[expr] = id;
5035 }
5036 }
5037 }
5038 else if(expr.id() == ID_array_comprehension)
5039 {
5041 {
5042 if(defined_expressions.find(expr) == defined_expressions.end())
5043 {
5044 const auto &array_comprehension = to_array_comprehension_expr(expr);
5045 const auto &array_type = array_comprehension.type();
5046 const auto &array_size = array_type.size();
5047
5048 const irep_idt id =
5049 "array_comprehension." + std::to_string(defined_expressions.size());
5050 out << "(declare-fun " << id << " () ";
5051 convert_type(array_type);
5052 out << ")\n";
5053
5054 out << "; the following is a substitute for lambda i . x(i)\n";
5055 out << "; universally quantified initialization of the array\n";
5056 out << "(assert (forall ((";
5057 convert_expr(array_comprehension.arg());
5058 out << " ";
5059 convert_type(array_size.type());
5060 out << ")) (=> (and (bvule (_ bv0 " << boolbv_width(array_size.type())
5061 << ") ";
5062 convert_expr(array_comprehension.arg());
5063 out << ") (bvult ";
5064 convert_expr(array_comprehension.arg());
5065 out << " ";
5066 convert_expr(array_size);
5067 out << ")) (= (select " << id << " ";
5068 convert_expr(array_comprehension.arg());
5069 out << ") ";
5070 if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
5071 {
5072 out << "(ite ";
5073 convert_expr(array_comprehension.body());
5074 out << " #b1 #b0)";
5075 }
5076 else
5077 {
5078 convert_expr(array_comprehension.body());
5079 }
5080 out << "))))\n";
5081
5082 defined_expressions[expr] = id;
5083 }
5084 }
5085 }
5086 else if(expr.id()==ID_array)
5087 {
5088 if(defined_expressions.find(expr)==defined_expressions.end())
5089 {
5090 const array_typet &array_type=to_array_type(expr.type());
5091
5092 const irep_idt id = "array." + std::to_string(defined_expressions.size());
5093 out << "; the following is a substitute for an array constructor" << "\n";
5094 out << "(declare-fun " << id << " () ";
5095 convert_type(array_type);
5096 out << ")" << "\n";
5097
5098 if(!is_zero_width(array_type.element_type(), ns))
5099 {
5100 for(std::size_t i = 0; i < expr.operands().size(); i++)
5101 {
5102 out << "(assert (= (select " << id << " ";
5103 convert_expr(from_integer(i, array_type.index_type()));
5104 out << ") "; // select
5105 if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
5106 {
5107 out << "(ite ";
5108 convert_expr(expr.operands()[i]);
5109 out << " #b1 #b0)";
5110 }
5111 else
5112 {
5113 convert_expr(expr.operands()[i]);
5114 }
5115 out << "))"
5116 << "\n"; // =, assert
5117 }
5118 }
5119
5120 defined_expressions[expr]=id;
5121 }
5122 }
5123 else if(expr.id()==ID_string_constant)
5124 {
5125 if(defined_expressions.find(expr)==defined_expressions.end())
5126 {
5127 // introduce a temporary array.
5129 const array_typet &array_type=to_array_type(tmp.type());
5130
5131 const irep_idt id =
5132 "string." + std::to_string(defined_expressions.size());
5133 out << "; the following is a substitute for a string" << "\n";
5134 out << "(declare-fun " << id << " () ";
5135 convert_type(array_type);
5136 out << ")" << "\n";
5137
5138 for(std::size_t i=0; i<tmp.operands().size(); i++)
5139 {
5140 out << "(assert (= (select " << id << ' ';
5141 convert_expr(from_integer(i, array_type.index_type()));
5142 out << ") "; // select
5143 convert_expr(tmp.operands()[i]);
5144 out << "))" << "\n";
5145 }
5146
5147 defined_expressions[expr]=id;
5148 }
5149 }
5150 else if(
5152 {
5153 if(object_sizes.find(*object_size) == object_sizes.end())
5154 {
5155 const irep_idt id = convert_identifier(
5156 "object_size." + std::to_string(object_sizes.size()));
5157 out << "(declare-fun " << id << " () ";
5159 out << ")"
5160 << "\n";
5161
5163 }
5164 }
5165 // clang-format off
5166 else if(!use_FPA_theory &&
5167 expr.operands().size() >= 1 &&
5168 (expr.id() == ID_floatbv_plus ||
5169 expr.id() == ID_floatbv_minus ||
5170 expr.id() == ID_floatbv_mult ||
5171 expr.id() == ID_floatbv_div ||
5172 expr.id() == ID_floatbv_typecast ||
5173 expr.id() == ID_ieee_float_equal ||
5174 expr.id() == ID_ieee_float_notequal ||
5175 ((expr.id() == ID_lt ||
5176 expr.id() == ID_gt ||
5177 expr.id() == ID_le ||
5178 expr.id() == ID_ge ||
5179 expr.id() == ID_isnan ||
5180 expr.id() == ID_isnormal ||
5181 expr.id() == ID_isfinite ||
5182 expr.id() == ID_isinf ||
5183 expr.id() == ID_sign ||
5184 expr.id() == ID_unary_minus ||
5185 expr.id() == ID_typecast ||
5186 expr.id() == ID_abs) &&
5187 to_multi_ary_expr(expr).op0().type().id() == ID_floatbv)))
5188 // clang-format on
5189 {
5190 irep_idt function =
5191 convert_identifier("float_bv." + expr.id_string() + floatbv_suffix(expr));
5192
5193 if(bvfp_set.insert(function).second)
5194 {
5195 out << "; this is a model for " << expr.id() << " : "
5196 << type2id(to_multi_ary_expr(expr).op0().type()) << " -> "
5197 << type2id(expr.type()) << "\n"
5198 << "(define-fun " << function << " (";
5199
5200 for(std::size_t i = 0; i < expr.operands().size(); i++)
5201 {
5202 if(i!=0)
5203 out << " ";
5204 out << "(op" << i << ' ';
5205 convert_type(expr.operands()[i].type());
5206 out << ')';
5207 }
5208
5209 out << ") ";
5210 convert_type(expr.type()); // return type
5211 out << ' ';
5212
5213 exprt tmp1=expr;
5214 for(std::size_t i = 0; i < tmp1.operands().size(); i++)
5215 tmp1.operands()[i]=
5216 smt2_symbolt("op"+std::to_string(i), tmp1.operands()[i].type());
5217
5218 exprt tmp2=float_bv(tmp1);
5219 tmp2=letify(tmp2);
5220 CHECK_RETURN(!tmp2.is_nil());
5221
5222 convert_expr(tmp2);
5223
5224 out << ")\n"; // define-fun
5225 }
5226 }
5227 else if(
5228 use_FPA_theory && expr.id() == ID_typecast &&
5229 to_typecast_expr(expr).op().type().id() == ID_floatbv &&
5230 expr.type().id() == ID_bv)
5231 {
5232 // This is _NOT_ a semantic conversion, but bit-wise.
5233 if(defined_expressions.find(expr) == defined_expressions.end())
5234 {
5235 // This conversion is non-trivial as it requires creating a
5236 // new bit-vector variable and then asserting that it converts
5237 // to the required floating-point number.
5238 const irep_idt id =
5239 "bvfromfloat." + std::to_string(defined_expressions.size());
5240 out << "(declare-fun " << id << " () ";
5241 convert_type(expr.type());
5242 out << ')' << '\n';
5243
5244 const typecast_exprt &tc = to_typecast_expr(expr);
5245 const auto &floatbv_type = to_floatbv_type(tc.op().type());
5246 out << "(assert (= ";
5247 out << "((_ to_fp " << floatbv_type.get_e() << " "
5248 << floatbv_type.get_f() + 1 << ") " << id << ')';
5249 convert_expr(tc.op());
5250 out << ')'; // =
5251 out << ')' << '\n';
5252
5253 defined_expressions[expr] = id;
5254 }
5255 }
5256 else if(expr.id() == ID_initial_state)
5257 {
5258 irep_idt function = "initial-state";
5259
5260 if(state_fkt_declared.insert(function).second)
5261 {
5262 out << "(declare-fun " << function << " (";
5263 convert_type(to_unary_expr(expr).op().type());
5264 out << ") ";
5265 convert_type(expr.type()); // return type
5266 out << ")\n"; // declare-fun
5267 }
5268 }
5269 else if(expr.id() == ID_evaluate)
5270 {
5271 irep_idt function = "evaluate-" + type2id(expr.type());
5272
5273 if(state_fkt_declared.insert(function).second)
5274 {
5275 out << "(declare-fun " << function << " (";
5276 convert_type(to_binary_expr(expr).op0().type());
5277 out << ' ';
5278 convert_type(to_binary_expr(expr).op1().type());
5279 out << ") ";
5280 convert_type(expr.type()); // return type
5281 out << ")\n"; // declare-fun
5282 }
5283 }
5284 else if(
5285 expr.id() == ID_state_is_cstring ||
5286 expr.id() == ID_state_is_dynamic_object ||
5287 expr.id() == ID_state_live_object || expr.id() == ID_state_writeable_object)
5288 {
5289 irep_idt function =
5290 expr.id() == ID_state_is_cstring ? "state-is-cstring"
5291 : expr.id() == ID_state_is_dynamic_object ? "state-is-dynamic-object"
5292 : expr.id() == ID_state_live_object ? "state-live-object"
5293 : "state-writeable-object";
5294
5295 if(state_fkt_declared.insert(function).second)
5296 {
5297 out << "(declare-fun " << function << " (";
5298 convert_type(to_binary_expr(expr).op0().type());
5299 out << ' ';
5300 convert_type(to_binary_expr(expr).op1().type());
5301 out << ") ";
5302 convert_type(expr.type()); // return type
5303 out << ")\n"; // declare-fun
5304 }
5305 }
5306 else if(
5307 expr.id() == ID_state_r_ok || expr.id() == ID_state_w_ok ||
5308 expr.id() == ID_state_rw_ok)
5309 {
5310 irep_idt function = expr.id() == ID_state_r_ok ? "state-r-ok"
5311 : expr.id() == ID_state_w_ok ? "state-w-ok"
5312 : "state-rw-ok";
5313
5314 if(state_fkt_declared.insert(function).second)
5315 {
5316 out << "(declare-fun " << function << " (";
5317 convert_type(to_ternary_expr(expr).op0().type());
5318 out << ' ';
5319 convert_type(to_ternary_expr(expr).op1().type());
5320 out << ' ';
5321 convert_type(to_ternary_expr(expr).op2().type());
5322 out << ") ";
5323 convert_type(expr.type()); // return type
5324 out << ")\n"; // declare-fun
5325 }
5326 }
5327 else if(expr.id() == ID_update_state)
5328 {
5329 irep_idt function =
5330 "update-state-" + type2id(to_multi_ary_expr(expr).op2().type());
5331
5332 if(state_fkt_declared.insert(function).second)
5333 {
5334 out << "(declare-fun " << function << " (";
5335 convert_type(to_multi_ary_expr(expr).op0().type());
5336 out << ' ';
5337 convert_type(to_multi_ary_expr(expr).op1().type());
5338 out << ' ';
5339 convert_type(to_multi_ary_expr(expr).op2().type());
5340 out << ") ";
5341 convert_type(expr.type()); // return type
5342 out << ")\n"; // declare-fun
5343 }
5344 }
5345 else if(expr.id() == ID_enter_scope_state)
5346 {
5347 irep_idt function =
5348 "enter-scope-state-" + type2id(to_binary_expr(expr).op1().type());
5349
5350 if(state_fkt_declared.insert(function).second)
5351 {
5352 out << "(declare-fun " << function << " (";
5353 convert_type(to_binary_expr(expr).op0().type());
5354 out << ' ';
5355 convert_type(to_binary_expr(expr).op1().type());
5356 out << ' ';
5358 out << ") ";
5359 convert_type(expr.type()); // return type
5360 out << ")\n"; // declare-fun
5361 }
5362 }
5363 else if(expr.id() == ID_exit_scope_state)
5364 {
5365 irep_idt function =
5366 "exit-scope-state-" + type2id(to_binary_expr(expr).op1().type());
5367
5368 if(state_fkt_declared.insert(function).second)
5369 {
5370 out << "(declare-fun " << function << " (";
5371 convert_type(to_binary_expr(expr).op0().type());
5372 out << ' ';
5373 convert_type(to_binary_expr(expr).op1().type());
5374 out << ") ";
5375 convert_type(expr.type()); // return type
5376 out << ")\n"; // declare-fun
5377 }
5378 }
5379 else if(expr.id() == ID_allocate)
5380 {
5381 irep_idt function = "allocate";
5382
5383 if(state_fkt_declared.insert(function).second)
5384 {
5385 out << "(declare-fun " << function << " (";
5386 convert_type(to_binary_expr(expr).op0().type());
5387 out << ' ';
5388 convert_type(to_binary_expr(expr).op1().type());
5389 out << ") ";
5390 convert_type(expr.type()); // return type
5391 out << ")\n"; // declare-fun
5392 }
5393 }
5394 else if(expr.id() == ID_reallocate)
5395 {
5396 irep_idt function = "reallocate";
5397
5398 if(state_fkt_declared.insert(function).second)
5399 {
5400 out << "(declare-fun " << function << " (";
5401 convert_type(to_ternary_expr(expr).op0().type());
5402 out << ' ';
5403 convert_type(to_ternary_expr(expr).op1().type());
5404 out << ' ';
5405 convert_type(to_ternary_expr(expr).op2().type());
5406 out << ") ";
5407 convert_type(expr.type()); // return type
5408 out << ")\n"; // declare-fun
5409 }
5410 }
5411 else if(expr.id() == ID_deallocate_state)
5412 {
5413 irep_idt function = "deallocate";
5414
5415 if(state_fkt_declared.insert(function).second)
5416 {
5417 out << "(declare-fun " << function << " (";
5418 convert_type(to_binary_expr(expr).op0().type());
5419 out << ' ';
5420 convert_type(to_binary_expr(expr).op1().type());
5421 out << ") ";
5422 convert_type(expr.type()); // return type
5423 out << ")\n"; // declare-fun
5424 }
5425 }
5426 else if(expr.id() == ID_object_address)
5427 {
5428 irep_idt function = "object-address";
5429
5430 if(state_fkt_declared.insert(function).second)
5431 {
5432 out << "(declare-fun " << function << " (String) ";
5433 convert_type(expr.type()); // return type
5434 out << ")\n"; // declare-fun
5435 }
5436 }
5437 else if(expr.id() == ID_field_address)
5438 {
5439 irep_idt function = "field-address-" + type2id(expr.type());
5440
5441 if(state_fkt_declared.insert(function).second)
5442 {
5443 out << "(declare-fun " << function << " (";
5444 convert_type(to_field_address_expr(expr).op().type());
5445 out << ' ';
5446 out << "String";
5447 out << ") ";
5448 convert_type(expr.type()); // return type
5449 out << ")\n"; // declare-fun
5450 }
5451 }
5452 else if(expr.id() == ID_element_address)
5453 {
5454 irep_idt function = "element-address-" + type2id(expr.type());
5455
5456 if(state_fkt_declared.insert(function).second)
5457 {
5458 out << "(declare-fun " << function << " (";
5459 convert_type(to_element_address_expr(expr).base().type());
5460 out << ' ';
5461 convert_type(to_element_address_expr(expr).index().type());
5462 out << ' '; // repeat, for the element size
5463 convert_type(to_element_address_expr(expr).index().type());
5464 out << ") ";
5465 convert_type(expr.type()); // return type
5466 out << ")\n"; // declare-fun
5467 }
5468 }
5469}
5470
5472{
5473 const typet &type = expr.type();
5474 PRECONDITION(type.id()==ID_array);
5475
5476 // arrays inside structs get flattened, unless we have datatypes
5477 if(expr.id() == ID_with)
5478 return use_array_theory(to_with_expr(expr).old());
5479 else
5480 return use_datatypes || expr.id() != ID_member;
5481}
5482
5484{
5485 if(type.id()==ID_array)
5486 {
5487 const array_typet &array_type=to_array_type(type);
5488 CHECK_RETURN(array_type.size().is_not_nil());
5489
5490 // we always use array theory for top-level arrays
5491 const typet &subtype = array_type.element_type();
5492
5493 // Arrays map the index type to the element type.
5494 out << "(Array ";
5495 convert_type(array_type.index_type());
5496 out << " ";
5497
5498 if(subtype.id()==ID_bool && !use_array_of_bool)
5499 out << "(_ BitVec 1)";
5500 else
5501 convert_type(array_type.element_type());
5502
5503 out << ")";
5504 }
5505 else if(type.id()==ID_bool)
5506 {
5507 out << "Bool";
5508 }
5509 else if(type.id() == ID_struct || type.id() == ID_struct_tag)
5510 {
5511 if(use_datatypes)
5512 {
5513 out << datatype_map.at(type);
5514 }
5515 else
5516 {
5517 std::size_t width=boolbv_width(type);
5518
5519 out << "(_ BitVec " << width << ")";
5520 }
5521 }
5522 else if(type.id()==ID_code)
5523 {
5524 // These may appear in structs.
5525 // We replace this by "Bool" in order to keep the same
5526 // member count.
5527 out << "Bool";
5528 }
5529 else if(type.id() == ID_union || type.id() == ID_union_tag)
5530 {
5531 std::size_t width=boolbv_width(type);
5532 const union_typet &union_type = type.id() == ID_union_tag
5534 : to_union_type(type);
5536 union_type.components().empty() || width != 0,
5537 "failed to get width of union");
5538
5539 out << "(_ BitVec " << width << ")";
5540 }
5541 else if(type.id()==ID_pointer)
5542 {
5543 out << "(_ BitVec "
5544 << boolbv_width(type) << ")";
5545 }
5546 else if(type.id()==ID_bv ||
5547 type.id()==ID_fixedbv ||
5548 type.id()==ID_unsignedbv ||
5549 type.id()==ID_signedbv ||
5550 type.id()==ID_c_bool)
5551 {
5552 out << "(_ BitVec "
5553 << to_bitvector_type(type).get_width() << ")";
5554 }
5555 else if(type.id()==ID_c_enum)
5556 {
5557 // these have an underlying type
5558 out << "(_ BitVec "
5559 << to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width()
5560 << ")";
5561 }
5562 else if(type.id()==ID_c_enum_tag)
5563 {
5565 }
5566 else if(type.id()==ID_floatbv)
5567 {
5568 const floatbv_typet &floatbv_type=to_floatbv_type(type);
5569
5570 if(use_FPA_theory)
5571 out << "(_ FloatingPoint "
5572 << floatbv_type.get_e() << " "
5573 << floatbv_type.get_f() + 1 << ")";
5574 else
5575 out << "(_ BitVec "
5576 << floatbv_type.get_width() << ")";
5577 }
5578 else if(type.id()==ID_rational ||
5579 type.id()==ID_real)
5580 out << "Real";
5581 else if(type.id()==ID_integer)
5582 out << "Int";
5583 else if(type.id()==ID_complex)
5584 {
5585 if(use_datatypes)
5586 {
5587 out << datatype_map.at(type);
5588 }
5589 else
5590 {
5591 std::size_t width=boolbv_width(type);
5592
5593 out << "(_ BitVec " << width << ")";
5594 }
5595 }
5596 else if(type.id()==ID_c_bit_field)
5597 {
5599 }
5600 else if(type.id() == ID_state)
5601 {
5602 out << "state";
5603 }
5604 else
5605 {
5606 UNEXPECTEDCASE("unsupported type: "+type.id_string());
5607 }
5608}
5609
5611{
5612 std::set<irep_idt> recstack;
5613 find_symbols_rec(type, recstack);
5614}
5615
5617 const typet &type,
5618 std::set<irep_idt> &recstack)
5619{
5620 if(type.id()==ID_array)
5621 {
5622 const array_typet &array_type=to_array_type(type);
5623 find_symbols(array_type.size());
5624 find_symbols_rec(array_type.element_type(), recstack);
5625 }
5626 else if(type.id()==ID_complex)
5627 {
5628 find_symbols_rec(to_complex_type(type).subtype(), recstack);
5629
5630 if(use_datatypes &&
5631 datatype_map.find(type)==datatype_map.end())
5632 {
5633 const std::string smt_typename =
5634 "complex." + std::to_string(datatype_map.size());
5635 datatype_map[type] = smt_typename;
5636
5637 out << "(declare-datatypes ((" << smt_typename << " 0)) "
5638 << "(((mk-" << smt_typename;
5639
5640 out << " (" << smt_typename << ".imag ";
5641 convert_type(to_complex_type(type).subtype());
5642 out << ")";
5643
5644 out << " (" << smt_typename << ".real ";
5645 convert_type(to_complex_type(type).subtype());
5646 out << ")";
5647
5648 out << "))))\n";
5649 }
5650 }
5651 else if(type.id() == ID_struct)
5652 {
5653 // Cater for mutually recursive struct types
5654 bool need_decl=false;
5655 if(use_datatypes &&
5656 datatype_map.find(type)==datatype_map.end())
5657 {
5658 const std::string smt_typename =
5659 "struct." + std::to_string(datatype_map.size());
5660 datatype_map[type] = smt_typename;
5661 need_decl=true;
5662 }
5663
5664 const struct_typet::componentst &components =
5665 to_struct_type(type).components();
5666
5667 for(const auto &component : components)
5668 find_symbols_rec(component.type(), recstack);
5669
5670 // Declare the corresponding SMT type if we haven't already.
5671 if(need_decl)
5672 {
5673 const std::string &smt_typename = datatype_map.at(type);
5674
5675 // We're going to create a datatype named something like `struct.0'.
5676 // It's going to have a single constructor named `mk-struct.0' with an
5677 // argument for each member of the struct. The declaration that
5678 // creates this type looks like:
5679 //
5680 // (declare-datatypes ((struct.0 0)) (((mk-struct.0
5681 // (struct.0.component1 type1)
5682 // ...
5683 // (struct.0.componentN typeN)))))
5684 out << "(declare-datatypes ((" << smt_typename << " 0)) "
5685 << "(((mk-" << smt_typename << " ";
5686
5687 for(const auto &component : components)
5688 {
5689 if(is_zero_width(component.type(), ns))
5690 continue;
5691
5692 out << "(" << smt_typename << "." << component.get_name()
5693 << " ";
5694 convert_type(component.type());
5695 out << ") ";
5696 }
5697
5698 out << "))))" << "\n";
5699
5700 // Let's also declare convenience functions to update individual
5701 // members of the struct whil we're at it. The functions are
5702 // named like `update-struct.0.component1'. Their declarations
5703 // look like:
5704 //
5705 // (declare-fun update-struct.0.component1
5706 // ((s struct.0) ; first arg -- the struct to update
5707 // (v type1)) ; second arg -- the value to update
5708 // struct.0 ; the output type
5709 // (mk-struct.0 ; build the new struct...
5710 // v ; the updated value
5711 // (struct.0.component2 s) ; retain the other members
5712 // ...
5713 // (struct.0.componentN s)))
5714
5715 for(struct_union_typet::componentst::const_iterator
5716 it=components.begin();
5717 it!=components.end();
5718 ++it)
5719 {
5720 if(is_zero_width(it->type(), ns))
5721 continue;
5722
5724 out << "(define-fun update-" << smt_typename << "."
5725 << component.get_name() << " "
5726 << "((s " << smt_typename << ") "
5727 << "(v ";
5728 convert_type(component.type());
5729 out << ")) " << smt_typename << " "
5730 << "(mk-" << smt_typename
5731 << " ";
5732
5733 for(struct_union_typet::componentst::const_iterator
5734 it2=components.begin();
5735 it2!=components.end();
5736 ++it2)
5737 {
5738 if(it==it2)
5739 out << "v ";
5740 else if(!is_zero_width(it2->type(), ns))
5741 {
5742 out << "(" << smt_typename << "."
5743 << it2->get_name() << " s) ";
5744 }
5745 }
5746
5747 out << "))" << "\n";
5748 }
5749
5750 out << "\n";
5751 }
5752 }
5753 else if(type.id() == ID_union)
5754 {
5755 const union_typet::componentst &components =
5756 to_union_type(type).components();
5757
5758 for(const auto &component : components)
5759 find_symbols_rec(component.type(), recstack);
5760 }
5761 else if(type.id()==ID_code)
5762 {
5763 const code_typet::parameterst &parameters=
5764 to_code_type(type).parameters();
5765 for(const auto &param : parameters)
5766 find_symbols_rec(param.type(), recstack);
5767
5768 find_symbols_rec(to_code_type(type).return_type(), recstack);
5769 }
5770 else if(type.id()==ID_pointer)
5771 {
5772 find_symbols_rec(to_pointer_type(type).base_type(), recstack);
5773 }
5774 else if(type.id() == ID_struct_tag)
5775 {
5776 const auto &struct_tag = to_struct_tag_type(type);
5777 const irep_idt &id = struct_tag.get_identifier();
5778
5779 if(recstack.find(id) == recstack.end())
5780 {
5781 const auto &base_struct = ns.follow_tag(struct_tag);
5782 recstack.insert(id);
5783 find_symbols_rec(base_struct, recstack);
5784 datatype_map[type] = datatype_map[base_struct];
5785 }
5786 }
5787 else if(type.id() == ID_union_tag)
5788 {
5789 const auto &union_tag = to_union_tag_type(type);
5790 const irep_idt &id = union_tag.get_identifier();
5791
5792 if(recstack.find(id) == recstack.end())
5793 {
5794 recstack.insert(id);
5795 find_symbols_rec(ns.follow_tag(union_tag), recstack);
5796 }
5797 }
5798 else if(type.id() == ID_state)
5799 {
5800 if(datatype_map.find(type) == datatype_map.end())
5801 {
5802 datatype_map[type] = "state";
5803 out << "(declare-sort state 0)\n";
5804 }
5805 }
5806 else if(type.id() == ID_mathematical_function)
5807 {
5808 const auto &mathematical_function_type =
5810 for(auto &d_type : mathematical_function_type.domain())
5811 find_symbols_rec(d_type, recstack);
5812
5813 find_symbols_rec(mathematical_function_type.codomain(), recstack);
5814 }
5815}
5816
5818{
5820}
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)
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 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:1616
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:33
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:3130
variablest & variables()
Definition std_expr.h:3120
Bit-wise negation of bit-vectors.
std::size_t get_width() const
Definition std_types.h:920
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:2987
const irep_idt & get_value() const
Definition std_expr.h:2995
void set_value(const irep_idt &value)
Definition std_expr.h:3000
resultt
Result of running the decision procedure.
Division.
Definition std_expr.h:1152
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:1361
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1291
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:3064
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:2370
exprt & cond()
Definition std_expr.h:2387
exprt & false_case()
Definition std_expr.h:2407
exprt & true_case()
Definition std_expr.h:2397
Boolean implication.
Definition std_expr.h:2183
Array index operator.
Definition std_expr.h:1465
exprt & index()
Definition std_expr.h:1505
exprt & array()
Definition std_expr.h:1495
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:3196
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3277
operandst & values()
Definition std_expr.h:3266
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3289
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:2841
const exprt & struct_op() const
Definition std_expr.h:2879
irep_idt get_component_name() const
Definition std_expr.h:2863
Binary minus.
Definition std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1223
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:3073
const irep_idt & get_identifier() const
Definition std_expr.h:320
Boolean negation.
Definition std_expr.h:2327
Disequality.
Definition std_expr.h:1420
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:1872
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:63
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:3055
Definition threeval.h:20
Semantic type conversion.
Definition std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2076
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:1765
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:2655
Operator to update elements in structs and arrays.
Definition std_expr.h:2471
exprt & new_value()
Definition std_expr.h:2501
exprt & where()
Definition std_expr.h:2491
exprt & old()
Definition std_expr.h:2481
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
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
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:80
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1895
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1598
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:1533
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1272
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1132
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3472
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:3654
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2102
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1201
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:1445
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:3320
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:2450
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2933
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:1811
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3037
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2352
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:2533
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2208
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2735
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:1402
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:1340
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:1146
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