Skip to content

Commit bfad11a

Browse files
TGWDBTGWDB
authored
Merge pull request #5808 from TGWDB/CPROVER-enum-is-in-range
This adds a new builtin function __CPROVER_enum_is_in_range to determine if an enum is one of the valid enum values. This fixes issue 5473: #5473
2 parents 27072c6 + baab734 commit bfad11a

19 files changed

+371
-0
lines changed

‎doc/cprover-manual/api.md

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -125,6 +125,38 @@ stored in the given arrays are equal. The function
125125
the array **dest**. The function **\_\_CPROVER\_array\_set** initializes
126126
the array **dest** with the given value.
127127
128+
129+
#### \_\_CPROVER\_enum\_is\_in\_range
130+
131+
```C
132+
__CPROVER_bool __CPROVER_enum_is_in_range();
133+
```
134+
135+
The function **\_\_CPROVER\_enum\_is\_in\_range** is used to check
136+
that an enumeration has one of the defined enumeration values. In
137+
the following example `__CPROVER_enum_is_in_range(ev1)` will return
138+
true and the assertion will pass
139+
```C
140+
enum my_enum { first, second };
141+
142+
int main()
143+
{
144+
enum my_enum ev1 = second;
145+
assert(__CPROVER_enum_is_in_range(ev1));
146+
}
147+
```
148+
However, in the example below the assertion will fail
149+
```C
150+
enum my_enum { first, second };
151+
152+
int main()
153+
{
154+
enum my_enum ev1 = second + 1;
155+
assert(__CPROVER_enum_is_in_range(ev1));
156+
}
157+
```
158+
159+
128160
#### Uninterpreted Functions
129161

130162
Uninterpreted functions are documented [here](./modeling-nondeterminism.md)).

‎regression/ansi-c/enum_is_in_range/enum_test10.c

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
#include <assert.h>
2+
3+
enum my_enum
4+
{
5+
first,
6+
second,
7+
third,
8+
fourth,
9+
fifth
10+
};
11+
12+
int main()
13+
{
14+
enum my_enum ev1;
15+
enum my_enum ev2;
16+
ev1 = first;
17+
ev2 = fifth;
18+
int i = 0;
19+
while(i < 10)
20+
{
21+
ev1++;
22+
assert(__CPROVER_enum_is_in_range(i));
23+
i++;
24+
}
25+
return 0;
26+
}

‎regression/ansi-c/enum_is_in_range/enum_test10.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
enum_test10.c
3+
4+
^EXIT=(6|70)$
5+
^SIGNAL=0$
6+
^file enum_test10.c line \d+ function main: __CPROVER_enum_is_in_range expects enum, but \(i\) has type `signed int`$
7+
--
8+
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): SUCCESS$
9+
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): FAILURE$
10+
^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
11+
--
12+
This test the type checking of argument for __CPROVER_enum_is_in_range

‎regression/ansi-c/enum_is_in_range/enum_test12.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <assert.h>
2+
3+
enum my_enum
4+
{
5+
first,
6+
second,
7+
third,
8+
fourth,
9+
fifth
10+
};
11+
12+
int main()
13+
{
14+
enum my_enum ev1;
15+
enum my_enum ev2;
16+
ev1 = first;
17+
ev2 = fifth;
18+
assert(__CPROVER_enum_is_in_range(ev1, ev2));
19+
return 0;
20+
}

‎regression/ansi-c/enum_is_in_range/enum_test12.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
enum_test12.c
3+
4+
^EXIT=(6|70)$
5+
^SIGNAL=0$
6+
^file enum_test12.c line \d+ function main: __CPROVER_enum_is_in_range takes exactly 1 argument, but 2 were provided$
7+
--
8+
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): SUCCESS$
9+
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): FAILURE$
10+
^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
11+
--
12+
This test the type checking of argument for __CPROVER_enum_is_in_range

‎regression/cbmc/enum_is_in_range/enum_test3.c

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#include <assert.h>
2+
3+
enum my_enum
4+
{
5+
first,
6+
second,
7+
third,
8+
fourth,
9+
fifth
10+
};
11+
12+
int main()
13+
{
14+
enum my_enum ev1;
15+
enum my_enum ev2;
16+
ev1 = first;
17+
ev2 = fifth;
18+
while(ev1 != ev2)
19+
{
20+
ev1++;
21+
assert(__CPROVER_enum_is_in_range(ev1));
22+
}
23+
return 0;
24+
}

‎regression/cbmc/enum_is_in_range/enum_test3.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
enum_test3.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS
7+
--
8+
^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range
9+
--
10+
This test is for the enum_is_in_range working properly, the negation
11+
is if the function is not defined.

‎regression/cbmc/enum_is_in_range/enum_test4.c

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
#include <assert.h>
2+
3+
enum my_enum
4+
{
5+
first,
6+
second,
7+
third,
8+
fourth,
9+
fifth
10+
};
11+
12+
int main()
13+
{
14+
enum my_enum ev1;
15+
enum my_enum ev2;
16+
ev1 = first;
17+
ev2 = fifth;
18+
int i = 0;
19+
while(i < 10)
20+
{
21+
ev1++;
22+
assert(__CPROVER_enum_is_in_range(ev1));
23+
i++;
24+
}
25+
return 0;
26+
}

‎regression/cbmc/enum_is_in_range/enum_test4.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
enum_test4.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): FAILURE$
7+
--
8+
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS$
9+
^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
10+
--
11+
This test is for the enum_is_in_range working properly and detecting
12+
when the enum is not in range. The negation tests are to ensure the
13+
out of range is detected, and if the function is not defined.

‎regression/cbmc/enum_is_in_range/enum_test5.c

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
#include <assert.h>
2+
3+
enum my_enum
4+
{
5+
first,
6+
second,
7+
third,
8+
fourth,
9+
fifth
10+
};
11+
12+
void testfun(enum my_enum ee)
13+
{
14+
}
15+
16+
int main()
17+
{
18+
enum my_enum ev1;
19+
enum my_enum ev2;
20+
__CPROVER_assume(__CPROVER_enum_is_in_range(ev1));
21+
enum my_enum ev3 = ev1;
22+
testfun(ev3);
23+
testfun(ev2);
24+
return 0;
25+
}

‎regression/cbmc/enum_is_in_range/enum_test5.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
enum_test5.c
3+
--enum-range-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.enum-range-check.6\] line \d+ enum range check in ev3: SUCCESS$
7+
^\[main.enum-range-check.7\] line \d+ enum range check in ev2: FAILURE$
8+
--
9+
^\[main.enum-range-check.6\] line \d+ enum range check in ev3: FAILURE$
10+
^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
11+
--
12+
This test is for the enum_is_in_range working in assume statements
13+
(and also value passing through assignments of enums). The failure
14+
test case is checking that range checks do work on enums.
15+
The negation tests are to ensure the assumption is taken into account
16+
for ev1 and thus ev3, and if the function is not defined.

‎regression/cbmc/enum_is_in_range/enum_test7.c

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#include <assert.h>
2+
3+
typedef enum
4+
{
5+
first,
6+
second,
7+
third,
8+
fourth,
9+
fifth
10+
} my_enum;
11+
12+
int main()
13+
{
14+
my_enum ev1;
15+
my_enum ev2;
16+
ev1 = first;
17+
ev2 = fifth;
18+
while(!(ev1 == ev2))
19+
{
20+
ev1++;
21+
assert(__CPROVER_enum_is_in_range(ev1));
22+
}
23+
return 0;
24+
}

‎regression/cbmc/enum_is_in_range/enum_test7.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
enum_test7.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS
7+
--
8+
^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range
9+
--
10+
This test is for the enum_is_in_range working properly, the negation
11+
is if the function is not defined.

‎regression/cbmc/enum_is_in_range/enum_test8.c

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
#include <assert.h>
2+
3+
typedef enum
4+
{
5+
first,
6+
second,
7+
third,
8+
fourth,
9+
fifth
10+
} my_enum;
11+
12+
int main()
13+
{
14+
my_enum ev1;
15+
my_enum ev2;
16+
ev1 = first;
17+
ev2 = fifth;
18+
int i = 0;
19+
while(i < 10)
20+
{
21+
ev1++;
22+
assert(__CPROVER_enum_is_in_range(ev1));
23+
i++;
24+
}
25+
return 0;
26+
}

‎regression/cbmc/enum_is_in_range/enum_test8.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
enum_test8.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): FAILURE$
7+
--
8+
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS$
9+
^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
10+
--
11+
This test is for the enum_is_in_range working properly and detecting
12+
when the enum is not in range. The negation tests are to ensure the
13+
out of range is detected, and if the function is not defined.

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2961,6 +2961,33 @@ exprt c_typecheck_baset::do_special_functions(
29612961
overflow.type() = bool_typet{};
29622962
return overflow;
29632963
}
2964+
else if(identifier == CPROVER_PREFIX "enum_is_in_range")
2965+
{
2966+
// Check correct number of arguments
2967+
if(expr.arguments().size() != 1)
2968+
{
2969+
std::ostringstream error_message;
2970+
error_message << expr.source_location().as_string() << ": " << identifier
2971+
<< " takes exactly 1 argument, but "
2972+
<< expr.arguments().size() << " were provided";
2973+
throw invalid_source_file_exceptiont{error_message.str()};
2974+
}
2975+
auto arg1 = expr.arguments()[0];
2976+
typecheck_expr(arg1);
2977+
if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
2978+
{
2979+
// Can't enum range check a non-enum
2980+
std::ostringstream error_message;
2981+
error_message << expr.source_location().as_string() << ": " << identifier
2982+
<< " expects enum, but (" << expr2c(arg1, *this)
2983+
<< ") has type `" << type2c(arg1.type(), *this) << '`';
2984+
throw invalid_source_file_exceptiont{error_message.str()};
2985+
}
2986+
else
2987+
{
2988+
return expr;
2989+
}
2990+
}
29642991
else if(
29652992
identifier == "__builtin_add_overflow" ||
29662993
identifier == "__builtin_sub_overflow" ||

‎src/ansi-c/cprover_builtin_headers.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -103,3 +103,6 @@ __CPROVER_bool __CPROVER_overflow_mult();
103103
__CPROVER_bool __CPROVER_overflow_plus();
104104
__CPROVER_bool __CPROVER_overflow_shl();
105105
__CPROVER_bool __CPROVER_overflow_unary_minus();
106+
107+
// enumerations
108+
__CPROVER_bool __CPROVER_enum_is_in_range();

‎src/goto-programs/builtin_functions.cpp

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -611,6 +611,32 @@ exprt make_va_list(const exprt &expr)
611611
return result;
612612
}
613613

614+
void goto_convertt::do_enum_is_in_range(
615+
const exprt &lhs,
616+
const symbol_exprt &function,
617+
const exprt::operandst &arguments,
618+
goto_programt &dest)
619+
{
620+
PRECONDITION(arguments.size() == 1);
621+
const auto enum_expr = arguments.front();
622+
const auto enum_type =
623+
type_try_dynamic_cast<c_enum_tag_typet>(enum_expr.type());
624+
PRECONDITION(enum_type);
625+
const c_enum_typet &c_enum_type = ns.follow_tag(*enum_type);
626+
const c_enum_typet::memberst enum_values = c_enum_type.members();
627+
628+
exprt::operandst disjuncts;
629+
for(const auto &enum_value : enum_values)
630+
{
631+
constant_exprt val{enum_value.get_value(), *enum_type};
632+
disjuncts.push_back(equal_exprt(enum_expr, std::move(val)));
633+
}
634+
635+
code_assignt assignment(lhs, disjunction(disjuncts));
636+
assignment.add_source_location() = function.source_location();
637+
copy(assignment, ASSIGN, dest);
638+
}
639+
614640
/// add function calls to function queue for later processing
615641
void goto_convertt::do_function_call_symbol(
616642
const exprt &lhs,
@@ -735,6 +761,10 @@ void goto_convertt::do_function_call_symbol(
735761
throw 0;
736762
}
737763
}
764+
else if(identifier == CPROVER_PREFIX "enum_is_in_range")
765+
{
766+
do_enum_is_in_range(lhs, function, arguments, dest);
767+
}
738768
else if(
739769
identifier == CPROVER_PREFIX "assert" ||
740770
identifier == CPROVER_PREFIX "precondition" ||

0 commit comments

Comments
 (0)