[klee-dev] KLEE Memory Mapping

[Andrew Santosa]

Hi Daniel,

Following is several ways that I know how a symbolic variable gets its name, but
none of them depends on debug information.

1. A variable is named by the user via klee_make_symbolic() API,
    however in a loop, indexed variants of the same variable may be produced.
    You can have a look at the SpecialFunctionHandler::handleMakeSymbolic().

2. Variables argN for some N are produced by symbolic command-line arguments.
   Refer to this tutorial on symbolic environment:
   Symbolic Environment · KLEE

| 
| 
|  | 
Symbolic Environment · KLEE


 |

 |

 |




3. A symbolic file created with -sym-files option such as "A" produces variables
    like "A-data" or "A-data-stat". You may also want to refer to the same tutorial.

4. const_arrN which KLEE creates when it cannot find a symbolic variable to read
    from. See ObjectState::getUpdates().

5. model_version variable which is generated with the option -posix-runtime and is
    constrained to equal 1. 
Best,
Andrew
 

    On Wednesday, 25 April 2018, 1:19:38 am GMT+8, Daniel Schwartz <d.schwartz at columbia.edu> wrote:  
 
 Hi,
I'm trying to understand how KLEE maps symbolic variables to expressions. How does KLEE get a unique name for each variable? Without debug information, I don't see how to trivially get one from an LLVM Instruction.

Can someone please explain this to me, or if it's too complicated for an email, point me in the right direction in the source code?



Thanks,Daniel Schwartz_______________________________________________
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