diff options
Diffstat (limited to 'backend/ValueDomain.v')
-rw-r--r-- | backend/ValueDomain.v | 244 |
1 files changed, 243 insertions, 1 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 779e7bb9..661d769d 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2069,7 +2069,6 @@ Definition divfs := binop_single Float32.div. Lemma divfs_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.divfs v w) (divfs x y). Proof (binop_single_sound Float32.div). - (** Conversions *) Definition zero_ext (nbits: Z) (v: aval) := @@ -2483,6 +2482,235 @@ Proof. destruct 1; simpl; auto with va. Qed. + +(* Extensions for KVX and Risc-V *) + +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. + +Lemma intoffloat_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (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]. +Qed. + +Lemma intuoffloat_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (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]. +Qed. + +Lemma intofsingle_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (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]. +Qed. + +Lemma intuofsingle_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (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]. +Qed. + +Lemma singleofint_total_sound: + forall v x, vmatch v x -> + vmatch (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. + +Lemma singleofintu_total_sound: + forall v x, vmatch v x -> + vmatch (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. + +Lemma longoffloat_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (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]. +Qed. + +Lemma longuoffloat_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (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]. +Qed. + +Lemma longofsingle_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (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]. +Qed. + +Lemma longuofsingle_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (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]. +Qed. + +Lemma singleoflong_total_sound: + forall v x, vmatch v x -> + vmatch (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. + +Lemma singleoflongu_total_sound: + forall v x, vmatch v x -> + vmatch (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. + +Lemma floatoflong_total_sound: + forall v x, vmatch v x -> + vmatch (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. + +Lemma floatoflongu_total_sound: + forall v x, vmatch v x -> + vmatch (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. + (** Comparisons and variation intervals *) Definition cmp_intv (c: comparison) (i: Z * Z) (n: Z) : abool := @@ -4734,6 +4962,20 @@ Hint Resolve cnot_sound symbol_address_sound longoffloat_sound longuoffloat_sound floatoflong_sound floatoflongu_sound longofsingle_sound longuofsingle_sound singleoflong_sound singleoflongu_sound longofwords_sound loword_sound hiword_sound + intoffloat_total_sound + intuoffloat_total_sound + intofsingle_total_sound + intuofsingle_total_sound + singleofint_total_sound + singleofintu_total_sound + longoffloat_total_sound + longuoffloat_total_sound + longofsingle_total_sound + longuofsingle_total_sound + singleoflong_total_sound + singleoflongu_total_sound + floatoflong_total_sound + floatoflongu_total_sound cmpu_bool_sound cmp_bool_sound cmplu_bool_sound cmpl_bool_sound cmpf_bool_sound cmpfs_bool_sound maskzero_sound : va. |