diff options
Diffstat (limited to 'riscV/ValueAOp.v')
| -rw-r--r-- | riscV/ValueAOp.v | 65 |
1 files changed, 56 insertions, 9 deletions
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index d50bd00f..fe519921 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -39,6 +39,32 @@ Definition may_undef_int (is_long: bool) (v1 v2: aval): aval := | _ => Ifptr Ptop end. +Definition shrx_imm_undef (v1 v2: aval): aval := + match v1 with + | I n1 => + match v2 with + | I n2 => + if Int.ltu n2 (Int.repr 31) + then I n1 + else Ifptr Ptop + | _ => Ifptr Ptop + end + | _ => Ifptr Ptop + end. + +Definition shrxl_imm_undef (v1 v2: aval): aval := + match v1 with + | L n1 => + match v2 with + | I n2 => + if Int.ltu n2 (Int.repr 63) + then L n1 + else Ifptr Ptop + | _ => Ifptr Ptop + end + | _ => Ifptr Ptop + 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 @@ -218,7 +244,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | 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) | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64) | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) @@ -227,11 +256,16 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) + | OEandil n, v1::nil => andl (L n) v1 + | OEoril n, v1::nil => orl (L n) v1 | 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 is_long, v1::v2::nil => may_undef_int is_long v1 v2 + | OEshrxundef n, v1::nil => shrx_imm_undef v1 (I n) + | OEshrxlundef n, v1::nil => shrxl_imm_undef v1 (I n) | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2) | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2) @@ -460,22 +494,35 @@ Proof. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. - simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; - try apply vmatch_ifptr_undef. - 10: - simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; - apply vmatch_ifptr_l. + { 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; + apply vmatch_ifptr_l. } + 1,10: simpl; eauto with va. - 9: + 2: unfold Op.may_undef_int, may_undef_int; destruct is_long; simpl; inv H0; inv H1; eauto with va; inv H; apply vmatch_ifptr_p; 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. + { 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. } + { unfold Op.shrx_imm_undef, shrx_imm_undef. + simpl; inv H1; eauto with va; + destruct (Int.ltu _ _); simpl; eauto with va. } + { unfold Op.shrxl_imm_undef, shrxl_imm_undef. + simpl; inv H1; eauto with va; + destruct (Int.ltu _ _); simpl; eauto with va. } all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. |