Skip to content

Commit 9a19114

Browse files
tautschnigtautschnig
committed
Rewrite byte_extract from multi-dimensional array
As a follow-up to 78839a9: add support for rewriting multiple-of-element size access to arrays when working with multi-dimensional arrays. Fixes: #8796
1 parent 76dd20f commit 9a19114

File tree

4 files changed

+164
-8
lines changed

4 files changed

+164
-8
lines changed

‎regression/contracts-dfcc/multi_dimensional_array_performance/main.c‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
#include <stdint.h>
2+
3+
#define __contract__(x) x
4+
#define __loop__(x) x
5+
6+
/* https://diffblue.github.io/cbmc/contracts-assigns.html */
7+
#define assigns(...) __CPROVER_assigns(__VA_ARGS__)
8+
9+
/* https://diffblue.github.io/cbmc/contracts-requires-ensures.html */
10+
#define requires(...) __CPROVER_requires(__VA_ARGS__)
11+
#define ensures(...) __CPROVER_ensures(__VA_ARGS__)
12+
/* https://diffblue.github.io/cbmc/contracts-loops.html */
13+
#define invariant(...) __CPROVER_loop_invariant(__VA_ARGS__)
14+
15+
#define memory_slice(...) __CPROVER_object_upto(__VA_ARGS__)
16+
#define memory_no_alias(...) __CPROVER_is_fresh(__VA_ARGS__)
17+
18+
/*
19+
* Prevent clang-format from corrupting CBMC's special ==> operator
20+
*/
21+
/* clang-format off */
22+
#define forall(qvar, qvar_lb, qvar_ub, predicate) \
23+
__CPROVER_forall \
24+
{ \
25+
unsigned qvar; \
26+
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate) \
27+
}
28+
29+
/* clang-format on */
30+
31+
/*
32+
* Prevent clang-format from corrupting CBMC's special ==> operator
33+
*/
34+
/* clang-format off */
35+
#define CBMC_CONCAT_(left, right) left##right
36+
#define CBMC_CONCAT(left, right) CBMC_CONCAT_(left, right)
37+
38+
#define array_bound_core(qvar, qvar_lb, qvar_ub, array_var, \
39+
value_lb, value_ub) \
40+
__CPROVER_forall \
41+
{ \
42+
unsigned qvar; \
43+
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
44+
(((int)(value_lb) <= ((array_var)[(qvar)])) && \
45+
(((array_var)[(qvar)]) < (int)(value_ub))) \
46+
}
47+
48+
#define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \
49+
array_bound_core(CBMC_CONCAT(_cbmc_idx, __LINE__), (qvar_lb), \
50+
(qvar_ub), (array_var), (value_lb), (value_ub))
51+
/* clang-format on */
52+
53+
#define MLDSA_K 2
54+
#define MLDSA_L 1
55+
#define MLDSA_N 16
56+
#define MLDSA_Q 8380417
57+
58+
typedef struct
59+
{
60+
int32_t coeffs[MLDSA_N];
61+
} mld_poly;
62+
63+
typedef struct
64+
{
65+
mld_poly vec[MLDSA_L];
66+
} mld_polyvecl;
67+
68+
typedef struct
69+
{
70+
mld_polyvecl vec[MLDSA_K];
71+
} mld_polymat;
72+
73+
74+
void mld_poly_permute_bitrev_to_custom(int32_t p[MLDSA_N])
75+
__contract__(
76+
requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N))
77+
requires(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q))
78+
assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N))
79+
ensures(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q))
80+
);
81+
82+
void mld_polymat_permute_bitrev_to_custom(mld_polymat *mat)
83+
__contract__(
84+
requires(memory_no_alias(mat, sizeof(mld_polymat)))
85+
requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
86+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
87+
assigns(memory_slice(mat, sizeof(mld_polymat)))
88+
ensures(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
89+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
90+
);
91+
92+
void mld_polymat_permute_bitrev_to_custom(mld_polymat *mat)
93+
{
94+
unsigned int i, j;
95+
for (i = 0; i < MLDSA_K; i++)
96+
__loop__(
97+
assigns(i, j, memory_slice(mat, sizeof(mld_polymat)))
98+
invariant(i <= MLDSA_K)
99+
invariant(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
100+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
101+
)
102+
{
103+
for (j = 0; j < MLDSA_L; j++)
104+
__loop__(
105+
assigns(j, memory_slice(mat, sizeof(mld_polymat)))
106+
invariant(i <= MLDSA_K)
107+
invariant(j <= MLDSA_L)
108+
invariant(forall(k2, 0, MLDSA_K, forall(l2, 0, MLDSA_L,
109+
array_bound(mat->vec[k2].vec[l2].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
110+
)
111+
{
112+
mld_poly_permute_bitrev_to_custom(mat->vec[i].vec[j].coeffs);
113+
}
114+
}
115+
}
116+
117+
int main()
118+
{
119+
mld_polymat *m;
120+
mld_polymat_permute_bitrev_to_custom(m);
121+
}

‎regression/contracts-dfcc/multi_dimensional_array_performance/program.desc‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--dfcc main --enforce-contract mld_polymat_permute_bitrev_to_custom --replace-call-with-contract mld_poly_permute_bitrev_to_custom --apply-loop-contracts _ --slice-formula --no-array-field-sensitivity --program-only
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
byte_extract_(big|little)_endian\([^,]*, [^,]+\* 4[^,]*, signed int\)
8+
--

‎regression/contracts-dfcc/multi_dimensional_array_performance/test.desc‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--dfcc main --enforce-contract mld_polymat_permute_bitrev_to_custom --replace-call-with-contract mld_poly_permute_bitrev_to_custom --apply-loop-contracts _ --slice-formula --no-array-field-sensitivity
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

‎src/util/pointer_offset_size.cpp‎

Lines changed: 27 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -722,6 +722,9 @@ std::optional<exprt> get_subexpression_at_offset(
722722
return {};
723723
}
724724

725+
const mp_integer elem_size_bytes =
726+
*elem_size_bits / config.ansi_c.char_width;
727+
725728
// If we have an offset C + x (where C is a constant) we can try to
726729
// recurse by first looking at the member at offset C.
727730
if(
@@ -766,14 +769,12 @@ std::optional<exprt> get_subexpression_at_offset(
766769
const exprt &other_factor =
767770
mul.op0().is_constant() ? mul.op1() : mul.op0();
768771

769-
if(const_factor % (*elem_size_bits / config.ansi_c.char_width) != 0)
772+
if(const_factor % elem_size_bytes != 0)
770773
return {};
771774

772775
exprt index = mult_exprt{
773776
other_factor,
774-
from_integer(
775-
const_factor / (*elem_size_bits / config.ansi_c.char_width),
776-
other_factor.type())};
777+
from_integer(const_factor / elem_size_bytes, other_factor.type())};
777778

778779
return get_subexpression_at_offset(
779780
index_exprt{
@@ -798,14 +799,32 @@ std::optional<exprt> get_subexpression_at_offset(
798799
const exprt &other_factor =
799800
offset_mult.op0().is_constant() ? offset_mult.op1() : offset_mult.op0();
800801

801-
if(const_factor % (*elem_size_bits / config.ansi_c.char_width) != 0)
802+
if(
803+
target_size_bits < elem_size_bits && const_factor < elem_size_bytes &&
804+
elem_size_bytes % const_factor == 0)
805+
{
806+
const mp_integer index_divider = elem_size_bytes / const_factor;
807+
exprt index = div_exprt{
808+
other_factor, from_integer(index_divider, other_factor.type())};
809+
exprt remaining_offset = mult_exprt{
810+
mod_exprt{
811+
other_factor, from_integer(index_divider, other_factor.type())},
812+
from_integer(const_factor, other_factor.type())};
813+
814+
return get_subexpression_at_offset(
815+
index_exprt{
816+
expr,
817+
typecast_exprt::conditional_cast(index, array_type->index_type())},
818+
remaining_offset,
819+
target_type,
820+
ns);
821+
}
822+
else if(const_factor % elem_size_bytes != 0)
802823
return {};
803824

804825
exprt index = mult_exprt{
805826
other_factor,
806-
from_integer(
807-
const_factor / (*elem_size_bits / config.ansi_c.char_width),
808-
other_factor.type())};
827+
from_integer(const_factor / elem_size_bytes, other_factor.type())};
809828

810829
return get_subexpression_at_offset(
811830
index_exprt{

0 commit comments

Comments
 (0)