1

我有一个关于使用 VST 和 switch 语句的问题。

当 switch 变量存在匹配的情况时，我无法编写逐步执行 switch 语句的证明。例如：

我可以为这样的事情写一个证明：

int switchTest(int x){
   switch (x){
      case(0): return 0;
      default: return 1;
   }
}

但是我不能为这样的事情写证明：

int switchTest(){
   int x = 5;
   switch (x){
      case(0): return 0;
      case(1): return 1;
      case(5): return 5;  //The matching case for x - causes my problem
      default: return 8;
   }
}

每当有“x”的匹配案例（如我的第二个代码示例）时，我在尝试为 switch 语句编写策略时遇到“没有匹配的匹配子句”错误。

通常我可以写类似：“forward_if”、“forward_if True”、“forward_if (PROP() LOCAL() SEP())”，它们适用于我的第一个代码示例，但不适用于我的第二个代码示例。

总而言之：第二个代码示例的证明中的下一行应该是什么？

Lemma body_switchTest: semax body Vprog Gprog f_switchTest switchTest_spec.
Proof.
start_function.
forward.
???

提前致谢！

4

1 回答 1

1

这确实是 VST 的 VST-Floyd 策略中的一个错误。您可以在 Import VST.floyd.proofauto 之后的任何地方进行修补：

Ltac process_cases sign ::= 
match goal with
| |- semax _ _ (seq_of_labeled_statement 
     match select_switch_case ?N (LScons (Some ?X) ?C ?SL)
      with Some _ => _ | None => _ end) _ =>
       let y := constr:(adjust_for_sign sign X) in let y := eval compute in y in 
      rewrite (select_switch_case_signed y); 
           [ | reflexivity | clear; compute; split; congruence];
     let E := fresh "E" in let NE := fresh "NE" in 
     destruct (zeq N (Int.unsigned (Int.repr y))) as [E|NE];
      [ try ( rewrite if_true; [  | symmetry; apply E]);
        unfold seq_of_labeled_statement at 1;
        apply unsigned_eq_eq in E;
        match sign with
        | Signed => apply repr_inj_signed in E; [ | rep_lia | rep_lia]
        | Unsigned => apply repr_inj_unsigned in E; [ | rep_lia | rep_lia]
        end;
        try match type of E with ?a = _ => is_var a; subst a end;
        repeat apply -> semax_skip_seq
     | try (rewrite if_false by (contradict NE; symmetry; apply NE));
        process_cases sign
    ]
| |- semax _ _ (seq_of_labeled_statement 
     match select_switch_case ?N (LScons None ?C ?SL)
      with Some _ => _ | None => _ end) _ =>
      change (select_switch_case N (LScons None C SL))
       with (select_switch_case N SL);
        process_cases sign
| |- semax _ _ (seq_of_labeled_statement 
     match select_switch_case ?N LSnil
      with Some _ => _ | None => _ end) _ =>
      change (select_switch_case N LSnil)
           with (@None labeled_statements);
      cbv iota;
      unfold seq_of_labeled_statement at 1;
      repeat apply -> semax_skip_seq
end.
于 2020-12-16T20:02:34.143 回答