cprover
symex_other.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
14 #include <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/rename.h>
18 #include <util/base_type.h>
19 #include <util/std_expr.h>
20 #include <util/byte_operators.h>
21 
22 #include <util/c_types.h>
23 
25  const goto_functionst &goto_functions,
26  statet &state)
27 {
28  const goto_programt::instructiont &instruction=*state.source.pc;
29 
30  const codet &code=to_code(instruction.code);
31 
32  const irep_idt &statement=code.get_statement();
33 
34  if(statement==ID_expression)
35  {
36  // ignore
37  }
38  else if(statement==ID_cpp_delete ||
39  statement=="cpp_delete[]")
40  {
41  codet clean_code=code;
42  clean_expr(clean_code, state, false);
43  symex_cpp_delete(state, clean_code);
44  }
45  else if(statement==ID_free)
46  {
47  // ignore
48  }
49  else if(statement==ID_printf)
50  {
51  codet clean_code=code;
52  clean_expr(clean_code, state, false);
53  symex_printf(state, nil_exprt(), clean_code);
54  }
55  else if(statement==ID_input)
56  {
57  codet clean_code(code);
58  clean_expr(clean_code, state, false);
59  symex_input(state, clean_code);
60  }
61  else if(statement==ID_output)
62  {
63  codet clean_code(code);
64  clean_expr(clean_code, state, false);
65  symex_output(state, clean_code);
66  }
67  else if(statement==ID_decl)
68  {
69  assert(false); // see symex_decl.cpp
70  }
71  else if(statement==ID_nondet)
72  {
73  // like skip
74  }
75  else if(statement==ID_asm)
76  {
77  // we ignore this for now
78  }
79  else if(statement==ID_array_copy ||
80  statement==ID_array_replace)
81  {
82  assert(code.operands().size()==2);
83 
84  codet clean_code(code);
85 
86  // we need to add dereferencing for both operands
87  dereference_exprt d0, d1;
88  d0.op0()=code.op0();
89  d0.type()=empty_typet();
90  d1.op0()=code.op1();
91  d1.type()=empty_typet();
92 
93  clean_code.op0()=d0;
94  clean_code.op1()=d1;
95 
96  clean_expr(clean_code.op0(), state, true);
97  exprt op0_offset=from_integer(0, index_type());
98  if(clean_code.op0().id()==byte_extract_id() &&
99  clean_code.op0().type().id()==ID_empty)
100  {
101  op0_offset=to_byte_extract_expr(clean_code.op0()).offset();
102  clean_code.op0()=clean_code.op0().op0();
103  }
104  clean_expr(clean_code.op1(), state, false);
105  exprt op1_offset=from_integer(0, index_type());
106  if(clean_code.op1().id()==byte_extract_id() &&
107  clean_code.op1().type().id()==ID_empty)
108  {
109  op1_offset=to_byte_extract_expr(clean_code.op1()).offset();
110  clean_code.op1()=clean_code.op1().op0();
111  }
112 
113  process_array_expr(clean_code.op0());
114  clean_expr(clean_code.op0(), state, true);
115  process_array_expr(clean_code.op1());
116  clean_expr(clean_code.op1(), state, false);
117 
118 
119  if(!base_type_eq(clean_code.op0().type(),
120  clean_code.op1().type(), ns) ||
121  !op0_offset.is_zero() || !op1_offset.is_zero())
122  {
124 
125  if(statement==ID_array_copy)
126  {
127  be.op()=clean_code.op1();
128  be.offset()=op1_offset;
129  be.type()=clean_code.op0().type();
130  clean_code.op1()=be;
131 
132  if(!op0_offset.is_zero())
133  {
134  byte_extract_exprt op0(
135  byte_extract_id(),
136  clean_code.op0(),
137  op0_offset,
138  clean_code.op0().type());
139  clean_code.op0()=op0;
140  }
141  }
142  else
143  {
144  // ID_array_replace
145  be.op()=clean_code.op0();
146  be.offset()=op0_offset;
147  be.type()=clean_code.op1().type();
148  clean_code.op0()=be;
149 
150  if(!op1_offset.is_zero())
151  {
152  byte_extract_exprt op1(
153  byte_extract_id(),
154  clean_code.op1(),
155  op1_offset,
156  clean_code.op1().type());
157  clean_code.op1()=op1;
158  }
159  }
160  }
161 
162  code_assignt assignment;
163  assignment.lhs()=clean_code.op0();
164  assignment.rhs()=clean_code.op1();
165  symex_assign(state, assignment);
166  }
167  else if(statement==ID_array_set)
168  {
169  assert(code.operands().size()==2);
170 
171  codet clean_code(code);
172 
173  // we need to add dereferencing for the first operand
175  d0.op0()=code.op0();
176  d0.type()=empty_typet();
177 
178  clean_code.op0()=d0;
179 
180  clean_expr(clean_code.op0(), state, true);
181  if(clean_code.op0().id()==byte_extract_id() &&
182  clean_code.op0().type().id()==ID_empty)
183  clean_code.op0()=clean_code.op0().op0();
184  clean_expr(clean_code.op1(), state, false);
185 
186  process_array_expr(clean_code.op0());
187  clean_expr(clean_code.op0(), state, true);
188 
189  const typet &op0_type=ns.follow(clean_code.op0().type());
190 
191  if(op0_type.id()!=ID_array)
192  throw "array_set expects array operand";
193 
194  const array_typet &array_type=
195  to_array_type(op0_type);
196 
197  if(!base_type_eq(array_type.subtype(),
198  clean_code.op1().type(), ns))
199  clean_code.op1().make_typecast(array_type.subtype());
200 
201  code_assignt assignment;
202  assignment.lhs()=clean_code.op0();
203  assignment.rhs()=array_of_exprt(clean_code.op1(), array_type);
204  symex_assign(state, assignment);
205  }
206  else if(statement==ID_user_specified_predicate ||
207  statement==ID_user_specified_parameter_predicates ||
208  statement==ID_user_specified_return_predicates)
209  {
210  // like skip
211  }
212  else if(statement==ID_fence)
213  {
214  target.memory_barrier(state.guard.as_expr(), state.source);
215  }
216  else
217  throw "unexpected statement: "+id2string(statement);
218 }
const irep_idt & get_statement() const
Definition: std_code.h:37
The type of an expression.
Definition: type.h:20
exprt as_expr() const
Definition: guard.h:43
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
symex_targett & target
Definition: goto_symex.h:105
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
virtual void symex_assign(statet &state, const code_assignt &code)
goto_programt::const_targett pc
Definition: symex_target.h:32
exprt & op0()
Definition: expr.h:84
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
typet & type()
Definition: expr.h:60
virtual void symex_printf(statet &state, const exprt &lhs, const exprt &rhs)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
exprt & lhs()
Definition: std_code.h:157
Expression classes for byte-level operators.
The NIL expression.
Definition: std_expr.h:3764
exprt & rhs()
Definition: std_code.h:162
The empty type.
Definition: std_types.h:53
Operator to dereference a pointer.
Definition: std_expr.h:2701
Symbolic Execution.
API to expression classes.
exprt & op1()
Definition: expr.h:87
irep_idt byte_extract_id()
virtual void symex_input(statet &state, const codet &code)
virtual void symex_other(const goto_functionst &goto_functions, statet &state)
Definition: symex_other.cpp:24
array constructor from single element
Definition: std_expr.h:1252
bitvector_typet index_type()
Definition: c_types.cpp:15
void clean_expr(exprt &expr, statet &state, bool write)
Base class for all expressions.
Definition: expr.h:46
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
arrays with given size
Definition: std_types.h:901
void process_array_expr(exprt &expr)
virtual void symex_cpp_delete(statet &state, const codet &code)
A statement in a programming language.
Definition: std_code.h:19
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
virtual void symex_output(statet &state, const codet &code)
operandst & operands()
Definition: expr.h:70
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const namespacet & ns
Definition: goto_symex.h:104
virtual void memory_barrier(const exprt &guard, const sourcet &source)=0
Assignment.
Definition: std_code.h:144
symex_targett::sourcet source