Hi
I've recently been looking at formal proof systems for minimizing bugs.
One common example is SPARK, which is an Ada variant which uses
contracts, guaranteed termination and lack of dynamic allocation to
make reasoning about SPARK programs much easier. This allows automatic
checking for things like overflows, out-of-bounds access and so on. A
great thing for code quality.
There is something similar for C called Frama-C (https://frama-c.com/).
It allows you to add contracts to functions and then attempts to prove
that the functions fulfill said contracts. Like SPARK it is also
possible to check for things like out-of-bounds accesses or
over/underflow. So I spent a few days going over qt-faststart.c (then
yet again after the recent patch), adding ACSL annotations here and
there, and rewriting parts of it to make the job of alt-ergo/why3/coq
much easier. It's far from done, roughly 29% of goals are yet to be
proven. But the purpose is to raise discussion rather than provide a
perfect solution.
I'd also like to know if anyone else on here has fiddled with frama-c,
and might know how one could make this part of the test system. For
example, I'd like a plot of % proved goals over time and the ability to
fail a build if a file that was 100% proved suddenly no longer is.
Doing this for a large project like FFmpeg is a serious undertaking,
but something I feel should really be done for all C projects. In my
case this is motivated by the recent cargo cult discussion about checks
in mxfdec.c, which an automated prover could take care of. There are of
course many more cases.
Patch attached. One thing I discovered is that all atom parsers expect
at least 8 bytes of atom data, so I was able to add contracts and
checks for that. Here's what "frama-c -wp -wp-rte qt-faststart.c" says
about it right now:
[wp] Proved goals: 240 / 340
Qed: 156 (4ms-16ms-1.2s)
Alt-Ergo: 84 (28ms-133ms-776ms) (403) (interrupted: 22)
(unknown: 78)
/TomasFrom d4e00db4d0922e745eb23b791b4f51e9d4e4d079 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <tjop...@acc.umu.se>
Date: Tue, 5 Jun 2018 10:26:00 +0200
Subject: [PATCH] frama-c:ify qt-faststart.c
It's far form perfect.
Some modifications have been made to make it easier to prove:
* some macros have been changed to inline functions
* function pointers have been replaced with an integer specifying the desired callback
* all atoms must be at least of size 8 (this already seemed to be the case, just not explicitly)
* update_stco_offsets() got a bit of a rework
---
tools/qt-faststart.c | 263 ++++++++++++++++++++++++++++++++++++++++++---------
1 file changed, 220 insertions(+), 43 deletions(-)
diff --git a/tools/qt-faststart.c b/tools/qt-faststart.c
index 5e88c38e6b..4b4733a418 100644
--- a/tools/qt-faststart.c
+++ b/tools/qt-faststart.c
@@ -42,33 +42,90 @@
#define ftello(x) _ftelli64(x)
#endif
-#define MIN(a,b) ((a) > (b) ? (b) : (a))
+/**
+First we do Proof by Weakest Precondition Calculus.
+We'll also want to do value analysis since thing can over/underflow.
+
+Some notes on WP options I've looked at:
+
+Option What I have to say What the manual says
+-----------------------------------------------------------------------------------------------------------------
+-wp Required to get it going Generate proof obligations for all (selected) properties.
+-wp-rte For dealing with run-time exceptions? Generate RTE guards before WP.
+-wp-dynamic Handle dynamic calls with specific annotations.
+-wp-init-const Use initializers for global const variables.
+-wp-invariants Handle generalized invariants inside loops.
+-wp-split Split conjunctions into sub-goals.
+-wp-model For setting memory model, such as
+ Hoare (simple, but incompatible with
+ heap memory pointers)
+
+frama-c -wp -wp-rte qt-faststart.c
+[wp] Proved goals: 240 / 340
+ Qed: 156 (4ms-18ms-1.4s)
+ Alt-Ergo: 84 (16ms-134ms-768ms) (403) (interrupted: 22) (unknown: 78)
+*/
+
+/*@ ensures a <= b ==> \result == a;
+ ensures a > b ==> \result == b;
+ assigns \nothing;
+ */
+static int64_t MIN(int64_t a, int64_t b)
+{
+ return a <= b ? a : b;
+}
-#define BE_32(x) (((uint32_t)(((uint8_t*)(x))[0]) << 24) | \
- (((uint8_t*)(x))[1] << 16) | \
- (((uint8_t*)(x))[2] << 8) | \
- ((uint8_t*)(x))[3])
+/*@ requires \valid(x + (0..3));
+ assigns \nothing;
+ */
+static uint32_t BE_32(const uint8_t *x)
+{
+ return ((uint32_t)x[0] << 24) +
+ ((uint32_t)x[1] << 16) +
+ ((uint32_t)x[2] << 8) +
+ x[3];
+}
-#define BE_64(x) (((uint64_t)(((uint8_t*)(x))[0]) << 56) | \
- ((uint64_t)(((uint8_t*)(x))[1]) << 48) | \
- ((uint64_t)(((uint8_t*)(x))[2]) << 40) | \
- ((uint64_t)(((uint8_t*)(x))[3]) << 32) | \
- ((uint64_t)(((uint8_t*)(x))[4]) << 24) | \
- ((uint64_t)(((uint8_t*)(x))[5]) << 16) | \
- ((uint64_t)(((uint8_t*)(x))[6]) << 8) | \
- ((uint64_t)( (uint8_t*)(x))[7]))
+/*@ requires \valid(x + (0..3));
+ assigns x[0..3];
+ */
+static void AV_WB32(uint8_t *x, uint32_t a)
+{
+ x[0] = a >> 24;
+ x[1] = a >> 16;
+ x[2] = a >> 8;
+ x[3] = a;
+}
-#define AV_WB32(p, val) { \
- ((uint8_t*)(p))[0] = ((val) >> 24) & 0xff; \
- ((uint8_t*)(p))[1] = ((val) >> 16) & 0xff; \
- ((uint8_t*)(p))[2] = ((val) >> 8) & 0xff; \
- ((uint8_t*)(p))[3] = (val) & 0xff; \
- }
+/*@ requires \valid(x + (0..7));
+ assigns \nothing;
+ */
+static uint64_t BE_64(const uint8_t *x)
+{
+ return ((uint64_t)x[0] << 56) +
+ ((uint64_t)x[1] << 48) +
+ ((uint64_t)x[2] << 40) +
+ ((uint64_t)x[3] << 32) +
+ ((uint64_t)x[4] << 24) +
+ ((uint64_t)x[5] << 16) +
+ ((uint64_t)x[6] << 8) +
+ x[7];
+}
-#define AV_WB64(p, val) { \
- AV_WB32(p, (val) >> 32) \
- AV_WB32(p + 4, val) \
- }
+/*@ requires \valid(x + (0..7));
+ assigns x[0..7];
+ */
+static void AV_WB64(uint8_t *x, uint64_t a)
+{
+ x[0] = a >> 56;
+ x[1] = a >> 48;
+ x[2] = a >> 40;
+ x[3] = a >> 32;
+ x[4] = a >> 24;
+ x[5] = a >> 16;
+ x[6] = a >> 8;
+ x[7] = a;
+}
#define BE_FOURCC(ch0, ch1, ch2, ch3) \
( (uint32_t)(unsigned char)(ch3) | \
@@ -122,23 +179,55 @@ typedef struct {
uint64_t new_moov_size;
} upgrade_stco_context_t;
-typedef int (*parse_atoms_callback_t)(void *context, atom_t *atom);
+//Called when fn == 0 in parse_atoms()
+static int update_chunk_offsets_callback(update_chunk_offsets_context_t *context, atom_t *atom);
+//Called when fn == 1 in parse_atoms()
+static int upgrade_stco_callback(upgrade_stco_context_t *context, atom_t *atom);
+/*@ requires size >= ATOM_PREAMBLE_SIZE;
+ requires \valid(buf + (0..size-1));
+ ensures -1 <= \result <= 0;
+
+ behavior update_chunk_offsets:
+ requires fn == 0;
+ requires \valid(chunk_context);
+ requires stco_context == NULL;
+
+ behavior upgrade_stco:
+ requires fn == 1;
+ requires chunk_context == NULL;
+ requires \valid(stco_context);
+
+ complete behaviors update_chunk_offsets, upgrade_stco;
+ */
static int parse_atoms(
unsigned char *buf,
uint64_t size,
- parse_atoms_callback_t callback,
- void *context)
+ int fn, //avoid function pointers
+ update_chunk_offsets_context_t *chunk_context,
+ upgrade_stco_context_t *stco_context)
{
unsigned char *pos = buf;
unsigned char *end = pos + size;
+ //@ assert end >= pos + ATOM_PREAMBLE_SIZE;
atom_t atom;
int ret;
+ //this needs work
+ /*@ loop invariant \valid(pos + (0..(ATOM_PREAMBLE_SIZE-1)));
+ loop invariant end - pos >= ATOM_PREAMBLE_SIZE;
+ loop invariant \valid(pos + (0 .. (end-pos-1)));
+ loop assigns pos;
+ loop variant end - pos;
+ */
while (end - pos >= ATOM_PREAMBLE_SIZE) {
+ //@ assert \valid(pos + (0..7));
atom.size = BE_32(pos);
atom.type = BE_32(pos + 4);
pos += ATOM_PREAMBLE_SIZE;
+ //we probably need to handle pos == end specially
+ //@ assert pos <= end;
+ //@ assert pos < end ==> \valid(pos + (0 .. (end-pos-1)));
atom.header_size = ATOM_PREAMBLE_SIZE;
switch (atom.size) {
@@ -148,6 +237,7 @@ static int parse_atoms(
return -1;
}
+ //@ assert \valid(pos + (0..7));
atom.size = BE_64(pos);
pos += 8;
atom.header_size = ATOM_PREAMBLE_SIZE + 8;
@@ -158,6 +248,7 @@ static int parse_atoms(
break;
}
+ //@ assert atom.header_size == 8 || atom.header_size == 16;
if (atom.size < atom.header_size) {
fprintf(stderr, "atom size %"PRIu64" too small\n", atom.size);
return -1;
@@ -170,8 +261,20 @@ static int parse_atoms(
return -1;
}
+ //both callbacks expect >= 8 bytes
+ if (atom.size < 8) {
+ fprintf(stderr, "atom size %"PRIu64" too small\n", atom.size);
+ return -1;
+ }
+
atom.data = pos;
- ret = callback(context, &atom);
+ //@ assert \valid(atom.data + ((-atom.header_size)..(atom.size-1)));
+ if (fn == 0) {
+ ret = update_chunk_offsets_callback(chunk_context, &atom);
+ } else { //1
+ ret = upgrade_stco_callback(stco_context, &atom);
+ }
+ //@ assert -1 <= ret <= 0;
if (ret < 0) {
return ret;
}
@@ -182,12 +285,15 @@ static int parse_atoms(
return 0;
}
+/*@ requires \valid(context);
+ requires \valid(atom);
+ requires 8 <= atom->size ==> \valid(atom->data + (0..(atom->size-1)));
+ ensures -1 <= \result <= 0;
+ */
static int update_stco_offsets(update_chunk_offsets_context_t *context, atom_t *atom)
{
uint32_t current_offset;
uint32_t offset_count;
- unsigned char *pos;
- unsigned char *end;
printf(" patching stco atom...\n");
if (atom->size < 8) {
@@ -195,29 +301,48 @@ static int update_stco_offsets(update_chunk_offsets_context_t *context, atom_t *
return -1;
}
+ //@ assert atom->size >= 8;
+ //@ assert \valid(atom->data + (0..7));
+ //@ assert \valid(atom->data + (0..(atom->size-1)));
offset_count = BE_32(atom->data + 4);
if (offset_count > (atom->size - 8) / 4) {
fprintf(stderr, "stco offset count %"PRIu32" too big\n", offset_count);
return -1;
}
+ //@ assert offset_count*4 + 8 <= atom->size;
+ //@ assert \valid(atom->data + (8 .. (8 + 4*offset_count - 1)));
context->stco_offset_count += offset_count;
context->stco_data_size += atom->size - 8;
- for (pos = atom->data + 8, end = pos + offset_count * 4;
- pos < end;
- pos += 4) {
+ /*@ loop invariant \valid(atom->data + ((8 + 4*i) .. (8 + 4*i + 3)));
+ loop assigns i;
+ loop variant offset_count - i;
+ */
+ for (uint32_t i = 0; i < offset_count; i++) {
+ //@ assert \valid(atom->data + ((8 + 4*i) .. (8 + 4*i + 3)));
+ unsigned char *pos = atom->data + 8 + 4*i;
+ //@ assert \valid(pos + (0..3));
current_offset = BE_32(pos);
if (current_offset > UINT_MAX - context->moov_atom_size) {
context->stco_overflow = 1;
+ //make frama-c happy
+ current_offset = ((uint64_t)current_offset + (context->moov_atom_size & 0xFFFFFFFF)) & 0xFFFFFFFF;
+ } else {
+ current_offset += context->moov_atom_size;
}
- current_offset += context->moov_atom_size;
+ //@ assert \valid(pos + (0..3));
AV_WB32(pos, current_offset);
}
return 0;
}
+/*@ requires \valid(context);
+ requires \valid(atom);
+ requires 8 <= atom->size ==> \valid(atom->data + (0..(atom->size-1)));
+ ensures -1 <= \result <= 0;
+ */
static int update_co64_offsets(update_chunk_offsets_context_t *context, atom_t *atom)
{
uint64_t current_offset;
@@ -248,9 +373,15 @@ static int update_co64_offsets(update_chunk_offsets_context_t *context, atom_t *
return 0;
}
-static int update_chunk_offsets_callback(void *ctx, atom_t *atom)
+/*@ requires \valid(context);
+ requires \valid(atom);
+ requires 8 <= atom->size;
+ requires 8 <= atom->header_size <= 16;
+ requires \valid(atom->data + ((-atom->header_size) .. (atom->size-1)));
+ ensures -1 <= \result <= 0;
+ */
+static int update_chunk_offsets_callback(update_chunk_offsets_context_t *context, atom_t *atom)
{
- update_chunk_offsets_context_t *context = ctx;
int ret;
switch (atom->type) {
@@ -274,15 +405,29 @@ static int update_chunk_offsets_callback(void *ctx, atom_t *atom)
ret = parse_atoms(
atom->data,
atom->size,
- update_chunk_offsets_callback,
- context);
+ 0,
+ context,
+ NULL);
context->depth--;
+ //@ assert -1 <= ret <= 0;
return ret;
}
return 0;
}
+/*@ behavior narrow_header:
+ requires header_size == 8;
+ requires \valid(header + (0..3));
+ assigns header[0..3];
+
+ behavior wide_header:
+ requires header_size == 16;
+ requires \valid(header + (8..15));
+ assigns header[8..15];
+
+ complete behaviors narrow_header, wide_header;
+ */
static void set_atom_size(unsigned char *header, uint32_t header_size, uint64_t size)
{
switch (header_size) {
@@ -296,6 +441,12 @@ static void set_atom_size(unsigned char *header, uint32_t header_size, uint64_t
}
}
+/*@ requires \valid(context);
+ requires \valid(atom);
+ requires 8 <= atom->size;
+ requires \valid(atom->data + (0 .. (atom->size-1)));
+ requires \valid(context->dest + (0..7));
+ */
static void upgrade_stco_atom(upgrade_stco_context_t *context, atom_t *atom)
{
unsigned char *pos;
@@ -325,9 +476,15 @@ static void upgrade_stco_atom(upgrade_stco_context_t *context, atom_t *atom)
}
}
-static int upgrade_stco_callback(void *ctx, atom_t *atom)
+/*@ requires \valid(context);
+ requires \valid(atom);
+ requires 8 <= atom->size;
+ requires 8 <= atom->header_size <= 16;
+ requires \valid(atom->data + ((-atom->header_size) .. (atom->size-1)));
+ ensures -1 <= \result <= 0;
+ */
+static int upgrade_stco_callback(upgrade_stco_context_t *context, atom_t *atom)
{
- upgrade_stco_context_t *context = ctx;
unsigned char *start_pos;
uint64_t copy_size;
@@ -350,7 +507,8 @@ static int upgrade_stco_callback(void *ctx, atom_t *atom)
if (parse_atoms(
atom->data,
atom->size,
- upgrade_stco_callback,
+ 1,
+ NULL,
context) < 0) {
return -1;
}
@@ -369,6 +527,12 @@ static int upgrade_stco_callback(void *ctx, atom_t *atom)
return 0;
}
+/*@ requires \valid(moov_atom);
+ requires \valid(moov_atom_size);
+ requires \valid((*moov_atom) + (0..(*moov_atom_size)));
+ requires *moov_atom_size >= 16;
+ ensures -1 <= \result <= 0;
+ */
static int update_moov_atom(
unsigned char **moov_atom,
uint64_t *moov_atom_size)
@@ -382,8 +546,9 @@ static int update_moov_atom(
if (parse_atoms(
*moov_atom,
*moov_atom_size,
- update_chunk_offsets_callback,
- &update_context) < 0) {
+ 0,
+ &update_context,
+ NULL) < 0) {
return -1;
}
@@ -409,7 +574,8 @@ static int update_moov_atom(
if (parse_atoms(
*moov_atom,
*moov_atom_size,
- upgrade_stco_callback,
+ 1,
+ NULL,
&upgrade_context) < 0) {
free(new_moov_atom);
return -1;
@@ -427,6 +593,11 @@ static int update_moov_atom(
return 0;
}
+/*@ requires argc >= 1;
+ requires \valid(argv + (0..argc-1));
+ requires \forall int i; 0 <= i <= argc-1 ==> \valid(argv[i]);
+ ensures 0 <= \result <= 1;
+ */
int main(int argc, char *argv[])
{
FILE *infile = NULL;
@@ -450,6 +621,8 @@ int main(int argc, char *argv[])
return 0;
}
+ //@ assert argc == 3;
+ //@ assert \valid(argv + (0..2));
if (!strcmp(argv[1], argv[2])) {
fprintf(stderr, "input and output files need to be different\n");
return 1;
@@ -485,6 +658,7 @@ int main(int argc, char *argv[])
atom_size);
goto error_out;
}
+ //@ assert \valid(ftyp_atom + (0..(ftyp_atom_size-1)));
if (fseeko(infile, -ATOM_PREAMBLE_SIZE, SEEK_CUR) ||
fread(ftyp_atom, atom_size, 1, infile) != 1 ||
(start_offset = ftello(infile)) < 0) {
@@ -566,6 +740,7 @@ int main(int argc, char *argv[])
fprintf(stderr, "could not allocate %"PRIu64" bytes for moov atom\n", atom_size);
goto error_out;
}
+ //@ assert \valid(moov_atom + (0..(moov_atom_size-1)));
if (fread(moov_atom, atom_size, 1, infile) != 1) {
perror(argv[1]);
goto error_out;
@@ -631,9 +806,11 @@ int main(int argc, char *argv[])
fprintf(stderr, "could not allocate %d bytes for copy_buffer\n", bytes_to_copy);
goto error_out;
}
+ //@ assert \valid(copy_buffer + (0..(bytes_to_copy-1)));
printf(" copying rest of file...\n");
while (last_offset) {
bytes_to_copy = MIN(bytes_to_copy, last_offset);
+ //@ assert \valid(copy_buffer + (0..(bytes_to_copy-1)));
if (fread(copy_buffer, bytes_to_copy, 1, infile) != 1) {
perror(argv[1]);
--
2.11.0
_______________________________________________
ffmpeg-devel mailing list
ffmpeg-devel@ffmpeg.org
http://ffmpeg.org/mailman/listinfo/ffmpeg-devel
