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)
197 convert_literal(to_literal_expr(assumption).get_literal());
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)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
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)
Definition: base_type.cpp:109
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
Definition: bytecode_info.h:60
int8_t s1
Definition: bytecode_info.h:59
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.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
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.
Definition: floatbv_expr.h:19
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)...
Definition: floatbv_expr.h:364
exprt & rounding_mode()
Definition: floatbv_expr.h:395
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
Definition: ieee_float.cpp:703
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
Definition: ieee_float.cpp:375
void build(const mp_integer &exp, const mp_integer &frac)
Definition: ieee_float.cpp:473
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.
Definition: floatbv_expr.h:176
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
Evaluates to true if the operand is NaN.
Definition: floatbv_expr.h:88
Evaluates to true if the operand is a normal number.
Definition: floatbv_expr.h:220
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
Definition: literal_expr.h:26
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
Definition: pointer_logic.h:64
numberingt< exprt, irep_hash > objects
Definition: pointer_logic.h:26
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 ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A base class for quantifier expressions.
Bit-vector replication.
constant_exprt & times()
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
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 &)
Definition: smt2_conv.cpp:3171
bool use_lambda_for_array
Definition: smt2_conv.h:65
void convert_type(const typet &)
Definition: smt2_conv.cpp:4876
void unflatten(wheret, const typet &, unsigned nesting=0)
Definition: smt2_conv.cpp:4313
bool use_array_theory(const exprt &)
Definition: smt2_conv.cpp:4855
void find_symbols(const exprt &expr)
Definition: smt2_conv.cpp:4572
std::size_t number_of_solver_calls
Definition: smt2_conv.h:96
void convert_typecast(const typecast_exprt &expr)
Definition: smt2_conv.cpp:2150
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
Definition: smt2_conv.cpp:185
tvt l_get(literalt l) const
Definition: smt2_conv.cpp:142
void convert_floatbv_rem(const binary_exprt &expr)
Definition: smt2_conv.cpp:3788
void convert_update(const exprt &expr)
Definition: smt2_conv.cpp:4058
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)
Definition: smt2_conv.cpp:702
void push() override
Unimplemented.
Definition: smt2_conv.cpp:863
void convert_is_dynamic_object(const unary_exprt &)
Definition: smt2_conv.cpp:3134
void convert_literal(const literalt)
Definition: smt2_conv.cpp:843
void convert_floatbv_div(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3673
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
Definition: smt2_conv.cpp:5226
const namespacet & ns
Definition: smt2_conv.h:88
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3768
boolbv_widtht boolbv_width
Definition: smt2_conv.h:94
void convert_constant(const constant_exprt &expr)
Definition: smt2_conv.cpp:2955
std::string floatbv_suffix(const exprt &) const
Definition: smt2_conv.cpp:948
void flatten2bv(const exprt &)
Definition: smt2_conv.cpp:4224
std::string notes
Definition: smt2_conv.h:90
void convert_div(const div_exprt &expr)
Definition: smt2_conv.cpp:3629
std::ostream & out
Definition: smt2_conv.h:89
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
Definition: smt2_conv.cpp:4525
std::string type2id(const typet &) const
Definition: smt2_conv.cpp:911
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.
Definition: smt2_conv.cpp:3414
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: smt2_conv.cpp:2683
struct_exprt parse_struct(const irept &s, const struct_typet &type)
Definition: smt2_conv.cpp:579
std::string logic
Definition: smt2_conv.h:90
void convert_mult(const mult_exprt &expr)
Definition: smt2_conv.cpp:3693
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
Definition: smt2_conv.cpp:4557
void define_object_size(const irep_idt &id, const exprt &expr)
Definition: smt2_conv.cpp:236
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: smt2_conv.cpp:281
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_conv.cpp:127
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3609
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)
Definition: smt2_conv.cpp:3115
static std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:880
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3471
void convert_struct(const struct_exprt &expr)
Definition: smt2_conv.cpp:2827
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)
Definition: smt2_conv.cpp:4163
void convert_euclidean_mod(const euclidean_mod_exprt &expr)
Definition: smt2_conv.cpp:3100
void convert_index(const index_exprt &expr)
Definition: smt2_conv.cpp:4065
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...
Definition: smt2_conv.cpp:834
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: smt2_conv.cpp:132
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.
Definition: smt2_conv.cpp:523
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'.
Definition: smt2_conv.cpp:4417
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)
Definition: smt2_conv.cpp:638
void convert_union(const union_exprt &expr)
Definition: smt2_conv.cpp:2922
exprt parse_union(const irept &s, const union_typet &type)
Definition: smt2_conv.cpp:563
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 ...
Definition: smt2_conv.cpp:479
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
Definition: smt2_conv.cpp:2891
void convert_with(const with_exprt &expr)
Definition: smt2_conv.cpp:3811
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)
Definition: smt2_conv.cpp:3278
defined_expressionst defined_expressions
Definition: smt2_conv.h:253
void pop() override
Currently, only implements a single stack element (no nested contexts)
Definition: smt2_conv.cpp:875
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt2_conv.cpp:5020
void write_header()
Definition: smt2_conv.cpp:155
solvert solver
Definition: smt2_conv.h:91
identifier_mapt identifier_map
Definition: smt2_conv.h:237
void convert_minus(const minus_exprt &expr)
Definition: smt2_conv.cpp:3512
void convert_expr(const exprt &)
Definition: smt2_conv.cpp:989
constant_exprt parse_literal(const irept &, const typet &type)
Definition: smt2_conv.cpp:341
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)
Definition: smt2_conv.cpp:955
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: smt2_conv.cpp:274
literalt convert(const exprt &expr)
Definition: smt2_conv.cpp:794
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
Definition: std_types.cpp:253
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.
Definition: floatbv_expr.h:425
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: floatbv_expr.h:245
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: floatbv_expr.h:157
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: floatbv_expr.h:201
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: floatbv_expr.h:113
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
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)
Definition: json_expr.cpp:206
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.
Definition: literal_expr.h:56
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.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
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)
Definition: string2int.cpp:40
const string_constantt & to_string_constant(const exprt &expr)
std::size_t object_bits
Definition: config.h:321