Library SelectOpproof

Correctness of instruction selection for operators





Require Import Coqlib.

Require Import Maps.

Require Import AST.

Require Import Integers.

Require Import Floats.

Require Import Values.

Require Import Mem.

Require Import Events.

Require Import Globalenvs.

Require Import Smallstep.

Require Import Cminor.

Require Import Op.

Require Import CminorSel.

Require Import SelectOp.




Open Local Scope cminorsel_scope.




Section CMCONSTR.




Variable ge: genv.

Variable sp: val.

Variable e: env.

Variable m: mem.

Useful lemmas and tactics

The following are trivial lemmas and custom tactics that help perform backward (inversion) and forward reasoning over the evaluation of operator applications.





Ltac EvalOp := eapply eval_Eop; eauto with evalexpr.




Ltac TrivialOp cstr := unfold cstr; intros; EvalOp.




Ltac InvEval1 :=

  match goal with

  | [ H: (eval_expr _ _ _ _ _ (Eop _ Enil) _) |- _ ] =>

      inv H; InvEval1

  | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: Enil)) _) |- _ ] =>

      inv H; InvEval1

  | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: _ ::: Enil)) _) |- _ ] =>

      inv H; InvEval1

  | [ H: (eval_exprlist _ _ _ _ _ Enil _) |- _ ] =>

      inv H; InvEval1

  | [ H: (eval_exprlist _ _ _ _ _ (_ ::: _) _) |- _ ] =>

      inv H; InvEval1

  | _ =>

      idtac

  end.




Ltac InvEval2 :=

  match goal with

  | [ H: (eval_operation _ _ _ nil = Some _) |- _ ] =>

      simpl in H; inv H

  | [ H: (eval_operation _ _ _ (_ :: nil) = Some _) |- _ ] =>

      simpl in H; FuncInv

  | [ H: (eval_operation _ _ _ (_ :: _ :: nil) = Some _) |- _ ] =>

      simpl in H; FuncInv

  | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) = Some _) |- _ ] =>

      simpl in H; FuncInv

  | _ =>

      idtac

  end.




Ltac InvEval := InvEval1; InvEval2; InvEval2.

Correctness of the smart constructors

We now show that the code generated by "smart constructor" functions such as SelectOp.notint behaves as expected. Continuing the notint example, we show that if the expression e evaluates to some integer value Vint n, then SelectOp.notint e evaluates to a value Vint (Int.not n) which is indeed the integer negation of the value of e.

All proofs follow a common pattern:

Reasoning by case over the result of the classification functions (such as add_match for integer addition), gathering additional information on the shape of the argument expressions in the non-default cases.
Inversion of the evaluations of the arguments, exploiting the additional information thus gathered.
Equational reasoning over the arithmetic operations performed, using the lemmas from the Int and Float modules.
Construction of an evaluation derivation for the expression returned by the smart constructor.





Theorem eval_notint:

  forall le a x,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le (notint a) (Vint (Int.not x)).






Lemma eval_notbool_base:

  forall le a v b,

  eval_expr ge sp e m le a v ->

  Val.bool_of_val v b ->

  eval_expr ge sp e m le (notbool_base a) (Val.of_bool (negb b)).






Hint Resolve Val.bool_of_true_val Val.bool_of_false_val

             Val.bool_of_true_val_inv Val.bool_of_false_val_inv: valboolof.




Theorem eval_notbool:

  forall le a v b,

  eval_expr ge sp e m le a v ->

  Val.bool_of_val v b ->

  eval_expr ge sp e m le (notbool a) (Val.of_bool (negb b)).






Theorem eval_addimm:

  forall le n a x,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le (addimm n a) (Vint (Int.add x n)).






Theorem eval_addimm_ptr:

  forall le n a b ofs,

  eval_expr ge sp e m le a (Vptr b ofs) ->

  eval_expr ge sp e m le (addimm n a) (Vptr b (Int.add ofs n)).






Theorem eval_add:

  forall le a b x y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  eval_expr ge sp e m le (add a b) (Vint (Int.add x y)).






Theorem eval_add_ptr:

  forall le a b p x y,

  eval_expr ge sp e m le a (Vptr p x) ->

  eval_expr ge sp e m le b (Vint y) ->

  eval_expr ge sp e m le (add a b) (Vptr p (Int.add x y)).






Theorem eval_add_ptr_2:

  forall le a b x p y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vptr p y) ->

  eval_expr ge sp e m le (add a b) (Vptr p (Int.add y x)).






Theorem eval_sub:

  forall le a b x y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)).






