[klee-dev] KLEE 3.1 released

[Cristian Cadar]

Hi all,

It is my pleasure to announce the release of KLEE 3.1!

Big thanks to all the contributors to this version.  The full list of 
changes can be found at https://github.com/klee/klee/releases/tag/v3.1


Best wishes,
Cristian

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

[klee-dev] KLEE 2024 -- Keynote speakers announced & early registration deadline coming up

[Cristian Cadar]

Dear all,

It is my pleasure to announce a fantastic list of keynotes -- Tevfik 
Bultan, Tomasz Kuchta, and Corina Pasareanu -- for the upcoming KLEE'24 
workshop:

https://srg.doc.ic.ac.uk/klee24/keynotes.html

The workshop will be co-located with ICSE'24, and will take place 15-16 
April in Lisbon:

https://srg.doc.ic.ac.uk/klee24/

The early registration deadline is coming up, on 12 February:
https://conf.researchr.org/attending/icse-2024/registration

We hope to see many of you at the workshop in Lisbon!

Best wishes,
Cristian, Daniel, Frank, Martin, as KLEE'24 Chairs

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

Re: [klee-dev] Mapping Path Constraint to the Actual Path in Source Code

[Cristian Cadar]

Hi,

KLEE does not provide this information, although you could add such 
metadata when adding a new constraint.  However, because constraint 
solving optimisations could combine constraints, obtaining the origin of 
a constraint might not be possible in the general case.


Best,
Cristian

On 25/01/2024 04:07, Bohan wrote:


收件人:klee-dev@imperial.ac.uk 
周三 2024/1/24 19:18

Hi,

I am new to Klee. I have a question about how to determine which path 
constraints generated in the KQuery file correspond to specific paths or 
lines of code in the original source code or in the IR?


For example; I have a dummy c code that have 3 path,

#include  #include  int main() {     int num; 
int a = 10;     // Make 'num' a symbolic variable 
klee_make_symbolic(, sizeof(num), "num");     if (num > a + 3) { 
     printf("branch 0.\n");     } else if (num < a) { 
printf("branch 1.\n");     } else {         printf("branch 2.\n");     } 
     return 0; }


And here is the Kquery file for a ktest file where the num = 2147483647, 
and it goes to branch 0.


|array num[4] : w32 -> w8 = symbolic (query [(Slt 13   
(ReadLSB w32 0 num))]         false) |


My question is there any info from Klee that tells this query is for the 
branch 0.


Thank you very much for help!


___
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] Different behavior when invoking the "error" function with the argument buffer from heap or stack

[Cristian Cadar]

Hi Haoxin,

It looks to me that you are not passing a null-terminated string to 
error() in the heap case, and the error reported by KLEE is genuine.


Best,
Cristian

On 24/01/2024 15:53, TU Haoxin wrote:

Dear KLEE developers,

Hope you are all doing well, and hope this is the right place to raise 
questions about KLEE.


I have a question regarding the modeling of the function `error` 
function in `klee-uclibc` when I used KLEE. Since I couldn't find 
similar cases either in the GitHub issue or the klee-dev mailing list, I 
would like to seek your suggestions here. I do apologize if I missed 
anything.


Please consider the following simple code (test.c):
```
#include 
#include 
#include 
#include 
#include 

static void * //_GL_ATTRIBUTE_PURE
nonnull (void *p)
{
   if (!p){
     exit(1);
   }
   return p;
}

void * xxmalloc (int s){
     return nonnull (malloc(s));
}

int main(){
     char *p =(char*) xxmalloc(10); // p from heap
     memset(p, 'A', 10);
     error(1, 1, p, p); // this is problematic
     //char* pp = "hello world.\n"; // pp from stack
     //error(1, 1, pp, pp); // this is ok
     free(p);
     return 0;
}
```

Commands to compile the above code and run klee (execute.sh):
```
#!/bin/bash
clang -emit-llvm -c -g test.c
klee --libc=uclibc --posix-runtime test.bc
```

Execute the script `execute.sh`, I got the following:

```
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 
93825035744416) at runtime/POSIX/fd.c:1007 10
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not 
modelled. Using alignment of 8.

KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
KLEE: ERROR: libc/stdio/_vfprintf.c:572: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 17386
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1
```

Here is the stack information when the error occurs:
```
Error: memory error: out of bound pointer
File: libc/stdio/_vfprintf.c
Line: 572
assembly.ll line: 18473
State: 1
Stack:
  #18473 in _ppfs_init (=93825004575232, =93825035189056) at 
libc/stdio/_vfprintf.c:572
  #100015268 in vfprintf (=93825004959696, =93825035189056, 
=93825035841056) at libc/stdio/_vfprintf.c:1888
  #200012650 in __error (=1, =1, =93825035189056) at 
libc/misc/error/error.c:57

  #39767 in __klee_posix_wrapped_main () at test.c:24
  #47354 in __user_main (=1, =93825013002624, =93825013002640) 
at runtime/POSIX/klee_init_env.c:245
  #50592 in __uClibc_main (=93825035146016, =1, =93825013002624, 
=0, =0, =0, =0) at libc/misc/internals/__uClibc_main.c:401

  #60757 in main (=1, =93825013002624)
Info:
  address: 93825035189066
  next: object at 93825004575232 of size 256
MO7712[256] allocated at vfprintf():  %7 = alloca 
%struct.ppfs_t.715, align 16

```
I tested the above code using clang-9 with klee-2.1 (as well as 
klee-2.3-pre).

```
$klee --version
KLEE 2.3-pre (https://klee.github.io)
   Build mode: Debug (Asserts: ON)
   Build revision: 0ba95edbad26fe70c8132f0731778d94f9609874

LLVM (http://llvm.org/):
   LLVM version 9.0.0
   Optimized build.
   Default target: x86_64-pc-linux-gnu
   Host CPU: skylake-avx512
```

The confusion is that when I replaced the pointer `p` from the heap to 
`pp` from the stack (as shown in the two commented lines), KLEE could 
execute the function `error` well. I think both the buffers from the 
heap or stack should work (I tested the native execution and these two 
versions of code both work ok) but it does not in KLEE, and I don't know 
why that is the case. Since the `error` function involves variadic 
arguments 
(https://github.com/klee/klee-uclibc/blob/klee_0_9_29/libc/misc/error/error.c#L50 ), I suspect that this is because KLEE has some implementation limitations of the handling of variadic functions when it involves the pointers from the heap (I also tried to find the reason behind it but failed). Could you please take a look and help me understand about this case? Why does KLLE behave differently when the pointer is from the heap or stack? Any ideas or insights are welcome!


Thank you so much for your time and help!


Best regards,
Haoxin

___
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] KLEE'24 workshop late submission deadline this Friday

[Cristian Cadar]

Dear all,

The late (and last) submission deadline for the KLEE'24 workshop is this 
Friday!


We have already accepted a number of interesting presentations and 
posters in the early submission round, and we are looking forward to 
more interesting contributions in the second round!

https://srg.doc.ic.ac.uk/klee24/

Also, the registration for the workshop, which next year is co-located 
with ICSE'24, is open!

https://conf.researchr.org/attending/icse-2024/registration

Best wishes,
Cristian

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

[klee-dev] KLEE 2024: First (visa-safe) submission deadline is TODAY

[Cristian Cadar]

Hi all,

A final reminder about the first (visa-safe) submission deadline for 
KLEE 2024.  We are looking forward to your submissions!  And thanks to 
everyone who has already submitted their interesting work!


https://srg.doc.ic.ac.uk/klee24/cfpresentations.html
https://srg.doc.ic.ac.uk/klee24/cfposters.html

Best,
Cristian

On 27/10/2023 13:23, Cristian Cadar wrote:

Hi all,

Just a short reminder that there is one week left until the early 
submission deadline for KLEE 2024!  As I mentioned before, the 
submission process is very lightweight: an abstract and a link to 
already published work that you'd like to present, or an extended 
abstract of up to two pages for work in progress.


https://srg.doc.ic.ac.uk/klee24/
https://srg.doc.ic.ac.uk/klee24/

Best wishes,
Cristian

On 13/09/2023 12:57, Cristian Cadar wrote:

Dear all,

It is my great pleasure to announce the 4th edition of the 
International KLEE Workshop on Symbolic Execution, KLEE 2024!


KLEE 2024 will take place in April in Lisbon, Portugal, co-located 
with ICSE 2024, the flagship software engineering conference:

https://srg.doc.ic.ac.uk/klee24/

KLEE 2024 follows three successful editions (2018, 2021 and 2022), 
which   together have gathered over 400 participants from six 
different continents spanning academia, industry and government.  One 
of the main goals of the workshop is to get together symbolic 
execution researchers, as well as KLEE developers and users to 
exchange ideas, understand each other’s interests and needs, and 
discuss the evolution of symbolic execution technology.  A particular 
emphasis will be placed on connecting academic researchers working 
with KLEE and symbolic execution with industrial users interested in 
using KLEE to improve their software products.


As in prior years, the workshop has no proceedings.  Instead, we will 
have a call for presentations and posters; the submission site is 
already open!  Both published and ongoing work are welcome to be 
presented and the submission is low-effort: an abstract and a link to 
published work, or an extended abstract of up to two pages for work in 
progress.


The first round deadline (which is more likely to guarantee a 
presentation/poster slot, as well as provide ample time to obtain a 
visa if needed) is on 3rd of November!


We thank again our sponsors for the first three editions: UK EPSRC, 
Baidu, Bloomberg, Fujitsu, Google, Qualcomm, Huawei, Samsung, Trail of 
Bits and Imperial College London.  If you would like to sponsor the 
next edition, please get in touch with me by replying to this message.


Looking forward to your submissions,
Cristian, also on behalf of Daniel, Frank and Martin as KLEE 2024 Chairs

___
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

[klee-dev] KLEE 2024: One week until first (visa-safe) deadline

[Cristian Cadar]

Hi all,

Just a short reminder that there is one week left until the early 
submission deadline for KLEE 2024!  As I mentioned before, the 
submission process is very lightweight: an abstract and a link to 
already published work that you'd like to present, or an extended 
abstract of up to two pages for work in progress.


https://srg.doc.ic.ac.uk/klee24/
https://srg.doc.ic.ac.uk/klee24/

Best wishes,
Cristian

On 13/09/2023 12:57, Cristian Cadar wrote:

Dear all,

It is my great pleasure to announce the 4th edition of the International 
KLEE Workshop on Symbolic Execution, KLEE 2024!


KLEE 2024 will take place in April in Lisbon, Portugal, co-located with 
ICSE 2024, the flagship software engineering conference:

https://srg.doc.ic.ac.uk/klee24/

KLEE 2024 follows three successful editions (2018, 2021 and 2022), which 
  together have gathered over 400 participants from six different 
continents spanning academia, industry and government.  One of the main 
goals of the workshop is to get together symbolic execution researchers, 
as well as KLEE developers and users to exchange ideas, understand each 
other’s interests and needs, and discuss the evolution of symbolic 
execution technology.  A particular emphasis will be placed on 
connecting academic researchers working with KLEE and symbolic execution 
with industrial users interested in using KLEE to improve their software 
products.


As in prior years, the workshop has no proceedings.  Instead, we will 
have a call for presentations and posters; the submission site is 
already open!  Both published and ongoing work are welcome to be 
presented and the submission is low-effort: an abstract and a link to 
published work, or an extended abstract of up to two pages for work in 
progress.


The first round deadline (which is more likely to guarantee a 
presentation/poster slot, as well as provide ample time to obtain a visa 
if needed) is on 3rd of November!


We thank again our sponsors for the first three editions: UK EPSRC, 
Baidu, Bloomberg, Fujitsu, Google, Qualcomm, Huawei, Samsung, Trail of 
Bits and Imperial College London.  If you would like to sponsor the next 
edition, please get in touch with me by replying to this message.


Looking forward to your submissions,
Cristian, also on behalf of Daniel, Frank and Martin as KLEE 2024 Chairs

___
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] Announcing KLEE 2024: 4th International KLEE Workshop on Symbolic Execution, April 2024 in Lisbon

[Cristian Cadar]

Dear all,

It is my great pleasure to announce the 4th edition of the International 
KLEE Workshop on Symbolic Execution, KLEE 2024!


KLEE 2024 will take place in April in Lisbon, Portugal, co-located with 
ICSE 2024, the flagship software engineering conference:

https://srg.doc.ic.ac.uk/klee24/

KLEE 2024 follows three successful editions (2018, 2021 and 2022), which 
 together have gathered over 400 participants from six different 
continents spanning academia, industry and government.  One of the main 
goals of the workshop is to get together symbolic execution researchers, 
as well as KLEE developers and users to exchange ideas, understand each 
other’s interests and needs, and discuss the evolution of symbolic 
execution technology.  A particular emphasis will be placed on 
connecting academic researchers working with KLEE and symbolic execution 
with industrial users interested in using KLEE to improve their software 
products.


As in prior years, the workshop has no proceedings.  Instead, we will 
have a call for presentations and posters; the submission site is 
already open!  Both published and ongoing work are welcome to be 
presented and the submission is low-effort: an abstract and a link to 
published work, or an extended abstract of up to two pages for work in 
progress.


The first round deadline (which is more likely to guarantee a 
presentation/poster slot, as well as provide ample time to obtain a visa 
if needed) is on 3rd of November!


We thank again our sponsors for the first three editions: UK EPSRC, 
Baidu, Bloomberg, Fujitsu, Google, Qualcomm, Huawei, Samsung, Trail of 
Bits and Imperial College London.  If you would like to sponsor the next 
edition, please get in touch with me by replying to this message.


Looking forward to your submissions,
Cristian, also on behalf of Daniel, Frank and Martin as KLEE 2024 Chairs

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

Re: [klee-dev] Why is ConstraintSet not a set?

[Cristian Cadar]

Hi,

KLEE does not add duplicate constraints, in fact it does not add a 
constraint if it is implied by the current PC.


Best,
Cristian

On 07/07/2023 06:57, Nguyễn Gia Phong wrote:

Hi,

I notice that ConstraintSet is implemented via std::vector.
This make me wonder about the likelihood of duplucated constraints
during executions.

Does anyone have any emprical data or experience regarding this aspect?

Regards,
McSinyx

___
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] KLEE 3.0 is released!

[Cristian Cadar]

Hi all,

KLEE 3.0 is released! KLEE now has a purposely-designed deterministic 
memory allocator (KDAlloc), improved detection of use-after-free errors, 
ability to handle UBSan checks, support for concrete inline assembly, 
better statistics, compatibility with newer LLVM versions & more!


Big thanks to all contributors, particularly @MartinNowack and @251 as 
both contributors and co-maintainers; and @danielschemmel, 
@operasfantom, @mishok2503, and @jbuening for co-authoring several of 
the major new features in this release.


The new version (our 10th!), release notes and full list of contributors 
can be found at:

https://github.com/klee/klee/releases/tag/v3.0

Enjoy!
Cristian

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

Re: [klee-dev] Getting symbolic expressions from the symbolic store with `klee_print_expr`

[Cristian Cadar]

Hi Ferhat,

Essentially, you want something like this:

printer.printExpression(arguments[1], ExprSMTLIBPrinter::SORT_BITVECTOR);

To do this right requires a bit more work, but as a quick proof of 
concept, just change the visibility of this method.


Best,
Cristian

On 03/04/2023 01:39, Ferhat Erata wrote:

Hi,

I wanted to ask about converting symbolic expressions in KQuery format
to SMTLIB format.

Currently, I am able to obtain the symbolic expressions using
`klee_print_expr` in KQuery format, but I need to manipulate them in
bit-vector logic, which requires converting them to SMTLIB format to
process them with preferably with Z3 or STP. I tried to modify the
code in `SpecialFunctionHandler.cpp` to generate SMTLIB expressions.
However, the resulting expressions are invalid assertions.

I have included an example in the email to illustrate my situation. I
would appreciate it if you could provide me with feedback.

Thank you for your time and assistance.

Best,
~ Ferhat

--

Please find an example in the following:
```
#include "klee/klee.h"

int main(int argc, char *argv[]) {
   int x;
   klee_make_symbolic(, sizeof(x), "x");
   int b, c;
   b = x + 10;
   klee_print_expr("b", b);
   c = x * x;
   klee_print_expr("c", c);
}
```

KLEE returns the following output in KQuery representations for those
variables as expected:
```
b:(Add w32 10
   (ReadLSB w32 0 x))
c:(Mul w32 N0:(ReadLSB w32 0 x)
   N0)
```

The first thing that came to my mind was to convert those expressions
to SMTLIB expressions. Therefore, I changed the code in
`SpecialFunctionHandler.cpp` as follows:
```
void SpecialFunctionHandler::handlePrintExpr(ExecutionState ,
   KInstruction *target,
   std::vector > ) {
   assert(arguments.size()==2 &&
  "invalid number of arguments to klee_print_expr");

   std::string msg_str = readStringAtAddress(state, arguments[0]);
   llvm::errs() << msg_str << ":" << arguments[1] << "\n";

   llvm::errs() << "\n";
   ExprSMTLIBPrinter printer;
   printer.setOutput(llvm::errs());
   Query query(state.constraints, arguments[1]);
   printer.setQuery(query);
   printer.generateOutput();
}
```

Now, I get the following:
```
b:(Add w32 10
   (ReadLSB w32 0 x))
(set-logic QF_AUFBV )
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (=  (_ bv4294967286 32) (concat  (select  x (_ bv3 32) )
(concat  (select  x (_ bv2 32) ) (concat  (select  x (_ bv1 32) )
(select  x (_ bv0 32) ) ) ) ) ) )
(check-sat)
(exit)

c:(Mul w32 N0:(ReadLSB w32 0 x)
   N0)
(set-logic QF_AUFBV )
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (=  (_ bv0 32) (bvmul  (! (concat  (select  x (_ bv3 32) )
(concat  (select  x (_ bv2 32) ) (concat  (select  x (_ bv1 32) )
(select  x (_ bv0 32) ) ) ) ) :named ?B1) ?B1 ) ) )
(check-sat)
(exit)
```

However, you can see that the code that I added turns them into
invalid assertions, however, I would expect getting symbolic
expressions that is semantically equivalent to those of KQuery:
```
[4294967286 ==
  Concat(x[3], Concat(x[2], Concat(x[1], x[0])))]

[0 ==
  Concat(x[3], Concat(x[2], Concat(x[1], x[0])))*
  Concat(x[3], Concat(x[2], Concat(x[1], x[0])))]
```

I would expect something similar to this with an additional symbolic input:
```
[Concat(b[3], Concat(b[2], Concat(b[1], b[0]))) == 10 +
  Concat(x[3], Concat(x[2], Concat(x[1], x[0])))]

[Concat(c[3], Concat(c[2], Concat(c[1], c[0]))) ==
  Concat(x[3], Concat(x[2], Concat(x[1], x[0])))*
  Concat(x[3], Concat(x[2], Concat(x[1], x[0])))]
```

Best,
~ Ferhat

___
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] General question

[Cristian Cadar]

Hi both,

Let me answer this as part of the more detailed email Ferhat sent today.

But more generally, you can use Kleaver to load queries in KQuery format 
and print them to SMT-LIB2 format:


kleaver --print-smtlib file.kquery

Best,
Cristian

On 30/03/2023 21:57, Ferhat Erata wrote:

Hi Teja,

I was also looking for this feature. Have you come up with a workaround?

Do you know if there is a way to transform expressions in kquery format 
to smt2 format?


Best,
~ Ferhat


On Mon, Jan 9, 2023 at 7:21 AM Teja Sai Srikar Bodavula 
mailto:btssri...@gmail.com>> wrote:


Hello, I was wondering if there is way in which we can get
symbolic formula for a variable in a code in smt2 format unlike
kquery format which we get using klee_print_expr.
___
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] About external shared libraries

[Cristian Cadar]

Hi Ziqi,

There is no such feature in KLEE currently.  If this is something you'd 
like to contribute, we'd be happy to discuss your proposal in more detail.


Best,
Cristian

On 25/02/2023 03:29, Ziqi Shuai wrote:

Hi all,
I'm trying to use KLEE to analyze some real-world programs such as image 
processing programs. Unfortunately, I found KLEE usually terminated 
early because of 'failed external call' errors, where the call was from 
shared libraries located in directories on the system search path.


I know I can resolve the trouble through loading necessary shared 
libraries manually, i.e., using the '-load' option. However, real-world 
programs often depend on a bulk of shared libraries, which make the 
manual way clumsy and tedious. Hence, I'd like to know whether KLEE is 
able to search for these shared libraries in an automatic way, just like 
what native executables do.


Best Regards,
Ziqi

___
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] Debugging options

[Cristian Cadar]

On 22/12/2022 16:09, Muralee, Siddharth wrote:

Hello,

I am currently working on a project to verify states that end due to 
errors such as "memory error: out of bound pointer". Currently, I am 
trying to extract some information about these states, and the most 
information I am able to extract is the instruction log from replaying 
only the seed file, using the options |--debug-print-instructions|​ and 
|--only-seed --seed-file|​ .


Is there any way to extract more details? While running an application 
with a seed input.
What other info would you like?  Most likely you would need to add 
support for additional info yourself.


Also, for the |debug-print-instructions=all:stderr|​ is there any way to 
restrict Klee from printing all the instructions inside the libraries? 
It takes an insane amount of time looping inside the runtime setup code 
as well as library functions such as sprintf etc. 
There are no options to do so, but this could be easily accomplished by 
changing the code.


To reduce the amount of logged data, you could use 
--debug-compress-instructions, which compresses the logged instructions 
in gzip format.


Best,
Cristian

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

Re: [klee-dev] On how the standard library is linked.

[Cristian Cadar]

Hi Alex,

We typically link against a custom version of uclibc, where printf is 
treated specially by default as an external function.  Does this answer 
your question?


It is possible to load binary-only libraries with KLEE via the --load 
option.


Best,
Cristian

On 03/11/2022 14:28, Alex Babushkin wrote:

Hello.

KLEE can call functions that do not have IR available as externals. Some 
C standard library functions are also called as externals (e.g. printf). 
How is the standard library linked to the JIT engine that calls 
externals?  Also, why isn't loading of binary-only libraries supported 
in KLEE? Are there serious reasons for that or is it just considered 
unnecessary?


Best regards,
Alex.

___
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] Use KLEE with JAVA and C#

[Cristian Cadar]

Hi Piyush,

The short answer is no.  More precisely, KLEE runs on LLVM bitcode, so 
you need an LLVM frontend for the language.  Each language also needs 
some additional support to work with KLEE.


Best,
Cristian

On 26/08/2022 02:09, Piyush Jha wrote:

Hi everyone,

I'm looking for a tool for symbolic execution in C# or JAVA. Does Klee 
support C# or JAVA?


I searched the mailing list archive and found the same question for JAVA 
posted several years back. Does anyone know if there are any updates 
regarding these?


I would really appreciate any help you can provide.

With kind regards,
Piyush

___
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] Running KLEE on Linux

[Cristian Cadar]

Hi Faysal,

You should contact the authors of those papers for more details, they 
might not be subscribed to this list.


Best,
Cristian

On 12/09/2022 08:46, Faysal Hossain Shezan wrote:
I saw your post: 
https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg03057.html 

But none of those two works seem to be working. (for the OSDI paper, we 
were not able to find the source code)


On Mon, Sep 12, 2022 at 2:44 AM Faysal Hossain Shezan 
mailto:fs...@virginia.edu>> wrote:


Hi,

We a group of researchers from the University of Virginia, the
University of Santa-Barbara, and University of California, Los
Angeles are working on finding exploits in Linux. Seeing the
performance of KLEE we want to use this tool on the Linux kernel.
Unfortunately, we are not able to run it on linux kernel due to
facing some errors during building .bc file. Can you point us to
some guideline or any previous work/link? It would be really helpful.



Thanks!

-- 
Regards,


*Faysal Hossain Shezan*
PhD Student
Department of  Computer Science
University of Virginia
Charlottesville, VA-22903
Website: https://www.cs.virginia.edu/~fs5ve/




--
Regards,

*Faysal Hossain Shezan*
PhD Student
Department of  Computer Science
University of Virginia
Charlottesville, VA-22903
Website: https://www.cs.virginia.edu/~fs5ve/ 



___
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] KLEE 2022 Workshop: Free online registration now available & in-person registration still open

[Cristian Cadar]

Hi all,

We have opened today the online registration for the KLEE'22 workshop, 
which is free for everyone! (but we might need to restrict the number of 
places)


In-person registration is still available until 1st September; if you 
can make it to London, in-person participation is the best way to 
experience the workshop.


https://srg.doc.ic.ac.uk/klee22/registration.html

We have an exciting list of keynotes and accepted contributions, which 
you can find here:

https://srg.doc.ic.ac.uk/klee22/keynotes.html
https://srg.doc.ic.ac.uk/klee22/accepted_contributions.html

I hope to see as many of you at the workshop!

Cristian, on behalf of the KLEE'22 Organising Team

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

Re: [klee-dev] Deadline moved to THURSDAY for presentation and poster proposals to the next KLEE Workshop

[Cristian Cadar]

Hi all,

We received some requests to extend the deadline.  The new deadline is 
now Thursday, 14th July, 23:55 BST (strict), see 
https://srg.doc.ic.ac.uk/klee22/deadlines.html


We are looking forward to your submissions!
Cristian, on behalf of the KLEE'22 Organizing Team

On 12/07/2022 09:56, Cristian Cadar wrote:

Hi all,

Just a reminder that the deadline for presentation and poster proposals 
to the next KLEE Workshop is today, 12th July.


Best,
Cristian

On 11/06/2022 22:55, Cristian Cadar wrote:

Hi all,

The submission site for the 3rd KLEE Workshop is now OPEN!  The 
deadline is in about one month, on 12th July.  We are looking forward 
to your interesting presentation and poster proposals!  Remember that 
the workshop has no proceedings, so you can present both published and 
ongoing work.

https://srg.doc.ic.ac.uk/klee22/cfpresentations.html
https://srg.doc.ic.ac.uk/klee22/cfposters.html

Best,
Cristian, on behalf of the KLEE'22 Organising Team


 Forwarded Message 
Subject: [klee-dev] 3rd International KLEE Workshop on Symbolic 
Execution -- 15-16 September, London and online

Date: Mon, 16 May 2022 23:00:20 +0100
From: Cristian Cadar 
To: klee-dev@imperial.ac.uk 

Hi all,

I'm very excited to announce the 3rd International KLEE Workshop on 
Symbolic Execution (KLEE 2022), taking place in London and online on 
15-16 September 2022:

https://srg.doc.ic.ac.uk/klee22/
https://twitter.com/kleesymex/status/1526310428485341187

The first two workshops were really great, with participants from 
around the world (over 80 to the first one in London, over 200 to the 
second one online) with an array of interesting keynotes, talks and 
posters:

https://srg.doc.ic.ac.uk/klee18/
https://srg.doc.ic.ac.uk/klee21/

I am looking forward to another one, so please consider contributing 
an interesting presentation and/or poster:

https://srg.doc.ic.ac.uk/klee22/cfpresentations.html
https://srg.doc.ic.ac.uk/klee22/cfposters.html

Big thanks to Daniel, Frank, Martin, Hassan and Jamie for their role 
as co-organizers of this 3rd edition!


Many thanks to Bloomberg, Samsung, Google and Imperial College London 
for their sponsorship!  To keep registration costs low, we are still 
looking for a few more sponsors, so if your organization is interested 
in sponsoring the workshop, please let me know.


Looking forward to seeing many of you in September!
Cristian

___
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


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

[klee-dev] Deadline TODAY for presentation and poster proposals to the next KLEE Workshop

[Cristian Cadar]

Hi all,

Just a reminder that the deadline for presentation and poster proposals 
to the next KLEE Workshop is today, 12th July.


Best,
Cristian

On 11/06/2022 22:55, Cristian Cadar wrote:

Hi all,

The submission site for the 3rd KLEE Workshop is now OPEN!  The deadline 
is in about one month, on 12th July.  We are looking forward to your 
interesting presentation and poster proposals!  Remember that the 
workshop has no proceedings, so you can present both published and 
ongoing work.

https://srg.doc.ic.ac.uk/klee22/cfpresentations.html
https://srg.doc.ic.ac.uk/klee22/cfposters.html

Best,
Cristian, on behalf of the KLEE'22 Organising Team


 Forwarded Message 
Subject: [klee-dev] 3rd International KLEE Workshop on Symbolic 
Execution -- 15-16 September, London and online

Date: Mon, 16 May 2022 23:00:20 +0100
From: Cristian Cadar 
To: klee-dev@imperial.ac.uk 

Hi all,

I'm very excited to announce the 3rd International KLEE Workshop on 
Symbolic Execution (KLEE 2022), taking place in London and online on 
15-16 September 2022:

https://srg.doc.ic.ac.uk/klee22/
https://twitter.com/kleesymex/status/1526310428485341187

The first two workshops were really great, with participants from around 
the world (over 80 to the first one in London, over 200 to the second 
one online) with an array of interesting keynotes, talks and posters:

https://srg.doc.ic.ac.uk/klee18/
https://srg.doc.ic.ac.uk/klee21/

I am looking forward to another one, so please consider contributing an 
interesting presentation and/or poster:

https://srg.doc.ic.ac.uk/klee22/cfpresentations.html
https://srg.doc.ic.ac.uk/klee22/cfposters.html

Big thanks to Daniel, Frank, Martin, Hassan and Jamie for their role as 
co-organizers of this 3rd edition!


Many thanks to Bloomberg, Samsung, Google and Imperial College London 
for their sponsorship!  To keep registration costs low, we are still 
looking for a few more sponsors, so if your organization is interested 
in sponsoring the workshop, please let me know.


Looking forward to seeing many of you in September!
Cristian

___
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] Working with fixed memory locations.

[Cristian Cadar]

Hi Marco, you seem to be reaching an issue with the solver, which is 
having trouble reasoning about the huge symbolic array (requiring 
excessive time and memory).  You should try to shrink that array if 
possible.  You can also try --optimize-array=all, but it might not help 
in your case.


Best,
Cristian

On 17/06/2022 05:02, Marco Vanotti wrote:
After letting it run for a few hours I've observed that klee spawns a 
subprocess that keeps growing on memory until it reaches ~100GiB and 
then it stops and restarts again.
Nothing is being printed indicating an error, but I'm not sure if the 
behavior is normal. This is with KLEE from the docker container.


I've tried building KLEE from source, both with STP and Z3 support, and 
running my program makes it crash with a segfault :(


Here is the backtrace for the crash with the STP solver: 
https://pastebin.com/raw/xpf9D9VD 


Best Regards,
Marco

On Thu, Jun 16, 2022 at 3:48 PM Marco Vanotti > wrote:


Hi Martin, Manuel,

Thanks for your answer :) !

On Thu, Jun 16, 2022 at 1:19 PM Nowack, Martin
mailto:m.now...@imperial.ac.uk>> wrote:

Hi Marco,

Maybe the following helps you:

https://github.com/klee/klee/blob/292600cf54d5fd73278f67a4f98c2f955cbdaa10/test/Feature/DefineFixedObject.c




This seems to be what I am looking for, thanks!. I tried using it
for small variables and it works. However, for a big object
(0x256000 bytes) it shows the following warning:

*KLEE: WARNING ONCE*: flushing 2449408 bytes on read, may be slow
and/or crash: MO195[2449408] allocated at main():  call void
@klee_define_fixed_object(i8* inttoptr (i64 8404992 to i8*), i64
2449408), !dbg !171
KLEE is still running, so maybe it just means it is slow.

I went with the approach of having my blob as a global variable, and
then `memcpy` it into the address after calling define_fixed_object.

Best,
Martin


On 16. Jun 2022, at 20:43, Carrasco, Manuel G
mailto:m.carra...@imperial.ac.uk>>
wrote:

Hi Marco!

I have a program that when compiled, adds a program header
that loads a data blob into a fixed memory location.

I'm sorry to ask, but could you explain a bit more how this
works? At first glance, I'd say that if any of this happens on
a stage later than LLVM-IR, it may be hard to mimic in KLEE.


I have a bunch of files that I add as .incbin into a section, and
then my linker scripts put them in a fixed address when it links the
program altogether. I think there is no way this would work with
LLVM IR.



As far as I understand, when KLEEexecutes a LLVM-IR load
instruction
,
it will try tofind

the
MemoryObjects (more than one if it is a symbolic pointer) that
contain the address. Conceptually, you want KLEE to somehow
have a MemoryObject at the hardcoded address.

One way to go could be modelling this as a LLVM-IR
GlobalVariable at your fixed address with the content of your
blob.  If this makes sense, you may want to check thisfunction
and
addExternalObject perhaps as well.


Thanks! This looks interesting, but I am a bit puzzled about how to
go with this. Should I recompile KLEE to add support for my use
case? I checked on the MemoryManager class and it seems like it just
allocates stuff at whatever place is available.



I apologise if you already know this!



I did not know any of that :) This is the second time I am using
KLEE, and the first one was a big failure :P

Thanks!
Marco



Best regards,
Manuel.


*From:*klee-dev-boun...@imperial.ac.uk

mailto:klee-dev-boun...@imperial.ac.uk>> on behalf of Marco
Vanotti mailto:mvano...@dc.uba.ar>>
*Sent:*16 June 2022 18:55
*To:*klee-dev mailto:klee-dev@imperial.ac.uk>>
*Subject:*[klee-dev] Working with fixed memory locations.
Hi klee-dev!

I am new to KLEE, and have a question about using it with one
of my programs.

I have a program that when compiled, adds a program header
that loads a data blob into a fixed memory location.

This means that my program has this fixed memory location
hardcoded all around the place (also this blob has references
to itself).

I 

Re: [klee-dev] Need help in understanding a kquery generated by KLEE

[Cristian Cadar]

Hi Sandip,

Those constants are most likely derived from concrete addresses, but you 
should try to simplify the program as much as possible and send a full 
program that can be compiled and run.


Best,
Cristian

On 02/05/2022 19:22, Sandip Ghosal wrote:

Hello,

I need help in understanding a kquery file generated by KLEE.

Consider the following C program:

void* foo(struct node *item1. struct node *item2){
          if(item1 == item2){
              item1->next = NULL;
          }
          return item1;
}

void main(){
       struct list *array[3];
       // next allocate memory for each array[I], i=0,1,2
      int item1 = klee_range(0, 3, "item1");
      int item2 = klee_range(0, 3, "item2");
      foo(array[item1], array[item2]);
}

Since my main objective is to understand the query, the above program is 
simplified and loosely written for reference. Now KLEE generates one 
kquery as follows:


array const_arr1[24] : w32 -> w8 = [32 77 0 133 168 85 0 0 240 68 0 133 
168 85 0 0 0 77 0 133 168 85 0 0]

array item1[4] : w32 -> w8 = symbolic
array item2[4] : w32 -> w8 = symbolic

(query [(Ult N0:(ReadLSB w32 0 item1)
               3)

          (Ult N1:(ReadLSB w32 0 item2)
               3)

          (Eq N2:(ReadLSB w64 N3:(Extract w32 0 (Mul w64 8 (SExt w64 
N0))) const_arr1)
              (ReadLSB w64 N4:(Extract w32 0 (Mul w64 8 (SExt w64 N1))) 
const_arr1))


          (Eq false
              (Ult (Add w64 18446649891435295456 N2) 9))

          (Ult (Add w64 18446649891435295488 N2) 9)]
         false)

I am struggling to understand the second and third last line of the 
query which seems to be performing a boundary check on a flat byte 
memory address. I understand KLEE is implicitly branching over the 
statement  item1->next = NULL, 18446649891435295456 perhaps is the base 
address for item1, and N2 computes the offset. However, I am failing to 
understand how the base address is computed and why it is always 
compared with a constant value of 9?


Thanks in advance.

--
Thanks & Regards
Sandip Ghosal




___
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] Errors when files unconform to the format!

[Cristian Cadar]

Hi Yukai,

You can use klee_assume 
(https://klee.github.io/docs/intrinsics/#klee_assumecondition) on the 
desired symbolic file created by the POSIX runtime, see 
https://github.com/klee/klee/blob/master/runtime/POSIX/fd_init.c#L61


Best,
Cristian

On 06/06/2022 15:06, 房合钧 wrote:

Hello!

I recently tried to use Klee to detect a project that handles PNG 
images. I use sym files to generate input files, but the generated files 
do not necessarily meet the format requirements of PNG pictures. 
Therefore, I hope to fix some characters to make the generated files 
conform to the format.


I found in the past mailing list that you mentioned that it can be 
specified through the file in POSIX, but I can't figure out which file 
can be set. So can you tell me the specific file path.


Similarly, I want to confirm whether Klee is also used in POSIX_ Assume 
(), or there are other functions.


If you are willing to give a simple example, it would be great.


Thanks and regards,
yukai

___
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] Idea: Klee experiment on Coreutils reimplementation in Rust

[Cristian Cadar]

You should look at the work of Alastair Reid / Google on this topic:
https://project-oak.github.io/rust-verification-tools/2021/07/14/coreutils.html

Best,
Cristian

On 04/06/2022 22:26, gwpub...@wp.pl wrote:

Klee got famous with coreutils experiments.

As they reimplement coreutils in Rust, maybe it would be interesting
to prepare e.g. Dockerfile allowing to repeat experiment but on those:
https://github.com/uutils/coreutils

___
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] KLEE for stateful C API

[Cristian Cadar]

Hi Niklaus,

