CBMC: /home/runner/work/cbmc/cbmc/src/util/expr

CBMC: /home/runner/work/cbmc/cbmc/src/util/expr_iterator.h Source File

9#ifndef CPROVER_UTIL_EXPR_ITERATOR_H

10#define CPROVER_UTIL_EXPR_ITERATOR_H

12#include <deque>

13#include <iterator>

14#include <functional>

15#include <set>

16#include <algorithm>

45{

50 std::reference_wrapper<const exprt> expr;

52};

67template<typename depth_iterator_t>

69{

70public:

77 template <typename other_depth_iterator_t>

80 template <typename other_depth_iterator_t>

83 {

84 return m_stack==other.m_stack;

85 }

87 template <typename other_depth_iterator_t>

90 {

91 return !(*this == other);

92 }

97 {

99 while(true)

100 {

101 if(m_stack.back().op_idx == m_stack.back().expr.get().operands().size())

102 {

105 break;

106 }

107

109 m_stack.back().expr.get().operands()[m_stack.back().op_idx]))

110 {

111 break;

112 }

114 }

116 }

117

119 {

123 {

125 return ++(*this);

126 }

128 }

129

133 {

136 return tmp;

137 }

138

142 {

144 return m_stack.back().expr.get();

145 }

146

151

152protected:

155

159

163

166 { m_stack=std::move(other.m_stack); }

169 {

170 m_stack = std::move(other.m_stack);

171 return *this;

172 }

173

175 {

176 return m_stack.front().expr.get();

177 }

178

185 {

187

189 for(auto &state : m_stack)

190 {

191

193 state.expr = *expr;

194

195 if(!(state == m_stack.back()))

196 expr = &expr->operands()[state.op_idx];

197 }

198 return *expr;

199 }

200

207 {

208 m_stack.emplace_back(expr);

209 return true;

210 }

211

212private:

213 std::deque<depth_iterator_expr_statet> m_stack;

214

217};

218

229

232{

233private:

237

238public:

241

248

257 const exprt &expr,

260 {

261

262

264 }

265

273 {

275 {

279 "mutate_root must return the same root node that depth_iteratort was "

280 "constructed with");

282 }

284 }

285};

286

289{

291public:

298private:

300 bool push_expr(const exprt &expr)

301 {

302 const bool inserted=this->m_traversed.insert(expr).second;

303 if(inserted)

305 return inserted;

306 }

308};

309

313{

314public:

318

320 {

321 return root.depth_cbegin();

322 }

323

325 {

326 return root.depth_cend();

327 }

328

329protected:

331};

332

338

343{

344public:

350

357

360

365

367 {

368 return !(*this == other);

369 }

370

374 {

376

377

379

381 return *this;

382

383

385

386

387 if(m_stack.back().op_idx < m_stack.back().expr.get().operands().size())

388 {

390 m_stack.back().expr.get().operands()[m_stack.back().op_idx]);

391 }

392

393

394 return *this;

395 }

396

400 {

402 ++(*this);

403 return tmp;

404 }

405

409 {

411 return m_stack.back().expr.get();

412 }

413

417 {

418 return &**this;

419 }

420

421private:

425 {

426 const exprt *current = &expr;

427 while(true)

428 {

429 m_stack.emplace_back(*current);

430 if(current->operands().empty())

431 break;

432 current = &current->operands().front();

433 }

434 }

435

436 std::deque<depth_iterator_expr_statet> m_stack;

437};

438

441{

442public:

447

452

457

458protected:

460};

461

467

468#endif

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

An adapter to yield a range (expected to satisfy C++20 std::ranges::range) of const_depth_iteratort.

const_depth_iteratort begin() const

const_depth_iteratort end() const

const_depth_iterator_range_adaptert(const exprt &_root)

const_depth_iteratort(const exprt &expr)

Create iterator starting at the supplied node (root)

const_depth_iteratort()=default

Create an end iterator.

An adapter to yield a range of const_post_depth_iteratort.

