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 --- backend/ValueDomain.v | 215 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 215 insertions(+) (limited to 'backend/ValueDomain.v') 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. -- cgit