summaryrefslogtreecommitdiffstats
path: root/src/file_jpg.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_jpg.c')
-rw-r--r--src/file_jpg.c1142
1 files changed, 814 insertions, 328 deletions
diff --git a/src/file_jpg.c b/src/file_jpg.c
index 8c8ae08..376f1b7 100644
--- a/src/file_jpg.c
+++ b/src/file_jpg.c
@@ -49,18 +49,22 @@
#include "file_jpg.h"
#include "file_tiff.h"
#include "setdate.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
+#if !defined(MAIN_jpg) && !defined(MAIN_fidentify)
extern const file_hint_t file_hint_doc;
extern const file_hint_t file_hint_indd;
extern const file_hint_t file_hint_mov;
extern const file_hint_t file_hint_riff;
extern const file_hint_t file_hint_rw2;
extern data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
+#endif
static void register_header_check_jpg(file_stat_t *file_stat);
-static int header_check_jpg(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new);
static void file_check_jpg(file_recovery_t *file_recovery);
-data_check_t data_check_jpg(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
+static data_check_t data_check_jpg(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
static int jpg_check_dht(const unsigned char *buffer, const unsigned int buffer_size, const unsigned i, const unsigned int size);
const file_hint_t file_hint_jpg= {
@@ -72,12 +76,12 @@ const file_hint_t file_hint_jpg= {
.register_header_check=&register_header_check_jpg
};
-static void register_header_check_jpg(file_stat_t *file_stat)
-{
- static const unsigned char jpg_header[3]= { 0xff,0xd8,0xff};
- register_header_check(0, jpg_header, sizeof(jpg_header), &header_check_jpg, file_stat);
-}
-
+/*@
+ @ requires \valid_read(buffer + (0 .. buffer_size-1));
+ @ requires \valid(height);
+ @ requires \valid(width);
+ @ requires \separated(buffer, height, width);
+ @*/
static void jpg_get_size(const unsigned char *buffer, const unsigned int buffer_size, unsigned int *height, unsigned int *width)
{
unsigned int i=2;
@@ -108,7 +112,7 @@ struct MP_IFD_Field
uint16_t tag;
uint16_t type;
uint32_t count;
- char value[0];
+ char value[4];
} __attribute__ ((gcc_struct, __packed__));
struct MP_Entry
@@ -120,6 +124,11 @@ struct MP_Entry
uint16_t dep2;
} __attribute__ ((gcc_struct, __packed__));
+/*@
+ @ requires size >= 8;
+ @ requires \valid_read(mpo + ( 0 .. size-1));
+ @ assigns \nothing;
+ @*/
static uint64_t check_mpo_be(const unsigned char *mpo, const uint64_t mpo_offset, const unsigned int size)
{
const uint16_t *tmp16;
@@ -129,40 +138,55 @@ static uint64_t check_mpo_be(const unsigned char *mpo, const uint64_t mpo_offset
unsigned int nbr;
unsigned int NumberOfImages=0;
unsigned int MPEntry_offset=0;
- const struct MP_Entry* MPEntry;
uint64_t max_offset=0;
#ifdef DEBUG_JPEG
log_info("check_mpo_be\n");
#endif
- if(offset+2 >= size)
+ if(offset >= size - 2)
return 0;
+ /*@ assert offset < size - 2; */
tmp16=(const uint16_t*)(&mpo[offset]);
nbr=be16(*tmp16);
offset+=2;
+ /* @offset: MP Index Fields*/
+ if(offset + nbr * 12 > size)
+ return 0;
+ /*@ assert offset + nbr * 12 <= size; */
+ /*@
+ @ loop invariant 0 <= i <= nbr;
+ @ loop assigns i, NumberOfImages, MPEntry_offset;
+ @ loop variant nbr-i;
+ @*/
for(i=0; i< nbr; i++)
{
- const struct MP_IFD_Field *field=(const struct MP_IFD_Field *)(&mpo[offset]);
- if(offset+12 > size)
- return 0;
+ /*@ assert 0 <= i < nbr; */
+ const unsigned char *field_ptr=&mpo[offset + i * 12];
+ /*@ assert \valid_read(field_ptr + ( 0 .. sizeof(struct MP_IFD_Field)-1)); */
+ const struct MP_IFD_Field *field=(const struct MP_IFD_Field *)field_ptr;
+ const unsigned int count=be32(field->count);
+ const unsigned int type=be16(field->type);
switch(be16(field->tag))
{
case 0xb000:
/* MPFVersion, type must be undefined */
- if(be16(field->type)!=7 || be32(field->count)!=4)
+ if(type!=7 || count!=4)
return 0;
break;
case 0xb001:
/* NumberOfImages, type must be long */
- if(be16(field->type)!=4 || be32(field->count)!=1)
+ if(type!=4 || count!=1)
return 0;
{
const uint32_t *tmp=(const uint32_t *)&field->value[0];
NumberOfImages=be32(*tmp);
+ if(NumberOfImages >= 0x100000)
+ return 0;
+ /*@ assert NumberOfImages < 0x100000; */
}
break;
case 0xb002:
/* MPEntry, type must be undefined */
- if(be16(field->type)!=7 || be32(field->count)!=16*NumberOfImages)
+ if(type!=7 || count!=16*NumberOfImages)
return 0;
{
const uint32_t *tmp=(const uint32_t *)&field->value[0];
@@ -170,74 +194,105 @@ static uint64_t check_mpo_be(const unsigned char *mpo, const uint64_t mpo_offset
}
break;
}
- offset+=12;
}
#ifdef DEBUG_JPEG
log_info("MPEntry_offset=%u, NumberOfImages=%u\n", MPEntry_offset, NumberOfImages);
#endif
+ /*@ assert NumberOfImages < 0x100000; */
+ if(MPEntry_offset > size)
+ return 0;
if(MPEntry_offset + 16*NumberOfImages > size)
return 0;
- for(i=0, MPEntry=(const struct MP_Entry*)(&mpo[MPEntry_offset]);
- i<NumberOfImages;
- i++, MPEntry++)
+ /*@
+ @ loop invariant 0 <= i <= NumberOfImages;
+ @ loop assigns i, max_offset;
+ @ loop variant NumberOfImages-i;
+ @*/
+ for(i=0; i<NumberOfImages; i++)
{
- uint64_t tmp=be32(MPEntry->offset)+be32(MPEntry->size);
+ /*@ assert 0 <= i < NumberOfImages; */
+ const unsigned char *MPEntry_ptr=&mpo[MPEntry_offset + i * sizeof(struct MP_Entry)];
+ /*@ assert \valid_read(MPEntry_ptr+ ( 0 .. sizeof(struct MP_Entry)-1)); */
+ const struct MP_Entry *MPEntry=(const struct MP_Entry*)MPEntry_ptr;
+ uint64_t tmp=be32(MPEntry->size);
#ifdef DEBUG_JPEG
log_info("offset=%lu, size=%lu\n",
(long unsigned)be32(MPEntry->offset),
(long unsigned)be32(MPEntry->size));
#endif
if(be32(MPEntry->offset)>0)
- tmp+=mpo_offset;
+ tmp+=be32(MPEntry->offset)+mpo_offset;
if(max_offset < tmp)
max_offset = tmp;
}
return max_offset;
}
+/*@
+ @ requires size >= 8;
+ @ requires \valid_read(mpo + ( 0 .. size-1));
+ @ assigns \nothing;
+ @*/
static uint64_t check_mpo_le(const unsigned char *mpo, const uint64_t mpo_offset, const unsigned int size)
{
const uint16_t *tmp16;
+ /* Offset to first IFD */
const uint32_t *tmp32=(const uint32_t *)(&mpo[4]);
unsigned int offset=le32(*tmp32);
unsigned int i;
unsigned int nbr;
unsigned int NumberOfImages=0;
unsigned int MPEntry_offset=0;
- const struct MP_Entry* MPEntry;
uint64_t max_offset=0;
#ifdef DEBUG_JPEG
log_info("check_mpo_le\n");
#endif
- if(offset+2 >= size)
+ if(offset >= size - 2)
return 0;
+ /*@ assert offset < size - 2; */
tmp16=(const uint16_t*)(&mpo[offset]);
nbr=le16(*tmp16);
offset+=2;
+ /* @offset: MP Index Fields*/
+ if(offset + nbr * 12 > size)
+ return 0;
+ /*@ assert offset + nbr * 12 <= size; */
+ /*@
+ @ loop invariant 0 <= i <= nbr;
+ @ loop assigns i, NumberOfImages, MPEntry_offset;
+ @ loop variant nbr-i;
+ @*/
for(i=0; i< nbr; i++)
{
- const struct MP_IFD_Field *field=(const struct MP_IFD_Field *)(&mpo[offset]);
- if(offset+12 > size)
- return 0;
+ /*@ assert 0 <= i < nbr; */
+ const unsigned char *field_ptr=&mpo[offset + i * 12];
+ /*@ assert \valid_read(field_ptr + ( 0 .. sizeof(struct MP_IFD_Field)-1)); */
+ const struct MP_IFD_Field *field=(const struct MP_IFD_Field *)field_ptr;
+ /*@ assert \valid_read(field); */
+ const unsigned int count=le32(field->count);
+ const unsigned int type=le16(field->type);
switch(le16(field->tag))
{
case 0xb000:
/* MPFVersion, type must be undefined */
- if(le16(field->type)!=7 || le32(field->count)!=4)
+ if(type!=7 || count!=4)
return 0;
break;
case 0xb001:
/* NumberOfImages, type must be long */
- if(le16(field->type)!=4 || le32(field->count)!=1)
+ if(type!=4 || count!=1)
return 0;
{
const uint32_t *tmp=(const uint32_t *)&field->value[0];
NumberOfImages=le32(*tmp);
+ if(NumberOfImages >= 0x100000)
+ return 0;
+ /*@ assert NumberOfImages < 0x100000; */
}
break;
case 0xb002:
/* MPEntry, type must be undefined */
- if(le16(field->type)!=7 || le32(field->count)!=16*NumberOfImages)
+ if(type!=7 || count!=16*NumberOfImages)
return 0;
{
const uint32_t *tmp=(const uint32_t *)&field->value[0];
@@ -245,33 +300,51 @@ static uint64_t check_mpo_le(const unsigned char *mpo, const uint64_t mpo_offset
}
break;
}
- offset+=12;
}
#ifdef DEBUG_JPEG
log_info("MPEntry_offset=%u, NumberOfImages=%u\n", MPEntry_offset, NumberOfImages);
#endif
+ /*@ assert NumberOfImages < 0x100000; */
+ if(MPEntry_offset > size)
+ return 0;
if(MPEntry_offset + 16*NumberOfImages > size)
return 0;
- for(i=0, MPEntry=(const struct MP_Entry*)(&mpo[MPEntry_offset]);
- i<NumberOfImages;
- i++, MPEntry++)
+ /*@
+ @ loop invariant 0 <= i <= NumberOfImages;
+ @ loop assigns i, max_offset;
+ @ loop variant NumberOfImages-i;
+ @*/
+ for(i=0; i<NumberOfImages; i++)
{
- uint64_t tmp=le32(MPEntry->offset)+le32(MPEntry->size);
+ /*@ assert 0 <= i < NumberOfImages; */
+ const unsigned char *MPEntry_ptr=&mpo[MPEntry_offset + i * sizeof(struct MP_Entry)];
+ /*@ assert \valid_read(MPEntry_ptr+ ( 0 .. sizeof(struct MP_Entry)-1)); */
+ const struct MP_Entry *MPEntry=(const struct MP_Entry*)MPEntry_ptr;
+ uint64_t tmp=le32(MPEntry->size);
#ifdef DEBUG_JPEG
log_info("offset=%lu, size=%lu\n",
(long unsigned)le32(MPEntry->offset),
(long unsigned)le32(MPEntry->size));
#endif
if(le32(MPEntry->offset)>0)
- tmp+=mpo_offset;
+ tmp+=(uint64_t)le32(MPEntry->offset) + mpo_offset;
if(max_offset < tmp)
max_offset = tmp;
}
return max_offset;
}
+/*@
+ @ requires size >= 8;
+ @ requires \valid_read(mpo + ( 0 .. size-1));
+ @ assigns \nothing;
+ @*/
static uint64_t check_mpo(const unsigned char *mpo, const uint64_t offset, const unsigned int size)
{
+ /* MP header:
+ * - MP Endian (4Byte)
+ * - Offset to First IFD (4Byte)
+ */
if(mpo[0]=='I' && mpo[1]=='I' && mpo[2]=='*' && mpo[3]==0)
{
return check_mpo_le(mpo, offset, size);
@@ -283,6 +356,13 @@ static uint64_t check_mpo(const unsigned char *mpo, const uint64_t offset, const
return 0;
}
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires valid_read_string((char *)&fr->filename);
+ @ requires \initialized(&fr->time);
+ @ requires fr->file_check==&file_check_mpo;
+ @*/
static void file_check_mpo(file_recovery_t *fr)
{
unsigned char buffer[512];
@@ -300,12 +380,21 @@ static void file_check_mpo(file_recovery_t *fr)
do
{
offset+=(uint64_t)2+size;
+ if(offset >= 0x8000000000000000)
+ {
+ fr->file_size=0;
+ return ;
+ }
+ /*@ assert offset < 0x8000000000000000; */
if(my_fseek(fr->handle, offset, SEEK_SET) < 0)
{
fr->file_size=0;
return ;
}
nbytes=fread(&buffer, 1, sizeof(buffer), fr->handle);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&buffer, sizeof(buffer));
+#endif
// log_info("file_check_mpo offset=%llu => nbytes=%d, buffer=%02x %02x\n",
// (long long unsigned)offset, nbytes, buffer[0], buffer[1]);
/* 0xda SOS Start Of Scan */
@@ -314,19 +403,22 @@ static void file_check_mpo(file_recovery_t *fr)
fr->file_size=0;
return ;
}
+ /*@ assert nbytes >= 8; */
size=(buffer[2]<<8)+buffer[3];
} while(!(buffer[1]==0xe2 &&
buffer[4]=='M' && buffer[5]=='P' && buffer[6]=='F' && buffer[7]==0));
#ifdef DEBUG_JPEG
log_info("Found at %lu\n", (long unsigned)offset);
#endif
- if(2+size > nbytes)
- size=nbytes-2;
- if(size<12)
+ if(8+size > nbytes)
+ size=nbytes-8;
+ /*@ assert 8 + size <= nbytes; */
+ if(size<16)
{
fr->file_size=0;
return ;
}
+ /*@ assert 16 <= size <= 65535; */
{
const uint64_t max_offset=check_mpo(buffer+8, offset+8, size-8);
fr->file_size=(max_offset > fr->file_size ? 0 : max_offset);
@@ -372,10 +464,83 @@ static int is_marker_valid(const unsigned int marker)
}
}
+/*@
+ @ requires \valid_read(buffer + (0 .. buffer_size-1));
+ @*/
+static time_t jpg_get_date(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int i, const unsigned int size)
+{ /* APP1 Exif information */
+ const unsigned int tiff_offset=i+2+8;
+ if(tiff_offset < buffer_size && size > 8)
+ {
+ /*@ assert tiff_offset < buffer_size; */
+ /*@ assert size > 8; */
+ unsigned int tiff_size=size-0x08;
+ if(buffer_size - tiff_offset < tiff_size)
+ {
+ tiff_size=buffer_size - tiff_offset;
+ /*@ assert tiff_offset + tiff_size == buffer_size; */
+ }
+ else
+ {
+ /*@ assert tiff_offset + tiff_size <= buffer_size; */
+ }
+ /*@ assert tiff_offset + tiff_size <= buffer_size; */
+ return get_date_from_tiff_header(&buffer[tiff_offset], tiff_size);
+ }
+ return 0;
+}
+
+
+/*@
+ @ requires buffer_size >= 10;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires file_recovery->file_stat==\null || valid_read_string((char*)&file_recovery->filename);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ requires separation: \separated(&file_hint_jpg, buffer+(..), file_recovery, file_recovery_new);
+ @ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
+ @ ensures \result == 1 ==> file_recovery_new->extension == file_hint_jpg.extension;
+ @ ensures \result == 1 ==> \initialized(&file_recovery_new->time);
+ @ ensures \result == 1 ==> file_recovery_new->calculated_file_size == 0;
+ @ ensures \result == 1 ==> file_recovery_new->file_size == 0;
+ @ ensures \result == 1 ==> file_recovery_new->min_filesize > 0;
+ @ ensures \result == 1 ==> file_recovery_new->offset_ok == 0;
+ @ ensures \result == 1 && buffer_size >= 4 ==> file_recovery_new->data_check == data_check_jpg;
+ @ ensures \result == 1 ==> file_recovery_new->file_check == file_check_jpg;
+ @ ensures \result == 1 ==> file_recovery_new->file_rename == \null;
+ @ ensures \result == 1 ==> valid_read_string(file_recovery_new->extension);
+ @*/
static int header_check_jpg(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
{
unsigned int i=2;
time_t jpg_time=0;
+ while(i+4<buffer_size && buffer[i]==0xff && is_marker_valid(buffer[i+1]))
+ {
+ const unsigned int size=(buffer[i+2]<<8)+buffer[i+3];
+ if(buffer[i+1]==0xff)
+ i++;
+ else
+ {
+ if(buffer[i+1]==0xe1)
+ { /* APP1 Exif information */
+ jpg_time=jpg_get_date(buffer, buffer_size, i, size);
+ }
+ else if(buffer[i+1]==0xc4)
+ {
+ /* DHT */
+ if(jpg_check_dht(buffer, buffer_size, i, 2+(buffer[i+2]<<8)+buffer[i+3])!=0)
+ return 0;
+ }
+ i+=2+size;
+ }
+ }
+ if(i+1 < file_recovery_new->blocksize && buffer[i+1]!=0xda)
+ return 0;
+ if(i+1 < 512 && buffer[i+1]!=0xda)
+ return 0;
if(file_recovery->file_stat!=NULL)
{
static const unsigned char jpg_header_app0_avi[0x0c]= {
@@ -388,17 +553,19 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
unsigned int width=0;
unsigned int height=0;
jpg_get_size(buffer, buffer_size, &height, &width);
+#if !defined(MAIN_jpg) && !defined(MAIN_fidentify)
if(file_recovery->file_stat->file_hint==&file_hint_indd)
{
if(header_ignored_adv(file_recovery, file_recovery_new)==0)
return 0;
}
if(file_recovery->file_stat->file_hint==&file_hint_doc &&
- strstr(file_recovery->filename, ".albm")!=NULL)
+ strstr(file_recovery->filename, ".albm")!=NULL)
{
if(header_ignored_adv(file_recovery, file_recovery_new)==0)
return 0;
}
+#endif
if( file_recovery->file_stat->file_hint==&file_hint_jpg)
{
/* Don't recover the thumb instead of the jpg itself */
@@ -432,6 +599,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
return 0;
}
}
+#if !defined(MAIN_jpg) && !defined(MAIN_fidentify)
/* Don't extract jpg inside AVI */
if( file_recovery->file_stat->file_hint==&file_hint_riff &&
(memcmp(buffer, jpg_header_app0_avi, sizeof(jpg_header_app0_avi))==0 ||
@@ -454,6 +622,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
if(header_ignored_adv(file_recovery, file_recovery_new)==0)
return 0;
}
+#endif
if(buffer[3]==0xdb) /* DQT */
{
header_ignored(file_recovery_new);
@@ -480,35 +649,6 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
return 0;
}
}
- while(i+4<buffer_size && buffer[i]==0xff && is_marker_valid(buffer[i+1]))
- {
- if(buffer[i+1]==0xff)
- i++;
- else
- {
- if(buffer[i+1]==0xe1)
- { /* APP1 Exif information */
- if(i+0x0A < buffer_size && 2+(buffer[i+2]<<8)+buffer[i+3] > 0x0A)
- {
- unsigned int tiff_size=2+(buffer[i+2]<<8)+buffer[i+3]-0x0A;
- if(buffer_size - (i+0x0A) < tiff_size)
- tiff_size=buffer_size - (i+0x0A);
- jpg_time=get_date_from_tiff_header((const TIFFHeader*)&buffer[i+0x0A], tiff_size);
- }
- }
- else if(buffer[i+1]==0xc4)
- {
- /* DHT */
- if(jpg_check_dht(buffer, buffer_size, i, 2+(buffer[i+2]<<8)+buffer[i+3])!=0)
- return 0;
- }
- i+=2+(buffer[i+2]<<8)+buffer[i+3];
- }
- }
- if(i+1 < file_recovery->blocksize && buffer[i+1]!=0xda)
- return 0;
- if(i+1 < 512 && buffer[i+1]!=0xda)
- return 0;
reset_file_recovery(file_recovery_new);
file_recovery_new->min_filesize=i;
file_recovery_new->calculated_file_size=0;
@@ -517,10 +657,11 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
file_recovery_new->file_check=&file_check_jpg;
if(buffer_size >= 4)
file_recovery_new->data_check=&data_check_jpg;
+ /*@ assert valid_read_string(file_recovery_new->extension); */
return 1;
}
-#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H)
+#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && !defined(__FRAMAC__)
struct my_error_mgr {
struct jpeg_error_mgr pub; /* "public" fields, must be the first field */
@@ -1176,7 +1317,7 @@ static uint64_t jpg_check_thumb(FILE *infile, const uint64_t offset, const unsig
if(jpeg_session.frame!=NULL && jpeg_session.flags!=0)
{
const uint64_t tmp=jpg_find_error(&jpeg_session, &offsets[0], checkpoint_offset);
-// log_info("jpg_check_thumb jpeg corrupted near %llu\n", offset_error);
+// log_info("jpg_check_thumb jpeg corrupted near %llu\n", (long long unsigned)offset_error);
if(tmp !=0 && offset_error > tmp)
offset_error=tmp;
// log_info("jpg_check_thumb find_error estimation %llu\n", (long long unsigned)offset_error);
@@ -1250,7 +1391,6 @@ static void jpg_check_picture(file_recovery_t *file_recovery)
(long long unsigned)file_recovery->offset_ok,
(long long unsigned)file_recovery->offset_error);
#endif
-#if 1
if(jpeg_session.frame!=NULL && jpeg_session.flags!=0)
{
const uint64_t offset_error=jpg_find_error(&jpeg_session, &offsets[0], file_recovery->checkpoint_offset);
@@ -1262,7 +1402,6 @@ static void jpg_check_picture(file_recovery_t *file_recovery)
(long long unsigned)file_recovery->offset_error);
#endif
}
-#endif
jpeg_session_delete(&jpeg_session);
return;
}
@@ -1328,13 +1467,19 @@ static void jpg_check_picture(file_recovery_t *file_recovery)
}
#endif
-static int jpg_check_dht(const unsigned char *buffer, const unsigned int buffer_size, const unsigned i, const unsigned int size)
+/*@
+ @ requires i < buffer_size;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ assigns \nothing;
+ @*/
+static int jpg_check_dht(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int i, const unsigned int size)
{
unsigned int j=i+4;
/* DHT must not be shorter than 18 bytes, 1+16+1 */
/* DHT should not be longer than 1088 bytes, 4*(1+16+255) */
if(size<18)
return 2;
+ /*@ loop assigns j; */
while(j < buffer_size && j < i+size)
{
const unsigned int tc=buffer[j]>>4;
@@ -1348,6 +1493,12 @@ static int jpg_check_dht(const unsigned char *buffer, const unsigned int buffer_
if(n > 3)
return 2;
j++;
+ /*@
+ @ loop invariant 0 <= l <= 16;
+ @ loop invariant sum <= l*255;
+ @ loop assigns l,sum;
+ @ loop variant 16-l;
+ @*/
for(l=0; l < 16; l++)
if(j+l < buffer_size)
sum+=buffer[j+l];
@@ -1369,299 +1520,410 @@ struct sof_header
uint16_t height; /* 0-65535 */
uint16_t width; /* 1-65535 */
unsigned char nbr; /* 1-255 */
+#if 0
unsigned char data[0];
+#endif
} __attribute__ ((gcc_struct, __packed__));
+/*@
+ @ requires \valid_read(buffer + (0..buffer_size-1));
+ @ assigns \nothing;
+ @*/
static int jpg_check_sof0(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int i)
{
- const struct sof_header *h=(const struct sof_header *)&buffer[i];
if(i+4 > buffer_size)
return 0;
- if(be16(h->length) < sizeof(struct sof_header)-2)
- return 1;
+ {
+ const struct sof_header *h=(const struct sof_header *)&buffer[i];
+ if(be16(h->length) < sizeof(struct sof_header)-2)
+ return 1;
+ }
if(i+2+8 > buffer_size)
return 0;
- if(h->precision!=8 || be16(h->width)==0 || h->nbr==0)
- return 1;
- if(be16(h->length) < 8+h->nbr*3)
- return 1;
+ {
+ const struct sof_header *h=(const struct sof_header *)&buffer[i];
+ if(h->precision!=8 || be16(h->width)==0 || h->nbr==0)
+ return 1;
+ if(be16(h->length) < 8+h->nbr*3)
+ return 1;
+ }
// if(i+2+be16(h->length) > buffer_size)
// return 0;
return 0;
}
+/*@
+ @ requires \valid_read(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires file_recovery->blocksize <= 1048576;
+ @ requires file_recovery->offset_error <= (1<<63) - 1;
+ @ ensures \valid(file_recovery->handle);
+ @*/
static void jpg_search_marker(file_recovery_t *file_recovery)
{
FILE* infile=file_recovery->handle;
unsigned char buffer[40*8192];
size_t nbytes;
+ const uint64_t offset_error=file_recovery->offset_error;
+ uint64_t offset_test=offset_error;
uint64_t offset;
- unsigned int i;
+ /*@ assert offset_test == offset_error; */
if(file_recovery->blocksize==0)
return ;
- offset=file_recovery->offset_error / file_recovery->blocksize * file_recovery->blocksize;
- i=file_recovery->offset_error % file_recovery->blocksize;
+ offset=offset_test / file_recovery->blocksize * file_recovery->blocksize;
if(my_fseek(infile, offset, SEEK_SET) < 0)
return ;
- do
+ /*@ assert offset_test == offset_error; */
+ /*@
+ @ loop invariant offset_test >= offset_error;
+ @*/
+ while((nbytes=fread(&buffer, 1, sizeof(buffer), infile))>0)
{
- while((nbytes=fread(&buffer, 1, sizeof(buffer), infile))>0)
+ unsigned int i;
+ /*@ assert 0 < nbytes <= sizeof(buffer); */
+ if(offset_test > 0x80000000)
+ return ;
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&buffer, sizeof(buffer));
+#endif
+ /*@ assert offset_test >= offset_error; */
+ offset=offset_test / file_recovery->blocksize * file_recovery->blocksize;
+ i=offset_test % file_recovery->blocksize;
+ /*@ assert offset + i == offset_test; */
+ /*@ assert i == offset_test - offset; */
+ /*@ assert offset_test >= offset_error; */
+ /*@
+ @ loop invariant offset + i >= offset_test;
+ @ loop invariant offset_test >= offset_error;
+ @ loop invariant 0 <= i < nbytes + file_recovery->blocksize;
+ @ loop assigns i,file_recovery->extra;
+ @*/
+ while(i+1<nbytes)
{
- for(;i+1<nbytes; i+=file_recovery->blocksize)
+ const uint64_t tmp=offset + i;
+ /*@ assert tmp == offset + i; */
+ /*@ assert tmp >= offset_test; */
+ /*@ assert offset_test >= offset_error; */
+ if(buffer[i]==0xff &&
+ (buffer[i+1]==0xd8 || /* SOI */
+ buffer[i+1]==0xdb || /* DQT */
+ (buffer[i+1]>=0xc0 && buffer[i+1]<=0xcf) || /* SOF0 - SOF15, 0xc4=DHT */
+ buffer[i+1]==0xda || /* SOS: Start Of Scan */
+ buffer[i+1]==0xdd || /* DRI */
+ (buffer[i+1]>=0xe0 && buffer[i+1]<=0xef) || /* APP0 - APP15 */
+ buffer[i+1]==0xfe) /* COM */
+ )
{
- if(buffer[i]==0xff &&
- (buffer[i+1]==0xd8 || /* SOI */
- buffer[i+1]==0xdb || /* DQT */
- (buffer[i+1]>=0xc0 && buffer[i+1]<=0xcf) || /* SOF0 - SOF15, 0xc4=DHT */
- buffer[i+1]==0xda || /* SOS: Start Of Scan */
- buffer[i+1]==0xdd || /* DRI */
- (buffer[i+1]>=0xe0 && buffer[i+1]<=0xef) || /* APP0 - APP15 */
- buffer[i+1]==0xfe) /* COM */
- )
+ file_recovery->extra=tmp - offset_error;
+#ifndef __FRAMAC__
+ if(file_recovery->extra % file_recovery->blocksize != 0)
{
- file_recovery->extra=offset + i - file_recovery->offset_error;
- if(file_recovery->extra % file_recovery->blocksize != 0)
- {
- log_info("jpg_search_marker %s extra=%llu\n",
- file_recovery->filename,
- (long long unsigned)file_recovery->extra);
- }
- return ;
+ log_info("jpg_search_marker %s extra=%llu\n",
+ file_recovery->filename,
+ (long long unsigned)file_recovery->extra);
}
+#endif
+ return ;
}
+ i+=file_recovery->blocksize;
}
- offset +=nbytes;
- i=i % file_recovery->blocksize;
- } while(nbytes == sizeof(buffer));
+ offset_test += nbytes;
+ }
return ;
}
-static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsigned int extract_thumb)
-{
- FILE* infile=file_recovery->handle;
- unsigned char buffer[40*8192];
- uint64_t thumb_offset=0;
- size_t nbytes;
- file_recovery->extra=0;
- if(my_fseek(infile, 0, SEEK_SET) < 0)
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires \valid(thumb_offset);
+ @ requires valid_read_string((char *)&file_recovery->filename);
+ @ requires file_recovery->blocksize > 0;
+ @ requires \valid_read(buffer + (0 .. nbytes-1));
+ @ requires \initialized(&file_recovery->time);
+ @ ensures \valid(file_recovery->handle);
+ @*/
+static int jpg_check_app1(file_recovery_t *file_recovery, const unsigned int extract_thumb, const unsigned char *buffer, const unsigned int i, const unsigned int offset, const unsigned int size, const size_t nbytes, uint64_t *thumb_offset)
+{ /* APP1 Exif information */
+ const unsigned int tiff_offset=i+2+8;
+ const unsigned char *potential_error=NULL;
+ const unsigned char *thumb_data=NULL;
+ const unsigned char *tiff;
+ unsigned int thumb_size=0;
+ unsigned int tiff_size;
+ if(tiff_offset >= nbytes || size <= 8)
+ return 1;
+ /*@ assert tiff_offset < nbytes; */
+ /*@ assert size > 8; */
+ tiff_size=size-0x08;
+ if(nbytes - tiff_offset < tiff_size)
+ {
+ tiff_size=nbytes - tiff_offset;
+ /*@ assert tiff_offset + tiff_size == nbytes; */
+ }
+ else
+ {
+ /*@ assert tiff_offset + tiff_size <= nbytes; */
+ }
+ /*@ assert tiff_offset + tiff_size <= nbytes; */
+ if(tiff_size<sizeof(TIFFHeader))
+ return 1;
+ /*@ assert tiff_size >= sizeof(TIFFHeader); */
+ /*@ assert \valid_read(buffer + (0 .. tiff_offset+tiff_size-1)); */
+ /*@ assert \valid_read((buffer + tiff_offset) + (0 .. tiff_size-1)); */
+ tiff=&buffer[tiff_offset];
+ /*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */
+ if(file_recovery->time==0)
+ {
+ /*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */
+ file_recovery->time=get_date_from_tiff_header(tiff, tiff_size);
+ }
+ *thumb_offset=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFOFFSET, &potential_error);
+ if(*thumb_offset!=0)
+ {
+ *thumb_offset+=tiff_offset;
+ thumb_data=buffer+ (*thumb_offset);
+ thumb_size=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFBYTECOUNT, &potential_error);
+ }
+ if(potential_error!=NULL)
+ {
+ file_recovery->offset_error=potential_error-buffer;
return 0;
- if((nbytes=fread(&buffer, 1, sizeof(buffer), infile))>0)
+ }
+ if(file_recovery->offset_ok<i)
+ file_recovery->offset_ok=i;
+ if(thumb_data!=0 && thumb_size!=0 && *thumb_offset < nbytes - 1)
{
- unsigned int offset;
- file_recovery->offset_error=0;
- for(offset=file_recovery->blocksize; offset < nbytes && file_recovery->offset_error==0; offset+=file_recovery->blocksize)
+ unsigned int j=*thumb_offset+2;
+ unsigned int thumb_sos_found=0;
+#ifdef DEBUG_JPEG
+ unsigned int j_old=j;
+#endif
+ if(buffer[*thumb_offset]!=0xff)
{
- if(buffer[offset]==0xff && buffer[offset+1]==0xd8 && buffer[offset+2]==0xff &&
- ((buffer[offset+3]==0xe1 && memcmp(&buffer[offset+6], "http://ns.adobe.com/xap/", 24)!=0)
- || buffer[offset+3]==0xec))
- {
- file_recovery->offset_error=offset;
- }
+ file_recovery->offset_error=*thumb_offset;
+ jpg_search_marker(file_recovery);
+ return 0;
}
- offset=2;
- while(offset + 4 < nbytes && (file_recovery->offset_error==0 || offset < file_recovery->offset_error))
+ if(buffer[*thumb_offset+1]!=0xd8)
{
- const unsigned int i=offset;
- const unsigned int size=(buffer[i+2]<<8)+buffer[i+3];
- if(buffer[i]!=0xff)
+ file_recovery->offset_error=*thumb_offset+1;
+ return 0;
+ }
+ while(j+4<nbytes && thumb_sos_found==0)
+ {
+ if(buffer[j]!=0xff)
{
+ file_recovery->offset_error=j;
#ifdef DEBUG_JPEG
- log_info("%s no marker at 0x%x\n", file_recovery->filename, i);
+ log_info("%s thumb no marker at 0x%x\n", file_recovery->filename, j);
+ log_error("%s Error between %u and %u\n", file_recovery->filename, j_old, j);
#endif
- file_recovery->offset_error=i;
jpg_search_marker(file_recovery);
- return thumb_offset;
+ return 0;
}
- if(buffer[i+1]==0xff)
+ if(buffer[j+1]==0xff)
{
/* See B.1.1.2 Markers in http://www.w3.org/Graphics/JPEG/itu-t81.pdf*/
- offset++;
+ j++;
continue;
}
#ifdef DEBUG_JPEG
- log_info("%s marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i);
+ log_info("%s thumb marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
#endif
- offset+=(uint64_t)2+size;
- if(buffer[i+1]==0xda) /* SOS: Start Of Scan */
+ if(buffer[j+1]==0xda) /* Thumb SOS: Start Of Scan */
+ thumb_sos_found=1;
+ else if(buffer[j+1]==0xc4) /* DHT */
{
- file_recovery->offset_ok=i+1;
- return thumb_offset;
- }
- else if(buffer[i+1]==0xe1)
- { /* APP1 Exif information */
-#if 1
- if(i+0x0A < nbytes && 2+size > 0x0A)
+ if(jpg_check_dht(buffer, nbytes, j, 2+(buffer[j+2]<<8)+buffer[j+3])!=0)
{
- const char *potential_error=NULL;
- const TIFFHeader *tiff=(const TIFFHeader*)&buffer[i+0x0A];
- unsigned int tiff_size=2+size-0x0A;
- const char *thumb_data=NULL;
- const char *ifbytecount=NULL;
- if(nbytes - (i+0x0A) < tiff_size)
- tiff_size=nbytes - (i+0x0A);
- if(file_recovery->time==0)
- file_recovery->time=get_date_from_tiff_header(tiff, tiff_size);
- thumb_data=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFOFFSET, &potential_error);
- if(thumb_data!=NULL)
- {
- thumb_offset=thumb_data-(const char*)buffer;
- ifbytecount=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFBYTECOUNT, &potential_error);
- }
- if(potential_error!=NULL)
- {
- file_recovery->offset_error=potential_error-(const char*)buffer;
- return 0;
- }
- if(file_recovery->offset_ok<i)
- file_recovery->offset_ok=i;
- if(thumb_data!=NULL && ifbytecount!=NULL)
- {
- const unsigned int thumb_size=ifbytecount-(const char*)tiff;
- if(thumb_offset < nbytes - 1)
- {
- unsigned int j=thumb_offset+2;
- unsigned int thumb_sos_found=0;
+ file_recovery->offset_error=j+2;
+ return 0;
+ }
+ }
+ else if(buffer[j+1]==0xdb || /* DQT */
+ buffer[j+1]==0xc0 || /* SOF0 */
+ buffer[j+1]==0xdd) /* DRI */
+ {
+ }
+ else if((buffer[j+1]>=0xc0 && buffer[j+1]<=0xcf) || /* SOF0 - SOF15 */
+ (buffer[j+1]>=0xe0 && buffer[j+1]<=0xef) || /* APP0 - APP15 */
+ buffer[j+1]==0xfe) /* COM */
+ {
+ /* Unusual marker, bug ? */
+ }
+ else
+ {
+ log_info("%s thumb unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
+ file_recovery->offset_error=j;
+ return 0;
+ }
+ if(file_recovery->offset_ok<j)
+ file_recovery->offset_ok=j;
#ifdef DEBUG_JPEG
- unsigned int j_old=j;
+ j_old=j;
#endif
- if(buffer[thumb_offset]!=0xff)
- {
- file_recovery->offset_error=thumb_offset;
- jpg_search_marker(file_recovery);
- return 0;
- }
- if(buffer[thumb_offset+1]!=0xd8)
- {
- file_recovery->offset_error=thumb_offset+1;
- return 0;
- }
- while(j+4<nbytes && thumb_sos_found==0)
- {
- if(buffer[j]!=0xff)
- {
- file_recovery->offset_error=j;
-#ifdef DEBUG_JPEG
- log_info("%s thumb no marker at 0x%x\n", file_recovery->filename, j);
- log_error("%s Error between %u and %u\n", file_recovery->filename, j_old, j);
-#endif
- jpg_search_marker(file_recovery);
- return 0;
- }
- if(buffer[j+1]==0xff)
- {
- /* See B.1.1.2 Markers in http://www.w3.org/Graphics/JPEG/itu-t81.pdf*/
- j++;
- continue;
- }
-#ifdef DEBUG_JPEG
- log_info("%s thumb marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
+ j+=2U+(buffer[j+2]<<8)+buffer[j+3];
+ }
+ if(thumb_sos_found>0 && extract_thumb>0
+ && offset < nbytes && buffer[offset]==0xff &&
+ *thumb_offset+thumb_size < nbytes)
+ {
+ char thumbname[2048];
+ char *sep;
+ /*@ assert sizeof(thumbname) == sizeof(file_recovery->filename); */
+ /*@ assert valid_read_string((char *)&file_recovery->filename); */
+ memcpy(thumbname,file_recovery->filename, sizeof(thumbname));
+ thumbname[sizeof(thumbname)-1]='\0';
+ /*@ assert valid_read_string(&thumbname[0]); */
+ sep=strrchr(thumbname,'/');
+ if(sep!=NULL
+#ifndef __FRAMAC__
+ && *(sep+1)=='f'
#endif
- if(buffer[j+1]==0xda) /* Thumb SOS: Start Of Scan */
- thumb_sos_found=1;
- else if(buffer[j+1]==0xc4) /* DHT */
- {
-#if 1
- if(jpg_check_dht(buffer, nbytes, j, 2+(buffer[j+2]<<8)+buffer[j+3])!=0)
- {
- file_recovery->offset_error=j+2;
- return 0;
- }
-#endif
- }
- else if(buffer[j+1]==0xdb || /* DQT */
- buffer[j+1]==0xc0 || /* SOF0 */
- buffer[j+1]==0xdd) /* DRI */
- {
- }
- else if((buffer[j+1]>=0xc0 && buffer[j+1]<=0xcf) || /* SOF0 - SOF15 */
- (buffer[j+1]>=0xe0 && buffer[j+1]<=0xef) || /* APP0 - APP15 */
- buffer[j+1]==0xfe) /* COM */
- {
- /* Unusual marker, bug ? */
- }
- else
- {
- log_info("%s thumb unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
- file_recovery->offset_error=j;
- return 0;
- }
- if(file_recovery->offset_ok<j)
- file_recovery->offset_ok=j;
-#ifdef DEBUG_JPEG
- j_old=j;
+ )
+ {
+ FILE *out;
+#ifndef __FRAMAC__
+ *(sep+1)='t';
#endif
- j+=2U+(buffer[j+2]<<8)+buffer[j+3];
- }
- if(thumb_sos_found>0 && extract_thumb>0
- && offset < nbytes && buffer[offset]==0xff)
- {
- char *thumbname;
- char *sep;
- thumbname=strdup(file_recovery->filename);
- sep=strrchr(thumbname,'/');
- if(sep!=NULL && *(sep+1)=='f' && thumb_offset+thumb_size < nbytes)
- {
- FILE *out;
- *(sep+1)='t';
- if((out=fopen(thumbname,"wb"))!=NULL)
- {
- if(fwrite(thumb_data, thumb_size, 1, out) < 1)
- {
- log_error("Can't write to %s: %s\n", thumbname, strerror(errno));
- }
- fclose(out);
- if(file_recovery->time!=0 && file_recovery->time!=(time_t)-1)
- set_date(thumbname, file_recovery->time, file_recovery->time);
- }
- else
- {
- log_error("fopen %s failed\n", thumbname);
- }
- }
- free(thumbname);
- }
- }
+ if((out=fopen(thumbname,"wb"))!=NULL)
+ {
+ const char *buffer_char=(const char *)buffer;
+ /*@ assert \valid_read(buffer_char + (0 .. nbytes - 1)); */
+ /*@ assert *thumb_offset + thumb_size < nbytes; */
+ /*@ assert \valid_read(buffer_char + (0 .. *thumb_offset + thumb_size - 1)); */
+ /*@ assert \valid_read(buffer_char + *thumb_offset + (0 .. thumb_size - 1)); */
+ const char *thumb_char=&buffer_char[*thumb_offset];
+ /*@ assert \valid_read(thumb_char + (0 .. thumb_size - 1)); */
+ if(fwrite(thumb_char, thumb_size, 1, out) < 1)
+ {
+ log_error("Can't write to %s: %s\n", thumbname, strerror(errno));
}
+ fclose(out);
+ if(file_recovery->time!=0 && file_recovery->time!=(time_t)-1)
+ set_date(thumbname, file_recovery->time, file_recovery->time);
}
-#endif
- }
- else if(buffer[i+1]==0xc4) /* DHT */
- {
-#if 1
- if(jpg_check_dht(buffer, nbytes, i, 2+size)!=0)
+ else
{
- file_recovery->offset_error=i+2;
- return thumb_offset;
+ log_error("fopen %s failed\n", thumbname);
}
-#endif
- if(file_recovery->offset_ok<i+1)
- file_recovery->offset_ok=i+1;
}
- else if(buffer[i+1]==0xdb || /* DQT */
- (buffer[i+1]>=0xc0 && buffer[i+1]<=0xcf) || /* SOF0 - SOF15 */
- buffer[i+1]==0xdd || /* DRI */
- (buffer[i+1]>=0xe0 && buffer[i+1]<=0xef) || /* APP0 - APP15 */
- buffer[i+1]==0xfe) /* COM */
- {
- if(file_recovery->offset_ok<i+1)
- file_recovery->offset_ok=i+1;
- }
- else
+ }
+ }
+ return 1;
+}
+
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires file_recovery->blocksize > 0;
+ @ requires \initialized(&file_recovery->time);
+ @ requires valid_read_string((char *)&file_recovery->filename);
+ */
+static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsigned int extract_thumb)
+{
+ FILE* infile=file_recovery->handle;
+ unsigned char buffer[40*8192];
+ uint64_t thumb_offset=0;
+ size_t nbytes;
+ unsigned int offset;
+ file_recovery->extra=0;
+ if(my_fseek(infile, 0, SEEK_SET) < 0)
+ return 0;
+ nbytes=fread(&buffer, 1, sizeof(buffer), infile);
+ if(nbytes <= 0)
+ return 0;
+ /*@ assert nbytes > 0; */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&buffer, sizeof(buffer));
+#endif
+ file_recovery->offset_error=0;
+ for(offset=file_recovery->blocksize; offset + 30 < nbytes && file_recovery->offset_error==0; offset+=file_recovery->blocksize)
+ {
+ if(buffer[offset]==0xff && buffer[offset+1]==0xd8 && buffer[offset+2]==0xff &&
+ ((buffer[offset+3]==0xe1 && memcmp(&buffer[offset+6], "http://ns.adobe.com/xap/", 24)!=0)
+ || buffer[offset+3]==0xec))
+ {
+ file_recovery->offset_error=offset;
+ }
+ }
+ offset=2;
+ while(offset + 4 < nbytes && (file_recovery->offset_error==0 || offset < file_recovery->offset_error))
+ {
+ const unsigned int i=offset;
+ const unsigned int size=(buffer[i+2]<<8)+buffer[i+3];
+ if(buffer[i]!=0xff)
+ {
+#if defined(DEBUG_JPEG) && !defined(__FRAMAC__)
+ log_info("%s no marker at 0x%x\n", file_recovery->filename, i);
+#endif
+ file_recovery->offset_error=i;
+ jpg_search_marker(file_recovery);
+ return thumb_offset;
+ }
+ if(buffer[i+1]==0xff)
+ {
+ /* See B.1.1.2 Markers in http://www.w3.org/Graphics/JPEG/itu-t81.pdf*/
+ offset++;
+ continue;
+ }
+#if defined(DEBUG_JPEG) && !defined(__FRAMAC__)
+ log_info("%s marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i);
+#endif
+ offset+=(uint64_t)2+size;
+ if(buffer[i+1]==0xda) /* SOS: Start Of Scan */
+ {
+ file_recovery->offset_ok=i+1;
+ return thumb_offset;
+ }
+ else if(buffer[i+1]==0xe1)
+ { /* APP1 Exif information */
+ if(jpg_check_app1(file_recovery, extract_thumb, buffer, i, offset, size, nbytes, &thumb_offset)==0)
+ return 0;
+ }
+ else if(buffer[i+1]==0xc4) /* DHT */
+ {
+ if(jpg_check_dht(buffer, nbytes, i, 2+size)!=0)
{
- log_info("%s unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i+1);
- file_recovery->offset_error=i+1;
+ file_recovery->offset_error=i+2;
return thumb_offset;
}
+ if(file_recovery->offset_ok<i+1)
+ file_recovery->offset_ok=i+1;
}
- if(offset > nbytes && nbytes < sizeof(buffer))
+ else if(buffer[i+1]==0xdb || /* DQT */
+ (buffer[i+1]>=0xc0 && buffer[i+1]<=0xcf) || /* SOF0 - SOF15 */
+ buffer[i+1]==0xdd || /* DRI */
+ (buffer[i+1]>=0xe0 && buffer[i+1]<=0xef) || /* APP0 - APP15 */
+ buffer[i+1]==0xfe) /* COM */
{
- file_recovery->offset_error=nbytes;
+ if(file_recovery->offset_ok<i+1)
+ file_recovery->offset_ok=i+1;
+ }
+ else
+ {
+#ifndef __FRAMAC__
+ log_info("%s unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i+1);
+#endif
+ file_recovery->offset_error=i+1;
return thumb_offset;
}
}
+ if(offset > nbytes && nbytes < sizeof(buffer))
+ {
+ file_recovery->offset_error=nbytes;
+ return thumb_offset;
+ }
return thumb_offset;
}
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires valid_read_string((char *)&file_recovery->filename);
+ @ requires \initialized(&file_recovery->time);
+ @ requires file_recovery->file_check == &file_check_mpo || file_recovery->file_check == &file_check_jpg;
+ @*/
static void file_check_jpg(file_recovery_t *file_recovery)
{
uint64_t thumb_offset;
@@ -1684,7 +1946,7 @@ static void file_check_jpg(file_recovery_t *file_recovery)
#ifdef DEBUG_JPEG
log_info("jpg_check_structure error at %llu\n", (long long unsigned)file_recovery->offset_error);
#endif
-#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H)
+#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && !defined(__FRAMAC__)
if(thumb_offset!=0 &&
(file_recovery->checkpoint_status==0 || thumb_error!=0) &&
(file_recovery->offset_error==0 || thumb_offset < file_recovery->offset_error))
@@ -1712,7 +1974,7 @@ static void file_check_jpg(file_recovery_t *file_recovery)
#endif
if(file_recovery->offset_error!=0)
return ;
-#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H)
+#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && ! defined(__FRAMAC__)
jpg_check_picture(file_recovery);
#else
file_recovery->file_size=file_recovery->calculated_file_size;
@@ -1731,27 +1993,39 @@ static void file_check_jpg(file_recovery_t *file_recovery)
#endif
}
+/*@
+ @ requires buffer_size >= 2 && (buffer_size&1)==0;
+ @ requires \valid(file_recovery);
+ @ requires file_recovery->calculated_file_size >= 2;
+ @ requires \valid_read(buffer + ( 0 .. buffer_size-1));
+ @ requires file_recovery->data_check == &data_check_jpg2;
+ @ ensures \result == DC_CONTINUE || \result == DC_STOP;
+ @ ensures file_recovery->data_check == &data_check_jpg2 || file_recovery->data_check == \null;
+ @ ensures file_recovery->data_check == &data_check_jpg2 ==> file_recovery->calculated_file_size >= 2;
+ @ ensures file_recovery->data_check == \null ==> file_recovery->calculated_file_size == 0;
+ @ assigns file_recovery->calculated_file_size;
+ @ assigns file_recovery->data_check;
+ @ assigns file_recovery->offset_error;
+ @*/
static data_check_t data_check_jpg2(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
-#if 0
- unsigned int old_marker=0;
-#endif
- if(file_recovery->calculated_file_size<2)
- {
- /* Reset to the correct file checker */
- file_recovery->data_check=&data_check_jpg;
- return data_check_jpg(buffer, buffer_size, file_recovery);
- }
+ /*@
+ @ loop assigns file_recovery->calculated_file_size;
+ @ loop assigns file_recovery->data_check;
+ @ loop assigns file_recovery->offset_error;
+ @*/
while(file_recovery->calculated_file_size + buffer_size/2 > file_recovery->file_size &&
file_recovery->calculated_file_size < file_recovery->file_size + buffer_size/2)
{
- const unsigned int i=file_recovery->calculated_file_size - file_recovery->file_size + buffer_size/2;
+ const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size;
+ /*@ assert file_recovery->data_check == &data_check_jpg2; */
if(buffer[i-1]==0xFF)
{
if(buffer[i]==0xd9)
{
/* JPEG_EOI */
file_recovery->calculated_file_size++;
+ /*@ assert file_recovery->data_check == &data_check_jpg2; */
return DC_STOP;
}
else if(buffer[i] >= 0xd0 && buffer[i] <= 0xd7)
@@ -1770,6 +2044,7 @@ static data_check_t data_check_jpg2(const unsigned char *buffer, const unsigned
/* TODO: store old_marker in file_recovery */
old_marker=buffer[i];
#endif
+ /*@ assert file_recovery->data_check == &data_check_jpg2; */
}
else if(buffer[i] == 0xda || buffer[i] == 0xc4)
{
@@ -1785,29 +2060,59 @@ static data_check_t data_check_jpg2(const unsigned char *buffer, const unsigned
(long long unsigned)file_recovery->calculated_file_size);
#endif
file_recovery->offset_error=file_recovery->calculated_file_size;
+ /*@ assert file_recovery->data_check == &data_check_jpg2; */
return DC_STOP;
}
}
+ /*@ assert file_recovery->data_check == &data_check_jpg2; */
file_recovery->calculated_file_size++;
}
return DC_CONTINUE;
}
-data_check_t data_check_jpg(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
+/*@
+ @ requires buffer_size >= 8;
+ @ requires (buffer_size&1)==0;
+ @ requires \valid(file_recovery);
+ @ requires buffer_size >= 4;
+ @ requires \valid_read(buffer + ( 0 .. buffer_size-1));
+ @ requires file_recovery->data_check == &data_check_jpg;
+ @ ensures \result == DC_CONTINUE || \result == DC_STOP;
+ @ ensures file_recovery->data_check == &data_check_jpg2 || file_recovery->data_check == &data_check_jpg || file_recovery->data_check == &data_check_size || file_recovery->data_check == \null;
+ @ ensures file_recovery->data_check == &data_check_jpg2 ==> file_recovery->calculated_file_size >= 2;
+ @ assigns file_recovery->calculated_file_size;
+ @ assigns file_recovery->data_check;
+ @ assigns file_recovery->file_check;
+ @ assigns file_recovery->offset_error;
+ @*/
+/* FIXME requires file_recovery->file_size == 0 || file_recovery->calculated_file_size >= file_recovery->file_size - 4; */
+/* FIXME ensures \result == DC_CONTINUE ==> (file_recovery->calculated_file_size >= file_recovery->file_size + buffer_size/2 - 4); */
+static data_check_t data_check_jpg(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
/* Skip the SOI */
- if(file_recovery->calculated_file_size==0)
- file_recovery->calculated_file_size+=2;
+ if(file_recovery->calculated_file_size<2)
+ file_recovery->calculated_file_size=2;
+ /*@ assert file_recovery->calculated_file_size >= 2; */
+ /*@ assert file_recovery->data_check == &data_check_jpg; */
/* Search SOS */
+ /*@
+ @ loop assigns file_recovery->calculated_file_size;
+ @ loop assigns file_recovery->data_check;
+ @ loop assigns file_recovery->file_check;
+ @ loop assigns file_recovery->offset_error;
+ @*/
while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size &&
file_recovery->calculated_file_size + 4 < file_recovery->file_size + buffer_size/2)
{
- const unsigned int i=file_recovery->calculated_file_size - file_recovery->file_size + buffer_size/2;
+ /*@ assert file_recovery->data_check == &data_check_jpg; */
+ const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size;
+ /*@ assert 0 <= i < buffer_size - 4 ; */
if(buffer[i]==0xFF && buffer[i+1]==0xFF)
file_recovery->calculated_file_size++;
else if(buffer[i]==0xFF)
{
const unsigned int size=(buffer[i+2]<<8)+buffer[i+3];
+ const uint64_t old_calculated_file_size=file_recovery->calculated_file_size;
#ifdef DEBUG_JPEG
log_info("data_check_jpg %02x%02x at %llu, next expected at %llu\n", buffer[i], buffer[i+1],
(long long unsigned)file_recovery->calculated_file_size,
@@ -1817,44 +2122,87 @@ data_check_t data_check_jpg(const unsigned char *buffer, const unsigned int buff
if(buffer[i+1]==0xc0) /* SOF0 */
{
if(jpg_check_sof0(buffer, buffer_size, i)!=0)
+ {
+ /*@ assert file_recovery->data_check == &data_check_jpg; */
return DC_STOP;
+ }
}
else if(buffer[i+1]==0xc4) /* DHT */
{
if(jpg_check_dht(buffer, buffer_size, i, 2+size)!=0)
+ {
+ /*@ assert file_recovery->data_check == &data_check_jpg; */
return DC_STOP;
+ }
}
else if(buffer[i+1]==0xda) /* SOS: Start Of Scan */
{
+ data_check_t tmp;
file_recovery->data_check=&data_check_jpg2;
- return data_check_jpg2(buffer, buffer_size, file_recovery);
+ /*@ assert file_recovery->calculated_file_size >= 2; */
+ tmp=data_check_jpg2(buffer, buffer_size, file_recovery);
+ /*@ assert file_recovery->data_check == &data_check_jpg2 || file_recovery->data_check == \null; */
+ /*@ assert file_recovery->data_check == &data_check_jpg2 ==> file_recovery->calculated_file_size >= 2; */
+ return tmp;
}
else if(buffer[i+1]==0xe2) /* APP2 Exif information */
{
if(i+8 < buffer_size &&
buffer[i+4]=='M' && buffer[i+5]=='P' && buffer[i+6]=='F' && buffer[i+7]==0)
{
- unsigned int size_test=size;
- if(i + 2 + size >= buffer_size)
- {
- size_test=buffer_size-i-2;
- }
+ const uint64_t offset=old_calculated_file_size+8;
if(i>=buffer_size/2)
{
- file_recovery->calculated_file_size-=2+size;
+ /* Restore previous value */
+ file_recovery->calculated_file_size=old_calculated_file_size;
+ /*@ assert file_recovery->data_check == &data_check_jpg; */
return DC_CONTINUE;
}
- if(size>12)
+ /*@ assert 0 <= i < buffer_size / 2 ; */
+ if( i + size <= buffer_size)
{
- const uint64_t offset=file_recovery->calculated_file_size-(2+size)+8;
- const uint64_t calculated_file_size=check_mpo(buffer+i+8, offset, size_test-8);
- if(calculated_file_size > 0)
+ /*@ assert i + size <= buffer_size; */
+ /*@ assert size <= buffer_size - i; */
+ if(size >= 16)
{
- /* Multi-picture format */
- file_recovery->calculated_file_size=calculated_file_size;
- file_recovery->data_check=&data_check_size;
- file_recovery->file_check=&file_check_mpo;
- return DC_CONTINUE;
+ /*@ assert 16 <= size <= 65535; */
+ /*@ assert \valid_read(buffer + (0 .. buffer_size-1)); */
+ /*@ assert \valid_read(buffer + (0 .. i+size-1)); */
+ /*@ assert \valid_read((buffer + i ) + (0 .. size-1)); */
+ /*@ assert \valid_read((buffer + i + 8) + (0 .. size-8-1)); */
+ const unsigned char *mpo=buffer + i + 8;
+ const unsigned int size_mpo=size-8;
+ /*@ assert \valid_read(mpo + (0 .. size-8-1)); */
+ /*@ assert \valid_read(mpo + (0 .. size_mpo-1)); */
+ const uint64_t calculated_file_size=check_mpo(mpo, offset, size_mpo);
+ if(calculated_file_size > 0)
+ {
+ /* Multi-picture format */
+ file_recovery->calculated_file_size=calculated_file_size;
+ file_recovery->data_check=&data_check_size;
+ file_recovery->file_check=&file_check_mpo;
+ /*@ assert file_recovery->data_check == &data_check_size; */
+ return DC_CONTINUE;
+ }
+ }
+ }
+ else
+ {
+ const unsigned int size_test=buffer_size-i;
+ /*@ assert size_test == buffer_size - i; */
+ if(size_test >= 16)
+ {
+ /*@ assert 16 <= size_test; */
+ const uint64_t calculated_file_size=check_mpo(buffer+i+8, offset, size_test-8);
+ if(calculated_file_size > 0)
+ {
+ /* Multi-picture format */
+ file_recovery->calculated_file_size=calculated_file_size;
+ file_recovery->data_check=&data_check_size;
+ file_recovery->file_check=&file_check_mpo;
+ /*@ assert file_recovery->data_check == &data_check_size; */
+ return DC_CONTINUE;
+ }
}
}
}
@@ -1866,9 +2214,13 @@ data_check_t data_check_jpg(const unsigned char *buffer, const unsigned int buff
log_info("data_check_jpg %02x at %llu\n", buffer[i],
(long long unsigned)file_recovery->calculated_file_size);
#endif
+ /*@ assert file_recovery->data_check == &data_check_jpg; */
return DC_STOP;
}
}
+ /*@ assert file_recovery->data_check == &data_check_jpg; */
+ /*@ assert file_recovery->calculated_file_size < file_recovery->file_size - buffer_size/2 || file_recovery->calculated_file_size >= file_recovery->file_size + buffer_size/2 - 4; */
+ /*X TODO assert file_recovery->calculated_file_size >= file_recovery->file_size + buffer_size/2 - 4; */
return DC_CONTINUE;
}
@@ -1892,3 +2244,137 @@ const char*td_jpeg_version(void)
return "none";
#endif
}
+
+
+/*@
+ @ requires \valid(file_stat);
+ @*/
+static void register_header_check_jpg(file_stat_t *file_stat)
+{
+ static const unsigned char jpg_header[3]= { 0xff,0xd8,0xff};
+ register_header_check(0, jpg_header, sizeof(jpg_header), &header_check_jpg, file_stat);
+}
+
+#if defined(MAIN_jpg)
+#define BLOCKSIZE 65536u
+int main()
+{
+ const char fn[] = "recup_dir.1/f0000000.jpg";
+ unsigned char buffer[BLOCKSIZE];
+ file_recovery_t file_recovery_new;
+ file_recovery_t file_recovery;
+ file_stat_t file_stats;
+
+ /*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+
+ reset_file_recovery(&file_recovery);
+ file_recovery.blocksize=BLOCKSIZE;
+ file_recovery_new.blocksize=BLOCKSIZE;
+ file_recovery_new.data_check=NULL;
+ file_recovery_new.file_stat=NULL;
+ file_recovery_new.file_check=NULL;
+ file_recovery_new.file_rename=NULL;
+ file_recovery_new.calculated_file_size=0;
+ file_recovery_new.file_size=0;
+ file_recovery_new.offset_ok=0;
+ file_recovery_new.checkpoint_status=0;
+ file_recovery_new.location.start=0;
+ file_recovery_new.offset_error=0;
+ file_recovery_new.time=0;
+
+ file_stats.file_hint=&file_hint_jpg;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ register_header_check_jpg(&file_stats);
+ if(header_check_jpg(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert file_recovery_new.file_check == file_check_jpg; */
+ /*@ assert file_recovery_new.extension == file_hint_jpg.extension; */
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.offset_ok == 0; */
+ /*@ assert valid_read_string((char *)&fn); */
+ /*@ assert \initialized(&file_recovery_new.time); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ /*@ assert valid_read_string((char *)&file_recovery_new.filename); */
+ /*@ assert file_recovery_new.offset_ok == 0; */
+ file_recovery_new.file_stat=&file_stats;
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_jpg; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ res_data_check=data_check_jpg(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ /*@ assert file_recovery_new.data_check == &data_check_jpg2 ==> file_recovery_new.calculated_file_size >= 2; */
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ /*@ assert file_recovery_new.data_check == &data_check_jpg || file_recovery_new.data_check == &data_check_jpg2 || file_recovery_new.data_check == &data_check_size || file_recovery_new.data_check == NULL; */
+ if(file_recovery_new.data_check == &data_check_jpg)
+ res_data_check=data_check_jpg(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ else if(file_recovery_new.data_check == &data_check_jpg2)
+ res_data_check=data_check_jpg2(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ else if(file_recovery_new.data_check == &data_check_size)
+ res_data_check=data_check_size(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ /*@ assert file_recovery_new.data_check == &data_check_jpg || file_recovery_new.data_check == &data_check_jpg2 || file_recovery_new.data_check == &data_check_size || file_recovery_new.data_check == NULL; */
+ if(file_recovery_new.data_check == &data_check_jpg)
+ res_data_check=data_check_jpg(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ else if(file_recovery_new.data_check == &data_check_jpg2)
+ res_data_check=data_check_jpg2(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ else if(file_recovery_new.data_check == &data_check_size)
+ res_data_check=data_check_size(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ }
+ }
+ }
+ /*@ assert file_recovery_new.offset_ok == 0; */
+ {
+ file_recovery_t file_recovery_new2;
+ /* Test when another file of the same is detected in the next block */
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+ header_check_jpg(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert file_recovery_new.offset_ok == 0; */
+ /*@ assert file_recovery_new.file_check == file_check_jpg || file_recovery_new.file_check == file_check_mpo; */
+ if(file_recovery_new.file_check == file_check_jpg)
+ {
+ file_recovery_new.handle=fopen(fn, "rb");
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_jpg(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ }
+ else
+ {
+ /*@ assert file_recovery_new.file_check == file_check_mpo; */
+ file_recovery_new.handle=fopen(fn, "rb");
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_mpo(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ }
+ return 0;
+}
+#endif