Discussion:
Help with collecting coverage information
(too old to reply)
Breno Miranda
2014-08-21 16:40:32 UTC
Permalink
Dear all,

I was playing around with klee using a toy example of the algorithm that
tells the triangle type according to its angles' values (code attached) to
get acquainted with the klee_assume method.
If I want to restrict KLEE to generate test cases that will explore only
isosceles triangles, I could use a klee_assume like this one:

klee_assume((a + b > c & a + c > b & b + c > a) & (a > 0 & b > 0 & c > 0) &
(a + b + c == 180) & (a == b | b == c | a == c) & !(a == b & b == c));

When KLEE explores the attached code, it outputs three test cases:
TC #1: a=80, b=80, *c=20*
TC #2: *a=20*, b=80, c=80
TC #3: a=80, *b=20*, c=80

Each time a different variable (a, b, c) is assigned to the "different"
angle (20). This is perfectly fine as KLEE is providing the three different
ways in which an isosceles triangle can be achieved to guarantee *full path
coverage*.

When considering branch coverage, however, the 3 test cases explore the
"same" branch (I understand that due to some C characteristics, the actual
number of branches is not exactly the number of branches associated with
the conditional statements, but here I am referring to the source-level
branches).

*Is there any way I could identify that these 3 test cases generated by
KLEE explore the same (source-level) branch?*

My initial thought was to get the information from .cov files generated for
each test cases but, differently from what I was expecting, it is not the
case that the three test cases explore the same lines:
TC #1: 7,8,*12,13,22*,30,31,32,35
TC #2: 7,8,11,30,31,32,35
TC #3: 7,8,11,30,31,32,35

Any ideas would be highly appreciated.

I look forward to hearing from you.

--
Yours sincerely,
Breno Miranda
Daniel Liew
2014-08-21 17:10:12 UTC
Permalink
Hi
Post by Breno Miranda
My initial thought was to get the information from .cov files generated for
each test cases but, differently from what I was expecting, it is not the
TC #1: 7,8,12,13,22,30,31,32,35
TC #2: 7,8,11,30,31,32,35
TC #3: 7,8,11,30,31,32,35
The lines are not the same because you've used short circuit operators
in the if statement so there are more branches than you might think. I
would advise that you take a look at the LLVM IR for your program
because will shows you the branches that KLEE actually sees. If you
look inside ``klee-last`` there is a file called assembly.ll . This is
the program that KLEE interpreted as LLVM IR. You can read the LLVM IR
file but some times it can be quite hard to visualise what's going on
so you can use LLVM's opt tool to visualise this IR file

$ opt -analyze -view-cfg klee-last/assembly.ll

which will launch an application (e.g. xdotpy if it in your PATH when
you built LLVM) to view the cfg. It will launch a program one at a
time for each function in assembly.ll

or

$ opt -analyze -dot-cfg klee-last/assembly.ll

which will spit out a .dot file per function. You can then open the
file of interest using a graphviz viewer of your choice (I prefer
xdotpy).

This will show you the control flow graph for each function definition
in assembly.ll

If you are unfamiliar with LLVM IR take a look at the Language
Reference ( http://llvm.org/docs/LangRef.html )

Hope that helps.

Thanks,
Dan.
Breno Miranda
2014-08-21 18:55:55 UTC
Permalink
Hi Daniel,

Thank you very much for your prompt and very detailed answer! I appreciate
it!

I'm not familiar with LLVM, so thanks for the reference material.

I'll try your suggestions and I'll get back to you if I have other
questions.

Thank you again!

__
Yours sincerely,
Breno Miranda
Post by Daniel Liew
Hi
Post by Breno Miranda
My initial thought was to get the information from .cov files generated
for
Post by Breno Miranda
each test cases but, differently from what I was expecting, it is not the
TC #1: 7,8,12,13,22,30,31,32,35
TC #2: 7,8,11,30,31,32,35
TC #3: 7,8,11,30,31,32,35
The lines are not the same because you've used short circuit operators
in the if statement so there are more branches than you might think. I
would advise that you take a look at the LLVM IR for your program
because will shows you the branches that KLEE actually sees. If you
look inside ``klee-last`` there is a file called assembly.ll . This is
the program that KLEE interpreted as LLVM IR. You can read the LLVM IR
file but some times it can be quite hard to visualise what's going on
so you can use LLVM's opt tool to visualise this IR file
$ opt -analyze -view-cfg klee-last/assembly.ll
which will launch an application (e.g. xdotpy if it in your PATH when
you built LLVM) to view the cfg. It will launch a program one at a
time for each function in assembly.ll
or
$ opt -analyze -dot-cfg klee-last/assembly.ll
which will spit out a .dot file per function. You can then open the
file of interest using a graphviz viewer of your choice (I prefer
xdotpy).
This will show you the control flow graph for each function definition
in assembly.ll
If you are unfamiliar with LLVM IR take a look at the Language
Reference ( http://llvm.org/docs/LangRef.html )
Hope that helps.
Thanks,
Dan.
Loading...