cprover
Loading...
Searching...
No Matches
symex_target_equation.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
12
14
15#include <chrono>
16
17#include <util/std_expr.h>
18
19#include "solver_hardness.h"
20#include "ssa_step.h"
21
22static std::function<void(solver_hardnesst &)>
23hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
24{
25 return [step_index, &step](solver_hardnesst &hardness) {
26 hardness.register_ssa(step_index, step.cond_expr, step.source.pc);
27 };
28}
29
31 const exprt &guard,
32 const ssa_exprt &ssa_object,
33 unsigned atomic_section_id,
34 const sourcet &source)
35{
37 SSA_stept &SSA_step=SSA_steps.back();
38
39 SSA_step.guard=guard;
40 SSA_step.ssa_lhs=ssa_object;
41 SSA_step.atomic_section_id=atomic_section_id;
42
43 merge_ireps(SSA_step);
44}
45
47 const exprt &guard,
48 const ssa_exprt &ssa_object,
49 unsigned atomic_section_id,
50 const sourcet &source)
51{
53 SSA_stept &SSA_step=SSA_steps.back();
54
55 SSA_step.guard=guard;
56 SSA_step.ssa_lhs=ssa_object;
57 SSA_step.atomic_section_id=atomic_section_id;
58
59 merge_ireps(SSA_step);
60}
61
64 const exprt &guard,
65 const sourcet &source)
66{
67 SSA_steps.emplace_back(source, goto_trace_stept::typet::SPAWN);
68 SSA_stept &SSA_step=SSA_steps.back();
69 SSA_step.guard=guard;
70
71 merge_ireps(SSA_step);
72}
73
75 const exprt &guard,
76 const sourcet &source)
77{
79 SSA_stept &SSA_step=SSA_steps.back();
80 SSA_step.guard=guard;
81
82 merge_ireps(SSA_step);
83}
84
87 const exprt &guard,
88 unsigned atomic_section_id,
89 const sourcet &source)
90{
92 SSA_stept &SSA_step=SSA_steps.back();
93 SSA_step.guard=guard;
94 SSA_step.atomic_section_id=atomic_section_id;
95
96 merge_ireps(SSA_step);
97}
98
101 const exprt &guard,
102 unsigned atomic_section_id,
103 const sourcet &source)
104{
106 SSA_stept &SSA_step=SSA_steps.back();
107 SSA_step.guard=guard;
108 SSA_step.atomic_section_id=atomic_section_id;
109
110 merge_ireps(SSA_step);
111}
112
114 const exprt &guard,
115 const ssa_exprt &ssa_lhs,
116 const exprt &ssa_full_lhs,
117 const exprt &original_full_lhs,
118 const exprt &ssa_rhs,
119 const sourcet &source,
120 assignment_typet assignment_type)
121{
122 PRECONDITION(ssa_lhs.is_not_nil());
123
124 SSA_steps.emplace_back(SSA_assignment_stept{source,
125 guard,
126 ssa_lhs,
127 ssa_full_lhs,
128 original_full_lhs,
129 ssa_rhs,
130 assignment_type});
131
132 merge_ireps(SSA_steps.back());
133}
134
136 const exprt &guard,
137 const ssa_exprt &ssa_lhs,
138 const exprt &initializer,
139 const sourcet &source,
140 assignment_typet assignment_type)
141{
142 PRECONDITION(ssa_lhs.is_not_nil());
143
144 SSA_steps.emplace_back(source, goto_trace_stept::typet::DECL);
145 SSA_stept &SSA_step=SSA_steps.back();
146
147 SSA_step.guard=guard;
148 SSA_step.ssa_lhs=ssa_lhs;
149 SSA_step.ssa_full_lhs = initializer;
150 SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
151 SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
152
153 // the condition is trivially true, and only
154 // there so we see the symbols
155 SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs);
156
157 merge_ireps(SSA_step);
158}
159
162 const exprt &,
163 const ssa_exprt &,
164 const sourcet &)
165{
166 // we currently don't record these
167}
168
170 const exprt &guard,
171 const sourcet &source)
172{
173 SSA_steps.emplace_back(source, goto_trace_stept::typet::LOCATION);
174 SSA_stept &SSA_step=SSA_steps.back();
175
176 SSA_step.guard=guard;
177
178 merge_ireps(SSA_step);
179}
180
182 const exprt &guard,
183 const irep_idt &function_id,
184 const std::vector<renamedt<exprt, L2>> &function_arguments,
185 const sourcet &source,
186 const bool hidden)
187{
189 SSA_stept &SSA_step=SSA_steps.back();
190
191 SSA_step.guard = guard;
192 SSA_step.called_function = function_id;
193 for(const auto &arg : function_arguments)
194 SSA_step.ssa_function_arguments.emplace_back(arg.get());
195 SSA_step.hidden = hidden;
196
197 merge_ireps(SSA_step);
198}
199
201 const exprt &guard,
202 const irep_idt &function_id,
203 const sourcet &source,
204 const bool hidden)
205{
207 SSA_stept &SSA_step=SSA_steps.back();
208
209 SSA_step.guard = guard;
210 SSA_step.called_function = function_id;
211 SSA_step.hidden = hidden;
212
213 merge_ireps(SSA_step);
214}
215
217 const exprt &guard,
218 const sourcet &source,
219 const irep_idt &output_id,
220 const std::list<renamedt<exprt, L2>> &args)
221{
222 SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
223 SSA_stept &SSA_step=SSA_steps.back();
224
225 SSA_step.guard=guard;
226 for(const auto &arg : args)
227 SSA_step.io_args.emplace_back(arg.get());
228 SSA_step.io_id=output_id;
229
230 merge_ireps(SSA_step);
231}
232
234 const exprt &guard,
235 const sourcet &source,
236 const irep_idt &output_id,
237 const irep_idt &fmt,
238 const std::list<exprt> &args)
239{
240 SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
241 SSA_stept &SSA_step=SSA_steps.back();
242
243 SSA_step.guard=guard;
244 SSA_step.io_args=args;
245 SSA_step.io_id=output_id;
246 SSA_step.formatted=true;
247 SSA_step.format_string=fmt;
248
249 merge_ireps(SSA_step);
250}
251
253 const exprt &guard,
254 const sourcet &source,
255 const irep_idt &input_id,
256 const std::list<exprt> &args)
257{
258 SSA_steps.emplace_back(source, goto_trace_stept::typet::INPUT);
259 SSA_stept &SSA_step=SSA_steps.back();
260
261 SSA_step.guard=guard;
262 SSA_step.io_args=args;
263 SSA_step.io_id=input_id;
264
265 merge_ireps(SSA_step);
266}
267
269 const exprt &guard,
270 const exprt &cond,
271 const sourcet &source)
272{
273 SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSUME);
274 SSA_stept &SSA_step=SSA_steps.back();
275
276 SSA_step.guard=guard;
277 SSA_step.cond_expr=cond;
278
279 merge_ireps(SSA_step);
280}
281
283 const exprt &guard,
284 const exprt &cond,
285 const std::string &msg,
286 const sourcet &source)
287{
288 SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSERT);
289 SSA_stept &SSA_step=SSA_steps.back();
290
291 SSA_step.guard=guard;
292 SSA_step.cond_expr=cond;
293 SSA_step.comment=msg;
294
295 merge_ireps(SSA_step);
296}
297
299 const exprt &guard,
300 const renamedt<exprt, L2> &cond,
301 const sourcet &source)
302{
303 SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
304 SSA_stept &SSA_step=SSA_steps.back();
305
306 SSA_step.guard=guard;
307 SSA_step.cond_expr = cond.get();
308
309 merge_ireps(SSA_step);
310}
311
313 const exprt &cond,
314 const std::string &msg,
315 const sourcet &source)
316{
317 // like assumption, but with global effect
319 SSA_stept &SSA_step=SSA_steps.back();
320
321 SSA_step.guard=true_exprt();
322 SSA_step.cond_expr=cond;
323 SSA_step.comment=msg;
324
325 merge_ireps(SSA_step);
326}
327
329 decision_proceduret &decision_procedure)
330{
331 with_solver_hardness(decision_procedure, [&](solver_hardnesst &hardness) {
332 hardness.register_ssa_size(SSA_steps.size());
333 });
334
335 convert_guards(decision_procedure);
336 convert_assignments(decision_procedure);
337 convert_decls(decision_procedure);
338 convert_assumptions(decision_procedure);
339 convert_goto_instructions(decision_procedure);
340 convert_function_calls(decision_procedure);
341 convert_io(decision_procedure);
342 convert_constraints(decision_procedure);
343}
344
346{
347 const auto convert_SSA_start = std::chrono::steady_clock::now();
348
349 convert_without_assertions(decision_procedure);
350 convert_assertions(decision_procedure);
351
352 const auto convert_SSA_stop = std::chrono::steady_clock::now();
353 std::chrono::duration<double> convert_SSA_runtime =
354 std::chrono::duration<double>(convert_SSA_stop - convert_SSA_start);
355 log.status() << "Runtime Convert SSA: " << convert_SSA_runtime.count() << "s"
356 << messaget::eom;
357}
358
360 decision_proceduret &decision_procedure)
361{
362 std::size_t step_index = 0;
363 for(auto &step : SSA_steps)
364 {
365 if(step.is_assignment() && !step.ignore && !step.converted)
366 {
367 log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
368 step.output(mstream);
369 mstream << messaget::eom;
370 });
371
372 decision_procedure.set_to_true(step.cond_expr);
373 step.converted = true;
375 decision_procedure, hardness_register_ssa(step_index, step));
376 }
377 ++step_index;
378 }
379}
380
382 decision_proceduret &decision_procedure)
383{
384 std::size_t step_index = 0;
385 for(auto &step : SSA_steps)
386 {
387 if(step.is_decl() && !step.ignore && !step.converted)
388 {
389 // The result is not used, these have no impact on
390 // the satisfiability of the formula.
391 decision_procedure.handle(step.cond_expr);
392 step.converted = true;
394 decision_procedure, hardness_register_ssa(step_index, step));
395 }
396 ++step_index;
397 }
398}
399
401 decision_proceduret &decision_procedure)
402{
403 std::size_t step_index = 0;
404 for(auto &step : SSA_steps)
405 {
406 if(step.ignore)
407 step.guard_handle = false_exprt();
408 else
409 {
410 log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
411 step.output(mstream);
412 mstream << messaget::eom;
413 });
414
415 step.guard_handle = decision_procedure.handle(step.guard);
417 decision_procedure, hardness_register_ssa(step_index, step));
418 }
419 ++step_index;
420 }
421}
422
424 decision_proceduret &decision_procedure)
425{
426 std::size_t step_index = 0;
427 for(auto &step : SSA_steps)
428 {
429 if(step.is_assume())
430 {
431 if(step.ignore)
432 step.cond_handle = true_exprt();
433 else
434 {
436 log.debug(), [&step](messaget::mstreamt &mstream) {
437 step.output(mstream);
438 mstream << messaget::eom;
439 });
440
441 step.cond_handle = decision_procedure.handle(step.cond_expr);
442
444 decision_procedure, hardness_register_ssa(step_index, step));
445 }
446 }
447 ++step_index;
448 }
449}
450
452 decision_proceduret &decision_procedure)
453{
454 std::size_t step_index = 0;
455 for(auto &step : SSA_steps)
456 {
457 if(step.is_goto())
458 {
459 if(step.ignore)
460 step.cond_handle = true_exprt();
461 else
462 {
464 log.debug(), [&step](messaget::mstreamt &mstream) {
465 step.output(mstream);
466 mstream << messaget::eom;
467 });
468
469 step.cond_handle = decision_procedure.handle(step.cond_expr);
471 decision_procedure, hardness_register_ssa(step_index, step));
472 }
473 }
474 ++step_index;
475 }
476}
477
479 decision_proceduret &decision_procedure)
480{
481 std::size_t step_index = 0;
482 for(auto &step : SSA_steps)
483 {
484 if(step.is_constraint() && !step.ignore && !step.converted)
485 {
486 log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
487 step.output(mstream);
488 mstream << messaget::eom;
489 });
490
491 decision_procedure.set_to_true(step.cond_expr);
492 step.converted = true;
493
495 decision_procedure, hardness_register_ssa(step_index, step));
496 }
497 ++step_index;
498 }
499}
500
502 decision_proceduret &decision_procedure,
503 bool optimized_for_single_assertions)
504{
505 // we find out if there is only _one_ assertion,
506 // which allows for a simpler formula
507
508 std::size_t number_of_assertions=count_assertions();
509
510 if(number_of_assertions==0)
511 return;
512
513 if(number_of_assertions == 1 && optimized_for_single_assertions)
514 {
515 std::size_t step_index = 0;
516 for(auto &step : SSA_steps)
517 {
518 // hide already converted assertions in the error trace
519 if(step.is_assert() && step.converted)
520 step.hidden = true;
521
522 if(step.is_assert() && !step.ignore && !step.converted)
523 {
524 step.converted = true;
525 decision_procedure.set_to_false(step.cond_expr);
526 step.cond_handle = false_exprt();
527
529 decision_procedure, hardness_register_ssa(step_index, step));
530 return; // prevent further assumptions!
531 }
532 else if(step.is_assume())
533 {
534 decision_procedure.set_to_true(step.cond_expr);
535
537 decision_procedure, hardness_register_ssa(step_index, step));
538 }
539 ++step_index;
540 }
541
542 UNREACHABLE; // unreachable
543 }
544
545 // We do (NOT a1) OR (NOT a2) ...
546 // where the a's are the assertions
547 or_exprt::operandst disjuncts;
548 disjuncts.reserve(number_of_assertions);
549
551
552 std::vector<goto_programt::const_targett> involved_steps;
553
554 for(auto &step : SSA_steps)
555 {
556 // hide already converted assertions in the error trace
557 if(step.is_assert() && step.converted)
558 step.hidden = true;
559
560 if(step.is_assert() && !step.ignore && !step.converted)
561 {
562 step.converted = true;
563
564 log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
565 step.output(mstream);
566 mstream << messaget::eom;
567 });
568
571 step.cond_expr);
572
573 // do the conversion
574 step.cond_handle = decision_procedure.handle(implication);
575
577 decision_procedure,
578 [&involved_steps, &step](solver_hardnesst &hardness) {
579 involved_steps.push_back(step.source.pc);
580 });
581
582 // store disjunct
583 disjuncts.push_back(not_exprt(step.cond_handle));
584 }
585 else if(step.is_assume())
586 {
587 // the assumptions have been converted before
588 // avoid deep nesting of ID_and expressions
589 if(assumption.id()==ID_and)
590 assumption.copy_to_operands(step.cond_handle);
591 else
592 assumption = and_exprt(assumption, step.cond_handle);
593
595 decision_procedure,
596 [&involved_steps, &step](solver_hardnesst &hardness) {
597 involved_steps.push_back(step.source.pc);
598 });
599 }
600 }
601
602 const auto assertion_disjunction = disjunction(disjuncts);
603 // the below is 'true' if there are no assertions
604 decision_procedure.set_to_true(assertion_disjunction);
605
607 decision_procedure,
608 [&assertion_disjunction, &involved_steps](solver_hardnesst &hardness) {
609 hardness.register_assertion_ssas(assertion_disjunction, involved_steps);
610 });
611}
612
614 decision_proceduret &decision_procedure)
615{
616 std::size_t step_index = 0;
617 for(auto &step : SSA_steps)
618 {
619 if(!step.ignore)
620 {
621 and_exprt::operandst conjuncts;
622 step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
623
624 for(const auto &arg : step.ssa_function_arguments)
625 {
626 if(arg.is_constant() ||
627 arg.id()==ID_string_constant)
628 step.converted_function_arguments.push_back(arg);
629 else
630 {
631 const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
632 symbol_exprt symbol(identifier, arg.type());
633
634 equal_exprt eq(arg, symbol);
635 merge_irep(eq);
636
637 decision_procedure.set_to(eq, true);
638 conjuncts.push_back(eq);
639 step.converted_function_arguments.push_back(symbol);
640 }
641 }
643 decision_procedure,
644 [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
645 hardness.register_ssa(
646 step_index, conjunction(conjuncts), step.source.pc);
647 });
648 }
649 ++step_index;
650 }
651}
652
654{
655 std::size_t step_index = 0;
656 for(auto &step : SSA_steps)
657 {
658 if(!step.ignore)
659 {
660 and_exprt::operandst conjuncts;
661 for(const auto &arg : step.io_args)
662 {
663 if(arg.is_constant() ||
664 arg.id()==ID_string_constant)
665 step.converted_io_args.push_back(arg);
666 else
667 {
668 const irep_idt identifier =
669 "symex::io::" + std::to_string(io_count++);
670 symbol_exprt symbol(identifier, arg.type());
671
672 equal_exprt eq(arg, symbol);
673 merge_irep(eq);
674
675 decision_procedure.set_to(eq, true);
676 conjuncts.push_back(eq);
677 step.converted_io_args.push_back(symbol);
678 }
679 }
681 decision_procedure,
682 [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
683 hardness.register_ssa(
684 step_index, conjunction(conjuncts), step.source.pc);
685 });
686 }
687 ++step_index;
688 }
689}
690
695{
696 merge_irep(SSA_step.guard);
697
698 merge_irep(SSA_step.ssa_lhs);
699 merge_irep(SSA_step.ssa_full_lhs);
701 merge_irep(SSA_step.ssa_rhs);
702
703 merge_irep(SSA_step.cond_expr);
704
705 for(auto &step : SSA_step.io_args)
706 merge_irep(step);
707
708 for(auto &arg : SSA_step.ssa_function_arguments)
709 merge_irep(arg);
710
711 // converted_io_args is merged in convert_io
712}
713
714void symex_target_equationt::output(std::ostream &out) const
715{
716 for(const auto &step : SSA_steps)
717 {
718 step.output(out);
719 out << "--------------\n";
720 }
721}
Single SSA step in the equation.
Definition: ssa_step.h:47
irep_idt io_id
Definition: ssa_step.h:159
irep_idt called_function
Definition: ssa_step.h:165
std::vector< exprt > ssa_function_arguments
Definition: ssa_step.h:168
exprt cond_expr
Definition: ssa_step.h:149
unsigned atomic_section_id
Definition: ssa_step.h:171
irep_idt format_string
Definition: ssa_step.h:159
bool formatted
Definition: ssa_step.h:160
exprt ssa_full_lhs
Definition: ssa_step.h:144
bool hidden
Definition: ssa_step.h:137
exprt guard
Definition: ssa_step.h:139
exprt ssa_rhs
Definition: ssa_step.h:145
std::string comment
Definition: ssa_step.h:151
symex_targett::sourcet source
Definition: ssa_step.h:49
exprt original_full_lhs
Definition: ssa_step.h:144
std::list< exprt > io_args
Definition: ssa_step.h:161
ssa_exprt ssa_lhs
Definition: ssa_step.h:143
Boolean AND.
Definition: std_expr.h:1974
virtual exprt handle(const exprt &expr)=0
Generate a handle, which is an expression that has the same value as the argument in any model that i...
void set_to_false(const exprt &expr)
For a Boolean expression expr, add the constraint 'not expr'.
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
virtual void set_to(const exprt &expr, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
The Boolean constant false.
Definition: std_expr.h:2865
Boolean implication.
Definition: std_expr.h:2037
bool is_not_nil() const
Definition: irep.h:380
mstreamt & debug() const
Definition: message.h:429
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition: message.cpp:139
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
Boolean negation.
Definition: std_expr.h:2181
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
const underlyingt & get() const
Definition: renamed.h:40
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
Expression to hold a symbol (variable)
Definition: std_expr.h:80
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
std::size_t count_assertions() const
void convert_decls(decision_proceduret &decision_procedure)
Converts declarations: these are effectively ignored by the decision procedure.
void convert_assumptions(decision_proceduret &decision_procedure)
Converts assumptions: convert the expression the assumption represents.
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
void convert_assignments(decision_proceduret &decision_procedure)
Converts assignments: set the equality lhs==rhs to True.
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
void merge_ireps(SSA_stept &SSA_step)
Merging causes identical ireps to be shared.
void convert_guards(decision_proceduret &decision_procedure)
Converts guards: convert the expression the guard represents.
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself.
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
Write to a local variable.
void convert_function_calls(decision_proceduret &decision_procedure)
Converts function calls: for each argument build an equality between its symbol and the argument itse...
void convert_constraints(decision_proceduret &decision_procedure)
Converts constraints: set the represented condition to True.
virtual void function_call(const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 > > &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 > > &args)
Record an output.
void convert_goto_instructions(decision_proceduret &decision_procedure)
Converts goto instructions: convert the expression representing the condition of this goto.
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &initializer, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
The Boolean constant true.
Definition: std_expr.h:2856
static exprt implication(exprt lhs, exprt rhs)
static void with_solver_hardness(decision_proceduret &maybe_hardness_collector, std::function< void(solver_hardnesst &hardness)> handler)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:34
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
API to expression classes.
A structure that facilitates collecting the complexity statistics from a decision procedure.
void register_ssa(std::size_t ssa_index, const exprt ssa_expression, goto_programt::const_targett pc)
Called from the symtex_target_equationt::convert_*, this function associates an SSA step to all the s...
void register_assertion_ssas(const exprt ssa_expression, const std::vector< goto_programt::const_targett > &pcs)
Called from the symtex_target_equationt::convert_assertions, this function associates the disjunction...
void register_ssa_size(std::size_t size)
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
goto_programt::const_targett pc
Definition: symex_target.h:42
static std::function< void(solver_hardnesst &)> hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
Generate Equation using Symbolic Execution.