From 67e68bd0e1b68d8ce1b6cde807189ceb4215a013 Mon Sep 17 00:00:00 2001 From: caballa Date: Wed, 2 Mar 2022 15:02:01 -0700 Subject: [PATCH 1/6] refactor(patricia): removed redundant code --- include/crab/domains/array_adaptive.hpp | 30 +- include/crab/domains/discrete_domains.hpp | 6 +- include/crab/domains/patricia_trees.hpp | 512 ++++------------------ include/crab/domains/separate_domains.hpp | 36 +- 4 files changed, 131 insertions(+), 453 deletions(-) diff --git a/include/crab/domains/array_adaptive.hpp b/include/crab/domains/array_adaptive.hpp index 132e6ac0..8be92ec1 100644 --- a/include/crab/domains/array_adaptive.hpp +++ b/include/crab/domains/array_adaptive.hpp @@ -345,22 +345,24 @@ class offset_map_t { class join_op : public binary_op_t { // apply is called when two bindings (one each from a // different map) have the same key(i.e., offset). - std::pair> apply(const cell_set_t &x, - const cell_set_t &y) { + std::pair> apply(const offset_t &, + const cell_set_t &x, + const cell_set_t &y) override { return {false, cell_set_impl::set_union(x, y)}; } // if one map does not have a key in the other map we add it. - bool default_is_absorbing() { return false; } + bool default_is_absorbing() override { return false; } }; class meet_op : public binary_op_t { - std::pair> apply(const cell_set_t &x, - const cell_set_t &y) { + std::pair> apply(const offset_t &, + const cell_set_t &x, + const cell_set_t &y) override { return {false, cell_set_impl::set_union(x, y)}; } // if one map does not have a key in the other map we ignore // it. - bool default_is_absorbing() { return true; } + bool default_is_absorbing() override { return true; } }; class domain_po : public partial_order_t { @@ -943,7 +945,7 @@ class array_adaptive_domain final class array_state_map_t { private: using patricia_tree_t = ikos::patricia_tree; - using key_binary_op_t = typename patricia_tree_t::key_binary_op_t; + using binary_op_t = typename patricia_tree_t::binary_op_t; public: using iterator = typename patricia_tree_t::iterator; @@ -951,7 +953,7 @@ class array_adaptive_domain final private: patricia_tree_t m_tree; - class join_op : public key_binary_op_t { + class join_op : public binary_op_t { cell_varmap_t &m_cvm_left; smashed_varmap_t &m_svm_left; base_domain_t &m_dom_left; @@ -968,16 +970,16 @@ class array_adaptive_domain final m_dom_right(dom_right) {} std::pair> - apply(const variable_t &k, const array_state &x, const array_state &y) { + apply(const variable_t &k, const array_state &x, const array_state &y) override { array_state z = x.join(k, y, m_cvm_left, m_svm_left, m_dom_left, m_cvm_right, m_svm_right, m_dom_right); return {false, boost::optional(z)}; } - bool default_is_absorbing() { return true; } + bool default_is_absorbing() override { return true; } }; // class join_op - class meet_op : public key_binary_op_t { + class meet_op : public binary_op_t { cell_varmap_t &m_cvm_left; smashed_varmap_t &m_svm_left; base_domain_t &m_dom_left; @@ -994,15 +996,15 @@ class array_adaptive_domain final m_dom_right(dom_right) {} std::pair> - apply(const variable_t &k, const array_state &x, const array_state &y) { + apply(const variable_t &k, const array_state &x, const array_state &y) override { array_state z = x.meet(k, y, m_cvm_left, m_svm_left, m_dom_left, m_cvm_right, m_svm_right, m_dom_right); return {false, boost::optional(z)}; } - bool default_is_absorbing() { return false; } + bool default_is_absorbing() override { return false; } }; // class meet_op - patricia_tree_t apply_operation(key_binary_op_t &o, patricia_tree_t t1, + patricia_tree_t apply_operation(binary_op_t &o, patricia_tree_t t1, const patricia_tree_t &t2) const { bool res = t1.merge_with(t2, o); if (res) { diff --git a/include/crab/domains/discrete_domains.hpp b/include/crab/domains/discrete_domains.hpp index 67a7c299..cfc4af0e 100644 --- a/include/crab/domains/discrete_domains.hpp +++ b/include/crab/domains/discrete_domains.hpp @@ -617,7 +617,8 @@ template class discrete_pair_domain { discrete_pair_domain(bool b) : m_is_top(b) {} class join_op : public binary_op_t { - std::pair> apply(const Value &x, const Value &y) { + std::pair> + apply(const Key &/*key*/, const Value &x, const Value &y) { Value z = x.operator|(y); if (z.is_top()) { return {false, boost::optional()}; @@ -629,7 +630,8 @@ template class discrete_pair_domain { }; // class join_op class meet_op : public binary_op_t { - std::pair> apply(const Value &x, const Value &y) { + std::pair> + apply(const Key &/*key*/, const Value &x, const Value &y) { Value z = x.operator&(y); if (z.is_bottom()) { return {true, boost::optional()}; diff --git a/include/crab/domains/patricia_trees.hpp b/include/crab/domains/patricia_trees.hpp index 5dbf6707..a24740b9 100644 --- a/include/crab/domains/patricia_trees.hpp +++ b/include/crab/domains/patricia_trees.hpp @@ -58,9 +58,9 @@ template class partial_order { public: virtual bool leq(const Value &, const Value &) = 0; - virtual bool default_is_top() = 0; // True if the default value is the top - // element for the partial order (false if - // it is bottom) + // True if the default value is the top element for the partial + // order (false if it is bottom) + virtual bool default_is_top() = 0; virtual ~partial_order() {} }; @@ -72,33 +72,27 @@ template class unary_op { virtual ~unary_op() {} }; -template class binary_op { +template +class binary_op { public: - // if first element of the pair is true then bottom and ignore second element - // else if second element of the pair is empty then top - // else the value stored in the second element of the pair. - virtual std::pair> - apply(const Value &, - const Value &) = 0; // The operation is idempotent: apply(x, x) = x - - virtual bool default_is_absorbing() = 0; // True if the default value is - // absorbing (false if it is neutral) + // If first element of the result_type is true then bottom and + // ignore second element. Otherwise, if second element of + // result_type is empty then top. Otherwise, the value stored in the + // second element of the pair. + using result_type = std::pair>; virtual ~binary_op() {} + + // Given two trees t1 and t2, v1 (v2) is the value associated to key + // k in t1 (t2). This operation returns a new value from v1 and v2. + // + // The operation is idempotent: apply(_, x, x) = x + virtual result_type apply(const Key &k, const Value &v1, const Value &v2) = 0; + + // True if the default value is absorbing (false if it is neutral) + virtual bool default_is_absorbing() = 0; }; - -template class key_binary_op { -public: - virtual std::pair> - // The operation is idempotent: apply(x, x) = x - apply(const Key &, const Value &, const Value &) = 0; - - virtual bool default_is_absorbing() = 0; // True if the default value is - // absorbing (false if it is neutral) - - virtual ~key_binary_op() {} -}; - + namespace patricia_trees_impl { template class tree; } // end namespace patricia_trees_impl @@ -106,7 +100,6 @@ template class tree; template > class patricia_tree { -private: using tree_t = patricia_trees_impl::tree; using tree_ptr = typename tree_t::ptr; @@ -118,7 +111,6 @@ class patricia_tree { using patricia_tree_t = patricia_tree; using unary_op_t = typename tree_t::unary_op_t; using binary_op_t = typename tree_t::binary_op_t; - using key_binary_op_t = typename tree_t::key_binary_op_t; using partial_order_t = typename tree_t::partial_order_t; using binding_t = typename tree_t::binding_t; @@ -132,15 +124,8 @@ class patricia_tree { friend class boost::iterator_core_access; friend class patricia_tree; - private: typename tree_t::iterator _it; - - public: - iterator() {} - - iterator(const patricia_tree_t &pt) : _it(pt._tree) {} - - private: + iterator(tree_ptr t) : _it(t) {} void increment() { ++this->_it; } @@ -149,17 +134,21 @@ class patricia_tree { binding_t dereference() const { return *this->_it; } + + public: + iterator() {} + + iterator(const patricia_tree_t &pt) : _it(pt._tree) {} }; // class iterator class insert_op : public binary_op_t { std::pair> - apply(const Value & /* old_value */, const Value &new_value) override { + apply(const Key & /*key*/, const Value & /* old_value */, const Value &new_value) override { return {false, boost::optional(new_value)}; } bool default_is_absorbing() override { return false; } }; // class insert_op -public: patricia_tree() {} patricia_tree(const patricia_tree_t &t) = default; @@ -197,7 +186,7 @@ class patricia_tree { return nullptr; } } - + bool merge_with(const patricia_tree_t &t, binary_op_t &op) { std::pair res; res = tree_t::merge(this->_tree, t._tree, op, true); @@ -208,17 +197,8 @@ class patricia_tree { return false; } } - bool merge_with(const patricia_tree_t &t, key_binary_op_t &op) { - std::pair res; - res = tree_t::key_merge(this->_tree, t._tree, op, true); - if (res.first) { - return true; // bottom must be propagated - } else { - this->_tree = res.second; - return false; - } - } + void insert(const Key &key, const Value &value) { insert_op op; std::pair res; @@ -246,7 +226,6 @@ class patricia_tree { // An efficient implement of a set based on patricia trees. template class patricia_tree_set { -private: using patricia_tree_t = patricia_tree; public: @@ -256,54 +235,24 @@ template class patricia_tree_set { using partial_order_t = typename patricia_tree_t::partial_order_t; private: - patricia_tree_t _tree; - -public: - class iterator - : public boost::iterator_facade { - friend class boost::iterator_core_access; - friend class patricia_tree_set; - - private: - typename patricia_tree_t::iterator _it; - - public: - iterator() {} - - iterator(const patricia_tree_set_t &ptset) : _it(ptset._tree) {} - - private: - iterator(patricia_tree_t t) : _it(t) {} - - void increment() { ++this->_it; } - - bool equal(const iterator &other) const { return this->_it == other._it; } - - Element dereference() const { return this->_it->first; } - - }; // class iterator -private: class union_op : public binary_op_t { virtual std::pair> - apply(const bool & /* x */, const bool & /* y */) override { + apply(const Element &, const bool & /* x */, const bool & /* y */) override { return {false, boost::optional(true)}; }; virtual bool default_is_absorbing() override { return false; } - - }; // class union_op + }; class intersection_op : public binary_op_t { virtual std::pair> - apply(const bool & /* x */, const bool & /* y */) override { + apply(const Element &, const bool & /* x */, const bool & /* y */) override { return {false, boost::optional(true)}; }; virtual bool default_is_absorbing() override { return true; } - - }; // class intersection_op + }; class subset_po : public partial_order_t { virtual bool leq(const bool & /* x */, const bool & /* y */) override { @@ -311,8 +260,13 @@ template class patricia_tree_set { }; virtual bool default_is_top() override { return false; } - }; // class subset_po + }; + + + patricia_tree_t _tree; + patricia_tree_set(patricia_tree_t &&t) : _tree(std::move(t)) {} + patricia_tree_t do_union(patricia_tree_t t1, const patricia_tree_t &t2) const { union_op o; @@ -337,9 +291,29 @@ template class patricia_tree_set { _tree.merge_with(t, o); } - patricia_tree_set(patricia_tree_t &&t) : _tree(std::move(t)) {} - + public: + class iterator + : public boost::iterator_facade { + friend class boost::iterator_core_access; + friend class patricia_tree_set; + + typename patricia_tree_t::iterator _it; + iterator(patricia_tree_t t) : _it(t) {} + + void increment() { ++this->_it; } + + bool equal(const iterator &other) const { return this->_it == other._it; } + + Element dereference() const { return this->_it->first; } + + public: + iterator() {} + + iterator(const patricia_tree_set_t &ptset) : _it(ptset._tree) {} + }; // class iterator + patricia_tree_set() {} patricia_tree_set(const Element &e) { this->_tree.insert(e, true); } @@ -480,8 +454,7 @@ template class tree { using tree_ptr = std::shared_ptr; using ptr = tree_ptr; using unary_op_t = unary_op; - using binary_op_t = binary_op; - using key_binary_op_t = key_binary_op; + using binary_op_t = binary_op; using partial_order_t = partial_order; struct binding_t { const Key &first; @@ -490,23 +463,18 @@ template class tree { : first(first_), second(second_) {} }; -public: static tree_ptr make_node(index_t, index_t, tree_ptr, tree_ptr); - static tree_ptr make_leaf(const Key &, const Value &); - static std::pair merge(tree_ptr, tree_ptr, binary_op_t &, - bool); - static std::pair key_merge(tree_ptr, tree_ptr, - key_binary_op_t &, bool); + static tree_ptr make_leaf(const Key &, const Value &); static tree_ptr join(tree_ptr t0, tree_ptr t1); + static std::pair merge(tree_ptr, tree_ptr, binary_op_t &, bool); static std::pair insert(tree_ptr, const Key &, const Value &, - binary_op_t &, bool); - static std::pair insert(tree_ptr, const Key &, const Value &, - key_binary_op_t &, bool); + binary_op_t &, bool); static tree_ptr transform(tree_ptr, unary_op_t &); static tree_ptr remove(tree_ptr, const Key &); static bool compare(tree_ptr, tree_ptr, partial_order_t &, bool); - -public: + virtual boost::optional lookup(const Key &) const = 0; + virtual const Value *find(const Key &) const = 0; + virtual std::size_t size() const = 0; virtual bool is_leaf() const = 0; virtual binding_t binding() const = 0; @@ -514,34 +482,21 @@ template class tree { virtual tree_ptr right_branch() const = 0; virtual index_t prefix() const = 0; virtual index_t branching_bit() const = 0; - virtual boost::optional lookup(const Key &) const = 0; - virtual const Value *find(const Key &) const = 0; - -public: + bool is_node() const { return !is_leaf(); } virtual ~tree() {} -public: class iterator - : public boost::iterator_facade { + : public boost::iterator_facade { friend class boost::iterator_core_access; - - private: using branching_t = std::pair; using branching_stack_t = std::vector; - - private: + tree_ptr _current; branching_stack_t _stack; - - public: - iterator() {} - - iterator(tree_ptr t) { this->look_for_next_leaf(t); } - - private: + void look_for_next_leaf(tree_ptr t) { if (t) { if (t->is_leaf()) { @@ -612,26 +567,27 @@ template class tree { CRAB_ERROR("Patricia tree: trying to dereference an empty iterator"); } } + + public: + iterator() {} - }; // class iterator + iterator(tree_ptr t) { this->look_for_next_leaf(t); } + }; // class iterator }; // class tree template class node : public tree { -private: using tree_ptr = typename tree::ptr; using binding_t = typename tree::binding_t; using node_t = node; -private: std::size_t _size; index_t _prefix; index_t _branching_bit; tree_ptr _left_branch; tree_ptr _right_branch; -private: node(); node(const node_t &); node_t &operator=(const node_t &); @@ -704,16 +660,13 @@ class node : public tree { template class leaf : public tree { -private: using tree_ptr = typename tree::ptr; using binding_t = typename tree::binding_t; using leaf_t = leaf; -private: Key _key; Value _value; -private: leaf(); leaf(const leaf_t &); leaf_t &operator=(const leaf_t &); @@ -819,106 +772,6 @@ tree::insert( std::pair res, res_lb, res_rb; std::pair> new_value; std::pair bottom = {true, nil}; - if (t) { - if (t->is_node()) { - index_t branching_bit = t->branching_bit(); - index_t prefix = t->prefix(); - if (match_prefix(key_.index(), prefix, branching_bit)) { - if (zero_bit(key_.index(), branching_bit)) { - tree_ptr lb = t->left_branch(); - tree_ptr new_lb; - if (lb) { - res = insert(lb, key_, value_, op, combine_left_to_right); - if (res.first) { - return bottom; - } - new_lb = res.second; - } else { - if (!op.default_is_absorbing()) { - new_lb = make_leaf(key_, value_); - } - } - if (new_lb == lb) { - return {false, t}; - } else { - return {false, make_node(prefix, branching_bit, new_lb, - t->right_branch())}; - } - } else { - tree_ptr rb = t->right_branch(); - tree_ptr new_rb; - if (rb) { - res = insert(rb, key_, value_, op, combine_left_to_right); - if (res.first) { - return bottom; - } - new_rb = res.second; - } else { - if (!op.default_is_absorbing()) { - new_rb = make_leaf(key_, value_); - } - } - if (new_rb == rb) { - return {false, t}; - } else { - return {false, - make_node(prefix, branching_bit, t->left_branch(), new_rb)}; - } - } - } else { - if (op.default_is_absorbing()) { - return {false, t}; - } else { - return {false, join(make_leaf(key_, value_), t)}; - } - } - } else { - binding_t b = t->binding(); - const Key &key = b.first; - const Value &value = b.second; - if (key.index() == key_.index()) { - new_value = combine_left_to_right ? op.apply(value, value_) - : op.apply(value_, value); - if (new_value.first) { - return bottom; - } - if (new_value.second) { - ValueEqual op; - if (op(*(new_value.second), value)) { - return {false, t}; - } else { - return {false, make_leaf(key_, *(new_value.second))}; - } - } else { - return {false, nil}; - } - } else { - if (op.default_is_absorbing()) { - return {false, t}; - } else { - return {false, join(make_leaf(key_, value_), t)}; - } - } - } - } else { - if (op.default_is_absorbing()) { - return {false, nil}; - } else { - return {false, make_leaf(key_, value_)}; - } - } -} - -template -std::pair::ptr> -tree::insert( - typename tree::ptr t, const Key &key_, - const Value &value_, key_binary_op_t &op, bool combine_left_to_right) { - using tree_ptr = typename tree::ptr; - tree_ptr nil; - std::pair res, res_lb, res_rb; - std::pair> new_value; - std::pair bottom = {true, nil}; if (t) { if (t->is_node()) { index_t branching_bit = t->branching_bit(); @@ -985,8 +838,8 @@ tree::insert( } if (new_value.second) { - ValueEqual op; - if (op(*(new_value.second), value)) { + ValueEqual eq; + if (eq(*(new_value.second), value)) { return {false, t}; } else { return {false, make_leaf(key_, *(new_value.second))}; @@ -1044,8 +897,8 @@ tree::transform( const Value &value = b.second; boost::optional new_value = op.apply(value); if (new_value) { - ValueEqual op; - if (op(*new_value, value)) { + ValueEqual eq; + if (eq(*new_value, value)) { return t; } else { return make_leaf(b.first, *new_value); @@ -1058,7 +911,7 @@ tree::transform( return t; } } - + template typename tree::ptr tree::remove( typename tree::ptr t, const Key &key_) { @@ -1121,185 +974,6 @@ tree::merge( std::pair res, res_lb, res_rb; std::pair> new_value; std::pair bottom = {true, nil}; - if (s) { - if (t) { - if (s == t) { - return {false, s}; - } else if (s->is_leaf()) { - binding_t b = s->binding(); - if (op.default_is_absorbing()) { - const Value *value = t->find(b.first); - if (value) { - new_value = combine_left_to_right ? op.apply(b.second, *value) - : op.apply(*value, b.second); - if (new_value.first) { - return bottom; - } - - if (new_value.second) { - ValueEqual op; - if (op(*(new_value.second), b.second)) { - return {false, s}; - } else { - return {false, make_leaf(b.first, *(new_value.second))}; - } - } else { - return {false, nil}; - } - } else { - return {false, nil}; - } - } else { - return insert(t, b.first, b.second, op, !combine_left_to_right); - } - } else if (t->is_leaf()) { - binding_t b = t->binding(); - if (op.default_is_absorbing()) { - const Value *value = s->find(b.first); - if (value) { - new_value = combine_left_to_right ? op.apply(*value, b.second) - : op.apply(b.second, *value); - if (new_value.first) { - return bottom; - } - if (new_value.second) { - ValueEqual op; - if (op(*(new_value.second), b.second)) { - return {false, t}; - } else { - return {false, make_leaf(b.first, *(new_value.second))}; - } - } else { - return {false, nil}; - } - } else { - return {false, nil}; - } - } else { - return insert(s, b.first, b.second, op, combine_left_to_right); - } - } else { - if (s->branching_bit() == t->branching_bit() && - s->prefix() == t->prefix()) { - res_lb = merge(s->left_branch(), t->left_branch(), op, - combine_left_to_right); - if (res_lb.first) { - return bottom; - } - tree_ptr new_lb = res_lb.second; - res_rb = merge(s->right_branch(), t->right_branch(), op, - combine_left_to_right); - if (res_rb.first) { - return bottom; - } - tree_ptr new_rb = res_rb.second; - if (new_lb == s->left_branch() && new_rb == s->right_branch()) { - return {false, s}; - } else if (new_lb == t->left_branch() && - new_rb == t->right_branch()) { - return {false, t}; - } else { - return {false, - make_node(s->prefix(), s->branching_bit(), new_lb, new_rb)}; - } - } else if (s->branching_bit() > t->branching_bit() && - match_prefix(t->prefix(), s->prefix(), s->branching_bit())) { - if (zero_bit(t->prefix(), s->branching_bit())) { - res_lb = merge(s->left_branch(), t, op, combine_left_to_right); - if (res_lb.first) { - return bottom; - } - tree_ptr new_lb = res_lb.second; - tree_ptr new_rb = - op.default_is_absorbing() ? nil : s->right_branch(); - if (new_lb == s->left_branch() && new_rb == s->right_branch()) { - return {false, s}; - } else { - return {false, make_node(s->prefix(), s->branching_bit(), new_lb, - new_rb)}; - } - } else { - tree_ptr new_lb = - op.default_is_absorbing() ? nil : s->left_branch(); - res_rb = merge(s->right_branch(), t, op, combine_left_to_right); - if (res_rb.first) { - return bottom; - } - tree_ptr new_rb = res_rb.second; - if (new_lb == s->left_branch() && new_rb == s->right_branch()) { - return {false, s}; - } else { - return {false, make_node(s->prefix(), s->branching_bit(), new_lb, - new_rb)}; - } - } - } else if (s->branching_bit() < t->branching_bit() && - match_prefix(s->prefix(), t->prefix(), t->branching_bit())) { - if (zero_bit(s->prefix(), t->branching_bit())) { - res_lb = merge(s, t->left_branch(), op, combine_left_to_right); - if (res_lb.first) { - return bottom; - } - tree_ptr new_lb = res_lb.second; - tree_ptr new_rb = - op.default_is_absorbing() ? nil : t->right_branch(); - if (new_lb == t->left_branch() && new_rb == t->right_branch()) { - return {false, t}; - } else { - return {false, make_node(t->prefix(), t->branching_bit(), new_lb, - new_rb)}; - } - } else { - tree_ptr new_lb = - op.default_is_absorbing() ? nil : t->left_branch(); - - res_rb = merge(s, t->right_branch(), op, combine_left_to_right); - if (res_rb.first) { - return bottom; - } - tree_ptr new_rb = res_rb.second; - if (new_lb == t->left_branch() && new_rb == t->right_branch()) { - return {false, t}; - } else { - return {false, make_node(t->prefix(), t->branching_bit(), new_lb, - new_rb)}; - } - } - } else { - if (op.default_is_absorbing()) { - return {false, nil}; - } else { - return {false, join(s, t)}; - } - } - } - } else { - if (op.default_is_absorbing()) { - return {false, nil}; - } else { - return {false, s}; - } - } - } else { - if (op.default_is_absorbing()) { - return {false, nil}; - } else { - return {false, t}; - } - } -} - -template -std::pair::ptr> -tree::key_merge( - typename tree::ptr s, - typename tree::ptr t, key_binary_op_t &op, - bool combine_left_to_right) { - using tree_ptr = typename tree::ptr; - tree_ptr nil; - std::pair res, res_lb, res_rb; - std::pair> new_value; - std::pair bottom = {true, nil}; if (s) { if (t) { if (s == t) { @@ -1317,8 +991,8 @@ tree::key_merge( } if (new_value.second) { - ValueEqual op; - if (op(*(new_value.second), b.second)) { + ValueEqual eq; + if (eq(*(new_value.second), b.second)) { return {false, s}; } else { return {false, make_leaf(b.first, *(new_value.second))}; @@ -1345,8 +1019,8 @@ tree::key_merge( } if (new_value.second) { - ValueEqual op; - if (op(*(new_value.second), b.second)) { + ValueEqual eq; + if (eq(*(new_value.second), b.second)) { return {false, t}; } else { return {false, make_leaf(b.first, *(new_value.second))}; @@ -1363,13 +1037,13 @@ tree::key_merge( } else { if (s->branching_bit() == t->branching_bit() && s->prefix() == t->prefix()) { - res_lb = key_merge(s->left_branch(), t->left_branch(), op, + res_lb = merge(s->left_branch(), t->left_branch(), op, combine_left_to_right); if (res_lb.first) { return bottom; } tree_ptr new_lb = res_lb.second; - res_rb = key_merge(s->right_branch(), t->right_branch(), op, + res_rb = merge(s->right_branch(), t->right_branch(), op, combine_left_to_right); if (res_rb.first) { return bottom; @@ -1387,7 +1061,7 @@ tree::key_merge( } else if (s->branching_bit() > t->branching_bit() && match_prefix(t->prefix(), s->prefix(), s->branching_bit())) { if (zero_bit(t->prefix(), s->branching_bit())) { - res_lb = key_merge(s->left_branch(), t, op, combine_left_to_right); + res_lb = merge(s->left_branch(), t, op, combine_left_to_right); if (res_lb.first) { return bottom; } @@ -1403,7 +1077,7 @@ tree::key_merge( } else { tree_ptr new_lb = op.default_is_absorbing() ? nil : s->left_branch(); - res_rb = key_merge(s->right_branch(), t, op, combine_left_to_right); + res_rb = merge(s->right_branch(), t, op, combine_left_to_right); if (res_rb.first) { return bottom; } @@ -1418,7 +1092,7 @@ tree::key_merge( } else if (s->branching_bit() < t->branching_bit() && match_prefix(s->prefix(), t->prefix(), t->branching_bit())) { if (zero_bit(s->prefix(), t->branching_bit())) { - res_lb = key_merge(s, t->left_branch(), op, combine_left_to_right); + res_lb = merge(s, t->left_branch(), op, combine_left_to_right); if (res_lb.first) { return bottom; } @@ -1435,7 +1109,7 @@ tree::key_merge( tree_ptr new_lb = op.default_is_absorbing() ? nil : t->left_branch(); - res_rb = key_merge(s, t->right_branch(), op, combine_left_to_right); + res_rb = merge(s, t->right_branch(), op, combine_left_to_right); if (res_rb.first) { return bottom; } diff --git a/include/crab/domains/separate_domains.hpp b/include/crab/domains/separate_domains.hpp index 707608a1..90fd70a6 100644 --- a/include/crab/domains/separate_domains.hpp +++ b/include/crab/domains/separate_domains.hpp @@ -59,11 +59,11 @@ class separate_domain { private: using patricia_tree_t = patricia_tree; - using unary_op_t = typename patricia_tree_t::unary_op_t; using binary_op_t = typename patricia_tree_t::binary_op_t; using partial_order_t = typename patricia_tree_t::partial_order_t; public: + using unary_op_t = typename patricia_tree_t::unary_op_t; using separate_domain_t = separate_domain; using iterator = typename patricia_tree_t::iterator; using key_type = Key; @@ -73,9 +73,9 @@ class separate_domain { bool _is_bottom; patricia_tree_t _tree; -public: class join_op : public binary_op_t { - virtual std::pair> apply(const Value &x, const Value &y) override { + virtual std::pair> + apply(const Key &/*key*/, const Value &x, const Value &y) override { Value z = x.operator|(y); if (z.is_top()) { return {false, boost::optional()}; @@ -90,7 +90,8 @@ class separate_domain { }; // class join_op class widening_op : public binary_op_t { - virtual std::pair> apply(const Value &x, const Value &y) override { + virtual std::pair> + apply(const Key &/*key*/, const Value &x, const Value &y) override { Value z = x.operator||(y); if (z.is_top()) { return {false, boost::optional()}; @@ -108,11 +109,11 @@ class separate_domain { template class widening_thresholds_op : public binary_op_t { const Thresholds &m_ts; - public: widening_thresholds_op(const Thresholds &ts) : m_ts(ts) {} - virtual std::pair> apply(const Value &x, const Value &y) override { + virtual std::pair> + apply(const Key &/*key*/, const Value &x, const Value &y) override { Value z = x.widening_thresholds(y, m_ts); if (z.is_top()) { return {false, boost::optional()}; @@ -128,7 +129,8 @@ class separate_domain { }; // class widening_thresholds_op class meet_op : public binary_op_t { - virtual std::pair> apply(const Value &x, const Value &y) override { + virtual std::pair> + apply(const Key &/*key*/, const Value &x, const Value &y) override { Value z = x.operator&(y); if (z.is_bottom()) { return {true, boost::optional()}; @@ -144,7 +146,8 @@ class separate_domain { }; // class meet_op class narrowing_op : public binary_op_t { - virtual std::pair> apply(const Value &x, const Value &y) override { + virtual std::pair> + apply(const Key &/*key*/, const Value &x, const Value &y) override { Value z = x.operator&&(y); if (z.is_bottom()) { return {true, boost::optional()}; @@ -170,12 +173,6 @@ class separate_domain { }; // class domain_po -public: - static separate_domain_t top() { return separate_domain_t(); } - - static separate_domain_t bottom() { return separate_domain_t(false); } - -private: static patricia_tree_t apply_operation(binary_op_t &o, patricia_tree_t t1, const patricia_tree_t &t2, bool &is_bottom) { @@ -194,6 +191,9 @@ class separate_domain { separate_domain_t &operator=(const separate_domain_t &o) = default; separate_domain_t &operator=(separate_domain_t &&o) = default; + static separate_domain_t top() { return separate_domain_t(); } + static separate_domain_t bottom() { return separate_domain_t(false); } + iterator begin() const { if (is_bottom()) { CRAB_ERROR("Separate domain: trying to invoke iterator on bottom"); @@ -515,8 +515,8 @@ template class separate_discrete_domain { } /* begin patricia_tree API */ class join_op : public binary_op_t { - std::pair> apply(const value_type &x, - const value_type &y) override { + std::pair> + apply(const key_type &/*key*/, const value_type &x, const value_type &y) override { value_type z = x.operator|(y); if (z.is_top()) { // special encoding for top: the patricia tree will not keep @@ -530,8 +530,8 @@ template class separate_discrete_domain { }; // class join_op class meet_op : public binary_op_t { - std::pair> apply(const value_type &x, - const value_type &y) override { + std::pair> + apply(const key_type &/*key*/, const value_type &x, const value_type &y) override { value_type z = x.operator&(y); // Returning this pair means that if z is bottom do not treat it // special and just update the patricia tree with z. From 688a4165702ffff484869ded3530bf85657435fc Mon Sep 17 00:00:00 2001 From: caballa Date: Wed, 2 Mar 2022 20:37:56 -0700 Subject: [PATCH 2/6] refactor(numbers): added hash method to safeint and wrapint --- include/crab/numbers/safeint.hpp | 2 ++ include/crab/numbers/wrapint.hpp | 2 ++ lib/safeint.cpp | 5 +++++ lib/wrapint.cpp | 13 +++++++++++++ 4 files changed, 22 insertions(+) diff --git a/include/crab/numbers/safeint.hpp b/include/crab/numbers/safeint.hpp index 1c5013d3..3ce29843 100644 --- a/include/crab/numbers/safeint.hpp +++ b/include/crab/numbers/safeint.hpp @@ -66,6 +66,8 @@ class safe_i64 { // TODO: output parameters whether operation overflows safe_i64 &operator-=(safe_i64 x); + std::size_t hash() const; + bool operator==(safe_i64 x) const; bool operator!=(safe_i64 x) const; diff --git a/include/crab/numbers/wrapint.hpp b/include/crab/numbers/wrapint.hpp index 33a2c0aa..d35cbc67 100644 --- a/include/crab/numbers/wrapint.hpp +++ b/include/crab/numbers/wrapint.hpp @@ -74,6 +74,8 @@ class wrapint { uint64_t get_uint64_t() const; + std::size_t hash() const; + // return the wrapint as an unsigned big number ikos::z_number get_unsigned_bignum() const; diff --git a/lib/safeint.cpp b/lib/safeint.cpp index 5e3d40cf..cf364855 100644 --- a/lib/safeint.cpp +++ b/lib/safeint.cpp @@ -4,6 +4,7 @@ #include #include +#include namespace crab { @@ -121,6 +122,10 @@ safe_i64 &safe_i64::operator-=(safe_i64 x) { return *this; } +std::size_t safe_i64::hash() const { + return std::hash{}(m_num); +} + bool safe_i64::operator==(safe_i64 x) const { return m_num == x.m_num; } bool safe_i64::operator!=(safe_i64 x) const { return m_num != x.m_num; } diff --git a/lib/wrapint.cpp b/lib/wrapint.cpp index 95f982c5..5ff68ee1 100644 --- a/lib/wrapint.cpp +++ b/lib/wrapint.cpp @@ -6,6 +6,7 @@ #include #include #include +#include namespace crab { @@ -184,6 +185,18 @@ ikos::z_number wrapint::get_signed_bignum() const { bool wrapint::is_zero() const { return _n == 0; } +std::size_t wrapint::hash() const { + auto combine = [](size_t seed, size_t hash_val) -> size_t { + // Similar to boost::hash_combine + seed ^= hash_val + 0x9e3779b9 + (seed << 6) + (seed >> 2); + return seed; + }; + size_t x = std::hash{}(_n); + size_t y = std::hash{}(_width); + size_t z = std::hash{}(_mod); + return combine(combine(x, y), z); +} + wrapint wrapint::operator+(wrapint x) const { sanity_check_bitwidths(x); From df0778453f3135b476fc4dbdf0e99a6254990f96 Mon Sep 17 00:00:00 2001 From: caballa Date: Wed, 2 Mar 2022 20:38:47 -0700 Subject: [PATCH 3/6] refactor(bignum): fast hasher for mpz_t --- lib/bignums.cpp | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/lib/bignums.cpp b/lib/bignums.cpp index 16a8ab4c..39a8d9d2 100644 --- a/lib/bignums.cpp +++ b/lib/bignums.cpp @@ -3,6 +3,11 @@ #include #include +#include + +#include +// part of C++17 +#include namespace ikos { namespace bignums_impl { @@ -116,10 +121,20 @@ std::string z_number::get_str(unsigned base) const { bignums_impl::scoped_cstring res(mpz_get_str(0, base, _n)); return std::string(res.m_str); } - + std::size_t z_number::hash() const { - boost::hash hasher; - return hasher(get_str()); +// https://www.boost.org/doc/libs/1_66_0/libs/multiprecision/doc/html/boost_multiprecision/tut/hash.html + auto hash_val = [](const mpz_srcptr v) { + boost::string_view view { + reinterpret_cast(v->_mp_d), abs(v->_mp_size) * sizeof(mp_limb_t) }; + size_t result = boost::hash{}(view); + // produce different hashes for negative x + if (v->_mp_size < 0) { + result = ~result; + } + return result; + }; + return hash_val(static_cast(_n)); } bool z_number::fits_sint() const { return mpz_fits_sint_p(_n); } @@ -403,8 +418,8 @@ std::string q_number::get_str(unsigned base) const { } std::size_t q_number::hash() const { - boost::hash hasher; - return hasher(get_str()); + // TOFIX: this needs to be faster. + return std::hash{}(get_str()); } q_number q_number::operator+(q_number x) const { From e1aa4d0746ebc5e730650fed60390309fec4716c Mon Sep 17 00:00:00 2001 From: caballa Date: Thu, 3 Mar 2022 12:49:08 -0700 Subject: [PATCH 4/6] fix(bignum): hash string_view in old boost versions --- lib/bignums.cpp | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/lib/bignums.cpp b/lib/bignums.cpp index 39a8d9d2..45915201 100644 --- a/lib/bignums.cpp +++ b/lib/bignums.cpp @@ -6,8 +6,8 @@ #include #include -// part of C++17 #include +#include namespace ikos { namespace bignums_impl { @@ -122,12 +122,20 @@ std::string z_number::get_str(unsigned base) const { return std::string(res.m_str); } -std::size_t z_number::hash() const { -// https://www.boost.org/doc/libs/1_66_0/libs/multiprecision/doc/html/boost_multiprecision/tut/hash.html +std::size_t z_number::hash() const { + // Inspired by + // https://www.boost.org/doc/libs/1_66_0/libs/multiprecision/doc/html/boost_multiprecision/tut/hash.html auto hash_val = [](const mpz_srcptr v) { - boost::string_view view { - reinterpret_cast(v->_mp_d), abs(v->_mp_size) * sizeof(mp_limb_t) }; + boost::string_view view(reinterpret_cast(v->_mp_d), + abs(v->_mp_size) * sizeof(mp_limb_t)); +#if BOOST_VERSION / 100 % 100 >= 74 + // I don't know for sure which boost version started supporting + // direct hashing of boost::string_view. I only know that 1.68 + // didn't and 1.74 does for sure. size_t result = boost::hash{}(view); +#else + size_t result = boost::hash_range(view.begin(), view.end()); +#endif // produce different hashes for negative x if (v->_mp_size < 0) { result = ~result; From a79d9b93aca9016bd6dea697a3cab9ee89e005bd Mon Sep 17 00:00:00 2001 From: Jorge Navas Date: Fri, 4 Mar 2022 09:42:28 -0700 Subject: [PATCH 5/6] Update README.md --- README.md | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index 8e3e62da..0d60cf38 100644 --- a/README.md +++ b/README.md @@ -13,18 +13,10 @@ -If you use this library please cite the paper using the bibtex reference below. -``` -@inproceedings{GN2021, - author={Arie Gurfinkel and Jorge A. Navas}, - title={Abstract Interpretation of {LLVM} with a Region-based Memory Model}, - booktitle = {Software Verification - 13th International Conference, {VSTTE} 2021, - and 14th International Workshop, {NSV} 2021, - October 18-19, 2021, Revised Selected Papers}, - year={2021} -} -``` +**If you use this library please cite this [paper](https://dblp.uni-trier.de/rec/conf/vstte/GurfinkelN21.html).** + +--- # Description # From 5e3fac483791a53d21583b1ae1daebce47284274 Mon Sep 17 00:00:00 2001 From: caballa Date: Fri, 11 Mar 2022 17:34:15 -0700 Subject: [PATCH 6/6] refactor(domains): remove array graph domain This was a proof-of-concept implementation of the paper A Partial-Order Approach to Array Content Analysis. However, the implementation is too inneficient and not well designed (e.g., use of global state). Due to lack of users, it is not worth it to keep it. We will commit soon a completely new implementation --- include/crab/domains/array_graph.hpp | 2603 ----------------- .../array_graph/array_segmentation.hpp | 285 -- include/crab/domains/split_dbm.hpp | 146 +- tests/crab_dom.hpp | 2 - tests/crab_inst.hpp | 1 - ...rray_graph.cc => array_graph.cc.NOCOMPILE} | 0 tests/expected_results.apron.out | 97 - tests/expected_results.elina.out | 97 - tests/expected_results.out | 97 - 9 files changed, 64 insertions(+), 3264 deletions(-) delete mode 100644 include/crab/domains/array_graph.hpp delete mode 100644 include/crab/domains/array_graph/array_segmentation.hpp rename tests/domains/{array_graph.cc => array_graph.cc.NOCOMPILE} (100%) diff --git a/include/crab/domains/array_graph.hpp b/include/crab/domains/array_graph.hpp deleted file mode 100644 index b0a11bae..00000000 --- a/include/crab/domains/array_graph.hpp +++ /dev/null @@ -1,2603 +0,0 @@ -/******************************************************************************* - * An array content domain. - * - * This domain is a simplified implementation of the paper: - * "A Partial-Order Approach to Array Content Analysis" by - * Gange, Navas, Schachte, Sondergaard, and Stuckey - * available here http://arxiv.org/pdf/1408.1754v1.pdf. - * - * It keeps a graph where vertices are array indexes and edges are - * labelled with weights. An edge (i,j) with weight w denotes that - * the property w holds for the array segment [i,j). A weight is an - * arbitrary lattice that can relate multiple array variables as well - * as array with scalar variables. - * - * This domain has the same word-level assumption that the - * array_smashing domain. - ******************************************************************************/ - -/** - * TODOs: - * - * The implementation works for toy programs but we need to fix the - * following issues for being able to analyze real programs: - * - * - landmarks must be kept as local state as part of each abstract - * state. - * - * - reduction between scalar and weight domains must be done - * incrementally. For that, we need some assumptions about the - * underlying scalar domain. For instance, if we assume zones then - * after each operation we know which are the indexes affected by - * the operation. We can use that information for doing reduction - * only on those indexes. This would remove the need of having - * methods such as array_graph_domain_helper_traits::is_unsat and - * array_graph_domain_helper_traits::active_variables which are - * anyway domain dependent. - **/ - -#pragma once - -#include -#include -#include -#include -#include -#include -#include -// XXX: for now the only scalar domain -#include -// XXX: if expression domain is a template parameter no need to include -#include -// XXX: for customized propagations between weight and scalar domains -#include -#include -#include -#include - -#include -#include -#include -#include - -#include -#include -#include -#include -#include - -#pragma GCC diagnostic push -#pragma GCC diagnostic ignored "-Wsign-compare" - -namespace crab { -namespace domains { -/* - A weighted directed graph where the weight is an abstract - domain. The graph should be always kept in a consistent form, - i.e., for all i,j,k:: weight(i,j) <= join(weight(i,k), weight(k,j)) -*/ -template -class array_graph { - -public: - // XXX: make this a template parameter later - // using graph_t = AdaptGraph; - using graph_t = SparseWtGraph; - using _vert_id = typename graph_t::vert_id; - using edge_ref_t = typename graph_t::edge_ref_t; - using Wt = typename graph_t::Wt; - using mut_val_ref_t = typename graph_t::mut_val_ref_t; - -private: - using GrPerm = GraphPerm; - using GrOps = SemiringGrOps; - using Wt_join = typename GrOps::Wt_join; - using Wt_meet = typename GrOps::Wt_meet; - - using vert_map_t = boost::container::flat_map; - using vmap_elt_t = typename vert_map_t::value_type; - using rev_map_t = std::vector>; - using vert_set_t = std::unordered_set<_vert_id>; - using array_graph_t = array_graph; - - vert_map_t _vert_map; - rev_map_t _rev_map; - graph_t _g; - vert_set_t _unstable; - bool _is_bottom; - - struct vert_set_wrap_t { - vert_set_wrap_t(const vert_set_t &_vs) : vs(_vs) {} - - bool operator[](_vert_id v) const { return vs.find(v) != vs.end(); } - const vert_set_t &vs; - }; - - _vert_id get_vert(Vertex v) { - auto it = _vert_map.find(v); - if (it != _vert_map.end()) - return (*it).second; - - _vert_id vert(_g.new_vertex()); - assert(vert <= _rev_map.size()); - - if (vert < _rev_map.size()) { - assert(!_rev_map[vert]); - _rev_map[vert] = v; - } else { - _rev_map.push_back(v); - } - _vert_map.insert(vmap_elt_t(v, vert)); - - return vert; - } - -public: - template class iterator { - public: - using iter_t = iterator; - iterator(const ItS &_it, const rev_map_t &_rev_map) - : it(_it), rev_map(_rev_map) {} - bool operator!=(const iter_t &o) { return it != o.it; } - iter_t &operator++(void) { - ++it; - return *this; - } - Vertex operator*(void)const { - if (!rev_map[*it]) - CRAB_ERROR("Reverse map failed"); - return *(rev_map[*it]); - } - - protected: - ItS it; - const rev_map_t &rev_map; - }; - - struct edge_t { - edge_t(Vertex _v, Wt &_w) : vert(_v), val(_w) {} - Vertex vert; - Wt &val; - }; - - template class edge_iterator { - public: - using iter_t = edge_iterator; - edge_iterator(const ItS &_it, const rev_map_t &_rev_map) - : it(_it), rev_map(_rev_map) {} - bool operator!=(const iter_t &o) { return it != o.it; } - iter_t &operator++(void) { - ++it; - return *this; - } - edge_t operator*(void)const { - edge_ref_t e = *it; - if (!rev_map[e.vert]) - CRAB_ERROR("Reverse map failed"); - Vertex v = *(rev_map[e.vert]); - return edge_t(v, e.val); - } - - protected: - ItS it; - const rev_map_t &rev_map; - }; - - template class iterator_range { - public: - using iterator = ItS; - iterator_range(const Range &r, const rev_map_t &rev_map) - : _r(r), _rev_map(rev_map) {} - iterator begin(void) const { return iterator(_r.begin(), _rev_map); } - iterator end(void) const { return iterator(_r.end(), _rev_map); } - - protected: - Range _r; - const rev_map_t &_rev_map; - }; - - using succ_transform_iterator = iterator; - using pred_transform_iterator = iterator; - using vert_transform_iterator = iterator; - using fwd_edge_transform_iterator = - edge_iterator; - using rev_edge_transform_iterator = - edge_iterator; - - using succ_range = - iterator_range; - using pred_range = - iterator_range; - using vert_range = - iterator_range; - using e_succ_range = iterator_range; - using e_pred_range = iterator_range; - - vert_range verts() { - typename graph_t::vert_range p = _g.verts(); - return vert_range(p, _rev_map); - } - - succ_range succs(Vertex v) { - typename graph_t::succ_range p = _g.succs(get_vert(v)); - return succ_range(p, _rev_map); - } - - pred_range preds(Vertex v) { - typename graph_t::pred_range p = _g.preds(get_vert(v)); - return pred_range(p, _rev_map); - } - - e_succ_range e_succs(Vertex v) { - typename graph_t::e_succ_range p = _g.e_succs(get_vert(v)); - return e_succ_range(p, _rev_map); - } - - e_pred_range e_preds(Vertex v) { - typename graph_t::e_pred_range p = _g.e_preds(get_vert(v)); - return e_pred_range(p, _rev_map); - } - -public: - array_graph(bool is_bottom = false) : _is_bottom(is_bottom) {} - - array_graph(const array_graph_t &o) - : _vert_map(o._vert_map), _rev_map(o._rev_map), _g(o._g), - _unstable(o._unstable), _is_bottom(false) { - if (o._is_bottom) - set_to_bottom(); - } - - array_graph(array_graph_t &&o) - : _vert_map(std::move(o._vert_map)), _rev_map(std::move(o._rev_map)), - _g(std::move(o._g)), _unstable(std::move(o._unstable)), - _is_bottom(o._is_bottom) {} - - array_graph(vert_map_t &vert_map, rev_map_t &rev_map, graph_t &g, - vert_set_t unstable) - : _vert_map(vert_map), _rev_map(rev_map), _g(g), _unstable(unstable), - _is_bottom(false) {} - - array_graph(vert_map_t &&vert_map, rev_map_t &&rev_map, graph_t &&g, - vert_set_t &&unstable) - : _vert_map(std::move(vert_map)), _rev_map(std::move(rev_map)), - _g(std::move(g)), _unstable(std::move(unstable)), _is_bottom(false) {} - - array_graph_t &operator=(const array_graph_t &o) { - if (this != &o) { - if (o._is_bottom) - set_to_bottom(); - else { - _is_bottom = false; - _vert_map = o._vert_map; - _rev_map = o._rev_map; - _g = o._g; - _unstable = o._unstable; - } - } - return *this; - } - - array_graph_t &operator=(array_graph_t &&o) { - if (o._is_bottom) { - set_to_bottom(); - } else { - _is_bottom = false; - _vert_map = std::move(o._vert_map); - _rev_map = std::move(o._rev_map); - _unstable = std::move(o._unstable); - _g = std::move(o._g); - } - return *this; - } - -public: - void set_to_bottom() { - _vert_map.clear(); - _rev_map.clear(); - _g.clear(); - _unstable.clear(); - _is_bottom = true; - } - - void set_to_top() { - array_graph_t dom = make_top(); - std::swap(*this, dom); - } - - array_graph_t make_top() const { return array_graph_t(false); } - - array_graph_t make_bottom() const { return array_graph_t(true); } - - bool is_bottom() const { return _is_bottom; } - - bool is_top() const { - if (_is_bottom) - return false; - return _g.is_empty(); - } - - bool lookup_edge(Vertex s, Vertex d, mut_val_ref_t *w) { - if (is_bottom()) - return false; - auto se = get_vert(s); - auto de = get_vert(d); - return _g.lookup(se, de, w); - } - - // // update edge but do not close graph - // void update_edge_unclosed(Vertex s, Weight w, Vertex d) { - // if (w.is_top()) return; - // normalize(); - // if (is_bottom()) return; - // auto se = get_vert(s); - // auto de = get_vert(d); - // Wt_meet op; - // _g.update_edge(se, w, de, op); - // } - - // close the graph after edge (s,d) has been updated - void close_edge(Vertex s, Vertex d) { - normalize(); - if (is_bottom()) - return; - auto se = get_vert(s); - auto de = get_vert(d); - GrOps::close_after_edge(_g, se, de); - } - - void update_edge(Vertex s, Weight w, Vertex d) { - if (w.is_top()) - return; - - normalize(); - - if (is_bottom()) - return; - - auto se = get_vert(s); - auto de = get_vert(d); - Wt_meet op; - _g.update_edge(se, w, de, op); - GrOps::close_after_edge(_g, se, de); - } - - // void full_close() { // for debugging - // if (is_bottom()) return; - // GrOps::floyd_warshall(_g); - // } - - void expand(Vertex s, Vertex d) { - if (is_bottom()) - return; - - auto it = _vert_map.find(d); - if (it != _vert_map.end()) { - CRAB_ERROR("array_graph expand failed because vertex ", d, - " already exists"); - } - - auto se = get_vert(s); - auto de = get_vert(d); - - for (auto edge : _g.e_preds(se)) - _g.add_edge(edge.vert, edge.val, de); - - for (auto edge : _g.e_succs(se)) - _g.add_edge(de, edge.val, edge.vert); - } - - void normalize() { -#if 0 - GrOps::closure(_g); // only for debugging purposes -#else - // Always maintained in closed form except for widening - if (_unstable.size() == 0) - return; - GrOps::close_after_widen(_g, vert_set_wrap_t(_unstable)); - _unstable.clear(); -#endif - } - - void operator|=(const array_graph_t &o) { *this = *this | o; } - - bool operator<=(const array_graph_t &o) const { - if (is_bottom()) - return true; - else if (o.is_bottom()) - return false; - else if (o.is_top()) - return true; - else if (is_top()) - return false; - else { - array_graph_t left(*this); - array_graph_t right(o); - - left.normalize(); - - if (left._vert_map.size() < right._vert_map.size()) - return false; - - // Set up a mapping from o to this. - std::vector vert_renaming(right._g.size(), -1); - for (auto p : right._vert_map) { - auto it = left._vert_map.find(p.first); - // We can't have this <= o if we're missing some - // vertex. - if (it == left._vert_map.end()) - return false; - vert_renaming[p.second] = (*it).second; - } - - assert(left._g.size() > 0); - mut_val_ref_t wx; - - for (_vert_id ox : right._g.verts()) { - assert(vert_renaming[ox] != -1); - _vert_id x = vert_renaming[ox]; - for (auto edge : right._g.e_succs(ox)) { - _vert_id oy = edge.vert; - assert(vert_renaming[ox] != -1); - _vert_id y = vert_renaming[oy]; - if (!left._g.lookup(x, y, &wx) || (!(wx.get() <= edge.val))) - return false; - } - } - return true; - } - } - - array_graph_t operator|(const array_graph_t &o) const { - - if (is_bottom() || o.is_top()) - return o; - else if (is_top() || o.is_bottom()) - return *this; - else { - CRAB_LOG("array-sgraph", crab::outs() << "Before join:\n" - << "Graph 1\n" - << *this << "\n" - << "Graph 2\n" - << o << "\n"); - - array_graph_t left(*this); - array_graph_t right(o); - - left.normalize(); - right.normalize(); - - // Figure out the common renaming. - std::vector<_vert_id> perm_x; - std::vector<_vert_id> perm_y; - - vert_map_t out_vmap; - rev_map_t out_revmap; - - for (auto p : left._vert_map) { - auto it = right._vert_map.find(p.first); - // Vertex exists in both - if (it != right._vert_map.end()) { - out_vmap.insert(vmap_elt_t(p.first, perm_x.size())); - out_revmap.push_back(p.first); - - perm_x.push_back(p.second); - perm_y.push_back((*it).second); - } - } - - // Build the permuted view of x and y. - assert(left._g.size() > 0); - GrPerm gx(perm_x, left._g); - assert(right._g.size() > 0); - GrPerm gy(perm_y, right._g); - - // We now have the relevant set of relations. Because g_rx - // and g_ry are closed, the result is also closed. - graph_t join_g(GrOps::join(gx, gy)); - - // Now garbage collect any unused vertices - for (_vert_id v : join_g.verts()) { - if (join_g.succs(v).size() == 0 && join_g.preds(v).size() == 0) { - join_g.forget(v); - if (out_revmap[v]) { - out_vmap.erase(*(out_revmap[v])); - out_revmap[v] = boost::none; - } - } - } - - array_graph_t res(std::move(out_vmap), std::move(out_revmap), - std::move(join_g), vert_set_t()); - CRAB_LOG("array-sgraph", crab::outs() << "Result join:\n" - << res << "\n";); - return res; - } - } - - template - array_graph_t widening_thresholds(const array_graph_t &o, - const Thresholds &) const { - return (*this || o); - } - - array_graph_t operator||(const array_graph_t &o) const { - if (is_bottom()) - return o; - else if (o.is_bottom()) - return *this; - else { - CRAB_LOG("array-sgraph", crab::outs() << "Before widening:\n" - << "Graph 1\n" - << *this << "\n" - << "Graph 2\n" - << o << "\n";); - array_graph_t right(o); - right.normalize(); - - // Figure out the common renaming - std::vector<_vert_id> perm_x; - std::vector<_vert_id> perm_y; - vert_map_t out_vmap; - rev_map_t out_revmap; - vert_set_t widen_unstable(_unstable); - - for (auto p : _vert_map) { - auto it = right._vert_map.find(p.first); - // Vertex exists in both - if (it != right._vert_map.end()) { - out_vmap.insert(vmap_elt_t(p.first, perm_x.size())); - out_revmap.push_back(p.first); - - perm_x.push_back(p.second); - perm_y.push_back((*it).second); - } - } - - graph_t left_g(_g); - // Build the permuted view of x and y. - // assert(left_g.size() > 0); - GrPerm gx(perm_x, left_g); - // assert(right._g.size() > 0); - GrPerm gy(perm_y, right._g); - - // Now perform the widening - std::vector<_vert_id> destabilized; - graph_t widen_g(GrOps::widen(gx, gy, destabilized)); - for (_vert_id v : destabilized) { - widen_unstable.insert(v); - } - - array_graph_t res(std::move(out_vmap), std::move(out_revmap), - std::move(widen_g), std::move(widen_unstable)); - CRAB_LOG("array-sgraph", crab::outs() << "Result widening:\n" - << res << "\n";); - return res; - } - } - - array_graph_t meet_or_narrowing(const array_graph_t &o, bool is_meet, - const std::string op) const { - - if (is_bottom() || o.is_top()) { - return *this; - } else if (is_top() || o.is_bottom()) { - return o; - } else { - CRAB_LOG("array-sgraph", crab::outs() << "Before " << op << ":\n" - << "Graph 1\n" - << *this << "\n" - << "Graph 2\n" - << o << "\n"); - - array_graph_t left(*this); - array_graph_t right(o); - - left.normalize(); - right.normalize(); - - // Figure out the common renaming. - std::vector<_vert_id> perm_x; - std::vector<_vert_id> perm_y; - - vert_map_t out_vmap; - rev_map_t out_revmap; - - for (auto p : left._vert_map) { - _vert_id vv = perm_x.size(); - out_vmap.insert(vmap_elt_t(p.first, vv)); - out_revmap.push_back(p.first); - - perm_x.push_back(p.second); - perm_y.push_back(-1); - } - - // Add missing mappings from the right operand. - for (auto p : right._vert_map) { - auto it = out_vmap.find(p.first); - if (it == out_vmap.end()) { - _vert_id vv = perm_y.size(); - out_revmap.push_back(p.first); - - perm_y.push_back(p.second); - perm_x.push_back(-1); - out_vmap.insert(vmap_elt_t(p.first, vv)); - } else { - perm_y[(*it).second] = p.second; - } - } - - // Build the permuted view of x and y. - GrPerm gx(perm_x, left._g); - GrPerm gy(perm_y, right._g); - - // Compute the syntactic meet/narrowing of the permuted graphs. - std::vector<_vert_id> changes; - graph_t out_g(GrOps::meet_or_narrowing(gx, gy, is_meet, changes)); - vert_set_t unstable; - for (_vert_id v : changes) - unstable.insert(v); - - GrOps::close_after_meet_or_narrowing(out_g, vert_set_wrap_t(unstable)); - - array_graph_t res(std::move(out_vmap), std::move(out_revmap), - std::move(out_g), vert_set_t()); - CRAB_LOG("array-sgraph", crab::outs() << "Result " << op << ":\n" - << res << "\n";); - return res; - } - } - - array_graph_t operator&(const array_graph_t &o) const { - return meet_or_narrowing(o, true, "meet"); - } - - array_graph_t operator&&(const array_graph_t &o) const { - return meet_or_narrowing(o, false, "narrowing"); - } - - // array_graph_t operator&(array_graph_t& o) { - - // if (is_bottom() || o.is_bottom()) - // return bottom(); - // else if (is_top()) - // return o; - // else if (o.is_top()) - // return *this; - // else { - // CRAB_LOG("array-sgraph", - // crab::outs() << "Before meet:\n"<<"Graph 1\n"<<*this<<"\n" - // <<"Graph 2\n"< perm_x; - // std::vector<_vert_id> perm_y; - - // vert_map_t out_vmap; - // rev_map_t out_revmap; - - // for(auto p : _vert_map) - // { - // _vert_id vv = perm_x.size(); - // out_vmap.insert(vmap_elt_t(p.first, vv)); - // out_revmap.push_back(p.first); - - // perm_x.push_back(p.second); - // perm_y.push_back(-1); - // } - - // // Add missing mappings from the right operand. - // for(auto p : o._vert_map) - // { - // auto it = out_vmap.find(p.first); - // if(it == out_vmap.end()) - // { - // _vert_id vv = perm_y.size(); - // out_revmap.push_back(p.first); - - // perm_y.push_back(p.second); - // perm_x.push_back(-1); - // out_vmap.insert(vmap_elt_t(p.first, vv)); - // } else { - // perm_y[(*it).second] = p.second; - // } - // } - - // // Build the permuted view of x and y. - // //assert(_g.size() > 0); - // GrPerm gx(perm_x, _g); - // //assert(o._g.size() > 0); - // GrPerm gy(perm_y, o._g); - - // // Compute the syntactic meet of the permuted graphs. - // std::vector<_vert_id> changes; - // graph_t meet_g(GrOps::meet_or_narrowing(gx, gy, true /*meet*/, - // changes)); vert_set_t unstable; for(_vert_id v : changes) - // unstable.insert(v); - - // GrOps::close_after_meet_or_narrowing(_g, vert_set_wrap_t(unstable)); - - // array_graph_t res(std::move(out_vmap), std::move(out_revmap), - // std::move(meet_g), vert_set_t()); - // CRAB_LOG("array-sgraph", crab::outs() << "Result meet:\n"<< res - // <<"\n";); return res; - // } - // } - - // array_graph_t operator&&(array_graph_t& o) { - // if (is_bottom() || o.is_bottom()) - // return bottom(); - // else if (is_top()) - // return o; - // else{ - // CRAB_LOG("array-sgraph", - // crab::outs() << "Before narrowing:\n"<<"Graph - // 1\n"<<*this<<"\n" - // <<"Graph 2\n"<second); - _rev_map[it->second] = boost::none; - _vert_map.erase(v); - } - } - - void remove_from_weights(typename Weight::variable_t v) { - mut_val_ref_t w_pq; - for (auto p : _g.verts()) - for (auto e : _g.e_succs(p)) { - auto q = e.vert; - if (_g.lookup(p, q, &w_pq)) { - Weight w = w_pq.get(); - w -= v; - Wt_meet op; - _g.update_edge(p, w, q, op); - GrOps::close_after_edge(_g, p, q); - } - } - } - - void write(crab_os &o) const { - array_graph_t tmp(*this); - write(o, tmp, true); - } - - // used also by array_graph_domain - static void write(crab_os &o, array_graph_t &g, bool print_bottom_edges) { - g.normalize(); - - if (g.is_bottom()) { - o << "_|_"; - return; - } else if (g.is_top()) { - o << "{}"; - return; - } else { - bool first = true; - o << "{"; - - // sorting only for helping debugging - std::vector<_vert_id> verts; - for (auto v : g._g.verts()) - verts.push_back(v); - std::sort(verts.begin(), verts.end()); - - for (_vert_id s : verts) { - if (!g._rev_map[s]) - continue; - - auto vs = *g._rev_map[s]; - - // sorting only for helping debugging - std::vector<_vert_id> succs; - for (auto d : g._g.succs(s)) - succs.push_back(d); - std::sort(succs.begin(), succs.end()); - - for (_vert_id d : succs) { - if (!g._rev_map[d]) - continue; - - auto w = g._g.edge_val(s, d); - if (!print_bottom_edges && w.is_bottom()) - continue; // do not print bottom edges - - auto vd = *g._rev_map[d]; - - if (first) - first = false; - else - o << ", "; - o << "[" << vs << "," << vd << ")=>" << w; - } - } - o << "}"; - } - } - - friend crab::crab_os &operator<<(crab::crab_os &o, const array_graph_t &g) { - g.write(o); - return o; - } -}; - -namespace array_graph_impl { - -// JN: I do not know how to propagate arbitrary invariants -// between weight and scalar domains in a domain-independent -// manner. Here, we define propagations between specific -// domains. - -template -ikos::interval -eval_interval(Dom dom, typename Dom::linear_expression_t e) { - ikos::interval r = e.constant(); - for (auto p : e) - r += p.first * dom[p.second]; - return r; -} - -template -void propagate_between_weight_and_scalar( - Dom1 src, typename Dom1::linear_expression_t src_e, variable_type ty, - Dom2 &dst, typename Dom2::variable_t dst_var) { - - if (ty.is_integer_array() || ty.is_real_array()) { - // --- XXX: simplification wrt Gange et.al.: - // Only non-relational numerical invariants are - // propagated from the graph domain to the scalar domain. - dst.set(dst_var, eval_interval(src, src_e)); - } else { - CRAB_WARN("Unsupported array type ", __LINE__, ":", - "missing propagation between weight and scalar domains"); - } -} - -} // namespace array_graph_impl - -// Landmark: another C++ datatype to wrap variables and numbers as -// graph vertices. - -enum landmark_kind_t { LMC, LMV, LMVP }; - -template class landmark { -protected: - landmark_kind_t _kind; - landmark(landmark_kind_t kind) : _kind(kind) {} - -public: - virtual ~landmark() {} - - landmark_kind_t kind() const { return _kind; } - - virtual bool operator==(const landmark &o) const = 0; - - virtual bool operator<(const landmark &o) const = 0; - - virtual void write(crab_os &o) const = 0; - - virtual std::size_t hash() const = 0; -}; - -template -class landmark_cst : public landmark { - - Number _n; - using landmark_t = landmark; - using landmark_cst_t = landmark_cst; - -public: - landmark_cst(Number n) : landmark_t(landmark_kind_t::LMC), _n(n) {} - - bool operator==(const landmark_t &o) const { - if (this->_kind != o.kind()) - return false; - - assert(o.kind() == landmark_kind_t::LMC); - auto o_ptr = static_cast(&o); - return (_n == o_ptr->_n); - } - - bool operator<(const landmark_t &o) const { - if (this->_kind != o.kind()) - return true; - - assert(o.kind() == landmark_kind_t::LMC); - return (_n < static_cast(&o)->_n); - } - - void write(crab_os &o) const { o << _n; } - - std::size_t hash() const { return std::hash{}(_n); } - - Number get_cst() const { return _n; } -}; - -template -class landmark_var : public landmark { - - Variable _v; - using landmark_t = landmark; - using landmark_var_t = landmark_var; - -public: - landmark_var(Variable v) : landmark_t(landmark_kind_t::LMV), _v(v) {} - - bool operator==(const landmark_t &o) const { - if (this->_kind != o.kind()) - return false; - - assert(o.kind() == landmark_kind_t::LMV); - auto o_ptr = static_cast(&o); - return (_v == o_ptr->_v); - } - - bool operator<(const landmark_t &o) const { - if (this->_kind == o.kind()) { - assert(o.kind() == landmark_kind_t::LMV); - auto o_ptr = static_cast(&o); - return (_v < o_ptr->_v); - } else if (o.kind() == LMC) { - return false; - } else if (o.kind() == LMVP) { - return true; - } else - CRAB_ERROR("unreachable!"); - } - - void write(crab_os &o) const { o << _v; } - - std::size_t hash() const { return _v.hash(); } - - Variable get_var() const { return _v; } -}; - -template -class landmark_varprime : public landmark { - std::string _lm; - Variable _v; - - using landmark_t = landmark; - using landmark_var_prime_t = landmark_varprime; - -public: - landmark_varprime(std::string lm, Variable v) - : landmark_t(landmark_kind_t::LMVP), _lm(lm), _v(v) {} - - bool operator==(const landmark_t &o) const { - if (this->_kind != o.kind()) - return false; - - assert(o.kind() == landmark_kind_t::LMVP); - auto o_ptr = static_cast(&o); - return (_v == o_ptr->_v); - } - - bool operator<(const landmark_t &o) const { - if (this->_kind != o.kind()) - return false; - - assert(o.kind() == landmark_kind_t::LMVP); - auto o_ptr = static_cast(&o); - return (_v < o_ptr->_v); - } - - void write(crab_os &o) const { o << _lm << "'"; } - - std::size_t hash() const { return _v.hash(); } - - Variable get_var() const { return _v; } -}; - -// Wrapper for landmark -template class landmark_ref { - using landmark_t = landmark; - using landmark_ref_t = landmark_ref; - -public: - // yeah I know this is bad ... - std::shared_ptr _ref; - - landmark_ref(Variable v, std::string name = "") : _ref(nullptr) { - if (name == "") { - _ref = std::static_pointer_cast( - std::make_shared>( - landmark_var(v))); - } else { - _ref = std::static_pointer_cast( - std::make_shared>( - landmark_varprime(name, v))); - } - } - landmark_ref(Number n) - : _ref(std::static_pointer_cast( - std::make_shared>( - landmark_cst(n)))) {} - - landmark_kind_t kind() const { return _ref->kind(); } - - bool operator==(const landmark_ref &o) const { return (*_ref == *(o._ref)); } - - bool operator<(const landmark_ref &o) const { return (*_ref < *(o._ref)); } - - void write(crab_os &o) const { _ref->write(o); } - - std::size_t hash() const { return _ref->hash(); } -}; - -// super unsafe! -template -inline Variable get_var(const landmark_ref &lm) { - assert(lm.kind() == LMVP); - return std::static_pointer_cast>( - lm._ref) - ->get_var(); -} - -// super unsafe! -template -inline Number get_cst(const landmark_ref &lm) { - assert(lm.kind() == LMC); - return std::static_pointer_cast>(lm._ref) - ->get_cst(); -} - -template -inline crab_os &operator<<(crab_os &o, - const landmark_ref &lm) { - lm.write(o); - return o; -} -} // end namespace domains -} // end namespace crab - -namespace std { -template -struct hash> { - using landmark_ref_t = crab::domains::landmark_ref; - size_t operator()(const landmark_ref_t &lm) { return lm.hash(); } -}; -} // namespace std - -namespace crab { -namespace domains { - -template struct landmark_ref_hasher { - size_t operator()(const landmark_ref &lm) const { - return lm.hash(); - } -}; - -template struct landmark_ref_equal { - bool operator()(const landmark_ref &lm1, - const landmark_ref &lm2) const { - return lm1 == lm2; - } -}; - -template -using landmark_ref_unordered_map = - std::unordered_map, MappedVal, - landmark_ref_hasher, - landmark_ref_equal>; - -/* - Reduced product of a numerical domain with a weighted array - graph. - - FIXME: the set of array landmarks are chosen statically before - starting the analysis (do_initialization). However, at - anytime only those alive (using scalar domain) are - considered. - - The main issue is that the landmarks are kept as global - state. This is really error-prone. For instance, - landmarks are reset each time a new CFG is analyzed. For - a summary-based inter-procedural analysis might be ok but - not, e.g., for inlining. -*/ -template -class array_graph_domain final - : public abstract_domain_api< - array_graph_domain> { -public: - using number_t = typename NumDom::number_t; - using varname_t = typename NumDom::varname_t; - -private: - static_assert(std::is_same::value, - "Scalar and Content domains must have the same number type"); - static_assert(std::is_same::value, - "Scalar and Content domains must have the same varname type"); - - // We need the operations is_unsat and active_variables from the - // scalar domain - static_assert( - std::is_same>::value, - "Scalar domain is supposed to be generic but currently only " - "split_dbm_domain supported"); - - using array_graph_domain_t = - array_graph_domain; - using abstract_domain_t = abstract_domain_api; - -public: - using typename abstract_domain_t::disjunctive_linear_constraint_system_t; - using typename abstract_domain_t::interval_t; - using typename abstract_domain_t::linear_constraint_system_t; - using typename abstract_domain_t::linear_constraint_t; - using typename abstract_domain_t::linear_expression_t; - using typename abstract_domain_t::reference_constraint_t; - using variable_t = typename NumDom::variable_t; - using variable_or_constant_t = typename NumDom::variable_or_constant_t; - using variable_vector_t = typename NumDom::variable_vector_t; - using variable_or_constant_vector_t = typename NumDom::variable_or_constant_vector_t; - - using landmark_cst_t = landmark_cst; - using landmark_var_t = landmark_var; - using landmark_var_prime_t = landmark_varprime; - using landmark_ref_t = landmark_ref; - using array_graph_t = array_graph; - - //// XXX: make this a template parameter later - using str_varname_t = crab::var_factory_impl::str_var_alloc_col::varname_t; - using str_interval_dom_t = - ikos::interval_domain; - using idom_info = - term::TDomInfo; - using expression_domain_t = term_domain; - -private: - using mut_val_ref_t = typename array_graph_t::mut_val_ref_t; - - // Quick wrapper to perform efficient unsat queries on the - // scalar domain. - struct solver_wrapper { - // XXX: do not pass by reference - NumDom _inv; - solver_wrapper(NumDom inv) : _inv(inv) {} - bool is_unsat(linear_constraint_t cst) { - // XXX: it might modify _inv so that's why we make a copy in - // the constructor. - return _inv.is_unsat(cst); - } - }; - - NumDom _scalar; - expression_domain_t - _expressions; // map each program variable to a symbolic expression - array_graph_t _g; - - // A landmark is either a variable or number that may appear as - // an array index. In addition, for each landmark l we keep - // track of a prime landmark l' whose meaning is l'=l+1. - - /// === Static data - using lm_map_t = - landmark_ref_unordered_map; - static lm_map_t s_var_landmarks; - static lm_map_t s_cst_landmarks; - - // --- landmark iterators - struct get_first : public std::unary_function { - get_first() {} - landmark_ref_t operator()(const typename lm_map_t::value_type &p) const { - return p.first; - } - }; - struct get_second : public std::unary_function { - get_second() {} - landmark_ref_t operator()(const typename lm_map_t::value_type &p) const { - return p.second; - } - }; - using lm_iterator = - boost::transform_iterator; - using lm_const_iterator = - boost::transform_iterator; - - using lm_prime_iterator = - boost::transform_iterator; - using lm_prime_const_iterator = - boost::transform_iterator; - - using lm_range = boost::iterator_range; - using lm_const_range = boost::iterator_range; - using lm_prime_range = boost::iterator_range; - using lm_prime_const_range = boost::iterator_range; - - lm_prime_iterator var_lm_prime_begin() { - return boost::make_transform_iterator(s_var_landmarks.begin(), - get_second()); - } - lm_prime_iterator var_lm_prime_end() { - return boost::make_transform_iterator(s_var_landmarks.end(), get_second()); - } - - lm_prime_const_iterator var_lm_prime_begin() const { - return boost::make_transform_iterator(s_var_landmarks.begin(), - get_second()); - } - lm_prime_const_iterator var_lm_prime_end() const { - return boost::make_transform_iterator(s_var_landmarks.end(), get_second()); - } - - lm_prime_range var_lm_primes() { - return boost::make_iterator_range(var_lm_prime_begin(), var_lm_prime_end()); - } - - lm_prime_const_range var_lm_primes() const { - return boost::make_iterator_range(var_lm_prime_begin(), var_lm_prime_end()); - } - - lm_prime_iterator cst_lm_prime_begin() { - return boost::make_transform_iterator(s_cst_landmarks.begin(), - get_second()); - } - lm_prime_iterator cst_lm_prime_end() { - return boost::make_transform_iterator(s_cst_landmarks.end(), get_second()); - } - - lm_prime_const_iterator cst_lm_prime_begin() const { - return boost::make_transform_iterator(s_cst_landmarks.begin(), - get_second()); - } - lm_prime_const_iterator cst_lm_prime_end() const { - return boost::make_transform_iterator(s_cst_landmarks.end(), get_second()); - } - - lm_prime_range cst_lm_primes() { - return boost::make_iterator_range(cst_lm_prime_begin(), cst_lm_prime_end()); - } - - lm_prime_const_range cst_lm_primes() const { - return boost::make_iterator_range(cst_lm_prime_begin(), cst_lm_prime_end()); - } - - Content make_content_bottom() const { - Content dom; - return dom.make_bottom(); - } - - Content make_content_top() const { - Content dom; - return dom.make_top(); - } - -public: - // Horrible hack: this method needs to be called before the analysis - // starts so that the domain can collect relevant indexes. - template static void do_initialization(CFG cfg) { - using array_segment_analysis_t = crab::analyzer::array_segmentation; - using array_segment_domain_t = - typename array_segment_analysis_t::array_segment_domain_t; - using array_cst_segment_visitor_t = - crab::analyzer::array_constant_segment_visitor; - - std::set lms; - // add variables - array_segment_analysis_t analysis(cfg); - analysis.exec(); - auto var_indexes = analysis.get_variables(cfg.entry()); - - if (var_indexes.begin() == var_indexes.end()) { - CRAB_WARN("No variables found in the cfg. No array graph landmarks will " - "be added\n"); - return; - } - lms.insert(var_indexes.begin(), var_indexes.end()); - - // add constants - // make sure 0 is always considered as an array index - lms.insert(landmark_ref_t(number_t(0))); - typename array_cst_segment_visitor_t::constant_set_t constants; - for (auto &bb : boost::make_iterator_range(cfg.begin(), cfg.end())) { - auto var_indexes = analysis.get_variables(bb.label()); - // XXX: use some heuristics to choose "relevant" constants - array_cst_segment_visitor_t vis(var_indexes); - for (auto &s : boost::make_iterator_range(bb.begin(), bb.end())) - s.accept(&vis); - auto cst_indexes = vis.get_constants(); - lms.insert(cst_indexes.begin(), cst_indexes.end()); - } - - // get variable factory - auto &vfac = const_cast(&((*var_indexes.begin()).name())) - ->get_var_factory(); - set_landmarks(lms, vfac); - } - - template - static void set_landmarks(const Range &lms, VarFactory &vfac) { - - s_var_landmarks.clear(); - s_cst_landmarks.clear(); - - unsigned num_vl = 0; - unsigned num_cl = 0; - - for (auto lm : lms) { - switch (lm.kind()) { - case LMV: { - auto v = - std::static_pointer_cast(lm._ref)->get_var(); - variable_t v_prime(vfac.get(v.name(), ".next")); - landmark_ref_t lm_prime(v_prime, v.name().str()); - s_var_landmarks.insert(std::make_pair(lm, lm_prime)); - num_vl++; - break; - } - case LMC: { - auto n = - std::static_pointer_cast(lm._ref)->get_cst(); - variable_t v_prime(vfac.get()); - landmark_ref_t lm_prime(v_prime, n.get_str()); - s_cst_landmarks.insert(std::make_pair(lm, lm_prime)); - num_cl++; - break; - } - default: - CRAB_ERROR("A landmark can only be either variable or constant"); - } - } - CRAB_LOG( - "array-sgraph-landmark", - crab::outs() << "Added " << num_vl << " variable landmarks " - << "and " << num_cl << " constant landmarks={"; - bool first = true; for (auto &l - : s_var_landmarks) { - if (!first) - crab::outs() << ","; - first = false; - crab::outs() << l.first; - } for (auto &l - : s_cst_landmarks) { - if (!first) - crab::outs() << ","; - first = false; - crab::outs() << l.first; - } crab::outs() << "}\n";); - } - -public: // public only for tests - void add_landmark(variable_t v) { - landmark_ref_t lm_v(v); - auto &vfac = const_cast(&(v.name()))->get_var_factory(); - landmark_ref_t lm_v_prime(variable_t(vfac.get(v.name(), ".next")), - v.name().str()); - // add pair x -> x' - s_var_landmarks.insert(std::make_pair(lm_v, lm_v_prime)); - // x' = x + 1 - _scalar += make_prime_relation(lm_v_prime, lm_v); - - // reduce between _scalar and the array graph - if (!reduce(_scalar, _g)) { - // FIXME: incremental version - // TODO: we can assume that the scalar domain is zones so - // that we can return the affected edges after each - // operation and apply reduction only on those edges. That - // would suffice for now. If the scalar domain is not zones - // then we don't reduce incrementally. - set_to_bottom(); - } - - CRAB_LOG("array-sgraph-landmark", crab::outs() - << "Added landmark " << v << "\n";); - } - - void remove_landmark(variable_t v) { - array_forget(v); - forget_prime_var(v); - s_var_landmarks.erase(landmark_ref_t(v)); - - CRAB_LOG("array-sgraph-landmark", crab::outs() - << "Removed landmark " << v << "\n";); - } - -private: - // By active we mean current variables that are kept track by - // the scalar domain. - void get_active_landmarks(NumDom &scalar, - std::vector &landmarks) const { - landmarks.reserve(s_cst_landmarks.size()); - for (auto p : s_cst_landmarks) { - landmarks.push_back(p.first); - landmarks.push_back(p.second); - } - std::vector active_vars; - scalar.active_variables(active_vars); - for (auto v : active_vars) { - auto it = s_var_landmarks.find(landmark_ref_t(v)); - if (it != s_var_landmarks.end()) { - landmarks.push_back(landmark_ref_t(v)); - landmarks.push_back(it->second); - } - } - } - - linear_expression_t make_expr(landmark_ref_t x) const { - switch (x.kind()) { - case LMC: - return std::static_pointer_cast(x._ref)->get_cst(); - case LMV: - return variable_t( - std::static_pointer_cast(x._ref)->get_var()); - case LMVP: - return variable_t( - std::static_pointer_cast(x._ref)->get_var()); - default: - CRAB_ERROR("unreachable!"); - } - } - - // make constraint x < y - linear_constraint_t make_lt_cst(landmark_ref_t x, landmark_ref_t y) const { - return linear_constraint_t(make_expr(x) <= make_expr(y) - 1); - } - - // make constraint x <= y - linear_constraint_t make_leq_cst(landmark_ref_t x, landmark_ref_t y) const { - return linear_constraint_t(make_expr(x) <= make_expr(y)); - } - - // make constraint x == y - linear_constraint_t make_eq_cst(landmark_ref_t x, landmark_ref_t y) const { - return linear_constraint_t(make_expr(x) == make_expr(y)); - } - - // make constraint x' == x+1 - linear_constraint_t make_prime_relation(landmark_ref_t x_prime, - landmark_ref_t x) const { - return linear_constraint_t(make_expr(x_prime) == make_expr(x) + 1); - } - - // return true if v is a landmark in the graph - bool is_landmark(variable_t v) const { - landmark_ref_t lm_v(v); - auto it = s_var_landmarks.find(lm_v); - return (it != s_var_landmarks.end()); - } - - // return true if n is a landmark in the graph - bool is_landmark(ikos::z_number n) const { - landmark_ref_t lm_n(n); - auto it = s_cst_landmarks.find(lm_n); - return (it != s_cst_landmarks.end()); - } - - // return the prime landmark of v - landmark_ref_t get_landmark_prime(variable_t v) const { - landmark_ref_t lm_v(v); - auto it = s_var_landmarks.find(lm_v); - assert(it != s_var_landmarks.end()); - return it->second; - } - - // Return the weight from the edge (i, i') otherwise top - Content array_edge(variable_t i) { - if (is_bottom()) - return make_content_bottom(); - if (is_top() || !is_landmark(i)) - return make_content_top(); - - mut_val_ref_t wi; - if (_g.lookup_edge(landmark_ref_t(i), get_landmark_prime(i), &wi)) - return wi.get(); - else - return make_content_top(); - } - - // Remove v from the edge (i,i') - void array_edge_forget(variable_t i, variable_t v) { - if (is_bottom()) - return; - - if (!is_landmark(i)) - return; - - mut_val_ref_t wi; - landmark_ref_t lm_i(i); - landmark_ref_t lm_i_prime = get_landmark_prime(i); - if (_g.lookup_edge(lm_i, lm_i_prime, &wi)) { - Content w = wi.get(); - w -= v; - // XXX: update_edge closes the array graph - _g.update_edge(lm_i, w, lm_i_prime); - } - } - - // Remove v from all vertices and edges - void array_forget(variable_t v) { - if (is_bottom()) - return; - if (!is_landmark(v)) - return; - - _g -= landmark_ref_t(v); - _g.remove_from_weights(v); - } - - // Update the weight from the edge (i, i') - void array_edge_update(variable_t i, Content w) { - if (is_bottom()) - return; - - //--- strong update - if (!is_landmark(i)) - return; - - landmark_ref_t lm_i(i); - landmark_ref_t lm_i_prime = get_landmark_prime(i); - - _g.update_edge(lm_i, w, lm_i_prime); - mut_val_ref_t wi; - if (!_g.lookup_edge(lm_i, lm_i_prime, &wi)) - return; - - //--- weak update - // An edge (p,q) must be weakened if p <= i <= q and p < q - solver_wrapper solve(_scalar); - mut_val_ref_t w_pq; - for (auto p : _g.verts()) { - for (auto e : _g.e_succs(p)) { - auto q = e.vert; - if ((p == lm_i) && (q == lm_i_prime)) - continue; - if (_g.lookup_edge(p, q, &w_pq) && w_pq.get().is_bottom()) - continue; - // we know already that p < q in the array graph - - // check p <= i - if (solve.is_unsat(make_leq_cst(p, lm_i))) - continue; - // check i' <= q - if (solve.is_unsat(make_leq_cst(lm_i_prime, q))) - continue; - - w_pq = w_pq.get() | wi.get(); - } - } - } - - // x := x op k - template - void apply_one_variable(arith_operation_t op, variable_t x, VarOrNum k) { - if (is_bottom()) - return; - - if (!is_landmark(x)) { - // If x is not a landmark we just apply the operation on the - // scalar domain and return. - apply_only_scalar(op, x, x, k); - return; - } - - landmark_ref_t lm_x(x); - landmark_ref_t lm_x_prime = get_landmark_prime(x); - - /// --- Add x_old and x_old' to store old values of x and x' - - auto &vfac = const_cast(&(x.name()))->get_var_factory(); - variable_t x_old(vfac.get()); - variable_t x_old_prime(vfac.get()); - landmark_ref_t lm_x_old(x_old); - landmark_ref_t lm_x_old_prime(x_old_prime, x_old.name().str()); - s_var_landmarks.insert(std::make_pair(lm_x_old, lm_x_old_prime)); - // x_old = x - _scalar.assign(x_old, x); - // relation between x_old and x' - _scalar += make_prime_relation(lm_x_old_prime, lm_x_old); - //_scalar += make_eq_cst(lm_x_old_prime, lm_x_prime); - - /*** Incremental graph reduction ***/ - //// x_old has all the x predecessors and successors - _g.expand(lm_x, lm_x_old); - //// x_old' has all the x' predecessors and successors - _g.expand(lm_x_prime, lm_x_old_prime); - //// edges between x and x_old - _g.update_edge(lm_x, make_content_bottom(), lm_x_old); - _g.update_edge(lm_x_old, make_content_bottom(), lm_x); - //// edges between x' and x_old' - _g.update_edge(lm_x_prime, make_content_bottom(), lm_x_old_prime); - _g.update_edge(lm_x_old_prime, make_content_bottom(), lm_x_prime); - //// edges between x_old and x_old' - mut_val_ref_t w; - if (_g.lookup_edge(lm_x, lm_x_prime, &w)) - _g.update_edge(lm_x_old, w.get(), lm_x_old_prime); - _g.update_edge(lm_x_old_prime, make_content_bottom(), lm_x_old); - - /// --- Remove x and x' - _g -= lm_x; - _g -= lm_x_prime; - - /// --- Perform operation in the scalar domain - _scalar.apply(op, x, x, k); - - // restore relation between x and x' - _scalar.apply(OP_ADDITION, get_var(lm_x_prime), x, 1); - //_scalar -= get_var(lm_x_prime); - //_scalar += make_prime_relation(lm_x_prime, lm_x); - - if (!reduce(_scalar, _g)) { // FIXME: incremental version - set_to_bottom(); - return; - } - - /// --- Remove x_old and x_old' - _g -= lm_x_old; - _g -= lm_x_old_prime; - _scalar -= x_old; - _scalar -= x_old_prime; - s_var_landmarks.erase(lm_x_old); - } - - // remove v' from scalar and array graph - void forget_prime_var(variable_t v) { - if (!is_landmark(v)) - return; - - landmark_ref_t lm_v_prime = get_landmark_prime(v); - _scalar -= get_var(lm_v_prime); - // XXX: v' cannot appear in the array weights so we do not - // need to call array_forget. - _g -= lm_v_prime; - } - - // perform the operation in the scalar domain assuming that - // nothing can be done in the graph domain. - template - void apply_only_scalar(Op op, variable_t x, variable_t y, K k) { - _scalar.apply(op, x, y, k); - - // Abstract x in the array graph - if (is_landmark(x)) { - array_forget(x); // remove x from the array graph - forget_prime_var(x); // remove x' from scalar and array graph - /// XXX: I think no need to reduce here - } - } - - // return a pair with the normalized offset and a bool that is - // true if a new landmark was added in the array graph - std::pair normalize_offset(variable_t o, ikos::z_number n) { - CRAB_LOG("array-sgraph-norm", crab::outs() - << "BEFORE NORMALIZE OFFSET: expressions=" - << _expressions << "\n"); - - // --- create a fresh variable no such that no := o; - auto &vfac = const_cast(&(o.name()))->get_var_factory(); - variable_t no(vfac.get()); - _expressions.assign(no, o); - - // -- apply no := no / n; in the expressions domain - _expressions.apply(arith_operation_t::OP_SDIV, no, no, n); - - // -- simplify the expression domain - bool simp_done = _expressions.simplify(no); - - CRAB_LOG("array-sgraph-norm", crab::outs() - << "AFTER NORMALIZE OFFSET: expressions=" - << _expressions << "\n"); - - if (!simp_done) { - CRAB_LOG( - "array-sgraph-norm", - crab::outs() - << "NO NORMALIZATION done using the expression abstraction\n"); - - // cleanup of the expression abstraction - _expressions -= no; - - bool added_lm = false; - if (!is_landmark(o)) { - add_landmark(o); - added_lm = true; - } - - return std::make_pair(o, added_lm); - } - - CRAB_LOG("array-sgraph-norm", - crab::outs() - << "NORMALIZATION DONE! using the expression abstraction\n"); - - // -- propagate equalities from _expressions to _scalar - linear_constraint_system_t e_csts; - reduced_domain_traits::extract( - _expressions, no, e_csts, /*only_equalities=*/false); - _scalar += e_csts; - - // -- add landmark for the new array index - add_landmark(no); - - // cleanup of the expression abstraction - _expressions -= no; - - return std::make_pair(no, true); - } - - // T1 and T2 are either variable_t or z_number - template - void array_init(variable_t arr, T1 src, T2 dst, linear_expression_t val) { - if (!is_landmark(src)) { - crab::outs() << "WARNING no landmark found for " << src << "\n"; - return; - } - - if (!is_landmark(dst)) { - crab::outs() << "WARNING no landmark found for " << dst << "\n"; - return; - } - - landmark_ref_t lm_src(src); - landmark_ref_t lm_dst(dst); - - Content w; // top - array_graph_impl::propagate_between_weight_and_scalar( - _scalar, val, arr.get_type(), w, arr); - _g.update_edge(lm_src, w, lm_dst); - } - - interval_t to_interval(linear_expression_t expr) { - interval_t r(expr.constant()); - for (typename linear_expression_t::iterator it = expr.begin(); - it != expr.end(); ++it) { - interval_t c(it->first); - r += c * _scalar[it->second]; - } - return r; - } - - // Perform the operation in the scalar (optionally expression) - // domain and reduce. - // - // NOTE: if the assignment is something like i = i + k then we - // will lose precision in the array graph. This kind of - // assignments should be managed by the apply methods instead. - void assign(variable_t x, linear_expression_t e, bool update_expressions) { - crab::CrabStats::count(domain_name() + ".count.assign"); - crab::ScopedCrabStats __st__(domain_name() + ".assign"); - - if (is_bottom()) - return; - - if (auto y = e.get_variable()) { - // skip x:=x - if ((*y) == x) - return; - } - - _scalar.assign(x, e); - if (update_expressions) - _expressions.assign(x, e); - - if (is_landmark(x)) { - array_forget(x); - // remove x' from scalar and array graph - forget_prime_var(x); - // restore the relationship between x and x' - _scalar.apply(OP_ADDITION, get_var(get_landmark_prime(x)), x, 1); - // XXX: is it needed ?? - //_g.close_edge(landmark_ref_t(x), get_landmark_prime(x)); - } - - if (!reduce(_scalar, _g)) { // FIXME: incremental version - set_to_bottom(); - return; - } - - CRAB_LOG("array-sgraph", crab::outs() << "Assign " << x << " := " << e - << " ==> " << *this << "\n";); - } - - // The reduction consists of detecting dead segments so it is - // done only in one direction (scalar -> array graph). Note that - // whenever an edge becomes bottom closure is also happening. - // Return false if bottom is detected during the reduction. - bool reduce(NumDom &scalar, array_graph_t &g) const { - crab::CrabStats::count(domain_name() + ".count.reduce"); - crab::ScopedCrabStats __st__(domain_name() + ".reduce"); - - scalar.normalize(); - g.normalize(); - - if (scalar.is_bottom() || g.is_bottom()) - return false; - - if (!scalar.is_top()) { - std::vector active_landmarks; - get_active_landmarks(scalar, active_landmarks); - solver_wrapper solve(scalar); - for (auto lm_s : active_landmarks) - for (auto lm_d : active_landmarks) { - // XXX: we do not exploit the following facts: - // - i < i' is always sat - // - i' < i is always unsat - // - if i < j unsat then i' < j unsat. - // - if i < j' unsat then i' < j unsat. - if ((lm_s == lm_d) || solve.is_unsat(make_lt_cst(lm_s, lm_d))) { - g.update_edge(lm_s, make_content_bottom(), lm_d); - } - } - } - return (!g.is_bottom()); - } - -public: - static void clear_global_state() { - s_var_landmarks.clear(); - s_cst_landmarks.clear(); - } - - array_graph_domain_t make_top() const override { - array_graph_domain_t out(false); - return out; - } - - array_graph_domain_t make_bottom() const override { - array_graph_domain_t out(true); - return out; - } - - void set_to_top() override { - _scalar.set_to_top(); - _expressions.set_to_top(); - _g.set_to_top(); - } - - void set_to_bottom() override { - _scalar.set_to_bottom(); - _expressions.set_to_bottom(); - _g.set_to_bottom(); - } - - array_graph_domain(bool is_bottom = false) { - if (is_bottom) { - set_to_bottom(); - } else { - set_to_top(); - } - } - - array_graph_domain(const NumDom &s, const expression_domain_t &e, - const array_graph_t &g) - : _scalar(s), _expressions(e), _g(g) { - if (_scalar.is_bottom() || _expressions.is_bottom() || _g.is_bottom()) - set_to_bottom(); - } - - array_graph_domain(NumDom &&s, expression_domain_t &&e, array_graph_t &&g) - : _scalar(std::move(s)), _expressions(std::move(e)), _g(std::move(g)) { - if (_scalar.is_bottom() || _expressions.is_bottom() || _g.is_bottom()) - set_to_bottom(); - } - - array_graph_domain(const array_graph_domain_t &o) - : _scalar(o._scalar), _expressions(o._expressions), _g(o._g) { - crab::CrabStats::count(domain_name() + ".count.copy"); - crab::ScopedCrabStats __st__(domain_name() + ".copy"); - } - - array_graph_domain(array_graph_domain_t &&o) - : _scalar(std::move(o._scalar)), _expressions(std::move(o._expressions)), - _g(std::move(o._g)) {} - - array_graph_domain_t &operator=(const array_graph_domain_t &o) { - crab::CrabStats::count(domain_name() + ".count.copy"); - crab::ScopedCrabStats __st__(domain_name() + ".copy"); - if (this != &o) { - _scalar = o._scalar; - _expressions = o._expressions; - _g = o._g; - } - return *this; - } - - array_graph_domain_t &operator=(array_graph_domain_t &&o) { - _scalar = std::move(o._scalar); - _expressions = std::move(o._expressions); - _g = std::move(o._g); - return *this; - } - - bool is_top() const override { - return _scalar.is_top() && _expressions.is_top() && _g.is_top(); - } - - bool is_bottom() const override { - return _scalar.is_bottom() || _expressions.is_bottom() || _g.is_bottom(); - } - - bool operator<=(const array_graph_domain_t &o) const override { - crab::CrabStats::count(domain_name() + ".count.leq"); - crab::ScopedCrabStats __st__(domain_name() + ".leq"); - - CRAB_LOG("array-sgraph", array_graph_domain_t left(*this); - array_graph_domain_t right(o); - crab::outs() << "Leq " << left << " and\n" - << right << "=\n";); - bool res = (_scalar <= o._scalar) && (_expressions <= o._expressions) && - (_g <= o._g); - CRAB_LOG("array-sgraph", crab::outs() << res << "\n";); - return res; - } - - void operator|=(const array_graph_domain_t &o) override { - *this = (*this | o); - } - - array_graph_domain_t operator|(const array_graph_domain_t &o) const override { - crab::CrabStats::count(domain_name() + ".count.join"); - crab::ScopedCrabStats __st__(domain_name() + ".join"); - - CRAB_LOG("array-sgraph", crab::outs() - << "Join " << *this << " and " << o << "=\n"); - array_graph_domain_t join(_scalar | o._scalar, - _expressions | o._expressions, _g | o._g); - CRAB_LOG("array-sgraph", crab::outs() << join << "\n";); - return join; - } - - array_graph_domain_t widening_thresholds( - const array_graph_domain_t &o, - const iterators::thresholds &ts) const override { - crab::CrabStats::count(domain_name() + ".count.widening"); - crab::ScopedCrabStats __st__(domain_name() + ".widening"); - - CRAB_LOG("array-sgraph", crab::outs() << "Widening (w/ thresholds) " - << *this << " and " << o << "=\n";); - auto widen_scalar(_scalar.widening_thresholds(o._scalar, ts)); - auto widen_expr(_expressions.widening_thresholds(o._expressions, ts)); - auto widen_g(_g.widening_thresholds(o._g, ts)); - if (!reduce(widen_scalar, widen_g)) { - CRAB_LOG("array-sgraph", crab::outs() << "_|_\n";); - return make_bottom(); - } else { - array_graph_domain_t widen(widen_scalar, widen_expr, widen_g); - CRAB_LOG("array-sgraph", crab::outs() << widen << "\n";); - return widen; - } - } - - array_graph_domain_t - operator||(const array_graph_domain_t &o) const override { - crab::CrabStats::count(domain_name() + ".count.widening"); - crab::ScopedCrabStats __st__(domain_name() + ".widening"); - - CRAB_LOG("array-sgraph", - crab::outs() << "Widening " << *this << " and " << o << "=\n"); - auto widen_scalar(_scalar || o._scalar); - auto widen_expr(_expressions || o._expressions); - auto widen_g(_g || o._g); - if (!reduce(widen_scalar, widen_g)) { - CRAB_LOG("array-sgraph", crab::outs() << "_|_\n";); - return make_bottom(); - } else { - array_graph_domain_t widen(widen_scalar, widen_expr, widen_g); - CRAB_LOG("array-sgraph", crab::outs() << widen << "\n";); - return widen; - } - } - - array_graph_domain_t operator&(const array_graph_domain_t &o) const override { - crab::CrabStats::count(domain_name() + ".count.meet"); - crab::ScopedCrabStats __st__(domain_name() + ".meet"); - - CRAB_LOG("array-sgraph", crab::outs() - << "Meet " << *this << " and " << o << "=\n"); - auto meet_scalar(_scalar & o._scalar); - auto meet_expr(_expressions & o._expressions); - auto meet_g(_g & o._g); - if (!reduce(meet_scalar, meet_g)) { - CRAB_LOG("array-sgraph", crab::outs() << "_|_\n";); - return make_bottom(); - } else { - array_graph_domain_t meet(meet_scalar, meet_expr, meet_g); - CRAB_LOG("array-sgraph", crab::outs() << meet << "\n";); - return meet; - } - } - - array_graph_domain_t - operator&&(const array_graph_domain_t &o) const override { - crab::CrabStats::count(domain_name() + ".count.narrowing"); - crab::ScopedCrabStats __st__(domain_name() + ".narrowing"); - - CRAB_LOG("array-sgraph", - crab::outs() << "Narrowing " << *this << " and " << o << "=\n"); - auto narrow_scalar(_scalar && o._scalar); - auto narrow_expr(_expressions && o._expressions); - auto narrow_g(_g && o._g); - if (!reduce(narrow_scalar, narrow_g)) { - CRAB_LOG("array-sgraph", crab::outs() << "_|_\n";); - return make_bottom(); - } else { - array_graph_domain_t narrow(narrow_scalar, narrow_expr, narrow_g); - CRAB_LOG("array-sgraph", crab::outs() << narrow << "\n";); - return narrow; - } - } - - void operator-=(const variable_t &v) override { - crab::CrabStats::count(domain_name() + ".count.forget"); - crab::ScopedCrabStats __st__(domain_name() + ".forget"); - - if (is_bottom()) - return; - - // remove v from scalar and array graph - _scalar -= v; - // remove v from expressions - _expressions -= v; - - if (is_landmark(v)) { - array_forget(v); - // remove v' from scalar and array graph - forget_prime_var(v); - } - } - - void project(const variable_vector_t &variables) override { - crab::CrabStats::count(domain_name() + ".count.project"); - crab::ScopedCrabStats __st__(domain_name() + ".project"); - - if (is_bottom() || is_top()) { - return; - } - if (variables.empty()) { - set_to_top(); - return; - } - - std::set keep_vars(variables.begin(), variables.end()); - std::vector active_vars; - _scalar.active_variables(active_vars); - for (auto v : active_vars) { - if (!keep_vars.count(v)) { - array_forget(v); - forget_prime_var(v); - } - } - - _scalar.project(variables); - _expressions.project(variables); - } - - void forget(const variable_vector_t &variables) override { - if (is_bottom() || is_top()) { - return; - } - for (variable_t v : variables) { - this->operator-=(v); - } - } - - void expand(const variable_t &var, const variable_t &new_var) override { - CRAB_WARN("array_graph_domain expand not implemented"); - } - - void normalize() override { - CRAB_WARN("array_graph_domain normalize not implemented"); - } - - void minimize() override { - _scalar.minimize(); - _expressions.minimize(); - } - - /* begin intrinsics operations */ - void intrinsic(std::string name, - const variable_or_constant_vector_t &inputs, - const variable_vector_t &outputs) override { - CRAB_WARN("Intrinsics ", name, " not implemented by ", domain_name()); - } - - void backward_intrinsic(std::string name, - const variable_or_constant_vector_t &inputs, - const variable_vector_t &outputs, - const array_graph_domain_t &invariant) override { - CRAB_WARN("Intrinsics ", name, " not implemented by ", domain_name()); - } - /* end intrinsics operations */ - - void rename(const variable_vector_t &from, - const variable_vector_t &to) override { - crab::CrabStats::count(domain_name() + ".count.rename"); - crab::ScopedCrabStats __st__(domain_name() + ".rename"); - - assert(from.size() == to.size()); - - if (is_top() || is_bottom()) - return; - - CRAB_WARN(domain_name(), "::rename not implemented"); - } - - void operator+=(const linear_constraint_system_t &csts) override { - crab::CrabStats::count(domain_name() + ".count.add_constraints"); - crab::ScopedCrabStats __st__(domain_name() + ".add_constraints"); - - if (is_bottom()) - return; - - _scalar += csts; - _expressions += csts; - - if (!reduce(_scalar, _g)) { // FIXME: incremental version - set_to_bottom(); - return; - } - CRAB_LOG("array-sgraph", - crab::outs() << "Assume(" << csts << ") --- " << *this << "\n";); - } - - void assign(const variable_t &x, const linear_expression_t &e) override { - assign(x, e, true); - } - - void apply(arith_operation_t op, const variable_t &x, const variable_t &y, - number_t z) override { - if (x == y) { - crab::CrabStats::count(domain_name() + ".count.apply"); - crab::ScopedCrabStats __st__(domain_name() + ".apply"); - _expressions.apply(op, x, y, z); - apply_one_variable(op, x, z); - CRAB_LOG("array-sgraph", crab::outs() - << "Apply " << x << " := " << y << " " << op - << " " << z << " ==> " << *this << "\n";); - } else { - switch (op) { - case OP_ADDITION: - assign(x, y + z); - break; - case OP_SUBTRACTION: - assign(x, y - z); - break; - case OP_MULTIPLICATION: - assign(x, y * z); - break; - default: - CRAB_WARN(op, "not implemented in array-sgraph\n"); - } - } - } - - void apply(arith_operation_t op, const variable_t &x, const variable_t &y, - const variable_t &z) override { - if (x == y) { - crab::CrabStats::count(domain_name() + ".count.apply"); - crab::ScopedCrabStats __st__(domain_name() + ".apply"); - _expressions.apply(op, x, y, z); - apply_one_variable(op, x, z); - CRAB_LOG("array-sgraph", crab::outs() - << "Apply " << x << " := " << y << " " << op - << " " << z << " ==> " << *this << "\n";); - } else { - switch (op) { - case OP_ADDITION: - assign(x, y + z); - break; - case OP_SUBTRACTION: - assign(x, y - z); - break; - default: - CRAB_WARN(op, "not implemented in array-sgraph"); - } - } - } - // backward arithmetic operations - - void backward_assign(const variable_t &x, const linear_expression_t &e, - const array_graph_domain_t &invariant) override { - operator-=(x); - CRAB_WARN("backward assign not implemented"); - } - - void backward_apply(arith_operation_t op, const variable_t &x, - const variable_t &y, number_t z, - const array_graph_domain_t &invariant) override { - operator-=(x); - CRAB_WARN("backward apply not implemented"); - } - - void backward_apply(arith_operation_t op, const variable_t &x, - const variable_t &y, const variable_t &z, - const array_graph_domain_t &invariant) override { - - operator-=(x); - CRAB_WARN("backward apply not implemented"); - } - - // boolean operations - void assign_bool_cst(const variable_t &lhs, - const linear_constraint_t &rhs) override { - operator-=(lhs); - CRAB_WARN("assign_bool_cst not implemented in array-sgraph"); - } - - void assign_bool_ref_cst(const variable_t &lhs, - const reference_constraint_t &rhs) override { - operator-=(lhs); - CRAB_WARN("assign_bool_cst not implemented in array-sgraph"); - } - - void assign_bool_var(const variable_t &lhs, const variable_t &rhs, - bool is_not_rhs) override { - operator-=(lhs); - CRAB_WARN("assign_bool_var not implemented in array-sgraph"); - } - - void apply_binary_bool(bool_operation_t op, const variable_t &x, - const variable_t &y, const variable_t &z) override { - - operator-=(x); - CRAB_WARN("apply_binary_bool not implemented in array-sgraph"); - } - - void assume_bool(const variable_t &v, bool is_negated) override { - CRAB_WARN("assume_bool not implemented in array-sgraph"); - } - - // backward boolean operations - void - backward_assign_bool_cst(const variable_t &lhs, - const linear_constraint_t &rhs, - const array_graph_domain_t &invariant) override { - operator-=(lhs); - CRAB_WARN("backward_assign_bool_cst not implemented in array-sgraph"); - } - - void - backward_assign_bool_ref_cst(const variable_t &lhs, - const reference_constraint_t &rhs, - const array_graph_domain_t &invariant) override { - operator-=(lhs); - CRAB_WARN("backward_assign_bool_cst not implemented in array-sgraph"); - } - - void - backward_assign_bool_var(const variable_t &lhs, const variable_t &rhs, - bool is_not_rhs, - const array_graph_domain_t &invariant) override { - operator-=(lhs); - CRAB_WARN("backward_assign_bool_var not implemented in array-sgraph"); - } - - void - backward_apply_binary_bool(bool_operation_t op, const variable_t &x, - const variable_t &y, const variable_t &z, - const array_graph_domain_t &invariant) override { - operator-=(x); - CRAB_WARN("backward_apply_binary_bool not implemented in array-sgraph"); - } - - // cast operations - - void apply(int_conv_operation_t op, const variable_t &dst, - const variable_t &src) override { - _expressions.apply(op, dst, src); - // assume unlimited precision so widths are ignored. - assign(dst, src, false); - } - - // bitwise operations - - void apply(bitwise_operation_t op, const variable_t &x, const variable_t &y, - const variable_t &z) override { - crab::CrabStats::count(domain_name() + ".count.apply"); - crab::ScopedCrabStats __st__(domain_name() + ".apply"); - - _expressions.apply(op, x, y, z); - // XXX: we give up soundly in the graph domain - apply_only_scalar(op, x, y, z); - } - - void apply(bitwise_operation_t op, const variable_t &x, const variable_t &y, - number_t k) override { - crab::CrabStats::count(domain_name() + ".count.apply"); - crab::ScopedCrabStats __st__(domain_name() + ".apply"); - - _expressions.apply(op, x, y, k); - // XXX: we give up soundly in the graph domain - apply_only_scalar(op, x, y, k); - } - - DEFAULT_SELECT(array_graph_domain_t) - DEFAULT_SELECT_BOOL(array_graph_domain_t) - - virtual interval_t operator[](const variable_t &v) override { - return _scalar[v]; - } - - virtual interval_t at(const variable_t &v) const override { - return _scalar.at(v); - } - - /// array_graph is a functor domain that implements all operations - /// except region/reference operations. - REGION_AND_REFERENCE_OPERATIONS_NOT_IMPLEMENTED(array_graph_domain_t) - - // array_operators_api - - virtual void array_init(const variable_t &a, - const linear_expression_t & /*elem_size*/, - const linear_expression_t &lb_idx, - const linear_expression_t &ub_idx, - const linear_expression_t &val) override { - - auto lb_var_opt = lb_idx.get_variable(); - auto ub_var_opt = ub_idx.get_variable(); - - if (lb_idx.is_constant() && ub_idx.is_constant()) - array_init(a, lb_idx.constant(), ub_idx.constant(), val); - else if (lb_idx.is_constant() && ub_var_opt) - array_init(a, lb_idx.constant(), *ub_var_opt, val); - else if (lb_var_opt && ub_idx.is_constant()) - array_init(a, *lb_var_opt, ub_idx.constant(), val); - else if (lb_var_opt && ub_var_opt) - array_init(a, *lb_var_opt, *ub_var_opt, val); - else - CRAB_ERROR("unreachable"); - } - - virtual void array_load(const variable_t &lhs, const variable_t &a, - const linear_expression_t &elem_size, - const linear_expression_t &i) override { - crab::CrabStats::count(domain_name() + ".count.load"); - crab::ScopedCrabStats __st__(domain_name() + ".load"); - - auto vi = i.get_variable(); - if (!vi) { - CRAB_WARN("TODO: array load index must be a variable"); - return; - } - - // -- normalization ensures that closure and reduction have - // -- been applied. - interval_t i_elem_size = to_interval(elem_size); - boost::optional n_elem_size = i_elem_size.singleton(); - if (!n_elem_size) { - CRAB_WARN("array_graph ignored array load because element size is not " - "constant"); - return; - } - assert(static_cast(*n_elem_size) > 0 && - static_cast(*n_elem_size) <= - std::numeric_limits::max()); - int64_t num_bytes = static_cast(*n_elem_size); - auto p = normalize_offset(*vi, num_bytes); - variable_t norm_idx = p.first; - - // #if 0 - // if (is_landmark(norm_idx)) { - // landmark_ref_t lm_norm_idx(norm_idx); - // landmark_ref_t lm_norm_idx_prime = get_landmark_prime(norm_idx); - - // _g.close_edge(lm_norm_idx, lm_norm_idx_prime); - // crab::outs() << "#### 1 " << _g << "\n"; - - // Content w; - // w += linear_constraint_t(linear_expression_t(lhs) == - // linear_expression_t(a)); crab::outs() << "#### 2 " << w << "\n"; - // //_g.update_edge_unclosed(lm_norm_idx, w, lm_norm_idx_prime); - // _g.update_edge(lm_norm_idx, w, lm_norm_idx_prime); - // } - // #endif - - Content w = array_edge(norm_idx); - - if (a.get_type().is_integer_array() || a.get_type().is_real_array()) { - // Only non-relational numerical invariants are - // propagated from the graph domain to the expressions domain. - _expressions.set(lhs, w[a]); - } - - array_graph_impl::propagate_between_weight_and_scalar(w, a, a.get_type(), - _scalar, lhs); - - // if normalize_offset created a landmark we remove it here to - // keep smaller array graph - if (p.second) - remove_landmark(norm_idx); - - /// XXX: due to the above simplification we need to reduce - /// only if the content of an array cell can be an index. - if (is_landmark(lhs)) - if (!reduce(_scalar, _g)) // FIXME: incremental version - set_to_bottom(); - - CRAB_LOG("array-sgraph", crab::outs() - << "Array read " << lhs << " := " << a << "[" - << i << "] ==> " << *this << "\n";); - } - - virtual void array_store(const variable_t &a, - const linear_expression_t &elem_size, - const linear_expression_t &i, - const linear_expression_t &val, - bool /*is_strong_update*/) override { - crab::CrabStats::count(domain_name() + ".count.store"); - crab::ScopedCrabStats __st__(domain_name() + ".store"); - - auto vi = i.get_variable(); - if (!vi) { - CRAB_WARN("TODO: array store index must be a variable"); - return; - } - - Content w; // top - array_graph_impl::propagate_between_weight_and_scalar(_scalar, val, - a.get_type(), w, a); - - interval_t i_elem_size = to_interval(elem_size); - boost::optional n_elem_size = i_elem_size.singleton(); - if (!n_elem_size) { - CRAB_WARN("array_graph ignored array store because element size is not " - "constant"); - return; - } - assert(static_cast(*n_elem_size) > 0 && - static_cast(*n_elem_size) <= - std::numeric_limits::max()); - int64_t num_bytes = static_cast(*n_elem_size); - auto p = normalize_offset(*vi, num_bytes); - variable_t norm_idx = p.first; - - array_edge_forget(norm_idx, a); - array_edge_update(norm_idx, w); - - // XXX: since we do not propagate from the array weights to - // the scalar domain I think we don't need to reduce here. - - CRAB_LOG("array-sgraph", crab::outs() << "Array write " << a << "[" << i - << "] := " << val << " ==> " << *this - << "\n";); - } - - virtual void array_store_range(const variable_t &a, - const linear_expression_t &elem_size, - const linear_expression_t &i, - const linear_expression_t &j, - const linear_expression_t &val) override { - CRAB_WARN("array_store_range in array_graph not implemented"); - } - - virtual void array_assign(const variable_t &lhs, - const variable_t &rhs) override { - CRAB_WARN("array_assign in array_graph not implemented"); - } - - // backward array operations - void backward_array_init(const variable_t &a, - const linear_expression_t &elem_size, - const linear_expression_t &lb_idx, - const linear_expression_t &ub_idx, - const linear_expression_t &val, - const array_graph_domain_t &invariant) override { - CRAB_WARN("backward_array_init in array_graph domain not implemented"); - } - void backward_array_load(const variable_t &lhs, const variable_t &a, - const linear_expression_t &elem_size, - const linear_expression_t &i, - const array_graph_domain_t &invariant) override { - CRAB_WARN("backward_array_load in array_graph domain not implemented"); - this->operator-=(lhs); - } - void backward_array_store(const variable_t &a, - const linear_expression_t &elem_size, - const linear_expression_t &i, - const linear_expression_t &v, bool is_strong_update, - const array_graph_domain_t &invariant) override { - CRAB_WARN("backward_array_store in array_graph domain not implemented"); - } - void backward_array_store_range( - const variable_t &a, const linear_expression_t &elem_size, - const linear_expression_t &i, const linear_expression_t &j, - const linear_expression_t &v, - const array_graph_domain_t &invariant) override { - CRAB_WARN( - "backward_array_store_range in array_graph domain not implemented"); - } - void backward_array_assign(const variable_t &lhs, const variable_t &rhs, - const array_graph_domain_t &invariant) override { - CRAB_WARN("backward_array_assign in array_graph domain not implemented"); - } - - void write(crab_os &o) const override { - NumDom copy_scalar(_scalar); - array_graph_t copy_g(_g); - // Remove all primed variables for pretty printing - for (auto lm : var_lm_primes()) { - copy_scalar -= get_var(lm); - copy_g -= lm; - } - for (auto lm : cst_lm_primes()) { - copy_scalar -= get_var(lm); - copy_g -= lm; - } - o << "(" << copy_scalar << ","; - array_graph_t::write(o, copy_g, false); // we do not print bottom edges - o << ")"; - // o << "##" << _expressions; - - CRAB_LOG("array-sgraph-print", o << "\n(" - << "S=" << _scalar << "," - << "E=" << _expressions << "," - << "G=" << _g << ")";); - } - - // XXX: the array domain is disjunctive so it is not really - // useful to express it through a conjunction of linear - // constraints - linear_constraint_system_t to_linear_constraint_system() const override { - CRAB_ERROR("array-sgraph does not implement to_linear_constraint_system"); - } - - disjunctive_linear_constraint_system_t - to_disjunctive_linear_constraint_system() const override { - CRAB_ERROR("TODO: array-sgraph does not implement " - "to_disjunctive_linear_constraint_system"); - } - - std::string domain_name() const override { - Content content; - std::string name("ArrayGraph(" + _scalar.domain_name() + "," + - content.domain_name() + ")"); - return name; - } -}; - -template -struct abstract_domain_traits> { - // assume Dom::variable_t = Content::variable_t - using number_t = typename Dom::number_t; - using varname_t = typename Dom::varname_t; -}; - -template -class special_domain_traits> { -public: - static void clear_global_state(void) { - array_graph_domain::clear_global_state(); - } -}; - -// Static data allocation -template -landmark_ref_unordered_map< - typename Dom::variable_t, typename Dom::number_t, - landmark_ref> - array_graph_domain::s_var_landmarks; - -template -landmark_ref_unordered_map< - typename Dom::variable_t, typename Dom::number_t, - landmark_ref> - array_graph_domain::s_cst_landmarks; - -} // end namespace domains -} // end namespace crab -#pragma GCC diagnostic pop diff --git a/include/crab/domains/array_graph/array_segmentation.hpp b/include/crab/domains/array_graph/array_segmentation.hpp deleted file mode 100644 index a6778bf1..00000000 --- a/include/crab/domains/array_graph/array_segmentation.hpp +++ /dev/null @@ -1,285 +0,0 @@ -#pragma once - -/* - Quick analysis to collect the set of variables and constants that might - define array segment boundaries. -*/ - -#include -#include -#include -#include -#include - -#include -#include - -namespace crab { - -namespace analyzer { - -template -class array_segment_ops - : public crab::iterators::killgen_operations_api< - CFG, ikos::discrete_domain> { - - using killgen_operations_api_t = crab::iterators::killgen_operations_api< - CFG, ikos::discrete_domain>; - -public: - using basic_block_label_t = typename CFG::basic_block_label_t; - using N = typename CFG::number_t; - using V = typename CFG::varname_t; - using variable_t = typename CFG::variable_t; - using array_segment_domain_t = - typename killgen_operations_api_t::killgen_domain_t; - -private: - class array_segment_visitor - : public crab::cfg::statement_visitor { - using bin_op_t = typename crab::cfg::statement_visitor::bin_op_t; - using assign_t = typename crab::cfg::statement_visitor::assign_t; - using assume_t = typename crab::cfg::statement_visitor::assume_t; - using select_t = typename crab::cfg::statement_visitor::select_t; - using assert_t = typename crab::cfg::statement_visitor::assert_t; - - using havoc_t = typename crab::cfg::statement_visitor::havoc_t; - using unreach_t = typename crab::cfg::statement_visitor::unreach_t; - using callsite_t = - typename crab::cfg::statement_visitor::callsite_t; - - using arr_init_t = - typename crab::cfg::statement_visitor::arr_init_t; - using arr_load_t = - typename crab::cfg::statement_visitor::arr_load_t; - typedef typename crab::cfg::statement_visitor::arr_store_t arr_store_t; - - // assume all statements have the same type expression_t; - using linear_expression_t = typename bin_op_t::linear_expression_t; - using linear_constraint_t = typename assume_t::linear_constraint_t; - - array_segment_domain_t get_variables(const linear_expression_t &e) const { - array_segment_domain_t res; - for (auto const &v : e.variables()) - res += v; - return res; - } - - array_segment_domain_t get_variables(const linear_constraint_t &c) const { - array_segment_domain_t res; - for (auto const &v : c.variables()) - res += v; - return res; - } - - public: - array_segment_domain_t m_indexes; - - array_segment_visitor(array_segment_domain_t inv) : m_indexes(inv) {} - - void visit(bin_op_t &s) { - if (!(m_indexes & s.lhs()).is_bottom()) { - m_indexes += get_variables(s.left()); - m_indexes += get_variables(s.right()); - } - } - - void visit(assign_t &s) { - if (!(m_indexes & s.lhs()).is_bottom()) { - m_indexes += get_variables(s.rhs()); - } - } - - void visit(assume_t &s) { - auto vars = get_variables(s.constraint()); - if (!(m_indexes & vars).is_bottom()) - m_indexes += vars; - } - - void visit(arr_init_t &s) { - m_indexes += get_variables(s.lb_index()); - m_indexes += get_variables(s.ub_index()); - } - - void visit(arr_load_t &s) { m_indexes += get_variables(s.index()); } - - void visit(arr_store_t &s) { - m_indexes += get_variables(s.lb_index()); - m_indexes += get_variables(s.ub_index()); - } - - void visit(unreach_t &) {} - - // FIXME: implement these - void visit(select_t &) {} - void visit(callsite_t &) {} - void visit(havoc_t &) {} - void visit(assert_t &) {} - }; - -public: - array_segment_ops(CFG cfg) : killgen_operations_api_t(cfg) {} - - virtual bool is_forward() override { return false; } - - virtual std::string name() override { return "array_segment"; } - - virtual void init_fixpoint() override {} - - virtual array_segment_domain_t entry() override { - return array_segment_domain_t::bottom(); - } - - virtual array_segment_domain_t merge(array_segment_domain_t d1, - array_segment_domain_t d2) override { - return d1 | d2; - } - - virtual array_segment_domain_t analyze(const basic_block_label_t &bb_id, - array_segment_domain_t in) override { - auto &bb = this->m_cfg.get_node(bb_id); - array_segment_visitor vis(in); - for (auto &s : bb) { - s.accept(&vis); - } - return vis.m_indexes; - } -}; - -template -class array_segmentation : public crab::iterators::killgen_fixpoint_iterator< - CFG, array_segment_ops> { -public: - using array_segment_ops_t = array_segment_ops; - using basic_block_label_t = typename CFG::basic_block_label_t; - using statement_t = typename CFG::statement_t; - using varname_t = typename CFG::varname_t; - using array_segment_domain_t = - typename array_segment_ops_t::array_segment_domain_t; - -private: - using killgen_fixpoint_iterator_t = - crab::iterators::killgen_fixpoint_iterator; - using segment_map_t = - boost::unordered_map; - - segment_map_t m_segment_map; - array_segment_ops_t m_array_segment_ops; - -public: - array_segmentation(CFG cfg) - : killgen_fixpoint_iterator_t(cfg, m_array_segment_ops), - m_array_segment_ops(cfg) {} - - array_segmentation(const array_segmentation &o) = delete; - array_segmentation &operator=(const array_segmentation &o) = delete; - - void exec() { - this->run(); - - CRAB_LOG("array-segment", - crab::outs() - << "Array segment variables alive at the block entries\n";); - - for (auto p : - boost::make_iterator_range(this->in_begin(), this->in_end())) { - CRAB_LOG("array-segment", crab::outs() - << p.first << ":" << p.second << "\n";); - m_segment_map.insert(std::make_pair(p.first, p.second)); - } - this->release_memory(); - } - - array_segment_domain_t get_variables(const basic_block_label_t &bb) const { - auto it = m_segment_map.find(bb); - if (it == m_segment_map.end()) - return array_segment_domain_t(); - else - return it->second; - } - - void write(crab_os &o) const {} -}; - -// Visitor for finding constants that might appear as array -// segment boundaries. -template -class array_constant_segment_visitor - : public crab::cfg::statement_visitor { - - using BBL = typename CFG::basic_block_label_t; - using N = typename CFG::number_t; - using V = typename CFG::varname_t; - using bin_op_t = typename crab::cfg::statement_visitor::bin_op_t; - using assign_t = typename crab::cfg::statement_visitor::assign_t; - using assume_t = typename crab::cfg::statement_visitor::assume_t; - using havoc_t = typename crab::cfg::statement_visitor::havoc_t; - using unreach_t = typename crab::cfg::statement_visitor::unreach_t; - using select_t = typename crab::cfg::statement_visitor::select_t; - using callsite_t = - typename crab::cfg::statement_visitor::callsite_t; - using assert_t = typename crab::cfg::statement_visitor::assert_t; - - using arr_init_t = - typename crab::cfg::statement_visitor::arr_init_t; - using arr_load_t = - typename crab::cfg::statement_visitor::arr_load_t; - using arr_store_t = - typename crab::cfg::statement_visitor::arr_store_t; - - using linear_expression_t = typename bin_op_t::linear_expression_t; - using number_t = typename linear_expression_t::number_t; - -public: - using constant_set_t = std::vector; - -private: - ArraySegmentDom m_dom; - constant_set_t m_csts; - -public: - array_constant_segment_visitor(ArraySegmentDom dom) : m_dom(dom) {} - - constant_set_t get_constants() { return m_csts; } - - /// XXX: we focus for now only on assignments - void visit(assign_t &s) { - if (!(m_dom & s.lhs()).is_bottom()) { - if (s.rhs().is_constant() && s.rhs().constant() >= 0 && - std::find(m_csts.begin(), m_csts.end(), s.rhs().constant()) == - m_csts.end()) { - m_csts.push_back(s.rhs().constant()); - // for decrementing loops we need to include the upper bound index i and - // i+1 - m_csts.push_back(s.rhs().constant() + 1); - } - } - } - - void visit(bin_op_t &s) {} - void visit(assume_t &s) {} - void visit(arr_init_t &s) {} - void visit(arr_load_t &s) {} - void visit(arr_store_t &s) {} - void visit(select_t &) {} - void visit(callsite_t &) {} - void visit(havoc_t &) {} - void visit(assert_t &) {} - void visit(unreach_t &) {} -}; - -} // end namespace analyzer -} // end namespace crab diff --git a/include/crab/domains/split_dbm.hpp b/include/crab/domains/split_dbm.hpp index 26b7c1f2..2845f305 100644 --- a/include/crab/domains/split_dbm.hpp +++ b/include/crab/domains/split_dbm.hpp @@ -329,7 +329,7 @@ class split_dbm_domain final /* x >= lb for each {x,lb} in lbs */ std::vector> &lbs, /* x <= ub for each {x,ub} in ubs */ - std::vector> &ubs) { + std::vector> &ubs) /*const*/ { Wt unbounded_lbcoeff; Wt unbounded_ubcoeff; @@ -358,7 +358,7 @@ class split_dbm_domain final } if (coeff > Wt(0)) { variable_t y(p.second); - bound_t y_lb = operator[](y).lb(); + bound_t y_lb = at(y).lb(); if (y_lb.is_infinite()) { if (unbounded_lbvar) { return; @@ -375,7 +375,7 @@ class split_dbm_domain final } } else { variable_t y(p.second); - bound_t y_ub = operator[](y).ub(); + bound_t y_ub = at(y).ub(); if (y_ub.is_infinite()) { if (unbounded_ubvar) { return; @@ -2175,18 +2175,71 @@ class split_dbm_domain final } } - interval_t operator[](const variable_t &x) override { - crab::CrabStats::count(domain_name() + ".count.to_intervals"); - crab::ScopedCrabStats __st__(domain_name() + ".to_intervals"); +// return true iff cst is unsatisfiable without modifying the DBM + bool is_unsat(const linear_constraint_t &cst) /*const*/ { + if (is_bottom() || cst.is_contradiction()) { + return true; + } - // Needed for accuracy - normalize(); + if (is_top() || cst.is_tautology()) { + return false; + } - if (is_bottom()) { - return interval_t::bottom(); + std::vector> lbs, ubs; + std::vector diffcsts; + + if (cst.is_inequality()) { + linear_expression_t exp = cst.expression(); + diffcsts_of_lin_leq(exp, diffcsts, lbs, ubs); + } else if (cst.is_strict_inequality()) { + auto nc = + ikos::linear_constraint_impl::strict_to_non_strict_inequality(cst); + if (nc.is_inequality()) { + linear_expression_t exp = nc.expression(); + diffcsts_of_lin_leq(exp, diffcsts, lbs, ubs); + } else { + // we couldn't convert the strict into a non-strict + return false; + } + } else if (cst.is_equality()) { + linear_expression_t exp = cst.expression(); + diffcsts_of_lin_leq(exp, diffcsts, lbs, ubs); + diffcsts_of_lin_leq(-exp, diffcsts, lbs, ubs); } else { - return get_interval(vert_map, g, x); + return false; + } + + // check difference constraints + for (auto diffcst : diffcsts) { + variable_t x = diffcst.first.first; + variable_t y = diffcst.first.second; + Wt k = diffcst.second; + if (is_unsat_edge(get_vert(y), get_vert(x), k)) { + return true; + } + } + + // check interval constraints + for (auto ub : ubs) { + if (is_unsat_edge(0, get_vert(ub.first), ub.second)) { + return true; + } + } + for (auto lb : lbs) { + if (is_unsat_edge(get_vert(lb.first), 0, -lb.second)) { + return true; + } } + + return false; + } + + interval_t operator[](const variable_t &x) override { + crab::CrabStats::count(domain_name() + ".count.to_intervals"); + crab::ScopedCrabStats __st__(domain_name() + ".to_intervals"); + normalize(); + return (is_bottom() ? interval_t::bottom() : + get_interval(vert_map, g, x)); } interval_t at(const variable_t &x) const override { @@ -2576,77 +2629,6 @@ class split_dbm_domain final } std::string domain_name() const override { return "SplitDBM"; } - - // ===== begin array_graph domain - // return true iff cst is unsatisfiable without modifying the DBM - bool is_unsat(const linear_constraint_t &cst) /*const*/ { - if (is_bottom() || cst.is_contradiction()) { - return true; - } - - if (is_top() || cst.is_tautology()) { - return false; - } - - std::vector> lbs, ubs; - std::vector diffcsts; - - if (cst.is_inequality()) { - linear_expression_t exp = cst.expression(); - diffcsts_of_lin_leq(exp, diffcsts, lbs, ubs); - } else if (cst.is_strict_inequality()) { - auto nc = - ikos::linear_constraint_impl::strict_to_non_strict_inequality(cst); - if (nc.is_inequality()) { - linear_expression_t exp = nc.expression(); - diffcsts_of_lin_leq(exp, diffcsts, lbs, ubs); - } else { - // we couldn't convert the strict into a non-strict - return false; - } - } else if (cst.is_equality()) { - linear_expression_t exp = cst.expression(); - diffcsts_of_lin_leq(exp, diffcsts, lbs, ubs); - diffcsts_of_lin_leq(-exp, diffcsts, lbs, ubs); - } else { - return false; - } - - // check difference constraints - for (auto diffcst : diffcsts) { - variable_t x = diffcst.first.first; - variable_t y = diffcst.first.second; - Wt k = diffcst.second; - if (is_unsat_edge(get_vert(y), get_vert(x), k)) { - return true; - } - } - - // check interval constraints - for (auto ub : ubs) { - if (is_unsat_edge(0, get_vert(ub.first), ub.second)) { - return true; - } - } - for (auto lb : lbs) { - if (is_unsat_edge(get_vert(lb.first), 0, -lb.second)) { - return true; - } - } - - return false; - } - - void active_variables(std::vector &out) const { - out.reserve(g.size()); - for (auto v : g.verts()) { - if (rev_map[v]) { - variable_t vv = *rev_map[v]; - out.push_back(vv); - } - } - } - // ===== end array_graph domain }; // class split_dbm_domain template diff --git a/tests/crab_dom.hpp b/tests/crab_dom.hpp index 2cb2f621..d4796e1f 100644 --- a/tests/crab_dom.hpp +++ b/tests/crab_dom.hpp @@ -4,7 +4,6 @@ #include #include -#include #include #include #include @@ -78,7 +77,6 @@ using z_aa_bool_int_t = array_adaptive_domain; using z_aa_sdbm_t = array_adaptive_domain; using z_aa_box_apron_t = array_adaptive_domain; using z_aa_zones_elina_t = array_adaptive_domain; -using z_ag_sdbm_intv_t = array_graph_domain; using z_as_dis_int_t = array_smashing; using z_as_sdbm_t = array_smashing; using z_as_bool_num_t = array_smashing; diff --git a/tests/crab_inst.hpp b/tests/crab_inst.hpp index 998e52d0..270dd623 100644 --- a/tests/crab_inst.hpp +++ b/tests/crab_inst.hpp @@ -41,7 +41,6 @@ Z_RUNNER(crab::domain_impl::z_wrapped_interval_domain_t) Z_RUNNER(crab::domain_impl::z_as_dis_int_t) Z_RUNNER(crab::domain_impl::z_as_sdbm_t) Z_RUNNER(crab::domain_impl::z_as_bool_num_t) -Z_RUNNER(crab::domain_impl::z_ag_sdbm_intv_t) Z_RUNNER(crab::domain_impl::z_aa_term_int_t) Z_RUNNER(crab::domain_impl::z_aa_bool_int_t) Z_RUNNER(crab::domain_impl::z_pow_aa_int_t) diff --git a/tests/domains/array_graph.cc b/tests/domains/array_graph.cc.NOCOMPILE similarity index 100% rename from tests/domains/array_graph.cc rename to tests/domains/array_graph.cc.NOCOMPILE diff --git a/tests/expected_results.apron.out b/tests/expected_results.apron.out index 31811364..0c065371 100644 --- a/tests/expected_results.apron.out +++ b/tests/expected_results.apron.out @@ -612,103 +612,6 @@ user-defined assertion checker === End ./test-bin/array_adaptive2 === === End ./test-bin/array_expansion === -=== Begin ./test-bin/array_graph === -Program 1: forall 0<= i< 10. a[i] = 123456Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A0 -> [123456, 123456]}, [0,2)=>{A0 -> [123456, 123456]}, [0,n1)=>{A0 -> [123456, 123456]}, [0,i)=>{A0 -> [123456, 123456]}, [1,2)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,2)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 2: forall 0<= i< 10. a[i] = b[i] = x and x = 123456Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [0,2)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [0,n1)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,2)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,2)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 3: forall 0<= i< 10. a[i] = 8 and b[i] = 5Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A -> [8, 8]; B -> [5, 5]}, [0,2)=>{A -> [8, 8]; B -> [5, 5]}, [0,n1)=>{A -> [8, 8]; B -> [5, 5]}, [0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,2)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,2)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 4: forall 0<= i < n. a[i] = 123456 (unbounded loop)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [1, +oo], n -> [1, +oo], n1-i<=1, n-i<=0, i-n<=0},{[0,1)=>{A -> [123456, 123456]}, [0,n1)=>{A -> [123456, 123456]}, [0,i)=>{A -> [123456, 123456]}, [0,n)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [1,n)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [2,n)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}, [n1,n)=>{A -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=-1, n1-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 6: a[0] = 89 and for all 1<= i < n. a[i] = a[i-1]Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -bb1_f=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -ret=({n1 -> [1, 1], i -> [2, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, n-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,2)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [0,n)=>{A -> [89, 89]}, [1,2)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [1,n)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [2,n)=>{A -> [89, 89]}, [n1,2)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}, [n1,n)=>{A -> [89, 89]}}) -bb1_t=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -bb2=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=-1, n1-n<=-1},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{3} bb1_f ret - -Program 7: forall 0<= i< 10 and i % 2 = 0. a[i] = 123456Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -bb1_f=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -ret=({n1 -> [1, 1], n2 -> [2, 2], i -> [10, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -bb1_t=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -bb2=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 9], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 8: forall 0<= i < n. 1 <= a[i] <= 2Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb1_f2=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb1_f=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,1)=>{A -> [2, 2]}, [i1,i2)=>{A -> [2, 2]}, [i1,n)=>{A -> [2, 2]}, [i2,1)=>{A -> [1, 1]}, [i2,i1)=>{A -> [1, 1]}, [i2,n)=>{A -> [1, 1]}}) -ret=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,1)=>{A -> [2, 2]}, [i1,i2)=>{A -> [2, 2]}, [i1,n)=>{A -> [2, 2]}, [i2,1)=>{A -> [1, 1]}, [i2,i1)=>{A -> [1, 1]}, [i2,n)=>{A -> [1, 1]}}) -bb1_f1=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb1_t=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb2=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=-1, i2-n<=-1},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb2b=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=-1, i2-n<=-1},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb3=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], val -> [1, 2], val-i2<=1, i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,1)=>{A -> [2, 2]}, [i1,i2)=>{A -> [2, 2]}, [i2,1)=>{A -> [1, 1]}, [i2,i1)=>{A -> [1, 1]}}) -bb2a=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=-1, i2-n<=-1},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -Abstract trace: entry (bb1 bb1_t bb2 bb2b bb2a bb3)^{4} bb1_f2 bb1_f1 bb1_f ret - -Program 9: forall 0<= i < n. a[i] == 123456 (decrementing loop)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({i -> [-1, 9]},{}) -bb1_f=({i -> [-1, 9]},{}) -ret=({i -> [-1, -1]},{[0,5)=>{A -> [123456, 123456]}, [0,6)=>{A -> [123456, 123456]}, [0,9)=>{A -> [123456, 123456]}, [0,10)=>{A -> [123456, 123456]}, [5,6)=>{A -> [123456, 123456]}, [5,9)=>{A -> [123456, 123456]}, [5,10)=>{A -> [123456, 123456]}, [6,9)=>{A -> [123456, 123456]}, [6,10)=>{A -> [123456, 123456]}, [9,10)=>{A -> [123456, 123456]}}) -bb1_t=({i -> [-1, 9]},{}) -bb2=({i -> [0, 9]},{}) -Abstract trace: entry (bb1 bb1_t bb2)^{5} bb1_f ret - -Program 10: forall 0<= i < n. a[i] == 123456 (decrementing loop w/ temp vars)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({i -> [-1, 9]},{}) -bb1_f=({i -> [-1, 9]},{}) -ret=({i -> [-1, -1]},{[0,5)=>{A -> [123456, 123456]}, [0,6)=>{A -> [123456, 123456]}, [0,9)=>{A -> [123456, 123456]}, [0,10)=>{A -> [123456, 123456]}, [5,6)=>{A -> [123456, 123456]}, [5,9)=>{A -> [123456, 123456]}, [5,10)=>{A -> [123456, 123456]}, [6,9)=>{A -> [123456, 123456]}, [6,10)=>{A -> [123456, 123456]}, [9,10)=>{A -> [123456, 123456]}}) -bb1_t=({i -> [-1, 9]},{}) -bb2=({i -> [0, 9]},{}) -Abstract trace: entry (bb1 bb1_t bb2)^{5} bb1_f ret - -Program 11: forall 0<= i< 10. a[i] = 123456 (w/ temp vars)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A0 -> [123456, 123456]}, [0,2)=>{A0 -> [123456, 123456]}, [0,n1)=>{A0 -> [123456, 123456]}, [0,i)=>{A0 -> [123456, 123456]}, [1,2)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,2)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -=== End ./test-bin/array_graph === === Begin ./test-bin/array_smashing === Program 1: forall 0<= i< 10. a[i] = 123456 Invariants using ArraySmashing(DisjunctiveIntervals) diff --git a/tests/expected_results.elina.out b/tests/expected_results.elina.out index 5cc03bbe..657b854d 100644 --- a/tests/expected_results.elina.out +++ b/tests/expected_results.elina.out @@ -251,103 +251,6 @@ user-defined assertion checker 0 Number of total unreachable checks === End ./test-bin/array_adaptive2 === -=== Begin ./test-bin/array_graph === -Program 1: forall 0<= i< 10. a[i] = 123456Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A0 -> [123456, 123456]}, [0,2)=>{A0 -> [123456, 123456]}, [0,n1)=>{A0 -> [123456, 123456]}, [0,i)=>{A0 -> [123456, 123456]}, [1,2)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,2)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 2: forall 0<= i< 10. a[i] = b[i] = x and x = 123456Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [0,2)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [0,n1)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,2)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,2)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 3: forall 0<= i< 10. a[i] = 8 and b[i] = 5Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A -> [8, 8]; B -> [5, 5]}, [0,2)=>{A -> [8, 8]; B -> [5, 5]}, [0,n1)=>{A -> [8, 8]; B -> [5, 5]}, [0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,2)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,2)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 4: forall 0<= i < n. a[i] = 123456 (unbounded loop)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [1, +oo], n -> [1, +oo], n1-i<=1, n-i<=0, i-n<=0},{[0,1)=>{A -> [123456, 123456]}, [0,n1)=>{A -> [123456, 123456]}, [0,i)=>{A -> [123456, 123456]}, [0,n)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [1,n)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [2,n)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}, [n1,n)=>{A -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=-1, n1-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 6: a[0] = 89 and for all 1<= i < n. a[i] = a[i-1]Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -bb1_f=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -ret=({n1 -> [1, 1], i -> [2, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, n-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,2)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [0,n)=>{A -> [89, 89]}, [1,2)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [1,n)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [2,n)=>{A -> [89, 89]}, [n1,2)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}, [n1,n)=>{A -> [89, 89]}}) -bb1_t=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -bb2=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=-1, n1-n<=-1},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{3} bb1_f ret - -Program 7: forall 0<= i< 10 and i % 2 = 0. a[i] = 123456Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -bb1_f=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -ret=({n1 -> [1, 1], n2 -> [2, 2], i -> [10, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -bb1_t=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -bb2=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 9], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 8: forall 0<= i < n. 1 <= a[i] <= 2Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb1_f2=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb1_f=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,1)=>{A -> [2, 2]}, [i1,i2)=>{A -> [2, 2]}, [i1,n)=>{A -> [2, 2]}, [i2,1)=>{A -> [1, 1]}, [i2,i1)=>{A -> [1, 1]}, [i2,n)=>{A -> [1, 1]}}) -ret=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,1)=>{A -> [2, 2]}, [i1,i2)=>{A -> [2, 2]}, [i1,n)=>{A -> [2, 2]}, [i2,1)=>{A -> [1, 1]}, [i2,i1)=>{A -> [1, 1]}, [i2,n)=>{A -> [1, 1]}}) -bb1_f1=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb1_t=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb2=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=-1, i2-n<=-1},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb2b=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=-1, i2-n<=-1},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb3=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], val -> [1, 2], val-i2<=1, i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,1)=>{A -> [2, 2]}, [i1,i2)=>{A -> [2, 2]}, [i2,1)=>{A -> [1, 1]}, [i2,i1)=>{A -> [1, 1]}}) -bb2a=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=-1, i2-n<=-1},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -Abstract trace: entry (bb1 bb1_t bb2 bb2b bb2a bb3)^{4} bb1_f2 bb1_f1 bb1_f ret - -Program 9: forall 0<= i < n. a[i] == 123456 (decrementing loop)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({i -> [-1, 9]},{}) -bb1_f=({i -> [-1, 9]},{}) -ret=({i -> [-1, -1]},{[0,5)=>{A -> [123456, 123456]}, [0,6)=>{A -> [123456, 123456]}, [0,9)=>{A -> [123456, 123456]}, [0,10)=>{A -> [123456, 123456]}, [5,6)=>{A -> [123456, 123456]}, [5,9)=>{A -> [123456, 123456]}, [5,10)=>{A -> [123456, 123456]}, [6,9)=>{A -> [123456, 123456]}, [6,10)=>{A -> [123456, 123456]}, [9,10)=>{A -> [123456, 123456]}}) -bb1_t=({i -> [-1, 9]},{}) -bb2=({i -> [0, 9]},{}) -Abstract trace: entry (bb1 bb1_t bb2)^{5} bb1_f ret - -Program 10: forall 0<= i < n. a[i] == 123456 (decrementing loop w/ temp vars)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({i -> [-1, 9]},{}) -bb1_f=({i -> [-1, 9]},{}) -ret=({i -> [-1, -1]},{[0,5)=>{A -> [123456, 123456]}, [0,6)=>{A -> [123456, 123456]}, [0,9)=>{A -> [123456, 123456]}, [0,10)=>{A -> [123456, 123456]}, [5,6)=>{A -> [123456, 123456]}, [5,9)=>{A -> [123456, 123456]}, [5,10)=>{A -> [123456, 123456]}, [6,9)=>{A -> [123456, 123456]}, [6,10)=>{A -> [123456, 123456]}, [9,10)=>{A -> [123456, 123456]}}) -bb1_t=({i -> [-1, 9]},{}) -bb2=({i -> [0, 9]},{}) -Abstract trace: entry (bb1 bb1_t bb2)^{5} bb1_f ret - -Program 11: forall 0<= i< 10. a[i] = 123456 (w/ temp vars)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A0 -> [123456, 123456]}, [0,2)=>{A0 -> [123456, 123456]}, [0,n1)=>{A0 -> [123456, 123456]}, [0,i)=>{A0 -> [123456, 123456]}, [1,2)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,2)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -=== End ./test-bin/array_graph === === Begin ./test-bin/array_smashing === Program 1: forall 0<= i< 10. a[i] = 123456 Invariants using ArraySmashing(DisjunctiveIntervals) diff --git a/tests/expected_results.out b/tests/expected_results.out index af2fd11e..f1be8eb8 100644 --- a/tests/expected_results.out +++ b/tests/expected_results.out @@ -251,103 +251,6 @@ user-defined assertion checker 0 Number of total unreachable checks === End ./test-bin/array_adaptive2 === -=== Begin ./test-bin/array_graph === -Program 1: forall 0<= i< 10. a[i] = 123456Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A0 -> [123456, 123456]}, [0,2)=>{A0 -> [123456, 123456]}, [0,n1)=>{A0 -> [123456, 123456]}, [0,i)=>{A0 -> [123456, 123456]}, [1,2)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,2)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 2: forall 0<= i< 10. a[i] = b[i] = x and x = 123456Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [0,2)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [0,n1)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,2)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,2)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]; B -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 3: forall 0<= i< 10. a[i] = 8 and b[i] = 5Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A -> [8, 8]; B -> [5, 5]}, [0,2)=>{A -> [8, 8]; B -> [5, 5]}, [0,n1)=>{A -> [8, 8]; B -> [5, 5]}, [0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,2)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,2)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A -> [8, 8]; B -> [5, 5]}, [1,i)=>{A -> [8, 8]; B -> [5, 5]}, [2,i)=>{A -> [8, 8]; B -> [5, 5]}, [n1,i)=>{A -> [8, 8]; B -> [5, 5]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 4: forall 0<= i < n. a[i] = 123456 (unbounded loop)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [1, +oo], n -> [1, +oo], n1-i<=1, n-i<=0, i-n<=0},{[0,1)=>{A -> [123456, 123456]}, [0,n1)=>{A -> [123456, 123456]}, [0,i)=>{A -> [123456, 123456]}, [0,n)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [1,n)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [2,n)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}, [n1,n)=>{A -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, +oo], n -> [1, +oo], n1-i<=1, i-n<=-1, n1-n<=0},{[0,i)=>{A -> [123456, 123456]}, [1,i)=>{A -> [123456, 123456]}, [2,i)=>{A -> [123456, 123456]}, [n1,i)=>{A -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 6: a[0] = 89 and for all 1<= i < n. a[i] = a[i-1]Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -bb1_f=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -ret=({n1 -> [1, 1], i -> [2, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, n-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,2)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [0,n)=>{A -> [89, 89]}, [1,2)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [1,n)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [2,n)=>{A -> [89, 89]}, [n1,2)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}, [n1,n)=>{A -> [89, 89]}}) -bb1_t=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=0},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -bb2=({n1 -> [1, 1], i -> [1, +oo], n -> [2, +oo], val -> [89, 89], n1-i<=0, i-n<=-1, n1-n<=-1},{[0,1)=>{A -> [89, 89]}, [0,n1)=>{A -> [89, 89]}, [0,i)=>{A -> [89, 89]}, [1,i)=>{A -> [89, 89]}, [2,i)=>{A -> [89, 89]}, [n1,i)=>{A -> [89, 89]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{3} bb1_f ret - -Program 7: forall 0<= i< 10 and i % 2 = 0. a[i] = 123456Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -bb1_f=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -ret=({n1 -> [1, 1], n2 -> [2, 2], i -> [10, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -bb1_t=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 11], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -bb2=({n1 -> [1, 1], n2 -> [2, 2], i -> [0, 9], n -> [1, +oo], i-n2<=9, n2-i<=2},{}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -Program 8: forall 0<= i < n. 1 <= a[i] <= 2Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb1_f2=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb1_f=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,1)=>{A -> [2, 2]}, [i1,i2)=>{A -> [2, 2]}, [i1,n)=>{A -> [2, 2]}, [i2,1)=>{A -> [1, 1]}, [i2,i1)=>{A -> [1, 1]}, [i2,n)=>{A -> [1, 1]}}) -ret=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,1)=>{A -> [2, 2]}, [i1,i2)=>{A -> [2, 2]}, [i1,n)=>{A -> [2, 2]}, [i2,1)=>{A -> [1, 1]}, [i2,i1)=>{A -> [1, 1]}, [i2,n)=>{A -> [1, 1]}}) -bb1_f1=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb1_t=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb2=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=-1, i2-n<=-1},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb2b=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=-1, i2-n<=-1},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -bb3=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], val -> [1, 2], val-i2<=1, i1-n<=0, i2-n<=0},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,1)=>{A -> [2, 2]}, [i1,i2)=>{A -> [2, 2]}, [i2,1)=>{A -> [1, 1]}, [i2,i1)=>{A -> [1, 1]}}) -bb2a=({i1 -> [0, +oo], i2 -> [0, +oo], n -> [1, +oo], i1-n<=-1, i2-n<=-1},{[0,i1)=>{A -> [-oo, 2]}, [0,i2)=>{A -> [1, +oo]}, [1,i1)=>{A -> [-oo, 2]}, [1,i2)=>{A -> [1, +oo]}, [i1,i2)=>{A -> [2, 2]}, [i2,i1)=>{A -> [1, 1]}}) -Abstract trace: entry (bb1 bb1_t bb2 bb2b bb2a bb3)^{4} bb1_f2 bb1_f1 bb1_f ret - -Program 9: forall 0<= i < n. a[i] == 123456 (decrementing loop)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({i -> [-1, 9]},{}) -bb1_f=({i -> [-1, 9]},{}) -ret=({i -> [-1, -1]},{[0,5)=>{A -> [123456, 123456]}, [0,6)=>{A -> [123456, 123456]}, [0,9)=>{A -> [123456, 123456]}, [0,10)=>{A -> [123456, 123456]}, [5,6)=>{A -> [123456, 123456]}, [5,9)=>{A -> [123456, 123456]}, [5,10)=>{A -> [123456, 123456]}, [6,9)=>{A -> [123456, 123456]}, [6,10)=>{A -> [123456, 123456]}, [9,10)=>{A -> [123456, 123456]}}) -bb1_t=({i -> [-1, 9]},{}) -bb2=({i -> [0, 9]},{}) -Abstract trace: entry (bb1 bb1_t bb2)^{5} bb1_f ret - -Program 10: forall 0<= i < n. a[i] == 123456 (decrementing loop w/ temp vars)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({i -> [-1, 9]},{}) -bb1_f=({i -> [-1, 9]},{}) -ret=({i -> [-1, -1]},{[0,5)=>{A -> [123456, 123456]}, [0,6)=>{A -> [123456, 123456]}, [0,9)=>{A -> [123456, 123456]}, [0,10)=>{A -> [123456, 123456]}, [5,6)=>{A -> [123456, 123456]}, [5,9)=>{A -> [123456, 123456]}, [5,10)=>{A -> [123456, 123456]}, [6,9)=>{A -> [123456, 123456]}, [6,10)=>{A -> [123456, 123456]}, [9,10)=>{A -> [123456, 123456]}}) -bb1_t=({i -> [-1, 9]},{}) -bb2=({i -> [0, 9]},{}) -Abstract trace: entry (bb1 bb1_t bb2)^{5} bb1_f ret - -Program 11: forall 0<= i< 10. a[i] = 123456 (w/ temp vars)Invariants using ArrayGraph(SplitDBM,Intervals) -entry=({},{}) -bb1=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_f=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -ret=({n1 -> [1, 1], i -> [10, 10], i-n1<=9, n1-i<=1},{[0,1)=>{A0 -> [123456, 123456]}, [0,2)=>{A0 -> [123456, 123456]}, [0,n1)=>{A0 -> [123456, 123456]}, [0,i)=>{A0 -> [123456, 123456]}, [1,2)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,2)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb1_t=({n1 -> [1, 1], i -> [0, 10], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -bb2=({n1 -> [1, 1], i -> [0, 9], i-n1<=9, n1-i<=1},{[0,i)=>{A0 -> [123456, 123456]}, [1,i)=>{A0 -> [123456, 123456]}, [2,i)=>{A0 -> [123456, 123456]}, [n1,i)=>{A0 -> [123456, 123456]}}) -Abstract trace: entry (bb1 bb1_t bb2)^{4} bb1_f ret - -=== End ./test-bin/array_graph === === Begin ./test-bin/array_smashing === Program 1: forall 0<= i< 10. a[i] = 123456 Invariants using ArraySmashing(DisjunctiveIntervals)