From 8c0644d8cbabba430b6990733ba0f2c2603c30f0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 19 Jan 2022 10:05:04 +0000 Subject: [PATCH 1/4] Support enum-typed constants in format_expr We should not have to fall back to irept pretty printing for these. --- regression/cbmc/enum_is_in_range/format.desc | 10 ++++++++++ .../cbmc/enum_is_in_range/no_duplicate.c | 19 +++++++++++++++++++ regression/validate-trace-xml-schema/check.py | 1 + src/util/format_expr.cpp | 4 ++++ 4 files changed, 34 insertions(+) create mode 100644 regression/cbmc/enum_is_in_range/format.desc create mode 100644 regression/cbmc/enum_is_in_range/no_duplicate.c 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/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index a707a7368a7..77bbdd0e061 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -25,6 +25,7 @@ ['integer-assignments1', 'integer-typecheck.desc'], ['destructors', 'compound_literal.desc'], ['destructors', 'enter_lexical_block.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/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(); } From 7597f90477d8dfb476641dd4a3226c426907a36d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 19 Jan 2022 10:06:17 +0000 Subject: [PATCH 2/4] Do not generate enum-value checks for function call left-hand sides We already disabled these checks for assignment left-hand sides, but need to do the same for function calls. Else we'd be asserting validity before the value has been assigned. Fixes: #6586, #6451 Co-authored-by: Ilia Levin --- regression/cbmc/enum_is_in_range/no_duplicate.desc | 8 ++++++++ src/analyses/goto_check_c.cpp | 11 ++++++++--- 2 files changed, 16 insertions(+), 3 deletions(-) create mode 100644 regression/cbmc/enum_is_in_range/no_duplicate.desc 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..b6c85fb7da2 --- /dev/null +++ b/regression/cbmc/enum_is_in_range/no_duplicate.desc @@ -0,0 +1,8 @@ +CORE +no_duplicate.c +--enum-range-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- 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()) From 8e391169deed48bde35a1e6871ed87e12607f602 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 19 Jan 2022 11:26:51 +0000 Subject: [PATCH 3/4] __CPROVER_enum_is_in_range should not yield redundant assertions The assertions generated by --enum-range-check must not apply to the expansion of __CPROVER_enum_is_in_range, for those would assert exactly the same. Also, those expressions are rather costly: for N enum values, N assertions would be generated. --- regression/cbmc/enum_is_in_range/no_duplicate.desc | 3 +++ src/goto-programs/builtin_functions.cpp | 1 + 2 files changed, 4 insertions(+) diff --git a/regression/cbmc/enum_is_in_range/no_duplicate.desc b/regression/cbmc/enum_is_in_range/no_duplicate.desc index b6c85fb7da2..20c2ce2693b 100644 --- a/regression/cbmc/enum_is_in_range/no_duplicate.desc +++ b/regression/cbmc/enum_is_in_range/no_duplicate.desc @@ -5,4 +5,7 @@ no_duplicate.c ^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/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 8c0a880ca4c..cf7db442bd5 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -638,6 +638,7 @@ void goto_convertt::do_enum_is_in_range( code_assignt assignment(lhs, disjunction(disjuncts)); assignment.add_source_location() = function.source_location(); + assignment.add_source_location().add_pragma("disable:enum-range-check"); copy(assignment, ASSIGN, dest); } From 7e0f8295916dce1ebf8f026d4ea098c8ef1f12a7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 27 Jan 2022 19:44:51 +0000 Subject: [PATCH 4/4] Simplify disjunctions over equalities to intervals Disjunctions over equalities of integer constants can be rewritten as closed intervals. This will most commonly appear when expanding enum_is_in_range. This also surfaced a bug in to_integer, which used the wrong type reference. --- .../enum_test3-simplified.desc | 10 +++ regression/validate-trace-xml-schema/check.py | 1 + src/goto-programs/builtin_functions.cpp | 2 +- src/util/arith_tools.cpp | 4 +- src/util/simplify_expr_boolean.cpp | 72 ++++++++++++++++++- 5 files changed, 84 insertions(+), 5 deletions(-) create mode 100644 regression/cbmc/enum_is_in_range/enum_test3-simplified.desc 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/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 77bbdd0e061..af5d919dc12 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -25,6 +25,7 @@ ['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'], diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index cf7db442bd5..a154338c099 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -636,7 +636,7 @@ 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/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