Library Values

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

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.

Definition block : Type := Z.
Definition eq_block := zeq.
A value is either:
  • a machine integer;
  • a floating-point number;
  • a pointer: a pair of a memory address and an integer offset with respect to this address;
  • the Vundef value denoting an arbitrary bit pattern, such as the value of an uninitialized variable.

Inductive val: Type :=
  | Vundef: val
  | Vint: int -> val
  | Vfloat: float -> val
  | Vptr: block -> int -> val.

Definition Vzero: val := Vint Int.zero.
Definition Vone: val := Vint Int.one.
Definition Vmone: val := Vint Int.mone.

Definition Vtrue: val := Vint Int.one.
Definition Vfalse: val := Vint Int.zero.
The module Val defines a number of arithmetic and logical operations over type val. Most of these operations are straightforward extensions of the corresponding integer or floating-point operations.

Module Val.

Definition of_bool (b: bool): val := if b then Vtrue else Vfalse.

Definition has_type (v: val) (t: typ) : Prop :=
  match v, t with
  | Vundef, _ => True
  | Vint _, Tint => True
  | Vfloat _, Tfloat => True
  | Vptr _ _, Tint => True
  | _, _ => False
  end.

Fixpoint has_type_list (vl: list val) (tl: list typ) {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.
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.

Definition is_true (v: val) : Prop :=
  match v with
  | Vint n => n <> Int.zero
  | Vptr b ofs => True
  | _ => False
  end.

Definition is_false (v: val) : Prop :=
  match v with
  | Vint n => n = Int.zero
  | _ => False
  end.

Inductive bool_of_val: val -> bool -> Prop :=
  | bool_of_val_int_true:
      forall n, n <> Int.zero -> bool_of_val (Vint n) true
  | bool_of_val_int_false:
      bool_of_val (Vint Int.zero) false
  | bool_of_val_ptr:
      forall b ofs, bool_of_val (Vptr b ofs) true.

Definition neg (v: val) : val :=
  match v with
  | Vint n => Vint (Int.neg n)
  | _ => Vundef
  end.

Definition negf (v: val) : val :=
  match v with
  | Vfloat f => Vfloat (Float.neg f)
  | _ => Vundef
  end.

Definition absf (v: val) : val :=
  match v with
  | Vfloat f => Vfloat (Float.abs f)
  | _ => Vundef
  end.

Definition intoffloat (v: val) : val :=
  match v with
  | Vfloat f => Vint (Float.intoffloat f)
  | _ => Vundef
  end.

Definition intuoffloat (v: val) : val :=
  match v with
  | Vfloat f => Vint (Float.intuoffloat f)
  | _ => Vundef
  end.

Definition floatofint (v: val) : val :=
  match v with
  | Vint n => Vfloat (Float.floatofint n)
  | _ => Vundef
  end.

Definition floatofintu (v: val) : val :=
  match v with
  | Vint n => Vfloat (Float.floatofintu n)
  | _ => Vundef
  end.

Definition notint (v: val) : val :=
  match v with
  | Vint n => Vint (Int.xor n Int.mone)
  | _ => Vundef
  end.

Definition notbool (v: val) : val :=
  match v with
  | Vint n => of_bool (Int.eq n Int.zero)
  | Vptr b ofs => Vfalse
  | _ => Vundef
  end.

Definition zero_ext (nbits: Z) (v: val) : val :=
  match v with
  | Vint n => Vint(Int.zero_ext nbits n)
  | _ => Vundef
  end.

Definition sign_ext (nbits: Z) (v: val) : val :=
  match v with
  | Vint n => Vint(Int.sign_ext nbits n)
  | _ => Vundef
  end.

Definition singleoffloat (v: val) : val :=
  match v with
  | Vfloat f => Vfloat(Float.singleoffloat f)
  | _ => Vundef
  end.

Definition add (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 => Vint(Int.add n1 n2)
  | Vptr b1 ofs1, Vint n2 => Vptr b1 (Int.add ofs1 n2)
  | Vint n1, Vptr b2 ofs2 => Vptr b2 (Int.add ofs2 n1)
  | _, _ => Vundef
  end.

Definition sub (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 => Vint(Int.sub n1 n2)
  | Vptr b1 ofs1, Vint n2 => Vptr b1 (Int.sub ofs1 n2)
  | Vptr b1 ofs1, Vptr b2 ofs2 =>
      if zeq b1 b2 then Vint(Int.sub ofs1 ofs2) else Vundef
  | _, _ => Vundef
  end.

Definition mul (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 => Vint(Int.mul n1 n2)
  | _, _ => Vundef
  end.

Definition divs (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
      if Int.eq n2 Int.zero then Vundef else Vint(Int.divs n1 n2)
  | _, _ => Vundef
  end.

Definition mods (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
      if Int.eq n2 Int.zero then Vundef else Vint(Int.mods n1 n2)
  | _, _ => Vundef
  end.

Definition divu (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
      if Int.eq n2 Int.zero then Vundef else Vint(Int.divu n1 n2)
  | _, _ => Vundef
  end.

Definition modu (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
      if Int.eq n2 Int.zero then Vundef else Vint(Int.modu n1 n2)
  | _, _ => Vundef
  end.

Definition and (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 => Vint(Int.and n1 n2)
  | _, _ => Vundef
  end.

Definition or (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 => Vint(Int.or n1 n2)
  | _, _ => Vundef
  end.

Definition xor (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 => Vint(Int.xor n1 n2)
  | _, _ => Vundef
  end.

Definition shl (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.shl n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition shr (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.shr n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition shr_carry (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.shr_carry n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition shrx (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.shrx n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition shru (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.shru n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition rolm (v: val) (amount mask: int): val :=
  match v with
  | Vint n => Vint(Int.rolm n amount mask)
  | _ => Vundef
  end.

Definition ror (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.ror n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition addf (v1 v2: val): val :=
  match v1, v2 with
  | Vfloat f1, Vfloat f2 => Vfloat(Float.add f1 f2)
  | _, _ => Vundef
  end.

Definition subf (v1 v2: val): val :=
  match v1, v2 with
  | Vfloat f1, Vfloat f2 => Vfloat(Float.sub f1 f2)
  | _, _ => Vundef
  end.

Definition mulf (v1 v2: val): val :=
  match v1, v2 with
  | Vfloat f1, Vfloat f2 => Vfloat(Float.mul f1 f2)
  | _, _ => Vundef
  end.

Definition divf (v1 v2: val): val :=
  match v1, v2 with
  | Vfloat f1, Vfloat f2 => Vfloat(Float.div f1 f2)
  | _, _ => Vundef
  end.

Definition cmp_mismatch (c: comparison): val :=
  match c with
  | Ceq => Vfalse
  | Cne => Vtrue
  | _ => Vundef
  end.

Definition cmp (c: comparison) (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 => of_bool (Int.cmp c n1 n2)
  | Vint n1, Vptr b2 ofs2 =>
      if Int.eq n1 Int.zero then cmp_mismatch c else Vundef
  | Vptr b1 ofs1, Vptr b2 ofs2 =>
      if zeq b1 b2
      then of_bool (Int.cmp c ofs1 ofs2)
      else cmp_mismatch c
  | Vptr b1 ofs1, Vint n2 =>
      if Int.eq n2 Int.zero then cmp_mismatch c else Vundef
  | _, _ => Vundef
  end.

Definition cmpu (c: comparison) (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
      of_bool (Int.cmpu c n1 n2)
  | Vint n1, Vptr b2 ofs2 =>
      if Int.eq n1 Int.zero then cmp_mismatch c else Vundef
  | Vptr b1 ofs1, Vptr b2 ofs2 =>
      if zeq b1 b2
      then of_bool (Int.cmpu c ofs1 ofs2)
      else cmp_mismatch c
  | Vptr b1 ofs1, Vint n2 =>
      if Int.eq n2 Int.zero then cmp_mismatch c else Vundef
  | _, _ => Vundef
  end.

Definition cmpf (c: comparison) (v1 v2: val): val :=
  match v1, v2 with
  | Vfloat f1, Vfloat f2 => of_bool (Float.cmp c f1 f2)
  | _, _ => Vundef
  end.
load_result is used in the memory model (library Mem) to post-process the results of a memory read. 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. Type mismatches (e.g. reading back a float as a Mint32) read back as Vundef.

Definition load_result (chunk: memory_chunk) (v: val) :=
  match chunk, v with
  | Mint8signed, Vint n => Vint (Int.sign_ext 8 n)
  | Mint8unsigned, Vint n => Vint (Int.zero_ext 8 n)
  | Mint16signed, Vint n => Vint (Int.sign_ext 16 n)
  | Mint16unsigned, Vint n => Vint (Int.zero_ext 16 n)
  | Mint32, Vint n => Vint n
  | Mint32, Vptr b ofs => Vptr b ofs
  | Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f)
  | Mfloat64, Vfloat f => Vfloat f
  | _, _ => Vundef
  end.
Theorems on arithmetic operations.

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


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


Theorem istrue_not_isfalse:
  forall v, is_false v -> is_true (notbool v).


Theorem isfalse_not_istrue:
  forall v, is_true v -> is_false (notbool v).


Theorem bool_of_true_val:
  forall v, is_true v -> bool_of_val v true.


Theorem bool_of_true_val2:
  forall v, bool_of_val v true -> is_true v.


Theorem bool_of_true_val_inv:
  forall v b, is_true v -> bool_of_val v b -> b = true.


Theorem bool_of_false_val:
  forall v, is_false v -> bool_of_val v false.


Theorem bool_of_false_val2:
  forall v, bool_of_val v false -> is_false v.


Theorem bool_of_false_val_inv:
  forall v b, is_false v -> bool_of_val v b -> b = false.


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


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


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


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


Theorem add_commut: forall x y, add x y = add y x.


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


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


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


Theorem neg_zero: neg Vzero = Vzero.


Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).


Theorem sub_zero_r: forall x, sub Vzero x = neg x.


Theorem sub_add_opp: forall x y, sub x (Vint y) = add x (Vint (Int.neg y)).


Theorem sub_opp_add: forall x y, sub x (Vint (Int.neg y)) = add x (Vint y).


Theorem sub_add_l:
  forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i).


Theorem sub_add_r:
  forall v1 v2 i, sub v1 (add v2 (Vint i)) = add (sub v1 v2) (Vint (Int.neg i)).


Theorem mul_commut: forall x y, mul x y = mul y x.


Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).


Theorem mul_add_distr_l:
  forall x y z, mul (add x y) z = add (mul x z) (mul y z).


Theorem mul_add_distr_r:
  forall x y z, mul x (add y z) = add (mul x y) (mul x z).


Theorem mul_pow2:
  forall x n logn,
  Int.is_power2 n = Some logn ->
  mul x (Vint n) = shl x (Vint logn).


Theorem mods_divs:
  forall x y, mods x y = sub x (mul (divs x y) y).


Theorem modu_divu:
  forall x y, modu x y = sub x (mul (divu x y) y).


Theorem divs_pow2:
  forall x n logn,
  Int.is_power2 n = Some logn ->
  divs x (Vint n) = shrx x (Vint logn).


Theorem divu_pow2:
  forall x n logn,
  Int.is_power2 n = Some logn ->
  divu x (Vint n) = shru x (Vint logn).


Theorem modu_pow2:
  forall x n logn,
  Int.is_power2 n = Some logn ->
  modu x (Vint n) = and x (Vint (Int.sub n Int.one)).


Theorem and_commut: forall x y, and x y = and y x.


Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).


Theorem or_commut: forall x y, or x y = or y x.


Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).


Theorem xor_commut: forall x y, xor x y = xor y x.


Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).


Theorem shl_mul: forall x y, Val.mul x (Val.shl Vone y) = Val.shl x y.


Theorem shl_rolm:
  forall x n,
  Int.ltu n Int.iwordsize = true ->
  shl x (Vint n) = rolm x n (Int.shl Int.mone n).


Theorem shru_rolm:
  forall x n,
  Int.ltu n Int.iwordsize = true ->
  shru x (Vint n) = rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n).


Theorem shrx_carry:
  forall x y,
  add (shr x y) (shr_carry x y) = shrx x y.


Theorem or_rolm:
  forall x n m1 m2,
  or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2).


Theorem rolm_rolm:
  forall x n1 m1 n2 m2,
  rolm (rolm x n1 m1) n2 m2 =
    rolm x (Int.modu (Int.add n1 n2) Int.iwordsize)
           (Int.and (Int.rol m1 n2) m2).


Theorem rolm_zero:
  forall x m,
  rolm x Int.zero m = and x (Vint m).


Theorem addf_commut: forall x y, addf x y = addf y x.


Lemma negate_cmp_mismatch:
  forall c,
  cmp_mismatch (negate_comparison c) = notbool(cmp_mismatch c).


Theorem negate_cmp:
  forall c x y,
  cmp (negate_comparison c) x y = notbool (cmp c x y).


Theorem negate_cmpu:
  forall c x y,
  cmpu (negate_comparison c) x y = notbool (cmpu c x y).


Lemma swap_cmp_mismatch:
  forall c, cmp_mismatch (swap_comparison c) = cmp_mismatch c.


Theorem swap_cmp:
  forall c x y,
  cmp (swap_comparison c) x y = cmp c y x.


Theorem swap_cmpu:
  forall c x y,
  cmpu (swap_comparison c) x y = cmpu c y x.


Theorem negate_cmpf_eq:
  forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2.


Theorem negate_cmpf_ne:
  forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2.


Lemma or_of_bool:
  forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2).


Theorem cmpf_le:
  forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2).


Theorem cmpf_ge:
  forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2).


Definition is_bool (v: val) :=
  v = Vundef \/ v = Vtrue \/ v = Vfalse.

Lemma of_bool_is_bool:
  forall b, is_bool (of_bool b).


Lemma undef_is_bool: is_bool Vundef.


Lemma cmp_mismatch_is_bool:
  forall c, is_bool (cmp_mismatch c).


Lemma cmp_is_bool:
  forall c v1 v2, is_bool (cmp c v1 v2).


Lemma cmpu_is_bool:
  forall c v1 v2, is_bool (cmpu c v1 v2).


Lemma cmpf_is_bool:
  forall c v1 v2, is_bool (cmpf c v1 v2).


Lemma notbool_is_bool:
  forall v, is_bool (notbool v).


Lemma notbool_xor:
  forall v, is_bool v -> v = xor (notbool v) Vone.


Lemma rolm_lt_zero:
  forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero).


Lemma rolm_ge_zero:
  forall v,
  xor (rolm v Int.one Int.one) (Vint Int.one) = cmp Cge v (Vint Int.zero).
The ``is less defined'' relation between values. A value is less defined than itself, and Vundef is less defined than any value.

Inductive lessdef: val -> val -> Prop :=
  | lessdef_refl: forall v, lessdef v v
  | lessdef_undef: forall v, lessdef Vundef v.

Inductive lessdef_list: list val -> list val -> Prop :=
  | lessdef_list_nil:
      lessdef_list nil nil
  | lessdef_list_cons:
      forall v1 v2 vl1 vl2,
      lessdef v1 v2 -> lessdef_list vl1 vl2 ->
      lessdef_list (v1 :: vl1) (v2 :: vl2).

Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.

Lemma lessdef_list_inv:
  forall vl1 vl2, lessdef_list vl1 vl2 -> vl1 = vl2 \/ In Vundef vl1.


Lemma load_result_lessdef:
  forall chunk v1 v2,
  lessdef v1 v2 -> lessdef (load_result chunk v1) (load_result chunk v2).


Lemma zero_ext_lessdef:
  forall n v1 v2, lessdef v1 v2 -> lessdef (zero_ext n v1) (zero_ext n v2).


Lemma sign_ext_lessdef:
  forall n v1 v2, lessdef v1 v2 -> lessdef (sign_ext n v1) (sign_ext n v2).


Lemma singleoffloat_lessdef:
  forall v1 v2, lessdef v1 v2 -> lessdef (singleoffloat v1) (singleoffloat v2).


End Val.