"bad optional access" when using --enforce-contract

[remi-delmas-3000]

• CBMC version: 5.38.0 (cbmc-5.38.0-36-gd570aa551)
• Operating system : Ubuntu 20.04

How to reproduce:

git clone https://github.com/remi-delmas-3000/s2n-tls.git
cd s2n-tls
git submodule update --init --recursive
git checkout function-contract-s2n_hash_digest-bad_optional_access_bug
cd tests/cbmc/proofs/s2n_hash_digest-contract
make result

Console output:

...
/home/ubuntu/s2n-tls/tests/litani/litani run-build
[5/12] s2n_hash_digest: checking function contracts                                                                                                                         FAILED: /home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/gotos/2.goto /tmp/litani/runs/664cb735-e4a1-48de-a7f8-ff7bb7b4fd22/status/67092c52-1055-4379-9028-1947b4b289d6.json

/home/ubuntu/s2n-tls/tests/litani/litani exec --command 'goto-instrument  --enforce-contract s2n_hash_digest /home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/gotos/1.goto /home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/gotos/2.goto' --pipeline-name s2n_hash_digest --ci-stage build --job-id 67092c52-1055-4379-9028-1947b4b289d6 --stdout-file /home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/logs/check_function_contracts-log.txt --description 's2n_hash_digest: checking function contracts' --status-file /tmp/litani/runs/664cb735-e4a1-48de-a7f8-ff7bb7b4fd22/status/67092c52-1055-4379-9028-1947b4b289d6.json --profile-memory-interval 10 --inputs /home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/gotos/1.goto --outputs /home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/gotos/2.goto --interleave-stdout-stderr

litani: Output file '/home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/gotos/2.goto' of pipeline 's2n_hash_digest' did not exist upon job completion. Not copying to artifacts directory. If this job is not supposed to emit the file, pass `--phony-outputs /home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/gotos/2.goto` to suppress this warning

ninja: build stopped: cannot make progress due to previous errors.

The step that fails is step 5 "enforce contracts", but it fails before the actual contract transformation code gets to run.

ubuntu:~/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract$ goto-instrument  --enforce-contract s2n_hash_digest /home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/gotos/1.goto /home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/gotos/2.goto
Reading GOTO program from '/home/ubuntu/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract/gotos/1.goto'
Function Pointer Removal
file /home/ubuntu/s2n-tls/crypto/s2n_hash.c line 542 function s2n_hash_init: replacing function pointer by 5 possible targets
file /home/ubuntu/s2n-tls/crypto/s2n_hash.c line 501 function s2n_hash_new: replacing function pointer by 7 possible targets
file /home/ubuntu/s2n-tls/crypto/s2n_hash.c line 573 function s2n_hash_copy: replacing function pointer by 5 possible targets
file /home/ubuntu/s2n-tls/crypto/s2n_hash.c line 554 function s2n_hash_update: replacing function pointer by 4 possible targets
file /home/ubuntu/s2n-tls/crypto/s2n_hash.c line 521 function s2n_hash_allow_md5_for_fips: replacing function pointer by 7 possible targets
file /home/ubuntu/s2n-tls/crypto/s2n_hash.c line 602 function s2n_hash_free: replacing function pointer by 7 possible targets
file /home/ubuntu/s2n-tls/crypto/s2n_hash.c line 586 function s2n_hash_reset: replacing function pointer by 7 possible targets
Virtual function removal
Cleaning inline assembler statements
bad optional access

Could this be related to changes introduced by PR #6340 ?

[NlightNFotis]

Hello.

I have done a git bisect between versions 5.38.0 and 5.39.0 of CBMC, and found that the commit introducing the bad optional access is fba232b.

I am not quite sure yet how the commit leads to bad optional access, but I'm continuing my investigation and will update you once my understanding is enhanced and/or a fix has been identified.

[remi-delmas-3000]

Thank you for the analysis, we are taking over to dig into the issue

