[klee-dev] How to determine the concretized size when dealing with malloc()

[Cristian Cadar]

Hi Austin,

Sorry to see that nobody has answered your email.  I'm not sure what you 
are trying to do though.  Are you trying to make KLEE choose a specific 
size?

(That code is a bit broken, btw.  We fixed it in some extensions but 
haven't managed to merge the changes into the mainline yet.)

Best,
Cristian

On 18/04/2022 10:55, Wang Austin wrote:
> Hello klee-dev members,
> 
> I'm working on a project involving KLEE and SMT solvers. We are 
> collecting queries from KLEE using the v2.2 klee docker image with the 
> "--use-query-log=solver:smt2" option. I observed that the queries 
> collected are not always complete when KLEE dealing with malloc(), and 
> KLEE would throw an error:
> ...
> KLEE: ERROR: tif_unix.c:334: concretized symbolic size
> ...
> 
> I'm expecting to determine the concretized size for malloc() in 
> accordance with the value of size in the actual execution and check if 
> the queries are more complete in this case.
> 
> I checked the source code (klee/lib/Core/Executor.cpp), finding that 
> KLEE would "optimize" when the size is symbolized. And I tried the 
> "--allocate-determ" option for memory management according to the 
> document, which I thought would determine the size to a specific value 
> and resolve the error, whereas, it doesn’t seem to be running right, 
> here are the results.
> 
> 1) Normal execution:
> ...
> KLEE: ERROR: tif_unix.c:334: concretized symbolic size
> KLEE: NOTE: now ignoring this error at this location
> KLEE: seeding done (0 states remain)
> ...
> 
> 2) Execution with --allocate-determ=1 --allocate-determ-size=10:
> ...
> KLEE: ERROR: tif_unix.c:334: concretized symbolic size
> KLEE: NOTE: now ignoring this error at this location
> KLEE: seeding done (0 states remain)
> KLEE: Deterministic memory allocation starting frow 0x7ff30000000
> ...
> 
> The size still got concretized or perhaps I misunderstood the usage of 
> the "--allocate-determ" option.
> 
> I’m wondering if there is a way to "determine the concretized size to a 
> specific value when malloc()" or "NOT to optimize the size", so I can 
> collect queries with more completeness using KLEE.
> 
> Best Regards,
> Austin Wang
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev