Module CopGeneric


Arithmetic and logical operators for the Compcert C and Clight languages

In this module, we have kept both the old operators on value and the new ones on symbolic values, and we prove for each pair of those operators that our new operations are abstractions of the old ones, i.e. if sem_* = Some v then exists v', sem_*_expr = Some v' /\ v' == v

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Ctypes.

Syntax of operators.

Require Import CopSyntax.

Type classification and semantics of operators.


Most C operators are overloaded (they apply to arguments of various types) and their semantics depend on the types of their arguments. The following classify_* functions take as arguments the types of the arguments of an operation. They return enough information to resolve overloading for this operator applications, such as ``both arguments are floats'', or ``the first is a pointer and the second is an integer''. This classification is used in the compiler (module Cshmgen) to resolve overloading statically. The sem_* functions below compute the result of an operator application. Since operators are overloaded, the result depends both on the static types of the arguments and on their run-time values. The corresponding classify_* function is first called on the types of the arguments to resolve static overloading. It is then followed by a case analysis on the values of the arguments.

Casts and truth values


Inductive classify_cast_cases : Type :=
  | cast_case_neutral (* int|pointer -> int32|pointer *)
  | cast_case_i2i (sz2:intsize) (si2:signedness) (* int -> int *)
  | cast_case_f2f (* double -> double *)
  | cast_case_s2s (* single -> single *)
  | cast_case_f2s (* double -> single *)
  | cast_case_s2f (* single -> double *)
  | cast_case_i2f (si1: signedness) (* int -> double *)
  | cast_case_i2s (si1: signedness) (* int -> single *)
  | cast_case_f2i (sz2:intsize) (si2:signedness) (* double -> int *)
  | cast_case_s2i (sz2:intsize) (si2:signedness) (* single -> int *)
  | cast_case_l2l (* long -> long *)
  | cast_case_i2l (si1: signedness) (* int -> long *)
  | cast_case_l2i (sz2: intsize) (si2: signedness) (* long -> int *)
  | cast_case_l2f (si1: signedness) (* long -> double *)
  | cast_case_l2s (si1: signedness) (* long -> single *)
  | cast_case_f2l (si2:signedness) (* double -> long *)
  | cast_case_s2l (si2:signedness) (* single -> long *)
  | cast_case_f2bool (* double -> bool *)
  | cast_case_s2bool (* single -> bool *)
  | cast_case_l2bool (* long -> bool *)
  | cast_case_p2bool (* pointer -> bool *)
  | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (* struct -> struct *)
  | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (* union -> union *)
  | cast_case_void (* any -> void *)
  | cast_case_default.

Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
  match tto, tfrom with
  | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) =>
    cast_case_i2i I32 si2
  | Tint IBool _ _, Tfloat F64 _ => cast_case_f2bool
  | Tint IBool _ _, Tfloat F32 _ => cast_case_s2bool
  | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool
  | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2
  | Tint sz2 si2 _, Tfloat F64 _ => cast_case_f2i sz2 si2
  | Tint sz2 si2 _, Tfloat F32 _ => cast_case_s2i sz2 si2
  | Tfloat F64 _, Tfloat F64 _ => cast_case_f2f
  | Tfloat F32 _, Tfloat F32 _ => cast_case_s2s
  | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f
  | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s
  | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1
  | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1
  | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
  | Tlong _ _, Tlong _ _ => cast_case_l2l
  | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1
  | Tint IBool _ _, Tlong _ _ => cast_case_l2bool
  | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2
  | Tlong si2 _, Tfloat F64 _ => cast_case_f2l si2
  | Tlong si2 _, Tfloat F32 _ => cast_case_s2l si2
  | Tfloat F64 _, Tlong si1 _ => cast_case_l2f si1
  | Tfloat F32 _, Tlong si1 _ => cast_case_l2s si1
  | (Tpointer _ _ | Tcomp_ptr _ _), Tlong _ _ => cast_case_l2i I32 Unsigned
  | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2
  | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2
  | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2
  | Tvoid, _ => cast_case_void
  | _, _ => cast_case_default
  end.

Semantics of casts. sem_cast v1 t1 t2 = Some v2 if value v1, viewed with static type t1, can be converted to type t2, resulting in value v2.

Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
  match sz, sg with
  | I8, Signed => Int.sign_ext 8 i
  | I8, Unsigned => Int.zero_ext 8 i
  | I16, Signed => Int.sign_ext 16 i
  | I16, Unsigned => Int.zero_ext 16 i
  | I32, _ => i
  | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one
  end.

Definition cast_int_float (si: signedness) (i: int) : float :=
  match si with
  | Signed => Float.of_int i
  | Unsigned => Float.of_intu i
  end.

Definition cast_float_int (si : signedness) (f: float) : option int :=
  match si with
  | Signed => Float.to_int f
  | Unsigned => Float.to_intu f
  end.

Definition cast_int_single (si: signedness) (i: int) : float32 :=
  match si with
  | Signed => Float32.of_int i
  | Unsigned => Float32.of_intu i
  end.

Definition cast_single_int (si : signedness) (f: float32) : option int :=
  match si with
  | Signed => Float32.to_int f
  | Unsigned => Float32.to_intu f
  end.

Definition cast_int_long (si: signedness) (i: int) : int64 :=
  match si with
  | Signed => Int64.repr (Int.signed i)
  | Unsigned => Int64.repr (Int.unsigned i)
  end.

