Skip to content

Commit bb8cfaa

Browse files
tautschnigtautschnig
committed
C library: Check upper bounds in memset, memcpy, memmove
1 parent 7d4984f commit bb8cfaa

File tree

4 files changed

+98
-30
lines changed

4 files changed

+98
-30
lines changed

‎regression/cbmc/memcpy1/main.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <stdint.h>
2+
#include <string.h>
3+
4+
int main()
5+
{
6+
uint8_t a;
7+
uint32_t b;
8+
9+
memcpy(&b, &a, sizeof(b));
10+
11+
return 0;
12+
}

‎regression/cbmc/memcpy1/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--bounds-check --pointer-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
\[(__builtin___memcpy_chk|memcpy)\.pointer_dereference\.16\] dereference failure: pointer outside object bounds in \*\(\(\(const char \*\)src \+ \(signed long (long )?int\)n\) - \(signed long (long )?int\)1\): FAILURE$
8+
\*\* 1 of 17 failed
9+
--
10+
^warning: ignoring

‎regression/cbmc/memset3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ main.c
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
\[.*] dereference failure: pointer outside dynamic object bounds in .*: FAILURE
8-
\*\* 1 of .* failed \(.*\)
8+
\*\* 2 of .* failed \(.*\)
99
--
1010
^warning: ignoring

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

Lines changed: 75 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -548,10 +548,16 @@ void *memcpy(void *dst, const void *src, size_t n)
548548
__CPROVER_POINTER_OBJECT(src), "memcpy src/dst overlap");
549549
(void)*(char *)dst; // check that the memory is accessible
550550
(void)*(const char *)src; // check that the memory is accessible
551-
//for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
552-
char src_n[n];
553-
__CPROVER_array_copy(src_n, (char*)src);
554-
__CPROVER_array_replace((char*)dst, src_n);
551+
552+
if(n > 0)
553+
{
554+
(void)*(((char *)dst) + n - 1); // check that the memory is accessible
555+
(void)*(((const char *)src) + n - 1); // check that the memory is accessible
556+
//for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
557+
char src_n[n];
558+
__CPROVER_array_copy(src_n, (char *)src);
559+
__CPROVER_array_replace((char *)dst, src_n);
560+
}
555561
#endif
556562
return dst;
557563
}
@@ -581,10 +587,16 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
581587
(void)*(char *)dst; // check that the memory is accessible
582588
(void)*(const char *)src; // check that the memory is accessible
583589
(void)size;
584-
//for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
585-
char src_n[n];
586-
__CPROVER_array_copy(src_n, (char*)src);
587-
__CPROVER_array_replace((char*)dst, src_n);
590+
591+
if(n > 0)
592+
{
593+
(void)*(((char *)dst) + n - 1); // check that the memory is accessible
594+
(void)*(((const char *)src) + n - 1); // check that the memory is accessible
595+
//for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
596+
char src_n[n];
597+
__CPROVER_array_copy(src_n, (char *)src);
598+
__CPROVER_array_replace((char *)dst, src_n);
599+
}
588600
#endif
589601
return dst;
590602
}
@@ -618,11 +630,16 @@ void *memset(void *s, int c, size_t n)
618630
__CPROVER_is_zero_string(s)=0;
619631
#else
620632
(void)*(char *)s; // check that the memory is accessible
621-
//char *sp=s;
622-
//for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
623-
unsigned char s_n[n];
624-
__CPROVER_array_set(s_n, (unsigned char)c);
625-
__CPROVER_array_replace((unsigned char*)s, s_n);
633+
634+
if(n > 0)
635+
{
636+
(void)*(((char *)s) + n - 1); // check that the memory is accessible
637+
//char *sp=s;
638+
//for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
639+
unsigned char s_n[n];
640+
__CPROVER_array_set(s_n, (unsigned char)c);
641+
__CPROVER_array_replace((unsigned char *)s, s_n);
642+
}
626643
#endif
627644
return s;
628645
}
@@ -646,13 +663,21 @@ void *__builtin_memset(void *s, int c, __CPROVER_size_t n)
646663
__CPROVER_zero_string_length(s)=0;
647664
}
648665
else
666+
{
649667
__CPROVER_is_zero_string(s)=0;
668+
}
650669
#else
651-
//char *sp=s;
652-
//for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
653-
unsigned char s_n[n];
654-
__CPROVER_array_set(s_n, (unsigned char)c);
655-
__CPROVER_array_replace((unsigned char*)s, s_n);
670+
(void)*(char *)s; // check that the memory is accessible
671+
672+
if(n > 0)
673+
{
674+
(void)*(((char *)s) + n - 1); // check that the memory is accessible
675+
//char *sp=s;
676+
//for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
677+
unsigned char s_n[n];
678+
__CPROVER_array_set(s_n, (unsigned char)c);
679+
__CPROVER_array_replace((unsigned char *)s, s_n);
680+
}
656681
#endif
657682
return s;
658683
}
@@ -681,11 +706,16 @@ void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_
681706
#else
682707
(void)*(char *)s; // check that the memory is accessible
683708
(void)size;
684-
//char *sp=s;
685-
//for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
686-
unsigned char s_n[n];
687-
__CPROVER_array_set(s_n, (unsigned char)c);
688-
__CPROVER_array_replace((unsigned char*)s, s_n);
709+
710+
if(n > 0)
711+
{
712+
(void)*(((char *)s) + n - 1); // check that the memory is accessible
713+
//char *sp=s;
714+
//for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
715+
unsigned char s_n[n];
716+
__CPROVER_array_set(s_n, (unsigned char)c);
717+
__CPROVER_array_replace((unsigned char *)s, s_n);
718+
}
689719
#endif
690720
return s;
691721
}
@@ -716,9 +746,15 @@ void *memmove(void *dest, const void *src, size_t n)
716746
#else
717747
(void)*(char *)dest; // check that the memory is accessible
718748
(void)*(const char *)src; // check that the memory is accessible
719-
char src_n[n];
720-
__CPROVER_array_copy(src_n, (char*)src);
721-
__CPROVER_array_replace((char*)dest, src_n);
749+
750+
if(n > 0)
751+
{
752+
(void)*(((char *)dest) + n - 1); // check that the memory is accessible
753+
(void)*(((const char *)src) + n - 1); // check that the memory is accessible
754+
char src_n[n];
755+
__CPROVER_array_copy(src_n, (char *)src);
756+
__CPROVER_array_replace((char *)dest, src_n);
757+
}
722758
#endif
723759
return dest;
724760
}
@@ -746,12 +782,22 @@ void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_s
746782
__CPROVER_zero_string_length(dest)=__CPROVER_zero_string_length(src);
747783
}
748784
else
785+
{
749786
__CPROVER_is_zero_string(dest)=0;
787+
}
750788
#else
789+
(void)*(char *)dest; // check that the memory is accessible
790+
(void)*(const char *)src; // check that the memory is accessible
751791
(void)size;
752-
char src_n[n];
753-
__CPROVER_array_copy(src_n, (char*)src);
754-
__CPROVER_array_replace((char*)dest, src_n);
792+
793+
if(n > 0)
794+
{
795+
(void)*(((char *)dest) + n - 1); // check that the memory is accessible
796+
(void)*(((const char *)src) + n - 1); // check that the memory is accessible
797+
char src_n[n];
798+
__CPROVER_array_copy(src_n, (char *)src);
799+
__CPROVER_array_replace((char *)dest, src_n);
800+
}
755801
#endif
756802
return dest;
757803
}

0 commit comments

Comments
 (0)