Can cbmc minimize $long f(nondet long X)$?

[Georgi Guninski]

I am experimenting with cbmc.

Question 1: Can cbmc minimize $long f(nondet long X)$ with as
few calls to SAT oracle as possible?

Question 2: How to convert the following problem to C + cbmc:

long f(nondet long X);
long L,U,M,X;
L=MINSIGNEDLOG;U=MAXSIGNEDLONG;

M=(L+U)/2
if (exist X, s.t. F(X)<=M) U=M;
else L=M;


M=(L+U)/2
if (exist X, s.t. F(X)<=M) U=M;
else L=M;

... and so long up to sizeof(long);

if we omit "exist X" the result is not good since we can get
in the other branch of the if().

[Martin Nyx Brain]

On Tue, 2020-11-03 at 04:51 -0800, Georgi Guninski wrote:
> I am experimenting with cbmc.
>
> Question 1: Can cbmc minimize $long f(nondet long X)$ with as
> few calls to SAT oracle as possible?

There is nothing built-in to CBMC to do this (2LS has some optimisation
but not really user-accessible). You could use binary search which
should only require log(n) queries in the worst case. From having done
similar things the common case will often be faster.

Use the following program:

int main(int argc, char **argv) {
long lowerBound = BOUND ;
long X;

long res = f(X);

assert(BOUND <= res);

return 0;
}

then write a script to:

1. Keep track of the current lower and upper bounds on the minimum
value.

2. run cbmc program.c -D BOUND=(lower + upper)/2

3.A. If it is SAT, set upper=value of res from model
3.B. If it is UNSAT, set lower=(lower + upper)/2

4. Loop back to 2 if upper != lower.

> Question 2: How to convert the following problem to C + cbmc:
>
> long f(nondet long X);
> long L,U,M,X;
> L=MINSIGNEDLOG;U=MAXSIGNEDLONG;
>
> M=(L+U)/2
> if (exist X, s.t. F(X)<=M) U=M;
> else L=M;
>
>
> M=(L+U)/2
> if (exist X, s.t. F(X)<=M) U=M;
> else L=M;
>
> ... and so long up to sizeof(long);
>
> if we omit "exist X" the result is not good since we can get
> in the other branch of the if().

I'm not quite sure what you want this program to do but it is pretty
close to being C. CBMC does have an existential quantifier but to be
honest you are probably best off creating a new variable each time you
want a different call f.

Cheers,
- Martin

[Georgi Guninski]

On Tue, Nov 3, 2020 at 6:26 PM Martin Nyx Brain
<martin...@cs.ox.ac.uk> wrote:

> I'm not quite sure what you want this program to do but it is pretty
> close to being C. CBMC does have an existential quantifier but to be
> honest you are probably best off creating a new variable each time you
> want a different call f.
>

Thanks for the reply and making cbmc opensource :)
The pseudo code was trying to unroll the binary search
in a single call to cbmc.

Since for existential quantification you recommend new variables,
what changes are needed to the following program so that
assert(0) is not reached and the comment is correct?

long f(long X) {
if(X<=1) return 1;
else return 2;
}

int main() {
long X1;
/*If exists X1 such that f(X1)<=1 then return 1*/
if(f(X1)<=1)
return 1;
__CPROVER_assert(0,"not reached");
return 0;
}

[Martin Nyx Brain]

On Wed, 2020-11-04 at 11:30 +0200, Georgi Guninski wrote:
> On Tue, Nov 3, 2020 at 6:26 PM Martin Nyx Brain
> <martin...@cs.ox.ac.uk> wrote:
>
> > I'm not quite sure what you want this program to do but it is
> > pretty
> > close to being C. CBMC does have an existential quantifier but to
> > be
> > honest you are probably best off creating a new variable each time
> > you
> > want a different call f.
> >
>
> Thanks for the reply and making cbmc opensource :)
> The pseudo code was trying to unroll the binary search
> in a single call to cbmc.

No worries :-) Unrolling it in to one call... you can do this. I'm
not sure it's the best way of solving this problem but it should be
possible.

> Since for existential quantification you recommend new variables,
> what changes are needed to the following program so that
> assert(0) is not reached and the comment is correct?
>
> long f(long X) {
> if(X<=1) return 1;
> else return 2;
> }
>
> int main() {
> long X1;
> /*If exists X1 such that f(X1)<=1 then return 1*/
> if(f(X1)<=1)
> return 1;
> __CPROVER_assert(0,"not reached");
> return 0;
> }

I think the code does what the comment says. There exists a variable
X1 and if (f(X1) <= 1) then return 1. Your comment doesn't say
anything about what is returned if !(f(X1) <= 1).

I don't know if it would help but maybe __CPROVER_assume(X) is what you
want. Officially the semantics are:

while(!X) {}

in practice it is implemented much more efficiently and it means that
after the statement, X will always be true. So:

__CPROVER_assume(X);
__CPROVER_assert(X);

means the assertion will always pass. Note that assert then assume
does not do the same thing!

Cheers,
- Martin