Definition cast_long_float (si: signedness) (i: int64) : float :=
  match si with
  | Signed => Float.of_long i
  | Unsigned => Float.of_longu i
  end.

Definition cast_long_single (si: signedness) (i: int64) : float32 :=
  match si with
  | Signed => Float32.of_long i
  | Unsigned => Float32.of_longu i
  end.

Definition cast_float_long (si : signedness) (f: float) : option int64 :=
  match si with
  | Signed => Float.to_long f
  | Unsigned => Float.to_longu f
  end.

Definition cast_single_long (si : signedness) (f: float32) : option int64 :=
  match si with
  | Signed => Float32.to_long f
  | Unsigned => Float32.to_longu f
  end.

Definition sem_cast (valid_ptr: block -> int -> bool) (v: val) (t1 t2: type) : option val :=
  match classify_cast t1 t2 with
  | cast_case_neutral =>
      match v with
      | Vint _ | Vptr _ _ => Some v
      | _ => None
      end
  | cast_case_i2i sz2 si2 =>
      match v with
      | Vint i => Some (Vint (cast_int_int sz2 si2 i))
      | _ => None
      end
  | cast_case_f2f =>
      match v with
      | Vfloat f => Some (Vfloat f)
      | _ => None
      end
  | cast_case_s2s =>
      match v with
      | Vsingle f => Some (Vsingle f)
      | _ => None
      end
  | cast_case_s2f =>
      match v with
      | Vsingle f => Some (Vfloat (Float.of_single f))
      | _ => None
      end
  | cast_case_f2s =>
      match v with
      | Vfloat f => Some (Vsingle (Float.to_single f))
      | _ => None
      end
  | cast_case_i2f si1 =>
      match v with
      | Vint i => Some (Vfloat (cast_int_float si1 i))
      | _ => None
      end
  | cast_case_i2s si1 =>
      match v with
      | Vint i => Some (Vsingle (cast_int_single si1 i))
      | _ => None
      end
  | cast_case_f2i sz2 si2 =>
      match v with
      | Vfloat f =>
          match cast_float_int si2 f with
          | Some i => Some (Vint (cast_int_int sz2 si2 i))
          | None => None
          end
      | _ => None
      end
  | cast_case_s2i sz2 si2 =>
      match v with
      | Vsingle f =>
          match cast_single_int si2 f with
          | Some i => Some (Vint (cast_int_int sz2 si2 i))
          | None => None
          end
      | _ => None
      end
  | cast_case_f2bool =>
      match v with
      | Vfloat f =>
          Some(Vint(if Float.cmp Ceq f Float.zero then Int.zero else Int.one))
      | _ => None
      end
  | cast_case_s2bool =>
      match v with
      | Vsingle f =>
          Some(Vint(if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one))
      | _ => None
      end
  | cast_case_p2bool =>
      match v with
      | Vint i => Some (Vint (cast_int_int IBool Signed i))
      | Vptr b o => if valid_ptr b o
                    then Some (Vint Int.one)
                    else None
      | _ => None
      end
  | cast_case_l2l =>
      match v with
      | Vlong n => Some (Vlong n)
      | _ => None
      end
  | cast_case_i2l si =>
      match v with
      | Vint n => Some(Vlong (cast_int_long si n))
      | _ => None
      end
  | cast_case_l2i sz si =>
      match v with
      | Vlong n => Some(Vint (cast_int_int sz si (Int.repr (Int64.unsigned n))))
      | _ => None
      end
  | cast_case_l2bool =>
      match v with
      | Vlong n =>
          Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one))
      | _ => None
      end
  | cast_case_l2f si1 =>
      match v with
      | Vlong i => Some (Vfloat (cast_long_float si1 i))
      | _ => None
      end
  | cast_case_l2s si1 =>
      match v with
      | Vlong i => Some (Vsingle (cast_long_single si1 i))
      | _ => None
      end
  | cast_case_f2l si2 =>
      match v with
      | Vfloat f =>
          match cast_float_long si2 f with
          | Some i => Some (Vlong i)
          | None => None
          end
      | _ => None
      end
  | cast_case_s2l si2 =>
      match v with
      | Vsingle f =>
          match cast_single_long si2 f with
          | Some i => Some (Vlong i)
          | None => None
          end
      | _ => None
      end
  | cast_case_struct id1 fld1 id2 fld2 =>
      match v with
      | Vptr b ofs =>
          if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
      | _ => None
      end
  | cast_case_union id1 fld1 id2 fld2 =>
      match v with
      | Vptr b ofs =>
          if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
      | _ => None
      end
  | cast_case_void =>
      Some v
  | cast_case_default =>
      None
  end.


The following describes types that can be interpreted as a boolean: integers, floats, pointers. It is used for the semantics of the ! and ? operators, as well as the if, while, and for statements.

Inductive classify_bool_cases : Type :=
  | bool_case_i (* integer *)
  | bool_case_f (* double float *)
  | bool_case_s (* single float *)
  | bool_case_p (* pointer *)
  | bool_case_l (* long *)
  | bool_default.

Definition classify_bool (ty: type) : classify_bool_cases :=
  match typeconv ty with
  | Ctypes.Tint _ _ _ => bool_case_i
  | Tpointer _ _ | Tcomp_ptr _ _ => bool_case_p
  | Ctypes.Tfloat F64 _ => bool_case_f
  | Ctypes.Tfloat F32 _ => bool_case_s
  | Ctypes.Tlong _ _ => bool_case_l
  | _ => bool_default
  end.

