This module defines the type of symbolic expressions that is used in the dynamic semantics of all our intermediate languages.

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Values_symbolictype.
Require Import NormaliseSpec.
Require Import Normalise.
Require Import IntFacts.
Require Import ExprEval.

same_eval states that two symbolic expressions are equivalent if they have the same type, and they evaluate identically in any given environment

Definition same_eval (v1 v2: expr_sym) : Prop :=
  forall alloc em,
    eSexpr alloc em v1 = eSexpr alloc em v2.

Lemma same_eval_sym:
  forall v1 v2,
    same_eval v1 v2 -> same_eval v2 v1.

Proof.

red; intros v1 v2 A alloc em; rewrite A; auto.
Qed.

Lemma same_eval_refl:
forall v,
same_eval v v.

Proof.

red; intros; auto.
Qed.

Lemma same_eval_trans:
  forall v1 v2 v3,
    same_eval v1 v2 ->
    same_eval v2 v3 ->
    same_eval v1 v3.

Proof.

red; intros v1 v2 v3 A B alloc em.
rewrite A; rewrite B; auto.
Qed.

Instance same_eval_equi : RelationClasses.Equivalence same_eval :=
  RelationClasses.Build_Equivalence _ _
                                     (same_eval_refl)
                                     (same_eval_sym)
                                     (same_eval_trans).

