From 0fd96a8a96336b6032835eb58ad418f737a6e354 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 21 Sep 2020 21:22:26 +0200 Subject: moved some "total" value domain functions to a central location --- kvx/ValueAOp.v | 271 --------------------------------------------------------- 1 file changed, 271 deletions(-) (limited to 'kvx/ValueAOp.v') diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index e634fdc0..ed8de163 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -16,87 +16,6 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op ExtValues ExtFloats RTL ValueDomain. - -Definition intoffloat_total (x: aval) := - match x with - | F f => - match Float.to_int f with - | Some i => I i - | None => ntop - end - | _ => ntop1 x - end. - -Definition intuoffloat_total (x: aval) := - match x with - | F f => - match Float.to_intu f with - | Some i => I i - | None => ntop - end - | _ => ntop1 x - end. - -Definition intofsingle_total (x: aval) := - match x with - | FS f => - match Float32.to_int f with - | Some i => I i - | None => ntop - end - | _ => ntop1 x - end. - -Definition intuofsingle_total (x: aval) := - match x with - | FS f => - match Float32.to_intu f with - | Some i => I i - | None => ntop - end - | _ => ntop1 x - end. - -Definition longoffloat_total (x: aval) := - match x with - | F f => - match Float.to_long f with - | Some i => L i - | None => ntop - end - | _ => ntop1 x - end. - -Definition longuoffloat_total (x: aval) := - match x with - | F f => - match Float.to_longu f with - | Some i => L i - | None => ntop - end - | _ => ntop1 x - end. - -Definition longofsingle_total (x: aval) := - match x with - | FS f => - match Float32.to_long f with - | Some i => L i - | None => ntop - end - | _ => ntop1 x - end. - -Definition longuofsingle_total (x: aval) := - match x with - | FS f => - match Float32.to_longu f with - | Some i => L i - | None => ntop - end - | _ => ntop1 x - end. - Definition minf := binop_float ExtFloat.min. Definition maxf := binop_float ExtFloat.max. Definition minfs := binop_single ExtFloat32.min. @@ -400,196 +319,6 @@ Hypothesis GENV: genv_match bc ge. Variable sp: block. Hypothesis STACK: bc sp = BCstack. -Lemma intoffloat_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.intoffloat v)) (intoffloat_total x). -Proof. - unfold Val.intoffloat, intoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve intoffloat_total_sound : va. - -Lemma intuoffloat_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x). -Proof. - unfold Val.intoffloat, intoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve intuoffloat_total_sound : va. - -Lemma intofsingle_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.intofsingle v)) (intofsingle_total x). -Proof. - unfold Val.intofsingle, intofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve intofsingle_total_sound : va. - -Lemma intuofsingle_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x). -Proof. - unfold Val.intofsingle, intofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve intuofsingle_total_sound : va. - -Lemma singleofint_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.singleofint v)) (singleofint x). -Proof. - unfold Val.singleofint, singleofint; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve singleofint_total_sound : va. - -Lemma singleofintu_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.singleofintu v)) (singleofintu x). -Proof. - unfold Val.singleofintu, singleofintu; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve singleofintu_total_sound : va. - -Lemma longoffloat_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.longoffloat v)) (longoffloat_total x). -Proof. - unfold Val.longoffloat, longoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve longoffloat_total_sound : va. - -Lemma longuoffloat_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x). -Proof. - unfold Val.longoffloat, longoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve longuoffloat_total_sound : va. - -Lemma longofsingle_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.longofsingle v)) (longofsingle_total x). -Proof. - unfold Val.longofsingle, longofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve longofsingle_total_sound : va. - -Lemma longuofsingle_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x). -Proof. - unfold Val.longofsingle, longofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve longuofsingle_total_sound : va. - -Lemma singleoflong_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.singleoflong v)) (singleoflong x). -Proof. - unfold Val.singleoflong, singleoflong; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve singleoflong_total_sound : va. - -Lemma singleoflongu_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.singleoflongu v)) (singleoflongu x). -Proof. - unfold Val.singleoflongu, singleoflongu; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve singleoflongu_total_sound : va. - -Lemma floatoflong_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.floatoflong v)) (floatoflong x). -Proof. - unfold Val.floatoflong, floatoflong; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve floatoflong_total_sound : va. - -Lemma floatoflongu_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.floatoflongu v)) (floatoflongu x). -Proof. - unfold Val.floatoflongu, floatoflongu; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve floatoflongu_total_sound : va. - Lemma minf_sound: forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y). Proof. -- cgit