Interpretation of values as truth values. Non-zero integers, non-zero floats and non-null pointers are considered as true. The integer zero (which also represents the null pointer) and the float 0.0 are false.

Definition bool_val (vptr: block -> int -> bool) (v: val) (t: type) : option bool :=
  match classify_bool t with
  | bool_case_i =>
      match v with
      | Vint n => Some (negb (Int.eq n Int.zero))
      | _ => None
      end
  | bool_case_f =>
      match v with
      | Vfloat f => Some (negb (Float.cmp Ceq f Float.zero))
      | _ => None
      end
  | bool_case_s =>
      match v with
      | Vsingle f => Some (negb (Float32.cmp Ceq f Float32.zero))
      | _ => None
      end
  | bool_case_p =>
      match v with
      | Vint n => Some (negb (Int.eq n Int.zero))
      | Vptr b ofs => if vptr b ofs then Some true else None
      | _ => None
      end
  | bool_case_l =>
      match v with
      | Vlong n => Some (negb (Int64.eq n Int64.zero))
      | _ => None
      end
  | bool_default => None
  end.

Unary operators


Boolean negation


Definition sem_notbool (vptr: block -> int -> bool) (v: val) (ty: type) : option val :=
  match classify_bool ty with
  | bool_case_i =>
      match v with
      | Vint n => Some (Values.Val.of_bool (Int.eq n Int.zero))
      | _ => None
      end
  | bool_case_f =>
      match v with
      | Vfloat f => Some (Values.Val.of_bool (Float.cmp Ceq f Float.zero))
      | _ => None
      end
  | bool_case_s =>
      match v with
      | Vsingle f => Some (Values.Val.of_bool (Float32.cmp Ceq f Float32.zero))
      | _ => None
      end
  | bool_case_p =>
      match v with
      | Vint n => Some (Values.Val.of_bool (Int.eq n Int.zero))
      | Vptr b ofs => if vptr b ofs then Some Vfalse else None
      | _ => None
      end
  | bool_case_l =>
      match v with
      | Vlong n => Some (Values.Val.of_bool (Int64.eq n Int64.zero))
      | _ => None
      end
  | bool_default => None
  end.

Opposite and absolute value


Inductive classify_neg_cases : Type :=
  | neg_case_i(s: signedness) (* int *)
  | neg_case_f (* double float *)
  | neg_case_s (* single float *)
  | neg_case_l(s: signedness) (* long *)
  | neg_default.

Definition classify_neg (ty: type) : classify_neg_cases :=
  match ty with
  | Ctypes.Tint I32 Unsigned _ => neg_case_i Unsigned
  | Ctypes.Tint _ _ _ => neg_case_i Signed
  | Ctypes.Tfloat F64 _ => neg_case_f
  | Ctypes.Tfloat F32 _ => neg_case_s
  | Ctypes.Tlong si _ => neg_case_l si
  | _ => neg_default
  end.

Definition sem_neg (v: val) (ty: type) : option val :=
  match classify_neg ty with
  | neg_case_i sg =>
      match v with
      | Vint n => Some (Vint (Int.neg n))
      | _ => None
      end
  | neg_case_f =>
      match v with
      | Vfloat f => Some (Vfloat (Float.neg f))
      | _ => None
      end
  | neg_case_s =>
      match v with
      | Vsingle f => Some (Vsingle (Float32.neg f))
      | _ => None
      end
  | neg_case_l sg =>
      match v with
      | Vlong n => Some (Vlong (Int64.neg n))
      | _ => None
      end
  | neg_default => None
  end.

Definition sem_absfloat (v: val) (ty: type) : option val :=
  match classify_neg ty with
  | neg_case_i sg =>
      match v with
      | Vint n => Some (Vfloat (Float.abs (cast_int_float sg n)))
      | _ => None
      end
  | neg_case_f =>
      match v with
      | Vfloat f => Some (Vfloat (Float.abs f))
      | _ => None
      end
  | neg_case_s =>
      match v with
      | Vsingle f => Some (Vfloat (Float.abs (Float.of_single f)))
      | _ => None
      end
  | neg_case_l sg =>
      match v with
      | Vlong n => Some (Vfloat (Float.abs (cast_long_float sg n)))
      | _ => None
      end
  | neg_default => None
  end.

Inductive classify_notint_cases : Type :=
  | notint_case_i(s: signedness) (* int *)
  | notint_case_l(s: signedness) (* long *)
  | notint_default.

Definition classify_notint (ty: type) : classify_notint_cases :=
  match ty with
  | Ctypes.Tint I32 Unsigned _ => notint_case_i Unsigned
  | Ctypes.Tint _ _ _ => notint_case_i Signed
  | Ctypes.Tlong si _ => notint_case_l si
  | _ => notint_default
  end.

Definition sem_notint (v: val) (ty: type): option val :=
  match classify_notint ty with
  | notint_case_i sg =>
      match v with
      | Vint n => Some (Vint (Int.not n))
      | _ => None
      end
  | notint_case_l sg =>
      match v with
      | Vlong n => Some (Vlong (Int64.not n))
      | _ => None
      end
  | notint_default => None
  end.


Binary operators


For binary operations, the "usual binary conversions" consist in

Inductive binarith_cases: Type :=
  | bin_case_i (s: signedness) (* at int type *)
  | bin_case_l (s: signedness) (* at long int type *)
  | bin_case_f (* at double float type *)
  | bin_case_s (* at single float type *)
  | bin_default. (* error *)

Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases :=
  match ty1, ty2 with
  | Ctypes.Tint I32 Unsigned _, Ctypes.Tint _ _ _ => bin_case_i Unsigned
  | Ctypes.Tint _ _ _, Ctypes.Tint I32 Unsigned _ => bin_case_i Unsigned
  | Ctypes.Tint _ _ _, Ctypes.Tint _ _ _ => bin_case_i Signed
  | Ctypes.Tlong Signed _, Ctypes.Tlong Signed _ => bin_case_l Signed
  | Ctypes.Tlong _ _, Ctypes.Tlong _ _ => bin_case_l Unsigned
  | Ctypes.Tlong sg _, Ctypes.Tint _ _ _ => bin_case_l sg
  | Ctypes.Tint _ _ _, Ctypes.Tlong sg _ => bin_case_l sg
  | Ctypes.Tfloat F32 _, Ctypes.Tfloat F32 _ => bin_case_s
  | Ctypes.Tfloat _ _, Ctypes.Tfloat _ _ => bin_case_f
  | Ctypes.Tfloat F64 _, (Ctypes.Tint _ _ _ | Ctypes.Tlong _ _) => bin_case_f
  | (Ctypes.Tint _ _ _ | Ctypes.Tlong _ _), Ctypes.Tfloat F64 _ => bin_case_f
  | Ctypes.Tfloat F32 _, (Ctypes.Tint _ _ _ | Ctypes.Tlong _ _) => bin_case_s
  | (Ctypes.Tint _ _ _ | Ctypes.Tlong _ _), Ctypes.Tfloat F32 _ => bin_case_s
  | _, _ => bin_default
  end.

The static type of the result. Both arguments are converted to this type before the actual computation.

Definition binarith_type (c: binarith_cases) : type :=
  match c with
  | bin_case_i sg => Ctypes.Tint I32 sg noattr
  | bin_case_l sg => Ctypes.Tlong sg noattr
  | bin_case_f => Ctypes.Tfloat F64 noattr
  | bin_case_s => Ctypes.Tfloat F32 noattr
  | bin_default => Tvoid
  end.

Definition sem_binarith
           (vptr: block -> int -> bool)
    (sem_int: signedness -> int -> int -> option val)
    (sem_long: signedness -> int64 -> int64 -> option val)
    (sem_float: float -> float -> option val)
    (sem_single: float32 -> float32 -> option val)
    (v1: val) (t1: type) (v2: val) (t2: type) : option val :=
  let c := classify_binarith t1 t2 in
  let t := binarith_type c in
  match sem_cast vptr v1 t1 t with
  | None => None
  | Some v1' =>
  match sem_cast vptr v2 t2 t with
  | None => None
  | Some v2' =>
  match c with
  | bin_case_i sg =>
      match v1', v2' with
      | Vint n1, Vint n2 => sem_int sg n1 n2
      | _, _ => None
      end
  | bin_case_f =>
      match v1', v2' with
      | Vfloat n1, Vfloat n2 => sem_float n1 n2
      | _, _ => None
      end
  | bin_case_s =>
      match v1', v2' with
      | Vsingle n1, Vsingle n2 => sem_single n1 n2
      | _, _ => None
      end
  | bin_case_l sg =>
      match v1', v2' with
      | Vlong n1, Vlong n2 => sem_long sg n1 n2
      | _, _ => None
      end
  | bin_default => None
  end end end.

Addition


Inductive classify_add_cases : Type :=
  | add_case_pi(ty: type) (* pointer, int *)
  | add_case_ip(ty: type) (* int, pointer *)
  | add_case_pl(ty: type) (* pointer, long *)
  | add_case_lp(ty: type) (* long, pointer *)
  | add_default. (* numerical type, numerical type *)

Definition classify_add (ty1: type) (ty2: type) :=
  match typeconv ty1, typeconv ty2 with
  | Tpointer ty _, Ctypes.Tint _ _ _ => add_case_pi ty
  | Ctypes.Tint _ _ _, Tpointer ty _ => add_case_ip ty
  | Tpointer ty _, Ctypes.Tlong _ _ => add_case_pl ty
  | Ctypes.Tlong _ _, Tpointer ty _ => add_case_lp ty
  | _, _ => add_default
  end.

Definition sem_add vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  match classify_add t1 t2 with
  | add_case_pi ty => (* pointer plus integer *)
      match v1,v2 with
      | Vptr b1 ofs1, Vint n2 =>
        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
      | _, _ => None
      end
  | add_case_ip ty => (* integer plus pointer *)
      match v1,v2 with
      | Vint n1, Vptr b2 ofs2 =>
        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
      | _, _ => None
      end
  | add_case_pl ty => (* pointer plus long *)
      match v1,v2 with
      | Vptr b1 ofs1, Vlong n2 =>
        let n2 := Int.repr (Int64.unsigned n2) in
        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
      | _, _ => None
      end
  | add_case_lp ty => (* long plus pointer *)
      match v1,v2 with
      | Vlong n1, Vptr b2 ofs2 =>
        let n1 := Int.repr (Int64.unsigned n1) in
        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
      | _, _ => None
      end
  | add_default =>
      sem_binarith vptr
        (fun sg n1 n2 => Some(Vint(Int.add n1 n2)))
        (fun sg n1 n2 => Some(Vlong(Int64.add n1 n2)))
        (fun n1 n2 => Some(Vfloat(Float.add n1 n2)))
        (fun n1 n2 => Some(Vsingle(Float32.add n1 n2)))
        v1 t1 v2 t2
  end.

