使用Frama-C WP验证含移位运算符的简单函数时出现证明超时的问题求助

问题描述 #

我最近在使用Frama-C的WP插件验证一个简单的左移函数时遇到了困惑——逻辑上完全成立的结论，用Alt-Ergo和Z3证明却都超时了。想请教大家该怎么解决这个问题。

测试代码

我的代码非常简单，只是对1做左移操作，契约里已经限制了移位范围：

/*@ 
  requires a >= 0 && a <= 2; 
  assigns \nothing; 
  ensures \result < 10; 
*/ 
int bob(int a) { 
  return 1 << a; 
}

验证命令及结果

我用以下命令执行验证：

frama-c test.c -wp -wp-prover="Alt-Ergo,z3" -wp-status

得到的输出如下：

[kernel] Parsing test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Timeout] typed_bob_ensures (Qed 1ms) (Alt-Ergo) (Cached)
[wp] [Cache] found:2
[wp] Proved goals: 3 / 4
Terminating: 1 Unreachable: 1
Qed: 1 (0.72ms) Timeout: 1
------------------------------------------------------------
Function bob
------------------------------------------------------------
Goal Post-condition (file test.c, line 110) in 'bob':
Let x = lsl(1, a).
Assume {
Type: is_sint32(a) /\ is_sint32(x).
(* Pre-condition *)
Have: (0 <= a) /\ (a <= 2).
}
Prove: x <= 9.
Prover Alt-Ergo 2.6.2 returns Timeout (Qed:1ms) (2s) (cached)
Prover Z3 4.8.12 returns Timeout (Qed:1ms) (2s) (cached)
------------------------------------------------------------

我的尝试与疑问

根据WP手册，有一个shift策略可以把lsl(a,k)转换为a*2^k，按说转换后这个证明应该能自动完成才对？

我尝试定义了如下策略：

/*@ 
  @strategy shift: \tactic("Wp.shift"); 
*/ 
/*@ 
  requires a >= 0 && a <= 2; 
  assigns \nothing; 
  ensures \result < 10; 
*/ 
int bob(int a) { 
  return 1 << a; 
} 
//@proof shift : bob;

也试过用-wp-strategy="shift"参数，但都没有效果，还是超时。我是不是哪里操作错了？有没有其他方法能让prover正确处理移位运算符的证明？

解决方案 #

你遇到的问题核心是默认情况下WP的移位策略未被正确触发，或者需要更明确的配置来引导 prover 完成推理。以下是几种可行的解决方法：

1. 正确配置并应用移位策略

你之前的策略定义可能没有被WP正确绑定到目标。可以尝试全局启用移位策略，或者明确指定将策略应用到bob函数的后置条件目标：

// 全局启用移位策略，对所有函数生效
/*@ @strategy global: \tactic("Wp.shift"); */

/*@ 
  requires a >= 0 && a <= 2; 
  assigns \nothing; 
  ensures \result < 10; 
*/ 
int bob(int a) { 
  return 1 << a; 
}

// 或者仅对bob的后置条件目标应用策略
//@proof: bob, goal Post-condition, tactic "Wp.shift";

如果还是不行，可以结合多项式化简策略，帮助prover快速处理乘法表达式：

/*@ @strategy shift_poly: \tactic("Wp.shift"); \tactic("Wp.polynomial"); */
//@proof shift_poly : bob;

当Wp.shift正确触发后，lsl(1,a)会被转换为1 * 2^a，结合a<=2的前置条件，2^a最大为4，1*4=4<10的结论会被瞬间证明。

2. 显式枚举移位范围（简单直接）

由于你的前置条件已经限制a只能取0、1、2三个值，完全可以在契约中显式枚举结果，让Qed prover直接完成证明：

/*@ 
  requires a >=0 && a <=2;
  assigns \nothing;
  ensures \result == (a==0 ? 1 : (a==1 ? 2 :4));
  ensures \result <10;
*/
int bob(int a) {
  return 1 <<a;
}

这种方式不需要调用外部prover，Qed会直接验证每个分支的结果都满足<10的要求。

3. 延长Prover超时时间（权宜之计）

有时候超时只是因为prover推理时间略长于默认的2秒，可以通过-wp-timeout参数延长超时时间，比如设置为5秒：

frama-c test.c -wp -wp-prover="Alt-Ergo,z3" -wp-status -wp-timeout=5

不过这只是临时解决方案，优先推荐通过策略调整让证明更高效。

4. 启用运行时检查（辅助推理）

你收到的Missing RTE guards警告提示WP没有为移位操作添加安全性检查，启用RTE后，WP会自动添加移位位数的合法性契约，可能间接帮助prover更好地推理：

frama-c test.c -wp -wp-rte -wp-prover="Alt-Ergo,z3" -wp-status

内容来源于stack exchange