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

[Andrew Santosa]

 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 with:

res=Solver::Unknown;
success=true;

So that every time KLEE would think that the solver has been invoked
successfully and it is not known that the current condition is valid or
unsatisfiable, which means it is only known to be satisfiable, tricking
KLEE into always forking a new state.

I hope that works.

Best,
Andrew

On Saturday, 5 May 2018, 1:19:26 am GMT+8, Charitha Saumya 
 wrote:  
 
 Hi,

I want to implement a search strategy in KLEE.

If I know some branch is feasible from prior knowledge (say I learn that 
for a some br instruction the true branch is always feasible),

How can I change KLEE to avoid calling the solver in Executor.cpp (in 
Instruction::Br)

and just guide the execution to next basic block?

Please help!

Thanks,

Charitha Saumya


___
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] Unable to build Klee with LLVM 3.8

[Cristian Cadar]

Hi Sang,

We plan to merge #729 into the mainline soon.  However, the other PR, 
#605, still needs some work.  But I hope to be able to bring support for 
3.8 into the mainline in the next few weeks.


Best,
Cristian

On 04/05/2018 22:44, Sang Phan wrote:

Hello,

I'm using a newer Ubuntu where LLVM 3.4 is no longer available. So I'm 
trying to build Klee with LLVM 3.8 following the instructions in this link:

http://klee.github.io/build-llvm38/

However, I couldn't merge the pull request. After running

|git merge pull729|

I got the following errors:

Auto-merging test/Runtime/POSIX/DirSeek.c
CONFLICT (content): Merge conflict in test/Runtime/POSIX/DirSeek.c
Auto-merging runtime/POSIX/fd.c
Auto-merging lib/Core/SpecialFunctionHandler.cpp
CONFLICT (content): Merge conflict in lib/Core/SpecialFunctionHandler.cpp
Auto-merging lib/Core/Memory.h
CONFLICT (content): Merge conflict in lib/Core/Memory.h
Auto-merging lib/Core/ExternalDispatcher.h
CONFLICT (content): Merge conflict in lib/Core/ExternalDispatcher.h
Auto-merging lib/Core/ExternalDispatcher.cpp
CONFLICT (content): Merge conflict in lib/Core/ExternalDispatcher.cpp
Auto-merging lib/Core/Executor.cpp
CONFLICT (content): Merge conflict in lib/Core/Executor.cpp
Automatic merge failed; fix conflicts and then commit the result.

It is not just trivial to delete the conflict marker, would you please 
tell me how to fix it.


Thanks,
Sang


___
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] Unable to build Klee with LLVM 3.8

[Sang Phan]

Hello,

I'm using a newer Ubuntu where LLVM 3.4 is no longer available. So I'm
trying to build Klee with LLVM 3.8 following the instructions in this link:
http://klee.github.io/build-llvm38/

However, I couldn't merge the pull request. After running

git merge pull729

I got the following errors:

Auto-merging test/Runtime/POSIX/DirSeek.c
CONFLICT (content): Merge conflict in test/Runtime/POSIX/DirSeek.c
Auto-merging runtime/POSIX/fd.c
Auto-merging lib/Core/SpecialFunctionHandler.cpp
CONFLICT (content): Merge conflict in lib/Core/SpecialFunctionHandler.cpp
Auto-merging lib/Core/Memory.h
CONFLICT (content): Merge conflict in lib/Core/Memory.h
Auto-merging lib/Core/ExternalDispatcher.h
CONFLICT (content): Merge conflict in lib/Core/ExternalDispatcher.h
Auto-merging lib/Core/ExternalDispatcher.cpp
CONFLICT (content): Merge conflict in lib/Core/ExternalDispatcher.cpp
Auto-merging lib/Core/Executor.cpp
CONFLICT (content): Merge conflict in lib/Core/Executor.cpp
Automatic merge failed; fix conflicts and then commit the result.

It is not just trivial to delete the conflict marker, would you please tell
me how to fix it.

Thanks,
Sang
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

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

[Charitha Saumya]

Hi,

I want to implement a search strategy in KLEE.

If I know some branch is feasible from prior knowledge (say I learn that 
for a some br instruction the true branch is always feasible),


How can I change KLEE to avoid calling the solver in Executor.cpp (in 
Instruction::Br)


and just guide the execution to next basic block?

Please help!

Thanks,

Charitha Saumya


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Space program in KLEE

[Norlina Pasaribu]

Hallo there,


I just tried Klee I Mac, and I using this command but command not found. is
this command only for linux ? or any suggestion for iMac ? Thank you very
much



ITs-iMac-7:Test Space itdel$ klee -posix-runtime -libc=uclibc -max-time=60
./space.bc A -sym-files 1 10

-bash: klee: command not found

ITs-iMac-7:Test Space itdel$


On Mon, Feb 12, 2018 at 10:12 AM, Norlina Pasaribu <
norli...@xlfutureleaders.com> wrote:

> Hello,
>
> I am so really thankful having chance to get KLEE contact. My name is
> Norlina Pasaribu from Institut Teknologi Del, Indonesia. Now, I am in my
> last year of my bachelor and getting a thesis about testing program. If you
> don't mind, let me to tell you a little about my project.
>
> We are really proud of you for buliding a KLEE tools for testing. I have
> Space program being the object for the testing. Space is C program contains
> 9000 line codes and I get from http://sir.unl.edu/.
> I found on some paper, that concolic testing is possible to implemented
> using KLEE.
>
> My plan is I would like to generate test-case for Space program using
> concolic testing method in KLEE. Space input is not numerical but Array
> Defenition Language (ADL).
>
> My question is, is that possible KLEE for generating test-case and for
> non-numerical input ?
>
> We really hope we be able to discuss more about it with you. If you dont
> mind, let us to get your respond.
>
> Thank you very much for attention.
>
> Best regards,
>
> Norlina Pasaribu
>
>
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev