diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index b857a74dd8f..06222ec5afa 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -329,10 +329,10 @@ void interval_domaint::assume_rec( { integer_intervalt &lhs_i=int_map[lhs_identifier]; integer_intervalt &rhs_i=int_map[rhs_identifier]; - lhs_i.meet(rhs_i); - rhs_i=lhs_i; - if(rhs_i.is_bottom()) - make_bottom(); + if(id == ID_lt && !lhs_i.is_less_than(rhs_i)) + lhs_i.make_less_than(rhs_i); + if(id == ID_le && !lhs_i.is_less_than_eq(rhs_i)) + lhs_i.make_less_than_eq(rhs_i); } else if(is_float(lhs.type()) && is_float(rhs.type())) { diff --git a/src/util/Makefile b/src/util/Makefile index 2f3eda6a6b0..2c4b4de1f58 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -106,6 +106,7 @@ SRC = allocate_objects.cpp \ version.cpp \ xml.cpp \ xml_irep.cpp \ + interval.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/util/interval.cpp b/src/util/interval.cpp new file mode 100644 index 00000000000..34161de013c --- /dev/null +++ b/src/util/interval.cpp @@ -0,0 +1,1975 @@ +/*******************************************************************\ + + Module: intervals + + Author: Daniel Neville (2017), Diffblue Ltd + +\*******************************************************************/ + +/* + * + * Types: Should we store a type for the entire interval? + * IMO: I think YES (for the case where we have -inf -> inf, we don't know otherwise + * + * This initial implementation only implements support for integers. + */ + +#include "interval.h" + +#include +#include +#include +#include +#include +#include + +const exprt &constant_interval_exprt::get_lower() const +{ + return op0(); +} + +const exprt &constant_interval_exprt::get_upper() const +{ + return op1(); +} + +constant_interval_exprt constant_interval_exprt::unary_plus() const +{ + return *this; +} + +constant_interval_exprt constant_interval_exprt::unary_minus() const +{ + if(is_single_value_interval()) + { + handle_constant_unary_expression(ID_unary_minus); + } + + exprt lower; + exprt upper; + + if(has_no_upper_bound()) + { + lower = min(); + } + else + { + lower = simplified_expr(unary_minus_exprt(get_upper())); + } + + if(has_no_lower_bound()) + { + upper = max(); + } + else + { + upper = simplified_expr(unary_minus_exprt(get_lower())); + } + + return constant_interval_exprt(lower, upper); +} + +constant_interval_exprt +constant_interval_exprt::plus(const constant_interval_exprt &o) const +{ + if(o.is_single_value_interval() && is_single_value_interval()) + { + handle_constant_binary_expression(o, ID_plus); + } + + exprt lower = min(); + exprt upper = max(); + + if(is_max(get_upper()) || is_max(o.get_upper())) + { + upper = max_exprt(type()); + } + else + { + INVARIANT( + !is_max(get_upper()) && !is_max(o.get_upper()), + "We just excluded this case"); + upper = simplified_expr(plus_exprt(get_upper(), o.get_upper())); + } + + if(is_min(get_lower()) || is_min(o.get_lower())) + { + lower = min_exprt(type()); + } + else + { + INVARIANT( + !is_min(get_lower()) && !is_min(o.get_lower()), + "We just excluded that case"); + lower = simplified_expr(plus_exprt(get_lower(), o.get_lower())); + } + + return simplified_interval(lower, upper); +} + +constant_interval_exprt +constant_interval_exprt::minus(const constant_interval_exprt &other) const +{ + if(other.is_single_value_interval() && is_single_value_interval()) + { + handle_constant_binary_expression(other, ID_minus); + } + + // [this.lower - other.upper, this.upper - other.lower] + return plus(other.unary_minus()); +} + +constant_interval_exprt +constant_interval_exprt::multiply(const constant_interval_exprt &o) const +{ + if(o.is_single_value_interval() && is_single_value_interval()) + { + handle_constant_binary_expression(o, ID_mult); + } + + return get_extremes(*this, o, ID_mult); +} + +constant_interval_exprt +constant_interval_exprt::divide(const constant_interval_exprt &o) const +{ + if(o.is_single_value_interval() && is_single_value_interval()) + { + handle_constant_binary_expression(o, ID_div); + } + + // If other might be division by zero, set everything to top. + if(o.contains_zero()) + { + return top(); + } + + return get_extremes(*this, o, ID_div); +} + +constant_interval_exprt +constant_interval_exprt::modulo(const constant_interval_exprt &o) const +{ + // SEE https://stackoverflow.com/questions/11720656/modulo-operation-with-negative-numbers + + if(o.is_single_value_interval() && is_single_value_interval()) + { + handle_constant_binary_expression(o, ID_mod); + } + + if(o.is_bottom()) + { + return top(); + } + + // If the RHS is 1, or -1 (signed only), then return zero. + if( + o == constant_interval_exprt(from_integer(1, o.type())) || + (o.is_signed() && o == constant_interval_exprt(from_integer(-1, o.type())))) + { + return constant_interval_exprt(zero()); + } + + // If other might be modulo by zero, set everything to top. + if(o.contains_zero()) + { + return top(); + } + + if(is_zero()) + { + return constant_interval_exprt(zero()); + } + + exprt lower = min(); + exprt upper = max(); + + // Positive case (cannot have zero on RHS). + // 10 % 5 = [0, 4], 3 % 5 = [0, 3] + if(!is_negative() && o.is_positive()) + { + lower = zero(); + upper = get_min(get_upper(), o.decrement().get_upper()); + } + + // [-5, 5] % [3] + if(is_negative(get_lower()) && is_positive(get_upper())) + { + INVARIANT( + contains_zero(), + "Zero should be between a negative and a positive value"); + // This can be done more accurately. + lower = get_min(o.get_lower(), get_lower()); + upper = get_max(o.get_upper(), get_upper()); + } + + if(is_negative() && o.is_negative()) + { + lower = get_min(o.get_lower(), o.get_lower()); + upper = zero(); + } + + return constant_interval_exprt(lower, upper); +} + +tvt constant_interval_exprt::is_definitely_true() const +{ + // tvt not + return !is_definitely_false(); +} + +tvt constant_interval_exprt::is_definitely_false() const +{ + if(type().id() == ID_bool) + { + if(is_single_value_interval()) + { + return tvt(get_lower() == false_exprt()); + } + else + { + return tvt::unknown(); + } + } + + if(equal(constant_interval_exprt(zero())).is_true()) + { + return tvt(true); + } + + if(contains(constant_interval_exprt(zero()))) + { + INVARIANT( + is_positive(get_upper()) || is_negative(get_lower()), + "If an interval contains zero its lower bound can't be positive" + " and its upper bound can't be negative"); + return tvt::unknown(); + } + + return tvt(false); +} + +tvt constant_interval_exprt::logical_or(const constant_interval_exprt &o) const +{ + PRECONDITION(type().id() == ID_bool); + PRECONDITION(o.type().id() == ID_bool); + + tvt a = is_definitely_true(); + tvt b = o.is_definitely_true(); + + return (a || b); +} + +tvt constant_interval_exprt::logical_and(const constant_interval_exprt &o) const +{ + PRECONDITION(type().id() == ID_bool); + PRECONDITION(o.type().id() == ID_bool); + + return (is_definitely_true() && o.is_definitely_true()); +} + +tvt constant_interval_exprt::logical_xor(const constant_interval_exprt &o) const +{ + PRECONDITION(type().id() == ID_bool); + PRECONDITION(o.type().id() == ID_bool); + + return ( + (is_definitely_true() && !o.is_definitely_true()) || + (!is_definitely_true() && o.is_definitely_true())); +} + +tvt constant_interval_exprt::logical_not() const +{ + PRECONDITION(type().id() == ID_bool); + + if(is_definitely_true().is_true()) + { + return tvt(false); + } + + if(is_definitely_false().is_true()) + { + return tvt(true); + } + + return tvt::unknown(); +} + +constant_interval_exprt +constant_interval_exprt::left_shift(const constant_interval_exprt &o) const +{ + if(o.is_single_value_interval() && is_single_value_interval()) + { + return handle_constant_binary_expression(o, ID_shl); + } + + if(is_negative(o.get_lower())) + { + return top(); + } + + return get_extremes(*this, o, ID_shl); +} + +// Arithmetic +constant_interval_exprt +constant_interval_exprt::right_shift(const constant_interval_exprt &o) const +{ + if(o.is_single_value_interval() && is_single_value_interval()) + { + return handle_constant_binary_expression(o, ID_ashr); + } + + if(is_negative(o.get_lower())) + { + return top(); + } + + return get_extremes(*this, o, ID_ashr); +} + +constant_interval_exprt +constant_interval_exprt::bitwise_xor(const constant_interval_exprt &o) const +{ + if(o.is_single_value_interval() && is_single_value_interval()) + { + return handle_constant_binary_expression(o, ID_bitxor); + } + + return top(); +} + +constant_interval_exprt +constant_interval_exprt::bitwise_or(const constant_interval_exprt &o) const +{ + if(o.is_single_value_interval() && is_single_value_interval()) + { + return handle_constant_binary_expression(o, ID_bitor); + } + + return top(); +} + +constant_interval_exprt +constant_interval_exprt::bitwise_and(const constant_interval_exprt &o) const +{ + if(o.is_single_value_interval() && is_single_value_interval()) + { + return handle_constant_binary_expression(o, ID_bitand); + } + + return top(); +} + +constant_interval_exprt constant_interval_exprt::bitwise_not() const +{ + if(is_single_value_interval()) + { + return handle_constant_unary_expression(ID_bitnot); + } + + return top(); +} + +tvt constant_interval_exprt::less_than(const constant_interval_exprt &o) const +{ + // [get_lower, get_upper] < [o.get_lower(), o.get_upper()] + if(is_single_value_interval() && o.is_single_value_interval()) + { + return tvt(less_than(get_lower(), o.get_lower())); + } + + if(less_than(get_upper(), o.get_lower())) + { + return tvt(true); + } + + if(greater_than(get_lower(), o.get_upper())) + { + return tvt(false); + } + + return tvt::unknown(); +} + +tvt constant_interval_exprt::greater_than( + const constant_interval_exprt &o) const +{ + return o.less_than(*this); +} + +tvt constant_interval_exprt::less_than_or_equal( + const constant_interval_exprt &o) const +{ + if(is_single_value_interval() && o.is_single_value_interval()) + { + return tvt(less_than_or_equal(get_lower(), o.get_lower())); + } + + // [get_lower, get_upper] <= [o.get_lower(), o.get_upper()] + if(less_than_or_equal(get_upper(), o.get_lower())) + { + return tvt(true); + } + + if(greater_than(get_lower(), o.get_upper())) + { + return tvt(false); + } + + return tvt::unknown(); +} + +tvt constant_interval_exprt::greater_than_or_equal( + const constant_interval_exprt &o) const +{ + return o.less_than_or_equal(*this); +} + +tvt constant_interval_exprt::equal(const constant_interval_exprt &o) const +{ + if(is_single_value_interval() && o.is_single_value_interval()) + { + return tvt(equal(get_lower(), o.get_lower())); + } + + if(equal(get_upper(), o.get_upper()) && equal(get_upper(), o.get_upper())) + { + return tvt(true); + } + + if( + less_than(o).is_true() || greater_than(o).is_true() || + o.less_than(*this).is_true() || o.greater_than(*this).is_true()) + { + return tvt(false); + } + + // Don't know. Could have [3, 5] == [4] (not equal) + return tvt::unknown(); +} + +tvt constant_interval_exprt::not_equal(const constant_interval_exprt &o) const +{ + return !equal(o); +} + +constant_interval_exprt constant_interval_exprt::increment() const +{ + return plus(constant_interval_exprt(from_integer(mp_integer(1), type()))); +} + +constant_interval_exprt constant_interval_exprt::decrement() const +{ + return minus(constant_interval_exprt(from_integer(mp_integer(1), type()))); +} + +constant_interval_exprt constant_interval_exprt::get_extremes( + const constant_interval_exprt &a, + const constant_interval_exprt &b, + const irep_idt &operation) +{ + std::vector results; + + generate_expression(a.get_lower(), b.get_lower(), operation, results); + generate_expression(a.get_lower(), b.get_upper(), operation, results); + generate_expression(a.get_upper(), b.get_lower(), operation, results); + generate_expression(a.get_upper(), b.get_upper(), operation, results); + + for(auto result : results) + { + if(!is_extreme(result) && contains_extreme(result)) + { + return constant_interval_exprt(result.type()); + } + } + + exprt min = get_min(results); + exprt max = get_max(results); + + return simplified_interval(min, max); +} + +exprt constant_interval_exprt::get_extreme( + std::vector values, + bool min_value) +{ + symbol_tablet symbol_table; + namespacet ns(symbol_table); // Empty + + if(values.size() == 0) + { + return nil_exprt(); + } + + if(values.size() == 1) + { + return *(values.begin()); + } + + if(values.size() == 2) + { + if(min_value) + { + return get_min(values.front(), values.back()); + } + else + { + return get_max(values.front(), values.back()); + } + } + + typet type = values.begin()->type(); + + for(auto v : values) + { + if((min_value && is_min(v)) || (!min_value && is_max(v))) + { + return v; + } + } + + for(auto left : values) + { + bool all_left_OP_right = true; + + for(auto right : values) + { + if( + (min_value && less_than_or_equal(left, right)) || + (!min_value && greater_than_or_equal(left, right))) + { + continue; + } + + all_left_OP_right = false; + break; + } + + if(all_left_OP_right) + { + return left; + } + } + + /* Return top */ + if(min_value) + { + return min_exprt(type); + } + else + { + return max_exprt(type); + } + + UNREACHABLE; +} + +void constant_interval_exprt::generate_expression( + const exprt &lhs, + const exprt &rhs, + const irep_idt &operation, + std::vector &collection) +{ + if(operation == ID_mult) + { + append_multiply_expression(lhs, rhs, collection); + } + else if(operation == ID_div) + { + collection.push_back(generate_division_expression(lhs, rhs)); + } + else if(operation == ID_mod) + { + collection.push_back(generate_modulo_expression(lhs, rhs)); + } + else if(operation == ID_shl || operation == ID_ashr) + { + collection.push_back(generate_shift_expression(lhs, rhs, operation)); + } +} + +/// Adds all possible values that may arise from multiplication (more than one, +/// in case of past the type boundary results). +/// \param lower lhs of multiplication +/// \param upper rhs of multiplication +/// \param collection vector of possible values +void constant_interval_exprt::append_multiply_expression( + const exprt &lower, + const exprt &upper, + std::vector &collection) +{ + PRECONDITION(lower.type().is_not_nil() && is_numeric(lower.type())); + + if(is_max(lower)) + { + append_multiply_expression_max(upper, collection); + } + else if(is_max(upper)) + { + append_multiply_expression_max(lower, collection); + } + else if(is_min(lower)) + { + append_multiply_expression_min(lower, upper, collection); + } + else if(is_min(upper)) + { + append_multiply_expression_min(upper, lower, collection); + } + else + { + INVARIANT( + !is_extreme(lower) && !is_extreme(upper), + "We ruled out extreme cases beforehand"); + + auto result = mult_exprt(lower, upper); + collection.push_back(simplified_expr(result)); + } +} + +/// Appends interval bounds that could arise from MAX * expr. Accommodates for +/// overflows by over-approximating. +/// \param expr the unknown side of multiplication +/// \param collection vector of collected bounds +void constant_interval_exprt::append_multiply_expression_max( + const exprt &expr, + std::vector &collection) +{ + if(is_min(expr)) + { + INVARIANT(!is_positive(expr), "Min value cannot be >0."); + INVARIANT( + is_negative(expr) || is_zero(expr), "Non-negative MIN must be zero."); + } + + if(is_zero(expr)) + collection.push_back(expr); + else + { + collection.push_back(max_exprt(expr)); + collection.push_back(min_exprt(expr)); + } +} + +/// Appends interval bounds that could arise from MIN * other. Accommodates for +/// overflows by over-approximating. +/// \param min the side known to be MIN for a given type +/// \param other the side of unknown value +/// \param collection reference to the vector of collected boundaries +void constant_interval_exprt::append_multiply_expression_min( + const exprt &min, + const exprt &other, + std::vector &collection) +{ + PRECONDITION(is_min(min)); + INVARIANT(!is_positive(min), "Min value cannot be >0."); + INVARIANT(is_negative(min) || is_zero(min), "Non-negative MIN must be zero."); + + if(is_zero(min)) + collection.push_back(min); + else if(is_zero(other)) + collection.push_back(other); + else + { + collection.push_back(min_exprt(min)); + collection.push_back(max_exprt(min)); + } +} + +exprt constant_interval_exprt::generate_division_expression( + const exprt &lhs, + const exprt &rhs) +{ + PRECONDITION(lhs.type().is_not_nil() && is_numeric(lhs.type())); + + PRECONDITION(!is_zero(rhs)); + + if(rhs.is_one()) + { + return lhs; + } + + if(is_max(lhs)) + { + if(is_negative(rhs)) + { + return min_exprt(lhs); + } + + return lhs; + } + + if(is_min(lhs)) + { + if(is_negative(rhs)) + { + return max_exprt(lhs); + } + + return lhs; + } + + INVARIANT(!is_extreme(lhs), "We ruled out extreme cases beforehand"); + + if(is_max(rhs)) + { + return zero(rhs); + } + + if(is_min(rhs)) + { + INVARIANT( + is_signed(rhs), "We think this is a signed integer for some reason?"); + return zero(rhs); + } + + INVARIANT( + !is_extreme(lhs) && !is_extreme(rhs), + "We ruled out extreme cases beforehand"); + + auto div_expr = div_exprt(lhs, rhs); + return simplified_expr(div_expr); +} + +exprt constant_interval_exprt::generate_modulo_expression( + const exprt &lhs, + const exprt &rhs) +{ + PRECONDITION(lhs.type().is_not_nil() && is_numeric(lhs.type())); + + PRECONDITION(!is_zero(rhs)); + + if(rhs.is_one()) + { + return lhs; + } + + if(is_max(lhs)) + { + if(is_negative(rhs)) + { + return min_exprt(lhs); + } + + return lhs; + } + + if(is_min(lhs)) + { + if(is_negative(rhs)) + { + return max_exprt(lhs); + } + + return lhs; + } + + INVARIANT(!is_extreme(lhs), "We rule out this case beforehand"); + + if(is_max(rhs)) + { + return zero(rhs); + } + + if(is_min(rhs)) + { + INVARIANT(is_signed(rhs), "We assume this is signed for some reason?"); + return zero(rhs); + } + + INVARIANT( + !is_extreme(lhs) && !is_extreme(rhs), + "We ruled out extreme values beforehand"); + + auto modulo_expr = mod_exprt(lhs, rhs); + return simplified_expr(modulo_expr); +} + +constant_interval_exprt constant_interval_exprt::eval(const irep_idt &id) const +{ + if(id == ID_unary_plus) + { + return unary_plus(); + } + if(id == ID_unary_minus) + { + return unary_minus(); + } + if(id == ID_bitnot) + { + return bitwise_not(); + } + if(id == ID_not) + { + return tvt_to_interval(logical_not()); + } + + return top(); +} + +constant_interval_exprt constant_interval_exprt::eval( + const irep_idt &binary_operator, + const constant_interval_exprt &other) const +{ + if(binary_operator == ID_plus) + { + return plus(other); + } + if(binary_operator == ID_minus) + { + return unary_minus(other); + } + if(binary_operator == ID_mult) + { + return multiply(other); + } + if(binary_operator == ID_div) + { + return divide(other); + } + if(binary_operator == ID_mod) + { + return modulo(other); + } + if(binary_operator == ID_shl) + { + return left_shift(other); + } + if(binary_operator == ID_ashr) + { + return right_shift(other); + } + if(binary_operator == ID_bitor) + { + return bitwise_or(other); + } + if(binary_operator == ID_bitand) + { + return bitwise_and(other); + } + if(binary_operator == ID_bitxor) + { + return bitwise_xor(other); + } + if(binary_operator == ID_lt) + { + return tvt_to_interval(less_than(other)); + } + if(binary_operator == ID_le) + { + return tvt_to_interval(less_than_or_equal(other)); + } + if(binary_operator == ID_gt) + { + return tvt_to_interval(greater_than(other)); + } + if(binary_operator == ID_ge) + { + return tvt_to_interval(greater_than_or_equal(other)); + } + if(binary_operator == ID_equal) + { + return tvt_to_interval(equal(other)); + } + if(binary_operator == ID_notequal) + { + return tvt_to_interval(not_equal(other)); + } + if(binary_operator == ID_and) + { + return tvt_to_interval(logical_and(other)); + } + if(binary_operator == ID_or) + { + return tvt_to_interval(logical_or(other)); + } + if(binary_operator == ID_xor) + { + return tvt_to_interval(logical_xor(other)); + } + + return top(); +} + +exprt constant_interval_exprt::generate_shift_expression( + const exprt &lhs, + const exprt &rhs, + const irep_idt &operation) +{ + PRECONDITION(operation == ID_shl || operation == ID_ashr); + + if(is_zero(lhs) || is_zero(rhs)) + { + // Shifting zero does nothing. + // Shifting BY zero also does nothing. + return lhs; + } + + INVARIANT(!is_negative(rhs), "Should be caught at an earlier stage."); + + if(is_max(lhs)) + { + return lhs; + } + + if(is_min(lhs)) + { + return lhs; + } + + if(is_max(rhs)) + { + return min_exprt(rhs); + } + + INVARIANT( + !is_extreme(lhs) && !is_extreme(rhs), + "We ruled out extreme cases beforehand"); + + auto shift_expr = shift_exprt(lhs, operation, rhs); + return simplified_expr(shift_expr); +} + +constant_interval_exprt +constant_interval_exprt::handle_constant_unary_expression( + const irep_idt &op) const +{ + if(is_single_value_interval()) + { + auto expr = unary_exprt(op, get_lower()); + return constant_interval_exprt(simplified_expr(expr)); + } + return top(); +} + +constant_interval_exprt +constant_interval_exprt::handle_constant_binary_expression( + const constant_interval_exprt &other, + const irep_idt &op) const +{ + PRECONDITION(is_single_value_interval() && other.is_single_value_interval()); + auto expr = binary_exprt(get_lower(), op, other.get_lower()); + return constant_interval_exprt(simplified_expr(expr)); +} + +exprt constant_interval_exprt::get_max(const exprt &a, const exprt &b) +{ + return greater_than(a, b) ? a : b; +} + +exprt constant_interval_exprt::get_min(const exprt &a, const exprt &b) +{ + return less_than(a, b) ? a : b; +} + +exprt constant_interval_exprt::get_min(std::vector &values) +{ + return get_extreme(values, true); +} + +exprt constant_interval_exprt::get_max(std::vector &values) +{ + return get_extreme(values, false); +} + +/* we don't simplify in the constructor otherwise */ +constant_interval_exprt +constant_interval_exprt::simplified_interval(exprt &l, exprt &r) +{ + return constant_interval_exprt(simplified_expr(l), simplified_expr(r)); +} + +exprt constant_interval_exprt::simplified_expr(exprt expr) +{ + symbol_tablet symbol_table; + const namespacet ns(symbol_table); + + PRECONDITION(!contains_extreme(expr)); + + return simplify_expr(expr, ns); +} + +constant_exprt constant_interval_exprt::zero(const typet &type) +{ + constant_exprt zero = from_integer(mp_integer(0), type); + INVARIANT( + zero.is_zero() || (type.id() == ID_bool && zero.is_false()), + "The value created from 0 should be zero or false"); + return zero; +} + +constant_exprt constant_interval_exprt::zero(const exprt &expr) +{ + return zero(expr.type()); +} + +constant_exprt +constant_interval_exprt::zero(const constant_interval_exprt &interval) +{ + return zero(interval.type()); +} + +constant_exprt constant_interval_exprt::zero() const +{ + return zero(type()); +} + +min_exprt constant_interval_exprt::min() const +{ + return min_exprt(type()); +} + +max_exprt constant_interval_exprt::max() const +{ + return max_exprt(type()); +} + +bool constant_interval_exprt::is_top() const +{ + return (has_no_lower_bound() && has_no_upper_bound()); +} + +bool constant_interval_exprt::is_bottom() const +{ + // This should ONLY happen for bottom. + return is_min(get_upper()) || is_max(get_lower()); +} + +constant_interval_exprt constant_interval_exprt::top(const typet &type) +{ + return constant_interval_exprt(type); +} + +constant_interval_exprt constant_interval_exprt::bottom(const typet &type) +{ + return constant_interval_exprt(max_exprt(type), min_exprt(type)); +} + +constant_interval_exprt constant_interval_exprt::top() const +{ + return constant_interval_exprt(type()); +} + +constant_interval_exprt constant_interval_exprt::bottom() const +{ + return bottom(type()); +} + +/* Helpers */ + +bool constant_interval_exprt::is_int() const +{ + return is_int(type()); +} + +bool constant_interval_exprt::is_float() const +{ + return is_float(type()); +} + +bool constant_interval_exprt::is_numeric(const typet &type) +{ + return is_int(type) || is_float(type); +} + +bool constant_interval_exprt::is_numeric() const +{ + return is_numeric(type()); +} + +bool constant_interval_exprt::is_numeric(const exprt &expr) +{ + return is_numeric(expr.type()); +} + +bool constant_interval_exprt::is_numeric( + const constant_interval_exprt &interval) +{ + return interval.is_numeric(); +} + +bool constant_interval_exprt::is_int(const typet &type) +{ + return (is_signed(type) || is_unsigned(type)); +} + +bool constant_interval_exprt::is_float(const typet &src) +{ + return src.id() == ID_floatbv; +} + +bool constant_interval_exprt::is_int(const exprt &expr) +{ + return is_int(expr.type()); +} + +bool constant_interval_exprt::is_int(const constant_interval_exprt &interval) +{ + return interval.is_int(); +} + +bool constant_interval_exprt::is_float(const exprt &expr) +{ + return is_float(expr.type()); +} + +bool constant_interval_exprt::is_float(const constant_interval_exprt &interval) +{ + return interval.is_float(); +} + +bool constant_interval_exprt::is_bitvector(const typet &t) +{ + return t.id() == ID_bv || t.id() == ID_signedbv || t.id() == ID_unsignedbv || + t.id() == ID_c_bool || + (t.id() == ID_c_bit_field && is_bitvector(t.subtype())); +} + +bool constant_interval_exprt::is_signed(const typet &t) +{ + return t.id() == ID_signedbv || + (t.id() == ID_c_bit_field && is_signed(t.subtype())); +} + +bool constant_interval_exprt::is_unsigned(const typet &t) +{ + return t.id() == ID_bv || t.id() == ID_unsignedbv || t.id() == ID_c_bool || + t.id() == ID_c_enum || + (t.id() == ID_c_bit_field && is_unsigned(t.subtype())); +} + +bool constant_interval_exprt::is_signed(const constant_interval_exprt &interval) +{ + return is_signed(interval.type()); +} + +bool constant_interval_exprt::is_unsigned( + const constant_interval_exprt &interval) +{ + return is_unsigned(interval.type()); +} + +bool constant_interval_exprt::is_bitvector( + const constant_interval_exprt &interval) +{ + return is_bitvector(interval.type()); +} + +bool constant_interval_exprt::is_signed(const exprt &expr) +{ + return is_signed(expr.type()); +} + +bool constant_interval_exprt::is_unsigned(const exprt &expr) +{ + return is_unsigned(expr.type()); +} + +bool constant_interval_exprt::is_bitvector(const exprt &expr) +{ + return is_bitvector(expr.type()); +} + +bool constant_interval_exprt::is_signed() const +{ + return is_signed(type()); +} + +bool constant_interval_exprt::is_unsigned() const +{ + return is_unsigned(type()); +} + +bool constant_interval_exprt::is_bitvector() const +{ + return is_bitvector(type()); +} + +bool constant_interval_exprt::is_extreme(const exprt &expr) +{ + return (is_max(expr) || is_min(expr)); +} + +bool constant_interval_exprt::is_extreme(const exprt &expr1, const exprt &expr2) +{ + return is_extreme(expr1) || is_extreme(expr2); +} + +bool constant_interval_exprt::has_no_upper_bound() const +{ + return is_max(get_upper()); +} + +bool constant_interval_exprt::has_no_lower_bound() const +{ + return is_min(get_lower()); +} + +bool constant_interval_exprt::is_max(const exprt &expr) +{ + return expr.id() == ID_max; +} + +bool constant_interval_exprt::is_min(const exprt &expr) +{ + return expr.id() == ID_min; +} + +bool constant_interval_exprt::is_positive(const exprt &expr) +{ + exprt simplified = simplified_expr(expr); + + if(expr.is_nil() || !simplified.is_constant() || expr.get(ID_value) == "") + { + return false; + } + + if(is_unsigned(expr) || is_max(expr)) + { + return true; + } + + INVARIANT(is_signed(expr), "Not implemented for floats"); + // Floats later + + if(is_min(expr)) + { + return false; + } + + return greater_than(expr, zero(expr)); +} + +bool constant_interval_exprt::is_zero(const exprt &expr) +{ + if(is_min(expr)) + { + if(is_unsigned(expr)) + { + return true; + } + else + { + return false; + } + } + + if(is_max(expr)) + { + return false; + } + + INVARIANT(!is_max(expr) && !is_min(expr), "We excluded those cases"); + + if(expr.is_zero()) + { + return true; + } + + return equal(expr, zero(expr)); +} + +bool constant_interval_exprt::is_negative(const exprt &expr) +{ + if(is_unsigned(expr) || is_max(expr)) + { + return false; + } + + INVARIANT( + is_signed(expr), "We don't support anything other than integers yet"); + + if(is_min(expr)) + { + return true; + } + + INVARIANT(!is_extreme(expr), "We excluded these cases before"); + + return less_than(expr, zero(expr)); +} + +exprt constant_interval_exprt::abs(const exprt &expr) +{ + if(is_signed(expr) && is_min(expr)) + { + return max_exprt(expr); + } + + if(is_max(expr) || is_unsigned(expr) || is_zero(expr) || is_positive(expr)) + { + return expr; + } + + return simplified_expr(unary_minus_exprt(expr)); +} + +bool constant_interval_exprt::equal(const exprt &a, const exprt &b) +{ + if(a == b) + { + return true; + } + + if(!is_numeric(a) || !is_numeric(b)) + { + INVARIANT( + !(a == b), + "Best we can do now is a==b?, but this is covered by the above, so " + "always false"); + return false; + } + + if(is_max(a) && is_max(b)) + { + return true; + } + + exprt l = (is_min(a) && is_unsigned(a)) ? zero(a) : a; + exprt r = (is_min(b) && is_unsigned(b)) ? zero(b) : b; + + // CANNOT use is_zero(X) but can use X.is_zero(); + if((is_min(l) && is_min(r))) + { + return true; + } + + if( + (is_max(l) && !is_max(r)) || (is_min(l) && !is_min(r)) || + (is_max(r) && !is_max(l)) || (is_min(r) && !is_min(l))) + { + return false; + } + + INVARIANT(!is_extreme(l, r), "We've excluded this before"); + + return simplified_expr(equal_exprt(l, r)).is_true(); +} + +// TODO: Signed/unsigned comparisons. +bool constant_interval_exprt::less_than(const exprt &a, const exprt &b) +{ + if(!is_numeric(a) || !is_numeric(b)) + { + return false; + } + + exprt l = (is_min(a) && is_unsigned(a)) ? zero(a) : a; + exprt r = (is_min(b) && is_unsigned(b)) ? zero(b) : b; + + if(is_max(l)) + { + return false; + } + + INVARIANT(!is_max(l), "We've just excluded this case"); + + if(is_min(r)) + { + // Can't be smaller than min. + return false; + } + + INVARIANT(!is_max(l) && !is_min(r), "We've excluded these cases"); + + if(is_min(l)) + { + return true; + } + + INVARIANT( + !is_max(l) && !is_min(r) && !is_min(l), + "These cases should have all been handled before this point"); + + if(is_max(r)) + { + // If r is max, then l is less, unless l is max. + return !is_max(l); + } + + INVARIANT( + !is_extreme(l) && !is_extreme(r), + "We have excluded all of these cases in the code above"); + + return simplified_expr(binary_relation_exprt(l, ID_lt, r)).is_true(); +} + +bool constant_interval_exprt::greater_than(const exprt &a, const exprt &b) +{ + return less_than(b, a); +} + +bool constant_interval_exprt::less_than_or_equal(const exprt &a, const exprt &b) +{ + return less_than(a, b) || equal(a, b); +} + +bool constant_interval_exprt::greater_than_or_equal( + const exprt &a, + const exprt &b) +{ + return greater_than(a, b) || equal(a, b); +} + +bool constant_interval_exprt::not_equal(const exprt &a, const exprt &b) +{ + return !equal(a, b); +} + +bool constant_interval_exprt::contains( + const constant_interval_exprt &interval) const +{ + // [a, b] Contains [c, d] If c >= a and d <= b. + return ( + less_than_or_equal(interval.get_upper(), get_upper()) && + greater_than_or_equal(interval.get_lower(), get_lower())); +} + +std::string constant_interval_exprt::to_string() const +{ + std::stringstream out; + out << *this; + return out.str(); +} + +std::ostream &operator<<(std::ostream &out, const constant_interval_exprt &i) +{ + out << "["; + + if(!i.has_no_lower_bound()) + { + // FIXME Not everything that's a bitvector is also an integer + if(i.is_bitvector(i.get_lower())) + { + out << binary2integer( + id2string(i.get_lower().get(ID_value)), i.is_signed()); + } + else + { + // TODO handle floating point numbers? + out << i.get_lower().get(ID_value); + } + } + else + { + if(i.is_signed(i.get_lower())) + { + out << "MIN"; + } + else + { + // FIXME Extremely sketchy, the opposite of + // FIXME "signed" isn't "unsigned" but + // FIXME "literally anything else" + out << "0"; + } + } + + out << ","; + + // FIXME See comments on is_min + if(!i.has_no_upper_bound()) + { + if(i.is_bitvector(i.get_upper())) + { + out << binary2integer( + id2string(i.get_upper().get(ID_value)), i.is_signed()); + } + else + { + out << i.get_upper().get(ID_value); + } + } + else + out << "MAX"; + + out << "]"; + + return out; +} + +bool operator<( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.less_than(rhs).is_true(); +} + +bool operator>( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.greater_than(rhs).is_true(); +} + +bool operator<=( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.less_than_or_equal(rhs).is_true(); +} + +bool operator>=( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.greater_than(rhs).is_true(); +} + +bool operator==( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.equal(rhs).is_true(); +} + +bool operator!=( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.not_equal(rhs).is_true(); +} + +const constant_interval_exprt operator+( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.unary_plus(rhs); +} + +const constant_interval_exprt operator-( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.minus(rhs); +} + +const constant_interval_exprt operator/( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.divide(rhs); +} + +const constant_interval_exprt operator*( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.multiply(rhs); +} + +const constant_interval_exprt operator%( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.modulo(rhs); +} + +const constant_interval_exprt operator&( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.bitwise_and(rhs); +} + +const constant_interval_exprt operator|( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.bitwise_or(rhs); +} + +const constant_interval_exprt operator^( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.bitwise_xor(rhs); +} + +const constant_interval_exprt operator!(const constant_interval_exprt &lhs) +{ + return lhs.bitwise_not(); +} + +const constant_interval_exprt operator<<( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.left_shift(rhs); +} + +const constant_interval_exprt operator>>( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + return lhs.right_shift(rhs); +} + +constant_interval_exprt +constant_interval_exprt::unary_plus(const constant_interval_exprt &a) +{ + return a.unary_plus(); +} + +constant_interval_exprt +constant_interval_exprt::unary_minus(const constant_interval_exprt &a) +{ + return a.unary_minus(); +} + +constant_interval_exprt +constant_interval_exprt::typecast(const typet &type) const +{ + if(this->type().id() == ID_bool && is_int(type)) + { + bool lower = !has_no_lower_bound() && get_lower().is_true(); + bool upper = has_no_upper_bound() || get_upper().is_true(); + + INVARIANT(!lower || upper, ""); + + constant_exprt lower_num = from_integer(lower, type); + constant_exprt upper_num = from_integer(upper, type); + + return constant_interval_exprt(lower_num, upper_num, type); + } + else + { + auto do_typecast = [&type](exprt e) { + if(e.id() == ID_min || e.id() == ID_max) + { + e.type() = type; + } + else + { + e = simplified_expr(typecast_exprt(e, type)); + } + return e; + }; + + exprt lower = do_typecast(get_lower()); + POSTCONDITION(lower.id() == get_lower().id()); + + exprt upper = do_typecast(get_upper()); + POSTCONDITION(upper.id() == get_upper().id()); + + return constant_interval_exprt(lower, upper, type); + } +} + +/* Binary */ +constant_interval_exprt constant_interval_exprt::plus( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.plus(b); +} + +constant_interval_exprt constant_interval_exprt::minus( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.minus(b); +} + +constant_interval_exprt constant_interval_exprt::multiply( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.multiply(b); +} + +constant_interval_exprt constant_interval_exprt::divide( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.divide(b); +} + +constant_interval_exprt constant_interval_exprt::modulo( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.modulo(b); +} + +/* Binary shifts */ +constant_interval_exprt constant_interval_exprt::left_shift( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.left_shift(b); +} + +constant_interval_exprt constant_interval_exprt::right_shift( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.right_shift(b); +} + +/* Unary bitwise */ +constant_interval_exprt +constant_interval_exprt::bitwise_not(const constant_interval_exprt &a) +{ + return a.bitwise_not(); +} + +/* Binary bitwise */ +constant_interval_exprt constant_interval_exprt::bitwise_xor( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.bitwise_xor(b); +} + +constant_interval_exprt constant_interval_exprt::bitwise_or( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.bitwise_or(b); +} + +constant_interval_exprt constant_interval_exprt::bitwise_and( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.bitwise_and(b); +} + +tvt constant_interval_exprt::less_than( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.less_than(b); +} + +tvt constant_interval_exprt::greater_than( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.greater_than(b); +} + +tvt constant_interval_exprt::less_than_or_equal( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.less_than_or_equal(b); +} + +tvt constant_interval_exprt::greater_than_or_equal( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.greater_than_or_equal(b); +} + +tvt constant_interval_exprt::equal( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.equal(b); +} + +tvt constant_interval_exprt::not_equal( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.equal(b); +} + +constant_interval_exprt +constant_interval_exprt::increment(const constant_interval_exprt &a) +{ + return a.increment(); +} + +constant_interval_exprt +constant_interval_exprt::decrement(const constant_interval_exprt &a) +{ + return a.decrement(); +} + +bool constant_interval_exprt::is_empty(const constant_interval_exprt &a) +{ + return a.is_empty(); +} + +bool constant_interval_exprt::is_single_value_interval( + const constant_interval_exprt &a) +{ + return a.is_single_value_interval(); +} + +bool constant_interval_exprt::is_top(const constant_interval_exprt &a) +{ + return a.is_top(); +} + +bool constant_interval_exprt::is_bottom(const constant_interval_exprt &a) +{ + return a.is_bottom(); +} + +bool constant_interval_exprt::is_min(const constant_interval_exprt &a) +{ + return a.has_no_lower_bound(); +} + +bool constant_interval_exprt::is_max(const constant_interval_exprt &a) +{ + return a.has_no_upper_bound(); +} + +bool constant_interval_exprt::contains_extreme(const exprt expr) +{ + forall_operands(it, expr) + { + if(is_extreme(*it)) + { + return true; + } + + if(it->has_operands()) + { + return contains_extreme(*it); + } + } + + return false; +} + +bool constant_interval_exprt::contains_extreme( + const exprt expr1, + const exprt expr2) +{ + return contains_extreme(expr1) || contains_extreme(expr2); +} + +bool constant_interval_exprt::is_empty() const +{ + if(greater_than(get_lower(), get_upper())) + { + return false; + } + + return true; +} + +bool constant_interval_exprt::is_single_value_interval() const +{ + return !is_extreme(get_lower()) && !is_extreme(get_upper()) && + equal(get_lower(), get_upper()); +} + +bool constant_interval_exprt::contains_zero() const +{ + if(!is_numeric()) + { + return false; + } + + if(get_lower().is_zero() || get_upper().is_zero()) + { + return true; + } + + if(is_unsigned() && is_min(get_lower())) + { + return true; + } + + if( + less_than_or_equal(get_lower(), zero()) && + greater_than_or_equal(get_upper(), zero())) + { + return true; + } + + return false; +} + +bool constant_interval_exprt::is_positive( + const constant_interval_exprt &interval) +{ + return interval.is_positive(); +} + +bool constant_interval_exprt::is_zero(const constant_interval_exprt &interval) +{ + return interval.is_zero(); +} + +bool constant_interval_exprt::is_negative( + const constant_interval_exprt &interval) +{ + return interval.is_negative(); +} + +bool constant_interval_exprt::is_positive() const +{ + return is_positive(get_lower()) && is_positive(get_upper()); +} + +bool constant_interval_exprt::is_zero() const +{ + return is_zero(get_lower()) && is_zero(get_upper()); +} + +bool constant_interval_exprt::is_negative() const +{ + return is_negative(get_lower()) && is_negative(get_upper()); +} + +tvt constant_interval_exprt::is_true(const constant_interval_exprt &a) +{ + return a.is_definitely_true(); +} + +tvt constant_interval_exprt::is_false(const constant_interval_exprt &a) +{ + return a.is_definitely_false(); +} + +tvt constant_interval_exprt::logical_and( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.logical_and(b); +} + +tvt constant_interval_exprt::logical_or( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.logical_or(b); +} + +tvt constant_interval_exprt::logical_xor( + const constant_interval_exprt &a, + const constant_interval_exprt &b) +{ + return a.logical_xor(b); +} + +tvt constant_interval_exprt::logical_not(const constant_interval_exprt &a) +{ + return a.logical_not(); +} + +constant_interval_exprt constant_interval_exprt::tvt_to_interval(const tvt &val) +{ + if(val.is_true()) + { + return constant_interval_exprt(true_exprt()); + } + else if(val.is_false()) + { + return constant_interval_exprt(false_exprt()); + } + else + { + return constant_interval_exprt(bool_typet()); + } +} diff --git a/src/util/interval.h b/src/util/interval.h new file mode 100644 index 00000000000..cadb323f19c --- /dev/null +++ b/src/util/interval.h @@ -0,0 +1,472 @@ +/*******************************************************************\ + + Module: intervals + + Author: Daniel Neville (2017) + +\*******************************************************************/ +#ifndef CPROVER_UTIL_INTERVAL_H +#define CPROVER_UTIL_INTERVAL_H + +#include +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include + +/// +∞ upper bound for intervals +class max_exprt : public exprt +{ +public: + explicit max_exprt(const typet &_type) : exprt(ID_max, _type) + { + } + + explicit max_exprt(const exprt &_expr) : exprt(ID_max, _expr.type()) + { + } +}; + +/// -∞ upper bound for intervals +class min_exprt : public exprt +{ +public: + explicit min_exprt(const typet &_type) : exprt(ID_min, _type) + { + } + + explicit min_exprt(const exprt &_expr) : exprt(ID_min, _expr.type()) + { + } +}; + +/// Represents an interval of values. +/// Bounds should be constant expressions +/// or min_exprt for the lower bound +/// or max_exprt for the upper bound +/// Also, lower bound should always be <= upper bound +class constant_interval_exprt : public binary_exprt +{ +public: + constant_interval_exprt( + const exprt &lower, + const exprt &upper, + const typet type) + : binary_exprt(lower, ID_constant_interval, upper, type) + { + PRECONDITION(is_well_formed()); + } + + constant_interval_exprt(const constant_interval_exprt &x) + : constant_interval_exprt(x.get_lower(), x.get_upper(), x.type()) + { + } + + explicit constant_interval_exprt(const exprt &x) + : constant_interval_exprt(x, x, x.type()) + { + } + + explicit constant_interval_exprt(const typet &type) + : constant_interval_exprt(min_exprt(type), max_exprt(type), type) + { + } + + constant_interval_exprt(const exprt &lower, const exprt &upper) + : constant_interval_exprt(lower, upper, lower.type()) + { + } + + bool is_well_formed() const + { + bool b = true; + + const typet &type = this->type(); + const exprt &lower = get_lower(); + const exprt &upper = get_upper(); + + b &= is_numeric() || type.id() == ID_bool || type.is_nil(); + + b &= type == lower.type(); + b &= type == upper.type(); + + b &= is_valid_bound(lower); + b &= is_valid_bound(upper); + + b &= !is_numeric() || is_bottom() || less_than_or_equal(lower, upper); + + return b; + } + + bool is_valid_bound(const exprt &expr) const + { + const irep_idt &id = expr.id(); + + bool b = true; + + b &= id == ID_constant || id == ID_min || id == ID_max; + + if(type().id() == ID_bool && id == ID_constant) + { + b &= expr == true_exprt() || expr == false_exprt(); + } + + return b; + } + + static constant_interval_exprt tvt_to_interval(const tvt &val); + + /* Naming scheme + * is_[X]? Returns bool / tvt + * get_[X]? Returns relevant object + * [X] Generator of some object. + * generate_[X] generator used for evaluation + */ + + /* Getters */ + const exprt &get_lower() const; + const exprt &get_upper() const; + + /** SET OF ARITHMETIC OPERATORS */ + constant_interval_exprt + handle_constant_unary_expression(const irep_idt &op) const; + constant_interval_exprt handle_constant_binary_expression( + const constant_interval_exprt &other, + const irep_idt &) const; + + constant_interval_exprt eval(const irep_idt &unary_operator) const; + constant_interval_exprt + eval(const irep_idt &binary_operator, const constant_interval_exprt &o) const; + + /* Unary arithmetic */ + constant_interval_exprt unary_plus() const; + constant_interval_exprt unary_minus() const; + + constant_interval_exprt typecast(const typet &type) const; + + /* Logical */ + tvt is_definitely_true() const; + tvt is_definitely_false() const; + + tvt logical_and(const constant_interval_exprt &o) const; + tvt logical_or(const constant_interval_exprt &o) const; + tvt logical_xor(const constant_interval_exprt &o) const; + tvt logical_not() const; + + /* Binary */ + constant_interval_exprt plus(const constant_interval_exprt &o) const; + constant_interval_exprt minus(const constant_interval_exprt &other) const; + constant_interval_exprt multiply(const constant_interval_exprt &o) const; + constant_interval_exprt divide(const constant_interval_exprt &o) const; + constant_interval_exprt modulo(const constant_interval_exprt &o) const; + + /* Binary shifts */ + constant_interval_exprt left_shift(const constant_interval_exprt &o) const; + constant_interval_exprt right_shift(const constant_interval_exprt &o) const; + + /* Unary bitwise */ + constant_interval_exprt bitwise_not() const; + + /* Binary bitwise */ + constant_interval_exprt bitwise_xor(const constant_interval_exprt &o) const; + constant_interval_exprt bitwise_or(const constant_interval_exprt &o) const; + constant_interval_exprt bitwise_and(const constant_interval_exprt &o) const; + + tvt less_than(const constant_interval_exprt &o) const; + tvt greater_than(const constant_interval_exprt &o) const; + tvt less_than_or_equal(const constant_interval_exprt &o) const; + tvt greater_than_or_equal(const constant_interval_exprt &o) const; + tvt equal(const constant_interval_exprt &o) const; + tvt not_equal(const constant_interval_exprt &o) const; + + constant_interval_exprt increment() const; + constant_interval_exprt decrement() const; + + bool is_empty() const; + bool is_single_value_interval() const; + /** END SET OF ARITHMETIC OPERATORS */ + + // tvt contains(constant_interval_exprt &o) const; + + /* SET OF EXPR COMPARATORS */ + static bool equal(const exprt &a, const exprt &b); + static bool not_equal(const exprt &a, const exprt &b); + static bool less_than(const exprt &a, const exprt &b); + static bool less_than_or_equal(const exprt &a, const exprt &b); + static bool greater_than(const exprt &a, const exprt &b); + static bool greater_than_or_equal(const exprt &a, const exprt &b); + /* END SET OF EXPR COMPS */ + + /* INTERVAL COMPARISONS, returns tvt.is_true(). False cannot be trusted + * (could be false or unknown, either use less_than, etc method or use the correct + * operator)! */ + friend bool operator<( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend bool operator>( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend bool operator<=( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend bool operator>=( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend bool operator==( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend bool operator!=( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + + /* Operator override for intervals */ + friend const constant_interval_exprt operator+( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend const constant_interval_exprt operator-( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend const constant_interval_exprt operator/( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend const constant_interval_exprt operator*( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend const constant_interval_exprt operator%( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend const constant_interval_exprt operator!( + const constant_interval_exprt &lhs); + friend const constant_interval_exprt operator&( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend const constant_interval_exprt operator|( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend const constant_interval_exprt operator^( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend const constant_interval_exprt operator<<( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + friend const constant_interval_exprt operator>>( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + + friend std::ostream & + operator<<(std::ostream &out, const constant_interval_exprt &i); + std::string to_string() const; + + /* Now static equivalents! */ + static tvt is_true(const constant_interval_exprt &a); + static tvt is_false(const constant_interval_exprt &a); + + static tvt logical_and( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + static tvt logical_or( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + static tvt logical_xor( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + static tvt logical_not(const constant_interval_exprt &a); + + static constant_interval_exprt unary_plus(const constant_interval_exprt &a); + static constant_interval_exprt unary_minus(const constant_interval_exprt &a); + + /* Binary */ + static constant_interval_exprt + plus(const constant_interval_exprt &a, const constant_interval_exprt &b); + static constant_interval_exprt + minus(const constant_interval_exprt &a, const constant_interval_exprt &b); + static constant_interval_exprt + multiply(const constant_interval_exprt &a, const constant_interval_exprt &b); + static constant_interval_exprt + divide(const constant_interval_exprt &a, const constant_interval_exprt &b); + static constant_interval_exprt + modulo(const constant_interval_exprt &a, const constant_interval_exprt &b); + + /* Binary shifts */ + static constant_interval_exprt left_shift( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + static constant_interval_exprt right_shift( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + + /* Unary bitwise */ + static constant_interval_exprt bitwise_not(const constant_interval_exprt &a); + + /* Binary bitwise */ + static constant_interval_exprt bitwise_xor( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + static constant_interval_exprt bitwise_or( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + static constant_interval_exprt bitwise_and( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + + static tvt + less_than(const constant_interval_exprt &a, const constant_interval_exprt &b); + static tvt greater_than( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + static tvt less_than_or_equal( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + static tvt greater_than_or_equal( + const constant_interval_exprt &a, + const constant_interval_exprt &b); + static tvt + equal(const constant_interval_exprt &a, const constant_interval_exprt &b); + static tvt + not_equal(const constant_interval_exprt &a, const constant_interval_exprt &b); + + static constant_interval_exprt increment(const constant_interval_exprt &a); + static constant_interval_exprt decrement(const constant_interval_exprt &a); + + static bool is_empty(const constant_interval_exprt &a); + static bool is_single_value_interval(const constant_interval_exprt &a); + + static bool is_top(const constant_interval_exprt &a); + static bool is_bottom(const constant_interval_exprt &a); + + static bool is_min(const constant_interval_exprt &a); + static bool is_max(const constant_interval_exprt &a); + /* End static equivalents */ + + bool is_top() const; + bool is_bottom() const; + static constant_interval_exprt top(const typet &type); + static constant_interval_exprt bottom(const typet &type); + constant_interval_exprt top() const; + constant_interval_exprt bottom() const; + + bool has_no_lower_bound() const; + bool has_no_upper_bound() const; + static bool is_min(const exprt &expr); + static bool is_max(const exprt &expr); + + /* Generate min and max exprt according to current type */ + min_exprt min() const; + max_exprt max() const; + + constant_exprt zero() const; + static constant_exprt zero(const typet &type); + static constant_exprt zero(const exprt &expr); + static constant_exprt zero(const constant_interval_exprt &interval); + + /* Private? */ + static constant_interval_exprt get_extremes( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs, + const irep_idt &operation); + static exprt get_extreme(std::vector values, bool min = true); + static exprt get_max(const exprt &a, const exprt &b); + static exprt get_min(const exprt &a, const exprt &b); + static exprt get_min(std::vector &values); + static exprt get_max(std::vector &values); + + /* we don't simplify in the constructor otherwise */ + static constant_interval_exprt simplified_interval(exprt &l, exprt &r); + static exprt simplified_expr(exprt expr); + + /* Helpers */ + /* Four common params: self, static: type, expr, interval */ + + bool is_numeric() const; + static bool is_numeric(const typet &type); + static bool is_numeric(const exprt &expr); + static bool is_numeric(const constant_interval_exprt &interval); + + bool is_int() const; + static bool is_int(const typet &type); + static bool is_int(const exprt &expr); + static bool is_int(const constant_interval_exprt &interval); + + bool is_float() const; + static bool is_float(const typet &type); + static bool is_float(const exprt &expr); + static bool is_float(const constant_interval_exprt &interval); + + bool is_bitvector() const; + static bool is_bitvector(const typet &type); + static bool is_bitvector(const constant_interval_exprt &interval); + static bool is_bitvector(const exprt &expr); + + bool is_signed() const; + static bool is_signed(const typet &type); + static bool is_signed(const exprt &expr); + static bool is_signed(const constant_interval_exprt &interval); + + bool is_unsigned() const; + static bool is_unsigned(const typet &type); + static bool is_unsigned(const exprt &expr); + static bool is_unsigned(const constant_interval_exprt &interval); + + bool contains_zero() const; + bool contains(const constant_interval_exprt &interval) const; + + static bool is_extreme(const exprt &expr); + static bool is_extreme(const exprt &expr1, const exprt &expr2); + + static bool contains_extreme(const exprt expr); + static bool contains_extreme(const exprt expr1, const exprt expr2); + + bool is_positive() const; + static bool is_positive(const exprt &expr); + static bool is_positive(const constant_interval_exprt &interval); + + bool is_zero() const; + static bool is_zero(const exprt &expr); + static bool is_zero(const constant_interval_exprt &interval); + + bool is_negative() const; + static bool is_negative(const exprt &expr); + static bool is_negative(const constant_interval_exprt &interval); + + static exprt abs(const exprt &expr); + +private: + static void generate_expression( + const exprt &lhs, + const exprt &rhs, + const irep_idt &operation, + std::vector &collection); + static void append_multiply_expression( + const exprt &lower, + const exprt &upper, + std::vector &collection); + static void append_multiply_expression_max( + const exprt &expr, + std::vector &collection); + static void append_multiply_expression_min( + const exprt &min, + const exprt &other, + std::vector &collection); + static exprt generate_division_expression(const exprt &lhs, const exprt &rhs); + static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs); + static exprt generate_shift_expression( + const exprt &lhs, + const exprt &rhs, + const irep_idt &operation); +}; + +inline const constant_interval_exprt & +to_constant_interval_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_constant_interval); + return static_cast(expr); +} + +#endif /* SRC_ANALYSES_INTERVAL_H_ */ diff --git a/src/util/interval_template.h b/src/util/interval_template.h index c6a3e64b0ef..d002db72424 100644 --- a/src/util/interval_template.h +++ b/src/util/interval_template.h @@ -143,6 +143,47 @@ template class interval_templatet } } + void make_bottom() + { + lower_set = upper_set = true; + upper = T(); + lower = upper + 1; + } + + void make_less_than_eq(interval_templatet &i) + { + if(upper_set && i.upper_set) + upper = std::min(upper, i.upper); + if(lower_set && i.lower_set) + i.lower = std::max(lower, i.lower); + } + + void make_less_than(interval_templatet &i) + { + make_less_than_eq(i); + if(singleton() && i.singleton() && lower == i.lower) + { + make_bottom(); + i.make_bottom(); + } + } + + bool is_less_than_eq(const interval_templatet &i) + { + if(i.lower_set && upper_set && upper <= i.lower) + return true; + else + return false; + } + + bool is_less_than(const interval_templatet &i) + { + if(i.lower_set && upper_set && upper < i.lower) + return true; + else + return false; + } + void approx_union_with(const interval_templatet &i) { if(i.lower_set && lower_set) @@ -230,16 +271,22 @@ template std::ostream &operator << (std::ostream &out, const interval_templatet &i) { if(i.lower_set) - out << '[' << i.lower; + { + out << "["; + out << i.lower; + } else - out << ")-INF"; + out << "(-INF"; - out << ','; + out << ","; if(i.upper_set) - out << i.upper << ']'; + { + out << i.upper; + out << "]"; + } else - out << "+INF("; + out << "+INF)"; return out; } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 2e286e0ba64..5b705b2adff 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -834,6 +834,9 @@ IREP_ID_ONE(statement_list_reset) IREP_ID_ONE(statement_list_not) IREP_ID_ONE(statement_list_instruction) IREP_ID_ONE(statement_list_instructions) +IREP_ID_ONE(max) +IREP_ID_ONE(min) +IREP_ID_ONE(constant_interval) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree diff --git a/unit/Makefile b/unit/Makefile index ed549005358..c22e07f423b 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -72,6 +72,14 @@ SRC += analyses/ai/ai.cpp \ util/format_number_range.cpp \ util/get_base_name.cpp \ util/graph.cpp \ + util/interval/multiply.cpp \ + util/interval/add.cpp \ + util/interval/get_extreme.cpp \ + util/interval/subtract.cpp \ + util/interval/modulo.cpp \ + util/interval/shift.cpp \ + util/interval/comparisons.cpp \ + util/interval/bitwise.cpp \ util/interval_constraint.cpp \ util/interval_union.cpp \ util/irep.cpp \ diff --git a/unit/util/interval/add.cpp b/unit/util/interval/add.cpp new file mode 100644 index 00000000000..73aee75759f --- /dev/null +++ b/unit/util/interval/add.cpp @@ -0,0 +1,95 @@ +/*******************************************************************\ + Module: Unit tests for variable/sensitivity/abstract_object::merge + Author: DiffBlue Limited +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +#define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) +#define V_(X) (bvrep2integer(X.c_str(), 32, true)) +#define CEV(X) (from_integer(mp_integer(X), signedbv_typet(32))) + +SCENARIO("add interval domain", "[core][analyses][interval][add]") +{ + GIVEN("Two simple signed intervals") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + WHEN("Both are positive [2,4]+[6,8]") + { + constant_interval_exprt left(CEV(2), CEV(4)); + constant_interval_exprt right(CEV(6), CEV(8)); + + constant_interval_exprt result = left.plus(right); + + THEN("Domain is consistent") + { + REQUIRE(V(left.get_lower()) == 2); + REQUIRE(V(left.get_upper()) == 4); + REQUIRE(V(right.get_lower()) == 6); + REQUIRE(V(right.get_upper()) == 8); + } + + THEN("The result is [8, 12]") + { + REQUIRE(V(result.get_lower()) == 8); + REQUIRE(V(result.get_upper()) == 12); + } + } + + WHEN("One contains infinite [2,4]+[6,INF]") + { + constant_interval_exprt left(CEV(2), CEV(4)); + constant_interval_exprt right(CEV(6), max_exprt(signedbv_typet(32))); + + constant_interval_exprt result = left.plus(right); + + THEN("Domain is consistent") + { + REQUIRE(V(left.get_lower()) == 2); + REQUIRE(V(left.get_upper()) == 4); + REQUIRE(V(right.get_lower()) == 6); + REQUIRE(right.has_no_upper_bound()); + } + + CAPTURE(result); + + THEN("The result is [8, MAX]") + { + REQUIRE(V(result.get_lower()) == 8); + REQUIRE(result.has_no_upper_bound()); + } + } + + WHEN("Both contain infinite [2,INF]+[6,INF]") + { + constant_interval_exprt left(CEV(2), max_exprt(signedbv_typet(32))); + constant_interval_exprt right(CEV(6), max_exprt(signedbv_typet(32))); + + constant_interval_exprt result = left.plus(right); + + THEN("Domain is consistent") + { + REQUIRE(V(left.get_lower()) == 2); + REQUIRE(left.has_no_upper_bound()); + REQUIRE(V(right.get_lower()) == 6); + REQUIRE(right.has_no_upper_bound()); + } + + CAPTURE(result); + + THEN("The result is [8, MAX]") + { + REQUIRE(V(result.get_lower()) == 8); + REQUIRE(result.has_no_upper_bound()); + } + } + } +} diff --git a/unit/util/interval/bitwise.cpp b/unit/util/interval/bitwise.cpp new file mode 100644 index 00000000000..8737956ff5e --- /dev/null +++ b/unit/util/interval/bitwise.cpp @@ -0,0 +1,64 @@ +/*******************************************************************\ + Module: Unit tests for variable/sensitivity/abstract_object::merge + Author: DiffBlue Limited +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +SCENARIO("bitwise interval domain", "[core][analyses][interval][bitwise]") +{ + WHEN("We have two unsigned single value intervals - 5 and 9") + { + const unsignedbv_typet &unsigned_int = unsignedbv_typet(32); + constant_interval_exprt five = + constant_interval_exprt(from_integer(5, unsigned_int)); + constant_interval_exprt nine = + constant_interval_exprt(from_integer(9, unsigned_int)); + + THEN("Bitwise or should yield bitwise representation of 13") + { + REQUIRE( + five.bitwise_or(nine) == + constant_interval_exprt(from_integer(13, unsigned_int))); + } + + THEN("Bitwise and should yield bitwise representation of 1") + { + REQUIRE( + five.bitwise_and(nine) == + constant_interval_exprt(from_integer(1, unsigned_int))); + REQUIRE( + (five & nine) == + constant_interval_exprt(from_integer(1, unsigned_int))); + } + + THEN("Bitwise xor should yield bitwise representation of 12") + { + REQUIRE( + five.bitwise_xor(nine) == + constant_interval_exprt(from_integer(12, unsigned_int))); + } + + THEN("Left shift on the 5 should produce 10") + { + REQUIRE( + five.left_shift( + constant_interval_exprt(from_integer(1, unsigned_int))) == + constant_interval_exprt(from_integer(10, unsigned_int))); + } + + THEN("Right shift on the 5 should produce 2") + { + REQUIRE( + five.right_shift( + constant_interval_exprt(from_integer(1, unsigned_int))) == + constant_interval_exprt(from_integer(2, unsigned_int))); + } + } +} diff --git a/unit/util/interval/comparisons.cpp b/unit/util/interval/comparisons.cpp new file mode 100644 index 00000000000..1a838bc0dd1 --- /dev/null +++ b/unit/util/interval/comparisons.cpp @@ -0,0 +1,208 @@ +/*******************************************************************\ + Module: Unit tests for variable/sensitivity/abstract_object::merge + Author: DiffBlue Limited +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +#define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) +#define V_(X) (bvrep2integer(X.c_str(), 32, true)) +#define CEV(X) (from_integer(mp_integer(X), signedbv_typet(32))) + +SCENARIO("comparison interval domain", "[core][analyses][interval][comparison]") +{ + GIVEN("Two simple signed intervals") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + WHEN("<, >, <=, >=, ==, != are tested on expressions") + { + THEN("Require correctness") + { + REQUIRE(constant_interval_exprt::less_than(CEV(0), CEV(1))); + REQUIRE(constant_interval_exprt::less_than(CEV(1), CEV(2))); + REQUIRE(constant_interval_exprt::less_than(CEV(1), CEV(100))); + + REQUIRE(constant_interval_exprt::less_than(CEV(-10), CEV(1))); + REQUIRE_FALSE(constant_interval_exprt::less_than(CEV(-10), CEV(-100))); + REQUIRE(constant_interval_exprt::less_than(CEV(-10), CEV(-5))); + REQUIRE(constant_interval_exprt::less_than( + CEV(-10), max_exprt(signedbv_typet(32)))); + REQUIRE(constant_interval_exprt::less_than( + CEV(10), max_exprt(signedbv_typet(32)))); + REQUIRE(constant_interval_exprt::less_than( + CEV(0), max_exprt(signedbv_typet(32)))); + + REQUIRE_FALSE(constant_interval_exprt::less_than( + CEV(-10), min_exprt(signedbv_typet(32)))); + REQUIRE_FALSE(constant_interval_exprt::less_than( + CEV(10), min_exprt(signedbv_typet(32)))); + REQUIRE_FALSE(constant_interval_exprt::less_than( + CEV(0), min_exprt(signedbv_typet(32)))); + + REQUIRE_FALSE(constant_interval_exprt::less_than( + min_exprt(signedbv_typet(32)), min_exprt(signedbv_typet(32)))); + REQUIRE_FALSE(constant_interval_exprt::less_than( + max_exprt(signedbv_typet(32)), min_exprt(signedbv_typet(32)))); + REQUIRE_FALSE(constant_interval_exprt::less_than( + max_exprt(signedbv_typet(32)), max_exprt(signedbv_typet(32)))); + REQUIRE(constant_interval_exprt::less_than( + min_exprt(signedbv_typet(32)), max_exprt(signedbv_typet(32)))); + + REQUIRE(constant_interval_exprt::equal( + min_exprt(signedbv_typet(32)), min_exprt(signedbv_typet(32)))); + REQUIRE(constant_interval_exprt::not_equal( + max_exprt(signedbv_typet(32)), min_exprt(signedbv_typet(32)))); + REQUIRE(constant_interval_exprt::equal( + max_exprt(signedbv_typet(32)), max_exprt(signedbv_typet(32)))); + REQUIRE(constant_interval_exprt::not_equal( + min_exprt(signedbv_typet(32)), max_exprt(signedbv_typet(32)))); + } + + THEN("") + { + REQUIRE_FALSE(constant_interval_exprt::greater_than(CEV(0), CEV(1))); + REQUIRE_FALSE(constant_interval_exprt::greater_than(CEV(1), CEV(2))); + REQUIRE_FALSE(constant_interval_exprt::greater_than(CEV(1), CEV(100))); + + REQUIRE_FALSE(constant_interval_exprt::greater_than(CEV(-10), CEV(1))); + REQUIRE(constant_interval_exprt::greater_than(CEV(-10), CEV(-100))); + REQUIRE_FALSE(constant_interval_exprt::greater_than(CEV(-10), CEV(-5))); + REQUIRE_FALSE(constant_interval_exprt::greater_than( + CEV(-10), max_exprt(signedbv_typet(32)))); + REQUIRE_FALSE(constant_interval_exprt::greater_than( + CEV(10), max_exprt(signedbv_typet(32)))); + REQUIRE_FALSE(constant_interval_exprt::greater_than( + CEV(0), max_exprt(signedbv_typet(32)))); + + REQUIRE(constant_interval_exprt::greater_than( + CEV(-10), min_exprt(signedbv_typet(32)))); + REQUIRE(constant_interval_exprt::greater_than( + CEV(10), min_exprt(signedbv_typet(32)))); + REQUIRE(constant_interval_exprt::greater_than( + CEV(0), min_exprt(signedbv_typet(32)))); + + REQUIRE_FALSE(constant_interval_exprt::greater_than( + min_exprt(signedbv_typet(32)), min_exprt(signedbv_typet(32)))); + REQUIRE(constant_interval_exprt::greater_than_or_equal( + min_exprt(signedbv_typet(32)), min_exprt(signedbv_typet(32)))); + + REQUIRE(constant_interval_exprt::greater_than( + max_exprt(signedbv_typet(32)), min_exprt(signedbv_typet(32)))); + REQUIRE(constant_interval_exprt::greater_than_or_equal( + max_exprt(signedbv_typet(32)), min_exprt(signedbv_typet(32)))); + + REQUIRE_FALSE(constant_interval_exprt::greater_than( + max_exprt(signedbv_typet(32)), max_exprt(signedbv_typet(32)))); + + REQUIRE_FALSE(constant_interval_exprt::greater_than( + min_exprt(signedbv_typet(32)), max_exprt(signedbv_typet(32)))); + } + } + + WHEN("<, >, <=, >=, ==, != are tested on intervals") + { + THEN("Require correctness") + { + CHECK( + constant_interval_exprt(CEV(10), CEV(20)) < + constant_interval_exprt(CEV(30), CEV(40))); + REQUIRE_FALSE( + constant_interval_exprt(CEV(10), CEV(30)) < + constant_interval_exprt(CEV(30), CEV(40))); + REQUIRE_FALSE( + constant_interval_exprt(CEV(10), CEV(20)) > + constant_interval_exprt(CEV(30), CEV(40))); + } + + THEN( + "[10, 29] < [30, 40] == true, [10, 30] < [30, 40] == unknown, [10, 31] " + "< [30, 40] == unknown") + { + CHECK( + constant_interval_exprt(CEV(10), CEV(29)) + .less_than(constant_interval_exprt(CEV(30), CEV(40))) == tvt(true)); + CHECK( + constant_interval_exprt(CEV(10), CEV(30)) + .less_than(constant_interval_exprt(CEV(30), CEV(40))) == + tvt::unknown()); + CHECK( + constant_interval_exprt(CEV(10), CEV(31)) + .less_than(constant_interval_exprt(CEV(30), CEV(40))) == + tvt::unknown()); + + CHECK( + constant_interval_exprt(CEV(30), CEV(40)) + .less_than(constant_interval_exprt(CEV(10), CEV(29))) == + tvt(false)); + } + + THEN( + "[10, 29] > [30, 40] == false, [10, 30] > [30, 40] == unknown, [10, " + "31] > [30, 40] == unknown") + { + CHECK( + constant_interval_exprt(CEV(10), CEV(29)) + .greater_than(constant_interval_exprt(CEV(30), CEV(40))) == + tvt(false)); + CHECK( + constant_interval_exprt(CEV(10), CEV(29)) + .greater_than(constant_interval_exprt(CEV(30), CEV(40))) == + constant_interval_exprt(CEV(30), CEV(40)) + .less_than(constant_interval_exprt(CEV(10), CEV(29)))); + + CHECK( + constant_interval_exprt(CEV(10), CEV(30)) + .greater_than(constant_interval_exprt(CEV(30), CEV(40))) == + tvt::unknown()); + CHECK( + constant_interval_exprt(CEV(10), CEV(31)) + .greater_than(constant_interval_exprt(CEV(30), CEV(40))) == + tvt::unknown()); + } + + THEN( + "[10, 29] <= [30, 40] == true, [10, 30] <= [30, 40] == true, [10, 31] " + "<- [30, 40] == unknown") + { + CHECK( + constant_interval_exprt(CEV(10), CEV(29)) + .less_than_or_equal(constant_interval_exprt(CEV(30), CEV(40))) == + tvt(true)); + CHECK( + constant_interval_exprt(CEV(10), CEV(30)) + .less_than_or_equal(constant_interval_exprt(CEV(30), CEV(40))) == + tvt(true)); + CHECK( + constant_interval_exprt(CEV(10), CEV(31)) + .less_than_or_equal(constant_interval_exprt(CEV(30), CEV(40))) == + tvt::unknown()); + } + + THEN( + "[10, 29] >= [30, 40] == false, [10, 30] >= [30, 40] == unknown, [10, " + "31] >= [30, 40] == unknown") + { + CHECK( + constant_interval_exprt(CEV(10), CEV(29)) + .greater_than_or_equal(constant_interval_exprt(CEV(30), CEV(40))) == + tvt(false)); + CHECK( + constant_interval_exprt(CEV(10), CEV(30)) + .greater_than_or_equal(constant_interval_exprt(CEV(30), CEV(40))) == + tvt::unknown()); + CHECK( + constant_interval_exprt(CEV(10), CEV(31)) + .greater_than_or_equal(constant_interval_exprt(CEV(30), CEV(40))) == + tvt::unknown()); + } + } + } +} diff --git a/unit/util/interval/divide.cpp b/unit/util/interval/divide.cpp new file mode 100644 index 00000000000..e69de29bb2d diff --git a/unit/util/interval/eval.cpp b/unit/util/interval/eval.cpp new file mode 100644 index 00000000000..d39b6894945 --- /dev/null +++ b/unit/util/interval/eval.cpp @@ -0,0 +1,65 @@ +/*******************************************************************\ + Module: Unit tests for intervals + Author: DiffBlue Limited +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +SCENARIO("Unary eval on intervals", "[core][analyses][interval][eval]") +{ + WHEN("Negating a boolean interval") + { + constant_interval_exprt true_interval = + constant_interval_exprt(true_exprt()); + constant_interval_exprt false_interval = + constant_interval_exprt(false_exprt()); + constant_interval_exprt bool_top_interval = + constant_interval_exprt(bool_typet()); + + THEN("True interval negated should equal the false interval") + { + REQUIRE(true_interval.eval(ID_not) == false_interval); + } + THEN("False interval negated should equal the true interval") + { + REQUIRE(false_interval.eval(ID_not) == true_interval); + } + THEN("An unknown boolean type should equal top (itself)") + { + REQUIRE(bool_top_interval.eval(ID_not) == bool_top_interval); + } + } + + WHEN("Unary operations to an interval") + { + constant_interval_exprt five = + constant_interval_exprt(from_integer(5, signedbv_typet(32))); + + THEN("When we apply unary addition to it, nothing should happen") + { + REQUIRE(five.eval(ID_unary_plus) == five); + } + + THEN("When we apply unary subtraction to it, it should be negated") + { + auto negated_val = + numeric_cast(five.eval(ID_unary_minus).get_lower()); + REQUIRE(negated_val.has_value()); + REQUIRE(negated_val.value() == -5); + } + + THEN("When we apply bitwise negation to it, is should be bitwise negated") + { + auto bitwise_negated_val = + numeric_cast(five.eval(ID_bitnot).get_lower()); + REQUIRE(bitwise_negated_val.has_value()); + REQUIRE(bitwise_negated_val.value() == (~5)); + } + } +} diff --git a/unit/util/interval/get_extreme.cpp b/unit/util/interval/get_extreme.cpp new file mode 100644 index 00000000000..71ada31d94a --- /dev/null +++ b/unit/util/interval/get_extreme.cpp @@ -0,0 +1,161 @@ +/*******************************************************************\ + Module: Unit tests for variable/sensitivity/abstract_object::merge + Author: DiffBlue Limited +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include +#include + +#define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) +#define V_(X) (bvrep2integer(X.c_str(), 32, true)) +#define CEV(X) (from_integer(mp_integer(X), signedbv_typet(32))) + +SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]") +{ + GIVEN("A selection of constant_exprts in a std::vector and map") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + std::vector ve; + + for(int i = -100; i <= 100; i++) + { + ve.push_back(from_integer(mp_integer(i), signedbv_typet(32))); + } + WHEN("-20 <= 20 is tested") + { + binary_predicate_exprt op1(CEV(-20), ID_le, CEV(20)); + bool interval_eval = + constant_interval_exprt::less_than_or_equal(CEV(-20), CEV(20)); + simplify(op1, ns); + + THEN("Require it is TRUE") + { + REQUIRE(op1.is_true()); + REQUIRE(interval_eval); + } + } + + WHEN("20 <= -20 is tested") + { + binary_predicate_exprt op1(CEV(20), ID_le, CEV(-20)); + bool interval_eval = + constant_interval_exprt::less_than_or_equal(CEV(20), CEV(-20)); + simplify(op1, ns); + + THEN("Require it is FALSE") + { + REQUIRE(op1.is_false()); + REQUIRE_FALSE(interval_eval); + } + } + + WHEN("-20 <= -20 is tested") + { + binary_predicate_exprt op1(CEV(-20), ID_le, CEV(-20)); + bool interval_eval = + constant_interval_exprt::less_than_or_equal(CEV(-20), CEV(-20)); + + simplify(op1, ns); + + THEN("Require it is TRUE") + { + REQUIRE(op1.is_true()); + REQUIRE(interval_eval); + REQUIRE(constant_interval_exprt::equal(CEV(1), CEV(1))); + } + } + + WHEN("Two are selected and min found [20, -20]") + { + std::vector selected = {CEV(20), CEV(-20)}; + + exprt min = constant_interval_exprt::get_extreme(selected, true); + exprt max = constant_interval_exprt::get_extreme(selected, false); + + THEN("Min (-20) and max (20) are verified") + { + CAPTURE(min.pretty()); + + REQUIRE(V(min) == -20); + REQUIRE(V(max) == 20); + } + } + + WHEN("Four are selected and min found [-20, 0, 20, 50]") + { + std::vector selected = {CEV(-20), CEV(0), CEV(50), CEV(20)}; + + exprt min = constant_interval_exprt::get_extreme(selected, true); + exprt max = constant_interval_exprt::get_extreme(selected, false); + + THEN("Min (-20) and max (50) are verified") + { + REQUIRE(V(min) == -20); + REQUIRE(V(max) == 50); + } + } + + WHEN("One is selected [-100]") + { + std::vector selected = {CEV(-100)}; + + exprt min = constant_interval_exprt::get_extreme(selected, true); + exprt max = constant_interval_exprt::get_extreme(selected, false); + + THEN("Max (-100) and min (-100) are verified") + { + REQUIRE(V(min) == -100); + REQUIRE(V(max) == -100); + } + } + + WHEN("Five are selected [20, 30, 15, 0, -100]") + { + std::vector selected = { + CEV(20), CEV(30), CEV(15), CEV(0), CEV(-100)}; + + exprt min = constant_interval_exprt::get_extreme(selected, true); + exprt max = constant_interval_exprt::get_extreme(selected, false); + + THEN("Max (30) and min (-100) are verified") + { + REQUIRE(V(min) == -100); + REQUIRE(V(max) == 30); + } + } + + WHEN("All from [-100:100] are selected") + { + exprt min = constant_interval_exprt::get_extreme(ve, true); + exprt max = constant_interval_exprt::get_extreme(ve, false); + + THEN("Max (100) and min (-100) are verified") + { + REQUIRE(V(min) == -100); + REQUIRE(V(max) == 100); + } + } + + WHEN("All from [-100:100] are shuffled and selected") + { + std::random_shuffle(ve.begin(), ve.end()); + + exprt min = constant_interval_exprt::get_extreme(ve, true); + exprt max = constant_interval_exprt::get_extreme(ve, false); + + THEN("Max (100) and min (-100) are verified") + { + REQUIRE(V(min) == -100); + REQUIRE(V(max) == 100); + } + } + } +} diff --git a/unit/util/interval/module_dependencies.txt b/unit/util/interval/module_dependencies.txt new file mode 100644 index 00000000000..253b4a5d0f0 --- /dev/null +++ b/unit/util/interval/module_dependencies.txt @@ -0,0 +1,3 @@ +testing-utils +util + diff --git a/unit/util/interval/modulo.cpp b/unit/util/interval/modulo.cpp new file mode 100644 index 00000000000..0095e473c10 --- /dev/null +++ b/unit/util/interval/modulo.cpp @@ -0,0 +1,73 @@ +/*******************************************************************\ + Module: Unit tests for variable/sensitivity/abstract_object::merge + Author: DiffBlue Limited +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +#define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) +#define V_(X) (bvrep2integer(X.c_str(), 32, true)) +#define CEV(X) (from_integer(mp_integer(X), signedbv_typet(32))) + +SCENARIO("modulo interval domain", "[core][analyses][interval][modulo]") +{ + GIVEN("Two simple signed intervals") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + WHEN("Positive RHS") + { + THEN("Ensure result is consistent.") + { + REQUIRE( + constant_interval_exprt(CEV(10), CEV(20)) + .modulo(constant_interval_exprt(CEV(5), CEV(5))) == + constant_interval_exprt(CEV(0), CEV(4))); + REQUIRE( + constant_interval_exprt(CEV(10), CEV(20)) + .modulo(constant_interval_exprt(CEV(4), CEV(5))) == + constant_interval_exprt(CEV(0), CEV(4))); + REQUIRE( + constant_interval_exprt(CEV(10), CEV(20)) + .modulo(constant_interval_exprt(CEV(0), CEV(5))) == + constant_interval_exprt::top(signedbv_typet(32))); + REQUIRE( + constant_interval_exprt(CEV(10), CEV(20)) + .modulo(constant_interval_exprt(CEV(-5), CEV(5))) == + constant_interval_exprt::top(signedbv_typet(32))); + + REQUIRE( + constant_interval_exprt(CEV(-10), CEV(20)) + .modulo(constant_interval_exprt(CEV(0), CEV(5))) == + constant_interval_exprt::top(signedbv_typet(32))); + REQUIRE( + constant_interval_exprt(CEV(-20), CEV(-10)) + .modulo(constant_interval_exprt(CEV(0), CEV(5))) == + constant_interval_exprt::top(signedbv_typet(32))); + + REQUIRE( + constant_interval_exprt(CEV(-20), CEV(-10)) + .modulo(constant_interval_exprt(CEV(1), CEV(1))) == + constant_interval_exprt(CEV(0))); + + REQUIRE( + constant_interval_exprt(CEV(30), CEV(50)) + .modulo(constant_interval_exprt(CEV(2), CEV(2))) == + constant_interval_exprt(CEV(0), CEV(1))); + + // Problems + REQUIRE( + constant_interval_exprt(CEV(30), max_exprt(signedbv_typet(32))) + .modulo(constant_interval_exprt(CEV(2), CEV(2))) == + constant_interval_exprt(CEV(0), CEV(1))); + } + } + } +} diff --git a/unit/util/interval/multiply.cpp b/unit/util/interval/multiply.cpp new file mode 100644 index 00000000000..7214e1ccf38 --- /dev/null +++ b/unit/util/interval/multiply.cpp @@ -0,0 +1,144 @@ +/*******************************************************************\ + Module: Unit tests for variable/sensitivity/abstract_object::merge + Author: DiffBlue Limited +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +#define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) +#define V_(X) (bvrep2integer(X.c_str(), 32, true)) +#define CEV(X) (from_integer(mp_integer(X), signedbv_typet(32))) + +SCENARIO("multiply interval domain", "[core][analyses][interval][multiply]") +{ + GIVEN("A selection of constant_exprts in a std::vector and map") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + WHEN("Both are positive [2,5]*[7,11]") + { + constant_interval_exprt a(CEV(2), CEV(5)); + constant_interval_exprt b(CEV(7), CEV(11)); + + constant_interval_exprt result = a.multiply(b); + + THEN("Domain is consistent") + { + CHECK(V(a.get_lower()) == 2); + CHECK(V(a.get_upper()) == 5); + CHECK(V(b.get_lower()) == 7); + CHECK(V(b.get_upper()) == 11); + } + + CAPTURE(result); + + THEN("The result is [14, 55]") + { + CHECK(V(result.get_lower()) == 14); + CHECK(V(result.get_upper()) == 55); + } + } + + WHEN("One is entirely negative [-2,-5]*[7,11]") + { + constant_interval_exprt a(CEV(-5), CEV(-2)); + constant_interval_exprt b(CEV(7), CEV(11)); + + constant_interval_exprt result = a.multiply(b); + + THEN("Domain is consistent") + { + CHECK(V(a.get_lower()) == -5); + CHECK(V(a.get_upper()) == -2); + CHECK(V(b.get_lower()) == 7); + CHECK(V(b.get_upper()) == 11); + } + + CAPTURE(result); + + THEN("The result is [-55, -14]") + { + CHECK(V(result.get_lower()) == mp_integer(-55)); + CHECK(V(result.get_upper()) == -14); + } + } + + WHEN("Range contains and extends from zero [-2,5]*[7,11]") + { + constant_interval_exprt a(CEV(-2), CEV(5)); + constant_interval_exprt b(CEV(7), CEV(11)); + + constant_interval_exprt result = a.multiply(b); + + THEN("Domain is consistent") + { + CHECK(V(a.get_lower()) == -2); + CHECK(V(a.get_upper()) == 5); + CHECK(V(b.get_lower()) == 7); + CHECK(V(b.get_upper()) == 11); + } + + CAPTURE(result); + + THEN("The result is [-22, 55]") + { + CHECK(V(result.get_lower()) == mp_integer(-22)); + CHECK(V(result.get_upper()) == 55); + } + } + + WHEN("One domain is infinite and other crosses zero [-2,5]*[7,INF]") + { + constant_interval_exprt a(CEV(-2), CEV(5)); + constant_interval_exprt b(CEV(7), max_exprt(signedbv_typet(32))); + + constant_interval_exprt result = a.multiply(b); + + THEN("Domain is consistent") + { + CHECK(V(a.get_lower()) == -2); + CHECK(V(a.get_upper()) == 5); + CHECK(V(b.get_lower()) == 7); + CHECK(constant_interval_exprt::is_max(b.get_upper())); + } + + CAPTURE(result); + + THEN("The result is [-INF, INF]") + { + CHECK(constant_interval_exprt::is_max(result.get_upper())); + CHECK(constant_interval_exprt::is_min(result.get_lower())); + } + } + + WHEN("One domain is infinite and other is positive [2,5]*[7,INF]") + { + constant_interval_exprt a(CEV(2), CEV(5)); + constant_interval_exprt b(CEV(7), max_exprt(signedbv_typet(32))); + constant_interval_exprt result = a.multiply(b); + + THEN("Domain is consistent") + { + CHECK(V(a.get_lower()) == 2); + CHECK(V(a.get_upper()) == 5); + CHECK(V(b.get_lower()) == 7); + CHECK(b.has_no_upper_bound()); + } + + THEN("The result is [-INF, INF]") + { + CAPTURE(result); + + CHECK(result.has_no_upper_bound()); + CHECK(result.has_no_lower_bound()); + } + } + } +} diff --git a/unit/util/interval/shift.cpp b/unit/util/interval/shift.cpp new file mode 100644 index 00000000000..3813bf97bbc --- /dev/null +++ b/unit/util/interval/shift.cpp @@ -0,0 +1,36 @@ +/*******************************************************************\ + Module: Unit tests for variable/sensitivity/abstract_object::merge + Author: DiffBlue Limited +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +#define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) +#define V_(X) (bvrep2integer(X.c_str(), 32, true)) +#define CEV(X) (from_integer(mp_integer(X), signedbv_typet(32))) + +SCENARIO("shift interval domain", "[core][analyses][interval][shift]") +{ + GIVEN("Two simple signed intervals") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + WHEN("Something") + { + THEN("Something else") + { + REQUIRE( + constant_interval_exprt(CEV(4), CEV(8)) + .left_shift(constant_interval_exprt(CEV(1))) == + constant_interval_exprt(CEV(8), CEV(16))); + } + } + } +} diff --git a/unit/util/interval/subtract.cpp b/unit/util/interval/subtract.cpp new file mode 100644 index 00000000000..84f2386493d --- /dev/null +++ b/unit/util/interval/subtract.cpp @@ -0,0 +1,147 @@ +/*******************************************************************\ + Module: Unit tests for variable/sensitivity/abstract_object::merge + Author: DiffBlue Limited +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +#define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) +#define V_(X) (bvrep2integer(X.c_str(), 32, true)) +#define CEV(X) (from_integer(mp_integer(X), signedbv_typet(32))) + +SCENARIO("subtract interval domain", "[core][analyses][interval][subtract]") +{ + GIVEN("Two simple signed intervals") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + WHEN("The result is positive [6,8]-[2,4]") + { + constant_interval_exprt left(CEV(6), CEV(8)); + constant_interval_exprt right(CEV(2), CEV(4)); + + constant_interval_exprt result = left.minus(right); + + THEN("Domain is consistent") + { + REQUIRE(V(left.get_lower()) == 6); + REQUIRE(V(left.get_upper()) == 8); + REQUIRE(V(right.get_lower()) == 2); + REQUIRE(V(right.get_upper()) == 4); + } + + THEN("The result is [2, 6]") + { + REQUIRE(V(result.get_lower()) == 2); + REQUIRE(V(result.get_upper()) == 6); + } + } + + WHEN("One contains infinite [2,4]-[6,INF]") + { + constant_interval_exprt left(CEV(2), CEV(4)); + constant_interval_exprt right(CEV(6), max_exprt(signedbv_typet(32))); + + constant_interval_exprt result = left.minus(right); + + THEN("Domain is consistent") + { + REQUIRE(V(left.get_lower()) == 2); + REQUIRE(V(left.get_upper()) == 4); + REQUIRE(V(right.get_lower()) == 6); + REQUIRE(right.has_no_upper_bound()); + } + + CAPTURE(result); + + THEN("The result is [MIN, -2]") + { + REQUIRE(V(result.get_upper()) == -2); + REQUIRE(result.has_no_lower_bound()); + } + } + + WHEN("Both contain infinite [2,INF]-[6,INF]") + { + constant_interval_exprt left(CEV(2), max_exprt(signedbv_typet(32))); + constant_interval_exprt right(CEV(6), max_exprt(signedbv_typet(32))); + + constant_interval_exprt result = left.minus(right); + + THEN("Domain is consistent") + { + REQUIRE(V(left.get_lower()) == 2); + REQUIRE(left.has_no_upper_bound()); + REQUIRE(V(right.get_lower()) == 6); + REQUIRE(right.has_no_upper_bound()); + } + + CAPTURE(result); + + THEN("The result is [MIN, MAX]") + { + REQUIRE(result.has_no_upper_bound()); + REQUIRE(result.has_no_lower_bound()); + } + } + } +} + +SCENARIO( + "Subtracting unsigned integers", + "[core][analyses][interval][subtract]") +{ + auto get_value = [](int x) { return from_integer(x, signedbv_typet(32)); }; + + WHEN("Subtracting two constant intervals") + { + auto lhs = constant_interval_exprt(get_value(10)); + auto rhs = constant_interval_exprt(get_value(3)); + THEN("it should work") + { + auto result = lhs.minus(rhs); + REQUIRE(result.is_single_value_interval()); + auto maybe_lower = numeric_cast(result.get_lower()); + REQUIRE(maybe_lower.has_value()); + REQUIRE(maybe_lower.value() == 7); + } + } + + WHEN("Subtracting zero from something") + { + auto lhs = constant_interval_exprt(get_value(10)); + auto rhs = constant_interval_exprt(get_value(0)); + + THEN("it should not give a completely crazy result") + { + auto result = lhs.minus(rhs); + REQUIRE(result.is_single_value_interval()); + auto maybe_lower = numeric_cast(result.get_lower()); + REQUIRE(maybe_lower.has_value()); + REQUIRE(maybe_lower.value() == 10); + } + } + + WHEN("Subtracting an non-constant interval containing zero") + { + auto lhs = constant_interval_exprt(get_value(10)); + auto rhs = constant_interval_exprt(get_value(0), get_value(1)); + THEN("it should not give a completely crazy result") + { + auto result = lhs.minus(rhs); + auto maybe_lower = numeric_cast(result.get_lower()); + REQUIRE(maybe_lower.has_value()); + REQUIRE(maybe_lower.value() == 9); + auto maybe_upper = numeric_cast(result.get_upper()); + REQUIRE(maybe_upper.has_value()); + REQUIRE(maybe_upper.value() == 10); + } + } +}