diff options
| -rw-r--r-- | backend/Selection.v | 36 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 28 | ||||
| -rw-r--r-- | mppa_k1c/Machregs.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/NeedOp.v | 44 | ||||
| -rw-r--r-- | test/monniaux/ternary_builtin/ternary_builtin.c | 16 |
6 files changed, 116 insertions, 14 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 5cfa3dcb..b9f5448c 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -276,6 +276,7 @@ Definition sel_builtin optid ef args := match ef with | EF_builtin name sign => (if String.string_dec name "__builtin_ternary_uint" + || String.string_dec name "__builtin_ternary_int" then match optid with | None => OK Sskip @@ -286,11 +287,12 @@ Definition sel_builtin optid ef args := ((sel_expr a3)::: (sel_expr a2)::: (sel_expr a1):::Enil))) - | _ => Error (msg "__builtin_ternary_ulong: arguments") + | _ => Error (msg "__builtin_ternary_(u)int: arguments") end end else if String.string_dec name "__builtin_ternary_ulong" + || String.string_dec name "__builtin_ternary_long" then match optid with | None => OK Sskip @@ -301,7 +303,37 @@ Definition sel_builtin optid ef args := ((sel_expr a3)::: (sel_expr a2)::: (sel_expr a1):::Enil))) - | _ => Error (msg "__builtin_ternary_uint: arguments") + | _ => Error (msg "__builtin_ternary_(u)long: arguments") + end + end + else + if String.string_dec name "__builtin_ternary_double" + then + match optid with + | None => OK Sskip + | Some id => + match args with + | a1::a2::a3::nil => + OK (Sassign id (Eop Oselectf + ((sel_expr a3)::: + (sel_expr a2)::: + (sel_expr a1):::Enil))) + | _ => Error (msg "__builtin_ternary_double: arguments") + end + end + else + if String.string_dec name "__builtin_ternary_float" + then + match optid with + | None => OK Sskip + | Some id => + match args with + | a1::a2::a3::nil => + OK (Sassign id (Eop Oselectfs + ((sel_expr a3)::: + (sel_expr a2)::: + (sel_expr a1):::Enil))) + | _ => Error (msg "__builtin_ternary_float: arguments") end end else diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c17ce75a..0f2e3674 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -188,6 +188,10 @@ let builtins_generic = { (* Ternary operator *) builtin_ternary "uint" (TInt(IUInt, [])); builtin_ternary "ulong" (TInt(IULong, [])); + builtin_ternary "int" (TInt(IInt, [])); + builtin_ternary "long" (TInt(ILong, [])); + builtin_ternary "double" (TFloat(FDouble, [])); + builtin_ternary "float" (TFloat(FFloat, [])); (* Annotations *) "__builtin_annot", diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 99ab1b91..f75f0bd3 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1665,6 +1665,34 @@ Opaque Int.eq. destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. +- (* Oselectf *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold selectl. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. +- (* Oselectfs *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold selectl. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. Qed. (** Memory accesses *) diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index f494c67d..f89f952f 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -209,7 +209,7 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect | Oselectl => true + | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect | Oselectl | Oselectf | Oselectfs => true | _ => false end. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index a6ecb820..f3ce8361 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -117,7 +117,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) | Ocmp c => needs_of_condition c - | Oselect | Oselectl => op3 (default nv) + | Oselect | Oselectl | Oselectf | Oselectfs => op3 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := @@ -227,6 +227,44 @@ Proof. constructor. Qed. +Lemma selectf_sound: + forall v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (selectf v0 v1 v2) (selectf w0 w1 w2) x. +Proof. + unfold default; intros. + destruct x; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + inv H. inv H0. inv H1. simpl. + constructor. +Qed. + +Lemma selectfs_sound: + forall v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (selectfs v0 v1 v2) (selectfs w0 w1 w2) x. +Proof. + unfold default; intros. + destruct x; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + inv H. inv H0. inv H1. simpl. + constructor. +Qed. + Remark default_idem: forall nv, default (default nv) = default nv. Proof. destruct nv; simpl; trivial. @@ -283,6 +321,10 @@ Proof. - apply select_sound; trivial. (* selectl *) - apply selectl_sound; trivial. + (* selectf *) +- apply selectf_sound; trivial. + (* selectfs *) +- apply selectfs_sound; trivial. Qed. Lemma operation_is_redundant_sound: diff --git a/test/monniaux/ternary_builtin/ternary_builtin.c b/test/monniaux/ternary_builtin/ternary_builtin.c index 1295581c..6ea456ab 100644 --- a/test/monniaux/ternary_builtin/ternary_builtin.c +++ b/test/monniaux/ternary_builtin/ternary_builtin.c @@ -1,14 +1,10 @@ #include <stdio.h> +#include <stdlib.h> -unsigned essai(int x, unsigned y, unsigned z) { - return __builtin_ternary_uint(x, y, z); -} - -unsigned long essai2(int x, unsigned long y, unsigned long z) { - return __builtin_ternary_ulong(x, y, z); -} - -int main() { - printf("%ld\n", essai2(0, 42, 69)); +int main(int argc, char **argv) { + int i=0; + if (argc >= 2) i=atoi(argv[1]); + printf("%ld\n", __builtin_ternary_int(i, 42, 69)); + printf("%f\n", __builtin_ternary_double(i, 42.0, 69.0)); return 0; } |