src/file_wim.c: rewrite header_check_wim(), add Frama-C annotations
This commit is contained in:
Christophe Grenier
parent
1655c91cc9
commit
6d4908eb2f
1 changed files with 93 additions and 47 deletions
140
src/file_wim.c
140
src/file_wim.c
|
|
@ -33,76 +33,122 @@
|
|||
#include "common.h"
|
||||
#include "log.h"
|
||||
|
||||
/*@ requires \valid(file_stat); */
|
||||
static void register_header_check_wim(file_stat_t *file_stat);
|
||||
/* http://go.microsoft.com/fwlink/?LinkId=92227 */
|
||||
|
||||
const file_hint_t file_hint_wim= {
|
||||
.extension="wim",
|
||||
.description="Windows imaging (WIM) image",
|
||||
.max_filesize=PHOTOREC_MAX_FILE_SIZE,
|
||||
.recover=1,
|
||||
.enable_by_default=1,
|
||||
.register_header_check=®ister_header_check_wim
|
||||
const file_hint_t file_hint_wim = {
|
||||
.extension = "wim",
|
||||
.description = "Windows imaging (WIM) image",
|
||||
.max_filesize = PHOTOREC_MAX_FILE_SIZE,
|
||||
.recover = 1,
|
||||
.enable_by_default = 1,
|
||||
.register_header_check = ®ister_header_check_wim
|
||||
};
|
||||
|
||||
struct reshdr_disk_short
|
||||
{
|
||||
union {
|
||||
uint64_t flags; /* one byte is a combination of RESHDR_FLAG_XXX */
|
||||
uint64_t size; /* the 7 low-bytes are used to store the size */
|
||||
union
|
||||
{
|
||||
uint64_t flags; /* one byte is a combination of RESHDR_FLAG_XXX */
|
||||
uint64_t size; /* the 7 low-bytes are used to store the size */
|
||||
};
|
||||
uint64_t offset;
|
||||
uint64_t original_size;
|
||||
} __attribute__ ((gcc_struct, __packed__));
|
||||
} __attribute__((gcc_struct, __packed__));
|
||||
|
||||
#define RESHDR_GET_SIZE(R) (le64(R.size) & 0x00FFFFFFFFFFFFFF)
|
||||
|
||||
struct _WIMHEADER_V1_PACKED
|
||||
{
|
||||
char ImageTag[8];
|
||||
uint32_t cbSize;
|
||||
uint32_t dwVersion;
|
||||
uint32_t dwFlags;
|
||||
uint32_t dwCompressionSize;
|
||||
unsigned char gWIMGuid[16];
|
||||
uint16_t usPartNumber;
|
||||
uint16_t usTotalParts;
|
||||
uint32_t dwImageCount;
|
||||
struct reshdr_disk_short rhOffsetTable;
|
||||
struct reshdr_disk_short rhXmlData;
|
||||
struct reshdr_disk_short rhBootMetadata;
|
||||
uint32_t dwBootIndex;
|
||||
struct reshdr_disk_short rhIntegrity;
|
||||
unsigned char bUnused[60];
|
||||
} __attribute__ ((gcc_struct, __packed__));
|
||||
char ImageTag[8];
|
||||
uint32_t cbSize;
|
||||
uint32_t dwVersion;
|
||||
uint32_t dwFlags;
|
||||
uint32_t dwCompressionSize;
|
||||
unsigned char gWIMGuid[16];
|
||||
uint16_t usPartNumber;
|
||||
uint16_t usTotalParts;
|
||||
uint32_t dwImageCount;
|
||||
struct reshdr_disk_short rhOffsetTable;
|
||||
struct reshdr_disk_short rhXmlData;
|
||||
struct reshdr_disk_short rhBootMetadata;
|
||||
uint32_t dwBootIndex;
|
||||
struct reshdr_disk_short rhIntegrity;
|
||||
unsigned char bUnused[60];
|
||||
} __attribute__((gcc_struct, __packed__));
|
||||
|
||||
/*@
|
||||
@ requires size <= 0x00FFFFFFFFFFFFFF;
|
||||
@ assigns \nothing;
|
||||
@*/
|
||||
static uint64_t wim_max(const uint64_t offset, const uint64_t size, const uint64_t max_size)
|
||||
{
|
||||
uint64_t tmp;
|
||||
if(size == 0)
|
||||
return max_size;
|
||||
if(offset > PHOTOREC_MAX_FILE_SIZE)
|
||||
return 0;
|
||||
tmp = offset + size;
|
||||
if(tmp > max_size)
|
||||
return tmp;
|
||||
return max_size;
|
||||
}
|
||||
|
||||
/*@
|
||||
@ requires buffer_size > sizeof(struct _WIMHEADER_V1_PACKED);
|
||||
@ requires \valid_read(buffer+(0..buffer_size-1));
|
||||
@ requires valid_file_recovery(file_recovery);
|
||||
@ requires \valid(file_recovery_new);
|
||||
@ requires file_recovery_new->blocksize > 0;
|
||||
@ requires separation: \separated(&file_hint_wim, buffer+(..), file_recovery, file_recovery_new);
|
||||
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
|
||||
@ assigns *file_recovery_new;
|
||||
@*/
|
||||
static int header_check_wim(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)
|
||||
{
|
||||
const struct _WIMHEADER_V1_PACKED *hdr=(const struct _WIMHEADER_V1_PACKED *)buffer;
|
||||
uint64_t size=le32(hdr->cbSize);
|
||||
if(le32(hdr->cbSize) < sizeof(struct _WIMHEADER_V1_PACKED))
|
||||
const struct _WIMHEADER_V1_PACKED *hdr = (const struct _WIMHEADER_V1_PACKED *)buffer;
|
||||
uint64_t size = le32(hdr->cbSize);
|
||||
const uint64_t rhOffsetTable_s = RESHDR_GET_SIZE(hdr->rhOffsetTable);
|
||||
/*@ assert rhOffsetTable_s <= 0x00FFFFFFFFFFFFFF; */
|
||||
const uint64_t rhOffsetTable_o = le64(hdr->rhOffsetTable.offset);
|
||||
const uint64_t rhXmlData_s = RESHDR_GET_SIZE(hdr->rhXmlData);
|
||||
/*@ assert rhXmlData_s <= 0x00FFFFFFFFFFFFFF; */
|
||||
const uint64_t rhXmlData_o = le64(hdr->rhXmlData.offset);
|
||||
const uint64_t rhBootMetadata_s = RESHDR_GET_SIZE(hdr->rhBootMetadata);
|
||||
/*@ assert rhBootMetadata_s <= 0x00FFFFFFFFFFFFFF; */
|
||||
const uint64_t rhBootMetadata_o = le64(hdr->rhBootMetadata.offset);
|
||||
const uint64_t rhIntegrity_s = RESHDR_GET_SIZE(hdr->rhIntegrity);
|
||||
/*@ assert rhIntegrity_s <= 0x00FFFFFFFFFFFFFF; */
|
||||
const uint64_t rhIntegrity_o = le64(hdr->rhIntegrity.offset);
|
||||
|
||||
if(size < sizeof(struct _WIMHEADER_V1_PACKED))
|
||||
return 0;
|
||||
#ifdef DEBUG_WIM
|
||||
log_info("cbSize %llu\n", (unsigned long long)le32(hdr->cbSize));
|
||||
log_info("cbSize %llu\n", (unsigned long long)size);
|
||||
log_info("dwCompressionSize %llu\n", (unsigned long long)le32(hdr->dwCompressionSize));
|
||||
log_info("rhOffsetTable %llu %llu\n", (unsigned long long)RESHDR_GET_SIZE(hdr->rhOffsetTable), (unsigned long long)le64(hdr->rhOffsetTable.offset));
|
||||
log_info("rhXmlData %llu %llu\n", (unsigned long long)RESHDR_GET_SIZE(hdr->rhXmlData), (unsigned long long)le64(hdr->rhXmlData.offset));
|
||||
log_info("rhBootMetadata %llu %llu\n", (unsigned long long)RESHDR_GET_SIZE(hdr->rhBootMetadata), (unsigned long long)le64(hdr->rhBootMetadata.offset));
|
||||
log_info("rhIntegrity %llu %llu\n", (unsigned long long)RESHDR_GET_SIZE(hdr->rhIntegrity), (unsigned long long)le64(hdr->rhIntegrity.offset));
|
||||
log_info("rhOffsetTable %llu %llu\n", (unsigned long long)rhOffsetTable_s, (unsigned long long)rhOffsetTable_o);
|
||||
log_info("rhXmlData %llu %llu\n", (unsigned long long)rhXmlData_s, (unsigned long long)rhXmlData_o);
|
||||
log_info("rhBootMetadata %llu %llu\n", (unsigned long long)rhBootMetadata_s, (unsigned long long)rhBootMetadata_o);
|
||||
log_info("rhIntegrity %llu %llu\n", (unsigned long long)rhIntegrity_s, (unsigned long long)rhIntegrity_o);
|
||||
#endif
|
||||
if(RESHDR_GET_SIZE(hdr->rhOffsetTable) > 0 && RESHDR_GET_SIZE(hdr->rhOffsetTable) + le64(hdr->rhOffsetTable.offset) > size)
|
||||
size=RESHDR_GET_SIZE(hdr->rhOffsetTable) + le64(hdr->rhOffsetTable.offset);
|
||||
if(RESHDR_GET_SIZE(hdr->rhXmlData) > 0 && RESHDR_GET_SIZE(hdr->rhXmlData) + le64(hdr->rhXmlData.offset) > size)
|
||||
size=RESHDR_GET_SIZE(hdr->rhXmlData) + le64(hdr->rhXmlData.offset);
|
||||
if(RESHDR_GET_SIZE(hdr->rhBootMetadata) > 0 && RESHDR_GET_SIZE(hdr->rhBootMetadata) + le64(hdr->rhBootMetadata.offset) > size)
|
||||
size=RESHDR_GET_SIZE(hdr->rhBootMetadata) + le64(hdr->rhBootMetadata.offset);
|
||||
if(RESHDR_GET_SIZE(hdr->rhIntegrity) > 0 && RESHDR_GET_SIZE(hdr->rhIntegrity) + le64(hdr->rhIntegrity.offset) > size)
|
||||
size=RESHDR_GET_SIZE(hdr->rhIntegrity) + le64(hdr->rhIntegrity.offset);
|
||||
size = wim_max(rhOffsetTable_o, rhOffsetTable_s, size);
|
||||
if(size == 0)
|
||||
return 0;
|
||||
size = wim_max(rhXmlData_o, rhXmlData_s, size);
|
||||
if(size == 0)
|
||||
return 0;
|
||||
size = wim_max(rhBootMetadata_o, rhBootMetadata_s, size);
|
||||
if(size == 0)
|
||||
return 0;
|
||||
size = wim_max(rhIntegrity_o, rhIntegrity_s, size);
|
||||
if(size == 0)
|
||||
return 0;
|
||||
reset_file_recovery(file_recovery_new);
|
||||
file_recovery_new->extension=file_hint_wim.extension;
|
||||
file_recovery_new->calculated_file_size=size;
|
||||
file_recovery_new->data_check=&data_check_size;
|
||||
file_recovery_new->file_check=&file_check_size;
|
||||
file_recovery_new->extension = file_hint_wim.extension;
|
||||
file_recovery_new->calculated_file_size = size;
|
||||
file_recovery_new->data_check = &data_check_size;
|
||||
file_recovery_new->file_check = &file_check_size;
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue