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 
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 
57 {
58  const irep_idt &statement=get_statement();
59 
60  if(has_operands())
61  {
62  if(statement==ID_block)
63  return to_code(operands().back()).last_statement();
64  else if(statement==ID_label)
65  return to_code(operands().back()).last_statement();
66  }
67 
68  return *this;
69 }
70 
74 {
75  const irep_idt &statement=get_statement();
76 
77  if(has_operands())
78  {
79  if(statement==ID_block)
80  return to_code(operands().back()).last_statement();
81  else if(statement==ID_label)
82  return to_code(operands().back()).last_statement();
83  }
84 
85  return *this;
86 }
87 
90 void code_blockt::append(const code_blockt &extra_block)
91 {
92  statements().reserve(statements().size() + extra_block.statements().size());
93 
94  for(const auto &statement : extra_block.statements())
95  {
96  add(statement);
97  }
98 }
99 
101 {
102  codet *last=this;
103 
104  while(true)
105  {
106  const irep_idt &statement=last->get_statement();
107 
108  if(statement==ID_block &&
109  !to_code_block(*last).statements().empty())
110  {
111  last=&to_code_block(*last).statements().back();
112  }
113  else if(statement==ID_label)
114  {
115  last = &(to_code_label(*last).code());
116  }
117  else
118  break;
119  }
120 
121  return *last;
122 }
123 
125  const exprt &condition, const source_locationt &loc)
126 {
127  code_blockt result({code_assertt(condition), code_assumet(condition)});
128 
129  for(auto &op : result.statements())
130  op.add_source_location() = loc;
131 
132  result.add_source_location() = loc;
133 
134  return result;
135 }
136 
138 {
139  const auto &sub = find(ID_parameters).get_sub();
140  std::vector<irep_idt> result;
141  result.reserve(sub.size());
142  for(const auto &s : sub)
143  result.push_back(s.get(ID_identifier));
144  return result;
145 }
146 
148  const std::vector<irep_idt> &parameter_identifiers)
149 {
150  auto &sub = add(ID_parameters).get_sub();
151  sub.reserve(parameter_identifiers.size());
152  for(const auto &id : parameter_identifiers)
153  {
154  sub.push_back(irept(ID_parameter));
155  sub.back().set(ID_identifier, id);
156  }
157 }
158 
160  std::vector<exprt> arguments,
162  : codet{ID_input, std::move(arguments)}
163 {
164  if(location)
165  add_source_location() = std::move(*location);
166  check(*this, validation_modet::INVARIANT);
167 }
168 
170  const irep_idt &description,
171  exprt expression,
174  string_constantt(description),
175  from_integer(0, index_type()))),
176  std::move(expression)},
177  std::move(location)}
178 {
179 }
180 
181 void code_inputt::check(const codet &code, const validation_modet vm)
182 {
183  DATA_CHECK(
184  vm, code.operands().size() >= 2, "input must have at least two operands");
185 }
186 
188  std::vector<exprt> arguments,
190  : codet{ID_output, std::move(arguments)}
191 {
192  if(location)
193  add_source_location() = std::move(*location);
194  check(*this, validation_modet::INVARIANT);
195 }
196 
198  const irep_idt &description,
199  exprt expression,
202  string_constantt(description),
203  from_integer(0, index_type()))),
204  std::move(expression)},
205  std::move(location)}
206 {
207 }
208 
209 void code_outputt::check(const codet &code, const validation_modet vm)
210 {
211  DATA_CHECK(
212  vm, code.operands().size() >= 2, "output must have at least two operands");
213 }
214 
216  exprt start_index,
217  exprt end_index,
218  symbol_exprt loop_index,
219  codet body,
220  source_locationt location)
221 {
222  PRECONDITION(start_index.type() == loop_index.type());
223  PRECONDITION(end_index.type() == loop_index.type());
225  loop_index,
226  plus_exprt(loop_index, from_integer(1, loop_index.type())),
227  location);
228 
229  return code_fort{
230  code_assignt{loop_index, std::move(start_index)},
231  binary_relation_exprt{loop_index, ID_lt, std::move(end_index)},
232  std::move(inc),
233  std::move(body)};
234 }
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:147
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:159
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
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:122
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
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:209
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
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:80
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:124
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:187
code_function_bodyt::get_parameter_identifiers
std::vector< irep_idt > get_parameter_identifiers() const
Definition: std_code.cpp:137
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:181
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:56
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:100
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:90
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:674
irept::get_sub
subt & get_sub()
Definition: irep.h:467
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:215
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:100
exprt::operands
operandst & operands()
Definition: expr.h:96
index_exprt
Array index operator.
Definition: std_expr.h:1242
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
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:243
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