Skip to content

Commit 4d6947d

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 b1fe1d8 commit 4d6947d

File tree

16 files changed

+188
-65
lines changed

16 files changed

+188
-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: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3800,6 +3800,7 @@ expr2ct::convert_function_or_norep(const exprt &src, unsigned &precedence)
38003800
{ID_concatenation, "CONCATENATION"},
38013801
{ID_count_leading_zeros, "__builtin_clz"},
38023802
{ID_dynamic_object, "DYNAMIC_OBJECT"},
3803+
{ID_find_first_set, "__builtin_ffs"},
38033804
{ID_floatbv_div, "FLOAT/"},
38043805
{ID_floatbv_minus, "FLOAT-"},
38053806
{ID_floatbv_mult, "FLOAT*"},

‎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+
}

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1992,6 +1992,11 @@ void smt2_convt::convert_expr(const exprt &expr)
19921992
exprt lowered = lower_clz(to_count_leading_zeros_expr(expr), ns);
19931993
convert_expr(lowered);
19941994
}
1995+
else if(expr.id() == ID_find_first_set)
1996+
{
1997+
exprt lowered = lower_ffs(to_find_first_set_expr(expr), ns);
1998+
convert_expr(lowered);
1999+
}
19952000
else
19962001
INVARIANT_WITH_DIAGNOSTICS(
19972002
false,

‎src/util/bitvector_expr.h

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -766,4 +766,77 @@ inline count_leading_zeros_exprt &to_count_leading_zeros_expr(exprt &expr)
766766
return ret;
767767
}
768768

769+
/// \brief Returns one plus the index of the least-significant one bit, or zero
770+
/// if the operand is zero.
771+
class find_first_set_exprt : public unary_exprt
772+
{
773+
public:
774+
find_first_set_exprt(exprt _op, typet _type)
775+
: unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
776+
{
777+
}
778+
779+
explicit find_first_set_exprt(const exprt &_op)
780+
: find_first_set_exprt(_op, _op.type())
781+
{
782+
}
783+
784+
static void check(
785+
const exprt &expr,
786+
const validation_modet vm = validation_modet::INVARIANT)
787+
{
788+
DATA_CHECK(
789+
vm,
790+
expr.operands().size() == 1,
791+
"unary expression must have a single operand");
792+
DATA_CHECK(
793+
vm,
794+
can_cast_type<bitvector_typet>(to_unary_expr(expr).op().type()),
795+
"operand must be of bitvector type");
796+
}
797+
798+
static void validate(
799+
const exprt &expr,
800+
const namespacet &,
801+
const validation_modet vm = validation_modet::INVARIANT)
802+
{
803+
check(expr, vm);
804+
}
805+
};
806+
807+
template <>
808+
inline bool can_cast_expr<find_first_set_exprt>(const exprt &base)
809+
{
810+
return base.id() == ID_find_first_set;
811+
}
812+
813+
inline void validate_expr(const find_first_set_exprt &value)
814+
{
815+
validate_operands(value, 1, "find_first_set must have one operand");
816+
}
817+
818+
/// \brief Cast an exprt to a \ref find_first_set_exprt
819+
///
820+
/// \a expr must be known to be \ref find_first_set_exprt.
821+
///
822+
/// \param expr: Source expression
823+
/// \return Object of type \ref find_first_set_exprt
824+
inline const find_first_set_exprt &to_find_first_set_expr(const exprt &expr)
825+
{
826+
PRECONDITION(expr.id() == ID_find_first_set);
827+
const find_first_set_exprt &ret =
828+
static_cast<const find_first_set_exprt &>(expr);
829+
validate_expr(ret);
830+
return ret;
831+
}
832+
833+
/// \copydoc to_find_first_set_expr(const exprt &)
834+
inline find_first_set_exprt &to_find_first_set_expr(exprt &expr)
835+
{
836+
PRECONDITION(expr.id() == ID_find_first_set);
837+
find_first_set_exprt &ret = static_cast<find_first_set_exprt &>(expr);
838+
validate_expr(ret);
839+
return ret;
840+
}
841+
769842
#endif // CPROVER_UTIL_BITVECTOR_EXPR_H

‎src/util/format_expr.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -153,6 +153,8 @@ static std::ostream &format_rec(std::ostream &os, const unary_exprt &src)
153153
os << '-';
154154
else if(src.id() == ID_count_leading_zeros)
155155
os << "clz";
156+
else if(src.id() == ID_find_first_set)
157+
os << "ffs";
156158
else
157159
return os << src.pretty();
158160

‎src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -843,6 +843,7 @@ IREP_ID_ONE(min)
843843
IREP_ID_ONE(constant_interval)
844844
IREP_ID_TWO(C_bounds_check, #bounds_check)
845845
IREP_ID_ONE(count_leading_zeros)
846+
IREP_ID_ONE(find_first_set)
846847

847848
// Projects depending on this code base that wish to extend the list of
848849
// available ids should provide a file local_irep_ids.def in their source tree

‎src/util/simplify_expr.cpp

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,25 @@ simplify_exprt::simplify_clz(const count_leading_zeros_exprt &expr)
172172
return from_integer(n_leading_zeros, expr.type());
173173
}
174174

175+
simplify_exprt::resultt<>
176+
simplify_exprt::simplify_ffs(const find_first_set_exprt &expr)
177+
{
178+
const auto const_bits_opt = expr2bits(
179+
expr.op(), byte_extract_id() == ID_byte_extract_little_endian, ns);
180+
181+
if(!const_bits_opt.has_value())
182+
return unchanged(expr);
183+
184+
// expr2bits generates a bit string starting with the least-significant bit
185+
std::size_t first_one_bit = const_bits_opt->find('1');
186+
if(first_one_bit == std::string::npos)
187+
first_one_bit = 0;
188+
else
189+
++first_one_bit;
190+
191+
return from_integer(first_one_bit, expr.type());
192+
}
193+
175194
/// Simplify String.endsWith function when arguments are constant
176195
/// \param expr: the expression to simplify
177196
/// \param ns: namespace
@@ -2421,6 +2440,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
24212440
{
24222441
r = simplify_clz(to_count_leading_zeros_expr(expr));
24232442
}
2443+
else if(expr.id() == ID_find_first_set)
2444+
{
2445+
r = simplify_ffs(to_find_first_set_expr(expr));
2446+
}
24242447
else if(expr.id() == ID_function_application)
24252448
{
24262449
r = simplify_function_application(to_function_application_expr(expr));

‎src/util/simplify_expr_class.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ class div_exprt;
4242
class exprt;
4343
class extractbit_exprt;
4444
class extractbits_exprt;
45+
class find_first_set_exprt;
4546
class floatbv_typecast_exprt;
4647
class function_application_exprt;
4748
class ieee_float_op_exprt;
@@ -204,6 +205,9 @@ class simplify_exprt
204205
/// Try to simplify count-leading-zeros to a constant expression.
205206
NODISCARD resultt<> simplify_clz(const count_leading_zeros_exprt &);
206207

208+
/// Try to simplify find-first-set to a constant expression.
209+
NODISCARD resultt<> simplify_ffs(const find_first_set_exprt &);
210+
207211
// auxiliary
208212
bool simplify_if_implies(
209213
exprt &expr, const exprt &cond, bool truth, bool &new_truth);

0 commit comments

Comments
 (0)