Skip to content

Counter-example traces for struct types incomplete #6845

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
J0hnDaniel opened this issue May 5, 2022 · 1 comment · Fixed by #6875
Closed

Counter-example traces for struct types incomplete #6845

J0hnDaniel opened this issue May 5, 2022 · 1 comment · Fixed by #6875
Labels
pending merge

Comments

@J0hnDaniel
Copy link

Description

CBMC version: 5.44
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc struct.c --function main --trace
What behaviour did you expect: a better display
What happened instead:
There is a state on which the struct display strange value see the

struct.c Code

#include <assert.h>

struct str
{
  float x;
  short y;
  int z;
};

int main (void)
{
  int q;
  struct str s;

  s.x = q;
  s.y = s.x+1;
  s.z = s.y + s.x;

  assert(q == s.z);

  return 1;
}

Trace Display Standard Output

Using the standard output here is what i get, look on state 25
Command used : cbmc struct.c --function main --trace
CBMC Trace

CBMC version 5.44.0 (cbmc-5.44.0) 64-bit x86_64 linux
Parsing struct.c
Converting
Type-checking struct
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00456427s
size of program expression: 47 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 2.4675e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0324137s
Running propositional reduction
Post-processing
Runtime Post-process: 0.000135331s
Solving with MiniSAT 2.2.1 with simplifier
4219 variables, 16057 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0945321s
Runtime decision procedure: 0.127061s
Building error trace

** Results:
struct.c function main
[main.assertion.1] line 19 assertion q == s.z: FAILURE

Trace for main.assertion.1:

State 24 file struct.c function main line 12 thread 0
----------------------------------------------------
  q=0 (00000000 00000000 00000000 00000000)

