Skip to content

Commit 1ea4a76

Browse files
Merge pull request #4791 from romainbrenguier/feature/range-zip
Add ranget::zip method
2 parents 5bd95a7 + 1011350 commit 1ea4a76

File tree

3 files changed

+164
-4
lines changed

3 files changed

+164
-4
lines changed

Diff for: src/goto-symex/symex_assign.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -398,21 +398,20 @@ void goto_symext::symex_assign_from_struct(
398398
const auto &components = to_struct_type(ns.follow(lhs.type())).components();
399399
PRECONDITION(rhs.operands().size() == components.size());
400400

401-
for(std::size_t i = 0; i < components.size(); ++i)
401+
for(const auto &comp_rhs : make_range(components).zip(rhs.operands()))
402402
{
403-
const auto &comp = components[i];
403+
const auto &comp = comp_rhs.first;
404404
const exprt lhs_field = state.field_sensitivity.apply(
405405
ns, state, member_exprt{lhs, comp.get_name(), comp.type()}, true);
406406
INVARIANT(
407407
lhs_field.id() == ID_symbol,
408408
"member of symbol should be susceptible to field-sensitivity");
409409

410-
const exprt &rhs_field = rhs.operands()[i];
411410
symex_assign_symbol(
412411
state,
413412
to_ssa_expr(lhs_field),
414413
full_lhs,
415-
rhs_field,
414+
comp_rhs.second,
416415
guard,
417416
assignment_type);
418417
}

Diff for: src/util/range.h

+104
Original file line numberDiff line numberDiff line change
@@ -265,6 +265,90 @@ struct concat_iteratort
265265
second_iteratort second_begin;
266266
};
267267

268+
/// Zip two ranges to make a range of pairs.
269+
/// On increment, both iterators are incremented.
270+
/// Ends when the two ranges reach their ends.
271+
/// Invariants are checking that one does not end before the other.
272+
template <typename first_iteratort, typename second_iteratort>
273+
struct zip_iteratort
274+
{
275+
public:
276+
using difference_type = typename first_iteratort::difference_type;
277+
using value_type = std::pair<
278+
typename first_iteratort::value_type,
279+
typename second_iteratort::value_type>;
280+
using pointer = value_type *;
281+
using reference = value_type &;
282+
using iterator_category = std::forward_iterator_tag;
283+
284+
bool operator==(const zip_iteratort &other) const
285+
{
286+
return first_begin == other.first_begin && first_end == other.first_end &&
287+
second_begin == other.second_begin && second_end == other.second_end;
288+
}
289+
290+
bool operator!=(const zip_iteratort &other) const
291+
{
292+
return !(*this == other);
293+
}
294+
295+
/// Preincrement operator
296+
zip_iteratort &operator++()
297+
{
298+
PRECONDITION(first_begin != first_end && second_begin != second_end);
299+
++first_begin;
300+
++second_begin;
301+
INVARIANT(
302+
(first_begin == first_end) == (second_begin == second_end),
303+
"Zipped ranges should have the same size");
304+
current = first_begin != first_end
305+
? std::make_shared<value_type>(*first_begin, *second_begin)
306+
: nullptr;
307+
return *this;
308+
}
309+
310+
/// Postincrement operator
311+
const zip_iteratort operator++(int)
312+
{
313+
zip_iteratort tmp(first_begin, first_end, second_begin, second_end);
314+
this->operator++();
315+
return tmp;
316+
}
317+
318+
reference operator*() const
319+
{
320+
PRECONDITION(current != nullptr);
321+
return *current;
322+
}
323+
324+
pointer operator->() const
325+
{
326+
return current.get();
327+
}
328+
329+
zip_iteratort(
330+
first_iteratort _first_begin,
331+
first_iteratort _first_end,
332+
second_iteratort _second_begin,
333+
second_iteratort _second_end)
334+
: first_begin(std::move(_first_begin)),
335+
first_end(std::move(_first_end)),
336+
second_begin(std::move(_second_begin)),
337+
second_end(std::move(_second_end))
338+
{
339+
PRECONDITION((first_begin == first_end) == (second_begin == second_end));
340+
if(first_begin != first_end)
341+
current = util_make_unique<value_type>(*first_begin, *second_begin);
342+
}
343+
344+
private:
345+
first_iteratort first_begin;
346+
first_iteratort first_end;
347+
second_iteratort second_begin;
348+
second_iteratort second_end;
349+
std::shared_ptr<value_type> current = nullptr;
350+
};
351+
268352
/// A range is a pair of a begin and an end iterators.
269353
/// The class provides useful methods such as map, filter and concat which only
270354
/// manipulate iterators and thus don't have to create instances of heavy data
@@ -337,6 +421,26 @@ struct ranget final
337421
concat_begin, concat_end);
338422
}
339423

