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 "std_expr.h"
18 #include "string_constant.h"
19 
23 {
24  const irep_idt &statement=get_statement();
25 
26  if(has_operands())
27  {
28  if(statement==ID_block)
29  return to_code(op0()).first_statement();
30  else if(statement==ID_label)
31  return to_code(op0()).first_statement();
32  }
33 
34  return *this;
35 }
36 
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 
72 {
73  const irep_idt &statement=get_statement();
74 
75  if(has_operands())
76  {
77  if(statement==ID_block)
78  return to_code(operands().back()).last_statement();
79  else if(statement==ID_label)
80  return to_code(operands().back()).last_statement();
81  }
82 
83  return *this;
84 }
85 
88 void code_blockt::append(const code_blockt &extra_block)
89 {
90  statements().reserve(statements().size() + extra_block.statements().size());
91 
92  for(const auto &statement : extra_block.statements())
93  {
94  add(statement);
95  }
96 }
97 
99 {
100  codet *last=this;
101 
102  while(true)
103  {
104  const irep_idt &statement=last->get_statement();
105 
106  if(statement==ID_block &&
107  !to_code_block(*last).statements().empty())
108  {
109  last=&to_code_block(*last).statements().back();
110  }
111  else if(statement==ID_label)
112  {
113  last = &(to_code_label(*last).code());
114  }
115  else
116  break;
117  }
118 
119  return *last;
120 }
121 
123  const exprt &condition, const source_locationt &loc)
124 {
125  code_blockt result({code_assertt(condition), code_assumet(condition)});
126 
127  for(auto &op : result.statements())
128  op.add_source_location() = loc;
129 
130  result.add_source_location() = loc;
131 
132  return result;
133 }
134 
136 {
137  const auto &sub = find(ID_parameters).get_sub();
138  std::vector<irep_idt> result;
139  result.reserve(sub.size());
140  for(const auto &s : sub)
141  result.push_back(s.get(ID_identifier));
142  return result;
143 }
144 
146  const std::vector<irep_idt> &parameter_identifiers)
147 {
148  auto &sub = add(ID_parameters).get_sub();
149  sub.reserve(parameter_identifiers.size());
150  for(const auto &id : parameter_identifiers)
151  {
152  sub.push_back(irept(ID_parameter));
153  sub.back().set(ID_identifier, id);
154  }
155 }
156 
158  std::vector<exprt> arguments,
160  : codet{ID_input, std::move(arguments)}
161 {
162  if(location)
163  add_source_location() = std::move(*location);
164  check(*this, validation_modet::INVARIANT);
165 }
166 
168  const irep_idt &description,
169  exprt expression,
172  string_constantt(description),
173  from_integer(0, index_type()))),
174  std::move(expression)},
175  std::move(location)}
176 {
177 }
178 
179 void code_inputt::check(const codet &code, const validation_modet vm)
180 {
181  DATA_CHECK(
182  vm, code.operands().size() >= 2, "input must have at least two operands");
183 }
184 
186  std::vector<exprt> arguments,
188  : codet{ID_output, std::move(arguments)}
189 {
190  if(location)
191  add_source_location() = std::move(*location);
192  check(*this, validation_modet::INVARIANT);
193 }
194 
196  const irep_idt &description,
197  exprt expression,
200  string_constantt(description),
201  from_integer(0, index_type()))),
202  std::move(expression)},
203  std::move(location)}
204 {
205 }
206 
207 void code_outputt::check(const codet &code, const validation_modet vm)
208 {
209  DATA_CHECK(
210  vm, code.operands().size() >= 2, "output must have at least two operands");
211 }
212 
214  exprt start_index,
215  exprt end_index,
216  symbol_exprt loop_index,
217  codet body,
218  source_locationt location)
219 {
220  PRECONDITION(start_index.type() == loop_index.type());
221  PRECONDITION(end_index.type() == loop_index.type());
223  loop_index,
224  plus_exprt(loop_index, from_integer(1, loop_index.type())),
225  location);
226 
227  return code_fort{
228  code_assignt{loop_index, std::move(start_index)},
229  binary_relation_exprt{loop_index, ID_lt, std::move(end_index)},
230  std::move(inc),
231  std::move(body)};
232 }
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:170
code_function_bodyt::set_parameter_identifiers
void set_parameter_identifiers(const std::vector< irep_idt > &)
Definition: std_code.cpp:145
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:103
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:157
code_fort
codet representation of a for statement.
Definition: std_code.h:1052
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:22
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
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:619
code_outputt::check
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.cpp:207
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:831
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
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:122
irept::irept
irept()=default
code_labelt::code
codet & code()
Definition: std_code.h:1425
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
code_outputt
A codet representing the declaration that an output of a particular description has a value which cor...
Definition: std_code.h:724
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
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:185
code_function_bodyt::get_parameter_identifiers
std::vector< irep_idt > get_parameter_identifiers() const
Definition: std_code.cpp:135
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
code_inputt::check
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.cpp:179
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:567
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1452
pointer_expr.h
API to expression classes for Pointers.
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:55
side_effect_expr_assignt
A side_effect_exprt that performs an assignment.
Definition: std_code.h:2013
validation_modet
validation_modet
Definition: validation_mode.h:13
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
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:677
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:88
code_fort::body
const codet & body() const
Definition: std_code.h:1097
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
irept::get_sub
subt & get_sub()
Definition: irep.h:466
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:213
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
code_blockt::find_last_statement
codet & find_last_statement()
Definition: std_code.cpp:98
exprt::operands
operandst & operands()
Definition: expr.h:96
index_exprt
Array index operator.
Definition: std_expr.h:1243
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
std_expr.h
API to expression classes.
c_types.h
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35