Subtraction


Inductive classify_sub_cases : Type :=
  | sub_case_pi(ty: type) (* pointer, int *)
  | sub_case_pp(ty: type) (* pointer, pointer *)
  | sub_case_pl(ty: type) (* pointer, long *)
  | sub_default. (* numerical type, numerical type *)

Definition classify_sub (ty1: type) (ty2: type) :=
  match typeconv ty1, typeconv ty2 with
  | Tpointer ty _, Ctypes.Tint _ _ _ => sub_case_pi ty
  | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty
  | Tpointer ty _, Ctypes.Tlong _ _ => sub_case_pl ty
  | _, _ => sub_default
  end.

Definition sem_sub vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  match classify_sub t1 t2 with
  | sub_case_pi ty => (* pointer minus integer *)
      match v1,v2 with
      | Vptr b1 ofs1, Vint n2 =>
          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
      | _, _ => None
      end
  | sub_case_pl ty => (* pointer minus long *)
      match v1,v2 with
      | Vptr b1 ofs1, Vlong n2 =>
          let n2 := Int.repr (Int64.unsigned n2) in
          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
      | _, _ => None
      end
  | sub_case_pp ty => (* pointer minus pointer *)
      match v1,v2 with
      | Vptr b1 ofs1, Vptr b2 ofs2 =>
          if eq_block b1 b2 then
            if Int.eq (Int.repr (sizeof ty)) Int.zero then None
            else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty))))
          else None
      | _, _ => None
      end
  | sub_default =>
      sem_binarith vptr
        (fun sg n1 n2 => Some(Vint(Int.sub n1 n2)))
        (fun sg n1 n2 => Some(Vlong(Int64.sub n1 n2)))
        (fun n1 n2 => Some(Vfloat(Float.sub n1 n2)))
        (fun n1 n2 => Some(Vsingle(Float32.sub n1 n2)))
        v1 t1 v2 t2
  end.
 

Multiplication, division, modulus


Definition sem_mul vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (fun sg n1 n2 => Some(Vint(Int.mul n1 n2)))
    (fun sg n1 n2 => Some(Vlong(Int64.mul n1 n2)))
    (fun n1 n2 => Some(Vfloat(Float.mul n1 n2)))
    (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2)))
    v1 t1 v2 t2.


Definition sem_div vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (fun sg n1 n2 =>
      match sg with
      | Signed =>
          if Int.eq n2 Int.zero
          || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
          then None else Some(Vint(Int.divs n1 n2))
      | Unsigned =>
          if Int.eq n2 Int.zero
          then None else Some(Vint(Int.divu n1 n2))
      end)
    (fun sg n1 n2 =>
      match sg with
      | Signed =>
          if Int64.eq n2 Int64.zero
          || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone
          then None else Some(Vlong(Int64.divs n1 n2))
      | Unsigned =>
          if Int64.eq n2 Int64.zero
          then None else Some(Vlong(Int64.divu n1 n2))
      end)
    (fun n1 n2 => Some(Vfloat(Float.div n1 n2)))
    (fun n1 n2 => Some(Vsingle(Float32.div n1 n2)))
    v1 t1 v2 t2.

Definition sem_mod vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (fun sg n1 n2 =>
      match sg with
      | Signed =>
          if Int.eq n2 Int.zero
          || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
          then None else Some(Vint(Int.mods n1 n2))
      | Unsigned =>
          if Int.eq n2 Int.zero
          then None else Some(Vint(Int.modu n1 n2))
      end)
    (fun sg n1 n2 =>
      match sg with
      | Signed =>
          if Int64.eq n2 Int64.zero
          || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone
          then None else Some(Vlong(Int64.mods n1 n2))
      | Unsigned =>
          if Int64.eq n2 Int64.zero
          then None else Some(Vlong(Int64.modu n1 n2))
      end)
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2.
 
Definition sem_and vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (fun sg n1 n2 => Some(Vint(Int.and n1 n2)))
    (fun sg n1 n2 => Some(Vlong(Int64.and n1 n2)))
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2.

Definition sem_or vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (fun sg n1 n2 => Some(Vint(Int.or n1 n2)))
    (fun sg n1 n2 => Some(Vlong(Int64.or n1 n2)))
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2.

Definition sem_xor vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (fun sg n1 n2 => Some(Vint(Int.xor n1 n2)))
    (fun sg n1 n2 => Some(Vlong(Int64.xor n1 n2)))
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2.

Shifts


Shifts do not perform the usual binary conversions. Instead, each argument is converted independently, and the signedness of the result is always that of the first argument.

Inductive classify_shift_cases : Type:=
  | shift_case_ii(s: signedness) (* int , int *)
  | shift_case_ll(s: signedness) (* long, long *)
  | shift_case_il(s: signedness) (* int, long *)
  | shift_case_li(s: signedness) (* long, int *)
  | shift_default.

