From 7b0b080b118c097c84d5fb57a353cddf8c96b3ef Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 29 Apr 2019 14:44:24 +0200 Subject: rm unsupported int -> double signed/unsigned ops --- mppa_k1c/NeedOp.v | 2 +- mppa_k1c/Op.v | 12 ------------ mppa_k1c/PrintOp.ml | 2 -- mppa_k1c/ValueAOp.v | 2 -- 4 files changed, 1 insertion(+), 17 deletions(-) diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index abdcd94a..c10f5c56 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -112,7 +112,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Onegfs | Oabsfs => op1 (default nv) | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) | Ofloatofsingle | Osingleoffloat => op1 (default nv) - | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv) + | Ointoffloat | Ointuoffloat => op1 (default nv) | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => op1 (default nv) | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 093c8c17..baf17cc0 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -178,8 +178,6 @@ Inductive operation : Type := (*c Conversions between int and float: *) | Ointoffloat (**r [rd = signed_int_of_float64(r1)] *) | Ointuoffloat (**r [rd = unsigned_int_of_float64(r1)] *) - | Ofloatofint (**r [rd = float64_of_signed_int(r1)] *) - | Ofloatofintu (**r [rd = float64_of_unsigned_int(r1)] *) | Ointofsingle (**r [rd = signed_int_of_float32(r1)] *) | Ointuofsingle (**r [rd = unsigned_int_of_float32(r1)] *) | Osingleofint (**r [rd = float32_of_signed_int(r1)] *) @@ -485,8 +483,6 @@ Definition eval_operation | Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1) | Ointoffloat, v1::nil => Val.intoffloat v1 | Ointuoffloat, v1::nil => Val.intuoffloat v1 - | Ofloatofint, v1::nil => Val.floatofint v1 - | Ofloatofintu, v1::nil => Val.floatofintu v1 | Ointofsingle, v1::nil => Val.intofsingle v1 | Ointuofsingle, v1::nil => Val.intuofsingle v1 | Osingleofint, v1::nil => Val.singleofint v1 @@ -683,8 +679,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ofloatofsingle => (Tsingle :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) | Ointuoffloat => (Tfloat :: nil, Tint) - | Ofloatofint => (Tint :: nil, Tfloat) - | Ofloatofintu => (Tint :: nil, Tfloat) | Ointofsingle => (Tsingle :: nil, Tint) | Ointuofsingle => (Tsingle :: nil, Tint) | Osingleofint => (Tint :: nil, Tsingle) @@ -919,9 +913,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* intoffloat, intuoffloat *) - destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2... - destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2... - (* floatofint, floatofintu *) - - destruct v0; simpl in H0; inv H0... - - destruct v0; simpl in H0; inv H0... (* intofsingle, intuofsingle *) - destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); inv H2... - destruct v0; simpl in H0; inv H0. destruct (Float32.to_intu f); inv H2... @@ -1532,9 +1523,6 @@ Proof. exists (Vint i); auto. - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2. exists (Vint i); auto. - (* floatofint, floatofintu *) - - inv H4; simpl in H1; inv H1. simpl. TrivialExists. - - inv H4; simpl in H1; inv H1. simpl. TrivialExists. (* intofsingle, intuofsingle *) - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2. exists (Vint i); auto. diff --git a/mppa_k1c/PrintOp.ml b/mppa_k1c/PrintOp.ml index 5ac00404..4b833014 100644 --- a/mppa_k1c/PrintOp.ml +++ b/mppa_k1c/PrintOp.ml @@ -141,8 +141,6 @@ let print_operation reg pp = function | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1 - | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 - | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1 | Olongoffloat, [r1] -> fprintf pp "longoffloat(%a)" reg r1 | Olonguoffloat, [r1] -> fprintf pp "longuoffloat(%a)" reg r1 | Ofloatoflong, [r1] -> fprintf pp "floatoflong(%a)" reg r1 diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index fe8bddcf..064686cc 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -256,8 +256,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 | Ointuoffloat, v1::nil => intuoffloat v1 - | Ofloatofint, v1::nil => floatofint v1 - | Ofloatofintu, v1::nil => floatofintu v1 | Ointofsingle, v1::nil => intofsingle v1 | Ointuofsingle, v1::nil => intuofsingle v1 | Osingleofint, v1::nil => singleofint v1 -- cgit