cprover
scratch_program.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: 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 
24 bool 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 & {
42  if(key == goto_functionst::entry_point())
43  return this_goto_function;
44  else
45  return functions.function_map.at(key);
46  };
47 
48  symex_state = symex.initialize_entry_point_state(get_goto_function);
49 
51 
52  if(do_slice)
53  {
54  slice(equation);
55  }
56 
57  if(equation.count_assertions()==0)
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 
114 static 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
205  assume(false_exprt());
206 
208 
209  update();
210 
211  for(goto_programt::targett t=instructions.begin();
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 }
decision_proceduret::get
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
goto_symext::symex_with_state
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
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functiont::body
goto_programt body
Definition: goto_function.h:26
scratch_programt::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: scratch_program.h:108
L2
@ L2
Definition: renamed.h:26
scratch_programt::ns
namespacet ns
Definition: scratch_program.h:109
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
optionst
Definition: options.h:23
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:315
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:644
scratch_programt::checker
decision_proceduret * checker
Definition: scratch_program.h:118
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
scratch_programt::symex
scratch_program_symext symex
Definition: scratch_program.h:113
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:576
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:661
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1015
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
exprt
Base class for all expressions.
Definition: expr.h:54
scratch_program.h
Loop Acceleration.
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
scratch_programt::append
void append(goto_programt::instructionst &instructions)
Definition: scratch_program.cpp:94
decision_procedure.h
Decision Procedure Interface.
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1082
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
symex_target_equationt::count_assertions
std::size_t count_assertions() const
Definition: symex_target_equation.h:233
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
scratch_programt::append_loop
void append_loop(goto_programt &program, goto_programt::targett loop_header)
Definition: scratch_program.cpp:197
scratch_programt::functions
goto_functionst functions
Definition: scratch_program.h:106
goto_programt::output
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
Definition: goto_program.cpp:584
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:909
scratch_programt::fix_types
void fix_types()
Definition: scratch_program.cpp:140
scratch_programt::eval
exprt eval(const exprt &e)
Definition: scratch_program.cpp:89
slice
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:198
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:310
fix_types
static void fix_types(exprt &expr)
Definition: scratch_program.cpp:114
scratch_programt::assume
targett assume(const exprt &guard)
Definition: scratch_program.cpp:109
decision_proceduret::resultt::D_ERROR
@ D_ERROR
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
scratch_programt::equation
symex_target_equationt equation
Definition: scratch_program.h:110
scratch_programt::append_path
void append_path(patht &path)
Definition: scratch_program.cpp:165
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
scratch_programt::symex_state
std::unique_ptr< goto_symex_statet > symex_state
Definition: scratch_program.h:105
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381
patht
std::list< path_nodet > patht
Definition: path.h:44
scratch_program_symext::initialize_entry_point_state
std::unique_ptr< statet > initialize_entry_point_state(const get_goto_functiont &get_goto_function)
Definition: scratch_program.h:55
symex_target_equationt::convert
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
Definition: symex_target_equation.cpp:347
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
scratch_programt::get_default_options
static optionst get_default_options()
Definition: scratch_program.cpp:223
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
scratch_programt::check_sat
bool check_sat(bool do_slice, guard_managert &guard_manager)
Definition: scratch_program.cpp:24
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
slice.h
Slicer for symex traces.
scratch_programt::assign
targett assign(const exprt &lhs, const exprt &rhs)
Definition: scratch_program.cpp:102
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646