Hidden attribute for malloc is inconsistent in traces

[markrtuttle]

CBMC version: 5.12.1
Operating system: MacOS
Exact command line resulting in the issue:
What behaviour did you expect:
What happened instead:

In error traces, for the function malloc, the function call is set to visible and the function return is set to hidden.

Can anyone help me debug this?

If I take the program main.c

#include <stdlib.h>
#include <assert.h>

main() {
  int x = malloc(sizeof(int));
  assert(0);
}

and run the command

cbmc --xml-ui --trace main.c

the xml output includes the tags

    <function_call hidden="false" step_nr="29" thread="0">
      <function display_name="malloc" identifier="malloc">
        <location file="&lt;builtin-library-malloc&gt;" line="6" working-directory="/private/tmp"/>
      </function>
      <location file="main.c" function="main" line="5" working-directory="/private/tmp"/>
    </function_call>

and

    <function_return hidden="true" step_nr="48" thread="0">
      <function display_name="malloc" identifier="malloc">
        <location file="&lt;builtin-library-malloc&gt;" line="6" working-directory="/private/tmp"/>
      </function>
      <location file="&lt;builtin-library-malloc&gt;" function="malloc" line="57" working-directory="/private/tmp"/>
    </function_return>

The call is visible and the return is hidden.

Similar incorrect behavior for the built-in function getenv

#include <stdlib.h>
#include <stdbool.h>

main() {
  bool b = getenv("S2N_DONT_MLOCK");
  assert(0);
}

<function_call hidden="false" step_nr="29" thread="0">
  <function display_name="getenv" identifier="getenv">
    <location file="&lt;builtin-library-getenv&gt;" line="14" working-directory="/private/tmp/test"/>
  </function>
  <location file="main.c" function="main" line="5" working-directory="/private/tmp/test"/>
</function_call>

<function_return hidden="true" step_nr="36" thread="0">
  <function display_name="getenv" identifier="getenv">
    <location file="&lt;builtin-library-getenv&gt;" line="14" working-directory="/private/tmp/test"/>
  </function>
  <location file="&lt;builtin-library-getenv&gt;" function="getenv" line="47" working-directory="/private/tmp/test"/>
</function_return>

But surprisingly correct behavior for the built-in function __builtin_alloca (the example below is for an invocation of the built-in __builtin_alloca nested within an invocation of the built-in getenv):

<function_call hidden="true" step_nr="522" thread="0">
  <function display_name="__builtin_alloca" identifier="__builtin_alloca">
    <location file="&lt;builtin-library-__builtin_alloca&gt;" line="5" working-directory="...deleted..."/>
  </function>
  <location file="&lt;builtin-library-getenv&gt;" function="getenv" line="42" working-directory="...deleted..."/>
</function_call>

<function_return hidden="true" step_nr="540" thread="0">
  <function display_name="__builtin_alloca" identifier="__builtin_alloca">
    <location file="&lt;builtin-library-__builtin_alloca&gt;" line="5" working-directory="...deleted..."/>
  </function>
  <location file="&lt;builtin-library-__builtin_alloca&gt;" function="__builtin_alloca" line="25" working-directory="...deleted..."/>
</function_return>

The hidden attribute of an xml step appears to come from a trace step which appears to come from an ssa step, and the hidden attribute on an ssa step appears to be set in goto_convert_functionst::hide. I can't see where the inconsistency would be coming from.

[hannes-steffenhagen-diffblue]

If you look here you’ll note it’s actually the entire body of malloc (including the return) that’s supposed to be hidden. The malloc function itself isn’t. This appears to be intentional, although I don’t know why it is that way.

[markrtuttle]

I saw that instance of __CPROVER_HIDE. I assumed it had a different semantics.

This is a real problem for me, because it makes it impossible to balance (in a principled way) function calls and returns in my representations of error traces.

But it also doesn't explain the visibility of the malloc steps that I elided in my initial example. If I take the program

#include <stdlib.h>
#include <assert.h>

typedef struct {int a; int b;} FOO;

main() {
  FOO *x = malloc(sizeof(FOO));
  assert(0);
}

then the error trace includes

<function_call hidden="false" step_nr="29" thread="0">
  <function display_name="malloc" identifier="malloc">
    <location file="&lt;builtin-library-malloc&gt;" line="6" working-directory="/private/tmp"/>
  </function>
  <location file="main.c" function="main" line="7" working-directory="/private/tmp"/>
</function_call>

<assignment assignment_type="actual_parameter" base_name="malloc_size" display_name="malloc::malloc_size" hidden="false" identifier="malloc::malloc_size" mode="C" step_nr="30" thread="0">
  <location file="main.c" function="main" line="7" working-directory="/private/tmp"/>
  <type>__CPROVER_size_t</type>
  <full_lhs>malloc_size</full_lhs>
  <full_lhs_value>8ul</full_lhs_value>
</assignment>

<assignment assignment_type="state" base_name="dynamic_object1" display_name="symex_dynamic::dynamic_object1" hidden="true" identifier="symex_dynamic::dynamic_object1" mode="C" step_nr="35" thread="0">
  <location file="&lt;builtin-library-malloc&gt;" function="malloc" line="38" working-directory="/private/tmp"/>
  <type>FOO</type>
  <full_lhs>dynamic_object1</full_lhs>
  <full_lhs_value>{ .a=0, .b=0 }</full_lhs_value>
</assignment>

