diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-02 19:49:30 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-02 19:49:30 +0100 |
commit | f0c1cc8327ecf2b1e3021bce66f2d6bb0265f6c0 (patch) | |
tree | 6d5c6988ad68cfe7052dc6dac267c4de53f0202b | |
parent | be3d241a0c2247f48dab2988f49e9c651417328b (diff) | |
parent | eaea751c200213e0f86cf51c1fe93b7ba09c4227 (diff) | |
download | compcert-kvx-f0c1cc8327ecf2b1e3021bce66f2d6bb0265f6c0.tar.gz compcert-kvx-f0c1cc8327ecf2b1e3021bce66f2d6bb0265f6c0.zip |
Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load
53 files changed, 1855 insertions, 601 deletions
@@ -45,15 +45,12 @@ /riscV/ConstpropOp.v /riscV/SelectOp.v /riscV/SelectLong.v -<<<<<<< HEAD /mppa_k1c/ConstpropOp.v /mppa_k1c/SelectOp.v /mppa_k1c/SelectLong.v -======= /aarch64/ConstpropOp.v /aarch64/SelectOp.v /aarch64/SelectLong.v ->>>>>>> e1725209b2b4401adc63ce5238fa5db7c134609c /backend/SelectDiv.v /backend/SplitLong.v /cparser/Parser.v @@ -80,6 +80,7 @@ BACKEND=\ Tailcall.v Tailcallproof.v \ Inlining.v Inliningspec.v Inliningproof.v \ Renumber.v Renumberproof.v \ + Duplicate.v Duplicateproof.v \ RTLtyping.v \ Kildall.v Liveness.v \ ValueDomain.v ValueAOp.v ValueAnalysis.v \ diff --git a/backend/Duplicate.v b/backend/Duplicate.v new file mode 100644 index 00000000..3ad37c83 --- /dev/null +++ b/backend/Duplicate.v @@ -0,0 +1,198 @@ +(** RTL node duplication using external oracle. Used to form superblock + structures *) + +Require Import AST RTL Maps Globalenvs. +Require Import Coqlib Errors Op. + +Local Open Scope error_monad_scope. +Local Open Scope positive_scope. + +(** External oracle returning the new RTL code (entry point unchanged), + along with the new entrypoint, and a mapping of new nodes to old nodes *) +Axiom duplicate_aux: function -> code * node * (PTree.t node). + +Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux". + +(** * Verification of node duplications *) + +Definition verify_is_copy dupmap n n' := + match dupmap!n' with + | None => Error(msg "verify_is_copy None") + | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end + end. + +Fixpoint verify_is_copy_list dupmap ln ln' := + match ln with + | n::ln => match ln' with + | n'::ln' => do u <- verify_is_copy dupmap n n'; + verify_is_copy_list dupmap ln ln' + | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end + | nil => match ln' with + | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") + | nil => OK tt end + end. + +Definition verify_mapping_entrypoint dupmap (f f': function): res unit := + verify_is_copy dupmap (fn_entrypoint f) (fn_entrypoint f'). + +Lemma product_eq {A B: Type} : + (forall (a b: A), {a=b} + {a<>b}) -> + (forall (c d: B), {c=d} + {c<>d}) -> + forall (x y: A+B), {x=y} + {x<>y}. +Proof. + intros H H'. intros. decide equality. +Qed. + +(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application" + * error when doing so *) +Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}. +Proof. + intros. + apply (builtin_arg_eq Pos.eq_dec). +Defined. +Global Opaque builtin_arg_eq_pos. + +Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}. +Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed. +Global Opaque builtin_res_eq_pos. + +Definition verify_match_inst dupmap inst tinst := + match inst with + | Inop n => match tinst with Inop n' => do u <- verify_is_copy dupmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end + + | Iop op lr r n => match tinst with + Iop op' lr' r' n' => + do u <- verify_is_copy dupmap n n'; + if (eq_operation op op') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then + OK tt + else Error (msg "Different r in Iop") + else Error (msg "Different lr in Iop") + else Error(msg "Different operations in Iop") + | _ => Error(msg "verify_match_inst Inop") end + + | Iload m a lr r n => match tinst with + | Iload m' a' lr' r' n' => + do u <- verify_is_copy dupmap n n'; + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r in Iload") + else Error (msg "Different lr in Iload") + else Error (msg "Different addressing in Iload") + else Error (msg "Different mchunk in Iload") + | _ => Error (msg "verify_match_inst Iload") end + + | Istore m a lr r n => match tinst with + | Istore m' a' lr' r' n' => + do u <- verify_is_copy dupmap n n'; + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r in Istore") + else Error (msg "Different lr in Istore") + else Error (msg "Different addressing in Istore") + else Error (msg "Different mchunk in Istore") + | _ => Error (msg "verify_match_inst Istore") end + + | Icall s ri lr r n => match tinst with + | Icall s' ri' lr' r' n' => + do u <- verify_is_copy dupmap n n'; + if (signature_eq s s') then + if (product_eq Pos.eq_dec ident_eq ri ri') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r r' in Icall") + else Error (msg "Different lr in Icall") + else Error (msg "Different ri in Icall") + else Error (msg "Different signatures in Icall") + | _ => Error (msg "verify_match_inst Icall") end + + | Itailcall s ri lr => match tinst with + | Itailcall s' ri' lr' => + if (signature_eq s s') then + if (product_eq Pos.eq_dec ident_eq ri ri') then + if (list_eq_dec Pos.eq_dec lr lr') then OK tt + else Error (msg "Different lr in Itailcall") + else Error (msg "Different ri in Itailcall") + else Error (msg "Different signatures in Itailcall") + | _ => Error (msg "verify_match_inst Itailcall") end + + | Ibuiltin ef lbar brr n => match tinst with + | Ibuiltin ef' lbar' brr' n' => + do u <- verify_is_copy dupmap n n'; + if (external_function_eq ef ef') then + if (list_eq_dec builtin_arg_eq_pos lbar lbar') then + if (builtin_res_eq_pos brr brr') then OK tt + else Error (msg "Different brr in Ibuiltin") + else Error (msg "Different lbar in Ibuiltin") + else Error (msg "Different ef in Ibuiltin") + | _ => Error (msg "verify_match_inst Ibuiltin") end + + | Icond cond lr n1 n2 => match tinst with + | Icond cond' lr' n1' n2' => + do u1 <- verify_is_copy dupmap n1 n1'; + do u2 <- verify_is_copy dupmap n2 n2'; + if (eq_condition cond cond') then + if (list_eq_dec Pos.eq_dec lr lr') then OK tt + else Error (msg "Different lr in Icond") + else Error (msg "Different cond in Icond") + | _ => Error (msg "verify_match_inst Icond") end + + | Ijumptable r ln => match tinst with + | Ijumptable r' ln' => + do u <- verify_is_copy_list dupmap ln ln'; + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r in Ijumptable") + | _ => Error (msg "verify_match_inst Ijumptable") end + + | Ireturn or => match tinst with + | Ireturn or' => + if (option_eq Pos.eq_dec or or') then OK tt + else Error (msg "Different or in Ireturn") + | _ => Error (msg "verify_match_inst Ireturn") end + end. + +Definition verify_mapping_mn dupmap f f' (m: positive*positive) := + let (tn, n) := m in + match (fn_code f)!n with + | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code f)!n") + | Some inst => match (fn_code f')!tn with + | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code xf)!tn") + | Some tinst => verify_match_inst dupmap inst tinst + end + end. + +Fixpoint verify_mapping_mn_rec dupmap f f' lm := + match lm with + | nil => OK tt + | m :: lm => do u <- verify_mapping_mn dupmap f f' m; + do u2 <- verify_mapping_mn_rec dupmap f f' lm; + OK tt + end. + +Definition verify_mapping_match_nodes dupmap (f f': function): res unit := + verify_mapping_mn_rec dupmap f f' (PTree.elements dupmap). + +(** Verifies that the [dupmap] of the translated function [f'] is giving correct information in regards to [f] *) +Definition verify_mapping dupmap (f f': function) : res unit := + do u <- verify_mapping_entrypoint dupmap f f'; + do v <- verify_mapping_match_nodes dupmap f f'; OK tt. + +(** * Entry points *) + +Definition transf_function (f: function) : res function := + let (tcte, dupmap) := duplicate_aux f in + let (tc, te) := tcte in + let f' := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in + do u <- verify_mapping dupmap f f'; + OK f'. + +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p.
\ No newline at end of file diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml new file mode 100644 index 00000000..9ff2ae55 --- /dev/null +++ b/backend/Duplicateaux.ml @@ -0,0 +1,13 @@ +open RTL +open Maps + +let rec make_identity_ptree_rec = function +| [] -> PTree.empty +| m::lm -> let (n, _) = m in PTree.set n n (make_identity_ptree_rec lm) + +let make_identity_ptree f = make_identity_ptree_rec (PTree.elements (fn_code f)) + +(* For now, identity function *) +let duplicate_aux f = + let pTreeId = make_identity_ptree f + in (((fn_code f), (fn_entrypoint f)), pTreeId) diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v new file mode 100644 index 00000000..39b7a353 --- /dev/null +++ b/backend/Duplicateproof.v @@ -0,0 +1,494 @@ +(** Correctness proof for code duplication *) +Require Import AST Linking Errors Globalenvs Smallstep. +Require Import Coqlib Maps Events Values. +Require Import Op RTL Duplicate. + +Local Open Scope positive_scope. + +(** * Definition of [match_states] (independently of the translation) *) + +(* est-ce plus simple de prendre dupmap: node -> node, avec un noeud hors CFG à la place de None ? *) +Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop := + | match_inst_nop: forall n n', + dupmap!n' = (Some n) -> match_inst dupmap (Inop n) (Inop n') + | match_inst_op: forall n n' op lr r, + dupmap!n' = (Some n) -> match_inst dupmap (Iop op lr r n) (Iop op lr r n') + | match_inst_load: forall n n' m a lr r, + dupmap!n' = (Some n) -> match_inst dupmap (Iload m a lr r n) (Iload m a lr r n') + | match_inst_store: forall n n' m a lr r, + dupmap!n' = (Some n) -> match_inst dupmap (Istore m a lr r n) (Istore m a lr r n') + | match_inst_call: forall n n' s ri lr r, + dupmap!n' = (Some n) -> match_inst dupmap (Icall s ri lr r n) (Icall s ri lr r n') + | match_inst_tailcall: forall s ri lr, + match_inst dupmap (Itailcall s ri lr) (Itailcall s ri lr) + | match_inst_builtin: forall n n' ef la br, + dupmap!n' = (Some n) -> match_inst dupmap (Ibuiltin ef la br n) (Ibuiltin ef la br n') + | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr, + dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) -> + match_inst dupmap (Icond c lr ifso ifnot) (Icond c lr ifso' ifnot') + | match_inst_jumptable: forall ln ln' r, + list_forall2 (fun n n' => (dupmap!n' = (Some n))) ln ln' -> + match_inst dupmap (Ijumptable r ln) (Ijumptable r ln') + | match_inst_return: forall or, match_inst dupmap (Ireturn or) (Ireturn or). + +Record match_function dupmap f f': Prop := { + dupmap_correct: forall n n', dupmap!n' = Some n -> + (forall i, (fn_code f)!n = Some i -> exists i', (fn_code f')!n' = Some i' /\ match_inst dupmap i i'); + dupmap_entrypoint: dupmap!(fn_entrypoint f') = Some (fn_entrypoint f); + preserv_fnsig: fn_sig f = fn_sig f'; + preserv_fnparams: fn_params f = fn_params f'; + preserv_fnstacksize: fn_stacksize f = fn_stacksize f' +}. + +Inductive match_fundef: RTL.fundef -> RTL.fundef -> Prop := + | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + | match_stackframe_intro + dupmap res f sp pc rs f' pc' + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc' = Some pc): + match_stackframes (Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs). + +Inductive match_states: state -> state -> Prop := + | match_states_intro + dupmap st f sp pc rs m st' f' pc' + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc' = Some pc): + match_states (State st f sp pc rs m) (State st' f' sp pc' rs m) + | match_states_call: + forall st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f'), + match_states (Callstate st f args m) (Callstate st' f' args m) + | match_states_return: + forall st st' v m + (STACKS: list_forall2 match_stackframes st st'), + match_states (Returnstate st v m) (Returnstate st' v m). + +(** * Auxiliary properties *) + + +Theorem transf_function_preserves: + forall f f', + transf_function f = OK f' -> + fn_sig f = fn_sig f' /\ fn_params f = fn_params f' /\ fn_stacksize f = fn_stacksize f'. +Proof. + intros. unfold transf_function in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H. + repeat (split; try reflexivity). +Qed. + + +Lemma verify_mapping_mn_rec_step: + forall dupmap lb b f f', + In b lb -> + verify_mapping_mn_rec dupmap f f' lb = OK tt -> + verify_mapping_mn dupmap f f' b = OK tt. +Proof. + induction lb; intros. + - monadInv H0. inversion H. + - inversion H. + + subst. monadInv H0. destruct x. assumption. + + monadInv H0. destruct x0. eapply IHlb; assumption. +Qed. + +Lemma verify_is_copy_correct: + forall dupmap n n', + verify_is_copy dupmap n n' = OK tt -> + dupmap ! n' = Some n. +Proof. + intros. unfold verify_is_copy in H. destruct (_ ! n') eqn:REVM; [|inversion H]. + destruct (n ?= p) eqn:NP; try (inversion H; fail). + eapply Pos.compare_eq in NP. subst. + reflexivity. +Qed. + +Lemma verify_is_copy_list_correct: + forall dupmap ln ln', + verify_is_copy_list dupmap ln ln' = OK tt -> + list_forall2 (fun n n' => dupmap ! n' = Some n) ln ln'. +Proof. + induction ln. + - intros. destruct ln'; monadInv H. constructor. + - intros. destruct ln'; monadInv H. destruct x. apply verify_is_copy_correct in EQ. + eapply IHln in EQ0. constructor; assumption. +Qed. + +Lemma verify_match_inst_correct: + forall dupmap i i', + verify_match_inst dupmap i i' = OK tt -> + match_inst dupmap i i'. +Proof. + intros. unfold verify_match_inst in H. + destruct i; try (inversion H; fail). +(* Inop *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + constructor; eauto. +(* Iop *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct (eq_operation _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst. + constructor. assumption. +(* Iload *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct (chunk_eq _ _); try discriminate. + destruct (eq_addressing _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst. + constructor. assumption. +(* Istore *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct (chunk_eq _ _); try discriminate. + destruct (eq_addressing _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst. + constructor. assumption. +(* Icall *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct (signature_eq _ _); try discriminate. + destruct (product_eq _ _ _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. subst. + constructor. assumption. +(* Itailcall *) + - destruct i'; try (inversion H; fail). + destruct (signature_eq _ _); try discriminate. + destruct (product_eq _ _ _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. subst. clear H. + constructor. +(* Ibuiltin *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct (external_function_eq _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (builtin_res_eq_pos _ _); try discriminate. subst. + constructor. assumption. +(* Icond *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct x0. eapply verify_is_copy_correct in EQ1. + destruct (eq_condition _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. subst. + constructor; assumption. +(* Ijumptable *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_list_correct in EQ. + destruct (Pos.eq_dec _ _); try discriminate. subst. + constructor. assumption. +(* Ireturn *) + - destruct i'; try (inversion H; fail). + destruct (option_eq _ _ _); try discriminate. subst. clear H. + constructor. +Qed. + + +Lemma verify_mapping_mn_correct mp n n' i f f' tc: + mp ! n' = Some n -> + (fn_code f) ! n = Some i -> + (fn_code f') = tc -> + verify_mapping_mn mp f f' (n', n) = OK tt -> + exists i', + tc ! n' = Some i' + /\ match_inst mp i i'. +Proof. + unfold verify_mapping_mn; intros H H0 H1 H2. rewrite H0 in H2. clear H0. rewrite H1 in H2. clear H1. + destruct (tc ! n') eqn:TCN; [| inversion H2]. + exists i0. split; auto. + eapply verify_match_inst_correct. assumption. +Qed. + + +Lemma verify_mapping_mn_rec_correct: + forall mp n n' i f f' tc, + mp ! n' = Some n -> + (fn_code f) ! n = Some i -> + (fn_code f') = tc -> + verify_mapping_mn_rec mp f f' (PTree.elements mp) = OK tt -> + exists i', + tc ! n' = Some i' + /\ match_inst mp i i'. +Proof. + intros. exploit PTree.elements_correct. eapply H. intros IN. + eapply verify_mapping_mn_rec_step in H2; eauto. + eapply verify_mapping_mn_correct; eauto. +Qed. + +Theorem transf_function_correct f f': + transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. +Proof. + unfold transf_function. + intros TRANSF. + destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). + monadInv TRANSF. + unfold verify_mapping in EQ. monadInv EQ. + exists mp; constructor 1; simpl; auto. + + (* correct *) + intros until n'. intros REVM i FNC. + unfold verify_mapping_match_nodes in EQ. simpl in EQ. destruct x1. + eapply verify_mapping_mn_rec_correct; eauto. + simpl; eauto. + + (* entrypoint *) + intros. unfold verify_mapping_entrypoint in EQ0. simpl in EQ0. + eapply verify_is_copy_correct; eauto. + destruct x0; auto. +Qed. + +Lemma transf_fundef_correct f f': + transf_fundef f = OK f' -> match_fundef f f'. +Proof. + intros TRANSF; destruct f; simpl; monadInv TRANSF. + + exploit transf_function_correct; eauto. + intros (dupmap & MATCH_F). + eapply match_Internal; eauto. + + eapply match_External. +Qed. + +(** * Preservation proof *) + +Definition match_prog (p tp: program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. + +Section PRESERVATION. + +Variable prog: program. +Variable tprog: program. + +Hypothesis TRANSL: match_prog prog tprog. + +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + rewrite <- (Genv.find_symbol_match TRANSL). reflexivity. +Qed. + +(* UNUSED LEMMA ? +Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z. +Proof. + unfold Senv.equiv. intuition congruence. +Qed. +*) + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof. + eapply (Genv.senv_match TRANSL). +Qed. + +Lemma functions_translated: + forall (v: val) (f: fundef), + Genv.find_funct ge v = Some f -> + exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog. +Proof. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & A & B & C). + repeat eexists; intuition eauto. + + unfold incl; auto. + + eapply linkorder_refl. +Qed. + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + exists tf, + Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. +Proof. + intros. + exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto. +Qed. + +Lemma function_sig_translated: + forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f. +Proof. + intros. destruct f. + - simpl in H. monadInv H. simpl. symmetry. apply transf_function_preserves. assumption. + - simpl in H. monadInv H. reflexivity. +Qed. + +Lemma list_nth_z_dupmap: + forall dupmap ln ln' (pc pc': node) val, + list_nth_z ln val = Some pc -> + list_forall2 (fun n n' => dupmap!n' = Some n) ln ln' -> + exists pc', + list_nth_z ln' val = Some pc' + /\ dupmap!pc' = Some pc. +Proof. + induction ln; intros until val; intros LNZ LFA. + - inv LNZ. + - inv LNZ. destruct (zeq val 0) eqn:ZEQ. + + inv H0. destruct ln'; inv LFA. + simpl. exists p. split; auto. + + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto. + intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. +Qed. + +Theorem transf_initial_states: + forall s1, initial_state prog s1 -> + exists s2, initial_state tprog s2 /\ match_states s1 s2. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF). + eexists. split. + - econstructor; eauto. + + eapply (Genv.init_mem_transf_partial TRANSL); eauto. + + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main. eauto. + + destruct f. + * monadInv TRANSF. rewrite <- H3. symmetry; eapply transf_function_preserves. assumption. + * monadInv TRANSF. assumption. + - constructor; eauto. + + constructor. + + apply transf_fundef_correct; auto. +Qed. + +Theorem transf_final_states: + forall s1 s2 r, + match_states s1 s2 -> final_state s1 r -> final_state s2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem step_simulation: + forall s1 t s1', step ge s1 t s1' -> + forall s2 (MS: match_states s1 s2), + exists s2', + step tge s2 t s2' + /\ match_states s1' s2'. +Proof. + Local Hint Resolve transf_fundef_correct. + induction 1; intros; inv MS. +(* Inop *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). + inv H3. + eexists. split. + + eapply exec_Inop; eauto. + + econstructor; eauto. +(* Iop *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Iop; eauto. erewrite eval_operation_preserved; eauto. + + econstructor; eauto. +(* Iload *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto. + + econstructor; eauto. +(* Istore *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto. + + econstructor; eauto. +(* Icall *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + destruct ros. + * simpl in H0. apply functions_translated in H0. + destruct H0 as (tf & cunit & TFUN & GFIND & LO). + eexists. split. + + eapply exec_Icall. eassumption. simpl. eassumption. + apply function_sig_translated. assumption. + + repeat (econstructor; eauto). + * simpl in H0. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. + apply function_ptr_translated in H0. destruct H0 as (tf & GFF & TF). + eexists. split. + + eapply exec_Icall. eassumption. simpl. rewrite symbols_preserved. rewrite GFS. + eassumption. apply function_sig_translated. assumption. + + repeat (econstructor; eauto). +(* Itailcall *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H10 & H11). inv H11. + pose symbols_preserved as SYMPRES. + destruct ros. + * simpl in H0. apply functions_translated in H0. + destruct H0 as (tf & cunit & TFUN & GFIND & LO). + eexists. split. + + eapply exec_Itailcall. eassumption. simpl. eassumption. + apply function_sig_translated. assumption. + erewrite <- preserv_fnstacksize; eauto. + + repeat (constructor; auto). + * simpl in H0. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. + apply function_ptr_translated in H0. destruct H0 as (tf & GFF & TF). + eexists. split. + + eapply exec_Itailcall. eassumption. simpl. rewrite symbols_preserved. rewrite GFS. + eassumption. apply function_sig_translated. assumption. + erewrite <- preserv_fnstacksize; eauto. + + repeat (constructor; auto). +(* Ibuiltin *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + + econstructor; eauto. +(* Icond *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Icond; eauto. + + econstructor; eauto. destruct b; auto. +(* Ijumptable *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + exploit list_nth_z_dupmap; eauto. intros (pc'1 & LNZ & REVM). + eexists. split. + + eapply exec_Ijumptable; eauto. + + econstructor; eauto. +(* Ireturn *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Ireturn; eauto. erewrite <- preserv_fnstacksize; eauto. + + econstructor; eauto. +(* exec_function_internal *) + - inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split. + + eapply exec_function_internal. erewrite <- preserv_fnstacksize; eauto. + + erewrite preserv_fnparams; eauto. + econstructor; eauto. apply dupmap_entrypoint. assumption. +(* exec_function_external *) + - inversion TRANSF as [|]; subst. eexists. split. + + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor. assumption. +(* exec_return *) + - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split. + + constructor. + + inv H1. econstructor; eauto. +Qed. + +Theorem transf_program_correct: + forward_simulation (semantics prog) (semantics tprog). +Proof. + eapply forward_simulation_step with match_states. + - eapply senv_preserved. + - eapply transf_initial_states. + - eapply transf_final_states. + - eapply step_simulation. +Qed. + +End PRESERVATION. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 92c18415..994d2652 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -321,7 +321,10 @@ Local Opaque mreg_type. + (* other ops *) destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans. econstructor; eauto. - apply wt_setreg. eapply Val.has_subtype; eauto. + + apply wt_setreg; auto; try (apply wt_undef_regs; auto). + eapply Val.has_subtype; eauto. + change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. red; intros; subst op. simpl in ISMOVE. destruct args; try discriminate. destruct args; discriminate. diff --git a/common/AST.v b/common/AST.v index bb8508b7..86cab287 100644 --- a/common/AST.v +++ b/common/AST.v @@ -17,7 +17,7 @@ the abstract syntax trees of many of the intermediate languages. *) Require Import String. -Require Import Coqlib Maps Errors Integers Floats. +Require Import Coqlib Maps Errors Integers Floats BinPos. Require Archi. Set Implicit Arguments. @@ -640,11 +640,28 @@ Inductive builtin_arg (A: Type) : Type := | BA_splitlong (hi lo: builtin_arg A) | BA_addptr (a1 a2: builtin_arg A). +Definition builtin_arg_eq {A: Type}: + (forall x y : A, {x = y} + {x <> y}) -> + forall (ba1 ba2: (builtin_arg A)), {ba1=ba2} + {ba1<>ba2}. +Proof. + intro. generalize Integers.int_eq int64_eq float_eq float32_eq chunk_eq ptrofs_eq ident_eq. + decide equality. +Defined. +Global Opaque builtin_arg_eq. + Inductive builtin_res (A: Type) : Type := | BR (x: A) | BR_none | BR_splitlong (hi lo: builtin_res A). +Definition builtin_res_eq {A: Type}: + (forall x y : A, {x = y} + {x <> y}) -> + forall (a b: builtin_res A), {a=b} + {a<>b}. +Proof. + intro. decide equality. +Defined. +Global Opaque builtin_res_eq. + Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident := match a with | BA_loadglobal chunk id ofs => id :: nil @@ -470,6 +470,7 @@ if test "$arch" = "mppa_k1c"; then system="linux" fi +# # AArch64 (ARMv8 64 bits) Target Configuration # if test "$arch" = "aarch64"; then @@ -567,14 +568,14 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10) + 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires one of the following Coq versions: 8.10, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0" + echo "Error: CompCert requires one of the following Coq versions: 8.10, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0" missingtools=true fi;; "") @@ -910,6 +911,4 @@ cat <<EOF Coq development will not be installed EOF fi - fi - diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 0112a5ec..193d83c4 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -18,6 +18,7 @@ type struct_passing_style = | SP_ref_callee (* by reference, callee takes copy *) | SP_ref_caller (* by reference, caller takes copy *) + | SP_value32_ref_callee (* by value if <= 32 bits, by ref_callee otherwise *) | SP_split_args (* by value, as a sequence of ints *) type struct_return_style = @@ -268,8 +269,9 @@ let mppa_k1c = bigendian = false; bitfields_msb_first = false; (* TO CHECK *) supports_unaligned_accesses = true; - struct_passing_style = SP_split_args; - struct_return_style = SR_int1248 } + struct_passing_style = SP_value32_ref_callee; + struct_return_style = SR_int1to4 } + let aarch64 = { i32lpll64 with name = "aarch64"; struct_passing_style = SP_ref_callee; (* Wrong *) diff --git a/cparser/Machine.mli b/cparser/Machine.mli index 31726d7f..ea25c4f6 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -17,6 +17,7 @@ type struct_passing_style = | SP_ref_callee (* by reference, callee takes copy *) | SP_ref_caller (* by reference, caller takes copy *) + | SP_value32_ref_callee (* by value if <= 32 bits, by ref_callee otherwise *) | SP_split_args (* by value, as a sequence of ints *) type struct_return_style = diff --git a/cparser/StructPassing.ml b/cparser/StructPassing.ml index 5c6454f0..3aff090e 100644 --- a/cparser/StructPassing.ml +++ b/cparser/StructPassing.ml @@ -68,7 +68,16 @@ let classify_param env ty = match !struct_passing_style with | SP_ref_callee -> Param_unchanged | SP_ref_caller -> Param_ref_caller - | _ -> + | SP_value32_ref_callee -> + (match sizeof env ty, alignof env ty with + | Some sz, Some al -> + if (sz <= 4) then + Param_flattened ((sz+3)/4, sz, al) (* FIXME - why (sz+3)/4 ? *) + else + Param_unchanged + | _, _ -> Param_unchanged (* when parsing prototype with incomplete structure definition *) + ) + | SP_split_args -> match sizeof env ty, alignof env ty with | Some sz, Some al -> Param_flattened ((sz + 3) / 4, sz, al) diff --git a/driver/Compiler.v b/driver/Compiler.v index 7536e8ff..f948d595 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -38,6 +38,7 @@ Require RTLgen. Require Tailcall. Require Inlining. Require Renumber. +Require Duplicate. Require Constprop. Require CSE. Require Deadcode. @@ -60,6 +61,7 @@ Require RTLgenproof. Require Tailcallproof. Require Inliningproof. Require Renumberproof. +Require Duplicateproof. Require Constpropproof. Require CSEproof. Require Deadcodeproof. @@ -128,17 +130,18 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ time "Duplicating" Duplicate.transf_program @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 7) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 8) @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ -242,6 +245,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog + ::: mkpass Duplicateproof.match_prog ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -308,6 +312,7 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. +<<<<<<< HEAD exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. @@ -320,6 +325,20 @@ Proof. exists p18; split. apply CleanupLabelsproof.transf_program_match; auto. exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. exists p20; split. apply Stackingproof.transf_program_match; auto. +======= + exists p10; split. apply Duplicateproof.transf_program_match; auto. + exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. + exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. + exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p15; split. apply Unusedglobproof.transf_program_match; auto. + exists p16; split. apply Allocproof.transf_program_match; auto. + exists p17; split. apply Tunnelingproof.transf_program_match. + exists p18; split. apply Linearizeproof.transf_program_match; auto. + exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. + exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. + exists p21; split. apply Stackingproof.transf_program_match; auto. +>>>>>>> origin/mppa-work exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -390,6 +409,7 @@ Ltac DestructM := eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply Duplicateproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. diff --git a/lib/Floats.v b/lib/Floats.v index 13350dd0..272efa52 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -16,7 +16,7 @@ (** Formalization of floating-point numbers, using the Flocq library. *) -Require Import Coqlib Zbits Integers. +Require Import Coqlib Zbits Integers Axioms. (*From Flocq*) Require Import Binary Bits Core. Require Import IEEE754_extra. @@ -27,8 +27,69 @@ Close Scope R_scope. Open Scope Z_scope. Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *) + +Definition float_eq: forall (i1 i2: float), {i1=i2} + {i1<>i2}. +Proof. + intros. destruct i1. +(* B754_zero *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_infinity *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_nan *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + generalize (Pos.eq_dec pl pl0). intro. inv H. + ++ left. apply eqb_prop in BEQ. subst. + assert (e = e0) by (apply proof_irr). congruence. + ++ right. intro. inv H. contradiction. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_finite *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ; [apply eqb_prop in BEQ | apply eqb_false_iff in BEQ]. + generalize (Pos.eq_dec m m0). intro. inv H. + generalize (Z.eq_dec e e1). intro. inv H. + 1: { left. assert (e0 = e2) by (apply proof_irr). congruence. } + all: right; intro; inv H; contradiction. +Qed. + Definition float32 := binary32. (**r the type of IEE754 single-precision FP numbers *) +Definition float32_eq: forall (i1 i2: float32), {i1=i2} + {i1<>i2}. +Proof. + intros. destruct i1. +(* B754_zero *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_infinity *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_nan *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + generalize (Pos.eq_dec pl pl0). intro. inv H. + ++ left. apply eqb_prop in BEQ. subst. + assert (e = e0) by (apply proof_irr). congruence. + ++ right. intro. inv H. contradiction. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_finite *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ; [apply eqb_prop in BEQ | apply eqb_false_iff in BEQ]. + generalize (Pos.eq_dec m m0). intro. inv H. + generalize (Z.eq_dec e e1). intro. inv H. + 1: { left. assert (e0 = e2) by (apply proof_irr). congruence. } + all: right; intro; inv H; contradiction. +Qed. + (** Boolean-valued comparisons *) Definition cmp_of_comparison (c: comparison) (x: option Datatypes.comparison) : bool := diff --git a/lib/Integers.v b/lib/Integers.v index 3b6c35eb..3e78ee60 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -16,7 +16,7 @@ (** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *) Require Import Eqdep_dec Zquot Zwf. -Require Import Coqlib Zbits. +Require Import Coqlib Zbits Axioms. Require Archi. (** * Comparisons *) @@ -29,6 +29,11 @@ Inductive comparison : Type := | Cgt : comparison (**r greater than *) | Cge : comparison. (**r greater than or equal *) +Definition comparison_eq: forall (x y: comparison), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + Definition negate_comparison (c: comparison): comparison := match c with | Ceq => Cne @@ -4535,8 +4540,26 @@ End Int64. Strategy 0 [Wordsize_64.wordsize]. +Definition int_eq: forall (i1 i2: int), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Notation int64 := Int64.int. +Definition int64_eq: forall (i1 i2: int64), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Global Opaque Int.repr Int64.repr Byte.repr. (** * Specialization to offsets in pointer values *) @@ -4813,6 +4836,15 @@ Strategy 0 [Wordsize_Ptrofs.wordsize]. Notation ptrofs := Ptrofs.int. +Definition ptrofs_eq: forall (i1 i2: ptrofs), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Global Opaque Ptrofs.repr. Hint Resolve Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v index cdcf58c3..69b32c7c 100644 --- a/mppa_k1c/Archi.v +++ b/mppa_k1c/Archi.v @@ -17,7 +17,6 @@ (** Architecture-dependent parameters for MPPA K1c. Mostly copied from the Risc-V backend *) Require Import ZArith List. -(*From Flocq*) Require Import Binary Bits. Definition ptr64 := true. diff --git a/mppa_k1c/Asmaux.v b/mppa_k1c/Asmaux.v index 94b39f4e..891d1068 100644 --- a/mppa_k1c/Asmaux.v +++ b/mppa_k1c/Asmaux.v @@ -2,4 +2,4 @@ Require Import Asm. Require Import AST. (** Constant only needed by Asmexpandaux.ml *) -Program Definition dummy_function := {| fn_code := nil; fn_sig := signature_main; fn_blocks := nil |}.
+Program Definition dummy_function := {| fn_code := nil; fn_sig := signature_main; fn_blocks := nil |}. diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 65792d13..c7cfe43c 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1665,11 +1665,17 @@ Hint Resolve bblock_simu_test_correct: wlp. Import UnsafeImpure. -Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_simu_test verb p1 p2). +Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := + match unsafe_coerce (bblock_simu_test verb p1 p2) with + | Some b => b + | None => false + end. Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2. Proof. - intros; unfold pure_bblock_simu_test. intros; eapply bblock_simu_test_correct; eauto. + unfold pure_bblock_simu_test. + destruct (unsafe_coerce (bblock_simu_test verb p1 p2)) eqn: UNSAFE; try discriminate. + intros; subst. eapply bblock_simu_test_correct; eauto. apply unsafe_coerce_not_really_correct; eauto. Qed. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index fd50f3b4..5825fd04 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -1112,10 +1112,12 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool := match i with + | MBgetstack ofs ty dst => before && negb (mreg_eq dst MFP) | MBsetstack src ofs ty => before | MBgetparam ofs ty dst => negb (mreg_eq dst MFP) | MBop op args res => before && negb (mreg_eq res MFP) - | _ => false + | MBload chunk addr args dst => before && negb (mreg_eq dst MFP) + | MBstore chunk addr args res => before end. (** This is the naive definition, which is not tail-recursive unlike the other backends *) diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 6baca8c0..cdbaf16a 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -47,7 +47,6 @@ Lemma senv_preserved: Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).
-
Lemma functions_translated:
forall b f,
Genv.find_funct_ptr ge b = Some f ->
@@ -65,8 +64,6 @@ Proof. monadInv B. rewrite H0 in EQ; inv EQ; auto.
Qed.
-(** * Properties of control flow *)
-
Lemma transf_function_no_overflow:
forall f tf,
transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
@@ -75,23 +72,7 @@ Proof. omega.
Qed.
-(** The following lemmas show that the translation from Mach to Asm
- preserves labels, in the sense that the following diagram commutes:
-<<
- translation
- Mach code ------------------------ Asm instr sequence
- | |
- | Mach.find_label lbl find_label lbl |
- | |
- v v
- Mach code tail ------------------- Asm instr seq tail
- translation
->>
- The proof demands many boring lemmas showing that Asm constructor
- functions do not introduce new labels.
-*)
-
-Section TRANSL_LABEL.
+Section TRANSL_LABEL. (* Lemmas on translation of MB.is_label into AB.is_label *) Lemma gen_bblocks_label:
forall hd bdy ex tbb tc,
@@ -113,7 +94,7 @@ Proof. all: inv GENB; simpl; auto.
Qed.
-Lemma in_dec_transl:
+Remark in_dec_transl: forall lbl hd,
(if in_dec lbl hd then true else false) = (if MB.in_dec lbl hd then true else false).
Proof.
@@ -226,7 +207,7 @@ Proof. rewrite H. auto.
Qed.
-Lemma transl_find_label:
+Theorem transl_find_label: forall lbl f tf,
transf_function f = OK tf ->
match MB.find_label lbl f.(MB.fn_code) with
@@ -241,8 +222,8 @@ Qed. End TRANSL_LABEL.
-(** A valid branch in a piece of Mach code translates to a valid ``go to''
- transition in the generated Asm code. *)
+(** A valid branch in a piece of Machblock code translates to a valid ``go to'' + transition in the generated Asmblock code. *) Lemma find_label_goto_label:
forall f tf lbl rs m c' b ofs,
@@ -270,48 +251,47 @@ Qed. (** Existence of return addresses *)
-(* NB: the hypothesis in comment on [b] is not needed in the proof !
-*)
Lemma return_address_exists:
- forall b f (* sg ros *) c, (* b.(MB.exit) = Some (MBcall sg ros) -> *) is_tail (b :: c) f.(MB.fn_code) ->
+ forall b f c, is_tail (b :: c) f.(MB.fn_code) -> exists ra, return_address_offset f c ra.
Proof.
intros. eapply Asmblockgenproof0.return_address_exists; eauto.
- intros. monadInv H0.
destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. monadInv EQ. simpl.
-(* rewrite transl_code'_transl_code in EQ0. *)
- exists x; exists true; split; auto. (* unfold fn_code. *)
+ exists x; exists true; split; auto. repeat constructor.
- - exact transf_function_no_overflow.
+- exact transf_function_no_overflow. Qed.
(** * Proof of semantic preservation *)
-(** Semantic preservation is proved using simulation diagrams
+(** Semantic preservation is proved using a complex simulation diagram of the following form.
<<
- st1 --------------- st2
- | |
- t| *|t
- | |
- v v
- st1'--------------- st2'
+ MB.step + ----------------------------------------> + header body exit + st1 -----> st2 -----> st3 ------------------> st4 + | | | | + | (A) | (B) | (C) | + match_codestate | | | | + | header | body1 | body2 | match_states + cs1 -----> cs2 -----> cs3 ------> cs4 | + | / \ exit | + match_asmstate | --------------- --->--- | + | / match_asmstate \ | + st'1 ---------------------------------------> st'2 + AB.step * >>
- The invariant is the [match_states] predicate below, which includes:
-- The Asm code pointed by the PC register is the translation of
- the current Mach code sequence.
-- Mach register values and Asm register values agree.
-*)
-
-(** We need to show that, in the simulation diagram, we cannot
- take infinitely many Mach transitions that correspond to zero
- transitions on the Asm side. Actually, all Mach transitions
- correspond to at least one Asm transition, except the
- transition from [Machsem.Returnstate] to [Machsem.State].
- So, the following integer measure will suffice to rule out
- the unwanted behaviour. *)
+ The invariant between each MB.step/AB.step is the [match_states] predicate below. + However, we also need to introduce an intermediary state [Codestate] which allows + us to reason on a finer grain, executing header, body and exit separately. + This [Codestate] consists in a state like [Asmblock.State], except that the + code is directly stored in the state, much like [Machblock.State]. It also features + additional useful elements to keep track of while executing a bblock. +*) Remark preg_of_not_FP: forall r, negb (mreg_eq r MFP) = true -> IR FP <> preg_of r.
Proof.
@@ -349,17 +329,18 @@ Inductive match_states: Machblock.state -> Asmvliw.state -> Prop := (Asmvliw.State rs m').
Record codestate :=
- Codestate { pstate: state;
+ Codestate { pstate: state; (**r projection to Asmblock.state *) pheader: list label;
- pbody1: list basic;
- pbody2: list basic;
- pctl: option control;
- fpok: bool;
- rem: list AB.bblock;
- cur: option bblock }.
-
-(* | Codestate: state -> list AB.bblock -> option bblock -> codestate. *)
-
+ pbody1: list basic; (**r list of basic instructions coming from the translation of the Machblock body *) + pbody2: list basic; (**r list of basic instructions coming from the translation of the Machblock exit *) + pctl: option control; (**r exit instruction, coming from the translation of the Machblock exit *) + ep: bool; (**r reflects the [ep] variable used in the translation *) + rem: list AB.bblock; (**r remaining bblocks to execute *) + cur: bblock (**r current bblock to execute - to keep track of its size when incrementing PC *) + }. + +(* The part that deals with Machblock <-> Codestate agreement + * Note about DXP: the property of [ep] only matters if the current block doesn't have a header, hence the condition *) Inductive match_codestate fb: Machblock.state -> codestate -> Prop :=
| match_codestate_intro:
forall s sp ms m rs0 m0 f tc ep c bb tbb tbc tbi
@@ -369,7 +350,6 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop := (TBC: transl_basic_code f (MB.body bb) (if MB.header bb then ep else false) = OK tbc)
(TIC: transl_instr_control f (MB.exit bb) = OK tbi)
(TBLS: transl_blocks f c false = OK tc)
-(* (TRANS: transl_blocks f (bb::c) ep = OK (tbb::tc)) *)
(AG: agree ms sp rs0)
(DXP: (if MB.header bb then ep else false) = true -> rs0#FP = parent_sp s)
,
@@ -377,14 +357,15 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop := {| pstate := (Asmvliw.State rs0 m0);
pheader := (MB.header bb);
pbody1 := tbc;
- pbody2 := (extract_basic tbi);
+ pbody2 := extract_basic tbi; pctl := extract_ctl tbi;
- fpok := ep;
+ ep := ep; rem := tc;
- cur := Some tbb
+ cur := tbb |}
.
+(* The part ensuring that the code in Codestate actually resides at [rs PC] *) Inductive match_asmstate fb: codestate -> Asmvliw.state -> Prop :=
| match_asmstate_some:
forall rs f tf tc m tbb ofs ep tbdy tex lhd
@@ -392,7 +373,6 @@ Inductive match_asmstate fb: codestate -> Asmvliw.state -> Prop := (TRANSF: transf_function f = OK tf)
(PCeq: rs PC = Vptr fb ofs)
(TAIL: code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (tbb::tc))
-(* (HDROK: header tbb = lhd) *)
,
match_asmstate fb
{| pstate := (Asmvliw.State rs m);
@@ -400,12 +380,13 @@ Inductive match_asmstate fb: codestate -> Asmvliw.state -> Prop := pbody1 := tbdy;
pbody2 := extract_basic tex;
pctl := extract_ctl tex;
- fpok := ep;
+ ep := ep; rem := tc;
- cur := Some tbb |}
+ cur := tbb |} (Asmvliw.State rs m)
.
+(* Useful for dealing with the many cases in some proofs *) Ltac exploreInst :=
repeat match goal with
| [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var
@@ -417,12 +398,14 @@ Ltac exploreInst := | [ H : Error _ = OK _ |- _ ] => inversion H
end.
+(** Some translation properties *) + Lemma transl_blocks_nonil:
forall f bb c tc ep,
transl_blocks f (bb::c) ep = OK tc ->
exists tbb tc', tc = tbb :: tc'.
Proof.
- intros until ep. intros TLBS. monadInv TLBS. monadInv EQ. unfold gen_bblocks.
+ intros until ep0. intros TLBS. monadInv TLBS. monadInv EQ. unfold gen_bblocks. destruct (extract_ctl x2).
- destruct c0; destruct i; simpl; eauto. destruct x1; simpl; eauto.
- destruct x1; simpl; eauto.
@@ -469,7 +452,7 @@ Lemma transl_blocks_distrib: -> transl_block f bb (if MB.header bb then ep else false) = OK (tbb :: nil)
/\ transl_blocks f c false = OK tc.
Proof.
- intros until ep. intros TLBS Hbuiltin.
+ intros until ep0. intros TLBS Hbuiltin. destruct bb as [hd bdy ex].
monadInv TLBS. monadInv EQ.
exploit no_builtin_preserved; eauto. intros Hectl. destruct Hectl.
@@ -584,6 +567,9 @@ Proof. * unfold transl_comp_notfloat32. exploreInst; try discriminate.
Qed.
+(* Proving that one can decompose a [match_state] relation into a [match_codestate] + and a [match_asmstate], along with some helpful properties tying both relations together *) + Theorem match_state_codestate:
forall mbs abs s fb sp bb c ms m,
(forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
@@ -596,7 +582,7 @@ Theorem match_state_codestate: /\ transl_blocks f (bb::c) ep = OK (tbb::tc)
/\ body tbb = pbody1 cs ++ pbody2 cs
/\ exit tbb = pctl cs
- /\ cur cs = Some tbb /\ rem cs = tc
+ /\ cur cs = tbb /\ rem cs = tc /\ pstate cs = abs.
Proof.
intros until m. intros Hnobuiltin Hnotempty Hmbs MS. subst. inv MS.
@@ -611,7 +597,7 @@ Proof. eapply transl_instr_control_nobuiltin; eauto.
intros (Hth & Htbdy & Htexit).
exists {| pstate := (State rs m'); pheader := (Machblock.header bb); pbody1 := x; pbody2 := extract_basic x0;
- pctl := extract_ctl x0; fpok := ep; rem := tc'; cur := Some tbb |}, fb, f, tbb, tc', ep.
+ pctl := extract_ctl x0; ep := ep0; rem := tc'; cur := tbb |}, fb, f, tbb, tc', ep0. repeat split. 1-2: econstructor; eauto.
{ destruct (MB.header bb). eauto. discriminate. } eauto.
unfold transl_blocks. fold transl_blocks. unfold transl_block. rewrite EQ. simpl. rewrite EQ1; simpl.
@@ -624,7 +610,7 @@ Definition mb_remove_body (bb: MB.bblock) := Lemma exec_straight_pnil:
forall c rs1 m1 rs2 m2,
- exec_straight tge c rs1 m1 (Pnop::gnil) rs2 m2 ->
+ exec_straight tge c rs1 m1 (Pnop ::g nil) rs2 m2 -> exec_straight tge c rs1 m1 nil rs2 m2.
Proof.
intros. eapply exec_straight_trans. eapply H. econstructor; eauto.
@@ -656,10 +642,9 @@ Lemma nextblock_preserves: Proof.
intros. destruct r; try discriminate.
subst. Simpl.
-(* - subst. Simpl. *)
Qed.
-Lemma cons3_app {A: Type}:
+Remark cons3_app {A: Type}: forall a b c (l: list A),
a :: b :: c :: l = (a :: b :: c :: nil) ++ l.
Proof.
@@ -693,36 +678,20 @@ Proof. induction lb; intros; simpl; congruence.
Qed.
-(* Lemma goto_label_inv:
- forall fn tbb l rs m b ofs,
- rs PC = Vptr b ofs ->
- goto_label fn l rs m = goto_label fn l (nextblock tbb rs) m.
-Proof.
- intros.
- unfold goto_label. rewrite nextblock_pc. unfold Val.offset_ptr. rewrite H.
- exploreInst; auto.
- unfold nextblock. rewrite Pregmap.gss.
-
-Qed.
-
-
-Lemma exec_control_goto_label_inv:
- exec_control tge fn (Some ctl) rs m = goto_label fn l rs m ->
- exec_control tge fn (Some ctl) (nextblock tbb rs) m = goto_label fn l (nextblock tbb rs) m.
-Proof.
-Qed. *)
-
+(* See (C) in the diagram. The proofs are mostly adapted from the previous Mach->Asm proofs, but are + unfortunately quite cumbersome. To reproduce them, it's best to have a Coq IDE with you and see by + yourself the steps *) Theorem step_simu_control:
- forall bb' fb fn s sp c ms' m' rs2 m2 E0 S'' rs1 m1 tbb tbdy2 tex cs2,
+ forall bb' fb fn s sp c ms' m' rs2 m2 t S'' rs1 m1 tbb tbdy2 tex cs2, MB.body bb' = nil ->
(forall ef args res, MB.exit bb' <> Some (MBbuiltin ef args res)) ->
Genv.find_funct_ptr tge fb = Some (Internal fn) ->
pstate cs2 = (Asmvliw.State rs2 m2) ->
pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex ->
- cur cs2 = Some tbb ->
+ cur cs2 = tbb -> match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 ->
match_asmstate fb cs2 (Asmvliw.State rs1 m1) ->
- exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') E0 S'' ->
+ exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') t S'' -> (exists rs3 m3 rs4 m4,
exec_body tge tbdy2 rs2 m2 = Next rs3 m3
/\ exec_control_rel tge fn tex tbb rs3 m3 rs4 m4
@@ -731,7 +700,7 @@ Proof. intros until cs2. intros Hbody Hbuiltin FIND Hpstate Hpbody1 Hpbody2 Hpctl Hcur MCS MAS ESTEP.
inv ESTEP.
- inv MCS. inv MAS. simpl in *.
- inv Hcur. inv Hpstate.
+ inv Hpstate. destruct ctl.
+ (* MBcall *)
destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
@@ -834,7 +803,6 @@ Proof. assert (f0 = f) by congruence. subst f0. assert (f1 = f) by congruence. subst f1. clear H11.
remember (nextblock tbb rs2) as rs2'.
- (* inv AT. monadInv H4. *)
exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND'.
assert (tf = fn) by congruence. subst tf.
exploit find_label_goto_label.
@@ -853,7 +821,6 @@ Proof. assert (forall r : preg, r <> PC -> rs' r = rs2 r).
{ intros. destruct r.
- destruct g. all: rewrite INV; Simpl; auto.
-(* - destruct g. all: rewrite INV; Simpl; auto. *)
- rewrite INV; Simpl; auto.
- contradiction. }
eauto with asmgen.
@@ -962,11 +929,8 @@ Proof. econstructor; eauto.
unfold nextblock, incrPC. repeat apply agree_set_other; auto with asmgen.
- - inv MCS. inv MAS. simpl in *. subst. inv Hpstate. inv Hcur.
-(* exploit transl_blocks_distrib; eauto. (* rewrite <- H2. discriminate. *)
- intros (TLB & TLBS).
- *) destruct bb' as [hd' bdy' ex']; simpl in *. subst.
-(* unfold transl_block in TLB. simpl in TLB. unfold gen_bblocks in TLB; simpl in TLB. inv TLB. *)
+ - inv MCS. inv MAS. simpl in *. subst. inv Hpstate. + destruct bb' as [hd' bdy' ex']; simpl in *. subst. monadInv TBC. monadInv TIC. simpl in *. rewrite H5. rewrite H6.
simpl. repeat eexists.
econstructor. 4: instantiate (3 := false). all:eauto.
@@ -1023,7 +987,8 @@ Proof. all: eauto.
Qed.
-Lemma step_simu_basic:
+(* Handling the individual instructions of theorem (B) in the above diagram. A bit less cumbersome, but still tough *) +Theorem step_simu_basic: forall bb bb' s fb sp c ms m rs1 m1 ms' m' bi cs1 tbdy bdy,
MB.header bb = nil -> MB.body bb = bi::(bdy) -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
bb' = {| MB.header := nil; MB.body := bdy; MB.exit := MB.exit bb |} ->
@@ -1032,7 +997,7 @@ Lemma step_simu_basic: match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
(exists rs2 m2 l cs2 tbdy',
cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := tbdy'; pbody2 := pbody2 cs1;
- pctl := pctl cs1; fpok := fp_is_parent (fpok cs1) bi; rem := rem cs1; cur := cur cs1 |}
+ pctl := pctl cs1; ep := fp_is_parent (ep cs1) bi; rem := rem cs1; cur := cur cs1 |} /\ tbdy = l ++ tbdy'
/\ exec_body tge l rs1 m1 = Next rs2 m2
/\ match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2).
@@ -1041,6 +1006,7 @@ Proof. simpl in *. inv Hpstate.
rewrite Hbody in TBC. monadInv TBC.
inv BSTEP.
+ - (* MBgetstack *)
simpl in EQ0.
unfold Mach.load_stack in H.
@@ -1056,12 +1022,17 @@ Proof. repeat (split; auto).
eapply basics_to_code_app; eauto.
remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
-(* assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. }
- rewrite <- Hheadereq. *) subst.
+ assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. } + subst. simpl in Hheadereq. - eapply match_codestate_intro; eauto. simpl. simpl in EQ. (* { destruct (MB.header bb); auto. } *)
+ eapply match_codestate_intro; eauto. + { simpl. simpl in EQ. rewrite <- Hheadereq in EQ. assumption. } eapply agree_set_mreg; eauto with asmgen.
- intro Hep. simpl in Hep. inv Hep.
+ intro Hep. simpl in Hep. + destruct (andb_prop _ _ Hep). clear Hep. + rewrite <- Hheadereq in DXP. subst. rewrite <- DXP. rewrite Hrs'2. reflexivity. + discriminate. apply preg_of_not_FP; assumption. reflexivity. + - (* MBsetstack *)
simpl in EQ0.
unfold Mach.store_stack in H.
@@ -1078,8 +1049,7 @@ Proof. repeat (split; auto).
eapply basics_to_code_app; eauto.
remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
-(* assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
- rewrite <- Hheadereq. *) subst.
+ subst. eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.
eapply agree_undef_regs; eauto with asmgen.
@@ -1095,10 +1065,9 @@ Proof. exploit Mem.loadv_extends. eauto. eexact H1. auto.
intros [v' [C D]].
- (* Opaque loadind. *)
-(* left; eapply exec_straight_steps; eauto; intros. monadInv TR. *)
monadInv EQ0. rewrite Hheader. rewrite Hheader in DXP.
- destruct ep eqn:EPeq.
+ destruct ep0 eqn:EPeq. + (* RTMP contains parent *)
+ exploit loadind_correct. eexact EQ1.
instantiate (2 := rs1). rewrite DXP; eauto.
@@ -1113,14 +1082,14 @@ Proof. { eapply basics_to_code_app; eauto. }
remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. }
- (* rewrite <- Hheadereq. *)subst.
+ subst. eapply match_codestate_intro; eauto.
eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
simpl; intros. rewrite R; auto with asmgen.
apply preg_of_not_FP; auto.
- (* GPR11 does not contain parent *)
+ (* RTMP does not contain parent *) + rewrite chunk_of_Tptr in A.
exploit loadind_ptr_correct. eexact A. intros [rs2 [P [Q R]]].
exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto.
@@ -1169,8 +1138,7 @@ Proof. repeat (split; auto).
eapply basics_to_code_app; eauto.
remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
-(* assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
- rewrite <- Hheadereq. *) subst.
+ subst. eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.
apply agree_set_undef_mreg with rs1; auto.
apply Val.lessdef_trans with v'; auto.
@@ -1197,12 +1165,15 @@ Local Transparent destroyed_by_op. repeat (split; auto).
eapply basics_to_code_app; eauto.
remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
-(* assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
- rewrite <- Hheadereq. *) subst.
+ assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } + subst. eapply match_codestate_intro; eauto. simpl. simpl in EQ.
-
- eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
- simpl; congruence.
+ rewrite <- Hheadereq in EQ. assumption. + eapply agree_set_mreg; eauto with asmgen. + intro Hep. simpl in Hep. + destruct (andb_prop _ _ Hep). clear Hep. + subst. rewrite <- DXP. rewrite R; try discriminate. reflexivity. + apply preg_of_not_FP; assumption. reflexivity. - (* notrap1 cannot happen *)
simpl in EQ0. unfold transl_load in EQ0.
@@ -1279,11 +1250,13 @@ Local Transparent destroyed_by_op. repeat (split; auto).
eapply basics_to_code_app; eauto.
remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+ assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } subst.
eapply match_codestate_intro; eauto. simpl. simpl in EQ.
-
+ rewrite <- Hheadereq in EQ. assumption. eapply agree_undef_regs; eauto with asmgen.
- simpl; congruence.
+ intro Hep. simpl in Hep. + subst. rewrite <- DXP. rewrite Q; try discriminate. reflexivity. reflexivity. Qed.
Lemma exec_body_trans:
@@ -1309,13 +1282,12 @@ Qed. Inductive exec_header: codestate -> codestate -> Prop :=
| exec_header_cons: forall cs1,
exec_header cs1 {| pstate := pstate cs1; pheader := nil; pbody1 := pbody1 cs1; pbody2 := pbody2 cs1;
- pctl := pctl cs1; fpok := (if pheader cs1 then fpok cs1 else false); rem := rem cs1;
- (* cur := match cur cs1 with None => None | Some bcur => Some (remove_header bcur) end *)
+ pctl := pctl cs1; ep := (if pheader cs1 then ep cs1 else false); rem := rem cs1; cur := cur cs1 |}.
-Lemma step_simu_header:
+(* Theorem (A) in the diagram, the easiest of all *) +Theorem step_simu_header: forall bb s fb sp c ms m rs1 m1 cs1,
-(* (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> *)
pstate cs1 = (State rs1 m1) ->
match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
(exists cs1',
@@ -1340,7 +1312,8 @@ Proof. simpl. econstructor; eauto.
Qed.
-Lemma step_simu_body:
+(* Theorem (B) in the diagram, using step_simu_basic + induction on the Machblock body *) +Theorem step_simu_body: forall bb s fb sp c ms m rs1 m1 ms' cs1 m',
MB.header bb = nil ->
(forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
@@ -1349,14 +1322,14 @@ Lemma step_simu_body: match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
(exists rs2 m2 cs2 ep,
cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := nil; pbody2 := pbody2 cs1;
- pctl := pctl cs1; fpok := ep; rem := rem cs1; cur := cur cs1 |}
+ pctl := pctl cs1; ep := ep; rem := rem cs1; cur := cur cs1 |} /\ exec_body tge (pbody1 cs1) rs1 m1 = Next rs2 m2
/\ match_codestate fb (MB.State s fb sp ({| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |}::c) ms' m') cs2).
Proof.
intros bb. destruct bb as [hd bdy ex]; simpl; auto. induction bdy as [|bi bdy].
- intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS.
inv BSTEP.
- exists rs1, m1, cs1, (fpok cs1).
+ exists rs1, m1, cs1, (ep cs1). inv MCS. inv Hpstate. simpl in *. monadInv TBC. repeat (split; simpl; auto).
econstructor; eauto.
- intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS. inv BSTEP.
@@ -1371,23 +1344,6 @@ Proof. rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto.
Qed.
-(* Lemma exec_body_straight:
- forall l rs0 m0 rs1 m1,
- l <> nil ->
- exec_body tge l rs0 m0 = Next rs1 m1 ->
- exec_straight tge l rs0 m0 nil rs1 m1.
-Proof.
- induction l as [|i1 l].
- intros. contradict H; auto.
- destruct l as [|i2 l].
- - intros until m1. intros _ EXEB. simpl in EXEB.
- destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.
- inv EXEB. econstructor; eauto.
- - intros until m1. intros _ EXEB. simpl in EXEB. simpl in IHl.
- destruct (exec_basic_instr tge i1 rs0 m0) eqn:EBI; try discriminate.
- econstructor; eauto. eapply IHl; eauto. discriminate.
-Qed. *)
-
Lemma exec_body_pc:
forall l rs1 m1 rs2 m2,
exec_body tge l rs1 m1 = Next rs2 m2 ->
@@ -1432,7 +1388,8 @@ Proof. contradict H. unfold mbsize. simpl. auto.
Qed.
-(* Alternative form of step_simulation_bblock, easier to prove *)
+(* Bringing theorems (A), (B) and (C) together, for the case of the absence of builtin instruction *) +(* This more general form is easier to prove, but the actual theorem is step_simulation_bblock further below *) Lemma step_simulation_bblock':
forall sf f sp bb bb' bb'' rs m rs' m' s'' c S1,
bb' = mb_remove_header bb ->
@@ -1481,8 +1438,6 @@ Proof. intros (cs1' & EXEH & MCS2).
(* step_simu_body part *)
-(* assert (MB.body bb = MB.body (mb_remove_header bb)). { destruct bb; simpl; auto. }
- rewrite H in BSTEP. clear H. *)
assert (Hpstate': pstate cs1' = pstate cs1). { inv EXEH; auto. }
exploit step_simu_body.
3: eapply BSTEP.
@@ -1502,8 +1457,8 @@ Proof. 9: eapply MCS'. all: simpl.
10: eapply ESTEP.
all: simpl; eauto.
- rewrite Hpbody2. rewrite Hpctl. rewrite Hcur.
- { inv MAS; simpl in *. inv Hcur. inv Hpstate2. eapply match_asmstate_some; eauto.
+ rewrite Hpbody2. rewrite Hpctl. + { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto. erewrite exec_body_pc; eauto. }
intros (rs3 & m3 & rs4 & m4 & EXEB' & EXECTL' & MS').
@@ -1528,11 +1483,11 @@ Proof. assert (f1 = f0) by congruence. subst f0.
rewrite PCeq in Hrs1pc. inv Hrs1pc.
exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''.
- inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ. inv Hcur.
+ inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ. eapply find_bblock_tail; eauto.
Qed.
-Lemma step_simulation_bblock:
+Theorem step_simulation_bblock: forall sf f sp bb ms m ms' m' S2 c,
body_step ge sf f sp (Machblock.body bb) ms m ms' m' ->
(forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
@@ -1548,12 +1503,7 @@ Proof. - econstructor.
Qed.
-Definition measure (s: MB.state) : nat :=
- match s with
- | MB.State _ _ _ _ _ _ => 0%nat
- | MB.Callstate _ _ _ _ => 0%nat
- | MB.Returnstate _ _ _ => 1%nat
- end.
+(** Dealing now with the builtin case *) Definition split (c: MB.code) :=
match c with
@@ -1609,7 +1559,7 @@ Proof. eapply transl_code_at_pc_split_builtin; eauto.
Qed.
-Lemma step_simulation_builtin:
+Theorem step_simulation_builtin: forall ef args res bb sf f sp c ms m t S2,
MB.body bb = nil -> MB.exit bb = Some (MBbuiltin ef args res) ->
exit_step return_address_offset ge (MB.exit bb) (Machblock.State sf f sp (bb :: c) ms m) t S2 ->
@@ -1656,6 +1606,16 @@ Proof. congruence.
Qed.
+(* Measure to prove finite stuttering, see the other backends *) +Definition measure (s: MB.state) : nat := + match s with + | MB.State _ _ _ _ _ _ => 0%nat + | MB.Callstate _ _ _ _ => 0%nat + | MB.Returnstate _ _ _ => 1%nat + end. + +(* The actual MB.step/AB.step simulation, using the above theorems, plus extra proofs + for the internal and external function cases *) Theorem step_simulation:
forall S1 t S2, MB.step return_address_offset ge S1 t S2 ->
forall S1' (MS: match_states S1 S1'),
@@ -1710,25 +1670,20 @@ Proof. exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.
intros [m3' [P Q]].
(* Execution of function prologue *)
- monadInv EQ0. (* rewrite transl_code'_transl_code in EQ1. *)
+ monadInv EQ0. set (tfbody := make_prologue f x0) in *.
set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *.
set (rs2 := rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef).
exploit (Pget_correct tge GPRA RA nil rs2 m2'); auto.
intros (rs' & U' & V').
-(* exploit (exec_straight_through_singleinst); eauto.
- intro W'. remember (nextblock _ rs') as rs''. *)
exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs' m2').
- rewrite chunk_of_Tptr in P.
+ { rewrite chunk_of_Tptr in P. assert (rs' GPRA = rs0 RA). { apply V'. }
assert (rs' SP = rs2 SP). { apply V'; discriminate. }
rewrite H4. rewrite H3.
- (* change (rs' GPRA) with (rs0 RA). *)
rewrite ATLR.
- change (rs2 SP) with sp. eexact P.
+ change (rs2 SP) with sp. eexact P. } intros (rs3 & U & V).
-(* exploit (exec_straight_through_singleinst); eauto.
- intro W. *)
assert (EXEC_PROLOGUE: exists rs3',
exec_straight_blocks tge tf
tf.(fn_blocks) rs0 m'
@@ -1774,7 +1729,6 @@ Local Transparent destroyed_at_function_entry. rewrite Heqrs3'. Simpl. rewrite V. inversion V'. rewrite H6. auto.
assert (r <> GPRA). { contradict H3; rewrite H3; unfold data_preg; auto. }
assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }
- (* rewrite H8; auto. *)
contradict H3; rewrite H3; unfold data_preg; auto.
contradict H3; rewrite H3; unfold data_preg; auto.
contradict H3; rewrite H3; unfold data_preg; auto.
@@ -1782,6 +1736,7 @@ Local Transparent destroyed_at_function_entry. intros. rewrite Heqrs3'. rewrite V by auto with asmgen.
assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }
rewrite H4 by auto with asmgen. reflexivity. discriminate.
+ - (* external function *)
inv MS.
exploit functions_translated; eauto.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index a360aa7c..d3eb1dde 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -1204,7 +1204,8 @@ Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. compute. discriminate. + + rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate. Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). @@ -1217,7 +1218,7 @@ Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. compute. discriminate. + rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate. Qed. Theorem eval_intoffloat: diff --git a/mppa_k1c/abstractbb/Impure/ImpConfig.v b/mppa_k1c/abstractbb/Impure/ImpConfig.v index 1bd93d4c..e49a4611 100644 --- a/mppa_k1c/abstractbb/Impure/ImpConfig.v +++ b/mppa_k1c/abstractbb/Impure/ImpConfig.v @@ -22,9 +22,9 @@ Module Type ImpureView. (* START COMMENT *) Module UnsafeImpure. - Parameter unsafe_coerce: forall {A}, t A -> A. + Parameter unsafe_coerce: forall {A}, t A -> option A. - Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=x -> mayRet k x. + Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=Some x -> mayRet k x. Extraction Inline unsafe_coerce. @@ -41,11 +41,11 @@ Module Impure: ImpureView. Module UnsafeImpure. - Definition unsafe_coerce {A} (x:t A) := x. + Definition unsafe_coerce {A} (x:t A) := Some x. - Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=x -> mayRet k x. + Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=Some x -> mayRet k x. Proof. - unfold unsafe_coerce, mayRet; auto. + unfold unsafe_coerce, mayRet; congruence. Qed. End UnsafeImpure. diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index ecaca7b3..0fa47fca 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -25,6 +25,8 @@ Require Import Op Locations Mach Asm. Local Open Scope string_scope. Local Open Scope error_monad_scope. +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. + (** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the compiler, mostly that argument and result registers are of the correct diff --git a/test/c/Makefile b/test/c/Makefile index 72814390..a2a80e06 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -8,7 +8,9 @@ EXECUTE:=timeout --signal=SIGTERM 20s $(EXECUTE) LIBS=$(LIBMATH) -TIME=ocaml unix.cma ../../tools/xtime.ml -o /dev/null -mintime 2.0 -minruns 4 +TIME=time >/dev/null +# FIXME - maybe this is better? From v3.6 +# TIME=ocaml unix.cma ../../tools/xtime.ml -o /dev/null -mintime 2.0 -minruns 4 PROGS?=fib integr qsort fft fftsp fftw sha1 sha3 aes almabench \ lists binarytrees fannkuch mandelbrot nbody \ diff --git a/test/c/Results/mandelbrot-mppa_k1c b/test/c/Results/mandelbrot-mppa_k1c Binary files differindex 246f7ce1..f50961fe 100644 --- a/test/c/Results/mandelbrot-mppa_k1c +++ b/test/c/Results/mandelbrot-mppa_k1c diff --git a/test/c/aes.c b/test/c/aes.c index 16f02e47..0a64fe60 100644 --- a/test/c/aes.c +++ b/test/c/aes.c @@ -1441,6 +1441,10 @@ int main(int argc, char ** argv) (u8 *)"\x00\x11\x22\x33\x44\x55\x66\x77\x88\x99\xAA\xBB\xCC\xDD\xEE\xFF", (u8 *)"\x8E\xA2\xB7\xCA\x51\x67\x45\xBF\xEA\xFC\x49\x90\x4B\x49\x60\x89", 5, 6); +#ifdef __K1C__ + do_bench(2000); +#else do_bench(1000000); +#endif return 0; } diff --git a/test/c/almabench.c b/test/c/almabench.c index 5487b062..4417200c 100644 --- a/test/c/almabench.c +++ b/test/c/almabench.c @@ -42,10 +42,15 @@ #define R2D (180.0 / PI) #define GAUSSK 0.01720209895 #define TEST_LOOPS 20 -#define TEST_LENGTH 36525 #define sineps 0.3977771559319137 #define coseps 0.9174820620691818 +#ifdef __K1C__ +#define TEST_LENGTH 12 +#else +#define TEST_LENGTH 36525 +#endif + const double amas [8] = { 6023600.0, 408523.5, 328900.5, 3098710.0, 1047.355, 3498.5, 22869.0, 19314.0 }; const double a [8][3] = diff --git a/test/c/mandelbrot.c b/test/c/mandelbrot.c index 133d55c5..fb8b929c 100644 --- a/test/c/mandelbrot.c +++ b/test/c/mandelbrot.c @@ -27,7 +27,7 @@ int main (int argc, char **argv) if (argc < 2) { #ifdef __K1C__ - w = h = 50; + w = h = 40; #else w = h = 1000; #endif diff --git a/test/c/sha1.c b/test/c/sha1.c index 0a6ac8fe..624030cc 100644 --- a/test/c/sha1.c +++ b/test/c/sha1.c @@ -231,6 +231,10 @@ int main(int argc, char ** argv) } do_test(test_input_1, test_output_1); do_test(test_input_2, test_output_2); +#ifdef __K1C__ + do_bench(500); +#else do_bench(200000); +#endif return 0; } diff --git a/test/c/sha3.c b/test/c/sha3.c index a0905817..164e3086 100644 --- a/test/c/sha3.c +++ b/test/c/sha3.c @@ -190,8 +190,13 @@ test_triplet_t testvec[4] = { } }; +#ifdef __K1C__ +#define DATALEN 1000 +#define NITER 7 +#else #define DATALEN 100000 #define NITER 25 +#endif int main() { diff --git a/test/c/siphash24.c b/test/c/siphash24.c index 4a42e013..ce0df78c 100644 --- a/test/c/siphash24.c +++ b/test/c/siphash24.c @@ -235,13 +235,19 @@ int test_vectors() u8 testdata[100] = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 12, 34, 56, 78, 90 }; +#ifdef __K1C__ +#define NITER 1000 +#else +#define NITER 1000000 +#endif + int speed_test(void) { u8 out[8], k[16]; int i; for(i = 0; i < 16; ++i ) k[i] = i; - for(i = 0; i < 1000000; i++) { + for(i = 0; i < NITER; i++) { testdata[99] = (u8) i; crypto_auth(out, testdata, 100, k); } diff --git a/test/endian.h b/test/endian.h index 8be2850c..d6e121f4 100644 --- a/test/endian.h +++ b/test/endian.h @@ -1,7 +1,7 @@ #if defined(__ppc__) || defined(__PPC__) || defined(__ARMEB__) #define ARCH_BIG_ENDIAN #elif defined(__i386__) || defined(__x86_64__) || defined(__ARMEL__) \ - || defined(__riscv) || defined(__aarch64__) + || defined(__riscv) || defined(__aarch64__) || defined(__K1C__) #undef ARCH_BIG_ENDIAN #else #error "unknown endianness" diff --git a/test/monniaux/Makefile b/test/monniaux/Makefile index a6b19891..d7437eea 100644 --- a/test/monniaux/Makefile +++ b/test/monniaux/Makefile @@ -20,9 +20,12 @@ oracle_times.txt: PostpassSchedulingOracle.patch bash build_benches.sh $@ measures.csv: - (cd ../../ && make -j20 && make install) - bash build_benches.sh - bash run_benches.sh $@ + @echo "Building compcert.." + @(cd ../../ && make -s -j20 && make -s install) + @echo "Building benches..." + @bash build_benches.sh + @echo "Benches built. Running benches..." + @bash run_benches.sh $@ #compile_times.pdf: gencompile.py verifier_times.txt oracle_times.txt # python3.5 $^ $@ @@ -32,4 +35,5 @@ measures.csv: .PHONY: clean: + @bash clean_benches.sh rm -f verifier_times.txt oracle_times.txt compile_times.pdf measure_times.k1c.pdf measures.csv diff --git a/test/monniaux/README.md b/test/monniaux/README.md index dbb3f337..14b062da 100644 --- a/test/monniaux/README.md +++ b/test/monniaux/README.md @@ -1,13 +1,18 @@ -# Benchmarking CompCert and GCC +# Benchmarking `CompCert` and GCC -rules.mk contains generic rules to compile with gcc and ccomp, with different -optimizations, and producing different binaries. It also produces a -measures.csv file containing the different timings given by the bench. +## Compiling `CompCert` -Up to 5 different optimizations can be used. +The first step to benchmark `CompCert` is to compile it - the `INSTALL.md` instructions of the project root folder should guide you on installing it. -To use this rule.mk, create a folder, put inside all the .c/.h source files, -and write a Makefile ressembling: +For the benchmarks to work, the compiler `ccomp` should be on your `$PATH`, with the runtime libraries installed correctly (with a successful `make install` on the project root directory). + +## Using the harness + +`rules.mk` contains generic rules to compile with `gcc` and `ccomp`, with different optimizations, and producing different binaries. It also produces a `measures.csv` file containing the different timings given by the bench. + +Up to 5 different sets of optimizations per compiler can be used. + +To use this `rules.mk`, create a folder, put inside all the .c/.h source files, and write a Makefile resembling: ```make TARGET=float_mat MEASURES="c1 c2 c3 c4 c5 c6 c7 c8" @@ -15,57 +20,88 @@ MEASURES="c1 c2 c3 c4 c5 c6 c7 c8" include ../rules.mk ``` -This is all that is required to write, the rules.mk handles everything. +This is all that is required to write, the `rules.mk` handles everything. -There is the possibility to define some variables to finetune what you want. -For instance, `ALL_CFILES` describes the .c source files whose objects are -to be linked. +There is the possibility to define some variables to fine tune what you want. For instance, `ALL_CFILES` describes the .c source files whose objects are to be linked. Here is an exhaustive list of the variables: - `TARGET`: name of the binary to produce - `MEASURES`: list of the different timings. This supposes that the program -prints something of the form "c3 cycles: 44131" for instance. In the above -example, the Makefile would generate such a line: -``` -float_mat c3, 1504675, 751514, 553235, 1929369, 1372441 -``` +prints something of the form `c3 cycles: 44131`. - `ALL_CFILES`: list of .c files to compile. By default, `$(wildcard *.c)` -- `CLOCK`: basename of the clock file to compile. Default `../clock` -- `ALL_CFLAGS`: cflags that are to be included for all compilers +- `CLOCK`: `basename` of the clock file to compile. Default `../clock` +- `ALL_CFLAGS`: `cflags` that are to be included for all compilers - `ALL_GCCFLAGS`: same, but GCC specific -- `ALL_CCOMPFLAGS`: same, but ccomp specific -- `K1C_CC`: GCC compiler (default k1-cos-gcc) -- `K1C_CCOMP`: compcert compiler (default ccomp) -- `EXECUTE_CYCLES`: running command (default `k1-cluster` with some options) -- `GCCiFLAGS` with i from 0 to 4: the wanted optimizations. If one of these flags is empty, nothing is done. Same for `CCOMPiFLAGS`. For now, the default values: -``` -# You can define up to GCC4FLAGS and CCOMP4FLAGS -GCC0FLAGS?= -GCC1FLAGS?=$(ALL_GCCFLAGS) -O1 -GCC2FLAGS?=$(ALL_GCCFLAGS) -O2 -GCC3FLAGS?=$(ALL_GCCFLAGS) -O3 -GCC4FLAGS?= -CCOMP0FLAGS?= -CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -fno-postpass -CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) -CCOMP3FLAGS?= -CCOMP4FLAGS?= - -# Prefix names -GCC0PREFIX?= -GCC1PREFIX?=.gcc.o1 -GCC2PREFIX?=.gcc.o2 -GCC3PREFIX?=.gcc.o3 -GCC4PREFIX?= -CCOMP0PREFIX?= -CCOMP1PREFIX?=.ccomp.o1 -CCOMP2PREFIX?=.ccomp.o2 -CCOMP3PREFIX?= -CCOMP4PREFIX?= -``` +- `ALL_CCOMPFLAGS`: same, but `ccomp` specific +- `K1C_CC`: GCC compiler (default `k1-cos-gcc`) +- `K1C_CCOMP`: `CompCert` compiler (default `ccomp`) +- `EXECUTE_CYCLES`: running command (default is `k1-cluster --syscall=libstd_scalls.so --cycle-based --`) +- `EXECUTE_ARGS`: execution arguments. You can use a macro `__BASE__` which expands to the name of the binary being executed. +- `GCCiFLAGS` with `i` from 0 to 4: the wanted optimizations. If one of these flags is empty, nothing is done. Same for `CCOMPiFLAGS`. Look at `rules.mk` to see the default values. You might find something like this: + + # You can define up to GCC4FLAGS and CCOMP4FLAGS + GCC0FLAGS?= + GCC1FLAGS?=$(ALL_GCCFLAGS) -O1 + GCC2FLAGS?=$(ALL_GCCFLAGS) -O2 + GCC3FLAGS?=$(ALL_GCCFLAGS) -O3 + GCC4FLAGS?= + CCOMP0FLAGS?= + CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -fno-postpass + CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) + CCOMP3FLAGS?= + CCOMP4FLAGS?= + + # Prefix names + GCC0PREFIX?= + GCC1PREFIX?=.gcc.o1 + GCC2PREFIX?=.gcc.o2 + GCC3PREFIX?=.gcc.o3 + GCC4PREFIX?= + CCOMP0PREFIX?= + CCOMP1PREFIX?=.ccomp.o1 + CCOMP2PREFIX?=.ccomp.o2 + CCOMP3PREFIX?= + CCOMP4PREFIX?= + +The `PREFIX` are the prefixes to add to the secondary produced files (assembly, object, executable, ..). You should be careful that if a `FLAGS` is set, then the according `PREFIX` should be set as well. + +Assembly files are generated in `asm/`, objects in `obj/`, binaries in `bin/` and outputs in `out/`. + +To compile and execute all the benches : `make` while in the `monniaux` directory (without any `-j` flag). Doing so will compile CompCert, install it, and then proceed to execute each bench. + +To compile and/or execute a single bench, `cd` to the bench directory, then: +- `make` for compiling the bench +- `make run` for running it + +You can use `-j` flag when in a single bench directory. + +## Individual scripts + +If you want to run the building and running scripts individually without having to use the `Makefile` from `test/monniaux`, you can run the `build_benches.sh` script which builds each bench using all the available cores on your machine. + +Once the benches are built, you can then run `run_benches.sh file.csv` where `file.csv` is where you want to store the timings of the benchmarks. `run_benches.sh` also uses all the available cores of your machine. + +## Adding timings to a benchmark + +If you just add a benchmark without any timing function, the resulting `measures.csv` file will be empty for lack of timing output. + +To add a timing, you must use the functions whose prototypes are in `clock.h` + + #include "../clock.h" + /* ... */ + clock_prepare(); + /* ... */ + clock_start(); + /* .. computations .. */ + clock_stop(); + /* ... */ + print_total_clock(); // print to stdout + printerr_total_clock(); // print to stderr + +If the benchmark doesn't use `stdout` in a binary way you can use `print_total_clock()`. However, some benchmarks like `jpeg-6b` print their binary content to `stdout`, which then messes up the `grep` command when attempting to use it to extract the cycles from `stdout`. -The `PREFIX` are the prefixes to add to the .s, .o, etc.. You should be careful that if a FLAGS is set, then the according PREFIX should be set as well. +The solution is then to use `printerr_total_clock()` which will print the cycles to `stderr`, and use `EXECUTE_ARGS` ressembling this: -Assembly files will be generated in `asm/`, objects in `obj/`, binaries in `bin/` and outputs in `out/`. + EXECUTE_ARGS=-dct int -outfile __BASE__.jpg testimg.ppm 2> __BASE__.out -To compile and execute all the benches : `make` +`__BASE__` is a macro that gets expanded to the base name - that is, the `TARGET` concatenated with one of the `GCCiPREFIX` or `CCOMPiPREFIX`. For instance, in `jpeg-6b`, `__BASE__` could be `jpeg-6b.ccomp.o2`. diff --git a/test/monniaux/benches.sh b/test/monniaux/benches.sh index 2365063a..434e1b15 100644 --- a/test/monniaux/benches.sh +++ b/test/monniaux/benches.sh @@ -1,3 +1,3 @@ -benches="binary_search bitsliced-aes bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow too_slow heptagon_radio_transmitter lustrev4_lustrec_heater_control lustrev4_lv4_heater_control lustrev4_lv6-en-2cgc_heater_control lustrev6-convertible-en-2cgc xor_and_mat" +benches="binary_search bitsliced-aes bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow too_slow heptagon_radio_transmitter lustrev4_lustrec_heater_control lustrev4_lv4_heater_control lustrev4_lv6-en-2cgc_heater_control lustrev6-convertible-en-2cgc xor_and_mat glpk-4.65 picosat-965 genann jpeg-6b zlib-1.2.11 ocaml tiff-4.0.10 ncompress" # Removed for now : ternary diff --git a/test/monniaux/build_benches.sh b/test/monniaux/build_benches.sh index 931cebac..01abf55d 100755 --- a/test/monniaux/build_benches.sh +++ b/test/monniaux/build_benches.sh @@ -2,15 +2,21 @@ TMPFILE=/tmp/1513times.txt +cores=$(grep -c ^processor /proc/cpuinfo) source benches.sh +default="\e[39m" +magenta="\e[35m" +red="\e[31m" + rm -f commands.txt rm -f $TMPFILE for bench in $benches; do + echo -e "${magenta}Building $bench..${default}" if [ "$1" == "" ]; then - (cd $bench && make -j20) + (cd $bench && make -s -j$cores > /dev/null &> /dev/null) || { echo -e "${red}Build failed" && break; } else - (cd $bench && make -j20) | grep -P "\d+: \d+\.\d+" >> $TMPFILE + (cd $bench && make -j$cores) | grep -P "\d+: \d+\.\d+" >> $TMPFILE fi done diff --git a/test/monniaux/clean_benches.sh b/test/monniaux/clean_benches.sh index c0a87ff9..dff15fd4 100755 --- a/test/monniaux/clean_benches.sh +++ b/test/monniaux/clean_benches.sh @@ -1,8 +1,12 @@ source benches.sh +blue="\e[34m" +default="\e[39m" + rm -f commands.txt for bench in $benches; do - (cd $bench && make clean) + echo -e "${blue}Cleaning $bench..${default}" + (cd $bench && make -s clean) done rm -f *.o diff --git a/test/monniaux/genann/Makefile b/test/monniaux/genann/Makefile new file mode 100644 index 00000000..2e76ec63 --- /dev/null +++ b/test/monniaux/genann/Makefile @@ -0,0 +1,4 @@ +ALL_CFILES= example4shorter.c genann.c +TARGET=genann4 + +include ../rules.mk diff --git a/test/monniaux/genann/make.proto b/test/monniaux/genann/make.proto deleted file mode 100644 index 7c4248bf..00000000 --- a/test/monniaux/genann/make.proto +++ /dev/null @@ -1,2 +0,0 @@ -sources: example4shorter.c genann.c -target: genann4
\ No newline at end of file diff --git a/test/monniaux/glpk-4.65/Makefile b/test/monniaux/glpk-4.65/Makefile index a0ab40dc..eaa3f4b0 100644 --- a/test/monniaux/glpk-4.65/Makefile +++ b/test/monniaux/glpk-4.65/Makefile @@ -1,39 +1,6 @@ ALL_CFLAGS += -I src/amd -I src/colamd -I src/mpl -I src/simplex -I src/api -I src/intopt -I src/minisat -I src/npp -I src/zlib -I src/bflib -I src/env -I src/misc -I src/draft -I src - -include ../rules.mk - -LIBS = -lm - -src=examples/glpsol.c $(wildcard src/*/*.c) - -PRODUCTS?=glpsol.gcc.host glpsol.ccomp.host glpsol.gcc.k1c glpsol.gcc.o1.k1c glpsol.ccomp.k1c -PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS)) - -all: $(PRODUCTS) - -.PHONY: -run: measures.csv - - -glpsol.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o - $(CC) $(CFLAGS) $+ $(LIBS) -o $@ -glpsol.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) $+ $(LIBS) -o $@ -glpsol.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ $(LIBS) -o $@ -glpsol.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ $(LIBS) -o $@ -glpsol.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ $(LIBS) -o $@ - +ALL_CFILES=examples/glpsol.c $(wildcard src/*/*.c) +TARGET=glpk EXECUTE_ARGS=--math examples/prod.mod -measures.csv: $(PRODUCTS_OUT) - echo "benches, gcc host,ccomp host,gcc k1c,gcc o1 k1c,ccomp k1c" > $@ - -.SECONDARY: - -.PHONY: -clean: - rm -f *.o *.s *.k1c *.csv - +include ../rules.mk diff --git a/test/monniaux/jpeg-6b/Makefile b/test/monniaux/jpeg-6b/Makefile index 5a45b729..2bec9bb7 100644 --- a/test/monniaux/jpeg-6b/Makefile +++ b/test/monniaux/jpeg-6b/Makefile @@ -1,6 +1,6 @@ -all: cjpeg.gcc.k1c.out djpeg.gcc.k1c.out cjpeg.gcc.o1.k1c.out djpeg.gcc.o1.k1c.out cjpeg.ccomp.k1c.out djpeg.ccomp.k1c.out +TARGET=jpeg-6b -LIBSOURCES= jcapimin.c jcapistd.c jccoefct.c jccolor.c jcdctmgr.c jchuff.c \ +ALL_CFILES= jcapimin.c jcapistd.c jccoefct.c jccolor.c jcdctmgr.c jchuff.c \ jcinit.c jcmainct.c jcmarker.c jcmaster.c jcomapi.c jcparam.c \ jcphuff.c jcprepct.c jcsample.c jctrans.c jdapimin.c jdapistd.c \ jdatadst.c jdatasrc.c jdcoefct.c jdcolor.c jddctmgr.c jdhuff.c \ @@ -8,36 +8,53 @@ LIBSOURCES= jcapimin.c jcapistd.c jccoefct.c jccolor.c jcdctmgr.c jchuff.c \ jdpostct.c jdsample.c jdtrans.c jerror.c jfdctflt.c jfdctfst.c \ jfdctint.c jidctflt.c jidctfst.c jidctint.c jidctred.c jquant1.c \ jquant2.c jutils.c jmemmgr.c jmemansi.c -CSOURCES=$(LIBSOURCES) rdppm.c rdgif.c rdtarga.c rdrle.c rdbmp.c rdswitch.c cdjpeg.c wrppm.c wrgif.c wrtarga.c wrrle.c wrbmp.c rdcolmap.c +ALL_CFILES+=rdppm.c rdgif.c rdtarga.c rdrle.c rdbmp.c rdswitch.c cdjpeg.c wrppm.c wrgif.c wrtarga.c wrrle.c wrbmp.c rdcolmap.c +ALL_CFILES+=cjpeg.c -LIB_K1C_GCC_OFILES=$(CSOURCES:.c=.gcc.k1c.o) -LIB_K1C_GCC_O1_OFILES=$(CSOURCES:.c=.gcc.o1.k1c.o) -LIB_K1C_CCOMP_OFILES=$(CSOURCES:.c=.ccomp.k1c.o) +EXECUTE_ARGS=-dct int -outfile __BASE__.jpg testimg.ppm 2> __BASE__.out include ../rules.mk -cjpeg.gcc.k1c: $(LIB_K1C_GCC_OFILES) cjpeg.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o -djpeg.gcc.k1c: $(LIB_K1C_GCC_OFILES) djpeg.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o - -cjpeg.gcc.o1.k1c: $(LIB_K1C_GCC_O1_OFILES) cjpeg.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o -djpeg.gcc.o1.k1c: $(LIB_K1C_GCC_O1_OFILES) djpeg.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o - -cjpeg.ccomp.k1c: $(LIB_K1C_CCOMP_OFILES) cjpeg.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o -djpeg.ccomp.k1c: $(LIB_K1C_CCOMP_OFILES) djpeg.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o - - -djpeg.%.out: djpeg.% - $(EXECUTE_CYCLES) $< -dct int -ppm -outfile $@.ppm testorig.jpg 2> $@ - cmp $@.ppm testimg.ppm 2>> $@ - -cjpeg.%.out: cjpeg.% - $(EXECUTE_CYCLES) $< -dct int -outfile $@.jpg testimg.ppm 2> $@ - cmp $@.jpg testimg.jpg 2>> $@ - -.SECONDARY: +#all: cjpeg.gcc.k1c.out djpeg.gcc.k1c.out cjpeg.gcc.o1.k1c.out djpeg.gcc.o1.k1c.out cjpeg.ccomp.k1c.out djpeg.ccomp.k1c.out +# +#LIBSOURCES= jcapimin.c jcapistd.c jccoefct.c jccolor.c jcdctmgr.c jchuff.c \ +# jcinit.c jcmainct.c jcmarker.c jcmaster.c jcomapi.c jcparam.c \ +# jcphuff.c jcprepct.c jcsample.c jctrans.c jdapimin.c jdapistd.c \ +# jdatadst.c jdatasrc.c jdcoefct.c jdcolor.c jddctmgr.c jdhuff.c \ +# jdinput.c jdmainct.c jdmarker.c jdmaster.c jdmerge.c jdphuff.c \ +# jdpostct.c jdsample.c jdtrans.c jerror.c jfdctflt.c jfdctfst.c \ +# jfdctint.c jidctflt.c jidctfst.c jidctint.c jidctred.c jquant1.c \ +# jquant2.c jutils.c jmemmgr.c jmemansi.c +#CSOURCES=$(LIBSOURCES) rdppm.c rdgif.c rdtarga.c rdrle.c rdbmp.c rdswitch.c cdjpeg.c wrppm.c wrgif.c wrtarga.c wrrle.c wrbmp.c rdcolmap.c +# +#LIB_K1C_GCC_OFILES=$(CSOURCES:.c=.gcc.k1c.o) +#LIB_K1C_GCC_O1_OFILES=$(CSOURCES:.c=.gcc.o1.k1c.o) +#LIB_K1C_CCOMP_OFILES=$(CSOURCES:.c=.ccomp.k1c.o) +# +#include ../rules.mk +# +#cjpeg.gcc.k1c: $(LIB_K1C_GCC_OFILES) cjpeg.gcc.k1c.o +# $(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o +#djpeg.gcc.k1c: $(LIB_K1C_GCC_OFILES) djpeg.gcc.k1c.o +# $(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o +# +#cjpeg.gcc.o1.k1c: $(LIB_K1C_GCC_O1_OFILES) cjpeg.gcc.k1c.o +# $(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o +#djpeg.gcc.o1.k1c: $(LIB_K1C_GCC_O1_OFILES) djpeg.gcc.k1c.o +# $(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o +# +#cjpeg.ccomp.k1c: $(LIB_K1C_CCOMP_OFILES) cjpeg.gcc.k1c.o +# $(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o +#djpeg.ccomp.k1c: $(LIB_K1C_CCOMP_OFILES) djpeg.gcc.k1c.o +# $(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o +# +# +#djpeg.%.out: djpeg.% +# $(EXECUTE_CYCLES) $< -dct int -ppm -outfile $@.ppm testorig.jpg 2> $@ +# cmp $@.ppm testimg.ppm 2>> $@ +# +#cjpeg.%.out: cjpeg.% +# $(EXECUTE_CYCLES) $< -dct int -outfile $@.jpg testimg.ppm 2> $@ +# cmp $@.jpg testimg.jpg 2>> $@ +# +#.SECONDARY: diff --git a/test/monniaux/ncompress/Makefile b/test/monniaux/ncompress/Makefile index cf543976..14a99d0b 100644 --- a/test/monniaux/ncompress/Makefile +++ b/test/monniaux/ncompress/Makefile @@ -1,52 +1,4 @@ -include ../rules.mk - -all: check - - -all: compress.gcc.host compress.ccomp.host compress.gcc.k1c compress.ccomp.k1c - -compress.gcc.host : compress42.c ../clock.gcc.host.o - $(CC) $(CFLAGS) $+ -o $@ - -compress.ccomp.host : compress42.c ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) $+ -o $@ - -compress.gcc.k1c : compress42.gcc.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -compress.ccomp.k1c : compress42.ccomp.k1c.o ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -INFILE=Makefile -COMPRESSED=foo.gcc.host.Z - -foo.gcc.host.Z: compress.gcc.host $(INFILE) - ./compress.gcc.host <$(INFILE) >foo.gcc.host.Z 2> foo.gcc.host.Z.out +TARGET=compress +EXECUTE_ARGS= < Makefile > __BASE__.Z 2> __BASE__.out -foo.ccomp.k1c.Z: compress.ccomp.k1c $(INFILE) - $(EXECUTE) ./compress.ccomp.k1c <$(INFILE) >foo.ccomp.k1c.Z 2> foo.ccomp.k1c.Z.out - -foo.gcc.k1c.Z: compress.gcc.k1c $(INFILE) - $(EXECUTE) ./compress.gcc.k1c <$(INFILE) >foo.gcc.k1c.Z 2> foo.gcc.k1c.Z.out - -foo.gcc.host.txt: compress.gcc.host $(COMPRESSED) - ./compress.gcc.host -d <$(COMPRESSED) >foo.gcc.host.txt 2> foo.gcc.host.txt.out - -foo.ccomp.k1c.txt: compress.gcc.host $(COMPRESSED) - $(EXECUTE) ./compress.ccomp.k1c -d <$(COMPRESSED) >foo.ccomp.k1c.txt 2> foo.ccomp.k1c.txt.out - -foo.gcc.k1c.txt: compress.gcc.host $(COMPRESSED) - $(EXECUTE) ./compress.gcc.k1c -d <$(COMPRESSED) >foo.gcc.k1c.txt 2> foo.gcc.k1c.txt.out - -check: foo.gcc.host.Z foo.gcc.host.txt foo.ccomp.k1c.Z foo.ccomp.k1c.txt foo.gcc.k1c.Z foo.gcc.k1c.txt - cmp foo.gcc.host.Z foo.ccomp.k1c.Z - cmp foo.gcc.host.Z foo.gcc.k1c.Z - cmp foo.gcc.host.txt foo.ccomp.k1c.txt - cmp foo.gcc.host.txt foo.gcc.k1c.txt - -clean: - rm -f *.Z *.txt *.out *.o *.s *.host *.k1c - -.PHONY: clean - -.SECONDARY: %.s +include ../rules.mk diff --git a/test/monniaux/ocaml/Makefile b/test/monniaux/ocaml/Makefile index b63c8864..20f32b65 100644 --- a/test/monniaux/ocaml/Makefile +++ b/test/monniaux/ocaml/Makefile @@ -1,33 +1,6 @@ -ALL_CFLAGS=-Ibyterun +TARGET=ocaml +ALL_CFLAGS=-Ibyterun -lm +ALL_CFILES=$(wildcard byterun/*.c) EXECUTE_ARGS=examples/quicksort include ../rules.mk - -ALL_CCOMPFLAGS= -LDLIBS=-lm - -CFILES=$(wildcard byterun/*.c) - -CCOMP_K1C_S=$(patsubst %.c,%.ccomp.k1c.s,$(CFILES)) -CCOMP_HOST_S=$(patsubst %.c,%.ccomp.host.s,$(CFILES)) - -GCC_K1C_S=$(patsubst %.c,%.gcc.k1c.s,$(CFILES)) -GCC_O1_K1C_S=$(patsubst %.c,%.gcc.o1.k1c.s,$(CFILES)) -GCC_HOST_S=$(patsubst %.c,%.gcc.host.s,$(CFILES)) - -all: $(CCOMP_K1C_S) $(GCC_K1C_S) ocamlrun.ccomp.k1c.out ocamlrun.gcc.k1c.out ocamlrun.gcc.o1.k1c.out - -ocamlrun.ccomp.k1c : $(CCOMP_K1C_S) ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ $(LDLIBS) - -ocamlrun.ccomp.host : $(CCOMP_HOST_S) ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) $+ -o $@ $(LDLIBS) - -ocamlrun.gcc.k1c : $(GCC_K1C_S) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ $(LDLIBS) - -ocamlrun.gcc.o1.k1c : $(GCC_O1_K1C_S) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ $(LDLIBS) - -ocamlrun.gcc.host : $(GCC_HOST_S) ../clock.gcc.host.o - $(CC) $(CFLAGS) $+ -o $@ $(LDLIBS) diff --git a/test/monniaux/pcre2-10.32/Makefile b/test/monniaux/pcre2-10.32/Makefile index 98c2c8c2..b6b66c37 100644 --- a/test/monniaux/pcre2-10.32/Makefile +++ b/test/monniaux/pcre2-10.32/Makefile @@ -1,4 +1,7 @@ -CFILES = \ +TARGET=pcre2 +ALL_CFLAGS = -DHAVE_CONFIG_H -DPCRE2_CODE_UNIT_WIDTH=8 +EXECUTE_ARGS=testdata/testinput6 > /dev/null 2> __BASE__.out +ALL_CFILES = \ pcre2_auto_possess.c \ pcre2_chartables.c \ pcre2_compile.c \ @@ -28,39 +31,5 @@ CFILES = \ pcre2posix.c \ pcre2test.c -HFILES = config.h pcre2_internal.h pcre2posix.h \ -pcre2.h pcre2_intmodedep.h pcre2_ucp.h - -K1C_GCC_OFILES=$(CFILES:.c=.gcc.k1c.o) -K1C_GCC_OFILES_O1=$(CFILES:.c=.gcc.o1.k1c.o) -K1C_CCOMP_OFILES=$(CFILES:.c=.ccomp.k1c.o) -K1C_GCC_SFILES=$(CFILES:.c=.gcc.k1c.s) -K1C_CCOMP_SFILES=$(CFILES:.c=.ccomp.k1c.s) -HOST_GCC_OFILES=$(CFILES:.c=.gcc.host.o) - -all: pcre2test.gcc.o1.k1c.out pcre2test.gcc.k1c.out pcre2test.ccomp.k1c.out $(K1C_GCC_SFILES) $(K1C_CCOMP_SFILES) - -ALL_CFLAGS = -DHAVE_CONFIG_H -DPCRE2_CODE_UNIT_WIDTH=8 -EXECUTE_ARGS = testdata/testinput6 - include ../rules.mk - -$(K1C_GCC_SFILES) $(K1C_GCC_OFILES_O1) $(K1C_CCOMP_SFILES) $(HOST_GCC_OFILES): $(HFILES) - -pcre2test.gcc.host: $(HOST_GCC_OFILES) - $(CC) $(CFLAGS) -o $@ $+ ../clock.gcc.host.o - -pcre2test.gcc.k1c: $(K1C_GCC_OFILES) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) -o $@ $+ - -pcre2test.gcc.o1.k1c: $(K1C_GCC_OFILES_O1) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ - -pcre2test.ccomp.k1c: $(K1C_CCOMP_OFILES) ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ - -.PHONY: clean - -clean: - rm -f *.s *.o *.k1c diff --git a/test/monniaux/pcre2-10.32/pcre2test.c b/test/monniaux/pcre2-10.32/pcre2test.c index 25a7c4a1..a1fb64cb 100644 --- a/test/monniaux/pcre2-10.32/pcre2test.c +++ b/test/monniaux/pcre2-10.32/pcre2test.c @@ -8792,7 +8792,7 @@ FREECONTEXTS; #endif clock_stop(); - print_total_clock(); + printerr_total_clock(); return yield; } diff --git a/test/monniaux/picosat-965/Makefile b/test/monniaux/picosat-965/Makefile index 991278ff..a887c0de 100644 --- a/test/monniaux/picosat-965/Makefile +++ b/test/monniaux/picosat-965/Makefile @@ -1,37 +1,11 @@ EXECUTE_ARGS=sudoku.sat - -include ../rules.mk - -#ALL_CFLAGS = -DNDEBUG ALL_CFLAGS = -DNALARM -DNZIP -DNGETRUSAGE -DNDEBUG -K1C_CFLAGS += $(EMBEDDED_CFLAGS) -K1C_CCOMPFLAGS += $(EMBEDDED_CFLAGS) -CCOMPFLAGS += -fbitfields -K1C_CCOMPFLAGS += -fbitfields # -fno-if-conversion - -K1C_CFLAGS += $(ALL_CFLAGS) -K1C_CCOMPFLAGS += $(ALL_CFLAGS) -CCOMPFLAGS += $(ALL_CFLAGS) -CFLAGS += $(ALL_CFLAGS) - -all: picosat.ccomp.k1c.s version.ccomp.k1c.s app.ccomp.k1c.s main.ccomp.k1c.s picosat.gcc.k1c.s version.gcc.k1c.s app.gcc.k1c.s main.gcc.k1c.s picosat.ccomp.k1c.out picosat.gcc.o1.k1c.out picosat.gcc.k1c.out picosat picosat.ccomp.host.out picosat.gcc.host.out - -picosat.ccomp.k1c : picosat.ccomp.k1c.s version.ccomp.k1c.s app.ccomp.k1c.s main.ccomp.k1c.s ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ +ALL_CCOMPFLAGS += -fbitfields # -fno-if-conversion +TARGET=picosat +ALL_CFILES=picosat.c version.c app.c main.c -picosat.gcc.k1c : picosat.gcc.k1c.s version.gcc.k1c.s app.gcc.k1c.s main.gcc.k1c.s ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -picosat.gcc.o1.k1c : picosat.gcc.o1.k1c.s version.gcc.o1.k1c.s app.gcc.o1.k1c.s main.gcc.o1.k1c.s ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -picosat.ccomp.host : picosat.ccomp.host.s version.ccomp.host.s app.ccomp.host.s main.ccomp.host.s ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) $+ -o $@ - -picosat.gcc.host : picosat.gcc.host.s version.gcc.host.s app.gcc.host.s main.gcc.host.s ../clock.gcc.host.o - $(CC) $(FLAGS) $+ -o $@ - -clean: - -rm -f *.s *.k1c *.out +include ../rules.mk -.PHONY: clean +# FIXME - what were these for? +#K1C_CFLAGS += $(EMBEDDED_CFLAGS) +#K1C_CCOMPFLAGS += $(EMBEDDED_CFLAGS) diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk index 9d05b4d6..2de2c466 100644 --- a/test/monniaux/rules.mk +++ b/test/monniaux/rules.mk @@ -7,6 +7,9 @@ ALL_CFILES?=$(wildcard *.c) # Name of the target TARGET?=toto +# Arguments of execution +EXECUTE_ARGS?= + # Name of the clock object CLOCK=../clock @@ -25,30 +28,31 @@ K1C_CC?=k1-cos-gcc K1C_CCOMP?=ccomp # Command to execute +#EXECUTE_CYCLES?=timeout --signal=SIGTERM 3m k1-cluster --syscall=libstd_scalls.so --cycle-based -- EXECUTE_CYCLES?=k1-cluster --syscall=libstd_scalls.so --cycle-based -- # You can define up to GCC4FLAGS and CCOMP4FLAGS -GCC0FLAGS?= -GCC1FLAGS?=$(ALL_GCCFLAGS) -O1 -g +GCC0FLAGS?=$(ALL_GCCFLAGS) -O0 +GCC1FLAGS?=$(ALL_GCCFLAGS) -O1 GCC2FLAGS?=$(ALL_GCCFLAGS) -O2 GCC3FLAGS?=$(ALL_GCCFLAGS) -O3 GCC4FLAGS?= -CCOMP0FLAGS?= -CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -O1 -g -CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) -CCOMP3FLAGS?= +CCOMP0FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fno-postpass +CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fpostpass= greedy +CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fno-if-conversion +CCOMP3FLAGS?=$(ALL_CCOMPFLAGS) -O2 CCOMP4FLAGS?= # Prefix names -GCC0PREFIX?= +GCC0PREFIX?=.gcc.o0 GCC1PREFIX?=.gcc.o1 GCC2PREFIX?=.gcc.o2 GCC3PREFIX?=.gcc.o3 GCC4PREFIX?= -CCOMP0PREFIX?= -CCOMP1PREFIX?=.ccomp.o1 -CCOMP2PREFIX?=.ccomp.o2 -CCOMP3PREFIX?= +CCOMP0PREFIX?=.ccomp.nobundle +CCOMP1PREFIX?=.ccomp.greedy +CCOMP2PREFIX?=.ccomp.noif +CCOMP3PREFIX?=.ccomp CCOMP4PREFIX?= # List of outfiles, updated by gen_rules @@ -92,7 +96,8 @@ obj/%.o: asm/%.s out/%.out: bin/%.bin @mkdir -p $(@D) - $(EXECUTE_CYCLES) $< | tee $@ + @rm -f $@ + $(EXECUTE_CYCLES) $< $(subst __BASE__,$(patsubst %.out,%,$@),$(EXECUTE_ARGS)) | tee -a $@ ## # Generating the rules for all the compiler/flags.. @@ -132,7 +137,7 @@ endif measures.csv: $(OUTFILES) @echo $(FIRSTLINE) > $@ - @for i in $(MEASURES); do\ + @for i in "$(MEASURES)"; do\ first=$$(grep "$$i cycles" $(firstword $(OUTFILES)));\ if test ! -z "$$first"; then\ if [ "$$i" != "time" ]; then\ @@ -153,5 +158,5 @@ run: measures.csv clean: rm -f *.o *.s *.bin *.out - rm -f asm/*.s bin/*.bin obj/*.o out/*.out + rm -rf asm/ bin/ obj/ out/ diff --git a/test/monniaux/run_benches.sh b/test/monniaux/run_benches.sh index 5f9f22cb..2b2e28d6 100755 --- a/test/monniaux/run_benches.sh +++ b/test/monniaux/run_benches.sh @@ -1,12 +1,16 @@ source benches.sh +cores=$(grep -c ^processor /proc/cpuinfo) +processes=$((cores/4)) + rm -f commands.txt for bench in $benches; do - echo "(cd $bench && make -j5 run)" >> commands.txt + echo "(cd $bench && echo \"Running $bench..\" &&\ + make -j4 run > /dev/null && echo \"$bench DONE\")" >> commands.txt done -cat commands.txt | xargs -n1 -I{} -P4 bash -c '{}' +cat commands.txt | xargs -n1 -I{} -P$processes bash -c '{}' ## # Gather all the CSV files diff --git a/test/monniaux/tiff-4.0.10/Makefile b/test/monniaux/tiff-4.0.10/Makefile index db3428fa..ac1aa276 100644 --- a/test/monniaux/tiff-4.0.10/Makefile +++ b/test/monniaux/tiff-4.0.10/Makefile @@ -1,52 +1,7 @@ +TARGET=ppm2tiff +ALL_CFLAGS=-lm ALL_CCOMPFLAGS = -flongdouble +EXECUTE_ARGS= -c g3 __BASE__.g3.tif < example_bw.pbm include ../rules.mk -LIBS=-lm - -src=$(wildcard *.c) - -PRODUCTS?=ppm2tiff.gcc.host ppm2tiff.ccomp.host ppm2tiff.gcc.k1c ppm2tiff.gcc.o1.k1c ppm2tiff.ccomp.k1c -PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS)) - -all: $(PRODUCTS) - -.PHONY: -run: measures.csv - -ppm2tiff.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o - $(CC) $(CFLAGS) $+ $(LIBS) -o $@ -ppm2tiff.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) $+ $(LIBS) -o $@ -ppm2tiff.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ $(LIBS) -o $@ -ppm2tiff.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ $(LIBS) -o $@ -ppm2tiff.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ $(LIBS) -o $@ - -ppm2tiff.gcc.host.out: ppm2tiff.gcc.host - bunzip2 < example_bw.pbm.bz2 | ./$< -c g3 $<.g3.tif | tee $@ - -ppm2tiff.ccomp.host.out: ppm2tiff.ccomp.host - bunzip2 < example_bw.pbm.bz2 | ./$< -c g3 $<.g3.tif | tee $@ - -ppm2tiff.gcc.k1c.out: ppm2tiff.gcc.k1c - bunzip2 < example_bw.pbm.bz2 | $(EXECUTE_CYCLES) ./$< -c g3 $<.g3.tif | tee $@ - -ppm2tiff.gcc.o1.k1c.out: ppm2tiff.gcc.o1.k1c - bunzip2 < example_bw.pbm.bz2 | $(EXECUTE_CYCLES) ./$< -c g3 $<.g3.tif | tee $@ - -ppm2tiff.ccomp.k1c.out: ppm2tiff.ccomp.k1c - bunzip2 < example_bw.pbm.bz2 | $(EXECUTE_CYCLES) ./$< -c g3 $<.g3.tif | tee $@ - -measures.csv: $(PRODUCTS_OUT) - echo "benches, gcc host,ccomp host,gcc k1c,gcc o1 k1c,ccomp k1c" > $@ - echo "ppm2tiff ", $$(grep 'cycles' ppm2tiff.gcc.host.out | cut -d':' -f2), $$(grep 'cycles' ppm2tiff.ccomp.host.out | cut -d':' -f2), $$(grep 'cycles' ppm2tiff.gcc.k1c.out | cut -d':' -f2), $$(grep 'cycles' ppm2tiff.gcc.o1.k1c.out | cut -d':' -f2), $$(grep 'cycles' ppm2tiff.ccomp.k1c.out | cut -d':' -f2)>> $@ - -.SECONDARY: - -.PHONY: -clean: - rm -f *.o *.s *.k1c *.csv - diff --git a/test/monniaux/tiff-4.0.10/example_bw.pbm b/test/monniaux/tiff-4.0.10/example_bw.pbm Binary files differnew file mode 100644 index 00000000..971a82bb --- /dev/null +++ b/test/monniaux/tiff-4.0.10/example_bw.pbm diff --git a/test/monniaux/zlib-1.2.11/Makefile b/test/monniaux/zlib-1.2.11/Makefile index 202f2ea4..9e6920f5 100644 --- a/test/monniaux/zlib-1.2.11/Makefile +++ b/test/monniaux/zlib-1.2.11/Makefile @@ -1,53 +1,62 @@ -ALL_CCOMPFLAGS = -faddx -ALL_CFLAGS = -D_POSIX_C_SOURCE=2 -D_LARGEFILE64_SOURCE=1 -U__STRICT_ANSI__ +TARGET=zlib -include ../rules.mk - -src=$(wildcard *.c) - -PRODUCTS?=minigzip.gcc.host minigzip.ccomp.host minigzip.gcc.k1c minigzip.gcc.o1.k1c minigzip.ccomp.k1c -PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS)) - -all: $(PRODUCTS) - -.PHONY: -run: measures.csv - - -minigzip.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o - $(CC) $(CFLAGS) $+ -lm -o $@ -minigzip.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) $+ -lm -o $@ -minigzip.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -lm -o $@ -minigzip.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -lm -o $@ -minigzip.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -lm -o $@ -measures.csv: $(PRODUCTS_OUT) - echo "benches, gcc host,ccomp host,gcc k1c,gcc o1 k1c,ccomp k1c" > $@ - echo "zlib ", $$(grep 'cycles' minigzip.gcc.host.out | cut -d':' -f2), $$(grep 'cycles' minigzip.ccomp.host.out | cut -d':' -f2), $$(grep 'cycles' minigzip.gcc.k1c.out | cut -d':' -f2), $$(grep 'cycles' minigzip.gcc.o1.k1c.out | cut -d':' -f2), $$(grep 'cycles' minigzip.ccomp.k1c.out | cut -d':' -f2)>> $@ +ALL_CCOMPFLAGS=-faddx +ALL_CFLAGS= -D_POSIX_C_SOURCE=2 -D_LARGEFILE64_SOURCE=1 -U__STRICT_ANSI__ +EXECUTE_ARGS=< zlib_small.txt > /dev/null 2> __BASE__.out -SAMPLE_FILE=zlib.h - -minigzip.gcc.host.out minigzip.gcc.host.output: minigzip.gcc.host - ./$< < $(SAMPLE_FILE) > $<.output 2> $@ - -minigzip.ccomp.host.out minigzip.ccomp.host.output: minigzip.ccomp.host - ./$< < $(SAMPLE_FILE) > $<.output 2> $@ - -minigzip.gcc.k1c.out minigzip.gcc.k1c.output: minigzip.gcc.k1c - $(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@ - -minigzip.gcc.o1.k1c.out minigzip.gcc.o1.k1c.output: minigzip.gcc.o1.k1c - $(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@ - -minigzip.ccomp.k1c.out minigzip.ccomp.k1c.output: minigzip.ccomp.k1c - $(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@ - -.SECONDARY: +include ../rules.mk -.PHONY: -clean: - rm -f *.o *.s *.k1c *.csv +#ALL_CCOMPFLAGS = -faddx +#ALL_CFLAGS = -D_POSIX_C_SOURCE=2 -D_LARGEFILE64_SOURCE=1 -U__STRICT_ANSI__ +# +#include ../rules.mk +# +#src=$(wildcard *.c) +# +#PRODUCTS?=minigzip.gcc.host minigzip.ccomp.host minigzip.gcc.k1c minigzip.gcc.o1.k1c minigzip.ccomp.k1c +#PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS)) +# +#all: $(PRODUCTS) +# +#.PHONY: +#run: measures.csv +# +# +#minigzip.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o +# $(CC) $(CFLAGS) $+ -lm -o $@ +#minigzip.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o +# $(CCOMP) $(CCOMPFLAGS) $+ -lm -o $@ +#minigzip.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o +# $(K1C_CC) $(K1C_CFLAGS) $+ -lm -o $@ +#minigzip.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o +# $(K1C_CC) $(K1C_CFLAGS_O1) $+ -lm -o $@ +#minigzip.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o +# $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -lm -o $@ +#measures.csv: $(PRODUCTS_OUT) +# echo "benches, gcc host,ccomp host,gcc k1c,gcc o1 k1c,ccomp k1c" > $@ +# echo "zlib ", $$(grep 'cycles' minigzip.gcc.host.out | cut -d':' -f2), $$(grep 'cycles' minigzip.ccomp.host.out | cut -d':' -f2), $$(grep 'cycles' minigzip.gcc.k1c.out | cut -d':' -f2), $$(grep 'cycles' minigzip.gcc.o1.k1c.out | cut -d':' -f2), $$(grep 'cycles' minigzip.ccomp.k1c.out | cut -d':' -f2)>> $@ +# +#SAMPLE_FILE=zlib.h +# +#minigzip.gcc.host.out minigzip.gcc.host.output: minigzip.gcc.host +# ./$< < $(SAMPLE_FILE) > $<.output 2> $@ +# +#minigzip.ccomp.host.out minigzip.ccomp.host.output: minigzip.ccomp.host +# ./$< < $(SAMPLE_FILE) > $<.output 2> $@ +# +#minigzip.gcc.k1c.out minigzip.gcc.k1c.output: minigzip.gcc.k1c +# $(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@ +# +#minigzip.gcc.o1.k1c.out minigzip.gcc.o1.k1c.output: minigzip.gcc.o1.k1c +# $(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@ +# +#minigzip.ccomp.k1c.out minigzip.ccomp.k1c.output: minigzip.ccomp.k1c +# $(EXECUTE_CYCLES) $< < $(SAMPLE_FILE) > $<.output 2> $@ +# +#.SECONDARY: +# +#.PHONY: +#clean: +# rm -f *.o *.s *.k1c *.csv +# diff --git a/test/monniaux/zlib-1.2.11/zlib_small.txt b/test/monniaux/zlib-1.2.11/zlib_small.txt new file mode 100644 index 00000000..2c494200 --- /dev/null +++ b/test/monniaux/zlib-1.2.11/zlib_small.txt @@ -0,0 +1,539 @@ + + + +#ifndef ZLIB_H +#define ZLIB_H + +#include "zconf.h" + +#ifdef __cplusplus +extern "C" { +#endif + +#define ZLIB_VERSION "1.2.11" +#define ZLIB_VERNUM 0x12b0 +#define ZLIB_VER_MAJOR 1 +#define ZLIB_VER_MINOR 2 +#define ZLIB_VER_REVISION 11 +#define ZLIB_VER_SUBREVISION 0 + + + + +typedef voidpf (*alloc_func) OF((voidpf opaque, uInt items, uInt size)); +typedef void (*free_func) OF((voidpf opaque, voidpf address)); + +struct internal_state; + +typedef struct z_stream_s { + z_const Bytef *next_in; + + uLong total_in; + + uInt avail_out; + + + z_const char *msg; + + + alloc_func zalloc; + + voidpf opaque; + + uLong adler; + +} z_stream; + +typedef z_stream FAR *z_streamp; + + + +typedef struct gz_header_s { + int text; + + int xflags; + + Bytef *extra; + + uInt extra_max; + + uInt name_max; + + uInt comm_max; + + int done; + +} gz_header; + +typedef gz_header FAR *gz_headerp; + + + + + + + +#define Z_OK 0 +#define Z_STREAM_END 1 +#define Z_NEED_DICT 2 +#define Z_ERRNO (-1) +#define Z_STREAM_ERROR (-2) +#define Z_DATA_ERROR (-3) +#define Z_MEM_ERROR (-4) +#define Z_BUF_ERROR (-5) +#define Z_VERSION_ERROR (-6) + + + +#define Z_NO_COMPRESSION 0 +#define Z_BEST_SPEED 1 +#define Z_BEST_COMPRESSION 9 +#define Z_DEFAULT_COMPRESSION (-1) + + + +#define Z_BINARY 0 +#define Z_TEXT 1 +#define Z_ASCII Z_TEXT + + +#define Z_DEFLATED 8 + + + +#define zlib_version zlibVersion() + + + +ZEXTERN const char * ZEXPORT zlibVersion OF((void)); + + + + + + + +ZEXTERN int ZEXPORT deflate OF((z_streamp strm, int flush)); + + + + +ZEXTERN int ZEXPORT deflateEnd OF((z_streamp strm)); + + + + + + + + +ZEXTERN int ZEXPORT inflate OF((z_streamp strm, int flush)); + + + + +ZEXTERN int ZEXPORT inflateEnd OF((z_streamp strm)); + + + + + + + + + + +ZEXTERN int ZEXPORT deflateSetDictionary OF((z_streamp strm, + const Bytef *dictionary, + uInt dictLength)); + + + +ZEXTERN int ZEXPORT deflateGetDictionary OF((z_streamp strm, + Bytef *dictionary, + uInt *dictLength)); + + + +ZEXTERN int ZEXPORT deflateCopy OF((z_streamp dest, + z_streamp source)); + + + +ZEXTERN int ZEXPORT deflateReset OF((z_streamp strm)); + + + +ZEXTERN int ZEXPORT deflateParams OF((z_streamp strm, + int level, + int strategy)); + + + +ZEXTERN int ZEXPORT deflateTune OF((z_streamp strm, + int good_length, + int max_lazy, + int nice_length, + int max_chain)); + + + +ZEXTERN uLong ZEXPORT deflateBound OF((z_streamp strm, + uLong sourceLen)); + + + +ZEXTERN int ZEXPORT deflatePending OF((z_streamp strm, + unsigned *pending, + int *bits)); + + + +ZEXTERN int ZEXPORT deflatePrime OF((z_streamp strm, + int bits, + int value)); + + + +ZEXTERN int ZEXPORT deflateSetHeader OF((z_streamp strm, + gz_headerp head)); + + + + + + +ZEXTERN int ZEXPORT inflateSetDictionary OF((z_streamp strm, + const Bytef *dictionary, + uInt dictLength)); + + + +ZEXTERN int ZEXPORT inflateGetDictionary OF((z_streamp strm, + Bytef *dictionary, + uInt *dictLength)); + + + +ZEXTERN int ZEXPORT inflateSync OF((z_streamp strm)); + + + +ZEXTERN int ZEXPORT inflateCopy OF((z_streamp dest, + z_streamp source)); + + + +ZEXTERN int ZEXPORT inflateReset OF((z_streamp strm)); + + + +ZEXTERN int ZEXPORT inflateReset2 OF((z_streamp strm, + int windowBits)); + + + +ZEXTERN int ZEXPORT inflatePrime OF((z_streamp strm, + int bits, + int value)); + + + +ZEXTERN long ZEXPORT inflateMark OF((z_streamp strm)); + + + +ZEXTERN int ZEXPORT inflateGetHeader OF((z_streamp strm, + gz_headerp head)); + + + + + + +typedef unsigned (*in_func) OF((void FAR *, + z_const unsigned char FAR * FAR *)); +typedef int (*out_func) OF((void FAR *, unsigned char FAR *, unsigned)); + +ZEXTERN int ZEXPORT inflateBack OF((z_streamp strm, + in_func in, void FAR *in_desc, + out_func out, void FAR *out_desc)); + + + +ZEXTERN int ZEXPORT inflateBackEnd OF((z_streamp strm)); + + + +ZEXTERN uLong ZEXPORT zlibCompileFlags OF((void)); + + + +#ifndef Z_SOLO + + + + +ZEXTERN int ZEXPORT compress OF((Bytef *dest, uLongf *destLen, + const Bytef *source, uLong sourceLen)); + + + +ZEXTERN int ZEXPORT compress2 OF((Bytef *dest, uLongf *destLen, + const Bytef *source, uLong sourceLen, + int level)); + + + +ZEXTERN uLong ZEXPORT compressBound OF((uLong sourceLen)); + + + +ZEXTERN int ZEXPORT uncompress OF((Bytef *dest, uLongf *destLen, + const Bytef *source, uLong sourceLen)); + + + +ZEXTERN int ZEXPORT uncompress2 OF((Bytef *dest, uLongf *destLen, + const Bytef *source, uLong *sourceLen)); + + + + + + +typedef struct gzFile_s *gzFile; + + +ZEXTERN gzFile ZEXPORT gzdopen OF((int fd, const char *mode)); + + + +ZEXTERN int ZEXPORT gzbuffer OF((gzFile file, unsigned size)); + + + +ZEXTERN int ZEXPORT gzsetparams OF((gzFile file, int level, int strategy)); + + + +ZEXTERN int ZEXPORT gzread OF((gzFile file, voidp buf, unsigned len)); + + + +ZEXTERN z_size_t ZEXPORT gzfread OF((voidp buf, z_size_t size, z_size_t nitems, + gzFile file)); + + + +ZEXTERN int ZEXPORT gzwrite OF((gzFile file, + voidpc buf, unsigned len)); + + + +ZEXTERN z_size_t ZEXPORT gzfwrite OF((voidpc buf, z_size_t size, + z_size_t nitems, gzFile file)); + + + +ZEXTERN int ZEXPORTVA gzprintf Z_ARG((gzFile file, const char *format, ...)); + + + +ZEXTERN int ZEXPORT gzputs OF((gzFile file, const char *s)); + + + +ZEXTERN char * ZEXPORT gzgets OF((gzFile file, char *buf, int len)); + + + +ZEXTERN int ZEXPORT gzputc OF((gzFile file, int c)); + + + +ZEXTERN int ZEXPORT gzgetc OF((gzFile file)); + + + +ZEXTERN int ZEXPORT gzungetc OF((int c, gzFile file)); + + + +ZEXTERN int ZEXPORT gzflush OF((gzFile file, int flush)); + + + + + + +ZEXTERN int ZEXPORT gzrewind OF((gzFile file)); + + + + + + + + + +ZEXTERN int ZEXPORT gzeof OF((gzFile file)); + + + +ZEXTERN int ZEXPORT gzdirect OF((gzFile file)); + + + +ZEXTERN int ZEXPORT gzclose OF((gzFile file)); + + + +ZEXTERN int ZEXPORT gzclose_r OF((gzFile file)); +ZEXTERN int ZEXPORT gzclose_w OF((gzFile file)); + + + +ZEXTERN const char * ZEXPORT gzerror OF((gzFile file, int *errnum)); + + + +ZEXTERN void ZEXPORT gzclearerr OF((gzFile file)); + + + +#endif + + + + + +ZEXTERN uLong ZEXPORT adler32 OF((uLong adler, const Bytef *buf, uInt len)); + + + +ZEXTERN uLong ZEXPORT adler32_z OF((uLong adler, const Bytef *buf, + z_size_t len)); + + + + + + +ZEXTERN uLong ZEXPORT crc32 OF((uLong crc, const Bytef *buf, uInt len)); + + + +ZEXTERN uLong ZEXPORT crc32_z OF((uLong adler, const Bytef *buf, + z_size_t len)); + + + + + + + + + +ZEXTERN int ZEXPORT deflateInit_ OF((z_streamp strm, int level, + const char *version, int stream_size)); +ZEXTERN int ZEXPORT inflateInit_ OF((z_streamp strm, + const char *version, int stream_size)); +ZEXTERN int ZEXPORT deflateInit2_ OF((z_streamp strm, int level, int method, + int windowBits, int memLevel, + int strategy, const char *version, + int stream_size)); +ZEXTERN int ZEXPORT inflateInit2_ OF((z_streamp strm, int windowBits, + const char *version, int stream_size)); +ZEXTERN int ZEXPORT inflateBackInit_ OF((z_streamp strm, int windowBits, + unsigned char FAR *window, + const char *version, + int stream_size)); +#ifdef Z_PREFIX_SET +# define z_deflateInit(strm, level) \ + deflateInit_((strm), (level), ZLIB_VERSION, (int)sizeof(z_stream)) +# define z_inflateInit(strm) \ + inflateInit_((strm), ZLIB_VERSION, (int)sizeof(z_stream)) +# define z_deflateInit2(strm, level, method, windowBits, memLevel, strategy) \ + deflateInit2_((strm),(level),(method),(windowBits),(memLevel),\ + (strategy), ZLIB_VERSION, (int)sizeof(z_stream)) +# define z_inflateInit2(strm, windowBits) \ + inflateInit2_((strm), (windowBits), ZLIB_VERSION, \ + (int)sizeof(z_stream)) +# define z_inflateBackInit(strm, windowBits, window) \ + inflateBackInit_((strm), (windowBits), (window), \ + ZLIB_VERSION, (int)sizeof(z_stream)) +#else +# define deflateInit(strm, level) \ + deflateInit_((strm), (level), ZLIB_VERSION, (int)sizeof(z_stream)) +# define inflateInit(strm) \ + inflateInit_((strm), ZLIB_VERSION, (int)sizeof(z_stream)) +# define deflateInit2(strm, level, method, windowBits, memLevel, strategy) \ + deflateInit2_((strm),(level),(method),(windowBits),(memLevel),\ + (strategy), ZLIB_VERSION, (int)sizeof(z_stream)) +# define inflateInit2(strm, windowBits) \ + inflateInit2_((strm), (windowBits), ZLIB_VERSION, \ + (int)sizeof(z_stream)) +# define inflateBackInit(strm, windowBits, window) \ + inflateBackInit_((strm), (windowBits), (window), \ + ZLIB_VERSION, (int)sizeof(z_stream)) +#endif + +#ifndef Z_SOLO + + + +struct gzFile_s { + unsigned have; + unsigned char *next; + z_off64_t pos; +}; +ZEXTERN int ZEXPORT gzgetc_ OF((gzFile file)); + +#ifdef Z_LARGE64 + ZEXTERN gzFile ZEXPORT gzopen64 OF((const char *, const char *)); + ZEXTERN z_off64_t ZEXPORT gzseek64 OF((gzFile, z_off64_t, int)); + ZEXTERN z_off64_t ZEXPORT gztell64 OF((gzFile)); + ZEXTERN z_off64_t ZEXPORT gzoffset64 OF((gzFile)); + ZEXTERN uLong ZEXPORT adler32_combine64 OF((uLong, uLong, z_off64_t)); + ZEXTERN uLong ZEXPORT crc32_combine64 OF((uLong, uLong, z_off64_t)); +#endif + +#if !defined(ZLIB_INTERNAL) && defined(Z_WANT64) +# ifdef Z_PREFIX_SET +# define z_gzopen z_gzopen64 +# define z_gzseek z_gzseek64 +# define z_gztell z_gztell64 +# define z_gzoffset z_gzoffset64 +# define z_adler32_combine z_adler32_combine64 +# define z_crc32_combine z_crc32_combine64 +# else +# define gzopen gzopen64 +# define gzseek gzseek64 +# define gztell gztell64 +# define gzoffset gzoffset64 +# define adler32_combine adler32_combine64 +# define crc32_combine crc32_combine64 +# endif +# ifndef Z_LARGE64 + ZEXTERN gzFile ZEXPORT gzopen64 OF((const char *, const char *)); + ZEXTERN z_off_t ZEXPORT gzseek64 OF((gzFile, z_off_t, int)); + ZEXTERN z_off_t ZEXPORT gztell64 OF((gzFile)); + ZEXTERN z_off_t ZEXPORT gzoffset64 OF((gzFile)); + ZEXTERN uLong ZEXPORT adler32_combine64 OF((uLong, uLong, z_off_t)); + ZEXTERN uLong ZEXPORT crc32_combine64 OF((uLong, uLong, z_off_t)); +# endif +#else + ZEXTERN gzFile ZEXPORT gzopen OF((const char *, const char *)); + ZEXTERN z_off_t ZEXPORT gzseek OF((gzFile, z_off_t, int)); + ZEXTERN z_off_t ZEXPORT gztell OF((gzFile)); + ZEXTERN z_off_t ZEXPORT gzoffset OF((gzFile)); + ZEXTERN uLong ZEXPORT adler32_combine OF((uLong, uLong, z_off_t)); + ZEXTERN uLong ZEXPORT crc32_combine OF((uLong, uLong, z_off_t)); +#endif + +#else + + + + diff --git a/test/regression/Makefile b/test/regression/Makefile index 585ffb1c..3447d6a5 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -10,7 +10,7 @@ LIBS=$(LIBMATH) # Can run, both in compiled mode and in interpreter mode, # and have reference output in Results -TESTS=int32 int64 floats floats-basics floats-lit \ +TESTS?=int32 int64 floats floats-basics floats-lit \ expr1 expr6 funptr2 initializers initializers2 initializers3 \ volatile1 volatile2 volatile3 volatile4 \ funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \ diff --git a/test/regression/extasm.c b/test/regression/extasm.c index 8abeb98f..352b930b 100644 --- a/test/regression/extasm.c +++ b/test/regression/extasm.c @@ -24,7 +24,7 @@ int clobbers(int x, int z) || (defined(ARCH_riscV) && defined(MODEL_64)) \ || (defined(ARCH_powerpc) && defined(MODEL_ppc64)) \ || (defined(ARCH_powerpc) && defined(MODEL_e5500)) \ - || (defined(ARCH_mppa_k1c) && defined(MODEL_64)) + || (defined(ARCH_mppa_k1c) && defined(MODEL_64)) \ || defined(ARCH_aarch64) #define SIXTYFOUR #else |