From 9c2c662a2a70545858d95b2f9f0a3625c506bc24 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 21 Sep 2020 21:37:16 +0200 Subject: moved Risc-V div ValueAOp to central location --- riscV/ValueAOp.v | 293 ------------------------------------------------------- 1 file changed, 293 deletions(-) (limited to 'riscV/ValueAOp.v') 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 := -- cgit