cprover
expr2statement_list.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Conversion from Expression or Type to Statement List
4 
5 Author: Matthias Weiss, matthias.weiss@diffblue.com
6 
7 \*******************************************************************/
8 
9 #include "expr2statement_list.h"
10 
11 #include <ansi-c/expr2c.h>
12 
13 #include <util/suffix.h>
14 #include <util/symbol_table.h>
15 
16 #include <algorithm>
17 #include <cstring>
18 #include <iostream>
19 
21 #define AND 'A'
22 
24 #define OR 'O'
25 
27 #define XOR 'X'
28 
30 #define NOT_POSTFIX 'N'
31 
33 #define NOT "NOT"
34 
36 #define OPERAND_SEPARATOR ' '
37 
39 #define LINE_SEPARATOR ";\n"
40 
43 #define NESTING_OPEN_LINE_SEPARATOR "(;\n"
44 
47 #define NESTING_CLOSED_LINE_SEPARATOR ");\n"
48 
50 #define REFERENCE_FLAG '#'
51 
53 #define SCOPE_SEPARATOR "::"
54 
62 static std::vector<exprt>
63 instrument_equal_operands(const exprt &lhs, const exprt &rhs)
64 {
65  std::vector<exprt> result;
66  if(ID_not != lhs.id() && ID_not != rhs.id())
67  {
68  // lhs == rhs is equivalent to X lhs; XN rhs;
69  result.push_back(lhs);
70  result.push_back(not_exprt{rhs});
71  }
72  else if(ID_not != lhs.id() && ID_not == rhs.id())
73  {
74  // lhs == !rhs is equivalent to X lhs; X rhs;
75  result.push_back(lhs);
76  result.push_back(to_not_expr(rhs).op());
77  }
78  else if(ID_not == lhs.id() && ID_not != rhs.id())
79  {
80  // !lhs == rhs is equivalent to X lhs; X rhs;
81  result.push_back(to_not_expr(lhs).op());
82  result.push_back(rhs);
83  }
84  else // ID_not == lhs.id() && ID_not == rhs.id()
85  {
86  // !lhs == !rhs is equivalent to X lhs; XN rhs;
87  result.push_back(to_not_expr(lhs).op());
88  result.push_back(rhs);
89  }
90  return result;
91 }
92 
97 static bool is_not_bool(const exprt &expr)
98 {
99  if(!expr.is_boolean())
100  return true;
101  for(const exprt &op : expr.operands())
102  if(!op.is_boolean())
103  return true;
104  return false;
105 }
106 
107 std::string expr2stl(const exprt &expr, const namespacet &ns)
108 {
109  expr2stlt expr2stl{ns};
110 
111  return expr2stl.convert(expr);
112 }
113 
114 std::string type2stl(const typet &type, const namespacet &ns)
115 {
116  // TODO: Implement type2stl.
117  // Expand this section so that it is able to properly convert from
118  // CBMC types to STL code.
119  return type2c(type, ns);
120 }
121 
123  : inside_bit_string(false), is_reference(false), ns(ns)
124 {
125 }
126 
127 std::string expr2stlt::convert(const exprt &expr)
128 {
129  // Redirect to expr2c if no boolean expression.
130  if(is_not_bool(expr))
131  return expr2c(expr, ns);
132 
133  if(ID_and == expr.id())
134  convert(to_and_expr(expr));
135  else if(ID_or == expr.id())
136  convert(to_or_expr(expr));
137  else if(ID_xor == expr.id())
138  convert(to_xor_expr(expr));
139  else if(ID_notequal == expr.id())
140  convert(to_notequal_expr(expr));
141  else if(ID_equal == expr.id())
142  convert(to_equal_expr(expr));
143  else if(ID_symbol == expr.id())
144  convert(to_symbol_expr(expr));
145  else if(ID_not == expr.id() && to_not_expr(expr).op().type().id() == ID_bool)
146  convert(to_not_expr(expr));
147  else // TODO: support more instructions in expr2stl.
148  return expr2c(expr, ns);
149 
150  return result.str();
151 }
152 
153 void expr2stlt::convert(const and_exprt &expr)
154 {
155  std::vector<exprt> operands = expr.operands();
156  convert_multiary_bool(operands, AND);
157 }
158 
159 void expr2stlt::convert(const or_exprt &expr)
160 {
161  std::vector<exprt> operands = expr.operands();
162  convert_multiary_bool(operands, OR);
163 }
164 
165 void expr2stlt::convert(const xor_exprt &expr)
166 {
167  std::vector<exprt> operands = expr.operands();
168  convert_multiary_bool(operands, XOR);
169 }
170 
172 {
173  std::vector<exprt> operands = expr.operands();
174  convert_multiary_bool(operands, XOR);
175 }
176 
178 {
179  std::vector<exprt> operands =
180  instrument_equal_operands(expr.lhs(), expr.rhs());
181  convert_multiary_bool(operands, XOR);
182 }
183 
184 void expr2stlt::convert(const not_exprt &expr)
185 {
186  // If a NOT expression is being handled here it must always mark the
187  // beginning of a new bit string.
189 
190  if(ID_symbol == expr.op().id())
191  {
192  // Use AN to load the symbol.
193  is_reference = true;
195  convert(to_symbol_expr(expr.op()));
197  }
198  else
199  {
200  // Use NOT to negate the RLO after the wrapped expression was loaded.
201  convert(expr.op());
203  }
204 }
205 
207 {
208  if(is_reference)
209  {
211  is_reference = false;
212  }
214 }
215 
217  std::vector<exprt> &operands,
218  const char operation)
219 {
221  convert_multiary_bool_operands(operands, operation);
222  else
223  {
225  convert_multiary_bool_operands(operands, operation);
226  }
227 }
228 
230  const std::vector<exprt> &operands,
231  const char operation)
232 {
233  for(const exprt &op : operands)
234  {
235  if(ID_not == op.id())
236  {
237  result << operation << NOT_POSTFIX;
239  }
240  else
241  {
242  result << operation;
244  }
245  }
246 }
247 
249 {
250  if(op.id() == ID_symbol)
251  {
252  is_reference = true;
254  convert(to_symbol_expr(op));
256  }
257  else
258  {
259  inside_bit_string = false;
261  convert(op);
263  }
264 }
265 
266 void expr2stlt::convert_first_non_trivial_operand(std::vector<exprt> &operands)
267 {
268  exprt non_trivial_op;
269  for(auto it{begin(operands)}; it != end(operands); ++it)
270  {
271  if(
272  (ID_symbol == it->id()) ||
273  (ID_not == it->id() && ID_symbol == to_not_expr(*it).op().id()))
274  continue;
275  else
276  {
277  non_trivial_op = *it;
278  operands.erase(it);
279  break;
280  }
281  }
282  // Important for some scenarios: Convert complex op first, set bit string
283  // flag to true afterwards.
284  if(non_trivial_op.is_not_nil())
285  convert(non_trivial_op);
286 
287  inside_bit_string = true;
288 }
289 
291 {
292  const symbolt *symbol;
293  std::string shorthand = id2string(identifier);
294  if(
295  !ns.lookup(identifier, symbol) && !symbol->base_name.empty() &&
296  has_suffix(shorthand, id2string(symbol->base_name)))
297  return symbol->base_name;
298 
299  const std::string::size_type pos = shorthand.rfind(SCOPE_SEPARATOR);
300  if(pos != std::string::npos)
301  shorthand.erase(0, pos + std::strlen(SCOPE_SEPARATOR));
302 
303  return shorthand;
304 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
instrument_equal_operands
static std::vector< exprt > instrument_equal_operands(const exprt &lhs, const exprt &rhs)
Modifies the parameters of a binary equal expression with the help of its symmetry properties.
Definition: expr2statement_list.cpp:63
expr2statement_list.h
NOT_POSTFIX
#define NOT_POSTFIX
Postfix for any negated boolean instruction.
Definition: expr2statement_list.cpp:30
NESTING_CLOSED_LINE_SEPARATOR
#define NESTING_CLOSED_LINE_SEPARATOR
Separator for the end of an instruction that closes a nesting layer.
Definition: expr2statement_list.cpp:47
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:641
pos
literalt pos(literalt a)
Definition: literal.h:194
typet
The type of an expression, extends irept.
Definition: type.h:29
xor_exprt
Boolean XOR.
Definition: std_expr.h:2308
expr2stlt
Class for saving the internal state of the conversion process.
Definition: expr2statement_list.h:32
and_exprt
Boolean AND.
Definition: std_expr.h:2137
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:631
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
expr2stlt::id_shorthand
irep_idt id_shorthand(const irep_idt &identifier)
Returns the given identifier in a form that is compatible with STL by looking up the symbol or cuttin...
Definition: expr2statement_list.cpp:290
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
equal_exprt
Equality.
Definition: std_expr.h:1190
notequal_exprt
Disequality.
Definition: std_expr.h:1248
OPERAND_SEPARATOR
#define OPERAND_SEPARATOR
Separator between the instruction code and it's operand.
Definition: expr2statement_list.cpp:36
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
expr2stlt::convert
std::string convert(const exprt &expr)
Invokes the conversion process for the given expression and calls itself recursively in the process.
Definition: expr2statement_list.cpp:127
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
REFERENCE_FLAG
#define REFERENCE_FLAG
Prefix for the reference to any variable.
Definition: expr2statement_list.cpp:50
or_exprt
Boolean OR.
Definition: std_expr.h:2245
SCOPE_SEPARATOR
#define SCOPE_SEPARATOR
CBMC-internal separator for variable scopes.
Definition: expr2statement_list.cpp:53
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3878
to_xor_expr
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2328
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
expr2stlt::ns
const namespacet & ns
Contains the symbol table of the current program to convert.
Definition: expr2statement_list.h:42
type2stl
std::string type2stl(const typet &type, const namespacet &ns)
Converts a given type to human-readable STL code.
Definition: expr2statement_list.cpp:114
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
expr2stlt::expr2stlt
expr2stlt(const namespacet &ns)
Creates a new instance of the converter.
Definition: expr2statement_list.cpp:122
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1273
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
expr2stlt::convert_bool_operand
void convert_bool_operand(const exprt &op)
Converts a single boolean operand and introduces an additional nesting layer if needed.
Definition: expr2statement_list.cpp:248
irept::id
const irep_idt & id() const
Definition: irep.h:418
dstringt::empty
bool empty() const
Definition: dstring.h:88
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
LINE_SEPARATOR
#define LINE_SEPARATOR
Separator between the end of an instruction and the next one.
Definition: expr2statement_list.cpp:39
AND
#define AND
STL code for an AND instruction.
Definition: expr2statement_list.cpp:21
to_or_expr
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2292
XOR
#define XOR
STL code for a XOR instruction.
Definition: expr2statement_list.cpp:27
suffix.h
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2868
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
NESTING_OPEN_LINE_SEPARATOR
#define NESTING_OPEN_LINE_SEPARATOR
Separator for the end of an instruction that introduces a new layer of nesting.
Definition: expr2statement_list.cpp:43
symbolt
Symbol table entry.
Definition: symbol.h:28
expr2stlt::convert_multiary_bool_operands
void convert_multiary_bool_operands(const std::vector< exprt > &operands, const char operation)
Iterates through all the given operands and converts them depending on the operation.
Definition: expr2statement_list.cpp:229
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1230
expr2stl
std::string expr2stl(const exprt &expr, const namespacet &ns)
Converts a given expression to human-readable STL code.
Definition: expr2statement_list.cpp:107
expr2stlt::inside_bit_string
bool inside_bit_string
Internal representation of the FC bit in STL.
Definition: expr2statement_list.h:35
expr2stlt::convert_multiary_bool
void convert_multiary_bool(std::vector< exprt > &operands, const char operation)
Iterates through all the given operands and converts them depending on the operation.
Definition: expr2statement_list.cpp:216
exprt::operands
operandst & operands()
Definition: expr.h:95
NOT
#define NOT
STL code for a NOT instruction.
Definition: expr2statement_list.cpp:33
type2c
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3894
OR
#define OR
STL code for an OR instruction.
Definition: expr2statement_list.cpp:24
symbol_table.h
Author: Diffblue Ltd.
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
expr2stlt::convert_first_non_trivial_operand
void convert_first_non_trivial_operand(std::vector< exprt > &operands)
Iterates through all the given operands in search for the first non-trivial operand (that encloses al...
Definition: expr2statement_list.cpp:266
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:119
expr2stlt::is_reference
bool is_reference
Flag to specify if the next symbol to convert is a reference to a variable.
Definition: expr2statement_list.h:39
to_and_expr
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2184
is_not_bool
static bool is_not_bool(const exprt &expr)
Checks if the expression or one of its parameters is not of type bool.
Definition: expr2statement_list.cpp:97
expr2stlt::result
std::stringstream result
Used for saving intermediate results of the conversion process.
Definition: expr2statement_list.h:45
not_exprt
Boolean negation.
Definition: std_expr.h:2843