Reluctant incremental Goblint does not reach fixpoint on some commits of chrony

[jerhard]

When performing a reluctant incremental analysis with Goblint (interactive_benchmarks, ee720d4) on some commits of chrony the reluctant incremental analysis does not reach the fixpoint.

The issue is potentially related to the treatment of functions with changed headers.

How to reproduce

Example on chrony, where the incremental does not reach a fixpoint:

Parent:
7a80647fb44a733ba5895898003376c319aea888

Command line:
./goblint --conf conf/custom/chrony.json -v --disable incremental.load --enable incremental.save ../chrony

Child (For Reluctant reanalysis):
5f4cbaab7e0e01c165fff657f2b53489c949fee4

Command line:

./goblint --conf conf/custom/chrony-incrpostsolver.json -v --enable incremental.load --disable incremental.save --enable incremental.reluctant.enabled ../chrony

Before each run of Goblint, the compile db has to be created in the chrony directory with this script.

Further Information

There are 38 cases on parent-child commit pairs on chrony where the reluctant incremental analysis has an unreached fixpoint. It is not easy to identify common characteristics of those commits that may give a hint whether some specific treatment is going wrong.
There are some cases the reluctant analysis fail where the header of a function is changed, but this does not apply to the (rather small) patch given in the example.

Analyzer log:
analyzer.log

Excerpt from unreached fixpoint:

Fixpoint not reached at node 69364 "(unsigned int )my_mode == 3U" on chrony/ntp_core.c:971:7-971:29
 Solver computed: [....]
[....] because {my_mode, my_mode}:
 not leq {0, smooth_time} because Set (exp): {my_mode, my_mode} not leq {0, smooth_time}
   because my_mode
 . 

[jerhard]

A reproducable case with the right Goblint version:

{"hash": "ff9301567e2702f2790bef14963975f99a96f766", "parent_hash": "e7a254265f0c26c80fa1c04beb9eb14064f97d2f", "CLOC": 22, "relCLOC": 22, "failed": true}

[sim642]

Set (exp): {my_mode, my_mode} not leq {0, smooth_time}

I believe these are var_eq analysis partitions, representing my_mode == my_mode and 0 == smooth_time. I see that the chrony conf makes var_eq context insensitive, which might have something to do with this.
The fact that there's an explicit identity partition seems odd. I guess if it were properly simplified away, the leq might hold.

[michael-schwarz]

Unfortunately, the same issue happens without var_eq as well.

[jerhard]

Commit with very minimal changes causing this:
{"hash": "1e727c4497dd028e4ea4f32fc3298e4bd580c68a", "parent_hash": "83010590af1e3a4e317d14747e5f643879701e45", "CLOC": 2, "relCLOC": 2, "failed": true}

[jerhard]

Another commit with rather small changes:
99e3c67a8104864300cebf58fdf6a7cece99c8c2
parent:
c4a2550518e19b0995ef143b44e7dabaa3851437

[jerhard]

Commit with very minimal changes causing this:
{"hash": "1e727c4497dd028e4ea4f32fc3298e4bd580c68a", "parent_hash": "83010590af1e3a4e317d14747e5f643879701e45", "CLOC": 2, "relCLOC": 2, "failed": true}

Looking at this with @stilscher, we found that for this commit, turning off the incremental postsolver did remove the warning about the unreached fixpoint. Maybe the problem is in the interplay between the reluctant analysis and the incremental postsolver.

Edit: Actually I am now not sure whether this was the only setting that was changed to make the issue disappear for this commit.

[jerhard]

I tried again deactivating some options, to see if there is an impact on the fixpoint issue. I now found that at least for one parent-child commit pair, the fixpoint is not reached in the child, even when changing some configurations regarding partial-contexts and deactivating the incremental postsolver.

On the commit pair:

PARENT=e7a254265f0c26c80fa1c04beb9eb14064f97d2f
CHILD=ff9301567e2702f2790bef14963975f99a96f766

