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 "pointer_expr.h"
17 #include "string_constant.h"
18 
22 {
23  const irep_idt &statement=get_statement();
24 
25  if(has_operands())
26  {
27  if(statement==ID_block)
28  return to_code(op0()).first_statement();
29  else if(statement==ID_label)
30  return to_code(op0()).first_statement();
31  }
32 
33  return *this;
34 }
35 
39 {
40  const irep_idt &statement=get_statement();
41 
42  if(has_operands())
43  {
44  if(statement==ID_block)
45  return to_code(op0()).first_statement();
46  else if(statement==ID_label)
47  return to_code(op0()).first_statement();
48  }
49 
50  return *this;
51 }
52 
56 {
57  const irep_idt &statement=get_statement();
58 
59  if(has_operands())
60  {
61  if(statement==ID_block)
62  return to_code(operands().back()).last_statement();
63  else if(statement==ID_label)
64  return to_code(operands().back()).last_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 void code_blockt::append(const code_blockt &extra_block)
90 {
91  statements().reserve(statements().size() + extra_block.statements().size());
92 
93  for(const auto &statement : extra_block.statements())
94  {
95  add(statement);
96  }
97 }
98 
100 {
101  codet *last=this;
102 
103  while(true)
104  {
105  const irep_idt &statement=last->get_statement();
106 
107  if(statement==ID_block &&
108  !to_code_block(*last).statements().empty())
109  {
110  last=&to_code_block(*last).statements().back();
111  }
112  else if(statement==ID_label)
113  {
114  last = &(to_code_label(*last).code());
115  }
116  else
117  break;
118  }
119 
120  return *last;
121 }
122 
124  const exprt &condition, const source_locationt &loc)
125 {
126  code_blockt result({code_assertt(condition), code_assumet(condition)});
127 
128  for(auto &op : result.statements())
129  op.add_source_location() = loc;
130 
131  result.add_source_location() = loc;
132 
133  return result;
134 }
135 
137 {
138  const auto &sub = find(ID_parameters).get_sub();
139  std::vector<irep_idt> result;
140  result.reserve(sub.size());
141  for(const auto &s : sub)
142  result.push_back(s.get(ID_identifier));
143  return result;
144 }
145 
147  const std::vector<irep_idt> &parameter_identifiers)
148 {
149  auto &sub = add(ID_parameters).get_sub();
150  sub.reserve(parameter_identifiers.size());
151  for(const auto &id : parameter_identifiers)
152  {
153  sub.push_back(irept(ID_parameter));
154  sub.back().set(ID_identifier, id);
155  }
156 }
157 
159  std::vector<exprt> arguments,
161  : codet{ID_input, std::move(arguments)}
162 {
163  if(location)
164  add_source_location() = std::move(*location);
166 }
167 
169  const irep_idt &description,
170  exprt expression,
173  string_constantt(description),
174  from_integer(0, index_type()))),
175  std::move(expression)},
176  std::move(location)}
177 {
178 }
179 
180 void code_inputt::check(const codet &code, const validation_modet vm)
181 {
182  DATA_CHECK(
183  vm, code.operands().size() >= 2, "input must have at least two operands");
184 }
185 
187  std::vector<exprt> arguments,
189  : codet{ID_output, std::move(arguments)}
190 {
191  if(location)
192  add_source_location() = std::move(*location);
194 }
195 
197  const irep_idt &description,
198  exprt expression,
201  string_constantt(description),
202  from_integer(0, index_type()))),
203  std::move(expression)},
204  std::move(location)}
205 {
206 }
207 
208 void code_outputt::check(const codet &code, const validation_modet vm)
209 {
210  DATA_CHECK(
211  vm, code.operands().size() >= 2, "output must have at least two operands");
212 }
213 
215  exprt start_index,
216  exprt end_index,
217  symbol_exprt loop_index,
218  codet body,
219  source_locationt location)
220 {
221  PRECONDITION(start_index.type() == loop_index.type());
222  PRECONDITION(end_index.type() == loop_index.type());
224  loop_index,
225  plus_exprt(loop_index, from_integer(1, loop_index.type())),
226  location);
227 
228  return code_fort{
229  code_assignt{loop_index, std::move(start_index)},
230  binary_relation_exprt{loop_index, ID_lt, std::move(end_index)},
231  std::move(inc),
232  std::move(body)};
233 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: pointer_expr.h:341
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:617
A codet representing an assignment in the program.
Definition: std_code.h:293
An assumption, which must hold in subsequent code.
Definition: std_code.h:565
A codet representing sequential composition of program statements.
Definition: std_code.h:168
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:89
void add(const codet &code)
Definition: std_code.h:206
code_operandst & statements()
Definition: std_code.h:176
codet & find_last_statement()
Definition: std_code.cpp:99
codet representation of a for statement.
Definition: std_code.h:1050
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:214
const codet & body() const
Definition: std_code.h:1095
std::vector< irep_idt > get_parameter_identifiers() const
Definition: std_code.cpp:136
void set_parameter_identifiers(const std::vector< irep_idt > &)
Definition: std_code.cpp:146
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:675
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:158
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.cpp:180
codet & code()
Definition: std_code.h:1423
A codet representing the declaration that an output of a particular description has a value which cor...
Definition: std_code.h:722
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.cpp:208
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:186
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them.
Definition: std_code.cpp:21
exprt & op0()
Definition: expr.h:99
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them.
Definition: std_code.cpp:55
const irep_idt & get_statement() const
Definition: std_code.h:69
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
source_locationt & add_source_location()
Definition: expr.h:235
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Array index operator.
Definition: std_expr.h:1328
irept()=default
subt & get_sub()
Definition: irep.h:467
irept & add(const irep_namet &name)
Definition: irep.cpp:116
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
The plus expression Associativity is not specified.
Definition: std_expr.h:914
A side_effect_exprt that performs an assignment.
Definition: std_code.h:2011
Expression to hold a symbol (variable)
Definition: std_expr.h:80
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:123
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1450
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:254
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet