Skip to content

Commit 4520385

Browse files
tautschnigtautschnig
committed
New expression: find_first_set_exprt
Rather than ad-hoc handling __builtin_ffs (and its variants) in the C front-end, make find-first-set available across the code base.
1 parent 66d3773 commit 4520385

File tree

16 files changed

+190
-65
lines changed

16 files changed

+190
-65
lines changed

‎regression/cbmc-library/__builtin_ffs-01/main.c renamed to ‎regression/cbmc/__builtin_ffs-01/main.c

Lines changed: 12 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,11 @@ int __builtin_ffsl(long);
77
int __builtin_ffsll(long long);
88
#endif
99

10+
#ifdef _MSC_VER
11+
# define _Static_assert(x, m) static_assert(x, m)
12+
#endif
13+
1014
int __VERIFIER_nondet_int();
11-
long __VERIFIER_nondet_long();
12-
long long __VERIFIER_nondet_long_long();
1315

1416
// http://graphics.stanford.edu/~seander/bithacks.html#ZerosOnRightMultLookup
1517
static const int multiply_de_bruijn_bit_position[32] = {
@@ -18,14 +20,14 @@ static const int multiply_de_bruijn_bit_position[32] = {
1820

1921
int main()
2022
{
21-
assert(__builtin_ffs(0) == 0);
22-
assert(__builtin_ffs(-1) == 1);
23-
assert(__builtin_ffs(INT_MIN) == sizeof(int) * 8);
24-
assert(__builtin_ffsl(INT_MIN) == sizeof(int) * 8);
25-
assert(__builtin_ffsl(LONG_MIN) == sizeof(long) * 8);
26-
assert(__builtin_ffsll(INT_MIN) == sizeof(int) * 8);
27-
assert(__builtin_ffsll(LLONG_MIN) == sizeof(long long) * 8);
28-
assert(__builtin_ffs(INT_MAX) == 1);
23+
_Static_assert(__builtin_ffs(0) == 0, "");
24+
_Static_assert(__builtin_ffs(-1) == 1, "");
25+
_Static_assert(__builtin_ffs(INT_MIN) == sizeof(int) * 8, "");
26+
_Static_assert(__builtin_ffsl(INT_MIN) == sizeof(int) * 8, "");
27+
_Static_assert(__builtin_ffsl(LONG_MIN) == sizeof(long) * 8, "");
28+
_Static_assert(__builtin_ffsll(INT_MIN) == sizeof(int) * 8, "");
29+
_Static_assert(__builtin_ffsll(LLONG_MIN) == sizeof(long long) * 8, "");
30+
_Static_assert(__builtin_ffs(INT_MAX) == 1, "");
2931

3032
int i = __VERIFIER_nondet_int();
3133
__CPROVER_assume(i != 0);

‎regression/cbmc-library/__builtin_ffs-01/test.desc renamed to ‎regression/cbmc/__builtin_ffs-01/test.desc

File renamed without changes.

‎scripts/expected_doxygen_warnings.txt

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -82,20 +82,20 @@
8282
warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8383
warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8484
warning: Included by graph for 'goto_model.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
85-
warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
85+
warning: Included by graph for 'arith_tools.h' not generated, too many nodes (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8686
warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8787
warning: Included by graph for 'config.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8888
warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8989
warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
9090
warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
91-
warning: Included by graph for 'invariant.h' not generated, too many nodes (188), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
91+
warning: Included by graph for 'invariant.h' not generated, too many nodes (189), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
9292
warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
9393
warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
9494
warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
9595
warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (101), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
9696
warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
97-
warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
97+
warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (79), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
9898
warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
99-
warning: Included by graph for 'std_expr.h' not generated, too many nodes (245), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
99+
warning: Included by graph for 'std_expr.h' not generated, too many nodes (246), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
100100
warning: Included by graph for 'std_types.h' not generated, too many nodes (121), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
101101
warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2698,6 +2698,24 @@ exprt c_typecheck_baset::do_special_functions(
26982698

26992699
return std::move(clz);
27002700
}
2701+
else if(
2702+
identifier == "__builtin_ffs" || identifier == "__builtin_ffsl" ||
2703+
identifier == "__builtin_ffsll")
2704+
{
2705+
if(expr.arguments().size() != 1)
2706+
{
2707+
error().source_location = f_op.source_location();
2708+
error() << identifier << " expects one operand" << eom;
2709+
throw 0;
2710+
}
2711+
2712+
typecheck_function_call_arguments(expr);
2713+
2714+
find_first_set_exprt ffs{expr.arguments().front(), expr.type()};
2715+
ffs.add_source_location() = source_location;
2716+
2717+
return std::move(ffs);
2718+
}
27012719
else if(identifier==CPROVER_PREFIX "equal")
27022720
{
27032721
if(expr.arguments().size()!=2)

‎src/ansi-c/expr2c.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3899,6 +3899,9 @@ std::string expr2ct::convert_with_precedence(
38993899
else if(src.id() == ID_count_leading_zeros)
39003900
return convert_function(src, "__builtin_clz");
39013901

3902+
else if(src.id() == ID_find_first_set)
3903+
return convert_function(src, "__builtin_ffs");
3904+
39023905
// no C language expression for internal representation
39033906
return convert_norep(src, precedence);
39043907
}

‎src/ansi-c/library/gcc.c

Lines changed: 0 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -33,57 +33,6 @@ inline void __sync_synchronize(void)
3333
#endif
3434
}
3535

36-
/* FUNCTION: __builtin_ffs */
37-
38-
int __builtin_clz(unsigned int x);
39-
40-
inline int __builtin_ffs(int x)
41-
{
42-
if(x == 0)
43-
return 0;
44-
45-
#pragma CPROVER check push
46-
#pragma CPROVER check disable "conversion"
47-
unsigned int u = (unsigned int)x;
48-
#pragma CPROVER check pop
49-
50-
return sizeof(int) * 8 - __builtin_clz(u & ~(u - 1));
51-
}
52-
53-
/* FUNCTION: __builtin_ffsl */
54-
55-
int __builtin_clzl(unsigned long x);
56-
57-
inline int __builtin_ffsl(long x)
58-
{
59-
if(x == 0)
60-
return 0;
61-
62-
#pragma CPROVER check push
63-
#pragma CPROVER check disable "conversion"
64-
unsigned long u = (unsigned long)x;
65-
#pragma CPROVER check pop
66-
67-
return sizeof(long) * 8 - __builtin_clzl(u & ~(u - 1));
68-
}
69-
70-
/* FUNCTION: __builtin_ffsll */
71-
72-
int __builtin_clzll(unsigned long long x);
73-
74-
inline int __builtin_ffsll(long long x)
75-
{
76-
if(x == 0)
77-
return 0;
78-
79-
#pragma CPROVER check push
80-
#pragma CPROVER check disable "conversion"
81-
unsigned long long u = (unsigned long long)x;
82-
#pragma CPROVER check pop
83-
84-
return sizeof(long long) * 8 - __builtin_clzll(u & ~(u - 1));
85-
}
86-
8736
/* FUNCTION: __atomic_test_and_set */
8837

8938
void __atomic_thread_fence(int memorder);

‎src/solvers/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,7 @@ SRC = $(BOOLEFORCE_SRC) \
141141
floatbv/float_approximation.cpp \
142142
lowering/byte_operators.cpp \
143143
lowering/count_leading_zeros.cpp \
144+
lowering/find_first_set.cpp \
144145
lowering/functions.cpp \
145146
lowering/popcount.cpp \
146147
bdd/miniBDD/miniBDD.cpp \

‎src/solvers/flattening/boolbv.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -230,6 +230,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
230230
return convert_bv(lower_popcount(to_popcount_expr(expr), ns));
231231
else if(expr.id() == ID_count_leading_zeros)
232232
return convert_bv(lower_clz(to_count_leading_zeros_expr(expr), ns));
233+
else if(expr.id() == ID_find_first_set)
234+
return convert_bv(lower_ffs(to_find_first_set_expr(expr), ns));
233235

234236
return conversion_failed(expr);
235237
}

‎src/solvers/lowering/expr_lowering.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Michael Tautschnig
1414
class byte_extract_exprt;
1515
class byte_update_exprt;
1616
class count_leading_zeros_exprt;
17+
class find_first_set_exprt;
1718
class namespacet;
1819
class popcount_exprt;
1920

@@ -57,4 +58,10 @@ exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns);
5758
/// \return Semantically equivalent expression
5859
exprt lower_clz(const count_leading_zeros_exprt &expr, const namespacet &ns);
5960

61+
/// Lower a find_first_set_exprt to arithmetic and logic expressions.
62+
/// \param expr: Input expression to be translated
63+
/// \param ns: Namespace for type lookups
64+
/// \return Semantically equivalent expression
65+
exprt lower_ffs(const find_first_set_exprt &expr, const namespacet &ns);
66+
6067
#endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */

‎src/solvers/lowering/find_first_set.cpp

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
/*******************************************************************\
2+
3+
Module: Lowering of find_first_set
4+
5+
Author: Michael Tautschnig
6+
7+
\*******************************************************************/
8+
9+
#include "expr_lowering.h"
10+
11+
#include <util/arith_tools.h>
12+
#include <util/bitvector_expr.h>
13+
#include <util/invariant.h>
14+
#include <util/pointer_offset_size.h>
15+
#include <util/simplify_expr.h>
16+
#include <util/std_expr.h>
17+
18+
exprt lower_ffs(const find_first_set_exprt &expr, const namespacet &ns)
19+
{
20+
exprt x = expr.op();
21+
const auto x_width = pointer_offset_bits(x.type(), ns);
22+
CHECK_RETURN(x_width.has_value() && *x_width >= 1);
23+
const std::size_t int_width = numeric_cast_v<std::size_t>(*x_width);
24+
25+
// bitwidth(x) - clz(x & ~((unsigned)x - 1));
26+
const unsignedbv_typet ut{int_width};
27+
minus_exprt minus_one{typecast_exprt::conditional_cast(x, ut),
28+
from_integer(1, ut)};
29+
count_leading_zeros_exprt clz{bitand_exprt{
30+
x, bitnot_exprt{typecast_exprt::conditional_cast(minus_one, x.type())}}};
31+
minus_exprt result{from_integer(*x_width, x.type()), lower_clz(clz, ns)};
32+
33+
return simplify_expr(
34+
typecast_exprt::conditional_cast(result, expr.type()), ns);
35+
}

0 commit comments

Comments
 (0)