CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
letify.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Introduce LET for common subexpressions
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "letify.h"
13
14#include <util/std_expr.h>
15
17 const exprt &expr,
19 std::vector<exprt> &let_order)
20{
21 // do not letify things with no children
22 if(expr.operands().empty())
23 return;
24
25 // did we already see the expression?
26 seen_expressionst::iterator entry = map.find(expr);
27
28 if(entry != map.end())
29 {
30 // yes, seen before, increase counter
31 let_count_idt &count_id = entry->second;
32 ++(count_id.count);
33 return;
34 }
35
36 // not seen before
37 for(auto &op : expr.operands())
39
41 map.find(expr) == map.end(), "expression should not have been seen yet");
42
44 symbol_exprt("_let_" + std::to_string(++let_id_count), expr.type());
45
46 map.insert(std::make_pair(expr, let_count_idt(1, let)));
47
48 let_order.push_back(expr);
49}
50
54 const exprt &expr,
55 const std::vector<exprt> &let_order,
56 const seen_expressionst &map)
57{
58 exprt result = substitute_let(expr, map);
59
60 // we build inside out, so go backwards in let order
61 for(auto r_it = let_order.rbegin(); r_it != let_order.rend(); r_it++)
62 {
63 const exprt &current = *r_it;
64
65 auto m_it = map.find(current);
66 PRECONDITION(m_it != map.end());
67
68 // Used more than once? Then a let pays off.
69 if(m_it->second.count > 1)
70 {
71 result = let_exprt(
72 m_it->second.let_symbol, substitute_let(current, map), result);
73 }
74 }
75
76 return result;
77}
78
80{
82 std::vector<exprt> let_order;
83
84 collect_bindings(expr, map, let_order);
85
86 return letify(expr, let_order, map);
87}
88
90{
91 if(expr.operands().empty())
92 return expr;
93
94 exprt tmp = expr;
95
96 for(auto &op : tmp.operands())
97 {
98 op.visit_pre([&map](exprt &expr) {
99 seen_expressionst::const_iterator it = map.find(expr);
100
101 // replace subexpression by let symbol if used more than once
102 if(it != map.end() && it->second.count > 1)
103 expr = it->second.let_symbol;
104 });
105 }
106
107 return tmp;
108}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
A let expression.
Definition std_expr.h:3331
static exprt letify(const exprt &expr, const std::vector< exprt > &let_order, const seen_expressionst &map)
Construct a nested let expression for expressions in let_order that are used more than once.
Definition letify.cpp:53
std::size_t let_id_count
Definition letify.h:22
void collect_bindings(const exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
Definition letify.cpp:16
std::unordered_map< exprt, let_count_idt, irep_hash > seen_expressionst
Definition letify.h:36
static exprt substitute_let(const exprt &expr, const seen_expressionst &map)
Definition letify.cpp:89
exprt operator()(const exprt &)
Definition letify.cpp:79
Expression to hold a symbol (variable)
Definition std_expr.h:131
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.