From ec97745e4675b72cbabd2a3bd12d6efdd8bfa6d6 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Mon, 6 Jul 2020 15:33:04 +0100 Subject: Implemented algorithm for new byte-addressed stack. --- src/common/Coquplib.v | 2 + src/common/IntegerExtra.v | 36 +- src/common/Monad.v | 4 + src/extraction/Extraction.v | 4 +- src/translation/HTLgen.v | 88 +- src/translation/HTLgenproof.v | 4311 +++++++++++++++++++++-------------------- src/translation/HTLgenspec.v | 918 ++++----- src/verilog/PrintHTL.ml | 2 +- src/verilog/PrintVerilog.ml | 10 +- src/verilog/PrintVerilog.mli | 4 +- src/verilog/Verilog.v | 33 +- 11 files changed, 2730 insertions(+), 2682 deletions(-) diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index 2295ff6..469eddc 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -235,3 +235,5 @@ Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B := Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B := let unused := debug_print (s ++ show a) in b. + +Notation "f $ x" := (f x) (at level 60, right associativity, only parsing). diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index fe7d94f..8e32c2c 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -298,44 +298,48 @@ Module IntExtra. (or (shl (repr (Byte.unsigned c)) (repr Byte.zwordsize)) (repr (Byte.unsigned d)))). - Definition byte1 (n: int) : byte := Byte.repr (unsigned n). + Definition byte0 (n: int) : byte := Byte.repr $ unsigned n. + Definition ibyte0 (n: int) : int := Int.repr $ Byte.unsigned $ byte0 n. - Definition byte2 (n: int) : byte := Byte.repr (unsigned (shru n (repr Byte.zwordsize))). + Definition byte1 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr Byte.zwordsize. + Definition ibyte1 (n: int) : int := Int.repr $ Byte.unsigned $ byte1 n. - Definition byte3 (n: int) : byte := Byte.repr (unsigned (shru n (repr (2 * Byte.zwordsize)))). + Definition byte2 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (2 * Byte.zwordsize). + Definition ibyte2 (n: int) : int := Int.repr $ Byte.unsigned $ byte2 n. - Definition byte4 (n: int) : byte := Byte.repr (unsigned (shru n (repr (3 * Byte.zwordsize)))). + Definition byte3 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (3 * Byte.zwordsize). + Definition ibyte3 (n: int) : int := Int.repr $ Byte.unsigned $ byte3 n. - Lemma bits_byte1: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n i. + Lemma bits_byte0: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte0 n) i = testbit n i. Proof. - intros. unfold byte1. rewrite Byte.testbit_repr; auto. + intros. unfold byte0. rewrite Byte.testbit_repr; auto. Qed. - Lemma bits_byte2: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + Byte.zwordsize). + Lemma bits_byte1: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n (i + Byte.zwordsize). Proof. - intros. unfold byte2. rewrite Byte.testbit_repr; auto. + intros. unfold byte1. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru. change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. apply zlt_true. omega. omega. Qed. - Lemma bits_byte3: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (2 * Byte.zwordsize)). + Lemma bits_byte2: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + (2 * Byte.zwordsize)). Proof. - intros. unfold byte3. rewrite Byte.testbit_repr; auto. + intros. unfold byte2. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). apply zlt_true. omega. omega. Qed. - Lemma bits_byte4: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte4 n) i = testbit n (i + (3 * Byte.zwordsize)). + Lemma bits_byte3: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (3 * Byte.zwordsize)). Proof. - intros. unfold byte4. rewrite Byte.testbit_repr; auto. + intros. unfold byte3. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). diff --git a/src/common/Monad.v b/src/common/Monad.v index 8517186..628963e 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -20,6 +20,10 @@ Module MonadExtra(M : Monad). Module MonadNotation. + Notation "A ; B" := + (bind A (fun _ => B)) + (at level 200, B at level 200). + Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index df21dc4..5d10cd7 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -16,7 +16,7 @@ * along with this program. If not, see . *) -From coqup Require Verilog Value Compiler. +From coqup Require Verilog ValueInt Compiler. From Coq Require DecidableClass. @@ -167,7 +167,7 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction - Verilog.module Value.uvalueToZ coqup.Compiler.transf_hls + Verilog.module ValueInt.uvalueToZ coqup.Compiler.transf_hls Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index e02d759..995977c 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -292,26 +292,16 @@ Definition check_address_parameter_unsigned (p : Z) : bool := Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) | Op.Aindexed off, r1::nil => - if (check_address_parameter_signed off) - then ret (boplitz Vadd r1 off) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned") + ret (boplitz Vadd r1 off) | 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 offset))) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned") + ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) | Op.Aindexed2 offset, r1::r2::nil => - if (check_address_parameter_signed offset) - then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset)) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address misaligned") + ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset)) | 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 (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address misaligned") + ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) | 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 a)) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned") + ret (Vlit (ZToValue a)) | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. @@ -390,27 +380,27 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") end. -Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) - (args : list reg) (stack : reg) : mon expr := - 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 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)) - (Vlit (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 (a / 4)))) - else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") - | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") - end. +(* Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) *) +(* (args : list reg) (stack : reg) : mon expr := *) +(* 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 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)) *) +(* (Vlit (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 (a / 4)))) *) +(* else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") *) +(* | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") *) +(* end. *) Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := match ns with @@ -424,6 +414,22 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := end) (enumerate 0 ns). +Definition add_single_cycle_load (n n' : node) (stack : reg) (addr : expr) (dst : reg) : mon unit := + let l0 := Vnonblock (Vvarb0 dst) (Vvari stack addr) in + let l1 := Vnonblock (Vvarb1 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) in + let l2 := Vnonblock (Vvarb2 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in + let l3 := Vnonblock (Vvarb3 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in + let instr := Vseq l0 $ Vseq l1 $ Vseq l2 $ l3 + in add_instr n n' instr. + +Definition add_single_cycle_store (n n' : node) (stack : reg) (addr : expr) (src : reg) : mon unit := + let l0 := Vnonblock (Vvari stack addr) (Vvarb0 src) in + let l1 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) (Vvarb1 src) in + let l2 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb2 src) in + let l3 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb3 src) in + let instr := Vseq l0 $ Vseq l1 $ Vseq l2 $ l3 + in add_instr n n' instr. + Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with (n, i) => @@ -434,12 +440,12 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni do _ <- declare_reg None dst 32; add_instr n n' (nonblock dst instr) | Iload mem addr args dst n' => - do src <- translate_arr_access mem addr args stack; + do addr' <- translate_eff_addressing addr args; do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst src) + add_single_cycle_load n n' stack addr' dst | Istore mem addr args src n' => - do dst <- translate_arr_access mem addr args stack; - add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + do addr' <- translate_eff_addressing addr args; + add_single_cycle_store n n' stack addr' src | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") @@ -543,7 +549,7 @@ Definition transf_module (f: function) : mon module := if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; - do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); + do (stack, stack_len) <- create_arr None 8 (Z.to_nat f.(fn_stacksize)); do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); do start <- create_reg (Some Vinput) 1; diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 305c14f..e404c82 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -31,2158 +31,2159 @@ Hint Resolve AssocMap.gso : htlproof. Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. -Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := - match_assocmap : forall f rs am, - (forall r, Ple r (RTL.max_reg_function f) -> - val_value_lessdef (Registers.Regmap.get r rs) am#r) -> - match_assocmaps f rs am. -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 st). -Hint Unfold state_st_wf : htlproof. - -Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : - Verilog.assocmap_arr -> Prop := -| match_arr : forall asa stack, - asa ! (m.(HTL.mod_stk)) = Some stack /\ - stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\ - (forall ptr, - 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 0) - (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> - match_arrs m f sp mem asa. - -Definition stack_based (v : Values.val) (sp : Values.block) : Prop := - match v with - | Values.Vptr sp' off => sp' = sp - | _ => True - end. - -Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop := - forall r, stack_based (Registers.Regmap.get r rs) sp. - -Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z) - (sp : Values.val) : Prop := - forall ptr, - 0 <= ptr < (stack_length / 4) -> - stack_based (Option.default - Values.Vundef - (Mem.loadv AST.Mint32 m - (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))) - spb. - -Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop := - forall ptr v, - hi <= ptr <= Integers.Ptrofs.max_unsigned -> - Z.modulo ptr 4 = 0 -> - Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\ - Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None. - -Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop := -| match_frames_nil : - match_frames nil nil. - - Lemma assumption_32bit : - forall v, - valueToPos (posToValue v) = v. - Proof. - Admitted. - -Inductive match_states : RTL.state -> HTL.state -> Prop := -| match_state : forall asa asr sf f sp sp' rs mem m st res - (MASSOC : match_assocmaps f rs asr) - (TF : tr_module f m) - (WF : state_st_wf m (HTL.State res m st asr asa)) - (MF : match_frames sf res) - (MARR : match_arrs m f sp mem asa) - (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) - (RSBP : reg_stack_based_pointers sp' rs) - (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) - (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem), - match_states (RTL.State sf f sp st rs mem) - (HTL.State res m st asr asa) -| match_returnstate : - forall - v v' stack mem res - (MF : match_frames stack res), - val_value_lessdef v v' -> - match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v') -| match_initial_call : - forall f m m0 - (TF : tr_module f m), - match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil). -Hint Constructors match_states : htlproof. - -Definition match_prog (p: RTL.program) (tp: HTL.program) := - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ - main_is_internal p = true. - -Definition match_prog_matches : - forall p tp, - match_prog p tp -> - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. - Proof. intros. unfold match_prog in H. tauto. Qed. - -Lemma transf_program_match: - forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp. -Proof. - intros. unfold transl_program in H. - destruct (main_is_internal p) eqn:?; try discriminate. - unfold match_prog. split. - apply Linking.match_transform_partial_program; auto. - assumption. -Qed. - -Lemma regs_lessdef_add_greater : - forall f rs1 rs2 n v, - Plt (RTL.max_reg_function f) n -> - match_assocmaps f rs1 rs2 -> - match_assocmaps f rs1 (AssocMap.set n v rs2). -Proof. - inversion 2; subst. - intros. constructor. - intros. unfold find_assocmap. unfold AssocMapExt.get_default. - rewrite AssocMap.gso. eauto. - apply Pos.le_lt_trans with _ _ n in H2. - unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. -Qed. -Hint Resolve regs_lessdef_add_greater : htlproof. - -Lemma regs_lessdef_add_match : - forall f rs am r v v', - val_value_lessdef v v' -> - match_assocmaps f rs am -> - match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am). -Proof. - inversion 2; subst. - constructor. intros. - destruct (peq r0 r); subst. - rewrite Registers.Regmap.gss. - unfold find_assocmap. unfold AssocMapExt.get_default. - rewrite AssocMap.gss. assumption. - - rewrite Registers.Regmap.gso; try assumption. - unfold find_assocmap. unfold AssocMapExt.get_default. - rewrite AssocMap.gso; eauto. -Qed. -Hint Resolve regs_lessdef_add_match : htlproof. - -Lemma list_combine_none : - forall n l, - length l = n -> - list_combine Verilog.merge_cell (list_repeat None n) l = l. -Proof. - induction n; intros; crush. - - symmetry. apply length_zero_iff_nil. auto. - - destruct l; crush. - rewrite list_repeat_cons. - crush. f_equal. - eauto. -Qed. - -Lemma combine_none : - forall n a, - a.(arr_length) = n -> - arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. -Proof. - intros. - unfold combine. - crush. - - rewrite <- (arr_wf a) in H. - apply list_combine_none. - assumption. -Qed. - -Lemma list_combine_lookup_first : - forall l1 l2 n, - length l1 = length l2 -> - nth_error l1 n = Some None -> - nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n. -Proof. - induction l1; intros; crush. - - rewrite nth_error_nil in H0. - discriminate. - - destruct l2 eqn:EQl2. crush. - simpl in H. invert H. - destruct n; simpl in *. - invert H0. simpl. reflexivity. - eauto. -Qed. - -Lemma combine_lookup_first : - forall a1 a2 n, - a1.(arr_length) = a2.(arr_length) -> - array_get_error n a1 = Some None -> - array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2. -Proof. - intros. - - unfold array_get_error in *. - apply list_combine_lookup_first; eauto. - rewrite a1.(arr_wf). rewrite a2.(arr_wf). - assumption. -Qed. - -Lemma list_combine_lookup_second : - forall l1 l2 n x, - length l1 = length l2 -> - nth_error l1 n = Some (Some x) -> - nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x). -Proof. - induction l1; intros; crush; auto. - - destruct l2 eqn:EQl2. crush. - simpl in H. invert H. - destruct n; simpl in *. - invert H0. simpl. reflexivity. - eauto. -Qed. - -Lemma combine_lookup_second : - forall a1 a2 n x, - a1.(arr_length) = a2.(arr_length) -> - array_get_error n a1 = Some (Some x) -> - array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x). -Proof. - intros. - - unfold array_get_error in *. - apply list_combine_lookup_second; eauto. - rewrite a1.(arr_wf). rewrite a2.(arr_wf). - assumption. -Qed. - -Ltac inv_state := - match goal with - MSTATE : match_states _ _ |- _ => - inversion MSTATE; - match goal with - TF : tr_module _ _ |- _ => - inversion TF; - match goal with - TC : forall _ _, - Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _, - H : Maps.PTree.get _ _ = Some _ |- _ => - apply TC in H; inversion H; - match goal with - TI : context[tr_instr] |- _ => - inversion TI - end - end - end -end; subst. - -Ltac unfold_func H := - match type of H with - | ?f = _ => unfold f in H; repeat (unfold_match H) - | ?f _ = _ => unfold f in H; repeat (unfold_match H) - | ?f _ _ = _ => unfold f in H; repeat (unfold_match H) - | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H) - | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H) - end. - -Lemma init_reg_assoc_empty : - forall f l, - match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l). -Proof. - induction l; simpl; constructor; intros. - - rewrite Registers.Regmap.gi. unfold find_assocmap. - unfold AssocMapExt.get_default. rewrite AssocMap.gempty. - constructor. - - - rewrite Registers.Regmap.gi. unfold find_assocmap. - unfold AssocMapExt.get_default. rewrite AssocMap.gempty. - constructor. -Qed. - -Lemma arr_lookup_some: - forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr) - (stack : Array (option value)) (H5 : asa ! r = Some stack) n, - exists x, Verilog.arr_assocmap_lookup asa r n = Some x. -Proof. - intros z r0 r asr asa stack H5 n. - eexists. - unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity. -Qed. -Hint Resolve arr_lookup_some : htlproof. - -Section CORRECTNESS. - - Variable prog : RTL.program. - Variable tprog : HTL.program. - - Hypothesis TRANSL : match_prog prog tprog. - - Lemma TRANSL' : - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. - Proof. intros; apply match_prog_matches; assumption. Qed. - - Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. - Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. - - Lemma symbols_preserved: - forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. - Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed. - - Lemma function_ptr_translated: - forall (b: Values.block) (f: RTL.fundef), - Genv.find_funct_ptr ge b = Some f -> - exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. - Proof. - intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. - intros (cu & tf & P & Q & R); exists tf; auto. - Qed. - - Lemma functions_translated: - forall (v: Values.val) (f: RTL.fundef), - Genv.find_funct ge v = Some f -> - exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. - Proof. - intros. exploit (Genv.find_funct_match TRANSL'); eauto. - intros (cu & tf & P & Q & R); exists tf; auto. - Qed. - - Lemma senv_preserved: - Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). - Proof - (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) -> - (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> - Op.eval_operation ge sp op - (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> - translate_instr op args s = OK e s' i -> - exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. - Proof. - 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; - unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); simplify. - - 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. 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 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. - Admitted. - - Lemma eval_cond_correct : - forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, - translate_condition cond args s1 = OK c s' i -> - Op.eval_condition - cond - (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) - m = Some b -> - Verilog.expr_runp f asr asa c (boolToValue b). - Admitted. - - (** The proof of semantic preservation for the translation of instructions - is a simulation argument based on diagrams of the following form: -<< - match_states - code st rs ---------------- State m st assoc - || | - || | - || | - \/ v - code st rs' --------------- State m st assoc' - match_states ->> - where [tr_code c data control fin rtrn st] is assumed to hold. - - The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. - *) - - Definition transl_instr_prop (instr : RTL.instruction) : Prop := - forall m asr asa fin rtrn st stmt trans res, - tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans -> - exists asr' asa', - HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). - - Opaque combine. - - Ltac tac0 := - match goal with - | [ |- context[valueToPos (posToValue _)] ] => rewrite assumption_32bit - - | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs - | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr - | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge - | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros - | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set - - | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack - - | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss - | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso - | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty - - | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] => - rewrite combine_lookup_first - - | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1 - | [ |- context[match_states _ _] ] => econstructor; auto - | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto - | [ |- match_assocmaps _ _ _ # _ <- (posToValue _) ] => - apply regs_lessdef_add_greater; [> unfold Plt; lia | assumption] - - | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => - unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal - | [ |- context[(AssocMap.combine _ _ _) ! _] ] => - try (rewrite AssocMap.gcombine; [> | reflexivity]) - - | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] => - rewrite Registers.Regmap.gss - | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] => - destruct (Pos.eq_dec s d) as [EQ|EQ]; - [> rewrite EQ | rewrite Registers.Regmap.gso; auto] - - | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H - | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |] - | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H - end. - - Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto. - Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto. - - Lemma transl_inop_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : RTL.regset) (m : mem) (pc' : RTL.node), - (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. - Proof. - intros s f sp pc rs m pc' H R1 MSTATE. - inv_state. - - unfold match_prog in TRANSL. - econstructor. - split. - apply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - (* processing of state *) - econstructor. - crush. - econstructor. - econstructor. - econstructor. - - all: invert MARR; big_tac. - Unshelve. - constructor. - Qed. - Hint Resolve transl_inop_correct : htlproof. - - Lemma transl_iop_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (op : Op.operation) (args : list Registers.reg) - (res0 : Registers.reg) (pc' : RTL.node) (v : Values.val), - (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> - Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. - Proof. - intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE. - inv_state. - exploit eval_correct; eauto. intros. inversion H1. inversion H2. - econstructor. split. - apply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - econstructor; simpl; trivial. - constructor; trivial. - econstructor; simpl; eauto. - simpl. econstructor. econstructor. - apply H3. simplify. - - all: big_tac. - - assert (Ple res0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - - unfold Ple in H10. lia. - apply regs_lessdef_add_match. assumption. - apply regs_lessdef_add_greater. unfold Plt; lia. assumption. - assert (Ple res0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in H12; lia. - unfold_merge. simpl. - rewrite AssocMap.gso. - apply AssocMap.gss. - apply st_greater_than_res. - - (*match_states*) - assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. - rewrite <- H1. - constructor; auto. - unfold_merge. - apply regs_lessdef_add_match. - constructor. - apply regs_lessdef_add_greater. - apply greater_than_max_func. - assumption. - - unfold state_st_wf. intros. inversion H2. subst. - unfold_merge. - rewrite AssocMap.gso. - apply AssocMap.gss. - apply st_greater_than_res. - - + econstructor. split. - apply Smallstep.plus_one. - eapply HTL.step_module; eauto. - econstructor; simpl; trivial. - constructor; trivial. - econstructor; simpl; eauto. - eapply eval_correct; eauto. - constructor. rewrite valueToInt_intToValue. trivial. - unfold_merge. simpl. - rewrite AssocMap.gso. - apply AssocMap.gss. - apply st_greater_than_res. - - match_states - assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. - rewrite <- H1. - constructor. - unfold_merge. - apply regs_lessdef_add_match. - constructor. - symmetry. apply valueToInt_intToValue. - apply regs_lessdef_add_greater. - apply greater_than_max_func. - assumption. assumption. - - unfold state_st_wf. intros. inversion H2. subst. - unfold_merge. - rewrite AssocMap.gso. - apply AssocMap.gss. - apply st_greater_than_res. - assumption. - Admitted. - Hint Resolve transl_iop_correct : htlproof. - - Ltac tac := - repeat match goal with - | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate - | [ _ : context[if (?x && ?y) then _ else _] |- _ ] => - let EQ1 := fresh "EQ" in - let EQ2 := fresh "EQ" in - destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in * - | [ _ : context[if ?x then _ else _] |- _ ] => - let EQ := fresh "EQ" in - destruct x eqn:EQ; simpl in * - | [ H : ret _ _ = _ |- _ ] => invert H - | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x - end. - - Ltac inv_arr_access := - match goal with - | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] => - destruct c, chunk, addr, args; crush; tac; crush - end. - - Lemma transl_iload_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) - (addr : Op.addressing) (args : list Registers.reg) (dst : Registers.reg) - (pc' : RTL.node) (a v : Values.val), - (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') -> - Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> - Mem.loadv chunk m a = Some v -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. - Proof. - intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. - inv_state. inv_arr_access. - - + (** Preamble *) - invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - unfold reg_stack_based_pointers in RSBP. - pose proof (RSBP r0) as RSBPr0. - - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. - - rewrite ARCHI in H1. crush. - subst. - - pose proof MASSOC as MASSOC'. - invert MASSOC'. - pose proof (H0 r0). - assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - apply H6 in HPler0. - invert HPler0; try congruence. - rewrite EQr0 in H8. - invert H8. - clear H0. clear H6. - - unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) - (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; crush. - rewrite Integers.Ptrofs.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. - apply PtrofsExtra.of_int_mod. - rewrite Integers.Int.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. } - - (** Read bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat x) - as EXPR_OK by admit - end. - rewrite <- EXPR_OK. - - specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - exploit H7; big_tac. - - (** RSBP preservation *) - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; big_tac. - rewrite NORMALISE in H0. rewrite H1 in H0. assumption. - - + (** Preamble *) - invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - unfold reg_stack_based_pointers in RSBP. - pose proof (RSBP r0) as RSBPr0. - pose proof (RSBP r1) as RSBPr1. - - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; - destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. - - rewrite ARCHI in H1. crush. - subst. - clear RSBPr1. - - pose proof MASSOC as MASSOC'. - invert MASSOC'. - pose proof (H0 r0). - pose proof (H0 r1). - assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - assert (HPler1 : Ple r1 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simpl; auto). - apply H6 in HPler0. - apply H8 in HPler1. - invert HPler0; invert HPler1; try congruence. - rewrite EQr0 in H9. - rewrite EQr1 in H11. - invert H9. invert H11. - clear H0. clear H6. clear H8. - - unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) - (Integers.Int.repr z0)))) as OFFSET. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; crush; try lia. - rewrite Integers.Ptrofs.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. - apply PtrofsExtra.of_int_mod. - apply IntExtra.add_mod; crush. - apply IntExtra.mul_mod2; crush. - rewrite Integers.Int.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. - rewrite Integers.Int.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. } - - (** Read bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat x) - as EXPR_OK by admit - end. - rewrite <- EXPR_OK. - - specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - exploit H7; big_tac. - - (** RSBP preservation *) - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; big_tac. - rewrite NORMALISE in H0. rewrite H1 in H0. assumption. - - + invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - rewrite ARCHI in H0. crush. - - unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; crush. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - rewrite ZERO in H1. clear ZERO. - rewrite Integers.Ptrofs.add_zero_l in H1. - - remember i0 as OFFSET. - - (** Modular preservation proof *) - rename H0 into MOD_PRESERVE. - - (** Read bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat x) - as EXPR_OK by admit - end. - rewrite <- EXPR_OK. - - specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - exploit H7; big_tac. - - (** RSBP preservation *) - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; big_tac. - rewrite NORMALISE in H0. rewrite H1 in H0. assumption. - Admitted. - Hint Resolve transl_iload_correct : htlproof. - - Lemma transl_istore_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) - (addr : Op.addressing) (args : list Registers.reg) (src : Registers.reg) - (pc' : RTL.node) (a : Values.val) (m' : mem), - (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') -> - Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> - Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. - Proof. - intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. - inv_state. inv_arr_access. - - + (** Preamble *) - invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - unfold reg_stack_based_pointers in RSBP. - pose proof (RSBP r0) as RSBPr0. - - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. - - rewrite ARCHI in H1. crush. - subst. - - pose proof MASSOC as MASSOC'. - invert MASSOC'. - pose proof (H0 r0). - assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - apply H6 in HPler0. - invert HPler0; try congruence. - rewrite EQr0 in H8. - invert H8. - clear H0. clear H6. - - unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) - (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; crush; try lia. - rewrite Integers.Ptrofs.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. - apply PtrofsExtra.of_int_mod. - rewrite Integers.Int.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. } - - (** Write bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat x) - as EXPR_OK by admit - end. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. - - econstructor. - repeat split; crush. - unfold HTL.empty_stack. - crush. - unfold Verilog.merge_arrs. - - rewrite AssocMap.gcombine. - 2: { reflexivity. } - unfold Verilog.arr_assocmap_set. - rewrite AssocMap.gss. - unfold Verilog.merge_arr. - rewrite AssocMap.gss. - setoid_rewrite H5. - reflexivity. - - rewrite combine_length. - rewrite <- array_set_len. - unfold arr_repeat. crush. - apply list_repeat_len. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. - rewrite H4. reflexivity. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) - (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. - - destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - - erewrite Mem.load_store_same. - 2: { rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite e. - rewrite Integers.Ptrofs.unsigned_repr. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - constructor. - erewrite combine_lookup_second. - simpl. - assert (Ple src (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simpl; auto); - apply H0 in H13. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - - assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H13. - rewrite Z_div_mult in H13; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia. - rewrite H13. rewrite EXPR_OK. - rewrite array_get_error_set_bound. - reflexivity. - unfold arr_length, arr_repeat. simpl. - rewrite list_repeat_len. lia. - - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. - simpl. - destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - rewrite Z2Nat.id in H15; try lia. - apply Zmult_lt_compat_r with (p := 4) in H15; try lia. - rewrite ZLib.div_mul_undo in H15; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - - rewrite <- EXPR_OK. - rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). - destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). - apply Z.mul_cancel_r with (p := 4) in e; try lia. - rewrite ZLib.div_mul_undo in e; try lia. - rewrite combine_lookup_first. - eapply H7; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - rewrite array_gso. - unfold array_get_error. - unfold arr_repeat. - crush. - apply list_repeat_lookup. - lia. - unfold_constants. - intro. - apply Z2Nat.inj_iff in H13; try lia. - apply Z.div_pos; try lia. - apply Integers.Ptrofs.unsigned_range. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - unfold arr_stack_based_pointers. - intros. - destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - - crush. - erewrite Mem.load_store_same. - 2: { rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite e. - rewrite Integers.Ptrofs.unsigned_repr. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - crush. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. - destruct (Archi.ptr64); try discriminate. - pose proof (RSBP src). rewrite EQ_SRC in H0. - assumption. - - simpl. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. - simpl. - destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - invert H0. - apply Zmult_lt_compat_r with (p := 4) in H14; try lia. - rewrite ZLib.div_mul_undo in H14; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - apply ASBP; assumption. - - unfold stack_bounds in *. intros. - simpl. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. right. simpl. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. - apply ZExtra.mod_0_bounds; crush; try lia. } - crush. - exploit (BOUNDS ptr); try lia. intros. crush. - exploit (BOUNDS ptr v); try lia. intros. - invert H0. - match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. - assert (Mem.valid_access m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) Writable). - { pose proof H1. eapply Mem.store_valid_access_2 in H0. - exact H0. eapply Mem.store_valid_access_3. eassumption. } - pose proof (Mem.valid_access_store m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) v). - apply X in H0. invert H0. congruence. - - + (** Preamble *) - invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - unfold reg_stack_based_pointers in RSBP. - pose proof (RSBP r0) as RSBPr0. - pose proof (RSBP r1) as RSBPr1. - - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; - destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. - - rewrite ARCHI in H1. crush. - subst. - clear RSBPr1. - - pose proof MASSOC as MASSOC'. - invert MASSOC'. - pose proof (H0 r0). - pose proof (H0 r1). - assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - assert (HPler1 : Ple r1 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simpl; auto). - apply H6 in HPler0. - apply H8 in HPler1. - invert HPler0; invert HPler1; try congruence. - rewrite EQr0 in H9. - rewrite EQr1 in H11. - invert H9. invert H11. - clear H0. clear H6. clear H8. - - unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) - (Integers.Int.repr z0)))) as OFFSET. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; crush; try lia. - rewrite Integers.Ptrofs.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. - apply PtrofsExtra.of_int_mod. - apply IntExtra.add_mod; crush. - apply IntExtra.mul_mod2; crush. - rewrite Integers.Int.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. - rewrite Integers.Int.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. } - - (** Write bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET destruct x eqn:EQ end; try reflexivity. - assert (Mem.valid_access m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) Writable). - { pose proof H1. eapply Mem.store_valid_access_2 in H0. - exact H0. eapply Mem.store_valid_access_3. eassumption. } - pose proof (Mem.valid_access_store m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) v). - apply X in H0. invert H0. congruence. - - + invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - rewrite ARCHI in H0. crush. - - unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; crush. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - rewrite ZERO in H1. clear ZERO. - rewrite Integers.Ptrofs.add_zero_l in H1. - - remember i0 as OFFSET. - - (** Modular preservation proof *) - rename H0 into MOD_PRESERVE. - - (** Write bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET destruct x eqn:EQ end; try reflexivity. - assert (Mem.valid_access m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) Writable). - { pose proof H1. eapply Mem.store_valid_access_2 in H0. - exact H0. eapply Mem.store_valid_access_3. eassumption. } - pose proof (Mem.valid_access_store m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) v). - apply X in H0. invert H0. congruence. - Admitted. - Hint Resolve transl_istore_correct : htlproof. - - Lemma transl_icond_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (cond : Op.condition) (args : list Registers.reg) - (ifso ifnot : RTL.node) (b : bool) (pc' : RTL.node), - (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) -> - Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> - pc' = (if b then ifso else ifnot) -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. - Proof. - intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE. - inv_state. - - eexists. split. apply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - eapply Verilog.stmnt_runp_Vnonblock_reg with - (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). - constructor. - - simpl. - destruct b. - eapply Verilog.erun_Vternary_true. - eapply eval_cond_correct; eauto. - constructor. - apply boolToValue_ValueToBool. - eapply Verilog.erun_Vternary_false. - eapply eval_cond_correct; eauto. - constructor. - apply boolToValue_ValueToBool. - constructor. - - big_tac. - - invert MARR. - destruct b; rewrite assumption_32bit; big_tac. - - Unshelve. - constructor. - Qed. - Hint Resolve transl_icond_correct : htlproof. - - Lemma transl_ijumptable_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node) - (n : Integers.Int.int) (pc' : RTL.node), - (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) -> - Registers.Regmap.get arg rs = Values.Vint n -> - list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. - Proof. - intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. - Admitted. - Hint Resolve transl_ijumptable_correct : htlproof. - - Lemma transl_ireturn_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) - (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) - (m' : mem), - (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> - Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> - forall R1 : HTL.state, - match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. - Proof. - intros s f stk pc rs m or m' H H0 R1 MSTATE. - inv_state. - - - econstructor. split. - eapply Smallstep.plus_two. - - eapply HTL.step_module; eauto. - apply assumption_32bit. - constructor. - econstructor; simpl; trivial. - econstructor; simpl; trivial. - constructor. - econstructor; simpl; trivial. - constructor. - - constructor. constructor. - - unfold state_st_wf in WF; big_tac; eauto. - - apply HTL.step_finish. - unfold Verilog.merge_regs. - unfold_merge; simpl. - rewrite AssocMap.gso. - apply AssocMap.gss. lia. - apply AssocMap.gss. - rewrite Events.E0_left. reflexivity. - - constructor; auto. - constructor. - - (* FIXME: Duplication *) - - econstructor. split. - eapply Smallstep.plus_two. - eapply HTL.step_module; eauto. - apply assumption_32bit. - constructor. - econstructor; simpl; trivial. - econstructor; simpl; trivial. - constructor. constructor. constructor. - constructor. constructor. constructor. - - unfold state_st_wf in WF; big_tac; eauto. - - apply HTL.step_finish. - unfold Verilog.merge_regs. - unfold_merge. - rewrite AssocMap.gso. - apply AssocMap.gss. simpl; lia. - apply AssocMap.gss. - rewrite Events.E0_left. trivial. - - constructor; auto. - - simpl. inversion MASSOC. subst. - unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. - apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. - assert (HPle : Ple r (RTL.max_reg_function f)). - eapply RTL.max_reg_function_use. eassumption. simpl; auto. - apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - - Unshelve. - all: constructor. - Qed. - Hint Resolve transl_ireturn_correct : htlproof. - - Lemma transl_callstate_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) - (m : mem) (m' : Mem.mem') (stk : Values.block), - Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> - forall R1 : HTL.state, - match_states (RTL.Callstate s (AST.Internal f) args m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states - (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) - (RTL.init_regs args (RTL.fn_params f)) m') R2. - Proof. - intros s f args m m' stk H R1 MSTATE. - - inversion MSTATE; subst. inversion TF; subst. - econstructor. split. apply Smallstep.plus_one. - eapply HTL.step_call. crush. - - apply match_state with (sp' := stk); eauto. - - all: big_tac. - - apply regs_lessdef_add_greater. - unfold Plt; lia. - apply init_reg_assoc_empty. - - constructor. - - destruct (Mem.load AST.Mint32 m' stk - (Integers.Ptrofs.unsigned (Integers.Ptrofs.add - Integers.Ptrofs.zero - (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. - pose proof Mem.load_alloc_same as LOAD_ALLOC. - pose proof H as ALLOC. - eapply LOAD_ALLOC in ALLOC. - 2: { exact LOAD. } - ptrofs. rewrite LOAD. - rewrite ALLOC. - repeat constructor. - - ptrofs. rewrite LOAD. - repeat constructor. - - unfold reg_stack_based_pointers. intros. - unfold RTL.init_regs; crush. - destruct (RTL.fn_params f); - rewrite Registers.Regmap.gi; constructor. - - unfold arr_stack_based_pointers. intros. - crush. - destruct (Mem.load AST.Mint32 m' stk - (Integers.Ptrofs.unsigned (Integers.Ptrofs.add - Integers.Ptrofs.zero - (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. - pose proof Mem.load_alloc_same as LOAD_ALLOC. - pose proof H as ALLOC. - eapply LOAD_ALLOC in ALLOC. - 2: { exact LOAD. } - rewrite ALLOC. - repeat constructor. - constructor. - - Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *) - Transparent Mem.load. - Transparent Mem.store. - unfold stack_bounds. - split. - - unfold Mem.alloc in H. - invert H. - crush. - unfold Mem.load. - intros. - match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H4. - unfold Mem.perm in H4. crush. - unfold Mem.perm_order' in H4. - small_tac. - exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. - rewrite Maps.PMap.gss in H8. - match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. - crush. - apply proj_sumbool_true in H10. lia. - - unfold Mem.alloc in H. - invert H. - crush. - unfold Mem.store. - intros. - match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H4. - unfold Mem.perm in H4. crush. - unfold Mem.perm_order' in H4. - small_tac. - exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. - rewrite Maps.PMap.gss in H8. - match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. - crush. - apply proj_sumbool_true in H10. lia. - Opaque Mem.alloc. - Opaque Mem.load. - Opaque Mem.store. - Qed. - Hint Resolve transl_callstate_correct : htlproof. - - Lemma transl_returnstate_correct: - forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) - (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) - (R1 : HTL.state), - match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. - Proof. - intros res0 f sp pc rs s vres m R1 MSTATE. - inversion MSTATE. inversion MF. - Qed. - Hint Resolve transl_returnstate_correct : htlproof. - - Lemma option_inv : - forall A x y, - @Some A x = Some y -> x = y. - Proof. intros. inversion H. trivial. Qed. - - Lemma main_tprog_internal : - forall b, - Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b -> - exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f). - Proof. - intros. - destruct TRANSL. unfold main_is_internal in H1. - repeat (unfold_match H1). replace b with b0. - exploit function_ptr_translated; eauto. intros [tf [A B]]. - unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B. - unfold_match B. inv B. econstructor. apply A. - - apply option_inv. rewrite <- Heqo. rewrite <- H. - rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). - trivial. symmetry; eapply Linking.match_program_main; eauto. - Qed. - - Lemma transl_initial_states : - forall s1 : Smallstep.state (RTL.semantics prog), - Smallstep.initial_state (RTL.semantics prog) s1 -> - exists s2 : Smallstep.state (HTL.semantics tprog), - Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2. - Proof. - induction 1. - destruct TRANSL. unfold main_is_internal in H4. - repeat (unfold_match H4). - assert (f = AST.Internal f1). apply option_inv. - rewrite <- Heqo0. rewrite <- H1. replace b with b0. - auto. apply option_inv. rewrite <- H0. rewrite <- Heqo. - trivial. - exploit function_ptr_translated; eauto. - intros [tf [A B]]. - unfold transl_fundef, Errors.bind in B. - unfold AST.transf_partial_fundef, Errors.bind in B. - repeat (unfold_match B). inversion B. subst. - exploit main_tprog_internal; eauto; intros. - rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). - apply Heqo. symmetry; eapply Linking.match_program_main; eauto. - inversion H5. - econstructor; split. econstructor. - apply (Genv.init_mem_transf_partial TRANSL'); eauto. - replace (AST.prog_main tprog) with (AST.prog_main prog). - rewrite symbols_preserved; eauto. - symmetry; eapply Linking.match_program_main; eauto. - apply H6. - - constructor. - apply transl_module_correct. - assert (Some (AST.Internal x) = Some (AST.Internal m)). - replace (AST.fundef HTL.module) with (HTL.fundef). - rewrite <- H6. setoid_rewrite <- A. trivial. - trivial. inv H7. assumption. - Qed. - Hint Resolve transl_initial_states : htlproof. - - Lemma transl_final_states : - forall (s1 : Smallstep.state (RTL.semantics prog)) - (s2 : Smallstep.state (HTL.semantics tprog)) - (r : Integers.Int.int), - match_states s1 s2 -> - Smallstep.final_state (RTL.semantics prog) s1 r -> - Smallstep.final_state (HTL.semantics tprog) s2 r. - Proof. - intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity. - Qed. - Hint Resolve transl_final_states : htlproof. - - Theorem transl_step_correct: - forall (S1 : RTL.state) t S2, - RTL.step ge S1 t S2 -> - forall (R1 : HTL.state), - match_states S1 R1 -> - exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. - Proof. - induction 1; eauto with htlproof; (intros; inv_state). - Qed. - Hint Resolve transl_step_correct : htlproof. - - Theorem transf_program_correct: - Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). - Proof. - eapply Smallstep.forward_simulation_plus; eauto with htlproof. - apply senv_preserved. - Qed. - -End CORRECTNESS. +(* Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := *) +(* match_assocmap : forall f rs am, *) +(* (forall r, Ple r (RTL.max_reg_function f) -> *) +(* val_value_lessdef (Registers.Regmap.get r rs) am#r) -> *) +(* match_assocmaps f rs am. *) +(* 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 st). *) +(* Hint Unfold state_st_wf : htlproof. *) + +(* Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : *) +(* Verilog.assocmap_arr -> Prop := *) +(* | match_arr : forall asa stack, *) +(* asa ! (m.(HTL.mod_stk)) = Some stack /\ *) +(* stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\ *) +(* (forall ptr, *) +(* 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 0) *) +(* (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> *) +(* match_arrs m f sp mem asa. *) + +(* Definition stack_based (v : Values.val) (sp : Values.block) : Prop := *) +(* match v with *) +(* | Values.Vptr sp' off => sp' = sp *) +(* | _ => True *) +(* end. *) + +(* Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop := *) +(* forall r, stack_based (Registers.Regmap.get r rs) sp. *) + +(* Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z) *) +(* (sp : Values.val) : Prop := *) +(* forall ptr, *) +(* 0 <= ptr < (stack_length / 4) -> *) +(* stack_based (Option.default *) +(* Values.Vundef *) +(* (Mem.loadv AST.Mint32 m *) +(* (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))) *) +(* spb. *) + +(* Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop := *) +(* forall ptr v, *) +(* hi <= ptr <= Integers.Ptrofs.max_unsigned -> *) +(* Z.modulo ptr 4 = 0 -> *) +(* Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\ *) +(* Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None. *) + +(* Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop := *) +(* | match_frames_nil : *) +(* match_frames nil nil. *) + +(* Lemma assumption_32bit : *) +(* forall v, *) +(* valueToPos (posToValue v) = v. *) +(* Proof. *) +(* Admitted. *) + +(* Inductive match_states : RTL.state -> HTL.state -> Prop := *) +(* | match_state : forall asa asr sf f sp sp' rs mem m st res *) +(* (MASSOC : match_assocmaps f rs asr) *) +(* (TF : tr_module f m) *) +(* (WF : state_st_wf m (HTL.State res m st asr asa)) *) +(* (MF : match_frames sf res) *) +(* (MARR : match_arrs m f sp mem asa) *) +(* (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) *) +(* (RSBP : reg_stack_based_pointers sp' rs) *) +(* (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) *) +(* (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem), *) +(* match_states (RTL.State sf f sp st rs mem) *) +(* (HTL.State res m st asr asa) *) +(* | match_returnstate : *) +(* forall *) +(* v v' stack mem res *) +(* (MF : match_frames stack res), *) +(* val_value_lessdef v v' -> *) +(* match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v') *) +(* | match_initial_call : *) +(* forall f m m0 *) +(* (TF : tr_module f m), *) +(* match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil). *) +(* Hint Constructors match_states : htlproof. *) + +(* Definition match_prog (p: RTL.program) (tp: HTL.program) := *) +(* Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ *) +(* main_is_internal p = true. *) + +(* Definition match_prog_matches : *) +(* forall p tp, *) +(* match_prog p tp -> *) +(* Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. *) +(* Proof. intros. unfold match_prog in H. tauto. Qed. *) + +(* Lemma transf_program_match: *) +(* forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp. *) +(* Proof. *) +(* intros. unfold transl_program in H. *) +(* destruct (main_is_internal p) eqn:?; try discriminate. *) +(* unfold match_prog. split. *) +(* apply Linking.match_transform_partial_program; auto. *) +(* assumption. *) +(* Qed. *) + +(* Lemma regs_lessdef_add_greater : *) +(* forall f rs1 rs2 n v, *) +(* Plt (RTL.max_reg_function f) n -> *) +(* match_assocmaps f rs1 rs2 -> *) +(* match_assocmaps f rs1 (AssocMap.set n v rs2). *) +(* Proof. *) +(* inversion 2; subst. *) +(* intros. constructor. *) +(* intros. unfold find_assocmap. unfold AssocMapExt.get_default. *) +(* rewrite AssocMap.gso. eauto. *) +(* apply Pos.le_lt_trans with _ _ n in H2. *) +(* unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. *) +(* Qed. *) +(* Hint Resolve regs_lessdef_add_greater : htlproof. *) + +(* Lemma regs_lessdef_add_match : *) +(* forall f rs am r v v', *) +(* val_value_lessdef v v' -> *) +(* match_assocmaps f rs am -> *) +(* match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am). *) +(* Proof. *) +(* inversion 2; subst. *) +(* constructor. intros. *) +(* destruct (peq r0 r); subst. *) +(* rewrite Registers.Regmap.gss. *) +(* unfold find_assocmap. unfold AssocMapExt.get_default. *) +(* rewrite AssocMap.gss. assumption. *) + +(* rewrite Registers.Regmap.gso; try assumption. *) +(* unfold find_assocmap. unfold AssocMapExt.get_default. *) +(* rewrite AssocMap.gso; eauto. *) +(* Qed. *) +(* Hint Resolve regs_lessdef_add_match : htlproof. *) + +(* Lemma list_combine_none : *) +(* forall n l, *) +(* length l = n -> *) +(* list_combine Verilog.merge_cell (list_repeat None n) l = l. *) +(* Proof. *) +(* induction n; intros; crush. *) +(* - symmetry. apply length_zero_iff_nil. auto. *) +(* - destruct l; crush. *) +(* rewrite list_repeat_cons. *) +(* crush. f_equal. *) +(* eauto. *) +(* Qed. *) + +(* Lemma combine_none : *) +(* forall n a, *) +(* a.(arr_length) = n -> *) +(* arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. *) +(* Proof. *) +(* intros. *) +(* unfold combine. *) +(* crush. *) + +(* rewrite <- (arr_wf a) in H. *) +(* apply list_combine_none. *) +(* assumption. *) +(* Qed. *) + +(* Lemma list_combine_lookup_first : *) +(* forall l1 l2 n, *) +(* length l1 = length l2 -> *) +(* nth_error l1 n = Some None -> *) +(* nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n. *) +(* Proof. *) +(* induction l1; intros; crush. *) + +(* rewrite nth_error_nil in H0. *) +(* discriminate. *) + +(* destruct l2 eqn:EQl2. crush. *) +(* simpl in H. invert H. *) +(* destruct n; simpl in *. *) +(* invert H0. simpl. reflexivity. *) +(* eauto. *) +(* Qed. *) + +(* Lemma combine_lookup_first : *) +(* forall a1 a2 n, *) +(* a1.(arr_length) = a2.(arr_length) -> *) +(* array_get_error n a1 = Some None -> *) +(* array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2. *) +(* Proof. *) +(* intros. *) + +(* unfold array_get_error in *. *) +(* apply list_combine_lookup_first; eauto. *) +(* rewrite a1.(arr_wf). rewrite a2.(arr_wf). *) +(* assumption. *) +(* Qed. *) + +(* Lemma list_combine_lookup_second : *) +(* forall l1 l2 n x, *) +(* length l1 = length l2 -> *) +(* nth_error l1 n = Some (Some x) -> *) +(* nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x). *) +(* Proof. *) +(* induction l1; intros; crush; auto. *) + +(* destruct l2 eqn:EQl2. crush. *) +(* simpl in H. invert H. *) +(* destruct n; simpl in *. *) +(* invert H0. simpl. reflexivity. *) +(* eauto. *) +(* Qed. *) + +(* Lemma combine_lookup_second : *) +(* forall a1 a2 n x, *) +(* a1.(arr_length) = a2.(arr_length) -> *) +(* array_get_error n a1 = Some (Some x) -> *) +(* array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x). *) +(* Proof. *) +(* intros. *) + +(* unfold array_get_error in *. *) +(* apply list_combine_lookup_second; eauto. *) +(* rewrite a1.(arr_wf). rewrite a2.(arr_wf). *) +(* assumption. *) +(* Qed. *) + +(* Ltac inv_state := *) +(* match goal with *) +(* MSTATE : match_states _ _ |- _ => *) +(* inversion MSTATE; *) +(* match goal with *) +(* TF : tr_module _ _ |- _ => *) +(* inversion TF; *) +(* match goal with *) +(* TC : forall _ _, *) +(* Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _, *) +(* H : Maps.PTree.get _ _ = Some _ |- _ => *) +(* apply TC in H; inversion H; *) +(* match goal with *) +(* TI : context[tr_instr] |- _ => *) +(* inversion TI *) +(* end *) +(* end *) +(* end *) +(* end; subst. *) + +(* Ltac unfold_func H := *) +(* match type of H with *) +(* | ?f = _ => unfold f in H; repeat (unfold_match H) *) +(* | ?f _ = _ => unfold f in H; repeat (unfold_match H) *) +(* | ?f _ _ = _ => unfold f in H; repeat (unfold_match H) *) +(* | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H) *) +(* | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H) *) +(* end. *) + +(* Lemma init_reg_assoc_empty : *) +(* forall f l, *) +(* match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l). *) +(* Proof. *) +(* induction l; simpl; constructor; intros. *) +(* - rewrite Registers.Regmap.gi. unfold find_assocmap. *) +(* unfold AssocMapExt.get_default. rewrite AssocMap.gempty. *) +(* constructor. *) + +(* - rewrite Registers.Regmap.gi. unfold find_assocmap. *) +(* unfold AssocMapExt.get_default. rewrite AssocMap.gempty. *) +(* constructor. *) +(* Qed. *) + +(* Lemma arr_lookup_some: *) +(* forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr) *) +(* (stack : Array (option value)) (H5 : asa ! r = Some stack) n, *) +(* exists x, Verilog.arr_assocmap_lookup asa r n = Some x. *) +(* Proof. *) +(* intros z r0 r asr asa stack H5 n. *) +(* eexists. *) +(* unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity. *) +(* Qed. *) +(* Hint Resolve arr_lookup_some : htlproof. *) + +(* Section CORRECTNESS. *) + +(* Variable prog : RTL.program. *) +(* Variable tprog : HTL.program. *) + +(* Hypothesis TRANSL : match_prog prog tprog. *) + +(* Lemma TRANSL' : *) +(* Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. *) +(* Proof. intros; apply match_prog_matches; assumption. Qed. *) + +(* Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. *) +(* Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. *) + +(* Lemma symbols_preserved: *) +(* forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. *) +(* Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed. *) + +(* Lemma function_ptr_translated: *) +(* forall (b: Values.block) (f: RTL.fundef), *) +(* Genv.find_funct_ptr ge b = Some f -> *) +(* exists tf, *) +(* Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. *) +(* Proof. *) +(* intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. *) +(* intros (cu & tf & P & Q & R); exists tf; auto. *) +(* Qed. *) + +(* Lemma functions_translated: *) +(* forall (v: Values.val) (f: RTL.fundef), *) +(* Genv.find_funct ge v = Some f -> *) +(* exists tf, *) +(* Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. *) +(* Proof. *) +(* intros. exploit (Genv.find_funct_match TRANSL'); eauto. *) +(* intros (cu & tf & P & Q & R); exists tf; auto. *) +(* Qed. *) + +(* Lemma senv_preserved: *) +(* Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). *) +(* Proof *) +(* (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) -> *) +(* (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> *) +(* Op.eval_operation ge sp op *) +(* (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> *) +(* translate_instr op args s = OK e s' i -> *) +(* exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. *) +(* Proof. *) +(* 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; *) +(* unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); simplify. *) +(* - 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. 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 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. *) +(* Admitted. *) + +(* Lemma eval_cond_correct : *) +(* forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, *) +(* translate_condition cond args s1 = OK c s' i -> *) +(* Op.eval_condition *) +(* cond *) +(* (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) *) +(* m = Some b -> *) +(* Verilog.expr_runp f asr asa c (boolToValue b). *) +(* Admitted. *) + +(* (** The proof of semantic preservation for the translation of instructions *) +(* is a simulation argument based on diagrams of the following form: *) +(* << *) +(* match_states *) +(* code st rs ---------------- State m st assoc *) +(* || | *) +(* || | *) +(* || | *) +(* \/ v *) +(* code st rs' --------------- State m st assoc' *) +(* match_states *) +(* >> *) +(* where [tr_code c data control fin rtrn st] is assumed to hold. *) + +(* The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. *) +(* *) *) + +(* Definition transl_instr_prop (instr : RTL.instruction) : Prop := *) +(* forall m asr asa fin rtrn st stmt trans res, *) +(* tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans -> *) +(* exists asr' asa', *) +(* HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). *) + +(* Opaque combine. *) + +(* Ltac tac0 := *) +(* match goal with *) +(* | [ |- context[valueToPos (posToValue _)] ] => rewrite assumption_32bit *) + +(* | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs *) +(* | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr *) +(* | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge *) +(* | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros *) +(* | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set *) + +(* | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack *) + +(* | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss *) +(* | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso *) +(* | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty *) + +(* | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] => *) +(* rewrite combine_lookup_first *) + +(* | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1 *) +(* | [ |- context[match_states _ _] ] => econstructor; auto *) +(* | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto *) +(* | [ |- match_assocmaps _ _ _ # _ <- (posToValue _) ] => *) +(* apply regs_lessdef_add_greater; [> unfold Plt; lia | assumption] *) + +(* | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => *) +(* unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal *) +(* | [ |- context[(AssocMap.combine _ _ _) ! _] ] => *) +(* try (rewrite AssocMap.gcombine; [> | reflexivity]) *) + +(* | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] => *) +(* rewrite Registers.Regmap.gss *) +(* | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] => *) +(* destruct (Pos.eq_dec s d) as [EQ|EQ]; *) +(* [> rewrite EQ | rewrite Registers.Regmap.gso; auto] *) + +(* | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H *) +(* | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |] *) +(* | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H *) +(* end. *) + +(* Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto. *) +(* Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto. *) + + (* Lemma transl_inop_correct: *) + (* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) + (* (rs : RTL.regset) (m : mem) (pc' : RTL.node), *) + (* (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> *) + (* forall R1 : HTL.state, *) + (* match_states (RTL.State s f sp pc rs m) R1 -> *) + (* exists R2 : HTL.state, *) + (* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *) + (* Proof. *) + (* intros s f sp pc rs m pc' H R1 MSTATE. *) + (* inv_state. *) + + (* unfold match_prog in TRANSL. *) + (* econstructor. *) + (* split. *) + (* apply Smallstep.plus_one. *) + (* eapply HTL.step_module; eauto. *) + (* apply assumption_32bit. *) + (* (* processing of state *) *) + (* econstructor. *) + (* crush. *) + (* econstructor. *) + (* econstructor. *) + (* econstructor. *) + + (* all: invert MARR; big_tac. *) + (* Unshelve. *) + (* constructor. *) + (* Qed. *) + (* Hint Resolve transl_inop_correct : htlproof. *) + + (* Lemma transl_iop_correct: *) + (* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) + (* (rs : Registers.Regmap.t Values.val) (m : mem) (op : Op.operation) (args : list Registers.reg) *) + (* (res0 : Registers.reg) (pc' : RTL.node) (v : Values.val), *) + (* (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> *) + (* Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> *) + (* forall R1 : HTL.state, *) + (* match_states (RTL.State s f sp pc rs m) R1 -> *) + (* exists R2 : HTL.state, *) + (* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *) + (* match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. *) + (* Proof. *) + (* intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE. *) + (* inv_state. *) + (* exploit eval_correct; eauto. intros. inversion H1. inversion H2. *) + (* econstructor. split. *) + (* apply Smallstep.plus_one. *) + (* eapply HTL.step_module; eauto. *) + (* apply assumption_32bit. *) + (* econstructor; simpl; trivial. *) + (* constructor; trivial. *) + (* econstructor; simpl; eauto. *) + (* simpl. econstructor. econstructor. *) + (* apply H3. simplify. *) + + (* all: big_tac. *) + + (* assert (Ple res0 (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) + + (* unfold Ple in H10. lia. *) + (* apply regs_lessdef_add_match. assumption. *) + (* apply regs_lessdef_add_greater. unfold Plt; lia. assumption. *) + (* assert (Ple res0 (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) + (* unfold Ple in H12; lia. *) + (* unfold_merge. simpl. *) + (* rewrite AssocMap.gso. *) + (* apply AssocMap.gss. *) + (* apply st_greater_than_res. *) + + (* (*match_states*) *) + (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *) + (* rewrite <- H1. *) + (* constructor; auto. *) + (* unfold_merge. *) + (* apply regs_lessdef_add_match. *) + (* constructor. *) + (* apply regs_lessdef_add_greater. *) + (* apply greater_than_max_func. *) + (* assumption. *) + + (* unfold state_st_wf. intros. inversion H2. subst. *) + (* unfold_merge. *) + (* rewrite AssocMap.gso. *) + (* apply AssocMap.gss. *) + (* apply st_greater_than_res. *) + + (* + econstructor. split. *) + (* apply Smallstep.plus_one. *) + (* eapply HTL.step_module; eauto. *) + (* econstructor; simpl; trivial. *) + (* constructor; trivial. *) + (* econstructor; simpl; eauto. *) + (* eapply eval_correct; eauto. *) + (* constructor. rewrite valueToInt_intToValue. trivial. *) + (* unfold_merge. simpl. *) + (* rewrite AssocMap.gso. *) + (* apply AssocMap.gss. *) + (* apply st_greater_than_res. *) + + (* match_states *) + (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *) + (* rewrite <- H1. *) + (* constructor. *) + (* unfold_merge. *) + (* apply regs_lessdef_add_match. *) + (* constructor. *) + (* symmetry. apply valueToInt_intToValue. *) + (* apply regs_lessdef_add_greater. *) + (* apply greater_than_max_func. *) + (* assumption. assumption. *) + + (* unfold state_st_wf. intros. inversion H2. subst. *) + (* unfold_merge. *) + (* rewrite AssocMap.gso. *) + (* apply AssocMap.gss. *) + (* apply st_greater_than_res. *) + (* assumption. *) + (* Admitted. *) + (* Hint Resolve transl_iop_correct : htlproof. *) + + (* Ltac tac := *) + (* repeat match goal with *) + (* | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate *) + (* | [ _ : context[if (?x && ?y) then _ else _] |- _ ] => *) + (* let EQ1 := fresh "EQ" in *) + (* let EQ2 := fresh "EQ" in *) + (* destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in * *) + (* | [ _ : context[if ?x then _ else _] |- _ ] => *) + (* let EQ := fresh "EQ" in *) + (* destruct x eqn:EQ; simpl in * *) + (* | [ H : ret _ _ = _ |- _ ] => invert H *) + (* | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x *) + (* end. *) + + (* Ltac inv_arr_access := *) + (* match goal with *) + (* | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] => *) + (* destruct c, chunk, addr, args; crush; tac; crush *) + (* end. *) + + (* Lemma transl_iload_correct: *) + (* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) + (* (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) *) + (* (addr : Op.addressing) (args : list Registers.reg) (dst : Registers.reg) *) + (* (pc' : RTL.node) (a v : Values.val), *) + (* (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') -> *) + (* Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> *) + (* Mem.loadv chunk m a = Some v -> *) + (* forall R1 : HTL.state, *) + (* match_states (RTL.State s f sp pc rs m) R1 -> *) + (* exists R2 : HTL.state, *) + (* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *) + (* match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. *) + (* Proof. *) + (* intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. *) + (* inv_state. inv_arr_access. *) + + (* + (** Preamble *) *) + (* invert MARR. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + + (* unfold reg_stack_based_pointers in RSBP. *) + (* pose proof (RSBP r0) as RSBPr0. *) + + (* destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. *) + + (* rewrite ARCHI in H1. crush. *) + (* subst. *) + + (* pose proof MASSOC as MASSOC'. *) + (* invert MASSOC'. *) + (* pose proof (H0 r0). *) + (* assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *) + (* apply H6 in HPler0. *) + (* invert HPler0; try congruence. *) + (* rewrite EQr0 in H8. *) + (* invert H8. *) + (* clear H0. clear H6. *) + + (* unfold check_address_parameter_signed in *; *) + (* unfold check_address_parameter_unsigned in *; crush. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) + (* (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *) + + (* (** Modular preservation proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) + (* { rewrite HeqOFFSET. *) + (* apply PtrofsExtra.add_mod; crush. *) + (* rewrite Integers.Ptrofs.unsigned_repr_eq. *) + (* rewrite <- Zmod_div_mod; crush. *) + (* apply PtrofsExtra.of_int_mod. *) + (* rewrite Integers.Int.unsigned_repr_eq. *) + (* rewrite <- Zmod_div_mod; crush. } *) + + (* (** Read bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET *) + (* assert (Z.to_nat *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu *) + (* OFFSET *) + (* (Integers.Ptrofs.repr 4))) *) + (* = *) + (* valueToNat x) *) + (* as EXPR_OK by admit *) + (* end. *) + (* rewrite <- EXPR_OK. *) + + (* specialize (H7 (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu *) + (* OFFSET *) + (* (Integers.Ptrofs.repr 4)))). *) + (* exploit H7; big_tac. *) + + (* (** RSBP preservation *) *) + (* unfold arr_stack_based_pointers in ASBP. *) + (* specialize (ASBP (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *) + (* exploit ASBP; big_tac. *) + (* rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *) + + (* + (** Preamble *) *) + (* invert MARR. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + + (* unfold reg_stack_based_pointers in RSBP. *) + (* pose proof (RSBP r0) as RSBPr0. *) + (* pose proof (RSBP r1) as RSBPr1. *) + + (* destruct (Registers.Regmap.get r0 rs) eqn:EQr0; *) + (* destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. *) + + (* rewrite ARCHI in H1. crush. *) + (* subst. *) + (* clear RSBPr1. *) + + (* pose proof MASSOC as MASSOC'. *) + (* invert MASSOC'. *) + (* pose proof (H0 r0). *) + (* pose proof (H0 r1). *) + (* assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *) + (* assert (HPler1 : Ple r1 (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *) + (* apply H6 in HPler0. *) + (* apply H8 in HPler1. *) + (* invert HPler0; invert HPler1; try congruence. *) + (* rewrite EQr0 in H9. *) + (* rewrite EQr1 in H11. *) + (* invert H9. invert H11. *) + (* clear H0. clear H6. clear H8. *) + + (* unfold check_address_parameter_signed in *; *) + (* unfold check_address_parameter_unsigned in *; crush. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) + (* (Integers.Ptrofs.of_int *) + (* (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *) + (* (Integers.Int.repr z0)))) as OFFSET. *) + + (* (** Modular preservation proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) + (* { rewrite HeqOFFSET. *) + (* apply PtrofsExtra.add_mod; crush; try lia. *) + (* rewrite Integers.Ptrofs.unsigned_repr_eq. *) + (* rewrite <- Zmod_div_mod; crush. *) + (* apply PtrofsExtra.of_int_mod. *) + (* apply IntExtra.add_mod; crush. *) + (* apply IntExtra.mul_mod2; crush. *) + (* rewrite Integers.Int.unsigned_repr_eq. *) + (* rewrite <- Zmod_div_mod; crush. *) + (* rewrite Integers.Int.unsigned_repr_eq. *) + (* rewrite <- Zmod_div_mod; crush. } *) + + (* (** Read bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET *) + (* assert (Z.to_nat *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu *) + (* OFFSET *) + (* (Integers.Ptrofs.repr 4))) *) + (* = *) + (* valueToNat x) *) + (* as EXPR_OK by admit *) + (* end. *) + (* rewrite <- EXPR_OK. *) + + (* specialize (H7 (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu *) + (* OFFSET *) + (* (Integers.Ptrofs.repr 4)))). *) + (* exploit H7; big_tac. *) + + (* (** RSBP preservation *) *) + (* unfold arr_stack_based_pointers in ASBP. *) + (* specialize (ASBP (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *) + (* exploit ASBP; big_tac. *) + (* rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *) + + (* + invert MARR. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + (* rewrite ARCHI in H0. crush. *) + + (* unfold check_address_parameter_unsigned in *; *) + (* unfold check_address_parameter_signed in *; crush. *) + + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* rewrite ZERO in H1. clear ZERO. *) + (* rewrite Integers.Ptrofs.add_zero_l in H1. *) + + (* remember i0 as OFFSET. *) + + (* (** Modular preservation proof *) *) + (* rename H0 into MOD_PRESERVE. *) + + (* (** Read bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET *) + (* assert (Z.to_nat *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu *) + (* OFFSET *) + (* (Integers.Ptrofs.repr 4))) *) + (* = *) + (* valueToNat x) *) + (* as EXPR_OK by admit *) + (* end. *) + (* rewrite <- EXPR_OK. *) + + (* specialize (H7 (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu *) + (* OFFSET *) + (* (Integers.Ptrofs.repr 4)))). *) + (* exploit H7; big_tac. *) + + (* (** RSBP preservation *) *) + (* unfold arr_stack_based_pointers in ASBP. *) + (* specialize (ASBP (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *) + (* exploit ASBP; big_tac. *) + (* rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *) + (* Admitted. *) + (* Hint Resolve transl_iload_correct : htlproof. *) + + (* Lemma transl_istore_correct: *) + (* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) + (* (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) *) + (* (addr : Op.addressing) (args : list Registers.reg) (src : Registers.reg) *) + (* (pc' : RTL.node) (a : Values.val) (m' : mem), *) + (* (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') -> *) + (* Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> *) + (* Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' -> *) + (* forall R1 : HTL.state, *) + (* match_states (RTL.State s f sp pc rs m) R1 -> *) + (* exists R2 : HTL.state, *) + (* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. *) + (* Proof. *) + (* intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. *) + (* inv_state. inv_arr_access. *) + + (* + (** Preamble *) *) + (* invert MARR. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + + (* unfold reg_stack_based_pointers in RSBP. *) + (* pose proof (RSBP r0) as RSBPr0. *) + + (* destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. *) + + (* rewrite ARCHI in H1. crush. *) + (* subst. *) + + (* pose proof MASSOC as MASSOC'. *) + (* invert MASSOC'. *) + (* pose proof (H0 r0). *) + (* assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *) + (* apply H6 in HPler0. *) + (* invert HPler0; try congruence. *) + (* rewrite EQr0 in H8. *) + (* invert H8. *) + (* clear H0. clear H6. *) + + (* unfold check_address_parameter_unsigned in *; *) + (* unfold check_address_parameter_signed in *; crush. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) + (* (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *) + + (* (** Modular preservation proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) + (* { rewrite HeqOFFSET. *) + (* apply PtrofsExtra.add_mod; crush; try lia. *) + (* rewrite Integers.Ptrofs.unsigned_repr_eq. *) + (* rewrite <- Zmod_div_mod; crush. *) + (* apply PtrofsExtra.of_int_mod. *) + (* rewrite Integers.Int.unsigned_repr_eq. *) + (* rewrite <- Zmod_div_mod; crush. } *) + + (* (** Write bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET *) + (* assert (Z.to_nat *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu *) + (* OFFSET *) + (* (Integers.Ptrofs.repr 4))) *) + (* = *) + (* valueToNat x) *) + (* as EXPR_OK by admit *) + (* end. *) + + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *) + + (* econstructor. *) + (* repeat split; crush. *) + (* unfold HTL.empty_stack. *) + (* crush. *) + (* unfold Verilog.merge_arrs. *) + + (* rewrite AssocMap.gcombine. *) + (* 2: { reflexivity. } *) + (* unfold Verilog.arr_assocmap_set. *) + (* rewrite AssocMap.gss. *) + (* unfold Verilog.merge_arr. *) + (* rewrite AssocMap.gss. *) + (* setoid_rewrite H5. *) + (* reflexivity. *) + + (* rewrite combine_length. *) + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* apply list_repeat_len. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite list_repeat_len. *) + (* rewrite H4. reflexivity. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) + (* (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *) + + (* destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *) + + (* erewrite Mem.load_store_same. *) + (* 2: { rewrite ZERO. *) + (* rewrite Integers.Ptrofs.add_zero_l. *) + (* rewrite e. *) + (* rewrite Integers.Ptrofs.unsigned_repr. *) + (* exact H1. *) + (* apply Integers.Ptrofs.unsigned_range_2. } *) + (* constructor. *) + (* erewrite combine_lookup_second. *) + (* simpl. *) + (* assert (Ple src (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) + (* apply H0 in H13. *) + (* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite list_repeat_len. auto. *) + + (* assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *) + (* rewrite Z.mul_comm in H13. *) + (* rewrite Z_div_mult in H13; try lia. *) + (* replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity. *) + (* rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia. *) + (* rewrite H13. rewrite EXPR_OK. *) + (* rewrite array_get_error_set_bound. *) + (* reflexivity. *) + (* unfold arr_length, arr_repeat. simpl. *) + (* rewrite list_repeat_len. lia. *) + + (* erewrite Mem.load_store_other with (m1 := m). *) + (* 2: { exact H1. } *) + (* 2: { right. *) + (* rewrite ZERO. *) + (* rewrite Integers.Ptrofs.add_zero_l. *) + (* rewrite Integers.Ptrofs.unsigned_repr. *) + (* simpl. *) + (* destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *) + (* right. *) + (* apply ZExtra.mod_0_bounds; try lia. *) + (* apply ZLib.Z_mod_mult'. *) + (* rewrite Z2Nat.id in H15; try lia. *) + (* apply Zmult_lt_compat_r with (p := 4) in H15; try lia. *) + (* rewrite ZLib.div_mul_undo in H15; try lia. *) + (* split; try lia. *) + (* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) + (* } *) + + (* rewrite <- EXPR_OK. *) + (* rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). *) + (* destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). *) + (* apply Z.mul_cancel_r with (p := 4) in e; try lia. *) + (* rewrite ZLib.div_mul_undo in e; try lia. *) + (* rewrite combine_lookup_first. *) + (* eapply H7; eauto. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite list_repeat_len. auto. *) + (* rewrite array_gso. *) + (* unfold array_get_error. *) + (* unfold arr_repeat. *) + (* crush. *) + (* apply list_repeat_lookup. *) + (* lia. *) + (* unfold_constants. *) + (* intro. *) + (* apply Z2Nat.inj_iff in H13; try lia. *) + (* apply Z.div_pos; try lia. *) + (* apply Integers.Ptrofs.unsigned_range. *) + + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* unfold arr_stack_based_pointers. *) + (* intros. *) + (* destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *) + + (* crush. *) + (* erewrite Mem.load_store_same. *) + (* 2: { rewrite ZERO. *) + (* rewrite Integers.Ptrofs.add_zero_l. *) + (* rewrite e. *) + (* rewrite Integers.Ptrofs.unsigned_repr. *) + (* exact H1. *) + (* apply Integers.Ptrofs.unsigned_range_2. } *) + (* crush. *) + (* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *) + (* destruct (Archi.ptr64); try discriminate. *) + (* pose proof (RSBP src). rewrite EQ_SRC in H0. *) + (* assumption. *) + + (* simpl. *) + (* erewrite Mem.load_store_other with (m1 := m). *) + (* 2: { exact H1. } *) + (* 2: { right. *) + (* rewrite ZERO. *) + (* rewrite Integers.Ptrofs.add_zero_l. *) + (* rewrite Integers.Ptrofs.unsigned_repr. *) + (* simpl. *) + (* destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *) + (* right. *) + (* apply ZExtra.mod_0_bounds; try lia. *) + (* apply ZLib.Z_mod_mult'. *) + (* invert H0. *) + (* apply Zmult_lt_compat_r with (p := 4) in H14; try lia. *) + (* rewrite ZLib.div_mul_undo in H14; try lia. *) + (* split; try lia. *) + (* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) + (* } *) + (* apply ASBP; assumption. *) + + (* unfold stack_bounds in *. intros. *) + (* simpl. *) + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* erewrite Mem.load_store_other with (m1 := m). *) + (* 2: { exact H1. } *) + (* 2: { right. right. simpl. *) + (* rewrite ZERO. *) + (* rewrite Integers.Ptrofs.add_zero_l. *) + (* rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *) + (* apply ZExtra.mod_0_bounds; crush; try lia. } *) + (* crush. *) + (* exploit (BOUNDS ptr); try lia. intros. crush. *) + (* exploit (BOUNDS ptr v); try lia. intros. *) + (* invert H0. *) + (* match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *) + (* assert (Mem.valid_access m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) Writable). *) + (* { pose proof H1. eapply Mem.store_valid_access_2 in H0. *) + (* exact H0. eapply Mem.store_valid_access_3. eassumption. } *) + (* pose proof (Mem.valid_access_store m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) v). *) + (* apply X in H0. invert H0. congruence. *) + + (* + (** Preamble *) *) + (* invert MARR. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + + (* unfold reg_stack_based_pointers in RSBP. *) + (* pose proof (RSBP r0) as RSBPr0. *) + (* pose proof (RSBP r1) as RSBPr1. *) + + (* destruct (Registers.Regmap.get r0 rs) eqn:EQr0; *) + (* destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. *) + + (* rewrite ARCHI in H1. crush. *) + (* subst. *) + (* clear RSBPr1. *) + + (* pose proof MASSOC as MASSOC'. *) + (* invert MASSOC'. *) + (* pose proof (H0 r0). *) + (* pose proof (H0 r1). *) + (* assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *) + (* assert (HPler1 : Ple r1 (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *) + (* apply H6 in HPler0. *) + (* apply H8 in HPler1. *) + (* invert HPler0; invert HPler1; try congruence. *) + (* rewrite EQr0 in H9. *) + (* rewrite EQr1 in H11. *) + (* invert H9. invert H11. *) + (* clear H0. clear H6. clear H8. *) + + (* unfold check_address_parameter_signed in *; *) + (* unfold check_address_parameter_unsigned in *; crush. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) + (* (Integers.Ptrofs.of_int *) + (* (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *) + (* (Integers.Int.repr z0)))) as OFFSET. *) + + (* (** Modular preservation proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) + (* { rewrite HeqOFFSET. *) + (* apply PtrofsExtra.add_mod; crush; try lia. *) + (* rewrite Integers.Ptrofs.unsigned_repr_eq. *) + (* rewrite <- Zmod_div_mod; crush. *) + (* apply PtrofsExtra.of_int_mod. *) + (* apply IntExtra.add_mod; crush. *) + (* apply IntExtra.mul_mod2; crush. *) + (* rewrite Integers.Int.unsigned_repr_eq. *) + (* rewrite <- Zmod_div_mod; crush. *) + (* rewrite Integers.Int.unsigned_repr_eq. *) + (* rewrite <- Zmod_div_mod; crush. } *) + + (* (** Write bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET destruct x eqn:EQ end; try reflexivity. *) + (* assert (Mem.valid_access m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) Writable). *) + (* { pose proof H1. eapply Mem.store_valid_access_2 in H0. *) + (* exact H0. eapply Mem.store_valid_access_3. eassumption. } *) + (* pose proof (Mem.valid_access_store m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) v). *) + (* apply X in H0. invert H0. congruence. *) + + (* + invert MARR. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + (* rewrite ARCHI in H0. crush. *) + + (* unfold check_address_parameter_unsigned in *; *) + (* unfold check_address_parameter_signed in *; crush. *) + + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* rewrite ZERO in H1. clear ZERO. *) + (* rewrite Integers.Ptrofs.add_zero_l in H1. *) + + (* remember i0 as OFFSET. *) + + (* (** Modular preservation proof *) *) + (* rename H0 into MOD_PRESERVE. *) + + (* (** Write bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET destruct x eqn:EQ end; try reflexivity. *) + (* assert (Mem.valid_access m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) Writable). *) + (* { pose proof H1. eapply Mem.store_valid_access_2 in H0. *) + (* exact H0. eapply Mem.store_valid_access_3. eassumption. } *) + (* pose proof (Mem.valid_access_store m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) v). *) + (* apply X in H0. invert H0. congruence. *) + (* Admitted. *) + (* Hint Resolve transl_istore_correct : htlproof. *) + + (* Lemma transl_icond_correct: *) + (* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) + (* (rs : Registers.Regmap.t Values.val) (m : mem) (cond : Op.condition) (args : list Registers.reg) *) + (* (ifso ifnot : RTL.node) (b : bool) (pc' : RTL.node), *) + (* (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) -> *) + (* Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> *) + (* pc' = (if b then ifso else ifnot) -> *) + (* forall R1 : HTL.state, *) + (* match_states (RTL.State s f sp pc rs m) R1 -> *) + (* exists R2 : HTL.state, *) + (* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *) + (* Proof. *) + (* intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE. *) + (* inv_state. *) + + (* eexists. split. apply Smallstep.plus_one. *) + (* eapply HTL.step_module; eauto. *) + (* apply assumption_32bit. *) + (* eapply Verilog.stmnt_runp_Vnonblock_reg with *) + (* (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). *) + (* constructor. *) + + (* simpl. *) + (* destruct b. *) + (* eapply Verilog.erun_Vternary_true. *) + (* eapply eval_cond_correct; eauto. *) + (* constructor. *) + (* apply boolToValue_ValueToBool. *) + (* eapply Verilog.erun_Vternary_false. *) + (* eapply eval_cond_correct; eauto. *) + (* constructor. *) + (* apply boolToValue_ValueToBool. *) + (* constructor. *) + + (* big_tac. *) + + (* invert MARR. *) + (* destruct b; rewrite assumption_32bit; big_tac. *) + + (* Unshelve. *) + (* constructor. *) + (* Qed. *) + (* Hint Resolve transl_icond_correct : htlproof. *) + + (* Lemma transl_ijumptable_correct: *) + (* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) + (* (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node) *) + (* (n : Integers.Int.int) (pc' : RTL.node), *) + (* (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) -> *) + (* Registers.Regmap.get arg rs = Values.Vint n -> *) + (* list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> *) + (* forall R1 : HTL.state, *) + (* match_states (RTL.State s f sp pc rs m) R1 -> *) + (* exists R2 : HTL.state, *) + (* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *) + (* Proof. *) + (* intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. *) + (* Admitted. *) + (* Hint Resolve transl_ijumptable_correct : htlproof. *) + + (* Lemma transl_ireturn_correct: *) + (* forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) *) + (* (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) *) + (* (m' : mem), *) + (* (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> *) + (* Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> *) + (* forall R1 : HTL.state, *) + (* match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> *) + (* exists R2 : HTL.state, *) + (* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *) + (* match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. *) + (* Proof. *) + (* intros s f stk pc rs m or m' H H0 R1 MSTATE. *) + (* inv_state. *) + + (* - econstructor. split. *) + (* eapply Smallstep.plus_two. *) + + (* eapply HTL.step_module; eauto. *) + (* apply assumption_32bit. *) + (* constructor. *) + (* econstructor; simpl; trivial. *) + (* econstructor; simpl; trivial. *) + (* constructor. *) + (* econstructor; simpl; trivial. *) + (* constructor. *) + + (* constructor. constructor. *) + + (* unfold state_st_wf in WF; big_tac; eauto. *) + + (* apply HTL.step_finish. *) + (* unfold Verilog.merge_regs. *) + (* unfold_merge; simpl. *) + (* rewrite AssocMap.gso. *) + (* apply AssocMap.gss. lia. *) + (* apply AssocMap.gss. *) + (* rewrite Events.E0_left. reflexivity. *) + + (* constructor; auto. *) + (* constructor. *) + + (* (* FIXME: Duplication *) *) + (* - econstructor. split. *) + (* eapply Smallstep.plus_two. *) + (* eapply HTL.step_module; eauto. *) + (* apply assumption_32bit. *) + (* constructor. *) + (* econstructor; simpl; trivial. *) + (* econstructor; simpl; trivial. *) + (* constructor. constructor. constructor. *) + (* constructor. constructor. constructor. *) + + (* unfold state_st_wf in WF; big_tac; eauto. *) + + (* apply HTL.step_finish. *) + (* unfold Verilog.merge_regs. *) + (* unfold_merge. *) + (* rewrite AssocMap.gso. *) + (* apply AssocMap.gss. simpl; lia. *) + (* apply AssocMap.gss. *) + (* rewrite Events.E0_left. trivial. *) + + (* constructor; auto. *) + + (* simpl. inversion MASSOC. subst. *) + (* unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. *) + (* apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. *) + (* assert (HPle : Ple r (RTL.max_reg_function f)). *) + (* eapply RTL.max_reg_function_use. eassumption. simpl; auto. *) + (* apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *) + + (* Unshelve. *) + (* all: constructor. *) + (* Qed. *) + (* Hint Resolve transl_ireturn_correct : htlproof. *) + + (* Lemma transl_callstate_correct: *) + (* forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) *) + (* (m : mem) (m' : Mem.mem') (stk : Values.block), *) + (* Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> *) + (* forall R1 : HTL.state, *) + (* match_states (RTL.Callstate s (AST.Internal f) args m) R1 -> *) + (* exists R2 : HTL.state, *) + (* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *) + (* match_states *) + (* (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) *) + (* (RTL.init_regs args (RTL.fn_params f)) m') R2. *) + (* Proof. *) + (* intros s f args m m' stk H R1 MSTATE. *) + + (* inversion MSTATE; subst. inversion TF; subst. *) + (* econstructor. split. apply Smallstep.plus_one. *) + (* eapply HTL.step_call. crush. *) + + (* apply match_state with (sp' := stk); eauto. *) + + (* all: big_tac. *) + + (* apply regs_lessdef_add_greater. *) + (* unfold Plt; lia. *) + (* apply init_reg_assoc_empty. *) + + (* constructor. *) + + (* destruct (Mem.load AST.Mint32 m' stk *) + (* (Integers.Ptrofs.unsigned (Integers.Ptrofs.add *) + (* Integers.Ptrofs.zero *) + (* (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. *) + (* pose proof Mem.load_alloc_same as LOAD_ALLOC. *) + (* pose proof H as ALLOC. *) + (* eapply LOAD_ALLOC in ALLOC. *) + (* 2: { exact LOAD. } *) + (* ptrofs. rewrite LOAD. *) + (* rewrite ALLOC. *) + (* repeat constructor. *) + + (* ptrofs. rewrite LOAD. *) + (* repeat constructor. *) + + (* unfold reg_stack_based_pointers. intros. *) + (* unfold RTL.init_regs; crush. *) + (* destruct (RTL.fn_params f); *) + (* rewrite Registers.Regmap.gi; constructor. *) + + (* unfold arr_stack_based_pointers. intros. *) + (* crush. *) + (* destruct (Mem.load AST.Mint32 m' stk *) + (* (Integers.Ptrofs.unsigned (Integers.Ptrofs.add *) + (* Integers.Ptrofs.zero *) + (* (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. *) + (* pose proof Mem.load_alloc_same as LOAD_ALLOC. *) + (* pose proof H as ALLOC. *) + (* eapply LOAD_ALLOC in ALLOC. *) + (* 2: { exact LOAD. } *) + (* rewrite ALLOC. *) + (* repeat constructor. *) + (* constructor. *) + + (* Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *) *) + (* Transparent Mem.load. *) + (* Transparent Mem.store. *) + (* unfold stack_bounds. *) + (* split. *) + + (* unfold Mem.alloc in H. *) + (* invert H. *) + (* crush. *) + (* unfold Mem.load. *) + (* intros. *) + (* match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. *) + (* invert v0. unfold Mem.range_perm in H4. *) + (* unfold Mem.perm in H4. crush. *) + (* unfold Mem.perm_order' in H4. *) + (* small_tac. *) + (* exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. *) + (* rewrite Maps.PMap.gss in H8. *) + (* match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. *) + (* crush. *) + (* apply proj_sumbool_true in H10. lia. *) + + (* unfold Mem.alloc in H. *) + (* invert H. *) + (* crush. *) + (* unfold Mem.store. *) + (* intros. *) + (* match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. *) + (* invert v0. unfold Mem.range_perm in H4. *) + (* unfold Mem.perm in H4. crush. *) + (* unfold Mem.perm_order' in H4. *) + (* small_tac. *) + (* exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. *) + (* rewrite Maps.PMap.gss in H8. *) + (* match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. *) + (* crush. *) + (* apply proj_sumbool_true in H10. lia. *) + (* Opaque Mem.alloc. *) + (* Opaque Mem.load. *) + (* Opaque Mem.store. *) + (* Qed. *) + (* Hint Resolve transl_callstate_correct : htlproof. *) + + (* Lemma transl_returnstate_correct: *) + (* forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) *) + (* (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) *) + (* (R1 : HTL.state), *) + (* match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> *) + (* exists R2 : HTL.state, *) + (* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *) + (* match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. *) + (* Proof. *) + (* intros res0 f sp pc rs s vres m R1 MSTATE. *) + (* inversion MSTATE. inversion MF. *) + (* Qed. *) + (* Hint Resolve transl_returnstate_correct : htlproof. *) + + (* Lemma option_inv : *) + (* forall A x y, *) + (* @Some A x = Some y -> x = y. *) + (* Proof. intros. inversion H. trivial. Qed. *) + + (* Lemma main_tprog_internal : *) + (* forall b, *) + (* Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b -> *) + (* exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f). *) + (* Proof. *) + (* intros. *) + (* destruct TRANSL. unfold main_is_internal in H1. *) + (* repeat (unfold_match H1). replace b with b0. *) + (* exploit function_ptr_translated; eauto. intros [tf [A B]]. *) + (* unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B. *) + (* unfold_match B. inv B. econstructor. apply A. *) + + (* apply option_inv. rewrite <- Heqo. rewrite <- H. *) + (* rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). *) + (* trivial. symmetry; eapply Linking.match_program_main; eauto. *) + (* Qed. *) + + (* Lemma transl_initial_states : *) + (* forall s1 : Smallstep.state (RTL.semantics prog), *) + (* Smallstep.initial_state (RTL.semantics prog) s1 -> *) + (* exists s2 : Smallstep.state (HTL.semantics tprog), *) + (* Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2. *) + (* Proof. *) + (* induction 1. *) + (* destruct TRANSL. unfold main_is_internal in H4. *) + (* repeat (unfold_match H4). *) + (* assert (f = AST.Internal f1). apply option_inv. *) + (* rewrite <- Heqo0. rewrite <- H1. replace b with b0. *) + (* auto. apply option_inv. rewrite <- H0. rewrite <- Heqo. *) + (* trivial. *) + (* exploit function_ptr_translated; eauto. *) + (* intros [tf [A B]]. *) + (* unfold transl_fundef, Errors.bind in B. *) + (* unfold AST.transf_partial_fundef, Errors.bind in B. *) + (* repeat (unfold_match B). inversion B. subst. *) + (* exploit main_tprog_internal; eauto; intros. *) + (* rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). *) + (* apply Heqo. symmetry; eapply Linking.match_program_main; eauto. *) + (* inversion H5. *) + (* econstructor; split. econstructor. *) + (* apply (Genv.init_mem_transf_partial TRANSL'); eauto. *) + (* replace (AST.prog_main tprog) with (AST.prog_main prog). *) + (* rewrite symbols_preserved; eauto. *) + (* symmetry; eapply Linking.match_program_main; eauto. *) + (* apply H6. *) + + (* constructor. *) + (* apply transl_module_correct. *) + (* assert (Some (AST.Internal x) = Some (AST.Internal m)). *) + (* replace (AST.fundef HTL.module) with (HTL.fundef). *) + (* rewrite <- H6. setoid_rewrite <- A. trivial. *) + (* trivial. inv H7. assumption. *) + (* Qed. *) + (* Hint Resolve transl_initial_states : htlproof. *) + + (* Lemma transl_final_states : *) + (* forall (s1 : Smallstep.state (RTL.semantics prog)) *) + (* (s2 : Smallstep.state (HTL.semantics tprog)) *) + (* (r : Integers.Int.int), *) + (* match_states s1 s2 -> *) + (* Smallstep.final_state (RTL.semantics prog) s1 r -> *) + (* Smallstep.final_state (HTL.semantics tprog) s2 r. *) + (* Proof. *) + (* intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity. *) + (* Qed. *) + (* Hint Resolve transl_final_states : htlproof. *) + + (* Theorem transl_step_correct: *) + (* forall (S1 : RTL.state) t S2, *) + (* RTL.step ge S1 t S2 -> *) + (* forall (R1 : HTL.state), *) + (* match_states S1 R1 -> *) + (* exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. *) + (* Proof. *) + (* induction 1; eauto with htlproof; (intros; inv_state). *) + (* Qed. *) + (* Hint Resolve transl_step_correct : htlproof. *) + +(* Theorem transf_program_correct: *) +(* Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). *) +(* Proof. *) +(* Admitted. *) +(* (* eapply Smallstep.forward_simulation_plus; eauto with htlproof. *) *) +(* (* apply senv_preserved. *) *) +(* (* Qed. *) *) + +(* End CORRECTNESS. *) diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index a9626c4..4662cf4 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -148,462 +148,462 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)). Hint Constructors tr_instr : htlspec. -Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) - (fin rtrn st stk : reg) : Prop := - tr_code_intro : - forall s t, - c!pc = Some i -> - stmnts!pc = Some s -> - trans!pc = Some t -> - tr_instr fin rtrn st stk i s t -> - tr_code c pc i stmnts trans fin rtrn st stk. -Hint Constructors tr_code : htlspec. - -Inductive tr_module (f : RTL.function) : module -> Prop := - tr_module_intro : - forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, - m = (mkmodule f.(RTL.fn_params) - data - control - f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> - (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> - tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> - stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> - Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> - 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> - st = ((RTL.max_reg_function f) + 1)%positive -> - fin = ((RTL.max_reg_function f) + 2)%positive -> - rtrn = ((RTL.max_reg_function f) + 3)%positive -> - stk = ((RTL.max_reg_function f) + 4)%positive -> - start = ((RTL.max_reg_function f) + 5)%positive -> - rst = ((RTL.max_reg_function f) + 6)%positive -> - clk = ((RTL.max_reg_function f) + 7)%positive -> - tr_module f m. -Hint Constructors tr_module : htlspec. - -Lemma create_reg_datapath_trans : - forall sz s s' x i iop, - create_reg iop sz s = OK x s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_datapath_trans : htlspec. - -Lemma create_reg_controllogic_trans : - forall sz s s' x i iop, - create_reg iop sz s = OK x s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_controllogic_trans : htlspec. - -Lemma declare_reg_datapath_trans : - forall sz s s' x i iop r, - declare_reg iop r sz s = OK x s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_datapath_trans : htlspec. - -Lemma declare_reg_controllogic_trans : - forall sz s s' x i iop r, - declare_reg iop r sz s = OK x s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_controllogic_trans : htlspec. - -Lemma declare_reg_freshreg_trans : - forall sz s s' x i iop r, - declare_reg iop r sz s = OK x s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. inversion 1; auto. Qed. -Hint Resolve declare_reg_freshreg_trans : htlspec. - -Lemma create_arr_datapath_trans : - forall sz ln s s' x i iop, - create_arr iop sz ln s = OK x s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_arr_datapath_trans : htlspec. - -Lemma create_arr_controllogic_trans : - forall sz ln s s' x i iop, - create_arr iop sz ln s = OK x s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_arr_controllogic_trans : htlspec. - -Lemma get_refl_x : - forall s s' x i, - get s = OK x s' i -> - s = x. -Proof. inversion 1. trivial. Qed. -Hint Resolve get_refl_x : htlspec. - -Lemma get_refl_s : - forall s s' x i, - get s = OK x s' i -> - s = s'. -Proof. inversion 1. trivial. Qed. -Hint Resolve get_refl_s : htlspec. - -Ltac inv_incr := - repeat match goal with - | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); eapply create_reg_datapath_trans in H; - eapply create_reg_controllogic_trans in H1 - | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); eapply create_arr_datapath_trans in H; - eapply create_arr_controllogic_trans in H1 - | [ H: get ?s = OK _ _ _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; - subst - | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H - | [ H: st_incr _ _ |- _ ] => destruct st_incr - end. - -Lemma collect_controllogic_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_datapath_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_freshreg_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_declare_controllogic_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. - intros. eapply collect_controllogic_trans; try eassumption. - intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. -Qed. - -Lemma collect_declare_datapath_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. - intros. eapply collect_datapath_trans; try eassumption. - intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. -Qed. - -Lemma collect_declare_freshreg_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. eapply collect_freshreg_trans; try eassumption. - inversion 1. auto. -Qed. - -Ltac unfold_match H := - match type of H with - | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate - end. - -Lemma translate_eff_addressing_freshreg_trans : - forall op args s r s' i, - translate_eff_addressing op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. - -Lemma translate_comparison_freshreg_trans : - forall op args s r s' i, - translate_comparison op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparison_freshreg_trans : htlspec. - -Lemma translate_comparison_imm_freshreg_trans : - forall op args s r s' i n, - translate_comparison_imm op args n s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. - -Lemma translate_condition_freshreg_trans : - forall op args s r s' i, - translate_condition op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. -Qed. -Hint Resolve translate_condition_freshreg_trans : htlspec. - -Lemma translate_instr_freshreg_trans : - forall op args s r s' i, - translate_instr op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. - monadInv H1. eauto with htlspec. -Qed. -Hint Resolve translate_instr_freshreg_trans : htlspec. - -Lemma translate_arr_access_freshreg_trans : - forall mem addr args st s r s' i, - translate_arr_access mem addr args st s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. -Qed. -Hint Resolve translate_arr_access_freshreg_trans : htlspec. - -Lemma add_instr_freshreg_trans : - forall n n' st s r s' i, - add_instr n n' st s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_instr_freshreg_trans : htlspec. - -Lemma add_branch_instr_freshreg_trans : - forall n n0 n1 e s r s' i, - add_branch_instr e n n0 n1 s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_branch_instr_freshreg_trans : htlspec. - -Lemma add_node_skip_freshreg_trans : - forall n1 n2 s r s' i, - add_node_skip n1 n2 s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_node_skip_freshreg_trans : htlspec. - -Lemma add_instr_skip_freshreg_trans : - forall n1 n2 s r s' i, - add_instr_skip n1 n2 s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_instr_skip_freshreg_trans : htlspec. - -Lemma transf_instr_freshreg_trans : - forall fin ret st instr s v s' i, - transf_instr fin ret st instr s = OK v s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. destruct instr eqn:?. subst. unfold transf_instr in H. - destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. - - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. - apply declare_reg_freshreg_trans in EQ1. congruence. - - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. - apply declare_reg_freshreg_trans in EQ1. congruence. - - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. - - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. - congruence. - - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. -Qed. -Hint Resolve transf_instr_freshreg_trans : htlspec. - -Lemma collect_trans_instr_freshreg_trans : - forall fin ret st l s s' i, - HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. eapply collect_freshreg_trans; try eassumption. - eauto with htlspec. -Qed. - -Ltac rewrite_states := - match goal with - | [ H: ?x ?s = ?x ?s' |- _ ] => - let c1 := fresh "c" in - let c2 := fresh "c" in - remember (?x ?s) as c1; remember (?x ?s') as c2; try subst - end. - -Ltac inv_add_instr' H := - match type of H with - | ?f _ _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H - end; repeat unfold_match H; inversion H. - -Ltac inv_add_instr := - lazymatch goal with - | H: context[add_instr_skip _ _ _] |- _ => - inv_add_instr' H - | H: context[add_instr_skip _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_instr _ _ _ _] |- _ => - inv_add_instr' H - | H: context[add_instr _ _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_branch_instr _ _ _ _ _] |- _ => - inv_add_instr' H - | H: context[add_branch_instr _ _ _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_node_skip _ _ _] |- _ => - inv_add_instr' H - | H: context[add_node_skip _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - end. - -Ltac destruct_optional := - match goal with H: option ?r |- _ => destruct H end. - -Lemma iter_expand_instr_spec : - forall l fin rtrn stack s s' i x c, - HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> - list_norepet (List.map fst l) -> - (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> - (forall pc instr, In (pc, instr) l -> - c!pc = Some instr -> - tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). -Proof. - induction l; simpl; intros; try contradiction. - destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. - destruct (peq pc pc1). - - subst. - destruct instr1 eqn:?; try discriminate; - try destruct_optional; inv_add_instr; econstructor; try assumption. - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. - eapply in_map with (f := fst) in H9. contradiction. - - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. - econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. - - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. - econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct H2. - * inversion H2. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H2. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct H2. - * inversion H2. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H2. contradiction. - - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. - * inversion H14. constructor. congruence. - * apply in_map with (f := fst) in H14. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. - * inversion H9. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H9. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. - * inversion H9. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H9. contradiction. - - - eapply IHl. apply EQ0. assumption. - destruct H2. inversion H2. subst. contradiction. - intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. - destruct H2. inv H2. contradiction. assumption. assumption. -Qed. -Hint Resolve iter_expand_instr_spec : htlspec. - -Lemma create_arr_inv : forall w x y z a b c d, - create_arr w x y z = OK (a, b) c d -> - y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). -Proof. - inversion 1; split; auto. -Qed. - -Lemma create_reg_inv : forall a b s r s' i, - create_reg a b s = OK r s' i -> - r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). -Proof. - inversion 1; auto. -Qed. - -Theorem transl_module_correct : - forall f m, - transl_module f = Errors.OK m -> tr_module f m. -Proof. - intros until m. - unfold transl_module. - unfold run_mon. - destruct (transf_module f (max_state f)) eqn:?; try discriminate. - intros. inv H. - inversion s; subst. - - unfold transf_module in *. - unfold stack_correct in *. - destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; - destruct (RTL.fn_stacksize f *) +(* stmnts!pc = Some s -> *) +(* trans!pc = Some t -> *) +(* tr_instr fin rtrn st stk i s t -> *) +(* tr_code c pc i stmnts trans fin rtrn st stk. *) +(* Hint Constructors tr_code : htlspec. *) + +(* Inductive tr_module (f : RTL.function) : module -> Prop := *) +(* tr_module_intro : *) +(* forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, *) +(* m = (mkmodule f.(RTL.fn_params) *) +(* data *) +(* control *) +(* f.(RTL.fn_entrypoint) *) +(* st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> *) +(* (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> *) +(* tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> *) +(* stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> *) +(* Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> *) +(* 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> *) +(* st = ((RTL.max_reg_function f) + 1)%positive -> *) +(* fin = ((RTL.max_reg_function f) + 2)%positive -> *) +(* rtrn = ((RTL.max_reg_function f) + 3)%positive -> *) +(* stk = ((RTL.max_reg_function f) + 4)%positive -> *) +(* start = ((RTL.max_reg_function f) + 5)%positive -> *) +(* rst = ((RTL.max_reg_function f) + 6)%positive -> *) +(* clk = ((RTL.max_reg_function f) + 7)%positive -> *) +(* tr_module f m. *) +(* Hint Constructors tr_module : htlspec. *) + +(* Lemma create_reg_datapath_trans : *) +(* forall sz s s' x i iop, *) +(* create_reg iop sz s = OK x s' i -> *) +(* s.(st_datapath) = s'.(st_datapath). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_reg_datapath_trans : htlspec. *) + +(* Lemma create_reg_controllogic_trans : *) +(* forall sz s s' x i iop, *) +(* create_reg iop sz s = OK x s' i -> *) +(* s.(st_controllogic) = s'.(st_controllogic). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_reg_controllogic_trans : htlspec. *) + +(* Lemma declare_reg_datapath_trans : *) +(* forall sz s s' x i iop r, *) +(* declare_reg iop r sz s = OK x s' i -> *) +(* s.(st_datapath) = s'.(st_datapath). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_reg_datapath_trans : htlspec. *) + +(* Lemma declare_reg_controllogic_trans : *) +(* forall sz s s' x i iop r, *) +(* declare_reg iop r sz s = OK x s' i -> *) +(* s.(st_controllogic) = s'.(st_controllogic). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_reg_controllogic_trans : htlspec. *) + +(* Lemma declare_reg_freshreg_trans : *) +(* forall sz s s' x i iop r, *) +(* declare_reg iop r sz s = OK x s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. inversion 1; auto. Qed. *) +(* Hint Resolve declare_reg_freshreg_trans : htlspec. *) + +(* Lemma create_arr_datapath_trans : *) +(* forall sz ln s s' x i iop, *) +(* create_arr iop sz ln s = OK x s' i -> *) +(* s.(st_datapath) = s'.(st_datapath). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_arr_datapath_trans : htlspec. *) + +(* Lemma create_arr_controllogic_trans : *) +(* forall sz ln s s' x i iop, *) +(* create_arr iop sz ln s = OK x s' i -> *) +(* s.(st_controllogic) = s'.(st_controllogic). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_arr_controllogic_trans : htlspec. *) + +(* Lemma get_refl_x : *) +(* forall s s' x i, *) +(* get s = OK x s' i -> *) +(* s = x. *) +(* Proof. inversion 1. trivial. Qed. *) +(* Hint Resolve get_refl_x : htlspec. *) + +(* Lemma get_refl_s : *) +(* forall s s' x i, *) +(* get s = OK x s' i -> *) +(* s = s'. *) +(* Proof. inversion 1. trivial. Qed. *) +(* Hint Resolve get_refl_s : htlspec. *) + +(* Ltac inv_incr := *) +(* repeat match goal with *) +(* | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => *) +(* let H1 := fresh "H" in *) +(* assert (H1 := H); eapply create_reg_datapath_trans in H; *) +(* eapply create_reg_controllogic_trans in H1 *) +(* | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => *) +(* let H1 := fresh "H" in *) +(* assert (H1 := H); eapply create_arr_datapath_trans in H; *) +(* eapply create_arr_controllogic_trans in H1 *) +(* | [ H: get ?s = OK _ _ _ |- _ ] => *) +(* let H1 := fresh "H" in *) +(* assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; *) +(* subst *) +(* | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H *) +(* | [ H: st_incr _ _ |- _ ] => destruct st_incr *) +(* end. *) + +(* Lemma collect_controllogic_trans : *) +(* forall A f l cs cs' ci, *) +(* (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> *) +(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). *) +(* Proof. *) +(* induction l; intros; monadInv H0. *) +(* - trivial. *) +(* - apply H in EQ. rewrite EQ. eauto. *) +(* Qed. *) + +(* Lemma collect_datapath_trans : *) +(* forall A f l cs cs' ci, *) +(* (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> *) +(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). *) +(* Proof. *) +(* induction l; intros; monadInv H0. *) +(* - trivial. *) +(* - apply H in EQ. rewrite EQ. eauto. *) +(* Qed. *) + +(* Lemma collect_freshreg_trans : *) +(* forall A f l cs cs' ci, *) +(* (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> *) +(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). *) +(* Proof. *) +(* induction l; intros; monadInv H0. *) +(* - trivial. *) +(* - apply H in EQ. rewrite EQ. eauto. *) +(* Qed. *) + +(* Lemma collect_declare_controllogic_trans : *) +(* forall io n l s s' i, *) +(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) +(* s.(st_controllogic) = s'.(st_controllogic). *) +(* Proof. *) +(* intros. eapply collect_controllogic_trans; try eassumption. *) +(* intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. *) +(* Qed. *) + +(* Lemma collect_declare_datapath_trans : *) +(* forall io n l s s' i, *) +(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) +(* s.(st_datapath) = s'.(st_datapath). *) +(* Proof. *) +(* intros. eapply collect_datapath_trans; try eassumption. *) +(* intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. *) +(* Qed. *) + +(* Lemma collect_declare_freshreg_trans : *) +(* forall io n l s s' i, *) +(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* intros. eapply collect_freshreg_trans; try eassumption. *) +(* inversion 1. auto. *) +(* Qed. *) + +(* Ltac unfold_match H := *) +(* match type of H with *) +(* | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate *) +(* end. *) + +(* Lemma translate_eff_addressing_freshreg_trans : *) +(* forall op args s r s' i, *) +(* translate_eff_addressing op args s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) +(* Qed. *) +(* Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. *) + +(* Lemma translate_comparison_freshreg_trans : *) +(* forall op args s r s' i, *) +(* translate_comparison op args s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) +(* Qed. *) +(* Hint Resolve translate_comparison_freshreg_trans : htlspec. *) + +(* Lemma translate_comparison_imm_freshreg_trans : *) +(* forall op args s r s' i n, *) +(* translate_comparison_imm op args n s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) +(* Qed. *) +(* Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. *) + +(* Lemma translate_condition_freshreg_trans : *) +(* forall op args s r s' i, *) +(* translate_condition op args s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *) +(* Qed. *) +(* Hint Resolve translate_condition_freshreg_trans : htlspec. *) + +(* Lemma translate_instr_freshreg_trans : *) +(* forall op args s r s' i, *) +(* translate_instr op args s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *) +(* monadInv H1. eauto with htlspec. *) +(* Qed. *) +(* Hint Resolve translate_instr_freshreg_trans : htlspec. *) + +(* Lemma translate_arr_access_freshreg_trans : *) +(* forall mem addr args st s r s' i, *) +(* translate_arr_access mem addr args st s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. *) +(* Qed. *) +(* Hint Resolve translate_arr_access_freshreg_trans : htlspec. *) + +(* Lemma add_instr_freshreg_trans : *) +(* forall n n' st s r s' i, *) +(* add_instr n n' st s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. *) +(* Hint Resolve add_instr_freshreg_trans : htlspec. *) + +(* Lemma add_branch_instr_freshreg_trans : *) +(* forall n n0 n1 e s r s' i, *) +(* add_branch_instr e n n0 n1 s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. *) +(* Hint Resolve add_branch_instr_freshreg_trans : htlspec. *) + +(* Lemma add_node_skip_freshreg_trans : *) +(* forall n1 n2 s r s' i, *) +(* add_node_skip n1 n2 s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. *) +(* Hint Resolve add_node_skip_freshreg_trans : htlspec. *) + +(* Lemma add_instr_skip_freshreg_trans : *) +(* forall n1 n2 s r s' i, *) +(* add_instr_skip n1 n2 s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. *) +(* Hint Resolve add_instr_skip_freshreg_trans : htlspec. *) + +(* Lemma transf_instr_freshreg_trans : *) +(* forall fin ret st instr s v s' i, *) +(* transf_instr fin ret st instr s = OK v s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* intros. destruct instr eqn:?. subst. unfold transf_instr in H. *) +(* destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. *) +(* - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. *) +(* apply declare_reg_freshreg_trans in EQ1. congruence. *) +(* - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. *) +(* apply declare_reg_freshreg_trans in EQ1. congruence. *) +(* - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. *) +(* - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. *) +(* congruence. *) +(* - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. *) +(* Qed. *) +(* Hint Resolve transf_instr_freshreg_trans : htlspec. *) + +(* Lemma collect_trans_instr_freshreg_trans : *) +(* forall fin ret st l s s' i, *) +(* HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* intros. eapply collect_freshreg_trans; try eassumption. *) +(* eauto with htlspec. *) +(* Qed. *) + +(* Ltac rewrite_states := *) +(* match goal with *) +(* | [ H: ?x ?s = ?x ?s' |- _ ] => *) +(* let c1 := fresh "c" in *) +(* let c2 := fresh "c" in *) +(* remember (?x ?s) as c1; remember (?x ?s') as c2; try subst *) +(* end. *) + +(* Ltac inv_add_instr' H := *) +(* match type of H with *) +(* | ?f _ _ _ = OK _ _ _ => unfold f in H *) +(* | ?f _ _ _ _ = OK _ _ _ => unfold f in H *) +(* | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H *) +(* end; repeat unfold_match H; inversion H. *) + +(* Ltac inv_add_instr := *) +(* lazymatch goal with *) +(* | H: context[add_instr_skip _ _ _] |- _ => *) +(* inv_add_instr' H *) +(* | H: context[add_instr_skip _ _] |- _ => *) +(* monadInv H; inv_incr; inv_add_instr *) +(* | H: context[add_instr _ _ _ _] |- _ => *) +(* inv_add_instr' H *) +(* | H: context[add_instr _ _ _] |- _ => *) +(* monadInv H; inv_incr; inv_add_instr *) +(* | H: context[add_branch_instr _ _ _ _ _] |- _ => *) +(* inv_add_instr' H *) +(* | H: context[add_branch_instr _ _ _ _] |- _ => *) +(* monadInv H; inv_incr; inv_add_instr *) +(* | H: context[add_node_skip _ _ _] |- _ => *) +(* inv_add_instr' H *) +(* | H: context[add_node_skip _ _] |- _ => *) +(* monadInv H; inv_incr; inv_add_instr *) +(* end. *) + +(* Ltac destruct_optional := *) +(* match goal with H: option ?r |- _ => destruct H end. *) + +(* Lemma iter_expand_instr_spec : *) +(* forall l fin rtrn stack s s' i x c, *) +(* HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> *) +(* list_norepet (List.map fst l) -> *) +(* (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> *) +(* (forall pc instr, In (pc, instr) l -> *) +(* c!pc = Some instr -> *) +(* tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). *) +(* Proof. *) +(* induction l; simpl; intros; try contradiction. *) +(* destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. *) +(* destruct (peq pc pc1). *) +(* - subst. *) +(* destruct instr1 eqn:?; try discriminate; *) +(* try destruct_optional; inv_add_instr; econstructor; try assumption. *) +(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. *) +(* eapply in_map with (f := fst) in H9. contradiction. *) + +(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. *) +(* econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. *) + +(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. *) +(* econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. *) + +(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct H2. *) +(* * inversion H2. *) +(* replace (st_st s2) with (st_st s0) by congruence. *) +(* eauto with htlspec. *) +(* * apply in_map with (f := fst) in H2. contradiction. *) + +(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct H2. *) +(* * inversion H2. *) +(* replace (st_st s2) with (st_st s0) by congruence. *) +(* eauto with htlspec. *) +(* * apply in_map with (f := fst) in H2. contradiction. *) + +(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + inversion H2. *) +(* * inversion H14. constructor. congruence. *) +(* * apply in_map with (f := fst) in H14. contradiction. *) + +(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + inversion H2. *) +(* * inversion H9. *) +(* replace (st_st s2) with (st_st s0) by congruence. *) +(* eauto with htlspec. *) +(* * apply in_map with (f := fst) in H9. contradiction. *) + +(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + inversion H2. *) +(* * inversion H9. *) +(* replace (st_st s2) with (st_st s0) by congruence. *) +(* eauto with htlspec. *) +(* * apply in_map with (f := fst) in H9. contradiction. *) + +(* - eapply IHl. apply EQ0. assumption. *) +(* destruct H2. inversion H2. subst. contradiction. *) +(* intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. *) +(* destruct H2. inv H2. contradiction. assumption. assumption. *) +(* Qed. *) +(* Hint Resolve iter_expand_instr_spec : htlspec. *) + +(* Lemma create_arr_inv : forall w x y z a b c d, *) +(* create_arr w x y z = OK (a, b) c d -> *) +(* y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). *) +(* Proof. *) +(* inversion 1; split; auto. *) +(* Qed. *) + +(* Lemma create_reg_inv : forall a b s r s' i, *) +(* create_reg a b s = OK r s' i -> *) +(* r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). *) +(* Proof. *) +(* inversion 1; auto. *) +(* Qed. *) + +(* Theorem transl_module_correct : *) +(* forall f m, *) +(* transl_module f = Errors.OK m -> tr_module f m. *) +(* Proof. *) +(* intros until m. *) +(* unfold transl_module. *) +(* unfold run_mon. *) +(* destruct (transf_module f (max_state f)) eqn:?; try discriminate. *) +(* intros. inv H. *) +(* inversion s; subst. *) + +(* unfold transf_module in *. *) +(* unfold stack_correct in *. *) +(* destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; *) +(* destruct (RTL.fn_stacksize f . *) -open Value +open ValueInt open Datatypes open Camlcoq open AST diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 5265c97..db78ad5 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -17,7 +17,7 @@ *) open Verilog -open Value +open ValueInt open Datatypes open Camlcoq @@ -70,11 +70,17 @@ let unop = function let register a = sprintf "reg_%d" (P.to_int a) -let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l)) +let literal l = sprintf "32'd%d" (Z.to_int (uvalueToZ l)) + +let byte n s = sprintf "reg_%d[%d:%d]" (P.to_int s) (7 + n * 8) (n * 8) let rec pprint_expr = function | Vlit l -> literal l | Vvar s -> register s + | Vvarb0 s -> byte 0 s + | Vvarb1 s -> byte 1 s + | Vvarb2 s -> byte 2 s + | Vvarb3 s -> byte 3 s | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"] | Vinputvar s -> register s | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index 62bf63f..5fd8fe9 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -18,8 +18,8 @@ val pprint_stmnt : int -> Verilog.stmnt -> string -val print_value : out_channel -> Value.value -> unit +val print_value : out_channel -> ValueInt.value -> unit val print_program : bool -> out_channel -> Verilog.program -> unit -val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit +val print_result : out_channel -> (BinNums.positive * ValueInt.value) list -> unit diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 064474a..921d9fd 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -29,7 +29,7 @@ Require Import Lia. Import ListNotations. -From coqup Require Import common.Coquplib common.Show verilog.ValueInt AssocMap Array. +From coqup Require Import common.Coquplib common.Show verilog.ValueInt IntegerExtra AssocMap Array. From compcert Require Events. From compcert Require Import Integers Errors Smallstep Globalenvs. @@ -154,9 +154,13 @@ Inductive unop : Type := (** ** Expressions *) Inductive expr : Type := -| Vlit : value -> expr -| Vvar : reg -> expr -| Vvari : reg -> expr -> expr +| Vlit : value -> expr (** literal *) +| Vvar : reg -> expr (** reg *) +| Vvarb0 : reg -> expr (** 1st byte projection of reg *) +| Vvarb1 : reg -> expr +| Vvarb2 : reg -> expr +| Vvarb3 : reg -> expr +| Vvari : reg -> expr -> expr (** array *) | Vinputvar : reg -> expr | Vbinop : binop -> expr -> expr -> expr | Vunop : unop -> expr -> expr @@ -340,6 +344,22 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop forall fext reg stack v r, reg#r = v -> expr_runp fext reg stack (Vvar r) v + | erun_Vvarb0 : + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvarb0 r) (IntExtra.ibyte0 v) + | erun_Vvarb1 : + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvarb1 r) (IntExtra.ibyte1 v) + | erun_Vvarb2 : + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvarb2 r) (IntExtra.ibyte2 v) + | erun_Vvarb3 : + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvarb3 r) (IntExtra.ibyte3 v) | erun_Vvari : forall fext reg stack v iexp i r, expr_runp fext reg stack iexp i -> @@ -429,6 +449,7 @@ Definition access_fext (f : fext) (r : reg) : res value := Inductive location : Type := | LocReg (_ : reg) +| LocRegB (_ : reg) (_ : nat) | LocArray (_ : reg) (_ : nat). Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop := @@ -775,6 +796,10 @@ Proof. repeat (try match goal with | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvarb0 _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvarb1 _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvarb2 _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvarb3 _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H -- cgit