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 From 8486b4c046914b1388b68fe906fe267108f84267 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 7 Jul 2020 17:27:08 +0100 Subject: Fixes to operators --- src/Compiler.v | 2 ++ src/translation/HTLgen.v | 4 +++- src/translation/HTLgenproof.v | 7 +++++-- src/verilog/Verilog.v | 5 ++--- 4 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/Compiler.v b/src/Compiler.v index db3a810..d716caa 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -98,6 +98,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program + @@ print (print_RTL 0) @@@ transf_backend. Local Open Scope linking_scope. @@ -129,6 +130,7 @@ Proof. destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. + rewrite ! compose_print_identity in T. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_backend in T. simpl in T. rewrite ! compose_print_identity in T. destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate. diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index e0f860e..1cc30c7 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -366,7 +366,9 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := (Vlit (intToValue n))))*) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) - | Op.Ororimm n, r::nil => ret (boplit Vror r n) + | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32))) + (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*) | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n))) | Op.Ocmp c, _ => translate_condition c args | Op.Osel c AST.Tint, r1::r2::rl => diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index da0b662..dd1d967 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -587,6 +587,9 @@ Section CORRECTNESS. - rewrite Heqb in Heqb0. discriminate. - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. - rewrite Heqb in Heqb0. discriminate. + (*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu, + Search Int.repr. + repeat (rewrite Int.unsigned_repr). auto.*) - unfold Op.eval_addressing32 in *. repeat (unfold_match H2); inv H2. + unfold translate_eff_addressing in *. repeat (unfold_match H1). destruct v0; inv Heql; rewrite H2; inv H1; repeat eval_correct_tac. @@ -811,7 +814,7 @@ Section CORRECTNESS. inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. - Unshelve. auto. + Unshelve. exact tt. Qed. Hint Resolve transl_inop_correct : htlproof. @@ -863,7 +866,7 @@ Section CORRECTNESS. assert (HPle: Ple res0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_def; eauto; simpl; auto). unfold Ple in HPle. lia. - Unshelve. trivial. + Unshelve. exact tt. Qed. Hint Resolve transl_iop_correct : htlproof. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 43df3dd..321bdc2 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -143,8 +143,8 @@ Inductive binop : Type := | Vxor : binop (** xor (binary [^|]) *) | Vshl : binop (** shift left ([<<]) *) | Vshr : binop (** shift right ([>>>]) *) -| Vshru : binop (** shift right unsigned ([>>]) *) -| Vror : binop. (** shift right unsigned ([>>]) *) +| Vshru : binop. (** shift right unsigned ([>>]) *) +(*| Vror : binop (** shift right unsigned ([>>]) *)*) (** ** Unary Operators *) @@ -325,7 +325,6 @@ Definition binop_run (op : binop) (v1 v2 : value) : option value := | Vshl => Some (Int.shl v1 v2) | Vshr => Some (Int.shr v1 v2) | Vshru => Some (Int.shru v1 v2) - | Vror => Some (Int.ror v1 v2) end. Definition unop_run (op : unop) (v1 : value) : value := -- cgit