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?

John Kugelman
  • 349,597
  • 67
  • 533
  • 578
user1888863
  • 399
  • 2
  • 9
  • 5
    Did you try running the code and purposely causing an overflow? – Jonny Henly Apr 11 '16 at 02:55
  • 1
    What are the types of these variables? Particularly, signed or unsigned? – user2357112 Apr 11 '16 at 03:01
  • 1
    Provide a [mcve]. The expression might invoke undefined behaviour in **all** operations. – too honest for this site Apr 11 '16 at 03: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 Apr 11 '16 at 03:21
  • @LưuVĩnhPhúc in the signed case the expression may evaluate to false (or any other program behaviour) – M.M Apr 11 '16 at 03:45
  • @M.M yes I just said that it's equal in the unsigned case. In signed case anything can happen – phuclv Apr 11 '16 at 03:46
  • @JonnyHenly while that's relevant to think about, it cannot be tested by running it - since anything could happen, it could just work, and actually that is the most likely result. – harold Apr 11 '16 at 07:45

2 Answers2

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.

zetavolt
  • 2,989
  • 1
  • 23
  • 33
  • 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 Apr 11 '16 at 03:26
  • I don't think that is how science & math works -- you have "absence of evidence" which does not prove anything – Soren Apr 11 '16 at 03: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: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#3-satisfiability – zetavolt Apr 11 '16 at 03: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.

Community
  • 1
  • 1
Soren
  • 14,402
  • 4
  • 41
  • 67