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