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>
16 
17 #include <goto-symex/slice.h>
18 
20 
21 #ifdef DEBUG
22 #include <iostream>
23 #endif
24 
25 bool scratch_programt::check_sat(bool do_slice)
26 {
27  fix_types();
28 
30 
31  remove_skip(*this);
32 
33 #ifdef DEBUG
34  std::cout << "Checking following program for satness:\n";
35  output(ns, "scratch", std::cout);
36 #endif
37 
39 
40  if(do_slice)
41  {
42  slice(equation);
43  }
44 
45  if(equation.count_assertions()==0)
46  {
47  // Symex sliced away all our assertions.
48 #ifdef DEBUG
49  std::cout << "Trivially unsat\n";
50 #endif
51  return false;
52  }
53 
55 
56 #ifdef DEBUG
57  std::cout << "Finished symex, invoking decision procedure.\n";
58 #endif
59 
61 }
62 
64 {
65  exprt ssa=e;
66 
67  symex_state.rename(ssa, ns);
68 
69  return checker->get(ssa);
70 }
71 
73 {
74  instructions.insert(
75  instructions.end(),
76  new_instructions.begin(),
77  new_instructions.end());
78 }
79 
81  const exprt &lhs,
82  const exprt &rhs)
83 {
84  code_assignt assignment(lhs, rhs);
85  targett instruction=add_instruction(ASSIGN);
86  instruction->code=assignment;
87 
88  return instruction;
89 }
90 
92 {
93  targett instruction=add_instruction(ASSUME);
94  instruction->guard=guard;
95 
96  return instruction;
97 }
98 
99 static void fix_types(exprt &expr)
100 {
101  Forall_operands(it, expr)
102  {
103  fix_types(*it);
104  }
105 
106  if(expr.id()==ID_equal ||
107  expr.id()==ID_notequal ||
108  expr.id()==ID_gt ||
109  expr.id()==ID_lt ||
110  expr.id()==ID_ge ||
111  expr.id()==ID_le)
112  {
113  exprt &lhs=expr.op0();
114  exprt &rhs=expr.op1();
115 
116  if(lhs.type()!=rhs.type())
117  {
118  typecast_exprt typecast(rhs, lhs.type());
119  expr.op1().swap(typecast);
120  }
121  }
122 }
123 
125 {
126  for(goto_programt::instructionst::iterator it=instructions.begin();
127  it!=instructions.end();
128  ++it)
129  {
130  if(it->is_assign())
131  {
132  code_assignt &code=to_code_assign(it->code);
133 
134  if(code.lhs().type()!=code.rhs().type())
135  {
136  typecast_exprt typecast(code.rhs(), code.lhs().type());
137  code.rhs()=typecast;
138  }
139  }
140  else if(it->is_assume() || it->is_assert())
141  {
142  ::fix_types(it->guard);
143  }
144  }
145 }
146 
148 {
149  for(patht::iterator it=path.begin();
150  it!=path.end();
151  ++it)
152  {
153  if(it->loc->is_assign() || it->loc->is_assume())
154  {
155  instructions.push_back(*it->loc);
156  }
157  else if(it->loc->is_goto())
158  {
159  if(it->guard.id()!=ID_nil)
160  {
161  add_instruction(ASSUME)->guard=it->guard;
162  }
163  }
164  else if(it->loc->is_assert())
165  {
166  add_instruction(ASSUME)->guard=it->loc->guard;
167  }
168  }
169 }
170 
172 {
173  goto_programt scratch;
174 
175  scratch.copy_from(program);
176  destructive_append(scratch);
177 }
178 
180  goto_programt &program,
181  goto_programt::targett loop_header)
182 {
183  append(program);
184 
185  // Update any back jumps to the loop header.
186  (void)loop_header; // unused parameter
187  assume(false_exprt());
188 
190 
191  update();
192 
193  for(goto_programt::targett t=instructions.begin();
194  t!=instructions.end();
195  ++t)
196  {
197  if(t->is_backwards_goto())
198  {
199  t->targets.clear();
200  t->targets.push_back(end);
201  }
202  }
203 }
204 
206 {
207  optionst ret;
208  ret.set_option("simplify", true);
209  return ret;
210 }
void update()
Update all indices.
Semantic type conversion.
Definition: std_expr.h:2277
void slice(symex_target_equationt &equation)
Definition: slice.cpp:208
symbol_tablet symex_symbol_table
targett assign(const exprt &lhs, const exprt &rhs)
void convert(prop_convt &prop_conv)
Interface method to initiate the conversion into a decision procedure format.
exprt & op0()
Definition: expr.h:84
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual exprt get(const exprt &expr) const =0
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:524
Decision Procedure Interface.
typet & type()
Return the type of the expression.
Definition: expr.h:68
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
std::list< instructiont > instructionst
Definition: goto_program.h:412
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:269
goto_functionst functions
virtual resultt dec_solve()=0
instructionst::iterator targett
Definition: goto_program.h:414
targett assume(const exprt &guard)
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
Definition: symex_main.cpp:227
exprt & rhs()
Definition: std_code.h:274
exprt eval(const exprt &e)
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
void append_loop(goto_programt &program, goto_programt::targett loop_header)
void append(goto_programt::instructionst &instructions)
exprt & op1()
Definition: expr.h:87
std::list< path_nodet > patht
Definition: path.h:45
Loop Acceleration.
The Boolean constant false.
Definition: std_expr.h:4452
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
symex_target_equationt equation
void append_path(patht &path)
static optionst get_default_options()
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
prop_convt * checker
Base class for all expressions.
Definition: expr.h:54
Slicer for symex traces.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
std::size_t count_assertions() const
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:26
goto_symex_statet symex_state
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
Program Transformation.
goto_symext symex
A codet representing an assignment in the program.
Definition: std_code.h:256
static void fix_types(exprt &expr)