I see. However, I think it's important to understand in a bit more
detail how KLEE operates if you want to report precise measurements. In
particular, note that the fact that we have two caches and that a branch
query (on which the first cache operates) is broken down into two
satisfiability queries may mean that your current formula might need to
be adjusted, depending on what exactly you would like to measure.
Best,
Cristian
On 17/10/14 17:17, Andrea Aquino wrote:
Thank you very much Cristian,
fortunately the programs I am dealing with at the moment are quite
small and KLEE takes a reasonable amount of time to perform its task.
When I will deal with bigger programs I will definitely have a look
at the SolverStats.cpp file :)
Best regards, Andrea Aquino
On 17 Oct 2014, at 18:03, Cristian Cadar <[email protected]>
wrote:
Hi Andrea,
This seems reasonable, but could be quite expensive, as you have to
log all these queries. A better way to do it would be to use the
statistics in lib/Solver/SolverStats.cpp (note that there are two
caches in KLEE, as explained briefly in our OSDI'08 paper and in a
bit more detail in CAV'13).
Best, Cristian
On 17/10/14 16:31, Andrea Aquino wrote:
Dear all,
I analyzed some programs using KLEE and I am trying to calculate
how many cache hits the cache implemented in KLEE gets.
I am currently doing it counting the formulas in the
all-queries.smt2 file (AQ), counting the formulas in the
solver-queries.smt2 file (SQ) and then calculating the percentage
of hits as: [(AQ - SQ) / AQ] * 100
Is this correct or am I doing some wrong assumption on the
content of these two files? If it is the case, what is the
easiest way to do it?
Best regards, Andrea Aquino
_______________________________________________ klee-dev mailing
list [email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing
list [email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
