Incorrect TRUE for warning: ignoring bswap

[lucasccordeiro]

./cbmc --graphml-witness witness.graphml --64 --propertyfile ../../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---net--netfilter--nfnetlink_log.ko_false-unreach-call.cil.c

Passing problem to propositional reduction
converting SSA
warning: ignoring bswap
  * type: unsignedbv
      * width: 32
      * #c_type: unsigned_int
  * #source_location: 
    * file: ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---net--netfilter--nfnetlink_log.ko_false-unreach-call.cil.c
    * line: 7012
    * function: __fswab32
    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_100fb440-a49d-470a-945c-070576e16c64/bin-2018/cbmc
  0: symbol
      * type: unsignedbv
          * width: 32
          * #c_type: unsigned_int
      * identifier: __fswab32::val!0@1#1
      * expression: symbol
          * type: unsignedbv
              * width: 32
              * #c_type: unsigned_int
          * identifier: __fswab32::val
      * L0: 0
      * L1: 1
      * L2: 1
      * L1_object_identifier: __fswab32::val!0@1
      * #SSA_symbol: 1
warning: ignoring bswap
  * type: unsignedbv
      * width: 32
      * #c_type: unsigned_int
  * #source_location: 
    * file: ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---net--netfilter--nfnetlink_log.ko_false-unreach-call.cil.c
    * line: 7012
    * function: __fswab32
    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_100fb440-a49d-470a-945c-070576e16c64/bin-2018/cbmc
  0: symbol
      * type: unsignedbv
          * width: 32
          * #c_type: unsigned_int
      * identifier: __fswab32::val!0@2#1
      * expression: symbol
          * type: unsignedbv
              * width: 32
              * #c_type: unsigned_int
          * identifier: __fswab32::val
      * L0: 0
      * L1: 2
      * L2: 1
      * L1_object_identifier: __fswab32::val!0@2
      * #SSA_symbol: 1
warning: ignoring bswap
  * type: unsignedbv
      * width: 32
      * #c_type: unsigned_int
  * #source_location: 
    * file: ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---net--netfilter--nfnetlink_log.ko_false-unreach-call.cil.c
    * line: 7012
    * function: __fswab32
    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_100fb440-a49d-470a-945c-070576e16c64/bin-2018/cbmc
  0: symbol
      * type: unsignedbv
          * width: 32
          * #c_type: unsigned_int
      * identifier: __fswab32::val!0@3#1
      * expression: symbol
          * type: unsignedbv
              * width: 32
              * #c_type: unsigned_int
          * identifier: __fswab32::val
      * L0: 0
      * L1: 3
      * L2: 1
      * L1_object_identifier: __fswab32::val!0@3
      * #SSA_symbol: 1
warning: ignoring bswap
  * type: unsignedbv
      * width: 32
      * #c_type: unsigned_int
  * #source_location: 
    * file: ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---net--netfilter--nfnetlink_log.ko_false-unreach-call.cil.c
    * line: 7012
    * function: __fswab32
    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_100fb440-a49d-470a-945c-070576e16c64/bin-2018/cbmc
  0: symbol
      * type: unsignedbv
          * width: 32
          * #c_type: unsigned_int
      * identifier: __fswab32::val!0@4#1
      * expression: symbol
          * type: unsignedbv
              * width: 32
              * #c_type: unsigned_int
          * identifier: __fswab32::val
      * L0: 0
      * L1: 4
      * L2: 1
      * L1_object_identifier: __fswab32::val!0@4
      * #SSA_symbol: 1
warning: ignoring bswap
  * type: unsignedbv
      * width: 32
      * #c_type: unsigned_int
  * #source_location: 
    * file: ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---net--netfilter--nfnetlink_log.ko_false-unreach-call.cil.c
    * line: 7012
    * function: __fswab32
    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_100fb440-a49d-470a-945c-070576e16c64/bin-2018/cbmc
  0: symbol
      * type: unsignedbv
          * width: 32
          * #c_type: unsigned_int
      * identifier: __fswab32::val!0@5#1
      * expression: symbol
          * type: unsignedbv
              * width: 32
              * #c_type: unsigned_int
          * identifier: __fswab32::val
      * L0: 0
      * L1: 5
      * L2: 1
      * L1_object_identifier: __fswab32::val!0@5
      * #SSA_symbol: 1
