From 2638a022276c932ed00dc3f64b0e58bc0114a3d7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 20 Mar 2019 12:55:03 +0100 Subject: la division flottante fonctionne --- mppa_k1c/SelectOp.vp | 13 +++++++++++-- mppa_k1c/SelectOpproof.v | 16 ++++++++++++++++ 2 files changed, 27 insertions(+), 2 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 80eb641c..19712d2f 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -69,6 +69,8 @@ Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_defau Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default. +Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default. +Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default. Class helper_functions := mk_helper_functions { i64_dtos: ident; (**r float64 -> signed long *) @@ -90,6 +92,8 @@ Class helper_functions := mk_helper_functions { i32_udiv: ident; (**r unsigned division *) i32_smod: ident; (**r signed remainder *) i32_umod: ident; (**r unsigned remainder *) + f64_div: ident; (**float division*) + f32_div: ident; (**float division*) }. Context {hf: helper_functions}. @@ -537,6 +541,11 @@ Nondetfunction builtin_arg (e: expr) := (* float division *) -Definition divfbase (e1: expr) (e2: expr) := - Eop Odivf (e1 ::: e2 ::: Enil). +Definition divf_base (e1: expr) (e2: expr) := + (* Eop Odivf (e1 ::: e2 ::: Enil). *) + Eexternal f64_div sig_ff_f (e1 ::: e2 ::: Enil). + +Definition divfs_base (e1: expr) (e2: expr) := + (* Eop Odivf (e1 ::: e2 ::: Enil). *) + Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil). End SELECT. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 5a3f4521..ca6c342a 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -1070,4 +1070,20 @@ Proof. - constructor; auto. Qed. +(* floating-point division *) +Theorem eval_divf_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v. +Proof. +Admitted. + +Theorem eval_divfs_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v. +Proof. +Admitted. End CMCONSTR. -- cgit