Patch set updated for coreboot: f2d24f2 cbfstool: Make the add action choose an aligned entries capacity

[Sol Boucher]

Sol Boucher ([e-mail]) just uploaded a new patch set to gerrit, which you can find at http://review.coreboot.org/9939

-gerrit

commit f2d24f266ced816cd50bb2949306d2e66a1e083b
Author: Sol Boucher 
Date:   Fri Apr 3 09:13:04 2015 -0700

cbfstool: Make the add action choose an aligned entries capacity

This fixes an inconsistency between `cbfstool create` and `cbfstool add` that
    was resulting in confusing claims about the amount of free space at the end of a
    CBFS. Calls to `cbfstool add` check whether a file fits under a given empty file
    entry by testing whether it would collide with the beginning of the *subsequent*
    file header; thus, if a file's end is unaligned, its reported size will not
    match the actual available capacity. Although deleted entries always end on an
    alignment boundary because `cbfstool remove` expands them to fill the available
    space, `cbfstool create` doesn't necessarily size a new entries region to result
    in an empty entry with an aligned end.
    This problem never resulted in clobbering important data because cbfstool would
    blindly reserve 64B (or the selected alignment) of free space immediately after
    the all-inclusive empty file entry. This change alters the way this reservation
    is reported: only the overhang past the alignment is used as hidden padding, and
    the empty entry's capacity is always reported such that it ends at an aligned
    address.
    Much of the time that went into this patch was spent building trust in the
    trickery cbfstool employs to avoid explicitly tracking the image's total
    capacity for entries, so below are two proofs of correctness to save others time
    and discourage inadvertent breakage:

OBSERVATION (A): A check in cbfs_image_create() guarantees that an aligned CBFS
    empty file header is small enough that it won't cross another aligned address.

OBSERVATION (B): In cbfs_image_create(), the initial empty entry is sized such
    that its contents end on an aligned address.

THM. 1: Placing a new file within an empty entry located below an existing file
    entry will never leave an aligned flash address containing neither the beginning
    of a file header nor part of a file.
     We can prove this by contradiction: assume a newly-added file neither fills to
     the end of the preexisting empty entry nor leaves room for another aligned
     empty header after it. Then the first aligned address after the end of the
     newly-inserted file...
      - CASE 1: ...already contains a preexisting file entry header.
        + Then that address contains a file header.
      - CASE 2: ...does not already house a file entry header.
        + Then because CBFS content doesn't fall outside headers, the area between
          there and the *next* aligned address after that is unused.
        + By (A), we can fit a file header without clobbering anything.
        + Then that address now contains a file header.

THM. 2: Placing a new file in an empty entry at the very end of the image such
    that it fits, but leaves no room for a final header, is guaranteed not to change
    the total amount of space for entries, even if that new file is later removed
    from the CBFS.
     Again, we use contradiction: assume that creating such a file causes a
     permanent...
      - CASE 1: ...increase in the amount of available space.
        + Then the combination of the inserted file, its header, and any padding
          must have exceeded the empty entry in size enough for it to cross at
          least one additional aligned address, since aligned addresses are how
          the limit on an entry's capacity is determined.
        + But adding the file couldn't have caused us to write past any further
          aligned addresses because they are the boundary's used when verifying
          that sufficient capacity exists; furthermore, by (B), no entry can ever
          terminate beyond where the initial empty entry did when the CBFS was
          first created.
        + Then the creation of the file did not result in a space increase.
      - CASE 2: ...decrease in the amount of available space.
        + Then the end of the new file entry crosses at least one fewer aligned
          address than did the empty file entry.
        + Then by (A), there is room to place a new file entry that describes the
          remaining available space at the first available aligned address.
        + Then there is now a new record showing the same amount of available space.
        + Then the creation of the file did not result in a space decrease.

BUG=chromium:473726
    TEST=Had the following conversation with cbfstool:
    $ ./cbfstool test.image create -s 0x100000 -m arm
    Created CBFS image (capacity = 1048408 bytes)
    $ ./cbfstool test.image print
    test.image: 1024 kB, bootblocksize 0, romsize 1048576, offset 0x40
    alignment: 64 bytes, architecture: arm

Name                           Offset     Type         Size
    (empty)                        0x40       null         1048408
    $ dd if=/dev/zero of=toobigmed.bin bs=1048409 count=1
    1+0 records in
    1+0 records out
    1048409 bytes (1.0 MB) copied, 0.0057865 s, 181 MB/s
    $ ./cbfstool test.image add -t 0x50 -f toobigmed.bin -n toobig
    E: Could not add [toobigmed.bin, 1048409 bytes (1023 KB)@0x0]; too big?
    E: Failed to add 'toobigmed.bin' into ROM image.
    $ truncate -s -1 toobigmed.bin
    $ ./cbfstool test.image add -t 0x50 -f toobigmed.bin -n toobig
    $ ./cbfstool test.image print
    test.image: 1024 kB, bootblocksize 0, romsize 1048576, offset 0x40
    alignment: 64 bytes, architecture: arm