[NlightNFotis]

Hi, I can give you some more information in case it helps you with your debugging.

• It looks like the bad optional access is created in src/goto-instrument/contracts/assigns.cpp:52 when the .value() of the size_of_expr is taken.
• I believe the reason for that is that for one of the dereference expressions, type has ID_empty causing a fall through the cases of size_of_expr and returning {} (the constructor of an empty optionalt).
• In particular, the offending structure looks like this in my debug log:

[DEBUG] address here is: pointer
[DEBUG] address type is: empty
---------------
[DEBUG] Address is address_of
  * type: pointer
      * width: 64
      0: empty
          * #source_location: 
            * file: /Users/fotiskoutoulakis/Devel/s2n-tls/crypto/s2n_hash.c
            * line: 558
            * function: 
            * working_directory: /Users/fotiskoutoulakis/Devel/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract
  0: dereference
      * type: empty
          * #source_location: 
            * file: /Users/fotiskoutoulakis/Devel/s2n-tls/crypto/s2n_hash.c
            * line: 558
            * function: 
            * working_directory: /Users/fotiskoutoulakis/Devel/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract
      * #source_location: 
        * file: /Users/fotiskoutoulakis/Devel/s2n-tls/crypto/s2n_hash.c
        * line: 560
        * function: 
        * working_directory: /Users/fotiskoutoulakis/Devel/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract
      * #lvalue: 1
      0: symbol
          * type: pointer
              * #source_location: 
                * file: /Users/fotiskoutoulakis/Devel/s2n-tls/crypto/s2n_hash.c
                * line: 558
                * function: 
                * working_directory: /Users/fotiskoutoulakis/Devel/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract
              * width: 64
              0: empty
                  * #source_location: 
                    * file: /Users/fotiskoutoulakis/Devel/s2n-tls/crypto/s2n_hash.c
                    * line: 558
                    * function: 
                    * working_directory: /Users/fotiskoutoulakis/Devel/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract
          * #source_location: 
            * file: /Users/fotiskoutoulakis/Devel/s2n-tls/crypto/s2n_hash.c
            * line: 560
            * function: 
            * working_directory: /Users/fotiskoutoulakis/Devel/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract
          * identifier: s2n_hash_digest::out
          * #lvalue: 1
[DEBUG] Nothing so far; id is empty
bad optional access

• In contrast to that, a valid (or at least, not crashing) structure looks like this:

[DEBUG] address here is: pointer
[DEBUG] address type is: pointer
---------------
[DEBUG] Address is address_of
  * type: pointer
      * width: 64
      0: pointer
          * #source_location: 
            * file: /Users/fotiskoutoulakis/Devel/s2n-tls/error/s2n_errno.h
            * line: 289
            * function: 
            * working_directory: /Users/fotiskoutoulakis/Devel/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract
          * width: 64
          0: signedbv
              * width: 8
              * #constant: 1
              * #c_type: char
  0: symbol
      * type: pointer
          * #source_location: 
            * file: /Users/fotiskoutoulakis/Devel/s2n-tls/error/s2n_errno.h
            * line: 289
            * function: 
            * working_directory: /Users/fotiskoutoulakis/Devel/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract
          * width: 64
          0: signedbv
              * width: 8
              * #constant: 1
              * #c_type: char
      * #source_location: 
        * file: /Users/fotiskoutoulakis/Devel/s2n-tls/crypto/s2n_hash.c
        * line: 560
        * function: 
        * working_directory: /Users/fotiskoutoulakis/Devel/s2n-tls/tests/cbmc/proofs/s2n_hash_digest-contract
      * identifier: s2n_debug_str
      * #lvalue: 1

• The debug output, I got it out of assigns.cpp by printing the .pretty() of the address passed to the dereference_exprt.

I hope this may be helpful to you!

[remi-delmas-3000]

Much appreciated thank you !