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

An error(UserWarning(f'Unexpected coverage goal xml data: "{basic_block_lines}"') from error) is reported from cbmc-viewer when I use more than one structure parameters in __CPROVER_ensures. #131

Closed Jerry-zhxf closed 1 year ago

Jerry-zhxf commented 1 year ago

CBMC version: 5.60.0 (cbmc-5.60.0) Architecture: x86_64 OS: linux gcc: 9.4.0 CBMC viewer: 3.6 Exact command line resulting in the issue:

cbmc-viewer --result /root/test_bug/logs/result.xml --coverage /root/test_bug/logs/coverage.xml --property /root/test_bug/logs/property.xml --srcdir /root/test_bug --goto /root/test_bug/gotos/test_harness.goto --reportdir /root/test_bug/report

test.h

typedef struct demo {
    int id;
} Demo;
int test(Demo *demo);

test.c

#include "test.h"
#include "cbmc_utils.h"

int test(Demo *demo)
{
    return test_long_contracts(demo);
}

int test_long_contracts(Demo *demo)
CBMC_ENSURES((demo->id == 1 && CBMC_RETURN_VALUE == 128) || CBMC_RETURN_VALUE == 384) // No Problem —— situation 1
// CBMC_ENSURES((demo->id == 1 && CBMC_RETURN_VALUE == 128) || (demo->id == 2 && CBMC_RETURN_VALUE == 256) || CBMC_RETURN_VALUE == 384) // Have Problem: UserWarning: Unexpected coverage goal xml data: "<Element 'basic_block_lines' at 0x7f838ae89580>" situation 2
{
    switch (demo->id) {
        case 1:
            return 128;
        case 2:
            return 256;
        default:
            return 384;
    }
}

test_harness.c

#include "test.h"

void test_harness(void)
{
    int id;
    test(id);
}

The entire process of generating the XML file uses this Makefile template and executes the make instruction.

situation 1

<?xml version="1.0" encoding="UTF-8"?>
<cprover>
<program>CBMC 5.60.0 (cbmc-5.60.0)</program>
<message type="STATUS-MESSAGE">
  <text>CBMC version 5.60.0 (cbmc-5.60.0) 64-bit x86_64 linux</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Reading GOTO program from file /root/test_bug/gotos/test_harness.goto</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Generating GOTO Program</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Adding CPROVER library (x86_64)</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Removal of function pointers and virtual functions</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Generic Property Instrumentation</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Rewriting existing assertions as assumptions</text>
</message>

<message type="WARNING">
  <text>Ignoring block 1 location 16 __CPROVER_replace_requires_is_fresh (missing source location)</text>
</message>

<message type="WARNING">
  <text>Ignoring block 2 location 19 __CPROVER_replace_requires_is_fresh (missing source location)</text>
</message>

<message type="WARNING">
  <text>Ignoring block 3 location 22 __CPROVER_replace_requires_is_fresh (missing source location)</text>
</message>

<message type="WARNING">
  <text>Ignoring block 4 location 25 __CPROVER_replace_requires_is_fresh (missing source location)</text>
</message>

<message type="WARNING">
  <text>Ignoring block 1 location 26 __CPROVER_replace_ensures_is_fresh (missing source location)</text>
</message>

<message type="WARNING">
  <text>Ignoring block 2 location 28 __CPROVER_replace_ensures_is_fresh (missing source location)</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Running with 8 object bits, 56 offset bits (user-specified)</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Starting Bounded Model Checking</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Symex: 0.0006105s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>size of program expression: 45 steps</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Generated 3 VCC(s), 3 remaining after simplification</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Postprocess Equation: 1.21e-05s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Passing problem to propositional reduction</text>
</message>

<message type="STATUS-MESSAGE">
  <text>converting SSA</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Convert SSA: 0.0004227s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Running propositional reduction</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Post-processing</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Post-process: 0.0002112s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Solving with MiniSAT 2.2.1 with simplifier</text>
</message>

<message type="STATUS-MESSAGE">
  <text>645 variables, 1815 clauses</text>
</message>

<message type="STATUS-MESSAGE">
  <text>SAT checker: instance is SATISFIABLE</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Solver: 0.0011409s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime decision procedure: 0.0016268s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Running propositional reduction</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Solving with MiniSAT 2.2.1 with simplifier</text>
</message>

<message type="STATUS-MESSAGE">
  <text>645 variables, 0 clauses</text>
</message>

<message type="STATUS-MESSAGE">
  <text>SAT checker: instance is SATISFIABLE</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Solver: 1.54e-05s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime decision procedure: 2.85e-05s</text>
</message>

<goal description="block 1 (lines /root/test_bug/test_harness.c:test_harness:5,6)" id="test_harness.coverage.1" status="SATISFIED">
  <location file="/root/test_bug/test_harness.c" function="test_harness" line="5" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test_harness.c" function="test_harness">5,6</line>
  </basic_block_lines>