There is no obvious improvement to recommend for the general case.  Of 
course, search heuristics have an important influence on which API 
sequences are explored first.  There is also a lot of research into this 
problem: I would recommend Randoop 
(https://homes.cs.washington.edu/~mernst/pubs/feedback-testgen-icse2007.pdf) 
and EvoSuite 
(https://www.evosuite.org/wp-content/papercite-data/pdf/esecfse11.pdf) 
as starting points.


Best,
Cristian

On 02/05/2022 08:50, Niklaus Leuenberger wrote:

Hello klee-dev members,

I'm currently testing out a few approaches on how to test and fuzz a
stateful C API. In the process thereof I found KLEE and am fascinated
by it. I managed to get it to work and am now asking if my approach is
ok or if it has some major drawbacks or problems.

Let's suppose we have following simple but buggy stateful API:
---
#include 
static int g_state;
void setState(int state) {
 g_state = state;
}
void run(void) {
 if (g_state == 123) {
 assert(0);
 }
}
---
If the state is set to 123 and then run() is invoked the placed assertion fails.

For this I have written following KLEE harness:
---
#include "klee/klee.h"
#include "buggy_api.h"
int main(void) {
 for (int i = 0; i < 2; ++i) { // sequentially call 2 APIs
 int f_select = klee_choose(2); // what API to call
 if (f_select == 0) {
 int state = 0;
 klee_make_symbolic(, sizeof(state), "state");
 setState(state);
 } else if (f_select == 1) {
 run();
 }
 }
 return 0;
}
---

When running with KLEE, the sequence of calls necessary to trigger the
assertion is found almost immediately. But when extending it with more
functions, each doubles the runtime. So it scales rather poorly on
larger APIs.
Is this how I can use KLEE for checking an API? Or does someone have
pointers to a better approach?

Best Regards,
Niklaus Leuenberger

___
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] How to determine the concretized size when dealing with malloc()

[Cristian Cadar]

Hi Austin,

Sorry to see that nobody has answered your email.  I'm not sure what you 
are trying to do though.  Are you trying to make KLEE choose a specific 
size?


(That code is a bit broken, btw.  We fixed it in some extensions but 
haven't managed to merge the changes into the mainline yet.)


Best,
Cristian

On 18/04/2022 10:55, Wang Austin wrote:

Hello klee-dev members,

I'm working on a project involving KLEE and SMT solvers. We are 
collecting queries from KLEE using the v2.2 klee docker image with the 
"--use-query-log=solver:smt2" option. I observed that the queries 
collected are not always complete when KLEE dealing with malloc(), and 
KLEE would throw an error:

...
KLEE: ERROR: tif_unix.c:334: concretized symbolic size
...

I'm expecting to determine the concretized size for malloc() in 
accordance with the value of size in the actual execution and check if 
the queries are more complete in this case.


I checked the source code (klee/lib/Core/Executor.cpp), finding that 
KLEE would "optimize" when the size is symbolized. And I tried the 
"--allocate-determ" option for memory management according to the 
document, which I thought would determine the size to a specific value 
and resolve the error, whereas, it doesn’t seem to be running right, 
here are the results.


1) Normal execution:
...
KLEE: ERROR: tif_unix.c:334: concretized symbolic size
KLEE: NOTE: now ignoring this error at this location
KLEE: seeding done (0 states remain)
...

2) Execution with --allocate-determ=1 --allocate-determ-size=10:
...
KLEE: ERROR: tif_unix.c:334: concretized symbolic size
KLEE: NOTE: now ignoring this error at this location
KLEE: seeding done (0 states remain)
KLEE: Deterministic memory allocation starting frow 0x7ff3000
...

The size still got concretized or perhaps I misunderstood the usage of 
the "--allocate-determ" option.


I’m wondering if there is a way to "determine the concretized size to a 
specific value when malloc()" or "NOT to optimize the size", so I can 
collect queries with more completeness using KLEE.


Best Regards,
Austin Wang

___
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] 3rd International KLEE Workshop on Symbolic Execution -- submission site NOW OPEN

[Cristian Cadar]

Hi all,

The submission site for the 3rd KLEE Workshop is now OPEN!  The deadline 
is in about one month, on 12th July.  We are looking forward to your 
interesting presentation and poster proposals!  Remember that the 
workshop has no proceedings, so you can present both published and 
ongoing work.

https://srg.doc.ic.ac.uk/klee22/cfpresentations.html
https://srg.doc.ic.ac.uk/klee22/cfposters.html

Best,
Cristian, on behalf of the KLEE'22 Organising Team


 Forwarded Message 
Subject: [klee-dev] 3rd International KLEE Workshop on Symbolic 
Execution -- 15-16 September, London and online

Date: Mon, 16 May 2022 23:00:20 +0100
From: Cristian Cadar 
To: klee-dev@imperial.ac.uk 

Hi all,

I'm very excited to announce the 3rd International KLEE Workshop on 
Symbolic Execution (KLEE 2022), taking place in London and online on 
15-16 September 2022:

https://srg.doc.ic.ac.uk/klee22/
https://twitter.com/kleesymex/status/1526310428485341187

The first two workshops were really great, with participants from around 
the world (over 80 to the first one in London, over 200 to the second 
one online) with an array of interesting keynotes, talks and posters:

https://srg.doc.ic.ac.uk/klee18/
https://srg.doc.ic.ac.uk/klee21/

I am looking forward to another one, so please consider contributing an 
interesting presentation and/or poster:

https://srg.doc.ic.ac.uk/klee22/cfpresentations.html
https://srg.doc.ic.ac.uk/klee22/cfposters.html

Big thanks to Daniel, Frank, Martin, Hassan and Jamie for their role as 
co-organizers of this 3rd edition!


Many thanks to Bloomberg, Samsung, Google and Imperial College London 
for their sponsorship!  To keep registration costs low, we are still 
looking for a few more sponsors, so if your organization is interested 
in sponsoring the workshop, please let me know.


Looking forward to seeing many of you in September!
Cristian

___
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] 3rd International KLEE Workshop on Symbolic Execution -- 15-16 September, London and online

[Cristian Cadar]

Hi all,

I'm very excited to announce the 3rd International KLEE Workshop on 
Symbolic Execution (KLEE 2022), taking place in London and online on 
15-16 September 2022:

https://srg.doc.ic.ac.uk/klee22/
https://twitter.com/kleesymex/status/1526310428485341187

The first two workshops were really great, with participants from around 
the world (over 80 to the first one in London, over 200 to the second 
one online) with an array of interesting keynotes, talks and posters:

https://srg.doc.ic.ac.uk/klee18/
https://srg.doc.ic.ac.uk/klee21/

I am looking forward to another one, so please consider contributing an 
interesting presentation and/or poster:

https://srg.doc.ic.ac.uk/klee22/cfpresentations.html
https://srg.doc.ic.ac.uk/klee22/cfposters.html

Big thanks to Daniel, Frank, Martin, Hassan and Jamie for their role as 
co-organizers of this 3rd edition!


Many thanks to Bloomberg, Samsung, Google and Imperial College London 
for their sponsorship!  To keep registration costs low, we are still 
looking for a few more sponsors, so if your organization is interested 
in sponsoring the workshop, please let me know.


Looking forward to seeing many of you in September!
Cristian

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

Re: [klee-dev] Collect path constraints with seed mode

[Cristian Cadar]

Hi,

On 21/09/2021 09:00, zy j wrote:

Hi,

I want to collect the path constraints of a specific PoC generated by 
fuzzing, I have found similar question in 
https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg02743.html 
, 
which helps a lot, I added --use-query-log=all:smt2,solver:smt2 
--write-cvcs --write-smt2s to dump the constraints into files, and I got 
the test01.cvc and test01.smt2 successfully.


Considering my purpose is to get the path constraints of given PoC, I 
should use test01.smt2 file, right? But the constraints in that file 
are very few, seems they are not in accumulate mode, but only record the 
constraints for the last branch. If I want to collect the whole path 
constraints for a given PoC (if there are 20 branches before crash, I 
want to collect all of the 20 branches' constraints), how can I do that?
I'm not sure what is the exact question here, but test*.smt2 should 
contain the path condition associated with that path.




Besides, I also noticed that there was a command line option named 
--write-pcs, which seems to be what I need: 
https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg00636.html 
. 
However, there is no --write-pcs in the latest version, is it replaced 
by other option?

It is now --write-kqueries

Best,
Cristian



Best regards,

Jiang


___
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] Need help in making a structure pointer symbolic

[Cristian Cadar]

Hi,

You can make pointers symbolic in KLEE, but this might not accomplish 
what you hope.  Making a pointer symbolic means it can refer to any 
address in memory, including invalid ones.


Best,
Cristian

On 04/03/2022 08:37, Sandip Ghosal wrote:

Hello Everyone,

Can somebody help me to make a pointer to a structure symbolic?

For example, I have a linked list node, and I am trying to make the 
pointer to the structure symbolic as follows:


struct Node{
    int data;
    struct Node *next;
}

struct Node *node = NULL;

node = (struct Node*)malloc(sizeof(struct Node))

klee_make_symbolic(node, sizeof(struct Node *), "e1");


Now what I understand is that Klee is not able to make memory address 
symbolic probably because of infinite address space. Please let me know 
if this is the limitation of Klee or there is some other way for making 
a pointer variable symbolic.


Thanks in advance.

--
Thanks & Regards
Sandip Ghosal




___
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] fork() : creating child processes in KLEE's execution

[Cristian Cadar]

Hi,

KLEE does not use the system call fork() to fork states.  See 
Executor::fork() in the code.


Best,
Cristian

On 23/02/2022 18:40, Pansilu Pitigalaarachchi wrote:

Hi,

I would like to check the possible scenarios where KLEE creates a child 
process.


1.My current understanding is that a 'state fork' performed at a branch 
condition will not result in a real forking of the KLEE process & does 
not invoke fork() syscall to create a child process of klee. i.e. the 
'state forking' described in the original KLEE paper is a process where 
the objects in klee's memory are updated to create a new state.

Can I check if this understanding is correct ?

2.In code, I encountered some cases where the fork() syscall is invoked.
lib/Solver/MetaSMTSolver.cpp
tools/klee-replay/file-creator.c
tools/klee-replay/klee-replay.c etc
Can I check if there are any cases where fork() syscall is issued to 
fork the klee process as a result of 'state forks' in symbolic execution ?


I went through the mailing list history and some literature/papers on 
klee, but cout not find a definite answer. I would really appreciate it 
if someone can help clarify.

Thanks in advance.
--
Pansilu Pitigalaarachchi


___
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] How should the function parameter be symbolised if the function parameter is a file type?

[Cristian Cadar]

Hi,

To use symbolic files, you should use KLEE's symbolic environment 
support.  See https://klee.github.io/docs/options/#symbolic-environment 
and the tutorials for information on how KLEE supports symbolic files.


Best wishes,
Cristian

On 18/01/2022 03:46, rongze xv wrote:

Hi,

I am confused about How should the function parameter be symbolised if 
the function parameter is a file type.


For example, I use KLEE to test a function ok_png ok_png_read(FILE 
*file, ok_png_decode_flags decode_flags), the test code written is as 
follows:

int main(int argc, char **argv){
      FILE *file = malloc(sizeof(FILE));
      klee_make_symbolic(file,sizeof(FILE),"file");
      ok_png_read(file,OK_PNG_COLOR_FORMAT_RGBA);
}
But always get something like this, “memcpy.c:29: memory error: out of 
bound pointer”, I think the function is not tested successfully, I don't 
know how to handle such a situation, please help.


If you can reply to me in your spare time, thank you very much!!

Sincerely，
Xu Rongze

___
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] Packaging klee on Nix - gtest broken?

[Cristian Cadar]

Hi all,

Indeed, it would be great to update 
https://klee.github.io/getting-started/ (via a PR at 
https://github.com/klee/klee.github.io) to mention the Fedora and Nix 
packages.  And thanks to everyone who is maintaining KLEE packages!


Best,
Cristian

On 05/01/2022 10:01, Julian Büning wrote:

Hi Lukas,

nice and thanks for letting me know!

I was briefly considering to go the same route, but didn't encounter 
your fix. But as it turns out, not using gtest_main (which I understand 
is more or less offered for convenience) has certain other advantages 
for KLEE (e.g. stack traces; reducing the number of combinations between 
vanilla Google Test, LLVM's Google Test, llvm-lit, and their respective 
versions). Still, it's certainly a nice addition for llvm-lit, hopefully 
somebody with commit access will pick it up soon!


Thanks to your email I also found out that there is actually a Fedora 
package for KLEE in the main repository. Awesome! I'm not sure how I 
missed that. You should definitely get it mentioned on klee.github.io!


Best,
Julian

On 1/5/22 10:15, Lukas Zaoral wrote:

Hi Julian,
I've encountered the same problem with lit and latest gtest when
I was packaging KLEE for Fedora as I had to use gtest from repos
due to Fedora's packaging guidelines.

I sent a patch to LLVM to fix this incompatibility at the beginning
of last April and it was finally accepted last month [1].  It still needs
to be committed, though.

Sincerely,
Lukas

[1] https://reviews.llvm.org/D100043

On Wed, Jan 5, 2022 at 9:44 AM Julian Büning
 wrote:


Hi Morgan,

nice to see your packaging efforts for KLEE!

I recently ran into some issues with more recent versions of Google Test
when building KLEE (and running unit tests). I just opened a PR that
addresses these: https://github.com/klee/klee/pull/1458

Among these issues is one that I image you may also have run into (as I
assume your package will not be built against Google Test 1.7.0), but it
differs quite a bit from the issue that you linked. Thus, I will go
ahead and describe what I experienced (hoping you can tell me if that
matches what you saw).

When building KLEE with Google Test 1.7.0 and running the unit tests, I
get 36 successfully passed tests. When instead using a newer Google Test
version, like 1.11.0, I get the same number of passed tests, but the
following 10 unresolved tests in addition:

Unresolved Tests (10):
    KLEE Unit tests :: ./AssignmentTest/Running main() from
/some/absolute/path/to/gtest_main.cc
    KLEE Unit tests :: ./DiscretePDFTest/Running main() from
/some/absolute/path/to/gtest_main.cc
    KLEE Unit tests :: ./ExprTest/Running main() from
/some/absolute/path/to/gtest_main.cc
    KLEE Unit tests :: ./RNGTest/Running main() from
/some/absolute/path/to/gtest_main.cc
    KLEE Unit tests :: ./RefTest/Running main() from
/some/absolute/path/to/gtest_main.cc
    KLEE Unit tests :: ./SearcherTest/Running main() from
/some/absolute/path/to/gtest_main.cc
    KLEE Unit tests :: ./SolverTest/Running main() from
/some/absolute/path/to/gtest_main.cc
    KLEE Unit tests :: ./TimeTest/Running main() from
/some/absolute/path/to/gtest_main.cc
    KLEE Unit tests :: ./TreeStreamTest/Running main() from
/some/absolute/path/to/gtest_main.cc
    KLEE Unit tests :: ./Z3SolverTest/Running main() from
/some/absolute/path/to/gtest_main.cc

For each of these "tests" I see some earlier output like this:

UNRESOLVED: KLEE Unit tests :: ./AssignmentTest/Running main() from
/some/absolute/path/to/gtest_main.cc (1 of 46)
 TEST 'KLEE Unit tests :: ./AssignmentTest/Running
main() from /some/absolute/path/to/gtest_main.cc' FAILED

Unable to find '[  PASSED  ] 1 test.' in gtest output:

Running main() from /some/absolute/path/to/gtest_main.cc
Note: Google Test filter = Running main() from
/some/absolute/path/to/gtest_main.cc
[==] Running 0 tests from 0 test cases.
[==] 0 tests from 0 test cases ran. (0 ms total)
[  PASSED  ] 0 tests.



The last 3 lines look similar to the output in the issue you linked. But
this is simply the output of Google Test when there are no `TEST()`s
next to `main()` in an executable. The rest stems from a different
problem (detailed below).

Is this also the issue you ran into? If yes, maybe you want try the
patches from the PR I linked above. If not and are you having a
different problem, maybe you could try to provide some more details?
Then I will try and see if can help resolve them.

--- BEGIN: More details ---

The issue we see above actually stems from llvm-lit, not from Google
Test itself. Starting from 1.8.1, Google Test's gtest_main.cc uses
`__FILE__` [1] instead of a fixed string [2] to output a line like this:
  > Running main() from /some/absolute/path/to/gtest_main.cc

To determine which tests exist, llvm-lit will call each executable with
the `--gtest_list_tests` argument. However, the (usually) first line
will be the above "Running main()" output. To 

Re: [klee-dev] Default counterexample value generated by solver

[Cristian Cadar]

Hi Weiqi,

There is an open PR trying to implement this behaviour, but 
unfortunately it has not been finalized yet (perhaps you'd like to work 
on it?):

https://github.com/klee/klee/pull/1117

Best,
Cristian

P.S. Kleaver does not pick the smallest valid value, the value generally 
comes from the solver


On 20/09/2021 16:59, Weiqi Wang wrote:

Hi,

I observed that when asked for a counterexample, kleaver picks the 
smallest valid value. I’m wondering if there’s a way to “seed the 
solver” so that it prioritizes the value given in the seed? For example, 
given constraint x != 1, the counterexample value would be 0. With a 
seed value 3, the solver picks 3 instead.


Best,

Weiqi


___
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] How to distinguish klee's print of different execution paths

[Cristian Cadar]

Hi, you would need to modify the code associated with those klee_ 
intrinsics to also output state information (see 
https://github.com/klee/klee/blob/master/lib/Core/SpecialFunctionHandler.cpp).


Best,
Cristian

On 01/09/2021 16:38, 樊雨鑫 wrote:

Hi,
 I am new to Klee, use it to do program analysis.
 I want some intermediate variables' symbolic expressions. So I use 
klee_print_expr() and klee_print_range() to make that.
 But Klee prints all messages together, and no information show whether two 
messages belong to the same execution path.
 for a very simple example: there are many massages printed but they looks 
have no difference except for the symbolic expressiones.
```for (int8_t i = 0; i < size; i++) {
 for (int8_t j = 0; j < size; j++) {
 bool omatch = (aarr[i] == barr[j]);
 klee_print_expr("omatch", omatch);
 if ( omatch ) {
 int8_tersection[i] = barr[j];
 break;
 }
 }
 }
```
 I tried to add random value as an id(by seed srand(time(0)))  at the end 
of the program, but different paths still may have the same random seeds.
 How to make it that make messages of klee_print_expr can be classified by 
their execution paths?
 
 Waiting for your reply.

___
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] Write to symbolic position

[Cristian Cadar]

Hi Weiqi,

Note that such an assignment does not impose any constraints on the 
input, which is why you don't see them in the path constraints 
(otherwise a simple code snippet such as buf[1] = '9'; buf[2] = '0' 
would be considered infeasible).  You might want to check the initial 
KLEE paper for more details.


