Crash with json ui

[zhassan-aws]

CBMC version: cbmc-5.50.0
Operating system: Ubuntu 20.04

Running the attached example with:

cbmc --unwind 2 --object-bits 10 a.out --pointer-check --json-ui

causes CBMC to crash:

[
  {
    "program": "CBMC 5.50.0 (cbmc-5.50.0)"
  },
  {
    "messageText": "CBMC version 5.50.0 (cbmc-5.50.0) 64-bit x86_64 linux",
    "messageType": "STATUS-MESSAGE"
  },
  {
    "messageText": "Reading GOTO program from file a.out",
    "messageType": "STATUS-MESSAGE"
  },

<snip>

            "assignmentType": "variable",
            "hidden": true,
            "internal": false,
            "lhs": "var_3.cases",
            "mode": "C",
            "sourceLocation": {
              "column": "27",
              "file": "/rustc/0c292c9667f1b202a9150d58bdd2e89e3e803996/library/core/src/result.rs",
              "function": "<std::result::Result<T, F> as std::ops::FromResidual<std::result::Result<std::convert::Infallible, E>>>::from_residual",
              "line": "2052"
            },
            "stepType": "assignment",
            "thread": 0,
            "value": {
              "member": {
                "name": "UnexpectedEof",
                "value": {
                  "members": [
                    {
                      "name": "0",
                      "value": {
                        "binary": "0000000000000000000000000000000000000000000000000000000000001000",
                        "data": "8ul",
                        "name": "integer",
                        "type": "__CPROVER_size_t",
                        "width": 64
                      }
                    }
                  ],
                  "name": "struct"
                }
              },
              "name": "union"
            }
          }--- begin invariant violation report ---
Invariant check failed
File: ../src/util/expr_cast.h:256 function: validate_operands
Condition: allow_more ? value.operands().size()>=number : value.operands().size()==number
Reason: Unary expressions must have one operand
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x55ec297ff270]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x55ec297ff819]
cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x48) [0x55ec29098368]
cbmc(validate_operands(exprt const&, unsigned long, char const*, bool)+0xd8) [0x55ec2918a828]
cbmc(json(exprt const&, namespacet const&, dstringt const&)+0x4373) [0x55ec2942dbe3]
cbmc(json(exprt const&, namespacet const&, dstringt const&)+0x2bbf) [0x55ec2942c42f]
cbmc(json(exprt const&, namespacet const&, dstringt const&)+0x2bbf) [0x55ec2942c42f]
cbmc(json(exprt const&, namespacet const&, dstringt const&)+0x8dc) [0x55ec2942a14c]
cbmc(json(exprt const&, namespacet const&, dstringt const&)+0x2bbf) [0x55ec2942c42f]
cbmc(convert_decl(json_objectt&, conversion_dependenciest const&, trace_optionst const&)+0xf2c) [0x55ec29436a5c]
cbmc(void convert<json_stream_arrayt>(namespacet const&, goto_tracet const&, json_stream_arrayt&, trace_optionst)+0x5c2) [0x55ec290bb2d2]
cbmc(output_properties_with_traces(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > > const&, goto_trace_storaget const&, trace_optionst const&, unsigned long, ui_message_handlert&)+0xbec) [0x55ec290d2b5c]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::report()+0x94) [0x55ec290a03e4]
cbmc(cbmc_parse_optionst::doit()+0xf9a) [0x55ec2909f81a]
cbmc(parse_options_baset::main()+0x8f) [0x55ec2909647f]
cbmc(main+0x39) [0x55ec29084d39]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f3c3c4180b3]
cbmc(_start+0x2e) [0x55ec29097d7e]


--- end invariant violation report ---

If I take out the --json-ui option, it doesn't crash:

CBMC version 5.50.0 (cbmc-5.50.0) 64-bit x86_64 linux
Reading GOTO program from file a.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 10 object bits, 54 offset bits (user-specified)
Starting Bounded Model Checking

<snip>


** 10 of 1128 failed (4 iterations)
VERIFICATION FAILED

json-ui-crash.tar.gz

[martin-cs]

Thank you for the detailed and helpful bug report. A quick look at this suggests this might be the problem:

