search

model-checking / cbmc-viewer

CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.
https://model-checking.github.io/cbmc-viewer/
Apache License 2.0
32 stars 11 forks source link

Report generation crashes in validation with humanized errors #27

Closed adpaco-aws closed 3 years ago

adpaco-aws commented 3 years ago

cbmc-viewer version: 2.3 (issue also present in 2.2) How to reproduce: On my branch default-materials-proof, go to aws-encryption-sdk-c/verification/cbmc/proofs/default_cmm_generate_enc_materials and make.

The error does appear frequently when working on proofs from that project. It appears to be crashing when building error traces.

Traceback (most recent call last):
  File "/usr/local/lib/python3.9/site-packages/voluptuous/humanize.py", line 38, in validate_with_humanized_errors
    return schema(data)
  File "/usr/local/lib/python3.9/site-packages/voluptuous/schema_builder.py", line 272, in __call__
    return self._compiled([], data)
  File "/usr/local/lib/python3.9/site-packages/voluptuous/schema_builder.py", line 594, in validate_dict
    return base_validate(path, iteritems(data), out)
  File "/usr/local/lib/python3.9/site-packages/voluptuous/schema_builder.py", line 432, in validate_mapping
    raise er.MultipleInvalid(errors)
voluptuous.error.MultipleInvalid: not a valid value for dictionary value @ data['traces']['default_cmm_generate_enc_materials.pointer_dereference.79'][56]['location']['function']

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/usr/local/bin/cbmc-viewer", line 8, in <module>
    sys.exit(viewer())
  File "/usr/local/lib/python3.9/site-packages/cbmc_viewer/viewer.py", line 161, in viewer
    traces = tracet.do_make_trace(args.viewer_trace, args.result,
  File "/usr/local/lib/python3.9/site-packages/cbmc_viewer/tracet.py", line 679, in do_make_trace
    return TraceFromCbmcText(cbmc_trace, srcdir, wkdir)
  File "/usr/local/lib/python3.9/site-packages/cbmc_viewer/tracet.py", line 181, in __init__
    super(TraceFromCbmcText, self).__init__(
  File "/usr/local/lib/python3.9/site-packages/cbmc_viewer/tracet.py", line 118, in __init__
    self.validate()
  File "/usr/local/lib/python3.9/site-packages/cbmc_viewer/tracet.py", line 134, in validate
    return voluptuous.humanize.validate_with_humanized_errors(
  File "/usr/local/lib/python3.9/site-packages/voluptuous/humanize.py", line 40, in validate_with_humanized_errors
    raise Error(humanize_error(data, e, max_sub_error_length))
voluptuous.error.Error: not a valid value for dictionary value @ data['traces']['aws_array_list_is_valid.overflow.6'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_is_valid.overflow.8'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_is_valid.pointer_primitives.10'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_is_valid.pointer_primitives.11'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_is_valid.pointer_primitives.12'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_is_valid.pointer_primitives.13'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_is_valid.pointer_primitives.14'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_is_valid.pointer_primitives.15'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_is_valid.pointer_primitives.16'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_is_valid.pointer_primitives.9'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_length.assertion.1'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_length.precondition.1'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_array_list_length.precondition.2'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_enc_materials_destroy.precondition.1'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.23'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.24'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.25'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.27'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.37'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.38'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.39'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.41'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.42'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.51'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.52'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.53'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.55'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.56'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.57'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.58'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.59'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.60'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.61'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.62'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.pointer_dereference.63'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.precondition.2'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.precondition.5'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_cryptosdk_keyring_on_encrypt.precondition.6'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_find.assertion.1'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_find.precondition.1'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.assertion.1'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.pointer_dereference.16'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.pointer_dereference.17'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.pointer_dereference.18'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.pointer_dereference.20'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.pointer_dereference.21'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.pointer_dereference.23'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.pointer_dereference.24'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.pointer_dereference.25'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.pointer_dereference.27'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.pointer_dereference.28'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['aws_hash_table_put.precondition.1'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['default_cmm_generate_enc_materials.pointer_dereference.79'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['default_cmm_generate_enc_materials.pointer_dereference.80'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['default_cmm_generate_enc_materials.pointer_dereference.81'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['default_cmm_generate_enc_materials.pointer_dereference.82'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['default_cmm_generate_enc_materials.pointer_dereference.83'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['default_cmm_generate_enc_materials.pointer_dereference.84'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['default_cmm_generate_enc_materials.pointer_dereference.85'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['default_cmm_generate_enc_materials_harness.assertion.1'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
not a valid value for dictionary value @ data['traces']['default_cmm_generate_enc_materials_harness.assertion.2'][56]['location']['function']. Got ('__atomic_load_n_U64 thread 0',)
markrtuttle commented 3 years ago

This is clearly a parsing error: looking at __atomic_load_n_U64 thread 0 as a function name. I suspect cbmc is producing a "malformed" source location for atomic builtins. I'll take a look on Monday.

markrtuttle commented 3 years ago

Resolved with pull request https://github.com/awslabs/aws-viewer-for-cbmc/pull/28