424+
template <typename other_iteratort>
425+
ranget<zip_iteratort<iteratort, other_iteratort>>
426+
zip(ranget<other_iteratort> other)
427+
{
428+
auto zip_begin = zip_iteratort<iteratort, other_iteratort>(
429+
begin(), end(), other.begin(), other.end());
430+
auto zip_end = zip_iteratort<iteratort, other_iteratort>(
431+
end(), end(), other.end(), other.end());
432+
return ranget<zip_iteratort<iteratort, other_iteratort>>(
433+
zip_begin, zip_end);
434+
}
435+
436+
template <typename containert>
437+
auto zip(containert &container)
438+
-> ranget<zip_iteratort<iteratort, decltype(container.begin())>>
439+
{
440+
return zip(
441+
ranget<decltype(container.begin())>{container.begin(), container.end()});
442+
}
443+
340444
bool empty() const
341445
{
342446
return begin_value == end_value;

Diff for: unit/util/range.cpp

+57
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Author: Romain Brenguier, [email protected]
66
77
\*******************************************************************/
88

9+
#include <list>
910
#include <vector>
1011

1112
#include <testing-utils/use_catch.h>
@@ -188,6 +189,62 @@ SCENARIO("range tests", "[core][util][range]")
188189
REQUIRE(input2 == expected_result2);
189190
}
190191
}
192+
GIVEN("A vectors of int and a list of strings.")
193+
{
194+
std::vector<int> int_vector{1, 2};
195+
std::list<std::string> string_list{"foo", "bar"};
196+
WHEN("We zip the vector and the list")
197+
{
198+
auto range = make_range(int_vector).zip(string_list);
199+
REQUIRE(!range.empty());
200+
THEN("First pair is (1, foo)")
201+
{
202+
const std::pair<int, std::string> first_pair = *range.begin();
203+
REQUIRE(first_pair.first == 1);
204+
REQUIRE(first_pair.second == "foo");
205+
}
206+
range = std::move(range).drop(1);
207+
THEN("Second pair is (2, bar)")
208+
{
209+
const std::pair<int, std::string> second_pair = *range.begin();
210+
REQUIRE(second_pair.first == 2);
211+
REQUIRE(second_pair.second == "bar");
212+
}
213+
range = std::move(range).drop(1);
214+
THEN("Range is empty")
215+
{
216+
REQUIRE(range.empty());
217+
}
218+
}
219+
}
220+
GIVEN("A constant vectors of int and a list of strings.")
221+
{
222+
const std::vector<int> int_vector{41, 27};
223+
const std::list<std::string> string_list{"boo", "far"};
224+
WHEN("We zip the vector and the list")
225+
{
226+
auto range = make_range(int_vector).zip(string_list);
227+
REQUIRE(!range.empty());
228+
THEN("First pair is (1, foo)")
229+
{
230+
const std::pair<int, std::string> first_pair = *range.begin();
231+
REQUIRE(first_pair.first == 41);
232+
REQUIRE(first_pair.second == "boo");
233+
}
234+
range = std::move(range).drop(1);
235+
THEN("Second pair is (2, bar)")
236+
{
237+
const std::pair<int, std::string> second_pair = *range.begin();
238+
REQUIRE(second_pair.first == 27);
239+
REQUIRE(second_pair.second == "far");
240+
}
241+
range = std::move(range).drop(1);
242+
THEN("Range is empty")
243+
{
244+
REQUIRE(range.empty());
245+
}
246+
}
247+
}
191248
}
192249

193250
class move_onlyt

0 commit comments

Comments
 (0)