Definition classify_shift (ty1: type) (ty2: type) :=
  match typeconv ty1, typeconv ty2 with
  | Ctypes.Tint I32 Unsigned _, Ctypes.Tint _ _ _ => shift_case_ii Unsigned
  | Ctypes.Tint _ _ _, Ctypes.Tint _ _ _ => shift_case_ii Signed
  | Ctypes.Tint I32 Unsigned _, Ctypes.Tlong _ _ => shift_case_il Unsigned
  | Ctypes.Tint _ _ _, Ctypes.Tlong _ _ => shift_case_il Signed
  | Ctypes.Tlong s _, Ctypes.Tint _ _ _ => shift_case_li s
  | Ctypes.Tlong s _, Ctypes.Tlong _ _ => shift_case_ll s
  | _,_ => shift_default
  end.

Definition sem_shift
    (sem_int: signedness -> int -> int -> int)
    (sem_long: signedness -> int64 -> int64 -> int64)
    (v1: val) (t1: type) (v2: val) (t2: type) : option val :=
  match classify_shift t1 t2 with
  | shift_case_ii sg =>
      match v1, v2 with
      | Vint n1, Vint n2 =>
          if Int.ltu n2 Int.iwordsize
          then Some(Vint(sem_int sg n1 n2)) else None
      | _, _ => None
      end
  | shift_case_il sg =>
      match v1, v2 with
      | Vint n1, Vlong n2 =>
          if Int64.ltu n2 (Int64.repr 32)
          then Some(Vint(sem_int sg n1 (Int64.loword n2))) else None
      | _, _ => None
      end
  | shift_case_li sg =>
      match v1, v2 with
      | Vlong n1, Vint n2 =>
          if Int.ltu n2 Int64.iwordsize'
          then Some(Vlong(sem_long sg n1 (Int64.repr (Int.unsigned n2)))) else None
      | _, _ => None
      end
  | shift_case_ll sg =>
      match v1, v2 with
      | Vlong n1, Vlong n2 =>
          if Int64.ltu n2 Int64.iwordsize
          then Some(Vlong(sem_long sg n1 n2)) else None
      | _, _ => None
      end
  | shift_default => None
  end.

Definition sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_shift
    (fun sg n1 n2 => Int.shl n1 n2)
    (fun sg n1 n2 => Int64.shl n1 n2)
    v1 t1 v2 t2.

Definition sem_shr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_shift
    (fun sg n1 n2 => match sg with Signed => Int.shr n1 n2 | Unsigned => Int.shru n1 n2 end)
    (fun sg n1 n2 => match sg with Signed => Int64.shr n1 n2 | Unsigned => Int64.shru n1 n2 end)
    v1 t1 v2 t2.

Comparisons


Inductive classify_cmp_cases : Type :=
  | cmp_case_pp (* pointer, pointer *)
  | cmp_case_pl (* pointer, long *)
  | cmp_case_lp (* long, pointer *)
  | cmp_default. (* numerical, numerical *)

Definition classify_cmp (ty1: type) (ty2: type) :=
  match typeconv ty1, typeconv ty2 with
  | Tpointer _ _ , Tpointer _ _ => cmp_case_pp
  | Tpointer _ _ , Ctypes.Tint _ _ _ => cmp_case_pp
  | Ctypes.Tint _ _ _, Tpointer _ _ => cmp_case_pp
  | Tpointer _ _ , Ctypes.Tlong _ _ => cmp_case_pl
  | Ctypes.Tlong _ _ , Tpointer _ _ => cmp_case_lp
  | _, _ => cmp_default
  end.

Definition sem_cmp (c:comparison)
                  (v1: val) (t1: type) (v2: val) (t2: type)
                  vptr: option val :=
  match classify_cmp t1 t2 with
  | cmp_case_pp =>
      option_map Values.Val.of_bool (Values.Val.cmpu_bool vptr c v1 v2)
  | cmp_case_pl =>
      match v2 with
      | Vlong n2 =>
          let n2 := Int.repr (Int64.unsigned n2) in
          option_map Values.Val.of_bool (Values.Val.cmpu_bool vptr c v1 (Vint n2))
      | _ => None
      end
  | cmp_case_lp =>
      match v1 with
      | Vlong n1 =>
          let n1 := Int.repr (Int64.unsigned n1) in
          option_map Values.Val.of_bool (Values.Val.cmpu_bool vptr c (Vint n1) v2)
      | _ => None
      end
  | cmp_default =>
      sem_binarith (fun b i => vptr b (Int.unsigned i))
        (fun sg n1 n2 =>
            Some(Values.Val.of_bool(match sg with Signed => Int.cmp c n1 n2 | Unsigned => Int.cmpu c n1 n2 end)))
        (fun sg n1 n2 =>
            Some(Values.Val.of_bool(match sg with Signed => Int64.cmp c n1 n2 | Unsigned => Int64.cmpu c n1 n2 end)))
        (fun n1 n2 =>
            Some(Values.Val.of_bool(Float.cmp c n1 n2)))
        (fun n1 n2 =>
            Some(Values.Val.of_bool(Float32.cmp c n1 n2)))
        v1 t1 v2 t2
  end.

Function applications


Inductive classify_fun_cases : Type :=
  | fun_case_f (targs: typelist) (tres: type) (cc: calling_convention) (* (pointer to) function *)
  | fun_default.

