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  bool unchanged =
69  ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);
70 
71  if(unchanged)
72  unmodified.asserts++;
73  else
74  simplified.asserts++;
75  }
76  else if(i_it->is_assume())
77  {
78  bool unchanged =
79  ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);
80 
81  if(unchanged)
82  unmodified.assumes++;
83  else
84  simplified.assumes++;
85  }
86  else if(i_it->is_goto())
87  {
88  bool unchanged =
89  ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);
90 
91  if(unchanged)
92  unmodified.gotos++;
93  else
94  simplified.gotos++;
95  }
96  else if(i_it->is_assign())
97  {
98  code_assignt &assign=to_code_assign(i_it->code);
99 
100  // Simplification needs to be aware of which side of the
101  // expression it is handling as:
102  // <i=0, j=1> i=j
103  // should simplify to i=1, not to 0=1.
104 
105  bool unchanged_lhs =
106  ai.abstract_state_before(i_it)->ai_simplify_lhs(assign.lhs(), ns);
107 
108  bool unchanged_rhs =
109  ai.abstract_state_before(i_it)->ai_simplify(assign.rhs(), ns);
110 
111  if(unchanged_lhs && unchanged_rhs)
112  unmodified.assigns++;
113  else
114  simplified.assigns++;
115  }
116  else if(i_it->is_function_call())
117  {
118  code_function_callt &fcall=to_code_function_call(i_it->code);
119 
120  bool unchanged =
121  ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns);
122 
123  exprt::operandst &args=fcall.arguments();
124 
125  for(auto &o : args)
126  unchanged &= ai.abstract_state_before(i_it)->ai_simplify(o, ns);
127 
128  if(unchanged)
129  unmodified.function_calls++;
130  else
131  simplified.function_calls++;
132  }
133  }
134  }
135 
136  // Make sure the references are correct.
137  goto_model.goto_functions.update();
138 
139  m.status() << "Simplified: "
140  << " assert: " << simplified.asserts
141  << ", assume: " << simplified.assumes
142  << ", goto: " << simplified.gotos
143  << ", assigns: " << simplified.assigns
144  << ", function calls: " << simplified.function_calls
145  << "\n"
146  << "Unmodified: "
147  << " assert: " << unmodified.asserts
148  << ", assume: " << unmodified.assumes
149  << ", goto: " << unmodified.gotos
150  << ", assigns: " << unmodified.assigns
151  << ", function calls: " << unmodified.function_calls
152  << messaget::eom;
153 
154 
155  // Remove obviously unreachable things and (now) unconditional branches
156  if(options.get_bool_option("simplify-slicing"))
157  {
158  m.status() << "Removing unreachable instructions" << messaget::eom;
159 
160  // Removes goto false
161  remove_skip(goto_model);
162 
163  // Convert unreachable to skips
165 
166  // Remove all of the new skips
167  remove_skip(goto_model);
168  }
169 
170  // restore return types before writing the binary
171  restore_returns(goto_model);
172  goto_model.goto_functions.update();
173 
174  m.status() << "Writing goto binary" << messaget::eom;
175  return write_goto_binary(out,
176  ns.get_symbol_table(),
177  goto_model.goto_functions);
178 }
mstreamt & progress() const
Definition: message.h:411
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
exprt & lhs()
Definition: std_code.h:269
Symbol Table + CFG.
argumentst & arguments()
Definition: std_code.h:1109
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
exprt & rhs()
Definition: std_code.h:274
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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.
codet representation of a function call statement.
Definition: std_code.h:1036
void restore_returns(goto_modelt &goto_model)
restores return statements
Remove function returns.
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
std::vector< exprt > operandst
Definition: expr.h:57
static eomt eom
Definition: message.h:284
mstreamt & status() const
Definition: message.h:401
Abstract Interpretation.
exprt & function()
Definition: std_code.h:1099
The basic interface of an abstract interpreter.
Definition: ai.h:32
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
#define Forall_goto_functions(it, functions)
Program Transformation.
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Options.
Program Transformation.
Write GOTO binaries.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173