Module Values_symbolictype

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

This module defines the type of symbolic values, along with their type-checking functions.

Inductive styp := Tint | Tlong | Tfloat | Tsingle.

Definition styp_eq (x y : styp) : {x = y} + {x <> y}.
Proof.
  decide equality.
Defined.

Lemma styp_eq_refl:
  forall x, styp_eq x x = left eq_refl.
Proof.
  destruct x; simpl; auto.
Qed.

The type lval defines low-level values, i.e. values without pointer or undefined values

Inductive lval : Type :=
| Vi (i:int)
| Vl (i:int64)
| Vf (f:float)
| Vs (f:float32)
.

Lemma eq_lval_inj_i:
  forall i j, Vi i = Vi j -> i = j.
Proof.
  intros.
  inv H; reflexivity.
Qed.

Lemma eq_lval_inj_l:
  forall i j, Vl i = Vl j -> i = j.
Proof.
  intros.
  inv H; reflexivity.
Qed.

Lemma eq_lval_inj_f:
  forall i j, Vf i = Vf j -> i = j.
Proof.
  intros.
  inv H; reflexivity.
Qed.

Lemma eq_lval_inj_s:
  forall i j, Vs i = Vs j -> i = j.
Proof.
  intros.
  inv H; reflexivity.
Qed.


Definition lval_eq_dec (x y : lval) : {x = y}+{x<> y}.
Proof.
  decide equality.
  apply Int.eq_dec.
  apply Int64.eq_dec.
  apply Float.eq_dec.
  apply Float32.eq_dec.
Qed.

Type-checking function for low-level values
Definition tcheck_lval (v:lval) : styp :=
  match v with
      Vi _ => Tint
    | Vl _ => Tlong
    | Vf _ => Tfloat
    | Vs _ => Tsingle
  end.

Definition wt_lval (v:lval) (t:styp) :=
  match v, t with
      Vi _, Tint
    | Vl _, Tlong
    | Vf _, Tfloat
    | Vs _, Tsingle => True
    | _, _ => False
  end.

Definition of unary/binary operators

Inductive se_signedness := SESigned | SEUnsigned.

Inductive unop_t :=
  OpBoolval : unop_t
| OpNotbool : unop_t
| OpNeg : unop_t
| OpNot : unop_t
| OpZeroext : Z -> unop_t
| OpSignext : Z -> unop_t
| OpRolm : int -> int -> unop_t
| OpAbsf
| OpConvert : se_signedness -> (styp*se_signedness) -> unop_t
| OpLoword : unop_t
| OpHiword : unop_t
| OpSingleofbits : unop_t
| OpDoubleofbits : unop_t
| OpBitsofsingle : unop_t
| OpBitsofdouble : unop_t.

Inductive binop_t :=
| OpAnd : binop_t
| OpOr : binop_t
| OpXor : binop_t
| OpAdd : binop_t
| OpSub : binop_t
| OpMul : binop_t
| OpMulh : se_signedness -> binop_t
| OpMull' : binop_t
| OpShrx : binop_t
| OpShr_carry : binop_t
| OpRor : binop_t
| OpFloatofwords : binop_t
| OpLongofwords : binop_t
| OpDiv : se_signedness -> binop_t
| OpMod : se_signedness -> binop_t
| OpCmp : se_signedness -> comparison -> binop_t
| OpShr : se_signedness -> binop_t
| OpShl : binop_t.


The type sval is identical to CompCert's value with the exception that undefined values are labelled by a location.

Inductive sval :=
| Eundef : block -> int -> sval
| Eint : int -> sval
| Elong : int64 -> sval
| Efloat : float -> sval
| Esingle : float32 -> sval
| Eptr : block -> int -> sval.


Inductive expr_sym : Type :=
| Eval : sval -> expr_sym
| Eunop : unop_t -> styp -> expr_sym -> expr_sym
| Ebinop : binop_t -> styp -> styp -> expr_sym -> expr_sym -> expr_sym.


Definition comp_eq_dec (c1 c2: comparison) : {c1=c2} + {c1 <> c2}.
Proof.
  decide equality.
Defined.

Definition se_signedness_eq_dec (s1 s2: se_signedness) : {s1=s2} + {s1 <> s2}.
Proof.
  decide equality.
Defined.

Hint Resolve Val.eq_val_dec.
Hint Resolve eq_nat_dec.
Hint Resolve Z_eq_dec.
Hint Resolve Int.eq_dec.
Hint Resolve Int64.eq_dec.
Hint Resolve styp_eq.
Hint Resolve se_signedness_eq_dec.
Hint Resolve comp_eq_dec.
Hint Resolve Float.eq_dec.
Hint Resolve Float32.eq_dec.

