Fixpoint not reached in some incremental runs on chrony

[jerhard]

Using the current master, 35 runs of the incremental analysis do not reach the fixpoint on chrony. This occurred with the regular incremental configuration. In all of the 35 runs, the unreached fixpoint is detected at the same code location within chrony.
In the experiments, it does not manifest in the runs where the incremental postsolver is active (with reluctant incremental analysis on or off).

Difference between rhs and computed solution.

Difference: Map: Reversed (top or Set (address (lval (offset (IntDomLifter(intdomtuple)))) * booleans)) * bottom or map:({}, mapping {
                                                                                                                                }) =
 Map: messages =
 trivial arrays: Array: mapping {
                          addr_type ->   Uninitialized
                          data ->   {}
                          descriptor ->   Uninitialized
                          if_index ->   Uninitialized
                          length ->   Uninitialized
                          local_addr ->
                            (If you see this, you are special!, Unknown)
                          remote_addr ->
                            (If you see this, you are special!, Unknown)
                          timestamp ->
                            mapping {
                              hw ->   mapping {
                                        tv_nsec ->   Uninitialized
                                        tv_sec ->   Uninitialized
                                      }
                              if_index ->   Uninitialized
                              kernel ->   mapping {
                                            tv_nsec ->   Uninitialized
                                            tv_sec ->   Uninitialized
                                          }
                              l2_length ->   Uninitialized
                              tx_flags ->   Uninitialized
                            }
                        } not leq Array: mapping {
                                             addr_type ->   Uninitialized
                                             data ->   {}
                                             descriptor ->   Uninitialized
                                             if_index ->   Uninitialized
                                             length ->   Uninitialized
                                             local_addr ->
                                               (If you see this, you are special!, Uninitialized)
                                             remote_addr ->
                                               (If you see this, you are special!, Uninitialized)
                                             timestamp ->
                                               mapping {
                                                 hw ->   mapping {
                                                           tv_nsec ->
                                                             Uninitialized
                                                           tv_sec ->
                                                             Uninitialized
                                                         }
                                                 if_index ->   Uninitialized
                                                 kernel ->   mapping {
                                                               tv_nsec ->
                                                                 Uninitialized
                                                               tv_sec ->
                                                                 Uninitialized
                                                             }
                                                 l2_length ->   Uninitialized
                                                 tx_flags ->   Uninitialized
                                               }
                                           }

[jerhard]

The fixpoint is not reached at a call:

Fixpoint not reached at L:node 47288 "received = SCK_ReceiveMessages(sock_fd,
                                                                     messages,
                                                                     4, flags);" on chrony/ntp_io.c:426:3-426:62

The line number chrony/ntp_io.c:426:3-426:62 is reported on this small commit, where the fixpoint issue also arises.

[jerhard]

The fixpoint is also not reached for this commit where only a function is added. Goblint accurately detects that only a function definition is added, and there are no evals recorded for this commit.

[jerhard]

