From 594c2825012d94675317f51cf6a3e97c2f88cd02 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 3 Jul 2020 21:05:45 +0100 Subject: Fixing HTLgenproof --- src/translation/HTLgen.v | 22 ++++++++++----------- src/translation/HTLgenproof.v | 45 ++++++++++++++++++++++++++++++------------- src/translation/HTLgenspec.v | 8 ++++---- src/verilog/HTL.v | 10 ++++------ src/verilog/ValueInt.v | 21 ++++++++++++++------ src/verilog/Verilog.v | 2 +- 6 files changed, 67 insertions(+), 41 deletions(-) diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index f58c9ae..1977f65 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -91,7 +91,7 @@ Definition state_goto (st : reg) (n : node) : stmnt := Vnonblock (Vvar st) (Vlit (posToValue n)). Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := - Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)). + Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). Definition check_empty_node_datapath: forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. @@ -244,7 +244,7 @@ Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := Vbinop op (Vvar r) (Vlit (intToValue l)). Definition boplitz (op: binop) (r: reg) (l: Z) : expr := - Vbinop op (Vvar r) (Vlit (ZToValue 32%nat l)). + Vbinop op (Vvar r) (Vlit (ZToValue l)). Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr := match c, args with @@ -297,7 +297,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned") | Op.Ascaled scale offset, r1::nil => if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) - then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) + then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned") | Op.Aindexed2 offset, r1::r2::nil => if (check_address_parameter_signed offset) @@ -310,7 +310,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in if (check_address_parameter_unsigned a) - then ret (Vlit (ZToValue 32 a)) + then ret (Vlit (ZToValue a)) else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned") | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. @@ -342,7 +342,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) | Op.Oshrximm n, r::nil => ret (Vbinop Vdiv (Vvar r) - (Vbinop Vshl (Vlit (ZToValue 32 1)) + (Vbinop Vshl (Vlit (ZToValue 1)) (Vlit (intToValue n)))) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) @@ -395,19 +395,19 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) | Mint32, Op.Aindexed off, r1::nil => if (check_address_parameter_signed off) - then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 32 4)))) + then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) else error (Errors.msg "HTLgen: translate_arr_access address misaligned") | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vvari stack (Vbinop Vdivu (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - (ZToValue 32 4))) + (ZToValue 4))) else error (Errors.msg "HTLgen: translate_arr_access address misaligned") | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in if (check_address_parameter_unsigned a) - then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) + then ret (Vvari stack (Vlit (ZToValue (a / 4)))) else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") end. @@ -420,7 +420,7 @@ Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := List.map (fun a => match a with - (i, n) => (Vlit (natToValue 32 i), Vnonblock (Vvar st) (Vlit (posToValue 32 n))) + (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n))) end) (enumerate 0 ns). @@ -452,9 +452,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Ireturn r => match r with | Some r' => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r'))) + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))) | None => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))) end end end. diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 956c3ed..79bca49 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -16,9 +16,9 @@ * along with this program. If not, see . *) -From compcert Require RTL Registers AST Integers. -From compcert Require Import Globalenvs Memory. -From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra. +From compcert Require RTL Registers AST. +From compcert Require Import Integers Globalenvs Memory. +From coqup Require Import Coquplib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra. From coqup Require HTL Verilog. Require Import Lia. @@ -41,7 +41,7 @@ Hint Constructors match_assocmaps : htlproof. Definition state_st_wf (m : HTL.module) (s : HTL.state) := forall st asa asr res, s = HTL.State res m st asa asr -> - asa!(m.(HTL.mod_st)) = Some (posToValue 32 st). + asa!(m.(HTL.mod_st)) = Some (posToValue st). Hint Unfold state_st_wf : htlproof. Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : @@ -53,7 +53,7 @@ Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem 0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) -> opt_val_value_lessdef (Mem.loadv AST.Mint32 mem (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))) - (Option.default (NToValue 32 0) + (Option.default (NToValue 0) (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> match_arrs m f sp mem asa. @@ -254,12 +254,6 @@ Proof. assumption. Qed. -(* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) -Lemma assumption_32bit : - forall v, - valueToPos (posToValue 32 v) = v. -Admitted. - Ltac inv_state := match goal with MSTATE : match_states _ _ |- _ => @@ -358,6 +352,14 @@ Section CORRECTNESS. (Genv.senv_transf_partial TRANSL'). Hint Resolve senv_preserved : htlproof. + Lemma ptrofs_inj : + forall a b, + Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b. + Proof. + intros. rewrite <- Ptrofs.repr_unsigned. symmetry. rewrite <- Ptrofs.repr_unsigned. + rewrite H. auto. + Qed. + Lemma eval_correct : forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st, match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> @@ -373,12 +375,29 @@ Section CORRECTNESS. - inv Heql. assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). apply H in HPle. eexists. split; try constructor; eauto. - - eexists. split. constructor. constructor. symmetry. apply valueToInt_intToValue. + - eexists. split. constructor. constructor. auto. - inv Heql. assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). apply H in HPle. eexists. split. econstructor; eauto. constructor. trivial. - unfold Verilog.unop_run. + unfold Verilog.unop_run. unfold Values.Val.neg. destruct (Registers.Regmap.get r rs) eqn:?; constructor. + inv HPle. auto. + - inv Heql. + assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + assert (HPle0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle. apply H in HPle0. + eexists. split. econstructor; eauto. constructor. trivial. + constructor. trivial. simplify. inv HPle. inv HPle0; constructor; auto. + + inv HPle0. constructor. unfold valueToPtr. Search Integers.Ptrofs.sub Integers.int. + pose proof Integers.Ptrofs.agree32_sub. unfold Integers.Ptrofs.agree32 in H3. + Print Integers.Ptrofs.agree32. unfold Ptrofs.of_int. simpl. + apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H3 in H4. + rewrite Ptrofs.unsigned_repr. apply H4. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. + auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. Lemma eval_cond_correct : forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index d2bd5af..799b198 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -18,7 +18,7 @@ From compcert Require RTL Op Maps Errors. From compcert Require Import Maps. -From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap. +From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap. Require Import Lia. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. @@ -127,12 +127,12 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - translate_condition cond args s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) | tr_instr_Ireturn_None : - tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) - (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip + tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%Z))) + (block rtrn (Vlit (ZToValue 0%Z)))) Vskip | tr_instr_Ireturn_Some : forall r, tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) - (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip + (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip | tr_instr_Iload : forall mem addr args s s' i c dst n, translate_arr_access mem addr args stk s = OK c s' i -> diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index a3623f0..df88f98 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -17,13 +17,11 @@ *) From Coq Require Import FSets.FMapPositive. -From coqup Require Import Coquplib Value AssocMap Array. +From coqup Require Import Coquplib ValueInt AssocMap Array. From coqup Require Verilog. From compcert Require Events Globalenvs Smallstep Integers Values. From compcert Require Import Maps. -Import HexNotationValue. - (** The purpose of the hardware transfer language (HTL) is to create a more hardware-like layout that is still similar to the register transfer language (RTL) that it came from. The main change is that function calls become module @@ -128,21 +126,21 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_finish : forall g m st asr asa retval sf, - asr!(m.(mod_finish)) = Some (1'h"1") -> + asr!(m.(mod_finish)) = Some (ZToValue 1) -> asr!(m.(mod_return)) = Some retval -> step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) | step_call : forall g m args res, step g (Callstate res m args) Events.E0 (State res m m.(mod_entrypoint) - (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint)) + (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) (init_regs args m.(mod_params))) (empty_stack m)) | step_return : forall g m asr asa i r sf pc mst, mst = mod_st m -> step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 - (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa). + (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index cc1d404..dff7b5c 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -138,6 +138,21 @@ Lemma uvalueToZ_ZToValue : uvalueToZ (ZToValue z) = z. Proof. auto using Int.unsigned_repr. Qed. +Lemma valueToPos_posToValue : + forall v, + 0 <= Z.pos v <= Int.max_unsigned -> + valueToPos (posToValue v) = v. +Proof. + unfold valueToPos, posToValue. + intros. rewrite Int.unsigned_repr. + apply Pos2Z.id. assumption. +Qed. + +Lemma valueToInt_intToValue : + forall v, + valueToInt (intToValue v) = v. +Proof. auto. Qed. + Lemma valToValue_lessdef : forall v v', valToValue v = Some v' -> @@ -152,9 +167,3 @@ Proof. inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. inv H1. apply Z.eqb_eq. apply Heqb0. Qed. - -Local Open Scope Z. - -Ltac word_op_value H := - intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold; - rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 5ef4dda..f5916ad 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -331,7 +331,7 @@ Definition binop_run (op : binop) (v1 v2 : value) : option value := Definition unop_run (op : unop) (v1 : value) : value := match op with - | Vneg => Int.notbool v1 + | Vneg => Int.neg v1 | Vnot => Int.not v1 end. -- cgit