Definition eq_expr_sym_dec (e1 e2: expr_sym) : {e1=e2} + {e1 <> e2}.
Proof.
  repeat decide equality; auto.
Defined.

Definition wt_val (v:val) (r:styp) : Prop :=
  match v, r with
      Vundef, _
    | Vint _, Tint
    | Vlong _, Tlong
    | Vptr _ _, Tint
    | Vfloat _, Tfloat
    | Vsingle _, Tsingle => True
    | _,_ => False
  end.

Lemma wt_val_dec : forall v r, {wt_val v r} + {~wt_val v r}.
Proof.
  intros.
  destruct v; destruct r; simpl; intuition.
Defined.


Inductive is_lval_typ : styp -> Prop :=
| isTint : is_lval_typ Tint
| isTlong : is_lval_typ Tlong.

Definition is_lval_typ_dec (t : styp) : {is_lval_typ t} +{ ~ is_lval_typ t}.
Proof.
  refine
    (match t as t' return {is_lval_typ t'}+{~is_lval_typ t'} with
       | Tint => left isTint
       | Tlong => left isTlong
       | _ => right _
     end);
  intro;
    abstract inversion H.
Defined.


Inductive is_float_typ : styp -> Prop :=
| isTfloat: is_float_typ Tfloat
| isTsingle: is_float_typ Tsingle.

Definition is_float_typ_dec (t : styp) : {is_float_typ t} +{ ~ is_float_typ t}.
Proof.
  refine
    (match t as t' return {is_float_typ t'}+{~is_float_typ t'} with
       | Tfloat => left isTfloat
       | Tsingle => left isTsingle
       | _ => right _
     end);
  intro;
    abstract inversion H.
Defined.


wt_unop o t r holds if the operator o can be used with an argument of type t and returns a result of type r

Definition styp_of_ast (t : typ) : styp :=
  match t with
      Tany32 | AST.Tint => Tint
    | Tany64 | AST.Tlong => Tlong
    | AST.Tfloat => Tfloat
    | AST.Tsingle => Tsingle
  end.

Definition wt_unop (u : unop_t) (t : styp) (r : styp) : Prop :=
  match u with
    | OpBoolval | OpNotbool | OpRolm _ _ => t = Tint /\ r = t
    | OpNeg => t = r
    | OpNot => t = r /\ is_lval_typ t
    | OpZeroext z => t = r /\ is_lval_typ t
    | OpSignext z => t = r /\ is_lval_typ t
    | OpAbsf => t = r /\ is_float_typ t
    | OpConvert s' (ti,s) => ti = r
    | OpLoword => t = Tlong /\ r = Tint
    | OpHiword => t = Tlong /\ r = Tint
    | OpSingleofbits => t = Tint /\ r = Tsingle
    | OpDoubleofbits => t = Tlong /\ r = Tfloat
    | OpBitsofsingle => t = Tsingle /\ r = Tint
    | OpBitsofdouble => t = Tfloat /\ r = Tlong
  end.

Binary operators are parametrised by a single type. This is sufficient to recover the type information for the arguments.


Definition wt_binop (b : binop_t) (t1 : styp) (t2 : styp) (r : styp) : Prop :=
  match b with
    | OpAnd | OpOr | OpXor => t1 = t2 /\ t1 = r /\ is_lval_typ t1
    | OpAdd | OpSub
    | OpMul | OpDiv _ => t1 = t2 /\ t1 = r
    | OpMod _ => t1 = t2 /\ t1 = r /\ is_lval_typ t1
    | OpCmp _ _ => t1 = t2 /\ r = Tint
    | OpShrx | OpShr_carry
    | OpRor => t1 = t2 /\ t1 = Tint /\ r = Tint
    | OpMull' => t1 = t2 /\ t1 = Tint /\ r = Tlong
    | OpMulh _ => t1 = t2 /\ t1 = Tint /\ r = Tint
    | OpFloatofwords => t1 = t2 /\ t1 = Tint /\ r = Tfloat
    | OpLongofwords => t1 = t2 /\ t1 = Tint /\ r = Tlong
    | OpShl | OpShr _ => t1 = r /\ t2 = Tint /\ is_lval_typ t1
  end.

Definition wt_sval (v : sval) (t : styp) : Prop :=
  match v with
    | Eundef _ _ => t = Tint
    | Eint _ => t = Tint
    | Elong _ => t = Tlong
    | Efloat _ => t = Tfloat
    | Esingle _ => t = Tsingle
    | Eptr _ _ => t = Tint
  end.

Fixpoint wt_expr (e:expr_sym) (r:styp) {struct e}: Prop :=
  match e with
    | Eval v => wt_sval v r
    | Eunop u t e => wt_expr e t /\ wt_unop u t r
    | Ebinop b t1 t2 e1 e2 => wt_expr e1 t1 /\ wt_expr e2 t2 /\ wt_binop b t1 t2 r
  end.


Executable type-checking
Definition tcheck_unop (u : unop_t) (t : styp) : option styp :=
  match u with
    | OpBoolval | OpNotbool | OpRolm _ _ => if styp_eq t Tint then Some Tint else None
    | OpNeg => Some t
    | OpNot | OpZeroext _ | OpSignext _ => if is_lval_typ_dec t then Some t else None
    | OpAbsf => if is_float_typ_dec t then Some t else None
    | OpConvert s' (ti,s) => Some ti
    | OpLoword | OpHiword => if styp_eq t Tlong then Some Tint else None
    | OpSingleofbits => if styp_eq t Tint then Some Tsingle else None
    | OpDoubleofbits => if styp_eq t Tlong then Some Tfloat else None
    | OpBitsofsingle => if styp_eq t Tsingle then Some Tint else None
    | OpBitsofdouble => if styp_eq t Tfloat then Some Tlong else None
  end.

Definition tcheck_binop (b : binop_t) (t1 : styp) (t2 : styp) : option styp :=
  match b with
    | OpAnd | OpOr | OpXor => if styp_eq t1 t2
                               then if is_lval_typ_dec t1 then Some t1
                                    else None
                               else None
    | OpAdd | OpSub
    | OpMul | OpDiv _ => if styp_eq t1 t2 then Some t1 else None
    | OpMod _ => if styp_eq t1 t2 then
                                 if is_lval_typ_dec t1
                                 then Some t1 else None
                               else None
    | OpCmp _ _ => if styp_eq t1 t2 then Some Tint else None
    | OpShrx | OpShr_carry
    | OpRor => if styp_eq t1 t2
                               then if styp_eq t1 Tint then Some Tint else None
                               else None
    | OpMull' => if styp_eq t1 t2
                         then if styp_eq t1 Tint then Some Tlong else None
                         else None
    | OpMulh _ => if styp_eq t1 t2
                         then if styp_eq t1 Tint then Some Tint else None
                         else None
    | OpFloatofwords => if styp_eq t1 t2
                         then if styp_eq t1 Tint then Some Tfloat else None
                         else None
    | OpLongofwords => if styp_eq t1 t2
                         then if styp_eq t1 Tint then Some Tlong else None
                         else None
    | OpShl | OpShr _ =>
              if styp_eq t2 Tint
              then if is_lval_typ_dec t1 then Some t1 else None
              else None
  end.

Definition tcheck_sval (v : sval) : styp :=
  match v with
    | Eundef _ _ => Tint
    | Eint _ => Tint
    | Elong _ => Tlong
    | Efloat _ => Tfloat
    | Esingle _ => Tsingle
    | Eptr _ _ => Tint
  end.

Definition has_typ (t : styp) (v : option styp) : bool :=
  match v with
    | None => false
    | Some t' => if styp_eq t t' then true else false
  end.

Lemma has_typ_true:
  forall t e,
    has_typ t e = true ->
    e = Some t.
Proof.
  unfold has_typ; simpl; intros.
  destruct e; simpl in *; intuition try congruence.
  destruct (styp_eq t s); simpl in *; intuition try congruence.
Qed.


Definition map2_option (A:Type) (f : A -> A -> option A) (x y : option A) : option A :=
  match x , y with
    | Some x , Some y => f x y
    | _ , _ => None
  end.


Fixpoint tcheck_expr (e:expr_sym) : option styp :=
  match e with
    | Eval v => Some (tcheck_sval v)
    | Eunop u t e => if has_typ t (tcheck_expr e)
                                    then tcheck_unop u t
                                    else None
    | Ebinop b t1 t2 e1 e2 =>
      if has_typ t1 (tcheck_expr e1)
      then if has_typ t2 (tcheck_expr e2)
           then tcheck_binop b t1 t2
           else None
      else None
  end.


Ltac tcheck :=
  match goal with
    | H : context [typ_eq ?X ?Y] |- _ => destruct (typ_eq X Y)
    | H : context [is_lval_typ_dec ?X] |- _ => destruct (is_lval_typ_dec X)
    | H : context [is_float_typ_dec ?X] |- _ => destruct (is_float_typ_dec X)
    | |- context [styp_eq ?X ?Y] => destruct (styp_eq X Y)
    | |- context [is_lval_typ_dec ?X] => destruct (is_lval_typ_dec X)
    | |- context [is_float_typ_dec ?X] => destruct (is_float_typ_dec X)

  end.


Lemma tcheck_sval_correct :
  forall s r, wt_sval s r <-> tcheck_sval s = r.
Proof.
  destruct s ; simpl ; intuition.
Qed.



Lemma tcheck_unop_correct :
  forall u ty r,
    tcheck_unop u ty = Some r <->
   wt_unop u ty r.
Proof.
  destruct u ; simpl ; intros; try tcheck ; subst; intuition try congruence; subst; auto.
Qed.

Lemma tcheck_binop_correct :
  forall b t1 t2 r,
    tcheck_binop b t1 t2 = Some r <->
    wt_binop b t1 t2 r.
Proof.
  destruct b eqn:? ; simpl ; intros ; try (repeat tcheck ; intuition congruence); subst; auto;
  repeat destr_cond_match; subst; intuition try congruence; subst; intuition try congruence.
Qed.

Lemma tcheck_expr_correct :
  forall e r,
    tcheck_expr e = Some r <-> wt_expr e r.
Proof.
  induction e ; simpl.
  * intros.
    rewrite tcheck_sval_correct.
    intuition congruence.
  * intro r.
    rewrite <- tcheck_unop_correct.
    repeat rewrite <- IHe.
    case_eq (tcheck_expr e) ; simpl; try intuition congruence.
    intros.
    destruct (styp_eq s s0); try intuition congruence.
  *
    intro r.
    case_eq (tcheck_expr e1) ; simpl; intros ; try rewrite <- IHe1 in *.
    -
      intros.
      destruct (styp_eq s s1) ; simpl ; try congruence.
      case_eq (tcheck_expr e2) ; simpl ; intros ; try rewrite <- IHe2 in *.
      destruct (styp_eq s0 s2) ; simpl ; try congruence.
      +
      rewrite tcheck_binop_correct.
      subst ; tauto.
      + intuition try congruence.
      + intuition congruence.
      + intuition try congruence.
    -
        intuition congruence.
Qed.


Lemma wt_expr_determ:
  forall e t1 t2,
    wt_expr e t1 ->
    wt_expr e t2 ->
    t1 = t2.
Proof.
  intros.
  rewrite <- tcheck_expr_correct in H.
  rewrite <- tcheck_expr_correct in H0.
  congruence.
Qed.

Lemma wt_expr_unop_inv:
  forall u t e ty,
    wt_expr (Eunop u t e) ty ->
    wt_expr e t.
Proof.
  intros.
  simpl in H. tauto.
Qed.

Lemma wt_expr_opInt :
  forall e r ,
    wt_expr e Tint ->
    wt_expr e r -> r <> Tint ->
    False.
Proof.
  intros. generalize (wt_expr_determ e Tint r); intuition congruence.
Qed.

Lemma sumbool_destr_and:
  forall A C : Prop, {A} + {~A} -> {C} + {~C} -> {A /\ C} + {~ (A /\ C)}.
Proof.
  intros.
  intuition.
Qed.

Lemma tcheck_expr_dec: forall e r,{ tcheck_expr e = Some r} + {~ tcheck_expr e = Some r}.
Proof.
  intros.
  destruct (tcheck_expr e);
    decide equality.
Qed.

Lemma wt_expr_dec : forall e r, { wt_expr e r } + { ~ wt_expr e r }.
Proof.
  intros.
  generalize (tcheck_expr_dec e r); intro H.
  refine(
      match H with
        | left p => left _
        | right p => right _
      end).
  * rewrite <- tcheck_expr_correct.
    auto.
  * rewrite <- tcheck_expr_correct.
    auto.
Qed.


When we normalise a symbolic expression, we must know into what kind of value we want to normalise it. This is the purpose of the result type. In particular, we would have no way of knowing whether an expression with type Tint should be normalised into a pointer or an integer.

Inductive result := Int | Long | Float | Single | Ptr.

Definition result_eq_dec (r1 r2: result) : { r1=r2 } + { r1 <> r2 }.
Proof.
  decide equality.
Defined.


Some operations are undefined by design (i.e. division by zero or oversized shifts), however we argue that these operations should be undefined in a deterministic fashion, i.e. they should always return the same value when instantiated with the same operands. The function eu (resp. eb) maps unary (resp. binary) operations and their arguments to an arbitrary value.

Parameter eu : unop_t -> styp -> lval -> lval.
Parameter eb : binop_t -> styp -> styp -> lval -> lval -> lval.

Moreover, these arbitrary values must be well-typed, in the following sense.

Definition wt_eu (eu: unop_t -> styp -> lval -> lval) : Prop :=
  forall u t l s,
    tcheck_unop u t = Some s ->
    wt_lval (eu u t l) s.

Definition wt_eb (eb: binop_t -> styp -> styp -> lval -> lval -> lval) : Prop :=
  forall b t t' l l' s,
    tcheck_binop b t t' = Some s ->
    wt_lval (eb b t t' l l') s.

Parameter Hwt_eu: wt_eu eu.
Parameter Hwt_eb: wt_eb eb.

Generated by coq2html