Commit 561a7cde authored by Dan Frumin's avatar Dan Frumin

Hackish treatment of pointer addition on the reified syntax

parent 6bafb34f
......@@ -138,11 +138,44 @@ Definition dbin_op_eval
| _, _ => dNone
end.
Definition dptr_plus_eval (E: known_locs) (dv1 dv2 : dval) : doption dval :=
match dv1,dv2 with
| dLocV (dLoc i), dLitV (dLitInt o) =>
(* DF: TODO: THIS MAY VERY BLOCK SIMPLIFICATION *)
(* TO PROPERLY HANDLE THIS CASE PLEASE DEEPLY EMBED THE NATURALS *)
match offset_of_val (LitV (LitInt o)) with
| None => dNone
| Some n =>
dSome (dLocV (dLocUnknown (cloc_add (dloc_interp E (dLoc i)) n)))
end
| dValUnknown _,dValUnknown _ =>
dUnknown (dValUnknown <$>
cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2))
| _,_ => dNone
end.
Lemma dptr_plus_eval_correct E dv1 dv2 w :
doption_interp (dptr_plus_eval E dv1 dv2) = Some w
cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2)
= Some (dval_interp E w).
Proof.
destruct dv1 as [?|??|[]|u1],dv2 as [[]|??|?|u2]; try naive_solver.
- cbn-[cbin_op_eval]. case_option_guard; inversion 1.
simplify_eq/=. repeat (case_option_guard; last omega).
simpl. repeat f_equal. rewrite Nat2Z.id.
(* TODO: WTF? *)
destruct (default (1%positive, 0%nat) (E !! n)) as [? ?] eqn:lol.
by rewrite lol.
- cbn-[cbin_op_eval].
destruct (cbin_op_eval PtrPlusOp u1 u2) as [w1|] eqn:Hw1;
intros; simplify_eq/=. done.
Qed.
Definition dcbin_op_eval (E: known_locs) (op : cbin_op) (dv1 dv2 : dval) : doption dval :=
match op with
| CBinOp op' => dbin_op_eval E op' dv1 dv2
| PtrPlusOp | PtrLtOp =>
| PtrPlusOp => dptr_plus_eval E dv1 dv2
| PtrLtOp =>
dUnknown (dValUnknown <$> cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
end.
......@@ -185,7 +218,7 @@ Lemma dcbin_op_eval_correct E op dv1 dv2 w :
Proof.
destruct op as [op'| |].
- apply dbin_op_eval_correct.
- cbn-[cbin_op_eval]. destruct (cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2)); naive_solver.
- apply dptr_plus_eval_correct.
- cbn-[cbin_op_eval]. destruct (cbin_op_eval PtrLtOp (dval_interp E dv1) (dval_interp E dv2)); naive_solver.
Qed.
......@@ -308,7 +341,10 @@ Proof. destruct op, dv1,dv2; simpl; repeat case_match; naive_solver. Qed.
Lemma dcbin_op_eval_dSome_wf E dv1 dv2 op dw:
dval_wf E dv1 dval_wf E dv2
dcbin_op_eval E op dv1 dv2 = dSome dw dval_wf E dw.
Proof. destruct op; first eauto using dbin_op_eval_dSome_wf; naive_solver. Qed.
Proof.
destruct op; first eauto using dbin_op_eval_dSome_wf; try naive_solver.
simpl. unfold dptr_plus_eval. repeat case_match; naive_solver.
Qed.
(** / Well-foundness of dcexpr w.r.t. known_locs *)
......
......@@ -67,41 +67,26 @@ Section memcpy.
rewrite Qp_half_half. iIntros "? ? ? ?".
vcg_continue. iIntros "Hqq Hpp Hw Hy". iLeft; iSplit; first done.
(* TODO: DF: vcgen doesnt do anything here *)
(* vcg_solver. iIntros "Hy Hw Hpp". *)
iApply (a_store_spec _ _
(λ v, v = cloc_to_val p pp C[LLvl] cloc_to_val (cloc_add p 1))
(λ v, v = w q C w qq C[LLvl] cloc_to_val (cloc_add q 1)) with "[Hpp] [Hqq Hw]")%I.
+ vcg_solver. iExists (dValUnknown (cloc_to_val (cloc_add p 1))).
iSplit.
{ iPureIntro. case_option_guard; last omega; simpl.
repeat f_equal. rewrite Nat2Z.id. by destruct p. }
iIntros "Hpp /=". vcg_continue. eauto.
+ vcg_solver. iExists (dValUnknown (cloc_to_val (cloc_add q 1))).
iSplit.
{ iPureIntro. case_option_guard; last omega; simpl.
repeat f_equal. rewrite Nat2Z.id. by destruct q. }
iIntros "Hq Hpp /=". vcg_continue. eauto with iFrame.
+ iNext. iIntros (? ?) "[% Hpp] (% & Hw & Hqq)"; simplify_eq/=.
iExists p,y. iSplit; eauto. iFrame. iIntros "Hy".
iModIntro.
iSpecialize ("IH" $! ls1 (cloc_add p 1) (cloc_add q 1)
with "[Hp] [Hq] Hpp Hqq []"); auto.
{ iApply (big_sepL_impl with "Hp"). iAlways. iIntros (k ? ?) "Hp".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l. }
{ iApply (big_sepL_impl with "Hq"). iAlways. iIntros (k ? ?) "Hq".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l. }
simpl. rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l.
iApply (awp_wand with "IH").
iIntros (?) "[Hp Hq]". rewrite !cloc_add_0. iFrame.
iSplitL "Hp".
* iApply (big_sepL_impl with "Hp"). iAlways. iIntros (k ? ?) "Hp".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l.
* iApply (big_sepL_impl with "Hq"). iAlways. iIntros (k ? ?) "Hq".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l.
vcg_solver. iIntros "Hy Hw Hpp Hqq".
iModIntro.
iSpecialize ("IH" $! ls1 (cloc_add p 1) (cloc_add q 1)
with "[Hp] [Hq] Hpp Hqq []"); auto.
{ iApply (big_sepL_impl with "Hp"). iAlways. iIntros (k ? ?) "Hp".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l. }
{ iApply (big_sepL_impl with "Hq"). iAlways. iIntros (k ? ?) "Hq".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l. }
simpl. rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l.
iApply (awp_wand with "IH").
iIntros (?) "[Hp Hq]". rewrite !cloc_add_0. iFrame.
iSplitL "Hp".
* iApply (big_sepL_impl with "Hp"). iAlways. iIntros (k ? ?) "Hp".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l.
* iApply (big_sepL_impl with "Hq"). iAlways. iIntros (k ? ?) "Hq".
rewrite /cloc_add /=.
by rewrite Nat.add_1_r Nat.add_succ_r Nat.add_succ_l.
Qed.
Lemma memcpy_spec (p q : cloc) (n : nat) (ls1 ls2 : list val) R :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment