Re: [klee-dev] Guided Search - Help

and only one path with symbolic data. This path should be generated with a concrete file. This is I'm working on a searcher but I cannot do it properly for now. Thanks On Sat, Oct 20, 2018, 09:58 Andrew Santosa wrote: Hi Alberto, Please keep in mind that, although KLEE still tries to follow

Re: [klee-dev] Guided Search - Help

Hi Alberto, Please keep in mind that, although KLEE still tries to follow the seed's path, the state it maintains is no longerthe concrete state, but the symbolic state. So, the symbolic file A no longer contains a concrete RGB value at coordinate(1, 1), but instead a symbolic value. By

Re: [klee-dev] Guided Search - Help

Hi Sang,  Yes -only-replay-seed could be the option to use instead of -only-seed, but you don't need to re-run KLEE for each seed though. There's -seed-out-dir option where you can specify a directory of seeds.  Best, Andrew  Sent from Yahoo Mail on Android On Tue, Oct 16, 2018 at 7:50 AM,

Re: [klee-dev] Guided Search - Help

w searcher in order to 'execute,' queries at runtime on the code. Thanks a lot! Alberto On Mon, Oct 15, 2018, 01:19 Andrew Santosa wrote: Hi Alberto,  Thank you for describing your problem. I had submitted this PR some while ago:  https://github.com/klee/klee/pull/956 Basically I would use gen-bout i

Re: [klee-dev] Guided Search - Help

Hi Alberto,  Thank you for describing your problem. I had submitted this PR some while ago:  https://github.com/klee/klee/pull/956 Basically I would use gen-bout implemented in the PR to create a ktest file using concrete inputs, then use the ktest file as a seed. In this way, all inputs will be

Re: [klee-dev] Built Program Using Gcov in KLEE

Hi Norlina, You first need to download and unpack Coreutils 6.11 in the following way: wget http://ftp.gnu.org/gnu/coreutils/coreutils-6.11.tar.gztar zxvf coreutils-6.11.tar.gzcd coreutils-6.11 Only after executing the above commands you can proceed with mkdir: mkdir obj-gcovcd

Re: [klee-dev] Test cases generated for symbolic file

, 2018 at 9:32 PM, Andrew Santosa wrote: > Hi Sang, > > I urgently need a tool like you mentioned, so I wrote one myself within KLEE > source tree. You can find the source as tools/gen-bout.cpp in the gen-bout > branch > of my KLEE fork: https://github.com/domainexpert/klee/tree/ge

Re: [klee-dev] Test cases generated for symbolic file

Hi Sang, I urgently need a tool like you mentioned, so I wrote one myself within KLEEsource tree. You can find the source as tools/gen-bout.cpp in the gen-bout branchof my KLEE fork: https://github.com/domainexpert/klee/tree/gen-bout I don't exactly know the answer to your question. For normal

Re: [klee-dev] Want to replay ".ktest" files from a single text file

Hi Sanghu, You don't seem to be using klee-replay here. Otherwise, instead of invoking a.out you would have invoked klee-replay, with a.out as its argument. Moreover, you can't just expect klee-replay to work on a single file containing all the ktest files by simple appending. I don't think

Re: [klee-dev] Symbolic Expression for Variable

Hi Ridwan, I think you can do this using klee_print_expr() without modifying KLEE.For example (from [klee-dev] question about klee_print_expr): | | | | [klee-dev] question about klee_print_expr | | | #include int main(int arc, char **argv)   { int a,b;

Re: [klee-dev] Concolic execution with Klee

Hi Sang, I don't think that is possible in KLEE since firstly, given concrete inputsit will likely simplify the constraints into a constant (true/false). Secondly,it does not collect the constraints into the path condition whenever it candecide that a branch can only go one way, which is to

Re: [klee-dev] How to avoid calling the solver if the branch is known at run-time

Hi Charitha, I think you would need to do the modification in Executor::fork(). You would notice within that function there is the following three lines: solver->setTimeout(timeout); bool success = solver->evaluate(current, condition, res); solver->setTimeout(0); I would try to replace those

Re: [klee-dev] KLEE Memory Mapping

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

Re: [klee-dev] How klee deal with index of array is symbolic?

Hi Qingyang, I think what you want to know is how to solve array constraints, e.g., x > a[x] in your example. You can have a look at the following paper on STP, which is one of the backend solvers KLEE uses: https://ece.uwaterloo.ca/~vganesh/Publications_files/vg2007-STP-CAV.pdf Section 3

Re: [klee-dev] Space program in KLEE Using concolic method

Hi Norlina, Yes, generally it is possible for KLEE to generate string inputs, including a program written in a particular language.For the space program that you are testing, I guess that you would need to provide a symbolic file as an input program.KLEE will then replace the content of the

Re: [klee-dev] Using <z3++.h> in headers

Hi Charitha, If I were you, I would try to run cmake in the following way: CXXFLAGS="-fexceptions" cmake ... Regards,Andrew On Wednesday, 7 February 2018, 4:19:31 am GMT+8, Charitha Saumya wrote: Hi all, I want use z3 C++ APIs in a C++ source file I have placed

Re: [klee-dev] Concretizing internal variables in coreutils experiment

