[klee-dev] Is it possible to implement a tool that genereates unit test driver for KLEE?

[Wei MA]

Hi,

Thanks.

Here it is, http://swtv.kaist.ac.kr/publications/icse18-conbrio.pdf

2.2 Concolic Unit Test Driver/Stub Generation

For each target function f , a concolic unit testing technique automatically generates symbolic stubs and a symbolic unit test driver. Symbolic stubs simply return symbolic values (without updating global variables and output parameters for simplicity) and a symbolic driver invokes f after assigning symbolic values to the input variables of f according to their types as follows:

• primitive types: primitive variables are directly assigned with primitive symbolic values of the corresponding types.

• array types: each array element is assigned with a symbolic variable according to the type of the array element (for a large array, only the first n elements are assigned with symbolic values where n is given by a user).

• pointer types: for a pointer variable ptr pointing to a variable of a type T, a driver allocates memory whose size is equal to the size of T and assigns the address of the allocated memory to ptr (i.e. ptr=malloc(sizeof(T))). Then, a driver assigns *ptr with a symbolic value of type T. If the size of T is not known (e.g. FILE in standard C library), NULL is assigned to ptr. If there exists a pointer variable ptr2 pointing to a symbolic variable of the same type T, a driver assigns ptr2 to ptr.

• structure types: a unit test driver specifies all fields of struct variable s as symbolic variables recursively (i.e. if s contains struct variable t, a unit test driver specifies the fields of t as symbolic too). A limitation of this approach is that the drivers and stubs often over-approximate the real environment of f and allow infeasible unit executions (i.e. executions of f which are not feasible at systemlevel) that may raise false alarms


________________________________
From: Nowack, Martin <m.nowack at imperial.ac.uk>
Sent: Monday, September 2, 2019 1:20:50 PM
To: Wei MA
Cc: klee-dev
Subject: Re: [klee-dev] Is it possible to implement a tool that genereates unit test driver for KLEE?

Dear Wei Ma,

Could you please summarise and provide a few details how the other symbolic execution engine is used?
This should help people to answer if this is possible with KLEE.

All the best,
Martin


On 31. Aug 2019, at 15:24, Wei MA <wei.ma at uni.lu<mailto:wei.ma at uni.lu>> wrote:


Dear All,

Recently, I found a series of papers from the same group that implements a tool that can generate unit test driver, http://swtv.kaist.ac.kr/tools/conbrio . But they use the other symbolic tool. Is it possible to do that in KLEE to implement a similar tool? Or there has been some work about it in KLEE.

Best Regards,
Wei Ma


_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed