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 }
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
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt & rhs()
Definition: std_code.h:317
exprt & lhs()
Definition: std_code.h:312
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:2726
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 generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:876
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
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:928
instructionst::iterator targett
Definition: goto_program.h:550
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:640
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:995
std::list< instructiont > instructionst
Definition: goto_program.h:548
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:822
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:657
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:407
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
std::size_t get_unique_l2_index(const irep_idt &id)
Definition: path_storage.h:109
goto_functionst functions
bool check_sat(bool do_slice, guard_managert &guard_manager)
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)
path_fifot path_storage
goto_symext symex
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:1781
Decision Procedure Interface.
#define Forall_operands(it, expr)
Definition: expr.h:25
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
std::list< path_nodet > patht
Definition: path.h:45
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
Program Transformation.
@ L2
Definition: renamed.h:20
static void fix_types(exprt &expr)
Loop Acceleration.
Slicer for symex traces.
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:724
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38