diff options
author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-03-07 16:21:13 +0100 |
---|---|---|
committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-03-07 16:21:13 +0100 |
commit | 25e82e849de35eaef24412b468d3a36c72f4fcb6 (patch) | |
tree | e6abc778dfa37ac5df55c8b0926ed681b9c04f04 /backend | |
parent | ab776cd94e000d07c4d14521a8d0c635d3b8412c (diff) | |
parent | 2d9138547d93c32c0ec5ae54b4afc022f5c434ff (diff) | |
download | compcert-kvx-25e82e849de35eaef24412b468d3a36c72f4fcb6.tar.gz compcert-kvx-25e82e849de35eaef24412b468d3a36c72f4fcb6.zip |
Merge remote-tracking branch 'origin/kvx_fp_division' into kvx-work
Diffstat (limited to 'backend')
-rw-r--r-- | backend/ValueDomain.v | 156 |
1 files changed, 156 insertions, 0 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 7a55147b..fcc70ac8 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2269,6 +2269,24 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition intofsingle_ne (x: aval) := + match x with + | FS f => + match Float32.to_int_ne f with + | Some i => I i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma intofsingle_ne_sound: + forall v x w, vmatch v x -> Val.intofsingle_ne v = Some w -> vmatch w (intofsingle_ne x). +Proof. + unfold Val.intofsingle_ne; intros. destruct v; try discriminate. + destruct (Float32.to_int_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + Definition intuofsingle (x: aval) := match x with | FS f => @@ -2287,6 +2305,24 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition intuofsingle_ne (x: aval) := + match x with + | FS f => + match Float32.to_intu_ne f with + | Some i => I i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma intuofsingle_ne_sound: + forall v x w, vmatch v x -> Val.intuofsingle_ne v = Some w -> vmatch w (intuofsingle_ne x). +Proof. + unfold Val.intuofsingle_ne; intros. destruct v; try discriminate. + destruct (Float32.to_intu_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + Definition singleofint (x: aval) := match x with | I i => FS(Float32.of_int i) @@ -2349,6 +2385,42 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition longoffloat_ne (x: aval) := + match x with + | F f => + match Float.to_long_ne f with + | Some i => L i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma longoffloat_ne_sound: + forall v x w, vmatch v x -> Val.longoffloat_ne v = Some w -> vmatch w (longoffloat_ne x). +Proof. + unfold Val.longoffloat_ne; intros. destruct v; try discriminate. + destruct (Float.to_long_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + +Definition longuoffloat_ne (x: aval) := + match x with + | F f => + match Float.to_longu_ne f with + | Some i => L i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma longuoffloat_ne_sound: + forall v x w, vmatch v x -> Val.longuoffloat_ne v = Some w -> vmatch w (longuoffloat_ne x). +Proof. + unfold Val.longuoffloat_ne; intros. destruct v; try discriminate. + destruct (Float.to_longu_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + Definition floatoflong (x: aval) := match x with | L i => F(Float.of_long i) @@ -2566,6 +2638,46 @@ Definition longuofsingle_total (x: aval) := | _ => ntop1 x end. +Definition intofsingle_ne_total (x: aval) := + match x with + | FS f => + match Float32.to_int_ne f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition intuofsingle_ne_total (x: aval) := + match x with + | FS f => + match Float32.to_intu_ne f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longoffloat_ne_total (x: aval) := + match x with + | F f => + match Float.to_long_ne f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longuoffloat_ne_total (x: aval) := + match x with + | F f => + match Float.to_longu_ne f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + Lemma intoffloat_total_sound: forall v x (MATCH : vmatch v x), @@ -2606,6 +2718,26 @@ Proof. all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. Qed. +Lemma intofsingle_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.intofsingle_ne v)) (intofsingle_ne_total x). +Proof. + unfold Val.intofsingle_ne, intofsingle_ne_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_int_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + +Lemma intuofsingle_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.intuofsingle_ne v)) (intuofsingle_ne_total x). +Proof. + unfold Val.intofsingle, intofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_intu_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + Lemma singleofint_total_sound: forall v x, vmatch v x -> vmatch (Val.maketotal (Val.singleofint v)) (singleofint x). @@ -2648,6 +2780,26 @@ Proof. all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. Qed. +Lemma longoffloat_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.longoffloat_ne v)) (longoffloat_ne_total x). +Proof. + unfold Val.longoffloat_ne, longoffloat_ne_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_long_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + +Lemma longuoffloat_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.longuoffloat_ne v)) (longuoffloat_ne_total x). +Proof. + unfold Val.longoffloat_ne, longoffloat_ne_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_longu_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + Lemma longofsingle_total_sound: forall v x (MATCH : vmatch v x), @@ -5200,6 +5352,10 @@ Global Hint Resolve cnot_sound symbol_address_sound intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound longoffloat_sound longuoffloat_sound floatoflong_sound floatoflongu_sound longofsingle_sound longuofsingle_sound singleoflong_sound singleoflongu_sound + intofsingle_ne_sound intuofsingle_ne_sound + longoffloat_ne_sound longuoffloat_ne_sound + intofsingle_ne_total_sound intuofsingle_ne_total_sound + longoffloat_ne_total_sound longuoffloat_ne_total_sound longofwords_sound loword_sound hiword_sound intoffloat_total_sound intuoffloat_total_sound |