[klee-dev] The algorithm of Min-Dist-to-Uncovered Searcher
Hi all, I saw the md2u(Min-Dist-to-Uncovered) search heuristic in KLEE. In my opinion, md2u is the strategy that when selecting a state KLEE aways consider about the states have the minimum distance to uncovered part of the code. I read the source code of the MinDistToUncovered, but I'm still confused about the implement of computeMinDistToUncovered function. So I have two questions: 1. If someone could give the algorithm description about how to compute the minimum distance to uncovered part in KLEE or explain the implement of computeMinDistToUncovered function in KLEE. And if I could compute the distance between two instructions in KLEE. 2. What's the difference between CovNew and MD2U search heuristic ? Thanks a lot. Chengyu Zhang -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: 18685412181 Mail: dale.chengyu.zh...@gmail.com ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] The algorithm of Min-Dist-to-Uncovered Searcher
Hi all, After reading the source code, I have figured out how MD2U strategy works. The main idea of MD2U strategy is : Init every uncovered instruction min-distance-to-uncovered value to 1, every covered instruction min-distance-to-uncovered value to 0; Iterate each instruction, inherit min-distance-to-uncovered value from it's successor, until no more min-distance-to-uncovered value have changed. Then we can get the min-distance-to-uncovered for every instruction. But I have a question that why KLEE set uncovered-update interval default to 30 ticks rather than every time we do stepInstruction function? Is it because of low efficiency or other reasons? Best regards, Chengyu 2016-11-02 18:00 GMT+08:00 Chengyu Zhang : > Hi all, > > I saw the md2u(Min-Dist-to-Uncovered) search heuristic in KLEE. > In my opinion, md2u is the strategy that when selecting a state KLEE aways > consider about > the states have the minimum distance to uncovered part of the code. I read > the source code > of the MinDistToUncovered, but I'm still confused about the implement of > computeMinDistToUncovered function. > > So I have two questions: > > 1. If someone could give the algorithm description about how to compute > the minimum distance to uncovered part in KLEE or explain the implement of > computeMinDistToUncovered function in KLEE. And if I could compute the > distance between two instructions in KLEE. > > 2. What's the difference between CovNew and MD2U search heuristic ? > > Thanks a lot. > Chengyu Zhang > > -- > 张枨宇 Chengyu Zhang > East China Normal University > School of Computer Science and Software Engineering > Tel: 18685412181 > Mail: dale.chengyu.zh...@gmail.com > -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: 18685412181 Mail: dale.chengyu.zh...@gmail.com ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] The algorithm of Min-Dist-to-Uncovered Searcher
Hi Martin, Thanks for your reply. I'm interested in giving a patch to improve the situation, and I would like to try. Here is my idea: First, I think we could update min-distance-to-uncovered dynamically when we need, such as there are no candidate state covering new instruction and need to be decided which state should be selected. So that we needn't update periodically, instead more effectively. Second, We could just calculate min-distance-to-uncovered for candidate instructions(The pc of candidate states) using Dijkstra's algorithm rather than iterating all instructions. In this way, we may decrease the cost of updating. Is my idea reasonable? Thanks and Cheers, Chengyu 2016-11-21 21:13 GMT+08:00 Martin Nowack : > Hi Chengyu, > > On 18 Nov 2016, at 15:16, Chengyu Zhang > wrote: > > > > But I have a question that why KLEE set uncovered-update interval > default to 30 ticks rather than every time we do stepInstruction function? > > Is it because of low efficiency or other reasons? > > > > Well, the current implementation is quite costly, therefore the high value > of 30s. > This might be less of a problem with older machines but becomes more > problematic with newer ones, > as they number of instructions per second might be much higher. So you > update less often and might > work more often with outdated information. > So you should vary that number according to your needs. > > (Of course, patches, which improve that situation are always welcome ;) ) > > Cheers, > Martin > > > > Best regards, > > Chengyu > > > > 2016-11-02 18:00 GMT+08:00 Chengyu Zhang : > > Hi all, > > > > I saw the md2u(Min-Dist-to-Uncovered) search heuristic in KLEE. > > In my opinion, md2u is the strategy that when selecting a state KLEE > aways consider about > > the states have the minimum distance to uncovered part of the code. I > read the source code > > of the MinDistToUncovered, but I'm still confused about the implement of > computeMinDistToUncovered function. > > > > So I have two questions: > > > > 1. If someone could give the algorithm description about how to compute > the minimum distance to uncovered part in KLEE or explain the implement of > computeMinDistToUncovered function in KLEE. And if I could compute the > distance between two instructions in KLEE. > > > > 2. What's the difference between CovNew and MD2U search heuristic ? > > > > Thanks a lot. > > Chengyu Zhang > > > > -- > > 张枨宇 Chengyu Zhang > > East China Normal University > > School of Computer Science and Software Engineering > > Tel: 18685412181 > > Mail: dale.chengyu.zh...@gmail.com > > > > > > > > -- > > 张枨宇 Chengyu Zhang > > East China Normal University > > School of Computer Science and Software Engineering > > Tel: 18685412181 > > Mail: dale.chengyu.zh...@gmail.com > > ___ > > klee-dev mailing list > > klee-dev@imperial.ac.uk > > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > --- > Martin Nowack > Research Assistant > > Technische Universität Dresden > Computer Science > Institute of Systems Architecture > Systems Engineering > 01062 Dresden > > Phone: +49 351 463 39608 > Email: martin_now...@tu-dresden.de > > > -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: +86 18685412181 Mail: dale.chengyu.zh...@gmail.com ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Information on reproducing exeperimetation on Coreutils.6.10 with Klee.
Hi Habib, You could read the "Per-path files" chapter in the link: http://klee.github.io/docs/files/ The file test..err may be the file you want. Best, Chengyu 2016-12-12 19:45 GMT+08:00 el habib Boudjema : > Thank you, for your fast answer. > Also I have another question : How to get the right test case that > triggered the bug ? > > 2016-12-12 11:56 GMT+01:00 Andrea Mattavelli > : > >> Hi, >> you can find the options used to run KLEE here: http://klee.github.io/do >> cs/coreutils-experiments/ >> >> Best, >> Andrea >> >> On 12 Dec 2016, at 10:37, el habib Boudjema >> wrote: >> >> Hello, >> >> I am a PhD student, I am using the Klee engine. >> >> I want to know how to reproduce the experimentation you did on Coreutils >> 6.10. For instance I successfully run the simple experimentation you show >> on : http://klee.github.io/tutorials/testing-coreutils/, and want to >> know what are precisely the options you gave to the tool to discover the >> bugs you found. >> >> >> Thank you in advance for your response. >> >> ___ >> 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 > > -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: +86 18685412181 Mail: dale.chengyu.zh...@gmail.com ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] use klee-fp support float
Hi， KLEE can't deal with the float in this version. KLEE will convert float to const when meet float. Because of the limited of STP solver (can't deal with the float constraints) , the develop group of KLEE is trying to add Z3 solver support in KLEE. But the feature have not completed yet. Best, Chengyu 2016年12月30日 +0800 07:01 Cx Qingyang ，写道： > Hi,I have successfully build klee-fp,but i don't know how to make it support > float.For example,in the get_sign.c,i change the int x to > float x.Firstly klee-gcc.cde -I ../../include -emit-llvm -c -g > get_sign.c,then klee.cde get_sign.o,and i get a warning :silently > concretizing expression(ReadLSB w32 0 a) to value 0. > > ___ > 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] How to limit unrolling loops times
Hi all, I want KLEE stops unrolling loop when meet the unrolling loop limit (For example, 10 times). I used "-max-depth" option to deal with the problem, but it can't be suitable for every program and it's not a good solution. I have found the "-unroll-threshold" option in "-help-hidden" can deal with the problem (maybe), but it seems doesn't work. Is there any options could deal with the problem? Or if anyone could tell me how to use "-unroll-threshold" option? Thanks forward, Chengyu -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: +86 18685412181 Mail: dale.chengyu.zh...@gmail.com ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] How to limit unrolling loops times
Hi Cristian, Thanks for your suggestion, I will try to make a heuristics searcher to solve the problem. Best, Chengyu 2017-01-11 6:28 GMT+08:00 Cristian Cadar : > Hi Chengyu, KLEE is not aware of loops per se, so there's no easy way to > achieve what you want. You might want to look instead at the search > heuristics that KLEE provides, to see if they are good enough for your > purposes. > > Best, > Cristian > > > On 04/01/2017 11:50, Chengyu Zhang wrote: > >> Hi all, >>I want KLEE stops unrolling loop when meet the unrolling loop limit >> (For example, 10 times). I used "-max-depth" option to deal with the >> problem, but it can't be suitable for every program and it's not a good >> solution. >>I have found the "-unroll-threshold" option in "-help-hidden" can >> deal with the problem (maybe), but it seems doesn't work. Is there any >> options could deal with the problem? Or if anyone could tell me how to >> use "-unroll-threshold" option? >> >> Thanks forward, >> Chengyu >> >> -- >> 张枨宇 Chengyu Zhang >> East China Normal University >> School of Computer Science and Software Engineering >> Tel: +86 18685412181 >> Mail: dale.chengyu.zh...@gmail.com <mailto:dale.chengyu.zh...@gmail.com> >> >> >> ___ >> 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 > -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: +86 18685412181 Mail: dale.chengyu.zh...@gmail.com ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] (Re)implementing a randomized fork
Hi Sean,
You could try random search strategy builded in KLEE with the command:
klee -search=random-state your_file_name.bc.
I think this feature would achieve your goal. If the strategy doesn't work
or can't satisfy you, you could inherit the Searcher Class in
/lib/Core/Searcher.cpp & /lib/Core/Searcher.h to implement your strategy
and register in /lib/Core/UserSearcher.cpp.
If you have any question about how to implement an own Searcher, you can
ask me.
Cheers,
Chengyu
2017-01-18 5:30 GMT+08:00 Sean Heelan :
> Hi,
>
> For various reasons a randomised fork would be beneficial when using
> batched searching. In case it isn't apparent, what I mean by a 'randomised
> fork' is randomly selecting whether the conditions for the true side of a
> branch or the false side are applied to the current state. At present the
> current state is always updated to represent the true side of the branch.
>
> It appears that there used to be such an option to KLEE, but it is now
> gone.
>
> My first attempt at reimplemting it involved the following modifications
> to Executor::fork around line 943:
>
> ```
> if (forkDist(mtRandEngine)) { // generate randomly a 0 or 1
> falseState = ¤t;
> trueState = falseState->branch();
> addedStates.push_back(trueState);
> } else {
> trueState = ¤t;
> falseState = trueState->branch();
> addedStates.push_back(falseState);
> }
> ```
>
> I assumed this would work, and the current state would be updated with the
> correct conditions accordingly. When testing it seems like this breaks the
> process tree, as after a while the following call in Executor::fork
> triggers an assertion failure
>
> ```
> std::pair res =
> processTree->split(current.ptreeNode, falseState, trueState);
> ```
>
> The assertion failure is in `split` and is because current.ptreeNode.left
> is not null.
>
> I hacked around this by simply removing that code (and all other ptree
> functionality), but then started getting failures in
> executeMemoryOperation. At this point I stopped, as I clearly don't
> understand the ramifications of my changes and I was hoping someone could
> help with that! Any suggestions as to where I've gone wrong would be
> appreciated.
>
> Cheers,
> Sean
>
> ___
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
--
张枨宇 Chengyu Zhang
East China Normal University
School of Computer Science and Software Engineering
Tel: +86 18685412181
Mail: dale.chengyu.zh...@gmail.com
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE: ERROR: error loading program 'pallin.c': Invalid bitcode signature
Maybe you should run KLEE on .bc file generated by Clang rather than .c file. Cheers, Chengyu 2017-10-12 15:44 GMT+08:00 Mahinder.Shrivas : > Hi All, > > I am trying to run several programs but most of them showing me error as > "Invalid bit code signature". > > I tried seeing in the previous mail list and tried to follow it but I > couldn't able to figure out the problem. Most of my analysis has been > struck because i am not able to run the programs. Can anyone suggest me > what could be the problem please? Any kind of the suggestion would be great. > > > *Below is the error I am getting while running the program : (2 Examples)* > > > 1. klee@000ed980a7fe:~/klee_src/excel/report$ time klee > -allow-external-sym-calls prime.c > > *KLEE: ERROR: error loading program 'prime.c': Invalid bitcode signature* > > > real 0m0.006s > > user 0m0.000s > > sys 0m0.000s > > > > 2. klee@000ed980a7fe:~/klee_src/excel/report$ time klee > -allow-external-sym-calls pallin.c > > *KLEE: ERROR: error loading program 'pallin.c': Invalid bitcode signature* > > > real 0m0.007s > > user 0m0.000s > > sys 0m0.000s > > > > *Below is the version of my clang and klee : * > > > *My version of clang is :* > > Mahinders-MacBook-Air:~ mahindershrivas$ clang --version > > Apple LLVM version 7.3.0 (clang-703.0.31) > > Target: x86_64-apple-darwin15.3.0 > > Thread model: posix > > InstalledDir: /Library/Developer/CommandLineTools/usr/bin > > > *My version of Klee is:* > > > klee@000ed980a7fe:~/klee_src/excel/report$ klee -version > > KLEE 1.4.0.0 (https://klee.github.io) > > Build mode: RelWithDebInfo (Asserts: TRUE) > > Build revision: unknown > > > LLVM (http://llvm.org/): > > LLVM version 3.4 > > > > Optimized build. > > Built Mar 5 2014 (17:05:10). > > Default target: x86_64-pc-linux-gnu > > Host CPU: x86-64 > > > > Thank you so much. > > > > With kind regards, > > Mahinder. > > > > > > > ___ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: +86 18685412181 Mail: dale.chengyu.zh...@gmail.com ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Questions about getting symbolic execution tree with KLEE
Hi Zachery, Do you mean the symbolic execution tree? There is a data structure named PTree(ProcessTree) in KLEE, which is generated during the symbolic execution process, PTree Node will fork when the corresponding State forks. The PTree contains some information of symbolic execution will be useful for you. Here is another KLEE feature may be useful. I'm not sure if it will work well. You can run KLEE with -write-paths (records both concrete an symbolic path) or -write-sym-paths (just records symbolic path) options, KLEE will write the binary sequences for each test case in the file named "paths.ts" or "symPaths.ts" which indicates the branch chooses for each case. Furthermore, there seems has a hack tool which could convert KLEE treestream's of path branch information into images ( https://github.com/klee/klee/tree/master/utils/hacks/TreeGraphs). I hope it helps you. Cheers Chengyu 2017-12-29 13:18 GMT+08:00 Zachery <958919...@qq.com>: > Hi all, > Since KLEE is a tool of symbolic execution, is there a way to output > the symbolic tree into a file? > I have searched for the solution both in klee-dev’s searchable archive > <http://www.mail-archive.com/klee-dev@imperial.ac.uk/> and Google Search, > but there seemed to be no answer. > So, could someone tell me how to get the symbolic tree or is there a > tool for this task? > > Thanks in advance, > Zachery > > > > ___ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: +86 18685412181 Mail: dale.chengyu.zh...@gmail.com ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
