diff --git a/doc/cprover-manual/api.md b/doc/cprover-manual/api.md index 5d191cc212c..ca1b76b998b 100644 --- a/doc/cprover-manual/api.md +++ b/doc/cprover-manual/api.md @@ -125,6 +125,38 @@ stored in the given arrays are equal. The function the array **dest**. The function **\_\_CPROVER\_array\_set** initializes the array **dest** with the given value. + +#### \_\_CPROVER\_enum\_is\_in\_range + +```C +__CPROVER_bool __CPROVER_enum_is_in_range(); +``` + +The function **\_\_CPROVER\_enum\_is\_in\_range** is used to check +that an enumeration has one of the defined enumeration values. In +the following example `__CPROVER_enum_is_in_range(ev1)` will return +true and the assertion will pass +```C +enum my_enum { first, second }; + +int main() +{ + enum my_enum ev1 = second; + assert(__CPROVER_enum_is_in_range(ev1)); +} +``` +However, in the example below the assertion will fail +```C +enum my_enum { first, second }; + +int main() +{ + enum my_enum ev1 = second + 1; + assert(__CPROVER_enum_is_in_range(ev1)); +} +``` + + #### Uninterpreted Functions Uninterpreted functions are documented [here](./modeling-nondeterminism.md)). diff --git a/regression/ansi-c/enum_is_in_range/enum_test10.c b/regression/ansi-c/enum_is_in_range/enum_test10.c new file mode 100644 index 00000000000..44a64c51d22 --- /dev/null +++ b/regression/ansi-c/enum_is_in_range/enum_test10.c @@ -0,0 +1,26 @@ +#include + +enum my_enum +{ + first, + second, + third, + fourth, + fifth +}; + +int main() +{ + enum my_enum ev1; + enum my_enum ev2; + ev1 = first; + ev2 = fifth; + int i = 0; + while(i < 10) + { + ev1++; + assert(__CPROVER_enum_is_in_range(i)); + i++; + } + return 0; +} diff --git a/regression/ansi-c/enum_is_in_range/enum_test10.desc b/regression/ansi-c/enum_is_in_range/enum_test10.desc new file mode 100644 index 00000000000..b2c77903bb7 --- /dev/null +++ b/regression/ansi-c/enum_is_in_range/enum_test10.desc @@ -0,0 +1,12 @@ +CORE +enum_test10.c + +^EXIT=(6|70)$ +^SIGNAL=0$ +^file enum_test10.c line \d+ function main: __CPROVER_enum_is_in_range expects enum, but \(i\) has type `signed int`$ +-- +^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): SUCCESS$ +^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): FAILURE$ +^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$ +-- +This test the type checking of argument for __CPROVER_enum_is_in_range diff --git a/regression/ansi-c/enum_is_in_range/enum_test12.c b/regression/ansi-c/enum_is_in_range/enum_test12.c new file mode 100644 index 00000000000..b079987b4b3 --- /dev/null +++ b/regression/ansi-c/enum_is_in_range/enum_test12.c @@ -0,0 +1,20 @@ +#include + +enum my_enum +{ + first, + second, + third, + fourth, + fifth +}; + +int main() +{ + enum my_enum ev1; + enum my_enum ev2; + ev1 = first; + ev2 = fifth; + assert(__CPROVER_enum_is_in_range(ev1, ev2)); + return 0; +} diff --git a/regression/ansi-c/enum_is_in_range/enum_test12.desc b/regression/ansi-c/enum_is_in_range/enum_test12.desc new file mode 100644 index 00000000000..983beaa2d81 --- /dev/null +++ b/regression/ansi-c/enum_is_in_range/enum_test12.desc @@ -0,0 +1,12 @@ +CORE +enum_test12.c + +^EXIT=(6|70)$ +^SIGNAL=0$ +^file enum_test12.c line \d+ function main: __CPROVER_enum_is_in_range takes exactly 1 argument, but 2 were provided$ +-- +^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): SUCCESS$ +^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): FAILURE$ +^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$ +-- +This test the type checking of argument for __CPROVER_enum_is_in_range diff --git a/regression/cbmc/enum_is_in_range/enum_test3.c b/regression/cbmc/enum_is_in_range/enum_test3.c new file mode 100644 index 00000000000..8ebe8935761 --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test3.c @@ -0,0 +1,24 @@ +#include + +enum my_enum +{ + first, + second, + third, + fourth, + fifth +}; + +int main() +{ + enum my_enum ev1; + enum my_enum ev2; + ev1 = first; + ev2 = fifth; + while(ev1 != ev2) + { + ev1++; + assert(__CPROVER_enum_is_in_range(ev1)); + } + return 0; +} diff --git a/regression/cbmc/enum_is_in_range/enum_test3.desc b/regression/cbmc/enum_is_in_range/enum_test3.desc new file mode 100644 index 00000000000..f5a94e90126 --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test3.desc @@ -0,0 +1,11 @@ +CORE +enum_test3.c + +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS +-- +^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range +-- +This test is for the enum_is_in_range working properly, the negation +is if the function is not defined. diff --git a/regression/cbmc/enum_is_in_range/enum_test4.c b/regression/cbmc/enum_is_in_range/enum_test4.c new file mode 100644 index 00000000000..66d63ef1c4f --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test4.c @@ -0,0 +1,26 @@ +#include + +enum my_enum +{ + first, + second, + third, + fourth, + fifth +}; + +int main() +{ + enum my_enum ev1; + enum my_enum ev2; + ev1 = first; + ev2 = fifth; + int i = 0; + while(i < 10) + { + ev1++; + assert(__CPROVER_enum_is_in_range(ev1)); + i++; + } + return 0; +} diff --git a/regression/cbmc/enum_is_in_range/enum_test4.desc b/regression/cbmc/enum_is_in_range/enum_test4.desc new file mode 100644 index 00000000000..cb92ba52f99 --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test4.desc @@ -0,0 +1,13 @@ +CORE +enum_test4.c + +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): FAILURE$ +-- +^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS$ +^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$ +-- +This test is for the enum_is_in_range working properly and detecting +when the enum is not in range. The negation tests are to ensure the +out of range is detected, and if the function is not defined. diff --git a/regression/cbmc/enum_is_in_range/enum_test5.c b/regression/cbmc/enum_is_in_range/enum_test5.c new file mode 100644 index 00000000000..504476ec5e9 --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test5.c @@ -0,0 +1,25 @@ +#include + +enum my_enum +{ + first, + second, + third, + fourth, + fifth +}; + +void testfun(enum my_enum ee) +{ +} + +int main() +{ + enum my_enum ev1; + enum my_enum ev2; + __CPROVER_assume(__CPROVER_enum_is_in_range(ev1)); + enum my_enum ev3 = ev1; + testfun(ev3); + testfun(ev2); + return 0; +} diff --git a/regression/cbmc/enum_is_in_range/enum_test5.desc b/regression/cbmc/enum_is_in_range/enum_test5.desc new file mode 100644 index 00000000000..05dda80155a --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test5.desc @@ -0,0 +1,16 @@ +CORE +enum_test5.c +--enum-range-check +^EXIT=10$ +^SIGNAL=0$ +^\[main.enum-range-check.6\] line \d+ enum range check in ev3: SUCCESS$ +^\[main.enum-range-check.7\] line \d+ enum range check in ev2: FAILURE$ +-- +^\[main.enum-range-check.6\] line \d+ enum range check in ev3: FAILURE$ +^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$ +-- +This test is for the enum_is_in_range working in assume statements +(and also value passing through assignments of enums). The failure +test case is checking that range checks do work on enums. +The negation tests are to ensure the assumption is taken into account +for ev1 and thus ev3, and if the function is not defined. diff --git a/regression/cbmc/enum_is_in_range/enum_test7.c b/regression/cbmc/enum_is_in_range/enum_test7.c new file mode 100644 index 00000000000..aca1367e24e --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test7.c @@ -0,0 +1,24 @@ +#include + +typedef enum +{ + first, + second, + third, + fourth, + fifth +} my_enum; + +int main() +{ + my_enum ev1; + my_enum ev2; + ev1 = first; + ev2 = fifth; + while(!(ev1 == ev2)) + { + ev1++; + assert(__CPROVER_enum_is_in_range(ev1)); + } + return 0; +} diff --git a/regression/cbmc/enum_is_in_range/enum_test7.desc b/regression/cbmc/enum_is_in_range/enum_test7.desc new file mode 100644 index 00000000000..613a2cbc8f9 --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test7.desc @@ -0,0 +1,11 @@ +CORE +enum_test7.c + +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS +-- +^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range +-- +This test is for the enum_is_in_range working properly, the negation +is if the function is not defined. diff --git a/regression/cbmc/enum_is_in_range/enum_test8.c b/regression/cbmc/enum_is_in_range/enum_test8.c new file mode 100644 index 00000000000..e2899dd53f6 --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test8.c @@ -0,0 +1,26 @@ +#include + +typedef enum +{ + first, + second, + third, + fourth, + fifth +} my_enum; + +int main() +{ + my_enum ev1; + my_enum ev2; + ev1 = first; + ev2 = fifth; + int i = 0; + while(i < 10) + { + ev1++; + assert(__CPROVER_enum_is_in_range(ev1)); + i++; + } + return 0; +} diff --git a/regression/cbmc/enum_is_in_range/enum_test8.desc b/regression/cbmc/enum_is_in_range/enum_test8.desc new file mode 100644 index 00000000000..b03055b46ea --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_test8.desc @@ -0,0 +1,13 @@ +CORE +enum_test8.c + +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): FAILURE$ +-- +^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS$ +^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$ +-- +This test is for the enum_is_in_range working properly and detecting +when the enum is not in range. The negation tests are to ensure the +out of range is detected, and if the function is not defined. diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 5afe177e6c0..287060b939e 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2841,6 +2841,33 @@ exprt c_typecheck_baset::do_special_functions( overflow.type() = bool_typet{}; return overflow; } + else if(identifier == CPROVER_PREFIX "enum_is_in_range") + { + // Check correct number of arguments + if(expr.arguments().size() != 1) + { + std::ostringstream error_message; + error_message << expr.source_location().as_string() << ": " << identifier + << " takes exactly 1 argument, but " + << expr.arguments().size() << " were provided"; + throw invalid_source_file_exceptiont{error_message.str()}; + } + auto arg1 = expr.arguments()[0]; + typecheck_expr(arg1); + if(!can_cast_type(arg1.type())) + { + // Can't enum range check a non-enum + std::ostringstream error_message; + error_message << expr.source_location().as_string() << ": " << identifier + << " expects enum, but (" << expr2c(arg1, *this) + << ") has type `" << type2c(arg1.type(), *this) << '`'; + throw invalid_source_file_exceptiont{error_message.str()}; + } + else + { + return expr; + } + } else if( identifier == "__builtin_add_overflow" || identifier == "__builtin_sub_overflow" || diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 1b9db5d06a3..8d5ec717f37 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -103,3 +103,6 @@ __CPROVER_bool __CPROVER_overflow_mult(); __CPROVER_bool __CPROVER_overflow_plus(); __CPROVER_bool __CPROVER_overflow_shl(); __CPROVER_bool __CPROVER_overflow_unary_minus(); + +// enumerations +__CPROVER_bool __CPROVER_enum_is_in_range(); diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 40e9bb0e1c9..6e32bc8cfd8 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -610,6 +610,32 @@ exprt make_va_list(const exprt &expr) return result; } +void goto_convertt::do_enum_is_in_range( + const exprt &lhs, + const symbol_exprt &function, + const exprt::operandst &arguments, + goto_programt &dest) +{ + PRECONDITION(arguments.size() == 1); + const auto enum_expr = arguments.front(); + const auto enum_type = + type_try_dynamic_cast(enum_expr.type()); + PRECONDITION(enum_type); + const c_enum_typet &c_enum_type = ns.follow_tag(*enum_type); + const c_enum_typet::memberst enum_values = c_enum_type.members(); + + exprt::operandst disjuncts; + for(const auto &enum_value : enum_values) + { + constant_exprt val{enum_value.get_value(), *enum_type}; + disjuncts.push_back(equal_exprt(enum_expr, std::move(val))); + } + + code_assignt assignment(lhs, disjunction(disjuncts)); + assignment.add_source_location() = function.source_location(); + copy(assignment, ASSIGN, dest); +} + /// add function calls to function queue for later processing void goto_convertt::do_function_call_symbol( const exprt &lhs, @@ -734,6 +760,10 @@ void goto_convertt::do_function_call_symbol( throw 0; } } + else if(identifier == CPROVER_PREFIX "enum_is_in_range") + { + do_enum_is_in_range(lhs, function, arguments, dest); + } else if( identifier == CPROVER_PREFIX "assert" || identifier == CPROVER_PREFIX "precondition" || diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index b0c429a0102..1bf726288a8 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -588,6 +588,26 @@ class goto_convertt:public messaget bool get_string_constant(const exprt &expr, irep_idt &); exprt get_constant(const exprt &expr); + /// \brief Converts calls to the built in `enum_is_in_range` function to a + /// test that the given enum value is in the valid range of values for that + /// enum type. + /// + /// Note that the check for the range of values is done by creating a + /// disjunction comparing the expression with each possible valid value. + /// \param lhs: The destination for the generated assignment. + /// \param function: The `enum_is_in_range` symbol of the source function call. + /// \param arguments: A collection of arguments, which is expected to contain a + /// single argument which is an expression that resolves to a value of + /// enum type. The arguments are expected to have been prevalidated by the + /// typechecking process. + /// \param dest: The goto program into which the generated assignment is + /// copied. + void do_enum_is_in_range( + const exprt &lhs, + const symbol_exprt &function, + const exprt::operandst &arguments, + goto_programt &dest); + // some built-in functions void do_atomic_begin( const exprt &lhs,