Commit cb93a301 authored by David Monniaux's avatar David Monniaux
Browse files

Merge github.com:AbsInt/CompCert into kvx-work

parents 23da7b35 b40aef6c
Pipeline #54778 failed with stage
in 254 minutes and 18 seconds
......@@ -970,9 +970,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pfmov rd r1 =>
Next (nextinstr (rs#rd <- (rs#r1))) m
| Pfmovimms rd f =>
Next (nextinstr (rs#rd <- (Vsingle f))) m
Next (nextinstr (rs#X16 <- Vundef #rd <- (Vsingle f))) m
| Pfmovimmd rd f =>
Next (nextinstr (rs#rd <- (Vfloat f))) m
Next (nextinstr (rs#X16 <- Vundef #rd <- (Vfloat f))) m
| Pfmovi S rd r1 =>
Next (nextinstr (rs#rd <- (float32_of_bits rs##r1))) m
| Pfmovi D rd r1 =>
......@@ -1097,7 +1097,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Vint n =>
match list_nth_z tbl (Int.unsigned n) with
| None => Stuck
| Some lbl => goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m
| Some lbl => goto_label f lbl (rs#X16 <- Vundef) m
end
| _ => Stuck
end
......@@ -1212,7 +1212,7 @@ Inductive step: state -> trace -> state -> Prop :=
external_call ef ge vargs m t vres m' ->
rs' = nextinstr
(set_res res vres
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
(undef_regs (IR X16 :: IR X30 :: map preg_of (destroyed_by_builtin ef)) rs)) ->
step (State rs m) t (State rs' m')
| exec_step_external:
forall b ef args res rs m t rs' m',
......
......@@ -868,13 +868,16 @@ Local Transparent destroyed_by_op.
econstructor; eauto.
instantiate (2 := tf); instantiate (1 := x).
unfold nextinstr. rewrite Pregmap.gss.
rewrite set_res_other. rewrite undef_regs_other_2.
rewrite set_res_other. rewrite undef_regs_other.
rewrite <- H1. simpl. econstructor; eauto.
eapply code_tail_next_int; eauto.
rewrite preg_notin_charact. intros. auto with asmgen.
simpl; intros. destruct H4. congruence. destruct H4. congruence.
exploit list_in_map_inv; eauto. intros (mr & U & V). subst.
auto with asmgen.
auto with asmgen.
apply agree_nextinstr. eapply agree_set_res; auto.
eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
eapply agree_undef_regs; eauto. intros.
simpl. rewrite undef_regs_other_2; auto. Simpl.
congruence.
Simpl.
......@@ -936,7 +939,7 @@ Local Transparent destroyed_by_op.
exploit functions_transl; eauto. intro FN.
generalize (transf_function_no_overflow _ _ H5); intro NOOV.
exploit find_label_goto_label. eauto. eauto.
instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef).
instantiate (2 := rs0#X16 <- Vundef).
Simpl. eauto.
eauto.
intros [tc' [rs' [A [B C]]]].
......
......@@ -696,7 +696,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pfsubd r1 r2 r3 =>
Next (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m
| Pflid r1 f =>
Next (nextinstr (rs#r1 <- (Vfloat f))) m
Next (nextinstr (rs#IR14 <- Vundef #r1 <- (Vfloat f))) m
| Pfcmpd r1 r2 =>
Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
| Pfcmpzd r1 =>
......@@ -923,7 +923,7 @@ Inductive step: state -> trace -> state -> Prop :=
external_call ef ge vargs m t vres m' ->
rs' = nextinstr
(set_res res vres
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
(undef_regs (IR IR14 :: map preg_of (destroyed_by_builtin ef)) rs)) ->
step (State rs m) t (State rs' m')
| exec_step_external:
forall b ef args res rs m t rs' m',
......
......@@ -761,13 +761,15 @@ Opaque loadind.
econstructor; eauto.
instantiate (2 := tf); instantiate (1 := x).
unfold nextinstr. rewrite Pregmap.gss.
rewrite set_res_other. rewrite undef_regs_other_2.
rewrite set_res_other. simpl. rewrite undef_regs_other_2.
rewrite Pregmap.gso by auto with asmgen.
rewrite <- H1. simpl. econstructor; eauto.
eapply code_tail_next_int; eauto.
rewrite preg_notin_charact. intros. auto with asmgen.
auto with asmgen.
apply agree_nextinstr. eapply agree_set_res; auto.
eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto.
eapply agree_undef_regs; eauto.
intros. simpl. rewrite undef_regs_other_2; auto. apply Pregmap.gso. auto with asmgen.
congruence.
- (* Mgoto *)
......
......@@ -490,6 +490,8 @@ let _ =
fatal_error no_loc "ambiguous '-o' option (multiple source files)";
if !num_input_files = 0 then
fatal_error no_loc "no input file";
if not !option_interp && !main_function_name <> "main" then
fatal_error no_loc "option '-main' requires option '-interp'";
let linker_args = time "Total compilation time" perform_actions () in
if not (nolink ()) && linker_args <> [] then begin
linker (output_filename_default "a.out") linker_args
......
......@@ -200,12 +200,9 @@ Inductive instruction : Type :=
| Pfadd: freg -> freg -> freg -> instruction (**r float addition *)
| Pfadds: freg -> freg -> freg -> instruction (**r float addition *)
| Pfcmpu: freg -> freg -> instruction (**r float comparison *)
| Pfcfi: freg -> ireg -> instruction (**r signed-int-to-float conversion (pseudo, PPC64) *)
| Pfcfl: freg -> ireg -> instruction (**r signed-long-to-float conversion (pseudo, PPC64) *)
| Pfcfiu: freg -> ireg -> instruction (**r unsigned-int-to-float conversion (pseudo, PPC64) *)
| Pfcfid: freg -> freg -> instruction (**r signed-long-to-float conversion (PPC64) *)
| Pfcti: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo) *)
| Pfctiu: ireg -> freg -> instruction (**r float-to-unsigned-int conversion, round towards 0 (pseudo, PPC64) *)
| Pfctid: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo, PPC64) *)
| Pfctidz: freg -> freg -> instruction (**r float-to-signed-long conversion, round towards 0 (PPC64) *)
| Pfctiw: freg -> freg -> instruction (**r float-to-signed-int conversion, round by default *)
......@@ -825,16 +822,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m
| Pfcmpu r1 r2 =>
Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
| Pfcfi rd r1 =>
Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m
| Pfcfl rd r1 =>
Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong rs#r1)))) m
| Pfcfiu rd r1 =>
Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m
| Pfcti rd r1 =>
Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m
| Pfctiu rd r1 =>
Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m
| Pfctid rd r1 =>
Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m
| Pfdiv rd r1 r2 =>
......@@ -1204,7 +1195,7 @@ Inductive step: state -> trace -> state -> Prop :=
external_call ef ge vargs m t vres m' ->
rs' = nextinstr
(set_res res vres
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
(undef_regs (IR GPR0 :: map preg_of (destroyed_by_builtin ef)) rs)) ->
step (State rs m) t (State rs' m')
| exec_step_external:
forall b ef args res rs m t rs' m',
......
......@@ -198,12 +198,9 @@ let pp_instructions pp ic =
| Pfadd (fr1,fr2,fr3) -> instruction pp "Pfadd" [Freg fr1; Freg fr2; Freg fr3]
| Pfadds (fr1,fr2,fr3) -> instruction pp "Pfadds" [Freg fr1; Freg fr2; Freg fr3]
| Pfcmpu (fr1,fr2) -> instruction pp "Pfcmpu" [Freg fr1; Freg fr2]
| Pfcfi (ir,fr)
| Pfcfl (ir,fr) -> assert false (* Should not occur *)
| Pfcfid (fr1,fr2) -> instruction pp "Pfcfid" [Freg fr1; Freg fr2]
| Pfcfiu _ (* Should not occur *)
| Pfcti _ (* Should not occur *)
| Pfctiu _ (* Should not occur *)
| Pfctid _ -> assert false (* Should not occur *)
| Pfctidz (fr1,fr2) -> instruction pp "Pfctidz" [Freg fr1; Freg fr2]
| Pfctiw (fr1,fr2) -> instruction pp "Pfctiw" [Freg fr1; Freg fr2]
......
......@@ -875,15 +875,6 @@ let expand_instruction instr =
emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz)))
else
emit (Plwz(GPR1, Cint ofs, GPR1))
| Pfcfi(r1, r2) ->
assert (Archi.ppc64);
emit (Pextsw(GPR0, r2));
emit (Pstdu(GPR0, Cint _m8, GPR1));
emit (Pcfi_adjust _8);
emit (Plfd(r1, Cint _0, GPR1));
emit (Pfcfid(r1, r1));
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
| Pfcfl(r1, r2) ->
assert (Archi.ppc64);
emit (Pstdu(r2, Cint _m8, GPR1));
......@@ -892,15 +883,6 @@ let expand_instruction instr =
emit (Pfcfid(r1, r1));
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
| Pfcfiu(r1, r2) ->
assert (Archi.ppc64);
emit (Prldicl(GPR0, r2, _0, _32));
emit (Pstdu(GPR0, Cint _m8, GPR1));
emit (Pcfi_adjust _8);
emit (Plfd(r1, Cint _0, GPR1));
emit (Pfcfid(r1, r1));
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
| Pfcti(r1, r2) ->
emit (Pfctiwz(FPR13, r2));
emit (Pstfdu(FPR13, Cint _m8, GPR1));
......@@ -908,14 +890,6 @@ let expand_instruction instr =
emit (Plwz(r1, Cint _4, GPR1));
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
| Pfctiu(r1, r2) ->
assert (Archi.ppc64);
emit (Pfctidz(FPR13, r2));
emit (Pstfdu(FPR13, Cint _m8, GPR1));
emit (Pcfi_adjust _8);
emit (Plwz(r1, Cint _4, GPR1));
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
| Pfctid(r1, r2) ->
assert (Archi.ppc64);
emit (Pfctidz(FPR13, r2));
......
......@@ -611,15 +611,6 @@ Definition transl_op
| Ointoffloat, a1 :: nil =>
do r1 <- freg_of a1; do r <- ireg_of res;
OK (Pfcti r r1 :: k)
| Ointuoffloat, a1 :: nil =>
do r1 <- freg_of a1; do r <- ireg_of res;
OK (Pfctiu r r1 :: k)
| Ofloatofint, a1 :: nil =>
do r1 <- ireg_of a1; do r <- freg_of res;
OK (Pfcfi r r1 :: k)
| Ofloatofintu, a1 :: nil =>
do r1 <- ireg_of a1; do r <- freg_of res;
OK (Pfcfiu r r1 :: k)
| Ofloatofwords, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res;
OK (Pfmake r r1 r2 :: k)
......
......@@ -789,16 +789,18 @@ Opaque loadind.
econstructor; eauto.
instantiate (2 := tf); instantiate (1 := x).
unfold nextinstr. rewrite Pregmap.gss.
rewrite set_res_other. rewrite undef_regs_other_2.
rewrite set_res_other. simpl. rewrite undef_regs_other_2.
rewrite Pregmap.gso by auto with asmgen.
rewrite <- H1. simpl. econstructor; eauto.
eapply code_tail_next_int; eauto.
rewrite preg_notin_charact. intros. auto with asmgen.
auto with asmgen.
apply agree_nextinstr. eapply agree_set_res; auto.
eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto.
eapply agree_undef_regs; eauto.
intros. simpl. rewrite undef_regs_other_2; auto. apply Pregmap.gso. auto with asmgen.
congruence.
intros. Simpl. rewrite set_res_other by auto.
rewrite undef_regs_other_2; auto with asmgen.
simpl. rewrite undef_regs_other_2; auto with asmgen.
- (* Mgoto *)
assert (f0 = f) by congruence. subst f0.
......
......@@ -1498,18 +1498,6 @@ Opaque Val.add.
rewrite H1; auto.
(* Ointoffloat *)
- replace v with (Val.maketotal (Val.intoffloat (rs x))).
TranslOpSimpl.
rewrite H1; auto.
(* Ointuoffloat *)
- replace v with (Val.maketotal (Val.intuoffloat (rs x))).
TranslOpSimpl.
rewrite H1; auto.
(* Ofloatofint *)
- replace v with (Val.maketotal (Val.floatofint (rs x))).
TranslOpSimpl.
rewrite H1; auto.
(* Ofloatofintu *)
- replace v with (Val.maketotal (Val.floatofintu (rs x))).
TranslOpSimpl.
rewrite H1; auto.
(* Ocmp *)
......
......@@ -166,7 +166,7 @@ Definition destroyed_by_op (op: operation): list mreg :=
| Ofloatconst _ => R12 :: nil
| Osingleconst _ => R12 :: nil
| Olongconst _ => R12 :: nil
| Ointoffloat | Ointuoffloat => F13 :: nil
| Ointoffloat => F13 :: nil
| Olongoffloat => F13 :: nil
| Oaddlimm _ => R12 :: nil
| Oandlimm _ => R12 :: nil
......
......@@ -61,7 +61,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Onegfs | Oabsfs => op1 (default nv)
| Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
| Osingleoffloat | Ofloatofsingle => op1 (default nv)
| Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv)
| Ointoffloat => op1 (default nv)
| Ofloatofwords | Omakelong => op2 (default nv)
| Olowlong | Ohighlong => op1 (default nv)
| Ocmp c => needs_of_condition c
......
......@@ -105,7 +105,7 @@ Inductive operation : Type :=
| Osubl: operation (**r [rd = r1 - r2] *)
| Onegl: operation (**r [rd = - r1] *)
| Omull: operation (**r [rd = r1 * r2] *)
| Omullhs: operation (**r [rd = high part of r1 * r2, signed] *)
| Omullhs: operation (**r [rd = high part of r1 * r2, signed] *)
| Omullhu: operation (**r [rd = high part of r1 * r2, unsigned] *)
| Odivl: operation (**r [rd = r1 / r2] (signed) *)
| Odivlu: operation (**r [rd = r1 / r2] (unsigned) *)
......@@ -141,9 +141,6 @@ Inductive operation : Type :=
| Ofloatofsingle: operation (**r [rd] is [r1] extended to double-precision float *)
(*c Conversions between int and float: *)
| Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *)
| Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] (PPC64 only) *)
| Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] (PPC64 only) *)
| Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] (PPC64 only *)
| Ofloatofwords: operation (**r [rd = float_of_words(r1,r2)] *)
(*c Manipulating 64-bit integers: *)
| Omakelong: operation (**r [rd = r1 << 32 | r2] *)
......@@ -299,9 +296,6 @@ Definition eval_operation
| Osingleoffloat, v1::nil => Some(Val.singleoffloat v1)
| 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
| Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2)
| Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2)
| Olowlong, v1::nil => Some(Val.loword v1)
......@@ -449,9 +443,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| Osingleoffloat => (Tfloat :: nil, Tsingle)
| Ofloatofsingle => (Tsingle :: nil, Tfloat)
| Ointoffloat => (Tfloat :: nil, Tint)
| Ointuoffloat => (Tfloat :: nil, Tint)
| Ofloatofint => (Tint :: nil, Tfloat)
| Ofloatofintu => (Tint :: nil, Tfloat)
| Ofloatofwords => (Tint :: Tint :: nil, Tfloat)
| Omakelong => (Tint :: Tint :: nil, Tlong)
| Olowlong => (Tlong :: nil, Tint)
......@@ -570,9 +561,6 @@ Proof with (try exact I; try reflexivity).
destruct v0...
destruct v0...
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...
destruct v0; simpl in H0; inv H0...
destruct v0; simpl in H0; inv H0...
destruct v0; destruct v1...
destruct v0; destruct v1...
destruct v0...
......@@ -1043,10 +1031,6 @@ Proof.
inv H4; simpl; auto.
inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2.
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.
inv H4; simpl in H1; inv H1; simpl. TrivialExists.
inv H4; simpl in H1; inv H1; simpl. TrivialExists.
inv H4; inv H2; simpl; auto.
inv H4; inv H2; simpl; auto.
inv H4; simpl; auto.
......
......@@ -468,7 +468,7 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
Definition intuoffloat (e: expr) :=
if Archi.ppc64 then
Eop Ointuoffloat (e ::: Enil)
Eop Olowlong (Eop Olongoffloat (e ::: Enil) ::: Enil)
else
Elet e
(Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
......@@ -482,7 +482,8 @@ Nondetfunction floatofintu (e: expr) :=
Eop (Ofloatconst (Float.of_intu n)) Enil
| _ =>
if Archi.ppc64 then
Eop Ofloatofintu (e ::: Enil) else
Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil)
else
subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
(Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
end.
......@@ -493,7 +494,8 @@ Nondetfunction floatofint (e: expr) :=
Eop (Ofloatconst (Float.of_int n)) Enil
| _ =>
if Archi.ppc64 then
Eop Ofloatofint (e ::: Enil) else
Eop Ofloatoflong (Eop Ocast32signed (e ::: Enil) ::: Enil)
else
subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
::: addimm Float.ox8000_0000 e ::: Enil))
(Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil)
......
......@@ -855,8 +855,13 @@ Proof.
destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0.
exists (Vint n); split; auto. unfold intuoffloat.
destruct Archi.ppc64.
econstructor. constructor; eauto. constructor. simpl; rewrite Heqo; auto.
set (im := Int.repr Int.half_modulus).
- apply Float.to_intu_to_long in Heqo.
econstructor. constructor. econstructor. econstructor; eauto. constructor.
simpl; rewrite Heqo; simpl; eauto. constructor.
simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned. auto.
assert (Int.modulus < Int64.max_unsigned) by (compute; auto).
generalize (Int.unsigned_range n). omega.
- set (im := Int.repr Int.half_modulus).
set (fm := Float.of_intu im).
assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)).
constructor. auto.
......@@ -893,11 +898,12 @@ Theorem eval_floatofint:
Proof.
intros until y. unfold floatofint. destruct (floatofint_match a); intros.
InvEval. TrivialExists.
destruct Archi.ppc64.
TrivialExists.
rename e0 into a. destruct x; simpl in H0; inv H0.
exists (Vfloat (Float.of_int i)); split; auto.
set (t1 := addimm Float.ox8000_0000 a).
destruct Archi.ppc64.
- rewrite Float.of_int_of_long.
EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto.
- set (t1 := addimm Float.ox8000_0000 a).
set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)).
set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1.
......@@ -917,12 +923,12 @@ Theorem eval_floatofintu:
Proof.
intros until y. unfold floatofintu. destruct (floatofintu_match a); intros.
InvEval. TrivialExists.
destruct Archi.ppc64.
TrivialExists.
rename e0 into a. destruct x; simpl in H0; inv H0.
exists (Vfloat (Float.of_intu i)); split; auto.
unfold floatofintu.
set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
destruct Archi.ppc64.
- rewrite Float.of_intu_of_long.
EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto.
- set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
exploit (eval_subf le t2).
unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor.
......
......@@ -557,22 +557,16 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3
| Pfcmpu(r1, r2) ->
fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2
| Pfcfi(r1, r2) ->
assert false
| Pfcfl(r1, r2) ->
assert false
| Pfcfid(r1, r2) ->
fprintf oc " fcfid %a, %a\n" freg r1 freg r2
| Pfcfiu(r1, r2) ->
assert false
| Pfcti(r1, r2) ->
assert false
| Pfctid(r1, r2) ->
assert false
| Pfctidz(r1, r2) ->
fprintf oc " fctidz %a, %a\n" freg r1 freg r2
| Pfctiu(r1, r2) ->
assert false
| Pfctiw(r1, r2) ->
fprintf oc " fctiw %a, %a\n" freg r1 freg r2
| Pfctiwz(r1, r2) ->
......
......@@ -133,9 +133,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
| Osingleoffloat, v1::nil => singleoffloat v1
| 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
| Ofloatofwords, v1::v2::nil => floatofwords v1 v2
| Omakelong, v1::v2::nil => longofwords v1 v2
| Olowlong, v1::nil => loword v1
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment