started working on vcgen using dcexpr and vcg_sp.

_CoqProject

@@ -9,7 +9,7 @@ theories/c_translation/monad.v
 theories/c_translation/proofmode.v
 theories/c_translation/translation.v
 theories/c_translation/derived.v
-theories/vcgen/dval.v
+theories/vcgen/dcexpr.v
 theories/vcgen/vcgen.v
 # theories/vcgen/test.v
 # theories/heap_lang_vcgen/dval.v

theories/vcgen/dcexpr.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.bi Require Import big_op.
+From iris_c.c_translation Require Import monad translation proofmode.
+
+
+  Inductive dloc :=
+    | dLoc : nat → dloc
+    | dLocUnknown : loc → dloc.
+
+  Global Instance dloc_decision : EqDecision dloc.
+  Proof. solve_decision. Defined.
+
+  Inductive dbase_lit : Type :=
+    | dLitInt : Z → dbase_lit
+    | dLitBool : bool → dbase_lit
+    | dLitUnit : dbase_lit
+    | dLitLoc : dloc → dbase_lit
+    | dLitUnknown : base_lit → dbase_lit.
+
+  Global Instance dlit_decision : EqDecision dbase_lit.
+  Proof. solve_decision. Defined.
+
+  Inductive dval : Type :=
+    | dLitV : dbase_lit → dval
+    | dValUnknown : val → dval.
+
+  Inductive doption (A : Type) : Type :=
+    | dNone : doption A
+    | dSome : A → doption A
+    | dUnknown : option A → doption A.
+
+  Arguments dNone {_}.
+  Arguments dSome {_} _.
+  Arguments dUnknown {_} _.
+
+  Global Instance doption_fmap : FMap doption := λ A B f m,
+    match m with
+    | dNone => dNone
+    | dSome x => dSome (f x)
+    | dUnknown o => dUnknown (f <$> o)
+    end.
+
+
+  Definition dloc_interp (E : list loc) (dl : dloc) : loc :=
+    match dl with
+    | dLoc i => from_option id inhabitant (E !! i)
+    | dLocUnknown l => l
+    end.
+
+  Definition dbase_lit_interp (E : list loc) (l : dbase_lit) : base_lit :=
+    match l with
+    | dLitInt x => LitInt x
+    | dLitBool b => LitBool b
+    | dLitUnit => LitUnit
+    | dLitLoc dl => LitLoc (dloc_interp E dl)
+    | dLitUnknown l => l
+    end.
+
+  Definition dval_interp (E : list loc) (v : dval) : val :=
+    match v with
+    | dLitV l => LitV (dbase_lit_interp E l)
+    | dValUnknown v => v
+    end.
+
+  Fixpoint doption_interp {A} (mx : doption A) : option A :=
+    match mx with
+    | dNone => None
+    | dSome x => Some x
+    | dUnknown mx => mx
+    end.
+
+  Definition dbin_op_eval_int (op : bin_op) (n1 n2 : Z) : dbase_lit :=
+    match op with
+    | PlusOp => dLitInt (n1 + n2)
+    | MinusOp => dLitInt (n1 - n2)
+    | MultOp => dLitInt (n1 * n2)
+    | QuotOp => dLitInt (n1 `quot` n2)
+    | RemOp => dLitInt (n1 `rem` n2)
+    | AndOp => dLitInt (Z.land n1 n2)
+    | OrOp => dLitInt (Z.lor n1 n2)
+    | XorOp => dLitInt (Z.lxor n1 n2)
+    | ShiftLOp => dLitInt (n1 ≪ n2)
+    | ShiftROp => dLitInt (n1 ≫ n2)
+    | LeOp => dLitBool (bool_decide (n1 ≤ n2))
+    | LtOp => dLitBool (bool_decide (n1 < n2))
+    | EqOp => dLitBool (bool_decide (n1 = n2))
+    end.
+
+  Lemma dbin_op_eval_int_correct E op n1 n2 :
+    bin_op_eval_int op n1 n2 = dbase_lit_interp E (dbin_op_eval_int op n1 n2).
+  Proof. by destruct op. Qed.
+
+  Definition dbin_op_eval_bool
+      (op : bin_op) (b1 b2 : bool) : doption dbase_lit :=
+    match op with
+    | PlusOp | MinusOp | MultOp | QuotOp | RemOp => dNone (* Arithmetic *)
+    | AndOp => dSome (dLitBool (b1 && b2))
+    | OrOp => dSome (dLitBool (b1 || b2))
+    | XorOp => dSome (dLitBool (xorb b1 b2))
+    | ShiftLOp | ShiftROp => dNone (* Shifts *)
+    | LeOp | LtOp => dNone (* InEquality *)
+    | EqOp => dSome (dLitBool (bool_decide (b1 = b2)))
+    end.
+
+  Lemma dbin_op_eval_bool_correct E op b1 b2 w :
+    dbin_op_eval_bool op b1 b2 = dSome w →
+    bin_op_eval_bool op b1 b2 = Some (dbase_lit_interp E w).
+  Proof. destruct op; simpl; try by inversion 1. Qed.
+
+  Definition dbin_op_eval
+             (E : list loc) (op : bin_op) (dv1 dv2 : dval) : doption dval :=
+    match dv1,dv2 with
+    | dValUnknown _, _ | _,dValUnknown _ =>
+       dUnknown
+        (dValUnknown <$> bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
+    | dLitV l1, dLitV l2 =>
+      if decide (op = EqOp)
+      then dSome $ dLitV $ dLitBool
+                 $ bool_decide (dbase_lit_interp E l1 = dbase_lit_interp E l2)
+      else match l1, l2 with
+           | (dLitInt n1), (dLitInt n2) =>
+             dSome $ dLitV $ dbin_op_eval_int op n1 n2
+           | (dLitBool b1), (dLitBool b2) =>
+             dLitV <$> dbin_op_eval_bool op b1 b2
+           | dLitUnknown _, _ | _, dLitUnknown _ =>
+               dUnknown (dValUnknown <$>
+                  bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
+           | _, _ => dNone
+           end
+    end.
+
+  Lemma dbin_op_eval_correct E op dv1 dv2 w :
+    doption_interp (dbin_op_eval E op dv1 dv2) = Some w →
+    bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) =
+    Some (dval_interp E w).
+  Proof.
+    destruct dv1 as [dl1 | v1].
+    - destruct dv2 as [dl2 | v2].
+      + unfold bin_op_eval. simpl. case_decide; simplify_eq/=.
+        { inversion 1. rewrite /bin_op_eval /=.  f_equal. simplify_eq /=.
+           do 2 case_bool_decide; simplify_eq /=; eauto. destruct H0. done. }
+        { rewrite /bin_op_eval; intros; destruct dl1, dl2;
+            rewrite /bin_op_eval_int /bin_op_eval_bool; simplify_eq /=; f_equal;
+              try (destruct op; done); simpl.
+          -  rewrite /bin_op_eval in H0; case_decide; first done.
+             destruct b; simplify_eq /=; f_equal.
+          - destruct op; simplify_eq /=; try done.
+          -  case_decide; first done. destruct b0; simplify_eq /=; f_equal.
+             destruct op; simplify_eq /=; try done.
+          -  case_decide; first done. destruct b; simplify_eq /=; f_equal.
+          -  case_decide; first done; destruct b; simplify_eq /=; f_equal;
+              destruct op; simplify_eq /=; try done.
+          -  case_decide; first done; destruct b; simplify_eq /=; f_equal.
+          -  case_decide; first done; destruct b; simplify_eq /=; f_equal.
+          -  case_decide; first done; destruct b,b0; simplify_eq /=; f_equal.
+             destruct op; simplify_eq /=; try done. }
+      + simpl; destruct (bin_op_eval op #(dbase_lit_interp E dl1) v2);
+          try by inversion 1.
+    - simpl; destruct (bin_op_eval op v1 (dval_interp E dv2));
+        try by inversion 1.
+  Qed.
+
+   (** ** LocLookup *)
+  Class LocLookup (E : list loc) (l : loc) (i : nat) :=
+    loc_lookup : E !! i = Some l.
+
+  Global Instance loc_lookup_here l E : LocLookup (l :: E) l 0.
+  Proof. done. Qed.
+
+  Global Instance loc_lookup_there l l' E i :
+    LocLookup E l i → LocLookup (l' :: E) l (S i).
+  Proof. done. Qed.
+
+  (** ** BaseLitQuote *)
+  Class BaseLitQuote (E : list loc) (l : base_lit) (dl : dbase_lit) :=
+    base_lit_quote : l = dbase_lit_interp E dl.
+
+  (** BaseLitQuote for locs *)
+  Global Instance base_lit_quote_loc E l i :
+    LocLookup E l i → BaseLitQuote E (LitLoc l) (dLitLoc (dLoc i)) | 1.
+  Proof. by rewrite /LocLookup /BaseLitQuote /= => ->. Qed.
+
+  Global Instance base_lit_quote_loc_unknown E l :
+    BaseLitQuote E (LitLoc l) (dLitLoc (dLocUnknown l)) | 10.
+  Proof. done. Qed.
+
+  (** BaseLitQuote for constants *)
+  Global Instance base_lit_quote_int E i :
+    BaseLitQuote E (LitInt i) (dLitInt i).
+  Proof. by rewrite /BaseLitQuote /=. Qed.
+
+  Global Instance base_lit_quote_default E l :
+    BaseLitQuote E l (dLitUnknown l) | 1000.
+  Proof. done. Qed.
+
+  (** IntoDVal *)
+  Class IntoDVal (E : list loc) (e : expr) (dv : dval) :=
+    into_dval : e = of_val (dval_interp E dv).
+
+  Global Instance into_dval_loc E l dl :
+    BaseLitQuote E l dl → IntoDVal E (Lit l) (dLitV dl).
+  Proof. by rewrite /BaseLitQuote /IntoDVal=> ->. Qed.
+
+  Global Instance into_dval_default E e v :
+    IntoVal e v → IntoDVal E e (dValUnknown v) | 1000.
+  Proof. by rewrite /IntoVal /IntoDVal=> /of_to_val ->. Qed.
+
+  (** DCexpr *)
+
+  (*TODO: extend this with other constructions :
+    alloc, unop, seq, while, invoke *)
+
+  Inductive dcexpr : Type :=
+  | dCVal  : dval → dcexpr
+  | dCLoad : dcexpr → dcexpr
+  | dCStore : dcexpr → dcexpr → dcexpr
+  | dCBinOp : bin_op → dcexpr → dcexpr → dcexpr.
+
+  Fixpoint dcexpr_interp (E: list loc) (d: dcexpr) : expr :=
+    match d with
+    | dCVal dv => a_ret (dval_interp E dv)
+    | dCLoad d1 => a_load (dcexpr_interp E d1)
+    | dCStore d1 d2 => a_store (dcexpr_interp E d1) (dcexpr_interp E d2)
+    | dCBinOp op d1 d2 => a_bin_op op (dcexpr_interp E d1) (dcexpr_interp E d2)
+    end.
+
+  Class IntoDCexpr (E: list loc) (e: expr) (de: dcexpr) :=
+    into_dcexpr : e = dcexpr_interp E de.
+
+  Global Instance into_dcexpr_val E v dv:
+    IntoDVal E v dv →
+    IntoDCexpr E (a_ret v) (dCVal dv).
+  Proof. by rewrite /IntoDCexpr=> ->. Qed.
+
+  Global Instance into_dcexpr_load E e de:
+    IntoDCexpr E e de →
+    IntoDCexpr E (a_load e) (dCLoad de).
+  Proof. by rewrite /IntoDCexpr=> ->. Qed.
+
+  Global Instance into_dcexpr_store E e1 e2 de1 de2:
+    IntoDCexpr E e1 de1 →
+    IntoDCexpr E e2 de2 →
+    IntoDCexpr E (a_store e1 e2) (dCStore de1 de2).
+  Proof. by rewrite /IntoDCexpr=> -> ->. Qed.

theories/vcgen/vcgen.v

 From iris.heap_lang Require Export proofmode notation.
 From iris.bi Require Import big_op.
-From iris_c.vcgen Require Import dval.
+From iris_c.vcgen Require Import dcexpr.
 From iris_c.c_translation Require Import monad translation proofmode.
 From iris_c.lib Require Import locking_heap U.
 
 Section vcg.
   Context `{amonadG Σ}.
 
-   Inductive wp_expr :=
+
+  Inductive wp_expr :=
     | Base : iProp Σ → wp_expr
     | Inhale : dloc → (dval → wp_expr) → wp_expr
     | Exhale : dloc → dval → level → wp_expr → wp_expr
@@ -20,7 +21,6 @@ Section vcg.
        (dval → dval → wp_expr) → wp_expr.
    Arguments Base _%I.
 
-
   Fixpoint wp_interp (E : list loc) (a : wp_expr) : iProp Σ :=
     match a with
     | Base P => P
@@ -56,6 +56,14 @@ Section vcg.
        ∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2))
   end%I.
 
+
+  Fixpoint vcg_wp (E: list loc) (s: list (nat * dval)) (de : dcexpr) (t: dval → wp_expr) : wp_expr :=
+    match de with
+    | dCVal dv => t dv
+    | dCLoad de1 => vcg_wp E s de1 (λ dv, IsLoc dv (λ l, Inhale l (λ w, Exhale l w ULvl (t w))))
+    | _ => t (dValUnknown #())
+    end.
+
   Lemma wp_interp_sane_sound E a : wp_interp_sane E a ⊢ wp_interp E a.
   Proof.
     generalize dependent E.
@@ -75,8 +83,10 @@ Section vcg.
       iSplitL "HΨ1". by iApply H0.
       iSplitL "HΨ2". by iApply H1.
       iIntros (dv1 dv2) "Hv1 Hv2". iApply H2.
-      iApply ("HΦ" with "Hv1 Hv2").
-  Qed.
+      admit.
+Admitted.
+
+ (* No need for those classes any more)
 
   Class AWpQuote (E : list loc) (e : expr) (R : iProp Σ) (Φ : dval → wp_expr) (t : wp_expr) :=
     wp_quote :
@@ -129,7 +139,7 @@ Section vcg.
       iApply (awp_wand with "H"). iIntros (?).
       iDestruct 1 as (dv <- dl ?) "HΨ1". iExists _.
       iSplit; eauto.
-    - iPoseProof (He2 with "HΨ2") as "H".      
+    - iPoseProof (He2 with "HΨ2") as "H".
       iApply (awp_wand with "H"). iIntros (?).
       iDestruct 1 as (dv <-) "$".
     - iNext. iIntros (l w) "HΨ1 HΨ2".
@@ -152,7 +162,7 @@ Section vcg.
     wp_op.
     - by apply dbin_op_eval_correct.
     - iExists w. auto.
-  Qed.  
+  Qed.
 
 
   Global Instance wp_quote_seq E e1 e2 Φ Ψ t `{Closed [] e2}:
@@ -167,6 +177,8 @@ Section vcg.
   Qed.
    *)
 
+*)
+
   Fixpoint exhale_list (s : list (nat * dval)) (Φ : wp_expr) : wp_expr :=
     match s with
     | (i, v) :: s' => Exhale (dLoc i) v ULvl (exhale_list s' Φ)
@@ -403,7 +415,7 @@ Section vcg.
     - by iApply Hexhale.
   Qed.
 
-  Lemma tac_vcg_opt_list_sound Γs_in Γs_out Γls Γp ps c e R Φ E t :
+ (* Lemma tac_vcg_opt_list_sound Γs_in Γs_out Γls Γp ps c e R Φ E t :
     MapstoListFromEnv Γs_in Γs_out Γls →
     E = env_to_known_locs Γls →
     ListOfMapsto Γls E ps →
@@ -456,6 +468,5 @@ Section Tests_vcg.
     iIntros "Hl". iExists l'. iSplit; eauto.
     iExists #1. iFrame.
   Qed.
-
-  
-End 
+*)
+End vcg.