如何检查两个用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;
}
样式二:
#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
变量的代码,但代码仍在循环中
3条答案
按热度按时间cyvaqqii1#
您可以通过 * 阅读代码 * 进行检查,这些代码不相等。
第一个代码有
而第二个密码
10
u4
。OT:不要这样写代码:C在很大程度上使我们不必使用标签和汇编风格的编码。
4c8rllxm2#
这是不平凡的证明这2个代码是等效的,我不知道任何工具,可以在一般情况下实现这一点。
第二个示例似乎是一个分解的版本,带有标签和goto沿着公共表达式因子分解。
给出一个反例是证明代码不等价的一种方法,但是如果代码确实等价,找到一个反例可能并不容易,而且完全不可能。
证明等价性的一种方法是将代码重写为可以证明的等价结构。如果可以达到第二个示例,则代码可以被认为是等效的。问题是,即使对于简单的情况,也不容易证明所有角落情况的精确等价性。
在问题代码中,用于临时子表达式的变量存在问题:一个全局变量
t
用于存储表达式i3 - i1
的值,该表达式用于外部for
循环测试,同一个变量t
用于内部循环的另一个计算.外部循环的第二次迭代使用if ( i2 < t ) goto for_tt;
中的t
的当前值,这似乎是不正确的。请注意,i3
在循环体中被修改,因此无论如何都应该为每次迭代重新计算t = i3 - i1;
。我敢赌一块钱这两个密码...
j1dl9f463#
如何检查两个用C语言编写的不同风格的代码是否等价?
一般来说,这个问题相当于halting problem,是无法回答的。
您可以尝试生成一组随机输入,并验证两个程序是否产生相同的结果。如果他们做了(说)10,000输入,他们是 * 可能 * 等效。