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

2022-06-16 Thread 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 0x7ff3000
...

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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


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

2022-04-19 Thread Wang Austin
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 0x7ff3000
...

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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev