cprover
Loading...
Searching...
No Matches
scratch_program.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: Matt Lewis
6
7\*******************************************************************/
8
11
12#include "scratch_program.h"
13
15
16#include <goto-symex/slice.h>
17
19
20#ifdef DEBUG
21#include <iostream>
22#endif
23
24bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
25{
26 fix_types();
27
29
30 remove_skip(*this);
31
32#ifdef DEBUG
33 std::cout << "Checking following program for satness:\n";
34 output(ns, "scratch", std::cout);
35#endif
36
37 goto_functiont this_goto_function;
38 this_goto_function.body.copy_from(*this);
39 auto get_goto_function =
40 [this, &this_goto_function](
41 const irep_idt &key) -> const goto_functionst::goto_functiont & {
43 return this_goto_function;
44 else
45 return functions.function_map.at(key);
46 };
47
49
51
52 if(do_slice)
53 {
55 }
56
58 {
59 // Symex sliced away all our assertions.
60#ifdef DEBUG
61 std::cout << "Trivially unsat\n";
62#endif
63 return false;
64 }
65
67
68#ifdef DEBUG
69 std::cout << "Finished symex, invoking decision procedure.\n";
70#endif
71
72 switch((*checker)())
73 {
75 throw "error running the SMT solver";
76
78 return true;
79
81 return false;
82
84 }
85
87}
88
90{
91 return checker->get(symex_state->rename<L2>(e, ns).get());
92}
93
95{
96 instructions.insert(
97 instructions.end(),
98 new_instructions.begin(),
99 new_instructions.end());
100}
101
103 const exprt &lhs,
104 const exprt &rhs)
105{
106 return add(goto_programt::make_assignment(lhs, rhs));
107}
108
110{
111 return add(goto_programt::make_assumption(guard));
112}
113
114static void fix_types(exprt &expr)
115{
116 Forall_operands(it, expr)
117 {
118 fix_types(*it);
119 }
120
121 if(expr.id()==ID_equal ||
122 expr.id()==ID_notequal ||
123 expr.id()==ID_gt ||
124 expr.id()==ID_lt ||
125 expr.id()==ID_ge ||
126 expr.id()==ID_le)
127 {
128 auto &rel_expr = to_binary_relation_expr(expr);
129 exprt &lhs = rel_expr.lhs();
130 exprt &rhs = rel_expr.rhs();
131
132 if(lhs.type()!=rhs.type())
133 {
134 typecast_exprt typecast(rhs, lhs.type());
135 rel_expr.rhs().swap(typecast);
136 }
137 }
138}
139
141{
142 for(goto_programt::instructionst::iterator it=instructions.begin();
143 it!=instructions.end();
144 ++it)
145 {
146 if(it->is_assign())
147 {
148 code_assignt &code = to_code_assign(it->code_nonconst());
149
150 if(code.lhs().type()!=code.rhs().type())
151 {
152 typecast_exprt typecast(code.rhs(), code.lhs().type());
153 code.rhs()=typecast;
154 }
155 }
156 else if(it->is_assume() || it->is_assert())
157 {
158 exprt cond = it->get_condition();
159 ::fix_types(cond);
160 it->set_condition(cond);
161 }
162 }
163}
164
166{
167 for(patht::iterator it=path.begin();
168 it!=path.end();
169 ++it)
170 {
171 if(it->loc->is_assign() || it->loc->is_assume())
172 {
173 instructions.push_back(*it->loc);
174 }
175 else if(it->loc->is_goto())
176 {
177 if(it->guard.id()!=ID_nil)
178 {
180 }
181 }
182 else if(it->loc->is_assert())
183 {
184 add(goto_programt::make_assumption(it->loc->get_condition()));
185 }
186 }
187}
188
190{
191 goto_programt scratch;
192
193 scratch.copy_from(program);
194 destructive_append(scratch);
195}
196
198 goto_programt &program,
199 goto_programt::targett loop_header)
200{
201 append(program);
202
203 // Update any back jumps to the loop header.
204 (void)loop_header; // unused parameter
206
208
209 update();
210
212 t!=instructions.end();
213 ++t)
214 {
215 if(t->is_backwards_goto())
216 {
217 t->targets.clear();
218 t->targets.push_back(end);
219 }
220 }
221}
222
224{
225 optionst ret;
226 ret.set_option("simplify", true);
227 return ret;
228}
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:199
A codet representing an assignment in the program.
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:934
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void update()
Update all indices.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:986
instructionst::iterator targett
Definition: goto_program.h:592
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::list< instructiont > instructionst
Definition: goto_program.h:590
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:880
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
virtual void symex_with_state(statet &state, const get_goto_functiont &get_goto_functions, symbol_tablet &new_symbol_table)
Symbolically execute the entire program starting from entry point.
Definition: symex_main.cpp:325
const irep_idt & id() const
Definition: irep.h:396
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
goto_functionst functions
bool check_sat(bool do_slice, guard_managert &guard_manager)
scratch_program_symext symex
targett assume(const exprt &guard)
void append_loop(goto_programt &program, goto_programt::targett loop_header)
targett assign(const exprt &lhs, const exprt &rhs)
symbol_tablet symex_symbol_table
static optionst get_default_options()
void append(goto_programt::instructionst &instructions)
decision_proceduret * checker
std::unique_ptr< goto_symex_statet > symex_state
exprt eval(const exprt &e)
void append_path(patht &path)
symex_target_equationt equation
std::size_t count_assertions() const
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
Semantic type conversion.
Definition: std_expr.h:1920
Decision Procedure Interface.
#define Forall_operands(it, expr)
Definition: expr.h:25
const code_assignt & to_code_assign(const codet &code)
std::list< path_nodet > patht
Definition: path.h:44
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
@ L2
Definition: renamed.h:26
static void fix_types(exprt &expr)
Loop Acceleration.
Slicer for symex traces.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
std::unique_ptr< statet > initialize_entry_point_state(const get_goto_functiont &get_goto_function)