</goal>

<goal description="block 2 (lines /root/test_bug/test_harness.c:test_harness:7)" id="test_harness.coverage.2" status="SATISFIED">
  <location file="/root/test_bug/test_harness.c" function="test_harness" line="7" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test_harness.c" function="test_harness">7</line>
  </basic_block_lines>
</goal>

<goal description="block 1 (lines /root/test_bug/test.c:test:6,7)" id="test.coverage.1" status="SATISFIED">
  <location file="/root/test_bug/test.c" function="test" line="6" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test.c" function="test">6,7</line>
  </basic_block_lines>
</goal>

<message type="STATUS-MESSAGE">
  <text>** 3 of 3 covered (100.0%)</text>
</message>

<message type="STATUS-MESSAGE">
  <text>** Used 3 iterations</text>
</message>

</cprover>

situation 2

<?xml version="1.0" encoding="UTF-8"?>
<cprover>
<program>CBMC 5.60.0 (cbmc-5.60.0)</program>
<message type="STATUS-MESSAGE">
  <text>CBMC version 5.60.0 (cbmc-5.60.0) 64-bit x86_64 linux</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Reading GOTO program from file /root/test_bug/gotos/test_harness.goto</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Generating GOTO Program</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Adding CPROVER library (x86_64)</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Removal of function pointers and virtual functions</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Generic Property Instrumentation</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Rewriting existing assertions as assumptions</text>
</message>

<message type="WARNING">
  <text>Ignoring block 1 location 26 __CPROVER_replace_requires_is_fresh (missing source location)</text>
</message>

<message type="WARNING">
  <text>Ignoring block 2 location 29 __CPROVER_replace_requires_is_fresh (missing source location)</text>
</message>

<message type="WARNING">
  <text>Ignoring block 3 location 32 __CPROVER_replace_requires_is_fresh (missing source location)</text>
</message>

<message type="WARNING">
  <text>Ignoring block 4 location 35 __CPROVER_replace_requires_is_fresh (missing source location)</text>
</message>

<message type="WARNING">
  <text>Ignoring block 1 location 52 __CPROVER_replace_ensures_is_fresh (missing source location)</text>
</message>

<message type="WARNING">
  <text>Ignoring block 2 location 54 __CPROVER_replace_ensures_is_fresh (missing source location)</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Running with 8 object bits, 56 offset bits (user-specified)</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Starting Bounded Model Checking</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Symex: 0.0009447s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>size of program expression: 65 steps</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Generated 9 VCC(s), 9 remaining after simplification</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Postprocess Equation: 1.21e-05s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Passing problem to propositional reduction</text>
</message>

<message type="STATUS-MESSAGE">
  <text>converting SSA</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Convert SSA: 0.0005083s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Running propositional reduction</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Post-processing</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Post-process: 0.0002255s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Solving with MiniSAT 2.2.1 with simplifier</text>
</message>

<message type="STATUS-MESSAGE">
  <text>659 variables, 1967 clauses</text>
</message>

<message type="STATUS-MESSAGE">
  <text>SAT checker: instance is SATISFIABLE</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Solver: 0.00145s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime decision procedure: 0.0020502s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Running propositional reduction</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Solving with MiniSAT 2.2.1 with simplifier</text>
</message>

<message type="STATUS-MESSAGE">
  <text>659 variables, 246 clauses</text>
</message>

<message type="STATUS-MESSAGE">
  <text>SAT checker: instance is SATISFIABLE</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Solver: 0.0004057s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime decision procedure: 0.0004359s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Running propositional reduction</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Solving with MiniSAT 2.2.1 with simplifier</text>
</message>

<message type="STATUS-MESSAGE">
  <text>659 variables, 239 clauses</text>
</message>

<message type="STATUS-MESSAGE">
  <text>SAT checker: instance is SATISFIABLE</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Solver: 0.0001405s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime decision procedure: 0.000165s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Running propositional reduction</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Solving with MiniSAT 2.2.1 with simplifier</text>
</message>

<message type="STATUS-MESSAGE">
  <text>659 variables, 2 clauses</text>
</message>

<message type="STATUS-MESSAGE">
  <text>SAT checker: instance is SATISFIABLE</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime Solver: 2.59e-05s</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Runtime decision procedure: 3.93e-05s</text>
</message>

<goal description="block 1 (lines /root/test_bug/test_harness.c:test_harness:5,6)" id="test_harness.coverage.1" status="SATISFIED">
  <location file="/root/test_bug/test_harness.c" function="test_harness" line="5" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test_harness.c" function="test_harness">5,6</line>
  </basic_block_lines>
</goal>

<goal description="block 2 (lines /root/test_bug/test_harness.c:test_harness:7)" id="test_harness.coverage.2" status="SATISFIED">
  <location file="/root/test_bug/test_harness.c" function="test_harness" line="7" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test_harness.c" function="test_harness">7</line>
  </basic_block_lines>