const_post_depth_iteratort end() const

const_post_depth_iterator_range_adaptert(const exprt &_root)

const_post_depth_iteratort begin() const

Post-order depth-first-search iterator.

bool operator!=(const const_post_depth_iteratort &other) const

void descend_to_leftmost_leaf(const exprt &expr)

Descend from the given expression to its leftmost leaf, pushing all nodes along the path onto the sta...

const exprt & operator*() const

Dereference operator Dereferencing end() iterator is undefined behaviour.

const_post_depth_iteratort & operator++()

Preincrement operator Do not call on the end() iterator.

const_post_depth_iteratort operator++(int)

Post-increment operator Expensive copy.

std::deque< depth_iterator_expr_statet > m_stack

const_post_depth_iteratort(const exprt &expr)

Create iterator starting at the supplied node (root).

const_post_depth_iteratort()=default

Create an end iterator.

const exprt * operator->() const

Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.

bool operator==(const const_post_depth_iteratort &other) const

std::forward_iterator_tag iterator_category

friend depth_iterator_baset

const_unique_depth_iteratort()=default

Create an end iterator.

bool push_expr(const exprt &expr)

Push expression onto the stack and add to the set of traversed exprts.

std::set< exprt > m_traversed

const_unique_depth_iteratort(const exprt &expr)

Create iterator starting at the supplied node (root)

Depth first search iterator base - iterates over supplied expression and all its operands recursively...

depth_iterator_t & next_sibling_or_parent()

depth_iterator_t & operator++()

Preincrement operator Do not call on the end() iterator.

depth_iterator_baset(const depth_iterator_baset &)=default

exprt & mutate()

Obtain non-const exprt reference.

std::deque< depth_iterator_expr_statet > m_stack

depth_iterator_baset & operator=(const depth_iterator_baset &)=default

const exprt * operator->() const

Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.

depth_iterator_baset(const exprt &root)

Create begin iterator, starting at the supplied node.

const exprt & operator*() const

Dereference operator Dereferencing end() iterator is undefined behaviour.

depth_iterator_baset(depth_iterator_baset &&other)

bool operator!=(const depth_iterator_baset< other_depth_iterator_t > &other) const

bool push_expr(const exprt &expr)

Pushes expression onto the stack If overridden, this function should be called from the inheriting cl...

bool operator==(const depth_iterator_baset< other_depth_iterator_t > &other) const

depth_iterator_t operator++(int)

Post-increment operator Expensive copy.

std::forward_iterator_tag iterator_category

depth_iterator_t & downcast()

depth_iterator_baset & operator=(depth_iterator_baset &&other)

~depth_iterator_baset()=default

Destructor Protected to discourage upcasting.

depth_iterator_baset()=default

Create end iterator.

depth_iteratort(const exprt &expr, std::function< exprt &()> mutate_root)

Create iterator starting at the supplied node (root) If mutations of the child nodes are required the...

depth_iteratort(exprt &expr)

Create iterator starting at the supplied node (root) All mutations of the child nodes will be reflect...

exprt & mutate()

Obtain non-const reference to the exprt instance currently pointed to by the iterator.

depth_iteratort()=default

Create an end iterator.

std::function< exprt &()> mutate_root

If this is non-empty then the root is currently const and this function must be called before any mut...

Base class for all expressions.

static const_depth_iterator_range_adaptert pre_traversal(const exprt &root)

bool operator==(const depth_iterator_expr_statet &left, const depth_iterator_expr_statet &right)

static const_post_depth_iterator_range_adaptert post_traversal(const exprt &root)

int __CPROVER_ID java::java io InputStream read

#define PRECONDITION(CONDITION)

#define INVARIANT(CONDITION, REASON)

This macro uses the wrapper function 'invariant_violated_string'.

Helper class for depth_iterator_baset.

std::reference_wrapper< const exprt > expr

depth_iterator_expr_statet(const exprt &expr)

exprt::operandst::const_iterator operands_iteratort