Re: [klee-dev] Question about KLEE Implementation on Collecting Symbolic Variables

2023-12-12 Thread Nowack, Martin
Hi Oleg,

Ah - yeah there is. The name is `klee::findSymbolicObjects` but it’s a bit 
hidden: 
https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/include/klee/Expr/ExprUtil.h#L38
 and 
https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/lib/Expr/ExprUtil.cpp#L123

In a nutshell, it’s a tree traversal and returns all used arrays.
This functionality is only really required in KLEE’s current implementation 
when a solver is called to generate assignments for expressions, e.g.:
https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/lib/Solver/STPSolver.cpp#L233.
 Therefore, it’s not really visible.

Best,
Martin





> On 12. Dec 2023, at 14:23, Oleg Sokolsky  wrote:
> 
> Hi Martin,
> 
> Thanks for the quick response.  Our question was slightly different, let me 
> clarify.  Given an instance of the Expr object, we want to obtain the set of 
> symbolic names used in that instance.  ExprPPrinter does it, for example, but 
> in a very specific way and, frankly, we struggled to understand how it works. 
>  We were wondering if there is a generic way to do it.  I was expecting a 
> visitor in the Expr hierarchy, or something similar, but could not find it.
> 
> Thanks again,
> Oleg
> 
> On 12/12/23 05:42, Nowack, Martin wrote:
>> Hi Haozhi Fan,
>> 
>> The symbolic names are generated using the call `klee_make_symbolic` 
>> indirectly or directly in your software under test.
>> KLEE tracks the memory object that have been associated with these calls 
>> (https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/lib/Core/Executor.cpp*L4435)
>>  and assigns it an array that has the same name or similar name that is 
>> unique.
>> Reading from this memory will result in read expressions that reference this 
>> array and are later used as part of the solver calls.
>> 
>> Best,
>> Martin
>> 
>>> On 11. Dec 2023, at 20:07, Haozhi Fan  wrote:
>>> 
>>> Dear klee-dev members,
>>> 
>>> I was wondering if you could share some insight into how KLEE collects the 
>>> set of symbolic names from an expression? Namely, how does KLEE generate 
>>> the kquery for a specific path condition and from which files should I be 
>>> looking for the details of such implementation? Thank you!
>>> 
>>> Best regards,
>>> Haozhi Fan
>>> ___
>>> 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 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


Re: [klee-dev] Question about KLEE Implementation on Collecting Symbolic Variables

2023-12-12 Thread Oleg Sokolsky

Hi Martin,

Thanks for the quick response.  Our question was slightly different, let 
me clarify.  Given an instance of the Expr object, we want to obtain the 
set of symbolic names used in that instance.  ExprPPrinter does it, for 
example, but in a very specific way and, frankly, we struggled to 
understand how it works.  We were wondering if there is a generic way to 
do it.  I was expecting a visitor in the Expr hierarchy, or something 
similar, but could not find it.


Thanks again,
Oleg

On 12/12/23 05:42, Nowack, Martin wrote:

Hi Haozhi Fan,

The symbolic names are generated using the call `klee_make_symbolic` indirectly 
or directly in your software under test.
KLEE tracks the memory object that have been associated with these calls 
(https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/lib/Core/Executor.cpp*L4435)
 and assigns it an array that has the same name or similar name that is unique.
Reading from this memory will result in read expressions that reference this 
array and are later used as part of the solver calls.

Best,
Martin


On 11. Dec 2023, at 20:07, Haozhi Fan  wrote:

Dear klee-dev members,

I was wondering if you could share some insight into how KLEE collects the set 
of symbolic names from an expression? Namely, how does KLEE generate the kquery 
for a specific path condition and from which files should I be looking for the 
details of such implementation? Thank you!

Best regards,
Haozhi Fan
___
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 mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


Re: [klee-dev] Question about KLEE Implementation on Collecting Symbolic Variables

2023-12-12 Thread Nowack, Martin
Hi Haozhi Fan,

The symbolic names are generated using the call `klee_make_symbolic` indirectly 
or directly in your software under test.
KLEE tracks the memory object that have been associated with these calls 
(https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/lib/Core/Executor.cpp#L4435)
 and assigns it an array that has the same name or similar name that is unique.
Reading from this memory will result in read expressions that reference this 
array and are later used as part of the solver calls.

Best,
Martin

> On 11. Dec 2023, at 20:07, Haozhi Fan  wrote:
> 
> Dear klee-dev members,
> 
> I was wondering if you could share some insight into how KLEE collects the 
> set of symbolic names from an expression? Namely, how does KLEE generate the 
> kquery for a specific path condition and from which files should I be looking 
> for the details of such implementation? Thank you!
> 
> Best regards,
> Haozhi Fan
> ___
> 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