From e1124cc355a9e42b0195e81f3fc4bf25013fae0b Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Mon, 22 Feb 2021 20:41:15 +0100 Subject: [PATCH] src/hfsp_struct.h: move struct from src/hfsp.h src/file_hfsp.c: add frama-c annotations --- src/Makefile.am | 4 +- src/file_hfsp.c | 16 ++++- src/hfsp.h | 149 ++++++++------------------------------------ src/hfsp_struct.h | 153 ++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 194 insertions(+), 128 deletions(-) create mode 100644 src/hfsp_struct.h diff --git a/src/Makefile.am b/src/Makefile.am index 8e1c666b..20e8d923 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -42,7 +42,7 @@ base_C = $(smallbase_C) autoset.c ewf.c fnctdsk.c hdaccess.c hdcache.c hdwin32 base_H = $(smallbase_H) alignio.h autoset.h ewf.h fnctdsk.h hdaccess.h hdwin32.h hidden.h guid_cmp.h guid_cpy.h hdcache.h hpa_dco.h intrf.h iso.h iso9660.h lang.h list.h list_sort.h log_part.h types.h io_redir.h msdos.h ntfs_utl.h parti386.h partgpt.h parthumax.h partmac.h partsun.h partxbox.h partauto.h sudo.h unicode.h win32.h fs_C = analyse.c bfs.c bsd.c btrfs.c cramfs.c exfat.c ext2.c fat.c fatx.c f2fs.c jfs.c gfs2.c hfs.c hfsp.c hpfs.c luks.c lvm.c md.c netware.c ntfs.c refs.c rfs.c savehdr.c sun.c swap.c sysv.c ufs.c vmfs.c wbfs.c xfs.c zfs.c -fs_H = analyse.h bfs.h bsd.h btrfs.h cramfs.h exfat.h ext2.h fat.h fatx.h f2fs.h f2fs_fs.h jfs_superblock.h jfs.h gfs2.h hfs.h hfsp.h hpfs.h luks.h lvm.h md.h netware.h ntfs.h ntfs_struct.h refs.h rfs.h savehdr.h sun.h swap.h sysv.h ufs.h vmfs.h wbfs.h xfs.h zfs.h +fs_H = analyse.h bfs.h bsd.h btrfs.h cramfs.h exfat.h ext2.h fat.h fatx.h f2fs.h f2fs_fs.h jfs_superblock.h jfs.h gfs2.h hfs.h hfsp.h hpfs.h hfsp_struct.h luks.h lvm.h md.h netware.h ntfs.h ntfs_struct.h refs.h rfs.h savehdr.h sun.h swap.h sysv.h ufs.h vmfs.h wbfs.h xfs.h zfs.h testdisk_ncurses_C = addpart.c addpartn.c adv.c askloc.c chgarch.c chgarchn.c chgtype.c chgtypen.c dimage.c dirn.c dirpart.c diskacc.c diskcapa.c edit.c ext2_sb.c ext2_sbn.c fat1x.c fat32.c fat_adv.c fat_cluster.c fatn.c geometry.c geometryn.c godmode.c hiddenn.c intrface.c intrfn.c nodisk.c ntfs_adv.c ntfs_fix.c ntfs_udl.c parti386n.c partgptn.c partmacn.c partsunn.c partxboxn.c tanalyse.c tbanner.c tdelete.c tdiskop.c tdisksel.c testdisk.c texfat.c thfs.c tload.c tlog.c tmbrcode.c tntfs.c toptions.c tpartwr.c testdisk_ncurses_H = addpart.h addpartn.h adv.h askloc.h chgarch.h chgarchn.h chgtype.h chgtypen.h dimage.h dirn.h dirpart.h diskacc.h diskcapa.h edit.h ext2_sb.h ext2_sbn.h fat1x.h fat32.h fat_adv.h fat_cluster.h fatn.h geometry.h geometryn.h godmode.h hiddenn.h intrface.h intrfn.h nodisk.h ntfs_adv.h ntfs_fix.h ntfs_udl.h partgptn.h parti386n.h partmacn.h partsunn.h partxboxn.h tanalyse.h tdelete.h tdiskop.h tdisksel.h texfat.h thfs.h tload.h tlog.h tmbrcode.h tntfs.h toptions.h tpartwr.h @@ -389,7 +389,7 @@ file_C = filegen.c \ file_zip.c \ file_zpr.c -file_H = ext2.h filegen.h file_doc.h file_jpg.h file_gz.h file_sp3.h file_tar.h file_tiff.h file_txt.h ole.h pe.h suspend.h +file_H = ext2.h hfsp_struct.h filegen.h file_doc.h file_jpg.h file_gz.h file_sp3.h file_tar.h file_tiff.h file_txt.h ntfs_struct.h ole.h pe.h suspend.h photorec_C = photorec.c phcfg.c addpart.c chgarch.c chgtype.c dir.c exfatp.c ext2grp.c ext2_dir.c ext2p.c fat_dir.c fatp.c file_found.c geometry.c ntfs_dir.c ntfsp.c pdisksel.c poptions.c sessionp.c dfxml.c partgptro.c diff --git a/src/file_hfsp.c b/src/file_hfsp.c index 0f7fc407..3c1ee35a 100644 --- a/src/file_hfsp.c +++ b/src/file_hfsp.c @@ -31,8 +31,9 @@ #include "types.h" #include "filegen.h" #include "common.h" -#include "hfsp.h" +#include "hfsp_struct.h" +/*@ requires \valid(file_stat); */ static void register_header_check_hfsp(file_stat_t *file_stat); const file_hint_t file_hint_hfsp= { @@ -44,6 +45,17 @@ const file_hint_t file_hint_hfsp= { .register_header_check=®ister_header_check_hfsp }; +/*@ + @ requires buffer_size >= sizeof(struct hfsp_vh); + @ 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_hfsp, buffer+(..), file_recovery, file_recovery_new); + @ ensures \result == 0 || \result == 1; + @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @ assigns *file_recovery_new; + @*/ static int header_check_hfsp(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 hfsp_vh *vh=(const struct hfsp_vh *)buffer; @@ -57,7 +69,9 @@ reset_file_recovery(file_recovery_new); static void register_header_check_hfsp(file_stat_t *file_stat) { register_header_check(0, "H+\0\4", 4, &header_check_hfsp, file_stat); +#ifndef __FRAMAC__ register_header_check(0, "HX\0\5", 4, &header_check_hfsp, file_stat); +#endif } #endif diff --git a/src/hfsp.h b/src/hfsp.h index f6e4b074..a961904b 100644 --- a/src/hfsp.h +++ b/src/hfsp.h @@ -1,12 +1,7 @@ /* File: hfsp.h, TestDisk - Copyright (C) 2005-2006 Christophe GRENIER - Original header comes from libhfs - library for reading and writing - Macintosh HFS volumes - Copyright (C) 2000 Klaus Halfmann - Original work by 1996-1998 Robert Leslie - other work 2000 from Brad Boyer (flar@pants.nu) + Copyright (C) 2005-2021 Christophe GRENIER This software is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -28,128 +23,32 @@ #ifdef __cplusplus extern "C" { #endif +#include "hfsp_struct.h" -#define HFSP_BOOT_SECTOR_SIZE 512 -#define HFSP_BLOCKSZ 512 /* A sector for Apple is always 512 bytes */ -#define HFSP_BLOCKSZ_BITS 9 /* 1<<9 == 512 */ -#define HFSP_VOLHEAD_SIG 0x482B /* 'H+' */ -#define HFSX_VOLHEAD_SIG 0x4858 /* 'HX' */ +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid(partition); + @ requires \separated(disk_car, partition); + @*/ +int check_HFSP(disk_t *disk_car, partition_t *partition, const int verbose); -#define HFSP_VERSION 4 -#define HFSX_VERSION 5 - -// Minimum Key size for all btrees -#define HFSP_CAT_KEY_MIN_LEN 6 - -// Maximum Key size for all btrees -#define HFSP_CAT_KEY_MAX_LEN 516 - -/* HFS+ includes POSIX permissions , although marked as reserved they will be - * used as such. Is ignored by MacOS 8-9 but probably not by MacOS X. - */ -typedef struct { - uint32_t owner; - uint32_t group; - uint32_t mode; - uint32_t dev; -} hfsp_perm; - -/* A single contiguous area (fragment) of a file */ -typedef struct { - uint32_t start_block; - uint32_t block_count; -} hfsp_extent; - -/* A file may contain up to 8 normale extents, all other - are found in some extra extent area */ -typedef hfsp_extent hfsp_extent_rec[8]; - -/* Information for a "Fork" in a file - * Forks are the "usual" DATA and RSRC forks or special files - * (e.g. the Volume Bitmap) - */ -typedef struct { - uint64_t total_size; // logical size - uint32_t clump_size; // number of bytes to preallocate - uint32_t total_blocks; - hfsp_extent_rec extents; // initial (8) extents -} hfsp_fork_raw; - -/* HFS+ Volume Header - * Always found at block 2 of the disk, a copy is stored - * at the second to last block of the disk. - */ -typedef struct hfsp_vh { - uint16_t signature; // 00: must be HFSPLUS_VOLHEAD_SIG 'H+' - uint16_t version; // 02: 4 for HFS+, 5 for HFSX - uint32_t attributes; // 04: See bit constants below - uint32_t last_mount_vers; // 08 - // Use a registered creator code here (See libhfsp.h) - // Mac OS uses '8.10' well - uint32_t reserved; // 0C - - uint32_t create_date; // 10 local time ! - uint32_t modify_date; // 14 GMT (?) - uint32_t backup_date; // 18 GMT (?) - uint32_t checked_date; // 1C GMT (?) fsck ? - - uint32_t file_count; // 20 - // not including special files but including DATA and RSRC forks - uint32_t folder_count; // 24 excluding the root folder - - uint32_t blocksize; // 28 - // must be multiple of HFSPLUS_SECTOR_SIZE, - // should be a multiple of 4k for harddisk - uint32_t total_blocks; // 2C - uint32_t free_blocks; // 30 - // The total number of unused allocation blocks on the disk. - - uint32_t next_alloc; - // hint where to search for next allocation blocks - uint32_t rsrc_clump_sz; - // default clump size for rsrc forks - uint32_t data_clump_sz; - // default clump size for data forks - uint32_t next_cnid; - // next unused catalog id - uint32_t write_count; - // increment on every mount (and write ?) - uint64_t encodings_bmp; - // for every encoding used on the disk a bit is set - // ignored but eventually must be cared for - char finder_info[32]; - hfsp_fork_raw alloc_file; - // stores bitmap of use/free blocks - hfsp_fork_raw ext_file; - // stores oferflow extents - hfsp_fork_raw cat_file; - // This contains the root directory - hfsp_fork_raw attr_file; - hfsp_fork_raw start_file; - // a special startup file may be described here (used by ?) -} hfsp_vh; - -/* HFS+ volume attributes */ -/* 0-6 reserved, may be used in memory only */ -#define HFSPLUS_VOL_RESERVED1 0x000000FF -#define HFSPLUS_VOL_HARDLOCK 0x00000080 // Used in Memory by finder only -#define HFSPLUS_VOL_UNMNT 0x00000100 - // clear this bit when mounting, set as last step of unmounting - // This is checked by (slower) ROM code -#define HFSPLUS_VOL_SPARE_BLK 0x00000200 -#define HFSPLUS_VOL_NOCACHE 0x00000400 - // in case of RAM or ROM disk (try a HFS+ Ramdisk :) -#define HFSPLUS_VOL_INCNSTNT 0x00000800 - // Reverse meaning as of HFSPLUS_VOL_UNMNT - // This is checked by (faster) Mac OS code -/* 12-14 reserved */ -#define HFSPLUS_VOL_RESERVED2 0x00007000 -#define HFSPLUS_VOL_SOFTLOCK 0x00008000 -#define HFSPLUS_VOL_RESERVED3 0xFFFF0000 - - -int check_HFSP(disk_t *disk_car,partition_t *partition,const int verbose); +/*@ + @ requires \valid_read(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid_read(vh); + @ requires \valid_read(partition); + @ requires \separated(disk_car, vh, partition); + @*/ int test_HFSP(const disk_t *disk_car, const struct hfsp_vh *vh, const partition_t *partition, const int verbose, const int dump_ind); + +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid_read(vh); + @ requires \valid(partition); + @ requires \separated(disk_car, vh, partition); + @*/ int recover_HFSP(disk_t *disk_car, const struct hfsp_vh *vh, partition_t *partition, const int verbose, const int dump_ind, const int backup); #ifdef __cplusplus diff --git a/src/hfsp_struct.h b/src/hfsp_struct.h new file mode 100644 index 00000000..a03997b8 --- /dev/null +++ b/src/hfsp_struct.h @@ -0,0 +1,153 @@ +/* + File: hfsp_struct.h, TestDisk + + Copyright (C) 2005-2006 Christophe GRENIER + Original header comes from libhfs - library for reading and writing + Macintosh HFS volumes + Copyright (C) 2000 Klaus Halfmann + Original work by 1996-1998 Robert Leslie + other work 2000 from Brad Boyer (flar@pants.nu) + + This software is free software; you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation; either version 2 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License along + with this program; if not, write the Free Software Foundation, Inc., 51 + Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. + + */ +#ifndef _HFSP_STRUCT_H +#define _HFSP_STRUCT_H +#ifdef __cplusplus +extern "C" { +#endif + +#define HFSP_BOOT_SECTOR_SIZE 512 +#define HFSP_BLOCKSZ 512 /* A sector for Apple is always 512 bytes */ +#define HFSP_BLOCKSZ_BITS 9 /* 1<<9 == 512 */ +#define HFSP_VOLHEAD_SIG 0x482B /* 'H+' */ +#define HFSX_VOLHEAD_SIG 0x4858 /* 'HX' */ + +#define HFSP_VERSION 4 +#define HFSX_VERSION 5 + +// Minimum Key size for all btrees +#define HFSP_CAT_KEY_MIN_LEN 6 + +// Maximum Key size for all btrees +#define HFSP_CAT_KEY_MAX_LEN 516 + +/* HFS+ includes POSIX permissions , although marked as reserved they will be + * used as such. Is ignored by MacOS 8-9 but probably not by MacOS X. + */ +typedef struct { + uint32_t owner; + uint32_t group; + uint32_t mode; + uint32_t dev; +} hfsp_perm; + +/* A single contiguous area (fragment) of a file */ +typedef struct { + uint32_t start_block; + uint32_t block_count; +} hfsp_extent; + +/* A file may contain up to 8 normale extents, all other + are found in some extra extent area */ +typedef hfsp_extent hfsp_extent_rec[8]; + +/* Information for a "Fork" in a file + * Forks are the "usual" DATA and RSRC forks or special files + * (e.g. the Volume Bitmap) + */ +typedef struct { + uint64_t total_size; // logical size + uint32_t clump_size; // number of bytes to preallocate + uint32_t total_blocks; + hfsp_extent_rec extents; // initial (8) extents +} hfsp_fork_raw; + +/* HFS+ Volume Header + * Always found at block 2 of the disk, a copy is stored + * at the second to last block of the disk. + */ +typedef struct hfsp_vh { + uint16_t signature; // 00: must be HFSPLUS_VOLHEAD_SIG 'H+' + uint16_t version; // 02: 4 for HFS+, 5 for HFSX + uint32_t attributes; // 04: See bit constants below + uint32_t last_mount_vers; // 08 + // Use a registered creator code here (See libhfsp.h) + // Mac OS uses '8.10' well + uint32_t reserved; // 0C + + uint32_t create_date; // 10 local time ! + uint32_t modify_date; // 14 GMT (?) + uint32_t backup_date; // 18 GMT (?) + uint32_t checked_date; // 1C GMT (?) fsck ? + + uint32_t file_count; // 20 + // not including special files but including DATA and RSRC forks + uint32_t folder_count; // 24 excluding the root folder + + uint32_t blocksize; // 28 + // must be multiple of HFSPLUS_SECTOR_SIZE, + // should be a multiple of 4k for harddisk + uint32_t total_blocks; // 2C + uint32_t free_blocks; // 30 + // The total number of unused allocation blocks on the disk. + + uint32_t next_alloc; + // hint where to search for next allocation blocks + uint32_t rsrc_clump_sz; + // default clump size for rsrc forks + uint32_t data_clump_sz; + // default clump size for data forks + uint32_t next_cnid; + // next unused catalog id + uint32_t write_count; + // increment on every mount (and write ?) + uint64_t encodings_bmp; + // for every encoding used on the disk a bit is set + // ignored but eventually must be cared for + char finder_info[32]; + hfsp_fork_raw alloc_file; + // stores bitmap of use/free blocks + hfsp_fork_raw ext_file; + // stores oferflow extents + hfsp_fork_raw cat_file; + // This contains the root directory + hfsp_fork_raw attr_file; + hfsp_fork_raw start_file; + // a special startup file may be described here (used by ?) +} hfsp_vh; + +/* HFS+ volume attributes */ +/* 0-6 reserved, may be used in memory only */ +#define HFSPLUS_VOL_RESERVED1 0x000000FF +#define HFSPLUS_VOL_HARDLOCK 0x00000080 // Used in Memory by finder only +#define HFSPLUS_VOL_UNMNT 0x00000100 + // clear this bit when mounting, set as last step of unmounting + // This is checked by (slower) ROM code +#define HFSPLUS_VOL_SPARE_BLK 0x00000200 +#define HFSPLUS_VOL_NOCACHE 0x00000400 + // in case of RAM or ROM disk (try a HFS+ Ramdisk :) +#define HFSPLUS_VOL_INCNSTNT 0x00000800 + // Reverse meaning as of HFSPLUS_VOL_UNMNT + // This is checked by (faster) Mac OS code +/* 12-14 reserved */ +#define HFSPLUS_VOL_RESERVED2 0x00007000 +#define HFSPLUS_VOL_SOFTLOCK 0x00008000 +#define HFSPLUS_VOL_RESERVED3 0xFFFF0000 + +#ifdef __cplusplus +} /* closing brace for extern "C" */ +#endif +#endif