Name                           Offset     Type         Size
    toobig                         0x40       raw          1048408
    $ ./cbfstool test.image remove
    -n toobig
    $ ./cbfstool test.image print
    test.image: 1024 kB, bootblocksize 0, romsize 1048576, offset 0x40
    alignment: 64 bytes, architecture: arm

Name                           Offset     Type         Size
    (empty)                        0x40       deleted      1048408
    $ ./cbfstool test.image print
    test.image: 1024 kB, bootblocksize 0, romsize 1048576, offset 0x40
    alignment: 64 bytes, architecture: arm

Name                           Offset     Type         Size
    (empty)                        0x40       deleted      1048408
    BRANCH=None

Change-Id: I118743e37469ef0226970decc900db5d9b92c5df
    Signed-off-by: Sol Boucher 
    Original-Commit-Id: e317ddca14bc36bc36e6406b758378c88e9ae04e
    Original-Change-Id: I294ee489b4918646c359b06aa1581918f2d8badc
    Original-Signed-off-by: Sol Boucher 
    Original-Reviewed-on: https://chromium-review.googlesource.com/263962
    Original-Reviewed-by: Hung-Te Lin 
    Original-Reviewed-by: Stefan Reinauer 
---
 util/cbfstool/cbfs_image.c | 42 +++++++++++++++++++++++++++++++++++++++---
 1 file changed, 39 insertions(+), 3 deletions(-)

diff --git a/util/cbfstool/cbfs_image.c b/util/cbfstool/cbfs_image.c
index 2581bef..8e0e9a4 100644
--- a/util/cbfstool/cbfs_image.c
+++ b/util/cbfstool/cbfs_image.c
@@ -28,6 +28,24 @@
 #include "common.h"
 #include "cbfs_image.h"

+/* Even though the file-adding functions---cbfs_add_entry() and
+ * cbfs_add_entry_at()---perform their sizing checks against the beginning of
+ * the subsequent section rather than a stable recorded value such as an empty
+ * file header's len field, it's possible to prove two interesting properties
+ * about their behavior:
+ *  - Placing a new file within an empty entry located below an existing file
+ *    entry will never leave an aligned flash address containing neither the
+ *    beginning of a file header nor part of a file.
+ *  - Placing a new file in an empty entry at the very end of the image such
+ *    that it fits, but leaves no room for a final header, is guaranteed not to
+ *    change the total amount of space for entries, even if that new file is
+ *    later removed from the CBFS.
+ * These properties are somewhat nonobvious from the implementation, so the
+ * reader is encouraged to blame this comment and examine the full proofs
+ * in the commit message before making significant changes that would risk
+ * removing said guarantees.
+ */
+
 /* The file name align is not defined in CBFS spec -- only a preference by
  * (old) cbfstool. */
 #define CBFS_FILENAME_ALIGN	(16)
@@ -185,6 +203,16 @@ int cbfs_image_create(struct cbfs_image *image,
          bootblock_offset, bootblock->size,
          header_offset, sizeof(header), entries_offset);

+	// This attribute must be given in order to prove that this module
+	// correctly preserves certain CBFS properties. See the block comment
+	// near the top of this file (and the associated commit message).
+	size_t empty_header_len = cbfs_calculate_file_header_size("");
+	if (align < empty_header_len) {
+		ERROR("CBFS must be aligned to at least %zu bytes\n",
+							empty_header_len);
+		return -1;
+	}
+
    if (buffer_create(&image->buffer, size, "(new)") != 0)
    	return -1;
    if ((image->header = malloc(sizeof(*image->header))) == NULL)
@@ -263,7 +291,11 @@ int cbfs_image_create(struct cbfs_image *image,
    	cbfs_len = bootblock_offset;
    if (header_offset > entries_offset && header_offset < cbfs_len)
    	cbfs_len = header_offset;
-	cbfs_len -= entries_offset + align + entry_header_len;
+	// This alignment is necessary in order to prove that this module
+	// correctly preserves certain CBFS properties. See the block comment
+	// near the top of this file (and the associated commit message).
+	cbfs_len -= cbfs_len % align;
+	cbfs_len -= entries_offset + entry_header_len;
    cbfs_create_empty_entry(entry, cbfs_len, "");
    LOG("Created CBFS image (capacity = %d bytes)\n", cbfs_len);
    return 0;
@@ -462,8 +494,12 @@ static int cbfs_add_entry_at(struct cbfs_image *image,

assert(addr < addr_next);
    if (addr_next - addr < min_entry_size) {
-		DEBUG("No space after content to keep CBFS structure.\n");
-		return -1;
+		DEBUG("No need for new "empty" entry\n");
+		/* No need to increase the size of the just
+		 * stored file to extend to next file. Alignment
+		 * of next file takes care of this.
+		 */
+		return 0;
    }

len = addr_next - addr - min_entry_size;