Best,
Cristian

On 26/08/2021 14:55, Weiqi Wang wrote:

Hi,

I’m wondering whether klee generate constraints when a concrete value is 
written to symbolic position? I tried a toy program and it seemed klee 
doesn’t. Specifically, I added a `buf[1] = ‘9’ before the password check 
in check_password(). But I only get constraint: (Eq 104 (Read w8 0 
A-data)) due to short-circuit evaluation. What I would like to see are 
two constriants: (Eq 104 (Read w8 0 A-data)) and (Eq 57 (Read w8 1 A-data))


Is there an easy way to add this feature? Could you give me some hint on 
which file to modify?


Best,

Weiqi


___
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] Improving KLEE coverage

[Cristian Cadar]

Hi Vlad,

It's difficult to say without seeing the full program, but it could be 
that KLEE is spending all its time in some other parts on the code.  You 
can use klee-stats to understand how many states are in memory, how much 
time is spent in constraint solving etc., and kcachegrind to visualize 
code-level statistics (see 
https://klee.github.io/tutorials/testing-coreutils/)


Best,
Cristian

On 23/07/2021 14:22, Vlad Ivanov wrote:

Hello KLEE developers,
  
first of all thank you for working on this tool and making it available to the

public. I'm working on using KLEE to fuzz a simple RPC protocol. The setup is as
follows:
  
1. Create a symbolic variable buffer_size and use klee_assume on it to create

a constraint of maximum size
2. Allocate a buffer of length buffer_size and make it symbolic as well
3. Take some data from random buffer and use it to create RPC request
4. Pass the request to the RPC endpoint input function
  
I've created a setup to collect coverage data after KLEE is done fuzzing and put

it into a HTML report. I can see that within several minutes, several paths are
discovered but for some reason, even when running for hours, KLEE doesn't seem
to be able to get past certain conditions in code.
  
To illustrate, here's a code example (numbers on the left represent hit count):
  
 163auto const cSize = mapSize(inputBuffer[4]);

 163
 163if (inputBuffer[5] != cSize)
 163{
 163return ArgumentError;
 163}
 0
 0  if (inputBuffer[6] != cSize)
 0  {
 0  return ArgumentError;
 0  }
  
While I can't share the exact program this is the type of checks that's

ultimately happening there. What I find interesting is that in order to reach
this point, a rather complex set of conditions has to be satisfied: basically,
7 or so positions in the input buffer need to match a specific set of constants.
These constants are discovered rather quickly, and it would seem to me that
there should be no trouble in finding the 8th one, but that's not what I'm
seeing, and after many hours of fuzzing I'm stuck with the same number of test
cases I had when I ran fuzzing just for a few minutes.
  
The command line I'm using to start fuzzing is rather simple:
  
 klee --optimize --libcxx --libc=uclibc --posix-runtime ./build/application
  
And here's a --version output:
  
 KLEE 2.2 ()

   Build mode: RelWithDebInfo (Asserts: ON)
   Build revision: 5719d2803e93252e5d4613f43afc7db0d72332f1
 
 LLVM ():

   LLVM version 11.0.0
   Optimized build.
   Default target: x86_64-unknown-linux-gnu
   Host CPU: skylake
  
KLEE is built with Z3 support.
  
What would be a good way to understand why it's not progressing further?

Perhaps there is some sort of option to try?

(apologies for the previous non-plaintext email)
  
Best Regards,
  
Vlad


___
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] Inquiry on path record and reply component of KLEE

[Cristian Cadar]

Hi Harper,

As I mentioned on GitHub, the .path feature is currently unmaintained, 
but it would be great to revive it.


Best,
Cristian

On 10/07/2021 15:24, Wei Chen wrote:

Dear developers,

Hi, I found there is a case that KLEE would generate the same .path 
files for different paths in programs. Further, when given different 
path files, the replay feature of Klee produces the same input for these 
two paths. Here are the details:


For the attached file test_1.c, the aforementioned problem can be 
reproduced by executing the following commands:


Attachment-1.png

KLEE would generate 3 paths for this program, then unfortunately 
klee-out-0/test02.path and klee-out-0/test03.path are exactly 
the same as each other. That’s weird because they are regarded as 
different paths by klee.


For the replay feature of klee, given klee-out-0/test01.path and 
klee-out-0/test02.path (two different paths), by executing klee with 
—-replay-path option, two paths will be replayed and two test cases will 
be generated.


However, the two test cases klee-out-1/test01.ktest and 
klee-out-2/test01.ktest are exactly the same with each other.


Attachment.png

The attachment test_2.c also has the same .path problem, but the reply 
feature works fine.


In that case, I’m wondering if there are some bugs inside the 
path-related component of klee. The version of klee that I used is shown 
as below:


image.png

Looking forward to your kind reply.

Best,
Harper

___
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] About the two methods of test replay.

[Cristian Cadar]

Hi Alex,

I noticed this email went unanswered, hopefully the response is still 
useful.  In short, we plan to maintain both replay methods.  As you 
point out, the klee-replay tool only works when there are no klee_ 
intrinsics in the code.  In this case, it is the preferred method, as 
it's easier to use, you just need the native binary and a ktest file. 
The other method is more general, but a bit more difficult to use.


Best,
Cristian

On 05/04/2021 21:46, Alex Babushkin wrote:
Hello, I'm sorry if this has ever been asked before, but why are there 
two methods for replaying test cases? The first is to link your bitcode 
file with the build-generated libraries consisting of functions in 
instrinsics.c and so on, and the second one is to use the klee-replay 
utility. I wonder whether one of the options is favoured or not, or 
maybe some option is to-be-deprecated in the future? Also, is there a 
guide on how to use the klee-replay utility properly? klee-replay.c has, 
for example, the "klee_make_symbolic" function definition, so, I assume, 
it is capable of replaying tests for programs that were instrumented 
with "klee_make_symbolic". Yet, klee-replay is mentioned only in the 
"Testing Coreutils" guide, in which there is no "klee-make-symbolic" 
instrumentation involved. So, how should executables for klee-replay be 
produced out of corresponding bitcode files?


Since this is a question about pure usage of the instrument, I'm sorry 
If it is a product of bad research of mine. If, however, not, then I 
think it would be good to add the appropriate documentation to the klee 
website.


Thank you for your response in advance, Alex.

___
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] Filename length for kleaver

[Cristian Cadar]

Hi Weiqi,

I haven't looked at the code yet, but if this happens only for filenames 
longer than 32 characters, this might be a bug.  Can you file an issue 
on GitHub, with an example?


Best,
Cristian

On 06/08/2021 21:23, Weiqi Wang wrote:

Hi,

I noticed that kleaver generates different solutions if the .kquery 
filename is longer than 32 characters. Is the filename used as some kind 
of seed for the solver?


Best,

Weiqi


___
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] Postdoctoral position at Imperial College London

[Cristian Cadar]

Hi all,

We have another open postdoctoral position in my group, which involves 
projects that build up on KLEE (as well as others):

https://srg.doc.ic.ac.uk/vacancies/postdoc-pass-22/

I am happy to answer any informal queries (but please don't reply to the 
whole list).


Best,
Cristian

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

Re: [klee-dev] Phi nodes and LLVM11

[Cristian Cadar]

Hi Alastair,

I think your suspicions are reasonable, but perhaps the first thing 
would be to report a small code example that triggers this issue.  Have 
you tried C-Reduce?


Best,
Cristian

On 28/06/2021 15:02, Alastair Reid wrote:

Hi,

I am seeing KLEE crash on a large example generated by the Rust compiler 
with LLVM11 and wonder if you could help suggest some ways to narrow 
down what is going wrong so that I can submit a usable bug report.


Given the repeated mention of phi nodes in the error output (below), I 
wonder if I should be looking in the PhiCleaner pass?
Or, given the mention of insertelement, I wonder if I should be looking 
at the Scalarizer pass (because I know that rustc and LLVM11 are 
aggressively using LLVM11's generic vector intrinsics.

Any thoughts?



What I am seeing is a large number of error reports like this:

Instruction does not dominate all uses!
   %.i0385 = phi i64 [ ,  ], [ %.i0664, %2236 ], [ 
%.i0381, %2227 ], !dbg !30427

   %.upto04194 = insertelement <4 x i64> undef, i64 %.i0385, i32 0

terminating in the following message and stack dump.

PHI nodes not grouped at top of basic block!
   %.i0345 = phi i64 [ ,  ], [ %.i0679, %2236 ], [ 
%.i0341, %2227 ]

label %2370
in function _ZN4test9run_tests17h3c40b1ee8455d4dbE
LLVM ERROR: Broken function found, compilation aborted!
  #0 0x7efc61604f8f llvm::sys::PrintStackTrace(llvm::raw_ostream&) 
(/usr/lib/llvm-11/lib/libLLVM-11.so.1+0xbd0f8f)
  #1 0x7efc616032c2 llvm::sys::RunSignalHandlers() 
(/usr/lib/llvm-11/lib/libLLVM-11.so.1+0xbcf2c2)

  #2 0x7efc61605465 (/usr/lib/llvm-11/lib/libLLVM-11.so.1+0xbd1465)
  #3 0x7efc60597d60 (/lib/x86_64-linux-gnu/libc.so.6+0x3bd60)
  #4 0x7efc60597ce1 raise 
./signal/../sysdeps/unix/sysv/linux/raise.c:51:1

  #5 0x7efc60581537 abort ./stdlib/abort.c:81:7
  #6 0x7efc61554d68 (/usr/lib/llvm-11/lib/libLLVM-11.so.1+0xb20d68)
  #7 0x7efc61554b88 (/usr/lib/llvm-11/lib/libLLVM-11.so.1+0xb20b88)
  #8 0x7efc61781b8f (/usr/lib/llvm-11/lib/libLLVM-11.so.1+0xd4db8f)
  #9 0x7efc61714059 
llvm::FPPassManager::runOnFunction(llvm::Function&) 
(/usr/lib/llvm-11/lib/libLLVM-11.so.1+0xce0059)
#10 0x7efc61719603 llvm::FPPassManager::runOnModule(llvm::Module&) 
(/usr/lib/llvm-11/lib/libLLVM-11.so.1+0xce5603)
#11 0x7efc61714670 llvm::legacy::PassManagerImpl::run(llvm::Module&) 
(/usr/lib/llvm-11/lib/libLLVM-11.so.1+0xce0670)
#12 0x56428d2b590b klee::KModule::checkModule() 
/usr/local/google/home/adreid/rust/klee/lib/Module/KModule.cpp:378:3
#13 0x56428d260f50 std::__uniq_ptr_implstd::default_delete >::_M_ptr() const 
/usr/include/c++/10/bits/unique_ptr.h:173:58
#14 0x56428d260f50 std::unique_ptrstd::default_delete >::get() const 
/usr/include/c++/10/bits/unique_ptr.h:422:27
#15 0x56428d260f50 std::unique_ptrstd::default_delete >::operator->() const 
/usr/include/c++/10/bits/unique_ptr.h:416:12
#16 0x56428d260f50 
klee::Executor::setModule(std::vectorstd::default_delete >, 
std::allocatorstd::default_delete > > >&, 
klee::Interpreter::ModuleOptions const&) 
/usr/local/google/home/adreid/rust/klee/lib/Core/Executor.cpp:567:20
#17 0x56428d23fbe0 main 
/usr/local/google/home/adreid/rust/klee/tools/klee/main.cpp:1415:46

#18 0x7efc60582d0a __libc_start_main ./csu/../csu/libc-start.c:308:16
#19 0x56428d24f56a _start (bin/klee+0x3a56a)
Aborted



___
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] Workshop starting in 15'!

[Cristian Cadar]

For those of you who registered, just a reminder that the workshop 
starts in 15' (making sure there is no timezone confusion!)


Best,
Cristian

On 09/06/2021 12:55, Cristian Cadar wrote:

Hi all,

Just a reminder that the registration for the KLEE workshop is closing 
today.  We have around 200 registrations, and many interesting talks, so 
it should be a lively workshop!

https://srg.doc.ic.ac.uk/klee21/registration.html

For those of you who have registered (except those having registered 
today), you should have received an email called "Instructions for 
attending the 2nd International KLEE Workshop" from kleesy...@gmail.com. 
  If you haven't received it, please check your spam folder first and 
then email us at kleesy...@gmail.com.


Best,
Cristian

On 25/05/2021 17:56, Cristian Cadar wrote:

Hi all,

I am happy to let you know that registration is now open for the 2nd 
KLEE workshop, taking place online on 10-11 June:

https://srg.doc.ic.ac.uk/klee21/registration.html

We have a very interesting program with a keynote from Chao Wang on 
adversarial symbolic execution for detecting side-channel leaks:

https://srg.doc.ic.ac.uk/klee21/keynote.html

and 24 presentations from across the globe on a variety of interesting 
topics:

https://srg.doc.ic.ac.uk/klee21/presentations.html

Big thanks to our sponsors this year: Bloomberg, Samsung, Google and 
Imperial College London!


Best,
Cristian

___
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

[klee-dev] [REMINDER] Registration now open for the 2nd International KLEE Workshop on Symbolic Execution

[Cristian Cadar]

Hi all,

Just a reminder that the registration for the KLEE workshop is closing 
today.  We have around 200 registrations, and many interesting talks, so 
it should be a lively workshop!

https://srg.doc.ic.ac.uk/klee21/registration.html

For those of you who have registered (except those having registered 
today), you should have received an email called "Instructions for 
attending the 2nd International KLEE Workshop" from kleesy...@gmail.com. 
 If you haven't received it, please check your spam folder first and 
then email us at kleesy...@gmail.com.


Best,
Cristian

On 25/05/2021 17:56, Cristian Cadar wrote:

Hi all,

I am happy to let you know that registration is now open for the 2nd 
KLEE workshop, taking place online on 10-11 June:

https://srg.doc.ic.ac.uk/klee21/registration.html

We have a very interesting program with a keynote from Chao Wang on 
adversarial symbolic execution for detecting side-channel leaks:

https://srg.doc.ic.ac.uk/klee21/keynote.html

and 24 presentations from across the globe on a variety of interesting 
topics:

https://srg.doc.ic.ac.uk/klee21/presentations.html

Big thanks to our sponsors this year: Bloomberg, Samsung, Google and 
Imperial College London!


Best,
Cristian

___
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] Registration now open for the 2nd International KLEE Workshop on Symbolic Execution

[Cristian Cadar]

Hi all,

I am happy to let you know that registration is now open for the 2nd 
KLEE workshop, taking place online on 10-11 June:

https://srg.doc.ic.ac.uk/klee21/registration.html

We have a very interesting program with a keynote from Chao Wang on 
adversarial symbolic execution for detecting side-channel leaks:

https://srg.doc.ic.ac.uk/klee21/keynote.html

and 24 presentations from across the globe on a variety of interesting 
topics:

https://srg.doc.ic.ac.uk/klee21/presentations.html

Big thanks to our sponsors this year: Bloomberg, Samsung, Google and 
Imperial College London!


Best,
Cristian

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

[klee-dev] 2nd KLEE Workshop: Presentation proposals due on 10th May

[Cristian Cadar]

Hi all,

Just a quick reminder that the presentation proposal deadline for the 
2nd International KLEE Workshop on Symbolic Execution is coming up, on 
Monday, 10th May.


We have already received many interesting proposals, but there is still 
time for more!


https://srg.doc.ic.ac.uk/klee21/cfpresentations.html

Best,
Cristian

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

Re: [klee-dev] KLEE as bitcode interpreter

[Cristian Cadar]

Yes, without any symbolic input, KLEE essentially functions like an 
interpreter for LLVM bitcode.


Best,
Cristian

On 19/03/2021 11:49, prashant chaturvedi wrote:

Hi all.
  I have compiled a source file to bitcode without debug information, 
i'm not using "any" of the KLEE's intrinsic, i.e i'm not making anything 
symbolic, just obtained a vanilla bitcode. If i run that bitcode in 
KLEE, does KLEE here work llike  a bitcode interpreter? (like lli).  Is 
it then really then same as running it on lli?


Thank you in advance!

___
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] Running KLEE for 32-bit

[Cristian Cadar]

Hi,

We don't support 32-bit anymore.  See e.g.:

https://github.com/klee/klee/issues/1327
https://github.com/klee/klee/issues/286

Cristian

On 23/03/2021 06:08, kmohit wrote:

Hi,
KLEE version: 2.2
LLVM version: 9.0.0
Uclibc version: 1.2
Solver: Z3
I am trying to run a 32-bit bitcode on KLEE but I am getting the 
following error :

*LLVM ERROR: 64-bit code requested on a subtarget that doesn't support it!*
**
**
*
*After a little bit of research I found that building klee on 32 bit 
system, I can run 32 bitcode on KLEE. However, I am unable to build 
KLEE-2.2 on 32 bit system.

My question is how can I run 32 bitcode on klee version 2.2.
Thanks  in advance !
Mohit kumar


For assimilation and dissemination of knowledge, visit cakes.cdac.in

150th Anniversary Mahatma Gandhi

 


[ C-DAC is on Social-Media too. Kindly follow us at:
Facebook: https://www.facebook.com/CDACINDIA & Twitter: @cdacindia ]

This e-mail is for the sole use of the intended recipient(s) and may
contain confidential and privileged information. If you are not the
intended recipient, please contact the sender by reply e-mail and destroy
all copies and the original message. Any unauthorized review, use,
disclosure, dissemination, forwarding, printing or copying of this email
is strictly prohibited and appropriate legal action will be taken.
 



___
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] Homebrew Package

[Cristian Cadar]

Hi Carlo,

We had a Homebrew tap set up a while ago see, 
https://github.com/klee/homebrew-klee, but it is currently unmaintained. 
 So what we need is to have maintainers for these different packages. 
This is why it was great to hear about the Homebrew package you created 
(which I hope you'd like to maintain) and about the other packages of 
KLEE being maintained by other volunteers.


Best,
Cristian

On 15/03/2021 21:41, Carlo Cabrera wrote:

Hi Cristian,


Could you document more precisely the challenges you have encountered? Perhaps 
it would be best to continue the discussion on GitHub; I've just created this 
issue: https://github.com/klee/klee/issues/1395


Sure, I'll respond to you there.


BTW, one major disadvantage with using the Homebrew package (compared to say, 
Docker) is that it doesn't have support for uclibc and the POSIX runtime.  This 
is, of course, a limitation of KLEE/uclibc on macOS rather than an issue with 
the package itself.  But that's why it would be great to have a package 
targetting Linux directly, with uclibc and POSIX runtime support included.


I agree. I could try to get this enabled for the Linux package, but it
seems I would need to get uClibc-ng packaged for Homebrew on Linux
first. It's doable, but may take me some time.

An alternative to this is for KLEE to host a Homebrew tap [1] in your
GitHub organisation. This will allow you to package KLEE yourself and
distribute it using the Homebrew CLI.

For example, once you have a tap with a KLEE package set up, installing
KLEE from your tap would be as simple as doing

 brew install klee/tap/klee

This can be set up so that it installs a pre-built binary package
configured the way you prefer. (There are some naming issues involved,
so the thing you're installing may not be called "klee/tap/klee"
exactly.)

[1] https://docs.brew.sh/Taps

Best,
Carlo



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

Re: [klee-dev] Using KLEE to analyze (complex) data structures

[Cristian Cadar]

Hi,

You say that you "got no useful results from KLEE so far" but it's 
difficult to help without more info and a self-contained program which 
reproduces the problem.


Most likely though, you are hitting the challenge described in this 
paper, which offers a solution (and an extension of KLEE) which can deal 
better with complex data structures such as hashtables:

https://srg.doc.ic.ac.uk/projects/klee-segmem/

Best,
Cristian

On 12/03/2021 10:53, Jens Van den Broeck wrote:

Hello klee-dev members,

I'm doing research on software protection techniques for compiled
programs. To assess the strength of one of my techniques, I want to know
whether KLEE can be used to analyze my protection. Conceptually, I
protect programs with "flexible opaque predicates", a form of
context-sensitive opaque predicates. Instead of encoding a TRUE or FALSE
value in a (complex) computation, I manipulate the state of some
(complex) data structure.

As an example, consider the following simplified program in which a hash
table is used to encode a flexible opaque predicate. Concretely, I want
to know whether or not there is a way for KLEE to indicate under what
conditions the TRUE and FALSE paths of the flexible opaque predicate
(label "flexible_opaque_predicate" in the example) implemented in
'protected_function' can be taken. Ideally, this would be some valid
state for the protection data structure ("protection_ds" in the example).

I tried marking the entire data structure as symbolic, but got no useful
results from KLEE so far: klee_make_symbolic(protection_ds,
sizeof(t_hashtable), "protection_ds"). But maybe there is another way?
Or it is not possible?

char *protection_key = "some_string";
t_hashtable *protection_ds = NULL;

// some implemented hash table operations
void hashtable_remove_entry(t_hashtable *table, void *key) {
   ... // hash key with function 'table->hash_func_ptr' and remove bucket
}
void hashtable_set_entry(t_hashtable *table, void *key, void *value) {
   ... // hash key with function 'table->hash_func_ptr' and store value
in bucket
}
bool hashtable_contains_entry(t_hashtable *table, void *key) {
   ... // hash key with function 'table->hash_func_ptr' and return TRUE
if bucket exists
}

void protected_function() {
   ...
   // set predicate to TRUE
   hashtable_set_entry(protection_ds, protection_key, (void *)42);
   ...
flexible_opaque_predicate:
   if (hashtable_contains_entry(protection_ds, protection_key) {
     ... // executed when the predicate is set to 'TRUE' (see higher)
   }
   else {
     ... // executed when the predicate is set to 'FALSE' (see below)
     goto finalize;
   }
   ...
   // set predicate to FALSE
   hashtable_remove_entry(protection_ds, protection_key);
   ...
   goto flexible_opaque_predicate;
finalize:
   ...
}

int main(int argc, char** argv) {
   protection_ds = create_hashtable(hash_func_ptr); //'hash_func_ptr' is
a pointer to a hash function
   ... // do some work
   protected_function();
   ... // do more work
}

Thanks in advance,
Jens



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

Re: [klee-dev] Homebrew Package

[Cristian Cadar]

Hi Carlo,

On 13/03/2021 14:21, Carlo Cabrera wrote:

Hi Cristian and Anton,

Thanks for the kind words.

I looked into getting a pre-built package on Linux, but it's a little
tricky because KLEE has some build dependencies that aren't in Homebrew.
Could you document more precisely the challenges you have encountered? 
Perhaps it would be best to continue the discussion on GitHub; I've just 
created this issue: https://github.com/klee/klee/issues/1395


BTW, one major disadvantage with using the Homebrew package (compared to 
say, Docker) is that it doesn't have support for uclibc and the POSIX 
runtime.  This is, of course, a limitation of KLEE/uclibc on macOS 
rather than an issue with the package itself.  But that's why it would 
be great to have a package targetting Linux directly, with uclibc and 
POSIX runtime support included.



However, I opened a pull request to update the website with installation
instructions.

Thanks!

Best,
Cristian



Best,
Carlo


On 12 Mar 2021, at 17:13, Cristian Cadar  wrote:

Hi Carlo,

This is great to hear!  Thanks for this contribution!

We should update the website with this info soon.

It would be of course great to have one for Linux too; from what I can tell, 
many of our users use Ubuntu, although I don't have any stats.

Best,
Cristian

On 12/03/2021 16:45, Carlo Cabrera wrote:

Dear klee-dev,
I noticed that packaging was listed as an open project on the website.
So, I submitted klee for packaging at Homebrew [1].
If you use Homebrew (on macOS or Linux), you can now install klee with
 brew install klee
It is built with libc++, but without exception handling. EH lead to a
build failure on macOS.
The Homebrew package has a pre-built binary on macOS. If there is
interest in one for Linux as well, I can look into it.
Best,
Carlo
[1] https://brew.sh
___
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

[klee-dev] 2nd edition of the KLEE workshop moving online

[Cristian Cadar]

Dear all,

Thanks, Alastair for the reminder, we have literally just reached a 
decision about the new editions of the KLEE workshop.


As you know, we were hoping to have the second edition in London, 
similar to the first.  The atmosphere at the first workshop was 
fantastic, and we were delighted to see the excellent feedback 
afterwards.  We have also run a survey among the authors of the 
presentations accepted to the upcoming edition of the workshop, and over 
90% of respondents expressed a preference for a physical workshop.


Unfortunately, given the current situation with the pandemic, it is not 
possible to organize a physical workshop this year.  As for the first 
edition, we have people from three different continents and the chances 
of unconstrained international travel from so many different countries 
is essentially zero.


So here are our plans.  We hope to have the next in-person KLEE workshop 
sometime in 2022; we will announce it once there is more clarity with 
respect to in-person events and international travel.  However, in the 
meantime, in order to have some continuity, we have decided to try a 
smaller online event this June.  We will have a separate call for online 
presentations, but if you already have a presentation accepted, you will 
be able to simply sign up for a slot.  Furthermore, it is ok to present 
the same talk at the online event this year and at the bigger in-person 
event next year.


We plan two sessions of a few hours each, with the goal of having at 
least one session at a workable time around the world.


The new dates are:
Submission deadline: 10 May 2021
Notification: 18 May 2021
Online workshop: Thursday, 10 June 2021 starting at 5pm UK time and
 Friday, 11 June 2021 starting at 10am UK time

Of course, the exact schedule will depend on the interest we see in an 
online workshop, and we might have a single session, or no online 
workshop at all, if interest is really low in an online event.


We will update the website and the submission site shortly.

Any feedback would be of course appreciated.

Looking forward to seeing you online in June!
Cristian, on behalf of the KLEE Workshop organizing team

On 15/03/2021 09:22, Alastair Reid wrote:
With the workshop fast approaching, I have been waiting for registration 
to open (and wondering if the workshop is only open to those 
presenting). https://srg.doc.ic.ac.uk/klee21/registration.html


--
Alastair

___
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] Homebrew Package

[Cristian Cadar]

Hi Carlo,

This is great to hear!  Thanks for this contribution!

We should update the website with this info soon.

It would be of course great to have one for Linux too; from what I can 
tell, many of our users use Ubuntu, although I don't have any stats.


Best,
Cristian

On 12/03/2021 16:45, Carlo Cabrera wrote:

Dear klee-dev,

I noticed that packaging was listed as an open project on the website.
So, I submitted klee for packaging at Homebrew [1].

If you use Homebrew (on macOS or Linux), you can now install klee with

 brew install klee

It is built with libc++, but without exception handling. EH lead to a
build failure on macOS.

The Homebrew package has a pre-built binary on macOS. If there is
interest in one for Linux as well, I can look into it.

Best,
Carlo

[1] https://brew.sh

___
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] Question on dereferencing a symbol pointer

[Cristian Cadar]

Hi,

The short answer is that KLEE does not support mmap.

However, it shouldn't crash and I cannot reproduce that behaviour: when 
I run it, KLEE reports a memory error at "*(int*)addr = 0;", as I also 
expected.


Best,
Cristian

On 09/03/2021 14:46, Liu, Mingyi wrote:

Hi klee-dev members,

I made a pointer symbolic in a program, but I didn't understand why the 
results were different with the following two scenarios.


Case 1:

#include "klee/klee.h"
#include 
#include 
#include 
#include 

int main(int argc, char* argv[]) {

   int* ptr;

   klee_make_symbolic(, sizeof(ptr), "ptr");

   void* addr = mmap((void*)(rand() & (~0xfff)), getpagesize(), 
PROT_READ | PROT_WRITE, MAP_ANONYMOUS | MAP_FIXED | MAP_PRIVATE, -1, 0);


   if (addr == MAP_FAILED) {
     printf("mmap error\n");
     exit(-1);
   }

   *(int*)addr = 0;

   printf("ptr=%p\n", ptr);

   if (ptr == (int*)addr) {
     printf("enter\n");
     *ptr = 65;
*printf("after: *ptr=%s\n", ptr);*
   }

   return 0;

}

After running klee with the command $ klee -write-kqueries 
-external-calls=all program.bc , I got 2 paths as expected:


KLEE: done: total instructions = 45
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

The output when executing against the second ktest file is shown below:

ptr=0x6b8b4000
enter
after: *ptr=A

However, in Case 2, the only difference is that I replaced 
*printf("after: *ptr=**%s**\n", **ptr**);* with *printf("after: 
*ptr=%d\n", *ptr); *. When running with the same command, the program 
was aborted with the following messages:


klee: /usr/lib/llvm-6.0/include/llvm/Support/Casting.h:92: static
bool llvm::isa_impl_cl::doit(const From*) [with To =
klee::ConstantExpr; From = klee::Expr]: Assertion `Val && "isa<>
used on a null pointer"' failed.
#0 0x7fe5c64b60ea llvm::sys::PrintStackTrace(llvm::raw_ostream&)
(/usr/lib/llvm-6.0/lib/libLLVM-6.0.so.1+0x81e0ea)
#1 0x7fe5c64b4366 llvm::sys::RunSignalHandlers()
(/usr/lib/llvm-6.0/lib/libLLVM-6.0.so.1+0x81c366)
#2 0x7fe5c64b449b (/usr/lib/llvm-6.0/lib/libLLVM-6.0.so.1+0x81c49b)
#3 0x7fe5c5173fd0 (/lib/x86_64-linux-gnu/libc.so.6+0x3efd0)
#4 0x7fe5c5173f47 gsignal

