CODEWITHSUNDEEP
coqcoq-tacticverifiable-c
R2D2
R2D2

Reputation: 11

How do I write a proof for a switch statement with VST/ coq?

I had a question regarding the use of VST and switch statements.

I am having trouble writing a proof that steps through the switch statement when there is a matching case for the switch variable. For example:

I CAN write a proof for something like this:

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

However I CANNOT write a proof for something like this:

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;
   }
}

Whenever there is a matching case for "x" (like my second code example), then I run into a "No matching clauses for match" error when trying to write a tactic for the switch statement.

Normally I could write something like: "forward_if", "forward_if True", "forward_if (PROP() LOCAL() SEP())", and they would work for my first code example, but not for my second code example.

In summary: what should the next line(s) in my proof be for the second code example?

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

Thanks in advance!

Upvotes: 1

Views: 234

Answers (1)

Andrew Appel
Andrew Appel

Reputation: 548

This is, indeed, a bug in the VST-Floyd tactics for VST. You can patch it by doing this anywhere after 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.

Upvotes: 1

Related Questions