False invariants in correctness witnesses generated by Goblint

[jprotopopov-ut]

This issue will be used to report false invariants contained in Goblint witnesses, as discovered by https://github.com/sws-lab/clang-witness-inject tool. Most of the issues are seemingly arbitrary, so I won't open separate ticket per each. The tool purpose is instrumenting program source code with assertions taken from correctness witnesses, and validating the assertions via compiling and running the program.

False invariants

• Program: https://github.com/goblint/bench/blob/master/concrat/Remotery/main.c
  Goblint revision: nightly sha256:454ed1481fd6d78e45ed0e58e458f5a32312491f2552535b5cf18e2077447a2d
  Configuration: --conf /opt/goblint/analyzer/share/goblint/conf/examples/large-program.json --enable witness.yaml.enabled
  Problematic invariant:

  - invariant:
      type: location_invariant
      location:
        file_name: main.c
        line: 1538
        column: 3
        function: strncat_s_safe_c
      value: dmax == 64U
      format: c_expression

• Program: https://github.com/goblint/bench/blob/master/concrat/lmdb/main.c
  Goblint revision and configuration: see above
  Problematic invariant:

  - invariant:
      type: location_invariant
      location:
        file_name: main.c
        line: 4103
        column: 5
        function: mdb_env_close
      value: dp == 0
      format: c_expression

False invariants while Function definition missing error appears

For the following program, Goblint produced false invariant(s) while issuing Function definition missing error. For completeness, I am documenting such cases too:

• Program: https://github.com/goblint/bench/blob/master/concrat/pigz/main.c
  Goblint revision and configuration: see above
  Problematic invariant:

  - invariant:
      type: location_invariant
      location:
        file_name: main.c
        line: 8929
        column: 3
        function: twist_
      value: # Value omitted for brevity
      format: c_expression

Other issues

Furthermore, there are multiple programs for which Goblint (revision and config as above) fails with the error Fatal error: exception Cilfacade.TypeOfError(typeOffset: Index on a non-array (0, struct __anonstruct_conn_t_702709736 )). In particular, axel, per-thread-array-join-counter

[jprotopopov-ut]

• Program: https://github.com/goblint/bench/blob/master/concrat/race-challenges/value-barrier.c
  Goblint configuration: --conf /opt/goblint/analyzer/share/goblint/conf/examples/very-precise.json --enable witness.yaml.enable
  Problematic invariant:

  - invariant:
      type: loop_invariant
      location:
        file_name: main.c
        line: 21
        column: 3
        function: thread
      value: 1LL >= (long long )ready + (long long )data
      format: c_expression

[jprotopopov-ut]

• Program: https://github.com/goblint/bench/blob/master/concrat/dnspod-sr/main.c
  Goblint revision: sha256:ed1f50204365b64d8e35626c44e2a44ad2cbef3733c9f998113081b202b756c1
  Goblint configuration: --conf /opt/goblint/analyzer/share/goblint/conf/examples/large-program.json

Fatal error: exception Cilfacade.TypeOfError(typeOffset: Index on a non-array ((long )"any_index", struct hdata ))

[jprotopopov-ut]

• Program https://github.com/goblint/bench/blob/master/concrat/level-ip/main.c
  Goblint revision and configuration: see above

Fatal error: exception Cilfacade.TypeOfError(typeOffset: Index on a non-array (0, struct timer ))

[michael-schwarz]

You might try to see if you can create a workflow involving creduce (https://github.com/csmith-project/creduce) to try to minimize these examples...

With such a minimal reproducible example, it would also be easier to reproduce and fix.

[jprotopopov-ut]

You might try to see if you can create a workflow involving creduce (https://github.com/csmith-project/creduce) to try to minimize these examples...

With such a minimal reproducible example, it would also be easier to reproduce and fix.

At the moment, my concern was simply documenting Goblint issues that I had discovered during testing of my tool. None of the reported bugs are critical as of now. As I work on the tool, I will probably continue updating this ticket with new findings, and later everything can be minimized in batches. Although, I believe the Index on a non-array error warrants a separate ticket already, because it has nothing to do with witnesses and was observed multiple times.