Help with simple algorithm needed (arithmetic overflow)

Sep 15, 2011 at 5:29 PM
Edited Sep 15, 2011 at 5:30 PM

Hi guys,
I am trying to verify a simple program using VCC 3.
My code is:

#include <vcc.h>
#include <limits.h>

int multiply(int termA, int termB)
_(requires termA >= 0 && termB >= 0 && termA * termB < INT_MAX)
_(ensures \result == termA * termB)
{
	int ret = 0;
	int i;
	for (i = 0; i != termB; ++i)
	_(invariant i >= 0)
	_(invariant i <= termB)
	_(invariant ret == termA * i)
	{
		ret += termA;
	}
	
	return ret;
}
VCC complains that ret += termA; might overflow. I tried various preconditions and loop invariants, 
but the only way I could make the error disappear was by adding the preconditions termA < 46340 && termB < 46340.
However, this is unsatisfactory as it unnecessarily constrains the function's scope.
I would be glad for any suggestions regarding how this function can be completely proven using VCC.
Thanks,
Marian
Sep 16, 2011 at 8:59 AM

Without having tested it maybe an additional invariant

i < termB ==> ret < INT_MAX - termA

could help VCC showing that there is no overflow. 

Also check out http://vcc.codeplex.com/wikipage?title=Arithmetic for the "unchecked"-annotation. Might be justified to use it here.

Sep 17, 2011 at 3:01 PM

Thanks for the suggestion! Using this invariant, the overflow warning indeed disappears. However the invariant itself can unfortunately not be proven.
If nobody has any futher suggestions I think I will resort to the "unchecked" statement.

Sep 19, 2011 at 9:18 AM
Edited Sep 19, 2011 at 9:20 AM

i guess you need to add some assertions or use a lemma that you prove separately.

from the top of my head i'd say you need something like

(termA * termB < INT_MAX) && (i < termB) && (ret == termA * i) ==> (ret < INT_MAX - termA)

the proof might go like this:

i < termB <==> i <= termB - 1

==> ret <= termA * (termB - 1)

<==> ret <= termA * termB - termA

==> ret < INT_MAX - termA

Maybe try to add the steps as assertions to guide VCC. Don't forget to use "i < termB" as a premise in the assertions.

Developer
Sep 19, 2011 at 1:08 PM

Here is the lemma that helps:

_(ghost _(pure) bool lemma(\integer a, \integer b, \integer i)
  _(requires a * b < INT_MAX)
  _(requires a >= 0 && i < b)
  _(ensures a * i + a < INT_MAX)
  _(returns \true)
{
  _(assert i + 1 <= b)
  _(assert a * (i + 1) <= a * b)
  return \true;
})

Verify this function by VCC using the command line switch "/oaf" that lets VCC treat the multiplication symbolically.

With the help of this lemma, your above function can be verified (with or without the "/oaf" option) after you insert the following line as the first statement in the loop body, directly before incrementing your variable "ret":

_(assert lemma(termA, termB, i))

By the way, it your precondition is probably weaker than what you intended.  You might have meant something like:

_(requires a >= 0 && b >= 0 && ((\integer) a) * ((\integer) b) < (\integer) INT_MAX)

Note that your condition "a * b < INT_MAX" holds for nearly all "a" and "b" due to integer overflow ("a * b <= INT_MAX" should be true for all integers "a" and "b").

Sep 20, 2011 at 10:52 AM

Quite sophisticated :)
Thank you both for your suggestions and explanations!

Coordinator
Sep 20, 2011 at 8:39 PM

Hi,

  just a small correction: arithmetic in pure annotation context (assert, contracts, etc.) actually defaults to being unbounded (unless in certain exceptional cases related to pure function definitions), so adding the additional (\integer) type casts does not make a difference here.

  Best, Mark

Sep 21, 2011 at 1:22 PM

Very good, that behavior seems more practical. Thanks again for the clarification!

Dec 4, 2011 at 6:12 PM

Hi all,

While trying to apply this technique to some code using integer division, it looks to me that in some cases it does not scale well (or am I overlooking something)?

For example

#include "vcc.h"
#include "limits.h"

_(ghost _(pure) bool lemma(\integer t1, \integer t2, \integer d1)
  _(requires t1 > 0 && t1 <= 65535)
  _(requires t2 > 0 && t2 <= 65535)
  _(requires d1 > 0 && d1 <= 65535)
  _(ensures (d1 + (d1 * t2) / t1) / t1 <= UINT_MAX)
  _(returns \true)
{
  return \true;
})

void test(unsigned  t1, unsigned  t2, unsigned d1)
_(requires t1 > 0 && t1 <= 65535)
_(requires t2 > 0 && t2 <= 65535)
_(requires d1 > 0 && d1 <= 65535)
{
 unsigned newEGV;
 _(assert lemma(t1, t2, d1))
 newEGV = (d1 + (d1 * t2) / t1) / t1;
 _(assert lemma(t1, t2, d1))
 newEGV; //including this line increases verification time 10-fold
}

Takes 270 seconds instead of 27 seconds "newEGV" is called the second time. (It is quite quick when arithmetic boundary checking is disabled.) Just out of curiosity: is there a more elegant approach for "containing" integer division in VCC?

(Extracted (simplified) from: http://www.cl.cam.ac.uk/%7Emjcg/FMStandardsWorkshop/example.pdf).

Best, Holger

Developer
Jan 19, 2012 at 6:36 PM

The performance variation seems to be a random seed issue; depending on which random seed you use, adding the last line can increase or decrease running time by an order of magnitude. This is unfortunate, but at least it does not indicate a scaling issue. (Note that the last line doesn't "call" newEGV; in fact, the new lone shouldn't even introduce a new proof obligation.)