builtin type vs user type conflict

[xbauch]

//--------------------------------------------------------------------------------
//test.c
//--------------------------------------------------------------------------------
struct _IO_FILE;
struct _IO_marker;

struct _IO_FILE{
  int  Id_MCDC_2;
  char * Id_MCDC_3;
  char * Id_MCDC_4;
  char * Id_MCDC_5;
  char * Id_MCDC_6;
  char * Id_MCDC_7;
  char * Id_MCDC_8;
  char * Id_MCDC_9;
  char * Id_MCDC_10;
  char * Id_MCDC_11;
  char * Id_MCDC_12;
  char * Id_MCDC_13;
  struct _IO_marker* Id_MCDC_14;
  struct _IO_FILE* Id_MCDC_15;
  int  Id_MCDC_16;
  int  Id_MCDC_17;
  long Id_MCDC_18;
  unsigned short  Id_MCDC_19;
  signed char  Id_MCDC_20;
  char  Id_MCDC_21 [1];
  void* Id_MCDC_22;
  long long Id_MCDC_23;
  void * Id_MCDC_24;
  void * Id_MCDC_25;
  void * Id_MCDC_26;
  void * Id_MCDC_27;
  unsigned long int Id_MCDC_28;
   int  Id_MCDC_29;
  char  Id_MCDC_30 [20];
} ;

typedef struct _IO_FILE FILE;

extern FILE* fopen(char  const* filename, char const*mode);

int main()
{
  if (fopen("in.eds", "r") == ((void *)0));
  for (int i = 0; i < 2; i++);
}

CBMC version: cbmc-5.10-836-g273f375aa-dirty
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc --unwinding-assertions --unwind 2 test.c
What behaviour did you expect: not to see invariant violation
What happened instead: invariants were violated

Problem analysis

• The input code implements it's own version of fopen and FILE.
• CBMC warns about redefining a symbol during linking, but does not stop
• during flattening, CBMC converts the equality between return_value_fopen and fopen#return_value to bit-vectors
• an invariant of this conversion is that both sides of the equation are of the same type
• the lhs has the user-defined type FILE but the rhs has the builtin-defined type FILE
• the two types (both structs) differ in the names of their components (not types)

Proposed solutions

1. fail, by means of an exception, when user tries to redefine a builtin symbol
2. accept user defined symbol and give it precedence over builtin
3. override user defined symbol
4. change base_type_eq check to ignore struct component's names

[kroening]

This appears to be covered by regression/cbmc/Linking7.

My view is that we can't really stop people from linking together files with functions that have somewhat inconsistent signatures.

This should be detected during symbolic simulation, and an appropriate type cast should be added.

[peterschrammel]

In this case it's not just renaming of struct members; various additional members have been inserted into the struct...

[xbauch]

I guess the difference from Linking7 is that the user is unaware of the builtin implementation. Here the question remains whether we prefer user-defined or builtin.

[peterschrammel]

The user has already got that choice by using --no-library. It's all or nothing, though.
The problem remains that there is no error message that tells the user what to do.

[tautschnig]

I'm biased, but #2016 is my preference.

[kroening]

@xbauch may I ask you to check whether #3089 fixes this?

[xbauch]

Yes, it does.

[tautschnig]

@xbauch may I ask you to check whether #3089 fixes this?

Yes, it does.

I do note that this largely just fixes the symptoms. The fact that we'd effectively be using two different versions of the C library remain, but #2016 is on my stack.

[xbauch]

I've tried checking out #2016 and it also fixes the issue.

[kroening]

I think we need both -- there will be people who simply have type-inconsistent definitions and declarations of functions, not involving libraries, which requires #3089.
At the same time, it would be good to avoid this from happening in the first instance in the case of library functions, using #2016.

[tautschnig]

#6547 will be another piece to the puzzle as it will make sure function type conflicts can be resolved at all.