Re: [klee-dev] Timed-out solver queries
Hi, On Tue, 14 Apr 2020 16:18:59 +0200 Hooman wrote: > As you rightfully mentioned I am not sure that any of the queries > time-out. However, I am also not sure if I should use all > -use-query-log=solver:smt2 -min-query-time-to-log=20 > --max-solver-time=20 options or klee will report timed-out queries > itself by default. (as -log-timed-out-queries option is true by > default). I also appreciate to have a response for my second question. 1. "-use-query-log=solver:smt2" enables query logging 2. "-min-query-time-to-log=20" sets a threshold to only log more expensive queries 3. "-max-solver-time=20" sets a time limit for the core (constraint) solver; keep in mind, that KLEE disables that limit in certain places 4. "-log-timed-out-queries" enables logging of timed out queries As you wrote, 4) is enabled by default. In KLEE it is used in a disjunction with 2). That means 2) prevents you from logging queries that didn't ran into the timeout. 1) is mandatory, otherwise KLEE doesn't log anything. On Tue, 14 Apr 2020 09:39:42 +0200 Hooman wrote: > 2- How is it possible to associate a timed-out query with certain > part of the code. So to understand what parts klee was not able to > cover. IMHO there is no mechanism in upstream KLEE. Easiest way is probably to modify KLEE's solver API: pass the corresponding state and print the current code location (prevPC). Kind regards, Frank ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Timed-out solver queries
*** This email originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. If you trust the sender, add them to your safe senders list https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for this address. *** Dear Professor Cadar, As you rightfully mentioned I am not sure that any of the queries time-out. However, I am also not sure if I should use all -use-query-log=solver:smt2 -min-query-time-to-log=20 --max-solver-time=20 options or klee will report timed-out queries itself by default. (as -log-timed-out-queries option is true by default). I also appreciate to have a response for my second question. Kind regards, Hooman On 2020-04-14 15:12, Cristian Cadar wrote: Hi Hooman, How do you know it is not working? Are you sure there are queries that time out? Best, Cristian On 14/04/2020 08:39, Hooman wrote: Dear all, I have two questions and I will appreciate any help. 1- I am wondering how is it possible to find out the percentage of timed-out queries out of all queries sent to solver? I am aware of the -log-timed-out-queries option. but apparently it is not working. because it is by default enabled but in a long klee execution (2 days) I don't see any logged timed-out queries. I also don't know where to look for it :) Moreover, I tried to combine -use-query-log=solver:smt2 -min-query-time-to-log=20 --max-solver-time=20 options together to kind of trying to log queries which took more than 20 seconds but solver-queries.smt2 file is empty after a long run. 2- How is it possible to associate a timed-out query with certain part of the code. So to understand what parts klee was not able to cover. Thank you very much. Kind regards, Hooman ___ 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] Timed-out solver queries
Hi Hooman, How do you know it is not working? Are you sure there are queries that time out? Best, Cristian On 14/04/2020 08:39, Hooman wrote: Dear all, I have two questions and I will appreciate any help. 1- I am wondering how is it possible to find out the percentage of timed-out queries out of all queries sent to solver? I am aware of the -log-timed-out-queries option. but apparently it is not working. because it is by default enabled but in a long klee execution (2 days) I don't see any logged timed-out queries. I also don't know where to look for it :) Moreover, I tried to combine -use-query-log=solver:smt2 -min-query-time-to-log=20 --max-solver-time=20 options together to kind of trying to log queries which took more than 20 seconds but solver-queries.smt2 file is empty after a long run. 2- How is it possible to associate a timed-out query with certain part of the code. So to understand what parts klee was not able to cover. Thank you very much. Kind regards, Hooman ___ 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] Timed-out solver queries
*** This email originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. If you trust the sender, add them to your safe senders list https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for this address. *** Dear all, I have two questions and I will appreciate any help. 1- I am wondering how is it possible to find out the percentage of timed-out queries out of all queries sent to solver? I am aware of the -log-timed-out-queries option. but apparently it is not working. because it is by default enabled but in a long klee execution (2 days) I don't see any logged timed-out queries. I also don't know where to look for it :) Moreover, I tried to combine -use-query-log=solver:smt2 -min-query-time-to-log=20 --max-solver-time=20 options together to kind of trying to log queries which took more than 20 seconds but solver-queries.smt2 file is empty after a long run. 2- How is it possible to associate a timed-out query with certain part of the code. So to understand what parts klee was not able to cover. Thank you very much. Kind regards, Hooman ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
