cprover
Loading...
Searching...
No Matches
axioms.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Axioms
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#include "axioms.h"
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/format_expr.h>
17#include <util/namespace.h>
20#include <util/prefix.h>
22#include <util/symbol.h>
23
25
26#include "simplify_state_expr.h"
27
28#include <iostream>
29
31{
32 constraints.push_back(std::move(src));
33}
34
39
41{
42 if(src.id() == ID_array)
43 {
44 auto &array_type = to_array_type(src);
45 array_type.element_type() = replace(array_type.element_type());
46 array_type.size() = replace(array_type.size());
47 return src;
48 }
49 else if(src.id() == ID_pointer)
50 {
52 replace(to_pointer_type(src).base_type());
53 return src;
54 }
55 else
56 return src;
57}
58
60{
61 // quadratic
62 for(auto a_it = evaluate_exprs.begin(); a_it != evaluate_exprs.end(); a_it++)
63 {
64 for(auto b_it = std::next(a_it); b_it != evaluate_exprs.end(); b_it++)
65 {
66 if(a_it->state() != b_it->state())
67 continue;
68
69 auto a_op = a_it->address();
71 b_it->address(), a_it->address().type());
72 auto operands_equal = equal_exprt(a_op, b_op);
74 operands_equal,
76 *a_it, typecast_exprt::conditional_cast(*b_it, a_it->type())));
77#if 0
78 if(verbose)
79 std::cout << "EVALUATE: " << format(implication) << '\n';
80#endif
82 }
83 }
84}
85
87{
88 // quadratic
89 for(auto a_it = is_cstring_exprs.begin(); a_it != is_cstring_exprs.end();
90 a_it++)
91 {
92 for(auto b_it = std::next(a_it); b_it != is_cstring_exprs.end(); b_it++)
93 {
94 if(a_it->state() != b_it->state())
95 continue;
96 auto a_op = a_it->address();
98 b_it->address(), a_it->address().type());
99 auto operands_equal = equal_exprt(a_op, b_op);
100 auto implication =
101 implies_exprt(operands_equal, equal_exprt(*a_it, *b_it));
102 if(verbose)
103 std::cout << "IS_CSTRING: " << format(implication) << '\n';
105 }
106 }
107}
108
110{
111 // p = &"string_literal" -> live_object(ς, p)
112 for(auto a_it = live_object_exprs.begin(); a_it != live_object_exprs.end();
113 a_it++)
114 {
115 for(auto b_it = address_of_exprs.begin(); b_it != address_of_exprs.end();
116 b_it++)
117 {
118 auto pointers_equal = same_object(a_it->address(), *b_it);
119 auto implication = implies_exprt(pointers_equal, *a_it);
120 if(verbose)
121 std::cout << "LIVE_OBJECT2: " << format(implication) << '\n';
123 }
124 }
125}
126
128{
129 // quadratic
130 for(auto a_it = live_object_exprs.begin(); a_it != live_object_exprs.end();
131 a_it++)
132 {
133 for(auto b_it = std::next(a_it); b_it != live_object_exprs.end(); b_it++)
134 {
135 if(a_it->state() != b_it->state())
136 continue;
137 auto operands_equal = same_object(a_it->address(), b_it->address());
138 auto implication =
139 implies_exprt(operands_equal, equal_exprt(*a_it, *b_it));
140 if(verbose)
141 std::cout << "LIVE_OBJECT1: " << format(implication) << '\n';
143 }
144 }
145}
146
148{
149 // p = &"string_literal" -> !writeable_object(ς, p)
150 for(auto a_it = writeable_object_exprs.begin();
151 a_it != writeable_object_exprs.end();
152 a_it++)
153 {
154 for(auto b_it = address_of_exprs.begin(); b_it != address_of_exprs.end();
155 b_it++)
156 {
157 auto pointers_equal = same_object(a_it->address(), *b_it);
158 auto implication = implies_exprt(pointers_equal, not_exprt(*a_it));
159 if(verbose)
160 std::cout << "WRITEABLE_OBJECT2: " << format(implication) << '\n';
162 }
163 }
164
165 // p = &some_object -> writeable_object(ς, p) as applicable
166 for(auto a_it = object_address_exprs.begin();
167 a_it != object_address_exprs.end();
168 a_it++)
169 {
170 if(a_it->object_identifier() == "return_value")
171 continue;
172 else if(has_prefix(id2string(a_it->object_identifier()), "va_args::"))
173 continue;
174 else if(has_prefix(id2string(a_it->object_identifier()), "va_arg::"))
175 continue;
176 else if(has_prefix(id2string(a_it->object_identifier()), "va_arg_array::"))
177 continue;
178 else if(has_prefix(id2string(a_it->object_identifier()), "old::"))
179 continue;
180
181 auto &symbol = ns.lookup(a_it->object_expr());
182 bool is_const = symbol.type.get_bool(ID_C_constant);
183 for(auto b_it = writeable_object_exprs.begin();
184 b_it != writeable_object_exprs.end();
185 b_it++)
186 {
187 auto pointers_equal = same_object(*a_it, b_it->address());
188 auto rhs = is_const ? static_cast<exprt>(not_exprt(*b_it))
189 : static_cast<exprt>(*b_it);
190 auto implication = implies_exprt(pointers_equal, rhs);
191 if(verbose)
192 std::cout << "WRITEABLE_OBJECT3: " << format(implication) << '\n';
194 }
195 }
196}
197
199{
200 // quadratic
201 for(auto a_it = writeable_object_exprs.begin();
202 a_it != writeable_object_exprs.end();
203 a_it++)
204 {
205 for(auto b_it = std::next(a_it); b_it != writeable_object_exprs.end();
206 b_it++)
207 {
208 if(a_it->state() != b_it->state())
209 continue;
210 auto operands_equal = same_object(a_it->address(), b_it->address());
211 auto implication =
212 implies_exprt(operands_equal, equal_exprt(*a_it, *b_it));
213 if(verbose)
214 std::cout << "WRITEABLE_OBJECT1: " << format(implication) << '\n';
216 }
217 }
218}
219
221{
222 // quadratic
223 for(auto a_it = is_dynamic_object_exprs.begin();
224 a_it != is_dynamic_object_exprs.end();
225 a_it++)
226 {
227 for(auto b_it = std::next(a_it); b_it != is_dynamic_object_exprs.end();
228 b_it++)
229 {
230 if(a_it->state() != b_it->state())
231 continue;
232 auto operands_equal = same_object(a_it->address(), b_it->address());
233 auto implication =
234 implies_exprt(operands_equal, equal_exprt(*a_it, *b_it));
235 if(verbose)
236 std::cout << "IS_DYNAMIC_OBJECT: " << format(implication) << '\n';
238 }
239 }
240}
241
243{
244 for(const auto &src : object_size_exprs)
245 {
246 auto src_simplified = simplify_state_expr_node(src, address_taken, ns);
247 if(src_simplified != src)
248 {
249 auto equal = equal_exprt(src, src_simplified);
250 if(verbose)
251 std::cout << "OBJECT_SIZE1: " << format(equal) << '\n';
252 dest << replace(equal);
253 }
254 }
255
256 // p = &"string_literal" -> object_size(ς, p) = strlen("string_literal")+1
257 for(auto a_it = object_size_exprs.begin(); a_it != object_size_exprs.end();
258 a_it++)
259 {
260 for(auto b_it = address_of_exprs.begin(); b_it != address_of_exprs.end();
261 b_it++)
262 {
263 if(b_it->object().id() == ID_string_constant)
264 {
265 auto &string_constant = to_string_constant(b_it->object());
266 auto pointers_equal = same_object(a_it->address(), *b_it);
267 auto size_equal = equal_exprt(
268 *a_it,
269 from_integer(string_constant.get_value().size() + 1, a_it->type()));
270 auto implication = implies_exprt(pointers_equal, size_equal);
271 if(verbose)
272 std::cout << "OBJECT_SIZE2: " << format(implication) << '\n';
274 }
275 }
276 }
277}
278
280{
281 // quadratic
282 for(auto a_it = object_size_exprs.begin(); a_it != object_size_exprs.end();
283 a_it++)
284 {
285 for(auto b_it = std::next(a_it); b_it != object_size_exprs.end(); b_it++)
286 {
287 if(a_it->state() != b_it->state())
288 continue;
289 auto operands_equal = same_object(a_it->address(), b_it->address());
290 auto implication =
291 implies_exprt(operands_equal, equal_exprt(*a_it, *b_it));
292 if(verbose)
293 std::cout << "OBJECT_SIZE: " << format(implication) << '\n';
295 }
296 }
297}
298
300{
301 // quadratic
302 for(auto a_it = ok_exprs.begin(); a_it != ok_exprs.end(); a_it++)
303 {
304 for(auto b_it = std::next(a_it); b_it != ok_exprs.end(); b_it++)
305 {
306 if(a_it->id() != b_it->id())
307 continue;
308 if(a_it->state() != b_it->state())
309 continue;
310 if(a_it->size() != b_it->size())
311 continue;
312 auto a_op = a_it->address();
314 b_it->address(), a_it->address().type());
315 auto operands_equal = equal_exprt(a_op, b_op);
316 auto implication =
317 implies_exprt(operands_equal, equal_exprt(*a_it, *b_it));
318 if(verbose)
319 std::cout << "OK: " << format(implication) << '\n';
321 }
322 }
323}
324
326{
327 for(const auto &initial_state_expr : initial_state_exprs)
328 {
329 // initial_state(ς) -> ¬live_object(ς, o) for any stack-allocated object o
330 for(const auto &object : address_taken)
331 {
332 const symbolt *symbol;
333 if(ns.lookup(object.get_identifier(), symbol))
334 continue;
335
336 if(symbol->is_static_lifetime || !symbol->is_lvalue)
337 continue;
338
340 initial_state_expr.op(), object_address_exprt(object));
342 auto implication =
343 implies_exprt(initial_state_expr, not_exprt(live_object));
344 if(verbose)
345 std::cout << "INITIAL_STATE: " << format(implication) << '\n';
347 }
348 }
349}
350
352{
353 auto r = replacement_map.find(src);
354 if(r == replacement_map.end())
355 return src;
356 else
357 return r->second;
358}
359
361{
362 src.type() = replace(src.type());
363
364 if(
365 src.id() == ID_initial_state || src.id() == ID_evaluate ||
366 src.id() == ID_state_is_cstring || src.id() == ID_state_cstrlen ||
367 src.id() == ID_state_is_sentinel_dll ||
368 src.id() == ID_state_is_dynamic_object ||
369 src.id() == ID_state_object_size || src.id() == ID_state_live_object ||
370 src.id() == ID_state_writeable_object || src.id() == ID_state_r_ok ||
371 src.id() == ID_state_w_ok || src.id() == ID_state_rw_ok ||
372 src.id() == ID_allocate || src.id() == ID_reallocate)
373 {
374 auto r = replacement_map.find(src);
375 if(r == replacement_map.end())
376 {
377 auto counter = ++counters[src.id()];
378 auto s =
379 symbol_exprt(src.id_string() + std::to_string(counter), src.type());
380 replacement_map.emplace(src, s);
381
382 if(src.id() == ID_state_is_cstring)
383 {
384 if(verbose)
385 std::cout << "R " << format(s) << " --> " << format(src) << '\n';
386 }
387
388 return std::move(s);
389 }
390 else
391 return r->second;
392 }
393
394 for(auto &op : src.operands())
395 op = replace(op);
396
397 return src;
398}
399
400void axiomst::node(const exprt &src)
401{
402 if(src.id() == ID_state_is_cstring)
403 {
404 add(to_state_is_cstring_expr(src), false);
405 }
406 else if(src.id() == ID_state_is_sentinel_dll)
407 {
408 auto &is_sentinel_dll_expr = to_state_is_sentinel_dll_expr(src);
409 is_sentinel_dll_exprs.insert(is_sentinel_dll_expr);
410
411 auto ok_expr_h_size_opt = size_of_expr(
412 to_pointer_type(is_sentinel_dll_expr.head().type()).base_type(), ns);
413
414 auto ok_expr_h = state_ok_exprt(
415 ID_state_rw_ok,
416 is_sentinel_dll_expr.state(),
417 is_sentinel_dll_expr.head(),
418 *ok_expr_h_size_opt);
419
420 auto ok_expr_t_size_opt = size_of_expr(
421 to_pointer_type(is_sentinel_dll_expr.tail().type()).base_type(), ns);
422
423 auto ok_expr_t = state_ok_exprt(
424 ID_state_rw_ok,
425 is_sentinel_dll_expr.state(),
426 is_sentinel_dll_expr.tail(),
427 *ok_expr_t_size_opt);
428
429 {
430 // is_sentinel_dll(ς, h, t) ⇒ rw_ok(ς, h) ∧ rw_ok(ς, t)
431 auto instance1 =
432 replace(implies_exprt(src, and_exprt(ok_expr_h, ok_expr_t)));
433 if(verbose)
434 std::cout << "AXIOM-is-sentinel-dll-1: " << format(instance1) << "\n";
435 dest << instance1;
436 }
437
438 {
439 // rw_ok(h) ∧ rw_ok(t) ∧ ς(h->n)=t ∧ ς(t->p)=h ⇒ is_sentinel_dll(ς, h, t)
440 auto head_next = sentinel_dll_next(
441 is_sentinel_dll_expr.state(), is_sentinel_dll_expr.head(), ns);
442
443 auto tail_prev = sentinel_dll_prev(
444 is_sentinel_dll_expr.state(), is_sentinel_dll_expr.tail(), ns);
445
446 if(head_next.has_value() && tail_prev.has_value())
447 {
448 auto head_next_is_tail =
449 equal_exprt(*head_next, is_sentinel_dll_expr.tail());
450
451 auto tail_prev_is_head =
452 equal_exprt(*tail_prev, is_sentinel_dll_expr.head());
453
454 auto instance2 = replace(implies_exprt(
455 and_exprt(
456 ok_expr_h, ok_expr_t /*, head_next_is_tail, tail_prev_is_head*/),
457 src));
458
459 if(verbose)
460 std::cout << "AXIOM-is-sentinel-dll-2: " << format(instance2) << "\n";
461 dest << instance2;
462 }
463 }
464 }
465 else if(src.id() == ID_evaluate)
466 {
467 const auto &evaluate_expr = to_evaluate_expr(src);
468 evaluate_exprs.insert(evaluate_expr);
469 }
470 else if(src.id() == ID_state_live_object)
471 {
472 const auto &live_object_expr = to_state_live_object_expr(src);
473 live_object_exprs.insert(live_object_expr);
474
475 {
476 // live_object(ς, p) --> p!=0
477 auto instance = replace(
478 implies_exprt(src, not_exprt(null_object(live_object_expr.address()))));
479 if(verbose)
480 std::cout << "AXIOMc: " << format(instance) << "\n";
481 dest << instance;
482 }
483 }
484 else if(src.id() == ID_state_writeable_object)
485 {
486 const auto &writeable_object_expr = to_state_writeable_object_expr(src);
487 writeable_object_exprs.insert(writeable_object_expr);
488 }
489 else if(src.id() == ID_state_is_dynamic_object)
490 {
491 const auto &is_dynamic_object_expr = to_state_is_dynamic_object_expr(src);
492 is_dynamic_object_exprs.insert(is_dynamic_object_expr);
493 }
494 else if(src.id() == ID_allocate)
495 {
496 const auto &allocate_expr = to_allocate_expr(src);
497
498 // May need to consider failure.
499 // live_object(ς, allocate(ς, s))
500 auto live_object_expr =
501 state_live_object_exprt(allocate_expr.state(), allocate_expr);
502 live_object_exprs.insert(live_object_expr);
503 auto instance1 = replace(live_object_expr);
504 if(verbose)
505 std::cout << "ALLOCATE1: " << format(instance1) << "\n";
506 dest << instance1;
507
508 // writeable_object(ς, allocate(ς, s))
509 auto writeable_object_expr =
510 state_writeable_object_exprt(allocate_expr.state(), allocate_expr);
511 writeable_object_exprs.insert(writeable_object_expr);
512 auto instance2 = replace(writeable_object_expr);
513 if(verbose)
514 std::cout << "ALLOCATE2: " << format(instance2) << "\n";
515 dest << instance2;
516
517 // object_size(ς, allocate(ς, s)) = s
518 auto object_size_expr = state_object_size_exprt(
519 allocate_expr.state(), allocate_expr, allocate_expr.size().type());
520 object_size_exprs.insert(object_size_expr);
521 auto instance3 =
522 replace(equal_exprt(object_size_expr, allocate_expr.size()));
523 if(verbose)
524 std::cout << "ALLOCATE3: " << format(instance3) << "\n";
525 dest << instance3;
526
527 // pointer_offset(allocate(ς, s)) = 0
528 auto pointer_offset_expr = pointer_offset(allocate_expr);
529 // pointer_offset_exprs.insert(pointer_offset_expr);
530 auto instance4 = replace(equal_exprt(
531 pointer_offset_expr, from_integer(0, pointer_offset_expr.type())));
532 if(verbose)
533 std::cout << "ALLOCATE4: " << format(instance4) << "\n";
534 dest << instance4;
535
536 // is_dynamic_object(ς, allocate(ς, s))
537 auto is_dynamic_object_expr =
538 state_is_dynamic_object_exprt(allocate_expr.state(), allocate_expr);
539 is_dynamic_object_exprs.insert(is_dynamic_object_expr);
540 auto instance5 = replace(is_dynamic_object_expr);
541 if(verbose)
542 std::cout << "ALLOCATE5: " << format(instance5) << "\n";
543 dest << instance5;
544 }
545 else if(src.id() == ID_reallocate)
546 {
547 const auto &reallocate_expr = to_reallocate_expr(src);
548
549 // May need to consider failure.
550 // live_object(ς, reallocate(ς, a, s))
551 auto live_object_expr =
552 state_live_object_exprt(reallocate_expr.state(), reallocate_expr);
553 live_object_exprs.insert(live_object_expr);
554 auto instance1 = replace(live_object_expr);
555 if(verbose)
556 std::cout << "REALLOCATE1: " << format(instance1) << "\n";
557 dest << instance1;
558
559 // object_size(ς, reallocate(ς, a, s)) = s
560 auto object_size_expr = state_object_size_exprt(
561 reallocate_expr.state(), reallocate_expr, reallocate_expr.size().type());
562 object_size_exprs.insert(object_size_expr);
563 auto instance2 =
564 replace(equal_exprt(object_size_expr, reallocate_expr.size()));
565 if(verbose)
566 std::cout << "REALLOCATE2: " << format(instance2) << "\n";
567 dest << instance2;
568
569 // pointer_offset(reallocate(ς, a, s)) = 0
570 auto pointer_offset_expr = pointer_offset(reallocate_expr);
571 // pointer_offset_exprs.insert(pointer_offset_expr);
572 auto instance3 = replace(equal_exprt(
573 pointer_offset_expr, from_integer(0, pointer_offset_expr.type())));
574 if(verbose)
575 std::cout << "REALLOCATE3: " << format(instance3) << "\n";
576 dest << instance3;
577
578 // is_dynamic_object(ς, reallocate(ς, s))
579 auto is_dynamic_object_expr =
580 state_is_dynamic_object_exprt(reallocate_expr.state(), reallocate_expr);
581 is_dynamic_object_exprs.insert(is_dynamic_object_expr);
582 auto instance4 = replace(is_dynamic_object_expr);
583 if(verbose)
584 std::cout << "REALLOCATE4: " << format(instance4) << "\n";
585 dest << instance4;
586 }
587 else if(src.id() == ID_deallocate_state)
588 {
589#if 0
590 // Disabled since any other thread may have reclaimed
591 // the memory.
592 const auto &deallocate_state_expr = to_deallocate_state_expr(src);
593
594 // ¬live_object(deallocate(ς, p), p)
595 auto live_object_expr = state_live_object_exprt(
596 deallocate_state_expr, deallocate_state_expr.address());
597 live_object_exprs.insert(live_object_expr);
598 auto instance1 = replace(not_exprt(live_object_expr));
599 if(verbose)
600 std::cout << "DEALLOCATE1: " << format(instance1) << "\n";
601 dest << instance1;
602#endif
603 }
604 else if(src.id() == ID_address_of)
605 {
607 }
608 else if(src.id() == ID_object_address)
609 {
611 }
612 else if(src.id() == ID_state_object_size)
613 {
614 const auto &object_size_expr = to_state_object_size_expr(src);
615 object_size_exprs.insert(object_size_expr);
616 }
617 else if(src.id() == ID_initial_state)
618 {
620 }
621 else if(
622 src.id() == ID_state_r_ok || src.id() == ID_state_w_ok ||
623 src.id() == ID_state_rw_ok)
624 {
625 add(to_state_ok_expr(src));
626 }
627}
628
629void axiomst::add(const state_ok_exprt &ok_expr)
630{
631 if(!ok_exprs.insert(ok_expr).second)
632 return; // already there
633
634 const auto &state = ok_expr.state();
635 const auto &pointer = ok_expr.address();
636 const auto &size = ok_expr.size();
637
638 {
639 // X_ok(p, s) <-->
640 // live_object(p)
641 // ∧ offset(p)+s≤object_size(p)
642 // ∧ writeable_object(p) if applicable
643 auto live_object = state_live_object_exprt(state, pointer);
645 auto live_object_simplified =
647
648 auto writeable_object = state_writeable_object_exprt(state, pointer);
650
651 auto writeable_object_simplified =
653
654 auto ssize_type = signed_size_type();
655 auto offset = pointer_offset_exprt(pointer, ssize_type);
656 auto offset_simplified =
658 // auto lower = binary_relation_exprt(
659 // offset_simplified, ID_ge, from_integer(0, ssize_type));
660
661 auto size_type = ::size_type();
662
663 // extend one bit, to cover overflow case
664 auto size_type_ext = unsignedbv_typet(size_type.get_width() + 1);
665
666 auto object_size = state_object_size_exprt(state, pointer, size_type);
668
669 auto object_size_casted = typecast_exprt(object_size, size_type_ext);
670
671 auto offset_casted_to_unsigned =
673 auto offset_extended = typecast_exprt::conditional_cast(
674 offset_casted_to_unsigned, size_type_ext);
675 auto size_casted = typecast_exprt::conditional_cast(size, size_type_ext);
676 auto upper = binary_relation_exprt(
677 plus_exprt(offset_extended, size_casted), ID_le, object_size_casted);
678
679 auto conjunction = and_exprt(live_object_simplified, upper);
680
681 if(ok_expr.id() == ID_state_w_ok || ok_expr.id() == ID_state_rw_ok)
683
684 auto instance = replace(equal_exprt(ok_expr, conjunction));
685
686 if(verbose)
687 std::cout << "AXIOMd: " << format(instance) << "\n";
688 dest << instance;
689 }
690
691 {
692 // X_ok(ς, p) --> p!=0
693 auto instance =
694 replace(implies_exprt(ok_expr, not_exprt(null_object(pointer))));
695 if(verbose)
696 std::cout << "AXIOMe: " << format(instance) << "\n";
697 dest << instance;
698 }
699}
700
701void axiomst::add(const state_is_cstring_exprt &is_cstring_expr, bool recursive)
702{
703 if(!is_cstring_exprs.insert(is_cstring_expr).second)
704 return; // already there
705
706 {
707 // is_cstring(ς, p) ⇒ r_ok(ς, p, 1)
708 auto ok_expr = ternary_exprt(
709 ID_state_r_ok,
710 is_cstring_expr.state(),
711 is_cstring_expr.address(),
713 bool_typet());
714
715 auto instance1 = replace(implies_exprt(is_cstring_expr, ok_expr));
716 if(verbose)
717 std::cout << "AXIOMa1: " << format(instance1) << "\n";
718 dest << instance1;
719
720 auto ok_simplified = simplify_state_expr(ok_expr, address_taken, ns);
721 ok_simplified.visit_pre([this](const exprt &src) { node(src); });
722 auto instance2 = replace(implies_exprt(is_cstring_expr, ok_simplified));
723 if(verbose)
724 std::cout << "AXIOMa2: " << format(instance2) << "\n";
725 dest << instance2;
726 }
727
728 if(!recursive)
729 {
730 // is_cstring(ς, p) --> is_cstring(ς, p + 1) ∨ ς(p)=0
731 auto state = is_cstring_expr.state();
732 auto p = is_cstring_expr.address();
733 auto one = from_integer(1, signed_size_type());
734 auto p_plus_one = plus_exprt(p, one, is_cstring_expr.op1().type());
735 auto is_cstring_plus_one = state_is_cstring_exprt(state, p_plus_one);
736 auto char_type = to_pointer_type(p.type()).base_type();
737 auto zero = from_integer(0, char_type);
738 auto star_p = evaluate_exprt(state, p, char_type);
739 auto is_zero = equal_exprt(star_p, zero);
740 auto instance = replace(
741 implies_exprt(is_cstring_expr, or_exprt(is_cstring_plus_one, is_zero)));
742 if(verbose)
743 std::cout << "AXIOMb: " << format(instance) << "\n";
744 dest << instance;
745 evaluate_exprs.insert(star_p);
746 add(is_cstring_plus_one, true); // rec. call
747 }
748}
749
751{
752 for(auto &constraint : constraints)
753 {
754 constraint.visit_pre([this](const exprt &src) { node(src); });
755
756 auto constraint_replaced = replace(constraint);
757#if 0
758 if(verbose)
759 {
760 std::cout << "CONSTRAINT1: " << format(constraint) << "\n";
761 std::cout << "CONSTRAINT2: " << format(constraint_replaced) << "\n";
762 }
763#endif
764 dest << constraint_replaced;
765 }
766
767 object_size();
768 live_object();
771
772 // functional consistency is done last
773 evaluate_fc();
775 ok_fc();
780}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Axioms.
unsignedbv_typet size_type()
Definition c_types.cpp:55
signedbv_typet signed_size_type()
Definition c_types.cpp:71
bitvector_typet char_type()
Definition c_types.cpp:111
Boolean AND.
Definition std_expr.h:2071
void is_dynamic_object_fc()
Definition axioms.cpp:220
std::set< address_of_exprt > address_of_exprs
Definition axioms.h:61
std::set< state_ok_exprt > ok_exprs
Definition axioms.h:65
std::unordered_map< exprt, symbol_exprt, irep_hash > replacement_map
Definition axioms.h:56
std::set< object_address_exprt > object_address_exprs
Definition axioms.h:63
std::set< state_live_object_exprt > live_object_exprs
Definition axioms.h:79
std::set< evaluate_exprt > evaluate_exprs
Definition axioms.h:69
void object_size()
Definition axioms.cpp:242
bool verbose
Definition axioms.h:49
void object_size_fc()
Definition axioms.cpp:279
std::set< state_is_dynamic_object_exprt > is_dynamic_object_exprs
Definition axioms.h:76
std::set< state_is_sentinel_dll_exprt > is_sentinel_dll_exprs
Definition axioms.h:91
std::set< initial_state_exprt > initial_state_exprs
Definition axioms.h:94
std::set< state_writeable_object_exprt > writeable_object_exprs
Definition axioms.h:83
void live_object_fc()
Definition axioms.cpp:127
void emit()
Definition axioms.cpp:750
const namespacet & ns
Definition axioms.h:50
void live_object()
Definition axioms.cpp:109
void ok_fc()
Definition axioms.cpp:299
std::map< irep_idt, std::size_t > counters
Definition axioms.h:57
exprt translate(exprt) const
Definition axioms.cpp:351
void set_to_true(exprt)
Definition axioms.cpp:30
void is_cstring_fc()
Definition axioms.cpp:86
void evaluate_fc()
Definition axioms.cpp:59
void set_to_false(exprt)
Definition axioms.cpp:35
void initial_state()
Definition axioms.cpp:325
std::set< state_is_cstring_exprt > is_cstring_exprs
Definition axioms.h:72
void writeable_object()
Definition axioms.cpp:147
const std::unordered_set< symbol_exprt, irep_hash > & address_taken
Definition axioms.h:48
decision_proceduret & dest
Definition axioms.h:47
std::set< state_object_size_exprt > object_size_exprs
Definition axioms.h:87
std::vector< exprt > constraints
Definition axioms.h:52
exprt replace(exprt)
Definition axioms.cpp:360
void add(const state_ok_exprt &)
Definition axioms.cpp:629
void writeable_object_fc()
Definition axioms.cpp:198
void node(const exprt &)
Definition axioms.cpp:400
exprt & op1()
Definition expr.h:128
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
std::size_t get_width() const
Definition std_types.h:876
The Boolean type.
Definition std_types.h:36
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
Boolean implication.
Definition std_expr.h:2134
const std::string & id_string() const
Definition irep.h:399
const irep_idt & id() const
Definition irep.h:396
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Boolean negation.
Definition std_expr.h:2278
Operator to return the address of an object.
Boolean OR.
Definition std_expr.h:2179
The plus expression Associativity is not specified.
Definition std_expr.h:947
The offset (in bytes) of a pointer relative to the object.
const typet & base_type() const
The type of the data what we point to.
const exprt & address() const
Definition state.h:595
const exprt & state() const
Definition state.h:585
const exprt & size() const
Definition state.h:857
const exprt & address() const
Definition state.h:847
const exprt & state() const
Definition state.h:837
Expression to hold a symbol (variable)
Definition std_expr.h:113
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
bool is_lvalue
Definition symbol.h:72
An expression with three operands.
Definition std_expr.h:49
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
Decision Procedure Interface.
static format_containert< T > format(const T &o)
Definition format.h:37
static exprt implication(exprt lhs, exprt rhs)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static int8_t r
Definition irep_hash.h:60
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
Various predicates over pointers in programs.
exprt simplify_state_expr_node(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
exprt simplify_state_expr(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
optionalt< exprt > sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &ns)
optionalt< exprt > sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &ns)
const state_is_sentinel_dll_exprt & to_state_is_sentinel_dll_expr(const exprt &expr)
Cast an exprt to a state_is_sentinel_dll_exprt.
Simplify State Expression.
const state_ok_exprt & to_state_ok_expr(const exprt &expr)
Cast an exprt to a state_ok_exprt.
Definition state.h:882
const state_is_cstring_exprt & to_state_is_cstring_expr(const exprt &expr)
Cast an exprt to a state_is_cstring_exprt.
Definition state.h:615
const reallocate_exprt & to_reallocate_expr(const exprt &expr)
Cast an exprt to a reallocate_exprt.
Definition state.h:353
const state_writeable_object_exprt & to_state_writeable_object_expr(const exprt &expr)
Cast an exprt to a state_writeable_object_exprt.
Definition state.h:553
const state_is_dynamic_object_exprt & to_state_is_dynamic_object_expr(const exprt &expr)
Cast an exprt to a state_is_dynamic_object_exprt.
Definition state.h:739
const state_object_size_exprt & to_state_object_size_expr(const exprt &expr)
Cast an exprt to a state_object_size_exprt.
Definition state.h:804
const deallocate_state_exprt & to_deallocate_state_expr(const exprt &expr)
Cast an exprt to a deallocate_state_exprt.
Definition state.h:446
const initial_state_exprt & to_initial_state_expr(const exprt &expr)
Cast an exprt to a initial_state_exprt.
Definition state.h:59
const allocate_exprt & to_allocate_expr(const exprt &expr)
Cast an exprt to a allocate_exprt.
Definition state.h:260
const evaluate_exprt & to_evaluate_expr(const exprt &expr)
Cast an exprt to a evaluate_exprt.
Definition state.h:130
const state_live_object_exprt & to_state_live_object_expr(const exprt &expr)
Cast an exprt to a state_live_object_exprt.
Definition state.h:499
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:63
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
const string_constantt & to_string_constant(const exprt &expr)
Symbol table entry.