diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-21 21:37:16 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-21 21:37:16 +0200 |
commit | 9c2c662a2a70545858d95b2f9f0a3625c506bc24 (patch) | |
tree | d3241409a2d5d8f8d13739077993e40ddc3c0a9e | |
parent | 0fd96a8a96336b6032835eb58ad418f737a6e354 (diff) | |
download | compcert-kvx-9c2c662a2a70545858d95b2f9f0a3625c506bc24.tar.gz compcert-kvx-9c2c662a2a70545858d95b2f9f0a3625c506bc24.zip |
moved Risc-V div ValueAOp to central location
-rw-r--r-- | backend/ValueDomain.v | 215 | ||||
-rw-r--r-- | riscV/ValueAOp.v | 293 |
2 files changed, 215 insertions, 293 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 661d769d..81a52bab 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2711,6 +2711,217 @@ Proof. all: try constructor. Qed. + +Definition divs_total (v w: aval) := + match w, v with + | I i2, I i1 => + if Int.eq i2 Int.zero + || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone + then ntop + else I (Int.divs i1 i2) + | _, _ => ntop2 v w + end. + +Lemma divs_total_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.divs v w)) (divs_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + { destruct (_ || _) eqn:E; cbn; unfold ntop; auto with va. + } + all: unfold ntop2; auto with va. + all: destruct (_ || _) eqn:E; unfold ntop2; cbn; auto with va. +Qed. + +Definition divu_total (v w: aval) := + match w, v with + | I i2, I i1 => + if Int.eq i2 Int.zero + then ntop + else I (Int.divu i1 i2) + | _, _ => ntop2 v w + end. + +Lemma divu_total_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.divu v w)) (divu_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + { destruct Int.eq eqn:E; cbn; unfold ntop; auto with va. + } + all: unfold ntop2; auto with va. + all: destruct Int.eq eqn:E; unfold ntop2; cbn; auto with va. +Qed. + +Definition mods_total (v w: aval) := + match w, v with + | I i2, I i1 => + if Int.eq i2 Int.zero + || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone + then ntop + else I (Int.mods i1 i2) + | _, _ => ntop2 v w + end. + +Lemma mods_total_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.mods v w)) (mods_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + { destruct (_ || _) eqn:E; cbn; unfold ntop; auto with va. + } + all: unfold ntop2; auto with va. + all: destruct (_ || _) eqn:E; unfold ntop2; cbn; auto with va. +Qed. + +Definition modu_total (v w: aval) := + match w, v with + | I i2, I i1 => + if Int.eq i2 Int.zero + then ntop + else I (Int.modu i1 i2) + | I i2, _ => uns (provenance v) (usize i2) + | _, _ => ntop2 v w + end. + +Lemma modu_total_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.modu v w)) (modu_total x y). +Proof. + assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)). + { + intros. apply is_uns_mon with (usize (Int.modu i j)). + { apply is_uns_usize. + } + unfold usize, Int.size. + apply Zsize_monotone. + generalize (Int.unsigned_range_2 j); intros RANGE. + assert (Int.unsigned j <> 0). + { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. } + exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD. + unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. + } + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + { destruct Int.eq eqn:E; unfold ntop; cbn; auto with va. + } + all: try discriminate. + all: unfold ntop2; auto with va. + all: try (destruct Int.eq eqn:E; cbn; unfold ntop2; auto with va; fail). + all: try apply vmatch_uns_undef. + + all: + generalize (Int.eq_spec i0 Int.zero); + destruct (Int.eq i0 Int.zero); + cbn; + intro. + all: try apply vmatch_uns_undef. + all: apply vmatch_uns; auto. +Qed. + + +Lemma shrx_total_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.shrx v w)) (shrx x y). +Proof. + intros until y. intros HX HY. + inv HX; inv HY; cbn. + all: unfold ntop1; auto with va. + all: destruct Int.ltu eqn:LTU; cbn; unfold ntop; auto with va. +Qed. + + +Definition divls_total (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + || Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone + then ntop + else L (Int64.divs i1 i2) + | _, _ => ntop2 v w + end. + +Lemma divls_total_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.divls v w)) (divls_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + all: unfold ntop2; auto with va. + all: destruct (_ || _) eqn:E; unfold ntop2, ntop; cbn; auto with va. +Qed. + +Definition divlu_total (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + then ntop + else L (Int64.divu i1 i2) + | _, _ => ntop2 v w + end. + +Lemma divlu_total_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.divlu v w)) (divlu_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + all: unfold ntop2; auto with va. + all: destruct Int64.eq eqn:E; unfold ntop2, ntop; cbn; auto with va. +Qed. + + +Definition modls_total (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + || Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone + then ntop + else L (Int64.mods i1 i2) + | _, _ => ntop2 v w + end. + +Lemma modls_total_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.modls v w)) (modls_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + all: unfold ntop2; auto with va. + all: destruct (_ || _) eqn:E; unfold ntop2, ntop; cbn; auto with va. +Qed. + + +Definition modlu_total (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + then ntop + else L (Int64.modu i1 i2) + | _, _ => ntop2 v w + end. + +Lemma modlu_total_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.modlu v w)) (modlu_total x y). +Proof. + intros until y. + intros HX HY. + inv HX; inv HY; cbn in *. + all: unfold ntop2; auto with va. + all: destruct Int64.eq eqn:E; cbn; unfold ntop2, ntop; auto with va. +Qed. + +Lemma shrxl_total_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.shrxl v w)) (shrxl x y). +Proof. + intros until y. intros HX HY. + inv HX; inv HY; cbn. + all: unfold ntop1; auto with va. + all: destruct Int.ltu eqn:LTU; cbn; unfold ntop; auto with va. +Qed. + (** Comparisons and variation intervals *) Definition cmp_intv (c: comparison) (i: Z * Z) (n: Z) : abool := @@ -4976,6 +5187,10 @@ Hint Resolve cnot_sound symbol_address_sound singleoflongu_total_sound floatoflong_total_sound floatoflongu_total_sound + divu_total_sound divs_total_sound + modu_total_sound mods_total_sound shrx_total_sound + divlu_total_sound divls_total_sound + modlu_total_sound modls_total_sound shrxl_total_sound cmpu_bool_sound cmp_bool_sound cmplu_bool_sound cmpl_bool_sound cmpf_bool_sound cmpfs_bool_sound maskzero_sound : va. diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 5d1797ae..14b53db9 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -15,299 +15,6 @@ Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op RTL ValueDomain. Require Import Zbits. -Definition divs_total (v w: aval) := - match w, v with - | I i2, I i1 => - if Int.eq i2 Int.zero - || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone - then ntop - else I (Int.divs i1 i2) - | _, _ => ntop2 v w - end. - -Lemma divs_total_sound1: - forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.divs v w = Some u -> vmatch bc u (divs_total x y). -Proof. - intros until y. - intros HX HY VAL. - inv HX; inv HY; cbn in *. - { destruct (_ || _) eqn:E. - discriminate. - inv VAL. - auto with va. - } - all: try discriminate. - all: destruct (_ || _) eqn:E; inv VAL; unfold ntop2; auto with va. -Qed. - -Lemma divs_total_sound: - forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divs v w)) (divs_total x y). -Proof. - intros until y. - intros HX HY. - inv HX; inv HY; cbn in *. - { destruct (_ || _) eqn:E; cbn; unfold ntop; auto with va. - } - all: unfold ntop2; auto with va. - all: destruct (_ || _) eqn:E; unfold ntop2; cbn; auto with va. -Qed. - -Definition divu_total (v w: aval) := - match w, v with - | I i2, I i1 => - if Int.eq i2 Int.zero - then ntop - else I (Int.divu i1 i2) - | _, _ => ntop2 v w - end. - -Lemma divu_total_sound1: - forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.divu v w = Some u -> vmatch bc u (divu_total x y). -Proof. - intros until y. - intros HX HY VAL. - inv HX; inv HY; cbn in *. - { destruct Int.eq eqn:E. - discriminate. - inv VAL. - auto with va. - } - all: try discriminate. - all: destruct Int.eq eqn:E; inv VAL; unfold ntop2; auto with va. -Qed. - -Lemma divu_total_sound: - forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divu v w)) (divu_total x y). -Proof. - intros until y. - intros HX HY. - inv HX; inv HY; cbn in *. - { destruct Int.eq eqn:E; cbn; unfold ntop; auto with va. - } - all: unfold ntop2; auto with va. - all: destruct Int.eq eqn:E; unfold ntop2; cbn; auto with va. -Qed. - -Definition mods_total (v w: aval) := - match w, v with - | I i2, I i1 => - if Int.eq i2 Int.zero - || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone - then ntop - else I (Int.mods i1 i2) - | _, _ => ntop2 v w - end. - -Lemma mods_total_sound1: - forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.mods v w = Some u -> vmatch bc u (mods x y). -Proof. - intros until y. - intros HX HY VAL. - inv HX; inv HY; cbn in *. - { destruct (_ || _) eqn:E. - discriminate. - inv VAL. - auto with va. - } - all: try discriminate. - all: destruct (_ || _) eqn:E; inv VAL; unfold ntop2; auto with va. -Qed. - -Lemma mods_total_sound: - forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.mods v w)) (mods_total x y). -Proof. - intros until y. - intros HX HY. - inv HX; inv HY; cbn in *. - { destruct (_ || _) eqn:E; cbn; unfold ntop; auto with va. - } - all: unfold ntop2; auto with va. - all: destruct (_ || _) eqn:E; unfold ntop2; cbn; auto with va. -Qed. - -Definition modu_total (v w: aval) := - match w, v with - | I i2, I i1 => - if Int.eq i2 Int.zero - then ntop - else I (Int.modu i1 i2) - | I i2, _ => uns (provenance v) (usize i2) - | _, _ => ntop2 v w - end. - -Lemma modu_total_sound1: - forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.modu v w = Some u -> vmatch bc u (modu x y). -Proof. - assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)). - { - intros. apply is_uns_mon with (usize (Int.modu i j)). - { apply is_uns_usize. - } - unfold usize, Int.size. - apply Zsize_monotone. - generalize (Int.unsigned_range_2 j); intros RANGE. - assert (Int.unsigned j <> 0). - { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. } - exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD. - unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. - } - - intros until y. - intros HX HY VAL. - inv HX; inv HY; cbn in *. - { destruct Int.eq eqn:E. - discriminate. - inv VAL. - auto with va. - } - all: try discriminate. - all: destruct Int.eq eqn:E; inv VAL; unfold ntop2; auto with va. - - all: - apply vmatch_uns; - apply UNS; - generalize (Int.eq_spec i0 Int.zero); - rewrite E; - auto. -Qed. - -Lemma modu_total_sound: - forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.modu v w)) (modu_total x y). -Proof. - assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)). - { - intros. apply is_uns_mon with (usize (Int.modu i j)). - { apply is_uns_usize. - } - unfold usize, Int.size. - apply Zsize_monotone. - generalize (Int.unsigned_range_2 j); intros RANGE. - assert (Int.unsigned j <> 0). - { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. } - exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD. - unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. - } - intros until y. - intros HX HY. - inv HX; inv HY; cbn in *. - { destruct Int.eq eqn:E; unfold ntop; cbn; auto with va. - } - all: try discriminate. - all: unfold ntop2; auto with va. - all: try (destruct Int.eq eqn:E; cbn; unfold ntop2; auto with va; fail). - all: try apply vmatch_uns_undef. - - all: - generalize (Int.eq_spec i0 Int.zero); - destruct (Int.eq i0 Int.zero); - cbn; - intro. - all: try apply vmatch_uns_undef. - all: apply vmatch_uns; auto. -Qed. - - -Lemma shrx_total_sound: - forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.shrx v w)) (shrx x y). -Proof. - intros until y. intros HX HY. - inv HX; inv HY; cbn. - all: unfold ntop1; auto with va. - all: destruct Int.ltu eqn:LTU; cbn; unfold ntop; auto with va. -Qed. - - -Definition divls_total (v w: aval) := - match w, v with - | L i2, L i1 => - if Int64.eq i2 Int64.zero - || Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone - then ntop - else L (Int64.divs i1 i2) - | _, _ => ntop2 v w - end. - -Lemma divls_total_sound: - forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divls v w)) (divls_total x y). -Proof. - intros until y. - intros HX HY. - inv HX; inv HY; cbn in *. - all: unfold ntop2; auto with va. - all: destruct (_ || _) eqn:E; unfold ntop2, ntop; cbn; auto with va. -Qed. - -Definition divlu_total (v w: aval) := - match w, v with - | L i2, L i1 => - if Int64.eq i2 Int64.zero - then ntop - else L (Int64.divu i1 i2) - | _, _ => ntop2 v w - end. - -Lemma divlu_total_sound: - forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divlu v w)) (divlu_total x y). -Proof. - intros until y. - intros HX HY. - inv HX; inv HY; cbn in *. - all: unfold ntop2; auto with va. - all: destruct Int64.eq eqn:E; unfold ntop2, ntop; cbn; auto with va. -Qed. - - -Definition modls_total (v w: aval) := - match w, v with - | L i2, L i1 => - if Int64.eq i2 Int64.zero - || Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone - then ntop - else L (Int64.mods i1 i2) - | _, _ => ntop2 v w - end. - -Lemma modls_total_sound: - forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.modls v w)) (modls_total x y). -Proof. - intros until y. - intros HX HY. - inv HX; inv HY; cbn in *. - all: unfold ntop2; auto with va. - all: destruct (_ || _) eqn:E; unfold ntop2, ntop; cbn; auto with va. -Qed. - - -Definition modlu_total (v w: aval) := - match w, v with - | L i2, L i1 => - if Int64.eq i2 Int64.zero - then ntop - else L (Int64.modu i1 i2) - | _, _ => ntop2 v w - end. - -Lemma modlu_total_sound: - forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.modlu v w)) (modlu_total x y). -Proof. - intros until y. - intros HX HY. - inv HX; inv HY; cbn in *. - all: unfold ntop2; auto with va. - all: destruct Int64.eq eqn:E; cbn; unfold ntop2, ntop; auto with va. -Qed. - -Lemma shrxl_total_sound: - forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.shrxl v w)) (shrxl x y). -Proof. - intros until y. intros HX HY. - inv HX; inv HY; cbn. - all: unfold ntop1; auto with va. - all: destruct Int.ltu eqn:LTU; cbn; unfold ntop; auto with va. -Qed. - -Hint Resolve divu_total_sound divs_total_sound modu_total_sound mods_total_sound shrx_total_sound divlu_total_sound divls_total_sound modlu_total_sound modls_total_sound shrxl_total_sound : va. - (** Value analysis for RISC V operators *) Definition eval_static_condition (cond: condition) (vl: list aval): abool := |