diff --git a/src/coq/Semantics/InfiniteToFinite.v b/src/coq/Semantics/InfiniteToFinite.v index 7bd26861..3e990015 100644 --- a/src/coq/Semantics/InfiniteToFinite.v +++ b/src/coq/Semantics/InfiniteToFinite.v @@ -10371,6 +10371,11 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF exists (lift_MemState ms_fin_final). + assert (Heap_in_bounds ms_fin_final) as HIB_FINAL. + { + admit. (* TODO: Heap_in_bounds *) + } + split. 2: apply lift_MemState_refine_prop. @@ -10405,7 +10410,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF eapply ptr_in_memstate_heap_inf_fin in H; eauto. apply free_bytes_freed in H. eapply fin_inf_byte_not_allocated in H; eauto. - apply lift_MemState_refine_prop. + apply lift_MemState_refine_prop; auto. } { (* Big pointer, shouldn't be allocated. *) @@ -10425,7 +10430,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF { (* ptr in finite range *) split; intros ALLOC. - eapply fin_inf_byte_allocated; eauto. - apply lift_MemState_refine_prop. + apply lift_MemState_refine_prop; auto. apply free_non_block_bytes_preserved. + intros CONTRA. eapply ptr_in_memstate_heap_fin_inf in CONTRA; eauto. @@ -10435,7 +10440,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF + intros CONTRA. eapply ptr_in_memstate_heap_fin_inf in CONTRA; eauto. + eapply inf_fin_byte_allocated; eauto. - apply lift_MemState_refine_prop. + apply lift_MemState_refine_prop; auto. } { (* Big pointer, shouldn't be allocated. *) @@ -10446,7 +10451,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF - eapply inf_fin_byte_allocated_exists in ALLOC; eauto. destruct ALLOC as (?&?&?). rewrite CONV in H0; discriminate. - apply lift_MemState_refine_prop. + apply lift_MemState_refine_prop; auto. } } - intros ptr byte H. @@ -10460,8 +10465,8 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF eapply ptr_in_memstate_heap_fin_inf in CONTRA; eauto. } eapply fin_inf_read_byte_spec; eauto. - apply lift_MemState_refine_prop. - - pose proof (lift_MemState_refine_prop ms_fin_final) as MSR'. + apply lift_MemState_refine_prop; auto. + - pose proof (lift_MemState_refine_prop ms_fin_final HIB_FINAL) as MSR'. epose proof inf_fin_read_byte_spec MSR' CONV RBS as (byte_fin&RBS_FIN&BYTE_REF). eapply free_non_frame_bytes_read in RBS_FIN. 2: { @@ -10481,7 +10486,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF destruct ALLOC as (?&?&?&?&?). red in H2. rewrite CONV in H2; discriminate. - apply lift_MemState_refine_prop. + apply lift_MemState_refine_prop; auto. } } - clear - PTR_REF MSR free_block. @@ -10517,14 +10522,14 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF auto. } - (* Free operation invariants *) - clear - MSR free_invariants. + clear - HIB_FINAL MSR free_invariants. destruct free_invariants. split. + eapply fin_inf_preserve_allocation_ids; eauto. - apply lift_MemState_refine_prop. + apply lift_MemState_refine_prop; auto. + eapply fin_inf_frame_stack_preserved; eauto. - apply lift_MemState_refine_prop. - Qed. + apply lift_MemState_refine_prop; auto. +Admitted. Lemma handle_free_fin_inf : forall {ms_fin_start ms_fin_final ms_inf_start res_fin args_fin args_inf}, @@ -10586,6 +10591,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF { (* MA *) intros a_fin ms_fin_ma MEMCPY. eapply handle_memcpy_fin_inf; eauto. + admit. (* TODO: Heap_in_bounds *) } intros ms_inf0 ms_fin0 ms_fin'0 a_fin a_inf b_fin _ MSR' EQV. @@ -10648,6 +10654,107 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF (* Unknown intrinsic *) cbn in *; auto. contradiction. + Admitted. + + Lemma to_ubytes_fin_inf_helper : + forall {uv_fin uv_inf t sid bytes_fin start}, + DVC1.uvalue_refine_strict uv_inf uv_fin -> + map_monad + (fun n : N => + n' <- LLVMParams64BitIntptr.IP.from_Z (Z.of_N n);; + ret + (Memory64BitIntptr.MP.BYTE_IMPL.uvalue_sbyte uv_fin t + (LLVMParams64BitIntptr.Events.DV.UVALUE_IPTR n') sid)) + (Nseq start (N.to_nat (FiniteSizeof.FinSizeof.sizeof_dtyp t))) = + NoOom bytes_fin -> + map_monad + (fun n : N => + n' <- LLVMParamsBigIntptr.IP.from_Z (Z.of_N n);; + ret + (MemoryBigIntptr.MP.BYTE_IMPL.uvalue_sbyte uv_inf t + (LLVMParamsBigIntptr.Events.DV.UVALUE_IPTR n') sid)) + (Nseq start (N.to_nat (FiniteSizeof.FinSizeof.sizeof_dtyp t))) = NoOom (map lift_SByte bytes_fin). + Proof. + intros uv_fin uv_inf t sid bytes_fin start UV_REF UBYTES. + generalize dependent bytes_fin. + generalize dependent start. + induction (N.to_nat (FiniteSizeof.FinSizeof.sizeof_dtyp t)); + intros start bytes_fin UBYTES. + - cbn in *. + inv UBYTES. + cbn. + reflexivity. + - rewrite <- cons_Nseq. + rewrite <- cons_Nseq in UBYTES. + + rewrite map_monad_unfold. + rewrite map_monad_unfold in UBYTES. + + cbn. + cbn in UBYTES. + + break_match_hyp; inv UBYTES. + break_match_hyp; inv H0. + break_match_hyp; inv Heqo. + + apply IHn in Heqo0. + cbn in Heqo0. + rewrite Heqo0. + cbn. + unfold MemoryBigIntptr.MP.BYTE_IMPL.uvalue_sbyte. + erewrite <- fin_to_inf_uvalue_refine_strict'; eauto. + erewrite <- fin_to_inf_uvalue_refine_strict'; eauto. + + rewrite DVC1.uvalue_refine_strict_equation. + rewrite DVC1.uvalue_convert_strict_equation. + cbn. + + erewrite FinToInfIntptrConvertSafe.intptr_convert_safe; eauto. + cbn. + erewrite IP64Bit.from_Z_to_Z; eauto. + Qed. + + (* TODO: move this *) + Definition lift_SBytes := map lift_SByte. + + Lemma lift_SBytes_refine : + forall {bytes_fin}, + sbytes_refine (lift_SBytes bytes_fin) bytes_fin. + Proof. + induction bytes_fin; cbn. + - constructor. + - constructor. + apply sbyte_refine_lifted. + apply IHbytes_fin. + Qed. + + (* TODO: should we know that uv_inf / uv_fin has type t? + + I think this would have to be an assumption, in theory the front + end would guarantee this for stores with a syntactic check. + *) + Lemma to_ubytes_fin_inf : + forall {uv_fin uv_inf t sid bytes_fin}, + DVC1.uvalue_refine_strict uv_inf uv_fin -> + Memory64BitIntptr.MMEP.MMSP.MemByte.to_ubytes uv_fin t sid = NoOom bytes_fin -> + exists bytes_inf, + MemoryBigIntptr.MMEP.MMSP.MemByte.to_ubytes uv_inf t sid = NoOom bytes_inf /\ + sbytes_refine bytes_inf bytes_fin. + Proof. + intros uv_fin uv_inf t sid bytes_fin UV_REF UBYTES. + exists (map lift_SByte bytes_fin). + split. + 2: { + apply lift_SBytes_refine. + } + + unfold MemoryBigIntptr.MMEP.MMSP.MemByte.to_ubytes, + Memory64BitIntptr.MMEP.MMSP.MemByte.to_ubytes in *. + + unfold LLVMParams64BitIntptr.SIZEOF.sizeof_dtyp, + LLVMParamsBigIntptr.SIZEOF.sizeof_dtyp in *. + + eapply to_ubytes_fin_inf_helper; eauto. Qed. (* TODO: Prove this *) @@ -10665,7 +10772,95 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF MemState_refine_prop ms_inf_final ms_fin_final. Proof. intros ms_fin_start ms_fin_final ms_inf_start uv_fin uv_inf t bytes_fin MSR UV_REF SERIALIZE. - Admitted. + + rewrite Memory64BitIntptr.MMEP.MemSpec.MemHelpers.serialize_sbytes_equation in SERIALIZE. + rewrite MemoryBigIntptr.MMEP.MemSpec.MemHelpers.serialize_sbytes_equation. + + induction uv_inf. + - pose proof UV_REF as UV_REF'. + rewrite DVC1.uvalue_refine_strict_equation in UV_REF. + rewrite DVC1.uvalue_convert_strict_equation in UV_REF. + cbn in UV_REF. + move UV_REF after SERIALIZE. + break_match_hyp; inv UV_REF. + + eapply MemPropT_fin_inf_bind. + 4: apply SERIALIZE. + all: eauto. + + { (* MA: fresh_sid *) + intros a_fin ms_fin_ma FRESH. + eapply fresh_sid_fin_inf; eauto. + } + + intros ms_inf ms_fin ms_fin' a_fin a_inf b_fin SID MSR_SID UBYTES. + cbn in SID, UBYTES; subst. + + red in UBYTES. + break_match_hyp; inv UBYTES. + + + eapply to_ubytes_fin_inf in Heqo0; eauto. + destruct Heqo0 as (?&?&?). + exists x. exists ms_inf. + split; auto. + red. + rewrite H. + cbn. auto. + + + try + solve + [ rewrite DVC1.dvalue_refine_strict_equation in UV_REF; + first + [ apply dvalue_convert_strict_i1_inv in UV_REF + | apply dvalue_convert_strict_i8_inv in UV_REF + | apply dvalue_convert_strict_i32_inv in UV_REF + | apply dvalue_convert_strict_i64_inv in UV_REF + | apply dvalue_convert_strict_iptr_inv in UV_REF + | apply dvalue_convert_strict_addr_inv in UV_REF + | apply dvalue_convert_strict_double_inv in UV_REF + | apply dvalue_convert_strict_float_inv in UV_REF + | apply dvalue_convert_strict_poison_inv in UV_REF + | apply dvalue_convert_strict_oom_inv in UV_REF + | apply dvalue_convert_strict_none_inv in UV_REF + | apply dvalue_convert_strict_struct_inv in UV_REF + | apply dvalue_convert_strict_packed_struct_inv in UV_REF + | apply dvalue_convert_strict_array_inv in UV_REF + | apply dvalue_convert_strict_vector_inv in UV_REF + ]; + first + [ destruct ADDR_REF as (?&?&?); subst + | inv ADDR_REF + ] + ]. + + rewrite DVC1.uvalue_refine_strict_equation in UV_REF. + apply uvalue_convert_strict_addr_inv in UV_REF. + first + [ apply uvalue_convert_strict_i1_inv in UV_REF + | apply uvalue_convert_strict_i8_inv in UV_REF + | apply uvalue_convert_strict_i32_inv in UV_REF + | apply uvalue_convert_strict_i64_inv in UV_REF + | apply uvalue_convert_strict_iptr_inv in UV_REF + | apply uvalue_convert_strict_addr_inv in UV_REF + | apply uvalue_convert_strict_double_inv in UV_REF + | apply uvalue_convert_strict_float_inv in UV_REF + | apply uvalue_convert_strict_poison_inv in UV_REF + | apply uvalue_convert_strict_oom_inv in UV_REF + | apply uvalue_convert_strict_none_inv in UV_REF + | apply uvalue_convert_strict_struct_inv in UV_REF + | apply uvalue_convert_strict_packed_struct_inv in UV_REF + | apply uvalue_convert_strict_array_inv in UV_REF + | apply uvalue_convert_strict_vector_inv in UV_REF + ]; + first + [ destruct ADDR_REF as (?&?&?); subst + | inv ADDR_REF + ]. + + + Qed. Lemma handle_store_fin_inf : forall {t addr_fin addr_inf uv_fin uv_inf ms_fin_start ms_fin_final ms_inf_start res_fin},