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