correctcomputation / checkedc-clang

This is the primary development repository for 3C, a tool for automatically converting legacy C code to the Checked C extension of C, which aims to enforce spatial memory safety. This repository is a fork of Checked C's.
14 stars 5 forks source link

3C produces different output for multiple files based on ordering #212

Closed sroy4899 closed 4 years ago

sroy4899 commented 4 years ago

Consider the two programs file1.c and file2.c. file1.c

typedef unsigned long size_t;
extern _Itype_for_any(T) void *calloc(size_t nmemb, size_t size) : itype(_Array_ptr<T>) byte_count(nmemb * size);
extern _Itype_for_any(T) void *malloc(size_t size) : itype(_Array_ptr<T>) byte_count(size);

int ** foo(int *);

int ** bar() {
    int *y = calloc(5, sizeof(int)); 
    int i;
    for(i = 0; i < 5; i++) { 
        y[i] = i+1;
    }
    int **z = foo(y);
    return z; 
}

file2.c:

typedef unsigned long size_t;
extern _Itype_for_any(T) void *calloc(size_t nmemb, size_t size) : itype(_Array_ptr<T>) byte_count(nmemb * size);

int ** foo(int *y) {
    int **z = calloc(5, sizeof(int *)); 
    int i;
    for(i = 0; i < 5; i++) { 
        z[i] = &y[i];
    }
    return z; 
}

When converting these programs, however, based on the order in which they are provided, the output differs:

cconv-standalone -alltypes -output-postfix=ONEFIRST file1.c file2.c ; 
cconv-standalone -alltypes -output-postfix=TWOFIRST file2.c file1.c
diff file1.ONEFIRST.c file1.TWOFIRST.c
... 
    6c6
    `< _Nt_array_ptr<_Ptr<int>> foo(_Array_ptr<int> y);
    ---
    > _Nt_array_ptr<_Ptr<int>> foo(_Array_ptr<int> y : count(5));
Machiry commented 4 years ago

Also, why are we not inferring length for:Why are we not inferring the length of p_nodes ? (Line 55) Ref: https://github.com/plum-umd/checkedc-clang/commit/93575edd96b29640fc8c83712ec100af9d9bc41f