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  update();
33 
34 #ifdef DEBUG
35  std::cout << "Checking following program for satness:\n";
36  output(ns, "scratch", std::cout);
37 #endif
38 
41 
42  symex(symex_state, functions, *this);
43 
44  if(do_slice)
45  {
46  slice(equation);
47  }
48 
49  if(equation.count_assertions()==0)
50  {
51  // Symex sliced away all our assertions.
52 #ifdef DEBUG
53  std::cout << "Trivially unsat\n";
54 #endif
55  return false;
56  }
57 
59 
60 #ifdef DEBUG
61  std::cout << "Finished symex, invoking decision procedure.\n";
62 #endif
63 
65 }
66 
68 {
69  exprt ssa=e;
70 
71  symex_state.rename(ssa, ns);
72 
73  return checker->get(ssa);
74 }
75 
77 {
78  instructions.insert(
79  instructions.end(),
80  new_instructions.begin(),
81  new_instructions.end());
82 }
83 
85  const exprt &lhs,
86  const exprt &rhs)
87 {
88  code_assignt assignment(lhs, rhs);
89  targett instruction=add_instruction(ASSIGN);
90  instruction->code=assignment;
91 
92  return instruction;
93 }
94 
96 {
97  targett instruction=add_instruction(ASSUME);
98  instruction->guard=guard;
99 
100  return instruction;
101 }
102 
103 static void fix_types(exprt &expr)
104 {
105  Forall_operands(it, expr)
106  {
107  fix_types(*it);
108  }
109 
110  if(expr.id()==ID_equal ||
111  expr.id()==ID_notequal ||
112  expr.id()==ID_gt ||
113  expr.id()==ID_lt ||
114  expr.id()==ID_ge ||
115  expr.id()==ID_le)
116  {
117  exprt &lhs=expr.op0();
118  exprt &rhs=expr.op1();
119 
120  if(lhs.type()!=rhs.type())
121  {
122  typecast_exprt typecast(rhs, lhs.type());
123  expr.op1().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  ::fix_types(it->guard);
147  }
148  }
149 }
150 
152 {
153  for(patht::iterator it=path.begin();
154  it!=path.end();
155  ++it)
156  {
157  if(it->loc->is_assign() || it->loc->is_assume())
158  {
159  instructions.push_back(*it->loc);
160  }
161  else if(it->loc->is_goto())
162  {
163  if(it->guard.id()!=ID_nil)
164  {
165  add_instruction(ASSUME)->guard=it->guard;
166  }
167  }
168  else if(it->loc->is_assert())
169  {
170  add_instruction(ASSUME)->guard=it->loc->guard;
171  }
172  }
173 }
174 
176 {
177  goto_programt scratch;
178 
179  scratch.copy_from(program);
180  destructive_append(scratch);
181 }
182 
184  goto_programt &program,
185  goto_programt::targett loop_header)
186 {
187  append(program);
188 
189  // Update any back jumps to the loop header.
190  assume(false_exprt());
191 
193 
194  update();
195 
196  for(goto_programt::targett t=instructions.begin();
197  t!=instructions.end();
198  ++t)
199  {
200  if(t->is_backwards_goto())
201  {
202  t->targets.clear();
203  t->targets.push_back(end);
204  }
205  }
206 }
const namespacet ns
semantic type conversion
Definition: std_expr.h:1725
void slice(symex_target_equationt &equation)
Definition: slice.cpp:209
targett add_instruction()
Adds an instruction at the end.
targett assign(const exprt &lhs, const exprt &rhs)
void convert(prop_convt &prop_conv)
exprt & op0()
Definition: expr.h:84
instructionst instructions
The list of instructions in the goto program.
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:94
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
Decision Procedure Interface.
typet & type()
Definition: expr.h:60
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
std::map< irep_idt, exprt > valuest
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
goto_functionst functions
virtual resultt dec_solve()=0
targett assume(const exprt &guard)
exprt & rhs()
Definition: std_code.h:162
exprt eval(const exprt &e)
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:3753
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
symex_target_equationt equation
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
void append_path(patht &path)
void copy_from(const goto_program_templatet< codeT, guardT > &src)
Copy a full goto program, preserving targets.
prop_convt * checker
Base class for all expressions.
Definition: expr.h:46
Slicer for symex traces.
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
void destructive_append(goto_program_templatet< codet, exprt > &p)
Appends the given program, which is destroyed.
goto_symex_statet symex_state
Program Transformation.
goto_symext symex
unsigned count_assertions() const
Assignment.
Definition: std_code.h:144