cprover
std_code.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Data structures representing statements in a program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "std_code.h"
13 
14 #include "arith_tools.h"
15 #include "c_types.h"
16 #include "std_expr.h"
17 #include "string_constant.h"
18 
24 {
25  if(get_statement()==ID_block)
26  return static_cast<code_blockt &>(*this);
27 
28  exprt tmp;
29  tmp.swap(*this);
30 
31  *this = codet(ID_block);
32  add_to_operands(std::move(tmp));
33 
34  return static_cast<code_blockt &>(*this);
35 }
36 
40 {
41  const irep_idt &statement=get_statement();
42 
43  if(has_operands())
44  {
45  if(statement==ID_block)
46  return to_code(op0()).first_statement();
47  else if(statement==ID_label)
48  return to_code(op0()).first_statement();
49  }
50 
51  return *this;
52 }
53 
56 {
57  const irep_idt &statement=get_statement();
58 
59  if(has_operands())
60  {
61  if(statement==ID_block)
62  return to_code(op0()).first_statement();
63  else if(statement==ID_label)
64  return to_code(op0()).first_statement();
65  }
66 
67  return *this;
68 }
69 
73 {
74  const irep_idt &statement=get_statement();
75 
76  if(has_operands())
77  {
78  if(statement==ID_block)
79  return to_code(operands().back()).last_statement();
80  else if(statement==ID_label)
81  return to_code(operands().back()).last_statement();
82  }
83 
84  return *this;
85 }
86 
89 {
90  const irep_idt &statement=get_statement();
91 
92  if(has_operands())
93  {
94  if(statement==ID_block)
95  return to_code(operands().back()).last_statement();
96  else if(statement==ID_label)
97  return to_code(operands().back()).last_statement();
98  }
99 
100  return *this;
101 }
102 
105 void code_blockt::append(const code_blockt &extra_block)
106 {
107  statements().reserve(statements().size() + extra_block.statements().size());
108 
109  for(const auto &statement : extra_block.statements())
110  {
111  add(statement);
112  }
113 }
114 
116 {
117  codet *last=this;
118 
119  while(true)
120  {
121  const irep_idt &statement=last->get_statement();
122 
123  if(statement==ID_block &&
124  !to_code_block(*last).statements().empty())
125  {
126  last=&to_code_block(*last).statements().back();
127  }
128  else if(statement==ID_label)
129  {
130  last = &(to_code_label(*last).code());
131  }
132  else
133  break;
134  }
135 
136  return *last;
137 }
138 
140  const exprt &condition, const source_locationt &loc)
141 {
142  code_blockt result({code_assertt(condition), code_assumet(condition)});
143 
144  for(auto &op : result.statements())
145  op.add_source_location() = loc;
146 
147  result.add_source_location() = loc;
148 
149  return result;
150 }
151 
153 {
154  const auto &sub = find(ID_parameters).get_sub();
155  std::vector<irep_idt> result;
156  result.reserve(sub.size());
157  for(const auto &s : sub)
158  result.push_back(s.get(ID_identifier));
159  return result;
160 }
161 
163  const std::vector<irep_idt> &parameter_identifiers)
164 {
165  auto &sub = add(ID_parameters).get_sub();
166  sub.reserve(parameter_identifiers.size());
167  for(const auto &id : parameter_identifiers)
168  {
169  sub.push_back(irept(ID_parameter));
170  sub.back().set(ID_identifier, id);
171  }
172 }
173 
175  std::vector<exprt> arguments,
177  : codet{ID_input, std::move(arguments)}
178 {
179  if(location)
180  add_source_location() = std::move(*location);
181  check(*this, validation_modet::INVARIANT);
182 }
183 
185  const irep_idt &description,
186  exprt expression,
189  string_constantt(description),
190  from_integer(0, index_type()))),
191  std::move(expression)},
192  std::move(location)}
193 {
194 }
195 
196 void code_inputt::check(const codet &code, const validation_modet vm)
197 {
198  DATA_CHECK(
199  vm, code.operands().size() >= 2, "input must have at least two operands");
200 }
201 
203  std::vector<exprt> arguments,
205  : codet{ID_output, std::move(arguments)}
206 {
207  if(location)
208  add_source_location() = std::move(*location);
209  check(*this, validation_modet::INVARIANT);
210 }
211 
213  const irep_idt &description,
214  exprt expression,
217  string_constantt(description),
218  from_integer(0, index_type()))),
219  std::move(expression)},
220  std::move(location)}
221 {
222 }
223 
224 void code_outputt::check(const codet &code, const validation_modet vm)
225 {
226  DATA_CHECK(
227  vm, code.operands().size() >= 2, "output must have at least two operands");
228 }
229 
231  exprt start_index,
232  exprt end_index,
233  symbol_exprt loop_index,
234  codet body,
235  source_locationt location)
236 {
237  PRECONDITION(start_index.type() == loop_index.type());
238  PRECONDITION(end_index.type() == loop_index.type());
240  loop_index,
241  plus_exprt(loop_index, from_integer(1, loop_index.type())),
242  location);
243 
244  return code_fort{
245  code_assignt{loop_index, std::move(start_index)},
246  binary_relation_exprt{loop_index, ID_lt, std::move(end_index)},
247  std::move(inc),
248  std::move(body)};
249 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:173
code_function_bodyt::set_parameter_identifiers
void set_parameter_identifiers(const std::vector< irep_idt > &)
Definition: std_code.cpp:162
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:101
code_inputt::code_inputt
code_inputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_input in user code.
Definition: std_code.cpp:174
code_fort
codet representation of a for statement.
Definition: std_code.h:1023
codet::first_statement
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them.
Definition: std_code.cpp:39
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
codet::codet
codet(const irep_idt &statement)
Definition: std_code.h:40
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:590
code_outputt::check
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.cpp:224
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:887
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
string_constantt
Definition: string_constant.h:16
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
create_fatal_assertion
code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &loc)
Create a fatal assertion, which checks a condition and then halts if it does not hold.
Definition: std_code.cpp:139
irept::irept
irept()=default
code_labelt::code
codet & code()
Definition: std_code.h:1403
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:158
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:181
code_outputt
A codet representing the declaration that an output of a particular description has a value which cor...
Definition: std_code.h:695
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_outputt::code_outputt
code_outputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_output in user code.
Definition: std_code.cpp:202
code_function_bodyt::get_parameter_identifiers
std::vector< irep_idt > get_parameter_identifiers() const
Definition: std_code.cpp:152
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
code_inputt::check
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.cpp:196
codet::make_block
class code_blockt & make_block()
If this codet is a code_blockt (i.e. it represents a block of statements), return the unmodified inpu...
Definition: std_code.cpp:23
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:538
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1430
codet::last_statement
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them.
Definition: std_code.cpp:72
side_effect_expr_assignt
A side_effect_exprt that performs an assignment.
Definition: std_code.h:2000
irept::swap
void swap(irept &irep)
Definition: irep.h:463
validation_modet
validation_modet
Definition: validation_mode.h:13
code_blockt::add
void add(const codet &code)
Definition: std_code.h:211
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
source_locationt
Definition: source_location.h:20
code_inputt
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:648
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
code_blockt::append
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:105
code_fort::body
const codet & body() const
Definition: std_code.h:1068
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
irept::get_sub
subt & get_sub()
Definition: irep.h:477
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:155
code_fort::from_index_bounds
static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)
Produce a code_fort representing:
Definition: std_code.cpp:230
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:259
loc
#define loc()
Definition: ansi_c_lex.yy.cpp:4684
code_blockt::find_last_statement
codet & find_last_statement()
Definition: std_code.cpp:115
exprt::operands
operandst & operands()
Definition: expr.h:95
index_exprt
Array index operator.
Definition: std_expr.h:1299
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2815
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:257
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:298
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
std_expr.h
c_types.h
validation_modet::INVARIANT
@ INVARIANT
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35