From b199026bdc781715d2c9f5fd3c0b587541c26f9d Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Jun 2019 16:19:19 +0100 Subject: [PATCH 1/5] Add zip method on ranget Allow to construct a range of pairs from a pair of ranges --- src/util/range.h | 96 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 96 insertions(+) diff --git a/src/util/range.h b/src/util/range.h index 3fa288c2b4..3d4ec7e005 100644 --- a/src/util/range.h +++ b/src/util/range.h @@ -265,6 +265,90 @@ private: second_iteratort second_begin; }; +/// Zip two ranges to make a range of pairs. +/// On increment, both iterators are incremented. +/// Ends when the two ranges reach their ends. +/// Invariants are checking that one does not end before the other. +template +struct zip_iteratort +{ +public: + using difference_type = typename first_iteratort::difference_type; + using value_type = std::pair< + typename first_iteratort::value_type, + typename second_iteratort::value_type>; + using pointer = value_type *; + using reference = value_type &; + using iterator_category = std::forward_iterator_tag; + + bool operator==(const zip_iteratort &other) const + { + return first_begin == other.first_begin && first_end == other.first_end && + second_begin == other.second_begin && second_end == other.second_end; + } + + bool operator!=(const zip_iteratort &other) const + { + return !(*this == other); + } + + /// Preincrement operator + zip_iteratort &operator++() + { + PRECONDITION(first_begin != first_end && second_begin != second_end); + ++first_begin; + ++second_begin; + INVARIANT( + (first_begin == first_end) == (second_begin == second_end), + "Zipped ranges should have the same size"); + current = first_begin != first_end + ? std::make_shared(*first_begin, *second_begin) + : nullptr; + return *this; + } + + /// Postincrement operator + const zip_iteratort operator++(int) + { + zip_iteratort tmp(first_begin, first_end, second_begin, second_end); + this->operator++(); + return tmp; + } + + reference operator*() const + { + PRECONDITION(current != nullptr); + return *current; + } + + pointer operator->() const + { + return current.get(); + } + + zip_iteratort( + first_iteratort _first_begin, + first_iteratort _first_end, + second_iteratort _second_begin, + second_iteratort _second_end) + : first_begin(std::move(_first_begin)), + first_end(std::move(_first_end)), + second_begin(std::move(_second_begin)), + second_end(std::move(_second_end)) + { + PRECONDITION((first_begin == first_end) == (second_begin == second_end)); + if(first_begin != first_end) + current = util_make_unique(*first_begin, *second_begin); + } + +private: + first_iteratort first_begin; + first_iteratort first_end; + second_iteratort second_begin; + second_iteratort second_end; + std::shared_ptr current = nullptr; +}; + /// A range is a pair of a begin and an end iterators. /// The class provides useful methods such as map, filter and concat which only /// manipulate iterators and thus don't have to create instances of heavy data @@ -337,6 +421,18 @@ public: concat_begin, concat_end); } + template + ranget> + zip(ranget other) + { + auto zip_begin = zip_iteratort( + begin(), end(), other.begin(), other.end()); + auto zip_end = zip_iteratort( + end(), end(), other.end(), other.end()); + return ranget>( + zip_begin, zip_end); + } + bool empty() const { return begin_value == end_value; From 47ec2690eb434f93ab59d5c135576d6def21223f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 14 Jun 2019 11:55:55 +0100 Subject: [PATCH 2/5] Overload of zip with container argument --- src/util/range.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/util/range.h b/src/util/range.h index 3d4ec7e005..10bb3f7d2f 100644 --- a/src/util/range.h +++ b/src/util/range.h @@ -433,6 +433,14 @@ public: zip_begin, zip_end); } + template + auto zip(containert &container) + -> ranget> + { + return zip( + ranget{container.begin(), container.end()}); + } + bool empty() const { return begin_value == end_value; From 0c0d997b2e9b977af6f34a02d92f8c8839c24473 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Jun 2019 16:21:12 +0100 Subject: [PATCH 3/5] Use zip to get rid of index in loop Using zip in a range-for loop makes it clearer that we iterate over both components and rhs operands, rather than having to look at how index `i` is used to tie the two together. --- src/goto-symex/symex_assign.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 2be9a9262c..3f84eda423 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -399,21 +399,20 @@ void goto_symext::symex_assign_from_struct( const struct_union_typet::componentst &components = type.components(); PRECONDITION(rhs.operands().size() == components.size()); - for(std::size_t i = 0; i < components.size(); ++i) + for(const auto &comp_rhs : make_range(components).zip(rhs.operands())) { - const auto &comp = components[i]; + const auto &comp = comp_rhs.first; const exprt lhs_field = state.field_sensitivity.apply( ns, state, member_exprt{lhs, comp.get_name(), comp.type()}, true); INVARIANT( lhs_field.id() == ID_symbol, "member of symbol should be susceptible to field-sensitivity"); - const exprt &rhs_field = rhs.operands()[i]; symex_assign_symbol( state, to_ssa_expr(lhs_field), full_lhs, - rhs_field, + comp_rhs.second, guard, assignment_type); } From 130a539cc800d472df70df4bcb3076380bd70373 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 14 Jun 2019 09:54:04 +0100 Subject: [PATCH 4/5] Add unit tests for ranget::zip This tests that the zip method behaves as expected on a vector of int and a list of strings zipped together. --- unit/util/range.cpp | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/unit/util/range.cpp b/unit/util/range.cpp index 7b0d8bc292..e4b3272639 100644 --- a/unit/util/range.cpp +++ b/unit/util/range.cpp @@ -6,6 +6,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com \*******************************************************************/ +#include #include #include @@ -188,6 +189,34 @@ SCENARIO("range tests", "[core][util][range]") REQUIRE(input2 == expected_result2); } } + GIVEN("A vectors of int and a list of strings.") + { + std::vector int_vector{1, 2}; + std::list string_list{"foo", "bar"}; + WHEN("We zip the vector and the list") + { + auto range = make_range(int_vector).zip(string_list); + REQUIRE(!range.empty()); + THEN("First pair is (1, foo)") + { + const std::pair first_pair = *range.begin(); + REQUIRE(first_pair.first == 1); + REQUIRE(first_pair.second == "foo"); + } + range = std::move(range).drop(1); + THEN("Second pair is (2, bar)") + { + const std::pair second_pair = *range.begin(); + REQUIRE(second_pair.first == 2); + REQUIRE(second_pair.second == "bar"); + } + range = std::move(range).drop(1); + THEN("Range is empty") + { + REQUIRE(range.empty()); + } + } + } } class move_onlyt From 1011350503f94cd3a0b45f9f95203dfaf05fa449 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 14 Jun 2019 11:58:38 +0100 Subject: [PATCH 5/5] Add zip unit test with constant vector --- unit/util/range.cpp | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/unit/util/range.cpp b/unit/util/range.cpp index e4b3272639..6470caceff 100644 --- a/unit/util/range.cpp +++ b/unit/util/range.cpp @@ -217,6 +217,34 @@ SCENARIO("range tests", "[core][util][range]") } } } + GIVEN("A constant vectors of int and a list of strings.") + { + const std::vector int_vector{41, 27}; + const std::list string_list{"boo", "far"}; + WHEN("We zip the vector and the list") + { + auto range = make_range(int_vector).zip(string_list); + REQUIRE(!range.empty()); + THEN("First pair is (1, foo)") + { + const std::pair first_pair = *range.begin(); + REQUIRE(first_pair.first == 41); + REQUIRE(first_pair.second == "boo"); + } + range = std::move(range).drop(1); + THEN("Second pair is (2, bar)") + { + const std::pair second_pair = *range.begin(); + REQUIRE(second_pair.first == 27); + REQUIRE(second_pair.second == "far"); + } + range = std::move(range).drop(1); + THEN("Range is empty") + { + REQUIRE(range.empty()); + } + } + } } class move_onlyt