aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.extr2
-rw-r--r--backend/OpHelpersproof.v2
-rw-r--r--backend/Selectionproof.v6
-rw-r--r--backend/SplitLongproof.v20
-rw-r--r--extraction/extraction.v1
-rw-r--r--mppa_k1c/Asmexpand.ml4
-rw-r--r--mppa_k1c/CBuiltins.ml4
-rw-r--r--mppa_k1c/SelectOpproof.v15
-rw-r--r--mppa_k1c/TargetPrinter.ml4
-rw-r--r--powerpc/SelectOpproof.v1
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.
generated by cgit (git 2.34.1) at 2024-05-20 12:20:30 +0000