如何检查用两种不同风格用C编写的两个代码是否等效？

Question

如何检查用两种不同风格用 C 编写的两个代码是否等效？

款式一：

#include <stdio.h>
#define K1 42
#define K2 1200

int i1, i2, i3 = -10;
unsigned u1, u2 = 1230, u3 = K1, u4;

int main( void ) {
    
    scanf( "%d", &i2 );
    scanf( "%u", &u1 );
    for ( i1 = i2 - 1; i2 < i3-i1 || u2 >= u1; u2 = u3, u3 = u3 % ++u4 ) {
        i2 = i2 / 2 + i3++;
        scanf( "%u", &u4 );
        do {
            i3 -= K2;
            u4 = ( u4 << 2 ) & ~ 0x04;
            i1 = i3 / i2;
        } while ( u4 < K1 && i1 + 23 >= i2 + 4 );
        u3 = --u1 + ( u4 -= 2);
    }
    u1 = ( u4 - u2 ) * 5 + ( u2 + u3 ) / 6 - u1;
    
    return 0;
}

款式2：

#include <stdio.h>
#define K1 42
#define K2 1200

int i1 = 0;
int i2 = 0;
int i3 = -10;
int t;
unsigned u1 = 0;
unsigned u2 = 1230;
unsigned u3 = K1;
unsigned u4 = 0 ;

int main(){

    scanf( "%d", &i2 );
    scanf( "%d", &u1 );
    i1 = i2 - 1;
    t = i3 - i1;
    
for_beg:
    if ( i2 < t ) goto for_tt;
    if ( u2 >= u1 ) goto for_tt;
    goto for_ff;

for_tt:
    i2 = i2 / 2;
    i2 += i3;
    i3 += 1;
    scanf( "%u", &u4 );
    
do_begin:
    i3 -= K2;
    u4 = u4 << 2;
    u4 = ~ 0x04;
    i1 = i3 / i2;
    
while_beg:
    if ( u4 >= K1 ) goto while_ff;
    t = i1 + 23;
    int t2 = i2 + 4;
    if ( t < t2 ) goto while_ff;
    goto do_begin;
    
while_ff:
    u1 -= 1;
    u4 -= 2;
    u3 = u1 + u4;

for_end:
    u4 += 1;
    u3 %= u4;
    goto for_beg;
    
for_ff:
    t = u4 - u2;
    t2 = u2 + u3;
    t *= 5;
    t2 /= 6;
    t += t2;
    t -= u1;
    
    return 0;
}

除了逐行验证代码之外，我还应该使用调试工具吗？ 谢谢！

我尝试通过打印

u1

变量来执行代码，但代码仍在循环中

Answer 1

证明这两个代码是等价的并不简单，我不知道有任何工具可以在一般情况下实现这一点。

第二个实例似乎是带有标签和 goto 以及常见表达式分解的分解版本。

显示单个反例是证明代码不等价的一种方法，但如果代码确实等价，找到反例可能并不容易，甚至是不可能的。

证明等价性的一种方法是将代码逐步重写为可以证明的等价结构。如果可以到达第二个实例，则可以认为代码是等效的。问题是，即使对于简单的情况，要证明所有极端情况的精确等价性也不是那么容易。

问题代码中，用于临时子表达式的变量存在问题：使用全局变量

t

来存储外层

i3 - i1

循环测试中使用的表达式

for

的值，同样的

t 

变量在内部循环中用于另一次计算...外部循环的第二次迭代使用

t

中

if ( i2 < t ) goto for_tt;

的当前值，这似乎不正确。请注意，

i3

在循环体中被修改，因此无论如何，每次迭代都应该重新计算

t = i3 - i1;

。

我愿意赌一美元，代码不等价......

Answer 2

如何检查用两种不同风格用C编写的两个代码是否等效？

在一般中，这个问题相当于停止问题，并且是无法回答的。

您可以尝试生成一组随机输入并验证两个程序是否产生相同的结果。如果它们对（比如说）10,000 个输入有效，那么它们“可能”是等价的。