[klee-dev] concretized symbolic size

[Michael]

Thx Daniel. Got that (the three states); my question is why does
your State 3 need to exist at all? This doesn not seem like an
error to me.

Guo,Shengjian <sjguoguo at baidu.com> writes:

> 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


-- 
Michael <sp1ff at pobox.com>