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 }
goto_symext::symex_with_state
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
Definition: symex_main.cpp:227
decision_proceduret::get
virtual exprt get(const exprt &expr) const =0
scratch_programt::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: scratch_program.h:80
scratch_programt::ns
namespacet ns
Definition: scratch_program.h:81
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
symex_target_equationt::convert
void convert(prop_convt &prop_conv)
Interface method to initiate the conversion into a decision procedure format.
Definition: symex_target_equation.cpp:366
optionst
Definition: options.h:22
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:412
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:86
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:506
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:591
fixedbv.h
goto_symex_statet::rename
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Definition: goto_symex_state.cpp:273
exprt
Base class for all expressions.
Definition: expr.h:54
scratch_programt::check_sat
bool check_sat()
Definition: scratch_program.h:65
scratch_program.h
exprt::op0
exprt & op0()
Definition: expr.h:84
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
scratch_programt::append
void append(goto_programt::instructionst &instructions)
Definition: scratch_program.cpp:72
decision_procedure.h
decision_proceduret::resultt::D_SATISFIABLE
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
symex_target_equationt::count_assertions
std::size_t count_assertions() const
Definition: symex_target_equation.h:346
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
scratch_programt::append_loop
void append_loop(goto_programt &program, goto_programt::targett loop_header)
Definition: scratch_program.cpp:179
scratch_programt::functions
goto_functionst functions
Definition: scratch_program.h:78
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:514
scratch_programt::fix_types
void fix_types()
Definition: scratch_program.cpp:124
scratch_programt::eval
exprt eval(const exprt &e)
Definition: scratch_program.cpp:63
decision_proceduret::dec_solve
virtual resultt dec_solve()=0
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
exprt::op1
exprt & op1()
Definition: expr.h:87
fix_types
static void fix_types(exprt &expr)
Definition: scratch_program.cpp:99
irept::swap
void swap(irept &irep)
Definition: irep.h:303
scratch_programt::assume
targett assume(const exprt &guard)
Definition: scratch_program.cpp:91
irept::id
const irep_idt & id() const
Definition: irep.h:259
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
END_FUNCTION
Definition: goto_program.h:42
SKIP
Definition: goto_program.h:38
scratch_programt::equation
symex_target_equationt equation
Definition: scratch_program.h:82
scratch_programt::append_path
void append_path(patht &path)
Definition: scratch_program.cpp:147
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:524
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
ASSIGN
Definition: goto_program.h:46
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
patht
std::list< path_nodet > patht
Definition: path.h:45
scratch_programt::symex
goto_symext symex
Definition: scratch_program.h:85
ASSUME
Definition: goto_program.h:35
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
scratch_programt::get_default_options
static optionst get_default_options()
Definition: scratch_program.cpp:205
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
remove_skip.h
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
scratch_programt::checker
prop_convt * checker
Definition: scratch_program.h:90
slice.h
scratch_programt::assign
targett assign(const exprt &lhs, const exprt &rhs)
Definition: scratch_program.cpp:80
scratch_programt::symex_state
goto_symex_statet symex_state
Definition: scratch_program.h:77
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
slice
void slice(symex_target_equationt &equation)
Definition: slice.cpp:208