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 
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 
38 {
39  const irep_idt &statement=get_statement();
40 
41  if(has_operands())
42  {
43  if(statement==ID_block)
44  return to_code(op0()).first_statement();
45  else if(statement==ID_label)
46  return to_code(op0()).first_statement();
47  }
48 
49  return *this;
50 }
51 
55 {
56  const irep_idt &statement=get_statement();
57 
58  if(has_operands())
59  {
60  if(statement==ID_block)
61  return to_code(operands().back()).last_statement();
62  else if(statement==ID_label)
63  return to_code(operands().back()).last_statement();
64  }
65 
66  return *this;
67 }
68 
71 {
72  const irep_idt &statement=get_statement();
73 
74  if(has_operands())
75  {
76  if(statement==ID_block)
77  return to_code(operands().back()).last_statement();
78  else if(statement==ID_label)
79  return to_code(operands().back()).last_statement();
80  }
81 
82  return *this;
83 }
84 
87 void code_blockt::append(const code_blockt &extra_block)
88 {
89  statements().reserve(statements().size() + extra_block.statements().size());
90 
91  for(const auto &statement : extra_block.statements())
92  {
93  add(statement);
94  }
95 }
96 
98 {
99  codet *last=this;
100 
101  while(true)
102  {
103  const irep_idt &statement=last->get_statement();
104 
105  if(statement==ID_block &&
106  !to_code_block(*last).statements().empty())
107  {
108  last=&to_code_block(*last).statements().back();
109  }
110  else if(statement==ID_label)
111  {
112  last = &(to_code_label(*last).code());
113  }
114  else
115  break;
116  }
117 
118  return *last;
119 }
120 
122  const exprt &condition, const source_locationt &loc)
123 {
124  code_blockt result({code_assertt(condition), code_assumet(condition)});
125 
126  for(auto &op : result.statements())
127  op.add_source_location() = loc;
128 
129  result.add_source_location() = loc;
130 
131  return result;
132 }
133 
135 {
136  const auto &sub = find(ID_parameters).get_sub();
137  std::vector<irep_idt> result;
138  result.reserve(sub.size());
139  for(const auto &s : sub)
140  result.push_back(s.get(ID_identifier));
141  return result;
142 }
143 
145  const std::vector<irep_idt> &parameter_identifiers)
146 {
147  auto &sub = add(ID_parameters).get_sub();
148  sub.reserve(parameter_identifiers.size());
149  for(const auto &id : parameter_identifiers)
150  {
151  sub.push_back(irept(ID_parameter));
152  sub.back().set(ID_identifier, id);
153  }
154 }
155 
157  std::vector<exprt> arguments,
159  : codet{ID_input, std::move(arguments)}
160 {
161  if(location)
162  add_source_location() = std::move(*location);
163  check(*this, validation_modet::INVARIANT);
164 }
165 
167  const irep_idt &description,
168  exprt expression,
171  string_constantt(description),
172  from_integer(0, index_type()))),
173  std::move(expression)},
174  std::move(location)}
175 {
176 }
177 
178 void code_inputt::check(const codet &code, const validation_modet vm)
179 {
180  DATA_CHECK(
181  vm, code.operands().size() >= 2, "input must have at least two operands");
182 }
183 
185  std::vector<exprt> arguments,
187  : codet{ID_output, std::move(arguments)}
188 {
189  if(location)
190  add_source_location() = std::move(*location);
191  check(*this, validation_modet::INVARIANT);
192 }
193 
195  const irep_idt &description,
196  exprt expression,
199  string_constantt(description),
200  from_integer(0, index_type()))),
201  std::move(expression)},
202  std::move(location)}
203 {
204 }
205 
206 void code_outputt::check(const codet &code, const validation_modet vm)
207 {
208  DATA_CHECK(
209  vm, code.operands().size() >= 2, "output must have at least two operands");
210 }
211 
213  exprt start_index,
214  exprt end_index,
215  symbol_exprt loop_index,
216  codet body,
217  source_locationt location)
218 {
219  PRECONDITION(start_index.type() == loop_index.type());
220  PRECONDITION(end_index.type() == loop_index.type());
222  loop_index,
223  plus_exprt(loop_index, from_integer(1, loop_index.type())),
224  location);
225 
226  return code_fort{
227  code_assignt{loop_index, std::move(start_index)},
228  binary_relation_exprt{loop_index, ID_lt, std::move(end_index)},
229  std::move(inc),
230  std::move(body)};
231 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:169
code_function_bodyt::set_parameter_identifiers
void set_parameter_identifiers(const std::vector< irep_idt > &)
Definition: std_code.cpp:144
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
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:156
code_fort
codet representation of a for statement.
Definition: std_code.h:1019
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:21
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:586
code_outputt::check
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.cpp:206
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:880
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:52
exprt::op0
exprt & op0()
Definition: expr.h:102
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
string_constantt
Definition: string_constant.h:15
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:121
irept::irept
irept()=default
code_labelt::code
codet & code()
Definition: std_code.h:1393
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:691
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:184
code_function_bodyt::get_parameter_identifiers
std::vector< irep_idt > get_parameter_identifiers() const
Definition: std_code.cpp:134
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:178
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:534
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1420
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:54
side_effect_expr_assignt
A side_effect_exprt that performs an assignment.
Definition: std_code.h:1989
validation_modet
validation_modet
Definition: validation_mode.h:12
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:19
code_inputt
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:644
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:87
code_fort::body
const codet & body() const
Definition: std_code.h:1065
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:724
irept::get_sub
subt & get_sub()
Definition: irep.h:477
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:212
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:97
exprt::operands
operandst & operands()
Definition: expr.h:95
index_exprt
Array index operator.
Definition: std_expr.h:1292
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2785
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:294
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
std_expr.h
c_types.h
validation_modet::INVARIANT
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34