From 83b556a101b7ed490acf9e127c5b4b9db40e1019 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 30 Mar 2021 11:25:28 +0200 Subject: Now a more general way to perform imm operations --- riscV/Asmgen.v | 15 +++++++++------ riscV/Asmgenproof.v | 1 + riscV/Asmgenproof1.v | 7 ++++++- riscV/ExpansionOracle.ml | 4 ++-- riscV/NeedOp.v | 3 +-- riscV/Op.v | 34 ++++++++++++++++++++++++---------- riscV/PrintOp.ml | 7 +++++-- riscV/RTLpathSE_simplify.v | 4 ++-- riscV/ValueAOp.v | 31 ++++++++++++++++++------------- 9 files changed, 68 insertions(+), 38 deletions(-) (limited to 'riscV') diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index d4c6b73a..54c7a7c0 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -219,6 +219,12 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru | Some false => sem r1 X0 end. +Definition get_opimmR0 (rd: ireg) (opi: opimm) := + match opi with + | OPimmADD i => Paddiw rd X0 i + | OPimmADDL i => Paddil rd X0 i + end. + Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := match cond, args with @@ -770,6 +776,9 @@ Definition transl_op | Ocmp cmp, _ => do rd <- ireg_of res; transl_cond_op cmp rd args k + | OEimmR0 opi, nil => + do rd <- ireg_of res; + OK (get_opimmR0 rd opi :: k) | OEseqw optR0, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; @@ -819,9 +828,6 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Paddiw rd rs n :: k) - | OEaddiwr0 n, nil => - do rd <- ireg_of res; - OK (Paddiw rd X0 n :: k) | OEandiw n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -879,9 +885,6 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Paddil rd rs n :: k) - | OEaddilr0 n, nil => - do rd <- ireg_of res; - OK (Paddil rd X0 n :: k) | OEandil n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 82c1917d..9a458b77 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -308,6 +308,7 @@ Opaque Int.eq. - apply opimm64_label; intros; exact I. - destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. - eapply transl_cond_op_label; eauto. +- destruct opi; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 639c9a64..6e5cc531 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1258,7 +1258,12 @@ Opaque Int.eq. { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) - 7,8,9,10,17,18,19,20: + { unfold get_opimmR0; destruct opi; simpl; + econstructor; split; try apply exec_straight_one; simpl; eauto; + split; intros; Simpl. + try rewrite Int.add_commut; auto. + try rewrite Int64.add_commut; auto. } + 7,8,9,16,17,18: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; try destruct (rs x0); try rewrite Int64.add_commut; diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 6eb82274..c03e0d03 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -117,7 +117,7 @@ let load_hilo64 dest hi lo succ map_consts not_final = let loadimm32 dest n succ map_consts not_final = match make_immed32 n with | Imm32_single imm -> - let op1 = OEaddiwr0 imm in + let op1 = OEimmR0 (OPimmADD imm) in let sv = find_or_addnmove op1 [] dest succ map_consts not_final in build_head_tuple [] sv | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts not_final @@ -125,7 +125,7 @@ let loadimm32 dest n succ map_consts not_final = let loadimm64 dest n succ map_consts not_final = match make_immed64 n with | Imm64_single imm -> - let op1 = OEaddilr0 imm in + let op1 = OEimmR0 (OPimmADDL imm) in let sv = find_or_addnmove op1 [] dest succ map_consts not_final in build_head_tuple [] sv | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts not_final diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index cfadea37..715951a0 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -87,6 +87,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) | Ocmp c => needs_of_condition c + | OEimmR0 _ => op1 (default nv) | OEseqw _ => op2 (default nv) | OEsnew _ => op2 (default nv) | OEsequw _ => op2 (default nv) @@ -98,7 +99,6 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OExoriw _ => op1 (bitwise nv) | OEluiw _ => op1 (default nv) | OEaddiw _ => op1 (default nv) - | OEaddiwr0 _ => op1 (default nv) | OEandiw n => op1 (andimm nv n) | OEoriw n => op1 (orimm nv n) | OEseql _ => op2 (default nv) @@ -112,7 +112,6 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OExoril _ => op1 (default nv) | OEluil _ => op1 (default nv) | OEaddil _ => op1 (default nv) - | OEaddilr0 _ => op1 (default nv) | OEandil _ => op1 (default nv) | OEoril _ => op1 (default nv) | OEloadli _ => op1 (default nv) diff --git a/riscV/Op.v b/riscV/Op.v index b8835c61..2ceffd4a 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -76,6 +76,11 @@ Inductive mayundef: Type := | MUshrx: int -> mayundef | MUshrxl: int -> mayundef. +(* This allow to have a single RTL constructor to perform an arith operation between an immediate and X0 *) +Inductive opimm: Type := + | OPimmADD: int -> opimm + | OPimmADDL: int64 -> opimm. + (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -179,6 +184,7 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) (* Expansed conditions *) + | OEimmR0 (opi: opimm) | OEseqw (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) | OEsnew (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) | OEsequw (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) @@ -188,7 +194,6 @@ Inductive operation : Type := | OEsltiw (n: int) (**r set-less-than immediate *) | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) | OEaddiw (n: int) (**r add immediate *) - | OEaddiwr0 (n: int) (**r add immediate *) | OEandiw (n: int) (**r and immediate *) | OEoriw (n: int) (**r or immediate *) | OExoriw (n: int) (**r xor immediate *) @@ -202,7 +207,6 @@ Inductive operation : Type := | OEsltil (n: int64) (**r set-less-than immediate *) | OEsltiul (n: int64) (**r set-less-than unsigned immediate *) | OEaddil (n: int64) (**r add immediate *) - | OEaddilr0 (n: int64) (**r add immediate *) | OEandil (n: int64) (**r and immediate *) | OEoril (n: int64) (**r or immediate *) | OExoril (n: int64) (**r xor immediate *) @@ -300,6 +304,12 @@ Definition eval_may_undef (mu: mayundef) (v1 v2: val): val := end end. +Definition eval_opimmR0 (opi: opimm): val := + match opi with + | OPimmADD i => Val.add (Vint i) zero32 + | OPimmADDL i => Val.addl (Vlong i) zero64 + end. + (** * Evaluation functions *) (** Evaluation of conditions, operators and addressing modes applied @@ -443,6 +453,7 @@ Definition eval_operation | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) (* Expansed conditions *) + | OEimmR0 opi, nil => Some (eval_opimmR0 opi) | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Ceq) v1 v2 zero32) | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Cne) v1 v2 zero32) | OEsequw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) @@ -454,7 +465,6 @@ Definition eval_operation | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n)) | OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12))) | OEaddiw n, v1::nil => Some (Val.add (Vint n) v1) - | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32) | OEandiw n, v1::nil => Some (Val.and (Vint n) v1) | OEoriw n, v1::nil => Some (Val.or (Vint n) v1) | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64)) @@ -468,7 +478,6 @@ Definition eval_operation | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n)) | OEluil n, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))) | OEaddil n, v1::nil => Some (Val.addl (Vlong n) v1) - | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64) | OEandil n, v1::nil => Some (Val.andl (Vlong n) v1) | OEoril n, v1::nil => Some (Val.orl (Vlong n) v1) | OEloadli n, nil => Some (Vlong n) @@ -557,6 +566,12 @@ Definition type_of_condition (c: condition) : list typ := | CEbgeul _ => Tlong :: Tlong :: nil end. +Definition type_of_opimmR0 (opi: opimm) : typ := + match opi with + | OPimmADD _ => Tint + | OPimmADDL _ => Tlong + end. + Definition type_of_operation (op: operation) : list typ * typ := match op with | Omove => (nil, Tint) (* treated specially *) @@ -652,6 +667,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoflong => (Tlong :: nil, Tsingle) | Osingleoflongu => (Tlong :: nil, Tsingle) | Ocmp c => (type_of_condition c, Tint) + | OEimmR0 opi => (nil, type_of_opimmR0 opi) | OEseqw _ => (Tint :: Tint :: nil, Tint) | OEsnew _ => (Tint :: Tint :: nil, Tint) | OEsequw _ => (Tint :: Tint :: nil, Tint) @@ -663,7 +679,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | OExoriw _ => (Tint :: nil, Tint) | OEluiw _ => (nil, Tint) | OEaddiw _ => (Tint :: nil, Tint) - | OEaddiwr0 _ => (nil, Tint) | OEandiw _ => (Tint :: nil, Tint) | OEoriw _ => (Tint :: nil, Tint) | OEseql _ => (Tlong :: Tlong :: nil, Tint) @@ -679,7 +694,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | OExoril _ => (Tlong :: nil, Tlong) | OEluil _ => (nil, Tlong) | OEaddil _ => (Tlong :: nil, Tlong) - | OEaddilr0 _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64) | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) @@ -907,6 +921,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; cbn; trivial. (* cmp *) - destruct (eval_condition cond vl m)... destruct b... + (* OEimmR0 *) + - destruct opi; unfold eval_opimmR0; simpl; auto. (* OEseqw *) - destruct optR0 as [[]|]; simpl; unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... @@ -932,8 +948,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... (* OEaddiw *) - fold (Val.add (Vint n) v0); apply type_add. - (* OEaddiwr0 *) - - trivial. (* OEandiw *) - destruct v0... (* OEoriw *) @@ -967,8 +981,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... (* OEaddil *) - fold (Val.addl (Vlong n) v0); apply type_addl. - (* OEaddilr0 *) - - trivial. (* OEandil *) - destruct v0... (* OEoril *) @@ -1769,6 +1781,8 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. + (* OEimmR0 *) + - destruct opi; unfold eval_opimmR0; simpl; auto. (* OEseqw *) - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index 3a775c20..9b3e8835 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -36,6 +36,10 @@ let mu_name pp = function | MUshrx i -> fprintf pp "MUshrx(%ld)" (camlint_of_coqint i) | MUshrxl i -> fprintf pp "MUshrxl(%ld)" (camlint_of_coqint i) +let get_immR0 pp = function + | OPimmADD i -> fprintf pp "OPimmADD(%ld)" (camlint_of_coqint i) + | OPimmADDL i -> fprintf pp "OPimmADDL(%ld)" (camlint_of_coqint i) + let get_optR0_s c reg pp r1 r2 = function | None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2 | Some true -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1 @@ -203,6 +207,7 @@ let print_operation reg pp = function | Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1 | Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1 | Ocmp c, args -> print_condition reg pp (c, args) + | OEimmR0 opi, [] -> fprintf pp "OEimmR0(%a)" get_immR0 opi | OEseqw optR0, [r1;r2] -> fprintf pp "OEseqw"; (get_optR0_s Ceq reg pp r1 r2 optR0) | OEsnew optR0, [r1;r2] -> fprintf pp "OEsnew"; (get_optR0_s Cne reg pp r1 r2 optR0) | OEsequw optR0, [r1;r2] -> fprintf pp "OEsequw"; (get_optR0_s Ceq reg pp r1 r2 optR0) @@ -214,7 +219,6 @@ let print_operation reg pp = function | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n) | OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n) - | OEaddiwr0 n, [] -> fprintf pp "OEaddiwr0(X0,%ld)" (camlint_of_coqint n) | OEandiw n, [r1] -> fprintf pp "OEandiw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEoriw n, [r1] -> fprintf pp "OEoriw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEseql optR0, [r1;r2] -> fprintf pp "OEseql"; (get_optR0_s Ceq reg pp r1 r2 optR0) @@ -228,7 +232,6 @@ let print_operation reg pp = function | OExoril n, [r1] -> fprintf pp "OExoril(%a,%ld)" reg r1 (camlint_of_coqint n) | OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n) | OEaddil n, [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n) - | OEaddilr0 n, [] -> fprintf pp "OEaddilr0(X0,%ld)" (camlint_of_coqint n) | OEandil n, [r1] -> fprintf pp "OEandil(%a,%ld)" reg r1 (camlint_of_coqint n) | OEoril n, [r1] -> fprintf pp "OEoril(%a,%ld)" reg r1 (camlint_of_coqint n) | OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n) diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 6066c7f5..08c1a6a0 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -50,14 +50,14 @@ Definition load_hilo64 (hi lo: int64) := Definition loadimm32 (n: int) := match make_immed32 n with | Imm32_single imm => - fSop (OEaddiwr0 imm) fSnil + fSop (OEimmR0 (OPimmADD imm)) fSnil | Imm32_pair hi lo => load_hilo32 hi lo end. Definition loadimm64 (n: int64) := match make_immed64 n with | Imm64_single imm => - fSop (OEaddilr0 imm) fSnil + fSop (OEimmR0 (OPimmADDL imm)) fSnil | Imm64_pair hi lo => load_hilo64 hi lo | Imm64_large imm => fSop (OEloadli imm) fSnil end. diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 82291f9c..b64040e1 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -51,6 +51,12 @@ Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := end end. +Definition eval_opimmR0 (opi: opimm): aval := + match opi with + | OPimmADD i => add (I i) zero32 + | OPimmADDL i => addl (L i) zero64 + end. + Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -220,6 +226,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) + | OEimmR0 opi, nil => eval_opimmR0 opi | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32) | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32) | OEsequw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32) @@ -231,7 +238,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OExoriw n, v1::nil => xor v1 (I n) | OEluiw n, nil => shl (I n) (I (Int.repr 12)) | OEaddiw n, v1::nil => add (I n) v1 - | OEaddiwr0 n, nil => add (I n) zero32 | OEandiw n, v1::nil => and (I n) v1 | OEoriw n, v1::nil => or (I n) v1 | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64) @@ -247,7 +253,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OExoril n, v1::nil => xorl v1 (L n) | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) | OEaddil n, v1::nil => addl (L n) v1 - | OEaddilr0 n, nil => addl (L n) zero64 | OEloadli n, nil => L (n) | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) @@ -472,36 +477,36 @@ Proof. destruct (propagate_float_constants tt); constructor. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. - + + unfold Op.eval_opimmR0, eval_opimmR0, Op.zero32, zero32, Op.zero64, zero64; + destruct opi; eauto with va. 3,4,6: apply eval_cmpu_sound; auto. 1,2,3: apply eval_cmp_sound; auto. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. { fold (Val.add (Vint n) a1); eauto with va. } - { unfold zero32; simpl; eauto with va. } { fold (Val.and (Vint n) a1); eauto with va. } { fold (Val.or (Vint n) a1); eauto with va. } { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; try apply vmatch_ifptr_undef. } 9: { fold (Val.addl (Vlong n) a1); eauto with va. } - 10: { fold (Val.andl (Vlong n) a1); eauto with va. } - 10: { fold (Val.orl (Vlong n) a1); eauto with va. } - 10: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; + 9: { fold (Val.andl (Vlong n) a1); eauto with va. } + 9: { fold (Val.orl (Vlong n) a1); eauto with va. } + 9: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; apply vmatch_ifptr_l. } 1,10: simpl; eauto with va. - 2: + 10: unfold Op.eval_may_undef, eval_may_undef; destruct mu; inv H1; inv H0; eauto with va; try destruct (Int.ltu _ _); simpl; try eapply vmatch_ifptr_p, pmatch_top'; eauto with va. - 3,4,6: apply eval_cmplu_sound; auto. - 1,2,3: apply eval_cmpl_sound; auto. - { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. } - { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. } - { unfold zero64; simpl; eauto with va. } + 4,5,7: apply eval_cmplu_sound; auto. + 1,3,4: apply eval_cmpl_sound; auto. + 2: { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. } + 2: { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. } all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. -- cgit