Theorem eval_sub_ptr_int:

  forall le a b p x y,

  eval_expr ge sp e m le a (Vptr p x) ->

  eval_expr ge sp e m le b (Vint y) ->

  eval_expr ge sp e m le (sub a b) (Vptr p (Int.sub x y)).






Theorem eval_sub_ptr_ptr:

  forall le a b p x y,

  eval_expr ge sp e m le a (Vptr p x) ->

  eval_expr ge sp e m le b (Vptr p y) ->

  eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)).






Lemma eval_rolm:

  forall le a amount mask x,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le (rolm a amount mask) (Vint (Int.rolm x amount mask)).






Theorem eval_shlimm:

  forall le a n x,

  eval_expr ge sp e m le a (Vint x) ->

  Int.ltu n Int.iwordsize = true ->

  eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)).






Theorem eval_shruimm:

  forall le a n x,

  eval_expr ge sp e m le a (Vint x) ->

  Int.ltu n Int.iwordsize = true ->

  eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)).






Lemma eval_mulimm_base:

  forall le a n x,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le (mulimm_base n a) (Vint (Int.mul x n)).






Theorem eval_mulimm:

  forall le a n x,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le (mulimm n a) (Vint (Int.mul x n)).






Theorem eval_mul:

  forall le a b x y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  eval_expr ge sp e m le (mul a b) (Vint (Int.mul x y)).






Theorem eval_divs:

  forall le a b x y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  y <> Int.zero ->

  eval_expr ge sp e m le (divs a b) (Vint (Int.divs x y)).






Lemma eval_mod_aux:

  forall divop semdivop,

  (forall sp x y,

   y <> Int.zero ->

   eval_operation ge sp divop (Vint x :: Vint y :: nil) =

   Some (Vint (semdivop x y))) ->

  forall le a b x y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  y <> Int.zero ->

  eval_expr ge sp e m le (mod_aux divop a b)

   (Vint (Int.sub x (Int.mul (semdivop x y) y))).






Theorem eval_mods:

  forall le a b x y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  y <> Int.zero ->

  eval_expr ge sp e m le (mods a b) (Vint (Int.mods x y)).






Lemma eval_divu_base:

  forall le a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  y <> Int.zero ->

  eval_expr ge sp e m le (Eop Odivu (a ::: b ::: Enil)) (Vint (Int.divu x y)).






Theorem eval_divu:

  forall le a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  y <> Int.zero ->

  eval_expr ge sp e m le (divu a b) (Vint (Int.divu x y)).






Theorem eval_modu:

  forall le a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  y <> Int.zero ->

  eval_expr ge sp e m le (modu a b) (Vint (Int.modu x y)).






Theorem eval_andimm:

  forall le n a x,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le (andimm n a) (Vint (Int.and x n)).






Theorem eval_and:

  forall le a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  eval_expr ge sp e m le (and a b) (Vint (Int.and x y)).






Remark eval_same_expr:

  forall a1 a2 le v1 v2,

  same_expr_pure a1 a2 = true ->

  eval_expr ge sp e m le a1 v1 ->

  eval_expr ge sp e m le a2 v2 ->

  a1 = a2 /\ v1 = v2.






Lemma eval_or:

  forall le a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  eval_expr ge sp e m le (or a b) (Vint (Int.or x y)).






Theorem eval_shl:

  forall le a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  Int.ltu y Int.iwordsize = true ->

  eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)).






Theorem eval_shru:

  forall le a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  Int.ltu y Int.iwordsize = true ->

  eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)).






Theorem eval_addf:

  forall le a x b y,

  eval_expr ge sp e m le a (Vfloat x) ->

  eval_expr ge sp e m le b (Vfloat y) ->

  eval_expr ge sp e m le (addf a b) (Vfloat (Float.add x y)).






Theorem eval_subf:

  forall le a x b y,

  eval_expr ge sp e m le a (Vfloat x) ->

  eval_expr ge sp e m le b (Vfloat y) ->

  eval_expr ge sp e m le (subf a b) (Vfloat (Float.sub x y)).






Lemma loadv_cast:

  forall chunk addr v,

  loadv chunk m addr = Some v ->

  match chunk with

  | Mint8signed => loadv chunk m addr = Some(Val.sign_ext 8 v)

  | Mint8unsigned => loadv chunk m addr = Some(Val.zero_ext 8 v)

  | Mint16signed => loadv chunk m addr = Some(Val.sign_ext 16 v)

  | Mint16unsigned => loadv chunk m addr = Some(Val.zero_ext 16 v)

  | Mfloat32 => loadv chunk m addr = Some(Val.singleoffloat v)

  | _ => True

  end.






Theorem eval_cast8signed:

  forall le a v,

  eval_expr ge sp e m le a v ->

  eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v).