Hi Charitha, You can try to run the configure script of Coreutils in the following way: CFLAGS=-I LDFLAGS=-L LIBS=-lkleeRuntest ./configure where is where libkleeRuntest.so* live. You may need to set LD_LIBRARY_PATH to for running the produced executable. I hope this helps. Andrew On

Re: [klee-dev] Constraints in SSA from

Hi Charitha, Perhaps others can provide better answer, but I believe it will involve significanteffort to implement what you want in KLEE. Since you also asked for other approaches, I am reminded of work I did years backon symbolic execution using constraint logic programs, which perhaps is

Re: [klee-dev] measuring the coverage using the test cases testN.TYPE.err

Hi BNM, If I understand correctly, here there are two categories of test suites discussed: one contains the test suite generatedby KLEE, and another contains test suites that come with the program itself. If you want to measure the coveragespecifically achieved by KLEE, then you should only run

Re: [klee-dev] Add a new solver to klee

Dear Qingyang, Perhaps you may want to first look the comments in SolverImpl.h. For this, you can generate the doxygen documentation in the following way: make doxygen The documentation for SolverImpl class should be here: docs/doxygen/html/classklee_1_1SolverImpl.html Regarding the

Re: [klee-dev] Is possible to mark a function as uninterpreted function?

t;focus more on other parts of the program. But the downside is it introduces >imprecision and false alarms. I wonder how KLEE devs/users view this >imprecision (as I'm quite new around here). Thanks! > >Regards, >Yude > >On Fri, Dec 23, 2016 at 8:11 PM, Andrew Santosa <asantosa

Re: [klee-dev] Is possible to mark a function as uninterpreted function?

™ smartphone Andrew Santosa wrote > > > On Friday, 23 December 2016, 14:37, Yude Lin > <yu...@student.unimelb.edu.au> wrote: > > > Hi Guys, > >For a function in the program source code, i.e., not a library function, >do you think we have reaso

Re: [klee-dev] Is possible to mark a function as uninterpreted function?

Dear Javier, I believe the straight answer is no. I think Z3, which is now supported by KLEE, supports uninterpreted functions, so itseems possible to implement this feature, but the question is why should C functionbe mathematical function? What if the C function has side effects? However, a

Re: [klee-dev] How to get （or capture ） the value of replaying a test case and the usage of KLEE

On no. 4, I think Lei's approach is probably fine for their purpose, assuming what needs to be accomplished here is simply making a, b, and c represent nondeterministic int input. But since scanf is a function that reads from the standard input, if one goes through the Coreutils tutorial

Re: [klee-dev] Inline assembly, concurrency

I think this idea has a merit. If we replaced many library code even with slightly different (or even slightly wrong) implementation in order to get the KLEE-executable bc, then KLEE execution can remain symbolic for longer before switching to concrete, potentially gaining better coverage. 

Re: [klee-dev] Solving path constraints incrementally

Hi Sergey, Although this is only a guess, my guess is that this is because KLEE is worklist-based, where an item in the worklist represents an execution state. The executor (Executor class) has a field searcher, whose runtime type determines the kind of exploration strategy used by KLEE.

Re: [klee-dev] confuse how klee collect symbolic constraints

Dear Qingkun, I believe the following is close to your original source: #include #include int get_sign(int x) {   if (x == 0) {     return 0;   }   if (x < 0) {     return -1;   }   return 1; } int main() {   int a;   klee_make_symbolic((char *) , sizeof(int), "a");   return get_sign(a); }

Re: [klee-dev] Will KLEE Be Able to Do Floating-Point Error Reasoning?

Sorry, following is the correct link to the previous email thread that I mentioned (which may have disappeared from my email). http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg02334.html Best, Andrew On Friday, 17 June 2016, 11:50, Andrew Santosa <santosa_1...@yahoo.com> wrote:

[klee-dev] Will KLEE Be Able to Do Floating-Point Error Reasoning?

Many thanks to Cristian for his reply to my previous question in this thread: Re: [klee-dev] Floating-Point Symbolic Execution |   | |   | |   |   |   |   |   | | Re: [klee-dev] Floating-Point Symbolic ExecutionHi Andrew,KLEE-FP/KLEE-CL (https://srg.doc.ic.ac.uk/projects/klee-cl/) is targeted

[klee-dev] Floating-Point Symbolic Execution

Dear All, In KLEE, it seems symbolic floating point variables are simply converted to int and grounded to 0. I am wonderingwhat is the current state of floating point symbolic execution support in KLEE? I know there has been some workon KLEE-FP in the past, but does it actually check path

Re: [klee-dev] Some questions about SMT solvers

Hi Fabrizio, 1. Your example is missing from your email, but I think validity in KLEE means that any valuation is a model (as in model theory). Whereas it seems your understanding of validity (some valuations are models) is more commonly known as satisfiability.2. I don't recall ever seeing

Re: [klee-dev] where is the class for "EqExpr" located

Hi Sumit, It's declared in include/klee/Expr.h using macro COMPARISON_EXPR_CLASS.Note that below the definition of that macro there is a line that says COMPARISON_EXPR_CLASS(Eq) Which actually declares EqExpr. Best,Andrew On Thursday, 24 March 2016, 4:18, Sumit Kumar

Re: [klee-dev] how to get this constraint in klee

I think you can't.In KLEE, each state is represented as a mapping of program variables to an expression in terms of initial symbolic values.This is probably better in terms of performance as the number of program variables is likely to be smaller than the length of the path. Storingthe