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  symex_state = util_make_unique<goto_symex_statet>(
42  guard_manager,
43  [this](const irep_idt &id) {
45  });
46 
48  *symex_state,
49  [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {
50  return functions.function_map.at(key);
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 
75 }
76 
78 {
79  return checker->get(symex_state->rename<L2>(e, ns).get());
80 }
81 
83 {
84  instructions.insert(
85  instructions.end(),
86  new_instructions.begin(),
87  new_instructions.end());
88 }
89 
91  const exprt &lhs,
92  const exprt &rhs)
93 {
94  return add(goto_programt::make_assignment(lhs, rhs));
95 }
96 
98 {
99  return add(goto_programt::make_assumption(guard));
100 }
101 
102 static void fix_types(exprt &expr)
103 {
104  Forall_operands(it, expr)
105  {
106  fix_types(*it);
107  }
108 
109  if(expr.id()==ID_equal ||
110  expr.id()==ID_notequal ||
111  expr.id()==ID_gt ||
112  expr.id()==ID_lt ||
113  expr.id()==ID_ge ||
114  expr.id()==ID_le)
115  {
116  auto &rel_expr = to_binary_relation_expr(expr);
117  exprt &lhs = rel_expr.lhs();
118  exprt &rhs = rel_expr.rhs();
119 
120  if(lhs.type()!=rhs.type())
121  {
122  typecast_exprt typecast(rhs, lhs.type());
123  rel_expr.rhs().swap(typecast);
124  }
125  }
126 }
127 
129 {
130  for(goto_programt::instructionst::iterator it=instructions.begin();
131  it!=instructions.end();
132  ++it)
133  {
134  if(it->is_assign())
135  {
136  code_assignt &code=to_code_assign(it->code);
137 
138  if(code.lhs().type()!=code.rhs().type())
139  {
140  typecast_exprt typecast(code.rhs(), code.lhs().type());
141  code.rhs()=typecast;
142  }
143  }
144  else if(it->is_assume() || it->is_assert())
145  {
146  exprt cond = it->get_condition();
147  ::fix_types(cond);
148  it->set_condition(cond);
149  }
150  }
151 }
152 
154 {
155  for(patht::iterator it=path.begin();
156  it!=path.end();
157  ++it)
158  {
159  if(it->loc->is_assign() || it->loc->is_assume())
160  {
161  instructions.push_back(*it->loc);
162  }
163  else if(it->loc->is_goto())
164  {
165  if(it->guard.id()!=ID_nil)
166  {
168  }
169  }
170  else if(it->loc->is_assert())
171  {
172  add(goto_programt::make_assumption(it->loc->get_condition()));
173  }
174  }
175 }
176 
178 {
179  goto_programt scratch;
180 
181  scratch.copy_from(program);
182  destructive_append(scratch);
183 }
184 
186  goto_programt &program,
187  goto_programt::targett loop_header)
188 {
189  append(program);
190 
191  // Update any back jumps to the loop header.
192  (void)loop_header; // unused parameter
193  assume(false_exprt());
194 
196 
197  update();
198 
199  for(goto_programt::targett t=instructions.begin();
200  t!=instructions.end();
201  ++t)
202  {
203  if(t->is_backwards_goto())
204  {
205  t->targets.clear();
206  t->targets.push_back(end);
207  }
208  }
209 }
210 
212 {
213  optionst ret;
214  ret.set_option("simplify", true);
215  return ret;
216 }
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:324
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
scratch_programt::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: scratch_program.h:83
L2
@ L2
Definition: renamed.h:20
scratch_programt::ns
namespacet ns
Definition: scratch_program.h:84
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
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:577
scratch_programt::checker
decision_proceduret * checker
Definition: scratch_program.h:93
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:85
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:541
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:626
fixedbv.h
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE
constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE
Limit the size of arrays for which field_sensitivity gets applied.
Definition: magic.h:21
exprt
Base class for all expressions.
Definition: expr.h:53
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:82
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:1024
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:81
scratch_programt::append_loop
void append_loop(goto_programt &program, goto_programt::targett loop_header)
Definition: scratch_program.cpp:185
scratch_programt::functions
goto_functionst functions
Definition: scratch_program.h:81
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:549
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
scratch_programt::fix_types
void fix_types()
Definition: scratch_program.cpp:128
scratch_programt::eval
exprt eval(const exprt &e)
Definition: scratch_program.cpp:77
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:102
scratch_programt::assume
targett assume(const exprt &guard)
Definition: scratch_program.cpp:97
irept::id
const irep_idt & id() const
Definition: irep.h:418
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
scratch_programt::equation
symex_target_equationt equation
Definition: scratch_program.h:85
scratch_programt::append_path
void append_path(patht &path)
Definition: scratch_program.cpp:153
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:669
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:585
scratch_programt::symex_state
std::unique_ptr< goto_symex_statet > symex_state
Definition: scratch_program.h:80
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_programt::symex
goto_symext symex
Definition: scratch_program.h:88
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:73
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
scratch_programt::get_default_options
static optionst get_default_options()
Definition: scratch_program.cpp:211
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:2013
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.
path_storaget::get_unique_l2_index
std::size_t get_unique_l2_index(const irep_idt &id)
Definition: path_storage.h:109
scratch_programt::assign
targett assign(const exprt &lhs, const exprt &rhs)
Definition: scratch_program.cpp:90
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:774
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
scratch_programt::path_storage
path_fifot path_storage
Definition: scratch_program.h:86