--- begin invariant violation report --- Invariant check failed File: ../src/util/expr_cast.h:256 function: validate_operands Condition: allow_more ? value.operands().size()>=number : value.operands().size()==number Reason: Unary expressions must have one operand Backtrace:

<snip>

cbmc(validate_operands(exprt const&, unsigned long, char const*, bool)+0xd8) [0x55ec2918a828] cbmc(json(exprt const&, namespacet const&, dstringt const&)+0x4373) [0x55ec2942dbe3] cbmc(json(exprt const&, namespacet const&, dstringt const&)+0x2bbf) [0x55ec2942c42f] cbmc(json(exprt const&, namespacet const&, dstringt const&)+0x2bbf) [0x55ec2942c42f] cbmc(json(exprt const&, namespacet const&, dstringt const&)+0x8dc) [0x55ec2942a14c] cbmc(json(exprt const&, namespacet const&, dstringt const&)+0x2bbf) [0x55ec2942c42f] cbmc(convert_decl(json_objectt&, conversion_dependenciest const&, trace_optionst const&)+0xf2c) [0x55ec29436a5c] cbmc(void convert<json_stream_arrayt>(namespacet const&, goto_tracet const&, json_stream_arrayt&, trace_optionst)+0x5c2) [0x55ec290bb2d2] cbmc(output_properties_with_traces(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > > const&, goto_trace_storaget const&, trace_optionst const&, unsigned long, ui_message_handlert&)+0xbec) [0x55ec290d2b5c] cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_che ckert>::report()+0x94) [0x55ec290a03e4] cbmc(cbmc_parse_optionst::doit()+0xf9a) [0x55ec2909f81a] cbmc(parse_options_baset::main()+0x8f) [0x55ec2909647f] cbmc(main+0x39) [0x55ec29084d39] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f3c3c4180b3] cbmc(_start+0x2e) [0x55ec29097d7e]

validate_operands seems to being called from the JSON conversion which would explain why it is crashing without it. This is an issue as it suggests we should really check this earlier on. However the actual bug is one of: 1. validate_operands is trying to convert something to a unary type that isn't a unary type. 2. the Rust front-end is using a unary operand ID type for something that isn't a unary operator. Would it be possible to have the Rust folks look into 2?

[zhassan-aws]

Thanks for the quick response. I'll try to minimize the Rust testcase to narrow down the source of the issue. Hopefully, this will give us insight on whether it's 1 or 2.

[martin-cs]

Thanks for the quick response. I'll try to minimize the Rust testcase to narrow down the source of the issue. Hopefully, this will give us insight on whether it's 1 or 2.

That would be helpful; thank you.

[zhassan-aws]

I found an example in the Kani regressions that fails with --json-ui:

fn takes_dyn_fun(fun: Box<dyn FnOnce() -> u32>) -> u32 {
    fun()
}

pub fn unit_to_u32() -> u32 {
    5
}

fn main() {
    assert!(takes_dyn_fun(Box::new(&unit_to_u32)) == 3, "Wrong u32")
}

when run with kani test.rs.

The corresponding goto files are in the attached tarball.

The crash can be reproduced on test.symtab.json.out using cbmc test.symtab.json.out --function main --json-ui. This is the goto binary converted from the json that Kani generated.

It can also be reproduced on the processed goto binary file test.goto using cbmc test.goto --json-ui.

iss-6691-min.tar.gz

[zhassan-aws]

Here's yet another minimal Rust example that results in the same crash when run with kani --unwind 2 vec_len.rs.:

fn main() {
    let a: Vec<Vec<i32>> = vec![vec![]; 1];
    assert!(false);
}

The corresponding goto programs are attached.

Both:

cbmc --unwind 2 vec_len.goto --json-ui

and

cbmc vec_len.symtab.json.out --json-ui --function main

result in the same crash.

vec_len.tar.gz

[martin-cs]

That's great, thanks for minimising it.

[tautschnig]

The bogus code is https://github.com/diffblue/cbmc/blob/7157df5944bdd15491995fd995d9b06eae287888/src/goto-programs/json_expr.cpp#L310..L312. It would require added simpl_expr.has_operands() as a further check to deal with pointer constants as generated by the back-end. What I'd prefer, however, is to fix this via #6598, which removes this weird case where some constants have operands (and, in particular, completely removes the affected piece of code).