From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/ValueAOp.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'powerpc/ValueAOp.v') diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index 77463f4b..a5a1db80 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -52,6 +52,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omove, v1::nil => v1 | Ointconst n, nil => I n | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop + | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) | Oaddrstack ofs, nil => Ptr (Stk ofs) | Ocast8signed, v1 :: nil => sign_ext 8 v1 @@ -92,7 +93,14 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osubf, v1::v2::nil => subf v1 v2 | Omulf, v1::v2::nil => mulf v1 v2 | Odivf, v1::v2::nil => divf v1 v2 + | Onegfs, v1::nil => negfs v1 + | Oabsfs, v1::nil => absfs v1 + | Oaddfs, v1::v2::nil => addfs v1 v2 + | Osubfs, v1::v2::nil => subfs v1 v2 + | Omulfs, v1::v2::nil => mulfs v1 v2 + | Odivfs, v1::v2::nil => divfs v1 v2 | Osingleoffloat, v1::nil => singleoffloat v1 + | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 | Ofloatofwords, v1::v2::nil => floatofwords v1 v2 | Omakelong, v1::v2::nil => longofwords v1 v2 @@ -163,6 +171,7 @@ Proof. unfold eval_operation, eval_static_operation; intros; destruct op; InvHyps; eauto with va. destruct (propagate_float_constants tt); constructor. + destruct (propagate_float_constants tt); constructor. rewrite Int.add_zero_l; eauto with va. fold (Val.sub (Vint i) a1). auto with va. apply floatofwords_sound; auto. -- cgit