cprover
static_simplifier.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: goto-analyzer
4 
5 Author: Martin Brain, martin.brain@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
9 #include "static_simplifier.h"
10 
11 #include <util/message.h>
12 #include <util/options.h>
13 
19 
20 #include <analyses/ai.h>
21 
30  goto_modelt &goto_model,
31  const ai_baset &ai,
32  const optionst &options,
33  message_handlert &message_handler,
34  std::ostream &out)
35 {
36  struct counterst
37  {
38  counterst() :
39  asserts(0),
40  assumes(0),
41  gotos(0),
42  assigns(0),
43  function_calls(0) {}
44 
45  std::size_t asserts;
46  std::size_t assumes;
47  std::size_t gotos;
48  std::size_t assigns;
49  std::size_t function_calls;
50  };
51 
52  counterst simplified;
53  counterst unmodified;
54 
55  namespacet ns(goto_model.symbol_table);
56 
57  messaget m(message_handler);
58  m.status() << "Simplifying program" << messaget::eom;
59 
60  Forall_goto_functions(f_it, goto_model.goto_functions)
61  {
62  Forall_goto_program_instructions(i_it, f_it->second.body)
63  {
64  m.progress() << "Simplifying " << f_it->first << messaget::eom;
65 
66  if(i_it->is_assert())
67  {
68  exprt cond = i_it->get_condition();
69 
70  bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(cond, ns);
71 
72  if(unchanged)
73  unmodified.asserts++;
74  else
75  {
76  simplified.asserts++;
77  i_it->set_condition(cond);
78  }
79  }
80  else if(i_it->is_assume())
81  {
82  exprt cond = i_it->get_condition();
83 
84  bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(cond, ns);
85 
86  if(unchanged)
87  unmodified.assumes++;
88  else
89  {
90  simplified.assumes++;
91  i_it->set_condition(cond);
92  }
93  }
94  else if(i_it->is_goto())
95  {
96  exprt cond = i_it->get_condition();
97 
98  bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(cond, ns);
99 
100  if(unchanged)
101  unmodified.gotos++;
102  else
103  {
104  simplified.gotos++;
105  i_it->set_condition(cond);
106  }
107  }
108  else if(i_it->is_assign())
109  {
110  auto assign = i_it->get_assign();
111 
112  // Simplification needs to be aware of which side of the
113  // expression it is handling as:
114  // <i=0, j=1> i=j
115  // should simplify to i=1, not to 0=1.
116 
117  bool unchanged_lhs =
118  ai.abstract_state_before(i_it)->ai_simplify_lhs(assign.lhs(), ns);
119 
120  bool unchanged_rhs =
121  ai.abstract_state_before(i_it)->ai_simplify(assign.rhs(), ns);
122 
123  if(unchanged_lhs && unchanged_rhs)
124  unmodified.assigns++;
125  else
126  {
127  simplified.assigns++;
128  i_it->set_assign(assign);
129  }
130  }
131  else if(i_it->is_function_call())
132  {
133  auto fcall = i_it->get_function_call();
134 
135  bool unchanged =
136  ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns);
137 
138  exprt::operandst &args=fcall.arguments();
139 
140  for(auto &o : args)
141  unchanged &= ai.abstract_state_before(i_it)->ai_simplify(o, ns);
142 
143  if(unchanged)
144  unmodified.function_calls++;
145  else
146  {
147  simplified.function_calls++;
148  i_it->set_function_call(fcall);
149  }
150  }
151  }
152  }
153 
154  // Make sure the references are correct.
155  goto_model.goto_functions.update();
156 
157  m.status() << "Simplified: "
158  << " assert: " << simplified.asserts
159  << ", assume: " << simplified.assumes
160  << ", goto: " << simplified.gotos
161  << ", assigns: " << simplified.assigns
162  << ", function calls: " << simplified.function_calls
163  << "\n"
164  << "Unmodified: "
165  << " assert: " << unmodified.asserts
166  << ", assume: " << unmodified.assumes
167  << ", goto: " << unmodified.gotos
168  << ", assigns: " << unmodified.assigns
169  << ", function calls: " << unmodified.function_calls
170  << messaget::eom;
171 
172 
173  // Remove obviously unreachable things and (now) unconditional branches
174  if(options.get_bool_option("simplify-slicing"))
175  {
176  m.status() << "Removing unreachable instructions" << messaget::eom;
177 
178  // Removes goto false
179  remove_skip(goto_model);
180 
181  // Convert unreachable to skips
183 
184  // Remove all of the new skips
185  remove_skip(goto_model);
186  }
187 
188  // restore return types before writing the binary
189  restore_returns(goto_model);
190  goto_model.goto_functions.update();
191 
192  m.status() << "Writing goto binary" << messaget::eom;
193  return write_goto_binary(out,
194  ns.get_symbol_table(),
195  goto_model.goto_functions);
196 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
optionst
Definition: options.h:23
static_simplifier.h
static_simplifier
bool static_simplifier(goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Simplifies the program using the information in the abstract domain.
Definition: static_simplifier.cpp:29
messaget::status
mstreamt & status() const
Definition: message.h:414
write_goto_binary
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Definition: write_goto_binary.cpp:25
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:85
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
ai_baset::abstract_state_before
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
Definition: ai.h:221
options.h
Options.
messaget::eom
static eomt eom
Definition: message.h:297
write_goto_binary.h
Write GOTO binaries.
remove_unreachable
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
Definition: remove_unreachable.cpp:20
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
ai.h
Abstract Interpretation.
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
remove_returns.h
Replace function returns by assignments to global variables.
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
goto_functionst::update
void update()
Definition: goto_functions.h:81
messaget::progress
mstreamt & progress() const
Definition: message.h:424
remove_unreachable.h
Program Transformation.
remove_skip.h
Program Transformation.
message.h
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
restore_returns
void restore_returns(goto_modelt &goto_model)
restores return statements
Definition: remove_returns.cpp:403