Theorem eval_cast8unsigned:

  forall le a v,

  eval_expr ge sp e m le a v ->

  eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v).






Theorem eval_cast16signed:

  forall le a v,

  eval_expr ge sp e m le a v ->

  eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v).






Theorem eval_cast16unsigned:

  forall le a v,

  eval_expr ge sp e m le a v ->

  eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v).






Theorem eval_singleoffloat:

  forall le a v,

  eval_expr ge sp e m le a v ->

  eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v).






Theorem eval_comp_int:

  forall le c a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x y)).






Remark eval_compare_null_transf:

  forall c x v,

  Cminor.eval_compare_null c x = Some v ->

  match eval_compare_null c x with

  | Some true => Some Vtrue

  | Some false => Some Vfalse

  | None => None (A:=val)

  end = Some v.






Theorem eval_comp_ptr_int:

  forall le c a x1 x2 b y v,

  eval_expr ge sp e m le a (Vptr x1 x2) ->

  eval_expr ge sp e m le b (Vint y) ->

  Cminor.eval_compare_null c y = Some v ->

  eval_expr ge sp e m le (comp c a b) v.






Remark eval_compare_null_swap:

  forall c x,

  Cminor.eval_compare_null (swap_comparison c) x = 

  Cminor.eval_compare_null c x.






Theorem eval_comp_int_ptr:

  forall le c a x b y1 y2 v,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vptr y1 y2) ->

  Cminor.eval_compare_null c x = Some v ->

  eval_expr ge sp e m le (comp c a b) v.






Theorem eval_comp_ptr_ptr:

  forall le c a x1 x2 b y1 y2,

  eval_expr ge sp e m le a (Vptr x1 x2) ->

  eval_expr ge sp e m le b (Vptr y1 y2) ->

  x1 = y1 ->

  eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)).






Theorem eval_comp_ptr_ptr_2:

  forall le c a x1 x2 b y1 y2 v,

  eval_expr ge sp e m le a (Vptr x1 x2) ->

  eval_expr ge sp e m le b (Vptr y1 y2) ->

  x1 <> y1 ->

  Cminor.eval_compare_mismatch c = Some v ->

  eval_expr ge sp e m le (comp c a b) v.






Theorem eval_compu:

  forall le c a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)).






Theorem eval_compf:

  forall le c a x b y,

  eval_expr ge sp e m le a (Vfloat x) ->

  eval_expr ge sp e m le b (Vfloat y) ->

  eval_expr ge sp e m le (compf c a b) (Val.of_bool(Float.cmp c x y)).






Theorem eval_negint:

  forall le a x,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le (negint a) (Vint (Int.neg x)).






Theorem eval_negf:

  forall le a x,

  eval_expr ge sp e m le a (Vfloat x) ->

  eval_expr ge sp e m le (negf a) (Vfloat (Float.neg x)).






Theorem eval_absf:

  forall le a x,

  eval_expr ge sp e m le a (Vfloat x) ->

  eval_expr ge sp e m le (absf a) (Vfloat (Float.abs x)).






Theorem eval_intoffloat:

  forall le a x,

  eval_expr ge sp e m le a (Vfloat x) ->

  eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)).






Theorem eval_intuoffloat:

  forall le a x,

  eval_expr ge sp e m le a (Vfloat x) ->

  eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)).






Theorem eval_floatofint:

  forall le a x,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)).






Theorem eval_floatofintu:

  forall le a x,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)).






Theorem eval_xor:

  forall le a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  eval_expr ge sp e m le (xor a b) (Vint (Int.xor x y)).






Theorem eval_shr:

  forall le a x b y,

  eval_expr ge sp e m le a (Vint x) ->

  eval_expr ge sp e m le b (Vint y) ->

  Int.ltu y Int.iwordsize = true ->

  eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)).






Theorem eval_mulf:

  forall le a x b y,

  eval_expr ge sp e m le a (Vfloat x) ->

  eval_expr ge sp e m le b (Vfloat y) ->

  eval_expr ge sp e m le (mulf a b) (Vfloat (Float.mul x y)).






Theorem eval_divf:

  forall le a x b y,

  eval_expr ge sp e m le a (Vfloat x) ->

  eval_expr ge sp e m le b (Vfloat y) ->

  eval_expr ge sp e m le (divf a b) (Vfloat (Float.div x y)).






Theorem eval_addressing:

  forall le chunk a v b ofs,

  eval_expr ge sp e m le a v ->

  v = Vptr b ofs ->

  match addressing chunk a with (mode, args) =>

    exists vl,

    eval_exprlist ge sp e m le args vl /\ 

    eval_addressing ge sp mode vl = Some v

  end.






End CMCONSTR.