Definition classify_fun (ty: type) :=
  match ty with
  | Tfunction args res cc => fun_case_f args res cc
  | Tpointer (Tfunction args res cc) _ => fun_case_f args res cc
  | _ => fun_default
  end.

Argument of a switch statement


Inductive classify_switch_cases : Type :=
  | switch_case_i
  | switch_case_l
  | switch_default.

Definition classify_switch (ty: type) :=
  match ty with
  | Ctypes.Tint _ _ _ => switch_case_i
  | Ctypes.Tlong _ _ => switch_case_l
  | _ => switch_default
  end.

Definition sem_switch_arg (v: val) (ty: type): option Z :=
  match classify_switch ty with
  | switch_case_i =>
      match v with Vint n => Some(Int.unsigned n) | _ => None end
  | switch_case_l =>
      match v with Vlong n => Some(Int64.unsigned n) | _ => None end
  | switch_default =>
      None
  end.

Combined semantics of unary and binary operators


Definition sem_unary_operation vptr
            (op: unary_operation) (v: val) (ty: type): option val :=
  match op with
  | Onotbool => sem_notbool vptr v ty
  | Onotint => sem_notint v ty
  | Oneg => sem_neg v ty
  | Oabsfloat => sem_absfloat v ty
  end.

Definition sem_binary_operation
    (op: binary_operation)
    (v1: val) (t1: type) (v2: val) (t2:type)
    m : option val :=
  let vptr := fun b i => m b (Int.unsigned i) in
  match op with
  | Oadd => sem_add vptr v1 t1 v2 t2
  | Osub => sem_sub vptr v1 t1 v2 t2
  | Omul => sem_mul vptr v1 t1 v2 t2
  | Omod => sem_mod vptr v1 t1 v2 t2
  | Odiv => sem_div vptr v1 t1 v2 t2
  | Oand => sem_and vptr v1 t1 v2 t2
  | Oor => sem_or vptr v1 t1 v2 t2
  | Oxor => sem_xor vptr v1 t1 v2 t2
  | Oshl => sem_shl v1 t1 v2 t2
  | Oshr => sem_shr v1 t1 v2 t2
  | Oeq => sem_cmp Ceq v1 t1 v2 t2 m
  | One => sem_cmp Cne v1 t1 v2 t2 m
  | Olt => sem_cmp Clt v1 t1 v2 t2 m
  | Ogt => sem_cmp Cgt v1 t1 v2 t2 m
  | Ole => sem_cmp Cle v1 t1 v2 t2 m
  | Oge => sem_cmp Cge v1 t1 v2 t2 m
  end.

Definition sem_incrdecr vptr (id: incr_or_decr) (v: val) (ty: type) :=
  match id with
  | Incr => sem_add vptr v ty (Vint Int.one) type_int32s
  | Decr => sem_sub vptr v ty (Vint Int.one) type_int32s
  end.

Definition incrdecr_type (ty: type) :=
  match typeconv ty with
  | Tpointer ty a => Tpointer ty a
  | Ctypes.Tint sz sg a => Ctypes.Tint sz sg noattr
  | Ctypes.Tlong sg a => Ctypes.Tlong sg noattr
  | Ctypes.Tfloat sz a => Ctypes.Tfloat sz noattr
  | _ => Tvoid
  end.


Some properties of operator semantics


This section collects some common-sense properties about the type classification and semantic functions above. These properties are not used in the CompCert semantics preservation proofs, but increase confidence in the specification and its relation with the ISO C99 standard.

Relation between Boolean value and casting to _Bool type.

Lemma cast_bool_bool_val:
  forall vptr v t,
  sem_cast vptr v t (Ctypes.Tint IBool Signed noattr) =
  match bool_val vptr v t with None => None | Some b => Some(Values.Val.of_bool b) end.
Proof.
  intros.
  assert (A: classify_bool t =
    match t with
    | Ctypes.Tint _ _ _ => bool_case_i
    | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p
    | Ctypes.Tfloat F64 _ => bool_case_f
    | Ctypes.Tfloat F32 _ => bool_case_s
    | Ctypes.Tlong _ _ => bool_case_l
    | _ => bool_default
    end).
  {
    unfold classify_bool; destruct t; simpl; auto. destruct i; auto.
  }
  unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto.
  destruct (Int.eq i0 Int.zero); auto.
  destruct (Int64.eq i Int64.zero); auto.
  destruct f; auto.
  destruct f; auto.
  destruct f; auto.
  destruct f; auto.
  destruct (Float.cmp Ceq f0 Float.zero); auto.
  destruct f; auto.
  destruct (Float32.cmp Ceq f0 Float32.zero); auto.
  destruct f; auto.
  destruct (Int.eq i Int.zero); auto.
  destruct (vptr b i); simpl; auto.
  destruct (Int.eq i Int.zero); auto.
  destruct (vptr b i); simpl; auto.
  destruct (Int.eq i Int.zero); auto.
  destruct (vptr b i); simpl; auto.
  destruct (Int.eq i0 Int.zero); auto.
  destruct (vptr b i0); simpl; auto.
Qed.

Relation between Boolean value and Boolean negation.

Lemma notbool_bool_val:
  forall vptr v t,
  sem_notbool vptr v t =
  match bool_val vptr v t with None => None | Some b => Some(Values.Val.of_bool (negb b)) end.
