[klee-dev] See llvm-ir

Nowack, Martin m.nowack at imperial.ac.uk
Tue Jun 30 17:25:25 BST 2020


Hi,

There is currently no real option that does generate test0000.ll.
But you can workaround with the following option:

`-debug-print-instructions=`

Here the excerpt of the help output
  --debug-print-instructions=<value>                      - Log instructions during execution.
    =all:stderr                                           -   Log all instructions to stderr in format [src, inst_id, llvm_inst]
    =src:stderr                                           -   Log all instructions to stderr in format [src, inst_id]
    =compact:stderr                                       -   Log all instructions to stderr in format [inst_id]
    =all:file                                             -   Log all instructions to file instructions.txt in format [src, inst_id, llvm_inst]
    =src:file                                             -   Log all instructions to file instructions.txt in format [src, inst_id]
    =compact:file                                         -   Log all instructions to file instructions.txt in format [inst_id]

For you the option should be: `=all:file` or `=compact:file` combined with 
```
  --debug-compress-instructions                           - Compress the logged instructions in gzip format (default=false).
```

After that you just use each line and split it. As example the following line (=all:):

```
libc/string/memset.c:27 2:3226:1:  br label %9, !dbg !1210, !llvm.loop !1218
```

[src:src_line src_col:assembly.ll-line:path-id: llvm inst]

Hope that helps,

Martin


> On 30. Jun 2020, at 16:53, Yugesh Kothari <kothariyugesh at gmail.com> wrote:
> 
> Hi,
> 
> When I run KLEE, the llvm-ir (.ll) file is saved as assembly.ll
> However I would like to see the llvm instructions that Klee runs on for each call-path or trace of the program (like if there are 3 program paths that klee explores then I would like to get test00000.ll, test00001.ll, test00002.ll or something along those lines)
> 
> Is there a flag to get this information?
> 
> Thanks!
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev




More information about the klee-dev mailing list