State 25 file struct.c function main line 13 thread 0
----------------------------------------------------
  s={ .x=s!0@1#1..x, .y=s!0@1#1..y, .$pad2=s!0@1#1..$pad2, .z=s!0@1#1..z } ({ ?, ?, ?, ? })

State 26 file struct.c function main line 15 thread 0
----------------------------------------------------
  s.x=0.0f (00000000 00000000 00000000 00000000)

State 27 file struct.c function main line 16 thread 0
----------------------------------------------------
  s.y=1 (00000000 00000001)

State 28 file struct.c function main line 17 thread 0
----------------------------------------------------
  s.z=1 (00000000 00000000 00000000 00000001)

Violated property:
  file struct.c function main line 19 thread 0
  assertion q == s.z
  q == s.z

XML UI output

Using XML UI option
Command cbmc struct.c --function main --trace --xml-ui
The types are not displayed for the child of the structure, e.g. struct

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

<message type="STATUS-MESSAGE">
  <text>Parsing struct.c</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Converting</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Type-checking struct</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>Running with 8 object bits, 56 offset bits (default)</text>
</message>

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

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

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

<message type="STATUS-MESSAGE">
  <text>simple slicing removed 5 assignments</text>
</message>

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

<message type="STATUS-MESSAGE">
  <text>Runtime Postprocess Equation: 3.13e-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.0326509s</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.000163779s</text>
</message>

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

<message type="STATUS-MESSAGE">
  <text>4219 variables, 16057 clauses</text>
</message>

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

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

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

<message type="STATUS-MESSAGE">
  <text>Building error trace</text>
</message>

<result property="main.assertion.1" status="FAILURE">
  <goto_trace>
    <function_call hidden="true" step_nr="2" thread="0">
      <function display_name="__CPROVER_initialize" identifier="__CPROVER_initialize">
        <location file="&lt;built-in-additions&gt;" line="40" working-directory="/home/testData/struct"/>
      </function>
    </function_call>
    <assignment assignment_type="state" base_name="__CPROVER_alloca_object" display_name="__CPROVER_alloca_object" hidden="true" identifier="__CPROVER_alloca_object" mode="C" step_nr="3" thread="0">
      <location file="&lt;built-in-additions&gt;" line="20" working-directory="/home/testData/struct"/>
      <type>const void *</type>
      <full_lhs>__CPROVER_alloca_object</full_lhs>
      <full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">NULL</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_dead_object" display_name="__CPROVER_dead_object" hidden="true" identifier="__CPROVER_dead_object" mode="C" step_nr="4" thread="0">
      <location file="&lt;built-in-additions&gt;" line="14" working-directory="/home/testData/struct"/>
      <type>const void *</type>
      <full_lhs>__CPROVER_dead_object</full_lhs>
      <full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">NULL</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_deallocated" display_name="__CPROVER_deallocated" hidden="true" identifier="__CPROVER_deallocated" mode="C" step_nr="5" thread="0">
      <location file="&lt;built-in-additions&gt;" line="13" working-directory="/home/testData/struct"/>
      <type>const void *</type>
      <full_lhs>__CPROVER_deallocated</full_lhs>
      <full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">NULL</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_malloc_failure_mode_assert_then_assume" display_name="__CPROVER_malloc_failure_mode_assert_then_assume" hidden="true" identifier="__CPROVER_malloc_failure_mode_assert_then_assume" mode="C" step_nr="6" thread="0">
      <location file="&lt;built-in-additions&gt;" line="23" working-directory="/home/testData/struct"/>
      <type>signed int</type>
      <full_lhs>__CPROVER_malloc_failure_mode_assert_then_assume</full_lhs>
      <full_lhs_value binary="00000000000000000000000000000010">2</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_malloc_failure_mode_return_null" display_name="__CPROVER_malloc_failure_mode_return_null" hidden="true" identifier="__CPROVER_malloc_failure_mode_return_null" mode="C" step_nr="7" thread="0">
      <location file="&lt;built-in-additions&gt;" line="22" working-directory="/home/testData/struct"/>
      <type>signed int</type>
      <full_lhs>__CPROVER_malloc_failure_mode_return_null</full_lhs>
      <full_lhs_value binary="00000000000000000000000000000001">1</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_malloc_is_new_array" display_name="__CPROVER_malloc_is_new_array" hidden="true" identifier="__CPROVER_malloc_is_new_array" mode="C" step_nr="8" thread="0">
      <location file="&lt;built-in-additions&gt;" line="17" working-directory="/home/testData/struct"/>
      <type>__CPROVER_bool</type>
      <full_lhs>__CPROVER_malloc_is_new_array</full_lhs>
      <full_lhs_value>FALSE</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_malloc_object" display_name="__CPROVER_malloc_object" hidden="true" identifier="__CPROVER_malloc_object" mode="C" step_nr="9" thread="0">
      <location file="&lt;built-in-additions&gt;" line="15" working-directory="/home/testData/struct"/>
      <type>const void *</type>
      <full_lhs>__CPROVER_malloc_object</full_lhs>
      <full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">NULL</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_malloc_size" display_name="__CPROVER_malloc_size" hidden="true" identifier="__CPROVER_malloc_size" mode="C" step_nr="10" thread="0">
      <location file="&lt;built-in-additions&gt;" line="16" working-directory="/home/testData/struct"/>
      <type>__CPROVER_size_t</type>
      <full_lhs>__CPROVER_malloc_size</full_lhs>
      <full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">0ul</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_max_malloc_size" display_name="__CPROVER_max_malloc_size" hidden="true" identifier="__CPROVER_max_malloc_size" mode="C" step_nr="11" thread="0">
      <location file="&lt;built-in-additions&gt;" line="24" working-directory="/home/testData/struct"/>
      <type>__CPROVER_size_t</type>
      <full_lhs>__CPROVER_max_malloc_size</full_lhs>
      <full_lhs_value binary="0000000010000000000000000000000000000000000000000000000000000000">36028797018963968ul</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_memory_leak" display_name="__CPROVER_memory_leak" hidden="true" identifier="__CPROVER_memory_leak" mode="C" step_nr="12" thread="0">
      <location file="&lt;built-in-additions&gt;" line="18" working-directory="/home/testData/struct"/>
      <type>const void *</type>
      <full_lhs>__CPROVER_memory_leak</full_lhs>
      <full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">NULL</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_next_thread_id" display_name="__CPROVER_next_thread_id" hidden="true" identifier="__CPROVER_next_thread_id" mode="C" step_nr="13" thread="0">
      <location file="&lt;built-in-additions&gt;" line="8" working-directory="/home/testData/struct"/>
      <type>unsigned long int</type>
      <full_lhs>__CPROVER_next_thread_id</full_lhs>
      <full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">0ul</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_next_thread_key" display_name="__CPROVER_next_thread_key" hidden="true" identifier="__CPROVER_next_thread_key" mode="C" step_nr="14" thread="0">
      <location file="&lt;built-in-additions&gt;" line="11" working-directory="/home/testData/struct"/>
      <type>unsigned long int</type>
      <full_lhs>__CPROVER_next_thread_key</full_lhs>
      <full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">0ul</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_pipe_count" display_name="__CPROVER_pipe_count" hidden="true" identifier="__CPROVER_pipe_count" mode="C" step_nr="15" thread="0">
      <location file="&lt;built-in-additions&gt;" line="38" working-directory="/home/testData/struct"/>
      <type>unsigned int</type>
      <full_lhs>__CPROVER_pipe_count</full_lhs>
      <full_lhs_value binary="00000000000000000000000000000000">0u</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_rounding_mode" display_name="__CPROVER_rounding_mode" hidden="true" identifier="__CPROVER_rounding_mode" mode="C" step_nr="16" thread="0">
      <location file="&lt;built-in-additions&gt;" line="29" working-directory="/home/testData/struct"/>
      <type>signed int</type>
      <full_lhs>__CPROVER_rounding_mode</full_lhs>
      <full_lhs_value binary="00000000000000000000000000000000">0</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_thread_id" display_name="__CPROVER_thread_id" hidden="true" identifier="__CPROVER_thread_id" mode="C" step_nr="17" thread="0">
      <location file="&lt;built-in-additions&gt;" line="6" working-directory="/home/testData/struct"/>
      <type>unsigned long int</type>
      <full_lhs>__CPROVER_thread_id</full_lhs>
      <full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">0ul</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_thread_key_dtors" display_name="__CPROVER_thread_key_dtors" hidden="true" identifier="__CPROVER_thread_key_dtors" mode="C" step_nr="18" thread="0">
      <location file="&lt;built-in-additions&gt;" line="10" working-directory="/home/testData/struct"/>
      <type>void (*[INFINITY()])(void *)</type>
      <full_lhs>__CPROVER_thread_key_dtors</full_lhs>
      <full_lhs_value>__CPROVER_thread_key_dtors!0#1</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_thread_keys" display_name="__CPROVER_thread_keys" hidden="true" identifier="__CPROVER_thread_keys" mode="C" step_nr="19" thread="0">
      <location file="&lt;built-in-additions&gt;" line="9" working-directory="/home/testData/struct"/>
      <type>const void *[INFINITY()]</type>
      <full_lhs>__CPROVER_thread_keys</full_lhs>
      <full_lhs_value>__CPROVER_thread_keys!0#1</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="__CPROVER_threads_exited" display_name="__CPROVER_threads_exited" hidden="true" identifier="__CPROVER_threads_exited" mode="C" step_nr="20" thread="0">
      <location file="&lt;built-in-additions&gt;" line="7" working-directory="/home/testData/struct"/>
      <type>__CPROVER_bool [INFINITY()]</type>
      <full_lhs>__CPROVER_threads_exited</full_lhs>
      <full_lhs_value>__CPROVER_threads_exited#1</full_lhs_value>
    </assignment>
    <function_return hidden="true" step_nr="21" thread="0">
      <function display_name="__CPROVER_initialize" identifier="__CPROVER_initialize">
        <location file="&lt;built-in-additions&gt;" line="40" working-directory="/home/testData/struct"/>
      </function>
    </function_return>
    <location-only hidden="false" step_nr="22" thread="0">
      <location file="struct.c" line="10" working-directory="/home/testData/struct"/>
    </location-only>
    <function_call hidden="false" step_nr="23" thread="0">
      <function display_name="main" identifier="main">
        <location file="struct.c" line="10" working-directory="/home/testData/struct"/>
      </function>
      <location file="struct.c" line="10" working-directory="/home/testData/struct"/>
    </function_call>
    <assignment assignment_type="state" base_name="q" display_name="main::1::q" hidden="false" identifier="main::1::q" mode="C" step_nr="24" thread="0">
      <location file="struct.c" function="main" line="12" working-directory="/home/testData/struct"/>
      <type>signed int</type>
      <full_lhs>q</full_lhs>
      <full_lhs_value binary="00000000000000000000000000000000">0</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="s" display_name="main::1::s" hidden="false" identifier="main::1::s" mode="C" step_nr="25" thread="0">
      <location file="struct.c" function="main" line="13" working-directory="/home/testData/struct"/>
      <type>struct str</type>
      <full_lhs>s</full_lhs>
      <full_lhs_value>{ .x=s!0@1#1..x, .y=s!0@1#1..y, .$pad2=s!0@1#1..$pad2, .z=s!0@1#1..z }</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="s" display_name="main::1::s" hidden="false" identifier="main::1::s" mode="C" step_nr="26" thread="0">
      <location file="struct.c" function="main" line="15" working-directory="/home/testData/struct"/>
      <type>struct str</type>
      <full_lhs>s.x</full_lhs>
      <full_lhs_value binary="00000000000000000000000000000000">0.0f</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="s" display_name="main::1::s" hidden="false" identifier="main::1::s" mode="C" step_nr="27" thread="0">
      <location file="struct.c" function="main" line="16" working-directory="/home/testData/struct"/>
      <type>struct str</type>
      <full_lhs>s.y</full_lhs>
      <full_lhs_value binary="0000000000000001">1</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="s" display_name="main::1::s" hidden="false" identifier="main::1::s" mode="C" step_nr="28" thread="0">
      <location file="struct.c" function="main" line="17" working-directory="/hometestData/struct"/>
      <type>struct str</type>
      <full_lhs>s.z</full_lhs>
      <full_lhs_value binary="00000000000000000000000000000001">1</full_lhs_value>
    </assignment>
    <failure hidden="false" property="main.assertion.1" reason="assertion q == s.z" step_nr="29" thread="0">
      <location file="struct.c" function="main" line="19" working-directory="/home/testData/struct"/>
    </failure>
  </goto_trace>
</result>

<message type="STATUS-MESSAGE">
  <text>VERIFICATION FAILED</text>
</message>

<cprover-status>FAILURE</cprover-status>

</cprover>

I am expecting that the type of s.x s.y s.z is not marked as struct str but as the type of the child, in my example
float, short and int respectively

Any ideas?
Thanks
@tautschnig
Copy link
Collaborator

I do have a fix for the XML type issue, but still need to continue looking into the missing values.

@tautschnig tautschnig self-assigned this May 19, 2022
tautschnig added a commit to tautschnig/cbmc that referenced this issue May 23, 2022
@tautschnig
Goto-symex: record value-at-declaration in the back-end
666b787 
Declarations are printed as part of a symex trace, and come with both a
symbol being declared as well as an (unconstrained) initial value for
that symbol. The decision procedure must learn about the initial value
to include it in the model. Else, the trace value would just be question
marks.

Fixes: diffblue#6845
@tautschnig tautschnig mentioned this issue May 23, 2022
Merged
3 tasks
@tautschnig tautschnig removed their assignment May 23, 2022
tautschnig added a commit to tautschnig/cbmc that referenced this issue May 24, 2022
@tautschnig
Goto-symex: record value-at-declaration in the back-end
0ce746a 
Declarations are printed as part of a symex trace, and come with both a
symbol being declared as well as an (unconstrained) initial value for
that symbol. The decision procedure must learn about the initial value
to include it in the model. Else, the trace value would just be question
marks.

Fixes: diffblue#6845
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Goto-symex: record value-at-declaration in the back-end tautschnig/cbmc
2 participants
@tautschnig @J0hnDaniel