Infinite loop (?) on symbolic execution

[mikhailramalho]

OBS: the new llvm frontend is required in order to reproduce this error.

The program in [1] causes esbmc to hang during symbolic execution. Maybe an infinite loop.

Symex trace shows:

    num_total_threads=0;
    num_threads_running=0;
    __ESBMC_deallocated=ARRAY_OF(FALSE);
    __ESBMC_alloc=ARRAY_OF(FALSE);
    p=&{ 2, 4 }[0];
    __ESBMC_alloc_size=ARRAY_OF(0);
    pc=&{ 1f, 10f, 100f }[0];
    __ESBMC_is_dynamic=ARRAY_OF(FALSE);
    FUNCTION_CALL:  pthread_start_main_hook()
    ATOMIC_BEGIN
    num_total_threads=num_total_threads + 1;
    num_threads_running=num_threads_running + 1;
    ATOMIC_END
    END_FUNCTION
    FUNCTION_CALL:  main()
    signed int n;
    n=2;
    signed int * p;
    p=&n;
    p=&{ *p, 0 }[0];

[jmorse]

What's the reference code here, [1] isn't obvious.

[mikhailramalho]

Ops.

[1] https://gist.github.com/mikhailramalho/0472f7e2e407082248e7

[jmorse]

Hi,

Reconstructed irep on the rhs of the assignment looks like this:

address_of
* pointer_obj : index
    * source_value : constant_array
        * members :
          0: dereference
            * pointer : symbol
                * name : c::test::main::2::p
                * renamelev : Level 0
                * level1_num : 0
                * level2_num : 0
                * thread_num : 0
                * node_num : 0
                * type : pointer
                  * subtype : signedbv
                      * width : 32
            * type : signedbv
              * width : 32
          1: constant_int
            * constant_value : 0
            * type : signedbv
              * width : 32

        * type : array
          * subtype : signedbv
              * width : 32
          * array_size : constant_int
              * constant_value : 2
              * type : signedbv
                * width : 32
          * size_is_infinite : false
    * index : constant_int
        * constant_value : 0
        * type : signedbv
          * width : 32
    * type : signedbv
      * width : 32
* type : pointer
  * subtype : signedbv
      * width : 32

The issue seems to be that we're not expecting an unevaluated dereference to crop up /inside/ the contents of the constant array. The dereference code, in the case of an index, is currently geared for resolving a dereference in the index-operand (here zero) or the array source, i.e. resolving what foo is in "p->foo[0]". It doesn't expect to be handed an array of raw values -- it assumes that the contents have already had any dereferences resolved in a previous assignment instruction that initialized the array being accessed.

We could hack it to consider this case; CBMC however creates a new variable to represent the temporary array, avoiding this problem by having a separate instruction in which the dereferences are flushed out. In addition, this resolves a memory uncertainty: you're taking the address of a temporary literal (which seems bad) and that should be seen as a local variable to that function (so that, for example, it's pointer could be invalidated when it goes out of scope). The current way you're doing it, by taking the address of a constant array, won't achieve that (and may lead to explosions later down the model checking chain, not certain).

IMO that's the best solution: create a new temporary array and assign values to it, then perform the assignment to p in a different instruction.

[jmorse]

This..... is still an issue as of 2017. Curses.

[github-actions[bot]]

Stale issue message

[github-actions[bot]]

Stale issue message