From cae21e8816db863bf99f87469c9680e150d28960 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 21 Sep 2020 09:17:05 +0200 Subject: maketotal mod & div --- riscV/ValueAOp.v | 310 +++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 302 insertions(+), 8 deletions(-) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 5670b5fe..5d1797ae 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -13,6 +13,300 @@ Require Import Coqlib Compopts. 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 *) @@ -59,10 +353,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omul, v1::v2::nil => mul v1 v2 | Omulhs, v1::v2::nil => mulhs v1 v2 | Omulhu, v1::v2::nil => mulhu v1 v2 - | Odiv, v1::v2::nil => divs v1 v2 - | Odivu, v1::v2::nil => divu v1 v2 - | Omod, v1::v2::nil => mods v1 v2 - | Omodu, v1::v2::nil => modu v1 v2 + | Odiv, v1::v2::nil => divs_total v1 v2 + | Odivu, v1::v2::nil => divu_total v1 v2 + | Omod, v1::v2::nil => mods_total v1 v2 + | Omodu, v1::v2::nil => modu_total v1 v2 | Oand, v1::v2::nil => and v1 v2 | Oandimm n, v1::nil => and v1 (I n) | Oor, v1::v2::nil => or v1 v2 @@ -88,10 +382,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omull, v1::v2::nil => mull v1 v2 | Omullhs, v1::v2::nil => mullhs v1 v2 | Omullhu, v1::v2::nil => mullhu v1 v2 - | Odivl, v1::v2::nil => divls v1 v2 - | Odivlu, v1::v2::nil => divlu v1 v2 - | Omodl, v1::v2::nil => modls v1 v2 - | Omodlu, v1::v2::nil => modlu v1 v2 + | Odivl, v1::v2::nil => divls_total v1 v2 + | Odivlu, v1::v2::nil => divlu_total v1 v2 + | Omodl, v1::v2::nil => modls_total v1 v2 + | Omodlu, v1::v2::nil => modlu_total v1 v2 | Oandl, v1::v2::nil => andl v1 v2 | Oandlimm n, v1::nil => andl v1 (L n) | Oorl, v1::v2::nil => orl v1 v2 -- cgit