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 
40 
42 
43  if(do_slice)
44  {
45  slice(equation);
46  }
47 
48  if(equation.count_assertions()==0)
49  {
50  // Symex sliced away all our assertions.
51 #ifdef DEBUG
52  std::cout << "Trivially unsat\n";
53 #endif
54  return false;
55  }
56 
58 
59 #ifdef DEBUG
60  std::cout << "Finished symex, invoking decision procedure.\n";
61 #endif
62 
64 }
65 
67 {
68  exprt ssa=e;
69 
70  symex_state.rename(ssa, ns);
71 
72  return checker->get(ssa);
73 }
74 
76 {
77  instructions.insert(
78  instructions.end(),
79  new_instructions.begin(),
80  new_instructions.end());
81 }
82 
84  const exprt &lhs,
85  const exprt &rhs)
86 {
87  code_assignt assignment(lhs, rhs);
88  targett instruction=add_instruction(ASSIGN);
89  instruction->code=assignment;
90 
91  return instruction;
92 }
93 
95 {
96  targett instruction=add_instruction(ASSUME);
97  instruction->guard=guard;
98 
99  return instruction;
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  exprt &lhs=expr.op0();
117  exprt &rhs=expr.op1();
118 
119  if(lhs.type()!=rhs.type())
120  {
121  typecast_exprt typecast(rhs, lhs.type());
122  expr.op1().swap(typecast);
123  }
124  }
125 }
126 
128 {
129  for(goto_programt::instructionst::iterator it=instructions.begin();
130  it!=instructions.end();
131  ++it)
132  {
133  if(it->is_assign())
134  {
135  code_assignt &code=to_code_assign(it->code);
136 
137  if(code.lhs().type()!=code.rhs().type())
138  {
139  typecast_exprt typecast(code.rhs(), code.lhs().type());
140  code.rhs()=typecast;
141  }
142  }
143  else if(it->is_assume() || it->is_assert())
144  {
145  ::fix_types(it->guard);
146  }
147  }
148 }
149 
151 {
152  for(patht::iterator it=path.begin();
153  it!=path.end();
154  ++it)
155  {
156  if(it->loc->is_assign() || it->loc->is_assume())
157  {
158  instructions.push_back(*it->loc);
159  }
160  else if(it->loc->is_goto())
161  {
162  if(it->guard.id()!=ID_nil)
163  {
164  add_instruction(ASSUME)->guard=it->guard;
165  }
166  }
167  else if(it->loc->is_assert())
168  {
169  add_instruction(ASSUME)->guard=it->loc->guard;
170  }
171  }
172 }
173 
175 {
176  goto_programt scratch;
177 
178  scratch.copy_from(program);
179  destructive_append(scratch);
180 }
181 
183  goto_programt &program,
184  goto_programt::targett loop_header)
185 {
186  append(program);
187 
188  // Update any back jumps to the loop header.
189  assume(false_exprt());
190 
192 
193  update();
194 
195  for(goto_programt::targett t=instructions.begin();
196  t!=instructions.end();
197  ++t)
198  {
199  if(t->is_backwards_goto())
200  {
201  t->targets.clear();
202  t->targets.push_back(end);
203  }
204  }
205 }
void update()
Update all indices.
semantic type conversion
Definition: std_expr.h:2111
void slice(symex_target_equationt &equation)
Definition: slice.cpp:209
symbol_tablet symex_symbol_table
targett assign(const exprt &lhs, const exprt &rhs)
void convert(prop_convt &prop_conv)
exprt & op0()
Definition: expr.h:72
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
bool constant_propagation
Definition: goto_symex.h:215
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
Decision Procedure Interface.
typet & type()
Definition: expr.h:56
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
std::list< instructiont > instructionst
Definition: goto_program.h:395
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
std::map< irep_idt, exprt > valuest
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
goto_functionst functions
virtual resultt dec_solve()=0
instructionst::iterator targett
Definition: goto_program.h:397
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:170
exprt & rhs()
Definition: std_code.h:213
exprt eval(const exprt &e)
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
void append_loop(goto_programt &program, goto_programt::targett loop_header)
void append(goto_programt::instructionst &instructions)
exprt & op1()
Definition: expr.h:75
std::list< path_nodet > patht
Definition: path.h:45
Loop Acceleration.
The boolean constant false.
Definition: std_expr.h:4499
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
symex_target_equationt equation
void append_path(patht &path)
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
prop_convt * checker
Base class for all expressions.
Definition: expr.h:42
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:231
#define Forall_operands(it, expr)
Definition: expr.h:23
goto_symex_statet symex_state
Program Transformation.
goto_symext symex
Assignment.
Definition: std_code.h:195
static void fix_types(exprt &expr)