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