/build/glibc-2ORdQG/glibc-2.27/signal/../sysdeps/unix/sysv/linux/raise.c:51:0
#5 0x7fe5c51758b1 abort
/build/glibc-2ORdQG/glibc-2.27/stdlib/abort.c:81:0
#6 0x7fe5c516542a __assert_fail_base
/build/glibc-2ORdQG/glibc-2.27/assert/assert.c:89:0
#7 0x7fe5c51654a2 (/lib/x86_64-linux-gnu/libc.so.6+0x304a2)
#8 0x55d863a75ba0
klee::ExprOptimizer::optimizeExpr(klee::ref const&,
bool) /vagrant/vagrant/xxx/klee/lib/Expr/ArrayExprOptimizer.cpp:193:0
#9 0x55d8639dd657
klee::ref::operator=(klee::ref&&)
/vagrant/vagrant/xxx/klee/include/klee/util/Ref.h:184:0
#10 0x55d8639dd657
klee::Executor::callExternalFunction(klee::ExecutionState&,
klee::KInstruction*, llvm::Function*,
std::vector,
std::allocator > >&)
/vagrant/vagrant/xxx/klee/lib/Core/Executor.cpp:3366:0
#11 0x55d8639e9668
klee::Executor::executeCall(klee::ExecutionState&,
klee::KInstruction*, llvm::Function*,
std::vector,
std::allocator > >&)
/vagrant/vagrant/xxx/klee/lib/Core/Executor.cpp:1441:0
#12 0x55d8639f11e7
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*)
/vagrant/vagrant/xxx/klee/lib/Core/Executor.cpp:2015:0
#13 0x55d8639f27ad klee::Executor::run(klee::ExecutionState&)
/vagrant/vagrant/xxx/klee/lib/Core/Executor.cpp:3110:0
#14 0x55d8639f30bc
std::enable_if
 >, std::is_move_constructible,
std::is_move_assignable >::value, void>::type
std::swap(klee::PTree*&, klee::PTree*&)
/usr/include/c++/7/bits/move.h:198:0
#15 0x55d8639f30bc std::unique_ptr >::reset(klee::PTree*)
/usr/include/c++/7/bits/unique_ptr.h:369:0
#16 0x55d8639f30bc std::unique_ptr >::operator=(decltype(nullptr))
/usr/include/c++/7/bits/unique_ptr.h:307:0
#17 0x55d8639f30bc
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**,
char**) /vagrant/vagrant/xxx/klee/lib/Core/Executor.cpp:4261:0
#18 0x55d8639c23f3 main
/vagrant/vagrant/xxx/klee/tools/klee/main.cpp:1555:0
#19 0x7fe5c5156b97 __libc_start_main
/build/glibc-2ORdQG/glibc-2.27/csu/../csu/libc-start.c:344:0
#20 0x55d8639ce7ea _start (.//klee+0x6c7ea)
Aborted (core dumped)


Could anyone please explain to me why that assertion failed? Or is it a 
bug?


Thanks in advance!

Best,
Mingyi

___
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] Use of -sym-stdin/stdout

[Cristian Cadar]

On 09/02/2021 14:09, Eduardo R B Marques wrote:

2) you should only use —sym-sdout if you need to symbolically analyze the 
contents of stdout, otherwise don't set it



Yes, that’s right, I do want to “analyze the contents of stdout”. But how can 
it be done? As I mentioned, the ktest files do not
seem to contain the symbolic “stdout”.

Note that this makes sense: stdout is only written into.
To analyze its contents, you will have to manipulate directly the stdout 
buffer used by the POSIX runtime; unfortunately there is no better 
interface right now.



Also, regarding my other question, I assume that —libc=uclibc is a requirement 
for using -sym-stdin/sym-stdout ?
No, it's not.  It can be used independently.  However, the issues you 
run into are related to the fact that you use libc functions that 
manipulate stdin/stdout, which are called as external functions without 
-—libc=uclibc.


Best,
Cristian



Thanks, best regards,
Eduarrod


On 9 Feb 2021, at 11:33, Cristian Cadar  wrote:

Hi Eduardo,

Indeed, we need better documentation here.  But in a nutshell:

1) printf is run concretely by default (you can add -DKLEE_SYM_PRINTF when 
compiling KLEE's uclibc to change this)

2) you should only use —sym-sdout if you need to symbolically analyze the 
contents of stdout, otherwise don't set it

Best,
Cristian

On 06/02/2021 20:28, Eduardo R B Marques wrote:

Hi,
I have a few questions regarding the use of the -sym-stdin / -sym-stdout 
options. Consider the following simple program in a file named foo.c:
*#include *
*
int main(int argc, char** argv) {
   int c = getchar();
   if (c >= 'a' && c <= 'z')
 printf("lower case\n");
   else if (c >= 'A' && c <= 'Z')
 printf("upper case\n");
   else printf("Other\n");
   return 0;
}*
Using the klee 2.1  docker image I compile it as follows:
*clang -emit-llvm -std=c89 foo.c -c -o foo.bc*
then execute it using:
*klee -posix-runtime --libc=uclibc foo.bc -sym-stdin 1 -sym-stdout*
I obtain a few warnings that do not seem (at first) too relevant regarding the 
use printf (external function), but that’s all.
5 paths are explored in total.
My questions arise when I consider variations of this overall setup:
1) Suppose I change the first printf call
*  printf("lower case\n”);*
to
*printf("lower case %c\n”, c);*
*
*
Then, during symbolic execution I get the following error:
*KLEE: ERROR: (location information missing) external call with symbolic 
argument: printf*
It puzzles me as to why getchar() is not “external” but printf is ?  If I use  
putchar(c)  or puts() then klee works fine.
2) If I specify *—libc=klee * in place of *—libc=uclibc* it seems “stdin” is 
not symbolic anymore, i.e. I have to type in the input character.
Why does this happen? I guess I should assume —libc=uclibc is a requirement for 
using —sym-stdin ?
3) When —sym-sdout  is on I see that .ktest files contain a stdout variable ("object 2)", 
in a similar way to stdin ("object 0"). However they do not seem to correspond to the 
actual output.
For instance, consider this simpler program:
*#include 
int main(int argc, char** argv) {
   int c = getchar();
   if (c >= 'a' && c <= 'z')
 putchar(c);
   return 0;
}*
Three ktest files are generated containing the stdin data:
*object 0: data: b'\x00'
object 0: data: b'{'
object 0: data: b'a'*
but the stdout data is always an array with size 1024 filled with zeros. This 
should not be the case for input ‘a’, right?
Best,
Eduardo
___
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] Use of -sym-stdin/stdout

[Cristian Cadar]

Hi Eduardo,

Indeed, we need better documentation here.  But in a nutshell:

1) printf is run concretely by default (you can add -DKLEE_SYM_PRINTF 
when compiling KLEE's uclibc to change this)


2) you should only use —sym-sdout if you need to symbolically analyze 
the contents of stdout, otherwise don't set it


Best,
Cristian

On 06/02/2021 20:28, Eduardo R B Marques wrote:

Hi,

I have a few questions regarding the use of the -sym-stdin / -sym-stdout 
options. Consider the following simple program in a file named foo.c:


*#include *
*
int main(int argc, char** argv) {
   int c = getchar();
   if (c >= 'a' && c <= 'z')
     printf("lower case\n");
   else if (c >= 'A' && c <= 'Z')
     printf("upper case\n");
   else printf("Other\n");
   return 0;
}*

Using the klee 2.1  docker image I compile it as follows:

*clang -emit-llvm -std=c89 foo.c -c -o foo.bc*

then execute it using:

*klee -posix-runtime --libc=uclibc foo.bc -sym-stdin 1 -sym-stdout*

I obtain a few warnings that do not seem (at first) too relevant 
regarding the use printf (external function), but that’s all.

5 paths are explored in total.

My questions arise when I consider variations of this overall setup:

