search

marek-trtik / cbmc

C Bounded Model Checker
http://www.cprover.org/cbmc
Other
0 stars 0 forks source link

18 red memsafety benchmarks #22

Closed marek-trtik closed 6 years ago

marek-trtik commented 6 years ago

Here are the 18 benchmarks for which CBMC returns wrong result:

            "ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i",
            "busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i",
            "busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/whoami-incomplete_true-no-overflow_true-valid-memsafety.i",
            "busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i",
marek-trtik commented 6 years ago

This benchmark is fixed: ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i see commit: https://github.com/marek-trtik/cbmc/commit/db218c2a6df9302196867c7cb8939e5582b50d0b

lucasccordeiro commented 6 years ago

As far as I remember, in the past we had problems about these busybox benchmarks in the competition due to undefined behaviour. We'll have to carefully debug them; unfortunately they are quite large benchmarks.

Previously, I think that CBMC used to fail with error messages like:

byte_update of unknown width:
byte_update_little_endian
  * type: array
      * size: symbol
          * type: unsignedbv
              * width: 64
              * #source_location: 
                * file: <built-in-additions>
                * line: 1
                * working_directory: /Users/lucasccordeiro/sv-benchmarks/c
              * #typedef: __CPROVER_size_t
              * #c_type: unsigned_long_int
          * identifier: symex_dynamic::dynamic_object_size8#1
...
marek-trtik commented 6 years ago

I fixed the issue (it was my fault) in this commit: https://github.com/marek-trtik/cbmc/commit/75b0171c9db364fd3e8c91a5775ccbd18e74fec0 So, CBMC does not return RED results. It either timeouts or terminates with an error, i.e. like in the past, as @lucasccordeiro mentioned.

marek-trtik commented 6 years ago

The problem of RED results was fixed => closing the issue.