1

Does this C expression always evaluate to true?

((x+y)<<4) + y - x == 17*y +15*x

From what I can tell the arithmetic is correct, but the only thing I am unsure about is what will happens in cases of overflow.

My understanding is that the C multiplication expressions handle overflow the same way as a bit shift would, but I am not sure.

Does anyone know the answer to this?

7
  • 5
    Did you try running the code and purposely causing an overflow? Commented Apr 11, 2016 at 2:55
  • 1
    What are the types of these variables? Particularly, signed or unsigned? Commented Apr 11, 2016 at 3:01
  • 1
    Provide a minimal reproducible example. The expression might invoke undefined behaviour in all operations. Commented Apr 11, 2016 at 3:08
  • in case of overflow both sides invoke undefined behavior (for signed types), or wrap around (for unsigned) and the result is still equal for both sides
    – phuclv
    Commented Apr 11, 2016 at 3:21
  • @LưuVĩnhPhúc in the signed case the expression may evaluate to false (or any other program behaviour)
    – M.M
    Commented Apr 11, 2016 at 3:45

2 Answers 2

2

You can run such examples through a SAT solver to check the satisfiability of equations or formulas like you just specified.

I didn't find any X or Y which satisfied your constraints (i.e, does there exist any X or Y which produce an inequality in this equation)

(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))

(assert (not (= (bvsub (bvadd (bvshl (bvadd x y) #x00000004) y) x)
                (bvadd (bvmul #x00000011 y) (bvmul #x0000000f x)))))

(check-sat)
(get-model)

In regards to overflow, logics over bitvectors generally provide no distinction between signed and unsigned bit-vectors as numbers. Instead, the theory of bit-vectors provides special signed versions of arithmetical operations where it makes a difference whether the bit-vector is treated as signed or unsigned. I have used the appropriate operator to the equation you've specified. Of course, you could just the results algebraically to (x+y)<<4 == 16y + 16x but a SMT solver handles cases like overflow which are difficult to formalize).

It doesn't matter what your instruction word size, there is no X or Y that can produce an inequality.

3
  • It is a formal "verification" of a decision procedure over bitvectors, it is an abstract model of the "world" of numerals that a C program inhabits.
    – zetavolt
    Commented Apr 11, 2016 at 3:26
  • I don't think that is how science & math works -- you have "absence of evidence" which does not prove anything
    – Soren
    Commented Apr 11, 2016 at 3:28
  • 1
    Without delving too deeply into Karl Popper and the philosophy of science here, the brief answer is -- Yes it is, this is a formal mathematical proof, or as close as you'll get without a kt-tactic out of a theorem prover like Coq. If you are interested in how the decision problem applies to formal verification of problems (even simple one such is this) Donald Knuth has a whole new fascicle on it. Wikipedia has a dense but largely accessible introduction to proving statements with SAT solvers: en.wikipedia.org/wiki/…
    – zetavolt
    Commented Apr 11, 2016 at 3:32
-1

The answer is "no" especially in case of overflow.

As you can see from answers here most computers are 2-complement, but they do not have to be (and historically there have been a few one-complement computers), and overflow errors are therefore undefined behaviour.

It may work on your computer but it is not guaranteed to work on all.

2
  • it's complement, not compliment
    – phuclv
    Commented Apr 11, 2016 at 3:20
  • 1
    Signed overflows are UB regardless of whether 2's complement is in use
    – M.M
    Commented Apr 11, 2016 at 3:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.