Simple example where KLEE can miss a bug (due to floating point)

klee_output.txt

klee@e7588606c9e8:~$ klee --allow-external-sym-calls --libc=uclibc --posix-runtime ./toy_156.bc --sym-files 1 88 A
KLEE: NOTE: Using klee-uclibc : /home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using POSIX model: /home/klee/klee_build/klee/Release+Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/./klee-out-1"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 61828272) at /home/klee/klee_src/runtime/POSIX/fd.c:980
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: ioctl: (TCGETS) symbolic file, incomplete model
KLEE: WARNING ONCE: calling external: printf(61699472, (ReadLSB w32 12 A-data)) at [no debug info]
File timestamp: 0
File timestamp: 0
Entry: bar = , KLEE: WARNING ONCE: silently concretizing (reason: floating point) expression (ReadLSB w32 36 A-data) to value 0 (:0)
fdata = 0.000000
Unknown type 0
intdata = 0
Entry: bar = , fdata = 0.000000
Unknown type 0
intdata = 0
Entry: bar = , fdata = 0.000000
Unknown type 0
intdata = 0
Entry: bar = , fdata = 0.000000
Unknown type 0
intdata = 0
Entry: bar = , intdata = 0
Unknown type 0
fdata = 0.000000
Entry: bar = , intdata = 0
Unknown type 0
fdata = 0.000000
Entry: bar = , fdata = 0.000000
Unknown type 0
intdata = 0
Entry: bar = , fdata = 0.000000
intdata = 0
Unknown type 0
Entry: bar = , Entry: bar = , intdata = 0
fdata = 0.000000
Unknown type 0
Unknown type 0
fdata = 0.000000
intdata = 0
Entry: bar = , fdata = 0.000000
Entry: bar = , Unknown type 0
intdata = 0
Unknown type 0
fdata = 0.000000
intdata = 0
Entry: bar = , fdata = 0.000000
intdata = 0
Unknown type 0
Entry: bar = , fdata = 0.000000
Unknown type 0
intdata = 0

KLEE: done: total instructions = 28413
KLEE: done: completed paths = 62
KLEE: done: generated tests = 62

testsmall-fuzzed-156.bin

toy_156.c

#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>

#pragma pack(1)
#define MAGIC 0x4c415641

unsigned int lava = 0;

enum {
    TYPEA = 1,
    TYPEB = 2
};

typedef struct {
    uint32_t magic;     // Magic value
    uint32_t reserved;  // Reserved for future use
    uint16_t num_recs;  // How many entries?
    uint16_t flags;     // None used yet
    uint32_t timestamp; // Unix Time
} file_header;

typedef struct {
    char bar[16];
    uint32_t type;
    union {
        float fdata;
        uint32_t intdata;
    } data;
} file_entry;

void parse_header(FILE *f, file_header *hdr) {
    if (1 != fread(hdr, sizeof(file_header), 1, f))
        exit(1);
    if (hdr->magic != MAGIC)
        exit(1);
}

file_entry * parse_record(FILE *f) {
    file_entry *ret = (file_entry *) malloc(sizeof(file_entry));
    if (1 != fread(ret, sizeof(file_entry), 1, f))
        exit(1);
    return ret;
}

void consume_record(file_entry *ent) {
    printf("Entry: bar = %.*s, ", 16, ent->bar);
    if (ent->type == TYPEA) {
        printf("fdata = %f\n", ent->data.fdata);
        if (ent)  {
            lava = ent->data.intdata;
        }
    }
    else if (ent->type == TYPEB) {
        printf("intdata = %u\n", ent->data.intdata);
    }
    else {
        printf("Unknown type %x\n", ent->type);
        exit(1);
    }
    free(ent);
}

int main(int argc, char **argv) {
    if (argc < 2) return 0;
    FILE *f = fopen(argv[1], "rb");
    file_header head;

    parse_header(f, &head);
    printf("File timestamp: %u\n", head.timestamp);

    unsigned i;
    for (i = 0; i < head.num_recs; i++) {
        file_entry *ent = parse_record(f);
        consume_record(ent + (lava * (0x6c61755d==lava)));
    }
    return 0;
}