From 160350774fdb60771a624c7d293b9bf474aa21d2 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sun, 14 Mar 2021 16:16:49 +0100 Subject: [PATCH] src/file_xfs.c: add Frama-C annotations src/xfs_struct.h: move structure from src/xfs.h --- src/Makefile.am | 4 +- src/file_xfs.c | 109 ++++++++++++++++++++++++++------------------ src/xfs.h | 78 +------------------------------- src/xfs_struct.h | 115 +++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 183 insertions(+), 123 deletions(-) create mode 100644 src/xfs_struct.h diff --git a/src/Makefile.am b/src/Makefile.am index 4fbb3c94..d1508ccd 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 hfsp_struct.h luks.h luks_struct.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 luks_struct.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 xfs_struct.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 @@ -390,7 +390,7 @@ file_C = filegen.c \ file_zpr.c \ utfsize.c -file_H = ext2.h hfsp_struct.h filegen.h file_doc.h file_jpg.h file_gz.h file_riff.h file_sp3.h file_tar.h file_tiff.h luks_struct.h ntfs_struct.h ole.h pe.h suspend.h utfsize.h +file_H = ext2.h hfsp_struct.h filegen.h file_doc.h file_jpg.h file_gz.h file_riff.h file_sp3.h file_tar.h file_tiff.h luks_struct.h ntfs_struct.h ole.h pe.h suspend.h utfsize.h xfs_struct.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_xfs.c b/src/file_xfs.c index 52fd7820..a309fbdd 100644 --- a/src/file_xfs.c +++ b/src/file_xfs.c @@ -30,55 +30,71 @@ #include #include "types.h" #include "common.h" -#include "xfs.h" +#include "xfs_struct.h" #include "filegen.h" +/*@ requires \valid(file_stat); */ static void register_header_check_xfs(file_stat_t *file_stat); -static int header_check_xfs_sb(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 file_hint_t file_hint_xfs= { - .extension="xfs", - .description="xfs structure", - .max_filesize=0, - .recover=1, - .enable_by_default=1, - .register_header_check=®ister_header_check_xfs +const file_hint_t file_hint_xfs = { + .extension = "xfs", + .description = "xfs structure", + .max_filesize = 0, + .recover = 1, + .enable_by_default = 1, + .register_header_check = ®ister_header_check_xfs }; +/*@ + @ requires buffer_size >= sizeof(struct xfs_sb); + @ 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_xfs, buffer+(..), file_recovery, file_recovery_new); + @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @ assigns *file_recovery_new; + @*/ static int header_check_xfs_sb(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 xfs_sb *sb=(const struct xfs_sb *)buffer; - const unsigned int sb_blocksize=be32(sb->sb_blocksize); - if( sb->sb_sectlog >= 16 || - sb->sb_inodelog >= 16 || - sb->sb_blocklog >= 16) + const struct xfs_sb *sb = (const struct xfs_sb *)buffer; + const unsigned int sb_blocksize = be32(sb->sb_blocksize); + if(sb->sb_sectlog >= 16 || sb->sb_inodelog >= 16 || sb->sb_blocklog >= 16) return 0; - if(sb->sb_magicnum!=be32(XFS_SB_MAGIC) || - be16(sb->sb_sectsize) != (1U << sb->sb_sectlog) || - sb_blocksize != (1U << sb->sb_blocklog) || - be16(sb->sb_inodesize) != (1U << sb->sb_inodelog)) + if(sb->sb_magicnum != be32(XFS_SB_MAGIC) || be16(sb->sb_sectsize) != (1U << sb->sb_sectlog) || sb_blocksize != (1U << sb->sb_blocklog) || be16(sb->sb_inodesize) != (1U << sb->sb_inodelog)) return 0; reset_file_recovery(file_recovery_new); - file_recovery_new->extension=file_hint_xfs.extension; - file_recovery_new->calculated_file_size=sb_blocksize; - file_recovery_new->data_check=&data_check_size; - file_recovery_new->file_check=&file_check_size; + file_recovery_new->extension = file_hint_xfs.extension; + file_recovery_new->calculated_file_size = sb_blocksize; + file_recovery_new->data_check = &data_check_size; + file_recovery_new->file_check = &file_check_size; return 1; } +/*@ assigns \nothing; */ static data_check_t data_check_stopasap(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) { return DC_STOP; } +/*@ + @ requires buffer_size > 0; + @ 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_xfs, buffer+(..), file_recovery, file_recovery_new); + @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @ assigns *file_recovery_new; + @*/ static int header_save_xfs(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) { - if(safe_header_only>0) + if(safe_header_only > 0) return 0; reset_file_recovery(file_recovery_new); - file_recovery_new->extension=file_hint_xfs.extension; - file_recovery_new->data_check=&data_check_stopasap; - file_recovery_new->min_filesize=512; + file_recovery_new->extension = file_hint_xfs.extension; + file_recovery_new->data_check = &data_check_stopasap; + file_recovery_new->min_filesize = 512; return 1; } @@ -88,9 +104,9 @@ typedef struct xfs_timestamp int32_t t_nsec; } xfs_timestamp_t; -typedef int64_t xfs_fsize_t; /* bytes in a file */ -typedef int32_t xfs_extnum_t; /* # of extents in a file */ -typedef int16_t xfs_aextnum_t; /* # extents in an attribute fork */ +typedef int64_t xfs_fsize_t; /* bytes in a file */ +typedef int32_t xfs_extnum_t; /* # of extents in a file */ +typedef int16_t xfs_aextnum_t; /* # extents in an attribute fork */ typedef struct xfs_dinode_core { @@ -121,31 +137,36 @@ typedef struct xfs_dinode_core uint32_t di_gen; } xfs_dinode_core_t; +/*@ + @ requires buffer_size >= sizeof(xfs_dinode_core_t); + @ 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_xfs, buffer+(..), file_recovery, file_recovery_new); + @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @ assigns *file_recovery_new; + @*/ static int header_check_xfs_inode(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 xfs_dinode_core_t *inode=(const xfs_dinode_core_t *)buffer; - if(safe_header_only>0) + const xfs_dinode_core_t *inode = (const xfs_dinode_core_t *)buffer; + if(safe_header_only > 0) return 0; - if(inode->di_version!=2 || - inode->di_pad[0]!=0 || inode->di_pad[1]!=0 || - inode->di_pad[2]!=0 || inode->di_pad[3]!=0 || - inode->di_pad[4]!=0 || inode->di_pad[5]!=0 || - inode->di_pad[6]!=0 || inode->di_pad[7]!=0) + if(inode->di_version != 2 || inode->di_pad[0] != 0 || inode->di_pad[1] != 0 || inode->di_pad[2] != 0 || inode->di_pad[3] != 0 || inode->di_pad[4] != 0 || inode->di_pad[5] != 0 || inode->di_pad[6] != 0 || inode->di_pad[7] != 0) return 0; reset_file_recovery(file_recovery_new); - file_recovery_new->extension=file_hint_xfs.extension; - file_recovery_new->data_check=&data_check_stopasap; + file_recovery_new->extension = file_hint_xfs.extension; + file_recovery_new->data_check = &data_check_stopasap; return 1; } - static void register_header_check_xfs(file_stat_t *file_stat) { - static const unsigned char xagf[8]={'X','A','G','F', 0,0,0,1}; - static const unsigned char xagi[8]={'X','A','G','I', 0,0,0,1}; - static const unsigned char abtb[8]={'A','B','T','B', 0,0,0,1}; - static const unsigned char abtc[8]={'A','B','T','C', 0,0,0,1}; - static const unsigned char iabt[8]={'I','A','B','T', 0,0,0,1}; + static const unsigned char xagf[8] = { 'X', 'A', 'G', 'F', 0, 0, 0, 1 }; + static const unsigned char xagi[8] = { 'X', 'A', 'G', 'I', 0, 0, 0, 1 }; + static const unsigned char abtb[8] = { 'A', 'B', 'T', 'B', 0, 0, 0, 1 }; + static const unsigned char abtc[8] = { 'A', 'B', 'T', 'C', 0, 0, 0, 1 }; + static const unsigned char iabt[8] = { 'I', 'A', 'B', 'T', 0, 0, 0, 1 }; register_header_check(0, "XFSB", 4, &header_check_xfs_sb, file_stat); register_header_check(0, xagf, 8, &header_save_xfs, file_stat); register_header_check(0, xagi, 8, &header_save_xfs, file_stat); diff --git a/src/xfs.h b/src/xfs.h index dbd654be..f55d1498 100644 --- a/src/xfs.h +++ b/src/xfs.h @@ -22,6 +22,7 @@ * */ +#include "xfs_struct.h" /* * Super block * Fits into a sector-sized buffer at address 0 of each allocation group. @@ -33,83 +34,6 @@ extern "C" { #endif -#define XFS_SUPERBLOCK_SIZE 512 - -#define XFS_SB_MAGIC 0x58465342 /* 'XFSB' */ -#define XFS_SB_VERSION_1 1 /* 5.3, 6.0.1, 6.1 */ -#define XFS_SB_VERSION_2 2 /* 6.2 - attributes */ -#define XFS_SB_VERSION_3 3 /* 6.2 - new inode version */ -#define XFS_SB_VERSION_4 4 /* 6.2+ - bitmask version */ -#define XFS_SB_VERSION_5 5 /* CRC enabled filesystem */ -#define XFS_SB_VERSION_NUMBITS 0x000f - -typedef uint32_t xfs_extlen_t; /* extent length in blocks */ -typedef uint64_t xfs_drfsbno_t; /* blockno in filesystem (raw) */ -typedef uint64_t xfs_drtbno_t; /* extent (block) in realtime area */ -typedef uint64_t xfs_ino_t; /* type */ -typedef uint32_t xfs_agblock_t; /* blockno in alloc. group */ -typedef uint32_t xfs_agnumber_t; /* allocation group number */ -typedef uint64_t xfs_dfsbno_t; - -struct xfs_sb -{ - uint32_t sb_magicnum; /* magic number == XFS_SB_MAGIC */ - uint32_t sb_blocksize; /* logical block size, bytes */ - xfs_drfsbno_t sb_dblocks; /* number of data blocks */ - xfs_drfsbno_t sb_rblocks; /* number of realtime blocks */ - xfs_drtbno_t sb_rextents; /* number of realtime extents */ - uint8_t sb_uuid[16]; /* file system unique id */ - xfs_dfsbno_t sb_logstart; /* starting block of log if internal */ - xfs_ino_t sb_rootino; /* root inode number */ - xfs_ino_t sb_rbmino; /* bitmap inode for realtime extents */ - xfs_ino_t sb_rsumino; /* summary inode for rt bitmap */ - xfs_agblock_t sb_rextsize; /* realtime extent size, blocks */ - xfs_agblock_t sb_agblocks; /* size of an allocation group */ - xfs_agnumber_t sb_agcount; /* number of allocation groups */ - xfs_extlen_t sb_rbmblocks; /* number of rt bitmap blocks */ - xfs_extlen_t sb_logblocks; /* number of log blocks */ - uint16_t sb_versionnum; /* header version == XFS_SB_VERSION */ - uint16_t sb_sectsize; /* volume sector size, bytes */ - uint16_t sb_inodesize; /* inode size, bytes */ - uint16_t sb_inopblock; /* inodes per block */ - char sb_fname[12]; /* file system name */ - uint8_t sb_blocklog; /* log2 of sb_blocksize */ - uint8_t sb_sectlog; /* log2 of sb_sectsize */ - uint8_t sb_inodelog; /* log2 of sb_inodesize */ - uint8_t sb_inopblog; /* log2 of sb_inopblock */ - uint8_t sb_agblklog; /* log2 of sb_agblocks (rounded up) */ - uint8_t sb_rextslog; /* log2 of sb_rextents */ - uint8_t sb_inprogress; /* mkfs is in progress, don't mount */ - uint8_t sb_imax_pct; /* max % of fs for inode space */ - /* statistics */ - /* - * These fields must remain contiguous. If you really - * want to change their layout, make sure you fix the - * code in xfs_trans_apply_sb_deltas(). - */ - uint64_t sb_icount; /* allocated inodes */ - uint64_t sb_ifree; /* free inodes */ - uint64_t sb_fdblocks; /* free data blocks */ - uint64_t sb_frextents; /* free realtime extents */ - /* - * End contiguous fields. - */ - xfs_ino_t sb_uquotino; /* user quota inode */ - xfs_ino_t sb_gquotino; /* group quota inode */ - uint16_t sb_qflags; /* quota flags */ - uint8_t sb_flags; /* misc. flags */ - uint8_t sb_shared_vn; /* shared version number */ - xfs_extlen_t sb_inoalignmt; /* inode chunk alignment, fsblocks */ - uint32_t sb_unit; /* stripe or raid unit */ - uint32_t sb_width; /* stripe or raid width */ - uint8_t sb_dirblklog; /* log2 of dir block size (fsbs) */ - uint8_t sb_logsectlog; /* log2 of the log sector size */ - uint16_t sb_logsectsize; /* sector size for the log, bytes */ - uint32_t sb_logsunit; /* stripe unit size for the log */ - uint32_t sb_features2; /* additonal feature bits */ -} __attribute__ ((gcc_struct, __packed__)); - - /*@ @ requires \valid(disk_car); @ requires \valid(partition); diff --git a/src/xfs_struct.h b/src/xfs_struct.h new file mode 100644 index 00000000..dea602f7 --- /dev/null +++ b/src/xfs_struct.h @@ -0,0 +1,115 @@ +/* + * File xfs_struct.h + * + * This program is free software; you can redistribute it and/or modify it + * under the terms of version 2 of the GNU General Public License as + * published by the Free Software Foundation. + * + * This program is distributed in the hope that it would be useful, but + * WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + * + * Further, this software is distributed without any warranty that it is + * free of the rightful claim of any third person regarding infringement + * or the like. Any license provided herein, whether implied or + * otherwise, applies only to this software file. Patent licenses, if + * any, provided herein do not apply to combinations of this program with + * other software, or any other product whatsoever. + * + * 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. + * + */ + +/* + * Super block + * Fits into a sector-sized buffer at address 0 of each allocation group. + * Only the first of these is ever updated except during growfs. + */ +#ifndef _XFS_STRUCT_H +#define _XFS_STRUCT_H +#ifdef __cplusplus +extern "C" { +#endif + +#define XFS_SUPERBLOCK_SIZE 512 + +#define XFS_SB_MAGIC 0x58465342 /* 'XFSB' */ +#define XFS_SB_VERSION_1 1 /* 5.3, 6.0.1, 6.1 */ +#define XFS_SB_VERSION_2 2 /* 6.2 - attributes */ +#define XFS_SB_VERSION_3 3 /* 6.2 - new inode version */ +#define XFS_SB_VERSION_4 4 /* 6.2+ - bitmask version */ +#define XFS_SB_VERSION_5 5 /* CRC enabled filesystem */ +#define XFS_SB_VERSION_NUMBITS 0x000f + +typedef uint32_t xfs_extlen_t; /* extent length in blocks */ +typedef uint64_t xfs_drfsbno_t; /* blockno in filesystem (raw) */ +typedef uint64_t xfs_drtbno_t; /* extent (block) in realtime area */ +typedef uint64_t xfs_ino_t; /* type */ +typedef uint32_t xfs_agblock_t; /* blockno in alloc. group */ +typedef uint32_t xfs_agnumber_t; /* allocation group number */ +typedef uint64_t xfs_dfsbno_t; + +struct xfs_sb +{ + uint32_t sb_magicnum; /* magic number == XFS_SB_MAGIC */ + uint32_t sb_blocksize; /* logical block size, bytes */ + xfs_drfsbno_t sb_dblocks; /* number of data blocks */ + xfs_drfsbno_t sb_rblocks; /* number of realtime blocks */ + xfs_drtbno_t sb_rextents; /* number of realtime extents */ + uint8_t sb_uuid[16]; /* file system unique id */ + xfs_dfsbno_t sb_logstart; /* starting block of log if internal */ + xfs_ino_t sb_rootino; /* root inode number */ + xfs_ino_t sb_rbmino; /* bitmap inode for realtime extents */ + xfs_ino_t sb_rsumino; /* summary inode for rt bitmap */ + xfs_agblock_t sb_rextsize; /* realtime extent size, blocks */ + xfs_agblock_t sb_agblocks; /* size of an allocation group */ + xfs_agnumber_t sb_agcount; /* number of allocation groups */ + xfs_extlen_t sb_rbmblocks; /* number of rt bitmap blocks */ + xfs_extlen_t sb_logblocks; /* number of log blocks */ + uint16_t sb_versionnum; /* header version == XFS_SB_VERSION */ + uint16_t sb_sectsize; /* volume sector size, bytes */ + uint16_t sb_inodesize; /* inode size, bytes */ + uint16_t sb_inopblock; /* inodes per block */ + char sb_fname[12]; /* file system name */ + uint8_t sb_blocklog; /* log2 of sb_blocksize */ + uint8_t sb_sectlog; /* log2 of sb_sectsize */ + uint8_t sb_inodelog; /* log2 of sb_inodesize */ + uint8_t sb_inopblog; /* log2 of sb_inopblock */ + uint8_t sb_agblklog; /* log2 of sb_agblocks (rounded up) */ + uint8_t sb_rextslog; /* log2 of sb_rextents */ + uint8_t sb_inprogress; /* mkfs is in progress, don't mount */ + uint8_t sb_imax_pct; /* max % of fs for inode space */ + /* statistics */ + /* + * These fields must remain contiguous. If you really + * want to change their layout, make sure you fix the + * code in xfs_trans_apply_sb_deltas(). + */ + uint64_t sb_icount; /* allocated inodes */ + uint64_t sb_ifree; /* free inodes */ + uint64_t sb_fdblocks; /* free data blocks */ + uint64_t sb_frextents; /* free realtime extents */ + /* + * End contiguous fields. + */ + xfs_ino_t sb_uquotino; /* user quota inode */ + xfs_ino_t sb_gquotino; /* group quota inode */ + uint16_t sb_qflags; /* quota flags */ + uint8_t sb_flags; /* misc. flags */ + uint8_t sb_shared_vn; /* shared version number */ + xfs_extlen_t sb_inoalignmt; /* inode chunk alignment, fsblocks */ + uint32_t sb_unit; /* stripe or raid unit */ + uint32_t sb_width; /* stripe or raid width */ + uint8_t sb_dirblklog; /* log2 of dir block size (fsbs) */ + uint8_t sb_logsectlog; /* log2 of the log sector size */ + uint16_t sb_logsectsize; /* sector size for the log, bytes */ + uint32_t sb_logsunit; /* stripe unit size for the log */ + uint32_t sb_features2; /* additonal feature bits */ +} __attribute__ ((gcc_struct, __packed__)); + +#ifdef __cplusplus +} /* closing brace for extern "C" */ +#endif +#endif