[klee-dev] Direct Search Towards Assertion

[Urmas Repinski]

Hi.

> Unfortunately, this does not affect the way paths are explored. In 
> general, it doesn't make sense to use klee_assume(false) and 
> klee_assume(true). The first one terminates the state (klee_assert or 
> klee_report_error are more appropriate for that) and the second one does 
> nothing.

Yes, it will behave exactly as defined, klee_assume(false) terminates the state and the klee_assume(true) does nothing.

Using this functionality it is possible to exclude all paths, where index != 3 , from the generation, to terminate all states where index != 3 , and to keep one state where index == 3. This should generate the required input.

As far as i see, usage of those 2 operators and plus logical conditions allows to modify code in this way, that only required set of inputs is generated.

I am terribly sorry, but i still think that usage of klee_assume() function can be reasonable for input generation. And not in this case only, i had made set of experiments on input generation by dynamical modification of the code using adding/removing klee_assume(...) function to the code and processing it by the KLEE. Unfortunately nothing is published, as far as no meaningful experimental results were achieved, but usage of KLEE klee_assume(...) function still can be extremely useful.


Urmas Repinski.



> Date: Thu, 10 Apr 2014 13:13:27 +0100
> From: paul.marinescu at imperial.ac.uk
> To: urrimus at hotmail.com; kirill.sc at gmail.com; klee-dev at imperial.ac.uk
> Subject: Re: [klee-dev] Direct Search Towards Assertion
> 
> Unfortunately, this does not affect the way paths are explored. In 
> general, it doesn't make sense to use klee_assume(false) and 
> klee_assume(true). The first one terminates the state (klee_assert or 
> klee_report_error are more appropriate for that) and the second one does 
> nothing.
> 
> Paul
> 
> On 10/04/14 12:51, Urmas Repinski wrote:
> > Hi.
> >
> > Sorry mistake in the code.
> >
> > #define n 10
> > int main() {
> >
> > int a[n];
> > klee_make_symbolic(&a, sizeof(a), "a");
> >
> > int index = 0;
> > for (int i = 1; i<n;i++){
> > if (a[i] < a[index])
> > index = i;
> >
> > }
> > printf("index: %i\n", index);
> >
> > if (index != 3){
> >                  klee_assume(false);
> > //klee_assert(false);
> > }
> >
> >         klee_assume(true);
> > return 0;
> > }
> >
> > Urmas.
> >
> > ------------------------------------------------------------------------
> > From: urrimus at hotmail.com
> > To: kirill.sc at gmail.com; klee-dev at imperial.ac.uk
> > Date: Thu, 10 Apr 2014 14:49:32 +0300
> > Subject: Re: [klee-dev] Direct Search Towards Assertion
> >
> > Hi, Kirill.
> >
> > As far as during generation paths, where klee_assume(false) occur, are
> > not processed, then i suggest to try following:
> >
> > If you require input when index == 3 to be generated, then it is
> > possible to disable all paths where index != 3, and to launch generation.
> >
> > This should make generation of the input with properties you require.
> >
> > Try this one:
> >
> > #define n 10
> > int main() {
> >
> > int a[n];
> > klee_make_symbolic(&a, sizeof(a), "a");
> >
> > int index = 0;
> > for (int i = 1; i<n;i++){
> > if (a[i] < a[index])
> > index = i;
> >
> > }
> > printf("index: %i\n", index);
> >
> > if (index != 3){
> >                  klee_assume(false);
> > //klee_assert(false);
> > }
> >
> >         klee_assume(false);
> > return 0;
> > }
> >
> >
> > This should help,
> > Urmas Repinski.
> >
> >
> > ------------------------------------------------------------------------
> > Date: Thu, 10 Apr 2014 09:25:10 +0100
> > From: kirill.sc at gmail.com
> > To: klee-dev at imperial.ac.uk
> > Subject: [klee-dev] Direct Search Towards Assertion
> >
> > Hello everyone.
> >
> > I have a simple example, with the list of symbolic integers, and I am
> > searching for the smallest one. At the end of the code I am checking if
> > element at position [3] was the smallest one, and assert.
> > code:
> >
> > #define n 10
> > int main() {
> >
> > int a[n];
> > klee_make_symbolic(&a, sizeof(a), "a");
> >
> > int index = 0;
> > for (int i = 1; i<n;i++){
> > if (a[i] < a[index])
> > index = i;
> >
> > }
> > printf("index: %i\n", index);
> >
> > if (index == 3){
> > klee_assert(false);
> > }
> >
> > return 0;
> > }
> >
> > I am running with "-search=dfs" argument. In this example KLEE generates
> > 2^(n-1) code paths in the for loop by trying all different combinations
> > of input data.
> >
> > Question: I do not really care to cover all possible code paths in the
> > for loop, I only care that the smallest element is not at position=3. I
> > expect this assertion to produce constrain something like: a[3] < a[0]
> > && a[3] < a[1] etc. Which should be easy to resolve.
> > How can I "ask" KLEE to try to trigger this assertion as quick as
> > possible at the beginning of the search?
> >
> > Thank you.
> > Kirill
> >
> > _______________________________________________ klee-dev mailing list
> > klee-dev at imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> >
> > _______________________________________________ klee-dev mailing list
> > klee-dev at imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> >
> >
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at imperial.ac.uk
> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> >
> 
 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed