From e63fef0613ed9e497279ae47b746413a093e9530 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 7 Jul 2020 16:00:58 +0100 Subject: Finished transl_cond --- src/translation/HTLgen.v | 4 -- src/translation/HTLgenproof.v | 103 ++++++++++++++++++------------------------ 2 files changed, 45 insertions(+), 62 deletions(-) diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 9f39edb..e0f860e 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -271,8 +271,6 @@ Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : mon expr := match c, args with - | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2) - | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2) | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2) | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2) | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2) @@ -283,8 +281,6 @@ Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : m Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int) : mon expr := match c, args with - | Integers.Ceq, r1::nil => ret (boplit Veq r1 i) - | Integers.Cne, r1::nil => ret (boplit Vne r1 i) | Integers.Clt, r1::nil => ret (boplit Vltu r1 i) | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i) | Integers.Cle, r1::nil => ret (boplit Vleu r1 i) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 7db0a2b..da0b662 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -519,6 +519,8 @@ Section CORRECTNESS. end. Ltac solve_cond := match goal with + | H : context[match _ with _ => _ end] |- _ => repeat (unfold_merge H) + | H : ?f = _ |- context[boolToValue ?f] => rewrite H; solve [auto] | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, H2 : Registers.Regmap.get ?r ?rs = Values.Vint _ |- _ => rewrite H2 in H; discriminate @@ -526,10 +528,16 @@ Section CORRECTNESS. H2 : Registers.Regmap.get ?r ?rs = Values.Vint _ |- _ => rewrite H2 in H; discriminate | H : Values.Vint _ = Registers.Regmap.get ?r ?rs, - H2 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _ |- _ => + H2 : Registers.Regmap.get ?r ?rs = Values.Vundef |- _ => rewrite H2 in H; discriminate | H : Values.Vint _ = Registers.Regmap.get ?r ?rs, - H2 : Registers.Regmap.get ?r ?rs = Values.Vint _ _ |- _ => + H2 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _ |- _ => + rewrite H2 in H; discriminate + | H : Values.Vundef = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _ |- _ => + rewrite H2 in H; discriminate + | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vundef |- _ => rewrite H2 in H; discriminate | |- context[val_value_lessdef Values.Vundef _] => econstructor; split; econstructor; econstructor; auto; solve [constructor] @@ -538,8 +546,20 @@ Section CORRECTNESS. H3 : Registers.Regmap.get ?r0 ?rs = Values.Vint _, H4 : Values.Vint _ = Registers.Regmap.get ?r0 ?rs|- _ => rewrite H1 in H2; rewrite H3 in H4; inv H2; inv H4; unfold valueToInt in *; constructor + | H1 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _, + H2 : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, + H3 : Registers.Regmap.get ?r0 ?rs = Values.Vptr _ _, + H4 : Values.Vptr _ _ = Registers.Regmap.get ?r0 ?rs|- _ => + rewrite H1 in H2; rewrite H3 in H4; inv H2; inv H4; unfold valueToInt in *; constructor; + unfold Ptrofs.ltu, Int.ltu in *; unfold Ptrofs.of_int in *; + repeat (rewrite Ptrofs.unsigned_repr in *; auto using Int.unsigned_range_2) | H : _ :: _ = _ :: _ |- _ => inv H | H : ret _ _ = OK _ _ _ |- _ => inv H + | |- _ => + eexists; split; [ econstructor; econstructor; auto + | simplify; inv_lessdef; repeat (unfold valueToPtr, valueToInt in *; solve_cond); + unfold valueToPtr in * + ] end. intros s sp op rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st MSTATE INSTR EVAL TR_INSTR. inv MSTATE. inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR; @@ -657,63 +677,30 @@ Section CORRECTNESS. repeat (match goal with |- context[match ?d with _ => _ end] => destruct d eqn:? end; match goal with H : context[match ?d with _ => _ end] |- _ => repeat unfold_match H end); try (match goal with |- context[if ?d then _ else _] => destruct d eqn:? end); + simplify; repeat solve_cond; + try (match goal with H : ?f = _ |- context[boolToValue ?f] => rewrite H; solve [auto] end); + try (match goal with H : context[match ?d with _ => _ end] |- _ => repeat unfold_match H end); simplify; repeat solve_cond. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1. auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1. auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + eexists. split. econstructor; econstructor; auto. - simplify. inv_lessdef; solve_cond. rewrite H1; auto. - + inv_lessdef; try solve_cond. - * unfold valueToInt, valueToPtr in *. rewrite H5 in H3. rewrite H4 in H2. inv H2. inv H3. - eexists. split. econstructor; econstructor; auto. simplify. - unfold Int.eq. - constructor. apply H in HPle1. inv HPle1. unfold valueToInt in *. rewrite Heqv2 in H2. inv H2. auto. - - rewrite H2. auto. - - - admit. (* eval_condition *) + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. - admit. (* select *) Admitted. -- cgit