Fixpoint not reached with address sets

[michael-schwarz]

I extracted this small sample from goblint/bench#7 via creduce.

int a;

int main() { c(&a); }
int c(int *f) {
  unsigned long d;
  int *e = &a;
  d = 0;
  while (1) {
    e = f++;
    d++;
  }
}

The issue is HoarePO: {a[def_exc:Unknown int([-63,63])], a, NULL, ?} not leq {a[def_exc:Unknown int([-63,63])], a[def_exc:Unknown int([-63,63])], NULL, ?}.

Full message:

michael@michael-ThinkPad-X1-Carbon-6th:~/Documents/goblint-cil/analyzer$ ./goblint 1.c
Fixpoint not reached at node 84 "tmp = f;" on 1.c:10:5-10:12
 Solver computed:
 {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(),
    top or Set (variables):{}, booleans:False, MT mode:Singlethreaded,
    Thread * lifted created and Unit:(([main], {}), bot),
    value domain * array partitioning deps * Vars with Weak Update * P:(mapping {
                                                                          Global {
                                                                            a ->
                                                                              (0)
                                                                          }
                                                                          Local {
                                                                            d ->
                                                                              (Unknown int([0,64]))
                                                                            e ->
                                                                              {&a[def_exc:Unknown int([-63,63])], &a[def_exc:Unknown int([-63,63])], &a}
                                                                          }
                                                                          Parameter {
                                                                            f ->
                                                                              {&a[def_exc:Unknown int([-63,63])], &a}
                                                                          }
                                                                          Temp {
                                                                            tmp ->
                                                                              {&a[def_exc:Unknown int([-63,63])], &a[def_exc:Unknown int([-63,63])], NULL, ?}
                                                                          }
                                                                        }, mapping {
                                                                               }, {}, {}),
    lifted node:Unknown node, Unit:()], mapping {
                                          })}
 Right-Hand-Side:
 {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(),
    top or Set (variables):{}, booleans:False, MT mode:Singlethreaded,
    Thread * lifted created and Unit:(([main], {}), bot),
    value domain * array partitioning deps * Vars with Weak Update * P:(mapping {
                                                                          Global {
                                                                            a ->
                                                                              (0)
                                                                          }
                                                                          Local {
                                                                            d ->
                                                                              (Unknown int([0,8]))
                                                                            e ->
                                                                              {&a[def_exc:Unknown int([-63,63])], &a}
                                                                          }
                                                                          Parameter {
                                                                            f ->
                                                                              {&a[def_exc:Unknown int([-63,63])], &a}
                                                                          }
                                                                          Temp {
                                                                            tmp ->
                                                                              {&a[def_exc:Unknown int([-63,63])], &a, NULL, ?}
                                                                          }
                                                                        }, mapping {
                                                                               }, {}, {}),
    lifted node:Unknown node, Unit:()], mapping {
                                          })}
 Difference: ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(),
               top or Set (variables):{}, booleans:False,
               MT mode:Singlethreaded,
               Thread * lifted created and Unit:(([main], {}), bot),
               value domain * array partitioning deps * Vars with Weak Update * P:(mapping {
                                                                                     Global {
                                                                                       a ->
                                                                                         (0)
                                                                                     }
                                                                                     Local {
                                                                                       d ->
                                                                                         (Unknown int([0,8]))
                                                                                       e ->
                                                                                         {&a[def_exc:Unknown int([-63,63])], &a}
                                                                                     }
                                                                                     Parameter {
                                                                                       f ->
                                                                                         {&a[def_exc:Unknown int([-63,63])], &a}
                                                                                     }
                                                                                     Temp {
                                                                                       tmp ->
                                                                                         {&a[def_exc:Unknown int([-63,63])], &a, NULL, ?}
                                                                                     }
                                                                                   }, mapping {
                                                                                          }, {}, {}),
               lifted node:Unknown node, Unit:()], mapping {
                                                     }):
 not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(),
           top or Set (variables):{}, booleans:False, MT mode:Singlethreaded,
           Thread * lifted created and Unit:(([main], {}), bot),
           value domain * array partitioning deps * Vars with Weak Update * P:(mapping {
                                                                                 Global {
                                                                                   a ->
                                                                                     (0)
                                                                                 }
                                                                                 Local {
                                                                                   d ->
                                                                                     (Unknown int([0,64]))
                                                                                   e ->
                                                                                     {&a[def_exc:Unknown int([-63,63])], &a[def_exc:Unknown int([-63,63])], &a}
                                                                                 }
                                                                                 Parameter {
                                                                                   f ->
                                                                                     {&a[def_exc:Unknown int([-63,63])], &a}
                                                                                 }
                                                                                 Temp {
                                                                                   tmp ->
                                                                                     {&a[def_exc:Unknown int([-63,63])], &a[def_exc:Unknown int([-63,63])], NULL, ?}
                                                                                 }
                                                                               }, mapping {
                                                                                      }, {}, {}),
           lifted node:Unknown node, Unit:()], mapping {
                                                 }) because Map: tmp =
 HoarePO: {a[def_exc:Unknown int([-63,63])], a, NULL, ?} not leq {a[def_exc:Unknown int([-63,63])], a[def_exc:Unknown int([-63,63])], NULL, ?}. 

It is a slightly different case than goblint/bench#7 where both address sets are (at least textually) the same, so there might be several issues here or one issues is manifesting itself differently.

[sim642]

I started looking into the minimized program and apparently it's a problem with the widening of address domain:

%%% ad: (tests/regression/02-base/71-ad.c:3:14-3:19)  widen {a[def_exc:1], a} {a[def_exc:Not {0}([0,7])]}
  %%% ad: -> {a[def_exc:Not {0}([0,7])], a[def_exc:Not {0}([0,7])]}