diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-06 16:54:17 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-07 09:08:40 +0200 |
| commit | f92ca339e9d1851fa4d469cdc867bfe1719c42a1 (patch) | |
| tree | a452b98f72a802972217b2615f4ce983a88e2f89 /backend/ValueDomain.v | |
| parent | b3bfdc3655479f7f8f1c5e3a7571473a72b421cb (diff) | |
| download | compcert-f92ca339e9d1851fa4d469cdc867bfe1719c42a1.tar.gz compcert-f92ca339e9d1851fa4d469cdc867bfe1719c42a1.zip | |
x86: operators Ointoffloat and Ointofsingle are total
This matches the semantics of the corresponding machine instructions,
and will help with branchless code.
Diffstat (limited to 'backend/ValueDomain.v')
| -rw-r--r-- | backend/ValueDomain.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index f6afa836..7ad138cf 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2187,6 +2187,23 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +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. + +Lemma intoffloat_total_sound: + forall v x, vmatch v x -> vmatch (Val.maketotal (Val.intoffloat v)) (intoffloat_total x). +Proof. + unfold Val.maketotal, Val.intoffloat, intoffloat_total; intros. + inv H; auto with va; destruct (Float.to_int f); auto with va. +Qed. + Definition intuoffloat (x: aval) := match x with | F f => @@ -2249,6 +2266,23 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +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. + +Lemma intofsingle_total_sound: + forall v x, vmatch v x -> vmatch (Val.maketotal (Val.intofsingle v)) (intofsingle_total x). +Proof. + unfold Val.maketotal, Val.intofsingle, intofsingle_total; intros. + inv H; auto with va; destruct (Float32.to_int f); auto with va. +Qed. + Definition intuofsingle (x: aval) := match x with | FS f => @@ -4675,6 +4709,7 @@ Hint Resolve cnot_sound symbol_address_sound singleoffloat_sound floatofsingle_sound intoffloat_sound intuoffloat_sound floatofint_sound floatofintu_sound intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound + intoffloat_total_sound intofsingle_total_sound longoffloat_sound longuoffloat_sound floatoflong_sound floatoflongu_sound longofsingle_sound longuofsingle_sound singleoflong_sound singleoflongu_sound longofwords_sound loword_sound hiword_sound |