diff --git a/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc b/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc new file mode 100644 index 00000000000..a13c311d41c --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc @@ -0,0 +1,10 @@ +CORE +enum_test3.c +--show-goto-functions +0 ≤ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ∧ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ≤ 4$ +^EXIT=0$ +^SIGNAL=0$ +-- +main::1::ev1 = 0 +-- +This test is to demonstrate simplification of enumerated ranges of integers. diff --git a/regression/cbmc/enum_is_in_range/format.desc b/regression/cbmc/enum_is_in_range/format.desc new file mode 100644 index 00000000000..6de3db06fa6 --- /dev/null +++ b/regression/cbmc/enum_is_in_range/format.desc @@ -0,0 +1,10 @@ +CORE +no_duplicate.c +--show-goto-functions +main::1::e = 1 ∨ main::1::e = 2 ∨ main::1::e = 4 ∨ main::1::e = 8 +^EXIT=0$ +^SIGNAL=0$ +-- +type: c_enum_tag +-- +This test is to show that format(expr) also works for enum-typed constants. diff --git a/regression/cbmc/enum_is_in_range/no_duplicate.c b/regression/cbmc/enum_is_in_range/no_duplicate.c new file mode 100644 index 00000000000..79d07bba3af --- /dev/null +++ b/regression/cbmc/enum_is_in_range/no_duplicate.c @@ -0,0 +1,19 @@ +enum enm +{ + first = 1, + second = 1 << 1, + third = 1 << 2, + fourth = 1 << 3, +}; + +static enum enm efunc(void) +{ + return second; +} + +int main(void) +{ + enum enm e = efunc(); + __CPROVER_assert(__CPROVER_enum_is_in_range(e), "enum failure"); + return (e); +} diff --git a/regression/cbmc/enum_is_in_range/no_duplicate.desc b/regression/cbmc/enum_is_in_range/no_duplicate.desc new file mode 100644 index 00000000000..20c2ce2693b --- /dev/null +++ b/regression/cbmc/enum_is_in_range/no_duplicate.desc @@ -0,0 +1,11 @@ +CORE +no_duplicate.c +--enum-range-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +line 17 enum range check in e: SUCCESS$ +-- +Test that enum range checks aren't applied to function-call left-hand sides, and +that no extra checks are generated for uses of __CPROVER_enum_is_in_range. diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index a707a7368a7..af5d919dc12 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -25,6 +25,8 @@ ['integer-assignments1', 'integer-typecheck.desc'], ['destructors', 'compound_literal.desc'], ['destructors', 'enter_lexical_block.desc'], + ['enum_is_in_range', 'enum_test3-simplified.desc'], + ['enum_is_in_range', 'format.desc'], ['r_w_ok9', 'simplify.desc'], ['reachability-slice-interproc2', 'test.desc'], # this one wants show-properties instead producing a trace diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp index edbaf7f7245..d07bbbd7b34 100644 --- a/src/analyses/goto_check_c.cpp +++ b/src/analyses/goto_check_c.cpp @@ -517,8 +517,7 @@ void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard) return; const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type(expr.type()); - symbolt enum_type = ns.lookup(c_enum_tag_type.get_identifier()); - const c_enum_typet &c_enum_type = to_c_enum_type(enum_type.type); + const c_enum_typet &c_enum_type = ns.follow_tag(c_enum_tag_type); const c_enum_typet::memberst enum_values = c_enum_type.members(); @@ -2148,7 +2147,13 @@ void goto_check_ct::goto_check( } else if(i.is_function_call()) { - check(i.call_lhs()); + // Disable enum range checks for left-hand sides as their values are yet + // to be set (by this function call). + { + flag_overridet resetter(i.source_location()); + resetter.disable_flag(enable_enum_range_check, "enum_range_check"); + check(i.call_lhs()); + } check(i.call_function()); for(const auto &arg : i.call_arguments()) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 8c0a880ca4c..a154338c099 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -636,8 +636,9 @@ void goto_convertt::do_enum_is_in_range( disjuncts.push_back(equal_exprt(enum_expr, std::move(val))); } - code_assignt assignment(lhs, disjunction(disjuncts)); + code_assignt assignment(lhs, simplify_expr(disjunction(disjuncts), ns)); assignment.add_source_location() = function.source_location(); + assignment.add_source_location().add_pragma("disable:enum-range-check"); copy(assignment, ASSIGN, dest); } diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index b306c4bef4d..168fd1a3a4d 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -59,13 +59,13 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value) const typet &underlying_type = to_c_enum_type(type).underlying_type(); if(underlying_type.id() == ID_signedbv) { - const auto width = to_signedbv_type(type).get_width(); + const auto width = to_signedbv_type(underlying_type).get_width(); int_value = bvrep2integer(value, width, true); return false; } else if(underlying_type.id() == ID_unsignedbv) { - const auto width = to_unsignedbv_type(type).get_width(); + const auto width = to_unsignedbv_type(underlying_type).get_width(); int_value = bvrep2integer(value, width, false); return false; } diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 43f1ea3145f..7853dcfe856 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -204,6 +204,10 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src) << format(pointer_type.base_type()) << ')'; } } + else if(type == ID_c_enum_tag) + { + return os << string2integer(id2string(src.get_value()), 16); + } else return os << src.pretty(); } diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index 8f66f948daa..27a203429c1 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -8,12 +8,15 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_expr_class.h" -#include - +#include "arith_tools.h" +#include "c_types.h" #include "expr_util.h" #include "mathematical_expr.h" +#include "namespace.h" #include "std_expr.h" +#include + simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) { if(!expr.has_operands()) @@ -96,6 +99,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) std::unordered_set expr_set; bool no_change = true; + bool may_be_reducible_to_interval = + expr.id() == ID_or && expr.operands().size() > 2; exprt::operandst new_operands = expr.operands(); @@ -127,7 +132,70 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) no_change = false; } else + { + if(may_be_reducible_to_interval) + may_be_reducible_to_interval = it->id() == ID_equal; it++; + } + } + + if(may_be_reducible_to_interval) + { + optionalt symbol_opt; + std::set values; + for(const exprt &op : new_operands) + { + equal_exprt eq = to_equal_expr(op); + if(eq.lhs().is_constant()) + std::swap(eq.lhs(), eq.rhs()); + if(auto s = expr_try_dynamic_cast(eq.lhs())) + { + if(!symbol_opt.has_value()) + symbol_opt = *s; + + if(*s == *symbol_opt) + { + if(auto c = expr_try_dynamic_cast(eq.rhs())) + { + constant_exprt c_tmp = *c; + if(c_tmp.type().id() == ID_c_enum_tag) + c_tmp.type() = ns.follow_tag(to_c_enum_tag_type(c_tmp.type())); + if(auto int_opt = numeric_cast(c_tmp)) + { + values.insert(*int_opt); + continue; + } + } + } + } + + symbol_opt.reset(); + break; + } + + if(symbol_opt.has_value() && values.size() >= 3) + { + mp_integer lower = *values.begin(); + mp_integer upper = *std::prev(values.end()); + if(upper - lower + 1 == mp_integer{values.size()}) + { + typet type = symbol_opt->type(); + if(symbol_opt->type().id() == ID_c_enum_tag) + { + type = ns.follow_tag(to_c_enum_tag_type(symbol_opt->type())) + .underlying_type(); + } + + less_than_or_equal_exprt lb{ + from_integer(lower, type), + typecast_exprt::conditional_cast(*symbol_opt, type)}; + less_than_or_equal_exprt ub{ + typecast_exprt::conditional_cast(*symbol_opt, type), + from_integer(upper, type)}; + + return and_exprt{lb, ub}; + } + } } // search for a and !a