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 
14 #include <util/fixedbv.h>
15 
17 
18 #include <goto-symex/slice.h>
19 
21 
22 #ifdef DEBUG
23 #include <iostream>
24 #endif
25 
26 bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
27 {
28  fix_types();
29 
31 
32  remove_skip(*this);
33 
34 #ifdef DEBUG
35  std::cout << "Checking following program for satness:\n";
36  output(ns, "scratch", std::cout);
37 #endif
38 
39  goto_functiont this_goto_function;
40  this_goto_function.body.copy_from(*this);
41  auto get_goto_function =
42  [this, &this_goto_function](
43  const irep_idt &key) -> const goto_functionst::goto_functiont & {
44  if(key == goto_functionst::entry_point())
45  return this_goto_function;
46  else
47  return functions.function_map.at(key);
48  };
49 
50  symex_state = symex.initialize_entry_point_state(get_goto_function);
51 
53 
54  if(do_slice)
55  {
56  slice(equation);
57  }
58 
59  if(equation.count_assertions()==0)
60  {
61  // Symex sliced away all our assertions.
62 #ifdef DEBUG
63  std::cout << "Trivially unsat\n";
64 #endif
65  return false;
66  }
67 
69 
70 #ifdef DEBUG
71  std::cout << "Finished symex, invoking decision procedure.\n";
72 #endif
73 
74  switch((*checker)())
75  {
77  throw "error running the SMT solver";
78 
80  return true;
81 
83  return false;
84 
86  }
87 
89 }
90 
92 {
93  return checker->get(symex_state->rename<L2>(e, ns).get());
94 }
95 
97 {
98  instructions.insert(
99  instructions.end(),
100  new_instructions.begin(),
101  new_instructions.end());
102 }
103 
105  const exprt &lhs,
106  const exprt &rhs)
107 {
108  return add(goto_programt::make_assignment(lhs, rhs));
109 }
110 
112 {
113  return add(goto_programt::make_assumption(guard));
114 }
115 
116 static void fix_types(exprt &expr)
117 {
118  Forall_operands(it, expr)
119  {
120  fix_types(*it);
121  }
122 
123  if(expr.id()==ID_equal ||
124  expr.id()==ID_notequal ||
125  expr.id()==ID_gt ||
126  expr.id()==ID_lt ||
127  expr.id()==ID_ge ||
128  expr.id()==ID_le)
129  {
130  auto &rel_expr = to_binary_relation_expr(expr);
131  exprt &lhs = rel_expr.lhs();
132  exprt &rhs = rel_expr.rhs();
133 
134  if(lhs.type()!=rhs.type())
135  {
136  typecast_exprt typecast(rhs, lhs.type());
137  rel_expr.rhs().swap(typecast);
138  }
139  }
140 }
141 
143 {
144  for(goto_programt::instructionst::iterator it=instructions.begin();
145  it!=instructions.end();
146  ++it)
147  {
148  if(it->is_assign())
149  {
150  code_assignt &code = to_code_assign(it->code_nonconst());
151 
152  if(code.lhs().type()!=code.rhs().type())
153  {
154  typecast_exprt typecast(code.rhs(), code.lhs().type());
155  code.rhs()=typecast;
156  }
157  }
158  else if(it->is_assume() || it->is_assert())
159  {
160  exprt cond = it->get_condition();
161  ::fix_types(cond);
162  it->set_condition(cond);
163  }
164  }
165 }
166 
168 {
169  for(patht::iterator it=path.begin();
170  it!=path.end();
171  ++it)
172  {
173  if(it->loc->is_assign() || it->loc->is_assume())
174  {
175  instructions.push_back(*it->loc);
176  }
177  else if(it->loc->is_goto())
178  {
179  if(it->guard.id()!=ID_nil)
180  {
182  }
183  }
184  else if(it->loc->is_assert())
185  {
186  add(goto_programt::make_assumption(it->loc->get_condition()));
187  }
188  }
189 }
190 
192 {
193  goto_programt scratch;
194 
195  scratch.copy_from(program);
196  destructive_append(scratch);
197 }
198 
200  goto_programt &program,
201  goto_programt::targett loop_header)
202 {
203  append(program);
204 
205  // Update any back jumps to the loop header.
206  (void)loop_header; // unused parameter
207  assume(false_exprt());
208 
210 
211  update();
212 
213  for(goto_programt::targett t=instructions.begin();
214  t!=instructions.end();
215  ++t)
216  {
217  if(t->is_backwards_goto())
218  {
219  t->targets.clear();
220  t->targets.push_back(end);
221  }
222  }
223 }
224 
226 {
227  optionst ret;
228  ret.set_option("simplify", true);
229  return ret;
230 }
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:326
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
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:29
scratch_programt::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: scratch_program.h:110
L2
@ L2
Definition: renamed.h:20
scratch_programt::ns
namespacet ns
Definition: scratch_program.h:111
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:317
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:561
scratch_programt::checker
decision_proceduret * checker
Definition: scratch_program.h:120
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:115
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:540
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:625
fixedbv.h
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:941
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:670
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:27
scratch_programt::append
void append(goto_programt::instructionst &instructions)
Definition: scratch_program.cpp:96
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:1008
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:23
symex_target_equationt::count_assertions
std::size_t count_assertions() const
Definition: symex_target_equation.h:240
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:199
scratch_programt::functions
goto_functionst functions
Definition: scratch_program.h:108
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:548
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:835
scratch_programt::fix_types
void fix_types()
Definition: scratch_program.cpp:142
scratch_programt::eval
exprt eval(const exprt &e)
Definition: scratch_program.cpp:91
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:197
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
fix_types
static void fix_types(exprt &expr)
Definition: scratch_program.cpp:116
scratch_programt::assume
targett assume(const exprt &guard)
Definition: scratch_program.cpp:111
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:27
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
scratch_programt::equation
symex_target_equationt equation
Definition: scratch_program.h:112
scratch_programt::append_path
void append_path(patht &path)
Definition: scratch_program.cpp:167
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:653
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
scratch_programt::symex_state
std::unique_ptr< goto_symex_statet > symex_state
Definition: scratch_program.h:107
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
patht
std::list< path_nodet > patht
Definition: path.h:45
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:57
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:349
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:889
scratch_programt::get_default_options
static optionst get_default_options()
Definition: scratch_program.cpp:225
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
scratch_programt::check_sat
bool check_sat(bool do_slice, guard_managert &guard_manager)
Definition: scratch_program.cpp:26
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
slice.h
Slicer for symex traces.
scratch_programt::assign
targett assign(const exprt &lhs, const exprt &rhs)
Definition: scratch_program.cpp:104
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:723
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563