[klee-dev] Direct Search Towards Assertion

[Paul Thomson]

Sure, this will limit the inputs generated, but will not allow the desired
inputs to be found (much) more quickly. You are essentially terminating the
state immediately before it would terminate anyway. So all paths are still
being explored.

Thanks,
Paul


On 10 April 2014 13:25, Urmas Repinski <urrimus at hotmail.com> wrote:

> 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
> > >
> >
>
> _______________________________________________
> 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