Move the symbolic executor to its own file, and do some renaming to be consistent with the paper.

_CoqProject

@@ -12,7 +12,8 @@ theories/c_translation/proofmode.v
 theories/c_translation/translation.v
 theories/vcgen/dcexpr.v
 theories/vcgen/denv.v
-theories/vcgen/vcgen.v
+theories/vcgen/vcg.v
+theories/vcgen/forward.v
 theories/vcgen/proofmode.v
 theories/vcgen/reification.v
 theories/tests/basics.v

theories/vcgen/forward.v

+From iris_c.c_translation Require Export translation.
+From iris_c.vcgen Require Export denv.
+From iris_c.lib Require Import Q.
+
+Section forward.
+  Context `{amonadG Σ}.
+
+  (** Evaluation of simple expressions *)
+  Fixpoint dexpr_eval (de : dexpr) : option dval :=
+    match de with
+    | dEVal dv => Some dv
+    | dEVar x => None
+    | dEPair de1 de2 =>
+       dv1 ← dexpr_eval de1;
+       dv2 ← dexpr_eval de2;
+       Some (dPairV dv1 dv2)
+    | dEFst de =>
+       dv ← dexpr_eval de;
+       match dv with dPairV dv1 _ => Some dv1 | _ => None end
+    | dESnd de =>
+       dv ← dexpr_eval de;
+       match dv with dPairV _ dv2 => Some dv2 | _ => None end
+    | dENone => Some dNone
+    | dEUnknown _ => None
+    end.
+
+  (** Computes the framing for the resources, necessary for the safety of the
+      expression, and simulatenously computes the strongest postcondition based on that.
+      See `forward_aux_correct` and `forward_correct`. *)
+  Fixpoint forward_aux (E: known_locs) (n : nat) (ms : list denv)
+      (de : dcexpr) : option (list denv * denv * dval) :=
+    match de, n with
+    | _, O => None
+    | dCRet de, _ => dv ← dexpr_eval de; Some (ms, [], dv)
+    | dCSeqBind x de1 de2, S n =>
+       ''(ms1, mNew1, dv1) ← forward_aux E n ms de1;
+       ''(ms2, mNew2, dv2) ← forward_aux E n (denv_unlock mNew1 :: ms1) (dce_subst' E x dv1 de2);
+       ''(ms3, mNew3) ← pop_stack ms2;
+       Some (ms3, denv_merge mNew2 mNew3, dv2)
+    | dCLoad de1, S n =>
+       ''(ms1, mNew, dl)     ← forward_aux E n ms de1;
+       i                     ← dloc_var_of_dval dl;
+       ''(ms2, mNew2, q, dv) ← denv_delete_frac_2 i ms1 mNew;
+       Some (ms2, denv_insert i ULvl q dv mNew2, dv)
+    | dCStore de1 de2, S n =>
+       ''(ms1, mNew1, dl) ← forward_aux E n ms de1;
+       i                  ← dloc_var_of_dval dl;
+       ''(ms2, mNew2, dv) ← forward_aux E n ms1 de2;
+       ''(ms3, mNew3, _)  ← denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
+       Some (ms3, denv_insert i LLvl 1%Q dv mNew3, dv)
+    | dCBinOp op de1 de2, S n =>
+       ''(ms1, mNew1, dv1) ← forward_aux E n ms de1;
+       ''(ms2, mNew2, dv2) ← forward_aux E n ms1 de2;
+       dv ← dcbin_op_eval E op dv1 dv2;
+       Some (ms2, denv_merge mNew1 mNew2, dv)
+    | dCPreBinOp op de1 de2, S n =>
+       ''(ms1, mNew1, dl) ← forward_aux E n ms de1;
+       i                  ← dloc_var_of_dval dl;
+       ''(ms2, mNew2, dv2) ← forward_aux E n ms1 de2;
+       ''(ms3, mNew3, dv) ← denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
+       dv3 ← dcbin_op_eval E op dv dv2;
+       Some (ms3, denv_insert i LLvl 1 dv3 mNew3, dv)
+    | dCUnOp op de, S n =>
+       ''(ms1, mNew1, dv) ← forward_aux E n ms de;
+       dv' ← dun_op_eval E op dv;
+       Some (ms1, mNew1, dv')
+    | dCPar de1 de2, S n =>
+       ''(ms1, mNew1, dv1) ← forward_aux E n ms de1;
+       ''(ms2, mNew2, dv2) ← forward_aux E n ms1 de2;
+         Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2))
+    | dCMutBind _ _ _, _ | dCAlloc _ _, _ | dCWhile _ _, _ | dCWhileV _ _, _
+      | dCCall _ _, _ | dCUnknown _, _ => None
+    end.
+
+  Definition forward (E: known_locs) (n : nat) (m : denv)
+      (de : dcexpr) : option (denv * denv * dval) :=
+    ''(ms,mNew,dv) ← forward_aux E n [m] de;
+    ''(_, m') ← pop_stack ms;
+    Some (m', mNew, dv).
+  Global Arguments forward _ _ !_ /.
+End forward.
+
+Section forward_spec.
+  Context `{amonadG Σ}.
+
+  Hint Extern 2 (_ `prefix_of` _) => etrans; [eassumption|].
+  Hint Extern 0 (0 < 1)%Q => reflexivity.
+  Hint Resolve dknown_bool_of_dval_correct.
+  Hint Resolve dloc_var_of_dval_wf dloc_var_of_dval_correct.
+  Hint Resolve denv_wf_1_stack_pop denv_wf_2_stack_pop.
+  Hint Resolve dun_op_eval_Some_wf dun_op_eval_correct.
+  Hint Resolve dcbin_op_eval_Some_wf dcbin_op_eval_correct.
+  Hint Resolve dce_subst_wf'.
+  Hint Resolve denv_wf_dval_wf_lookup.
+  Hint Resolve denv_wf_insert denv_wf_merge denv_wf_unlock.
+  Hint Resolve denv_wf_delete_full denv_wf_dval_wf_delete_full.
+  Hint Resolve denv_wf_1_delete_frac_2 denv_wf_2_delete_frac_2.
+  Hint Resolve denv_wf_frac_wf_delete_frac_2 denv_wf_dval_wf_delete_frac_2.
+  Hint Resolve denv_wf_1_delete_full_2 denv_wf_2_delete_full_2.
+  Hint Resolve denv_wf_dval_wf_delete_full_2.
+
+  Lemma dexpr_eval_wf E de dv :
+    dexpr_eval de = Some dv → dexpr_wf E de → dval_wf E dv.
+  Proof.
+    revert dv. induction de; intros; repeat (simplify_option_eq || case_match);
+      repeat match goal with
+      | H : ∀ _, _ |- _ => efeed specialize H; [done..|]
+      end; naive_solver.
+  Qed.
+  Hint Resolve dexpr_eval_wf.
+
+  Lemma forward_aux_length E de ms ms' mNew dv n :
+    forward_aux E n ms de = Some (ms', mNew, dv) → length ms = length ms'.
+  Proof.
+    revert de ms ms' mNew dv.
+    induction n as [|n IH]; intros [] **; repeat (simplify_option_eq || case_match);
+      repeat match goal with
+      | H : pop_stack ?ms = _|- _ => is_var ms; destruct ms
+      | H : denv_delete_frac_2 _ _ _ = _ |- _ => apply denv_length_delete_frac_2 in H
+      | H : denv_delete_full_2 _ _ _ = _ |- _ => apply denv_length_delete_full_2 in H
+      | H : forward_aux _ _ _ _ = _ |- _ => apply IH in H
+      end; simplify_eq/=; eauto with lia.
+  Qed.
+
+  Lemma denv_wf_all_wf_forward_aux E de ms ms' mNew dv n :
+    forward_aux E n ms de = Some (ms', mNew, dv) →
+    Forall (denv_wf E) ms → dcexpr_wf E de →
+    Forall (denv_wf E) ms' ∧ denv_wf E mNew ∧ dval_wf E dv.
+  Proof.
+    revert de ms ms' mNew dv. induction n; intros [] **;
+      repeat (case_match || simplify_option_eq); destruct_and?;
+      repeat match reverse goal with
+      | IH : ∀ _ _ _ _ _, forward_aux _ _ _ _ = Some _ → _,
+        H : forward_aux _ _ _ _ = Some _ |- _ =>
+         destruct (IH _ _ _ _ _ H) as (?&?&?); clear H; [by eauto..|]
+      end; split_and!; eauto 10.
+  Qed.
+  Lemma denv_wf_1_forward_aux E de ms ms' mNew dv n :
+    forward_aux E n ms de = Some (ms', mNew, dv) →
+    Forall (denv_wf E) ms → dcexpr_wf E de → Forall (denv_wf E) ms'.
+  Proof. intros; eapply denv_wf_all_wf_forward_aux; eauto. Qed.
+  Lemma denv_wf_2_forward_aux E de ms ms' mNew dv n :
+    forward_aux E n ms de = Some (ms', mNew, dv) →
+    Forall (denv_wf E) ms → dcexpr_wf E de → denv_wf E mNew.
+  Proof. intros; eapply denv_wf_all_wf_forward_aux; eauto. Qed.
+  Lemma denv_wf_dval_wf_forward_aux E de ms ms' mNew dv n :
+    forward_aux E n ms de = Some (ms', mNew, dv) →
+    Forall (denv_wf E) ms → dcexpr_wf E de → dval_wf E dv.
+  Proof. intros; eapply denv_wf_all_wf_forward_aux; eauto. Qed.
+  Hint Resolve denv_wf_1_forward_aux denv_wf_2_forward_aux denv_wf_dval_wf_forward_aux.
+
+  Lemma denv_wf_1_forward E de m m' mNew dv n :
+    forward E n m de = Some (m', mNew, dv) →
+    denv_wf E m → dcexpr_wf E de → denv_wf E m'.
+  Proof.
+    rewrite /forward. intros; repeat (case_match || simplify_option_eq); eauto.
+  Qed.
+  Lemma denv_wf_2_forward E de m m' mNew dv n :
+    forward E n m de = Some (m', mNew, dv) →
+    denv_wf E m → dcexpr_wf E de → denv_wf E mNew.
+  Proof.
+    rewrite /forward. intros; repeat (case_match || simplify_option_eq); eauto.
+  Qed.
+  Lemma denv_wf_dval_wf_forward E de m m' mNew dv n :
+    forward E n m de = Some (m', mNew, dv) →
+    denv_wf E m → dcexpr_wf E de → dval_wf E dv.
+  Proof.
+    rewrite /forward. intros; repeat (case_match || simplify_option_eq); eauto.
+  Qed.
+  Hint Resolve denv_wf_1_forward denv_wf_2_forward denv_wf_dval_wf_forward.
+
+  Lemma dexpr_eval_correct E de dv :
+    dexpr_eval de = Some dv →
+    WP dexpr_interp E de {{ v, ⌜v = dval_interp E dv⌝ }}%I.
+  Proof.
+    iIntros (Hde). iInduction de as [] "IH" forall (dv Hde); simplify_option_eq.
+    - by iApply wp_value.
+    - wp_bind (dexpr_interp E _).
+      iApply wp_wand; [by iApply "IH1"|iIntros (? ->)].
+      wp_bind (dexpr_interp E _).
+      iApply wp_wand; [by iApply "IH"|iIntros (? ->)]. by wp_pures.
+    - case_match; simplify_eq/=. wp_bind (dexpr_interp E _).
+      iApply wp_wand; [by iApply "IH"|iIntros (? ->)]. by wp_pures.
+    - case_match; simplify_eq/=. wp_bind (dexpr_interp E _).
+      iApply wp_wand; [by iApply "IH"|iIntros (? ->)]. by wp_pures.
+    - by wp_pures.
+  Qed.
+
+  Lemma forward_aux_correct E de ms ms' mNew dv R n :
+    forward_aux E n ms de = Some (ms', mNew, dv) →
+    Forall (denv_wf E) ms → dcexpr_wf E de →
+    denv_stack_interp E ms ms' (AWP dcexpr_interp E de @ R
+      {{ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mNew }})%I.
+  Proof.
+    iIntros (Hsp Hms Hde).
+    iInduction n as [|n IH] "IH" forall (de ms ms' mNew dv Hsp Hms Hde).
+    { by destruct de. }
+    destruct de; simplify_eq/=; destruct_and?.
+    - (* return *)
+      destruct (dexpr_eval _) as [dv1|] eqn:?; simplify_eq /=.
+      iApply denv_stack_interp_intro; iApply awp_ret.
+      iApply wp_wand; first by iApply dexpr_eval_correct.
+      iIntros (? ->). iSplit; first done. by rewrite /denv_interp.
+    - (* bind *)
+      destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
+      destruct (forward_aux _ _ (_ :: _) _) as [[[ms2 mNew2] dv2]|] eqn:?; simplify_eq /=.
+      destruct ms2 as [|m2 ms2'] eqn:?; simplify_eq/=.
+      assert (denv_wf E m2 ∧ Forall (denv_wf E) ms') as [??].
+      { apply (Forall_cons (denv_wf E)); eauto 10. }
+      iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
+      iDestruct ("IH" $! _ (_ :: ms1) with "[//] [] []") as "H2 /="; eauto 10.
+      iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
+      iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
+      iApply a_seq_bind_spec. iApply (awp_wand with "H1"); iIntros (v1) "[-> Hm]".
+      iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro.
+      iDestruct ("H2" with "Hm") as "[Hm2 H]". rewrite -dcexpr_interp_subst'.
+      iApply (awp_wand with "H"); iIntros (v2) "[-> Hm]".
+      iSplit; first done. iApply (denv_merge_interp with "[$]"); eauto 10.
+    - (* load *)
+      destruct (forward_aux _ _ _ _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
+      destruct (dloc_var_of_dval _) as [i|] eqn:?; simplify_eq/=.
+      destruct (denv_delete_frac_2 i _ _) as [[[[ms2 mNew2] q] dv2]|] eqn:?; simplify_eq/=.
+      iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H".
+      iDestruct (denv_stack_interp_trans with "H []") as "H".
+      { iApply denv_delete_frac_2_interp; eauto. }
+      iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
+      iApply a_load_spec. iApply (awp_wand with "H1"); iIntros (v1) "[-> Hm]".
+      iDestruct ("H2" with "Hm") as "[Hm2 Hi]".
+      iExists _, _. iFrame "Hi". iSplit; first by eauto.
+      iIntros "Hi"; iSplit; first done.
+      iApply denv_insert_interp; eauto with iFrame.
+    - (* assign *)
+      destruct (forward_aux _ _ _ _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
+      destruct (dloc_var_of_dval _) as [i|] eqn:?; simplify_eq/=.
+      destruct (forward_aux _ _ ms1 _) as [[[ms2 mNew2] dv2]|] eqn:?; simplify_eq /=.
+      destruct (denv_delete_full_2 i ms2 _) as [[[ms3 mNew3] dv3]|] eqn:?; simplify_eq/=.
+      iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
+      iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
+      iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
+      iDestruct (denv_stack_interp_trans with "H []") as "H".
+      { iApply denv_delete_full_2_interp; eauto. }
+      iApply (denv_stack_interp_wand with "H"); iIntros "[[H1 H2] H]".
+      iApply (a_store_spec with "H1 H2").
+      iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
+      iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]".
+      { iApply denv_merge_interp; eauto with iFrame. }
+      iExists _, _. iFrame "Hi". iSplit; first by eauto.
+      iIntros "Hi"; iSplit; first done.
+      iApply denv_insert_interp; eauto 10 with iFrame.
+    - (* bin op *)
+      destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
+      destruct (forward_aux _ _ ms1 _) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
+      destruct (dcbin_op_eval _ _ _ _) eqn:?; simplify_eq/=.
+      iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
+      iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
+      iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
+      iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
+      iApply (a_bin_op_spec with "H1 H2"); iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
+      iExists _. repeat (iSplit; first by eauto).
+      iApply denv_merge_interp; eauto 10 with iFrame.
+    - (* pre bin op *)
+      destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
+      destruct (dloc_var_of_dval _) as [i|] eqn:?; simplify_eq/=.
+      destruct (forward_aux _ _ ms1 _) as [[[ms2 mNew2] dv2]|] eqn:?; simplify_eq /=.
+      destruct (denv_delete_full_2 i ms2 _)
+        as [[[ms3 mNew3] dv'] |] eqn:?; simplify_eq/=.
+      destruct (dcbin_op_eval _ _ _ _) eqn:?; simplify_eq/=.
+      iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
+      iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
+      iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
+      iDestruct (denv_stack_interp_trans with "H []") as "H".
+      { iApply denv_delete_full_2_interp; eauto. }
+      iApply (denv_stack_interp_wand with "H"); iIntros "[[H1 H2] H]".
+      iApply (a_pre_bin_op_spec with "H1 H2").
+      iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
+      iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]".
+      { iApply denv_merge_interp; eauto with iFrame. }
+      iExists _, _, _. iFrame "Hi". repeat (iSplit; first by eauto).
+      iIntros "Hi"; iSplit; first done.
+      iApply denv_insert_interp; eauto 10 with iFrame.
+    - (* un op *)
+      destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
+      destruct (dun_op_eval _ _ _) as [dw|] eqn:?; simplify_eq/=.
+      iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H".
+      iApply (denv_stack_interp_wand with "H"); iIntros "H".
+      iApply a_un_op_spec. iApply (awp_wand with "H"); iIntros (v1) "[-> $]"; eauto.
+    - (* par *)
+      destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
+      destruct (forward_aux _ _ ms1 _) as [[[ms2 mNew2] dv2]|] eqn:?; simplify_eq /=.
+      iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
+      iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
+      iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
+      iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
+      iApply (awp_par with "H1 H2"); iIntros "!>" (v1 v2) "[-> Hm1] [-> Hm2] !>".
+      iSplit; first done. iApply denv_merge_interp; eauto 10 with iFrame.
+  Qed.
+
+  Lemma forward_correct E de m m' mNew dv R n :
+    forward E n m de = Some (m', mNew, dv) →
+    denv_wf E m → dcexpr_wf E de →
+    denv_interp E m -∗
+    denv_interp E m' ∗ AWP dcexpr_interp E de @ R {{ v,
+      ⌜v = dval_interp E dv⌝ ∧ denv_interp E mNew }}.
+  Proof.
+    rewrite /forward. iIntros (Hsp Hwfm Hwf) "Hm".
+    destruct (forward_aux E n [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp'; simplify_eq/=.
+    destruct ms as [|m'' ms]; simplify_eq/=.
+    pose proof (forward_aux_length  _ _ _ _ _ _ _ Hsp'); destruct ms; simplify_eq/=.
+    iDestruct (forward_aux_correct _ _ [_] [_] with "Hm") as "[$$]"; eauto.
+  Qed.
+End forward_spec.

theories/vcgen/proofmode.v

 From iris_c.c_translation Require Export translation.
-From iris_c.vcgen Require Import vcgen denv reification.
+From iris_c.vcgen Require Import vcg denv reification.
 From iris.proofmode Require Import environments coq_tactics.
 Import env_notations.
 
@@ -88,7 +88,7 @@ Section tactics.
   Lemma tac_vcg E1 E2 Γp Γs_in Γs_out m c e de R Φ :
     IntoDEnv [] E1 Γs_in Γs_out m →
     IntoDCExpr E1 E2 e de →
-    envs_entails (Envs Γp Γs_out c) (vcg_wp_while E2 (dcexpr_size de) m de R
+    envs_entails (Envs Γp Γs_out c) (vcg_while E2 (dcexpr_size de) m de R
       (λ E3 m dv, wand_denv_interp E3 m (Φ (dval_interp E3 dv)))) →
     envs_entails (Envs Γp Γs_in c) (AWP e @ R {{ Φ }}).
   Proof.
@@ -99,9 +99,9 @@ Section tactics.
     iDestruct (Hentails with "[$HΓs $HΓp]") as "HΓs".
     { iPureIntro; constructor; naive_solver. }
     iApply (awp_wand with "[-]").
-    { iApply (vcg_wp_while_correct with "[Hm] HΓs"); eauto using denv_wf_mono.
+    { iApply (vcg_while_correct with "[Hm] HΓs"); eauto using denv_wf_mono.
       iApply (denv_interp_mono with "Hm"); eauto. }
-    rewrite /vcg_wp_continuation. iIntros (v) "H".
+    rewrite /vcg_continuation. iIntros (v) "H".
     iDestruct "H" as (E3 dv m' -> ???) "[Hm HΦ]".
     by iApply (wand_denv_interp_spec with "HΦ").
   Qed.
@@ -110,7 +110,7 @@ Section tactics.
     IntoDEnv E1 E2 Γs_in Γs_out m →
     IntoDVal E2 E3 v dv →
     envs_entails (Envs Γp Γs_out c) (Φ E3 m dv) →
-    envs_entails (Envs Γp Γs_in c) (vcg_wp_continuation E1 Φ v).
+    envs_entails (Envs Γp Γs_in c) (vcg_continuation E1 Φ v).
   Proof.
     intros [HΓ ????] [-> ??]; rewrite !envs_entails_eq /= /of_envs.
     iIntros (Hentails) "(Hwf & #HΓp & HΓs)".
@@ -124,7 +124,7 @@ Section tactics.
 End tactics.
 
 (* Make sure users do not see auxiliary junk *)
-Arguments vcg_wp_continuation {_ _ _ _}.
+Arguments vcg_continuation {_ _ _ _}.
 
 Ltac vcg :=
   iStartProof;