</goal>

<goal description="block 1 (lines /root/test_bug/test.c::10; /root/test_bug/test.c:test:6)" id="test.coverage.1" status="SATISFIED">
  <location file="/root/test_bug/test.c" function="test" line="6" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test.c" function="">10</line>
    <line file="/root/test_bug/test.c" function="test">6</line>
  </basic_block_lines>
</goal>

<goal description="block 2 (lines /root/test_bug/test.c::10)" id="test.coverage.2" status="SATISFIED">
  <location file="/root/test_bug/test.c" function="test" line="10" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test.c" function="">10</line>
  </basic_block_lines>
</goal>

<goal description="block 3 (lines /root/test_bug/test.c::10; /root/test_bug/test.c:test:6)" id="test.coverage.3" status="SATISFIED">
  <location file="/root/test_bug/test.c" function="test" line="10" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test.c" function="">10</line>
    <line file="/root/test_bug/test.c" function="test">6</line>
  </basic_block_lines>
</goal>

<goal description="block 4 (lines /root/test_bug/test.c::10)" id="test.coverage.4" status="SATISFIED">
  <location file="/root/test_bug/test.c" function="test" line="10" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test.c" function="">10</line>
  </basic_block_lines>
</goal>

<goal description="block 5 (lines /root/test_bug/test.c::10)" id="test.coverage.5" status="SATISFIED">
  <location file="/root/test_bug/test.c" function="test" line="10" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test.c" function="">10</line>
  </basic_block_lines>
</goal>

<goal description="block 6 (lines /root/test_bug/test.c::10; /root/test_bug/test.c:test:6)" id="test.coverage.6" status="SATISFIED">
  <location file="/root/test_bug/test.c" function="test" line="10" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test.c" function="">10</line>
    <line file="/root/test_bug/test.c" function="test">6</line>
  </basic_block_lines>
</goal>

<goal description="block 7 (lines /root/test_bug/test.c:test:6,7)" id="test.coverage.7" status="SATISFIED">
  <location file="/root/test_bug/test.c" function="test" line="6" working-directory="/root/test_bug"/>
  <basic_block_lines>
    <line file="/root/test_bug/test.c" function="test">6,7</line>
  </basic_block_lines>
</goal>

<message type="STATUS-MESSAGE">
  <text>** 9 of 9 covered (100.0%)</text>
</message>

<message type="STATUS-MESSAGE">
  <text>** Used 5 iterations</text>
</message>

</cprover>

error reports image

Traceback (most recent call last):
  File "/usr/local/lib/python3.10/dist-packages/cbmc_viewer/coveraget.py", line 543, in parse_basic_block_lines
    assert all(fyle and func and line for fyle, func, line in lines)
AssertionError

The above exception was the direct cause of the following exception:

Traceback (most recent call last):
  File "/usr/local/bin/cbmc-viewer", line 8, in <module>
    sys.exit(main())
  File "/usr/local/lib/python3.10/dist-packages/cbmc_viewer/cbmc_viewer.py", line 13, in main
    args.func(args)
  File "/usr/local/lib/python3.10/dist-packages/cbmc_viewer/viewer.py", line 98, in viewer
    coverage = coveraget.make_and_save_coverage(args, jsondir / 'viewer-coverage.json')
  File "/usr/local/lib/python3.10/dist-packages/cbmc_viewer/coveraget.py", line 616, in make_and_save_coverage
    obj = make_coverage(args)
  File "/usr/local/lib/python3.10/dist-packages/cbmc_viewer/coveraget.py", line 605, in make_coverage
    return CoverageFromCbmcXml(cbmc_coverage, srcdir)
  File "/usr/local/lib/python3.10/dist-packages/cbmc_viewer/coveraget.py", line 390, in __init__
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/usr/local/lib/python3.10/dist-packages/cbmc_viewer/coveraget.py", line 390, in <listcomp>
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/usr/local/lib/python3.10/dist-packages/cbmc_viewer/coveraget.py", line 402, in load_cbmc_xml
    lines = (parse_basic_block_lines(goal.find("basic_block_lines")) or
  File "/usr/local/lib/python3.10/dist-packages/cbmc_viewer/coveraget.py", line 547, in parse_basic_block_lines
    raise UserWarning(f'Unexpected coverage goal xml data: "{basic_block_lines}"') from error
UserWarning: Unexpected coverage goal xml data: "<Element 'basic_block_lines' at 0x7f838ae89580>"

Is this a bug? Or is there something wrong with the writing of the contracts?

nwetzler commented 1 year ago

This is caused by an issue in CBMC that was fixed in CBMC version 5.64.0.

https://github.com/diffblue/cbmc/pull/7037 https://github.com/diffblue/cbmc/commit/83abf73a541646fa855888a0050de1eb7cae2ea4

tautschnig commented 1 year ago

Closing given @nwetzler's clarification. Please feel free to re-open if the issue persists.