1) Suppose I change the first printf call
*  printf("lower case\n”);*
to
*printf("lower case %c\n”, c);*
*
*
Then, during symbolic execution I get the following error:

*KLEE: ERROR: (location information missing) external call with symbolic 
argument: printf*


It puzzles me as to why getchar() is not “external” but printf is ?  If 
I use  putchar(c)  or puts() then klee works fine.


2) If I specify *—libc=klee * in place of *—libc=uclibc* it seems 
“stdin” is not symbolic anymore, i.e. I have to type in the input character.
Why does this happen? I guess I should assume —libc=uclibc is a 
requirement for using —sym-stdin ?


3) When —sym-sdout  is on I see that .ktest files contain a stdout 
variable ("object 2)", in a similar way to stdin ("object 0"). However 
they do not seem to correspond to the actual output.

For instance, consider this simpler program:

*#include 
int main(int argc, char** argv) {
   int c = getchar();
   if (c >= 'a' && c <= 'z')
     putchar(c);
   return 0;
}*

Three ktest files are generated containing the stdin data:

*object 0: data: b'\x00'
object 0: data: b'{'
object 0: data: b'a'*

but the stdout data is always an array with size 1024 filled with zeros. 
This should not be the case for input ‘a’, right?


Best,
Eduardo

___
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] math.h functions interpreted as external

[Cristian Cadar]

Hi Juan,

The warnings say that no implementation for these functions is 
available.  You should compile uclibc with support for these functions.


However, note that mainline KLEE does not have support for symbolic 
floating point operations, but there are a couple of (open-source but 
unmaintained) extensions of KLEE which do:

https://srg.doc.ic.ac.uk/publications/17-klee-n-version-fp-ase.html

Best,
Cristian

On 07/01/2021 10:26, juanfrancisco.garcia wrote:

I'm getting this warnings for all math.h functions,

KLEE: WARNING ONCE: calling external: floor(9221120237041090560)
KLEE: WARNING ONCE: calling external: round(0)

math.h is included, and if I change libc to uclibc I also get this 
warnings:


KLEE: WARNING: undefined reference to function: acos
KLEE: WARNING: undefined reference to function: atan2
KLEE: WARNING: undefined reference to function: ceil
KLEE: WARNING: undefined reference to function: cos
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: round
KLEE: WARNING: undefined reference to function: sin
KLEE: WARNING: undefined reference to function: sqrt


Are math.h functions supported in klee?

I also tried with z3 solver that supports floating point, and it gives 
the same warnings.


Thanks in advance,
Juan Francisco García




___
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] Question on use-after-free detection.

[Cristian Cadar]

You are right, KLEE doesn't catch this use-after-free bug currently, as 
it doesn't implement a quarantine.  It wouldn't it be too hard to add 
this though (you might want to refer to the ASan paper for details).


Best,
Cristian

On 02/01/2021 18:16, Yoonseok Ko wrote:

Hello,

  I have an additional question on this comment: 
https://github.com/klee/klee/issues/1254 



  @ccadar mentioned that KLEE already finds the kind of bugs that 
AddressSanitizer detects, but I don't clearly understand.


  For example, consider the following code fragment:
```
  int *o1 = (int*)malloc(4);
  free(o1);
  int *o2 = (int*)malloc(4);
  *o1 = 10; /* use-after-free */
```

The code uses the memory block allocated to the object 'o1' after it is 
freed (at line 2).

ASan simply detects and reports it as 'use-after-free'.

But, KLEE does not report an alarm when the second `malloc` allocates 
the same memory block as allocated by the first `malloc`.
Since KLEE simply relies on the standard malloc semantics, the same 
memory block can be allocated.
And, when there is a memory access, KLEE only checks whether the 
dereferenced memory block is *currently* valid.

So, the last line `*o1 = 10` is valid because `o2 == o1`.

Do you support any other mechanism to catch such an issue?

Thank you.

Best regards,
Yoonseok


___
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] Postdoc and PhD positions related to KLEE at Imperial College London

[Cristian Cadar]

Hi all,

I have a couple of postdoctoral positions in my group at Imperial 
College London, at least one of which will involve KLEE:

https://srg.doc.ic.ac.uk/vacancies/postdoc-pass-21/

The application deadline is 7th January 2021.

We also have fully-funded PhD positions, for which I am of course happy 
to consider KLEE-related topics:

https://www.imperial.ac.uk/computing/prospective-students/phd/

Informal inquiries are encouraged, simply reply (but don't reply-all) to
this email.

Best,
Cristian


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

Re: [klee-dev] Bool vs i1 in STPBuilder

[Cristian Cadar]

Hi Alastair,

Our assumption is that code should not be able to construct such 
expressions in the first place and they are thus invalid at the KQuery 
level.  That expression is also invalid at the SMT level, as Concat 
should take bitvectors and not booleans as arguments.  If for some 
reason Rust code ends up generating such expressions (and the bug is not 
elsewhere), then we need to either reconsider or our assumptions and/or 
fix the expression construction.


You could try --debug-print-instructions=all:stderr to find the part of 
the code that generates this.


You could also instrument the expression creation part in Expr.h/cpp to 
find out where a Concat expression receives a comparison expression as 
one of its subexpressions.  In general, we should add extra checks 
during expression construction to catch invalid expressions early.


Best,
Cristian

On 16/12/2020 15:54, Alastair Reid wrote:
I am trying to chase down a bug that occurs while applying KLEE to a 
multi-module Rust program (assembly.ll is approx 200k lines).
I'm hoping for suggestions of what might be wrong and/or how to narrow 
down the cause of the bug.


What I am seeing in the stack trace is 
that klee::STPBuilder::constructActual calls vc_bvConcatExpr (in STP) 
which calls stp::checkChildrenAreBV which prints an error message and dies.
The error message involves a very large term but the start of it is as 
follows (I have bold-faced the top two levels of the term)


The type is: 0
Fatal Error: BVTypeCheck:ChildNodes of bitvector-terms must be
bitvectors

*14808:(BVCONCAT*
*  14806:(BVSGT*
     988:0x00
     14798:(ITE
     ))
*  14774:(BVSGT
*    988:0x00
     14766:(ITE
       14760:(EQ
         14724:(READ
           [14720]
           14386:(BVEXTRACT
             [14380]
             13594:0x001F
             60:0x))
         [14758])
       14406:0xFF
       988:0x00)))
0
error: STP Error: BVTypeCheck:ChildNodes of bitvector-terms must be
bitvectors


The first argument of BVCONCAT is the result of BVSGT and STP 
distinguishes between booleans and bitvectors.

So I think that the error is in the code in KLEE that constructed this term.

But, after that, I am not sure what is going on - here are my confused 
thoughts...


I suspect that the problem is that LLVM represents booleans as 
bitvectors of length 1.


So there must be a part of KLEE (in STPBuilder???) that is responsible 
for deciding whether a bitvector of length 1 should be represented by an 
STP bitvector or by an STP boolean?


And, I see this comment above klee::STPBuilder::constructActual 
and klee::STPBuilder::construct


      /** if *width_out!=1 then result is a bitvector,
           otherwise it is a bool */

There are two potential problems with this (but these might be 
red-herrings?)


1) The width_out pointer can be null - in which case the width is not 
written.

     And the code that converts Expr::Concat to STP passes a null pointer.
     this code (from STPBuilder.cpp) is not distinguishing booleans

571   case Expr::Concat: {
572     ConcatExpr *ce = cast(e);
573     unsigned numKids = ce->getNumKids();
574     ExprHandle res = construct(ce->getKid(numKids-1), 0);
575     for (int i=numKids-2; i>=0; i--) {
576       res = vc_bvConcatExpr(vc, construct(ce->getKid(i), 0), res);
577     }
578     *width_out = ce->getWidth();
579     return res;
580   }

2) This seems to treat all 1-bit bitvectors as booleans - is this always 
true?
      In particular, I wonder whether the Rust compiler satisfies this 
assumption?




But these could be red-herrings. The expression being converted is a bit 
unusual


       concat(sgt(_,_), sgt(_,_))

It's not impossible but it is a bit odd. So maybe something went wrong 
elsewhere in KLEE to construct this code?



Any thoughts on how to debug this or on my interpretation of the code 
above would be great!


Are there any command line flags that would generate a trace as the Expr 
is being constructed? This would let me find the part of assembly.ll 
that is triggering the problem and hopefully figure out if the problem 
is in STPBuilder or elsewhere.


Thanks,

Alastair

___
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] How to handle 32bit bc file with 64bit klee

[Cristian Cadar]

In particular, I would suggest to continue at 
https://github.com/klee/klee/issues/286


Cristian

On 15/12/2020 14:35, Nowack, Martin wrote:

Hi,
There are a couple of missing features.
Can you open an issue https://github.com/klee/klee/issues ? we can 
continue the discussion there.


Best,
Martin

On 15. Dec 2020, at 13:41, JingXiaoni > wrote:



Hi all,
l have some problems
on using klee,need your help .Thanks in advance
My test target is 32bit app.Now I compile llvm and klee in x86_64, 
then add -m32 option on compile target object.

For example:
for bc file
clang++ -m32 sample.cpp -c -o sample.bc
for app
clang++ -m32 sample.cpp -o sample -lkleeRuntest
Now I have 2 issues
1. bc file compile is success.But when I use klee to generate test 
cases.There is a error info"LLVM ERROR:64-bit code requested on a 
subtarget that doesn't support it". I would like to make klee can 
handle 32bit bc.Then add option in CMakeList.txt with 
add_complie_option(--target=i386-pc-linux-gun).remake makefile and 
make,make has a warning that "cc1 plus:warning:command line option 
'-ftarget=i386-pc-linux-gun'is valid for Java but not for c++".Add 
Klee can’t work for 32 bit bc,too.
So my question is how to add compile options in cmake or make file to 
make 64bit Klee can support 32bit bc file?
2.When I compile 32 bit app with Klee lib(libKleeRuntest),It shows 
can’t find this lib but when I compile 64bit app,there is no 
problem.Does it mean I need to compile a 32bit Klee to use it or is 
there some other way to set it up and it will work?

Thanks for your help.


___
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] Strange compilation failure on 32-bit FreeBSD

[Cristian Cadar]

Hi Gleb,

Please see the discussion at https://github.com/klee/klee/issues/1327.

In short, we're not supporting 32-bit platforms anymore, but if someone 
wants to revive support for this, we're happy to accept such a contribution.


Best,
Cristian

On 13/12/2020 19:55, Gleb Popov wrote:

Hello KLEE devs.

I stumbled upon a strange building failure when trying to compile KLEE 
on i386 FreeBSD. Here's the log:


