A question about the addition operation of bit vectors

[angel...@gmail.com]

Dear all,

   

    The addition of bit vectors may produce a result that was not expected.

    For example, for a constraint (a<b)&&(a>b+100), which is expressed using cvc as follows.

      a: BITVECTOR(8);

      b: BITVECTOR(8);

    %----------------------------------------------------

     ASSERT BVGT(a,BVPLUS(8,0bin01100100,b));

     ASSERT BVLT(a,b);

    %----------------------------------------------------

   QUERY FALSE;

   

   STP reports invalid and gives a counterexample as: a=0xC0,b=0xD8.

   The reason for this is that b+100 results in an overflow and its value is truncated.

  But, we usually do not want to get such result. My question is: Do we have any method to avoid such kinds of solutions for our constraint?

  I have put another assertion "ASSERT BVGT (BVPLUS(8,0bin01100100,b),b);" into the above cvc file, and STP reports "Valid". 

  But this method may be inapplicable when we process a path condition of a program, because we may not know exactly the details of every addition operation.

  If anyone has the experiences in tackling this issue, I hope you can give me some suggestions.

  Any of your help will be much appreciated!

Best regards,

Mingyue Jiang

   

[Jonas Wagner]

Hi Mingyue Jiang,

I think the right solution depends on what you want to achieve. Why do you need to avoid such solutions?

If you're verifying a program in C that uses unsigned integers, then addition overflow is well-defined, and your verifier should take that possibility into account. Overflow is also well-defined in Java, and a number of other languages.

If the program is a C program using signed integers, then the behavior of overflow is no more well-defined; the C language gives no guarantees in this case, and the compiler can assume overflow will never happen. One of the easiest ways to handle this is using a tool such as UndefinedBehaviorSanitizer (i.e., using the -fsanitize=undefined option in GCC or Clang). This adds assertions to the program that terminate the program if undefined behavior would happen.

Finally, you have the option of using mathematical integers instead of bitvectors.

Does this help?

Jonas

--

---
You received this message because you are subscribed to the Google Groups "stp-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to stp-users+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[angel...@gmail.com]

Hi,Jonas,

   Thanks for your explanation.

  

   I want to avoid such kind of solutions because I'm using the solutions of STP as a test input for a program.

   For example, for a test input (a,b), if their relation is "a=b+10", the expected concrete values of 'a' and 'b' should satisfy 'a>b'. But if 'b+10' leads to an overflow (i.e, b=2147483646), we may get a pair of values which satisfy  'a<b'.

   These two pairs of test inputs my result in different program behaviors.

   I'm also confused why STP always generates values (as counterexample) that may lead to overflow when there are alternative values that will not. For the above example, we can get many values for b which do not make 'b+10' overflow.

    

   I used KLEE to generate path conditions, which is specified in CVC. So I have no idea to use mathematical integers instead of bitvector.

Best regards,

Mingyue

[J Schwartz]

Mingyue Jiang said:
> The reason for this is that b+100 results in an overflow and its value is
> truncated.

I create STP expressions for integer arithmetic expressions and I use
bit vectors to represent the integers, so I run into this problem,
too.

I solve it by collecting additional assertions that will need to be
met, while I'm constructing the expression. So, if I'm constructing
"x+y", I need to also assert that "x+y >= x" (or "x+y >= y", either
will do). I have similar assertions for: underflow of subtraction ("x
>= x-y"), overflow of multiplication ("y == 0 || x*y >= x"), overflow
of base 2 exponentiation ("x == 0 || 2^x >= x").

Jonas Wagner said:
> Finally, you have the option of using mathematical integers instead of bitvectors.

No. I don't use integers because some of the operations that I need
were not available for integers. Instead, I use bit vectors, for
which I can represent all the operators that I need. I implemented
this a while ago, so I don't recall which operators weren't available;
but the set of operations that I represent are: addition, subtraction,
multiplication, base-2 exponentiation, max, min, divison (returning
the integer ceiling), base-2 log (returning the integer ceiling).

J

[Jonas Wagner]

Hi,

I want to avoid such kind of solutions because I'm using the solutions of STP as a test input for a program.

Could you modify your program instead? If the program does not check for overflow where it should, that could be a problem.

I used KLEE to generate path conditions, which is specified in CVC. So I have no idea to use mathematical integers instead of bitvector.

If you use KLEE, then you're in the LLVM world, and it shouldn't be too hard to use UndefinedBehaviorSanitizer to add overflow checks for you. For instance, you could compile your program with

    clang -O2 -Wall -g -fsanitize=undefined -fno-sanitize-recover -flto -o myprogram.bc -c myprogram.c

Then, myprogram.bc will be a bitcode file that you can pass to KLEE. in addition, any path that exits successfully will have overflow checks in the path condition.

Cheers,
Jonas