diff options
| -rw-r--r-- | aarch64/TargetPrinter.ml | 5 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 5 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 83 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 4 | ||||
| -rw-r--r-- | cfrontend/SimplExprspec.v | 176 | ||||
| -rw-r--r-- | lib/Printlines.ml | 10 | ||||
| -rw-r--r-- | riscV/TargetPrinter.ml | 5 | ||||
| -rw-r--r-- | test/regression/Makefile | 2 | ||||
| -rw-r--r-- | test/regression/Results/telescopes | 7 | ||||
| -rw-r--r-- | test/regression/telescopes.c | 47 | ||||
| -rw-r--r-- | x86/TargetPrinter.ml | 5 |
11 files changed, 242 insertions, 107 deletions
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index cde5668b..664110d1 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -164,7 +164,10 @@ module ELF_System : SYSTEM = | Section_data i | Section_small_data i -> variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - variable_section ~sec:".section .rodata" i + variable_section + ~sec:".section .rodata" + ~reloc:".section .data.rel.ro,\"aw\",@progbits" + i | Section_string sz -> elf_mergeable_string_section sz ".section .rodata" | Section_literal sz -> diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 20ca59d6..b6362ca9 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -150,7 +150,10 @@ struct | Section_data i | Section_small_data i -> variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - variable_section ~sec:".section .rodata" i + variable_section + ~sec:".section .rodata" + ~reloc:".section .data.rel.ro,\"aw\",%progbits" + i | Section_string _ -> ".section .rodata" | Section_literal _ -> ".text" | Section_jumptable -> ".text" diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index cf5dd6d1..1db62013 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -251,20 +251,14 @@ Definition make_assign_value (bf: bitfield) (r: expr): expr := | Bits sz sg pos width => make_normalize sz sg width r end. -(** Translation of expressions. Return a pair [(sl, a)] of - a list of statements [sl] and a pure expression [a]. -- If the [dst] argument is [For_val], the statements [sl] - perform the side effects of the original expression, - and [a] evaluates to the same value as the original expression. -- If the [dst] argument is [For_effects], the statements [sl] - perform the side effects of the original expression, - and [a] is meaningless. -- If the [dst] argument is [For_set tyl tvar], the statements [sl] - perform the side effects of the original expression, then - assign the value of the original expression to the temporary [tvar]. - The value is casted according to the list of types [tyl] before - assignment. In this case, [a] is meaningless. -*) +(** The destinations for evaluating an expression. +- [For_val]: evaluate the expression for its side effects and its final value. +- [For_effects]: evaluate the expression for its side effects only; + the final value is ignored. +- [For_set dest]: evaluate the expression for its side effects and its value, + then cast and assign its value to temporaries as described in [dest], + which is a nonempty list of (destination-type, source-type, temporary-name) + triples. *) Inductive set_destination : Type := | SDbase (tycast ty: type) (tmp: ident) @@ -277,12 +271,16 @@ Inductive destination : Type := Definition dummy_expr := Econst_int Int.zero type_int32s. +(** Perform the assignments described by [sd]. *) + Fixpoint do_set (sd: set_destination) (a: expr) : list statement := match sd with | SDbase tycast ty tmp => Sset tmp (Ecast a tycast) :: nil | SDcons tycast ty tmp sd' => Sset tmp (Ecast a tycast) :: do_set sd' (Etempvar tmp ty) end. +(** Perform the assignments described by [dst], if any. *) + Definition finish (dst: destination) (sl: list statement) (a: expr) := match dst with | For_val => (sl, a) @@ -290,12 +288,35 @@ Definition finish (dst: destination) (sl: list statement) (a: expr) := | For_set sd => (sl ++ do_set sd a, a) end. +(** Smart constructor for destinations. + For chained assignments, better code is generated eventually + if the same temporary is reused. However, temporaries must have + unique types, otherwise Cminor type reconstruction can fail, + hence reuse is restricted to the case where the new type + and the original type coincide. *) + Definition sd_temp (sd: set_destination) := match sd with SDbase _ _ tmp => tmp | SDcons _ _ tmp _ => tmp end. -Definition sd_seqbool_val (tmp: ident) (ty: type) := - SDbase type_bool ty tmp. -Definition sd_seqbool_set (ty: type) (sd: set_destination) := - let tmp := sd_temp sd in SDcons type_bool ty tmp sd. + +Definition sd_head_type (sd: set_destination) := + match sd with SDbase _ ty _ => ty | SDcons _ ty _ _ => ty end. + +Definition temp_for_sd (ty: type) (sd: set_destination) : mon ident := + if type_eq ty (sd_head_type sd) then ret (sd_temp sd) else gensym ty. + +(** Translation of expressions. Return a pair [(sl, a)] of + a list of statements [sl] and a pure expression [a]. +- If the [dst] argument is [For_val], the statements [sl] + perform the side effects of the original expression, + and [a] evaluates to the same value as the original expression. +- If the [dst] argument is [For_effects], the statements [sl] + perform the side effects of the original expression, + and [a] is meaningless. +- If the [dst] argument is [For_set sd], the statements [sl] + perform the side effects of the original expression, then + assign the value of the original expression to one or several + temporaries, as described by the destination [sd]. +*) Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) := match a with @@ -350,7 +371,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement match dst with | For_val => do t <- gensym ty; - do (sl2, a2) <- transl_expr (For_set (sd_seqbool_val t ty)) r2; + let sd := SDbase type_bool ty t in + do (sl2, a2) <- transl_expr (For_set sd) r2; ret (sl1 ++ makeif a1 (makeseq sl2) (Sset t (Econst_int Int.zero ty)) :: nil, Etempvar t ty) @@ -358,7 +380,9 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement do (sl2, a2) <- transl_expr For_effects r2; ret (sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil, dummy_expr) | For_set sd => - do (sl2, a2) <- transl_expr (For_set (sd_seqbool_set ty sd)) r2; + do t <- temp_for_sd ty sd; + let sd' := SDcons type_bool ty t sd in + do (sl2, a2) <- transl_expr (For_set sd') r2; ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq (do_set sd (Econst_int Int.zero ty))) :: nil, dummy_expr) @@ -368,7 +392,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement match dst with | For_val => do t <- gensym ty; - do (sl2, a2) <- transl_expr (For_set (sd_seqbool_val t ty)) r2; + let sd := SDbase type_bool ty t in + do (sl2, a2) <- transl_expr (For_set sd) r2; ret (sl1 ++ makeif a1 (Sset t (Econst_int Int.one ty)) (makeseq sl2) :: nil, Etempvar t ty) @@ -376,7 +401,9 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement do (sl2, a2) <- transl_expr For_effects r2; ret (sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil, dummy_expr) | For_set sd => - do (sl2, a2) <- transl_expr (For_set (sd_seqbool_set ty sd)) r2; + do t <- temp_for_sd ty sd; + let sd' := SDcons type_bool ty t sd in + do (sl2, a2) <- transl_expr (For_set sd') r2; ret (sl1 ++ makeif a1 (makeseq (do_set sd (Econst_int Int.one ty))) (makeseq sl2) :: nil, dummy_expr) @@ -386,8 +413,9 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement match dst with | For_val => do t <- gensym ty; - do (sl2, a2) <- transl_expr (For_set (SDbase ty ty t)) r2; - do (sl3, a3) <- transl_expr (For_set (SDbase ty ty t)) r3; + let sd := SDbase ty ty t in + do (sl2, a2) <- transl_expr (For_set sd) r2; + do (sl3, a3) <- transl_expr (For_set sd) r3; ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil, Etempvar t ty) | For_effects => @@ -396,9 +424,10 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil, dummy_expr) | For_set sd => - do t <- gensym ty; - do (sl2, a2) <- transl_expr (For_set (SDcons ty ty t sd)) r2; - do (sl3, a3) <- transl_expr (For_set (SDcons ty ty t sd)) r3; + do t <- temp_for_sd ty sd; + let sd' := SDcons ty ty t sd in + do (sl2, a2) <- transl_expr (For_set sd') r2; + do (sl3, a3) <- transl_expr (For_set sd') r3; ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil, dummy_expr) end diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index ea89a8ba..2aed0cdf 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1611,7 +1611,7 @@ Ltac NOTIN := apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto. + apply S. apply tr_paren_set with (a1 := a2) (t := t); auto. apply tr_expr_monotone with tmp2; eauto. auto. auto. - (* seqand false *) exploit tr_top_leftcontext; eauto. clear TR. @@ -1720,7 +1720,7 @@ Ltac NOTIN := apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto. + apply S. apply tr_paren_set with (a1 := a2) (t := t); auto. apply tr_expr_monotone with tmp2; eauto. auto. auto. - (* condition *) exploit tr_top_leftcontext; eauto. clear TR. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index b689bdeb..1e2b4409 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -137,7 +137,7 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> (Ecast a1 ty) tmp | tr_seqand_val: forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> - tr_expr le (For_set (sd_seqbool_val t ty)) e2 sl2 a2 tmp2 -> + tr_expr le (For_set (SDbase type_bool ty t)) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> tr_expr le For_val (Csyntax.Eseqand e1 e2 ty) @@ -152,18 +152,18 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> tr_expr le For_effects (Csyntax.Eseqand e1 e2 ty) (sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil) any tmp - | tr_seqand_set: forall le sd e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp, + | tr_seqand_set: forall le sd e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> - tr_expr le (For_set (sd_seqbool_set ty sd)) e2 sl2 a2 tmp2 -> + tr_expr le (For_set (SDcons type_bool ty t sd)) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> - incl tmp1 tmp -> incl tmp2 tmp -> In (sd_temp sd) tmp -> + incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> tr_expr le (For_set sd) (Csyntax.Eseqand e1 e2 ty) (sl1 ++ makeif a1 (makeseq sl2) (makeseq (do_set sd (Econst_int Int.zero ty))) :: nil) any tmp | tr_seqor_val: forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> - tr_expr le (For_set (sd_seqbool_val t ty)) e2 sl2 a2 tmp2 -> + tr_expr le (For_set (SDbase type_bool ty t)) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> tr_expr le For_val (Csyntax.Eseqor e1 e2 ty) @@ -178,11 +178,11 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> tr_expr le For_effects (Csyntax.Eseqor e1 e2 ty) (sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil) any tmp - | tr_seqor_set: forall le sd e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp, + | tr_seqor_set: forall le sd e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> - tr_expr le (For_set (sd_seqbool_set ty sd)) e2 sl2 a2 tmp2 -> + tr_expr le (For_set (SDcons type_bool ty t sd)) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> - incl tmp1 tmp -> incl tmp2 tmp -> In (sd_temp sd) tmp -> + incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> tr_expr le (For_set sd) (Csyntax.Eseqor e1 e2 ty) (sl1 ++ makeif a1 (makeseq (do_set sd (Econst_int Int.one ty))) (makeseq sl2) :: nil) @@ -642,7 +642,7 @@ Lemma contained_disjoint: contained l1 g1 g2 -> contained l2 g2 g3 -> list_disjoint l1 l2. Proof. intros; red; intros. red; intro; subst y. - exploit H; eauto. intros [A B]. exploit H0; eauto. intros [Csyntax D]. + exploit H; eauto. intros [A B]. exploit H0; eauto. intros [C D]. elim (Plt_strict x). apply Plt_Ple_trans with (gen_next g2); auto. Qed. @@ -650,45 +650,73 @@ Lemma contained_notin: forall g1 l g2 id g3, contained l g1 g2 -> within id g2 g3 -> ~In id l. Proof. - intros; red; intros. exploit H; eauto. intros [Csyntax D]. destruct H0 as [A B]. + intros; red; intros. exploit H; eauto. intros [C D]. destruct H0 as [A B]. elim (Plt_strict id). apply Plt_Ple_trans with (gen_next g2); auto. Qed. +Hint Resolve gensym_within within_widen contained_widen + contained_cons contained_app contained_disjoint + contained_notin contained_nil + incl_refl incl_tl incl_app incl_appl incl_appr incl_same_head incl_cons + in_eq in_cons in_or_app + Ple_trans Ple_refl: gensym. + +(** ** Properties of destinations *) + Definition dest_below (dst: destination) (g: generator) : Prop := match dst with | For_set sd => Plt (sd_temp sd) g.(gen_next) | _ => True end. +Lemma dest_below_le: + forall dst g1 g2, + dest_below dst g1 -> Ple g1.(gen_next) g2.(gen_next) -> dest_below dst g2. +Proof. + intros. destruct dst; simpl in *; eauto using Plt_Ple_trans. +Qed. + Remark dest_for_val_below: forall g, dest_below For_val g. Proof. intros; simpl; auto. Qed. Remark dest_for_effect_below: forall g, dest_below For_effects g. Proof. intros; simpl; auto. Qed. -Lemma dest_for_set_seqbool_val: - forall tmp ty g1 g2, - within tmp g1 g2 -> dest_below (For_set (sd_seqbool_val tmp ty)) g2. +Lemma dest_for_set_base_below: forall tmp tycast ty g1 g2, + within tmp g1 g2 -> dest_below (For_set (SDbase tycast ty tmp)) g2. Proof. - intros. destruct H. simpl. auto. + intros. destruct H. auto. Qed. -Lemma dest_for_set_seqbool_set: - forall sd ty g, dest_below (For_set sd) g -> dest_below (For_set (sd_seqbool_set ty sd)) g. -Proof. - intros. assumption. -Qed. +Hint Resolve dest_below_le dest_for_set_base_below : gensym. +Local Hint Resolve dest_for_val_below dest_for_effect_below : core. -Lemma dest_for_set_condition_val: - forall tmp tycast ty g1 g2, within tmp g1 g2 -> dest_below (For_set (SDbase tycast ty tmp)) g2. +(** ** Properties of [temp_for_sd] *) + +Definition good_temp_for_sd (ty: type) (tmp: ident) (sd: set_destination) (g1 g2 g3: generator) : Prop := + Plt (sd_temp sd) g1.(gen_next) + /\ Ple g1.(gen_next) g2.(gen_next) + /\ Ple g2.(gen_next) g3.(gen_next) + /\ if type_eq ty (sd_head_type sd) then tmp = sd_temp sd else within tmp g2 g3. + +Lemma temp_for_sd_charact: forall ty tmp sd g1 g2 g3 I, + dest_below (For_set sd) g1 -> + temp_for_sd ty sd g2 = Res tmp g3 I -> + Ple g1.(gen_next) g2.(gen_next) -> + good_temp_for_sd ty tmp sd g1 g2 g3. Proof. - intros. destruct H. simpl. auto. + unfold temp_for_sd, good_temp_for_sd; intros. destruct type_eq. +- inv H0. tauto. +- eauto with gensym. Qed. -Lemma dest_for_set_condition_set: - forall sd tmp tycast ty g1 g2, dest_below (For_set sd) g2 -> within tmp g1 g2 -> dest_below (For_set (SDcons tycast ty tmp sd)) g2. +Lemma dest_for_set_cons_below: forall tycast ty tmp sd g1 g2 g3, + good_temp_for_sd ty tmp sd g1 g2 g3 -> + dest_below (For_set (SDcons tycast ty tmp sd)) g3. Proof. - intros. destruct H0. simpl. auto. + intros until g3; intros (P & Q & R & S). simpl. destruct type_eq. +- subst tmp. unfold Ple, Plt in *; lia. +- destruct S; auto. Qed. Lemma sd_temp_notin: @@ -698,24 +726,41 @@ Proof. elim (Plt_strict (sd_temp sd)). apply Plt_Ple_trans with (gen_next g1); auto. Qed. -Lemma dest_below_le: - forall dst g1 g2, - dest_below dst g1 -> Ple g1.(gen_next) g2.(gen_next) -> dest_below dst g2. +Definition used_temp_for_sd (ty: type) (tmp: ident) (sd: set_destination) : list ident := + if type_eq ty (sd_head_type sd) then nil else tmp :: nil. + +Lemma temp_for_sd_disj: forall tmp1 tmp2 ty t sd g1 g2 g3 g4, + good_temp_for_sd ty t sd g1 g2 g3 -> + contained tmp1 g1 g2 -> + contained tmp2 g3 g4 -> + list_disjoint tmp1 (t :: tmp2). Proof. - intros. destruct dst; simpl in *; auto. eapply Plt_Ple_trans; eauto. + intros. destruct H as (P & Q & R & S). + apply list_disjoint_cons_r; eauto with gensym. + destruct type_eq. +- subst t. eapply sd_temp_notin; eauto. +- eauto with gensym. Qed. -Hint Resolve gensym_within within_widen contained_widen - contained_cons contained_app contained_disjoint - contained_notin contained_nil - dest_for_set_seqbool_val dest_for_set_seqbool_set - dest_for_set_condition_val dest_for_set_condition_set - sd_temp_notin dest_below_le - incl_refl incl_tl incl_app incl_appl incl_appr incl_same_head - in_eq in_cons - Ple_trans Ple_refl: gensym. +Lemma temp_for_sd_in: forall tmp ty t sd g1 g2 g3, + good_temp_for_sd ty t sd g1 g2 g3 -> + In t (sd_temp sd :: used_temp_for_sd ty t sd ++ tmp). +Proof. + intros. destruct H as (P & Q & R & S). unfold used_temp_for_sd. destruct type_eq. +- subst t. auto with coqlib. +- simpl; auto. +Qed. -Local Hint Resolve dest_for_val_below dest_for_effect_below : core. +Lemma temp_for_sd_contained: forall ty t sd g1 g2 g3, + good_temp_for_sd ty t sd g1 g2 g3 -> + contained (used_temp_for_sd ty t sd) g2 g3. +Proof. + intros. destruct H as (P & Q & R & S). unfold used_temp_for_sd. + destruct type_eq; eauto with gensym. +Qed. + +Hint Resolve temp_for_sd_charact dest_for_set_cons_below + sd_temp_notin temp_for_sd_disj temp_for_sd_in temp_for_sd_contained: gensym. (** ** Correctness of the translation functions *) @@ -741,14 +786,6 @@ Ltac UseFinish := repeat rewrite app_ass end. -(* -Fixpoint add_set_dest (sd: set_destination) (tmps: list ident) := - match sd with - | SDbase ty tmp => tmp :: tmps - | SDcons ty tmp sd' => tmp :: add_set_dest sd' tmps - end. -*) - Definition add_dest (dst: destination) (tmps: list ident) := match dst with | For_set sd => sd_temp sd :: tmps @@ -769,6 +806,7 @@ Proof. intros. apply tr_expr_monotone with tmps; auto. apply add_dest_incl. Qed. + Lemma is_bitfield_access_meets_spec: forall l g bf g' I, is_bitfield_access ce l g = Res bf g' I -> tr_is_bitfield_access l bf. @@ -838,7 +876,7 @@ Opaque makeif. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. - (* valof *) monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. - exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish. + exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. @@ -853,7 +891,7 @@ Opaque makeif. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. - (* binop *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish. + exploit H0; eauto. intros [tmp2 [C D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. @@ -883,7 +921,7 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. + (* for effects *) - exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. + exploit H0; eauto with gensym. intros [tmp2 [C D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqand_effects; eauto with gensym. @@ -891,15 +929,15 @@ Opaque makeif. + (* for set *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. simpl add_dest in *. - exists (tmp1 ++ tmp2); split. - intros; eapply tr_seqand_set; eauto with gensym. - apply list_disjoint_cons_r; eauto with gensym. + exists (used_temp_for_sd ty x0 sd ++ tmp1 ++ tmp2); split. + intros; eapply tr_seqand_set; eauto 4 with gensym; eauto 7 with gensym. + apply contained_app. eauto with gensym. apply contained_app; eauto with gensym. - (* seqor *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. + (* for value *) - exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. + exploit H0; eauto with gensym. intros [tmp2 [C D]]. simpl add_dest in *. exists (x0 :: tmp1 ++ tmp2); split. intros; eapply tr_seqor_val; eauto with gensym. @@ -915,9 +953,9 @@ Opaque makeif. + (* for set *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. simpl add_dest in *. - exists (tmp1 ++ tmp2); split. - intros; eapply tr_seqor_set; eauto with gensym. - apply list_disjoint_cons_r; eauto with gensym. + exists (used_temp_for_sd ty x0 sd ++ tmp1 ++ tmp2); split. + intros; eapply tr_seqor_set; eauto 4 with gensym; eauto 7 with gensym. + apply contained_app. eauto with gensym. apply contained_app; eauto with gensym. - (* condition *) monadInv H2. exploit H; eauto. intros [tmp1 [A B]]. @@ -934,7 +972,7 @@ Opaque makeif. apply contained_app. eauto with gensym. apply contained_app; eauto with gensym. + (* for effects *) - exploit H0; eauto. intros [tmp2 [Csyntax D]]. + exploit H0; eauto. intros [tmp2 [C D]]. exploit H1; eauto. intros [tmp3 [E F]]. simpl add_dest in *. exists (tmp1 ++ tmp2 ++ tmp3); split. @@ -942,13 +980,13 @@ Opaque makeif. apply contained_app; eauto with gensym. + (* for test *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. - exploit H1; eauto 10 with gensym. intros [tmp3 [E F]]. + exploit H1; eauto 6 with gensym. intros [tmp3 [E F]]. simpl add_dest in *. - exists (x0 :: tmp1 ++ tmp2 ++ tmp3); split. - intros; eapply tr_condition_set; eauto with gensym. - apply list_disjoint_cons_r; eauto with gensym. - apply list_disjoint_cons_r; eauto with gensym. - apply contained_cons; eauto with gensym. + exists (used_temp_for_sd ty x0 sd ++ tmp1 ++ tmp2 ++ tmp3); split. + intros; eapply tr_condition_set; eauto 4 with gensym. + apply incl_cons; eauto with gensym. + apply incl_cons; eauto with gensym. + apply contained_app; eauto with gensym. apply contained_app; eauto with gensym. apply contained_app; eauto with gensym. - (* sizeof *) @@ -959,7 +997,7 @@ Opaque makeif. exists (@nil ident); split; auto with gensym. constructor. - (* assign *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [Csyntax D]]. + exploit H0; eauto. intros [tmp2 [C D]]. apply is_bitfield_access_meets_spec in EQ0. destruct dst; monadInv EQ3; simpl add_dest in *. + (* for value *) @@ -979,7 +1017,7 @@ Opaque makeif. apply contained_app; eauto with gensym. - (* assignop *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [Csyntax D]]. + exploit H0; eauto. intros [tmp2 [C D]]. exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]]. apply is_bitfield_access_meets_spec in EQ2. destruct dst; monadInv EQ4; simpl add_dest in *. @@ -1018,7 +1056,7 @@ Opaque makeif. apply contained_cons; eauto with gensym. - (* comma *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. + exploit H0; eauto with gensym. intros [tmp2 [C D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. destruct dst; simpl; eauto with gensym. @@ -1028,7 +1066,7 @@ Opaque makeif. apply contained_app; eauto with gensym. - (* call *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [Csyntax D]]. + exploit H0; eauto. intros [tmp2 [C D]]. destruct dst; monadInv EQ2; simpl add_dest in *. + (* for value *) exists (x1 :: tmp1 ++ tmp2); split. @@ -1067,7 +1105,7 @@ Opaque makeif. monadInv H; exists (@nil ident); split; auto with gensym. constructor. - (* cons *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [Csyntax D]]. + exploit H0; eauto. intros [tmp2 [C D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. eauto with gensym. diff --git a/lib/Printlines.ml b/lib/Printlines.ml index 135672cc..b270e229 100644 --- a/lib/Printlines.ml +++ b/lib/Printlines.ml @@ -25,7 +25,7 @@ type filebuf = { the first character of line number [b.lineno]. *) let openfile f = - { chan = open_in f; + { chan = open_in_bin f; lineno = 1 } let close b = @@ -101,11 +101,13 @@ let copy oc pref b first last = try while b.lineno <= last do let c = input_char b.chan in - output_char oc c; - if c = '\n' then begin + match c with + | '\n' -> + output_char oc c; b.lineno <- b.lineno + 1; if b.lineno <= last then output_string oc pref - end + | '\r' | '\011' | '\012' -> output_char oc ' ' + | _ -> output_char oc c done with End_of_file -> output_char oc '\n' diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 373bd1a5..3d258257 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -110,7 +110,10 @@ module Target : TARGET = | Section_data i | Section_small_data i -> variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - variable_section ~sec:".section .rodata" i + variable_section + ~sec:".section .rodata" + ~reloc:".section .data.rel.ro,\"aw\",@progbits" + i | Section_string sz -> elf_mergeable_string_section sz ".section .rodata" | Section_literal sz -> diff --git a/test/regression/Makefile b/test/regression/Makefile index 0cc0fa3f..23125001 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -15,7 +15,7 @@ TESTS=int32 int64 floats floats-basics floats-lit \ volatile1 volatile2 volatile3 volatile4 \ funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \ sizeof1 sizeof2 binops bool for1 for2 switch switch2 compound \ - decl1 bitfields9 ptrs3 \ + decl1 bitfields9 ptrs3 telescopes \ parsing krfun ifconv generic # stringlit charlit # temporarily removed diff --git a/test/regression/Results/telescopes b/test/regression/Results/telescopes new file mode 100644 index 00000000..042e45bd --- /dev/null +++ b/test/regression/Results/telescopes @@ -0,0 +1,7 @@ +orand: 1 0 0 1 +andor: 0 1 1 0 +choose: 23 45 +choose2: 23 45 89 67 +choosed: 23.32 45.54 +choose2d: 23 45 89 67.76 +chooseandl: 23 0 0 1 diff --git a/test/regression/telescopes.c b/test/regression/telescopes.c new file mode 100644 index 00000000..02ff3b60 --- /dev/null +++ b/test/regression/telescopes.c @@ -0,0 +1,47 @@ +/* Nested `||`, `&&` and ` ? : ` expressions. */ + +#include <stdio.h> + +int orand(int x, int y, int z) { return x || (y && z); } + +int andor(int x, int y, int z) { return (x || y) && z; } + +int choose(int x, int y, int z) { return x ? y : z; } + +int choose2(int a, int x1, int y1, int z1, int x2, int y2, int z2) +{ return a ? (x1 ? y1 : z1) : (x2 ? y2 : z2); } + +double choosed(int x, double y, double z) { return x ? y : z; } + +double choose2d(int a, int x1, long long y1, int z1, int x2, double y2, long long z2) +{ return a ? (x1 ? y1 : z1) : (x2 ? y2 : z2); } + +long long chooseandl(int a, long long x, int y, int z) +{ return a ? x : y && z; } + +int main() +{ + printf("orand: %d %d %d %d\n", + orand(1,0,0), orand(0,1,0), orand(0,0,1), orand(0,1,1)); + printf("andor: %d %d %d %d\n", + andor(0,0,1), andor(1,0,1), andor(0,1,1), andor(1,1,0)); + printf("choose: %d %d\n", + choose(1, 23, 45), choose(0, 23, 45)); + printf("choose2: %d %d %d %d\n", + choose2(1, 1, 23, 45, 0, 67, 89), + choose2(1, 0, 23, 45, 0, 67, 89), + choose2(0, 0, 23, 45, 0, 67, 89), + choose2(0, 0, 23, 45, 1, 67, 89)); + printf("choosed: %g %g\n", + choosed(1, 23.32, 45.54), choosed(0, 23.32, 45.54)); + printf("choose2d: %g %g %g %g\n", + choose2d(1, 1, 23, 45, 0, 67.76, 89), + choose2d(1, 0, 23, 45, 0, 67.76, 89), + choose2d(0, 0, 23, 45, 0, 67.76, 89), + choose2d(0, 0, 23, 45, 1, 67.76, 89)); + printf("chooseandl: %lld %lld %lld %lld\n", + chooseandl(1, 23, 0, 0), + chooseandl(0, 23, 0, 1), + chooseandl(0, 23, 1, 0), + chooseandl(0, 23, 1, 1)); +} diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index dad8d15c..f529a89d 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -137,7 +137,10 @@ module ELF_System : SYSTEM = | Section_data i | Section_small_data i -> variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - variable_section ~sec:".section .rodata" i + variable_section + ~sec:".section .rodata" + ~reloc:".section .data.rel.ro,\"aw\",@progbits" + i | Section_string sz -> elf_mergeable_string_section sz ".section .rodata" | Section_literal sz -> |