Apron: Invariants for variables of type `unsigned long` wrong

[michael-schwarz]

Consider the following program extracted from libaco which is one of the programs I am considering for #1417:

#include<pthread.h>
pthread_mutex_t mtx;
int g;

void *pmain(void *pthread_in_arg )
{
  unsigned long tmp_gl_ct ;

  pthread_mutex_lock(& mtx);
  tmp_gl_ct = g;
  pthread_mutex_unlock(& mtx);
  return ((void *)0);
}

int main()
{
  pthread_t t1;
  pthread_create(& t1, 0, pmain, 0);
  pthread_join(t1, 0);
  return 0;
}

Creating a YAML witness from it (via ./goblint --conf conf/traces-rel.json --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable allglobs -v --enable witness.yaml.enabled notlibaco.c --set witness.yaml.path notlibaco.yml) yields

- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bcbb0e1-df8c-4b8d-8a00-ea9aa25ab8b1
    creation_time: 2024-07-10T12:42:46Z
    producer:
      name: Goblint
      version: heads/michael-schwarz-dissertation-0-g970a99913-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/traces-rel.json'' ''--set'' ''ana.activated[+]''
        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
        ''mutex-meet-tid-cluster12'' ''--enable'' ''allglobs'' ''-v'' ''--enable''
        ''witness.yaml.enabled'' ''notlibaco.c'' ''--set'' ''witness.yaml.path'' ''notlibaco.yml'''
    task:
      input_files:
      - notlibaco.c
      input_file_hashes:
        notlibaco.c: e36c8d4402977c57e85e6fe02221ae759457e969afc37d9852c8c500d836c19f
      data_model: LP64
      language: C
  location:
    file_name: notlibaco.c
    file_hash: e36c8d4402977c57e85e6fe02221ae759457e969afc37d9852c8c500d836c19f
    line: 12
    column: 3
    function: pmain
  location_invariant:
    string: (0LL - (long long )g) + (long long )tmp_gl_ct >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13ab3ea7-f159-4c45-95ff-765acf3c0ec7
    creation_time: 2024-07-10T12:42:46Z
    producer:
      name: Goblint
      version: heads/michael-schwarz-dissertation-0-g970a99913-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/traces-rel.json'' ''--set'' ''ana.activated[+]''
        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
        ''mutex-meet-tid-cluster12'' ''--enable'' ''allglobs'' ''-v'' ''--enable''
        ''witness.yaml.enabled'' ''notlibaco.c'' ''--set'' ''witness.yaml.path'' ''notlibaco.yml'''
    task:
      input_files:
      - notlibaco.c
      input_file_hashes:
        notlibaco.c: e36c8d4402977c57e85e6fe02221ae759457e969afc37d9852c8c500d836c19f
      data_model: LP64
      language: C
  location:
    file_name: notlibaco.c
    file_hash: e36c8d4402977c57e85e6fe02221ae759457e969afc37d9852c8c500d836c19f
    line: 12
    column: 3
    function: pmain
  location_invariant:
    string: (long long )g + (long long )tmp_gl_ct >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d33de886-9d25-4455-a287-08e516c8a0ed
    creation_time: 2024-07-10T12:42:46Z
    producer:
      name: Goblint
      version: heads/michael-schwarz-dissertation-0-g970a99913-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/traces-rel.json'' ''--set'' ''ana.activated[+]''
        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
        ''mutex-meet-tid-cluster12'' ''--enable'' ''allglobs'' ''-v'' ''--enable''
        ''witness.yaml.enabled'' ''notlibaco.c'' ''--set'' ''witness.yaml.path'' ''notlibaco.yml'''
    task:
      input_files:
      - notlibaco.c
      input_file_hashes:
        notlibaco.c: e36c8d4402977c57e85e6fe02221ae759457e969afc37d9852c8c500d836c19f
      data_model: LP64
      language: C
  location:
    file_name: notlibaco.c
    file_hash: e36c8d4402977c57e85e6fe02221ae759457e969afc37d9852c8c500d836c19f
    line: 12
    column: 3
    function: pmain
  location_invariant:
    string: 0LL - (long long )g >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9484e898-6315-48a5-807f-f86dd2bd2ede
    creation_time: 2024-07-10T12:42:46Z
    producer:
      name: Goblint
      version: heads/michael-schwarz-dissertation-0-g970a99913-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/traces-rel.json'' ''--set'' ''ana.activated[+]''
        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
        ''mutex-meet-tid-cluster12'' ''--enable'' ''allglobs'' ''-v'' ''--enable''
        ''witness.yaml.enabled'' ''notlibaco.c'' ''--set'' ''witness.yaml.path'' ''notlibaco.yml'''
    task:
      input_files:
      - notlibaco.c
      input_file_hashes:
        notlibaco.c: e36c8d4402977c57e85e6fe02221ae759457e969afc37d9852c8c500d836c19f
      data_model: LP64
      language: C
  location:
    file_name: notlibaco.c
    file_hash: e36c8d4402977c57e85e6fe02221ae759457e969afc37d9852c8c500d836c19f
    line: 12
    column: 3
    function: pmain
  location_invariant:
    string: (long long )g >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 894f19db-b1ef-4982-83c0-cf4404861ab1
    creation_time: 2024-07-10T12:42:46Z
    producer:
      name: Goblint
      version: heads/michael-schwarz-dissertation-0-g970a99913-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/traces-rel.json'' ''--set'' ''ana.activated[+]''
        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
        ''mutex-meet-tid-cluster12'' ''--enable'' ''allglobs'' ''-v'' ''--enable''
        ''witness.yaml.enabled'' ''notlibaco.c'' ''--set'' ''witness.yaml.path'' ''notlibaco.yml'''
    task:
      input_files:
      - notlibaco.c
      input_file_hashes:
        notlibaco.c: e36c8d4402977c57e85e6fe02221ae759457e969afc37d9852c8c500d836c19f
      data_model: LP64
      language: C
  location:
    file_name: notlibaco.c
    file_hash: e36c8d4402977c57e85e6fe02221ae759457e969afc37d9852c8c500d836c19f
    line: 12
    column: 3
    function: pmain
  location_invariant:
    string: (long long )tmp_gl_ct >= 0LL
    type: assertion
    format: C

However, subsequent self-validation with ./goblint --conf conf/traces-rel.json --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable allglobs -v --set witness.yaml.validate notlibaco.yml notlibaco.c yields the message that only 2/5 invariants can be confirmed.

[Info][Witness] witness validation summary:
  confirmed: 2
  unconfirmed: 3
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 5

One of the invariants that cannot be re-confirmed, is (long long )tmp_gl_ct >= 0LL.
This is correct, as this invariant may not hold (if we assume uninitialized variables are top), as long long and unsigned long have the same bit-length but different ranges.

Wrong reasoning I used earlier:

• Invaraint holds vacuously as tmp_gl_ct has type unsigned long.

[michael-schwarz]

It does not have anything to do with logic to exclude temporaries, the problem is still there after renaming the variable.

[michael-schwarz]

Adding the assertion as a __goblint_check also can not be verified, so it seems the shortcoming may be on the generation side?

[sim642]

Maybe this has to do with the long long casts that we blindly add to all Apron invariants?

[michael-schwarz]

Nevertheless, it should still hold even after making this cast.

[michael-schwarz]

Actually claiming that this holds is in fact wrong! long long and long have the same length on LP64 machines, so this supposed invariant actually isn't one!

[michael-schwarz]

I now have the following minimal program

#include<pthread.h>
int *b;
pthread_mutex_t e;

void main() {
    int g;
    int a;
    b = &g;

    pthread_mutex_lock(&e);
}

where some 4 invariants cannot be shown after locking e, such as (4294967294LL - (long long )a) - (long long )g >= 0LL. Enabling the interval domain makes us able to show the assertions.

[michael-schwarz]

However, the bounds seem to be correct, they result from interval arithmetic. If I don't assign the address of g to b, verification also succeeds without intervals.

[sim642]

This minimal program locks a mutex in single-threaded mode which should be fine, but maybe we handle something incorrectly in such case? Or is the locking there just as a place for after-lock invariant generation?