Wird dieser C-Ausdruck immer als wahr ausgewertet?Bit-Manipulations-Rätsel
((x+y)<<4) + y - x == 17*y +15*x
Von dem, was ich der Arithmetik sagen kann, ist richtig, aber das einzige, was ich bin nicht sicher, über das, was wird in Fällen von Überlauf passiert.
Mein Verständnis ist, dass die C-Multiplikation Ausdrücke handhaben gleichen Weg wie eine Bit-Verschiebung wäre, aber ich bin mir nicht sicher.
Kennt jemand die Antwort darauf?
Die Antwort ist "Nein", besonders im Falle eines Überlaufs.
Wie Sie aus Antworten sehen here die meisten Computer sind 2-Komplement, aber sie müssen nicht sein (und in der Vergangenheit gab es ein paar Ein-Komplement-Computer), und Überlauffehler sind daher undefiniert Verhalten.
Es kann auf Ihrem Computer funktionieren, aber es ist nicht garantiert, dass alle funktionieren.
es ist * Komplement *, nicht * Kompliment * –
Signed Überläufe sind UB unabhängig davon, ob 2 Komplement verwendet wird –
Sie können solche Beispiele über eine SAT solver ausführen, um die Erfüllbarkeit von Gleichungen oder Formeln wie Sie gerade angegeben zu überprüfen.
I, die Ihre Einschränkungen erfüllt hatte keine X oder Y finden (dh existiert dort eine beliebige X oder Y, die eine Ungleichheit in dieser Gleichung erzeugen)
(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 Bezug auf Überlauf, Logiken über bitvectors geben im Allgemeinen keine Unterscheidung zwischen vorzeichenbehafteten und vorzeichenlosen Bitvektoren als Zahlen vor. Stattdessen liefert die Theorie der Bitvektoren spezielle signierte Versionen von arithmetischen Operationen, bei denen es einen Unterschied macht, ob der Bitvektor als vorzeichenbehaftet oder vorzeichenlos behandelt wird. Ich habe den entsprechenden Operator für die von Ihnen angegebene Gleichung verwendet. Natürlich könnten Sie nur die Ergebnisse algebraisch zu (x+y)<<4 == 16y + 16x, aber ein SMT-Löser behandelt Fälle wie Überlauf, die schwer zu formalisieren sind).
Es spielt keine Rolle, was Ihre Instruktion Wortgröße, es gibt keine X oder Y, die eine Ungleichheit produzieren kann.
Wie ist das "C" -Code? – Soren
Es ist eine formelle "Verifikation" einer Entscheidungsprozedur über Bitvektoren, es ist ein abstraktes Modell der "Welt" der Zahlen, die ein C-Programm bewohnt. –
Ich glaube nicht, dass so Wissenschaft und Mathematik funktioniert - Sie haben "Abwesenheit von Beweisen", die nichts beweisen – Soren
Haben Sie versucht, den Code auszuführen und absichtlich einen Überlauf zu verursachen? –
Was sind die Arten dieser Variablen? Insbesondere signiert oder unsigniert? – user2357112
Stellen Sie eine [mcve] bereit. Der Ausdruck könnte ein undefiniertes Verhalten in ** all ** -Operationen auslösen. – Olaf