Skip to content

Commit db8d846

Browse files
kroeningkroening
committed
use __CPROVER_r/w_ok in string.c library
1 parent 732ce2a commit db8d846

File tree

4 files changed

+32
-27
lines changed

4 files changed

+32
-27
lines changed

‎regression/cbmc/memcpy1/test.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ main.c
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
\[(__builtin___memcpy_chk|memcpy)\.pointer_dereference\.[0-9]+\] dereference failure: pointer outside object bounds in \*\(\(\(const char \*\)src \+ \(signed (long (long )?)?int\)n\) - (\(signed long (long )?int\))?1\): FAILURE$
7+
^\[main\.precondition_instance\..*\] memcpy source region readable: FAILURE$
88
\*\* 1 of [0-9]+ failed
99
--
1010
^warning: ignoring

‎regression/cbmc/memset1/test.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ main.c
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
\[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE
8-
\*\* 1 of 12 failed
7+
^\[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE$
8+
\*\* 1 of .* failed
99
--
1010
^warning: ignoring

‎regression/cbmc/memset3/test.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ main.c
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
\[.*] dereference failure: pointer outside dynamic object bounds in .*: FAILURE
8-
\*\* 2 of .* failed \(.*\)
7+
^\[main\.precondition_instance\..*] memset destination region writeable: FAILURE$
8+
\*\* 1 of .* failed \(.*\)
99
--
1010
^warning: ignoring

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

Lines changed: 27 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -597,13 +597,13 @@ void *memcpy(void *dst, const void *src, size_t n)
597597
__CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
598598
__CPROVER_POINTER_OBJECT(src),
599599
"memcpy src/dst overlap");
600+
__CPROVER_precondition(__CPROVER_r_ok(src, n),
601+
"memcpy source region readable");
602+
__CPROVER_precondition(__CPROVER_w_ok(dst, n),
603+
"memcpy destination region writeable");
600604

601605
if(n > 0)
602606
{
603-
(void)*(char *)dst; // check that the memory is accessible
604-
(void)*(const char *)src; // check that the memory is accessible
605-
(void)*(((char *)dst) + n - 1); // check that the memory is accessible
606-
(void)*(((const char *)src) + n - 1); // check that the memory is accessible
607607
//for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
608608
char src_n[n];
609609
__CPROVER_array_copy(src_n, (char *)src);
@@ -639,14 +639,14 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
639639
__CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
640640
__CPROVER_POINTER_OBJECT(src),
641641
"memcpy src/dst overlap");
642+
__CPROVER_precondition(__CPROVER_r_ok(src, n),
643+
"memcpy source region readable");
644+
__CPROVER_precondition(__CPROVER_w_ok(dst, n),
645+
"memcpy destination region writeable");
642646
(void)size;
643647

644648
if(n > 0)
645649
{
646-
(void)*(char *)dst; // check that the memory is accessible
647-
(void)*(const char *)src; // check that the memory is accessible
648-
(void)*(((char *)dst) + n - 1); // check that the memory is accessible
649-
(void)*(((const char *)src) + n - 1); // check that the memory is accessible
650650
//for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
651651
char src_n[n];
652652
__CPROVER_array_copy(src_n, (char *)src);
@@ -685,11 +685,11 @@ void *memset(void *s, int c, size_t n)
685685
else
686686
__CPROVER_is_zero_string(s)=0;
687687
#else
688+
__CPROVER_precondition(__CPROVER_w_ok(s, n),
689+
"memset destination region writeable");
688690

689691
if(n > 0)
690692
{
691-
(void)*(char *)s; // check that the memory is accessible
692-
(void)*(((char *)s) + n - 1); // check that the memory is accessible
693693
//char *sp=s;
694694
//for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
695695
unsigned char s_n[n];
@@ -724,11 +724,11 @@ void *__builtin_memset(void *s, int c, __CPROVER_size_t n)
724724
__CPROVER_is_zero_string(s)=0;
725725
}
726726
#else
727+
__CPROVER_precondition(__CPROVER_w_ok(s, n),
728+
"memset destination region writeable");
727729

728730
if(n > 0)
729731
{
730-
(void)*(char *)s; // check that the memory is accessible
731-
(void)*(((char *)s) + n - 1); // check that the memory is accessible
732732
//char *sp=s;
733733
//for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
734734
unsigned char s_n[n];
@@ -763,12 +763,12 @@ void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_
763763
else
764764
__CPROVER_is_zero_string(s)=0;
765765
#else
766+
__CPROVER_precondition(__CPROVER_w_ok(s, n),
767+
"memset destination region writeable");
766768
(void)size;
767769

768770
if(n > 0)
769771
{
770-
(void)*(char *)s; // check that the memory is accessible
771-
(void)*(((char *)s) + n - 1); // check that the memory is accessible
772772
//char *sp=s;
773773
//for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
774774
unsigned char s_n[n];
@@ -804,13 +804,13 @@ void *memmove(void *dest, const void *src, size_t n)
804804
else
805805
__CPROVER_is_zero_string(dest)=0;
806806
#else
807+
__CPROVER_precondition(__CPROVER_r_ok(src, n),
808+
"memmove source region readable");
809+
__CPROVER_precondition(__CPROVER_w_ok(dest, n),
810+
"memmove destination region writeable");
807811

808812
if(n > 0)
809813
{
810-
(void)*(char *)dest; // check that the memory is accessible
811-
(void)*(const char *)src; // check that the memory is accessible
812-
(void)*(((char *)dest) + n - 1); // check that the memory is accessible
813-
(void)*(((const char *)src) + n - 1); // check that the memory is accessible
814814
char src_n[n];
815815
__CPROVER_array_copy(src_n, (char *)src);
816816
__CPROVER_array_replace((char *)dest, src_n);
@@ -848,14 +848,14 @@ void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_s
848848
__CPROVER_is_zero_string(dest)=0;
849849
}
850850
#else
851+
__CPROVER_precondition(__CPROVER_r_ok(src, n),
852+
"memmove source region readable");
853+
__CPROVER_precondition(__CPROVER_w_ok(dest, n),
854+
"memmove destination region writeable");
851855
(void)size;
852856

853857
if(n > 0)
854858
{
855-
(void)*(char *)dest; // check that the memory is accessible
856-
(void)*(const char *)src; // check that the memory is accessible
857-
(void)*(((char *)dest) + n - 1); // check that the memory is accessible
858-
(void)*(((const char *)src) + n - 1); // check that the memory is accessible
859859
char src_n[n];
860860
__CPROVER_array_copy(src_n, (char *)src);
861861
__CPROVER_array_replace((char *)dest, src_n);
@@ -883,6 +883,11 @@ inline int memcmp(const void *s1, const void *s2, size_t n)
883883
__CPROVER_precondition(__CPROVER_buffer_size(s2)>=n,
884884
"memcmp buffer overflow of 2nd argument");
885885
#else
886+
__CPROVER_precondition(__CPROVER_r_ok(s1, n),
887+
"memcmp region 1 readable");
888+
__CPROVER_precondition(__CPROVER_r_ok(s2, n),
889+
"memcpy region 2 readable");
890+
886891
const unsigned char *sc1=s1, *sc2=s2;
887892
for(; n!=0; n--)
888893
{

0 commit comments

Comments
 (0)