From 39c336a3e507b9264cd80d1721b724dc5606de6d Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 18 Jun 2020 00:47:29 +0100 Subject: Fix up ILoad proof. --- src/translation/HTLgenproof.v | 153 ++++++++++++++++-------------------------- 1 file changed, 58 insertions(+), 95 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 80d936f..8a246f3 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -21,6 +21,8 @@ From compcert Require Import Globalenvs Memory. From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array. From coqup Require HTL Verilog. +Require Import Lia. + Local Open Scope assocmap. Hint Resolve Smallstep.forward_simulation_plus : htlproof. @@ -449,16 +451,6 @@ Section CORRECTNESS. (* assumption. *) admit. - Ltac invert x := inversion x; subst; clear x. - - Ltac clear_obvious := - repeat match goal with - | [ H : ex _ |- _ ] => invert H - | [ H : Some _ = Some _ |- _ ] => invert H - end. - - Ltac simplify := simpl in *; clear_obvious; simpl in *; try discriminate. - Ltac rt := repeat match goal with | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate @@ -473,8 +465,8 @@ Section CORRECTNESS. | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x end. - - - destruct c, chunk, addr, args; simplify; rt; simplify. + - (* FIXME: Should be able to use the spec to avoid destructing here. *) + destruct c, chunk, addr, args; simplify; rt; simplify. + admit. (* FIXME: Alignment *) + admit. @@ -486,104 +478,75 @@ Section CORRECTNESS. destruct (Archi.ptr64) eqn:ARCHI; simplify. rewrite ARCHI in H0. simplify. - (* Out of bounds reads are undefined behaviour. *) - assert (forall ptr v, f.(RTL.fn_stacksize) <= ptr -> - Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr)) = Some v -> - v = Values.Vundef) as INVALID_READ by admit. - - (* Case split on whether read is out of bounds. *) - destruct (RTL.fn_stacksize f <=? Integers.Ptrofs.unsigned i0) eqn:BOUND. - * assert (RTL.fn_stacksize f <= Integers.Ptrofs.unsigned i0) as OUT_OF_BOUNDS. { - apply Zle_bool_imp_le. assumption. - } - eapply INVALID_READ in OUT_OF_BOUNDS. - 2: { rewrite Integers.Ptrofs.repr_unsigned. eassumption. } - - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. simplify. - econstructor. econstructor. econstructor. econstructor. simplify. - - unfold Verilog.arr_assocmap_lookup. rewrite H3. - reflexivity. - - simplify. unfold_merge. apply AssocMap.gss. - - simplify. rewrite assumption_32bit. - constructor. - - unfold_merge. - apply regs_lessdef_add_greater. - apply greater_than_max_func. - - apply regs_lessdef_add_match. - rewrite OUT_OF_BOUNDS. - constructor. assumption. - assumption. + (** Here we are assuming that any stack read will be within the bounds + of the activation record. *) + assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit. + assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. - unfold state_st_wf. inversion 1. simplify. - unfold_merge. apply AssocMap.gss. - - assumption. - - econstructor; simplify; try reflexivity; eassumption. - - * assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as IN_BOUNDS. { - rewrite Z.leb_antisym in BOUND. - rewrite negb_false_iff in BOUND. - apply Zlt_is_lt_bool. assumption. - } + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. econstructor. simplify. - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. simplify. - econstructor. econstructor. econstructor. econstructor. simplify. + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H3. + f_equal. - unfold Verilog.arr_assocmap_lookup. rewrite H3. - reflexivity. + simplify. unfold Verilog.merge_regs. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. - simplify. unfold_merge. apply AssocMap.gss. + simplify. rewrite assumption_32bit. + constructor. - simplify. rewrite assumption_32bit. - constructor. + unfold Verilog.merge_regs. unfold_merge. + apply regs_lessdef_add_match. - unfold_merge. - apply regs_lessdef_add_greater. - apply greater_than_max_func. + (** Equality proof *) + admit. - apply regs_lessdef_add_match. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. assumption. - assert (exists ptr, (Z.to_nat ptr / 4)%nat = (valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned i0 / 4)))) - by admit. - simplify. rewrite <- H5. - specialize (H4 x). - assert (0 <= x < Z.of_nat (Z.to_nat (RTL.fn_stacksize f / 4))) by admit. - apply H4 in H0. - invert H0. - assert (Integers.Ptrofs.repr x = i0) by admit. - rewrite H0 in H6. - rewrite H1 in H6. - invert H6. - assumption. + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. - assert (Integers.Ptrofs.repr x = i0) by admit. - rewrite H0 in H7. - rewrite H1 in H7. - discriminate. + assumption. - assumption. + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H3. + reflexivity. - assumption. + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. - unfold state_st_wf. inversion 1. simplify. - unfold_merge. apply AssocMap.gss. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + congruence. - assumption. + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. - econstructor; simplify; try reflexivity; eassumption. + assumption. - destruct c, chunk, addr, args; simplify; rt; simplify. + admit. -- cgit