with this configuration: chrony-incrpostsolver.txt (change file extension to .json for it to work; Github won't allow json files here)

where:

• ana.base.context.non-ptr: true
• var_eq is removed
• incremental.postsolver.enabled: false
• incremental.restart.write-only: false

The fixpoint is not reached.

First fixpoint warning for the reluctant run

Fixpoint not reached at node 92627 "si->lo_limit -= extra_disp;" on /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:668:7-668:33
 Solver computed:
 {([Unit:(), Reversed (top or Set (varinfo)):{}, Reversed (top or Set (exp)):{},
    Unit:(), Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(),
    Unit:(), top or Set (variables):{line}, booleans:False,
    MT mode:Multithreaded (main), Thread * lifted created and Unit:(main, ()),
    value domain * array partitioning deps * Vars with Weak Update * Unit:(mapping {
                                                                             Global {
                                                                               ((alloc@sid:93330@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:231:3-231:87) ->
                                                                                 (mapping {
                                                                                    active ->
                                                                                      (Unknown int([0,1]),[0,1])
                                                                                    distant ->
                                                                                      (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                    index ->
                                                                                      (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                    ip_addr ->
                                                                                      {NULL}
                                                                                    leap ->
                                                                                      (3,[3,3])
                                                                                    reachability ->
                                                                                      (0,[0,0])
                                                                                    reachability_size ->
                                                                                      (0,[0,0])
                                                                                    ref_id ->
                                                                                      (Unknown int([0,32]),[0,4294967295])
                                                                                    sel_info ->
                                                                                      mapping {
                                                                                        hi_limit ->
                                                                                          
                                                                                        last_sample_ago ->
                                                                                          
                                                                                        lo_limit ->
                                                                                          
                                                                                        root_distance ->
                                                                                          
                                                                                        select_ok ->
                                                                                          (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                        std_dev ->
                                                                                          
                                                                                        stratum ->
                                                                                          (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      }
                                                                                    sel_options ->
                                                                                      (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                    sel_score ->
                                                                                      
                                                                                    stats ->
                                                                                      {&((alloc@sid:92463@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sourcestats.c:215:3-215:79)}
                                                                                    status ->
                                                                                      (Unknown int([0,7]),[0,16])
                                                                                    type ->
                                                                                      (1,[1,1])
                                                                                    updates ->
                                                                                      (0,[0,0])
                                                                                  }, (120,[120,120]), true)
                                                                             }
                                                                             Local {
                                                                               si ->
                                                                                 {?, NULL, &((alloc@sid:93330@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:231:3-231:87).sel_info}
                                                                               now ->
                                                                                 mapping {
                                                                                   tv_nsec ->
                                                                                     (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                   tv_sec ->
                                                                                     (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                 }
                                                                               ref_time ->
                                                                                 mapping {
                                                                                   tv_nsec ->
                                                                                     (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                   tv_sec ->
                                                                                     (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                 }
                                                                               i ->
                                                                                 (Unknown int([-31,31]),[0,2147483646])
                                                                               j ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               j1___0 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               j2 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               index___0 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               sel_prefer ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               n_endpoints ->
                                                                                 (0,[0,0])
                                                                               n_sel_sources ->
                                                                                 (0,[0,0])
                                                                               sel_req_source ->
                                                                                 (Unknown int([0,1]),[0,2147483647])
                                                                               n_badstats_sources ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               max_sel_reach ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               max_sel_reach_size ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               max_badstat_reach ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               depth ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               best_depth ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               trust_depth ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               best_trust_depth ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               combined ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               stratum ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               min_stratum ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               max_score_index ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               orphan_stratum ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               orphan_source ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               leap_votes ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               leap_ins ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               leap_del ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               src_offset ->
                                                                                 
                                                                               src_offset_sd ->
                                                                                 
                                                                               src_frequency ->
                                                                                 
                                                                               src_frequency_sd ->
                                                                                 
                                                                               src_skew ->
                                                                                 
                                                                               src_root_delay ->
                                                                                 
                                                                               src_root_dispersion ->
                                                                                 
                                                                               best_lo ->
                                                                                 
                                                                               best_hi ->
                                                                                 
                                                                               distance ->
                                                                                 
                                                                               sel_src_distance ->
                                                                                 
                                                                               max_score ->
                                                                                 
                                                                               first_sample_ago ->
                                                                                 
                                                                               max_reach_sample_ago ->
                                                                                 
                                                                               leap_status ->
                                                                                 Unknown
                                                                               extra_disp ->
                                                                                 
                                                                               local_ref_id ->
                                                                                 (Unknown int([0,32]),[0,4294967295])
                                                                             }
                                                                             Parameter {
                                                                               updated_inst ->
                                                                                 {?, NULL, &((alloc@sid:27859@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:229:3-229:87)}
                                                                             }
                                                                             Temp {
                                                                               tmp ->
                                                                                 
                                                                               tmp___0 ->
                                                                                 (Unknown int([0,32]),[0,4294967295])
                                                                               tmp___1 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               tmp___2 ->
                                                                                 {?, NULL}
                                                                               tmp___3 ->
                                                                                 {?, NULL}
                                                                               tmp___4 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               tmp___5 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               tmp___6 ->
                                                                                 (Unknown int([0,32]),[0,4294967295])
                                                                               tmp___7 ->
                                                                                 {?, NULL}
                                                                             }
                                                                           }, mapping {
                                                                                  }, {}, ()),
    top or std * lifted node:(mapping {
                                }, Unknown node), Unit:()], mapping {
                                                              })}
 Right-Hand-Side:
 {([Unit:(), Reversed (top or Set (varinfo)):{}, Reversed (top or Set (exp)):{},
    Unit:(), Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(),
    Unit:(), top or Set (variables):{line}, booleans:False,
    MT mode:Multithreaded (main), Thread * lifted created and Unit:(main, ()),
    value domain * array partitioning deps * Vars with Weak Update * Unit:(mapping {
                                                                             Global {
                                                                               ((alloc@sid:93330@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:231:3-231:87) ->
                                                                                 (mapping {
                                                                                    active ->
                                                                                      (Unknown int([0,1]),[0,1])
                                                                                    distant ->
                                                                                      (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                    index ->
                                                                                      (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                    ip_addr ->
                                                                                      {NULL}
                                                                                    leap ->
                                                                                      (Unknown int([0,32]),[0,4294967295])
                                                                                    reachability ->
                                                                                      (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                    reachability_size ->
                                                                                      (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                    ref_id ->
                                                                                      (Unknown int([0,32]),[0,4294967295])
                                                                                    sel_info ->
                                                                                      mapping {
                                                                                        hi_limit ->
                                                                                          
                                                                                        last_sample_ago ->
                                                                                          
                                                                                        lo_limit ->
                                                                                          
                                                                                        root_distance ->
                                                                                          
                                                                                        select_ok ->
                                                                                          (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                        std_dev ->
                                                                                          
                                                                                        stratum ->
                                                                                          (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      }
                                                                                    sel_options ->
                                                                                      (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                    sel_score ->
                                                                                      
                                                                                    stats ->
                                                                                      {&((alloc@sid:92463@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sourcestats.c:215:3-215:79)}
                                                                                    status ->
                                                                                      (Unknown int([0,7]),[0,16])
                                                                                    type ->
                                                                                      (1,[1,1])
                                                                                    updates ->
                                                                                      (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                  }, (120,[120,120]), true)
                                                                             }
                                                                             Local {
                                                                               si ->
                                                                                 {?, NULL, &((alloc@sid:93330@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:231:3-231:87).sel_info}
                                                                               now ->
                                                                                 mapping {
                                                                                   tv_nsec ->
                                                                                     (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                   tv_sec ->
                                                                                     (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                 }
                                                                               ref_time ->
                                                                                 mapping {
                                                                                   tv_nsec ->
                                                                                     (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                   tv_sec ->
                                                                                     (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                 }
                                                                               i ->
                                                                                 (Unknown int([-31,31]),[0,2147483646])
                                                                               j ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               j1___0 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               j2 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               index___0 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               sel_prefer ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               n_endpoints ->
                                                                                 (0,[0,0])
                                                                               n_sel_sources ->
                                                                                 (0,[0,0])
                                                                               sel_req_source ->
                                                                                 (Unknown int([0,1]),[0,2147483647])
                                                                               n_badstats_sources ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               max_sel_reach ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               max_sel_reach_size ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               max_badstat_reach ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               depth ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               best_depth ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               trust_depth ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               best_trust_depth ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               combined ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               stratum ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               min_stratum ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               max_score_index ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               orphan_stratum ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               orphan_source ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               leap_votes ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               leap_ins ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               leap_del ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               src_offset ->
                                                                                 
                                                                               src_offset_sd ->
                                                                                 
                                                                               src_frequency ->
                                                                                 
                                                                               src_frequency_sd ->
                                                                                 
                                                                               src_skew ->
                                                                                 
                                                                               src_root_delay ->
                                                                                 
                                                                               src_root_dispersion ->
                                                                                 
                                                                               best_lo ->
                                                                                 
                                                                               best_hi ->
                                                                                 
                                                                               distance ->
                                                                                 
                                                                               sel_src_distance ->
                                                                                 
                                                                               max_score ->
                                                                                 
                                                                               first_sample_ago ->
                                                                                 
                                                                               max_reach_sample_ago ->
                                                                                 
                                                                               leap_status ->
                                                                                 Unknown
                                                                               extra_disp ->
                                                                                 
                                                                               local_ref_id ->
                                                                                 (Unknown int([0,32]),[0,4294967295])
                                                                             }
                                                                             Parameter {
                                                                               updated_inst ->
                                                                                 {?, NULL, &((alloc@sid:27859@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:229:3-229:87)}
                                                                             }
                                                                             Temp {
                                                                               tmp ->
                                                                                 
                                                                               tmp___0 ->
                                                                                 (Unknown int([0,32]),[0,4294967295])
                                                                               tmp___1 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               tmp___2 ->
                                                                                 {?, NULL}
                                                                               tmp___3 ->
                                                                                 {?, NULL}
                                                                               tmp___4 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               tmp___5 ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                               tmp___6 ->
                                                                                 (Unknown int([0,32]),[0,4294967295])
                                                                               tmp___7 ->
                                                                                 {?, NULL}
                                                                             }
                                                                           }, mapping {
                                                                                  }, {}, ()),
    top or std * lifted node:(mapping {
                                }, Unknown node), Unit:()], mapping {
                                                              })}
 Difference: ([Unit:(), Reversed (top or Set (varinfo)):{},
               Reversed (top or Set (exp)):{}, Unit:(),
               Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(),
               Unit:(), top or Set (variables):{line}, booleans:False,
               MT mode:Multithreaded (main),
               Thread * lifted created and Unit:(main, ()),
               value domain * array partitioning deps * Vars with Weak Update * Unit:(mapping {
                                                                                        Global {
                                                                                          ((alloc@sid:93330@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:231:3-231:87) ->
                                                                                            (mapping {
                                                                                               active ->
                                                                                                 (Unknown int([0,1]),[0,1])
                                                                                               distant ->
                                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                               index ->
                                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                               ip_addr ->
                                                                                                 {NULL}
                                                                                               leap ->
                                                                                                 (Unknown int([0,32]),[0,4294967295])
                                                                                               reachability ->
                                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                               reachability_size ->
                                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                               ref_id ->
                                                                                                 (Unknown int([0,32]),[0,4294967295])
                                                                                               sel_info ->
                                                                                                 mapping {
                                                                                                   hi_limit ->
                                                                                                     
                                                                                                   last_sample_ago ->
                                                                                                     
                                                                                                   lo_limit ->
                                                                                                     
                                                                                                   root_distance ->
                                                                                                     
                                                                                                   select_ok ->
                                                                                                     (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                   std_dev ->
                                                                                                     
                                                                                                   stratum ->
                                                                                                     (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                 }
                                                                                               sel_options ->
                                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                               sel_score ->
                                                                                                 
                                                                                               stats ->
                                                                                                 {&((alloc@sid:92463@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sourcestats.c:215:3-215:79)}
                                                                                               status ->
                                                                                                 (Unknown int([0,7]),[0,16])
                                                                                               type ->
                                                                                                 (1,[1,1])
                                                                                               updates ->
                                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                             }, (120,[120,120]), true)
                                                                                        }
                                                                                        Local {
                                                                                          si ->
                                                                                            {?, NULL, &((alloc@sid:93330@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:231:3-231:87).sel_info}
                                                                                          now ->
                                                                                            mapping {
                                                                                              tv_nsec ->
                                                                                                (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                              tv_sec ->
                                                                                                (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                            }
                                                                                          ref_time ->
                                                                                            mapping {
                                                                                              tv_nsec ->
                                                                                                (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                              tv_sec ->
                                                                                                (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                            }
                                                                                          i ->
                                                                                            (Unknown int([-31,31]),[0,2147483646])
                                                                                          j ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          j1___0 ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          j2 ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          index___0 ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          sel_prefer ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          n_endpoints ->
                                                                                            (0,[0,0])
                                                                                          n_sel_sources ->
                                                                                            (0,[0,0])
                                                                                          sel_req_source ->
                                                                                            (Unknown int([0,1]),[0,2147483647])
                                                                                          n_badstats_sources ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          max_sel_reach ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          max_sel_reach_size ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          max_badstat_reach ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          depth ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          best_depth ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          trust_depth ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          best_trust_depth ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          combined ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          stratum ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          min_stratum ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          max_score_index ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          orphan_stratum ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          orphan_source ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          leap_votes ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          leap_ins ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          leap_del ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          src_offset ->
                                                                                            
                                                                                          src_offset_sd ->
                                                                                            
                                                                                          src_frequency ->
                                                                                            
                                                                                          src_frequency_sd ->
                                                                                            
                                                                                          src_skew ->
                                                                                            
                                                                                          src_root_delay ->
                                                                                            
                                                                                          src_root_dispersion ->
                                                                                            
                                                                                          best_lo ->
                                                                                            
                                                                                          best_hi ->
                                                                                            
                                                                                          distance ->
                                                                                            
                                                                                          sel_src_distance ->
                                                                                            
                                                                                          max_score ->
                                                                                            
                                                                                          first_sample_ago ->
                                                                                            
                                                                                          max_reach_sample_ago ->
                                                                                            
                                                                                          leap_status ->
                                                                                            Unknown
                                                                                          extra_disp ->
                                                                                            
                                                                                          local_ref_id ->
                                                                                            (Unknown int([0,32]),[0,4294967295])
                                                                                        }
                                                                                        Parameter {
                                                                                          updated_inst ->
                                                                                            {?, NULL, &((alloc@sid:27859@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:229:3-229:87)}
                                                                                        }
                                                                                        Temp {
                                                                                          tmp ->
                                                                                            
                                                                                          tmp___0 ->
                                                                                            (Unknown int([0,32]),[0,4294967295])
                                                                                          tmp___1 ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          tmp___2 ->
                                                                                            {?, NULL}
                                                                                          tmp___3 ->
                                                                                            {?, NULL}
                                                                                          tmp___4 ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          tmp___5 ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                          tmp___6 ->
                                                                                            (Unknown int([0,32]),[0,4294967295])
                                                                                          tmp___7 ->
                                                                                            {?, NULL}
                                                                                        }
                                                                                      }, mapping {
                                                                                             }, {}, ()),
               top or std * lifted node:(mapping {
                                           }, Unknown node), Unit:()], mapping {
                                                                         }):
 not leq ([Unit:(), Reversed (top or Set (varinfo)):{},
           Reversed (top or Set (exp)):{}, Unit:(),
           Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), Unit:(),
           top or Set (variables):{line}, booleans:False,
           MT mode:Multithreaded (main),
           Thread * lifted created and Unit:(main, ()),
           value domain * array partitioning deps * Vars with Weak Update * Unit:(mapping {
                                                                                    Global {
                                                                                      ((alloc@sid:93330@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:231:3-231:87) ->
                                                                                        (mapping {
                                                                                           active ->
                                                                                             (Unknown int([0,1]),[0,1])
                                                                                           distant ->
                                                                                             (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                           index ->
                                                                                             (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                           ip_addr ->
                                                                                             {NULL}
                                                                                           leap ->
                                                                                             (3,[3,3])
                                                                                           reachability ->
                                                                                             (0,[0,0])
                                                                                           reachability_size ->
                                                                                             (0,[0,0])
                                                                                           ref_id ->
                                                                                             (Unknown int([0,32]),[0,4294967295])
                                                                                           sel_info ->
                                                                                             mapping {
                                                                                               hi_limit ->
                                                                                                 
                                                                                               last_sample_ago ->
                                                                                                 
                                                                                               lo_limit ->
                                                                                                 
                                                                                               root_distance ->
                                                                                                 
                                                                                               select_ok ->
                                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                               std_dev ->
                                                                                                 
                                                                                               stratum ->
                                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                             }
                                                                                           sel_options ->
                                                                                             (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                           sel_score ->
                                                                                             
                                                                                           stats ->
                                                                                             {&((alloc@sid:92463@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sourcestats.c:215:3-215:79)}
                                                                                           status ->
                                                                                             (Unknown int([0,7]),[0,16])
                                                                                           type ->
                                                                                             (1,[1,1])
                                                                                           updates ->
                                                                                             (0,[0,0])
                                                                                         }, (120,[120,120]), true)
                                                                                    }
                                                                                    Local {
                                                                                      si ->
                                                                                        {?, NULL, &((alloc@sid:93330@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:231:3-231:87).sel_info}
                                                                                      now ->
                                                                                        mapping {
                                                                                          tv_nsec ->
                                                                                            (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                          tv_sec ->
                                                                                            (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                        }
                                                                                      ref_time ->
                                                                                        mapping {
                                                                                          tv_nsec ->
                                                                                            (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                          tv_sec ->
                                                                                            (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])
                                                                                        }
                                                                                      i ->
                                                                                        (Unknown int([-31,31]),[0,2147483646])
                                                                                      j ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      j1___0 ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      j2 ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      index___0 ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      sel_prefer ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      n_endpoints ->
                                                                                        (0,[0,0])
                                                                                      n_sel_sources ->
                                                                                        (0,[0,0])
                                                                                      sel_req_source ->
                                                                                        (Unknown int([0,1]),[0,2147483647])
                                                                                      n_badstats_sources ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      max_sel_reach ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      max_sel_reach_size ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      max_badstat_reach ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      depth ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      best_depth ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      trust_depth ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      best_trust_depth ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      combined ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      stratum ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      min_stratum ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      max_score_index ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      orphan_stratum ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      orphan_source ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      leap_votes ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      leap_ins ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      leap_del ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      src_offset ->
                                                                                        
                                                                                      src_offset_sd ->
                                                                                        
                                                                                      src_frequency ->
                                                                                        
                                                                                      src_frequency_sd ->
                                                                                        
                                                                                      src_skew ->
                                                                                        
                                                                                      src_root_delay ->
                                                                                        
                                                                                      src_root_dispersion ->
                                                                                        
                                                                                      best_lo ->
                                                                                        
                                                                                      best_hi ->
                                                                                        
                                                                                      distance ->
                                                                                        
                                                                                      sel_src_distance ->
                                                                                        
                                                                                      max_score ->
                                                                                        
                                                                                      first_sample_ago ->
                                                                                        
                                                                                      max_reach_sample_ago ->
                                                                                        
                                                                                      leap_status ->
                                                                                        Unknown
                                                                                      extra_disp ->
                                                                                        
                                                                                      local_ref_id ->
                                                                                        (Unknown int([0,32]),[0,4294967295])
                                                                                    }
                                                                                    Parameter {
                                                                                      updated_inst ->
                                                                                        {?, NULL, &((alloc@sid:27859@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:229:3-229:87)}
                                                                                    }
                                                                                    Temp {
                                                                                      tmp ->
                                                                                        
                                                                                      tmp___0 ->
                                                                                        (Unknown int([0,32]),[0,4294967295])
                                                                                      tmp___1 ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      tmp___2 ->
                                                                                        {?, NULL}
                                                                                      tmp___3 ->
                                                                                        {?, NULL}
                                                                                      tmp___4 ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      tmp___5 ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                      tmp___6 ->
                                                                                        (Unknown int([0,32]),[0,4294967295])
                                                                                      tmp___7 ->
                                                                                        {?, NULL}
                                                                                    }
                                                                                  }, mapping {
                                                                                         }, {}, ()),
           top or std * lifted node:(mapping {
                                       }, Unknown node), Unit:()], mapping {
                                                                     }) because Map: ((alloc@sid:93330@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:231:3-231:87) =
 {Map: leap = (Unknown int([0,32]),[0,4294967295]) instead of (3,[3,3])
  Map: reachability =
  (Unknown int([-31,31]),[-2147483648,2147483647]) instead of (0,[0,0])
  Map: reachability_size =
  (Unknown int([-31,31]),[-2147483648,2147483647]) instead of (0,[0,0])
  Map: updates =
  (Unknown int([-31,31]),[-2147483648,2147483647]) instead of (0,[0,0]) ...}. 

[jerhard]

Here is a script that can be run to automatically execute the steps to run Goblint on the parent and child commit. The script assumes to be executed from a sibling folder of chrony and analyzer.

[jerhard]

I changed the implementation in td3 that calls the postsolver with

      Post.post st (!reluctant_vs @ vs) rho;

to instead only append !reluctant_vs if the incremental postsolver is on.

      let additional_vars =
        if GobConfig.get_bool "incremental.postsolver.enabled" then !reluctant_vs else []
      in
      Post.post st (additional_vars @ vs) rho;

I then ran with the non-incremental postsolver, and the fixpoint issue did not show up for commits: PARENT=e7a254265f0c26c80fa1c04beb9eb14064f97d2f
CHILD=ff9301567e2702f2790bef14963975f99a96f766.

I am not sure though whether the non-incremental postsolver then does all the necessary checks or whether it then is missing some checks.

[sim642]

The non-incremental postsolver always does a full pass, so it should be checking everything necessary and emitting also all the reached warnings.

Although it's surprising that reluctant_vs would be the problem because they are reluctant variables, which are not destabilized, so the check should still pass for them.
Or maybe it's somehow related to cheap_full_reach, which also uses reluctant_vs and already is conditional on incr_verify.

[jerhard]

I looked again at the small commit which is now easier to debug, thanks to @stilscher 's patch to the compile db script for chrony. (It avoids that some macro in chrony's config.h is set differently after each configure.)

Analyzing the chlid commit with reluctant analysis, the postsolver reports that the fixpoint is not reached.

Earlier in the output, the following is reported about the reluctant solving phase :

Separately solving changed functions...
test for call of SRC_ResetInstance (27025)
in infl after solving: node 27777 "n_sources ++;"
Destabilization not required...
test for call of SRC_ResetInstance (27025)
in infl after solving: node 57320 "! ntp_only"
Destabilization not required...
test for call of SRC_CreateNewInstance (27019)
Further destabilization happened ...
Final solve...

The function SRC_ResetInstance is analyzed reluctantly (twice, for different calling contexts), and for both instances no destabilization is required. Thus, they are added to reluctant_vs.

Then, the function SRC_CreateNewInstance is analyzed reluctantly, but further destabilization was required.

Later, the (non-incremental) postsolver reports that the fixpoint is not reached for the return node of SRC_ResetInstance. No fixpoint issue is reported when !reluctant is not passed to the postsolver.

My hypothesis is that the calls to SRC_ResetInstance that were reluctantly analyzed are actually no longer reachable, and that the solver did not compute a fixpoint for them. This would explain why the (non-incremental) postsolver does not complain when reluctant_vs is not explicitly passed to it.

Reluctant solving

change_info = { unchanged = 8052; changed = 2; added = 0; removed = 0 }
Completely changed function: SRC_ResetInstance
Completely changed function: SRC_CreateNewInstance
Removing data for changed and removed functions...
Data after clean-up:
|rho|=62455
|stable|=62455
|infl|=58902
|wpoint|=0
|side_dep|=12297
|side_infl|=32750
|var_messages|=4
|rho_write|=26217
|dep|=49949
Separately solving changed functions...
test for call of SRC_ResetInstance (27025)
in infl after solving: node 27777 "n_sources ++;"
Destabilization not required...
test for call of SRC_ResetInstance (27025)
in infl after solving: node 57320 "! ntp_only"
Destabilization not required...
test for call of SRC_CreateNewInstance (27019)
Further destabilization happened ...
Final solve...

[.... omitted ... ]

Fixpoint

!reluctant_vs:
call of SRC_ResetInstance (27025) on /home/julian/Entwicklung/Programm_Analyse/chrony/sources.h:74:13-74:53
call of SRC_ResetInstance (27025) on /home/julian/Entwicklung/Programm_Analyse/chrony/sources.h:74:13-74:53
end of !reluctant_vs
Postsolving

Fixpoint not reached at node 89460 "return;" on /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:303:1-303:1
 Solver computed:
 {([Unit:(), Reversed (top or Set (varinfo)):{},
    top or Set (Set (exp)):{{result, instance}}, Reversed (top or Set (exp)):{},
    Unit:(), Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(),
    Unit:(), top or Set (variables):{line}, booleans:False,
    MT mode:Singlethreaded, Thread * lifted created and Unit:(main, bot),
    value domain * array partitioning deps * Vars with Weak Update * Unit:(mapping {
                                                                             Parameter {
                                                                               instance ->
                                                                                 {&((alloc@sid:27747@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:229:3-229:87)}
                                                                             }
                                                                           }, mapping {
                                                                                  }, {}, ()),
    top or std * lifted node:(mapping {
                                }, Unknown node), Unit:()], mapping {
                                                              })}
 Right-Hand-Side:
 {([Unit:(), Reversed (top or Set (varinfo)):{}, top or Set (Set (exp)):{},
    Reversed (top or Set (exp)):{}, Unit:(),
    Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), Unit:(),
    top or Set (variables):{line}, booleans:False, MT mode:Singlethreaded,
    Thread * lifted created and Unit:(main, bot),
    value domain * array partitioning deps * Vars with Weak Update * Unit:(mapping {
                                                                             Parameter {
                                                                               instance ->
                                                                                 {&((alloc@sid:27747@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:229:3-229:87)}
                                                                             }
                                                                           }, mapping {
                                                                                  }, {}, ()),
    top or std * lifted node:(mapping {
                                }, Unknown node), Unit:()], mapping {
                                                              })}
 Difference: ([Unit:(), Reversed (top or Set (varinfo)):{},
               top or Set (Set (exp)):{}, Reversed (top or Set (exp)):{},
               Unit:(), Reversed (top or Set (Normal Lvals * booleans)):{},
               Unit:(), Unit:(), top or Set (variables):{line}, booleans:False,
               MT mode:Singlethreaded,
               Thread * lifted created and Unit:(main, bot),
               value domain * array partitioning deps * Vars with Weak Update * Unit:(mapping {
                                                                                        Parameter {
                                                                                          instance ->
                                                                                            {&((alloc@sid:27747@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:229:3-229:87)}
                                                                                        }
                                                                                      }, mapping {
                                                                                             }, {}, ()),
               top or std * lifted node:(mapping {
                                           }, Unknown node), Unit:()], mapping {
                                                                         }):
 not leq ([Unit:(), Reversed (top or Set (varinfo)):{},
           top or Set (Set (exp)):{{result, instance}},
           Reversed (top or Set (exp)):{}, Unit:(),
           Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), Unit:(),
           top or Set (variables):{line}, booleans:False,
           MT mode:Singlethreaded, Thread * lifted created and Unit:(main, bot),
           value domain * array partitioning deps * Vars with Weak Update * Unit:(mapping {
                                                                                    Parameter {
                                                                                      instance ->
                                                                                        {&((alloc@sid:27747@tid:main(#top)), /home/julian/Entwicklung/Programm_Analyse/chrony/sources.c:229:3-229:87)}
                                                                                    }
                                                                                  }, mapping {
                                                                                         }, {}, ()),
           top or std * lifted node:(mapping {
                                       }, Unknown node), Unit:()], mapping {
                                                                     }) because {result, instance}:
 .```

</summary>

[jerhard]

My hypothesis is that the calls to SRC_ResetInstance that were reluctantly analyzed are actually no longer reachable, and that the solver did not compute a fixpoint for them. This would explain why the (non-incremental) postsolver does not complain when reluctant_vs is not explicitly passed to it.

I think it should work to only pass those unknowns from !reluctant_vs to the postsolver that are stable.