In file included from 
/wrkdirs/usr/ports/security/klee/work/klee-2.2/lib/Core/PTree.cpp:10:
In file included from 
/wrkdirs/usr/ports/security/klee/work/klee-2.2/lib/Core/PTree.h:15:
/usr/local/llvm90/include/llvm/ADT/PointerIntPair.h:147:3: error: 
static_assert failed due to requirement '3U <= 
PointerLikeTypeTraits::NumLowBitsAvailable' 
"PointerIntPair with integer size too large for pointer"

  static_assert(IntBits <= PtrTraits::NumLowBitsAvailable,
  ^ ~
/usr/local/llvm90/include/llvm/ADT/PointerIntPair.h:71:13: note: in 
instantiation of template class 
'llvm::PointerIntPairInfollvm::PointerLikeTypeTraits >' requested here

    Value = Info::updatePointer(0, PtrVal);
    ^
/usr/local/llvm90/include/llvm/ADT/PointerIntPair.h:56:47: note: in 
instantiation of member function 'llvm::PointerIntPair*, 3, unsigned char, llvm::PointerLikeTypeTraits, 
llvm::PointerIntPairInfoointerLikeTypeTraits > >::initWithPointer' requested 
here

  explicit PointerIntPair(PointerTy PtrVal) { initWithPointer(PtrVal); }
  ^
/wrkdirs/usr/ports/security/klee/work/klee-2.2/lib/Core/PTree.cpp:35:12: 
note: in instantiation of member function 
'llvm::PointerIntPairllvm::PointerLikeTypeTraits, 
llvm::PointerIntPairInfo*, 3, llvm::PointerLikeTypeTraits > 
 >::PointerIntPair' requested here

    : root(PTreeNodePtr(new PTreeNode(nullptr, initialState))) {
   ^

Any ideas what might be wrong here?

Thanks in advance.

___
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] KLEE 2.2 released

[Cristian Cadar]

Dear all,

KLEE 2.2 is now released, many thanks for all the great contributions!

And extra thanks to my co-maintainer @MartinNowack and to the authors of 
key improvements this release: @corrodedHash, @futile, @jbuening, @251, 
@kren1, @MartinNowack.


The full list of changes can be found at
https://github.com/klee/klee/releases/tag/v2.2

Best,
Cristian

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

Re: [klee-dev] [KLEE] write to a symbolic address & constraints for write

[Cristian Cadar]

Hi Mingyi, it's unclear to me what you are running exactly.  In general, 
it's good to include a complete program and the exact commands you ran.


Best wishes,
Cristian

On 20/11/2020 02:58, Liu, Mingyi wrote:

Hi klee-dev members,

I made args symbolic and provided a seed ktest file for the following 
target (code snippets):


if(*(u64*)args >= 0x327b2000&& *(u64*)args <= 0x643c9000) {

printf("WRITE\n");
   *(u64*)*(u64*)args = 4;

printf("val1 = %llx\n", *(u64*)args);
printf("point_to1 = %p\n", *(u64*)*(u64*)args);

}

when running the compiled target with that seed ktest file, I got the 
following:


WRITE
val1 = 327b2000
point_to1 = 0x4

But, when running the target under KLEE with the seed option, I got the 
following:


WRITE

val1 = 327b2000

Given that 0x327b2000 is a valid address, why was the last line failed? 
Does that mean we cannot write to a symbolic address?


Another question is that, I made a, b and c symbolic for the following 
target, and run it under KLEE with seed(a=2, b=3) option:


printf("a=%d\nb=%d\nc=%d\n", a, b, c);

if(a > 0&& a < 100&& b > 0&& b < 100) {
sprintf((char*)buf, "%*d%*d%n\n", a, 0, b, 0, );
}

printf("c=%d\n", c);

It was executed successfully (because  is not symbolic?) and had the 
following output:


a=0

b=0

c=0

c=5

Then I checked the kquery file, the constraints for a (=2) and b (=3) 
could be identified easily by:


(Eq false (Sle N0 1))
(Eq false
          (Ult 0
                   (Add w64 18446744073709551615
                            (SExt w64 (Add w32 4294967295 N0)
(Eq false (Sle N1 1))
(Ult 0
  (Add w64 18446744073709551615
                        N2:(SExt w64 (Add w32 4294967295 N1
(Eq false
          (Ult 0 (Add w64 18446744073709551614 N2)))]

But there are no constraints for "write" or "store" the value 5. It's 
known that the KQuery language supports "read" expressions such as Read 
and ReadLSB, I am wondering does it have "write" or "store" expressions? 
If not, why "write" or "store" are not that necessary?



Thanks in advance, your help will be much appreciated!


Best,

Mingyi Liu


___
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] How to make assumption on symbolic stdin in klee

[Cristian Cadar]

Hi Pushi, to do this, you will need to modify the code in runtime/POSIX.

Best,
Cristian

On 16/11/2020 12:34, Pushi Zhang wrote:

Hi all,

       As in the documentation of klee, we can use command "-sym-stdin" 
to make inputs symbolic.


       Here my question is: how can we make assumptions to the symbolic 
stdin, like in klee_assume?


Best,
Pushi

___
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] KLEE floating-point support

[Cristian Cadar]

Hi Aleksei,

From what I understand, you managed to rebase the KLEE-Float extension 
on top of KLEE's mainline.  That's great!


As I mentioned on GitHub, my main concern is that KLEE-Float changes the 
expression representation, which has a significant impact on the core of 
KLEE.  The question is whether it is possible to integrate the changes 
in such a way that the core of KLEE is minimally affected.  This would 
require incremental changes and careful measurements.


I am also considering right now experimenting with supporting FP 
programs via fixed-point arithmetic, see the last project at 
https://klee.github.io/projects/.


My proposal would be to first submit your changes to the KLEE-Float 
project at https://github.com/srg-imperial/klee-float.  There is still 
interest in that extension, but it's starting to show its age, as you 
can see in the open issues.  In fact, even the Docker container is 
difficult to run these days, as Arch Linux changed its packaging format 
in the meantime.


Best,
Cristian

On 22/11/2020 21:08, Aleksei Pleshakov wrote:
I currently have the https://github.com/srg-imperial/klee-float 
patch along with some FP intrinsics 
supported here: https://github.com/qrort/klee 
. You have mentioned that you'd be happy 
to discuss the possibilities of this to be merged in mainline KLEE in 
this issue . I am 
willing to take the work that needs to be done. Can we discuss it? :)


___
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] Retrieve concrete values of variables from an execution path

[Cristian Cadar]

Hi Seemanta,

Since you didn't include a full program, it's not clear what you want to 
do exactly.  But at a higher level, note that KLEE is not a concolic 
execution engine, although it has some concolic execution features. 
However, it uses a counterexample cache, so you could adapt the code 
from there to retrieve concrete values.


Best,
Cristian

On 03/11/2020 16:29, Seemanta Saha wrote:

Hello,

Need help to retrieve concrete values of variables from an execution path.

I can retrieve information like path constraint, number of instructions 
stepped for a symbolic path using the ExecutionState class. Is it 
possible to retrieve concrete values of variables of an execution state 
using the ExecutionState class?


For example, Consider this following program:

int base = 8;

int checked_copy (unsigned int i ) {

int v;

if ( i < 16)

v = base + i ;

else

v = base;

return v;

}

If I execute this program symbolically, I am going to get 17 path 
constraints but 16 distinct values for v (8 to 23). When symbolically 
executing, value of v will be represented as a symbolic expression and 
all I can retrieve is the path constraint. But, I want to retrieve the 
concrete values for v for each execution path. How can I do that?


Regards

Seemanta



--
Regards
Seemanta Saha
Verification Lab (V-Lab)
University of California Santa Barbara

___
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] KLEE Open Projects list

[Cristian Cadar]

Hi all,

I have updated the list of KLEE Open Projects at 
https://klee.github.io/projects/


In particular -- and as also advertised on Twitter -- we are looking for 
package maintainers for Ubuntu and other popular distributions (thanks 
to Gleb Popov for maintaining KLEE's package on FreeBSD) and also for 
active maintainers and developers for KLEE Web 
(http://klee.doc.ic.ac.uk/, https://github.com/klee/klee-web).


Let me know if you're interested in any of the projects listed there.

Best,
Cristian

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

[klee-dev] KLEE: external tutorials, blog posts & more

[Cristian Cadar]

Hi all,

I've just added to the KLEE website a list of external tutorials, blog 
posts and other external resources on KLEE.  In particular, I added a 
link David Korczynski's video tutorials on KLEE; Dennis Yurichev's 
"SAT/SMT by Example" book; Alastair Reid's project on checking Rust code 
(thanks Alastair for sharing the info with the list); and a recent blog 
post from Timotej Kapus and me on measuring coverage in symbolic 
execution (alongside other external resources that were already there).


Please check https://klee.github.io/tutorials/ for the full list.

If you are aware of other good resources on KLEE, please let me know (or 
simply contribute a PR at https://github.com/klee/klee.github.io/pulls).


On a related note, please also consider contributing to the list of 
publications (and associated systems) that report on using/extending 
KLEE: https://klee.github.io/publications/.  The list has now over 160 
interesting publications; big thanks to Frank Busse, who is currently 
maintaining it.


Best wishes,
Cristian

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

Re: [klee-dev] Crosschecking core solvers and printing the query causing the mismatch

[Cristian Cadar]

Hi, I think what you want is --debug-crosscheck-core-solver.

Best,
Cristian

On 16/09/2020 18:54, Shuo Ding wrote:

Hi All,

My goal is to compare the outputs of two core solvers (e.g. Z3 and STP) 
and get the query issued to those core solvers causing the mismatch. 
However, it seems that the -debug-validate-solver option does something 
slightly different from what I need.


By looking at the code in ConstructSolverChain.cpp 
(https://github.com/klee/klee/blob/v2.1/lib/Solver/ConstructSolverChain.cpp) 
of version 2.1, it seems that this implementation compares:


(1) the output of the whole solver chain with the output of the oracle 
solver (line 72), and


(2) the output of almost the whole solver chain with the output of the 
solver chain's core solver (line 58).


However, I want to compare two core solvers, and get the query issued to 
them causing the mismatch.


I guess I can just reorder those solvers to realize that (using 
--log-partial-queries-early=true to ensure that the mismatched query can 
be logged). However, I cannot test whether this solution works until I 
actually find a mismatch. Could someone confirm this or give me some 
suggestions?


Also, I'm assuming that the debug validating solver will terminate KLEE 
when it sees a mismatch, as I can see there are some assertions in the 
implementation of the debug validating solver. Is this correct?


Thanks!

Sincerely,
Shuo


___
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] About klee's detection problems in real software

[Cristian Cadar]

Hi,

Yes, you need to compile the system under test to LLVM bitcode. 
However, nowadays things are much easier with the use of wllvm, as 
illustrated in that tutorial.


Regarding the error you mentioned, just look in the .external.err file, 
it should contain an explanation about the issue.


Best,
Cristian

On 15/09/2020 04:30, rongze xv wrote:

Hi all，

I am a graduate student, my name is Xu Rongze. I recently read your 
paper "KLEE: Unassisted and Automatic Generation of High-Coverage Tests 
for Complex Systems Programs",  and learn how to use KLEE. I saw the 
tutorial on the official website: "Testing Coreutils" clearly stated 
"One of the difficult parts of testing real software using KLEE is that 
it must be first compiled so that the final program is an LLVM bitcode 
file and not a native binary. " I think this means that when I use KLEE 
to test real software, I need to build the environment for each real 
software?  If I test a function level code in a project, do I need to 
write the corresponding driver, or do I need to write only one driver 
for a project?


When I tested in coreutils, I tested the echo.bc file separately 
according to the tutorial and there was no problem, but I tested other 
files separately, such as tr.bc, and an error (external.err) occurred. I 
don't know the reason. Is it related to the driver?


If you can reply to me in your spare time, thank you very much!!

Sincerely，
Xu Rongze

___
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] Dealing with missing intrinsics (Rust support)

[Cristian Cadar]

+1 to this, we should only terminate those paths that hit unhandled 
intrinsics.  This is what we do with unavailable external functions and 
inline assembly for instance, so we should adopt the same behaviour here.


Best,
Cristian

On 14/08/2020 18:06, Nowack, Martin wrote:

Hi Alastair,

I would also rather use option 3.
Normally, the `LowerIntrinsic` pass should try to replace appropriate 
calls if possible. It should not terminate it.


Beside your attached code, I would suggest to change the following code 
line in `lib/Core/Executor.cpp`:

https://github.com/klee/klee/blob/088fc21e12c9675161172899be5ef5051f1ae96b/lib/Core/Executor.cpp#L1514

Instead of an `klee_error` which terminates the whole KLEE execution, 
one could terminate the current path.
This allows to explore other paths that don’t contain such instructions 
or at least explore a path until it reaches such instruction, which I 
guess might be valuable in itself.



As you mentioned inline assembly, there is a currently a pass which 
tries to lift mostly memory barriers into LLVM intrinsics that are 
handles as NOPs. More complex things are hard to handle.

(https://github.com/klee/klee/blob/088fc21e12c9675161172899be5ef5051f1ae96b/lib/Module/RaiseAsm.cpp)

Hope that helps.

Best,
Martin

On 14. Aug 2020, at 17:33, Alastair Reid > wrote:


Hi,


I want to check what the best way is to deal with missing intrinsics 
when adapting KLEE for a new language and new standard libraries.

In particular, what kind of changes should I make and submit as PRs?

I am trying to use KLEE with a modest sized Rust application (about 
20kloc) but that depends on over 100 other libraries ("crates") and 
Rust's fairly rich standard library.
Given the amount of code involved, it is unsurprising that the 
resulting LLVM bitcode files use some intrinsics that KLEE does not 
support.
I don't know whether I have a complete list but at least the following 
are needed:


    maxnum               minnum
    x86_avx2_pshuf_b     x86_ssse3_pshuf_b_128
    x86_avx2_pslli_d     x86_avx2_psrli_d
    x86_avx_ldu_dq_256   x86_sse3_ldu_dq
    x86_sse2_pslli_d     x86_sse2_psrli_d
    x86_sse2_pause
    x86_avx_vzeroupper

As far as I can tell, KLEE checks that it accepts all intrinsics 
before starting symbolic execution.
So it can reject a program even if there is no feasible path these 
intrinsics just because they are in the bitcode file.
I have seen this happen in my current trials (on short test programs 
that only use the standard library).



I see three solutions - with various pros/cons

1) Implement all missing intrinsics.
    This seems like a good option for target independent intrinsics 
like maxnum (IEEE float min/max)
    And it might be necessary for x86_sse2_pause because LLVM will 
emit this instruction even if you disable SSE2 (this instruction is a 
NOP on old x86 cores - it makes spinlocks faster on modern cores).


    The disadvantage is that implementing all LLVM intrinsics is a 
Sisyphean task.
    (I have not even explored what intrinsics are required on Arm - 
which is a much more

    widespread ISA than x86!)

2) Compile the libraries with AVX and SSE features disabled.
    This should fix most of the intrinsics (except for 
maxnum/minnum/x86_sse2_pause).


    The disadvantage of messing with compilation options is that this 
becomes quite hard

     to do in large, complex projects.

3) Change KLEE to ignore any missing intrinsics unless it actually 
executes them.
    This would make option 1 less painful because I would only need to 
implement

    intrinsics that are truly needed.

    I have a change that would do this - but I don't think it is ready 
to submit as a PR yet.

    (diff attached at end).

    (Using this change, I got a bit further with the application - I 
was able to start running
    the code in KLEE but it then got stuck because one of the 
libraries contains a mix of

    Rust, C and assembly code. But that's a problem for next week...)

I am currently leaning towards option 3 but I want to check which is 
preferred and there are a few possible variants (sketched at the end)


--
Alastair Reid

ps Here is the change. It ignores all intrinsics on the above list 
during the Cleaner pass (but still reports an error if it hits them 
during execution).


The main goal of this code is to avoid calling 
"IL->LowerIntrinsicCall(ii);" in the default case because that LLVM 
function fails an assertion if it cannot lower the call.
(The function is defined in LLVM in 
llvm/lib/CodeGen/IntrinsicLowering.cpp)


Some things that I am unsure about are:
- I am a bit uneasy about hardcoding the list of intrinsics to ignore.
- Is there a need for a command line option to enable/disable ignoring 
unknown intrinsics.


diff --git a/lib/Module/IntrinsicCleaner.cpp 
b/lib/Module/IntrinsicCleaner.cpp

index a1d4fdda..e88d5300 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ 

Re: [klee-dev] Klee & pointers

[Cristian Cadar]

Hi Igor,

For this example, I don't think it makes sense to make the pointer 
itself symbolic.  You could instead replace the klee_make_symbolic call 
with klee_make_symbolic(a, sizeof(*a), "a"); to make the malloc'ed 
memory symbolic.


If you're interested in symbolic pointers more generally, I would 
recommend this paper, which contains in the beginning a discussion of 
the different memory models used in symbolic execution (as well as 
proposing a new model):

https://srg.doc.ic.ac.uk/publications/19-segmem-esecfse.html

Best,
Cristian

On 09/08/2020 14:45, Breger, Igor (Mobileye) wrote:

Hi all,

I am trying to generate function coverage tests.  From the tutorial and 
mail-archive I could not understand how I can define  pointer as 
symbolic and also the data it point to.


In the follow example, if I make a pointer symbolic, most of the tests 
KLEE generate are invalid ( 6 of 7 ) . The only valid test is with NULL 
values.


I would appreciate any help.

Best Regards,

Igor

#include "klee/klee.h"

#include 

int get_sign(int *a) {

   if ( a == NULL)

     return 2;

   int x = *a;

   if (x == 0)

     return 0;

   if (x < 0)

     return -1;

   else

 return 1;

}

int main() {

   int *a = (int*)malloc(sizeof(int));

   klee_make_symbolic(, sizeof(a), "a");

   return get_sign(a);

}

-
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.


___
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] Dummy pthread library?

[Cristian Cadar]

Hi again Alastair,

I'm not aware of anything like this, but it would be a nice extension of 
KLEE's POSIX environment.


Best,
Cristian

On 30/07/2020 17:37, Alastair Reid wrote:
Is there a dummy pthread library that I can use with single-threaded 
programs that only use a single thread but are linked against 
thread-safe libraries (i.e., threads that call pthread_* functions).


I am 99.9% sure that I don't need any actual thread support - just an 
implementation that pretends to support a single thread.
I'm guessing that a dummy library would mostly consist of a bunch of 
functions that return constant values because there is only one thread, 
no lock contention, etc.

And I'm also guessing that somebody has already implemented such a library.

--
Alastair Reid

ps The functions that I need (as reported when I run KLEE) are:

   pthread_attr_destroy
   pthread_attr_getstack
   pthread_attr_init
   pthread_cond_destroy
   pthread_cond_init
   pthread_cond_signal
   pthread_cond_wait
   pthread_condattr_destroy
   pthread_condattr_init
   pthread_condattr_setclock
   pthread_getattr_np
   pthread_getspecific
   pthread_key_create
   pthread_key_delete
   pthread_mutex_destroy
   pthread_mutex_init
   pthread_mutex_lock
   pthread_mutex_unlock
   pthread_mutexattr_destroy
   pthread_mutexattr_init
   pthread_mutexattr_settype
   pthread_rwlock_rdlock
   pthread_rwlock_unlock
   pthread_rwlock_wrlock
   pthread_self
   pthread_setspecific

___
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] Distinguishing klee from runtest

[Cristian Cadar]

Hi Alastair,

Unless I'm misremembering things, we've never added anything like this, 
but this is the right approach, and I'd be happy to accept such a PR.  I 
think the right way to do this would be to have this as an intrinsic 
defined in both runtime/Intrinsic and runtime/Runtest.


Best,
Cristian

On 30/07/2020 16:45, Alastair Reid wrote:
Is there a function that I can use in a program to distinguish between 
running under KLEE and replaying a ktest using libkleeRuntest?


The reason that I want this is so that my test harness can print 
symbolic values when replaying with concrete values but does not do so 
when running under KLEE.

This is especially useful when generating structured symbolic values.
In particular, when using KLEE with Rust, it is much, much better to use 
the std::fmt::Debug api to print structure values like Vectors, 
BinaryHeaps, BTreeMap, etc. than to run ktest-tool to see the raw 
symbolic values that were used to construct the object.


If there is not a standard way of doing this, I propose to submit a PR 
that adds the following function to klee.h (with two alternative 
implementations).


     int klee_is_replay();
     // return 1 if replaying under libkleeRuntest
     // return 0 if executing symbolically under KLEE

Suggestions for different name, etc. welcome.

--
Alastair


___
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] Checking Tool Equivalence

[Cristian Cadar]

Hi Linda,

I cannot find that infrastructure anymore, but as explained in the 
paper, the idea was to rename global symbols and link the two tools 
together, accompanied by a new main function that looks similar in 
spirit to the one in Figure 11.  The only tricky part is to capture and 
compare the stdout, for which we used the --sym-stdout option of the 
POSIX runtime.


Hope this helps,
Cristian

On 29/07/2020 07:15, Linda Dart wrote:

Hello,

The OSDI 2008 paper mentions that Klee was used for checking tool 
equivalence, which took two tools and asserted that they were equal. A 
"simple infrastructure" was built to automate crosschecking of two 
tools. I was wondering if you could provide more insight on how to 
implement this infrastructure?


Thanks,
Linda

___
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] Dbg Location

[Cristian Cadar]

KLEE performs various transformations & optimizations on the input 
bitcode file, which is why you see those differences.


Best,
Cristian

On 23/07/2020 09:55, Yugesh Kothari wrote:

Hi,

I had a question about the dbg location as seem in the assembly.ll file 
generated by Klee.
I assume that Klee operates on this assembly.ll file (so please correct 
me if wrong).


I was comparing the dbg location information printed in assembly.ll and 
the .ll file generated by running llvm-dis input.bc and found them to be 
different. I was wondering why this is the case?


Thanks!

___
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] code style for easy, efficient symbolic execution

[Cristian Cadar]

Hi Laszlo,

There is no optimal code style for symbolic execution, although 
sometimes the style can significantly influence performance.  There is 
some research on these topics (e.g., estimating constraint solving 
performance, understanding the impact of program transformations in 
symbolic execution), but it is still far away from the kind of cost 
model you are looking for.


Best,
Cristian

On 02/07/2020 18:27, Nemeth, Laszlo wrote:

Hi,

I’m using klee to check various properties of models. When generating 
the C representation I have two options:


 1. A bunch of global declarations. This is the current approach, and
pretty easy to generate.
 2. A more object-oriented way: state is local to components and
components communicate via messages (function calls with parameters).

The models are large, my generated files are 10-15k lines. And running 
them takes about four weeks on the hardware available to me, which isn’t 
really acceptable. I’ve already run test to determine if the number of 
symbolic variables or the size of those domains are the problem. When 
the domains are constrained (klee_range(0, 2) instead of klee_range(0, 
65535)), there is a speedup but negligible. I have models with a few 
hundred symbolic variables.


Question to someone knowledgeable about klee’s internals: which 
representation would be easier (resulting in faster execution) for klee 
to process?


Or in more general terms, does klee have some sort of a cost semantics? 
Should I generate loops or recursion? As far as I can tell, aggressive 
compiler optimizations are switched off in the Makefile for clang, is it 
worth trying to generate inlineable code, ie a trade-off between 
function calls and code size?


Insights, pointers to papers are much appreciated.

Thanks,

   Laszlo


___
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] Executing Concretely inside a certain function

[Cristian Cadar]

Hi,

There is no direct way to do this, in the sense that KLEE doesn't have 
such an option.  One possibility would be to concretize the arguments to 
the function using calls to klee_get_value_*.  This is particularly easy 
if the arguments have primitive types.


Best,
Cristian

On 17/06/2020 13:43, Hooman wrote:

Dear all,

I was wondering if there is a simple way to make KLEE execute a function 
concretely. Here's the situation:


I am calling a function which causes state explosion. I want KLEE not to 
fork inside that function(some parameters to the function are symbolic). 
Is there any simple way to do that. Thanks in advance.



Best,

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

Re: [klee-dev] Error while using C++ STL, libcxx

[Cristian Cadar]

On 26/05/2020 13:32, Namrata Jain wrote:
I also want to know about klee version-2.1-pre, is it the same as 
version 2.0? This is because I have made some changes in my klee source 
(2.1-pre) for a project and now I will be using version-2.1.
2.1-pre is the version string reported by the mainline between releases 
2.0 and 2.1.


Cristian

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

Re: [klee-dev] ERROR 21: Can not open input file: .adl**

[Cristian Cadar]

The POSIX runtime model creates file names 'A', 'B', 'C', etc.  You can 
easily extend the model to support other file names, but this is not 
part of the mainline.


You can read more about --sym-files in this tutorial: 
https://klee.github.io/tutorials/using-symbolic/


Cristian

On 28/05/2020 18:33, Nani Hutagaol wrote:

Hi all,

I'm try to run a program that have to read a file. On the readfile 
function, there's a piece of code like this,,


strcpy(adlfilename, filename);
strcat(adlfilename, ".adl");
if ((f = fopen(adlfilename, "r")) == NULL) {
printf("%s %s", ErrorMessages[21], adlfilename);
return 21;
};


On shortf explanation, it need an input file with type is .adl,

On my execution, I run with command:
klee --only-output-states-covering-new --optimize --libc=uclibc 
  --max-time=60s --posix-runtime ./program.bc  --sym-args 0 1 2 
--sym-files 1 10 --sym-stdin 10 --sym-stdout,


It just need around 2 seconds to stop the execution, because it end with 
error like this,


ERROR 21: Can not open input file: .adl** ERROR 21: Can not open input 
file: /.adl** ERROR 21: Can not open input file: .adl** ERROR 21: Can 
not open input file: //.adl** ERROR 21: Can not open input file: / 
.adl** ERROR 21: Can not open input file: /.adl** ERROR 21: Can not open 
input file: .adl** ERROR 21: Can not open input file: / .adl** ERROR 21: 
Can not open input file: .adl** ERROR 21: Can not open input file: 
///.adl** ERROR 21: Can not open input file: / /.adl** ERROR 21: Can not 
open input file: // .adl**


I'm so very confused about that, because I can't move to the next process,
Btw isn't --sym-files option aims to form symbolic file to be used as 
input file into the program? So, why it return error can't open input 
file although I use this option?


--
Warm Regards
_Nani Renova Hutagaol_

___
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] Why KLEE still symbolic executing program after reaching max-fork?

[Cristian Cadar]

Hi,

This was the simplest way to implement --max-forks.  I agree you could 
improve this, depending also on what you want to achieve.


Best,
Cristian

On 25/05/2020 10:31, XIE Xuan wrote:

Hi all,

I am reading KLEE’s source code and find that if I set “-max-fork=n” 
when KLEE reach its fork limit n, it will still symbolic executing the 
program. In my understanding, when KLEE stops forking, there is no need 
to invoke SMT solver to check which branch is reachable or not, 
therefore it is also unnecessary to symbolic executing the program in 
order to set up more constraints. Thus I would like to know why KLEE not 
concretely running the program after reaching fork limit?


Thanks!


___
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] KLEE workshop deadline extended to Tuesday

[Cristian Cadar]

Dear all,

Based on some requests, we are extending the deadline for sending 
presentation proposals to the KLEE workshop to Tuesday, 12 May:


https://srg.doc.ic.ac.uk/klee20/cfpresentations.html

Best,
Cristian

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

