diff options
| -rw-r--r-- | backend/SelectDiv.vp | 8 | ||||
| -rw-r--r-- | backend/SelectDivproof.v | 8 | ||||
| -rw-r--r-- | backend/Selection.v | 5 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 18 | ||||
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 13 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 16 | ||||
| -rw-r--r-- | runtime/mppa_k1c/Makefile | 3 | ||||
| -rw-r--r-- | runtime/mppa_k1c/i64_sdiv.c | 10 |
8 files changed, 67 insertions, 14 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 662162e8..7241d028 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -316,25 +316,25 @@ Definition modls (e1 e2: expr) := Definition divfimm (e: expr) (n: float) := match Float.exact_inverse n with | Some n' => Eop Omulf (e ::: Eop (Ofloatconst n') Enil ::: Enil) - | None => divfbase e (Eop (Ofloatconst n) Enil) + | None => divf_base e (Eop (Ofloatconst n) Enil) end. Nondetfunction divf (e1: expr) (e2: expr) := match e2 with | Eop (Ofloatconst n2) Enil => divfimm e1 n2 - | _ => divfbase e1 e2 + | _ => divf_base e1 e2 end. Definition divfsimm (e: expr) (n: float32) := match Float32.exact_inverse n with | Some n' => Eop Omulfs (e ::: Eop (Osingleconst n') Enil ::: Enil) - | None => Eop Odivfs (e ::: Eop (Osingleconst n) Enil ::: Enil) + | None => divfs_base e (Eop (Osingleconst n) Enil) end. Nondetfunction divfs (e1: expr) (e2: expr) := match e2 with | Eop (Osingleconst n2) Enil => divfsimm e1 n2 - | _ => Eop Odivfs (e1 ::: e2 ::: Enil) + | _ => divfs_base e1 e2 end. End SELECT.
\ No newline at end of file diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 9b99fcbf..dbd3f58d 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -949,8 +949,8 @@ Proof. EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. simpl; eauto. destruct x; simpl; auto. erewrite Float.div_mul_inverse; eauto. - + TrivialExists. -- TrivialExists. + + apply eval_divf_base; trivial. +- apply eval_divf_base; trivial. Qed. Theorem eval_divfs: @@ -965,8 +965,8 @@ Proof. EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. simpl; eauto. destruct x; simpl; auto. erewrite Float32.div_mul_inverse; eauto. - + TrivialExists. -- TrivialExists. + + apply eval_divfs_base; trivial. +- apply eval_divfs_base; trivial. Qed. End CMCONSTRS. diff --git a/backend/Selection.v b/backend/Selection.v index fc9315dc..aba84049 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -395,12 +395,15 @@ Definition get_helpers (defmap: PTree.t globdef) : res helper_functions := do i32_udiv <- lookup_helper globs "__compcert_i32_udiv" sig_ii_i ; do i32_smod <- lookup_helper globs "__compcert_i32_smod" sig_ii_i ; do i32_umod <- lookup_helper globs "__compcert_i32_umod" sig_ii_i ; + do f64_div <- lookup_helper globs "__compcert_f64_div" sig_ff_f ; + do f32_div <- lookup_helper globs "__compcert_f32_div" sig_ss_s ; OK (mk_helper_functions i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof i64_sdiv i64_udiv i64_smod i64_umod i64_shl i64_shr i64_sar i64_umulh i64_smulh - i32_sdiv i32_udiv i32_smod i32_umod). + i32_sdiv i32_udiv i32_smod i32_umod + f64_div f32_div). (** Conversion of programs. *) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index f0ae4367..bd9b7487 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -311,6 +311,14 @@ let builtins_generic = { (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); + "__compcert_f32_div", + (TFloat(FFloat,[]), + [TFloat(FFloat,[]); TFloat(FFloat,[])], + false); + "__compcert_f64_div", + (TFloat(FDouble,[]), + [TFloat(FDouble,[]); TFloat(FDouble,[])], + false); ] } @@ -1214,7 +1222,10 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" -let re_runtime = Str.regexp "__compcert_i" +let re_runtime64 = Str.regexp "__compcert_i64" +let re_runtime32 = Str.regexp "__compcert_i32" +let re_runtimef32 = Str.regexp "__compcert_f32" +let re_runtimef64 = Str.regexp "__compcert_f64" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = @@ -1227,7 +1238,10 @@ let convertFundecl env (sto, id, ty, optinit) = let ef = if id.name = "malloc" then AST.EF_malloc else if id.name = "free" then AST.EF_free else - if Str.string_match re_runtime id.name 0 + if Str.string_match re_runtime64 id.name 0 + || Str.string_match re_runtime32 id.name 0 + || Str.string_match re_runtimef64 id.name 0 + || Str.string_match re_runtimef32 id.name 0 then AST.EF_runtime(id'', sg) else if Str.string_match re_builtin id.name 0 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. diff --git a/runtime/mppa_k1c/Makefile b/runtime/mppa_k1c/Makefile index 9f2ba980..4e47f567 100644 --- a/runtime/mppa_k1c/Makefile +++ b/runtime/mppa_k1c/Makefile @@ -11,4 +11,5 @@ all: $(SFILES) .SECONDARY: %.s: %.c $(CCOMPPATH) $(CCOMP) $(CFLAGS) -S $< -o $@ - sed -i -e 's/i64_/__compcert_i64_/g' -e 's/i32_/__compcert_i32_/g' $@ + sed -i -e 's/i64_/__compcert_i64_/g' -e 's/i32_/__compcert_i32_/g' \ + -e 's/f64_/__compcert_f64_/g' -e 's/f32_/__compcert_f32_/g' $@ diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c index e312f6e8..0b281d3e 100644 --- a/runtime/mppa_k1c/i64_sdiv.c +++ b/runtime/mppa_k1c/i64_sdiv.c @@ -40,4 +40,14 @@ int i32_sdiv (int a, int b) { return __divdi3 (a, b); } + +extern double __divdf3(double, double); +double f64_div(double a, double b) { + return __divdf3(a, b); +} + +extern float __divsf3(float, float); +float f32_div(float a, float b) { + return __divsf3(a, b); +} #endif |