Lemma norm_eq:
  forall e e' bound align
    (SE: same_eval_on (compat Int.max_unsigned bound align) e e'),
    normalise bound align e = normalise bound align e'.

Proof.

intros.
eapply norm_eq''; simpl; eauto.
Qed.

Ebinop and Eunop are morphisms for same_eval.

Lemma binop_same_eval:
  forall x x' y y' op t t',
    same_eval x x' -> same_eval y y' ->
    same_eval (Ebinop op t t' x y)
      (Ebinop op t t' x' y').

Proof.

intros x x' y y' op t t' A B alloc em.
simpl. rewrite A; rewrite B. auto.
Qed.

Lemma unop_same_eval:
  forall x x' op t ,
    same_eval x x' ->
    same_eval (Eunop op t x) (Eunop op t x').

Proof.

intros x x' op t A alloc em ;
simpl; rewrite A; auto.
Qed.

Definition conserves_same_eval (f: expr_sym -> expr_sym -> option expr_sym) : Prop :=
  forall a b a1 b1,
    same_eval a b ->
    same_eval a1 b1 ->
    match f a a1, f b b1 with
        Some c, Some d => same_eval c d
      | None, None => True
      | _ , _ => False
    end.

Ltac se_rew :=
  repeat ((apply unop_same_eval; simpl; auto)
            ||
            (apply binop_same_eval; simpl; eauto)
            || reflexivity || auto).

Lemma list_forall2_same_eval_refl:
  forall l,
    list_forall2 same_eval l l.

Proof.

induction l; simpl; intros; constructor; auto.
reflexivity.
Qed.

Lemma list_forall2_same_eval_sym:
  forall l1 l2,
    list_forall2 same_eval l1 l2 ->
    list_forall2 same_eval l2 l1.

Proof.

induction 1; simpl; intros; constructor; auto.
symmetry; auto.
Qed.

Lemma list_forall2_same_eval_trans:
  forall l1 l2 l3,
    list_forall2 same_eval l1 l2 ->
    list_forall2 same_eval l2 l3 ->
    list_forall2 same_eval l1 l3.

Proof.

  induction l1; simpl; intros.
  - inv H. inv H0; constructor; auto.
  - inv H. inv H0.
    constructor; auto.
    rewrite H3; auto.
    eapply IHl1; eauto.
Qed.

Instance lf2_se_inst: RelationClasses.Equivalence (list_forall2 same_eval).

Proof.

  constructor; red; intros.
  apply list_forall2_same_eval_refl.
  apply list_forall2_same_eval_sym; auto.
  eapply list_forall2_same_eval_trans; eauto.
Qed.

Operations over values

The module Val defines a number of arithmetic and logical operations over type expr_sym. These operations are generalisations of the operations on values and build symbolic expressions.

Module Val.

  Hint Resolve Val.eq_val_dec.
  Hint Resolve eq_nat_dec.
  Hint Resolve Z_eq_dec.
  Hint Resolve Int.eq_dec.
  Hint Resolve typ_eq.
  Hint Resolve se_signedness_eq_dec.
  Hint Resolve comp_eq_dec.

  Definition has_type (v: expr_sym) (t: styp) : Prop :=
    wt_expr v t.

  Fixpoint has_type_list (vl: list expr_sym) (tl: list styp) {struct vl} : Prop :=
    match vl, tl with
      | nil, nil => True
      | v1 :: vs, t1 :: ts => has_type v1 t1 /\ has_type_list vs ts
      | _, _ => False
    end.

  Definition has_opttype (v: expr_sym) (ot: option styp) : Prop :=
    match ot with
      | None => False
      | Some t => has_type v t
    end.

Truth values. Pointers and non-zero integers are treated as True. The integer 0 (also used to represent the null pointer) is False. Vundef and floats are neither true nor false.

  Inductive bool_of_val: expr_sym -> bool -> Prop :=
  | bool_of_expr_val : forall v b, Val.bool_of_val v b -> bool_of_val (Eval v) b
  .

Arithmetic operations

Operations on 64-bit integers

  Definition longofwords (v1 v2: expr_sym): expr_sym :=
    (Ebinop OpLongofwords Tint Tint) v1 v2.

  Definition loword (v1 : expr_sym): expr_sym :=
    (Eunop OpLoword Tlong) v1.

  Definition hiword (v1 : expr_sym): expr_sym :=
    (Eunop OpHiword Tlong) v1 .

  Definition negl (v: expr_sym) : expr_sym :=
    (Eunop OpNeg Tlong) v.

  Definition notl (v: expr_sym) : expr_sym :=
    (Eunop OpNot Tlong) v.

  Definition longofint (v: expr_sym) : expr_sym :=
    (Eunop (OpConvert SESigned (Tlong,SESigned)) Tint ) v.

  Definition longofsingle (v: expr_sym) : expr_sym :=
    (Eunop (OpConvert SESigned (Tlong,SESigned)) Tsingle ) v.

  Definition longuofsingle (v: expr_sym) : expr_sym :=
    (Eunop (OpConvert SESigned (Tlong,SEUnsigned)) Tsingle ) v.

  Definition longofintu (v: expr_sym) : expr_sym :=
    (Eunop (OpConvert SEUnsigned (Tlong,SESigned)) Tint ) v.

  Definition longoffloat (v: expr_sym) : expr_sym :=
    (fun x => (Eunop (OpConvert SESigned (Tlong,SESigned)) Tfloat x)) v.

  Definition longuoffloat (v: expr_sym) : expr_sym :=
    (fun x => (Eunop (OpConvert SESigned (Tlong,SEUnsigned)) Tfloat x)) v.

  Definition floatoflong (v: expr_sym) : expr_sym :=
    (fun x => (Eunop (OpConvert SESigned (Tfloat,SESigned)) Tlong x)) v.

  Definition floatoflongu (v: expr_sym) : expr_sym :=
    (fun x => (Eunop (OpConvert SEUnsigned (Tfloat,SESigned)) Tlong x)) v.

  Definition addl (v1 v2: expr_sym) : expr_sym :=
    (Ebinop OpAdd Tlong Tlong) v1 v2.

  Definition subl (v1 v2: expr_sym) : expr_sym :=
    (Ebinop OpSub Tlong Tlong) v1 v2.

  Definition mull (v1 v2: expr_sym) : expr_sym :=
    (Ebinop OpMul Tlong Tlong) v1 v2.

  Definition mull' (v1 v2: expr_sym) : expr_sym :=
    (Ebinop OpMull' Tint Tint) v1 v2.

  Definition divls (v1 v2: expr_sym): expr_sym :=
    (fun x y => (Ebinop (OpDiv SESigned) Tlong Tlong x y)) v1 v2.

  Definition modls (v1 v2: expr_sym): expr_sym :=
    (fun x y => (Ebinop (OpMod SESigned) Tlong Tlong x y)) v1 v2.

  Definition divlu (v1 v2: expr_sym): expr_sym :=
    (fun x y => (Ebinop (OpDiv SEUnsigned) Tlong Tlong x y)) v1 v2.

  Definition modlu (v1 v2: expr_sym): expr_sym :=
    (fun x y => (Ebinop (OpMod SEUnsigned) Tlong Tlong x y)) v1 v2.

  Definition andl (v1 v2: expr_sym): expr_sym :=
    (Ebinop OpAnd Tlong Tlong) v1 v2.

  Definition orl (v1 v2: expr_sym): expr_sym :=
    (Ebinop OpOr Tlong Tlong) v1 v2.

  Definition xorl (v1 v2: expr_sym): expr_sym :=
    (Ebinop OpXor Tlong Tlong) v1 v2.

  Definition shll (v1 v2: expr_sym): expr_sym :=
    (Ebinop OpShl Tlong Tint) v1 v2.

  Definition shrl (v1 v2: expr_sym): expr_sym :=
    (Ebinop (OpShr SESigned) Tlong Tint) v1 v2.

  Definition shrlu (v1 v2: expr_sym): expr_sym :=
    (Ebinop (OpShr SEUnsigned) Tlong Tint) v1 v2.

  Definition bitsofsingle (v1 : expr_sym) : expr_sym :=
    Eunop (OpBitsofsingle) Tsingle v1.

  Definition bitsofdouble (v1 : expr_sym) : expr_sym :=
    Eunop (OpBitsofdouble) Tfloat v1.

Comparisons

  Section COMPARISONS.

    Definition cmp_bool (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (Ebinop (OpCmp SESigned c) Tint Tint v1 v2).

    Definition cmp_different_blocks (c: comparison): option bool :=
      match c with
        | Ceq => Some false
        | Cne => Some true
        | _ => None
      end.

    Definition cmpu_bool (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (Ebinop (OpCmp SEUnsigned c) Tint Tint v1 v2).

    Definition cmpf_bool (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (Ebinop (OpCmp SESigned c) Tfloat Tfloat v1 v2).

    Definition cmpfs_bool (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (Ebinop (OpCmp SESigned c) Tsingle Tsingle v1 v2).

    Definition cmpl_bool (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (Ebinop (OpCmp SESigned c) Tlong Tlong v1 v2).

    Definition cmplu_bool (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (Ebinop (OpCmp SEUnsigned c) Tlong Tlong v1 v2).

    Definition maskzero_bool (v:expr_sym) (mask: int): expr_sym :=
      Ebinop (OpCmp SEUnsigned Ceq) Tint Tint (Ebinop OpAnd Tint Tint v (Eval (Vint mask)))
             (Eval (Vint Int.zero)).

    Definition cmp (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (cmp_bool c v1 v2).

    Definition cmpu (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (cmpu_bool c v1 v2).

    Definition cmpf (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (cmpf_bool c v1 v2).

    Definition cmpfs (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (cmpfs_bool c v1 v2).

    Definition cmpl (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (cmpl_bool c v1 v2).

    Definition cmplu (c: comparison) (v1 v2: expr_sym): expr_sym :=
      (cmplu_bool c v1 v2).

  End COMPARISONS.

load_result reflects the effect of storing a value with a given memory chunk, then reading it back with the same chunk. Depending on the chunk and the type of the value, some normalization occurs. For instance, consider storing the integer value 0xFFF on 1 byte at a given address, and reading it back. If it is read back with chunk Mint8unsigned, zero-extension must be performed, resulting in 0xFF. If it is read back as a Mint8signed, sign-extension is performed and 0xFFFFFFFF is returned.

  Definition load_result (chunk: memory_chunk) (v: expr_sym) : expr_sym :=
  match chunk with
    | Mint8signed => sign_ext 8 v
    | Mint8unsigned => zero_ext 8 v
    | Mint16signed => sign_ext 16 v
    | Mint16unsigned => zero_ext 16 v
    | Mint32 => sign_ext 32 v
    | Mint64 => Eunop (OpSignext 64) Tlong v
    | Mfloat32 => Eunop (OpConvert SESigned (Tsingle, SESigned)) Tsingle v
    | Mfloat64 => Eunop (OpConvert SESigned (Tfloat, SESigned)) Tfloat v
    | Many32 => if wt_expr_dec v Tint then v
               else if wt_expr_dec v Tsingle then v
                    else Eval Vundef
    | Many64 => v
  end.

  Lemma load_result_type:
    forall chunk v,
      has_type v (styp_of_ast (type_of_chunk chunk)) ->
      has_type (load_result chunk v) (styp_of_ast (type_of_chunk chunk)).

Proof.

    intros.
    unfold has_type in *.
    des v; try (des (s:sval)); des chunk; try constructor.
    repeat destr.
    repeat destr.
    repeat destr.
  Qed.

Theorems on arithmetic operations.

  Theorem cast8unsigned_and:
    forall x,
      same_eval (zero_ext 8 x) (and x (Eval (Vint(Int.repr 255)))).

Proof.

    red; intros; simpl; seval.
    rewrite Int.zero_ext_and; auto; omega.
  Qed.

  Theorem cast16unsigned_and:
    forall x,
      same_eval (zero_ext 16 x) (and x (Eval (Vint(Int.repr 65535)))).

Proof.

    red; intros; simpl; seval.
    rewrite Int.zero_ext_and; auto; omega.
  Qed.

Theorem notbool_negb_1:
forall b, same_eval (of_bool (negb b)) (notbool (of_bool b)).

Proof.

    unfold notbool.
    red; simpl; intros; seval; des b.
  Qed.

Theorem notbool_negb_2:
forall b, same_eval (of_bool b) (notbool (of_bool (negb b))).

Proof.

    unfold notbool.
    red; simpl; intros; seval; des b.
  Qed.

Theorem notbool_idem2:
forall b, same_eval (notbool(notbool(of_bool b))) (of_bool b).

Proof.

    unfold notbool.
    red; simpl; intros; seval; des b.
  Qed.

  Theorem notbool_idem3:
    forall x, same_eval (notbool(notbool(notbool x))) (notbool x).

Proof.

    unfold notbool.
    red; simpl; intros; seval.
    des (Int.eq i Int.zero).
  Qed.

Theorem add_commut: forall x y, same_eval (add x y) (add y x).

Proof.

unfold add; red; simpl; intros; seval; sint.
Qed.

Theorem add_assoc: forall x y z, same_eval (add (add x y) z) (add x (add y z)).

Proof.

unfold add; red; simpl; intros; seval; sint.
Qed.

Theorem add_permut: forall x y z, same_eval (add x (add y z)) (add y (add x z)).

Proof.

    unfold add; red; simpl; intros; seval; sint.
    apply Int.add_permut.
  Qed.

Theorem add_permut_4:
forall x y z t, same_eval (add (add x y) (add z t)) (add (add x z) (add y t)).

Proof.

    red; simpl; intros; seval; sint;
    match goal with
      | |- Int.add ?i0 (Int.add ?i1 ?i2) = Int.add ?i1 (Int.add ?i0 ?i2) =>
        rewrite (Int.add_permut i0 i1 i2); auto
      | |- Int.add ?i1 (Int.add ?i ?i0) = Int.add ?i0 (Int.add ?i ?i1) =>
        rewrite (Int.add_commut i i0); rewrite (Int.add_permut i1 i0 i);
        rewrite (Int.add_commut i1 i); auto
      | |- Int.add ?i2 (Int.add ?i ?i0) = Int.add ?i (Int.add ?i0 ?i2) =>
        rewrite (Int.add_commut i0 i2); rewrite (Int.add_permut i2 i i0); auto
      | |- Int.add ?i (Int.add ?i1 ?i2) = Int.add ?i2 (Int.add ?i ?i1) =>
        rewrite (Int.add_permut i2 i i1); rewrite (Int.add_commut i2 i1); auto
    end.
  Qed.

We generalize the injection relation so that it specializes undefined values, labelled with locations, into concrete bytes. The injection is parameterised by an extra parameter of type partial_undef_allocation which specifies how undefined values are specialized. Specialization is then performed by function subst.

  Definition partial_undef_allocation := block -> int -> option byte.

  Fixpoint subst (m:partial_undef_allocation) (e: expr_sym) : expr_sym :=
    match e with
      | Eundef b i =>
        match m b i with
            Some byte => Eval (Vint (Int.repr (Byte.unsigned byte)))
          | _ => e
        end
      | Eval ev => Eval ev
      | Eunop u t e => Eunop u t (subst m e)
      | Ebinop b t r e f => Ebinop b t r (subst m e) (subst m f)
    end.

  Lemma subst_id :
    forall e, subst (fun _ _ => None) e = e.

Proof.

    induction e; simpl; eauto.
    rewrite IHe; auto.
    rewrite IHe1; rewrite IHe2; auto.
  Qed.

The evaluation of an expression with substitution m is equal to the evaluation of the same expression in an enriched environment, as computed by aug_em.

  Definition aug_em (em : block -> int -> byte) (m : partial_undef_allocation) :=
    fun b i =>
      match m b i with
          Some byte => byte
        | _ => em b i
      end.

Lemma subst_type:
  forall m e t,
    wt_expr e t <->
    wt_expr (Val.subst m e) t.

Proof.

  induction e; simpl; intros; try tauto.
  - destr; subst; simpl; auto. des t.
  - destr. rewrite <- IHe; auto. rewrite IHe; auto.
  - destr. rewrite <- IHe1; auto. rewrite <- IHe2; auto.
    rewrite IHe1; auto. rewrite IHe2; auto.
Qed.

  Lemma eSexpr_subst_em:
    forall v alloc em m,
      eSexpr alloc em (subst m v) =
      eSexpr alloc (aug_em em m) v.

Proof.

    unfold aug_em; induction v; simpl; intros; auto.
    - destr.
    - rewrite IHv. auto.
    - rewrite IHv1. rewrite IHv2.
      auto.
  Qed.

  Definition option_map2 { A B C} (f : A -> B -> C) (a: option A) (b: option B) : option C :=
    match a, b with
        Some aa, Some bb => Some (f aa bb)
      | _ , _ => None
    end.

The function apply_inj injects a symbolic expression v1 syntactically, where pointers and undefined labels are injected in the same sense as in val_inject. This fails when e mentions a block that is not injected by f.

  Definition inj_undef (f:meminj) (b:block) (i:int) : option expr_sym :=
    match f b with
        Some (b',delta) => Some (Eundef b' (Int.add i (Int.repr delta)))
      | _ => None
    end.

  Definition inj_ptr (f:meminj) (b:block) (i:int) : option expr_sym :=
    match f b with
        Some (b',delta) => Some (Eval (Vptr b' (Int.add i (Int.repr delta))))
      | _ => None
    end.

  Fixpoint apply_inj (f:meminj) (v1: expr_sym) : option expr_sym :=
    match v1 with
        Eundef b i => inj_undef f b i
      | Eval v =>
        match v with
          | Vptr b i => inj_ptr f b i
          | _ => Some (Eval v)
        end
      | Eunop u t e => option_map (Eunop u t) (apply_inj f e)
      | Ebinop b t1 t2 e1 e2 => option_map2 (Ebinop b t1 t2) (apply_inj f e1) (apply_inj f e2)
    end.

expr_inject is the composition of apply_inj and subst.

  Record expr_inject' f e1 e2 : Prop :=
    mk_expr_inject {
        inj_ok: apply_inj f e1 = Some e2
      }.

  Definition expr_inject (f:meminj) (v1 v2: expr_sym) : Prop :=
    expr_inject' f v1 v2.



Lemma ai_type:
  forall f e1 e2 t,
    apply_inj f e1 = Some e2 ->
    (wt_expr e1 t <->
     wt_expr e2 t).

Proof.

  split; revert e1 e2 t H.
  {
    induction e1; simpl; intros e2 t EI WT.
  - des v; inv EI; simpl; des t.
    unfold Val.inj_ptr in H0; des (f b); des p.
    inv H0; simpl; auto.
  - inv EI.
    unfold Val.inj_undef in H0.
    des (f b); des p; inv H0; simpl; auto.
  - destr_and.
    inv EI.
    des (Val.apply_inj f e1). inv H2. destr.
    apply IHe1; auto.
  - repeat destr_and.
    inv EI.
    des (Val.apply_inj f e1_1).
    des (Val.apply_inj f e1_2).
    inv H3; destr.
    apply IHe1_1; auto.
    apply IHe1_2; auto.
  }
    {
    induction e1; simpl; intros e2 t EI WT.
  - des v; inv EI; simpl; des t;
    unfold Val.inj_ptr in H0; des (f b); des p;
    inv H0; simpl; auto.
  - inv EI.
    unfold Val.inj_undef in H0.
    des (f b); des p; inv H0; simpl; auto.
  - destr_and.
    des (Val.apply_inj f e1); inv EI; destr.
    eapply IHe1; eauto.
  - repeat destr_and.
    des (Val.apply_inj f e1_1);
    des (Val.apply_inj f e1_2); inv EI; destr.
    eapply IHe1_1; eauto.
    eapply IHe1_2; eauto.
  }
Qed.

Lemma ei_type:
  forall f e1 e2 t,
    expr_inject f e1 e2 ->
    (wt_expr e1 t <->
     wt_expr e2 t).

Proof.

  intros f e1 e2 t EI.
  inv EI.
  apply ai_type with (t:=t) in inj_ok0; eauto.
Qed.

  Inductive expr_list_inject (f:meminj) : list expr_sym -> list expr_sym -> Prop :=
  | expr_nil_inject:
      expr_list_inject f nil nil
  | expr_cons_inject:
      forall v v' vl vl'
        (EI: expr_inject f v v')
        (ELI: expr_list_inject f vl vl'),
        expr_list_inject f (v::vl) (v'::vl').

  Hint Resolve expr_nil_inject expr_cons_inject.

  Section EXPR_INJ_OPS.

This sections states that unary/binary operations are morphisms for expr_inject, and states some specializations of it.

    Variable f : meminj.

    Lemma expr_inject_unop:
      forall f u t e1 e2,
        expr_inject f e1 e2 ->
        expr_inject f (Eunop u t e1) (Eunop u t e2).

Proof.

      intros; inv H; constructor; simpl.
      rewrite inj_ok0; simpl; auto.
    Qed.

    Lemma expr_inject_binop:
      forall f b t1 t2 e1 e2 e1' e2',
        expr_inject f e1 e2 ->
        expr_inject f e1' e2' ->
        expr_inject f (Ebinop b t1 t2 e1 e1') (Ebinop b t1 t2 e2 e2').

Proof.

      intros; inv H; inv H0; econstructor; simpl.
      rewrite inj_ok0; simpl; auto.
      rewrite inj_ok1; simpl ; auto.
    Qed.

    Lemma expr_load_result_inject':
      forall chunk v1 v2,
        expr_inject f v1 v2 ->
        expr_inject f (load_result chunk v1) (load_result chunk v2).

Proof.

      intros.
      des chunk;
        unfold sign_ext, zero_ext;
        try apply expr_inject_unop; auto.
      repeat destr.
      inv H.
      erewrite ai_type with ( e2:= v2) in w; eauto; congruence.
      inv H. erewrite ai_type with ( e2:= v2) in w; eauto; congruence.
      inv H. erewrite <- ai_type with ( e1:= v1) in w; eauto; congruence.
      inv H. erewrite <- ai_type with ( e1:= v1) in w; eauto; congruence.
      constructor; auto.
    Qed.

    Remark expr_add_inject:
      forall v1 v1' v2 v2',
        expr_inject f v1 v1' ->
        expr_inject f v2 v2' ->
        expr_inject f (add v1 v2) (add v1' v2').

Proof.

      unfold add.
      intros. apply expr_inject_binop; auto.
    Qed.

    Remark expr_sub_inject:
      forall v1 v1' v2 v2',
        expr_inject f v1 v1' ->
        expr_inject f v2 v2' ->
        expr_inject f (sub v1 v2) (sub v1' v2').

Proof.

      intros. unfold sub.
      apply expr_inject_binop; auto.
    Qed.

    Lemma expr_cmp_bool_inject:
      forall c v1 v2 v1' v2',
        expr_inject f v1 v1' ->
        expr_inject f v2 v2' ->
        expr_inject f (cmp_bool c v1 v2) (cmp_bool c v1' v2').

Proof.

      intros.
      apply expr_inject_binop; auto.
    Qed.

    Lemma expr_cmpu_bool_inject:
      forall c v1 v2 v1' v2',
        expr_inject f v1 v1' ->
        expr_inject f v2 v2' ->
        expr_inject f (cmpu_bool c v1 v2) (cmpu_bool c v1' v2').

Proof.

intros. apply expr_inject_binop; auto.
Qed.

    Lemma expr_longofwords_inject:
      forall v1 v2 v1' v2',
        expr_inject f v1 v1' ->
        expr_inject f v2 v2' ->
        expr_inject f (longofwords v1 v2) (longofwords v1' v2').

Proof.

      intros.
      apply expr_inject_binop; auto.
    Qed.

Lemma expr_loword_inject:
forall v v', expr_inject f v v' -> expr_inject f (loword v) (loword v').

Proof.

      intros.
      apply expr_inject_unop; auto.
    Qed.

Lemma expr_hiword_inject:
forall v v', expr_inject f v v' -> expr_inject f (hiword v) (hiword v').

Proof.

      intros.
      apply expr_inject_unop; auto.
    Qed.

  End EXPR_INJ_OPS.

  Definition inj_incr_compat (ei: meminj -> expr_sym -> expr_sym -> Prop) :=
    forall f f' e1 e2
           (INCR: inject_incr f f')
           (EI: ei f e1 e2),
      ei f' e1 e2.

Incremental injections

  Lemma apply_inj_incr:
    forall f1 f2 e e',
      inject_incr f1 f2 ->
      apply_inj f1 e = Some e' ->
      apply_inj f2 e = Some e'.

Proof.

    induction e; simpl; intros.
    - des v.
      specialize (H b).
      unfold inj_ptr in *.
      des (f1 b); des p.
      erewrite H; eauto.
    - specialize (H b).
      unfold inj_undef in *.
      des (f1 b); des p.
      erewrite H; eauto.
    - unfold option_map in *.
      des (apply_inj f1 e).
      erewrite IHe; eauto.
    - unfold option_map2 in *.
      des (apply_inj f1 e1).
      des (apply_inj f1 e2).
      erewrite IHe1; eauto.
      erewrite IHe2; eauto.
  Qed.

  Lemma apply_inj_incr':
    forall e',
      inj_incr_compat (fun f e _ => apply_inj f e = Some e').
    red; intros. eapply apply_inj_incr; eauto.
  Qed.

Module Values_symbolic

Operations over values