cprover
static_simplifier.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: goto-analyzer
4
5Author: 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 // copy
129 auto call_function = as_const(*i_it).call_function();
130 auto call_arguments = as_const(*i_it).call_arguments();
131
132 bool unchanged =
133 ai.abstract_state_before(i_it)->ai_simplify(call_function, ns);
134
135 for(auto &o : call_arguments)
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->call_function() = std::move(call_function);
144 i_it->call_arguments() = std::move(call_arguments);
145 }
146 }
147 }
148 }
149
150 // Make sure the references are correct.
151 goto_model.goto_functions.update();
152
153 m.status() << "Simplified: "
154 << " assert: " << simplified.asserts
155 << ", assume: " << simplified.assumes
156 << ", goto: " << simplified.gotos
157 << ", assigns: " << simplified.assigns
158 << ", function calls: " << simplified.function_calls
159 << "\n"
160 << "Unmodified: "
161 << " assert: " << unmodified.asserts
162 << ", assume: " << unmodified.assumes
163 << ", goto: " << unmodified.gotos
164 << ", assigns: " << unmodified.assigns
165 << ", function calls: " << unmodified.function_calls
166 << messaget::eom;
167
168
169 // Remove obviously unreachable things and (now) unconditional branches
170 if(options.get_bool_option("simplify-slicing"))
171 {
172 m.status() << "Removing unreachable instructions" << messaget::eom;
173
174 // Removes goto false
175 remove_skip(goto_model);
176
177 // Convert unreachable to skips
179
180 // Remove all of the new skips
181 remove_skip(goto_model);
182 }
183
184 // restore return types before writing the binary
185 restore_returns(goto_model);
186 goto_model.goto_functions.update();
187
188 m.status() << "Writing goto binary" << messaget::eom;
189 return write_goto_binary(out,
190 ns.get_symbol_table(),
191 goto_model.goto_functions);
192}
Abstract Interpretation.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
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
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 & progress() const
Definition: message.h:424
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
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:88
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.