@stilscher pointed out that this may have to do with anonymous types in C. Indeed, it turns out the type of local_addr is an anonymous union or anonymous struct (in the commits I've checked), see here: https://github.com/mlichvar/chrony/blob/934b8712a57e324581a15ddb4f6c84cd67a5673e/socket.h#L64-L66

Previously, there were similar fixpoint issues that were caused by different names and/or ckeys assigned to the anonymous types by CIL. This may be a similar issue.

[sim642]

Something about anonymous structs came up in #678 but maybe that aspect wasn't fixed?
I haven't looked into the details but maybe incremental comparison of struct types should ignore names of anonymous structs and consider them equal if the contents are?

[jerhard]

I had a look at the previously mentioned commit where only a function was added. For the parent commit of that commit, at the node, where the incremental analysis of the child does not reach the fixpoint, the solver computes local_addr -> (If you see this, you are special!, Uninitialized) as does the right-hand side in the postsolving.

From this, I would conclude for the child commit, that the right-hand-side that is not subsumed, that yields local_addr -> (If you see this, you are special!, Unknown), is the problem (rather than the solution not being accessed correctly). For the parent commit the computed solution subsumes the right-hand-side; and there are no relevant code changes that should change that fact.

Computed value in non-incremental run

{([Unit:(), Reversed (top or Set (varinfo)):{}, top or Set (Set (exp)):{},
    Reversed (top or Set (exp)):{}, Unit:(),
    Reversed (top or Set (address (lval (offset (IntDomLifter(intdomtuple)))) * booleans)) * bottom or map:({}, mapping {
                                                                                                                  }),
    Unit:(), Unit:(), top or Set (variables):{line}, booleans:False,
    MT mode:Multithreaded (main),
    lifted varinfo * node * chain option * Thread * lifted created (once) * created (multiple times) and Unit:(unknown node, main, ()),
    value domain * array partitioning deps * Vars with Weak Update * Unit:(mapping {
                                                                             Local {
                                                                               messages ->
                                                                                 (Array: mapping {
                                                                                           addr_type ->
                                                                                             Uninitialized
                                                                                           data ->
                                                                                             {}
                                                                                           descriptor ->
                                                                                             Uninitialized
                                                                                           if_index ->
                                                                                             Uninitialized
                                                                                           length ->
                                                                                             Uninitialized
                                                                                           local_addr ->
                                                                                             (If you see this, you are special!, Uninitialized)
                                                                                           remote_addr ->
                                                                                             (If you see this, you are special!, Uninitialized)
                                                                                           timestamp ->
                                                                                             mapping {
                                                                                               hw ->
                                                                                                 mapping {
                                                                                                   tv_nsec ->
                                                                                                     Uninitialized
                                                                                                   tv_sec ->
                                                                                                     Uninitialized
                                                                                                 }
                                                                                               if_index ->
                                                                                                 Uninitialized
                                                                                               kernel ->
                                                                                                 mapping {
                                                                                                   tv_nsec ->
                                                                                                     Uninitialized
                                                                                                   tv_sec ->
                                                                                                     Uninitialized
                                                                                                 }
                                                                                               l2_length ->
                                                                                                 Uninitialized
                                                                                               tx_flags ->
                                                                                                 Uninitialized
                                                                                             }
                                                                                         }, (4,[4,4]))
                                                                               i ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               received ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               flags ->
                                                                                 (Unknown int([0,1]),[0,1])
                                                                             }
                                                                             Parameter {
                                                                               sock_fd ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               event ->

[jerhard]

The first commit of Goblint in the recent past where Fixpoint appears for the output logs on a select subset of chrony-commits is the commit (8d22c45).

I still have to have a look whether there are other issues at the previous commit that may mask the issue in the previous commit (e.g. if more runs were failing due to other reasons).
Edit: It turns out that on the previous goblint commit (53938bc) all the incremental runs fail. This is due to the some reflifts that were still implemented via failwiths before.

Edit: With the parent commit of 53938bc, which is d025538, no fixpoint issue appears on the tested chrony commits.
So it seems that the issue manifested with 8d22c45 and 53938bc.

[jerhard]

Undoing the changes to the relift functions as in d34cd61ef00534cdd552e7a7ca9f83c544d5ce84 indeed leads to the Fixpoint warnings going away on the chrony commits tested.
Since the the relift functions were looking meaningful, it may be that reverting back justs hides the issue somehow. It may also be that the implementation of the relift in some of these places may have lead to inconsistencies compared to modules where the relifting is not done.

[michael-schwarz]

This morning @jerhard and I were able to narrow it down: It is the addition of relifting to the CPA, that causes the analysis to start failing. Curiously, CPA is HashCached, so that may have something to do with it.

[jerhard]

I removed the HashCached Lifter for the CPA, and the fixpoint issue remains.

[jerhard]

When deactivating the relift of arrays in ValueDomain.relift on the current master-branch, no fixpoints issues are reported on the tested chrony commits.

[michael-schwarz]

That is very strange: You said you are not using partitioned arrays, right?