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