Proof.
  intros. unfold sem_notbool, bool_val.
  destruct (classify_bool t); auto; destruct v; auto; try rewrite negb_involutive; auto.
  destruct (vptr b i); simpl; auto.
Qed.

Relation with the arithmetic conversions of ISO C99, section 6.3.1

Module ArithConv.

This is the ISO C algebra of arithmetic types, without qualifiers. S stands for "signed" and U for "unsigned".

Inductive int_type : Type :=
  | _Bool
  | Char | SChar | UChar
  | Short | UShort
  | Int | UInt
  | Long | ULong
  | Longlong | ULonglong.

Inductive arith_type : Type :=
  | I (it: int_type)
  | Float
  | Double
  | Longdouble.

Definition eq_int_type: forall (x y: int_type), {x=y} + {x<>y}.
Proof.
decide equality. Defined.

Definition is_unsigned (t: int_type) : bool :=
  match t with
  | _Bool => true
  | Char => false (* as in most of CompCert's target ABIs *)
  | SChar => false
  | UChar => true
  | Short => false
  | UShort => true
  | Int => false
  | UInt => true
  | Long => false
  | ULong => true
  | Longlong => false
  | ULonglong => true
  end.

Definition unsigned_type (t: int_type) : int_type :=
  match t with
  | Char => UChar
  | SChar => UChar
  | Short => UShort
  | Int => UInt
  | Long => ULong
  | Longlong => ULonglong
  | _ => t
  end.

Definition int_sizeof (t: int_type) : Z :=
  match t with
  | _Bool | Char | SChar | UChar => 1
  | Short | UShort => 2
  | Int | UInt | Long | ULong => 4
  | Longlong | ULonglong => 8
  end.

6.3.1.1 para 1: integer conversion rank

Definition rank (t: int_type) : Z :=
  match t with
  | _Bool => 1
  | Char | SChar | UChar => 2
  | Short | UShort => 3
  | Int | UInt => 4
  | Long | ULong => 5
  | Longlong | ULonglong => 6
  end.

6.3.1.1 para 2: integer promotions, a.k.a. usual unary conversions

Definition integer_promotion (t: int_type) : int_type :=
  if zlt (rank t) (rank Int) then Int else t.

6.3.1.8: Usual arithmetic conversions, a.k.a. binary conversions. This function returns the type to which the two operands must be converted.

Definition usual_arithmetic_conversion (t1 t2: arith_type) : arith_type :=
  match t1, t2 with
  | Longdouble, _ | _, Longdouble => Longdouble
  | Double, _ | _, Double => Double
  | Float, _ | _, Float => Float
  | I i1, I i2 =>
    let j1 := integer_promotion i1 in
    let j2 := integer_promotion i2 in
    if eq_int_type j1 j2 then I j1 else
    match is_unsigned j1, is_unsigned j2 with
    | true, true | false, false =>
        if zlt (rank j1) (rank j2) then I j2 else I j1
    | true, false =>
        if zle (rank j2) (rank j1) then I j1 else
        if zlt (int_sizeof j1) (int_sizeof j2) then I j2 else
        I (unsigned_type j2)
    | false, true =>
        if zle (rank j1) (rank j2) then I j2 else
        if zlt (int_sizeof j2) (int_sizeof j1) then I j1 else
        I (unsigned_type j1)
    end
  end.

Mapping ISO arithmetic types to CompCert types

Definition proj_type (t: arith_type) : type :=
  match t with
  | I _Bool => Ctypes.Tint IBool Unsigned noattr
  | I Char => Ctypes.Tint I8 Unsigned noattr
  | I SChar => Ctypes.Tint I8 Signed noattr
  | I UChar => Ctypes.Tint I8 Unsigned noattr
  | I Short => Ctypes.Tint I16 Signed noattr
  | I UShort => Ctypes.Tint I16 Unsigned noattr
  | I Int => Ctypes.Tint I32 Signed noattr
  | I UInt => Ctypes.Tint I32 Unsigned noattr
  | I Long => Ctypes.Tint I32 Signed noattr
  | I ULong => Ctypes.Tint I32 Unsigned noattr
  | I Longlong => Ctypes.Tlong Signed noattr
  | I ULonglong => Ctypes.Tlong Unsigned noattr
  | Float => Ctypes.Tfloat F32 noattr
  | Double => Ctypes.Tfloat F64 noattr
  | Longdouble => Ctypes.Tfloat F64 noattr
  end.

Relation between typeconv and integer promotion.

Lemma typeconv_integer_promotion:
  forall i, typeconv (proj_type (I i)) = proj_type (I (integer_promotion i)).
Proof.
  destruct i; reflexivity.
Qed.

Relation between classify_binarith and arithmetic conversion.

Lemma classify_binarith_arithmetic_conversion:
  forall t1 t2,
  binarith_type (classify_binarith (proj_type t1) (proj_type t2)) =
  proj_type (usual_arithmetic_conversion t1 t2).
Proof.
  destruct t1; destruct t2; try reflexivity.
- destruct it; destruct it0; reflexivity.
- destruct it; reflexivity.
- destruct it; reflexivity.
- destruct it; reflexivity.
- destruct it; reflexivity.
- destruct it; reflexivity.
- destruct it; reflexivity.
Qed.

End ArithConv.

 
Generated by coq2html