From 780ad9d001af651a49d7470e963ed9a49ee11a4c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 19 Jul 2019 19:49:46 +0200 Subject: various fixes --- Makefile.extr | 2 +- backend/OpHelpersproof.v | 2 +- backend/Selectionproof.v | 6 +++--- backend/SplitLongproof.v | 20 -------------------- extraction/extraction.v | 1 + mppa_k1c/Asmexpand.ml | 4 ++-- mppa_k1c/CBuiltins.ml | 4 ++-- mppa_k1c/SelectOpproof.v | 15 +++++++++++++++ mppa_k1c/TargetPrinter.ml | 4 +++- powerpc/SelectOpproof.v | 1 - 10 files changed, 28 insertions(+), 31 deletions(-) diff --git a/Makefile.extr b/Makefile.extr index c903d6fd..51e9be59 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -49,7 +49,7 @@ INCLUDES=$(patsubst %,-I %, $(DIRS)) # Control of warnings: -WARNINGS=-w +a-4-9-27 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03 +WARNINGS=-w +a-4-9-27-42 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03 extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60 extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60 diff --git a/backend/OpHelpersproof.v b/backend/OpHelpersproof.v index 63040c5f..08da8a36 100644 --- a/backend/OpHelpersproof.v +++ b/backend/OpHelpersproof.v @@ -75,4 +75,4 @@ Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) /\ helper_declared p i32_umod "__compcert_i32_umod" sig_ii_i /\ helper_declared p f32_div "__compcert_f32_div" sig_ss_s /\ helper_declared p f64_div "__compcert_f64_div" sig_ff_f -. +. \ No newline at end of file diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 622992e5..8a827af2 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -1189,12 +1189,12 @@ Proof. (* store *) - unfold store. destruct (addressing m (sel_expr e)); simpl; auto. (* call *) - destruct (classify_call (prog_defmap cunit) e); simpl; auto. +- destruct (classify_call (prog_defmap cunit) e); simpl; auto. rewrite sel_builtin_nolabel; auto. (* tailcall *) - destruct (classify_call (prog_defmap cunit) e); simpl; auto. +- destruct (classify_call (prog_defmap cunit) e); simpl; auto. (* builtin *) - rewrite sel_builtin_nolabel; auto. +- rewrite sel_builtin_nolabel; auto. (* seq *) - exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index b13bd1f7..c8e3b94c 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -25,26 +25,6 @@ Local Open Scope string_scope. (** * Properties of the helper functions *) -Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := - (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))). - -Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) V) (hf: helper_functions) : Prop := - helper_declared p i64_dtos "__compcert_i64_dtos" sig_f_l - /\ helper_declared p i64_dtou "__compcert_i64_dtou" sig_f_l - /\ helper_declared p i64_stod "__compcert_i64_stod" sig_l_f - /\ helper_declared p i64_utod "__compcert_i64_utod" sig_l_f - /\ helper_declared p i64_stof "__compcert_i64_stof" sig_l_s - /\ helper_declared p i64_utof "__compcert_i64_utof" sig_l_s - /\ helper_declared p i64_sdiv "__compcert_i64_sdiv" sig_ll_l - /\ helper_declared p i64_udiv "__compcert_i64_udiv" sig_ll_l - /\ helper_declared p i64_smod "__compcert_i64_smod" sig_ll_l - /\ helper_declared p i64_umod "__compcert_i64_umod" sig_ll_l - /\ helper_declared p i64_shl "__compcert_i64_shl" sig_li_l - /\ helper_declared p i64_shr "__compcert_i64_shr" sig_li_l - /\ helper_declared p i64_sar "__compcert_i64_sar" sig_li_l - /\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l - /\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l. - (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. diff --git a/extraction/extraction.v b/extraction/extraction.v index caf4330b..e4c1cb25 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -34,6 +34,7 @@ Require Clight. Require Compiler. Require Parser. Require Initializers. +Require Asmaux. (* Standard lib *) Require Import ExtrOcamlBasic. diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index 65dee6c7..556fac9a 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -467,11 +467,11 @@ let expand_builtin_inline name args res = let open Asmvliw in emit (Pdzerol addr) | "__builtin_k1_afaddd", [BA(IR addr); BA (IR incr_res)], BR(IR res) -> (if res <> incr_res - then (emit (Pmv(res, incr_res)); emit Psemi)); + then (emit (Asm.Pmv(res, incr_res)); emit Psemi)); emit (Pafaddd(addr, res)) | "__builtin_k1_afaddw", [BA(IR addr); BA (IR incr_res)], BR(IR res) -> (if res <> incr_res - then (emit (Pmv(res, incr_res)); emit Psemi)); + then (emit (Asm.Pmv(res, incr_res)); emit Psemi)); emit (Pafaddw(addr, res)) | "__builtin_alclrd", [BA(IR addr)], BR(IR res) -> emit (Palclrd(res, addr)) diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index 2f80c90f..09a9ba97 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -18,11 +18,11 @@ open C let builtins = { - Builtins.typedefs = [ + builtin_typedefs = [ "__builtin_va_list", TPtr(TVoid [], []) ]; (* The builtin list is inspired from the GCC file builtin_k1.h *) - Builtins.functions = [ (* Some builtins are commented out because their opcode is not present (yet?) *) + builtin_functions = [ (* Some builtins are commented out because their opcode is not present (yet?) *) (* BCU Instructions *) "__builtin_k1_await", (TVoid [], [], false); (* DONE *) "__builtin_k1_barrier", (TVoid [], [], false); (* DONE *) diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 21a06857..e009ed98 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -17,6 +17,7 @@ (** Correctness of instruction selection for operators *) +Require Import Builtins. Require Import Coqlib. Require Import Maps. Require Import AST. @@ -29,6 +30,7 @@ Require Import Globalenvs. Require Import Cminor. Require Import Op. Require Import CminorSel. +Require Import Builtins1. Require Import SelectOp. Require Import Events. Require Import OpHelpers. @@ -1629,4 +1631,17 @@ Proof. intros; unfold divfs_base. econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. + +(** Platform-specific known builtins *) + +Theorem eval_platform_builtin: + forall bf al a vl v le, + platform_builtin bf al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem bf vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + intros. discriminate. +Qed. + End CMCONSTR. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 674695d9..dafad7fb 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -140,6 +140,8 @@ module Target (*: TARGET*) = | RA -> output_string oc "$ra" | _ -> assert false + let preg_asm oc ty = preg oc + let preg_annot = let open Asmvliw in function | IR r -> int_reg_name r | RA -> "$ra" @@ -324,7 +326,7 @@ module Target (*: TARGET*) = (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; + print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 63066135..b0cd70a4 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -1095,5 +1095,4 @@ Proof. intros. discriminate. Qed. ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf End CMCONSTR. -- cgit