[klee-dev] concretized symbolic size

[Guo,Shengjian]

Hi,

To my understanding, KLEE will maintain three states in handling a symbolic-size memory allocation:

State 1 -- tries to allocate a concrete size buffer, which is 128 by default.
State 2 (forked from State 1) -- assigns a NULL return value to the "calloc" function call.
State 3 (forked from State 2) -- the "concretized symbolic size" error state, as you witnessed.

Daniel.

On 2/13/21, 11:10, "klee-dev-bounces at imperial.ac.uk on behalf of Michael" <klee-dev-bounces at imperial.ac.uk on behalf of sp1ff at pobox.com> wrote:

    Hi,

    I'm using klee for the first time and am seeing it stop with the
    following error:

      KLEE: ERROR: EXITING ON ERROR:
      Error:  concretized symbolic size
      File:  libc/misc/dirent/opendir.c
      Line: 74
      assembly.ll line: 37501
      State: 48
      Stack:
              #000037501 in opendir (=94123719640632) at
              libc/misc/dirent/opendir.c:74
              #100027688 in apprentice_load (=94123697244416,
              =94123719640632, =0) at ../../src/apprentice.c:1394
              #200027566 in apprentice_1 (=94123697244416,
              =94123719640632, =0) at ../../src/apprentice.c:465
              #300027427 in file_apprentice (=94123697244416,
              =94123719026688, =0) at ../../src/apprentice.c:716
              #400033959 in magic_load (=94123697244416 ,
              =94123719026688) at ../../src/magic.c: 302
              #500002320 in load (=94123719026688, =0) at
              ../../src/file.c:479
              #600002034 in __klee_posix_wrapped_main (=4,
              =94123719649200) at ../../src/file.c:401
              #700037208 in __user_main (=7, =94123690168064,
              =94123690168128) at runtime/POSIX/klee_init_env.c:245
              #800001460 in __uClibc_main (=7, =94123690168064) at
              libc/misc/internals/__uClibc_main.c:401
              #900001626 in main (=7, =94123690168064)

    I *think* I understand what's happening. The code is calling
    calloc with a size argument that it read from the (symbolic) file
    system. Reading Executor::initializeGlobalAlias, klee correctly
    sees that this could be a very large number causing the
    allocation to fail.

    My question is: so what if it fails? In ths particular case,  the
    code under test would detect that & handle it. Would it not be
    better for klee to assume allocation failure,  return nil to the
    caller & let the chips fall where they may?

    Or am I missing something?

    Thanks for this great tool, BTW.

    --
    Michael <sp1ff at pobox.com>

    _______________________________________________
    klee-dev mailing list
    klee-dev at imperial.ac.uk
    https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: DBD43D8Fbdmailsec_embed_bg.png
Type: image/png
Size: 3756 bytes
Desc: DBD43D8Fbdmailsec_embed_bg.png
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20210213/8bf327d9/attachment.png>