Re: [klee-dev] 2nd International KLEE Workshop on Symbolic Execution

[Cristian Cadar]

Dear all,

I am writing to remind you of the deadline for submitting a presentation 
proposal to the upcoming KLEE workshop: Friday, 8 May.


I realize now that things are quite uncertain due to the COVID-19 
situation.  Therefore, we have also reserved 22-23 April 2021 as 
alternative dates if we need to postpone the workshop, and added a 
question about your availability on EasyChair (don't worry if you have 
already submitted, we will contact you separately later on).  But it 
would still be helpful to get your submissions now, to get a better feel 
for your interest and preferences in the workshop.


Best,
Cristian

On 19/02/2020 14:58, Cadar, Cristian wrote:

Dear all,

I am excited to announce the 2nd International KLEE Workshop on Symbolic
Execution, which will take place on 14-15 September 2020 at Imperial
College London:
https://srg.doc.ic.ac.uk/klee20/

The goal of the workshop is to bring together symbolic execution
researchers, KLEE users and KLEE developers to exchange ideas, find out
about new research in the field, understand each other’s interests and
needs, discuss the evolution of KLEE, and more.

The first edition of the workshop (https://srg.doc.ic.ac.uk/klee18/) was
really great, with a fantastic set of presentations from both academia
and industry and excellent discussions on KLEE, symbolic execution and
related topics.

I hope you'll make the second edition of the workshop equally successful
by responding to the call for presentations, with a deadline of 8 May:
https://srg.doc.ic.ac.uk/klee20/cfpresentations.html

We will also be making regular announcements about the workshop via
@kleesymex on Twitter (the tweets are also available on the workshop
webpage).

Finally, but importantly to keep registration costs low, if your company
would like to sponsor the workshop, please get in touch!

Best,
Cristian and the KLEE 2020 Organising Team
___
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] Type of bugs that KLEE can find

[Cristian Cadar]

Hi,

The kind of bugs KLEE can find are memory errors (buffer overflows, null 
pointer dereference, etc.),  division/modulo by zero, overshifts, and 
assertion violations.  If I forgot anything, others should feel free to 
add to this list.  KLEE does not report memory leaks, but it could be 
extended to do so.


We should indeed document this better, so if anyone would like to add a 
complete list to the website, that would be great.


Best,
Cristian

On 17/04/2020 11:05, XIE Xuan wrote:

Dear all,

I would like to ask what types of bugs can KLEE find?  I only find a 
simple introduction about the error KLEE report here: 
http://klee.github.io/tutorials/testing-regex/


Do you have detailed documentation?

What’s more, is KLEE able to discover memory leak, i.e. forget to free() 
after malloc()? From the introduction above, it seems that KLEE is not 
able to find it.


Thanks!


___
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] KLEE Slow execution while executing natively

[Cristian Cadar]

Improving the interpretation speed of KLEE is on our todo list.  But 
KLEE's speed should be comparable to that of lli in interpreter mode 
(lli --force-interpreter=true).  If you have examples where it's slower, 
I'd be curious to take a look, please open an issue on GitHub.


Best,
Cristian

On 14/04/2020 09:50, Hooman wrote:

Dear all,

I am trying to execute part of a program symbolically. before using 
klee_make_symbolic() function, I have some functions which are supposed 
to be executed natively because I have not made anything symbolic yet. 
However, this part is executed really slowly. When I execute this part 
with llvm interpreter, It is executed much faster. I would appreciate 
any kind of help.



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

Re: [klee-dev] KLEE aborts with tcmalloc error

[Cristian Cadar]

As you can see from the log ("LLVM ERROR: out of memory") the run 
exhausted all available memory.  This is not that surprising for a 36h 
run.  When you enable query logging, memory consumption increases 
further, as the textual representation of the queries can become massive 
after a long run.


Best,
Cristian

On 16/04/2020 09:31, Hooman wrote:

Dear all,

I run klee with following options:

klee --simplify-sym-indices --write-cvcs --write-cov --output-module 
--disable-inlining --optimize --use-forked-solver --use-cex-cache 
--libc=uclibc --posix-runtime --external-calls=all 
--only-output-states-covering-new --max-memory-inhibit=false 
--max-static-fork-pct=1 --max-static-solve-pct=1 
--max-static-cpfork-pct=1 --switch-type=internal --search=random-path 
--search=nurs:covnew --max-memory=16000 --max-sym-array-size=4096 
-use-query-log=solver:smt2 -log-timed-out-queries 
-min-query-time-to-log=20 --max-solver-time=20


after like 36 hours of running I get the attached results and klee 
aborts. The interesting fact is that when I run the same experiment 
without -use-query-log=solver:smt2 -log-timed-out-queries 
-min-query-time-to-log=20 options, the experiment finishes. I would 
appreciate any help.



Kind regards,

Hooman


Attached error upon abortion:

tcmalloc: large alloc 1330126848 bytes == 0x55d304afc000 @ 
0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 
0x7fcd37542edf 0x55cef2d2c686 0x55cef2d32cc7 0x55cef2d33c12 
0x55cef2d34038 0x55cef2d334f8 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
tcmalloc: large alloc 2660245504 bytes == 0x55d353f7e000 @ 
0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 
0x7fcd37542edf 0x55cef2d35438 0x55cef2d33dde 0x55cef2d34038 
0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d356b0 
0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 
0x55cef2d34038 0x55cef2d3676e 0x55cef2d33d3d 0x55cef2d34038 
0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d356b0 
0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 
0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d
tcmalloc: large alloc 5320482816 bytes == 0x55d3f308 @ 
0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 
0x7fcd37542edf 0x55cef2d2c686 0x55cef2d32dbd 0x55cef2d33c12 
0x55cef2d34038 0x55cef2d334f8 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
tcmalloc: large alloc 10640957440 bytes == 0x55d530282000 @ 
0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 
0x7fcd37542edf 0x55cef2d34478 0x55cef2d33e6d 0x55cef2d34038 
0x55cef2d356b0 0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 
0x55cef2d33e6d 0x55cef2d34038 0x55cef2d3676e 0x55cef2d33d3d 
0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 
0x55cef2d356b0 0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 
0x55cef2d33e6d 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 
0x55cef2d34038 0x55cef2d35111 0x55cef2d33d8b
tcmalloc: large alloc 21281906688 bytes == (nil) @  0x7fcd3a5bff2d 
0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 0x7fcd37542edf 
0x55cef2d33460 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 
0x55cef2d334ca 0x55cef2d334ca

LLVM ERROR: out of memory
LLVMSymbolizer: error reading file: No such file or directory
#0 0x7fcd3755ec2f llvm::sys::PrintStackTrace(llvm::raw_ostream&) 
(/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cec2f)
#1 0x7fcd3755d132 llvm::sys::RunSignalHandlers() 
(/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cd132)

#2 0x7fcd3755ef42 (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cef42)
#3 0x7fcd366cf840 (/lib/x86_64-linux-gnu/libc.so.6+0x37840)
#4 0x7fcd366cf7bb gsignal (/lib/x86_64-linux-gnu/libc.so.6+0x377bb)
#5 0x7fcd366ba535 abort (/lib/x86_64-linux-gnu/libc.so.6+0x22535)
#6 0x7fcd374f8e13 llvm::report_bad_alloc_error(char const*, bool) 
(/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x968e13)

#7 0x7fcd374f8e92 (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x968e92)
#8 0x7fcd3a5bf748 _init 
(/usr/lib/x86_64-linux-gnu/libtcmalloc.so.4+0x17748)
#9 0x7fcd3a5dfef5 tcmalloc::allocate_full_cpp_throw_oom(unsigned 
long) (/usr/lib/x86_64-linux-gnu/libtcmalloc.so.4+0x37ef5)
#10 0x7fcd36b25eeb std::__cxx11::basic_stringstd::char_traits, std::allocator 

Re: [klee-dev] Timed-out solver queries

[Cristian Cadar]

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

Re: [klee-dev] KLEE finishes fast

[Cristian Cadar]

Hi,

Without including the program, it's not clear whether KLEE should have 
run for longer.  One relevant thing one can tell from the log is that 
KLEE concretized a symbolic object size.


Best,
Cristian

On 24/03/2020 09:45, XIE Xuan wrote:

Dear KLEE,

I am running KLEE on a fuzzing dirver. But KLEE finish in a few seconds. 
And it generates warning shown below. I don’t know whether it is because 
of the missing of math function (but those are floating math function, 
which is not supported by KLEE anyway). Do you have any idea of how to 
debug it? I am happy to provide more information if needed!


```

KLEE: NOTE: Using POSIX model: 
/root/trial/klee/build/Debug+Asserts/lib/libkleeRuntimePOSIX.bca


KLEE: NOTE: Using klee-uclibc : 
/root/trial/klee/build/Debug+Asserts/lib/klee-uclibc.bca


KLEE: output directory is "/root/tmp/ "

KLEE: Using STP solver backend

WARNING: this target does not support the llvm.stacksave intrinsic.

KLEE: WARNING: undefined reference to function: __fpclassifyf

KLEE: WARNING: undefined reference to function: __isinf

KLEE: WARNING: undefined reference to function: __isnanf

KLEE: WARNING: undefined reference to function: atan2

KLEE: WARNING: undefined reference to function: ceil

KLEE: WARNING: undefined reference to function: cos

KLEE: WARNING: undefined reference to function: exp

KLEE: WARNING: undefined reference to function: floor

KLEE: WARNING: undefined reference to function: floorf

KLEE: WARNING: undefined reference to function: llvm.fabs.f32

KLEE: WARNING: undefined reference to function: llvm.fabs.f64

KLEE: WARNING: undefined reference to function: log

KLEE: WARNING: undefined reference to function: log10

KLEE: WARNING: undefined reference to function: pow

KLEE: WARNING: undefined reference to function: sin

KLEE: WARNING: undefined reference to function: sqrt

KLEE: WARNING: undefined reference to function: sqrtf

KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 
93958238439968) at /root/trial/klee/runtime/POSIX/fd.c:990 10


KLEE: WARNING ONCE: calling __user_main with extra arguments.

KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not 
modelled. Using alignment of 8.


KLEE: WARNING ONCE: calling external: gettimeofday(93958238379168, 0) at 
/root/trial/klee/runtime/POSIX/stubs.c:174 7


KLEE: ERROR: cmserr.c:97: 0.486355: concretized symbolic size

KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 90013

KLEE: done: completed paths = 3

KLEE: done: generated tests = 3

```

Best Regards,

Xuan XIE


___
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] Postdoctoral and PhD positions at Imperial College London related to KLEE

[Cristian Cadar]

Hi all,

I have again both postdoctoral and PhD positions in my group at Imperial 
College London to  work on topics involving KLEE (as well as other 
topics).  You can find more details at:

https://srg.doc.ic.ac.uk/vacancies/postdoc-pass-20/
https://srg.doc.ic.ac.uk/vacancies/phd-pass-20/

The application deadline is 3rd May 2020.

Informal inquiries are encouraged, simply reply (but don't reply-all) to
this email.

Best,
Cristian

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

Re: [klee-dev] Status of KATCH

[Cristian Cadar]

I see your point :)  But as a research project, it is still available if 
you want to give it a try.


Cristian

On 27/09/18 05:53, Xiao Liang Yu wrote:

Hello Cristian,

Does not integrated into mainline mean that it's discontinued?

Thanks
Xiao Liang

On Wed, 26 Sep 2018, 8:07 PM Cristian Cadar, <mailto:c.ca...@imperial.ac.uk>> wrote:


Hi Sang,

KATCH was unfortunately not integrated into the mainline, but you
should
still be able to build it using LLVM 2.9 if you'd like to give it a try.

Best,
Cristian

On 21/09/18 18:47, Sang Phan wrote:
 > Hi everyone,
 >
 > May I ask what is the status of KATCH?
 > https://srg.doc.ic.ac.uk/projects/katch/
 >
 > LLVM 2.9 is no longer supported, what is the latest version of
LLVM that
 > it can be built? (and also versions of other required packages)
 >
 > Thanks,
 > Sang
 >
 >
 > ___
 > klee-dev mailing list
 > klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
 > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
 >

___
klee-dev mailing list
klee-dev@imperial.ac.uk <mailto: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] Status of KATCH

[Cristian Cadar]

Hi Sang,

KATCH was unfortunately not integrated into the mainline, but you should 
still be able to build it using LLVM 2.9 if you'd like to give it a try.


Best,
Cristian

On 21/09/18 18:47, Sang Phan wrote:

Hi everyone,

May I ask what is the status of KATCH?
https://srg.doc.ic.ac.uk/projects/katch/

LLVM 2.9 is no longer supported, what is the latest version of LLVM that 
it can be built? (and also versions of other required packages)


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

Re: [klee-dev] Solver goals

[Cristian Cadar]

Hi Andy, the answer to the first two questions is a qualified yes -- you 
can make these guarantees assuming no interaction with external code, no 
constraint solving timeouts, no bugs in KLEE, etc.  As to your final 
question, there are several research projects that aim to do this (e.g., 
https://srg.doc.ic.ac.uk/projects/katch/), but they are not part of the 
KLEE mainline.


Cristian

On 12/09/18 13:18, Andy Owen wrote:

Hi, I have two questions which seem vaguely related:

1) If I run "klee foo.bc" and wait for it to finish, and it generates a 
bunch of test vectors, then what guarantees can I make about that set of 
test vectors?
- Can I guarantee that all possible lines of code (or basic blocks) 
which can be reached (within the constraints of what memory I made 
symbolic) will be reached?
- Can I guarantee that it is impossible for my code to dereference NULL 
or fail an assert (again with the same constraints) or there will be a 
test that demonstrates this?
- Will all the tests generated be distinct according to some property 
(e.g. the set of basic blocks they hit will be different)?


2) Is there a way to give KLEE a specific goal, so instead of generating 
lots of test cases, it instead tries to generate a single test case that 
does a specific thing (e.g. hits a klee_assert())?


Thanks for any assistance. I've searched lots over the KLEE 
documentation, but I haven't been able to find anything so far.


Andy


___
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] Test cases generated for symbolic file

[Cristian Cadar]

Hi, you can ignore the model_version, it just keeps track of the version 
for the POSIX model.  The stat buffer keeps the stat info associated 
with the file (see e.g. 
http://man7.org/linux/man-pages/man2/stat.2.html).  If you have time, it 
would be useful to document this on the website (e.g., at 
http://klee.github.io/tutorials/using-symbolic/) by submitting a PR at 
https://github.com/klee/klee.github.io


Best,
Cristian

On 21/06/18 21:55, Sang Phan wrote:

Hello,

I'm trying to understand the test cases generated when the input is
symbolic file.
For the password example under this link:
https://klee.github.io/tutorials/using-symbolic/, a test case viewed
by ktest-tool is the following:

https://klee.github.io/tutorials/using-symbolic/


ktest file : 'test04.ktest'
args   : ['password.bc', 'A', '-sym-files', '1', '10']
num objects: 3
object0: name: b'A-data'
object0: size: 10
object0: data: b'hel\x00\x00\x00\x00\x00\x00\x00'
object1: name: b'A-data-stat'
object1: size: 144
object1: data:
b'\x05\x08\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xea\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object2: name: b'model_version'
object2: size: 4
object2: data: b'\x01\x00\x00\x00'

+ I understand A-data is the content of the file, but what is
A-data-stat and model-version?
+ From the gen-random-bout, it seems data-stat can be generated
randomly, but how about model-version?

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

Re: [klee-dev] Options for symbolic environments no longer exist?

[Cristian Cadar]

This should still work under Docker. Are you sure you are passing the 
options correctly?  Those are not options to the KLEE tool itself, take 
a look at the tutorials for examples.  If you still have problems, 
please fill out a bug report detailing the exact steps you followed.


Cristian

On 09/06/18 22:36, Sang Phan wrote:

Hello,

I want to use KLEE with symbolic file or stdin. According to the
following document, I need to use -sym-files or -sym-stdin
http://klee.github.io/docs/options/


However, these options no longer exist in the latest release of KLEE
(docker). May I ask if they are broken, or are changed to something
else?

Thank you,
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

Re: [klee-dev] LLVM Error in Klee: does not support intrinsic function

[Cristian Cadar]

Thanks for reporting this.  Can you create a small test case and fill 
out a bug report on GitHub?


Cristian

On 11/06/18 05:20, Ridwan Shariffdeen wrote:

Hi,

I am trying to run klee with OpenJPEG 
(https://github.com/uclouvain/openjpeg), and encountered the following 
error:


LLVM ERROR: Code generator does not support intrinsic function 
'llvm.x86.sse2.psrai.d'!


Is it some limitation in Klee with vector generation 
(https://github.com/klee/klee/issues/660) ? or am I missing some 
instruction?


I am using WLLVM to compile with debug info and using extract-bc to 
generate the bytecode.


Any help on this is appreciated.

Thanks!



___
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] Klee Process Tree

[Cristian Cadar]

Hi Sang,

The option for dumping and visualizing the process tree is not well 
tested, so it would be useful to report bugs on GitHub, or even better, 
contribute a fix, if you have one.


Best,
Cristian

On 24/05/2018 22:58, Sang Phan wrote:

Hi everyone,

I'm trying to dump the process tree of Klee, but I get a segmentation fault.
The reason is that the conditions are not added to the tree nodes, e.g. 
when splitting.

I wonder if this tree has ever worked before.

Also, the dumping is called only once in the ExecutionTimer, but this 
class seems to be dead code.


Best,
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

Re: [klee-dev] About -sym-stdout

[Cristian Cadar]

Hi, many programs write their output to stdout, and if this output is 
symbolic, you might want to check that it respects various properties. 
For instance, we used this option for the crosschecking study between 
Coreutils and Busybox utilities in the original KLEE paper.


I agree more documentation would be useful.

Best,
Cristian

On 05/05/18 17:37, Xiao Liang Yu wrote:

Hello,

I have realized there is a|-sym-stdout|argument in KLEE. While the 
documentation says that it will make the|stdout|symbolic, I don’t see 
how it is useful. Would be great if there are some example use-cases for 
which|-sym-stdout|is useful.


Thanks!

Xiao Liang YU


___
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

Re: [klee-dev] Replay ktestfile directory

[Cristian Cadar]

Hi Awanish, this might be a bug, but we'd need more info.  Can you open 
a bug report/issue on GitHub with steps to reproduce this?


Best,
Cristian

On 01/04/18 17:01, Awanish Pandey wrote:

Hi,

I run klee over the coreutils using the command mentioned in coreutils 
experiments. When I replay the using


-replay-ktest-dir="---" it is giving warning "KLEE: WARNING ONCE: replay 
did not consume all objects in test input.

"
Out of 156 test cases in ptx replay was able to run only 6 test cases. 
What is the problem or I am doing something wrong


--
Thanking You
Awanish Pandey
PhD, CSE
IIT Kanpur


___
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