warning: ignoring bswap
  * type: unsignedbv
      * width: 32
      * #c_type: unsigned_int
  * #source_location: 
    * file: ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---net--netfilter--nfnetlink_log.ko_false-unreach-call.cil.c
    * line: 7012
    * function: __fswab32
    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_100fb440-a49d-470a-945c-070576e16c64/bin-2018/cbmc
  0: symbol
      * type: unsignedbv
          * width: 32
          * #c_type: unsigned_int
      * identifier: __fswab32::val!0@6#1
      * expression: symbol
          * type: unsignedbv
              * width: 32
              * #c_type: unsigned_int
          * identifier: __fswab32::val
      * L0: 0
      * L1: 6
      * L2: 1
      * L1_object_identifier: __fswab32::val!0@6
      * #SSA_symbol: 1
warning: ignoring bswap
  * type: unsignedbv
      * width: 32
      * #c_type: unsigned_int
  * #source_location: 
    * file: ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---net--netfilter--nfnetlink_log.ko_false-unreach-call.cil.c
    * line: 7012
    * function: __fswab32
    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_100fb440-a49d-470a-945c-070576e16c64/bin-2018/cbmc
  0: symbol
      * type: unsignedbv
          * width: 32
          * #c_type: unsigned_int
      * identifier: __fswab32::val!0@7#1
      * expression: symbol
          * type: unsignedbv
              * width: 32
              * #c_type: unsigned_int
          * identifier: __fswab32::val
      * L0: 0
      * L1: 7
      * L2: 1
      * L1_object_identifier: __fswab32::val!0@7
      * #SSA_symbol: 1
warning: ignoring bswap
  * type: unsignedbv
      * width: 32
      * #c_type: unsigned_int
  * #source_location: 
    * file: ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---net--netfilter--nfnetlink_log.ko_false-unreach-call.cil.c
    * line: 7012
    * function: __fswab32
    * working_directory: /tmp/vcloud-vcloud-master/worker/working_dir_100fb440-a49d-470a-945c-070576e16c64/bin-2018/cbmc
  0: symbol
      * type: unsignedbv
          * width: 32
          * #c_type: unsigned_int
      * identifier: __fswab32::val!0@8#1
      * expression: symbol
          * type: unsignedbv
              * width: 32
              * #c_type: unsigned_int
          * identifier: __fswab32::val
      * L0: 0
      * L1: 8
      * L2: 1
      * L1_object_identifier: __fswab32::val!0@8
      * #SSA_symbol: 1
Running propositional reduction
Post-processing
Solving with Glucose Syrup with simplifier
2288405 variables, 7357188 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 3.301s
VERIFICATION SUCCESSFUL
EC=0
TRUE

[lucasccordeiro]

@tautschnig: I think I have seen one of your PRs related to bswap.

[tautschnig]

Yes, but 1) should that be the root cause then there's a problem with the benchmark as it would rely on GCC built-ins; 2) I believe we would generate non-deterministic values in such a case, and thus over-approximate rather than introduce an error. Also, the solver terminates VERY quickly, so I'd be a bit surprised if it were related to bswap.

[lucasccordeiro]

Thanks for the feedback.

I'm taking a look at this issue right now.

On 4 December 2017 at 11:44, Michael Tautschnig notifications@github.com wrote:

Yes, but 1) should that be the root cause then there's a problem with the benchmark as it would rely on GCC built-ins; 2) I believe we would generate non-deterministic values in such a case, and thus over-approximate rather than introduce an error. Also, the solver terminates VERY quickly, so I'd be a bit surprised if it were related to bswap.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/marek-trtik/cbmc/issues/38#issuecomment-348939061, or mute the thread https://github.com/notifications/unsubscribe-auth/ADheHW11FV4XVmnF1GIByvONdRTVy0-pks5s89ssgaJpZM4Q0hRc .

[marek-trtik]

Here are results of my investigation:

• I failed to manually prove or disprove the classification of the benchmark, because the benchmark is big and messy, and no short property-violating error trace exists (I failed to find any).
• For low unwind constant CBMC terminates with TRUE, for larger constants (e.g. 40) it timeouts (15min).
• I checked other tools for error traces, namely CPA-seq, SMACK, ESBMC, UAutomizer. But none of them successfully analysed the benchmarks (typically timeouts).