<assignment assignment_type="state" base_name="dynamic_object1" display_name="symex_dynamic::dynamic_object1" hidden="false" identifier="symex_dynamic::dynamic_object1" mode="C" step_nr="36" thread="0">
  <location file="&lt;builtin-library-malloc&gt;" function="malloc" line="38" working-directory="/private/tmp"/>
  <type>FOO</type>
  <full_lhs>dynamic_object1.a</full_lhs>
  <full_lhs_value>0</full_lhs_value>
</assignment>

<assignment assignment_type="state" base_name="dynamic_object1" display_name="symex_dynamic::dynamic_object1" hidden="false" identifier="symex_dynamic::dynamic_object1" mode="C" step_nr="37" thread="0">
  <location file="&lt;builtin-library-malloc&gt;" function="malloc" line="38" working-directory="/private/tmp"/>
  <type>FOO</type>
  <full_lhs>dynamic_object1.b</full_lhs>
  <full_lhs_value>0</full_lhs_value>
</assignment>

<function_return hidden="true" step_nr="50" thread="0">
  <function display_name="malloc" identifier="malloc">
    <location file="&lt;builtin-library-malloc&gt;" line="6" working-directory="/private/tmp"/>
  </function>
  <location file="&lt;builtin-library-malloc&gt;" function="malloc" line="57" working-directory="/private/tmp"/>
</function_return>

So the call and the assignments to .a and .b are visible and the return is hidden. The internal steps are not hidden. This is actually the visibility I want to see in an error trace, because I want to see the values assigned to struct members in the error trace. I just need the function return to be visible, too.

[hannes-steffenhagen-diffblue]

So I have a small test like this:

#include <assert.h>

int get_x_plus_one(int x) {
__CPROVER_HIDE:
  return x + 1;
}

int main(void) {
  int x = 0;
  int y = get_x_plus_one(x);
  assert(y == 0);
}

And in the trace I get

    <function_call hidden="false" step_nr="29" thread="0">
      <function display_name="get_x_plus_one" identifier="get_x_plus_one">
        <location file="test.c" line="3" working-directory="/tmp"/>
      </function>
      <location file="test.c" function="main" line="10" working-directory="/tmp"/>
    </function_call>
    <assignment assignment_type="actual_parameter" base_name="x" display_name="get_x_plus_one::x" hidden="false" identifier="get_x_plus_one::x" mode="C" step_nr="30" thread="0">
      <location file="test.c" function="main" line="10" working-directory="/tmp"/>
      <type>signed int</type>
      <full_lhs>x</full_lhs>
      <full_lhs_value>0</full_lhs_value>
    </assignment>
    <assignment assignment_type="state" base_name="get_x_plus_one#return_value" display_name="get_x_plus_one#return_value" hidden="true" identifier="get_x_plus_one#return_value" mode="C" step_nr="31" thread="0">
      <location file="test.c" function="get_x_plus_one" line="5" working-directory="/tmp"/>
      <type>signed int</type>
      <full_lhs>get_x_plus_one#return_value</full_lhs>
      <full_lhs_value>1</full_lhs_value>
    </assignment>
    <function_return hidden="true" step_nr="32" thread="0">
      <function display_name="get_x_plus_one" identifier="get_x_plus_one">
        <location file="test.c" line="3" working-directory="/tmp"/>
      </function>
      <location file="test.c" function="get_x_plus_one" line="6" working-directory="/tmp"/>
    </function_return>

If I remove the __CPROVER_HIDE: the return is visible in the trace, like I would expect.

Which is in line with what I expect here, although I understand it’s not really what you want in this case. For clarification, what is the problem we are trying to solve? If it is just the attribute being set in the XML this could be fixed in post processing, I’m guessing though this isn’t why this is causing troubles for you?

We could easily ‘fix’ this by making sure that returns don’t get marked as hidden in the standard library, or just have a general preprocessing rule unsetting the hidden flag from returns when we see it, I just want to make sure that’d actually solve your problem (and I’d like to hear from @peterschrammel, @martin-cs or @kroening if they can think of any reasons why doing so might cause other problems) before doing this.

[hannes-steffenhagen-diffblue]

^- for clarification on the above questions: What I’m asking is, when are you expecting hidden to be set on calls and returns? I got the impression you are expecting returns to be visible or hidden whenever the corresponding function call is, is that correct?

[martin-cs]

@hannes-steffenhagen-diffblue some historical context... CPROVER_HIDE was an old feature when I started working on CPROVER. @tautschnig may have explained it to me back then but maybe I am confused about this. Note that it significantly pre-dates the change in how return statements were handled (i.e. remove returns).

I think its purpose is to omit the details modelling of the standard library from the traces. The traces are / were supposed to be human readable and just like you generally want your debugger to skip the internals of how malloc works, so the trace will omit the behaviour of our standard library 'implementation'. Is this a useful feature : probably because why should people need to know how our models work. Is CPROVER_HIDE a good way of providing this feature ... ummm... maybe? I am not sure if it is applied consistently throughout our modelled library. Maybe it should be used for other auto-generated things like function bodies?

My expectation is that it omits from the trace all steps from when it is called to the end of the function (including any function calls, not 100% sure about assertions). I think the caller should still have the call, return and assignment of return value.

You might also want to look at #1272, to quote @tautschnig This PR still includes a significant discussion about "internal" symbols. To be resolved by @peterschrammel and myself.

[hannes-steffenhagen-diffblue]

This is internally tracked as ADA-575

[hannes-steffenhagen-diffblue]

I’m closing this for now as it’s not obvious that there is anything that needs to be changed here, other than noting that the behaviour of internal flags can be a bit confusing to end users and should be better documented.