Fixpoint not reached in incremental analysis on some commits of chrony

[jerhard]

On chrony, when analyzing the commit a2372b0c3abfc85d11c1684c0fb6370cc329e5c4 non-incrementally, and analyzing the child commit 3cef7f975cd2ecdceb62c72dd31f96c515744acc incrementally, the fixpoint is not reached during the analysis of the child commit. This is with Goblint on the branch interactive_benchmarking (29d9c21).

Command line for non-incremental analysis of child-commit:

./goblint --conf conf/custom/figlet.json -v --disable incremental.load --enable incremental.save ../chrony 

Command line for incremental analysis of child commit:

./goblint --conf conf/custom/figlet.json -v --enable incremental.load --disable incremental.save ../chrony 

To build the compile db before the analysis, the following script must be run within the chrony directory:

#!/usr/bin/env bash
git clean -fdx
./configure
make -j 1 chronyd | tee build.log
compiledb --parse build.log

Message about not reached Fixpoint

Postsolving


[Warning][Unsound] No suitable function to be called at call site. Continuing with state before call. (chrony/sys_generic.c:305:5-305:66)
[Warning][Unsound] Unknown call to function *(ptr->handler). (chrony/local.c:633:6-633:46)
[Warning][Unsound] No suitable function to be called at call site. Continuing with state before call. (chrony/local.c:633:6-633:46)
[Warning][Unsound] Unknown call to function *(ptr->handler). (chrony/local.c:291:6-291:76)
[Warning][Unsound] No suitable function to be called at call site. Continuing with state before call. (chrony/local.c:291:6-291:76)
[Warning][Unsound] Unknown call to function *((inst->driver)->init). (chrony/refclock.c:247:7-247:54)
[Warning][Unsound] No suitable function to be called at call site. Continuing with state before call. (chrony/refclock.c:247:7-247:54)
[Warning][Unsound] No suitable function to be called at call site. Continuing with state before call. (chrony/socket.c:386:5-386:58)
[Warning][Unsound] No suitable function to be called at call site. Continuing with state before call. (chrony/sys_generic.c:149:3-149:45)
[Warning][Unsound] No suitable function to be called at call site. Continuing with state before call. (chrony/sys_generic.c:150:3-150:31)
Fixpoint not reached at entry state of LCL_CanSystemLeap (52620) on chrony/local.c:690:1-694:1
Origin: node 11617 "tmp___5" on chrony/reference.c:257:7-257:62
 Solver computed:
 bot
 Side-effect:
 {([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 {
                                                                             }, 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 {
                                                                                         }, mapping {
                                                                                              }, {}, ()),
                top or std * lifted node:(mapping {
                                            }, Unknown node), Unit:()], mapping {
                                                                          })} instead of bot
Fixpoint not reached at node 6859 "LCL_ReadRawTime(& raw);" on chrony/local.c:696:3-696:24
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
Fixpoint not reached at node 6858 "drv_set_leap" on chrony/local.c:693:3-693:30
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
Fixpoint not reached at node 6860 "LCL_GetOffsetCorrection(& raw, & correction,
                                                           (double *)((void *)0));" on chrony/local.c:697:3-697:50
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
Fixpoint not reached at node 6861 "LCL_AccumulateOffset(correction, 0.0);" on chrony/local.c:698:3-698:40
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
Fixpoint not reached at node 6862 "return;" on chrony/local.c:699:1-699:1
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
Fixpoint not reached at call of LCL_CanSystemLeap (52620) on chrony/local.c:690:1-694:1
 Solver computed:
 bot
 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 {
                                                                             Temp {
                                                                               RETURN ->
                                                                                 (Unknown int([0,1]),[0,1])
                                                                             }
                                                                           }, mapping {
                                                                                  }, {}, ()),
    top or std * lifted node:(mapping {
                                }, Unknown node), Unit:()], mapping {
                                                              })}
Fixpoint not reached at call of LCL_CanSystemLeap (52620) on chrony/local.c:690:1-694:1
 Solver computed:
 bot
 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 {
                                                                             Temp {
                                                                               RETURN ->
                                                                                 (Unknown int([0,1]),[0,1])
                                                                             }
                                                                           }, 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 {
                                                                                         Temp {
                                                                                           RETURN ->
                                                                                             (Unknown int([0,1]),[0,1])
                                                                                         }
                                                                                       }, mapping {
                                                                                              }, {}, ()),
                top or std * lifted node:(mapping {
                                            }, Unknown node), Unit:()], mapping {
                                                                          })} instead of bot

[jerhard]

The Dead code instead of bot that is produced here in the postsolver is noticeable. This occurs in 16 our of 18 commits for which the Fixpoint was not reached on chrony.

[jerhard]

A possibly different Fixpoint issue occurs on the same repo, with the same settings on the incremental analyis of the child commit on other commits of chrony. Here, the Dead code instead of bot does not appear. It may or may not relate to the same underlying problem.

Parent commit:
d69ac0718366995bdd50066723c746dc0f08f344

Child commit:
1b82604f615f5ac35992697c0bea8ba7092172d1

Fixpoint not reached message

Fixpoint not reached at node 3490 "return;" on chrony/conf.c:447:1-447:1
 Solver computed:
 {([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 {
                                                                             Global {
                                                                               include_level ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                             }
                                                                             Local {
                                                                               in ->
                                                                                 {?, NULL}
                                                                               i ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                             }
                                                                             Parameter {
                                                                               filename___0 ->
                                                                                 {?, NULL}
                                                                             }
                                                                             Temp {
                                                                               tmp ->
                                                                                 {?, NULL}
                                                                             }
                                                                           }, 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 {
                                                                             Global {
                                                                               print_config ->
                                                                                 (1,[1,1])
                                                                               include_level ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                             }
                                                                             Local {
                                                                               in ->
                                                                                 {?, NULL}
                                                                               i ->
                                                                                 (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                             }
                                                                             Parameter {
                                                                               filename___0 ->
                                                                                 {?, NULL}
                                                                             }
                                                                             Temp {
                                                                               tmp ->
                                                                                 {?, NULL}
                                                                             }
                                                                           }, 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 {
                                                                                        Global {
                                                                                          print_config ->
                                                                                            (1,[1,1])
                                                                                          include_level ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                        }
                                                                                        Local {
                                                                                          in ->
                                                                                            {?, NULL}
                                                                                          i ->
                                                                                            (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                        }
                                                                                        Parameter {
                                                                                          filename___0 ->
                                                                                            {?, NULL}
                                                                                        }
                                                                                        Temp {
                                                                                          tmp ->
                                                                                            {?, NULL}
                                                                                        }
                                                                                      }, mapping {
                                                                                             }, {}, ()),
               top or std * lifted node:(mapping {
                                           }, Unknown node), Unit:()], mapping {
                                                                         }):
 not leq ([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 {
                                                                                    Global {
                                                                                      include_level ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                    }
                                                                                    Local {
                                                                                      in ->
                                                                                        {?, NULL}
                                                                                      i ->
                                                                                        (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                    }
                                                                                    Parameter {
                                                                                      filename___0 ->
                                                                                        {?, NULL}
                                                                                    }
                                                                                    Temp {
                                                                                      tmp ->
                                                                                        {?, NULL}
                                                                                    }
                                                                                  }, mapping {
                                                                                         }, {}, ()),
           top or std * lifted node:(mapping {
                                       }, Unknown node), Unit:()], mapping {
                                                                     }) because Map: print_config =
 compound: (1,[1,1]) not same type as Uninitialized.