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  for(auto &gf_entry : goto_model.goto_functions.function_map)
61  {
62  Forall_goto_program_instructions(i_it, gf_entry.second.body)
63  {
64  m.progress() << "Simplifying " << gf_entry.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  // Simplification needs to be aware of which side of the
111  // expression it is handling as:
112  // <i=0, j=1> i=j
113  // should simplify to i=1, not to 0=1.
114 
115  bool unchanged_lhs = ai.abstract_state_before(i_it)->ai_simplify_lhs(
116  i_it->assign_lhs_nonconst(), ns);
117 
118  bool unchanged_rhs = ai.abstract_state_before(i_it)->ai_simplify(
119  i_it->assign_rhs_nonconst(), ns);
120 
121  if(unchanged_lhs && unchanged_rhs)
122  unmodified.assigns++;
123  else
124  simplified.assigns++;
125  }
126  else if(i_it->is_function_call())
127  {
128  auto fcall = i_it->get_function_call();
129 
130  bool unchanged =
131  ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns);
132 
133  exprt::operandst &args=fcall.arguments();
134 
135  for(auto &o : args)
136  unchanged &= ai.abstract_state_before(i_it)->ai_simplify(o, ns);
137 
138  if(unchanged)
139  unmodified.function_calls++;
140  else
141  {
142  simplified.function_calls++;
143  i_it->set_function_call(fcall);
144  }
145  }
146  }
147  }
148 
149  // Make sure the references are correct.
150  goto_model.goto_functions.update();
151 
152  m.status() << "Simplified: "
153  << " assert: " << simplified.asserts
154  << ", assume: " << simplified.assumes
155  << ", goto: " << simplified.gotos
156  << ", assigns: " << simplified.assigns
157  << ", function calls: " << simplified.function_calls
158  << "\n"
159  << "Unmodified: "
160  << " assert: " << unmodified.asserts
161  << ", assume: " << unmodified.assumes
162  << ", goto: " << unmodified.gotos
163  << ", assigns: " << unmodified.assigns
164  << ", function calls: " << unmodified.function_calls
165  << messaget::eom;
166 
167 
168  // Remove obviously unreachable things and (now) unconditional branches
169  if(options.get_bool_option("simplify-slicing"))
170  {
171  m.status() << "Removing unreachable instructions" << messaget::eom;
172 
173  // Removes goto false
174  remove_skip(goto_model);
175 
176  // Convert unreachable to skips
178 
179  // Remove all of the new skips
180  remove_skip(goto_model);
181  }
182 
183  // restore return types before writing the binary
184  restore_returns(goto_model);
185  goto_model.goto_functions.update();
186 
187  m.status() << "Writing goto binary" << messaget::eom;
188  return write_goto_binary(out,
189  ns.get_symbol_table(),
190  goto_model.goto_functions);
191 }
Abstract Interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
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:223
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & status() const
Definition: message.h:414
mstreamt & progress() const
Definition: message.h:424
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:123
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
Options.
void restore_returns(goto_modelt &goto_model)
restores return statements
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
Program Transformation.
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
Program Transformation.
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.
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.
Write GOTO binaries.